%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO214+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n019.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:15 EDT 2023
% Result : Theorem 0.27s 1.36s
% Output : Proof 0.27s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : GEO214+1 : TPTP v8.1.2. Released v3.3.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.12/0.32 % Computer : n019.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 300
% 0.12/0.32 % DateTime : Fri May 19 04:08:27 EDT 2023
% 0.12/0.32 % CPUTime :
% 0.27/1.36
% 0.27/1.36 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.27/1.36 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.27/1.36 %-----------------------------------------------------
% 0.27/1.36 ncf(matrix, plain, [(180 ^ _31464) ^ [] : [-(unorthogonal_lines(177 ^ [], 178 ^ []))], (182 ^ _31464) ^ [] : [unorthogonal_lines(178 ^ [], 177 ^ [])], (114 ^ _31464) ^ [_35293, _35295] : [convergent_lines(parallel_through_point(_35293, _35295), _35293)], (116 ^ _31464) ^ [_35389, _35391] : [apart_point_and_line(_35391, parallel_through_point(_35389, _35391))], (118 ^ _31464) ^ [_35495, _35497, _35499] : [distinct_lines(_35497, _35495), -(apart_point_and_line(_35499, _35497)), -(apart_point_and_line(_35499, _35495)), -(convergent_lines(_35497, _35495))], (132 ^ _31464) ^ [_35903, _35905] : [-(convergent_lines(_35905, _35903)), -(unorthogonal_lines(_35905, _35903))], (138 ^ _31464) ^ [_36128, _36130, _36132] : [convergent_lines(_36132, _36130), unorthogonal_lines(_36132, _36130), 147 ^ _31464 : [(148 ^ _31464) ^ [] : [-(convergent_lines(_36132, _36128))], (150 ^ _31464) ^ [] : [-(unorthogonal_lines(_36132, _36128))]], 151 ^ _31464 : [(152 ^ _31464) ^ [] : [-(convergent_lines(_36130, _36128))], (154 ^ _31464) ^ [] : [-(unorthogonal_lines(_36130, _36128))]]], (156 ^ _31464) ^ [_36671, _36673] : [unorthogonal_lines(orthogonal_through_point(_36671, _36673), _36671)], (158 ^ _31464) ^ [_36767, _36769] : [apart_point_and_line(_36769, orthogonal_through_point(_36767, _36769))], (160 ^ _31464) ^ [_36887, _36889, _36891, _36893] : [distinct_lines(_36891, _36889), -(apart_point_and_line(_36893, _36891)), -(apart_point_and_line(_36893, _36889)), -(unorthogonal_lines(_36891, _36887)), -(unorthogonal_lines(_36889, _36887))], (2 ^ _31464) ^ [_31567] : [distinct_points(_31567, _31567)], (4 ^ _31464) ^ [_31644] : [distinct_lines(_31644, _31644)], (6 ^ _31464) ^ [_31721] : [convergent_lines(_31721, _31721)], (8 ^ _31464) ^ [_31842, _31844, _31846] : [distinct_points(_31846, _31844), -(distinct_points(_31846, _31842)), -(distinct_points(_31844, _31842))], (18 ^ _31464) ^ [_32166, _32168, _32170] : [distinct_lines(_32170, _32168), -(distinct_lines(_32170, _32166)), -(distinct_lines(_32168, _32166))], (28 ^ _31464) ^ [_32490, _32492, _32494] : [convergent_lines(_32494, _32492), -(convergent_lines(_32494, _32490)), -(convergent_lines(_32492, _32490))], (38 ^ _31464) ^ [_32800, _32802] : [distinct_points(_32802, _32800), apart_point_and_line(_32802, line_connecting(_32802, _32800))], (44 ^ _31464) ^ [_33017, _33019] : [distinct_points(_33019, _33017), apart_point_and_line(_33017, line_connecting(_33019, _33017))], (50 ^ _31464) ^ [_33234, _33236] : [convergent_lines(_33236, _33234), apart_point_and_line(intersection_point(_33236, _33234), _33236)], (56 ^ _31464) ^ [_33451, _33453] : [convergent_lines(_33453, _33451), apart_point_and_line(intersection_point(_33453, _33451), _33451)], (62 ^ _31464) ^ [_33696, _33698, _33700, _33702] : [distinct_points(_33702, _33700), distinct_lines(_33698, _33696), -(apart_point_and_line(_33702, _33698)), -(apart_point_and_line(_33702, _33696)), -(apart_point_and_line(_33700, _33698)), -(apart_point_and_line(_33700, _33696))], (84 ^ _31464) ^ [_34325, _34327, _34329] : [apart_point_and_line(_34329, _34327), -(distinct_points(_34329, _34325)), -(apart_point_and_line(_34325, _34327))], (94 ^ _31464) ^ [_34649, _34651, _34653] : [apart_point_and_line(_34653, _34651), -(distinct_lines(_34651, _34649)), -(apart_point_and_line(_34653, _34649))], (104 ^ _31464) ^ [_34953, _34955, _34957] : [convergent_lines(_34957, _34955), -(distinct_lines(_34955, _34953)), -(convergent_lines(_34957, _34953))]], input).
% 0.27/1.36 ncf('1',plain,[convergent_lines(178 ^ [], 178 ^ [])],start(6 ^ 0,bind([[_31721], [178 ^ []]]))).
% 0.27/1.36 ncf('1.1',plain,[-(convergent_lines(178 ^ [], 178 ^ [])), convergent_lines(178 ^ [], 177 ^ []), -(convergent_lines(177 ^ [], 178 ^ []))],extension(28 ^ 1,bind([[_32490, _32492, _32494], [178 ^ [], 177 ^ [], 178 ^ []]]))).
% 0.27/1.36 ncf('1.1.1',plain,[-(convergent_lines(178 ^ [], 177 ^ [])), -(unorthogonal_lines(178 ^ [], 177 ^ []))],extension(132 ^ 2,bind([[_35903, _35905], [177 ^ [], 178 ^ []]]))).
% 0.27/1.36 ncf('1.1.1.1',plain,[unorthogonal_lines(178 ^ [], 177 ^ [])],extension(182 ^ 3)).
% 0.27/1.36 ncf('1.1.2',plain,[convergent_lines(177 ^ [], 178 ^ []), unorthogonal_lines(177 ^ [], 178 ^ []), 148 : -(convergent_lines(177 ^ [], 177 ^ [])), 154 : -(unorthogonal_lines(178 ^ [], 177 ^ []))],extension(138 ^ 2,bind([[_36128, _36130, _36132], [177 ^ [], 178 ^ [], 177 ^ []]]))).
% 0.27/1.36 ncf('1.1.2.1',plain,[-(unorthogonal_lines(177 ^ [], 178 ^ []))],extension(180 ^ 3)).
% 0.27/1.36 ncf('1.1.2.2',plain,[convergent_lines(177 ^ [], 177 ^ [])],extension(6 ^ 5,bind([[_31721], [177 ^ []]]))).
% 0.27/1.36 ncf('1.1.2.3',plain,[unorthogonal_lines(178 ^ [], 177 ^ [])],extension(182 ^ 5)).
% 0.27/1.36 %-----------------------------------------------------
% 0.27/1.36 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------