%
% xx=e groups are commutative.
%

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.



-------- PROOF -------- 
Length of proof is 5.  Level of proof is 4.

---------------- 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 -------------