----- Otter 3.0.6, Feb 2000 -----
----> UNIT CONFLICT at   0.00 sec ----> 22 [binary,20.1,19.1] $F.

Length of proof is 10.  Level of proof is 5.

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

1 [] p(B,B,A)!=A|p(A,B,B)!=A|p(A,B,A)!=A|f(A)!=A.
2 [] x=x.
3 [] p(p(x,x,y),p(f(z),u,z),z)=y.
6,5 [para_into,3.1.1.1,3.1.1] p(x,p(f(y),z,y),y)=x.
8,7 [back_demod,3,demod,6] p(x,x,y)=y.
9 [back_demod,1,demod,8,unit_del,2] p(A,B,B)!=A|p(A,B,A)!=A|f(A)!=A.
11,10 [para_into,5.1.1.2,7.1.1] p(x,y,y)=x.
12 [para_into,5.1.1.2,5.1.1] p(x,f(y),y)=x.
14 [para_into,5.1.1,7.1.1,flip.1] p(f(x),y,x)=x.
16 [back_demod,9,demod,11,unit_del,2] p(A,B,A)!=A|f(A)!=A.
18,17 [para_into,12.1.1,7.1.1,flip.1] f(x)=x.
19 [back_demod,16,demod,18,unit_del,2] p(A,B,A)!=A.
20 [back_demod,14,demod,18] p(x,y,x)=x.
22 [binary,20.1,19.1] $F.

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