%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : GEO255+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 : n012.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:37 EDT 2022 % Result : Theorem 0.37s 0.56s % Output : Proof 0.37s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : GEO255+3 : TPTP v8.1.0. Released v4.0.0. % 0.07/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n012.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 14:39:08 EDT 2022 % 0.12/0.34 % CPUTime : % 0.37/0.56 % SZS status Theorem % 0.37/0.56 (* PROOF-FOUND *) % 0.37/0.56 (* BEGIN-PROOF *) % 0.37/0.56 % SZS output start Proof % 0.37/0.56 1. (unequally_directed_lines (line_connecting T_0 T_1) T_2) (-. (unequally_directed_lines (line_connecting T_0 T_1) T_2)) ### Axiom % 0.37/0.56 2. (unequally_directed_lines (line_connecting T_0 T_1) T_2) (-. (unequally_directed_lines (line_connecting T_0 T_1) T_2)) ### Axiom % 0.37/0.56 3. (unequally_directed_lines (line_connecting T_0 T_1) (line_connecting T_0 T_1)) (-. (unequally_directed_lines (line_connecting T_0 T_1) (line_connecting T_0 T_1))) ### Axiom % 0.37/0.56 4. (-. (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line T_2))) (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line T_2)) ### Axiom % 0.37/0.56 5. (-. (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line T_2))) (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line T_2)) ### Axiom % 0.37/0.56 6. ((unequally_directed_lines (line_connecting T_0 T_1) (line_connecting T_0 T_1)) => ((unequally_directed_lines (line_connecting T_0 T_1) (reverse_line T_2)) \/ (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line T_2)))) (-. (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line T_2))) (unequally_directed_lines (line_connecting T_0 T_1) (line_connecting T_0 T_1)) ### DisjTree 3 4 5 % 0.37/0.56 7. (All N, ((unequally_directed_lines (line_connecting T_0 T_1) (line_connecting T_0 T_1)) => ((unequally_directed_lines (line_connecting T_0 T_1) N) \/ (unequally_directed_lines (line_connecting T_0 T_1) N)))) (unequally_directed_lines (line_connecting T_0 T_1) (line_connecting T_0 T_1)) (-. (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line T_2))) ### All 6 % 0.37/0.56 8. (All M, (All N, ((unequally_directed_lines (line_connecting T_0 T_1) M) => ((unequally_directed_lines (line_connecting T_0 T_1) N) \/ (unequally_directed_lines M N))))) (-. (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line T_2))) (unequally_directed_lines (line_connecting T_0 T_1) (line_connecting T_0 T_1)) ### All 7 % 0.37/0.56 9. (-. (unequally_directed_lines T_2 (line_connecting T_0 T_1))) (unequally_directed_lines T_2 (line_connecting T_0 T_1)) ### Axiom % 0.37/0.56 10. ((unequally_directed_lines (line_connecting T_0 T_1) T_2) => ((unequally_directed_lines (line_connecting T_0 T_1) (line_connecting T_0 T_1)) \/ (unequally_directed_lines T_2 (line_connecting T_0 T_1)))) (-. (unequally_directed_lines T_2 (line_connecting T_0 T_1))) (-. (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line T_2))) (All M, (All N, ((unequally_directed_lines (line_connecting T_0 T_1) M) => ((unequally_directed_lines (line_connecting T_0 T_1) N) \/ (unequally_directed_lines M N))))) (unequally_directed_lines (line_connecting T_0 T_1) T_2) ### DisjTree 2 8 9 % 0.37/0.56 11. (All N, ((unequally_directed_lines (line_connecting T_0 T_1) T_2) => ((unequally_directed_lines (line_connecting T_0 T_1) N) \/ (unequally_directed_lines T_2 N)))) (unequally_directed_lines (line_connecting T_0 T_1) T_2) (All M, (All N, ((unequally_directed_lines (line_connecting T_0 T_1) M) => ((unequally_directed_lines (line_connecting T_0 T_1) N) \/ (unequally_directed_lines M N))))) (-. (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line T_2))) (-. (unequally_directed_lines T_2 (line_connecting T_0 T_1))) ### All 10 % 0.37/0.56 12. (-. (unequally_directed_lines T_2 (line_connecting T_0 T_1))) (-. (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line T_2))) (All M, (All N, ((unequally_directed_lines (line_connecting T_0 T_1) M) => ((unequally_directed_lines (line_connecting T_0 T_1) N) \/ (unequally_directed_lines M N))))) (unequally_directed_lines (line_connecting T_0 T_1) T_2) ### All 11 % 0.37/0.56 13. (All L, (All M, (All N, ((unequally_directed_lines L M) => ((unequally_directed_lines L N) \/ (unequally_directed_lines M N)))))) (unequally_directed_lines (line_connecting T_0 T_1) T_2) (-. (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line T_2))) (-. (unequally_directed_lines T_2 (line_connecting T_0 T_1))) ### All 12 % 0.37/0.56 14. (unequally_directed_lines (line_connecting T_0 T_1) T_2) (-. (unequally_directed_lines (line_connecting T_0 T_1) T_2)) ### Axiom % 0.37/0.56 15. (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line T_2)) (-. (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line T_2))) ### Axiom % 0.37/0.56 16. (-. (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line (line_connecting T_1 T_0)))) (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line (line_connecting T_1 T_0))) ### Axiom % 0.37/0.56 17. ((unequally_directed_lines (line_connecting T_0 T_1) (line_connecting T_1 T_0)) /\ (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line (line_connecting T_1 T_0)))) (-. (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line (line_connecting T_1 T_0)))) ### And 16 % 0.37/0.56 18. (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (unequally_directed_lines T_2 (line_connecting T_1 T_0)) ### Axiom % 0.37/0.56 19. ((unequally_directed_lines T_2 (line_connecting T_1 T_0)) /\ (unequally_directed_lines T_2 (reverse_line (line_connecting T_1 T_0)))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) ### And 18 % 0.37/0.56 20. (((unequally_directed_lines (line_connecting T_0 T_1) T_2) /\ (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line T_2))) => (((unequally_directed_lines (line_connecting T_0 T_1) (line_connecting T_1 T_0)) /\ (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line (line_connecting T_1 T_0)))) \/ ((unequally_directed_lines T_2 (line_connecting T_1 T_0)) /\ (unequally_directed_lines T_2 (reverse_line (line_connecting T_1 T_0)))))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (-. (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line (line_connecting T_1 T_0)))) (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line T_2)) (unequally_directed_lines (line_connecting T_0 T_1) T_2) ### DisjTree 14 15 17 19 % 0.37/0.56 21. (All N, (((unequally_directed_lines (line_connecting T_0 T_1) T_2) /\ (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line T_2))) => (((unequally_directed_lines (line_connecting T_0 T_1) N) /\ (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line N))) \/ ((unequally_directed_lines T_2 N) /\ (unequally_directed_lines T_2 (reverse_line N)))))) (unequally_directed_lines (line_connecting T_0 T_1) T_2) (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line T_2)) (-. (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line (line_connecting T_1 T_0)))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) ### All 20 % 0.37/0.56 22. (All M, (All N, (((unequally_directed_lines (line_connecting T_0 T_1) M) /\ (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line M))) => (((unequally_directed_lines (line_connecting T_0 T_1) N) /\ (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N))))))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (-. (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line (line_connecting T_1 T_0)))) (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line T_2)) (unequally_directed_lines (line_connecting T_0 T_1) T_2) ### All 21 % 0.37/0.56 23. (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 (line_connecting T_0 T_1) T_2) (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line T_2)) (-. (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line (line_connecting T_1 T_0)))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) ### All 22 % 0.37/0.56 24. ((unequally_directed_lines (line_connecting T_0 T_1) T_2) /\ (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line T_2))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (-. (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line (line_connecting T_1 T_0)))) (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)))))))) ### And 23 % 0.37/0.56 25. (-. (unequally_directed_lines T_2 T_2)) (unequally_directed_lines T_2 T_2) ### Axiom % 0.37/0.56 26. ((unequally_directed_lines T_2 T_2) /\ (unequally_directed_lines T_2 (reverse_line T_2))) (-. (unequally_directed_lines T_2 T_2)) ### And 25 % 0.37/0.56 27. (((unequally_directed_lines (line_connecting T_0 T_1) T_2) /\ (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line T_2))) => (((unequally_directed_lines (line_connecting T_0 T_1) T_2) /\ (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line T_2))) \/ ((unequally_directed_lines T_2 T_2) /\ (unequally_directed_lines T_2 (reverse_line T_2))))) (-. (unequally_directed_lines T_2 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 (line_connecting T_0 T_1) (reverse_line (line_connecting T_1 T_0)))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (-. (unequally_directed_lines T_2 (line_connecting T_0 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 (line_connecting T_0 T_1) T_2) ### DisjTree 1 13 24 26 % 0.37/0.56 28. (All N, (((unequally_directed_lines (line_connecting T_0 T_1) T_2) /\ (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line T_2))) => (((unequally_directed_lines (line_connecting T_0 T_1) N) /\ (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line N))) \/ ((unequally_directed_lines T_2 N) /\ (unequally_directed_lines T_2 (reverse_line N)))))) (unequally_directed_lines (line_connecting T_0 T_1) T_2) (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_2 (line_connecting T_0 T_1))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (-. (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line (line_connecting T_1 T_0)))) (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_2 T_2)) ### All 27 % 0.37/0.56 29. (All M, (All N, (((unequally_directed_lines (line_connecting T_0 T_1) M) /\ (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line M))) => (((unequally_directed_lines (line_connecting T_0 T_1) N) /\ (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N))))))) (-. (unequally_directed_lines T_2 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 (line_connecting T_0 T_1) (reverse_line (line_connecting T_1 T_0)))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (-. (unequally_directed_lines T_2 (line_connecting T_0 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 (line_connecting T_0 T_1) T_2) ### All 28 % 0.37/0.56 30. (unequally_directed_lines (line_connecting T_0 T_1) T_2) (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_2 (line_connecting T_0 T_1))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (-. (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line (line_connecting T_1 T_0)))) (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_2 T_2)) ### All 29 % 0.37/0.56 31. (unequally_directed_lines T_2 T_2) (-. (unequally_directed_lines T_2 T_2)) ### Axiom % 0.37/0.56 32. (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (unequally_directed_lines T_2 (line_connecting T_1 T_0)) ### Axiom % 0.37/0.56 33. (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (unequally_directed_lines T_2 (line_connecting T_1 T_0)) ### Axiom % 0.37/0.56 34. ((unequally_directed_lines T_2 T_2) => ((unequally_directed_lines T_2 (line_connecting T_1 T_0)) \/ (unequally_directed_lines T_2 (line_connecting T_1 T_0)))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (unequally_directed_lines T_2 T_2) ### DisjTree 31 32 33 % 0.37/0.56 35. (All N, ((unequally_directed_lines T_2 T_2) => ((unequally_directed_lines T_2 N) \/ (unequally_directed_lines T_2 N)))) (unequally_directed_lines T_2 T_2) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) ### All 34 % 0.37/0.56 36. (All M, (All N, ((unequally_directed_lines T_2 M) => ((unequally_directed_lines T_2 N) \/ (unequally_directed_lines M N))))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (unequally_directed_lines T_2 T_2) ### All 35 % 0.37/0.56 37. ((unequally_directed_lines T_2 T_2) => ((unequally_directed_lines T_2 T_2) \/ (unequally_directed_lines T_2 T_2))) (All M, (All N, ((unequally_directed_lines T_2 M) => ((unequally_directed_lines T_2 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 (line_connecting T_0 T_1) (reverse_line (line_connecting T_1 T_0)))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (-. (unequally_directed_lines T_2 (line_connecting T_0 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 (line_connecting T_0 T_1) T_2) ### DisjTree 30 36 36 % 0.37/0.56 38. (All N, ((unequally_directed_lines T_2 T_2) => ((unequally_directed_lines T_2 N) \/ (unequally_directed_lines T_2 N)))) (unequally_directed_lines (line_connecting T_0 T_1) T_2) (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_2 (line_connecting T_0 T_1))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (-. (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line (line_connecting T_1 T_0)))) (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_2 M) => ((unequally_directed_lines T_2 N) \/ (unequally_directed_lines M N))))) ### All 37 % 0.37/0.56 39. (All M, (All N, ((unequally_directed_lines T_2 M) => ((unequally_directed_lines T_2 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 (line_connecting T_0 T_1) (reverse_line (line_connecting T_1 T_0)))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (-. (unequally_directed_lines T_2 (line_connecting T_0 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 (line_connecting T_0 T_1) T_2) ### All 38 % 0.37/0.57 40. (unequally_directed_lines (line_connecting T_0 T_1) T_2) (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_2 (line_connecting T_0 T_1))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (-. (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line (line_connecting T_1 T_0)))) (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 39 % 0.37/0.57 41. (unequally_directed_lines (line_connecting T_1 T_0) (line_connecting T_0 T_1)) (-. (unequally_directed_lines (line_connecting T_1 T_0) (line_connecting T_0 T_1))) ### Axiom % 0.37/0.57 42. (-. (unequally_directed_lines (line_connecting T_1 T_0) T_2)) (unequally_directed_lines (line_connecting T_1 T_0) T_2) ### Axiom % 0.37/0.57 43. (-. (unequally_directed_lines (line_connecting T_0 T_1) T_2)) (unequally_directed_lines (line_connecting T_0 T_1) T_2) ### Axiom % 0.37/0.57 44. ((unequally_directed_lines (line_connecting T_1 T_0) (line_connecting T_0 T_1)) => ((unequally_directed_lines (line_connecting T_1 T_0) T_2) \/ (unequally_directed_lines (line_connecting T_0 T_1) T_2))) (-. (unequally_directed_lines (line_connecting T_0 T_1) T_2)) (-. (unequally_directed_lines (line_connecting T_1 T_0) T_2)) (unequally_directed_lines (line_connecting T_1 T_0) (line_connecting T_0 T_1)) ### DisjTree 41 42 43 % 0.37/0.57 45. (All N, ((unequally_directed_lines (line_connecting T_1 T_0) (line_connecting T_0 T_1)) => ((unequally_directed_lines (line_connecting T_1 T_0) N) \/ (unequally_directed_lines (line_connecting T_0 T_1) N)))) (unequally_directed_lines (line_connecting T_1 T_0) (line_connecting T_0 T_1)) (-. (unequally_directed_lines (line_connecting T_1 T_0) T_2)) (-. (unequally_directed_lines (line_connecting T_0 T_1) T_2)) ### All 44 % 0.37/0.57 46. (All M, (All N, ((unequally_directed_lines (line_connecting T_1 T_0) M) => ((unequally_directed_lines (line_connecting T_1 T_0) N) \/ (unequally_directed_lines M N))))) (-. (unequally_directed_lines (line_connecting T_0 T_1) T_2)) (-. (unequally_directed_lines (line_connecting T_1 T_0) T_2)) (unequally_directed_lines (line_connecting T_1 T_0) (line_connecting T_0 T_1)) ### All 45 % 0.37/0.57 47. (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line T_2)) (-. (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line T_2))) ### Axiom % 0.37/0.57 48. (((unequally_directed_lines (line_connecting T_0 T_1) T_2) /\ (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line T_2))) => (((unequally_directed_lines (line_connecting T_0 T_1) T_2) /\ (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line T_2))) \/ ((unequally_directed_lines T_2 T_2) /\ (unequally_directed_lines T_2 (reverse_line T_2))))) (-. (unequally_directed_lines T_2 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 (line_connecting T_0 T_1) (reverse_line (line_connecting T_1 T_0)))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line T_2)) (unequally_directed_lines (line_connecting T_1 T_0) (line_connecting T_0 T_1)) (-. (unequally_directed_lines (line_connecting T_1 T_0) T_2)) (All M, (All N, ((unequally_directed_lines (line_connecting T_1 T_0) M) => ((unequally_directed_lines (line_connecting T_1 T_0) N) \/ (unequally_directed_lines M N))))) ### DisjTree 46 47 24 26 % 0.37/0.57 49. (All N, (((unequally_directed_lines (line_connecting T_0 T_1) T_2) /\ (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line T_2))) => (((unequally_directed_lines (line_connecting T_0 T_1) N) /\ (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line N))) \/ ((unequally_directed_lines T_2 N) /\ (unequally_directed_lines T_2 (reverse_line N)))))) (All M, (All N, ((unequally_directed_lines (line_connecting T_1 T_0) M) => ((unequally_directed_lines (line_connecting T_1 T_0) N) \/ (unequally_directed_lines M N))))) (-. (unequally_directed_lines (line_connecting T_1 T_0) T_2)) (unequally_directed_lines (line_connecting T_1 T_0) (line_connecting T_0 T_1)) (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line T_2)) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (-. (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line (line_connecting T_1 T_0)))) (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_2 T_2)) ### All 48 % 0.37/0.57 50. (All M, (All N, (((unequally_directed_lines (line_connecting T_0 T_1) M) /\ (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line M))) => (((unequally_directed_lines (line_connecting T_0 T_1) N) /\ (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N))))))) (-. (unequally_directed_lines T_2 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 (line_connecting T_0 T_1) (reverse_line (line_connecting T_1 T_0)))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line T_2)) (unequally_directed_lines (line_connecting T_1 T_0) (line_connecting T_0 T_1)) (-. (unequally_directed_lines (line_connecting T_1 T_0) T_2)) (All M, (All N, ((unequally_directed_lines (line_connecting T_1 T_0) M) => ((unequally_directed_lines (line_connecting T_1 T_0) N) \/ (unequally_directed_lines M N))))) ### All 49 % 0.37/0.57 51. (All M, (All N, ((unequally_directed_lines (line_connecting T_1 T_0) M) => ((unequally_directed_lines (line_connecting T_1 T_0) N) \/ (unequally_directed_lines M N))))) (-. (unequally_directed_lines (line_connecting T_1 T_0) T_2)) (unequally_directed_lines (line_connecting T_1 T_0) (line_connecting T_0 T_1)) (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line T_2)) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (-. (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line (line_connecting T_1 T_0)))) (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_2 T_2)) ### All 50 % 0.37/0.57 52. (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_2 T_2) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) ### All 36 % 0.37/0.57 53. ((unequally_directed_lines T_2 T_2) => ((unequally_directed_lines T_2 T_2) \/ (unequally_directed_lines T_2 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 (line_connecting T_0 T_1) (reverse_line (line_connecting T_1 T_0)))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line T_2)) (unequally_directed_lines (line_connecting T_1 T_0) (line_connecting T_0 T_1)) (-. (unequally_directed_lines (line_connecting T_1 T_0) T_2)) (All M, (All N, ((unequally_directed_lines (line_connecting T_1 T_0) M) => ((unequally_directed_lines (line_connecting T_1 T_0) N) \/ (unequally_directed_lines M N))))) ### DisjTree 51 52 52 % 0.37/0.58 54. (All N, ((unequally_directed_lines T_2 T_2) => ((unequally_directed_lines T_2 N) \/ (unequally_directed_lines T_2 N)))) (All M, (All N, ((unequally_directed_lines (line_connecting T_1 T_0) M) => ((unequally_directed_lines (line_connecting T_1 T_0) N) \/ (unequally_directed_lines M N))))) (-. (unequally_directed_lines (line_connecting T_1 T_0) T_2)) (unequally_directed_lines (line_connecting T_1 T_0) (line_connecting T_0 T_1)) (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line T_2)) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (-. (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line (line_connecting T_1 T_0)))) (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)))))) ### All 53 % 0.37/0.58 55. (All M, (All N, ((unequally_directed_lines T_2 M) => ((unequally_directed_lines T_2 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)))))) (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 (line_connecting T_0 T_1) (reverse_line (line_connecting T_1 T_0)))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line T_2)) (unequally_directed_lines (line_connecting T_1 T_0) (line_connecting T_0 T_1)) (-. (unequally_directed_lines (line_connecting T_1 T_0) T_2)) (All M, (All N, ((unequally_directed_lines (line_connecting T_1 T_0) M) => ((unequally_directed_lines (line_connecting T_1 T_0) N) \/ (unequally_directed_lines M N))))) ### All 54 % 0.37/0.58 56. (All M, (All N, ((unequally_directed_lines (line_connecting T_1 T_0) M) => ((unequally_directed_lines (line_connecting T_1 T_0) N) \/ (unequally_directed_lines M N))))) (-. (unequally_directed_lines (line_connecting T_1 T_0) T_2)) (unequally_directed_lines (line_connecting T_1 T_0) (line_connecting T_0 T_1)) (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line T_2)) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (-. (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line (line_connecting T_1 T_0)))) (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)))))) ### All 55 % 0.37/0.58 57. ((unequally_directed_lines (line_connecting T_0 T_1) T_2) \/ (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line T_2))) (unequally_directed_lines (line_connecting T_1 T_0) (line_connecting T_0 T_1)) (-. (unequally_directed_lines (line_connecting T_1 T_0) T_2)) (All M, (All N, ((unequally_directed_lines (line_connecting T_1 T_0) M) => ((unequally_directed_lines (line_connecting T_1 T_0) 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 (line_connecting T_0 T_1) (reverse_line (line_connecting T_1 T_0)))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (-. (unequally_directed_lines T_2 (line_connecting T_0 T_1))) (All L, (All M, (All N, ((unequally_directed_lines L M) => ((unequally_directed_lines L N) \/ (unequally_directed_lines M N)))))) ### Or 40 56 % 0.37/0.58 58. (All M, ((unequally_directed_lines (line_connecting T_0 T_1) M) \/ (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line M)))) (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_2 (line_connecting T_0 T_1))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (-. (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line (line_connecting T_1 T_0)))) (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 (line_connecting T_1 T_0) M) => ((unequally_directed_lines (line_connecting T_1 T_0) N) \/ (unequally_directed_lines M N))))) (-. (unequally_directed_lines (line_connecting T_1 T_0) T_2)) (unequally_directed_lines (line_connecting T_1 T_0) (line_connecting T_0 T_1)) ### All 57 % 0.37/0.58 59. (unequally_directed_lines (line_connecting T_1 T_0) T_2) (-. (unequally_directed_lines (line_connecting T_1 T_0) T_2)) ### Axiom % 0.37/0.58 60. (unequally_directed_lines (line_connecting T_1 T_0) T_2) (-. (unequally_directed_lines (line_connecting T_1 T_0) T_2)) ### Axiom % 0.37/0.58 61. (-. (unequally_directed_lines (line_connecting T_1 T_0) (line_connecting T_1 T_0))) (unequally_directed_lines (line_connecting T_1 T_0) (line_connecting T_1 T_0)) ### Axiom % 0.37/0.58 62. (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (unequally_directed_lines T_2 (line_connecting T_1 T_0)) ### Axiom % 0.37/0.58 63. ((unequally_directed_lines (line_connecting T_1 T_0) T_2) => ((unequally_directed_lines (line_connecting T_1 T_0) (line_connecting T_1 T_0)) \/ (unequally_directed_lines T_2 (line_connecting T_1 T_0)))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (-. (unequally_directed_lines (line_connecting T_1 T_0) (line_connecting T_1 T_0))) (unequally_directed_lines (line_connecting T_1 T_0) T_2) ### DisjTree 60 61 62 % 0.37/0.58 64. (All N, ((unequally_directed_lines (line_connecting T_1 T_0) T_2) => ((unequally_directed_lines (line_connecting T_1 T_0) N) \/ (unequally_directed_lines T_2 N)))) (unequally_directed_lines (line_connecting T_1 T_0) T_2) (-. (unequally_directed_lines (line_connecting T_1 T_0) (line_connecting T_1 T_0))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) ### All 63 % 0.37/0.58 65. (unequally_directed_lines (line_connecting T_1 T_0) (line_connecting T_1 T_0)) (-. (unequally_directed_lines (line_connecting T_1 T_0) (line_connecting T_1 T_0))) ### Axiom % 0.37/0.58 66. (-. (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line T_2))) (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line T_2)) ### Axiom % 0.37/0.58 67. (-. (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line T_2))) (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line T_2)) ### Axiom % 0.37/0.58 68. ((unequally_directed_lines (line_connecting T_1 T_0) (line_connecting T_1 T_0)) => ((unequally_directed_lines (line_connecting T_1 T_0) (reverse_line T_2)) \/ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line T_2)))) (-. (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line T_2))) (unequally_directed_lines (line_connecting T_1 T_0) (line_connecting T_1 T_0)) ### DisjTree 65 66 67 % 0.37/0.58 69. (All N, ((unequally_directed_lines (line_connecting T_1 T_0) (line_connecting T_1 T_0)) => ((unequally_directed_lines (line_connecting T_1 T_0) N) \/ (unequally_directed_lines (line_connecting T_1 T_0) N)))) (unequally_directed_lines (line_connecting T_1 T_0) (line_connecting T_1 T_0)) (-. (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line T_2))) ### All 68 % 0.37/0.58 70. (All M, (All N, ((unequally_directed_lines (line_connecting T_1 T_0) M) => ((unequally_directed_lines (line_connecting T_1 T_0) N) \/ (unequally_directed_lines M N))))) (-. (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line T_2))) (unequally_directed_lines (line_connecting T_1 T_0) (line_connecting T_1 T_0)) ### All 69 % 0.37/0.58 71. (-. (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line (line_connecting T_1 T_0)))) (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line (line_connecting T_1 T_0))) ### Axiom % 0.37/0.58 72. ((unequally_directed_lines (line_connecting T_1 T_0) (line_connecting T_1 T_0)) \/ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line (line_connecting T_1 T_0)))) (-. (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line (line_connecting T_1 T_0)))) (-. (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line T_2))) (All M, (All N, ((unequally_directed_lines (line_connecting T_1 T_0) M) => ((unequally_directed_lines (line_connecting T_1 T_0) N) \/ (unequally_directed_lines M N))))) ### Or 70 71 % 0.37/0.58 73. (All M, ((unequally_directed_lines (line_connecting T_1 T_0) M) \/ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line M)))) (All M, (All N, ((unequally_directed_lines (line_connecting T_1 T_0) M) => ((unequally_directed_lines (line_connecting T_1 T_0) N) \/ (unequally_directed_lines M N))))) (-. (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line T_2))) (-. (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line (line_connecting T_1 T_0)))) ### All 72 % 0.37/0.58 74. (unequally_directed_lines (line_connecting T_1 T_0) T_2) (-. (unequally_directed_lines (line_connecting T_1 T_0) T_2)) ### Axiom % 0.37/0.58 75. (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line T_2)) (-. (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line T_2))) ### Axiom % 0.37/0.58 76. (-. (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line (line_connecting T_0 T_1)))) (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line (line_connecting T_0 T_1))) ### Axiom % 0.37/0.58 77. ((unequally_directed_lines (line_connecting T_1 T_0) (line_connecting T_0 T_1)) /\ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line (line_connecting T_0 T_1)))) (-. (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line (line_connecting T_0 T_1)))) ### And 76 % 0.37/0.58 78. (-. (unequally_directed_lines T_2 (line_connecting T_0 T_1))) (unequally_directed_lines T_2 (line_connecting T_0 T_1)) ### Axiom % 0.37/0.58 79. ((unequally_directed_lines T_2 (line_connecting T_0 T_1)) /\ (unequally_directed_lines T_2 (reverse_line (line_connecting T_0 T_1)))) (-. (unequally_directed_lines T_2 (line_connecting T_0 T_1))) ### And 78 % 0.37/0.58 80. (((unequally_directed_lines (line_connecting T_1 T_0) T_2) /\ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line T_2))) => (((unequally_directed_lines (line_connecting T_1 T_0) (line_connecting T_0 T_1)) /\ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line (line_connecting T_0 T_1)))) \/ ((unequally_directed_lines T_2 (line_connecting T_0 T_1)) /\ (unequally_directed_lines T_2 (reverse_line (line_connecting T_0 T_1)))))) (-. (unequally_directed_lines T_2 (line_connecting T_0 T_1))) (-. (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line (line_connecting T_0 T_1)))) (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line T_2)) (unequally_directed_lines (line_connecting T_1 T_0) T_2) ### DisjTree 74 75 77 79 % 0.37/0.58 81. (All N, (((unequally_directed_lines (line_connecting T_1 T_0) T_2) /\ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line T_2))) => (((unequally_directed_lines (line_connecting T_1 T_0) N) /\ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line N))) \/ ((unequally_directed_lines T_2 N) /\ (unequally_directed_lines T_2 (reverse_line N)))))) (unequally_directed_lines (line_connecting T_1 T_0) T_2) (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line T_2)) (-. (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line (line_connecting T_0 T_1)))) (-. (unequally_directed_lines T_2 (line_connecting T_0 T_1))) ### All 80 % 0.37/0.58 82. (All M, (All N, (((unequally_directed_lines (line_connecting T_1 T_0) M) /\ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line M))) => (((unequally_directed_lines (line_connecting T_1 T_0) N) /\ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N))))))) (-. (unequally_directed_lines T_2 (line_connecting T_0 T_1))) (-. (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line (line_connecting T_0 T_1)))) (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line T_2)) (unequally_directed_lines (line_connecting T_1 T_0) T_2) ### All 81 % 0.37/0.58 83. (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 (line_connecting T_1 T_0) T_2) (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line T_2)) (-. (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line (line_connecting T_0 T_1)))) (-. (unequally_directed_lines T_2 (line_connecting T_0 T_1))) ### All 82 % 0.37/0.58 84. ((unequally_directed_lines (line_connecting T_1 T_0) T_2) /\ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line T_2))) (-. (unequally_directed_lines T_2 (line_connecting T_0 T_1))) (-. (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line (line_connecting 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)))))))) ### And 83 % 0.37/0.58 85. (((unequally_directed_lines (line_connecting T_1 T_0) (line_connecting T_1 T_0)) /\ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line (line_connecting T_1 T_0)))) => (((unequally_directed_lines (line_connecting T_1 T_0) T_2) /\ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line T_2))) \/ ((unequally_directed_lines (line_connecting T_1 T_0) T_2) /\ (unequally_directed_lines (line_connecting T_1 T_0) (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 (line_connecting T_1 T_0) (reverse_line (line_connecting T_0 T_1)))) (-. (unequally_directed_lines T_2 (line_connecting T_0 T_1))) (-. (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line T_2))) (All M, (All N, ((unequally_directed_lines (line_connecting T_1 T_0) M) => ((unequally_directed_lines (line_connecting T_1 T_0) N) \/ (unequally_directed_lines M N))))) (All M, ((unequally_directed_lines (line_connecting T_1 T_0) M) \/ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line M)))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (unequally_directed_lines (line_connecting T_1 T_0) T_2) (All N, ((unequally_directed_lines (line_connecting T_1 T_0) T_2) => ((unequally_directed_lines (line_connecting T_1 T_0) N) \/ (unequally_directed_lines T_2 N)))) ### DisjTree 64 73 84 84 % 0.37/0.59 86. (All N, (((unequally_directed_lines (line_connecting T_1 T_0) (line_connecting T_1 T_0)) /\ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line (line_connecting T_1 T_0)))) => (((unequally_directed_lines (line_connecting T_1 T_0) N) /\ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line N))) \/ ((unequally_directed_lines (line_connecting T_1 T_0) N) /\ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line N)))))) (All N, ((unequally_directed_lines (line_connecting T_1 T_0) T_2) => ((unequally_directed_lines (line_connecting T_1 T_0) N) \/ (unequally_directed_lines T_2 N)))) (unequally_directed_lines (line_connecting T_1 T_0) T_2) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (All M, ((unequally_directed_lines (line_connecting T_1 T_0) M) \/ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line M)))) (All M, (All N, ((unequally_directed_lines (line_connecting T_1 T_0) M) => ((unequally_directed_lines (line_connecting T_1 T_0) N) \/ (unequally_directed_lines M N))))) (-. (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line T_2))) (-. (unequally_directed_lines T_2 (line_connecting T_0 T_1))) (-. (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line (line_connecting 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)))))))) ### All 85 % 0.37/0.59 87. (All M, (All N, (((unequally_directed_lines (line_connecting T_1 T_0) M) /\ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line M))) => (((unequally_directed_lines (line_connecting T_1 T_0) N) /\ (unequally_directed_lines (line_connecting T_1 T_0) (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 (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 (line_connecting T_1 T_0) (reverse_line (line_connecting T_0 T_1)))) (-. (unequally_directed_lines T_2 (line_connecting T_0 T_1))) (-. (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line T_2))) (All M, (All N, ((unequally_directed_lines (line_connecting T_1 T_0) M) => ((unequally_directed_lines (line_connecting T_1 T_0) N) \/ (unequally_directed_lines M N))))) (All M, ((unequally_directed_lines (line_connecting T_1 T_0) M) \/ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line M)))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (unequally_directed_lines (line_connecting T_1 T_0) T_2) (All N, ((unequally_directed_lines (line_connecting T_1 T_0) T_2) => ((unequally_directed_lines (line_connecting T_1 T_0) N) \/ (unequally_directed_lines T_2 N)))) ### All 86 % 0.37/0.59 88. (((unequally_directed_lines (line_connecting T_1 T_0) T_2) /\ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line T_2))) => (((unequally_directed_lines (line_connecting T_1 T_0) T_2) /\ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line T_2))) \/ ((unequally_directed_lines T_2 T_2) /\ (unequally_directed_lines T_2 (reverse_line T_2))))) (-. (unequally_directed_lines T_2 T_2)) (All N, ((unequally_directed_lines (line_connecting T_1 T_0) T_2) => ((unequally_directed_lines (line_connecting T_1 T_0) N) \/ (unequally_directed_lines T_2 N)))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (All M, ((unequally_directed_lines (line_connecting T_1 T_0) M) \/ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line M)))) (All M, (All N, ((unequally_directed_lines (line_connecting T_1 T_0) M) => ((unequally_directed_lines (line_connecting T_1 T_0) N) \/ (unequally_directed_lines M N))))) (-. (unequally_directed_lines T_2 (line_connecting T_0 T_1))) (-. (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line (line_connecting 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)))))))) (All M, (All N, (((unequally_directed_lines (line_connecting T_1 T_0) M) /\ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line M))) => (((unequally_directed_lines (line_connecting T_1 T_0) N) /\ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N))))))) (unequally_directed_lines (line_connecting T_1 T_0) T_2) ### DisjTree 59 87 84 26 % 0.37/0.59 89. (All N, (((unequally_directed_lines (line_connecting T_1 T_0) T_2) /\ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line T_2))) => (((unequally_directed_lines (line_connecting T_1 T_0) N) /\ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line N))) \/ ((unequally_directed_lines T_2 N) /\ (unequally_directed_lines T_2 (reverse_line N)))))) (unequally_directed_lines (line_connecting T_1 T_0) T_2) (All M, (All N, (((unequally_directed_lines (line_connecting T_1 T_0) M) /\ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line M))) => (((unequally_directed_lines (line_connecting T_1 T_0) N) /\ (unequally_directed_lines (line_connecting T_1 T_0) (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 (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 (line_connecting T_1 T_0) (reverse_line (line_connecting T_0 T_1)))) (-. (unequally_directed_lines T_2 (line_connecting T_0 T_1))) (All M, (All N, ((unequally_directed_lines (line_connecting T_1 T_0) M) => ((unequally_directed_lines (line_connecting T_1 T_0) N) \/ (unequally_directed_lines M N))))) (All M, ((unequally_directed_lines (line_connecting T_1 T_0) M) \/ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line M)))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (All N, ((unequally_directed_lines (line_connecting T_1 T_0) T_2) => ((unequally_directed_lines (line_connecting T_1 T_0) N) \/ (unequally_directed_lines T_2 N)))) (-. (unequally_directed_lines T_2 T_2)) ### All 88 % 0.37/0.59 90. (-. (unequally_directed_lines T_2 T_2)) (All N, ((unequally_directed_lines (line_connecting T_1 T_0) T_2) => ((unequally_directed_lines (line_connecting T_1 T_0) N) \/ (unequally_directed_lines T_2 N)))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (All M, ((unequally_directed_lines (line_connecting T_1 T_0) M) \/ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line M)))) (All M, (All N, ((unequally_directed_lines (line_connecting T_1 T_0) M) => ((unequally_directed_lines (line_connecting T_1 T_0) N) \/ (unequally_directed_lines M N))))) (-. (unequally_directed_lines T_2 (line_connecting T_0 T_1))) (-. (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line (line_connecting 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)))))))) (All M, (All N, (((unequally_directed_lines (line_connecting T_1 T_0) M) /\ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line M))) => (((unequally_directed_lines (line_connecting T_1 T_0) N) /\ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N))))))) (unequally_directed_lines (line_connecting T_1 T_0) T_2) ### All 89 % 0.37/0.59 91. ((unequally_directed_lines T_2 T_2) => ((unequally_directed_lines T_2 T_2) \/ (unequally_directed_lines T_2 T_2))) (All M, (All N, ((unequally_directed_lines T_2 M) => ((unequally_directed_lines T_2 N) \/ (unequally_directed_lines M N))))) (unequally_directed_lines (line_connecting T_1 T_0) T_2) (All M, (All N, (((unequally_directed_lines (line_connecting T_1 T_0) M) /\ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line M))) => (((unequally_directed_lines (line_connecting T_1 T_0) N) /\ (unequally_directed_lines (line_connecting T_1 T_0) (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 (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 (line_connecting T_1 T_0) (reverse_line (line_connecting T_0 T_1)))) (-. (unequally_directed_lines T_2 (line_connecting T_0 T_1))) (All M, (All N, ((unequally_directed_lines (line_connecting T_1 T_0) M) => ((unequally_directed_lines (line_connecting T_1 T_0) N) \/ (unequally_directed_lines M N))))) (All M, ((unequally_directed_lines (line_connecting T_1 T_0) M) \/ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line M)))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (All N, ((unequally_directed_lines (line_connecting T_1 T_0) T_2) => ((unequally_directed_lines (line_connecting T_1 T_0) N) \/ (unequally_directed_lines T_2 N)))) ### DisjTree 90 36 36 % 0.37/0.59 92. (All N, ((unequally_directed_lines T_2 T_2) => ((unequally_directed_lines T_2 N) \/ (unequally_directed_lines T_2 N)))) (All N, ((unequally_directed_lines (line_connecting T_1 T_0) T_2) => ((unequally_directed_lines (line_connecting T_1 T_0) N) \/ (unequally_directed_lines T_2 N)))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (All M, ((unequally_directed_lines (line_connecting T_1 T_0) M) \/ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line M)))) (All M, (All N, ((unequally_directed_lines (line_connecting T_1 T_0) M) => ((unequally_directed_lines (line_connecting T_1 T_0) N) \/ (unequally_directed_lines M N))))) (-. (unequally_directed_lines T_2 (line_connecting T_0 T_1))) (-. (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line (line_connecting 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)))))))) (All M, (All N, (((unequally_directed_lines (line_connecting T_1 T_0) M) /\ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line M))) => (((unequally_directed_lines (line_connecting T_1 T_0) N) /\ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N))))))) (unequally_directed_lines (line_connecting T_1 T_0) T_2) (All M, (All N, ((unequally_directed_lines T_2 M) => ((unequally_directed_lines T_2 N) \/ (unequally_directed_lines M N))))) ### All 91 % 0.37/0.59 93. (All M, (All N, ((unequally_directed_lines T_2 M) => ((unequally_directed_lines T_2 N) \/ (unequally_directed_lines M N))))) (unequally_directed_lines (line_connecting T_1 T_0) T_2) (All M, (All N, (((unequally_directed_lines (line_connecting T_1 T_0) M) /\ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line M))) => (((unequally_directed_lines (line_connecting T_1 T_0) N) /\ (unequally_directed_lines (line_connecting T_1 T_0) (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 (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 (line_connecting T_1 T_0) (reverse_line (line_connecting T_0 T_1)))) (-. (unequally_directed_lines T_2 (line_connecting T_0 T_1))) (All M, (All N, ((unequally_directed_lines (line_connecting T_1 T_0) M) => ((unequally_directed_lines (line_connecting T_1 T_0) N) \/ (unequally_directed_lines M N))))) (All M, ((unequally_directed_lines (line_connecting T_1 T_0) M) \/ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line M)))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (All N, ((unequally_directed_lines (line_connecting T_1 T_0) T_2) => ((unequally_directed_lines (line_connecting T_1 T_0) N) \/ (unequally_directed_lines T_2 N)))) ### All 92 % 0.37/0.59 94. (All L, (All M, (All N, ((unequally_directed_lines L M) => ((unequally_directed_lines L N) \/ (unequally_directed_lines M N)))))) (All N, ((unequally_directed_lines (line_connecting T_1 T_0) T_2) => ((unequally_directed_lines (line_connecting T_1 T_0) N) \/ (unequally_directed_lines T_2 N)))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (All M, ((unequally_directed_lines (line_connecting T_1 T_0) M) \/ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line M)))) (All M, (All N, ((unequally_directed_lines (line_connecting T_1 T_0) M) => ((unequally_directed_lines (line_connecting T_1 T_0) N) \/ (unequally_directed_lines M N))))) (-. (unequally_directed_lines T_2 (line_connecting T_0 T_1))) (-. (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line (line_connecting 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)))))))) (All M, (All N, (((unequally_directed_lines (line_connecting T_1 T_0) M) /\ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line M))) => (((unequally_directed_lines (line_connecting T_1 T_0) N) /\ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N))))))) (unequally_directed_lines (line_connecting T_1 T_0) T_2) ### All 93 % 0.37/0.59 95. ((unequally_directed_lines (line_connecting T_1 T_0) T_2) => ((unequally_directed_lines (line_connecting T_1 T_0) T_2) \/ (unequally_directed_lines T_2 T_2))) (All M, (All N, (((unequally_directed_lines (line_connecting T_1 T_0) M) /\ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line M))) => (((unequally_directed_lines (line_connecting T_1 T_0) N) /\ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N))))))) (-. (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line (line_connecting T_0 T_1)))) (All M, ((unequally_directed_lines (line_connecting T_1 T_0) M) \/ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line M)))) (All N, ((unequally_directed_lines (line_connecting T_1 T_0) T_2) => ((unequally_directed_lines (line_connecting T_1 T_0) N) \/ (unequally_directed_lines T_2 N)))) (unequally_directed_lines (line_connecting T_1 T_0) (line_connecting T_0 T_1)) (All M, (All N, ((unequally_directed_lines (line_connecting T_1 T_0) M) => ((unequally_directed_lines (line_connecting T_1 T_0) 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 (line_connecting T_0 T_1) (reverse_line (line_connecting T_1 T_0)))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (-. (unequally_directed_lines T_2 (line_connecting T_0 T_1))) (All L, (All M, (All N, ((unequally_directed_lines L M) => ((unequally_directed_lines L N) \/ (unequally_directed_lines M N)))))) (All M, ((unequally_directed_lines (line_connecting T_0 T_1) M) \/ (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line M)))) ### DisjTree 58 94 52 % 0.37/0.60 96. (All M, ((unequally_directed_lines (line_connecting T_0 T_1) M) \/ (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line M)))) (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_2 (line_connecting T_0 T_1))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (-. (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line (line_connecting T_1 T_0)))) (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 (line_connecting T_1 T_0) M) => ((unequally_directed_lines (line_connecting T_1 T_0) N) \/ (unequally_directed_lines M N))))) (unequally_directed_lines (line_connecting T_1 T_0) (line_connecting T_0 T_1)) (All N, ((unequally_directed_lines (line_connecting T_1 T_0) T_2) => ((unequally_directed_lines (line_connecting T_1 T_0) N) \/ (unequally_directed_lines T_2 N)))) (All M, ((unequally_directed_lines (line_connecting T_1 T_0) M) \/ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line M)))) (-. (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line (line_connecting T_0 T_1)))) (All M, (All N, (((unequally_directed_lines (line_connecting T_1 T_0) M) /\ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line M))) => (((unequally_directed_lines (line_connecting T_1 T_0) N) /\ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N))))))) ### All 95 % 0.37/0.60 97. (All M, (All N, (((unequally_directed_lines (line_connecting T_1 T_0) M) /\ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line M))) => (((unequally_directed_lines (line_connecting T_1 T_0) N) /\ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line N))) \/ ((unequally_directed_lines M N) /\ (unequally_directed_lines M (reverse_line N))))))) (-. (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line (line_connecting T_0 T_1)))) (All M, ((unequally_directed_lines (line_connecting T_1 T_0) M) \/ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line M)))) (unequally_directed_lines (line_connecting T_1 T_0) (line_connecting T_0 T_1)) (All M, (All N, ((unequally_directed_lines (line_connecting T_1 T_0) M) => ((unequally_directed_lines (line_connecting T_1 T_0) 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 (line_connecting T_0 T_1) (reverse_line (line_connecting T_1 T_0)))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (-. (unequally_directed_lines T_2 (line_connecting T_0 T_1))) (All L, (All M, (All N, ((unequally_directed_lines L M) => ((unequally_directed_lines L N) \/ (unequally_directed_lines M N)))))) (All M, ((unequally_directed_lines (line_connecting T_0 T_1) M) \/ (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line M)))) ### All 96 % 0.37/0.60 98. (All M, ((unequally_directed_lines (line_connecting T_0 T_1) M) \/ (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line M)))) (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_2 (line_connecting T_0 T_1))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (-. (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line (line_connecting T_1 T_0)))) (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 (line_connecting T_1 T_0) M) => ((unequally_directed_lines (line_connecting T_1 T_0) N) \/ (unequally_directed_lines M N))))) (unequally_directed_lines (line_connecting T_1 T_0) (line_connecting T_0 T_1)) (All M, ((unequally_directed_lines (line_connecting T_1 T_0) M) \/ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line M)))) (-. (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line (line_connecting T_0 T_1)))) ### All 97 % 0.37/0.60 99. (-. (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line (line_connecting T_0 T_1)))) (All M, ((unequally_directed_lines (line_connecting T_1 T_0) M) \/ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line M)))) (unequally_directed_lines (line_connecting T_1 T_0) (line_connecting 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 (line_connecting T_0 T_1) (reverse_line (line_connecting T_1 T_0)))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (-. (unequally_directed_lines T_2 (line_connecting T_0 T_1))) (All L, (All M, (All N, ((unequally_directed_lines L M) => ((unequally_directed_lines L N) \/ (unequally_directed_lines M N)))))) (All M, ((unequally_directed_lines (line_connecting T_0 T_1) M) \/ (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line M)))) ### All 98 % 0.37/0.60 100. (All L, (All M, ((unequally_directed_lines L M) \/ (unequally_directed_lines L (reverse_line M))))) (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_2 (line_connecting T_0 T_1))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (-. (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line (line_connecting T_1 T_0)))) (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 (line_connecting T_1 T_0) (line_connecting T_0 T_1)) (All M, ((unequally_directed_lines (line_connecting T_1 T_0) M) \/ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line M)))) (-. (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line (line_connecting T_0 T_1)))) ### All 99 % 0.37/0.60 101. (-. (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line (line_connecting T_0 T_1)))) (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line (line_connecting T_0 T_1))) ### Axiom % 0.37/0.60 102. ((unequally_directed_lines (line_connecting T_1 T_0) (line_connecting T_0 T_1)) \/ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line (line_connecting T_0 T_1)))) (-. (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line (line_connecting T_0 T_1)))) (All M, ((unequally_directed_lines (line_connecting T_1 T_0) M) \/ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line M)))) (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 (line_connecting T_0 T_1) (reverse_line (line_connecting T_1 T_0)))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (-. (unequally_directed_lines T_2 (line_connecting T_0 T_1))) (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, ((unequally_directed_lines L M) \/ (unequally_directed_lines L (reverse_line M))))) ### Or 100 101 % 0.37/0.60 103. (All L, (All M, ((unequally_directed_lines L M) \/ (unequally_directed_lines L (reverse_line M))))) (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_2 (line_connecting T_0 T_1))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (-. (unequally_directed_lines (line_connecting T_0 T_1) (reverse_line (line_connecting T_1 T_0)))) (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, ((unequally_directed_lines (line_connecting T_1 T_0) M) \/ (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line M)))) (-. (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line (line_connecting T_0 T_1)))) ### All 102 % 0.37/0.60 104. (-. (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line (line_connecting 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 (line_connecting T_0 T_1) (reverse_line (line_connecting T_1 T_0)))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (-. (unequally_directed_lines T_2 (line_connecting T_0 T_1))) (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, ((unequally_directed_lines L M) \/ (unequally_directed_lines L (reverse_line M))))) ### All 103 % 0.37/0.60 105. (equally_directed_lines (line_connecting T_0 T_1) (reverse_line (line_connecting T_1 T_0))) (All L, (All M, ((unequally_directed_lines L M) \/ (unequally_directed_lines L (reverse_line M))))) (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_2 (line_connecting T_0 T_1))) (-. (unequally_directed_lines T_2 (line_connecting T_1 T_0))) (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 (line_connecting T_1 T_0) (reverse_line (line_connecting T_0 T_1)))) ### Extension/test/a4_defns 104 % 0.37/0.60 106. (distinct_points T_0 T_1) (-. (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line (line_connecting 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_2 (line_connecting T_1 T_0))) (-. (unequally_directed_lines T_2 (line_connecting T_0 T_1))) (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, ((unequally_directed_lines L M) \/ (unequally_directed_lines L (reverse_line M))))) ### Extension/test/ax9_cons_objs 105 % 0.37/0.60 107. (equally_directed_lines T_2 (line_connecting T_0 T_1)) (All L, (All M, ((unequally_directed_lines L M) \/ (unequally_directed_lines L (reverse_line M))))) (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_2 (line_connecting T_1 T_0))) (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 (line_connecting T_1 T_0) (reverse_line (line_connecting T_0 T_1)))) (distinct_points T_0 T_1) ### Extension/test/a4_defns 106 % 0.37/0.60 108. (before_on_line T_2 T_0 T_1) (-. (unequally_directed_lines (line_connecting T_1 T_0) (reverse_line (line_connecting 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_2 (line_connecting 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 L, (All M, ((unequally_directed_lines L M) \/ (unequally_directed_lines L (reverse_line M))))) ### Extension/test/ax4_defns 107 % 0.37/0.60 109. (equally_directed_lines (line_connecting T_1 T_0) (reverse_line (line_connecting T_0 T_1))) (All L, (All M, ((unequally_directed_lines L M) \/ (unequally_directed_lines L (reverse_line M))))) (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_2 (line_connecting T_1 T_0))) (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)))))))) (before_on_line T_2 T_0 T_1) ### Extension/test/a4_defns 108 % 0.37/0.60 110. (distinct_points T_1 T_0) (before_on_line T_2 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_2 (line_connecting 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 L, (All M, ((unequally_directed_lines L M) \/ (unequally_directed_lines L (reverse_line M))))) ### Extension/test/ax9_cons_objs 109 % 0.37/0.60 111. (equally_directed_lines T_2 (line_connecting T_1 T_0)) (All L, (All M, ((unequally_directed_lines L M) \/ (unequally_directed_lines L (reverse_line M))))) (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)))))))) (before_on_line T_2 T_0 T_1) (distinct_points T_1 T_0) ### Extension/test/a4_defns 110 % 0.37/0.60 112. (before_on_line T_2 T_1 T_0) (before_on_line T_2 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)))))))) (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, ((unequally_directed_lines L M) \/ (unequally_directed_lines L (reverse_line M))))) ### Extension/test/ax4_defns 111 % 0.37/0.60 113. ((before_on_line T_2 T_1 T_0) /\ (before_on_line T_2 T_0 T_1)) (All L, (All M, ((unequally_directed_lines L M) \/ (unequally_directed_lines L (reverse_line M))))) (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)))))))) ### And 112 % 0.37/0.60 114. (-. (-. ((before_on_line T_2 T_1 T_0) /\ (before_on_line T_2 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)))))))) (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, ((unequally_directed_lines L M) \/ (unequally_directed_lines L (reverse_line M))))) ### NotNot 113 % 0.37/0.60 115. (-. (All B, (-. ((before_on_line T_2 T_1 B) /\ (before_on_line T_2 B T_1))))) (All L, (All M, ((unequally_directed_lines L M) \/ (unequally_directed_lines L (reverse_line M))))) (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 114 % 0.37/0.60 116. (-. (All A, (All B, (-. ((before_on_line T_2 A B) /\ (before_on_line T_2 B A)))))) (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)))))) (All L, (All M, ((unequally_directed_lines L M) \/ (unequally_directed_lines L (reverse_line M))))) ### NotAllEx 115 % 0.37/0.60 117. (-. (All L, (All A, (All B, (-. ((before_on_line L A B) /\ (before_on_line L B A))))))) (All L, (All M, ((unequally_directed_lines L M) \/ (unequally_directed_lines L (reverse_line M))))) (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 116 % 0.37/0.60 % SZS output end Proof % 0.37/0.60 (* END-PROOF *) %------------------------------------------------------------------------------