%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO181+3 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n001.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:05 EDT 2023
% Result : Theorem 0.38s 1.37s
% Output : Proof 0.38s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GEO181+3 : TPTP v8.1.2. Released v4.0.0.
% 0.00/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n001.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 05:07:35 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.38/1.37
% 0.38/1.37 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.38/1.37 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.38/1.37 %-----------------------------------------------------
% 0.38/1.37 ncf(matrix, plain, [(329 ^ _49959) ^ [] : [-(distinct_points(325 ^ [], 326 ^ []))], (331 ^ _49959) ^ [] : [-(apart_point_and_line(327 ^ [], line_connecting(325 ^ [], 326 ^ [])))], (333 ^ _49959) ^ [] : [apart_point_and_line(326 ^ [], line_connecting(325 ^ [], 327 ^ []))], (2 ^ _49959) ^ [_50062] : [distinct_points(_50062, _50062)], (4 ^ _49959) ^ [_50139] : [distinct_lines(_50139, _50139)], (6 ^ _49959) ^ [_50216] : [convergent_lines(_50216, _50216)], (8 ^ _49959) ^ [_50337, _50339, _50341] : [distinct_points(_50341, _50339), -(distinct_points(_50341, _50337)), -(distinct_points(_50339, _50337))], (18 ^ _49959) ^ [_50661, _50663, _50665] : [distinct_lines(_50665, _50663), -(distinct_lines(_50665, _50661)), -(distinct_lines(_50663, _50661))], (28 ^ _49959) ^ [_50985, _50987, _50989] : [convergent_lines(_50989, _50987), -(convergent_lines(_50989, _50985)), -(convergent_lines(_50987, _50985))], (38 ^ _49959) ^ [_51295, _51297] : [distinct_points(_51297, _51295), apart_point_and_line(_51297, line_connecting(_51297, _51295))], (44 ^ _49959) ^ [_51512, _51514] : [distinct_points(_51514, _51512), apart_point_and_line(_51512, line_connecting(_51514, _51512))], (50 ^ _49959) ^ [_51729, _51731] : [convergent_lines(_51731, _51729), apart_point_and_line(intersection_point(_51731, _51729), _51731)], (56 ^ _49959) ^ [_51946, _51948] : [convergent_lines(_51948, _51946), apart_point_and_line(intersection_point(_51948, _51946), _51946)], (62 ^ _49959) ^ [_52191, _52193, _52195, _52197] : [distinct_points(_52197, _52195), distinct_lines(_52193, _52191), -(apart_point_and_line(_52197, _52193)), -(apart_point_and_line(_52197, _52191)), -(apart_point_and_line(_52195, _52193)), -(apart_point_and_line(_52195, _52191))], (84 ^ _49959) ^ [_52820, _52822, _52824] : [apart_point_and_line(_52824, _52822), -(distinct_points(_52824, _52820)), -(apart_point_and_line(_52820, _52822))], (94 ^ _49959) ^ [_53144, _53146, _53148] : [apart_point_and_line(_53148, _53146), -(distinct_lines(_53146, _53144)), -(apart_point_and_line(_53148, _53144))], (104 ^ _49959) ^ [_53448, _53450, _53452] : [convergent_lines(_53452, _53450), -(distinct_lines(_53450, _53448)), -(convergent_lines(_53452, _53448))], (114 ^ _49959) ^ [_53784, _53786] : [distinct_lines(_53786, _53784), -(convergent_lines(_53786, _53784))], (120 ^ _49959) ^ [_53998, _54000] : [convergent_lines(parallel_through_point(_53998, _54000), _53998)], (122 ^ _49959) ^ [_54094, _54096] : [apart_point_and_line(_54096, parallel_through_point(_54094, _54096))], (124 ^ _49959) ^ [_54200, _54202, _54204] : [distinct_lines(_54202, _54200), -(apart_point_and_line(_54204, _54202)), -(apart_point_and_line(_54204, _54200)), -(convergent_lines(_54202, _54200))], (138 ^ _49959) ^ [_54628, _54630] : [-(convergent_lines(_54630, _54628)), -(unorthogonal_lines(_54630, _54628))], (144 ^ _49959) ^ [_54853, _54855, _54857] : [convergent_lines(_54857, _54855), unorthogonal_lines(_54857, _54855), 153 ^ _49959 : [(154 ^ _49959) ^ [] : [-(convergent_lines(_54857, _54853))], (156 ^ _49959) ^ [] : [-(unorthogonal_lines(_54857, _54853))]], 157 ^ _49959 : [(158 ^ _49959) ^ [] : [-(convergent_lines(_54855, _54853))], (160 ^ _49959) ^ [] : [-(unorthogonal_lines(_54855, _54853))]]], (162 ^ _49959) ^ [_55396, _55398] : [unorthogonal_lines(orthogonal_through_point(_55396, _55398), _55396)], (164 ^ _49959) ^ [_55492, _55494] : [apart_point_and_line(_55494, orthogonal_through_point(_55492, _55494))], (166 ^ _49959) ^ [_55612, _55614, _55616, _55618] : [distinct_lines(_55616, _55614), -(apart_point_and_line(_55618, _55616)), -(apart_point_and_line(_55618, _55614)), -(unorthogonal_lines(_55616, _55612)), -(unorthogonal_lines(_55614, _55612))], (184 ^ _49959) ^ [_56156, _56158] : [-(convergent_lines(_56158, _56156)), -(unorthogonal_lines(_56158, _56156))], (208 ^ _49959) ^ [_56950, _56952, _56954] : [convergent_lines(_56952, _56950), -(unorthogonal_lines(_56954, _56952)), -(unorthogonal_lines(_56954, _56950))], (190 ^ _49959) ^ [_56385, _56387, _56389] : [193 ^ _49959 : [(194 ^ _49959) ^ [] : [-(convergent_lines(_56389, _56387))], (196 ^ _49959) ^ [] : [-(unorthogonal_lines(_56389, _56387))]], 197 ^ _49959 : [(198 ^ _49959) ^ [] : [-(convergent_lines(_56389, _56385))], (200 ^ _49959) ^ [] : [-(unorthogonal_lines(_56389, _56385))]], convergent_lines(_56387, _56385), unorthogonal_lines(_56387, _56385)], (218 ^ _49959) ^ [_57290, _57292] : [-(line(line_connecting(_57292, _57290))), point(_57292), point(_57290), distinct_points(_57292, _57290)], (232 ^ _49959) ^ [_57678, _57680] : [-(point(intersection_point(_57680, _57678))), line(_57680), line(_57678), convergent_lines(_57680, _57678)], (246 ^ _49959) ^ [_58066, _58068] : [-(line(parallel_through_point(_58068, _58066))), line(_58068), point(_58066)], (256 ^ _49959) ^ [_58345, _58347] : [-(line(orthogonal_through_point(_58347, _58345))), line(_58347), point(_58345)], (266 ^ _49959) ^ [_58679, _58681] : [equal_points(_58681, _58679), distinct_points(_58681, _58679)], (272 ^ _49959) ^ [_58842, _58844] : [-(distinct_points(_58844, _58842)), -(equal_points(_58844, _58842))], (278 ^ _49959) ^ [_59086, _59088] : [equal_lines(_59088, _59086), distinct_lines(_59088, _59086)], (284 ^ _49959) ^ [_59249, _59251] : [-(distinct_lines(_59251, _59249)), -(equal_lines(_59251, _59249))], (290 ^ _49959) ^ [_59493, _59495] : [parallel_lines(_59495, _59493), convergent_lines(_59495, _59493)], (296 ^ _49959) ^ [_59656, _59658] : [-(convergent_lines(_59658, _59656)), -(parallel_lines(_59658, _59656))], (302 ^ _49959) ^ [_59900, _59902] : [incident_point_and_line(_59902, _59900), apart_point_and_line(_59902, _59900)], (308 ^ _49959) ^ [_60063, _60065] : [-(apart_point_and_line(_60065, _60063)), -(incident_point_and_line(_60065, _60063))], (314 ^ _49959) ^ [_60287, _60289] : [orthogonal_lines(_60289, _60287), unorthogonal_lines(_60289, _60287)], (320 ^ _49959) ^ [_60450, _60452] : [-(unorthogonal_lines(_60452, _60450)), -(orthogonal_lines(_60452, _60450))]], input).
% 0.38/1.37 ncf('1',plain,[distinct_lines(line_connecting(325 ^ [], 326 ^ []), line_connecting(325 ^ [], 326 ^ []))],start(4 ^ 0,bind([[_50139], [line_connecting(325 ^ [], 326 ^ [])]]))).
% 0.38/1.37 ncf('1.1',plain,[-(distinct_lines(line_connecting(325 ^ [], 326 ^ []), line_connecting(325 ^ [], 326 ^ []))), distinct_lines(line_connecting(325 ^ [], 326 ^ []), parallel_through_point(line_connecting(325 ^ [], 326 ^ []), 327 ^ [])), -(distinct_lines(parallel_through_point(line_connecting(325 ^ [], 326 ^ []), 327 ^ []), line_connecting(325 ^ [], 326 ^ [])))],extension(18 ^ 1,bind([[_50661, _50663, _50665], [line_connecting(325 ^ [], 326 ^ []), parallel_through_point(line_connecting(325 ^ [], 326 ^ []), 327 ^ []), line_connecting(325 ^ [], 326 ^ [])]]))).
% 0.38/1.37 ncf('1.1.1',plain,[-(distinct_lines(line_connecting(325 ^ [], 326 ^ []), parallel_through_point(line_connecting(325 ^ [], 326 ^ []), 327 ^ []))), apart_point_and_line(327 ^ [], line_connecting(325 ^ [], 326 ^ [])), -(apart_point_and_line(327 ^ [], parallel_through_point(line_connecting(325 ^ [], 326 ^ []), 327 ^ [])))],extension(94 ^ 2,bind([[_53144, _53146, _53148], [parallel_through_point(line_connecting(325 ^ [], 326 ^ []), 327 ^ []), line_connecting(325 ^ [], 326 ^ []), 327 ^ []]]))).
% 0.38/1.37 ncf('1.1.1.1',plain,[-(apart_point_and_line(327 ^ [], line_connecting(325 ^ [], 326 ^ [])))],extension(331 ^ 3)).
% 0.38/1.37 ncf('1.1.1.2',plain,[apart_point_and_line(327 ^ [], parallel_through_point(line_connecting(325 ^ [], 326 ^ []), 327 ^ []))],extension(122 ^ 3,bind([[_54094, _54096], [line_connecting(325 ^ [], 326 ^ []), 327 ^ []]]))).
% 0.38/1.37 ncf('1.1.2',plain,[distinct_lines(parallel_through_point(line_connecting(325 ^ [], 326 ^ []), 327 ^ []), line_connecting(325 ^ [], 326 ^ [])), -(convergent_lines(parallel_through_point(line_connecting(325 ^ [], 326 ^ []), 327 ^ []), line_connecting(325 ^ [], 326 ^ [])))],extension(114 ^ 2,bind([[_53784, _53786], [line_connecting(325 ^ [], 326 ^ []), parallel_through_point(line_connecting(325 ^ [], 326 ^ []), 327 ^ [])]]))).
% 0.38/1.37 ncf('1.1.2.1',plain,[convergent_lines(parallel_through_point(line_connecting(325 ^ [], 326 ^ []), 327 ^ []), line_connecting(325 ^ [], 326 ^ []))],extension(120 ^ 3,bind([[_53998, _54000], [line_connecting(325 ^ [], 326 ^ []), 327 ^ []]]))).
% 0.38/1.37 %-----------------------------------------------------
% 0.38/1.37 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------