%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : COM141+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:16 EDT 2022 % Result : Theorem 17.82s 18.07s % Output : Proof 17.92s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : COM141+1 : TPTP v8.1.0. Released v6.4.0. % 0.07/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n026.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 17:29:08 EDT 2022 % 0.12/0.33 % CPUTime : % 17.82/18.07 % SZS status Theorem % 17.82/18.07 (* PROOF-FOUND *) % 17.82/18.07 (* BEGIN-PROOF *) % 17.82/18.07 % SZS output start Proof % 17.82/18.07 1. (T_0 = T_1) (T_0 != T_1) ### Axiom % 17.82/18.07 2. ((vlookup T_0 T_2) = (vnoType)) ((vlookup T_0 T_2) != (vnoType)) ### Axiom % 17.82/18.07 3. (vtcheck T_2 (vabs T_1 T_3 (veabs)) T_4) (-. (vtcheck T_2 (vabs T_1 T_3 (veabs)) T_4)) ### Axiom % 17.82/18.07 4. (-. (vtcheck (vbind T_0 T_5 T_2) (vabs T_1 T_3 (veabs)) T_4)) (vtcheck (vbind T_0 T_5 T_2) (vabs T_1 T_3 (veabs)) T_4) ### Axiom % 17.82/18.07 5. (((T_0 = T_1) /\ (((vlookup T_0 T_2) = (vnoType)) /\ (vtcheck T_2 (vabs T_1 T_3 (veabs)) T_4))) => (vtcheck (vbind T_0 T_5 T_2) (vabs T_1 T_3 (veabs)) T_4)) (-. (vtcheck (vbind T_0 T_5 T_2) (vabs T_1 T_3 (veabs)) T_4)) (vtcheck T_2 (vabs T_1 T_3 (veabs)) T_4) ((vlookup T_0 T_2) = (vnoType)) (T_0 = T_1) ### DisjTree 1 2 3 4 % 17.82/18.07 6. (All VT, (((T_0 = T_1) /\ (((vlookup T_0 T_2) = (vnoType)) /\ (vtcheck T_2 (vabs T_1 T_3 (veabs)) VT))) => (vtcheck (vbind T_0 T_5 T_2) (vabs T_1 T_3 (veabs)) VT))) (T_0 = T_1) ((vlookup T_0 T_2) = (vnoType)) (vtcheck T_2 (vabs T_1 T_3 (veabs)) T_4) (-. (vtcheck (vbind T_0 T_5 T_2) (vabs T_1 T_3 (veabs)) T_4)) ### All 5 % 17.82/18.07 7. (All VS1, (All VT, (((T_0 = T_1) /\ (((vlookup T_0 T_2) = (vnoType)) /\ (vtcheck T_2 (vabs T_1 VS1 (veabs)) VT))) => (vtcheck (vbind T_0 T_5 T_2) (vabs T_1 VS1 (veabs)) VT)))) (-. (vtcheck (vbind T_0 T_5 T_2) (vabs T_1 T_3 (veabs)) T_4)) (vtcheck T_2 (vabs T_1 T_3 (veabs)) T_4) ((vlookup T_0 T_2) = (vnoType)) (T_0 = T_1) ### All 6 % 17.82/18.07 8. ((vlookup T_0 T_2) = (vnoType)) ((vlookup T_0 T_2) != (vnoType)) ### Axiom % 17.82/18.07 9. (vtcheck T_2 (vabs T_1 T_3 (veabs)) T_4) (-. (vtcheck T_2 (vabs T_1 T_3 (veabs)) T_4)) ### Axiom % 17.82/18.07 10. (-. (vtcheck (vbind T_0 T_5 T_2) (vabs T_1 T_3 (veabs)) T_4)) (vtcheck (vbind T_0 T_5 T_2) (vabs T_1 T_3 (veabs)) T_4) ### Axiom % 17.82/18.07 11. (((T_0 != T_1) /\ (((vlookup T_0 T_2) = (vnoType)) /\ (vtcheck T_2 (vabs T_1 T_3 (veabs)) T_4))) => (vtcheck (vbind T_0 T_5 T_2) (vabs T_1 T_3 (veabs)) T_4)) ((vlookup T_0 T_2) = (vnoType)) (vtcheck T_2 (vabs T_1 T_3 (veabs)) T_4) (-. (vtcheck (vbind T_0 T_5 T_2) (vabs T_1 T_3 (veabs)) T_4)) (All VS1, (All VT, (((T_0 = T_1) /\ (((vlookup T_0 T_2) = (vnoType)) /\ (vtcheck T_2 (vabs T_1 VS1 (veabs)) VT))) => (vtcheck (vbind T_0 T_5 T_2) (vabs T_1 VS1 (veabs)) VT)))) ### DisjTree 7 8 9 10 % 17.82/18.07 12. (All VT, (((T_0 != T_1) /\ (((vlookup T_0 T_2) = (vnoType)) /\ (vtcheck T_2 (vabs T_1 T_3 (veabs)) VT))) => (vtcheck (vbind T_0 T_5 T_2) (vabs T_1 T_3 (veabs)) VT))) (All VS1, (All VT, (((T_0 = T_1) /\ (((vlookup T_0 T_2) = (vnoType)) /\ (vtcheck T_2 (vabs T_1 VS1 (veabs)) VT))) => (vtcheck (vbind T_0 T_5 T_2) (vabs T_1 VS1 (veabs)) VT)))) (-. (vtcheck (vbind T_0 T_5 T_2) (vabs T_1 T_3 (veabs)) T_4)) (vtcheck T_2 (vabs T_1 T_3 (veabs)) T_4) ((vlookup T_0 T_2) = (vnoType)) ### All 11 % 17.82/18.07 13. (All VS1, (All VT, (((T_0 != T_1) /\ (((vlookup T_0 T_2) = (vnoType)) /\ (vtcheck T_2 (vabs T_1 VS1 (veabs)) VT))) => (vtcheck (vbind T_0 T_5 T_2) (vabs T_1 VS1 (veabs)) VT)))) ((vlookup T_0 T_2) = (vnoType)) (vtcheck T_2 (vabs T_1 T_3 (veabs)) T_4) (-. (vtcheck (vbind T_0 T_5 T_2) (vabs T_1 T_3 (veabs)) T_4)) (All VS1, (All VT, (((T_0 = T_1) /\ (((vlookup T_0 T_2) = (vnoType)) /\ (vtcheck T_2 (vabs T_1 VS1 (veabs)) VT))) => (vtcheck (vbind T_0 T_5 T_2) (vabs T_1 VS1 (veabs)) VT)))) ### All 12 % 17.82/18.07 14. (All Vy, (All VS1, (All VT, (((T_0 = Vy) /\ (((vlookup T_0 T_2) = (vnoType)) /\ (vtcheck T_2 (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind T_0 T_5 T_2) (vabs Vy VS1 (veabs)) VT))))) (-. (vtcheck (vbind T_0 T_5 T_2) (vabs T_1 T_3 (veabs)) T_4)) (vtcheck T_2 (vabs T_1 T_3 (veabs)) T_4) ((vlookup T_0 T_2) = (vnoType)) (All VS1, (All VT, (((T_0 != T_1) /\ (((vlookup T_0 T_2) = (vnoType)) /\ (vtcheck T_2 (vabs T_1 VS1 (veabs)) VT))) => (vtcheck (vbind T_0 T_5 T_2) (vabs T_1 VS1 (veabs)) VT)))) ### All 13 % 17.82/18.07 15. (All Vy, (All VS1, (All VT, (((T_0 != Vy) /\ (((vlookup T_0 T_2) = (vnoType)) /\ (vtcheck T_2 (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind T_0 T_5 T_2) (vabs Vy VS1 (veabs)) VT))))) ((vlookup T_0 T_2) = (vnoType)) (vtcheck T_2 (vabs T_1 T_3 (veabs)) T_4) (-. (vtcheck (vbind T_0 T_5 T_2) (vabs T_1 T_3 (veabs)) T_4)) (All Vy, (All VS1, (All VT, (((T_0 = Vy) /\ (((vlookup T_0 T_2) = (vnoType)) /\ (vtcheck T_2 (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind T_0 T_5 T_2) (vabs Vy VS1 (veabs)) VT))))) ### All 14 % 17.82/18.07 16. (All VC, (All Vy, (All VS1, (All VT, (((T_0 = Vy) /\ (((vlookup T_0 VC) = (vnoType)) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind T_0 T_5 VC) (vabs Vy VS1 (veabs)) VT)))))) (-. (vtcheck (vbind T_0 T_5 T_2) (vabs T_1 T_3 (veabs)) T_4)) (vtcheck T_2 (vabs T_1 T_3 (veabs)) T_4) ((vlookup T_0 T_2) = (vnoType)) (All Vy, (All VS1, (All VT, (((T_0 != Vy) /\ (((vlookup T_0 T_2) = (vnoType)) /\ (vtcheck T_2 (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind T_0 T_5 T_2) (vabs Vy VS1 (veabs)) VT))))) ### All 15 % 17.82/18.07 17. (All VC, (All Vy, (All VS1, (All VT, (((T_0 != Vy) /\ (((vlookup T_0 VC) = (vnoType)) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind T_0 T_5 VC) (vabs Vy VS1 (veabs)) VT)))))) ((vlookup T_0 T_2) = (vnoType)) (vtcheck T_2 (vabs T_1 T_3 (veabs)) T_4) (-. (vtcheck (vbind T_0 T_5 T_2) (vabs T_1 T_3 (veabs)) T_4)) (All VC, (All Vy, (All VS1, (All VT, (((T_0 = Vy) /\ (((vlookup T_0 VC) = (vnoType)) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind T_0 T_5 VC) (vabs Vy VS1 (veabs)) VT)))))) ### All 16 % 17.82/18.07 18. (All VS, (All VC, (All Vy, (All VS1, (All VT, (((T_0 = Vy) /\ (((vlookup T_0 VC) = (vnoType)) /\ (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_2) (vabs T_1 T_3 (veabs)) T_4)) (vtcheck T_2 (vabs T_1 T_3 (veabs)) T_4) ((vlookup T_0 T_2) = (vnoType)) (All VC, (All Vy, (All VS1, (All VT, (((T_0 != Vy) /\ (((vlookup T_0 VC) = (vnoType)) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind T_0 T_5 VC) (vabs Vy VS1 (veabs)) VT)))))) ### All 17 % 17.82/18.07 19. (All VS, (All VC, (All Vy, (All VS1, (All VT, (((T_0 != Vy) /\ (((vlookup T_0 VC) = (vnoType)) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind T_0 VS VC) (vabs Vy VS1 (veabs)) VT))))))) ((vlookup T_0 T_2) = (vnoType)) (vtcheck T_2 (vabs T_1 T_3 (veabs)) T_4) (-. (vtcheck (vbind T_0 T_5 T_2) (vabs T_1 T_3 (veabs)) T_4)) (All VS, (All VC, (All Vy, (All VS1, (All VT, (((T_0 = Vy) /\ (((vlookup T_0 VC) = (vnoType)) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind T_0 VS VC) (vabs Vy VS1 (veabs)) VT))))))) ### All 18 % 17.82/18.07 20. (All Vx, (All VS, (All VC, (All Vy, (All VS1, (All VT, (((Vx = Vy) /\ (((vlookup Vx VC) = (vnoType)) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind Vx VS VC) (vabs Vy VS1 (veabs)) VT)))))))) (-. (vtcheck (vbind T_0 T_5 T_2) (vabs T_1 T_3 (veabs)) T_4)) (vtcheck T_2 (vabs T_1 T_3 (veabs)) T_4) ((vlookup T_0 T_2) = (vnoType)) (All VS, (All VC, (All Vy, (All VS1, (All VT, (((T_0 != Vy) /\ (((vlookup T_0 VC) = (vnoType)) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind T_0 VS VC) (vabs Vy VS1 (veabs)) VT))))))) ### All 19 % 17.82/18.07 21. (All Vx, (All VS, (All VC, (All Vy, (All VS1, (All VT, (((Vx != Vy) /\ (((vlookup Vx VC) = (vnoType)) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind Vx VS VC) (vabs Vy VS1 (veabs)) VT)))))))) ((vlookup T_0 T_2) = (vnoType)) (vtcheck T_2 (vabs T_1 T_3 (veabs)) T_4) (-. (vtcheck (vbind T_0 T_5 T_2) (vabs T_1 T_3 (veabs)) T_4)) (All Vx, (All VS, (All VC, (All Vy, (All VS1, (All VT, (((Vx = Vy) /\ (((vlookup Vx VC) = (vnoType)) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind Vx VS VC) (vabs Vy VS1 (veabs)) VT)))))))) ### All 20 % 17.82/18.07 22. (-. ((((vlookup T_0 T_2) = (vnoType)) /\ (vtcheck T_2 (vabs T_1 T_3 (veabs)) T_4)) => (vtcheck (vbind T_0 T_5 T_2) (vabs T_1 T_3 (veabs)) T_4))) (All Vx, (All VS, (All VC, (All Vy, (All VS1, (All VT, (((Vx = Vy) /\ (((vlookup Vx VC) = (vnoType)) /\ (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) /\ (((vlookup Vx VC) = (vnoType)) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind Vx VS VC) (vabs Vy VS1 (veabs)) VT)))))))) ### ConjTree 21 % 17.82/18.07 23. (-. (All VT, ((((vlookup T_0 T_2) = (vnoType)) /\ (vtcheck T_2 (vabs T_1 T_3 (veabs)) VT)) => (vtcheck (vbind T_0 T_5 T_2) (vabs T_1 T_3 (veabs)) VT)))) (All Vx, (All VS, (All VC, (All Vy, (All VS1, (All VT, (((Vx != Vy) /\ (((vlookup Vx VC) = (vnoType)) /\ (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) /\ (((vlookup Vx VC) = (vnoType)) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind Vx VS VC) (vabs Vy VS1 (veabs)) VT)))))))) ### NotAllEx 22 % 17.92/18.08 24. (-. (All VS1, (All VT, ((((vlookup T_0 T_2) = (vnoType)) /\ (vtcheck T_2 (vabs T_1 VS1 (veabs)) VT)) => (vtcheck (vbind T_0 T_5 T_2) (vabs T_1 VS1 (veabs)) VT))))) (All Vx, (All VS, (All VC, (All Vy, (All VS1, (All VT, (((Vx = Vy) /\ (((vlookup Vx VC) = (vnoType)) /\ (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) /\ (((vlookup Vx VC) = (vnoType)) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind Vx VS VC) (vabs Vy VS1 (veabs)) VT)))))))) ### NotAllEx 23 % 17.92/18.08 25. (-. (All Vy, (All VS1, (All VT, ((((vlookup T_0 T_2) = (vnoType)) /\ (vtcheck T_2 (vabs Vy VS1 (veabs)) VT)) => (vtcheck (vbind T_0 T_5 T_2) (vabs Vy VS1 (veabs)) VT)))))) (All Vx, (All VS, (All VC, (All Vy, (All VS1, (All VT, (((Vx != Vy) /\ (((vlookup Vx VC) = (vnoType)) /\ (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) /\ (((vlookup Vx VC) = (vnoType)) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind Vx VS VC) (vabs Vy VS1 (veabs)) VT)))))))) ### NotAllEx 24 % 17.92/18.08 26. (-. (All VC, (All Vy, (All VS1, (All VT, ((((vlookup T_0 VC) = (vnoType)) /\ (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) /\ (((vlookup Vx VC) = (vnoType)) /\ (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) /\ (((vlookup Vx VC) = (vnoType)) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind Vx VS VC) (vabs Vy VS1 (veabs)) VT)))))))) ### NotAllEx 25 % 17.92/18.08 27. (-. (All VS, (All VC, (All Vy, (All VS1, (All VT, ((((vlookup T_0 VC) = (vnoType)) /\ (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) /\ (((vlookup Vx VC) = (vnoType)) /\ (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) /\ (((vlookup Vx VC) = (vnoType)) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind Vx VS VC) (vabs Vy VS1 (veabs)) VT)))))))) ### NotAllEx 26 % 17.92/18.08 28. (-. (All Vx, (All VS, (All VC, (All Vy, (All VS1, (All VT, ((((vlookup Vx VC) = (vnoType)) /\ (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) /\ (((vlookup Vx VC) = (vnoType)) /\ (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) /\ (((vlookup Vx VC) = (vnoType)) /\ (vtcheck VC (vabs Vy VS1 (veabs)) VT))) => (vtcheck (vbind Vx VS VC) (vabs Vy VS1 (veabs)) VT)))))))) ### NotAllEx 27 % 17.92/18.08 % SZS output end Proof % 17.92/18.08 (* END-PROOF *) %------------------------------------------------------------------------------