%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO170+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n017.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:02 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.11/0.12 % Problem : GEO170+1 : TPTP v8.1.2. Released v3.3.0.
% 0.11/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n017.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 03:49:31 EDT 2023
% 0.12/0.33 % 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, [(117 ^ _21959) ^ [] : [-(distinct_points(113 ^ [], 114 ^ []))], (119 ^ _21959) ^ [] : [apart_point_and_line(113 ^ [], 115 ^ [])], (121 ^ _21959) ^ [] : [apart_point_and_line(114 ^ [], 115 ^ [])], (123 ^ _21959) ^ [] : [-(distinct_lines(115 ^ [], line_connecting(113 ^ [], 114 ^ [])))], (2 ^ _21959) ^ [_22042] : [distinct_points(_22042, _22042)], (4 ^ _21959) ^ [_22119] : [distinct_lines(_22119, _22119)], (6 ^ _21959) ^ [_22196] : [convergent_lines(_22196, _22196)], (8 ^ _21959) ^ [_22317, _22319, _22321] : [distinct_points(_22321, _22319), -(distinct_points(_22321, _22317)), -(distinct_points(_22319, _22317))], (18 ^ _21959) ^ [_22641, _22643, _22645] : [distinct_lines(_22645, _22643), -(distinct_lines(_22645, _22641)), -(distinct_lines(_22643, _22641))], (28 ^ _21959) ^ [_22965, _22967, _22969] : [convergent_lines(_22969, _22967), -(convergent_lines(_22969, _22965)), -(convergent_lines(_22967, _22965))], (38 ^ _21959) ^ [_23275, _23277] : [distinct_points(_23277, _23275), apart_point_and_line(_23277, line_connecting(_23277, _23275))], (44 ^ _21959) ^ [_23492, _23494] : [distinct_points(_23494, _23492), apart_point_and_line(_23492, line_connecting(_23494, _23492))], (50 ^ _21959) ^ [_23709, _23711] : [convergent_lines(_23711, _23709), apart_point_and_line(intersection_point(_23711, _23709), _23711)], (56 ^ _21959) ^ [_23926, _23928] : [convergent_lines(_23928, _23926), apart_point_and_line(intersection_point(_23928, _23926), _23926)], (62 ^ _21959) ^ [_24171, _24173, _24175, _24177] : [distinct_points(_24177, _24175), distinct_lines(_24173, _24171), -(apart_point_and_line(_24177, _24173)), -(apart_point_and_line(_24177, _24171)), -(apart_point_and_line(_24175, _24173)), -(apart_point_and_line(_24175, _24171))], (84 ^ _21959) ^ [_24800, _24802, _24804] : [apart_point_and_line(_24804, _24802), -(distinct_points(_24804, _24800)), -(apart_point_and_line(_24800, _24802))], (94 ^ _21959) ^ [_25124, _25126, _25128] : [apart_point_and_line(_25128, _25126), -(distinct_lines(_25126, _25124)), -(apart_point_and_line(_25128, _25124))], (104 ^ _21959) ^ [_25428, _25430, _25432] : [convergent_lines(_25432, _25430), -(distinct_lines(_25430, _25428)), -(convergent_lines(_25432, _25428))]], input).
% 0.32/1.38 ncf('1',plain,[apart_point_and_line(113 ^ [], 115 ^ [])],start(119 ^ 0)).
% 0.32/1.38 ncf('1.1',plain,[-(apart_point_and_line(113 ^ [], 115 ^ [])), distinct_points(113 ^ [], 114 ^ []), distinct_lines(115 ^ [], line_connecting(113 ^ [], 114 ^ [])), -(apart_point_and_line(113 ^ [], line_connecting(113 ^ [], 114 ^ []))), -(apart_point_and_line(114 ^ [], 115 ^ [])), -(apart_point_and_line(114 ^ [], line_connecting(113 ^ [], 114 ^ [])))],extension(62 ^ 1,bind([[_24171, _24173, _24175, _24177], [line_connecting(113 ^ [], 114 ^ []), 115 ^ [], 114 ^ [], 113 ^ []]]))).
% 0.32/1.38 ncf('1.1.1',plain,[-(distinct_points(113 ^ [], 114 ^ []))],extension(117 ^ 2)).
% 0.32/1.38 ncf('1.1.2',plain,[-(distinct_lines(115 ^ [], line_connecting(113 ^ [], 114 ^ [])))],extension(123 ^ 2)).
% 0.32/1.38 ncf('1.1.3',plain,[apart_point_and_line(113 ^ [], line_connecting(113 ^ [], 114 ^ [])), distinct_points(113 ^ [], 114 ^ [])],extension(38 ^ 2,bind([[_23275, _23277], [114 ^ [], 113 ^ []]]))).
% 0.32/1.38 ncf('1.1.3.1',plain,[-(distinct_points(113 ^ [], 114 ^ []))],lemmata('[1].x')).
% 0.32/1.38 ncf('1.1.4',plain,[apart_point_and_line(114 ^ [], 115 ^ [])],extension(121 ^ 2)).
% 0.32/1.38 ncf('1.1.5',plain,[apart_point_and_line(114 ^ [], line_connecting(113 ^ [], 114 ^ [])), distinct_points(113 ^ [], 114 ^ [])],extension(44 ^ 2,bind([[_23492, _23494], [114 ^ [], 113 ^ []]]))).
% 0.32/1.38 ncf('1.1.5.1',plain,[-(distinct_points(113 ^ [], 114 ^ []))],lemmata('[1].x')).
% 0.32/1.38 %-----------------------------------------------------
% 0.32/1.38 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------