%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : GEO220+3 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n009.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:31:17 EDT 2022 % Result : Theorem 7.96s 8.16s % Output : Proof 7.96s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : GEO220+3 : TPTP v8.1.0. Released v4.0.0. % 0.04/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.13/0.33 % Computer : n009.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % 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 19:55:37 EDT 2022 % 0.13/0.34 % CPUTime : % 7.96/8.16 % SZS status Theorem % 7.96/8.16 (* PROOF-FOUND *) % 7.96/8.16 (* BEGIN-PROOF *) % 7.96/8.16 % SZS output start Proof % 7.96/8.16 1. (-. (unorthogonal_lines T_0 T_1)) (unorthogonal_lines T_0 T_1) ### Axiom % 7.96/8.16 2. (-. (unorthogonal_lines T_0 T_2)) (unorthogonal_lines T_0 T_2) ### Axiom % 7.96/8.16 3. (convergent_lines T_1 T_2) (-. (convergent_lines T_1 T_2)) ### Axiom % 7.96/8.16 4. (((-. (unorthogonal_lines T_0 T_1)) /\ (-. (unorthogonal_lines T_0 T_2))) => (-. (convergent_lines T_1 T_2))) (convergent_lines T_1 T_2) (-. (unorthogonal_lines T_0 T_2)) (-. (unorthogonal_lines T_0 T_1)) ### DisjTree 1 2 3 % 7.96/8.16 5. (All N, (((-. (unorthogonal_lines T_0 T_1)) /\ (-. (unorthogonal_lines T_0 N))) => (-. (convergent_lines T_1 N)))) (-. (unorthogonal_lines T_0 T_1)) (-. (unorthogonal_lines T_0 T_2)) (convergent_lines T_1 T_2) ### All 4 % 7.96/8.16 6. (All M, (All N, (((-. (unorthogonal_lines T_0 M)) /\ (-. (unorthogonal_lines T_0 N))) => (-. (convergent_lines M N))))) (convergent_lines T_1 T_2) (-. (unorthogonal_lines T_0 T_2)) (-. (unorthogonal_lines T_0 T_1)) ### All 5 % 7.96/8.16 7. (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (-. (unorthogonal_lines T_0 T_1)) (-. (unorthogonal_lines T_0 T_2)) (convergent_lines T_1 T_2) ### All 6 % 7.96/8.16 8. (-. (-. (convergent_lines T_1 T_2))) (-. (unorthogonal_lines T_0 T_2)) (-. (unorthogonal_lines T_0 T_1)) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) ### NotNot 7 % 7.96/8.16 9. (-. (parallel_lines T_1 T_2)) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (-. (unorthogonal_lines T_0 T_1)) (-. (unorthogonal_lines T_0 T_2)) ### Definition-Pseudo(parallel_lines) 8 % 7.96/8.16 10. (orthogonal_lines T_0 T_2) (-. (unorthogonal_lines T_0 T_1)) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (-. (parallel_lines T_1 T_2)) ### Definition-Pseudo(orthogonal_lines) 9 % 7.96/8.16 11. (orthogonal_lines T_0 T_1) (-. (parallel_lines T_1 T_2)) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) (orthogonal_lines T_0 T_2) ### Definition-Pseudo(orthogonal_lines) 10 % 7.96/8.16 12. (-. (((orthogonal_lines T_0 T_1) /\ (orthogonal_lines T_0 T_2)) => (parallel_lines T_1 T_2))) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) ### ConjTree 11 % 7.96/8.16 13. (-. (All N, (((orthogonal_lines T_0 T_1) /\ (orthogonal_lines T_0 N)) => (parallel_lines T_1 N)))) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) ### NotAllEx 12 % 7.96/8.16 14. (-. (All M, (All N, (((orthogonal_lines T_0 M) /\ (orthogonal_lines T_0 N)) => (parallel_lines M N))))) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) ### NotAllEx 13 % 7.96/8.16 15. (-. (All L, (All M, (All N, (((orthogonal_lines L M) /\ (orthogonal_lines L N)) => (parallel_lines M N)))))) (All L, (All M, (All N, (((-. (unorthogonal_lines L M)) /\ (-. (unorthogonal_lines L N))) => (-. (convergent_lines M N)))))) ### NotAllEx 14 % 7.96/8.16 % SZS output end Proof % 7.96/8.16 (* END-PROOF *) %------------------------------------------------------------------------------