%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO210+2 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n012.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:14 EDT 2023
% Result : Theorem 0.32s 1.39s
% Output : Proof 0.32s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GEO210+2 : TPTP v8.1.2. Released v3.3.0.
% 0.03/0.13 % Command : nanocop.sh %s %d
% 0.12/0.34 % Computer : n012.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Fri May 19 04:13:46 EDT 2023
% 0.12/0.34 % CPUTime :
% 0.32/1.39
% 0.32/1.39 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.32/1.39 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.32/1.39 %-----------------------------------------------------
% 0.32/1.39 ncf(matrix, plain, [(177 ^ _30773) ^ [] : [apart_point_and_line(173 ^ [], 174 ^ [])], (179 ^ _30773) ^ [] : [unorthogonal_lines(174 ^ [], 175 ^ [])], (181 ^ _30773) ^ [] : [-(distinct_lines(174 ^ [], orthogonal_through_point(175 ^ [], 173 ^ [])))], (110 ^ _30773) ^ [_34427, _34429] : [convergent_lines(parallel_through_point(_34427, _34429), _34427)], (112 ^ _30773) ^ [_34523, _34525] : [apart_point_and_line(_34525, parallel_through_point(_34523, _34525))], (114 ^ _30773) ^ [_34629, _34631, _34633] : [distinct_lines(_34631, _34629), -(apart_point_and_line(_34633, _34631)), -(apart_point_and_line(_34633, _34629)), -(convergent_lines(_34631, _34629))], (128 ^ _30773) ^ [_35037, _35039] : [-(convergent_lines(_35039, _35037)), -(unorthogonal_lines(_35039, _35037))], (134 ^ _30773) ^ [_35262, _35264, _35266] : [convergent_lines(_35266, _35264), unorthogonal_lines(_35266, _35264), 143 ^ _30773 : [(144 ^ _30773) ^ [] : [-(convergent_lines(_35266, _35262))], (146 ^ _30773) ^ [] : [-(unorthogonal_lines(_35266, _35262))]], 147 ^ _30773 : [(148 ^ _30773) ^ [] : [-(convergent_lines(_35264, _35262))], (150 ^ _30773) ^ [] : [-(unorthogonal_lines(_35264, _35262))]]], (152 ^ _30773) ^ [_35805, _35807] : [unorthogonal_lines(orthogonal_through_point(_35805, _35807), _35805)], (154 ^ _30773) ^ [_35901, _35903] : [apart_point_and_line(_35903, orthogonal_through_point(_35901, _35903))], (156 ^ _30773) ^ [_36021, _36023, _36025, _36027] : [distinct_lines(_36025, _36023), -(apart_point_and_line(_36027, _36025)), -(apart_point_and_line(_36027, _36023)), -(unorthogonal_lines(_36025, _36021)), -(unorthogonal_lines(_36023, _36021))], (2 ^ _30773) ^ [_30876] : [distinct_points(_30876, _30876)], (4 ^ _30773) ^ [_30953] : [distinct_lines(_30953, _30953)], (6 ^ _30773) ^ [_31030] : [convergent_lines(_31030, _31030)], (8 ^ _30773) ^ [_31151, _31153, _31155] : [distinct_points(_31155, _31153), -(distinct_points(_31155, _31151)), -(distinct_points(_31153, _31151))], (18 ^ _30773) ^ [_31475, _31477, _31479] : [distinct_lines(_31479, _31477), -(distinct_lines(_31479, _31475)), -(distinct_lines(_31477, _31475))], (28 ^ _30773) ^ [_31799, _31801, _31803] : [convergent_lines(_31803, _31801), -(convergent_lines(_31803, _31799)), -(convergent_lines(_31801, _31799))], (38 ^ _30773) ^ [_32123, _32125, _32127] : [distinct_points(_32127, _32125), apart_point_and_line(_32123, line_connecting(_32127, _32125)), 45 ^ _30773 : [(46 ^ _30773) ^ [] : [-(distinct_points(_32123, _32127))], (48 ^ _30773) ^ [] : [-(distinct_points(_32123, _32125))]]], (50 ^ _30773) ^ [_32529, _32531, _32533] : [convergent_lines(_32533, _32531), 55 ^ _30773 : [(56 ^ _30773) ^ [] : [apart_point_and_line(_32529, _32533)], (58 ^ _30773) ^ [] : [apart_point_and_line(_32529, _32531)]], -(distinct_points(_32529, intersection_point(_32533, _32531)))], (62 ^ _30773) ^ [_32948, _32950, _32952, _32954] : [distinct_points(_32954, _32952), distinct_lines(_32950, _32948), -(apart_point_and_line(_32954, _32950)), -(apart_point_and_line(_32954, _32948)), -(apart_point_and_line(_32952, _32950)), -(apart_point_and_line(_32952, _32948))], (84 ^ _30773) ^ [_33577, _33579, _33581] : [apart_point_and_line(_33581, _33579), -(distinct_points(_33581, _33577)), -(apart_point_and_line(_33577, _33579))], (104 ^ _30773) ^ [_34191, _34193] : [convergent_lines(_34193, _34191), -(distinct_lines(_34193, _34191))], (94 ^ _30773) ^ [_33901, _33903, _33905] : [apart_point_and_line(_33905, _33903), -(distinct_lines(_33903, _33901)), -(apart_point_and_line(_33905, _33901))]], input).
% 0.32/1.39 ncf('1',plain,[apart_point_and_line(173 ^ [], 174 ^ [])],start(177 ^ 0)).
% 0.32/1.39 ncf('1.1',plain,[-(apart_point_and_line(173 ^ [], 174 ^ [])), distinct_lines(174 ^ [], orthogonal_through_point(175 ^ [], 173 ^ [])), -(apart_point_and_line(173 ^ [], orthogonal_through_point(175 ^ [], 173 ^ []))), -(unorthogonal_lines(174 ^ [], 175 ^ [])), -(unorthogonal_lines(orthogonal_through_point(175 ^ [], 173 ^ []), 175 ^ []))],extension(156 ^ 1,bind([[_36021, _36023, _36025, _36027], [175 ^ [], orthogonal_through_point(175 ^ [], 173 ^ []), 174 ^ [], 173 ^ []]]))).
% 0.32/1.39 ncf('1.1.1',plain,[-(distinct_lines(174 ^ [], orthogonal_through_point(175 ^ [], 173 ^ [])))],extension(181 ^ 2)).
% 0.32/1.39 ncf('1.1.2',plain,[apart_point_and_line(173 ^ [], orthogonal_through_point(175 ^ [], 173 ^ []))],extension(154 ^ 2,bind([[_35901, _35903], [175 ^ [], 173 ^ []]]))).
% 0.32/1.39 ncf('1.1.3',plain,[unorthogonal_lines(174 ^ [], 175 ^ [])],extension(179 ^ 2)).
% 0.32/1.39 ncf('1.1.4',plain,[unorthogonal_lines(orthogonal_through_point(175 ^ [], 173 ^ []), 175 ^ [])],extension(152 ^ 2,bind([[_35805, _35807], [175 ^ [], 173 ^ []]]))).
% 0.32/1.39 %-----------------------------------------------------
% 0.32/1.39 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------