%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO183+3 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n023.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:06 EDT 2023
% Result : Theorem 38.60s 37.53s
% Output : Proof 38.60s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : GEO183+3 : TPTP v8.1.2. Released v4.0.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n023.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:48:28 EDT 2023
% 0.12/0.33 % CPUTime :
% 38.60/37.53
% 38.60/37.53 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 38.60/37.53 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 38.60/37.53 %-----------------------------------------------------
% 38.60/37.53 ncf(matrix, plain, [(330 ^ _51389) ^ [] : [-(distinct_points(325 ^ [], 326 ^ []))], (332 ^ _51389) ^ [] : [-(convergent_lines(327 ^ [], 328 ^ []))], (334 ^ _51389) ^ [] : [-(equal_lines(327 ^ [], line_connecting(325 ^ [], 326 ^ [])))], (336 ^ _51389) ^ [] : [incident_point_and_line(325 ^ [], 327 ^ []), incident_point_and_line(326 ^ [], 327 ^ [])], (2 ^ _51389) ^ [_51492] : [distinct_points(_51492, _51492)], (4 ^ _51389) ^ [_51569] : [distinct_lines(_51569, _51569)], (6 ^ _51389) ^ [_51646] : [convergent_lines(_51646, _51646)], (8 ^ _51389) ^ [_51767, _51769, _51771] : [distinct_points(_51771, _51769), -(distinct_points(_51771, _51767)), -(distinct_points(_51769, _51767))], (18 ^ _51389) ^ [_52091, _52093, _52095] : [distinct_lines(_52095, _52093), -(distinct_lines(_52095, _52091)), -(distinct_lines(_52093, _52091))], (28 ^ _51389) ^ [_52415, _52417, _52419] : [convergent_lines(_52419, _52417), -(convergent_lines(_52419, _52415)), -(convergent_lines(_52417, _52415))], (38 ^ _51389) ^ [_52725, _52727] : [distinct_points(_52727, _52725), apart_point_and_line(_52727, line_connecting(_52727, _52725))], (44 ^ _51389) ^ [_52942, _52944] : [distinct_points(_52944, _52942), apart_point_and_line(_52942, line_connecting(_52944, _52942))], (50 ^ _51389) ^ [_53159, _53161] : [convergent_lines(_53161, _53159), apart_point_and_line(intersection_point(_53161, _53159), _53161)], (56 ^ _51389) ^ [_53376, _53378] : [convergent_lines(_53378, _53376), apart_point_and_line(intersection_point(_53378, _53376), _53376)], (62 ^ _51389) ^ [_53621, _53623, _53625, _53627] : [distinct_points(_53627, _53625), distinct_lines(_53623, _53621), -(apart_point_and_line(_53627, _53623)), -(apart_point_and_line(_53627, _53621)), -(apart_point_and_line(_53625, _53623)), -(apart_point_and_line(_53625, _53621))], (84 ^ _51389) ^ [_54250, _54252, _54254] : [apart_point_and_line(_54254, _54252), -(distinct_points(_54254, _54250)), -(apart_point_and_line(_54250, _54252))], (94 ^ _51389) ^ [_54574, _54576, _54578] : [apart_point_and_line(_54578, _54576), -(distinct_lines(_54576, _54574)), -(apart_point_and_line(_54578, _54574))], (104 ^ _51389) ^ [_54878, _54880, _54882] : [convergent_lines(_54882, _54880), -(distinct_lines(_54880, _54878)), -(convergent_lines(_54882, _54878))], (114 ^ _51389) ^ [_55214, _55216] : [distinct_lines(_55216, _55214), -(convergent_lines(_55216, _55214))], (120 ^ _51389) ^ [_55428, _55430] : [convergent_lines(parallel_through_point(_55428, _55430), _55428)], (122 ^ _51389) ^ [_55524, _55526] : [apart_point_and_line(_55526, parallel_through_point(_55524, _55526))], (124 ^ _51389) ^ [_55630, _55632, _55634] : [distinct_lines(_55632, _55630), -(apart_point_and_line(_55634, _55632)), -(apart_point_and_line(_55634, _55630)), -(convergent_lines(_55632, _55630))], (138 ^ _51389) ^ [_56058, _56060] : [-(convergent_lines(_56060, _56058)), -(unorthogonal_lines(_56060, _56058))], (144 ^ _51389) ^ [_56283, _56285, _56287] : [convergent_lines(_56287, _56285), unorthogonal_lines(_56287, _56285), 153 ^ _51389 : [(154 ^ _51389) ^ [] : [-(convergent_lines(_56287, _56283))], (156 ^ _51389) ^ [] : [-(unorthogonal_lines(_56287, _56283))]], 157 ^ _51389 : [(158 ^ _51389) ^ [] : [-(convergent_lines(_56285, _56283))], (160 ^ _51389) ^ [] : [-(unorthogonal_lines(_56285, _56283))]]], (162 ^ _51389) ^ [_56826, _56828] : [unorthogonal_lines(orthogonal_through_point(_56826, _56828), _56826)], (164 ^ _51389) ^ [_56922, _56924] : [apart_point_and_line(_56924, orthogonal_through_point(_56922, _56924))], (166 ^ _51389) ^ [_57042, _57044, _57046, _57048] : [distinct_lines(_57046, _57044), -(apart_point_and_line(_57048, _57046)), -(apart_point_and_line(_57048, _57044)), -(unorthogonal_lines(_57046, _57042)), -(unorthogonal_lines(_57044, _57042))], (184 ^ _51389) ^ [_57586, _57588] : [-(convergent_lines(_57588, _57586)), -(unorthogonal_lines(_57588, _57586))], (208 ^ _51389) ^ [_58380, _58382, _58384] : [convergent_lines(_58382, _58380), -(unorthogonal_lines(_58384, _58382)), -(unorthogonal_lines(_58384, _58380))], (190 ^ _51389) ^ [_57815, _57817, _57819] : [193 ^ _51389 : [(194 ^ _51389) ^ [] : [-(convergent_lines(_57819, _57817))], (196 ^ _51389) ^ [] : [-(unorthogonal_lines(_57819, _57817))]], 197 ^ _51389 : [(198 ^ _51389) ^ [] : [-(convergent_lines(_57819, _57815))], (200 ^ _51389) ^ [] : [-(unorthogonal_lines(_57819, _57815))]], convergent_lines(_57817, _57815), unorthogonal_lines(_57817, _57815)], (218 ^ _51389) ^ [_58720, _58722] : [-(line(line_connecting(_58722, _58720))), point(_58722), point(_58720), distinct_points(_58722, _58720)], (232 ^ _51389) ^ [_59108, _59110] : [-(point(intersection_point(_59110, _59108))), line(_59110), line(_59108), convergent_lines(_59110, _59108)], (246 ^ _51389) ^ [_59496, _59498] : [-(line(parallel_through_point(_59498, _59496))), line(_59498), point(_59496)], (256 ^ _51389) ^ [_59775, _59777] : [-(line(orthogonal_through_point(_59777, _59775))), line(_59777), point(_59775)], (266 ^ _51389) ^ [_60109, _60111] : [equal_points(_60111, _60109), distinct_points(_60111, _60109)], (272 ^ _51389) ^ [_60272, _60274] : [-(distinct_points(_60274, _60272)), -(equal_points(_60274, _60272))], (278 ^ _51389) ^ [_60516, _60518] : [equal_lines(_60518, _60516), distinct_lines(_60518, _60516)], (284 ^ _51389) ^ [_60679, _60681] : [-(distinct_lines(_60681, _60679)), -(equal_lines(_60681, _60679))], (290 ^ _51389) ^ [_60923, _60925] : [parallel_lines(_60925, _60923), convergent_lines(_60925, _60923)], (296 ^ _51389) ^ [_61086, _61088] : [-(convergent_lines(_61088, _61086)), -(parallel_lines(_61088, _61086))], (302 ^ _51389) ^ [_61330, _61332] : [incident_point_and_line(_61332, _61330), apart_point_and_line(_61332, _61330)], (308 ^ _51389) ^ [_61493, _61495] : [-(apart_point_and_line(_61495, _61493)), -(incident_point_and_line(_61495, _61493))], (314 ^ _51389) ^ [_61717, _61719] : [orthogonal_lines(_61719, _61717), unorthogonal_lines(_61719, _61717)], (320 ^ _51389) ^ [_61880, _61882] : [-(unorthogonal_lines(_61882, _61880)), -(orthogonal_lines(_61882, _61880))]], input).
% 38.60/37.53 ncf('1',plain,[equal_lines(327 ^ [], line_connecting(325 ^ [], 326 ^ [])), distinct_lines(327 ^ [], line_connecting(325 ^ [], 326 ^ []))],start(278 ^ 0,bind([[_60516, _60518], [line_connecting(325 ^ [], 326 ^ []), 327 ^ []]]))).
% 38.60/37.53 ncf('1.1',plain,[-(equal_lines(327 ^ [], line_connecting(325 ^ [], 326 ^ [])))],extension(334 ^ 1)).
% 38.60/37.53 ncf('1.2',plain,[-(distinct_lines(327 ^ [], line_connecting(325 ^ [], 326 ^ []))), apart_point_and_line(325 ^ [], 327 ^ []), -(apart_point_and_line(325 ^ [], line_connecting(325 ^ [], 326 ^ [])))],extension(94 ^ 1,bind([[_54574, _54576, _54578], [line_connecting(325 ^ [], 326 ^ []), 327 ^ [], 325 ^ []]]))).
% 38.60/37.53 ncf('1.2.1',plain,[-(apart_point_and_line(325 ^ [], 327 ^ [])), -(incident_point_and_line(325 ^ [], 327 ^ []))],extension(308 ^ 2,bind([[_61493, _61495], [327 ^ [], 325 ^ []]]))).
% 38.60/37.53 ncf('1.2.1.1',plain,[incident_point_and_line(325 ^ [], 327 ^ []), incident_point_and_line(326 ^ [], 327 ^ [])],extension(336 ^ 3)).
% 38.60/37.53 ncf('1.2.1.1.1',plain,[-(incident_point_and_line(326 ^ [], 327 ^ [])), -(apart_point_and_line(326 ^ [], 327 ^ []))],extension(308 ^ 4,bind([[_61493, _61495], [327 ^ [], 326 ^ []]]))).
% 38.60/37.53 ncf('1.2.1.1.1.1',plain,[apart_point_and_line(326 ^ [], 327 ^ []), -(distinct_lines(327 ^ [], line_connecting(325 ^ [], 326 ^ []))), -(apart_point_and_line(326 ^ [], line_connecting(325 ^ [], 326 ^ [])))],extension(94 ^ 5,bind([[_54574, _54576, _54578], [line_connecting(325 ^ [], 326 ^ []), 327 ^ [], 326 ^ []]]))).
% 38.60/37.53 ncf('1.2.1.1.1.1.1',plain,[distinct_lines(327 ^ [], line_connecting(325 ^ [], 326 ^ []))],reduction('1')).
% 38.60/37.53 ncf('1.2.1.1.1.1.2',plain,[apart_point_and_line(326 ^ [], line_connecting(325 ^ [], 326 ^ [])), distinct_points(325 ^ [], 326 ^ [])],extension(44 ^ 6,bind([[_52942, _52944], [326 ^ [], 325 ^ []]]))).
% 38.60/37.53 ncf('1.2.1.1.1.1.2.1',plain,[-(distinct_points(325 ^ [], 326 ^ []))],extension(330 ^ 7)).
% 38.60/37.53 ncf('1.2.2',plain,[apart_point_and_line(325 ^ [], line_connecting(325 ^ [], 326 ^ [])), distinct_points(325 ^ [], 326 ^ [])],extension(38 ^ 2,bind([[_52725, _52727], [326 ^ [], 325 ^ []]]))).
% 38.60/37.53 ncf('1.2.2.1',plain,[-(distinct_points(325 ^ [], 326 ^ []))],extension(330 ^ 3)).
% 38.60/37.53 %-----------------------------------------------------
% 38.60/37.53 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------