%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : GEO210+3 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n011.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:03:43 EDT 2022
% Result : Theorem 0.35s 1.44s
% Output : Proof 0.45s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : GEO210+3 : TPTP v8.1.0. Released v4.0.0.
% 0.12/0.14 % Command : leancop_casc.sh %s %d
% 0.13/0.35 % Computer : n011.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 600
% 0.13/0.36 % DateTime : Fri Jun 17 18:07:22 EDT 2022
% 0.13/0.36 % CPUTime :
% 0.35/1.44 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.35/1.45 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.35/1.45
% 0.35/1.45 %-----------------------------------------------------
% 0.35/1.45 fof(con, conjecture, ! [_39607, _39610, _39613] : (incident_point_and_line(_39607, _39610) & orthogonal_lines(_39610, _39613) => equal_lines(_39610, orthogonal_through_point(_39613, _39607))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', con)).
% 0.35/1.45 fof(ci3, axiom, ! [_39827, _39830] : (convergent_lines(_39827, _39830) => ~ apart_point_and_line(intersection_point(_39827, _39830), _39827)), file('/export/starexec/sandbox/benchmark/Axioms/GEO006+0.ax', ci3)).
% 0.35/1.45 fof(ci4, axiom, ! [_39996, _39999] : (convergent_lines(_39996, _39999) => ~ apart_point_and_line(intersection_point(_39996, _39999), _39999)), file('/export/starexec/sandbox/benchmark/Axioms/GEO006+0.ax', ci4)).
% 0.35/1.45 fof(p1, axiom, ! [_40169, _40172] : (distinct_lines(_40169, _40172) => convergent_lines(_40169, _40172)), file('/export/starexec/sandbox/benchmark/Axioms/GEO006+1.ax', p1)).
% 0.35/1.45 fof(ooc1, axiom, ! [_40323, _40326] : ~ unorthogonal_lines(orthogonal_through_point(_40326, _40323), _40326), file('/export/starexec/sandbox/benchmark/Axioms/GEO006+3.ax', ooc1)).
% 0.35/1.45 fof(ouo1, axiom, ! [_40465, _40468, _40471, _40474] : (distinct_lines(_40468, _40471) => apart_point_and_line(_40465, _40468) | apart_point_and_line(_40465, _40471) | unorthogonal_lines(_40468, _40474) | unorthogonal_lines(_40471, _40474)), file('/export/starexec/sandbox/benchmark/Axioms/GEO006+3.ax', ouo1)).
% 0.35/1.45 fof(ax2, axiom, ! [_40730, _40733] : (equal_lines(_40730, _40733) <=> ~ distinct_lines(_40730, _40733)), file('/export/starexec/sandbox/benchmark/Axioms/GEO006+6.ax', ax2)).
% 0.35/1.45 fof(a5, axiom, ! [_40887, _40890] : (orthogonal_lines(_40887, _40890) <=> ~ unorthogonal_lines(_40887, _40890)), file('/export/starexec/sandbox/benchmark/Axioms/GEO006+6.ax', a5)).
% 0.35/1.45
% 0.35/1.45 cnf(1, plain, [-(orthogonal_lines(2 ^ [], 3 ^ []))], clausify(con)).
% 0.35/1.45 cnf(2, plain, [equal_lines(2 ^ [], orthogonal_through_point(3 ^ [], 1 ^ []))], clausify(con)).
% 0.35/1.45 cnf(3, plain, [convergent_lines(_14958, _15008), apart_point_and_line(intersection_point(_14958, _15008), _14958)], clausify(ci3)).
% 0.35/1.45 cnf(4, plain, [convergent_lines(_15331, _15381), apart_point_and_line(intersection_point(_15331, _15381), _15381)], clausify(ci4)).
% 0.35/1.45 cnf(5, plain, [distinct_lines(_18131, _18176), -(convergent_lines(_18131, _18176))], clausify(p1)).
% 0.35/1.45 cnf(6, plain, [unorthogonal_lines(orthogonal_through_point(_20711, _20667), _20711)], clausify(ooc1)).
% 0.35/1.45 cnf(7, plain, [distinct_lines(_21304, _21376), -(apart_point_and_line(_21231, _21304)), -(apart_point_and_line(_21231, _21376)), -(unorthogonal_lines(_21304, _21447)), -(unorthogonal_lines(_21376, _21447))], clausify(ouo1)).
% 0.35/1.45 cnf(8, plain, [-(equal_lines(_25869, _25916)), -(distinct_lines(_25869, _25916))], clausify(ax2)).
% 0.35/1.45 cnf(9, plain, [orthogonal_lines(_26849, _26896), unorthogonal_lines(_26849, _26896)], clausify(a5)).
% 0.35/1.45
% 0.35/1.45 cnf('1',plain,[convergent_lines(2 ^ [], orthogonal_through_point(3 ^ [], 1 ^ [])), apart_point_and_line(intersection_point(2 ^ [], orthogonal_through_point(3 ^ [], 1 ^ [])), 2 ^ [])],start(3,bind([[_15008, _14958], [orthogonal_through_point(3 ^ [], 1 ^ []), 2 ^ []]]))).
% 0.35/1.45 cnf('1.1',plain,[-(convergent_lines(2 ^ [], orthogonal_through_point(3 ^ [], 1 ^ []))), distinct_lines(2 ^ [], orthogonal_through_point(3 ^ [], 1 ^ []))],extension(5,bind([[_18131, _18176], [2 ^ [], orthogonal_through_point(3 ^ [], 1 ^ [])]]))).
% 0.35/1.45 cnf('1.1.1',plain,[-(distinct_lines(2 ^ [], orthogonal_through_point(3 ^ [], 1 ^ []))), -(equal_lines(2 ^ [], orthogonal_through_point(3 ^ [], 1 ^ [])))],extension(8,bind([[_25869, _25916], [2 ^ [], orthogonal_through_point(3 ^ [], 1 ^ [])]]))).
% 0.35/1.45 cnf('1.1.1.1',plain,[equal_lines(2 ^ [], orthogonal_through_point(3 ^ [], 1 ^ []))],extension(2)).
% 0.35/1.45 cnf('1.2',plain,[-(apart_point_and_line(intersection_point(2 ^ [], orthogonal_through_point(3 ^ [], 1 ^ [])), 2 ^ [])), distinct_lines(2 ^ [], orthogonal_through_point(3 ^ [], 1 ^ [])), -(apart_point_and_line(intersection_point(2 ^ [], orthogonal_through_point(3 ^ [], 1 ^ [])), orthogonal_through_point(3 ^ [], 1 ^ []))), -(unorthogonal_lines(2 ^ [], 3 ^ [])), -(unorthogonal_lines(orthogonal_through_point(3 ^ [], 1 ^ []), 3 ^ []))],extension(7,bind([[_21231, _21304, _21376, _21447], [intersection_point(2 ^ [], orthogonal_through_point(3 ^ [], 1 ^ [])), 2 ^ [], orthogonal_through_point(3 ^ [], 1 ^ []), 3 ^ []]]))).
% 0.35/1.45 cnf('1.2.1',plain,[-(distinct_lines(2 ^ [], orthogonal_through_point(3 ^ [], 1 ^ []))), -(equal_lines(2 ^ [], orthogonal_through_point(3 ^ [], 1 ^ [])))],extension(8,bind([[_25869, _25916], [2 ^ [], orthogonal_through_point(3 ^ [], 1 ^ [])]]))).
% 0.35/1.45 cnf('1.2.1.1',plain,[equal_lines(2 ^ [], orthogonal_through_point(3 ^ [], 1 ^ []))],extension(2)).
% 0.35/1.45 cnf('1.2.2',plain,[apart_point_and_line(intersection_point(2 ^ [], orthogonal_through_point(3 ^ [], 1 ^ [])), orthogonal_through_point(3 ^ [], 1 ^ [])), convergent_lines(2 ^ [], orthogonal_through_point(3 ^ [], 1 ^ []))],extension(4,bind([[_15331, _15381], [2 ^ [], orthogonal_through_point(3 ^ [], 1 ^ [])]]))).
% 0.35/1.45 cnf('1.2.2.1',plain,[-(convergent_lines(2 ^ [], orthogonal_through_point(3 ^ [], 1 ^ [])))],lemmata('1')).
% 0.35/1.45 cnf('1.2.3',plain,[unorthogonal_lines(2 ^ [], 3 ^ []), orthogonal_lines(2 ^ [], 3 ^ [])],extension(9,bind([[_26849, _26896], [2 ^ [], 3 ^ []]]))).
% 0.35/1.45 cnf('1.2.3.1',plain,[-(orthogonal_lines(2 ^ [], 3 ^ []))],extension(1)).
% 0.35/1.45 cnf('1.2.4',plain,[unorthogonal_lines(orthogonal_through_point(3 ^ [], 1 ^ []), 3 ^ [])],extension(6,bind([[_20667, _20711], [1 ^ [], 3 ^ []]]))).
% 0.35/1.45 %-----------------------------------------------------
% 0.45/1.46
% 0.45/1.46 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------