%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO220+2 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n020.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.33s 1.39s
% Output : Proof 0.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO220+2 : TPTP v8.1.2. Released v3.3.0.
% 0.07/0.13 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n020.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Fri May 19 04:27:17 EDT 2023
% 0.13/0.34 % CPUTime :
% 0.33/1.39
% 0.33/1.39 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.33/1.39 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.33/1.39 %-----------------------------------------------------
% 0.33/1.39 ncf(matrix, plain, [(147 ^ _25426) ^ [] : [unorthogonal_lines(143 ^ [], 144 ^ [])], (149 ^ _25426) ^ [] : [unorthogonal_lines(143 ^ [], 145 ^ [])], (151 ^ _25426) ^ [] : [-(convergent_lines(144 ^ [], 145 ^ []))], (110 ^ _25426) ^ [_29076, _29078] : [-(convergent_lines(_29078, _29076)), -(unorthogonal_lines(_29078, _29076))], (134 ^ _25426) ^ [_29870, _29872, _29874] : [convergent_lines(_29872, _29870), -(unorthogonal_lines(_29874, _29872)), -(unorthogonal_lines(_29874, _29870))], (116 ^ _25426) ^ [_29305, _29307, _29309] : [119 ^ _25426 : [(120 ^ _25426) ^ [] : [-(convergent_lines(_29309, _29307))], (122 ^ _25426) ^ [] : [-(unorthogonal_lines(_29309, _29307))]], 123 ^ _25426 : [(124 ^ _25426) ^ [] : [-(convergent_lines(_29309, _29305))], (126 ^ _25426) ^ [] : [-(unorthogonal_lines(_29309, _29305))]], convergent_lines(_29307, _29305), unorthogonal_lines(_29307, _29305)], (2 ^ _25426) ^ [_25529] : [distinct_points(_25529, _25529)], (4 ^ _25426) ^ [_25606] : [distinct_lines(_25606, _25606)], (6 ^ _25426) ^ [_25683] : [convergent_lines(_25683, _25683)], (8 ^ _25426) ^ [_25804, _25806, _25808] : [distinct_points(_25808, _25806), -(distinct_points(_25808, _25804)), -(distinct_points(_25806, _25804))], (18 ^ _25426) ^ [_26128, _26130, _26132] : [distinct_lines(_26132, _26130), -(distinct_lines(_26132, _26128)), -(distinct_lines(_26130, _26128))], (28 ^ _25426) ^ [_26452, _26454, _26456] : [convergent_lines(_26456, _26454), -(convergent_lines(_26456, _26452)), -(convergent_lines(_26454, _26452))], (38 ^ _25426) ^ [_26776, _26778, _26780] : [distinct_points(_26780, _26778), apart_point_and_line(_26776, line_connecting(_26780, _26778)), 45 ^ _25426 : [(46 ^ _25426) ^ [] : [-(distinct_points(_26776, _26780))], (48 ^ _25426) ^ [] : [-(distinct_points(_26776, _26778))]]], (50 ^ _25426) ^ [_27182, _27184, _27186] : [convergent_lines(_27186, _27184), 55 ^ _25426 : [(56 ^ _25426) ^ [] : [apart_point_and_line(_27182, _27186)], (58 ^ _25426) ^ [] : [apart_point_and_line(_27182, _27184)]], -(distinct_points(_27182, intersection_point(_27186, _27184)))], (62 ^ _25426) ^ [_27601, _27603, _27605, _27607] : [distinct_points(_27607, _27605), distinct_lines(_27603, _27601), -(apart_point_and_line(_27607, _27603)), -(apart_point_and_line(_27607, _27601)), -(apart_point_and_line(_27605, _27603)), -(apart_point_and_line(_27605, _27601))], (84 ^ _25426) ^ [_28230, _28232, _28234] : [apart_point_and_line(_28234, _28232), -(distinct_points(_28234, _28230)), -(apart_point_and_line(_28230, _28232))], (104 ^ _25426) ^ [_28844, _28846] : [convergent_lines(_28846, _28844), -(distinct_lines(_28846, _28844))], (94 ^ _25426) ^ [_28554, _28556, _28558] : [apart_point_and_line(_28558, _28556), -(distinct_lines(_28556, _28554)), -(apart_point_and_line(_28558, _28554))]], input).
% 0.33/1.39 ncf('1',plain,[unorthogonal_lines(143 ^ [], 144 ^ [])],start(147 ^ 0)).
% 0.33/1.39 ncf('1.1',plain,[-(unorthogonal_lines(143 ^ [], 144 ^ [])), convergent_lines(144 ^ [], 145 ^ []), -(unorthogonal_lines(143 ^ [], 145 ^ []))],extension(134 ^ 1,bind([[_29870, _29872, _29874], [145 ^ [], 144 ^ [], 143 ^ []]]))).
% 0.33/1.39 ncf('1.1.1',plain,[-(convergent_lines(144 ^ [], 145 ^ []))],extension(151 ^ 2)).
% 0.33/1.39 ncf('1.1.2',plain,[unorthogonal_lines(143 ^ [], 145 ^ [])],extension(149 ^ 2)).
% 0.33/1.39 %-----------------------------------------------------
% 0.33/1.39 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------