%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO239+1 : TPTP v8.1.2. Bugfixed v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n011.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:19 EDT 2023
% Result : Theorem 0.30s 1.35s
% Output : Proof 0.30s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.10 % Problem : GEO239+1 : TPTP v8.1.2. Bugfixed v6.4.0.
% 0.10/0.10 % Command : nanocop.sh %s %d
% 0.11/0.31 % Computer : n011.cluster.edu
% 0.11/0.31 % Model : x86_64 x86_64
% 0.11/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.31 % Memory : 8042.1875MB
% 0.11/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.31 % CPULimit : 300
% 0.11/0.31 % WCLimit : 300
% 0.11/0.31 % DateTime : Fri May 19 03:59:33 EDT 2023
% 0.17/0.31 % CPUTime :
% 0.30/1.35
% 0.30/1.35 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.30/1.35 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.30/1.35 %-----------------------------------------------------
% 0.30/1.35 ncf(matrix, plain, [(395 ^ _51803) ^ [] : [apart_point_and_line(391 ^ [], 393 ^ [])], (397 ^ _51803) ^ [] : [-(left_apart_point(392 ^ [], 393 ^ []))], (399 ^ _51803) ^ [] : [left_convergent_lines(393 ^ [], line_connecting(391 ^ [], 392 ^ []))], (12 ^ _51803) ^ [_52201, _52203] : [13 ^ _51803 : [(14 ^ _51803) ^ [] : [left_apart_point(_52203, _52201)], (16 ^ _51803) ^ [] : [left_apart_point(_52203, reverse_line(_52201))]], -(apart_point_and_line(_52203, _52201))], (2 ^ _51803) ^ [_51945, _51947] : [apart_point_and_line(_51947, _51945), -(left_apart_point(_51947, _51945)), -(left_apart_point(_51947, reverse_line(_51945)))], (20 ^ _51803) ^ [_52520, _52522] : [convergent_lines(_52522, _52520), 23 ^ _51803 : [(24 ^ _51803) ^ [] : [-(unequally_directed_lines(_52522, _52520))], (26 ^ _51803) ^ [] : [-(unequally_directed_lines(_52522, reverse_line(_52520)))]]], (28 ^ _51803) ^ [_52761, _52763] : [-(convergent_lines(_52763, _52761)), unequally_directed_lines(_52763, _52761), unequally_directed_lines(_52763, reverse_line(_52761))], (38 ^ _51803) ^ [_53109, _53111, _53113] : [divides_points(_53109, _53113, _53111), 43 ^ _51803 : [(44 ^ _51803) ^ [] : [-(left_apart_point(_53113, _53109))], (46 ^ _51803) ^ [] : [-(left_apart_point(_53111, reverse_line(_53109)))]], 47 ^ _51803 : [(48 ^ _51803) ^ [] : [-(left_apart_point(_53113, reverse_line(_53109)))], (50 ^ _51803) ^ [] : [-(left_apart_point(_53111, _53109))]]], (52 ^ _51803) ^ [_53535, _53537, _53539] : [-(divides_points(_53535, _53539, _53537)), 53 ^ _51803 : [(54 ^ _51803) ^ [] : [left_apart_point(_53539, _53535), left_apart_point(_53537, reverse_line(_53535))], (60 ^ _51803) ^ [] : [left_apart_point(_53539, reverse_line(_53535)), left_apart_point(_53537, _53535)]]], (68 ^ _51803) ^ [_54068, _54070, _54072] : [before_on_line(_54072, _54070, _54068), 71 ^ _51803 : [(72 ^ _51803) ^ [] : [-(distinct_points(_54070, _54068))], (74 ^ _51803) ^ [] : [left_apart_point(_54070, _54072)], (76 ^ _51803) ^ [] : [left_apart_point(_54070, reverse_line(_54072))], (78 ^ _51803) ^ [] : [left_apart_point(_54068, _54072)], (80 ^ _51803) ^ [] : [left_apart_point(_54068, reverse_line(_54072))], (82 ^ _51803) ^ [] : [unequally_directed_lines(_54072, line_connecting(_54070, _54068))]]], (84 ^ _51803) ^ [_54638, _54640, _54642] : [-(before_on_line(_54642, _54640, _54638)), distinct_points(_54640, _54638), -(left_apart_point(_54640, _54642)), -(left_apart_point(_54640, reverse_line(_54642))), -(unequally_directed_lines(_54642, line_connecting(_54640, _54638))), -(left_apart_point(_54638, _54642)), -(left_apart_point(_54638, reverse_line(_54642)))], (110 ^ _51803) ^ [_55407, _55409, _55411, _55413] : [between_on_line(_55413, _55411, _55409, _55407), 115 ^ _51803 : [(116 ^ _51803) ^ [] : [-(before_on_line(_55413, _55411, _55409))], (118 ^ _51803) ^ [] : [-(before_on_line(_55413, _55409, _55407))]], 119 ^ _51803 : [(120 ^ _51803) ^ [] : [-(before_on_line(_55413, _55407, _55409))], (122 ^ _51803) ^ [] : [-(before_on_line(_55413, _55409, _55411))]]], (124 ^ _51803) ^ [_55849, _55851, _55853, _55855] : [-(between_on_line(_55855, _55853, _55851, _55849)), 125 ^ _51803 : [(126 ^ _51803) ^ [] : [before_on_line(_55855, _55853, _55851), before_on_line(_55855, _55851, _55849)], (132 ^ _51803) ^ [] : [before_on_line(_55855, _55849, _55851), before_on_line(_55855, _55851, _55853)]]], (140 ^ _51803) ^ [_56327] : [distinct_points(_56327, _56327)], (142 ^ _51803) ^ [_56448, _56450, _56452] : [distinct_points(_56452, _56450), -(distinct_points(_56452, _56448)), -(distinct_points(_56450, _56448))], (152 ^ _51803) ^ [_56728] : [distinct_lines(_56728, _56728)], (154 ^ _51803) ^ [_56849, _56851, _56853] : [distinct_lines(_56853, _56851), -(distinct_lines(_56853, _56849)), -(distinct_lines(_56851, _56849))], (164 ^ _51803) ^ [_57129] : [unequally_directed_lines(_57129, _57129)], (166 ^ _51803) ^ [_57250, _57252, _57254] : [unequally_directed_lines(_57254, _57252), -(unequally_directed_lines(_57254, _57250)), -(unequally_directed_lines(_57252, _57250))], (176 ^ _51803) ^ [_57574, _57576, _57578] : [unequally_directed_lines(_57578, _57576), unequally_directed_lines(_57578, reverse_line(_57576)), 185 ^ _51803 : [(186 ^ _51803) ^ [] : [-(unequally_directed_lines(_57578, _57574))], (188 ^ _51803) ^ [] : [-(unequally_directed_lines(_57578, reverse_line(_57574)))]], 189 ^ _51803 : [(190 ^ _51803) ^ [] : [-(unequally_directed_lines(_57576, _57574))], (192 ^ _51803) ^ [] : [-(unequally_directed_lines(_57576, reverse_line(_57574)))]]], (194 ^ _51803) ^ [_58145, _58147] : [line(_58147), line(_58145), -(unequally_directed_lines(_58147, _58145)), -(unequally_directed_lines(_58147, reverse_line(_58145)))], (208 ^ _51803) ^ [_58536, _58538] : [unequally_directed_lines(_58538, _58536), unequally_directed_lines(_58538, reverse_line(_58536)), -(left_convergent_lines(_58538, _58536)), -(left_convergent_lines(_58538, reverse_line(_58536)))], (222 ^ _51803) ^ [_58939, _58941] : [left_apart_point(_58941, _58939)], (224 ^ _51803) ^ [_58984, _58986] : [left_apart_point(_58986, reverse_line(_58984))], (226 ^ _51803) ^ [_59101, _59103] : [left_convergent_lines(_59103, _59101)], (228 ^ _51803) ^ [_59146, _59148] : [left_convergent_lines(_59148, reverse_line(_59146))], (230 ^ _51803) ^ [_59259, _59261] : [-(line(line_connecting(_59261, _59259))), point(_59261), point(_59259), distinct_points(_59261, _59259)], (244 ^ _51803) ^ [_59647, _59649] : [-(point(intersection_point(_59649, _59647))), line(_59649), line(_59647), unequally_directed_lines(_59649, _59647), unequally_directed_lines(_59649, reverse_line(_59647))], (262 ^ _51803) ^ [_60128, _60130] : [-(line(parallel_through_point(_60130, _60128))), point(_60128), line(_60130)], (272 ^ _51803) ^ [_60413] : [line(_60413), -(line(reverse_line(_60413)))], (278 ^ _51803) ^ [_60617, _60619] : [distinct_points(_60619, _60617), 281 ^ _51803 : [(282 ^ _51803) ^ [] : [apart_point_and_line(_60619, line_connecting(_60619, _60617))], (284 ^ _51803) ^ [] : [apart_point_and_line(_60617, line_connecting(_60619, _60617))]]], (286 ^ _51803) ^ [_60916, _60918] : [293 ^ _51803 : [(294 ^ _51803) ^ [] : [apart_point_and_line(intersection_point(_60918, _60916), _60918)], (296 ^ _51803) ^ [] : [apart_point_and_line(intersection_point(_60918, _60916), _60916)]], unequally_directed_lines(_60918, _60916), unequally_directed_lines(_60918, reverse_line(_60916))], (298 ^ _51803) ^ [_61292, _61294] : [apart_point_and_line(_61294, parallel_through_point(_61292, _61294))], (300 ^ _51803) ^ [_61374] : [distinct_lines(_61374, reverse_line(_61374))], (302 ^ _51803) ^ [_61467, _61469] : [unequally_directed_lines(line_connecting(_61469, _61467), reverse_line(line_connecting(_61467, _61469)))], (304 ^ _51803) ^ [_61568, _61570] : [unequally_directed_lines(parallel_through_point(_61568, _61570), _61568)], (306 ^ _51803) ^ [_61708, _61710, _61712, _61714] : [distinct_points(_61714, _61712), distinct_lines(_61710, _61708), -(left_apart_point(_61714, _61710)), -(left_apart_point(_61712, _61710)), -(left_apart_point(_61714, _61708)), -(left_apart_point(_61712, _61708)), -(left_apart_point(_61714, reverse_line(_61710))), -(left_apart_point(_61712, reverse_line(_61710))), -(left_apart_point(_61714, reverse_line(_61708))), -(left_apart_point(_61712, reverse_line(_61708)))], (344 ^ _51803) ^ [_62745, _62747, _62749] : [distinct_points(_62749, _62747), left_apart_point(_62749, _62745), -(left_apart_point(_62747, _62745)), -(left_convergent_lines(line_connecting(_62749, _62747), _62745))], (358 ^ _51803) ^ [_63170, _63172, _63174] : [left_apart_point(_63174, _63170), -(distinct_points(_63174, _63172)), -(left_apart_point(_63172, _63170))], (382 ^ _51803) ^ [_63897, _63899, _63901] : [left_convergent_lines(_63901, _63899), -(unequally_directed_lines(_63899, _63897)), -(left_convergent_lines(_63901, _63897))], (368 ^ _51803) ^ [_63494, _63496, _63498] : [left_apart_point(_63498, _63496), unequally_directed_lines(_63496, _63494), -(distinct_lines(_63496, _63494)), -(left_apart_point(_63498, reverse_line(_63494)))]], input).
% 0.30/1.35 ncf('1',plain,[left_apart_point(392 ^ [], 393 ^ [])],start(222 ^ 0,bind([[_58939, _58941], [393 ^ [], 392 ^ []]]))).
% 0.30/1.35 ncf('1.1',plain,[-(left_apart_point(392 ^ [], 393 ^ []))],extension(397 ^ 1)).
% 0.30/1.35 %-----------------------------------------------------
% 0.30/1.35 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------