%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : GEO212+1 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n022.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:10 EDT 2022 % Result : Theorem 8.09s 8.31s % Output : Proof 8.44s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : GEO212+1 : TPTP v8.1.0. Released v3.3.0. % 0.07/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.14/0.34 % Computer : n022.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 600 % 0.14/0.34 % DateTime : Sat Jun 18 00:03:02 EDT 2022 % 0.14/0.34 % CPUTime : % 8.09/8.31 % SZS status Theorem % 8.09/8.31 (* PROOF-FOUND *) % 8.09/8.31 (* BEGIN-PROOF *) % 8.09/8.31 % SZS output start Proof % 8.09/8.31 1. (convergent_lines T_0 T_0) (-. (convergent_lines T_0 T_0)) ### Axiom % 8.09/8.31 2. (All X, (-. (convergent_lines X X))) (convergent_lines T_0 T_0) ### All 1 % 8.09/8.31 3. (convergent_lines T_0 T_1) (-. (convergent_lines T_0 T_1)) ### Axiom % 8.09/8.31 4. (convergent_lines T_0 T_2) (-. (convergent_lines T_0 T_2)) ### Axiom % 8.09/8.31 5. (-. (convergent_lines T_0 T_0)) (convergent_lines T_0 T_0) ### Axiom % 8.09/8.31 6. (-. (convergent_lines T_2 T_0)) (convergent_lines T_2 T_0) ### Axiom % 8.09/8.31 7. ((convergent_lines T_0 T_2) => ((convergent_lines T_0 T_0) \/ (convergent_lines T_2 T_0))) (-. (convergent_lines T_2 T_0)) (-. (convergent_lines T_0 T_0)) (convergent_lines T_0 T_2) ### DisjTree 4 5 6 % 8.09/8.31 8. (All Z, ((convergent_lines T_0 T_2) => ((convergent_lines T_0 Z) \/ (convergent_lines T_2 Z)))) (convergent_lines T_0 T_2) (-. (convergent_lines T_0 T_0)) (-. (convergent_lines T_2 T_0)) ### All 7 % 8.09/8.31 9. (All Y, (All Z, ((convergent_lines T_0 Y) => ((convergent_lines T_0 Z) \/ (convergent_lines Y Z))))) (-. (convergent_lines T_2 T_0)) (-. (convergent_lines T_0 T_0)) (convergent_lines T_0 T_2) ### All 8 % 8.09/8.31 10. (convergent_lines T_1 T_2) (-. (convergent_lines T_1 T_2)) ### Axiom % 8.09/8.31 11. (-. (convergent_lines T_1 T_1)) (convergent_lines T_1 T_1) ### Axiom % 8.09/8.31 12. (-. (convergent_lines T_2 T_1)) (convergent_lines T_2 T_1) ### Axiom % 8.09/8.31 13. ((convergent_lines T_1 T_2) => ((convergent_lines T_1 T_1) \/ (convergent_lines T_2 T_1))) (-. (convergent_lines T_2 T_1)) (-. (convergent_lines T_1 T_1)) (convergent_lines T_1 T_2) ### DisjTree 10 11 12 % 8.09/8.31 14. (All Z, ((convergent_lines T_1 T_2) => ((convergent_lines T_1 Z) \/ (convergent_lines T_2 Z)))) (convergent_lines T_1 T_2) (-. (convergent_lines T_1 T_1)) (-. (convergent_lines T_2 T_1)) ### All 13 % 8.09/8.31 15. (All Y, (All Z, ((convergent_lines T_1 Y) => ((convergent_lines T_1 Z) \/ (convergent_lines Y Z))))) (-. (convergent_lines T_2 T_1)) (-. (convergent_lines T_1 T_1)) (convergent_lines T_1 T_2) ### All 14 % 8.09/8.31 16. ((convergent_lines T_0 T_1) => ((convergent_lines T_0 T_2) \/ (convergent_lines T_1 T_2))) (-. (convergent_lines T_1 T_1)) (-. (convergent_lines T_2 T_1)) (All Y, (All Z, ((convergent_lines T_1 Y) => ((convergent_lines T_1 Z) \/ (convergent_lines Y Z))))) (-. (convergent_lines T_0 T_0)) (-. (convergent_lines T_2 T_0)) (All Y, (All Z, ((convergent_lines T_0 Y) => ((convergent_lines T_0 Z) \/ (convergent_lines Y Z))))) (convergent_lines T_0 T_1) ### DisjTree 3 9 15 % 8.09/8.31 17. (All Z, ((convergent_lines T_0 T_1) => ((convergent_lines T_0 Z) \/ (convergent_lines T_1 Z)))) (convergent_lines T_0 T_1) (All Y, (All Z, ((convergent_lines T_0 Y) => ((convergent_lines T_0 Z) \/ (convergent_lines Y Z))))) (-. (convergent_lines T_2 T_0)) (-. (convergent_lines T_0 T_0)) (All Y, (All Z, ((convergent_lines T_1 Y) => ((convergent_lines T_1 Z) \/ (convergent_lines Y Z))))) (-. (convergent_lines T_2 T_1)) (-. (convergent_lines T_1 T_1)) ### All 16 % 8.09/8.31 18. (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (-. (convergent_lines T_1 T_1)) (-. (convergent_lines T_2 T_1)) (-. (convergent_lines T_0 T_0)) (-. (convergent_lines T_2 T_0)) (All Y, (All Z, ((convergent_lines T_0 Y) => ((convergent_lines T_0 Z) \/ (convergent_lines Y Z))))) (convergent_lines T_0 T_1) (All Z, ((convergent_lines T_0 T_1) => ((convergent_lines T_0 Z) \/ (convergent_lines T_1 Z)))) ### All 17 % 8.09/8.31 19. (unorthogonal_lines T_0 T_0) (-. (unorthogonal_lines T_0 T_0)) ### Axiom % 8.09/8.31 20. (-. (unorthogonal_lines T_0 T_1)) (unorthogonal_lines T_0 T_1) ### Axiom % 8.09/8.31 21. ((convergent_lines T_0 T_1) /\ (unorthogonal_lines T_0 T_1)) (-. (unorthogonal_lines T_0 T_1)) ### And 20 % 8.09/8.31 22. (((convergent_lines T_0 T_0) /\ (unorthogonal_lines T_0 T_0)) => (((convergent_lines T_0 T_1) /\ (unorthogonal_lines T_0 T_1)) \/ ((convergent_lines T_0 T_1) /\ (unorthogonal_lines T_0 T_1)))) (-. (unorthogonal_lines T_0 T_1)) (unorthogonal_lines T_0 T_0) (All Z, ((convergent_lines T_0 T_1) => ((convergent_lines T_0 Z) \/ (convergent_lines T_1 Z)))) (convergent_lines T_0 T_1) (All Y, (All Z, ((convergent_lines T_0 Y) => ((convergent_lines T_0 Z) \/ (convergent_lines Y Z))))) (-. (convergent_lines T_2 T_0)) (-. (convergent_lines T_2 T_1)) (-. (convergent_lines T_1 T_1)) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) ### DisjTree 18 19 21 21 % 8.09/8.31 23. (All N, (((convergent_lines T_0 T_0) /\ (unorthogonal_lines T_0 T_0)) => (((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N)) \/ ((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N))))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (-. (convergent_lines T_1 T_1)) (-. (convergent_lines T_2 T_1)) (-. (convergent_lines T_2 T_0)) (All Y, (All Z, ((convergent_lines T_0 Y) => ((convergent_lines T_0 Z) \/ (convergent_lines Y Z))))) (convergent_lines T_0 T_1) (All Z, ((convergent_lines T_0 T_1) => ((convergent_lines T_0 Z) \/ (convergent_lines T_1 Z)))) (unorthogonal_lines T_0 T_0) (-. (unorthogonal_lines T_0 T_1)) ### All 22 % 8.09/8.31 24. (All M, (All N, (((convergent_lines T_0 M) /\ (unorthogonal_lines T_0 M)) => (((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N)))))) (-. (unorthogonal_lines T_0 T_1)) (unorthogonal_lines T_0 T_0) (All Z, ((convergent_lines T_0 T_1) => ((convergent_lines T_0 Z) \/ (convergent_lines T_1 Z)))) (convergent_lines T_0 T_1) (All Y, (All Z, ((convergent_lines T_0 Y) => ((convergent_lines T_0 Z) \/ (convergent_lines Y Z))))) (-. (convergent_lines T_2 T_0)) (-. (convergent_lines T_2 T_1)) (-. (convergent_lines T_1 T_1)) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) ### All 23 % 8.09/8.31 25. (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (-. (convergent_lines T_1 T_1)) (-. (convergent_lines T_2 T_1)) (-. (convergent_lines T_2 T_0)) (All Y, (All Z, ((convergent_lines T_0 Y) => ((convergent_lines T_0 Z) \/ (convergent_lines Y Z))))) (convergent_lines T_0 T_1) (All Z, ((convergent_lines T_0 T_1) => ((convergent_lines T_0 Z) \/ (convergent_lines T_1 Z)))) (unorthogonal_lines T_0 T_0) (-. (unorthogonal_lines T_0 T_1)) ### All 24 % 8.09/8.31 26. (-. (unorthogonal_lines T_0 T_1)) (unorthogonal_lines T_0 T_0) (convergent_lines T_0 T_1) (All Y, (All Z, ((convergent_lines T_0 Y) => ((convergent_lines T_0 Z) \/ (convergent_lines Y Z))))) (-. (convergent_lines T_2 T_0)) (-. (convergent_lines T_2 T_1)) (-. (convergent_lines T_1 T_1)) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) ### All 25 % 8.09/8.31 27. (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (-. (convergent_lines T_1 T_1)) (-. (convergent_lines T_2 T_1)) (-. (convergent_lines T_2 T_0)) (convergent_lines T_0 T_1) (unorthogonal_lines T_0 T_0) (-. (unorthogonal_lines T_0 T_1)) ### All 26 % 8.09/8.31 28. ((convergent_lines T_0 T_0) \/ (unorthogonal_lines T_0 T_0)) (-. (unorthogonal_lines T_0 T_1)) (convergent_lines T_0 T_1) (-. (convergent_lines T_2 T_0)) (-. (convergent_lines T_2 T_1)) (-. (convergent_lines T_1 T_1)) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (All X, (-. (convergent_lines X X))) ### Or 2 27 % 8.09/8.31 29. (All M, ((convergent_lines T_0 M) \/ (unorthogonal_lines T_0 M))) (All X, (-. (convergent_lines X X))) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (-. (convergent_lines T_1 T_1)) (-. (convergent_lines T_2 T_1)) (-. (convergent_lines T_2 T_0)) (convergent_lines T_0 T_1) (-. (unorthogonal_lines T_0 T_1)) ### All 28 % 8.44/8.61 30. (-. (unorthogonal_lines T_0 T_1)) (unorthogonal_lines T_0 T_1) ### Axiom % 8.44/8.61 31. ((convergent_lines T_0 T_1) \/ (unorthogonal_lines T_0 T_1)) (-. (unorthogonal_lines T_0 T_1)) (-. (convergent_lines T_2 T_0)) (-. (convergent_lines T_2 T_1)) (-. (convergent_lines T_1 T_1)) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (All X, (-. (convergent_lines X X))) (All M, ((convergent_lines T_0 M) \/ (unorthogonal_lines T_0 M))) ### Or 29 30 % 8.44/8.61 32. (All M, ((convergent_lines T_0 M) \/ (unorthogonal_lines T_0 M))) (All X, (-. (convergent_lines X X))) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (-. (convergent_lines T_1 T_1)) (-. (convergent_lines T_2 T_1)) (-. (convergent_lines T_2 T_0)) (-. (unorthogonal_lines T_0 T_1)) ### All 31 % 8.44/8.61 33. (unorthogonal_lines T_2 T_0) (-. (unorthogonal_lines T_2 T_0)) ### Axiom % 8.44/8.61 34. (-. (convergent_lines T_2 T_1)) (convergent_lines T_2 T_1) ### Axiom % 8.44/8.61 35. ((convergent_lines T_2 T_1) /\ (unorthogonal_lines T_2 T_1)) (-. (convergent_lines T_2 T_1)) ### And 34 % 8.44/8.61 36. (((convergent_lines T_2 T_0) /\ (unorthogonal_lines T_2 T_0)) => (((convergent_lines T_2 T_1) /\ (unorthogonal_lines T_2 T_1)) \/ ((convergent_lines T_0 T_1) /\ (unorthogonal_lines T_0 T_1)))) (unorthogonal_lines T_2 T_0) (-. (unorthogonal_lines T_0 T_1)) (-. (convergent_lines T_2 T_1)) (-. (convergent_lines T_1 T_1)) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (All X, (-. (convergent_lines X X))) (All M, ((convergent_lines T_0 M) \/ (unorthogonal_lines T_0 M))) ### DisjTree 32 33 35 21 % 8.44/8.61 37. (All N, (((convergent_lines T_2 T_0) /\ (unorthogonal_lines T_2 T_0)) => (((convergent_lines T_2 N) /\ (unorthogonal_lines T_2 N)) \/ ((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N))))) (All M, ((convergent_lines T_0 M) \/ (unorthogonal_lines T_0 M))) (All X, (-. (convergent_lines X X))) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (-. (convergent_lines T_1 T_1)) (-. (convergent_lines T_2 T_1)) (-. (unorthogonal_lines T_0 T_1)) (unorthogonal_lines T_2 T_0) ### All 36 % 8.44/8.61 38. (All L, (All M, ((convergent_lines L M) \/ (unorthogonal_lines L M)))) (unorthogonal_lines T_2 T_0) (-. (unorthogonal_lines T_0 T_1)) (-. (convergent_lines T_2 T_1)) (-. (convergent_lines T_1 T_1)) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (All X, (-. (convergent_lines X X))) (All N, (((convergent_lines T_2 T_0) /\ (unorthogonal_lines T_2 T_0)) => (((convergent_lines T_2 N) /\ (unorthogonal_lines T_2 N)) \/ ((convergent_lines T_0 N) /\ (unorthogonal_lines T_0 N))))) ### All 37 % 8.44/8.61 39. (All M, (All N, (((convergent_lines T_2 M) /\ (unorthogonal_lines T_2 M)) => (((convergent_lines T_2 N) /\ (unorthogonal_lines T_2 N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N)))))) (All X, (-. (convergent_lines X X))) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (-. (convergent_lines T_1 T_1)) (-. (convergent_lines T_2 T_1)) (-. (unorthogonal_lines T_0 T_1)) (unorthogonal_lines T_2 T_0) (All L, (All M, ((convergent_lines L M) \/ (unorthogonal_lines L M)))) ### All 38 % 8.44/8.61 40. (All L, (All M, ((convergent_lines L M) \/ (unorthogonal_lines L M)))) (unorthogonal_lines T_2 T_0) (-. (unorthogonal_lines T_0 T_1)) (-. (convergent_lines T_2 T_1)) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (All X, (-. (convergent_lines X X))) (All M, (All N, (((convergent_lines T_2 M) /\ (unorthogonal_lines T_2 M)) => (((convergent_lines T_2 N) /\ (unorthogonal_lines T_2 N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N)))))) ### All 39 % 8.44/8.61 41. (All X, (-. (convergent_lines X X))) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (-. (convergent_lines T_2 T_1)) (-. (unorthogonal_lines T_0 T_1)) (unorthogonal_lines T_2 T_0) (All L, (All M, ((convergent_lines L M) \/ (unorthogonal_lines L M)))) ### All 40 % 8.44/8.61 42. (-. ((unorthogonal_lines T_2 T_0) => ((convergent_lines T_2 T_1) \/ (unorthogonal_lines T_0 T_1)))) (All L, (All M, ((convergent_lines L M) \/ (unorthogonal_lines L M)))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (All X, (-. (convergent_lines X X))) ### ConjTree 41 % 8.44/8.61 43. (-. (All N, ((unorthogonal_lines T_2 T_0) => ((convergent_lines T_2 N) \/ (unorthogonal_lines T_0 N))))) (All X, (-. (convergent_lines X X))) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (All L, (All M, ((convergent_lines L M) \/ (unorthogonal_lines L M)))) ### NotAllEx 42 % 8.44/8.61 44. (-. (All M, (All N, ((unorthogonal_lines T_2 M) => ((convergent_lines T_2 N) \/ (unorthogonal_lines M N)))))) (All L, (All M, ((convergent_lines L M) \/ (unorthogonal_lines L M)))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (All X, (-. (convergent_lines X X))) ### NotAllEx 43 % 8.44/8.61 45. (-. (All L, (All M, (All N, ((unorthogonal_lines L M) => ((convergent_lines L N) \/ (unorthogonal_lines M N))))))) (All X, (-. (convergent_lines X X))) (All L, (All M, (All N, (((convergent_lines L M) /\ (unorthogonal_lines L M)) => (((convergent_lines L N) /\ (unorthogonal_lines L N)) \/ ((convergent_lines M N) /\ (unorthogonal_lines M N))))))) (All X, (All Y, (All Z, ((convergent_lines X Y) => ((convergent_lines X Z) \/ (convergent_lines Y Z)))))) (All L, (All M, ((convergent_lines L M) \/ (unorthogonal_lines L M)))) ### NotAllEx 44 % 8.44/8.61 % SZS output end Proof % 8.44/8.61 (* END-PROOF *) %------------------------------------------------------------------------------