%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO241+1 : TPTP v8.1.2. Bugfixed v6.4.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:20 EDT 2023
% Result : Theorem 0.32s 1.38s
% Output : Proof 0.32s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : GEO241+1 : TPTP v8.1.2. Bugfixed v6.4.0.
% 0.06/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n007.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:05:53 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.32/1.38
% 0.32/1.38 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.32/1.38 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.32/1.38 %-----------------------------------------------------
% 0.32/1.38 ncf(matrix, plain, [(395 ^ _52117) ^ [] : [apart_point_and_line(391 ^ [], 393 ^ [])], (397 ^ _52117) ^ [] : [-(distinct_points(391 ^ [], 392 ^ []))], (399 ^ _52117) ^ [] : [-(left_convergent_lines(393 ^ [], line_connecting(391 ^ [], 392 ^ [])))], (401 ^ _52117) ^ [] : [left_apart_point(392 ^ [], 393 ^ [])], (12 ^ _52117) ^ [_52515, _52517] : [13 ^ _52117 : [(14 ^ _52117) ^ [] : [left_apart_point(_52517, _52515)], (16 ^ _52117) ^ [] : [left_apart_point(_52517, reverse_line(_52515))]], -(apart_point_and_line(_52517, _52515))], (2 ^ _52117) ^ [_52259, _52261] : [apart_point_and_line(_52261, _52259), -(left_apart_point(_52261, _52259)), -(left_apart_point(_52261, reverse_line(_52259)))], (20 ^ _52117) ^ [_52834, _52836] : [convergent_lines(_52836, _52834), 23 ^ _52117 : [(24 ^ _52117) ^ [] : [-(unequally_directed_lines(_52836, _52834))], (26 ^ _52117) ^ [] : [-(unequally_directed_lines(_52836, reverse_line(_52834)))]]], (28 ^ _52117) ^ [_53075, _53077] : [-(convergent_lines(_53077, _53075)), unequally_directed_lines(_53077, _53075), unequally_directed_lines(_53077, reverse_line(_53075))], (38 ^ _52117) ^ [_53423, _53425, _53427] : [divides_points(_53423, _53427, _53425), 43 ^ _52117 : [(44 ^ _52117) ^ [] : [-(left_apart_point(_53427, _53423))], (46 ^ _52117) ^ [] : [-(left_apart_point(_53425, reverse_line(_53423)))]], 47 ^ _52117 : [(48 ^ _52117) ^ [] : [-(left_apart_point(_53427, reverse_line(_53423)))], (50 ^ _52117) ^ [] : [-(left_apart_point(_53425, _53423))]]], (52 ^ _52117) ^ [_53849, _53851, _53853] : [-(divides_points(_53849, _53853, _53851)), 53 ^ _52117 : [(54 ^ _52117) ^ [] : [left_apart_point(_53853, _53849), left_apart_point(_53851, reverse_line(_53849))], (60 ^ _52117) ^ [] : [left_apart_point(_53853, reverse_line(_53849)), left_apart_point(_53851, _53849)]]], (68 ^ _52117) ^ [_54382, _54384, _54386] : [before_on_line(_54386, _54384, _54382), 71 ^ _52117 : [(72 ^ _52117) ^ [] : [-(distinct_points(_54384, _54382))], (74 ^ _52117) ^ [] : [left_apart_point(_54384, _54386)], (76 ^ _52117) ^ [] : [left_apart_point(_54384, reverse_line(_54386))], (78 ^ _52117) ^ [] : [left_apart_point(_54382, _54386)], (80 ^ _52117) ^ [] : [left_apart_point(_54382, reverse_line(_54386))], (82 ^ _52117) ^ [] : [unequally_directed_lines(_54386, line_connecting(_54384, _54382))]]], (84 ^ _52117) ^ [_54952, _54954, _54956] : [-(before_on_line(_54956, _54954, _54952)), distinct_points(_54954, _54952), -(left_apart_point(_54954, _54956)), -(left_apart_point(_54954, reverse_line(_54956))), -(unequally_directed_lines(_54956, line_connecting(_54954, _54952))), -(left_apart_point(_54952, _54956)), -(left_apart_point(_54952, reverse_line(_54956)))], (110 ^ _52117) ^ [_55721, _55723, _55725, _55727] : [between_on_line(_55727, _55725, _55723, _55721), 115 ^ _52117 : [(116 ^ _52117) ^ [] : [-(before_on_line(_55727, _55725, _55723))], (118 ^ _52117) ^ [] : [-(before_on_line(_55727, _55723, _55721))]], 119 ^ _52117 : [(120 ^ _52117) ^ [] : [-(before_on_line(_55727, _55721, _55723))], (122 ^ _52117) ^ [] : [-(before_on_line(_55727, _55723, _55725))]]], (124 ^ _52117) ^ [_56163, _56165, _56167, _56169] : [-(between_on_line(_56169, _56167, _56165, _56163)), 125 ^ _52117 : [(126 ^ _52117) ^ [] : [before_on_line(_56169, _56167, _56165), before_on_line(_56169, _56165, _56163)], (132 ^ _52117) ^ [] : [before_on_line(_56169, _56163, _56165), before_on_line(_56169, _56165, _56167)]]], (140 ^ _52117) ^ [_56641] : [distinct_points(_56641, _56641)], (142 ^ _52117) ^ [_56762, _56764, _56766] : [distinct_points(_56766, _56764), -(distinct_points(_56766, _56762)), -(distinct_points(_56764, _56762))], (152 ^ _52117) ^ [_57042] : [distinct_lines(_57042, _57042)], (154 ^ _52117) ^ [_57163, _57165, _57167] : [distinct_lines(_57167, _57165), -(distinct_lines(_57167, _57163)), -(distinct_lines(_57165, _57163))], (164 ^ _52117) ^ [_57443] : [unequally_directed_lines(_57443, _57443)], (166 ^ _52117) ^ [_57564, _57566, _57568] : [unequally_directed_lines(_57568, _57566), -(unequally_directed_lines(_57568, _57564)), -(unequally_directed_lines(_57566, _57564))], (176 ^ _52117) ^ [_57888, _57890, _57892] : [unequally_directed_lines(_57892, _57890), unequally_directed_lines(_57892, reverse_line(_57890)), 185 ^ _52117 : [(186 ^ _52117) ^ [] : [-(unequally_directed_lines(_57892, _57888))], (188 ^ _52117) ^ [] : [-(unequally_directed_lines(_57892, reverse_line(_57888)))]], 189 ^ _52117 : [(190 ^ _52117) ^ [] : [-(unequally_directed_lines(_57890, _57888))], (192 ^ _52117) ^ [] : [-(unequally_directed_lines(_57890, reverse_line(_57888)))]]], (194 ^ _52117) ^ [_58459, _58461] : [line(_58461), line(_58459), -(unequally_directed_lines(_58461, _58459)), -(unequally_directed_lines(_58461, reverse_line(_58459)))], (208 ^ _52117) ^ [_58850, _58852] : [unequally_directed_lines(_58852, _58850), unequally_directed_lines(_58852, reverse_line(_58850)), -(left_convergent_lines(_58852, _58850)), -(left_convergent_lines(_58852, reverse_line(_58850)))], (222 ^ _52117) ^ [_59253, _59255] : [left_apart_point(_59255, _59253)], (224 ^ _52117) ^ [_59298, _59300] : [left_apart_point(_59300, reverse_line(_59298))], (226 ^ _52117) ^ [_59415, _59417] : [left_convergent_lines(_59417, _59415)], (228 ^ _52117) ^ [_59460, _59462] : [left_convergent_lines(_59462, reverse_line(_59460))], (230 ^ _52117) ^ [_59573, _59575] : [-(line(line_connecting(_59575, _59573))), point(_59575), point(_59573), distinct_points(_59575, _59573)], (244 ^ _52117) ^ [_59961, _59963] : [-(point(intersection_point(_59963, _59961))), line(_59963), line(_59961), unequally_directed_lines(_59963, _59961), unequally_directed_lines(_59963, reverse_line(_59961))], (262 ^ _52117) ^ [_60442, _60444] : [-(line(parallel_through_point(_60444, _60442))), point(_60442), line(_60444)], (272 ^ _52117) ^ [_60727] : [line(_60727), -(line(reverse_line(_60727)))], (278 ^ _52117) ^ [_60931, _60933] : [distinct_points(_60933, _60931), 281 ^ _52117 : [(282 ^ _52117) ^ [] : [apart_point_and_line(_60933, line_connecting(_60933, _60931))], (284 ^ _52117) ^ [] : [apart_point_and_line(_60931, line_connecting(_60933, _60931))]]], (286 ^ _52117) ^ [_61230, _61232] : [293 ^ _52117 : [(294 ^ _52117) ^ [] : [apart_point_and_line(intersection_point(_61232, _61230), _61232)], (296 ^ _52117) ^ [] : [apart_point_and_line(intersection_point(_61232, _61230), _61230)]], unequally_directed_lines(_61232, _61230), unequally_directed_lines(_61232, reverse_line(_61230))], (298 ^ _52117) ^ [_61606, _61608] : [apart_point_and_line(_61608, parallel_through_point(_61606, _61608))], (300 ^ _52117) ^ [_61688] : [distinct_lines(_61688, reverse_line(_61688))], (302 ^ _52117) ^ [_61781, _61783] : [unequally_directed_lines(line_connecting(_61783, _61781), reverse_line(line_connecting(_61781, _61783)))], (304 ^ _52117) ^ [_61882, _61884] : [unequally_directed_lines(parallel_through_point(_61882, _61884), _61882)], (306 ^ _52117) ^ [_62022, _62024, _62026, _62028] : [distinct_points(_62028, _62026), distinct_lines(_62024, _62022), -(left_apart_point(_62028, _62024)), -(left_apart_point(_62026, _62024)), -(left_apart_point(_62028, _62022)), -(left_apart_point(_62026, _62022)), -(left_apart_point(_62028, reverse_line(_62024))), -(left_apart_point(_62026, reverse_line(_62024))), -(left_apart_point(_62028, reverse_line(_62022))), -(left_apart_point(_62026, reverse_line(_62022)))], (344 ^ _52117) ^ [_63059, _63061, _63063] : [distinct_points(_63063, _63061), left_apart_point(_63063, _63059), -(left_apart_point(_63061, _63059)), -(left_convergent_lines(line_connecting(_63063, _63061), _63059))], (358 ^ _52117) ^ [_63484, _63486, _63488] : [left_apart_point(_63488, _63484), -(distinct_points(_63488, _63486)), -(left_apart_point(_63486, _63484))], (382 ^ _52117) ^ [_64211, _64213, _64215] : [left_convergent_lines(_64215, _64213), -(unequally_directed_lines(_64213, _64211)), -(left_convergent_lines(_64215, _64211))], (368 ^ _52117) ^ [_63808, _63810, _63812] : [left_apart_point(_63812, _63810), unequally_directed_lines(_63810, _63808), -(distinct_lines(_63810, _63808)), -(left_apart_point(_63812, reverse_line(_63808)))]], input).
% 0.32/1.38 ncf('1',plain,[left_convergent_lines(393 ^ [], line_connecting(391 ^ [], 392 ^ []))],start(226 ^ 0,bind([[_59415, _59417], [line_connecting(391 ^ [], 392 ^ []), 393 ^ []]]))).
% 0.32/1.38 ncf('1.1',plain,[-(left_convergent_lines(393 ^ [], line_connecting(391 ^ [], 392 ^ [])))],extension(399 ^ 1)).
% 0.32/1.38 %-----------------------------------------------------
% 0.32/1.38 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------