%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO174+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n015.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:03 EDT 2023
% Result : Theorem 0.36s 1.40s
% Output : Proof 0.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : GEO174+1 : TPTP v8.1.2. Released v3.3.0.
% 0.13/0.13 % Command : nanocop.sh %s %d
% 0.15/0.35 % Computer : n015.cluster.edu
% 0.15/0.35 % Model : x86_64 x86_64
% 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.35 % Memory : 8042.1875MB
% 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.35 % CPULimit : 300
% 0.15/0.35 % WCLimit : 300
% 0.15/0.35 % DateTime : Fri May 19 04:18:52 EDT 2023
% 0.21/0.35 % CPUTime :
% 0.36/1.40
% 0.36/1.40 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.36/1.40 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.36/1.40 %-----------------------------------------------------
% 0.36/1.40 ncf(matrix, plain, [(128 ^ _22488) ^ [] : [distinct_lines(115 ^ [], line_connecting(113 ^ [], 114 ^ []))], (118 ^ _22488) ^ [] : [-(distinct_points(113 ^ [], 114 ^ []))], (120 ^ _22488) ^ [] : [-(convergent_lines(115 ^ [], 116 ^ []))], (122 ^ _22488) ^ [] : [-(apart_point_and_line(113 ^ [], 115 ^ [])), -(apart_point_and_line(114 ^ [], 115 ^ []))], (2 ^ _22488) ^ [_22571] : [distinct_points(_22571, _22571)], (4 ^ _22488) ^ [_22648] : [distinct_lines(_22648, _22648)], (6 ^ _22488) ^ [_22725] : [convergent_lines(_22725, _22725)], (8 ^ _22488) ^ [_22846, _22848, _22850] : [distinct_points(_22850, _22848), -(distinct_points(_22850, _22846)), -(distinct_points(_22848, _22846))], (18 ^ _22488) ^ [_23170, _23172, _23174] : [distinct_lines(_23174, _23172), -(distinct_lines(_23174, _23170)), -(distinct_lines(_23172, _23170))], (28 ^ _22488) ^ [_23494, _23496, _23498] : [convergent_lines(_23498, _23496), -(convergent_lines(_23498, _23494)), -(convergent_lines(_23496, _23494))], (38 ^ _22488) ^ [_23804, _23806] : [distinct_points(_23806, _23804), apart_point_and_line(_23806, line_connecting(_23806, _23804))], (44 ^ _22488) ^ [_24021, _24023] : [distinct_points(_24023, _24021), apart_point_and_line(_24021, line_connecting(_24023, _24021))], (50 ^ _22488) ^ [_24238, _24240] : [convergent_lines(_24240, _24238), apart_point_and_line(intersection_point(_24240, _24238), _24240)], (56 ^ _22488) ^ [_24455, _24457] : [convergent_lines(_24457, _24455), apart_point_and_line(intersection_point(_24457, _24455), _24455)], (62 ^ _22488) ^ [_24700, _24702, _24704, _24706] : [distinct_points(_24706, _24704), distinct_lines(_24702, _24700), -(apart_point_and_line(_24706, _24702)), -(apart_point_and_line(_24706, _24700)), -(apart_point_and_line(_24704, _24702)), -(apart_point_and_line(_24704, _24700))], (84 ^ _22488) ^ [_25329, _25331, _25333] : [apart_point_and_line(_25333, _25331), -(distinct_points(_25333, _25329)), -(apart_point_and_line(_25329, _25331))], (94 ^ _22488) ^ [_25653, _25655, _25657] : [apart_point_and_line(_25657, _25655), -(distinct_lines(_25655, _25653)), -(apart_point_and_line(_25657, _25653))], (104 ^ _22488) ^ [_25957, _25959, _25961] : [convergent_lines(_25961, _25959), -(distinct_lines(_25959, _25957)), -(convergent_lines(_25961, _25957))]], input).
% 0.36/1.40 ncf('1',plain,[distinct_lines(115 ^ [], line_connecting(113 ^ [], 114 ^ []))],start(128 ^ 0)).
% 0.36/1.40 ncf('1.1',plain,[-(distinct_lines(115 ^ [], line_connecting(113 ^ [], 114 ^ []))), apart_point_and_line(113 ^ [], 115 ^ []), -(apart_point_and_line(113 ^ [], line_connecting(113 ^ [], 114 ^ [])))],extension(94 ^ 1,bind([[_25653, _25655, _25657], [line_connecting(113 ^ [], 114 ^ []), 115 ^ [], 113 ^ []]]))).
% 0.36/1.40 ncf('1.1.1',plain,[-(apart_point_and_line(113 ^ [], 115 ^ [])), -(apart_point_and_line(114 ^ [], 115 ^ []))],extension(122 ^ 2)).
% 0.36/1.40 ncf('1.1.1.1',plain,[apart_point_and_line(114 ^ [], 115 ^ []), -(distinct_lines(115 ^ [], line_connecting(113 ^ [], 114 ^ []))), -(apart_point_and_line(114 ^ [], line_connecting(113 ^ [], 114 ^ [])))],extension(94 ^ 3,bind([[_25653, _25655, _25657], [line_connecting(113 ^ [], 114 ^ []), 115 ^ [], 114 ^ []]]))).
% 0.36/1.40 ncf('1.1.1.1.1',plain,[distinct_lines(115 ^ [], line_connecting(113 ^ [], 114 ^ []))],reduction('1')).
% 0.36/1.40 ncf('1.1.1.1.2',plain,[apart_point_and_line(114 ^ [], line_connecting(113 ^ [], 114 ^ [])), distinct_points(113 ^ [], 114 ^ [])],extension(44 ^ 4,bind([[_24021, _24023], [114 ^ [], 113 ^ []]]))).
% 0.36/1.40 ncf('1.1.1.1.2.1',plain,[-(distinct_points(113 ^ [], 114 ^ []))],extension(118 ^ 5)).
% 0.36/1.40 ncf('1.1.2',plain,[apart_point_and_line(113 ^ [], line_connecting(113 ^ [], 114 ^ [])), distinct_points(113 ^ [], 114 ^ [])],extension(38 ^ 2,bind([[_23804, _23806], [114 ^ [], 113 ^ []]]))).
% 0.36/1.40 ncf('1.1.2.1',plain,[-(distinct_points(113 ^ [], 114 ^ []))],extension(118 ^ 3)).
% 0.36/1.40 %-----------------------------------------------------
% 0.36/1.40 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------