%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : GEO255+1 : TPTP v9.0.0. Bugfixed v6.4.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% 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 : 300s
% DateTime : Sat Jun 21 05:06:09 AM UTC 2025
% Result : Theorem 0.20s 0.46s
% Output : Proof 0.20s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : GEO255+1 : TPTP v9.0.0. Bugfixed v6.4.0.
% 0.12/0.12 % Command : run_E %s %d THM
% 0.12/0.34 % Computer : n012.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu Jun 19 14:42:41 EDT 2025
% 0.12/0.34 % CPUTime :
% 0.20/0.46 % SZS status Theorem
% 0.20/0.46 % SZS output start Proof
% 0.20/0.46 tff(unequally_directed_lines_type, type, (
% 0.20/0.46 unequally_directed_lines: ( $i * $i ) > $o)).
% 0.20/0.46 tff(line_connecting_type, type, (
% 0.20/0.46 line_connecting: ( $i * $i ) > $i)).
% 0.20/0.46 tff(tptp_fun_A_1_type, type, (
% 0.20/0.46 tptp_fun_A_1: $i)).
% 0.20/0.46 tff(tptp_fun_B_0_type, type, (
% 0.20/0.46 tptp_fun_B_0: $i)).
% 0.20/0.46 tff(reverse_line_type, type, (
% 0.20/0.46 reverse_line: $i > $i)).
% 0.20/0.46 tff(tptp_fun_L_2_type, type, (
% 0.20/0.46 tptp_fun_L_2: $i)).
% 0.20/0.46 tff(distinct_points_type, type, (
% 0.20/0.46 distinct_points: ( $i * $i ) > $o)).
% 0.20/0.46 tff(left_apart_point_type, type, (
% 0.20/0.46 left_apart_point: ( $i * $i ) > $o)).
% 0.20/0.46 tff(before_on_line_type, type, (
% 0.20/0.46 before_on_line: ( $i * $i * $i ) > $o)).
% 0.20/0.46 tff(line_type, type, (
% 0.20/0.46 line: $i > $o)).
% 0.20/0.46 tff(left_convergent_lines_type, type, (
% 0.20/0.46 left_convergent_lines: ( $i * $i ) > $o)).
% 0.20/0.46 tff(1,plain,
% 0.20/0.46 (^[L: $i, A: $i, B: $i] : refl((~((unequally_directed_lines(L, line_connecting(A, B)) | left_apart_point(B, reverse_line(L)) | left_apart_point(B, L) | left_apart_point(A, reverse_line(L)) | left_apart_point(A, L) | (~distinct_points(A, B))) <=> before_on_line(L, A, B))) <=> (~((unequally_directed_lines(L, line_connecting(A, B)) | left_apart_point(B, reverse_line(L)) | left_apart_point(B, L) | left_apart_point(A, reverse_line(L)) | left_apart_point(A, L) | (~distinct_points(A, B))) <=> before_on_line(L, A, B))))),
% 0.20/0.46 inference(bind,[status(th)],[])).
% 0.20/0.46 tff(2,plain,
% 0.20/0.46 (![L: $i, A: $i, B: $i] : (~((unequally_directed_lines(L, line_connecting(A, B)) | left_apart_point(B, reverse_line(L)) | left_apart_point(B, L) | left_apart_point(A, reverse_line(L)) | left_apart_point(A, L) | (~distinct_points(A, B))) <=> before_on_line(L, A, B))) <=> ![L: $i, A: $i, B: $i] : (~((unequally_directed_lines(L, line_connecting(A, B)) | left_apart_point(B, reverse_line(L)) | left_apart_point(B, L) | left_apart_point(A, reverse_line(L)) | left_apart_point(A, L) | (~distinct_points(A, B))) <=> before_on_line(L, A, B)))),
% 0.20/0.46 inference(quant_intro,[status(thm)],[1])).
% 0.20/0.46 tff(3,plain,
% 0.20/0.46 (^[L: $i, A: $i, B: $i] : trans(trans(monotonicity(rewrite((distinct_points(A, B) & (~(left_apart_point(A, L) | left_apart_point(A, reverse_line(L)))) & (~(left_apart_point(B, L) | left_apart_point(B, reverse_line(L)))) & (~unequally_directed_lines(L, line_connecting(A, B)))) <=> (~(unequally_directed_lines(L, line_connecting(A, B)) | left_apart_point(B, reverse_line(L)) | left_apart_point(B, L) | left_apart_point(A, reverse_line(L)) | left_apart_point(A, L) | (~distinct_points(A, B))))), ((before_on_line(L, A, B) <=> (distinct_points(A, B) & (~(left_apart_point(A, L) | left_apart_point(A, reverse_line(L)))) & (~(left_apart_point(B, L) | left_apart_point(B, reverse_line(L)))) & (~unequally_directed_lines(L, line_connecting(A, B))))) <=> (before_on_line(L, A, B) <=> (~(unequally_directed_lines(L, line_connecting(A, B)) | left_apart_point(B, reverse_line(L)) | left_apart_point(B, L) | left_apart_point(A, reverse_line(L)) | left_apart_point(A, L) | (~distinct_points(A, B))))))), rewrite((before_on_line(L, A, B) <=> (~(unequally_directed_lines(L, line_connecting(A, B)) | left_apart_point(B, reverse_line(L)) | left_apart_point(B, L) | left_apart_point(A, reverse_line(L)) | left_apart_point(A, L) | (~distinct_points(A, B))))) <=> (~((unequally_directed_lines(L, line_connecting(A, B)) | left_apart_point(B, reverse_line(L)) | left_apart_point(B, L) | left_apart_point(A, reverse_line(L)) | left_apart_point(A, L) | (~distinct_points(A, B))) <=> before_on_line(L, A, B)))), ((before_on_line(L, A, B) <=> (distinct_points(A, B) & (~(left_apart_point(A, L) | left_apart_point(A, reverse_line(L)))) & (~(left_apart_point(B, L) | left_apart_point(B, reverse_line(L)))) & (~unequally_directed_lines(L, line_connecting(A, B))))) <=> (~((unequally_directed_lines(L, line_connecting(A, B)) | left_apart_point(B, reverse_line(L)) | left_apart_point(B, L) | left_apart_point(A, reverse_line(L)) | left_apart_point(A, L) | (~distinct_points(A, B))) <=> before_on_line(L, A, B))))), rewrite((~((unequally_directed_lines(L, line_connecting(A, B)) | left_apart_point(B, reverse_line(L)) | left_apart_point(B, L) | left_apart_point(A, reverse_line(L)) | left_apart_point(A, L) | (~distinct_points(A, B))) <=> before_on_line(L, A, B))) <=> (~((unequally_directed_lines(L, line_connecting(A, B)) | left_apart_point(B, reverse_line(L)) | left_apart_point(B, L) | left_apart_point(A, reverse_line(L)) | left_apart_point(A, L) | (~distinct_points(A, B))) <=> before_on_line(L, A, B)))), ((before_on_line(L, A, B) <=> (distinct_points(A, B) & (~(left_apart_point(A, L) | left_apart_point(A, reverse_line(L)))) & (~(left_apart_point(B, L) | left_apart_point(B, reverse_line(L)))) & (~unequally_directed_lines(L, line_connecting(A, B))))) <=> (~((unequally_directed_lines(L, line_connecting(A, B)) | left_apart_point(B, reverse_line(L)) | left_apart_point(B, L) | left_apart_point(A, reverse_line(L)) | left_apart_point(A, L) | (~distinct_points(A, B))) <=> before_on_line(L, A, B)))))),
% 0.20/0.47 inference(bind,[status(th)],[])).
% 0.20/0.47 tff(4,plain,
% 0.20/0.47 (![L: $i, A: $i, B: $i] : (before_on_line(L, A, B) <=> (distinct_points(A, B) & (~(left_apart_point(A, L) | left_apart_point(A, reverse_line(L)))) & (~(left_apart_point(B, L) | left_apart_point(B, reverse_line(L)))) & (~unequally_directed_lines(L, line_connecting(A, B))))) <=> ![L: $i, A: $i, B: $i] : (~((unequally_directed_lines(L, line_connecting(A, B)) | left_apart_point(B, reverse_line(L)) | left_apart_point(B, L) | left_apart_point(A, reverse_line(L)) | left_apart_point(A, L) | (~distinct_points(A, B))) <=> before_on_line(L, A, B)))),
% 0.20/0.47 inference(quant_intro,[status(thm)],[3])).
% 0.20/0.47 tff(5,plain,
% 0.20/0.47 (![L: $i, A: $i, B: $i] : (before_on_line(L, A, B) <=> (distinct_points(A, B) & (~(left_apart_point(A, L) | left_apart_point(A, reverse_line(L)))) & (~(left_apart_point(B, L) | left_apart_point(B, reverse_line(L)))) & (~unequally_directed_lines(L, line_connecting(A, B))))) <=> ![L: $i, A: $i, B: $i] : (before_on_line(L, A, B) <=> (distinct_points(A, B) & (~(left_apart_point(A, L) | left_apart_point(A, reverse_line(L)))) & (~(left_apart_point(B, L) | left_apart_point(B, reverse_line(L)))) & (~unequally_directed_lines(L, line_connecting(A, B)))))),
% 0.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(6,plain,
% 0.20/0.47 (^[L: $i, A: $i, B: $i] : rewrite((before_on_line(L, A, B) <=> (((distinct_points(A, B) & (~(left_apart_point(A, L) | left_apart_point(A, reverse_line(L))))) & (~(left_apart_point(B, L) | left_apart_point(B, reverse_line(L))))) & (~unequally_directed_lines(L, line_connecting(A, B))))) <=> (before_on_line(L, A, B) <=> (distinct_points(A, B) & (~(left_apart_point(A, L) | left_apart_point(A, reverse_line(L)))) & (~(left_apart_point(B, L) | left_apart_point(B, reverse_line(L)))) & (~unequally_directed_lines(L, line_connecting(A, B))))))),
% 0.20/0.47 inference(bind,[status(th)],[])).
% 0.20/0.47 tff(7,plain,
% 0.20/0.47 (![L: $i, A: $i, B: $i] : (before_on_line(L, A, B) <=> (((distinct_points(A, B) & (~(left_apart_point(A, L) | left_apart_point(A, reverse_line(L))))) & (~(left_apart_point(B, L) | left_apart_point(B, reverse_line(L))))) & (~unequally_directed_lines(L, line_connecting(A, B))))) <=> ![L: $i, A: $i, B: $i] : (before_on_line(L, A, B) <=> (distinct_points(A, B) & (~(left_apart_point(A, L) | left_apart_point(A, reverse_line(L)))) & (~(left_apart_point(B, L) | left_apart_point(B, reverse_line(L)))) & (~unequally_directed_lines(L, line_connecting(A, B)))))),
% 0.20/0.47 inference(quant_intro,[status(thm)],[6])).
% 0.20/0.47 tff(8,axiom,(![L: $i, A: $i, B: $i] : (before_on_line(L, A, B) <=> (((distinct_points(A, B) & (~(left_apart_point(A, L) | left_apart_point(A, reverse_line(L))))) & (~(left_apart_point(B, L) | left_apart_point(B, reverse_line(L))))) & (~unequally_directed_lines(L, line_connecting(A, B)))))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax','bf_def')).
% 0.20/0.47 tff(9,plain,
% 0.20/0.47 (![L: $i, A: $i, B: $i] : (before_on_line(L, A, B) <=> (distinct_points(A, B) & (~(left_apart_point(A, L) | left_apart_point(A, reverse_line(L)))) & (~(left_apart_point(B, L) | left_apart_point(B, reverse_line(L)))) & (~unequally_directed_lines(L, line_connecting(A, B)))))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[8, 7])).
% 0.20/0.47 tff(10,plain,
% 0.20/0.47 (![L: $i, A: $i, B: $i] : (before_on_line(L, A, B) <=> (distinct_points(A, B) & (~(left_apart_point(A, L) | left_apart_point(A, reverse_line(L)))) & (~(left_apart_point(B, L) | left_apart_point(B, reverse_line(L)))) & (~unequally_directed_lines(L, line_connecting(A, B)))))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[9, 5])).
% 0.20/0.47 tff(11,plain,(
% 0.20/0.47 ![L: $i, A: $i, B: $i] : (before_on_line(L, A, B) <=> (distinct_points(A, B) & (~(left_apart_point(A, L) | left_apart_point(A, reverse_line(L)))) & (~(left_apart_point(B, L) | left_apart_point(B, reverse_line(L)))) & (~unequally_directed_lines(L, line_connecting(A, B)))))),
% 0.20/0.47 inference(skolemize,[status(sab)],[10])).
% 0.20/0.47 tff(12,plain,
% 0.20/0.47 (![L: $i, A: $i, B: $i] : (~((unequally_directed_lines(L, line_connecting(A, B)) | left_apart_point(B, reverse_line(L)) | left_apart_point(B, L) | left_apart_point(A, reverse_line(L)) | left_apart_point(A, L) | (~distinct_points(A, B))) <=> before_on_line(L, A, B)))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[11, 4])).
% 0.20/0.47 tff(13,plain,
% 0.20/0.47 (![L: $i, A: $i, B: $i] : (~((unequally_directed_lines(L, line_connecting(A, B)) | left_apart_point(B, reverse_line(L)) | left_apart_point(B, L) | left_apart_point(A, reverse_line(L)) | left_apart_point(A, L) | (~distinct_points(A, B))) <=> before_on_line(L, A, B)))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[12, 2])).
% 0.20/0.47 tff(14,plain,
% 0.20/0.47 ((~![L: $i, A: $i, B: $i] : (~((unequally_directed_lines(L, line_connecting(A, B)) | left_apart_point(B, reverse_line(L)) | left_apart_point(B, L) | left_apart_point(A, reverse_line(L)) | left_apart_point(A, L) | (~distinct_points(A, B))) <=> before_on_line(L, A, B)))) | (~((unequally_directed_lines(L!2, line_connecting(A!1, B!0)) | left_apart_point(B!0, reverse_line(L!2)) | left_apart_point(B!0, L!2) | left_apart_point(A!1, reverse_line(L!2)) | left_apart_point(A!1, L!2) | (~distinct_points(A!1, B!0))) <=> before_on_line(L!2, A!1, B!0)))),
% 0.20/0.47 inference(quant_inst,[status(thm)],[])).
% 0.20/0.47 tff(15,plain,
% 0.20/0.47 (~((unequally_directed_lines(L!2, line_connecting(A!1, B!0)) | left_apart_point(B!0, reverse_line(L!2)) | left_apart_point(B!0, L!2) | left_apart_point(A!1, reverse_line(L!2)) | left_apart_point(A!1, L!2) | (~distinct_points(A!1, B!0))) <=> before_on_line(L!2, A!1, B!0))),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[14, 13])).
% 0.20/0.47 tff(16,plain,
% 0.20/0.47 ((~![L: $i, A: $i, B: $i] : ((~(line(L) & distinct_points(A, B))) | (~(before_on_line(L, A, B) & before_on_line(L, B, A))))) <=> (~![L: $i, A: $i, B: $i] : ((~(line(L) & distinct_points(A, B))) | (~(before_on_line(L, A, B) & before_on_line(L, B, A)))))),
% 0.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(17,plain,
% 0.20/0.47 ((~![L: $i, A: $i, B: $i] : ((line(L) & distinct_points(A, B)) => (~(before_on_line(L, A, B) & before_on_line(L, B, A))))) <=> (~![L: $i, A: $i, B: $i] : ((~(line(L) & distinct_points(A, B))) | (~(before_on_line(L, A, B) & before_on_line(L, B, A)))))),
% 0.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(18,axiom,(~![L: $i, A: $i, B: $i] : ((line(L) & distinct_points(A, B)) => (~(before_on_line(L, A, B) & before_on_line(L, B, A))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','con')).
% 0.20/0.47 tff(19,plain,
% 0.20/0.47 (~![L: $i, A: $i, B: $i] : ((~(line(L) & distinct_points(A, B))) | (~(before_on_line(L, A, B) & before_on_line(L, B, A))))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[18, 17])).
% 0.20/0.47 tff(20,plain,
% 0.20/0.47 (~![L: $i, A: $i, B: $i] : ((~(line(L) & distinct_points(A, B))) | (~(before_on_line(L, A, B) & before_on_line(L, B, A))))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[19, 16])).
% 0.20/0.47 tff(21,plain,
% 0.20/0.47 (~![L: $i, A: $i, B: $i] : ((~(line(L) & distinct_points(A, B))) | (~(before_on_line(L, A, B) & before_on_line(L, B, A))))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[20, 16])).
% 0.20/0.47 tff(22,plain,
% 0.20/0.47 (~![L: $i, A: $i, B: $i] : ((~(line(L) & distinct_points(A, B))) | (~(before_on_line(L, A, B) & before_on_line(L, B, A))))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[21, 16])).
% 0.20/0.47 tff(23,plain,(
% 0.20/0.47 ~((~(line(L!2) & distinct_points(A!1, B!0))) | (~(before_on_line(L!2, A!1, B!0) & before_on_line(L!2, B!0, A!1))))),
% 0.20/0.47 inference(skolemize,[status(sab)],[22])).
% 0.20/0.47 tff(24,plain,
% 0.20/0.47 (before_on_line(L!2, A!1, B!0) & before_on_line(L!2, B!0, A!1)),
% 0.20/0.47 inference(or_elim,[status(thm)],[23])).
% 0.20/0.47 tff(25,plain,
% 0.20/0.47 (before_on_line(L!2, A!1, B!0)),
% 0.20/0.47 inference(and_elim,[status(thm)],[24])).
% 0.20/0.47 tff(26,plain,
% 0.20/0.47 (((unequally_directed_lines(L!2, line_connecting(A!1, B!0)) | left_apart_point(B!0, reverse_line(L!2)) | left_apart_point(B!0, L!2) | left_apart_point(A!1, reverse_line(L!2)) | left_apart_point(A!1, L!2) | (~distinct_points(A!1, B!0))) <=> before_on_line(L!2, A!1, B!0)) | (~(unequally_directed_lines(L!2, line_connecting(A!1, B!0)) | left_apart_point(B!0, reverse_line(L!2)) | left_apart_point(B!0, L!2) | left_apart_point(A!1, reverse_line(L!2)) | left_apart_point(A!1, L!2) | (~distinct_points(A!1, B!0)))) | (~before_on_line(L!2, A!1, B!0))),
% 0.20/0.47 inference(tautology,[status(thm)],[])).
% 0.20/0.47 tff(27,plain,
% 0.20/0.47 (((unequally_directed_lines(L!2, line_connecting(A!1, B!0)) | left_apart_point(B!0, reverse_line(L!2)) | left_apart_point(B!0, L!2) | left_apart_point(A!1, reverse_line(L!2)) | left_apart_point(A!1, L!2) | (~distinct_points(A!1, B!0))) <=> before_on_line(L!2, A!1, B!0)) | (~(unequally_directed_lines(L!2, line_connecting(A!1, B!0)) | left_apart_point(B!0, reverse_line(L!2)) | left_apart_point(B!0, L!2) | left_apart_point(A!1, reverse_line(L!2)) | left_apart_point(A!1, L!2) | (~distinct_points(A!1, B!0))))),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[26, 25])).
% 0.20/0.47 tff(28,plain,
% 0.20/0.47 (~(unequally_directed_lines(L!2, line_connecting(A!1, B!0)) | left_apart_point(B!0, reverse_line(L!2)) | left_apart_point(B!0, L!2) | left_apart_point(A!1, reverse_line(L!2)) | left_apart_point(A!1, L!2) | (~distinct_points(A!1, B!0)))),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[27, 15])).
% 0.20/0.47 tff(29,plain,
% 0.20/0.47 ((unequally_directed_lines(L!2, line_connecting(A!1, B!0)) | left_apart_point(B!0, reverse_line(L!2)) | left_apart_point(B!0, L!2) | left_apart_point(A!1, reverse_line(L!2)) | left_apart_point(A!1, L!2) | (~distinct_points(A!1, B!0))) | (~unequally_directed_lines(L!2, line_connecting(A!1, B!0)))),
% 0.20/0.47 inference(tautology,[status(thm)],[])).
% 0.20/0.47 tff(30,plain,
% 0.20/0.47 (~unequally_directed_lines(L!2, line_connecting(A!1, B!0))),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[29, 28])).
% 0.20/0.47 tff(31,plain,
% 0.20/0.47 (^[L: $i, M: $i, N: $i] : refl((unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M))) <=> (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M))))),
% 0.20/0.47 inference(bind,[status(th)],[])).
% 0.20/0.47 tff(32,plain,
% 0.20/0.47 (![L: $i, M: $i, N: $i] : (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M))) <=> ![L: $i, M: $i, N: $i] : (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M)))),
% 0.20/0.47 inference(quant_intro,[status(thm)],[31])).
% 0.20/0.47 tff(33,plain,
% 0.20/0.47 (![L: $i, M: $i, N: $i] : (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M))) <=> ![L: $i, M: $i, N: $i] : (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M)))),
% 0.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(34,plain,
% 0.20/0.47 (^[L: $i, M: $i, N: $i] : trans(monotonicity(rewrite((unequally_directed_lines(L, N) | unequally_directed_lines(M, N)) <=> (unequally_directed_lines(M, N) | unequally_directed_lines(L, N))), ((unequally_directed_lines(L, M) => (unequally_directed_lines(L, N) | unequally_directed_lines(M, N))) <=> (unequally_directed_lines(L, M) => (unequally_directed_lines(M, N) | unequally_directed_lines(L, N))))), rewrite((unequally_directed_lines(L, M) => (unequally_directed_lines(M, N) | unequally_directed_lines(L, N))) <=> (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M)))), ((unequally_directed_lines(L, M) => (unequally_directed_lines(L, N) | unequally_directed_lines(M, N))) <=> (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M)))))),
% 0.20/0.47 inference(bind,[status(th)],[])).
% 0.20/0.47 tff(35,plain,
% 0.20/0.47 (![L: $i, M: $i, N: $i] : (unequally_directed_lines(L, M) => (unequally_directed_lines(L, N) | unequally_directed_lines(M, N))) <=> ![L: $i, M: $i, N: $i] : (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M)))),
% 0.20/0.47 inference(quant_intro,[status(thm)],[34])).
% 0.20/0.47 tff(36,axiom,(![L: $i, M: $i, N: $i] : (unequally_directed_lines(L, M) => (unequally_directed_lines(L, N) | unequally_directed_lines(M, N)))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax','oag6')).
% 0.20/0.47 tff(37,plain,
% 0.20/0.47 (![L: $i, M: $i, N: $i] : (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M)))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[36, 35])).
% 0.20/0.47 tff(38,plain,
% 0.20/0.47 (![L: $i, M: $i, N: $i] : (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M)))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[37, 33])).
% 0.20/0.47 tff(39,plain,(
% 0.20/0.47 ![L: $i, M: $i, N: $i] : (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M)))),
% 0.20/0.47 inference(skolemize,[status(sab)],[38])).
% 0.20/0.47 tff(40,plain,
% 0.20/0.47 (![L: $i, M: $i, N: $i] : (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M)))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[39, 32])).
% 0.20/0.47 tff(41,plain,
% 0.20/0.47 (((~![L: $i, M: $i, N: $i] : (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M)))) | (unequally_directed_lines(L!2, line_connecting(A!1, B!0)) | (~unequally_directed_lines(L!2, L!2)))) <=> ((~![L: $i, M: $i, N: $i] : (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M)))) | unequally_directed_lines(L!2, line_connecting(A!1, B!0)) | (~unequally_directed_lines(L!2, L!2)))),
% 0.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(42,plain,
% 0.20/0.47 ((unequally_directed_lines(L!2, line_connecting(A!1, B!0)) | unequally_directed_lines(L!2, line_connecting(A!1, B!0)) | (~unequally_directed_lines(L!2, L!2))) <=> (unequally_directed_lines(L!2, line_connecting(A!1, B!0)) | (~unequally_directed_lines(L!2, L!2)))),
% 0.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(43,plain,
% 0.20/0.47 (((~![L: $i, M: $i, N: $i] : (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M)))) | (unequally_directed_lines(L!2, line_connecting(A!1, B!0)) | unequally_directed_lines(L!2, line_connecting(A!1, B!0)) | (~unequally_directed_lines(L!2, L!2)))) <=> ((~![L: $i, M: $i, N: $i] : (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M)))) | (unequally_directed_lines(L!2, line_connecting(A!1, B!0)) | (~unequally_directed_lines(L!2, L!2))))),
% 0.20/0.47 inference(monotonicity,[status(thm)],[42])).
% 0.20/0.47 tff(44,plain,
% 0.20/0.47 (((~![L: $i, M: $i, N: $i] : (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M)))) | (unequally_directed_lines(L!2, line_connecting(A!1, B!0)) | unequally_directed_lines(L!2, line_connecting(A!1, B!0)) | (~unequally_directed_lines(L!2, L!2)))) <=> ((~![L: $i, M: $i, N: $i] : (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M)))) | unequally_directed_lines(L!2, line_connecting(A!1, B!0)) | (~unequally_directed_lines(L!2, L!2)))),
% 0.20/0.47 inference(transitivity,[status(thm)],[43, 41])).
% 0.20/0.47 tff(45,plain,
% 0.20/0.47 ((~![L: $i, M: $i, N: $i] : (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M)))) | (unequally_directed_lines(L!2, line_connecting(A!1, B!0)) | unequally_directed_lines(L!2, line_connecting(A!1, B!0)) | (~unequally_directed_lines(L!2, L!2)))),
% 0.20/0.47 inference(quant_inst,[status(thm)],[])).
% 0.20/0.47 tff(46,plain,
% 0.20/0.47 ((~![L: $i, M: $i, N: $i] : (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M)))) | unequally_directed_lines(L!2, line_connecting(A!1, B!0)) | (~unequally_directed_lines(L!2, L!2))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[45, 44])).
% 0.20/0.47 tff(47,plain,
% 0.20/0.47 (~unequally_directed_lines(L!2, L!2)),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[46, 40, 30])).
% 0.20/0.47 tff(48,plain,
% 0.20/0.47 (line(L!2) & distinct_points(A!1, B!0)),
% 0.20/0.47 inference(or_elim,[status(thm)],[23])).
% 0.20/0.47 tff(49,plain,
% 0.20/0.47 (line(L!2)),
% 0.20/0.47 inference(and_elim,[status(thm)],[48])).
% 0.20/0.47 tff(50,plain,
% 0.20/0.47 (^[L: $i, M: $i] : refl((unequally_directed_lines(L, reverse_line(M)) | unequally_directed_lines(L, M) | (~line(M)) | (~line(L))) <=> (unequally_directed_lines(L, reverse_line(M)) | unequally_directed_lines(L, M) | (~line(M)) | (~line(L))))),
% 0.20/0.47 inference(bind,[status(th)],[])).
% 0.20/0.47 tff(51,plain,
% 0.20/0.47 (![L: $i, M: $i] : (unequally_directed_lines(L, reverse_line(M)) | unequally_directed_lines(L, M) | (~line(M)) | (~line(L))) <=> ![L: $i, M: $i] : (unequally_directed_lines(L, reverse_line(M)) | unequally_directed_lines(L, M) | (~line(M)) | (~line(L)))),
% 0.20/0.47 inference(quant_intro,[status(thm)],[50])).
% 0.20/0.47 tff(52,plain,
% 0.20/0.47 (^[L: $i, M: $i] : trans(monotonicity(trans(monotonicity(rewrite((line(L) & line(M)) <=> (~((~line(M)) | (~line(L))))), ((~(line(L) & line(M))) <=> (~(~((~line(M)) | (~line(L))))))), rewrite((~(~((~line(M)) | (~line(L))))) <=> ((~line(M)) | (~line(L)))), ((~(line(L) & line(M))) <=> ((~line(M)) | (~line(L))))), ((unequally_directed_lines(L, reverse_line(M)) | unequally_directed_lines(L, M) | (~(line(L) & line(M)))) <=> (unequally_directed_lines(L, reverse_line(M)) | unequally_directed_lines(L, M) | ((~line(M)) | (~line(L)))))), rewrite((unequally_directed_lines(L, reverse_line(M)) | unequally_directed_lines(L, M) | ((~line(M)) | (~line(L)))) <=> (unequally_directed_lines(L, reverse_line(M)) | unequally_directed_lines(L, M) | (~line(M)) | (~line(L)))), ((unequally_directed_lines(L, reverse_line(M)) | unequally_directed_lines(L, M) | (~(line(L) & line(M)))) <=> (unequally_directed_lines(L, reverse_line(M)) | unequally_directed_lines(L, M) | (~line(M)) | (~line(L)))))),
% 0.20/0.47 inference(bind,[status(th)],[])).
% 0.20/0.47 tff(53,plain,
% 0.20/0.47 (![L: $i, M: $i] : (unequally_directed_lines(L, reverse_line(M)) | unequally_directed_lines(L, M) | (~(line(L) & line(M)))) <=> ![L: $i, M: $i] : (unequally_directed_lines(L, reverse_line(M)) | unequally_directed_lines(L, M) | (~line(M)) | (~line(L)))),
% 0.20/0.47 inference(quant_intro,[status(thm)],[52])).
% 0.20/0.47 tff(54,plain,
% 0.20/0.47 (![L: $i, M: $i] : (unequally_directed_lines(L, reverse_line(M)) | unequally_directed_lines(L, M) | (~(line(L) & line(M)))) <=> ![L: $i, M: $i] : (unequally_directed_lines(L, reverse_line(M)) | unequally_directed_lines(L, M) | (~(line(L) & line(M))))),
% 0.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(55,plain,
% 0.20/0.47 (^[L: $i, M: $i] : rewrite(((line(L) & line(M)) => (unequally_directed_lines(L, M) | unequally_directed_lines(L, reverse_line(M)))) <=> (unequally_directed_lines(L, reverse_line(M)) | unequally_directed_lines(L, M) | (~(line(L) & line(M)))))),
% 0.20/0.47 inference(bind,[status(th)],[])).
% 0.20/0.47 tff(56,plain,
% 0.20/0.47 (![L: $i, M: $i] : ((line(L) & line(M)) => (unequally_directed_lines(L, M) | unequally_directed_lines(L, reverse_line(M)))) <=> ![L: $i, M: $i] : (unequally_directed_lines(L, reverse_line(M)) | unequally_directed_lines(L, M) | (~(line(L) & line(M))))),
% 0.20/0.47 inference(quant_intro,[status(thm)],[55])).
% 0.20/0.47 tff(57,axiom,(![L: $i, M: $i] : ((line(L) & line(M)) => (unequally_directed_lines(L, M) | unequally_directed_lines(L, reverse_line(M))))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax','oag8')).
% 0.20/0.47 tff(58,plain,
% 0.20/0.47 (![L: $i, M: $i] : (unequally_directed_lines(L, reverse_line(M)) | unequally_directed_lines(L, M) | (~(line(L) & line(M))))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[57, 56])).
% 0.20/0.47 tff(59,plain,
% 0.20/0.47 (![L: $i, M: $i] : (unequally_directed_lines(L, reverse_line(M)) | unequally_directed_lines(L, M) | (~(line(L) & line(M))))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[58, 54])).
% 0.20/0.47 tff(60,plain,(
% 0.20/0.47 ![L: $i, M: $i] : (unequally_directed_lines(L, reverse_line(M)) | unequally_directed_lines(L, M) | (~(line(L) & line(M))))),
% 0.20/0.47 inference(skolemize,[status(sab)],[59])).
% 0.20/0.47 tff(61,plain,
% 0.20/0.47 (![L: $i, M: $i] : (unequally_directed_lines(L, reverse_line(M)) | unequally_directed_lines(L, M) | (~line(M)) | (~line(L)))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[60, 53])).
% 0.20/0.47 tff(62,plain,
% 0.20/0.47 (![L: $i, M: $i] : (unequally_directed_lines(L, reverse_line(M)) | unequally_directed_lines(L, M) | (~line(M)) | (~line(L)))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[61, 51])).
% 0.20/0.47 tff(63,plain,
% 0.20/0.47 (((~![L: $i, M: $i] : (unequally_directed_lines(L, reverse_line(M)) | unequally_directed_lines(L, M) | (~line(M)) | (~line(L)))) | (unequally_directed_lines(L!2, L!2) | (~line(L!2)) | unequally_directed_lines(L!2, reverse_line(L!2)))) <=> ((~![L: $i, M: $i] : (unequally_directed_lines(L, reverse_line(M)) | unequally_directed_lines(L, M) | (~line(M)) | (~line(L)))) | unequally_directed_lines(L!2, L!2) | (~line(L!2)) | unequally_directed_lines(L!2, reverse_line(L!2)))),
% 0.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(64,plain,
% 0.20/0.47 ((unequally_directed_lines(L!2, reverse_line(L!2)) | unequally_directed_lines(L!2, L!2) | (~line(L!2)) | (~line(L!2))) <=> (unequally_directed_lines(L!2, L!2) | (~line(L!2)) | unequally_directed_lines(L!2, reverse_line(L!2)))),
% 0.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(65,plain,
% 0.20/0.47 (((~![L: $i, M: $i] : (unequally_directed_lines(L, reverse_line(M)) | unequally_directed_lines(L, M) | (~line(M)) | (~line(L)))) | (unequally_directed_lines(L!2, reverse_line(L!2)) | unequally_directed_lines(L!2, L!2) | (~line(L!2)) | (~line(L!2)))) <=> ((~![L: $i, M: $i] : (unequally_directed_lines(L, reverse_line(M)) | unequally_directed_lines(L, M) | (~line(M)) | (~line(L)))) | (unequally_directed_lines(L!2, L!2) | (~line(L!2)) | unequally_directed_lines(L!2, reverse_line(L!2))))),
% 0.20/0.47 inference(monotonicity,[status(thm)],[64])).
% 0.20/0.47 tff(66,plain,
% 0.20/0.47 (((~![L: $i, M: $i] : (unequally_directed_lines(L, reverse_line(M)) | unequally_directed_lines(L, M) | (~line(M)) | (~line(L)))) | (unequally_directed_lines(L!2, reverse_line(L!2)) | unequally_directed_lines(L!2, L!2) | (~line(L!2)) | (~line(L!2)))) <=> ((~![L: $i, M: $i] : (unequally_directed_lines(L, reverse_line(M)) | unequally_directed_lines(L, M) | (~line(M)) | (~line(L)))) | unequally_directed_lines(L!2, L!2) | (~line(L!2)) | unequally_directed_lines(L!2, reverse_line(L!2)))),
% 0.20/0.47 inference(transitivity,[status(thm)],[65, 63])).
% 0.20/0.47 tff(67,plain,
% 0.20/0.47 ((~![L: $i, M: $i] : (unequally_directed_lines(L, reverse_line(M)) | unequally_directed_lines(L, M) | (~line(M)) | (~line(L)))) | (unequally_directed_lines(L!2, reverse_line(L!2)) | unequally_directed_lines(L!2, L!2) | (~line(L!2)) | (~line(L!2)))),
% 0.20/0.47 inference(quant_inst,[status(thm)],[])).
% 0.20/0.47 tff(68,plain,
% 0.20/0.47 ((~![L: $i, M: $i] : (unequally_directed_lines(L, reverse_line(M)) | unequally_directed_lines(L, M) | (~line(M)) | (~line(L)))) | unequally_directed_lines(L!2, L!2) | (~line(L!2)) | unequally_directed_lines(L!2, reverse_line(L!2))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[67, 66])).
% 0.20/0.47 tff(69,plain,
% 0.20/0.47 (unequally_directed_lines(L!2, reverse_line(L!2))),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[68, 62, 49, 47])).
% 0.20/0.47 tff(70,plain,
% 0.20/0.47 (((~![L: $i, A: $i, B: $i] : (~((unequally_directed_lines(L, line_connecting(A, B)) | left_apart_point(B, reverse_line(L)) | left_apart_point(B, L) | left_apart_point(A, reverse_line(L)) | left_apart_point(A, L) | (~distinct_points(A, B))) <=> before_on_line(L, A, B)))) | (~((left_apart_point(B!0, reverse_line(L!2)) | left_apart_point(B!0, L!2) | left_apart_point(A!1, reverse_line(L!2)) | left_apart_point(A!1, L!2) | unequally_directed_lines(L!2, line_connecting(B!0, A!1)) | (~distinct_points(B!0, A!1))) <=> before_on_line(L!2, B!0, A!1)))) <=> ((~![L: $i, A: $i, B: $i] : (~((unequally_directed_lines(L, line_connecting(A, B)) | left_apart_point(B, reverse_line(L)) | left_apart_point(B, L) | left_apart_point(A, reverse_line(L)) | left_apart_point(A, L) | (~distinct_points(A, B))) <=> before_on_line(L, A, B)))) | (~((left_apart_point(B!0, reverse_line(L!2)) | left_apart_point(B!0, L!2) | left_apart_point(A!1, reverse_line(L!2)) | left_apart_point(A!1, L!2) | unequally_directed_lines(L!2, line_connecting(B!0, A!1)) | (~distinct_points(B!0, A!1))) <=> before_on_line(L!2, B!0, A!1))))),
% 0.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(71,plain,
% 0.20/0.47 ((~((left_apart_point(B!0, reverse_line(L!2)) | left_apart_point(B!0, L!2) | left_apart_point(A!1, reverse_line(L!2)) | left_apart_point(A!1, L!2) | unequally_directed_lines(L!2, line_connecting(B!0, A!1)) | (~distinct_points(B!0, A!1))) <=> before_on_line(L!2, B!0, A!1))) <=> (~((left_apart_point(B!0, reverse_line(L!2)) | left_apart_point(B!0, L!2) | left_apart_point(A!1, reverse_line(L!2)) | left_apart_point(A!1, L!2) | unequally_directed_lines(L!2, line_connecting(B!0, A!1)) | (~distinct_points(B!0, A!1))) <=> before_on_line(L!2, B!0, A!1)))),
% 0.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(72,plain,
% 0.20/0.47 (((unequally_directed_lines(L!2, line_connecting(B!0, A!1)) | left_apart_point(A!1, reverse_line(L!2)) | left_apart_point(A!1, L!2) | left_apart_point(B!0, reverse_line(L!2)) | left_apart_point(B!0, L!2) | (~distinct_points(B!0, A!1))) <=> before_on_line(L!2, B!0, A!1)) <=> ((left_apart_point(B!0, reverse_line(L!2)) | left_apart_point(B!0, L!2) | left_apart_point(A!1, reverse_line(L!2)) | left_apart_point(A!1, L!2) | unequally_directed_lines(L!2, line_connecting(B!0, A!1)) | (~distinct_points(B!0, A!1))) <=> before_on_line(L!2, B!0, A!1))),
% 0.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(73,plain,
% 0.20/0.47 ((~((unequally_directed_lines(L!2, line_connecting(B!0, A!1)) | left_apart_point(A!1, reverse_line(L!2)) | left_apart_point(A!1, L!2) | left_apart_point(B!0, reverse_line(L!2)) | left_apart_point(B!0, L!2) | (~distinct_points(B!0, A!1))) <=> before_on_line(L!2, B!0, A!1))) <=> (~((left_apart_point(B!0, reverse_line(L!2)) | left_apart_point(B!0, L!2) | left_apart_point(A!1, reverse_line(L!2)) | left_apart_point(A!1, L!2) | unequally_directed_lines(L!2, line_connecting(B!0, A!1)) | (~distinct_points(B!0, A!1))) <=> before_on_line(L!2, B!0, A!1)))),
% 0.20/0.47 inference(monotonicity,[status(thm)],[72])).
% 0.20/0.47 tff(74,plain,
% 0.20/0.47 ((~((unequally_directed_lines(L!2, line_connecting(B!0, A!1)) | left_apart_point(A!1, reverse_line(L!2)) | left_apart_point(A!1, L!2) | left_apart_point(B!0, reverse_line(L!2)) | left_apart_point(B!0, L!2) | (~distinct_points(B!0, A!1))) <=> before_on_line(L!2, B!0, A!1))) <=> (~((left_apart_point(B!0, reverse_line(L!2)) | left_apart_point(B!0, L!2) | left_apart_point(A!1, reverse_line(L!2)) | left_apart_point(A!1, L!2) | unequally_directed_lines(L!2, line_connecting(B!0, A!1)) | (~distinct_points(B!0, A!1))) <=> before_on_line(L!2, B!0, A!1)))),
% 0.20/0.47 inference(transitivity,[status(thm)],[73, 71])).
% 0.20/0.47 tff(75,plain,
% 0.20/0.47 (((~![L: $i, A: $i, B: $i] : (~((unequally_directed_lines(L, line_connecting(A, B)) | left_apart_point(B, reverse_line(L)) | left_apart_point(B, L) | left_apart_point(A, reverse_line(L)) | left_apart_point(A, L) | (~distinct_points(A, B))) <=> before_on_line(L, A, B)))) | (~((unequally_directed_lines(L!2, line_connecting(B!0, A!1)) | left_apart_point(A!1, reverse_line(L!2)) | left_apart_point(A!1, L!2) | left_apart_point(B!0, reverse_line(L!2)) | left_apart_point(B!0, L!2) | (~distinct_points(B!0, A!1))) <=> before_on_line(L!2, B!0, A!1)))) <=> ((~![L: $i, A: $i, B: $i] : (~((unequally_directed_lines(L, line_connecting(A, B)) | left_apart_point(B, reverse_line(L)) | left_apart_point(B, L) | left_apart_point(A, reverse_line(L)) | left_apart_point(A, L) | (~distinct_points(A, B))) <=> before_on_line(L, A, B)))) | (~((left_apart_point(B!0, reverse_line(L!2)) | left_apart_point(B!0, L!2) | left_apart_point(A!1, reverse_line(L!2)) | left_apart_point(A!1, L!2) | unequally_directed_lines(L!2, line_connecting(B!0, A!1)) | (~distinct_points(B!0, A!1))) <=> before_on_line(L!2, B!0, A!1))))),
% 0.20/0.47 inference(monotonicity,[status(thm)],[74])).
% 0.20/0.47 tff(76,plain,
% 0.20/0.47 (((~![L: $i, A: $i, B: $i] : (~((unequally_directed_lines(L, line_connecting(A, B)) | left_apart_point(B, reverse_line(L)) | left_apart_point(B, L) | left_apart_point(A, reverse_line(L)) | left_apart_point(A, L) | (~distinct_points(A, B))) <=> before_on_line(L, A, B)))) | (~((unequally_directed_lines(L!2, line_connecting(B!0, A!1)) | left_apart_point(A!1, reverse_line(L!2)) | left_apart_point(A!1, L!2) | left_apart_point(B!0, reverse_line(L!2)) | left_apart_point(B!0, L!2) | (~distinct_points(B!0, A!1))) <=> before_on_line(L!2, B!0, A!1)))) <=> ((~![L: $i, A: $i, B: $i] : (~((unequally_directed_lines(L, line_connecting(A, B)) | left_apart_point(B, reverse_line(L)) | left_apart_point(B, L) | left_apart_point(A, reverse_line(L)) | left_apart_point(A, L) | (~distinct_points(A, B))) <=> before_on_line(L, A, B)))) | (~((left_apart_point(B!0, reverse_line(L!2)) | left_apart_point(B!0, L!2) | left_apart_point(A!1, reverse_line(L!2)) | left_apart_point(A!1, L!2) | unequally_directed_lines(L!2, line_connecting(B!0, A!1)) | (~distinct_points(B!0, A!1))) <=> before_on_line(L!2, B!0, A!1))))),
% 0.20/0.47 inference(transitivity,[status(thm)],[75, 70])).
% 0.20/0.47 tff(77,plain,
% 0.20/0.47 ((~![L: $i, A: $i, B: $i] : (~((unequally_directed_lines(L, line_connecting(A, B)) | left_apart_point(B, reverse_line(L)) | left_apart_point(B, L) | left_apart_point(A, reverse_line(L)) | left_apart_point(A, L) | (~distinct_points(A, B))) <=> before_on_line(L, A, B)))) | (~((unequally_directed_lines(L!2, line_connecting(B!0, A!1)) | left_apart_point(A!1, reverse_line(L!2)) | left_apart_point(A!1, L!2) | left_apart_point(B!0, reverse_line(L!2)) | left_apart_point(B!0, L!2) | (~distinct_points(B!0, A!1))) <=> before_on_line(L!2, B!0, A!1)))),
% 0.20/0.47 inference(quant_inst,[status(thm)],[])).
% 0.20/0.47 tff(78,plain,
% 0.20/0.47 ((~![L: $i, A: $i, B: $i] : (~((unequally_directed_lines(L, line_connecting(A, B)) | left_apart_point(B, reverse_line(L)) | left_apart_point(B, L) | left_apart_point(A, reverse_line(L)) | left_apart_point(A, L) | (~distinct_points(A, B))) <=> before_on_line(L, A, B)))) | (~((left_apart_point(B!0, reverse_line(L!2)) | left_apart_point(B!0, L!2) | left_apart_point(A!1, reverse_line(L!2)) | left_apart_point(A!1, L!2) | unequally_directed_lines(L!2, line_connecting(B!0, A!1)) | (~distinct_points(B!0, A!1))) <=> before_on_line(L!2, B!0, A!1)))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[77, 76])).
% 0.20/0.47 tff(79,plain,
% 0.20/0.47 (~((left_apart_point(B!0, reverse_line(L!2)) | left_apart_point(B!0, L!2) | left_apart_point(A!1, reverse_line(L!2)) | left_apart_point(A!1, L!2) | unequally_directed_lines(L!2, line_connecting(B!0, A!1)) | (~distinct_points(B!0, A!1))) <=> before_on_line(L!2, B!0, A!1))),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[78, 13])).
% 0.20/0.48 tff(80,plain,
% 0.20/0.48 (before_on_line(L!2, B!0, A!1)),
% 0.20/0.48 inference(and_elim,[status(thm)],[24])).
% 0.20/0.48 tff(81,plain,
% 0.20/0.48 (((left_apart_point(B!0, reverse_line(L!2)) | left_apart_point(B!0, L!2) | left_apart_point(A!1, reverse_line(L!2)) | left_apart_point(A!1, L!2) | unequally_directed_lines(L!2, line_connecting(B!0, A!1)) | (~distinct_points(B!0, A!1))) <=> before_on_line(L!2, B!0, A!1)) | (~(left_apart_point(B!0, reverse_line(L!2)) | left_apart_point(B!0, L!2) | left_apart_point(A!1, reverse_line(L!2)) | left_apart_point(A!1, L!2) | unequally_directed_lines(L!2, line_connecting(B!0, A!1)) | (~distinct_points(B!0, A!1)))) | (~before_on_line(L!2, B!0, A!1))),
% 0.20/0.48 inference(tautology,[status(thm)],[])).
% 0.20/0.48 tff(82,plain,
% 0.20/0.48 (((left_apart_point(B!0, reverse_line(L!2)) | left_apart_point(B!0, L!2) | left_apart_point(A!1, reverse_line(L!2)) | left_apart_point(A!1, L!2) | unequally_directed_lines(L!2, line_connecting(B!0, A!1)) | (~distinct_points(B!0, A!1))) <=> before_on_line(L!2, B!0, A!1)) | (~(left_apart_point(B!0, reverse_line(L!2)) | left_apart_point(B!0, L!2) | left_apart_point(A!1, reverse_line(L!2)) | left_apart_point(A!1, L!2) | unequally_directed_lines(L!2, line_connecting(B!0, A!1)) | (~distinct_points(B!0, A!1))))),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[81, 80])).
% 0.20/0.48 tff(83,plain,
% 0.20/0.48 (~(left_apart_point(B!0, reverse_line(L!2)) | left_apart_point(B!0, L!2) | left_apart_point(A!1, reverse_line(L!2)) | left_apart_point(A!1, L!2) | unequally_directed_lines(L!2, line_connecting(B!0, A!1)) | (~distinct_points(B!0, A!1)))),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[82, 79])).
% 0.20/0.48 tff(84,plain,
% 0.20/0.48 ((left_apart_point(B!0, reverse_line(L!2)) | left_apart_point(B!0, L!2) | left_apart_point(A!1, reverse_line(L!2)) | left_apart_point(A!1, L!2) | unequally_directed_lines(L!2, line_connecting(B!0, A!1)) | (~distinct_points(B!0, A!1))) | (~unequally_directed_lines(L!2, line_connecting(B!0, A!1)))),
% 0.20/0.48 inference(tautology,[status(thm)],[])).
% 0.20/0.48 tff(85,plain,
% 0.20/0.48 (~unequally_directed_lines(L!2, line_connecting(B!0, A!1))),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[84, 83])).
% 0.20/0.48 tff(86,plain,
% 0.20/0.48 (((~![L: $i, M: $i, N: $i] : (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M)))) | (unequally_directed_lines(L!2, line_connecting(B!0, A!1)) | (~unequally_directed_lines(L!2, reverse_line(L!2))) | unequally_directed_lines(reverse_line(L!2), line_connecting(B!0, A!1)))) <=> ((~![L: $i, M: $i, N: $i] : (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M)))) | unequally_directed_lines(L!2, line_connecting(B!0, A!1)) | (~unequally_directed_lines(L!2, reverse_line(L!2))) | unequally_directed_lines(reverse_line(L!2), line_connecting(B!0, A!1)))),
% 0.20/0.48 inference(rewrite,[status(thm)],[])).
% 0.20/0.48 tff(87,plain,
% 0.20/0.48 ((unequally_directed_lines(reverse_line(L!2), line_connecting(B!0, A!1)) | unequally_directed_lines(L!2, line_connecting(B!0, A!1)) | (~unequally_directed_lines(L!2, reverse_line(L!2)))) <=> (unequally_directed_lines(L!2, line_connecting(B!0, A!1)) | (~unequally_directed_lines(L!2, reverse_line(L!2))) | unequally_directed_lines(reverse_line(L!2), line_connecting(B!0, A!1)))),
% 0.20/0.48 inference(rewrite,[status(thm)],[])).
% 0.20/0.48 tff(88,plain,
% 0.20/0.48 (((~![L: $i, M: $i, N: $i] : (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M)))) | (unequally_directed_lines(reverse_line(L!2), line_connecting(B!0, A!1)) | unequally_directed_lines(L!2, line_connecting(B!0, A!1)) | (~unequally_directed_lines(L!2, reverse_line(L!2))))) <=> ((~![L: $i, M: $i, N: $i] : (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M)))) | (unequally_directed_lines(L!2, line_connecting(B!0, A!1)) | (~unequally_directed_lines(L!2, reverse_line(L!2))) | unequally_directed_lines(reverse_line(L!2), line_connecting(B!0, A!1))))),
% 0.20/0.48 inference(monotonicity,[status(thm)],[87])).
% 0.20/0.48 tff(89,plain,
% 0.20/0.48 (((~![L: $i, M: $i, N: $i] : (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M)))) | (unequally_directed_lines(reverse_line(L!2), line_connecting(B!0, A!1)) | unequally_directed_lines(L!2, line_connecting(B!0, A!1)) | (~unequally_directed_lines(L!2, reverse_line(L!2))))) <=> ((~![L: $i, M: $i, N: $i] : (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M)))) | unequally_directed_lines(L!2, line_connecting(B!0, A!1)) | (~unequally_directed_lines(L!2, reverse_line(L!2))) | unequally_directed_lines(reverse_line(L!2), line_connecting(B!0, A!1)))),
% 0.20/0.48 inference(transitivity,[status(thm)],[88, 86])).
% 0.20/0.48 tff(90,plain,
% 0.20/0.48 ((~![L: $i, M: $i, N: $i] : (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M)))) | (unequally_directed_lines(reverse_line(L!2), line_connecting(B!0, A!1)) | unequally_directed_lines(L!2, line_connecting(B!0, A!1)) | (~unequally_directed_lines(L!2, reverse_line(L!2))))),
% 0.20/0.48 inference(quant_inst,[status(thm)],[])).
% 0.20/0.48 tff(91,plain,
% 0.20/0.48 ((~![L: $i, M: $i, N: $i] : (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M)))) | unequally_directed_lines(L!2, line_connecting(B!0, A!1)) | (~unequally_directed_lines(L!2, reverse_line(L!2))) | unequally_directed_lines(reverse_line(L!2), line_connecting(B!0, A!1))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[90, 89])).
% 0.20/0.48 tff(92,plain,
% 0.20/0.48 (unequally_directed_lines(reverse_line(L!2), line_connecting(B!0, A!1))),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[91, 40, 85, 69])).
% 0.20/0.48 tff(93,plain,
% 0.20/0.48 (^[L: $i, M: $i] : refl((~(left_convergent_lines(L, M) | left_convergent_lines(L, reverse_line(M)))) <=> (~(left_convergent_lines(L, M) | left_convergent_lines(L, reverse_line(M)))))),
% 0.20/0.48 inference(bind,[status(th)],[])).
% 0.20/0.48 tff(94,plain,
% 0.20/0.48 (![L: $i, M: $i] : (~(left_convergent_lines(L, M) | left_convergent_lines(L, reverse_line(M)))) <=> ![L: $i, M: $i] : (~(left_convergent_lines(L, M) | left_convergent_lines(L, reverse_line(M))))),
% 0.20/0.48 inference(quant_intro,[status(thm)],[93])).
% 0.20/0.48 tff(95,plain,
% 0.20/0.48 (![L: $i, M: $i] : (~(left_convergent_lines(L, M) | left_convergent_lines(L, reverse_line(M)))) <=> ![L: $i, M: $i] : (~(left_convergent_lines(L, M) | left_convergent_lines(L, reverse_line(M))))),
% 0.20/0.48 inference(rewrite,[status(thm)],[])).
% 0.20/0.48 tff(96,axiom,(![L: $i, M: $i] : (~(left_convergent_lines(L, M) | left_convergent_lines(L, reverse_line(M))))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax','oag11')).
% 0.20/0.48 tff(97,plain,
% 0.20/0.48 (![L: $i, M: $i] : (~(left_convergent_lines(L, M) | left_convergent_lines(L, reverse_line(M))))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[96, 95])).
% 0.20/0.48 tff(98,plain,(
% 0.20/0.48 ![L: $i, M: $i] : (~(left_convergent_lines(L, M) | left_convergent_lines(L, reverse_line(M))))),
% 0.20/0.48 inference(skolemize,[status(sab)],[97])).
% 0.20/0.48 tff(99,plain,
% 0.20/0.48 (![L: $i, M: $i] : (~(left_convergent_lines(L, M) | left_convergent_lines(L, reverse_line(M))))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[98, 94])).
% 0.20/0.48 tff(100,plain,
% 0.20/0.48 ((~![L: $i, M: $i] : (~(left_convergent_lines(L, M) | left_convergent_lines(L, reverse_line(M))))) | (~(left_convergent_lines(reverse_line(L!2), line_connecting(A!1, B!0)) | left_convergent_lines(reverse_line(L!2), reverse_line(line_connecting(A!1, B!0)))))),
% 0.20/0.48 inference(quant_inst,[status(thm)],[])).
% 0.20/0.48 tff(101,plain,
% 0.20/0.48 (~(left_convergent_lines(reverse_line(L!2), line_connecting(A!1, B!0)) | left_convergent_lines(reverse_line(L!2), reverse_line(line_connecting(A!1, B!0))))),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[100, 99])).
% 0.20/0.48 tff(102,plain,
% 0.20/0.48 ((left_convergent_lines(reverse_line(L!2), line_connecting(A!1, B!0)) | left_convergent_lines(reverse_line(L!2), reverse_line(line_connecting(A!1, B!0)))) | (~left_convergent_lines(reverse_line(L!2), reverse_line(line_connecting(A!1, B!0))))),
% 0.20/0.48 inference(tautology,[status(thm)],[])).
% 0.20/0.48 tff(103,plain,
% 0.20/0.48 (~left_convergent_lines(reverse_line(L!2), reverse_line(line_connecting(A!1, B!0)))),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[102, 101])).
% 0.20/0.48 tff(104,plain,
% 0.20/0.48 ((left_convergent_lines(reverse_line(L!2), line_connecting(A!1, B!0)) | left_convergent_lines(reverse_line(L!2), reverse_line(line_connecting(A!1, B!0)))) | (~left_convergent_lines(reverse_line(L!2), line_connecting(A!1, B!0)))),
% 0.20/0.48 inference(tautology,[status(thm)],[])).
% 0.20/0.48 tff(105,plain,
% 0.20/0.48 (~left_convergent_lines(reverse_line(L!2), line_connecting(A!1, B!0))),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[104, 101])).
% 0.20/0.48 tff(106,plain,
% 0.20/0.48 (((~![L: $i, M: $i, N: $i] : (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M)))) | (unequally_directed_lines(L!2, line_connecting(A!1, B!0)) | (~unequally_directed_lines(L!2, reverse_line(L!2))) | unequally_directed_lines(reverse_line(L!2), line_connecting(A!1, B!0)))) <=> ((~![L: $i, M: $i, N: $i] : (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M)))) | unequally_directed_lines(L!2, line_connecting(A!1, B!0)) | (~unequally_directed_lines(L!2, reverse_line(L!2))) | unequally_directed_lines(reverse_line(L!2), line_connecting(A!1, B!0)))),
% 0.20/0.48 inference(rewrite,[status(thm)],[])).
% 0.20/0.48 tff(107,plain,
% 0.20/0.48 ((unequally_directed_lines(reverse_line(L!2), line_connecting(A!1, B!0)) | unequally_directed_lines(L!2, line_connecting(A!1, B!0)) | (~unequally_directed_lines(L!2, reverse_line(L!2)))) <=> (unequally_directed_lines(L!2, line_connecting(A!1, B!0)) | (~unequally_directed_lines(L!2, reverse_line(L!2))) | unequally_directed_lines(reverse_line(L!2), line_connecting(A!1, B!0)))),
% 0.20/0.48 inference(rewrite,[status(thm)],[])).
% 0.20/0.48 tff(108,plain,
% 0.20/0.48 (((~![L: $i, M: $i, N: $i] : (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M)))) | (unequally_directed_lines(reverse_line(L!2), line_connecting(A!1, B!0)) | unequally_directed_lines(L!2, line_connecting(A!1, B!0)) | (~unequally_directed_lines(L!2, reverse_line(L!2))))) <=> ((~![L: $i, M: $i, N: $i] : (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M)))) | (unequally_directed_lines(L!2, line_connecting(A!1, B!0)) | (~unequally_directed_lines(L!2, reverse_line(L!2))) | unequally_directed_lines(reverse_line(L!2), line_connecting(A!1, B!0))))),
% 0.20/0.48 inference(monotonicity,[status(thm)],[107])).
% 0.20/0.48 tff(109,plain,
% 0.20/0.48 (((~![L: $i, M: $i, N: $i] : (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M)))) | (unequally_directed_lines(reverse_line(L!2), line_connecting(A!1, B!0)) | unequally_directed_lines(L!2, line_connecting(A!1, B!0)) | (~unequally_directed_lines(L!2, reverse_line(L!2))))) <=> ((~![L: $i, M: $i, N: $i] : (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M)))) | unequally_directed_lines(L!2, line_connecting(A!1, B!0)) | (~unequally_directed_lines(L!2, reverse_line(L!2))) | unequally_directed_lines(reverse_line(L!2), line_connecting(A!1, B!0)))),
% 0.20/0.48 inference(transitivity,[status(thm)],[108, 106])).
% 0.20/0.48 tff(110,plain,
% 0.20/0.48 ((~![L: $i, M: $i, N: $i] : (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M)))) | (unequally_directed_lines(reverse_line(L!2), line_connecting(A!1, B!0)) | unequally_directed_lines(L!2, line_connecting(A!1, B!0)) | (~unequally_directed_lines(L!2, reverse_line(L!2))))),
% 0.20/0.48 inference(quant_inst,[status(thm)],[])).
% 0.20/0.48 tff(111,plain,
% 0.20/0.48 ((~![L: $i, M: $i, N: $i] : (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M)))) | unequally_directed_lines(L!2, line_connecting(A!1, B!0)) | (~unequally_directed_lines(L!2, reverse_line(L!2))) | unequally_directed_lines(reverse_line(L!2), line_connecting(A!1, B!0))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[110, 109])).
% 0.20/0.48 tff(112,plain,
% 0.20/0.48 (unequally_directed_lines(reverse_line(L!2), line_connecting(A!1, B!0))),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[111, 40, 30, 69])).
% 0.20/0.48 tff(113,plain,
% 0.20/0.48 (^[L: $i, M: $i] : refl((left_convergent_lines(L, reverse_line(M)) | left_convergent_lines(L, M) | (~unequally_directed_lines(L, M)) | (~unequally_directed_lines(L, reverse_line(M)))) <=> (left_convergent_lines(L, reverse_line(M)) | left_convergent_lines(L, M) | (~unequally_directed_lines(L, M)) | (~unequally_directed_lines(L, reverse_line(M)))))),
% 0.20/0.48 inference(bind,[status(th)],[])).
% 0.20/0.48 tff(114,plain,
% 0.20/0.48 (![L: $i, M: $i] : (left_convergent_lines(L, reverse_line(M)) | left_convergent_lines(L, M) | (~unequally_directed_lines(L, M)) | (~unequally_directed_lines(L, reverse_line(M)))) <=> ![L: $i, M: $i] : (left_convergent_lines(L, reverse_line(M)) | left_convergent_lines(L, M) | (~unequally_directed_lines(L, M)) | (~unequally_directed_lines(L, reverse_line(M))))),
% 0.20/0.48 inference(quant_intro,[status(thm)],[113])).
% 0.20/0.48 tff(115,plain,
% 0.20/0.48 (^[L: $i, M: $i] : trans(monotonicity(trans(monotonicity(rewrite((unequally_directed_lines(L, M) & unequally_directed_lines(L, reverse_line(M))) <=> (~((~unequally_directed_lines(L, M)) | (~unequally_directed_lines(L, reverse_line(M)))))), ((~(unequally_directed_lines(L, M) & unequally_directed_lines(L, reverse_line(M)))) <=> (~(~((~unequally_directed_lines(L, M)) | (~unequally_directed_lines(L, reverse_line(M)))))))), rewrite((~(~((~unequally_directed_lines(L, M)) | (~unequally_directed_lines(L, reverse_line(M)))))) <=> ((~unequally_directed_lines(L, M)) | (~unequally_directed_lines(L, reverse_line(M))))), ((~(unequally_directed_lines(L, M) & unequally_directed_lines(L, reverse_line(M)))) <=> ((~unequally_directed_lines(L, M)) | (~unequally_directed_lines(L, reverse_line(M)))))), ((left_convergent_lines(L, reverse_line(M)) | left_convergent_lines(L, M) | (~(unequally_directed_lines(L, M) & unequally_directed_lines(L, reverse_line(M))))) <=> (left_convergent_lines(L, reverse_line(M)) | left_convergent_lines(L, M) | ((~unequally_directed_lines(L, M)) | (~unequally_directed_lines(L, reverse_line(M))))))), rewrite((left_convergent_lines(L, reverse_line(M)) | left_convergent_lines(L, M) | ((~unequally_directed_lines(L, M)) | (~unequally_directed_lines(L, reverse_line(M))))) <=> (left_convergent_lines(L, reverse_line(M)) | left_convergent_lines(L, M) | (~unequally_directed_lines(L, M)) | (~unequally_directed_lines(L, reverse_line(M))))), ((left_convergent_lines(L, reverse_line(M)) | left_convergent_lines(L, M) | (~(unequally_directed_lines(L, M) & unequally_directed_lines(L, reverse_line(M))))) <=> (left_convergent_lines(L, reverse_line(M)) | left_convergent_lines(L, M) | (~unequally_directed_lines(L, M)) | (~unequally_directed_lines(L, reverse_line(M))))))),
% 0.20/0.48 inference(bind,[status(th)],[])).
% 0.20/0.48 tff(116,plain,
% 0.20/0.48 (![L: $i, M: $i] : (left_convergent_lines(L, reverse_line(M)) | left_convergent_lines(L, M) | (~(unequally_directed_lines(L, M) & unequally_directed_lines(L, reverse_line(M))))) <=> ![L: $i, M: $i] : (left_convergent_lines(L, reverse_line(M)) | left_convergent_lines(L, M) | (~unequally_directed_lines(L, M)) | (~unequally_directed_lines(L, reverse_line(M))))),
% 0.20/0.48 inference(quant_intro,[status(thm)],[115])).
% 0.20/0.48 tff(117,plain,
% 0.20/0.48 (![L: $i, M: $i] : (left_convergent_lines(L, reverse_line(M)) | left_convergent_lines(L, M) | (~(unequally_directed_lines(L, M) & unequally_directed_lines(L, reverse_line(M))))) <=> ![L: $i, M: $i] : (left_convergent_lines(L, reverse_line(M)) | left_convergent_lines(L, M) | (~(unequally_directed_lines(L, M) & unequally_directed_lines(L, reverse_line(M)))))),
% 0.20/0.48 inference(rewrite,[status(thm)],[])).
% 0.20/0.48 tff(118,plain,
% 0.20/0.48 (^[L: $i, M: $i] : rewrite(((unequally_directed_lines(L, M) & unequally_directed_lines(L, reverse_line(M))) => (left_convergent_lines(L, M) | left_convergent_lines(L, reverse_line(M)))) <=> (left_convergent_lines(L, reverse_line(M)) | left_convergent_lines(L, M) | (~(unequally_directed_lines(L, M) & unequally_directed_lines(L, reverse_line(M))))))),
% 0.20/0.48 inference(bind,[status(th)],[])).
% 0.20/0.48 tff(119,plain,
% 0.20/0.48 (![L: $i, M: $i] : ((unequally_directed_lines(L, M) & unequally_directed_lines(L, reverse_line(M))) => (left_convergent_lines(L, M) | left_convergent_lines(L, reverse_line(M)))) <=> ![L: $i, M: $i] : (left_convergent_lines(L, reverse_line(M)) | left_convergent_lines(L, M) | (~(unequally_directed_lines(L, M) & unequally_directed_lines(L, reverse_line(M)))))),
% 0.20/0.48 inference(quant_intro,[status(thm)],[118])).
% 0.20/0.48 tff(120,axiom,(![L: $i, M: $i] : ((unequally_directed_lines(L, M) & unequally_directed_lines(L, reverse_line(M))) => (left_convergent_lines(L, M) | left_convergent_lines(L, reverse_line(M))))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax','oag9')).
% 0.20/0.48 tff(121,plain,
% 0.20/0.48 (![L: $i, M: $i] : (left_convergent_lines(L, reverse_line(M)) | left_convergent_lines(L, M) | (~(unequally_directed_lines(L, M) & unequally_directed_lines(L, reverse_line(M)))))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[120, 119])).
% 0.20/0.48 tff(122,plain,
% 0.20/0.48 (![L: $i, M: $i] : (left_convergent_lines(L, reverse_line(M)) | left_convergent_lines(L, M) | (~(unequally_directed_lines(L, M) & unequally_directed_lines(L, reverse_line(M)))))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[121, 117])).
% 0.20/0.48 tff(123,plain,(
% 0.20/0.48 ![L: $i, M: $i] : (left_convergent_lines(L, reverse_line(M)) | left_convergent_lines(L, M) | (~(unequally_directed_lines(L, M) & unequally_directed_lines(L, reverse_line(M)))))),
% 0.20/0.48 inference(skolemize,[status(sab)],[122])).
% 0.20/0.48 tff(124,plain,
% 0.20/0.48 (![L: $i, M: $i] : (left_convergent_lines(L, reverse_line(M)) | left_convergent_lines(L, M) | (~unequally_directed_lines(L, M)) | (~unequally_directed_lines(L, reverse_line(M))))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[123, 116])).
% 0.20/0.48 tff(125,plain,
% 0.20/0.48 (![L: $i, M: $i] : (left_convergent_lines(L, reverse_line(M)) | left_convergent_lines(L, M) | (~unequally_directed_lines(L, M)) | (~unequally_directed_lines(L, reverse_line(M))))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[124, 114])).
% 0.20/0.48 tff(126,plain,
% 0.20/0.48 (((~![L: $i, M: $i] : (left_convergent_lines(L, reverse_line(M)) | left_convergent_lines(L, M) | (~unequally_directed_lines(L, M)) | (~unequally_directed_lines(L, reverse_line(M))))) | (left_convergent_lines(reverse_line(L!2), line_connecting(A!1, B!0)) | left_convergent_lines(reverse_line(L!2), reverse_line(line_connecting(A!1, B!0))) | (~unequally_directed_lines(reverse_line(L!2), reverse_line(line_connecting(A!1, B!0)))) | (~unequally_directed_lines(reverse_line(L!2), line_connecting(A!1, B!0))))) <=> ((~![L: $i, M: $i] : (left_convergent_lines(L, reverse_line(M)) | left_convergent_lines(L, M) | (~unequally_directed_lines(L, M)) | (~unequally_directed_lines(L, reverse_line(M))))) | left_convergent_lines(reverse_line(L!2), line_connecting(A!1, B!0)) | left_convergent_lines(reverse_line(L!2), reverse_line(line_connecting(A!1, B!0))) | (~unequally_directed_lines(reverse_line(L!2), reverse_line(line_connecting(A!1, B!0)))) | (~unequally_directed_lines(reverse_line(L!2), line_connecting(A!1, B!0))))),
% 0.20/0.48 inference(rewrite,[status(thm)],[])).
% 0.20/0.48 tff(127,plain,
% 0.20/0.48 ((left_convergent_lines(reverse_line(L!2), reverse_line(line_connecting(A!1, B!0))) | left_convergent_lines(reverse_line(L!2), line_connecting(A!1, B!0)) | (~unequally_directed_lines(reverse_line(L!2), line_connecting(A!1, B!0))) | (~unequally_directed_lines(reverse_line(L!2), reverse_line(line_connecting(A!1, B!0))))) <=> (left_convergent_lines(reverse_line(L!2), line_connecting(A!1, B!0)) | left_convergent_lines(reverse_line(L!2), reverse_line(line_connecting(A!1, B!0))) | (~unequally_directed_lines(reverse_line(L!2), reverse_line(line_connecting(A!1, B!0)))) | (~unequally_directed_lines(reverse_line(L!2), line_connecting(A!1, B!0))))),
% 0.20/0.48 inference(rewrite,[status(thm)],[])).
% 0.20/0.48 tff(128,plain,
% 0.20/0.48 (((~![L: $i, M: $i] : (left_convergent_lines(L, reverse_line(M)) | left_convergent_lines(L, M) | (~unequally_directed_lines(L, M)) | (~unequally_directed_lines(L, reverse_line(M))))) | (left_convergent_lines(reverse_line(L!2), reverse_line(line_connecting(A!1, B!0))) | left_convergent_lines(reverse_line(L!2), line_connecting(A!1, B!0)) | (~unequally_directed_lines(reverse_line(L!2), line_connecting(A!1, B!0))) | (~unequally_directed_lines(reverse_line(L!2), reverse_line(line_connecting(A!1, B!0)))))) <=> ((~![L: $i, M: $i] : (left_convergent_lines(L, reverse_line(M)) | left_convergent_lines(L, M) | (~unequally_directed_lines(L, M)) | (~unequally_directed_lines(L, reverse_line(M))))) | (left_convergent_lines(reverse_line(L!2), line_connecting(A!1, B!0)) | left_convergent_lines(reverse_line(L!2), reverse_line(line_connecting(A!1, B!0))) | (~unequally_directed_lines(reverse_line(L!2), reverse_line(line_connecting(A!1, B!0)))) | (~unequally_directed_lines(reverse_line(L!2), line_connecting(A!1, B!0)))))),
% 0.20/0.48 inference(monotonicity,[status(thm)],[127])).
% 0.20/0.48 tff(129,plain,
% 0.20/0.48 (((~![L: $i, M: $i] : (left_convergent_lines(L, reverse_line(M)) | left_convergent_lines(L, M) | (~unequally_directed_lines(L, M)) | (~unequally_directed_lines(L, reverse_line(M))))) | (left_convergent_lines(reverse_line(L!2), reverse_line(line_connecting(A!1, B!0))) | left_convergent_lines(reverse_line(L!2), line_connecting(A!1, B!0)) | (~unequally_directed_lines(reverse_line(L!2), line_connecting(A!1, B!0))) | (~unequally_directed_lines(reverse_line(L!2), reverse_line(line_connecting(A!1, B!0)))))) <=> ((~![L: $i, M: $i] : (left_convergent_lines(L, reverse_line(M)) | left_convergent_lines(L, M) | (~unequally_directed_lines(L, M)) | (~unequally_directed_lines(L, reverse_line(M))))) | left_convergent_lines(reverse_line(L!2), line_connecting(A!1, B!0)) | left_convergent_lines(reverse_line(L!2), reverse_line(line_connecting(A!1, B!0))) | (~unequally_directed_lines(reverse_line(L!2), reverse_line(line_connecting(A!1, B!0)))) | (~unequally_directed_lines(reverse_line(L!2), line_connecting(A!1, B!0))))),
% 0.20/0.48 inference(transitivity,[status(thm)],[128, 126])).
% 0.20/0.48 tff(130,plain,
% 0.20/0.48 ((~![L: $i, M: $i] : (left_convergent_lines(L, reverse_line(M)) | left_convergent_lines(L, M) | (~unequally_directed_lines(L, M)) | (~unequally_directed_lines(L, reverse_line(M))))) | (left_convergent_lines(reverse_line(L!2), reverse_line(line_connecting(A!1, B!0))) | left_convergent_lines(reverse_line(L!2), line_connecting(A!1, B!0)) | (~unequally_directed_lines(reverse_line(L!2), line_connecting(A!1, B!0))) | (~unequally_directed_lines(reverse_line(L!2), reverse_line(line_connecting(A!1, B!0)))))),
% 0.20/0.48 inference(quant_inst,[status(thm)],[])).
% 0.20/0.48 tff(131,plain,
% 0.20/0.48 ((~![L: $i, M: $i] : (left_convergent_lines(L, reverse_line(M)) | left_convergent_lines(L, M) | (~unequally_directed_lines(L, M)) | (~unequally_directed_lines(L, reverse_line(M))))) | left_convergent_lines(reverse_line(L!2), line_connecting(A!1, B!0)) | left_convergent_lines(reverse_line(L!2), reverse_line(line_connecting(A!1, B!0))) | (~unequally_directed_lines(reverse_line(L!2), reverse_line(line_connecting(A!1, B!0)))) | (~unequally_directed_lines(reverse_line(L!2), line_connecting(A!1, B!0)))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[130, 129])).
% 0.20/0.48 tff(132,plain,
% 0.20/0.48 (~unequally_directed_lines(reverse_line(L!2), reverse_line(line_connecting(A!1, B!0)))),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[131, 125, 112, 105, 103])).
% 0.20/0.48 tff(133,plain,
% 0.20/0.48 (^[A: $i, B: $i] : refl((~unequally_directed_lines(line_connecting(A, B), reverse_line(line_connecting(B, A)))) <=> (~unequally_directed_lines(line_connecting(A, B), reverse_line(line_connecting(B, A)))))),
% 0.20/0.48 inference(bind,[status(th)],[])).
% 0.20/0.48 tff(134,plain,
% 0.20/0.48 (![A: $i, B: $i] : (~unequally_directed_lines(line_connecting(A, B), reverse_line(line_connecting(B, A)))) <=> ![A: $i, B: $i] : (~unequally_directed_lines(line_connecting(A, B), reverse_line(line_connecting(B, A))))),
% 0.20/0.48 inference(quant_intro,[status(thm)],[133])).
% 0.20/0.48 tff(135,plain,
% 0.20/0.48 (![A: $i, B: $i] : (~unequally_directed_lines(line_connecting(A, B), reverse_line(line_connecting(B, A)))) <=> ![A: $i, B: $i] : (~unequally_directed_lines(line_connecting(A, B), reverse_line(line_connecting(B, A))))),
% 0.20/0.48 inference(rewrite,[status(thm)],[])).
% 0.20/0.48 tff(136,axiom,(![A: $i, B: $i] : (~unequally_directed_lines(line_connecting(A, B), reverse_line(line_connecting(B, A))))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax','oagco9')).
% 0.20/0.48 tff(137,plain,
% 0.20/0.48 (![A: $i, B: $i] : (~unequally_directed_lines(line_connecting(A, B), reverse_line(line_connecting(B, A))))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[136, 135])).
% 0.20/0.48 tff(138,plain,(
% 0.20/0.48 ![A: $i, B: $i] : (~unequally_directed_lines(line_connecting(A, B), reverse_line(line_connecting(B, A))))),
% 0.20/0.48 inference(skolemize,[status(sab)],[137])).
% 0.20/0.48 tff(139,plain,
% 0.20/0.48 (![A: $i, B: $i] : (~unequally_directed_lines(line_connecting(A, B), reverse_line(line_connecting(B, A))))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[138, 134])).
% 0.20/0.48 tff(140,plain,
% 0.20/0.48 ((~![A: $i, B: $i] : (~unequally_directed_lines(line_connecting(A, B), reverse_line(line_connecting(B, A))))) | (~unequally_directed_lines(line_connecting(B!0, A!1), reverse_line(line_connecting(A!1, B!0))))),
% 0.20/0.48 inference(quant_inst,[status(thm)],[])).
% 0.20/0.48 tff(141,plain,
% 0.20/0.48 (~unequally_directed_lines(line_connecting(B!0, A!1), reverse_line(line_connecting(A!1, B!0)))),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[140, 139])).
% 0.20/0.48 tff(142,plain,
% 0.20/0.48 (((~![L: $i, M: $i, N: $i] : (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M)))) | (unequally_directed_lines(line_connecting(B!0, A!1), reverse_line(line_connecting(A!1, B!0))) | (~unequally_directed_lines(reverse_line(L!2), line_connecting(B!0, A!1))) | unequally_directed_lines(reverse_line(L!2), reverse_line(line_connecting(A!1, B!0))))) <=> ((~![L: $i, M: $i, N: $i] : (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M)))) | unequally_directed_lines(line_connecting(B!0, A!1), reverse_line(line_connecting(A!1, B!0))) | (~unequally_directed_lines(reverse_line(L!2), line_connecting(B!0, A!1))) | unequally_directed_lines(reverse_line(L!2), reverse_line(line_connecting(A!1, B!0))))),
% 0.20/0.48 inference(rewrite,[status(thm)],[])).
% 0.20/0.48 tff(143,plain,
% 0.20/0.48 ((unequally_directed_lines(line_connecting(B!0, A!1), reverse_line(line_connecting(A!1, B!0))) | unequally_directed_lines(reverse_line(L!2), reverse_line(line_connecting(A!1, B!0))) | (~unequally_directed_lines(reverse_line(L!2), line_connecting(B!0, A!1)))) <=> (unequally_directed_lines(line_connecting(B!0, A!1), reverse_line(line_connecting(A!1, B!0))) | (~unequally_directed_lines(reverse_line(L!2), line_connecting(B!0, A!1))) | unequally_directed_lines(reverse_line(L!2), reverse_line(line_connecting(A!1, B!0))))),
% 0.20/0.48 inference(rewrite,[status(thm)],[])).
% 0.20/0.48 tff(144,plain,
% 0.20/0.48 (((~![L: $i, M: $i, N: $i] : (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M)))) | (unequally_directed_lines(line_connecting(B!0, A!1), reverse_line(line_connecting(A!1, B!0))) | unequally_directed_lines(reverse_line(L!2), reverse_line(line_connecting(A!1, B!0))) | (~unequally_directed_lines(reverse_line(L!2), line_connecting(B!0, A!1))))) <=> ((~![L: $i, M: $i, N: $i] : (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M)))) | (unequally_directed_lines(line_connecting(B!0, A!1), reverse_line(line_connecting(A!1, B!0))) | (~unequally_directed_lines(reverse_line(L!2), line_connecting(B!0, A!1))) | unequally_directed_lines(reverse_line(L!2), reverse_line(line_connecting(A!1, B!0)))))),
% 0.20/0.48 inference(monotonicity,[status(thm)],[143])).
% 0.20/0.48 tff(145,plain,
% 0.20/0.48 (((~![L: $i, M: $i, N: $i] : (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M)))) | (unequally_directed_lines(line_connecting(B!0, A!1), reverse_line(line_connecting(A!1, B!0))) | unequally_directed_lines(reverse_line(L!2), reverse_line(line_connecting(A!1, B!0))) | (~unequally_directed_lines(reverse_line(L!2), line_connecting(B!0, A!1))))) <=> ((~![L: $i, M: $i, N: $i] : (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M)))) | unequally_directed_lines(line_connecting(B!0, A!1), reverse_line(line_connecting(A!1, B!0))) | (~unequally_directed_lines(reverse_line(L!2), line_connecting(B!0, A!1))) | unequally_directed_lines(reverse_line(L!2), reverse_line(line_connecting(A!1, B!0))))),
% 0.20/0.48 inference(transitivity,[status(thm)],[144, 142])).
% 0.20/0.48 tff(146,plain,
% 0.20/0.48 ((~![L: $i, M: $i, N: $i] : (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M)))) | (unequally_directed_lines(line_connecting(B!0, A!1), reverse_line(line_connecting(A!1, B!0))) | unequally_directed_lines(reverse_line(L!2), reverse_line(line_connecting(A!1, B!0))) | (~unequally_directed_lines(reverse_line(L!2), line_connecting(B!0, A!1))))),
% 0.20/0.48 inference(quant_inst,[status(thm)],[])).
% 0.20/0.48 tff(147,plain,
% 0.20/0.48 ((~![L: $i, M: $i, N: $i] : (unequally_directed_lines(M, N) | unequally_directed_lines(L, N) | (~unequally_directed_lines(L, M)))) | unequally_directed_lines(line_connecting(B!0, A!1), reverse_line(line_connecting(A!1, B!0))) | (~unequally_directed_lines(reverse_line(L!2), line_connecting(B!0, A!1))) | unequally_directed_lines(reverse_line(L!2), reverse_line(line_connecting(A!1, B!0)))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[146, 145])).
% 0.20/0.48 tff(148,plain,
% 0.20/0.48 ($false),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[147, 40, 141, 132, 92])).
% 0.20/0.48 % SZS output end Proof
% 0.20/0.49 % E exiting
%------------------------------------------------------------------------------