%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : COM133+1 : TPTP v8.1.0. Released v6.4.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n003.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Fri Jul 15 01:46:14 EDT 2022 % Result : Theorem 22.06s 22.23s % Output : Proof 22.06s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : COM133+1 : TPTP v8.1.0. Released v6.4.0. % 0.11/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n003.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Thu Jun 16 19:10:56 EDT 2022 % 0.19/0.33 % CPUTime : % 22.06/22.23 % SZS status Theorem % 22.06/22.23 (* PROOF-FOUND *) % 22.06/22.23 (* BEGIN-PROOF *) % 22.06/22.23 % SZS output start Proof % 22.06/22.23 1. (T_0 = T_1) (T_0 != T_1) ### Axiom % 22.06/22.23 2. (vtcheck T_2 T_3 T_4) (-. (vtcheck T_2 T_3 T_4)) ### Axiom % 22.06/22.23 3. (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) T_6) (-. (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) T_6)) ### Axiom % 22.06/22.23 4. (-. (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) T_6)) (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) T_6) ### Axiom % 22.06/22.23 5. (((T_0 = T_1) /\ ((vtcheck T_2 T_3 T_4) /\ (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) T_6))) => (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) T_6)) (-. (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) T_6)) (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) T_6) (vtcheck T_2 T_3 T_4) (T_0 = T_1) ### DisjTree 1 2 3 4 % 22.06/22.23 6. (All VT2, (((T_0 = T_1) /\ ((vtcheck T_2 T_3 T_4) /\ (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) VT2))) => (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) VT2))) (T_0 = T_1) (vtcheck T_2 T_3 T_4) (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) T_6) (-. (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) T_6)) ### All 5 % 22.06/22.23 7. (All Ve1, (All VT2, (((T_0 = T_1) /\ ((vtcheck T_2 T_3 T_4) /\ (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 Ve1) VT2))) => (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 Ve1)) VT2)))) (-. (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) T_6)) (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) T_6) (vtcheck T_2 T_3 T_4) (T_0 = T_1) ### All 6 % 22.06/22.23 8. (All VS, (All Ve1, (All VT2, (((T_0 = T_1) /\ ((vtcheck T_2 T_3 T_4) /\ (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 VS Ve1) VT2))) => (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 VS Ve1)) VT2))))) (T_0 = T_1) (vtcheck T_2 T_3 T_4) (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) T_6) (-. (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) T_6)) ### All 7 % 22.06/22.23 9. (All Vy, (All VS, (All Ve1, (All VT2, (((T_0 = Vy) /\ ((vtcheck T_2 T_3 T_4) /\ (vtcheck (vbind T_0 T_4 T_2) (vabs Vy VS Ve1) VT2))) => (vtcheck T_2 (vsubst T_0 T_3 (vabs Vy VS Ve1)) VT2)))))) (-. (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) T_6)) (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) T_6) (vtcheck T_2 T_3 T_4) (T_0 = T_1) ### All 8 % 22.06/22.23 10. (All Ve, (All Vy, (All VS, (All Ve1, (All VT2, (((T_0 = Vy) /\ ((vtcheck T_2 Ve T_4) /\ (vtcheck (vbind T_0 T_4 T_2) (vabs Vy VS Ve1) VT2))) => (vtcheck T_2 (vsubst T_0 Ve (vabs Vy VS Ve1)) VT2))))))) (T_0 = T_1) (vtcheck T_2 T_3 T_4) (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) T_6) (-. (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) T_6)) ### All 9 % 22.06/22.23 11. (All Vx, (All Ve, (All Vy, (All VS, (All Ve1, (All VT2, (((Vx = Vy) /\ ((vtcheck T_2 Ve T_4) /\ (vtcheck (vbind Vx T_4 T_2) (vabs Vy VS Ve1) VT2))) => (vtcheck T_2 (vsubst Vx Ve (vabs Vy VS Ve1)) VT2)))))))) (-. (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) T_6)) (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) T_6) (vtcheck T_2 T_3 T_4) (T_0 = T_1) ### All 10 % 22.06/22.23 12. (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All Ve1, (All VT2, (((Vx = Vy) /\ ((vtcheck VC Ve T_4) /\ (vtcheck (vbind Vx T_4 VC) (vabs Vy VS Ve1) VT2))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS Ve1)) VT2))))))))) (T_0 = T_1) (vtcheck T_2 T_3 T_4) (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) T_6) (-. (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) T_6)) ### All 11 % 22.06/22.23 13. (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All Ve1, (All VT2, (((Vx = Vy) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS Ve1) VT2))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS Ve1)) VT2)))))))))) (-. (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) T_6)) (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) T_6) (vtcheck T_2 T_3 T_4) (T_0 = T_1) ### All 12 % 22.06/22.23 14. (visFreeVar T_1 T_3) (-. (visFreeVar T_1 T_3)) ### Axiom % 22.06/22.23 15. (vtcheck T_2 T_3 T_4) (-. (vtcheck T_2 T_3 T_4)) ### Axiom % 22.06/22.23 16. (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) T_6) (-. (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) T_6)) ### Axiom % 22.06/22.23 17. (-. (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) T_6)) (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) T_6) ### Axiom % 22.06/22.23 18. (((T_0 != T_1) /\ ((visFreeVar T_1 T_3) /\ ((vtcheck T_2 T_3 T_4) /\ (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) T_6)))) => (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) T_6)) (visFreeVar T_1 T_3) (vtcheck T_2 T_3 T_4) (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) T_6) (-. (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) T_6)) (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All Ve1, (All VT2, (((Vx = Vy) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS Ve1) VT2))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS Ve1)) VT2)))))))))) ### DisjTree 13 14 15 16 17 % 22.06/22.23 19. (All VT2, (((T_0 != T_1) /\ ((visFreeVar T_1 T_3) /\ ((vtcheck T_2 T_3 T_4) /\ (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) VT2)))) => (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) VT2))) (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All Ve1, (All VT2, (((Vx = Vy) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS Ve1) VT2))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS Ve1)) VT2)))))))))) (-. (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) T_6)) (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) T_6) (vtcheck T_2 T_3 T_4) (visFreeVar T_1 T_3) ### All 18 % 22.06/22.23 20. (vtcheck T_2 T_3 T_4) (-. (vtcheck T_2 T_3 T_4)) ### Axiom % 22.06/22.23 21. (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) T_6) (-. (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) T_6)) ### Axiom % 22.06/22.23 22. (-. (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) T_6)) (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) T_6) ### Axiom % 22.06/22.23 23. (((T_0 != T_1) /\ ((-. (visFreeVar T_1 T_3)) /\ ((vtcheck T_2 T_3 T_4) /\ (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) T_6)))) => (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) T_6)) (All VT2, (((T_0 != T_1) /\ ((visFreeVar T_1 T_3) /\ ((vtcheck T_2 T_3 T_4) /\ (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) VT2)))) => (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) VT2))) (vtcheck T_2 T_3 T_4) (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) T_6) (-. (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) T_6)) (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All Ve1, (All VT2, (((Vx = Vy) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS Ve1) VT2))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS Ve1)) VT2)))))))))) ### DisjTree 13 19 20 21 22 % 22.06/22.23 24. (All VT2, (((T_0 != T_1) /\ ((-. (visFreeVar T_1 T_3)) /\ ((vtcheck T_2 T_3 T_4) /\ (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) VT2)))) => (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) VT2))) (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All Ve1, (All VT2, (((Vx = Vy) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS Ve1) VT2))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS Ve1)) VT2)))))))))) (-. (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) T_6)) (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) T_6) (vtcheck T_2 T_3 T_4) (All VT2, (((T_0 != T_1) /\ ((visFreeVar T_1 T_3) /\ ((vtcheck T_2 T_3 T_4) /\ (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) VT2)))) => (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) VT2))) ### All 23 % 22.06/22.23 25. (All VS, (All VT2, (((T_0 != T_1) /\ ((visFreeVar T_1 T_3) /\ ((vtcheck T_2 T_3 T_4) /\ (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 VS (veabs)) VT2)))) => (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 VS (veabs))) VT2)))) (vtcheck T_2 T_3 T_4) (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) T_6) (-. (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) T_6)) (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All Ve1, (All VT2, (((Vx = Vy) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS Ve1) VT2))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS Ve1)) VT2)))))))))) (All VT2, (((T_0 != T_1) /\ ((-. (visFreeVar T_1 T_3)) /\ ((vtcheck T_2 T_3 T_4) /\ (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) VT2)))) => (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) VT2))) ### All 24 % 22.06/22.23 26. (All VS, (All VT2, (((T_0 != T_1) /\ ((-. (visFreeVar T_1 T_3)) /\ ((vtcheck T_2 T_3 T_4) /\ (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 VS (veabs)) VT2)))) => (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 VS (veabs))) VT2)))) (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All Ve1, (All VT2, (((Vx = Vy) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS Ve1) VT2))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS Ve1)) VT2)))))))))) (-. (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) T_6)) (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) T_6) (vtcheck T_2 T_3 T_4) (All VS, (All VT2, (((T_0 != T_1) /\ ((visFreeVar T_1 T_3) /\ ((vtcheck T_2 T_3 T_4) /\ (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 VS (veabs)) VT2)))) => (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 VS (veabs))) VT2)))) ### All 25 % 22.06/22.27 27. (All Vy, (All VS, (All VT2, (((T_0 != Vy) /\ ((visFreeVar Vy T_3) /\ ((vtcheck T_2 T_3 T_4) /\ (vtcheck (vbind T_0 T_4 T_2) (vabs Vy VS (veabs)) VT2)))) => (vtcheck T_2 (vsubst T_0 T_3 (vabs Vy VS (veabs))) VT2))))) (vtcheck T_2 T_3 T_4) (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) T_6) (-. (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) T_6)) (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All Ve1, (All VT2, (((Vx = Vy) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS Ve1) VT2))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS Ve1)) VT2)))))))))) (All VS, (All VT2, (((T_0 != T_1) /\ ((-. (visFreeVar T_1 T_3)) /\ ((vtcheck T_2 T_3 T_4) /\ (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 VS (veabs)) VT2)))) => (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 VS (veabs))) VT2)))) ### All 26 % 22.06/22.27 28. (All Vy, (All VS, (All VT2, (((T_0 != Vy) /\ ((-. (visFreeVar Vy T_3)) /\ ((vtcheck T_2 T_3 T_4) /\ (vtcheck (vbind T_0 T_4 T_2) (vabs Vy VS (veabs)) VT2)))) => (vtcheck T_2 (vsubst T_0 T_3 (vabs Vy VS (veabs))) VT2))))) (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All Ve1, (All VT2, (((Vx = Vy) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS Ve1) VT2))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS Ve1)) VT2)))))))))) (-. (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) T_6)) (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) T_6) (vtcheck T_2 T_3 T_4) (All Vy, (All VS, (All VT2, (((T_0 != Vy) /\ ((visFreeVar Vy T_3) /\ ((vtcheck T_2 T_3 T_4) /\ (vtcheck (vbind T_0 T_4 T_2) (vabs Vy VS (veabs)) VT2)))) => (vtcheck T_2 (vsubst T_0 T_3 (vabs Vy VS (veabs))) VT2))))) ### All 27 % 22.06/22.27 29. (All Ve, (All Vy, (All VS, (All VT2, (((T_0 != Vy) /\ ((-. (visFreeVar Vy Ve)) /\ ((vtcheck T_2 Ve T_4) /\ (vtcheck (vbind T_0 T_4 T_2) (vabs Vy VS (veabs)) VT2)))) => (vtcheck T_2 (vsubst T_0 Ve (vabs Vy VS (veabs))) VT2)))))) (All Vy, (All VS, (All VT2, (((T_0 != Vy) /\ ((visFreeVar Vy T_3) /\ ((vtcheck T_2 T_3 T_4) /\ (vtcheck (vbind T_0 T_4 T_2) (vabs Vy VS (veabs)) VT2)))) => (vtcheck T_2 (vsubst T_0 T_3 (vabs Vy VS (veabs))) VT2))))) (vtcheck T_2 T_3 T_4) (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) T_6) (-. (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) T_6)) (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All Ve1, (All VT2, (((Vx = Vy) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS Ve1) VT2))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS Ve1)) VT2)))))))))) ### All 28 % 22.06/22.27 30. (All Ve, (All Vy, (All VS, (All VT2, (((T_0 != Vy) /\ ((visFreeVar Vy Ve) /\ ((vtcheck T_2 Ve T_4) /\ (vtcheck (vbind T_0 T_4 T_2) (vabs Vy VS (veabs)) VT2)))) => (vtcheck T_2 (vsubst T_0 Ve (vabs Vy VS (veabs))) VT2)))))) (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All Ve1, (All VT2, (((Vx = Vy) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS Ve1) VT2))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS Ve1)) VT2)))))))))) (-. (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) T_6)) (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) T_6) (vtcheck T_2 T_3 T_4) (All Ve, (All Vy, (All VS, (All VT2, (((T_0 != Vy) /\ ((-. (visFreeVar Vy Ve)) /\ ((vtcheck T_2 Ve T_4) /\ (vtcheck (vbind T_0 T_4 T_2) (vabs Vy VS (veabs)) VT2)))) => (vtcheck T_2 (vsubst T_0 Ve (vabs Vy VS (veabs))) VT2)))))) ### All 29 % 22.06/22.27 31. (All Vx, (All Ve, (All Vy, (All VS, (All VT2, (((Vx != Vy) /\ ((-. (visFreeVar Vy Ve)) /\ ((vtcheck T_2 Ve T_4) /\ (vtcheck (vbind Vx T_4 T_2) (vabs Vy VS (veabs)) VT2)))) => (vtcheck T_2 (vsubst Vx Ve (vabs Vy VS (veabs))) VT2))))))) (vtcheck T_2 T_3 T_4) (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) T_6) (-. (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) T_6)) (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All Ve1, (All VT2, (((Vx = Vy) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS Ve1) VT2))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS Ve1)) VT2)))))))))) (All Ve, (All Vy, (All VS, (All VT2, (((T_0 != Vy) /\ ((visFreeVar Vy Ve) /\ ((vtcheck T_2 Ve T_4) /\ (vtcheck (vbind T_0 T_4 T_2) (vabs Vy VS (veabs)) VT2)))) => (vtcheck T_2 (vsubst T_0 Ve (vabs Vy VS (veabs))) VT2)))))) ### All 30 % 22.06/22.27 32. (All Vx, (All Ve, (All Vy, (All VS, (All VT2, (((Vx != Vy) /\ ((visFreeVar Vy Ve) /\ ((vtcheck T_2 Ve T_4) /\ (vtcheck (vbind Vx T_4 T_2) (vabs Vy VS (veabs)) VT2)))) => (vtcheck T_2 (vsubst Vx Ve (vabs Vy VS (veabs))) VT2))))))) (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All Ve1, (All VT2, (((Vx = Vy) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS Ve1) VT2))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS Ve1)) VT2)))))))))) (-. (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) T_6)) (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) T_6) (vtcheck T_2 T_3 T_4) (All Vx, (All Ve, (All Vy, (All VS, (All VT2, (((Vx != Vy) /\ ((-. (visFreeVar Vy Ve)) /\ ((vtcheck T_2 Ve T_4) /\ (vtcheck (vbind Vx T_4 T_2) (vabs Vy VS (veabs)) VT2)))) => (vtcheck T_2 (vsubst Vx Ve (vabs Vy VS (veabs))) VT2))))))) ### All 31 % 22.06/22.27 33. (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All VT2, (((Vx != Vy) /\ ((-. (visFreeVar Vy Ve)) /\ ((vtcheck VC Ve T_4) /\ (vtcheck (vbind Vx T_4 VC) (vabs Vy VS (veabs)) VT2)))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS (veabs))) VT2)))))))) (vtcheck T_2 T_3 T_4) (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) T_6) (-. (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) T_6)) (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All Ve1, (All VT2, (((Vx = Vy) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS Ve1) VT2))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS Ve1)) VT2)))))))))) (All Vx, (All Ve, (All Vy, (All VS, (All VT2, (((Vx != Vy) /\ ((visFreeVar Vy Ve) /\ ((vtcheck T_2 Ve T_4) /\ (vtcheck (vbind Vx T_4 T_2) (vabs Vy VS (veabs)) VT2)))) => (vtcheck T_2 (vsubst Vx Ve (vabs Vy VS (veabs))) VT2))))))) ### All 32 % 22.06/22.27 34. (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All VT2, (((Vx != Vy) /\ ((visFreeVar Vy Ve) /\ ((vtcheck VC Ve T_4) /\ (vtcheck (vbind Vx T_4 VC) (vabs Vy VS (veabs)) VT2)))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS (veabs))) VT2)))))))) (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All Ve1, (All VT2, (((Vx = Vy) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS Ve1) VT2))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS Ve1)) VT2)))))))))) (-. (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) T_6)) (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) T_6) (vtcheck T_2 T_3 T_4) (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All VT2, (((Vx != Vy) /\ ((-. (visFreeVar Vy Ve)) /\ ((vtcheck VC Ve T_4) /\ (vtcheck (vbind Vx T_4 VC) (vabs Vy VS (veabs)) VT2)))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS (veabs))) VT2)))))))) ### All 33 % 22.06/22.27 35. (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All VT2, (((Vx != Vy) /\ ((-. (visFreeVar Vy Ve)) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS (veabs)) VT2)))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS (veabs))) VT2))))))))) (vtcheck T_2 T_3 T_4) (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) T_6) (-. (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) T_6)) (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All Ve1, (All VT2, (((Vx = Vy) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS Ve1) VT2))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS Ve1)) VT2)))))))))) (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All VT2, (((Vx != Vy) /\ ((visFreeVar Vy Ve) /\ ((vtcheck VC Ve T_4) /\ (vtcheck (vbind Vx T_4 VC) (vabs Vy VS (veabs)) VT2)))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS (veabs))) VT2)))))))) ### All 34 % 22.06/22.29 36. (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All VT2, (((Vx != Vy) /\ ((visFreeVar Vy Ve) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS (veabs)) VT2)))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS (veabs))) VT2))))))))) (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All Ve1, (All VT2, (((Vx = Vy) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS Ve1) VT2))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS Ve1)) VT2)))))))))) (-. (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) T_6)) (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) T_6) (vtcheck T_2 T_3 T_4) (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All VT2, (((Vx != Vy) /\ ((-. (visFreeVar Vy Ve)) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS (veabs)) VT2)))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS (veabs))) VT2))))))))) ### All 35 % 22.06/22.29 37. (-. (((vtcheck T_2 T_3 T_4) /\ (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) T_6)) => (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) T_6))) (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All VT2, (((Vx != Vy) /\ ((-. (visFreeVar Vy Ve)) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS (veabs)) VT2)))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS (veabs))) VT2))))))))) (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All Ve1, (All VT2, (((Vx = Vy) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS Ve1) VT2))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS Ve1)) VT2)))))))))) (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All VT2, (((Vx != Vy) /\ ((visFreeVar Vy Ve) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS (veabs)) VT2)))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS (veabs))) VT2))))))))) ### ConjTree 36 % 22.06/22.29 38. (-. (All VT2, (((vtcheck T_2 T_3 T_4) /\ (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 T_5 (veabs)) VT2)) => (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 T_5 (veabs))) VT2)))) (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All VT2, (((Vx != Vy) /\ ((visFreeVar Vy Ve) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS (veabs)) VT2)))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS (veabs))) VT2))))))))) (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All Ve1, (All VT2, (((Vx = Vy) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS Ve1) VT2))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS Ve1)) VT2)))))))))) (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All VT2, (((Vx != Vy) /\ ((-. (visFreeVar Vy Ve)) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS (veabs)) VT2)))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS (veabs))) VT2))))))))) ### NotAllEx 37 % 22.06/22.29 39. (-. (All VS, (All VT2, (((vtcheck T_2 T_3 T_4) /\ (vtcheck (vbind T_0 T_4 T_2) (vabs T_1 VS (veabs)) VT2)) => (vtcheck T_2 (vsubst T_0 T_3 (vabs T_1 VS (veabs))) VT2))))) (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All VT2, (((Vx != Vy) /\ ((-. (visFreeVar Vy Ve)) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS (veabs)) VT2)))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS (veabs))) VT2))))))))) (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All Ve1, (All VT2, (((Vx = Vy) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS Ve1) VT2))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS Ve1)) VT2)))))))))) (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All VT2, (((Vx != Vy) /\ ((visFreeVar Vy Ve) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS (veabs)) VT2)))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS (veabs))) VT2))))))))) ### NotAllEx 38 % 22.06/22.29 40. (-. (All Vy, (All VS, (All VT2, (((vtcheck T_2 T_3 T_4) /\ (vtcheck (vbind T_0 T_4 T_2) (vabs Vy VS (veabs)) VT2)) => (vtcheck T_2 (vsubst T_0 T_3 (vabs Vy VS (veabs))) VT2)))))) (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All VT2, (((Vx != Vy) /\ ((visFreeVar Vy Ve) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS (veabs)) VT2)))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS (veabs))) VT2))))))))) (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All Ve1, (All VT2, (((Vx = Vy) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS Ve1) VT2))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS Ve1)) VT2)))))))))) (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All VT2, (((Vx != Vy) /\ ((-. (visFreeVar Vy Ve)) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS (veabs)) VT2)))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS (veabs))) VT2))))))))) ### NotAllEx 39 % 22.06/22.29 41. (-. (All Ve, (All Vy, (All VS, (All VT2, (((vtcheck T_2 Ve T_4) /\ (vtcheck (vbind T_0 T_4 T_2) (vabs Vy VS (veabs)) VT2)) => (vtcheck T_2 (vsubst T_0 Ve (vabs Vy VS (veabs))) VT2))))))) (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All VT2, (((Vx != Vy) /\ ((-. (visFreeVar Vy Ve)) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS (veabs)) VT2)))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS (veabs))) VT2))))))))) (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All Ve1, (All VT2, (((Vx = Vy) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS Ve1) VT2))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS Ve1)) VT2)))))))))) (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All VT2, (((Vx != Vy) /\ ((visFreeVar Vy Ve) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS (veabs)) VT2)))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS (veabs))) VT2))))))))) ### NotAllEx 40 % 22.06/22.29 42. (-. (All Vx, (All Ve, (All Vy, (All VS, (All VT2, (((vtcheck T_2 Ve T_4) /\ (vtcheck (vbind Vx T_4 T_2) (vabs Vy VS (veabs)) VT2)) => (vtcheck T_2 (vsubst Vx Ve (vabs Vy VS (veabs))) VT2)))))))) (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All VT2, (((Vx != Vy) /\ ((visFreeVar Vy Ve) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS (veabs)) VT2)))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS (veabs))) VT2))))))))) (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All Ve1, (All VT2, (((Vx = Vy) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS Ve1) VT2))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS Ve1)) VT2)))))))))) (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All VT2, (((Vx != Vy) /\ ((-. (visFreeVar Vy Ve)) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS (veabs)) VT2)))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS (veabs))) VT2))))))))) ### NotAllEx 41 % 22.06/22.29 43. (-. (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All VT2, (((vtcheck VC Ve T_4) /\ (vtcheck (vbind Vx T_4 VC) (vabs Vy VS (veabs)) VT2)) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS (veabs))) VT2))))))))) (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All VT2, (((Vx != Vy) /\ ((-. (visFreeVar Vy Ve)) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS (veabs)) VT2)))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS (veabs))) VT2))))))))) (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All Ve1, (All VT2, (((Vx = Vy) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS Ve1) VT2))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS Ve1)) VT2)))))))))) (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All VT2, (((Vx != Vy) /\ ((visFreeVar Vy Ve) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS (veabs)) VT2)))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS (veabs))) VT2))))))))) ### NotAllEx 42 % 22.06/22.29 44. (-. (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All VT2, (((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS (veabs)) VT2)) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS (veabs))) VT2)))))))))) (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All VT2, (((Vx != Vy) /\ ((visFreeVar Vy Ve) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS (veabs)) VT2)))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS (veabs))) VT2))))))))) (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All Ve1, (All VT2, (((Vx = Vy) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS Ve1) VT2))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS Ve1)) VT2)))))))))) (All VT, (All VC, (All Vx, (All Ve, (All Vy, (All VS, (All VT2, (((Vx != Vy) /\ ((-. (visFreeVar Vy Ve)) /\ ((vtcheck VC Ve VT) /\ (vtcheck (vbind Vx VT VC) (vabs Vy VS (veabs)) VT2)))) => (vtcheck VC (vsubst Vx Ve (vabs Vy VS (veabs))) VT2))))))))) ### NotAllEx 43 % 22.06/22.30 % SZS output end Proof % 22.06/22.30 (* END-PROOF *) %------------------------------------------------------------------------------