%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO234+3 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n008.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 1.03s 1.36s
% Output : Proof 1.03s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.11 % Problem : GEO234+3 : TPTP v8.1.2. Released v4.0.0.
% 0.10/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n008.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Fri May 19 04:08:39 EDT 2023
% 0.12/0.33 % CPUTime :
% 1.03/1.36
% 1.03/1.36 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 1.03/1.36 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.03/1.36 %-----------------------------------------------------
% 1.03/1.36 ncf(matrix, plain, [(439 ^ _59344) ^ [] : [-(unequally_directed_opposite_lines(435 ^ [], 436 ^ []))], (441 ^ _59344) ^ [] : [unequally_directed_lines(435 ^ [], 437 ^ [])], (443 ^ _59344) ^ [] : [unequally_directed_opposite_lines(436 ^ [], 437 ^ [])], (2 ^ _59344) ^ [_59486, _59488] : [unequally_directed_opposite_lines(_59488, _59486), -(unequally_directed_lines(_59488, reverse_line(_59486)))], (8 ^ _59344) ^ [_59652, _59654] : [unequally_directed_lines(_59654, reverse_line(_59652)), -(unequally_directed_opposite_lines(_59654, _59652))], (14 ^ _59344) ^ [_59897, _59899] : [right_apart_point(_59899, _59897), -(left_apart_point(_59899, reverse_line(_59897)))], (20 ^ _59344) ^ [_60063, _60065] : [left_apart_point(_60065, reverse_line(_60063)), -(right_apart_point(_60065, _60063))], (26 ^ _59344) ^ [_60308, _60310] : [right_convergent_lines(_60310, _60308), -(left_convergent_lines(_60310, reverse_line(_60308)))], (32 ^ _59344) ^ [_60474, _60476] : [left_convergent_lines(_60476, reverse_line(_60474)), -(right_convergent_lines(_60476, _60474))], (38 ^ _59344) ^ [_60719, _60721] : [equally_directed_lines(_60721, _60719), unequally_directed_lines(_60721, _60719)], (44 ^ _59344) ^ [_60882, _60884] : [-(unequally_directed_lines(_60884, _60882)), -(equally_directed_lines(_60884, _60882))], (50 ^ _59344) ^ [_61126, _61128] : [equally_directed_opposite_lines(_61128, _61126), unequally_directed_opposite_lines(_61128, _61126)], (56 ^ _59344) ^ [_61289, _61291] : [-(unequally_directed_opposite_lines(_61291, _61289)), -(equally_directed_opposite_lines(_61291, _61289))], (72 ^ _59344) ^ [_61785, _61787] : [73 ^ _59344 : [(74 ^ _59344) ^ [] : [left_apart_point(_61787, _61785)], (76 ^ _59344) ^ [] : [right_apart_point(_61787, _61785)]], -(apart_point_and_line(_61787, _61785))], (62 ^ _59344) ^ [_61533, _61535] : [apart_point_and_line(_61535, _61533), -(left_apart_point(_61535, _61533)), -(right_apart_point(_61535, _61533))], (80 ^ _59344) ^ [_62100, _62102] : [convergent_lines(_62102, _62100), 83 ^ _59344 : [(84 ^ _59344) ^ [] : [-(unequally_directed_lines(_62102, _62100))], (86 ^ _59344) ^ [] : [-(unequally_directed_opposite_lines(_62102, _62100))]]], (88 ^ _59344) ^ [_62337, _62339] : [-(convergent_lines(_62339, _62337)), unequally_directed_lines(_62339, _62337), unequally_directed_opposite_lines(_62339, _62337)], (98 ^ _59344) ^ [_62681, _62683, _62685] : [divides_points(_62681, _62685, _62683), 103 ^ _59344 : [(104 ^ _59344) ^ [] : [-(left_apart_point(_62685, _62681))], (106 ^ _59344) ^ [] : [-(right_apart_point(_62683, _62681))]], 107 ^ _59344 : [(108 ^ _59344) ^ [] : [-(right_apart_point(_62685, _62681))], (110 ^ _59344) ^ [] : [-(left_apart_point(_62683, _62681))]]], (112 ^ _59344) ^ [_63099, _63101, _63103] : [-(divides_points(_63099, _63103, _63101)), 113 ^ _59344 : [(114 ^ _59344) ^ [] : [left_apart_point(_63103, _63099), right_apart_point(_63101, _63099)], (120 ^ _59344) ^ [] : [right_apart_point(_63103, _63099), left_apart_point(_63101, _63099)]]], (128 ^ _59344) ^ [_63624, _63626, _63628] : [before_on_line(_63628, _63626, _63624), 131 ^ _59344 : [(132 ^ _59344) ^ [] : [-(distinct_points(_63626, _63624))], (134 ^ _59344) ^ [] : [-(incident_point_and_line(_63626, _63628))], (136 ^ _59344) ^ [] : [-(incident_point_and_line(_63624, _63628))], (138 ^ _59344) ^ [] : [-(equally_directed_lines(_63628, line_connecting(_63626, _63624)))]]], (140 ^ _59344) ^ [_64029, _64031, _64033] : [-(before_on_line(_64033, _64031, _64029)), distinct_points(_64031, _64029), incident_point_and_line(_64031, _64033), incident_point_and_line(_64029, _64033), equally_directed_lines(_64033, line_connecting(_64031, _64029))], (158 ^ _59344) ^ [_64591, _64593, _64595, _64597] : [between_on_line(_64597, _64595, _64593, _64591), 163 ^ _59344 : [(164 ^ _59344) ^ [] : [-(before_on_line(_64597, _64595, _64593))], (166 ^ _59344) ^ [] : [-(before_on_line(_64597, _64593, _64591))]], 167 ^ _59344 : [(168 ^ _59344) ^ [] : [-(before_on_line(_64597, _64591, _64593))], (170 ^ _59344) ^ [] : [-(before_on_line(_64597, _64593, _64595))]]], (172 ^ _59344) ^ [_65033, _65035, _65037, _65039] : [-(between_on_line(_65039, _65037, _65035, _65033)), 173 ^ _59344 : [(174 ^ _59344) ^ [] : [before_on_line(_65039, _65037, _65035), before_on_line(_65039, _65035, _65033)], (180 ^ _59344) ^ [] : [before_on_line(_65039, _65033, _65035), before_on_line(_65039, _65035, _65037)]]], (188 ^ _59344) ^ [_65511] : [distinct_points(_65511, _65511)], (190 ^ _59344) ^ [_65632, _65634, _65636] : [distinct_points(_65636, _65634), -(distinct_points(_65636, _65632)), -(distinct_points(_65634, _65632))], (200 ^ _59344) ^ [_65912] : [distinct_lines(_65912, _65912)], (202 ^ _59344) ^ [_66033, _66035, _66037] : [distinct_lines(_66037, _66035), -(distinct_lines(_66037, _66033)), -(distinct_lines(_66035, _66033))], (212 ^ _59344) ^ [_66314] : [-(equally_directed_lines(_66314, _66314))], (214 ^ _59344) ^ [_66435, _66437, _66439] : [unequally_directed_lines(_66439, _66437), -(unequally_directed_lines(_66439, _66435)), -(unequally_directed_lines(_66437, _66435))], (224 ^ _59344) ^ [_66759, _66761, _66763] : [unequally_directed_lines(_66763, _66761), unequally_directed_lines(_66763, reverse_line(_66761)), 233 ^ _59344 : [(234 ^ _59344) ^ [] : [-(unequally_directed_lines(_66763, _66759))], (236 ^ _59344) ^ [] : [-(unequally_directed_lines(_66763, reverse_line(_66759)))]], 237 ^ _59344 : [(238 ^ _59344) ^ [] : [-(unequally_directed_lines(_66761, _66759))], (240 ^ _59344) ^ [] : [-(unequally_directed_lines(_66761, reverse_line(_66759)))]]], (242 ^ _59344) ^ [_67330, _67332] : [-(unequally_directed_lines(_67332, _67330)), -(unequally_directed_lines(_67332, reverse_line(_67330)))], (248 ^ _59344) ^ [_67545, _67547] : [unequally_directed_lines(_67547, _67545), unequally_directed_lines(_67547, reverse_line(_67545)), -(left_convergent_lines(_67547, _67545)), -(left_convergent_lines(_67547, reverse_line(_67545)))], (262 ^ _59344) ^ [_67948, _67950] : [left_apart_point(_67950, _67948)], (264 ^ _59344) ^ [_67993, _67995] : [left_apart_point(_67995, reverse_line(_67993))], (266 ^ _59344) ^ [_68110, _68112] : [left_convergent_lines(_68112, _68110)], (268 ^ _59344) ^ [_68155, _68157] : [left_convergent_lines(_68157, reverse_line(_68155))], (270 ^ _59344) ^ [_68268, _68270] : [-(line(line_connecting(_68270, _68268))), point(_68270), point(_68268), distinct_points(_68270, _68268)], (284 ^ _59344) ^ [_68656, _68658] : [-(point(intersection_point(_68658, _68656))), line(_68658), line(_68656), unequally_directed_lines(_68658, _68656), unequally_directed_lines(_68658, reverse_line(_68656))], (302 ^ _59344) ^ [_69137, _69139] : [-(line(parallel_through_point(_69139, _69137))), point(_69137), line(_69139)], (312 ^ _59344) ^ [_69422] : [line(_69422), -(line(reverse_line(_69422)))], (318 ^ _59344) ^ [_69626, _69628] : [distinct_points(_69628, _69626), 321 ^ _59344 : [(322 ^ _59344) ^ [] : [apart_point_and_line(_69628, line_connecting(_69628, _69626))], (324 ^ _59344) ^ [] : [apart_point_and_line(_69626, line_connecting(_69628, _69626))]]], (326 ^ _59344) ^ [_69925, _69927] : [333 ^ _59344 : [(334 ^ _59344) ^ [] : [apart_point_and_line(intersection_point(_69927, _69925), _69927)], (336 ^ _59344) ^ [] : [apart_point_and_line(intersection_point(_69927, _69925), _69925)]], unequally_directed_lines(_69927, _69925), unequally_directed_lines(_69927, reverse_line(_69925))], (338 ^ _59344) ^ [_70301, _70303] : [apart_point_and_line(_70303, parallel_through_point(_70301, _70303))], (340 ^ _59344) ^ [_70383] : [distinct_lines(_70383, reverse_line(_70383))], (342 ^ _59344) ^ [_70492, _70494] : [distinct_points(_70494, _70492), -(equally_directed_lines(line_connecting(_70494, _70492), reverse_line(line_connecting(_70492, _70494))))], (348 ^ _59344) ^ [_70703, _70705] : [-(equally_directed_lines(parallel_through_point(_70703, _70705), _70703))], (350 ^ _59344) ^ [_70843, _70845, _70847, _70849] : [distinct_points(_70849, _70847), distinct_lines(_70845, _70843), -(left_apart_point(_70849, _70845)), -(left_apart_point(_70847, _70845)), -(left_apart_point(_70849, _70843)), -(left_apart_point(_70847, _70843)), -(left_apart_point(_70849, reverse_line(_70845))), -(left_apart_point(_70847, reverse_line(_70845))), -(left_apart_point(_70849, reverse_line(_70843))), -(left_apart_point(_70847, reverse_line(_70843)))], (388 ^ _59344) ^ [_71880, _71882, _71884] : [distinct_points(_71884, _71882), left_apart_point(_71884, _71880), -(left_apart_point(_71882, _71880)), -(left_convergent_lines(line_connecting(_71884, _71882), _71880))], (402 ^ _59344) ^ [_72305, _72307, _72309] : [left_apart_point(_72309, _72305), -(distinct_points(_72309, _72307)), -(left_apart_point(_72307, _72305))], (426 ^ _59344) ^ [_73032, _73034, _73036] : [left_convergent_lines(_73036, _73034), -(unequally_directed_lines(_73034, _73032)), -(left_convergent_lines(_73036, _73032))], (412 ^ _59344) ^ [_72629, _72631, _72633] : [left_apart_point(_72633, _72631), unequally_directed_lines(_72631, _72629), -(distinct_lines(_72631, _72629)), -(left_apart_point(_72633, reverse_line(_72629)))]], input).
% 1.03/1.36 ncf('1',plain,[unequally_directed_opposite_lines(436 ^ [], 437 ^ [])],start(443 ^ 0)).
% 1.03/1.36 ncf('1.1',plain,[-(unequally_directed_opposite_lines(436 ^ [], 437 ^ [])), unequally_directed_lines(436 ^ [], reverse_line(437 ^ []))],extension(8 ^ 1,bind([[_59652, _59654], [437 ^ [], 436 ^ []]]))).
% 1.03/1.36 ncf('1.1.1',plain,[-(unequally_directed_lines(436 ^ [], reverse_line(437 ^ []))), unequally_directed_lines(436 ^ [], reverse_line(436 ^ [])), -(unequally_directed_lines(reverse_line(436 ^ []), reverse_line(437 ^ [])))],extension(214 ^ 2,bind([[_66435, _66437, _66439], [reverse_line(437 ^ []), reverse_line(436 ^ []), 436 ^ []]]))).
% 1.03/1.36 ncf('1.1.1.1',plain,[-(unequally_directed_lines(436 ^ [], reverse_line(436 ^ []))), unequally_directed_lines(436 ^ [], reverse_line(436 ^ [])), -(unequally_directed_lines(reverse_line(436 ^ []), reverse_line(436 ^ [])))],extension(214 ^ 3,bind([[_66435, _66437, _66439], [reverse_line(436 ^ []), reverse_line(436 ^ []), 436 ^ []]]))).
% 1.03/1.36 ncf('1.1.1.1.1',plain,[-(unequally_directed_lines(436 ^ [], reverse_line(436 ^ []))), unequally_directed_lines(436 ^ [], 436 ^ []), -(unequally_directed_lines(436 ^ [], reverse_line(436 ^ [])))],extension(214 ^ 4,bind([[_66435, _66437, _66439], [reverse_line(436 ^ []), 436 ^ [], 436 ^ []]]))).
% 1.03/1.36 ncf('1.1.1.1.1.1',plain,[-(unequally_directed_lines(436 ^ [], 436 ^ [])), -(unequally_directed_lines(436 ^ [], reverse_line(436 ^ [])))],extension(242 ^ 5,bind([[_67330, _67332], [436 ^ [], 436 ^ []]]))).
% 1.03/1.36 ncf('1.1.1.1.1.1.1',plain,[unequally_directed_lines(436 ^ [], reverse_line(436 ^ []))],reduction('1.1.1.1')).
% 1.03/1.36 ncf('1.1.1.1.1.2',plain,[unequally_directed_lines(436 ^ [], reverse_line(436 ^ []))],reduction('1.1.1.1')).
% 1.03/1.36 ncf('1.1.1.1.2',plain,[unequally_directed_lines(reverse_line(436 ^ []), reverse_line(436 ^ [])), equally_directed_lines(reverse_line(436 ^ []), reverse_line(436 ^ []))],extension(38 ^ 4,bind([[_60719, _60721], [reverse_line(436 ^ []), reverse_line(436 ^ [])]]))).
% 1.03/1.36 ncf('1.1.1.1.2.1',plain,[-(equally_directed_lines(reverse_line(436 ^ []), reverse_line(436 ^ [])))],extension(212 ^ 5,bind([[_66314], [reverse_line(436 ^ [])]]))).
% 1.03/1.36 ncf('1.1.1.2',plain,[unequally_directed_lines(reverse_line(436 ^ []), reverse_line(437 ^ [])), unequally_directed_lines(reverse_line(436 ^ []), 437 ^ []), 234 : -(unequally_directed_lines(reverse_line(436 ^ []), reverse_line(436 ^ []))), 238 : -(unequally_directed_lines(437 ^ [], reverse_line(436 ^ [])))],extension(224 ^ 3,bind([[_66759, _66761, _66763], [reverse_line(436 ^ []), 437 ^ [], reverse_line(436 ^ [])]]))).
% 1.03/1.36 ncf('1.1.1.2.1',plain,[-(unequally_directed_lines(reverse_line(436 ^ []), 437 ^ [])), unequally_directed_lines(435 ^ [], reverse_line(436 ^ [])), -(unequally_directed_lines(435 ^ [], 437 ^ []))],extension(214 ^ 4,bind([[_66435, _66437, _66439], [437 ^ [], reverse_line(436 ^ []), 435 ^ []]]))).
% 1.03/1.36 ncf('1.1.1.2.1.1',plain,[-(unequally_directed_lines(435 ^ [], reverse_line(436 ^ []))), unequally_directed_opposite_lines(435 ^ [], 436 ^ [])],extension(2 ^ 5,bind([[_59486, _59488], [436 ^ [], 435 ^ []]]))).
% 1.03/1.36 ncf('1.1.1.2.1.1.1',plain,[-(unequally_directed_opposite_lines(435 ^ [], 436 ^ []))],extension(439 ^ 6)).
% 1.03/1.36 ncf('1.1.1.2.1.2',plain,[unequally_directed_lines(435 ^ [], 437 ^ [])],extension(441 ^ 5)).
% 1.03/1.36 ncf('1.1.1.2.2',plain,[unequally_directed_lines(reverse_line(436 ^ []), reverse_line(436 ^ [])), equally_directed_lines(reverse_line(436 ^ []), reverse_line(436 ^ []))],extension(38 ^ 6,bind([[_60719, _60721], [reverse_line(436 ^ []), reverse_line(436 ^ [])]]))).
% 1.03/1.36 ncf('1.1.1.2.2.1',plain,[-(equally_directed_lines(reverse_line(436 ^ []), reverse_line(436 ^ [])))],extension(212 ^ 7,bind([[_66314], [reverse_line(436 ^ [])]]))).
% 1.03/1.36 ncf('1.1.1.2.3',plain,[unequally_directed_lines(437 ^ [], reverse_line(436 ^ [])), unequally_directed_lines(437 ^ [], reverse_line(reverse_line(436 ^ []))), -(left_convergent_lines(437 ^ [], reverse_line(436 ^ []))), -(left_convergent_lines(437 ^ [], reverse_line(reverse_line(436 ^ []))))],extension(248 ^ 6,bind([[_67545, _67547], [reverse_line(436 ^ []), 437 ^ []]]))).
% 1.03/1.36 ncf('1.1.1.2.3.1',plain,[-(unequally_directed_lines(437 ^ [], reverse_line(reverse_line(436 ^ []))))],extension(240 ^ 7)).
% 1.03/1.36 ncf('1.1.1.2.3.2',plain,[left_convergent_lines(437 ^ [], reverse_line(436 ^ []))],extension(266 ^ 7,bind([[_68110, _68112], [reverse_line(436 ^ []), 437 ^ []]]))).
% 1.03/1.36 ncf('1.1.1.2.3.3',plain,[left_convergent_lines(437 ^ [], reverse_line(reverse_line(436 ^ [])))],extension(266 ^ 7,bind([[_68110, _68112], [reverse_line(reverse_line(436 ^ [])), 437 ^ []]]))).
% 1.03/1.36 %-----------------------------------------------------
% 1.03/1.36 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------