%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO242+3 : TPTP v8.1.2. Released v4.0.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:20 EDT 2023
% Result : Theorem 0.37s 1.40s
% Output : Proof 0.37s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : GEO242+3 : TPTP v8.1.2. Released v4.0.0.
% 0.04/0.13 % Command : nanocop.sh %s %d
% 0.13/0.35 % Computer : n020.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Fri May 19 04:25:32 EDT 2023
% 0.13/0.35 % CPUTime :
% 0.37/1.40
% 0.37/1.40 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.37/1.40 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.37/1.40 %-----------------------------------------------------
% 0.37/1.40 ncf(matrix, plain, [(439 ^ _56257) ^ [] : [-(incident_point_and_line(435 ^ [], 437 ^ []))], (441 ^ _56257) ^ [] : [-(distinct_points(435 ^ [], 436 ^ []))], (443 ^ _56257) ^ [] : [-(right_convergent_lines(437 ^ [], line_connecting(435 ^ [], 436 ^ [])))], (445 ^ _56257) ^ [] : [right_apart_point(436 ^ [], 437 ^ [])], (2 ^ _56257) ^ [_56399, _56401] : [unequally_directed_opposite_lines(_56401, _56399), -(unequally_directed_lines(_56401, reverse_line(_56399)))], (8 ^ _56257) ^ [_56565, _56567] : [unequally_directed_lines(_56567, reverse_line(_56565)), -(unequally_directed_opposite_lines(_56567, _56565))], (14 ^ _56257) ^ [_56810, _56812] : [right_apart_point(_56812, _56810), -(left_apart_point(_56812, reverse_line(_56810)))], (20 ^ _56257) ^ [_56976, _56978] : [left_apart_point(_56978, reverse_line(_56976)), -(right_apart_point(_56978, _56976))], (26 ^ _56257) ^ [_57221, _57223] : [right_convergent_lines(_57223, _57221), -(left_convergent_lines(_57223, reverse_line(_57221)))], (32 ^ _56257) ^ [_57387, _57389] : [left_convergent_lines(_57389, reverse_line(_57387)), -(right_convergent_lines(_57389, _57387))], (38 ^ _56257) ^ [_57632, _57634] : [equally_directed_lines(_57634, _57632), unequally_directed_lines(_57634, _57632)], (44 ^ _56257) ^ [_57795, _57797] : [-(unequally_directed_lines(_57797, _57795)), -(equally_directed_lines(_57797, _57795))], (50 ^ _56257) ^ [_58039, _58041] : [equally_directed_opposite_lines(_58041, _58039), unequally_directed_opposite_lines(_58041, _58039)], (56 ^ _56257) ^ [_58202, _58204] : [-(unequally_directed_opposite_lines(_58204, _58202)), -(equally_directed_opposite_lines(_58204, _58202))], (72 ^ _56257) ^ [_58698, _58700] : [73 ^ _56257 : [(74 ^ _56257) ^ [] : [left_apart_point(_58700, _58698)], (76 ^ _56257) ^ [] : [right_apart_point(_58700, _58698)]], -(apart_point_and_line(_58700, _58698))], (62 ^ _56257) ^ [_58446, _58448] : [apart_point_and_line(_58448, _58446), -(left_apart_point(_58448, _58446)), -(right_apart_point(_58448, _58446))], (80 ^ _56257) ^ [_59013, _59015] : [convergent_lines(_59015, _59013), 83 ^ _56257 : [(84 ^ _56257) ^ [] : [-(unequally_directed_lines(_59015, _59013))], (86 ^ _56257) ^ [] : [-(unequally_directed_opposite_lines(_59015, _59013))]]], (88 ^ _56257) ^ [_59250, _59252] : [-(convergent_lines(_59252, _59250)), unequally_directed_lines(_59252, _59250), unequally_directed_opposite_lines(_59252, _59250)], (98 ^ _56257) ^ [_59594, _59596, _59598] : [divides_points(_59594, _59598, _59596), 103 ^ _56257 : [(104 ^ _56257) ^ [] : [-(left_apart_point(_59598, _59594))], (106 ^ _56257) ^ [] : [-(right_apart_point(_59596, _59594))]], 107 ^ _56257 : [(108 ^ _56257) ^ [] : [-(right_apart_point(_59598, _59594))], (110 ^ _56257) ^ [] : [-(left_apart_point(_59596, _59594))]]], (112 ^ _56257) ^ [_60012, _60014, _60016] : [-(divides_points(_60012, _60016, _60014)), 113 ^ _56257 : [(114 ^ _56257) ^ [] : [left_apart_point(_60016, _60012), right_apart_point(_60014, _60012)], (120 ^ _56257) ^ [] : [right_apart_point(_60016, _60012), left_apart_point(_60014, _60012)]]], (128 ^ _56257) ^ [_60537, _60539, _60541] : [before_on_line(_60541, _60539, _60537), 131 ^ _56257 : [(132 ^ _56257) ^ [] : [-(distinct_points(_60539, _60537))], (134 ^ _56257) ^ [] : [-(incident_point_and_line(_60539, _60541))], (136 ^ _56257) ^ [] : [-(incident_point_and_line(_60537, _60541))], (138 ^ _56257) ^ [] : [-(equally_directed_lines(_60541, line_connecting(_60539, _60537)))]]], (140 ^ _56257) ^ [_60942, _60944, _60946] : [-(before_on_line(_60946, _60944, _60942)), distinct_points(_60944, _60942), incident_point_and_line(_60944, _60946), incident_point_and_line(_60942, _60946), equally_directed_lines(_60946, line_connecting(_60944, _60942))], (158 ^ _56257) ^ [_61504, _61506, _61508, _61510] : [between_on_line(_61510, _61508, _61506, _61504), 163 ^ _56257 : [(164 ^ _56257) ^ [] : [-(before_on_line(_61510, _61508, _61506))], (166 ^ _56257) ^ [] : [-(before_on_line(_61510, _61506, _61504))]], 167 ^ _56257 : [(168 ^ _56257) ^ [] : [-(before_on_line(_61510, _61504, _61506))], (170 ^ _56257) ^ [] : [-(before_on_line(_61510, _61506, _61508))]]], (172 ^ _56257) ^ [_61946, _61948, _61950, _61952] : [-(between_on_line(_61952, _61950, _61948, _61946)), 173 ^ _56257 : [(174 ^ _56257) ^ [] : [before_on_line(_61952, _61950, _61948), before_on_line(_61952, _61948, _61946)], (180 ^ _56257) ^ [] : [before_on_line(_61952, _61946, _61948), before_on_line(_61952, _61948, _61950)]]], (188 ^ _56257) ^ [_62424] : [distinct_points(_62424, _62424)], (190 ^ _56257) ^ [_62545, _62547, _62549] : [distinct_points(_62549, _62547), -(distinct_points(_62549, _62545)), -(distinct_points(_62547, _62545))], (200 ^ _56257) ^ [_62825] : [distinct_lines(_62825, _62825)], (202 ^ _56257) ^ [_62946, _62948, _62950] : [distinct_lines(_62950, _62948), -(distinct_lines(_62950, _62946)), -(distinct_lines(_62948, _62946))], (212 ^ _56257) ^ [_63227] : [-(equally_directed_lines(_63227, _63227))], (214 ^ _56257) ^ [_63348, _63350, _63352] : [unequally_directed_lines(_63352, _63350), -(unequally_directed_lines(_63352, _63348)), -(unequally_directed_lines(_63350, _63348))], (224 ^ _56257) ^ [_63672, _63674, _63676] : [unequally_directed_lines(_63676, _63674), unequally_directed_lines(_63676, reverse_line(_63674)), 233 ^ _56257 : [(234 ^ _56257) ^ [] : [-(unequally_directed_lines(_63676, _63672))], (236 ^ _56257) ^ [] : [-(unequally_directed_lines(_63676, reverse_line(_63672)))]], 237 ^ _56257 : [(238 ^ _56257) ^ [] : [-(unequally_directed_lines(_63674, _63672))], (240 ^ _56257) ^ [] : [-(unequally_directed_lines(_63674, reverse_line(_63672)))]]], (242 ^ _56257) ^ [_64243, _64245] : [-(unequally_directed_lines(_64245, _64243)), -(unequally_directed_lines(_64245, reverse_line(_64243)))], (248 ^ _56257) ^ [_64458, _64460] : [unequally_directed_lines(_64460, _64458), unequally_directed_lines(_64460, reverse_line(_64458)), -(left_convergent_lines(_64460, _64458)), -(left_convergent_lines(_64460, reverse_line(_64458)))], (262 ^ _56257) ^ [_64861, _64863] : [left_apart_point(_64863, _64861)], (264 ^ _56257) ^ [_64906, _64908] : [left_apart_point(_64908, reverse_line(_64906))], (266 ^ _56257) ^ [_65023, _65025] : [left_convergent_lines(_65025, _65023)], (268 ^ _56257) ^ [_65068, _65070] : [left_convergent_lines(_65070, reverse_line(_65068))], (270 ^ _56257) ^ [_65181, _65183] : [-(line(line_connecting(_65183, _65181))), point(_65183), point(_65181), distinct_points(_65183, _65181)], (284 ^ _56257) ^ [_65569, _65571] : [-(point(intersection_point(_65571, _65569))), line(_65571), line(_65569), unequally_directed_lines(_65571, _65569), unequally_directed_lines(_65571, reverse_line(_65569))], (302 ^ _56257) ^ [_66050, _66052] : [-(line(parallel_through_point(_66052, _66050))), point(_66050), line(_66052)], (312 ^ _56257) ^ [_66335] : [line(_66335), -(line(reverse_line(_66335)))], (318 ^ _56257) ^ [_66539, _66541] : [distinct_points(_66541, _66539), 321 ^ _56257 : [(322 ^ _56257) ^ [] : [apart_point_and_line(_66541, line_connecting(_66541, _66539))], (324 ^ _56257) ^ [] : [apart_point_and_line(_66539, line_connecting(_66541, _66539))]]], (326 ^ _56257) ^ [_66838, _66840] : [333 ^ _56257 : [(334 ^ _56257) ^ [] : [apart_point_and_line(intersection_point(_66840, _66838), _66840)], (336 ^ _56257) ^ [] : [apart_point_and_line(intersection_point(_66840, _66838), _66838)]], unequally_directed_lines(_66840, _66838), unequally_directed_lines(_66840, reverse_line(_66838))], (338 ^ _56257) ^ [_67214, _67216] : [apart_point_and_line(_67216, parallel_through_point(_67214, _67216))], (340 ^ _56257) ^ [_67296] : [distinct_lines(_67296, reverse_line(_67296))], (342 ^ _56257) ^ [_67405, _67407] : [distinct_points(_67407, _67405), -(equally_directed_lines(line_connecting(_67407, _67405), reverse_line(line_connecting(_67405, _67407))))], (348 ^ _56257) ^ [_67616, _67618] : [-(equally_directed_lines(parallel_through_point(_67616, _67618), _67616))], (350 ^ _56257) ^ [_67756, _67758, _67760, _67762] : [distinct_points(_67762, _67760), distinct_lines(_67758, _67756), -(left_apart_point(_67762, _67758)), -(left_apart_point(_67760, _67758)), -(left_apart_point(_67762, _67756)), -(left_apart_point(_67760, _67756)), -(left_apart_point(_67762, reverse_line(_67758))), -(left_apart_point(_67760, reverse_line(_67758))), -(left_apart_point(_67762, reverse_line(_67756))), -(left_apart_point(_67760, reverse_line(_67756)))], (388 ^ _56257) ^ [_68793, _68795, _68797] : [distinct_points(_68797, _68795), left_apart_point(_68797, _68793), -(left_apart_point(_68795, _68793)), -(left_convergent_lines(line_connecting(_68797, _68795), _68793))], (402 ^ _56257) ^ [_69218, _69220, _69222] : [left_apart_point(_69222, _69218), -(distinct_points(_69222, _69220)), -(left_apart_point(_69220, _69218))], (426 ^ _56257) ^ [_69945, _69947, _69949] : [left_convergent_lines(_69949, _69947), -(unequally_directed_lines(_69947, _69945)), -(left_convergent_lines(_69949, _69945))], (412 ^ _56257) ^ [_69542, _69544, _69546] : [left_apart_point(_69546, _69544), unequally_directed_lines(_69544, _69542), -(distinct_lines(_69544, _69542)), -(left_apart_point(_69546, reverse_line(_69542)))]], input).
% 0.37/1.40 ncf('1',plain,[left_convergent_lines(437 ^ [], reverse_line(line_connecting(435 ^ [], 436 ^ [])))],start(266 ^ 0,bind([[_65023, _65025], [reverse_line(line_connecting(435 ^ [], 436 ^ [])), 437 ^ []]]))).
% 0.37/1.40 ncf('1.1',plain,[-(left_convergent_lines(437 ^ [], reverse_line(line_connecting(435 ^ [], 436 ^ [])))), right_convergent_lines(437 ^ [], line_connecting(435 ^ [], 436 ^ []))],extension(26 ^ 1,bind([[_57221, _57223], [line_connecting(435 ^ [], 436 ^ []), 437 ^ []]]))).
% 0.37/1.40 ncf('1.1.1',plain,[-(right_convergent_lines(437 ^ [], line_connecting(435 ^ [], 436 ^ [])))],extension(443 ^ 2)).
% 0.37/1.40 %-----------------------------------------------------
% 0.37/1.40 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------