----- Otter 3.0.3d, Feb 1995 ----- The job was started by mccune on altair.mcs.anl.gov, Mon Mar 6 15:05:34 1995 ----> UNIT CONFLICT at 51.15 sec ----> 209 [binary,207.1,7.1] $Ans("g(x)=x"). Length of proof is 17. Level of proof is 12. ---------------- PROOF ---------------- 7 [] g(A)!=A|$Ans("g(x)=x"). 10,9 [] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((y^ (((((y v u)^ (v v y))^y)^w) v ((((y^u) v (v^y)) v y)^ ((((y v u)^ (v v y))^y) v w)))) v (v6^ (y v (((((y v u)^ (v v y))^y)^w) v ((((y^u) v (v^y)) v y)^ ((((y v u)^ (v v y))^y) v w))))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 12,11 [para_into,9.1.1.2.1.2.1,9.1.1] (((x^ ((y^z) v (z^ (y v z)))) v (((y^z) v (z^ (y v z)))^ (x v ((y^z) v (z^ (y v z))))))^u) v (((x^g((y^z) v (z^ (y v z)))) v (z^ (x v g((y^z) v (z^ (y v z))))))^ (((x^ ((y^z) v (z^ (y v z)))) v (((y^z) v (z^ (y v z)))^ (x v ((y^z) v (z^ (y v z)))))) v u))= (y^z) v (z^ (y v z)). 13 [para_into,11.1.1.1.1.1.2,9.1.1,demod,10,10,10,10,10,10,10,10] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((u^g(y)) v (((y^ (((((y v v)^ (w v y))^y)^v6) v ((((y^v) v (w^y)) v y)^ ((((y v v)^ (w v y))^y) v v6)))) v (v7^ (y v (((((y v v)^ (w v y))^y)^v6) v ((((y^v) v (w^y)) v y)^ ((((y v v)^ (w v y))^y) v v6))))))^ (u v g(y))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 16,15 [para_into,13.1.1.2.1,9.1.1] (((((x^y) v (y^ (x v y)))^y) v (y^ (((x^y) v (y^ (x v y))) v y)))^z) v (y^ (((((x^y) v (y^ (x v y)))^y) v (y^ (((x^y) v (y^ (x v y))) v y))) v z))=y. 20,19 [para_into,15.1.1.1.1,15.1.1,demod,16] (x^y) v (x^ (x v y))=x. 22,21 [para_from,15.1.1,11.1.1.2.1.2.2.2.1,demod,16,16,16,16,16,16,16,16] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (y^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 25 [para_from,19.1.1,13.1.1.2.1.2.1.2.1] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((u^g(y)) v (y^ (u v g(y))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 38,37 [para_into,21.1.1.1.1,21.1.1,demod,22,22,20,flip.1] (x^g(y)) v (y^ (x v g(y)))=y. 41 [para_into,21.1.1.2.1,11.1.1,demod,12,12,20,flip.1] (x^g((y^z) v (z^ (y v z)))) v (z^ (x v g((y^z) v (z^ (y v z)))))= (y^z) v (z^ (y v z)). 43 [para_into,21.1.1.2.1,9.1.1,demod,10,10,20,flip.1] (x^g(y)) v (((y^ (((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v)))) v (w^ (y v (((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v))))))^ (x v g(y)))=y. 51 [back_demod,25,demod,38,38] (((x^y) v (y^ (x v y)))^z) v (y^ (((x^y) v (y^ (x v y))) v z))=y. 72,71 [para_into,41.1.1,51.1.1,flip.1] (x^y) v (y^ (x v y))=y. 149 [para_into,43.1.1.2.1.1.2,71.1.1,demod,72] (x^g(y)) v (((y^ (((y^z) v (u^y)) v y)) v (v^ (y v (((y^z) v (u^y)) v y))))^ (x v g(y)))=y. 155 [para_into,149.1.1.2.1,71.1.1] (x^g(y)) v ((((y^z) v (u^y)) v y)^ (x v g(y)))=y. 157 [para_into,149.1.1,19.1.1] (x^ (((x^y) v (z^x)) v x)) v (u^ (x v (((x^y) v (z^x)) v x)))=x. 160,159 [para_into,155.1.1,19.1.1] ((x^y) v (z^x)) v x=x. 161 [back_demod,157,demod,160,160] (x^x) v (y^ (x v x))=x. 207 [para_into,161.1.1,37.1.1,flip.1] g(x)=x. 209 [binary,207.1,7.1] $Ans("g(x)=x"). ------------ end of proof ------------- ----> UNIT CONFLICT at 63.22 sec ----> 1098 [binary,1096.1,1.1] $Ans(idem_meet). Length of proof is 32. Level of proof is 21. ---------------- PROOF ---------------- 1 [] A^A!=A|$Ans(idem_meet). 10,9 [] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((y^ (((((y v u)^ (v v y))^y)^w) v ((((y^u) v (v^y)) v y)^ ((((y v u)^ (v v y))^y) v w)))) v (v6^ (y v (((((y v u)^ (v v y))^y)^w) v ((((y^u) v (v^y)) v y)^ ((((y v u)^ (v v y))^y) v w))))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 12,11 [para_into,9.1.1.2.1.2.1,9.1.1] (((x^ ((y^z) v (z^ (y v z)))) v (((y^z) v (z^ (y v z)))^ (x v ((y^z) v (z^ (y v z))))))^u) v (((x^g((y^z) v (z^ (y v z)))) v (z^ (x v g((y^z) v (z^ (y v z))))))^ (((x^ ((y^z) v (z^ (y v z)))) v (((y^z) v (z^ (y v z)))^ (x v ((y^z) v (z^ (y v z)))))) v u))= (y^z) v (z^ (y v z)). 13 [para_into,11.1.1.1.1.1.2,9.1.1,demod,10,10,10,10,10,10,10,10] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((u^g(y)) v (((y^ (((((y v v)^ (w v y))^y)^v6) v ((((y^v) v (w^y)) v y)^ ((((y v v)^ (w v y))^y) v v6)))) v (v7^ (y v (((((y v v)^ (w v y))^y)^v6) v ((((y^v) v (w^y)) v y)^ ((((y v v)^ (w v y))^y) v v6))))))^ (u v g(y))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 16,15 [para_into,13.1.1.2.1,9.1.1] (((((x^y) v (y^ (x v y)))^y) v (y^ (((x^y) v (y^ (x v y))) v y)))^z) v (y^ (((((x^y) v (y^ (x v y)))^y) v (y^ (((x^y) v (y^ (x v y))) v y))) v z))=y. 20,19 [para_into,15.1.1.1.1,15.1.1,demod,16] (x^y) v (x^ (x v y))=x. 22,21 [para_from,15.1.1,11.1.1.2.1.2.2.2.1,demod,16,16,16,16,16,16,16,16] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (y^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 25 [para_from,19.1.1,13.1.1.2.1.2.1.2.1] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((u^g(y)) v (y^ (u v g(y))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 38,37 [para_into,21.1.1.1.1,21.1.1,demod,22,22,20,flip.1] (x^g(y)) v (y^ (x v g(y)))=y. 41 [para_into,21.1.1.2.1,11.1.1,demod,12,12,20,flip.1] (x^g((y^z) v (z^ (y v z)))) v (z^ (x v g((y^z) v (z^ (y v z)))))= (y^z) v (z^ (y v z)). 43 [para_into,21.1.1.2.1,9.1.1,demod,10,10,20,flip.1] (x^g(y)) v (((y^ (((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v)))) v (w^ (y v (((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v))))))^ (x v g(y)))=y. 51 [back_demod,25,demod,38,38] (((x^y) v (y^ (x v y)))^z) v (y^ (((x^y) v (y^ (x v y))) v z))=y. 72,71 [para_into,41.1.1,51.1.1,flip.1] (x^y) v (y^ (x v y))=y. 85 [para_from,71.1.1,19.1.1.2.2] ((x^y)^ (y^ (x v y))) v ((x^y)^y)=x^y. 149 [para_into,43.1.1.2.1.1.2,71.1.1,demod,72] (x^g(y)) v (((y^ (((y^z) v (u^y)) v y)) v (v^ (y v (((y^z) v (u^y)) v y))))^ (x v g(y)))=y. 151 [para_into,43.1.1.2.1,71.1.1] (x^g(y)) v ((((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v)))^ (x v g(y)))=y. 155 [para_into,149.1.1.2.1,71.1.1] (x^g(y)) v ((((y^z) v (u^y)) v y)^ (x v g(y)))=y. 157 [para_into,149.1.1,19.1.1] (x^ (((x^y) v (z^x)) v x)) v (u^ (x v (((x^y) v (z^x)) v x)))=x. 160,159 [para_into,155.1.1,19.1.1] ((x^y) v (z^x)) v x=x. 161 [back_demod,157,demod,160,160] (x^x) v (y^ (x v x))=x. 165 [back_demod,151,demod,160] (x^g(y)) v ((((((y v z)^ (u v y))^y)^v) v (y^ ((((y v z)^ (u v y))^y) v v)))^ (x v g(y)))=y. 208,207 [para_into,161.1.1,37.1.1,flip.1] g(x)=x. 212 [back_demod,165,demod,208,208] (x^y) v ((((((y v z)^ (u v y))^y)^v) v (y^ ((((y v z)^ (u v y))^y) v v)))^ (x v y))=y. 292 [para_into,212.1.1.2.1,161.1.1] (x^y) v ((((y v z)^ (u v y))^y)^ (x v y))=y. 396 [para_into,292.1.1,19.1.1] ((x v y)^ (z v x))^x=x. 460 [para_into,396.1.1.1.2,159.1.1] ((x v y)^x)^x=x. 605,604 [para_into,460.1.1.1.1,19.1.1] (x^ (x^y))^ (x^y)=x^y. 647,646 [para_from,460.1.1,71.1.1.1] x v (x^ (((x v y)^x) v x))=x. 781,780 [para_from,646.1.1,396.1.1.1.1] (x^ (y v x))^x=x. 800 [para_from,646.1.1,85.1.1.1.2.2,demod,781,605] ((x^ (x^ (((x v y)^x) v x)))^x) v (x^ (((x v y)^x) v x))=x^ (x^ (((x v y)^x) v x)). 966 [para_into,780.1.1.1.2,646.1.1,demod,781] x^ (x^ (((x v y)^x) v x))=x^ (((x v y)^x) v x). 1007,1006 [para_into,780.1.1.1.2,71.1.1,demod,781] x^ (x^ (y v x))=x^ (y v x). 1021,1020 [back_demod,800,demod,1007,781,647,1007,flip.1] x^ (((x v y)^x) v x)=x. 1096 [back_demod,966,demod,1021,1021] x^x=x. 1098 [binary,1096.1,1.1] $Ans(idem_meet). ------------ end of proof ------------- ----> UNIT CONFLICT at 64.02 sec ----> 1167 [binary,1165.1,4.1] $Ans(idem_join). Length of proof is 49. Level of proof is 24. ---------------- PROOF ---------------- 4 [] A v A!=A|$Ans(idem_join). 10,9 [] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((y^ (((((y v u)^ (v v y))^y)^w) v ((((y^u) v (v^y)) v y)^ ((((y v u)^ (v v y))^y) v w)))) v (v6^ (y v (((((y v u)^ (v v y))^y)^w) v ((((y^u) v (v^y)) v y)^ ((((y v u)^ (v v y))^y) v w))))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 12,11 [para_into,9.1.1.2.1.2.1,9.1.1] (((x^ ((y^z) v (z^ (y v z)))) v (((y^z) v (z^ (y v z)))^ (x v ((y^z) v (z^ (y v z))))))^u) v (((x^g((y^z) v (z^ (y v z)))) v (z^ (x v g((y^z) v (z^ (y v z))))))^ (((x^ ((y^z) v (z^ (y v z)))) v (((y^z) v (z^ (y v z)))^ (x v ((y^z) v (z^ (y v z)))))) v u))= (y^z) v (z^ (y v z)). 13 [para_into,11.1.1.1.1.1.2,9.1.1,demod,10,10,10,10,10,10,10,10] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((u^g(y)) v (((y^ (((((y v v)^ (w v y))^y)^v6) v ((((y^v) v (w^y)) v y)^ ((((y v v)^ (w v y))^y) v v6)))) v (v7^ (y v (((((y v v)^ (w v y))^y)^v6) v ((((y^v) v (w^y)) v y)^ ((((y v v)^ (w v y))^y) v v6))))))^ (u v g(y))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 16,15 [para_into,13.1.1.2.1,9.1.1] (((((x^y) v (y^ (x v y)))^y) v (y^ (((x^y) v (y^ (x v y))) v y)))^z) v (y^ (((((x^y) v (y^ (x v y)))^y) v (y^ (((x^y) v (y^ (x v y))) v y))) v z))=y. 20,19 [para_into,15.1.1.1.1,15.1.1,demod,16] (x^y) v (x^ (x v y))=x. 22,21 [para_from,15.1.1,11.1.1.2.1.2.2.2.1,demod,16,16,16,16,16,16,16,16] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (y^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 23 [para_into,19.1.1.2.2,19.1.1] ((x^y)^ (x^ (x v y))) v ((x^y)^x)=x^y. 25 [para_from,19.1.1,13.1.1.2.1.2.1.2.1] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((u^g(y)) v (y^ (u v g(y))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 33 [para_into,23.1.1.1.2.2,19.1.1] (((x^y)^ (x^ (x v y)))^ ((x^y)^x)) v (((x^y)^ (x^ (x v y)))^ (x^y))= (x^y)^ (x^ (x v y)). 38,37 [para_into,21.1.1.1.1,21.1.1,demod,22,22,20,flip.1] (x^g(y)) v (y^ (x v g(y)))=y. 41 [para_into,21.1.1.2.1,11.1.1,demod,12,12,20,flip.1] (x^g((y^z) v (z^ (y v z)))) v (z^ (x v g((y^z) v (z^ (y v z)))))= (y^z) v (z^ (y v z)). 43 [para_into,21.1.1.2.1,9.1.1,demod,10,10,20,flip.1] (x^g(y)) v (((y^ (((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v)))) v (w^ (y v (((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v))))))^ (x v g(y)))=y. 51 [back_demod,25,demod,38,38] (((x^y) v (y^ (x v y)))^z) v (y^ (((x^y) v (y^ (x v y))) v z))=y. 72,71 [para_into,41.1.1,51.1.1,flip.1] (x^y) v (y^ (x v y))=y. 73 [para_into,71.1.1.2.2,71.1.1] ((x^y)^ (y^ (x v y))) v ((y^ (x v y))^y)=y^ (x v y). 82,81 [para_into,71.1.1.2.2,19.1.1] ((x^y)^ (x^ (x v y))) v ((x^ (x v y))^x)=x^ (x v y). 85 [para_from,71.1.1,19.1.1.2.2] ((x^y)^ (y^ (x v y))) v ((x^y)^y)=x^y. 115 [para_into,73.1.1.1.2.2,19.1.1,demod,20,20] (((x^y)^ (x^ (x v y)))^ ((x^ (x v y))^x)) v (((x^ (x v y))^x)^ (x^ (x v y)))= (x^ (x v y))^x. 133 [para_from,81.1.1,73.1.1.2.1.2,demod,82,82] ((((x^y)^ (x^ (x v y)))^ ((x^ (x v y))^x))^ (((x^ (x v y))^x)^ (x^ (x v y)))) v ((((x^ (x v y))^x)^ (x^ (x v y)))^ ((x^ (x v y))^x))= ((x^ (x v y))^x)^ (x^ (x v y)). 149 [para_into,43.1.1.2.1.1.2,71.1.1,demod,72] (x^g(y)) v (((y^ (((y^z) v (u^y)) v y)) v (v^ (y v (((y^z) v (u^y)) v y))))^ (x v g(y)))=y. 151 [para_into,43.1.1.2.1,71.1.1] (x^g(y)) v ((((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v)))^ (x v g(y)))=y. 155 [para_into,149.1.1.2.1,71.1.1] (x^g(y)) v ((((y^z) v (u^y)) v y)^ (x v g(y)))=y. 157 [para_into,149.1.1,19.1.1] (x^ (((x^y) v (z^x)) v x)) v (u^ (x v (((x^y) v (z^x)) v x)))=x. 160,159 [para_into,155.1.1,19.1.1] ((x^y) v (z^x)) v x=x. 161 [back_demod,157,demod,160,160] (x^x) v (y^ (x v x))=x. 165 [back_demod,151,demod,160] (x^g(y)) v ((((((y v z)^ (u v y))^y)^v) v (y^ ((((y v z)^ (u v y))^y) v v)))^ (x v g(y)))=y. 205 [para_from,159.1.1,71.1.1.2.2] (((x^y) v (z^x))^x) v (x^x)=x. 208,207 [para_into,161.1.1,37.1.1,flip.1] g(x)=x. 212 [back_demod,165,demod,208,208] (x^y) v ((((((y v z)^ (u v y))^y)^v) v (y^ ((((y v z)^ (u v y))^y) v v)))^ (x v y))=y. 292 [para_into,212.1.1.2.1,161.1.1] (x^y) v ((((y v z)^ (u v y))^y)^ (x v y))=y. 396 [para_into,292.1.1,19.1.1] ((x v y)^ (z v x))^x=x. 460 [para_into,396.1.1.1.2,159.1.1] ((x v y)^x)^x=x. 512 [para_from,396.1.1,205.1.1.1.1.2] (((x^y) v x)^x) v (x^x)=x. 605,604 [para_into,460.1.1.1.1,19.1.1] (x^ (x^y))^ (x^y)=x^y. 647,646 [para_from,460.1.1,71.1.1.1] x v (x^ (((x v y)^x) v x))=x. 779,778 [para_from,646.1.1,460.1.1.1.1] (x^x)^x=x. 781,780 [para_from,646.1.1,396.1.1.1.1] (x^ (y v x))^x=x. 782 [para_from,646.1.1,133.1.1.2.1.2.2,demod,647,647,779,647,779,647,647,779,647,779,647,779,647] ((((x^ (x^ (((x v y)^x) v x)))^ (x^x))^x)^ (x^ (x^x))) v ((x^ (x^x))^x)=x^ (x^x). 784 [para_from,646.1.1,115.1.1.2.2.2,demod,647,647,779,647,779,647,779] (((x^ (x^ (((x v y)^x) v x)))^ (x^x))^x) v (x^ (x^x))=x. 790 [para_from,646.1.1,33.1.1.2.1.2.2,demod,647,647] (((x^ (x^ (((x v y)^x) v x)))^ (x^x))^ ((x^ (x^ (((x v y)^x) v x)))^x)) v (((x^ (x^ (((x v y)^x) v x)))^ (x^x))^ (x^ (x^ (((x v y)^x) v x))))= (x^ (x^ (((x v y)^x) v x)))^ (x^x). 800 [para_from,646.1.1,85.1.1.1.2.2,demod,781,605] ((x^ (x^ (((x v y)^x) v x)))^x) v (x^ (((x v y)^x) v x))=x^ (x^ (((x v y)^x) v x)). 966 [para_into,780.1.1.1.2,646.1.1,demod,781] x^ (x^ (((x v y)^x) v x))=x^ (((x v y)^x) v x). 969,968 [para_into,780.1.1.1.2,512.1.1,demod,779] x^ (x^x)=x^x. 1007,1006 [para_into,780.1.1.1.2,71.1.1,demod,781] x^ (x^ (y v x))=x^ (y v x). 1021,1020 [back_demod,800,demod,1007,781,647,1007,flip.1] x^ (((x v y)^x) v x)=x. 1029,1028 [back_demod,790,demod,1021,1021,779,1021,1021,779,1021] (((x^x)^ (x^x))^x) v (x^x)= (x^x)^ (x^x). 1033,1032 [back_demod,784,demod,1021,969,1029] (x^x)^ (x^x)=x. 1034 [back_demod,782,demod,1021,1033,969,1033,969,779,969] x v x=x^x. 1097,1096 [back_demod,966,demod,1021,1021] x^x=x. 1165 [back_demod,1034,demod,1097] x v x=x. 1167 [binary,1165.1,4.1] $Ans(idem_join). ------------ end of proof ------------- ----> UNIT CONFLICT at 65.88 sec ----> 1288 [binary,1286.1,6.1] $Ans(a3_join). Length of proof is 72. Level of proof is 29. ---------------- PROOF ---------------- 6 [] ((A^C) v (B^C)) v C!=C|$Ans(a3_join). 10,9 [] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((y^ (((((y v u)^ (v v y))^y)^w) v ((((y^u) v (v^y)) v y)^ ((((y v u)^ (v v y))^y) v w)))) v (v6^ (y v (((((y v u)^ (v v y))^y)^w) v ((((y^u) v (v^y)) v y)^ ((((y v u)^ (v v y))^y) v w))))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 12,11 [para_into,9.1.1.2.1.2.1,9.1.1] (((x^ ((y^z) v (z^ (y v z)))) v (((y^z) v (z^ (y v z)))^ (x v ((y^z) v (z^ (y v z))))))^u) v (((x^g((y^z) v (z^ (y v z)))) v (z^ (x v g((y^z) v (z^ (y v z))))))^ (((x^ ((y^z) v (z^ (y v z)))) v (((y^z) v (z^ (y v z)))^ (x v ((y^z) v (z^ (y v z)))))) v u))= (y^z) v (z^ (y v z)). 13 [para_into,11.1.1.1.1.1.2,9.1.1,demod,10,10,10,10,10,10,10,10] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((u^g(y)) v (((y^ (((((y v v)^ (w v y))^y)^v6) v ((((y^v) v (w^y)) v y)^ ((((y v v)^ (w v y))^y) v v6)))) v (v7^ (y v (((((y v v)^ (w v y))^y)^v6) v ((((y^v) v (w^y)) v y)^ ((((y v v)^ (w v y))^y) v v6))))))^ (u v g(y))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 16,15 [para_into,13.1.1.2.1,9.1.1] (((((x^y) v (y^ (x v y)))^y) v (y^ (((x^y) v (y^ (x v y))) v y)))^z) v (y^ (((((x^y) v (y^ (x v y)))^y) v (y^ (((x^y) v (y^ (x v y))) v y))) v z))=y. 20,19 [para_into,15.1.1.1.1,15.1.1,demod,16] (x^y) v (x^ (x v y))=x. 22,21 [para_from,15.1.1,11.1.1.2.1.2.2.2.1,demod,16,16,16,16,16,16,16,16] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (y^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 23 [para_into,19.1.1.2.2,19.1.1] ((x^y)^ (x^ (x v y))) v ((x^y)^x)=x^y. 25 [para_from,19.1.1,13.1.1.2.1.2.1.2.1] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((u^g(y)) v (y^ (u v g(y))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 33 [para_into,23.1.1.1.2.2,19.1.1] (((x^y)^ (x^ (x v y)))^ ((x^y)^x)) v (((x^y)^ (x^ (x v y)))^ (x^y))= (x^y)^ (x^ (x v y)). 38,37 [para_into,21.1.1.1.1,21.1.1,demod,22,22,20,flip.1] (x^g(y)) v (y^ (x v g(y)))=y. 41 [para_into,21.1.1.2.1,11.1.1,demod,12,12,20,flip.1] (x^g((y^z) v (z^ (y v z)))) v (z^ (x v g((y^z) v (z^ (y v z)))))= (y^z) v (z^ (y v z)). 43 [para_into,21.1.1.2.1,9.1.1,demod,10,10,20,flip.1] (x^g(y)) v (((y^ (((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v)))) v (w^ (y v (((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v))))))^ (x v g(y)))=y. 51 [back_demod,25,demod,38,38] (((x^y) v (y^ (x v y)))^z) v (y^ (((x^y) v (y^ (x v y))) v z))=y. 72,71 [para_into,41.1.1,51.1.1,flip.1] (x^y) v (y^ (x v y))=y. 73 [para_into,71.1.1.2.2,71.1.1] ((x^y)^ (y^ (x v y))) v ((y^ (x v y))^y)=y^ (x v y). 82,81 [para_into,71.1.1.2.2,19.1.1] ((x^y)^ (x^ (x v y))) v ((x^ (x v y))^x)=x^ (x v y). 85 [para_from,71.1.1,19.1.1.2.2] ((x^y)^ (y^ (x v y))) v ((x^y)^y)=x^y. 101 [para_from,85.1.1,71.1.1.2.2] (((x^y)^ (y^ (x v y)))^ ((x^y)^y)) v (((x^y)^y)^ (x^y))= (x^y)^y. 107 [para_into,73.1.1.1.2.2,71.1.1,demod,72,72] (((x^y)^ (y^ (x v y)))^ ((y^ (x v y))^y)) v (((y^ (x v y))^y)^ (y^ (x v y)))= (y^ (x v y))^y. 115 [para_into,73.1.1.1.2.2,19.1.1,demod,20,20] (((x^y)^ (x^ (x v y)))^ ((x^ (x v y))^x)) v (((x^ (x v y))^x)^ (x^ (x v y)))= (x^ (x v y))^x. 133 [para_from,81.1.1,73.1.1.2.1.2,demod,82,82] ((((x^y)^ (x^ (x v y)))^ ((x^ (x v y))^x))^ (((x^ (x v y))^x)^ (x^ (x v y)))) v ((((x^ (x v y))^x)^ (x^ (x v y)))^ ((x^ (x v y))^x))= ((x^ (x v y))^x)^ (x^ (x v y)). 149 [para_into,43.1.1.2.1.1.2,71.1.1,demod,72] (x^g(y)) v (((y^ (((y^z) v (u^y)) v y)) v (v^ (y v (((y^z) v (u^y)) v y))))^ (x v g(y)))=y. 151 [para_into,43.1.1.2.1,71.1.1] (x^g(y)) v ((((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v)))^ (x v g(y)))=y. 155 [para_into,149.1.1.2.1,71.1.1] (x^g(y)) v ((((y^z) v (u^y)) v y)^ (x v g(y)))=y. 157 [para_into,149.1.1,19.1.1] (x^ (((x^y) v (z^x)) v x)) v (u^ (x v (((x^y) v (z^x)) v x)))=x. 160,159 [para_into,155.1.1,19.1.1] ((x^y) v (z^x)) v x=x. 162,161 [back_demod,157,demod,160,160] (x^x) v (y^ (x v x))=x. 165 [back_demod,151,demod,160] (x^g(y)) v ((((((y v z)^ (u v y))^y)^v) v (y^ ((((y v z)^ (u v y))^y) v v)))^ (x v g(y)))=y. 205 [para_from,159.1.1,71.1.1.2.2] (((x^y) v (z^x))^x) v (x^x)=x. 208,207 [para_into,161.1.1,37.1.1,flip.1] g(x)=x. 212 [back_demod,165,demod,208,208] (x^y) v ((((((y v z)^ (u v y))^y)^v) v (y^ ((((y v z)^ (u v y))^y) v v)))^ (x v y))=y. 230 [para_from,161.1.1,107.1.1.2.2.2,demod,162,162,162,162] ((((x^x)^ (y^ (x v x)))^ ((y^ (x v x))^x))^ (((y^ (x v x))^x)^ (y^ (x v x)))) v ((((y^ (x v x))^x)^ (y^ (x v x)))^ ((y^ (x v x))^x))= ((y^ (x v x))^x)^ (y^ (x v x)). 234 [para_from,161.1.1,73.1.1.2.1.2,demod,162,162] (((x^x)^ (y^ (x v x)))^ ((y^ (x v x))^x)) v (((y^ (x v x))^x)^ (y^ (x v x)))= (y^ (x v x))^x. 236 [para_from,161.1.1,85.1.1.1.2.2] (((x^x)^ (y^ (x v x)))^ ((y^ (x v x))^x)) v (((x^x)^ (y^ (x v x)))^ (y^ (x v x)))= (x^x)^ (y^ (x v x)). 242 [para_from,161.1.1,71.1.1.2.2] ((x^x)^ (y^ (x v x))) v ((y^ (x v x))^x)=y^ (x v x). 292 [para_into,212.1.1.2.1,161.1.1] (x^y) v ((((y v z)^ (u v y))^y)^ (x v y))=y. 396 [para_into,292.1.1,19.1.1] ((x v y)^ (z v x))^x=x. 460 [para_into,396.1.1.1.2,159.1.1] ((x v y)^x)^x=x. 512 [para_from,396.1.1,205.1.1.1.1.2] (((x^y) v x)^x) v (x^x)=x. 599,598 [para_into,460.1.1.1.1,71.1.1] (x^ (y^x))^ (y^x)=y^x. 605,604 [para_into,460.1.1.1.1,19.1.1] (x^ (x^y))^ (x^y)=x^y. 647,646 [para_from,460.1.1,71.1.1.1] x v (x^ (((x v y)^x) v x))=x. 779,778 [para_from,646.1.1,460.1.1.1.1] (x^x)^x=x. 781,780 [para_from,646.1.1,396.1.1.1.1] (x^ (y v x))^x=x. 782 [para_from,646.1.1,133.1.1.2.1.2.2,demod,647,647,779,647,779,647,647,779,647,779,647,779,647] ((((x^ (x^ (((x v y)^x) v x)))^ (x^x))^x)^ (x^ (x^x))) v ((x^ (x^x))^x)=x^ (x^x). 784 [para_from,646.1.1,115.1.1.2.2.2,demod,647,647,779,647,779,647,779] (((x^ (x^ (((x v y)^x) v x)))^ (x^x))^x) v (x^ (x^x))=x. 790 [para_from,646.1.1,33.1.1.2.1.2.2,demod,647,647] (((x^ (x^ (((x v y)^x) v x)))^ (x^x))^ ((x^ (x^ (((x v y)^x) v x)))^x)) v (((x^ (x^ (((x v y)^x) v x)))^ (x^x))^ (x^ (x^ (((x v y)^x) v x))))= (x^ (x^ (((x v y)^x) v x)))^ (x^x). 800 [para_from,646.1.1,85.1.1.1.2.2,demod,781,605] ((x^ (x^ (((x v y)^x) v x)))^x) v (x^ (((x v y)^x) v x))=x^ (x^ (((x v y)^x) v x)). 966 [para_into,780.1.1.1.2,646.1.1,demod,781] x^ (x^ (((x v y)^x) v x))=x^ (((x v y)^x) v x). 969,968 [para_into,780.1.1.1.2,512.1.1,demod,779] x^ (x^x)=x^x. 972 [para_into,780.1.1.1.2,242.1.1] (((x^ (y v y))^y)^ (x^ (y v y)))^ ((x^ (y v y))^y)= (x^ (y v y))^y. 976 [para_into,780.1.1.1.2,161.1.1] ((x^ (y v y))^y)^ (x^ (y v y))=x^ (y v y). 990 [para_into,780.1.1.1.2,101.1.1] ((((x^y)^y)^ (x^y))^ ((x^y)^y))^ (((x^y)^y)^ (x^y))= ((x^y)^y)^ (x^y). 999,998 [para_into,780.1.1.1.2,85.1.1] (((x^y)^y)^ (x^y))^ ((x^y)^y)= (x^y)^y. 1007,1006 [para_into,780.1.1.1.2,71.1.1,demod,781] x^ (x^ (y v x))=x^ (y v x). 1021,1020 [back_demod,800,demod,1007,781,647,1007,flip.1] x^ (((x v y)^x) v x)=x. 1029,1028 [back_demod,790,demod,1021,1021,779,1021,1021,779,1021] (((x^x)^ (x^x))^x) v (x^x)= (x^x)^ (x^x). 1033,1032 [back_demod,784,demod,1021,969,1029] (x^x)^ (x^x)=x. 1035,1034 [back_demod,782,demod,1021,1033,969,1033,969,779,969] x v x=x^x. 1064 [back_demod,230,demod,1035,1035,1035,1035,1035,1035,1035,1035,1035] ((((x^x)^ (y^ (x^x)))^ ((y^ (x^x))^x))^ (((y^ (x^x))^x)^ (y^ (x^x)))) v ((((y^ (x^x))^x)^ (y^ (x^x)))^ ((y^ (x^x))^x))= ((y^ (x^x))^x)^ (y^ (x^x)). 1066 [back_demod,972,demod,1035,1035,1035,1035] (((x^ (y^y))^y)^ (x^ (y^y)))^ ((x^ (y^y))^y)= (x^ (y^y))^y. 1068 [back_demod,234,demod,1035,1035,1035,1035,1035] (((x^x)^ (y^ (x^x)))^ ((y^ (x^x))^x)) v (((y^ (x^x))^x)^ (y^ (x^x)))= (y^ (x^x))^x. 1078 [back_demod,990,demod,999] ((x^y)^y)^ (((x^y)^y)^ (x^y))= ((x^y)^y)^ (x^y). 1097,1096 [back_demod,966,demod,1021,1021] x^x=x. 1124,1123 [back_demod,976,demod,1035,1097,1035,1097,1035,1097] ((x^y)^y)^ (x^y)=x^y. 1150,1149 [back_demod,236,demod,1097,1035,1097,1035,1097,1097,1035,1097,1035,1097,599,1097,1035,1097] ((x^ (y^x))^ ((y^x)^x)) v (y^x)=x^ (y^x). 1153 [back_demod,1064,demod,1097,1097,1097,1097,1097,1124,1097,1097,1124,1097,1097,1097,1124] (((x^ (y^x))^ ((y^x)^x))^ (y^x)) v ((y^x)^ ((y^x)^x))=y^x. 1162,1161 [back_demod,1068,demod,1097,1097,1097,1097,1097,1124,1150,1097,flip.1] (x^y)^y=y^ (x^y). 1164,1163 [back_demod,1066,demod,1097,1162,1097,1162,1097,1162,1162,1097,1162] (x^ (y^x))^ ((y^x)^ (x^ (y^x)))=x^ (y^x). 1166,1165 [back_demod,1034,demod,1097] x v x=x. 1179,1178 [back_demod,1078,demod,1162,1162,1162,1164,1162,1162,flip.1] (x^y)^ (y^ (x^y))=y^ (x^y). 1190 [back_demod,1153,demod,1162,1097,1162,1179,1162,1179,1166] x^ (y^x)=y^x. 1286 [para_from,1190.1.1,159.1.1.1.1] ((x^y) v (z^y)) v y=y. 1288 [binary,1286.1,6.1] $Ans(a3_join). ------------ end of proof ------------- ----> UNIT CONFLICT at 67.73 sec ----> 1427 [binary,1425.1,3.1] $Ans(a3_meet). Length of proof is 90. Level of proof is 34. ---------------- PROOF ---------------- 3 [] ((A v C)^ (B v C))^C!=C|$Ans(a3_meet). 10,9 [] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((y^ (((((y v u)^ (v v y))^y)^w) v ((((y^u) v (v^y)) v y)^ ((((y v u)^ (v v y))^y) v w)))) v (v6^ (y v (((((y v u)^ (v v y))^y)^w) v ((((y^u) v (v^y)) v y)^ ((((y v u)^ (v v y))^y) v w))))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 12,11 [para_into,9.1.1.2.1.2.1,9.1.1] (((x^ ((y^z) v (z^ (y v z)))) v (((y^z) v (z^ (y v z)))^ (x v ((y^z) v (z^ (y v z))))))^u) v (((x^g((y^z) v (z^ (y v z)))) v (z^ (x v g((y^z) v (z^ (y v z))))))^ (((x^ ((y^z) v (z^ (y v z)))) v (((y^z) v (z^ (y v z)))^ (x v ((y^z) v (z^ (y v z)))))) v u))= (y^z) v (z^ (y v z)). 13 [para_into,11.1.1.1.1.1.2,9.1.1,demod,10,10,10,10,10,10,10,10] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((u^g(y)) v (((y^ (((((y v v)^ (w v y))^y)^v6) v ((((y^v) v (w^y)) v y)^ ((((y v v)^ (w v y))^y) v v6)))) v (v7^ (y v (((((y v v)^ (w v y))^y)^v6) v ((((y^v) v (w^y)) v y)^ ((((y v v)^ (w v y))^y) v v6))))))^ (u v g(y))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 16,15 [para_into,13.1.1.2.1,9.1.1] (((((x^y) v (y^ (x v y)))^y) v (y^ (((x^y) v (y^ (x v y))) v y)))^z) v (y^ (((((x^y) v (y^ (x v y)))^y) v (y^ (((x^y) v (y^ (x v y))) v y))) v z))=y. 20,19 [para_into,15.1.1.1.1,15.1.1,demod,16] (x^y) v (x^ (x v y))=x. 22,21 [para_from,15.1.1,11.1.1.2.1.2.2.2.1,demod,16,16,16,16,16,16,16,16] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (y^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 23 [para_into,19.1.1.2.2,19.1.1] ((x^y)^ (x^ (x v y))) v ((x^y)^x)=x^y. 25 [para_from,19.1.1,13.1.1.2.1.2.1.2.1] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((u^g(y)) v (y^ (u v g(y))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 33 [para_into,23.1.1.1.2.2,19.1.1] (((x^y)^ (x^ (x v y)))^ ((x^y)^x)) v (((x^y)^ (x^ (x v y)))^ (x^y))= (x^y)^ (x^ (x v y)). 38,37 [para_into,21.1.1.1.1,21.1.1,demod,22,22,20,flip.1] (x^g(y)) v (y^ (x v g(y)))=y. 41 [para_into,21.1.1.2.1,11.1.1,demod,12,12,20,flip.1] (x^g((y^z) v (z^ (y v z)))) v (z^ (x v g((y^z) v (z^ (y v z)))))= (y^z) v (z^ (y v z)). 43 [para_into,21.1.1.2.1,9.1.1,demod,10,10,20,flip.1] (x^g(y)) v (((y^ (((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v)))) v (w^ (y v (((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v))))))^ (x v g(y)))=y. 51 [back_demod,25,demod,38,38] (((x^y) v (y^ (x v y)))^z) v (y^ (((x^y) v (y^ (x v y))) v z))=y. 72,71 [para_into,41.1.1,51.1.1,flip.1] (x^y) v (y^ (x v y))=y. 73 [para_into,71.1.1.2.2,71.1.1] ((x^y)^ (y^ (x v y))) v ((y^ (x v y))^y)=y^ (x v y). 82,81 [para_into,71.1.1.2.2,19.1.1] ((x^y)^ (x^ (x v y))) v ((x^ (x v y))^x)=x^ (x v y). 85 [para_from,71.1.1,19.1.1.2.2] ((x^y)^ (y^ (x v y))) v ((x^y)^y)=x^y. 89 [para_into,85.1.1.1.2.2,71.1.1] (((x^y)^ (y^ (x v y)))^ ((y^ (x v y))^y)) v (((x^y)^ (y^ (x v y)))^ (y^ (x v y)))= (x^y)^ (y^ (x v y)). 101 [para_from,85.1.1,71.1.1.2.2] (((x^y)^ (y^ (x v y)))^ ((x^y)^y)) v (((x^y)^y)^ (x^y))= (x^y)^y. 107 [para_into,73.1.1.1.2.2,71.1.1,demod,72,72] (((x^y)^ (y^ (x v y)))^ ((y^ (x v y))^y)) v (((y^ (x v y))^y)^ (y^ (x v y)))= (y^ (x v y))^y. 115 [para_into,73.1.1.1.2.2,19.1.1,demod,20,20] (((x^y)^ (x^ (x v y)))^ ((x^ (x v y))^x)) v (((x^ (x v y))^x)^ (x^ (x v y)))= (x^ (x v y))^x. 133 [para_from,81.1.1,73.1.1.2.1.2,demod,82,82] ((((x^y)^ (x^ (x v y)))^ ((x^ (x v y))^x))^ (((x^ (x v y))^x)^ (x^ (x v y)))) v ((((x^ (x v y))^x)^ (x^ (x v y)))^ ((x^ (x v y))^x))= ((x^ (x v y))^x)^ (x^ (x v y)). 149 [para_into,43.1.1.2.1.1.2,71.1.1,demod,72] (x^g(y)) v (((y^ (((y^z) v (u^y)) v y)) v (v^ (y v (((y^z) v (u^y)) v y))))^ (x v g(y)))=y. 151 [para_into,43.1.1.2.1,71.1.1] (x^g(y)) v ((((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v)))^ (x v g(y)))=y. 155 [para_into,149.1.1.2.1,71.1.1] (x^g(y)) v ((((y^z) v (u^y)) v y)^ (x v g(y)))=y. 157 [para_into,149.1.1,19.1.1] (x^ (((x^y) v (z^x)) v x)) v (u^ (x v (((x^y) v (z^x)) v x)))=x. 160,159 [para_into,155.1.1,19.1.1] ((x^y) v (z^x)) v x=x. 162,161 [back_demod,157,demod,160,160] (x^x) v (y^ (x v x))=x. 165 [back_demod,151,demod,160] (x^g(y)) v ((((((y v z)^ (u v y))^y)^v) v (y^ ((((y v z)^ (u v y))^y) v v)))^ (x v g(y)))=y. 205 [para_from,159.1.1,71.1.1.2.2] (((x^y) v (z^x))^x) v (x^x)=x. 208,207 [para_into,161.1.1,37.1.1,flip.1] g(x)=x. 212 [back_demod,165,demod,208,208] (x^y) v ((((((y v z)^ (u v y))^y)^v) v (y^ ((((y v z)^ (u v y))^y) v v)))^ (x v y))=y. 228 [para_from,161.1.1,19.1.1.2.2] ((x^x)^ (y^ (x v x))) v ((x^x)^x)=x^x. 230 [para_from,161.1.1,107.1.1.2.2.2,demod,162,162,162,162] ((((x^x)^ (y^ (x v x)))^ ((y^ (x v x))^x))^ (((y^ (x v x))^x)^ (y^ (x v x)))) v ((((y^ (x v x))^x)^ (y^ (x v x)))^ ((y^ (x v x))^x))= ((y^ (x v x))^x)^ (y^ (x v x)). 234 [para_from,161.1.1,73.1.1.2.1.2,demod,162,162] (((x^x)^ (y^ (x v x)))^ ((y^ (x v x))^x)) v (((y^ (x v x))^x)^ (y^ (x v x)))= (y^ (x v x))^x. 236 [para_from,161.1.1,85.1.1.1.2.2] (((x^x)^ (y^ (x v x)))^ ((y^ (x v x))^x)) v (((x^x)^ (y^ (x v x)))^ (y^ (x v x)))= (x^x)^ (y^ (x v x)). 242 [para_from,161.1.1,71.1.1.2.2] ((x^x)^ (y^ (x v x))) v ((y^ (x v x))^x)=y^ (x v x). 292 [para_into,212.1.1.2.1,161.1.1] (x^y) v ((((y v z)^ (u v y))^y)^ (x v y))=y. 397,396 [para_into,292.1.1,19.1.1] ((x v y)^ (z v x))^x=x. 460 [para_into,396.1.1.1.2,159.1.1] ((x v y)^x)^x=x. 512 [para_from,396.1.1,205.1.1.1.1.2] (((x^y) v x)^x) v (x^x)=x. 518 [para_from,396.1.1,159.1.1.1.2] ((x^y) v x) v x=x. 540 [para_from,396.1.1,89.1.1.2.1.1,demod,397,397] ((x^ (x^ (((x v y)^ (z v x)) v x)))^ ((x^ (((x v y)^ (z v x)) v x))^x)) v ((x^ (x^ (((x v y)^ (z v x)) v x)))^ (x^ (((x v y)^ (z v x)) v x)))=x^ (x^ (((x v y)^ (z v x)) v x)). 547,546 [para_from,396.1.1,71.1.1.1] x v (x^ (((x v y)^ (z v x)) v x))=x. 599,598 [para_into,460.1.1.1.1,71.1.1] (x^ (y^x))^ (y^x)=y^x. 605,604 [para_into,460.1.1.1.1,19.1.1] (x^ (x^y))^ (x^y)=x^y. 606 [back_demod,540,demod,605] ((x^ (x^ (((x v y)^ (z v x)) v x)))^ ((x^ (((x v y)^ (z v x)) v x))^x)) v (x^ (((x v y)^ (z v x)) v x))=x^ (x^ (((x v y)^ (z v x)) v x)). 647,646 [para_from,460.1.1,71.1.1.1] x v (x^ (((x v y)^x) v x))=x. 702 [para_from,518.1.1,460.1.1.1.1] (x^ ((x^y) v x))^ ((x^y) v x)= (x^y) v x. 779,778 [para_from,646.1.1,460.1.1.1.1] (x^x)^x=x. 781,780 [para_from,646.1.1,396.1.1.1.1] (x^ (y v x))^x=x. 782 [para_from,646.1.1,133.1.1.2.1.2.2,demod,647,647,779,647,779,647,647,779,647,779,647,779,647] ((((x^ (x^ (((x v y)^x) v x)))^ (x^x))^x)^ (x^ (x^x))) v ((x^ (x^x))^x)=x^ (x^x). 784 [para_from,646.1.1,115.1.1.2.2.2,demod,647,647,779,647,779,647,779] (((x^ (x^ (((x v y)^x) v x)))^ (x^x))^x) v (x^ (x^x))=x. 790 [para_from,646.1.1,33.1.1.2.1.2.2,demod,647,647] (((x^ (x^ (((x v y)^x) v x)))^ (x^x))^ ((x^ (x^ (((x v y)^x) v x)))^x)) v (((x^ (x^ (((x v y)^x) v x)))^ (x^x))^ (x^ (x^ (((x v y)^x) v x))))= (x^ (x^ (((x v y)^x) v x)))^ (x^x). 800 [para_from,646.1.1,85.1.1.1.2.2,demod,781,605] ((x^ (x^ (((x v y)^x) v x)))^x) v (x^ (((x v y)^x) v x))=x^ (x^ (((x v y)^x) v x)). 860 [back_demod,228,demod,779] ((x^x)^ (y^ (x v x))) v x=x^x. 884 [back_demod,606,demod,781] ((x^ (x^ (((x v y)^ (z v x)) v x)))^x) v (x^ (((x v y)^ (z v x)) v x))=x^ (x^ (((x v y)^ (z v x)) v x)). 966 [para_into,780.1.1.1.2,646.1.1,demod,781] x^ (x^ (((x v y)^x) v x))=x^ (((x v y)^x) v x). 969,968 [para_into,780.1.1.1.2,512.1.1,demod,779] x^ (x^x)=x^x. 972 [para_into,780.1.1.1.2,242.1.1] (((x^ (y v y))^y)^ (x^ (y v y)))^ ((x^ (y v y))^y)= (x^ (y v y))^y. 976 [para_into,780.1.1.1.2,161.1.1] ((x^ (y v y))^y)^ (x^ (y v y))=x^ (y v y). 990 [para_into,780.1.1.1.2,101.1.1] ((((x^y)^y)^ (x^y))^ ((x^y)^y))^ (((x^y)^y)^ (x^y))= ((x^y)^y)^ (x^y). 999,998 [para_into,780.1.1.1.2,85.1.1] (((x^y)^y)^ (x^y))^ ((x^y)^y)= (x^y)^y. 1007,1006 [para_into,780.1.1.1.2,71.1.1,demod,781] x^ (x^ (y v x))=x^ (y v x). 1021,1020 [back_demod,800,demod,1007,781,647,1007,flip.1] x^ (((x v y)^x) v x)=x. 1029,1028 [back_demod,790,demod,1021,1021,779,1021,1021,779,1021] (((x^x)^ (x^x))^x) v (x^x)= (x^x)^ (x^x). 1033,1032 [back_demod,784,demod,1021,969,1029] (x^x)^ (x^x)=x. 1035,1034 [back_demod,782,demod,1021,1033,969,1033,969,779,969] x v x=x^x. 1064 [back_demod,230,demod,1035,1035,1035,1035,1035,1035,1035,1035,1035] ((((x^x)^ (y^ (x^x)))^ ((y^ (x^x))^x))^ (((y^ (x^x))^x)^ (y^ (x^x)))) v ((((y^ (x^x))^x)^ (y^ (x^x)))^ ((y^ (x^x))^x))= ((y^ (x^x))^x)^ (y^ (x^x)). 1066 [back_demod,972,demod,1035,1035,1035,1035] (((x^ (y^y))^y)^ (x^ (y^y)))^ ((x^ (y^y))^y)= (x^ (y^y))^y. 1068 [back_demod,234,demod,1035,1035,1035,1035,1035] (((x^x)^ (y^ (x^x)))^ ((y^ (x^x))^x)) v (((y^ (x^x))^x)^ (y^ (x^x)))= (y^ (x^x))^x. 1078 [back_demod,990,demod,999] ((x^y)^y)^ (((x^y)^y)^ (x^y))= ((x^y)^y)^ (x^y). 1097,1096 [back_demod,966,demod,1021,1021] x^x=x. 1107 [back_demod,884,demod,1007,781,547,1007,flip.1] x^ (((x v y)^ (z v x)) v x)=x. 1124,1123 [back_demod,976,demod,1035,1097,1035,1097,1035,1097] ((x^y)^y)^ (x^y)=x^y. 1133 [back_demod,860,demod,1097,1035,1097,1097] (x^ (y^x)) v x=x. 1150,1149 [back_demod,236,demod,1097,1035,1097,1035,1097,1097,1035,1097,1035,1097,599,1097,1035,1097] ((x^ (y^x))^ ((y^x)^x)) v (y^x)=x^ (y^x). 1153 [back_demod,1064,demod,1097,1097,1097,1097,1097,1124,1097,1097,1124,1097,1097,1097,1124] (((x^ (y^x))^ ((y^x)^x))^ (y^x)) v ((y^x)^ ((y^x)^x))=y^x. 1162,1161 [back_demod,1068,demod,1097,1097,1097,1097,1097,1124,1150,1097,flip.1] (x^y)^y=y^ (x^y). 1164,1163 [back_demod,1066,demod,1097,1162,1097,1162,1097,1162,1162,1097,1162] (x^ (y^x))^ ((y^x)^ (x^ (y^x)))=x^ (y^x). 1166,1165 [back_demod,1034,demod,1097] x v x=x. 1179,1178 [back_demod,1078,demod,1162,1162,1162,1164,1162,1162,flip.1] (x^y)^ (y^ (x^y))=y^ (x^y). 1191,1190 [back_demod,1153,demod,1162,1097,1162,1179,1162,1179,1166] x^ (y^x)=y^x. 1203,1202 [back_demod,702,demod,1162,1191] x^ ((x^y) v x)= (x^y) v x. 1222 [back_demod,1133,demod,1191] (x^y) v y=y. 1238 [para_from,780.1.1,71.1.1.1,demod,1203] x v ((x^ (y v x)) v x)=x. 1248 [para_from,780.1.1,19.1.1.1] x v ((x^ (y v x))^ ((x^ (y v x)) v x))=x^ (y v x). 1352,1351 [para_into,1107.1.1.2.1.1,1238.1.1,demod,1203] (x^ (y v x)) v x=x. 1379 [back_demod,1248,demod,1352,781,1166,flip.1] x^ (y v x)=x. 1405 [para_from,1379.1.1,1222.1.1.1] x v (y v x)=y v x. 1425 [para_from,1405.1.1,396.1.1.1.1] ((x v y)^ (z v y))^y=y. 1427 [binary,1425.1,3.1] $Ans(a3_meet). ------------ end of proof ------------- ----> UNIT CONFLICT at 69.54 sec ----> 1687 [binary,1686.1,2.1] $Ans(comm_meet). Length of proof is 106. Level of proof is 40. ---------------- PROOF ---------------- 2 [] A^B!=B^A|$Ans(comm_meet). 10,9 [] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((y^ (((((y v u)^ (v v y))^y)^w) v ((((y^u) v (v^y)) v y)^ ((((y v u)^ (v v y))^y) v w)))) v (v6^ (y v (((((y v u)^ (v v y))^y)^w) v ((((y^u) v (v^y)) v y)^ ((((y v u)^ (v v y))^y) v w))))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 12,11 [para_into,9.1.1.2.1.2.1,9.1.1] (((x^ ((y^z) v (z^ (y v z)))) v (((y^z) v (z^ (y v z)))^ (x v ((y^z) v (z^ (y v z))))))^u) v (((x^g((y^z) v (z^ (y v z)))) v (z^ (x v g((y^z) v (z^ (y v z))))))^ (((x^ ((y^z) v (z^ (y v z)))) v (((y^z) v (z^ (y v z)))^ (x v ((y^z) v (z^ (y v z)))))) v u))= (y^z) v (z^ (y v z)). 13 [para_into,11.1.1.1.1.1.2,9.1.1,demod,10,10,10,10,10,10,10,10] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((u^g(y)) v (((y^ (((((y v v)^ (w v y))^y)^v6) v ((((y^v) v (w^y)) v y)^ ((((y v v)^ (w v y))^y) v v6)))) v (v7^ (y v (((((y v v)^ (w v y))^y)^v6) v ((((y^v) v (w^y)) v y)^ ((((y v v)^ (w v y))^y) v v6))))))^ (u v g(y))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 16,15 [para_into,13.1.1.2.1,9.1.1] (((((x^y) v (y^ (x v y)))^y) v (y^ (((x^y) v (y^ (x v y))) v y)))^z) v (y^ (((((x^y) v (y^ (x v y)))^y) v (y^ (((x^y) v (y^ (x v y))) v y))) v z))=y. 20,19 [para_into,15.1.1.1.1,15.1.1,demod,16] (x^y) v (x^ (x v y))=x. 22,21 [para_from,15.1.1,11.1.1.2.1.2.2.2.1,demod,16,16,16,16,16,16,16,16] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (y^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 23 [para_into,19.1.1.2.2,19.1.1] ((x^y)^ (x^ (x v y))) v ((x^y)^x)=x^y. 25 [para_from,19.1.1,13.1.1.2.1.2.1.2.1] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((u^g(y)) v (y^ (u v g(y))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 33 [para_into,23.1.1.1.2.2,19.1.1] (((x^y)^ (x^ (x v y)))^ ((x^y)^x)) v (((x^y)^ (x^ (x v y)))^ (x^y))= (x^y)^ (x^ (x v y)). 38,37 [para_into,21.1.1.1.1,21.1.1,demod,22,22,20,flip.1] (x^g(y)) v (y^ (x v g(y)))=y. 41 [para_into,21.1.1.2.1,11.1.1,demod,12,12,20,flip.1] (x^g((y^z) v (z^ (y v z)))) v (z^ (x v g((y^z) v (z^ (y v z)))))= (y^z) v (z^ (y v z)). 43 [para_into,21.1.1.2.1,9.1.1,demod,10,10,20,flip.1] (x^g(y)) v (((y^ (((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v)))) v (w^ (y v (((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v))))))^ (x v g(y)))=y. 51 [back_demod,25,demod,38,38] (((x^y) v (y^ (x v y)))^z) v (y^ (((x^y) v (y^ (x v y))) v z))=y. 72,71 [para_into,41.1.1,51.1.1,flip.1] (x^y) v (y^ (x v y))=y. 73 [para_into,71.1.1.2.2,71.1.1] ((x^y)^ (y^ (x v y))) v ((y^ (x v y))^y)=y^ (x v y). 82,81 [para_into,71.1.1.2.2,19.1.1] ((x^y)^ (x^ (x v y))) v ((x^ (x v y))^x)=x^ (x v y). 85 [para_from,71.1.1,19.1.1.2.2] ((x^y)^ (y^ (x v y))) v ((x^y)^y)=x^y. 89 [para_into,85.1.1.1.2.2,71.1.1] (((x^y)^ (y^ (x v y)))^ ((y^ (x v y))^y)) v (((x^y)^ (y^ (x v y)))^ (y^ (x v y)))= (x^y)^ (y^ (x v y)). 101 [para_from,85.1.1,71.1.1.2.2] (((x^y)^ (y^ (x v y)))^ ((x^y)^y)) v (((x^y)^y)^ (x^y))= (x^y)^y. 107 [para_into,73.1.1.1.2.2,71.1.1,demod,72,72] (((x^y)^ (y^ (x v y)))^ ((y^ (x v y))^y)) v (((y^ (x v y))^y)^ (y^ (x v y)))= (y^ (x v y))^y. 115 [para_into,73.1.1.1.2.2,19.1.1,demod,20,20] (((x^y)^ (x^ (x v y)))^ ((x^ (x v y))^x)) v (((x^ (x v y))^x)^ (x^ (x v y)))= (x^ (x v y))^x. 133 [para_from,81.1.1,73.1.1.2.1.2,demod,82,82] ((((x^y)^ (x^ (x v y)))^ ((x^ (x v y))^x))^ (((x^ (x v y))^x)^ (x^ (x v y)))) v ((((x^ (x v y))^x)^ (x^ (x v y)))^ ((x^ (x v y))^x))= ((x^ (x v y))^x)^ (x^ (x v y)). 149 [para_into,43.1.1.2.1.1.2,71.1.1,demod,72] (x^g(y)) v (((y^ (((y^z) v (u^y)) v y)) v (v^ (y v (((y^z) v (u^y)) v y))))^ (x v g(y)))=y. 151 [para_into,43.1.1.2.1,71.1.1] (x^g(y)) v ((((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v)))^ (x v g(y)))=y. 155 [para_into,149.1.1.2.1,71.1.1] (x^g(y)) v ((((y^z) v (u^y)) v y)^ (x v g(y)))=y. 157 [para_into,149.1.1,19.1.1] (x^ (((x^y) v (z^x)) v x)) v (u^ (x v (((x^y) v (z^x)) v x)))=x. 160,159 [para_into,155.1.1,19.1.1] ((x^y) v (z^x)) v x=x. 162,161 [back_demod,157,demod,160,160] (x^x) v (y^ (x v x))=x. 165 [back_demod,151,demod,160] (x^g(y)) v ((((((y v z)^ (u v y))^y)^v) v (y^ ((((y v z)^ (u v y))^y) v v)))^ (x v g(y)))=y. 189 [para_from,159.1.1,19.1.1.2.2] (((x^y) v (z^x))^x) v (((x^y) v (z^x))^x)= (x^y) v (z^x). 205 [para_from,159.1.1,71.1.1.2.2] (((x^y) v (z^x))^x) v (x^x)=x. 208,207 [para_into,161.1.1,37.1.1,flip.1] g(x)=x. 212 [back_demod,165,demod,208,208] (x^y) v ((((((y v z)^ (u v y))^y)^v) v (y^ ((((y v z)^ (u v y))^y) v v)))^ (x v y))=y. 228 [para_from,161.1.1,19.1.1.2.2] ((x^x)^ (y^ (x v x))) v ((x^x)^x)=x^x. 230 [para_from,161.1.1,107.1.1.2.2.2,demod,162,162,162,162] ((((x^x)^ (y^ (x v x)))^ ((y^ (x v x))^x))^ (((y^ (x v x))^x)^ (y^ (x v x)))) v ((((y^ (x v x))^x)^ (y^ (x v x)))^ ((y^ (x v x))^x))= ((y^ (x v x))^x)^ (y^ (x v x)). 234 [para_from,161.1.1,73.1.1.2.1.2,demod,162,162] (((x^x)^ (y^ (x v x)))^ ((y^ (x v x))^x)) v (((y^ (x v x))^x)^ (y^ (x v x)))= (y^ (x v x))^x. 236 [para_from,161.1.1,85.1.1.1.2.2] (((x^x)^ (y^ (x v x)))^ ((y^ (x v x))^x)) v (((x^x)^ (y^ (x v x)))^ (y^ (x v x)))= (x^x)^ (y^ (x v x)). 242 [para_from,161.1.1,71.1.1.2.2] ((x^x)^ (y^ (x v x))) v ((y^ (x v x))^x)=y^ (x v x). 292 [para_into,212.1.1.2.1,161.1.1] (x^y) v ((((y v z)^ (u v y))^y)^ (x v y))=y. 397,396 [para_into,292.1.1,19.1.1] ((x v y)^ (z v x))^x=x. 442 [para_into,396.1.1.1.1,71.1.1] (x^ (y v (z^x)))^ (z^x)=z^x. 461,460 [para_into,396.1.1.1.2,159.1.1] ((x v y)^x)^x=x. 504 [para_from,396.1.1,242.1.1.2] ((x^x)^ ((x v y)^ (x v x))) v x= (x v y)^ (x v x). 512 [para_from,396.1.1,205.1.1.1.1.2] (((x^y) v x)^x) v (x^x)=x. 518 [para_from,396.1.1,159.1.1.1.2] ((x^y) v x) v x=x. 540 [para_from,396.1.1,89.1.1.2.1.1,demod,397,397] ((x^ (x^ (((x v y)^ (z v x)) v x)))^ ((x^ (((x v y)^ (z v x)) v x))^x)) v ((x^ (x^ (((x v y)^ (z v x)) v x)))^ (x^ (((x v y)^ (z v x)) v x)))=x^ (x^ (((x v y)^ (z v x)) v x)). 547,546 [para_from,396.1.1,71.1.1.1] x v (x^ (((x v y)^ (z v x)) v x))=x. 599,598 [para_into,460.1.1.1.1,71.1.1] (x^ (y^x))^ (y^x)=y^x. 605,604 [para_into,460.1.1.1.1,19.1.1] (x^ (x^y))^ (x^y)=x^y. 606 [back_demod,540,demod,605] ((x^ (x^ (((x v y)^ (z v x)) v x)))^ ((x^ (((x v y)^ (z v x)) v x))^x)) v (x^ (((x v y)^ (z v x)) v x))=x^ (x^ (((x v y)^ (z v x)) v x)). 624 [para_from,460.1.1,189.1.1.2.1.1,demod,461,461] ((x v (y^ ((x v z)^x)))^ ((x v z)^x)) v ((x v (y^ ((x v z)^x)))^ ((x v z)^x))=x v (y^ ((x v z)^x)). 647,646 [para_from,460.1.1,71.1.1.1] x v (x^ (((x v y)^x) v x))=x. 700 [para_into,518.1.1.1.1,396.1.1] (x v ((x v y)^ (z v x))) v ((x v y)^ (z v x))= (x v y)^ (z v x). 702 [para_from,518.1.1,460.1.1.1.1] (x^ ((x^y) v x))^ ((x^y) v x)= (x^y) v x. 779,778 [para_from,646.1.1,460.1.1.1.1] (x^x)^x=x. 781,780 [para_from,646.1.1,396.1.1.1.1] (x^ (y v x))^x=x. 782 [para_from,646.1.1,133.1.1.2.1.2.2,demod,647,647,779,647,779,647,647,779,647,779,647,779,647] ((((x^ (x^ (((x v y)^x) v x)))^ (x^x))^x)^ (x^ (x^x))) v ((x^ (x^x))^x)=x^ (x^x). 784 [para_from,646.1.1,115.1.1.2.2.2,demod,647,647,779,647,779,647,779] (((x^ (x^ (((x v y)^x) v x)))^ (x^x))^x) v (x^ (x^x))=x. 790 [para_from,646.1.1,33.1.1.2.1.2.2,demod,647,647] (((x^ (x^ (((x v y)^x) v x)))^ (x^x))^ ((x^ (x^ (((x v y)^x) v x)))^x)) v (((x^ (x^ (((x v y)^x) v x)))^ (x^x))^ (x^ (x^ (((x v y)^x) v x))))= (x^ (x^ (((x v y)^x) v x)))^ (x^x). 800 [para_from,646.1.1,85.1.1.1.2.2,demod,781,605] ((x^ (x^ (((x v y)^x) v x)))^x) v (x^ (((x v y)^x) v x))=x^ (x^ (((x v y)^x) v x)). 861,860 [back_demod,228,demod,779] ((x^x)^ (y^ (x v x))) v x=x^x. 884 [back_demod,606,demod,781] ((x^ (x^ (((x v y)^ (z v x)) v x)))^x) v (x^ (((x v y)^ (z v x)) v x))=x^ (x^ (((x v y)^ (z v x)) v x)). 904 [back_demod,504,demod,861,flip.1] (x v y)^ (x v x)=x^x. 966 [para_into,780.1.1.1.2,646.1.1,demod,781] x^ (x^ (((x v y)^x) v x))=x^ (((x v y)^x) v x). 969,968 [para_into,780.1.1.1.2,512.1.1,demod,779] x^ (x^x)=x^x. 972 [para_into,780.1.1.1.2,242.1.1] (((x^ (y v y))^y)^ (x^ (y v y)))^ ((x^ (y v y))^y)= (x^ (y v y))^y. 976 [para_into,780.1.1.1.2,161.1.1] ((x^ (y v y))^y)^ (x^ (y v y))=x^ (y v y). 990 [para_into,780.1.1.1.2,101.1.1] ((((x^y)^y)^ (x^y))^ ((x^y)^y))^ (((x^y)^y)^ (x^y))= ((x^y)^y)^ (x^y). 999,998 [para_into,780.1.1.1.2,85.1.1] (((x^y)^y)^ (x^y))^ ((x^y)^y)= (x^y)^y. 1007,1006 [para_into,780.1.1.1.2,71.1.1,demod,781] x^ (x^ (y v x))=x^ (y v x). 1021,1020 [back_demod,800,demod,1007,781,647,1007,flip.1] x^ (((x v y)^x) v x)=x. 1029,1028 [back_demod,790,demod,1021,1021,779,1021,1021,779,1021] (((x^x)^ (x^x))^x) v (x^x)= (x^x)^ (x^x). 1033,1032 [back_demod,784,demod,1021,969,1029] (x^x)^ (x^x)=x. 1035,1034 [back_demod,782,demod,1021,1033,969,1033,969,779,969] x v x=x^x. 1064 [back_demod,230,demod,1035,1035,1035,1035,1035,1035,1035,1035,1035] ((((x^x)^ (y^ (x^x)))^ ((y^ (x^x))^x))^ (((y^ (x^x))^x)^ (y^ (x^x)))) v ((((y^ (x^x))^x)^ (y^ (x^x)))^ ((y^ (x^x))^x))= ((y^ (x^x))^x)^ (y^ (x^x)). 1066 [back_demod,972,demod,1035,1035,1035,1035] (((x^ (y^y))^y)^ (x^ (y^y)))^ ((x^ (y^y))^y)= (x^ (y^y))^y. 1068 [back_demod,234,demod,1035,1035,1035,1035,1035] (((x^x)^ (y^ (x^x)))^ ((y^ (x^x))^x)) v (((y^ (x^x))^x)^ (y^ (x^x)))= (y^ (x^x))^x. 1078 [back_demod,990,demod,999] ((x^y)^y)^ (((x^y)^y)^ (x^y))= ((x^y)^y)^ (x^y). 1097,1096 [back_demod,966,demod,1021,1021] x^x=x. 1107 [back_demod,884,demod,1007,781,547,1007,flip.1] x^ (((x v y)^ (z v x)) v x)=x. 1124,1123 [back_demod,976,demod,1035,1097,1035,1097,1035,1097] ((x^y)^y)^ (x^y)=x^y. 1128,1127 [back_demod,904,demod,1035,1097,1097] (x v y)^x=x. 1135 [back_demod,624,demod,1128,1128,1128,1128,1128,1128,1035,1097,1128,flip.1] x v (y^x)=x. 1150,1149 [back_demod,236,demod,1097,1035,1097,1035,1097,1097,1035,1097,1035,1097,599,1097,1035,1097] ((x^ (y^x))^ ((y^x)^x)) v (y^x)=x^ (y^x). 1153 [back_demod,1064,demod,1097,1097,1097,1097,1097,1124,1097,1097,1124,1097,1097,1097,1124] (((x^ (y^x))^ ((y^x)^x))^ (y^x)) v ((y^x)^ ((y^x)^x))=y^x. 1162,1161 [back_demod,1068,demod,1097,1097,1097,1097,1097,1124,1150,1097,flip.1] (x^y)^y=y^ (x^y). 1164,1163 [back_demod,1066,demod,1097,1162,1097,1162,1097,1162,1162,1097,1162] (x^ (y^x))^ ((y^x)^ (x^ (y^x)))=x^ (y^x). 1166,1165 [back_demod,1034,demod,1097] x v x=x. 1179,1178 [back_demod,1078,demod,1162,1162,1162,1164,1162,1162,flip.1] (x^y)^ (y^ (x^y))=y^ (x^y). 1191,1190 [back_demod,1153,demod,1162,1097,1162,1179,1162,1179,1166] x^ (y^x)=y^x. 1203,1202 [back_demod,702,demod,1162,1191] x^ ((x^y) v x)= (x^y) v x. 1205,1204 [back_demod,604,demod,1162,1191] x^ (x^y)=x^y. 1238 [para_from,780.1.1,71.1.1.1,demod,1203] x v ((x^ (y v x)) v x)=x. 1248 [para_from,780.1.1,19.1.1.1] x v ((x^ (y v x))^ ((x^ (y v x)) v x))=x^ (y v x). 1262 [para_from,1127.1.1,23.1.1.2.1,demod,1128,1128] (x^ ((x v y)^ ((x v y) v x))) v (x^ (x v y))=x. 1266 [para_from,1127.1.1,19.1.1.1] x v ((x v y)^ ((x v y) v x))=x v y. 1309 [para_from,1204.1.1,23.1.1.2.1,demod,1205,1205] ((x^y)^ (x^ (x v (x^y)))) v ((x^y)^x)=x^y. 1352,1351 [para_into,1107.1.1.2.1.1,1238.1.1,demod,1203] (x^ (y v x)) v x=x. 1379 [back_demod,1248,demod,1352,781,1166,flip.1] x^ (y v x)=x. 1402,1401 [para_from,1379.1.1,1135.1.1.2] (x v y) v y=x v y. 1410,1409 [back_demod,700,demod,1402] x v ((x v y)^ (z v x))= (x v y)^ (z v x). 1412,1411 [back_demod,1266,demod,1410] (x v y)^ ((x v y) v x)=x v y. 1414,1413 [back_demod,1262,demod,1412,1166] x^ (x v y)=x. 1415 [back_demod,1309,demod,1414,1166] (x^y)^x=x^y. 1432 [para_from,1415.1.1,1135.1.1.2] x v (x^y)=x. 1651,1650 [para_into,442.1.1.1.2,1432.1.1] (x^y)^ (y^x)=y^x. 1686 [para_from,1650.1.1,1415.1.1.1,demod,1651,1651] x^y=y^x. 1687 [binary,1686.1,2.1] $Ans(comm_meet). ------------ end of proof ------------- ----> UNIT CONFLICT at 126.31 sec ----> 7949 [binary,7948.1,5.1] $Ans(comm_join). Length of proof is 104. Level of proof is 38. ---------------- PROOF ---------------- 5 [] A v B!=B v A|$Ans(comm_join). 10,9 [] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((y^ (((((y v u)^ (v v y))^y)^w) v ((((y^u) v (v^y)) v y)^ ((((y v u)^ (v v y))^y) v w)))) v (v6^ (y v (((((y v u)^ (v v y))^y)^w) v ((((y^u) v (v^y)) v y)^ ((((y v u)^ (v v y))^y) v w))))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 12,11 [para_into,9.1.1.2.1.2.1,9.1.1] (((x^ ((y^z) v (z^ (y v z)))) v (((y^z) v (z^ (y v z)))^ (x v ((y^z) v (z^ (y v z))))))^u) v (((x^g((y^z) v (z^ (y v z)))) v (z^ (x v g((y^z) v (z^ (y v z))))))^ (((x^ ((y^z) v (z^ (y v z)))) v (((y^z) v (z^ (y v z)))^ (x v ((y^z) v (z^ (y v z)))))) v u))= (y^z) v (z^ (y v z)). 13 [para_into,11.1.1.1.1.1.2,9.1.1,demod,10,10,10,10,10,10,10,10] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((u^g(y)) v (((y^ (((((y v v)^ (w v y))^y)^v6) v ((((y^v) v (w^y)) v y)^ ((((y v v)^ (w v y))^y) v v6)))) v (v7^ (y v (((((y v v)^ (w v y))^y)^v6) v ((((y^v) v (w^y)) v y)^ ((((y v v)^ (w v y))^y) v v6))))))^ (u v g(y))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 16,15 [para_into,13.1.1.2.1,9.1.1] (((((x^y) v (y^ (x v y)))^y) v (y^ (((x^y) v (y^ (x v y))) v y)))^z) v (y^ (((((x^y) v (y^ (x v y)))^y) v (y^ (((x^y) v (y^ (x v y))) v y))) v z))=y. 20,19 [para_into,15.1.1.1.1,15.1.1,demod,16] (x^y) v (x^ (x v y))=x. 22,21 [para_from,15.1.1,11.1.1.2.1.2.2.2.1,demod,16,16,16,16,16,16,16,16] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (y^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 23 [para_into,19.1.1.2.2,19.1.1] ((x^y)^ (x^ (x v y))) v ((x^y)^x)=x^y. 25 [para_from,19.1.1,13.1.1.2.1.2.1.2.1] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((u^g(y)) v (y^ (u v g(y))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 33 [para_into,23.1.1.1.2.2,19.1.1] (((x^y)^ (x^ (x v y)))^ ((x^y)^x)) v (((x^y)^ (x^ (x v y)))^ (x^y))= (x^y)^ (x^ (x v y)). 38,37 [para_into,21.1.1.1.1,21.1.1,demod,22,22,20,flip.1] (x^g(y)) v (y^ (x v g(y)))=y. 41 [para_into,21.1.1.2.1,11.1.1,demod,12,12,20,flip.1] (x^g((y^z) v (z^ (y v z)))) v (z^ (x v g((y^z) v (z^ (y v z)))))= (y^z) v (z^ (y v z)). 43 [para_into,21.1.1.2.1,9.1.1,demod,10,10,20,flip.1] (x^g(y)) v (((y^ (((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v)))) v (w^ (y v (((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v))))))^ (x v g(y)))=y. 51 [back_demod,25,demod,38,38] (((x^y) v (y^ (x v y)))^z) v (y^ (((x^y) v (y^ (x v y))) v z))=y. 72,71 [para_into,41.1.1,51.1.1,flip.1] (x^y) v (y^ (x v y))=y. 73 [para_into,71.1.1.2.2,71.1.1] ((x^y)^ (y^ (x v y))) v ((y^ (x v y))^y)=y^ (x v y). 82,81 [para_into,71.1.1.2.2,19.1.1] ((x^y)^ (x^ (x v y))) v ((x^ (x v y))^x)=x^ (x v y). 85 [para_from,71.1.1,19.1.1.2.2] ((x^y)^ (y^ (x v y))) v ((x^y)^y)=x^y. 89 [para_into,85.1.1.1.2.2,71.1.1] (((x^y)^ (y^ (x v y)))^ ((y^ (x v y))^y)) v (((x^y)^ (y^ (x v y)))^ (y^ (x v y)))= (x^y)^ (y^ (x v y)). 101 [para_from,85.1.1,71.1.1.2.2] (((x^y)^ (y^ (x v y)))^ ((x^y)^y)) v (((x^y)^y)^ (x^y))= (x^y)^y. 107 [para_into,73.1.1.1.2.2,71.1.1,demod,72,72] (((x^y)^ (y^ (x v y)))^ ((y^ (x v y))^y)) v (((y^ (x v y))^y)^ (y^ (x v y)))= (y^ (x v y))^y. 115 [para_into,73.1.1.1.2.2,19.1.1,demod,20,20] (((x^y)^ (x^ (x v y)))^ ((x^ (x v y))^x)) v (((x^ (x v y))^x)^ (x^ (x v y)))= (x^ (x v y))^x. 133 [para_from,81.1.1,73.1.1.2.1.2,demod,82,82] ((((x^y)^ (x^ (x v y)))^ ((x^ (x v y))^x))^ (((x^ (x v y))^x)^ (x^ (x v y)))) v ((((x^ (x v y))^x)^ (x^ (x v y)))^ ((x^ (x v y))^x))= ((x^ (x v y))^x)^ (x^ (x v y)). 149 [para_into,43.1.1.2.1.1.2,71.1.1,demod,72] (x^g(y)) v (((y^ (((y^z) v (u^y)) v y)) v (v^ (y v (((y^z) v (u^y)) v y))))^ (x v g(y)))=y. 151 [para_into,43.1.1.2.1,71.1.1] (x^g(y)) v ((((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v)))^ (x v g(y)))=y. 155 [para_into,149.1.1.2.1,71.1.1] (x^g(y)) v ((((y^z) v (u^y)) v y)^ (x v g(y)))=y. 157 [para_into,149.1.1,19.1.1] (x^ (((x^y) v (z^x)) v x)) v (u^ (x v (((x^y) v (z^x)) v x)))=x. 160,159 [para_into,155.1.1,19.1.1] ((x^y) v (z^x)) v x=x. 162,161 [back_demod,157,demod,160,160] (x^x) v (y^ (x v x))=x. 165 [back_demod,151,demod,160] (x^g(y)) v ((((((y v z)^ (u v y))^y)^v) v (y^ ((((y v z)^ (u v y))^y) v v)))^ (x v g(y)))=y. 189 [para_from,159.1.1,19.1.1.2.2] (((x^y) v (z^x))^x) v (((x^y) v (z^x))^x)= (x^y) v (z^x). 205 [para_from,159.1.1,71.1.1.2.2] (((x^y) v (z^x))^x) v (x^x)=x. 208,207 [para_into,161.1.1,37.1.1,flip.1] g(x)=x. 212 [back_demod,165,demod,208,208] (x^y) v ((((((y v z)^ (u v y))^y)^v) v (y^ ((((y v z)^ (u v y))^y) v v)))^ (x v y))=y. 228 [para_from,161.1.1,19.1.1.2.2] ((x^x)^ (y^ (x v x))) v ((x^x)^x)=x^x. 230 [para_from,161.1.1,107.1.1.2.2.2,demod,162,162,162,162] ((((x^x)^ (y^ (x v x)))^ ((y^ (x v x))^x))^ (((y^ (x v x))^x)^ (y^ (x v x)))) v ((((y^ (x v x))^x)^ (y^ (x v x)))^ ((y^ (x v x))^x))= ((y^ (x v x))^x)^ (y^ (x v x)). 234 [para_from,161.1.1,73.1.1.2.1.2,demod,162,162] (((x^x)^ (y^ (x v x)))^ ((y^ (x v x))^x)) v (((y^ (x v x))^x)^ (y^ (x v x)))= (y^ (x v x))^x. 236 [para_from,161.1.1,85.1.1.1.2.2] (((x^x)^ (y^ (x v x)))^ ((y^ (x v x))^x)) v (((x^x)^ (y^ (x v x)))^ (y^ (x v x)))= (x^x)^ (y^ (x v x)). 242 [para_from,161.1.1,71.1.1.2.2] ((x^x)^ (y^ (x v x))) v ((y^ (x v x))^x)=y^ (x v x). 292 [para_into,212.1.1.2.1,161.1.1] (x^y) v ((((y v z)^ (u v y))^y)^ (x v y))=y. 397,396 [para_into,292.1.1,19.1.1] ((x v y)^ (z v x))^x=x. 461,460 [para_into,396.1.1.1.2,159.1.1] ((x v y)^x)^x=x. 504 [para_from,396.1.1,242.1.1.2] ((x^x)^ ((x v y)^ (x v x))) v x= (x v y)^ (x v x). 512 [para_from,396.1.1,205.1.1.1.1.2] (((x^y) v x)^x) v (x^x)=x. 518 [para_from,396.1.1,159.1.1.1.2] ((x^y) v x) v x=x. 540 [para_from,396.1.1,89.1.1.2.1.1,demod,397,397] ((x^ (x^ (((x v y)^ (z v x)) v x)))^ ((x^ (((x v y)^ (z v x)) v x))^x)) v ((x^ (x^ (((x v y)^ (z v x)) v x)))^ (x^ (((x v y)^ (z v x)) v x)))=x^ (x^ (((x v y)^ (z v x)) v x)). 547,546 [para_from,396.1.1,71.1.1.1] x v (x^ (((x v y)^ (z v x)) v x))=x. 599,598 [para_into,460.1.1.1.1,71.1.1] (x^ (y^x))^ (y^x)=y^x. 605,604 [para_into,460.1.1.1.1,19.1.1] (x^ (x^y))^ (x^y)=x^y. 606 [back_demod,540,demod,605] ((x^ (x^ (((x v y)^ (z v x)) v x)))^ ((x^ (((x v y)^ (z v x)) v x))^x)) v (x^ (((x v y)^ (z v x)) v x))=x^ (x^ (((x v y)^ (z v x)) v x)). 624 [para_from,460.1.1,189.1.1.2.1.1,demod,461,461] ((x v (y^ ((x v z)^x)))^ ((x v z)^x)) v ((x v (y^ ((x v z)^x)))^ ((x v z)^x))=x v (y^ ((x v z)^x)). 647,646 [para_from,460.1.1,71.1.1.1] x v (x^ (((x v y)^x) v x))=x. 700 [para_into,518.1.1.1.1,396.1.1] (x v ((x v y)^ (z v x))) v ((x v y)^ (z v x))= (x v y)^ (z v x). 702 [para_from,518.1.1,460.1.1.1.1] (x^ ((x^y) v x))^ ((x^y) v x)= (x^y) v x. 779,778 [para_from,646.1.1,460.1.1.1.1] (x^x)^x=x. 781,780 [para_from,646.1.1,396.1.1.1.1] (x^ (y v x))^x=x. 782 [para_from,646.1.1,133.1.1.2.1.2.2,demod,647,647,779,647,779,647,647,779,647,779,647,779,647] ((((x^ (x^ (((x v y)^x) v x)))^ (x^x))^x)^ (x^ (x^x))) v ((x^ (x^x))^x)=x^ (x^x). 784 [para_from,646.1.1,115.1.1.2.2.2,demod,647,647,779,647,779,647,779] (((x^ (x^ (((x v y)^x) v x)))^ (x^x))^x) v (x^ (x^x))=x. 790 [para_from,646.1.1,33.1.1.2.1.2.2,demod,647,647] (((x^ (x^ (((x v y)^x) v x)))^ (x^x))^ ((x^ (x^ (((x v y)^x) v x)))^x)) v (((x^ (x^ (((x v y)^x) v x)))^ (x^x))^ (x^ (x^ (((x v y)^x) v x))))= (x^ (x^ (((x v y)^x) v x)))^ (x^x). 800 [para_from,646.1.1,85.1.1.1.2.2,demod,781,605] ((x^ (x^ (((x v y)^x) v x)))^x) v (x^ (((x v y)^x) v x))=x^ (x^ (((x v y)^x) v x)). 861,860 [back_demod,228,demod,779] ((x^x)^ (y^ (x v x))) v x=x^x. 884 [back_demod,606,demod,781] ((x^ (x^ (((x v y)^ (z v x)) v x)))^x) v (x^ (((x v y)^ (z v x)) v x))=x^ (x^ (((x v y)^ (z v x)) v x)). 904 [back_demod,504,demod,861,flip.1] (x v y)^ (x v x)=x^x. 966 [para_into,780.1.1.1.2,646.1.1,demod,781] x^ (x^ (((x v y)^x) v x))=x^ (((x v y)^x) v x). 969,968 [para_into,780.1.1.1.2,512.1.1,demod,779] x^ (x^x)=x^x. 972 [para_into,780.1.1.1.2,242.1.1] (((x^ (y v y))^y)^ (x^ (y v y)))^ ((x^ (y v y))^y)= (x^ (y v y))^y. 976 [para_into,780.1.1.1.2,161.1.1] ((x^ (y v y))^y)^ (x^ (y v y))=x^ (y v y). 990 [para_into,780.1.1.1.2,101.1.1] ((((x^y)^y)^ (x^y))^ ((x^y)^y))^ (((x^y)^y)^ (x^y))= ((x^y)^y)^ (x^y). 999,998 [para_into,780.1.1.1.2,85.1.1] (((x^y)^y)^ (x^y))^ ((x^y)^y)= (x^y)^y. 1007,1006 [para_into,780.1.1.1.2,71.1.1,demod,781] x^ (x^ (y v x))=x^ (y v x). 1021,1020 [back_demod,800,demod,1007,781,647,1007,flip.1] x^ (((x v y)^x) v x)=x. 1029,1028 [back_demod,790,demod,1021,1021,779,1021,1021,779,1021] (((x^x)^ (x^x))^x) v (x^x)= (x^x)^ (x^x). 1033,1032 [back_demod,784,demod,1021,969,1029] (x^x)^ (x^x)=x. 1035,1034 [back_demod,782,demod,1021,1033,969,1033,969,779,969] x v x=x^x. 1064 [back_demod,230,demod,1035,1035,1035,1035,1035,1035,1035,1035,1035] ((((x^x)^ (y^ (x^x)))^ ((y^ (x^x))^x))^ (((y^ (x^x))^x)^ (y^ (x^x)))) v ((((y^ (x^x))^x)^ (y^ (x^x)))^ ((y^ (x^x))^x))= ((y^ (x^x))^x)^ (y^ (x^x)). 1066 [back_demod,972,demod,1035,1035,1035,1035] (((x^ (y^y))^y)^ (x^ (y^y)))^ ((x^ (y^y))^y)= (x^ (y^y))^y. 1068 [back_demod,234,demod,1035,1035,1035,1035,1035] (((x^x)^ (y^ (x^x)))^ ((y^ (x^x))^x)) v (((y^ (x^x))^x)^ (y^ (x^x)))= (y^ (x^x))^x. 1078 [back_demod,990,demod,999] ((x^y)^y)^ (((x^y)^y)^ (x^y))= ((x^y)^y)^ (x^y). 1097,1096 [back_demod,966,demod,1021,1021] x^x=x. 1107 [back_demod,884,demod,1007,781,547,1007,flip.1] x^ (((x v y)^ (z v x)) v x)=x. 1124,1123 [back_demod,976,demod,1035,1097,1035,1097,1035,1097] ((x^y)^y)^ (x^y)=x^y. 1128,1127 [back_demod,904,demod,1035,1097,1097] (x v y)^x=x. 1135 [back_demod,624,demod,1128,1128,1128,1128,1128,1128,1035,1097,1128,flip.1] x v (y^x)=x. 1150,1149 [back_demod,236,demod,1097,1035,1097,1035,1097,1097,1035,1097,1035,1097,599,1097,1035,1097] ((x^ (y^x))^ ((y^x)^x)) v (y^x)=x^ (y^x). 1153 [back_demod,1064,demod,1097,1097,1097,1097,1097,1124,1097,1097,1124,1097,1097,1097,1124] (((x^ (y^x))^ ((y^x)^x))^ (y^x)) v ((y^x)^ ((y^x)^x))=y^x. 1162,1161 [back_demod,1068,demod,1097,1097,1097,1097,1097,1124,1150,1097,flip.1] (x^y)^y=y^ (x^y). 1164,1163 [back_demod,1066,demod,1097,1162,1097,1162,1097,1162,1162,1097,1162] (x^ (y^x))^ ((y^x)^ (x^ (y^x)))=x^ (y^x). 1166,1165 [back_demod,1034,demod,1097] x v x=x. 1179,1178 [back_demod,1078,demod,1162,1162,1162,1164,1162,1162,flip.1] (x^y)^ (y^ (x^y))=y^ (x^y). 1191,1190 [back_demod,1153,demod,1162,1097,1162,1179,1162,1179,1166] x^ (y^x)=y^x. 1203,1202 [back_demod,702,demod,1162,1191] x^ ((x^y) v x)= (x^y) v x. 1238 [para_from,780.1.1,71.1.1.1,demod,1203] x v ((x^ (y v x)) v x)=x. 1248 [para_from,780.1.1,19.1.1.1] x v ((x^ (y v x))^ ((x^ (y v x)) v x))=x^ (y v x). 1262 [para_from,1127.1.1,23.1.1.2.1,demod,1128,1128] (x^ ((x v y)^ ((x v y) v x))) v (x^ (x v y))=x. 1266 [para_from,1127.1.1,19.1.1.1] x v ((x v y)^ ((x v y) v x))=x v y. 1286 [para_from,1190.1.1,159.1.1.1.1] ((x^y) v (z^y)) v y=y. 1352,1351 [para_into,1107.1.1.2.1.1,1238.1.1,demod,1203] (x^ (y v x)) v x=x. 1379 [back_demod,1248,demod,1352,781,1166,flip.1] x^ (y v x)=x. 1402,1401 [para_from,1379.1.1,1135.1.1.2] (x v y) v y=x v y. 1403 [para_from,1379.1.1,1286.1.1.1.1] (x v (y^ (z v x))) v (z v x)=z v x. 1410,1409 [back_demod,700,demod,1402] x v ((x v y)^ (z v x))= (x v y)^ (z v x). 1412,1411 [back_demod,1266,demod,1410] (x v y)^ ((x v y) v x)=x v y. 1413 [back_demod,1262,demod,1412,1166] x^ (x v y)=x. 1423 [para_from,1413.1.1,1135.1.1.2] (x v y) v x=x v y. 7729,7728 [para_into,1403.1.1.1.2,1413.1.1] (x v y) v (y v x)=y v x. 7948 [para_from,7728.1.1,1423.1.1.1,demod,7729,7729] x v y=y v x. 7949 [binary,7948.1,5.1] $Ans(comm_join). ------------ end of proof -------------