%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO223+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.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 : 300s
% DateTime : Fri May 19 11:12:17 EDT 2023
% Result : Theorem 15.26s 15.84s
% Output : Proof 15.26s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.11 % Problem : GEO223+1 : TPTP v8.1.2. Released v3.3.0.
% 0.07/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n020.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 : 300
% 0.12/0.33 % DateTime : Fri May 19 04:28:02 EDT 2023
% 0.12/0.33 % CPUTime :
% 15.26/15.84
% 15.26/15.84 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 15.26/15.84 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.26/15.84 %-----------------------------------------------------
% 15.26/15.84 ncf(matrix, plain, [(180 ^ _33125) ^ [] : [-(distinct_lines(parallel_through_point(178 ^ [], 177 ^ []), orthogonal_through_point(orthogonal_through_point(178 ^ [], 177 ^ []), 177 ^ [])))], (114 ^ _33125) ^ [_36954, _36956] : [convergent_lines(parallel_through_point(_36954, _36956), _36954)], (116 ^ _33125) ^ [_37050, _37052] : [apart_point_and_line(_37052, parallel_through_point(_37050, _37052))], (118 ^ _33125) ^ [_37156, _37158, _37160] : [distinct_lines(_37158, _37156), -(apart_point_and_line(_37160, _37158)), -(apart_point_and_line(_37160, _37156)), -(convergent_lines(_37158, _37156))], (132 ^ _33125) ^ [_37564, _37566] : [-(convergent_lines(_37566, _37564)), -(unorthogonal_lines(_37566, _37564))], (138 ^ _33125) ^ [_37789, _37791, _37793] : [convergent_lines(_37793, _37791), unorthogonal_lines(_37793, _37791), 147 ^ _33125 : [(148 ^ _33125) ^ [] : [-(convergent_lines(_37793, _37789))], (150 ^ _33125) ^ [] : [-(unorthogonal_lines(_37793, _37789))]], 151 ^ _33125 : [(152 ^ _33125) ^ [] : [-(convergent_lines(_37791, _37789))], (154 ^ _33125) ^ [] : [-(unorthogonal_lines(_37791, _37789))]]], (156 ^ _33125) ^ [_38332, _38334] : [unorthogonal_lines(orthogonal_through_point(_38332, _38334), _38332)], (158 ^ _33125) ^ [_38428, _38430] : [apart_point_and_line(_38430, orthogonal_through_point(_38428, _38430))], (160 ^ _33125) ^ [_38548, _38550, _38552, _38554] : [distinct_lines(_38552, _38550), -(apart_point_and_line(_38554, _38552)), -(apart_point_and_line(_38554, _38550)), -(unorthogonal_lines(_38552, _38548)), -(unorthogonal_lines(_38550, _38548))], (2 ^ _33125) ^ [_33228] : [distinct_points(_33228, _33228)], (4 ^ _33125) ^ [_33305] : [distinct_lines(_33305, _33305)], (6 ^ _33125) ^ [_33382] : [convergent_lines(_33382, _33382)], (8 ^ _33125) ^ [_33503, _33505, _33507] : [distinct_points(_33507, _33505), -(distinct_points(_33507, _33503)), -(distinct_points(_33505, _33503))], (18 ^ _33125) ^ [_33827, _33829, _33831] : [distinct_lines(_33831, _33829), -(distinct_lines(_33831, _33827)), -(distinct_lines(_33829, _33827))], (28 ^ _33125) ^ [_34151, _34153, _34155] : [convergent_lines(_34155, _34153), -(convergent_lines(_34155, _34151)), -(convergent_lines(_34153, _34151))], (38 ^ _33125) ^ [_34461, _34463] : [distinct_points(_34463, _34461), apart_point_and_line(_34463, line_connecting(_34463, _34461))], (44 ^ _33125) ^ [_34678, _34680] : [distinct_points(_34680, _34678), apart_point_and_line(_34678, line_connecting(_34680, _34678))], (50 ^ _33125) ^ [_34895, _34897] : [convergent_lines(_34897, _34895), apart_point_and_line(intersection_point(_34897, _34895), _34897)], (56 ^ _33125) ^ [_35112, _35114] : [convergent_lines(_35114, _35112), apart_point_and_line(intersection_point(_35114, _35112), _35112)], (62 ^ _33125) ^ [_35357, _35359, _35361, _35363] : [distinct_points(_35363, _35361), distinct_lines(_35359, _35357), -(apart_point_and_line(_35363, _35359)), -(apart_point_and_line(_35363, _35357)), -(apart_point_and_line(_35361, _35359)), -(apart_point_and_line(_35361, _35357))], (84 ^ _33125) ^ [_35986, _35988, _35990] : [apart_point_and_line(_35990, _35988), -(distinct_points(_35990, _35986)), -(apart_point_and_line(_35986, _35988))], (94 ^ _33125) ^ [_36310, _36312, _36314] : [apart_point_and_line(_36314, _36312), -(distinct_lines(_36312, _36310)), -(apart_point_and_line(_36314, _36310))], (104 ^ _33125) ^ [_36614, _36616, _36618] : [convergent_lines(_36618, _36616), -(distinct_lines(_36616, _36614)), -(convergent_lines(_36618, _36614))]], input).
% 15.26/15.84 ncf('1',plain,[convergent_lines(parallel_through_point(178 ^ [], 177 ^ []), 178 ^ [])],start(114 ^ 0,bind([[_36954, _36956], [178 ^ [], 177 ^ []]]))).
% 15.26/15.84 ncf('1.1',plain,[-(convergent_lines(parallel_through_point(178 ^ [], 177 ^ []), 178 ^ [])), convergent_lines(orthogonal_through_point(178 ^ [], 177 ^ []), parallel_through_point(178 ^ [], 177 ^ [])), unorthogonal_lines(orthogonal_through_point(178 ^ [], 177 ^ []), parallel_through_point(178 ^ [], 177 ^ [])), 150 : -(unorthogonal_lines(orthogonal_through_point(178 ^ [], 177 ^ []), 178 ^ []))],extension(138 ^ 1,bind([[_37789, _37791, _37793], [178 ^ [], parallel_through_point(178 ^ [], 177 ^ []), orthogonal_through_point(178 ^ [], 177 ^ [])]]))).
% 15.26/15.84 ncf('1.1.1',plain,[-(convergent_lines(orthogonal_through_point(178 ^ [], 177 ^ []), parallel_through_point(178 ^ [], 177 ^ []))), convergent_lines(orthogonal_through_point(178 ^ [], 177 ^ []), 178 ^ []), -(convergent_lines(178 ^ [], parallel_through_point(178 ^ [], 177 ^ [])))],extension(28 ^ 2,bind([[_34151, _34153, _34155], [parallel_through_point(178 ^ [], 177 ^ []), 178 ^ [], orthogonal_through_point(178 ^ [], 177 ^ [])]]))).
% 15.26/15.84 ncf('1.1.1.1',plain,[-(convergent_lines(orthogonal_through_point(178 ^ [], 177 ^ []), 178 ^ [])), -(unorthogonal_lines(orthogonal_through_point(178 ^ [], 177 ^ []), 178 ^ []))],extension(132 ^ 3,bind([[_37564, _37566], [178 ^ [], orthogonal_through_point(178 ^ [], 177 ^ [])]]))).
% 15.26/15.84 ncf('1.1.1.1.1',plain,[unorthogonal_lines(orthogonal_through_point(178 ^ [], 177 ^ []), 178 ^ [])],extension(156 ^ 4,bind([[_38332, _38334], [178 ^ [], 177 ^ []]]))).
% 15.26/15.84 ncf('1.1.1.2',plain,[convergent_lines(178 ^ [], parallel_through_point(178 ^ [], 177 ^ [])), -(convergent_lines(178 ^ [], 178 ^ [])), -(convergent_lines(parallel_through_point(178 ^ [], 177 ^ []), 178 ^ []))],extension(28 ^ 3,bind([[_34151, _34153, _34155], [178 ^ [], parallel_through_point(178 ^ [], 177 ^ []), 178 ^ []]]))).
% 15.26/15.84 ncf('1.1.1.2.1',plain,[convergent_lines(178 ^ [], 178 ^ [])],extension(6 ^ 4,bind([[_33382], [178 ^ []]]))).
% 15.26/15.84 ncf('1.1.1.2.2',plain,[convergent_lines(parallel_through_point(178 ^ [], 177 ^ []), 178 ^ [])],reduction('1')).
% 15.26/15.84 ncf('1.1.2',plain,[-(unorthogonal_lines(orthogonal_through_point(178 ^ [], 177 ^ []), parallel_through_point(178 ^ [], 177 ^ []))), convergent_lines(parallel_through_point(178 ^ [], 177 ^ []), orthogonal_through_point(178 ^ [], 177 ^ [])), unorthogonal_lines(parallel_through_point(178 ^ [], 177 ^ []), orthogonal_through_point(178 ^ [], 177 ^ [])), 148 : -(convergent_lines(parallel_through_point(178 ^ [], 177 ^ []), parallel_through_point(178 ^ [], 177 ^ [])))],extension(138 ^ 2,bind([[_37789, _37791, _37793], [parallel_through_point(178 ^ [], 177 ^ []), orthogonal_through_point(178 ^ [], 177 ^ []), parallel_through_point(178 ^ [], 177 ^ [])]]))).
% 15.26/15.84 ncf('1.1.2.1',plain,[-(convergent_lines(parallel_through_point(178 ^ [], 177 ^ []), orthogonal_through_point(178 ^ [], 177 ^ []))), convergent_lines(orthogonal_through_point(178 ^ [], 177 ^ []), parallel_through_point(178 ^ [], 177 ^ [])), -(convergent_lines(orthogonal_through_point(178 ^ [], 177 ^ []), orthogonal_through_point(178 ^ [], 177 ^ [])))],extension(28 ^ 3,bind([[_34151, _34153, _34155], [orthogonal_through_point(178 ^ [], 177 ^ []), parallel_through_point(178 ^ [], 177 ^ []), orthogonal_through_point(178 ^ [], 177 ^ [])]]))).
% 15.26/15.84 ncf('1.1.2.1.1',plain,[-(convergent_lines(orthogonal_through_point(178 ^ [], 177 ^ []), parallel_through_point(178 ^ [], 177 ^ []))), -(unorthogonal_lines(orthogonal_through_point(178 ^ [], 177 ^ []), parallel_through_point(178 ^ [], 177 ^ [])))],extension(132 ^ 4,bind([[_37564, _37566], [parallel_through_point(178 ^ [], 177 ^ []), orthogonal_through_point(178 ^ [], 177 ^ [])]]))).
% 15.26/15.84 ncf('1.1.2.1.1.1',plain,[unorthogonal_lines(orthogonal_through_point(178 ^ [], 177 ^ []), parallel_through_point(178 ^ [], 177 ^ []))],reduction('1.1')).
% 15.26/15.84 ncf('1.1.2.1.2',plain,[convergent_lines(orthogonal_through_point(178 ^ [], 177 ^ []), orthogonal_through_point(178 ^ [], 177 ^ []))],extension(6 ^ 4,bind([[_33382], [orthogonal_through_point(178 ^ [], 177 ^ [])]]))).
% 15.26/15.84 ncf('1.1.2.2',plain,[-(unorthogonal_lines(parallel_through_point(178 ^ [], 177 ^ []), orthogonal_through_point(178 ^ [], 177 ^ []))), distinct_lines(parallel_through_point(178 ^ [], 177 ^ []), orthogonal_through_point(orthogonal_through_point(178 ^ [], 177 ^ []), 177 ^ [])), -(apart_point_and_line(177 ^ [], parallel_through_point(178 ^ [], 177 ^ []))), -(apart_point_and_line(177 ^ [], orthogonal_through_point(orthogonal_through_point(178 ^ [], 177 ^ []), 177 ^ []))), -(unorthogonal_lines(orthogonal_through_point(orthogonal_through_point(178 ^ [], 177 ^ []), 177 ^ []), orthogonal_through_point(178 ^ [], 177 ^ [])))],extension(160 ^ 3,bind([[_38548, _38550, _38552, _38554], [orthogonal_through_point(178 ^ [], 177 ^ []), orthogonal_through_point(orthogonal_through_point(178 ^ [], 177 ^ []), 177 ^ []), parallel_through_point(178 ^ [], 177 ^ []), 177 ^ []]]))).
% 15.26/15.84 ncf('1.1.2.2.1',plain,[-(distinct_lines(parallel_through_point(178 ^ [], 177 ^ []), orthogonal_through_point(orthogonal_through_point(178 ^ [], 177 ^ []), 177 ^ [])))],extension(180 ^ 4)).
% 15.26/15.84 ncf('1.1.2.2.2',plain,[apart_point_and_line(177 ^ [], parallel_through_point(178 ^ [], 177 ^ []))],extension(116 ^ 4,bind([[_37050, _37052], [178 ^ [], 177 ^ []]]))).
% 15.26/15.84 ncf('1.1.2.2.3',plain,[apart_point_and_line(177 ^ [], orthogonal_through_point(orthogonal_through_point(178 ^ [], 177 ^ []), 177 ^ []))],extension(158 ^ 4,bind([[_38428, _38430], [orthogonal_through_point(178 ^ [], 177 ^ []), 177 ^ []]]))).
% 15.26/15.84 ncf('1.1.2.2.4',plain,[unorthogonal_lines(orthogonal_through_point(orthogonal_through_point(178 ^ [], 177 ^ []), 177 ^ []), orthogonal_through_point(178 ^ [], 177 ^ []))],extension(156 ^ 4,bind([[_38332, _38334], [orthogonal_through_point(178 ^ [], 177 ^ []), 177 ^ []]]))).
% 15.26/15.84 ncf('1.1.2.3',plain,[convergent_lines(parallel_through_point(178 ^ [], 177 ^ []), parallel_through_point(178 ^ [], 177 ^ []))],extension(6 ^ 5,bind([[_33382], [parallel_through_point(178 ^ [], 177 ^ [])]]))).
% 15.26/15.84 ncf('1.1.3',plain,[unorthogonal_lines(orthogonal_through_point(178 ^ [], 177 ^ []), 178 ^ [])],extension(156 ^ 4,bind([[_38332, _38334], [178 ^ [], 177 ^ []]]))).
% 15.26/15.84 %-----------------------------------------------------
% 15.26/15.84 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------