%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO215+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n013.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.34s 1.38s
% Output : Proof 0.34s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GEO215+1 : TPTP v8.1.2. Released v3.3.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n013.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:06:05 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.34/1.38
% 0.34/1.38 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.34/1.38 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.34/1.38 %-----------------------------------------------------
% 0.34/1.38 ncf(matrix, plain, [(181 ^ _32427) ^ [] : [-(convergent_lines(177 ^ [], 178 ^ []))], (183 ^ _32427) ^ [] : [unorthogonal_lines(177 ^ [], 179 ^ [])], (185 ^ _32427) ^ [] : [unorthogonal_lines(178 ^ [], 179 ^ [])], (114 ^ _32427) ^ [_36256, _36258] : [convergent_lines(parallel_through_point(_36256, _36258), _36256)], (116 ^ _32427) ^ [_36352, _36354] : [apart_point_and_line(_36354, parallel_through_point(_36352, _36354))], (118 ^ _32427) ^ [_36458, _36460, _36462] : [distinct_lines(_36460, _36458), -(apart_point_and_line(_36462, _36460)), -(apart_point_and_line(_36462, _36458)), -(convergent_lines(_36460, _36458))], (132 ^ _32427) ^ [_36866, _36868] : [-(convergent_lines(_36868, _36866)), -(unorthogonal_lines(_36868, _36866))], (138 ^ _32427) ^ [_37091, _37093, _37095] : [convergent_lines(_37095, _37093), unorthogonal_lines(_37095, _37093), 147 ^ _32427 : [(148 ^ _32427) ^ [] : [-(convergent_lines(_37095, _37091))], (150 ^ _32427) ^ [] : [-(unorthogonal_lines(_37095, _37091))]], 151 ^ _32427 : [(152 ^ _32427) ^ [] : [-(convergent_lines(_37093, _37091))], (154 ^ _32427) ^ [] : [-(unorthogonal_lines(_37093, _37091))]]], (156 ^ _32427) ^ [_37634, _37636] : [unorthogonal_lines(orthogonal_through_point(_37634, _37636), _37634)], (158 ^ _32427) ^ [_37730, _37732] : [apart_point_and_line(_37732, orthogonal_through_point(_37730, _37732))], (160 ^ _32427) ^ [_37850, _37852, _37854, _37856] : [distinct_lines(_37854, _37852), -(apart_point_and_line(_37856, _37854)), -(apart_point_and_line(_37856, _37852)), -(unorthogonal_lines(_37854, _37850)), -(unorthogonal_lines(_37852, _37850))], (2 ^ _32427) ^ [_32530] : [distinct_points(_32530, _32530)], (4 ^ _32427) ^ [_32607] : [distinct_lines(_32607, _32607)], (6 ^ _32427) ^ [_32684] : [convergent_lines(_32684, _32684)], (8 ^ _32427) ^ [_32805, _32807, _32809] : [distinct_points(_32809, _32807), -(distinct_points(_32809, _32805)), -(distinct_points(_32807, _32805))], (18 ^ _32427) ^ [_33129, _33131, _33133] : [distinct_lines(_33133, _33131), -(distinct_lines(_33133, _33129)), -(distinct_lines(_33131, _33129))], (28 ^ _32427) ^ [_33453, _33455, _33457] : [convergent_lines(_33457, _33455), -(convergent_lines(_33457, _33453)), -(convergent_lines(_33455, _33453))], (38 ^ _32427) ^ [_33763, _33765] : [distinct_points(_33765, _33763), apart_point_and_line(_33765, line_connecting(_33765, _33763))], (44 ^ _32427) ^ [_33980, _33982] : [distinct_points(_33982, _33980), apart_point_and_line(_33980, line_connecting(_33982, _33980))], (50 ^ _32427) ^ [_34197, _34199] : [convergent_lines(_34199, _34197), apart_point_and_line(intersection_point(_34199, _34197), _34199)], (56 ^ _32427) ^ [_34414, _34416] : [convergent_lines(_34416, _34414), apart_point_and_line(intersection_point(_34416, _34414), _34414)], (62 ^ _32427) ^ [_34659, _34661, _34663, _34665] : [distinct_points(_34665, _34663), distinct_lines(_34661, _34659), -(apart_point_and_line(_34665, _34661)), -(apart_point_and_line(_34665, _34659)), -(apart_point_and_line(_34663, _34661)), -(apart_point_and_line(_34663, _34659))], (84 ^ _32427) ^ [_35288, _35290, _35292] : [apart_point_and_line(_35292, _35290), -(distinct_points(_35292, _35288)), -(apart_point_and_line(_35288, _35290))], (94 ^ _32427) ^ [_35612, _35614, _35616] : [apart_point_and_line(_35616, _35614), -(distinct_lines(_35614, _35612)), -(apart_point_and_line(_35616, _35612))], (104 ^ _32427) ^ [_35916, _35918, _35920] : [convergent_lines(_35920, _35918), -(distinct_lines(_35918, _35916)), -(convergent_lines(_35920, _35916))]], input).
% 0.34/1.38 ncf('1',plain,[distinct_lines(178 ^ [], 178 ^ [])],start(4 ^ 0,bind([[_32607], [178 ^ []]]))).
% 0.34/1.38 ncf('1.1',plain,[-(distinct_lines(178 ^ [], 178 ^ [])), distinct_lines(178 ^ [], 177 ^ []), -(distinct_lines(177 ^ [], 178 ^ []))],extension(18 ^ 1,bind([[_33129, _33131, _33133], [178 ^ [], 177 ^ [], 178 ^ []]]))).
% 0.34/1.38 ncf('1.1.1',plain,[-(distinct_lines(178 ^ [], 177 ^ [])), convergent_lines(177 ^ [], 178 ^ []), -(convergent_lines(177 ^ [], 177 ^ []))],extension(104 ^ 2,bind([[_35916, _35918, _35920], [177 ^ [], 178 ^ [], 177 ^ []]]))).
% 0.34/1.38 ncf('1.1.1.1',plain,[-(convergent_lines(177 ^ [], 178 ^ []))],extension(181 ^ 3)).
% 0.34/1.38 ncf('1.1.1.2',plain,[convergent_lines(177 ^ [], 177 ^ [])],extension(6 ^ 3,bind([[_32684], [177 ^ []]]))).
% 0.34/1.38 ncf('1.1.2',plain,[distinct_lines(177 ^ [], 178 ^ []), -(apart_point_and_line(intersection_point(177 ^ [], 178 ^ []), 177 ^ [])), -(apart_point_and_line(intersection_point(177 ^ [], 178 ^ []), 178 ^ [])), -(unorthogonal_lines(177 ^ [], 179 ^ [])), -(unorthogonal_lines(178 ^ [], 179 ^ []))],extension(160 ^ 2,bind([[_37850, _37852, _37854, _37856], [179 ^ [], 178 ^ [], 177 ^ [], intersection_point(177 ^ [], 178 ^ [])]]))).
% 0.34/1.38 ncf('1.1.2.1',plain,[apart_point_and_line(intersection_point(177 ^ [], 178 ^ []), 177 ^ []), convergent_lines(177 ^ [], 178 ^ [])],extension(50 ^ 3,bind([[_34197, _34199], [178 ^ [], 177 ^ []]]))).
% 0.34/1.38 ncf('1.1.2.1.1',plain,[-(convergent_lines(177 ^ [], 178 ^ []))],extension(181 ^ 4)).
% 0.34/1.38 ncf('1.1.2.2',plain,[apart_point_and_line(intersection_point(177 ^ [], 178 ^ []), 178 ^ []), convergent_lines(177 ^ [], 178 ^ [])],extension(56 ^ 3,bind([[_34414, _34416], [178 ^ [], 177 ^ []]]))).
% 0.34/1.38 ncf('1.1.2.2.1',plain,[-(convergent_lines(177 ^ [], 178 ^ []))],extension(181 ^ 4)).
% 0.34/1.38 ncf('1.1.2.3',plain,[unorthogonal_lines(177 ^ [], 179 ^ [])],extension(183 ^ 3)).
% 0.34/1.38 ncf('1.1.2.4',plain,[unorthogonal_lines(178 ^ [], 179 ^ [])],extension(185 ^ 3)).
% 0.34/1.38 %-----------------------------------------------------
% 0.34/1.38 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------