----- Otter 3.0.3d, Feb 1995 ----- The job was started by mccune on gyro, Tue Feb 28 16:07:53 1995 ----> UNIT CONFLICT at 0.28 sec ----> 57 [binary,55.1,54.1] -> . Length of proof is 18. Level of proof is 11. ---------------- PROOF ---------------- 1 [] -> x=x. 2 [] p(A,A,B)=A, p(A,B,A)=A, p(B,A,A)=A, f(A)=A, g(A)=A -> . 4,3 [] -> p(p(x,y,y),p(x,p(y,z,f(y)),g(y)),u)=y. 5 [para_into,3.1.1.2.2,3.1.1] -> p(p(x,p(y,z,z),p(y,z,z)),p(x,z,g(p(y,z,z))),u)=p(y,z,z). 7 [para_into,5.1.1.1.2,3.1.1,demod,4,4,4] -> p(p(x,y,y),p(x,p(z,p(y,u,f(y)),g(y)),g(y)),v)=y. 10,9 [para_into,7.1.1.2,3.1.1] -> p(p(p(x,y,y),y,y),y,z)=y. 16,15 [para_into,9.1.1.1,9.1.1] -> p(x,x,y)=x. 17 [back_demod,2,demod,16,unit_del,1] p(A,B,A)=A, p(B,A,A)=A, f(A)=A, g(A)=A -> . 19,18 [para_from,9.1.1,5.1.1.2.3.1,demod,10,10,10] -> p(p(x,y,y),p(x,y,g(y)),z)=y. 22 [para_from,15.1.1,7.1.1.2.2.2] -> p(p(x,y,y),p(x,p(z,y,g(y)),g(y)),u)=y. 33,32 [para_into,18.1.1.1,18.1.1,demod,19,16,flip.1] -> p(x,y,g(y))=y. 40 [para_into,18.1.1.2,3.1.1,demod,4,16,flip.1] -> p(x,p(y,z,f(y)),g(y))=y. 42 [back_demod,22,demod,33,33] -> p(p(x,y,y),y,z)=y. 44 [para_into,40.1.1,42.1.1] -> p(x,y,f(x))=x. 47,46 [para_into,44.1.1,42.1.1,flip.1] -> p(x,y,y)=y. 48 [back_demod,17,demod,47,unit_del,1] p(A,B,A)=A, f(A)=A, g(A)=A -> . 50,49 [para_into,46.1.1,44.1.1,flip.1] -> f(x)=x. 51 [back_demod,48,demod,50,unit_del,1] p(A,B,A)=A, g(A)=A -> . 53,52 [back_demod,44,demod,50] -> p(x,y,x)=x. 54 [back_demod,51,demod,53,unit_del,1] g(A)=A -> . 55 [para_into,52.1.1,32.1.1,flip.1] -> g(x)=x. 57 [binary,55.1,54.1] -> . ------------ end of proof -------------