%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO221+2 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n013.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:16 EDT 2023
% Result : Theorem 0.37s 1.39s
% Output : Proof 0.37s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : GEO221+2 : TPTP v8.1.2. Released v3.3.0.
% 0.12/0.13 % Command : nanocop.sh %s %d
% 0.14/0.34 % Computer : n013.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Fri May 19 04:27:50 EDT 2023
% 0.14/0.34 % CPUTime :
% 0.37/1.39
% 0.37/1.39 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.37/1.39 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.37/1.39 %-----------------------------------------------------
% 0.37/1.39 ncf(matrix, plain, [(177 ^ _30665) ^ [] : [apart_point_and_line(174 ^ [], orthogonal_through_point(175 ^ [], 173 ^ []))], (179 ^ _30665) ^ [] : [-(distinct_lines(orthogonal_through_point(175 ^ [], 173 ^ []), orthogonal_through_point(175 ^ [], 174 ^ [])))], (110 ^ _30665) ^ [_34319, _34321] : [convergent_lines(parallel_through_point(_34319, _34321), _34319)], (112 ^ _30665) ^ [_34415, _34417] : [apart_point_and_line(_34417, parallel_through_point(_34415, _34417))], (114 ^ _30665) ^ [_34521, _34523, _34525] : [distinct_lines(_34523, _34521), -(apart_point_and_line(_34525, _34523)), -(apart_point_and_line(_34525, _34521)), -(convergent_lines(_34523, _34521))], (128 ^ _30665) ^ [_34929, _34931] : [-(convergent_lines(_34931, _34929)), -(unorthogonal_lines(_34931, _34929))], (134 ^ _30665) ^ [_35154, _35156, _35158] : [convergent_lines(_35158, _35156), unorthogonal_lines(_35158, _35156), 143 ^ _30665 : [(144 ^ _30665) ^ [] : [-(convergent_lines(_35158, _35154))], (146 ^ _30665) ^ [] : [-(unorthogonal_lines(_35158, _35154))]], 147 ^ _30665 : [(148 ^ _30665) ^ [] : [-(convergent_lines(_35156, _35154))], (150 ^ _30665) ^ [] : [-(unorthogonal_lines(_35156, _35154))]]], (152 ^ _30665) ^ [_35697, _35699] : [unorthogonal_lines(orthogonal_through_point(_35697, _35699), _35697)], (154 ^ _30665) ^ [_35793, _35795] : [apart_point_and_line(_35795, orthogonal_through_point(_35793, _35795))], (156 ^ _30665) ^ [_35913, _35915, _35917, _35919] : [distinct_lines(_35917, _35915), -(apart_point_and_line(_35919, _35917)), -(apart_point_and_line(_35919, _35915)), -(unorthogonal_lines(_35917, _35913)), -(unorthogonal_lines(_35915, _35913))], (2 ^ _30665) ^ [_30768] : [distinct_points(_30768, _30768)], (4 ^ _30665) ^ [_30845] : [distinct_lines(_30845, _30845)], (6 ^ _30665) ^ [_30922] : [convergent_lines(_30922, _30922)], (8 ^ _30665) ^ [_31043, _31045, _31047] : [distinct_points(_31047, _31045), -(distinct_points(_31047, _31043)), -(distinct_points(_31045, _31043))], (18 ^ _30665) ^ [_31367, _31369, _31371] : [distinct_lines(_31371, _31369), -(distinct_lines(_31371, _31367)), -(distinct_lines(_31369, _31367))], (28 ^ _30665) ^ [_31691, _31693, _31695] : [convergent_lines(_31695, _31693), -(convergent_lines(_31695, _31691)), -(convergent_lines(_31693, _31691))], (38 ^ _30665) ^ [_32015, _32017, _32019] : [distinct_points(_32019, _32017), apart_point_and_line(_32015, line_connecting(_32019, _32017)), 45 ^ _30665 : [(46 ^ _30665) ^ [] : [-(distinct_points(_32015, _32019))], (48 ^ _30665) ^ [] : [-(distinct_points(_32015, _32017))]]], (50 ^ _30665) ^ [_32421, _32423, _32425] : [convergent_lines(_32425, _32423), 55 ^ _30665 : [(56 ^ _30665) ^ [] : [apart_point_and_line(_32421, _32425)], (58 ^ _30665) ^ [] : [apart_point_and_line(_32421, _32423)]], -(distinct_points(_32421, intersection_point(_32425, _32423)))], (62 ^ _30665) ^ [_32840, _32842, _32844, _32846] : [distinct_points(_32846, _32844), distinct_lines(_32842, _32840), -(apart_point_and_line(_32846, _32842)), -(apart_point_and_line(_32846, _32840)), -(apart_point_and_line(_32844, _32842)), -(apart_point_and_line(_32844, _32840))], (84 ^ _30665) ^ [_33469, _33471, _33473] : [apart_point_and_line(_33473, _33471), -(distinct_points(_33473, _33469)), -(apart_point_and_line(_33469, _33471))], (104 ^ _30665) ^ [_34083, _34085] : [convergent_lines(_34085, _34083), -(distinct_lines(_34085, _34083))], (94 ^ _30665) ^ [_33793, _33795, _33797] : [apart_point_and_line(_33797, _33795), -(distinct_lines(_33795, _33793)), -(apart_point_and_line(_33797, _33793))]], input).
% 0.37/1.39 ncf('1',plain,[apart_point_and_line(174 ^ [], orthogonal_through_point(175 ^ [], 173 ^ []))],start(177 ^ 0)).
% 0.37/1.39 ncf('1.1',plain,[-(apart_point_and_line(174 ^ [], orthogonal_through_point(175 ^ [], 173 ^ []))), distinct_lines(orthogonal_through_point(175 ^ [], 173 ^ []), orthogonal_through_point(175 ^ [], 174 ^ [])), -(apart_point_and_line(174 ^ [], orthogonal_through_point(175 ^ [], 174 ^ []))), -(unorthogonal_lines(orthogonal_through_point(175 ^ [], 173 ^ []), 175 ^ [])), -(unorthogonal_lines(orthogonal_through_point(175 ^ [], 174 ^ []), 175 ^ []))],extension(156 ^ 1,bind([[_35913, _35915, _35917, _35919], [175 ^ [], orthogonal_through_point(175 ^ [], 174 ^ []), orthogonal_through_point(175 ^ [], 173 ^ []), 174 ^ []]]))).
% 0.37/1.39 ncf('1.1.1',plain,[-(distinct_lines(orthogonal_through_point(175 ^ [], 173 ^ []), orthogonal_through_point(175 ^ [], 174 ^ [])))],extension(179 ^ 2)).
% 0.37/1.39 ncf('1.1.2',plain,[apart_point_and_line(174 ^ [], orthogonal_through_point(175 ^ [], 174 ^ []))],extension(154 ^ 2,bind([[_35793, _35795], [175 ^ [], 174 ^ []]]))).
% 0.37/1.39 ncf('1.1.3',plain,[unorthogonal_lines(orthogonal_through_point(175 ^ [], 173 ^ []), 175 ^ [])],extension(152 ^ 2,bind([[_35697, _35699], [175 ^ [], 173 ^ []]]))).
% 0.37/1.39 ncf('1.1.4',plain,[unorthogonal_lines(orthogonal_through_point(175 ^ [], 174 ^ []), 175 ^ [])],extension(152 ^ 2,bind([[_35697, _35699], [175 ^ [], 174 ^ []]]))).
% 0.37/1.39 %-----------------------------------------------------
% 0.37/1.39 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------