%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : GEO112+1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n029.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 : Sat Jul 16 06:30:09 EDT 2022 % Result : Theorem 2.73s 2.91s % Output : Proof 2.73s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : GEO112+1 : TPTP v8.1.0. Released v2.4.0. % 0.07/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.13/0.34 % Computer : n029.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Fri Jun 17 23:38:44 EDT 2022 % 0.13/0.34 % CPUTime : % 2.73/2.91 % SZS status Theorem % 2.73/2.91 (* PROOF-FOUND *) % 2.73/2.91 (* BEGIN-PROOF *) % 2.73/2.91 % SZS output start Proof % 2.73/2.91 1. (T_0 != T_1) (T_1 = T_0) ### Sym(=) % 2.73/2.91 2. (-. (T_1 != T_0)) (T_0 != T_1) ### NotNot 1 % 2.73/2.91 3. (All P, ((incident_c P T_2) => (incident_c P T_3))) (-. (All P, ((incident_c P T_2) => (incident_c P T_3)))) ### Axiom % 2.73/2.91 4. (-. (part_of T_2 T_3)) (All P, ((incident_c P T_2) => (incident_c P T_3))) ### Definition-Pseudo(part_of) 3 % 2.73/2.91 5. ((incident_c T_1 T_2) /\ (All C1, (All C2, (((part_of C1 T_2) /\ ((part_of C2 T_2) /\ ((incident_c T_1 C1) /\ (incident_c T_1 C2)))) => ((part_of C1 C2) \/ (part_of C2 C1)))))) (-. ((incident_c T_1 T_2) /\ (All C1, (All C2, (((part_of C1 T_2) /\ ((part_of C2 T_2) /\ ((incident_c T_1 C1) /\ (incident_c T_1 C2)))) => ((part_of C1 C2) \/ (part_of C2 C1))))))) ### Axiom % 2.73/2.91 6. (-. (end_point T_1 T_2)) ((incident_c T_1 T_2) /\ (All C1, (All C2, (((part_of C1 T_2) /\ ((part_of C2 T_2) /\ ((incident_c T_1 C1) /\ (incident_c T_1 C2)))) => ((part_of C1 C2) \/ (part_of C2 C1)))))) ### Definition-Pseudo(end_point) 5 % 2.73/2.91 7. ((incident_c T_0 T_2) /\ (All C1, (All C2, (((part_of C1 T_2) /\ ((part_of C2 T_2) /\ ((incident_c T_0 C1) /\ (incident_c T_0 C2)))) => ((part_of C1 C2) \/ (part_of C2 C1)))))) (-. ((incident_c T_0 T_2) /\ (All C1, (All C2, (((part_of C1 T_2) /\ ((part_of C2 T_2) /\ ((incident_c T_0 C1) /\ (incident_c T_0 C2)))) => ((part_of C1 C2) \/ (part_of C2 C1))))))) ### Axiom % 2.73/2.91 8. (-. (end_point T_0 T_2)) ((incident_c T_0 T_2) /\ (All C1, (All C2, (((part_of C1 T_2) /\ ((part_of C2 T_2) /\ ((incident_c T_0 C1) /\ (incident_c T_0 C2)))) => ((part_of C1 C2) \/ (part_of C2 C1)))))) ### Definition-Pseudo(end_point) 7 % 2.73/2.91 9. ((incident_c T_4 T_2) /\ (-. (end_point T_4 T_2))) (-. ((incident_c T_4 T_2) /\ (-. (end_point T_4 T_2)))) ### Axiom % 2.73/2.91 10. (-. (inner_point T_4 T_2)) ((incident_c T_4 T_2) /\ (-. (end_point T_4 T_2))) ### Definition-Pseudo(inner_point) 9 % 2.73/2.91 11. (-. ((part_of T_2 T_3) /\ ((end_point T_1 T_2) /\ ((end_point T_0 T_2) /\ (inner_point T_4 T_2))))) ((incident_c T_4 T_2) /\ (-. (end_point T_4 T_2))) ((incident_c T_0 T_2) /\ (All C1, (All C2, (((part_of C1 T_2) /\ ((part_of C2 T_2) /\ ((incident_c T_0 C1) /\ (incident_c T_0 C2)))) => ((part_of C1 C2) \/ (part_of C2 C1)))))) ((incident_c T_1 T_2) /\ (All C1, (All C2, (((part_of C1 T_2) /\ ((part_of C2 T_2) /\ ((incident_c T_1 C1) /\ (incident_c T_1 C2)))) => ((part_of C1 C2) \/ (part_of C2 C1)))))) (All P, ((incident_c P T_2) => (incident_c P T_3))) ### DisjTree 4 6 8 10 % 2.73/2.91 12. (-. (Ex Cpp, ((part_of Cpp T_3) /\ ((end_point T_1 Cpp) /\ ((end_point T_0 Cpp) /\ (inner_point T_4 Cpp)))))) (All P, ((incident_c P T_2) => (incident_c P T_3))) ((incident_c T_1 T_2) /\ (All C1, (All C2, (((part_of C1 T_2) /\ ((part_of C2 T_2) /\ ((incident_c T_1 C1) /\ (incident_c T_1 C2)))) => ((part_of C1 C2) \/ (part_of C2 C1)))))) ((incident_c T_0 T_2) /\ (All C1, (All C2, (((part_of C1 T_2) /\ ((part_of C2 T_2) /\ ((incident_c T_0 C1) /\ (incident_c T_0 C2)))) => ((part_of C1 C2) \/ (part_of C2 C1)))))) ((incident_c T_4 T_2) /\ (-. (end_point T_4 T_2))) ### NotExists 11 % 2.73/2.91 13. (-. ((T_1 != T_0) /\ (Ex Cpp, ((part_of Cpp T_3) /\ ((end_point T_1 Cpp) /\ ((end_point T_0 Cpp) /\ (inner_point T_4 Cpp))))))) ((incident_c T_4 T_2) /\ (-. (end_point T_4 T_2))) ((incident_c T_0 T_2) /\ (All C1, (All C2, (((part_of C1 T_2) /\ ((part_of C2 T_2) /\ ((incident_c T_0 C1) /\ (incident_c T_0 C2)))) => ((part_of C1 C2) \/ (part_of C2 C1)))))) ((incident_c T_1 T_2) /\ (All C1, (All C2, (((part_of C1 T_2) /\ ((part_of C2 T_2) /\ ((incident_c T_1 C1) /\ (incident_c T_1 C2)))) => ((part_of C1 C2) \/ (part_of C2 C1)))))) (All P, ((incident_c P T_2) => (incident_c P T_3))) (T_0 != T_1) ### NotAnd 2 12 % 2.73/2.91 14. (-. (between_c T_3 T_1 T_4 T_0)) (T_0 != T_1) (All P, ((incident_c P T_2) => (incident_c P T_3))) ((incident_c T_1 T_2) /\ (All C1, (All C2, (((part_of C1 T_2) /\ ((part_of C2 T_2) /\ ((incident_c T_1 C1) /\ (incident_c T_1 C2)))) => ((part_of C1 C2) \/ (part_of C2 C1)))))) ((incident_c T_0 T_2) /\ (All C1, (All C2, (((part_of C1 T_2) /\ ((part_of C2 T_2) /\ ((incident_c T_0 C1) /\ (incident_c T_0 C2)))) => ((part_of C1 C2) \/ (part_of C2 C1)))))) ((incident_c T_4 T_2) /\ (-. (end_point T_4 T_2))) ### Definition-Pseudo(between_c) 13 % 2.73/2.91 15. (inner_point T_4 T_2) ((incident_c T_0 T_2) /\ (All C1, (All C2, (((part_of C1 T_2) /\ ((part_of C2 T_2) /\ ((incident_c T_0 C1) /\ (incident_c T_0 C2)))) => ((part_of C1 C2) \/ (part_of C2 C1)))))) ((incident_c T_1 T_2) /\ (All C1, (All C2, (((part_of C1 T_2) /\ ((part_of C2 T_2) /\ ((incident_c T_1 C1) /\ (incident_c T_1 C2)))) => ((part_of C1 C2) \/ (part_of C2 C1)))))) (All P, ((incident_c P T_2) => (incident_c P T_3))) (T_0 != T_1) (-. (between_c T_3 T_1 T_4 T_0)) ### Definition-Pseudo(inner_point) 14 % 2.73/2.91 16. (end_point T_1 T_2) (-. (between_c T_3 T_1 T_4 T_0)) (T_0 != T_1) (All P, ((incident_c P T_2) => (incident_c P T_3))) ((incident_c T_0 T_2) /\ (All C1, (All C2, (((part_of C1 T_2) /\ ((part_of C2 T_2) /\ ((incident_c T_0 C1) /\ (incident_c T_0 C2)))) => ((part_of C1 C2) \/ (part_of C2 C1)))))) (inner_point T_4 T_2) ### Definition-Pseudo(end_point) 15 % 2.73/2.91 17. (end_point T_0 T_2) (inner_point T_4 T_2) (All P, ((incident_c P T_2) => (incident_c P T_3))) (T_0 != T_1) (-. (between_c T_3 T_1 T_4 T_0)) (end_point T_1 T_2) ### Definition-Pseudo(end_point) 16 % 2.73/2.91 18. (part_of T_2 T_3) (end_point T_1 T_2) (-. (between_c T_3 T_1 T_4 T_0)) (T_0 != T_1) (inner_point T_4 T_2) (end_point T_0 T_2) ### Definition-Pseudo(part_of) 17 % 2.73/2.91 19. ((part_of T_2 T_3) /\ ((end_point T_0 T_2) /\ ((end_point T_1 T_2) /\ (inner_point T_4 T_2)))) (T_0 != T_1) (-. (between_c T_3 T_1 T_4 T_0)) ### ConjTree 18 % 2.73/2.91 20. (Ex Cpp, ((part_of Cpp T_3) /\ ((end_point T_0 Cpp) /\ ((end_point T_1 Cpp) /\ (inner_point T_4 Cpp))))) (-. (between_c T_3 T_1 T_4 T_0)) (T_0 != T_1) ### Exists 19 % 2.73/2.91 21. ((T_0 != T_1) /\ (Ex Cpp, ((part_of Cpp T_3) /\ ((end_point T_0 Cpp) /\ ((end_point T_1 Cpp) /\ (inner_point T_4 Cpp)))))) (-. (between_c T_3 T_1 T_4 T_0)) ### And 20 % 2.73/2.91 22. (between_c T_3 T_0 T_4 T_1) (-. (between_c T_3 T_1 T_4 T_0)) ### Definition-Pseudo(between_c) 21 % 2.73/2.91 23. (-. ((between_c T_3 T_0 T_4 T_1) => (between_c T_3 T_1 T_4 T_0))) ### NotImply 22 % 2.73/2.91 24. (-. (All R, ((between_c T_3 T_0 T_4 R) => (between_c T_3 R T_4 T_0)))) ### NotAllEx 23 % 2.73/2.91 25. (-. (All Q, (All R, ((between_c T_3 T_0 Q R) => (between_c T_3 R Q T_0))))) ### NotAllEx 24 % 2.73/2.91 26. (-. (All P, (All Q, (All R, ((between_c T_3 P Q R) => (between_c T_3 R Q P)))))) ### NotAllEx 25 % 2.73/2.91 27. (-. (All C, (All P, (All Q, (All R, ((between_c C P Q R) => (between_c C R Q P))))))) ### NotAllEx 26 % 2.73/2.91 % SZS output end Proof % 2.73/2.91 (* END-PROOF *) %------------------------------------------------------------------------------