%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO261+3 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n011.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.36s 1.37s
% Output : Proof 0.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO261+3 : TPTP v8.1.2. Released v4.0.0.
% 0.07/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n011.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:39:03 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.36/1.37
% 0.36/1.37 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.36/1.37 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.36/1.37 %-----------------------------------------------------
% 0.36/1.37 ncf(matrix, plain, [(441 ^ _59524) ^ [] : [-(between_on_line(435 ^ [], 437 ^ [], 438 ^ [], 439 ^ []))], (443 ^ _59524) ^ [] : [-(convergent_lines(435 ^ [], 436 ^ []))], (445 ^ _59524) ^ [] : [-(incident_point_and_line(438 ^ [], 436 ^ []))], (447 ^ _59524) ^ [] : [divides_points(436 ^ [], 437 ^ [], 439 ^ [])], (2 ^ _59524) ^ [_59666, _59668] : [unequally_directed_opposite_lines(_59668, _59666), -(unequally_directed_lines(_59668, reverse_line(_59666)))], (8 ^ _59524) ^ [_59832, _59834] : [unequally_directed_lines(_59834, reverse_line(_59832)), -(unequally_directed_opposite_lines(_59834, _59832))], (14 ^ _59524) ^ [_60077, _60079] : [right_apart_point(_60079, _60077), -(left_apart_point(_60079, reverse_line(_60077)))], (20 ^ _59524) ^ [_60243, _60245] : [left_apart_point(_60245, reverse_line(_60243)), -(right_apart_point(_60245, _60243))], (26 ^ _59524) ^ [_60488, _60490] : [right_convergent_lines(_60490, _60488), -(left_convergent_lines(_60490, reverse_line(_60488)))], (32 ^ _59524) ^ [_60654, _60656] : [left_convergent_lines(_60656, reverse_line(_60654)), -(right_convergent_lines(_60656, _60654))], (38 ^ _59524) ^ [_60899, _60901] : [equally_directed_lines(_60901, _60899), unequally_directed_lines(_60901, _60899)], (44 ^ _59524) ^ [_61062, _61064] : [-(unequally_directed_lines(_61064, _61062)), -(equally_directed_lines(_61064, _61062))], (50 ^ _59524) ^ [_61306, _61308] : [equally_directed_opposite_lines(_61308, _61306), unequally_directed_opposite_lines(_61308, _61306)], (56 ^ _59524) ^ [_61469, _61471] : [-(unequally_directed_opposite_lines(_61471, _61469)), -(equally_directed_opposite_lines(_61471, _61469))], (72 ^ _59524) ^ [_61965, _61967] : [73 ^ _59524 : [(74 ^ _59524) ^ [] : [left_apart_point(_61967, _61965)], (76 ^ _59524) ^ [] : [right_apart_point(_61967, _61965)]], -(apart_point_and_line(_61967, _61965))], (62 ^ _59524) ^ [_61713, _61715] : [apart_point_and_line(_61715, _61713), -(left_apart_point(_61715, _61713)), -(right_apart_point(_61715, _61713))], (80 ^ _59524) ^ [_62280, _62282] : [convergent_lines(_62282, _62280), 83 ^ _59524 : [(84 ^ _59524) ^ [] : [-(unequally_directed_lines(_62282, _62280))], (86 ^ _59524) ^ [] : [-(unequally_directed_opposite_lines(_62282, _62280))]]], (88 ^ _59524) ^ [_62517, _62519] : [-(convergent_lines(_62519, _62517)), unequally_directed_lines(_62519, _62517), unequally_directed_opposite_lines(_62519, _62517)], (98 ^ _59524) ^ [_62861, _62863, _62865] : [divides_points(_62861, _62865, _62863), 103 ^ _59524 : [(104 ^ _59524) ^ [] : [-(left_apart_point(_62865, _62861))], (106 ^ _59524) ^ [] : [-(right_apart_point(_62863, _62861))]], 107 ^ _59524 : [(108 ^ _59524) ^ [] : [-(right_apart_point(_62865, _62861))], (110 ^ _59524) ^ [] : [-(left_apart_point(_62863, _62861))]]], (112 ^ _59524) ^ [_63279, _63281, _63283] : [-(divides_points(_63279, _63283, _63281)), 113 ^ _59524 : [(114 ^ _59524) ^ [] : [left_apart_point(_63283, _63279), right_apart_point(_63281, _63279)], (120 ^ _59524) ^ [] : [right_apart_point(_63283, _63279), left_apart_point(_63281, _63279)]]], (128 ^ _59524) ^ [_63804, _63806, _63808] : [before_on_line(_63808, _63806, _63804), 131 ^ _59524 : [(132 ^ _59524) ^ [] : [-(distinct_points(_63806, _63804))], (134 ^ _59524) ^ [] : [-(incident_point_and_line(_63806, _63808))], (136 ^ _59524) ^ [] : [-(incident_point_and_line(_63804, _63808))], (138 ^ _59524) ^ [] : [-(equally_directed_lines(_63808, line_connecting(_63806, _63804)))]]], (140 ^ _59524) ^ [_64209, _64211, _64213] : [-(before_on_line(_64213, _64211, _64209)), distinct_points(_64211, _64209), incident_point_and_line(_64211, _64213), incident_point_and_line(_64209, _64213), equally_directed_lines(_64213, line_connecting(_64211, _64209))], (158 ^ _59524) ^ [_64771, _64773, _64775, _64777] : [between_on_line(_64777, _64775, _64773, _64771), 163 ^ _59524 : [(164 ^ _59524) ^ [] : [-(before_on_line(_64777, _64775, _64773))], (166 ^ _59524) ^ [] : [-(before_on_line(_64777, _64773, _64771))]], 167 ^ _59524 : [(168 ^ _59524) ^ [] : [-(before_on_line(_64777, _64771, _64773))], (170 ^ _59524) ^ [] : [-(before_on_line(_64777, _64773, _64775))]]], (172 ^ _59524) ^ [_65213, _65215, _65217, _65219] : [-(between_on_line(_65219, _65217, _65215, _65213)), 173 ^ _59524 : [(174 ^ _59524) ^ [] : [before_on_line(_65219, _65217, _65215), before_on_line(_65219, _65215, _65213)], (180 ^ _59524) ^ [] : [before_on_line(_65219, _65213, _65215), before_on_line(_65219, _65215, _65217)]]], (188 ^ _59524) ^ [_65691] : [distinct_points(_65691, _65691)], (190 ^ _59524) ^ [_65812, _65814, _65816] : [distinct_points(_65816, _65814), -(distinct_points(_65816, _65812)), -(distinct_points(_65814, _65812))], (200 ^ _59524) ^ [_66092] : [distinct_lines(_66092, _66092)], (202 ^ _59524) ^ [_66213, _66215, _66217] : [distinct_lines(_66217, _66215), -(distinct_lines(_66217, _66213)), -(distinct_lines(_66215, _66213))], (212 ^ _59524) ^ [_66494] : [-(equally_directed_lines(_66494, _66494))], (214 ^ _59524) ^ [_66615, _66617, _66619] : [unequally_directed_lines(_66619, _66617), -(unequally_directed_lines(_66619, _66615)), -(unequally_directed_lines(_66617, _66615))], (224 ^ _59524) ^ [_66939, _66941, _66943] : [unequally_directed_lines(_66943, _66941), unequally_directed_lines(_66943, reverse_line(_66941)), 233 ^ _59524 : [(234 ^ _59524) ^ [] : [-(unequally_directed_lines(_66943, _66939))], (236 ^ _59524) ^ [] : [-(unequally_directed_lines(_66943, reverse_line(_66939)))]], 237 ^ _59524 : [(238 ^ _59524) ^ [] : [-(unequally_directed_lines(_66941, _66939))], (240 ^ _59524) ^ [] : [-(unequally_directed_lines(_66941, reverse_line(_66939)))]]], (242 ^ _59524) ^ [_67510, _67512] : [-(unequally_directed_lines(_67512, _67510)), -(unequally_directed_lines(_67512, reverse_line(_67510)))], (248 ^ _59524) ^ [_67725, _67727] : [unequally_directed_lines(_67727, _67725), unequally_directed_lines(_67727, reverse_line(_67725)), -(left_convergent_lines(_67727, _67725)), -(left_convergent_lines(_67727, reverse_line(_67725)))], (262 ^ _59524) ^ [_68128, _68130] : [left_apart_point(_68130, _68128)], (264 ^ _59524) ^ [_68173, _68175] : [left_apart_point(_68175, reverse_line(_68173))], (266 ^ _59524) ^ [_68290, _68292] : [left_convergent_lines(_68292, _68290)], (268 ^ _59524) ^ [_68335, _68337] : [left_convergent_lines(_68337, reverse_line(_68335))], (270 ^ _59524) ^ [_68448, _68450] : [-(line(line_connecting(_68450, _68448))), point(_68450), point(_68448), distinct_points(_68450, _68448)], (284 ^ _59524) ^ [_68836, _68838] : [-(point(intersection_point(_68838, _68836))), line(_68838), line(_68836), unequally_directed_lines(_68838, _68836), unequally_directed_lines(_68838, reverse_line(_68836))], (302 ^ _59524) ^ [_69317, _69319] : [-(line(parallel_through_point(_69319, _69317))), point(_69317), line(_69319)], (312 ^ _59524) ^ [_69602] : [line(_69602), -(line(reverse_line(_69602)))], (318 ^ _59524) ^ [_69806, _69808] : [distinct_points(_69808, _69806), 321 ^ _59524 : [(322 ^ _59524) ^ [] : [apart_point_and_line(_69808, line_connecting(_69808, _69806))], (324 ^ _59524) ^ [] : [apart_point_and_line(_69806, line_connecting(_69808, _69806))]]], (326 ^ _59524) ^ [_70105, _70107] : [333 ^ _59524 : [(334 ^ _59524) ^ [] : [apart_point_and_line(intersection_point(_70107, _70105), _70107)], (336 ^ _59524) ^ [] : [apart_point_and_line(intersection_point(_70107, _70105), _70105)]], unequally_directed_lines(_70107, _70105), unequally_directed_lines(_70107, reverse_line(_70105))], (338 ^ _59524) ^ [_70481, _70483] : [apart_point_and_line(_70483, parallel_through_point(_70481, _70483))], (340 ^ _59524) ^ [_70563] : [distinct_lines(_70563, reverse_line(_70563))], (342 ^ _59524) ^ [_70672, _70674] : [distinct_points(_70674, _70672), -(equally_directed_lines(line_connecting(_70674, _70672), reverse_line(line_connecting(_70672, _70674))))], (348 ^ _59524) ^ [_70883, _70885] : [-(equally_directed_lines(parallel_through_point(_70883, _70885), _70883))], (350 ^ _59524) ^ [_71023, _71025, _71027, _71029] : [distinct_points(_71029, _71027), distinct_lines(_71025, _71023), -(left_apart_point(_71029, _71025)), -(left_apart_point(_71027, _71025)), -(left_apart_point(_71029, _71023)), -(left_apart_point(_71027, _71023)), -(left_apart_point(_71029, reverse_line(_71025))), -(left_apart_point(_71027, reverse_line(_71025))), -(left_apart_point(_71029, reverse_line(_71023))), -(left_apart_point(_71027, reverse_line(_71023)))], (388 ^ _59524) ^ [_72060, _72062, _72064] : [distinct_points(_72064, _72062), left_apart_point(_72064, _72060), -(left_apart_point(_72062, _72060)), -(left_convergent_lines(line_connecting(_72064, _72062), _72060))], (402 ^ _59524) ^ [_72485, _72487, _72489] : [left_apart_point(_72489, _72485), -(distinct_points(_72489, _72487)), -(left_apart_point(_72487, _72485))], (426 ^ _59524) ^ [_73212, _73214, _73216] : [left_convergent_lines(_73216, _73214), -(unequally_directed_lines(_73214, _73212)), -(left_convergent_lines(_73216, _73212))], (412 ^ _59524) ^ [_72809, _72811, _72813] : [left_apart_point(_72813, _72811), unequally_directed_lines(_72811, _72809), -(distinct_lines(_72811, _72809)), -(left_apart_point(_72813, reverse_line(_72809)))]], input).
% 0.36/1.37 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([[_60899, _60901], [reverse_line(436 ^ []), reverse_line(436 ^ [])]]))).
% 0.36/1.37 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([[_61062, _61064], [reverse_line(436 ^ []), reverse_line(436 ^ [])]]))).
% 0.36/1.37 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([[_67725, _67727], [reverse_line(436 ^ []), reverse_line(436 ^ [])]]))).
% 0.36/1.37 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([[_66615, _66617, _66619], [reverse_line(reverse_line(436 ^ [])), reverse_line(436 ^ []), reverse_line(436 ^ [])]]))).
% 0.36/1.37 ncf('1.1.1.1.1',plain,[-(unequally_directed_lines(reverse_line(436 ^ []), reverse_line(436 ^ [])))],reduction('1.1')).
% 0.36/1.37 ncf('1.1.1.1.2',plain,[unequally_directed_lines(reverse_line(436 ^ []), reverse_line(reverse_line(436 ^ [])))],reduction('1.1.1')).
% 0.36/1.37 ncf('1.1.1.2',plain,[left_convergent_lines(reverse_line(436 ^ []), reverse_line(436 ^ []))],extension(266 ^ 3,bind([[_68290, _68292], [reverse_line(436 ^ []), reverse_line(436 ^ [])]]))).
% 0.36/1.37 ncf('1.1.1.3',plain,[left_convergent_lines(reverse_line(436 ^ []), reverse_line(reverse_line(436 ^ [])))],extension(266 ^ 3,bind([[_68290, _68292], [reverse_line(reverse_line(436 ^ [])), reverse_line(436 ^ [])]]))).
% 0.36/1.37 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([[_66615, _66617, _66619], [reverse_line(436 ^ []), reverse_line(436 ^ []), 435 ^ []]]))).
% 0.36/1.37 ncf('1.2.1',plain,[-(unequally_directed_lines(435 ^ [], reverse_line(436 ^ []))), unequally_directed_opposite_lines(435 ^ [], 436 ^ [])],extension(2 ^ 2,bind([[_59666, _59668], [436 ^ [], 435 ^ []]]))).
% 0.36/1.37 ncf('1.2.1.1',plain,[-(unequally_directed_opposite_lines(435 ^ [], 436 ^ [])), convergent_lines(435 ^ [], 436 ^ [])],extension(80 ^ 3,bind([[_62280, _62282], [436 ^ [], 435 ^ []]]))).
% 0.36/1.37 ncf('1.2.1.1.1',plain,[-(convergent_lines(435 ^ [], 436 ^ []))],extension(443 ^ 4)).
% 0.36/1.37 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([[_67725, _67727], [436 ^ [], 435 ^ []]]))).
% 0.36/1.37 ncf('1.2.2.1',plain,[-(unequally_directed_lines(435 ^ [], 436 ^ [])), convergent_lines(435 ^ [], 436 ^ [])],extension(80 ^ 3,bind([[_62280, _62282], [436 ^ [], 435 ^ []]]))).
% 0.36/1.37 ncf('1.2.2.1.1',plain,[-(convergent_lines(435 ^ [], 436 ^ []))],extension(443 ^ 4)).
% 0.36/1.37 ncf('1.2.2.2',plain,[left_convergent_lines(435 ^ [], 436 ^ [])],extension(266 ^ 3,bind([[_68290, _68292], [436 ^ [], 435 ^ []]]))).
% 0.36/1.37 ncf('1.2.2.3',plain,[left_convergent_lines(435 ^ [], reverse_line(436 ^ []))],extension(266 ^ 3,bind([[_68290, _68292], [reverse_line(436 ^ []), 435 ^ []]]))).
% 0.36/1.37 %-----------------------------------------------------
% 0.36/1.37 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------