%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : GEO223+2 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n015.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:55 EDT 2022
% Result : Theorem 138.02s 133.79s
% Output : Proof 138.02s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO223+2 : TPTP v8.1.0. Released v3.3.0.
% 0.07/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n015.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Sat Jun 18 06:38:58 EDT 2022
% 0.12/0.33 % CPUTime :
% 138.02/133.79 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 138.02/133.79 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 138.02/133.80
% 138.02/133.80 %-----------------------------------------------------
% 138.02/133.80 fof(con, conjecture, ! [_28812, _28815] : ~ distinct_lines(parallel_through_point(_28815, _28812), orthogonal_through_point(orthogonal_through_point(_28815, _28812), _28812)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', con)).
% 138.02/133.80 fof(cp1, axiom, ! [_28985, _28988] : ~ convergent_lines(parallel_through_point(_28988, _28985), _28988), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+2.ax', cp1)).
% 138.02/133.80 fof(cp2, axiom, ! [_29126, _29129] : ~ apart_point_and_line(_29126, parallel_through_point(_29129, _29126)), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+2.ax', cp2)).
% 138.02/133.80 fof(occu1, axiom, ! [_29268, _29271] : (convergent_lines(_29268, _29271) | unorthogonal_lines(_29268, _29271)), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+3.ax', occu1)).
% 138.02/133.80 fof(oac1, axiom, ! [_29415, _29418, _29421] : (convergent_lines(_29415, _29418) & unorthogonal_lines(_29415, _29418) => convergent_lines(_29415, _29421) & unorthogonal_lines(_29415, _29421) | convergent_lines(_29418, _29421) & unorthogonal_lines(_29418, _29421)), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+3.ax', oac1)).
% 138.02/133.80 fof(ooc1, axiom, ! [_29697, _29700] : ~ unorthogonal_lines(orthogonal_through_point(_29700, _29697), _29700), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+3.ax', ooc1)).
% 138.02/133.80 fof(ooc2, axiom, ! [_29838, _29841] : ~ apart_point_and_line(_29838, orthogonal_through_point(_29841, _29838)), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+3.ax', ooc2)).
% 138.02/133.80 fof(ouo1, axiom, ! [_29979, _29982, _29985, _29988] : (distinct_lines(_29982, _29985) => apart_point_and_line(_29979, _29982) | apart_point_and_line(_29979, _29985) | unorthogonal_lines(_29982, _29988) | unorthogonal_lines(_29985, _29988)), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+3.ax', ouo1)).
% 138.02/133.80 fof(apart3, axiom, ! [_30233] : ~ convergent_lines(_30233, _30233), file('/export/starexec/sandbox2/benchmark/Axioms/GEO008+0.ax', apart3)).
% 138.02/133.80 fof(apart6, axiom, ! [_30349, _30352, _30355] : (convergent_lines(_30349, _30352) => convergent_lines(_30349, _30355) | convergent_lines(_30352, _30355)), file('/export/starexec/sandbox2/benchmark/Axioms/GEO008+0.ax', apart6)).
% 138.02/133.80
% 138.02/133.80 cnf(1, plain, [-(distinct_lines(parallel_through_point(2 ^ [], 1 ^ []), orthogonal_through_point(orthogonal_through_point(2 ^ [], 1 ^ []), 1 ^ [])))], clausify(con)).
% 138.02/133.80 cnf(2, plain, [convergent_lines(parallel_through_point(_13532, _13488), _13532)], clausify(cp1)).
% 138.02/133.80 cnf(3, plain, [apart_point_and_line(_13775, parallel_through_point(_13819, _13775))], clausify(cp2)).
% 138.02/133.80 cnf(4, plain, [-(convergent_lines(_14641, _14686)), -(unorthogonal_lines(_14641, _14686))], clausify(occu1)).
% 138.02/133.80 cnf(5, plain, [unorthogonal_lines(_14951, _15025), convergent_lines(_14951, _15025), -(convergent_lines(_14951, _15098)), -(unorthogonal_lines(_15025, _15098))], clausify(oac1)).
% 138.02/133.80 cnf(6, plain, [unorthogonal_lines(_14951, _15025), convergent_lines(_14951, _15025), -(unorthogonal_lines(_14951, _15098)), -(convergent_lines(_15025, _15098))], clausify(oac1)).
% 138.02/133.80 cnf(7, plain, [unorthogonal_lines(orthogonal_through_point(_15738, _15694), _15738)], clausify(ooc1)).
% 138.02/133.80 cnf(8, plain, [apart_point_and_line(_15981, orthogonal_through_point(_16025, _15981))], clausify(ooc2)).
% 138.02/133.80 cnf(9, plain, [distinct_lines(_16331, _16403), -(apart_point_and_line(_16258, _16331)), -(apart_point_and_line(_16258, _16403)), -(unorthogonal_lines(_16331, _16474)), -(unorthogonal_lines(_16403, _16474))], clausify(ouo1)).
% 138.02/133.80 cnf(10, plain, [convergent_lines(_8435, _8435)], clausify(apart3)).
% 138.02/133.80 cnf(11, plain, [convergent_lines(_9561, _9617), -(convergent_lines(_9561, _9672)), -(convergent_lines(_9617, _9672))], clausify(apart6)).
% 138.02/133.80
% 138.02/133.80 cnf('1',plain,[convergent_lines(parallel_through_point(2 ^ [], 1 ^ []), 2 ^ [])],start(2,bind([[_13488, _13532], [1 ^ [], 2 ^ []]]))).
% 138.02/133.80 cnf('1.1',plain,[-(convergent_lines(parallel_through_point(2 ^ [], 1 ^ []), 2 ^ [])), unorthogonal_lines(orthogonal_through_point(2 ^ [], 1 ^ []), parallel_through_point(2 ^ [], 1 ^ [])), convergent_lines(orthogonal_through_point(2 ^ [], 1 ^ []), parallel_through_point(2 ^ [], 1 ^ [])), -(unorthogonal_lines(orthogonal_through_point(2 ^ [], 1 ^ []), 2 ^ []))],extension(6,bind([[_15025, _14951, _15098], [parallel_through_point(2 ^ [], 1 ^ []), orthogonal_through_point(2 ^ [], 1 ^ []), 2 ^ []]]))).
% 138.02/133.80 cnf('1.1.1',plain,[-(unorthogonal_lines(orthogonal_through_point(2 ^ [], 1 ^ []), parallel_through_point(2 ^ [], 1 ^ []))), unorthogonal_lines(parallel_through_point(2 ^ [], 1 ^ []), orthogonal_through_point(2 ^ [], 1 ^ [])), convergent_lines(parallel_through_point(2 ^ [], 1 ^ []), orthogonal_through_point(2 ^ [], 1 ^ [])), -(convergent_lines(parallel_through_point(2 ^ [], 1 ^ []), parallel_through_point(2 ^ [], 1 ^ [])))],extension(5,bind([[_15025, _14951, _15098], [orthogonal_through_point(2 ^ [], 1 ^ []), parallel_through_point(2 ^ [], 1 ^ []), parallel_through_point(2 ^ [], 1 ^ [])]]))).
% 138.02/133.80 cnf('1.1.1.1',plain,[-(unorthogonal_lines(parallel_through_point(2 ^ [], 1 ^ []), orthogonal_through_point(2 ^ [], 1 ^ []))), distinct_lines(parallel_through_point(2 ^ [], 1 ^ []), orthogonal_through_point(orthogonal_through_point(2 ^ [], 1 ^ []), 1 ^ [])), -(apart_point_and_line(1 ^ [], parallel_through_point(2 ^ [], 1 ^ []))), -(apart_point_and_line(1 ^ [], orthogonal_through_point(orthogonal_through_point(2 ^ [], 1 ^ []), 1 ^ []))), -(unorthogonal_lines(orthogonal_through_point(orthogonal_through_point(2 ^ [], 1 ^ []), 1 ^ []), orthogonal_through_point(2 ^ [], 1 ^ [])))],extension(9,bind([[_16331, _16258, _16403, _16474], [parallel_through_point(2 ^ [], 1 ^ []), 1 ^ [], orthogonal_through_point(orthogonal_through_point(2 ^ [], 1 ^ []), 1 ^ []), orthogonal_through_point(2 ^ [], 1 ^ [])]]))).
% 138.02/133.80 cnf('1.1.1.1.1',plain,[-(distinct_lines(parallel_through_point(2 ^ [], 1 ^ []), orthogonal_through_point(orthogonal_through_point(2 ^ [], 1 ^ []), 1 ^ [])))],extension(1)).
% 138.02/133.80 cnf('1.1.1.1.2',plain,[apart_point_and_line(1 ^ [], parallel_through_point(2 ^ [], 1 ^ []))],extension(3,bind([[_13819, _13775], [2 ^ [], 1 ^ []]]))).
% 138.02/133.80 cnf('1.1.1.1.3',plain,[apart_point_and_line(1 ^ [], orthogonal_through_point(orthogonal_through_point(2 ^ [], 1 ^ []), 1 ^ []))],extension(8,bind([[_16025, _15981], [orthogonal_through_point(2 ^ [], 1 ^ []), 1 ^ []]]))).
% 138.02/133.80 cnf('1.1.1.1.4',plain,[unorthogonal_lines(orthogonal_through_point(orthogonal_through_point(2 ^ [], 1 ^ []), 1 ^ []), orthogonal_through_point(2 ^ [], 1 ^ []))],extension(7,bind([[_15694, _15738], [1 ^ [], orthogonal_through_point(2 ^ [], 1 ^ [])]]))).
% 138.02/133.80 cnf('1.1.1.2',plain,[-(convergent_lines(parallel_through_point(2 ^ [], 1 ^ []), orthogonal_through_point(2 ^ [], 1 ^ []))), convergent_lines(orthogonal_through_point(2 ^ [], 1 ^ []), parallel_through_point(2 ^ [], 1 ^ [])), -(convergent_lines(orthogonal_through_point(2 ^ [], 1 ^ []), orthogonal_through_point(2 ^ [], 1 ^ [])))],extension(11,bind([[_9617, _9561, _9672], [parallel_through_point(2 ^ [], 1 ^ []), orthogonal_through_point(2 ^ [], 1 ^ []), orthogonal_through_point(2 ^ [], 1 ^ [])]]))).
% 138.02/133.80 cnf('1.1.1.2.1',plain,[-(convergent_lines(orthogonal_through_point(2 ^ [], 1 ^ []), parallel_through_point(2 ^ [], 1 ^ []))), -(unorthogonal_lines(orthogonal_through_point(2 ^ [], 1 ^ []), parallel_through_point(2 ^ [], 1 ^ [])))],extension(4,bind([[_14641, _14686], [orthogonal_through_point(2 ^ [], 1 ^ []), parallel_through_point(2 ^ [], 1 ^ [])]]))).
% 138.02/133.80 cnf('1.1.1.2.1.1',plain,[unorthogonal_lines(orthogonal_through_point(2 ^ [], 1 ^ []), parallel_through_point(2 ^ [], 1 ^ []))],reduction('1.1')).
% 138.02/133.80 cnf('1.1.1.2.2',plain,[convergent_lines(orthogonal_through_point(2 ^ [], 1 ^ []), orthogonal_through_point(2 ^ [], 1 ^ []))],extension(10,bind([[_8435], [orthogonal_through_point(2 ^ [], 1 ^ [])]]))).
% 138.02/133.80 cnf('1.1.1.3',plain,[convergent_lines(parallel_through_point(2 ^ [], 1 ^ []), parallel_through_point(2 ^ [], 1 ^ []))],extension(10,bind([[_8435], [parallel_through_point(2 ^ [], 1 ^ [])]]))).
% 138.02/133.80 cnf('1.1.2',plain,[-(convergent_lines(orthogonal_through_point(2 ^ [], 1 ^ []), parallel_through_point(2 ^ [], 1 ^ []))), convergent_lines(orthogonal_through_point(2 ^ [], 1 ^ []), 2 ^ []), -(convergent_lines(2 ^ [], parallel_through_point(2 ^ [], 1 ^ [])))],extension(11,bind([[_9561, _9617, _9672], [orthogonal_through_point(2 ^ [], 1 ^ []), 2 ^ [], parallel_through_point(2 ^ [], 1 ^ [])]]))).
% 138.02/133.80 cnf('1.1.2.1',plain,[-(convergent_lines(orthogonal_through_point(2 ^ [], 1 ^ []), 2 ^ [])), -(unorthogonal_lines(orthogonal_through_point(2 ^ [], 1 ^ []), 2 ^ []))],extension(4,bind([[_14641, _14686], [orthogonal_through_point(2 ^ [], 1 ^ []), 2 ^ []]]))).
% 138.02/133.80 cnf('1.1.2.1.1',plain,[unorthogonal_lines(orthogonal_through_point(2 ^ [], 1 ^ []), 2 ^ [])],extension(7,bind([[_15694, _15738], [1 ^ [], 2 ^ []]]))).
% 138.02/133.80 cnf('1.1.2.2',plain,[convergent_lines(2 ^ [], parallel_through_point(2 ^ [], 1 ^ [])), -(convergent_lines(2 ^ [], 2 ^ [])), -(convergent_lines(parallel_through_point(2 ^ [], 1 ^ []), 2 ^ []))],extension(11,bind([[_9561, _9617, _9672], [2 ^ [], parallel_through_point(2 ^ [], 1 ^ []), 2 ^ []]]))).
% 138.02/133.80 cnf('1.1.2.2.1',plain,[convergent_lines(2 ^ [], 2 ^ [])],extension(10,bind([[_8435], [2 ^ []]]))).
% 138.02/133.80 cnf('1.1.2.2.2',plain,[convergent_lines(parallel_through_point(2 ^ [], 1 ^ []), 2 ^ [])],extension(2,bind([[_13488, _13532], [1 ^ [], 2 ^ []]]))).
% 138.02/133.80 cnf('1.1.3',plain,[unorthogonal_lines(orthogonal_through_point(2 ^ [], 1 ^ []), 2 ^ [])],extension(7,bind([[_15694, _15738], [1 ^ [], 2 ^ []]]))).
% 138.02/133.80 %-----------------------------------------------------
% 138.02/133.80
% 138.02/133.80 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------