%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO225+2 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n028.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:17 EDT 2023
% Result : Theorem 0.32s 1.38s
% Output : Proof 0.32s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO225+2 : TPTP v8.1.2. Released v3.3.0.
% 0.07/0.13 % Command : nanocop.sh %s %d
% 0.13/0.33 % Computer : n028.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Fri May 19 04:19:19 EDT 2023
% 0.13/0.34 % CPUTime :
% 0.32/1.38
% 0.32/1.38 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.32/1.38 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.32/1.38 %-----------------------------------------------------
% 0.32/1.38 ncf(matrix, plain, [(160 ^ _26722) ^ [] : [-(point(157 ^ []))], (162 ^ _26722) ^ [] : [-(point(158 ^ []))], (164 ^ _26722) ^ [] : [-(distinct_points(157 ^ [], 158 ^ []))], (166 ^ _26722) ^ [_32023] : [-(line(_32023))], (168 ^ _26722) ^ [_32081] : [-(apart_point_and_line(157 ^ [], _32081)), -(apart_point_and_line(158 ^ [], _32081))], (110 ^ _26722) ^ [_30372, _30374] : [-(line(line_connecting(_30374, _30372))), point(_30374), point(_30372), distinct_points(_30374, _30372)], (124 ^ _26722) ^ [_30760, _30762] : [-(point(intersection_point(_30762, _30760))), line(_30762), line(_30760), convergent_lines(_30762, _30760)], (138 ^ _26722) ^ [_31148, _31150] : [-(line(parallel_through_point(_31150, _31148))), line(_31150), point(_31148)], (148 ^ _26722) ^ [_31427, _31429] : [-(line(orthogonal_through_point(_31429, _31427))), line(_31429), point(_31427)], (2 ^ _26722) ^ [_26825] : [distinct_points(_26825, _26825)], (4 ^ _26722) ^ [_26902] : [distinct_lines(_26902, _26902)], (6 ^ _26722) ^ [_26979] : [convergent_lines(_26979, _26979)], (8 ^ _26722) ^ [_27100, _27102, _27104] : [distinct_points(_27104, _27102), -(distinct_points(_27104, _27100)), -(distinct_points(_27102, _27100))], (18 ^ _26722) ^ [_27424, _27426, _27428] : [distinct_lines(_27428, _27426), -(distinct_lines(_27428, _27424)), -(distinct_lines(_27426, _27424))], (28 ^ _26722) ^ [_27748, _27750, _27752] : [convergent_lines(_27752, _27750), -(convergent_lines(_27752, _27748)), -(convergent_lines(_27750, _27748))], (38 ^ _26722) ^ [_28072, _28074, _28076] : [distinct_points(_28076, _28074), apart_point_and_line(_28072, line_connecting(_28076, _28074)), 45 ^ _26722 : [(46 ^ _26722) ^ [] : [-(distinct_points(_28072, _28076))], (48 ^ _26722) ^ [] : [-(distinct_points(_28072, _28074))]]], (50 ^ _26722) ^ [_28478, _28480, _28482] : [convergent_lines(_28482, _28480), 55 ^ _26722 : [(56 ^ _26722) ^ [] : [apart_point_and_line(_28478, _28482)], (58 ^ _26722) ^ [] : [apart_point_and_line(_28478, _28480)]], -(distinct_points(_28478, intersection_point(_28482, _28480)))], (62 ^ _26722) ^ [_28897, _28899, _28901, _28903] : [distinct_points(_28903, _28901), distinct_lines(_28899, _28897), -(apart_point_and_line(_28903, _28899)), -(apart_point_and_line(_28903, _28897)), -(apart_point_and_line(_28901, _28899)), -(apart_point_and_line(_28901, _28897))], (84 ^ _26722) ^ [_29526, _29528, _29530] : [apart_point_and_line(_29530, _29528), -(distinct_points(_29530, _29526)), -(apart_point_and_line(_29526, _29528))], (104 ^ _26722) ^ [_30140, _30142] : [convergent_lines(_30142, _30140), -(distinct_lines(_30142, _30140))], (94 ^ _26722) ^ [_29850, _29852, _29854] : [apart_point_and_line(_29854, _29852), -(distinct_lines(_29852, _29850)), -(apart_point_and_line(_29854, _29850))]], input).
% 0.32/1.38 ncf('1',plain,[distinct_points(157 ^ [], 157 ^ [])],start(2 ^ 0,bind([[_26825], [157 ^ []]]))).
% 0.32/1.38 ncf('1.1',plain,[-(distinct_points(157 ^ [], 157 ^ [])), distinct_points(157 ^ [], 158 ^ []), -(distinct_points(158 ^ [], 157 ^ []))],extension(8 ^ 1,bind([[_27100, _27102, _27104], [157 ^ [], 158 ^ [], 157 ^ []]]))).
% 0.32/1.38 ncf('1.1.1',plain,[-(distinct_points(157 ^ [], 158 ^ []))],extension(164 ^ 2)).
% 0.32/1.38 ncf('1.1.2',plain,[distinct_points(158 ^ [], 157 ^ []), apart_point_and_line(158 ^ [], line_connecting(158 ^ [], 157 ^ [])), 46 : -(distinct_points(158 ^ [], 158 ^ []))],extension(38 ^ 2,bind([[_28072, _28074, _28076], [158 ^ [], 157 ^ [], 158 ^ []]]))).
% 0.32/1.38 ncf('1.1.2.1',plain,[-(apart_point_and_line(158 ^ [], line_connecting(158 ^ [], 157 ^ []))), -(apart_point_and_line(157 ^ [], line_connecting(158 ^ [], 157 ^ [])))],extension(168 ^ 3,bind([[_32081], [line_connecting(158 ^ [], 157 ^ [])]]))).
% 0.32/1.38 ncf('1.1.2.1.1',plain,[apart_point_and_line(157 ^ [], line_connecting(158 ^ [], 157 ^ [])), distinct_points(158 ^ [], 157 ^ []), 48 : -(distinct_points(157 ^ [], 157 ^ []))],extension(38 ^ 4,bind([[_28072, _28074, _28076], [157 ^ [], 157 ^ [], 158 ^ []]]))).
% 0.32/1.38 ncf('1.1.2.1.1.1',plain,[-(distinct_points(158 ^ [], 157 ^ []))],reduction('1.1')).
% 0.32/1.38 ncf('1.1.2.1.1.2',plain,[distinct_points(157 ^ [], 157 ^ [])],reduction('1')).
% 0.32/1.38 ncf('1.1.2.2',plain,[distinct_points(158 ^ [], 158 ^ [])],extension(2 ^ 5,bind([[_26825], [158 ^ []]]))).
% 0.32/1.38 %-----------------------------------------------------
% 0.32/1.38 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------