%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO186+3 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n022.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:07 EDT 2023
% Result : Theorem 0.41s 1.39s
% Output : Proof 0.41s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GEO186+3 : TPTP v8.1.2. Released v4.0.0.
% 0.03/0.13 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n022.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Fri May 19 03:56:32 EDT 2023
% 0.13/0.35 % CPUTime :
% 0.41/1.39
% 0.41/1.39 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.41/1.39 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.41/1.39 %-----------------------------------------------------
% 0.41/1.39 ncf(matrix, plain, [(330 ^ _52033) ^ [] : [-(distinct_points(325 ^ [], 326 ^ []))], (332 ^ _52033) ^ [] : [-(convergent_lines(327 ^ [], 328 ^ []))], (334 ^ _52033) ^ [] : [-(incident_point_and_line(325 ^ [], 327 ^ []))], (336 ^ _52033) ^ [] : [-(incident_point_and_line(325 ^ [], 328 ^ []))], (338 ^ _52033) ^ [] : [equal_points(325 ^ [], intersection_point(327 ^ [], 328 ^ []))], (2 ^ _52033) ^ [_52136] : [distinct_points(_52136, _52136)], (4 ^ _52033) ^ [_52213] : [distinct_lines(_52213, _52213)], (6 ^ _52033) ^ [_52290] : [convergent_lines(_52290, _52290)], (8 ^ _52033) ^ [_52411, _52413, _52415] : [distinct_points(_52415, _52413), -(distinct_points(_52415, _52411)), -(distinct_points(_52413, _52411))], (18 ^ _52033) ^ [_52735, _52737, _52739] : [distinct_lines(_52739, _52737), -(distinct_lines(_52739, _52735)), -(distinct_lines(_52737, _52735))], (28 ^ _52033) ^ [_53059, _53061, _53063] : [convergent_lines(_53063, _53061), -(convergent_lines(_53063, _53059)), -(convergent_lines(_53061, _53059))], (38 ^ _52033) ^ [_53369, _53371] : [distinct_points(_53371, _53369), apart_point_and_line(_53371, line_connecting(_53371, _53369))], (44 ^ _52033) ^ [_53586, _53588] : [distinct_points(_53588, _53586), apart_point_and_line(_53586, line_connecting(_53588, _53586))], (50 ^ _52033) ^ [_53803, _53805] : [convergent_lines(_53805, _53803), apart_point_and_line(intersection_point(_53805, _53803), _53805)], (56 ^ _52033) ^ [_54020, _54022] : [convergent_lines(_54022, _54020), apart_point_and_line(intersection_point(_54022, _54020), _54020)], (62 ^ _52033) ^ [_54265, _54267, _54269, _54271] : [distinct_points(_54271, _54269), distinct_lines(_54267, _54265), -(apart_point_and_line(_54271, _54267)), -(apart_point_and_line(_54271, _54265)), -(apart_point_and_line(_54269, _54267)), -(apart_point_and_line(_54269, _54265))], (84 ^ _52033) ^ [_54894, _54896, _54898] : [apart_point_and_line(_54898, _54896), -(distinct_points(_54898, _54894)), -(apart_point_and_line(_54894, _54896))], (94 ^ _52033) ^ [_55218, _55220, _55222] : [apart_point_and_line(_55222, _55220), -(distinct_lines(_55220, _55218)), -(apart_point_and_line(_55222, _55218))], (104 ^ _52033) ^ [_55522, _55524, _55526] : [convergent_lines(_55526, _55524), -(distinct_lines(_55524, _55522)), -(convergent_lines(_55526, _55522))], (114 ^ _52033) ^ [_55858, _55860] : [distinct_lines(_55860, _55858), -(convergent_lines(_55860, _55858))], (120 ^ _52033) ^ [_56072, _56074] : [convergent_lines(parallel_through_point(_56072, _56074), _56072)], (122 ^ _52033) ^ [_56168, _56170] : [apart_point_and_line(_56170, parallel_through_point(_56168, _56170))], (124 ^ _52033) ^ [_56274, _56276, _56278] : [distinct_lines(_56276, _56274), -(apart_point_and_line(_56278, _56276)), -(apart_point_and_line(_56278, _56274)), -(convergent_lines(_56276, _56274))], (138 ^ _52033) ^ [_56702, _56704] : [-(convergent_lines(_56704, _56702)), -(unorthogonal_lines(_56704, _56702))], (144 ^ _52033) ^ [_56927, _56929, _56931] : [convergent_lines(_56931, _56929), unorthogonal_lines(_56931, _56929), 153 ^ _52033 : [(154 ^ _52033) ^ [] : [-(convergent_lines(_56931, _56927))], (156 ^ _52033) ^ [] : [-(unorthogonal_lines(_56931, _56927))]], 157 ^ _52033 : [(158 ^ _52033) ^ [] : [-(convergent_lines(_56929, _56927))], (160 ^ _52033) ^ [] : [-(unorthogonal_lines(_56929, _56927))]]], (162 ^ _52033) ^ [_57470, _57472] : [unorthogonal_lines(orthogonal_through_point(_57470, _57472), _57470)], (164 ^ _52033) ^ [_57566, _57568] : [apart_point_and_line(_57568, orthogonal_through_point(_57566, _57568))], (166 ^ _52033) ^ [_57686, _57688, _57690, _57692] : [distinct_lines(_57690, _57688), -(apart_point_and_line(_57692, _57690)), -(apart_point_and_line(_57692, _57688)), -(unorthogonal_lines(_57690, _57686)), -(unorthogonal_lines(_57688, _57686))], (184 ^ _52033) ^ [_58230, _58232] : [-(convergent_lines(_58232, _58230)), -(unorthogonal_lines(_58232, _58230))], (208 ^ _52033) ^ [_59024, _59026, _59028] : [convergent_lines(_59026, _59024), -(unorthogonal_lines(_59028, _59026)), -(unorthogonal_lines(_59028, _59024))], (190 ^ _52033) ^ [_58459, _58461, _58463] : [193 ^ _52033 : [(194 ^ _52033) ^ [] : [-(convergent_lines(_58463, _58461))], (196 ^ _52033) ^ [] : [-(unorthogonal_lines(_58463, _58461))]], 197 ^ _52033 : [(198 ^ _52033) ^ [] : [-(convergent_lines(_58463, _58459))], (200 ^ _52033) ^ [] : [-(unorthogonal_lines(_58463, _58459))]], convergent_lines(_58461, _58459), unorthogonal_lines(_58461, _58459)], (218 ^ _52033) ^ [_59364, _59366] : [-(line(line_connecting(_59366, _59364))), point(_59366), point(_59364), distinct_points(_59366, _59364)], (232 ^ _52033) ^ [_59752, _59754] : [-(point(intersection_point(_59754, _59752))), line(_59754), line(_59752), convergent_lines(_59754, _59752)], (246 ^ _52033) ^ [_60140, _60142] : [-(line(parallel_through_point(_60142, _60140))), line(_60142), point(_60140)], (256 ^ _52033) ^ [_60419, _60421] : [-(line(orthogonal_through_point(_60421, _60419))), line(_60421), point(_60419)], (266 ^ _52033) ^ [_60753, _60755] : [equal_points(_60755, _60753), distinct_points(_60755, _60753)], (272 ^ _52033) ^ [_60916, _60918] : [-(distinct_points(_60918, _60916)), -(equal_points(_60918, _60916))], (278 ^ _52033) ^ [_61160, _61162] : [equal_lines(_61162, _61160), distinct_lines(_61162, _61160)], (284 ^ _52033) ^ [_61323, _61325] : [-(distinct_lines(_61325, _61323)), -(equal_lines(_61325, _61323))], (290 ^ _52033) ^ [_61567, _61569] : [parallel_lines(_61569, _61567), convergent_lines(_61569, _61567)], (296 ^ _52033) ^ [_61730, _61732] : [-(convergent_lines(_61732, _61730)), -(parallel_lines(_61732, _61730))], (302 ^ _52033) ^ [_61974, _61976] : [incident_point_and_line(_61976, _61974), apart_point_and_line(_61976, _61974)], (308 ^ _52033) ^ [_62137, _62139] : [-(apart_point_and_line(_62139, _62137)), -(incident_point_and_line(_62139, _62137))], (314 ^ _52033) ^ [_62361, _62363] : [orthogonal_lines(_62363, _62361), unorthogonal_lines(_62363, _62361)], (320 ^ _52033) ^ [_62524, _62526] : [-(unorthogonal_lines(_62526, _62524)), -(orthogonal_lines(_62526, _62524))]], input).
% 0.41/1.39 ncf('1',plain,[convergent_lines(327 ^ [], 328 ^ []), apart_point_and_line(intersection_point(327 ^ [], 328 ^ []), 327 ^ [])],start(50 ^ 0,bind([[_53803, _53805], [328 ^ [], 327 ^ []]]))).
% 0.41/1.39 ncf('1.1',plain,[-(convergent_lines(327 ^ [], 328 ^ []))],extension(332 ^ 1)).
% 0.41/1.39 ncf('1.2',plain,[-(apart_point_and_line(intersection_point(327 ^ [], 328 ^ []), 327 ^ [])), distinct_points(intersection_point(327 ^ [], 328 ^ []), 325 ^ []), distinct_lines(328 ^ [], 327 ^ []), -(apart_point_and_line(intersection_point(327 ^ [], 328 ^ []), 328 ^ [])), -(apart_point_and_line(325 ^ [], 328 ^ [])), -(apart_point_and_line(325 ^ [], 327 ^ []))],extension(62 ^ 1,bind([[_54265, _54267, _54269, _54271], [327 ^ [], 328 ^ [], 325 ^ [], intersection_point(327 ^ [], 328 ^ [])]]))).
% 0.41/1.39 ncf('1.2.1',plain,[-(distinct_points(intersection_point(327 ^ [], 328 ^ []), 325 ^ [])), distinct_points(325 ^ [], intersection_point(327 ^ [], 328 ^ [])), -(distinct_points(325 ^ [], 325 ^ []))],extension(8 ^ 2,bind([[_52411, _52413, _52415], [325 ^ [], intersection_point(327 ^ [], 328 ^ []), 325 ^ []]]))).
% 0.41/1.39 ncf('1.2.1.1',plain,[-(distinct_points(325 ^ [], intersection_point(327 ^ [], 328 ^ []))), -(equal_points(325 ^ [], intersection_point(327 ^ [], 328 ^ [])))],extension(272 ^ 3,bind([[_60916, _60918], [intersection_point(327 ^ [], 328 ^ []), 325 ^ []]]))).
% 0.41/1.39 ncf('1.2.1.1.1',plain,[equal_points(325 ^ [], intersection_point(327 ^ [], 328 ^ []))],extension(338 ^ 4)).
% 0.41/1.39 ncf('1.2.1.2',plain,[distinct_points(325 ^ [], 325 ^ [])],extension(2 ^ 3,bind([[_52136], [325 ^ []]]))).
% 0.41/1.39 ncf('1.2.2',plain,[-(distinct_lines(328 ^ [], 327 ^ [])), convergent_lines(327 ^ [], 328 ^ []), -(convergent_lines(327 ^ [], 327 ^ []))],extension(104 ^ 2,bind([[_55522, _55524, _55526], [327 ^ [], 328 ^ [], 327 ^ []]]))).
% 0.41/1.39 ncf('1.2.2.1',plain,[-(convergent_lines(327 ^ [], 328 ^ []))],extension(332 ^ 3)).
% 0.41/1.39 ncf('1.2.2.2',plain,[convergent_lines(327 ^ [], 327 ^ [])],extension(6 ^ 3,bind([[_52290], [327 ^ []]]))).
% 0.41/1.39 ncf('1.2.3',plain,[apart_point_and_line(intersection_point(327 ^ [], 328 ^ []), 328 ^ []), convergent_lines(327 ^ [], 328 ^ [])],extension(56 ^ 2,bind([[_54020, _54022], [328 ^ [], 327 ^ []]]))).
% 0.41/1.39 ncf('1.2.3.1',plain,[-(convergent_lines(327 ^ [], 328 ^ []))],lemmata('x')).
% 0.41/1.39 ncf('1.2.4',plain,[apart_point_and_line(325 ^ [], 328 ^ []), incident_point_and_line(325 ^ [], 328 ^ [])],extension(302 ^ 2,bind([[_61974, _61976], [328 ^ [], 325 ^ []]]))).
% 0.41/1.39 ncf('1.2.4.1',plain,[-(incident_point_and_line(325 ^ [], 328 ^ []))],extension(336 ^ 3)).
% 0.41/1.39 ncf('1.2.5',plain,[apart_point_and_line(325 ^ [], 327 ^ []), incident_point_and_line(325 ^ [], 327 ^ [])],extension(302 ^ 2,bind([[_61974, _61976], [327 ^ [], 325 ^ []]]))).
% 0.41/1.39 ncf('1.2.5.1',plain,[-(incident_point_and_line(325 ^ [], 327 ^ []))],extension(334 ^ 3)).
% 0.41/1.39 %-----------------------------------------------------
% 0.41/1.39 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------