%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : COM125+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 : n026.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:13 EDT 2022 % Result : Theorem 22.74s 22.97s % Output : Proof 22.80s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.08 % Problem : COM125+1 : TPTP v8.1.0. Released v6.4.0. % 0.04/0.08 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.08/0.28 % Computer : n026.cluster.edu % 0.08/0.28 % Model : x86_64 x86_64 % 0.08/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.28 % Memory : 8042.1875MB % 0.08/0.28 % OS : Linux 3.10.0-693.el7.x86_64 % 0.08/0.28 % CPULimit : 300 % 0.08/0.28 % WCLimit : 600 % 0.08/0.28 % DateTime : Thu Jun 16 18:28:23 EDT 2022 % 0.08/0.28 % CPUTime : % 22.74/22.97 % SZS status Theorem % 22.74/22.97 (* PROOF-FOUND *) % 22.74/22.97 (* BEGIN-PROOF *) % 22.74/22.97 % SZS output start Proof % 22.74/22.97 1. (T_0 = T_1) (T_0 != T_1) ### Axiom % 22.74/22.97 2. (-. (visFreeVar T_0 (vabs T_1 T_2 (veabs)))) (visFreeVar T_0 (vabs T_1 T_2 (veabs))) ### Axiom % 22.74/22.97 3. (vtcheck T_3 (vabs T_1 T_2 (veabs)) T_4) (-. (vtcheck T_3 (vabs T_1 T_2 (veabs)) T_4)) ### Axiom % 22.74/22.97 4. (-. (vtcheck (vbind T_0 T_5 T_3) (vabs T_1 T_2 (veabs)) T_4)) (vtcheck (vbind T_0 T_5 T_3) (vabs T_1 T_2 (veabs)) T_4) ### Axiom % 22.74/22.97 5. (((T_0 = T_1) /\ ((-. (visFreeVar T_0 (vabs T_1 T_2 (veabs)))) /\ (vtcheck T_3 (vabs T_1 T_2 (veabs)) T_4))) => (vtcheck (vbind T_0 T_5 T_3) (vabs T_1 T_2 (veabs)) T_4)) (-. (vtcheck (vbind T_0 T_5 T_3) (vabs T_1 T_2 (veabs)) T_4)) (vtcheck T_3 (vabs T_1 T_2 (veabs)) T_4) (-. (visFreeVar T_0 (vabs T_1 T_2 (veabs)))) (T_0 = T_1) ### DisjTree 1 2 3 4 % 22.74/22.97 6. (All VT, (((T_0 = T_1) /\ ((-. (visFreeVar T_0 (vabs T_1 T_2 (veabs)))) /\ (vtcheck T_3 (vabs T_1 T_2 (veabs)) VT))) => (vtcheck (vbind T_0 T_5 T_3) (vabs T_1 T_2 (veabs)) VT))) (T_0 = T_1) (-. (visFreeVar T_0 (vabs T_1 T_2 (veabs)))) (vtcheck T_3 (vabs T_1 T_2 (veabs)) T_4) (-. (vtcheck (vbind T_0 T_5 T_3) (vabs T_1 T_2 (veabs)) T_4)) ### All 5 % 22.74/22.97 7. (-. (visFreeVar T_0 (vabs T_1 T_2 (veabs)))) (visFreeVar T_0 (vabs T_1 T_2 (veabs))) ### Axiom % 22.74/22.97 8. (vtcheck T_3 (vabs T_1 T_2 (veabs)) T_4) (-. (vtcheck T_3 (vabs T_1 T_2 (veabs)) T_4)) ### Axiom % 22.74/22.97 9. (-. (vtcheck (vbind T_0 T_5 T_3) (vabs T_1 T_2 (veabs)) T_4)) (vtcheck (vbind T_0 T_5 T_3) (vabs T_1 T_2 (veabs)) T_4) ### Axiom % 22.74/22.97 10. (((T_0 != T_1) /\ ((-. (visFreeVar T_0 (vabs T_1 T_2 (veabs)))) /\ (vtcheck T_3 (vabs T_1 T_2 (veabs)) T_4))) => (vtcheck (vbind T_0 T_5 T_3) (vabs T_1 T_2 (veabs)) T_4)) (-. (vtcheck (vbind T_0 T_5 T_3) (vabs T_1 T_2 (veabs)) T_4)) (vtcheck T_3 (vabs T_1 T_2 (veabs)) T_4) (-. (visFreeVar T_0 (vabs T_1 T_2 (veabs)))) (All VT, (((T_0 = T_1) /\ ((-. (visFreeVar T_0 (vabs T_1 T_2 (veabs)))) /\ (vtcheck T_3 (vabs T_1 T_2 (veabs)) VT))) => (vtcheck (vbind T_0 T_5 T_3) (vabs T_1 T_2 (veabs)) VT))) ### DisjTree 6 7 8 9 % 22.74/22.97 11. (All VT, (((T_0 != T_1) /\ ((-. (visFreeVar T_0 (vabs T_1 T_2 (veabs)))) /\ (vtcheck T_3 (vabs T_1 T_2 (veabs)) VT))) => (vtcheck (vbind T_0 T_5 T_3) (vabs T_1 T_2 (veabs)) VT))) (All VT, (((T_0 = T_1) /\ ((-. (visFreeVar T_0 (vabs T_1 T_2 (veabs)))) /\ (vtcheck T_3 (vabs T_1 T_2 (veabs)) VT))) => (vtcheck (vbind T_0 T_5 T_3) (vabs T_1 T_2 (veabs)) VT))) (-. (visFreeVar T_0 (vabs T_1 T_2 (veabs)))) (vtcheck T_3 (vabs T_1 T_2 (veabs)) T_4) (-. (vtcheck (vbind T_0 T_5 T_3) (vabs T_1 T_2 (veabs)) T_4)) ### All 10 % 22.74/22.97 12. (All VS1, (All VT, (((T_0 = T_1) /\ ((-. (visFreeVar T_0 (vabs T_1 VS1 (veabs)))) /\ (vtcheck T_3 (vabs T_1 VS1 (veabs)) VT))) => (vtcheck (vbind T_0 T_5 T_3) (vabs T_1 VS1 (veabs)) VT)))) (-. (vtcheck (vbind T_0 T_5 T_3) (vabs T_1 T_2 (veabs)) T_4)) (vtcheck T_3 (vabs T_1 T_2 (veabs)) T_4) (-. (visFreeVar T_0 (vabs T_1 T_2 (veabs)))) (All VT, (((T_0 != T_1) /\ ((-. (visFreeVar T_0 (vabs T_1 T_2 (veabs)))) /\ (vtcheck T_3 (vabs T_1 T_2 (veabs)) VT))) => (vtcheck (vbind T_0 T_5 T_3) (vabs T_1 T_2 (veabs)) VT))) ### All 11 % 22.74/22.97 13. (All VS1, (All VT, (((T_0 != T_1) /\ ((-. (visFreeVar T_0 (vabs T_1 VS1 (veabs)))) /\ (vtcheck T_3 (vabs T_1 VS1 (veabs)) VT))) => (vtcheck (vbind T_0 T_5 T_3) (vabs T_1 VS1 (veabs)) VT)))) (-. (visFreeVar T_0 (vabs T_1 T_2 (veabs)))) (vtcheck T_3 (vabs T_1 T_2 (veabs)) T_4) (-. (vtcheck (vbind T_0 T_5 T_3) (vabs T_1 T_2 (veabs)) T_4)) (All VS1, (All VT, (((T_0 = T_1) /\ ((-. (visFreeVar T_0 (vabs T_1 VS1 (veabs)))) /\ (vtcheck T_3 (vabs T_1 VS1 (veabs)) VT))) => (vtcheck (vbind T_0 T_5 T_3) (vabs T_1 VS1 (veabs)) VT)))) ### All 12 % 22.74/22.97 14. (All Vy, (All VS1, (All VT, (((T_0 = Vy) /\ ((-. (visFreeVar T_0 (vabs Vy VS1 (veabs)))) /\ (vtcheck T_3 (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind T_0 T_5 T_3) (vabs Vy VS1 (veabs)) VT))))) (-. (vtcheck (vbind T_0 T_5 T_3) (vabs T_1 T_2 (veabs)) T_4)) (vtcheck T_3 (vabs T_1 T_2 (veabs)) T_4) (-. (visFreeVar T_0 (vabs T_1 T_2 (veabs)))) (All VS1, (All VT, (((T_0 != T_1) /\ ((-. (visFreeVar T_0 (vabs T_1 VS1 (veabs)))) /\ (vtcheck T_3 (vabs T_1 VS1 (veabs)) VT))) => (vtcheck (vbind T_0 T_5 T_3) (vabs T_1 VS1 (veabs)) VT)))) ### All 13 % 22.74/22.97 15. (All Vy, (All VS1, (All VT, (((T_0 != Vy) /\ ((-. (visFreeVar T_0 (vabs Vy VS1 (veabs)))) /\ (vtcheck T_3 (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind T_0 T_5 T_3) (vabs Vy VS1 (veabs)) VT))))) (-. (visFreeVar T_0 (vabs T_1 T_2 (veabs)))) (vtcheck T_3 (vabs T_1 T_2 (veabs)) T_4) (-. (vtcheck (vbind T_0 T_5 T_3) (vabs T_1 T_2 (veabs)) T_4)) (All Vy, (All VS1, (All VT, (((T_0 = Vy) /\ ((-. (visFreeVar T_0 (vabs Vy VS1 (veabs)))) /\ (vtcheck T_3 (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind T_0 T_5 T_3) (vabs Vy VS1 (veabs)) VT))))) ### All 14 % 22.74/22.97 16. (All VC, (All Vy, (All VS1, (All VT, (((T_0 != Vy) /\ ((-. (visFreeVar T_0 (vabs Vy VS1 (veabs)))) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind T_0 T_5 VC) (vabs Vy VS1 (veabs)) VT)))))) (All Vy, (All VS1, (All VT, (((T_0 = Vy) /\ ((-. (visFreeVar T_0 (vabs Vy VS1 (veabs)))) /\ (vtcheck T_3 (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind T_0 T_5 T_3) (vabs Vy VS1 (veabs)) VT))))) (-. (vtcheck (vbind T_0 T_5 T_3) (vabs T_1 T_2 (veabs)) T_4)) (vtcheck T_3 (vabs T_1 T_2 (veabs)) T_4) (-. (visFreeVar T_0 (vabs T_1 T_2 (veabs)))) ### All 15 % 22.74/22.97 17. (All VC, (All Vy, (All VS1, (All VT, (((T_0 = Vy) /\ ((-. (visFreeVar T_0 (vabs Vy VS1 (veabs)))) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind T_0 T_5 VC) (vabs Vy VS1 (veabs)) VT)))))) (-. (visFreeVar T_0 (vabs T_1 T_2 (veabs)))) (vtcheck T_3 (vabs T_1 T_2 (veabs)) T_4) (-. (vtcheck (vbind T_0 T_5 T_3) (vabs T_1 T_2 (veabs)) T_4)) (All VC, (All Vy, (All VS1, (All VT, (((T_0 != Vy) /\ ((-. (visFreeVar T_0 (vabs Vy VS1 (veabs)))) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind T_0 T_5 VC) (vabs Vy VS1 (veabs)) VT)))))) ### All 16 % 22.74/22.97 18. (All VS, (All VC, (All Vy, (All VS1, (All VT, (((T_0 != Vy) /\ ((-. (visFreeVar T_0 (vabs Vy VS1 (veabs)))) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind T_0 VS VC) (vabs Vy VS1 (veabs)) VT))))))) (-. (vtcheck (vbind T_0 T_5 T_3) (vabs T_1 T_2 (veabs)) T_4)) (vtcheck T_3 (vabs T_1 T_2 (veabs)) T_4) (-. (visFreeVar T_0 (vabs T_1 T_2 (veabs)))) (All VC, (All Vy, (All VS1, (All VT, (((T_0 = Vy) /\ ((-. (visFreeVar T_0 (vabs Vy VS1 (veabs)))) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind T_0 T_5 VC) (vabs Vy VS1 (veabs)) VT)))))) ### All 17 % 22.74/22.97 19. (All VS, (All VC, (All Vy, (All VS1, (All VT, (((T_0 = Vy) /\ ((-. (visFreeVar T_0 (vabs Vy VS1 (veabs)))) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind T_0 VS VC) (vabs Vy VS1 (veabs)) VT))))))) (-. (visFreeVar T_0 (vabs T_1 T_2 (veabs)))) (vtcheck T_3 (vabs T_1 T_2 (veabs)) T_4) (-. (vtcheck (vbind T_0 T_5 T_3) (vabs T_1 T_2 (veabs)) T_4)) (All VS, (All VC, (All Vy, (All VS1, (All VT, (((T_0 != Vy) /\ ((-. (visFreeVar T_0 (vabs Vy VS1 (veabs)))) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind T_0 VS VC) (vabs Vy VS1 (veabs)) VT))))))) ### All 18 % 22.74/22.97 20. (All Vx, (All VS, (All VC, (All Vy, (All VS1, (All VT, (((Vx != Vy) /\ ((-. (visFreeVar Vx (vabs Vy VS1 (veabs)))) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind Vx VS VC) (vabs Vy VS1 (veabs)) VT)))))))) (-. (vtcheck (vbind T_0 T_5 T_3) (vabs T_1 T_2 (veabs)) T_4)) (vtcheck T_3 (vabs T_1 T_2 (veabs)) T_4) (-. (visFreeVar T_0 (vabs T_1 T_2 (veabs)))) (All VS, (All VC, (All Vy, (All VS1, (All VT, (((T_0 = Vy) /\ ((-. (visFreeVar T_0 (vabs Vy VS1 (veabs)))) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind T_0 VS VC) (vabs Vy VS1 (veabs)) VT))))))) ### All 19 % 22.74/22.97 21. (All Vx, (All VS, (All VC, (All Vy, (All VS1, (All VT, (((Vx = Vy) /\ ((-. (visFreeVar Vx (vabs Vy VS1 (veabs)))) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind Vx VS VC) (vabs Vy VS1 (veabs)) VT)))))))) (-. (visFreeVar T_0 (vabs T_1 T_2 (veabs)))) (vtcheck T_3 (vabs T_1 T_2 (veabs)) T_4) (-. (vtcheck (vbind T_0 T_5 T_3) (vabs T_1 T_2 (veabs)) T_4)) (All Vx, (All VS, (All VC, (All Vy, (All VS1, (All VT, (((Vx != Vy) /\ ((-. (visFreeVar Vx (vabs Vy VS1 (veabs)))) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind Vx VS VC) (vabs Vy VS1 (veabs)) VT)))))))) ### All 20 % 22.80/22.98 22. (-. (((-. (visFreeVar T_0 (vabs T_1 T_2 (veabs)))) /\ (vtcheck T_3 (vabs T_1 T_2 (veabs)) T_4)) => (vtcheck (vbind T_0 T_5 T_3) (vabs T_1 T_2 (veabs)) T_4))) (All Vx, (All VS, (All VC, (All Vy, (All VS1, (All VT, (((Vx != Vy) /\ ((-. (visFreeVar Vx (vabs Vy VS1 (veabs)))) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind Vx VS VC) (vabs Vy VS1 (veabs)) VT)))))))) (All Vx, (All VS, (All VC, (All Vy, (All VS1, (All VT, (((Vx = Vy) /\ ((-. (visFreeVar Vx (vabs Vy VS1 (veabs)))) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind Vx VS VC) (vabs Vy VS1 (veabs)) VT)))))))) ### ConjTree 21 % 22.80/22.98 23. (-. (All VT, (((-. (visFreeVar T_0 (vabs T_1 T_2 (veabs)))) /\ (vtcheck T_3 (vabs T_1 T_2 (veabs)) VT)) => (vtcheck (vbind T_0 T_5 T_3) (vabs T_1 T_2 (veabs)) VT)))) (All Vx, (All VS, (All VC, (All Vy, (All VS1, (All VT, (((Vx = Vy) /\ ((-. (visFreeVar Vx (vabs Vy VS1 (veabs)))) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind Vx VS VC) (vabs Vy VS1 (veabs)) VT)))))))) (All Vx, (All VS, (All VC, (All Vy, (All VS1, (All VT, (((Vx != Vy) /\ ((-. (visFreeVar Vx (vabs Vy VS1 (veabs)))) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind Vx VS VC) (vabs Vy VS1 (veabs)) VT)))))))) ### NotAllEx 22 % 22.80/22.98 24. (-. (All VS1, (All VT, (((-. (visFreeVar T_0 (vabs T_1 VS1 (veabs)))) /\ (vtcheck T_3 (vabs T_1 VS1 (veabs)) VT)) => (vtcheck (vbind T_0 T_5 T_3) (vabs T_1 VS1 (veabs)) VT))))) (All Vx, (All VS, (All VC, (All Vy, (All VS1, (All VT, (((Vx != Vy) /\ ((-. (visFreeVar Vx (vabs Vy VS1 (veabs)))) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind Vx VS VC) (vabs Vy VS1 (veabs)) VT)))))))) (All Vx, (All VS, (All VC, (All Vy, (All VS1, (All VT, (((Vx = Vy) /\ ((-. (visFreeVar Vx (vabs Vy VS1 (veabs)))) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind Vx VS VC) (vabs Vy VS1 (veabs)) VT)))))))) ### NotAllEx 23 % 22.80/22.98 25. (-. (All Vy, (All VS1, (All VT, (((-. (visFreeVar T_0 (vabs Vy VS1 (veabs)))) /\ (vtcheck T_3 (vabs Vy VS1 (veabs)) VT)) => (vtcheck (vbind T_0 T_5 T_3) (vabs Vy VS1 (veabs)) VT)))))) (All Vx, (All VS, (All VC, (All Vy, (All VS1, (All VT, (((Vx = Vy) /\ ((-. (visFreeVar Vx (vabs Vy VS1 (veabs)))) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind Vx VS VC) (vabs Vy VS1 (veabs)) VT)))))))) (All Vx, (All VS, (All VC, (All Vy, (All VS1, (All VT, (((Vx != Vy) /\ ((-. (visFreeVar Vx (vabs Vy VS1 (veabs)))) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind Vx VS VC) (vabs Vy VS1 (veabs)) VT)))))))) ### NotAllEx 24 % 22.80/22.98 26. (-. (All VC, (All Vy, (All VS1, (All VT, (((-. (visFreeVar T_0 (vabs Vy VS1 (veabs)))) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT)) => (vtcheck (vbind T_0 T_5 VC) (vabs Vy VS1 (veabs)) VT))))))) (All Vx, (All VS, (All VC, (All Vy, (All VS1, (All VT, (((Vx != Vy) /\ ((-. (visFreeVar Vx (vabs Vy VS1 (veabs)))) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind Vx VS VC) (vabs Vy VS1 (veabs)) VT)))))))) (All Vx, (All VS, (All VC, (All Vy, (All VS1, (All VT, (((Vx = Vy) /\ ((-. (visFreeVar Vx (vabs Vy VS1 (veabs)))) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind Vx VS VC) (vabs Vy VS1 (veabs)) VT)))))))) ### NotAllEx 25 % 22.80/22.98 27. (-. (All VS, (All VC, (All Vy, (All VS1, (All VT, (((-. (visFreeVar T_0 (vabs Vy VS1 (veabs)))) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT)) => (vtcheck (vbind T_0 VS VC) (vabs Vy VS1 (veabs)) VT)))))))) (All Vx, (All VS, (All VC, (All Vy, (All VS1, (All VT, (((Vx = Vy) /\ ((-. (visFreeVar Vx (vabs Vy VS1 (veabs)))) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind Vx VS VC) (vabs Vy VS1 (veabs)) VT)))))))) (All Vx, (All VS, (All VC, (All Vy, (All VS1, (All VT, (((Vx != Vy) /\ ((-. (visFreeVar Vx (vabs Vy VS1 (veabs)))) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind Vx VS VC) (vabs Vy VS1 (veabs)) VT)))))))) ### NotAllEx 26 % 22.80/22.98 28. (-. (All Vx, (All VS, (All VC, (All Vy, (All VS1, (All VT, (((-. (visFreeVar Vx (vabs Vy VS1 (veabs)))) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT)) => (vtcheck (vbind Vx VS VC) (vabs Vy VS1 (veabs)) VT))))))))) (All Vx, (All VS, (All VC, (All Vy, (All VS1, (All VT, (((Vx != Vy) /\ ((-. (visFreeVar Vx (vabs Vy VS1 (veabs)))) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind Vx VS VC) (vabs Vy VS1 (veabs)) VT)))))))) (All Vx, (All VS, (All VC, (All Vy, (All VS1, (All VT, (((Vx = Vy) /\ ((-. (visFreeVar Vx (vabs Vy VS1 (veabs)))) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind Vx VS VC) (vabs Vy VS1 (veabs)) VT)))))))) ### NotAllEx 27 % 22.80/22.98 % SZS output end Proof % 22.80/22.98 (* END-PROOF *) %------------------------------------------------------------------------------