%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO178+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n024.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:04 EDT 2023
% Result : Theorem 0.34s 1.37s
% Output : Proof 0.34s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GEO178+1 : TPTP v8.1.2. Released v3.3.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n024.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:07:51 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.34/1.37
% 0.34/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.34/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.34/1.37 %-----------------------------------------------------
% 0.34/1.37 ncf(matrix, plain, [(117 ^ _21943) ^ [] : [-(distinct_points(113 ^ [], 114 ^ []))], (119 ^ _21943) ^ [] : [-(apart_point_and_line(115 ^ [], line_connecting(113 ^ [], 114 ^ [])))], (121 ^ _21943) ^ [] : [distinct_points(115 ^ [], 113 ^ []), distinct_points(115 ^ [], 114 ^ [])], (2 ^ _21943) ^ [_22026] : [distinct_points(_22026, _22026)], (4 ^ _21943) ^ [_22103] : [distinct_lines(_22103, _22103)], (6 ^ _21943) ^ [_22180] : [convergent_lines(_22180, _22180)], (8 ^ _21943) ^ [_22301, _22303, _22305] : [distinct_points(_22305, _22303), -(distinct_points(_22305, _22301)), -(distinct_points(_22303, _22301))], (18 ^ _21943) ^ [_22625, _22627, _22629] : [distinct_lines(_22629, _22627), -(distinct_lines(_22629, _22625)), -(distinct_lines(_22627, _22625))], (28 ^ _21943) ^ [_22949, _22951, _22953] : [convergent_lines(_22953, _22951), -(convergent_lines(_22953, _22949)), -(convergent_lines(_22951, _22949))], (38 ^ _21943) ^ [_23259, _23261] : [distinct_points(_23261, _23259), apart_point_and_line(_23261, line_connecting(_23261, _23259))], (44 ^ _21943) ^ [_23476, _23478] : [distinct_points(_23478, _23476), apart_point_and_line(_23476, line_connecting(_23478, _23476))], (50 ^ _21943) ^ [_23693, _23695] : [convergent_lines(_23695, _23693), apart_point_and_line(intersection_point(_23695, _23693), _23695)], (56 ^ _21943) ^ [_23910, _23912] : [convergent_lines(_23912, _23910), apart_point_and_line(intersection_point(_23912, _23910), _23910)], (62 ^ _21943) ^ [_24155, _24157, _24159, _24161] : [distinct_points(_24161, _24159), distinct_lines(_24157, _24155), -(apart_point_and_line(_24161, _24157)), -(apart_point_and_line(_24161, _24155)), -(apart_point_and_line(_24159, _24157)), -(apart_point_and_line(_24159, _24155))], (84 ^ _21943) ^ [_24784, _24786, _24788] : [apart_point_and_line(_24788, _24786), -(distinct_points(_24788, _24784)), -(apart_point_and_line(_24784, _24786))], (94 ^ _21943) ^ [_25108, _25110, _25112] : [apart_point_and_line(_25112, _25110), -(distinct_lines(_25110, _25108)), -(apart_point_and_line(_25112, _25108))], (104 ^ _21943) ^ [_25412, _25414, _25416] : [convergent_lines(_25416, _25414), -(distinct_lines(_25414, _25412)), -(convergent_lines(_25416, _25412))]], input).
% 0.34/1.37 ncf('1',plain,[distinct_points(115 ^ [], 113 ^ []), distinct_points(115 ^ [], 114 ^ [])],start(121 ^ 0)).
% 0.34/1.37 ncf('1.1',plain,[-(distinct_points(115 ^ [], 113 ^ [])), apart_point_and_line(115 ^ [], line_connecting(113 ^ [], 114 ^ [])), -(apart_point_and_line(113 ^ [], line_connecting(113 ^ [], 114 ^ [])))],extension(84 ^ 1,bind([[_24784, _24786, _24788], [113 ^ [], line_connecting(113 ^ [], 114 ^ []), 115 ^ []]]))).
% 0.34/1.37 ncf('1.1.1',plain,[-(apart_point_and_line(115 ^ [], line_connecting(113 ^ [], 114 ^ [])))],extension(119 ^ 2)).
% 0.34/1.37 ncf('1.1.2',plain,[apart_point_and_line(113 ^ [], line_connecting(113 ^ [], 114 ^ [])), distinct_points(113 ^ [], 114 ^ [])],extension(38 ^ 2,bind([[_23259, _23261], [114 ^ [], 113 ^ []]]))).
% 0.34/1.37 ncf('1.1.2.1',plain,[-(distinct_points(113 ^ [], 114 ^ []))],extension(117 ^ 3)).
% 0.34/1.37 ncf('1.2',plain,[-(distinct_points(115 ^ [], 114 ^ [])), apart_point_and_line(115 ^ [], line_connecting(113 ^ [], 114 ^ [])), -(apart_point_and_line(114 ^ [], line_connecting(113 ^ [], 114 ^ [])))],extension(84 ^ 1,bind([[_24784, _24786, _24788], [114 ^ [], line_connecting(113 ^ [], 114 ^ []), 115 ^ []]]))).
% 0.34/1.37 ncf('1.2.1',plain,[-(apart_point_and_line(115 ^ [], line_connecting(113 ^ [], 114 ^ [])))],extension(119 ^ 2)).
% 0.34/1.37 ncf('1.2.2',plain,[apart_point_and_line(114 ^ [], line_connecting(113 ^ [], 114 ^ [])), distinct_points(113 ^ [], 114 ^ [])],extension(44 ^ 2,bind([[_23476, _23478], [114 ^ [], 113 ^ []]]))).
% 0.34/1.37 ncf('1.2.2.1',plain,[-(distinct_points(113 ^ [], 114 ^ []))],extension(117 ^ 3)).
% 0.34/1.37 %-----------------------------------------------------
% 0.34/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------