----- Otter 3.0.6, Feb 2000 ----- ----> UNIT CONFLICT at 0.01 sec ----> 14 [binary,13.1,2.1] $F. Length of proof is 1. Level of proof is 1. ---------------- PROOF ---------------- 1 [] p(p(f1(A),A,f2(B)),B,p(C,D,p(C,E,E)))!=C. 2 [] x=x. 4,3 [] p(x,x,y)=y. 6,5 [] p(x,y,y)=x. 8,7 [] p(x,y,x)=x. 10,9 [] f1(x)=x. 12,11 [] f2(x)=x. 13 [back_demod,1,demod,10,12,4,6,8,4] C!=C. 14 [binary,13.1,2.1] $F. ------------ end of proof -------------