Length of proof is 72. Level of proof is 35. This proof is strictly forward (i.e., a derivation of {L1,L2,L3,L4}) and is demodulation free except for simplifications with LT-77a itself. ---------------- PROOF ---------------- 2 [] cx v (cy^ (cx^cz))!=cx|cx^ (cy v (cx v cz))!=cx| ((cy^cx) v (cx^cz)) v cx!=cx| ((cy v cx)^ (cx v cz))^cx!=cx # label("McKenzie {L1,L2,L3,L4}"). 3 [] (((x^y) v (y^ (x v y)))^z) v (((x^ (((x1^y) v (y^x2)) v y)) v (((y^ (((x1 v (y v x2))^ (x3 v y))^y)) v (u^ (y v (((y v xnew)^ (x3 v y))^y))))^ (x v (((x1^y) v (y^x2)) v y))))^ (((x^y) v (y^ (x v y))) v z))=y # label("LT-77a"). 4 [] (((x^y) v (y^ (x v y)))^z) v (((x^ (((x1^y) v (y^x2)) v y)) v (((y^ (((x1 v (y v x2))^ (x3 v y))^y)) v (u^ (y v (((y v xnew)^ (x3 v y))^y))))^ (x v (((x1^y) v (y^x2)) v y))))^ (((x^y) v (y^ (x v y))) v z))=y # label("LT-77a"). 84 [para_into,3.1.1.2.1.2.1,3.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^ (((((y^z) v (z^ (y v z)))^ ((y^z) v (z^ (y v z)))) v (((y^z) v (z^ (y v z)))^v)) v ((y^z) v (z^ (y v z))))) v (z^ (x v (((((y^z) v (z^ (y v z)))^ ((y^z) v (z^ (y v z)))) v (((y^z) v (z^ (y v z)))^v)) v ((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)). 85 [para_into,84.1.1.1.1.1.2,3.1.1,demod,4,4,4,4,4,4,4,4,4,4,4,4,4,4] (((x^y) v (y^ (x v y)))^z) v (((x^ (((y^y) v (y^u)) v y)) v (((v^ (((w^y) v (y^v6)) v y)) v (((y^ (((w v (y v v6))^ (v7 v y))^y)) v (v8^ (y v (((y v v9)^ (v7 v y))^y))))^ (v v (((w^y) v (y^v6)) v y))))^ (x v (((y^y) v (y^u)) v y))))^ (((x^y) v (y^ (x v y))) v z))=y. 86 [para_into,85.1.1.2.1,3.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. 87 [para_into,86.1.1.1.1,86.1.1] (x^y) v (x^ (((((((z^x) v (x^ (z v x)))^x) v (x^ (((z^x) v (x^ (z v x))) v x)))^x) v (x^ (((((z^x) v (x^ (z v x)))^x) v (x^ (((z^x) v (x^ (z v x))) v x))) v x))) v y))=x. 88 [para_into,87.1.1.2.2.1,86.1.1] (x^y) v (x^ (x v y))=x. 90 [para_from,88.1.1,85.1.1.2.1.2.1.2.1] (((x^y) v (y^ (x v y)))^z) v (((x^ (((y^y) v (y^u)) v y)) v (((v^ (((y^y) v (y^w)) v y)) v (y^ (v v (((y^y) v (y^w)) v y))))^ (x v (((y^y) v (y^u)) v y))))^ (((x^y) v (y^ (x v y))) v z))=y. 91 [para_from,88.1.1,3.1.1.2.1.2.1] (((x^y) v (y^ (x v y)))^z) v (((x^ (((y^y) v (y^u)) v y)) v (y^ (x v (((y^y) v (y^u)) v y))))^ (((x^y) v (y^ (x v y))) v z))=y. 92 [para_into,91.1.1.1.1,91.1.1] (x^y) v (((((z^x) v (x^ (z v x)))^ (((((z^ (((x^x) v (x^u)) v x)) v (x^ (z v (((x^x) v (x^u)) v x))))^ ((z^ (((x^x) v (x^u)) v x)) v (x^ (z v (((x^x) v (x^u)) v x))))) v (((z^ (((x^x) v (x^u)) v x)) v (x^ (z v (((x^x) v (x^u)) v x))))^v)) v ((z^ (((x^x) v (x^u)) v x)) v (x^ (z v (((x^x) v (x^u)) v x)))))) v (((z^ (((x^x) v (x^u)) v x)) v (x^ (z v (((x^x) v (x^u)) v x))))^ (((z^x) v (x^ (z v x))) v (((((z^ (((x^x) v (x^u)) v x)) v (x^ (z v (((x^x) v (x^u)) v x))))^ ((z^ (((x^x) v (x^u)) v x)) v (x^ (z v (((x^x) v (x^u)) v x))))) v (((z^ (((x^x) v (x^u)) v x)) v (x^ (z v (((x^x) v (x^u)) v x))))^v)) v ((z^ (((x^x) v (x^u)) v x)) v (x^ (z v (((x^x) v (x^u)) v x))))))))^ (((((z^x) v (x^ (z v x)))^ ((z^ (((x^x) v (x^u)) v x)) v (x^ (z v (((x^x) v (x^u)) v x))))) v (((z^ (((x^x) v (x^u)) v x)) v (x^ (z v (((x^x) v (x^u)) v x))))^ (((z^x) v (x^ (z v x))) v ((z^ (((x^x) v (x^u)) v x)) v (x^ (z v (((x^x) v (x^u)) v x))))))) v y))= (z^ (((x^x) v (x^u)) v x)) v (x^ (z v (((x^x) v (x^u)) v x))). 94 [para_into,92.1.1.2.1,91.1.1] (x^y) v (x^ (((((z^x) v (x^ (z v x)))^ ((z^ (((x^x) v (x^u)) v x)) v (x^ (z v (((x^x) v (x^u)) v x))))) v (((z^ (((x^x) v (x^u)) v x)) v (x^ (z v (((x^x) v (x^u)) v x))))^ (((z^x) v (x^ (z v x))) v ((z^ (((x^x) v (x^u)) v x)) v (x^ (z v (((x^x) v (x^u)) v x))))))) v y))= (z^ (((x^x) v (x^u)) v x)) v (x^ (z v (((x^x) v (x^u)) v x))). 95 [para_into,94.1.1.2.2.1,91.1.1,flip.1] (x^ (((y^y) v (y^z)) v y)) v (y^ (x v (((y^y) v (y^z)) v y)))= (y^u) v (y^ (y v u)). 99 [para_into,95.1.2,88.1.1] (x^ (((y^y) v (y^z)) v y)) v (y^ (x v (((y^y) v (y^z)) v y)))=y. 101 [para_into,99.1.1.1.2.1,88.1.1] (x^ (y v y)) v (y^ (x v (((y^y) v (y^ (y v y))) v y)))=y. 103 [para_into,99.1.1,3.1.1,flip.1] (x^ (((y^z) v (z^u)) v z)) v (((z^ (((y v (z v u))^ (v v z))^z)) v (w^ (z v (((z v v6)^ (v v z))^z))))^ (x v (((y^z) v (z^u)) v z)))=z. 105 [para_into,101.1.1.2.2.2.1,88.1.1] (x^ (y v y)) v (y^ (x v (y v y)))=y. 108 [para_into,103.1.1,88.1.1] (x^ (((y v (x v z))^ (u v x))^x)) v (v^ (x v (((x v w)^ (u v x))^x)))=x. 109 [para_into,108.1.1,90.1.1,flip.1] (x^y) v (y^ (x v y))=y. 116 [para_into,109.1.1,108.1.1,flip.1] ((x v (x v y))^ (z v x))^x=x. 126 [para_from,116.1.1,108.1.1.1.2] (x^x) v (y^ (x v (((x v z)^ (u v x))^x)))=x. 134 [para_into,126.1.1.2.2.2,116.1.1] (x^x) v (y^ (x v x))=x. 136 [para_from,126.1.1,88.1.1.2.2] ((x^x)^ (y^ (x v (((x v z)^ (u v x))^x)))) v ((x^x)^x)=x^x. 138 [para_into,134.1.1,103.1.1,flip.1] ((x^y) v (y^z)) v y=y # label("L3"). 139 [para_into,134.1.1,105.1.1,flip.1] x v x=x. 144 [para_from,139.1.1,134.1.1.2.2] (x^x) v (y^x)=x. 147 [para_from,139.1.1,108.1.1.2.2.2.1.2] (x^ (((y v (x v z))^ (x v x))^x)) v (u^ (x v (((x v v)^x)^x)))=x. 162 [para_from,139.1.1,116.1.1.1.1.2] ((x v x)^ (y v x))^x=x. 164 [para_into,144.1.1,139.1.1] x^x=x. 178 [para_from,164.1.1,144.1.1.1] x v (y^x)=x. 179 [para_from,164.1.1,134.1.1.1] x v (y^ (x v x))=x. 192 [para_from,178.1.1,109.1.1.2.2] (x^ (y^x)) v ((y^x)^x)=y^x. 197 [para_into,138.1.1.1.1,164.1.1] (x v (x^y)) v x=x. 200 [para_into,138.1.1.1,179.1.1] (x^y) v y=y. 225 [para_from,197.1.1,88.1.1.2.2] ((x v (x^y))^x) v ((x v (x^y))^x)=x v (x^y). 228 [para_into,162.1.1.1.1,139.1.1] (x^ (y v x))^x=x. 245 [para_into,228.1.1.1.2,109.1.1] ((x^ (y v x))^x)^ (x^ (y v x))=x^ (y v x). 251 [para_from,228.1.1,109.1.1.1] x v (x^ ((x^ (y v x)) v x))=x. 259 [para_from,251.1.1,88.1.1.2.2] (x^ (x^ ((x^ (y v x)) v x))) v (x^x)=x. 320 [para_into,245.1.1.1,228.1.1] x^ (x^ (y v x))=x^ (y v x). 390 [para_from,320.1.1,259.1.1.1] (x^ ((x^ (y v x)) v x)) v (x^x)=x. 424 [para_into,390.1.1.2,164.1.1] (x^ ((x^ (y v x)) v x)) v x=x. 474 [para_into,225.1.1,139.1.1] (x v (x^y))^x=x v (x^y). 564 [para_into,136.1.1.1.1,164.1.1] (x^ (y^ (x v (((x v z)^ (u v x))^x)))) v ((x^x)^x)=x^x. 592 [para_into,564.1.1.1.2.2,178.1.1] (x^ (y^x)) v ((x^x)^x)=x^x. 621 [para_into,592.1.1.2.1,164.1.1] (x^ (y^x)) v (x^x)=x^x. 671 [para_into,621.1.1.2,164.1.1] (x^ (y^x)) v x=x^x. 726 [para_into,671.1.2,164.1.1] (x^ (y^x)) v x=x. 806 [para_into,147.1.1.1.2.1.2,139.1.1] (x^ (((y v (x v z))^x)^x)) v (u^ (x v (((x v v)^x)^x)))=x. 819 [para_into,806.1.1.2.2,178.1.1] (x^ (((y v (x v z))^x)^x)) v (u^x)=x. 843 [para_into,819.1.1,192.1.1] ((x v (y v z))^y)^y=y. 864 [para_from,843.1.1,192.1.1.2] (x^ ((y v (x v z))^x)) v x= (y v (x v z))^x. 895 [para_into,864.1.1,726.1.1,flip.1] (x v (y v z))^y=y. 960 [para_into,895.1.1.1.2,200.1.1] (x v y)^ (z^y)=z^y. 969 [para_into,895.1.1.1,726.1.1] (x v y)^x=x. 1009 [para_into,969.1.1,474.1.1] x v (x^y)=x. 1025 [para_from,969.1.1,88.1.1.1] x v ((x v y)^ ((x v y) v x))=x v y. 1269 [para_into,1009.1.1.2,960.1.1] (x v y) v (z^y)=x v y. 1270 [para_into,1009.1.1.2,969.1.1] (x v y) v x=x v y. 1271 [para_into,1009.1.1.2,895.1.1] (x v (y v z)) v y=x v (y v z). 1277 [para_into,1009.1.1.2,228.1.1] (x^ (y v x)) v x=x^ (y v x). 1360 [para_from,1270.1.1,1025.1.1.2.2] x v ((x v y)^ (x v y))=x v y. 1457 [para_into,1269.1.1.1,1009.1.1] x v (y^ (x^z))=x v (x^z). 1796 [para_into,1277.1.1,424.1.1,flip.1] x^ ((x^ (y v x)) v x)=x. 1894 [para_into,1796.1.1.2.1.2,1009.1.1] (x^y)^ (((x^y)^x) v (x^y))=x^y. 1990 [para_into,1360.1.1.2,164.1.1] x v (x v y)=x v y. 2134 [para_from,1990.1.1,116.1.1.1.1] ((x v y)^ (z v x))^x=x. 2259 [para_into,1457.1.2,1009.1.1] x v (y^ (x^z))=x # label("L1"). 2379 [para_into,1894.1.1.2.1,228.1.1] (x^ (y v x))^ (x v (x^ (y v x)))=x^ (y v x). 2546 [para_into,2379.1.1.2,1009.1.1] (x^ (y v x))^x=x^ (y v x). 2678 [para_into,2546.1.1,228.1.1,flip.1] x^ (y v x)=x. 2778 [para_into,2678.1.1.2,1271.1.1] x^ (y v (x v z))=x # label("L2"). 2817 [para_from,2678.1.1,109.1.1.1] x v ((y v x)^ (x v (y v x)))=y v x. 3413 [para_into,2134.1.1.1.2,1270.1.1] ((x v y)^ (x v z))^x=x. 3446 [para_into,3413.1.1.1.1,2817.1.1] ((x v y)^ (y v z))^y=y # label("L4"). 3492 [hyper,3446,2,2259,2778,138] $F. ------------ end of proof / derivation -------------