%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : GEO082+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 : 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 : Sat Jul 16 06:29:56 EDT 2022 % Result : Theorem 3.22s 3.42s % Output : Proof 3.22s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.02/0.06 % Problem : GEO082+1 : TPTP v8.1.0. Released v2.4.0. % 0.02/0.07 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.06/0.25 % Computer : n003.cluster.edu % 0.06/0.25 % Model : x86_64 x86_64 % 0.06/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.25 % Memory : 8042.1875MB % 0.06/0.25 % OS : Linux 3.10.0-693.el7.x86_64 % 0.06/0.25 % CPULimit : 300 % 0.06/0.25 % WCLimit : 600 % 0.06/0.25 % DateTime : Fri Jun 17 21:27:27 EDT 2022 % 0.06/0.25 % CPUTime : % 3.22/3.42 % SZS status Theorem % 3.22/3.42 (* PROOF-FOUND *) % 3.22/3.42 (* BEGIN-PROOF *) % 3.22/3.42 % SZS output start Proof % 3.22/3.42 1. (incident_c T_0 T_1) (-. (incident_c T_0 T_1)) ### Axiom % 3.22/3.42 2. (-. (incident_c T_0 T_2)) (incident_c T_0 T_2) ### Axiom % 3.22/3.42 3. ((incident_c T_0 T_1) => (incident_c T_0 T_2)) (-. (incident_c T_0 T_2)) (incident_c T_0 T_1) ### Imply 1 2 % 3.22/3.42 4. (All P, ((incident_c P T_1) => (incident_c P T_2))) (incident_c T_0 T_1) (-. (incident_c T_0 T_2)) ### All 3 % 3.22/3.42 5. (incident_c T_0 T_2) (-. (incident_c T_0 T_2)) ### Axiom % 3.22/3.42 6. (-. (incident_c T_0 T_1)) (incident_c T_0 T_1) ### Axiom % 3.22/3.42 7. ((incident_c T_0 T_2) => (incident_c T_0 T_1)) (-. (incident_c T_0 T_1)) (incident_c T_0 T_2) ### Imply 5 6 % 3.22/3.42 8. (All P, ((incident_c P T_2) => (incident_c P T_1))) (incident_c T_0 T_2) (-. (incident_c T_0 T_1)) ### All 7 % 3.22/3.42 9. (-. ((incident_c T_0 T_2) <=> (incident_c T_0 T_1))) (All P, ((incident_c P T_2) => (incident_c P T_1))) (All P, ((incident_c P T_1) => (incident_c P T_2))) ### NotEquiv 4 8 % 3.22/3.42 10. (-. (All P, ((incident_c P T_2) <=> (incident_c P T_1)))) (All P, ((incident_c P T_1) => (incident_c P T_2))) (All P, ((incident_c P T_2) => (incident_c P T_1))) ### NotAllEx 9 % 3.22/3.42 11. (T_2 != T_1) (T_2 = T_1) ### Axiom % 3.22/3.42 12. ((All P, ((incident_c P T_2) <=> (incident_c P T_1))) => (T_2 = T_1)) (T_2 != T_1) (All P, ((incident_c P T_2) => (incident_c P T_1))) (All P, ((incident_c P T_1) => (incident_c P T_2))) ### Imply 10 11 % 3.22/3.42 13. (All C1, ((All P, ((incident_c P T_2) <=> (incident_c P C1))) => (T_2 = C1))) (All P, ((incident_c P T_1) => (incident_c P T_2))) (All P, ((incident_c P T_2) => (incident_c P T_1))) (T_2 != T_1) ### All 12 % 3.22/3.42 14. (All C, (All C1, ((All P, ((incident_c P C) <=> (incident_c P C1))) => (C = C1)))) (T_2 != T_1) (All P, ((incident_c P T_2) => (incident_c P T_1))) (All P, ((incident_c P T_1) => (incident_c P T_2))) ### All 13 % 3.22/3.42 15. (part_of T_1 T_2) (All P, ((incident_c P T_2) => (incident_c P T_1))) (T_2 != T_1) (All C, (All C1, ((All P, ((incident_c P C) <=> (incident_c P C1))) => (C = C1)))) ### Definition-Pseudo(part_of) 14 % 3.22/3.42 16. (part_of T_2 T_1) (All C, (All C1, ((All P, ((incident_c P C) <=> (incident_c P C1))) => (C = C1)))) (T_2 != T_1) (part_of T_1 T_2) ### Definition-Pseudo(part_of) 15 % 3.22/3.42 17. (-. (((part_of T_2 T_1) /\ (part_of T_1 T_2)) => (T_2 = T_1))) (All C, (All C1, ((All P, ((incident_c P C) <=> (incident_c P C1))) => (C = C1)))) ### ConjTree 16 % 3.22/3.42 18. (-. (All C2, (((part_of T_2 C2) /\ (part_of C2 T_2)) => (T_2 = C2)))) (All C, (All C1, ((All P, ((incident_c P C) <=> (incident_c P C1))) => (C = C1)))) ### NotAllEx 17 % 3.22/3.42 19. (-. (All C1, (All C2, (((part_of C1 C2) /\ (part_of C2 C1)) => (C1 = C2))))) (All C, (All C1, ((All P, ((incident_c P C) <=> (incident_c P C1))) => (C = C1)))) ### NotAllEx 18 % 3.22/3.42 % SZS output end Proof % 3.22/3.42 (* END-PROOF *) %------------------------------------------------------------------------------