%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO252+1 : TPTP v8.1.2. Bugfixed v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n006.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:21 EDT 2023
% Result : Theorem 0.33s 1.38s
% Output : Proof 0.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : GEO252+1 : TPTP v8.1.2. Bugfixed v6.4.0.
% 0.06/0.12 % Command : nanocop.sh %s %d
% 0.13/0.33 % Computer : n006.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Fri May 19 04:10:06 EDT 2023
% 0.13/0.33 % CPUTime :
% 0.33/1.38
% 0.33/1.38 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.33/1.38 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.33/1.38 %-----------------------------------------------------
% 0.33/1.38 ncf(matrix, plain, [(395 ^ _52100) ^ [] : [-(left_apart_point(391 ^ [], 393 ^ []))], (397 ^ _52100) ^ [] : [-(left_apart_point(392 ^ [], reverse_line(393 ^ [])))], (399 ^ _52100) ^ [] : [distinct_points(391 ^ [], 392 ^ []), left_convergent_lines(line_connecting(391 ^ [], 392 ^ []), 393 ^ [])], (12 ^ _52100) ^ [_52498, _52500] : [13 ^ _52100 : [(14 ^ _52100) ^ [] : [left_apart_point(_52500, _52498)], (16 ^ _52100) ^ [] : [left_apart_point(_52500, reverse_line(_52498))]], -(apart_point_and_line(_52500, _52498))], (2 ^ _52100) ^ [_52242, _52244] : [apart_point_and_line(_52244, _52242), -(left_apart_point(_52244, _52242)), -(left_apart_point(_52244, reverse_line(_52242)))], (20 ^ _52100) ^ [_52817, _52819] : [convergent_lines(_52819, _52817), 23 ^ _52100 : [(24 ^ _52100) ^ [] : [-(unequally_directed_lines(_52819, _52817))], (26 ^ _52100) ^ [] : [-(unequally_directed_lines(_52819, reverse_line(_52817)))]]], (28 ^ _52100) ^ [_53058, _53060] : [-(convergent_lines(_53060, _53058)), unequally_directed_lines(_53060, _53058), unequally_directed_lines(_53060, reverse_line(_53058))], (38 ^ _52100) ^ [_53406, _53408, _53410] : [divides_points(_53406, _53410, _53408), 43 ^ _52100 : [(44 ^ _52100) ^ [] : [-(left_apart_point(_53410, _53406))], (46 ^ _52100) ^ [] : [-(left_apart_point(_53408, reverse_line(_53406)))]], 47 ^ _52100 : [(48 ^ _52100) ^ [] : [-(left_apart_point(_53410, reverse_line(_53406)))], (50 ^ _52100) ^ [] : [-(left_apart_point(_53408, _53406))]]], (52 ^ _52100) ^ [_53832, _53834, _53836] : [-(divides_points(_53832, _53836, _53834)), 53 ^ _52100 : [(54 ^ _52100) ^ [] : [left_apart_point(_53836, _53832), left_apart_point(_53834, reverse_line(_53832))], (60 ^ _52100) ^ [] : [left_apart_point(_53836, reverse_line(_53832)), left_apart_point(_53834, _53832)]]], (68 ^ _52100) ^ [_54365, _54367, _54369] : [before_on_line(_54369, _54367, _54365), 71 ^ _52100 : [(72 ^ _52100) ^ [] : [-(distinct_points(_54367, _54365))], (74 ^ _52100) ^ [] : [left_apart_point(_54367, _54369)], (76 ^ _52100) ^ [] : [left_apart_point(_54367, reverse_line(_54369))], (78 ^ _52100) ^ [] : [left_apart_point(_54365, _54369)], (80 ^ _52100) ^ [] : [left_apart_point(_54365, reverse_line(_54369))], (82 ^ _52100) ^ [] : [unequally_directed_lines(_54369, line_connecting(_54367, _54365))]]], (84 ^ _52100) ^ [_54935, _54937, _54939] : [-(before_on_line(_54939, _54937, _54935)), distinct_points(_54937, _54935), -(left_apart_point(_54937, _54939)), -(left_apart_point(_54937, reverse_line(_54939))), -(unequally_directed_lines(_54939, line_connecting(_54937, _54935))), -(left_apart_point(_54935, _54939)), -(left_apart_point(_54935, reverse_line(_54939)))], (110 ^ _52100) ^ [_55704, _55706, _55708, _55710] : [between_on_line(_55710, _55708, _55706, _55704), 115 ^ _52100 : [(116 ^ _52100) ^ [] : [-(before_on_line(_55710, _55708, _55706))], (118 ^ _52100) ^ [] : [-(before_on_line(_55710, _55706, _55704))]], 119 ^ _52100 : [(120 ^ _52100) ^ [] : [-(before_on_line(_55710, _55704, _55706))], (122 ^ _52100) ^ [] : [-(before_on_line(_55710, _55706, _55708))]]], (124 ^ _52100) ^ [_56146, _56148, _56150, _56152] : [-(between_on_line(_56152, _56150, _56148, _56146)), 125 ^ _52100 : [(126 ^ _52100) ^ [] : [before_on_line(_56152, _56150, _56148), before_on_line(_56152, _56148, _56146)], (132 ^ _52100) ^ [] : [before_on_line(_56152, _56146, _56148), before_on_line(_56152, _56148, _56150)]]], (140 ^ _52100) ^ [_56624] : [distinct_points(_56624, _56624)], (142 ^ _52100) ^ [_56745, _56747, _56749] : [distinct_points(_56749, _56747), -(distinct_points(_56749, _56745)), -(distinct_points(_56747, _56745))], (152 ^ _52100) ^ [_57025] : [distinct_lines(_57025, _57025)], (154 ^ _52100) ^ [_57146, _57148, _57150] : [distinct_lines(_57150, _57148), -(distinct_lines(_57150, _57146)), -(distinct_lines(_57148, _57146))], (164 ^ _52100) ^ [_57426] : [unequally_directed_lines(_57426, _57426)], (166 ^ _52100) ^ [_57547, _57549, _57551] : [unequally_directed_lines(_57551, _57549), -(unequally_directed_lines(_57551, _57547)), -(unequally_directed_lines(_57549, _57547))], (176 ^ _52100) ^ [_57871, _57873, _57875] : [unequally_directed_lines(_57875, _57873), unequally_directed_lines(_57875, reverse_line(_57873)), 185 ^ _52100 : [(186 ^ _52100) ^ [] : [-(unequally_directed_lines(_57875, _57871))], (188 ^ _52100) ^ [] : [-(unequally_directed_lines(_57875, reverse_line(_57871)))]], 189 ^ _52100 : [(190 ^ _52100) ^ [] : [-(unequally_directed_lines(_57873, _57871))], (192 ^ _52100) ^ [] : [-(unequally_directed_lines(_57873, reverse_line(_57871)))]]], (194 ^ _52100) ^ [_58442, _58444] : [line(_58444), line(_58442), -(unequally_directed_lines(_58444, _58442)), -(unequally_directed_lines(_58444, reverse_line(_58442)))], (208 ^ _52100) ^ [_58833, _58835] : [unequally_directed_lines(_58835, _58833), unequally_directed_lines(_58835, reverse_line(_58833)), -(left_convergent_lines(_58835, _58833)), -(left_convergent_lines(_58835, reverse_line(_58833)))], (222 ^ _52100) ^ [_59236, _59238] : [left_apart_point(_59238, _59236)], (224 ^ _52100) ^ [_59281, _59283] : [left_apart_point(_59283, reverse_line(_59281))], (226 ^ _52100) ^ [_59398, _59400] : [left_convergent_lines(_59400, _59398)], (228 ^ _52100) ^ [_59443, _59445] : [left_convergent_lines(_59445, reverse_line(_59443))], (230 ^ _52100) ^ [_59556, _59558] : [-(line(line_connecting(_59558, _59556))), point(_59558), point(_59556), distinct_points(_59558, _59556)], (244 ^ _52100) ^ [_59944, _59946] : [-(point(intersection_point(_59946, _59944))), line(_59946), line(_59944), unequally_directed_lines(_59946, _59944), unequally_directed_lines(_59946, reverse_line(_59944))], (262 ^ _52100) ^ [_60425, _60427] : [-(line(parallel_through_point(_60427, _60425))), point(_60425), line(_60427)], (272 ^ _52100) ^ [_60710] : [line(_60710), -(line(reverse_line(_60710)))], (278 ^ _52100) ^ [_60914, _60916] : [distinct_points(_60916, _60914), 281 ^ _52100 : [(282 ^ _52100) ^ [] : [apart_point_and_line(_60916, line_connecting(_60916, _60914))], (284 ^ _52100) ^ [] : [apart_point_and_line(_60914, line_connecting(_60916, _60914))]]], (286 ^ _52100) ^ [_61213, _61215] : [293 ^ _52100 : [(294 ^ _52100) ^ [] : [apart_point_and_line(intersection_point(_61215, _61213), _61215)], (296 ^ _52100) ^ [] : [apart_point_and_line(intersection_point(_61215, _61213), _61213)]], unequally_directed_lines(_61215, _61213), unequally_directed_lines(_61215, reverse_line(_61213))], (298 ^ _52100) ^ [_61589, _61591] : [apart_point_and_line(_61591, parallel_through_point(_61589, _61591))], (300 ^ _52100) ^ [_61671] : [distinct_lines(_61671, reverse_line(_61671))], (302 ^ _52100) ^ [_61764, _61766] : [unequally_directed_lines(line_connecting(_61766, _61764), reverse_line(line_connecting(_61764, _61766)))], (304 ^ _52100) ^ [_61865, _61867] : [unequally_directed_lines(parallel_through_point(_61865, _61867), _61865)], (306 ^ _52100) ^ [_62005, _62007, _62009, _62011] : [distinct_points(_62011, _62009), distinct_lines(_62007, _62005), -(left_apart_point(_62011, _62007)), -(left_apart_point(_62009, _62007)), -(left_apart_point(_62011, _62005)), -(left_apart_point(_62009, _62005)), -(left_apart_point(_62011, reverse_line(_62007))), -(left_apart_point(_62009, reverse_line(_62007))), -(left_apart_point(_62011, reverse_line(_62005))), -(left_apart_point(_62009, reverse_line(_62005)))], (344 ^ _52100) ^ [_63042, _63044, _63046] : [distinct_points(_63046, _63044), left_apart_point(_63046, _63042), -(left_apart_point(_63044, _63042)), -(left_convergent_lines(line_connecting(_63046, _63044), _63042))], (358 ^ _52100) ^ [_63467, _63469, _63471] : [left_apart_point(_63471, _63467), -(distinct_points(_63471, _63469)), -(left_apart_point(_63469, _63467))], (382 ^ _52100) ^ [_64194, _64196, _64198] : [left_convergent_lines(_64198, _64196), -(unequally_directed_lines(_64196, _64194)), -(left_convergent_lines(_64198, _64194))], (368 ^ _52100) ^ [_63791, _63793, _63795] : [left_apart_point(_63795, _63793), unequally_directed_lines(_63793, _63791), -(distinct_lines(_63793, _63791)), -(left_apart_point(_63795, reverse_line(_63791)))]], input).
% 0.33/1.38 ncf('1',plain,[left_apart_point(391 ^ [], 393 ^ [])],start(222 ^ 0,bind([[_59236, _59238], [393 ^ [], 391 ^ []]]))).
% 0.33/1.38 ncf('1.1',plain,[-(left_apart_point(391 ^ [], 393 ^ []))],extension(395 ^ 1)).
% 0.33/1.38 %-----------------------------------------------------
% 0.33/1.38 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------