%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : GEO234+1 : TPTP v8.1.0. Bugfixed v6.4.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n021.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:26 EDT 2022 % Result : Theorem 0.18s 0.51s % Output : Proof 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : GEO234+1 : TPTP v8.1.0. Bugfixed v6.4.0. % 0.00/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n021.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 : Sat Jun 18 06:08:01 EDT 2022 % 0.12/0.34 % CPUTime : % 0.18/0.51 % SZS status Theorem % 0.18/0.51 (* PROOF-FOUND *) % 0.18/0.51 (* BEGIN-PROOF *) % 0.18/0.51 % SZS output start Proof % 0.18/0.51 1. (unequally_directed_lines T_0 (reverse_line T_1)) (-. (unequally_directed_lines T_0 (reverse_line T_1))) ### Axiom % 0.18/0.51 2. (unequally_directed_lines T_0 T_1) (-. (unequally_directed_lines T_0 T_1)) ### Axiom % 0.18/0.51 3. (unequally_directed_lines T_0 T_0) ### Extension/test/oag5 % 0.18/0.51 4. (unequally_directed_lines T_1 T_0) (-. (unequally_directed_lines T_1 T_0)) ### Axiom % 0.18/0.51 5. (unequally_directed_lines T_1 T_1) ### Extension/test/oag5 % 0.18/0.51 6. (unequally_directed_lines T_1 T_0) (-. (unequally_directed_lines T_1 T_0)) ### Axiom % 0.18/0.51 7. (unequally_directed_lines T_0 T_1) (-. (unequally_directed_lines T_0 T_1)) ### Axiom % 0.18/0.51 8. (unequally_directed_lines T_0 (reverse_line T_1)) (-. (unequally_directed_lines T_0 (reverse_line T_1))) ### Axiom % 0.18/0.51 9. ((unequally_directed_lines T_0 T_0) /\ (unequally_directed_lines T_0 (reverse_line T_0))) ### And 3 % 0.18/0.51 10. (-. (unequally_directed_lines T_1 (reverse_line T_0))) (unequally_directed_lines T_1 (reverse_line T_0)) ### Axiom % 0.18/0.51 11. ((unequally_directed_lines T_1 T_0) /\ (unequally_directed_lines T_1 (reverse_line T_0))) (-. (unequally_directed_lines T_1 (reverse_line T_0))) ### And 10 % 0.18/0.51 12. (((unequally_directed_lines T_0 T_1) /\ (unequally_directed_lines T_0 (reverse_line T_1))) => (((unequally_directed_lines T_0 T_0) /\ (unequally_directed_lines T_0 (reverse_line T_0))) \/ ((unequally_directed_lines T_1 T_0) /\ (unequally_directed_lines T_1 (reverse_line T_0))))) (-. (unequally_directed_lines T_1 (reverse_line T_0))) (unequally_directed_lines T_0 (reverse_line T_1)) (unequally_directed_lines T_0 T_1) ### DisjTree 7 8 9 11 % 0.18/0.51 13. (All N, (((unequally_directed_lines T_0 T_1) /\ (unequally_directed_lines T_0 (reverse_line T_1))) => (((unequally_directed_lines T_0 N) /\ (unequally_directed_lines T_0 (reverse_line N))) \/ ((unequally_directed_lines T_1 N) /\ (unequally_directed_lines T_1 (reverse_line N)))))) (unequally_directed_lines T_0 T_1) (unequally_directed_lines T_0 (reverse_line T_1)) (-. (unequally_directed_lines T_1 (reverse_line T_0))) ### All 12 % 0.18/0.51 14. (All M, (All N, (((unequally_directed_lines T_0 M) /\ (unequally_directed_lines T_0 (reverse_line M))) => (((unequally_directed_lines T_0 N) /\ (unequally_directed_lines T_0 (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N))))))) (-. (unequally_directed_lines T_1 (reverse_line T_0))) (unequally_directed_lines T_0 (reverse_line T_1)) (unequally_directed_lines T_0 T_1) ### All 13 % 0.18/0.51 15. (-. (unequally_directed_lines T_1 (reverse_line T_2))) (unequally_directed_lines T_1 (reverse_line T_2)) ### Axiom % 0.18/0.51 16. ((unequally_directed_lines T_1 T_2) /\ (unequally_directed_lines T_1 (reverse_line T_2))) (-. (unequally_directed_lines T_1 (reverse_line T_2))) ### And 15 % 0.18/0.51 17. (-. (unequally_directed_lines T_0 T_2)) (unequally_directed_lines T_0 T_2) ### Axiom % 0.18/0.51 18. ((unequally_directed_lines T_0 T_2) /\ (unequally_directed_lines T_0 (reverse_line T_2))) (-. (unequally_directed_lines T_0 T_2)) ### And 17 % 0.18/0.51 19. (((unequally_directed_lines T_1 T_0) /\ (unequally_directed_lines T_1 (reverse_line T_0))) => (((unequally_directed_lines T_1 T_2) /\ (unequally_directed_lines T_1 (reverse_line T_2))) \/ ((unequally_directed_lines T_0 T_2) /\ (unequally_directed_lines T_0 (reverse_line T_2))))) (-. (unequally_directed_lines T_0 T_2)) (-. (unequally_directed_lines T_1 (reverse_line T_2))) (unequally_directed_lines T_0 T_1) (unequally_directed_lines T_0 (reverse_line T_1)) (All M, (All N, (((unequally_directed_lines T_0 M) /\ (unequally_directed_lines T_0 (reverse_line M))) => (((unequally_directed_lines T_0 N) /\ (unequally_directed_lines T_0 (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N))))))) (unequally_directed_lines T_1 T_0) ### DisjTree 6 14 16 18 % 0.18/0.51 20. (All N, (((unequally_directed_lines T_1 T_0) /\ (unequally_directed_lines T_1 (reverse_line T_0))) => (((unequally_directed_lines T_1 N) /\ (unequally_directed_lines T_1 (reverse_line N))) \/ ((unequally_directed_lines T_0 N) /\ (unequally_directed_lines T_0 (reverse_line N)))))) (unequally_directed_lines T_1 T_0) (All M, (All N, (((unequally_directed_lines T_0 M) /\ (unequally_directed_lines T_0 (reverse_line M))) => (((unequally_directed_lines T_0 N) /\ (unequally_directed_lines T_0 (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N))))))) (unequally_directed_lines T_0 (reverse_line T_1)) (unequally_directed_lines T_0 T_1) (-. (unequally_directed_lines T_1 (reverse_line T_2))) (-. (unequally_directed_lines T_0 T_2)) ### All 19 % 0.18/0.51 21. (All L, (All M, (All N, (((unequally_directed_lines L M) /\ (unequally_directed_lines L (reverse_line M))) => (((unequally_directed_lines L N) /\ (unequally_directed_lines L (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N)))))))) (-. (unequally_directed_lines T_0 T_2)) (-. (unequally_directed_lines T_1 (reverse_line T_2))) (unequally_directed_lines T_0 T_1) (unequally_directed_lines T_0 (reverse_line T_1)) (unequally_directed_lines T_1 T_0) (All N, (((unequally_directed_lines T_1 T_0) /\ (unequally_directed_lines T_1 (reverse_line T_0))) => (((unequally_directed_lines T_1 N) /\ (unequally_directed_lines T_1 (reverse_line N))) \/ ((unequally_directed_lines T_0 N) /\ (unequally_directed_lines T_0 (reverse_line N)))))) ### All 20 % 0.18/0.51 22. (All M, (All N, (((unequally_directed_lines T_1 M) /\ (unequally_directed_lines T_1 (reverse_line M))) => (((unequally_directed_lines T_1 N) /\ (unequally_directed_lines T_1 (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N))))))) (unequally_directed_lines T_1 T_0) (unequally_directed_lines T_0 (reverse_line T_1)) (unequally_directed_lines T_0 T_1) (-. (unequally_directed_lines T_1 (reverse_line T_2))) (-. (unequally_directed_lines T_0 T_2)) (All L, (All M, (All N, (((unequally_directed_lines L M) /\ (unequally_directed_lines L (reverse_line M))) => (((unequally_directed_lines L N) /\ (unequally_directed_lines L (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N)))))))) ### All 21 % 0.18/0.51 23. ((unequally_directed_lines T_1 T_0) => ((unequally_directed_lines T_1 T_1) \/ (unequally_directed_lines T_0 T_1))) (All L, (All M, (All N, (((unequally_directed_lines L M) /\ (unequally_directed_lines L (reverse_line M))) => (((unequally_directed_lines L N) /\ (unequally_directed_lines L (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N)))))))) (-. (unequally_directed_lines T_0 T_2)) (-. (unequally_directed_lines T_1 (reverse_line T_2))) (unequally_directed_lines T_0 (reverse_line T_1)) (All M, (All N, (((unequally_directed_lines T_1 M) /\ (unequally_directed_lines T_1 (reverse_line M))) => (((unequally_directed_lines T_1 N) /\ (unequally_directed_lines T_1 (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N))))))) (unequally_directed_lines T_1 T_0) ### DisjTree 4 5 22 % 0.18/0.51 24. (All N, ((unequally_directed_lines T_1 T_0) => ((unequally_directed_lines T_1 N) \/ (unequally_directed_lines T_0 N)))) (unequally_directed_lines T_1 T_0) (All M, (All N, (((unequally_directed_lines T_1 M) /\ (unequally_directed_lines T_1 (reverse_line M))) => (((unequally_directed_lines T_1 N) /\ (unequally_directed_lines T_1 (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N))))))) (unequally_directed_lines T_0 (reverse_line T_1)) (-. (unequally_directed_lines T_1 (reverse_line T_2))) (-. (unequally_directed_lines T_0 T_2)) (All L, (All M, (All N, (((unequally_directed_lines L M) /\ (unequally_directed_lines L (reverse_line M))) => (((unequally_directed_lines L N) /\ (unequally_directed_lines L (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N)))))))) ### All 23 % 0.18/0.51 25. (All M, (All N, ((unequally_directed_lines T_1 M) => ((unequally_directed_lines T_1 N) \/ (unequally_directed_lines M N))))) (All L, (All M, (All N, (((unequally_directed_lines L M) /\ (unequally_directed_lines L (reverse_line M))) => (((unequally_directed_lines L N) /\ (unequally_directed_lines L (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N)))))))) (-. (unequally_directed_lines T_0 T_2)) (-. (unequally_directed_lines T_1 (reverse_line T_2))) (unequally_directed_lines T_0 (reverse_line T_1)) (All M, (All N, (((unequally_directed_lines T_1 M) /\ (unequally_directed_lines T_1 (reverse_line M))) => (((unequally_directed_lines T_1 N) /\ (unequally_directed_lines T_1 (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N))))))) (unequally_directed_lines T_1 T_0) ### All 24 % 0.18/0.52 26. (All L, (All M, (All N, ((unequally_directed_lines L M) => ((unequally_directed_lines L N) \/ (unequally_directed_lines M N)))))) (unequally_directed_lines T_1 T_0) (All M, (All N, (((unequally_directed_lines T_1 M) /\ (unequally_directed_lines T_1 (reverse_line M))) => (((unequally_directed_lines T_1 N) /\ (unequally_directed_lines T_1 (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N))))))) (unequally_directed_lines T_0 (reverse_line T_1)) (-. (unequally_directed_lines T_1 (reverse_line T_2))) (-. (unequally_directed_lines T_0 T_2)) (All L, (All M, (All N, (((unequally_directed_lines L M) /\ (unequally_directed_lines L (reverse_line M))) => (((unequally_directed_lines L N) /\ (unequally_directed_lines L (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N)))))))) ### All 25 % 0.18/0.52 27. (All L, (All M, (All N, (((unequally_directed_lines L M) /\ (unequally_directed_lines L (reverse_line M))) => (((unequally_directed_lines L N) /\ (unequally_directed_lines L (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N)))))))) (-. (unequally_directed_lines T_0 T_2)) (-. (unequally_directed_lines T_1 (reverse_line T_2))) (unequally_directed_lines T_0 (reverse_line T_1)) (unequally_directed_lines T_1 T_0) (All L, (All M, (All N, ((unequally_directed_lines L M) => ((unequally_directed_lines L N) \/ (unequally_directed_lines M N)))))) ### All 26 % 0.18/0.52 28. ((unequally_directed_lines T_0 T_1) => ((unequally_directed_lines T_0 T_0) \/ (unequally_directed_lines T_1 T_0))) (All L, (All M, (All N, ((unequally_directed_lines L M) => ((unequally_directed_lines L N) \/ (unequally_directed_lines M N)))))) (unequally_directed_lines T_0 (reverse_line T_1)) (-. (unequally_directed_lines T_1 (reverse_line T_2))) (-. (unequally_directed_lines T_0 T_2)) (All L, (All M, (All N, (((unequally_directed_lines L M) /\ (unequally_directed_lines L (reverse_line M))) => (((unequally_directed_lines L N) /\ (unequally_directed_lines L (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N)))))))) (unequally_directed_lines T_0 T_1) ### DisjTree 2 3 27 % 0.18/0.52 29. (All N, ((unequally_directed_lines T_0 T_1) => ((unequally_directed_lines T_0 N) \/ (unequally_directed_lines T_1 N)))) (unequally_directed_lines T_0 T_1) (All L, (All M, (All N, (((unequally_directed_lines L M) /\ (unequally_directed_lines L (reverse_line M))) => (((unequally_directed_lines L N) /\ (unequally_directed_lines L (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N)))))))) (-. (unequally_directed_lines T_0 T_2)) (-. (unequally_directed_lines T_1 (reverse_line T_2))) (unequally_directed_lines T_0 (reverse_line T_1)) (All L, (All M, (All N, ((unequally_directed_lines L M) => ((unequally_directed_lines L N) \/ (unequally_directed_lines M N)))))) ### All 28 % 0.18/0.52 30. (All M, (All N, ((unequally_directed_lines T_0 M) => ((unequally_directed_lines T_0 N) \/ (unequally_directed_lines M N))))) (All L, (All M, (All N, ((unequally_directed_lines L M) => ((unequally_directed_lines L N) \/ (unequally_directed_lines M N)))))) (unequally_directed_lines T_0 (reverse_line T_1)) (-. (unequally_directed_lines T_1 (reverse_line T_2))) (-. (unequally_directed_lines T_0 T_2)) (All L, (All M, (All N, (((unequally_directed_lines L M) /\ (unequally_directed_lines L (reverse_line M))) => (((unequally_directed_lines L N) /\ (unequally_directed_lines L (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N)))))))) (unequally_directed_lines T_0 T_1) ### All 29 % 0.18/0.52 31. (unequally_directed_lines (reverse_line T_1) T_1) (-. (unequally_directed_lines (reverse_line T_1) T_1)) ### Axiom % 0.18/0.52 32. (unequally_directed_lines (reverse_line T_1) (reverse_line T_1)) ### Extension/test/oag5 % 0.18/0.52 33. (unequally_directed_lines T_0 (reverse_line T_1)) (-. (unequally_directed_lines T_0 (reverse_line T_1))) ### Axiom % 0.18/0.52 34. (-. (unequally_directed_lines T_0 T_2)) (unequally_directed_lines T_0 T_2) ### Axiom % 0.18/0.52 35. (unequally_directed_lines T_1 (reverse_line T_1)) (-. (unequally_directed_lines T_1 (reverse_line T_1))) ### Axiom % 0.18/0.52 36. (-. (unequally_directed_lines T_1 (reverse_line T_2))) (unequally_directed_lines T_1 (reverse_line T_2)) ### Axiom % 0.18/0.52 37. (unequally_directed_lines (reverse_line T_1) T_2) (-. (unequally_directed_lines (reverse_line T_1) T_2)) ### Axiom % 0.18/0.52 38. (unequally_directed_lines (reverse_line T_1) (reverse_line T_2)) (-. (unequally_directed_lines (reverse_line T_1) (reverse_line T_2))) ### Axiom % 0.18/0.52 39. ((unequally_directed_lines (reverse_line T_1) T_1) /\ (unequally_directed_lines (reverse_line T_1) (reverse_line T_1))) ### And 32 % 0.18/0.52 40. (-. (unequally_directed_lines T_2 T_1)) (unequally_directed_lines T_2 T_1) ### Axiom % 0.18/0.52 41. ((unequally_directed_lines T_2 T_1) /\ (unequally_directed_lines T_2 (reverse_line T_1))) (-. (unequally_directed_lines T_2 T_1)) ### And 40 % 0.18/0.52 42. (((unequally_directed_lines (reverse_line T_1) T_2) /\ (unequally_directed_lines (reverse_line T_1) (reverse_line T_2))) => (((unequally_directed_lines (reverse_line T_1) T_1) /\ (unequally_directed_lines (reverse_line T_1) (reverse_line T_1))) \/ ((unequally_directed_lines T_2 T_1) /\ (unequally_directed_lines T_2 (reverse_line T_1))))) (-. (unequally_directed_lines T_2 T_1)) (unequally_directed_lines (reverse_line T_1) (reverse_line T_2)) (unequally_directed_lines (reverse_line T_1) T_2) ### DisjTree 37 38 39 41 % 0.18/0.52 43. (All N, (((unequally_directed_lines (reverse_line T_1) T_2) /\ (unequally_directed_lines (reverse_line T_1) (reverse_line T_2))) => (((unequally_directed_lines (reverse_line T_1) N) /\ (unequally_directed_lines (reverse_line T_1) (reverse_line N))) \/ ((unequally_directed_lines T_2 N) /\ (unequally_directed_lines T_2 (reverse_line N)))))) (unequally_directed_lines (reverse_line T_1) T_2) (unequally_directed_lines (reverse_line T_1) (reverse_line T_2)) (-. (unequally_directed_lines T_2 T_1)) ### All 42 % 0.18/0.52 44. (All M, (All N, (((unequally_directed_lines (reverse_line T_1) M) /\ (unequally_directed_lines (reverse_line T_1) (reverse_line M))) => (((unequally_directed_lines (reverse_line T_1) N) /\ (unequally_directed_lines (reverse_line T_1) (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N))))))) (-. (unequally_directed_lines T_2 T_1)) (unequally_directed_lines (reverse_line T_1) (reverse_line T_2)) (unequally_directed_lines (reverse_line T_1) T_2) ### All 43 % 0.18/0.52 45. (All L, (All M, (All N, (((unequally_directed_lines L M) /\ (unequally_directed_lines L (reverse_line M))) => (((unequally_directed_lines L N) /\ (unequally_directed_lines L (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N)))))))) (unequally_directed_lines (reverse_line T_1) T_2) (unequally_directed_lines (reverse_line T_1) (reverse_line T_2)) (-. (unequally_directed_lines T_2 T_1)) ### All 44 % 0.18/0.52 46. (-. (unequally_directed_lines T_2 T_0)) (unequally_directed_lines T_2 T_0) ### Axiom % 0.18/0.52 47. (unequally_directed_lines T_1 T_0) (unequally_directed_lines T_0 (reverse_line T_1)) (-. (unequally_directed_lines T_1 (reverse_line T_2))) (-. (unequally_directed_lines T_0 T_2)) (All L, (All M, (All N, (((unequally_directed_lines L M) /\ (unequally_directed_lines L (reverse_line M))) => (((unequally_directed_lines L N) /\ (unequally_directed_lines L (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N)))))))) (All M, (All N, ((unequally_directed_lines T_1 M) => ((unequally_directed_lines T_1 N) \/ (unequally_directed_lines M N))))) ### All 25 % 0.18/0.52 48. ((unequally_directed_lines T_2 T_1) => ((unequally_directed_lines T_2 T_0) \/ (unequally_directed_lines T_1 T_0))) (All M, (All N, ((unequally_directed_lines T_1 M) => ((unequally_directed_lines T_1 N) \/ (unequally_directed_lines M N))))) (-. (unequally_directed_lines T_0 T_2)) (-. (unequally_directed_lines T_1 (reverse_line T_2))) (unequally_directed_lines T_0 (reverse_line T_1)) (-. (unequally_directed_lines T_2 T_0)) (unequally_directed_lines (reverse_line T_1) (reverse_line T_2)) (unequally_directed_lines (reverse_line T_1) T_2) (All L, (All M, (All N, (((unequally_directed_lines L M) /\ (unequally_directed_lines L (reverse_line M))) => (((unequally_directed_lines L N) /\ (unequally_directed_lines L (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N)))))))) ### DisjTree 45 46 47 % 0.18/0.52 49. (All N, ((unequally_directed_lines T_2 T_1) => ((unequally_directed_lines T_2 N) \/ (unequally_directed_lines T_1 N)))) (All L, (All M, (All N, (((unequally_directed_lines L M) /\ (unequally_directed_lines L (reverse_line M))) => (((unequally_directed_lines L N) /\ (unequally_directed_lines L (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N)))))))) (unequally_directed_lines (reverse_line T_1) T_2) (unequally_directed_lines (reverse_line T_1) (reverse_line T_2)) (-. (unequally_directed_lines T_2 T_0)) (unequally_directed_lines T_0 (reverse_line T_1)) (-. (unequally_directed_lines T_1 (reverse_line T_2))) (-. (unequally_directed_lines T_0 T_2)) (All M, (All N, ((unequally_directed_lines T_1 M) => ((unequally_directed_lines T_1 N) \/ (unequally_directed_lines M N))))) ### All 48 % 0.18/0.52 50. (unequally_directed_lines T_2 T_2) ### Extension/test/oag5 % 0.18/0.52 51. (-. (unequally_directed_lines T_0 T_2)) (unequally_directed_lines T_0 T_2) ### Axiom % 0.18/0.52 52. ((unequally_directed_lines T_2 T_0) => ((unequally_directed_lines T_2 T_2) \/ (unequally_directed_lines T_0 T_2))) (All M, (All N, ((unequally_directed_lines T_1 M) => ((unequally_directed_lines T_1 N) \/ (unequally_directed_lines M N))))) (-. (unequally_directed_lines T_0 T_2)) (-. (unequally_directed_lines T_1 (reverse_line T_2))) (unequally_directed_lines T_0 (reverse_line T_1)) (unequally_directed_lines (reverse_line T_1) (reverse_line T_2)) (unequally_directed_lines (reverse_line T_1) T_2) (All L, (All M, (All N, (((unequally_directed_lines L M) /\ (unequally_directed_lines L (reverse_line M))) => (((unequally_directed_lines L N) /\ (unequally_directed_lines L (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N)))))))) (All N, ((unequally_directed_lines T_2 T_1) => ((unequally_directed_lines T_2 N) \/ (unequally_directed_lines T_1 N)))) ### DisjTree 49 50 51 % 0.18/0.52 53. (All N, ((unequally_directed_lines T_2 T_0) => ((unequally_directed_lines T_2 N) \/ (unequally_directed_lines T_0 N)))) (All N, ((unequally_directed_lines T_2 T_1) => ((unequally_directed_lines T_2 N) \/ (unequally_directed_lines T_1 N)))) (All L, (All M, (All N, (((unequally_directed_lines L M) /\ (unequally_directed_lines L (reverse_line M))) => (((unequally_directed_lines L N) /\ (unequally_directed_lines L (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N)))))))) (unequally_directed_lines (reverse_line T_1) T_2) (unequally_directed_lines (reverse_line T_1) (reverse_line T_2)) (unequally_directed_lines T_0 (reverse_line T_1)) (-. (unequally_directed_lines T_1 (reverse_line T_2))) (-. (unequally_directed_lines T_0 T_2)) (All M, (All N, ((unequally_directed_lines T_1 M) => ((unequally_directed_lines T_1 N) \/ (unequally_directed_lines M N))))) ### All 52 % 0.18/0.52 54. (All M, (All N, ((unequally_directed_lines T_2 M) => ((unequally_directed_lines T_2 N) \/ (unequally_directed_lines M N))))) (All M, (All N, ((unequally_directed_lines T_1 M) => ((unequally_directed_lines T_1 N) \/ (unequally_directed_lines M N))))) (-. (unequally_directed_lines T_0 T_2)) (-. (unequally_directed_lines T_1 (reverse_line T_2))) (unequally_directed_lines T_0 (reverse_line T_1)) (unequally_directed_lines (reverse_line T_1) (reverse_line T_2)) (unequally_directed_lines (reverse_line T_1) T_2) (All L, (All M, (All N, (((unequally_directed_lines L M) /\ (unequally_directed_lines L (reverse_line M))) => (((unequally_directed_lines L N) /\ (unequally_directed_lines L (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N)))))))) (All N, ((unequally_directed_lines T_2 T_0) => ((unequally_directed_lines T_2 N) \/ (unequally_directed_lines T_0 N)))) ### All 53 % 0.18/0.52 55. (All L, (All M, (All N, (((unequally_directed_lines L M) /\ (unequally_directed_lines L (reverse_line M))) => (((unequally_directed_lines L N) /\ (unequally_directed_lines L (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N)))))))) (unequally_directed_lines (reverse_line T_1) T_2) (unequally_directed_lines (reverse_line T_1) (reverse_line T_2)) (unequally_directed_lines T_0 (reverse_line T_1)) (-. (unequally_directed_lines T_1 (reverse_line T_2))) (-. (unequally_directed_lines T_0 T_2)) (All M, (All N, ((unequally_directed_lines T_1 M) => ((unequally_directed_lines T_1 N) \/ (unequally_directed_lines M N))))) (All M, (All N, ((unequally_directed_lines T_2 M) => ((unequally_directed_lines T_2 N) \/ (unequally_directed_lines M N))))) ### All 54 % 0.18/0.52 56. (All L, (All M, (All N, ((unequally_directed_lines L M) => ((unequally_directed_lines L N) \/ (unequally_directed_lines M N)))))) (All M, (All N, ((unequally_directed_lines T_1 M) => ((unequally_directed_lines T_1 N) \/ (unequally_directed_lines M N))))) (-. (unequally_directed_lines T_0 T_2)) (-. (unequally_directed_lines T_1 (reverse_line T_2))) (unequally_directed_lines T_0 (reverse_line T_1)) (unequally_directed_lines (reverse_line T_1) (reverse_line T_2)) (unequally_directed_lines (reverse_line T_1) T_2) (All L, (All M, (All N, (((unequally_directed_lines L M) /\ (unequally_directed_lines L (reverse_line M))) => (((unequally_directed_lines L N) /\ (unequally_directed_lines L (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N)))))))) ### All 55 % 0.18/0.52 57. ((unequally_directed_lines T_1 (reverse_line T_1)) => ((unequally_directed_lines T_1 (reverse_line T_2)) \/ (unequally_directed_lines (reverse_line T_1) (reverse_line T_2)))) (All L, (All M, (All N, (((unequally_directed_lines L M) /\ (unequally_directed_lines L (reverse_line M))) => (((unequally_directed_lines L N) /\ (unequally_directed_lines L (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N)))))))) (unequally_directed_lines (reverse_line T_1) T_2) (unequally_directed_lines T_0 (reverse_line T_1)) (-. (unequally_directed_lines T_0 T_2)) (All M, (All N, ((unequally_directed_lines T_1 M) => ((unequally_directed_lines T_1 N) \/ (unequally_directed_lines M N))))) (All L, (All M, (All N, ((unequally_directed_lines L M) => ((unequally_directed_lines L N) \/ (unequally_directed_lines M N)))))) (-. (unequally_directed_lines T_1 (reverse_line T_2))) (unequally_directed_lines T_1 (reverse_line T_1)) ### DisjTree 35 36 56 % 0.18/0.52 58. (All N, ((unequally_directed_lines T_1 (reverse_line T_1)) => ((unequally_directed_lines T_1 N) \/ (unequally_directed_lines (reverse_line T_1) N)))) (unequally_directed_lines T_1 (reverse_line T_1)) (-. (unequally_directed_lines T_1 (reverse_line T_2))) (All L, (All M, (All N, ((unequally_directed_lines L M) => ((unequally_directed_lines L N) \/ (unequally_directed_lines M N)))))) (All M, (All N, ((unequally_directed_lines T_1 M) => ((unequally_directed_lines T_1 N) \/ (unequally_directed_lines M N))))) (-. (unequally_directed_lines T_0 T_2)) (unequally_directed_lines T_0 (reverse_line T_1)) (unequally_directed_lines (reverse_line T_1) T_2) (All L, (All M, (All N, (((unequally_directed_lines L M) /\ (unequally_directed_lines L (reverse_line M))) => (((unequally_directed_lines L N) /\ (unequally_directed_lines L (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N)))))))) ### All 57 % 0.18/0.53 59. (All L, (All M, (All N, (((unequally_directed_lines L M) /\ (unequally_directed_lines L (reverse_line M))) => (((unequally_directed_lines L N) /\ (unequally_directed_lines L (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N)))))))) (unequally_directed_lines (reverse_line T_1) T_2) (unequally_directed_lines T_0 (reverse_line T_1)) (-. (unequally_directed_lines T_0 T_2)) (All M, (All N, ((unequally_directed_lines T_1 M) => ((unequally_directed_lines T_1 N) \/ (unequally_directed_lines M N))))) (All L, (All M, (All N, ((unequally_directed_lines L M) => ((unequally_directed_lines L N) \/ (unequally_directed_lines M N)))))) (-. (unequally_directed_lines T_1 (reverse_line T_2))) (unequally_directed_lines T_1 (reverse_line T_1)) ### All 58 % 0.18/0.53 60. ((unequally_directed_lines T_0 (reverse_line T_1)) => ((unequally_directed_lines T_0 T_2) \/ (unequally_directed_lines (reverse_line T_1) T_2))) (unequally_directed_lines T_1 (reverse_line T_1)) (-. (unequally_directed_lines T_1 (reverse_line T_2))) (All L, (All M, (All N, ((unequally_directed_lines L M) => ((unequally_directed_lines L N) \/ (unequally_directed_lines M N)))))) (All M, (All N, ((unequally_directed_lines T_1 M) => ((unequally_directed_lines T_1 N) \/ (unequally_directed_lines M N))))) (All L, (All M, (All N, (((unequally_directed_lines L M) /\ (unequally_directed_lines L (reverse_line M))) => (((unequally_directed_lines L N) /\ (unequally_directed_lines L (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N)))))))) (-. (unequally_directed_lines T_0 T_2)) (unequally_directed_lines T_0 (reverse_line T_1)) ### DisjTree 33 34 59 % 0.18/0.53 61. (All N, ((unequally_directed_lines T_0 (reverse_line T_1)) => ((unequally_directed_lines T_0 N) \/ (unequally_directed_lines (reverse_line T_1) N)))) (unequally_directed_lines T_0 (reverse_line T_1)) (-. (unequally_directed_lines T_0 T_2)) (All L, (All M, (All N, (((unequally_directed_lines L M) /\ (unequally_directed_lines L (reverse_line M))) => (((unequally_directed_lines L N) /\ (unequally_directed_lines L (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N)))))))) (All M, (All N, ((unequally_directed_lines T_1 M) => ((unequally_directed_lines T_1 N) \/ (unequally_directed_lines M N))))) (All L, (All M, (All N, ((unequally_directed_lines L M) => ((unequally_directed_lines L N) \/ (unequally_directed_lines M N)))))) (-. (unequally_directed_lines T_1 (reverse_line T_2))) (unequally_directed_lines T_1 (reverse_line T_1)) ### All 60 % 0.18/0.53 62. (All M, (All N, ((unequally_directed_lines T_0 M) => ((unequally_directed_lines T_0 N) \/ (unequally_directed_lines M N))))) (unequally_directed_lines T_1 (reverse_line T_1)) (-. (unequally_directed_lines T_1 (reverse_line T_2))) (All L, (All M, (All N, ((unequally_directed_lines L M) => ((unequally_directed_lines L N) \/ (unequally_directed_lines M N)))))) (All M, (All N, ((unequally_directed_lines T_1 M) => ((unequally_directed_lines T_1 N) \/ (unequally_directed_lines M N))))) (All L, (All M, (All N, (((unequally_directed_lines L M) /\ (unequally_directed_lines L (reverse_line M))) => (((unequally_directed_lines L N) /\ (unequally_directed_lines L (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N)))))))) (-. (unequally_directed_lines T_0 T_2)) (unequally_directed_lines T_0 (reverse_line T_1)) ### All 61 % 0.18/0.53 63. (unequally_directed_lines T_0 (reverse_line T_1)) (-. (unequally_directed_lines T_0 T_2)) (All L, (All M, (All N, (((unequally_directed_lines L M) /\ (unequally_directed_lines L (reverse_line M))) => (((unequally_directed_lines L N) /\ (unequally_directed_lines L (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N)))))))) (All L, (All M, (All N, ((unequally_directed_lines L M) => ((unequally_directed_lines L N) \/ (unequally_directed_lines M N)))))) (-. (unequally_directed_lines T_1 (reverse_line T_2))) (unequally_directed_lines T_1 (reverse_line T_1)) (All M, (All N, ((unequally_directed_lines T_0 M) => ((unequally_directed_lines T_0 N) \/ (unequally_directed_lines M N))))) ### All 62 % 0.18/0.53 64. ((unequally_directed_lines (reverse_line T_1) T_1) => ((unequally_directed_lines (reverse_line T_1) (reverse_line T_1)) \/ (unequally_directed_lines T_1 (reverse_line T_1)))) (All M, (All N, ((unequally_directed_lines T_0 M) => ((unequally_directed_lines T_0 N) \/ (unequally_directed_lines M N))))) (-. (unequally_directed_lines T_1 (reverse_line T_2))) (All L, (All M, (All N, ((unequally_directed_lines L M) => ((unequally_directed_lines L N) \/ (unequally_directed_lines M N)))))) (All L, (All M, (All N, (((unequally_directed_lines L M) /\ (unequally_directed_lines L (reverse_line M))) => (((unequally_directed_lines L N) /\ (unequally_directed_lines L (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N)))))))) (-. (unequally_directed_lines T_0 T_2)) (unequally_directed_lines T_0 (reverse_line T_1)) (unequally_directed_lines (reverse_line T_1) T_1) ### DisjTree 31 32 63 % 0.18/0.53 65. (All N, ((unequally_directed_lines (reverse_line T_1) T_1) => ((unequally_directed_lines (reverse_line T_1) N) \/ (unequally_directed_lines T_1 N)))) (unequally_directed_lines (reverse_line T_1) T_1) (unequally_directed_lines T_0 (reverse_line T_1)) (-. (unequally_directed_lines T_0 T_2)) (All L, (All M, (All N, (((unequally_directed_lines L M) /\ (unequally_directed_lines L (reverse_line M))) => (((unequally_directed_lines L N) /\ (unequally_directed_lines L (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N)))))))) (All L, (All M, (All N, ((unequally_directed_lines L M) => ((unequally_directed_lines L N) \/ (unequally_directed_lines M N)))))) (-. (unequally_directed_lines T_1 (reverse_line T_2))) (All M, (All N, ((unequally_directed_lines T_0 M) => ((unequally_directed_lines T_0 N) \/ (unequally_directed_lines M N))))) ### All 64 % 0.18/0.53 66. (All M, (All N, ((unequally_directed_lines (reverse_line T_1) M) => ((unequally_directed_lines (reverse_line T_1) N) \/ (unequally_directed_lines M N))))) (All M, (All N, ((unequally_directed_lines T_0 M) => ((unequally_directed_lines T_0 N) \/ (unequally_directed_lines M N))))) (-. (unequally_directed_lines T_1 (reverse_line T_2))) (All L, (All M, (All N, ((unequally_directed_lines L M) => ((unequally_directed_lines L N) \/ (unequally_directed_lines M N)))))) (All L, (All M, (All N, (((unequally_directed_lines L M) /\ (unequally_directed_lines L (reverse_line M))) => (((unequally_directed_lines L N) /\ (unequally_directed_lines L (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N)))))))) (-. (unequally_directed_lines T_0 T_2)) (unequally_directed_lines T_0 (reverse_line T_1)) (unequally_directed_lines (reverse_line T_1) T_1) ### All 65 % 0.18/0.53 67. (unequally_directed_lines (reverse_line T_1) T_1) (unequally_directed_lines T_0 (reverse_line T_1)) (-. (unequally_directed_lines T_0 T_2)) (All L, (All M, (All N, (((unequally_directed_lines L M) /\ (unequally_directed_lines L (reverse_line M))) => (((unequally_directed_lines L N) /\ (unequally_directed_lines L (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N)))))))) (All L, (All M, (All N, ((unequally_directed_lines L M) => ((unequally_directed_lines L N) \/ (unequally_directed_lines M N)))))) (-. (unequally_directed_lines T_1 (reverse_line T_2))) (All M, (All N, ((unequally_directed_lines T_0 M) => ((unequally_directed_lines T_0 N) \/ (unequally_directed_lines M N))))) ### All 66 % 0.18/0.53 68. ((unequally_directed_lines T_0 (reverse_line T_1)) => ((unequally_directed_lines T_0 T_1) \/ (unequally_directed_lines (reverse_line T_1) T_1))) (All L, (All M, (All N, (((unequally_directed_lines L M) /\ (unequally_directed_lines L (reverse_line M))) => (((unequally_directed_lines L N) /\ (unequally_directed_lines L (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N)))))))) (-. (unequally_directed_lines T_0 T_2)) (-. (unequally_directed_lines T_1 (reverse_line T_2))) (All L, (All M, (All N, ((unequally_directed_lines L M) => ((unequally_directed_lines L N) \/ (unequally_directed_lines M N)))))) (All M, (All N, ((unequally_directed_lines T_0 M) => ((unequally_directed_lines T_0 N) \/ (unequally_directed_lines M N))))) (unequally_directed_lines T_0 (reverse_line T_1)) ### DisjTree 1 30 67 % 0.18/0.53 69. (All N, ((unequally_directed_lines T_0 (reverse_line T_1)) => ((unequally_directed_lines T_0 N) \/ (unequally_directed_lines (reverse_line T_1) N)))) (unequally_directed_lines T_0 (reverse_line T_1)) (All M, (All N, ((unequally_directed_lines T_0 M) => ((unequally_directed_lines T_0 N) \/ (unequally_directed_lines M N))))) (All L, (All M, (All N, ((unequally_directed_lines L M) => ((unequally_directed_lines L N) \/ (unequally_directed_lines M N)))))) (-. (unequally_directed_lines T_1 (reverse_line T_2))) (-. (unequally_directed_lines T_0 T_2)) (All L, (All M, (All N, (((unequally_directed_lines L M) /\ (unequally_directed_lines L (reverse_line M))) => (((unequally_directed_lines L N) /\ (unequally_directed_lines L (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N)))))))) ### All 68 % 0.18/0.53 70. (All L, (All M, (All N, (((unequally_directed_lines L M) /\ (unequally_directed_lines L (reverse_line M))) => (((unequally_directed_lines L N) /\ (unequally_directed_lines L (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N)))))))) (-. (unequally_directed_lines T_0 T_2)) (-. (unequally_directed_lines T_1 (reverse_line T_2))) (All L, (All M, (All N, ((unequally_directed_lines L M) => ((unequally_directed_lines L N) \/ (unequally_directed_lines M N)))))) (All M, (All N, ((unequally_directed_lines T_0 M) => ((unequally_directed_lines T_0 N) \/ (unequally_directed_lines M N))))) (unequally_directed_lines T_0 (reverse_line T_1)) ### All 69 % 0.18/0.53 71. (unequally_directed_lines T_0 (reverse_line T_1)) (All L, (All M, (All N, ((unequally_directed_lines L M) => ((unequally_directed_lines L N) \/ (unequally_directed_lines M N)))))) (-. (unequally_directed_lines T_1 (reverse_line T_2))) (-. (unequally_directed_lines T_0 T_2)) (All L, (All M, (All N, (((unequally_directed_lines L M) /\ (unequally_directed_lines L (reverse_line M))) => (((unequally_directed_lines L N) /\ (unequally_directed_lines L (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N)))))))) ### All 70 % 0.18/0.53 72. (-. ((unequally_directed_lines T_0 (reverse_line T_1)) => ((unequally_directed_lines T_0 T_2) \/ (unequally_directed_lines T_1 (reverse_line T_2))))) (All L, (All M, (All N, (((unequally_directed_lines L M) /\ (unequally_directed_lines L (reverse_line M))) => (((unequally_directed_lines L N) /\ (unequally_directed_lines L (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N)))))))) (All L, (All M, (All N, ((unequally_directed_lines L M) => ((unequally_directed_lines L N) \/ (unequally_directed_lines M N)))))) ### ConjTree 71 % 0.18/0.53 73. (-. (All N, ((unequally_directed_lines T_0 (reverse_line T_1)) => ((unequally_directed_lines T_0 N) \/ (unequally_directed_lines T_1 (reverse_line N)))))) (All L, (All M, (All N, ((unequally_directed_lines L M) => ((unequally_directed_lines L N) \/ (unequally_directed_lines M N)))))) (All L, (All M, (All N, (((unequally_directed_lines L M) /\ (unequally_directed_lines L (reverse_line M))) => (((unequally_directed_lines L N) /\ (unequally_directed_lines L (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N)))))))) ### NotAllEx 72 % 0.18/0.53 74. (-. (All M, (All N, ((unequally_directed_lines T_0 (reverse_line M)) => ((unequally_directed_lines T_0 N) \/ (unequally_directed_lines M (reverse_line N))))))) (All L, (All M, (All N, (((unequally_directed_lines L M) /\ (unequally_directed_lines L (reverse_line M))) => (((unequally_directed_lines L N) /\ (unequally_directed_lines L (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N)))))))) (All L, (All M, (All N, ((unequally_directed_lines L M) => ((unequally_directed_lines L N) \/ (unequally_directed_lines M N)))))) ### NotAllEx 73 % 0.18/0.53 75. (-. (All L, (All M, (All N, ((unequally_directed_lines L (reverse_line M)) => ((unequally_directed_lines L N) \/ (unequally_directed_lines M (reverse_line N)))))))) (All L, (All M, (All N, ((unequally_directed_lines L M) => ((unequally_directed_lines L N) \/ (unequally_directed_lines M N)))))) (All L, (All M, (All N, (((unequally_directed_lines L M) /\ (unequally_directed_lines L (reverse_line M))) => (((unequally_directed_lines L N) /\ (unequally_directed_lines L (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N)))))))) ### NotAllEx 74 % 0.18/0.53 % SZS output end Proof % 0.18/0.53 (* END-PROOF *) %------------------------------------------------------------------------------