%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO226+2 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n017.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:18 EDT 2023
% Result : Theorem 0.32s 1.37s
% Output : Proof 0.32s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.12 % Problem : GEO226+2 : TPTP v8.1.2. Released v3.3.0.
% 0.09/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n017.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 03:32:01 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.32/1.37
% 0.32/1.37 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.32/1.37 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.32/1.37 %-----------------------------------------------------
% 0.32/1.37 ncf(matrix, plain, [(160 ^ _26390) ^ [] : [-(line(157 ^ []))], (162 ^ _26390) ^ [] : [-(line(158 ^ []))], (164 ^ _26390) ^ [] : [-(convergent_lines(157 ^ [], 158 ^ []))], (166 ^ _26390) ^ [_31691] : [-(point(_31691))], (168 ^ _26390) ^ [_31749] : [-(apart_point_and_line(_31749, 157 ^ [])), -(apart_point_and_line(_31749, 158 ^ []))], (110 ^ _26390) ^ [_30040, _30042] : [-(line(line_connecting(_30042, _30040))), point(_30042), point(_30040), distinct_points(_30042, _30040)], (124 ^ _26390) ^ [_30428, _30430] : [-(point(intersection_point(_30430, _30428))), line(_30430), line(_30428), convergent_lines(_30430, _30428)], (138 ^ _26390) ^ [_30816, _30818] : [-(line(parallel_through_point(_30818, _30816))), line(_30818), point(_30816)], (148 ^ _26390) ^ [_31095, _31097] : [-(line(orthogonal_through_point(_31097, _31095))), line(_31097), point(_31095)], (2 ^ _26390) ^ [_26493] : [distinct_points(_26493, _26493)], (4 ^ _26390) ^ [_26570] : [distinct_lines(_26570, _26570)], (6 ^ _26390) ^ [_26647] : [convergent_lines(_26647, _26647)], (8 ^ _26390) ^ [_26768, _26770, _26772] : [distinct_points(_26772, _26770), -(distinct_points(_26772, _26768)), -(distinct_points(_26770, _26768))], (18 ^ _26390) ^ [_27092, _27094, _27096] : [distinct_lines(_27096, _27094), -(distinct_lines(_27096, _27092)), -(distinct_lines(_27094, _27092))], (28 ^ _26390) ^ [_27416, _27418, _27420] : [convergent_lines(_27420, _27418), -(convergent_lines(_27420, _27416)), -(convergent_lines(_27418, _27416))], (38 ^ _26390) ^ [_27740, _27742, _27744] : [distinct_points(_27744, _27742), apart_point_and_line(_27740, line_connecting(_27744, _27742)), 45 ^ _26390 : [(46 ^ _26390) ^ [] : [-(distinct_points(_27740, _27744))], (48 ^ _26390) ^ [] : [-(distinct_points(_27740, _27742))]]], (50 ^ _26390) ^ [_28146, _28148, _28150] : [convergent_lines(_28150, _28148), 55 ^ _26390 : [(56 ^ _26390) ^ [] : [apart_point_and_line(_28146, _28150)], (58 ^ _26390) ^ [] : [apart_point_and_line(_28146, _28148)]], -(distinct_points(_28146, intersection_point(_28150, _28148)))], (62 ^ _26390) ^ [_28565, _28567, _28569, _28571] : [distinct_points(_28571, _28569), distinct_lines(_28567, _28565), -(apart_point_and_line(_28571, _28567)), -(apart_point_and_line(_28571, _28565)), -(apart_point_and_line(_28569, _28567)), -(apart_point_and_line(_28569, _28565))], (84 ^ _26390) ^ [_29194, _29196, _29198] : [apart_point_and_line(_29198, _29196), -(distinct_points(_29198, _29194)), -(apart_point_and_line(_29194, _29196))], (104 ^ _26390) ^ [_29808, _29810] : [convergent_lines(_29810, _29808), -(distinct_lines(_29810, _29808))], (94 ^ _26390) ^ [_29518, _29520, _29522] : [apart_point_and_line(_29522, _29520), -(distinct_lines(_29520, _29518)), -(apart_point_and_line(_29522, _29518))]], input).
% 0.32/1.37 ncf('1',plain,[distinct_points(intersection_point(157 ^ [], 158 ^ []), intersection_point(157 ^ [], 158 ^ []))],start(2 ^ 0,bind([[_26493], [intersection_point(157 ^ [], 158 ^ [])]]))).
% 0.32/1.37 ncf('1.1',plain,[-(distinct_points(intersection_point(157 ^ [], 158 ^ []), intersection_point(157 ^ [], 158 ^ []))), convergent_lines(157 ^ [], 158 ^ []), 56 : apart_point_and_line(intersection_point(157 ^ [], 158 ^ []), 157 ^ [])],extension(50 ^ 1,bind([[_28146, _28148, _28150], [intersection_point(157 ^ [], 158 ^ []), 158 ^ [], 157 ^ []]]))).
% 0.32/1.37 ncf('1.1.1',plain,[-(convergent_lines(157 ^ [], 158 ^ []))],extension(164 ^ 2)).
% 0.32/1.37 ncf('1.1.2',plain,[-(apart_point_and_line(intersection_point(157 ^ [], 158 ^ []), 157 ^ [])), -(apart_point_and_line(intersection_point(157 ^ [], 158 ^ []), 158 ^ []))],extension(168 ^ 4,bind([[_31749], [intersection_point(157 ^ [], 158 ^ [])]]))).
% 0.32/1.37 ncf('1.1.2.1',plain,[apart_point_and_line(intersection_point(157 ^ [], 158 ^ []), 158 ^ [])],extension(58 ^ 5)).
% 0.32/1.37 %-----------------------------------------------------
% 0.32/1.37 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------