%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO207+2 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n007.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:13 EDT 2023
% Result : Theorem 0.35s 1.40s
% Output : Proof 0.35s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.13 % Problem : GEO207+2 : TPTP v8.1.2. Released v3.3.0.
% 0.05/0.14 % Command : nanocop.sh %s %d
% 0.14/0.35 % Computer : n007.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Fri May 19 03:59:08 EDT 2023
% 0.14/0.35 % CPUTime :
% 0.35/1.40
% 0.35/1.40 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.35/1.40 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.35/1.40 %-----------------------------------------------------
% 0.35/1.40 ncf(matrix, plain, [(129 ^ _22122) ^ [] : [-(convergent_lines(127 ^ [], 127 ^ []))], (110 ^ _22122) ^ [_25756, _25758] : [convergent_lines(parallel_through_point(_25756, _25758), _25756)], (112 ^ _22122) ^ [_25852, _25854] : [apart_point_and_line(_25854, parallel_through_point(_25852, _25854))], (114 ^ _22122) ^ [_25958, _25960, _25962] : [distinct_lines(_25960, _25958), -(apart_point_and_line(_25962, _25960)), -(apart_point_and_line(_25962, _25958)), -(convergent_lines(_25960, _25958))], (2 ^ _22122) ^ [_22225] : [distinct_points(_22225, _22225)], (4 ^ _22122) ^ [_22302] : [distinct_lines(_22302, _22302)], (6 ^ _22122) ^ [_22379] : [convergent_lines(_22379, _22379)], (8 ^ _22122) ^ [_22500, _22502, _22504] : [distinct_points(_22504, _22502), -(distinct_points(_22504, _22500)), -(distinct_points(_22502, _22500))], (18 ^ _22122) ^ [_22824, _22826, _22828] : [distinct_lines(_22828, _22826), -(distinct_lines(_22828, _22824)), -(distinct_lines(_22826, _22824))], (28 ^ _22122) ^ [_23148, _23150, _23152] : [convergent_lines(_23152, _23150), -(convergent_lines(_23152, _23148)), -(convergent_lines(_23150, _23148))], (38 ^ _22122) ^ [_23472, _23474, _23476] : [distinct_points(_23476, _23474), apart_point_and_line(_23472, line_connecting(_23476, _23474)), 45 ^ _22122 : [(46 ^ _22122) ^ [] : [-(distinct_points(_23472, _23476))], (48 ^ _22122) ^ [] : [-(distinct_points(_23472, _23474))]]], (50 ^ _22122) ^ [_23878, _23880, _23882] : [convergent_lines(_23882, _23880), 55 ^ _22122 : [(56 ^ _22122) ^ [] : [apart_point_and_line(_23878, _23882)], (58 ^ _22122) ^ [] : [apart_point_and_line(_23878, _23880)]], -(distinct_points(_23878, intersection_point(_23882, _23880)))], (62 ^ _22122) ^ [_24297, _24299, _24301, _24303] : [distinct_points(_24303, _24301), distinct_lines(_24299, _24297), -(apart_point_and_line(_24303, _24299)), -(apart_point_and_line(_24303, _24297)), -(apart_point_and_line(_24301, _24299)), -(apart_point_and_line(_24301, _24297))], (84 ^ _22122) ^ [_24926, _24928, _24930] : [apart_point_and_line(_24930, _24928), -(distinct_points(_24930, _24926)), -(apart_point_and_line(_24926, _24928))], (104 ^ _22122) ^ [_25540, _25542] : [convergent_lines(_25542, _25540), -(distinct_lines(_25542, _25540))], (94 ^ _22122) ^ [_25250, _25252, _25254] : [apart_point_and_line(_25254, _25252), -(distinct_lines(_25252, _25250)), -(apart_point_and_line(_25254, _25250))]], input).
% 0.35/1.40 ncf('1',plain,[distinct_lines(127 ^ [], 127 ^ [])],start(4 ^ 0,bind([[_22302], [127 ^ []]]))).
% 0.35/1.40 ncf('1.1',plain,[-(distinct_lines(127 ^ [], 127 ^ [])), convergent_lines(127 ^ [], 127 ^ [])],extension(104 ^ 1,bind([[_25540, _25542], [127 ^ [], 127 ^ []]]))).
% 0.35/1.40 ncf('1.1.1',plain,[-(convergent_lines(127 ^ [], 127 ^ []))],extension(129 ^ 2)).
% 0.35/1.40 %-----------------------------------------------------
% 0.35/1.40 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------