set(auto).

...

formula_list(usable).

all x (x=x).

all x y z (f(f(x,y),z)=f(x,f(y,z))).

exists e ((all x (f(e,x)=x))& 
          (all x exists y (f(y,x)=e))& 
          (all x (f(x,x)=e))).

-(all x y (f(x,y)=f(y,x))).

end_of_list.

-------> usable clausifies to:

list(usable).
0 [] x=x.
0 [] f(f(x,y),z)=f(x,f(y,z)).
0 [] f($c1,x)=x.
0 [] f($f1(x1),x1)=$c1.
0 [] f(x2,x2)=$c1.
0 [] f($c3,$c2)!=f($c2,$c3).
end_of_list.

...







All clauses are units, and equality is present; the
strategy will be Knuth-Bendix with positive clauses in 
sos.







---------------- PROOF ----------------

1 [] f($c3,$c2)!=f($c2,$c3).
3 [] f(f(x,y),z)=f(x,f(y,z)).
6,5 [] f($c1,x)=x.
9 [] f(x,x)=$c1.
11 [para_into,3.1.1.1,9.1.1,demod,6,flip.1] 
f(x,f(x,y))=y.
15 [para_into,3.1.1,9.1.1,flip.1] f(x,f(y,f(x,y)))=$c1.
18,17 [para_into,11.1.1.2,9.1.1] f(x,$c1)=x.
25 [para_from,15.1.1,11.1.1.2,demod,18,flip.1] 
f(x,f(y,x))=y.
29 [para_from,25.1.1,11.1.1.2] f(x,y)=f(y,x).
30 [binary,29.1,1.1] $F.

------------ end of proof -------------

----------- times (seconds) -----------
user CPU time          0.45        (0 hr, 0 min, 0 sec)