%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : GEO262+3 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n020.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 05:04:18 EDT 2022
% Result : Theorem 0.35s 1.42s
% Output : Proof 0.35s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GEO262+3 : TPTP v8.1.0. Released v4.0.0.
% 0.11/0.13 % Command : leancop_casc.sh %s %d
% 0.13/0.34 % Computer : n020.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Sat Jun 18 04:28:34 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.35/1.42 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.35/1.43 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.35/1.43
% 0.35/1.43 %-----------------------------------------------------
% 0.35/1.43 fof(con, conjecture, ! [_45019, _45022, _45025, _45028, _45031, _45034] : (between_on_line(_45019, _45028, _45031, _45034) & convergent_lines(_45019, _45022) & incident_point_and_line(_45031, _45022) & convergent_lines(_45019, _45025) & convergent_lines(_45022, _45025) & incident_point_and_line(_45031, _45025) => between_on_line(_45022, intersection_point(_45022, parallel_through_point(_45025, _45028)), _45031, intersection_point(_45022, parallel_through_point(_45025, _45034)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', con)).
% 0.35/1.43 fof(a1_defns, axiom, ! [_45446, _45449] : (unequally_directed_opposite_lines(_45446, _45449) <=> unequally_directed_lines(_45446, reverse_line(_45449))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO009+0.ax', a1_defns)).
% 0.35/1.43 fof(a4_defns, axiom, ! [_45606, _45609] : (equally_directed_lines(_45606, _45609) <=> ~ unequally_directed_lines(_45606, _45609)), file('/export/starexec/sandbox2/benchmark/Axioms/GEO009+0.ax', a4_defns)).
% 0.35/1.43 fof(a7_defns, axiom, ! [_45776, _45779] : (convergent_lines(_45776, _45779) <=> unequally_directed_lines(_45776, _45779) & unequally_directed_opposite_lines(_45776, _45779)), file('/export/starexec/sandbox2/benchmark/Axioms/GEO009+0.ax', a7_defns)).
% 0.35/1.43 fof(ax9_basics, axiom, ! [_45991, _45994] : (unequally_directed_lines(_45991, _45994) & unequally_directed_lines(_45991, reverse_line(_45994)) => left_convergent_lines(_45991, _45994) | left_convergent_lines(_45991, reverse_line(_45994))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO009+0.ax', ax9_basics)).
% 0.35/1.43 fof(ax11_basics, axiom, ! [_46213, _46216] : ~ (left_convergent_lines(_46213, _46216) | left_convergent_lines(_46213, reverse_line(_46216))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO009+0.ax', ax11_basics)).
% 0.35/1.43
% 0.35/1.43 cnf(1, plain, [-(convergent_lines(1 ^ [], 2 ^ []))], clausify(con)).
% 0.35/1.43 cnf(2, plain, [unequally_directed_opposite_lines(_12115, _12162), -(unequally_directed_lines(_12115, reverse_line(_12162)))], clausify(a1_defns)).
% 0.35/1.43 cnf(3, plain, [equally_directed_lines(_13105, _13152), unequally_directed_lines(_13105, _13152)], clausify(a4_defns)).
% 0.35/1.43 cnf(4, plain, [-(equally_directed_lines(_13105, _13152)), -(unequally_directed_lines(_13105, _13152))], clausify(a4_defns)).
% 0.35/1.43 cnf(5, plain, [convergent_lines(_14161, _14212), -(unequally_directed_lines(_14161, _14212))], clausify(a7_defns)).
% 0.35/1.43 cnf(6, plain, [convergent_lines(_14161, _14212), -(unequally_directed_opposite_lines(_14161, _14212))], clausify(a7_defns)).
% 0.35/1.43 cnf(7, plain, [unequally_directed_lines(_20096, reverse_line(_20157)), unequally_directed_lines(_20096, _20157), -(left_convergent_lines(_20096, _20157)), -(left_convergent_lines(_20096, reverse_line(_20157)))], clausify(ax9_basics)).
% 0.35/1.43 cnf(8, plain, [left_convergent_lines(_20968, _21017)], clausify(ax11_basics)).
% 0.35/1.43
% 0.35/1.43 cnf('1',plain,[equally_directed_lines(1 ^ [], reverse_line(2 ^ [])), unequally_directed_lines(1 ^ [], reverse_line(2 ^ []))],start(3,bind([[_13105, _13152], [1 ^ [], reverse_line(2 ^ [])]]))).
% 0.35/1.43 cnf('1.1',plain,[-(equally_directed_lines(1 ^ [], reverse_line(2 ^ []))), -(unequally_directed_lines(1 ^ [], reverse_line(2 ^ [])))],extension(4,bind([[_13105, _13152], [1 ^ [], reverse_line(2 ^ [])]]))).
% 0.35/1.43 cnf('1.1.1',plain,[unequally_directed_lines(1 ^ [], reverse_line(2 ^ [])), unequally_directed_lines(1 ^ [], 2 ^ []), -(left_convergent_lines(1 ^ [], 2 ^ [])), -(left_convergent_lines(1 ^ [], reverse_line(2 ^ [])))],extension(7,bind([[_20096, _20157], [1 ^ [], 2 ^ []]]))).
% 0.35/1.43 cnf('1.1.1.1',plain,[-(unequally_directed_lines(1 ^ [], 2 ^ [])), convergent_lines(1 ^ [], 2 ^ [])],extension(5,bind([[_14161, _14212], [1 ^ [], 2 ^ []]]))).
% 0.35/1.43 cnf('1.1.1.1.1',plain,[-(convergent_lines(1 ^ [], 2 ^ []))],extension(1)).
% 0.35/1.43 cnf('1.1.1.2',plain,[left_convergent_lines(1 ^ [], 2 ^ [])],extension(8,bind([[_20968, _21017], [1 ^ [], 2 ^ []]]))).
% 0.35/1.43 cnf('1.1.1.3',plain,[left_convergent_lines(1 ^ [], reverse_line(2 ^ []))],extension(8,bind([[_20968, _21017], [1 ^ [], reverse_line(2 ^ [])]]))).
% 0.35/1.43 cnf('1.2',plain,[-(unequally_directed_lines(1 ^ [], reverse_line(2 ^ []))), unequally_directed_opposite_lines(1 ^ [], 2 ^ [])],extension(2,bind([[_12115, _12162], [1 ^ [], 2 ^ []]]))).
% 0.35/1.43 cnf('1.2.1',plain,[-(unequally_directed_opposite_lines(1 ^ [], 2 ^ [])), convergent_lines(1 ^ [], 2 ^ [])],extension(6,bind([[_14161, _14212], [1 ^ [], 2 ^ []]]))).
% 0.35/1.43 cnf('1.2.1.1',plain,[-(convergent_lines(1 ^ [], 2 ^ []))],extension(1)).
% 0.35/1.43 %-----------------------------------------------------
% 0.35/1.44
% 0.35/1.44 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------