%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO237+1 : TPTP v8.1.2. Bugfixed v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n014.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.37s 1.42s
% Output : Proof 0.37s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.14 % Problem : GEO237+1 : TPTP v8.1.2. Bugfixed v6.4.0.
% 0.07/0.14 % Command : nanocop.sh %s %d
% 0.15/0.36 % Computer : n014.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 300
% 0.15/0.36 % DateTime : Fri May 19 04:33:27 EDT 2023
% 0.15/0.36 % CPUTime :
% 0.37/1.42
% 0.37/1.42 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.37/1.42 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.37/1.42 %-----------------------------------------------------
% 0.37/1.42 ncf(matrix, plain, [(396 ^ _52756) ^ [] : [-(apart_point_and_line(393 ^ [], 394 ^ []))], (398 ^ _52756) ^ [] : [-(divides_points(394 ^ [], 391 ^ [], 392 ^ []))], (400 ^ _52756) ^ [] : [divides_points(394 ^ [], 391 ^ [], 393 ^ [])], (402 ^ _52756) ^ [] : [divides_points(394 ^ [], 392 ^ [], 393 ^ [])], (12 ^ _52756) ^ [_53154, _53156] : [13 ^ _52756 : [(14 ^ _52756) ^ [] : [left_apart_point(_53156, _53154)], (16 ^ _52756) ^ [] : [left_apart_point(_53156, reverse_line(_53154))]], -(apart_point_and_line(_53156, _53154))], (2 ^ _52756) ^ [_52898, _52900] : [apart_point_and_line(_52900, _52898), -(left_apart_point(_52900, _52898)), -(left_apart_point(_52900, reverse_line(_52898)))], (20 ^ _52756) ^ [_53473, _53475] : [convergent_lines(_53475, _53473), 23 ^ _52756 : [(24 ^ _52756) ^ [] : [-(unequally_directed_lines(_53475, _53473))], (26 ^ _52756) ^ [] : [-(unequally_directed_lines(_53475, reverse_line(_53473)))]]], (28 ^ _52756) ^ [_53714, _53716] : [-(convergent_lines(_53716, _53714)), unequally_directed_lines(_53716, _53714), unequally_directed_lines(_53716, reverse_line(_53714))], (38 ^ _52756) ^ [_54062, _54064, _54066] : [divides_points(_54062, _54066, _54064), 43 ^ _52756 : [(44 ^ _52756) ^ [] : [-(left_apart_point(_54066, _54062))], (46 ^ _52756) ^ [] : [-(left_apart_point(_54064, reverse_line(_54062)))]], 47 ^ _52756 : [(48 ^ _52756) ^ [] : [-(left_apart_point(_54066, reverse_line(_54062)))], (50 ^ _52756) ^ [] : [-(left_apart_point(_54064, _54062))]]], (52 ^ _52756) ^ [_54488, _54490, _54492] : [-(divides_points(_54488, _54492, _54490)), 53 ^ _52756 : [(54 ^ _52756) ^ [] : [left_apart_point(_54492, _54488), left_apart_point(_54490, reverse_line(_54488))], (60 ^ _52756) ^ [] : [left_apart_point(_54492, reverse_line(_54488)), left_apart_point(_54490, _54488)]]], (68 ^ _52756) ^ [_55021, _55023, _55025] : [before_on_line(_55025, _55023, _55021), 71 ^ _52756 : [(72 ^ _52756) ^ [] : [-(distinct_points(_55023, _55021))], (74 ^ _52756) ^ [] : [left_apart_point(_55023, _55025)], (76 ^ _52756) ^ [] : [left_apart_point(_55023, reverse_line(_55025))], (78 ^ _52756) ^ [] : [left_apart_point(_55021, _55025)], (80 ^ _52756) ^ [] : [left_apart_point(_55021, reverse_line(_55025))], (82 ^ _52756) ^ [] : [unequally_directed_lines(_55025, line_connecting(_55023, _55021))]]], (84 ^ _52756) ^ [_55591, _55593, _55595] : [-(before_on_line(_55595, _55593, _55591)), distinct_points(_55593, _55591), -(left_apart_point(_55593, _55595)), -(left_apart_point(_55593, reverse_line(_55595))), -(unequally_directed_lines(_55595, line_connecting(_55593, _55591))), -(left_apart_point(_55591, _55595)), -(left_apart_point(_55591, reverse_line(_55595)))], (110 ^ _52756) ^ [_56360, _56362, _56364, _56366] : [between_on_line(_56366, _56364, _56362, _56360), 115 ^ _52756 : [(116 ^ _52756) ^ [] : [-(before_on_line(_56366, _56364, _56362))], (118 ^ _52756) ^ [] : [-(before_on_line(_56366, _56362, _56360))]], 119 ^ _52756 : [(120 ^ _52756) ^ [] : [-(before_on_line(_56366, _56360, _56362))], (122 ^ _52756) ^ [] : [-(before_on_line(_56366, _56362, _56364))]]], (124 ^ _52756) ^ [_56802, _56804, _56806, _56808] : [-(between_on_line(_56808, _56806, _56804, _56802)), 125 ^ _52756 : [(126 ^ _52756) ^ [] : [before_on_line(_56808, _56806, _56804), before_on_line(_56808, _56804, _56802)], (132 ^ _52756) ^ [] : [before_on_line(_56808, _56802, _56804), before_on_line(_56808, _56804, _56806)]]], (140 ^ _52756) ^ [_57280] : [distinct_points(_57280, _57280)], (142 ^ _52756) ^ [_57401, _57403, _57405] : [distinct_points(_57405, _57403), -(distinct_points(_57405, _57401)), -(distinct_points(_57403, _57401))], (152 ^ _52756) ^ [_57681] : [distinct_lines(_57681, _57681)], (154 ^ _52756) ^ [_57802, _57804, _57806] : [distinct_lines(_57806, _57804), -(distinct_lines(_57806, _57802)), -(distinct_lines(_57804, _57802))], (164 ^ _52756) ^ [_58082] : [unequally_directed_lines(_58082, _58082)], (166 ^ _52756) ^ [_58203, _58205, _58207] : [unequally_directed_lines(_58207, _58205), -(unequally_directed_lines(_58207, _58203)), -(unequally_directed_lines(_58205, _58203))], (176 ^ _52756) ^ [_58527, _58529, _58531] : [unequally_directed_lines(_58531, _58529), unequally_directed_lines(_58531, reverse_line(_58529)), 185 ^ _52756 : [(186 ^ _52756) ^ [] : [-(unequally_directed_lines(_58531, _58527))], (188 ^ _52756) ^ [] : [-(unequally_directed_lines(_58531, reverse_line(_58527)))]], 189 ^ _52756 : [(190 ^ _52756) ^ [] : [-(unequally_directed_lines(_58529, _58527))], (192 ^ _52756) ^ [] : [-(unequally_directed_lines(_58529, reverse_line(_58527)))]]], (194 ^ _52756) ^ [_59098, _59100] : [line(_59100), line(_59098), -(unequally_directed_lines(_59100, _59098)), -(unequally_directed_lines(_59100, reverse_line(_59098)))], (208 ^ _52756) ^ [_59489, _59491] : [unequally_directed_lines(_59491, _59489), unequally_directed_lines(_59491, reverse_line(_59489)), -(left_convergent_lines(_59491, _59489)), -(left_convergent_lines(_59491, reverse_line(_59489)))], (222 ^ _52756) ^ [_59892, _59894] : [left_apart_point(_59894, _59892)], (224 ^ _52756) ^ [_59937, _59939] : [left_apart_point(_59939, reverse_line(_59937))], (226 ^ _52756) ^ [_60054, _60056] : [left_convergent_lines(_60056, _60054)], (228 ^ _52756) ^ [_60099, _60101] : [left_convergent_lines(_60101, reverse_line(_60099))], (230 ^ _52756) ^ [_60212, _60214] : [-(line(line_connecting(_60214, _60212))), point(_60214), point(_60212), distinct_points(_60214, _60212)], (244 ^ _52756) ^ [_60600, _60602] : [-(point(intersection_point(_60602, _60600))), line(_60602), line(_60600), unequally_directed_lines(_60602, _60600), unequally_directed_lines(_60602, reverse_line(_60600))], (262 ^ _52756) ^ [_61081, _61083] : [-(line(parallel_through_point(_61083, _61081))), point(_61081), line(_61083)], (272 ^ _52756) ^ [_61366] : [line(_61366), -(line(reverse_line(_61366)))], (278 ^ _52756) ^ [_61570, _61572] : [distinct_points(_61572, _61570), 281 ^ _52756 : [(282 ^ _52756) ^ [] : [apart_point_and_line(_61572, line_connecting(_61572, _61570))], (284 ^ _52756) ^ [] : [apart_point_and_line(_61570, line_connecting(_61572, _61570))]]], (286 ^ _52756) ^ [_61869, _61871] : [293 ^ _52756 : [(294 ^ _52756) ^ [] : [apart_point_and_line(intersection_point(_61871, _61869), _61871)], (296 ^ _52756) ^ [] : [apart_point_and_line(intersection_point(_61871, _61869), _61869)]], unequally_directed_lines(_61871, _61869), unequally_directed_lines(_61871, reverse_line(_61869))], (298 ^ _52756) ^ [_62245, _62247] : [apart_point_and_line(_62247, parallel_through_point(_62245, _62247))], (300 ^ _52756) ^ [_62327] : [distinct_lines(_62327, reverse_line(_62327))], (302 ^ _52756) ^ [_62420, _62422] : [unequally_directed_lines(line_connecting(_62422, _62420), reverse_line(line_connecting(_62420, _62422)))], (304 ^ _52756) ^ [_62521, _62523] : [unequally_directed_lines(parallel_through_point(_62521, _62523), _62521)], (306 ^ _52756) ^ [_62661, _62663, _62665, _62667] : [distinct_points(_62667, _62665), distinct_lines(_62663, _62661), -(left_apart_point(_62667, _62663)), -(left_apart_point(_62665, _62663)), -(left_apart_point(_62667, _62661)), -(left_apart_point(_62665, _62661)), -(left_apart_point(_62667, reverse_line(_62663))), -(left_apart_point(_62665, reverse_line(_62663))), -(left_apart_point(_62667, reverse_line(_62661))), -(left_apart_point(_62665, reverse_line(_62661)))], (344 ^ _52756) ^ [_63698, _63700, _63702] : [distinct_points(_63702, _63700), left_apart_point(_63702, _63698), -(left_apart_point(_63700, _63698)), -(left_convergent_lines(line_connecting(_63702, _63700), _63698))], (358 ^ _52756) ^ [_64123, _64125, _64127] : [left_apart_point(_64127, _64123), -(distinct_points(_64127, _64125)), -(left_apart_point(_64125, _64123))], (382 ^ _52756) ^ [_64850, _64852, _64854] : [left_convergent_lines(_64854, _64852), -(unequally_directed_lines(_64852, _64850)), -(left_convergent_lines(_64854, _64850))], (368 ^ _52756) ^ [_64447, _64449, _64451] : [left_apart_point(_64451, _64449), unequally_directed_lines(_64449, _64447), -(distinct_lines(_64449, _64447)), -(left_apart_point(_64451, reverse_line(_64447)))]], input).
% 0.37/1.42 ncf('1',plain,[left_apart_point(393 ^ [], 394 ^ [])],start(222 ^ 0,bind([[_59892, _59894], [394 ^ [], 393 ^ []]]))).
% 0.37/1.42 ncf('1.1',plain,[-(left_apart_point(393 ^ [], 394 ^ [])), apart_point_and_line(393 ^ [], 394 ^ []), -(left_apart_point(393 ^ [], reverse_line(394 ^ [])))],extension(2 ^ 1,bind([[_52898, _52900], [394 ^ [], 393 ^ []]]))).
% 0.37/1.42 ncf('1.1.1',plain,[-(apart_point_and_line(393 ^ [], 394 ^ []))],extension(396 ^ 2)).
% 0.37/1.42 ncf('1.1.2',plain,[left_apart_point(393 ^ [], reverse_line(394 ^ []))],extension(222 ^ 2,bind([[_59892, _59894], [reverse_line(394 ^ []), 393 ^ []]]))).
% 0.37/1.42 %-----------------------------------------------------
% 0.37/1.42 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------