%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO248+1 : TPTP v8.1.2. Bugfixed v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n001.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.37s
% Output : Proof 0.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO248+1 : TPTP v8.1.2. Bugfixed v6.4.0.
% 0.07/0.12 % Command : nanocop.sh %s %d
% 0.11/0.33 % Computer : n001.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Fri May 19 04:50:20 EDT 2023
% 0.11/0.33 % CPUTime :
% 0.33/1.37
% 0.33/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.33/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.33/1.37 %-----------------------------------------------------
% 0.33/1.37 ncf(matrix, plain, [(395 ^ _51739) ^ [] : [-(left_apart_point(391 ^ [], 393 ^ []))], (397 ^ _51739) ^ [] : [-(left_apart_point(392 ^ [], parallel_through_point(393 ^ [], 391 ^ [])))], (399 ^ _51739) ^ [] : [left_apart_point(392 ^ [], 393 ^ [])], (12 ^ _51739) ^ [_52137, _52139] : [13 ^ _51739 : [(14 ^ _51739) ^ [] : [left_apart_point(_52139, _52137)], (16 ^ _51739) ^ [] : [left_apart_point(_52139, reverse_line(_52137))]], -(apart_point_and_line(_52139, _52137))], (2 ^ _51739) ^ [_51881, _51883] : [apart_point_and_line(_51883, _51881), -(left_apart_point(_51883, _51881)), -(left_apart_point(_51883, reverse_line(_51881)))], (20 ^ _51739) ^ [_52456, _52458] : [convergent_lines(_52458, _52456), 23 ^ _51739 : [(24 ^ _51739) ^ [] : [-(unequally_directed_lines(_52458, _52456))], (26 ^ _51739) ^ [] : [-(unequally_directed_lines(_52458, reverse_line(_52456)))]]], (28 ^ _51739) ^ [_52697, _52699] : [-(convergent_lines(_52699, _52697)), unequally_directed_lines(_52699, _52697), unequally_directed_lines(_52699, reverse_line(_52697))], (38 ^ _51739) ^ [_53045, _53047, _53049] : [divides_points(_53045, _53049, _53047), 43 ^ _51739 : [(44 ^ _51739) ^ [] : [-(left_apart_point(_53049, _53045))], (46 ^ _51739) ^ [] : [-(left_apart_point(_53047, reverse_line(_53045)))]], 47 ^ _51739 : [(48 ^ _51739) ^ [] : [-(left_apart_point(_53049, reverse_line(_53045)))], (50 ^ _51739) ^ [] : [-(left_apart_point(_53047, _53045))]]], (52 ^ _51739) ^ [_53471, _53473, _53475] : [-(divides_points(_53471, _53475, _53473)), 53 ^ _51739 : [(54 ^ _51739) ^ [] : [left_apart_point(_53475, _53471), left_apart_point(_53473, reverse_line(_53471))], (60 ^ _51739) ^ [] : [left_apart_point(_53475, reverse_line(_53471)), left_apart_point(_53473, _53471)]]], (68 ^ _51739) ^ [_54004, _54006, _54008] : [before_on_line(_54008, _54006, _54004), 71 ^ _51739 : [(72 ^ _51739) ^ [] : [-(distinct_points(_54006, _54004))], (74 ^ _51739) ^ [] : [left_apart_point(_54006, _54008)], (76 ^ _51739) ^ [] : [left_apart_point(_54006, reverse_line(_54008))], (78 ^ _51739) ^ [] : [left_apart_point(_54004, _54008)], (80 ^ _51739) ^ [] : [left_apart_point(_54004, reverse_line(_54008))], (82 ^ _51739) ^ [] : [unequally_directed_lines(_54008, line_connecting(_54006, _54004))]]], (84 ^ _51739) ^ [_54574, _54576, _54578] : [-(before_on_line(_54578, _54576, _54574)), distinct_points(_54576, _54574), -(left_apart_point(_54576, _54578)), -(left_apart_point(_54576, reverse_line(_54578))), -(unequally_directed_lines(_54578, line_connecting(_54576, _54574))), -(left_apart_point(_54574, _54578)), -(left_apart_point(_54574, reverse_line(_54578)))], (110 ^ _51739) ^ [_55343, _55345, _55347, _55349] : [between_on_line(_55349, _55347, _55345, _55343), 115 ^ _51739 : [(116 ^ _51739) ^ [] : [-(before_on_line(_55349, _55347, _55345))], (118 ^ _51739) ^ [] : [-(before_on_line(_55349, _55345, _55343))]], 119 ^ _51739 : [(120 ^ _51739) ^ [] : [-(before_on_line(_55349, _55343, _55345))], (122 ^ _51739) ^ [] : [-(before_on_line(_55349, _55345, _55347))]]], (124 ^ _51739) ^ [_55785, _55787, _55789, _55791] : [-(between_on_line(_55791, _55789, _55787, _55785)), 125 ^ _51739 : [(126 ^ _51739) ^ [] : [before_on_line(_55791, _55789, _55787), before_on_line(_55791, _55787, _55785)], (132 ^ _51739) ^ [] : [before_on_line(_55791, _55785, _55787), before_on_line(_55791, _55787, _55789)]]], (140 ^ _51739) ^ [_56263] : [distinct_points(_56263, _56263)], (142 ^ _51739) ^ [_56384, _56386, _56388] : [distinct_points(_56388, _56386), -(distinct_points(_56388, _56384)), -(distinct_points(_56386, _56384))], (152 ^ _51739) ^ [_56664] : [distinct_lines(_56664, _56664)], (154 ^ _51739) ^ [_56785, _56787, _56789] : [distinct_lines(_56789, _56787), -(distinct_lines(_56789, _56785)), -(distinct_lines(_56787, _56785))], (164 ^ _51739) ^ [_57065] : [unequally_directed_lines(_57065, _57065)], (166 ^ _51739) ^ [_57186, _57188, _57190] : [unequally_directed_lines(_57190, _57188), -(unequally_directed_lines(_57190, _57186)), -(unequally_directed_lines(_57188, _57186))], (176 ^ _51739) ^ [_57510, _57512, _57514] : [unequally_directed_lines(_57514, _57512), unequally_directed_lines(_57514, reverse_line(_57512)), 185 ^ _51739 : [(186 ^ _51739) ^ [] : [-(unequally_directed_lines(_57514, _57510))], (188 ^ _51739) ^ [] : [-(unequally_directed_lines(_57514, reverse_line(_57510)))]], 189 ^ _51739 : [(190 ^ _51739) ^ [] : [-(unequally_directed_lines(_57512, _57510))], (192 ^ _51739) ^ [] : [-(unequally_directed_lines(_57512, reverse_line(_57510)))]]], (194 ^ _51739) ^ [_58081, _58083] : [line(_58083), line(_58081), -(unequally_directed_lines(_58083, _58081)), -(unequally_directed_lines(_58083, reverse_line(_58081)))], (208 ^ _51739) ^ [_58472, _58474] : [unequally_directed_lines(_58474, _58472), unequally_directed_lines(_58474, reverse_line(_58472)), -(left_convergent_lines(_58474, _58472)), -(left_convergent_lines(_58474, reverse_line(_58472)))], (222 ^ _51739) ^ [_58875, _58877] : [left_apart_point(_58877, _58875)], (224 ^ _51739) ^ [_58920, _58922] : [left_apart_point(_58922, reverse_line(_58920))], (226 ^ _51739) ^ [_59037, _59039] : [left_convergent_lines(_59039, _59037)], (228 ^ _51739) ^ [_59082, _59084] : [left_convergent_lines(_59084, reverse_line(_59082))], (230 ^ _51739) ^ [_59195, _59197] : [-(line(line_connecting(_59197, _59195))), point(_59197), point(_59195), distinct_points(_59197, _59195)], (244 ^ _51739) ^ [_59583, _59585] : [-(point(intersection_point(_59585, _59583))), line(_59585), line(_59583), unequally_directed_lines(_59585, _59583), unequally_directed_lines(_59585, reverse_line(_59583))], (262 ^ _51739) ^ [_60064, _60066] : [-(line(parallel_through_point(_60066, _60064))), point(_60064), line(_60066)], (272 ^ _51739) ^ [_60349] : [line(_60349), -(line(reverse_line(_60349)))], (278 ^ _51739) ^ [_60553, _60555] : [distinct_points(_60555, _60553), 281 ^ _51739 : [(282 ^ _51739) ^ [] : [apart_point_and_line(_60555, line_connecting(_60555, _60553))], (284 ^ _51739) ^ [] : [apart_point_and_line(_60553, line_connecting(_60555, _60553))]]], (286 ^ _51739) ^ [_60852, _60854] : [293 ^ _51739 : [(294 ^ _51739) ^ [] : [apart_point_and_line(intersection_point(_60854, _60852), _60854)], (296 ^ _51739) ^ [] : [apart_point_and_line(intersection_point(_60854, _60852), _60852)]], unequally_directed_lines(_60854, _60852), unequally_directed_lines(_60854, reverse_line(_60852))], (298 ^ _51739) ^ [_61228, _61230] : [apart_point_and_line(_61230, parallel_through_point(_61228, _61230))], (300 ^ _51739) ^ [_61310] : [distinct_lines(_61310, reverse_line(_61310))], (302 ^ _51739) ^ [_61403, _61405] : [unequally_directed_lines(line_connecting(_61405, _61403), reverse_line(line_connecting(_61403, _61405)))], (304 ^ _51739) ^ [_61504, _61506] : [unequally_directed_lines(parallel_through_point(_61504, _61506), _61504)], (306 ^ _51739) ^ [_61644, _61646, _61648, _61650] : [distinct_points(_61650, _61648), distinct_lines(_61646, _61644), -(left_apart_point(_61650, _61646)), -(left_apart_point(_61648, _61646)), -(left_apart_point(_61650, _61644)), -(left_apart_point(_61648, _61644)), -(left_apart_point(_61650, reverse_line(_61646))), -(left_apart_point(_61648, reverse_line(_61646))), -(left_apart_point(_61650, reverse_line(_61644))), -(left_apart_point(_61648, reverse_line(_61644)))], (344 ^ _51739) ^ [_62681, _62683, _62685] : [distinct_points(_62685, _62683), left_apart_point(_62685, _62681), -(left_apart_point(_62683, _62681)), -(left_convergent_lines(line_connecting(_62685, _62683), _62681))], (358 ^ _51739) ^ [_63106, _63108, _63110] : [left_apart_point(_63110, _63106), -(distinct_points(_63110, _63108)), -(left_apart_point(_63108, _63106))], (382 ^ _51739) ^ [_63833, _63835, _63837] : [left_convergent_lines(_63837, _63835), -(unequally_directed_lines(_63835, _63833)), -(left_convergent_lines(_63837, _63833))], (368 ^ _51739) ^ [_63430, _63432, _63434] : [left_apart_point(_63434, _63432), unequally_directed_lines(_63432, _63430), -(distinct_lines(_63432, _63430)), -(left_apart_point(_63434, reverse_line(_63430)))]], input).
% 0.33/1.37 ncf('1',plain,[left_apart_point(391 ^ [], 393 ^ [])],start(222 ^ 0,bind([[_58875, _58877], [393 ^ [], 391 ^ []]]))).
% 0.33/1.37 ncf('1.1',plain,[-(left_apart_point(391 ^ [], 393 ^ []))],extension(395 ^ 1)).
% 0.33/1.37 %-----------------------------------------------------
% 0.33/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------