%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO184+2 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n018.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 0.33s 1.36s
% Output : Proof 0.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GEO184+2 : TPTP v8.1.2. Released v3.3.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.13/0.32 % Computer : n018.cluster.edu
% 0.13/0.32 % Model : x86_64 x86_64
% 0.13/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.32 % Memory : 8042.1875MB
% 0.13/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.32 % CPULimit : 300
% 0.13/0.32 % WCLimit : 300
% 0.13/0.32 % DateTime : Fri May 19 04:14:28 EDT 2023
% 0.13/0.32 % CPUTime :
% 0.33/1.36
% 0.33/1.36 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.33/1.36 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.33/1.36 %-----------------------------------------------------
% 0.33/1.36 ncf(matrix, plain, [(114 ^ _21874) ^ [] : [-(distinct_points(109 ^ [], 110 ^ []))], (116 ^ _21874) ^ [] : [-(convergent_lines(111 ^ [], 112 ^ []))], (118 ^ _21874) ^ [] : [apart_point_and_line(109 ^ [], 111 ^ [])], (120 ^ _21874) ^ [] : [apart_point_and_line(110 ^ [], 111 ^ [])], (122 ^ _21874) ^ [] : [-(distinct_lines(111 ^ [], line_connecting(109 ^ [], 110 ^ [])))], (2 ^ _21874) ^ [_21957] : [distinct_points(_21957, _21957)], (4 ^ _21874) ^ [_22034] : [distinct_lines(_22034, _22034)], (6 ^ _21874) ^ [_22111] : [convergent_lines(_22111, _22111)], (8 ^ _21874) ^ [_22232, _22234, _22236] : [distinct_points(_22236, _22234), -(distinct_points(_22236, _22232)), -(distinct_points(_22234, _22232))], (18 ^ _21874) ^ [_22556, _22558, _22560] : [distinct_lines(_22560, _22558), -(distinct_lines(_22560, _22556)), -(distinct_lines(_22558, _22556))], (28 ^ _21874) ^ [_22880, _22882, _22884] : [convergent_lines(_22884, _22882), -(convergent_lines(_22884, _22880)), -(convergent_lines(_22882, _22880))], (38 ^ _21874) ^ [_23204, _23206, _23208] : [distinct_points(_23208, _23206), apart_point_and_line(_23204, line_connecting(_23208, _23206)), 45 ^ _21874 : [(46 ^ _21874) ^ [] : [-(distinct_points(_23204, _23208))], (48 ^ _21874) ^ [] : [-(distinct_points(_23204, _23206))]]], (50 ^ _21874) ^ [_23610, _23612, _23614] : [convergent_lines(_23614, _23612), 55 ^ _21874 : [(56 ^ _21874) ^ [] : [apart_point_and_line(_23610, _23614)], (58 ^ _21874) ^ [] : [apart_point_and_line(_23610, _23612)]], -(distinct_points(_23610, intersection_point(_23614, _23612)))], (62 ^ _21874) ^ [_24029, _24031, _24033, _24035] : [distinct_points(_24035, _24033), distinct_lines(_24031, _24029), -(apart_point_and_line(_24035, _24031)), -(apart_point_and_line(_24035, _24029)), -(apart_point_and_line(_24033, _24031)), -(apart_point_and_line(_24033, _24029))], (84 ^ _21874) ^ [_24658, _24660, _24662] : [apart_point_and_line(_24662, _24660), -(distinct_points(_24662, _24658)), -(apart_point_and_line(_24658, _24660))], (104 ^ _21874) ^ [_25272, _25274] : [convergent_lines(_25274, _25272), -(distinct_lines(_25274, _25272))], (94 ^ _21874) ^ [_24982, _24984, _24986] : [apart_point_and_line(_24986, _24984), -(distinct_lines(_24984, _24982)), -(apart_point_and_line(_24986, _24982))]], input).
% 0.33/1.36 ncf('1',plain,[apart_point_and_line(109 ^ [], 111 ^ [])],start(118 ^ 0)).
% 0.33/1.36 ncf('1.1',plain,[-(apart_point_and_line(109 ^ [], 111 ^ [])), distinct_points(109 ^ [], 110 ^ []), distinct_lines(111 ^ [], line_connecting(109 ^ [], 110 ^ [])), -(apart_point_and_line(109 ^ [], line_connecting(109 ^ [], 110 ^ []))), -(apart_point_and_line(110 ^ [], 111 ^ [])), -(apart_point_and_line(110 ^ [], line_connecting(109 ^ [], 110 ^ [])))],extension(62 ^ 1,bind([[_24029, _24031, _24033, _24035], [line_connecting(109 ^ [], 110 ^ []), 111 ^ [], 110 ^ [], 109 ^ []]]))).
% 0.33/1.36 ncf('1.1.1',plain,[-(distinct_points(109 ^ [], 110 ^ []))],extension(114 ^ 2)).
% 0.33/1.36 ncf('1.1.2',plain,[-(distinct_lines(111 ^ [], line_connecting(109 ^ [], 110 ^ [])))],extension(122 ^ 2)).
% 0.33/1.36 ncf('1.1.3',plain,[apart_point_and_line(109 ^ [], line_connecting(109 ^ [], 110 ^ [])), distinct_points(109 ^ [], 110 ^ []), 46 : -(distinct_points(109 ^ [], 109 ^ []))],extension(38 ^ 2,bind([[_23204, _23206, _23208], [109 ^ [], 110 ^ [], 109 ^ []]]))).
% 0.33/1.36 ncf('1.1.3.1',plain,[-(distinct_points(109 ^ [], 110 ^ []))],lemmata('[1].x')).
% 0.33/1.36 ncf('1.1.3.2',plain,[distinct_points(109 ^ [], 109 ^ [])],extension(2 ^ 5,bind([[_21957], [109 ^ []]]))).
% 0.33/1.36 ncf('1.1.4',plain,[apart_point_and_line(110 ^ [], 111 ^ [])],extension(120 ^ 2)).
% 0.33/1.36 ncf('1.1.5',plain,[apart_point_and_line(110 ^ [], line_connecting(109 ^ [], 110 ^ [])), distinct_points(109 ^ [], 110 ^ []), 48 : -(distinct_points(110 ^ [], 110 ^ []))],extension(38 ^ 2,bind([[_23204, _23206, _23208], [110 ^ [], 110 ^ [], 109 ^ []]]))).
% 0.33/1.36 ncf('1.1.5.1',plain,[-(distinct_points(109 ^ [], 110 ^ []))],lemmata('[1].x')).
% 0.33/1.36 ncf('1.1.5.2',plain,[distinct_points(110 ^ [], 110 ^ [])],extension(2 ^ 5,bind([[_21957], [110 ^ []]]))).
% 0.33/1.36 %-----------------------------------------------------
% 0.33/1.36 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------