Length of proof is 60. Level of proof is 36. This proof is strictly forward (i.e., a derivation of {L1,L2,L3,L4}) and is demodulation free except for simplifications with LT-77 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. 3 [] (((xa^y) v (y^ (xb v y)))^xc) v (((xd^ (((xe^y) v (y^xf)) v y)) v (((y^ (((xg v (y v xh))^ (xi v y))^y)) v (xj^ (y v (((y v x)^ (xm v y))^y))))^ (xn v (((xo^y) v (y^xp)) v y))))^ (((xq^y) v (y^ (xr v y))) v xs))=y # label("LT-77"). 4 [] (((xa^y) v (y^ (xb v y)))^xc) v (((xd^ (((xe^y) v (y^xf)) v y)) v (((y^ (((xg v (y v xh))^ (xi v y))^y)) v (xj^ (y v (((y v x)^ (xm v y))^y))))^ (xn v (((xo^y) v (y^xp)) v y))))^ (((xq^y) v (y^ (xr v y))) v xs))=y # label("LT-77"). 81 [para_into,3.1.1.2.1.2.1,3.1.1] (((x^ ((y^z) v (z^ (u v z)))) v (((y^z) v (z^ (u v z)))^ (v v ((y^z) v (z^ (u v z))))))^w) v (((v6^ (((v7^ ((y^z) v (z^ (u v z)))) v (((y^z) v (z^ (u v z)))^v8)) v ((y^z) v (z^ (u v z))))) v (z^ (v9 v (((v10^ ((y^z) v (z^ (u v z)))) v (((y^z) v (z^ (u v z)))^v11)) v ((y^z) v (z^ (u v z)))))))^ (((v12^ ((y^z) v (z^ (u v z)))) v (((y^z) v (z^ (u v z)))^ (v13 v ((y^z) v (z^ (u v z)))))) v v14))= (y^z) v (z^ (u v z)). 90 [para_into,81.1.1.1.1.1.2,3.1.1,demod,4,4,4,4,4,4,4,4,4,4,4,4] (((x^y) v (y^ (z v y)))^u) v (((v^ (((w^y) v (y^v6)) v y)) v (((v7^ (((v8^y) v (y^v9)) v y)) v (((y^ (((v10 v (y v v11))^ (v12 v y))^y)) v (v13^ (y v (((y v v14)^ (v15 v y))^y))))^ (v16 v (((v17^y) v (y^v18)) v y))))^ (v19 v (((v20^y) v (y^v21)) v y))))^ (((v22^y) v (y^ (v23 v y))) v v24))=y. 202 [para_into,90.1.1.2.1,3.1.1] (((x^y) v (y^ (z v y)))^u) v (y^ (((v^y) v (y^ (w v y))) v v6))=y. 251 [para_into,202.1.1.1.1,202.1.1] (x^y) v (x^ (((z^x) v (x^ (u v x))) v v))=x. 261 [para_into,202.1.1.2.2.1,202.1.1] (((x^y) v (y^ (z v y)))^u) v (y^ (y v v))=y. 313 [para_from,202.1.1,3.1.1.2.1] (((x^y) v (y^ (z v y)))^u) v (((y^ (((v v (y v w))^ (v6 v y))^y)) v (v7^ (y v (((y v v8)^ (v9 v y))^y))))^ (((v10^y) v (y^ (v11 v y))) v v12))=y. 321 [para_into,251.1.1.2.2.1,251.1.1] (x^y) v (x^ (x v z))=x. 356 [para_into,321.1.1.2.2,321.1.1] ((x^y)^z) v ((x^y)^x)=x^y. 396 [para_from,321.1.1,3.1.1.2.1.2.1] (((x^y) v (y^ (z v y)))^u) v (((v^ (((w^y) v (y^v6)) v y)) v (y^ (v7 v (((v8^y) v (y^v9)) v y))))^ (((v10^y) v (y^ (v11 v y))) v v12))=y. 575 [para_into,396.1.1.1.1,261.1.1] (x^y) v (((z^ (((u^x) v (x^v)) v x)) v (x^ (w v (((v6^x) v (x^v7)) v x))))^ (((v8^x) v (x^ (v9 v x))) v v10))=x. 707 [para_into,575.1.1.2.2.1,261.1.1] (x^y) v (((z^ (((u^x) v (x^v)) v x)) v (x^ (w v (((v6^x) v (x^v7)) v x))))^ (x v v8))=x. 743 [para_into,707.1.1.2.1.1.2.1,261.1.1] (x^y) v (((z^ (x v x)) v (x^ (u v (((v^x) v (x^w)) v x))))^ (x v v6))=x. 752 [para_into,707.1.1.2.1.2.2.2.1,261.1.1] (x^y) v (((z^ (((u^x) v (x^v)) v x)) v (x^ (w v (x v x))))^ (x v v6))=x. 816 [para_into,743.1.1.2.1.2.2.2.1,261.1.1] (x^y) v (((z^ (x v x)) v (x^ (u v (x v x))))^ (x v v))=x. 895 [para_into,816.1.1.2.1.1.2,356.1.1] (((x^y)^x)^z) v (((u^ (x^y)) v (((x^y)^x)^ (v v (((x^y)^x) v ((x^y)^x)))))^ (((x^y)^x) v w))= (x^y)^x. 1087 [para_into,895.1.1.2.1.2.2.2,356.1.1] (((x^y)^x)^z) v (((u^ (x^y)) v (((x^y)^x)^ (v v (x^y))))^ (((x^y)^x) v w))= (x^y)^x. 1374 [para_from,1087.1.1,3.1.1.2.1] (((x^y) v (y^ (z v y)))^u) v (((((y v (y v v))^ (w v y))^y)^ ((y v (y v v))^ (w v y)))^ (((v6^y) v (y^ (v7 v y))) v v8))=y. 1479 [para_into,1374.1.1.1.1,261.1.1] (x^y) v (((((x v (x v z))^ (u v x))^x)^ ((x v (x v z))^ (u v x)))^ (((v^x) v (x^ (w v x))) v v6))=x. 1756 [para_into,1479.1.1.2.2.1,261.1.1] (x^y) v (((((x v (x v z))^ (u v x))^x)^ ((x v (x v z))^ (u v x)))^ (x v v))=x. 2034 [para_into,313.1.1.2.2.1,261.1.1] (((x^y) v (y^ (z v y)))^u) v (((y^ (((v v (y v w))^ (v6 v y))^y)) v (v7^ (y v (((y v v8)^ (v9 v y))^y))))^ (y v v10))=y. 2160 [para_into,2034.1.1.1.1,261.1.1] (x^y) v (((x^ (((z v (x v u))^ (v v x))^x)) v (w^ (x v (((x v v6)^ (v7 v x))^x))))^ (x v v8))=x. 2329 [para_into,2160.1.1.2.1,313.1.1] (((x^y) v (y^ (z v y)))^u) v (y^ (((x^y) v (y^ (z v y))) v v))= (x^y) v (y^ (z v y)). 2474 [para_into,2329.1.1,202.1.1,flip.1] (x^y) v (y^ (z v y))=y. 2740 [para_into,2474.1.1,2160.1.1,flip.1] (x^ (((y v (x v z))^ (u v x))^x)) v (v^ (x v (((x v w)^ (v6 v x))^x)))=x. 2741 [para_into,2474.1.1,1756.1.1,flip.1] (((x v (x v y))^ (z v x))^x)^ ((x v (x v y))^ (z v x))=x. 2743 [para_into,2474.1.1,752.1.1,flip.1] (x^ (((y^z) v (z^u)) v z)) v (z^ (v v (z v z)))=z. 3074 [para_from,2741.1.1,356.1.1.2] ((((x v (x v y))^ (z v x))^x)^u) v x= ((x v (x v y))^ (z v x))^x. 3197 [para_into,3074.1.1.1,2741.1.1,flip.1] ((x v (x v y))^ (z v x))^x=x v x. 3824 [para_into,2740.1.1,2474.1.1] ((x v (x v y))^ (z v x))^x=x. 3973 [para_into,3824.1.1,3197.1.1] x v x=x. 3976 [para_from,3824.1.1,2740.1.1.2.2.2] (x^ (((y v (x v z))^ (u v x))^x)) v (v^ (x v x))=x. 3978 [para_from,3824.1.1,2740.1.1.1.2] (x^x) v (y^ (x v (((x v z)^ (u v x))^x)))=x. 4098 [para_into,3973.1.1,356.1.1,flip.1] (x^y)^x=x^y. 4099 [para_into,3973.1.1,321.1.1,flip.1] x^ (x v y)=x. 4203 [para_from,3973.1.1,2474.1.1.2.2] (x^y) v (y^y)=y. 4244 [para_into,4099.1.1.2,3973.1.1] x^x=x. 4264 [para_from,4099.1.1,2743.1.1.1] ((x^y) v (y^z)) v (y^ (u v (y v y)))=y. 4342 [para_from,4099.1.1,2474.1.1.2] (x^y) v y=y. 4462 [para_into,4342.1.1.1,4099.1.1] x v (x v y)=x v y. 5120 [para_from,4462.1.1,3824.1.1.1.1] ((x v y)^ (z v x))^x=x. 5367 [para_into,4264.1.1.2,4099.1.1] ((x^y) v (y^z)) v y=y # label("L3"). 5506 [para_into,3978.1.1.1,4244.1.1] x v (y^ (x v (((x v z)^ (u v x))^x)))=x. 5748 [para_into,3976.1.1.2.2,3973.1.1] (x^ (((y v (x v z))^ (u v x))^x)) v (v^x)=x. 5886 [para_into,5748.1.1,4342.1.1] ((x v (y v z))^ (u v y))^y=y. 5963 [para_into,5120.1.1.1.1,4203.1.1] (x^ (y v (z^x)))^ (z^x)=z^x. 6002 [para_from,5120.1.1,5506.1.1.2.2.2] x v (y^ (x v x))=x. 6061 [para_into,6002.1.1.2.2,3973.1.1] x v (y^x)=x. 6105 [para_into,6061.1.1.2,4098.1.1] x v (x^y)=x. 6540 [para_from,6105.1.1,5963.1.1.1.2] (x^y)^ (y^x)=y^x. 6637 [para_into,6540.1.1,4098.1.2] ((x^y)^ (y^x))^ (x^y)=y^x. 7006 [para_into,6637.1.1.1,6540.1.1] (x^y)^ (y^x)=x^y. 7433 [para_into,7006.1.1,6540.1.1] x^y=y^x. 7757 [para_from,7433.1.1,5120.1.1.1] ((x v y)^ (y v z))^y=y # label("L4"). 9700 [para_into,5886.1.1.1,4099.1.1] (x v (y v z))^y=y. 9791 [para_into,9700.1.1,7433.1.2] x^ (y v (x v z))=x # label("L2"). 9883 [para_into,9791.1.1.2.2,4203.1.1] (x^y)^ (z v y)=x^y. 10076 [para_from,9883.1.1,6061.1.1.2] (x v y) v (z^y)=x v y. 10743 [para_from,10076.1.2,6002.1.1.2.2] x v (y^ ((x v x) v (z^x)))=x. 10938 [para_into,10743.1.1.2,9883.1.1] x v (y^ (z^x))=x. 11037 [para_into,10938.1.1.2.2,7433.1.2] x v (y^ (x^z))=x # label("L1"). 11139 [hyper,11037,2,9791,5367,7757] $F. ------------ end of proof / derivation -------------