%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO263+3 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n009.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:23 EDT 2023
% Result : Theorem 0.38s 1.41s
% Output : Proof 0.38s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : GEO263+3 : TPTP v8.1.2. Released v4.0.0.
% 0.08/0.14 % Command : nanocop.sh %s %d
% 0.14/0.36 % Computer : n009.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Fri May 19 04:07:33 EDT 2023
% 0.14/0.36 % CPUTime :
% 0.38/1.41
% 0.38/1.41 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.38/1.41 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.38/1.41 %-----------------------------------------------------
% 0.38/1.41 ncf(matrix, plain, [(442 ^ _61168) ^ [] : [-(between_on_line(435 ^ [], 438 ^ [], 439 ^ [], 440 ^ []))], (444 ^ _61168) ^ [] : [-(convergent_lines(435 ^ [], 436 ^ []))], (446 ^ _61168) ^ [] : [-(convergent_lines(435 ^ [], 437 ^ []))], (448 ^ _61168) ^ [] : [-(convergent_lines(436 ^ [], 437 ^ []))], (450 ^ _61168) ^ [] : [between_on_line(436 ^ [], intersection_point(436 ^ [], parallel_through_point(437 ^ [], 438 ^ [])), intersection_point(436 ^ [], parallel_through_point(437 ^ [], 439 ^ [])), intersection_point(436 ^ [], parallel_through_point(437 ^ [], 440 ^ [])))], (2 ^ _61168) ^ [_61310, _61312] : [unequally_directed_opposite_lines(_61312, _61310), -(unequally_directed_lines(_61312, reverse_line(_61310)))], (8 ^ _61168) ^ [_61476, _61478] : [unequally_directed_lines(_61478, reverse_line(_61476)), -(unequally_directed_opposite_lines(_61478, _61476))], (14 ^ _61168) ^ [_61721, _61723] : [right_apart_point(_61723, _61721), -(left_apart_point(_61723, reverse_line(_61721)))], (20 ^ _61168) ^ [_61887, _61889] : [left_apart_point(_61889, reverse_line(_61887)), -(right_apart_point(_61889, _61887))], (26 ^ _61168) ^ [_62132, _62134] : [right_convergent_lines(_62134, _62132), -(left_convergent_lines(_62134, reverse_line(_62132)))], (32 ^ _61168) ^ [_62298, _62300] : [left_convergent_lines(_62300, reverse_line(_62298)), -(right_convergent_lines(_62300, _62298))], (38 ^ _61168) ^ [_62543, _62545] : [equally_directed_lines(_62545, _62543), unequally_directed_lines(_62545, _62543)], (44 ^ _61168) ^ [_62706, _62708] : [-(unequally_directed_lines(_62708, _62706)), -(equally_directed_lines(_62708, _62706))], (50 ^ _61168) ^ [_62950, _62952] : [equally_directed_opposite_lines(_62952, _62950), unequally_directed_opposite_lines(_62952, _62950)], (56 ^ _61168) ^ [_63113, _63115] : [-(unequally_directed_opposite_lines(_63115, _63113)), -(equally_directed_opposite_lines(_63115, _63113))], (72 ^ _61168) ^ [_63609, _63611] : [73 ^ _61168 : [(74 ^ _61168) ^ [] : [left_apart_point(_63611, _63609)], (76 ^ _61168) ^ [] : [right_apart_point(_63611, _63609)]], -(apart_point_and_line(_63611, _63609))], (62 ^ _61168) ^ [_63357, _63359] : [apart_point_and_line(_63359, _63357), -(left_apart_point(_63359, _63357)), -(right_apart_point(_63359, _63357))], (80 ^ _61168) ^ [_63924, _63926] : [convergent_lines(_63926, _63924), 83 ^ _61168 : [(84 ^ _61168) ^ [] : [-(unequally_directed_lines(_63926, _63924))], (86 ^ _61168) ^ [] : [-(unequally_directed_opposite_lines(_63926, _63924))]]], (88 ^ _61168) ^ [_64161, _64163] : [-(convergent_lines(_64163, _64161)), unequally_directed_lines(_64163, _64161), unequally_directed_opposite_lines(_64163, _64161)], (98 ^ _61168) ^ [_64505, _64507, _64509] : [divides_points(_64505, _64509, _64507), 103 ^ _61168 : [(104 ^ _61168) ^ [] : [-(left_apart_point(_64509, _64505))], (106 ^ _61168) ^ [] : [-(right_apart_point(_64507, _64505))]], 107 ^ _61168 : [(108 ^ _61168) ^ [] : [-(right_apart_point(_64509, _64505))], (110 ^ _61168) ^ [] : [-(left_apart_point(_64507, _64505))]]], (112 ^ _61168) ^ [_64923, _64925, _64927] : [-(divides_points(_64923, _64927, _64925)), 113 ^ _61168 : [(114 ^ _61168) ^ [] : [left_apart_point(_64927, _64923), right_apart_point(_64925, _64923)], (120 ^ _61168) ^ [] : [right_apart_point(_64927, _64923), left_apart_point(_64925, _64923)]]], (128 ^ _61168) ^ [_65448, _65450, _65452] : [before_on_line(_65452, _65450, _65448), 131 ^ _61168 : [(132 ^ _61168) ^ [] : [-(distinct_points(_65450, _65448))], (134 ^ _61168) ^ [] : [-(incident_point_and_line(_65450, _65452))], (136 ^ _61168) ^ [] : [-(incident_point_and_line(_65448, _65452))], (138 ^ _61168) ^ [] : [-(equally_directed_lines(_65452, line_connecting(_65450, _65448)))]]], (140 ^ _61168) ^ [_65853, _65855, _65857] : [-(before_on_line(_65857, _65855, _65853)), distinct_points(_65855, _65853), incident_point_and_line(_65855, _65857), incident_point_and_line(_65853, _65857), equally_directed_lines(_65857, line_connecting(_65855, _65853))], (158 ^ _61168) ^ [_66415, _66417, _66419, _66421] : [between_on_line(_66421, _66419, _66417, _66415), 163 ^ _61168 : [(164 ^ _61168) ^ [] : [-(before_on_line(_66421, _66419, _66417))], (166 ^ _61168) ^ [] : [-(before_on_line(_66421, _66417, _66415))]], 167 ^ _61168 : [(168 ^ _61168) ^ [] : [-(before_on_line(_66421, _66415, _66417))], (170 ^ _61168) ^ [] : [-(before_on_line(_66421, _66417, _66419))]]], (172 ^ _61168) ^ [_66857, _66859, _66861, _66863] : [-(between_on_line(_66863, _66861, _66859, _66857)), 173 ^ _61168 : [(174 ^ _61168) ^ [] : [before_on_line(_66863, _66861, _66859), before_on_line(_66863, _66859, _66857)], (180 ^ _61168) ^ [] : [before_on_line(_66863, _66857, _66859), before_on_line(_66863, _66859, _66861)]]], (188 ^ _61168) ^ [_67335] : [distinct_points(_67335, _67335)], (190 ^ _61168) ^ [_67456, _67458, _67460] : [distinct_points(_67460, _67458), -(distinct_points(_67460, _67456)), -(distinct_points(_67458, _67456))], (200 ^ _61168) ^ [_67736] : [distinct_lines(_67736, _67736)], (202 ^ _61168) ^ [_67857, _67859, _67861] : [distinct_lines(_67861, _67859), -(distinct_lines(_67861, _67857)), -(distinct_lines(_67859, _67857))], (212 ^ _61168) ^ [_68138] : [-(equally_directed_lines(_68138, _68138))], (214 ^ _61168) ^ [_68259, _68261, _68263] : [unequally_directed_lines(_68263, _68261), -(unequally_directed_lines(_68263, _68259)), -(unequally_directed_lines(_68261, _68259))], (224 ^ _61168) ^ [_68583, _68585, _68587] : [unequally_directed_lines(_68587, _68585), unequally_directed_lines(_68587, reverse_line(_68585)), 233 ^ _61168 : [(234 ^ _61168) ^ [] : [-(unequally_directed_lines(_68587, _68583))], (236 ^ _61168) ^ [] : [-(unequally_directed_lines(_68587, reverse_line(_68583)))]], 237 ^ _61168 : [(238 ^ _61168) ^ [] : [-(unequally_directed_lines(_68585, _68583))], (240 ^ _61168) ^ [] : [-(unequally_directed_lines(_68585, reverse_line(_68583)))]]], (242 ^ _61168) ^ [_69154, _69156] : [-(unequally_directed_lines(_69156, _69154)), -(unequally_directed_lines(_69156, reverse_line(_69154)))], (248 ^ _61168) ^ [_69369, _69371] : [unequally_directed_lines(_69371, _69369), unequally_directed_lines(_69371, reverse_line(_69369)), -(left_convergent_lines(_69371, _69369)), -(left_convergent_lines(_69371, reverse_line(_69369)))], (262 ^ _61168) ^ [_69772, _69774] : [left_apart_point(_69774, _69772)], (264 ^ _61168) ^ [_69817, _69819] : [left_apart_point(_69819, reverse_line(_69817))], (266 ^ _61168) ^ [_69934, _69936] : [left_convergent_lines(_69936, _69934)], (268 ^ _61168) ^ [_69979, _69981] : [left_convergent_lines(_69981, reverse_line(_69979))], (270 ^ _61168) ^ [_70092, _70094] : [-(line(line_connecting(_70094, _70092))), point(_70094), point(_70092), distinct_points(_70094, _70092)], (284 ^ _61168) ^ [_70480, _70482] : [-(point(intersection_point(_70482, _70480))), line(_70482), line(_70480), unequally_directed_lines(_70482, _70480), unequally_directed_lines(_70482, reverse_line(_70480))], (302 ^ _61168) ^ [_70961, _70963] : [-(line(parallel_through_point(_70963, _70961))), point(_70961), line(_70963)], (312 ^ _61168) ^ [_71246] : [line(_71246), -(line(reverse_line(_71246)))], (318 ^ _61168) ^ [_71450, _71452] : [distinct_points(_71452, _71450), 321 ^ _61168 : [(322 ^ _61168) ^ [] : [apart_point_and_line(_71452, line_connecting(_71452, _71450))], (324 ^ _61168) ^ [] : [apart_point_and_line(_71450, line_connecting(_71452, _71450))]]], (326 ^ _61168) ^ [_71749, _71751] : [333 ^ _61168 : [(334 ^ _61168) ^ [] : [apart_point_and_line(intersection_point(_71751, _71749), _71751)], (336 ^ _61168) ^ [] : [apart_point_and_line(intersection_point(_71751, _71749), _71749)]], unequally_directed_lines(_71751, _71749), unequally_directed_lines(_71751, reverse_line(_71749))], (338 ^ _61168) ^ [_72125, _72127] : [apart_point_and_line(_72127, parallel_through_point(_72125, _72127))], (340 ^ _61168) ^ [_72207] : [distinct_lines(_72207, reverse_line(_72207))], (342 ^ _61168) ^ [_72316, _72318] : [distinct_points(_72318, _72316), -(equally_directed_lines(line_connecting(_72318, _72316), reverse_line(line_connecting(_72316, _72318))))], (348 ^ _61168) ^ [_72527, _72529] : [-(equally_directed_lines(parallel_through_point(_72527, _72529), _72527))], (350 ^ _61168) ^ [_72667, _72669, _72671, _72673] : [distinct_points(_72673, _72671), distinct_lines(_72669, _72667), -(left_apart_point(_72673, _72669)), -(left_apart_point(_72671, _72669)), -(left_apart_point(_72673, _72667)), -(left_apart_point(_72671, _72667)), -(left_apart_point(_72673, reverse_line(_72669))), -(left_apart_point(_72671, reverse_line(_72669))), -(left_apart_point(_72673, reverse_line(_72667))), -(left_apart_point(_72671, reverse_line(_72667)))], (388 ^ _61168) ^ [_73704, _73706, _73708] : [distinct_points(_73708, _73706), left_apart_point(_73708, _73704), -(left_apart_point(_73706, _73704)), -(left_convergent_lines(line_connecting(_73708, _73706), _73704))], (402 ^ _61168) ^ [_74129, _74131, _74133] : [left_apart_point(_74133, _74129), -(distinct_points(_74133, _74131)), -(left_apart_point(_74131, _74129))], (426 ^ _61168) ^ [_74856, _74858, _74860] : [left_convergent_lines(_74860, _74858), -(unequally_directed_lines(_74858, _74856)), -(left_convergent_lines(_74860, _74856))], (412 ^ _61168) ^ [_74453, _74455, _74457] : [left_apart_point(_74457, _74455), unequally_directed_lines(_74455, _74453), -(distinct_lines(_74455, _74453)), -(left_apart_point(_74457, reverse_line(_74453)))]], input).
% 0.38/1.41 ncf('1',plain,[equally_directed_lines(reverse_line(436 ^ []), reverse_line(436 ^ [])), unequally_directed_lines(reverse_line(436 ^ []), reverse_line(436 ^ []))],start(38 ^ 0,bind([[_62543, _62545], [reverse_line(436 ^ []), reverse_line(436 ^ [])]]))).
% 0.38/1.41 ncf('1.1',plain,[-(equally_directed_lines(reverse_line(436 ^ []), reverse_line(436 ^ []))), -(unequally_directed_lines(reverse_line(436 ^ []), reverse_line(436 ^ [])))],extension(44 ^ 1,bind([[_62706, _62708], [reverse_line(436 ^ []), reverse_line(436 ^ [])]]))).
% 0.38/1.41 ncf('1.1.1',plain,[unequally_directed_lines(reverse_line(436 ^ []), reverse_line(436 ^ [])), unequally_directed_lines(reverse_line(436 ^ []), reverse_line(reverse_line(436 ^ []))), -(left_convergent_lines(reverse_line(436 ^ []), reverse_line(436 ^ []))), -(left_convergent_lines(reverse_line(436 ^ []), reverse_line(reverse_line(436 ^ []))))],extension(248 ^ 2,bind([[_69369, _69371], [reverse_line(436 ^ []), reverse_line(436 ^ [])]]))).
% 0.38/1.41 ncf('1.1.1.1',plain,[-(unequally_directed_lines(reverse_line(436 ^ []), reverse_line(reverse_line(436 ^ [])))), unequally_directed_lines(reverse_line(436 ^ []), reverse_line(436 ^ [])), -(unequally_directed_lines(reverse_line(436 ^ []), reverse_line(reverse_line(436 ^ []))))],extension(214 ^ 3,bind([[_68259, _68261, _68263], [reverse_line(reverse_line(436 ^ [])), reverse_line(436 ^ []), reverse_line(436 ^ [])]]))).
% 0.38/1.41 ncf('1.1.1.1.1',plain,[-(unequally_directed_lines(reverse_line(436 ^ []), reverse_line(436 ^ [])))],reduction('1.1')).
% 0.38/1.41 ncf('1.1.1.1.2',plain,[unequally_directed_lines(reverse_line(436 ^ []), reverse_line(reverse_line(436 ^ [])))],reduction('1.1.1')).
% 0.38/1.41 ncf('1.1.1.2',plain,[left_convergent_lines(reverse_line(436 ^ []), reverse_line(436 ^ []))],extension(266 ^ 3,bind([[_69934, _69936], [reverse_line(436 ^ []), reverse_line(436 ^ [])]]))).
% 0.38/1.41 ncf('1.1.1.3',plain,[left_convergent_lines(reverse_line(436 ^ []), reverse_line(reverse_line(436 ^ [])))],extension(266 ^ 3,bind([[_69934, _69936], [reverse_line(reverse_line(436 ^ [])), reverse_line(436 ^ [])]]))).
% 0.38/1.41 ncf('1.2',plain,[-(unequally_directed_lines(reverse_line(436 ^ []), reverse_line(436 ^ []))), unequally_directed_lines(435 ^ [], reverse_line(436 ^ [])), -(unequally_directed_lines(435 ^ [], reverse_line(436 ^ [])))],extension(214 ^ 1,bind([[_68259, _68261, _68263], [reverse_line(436 ^ []), reverse_line(436 ^ []), 435 ^ []]]))).
% 0.38/1.41 ncf('1.2.1',plain,[-(unequally_directed_lines(435 ^ [], reverse_line(436 ^ []))), unequally_directed_opposite_lines(435 ^ [], 436 ^ [])],extension(2 ^ 2,bind([[_61310, _61312], [436 ^ [], 435 ^ []]]))).
% 0.38/1.41 ncf('1.2.1.1',plain,[-(unequally_directed_opposite_lines(435 ^ [], 436 ^ [])), convergent_lines(435 ^ [], 436 ^ [])],extension(80 ^ 3,bind([[_63924, _63926], [436 ^ [], 435 ^ []]]))).
% 0.38/1.41 ncf('1.2.1.1.1',plain,[-(convergent_lines(435 ^ [], 436 ^ []))],extension(444 ^ 4)).
% 0.38/1.41 ncf('1.2.2',plain,[unequally_directed_lines(435 ^ [], reverse_line(436 ^ [])), unequally_directed_lines(435 ^ [], 436 ^ []), -(left_convergent_lines(435 ^ [], 436 ^ [])), -(left_convergent_lines(435 ^ [], reverse_line(436 ^ [])))],extension(248 ^ 2,bind([[_69369, _69371], [436 ^ [], 435 ^ []]]))).
% 0.38/1.41 ncf('1.2.2.1',plain,[-(unequally_directed_lines(435 ^ [], 436 ^ [])), convergent_lines(435 ^ [], 436 ^ [])],extension(80 ^ 3,bind([[_63924, _63926], [436 ^ [], 435 ^ []]]))).
% 0.38/1.41 ncf('1.2.2.1.1',plain,[-(convergent_lines(435 ^ [], 436 ^ []))],extension(444 ^ 4)).
% 0.38/1.41 ncf('1.2.2.2',plain,[left_convergent_lines(435 ^ [], 436 ^ [])],extension(266 ^ 3,bind([[_69934, _69936], [436 ^ [], 435 ^ []]]))).
% 0.38/1.41 ncf('1.2.2.3',plain,[left_convergent_lines(435 ^ [], reverse_line(436 ^ []))],extension(266 ^ 3,bind([[_69934, _69936], [reverse_line(436 ^ []), 435 ^ []]]))).
% 0.38/1.41 %-----------------------------------------------------
% 0.38/1.41 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------