%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : GEO188+3 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n019.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:24 EDT 2022
% Result : Theorem 0.74s 1.41s
% Output : Proof 0.82s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : GEO188+3 : TPTP v8.1.0. Released v4.0.0.
% 0.06/0.13 % Command : leancop_casc.sh %s %d
% 0.13/0.34 % Computer : n019.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:01:24 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.74/1.41 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.74/1.42 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.82/1.42
% 0.82/1.42 %-----------------------------------------------------
% 0.82/1.42 fof(con, conjecture, ! [_39013, _39016, _39019] : (distinct_points(_39013, _39016) & distinct_points(_39013, _39019) & distinct_points(_39016, _39019) & incident_point_and_line(_39019, line_connecting(_39013, _39016)) => incident_point_and_line(_39013, line_connecting(_39019, _39016))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', con)).
% 0.82/1.42 fof(apart2, axiom, ! [_39287] : ~ distinct_lines(_39287, _39287), file('/export/starexec/sandbox/benchmark/Axioms/GEO006+0.ax', apart2)).
% 0.82/1.42 fof(apart5, axiom, ! [_39403, _39406, _39409] : (distinct_lines(_39403, _39406) => distinct_lines(_39403, _39409) | distinct_lines(_39406, _39409)), file('/export/starexec/sandbox/benchmark/Axioms/GEO006+0.ax', apart5)).
% 0.82/1.42 fof(ceq2, axiom, ! [_39595, _39598, _39601] : (apart_point_and_line(_39595, _39598) => distinct_lines(_39598, _39601) | apart_point_and_line(_39595, _39601)), file('/export/starexec/sandbox/benchmark/Axioms/GEO006+0.ax', ceq2)).
% 0.82/1.42 fof(p1, axiom, ! [_39781, _39784] : (distinct_lines(_39781, _39784) => convergent_lines(_39781, _39784)), file('/export/starexec/sandbox/benchmark/Axioms/GEO006+1.ax', p1)).
% 0.82/1.42 fof(cp1, axiom, ! [_39927, _39930] : ~ convergent_lines(parallel_through_point(_39930, _39927), _39930), file('/export/starexec/sandbox/benchmark/Axioms/GEO006+2.ax', cp1)).
% 0.82/1.42 fof(cp2, axiom, ! [_40068, _40071] : ~ apart_point_and_line(_40068, parallel_through_point(_40071, _40068)), file('/export/starexec/sandbox/benchmark/Axioms/GEO006+2.ax', cp2)).
% 0.82/1.42 fof(a4, axiom, ! [_40235, _40238] : (incident_point_and_line(_40235, _40238) <=> ~ apart_point_and_line(_40235, _40238)), file('/export/starexec/sandbox/benchmark/Axioms/GEO006+6.ax', a4)).
% 0.82/1.42
% 0.82/1.42 cnf(1, plain, [incident_point_and_line(1 ^ [], line_connecting(3 ^ [], 2 ^ []))], clausify(con)).
% 0.82/1.42 cnf(2, plain, [distinct_lines(_12523, _12523)], clausify(apart2)).
% 0.82/1.42 cnf(3, plain, [distinct_lines(_13374, _13430), -(distinct_lines(_13374, _13485)), -(distinct_lines(_13430, _13485))], clausify(apart5)).
% 0.82/1.42 cnf(4, plain, [apart_point_and_line(_17108, _17164), -(distinct_lines(_17164, _17219)), -(apart_point_and_line(_17108, _17219))], clausify(ceq2)).
% 0.82/1.42 cnf(5, plain, [distinct_lines(_18227, _18272), -(convergent_lines(_18227, _18272))], clausify(p1)).
% 0.82/1.42 cnf(6, plain, [convergent_lines(parallel_through_point(_18591, _18547), _18591)], clausify(cp1)).
% 0.82/1.42 cnf(7, plain, [apart_point_and_line(_18834, parallel_through_point(_18878, _18834))], clausify(cp2)).
% 0.82/1.42 cnf(8, plain, [-(incident_point_and_line(_26625, _26672)), -(apart_point_and_line(_26625, _26672))], clausify(a4)).
% 0.82/1.42
% 0.82/1.42 cnf('1',plain,[convergent_lines(parallel_through_point(line_connecting(3 ^ [], 2 ^ []), 1 ^ []), line_connecting(3 ^ [], 2 ^ []))],start(6,bind([[_18547, _18591], [1 ^ [], line_connecting(3 ^ [], 2 ^ [])]]))).
% 0.82/1.42 cnf('1.1',plain,[-(convergent_lines(parallel_through_point(line_connecting(3 ^ [], 2 ^ []), 1 ^ []), line_connecting(3 ^ [], 2 ^ []))), distinct_lines(parallel_through_point(line_connecting(3 ^ [], 2 ^ []), 1 ^ []), line_connecting(3 ^ [], 2 ^ []))],extension(5,bind([[_18227, _18272], [parallel_through_point(line_connecting(3 ^ [], 2 ^ []), 1 ^ []), line_connecting(3 ^ [], 2 ^ [])]]))).
% 0.82/1.42 cnf('1.1.1',plain,[-(distinct_lines(parallel_through_point(line_connecting(3 ^ [], 2 ^ []), 1 ^ []), line_connecting(3 ^ [], 2 ^ []))), distinct_lines(line_connecting(3 ^ [], 2 ^ []), parallel_through_point(line_connecting(3 ^ [], 2 ^ []), 1 ^ [])), -(distinct_lines(line_connecting(3 ^ [], 2 ^ []), line_connecting(3 ^ [], 2 ^ [])))],extension(3,bind([[_13430, _13374, _13485], [parallel_through_point(line_connecting(3 ^ [], 2 ^ []), 1 ^ []), line_connecting(3 ^ [], 2 ^ []), line_connecting(3 ^ [], 2 ^ [])]]))).
% 0.82/1.42 cnf('1.1.1.1',plain,[-(distinct_lines(line_connecting(3 ^ [], 2 ^ []), parallel_through_point(line_connecting(3 ^ [], 2 ^ []), 1 ^ []))), apart_point_and_line(1 ^ [], line_connecting(3 ^ [], 2 ^ [])), -(apart_point_and_line(1 ^ [], parallel_through_point(line_connecting(3 ^ [], 2 ^ []), 1 ^ [])))],extension(4,bind([[_17164, _17108, _17219], [line_connecting(3 ^ [], 2 ^ []), 1 ^ [], parallel_through_point(line_connecting(3 ^ [], 2 ^ []), 1 ^ [])]]))).
% 0.82/1.42 cnf('1.1.1.1.1',plain,[-(apart_point_and_line(1 ^ [], line_connecting(3 ^ [], 2 ^ []))), -(incident_point_and_line(1 ^ [], line_connecting(3 ^ [], 2 ^ [])))],extension(8,bind([[_26625, _26672], [1 ^ [], line_connecting(3 ^ [], 2 ^ [])]]))).
% 0.82/1.42 cnf('1.1.1.1.1.1',plain,[incident_point_and_line(1 ^ [], line_connecting(3 ^ [], 2 ^ []))],extension(1)).
% 0.82/1.42 cnf('1.1.1.1.2',plain,[apart_point_and_line(1 ^ [], parallel_through_point(line_connecting(3 ^ [], 2 ^ []), 1 ^ []))],extension(7,bind([[_18878, _18834], [line_connecting(3 ^ [], 2 ^ []), 1 ^ []]]))).
% 0.82/1.42 cnf('1.1.1.2',plain,[distinct_lines(line_connecting(3 ^ [], 2 ^ []), line_connecting(3 ^ [], 2 ^ []))],extension(2,bind([[_12523], [line_connecting(3 ^ [], 2 ^ [])]]))).
% 0.82/1.42 %-----------------------------------------------------
% 0.82/1.43
% 0.82/1.43 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------