%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO189+2 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n024.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:07 EDT 2023
% Result : Theorem 0.35s 1.38s
% Output : Proof 0.35s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GEO189+2 : TPTP v8.1.2. Released v3.3.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.13/0.33 % Computer : n024.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:23:51 EDT 2023
% 0.13/0.33 % CPUTime :
% 0.35/1.38
% 0.35/1.38 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.35/1.38 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.35/1.38 %-----------------------------------------------------
% 0.35/1.38 ncf(matrix, plain, [(113 ^ _23614) ^ [] : [-(distinct_points(109 ^ [], 110 ^ []))], (115 ^ _23614) ^ [] : [-(distinct_points(109 ^ [], 111 ^ []))], (117 ^ _23614) ^ [] : [-(distinct_points(110 ^ [], 111 ^ []))], (119 ^ _23614) ^ [] : [apart_point_and_line(111 ^ [], line_connecting(109 ^ [], 110 ^ []))], (121 ^ _23614) ^ [] : [-(apart_point_and_line(110 ^ [], line_connecting(109 ^ [], 111 ^ [])))], (2 ^ _23614) ^ [_23697] : [distinct_points(_23697, _23697)], (4 ^ _23614) ^ [_23774] : [distinct_lines(_23774, _23774)], (6 ^ _23614) ^ [_23851] : [convergent_lines(_23851, _23851)], (8 ^ _23614) ^ [_23972, _23974, _23976] : [distinct_points(_23976, _23974), -(distinct_points(_23976, _23972)), -(distinct_points(_23974, _23972))], (18 ^ _23614) ^ [_24296, _24298, _24300] : [distinct_lines(_24300, _24298), -(distinct_lines(_24300, _24296)), -(distinct_lines(_24298, _24296))], (28 ^ _23614) ^ [_24620, _24622, _24624] : [convergent_lines(_24624, _24622), -(convergent_lines(_24624, _24620)), -(convergent_lines(_24622, _24620))], (38 ^ _23614) ^ [_24944, _24946, _24948] : [distinct_points(_24948, _24946), apart_point_and_line(_24944, line_connecting(_24948, _24946)), 45 ^ _23614 : [(46 ^ _23614) ^ [] : [-(distinct_points(_24944, _24948))], (48 ^ _23614) ^ [] : [-(distinct_points(_24944, _24946))]]], (50 ^ _23614) ^ [_25350, _25352, _25354] : [convergent_lines(_25354, _25352), 55 ^ _23614 : [(56 ^ _23614) ^ [] : [apart_point_and_line(_25350, _25354)], (58 ^ _23614) ^ [] : [apart_point_and_line(_25350, _25352)]], -(distinct_points(_25350, intersection_point(_25354, _25352)))], (62 ^ _23614) ^ [_25769, _25771, _25773, _25775] : [distinct_points(_25775, _25773), distinct_lines(_25771, _25769), -(apart_point_and_line(_25775, _25771)), -(apart_point_and_line(_25775, _25769)), -(apart_point_and_line(_25773, _25771)), -(apart_point_and_line(_25773, _25769))], (84 ^ _23614) ^ [_26398, _26400, _26402] : [apart_point_and_line(_26402, _26400), -(distinct_points(_26402, _26398)), -(apart_point_and_line(_26398, _26400))], (104 ^ _23614) ^ [_27012, _27014] : [convergent_lines(_27014, _27012), -(distinct_lines(_27014, _27012))], (94 ^ _23614) ^ [_26722, _26724, _26726] : [apart_point_and_line(_26726, _26724), -(distinct_lines(_26724, _26722)), -(apart_point_and_line(_26726, _26722))]], input).
% 0.35/1.38 ncf('1',plain,[apart_point_and_line(111 ^ [], line_connecting(109 ^ [], 110 ^ []))],start(119 ^ 0)).
% 0.35/1.38 ncf('1.1',plain,[-(apart_point_and_line(111 ^ [], line_connecting(109 ^ [], 110 ^ []))), distinct_points(111 ^ [], 109 ^ []), distinct_lines(line_connecting(109 ^ [], 111 ^ []), line_connecting(109 ^ [], 110 ^ [])), -(apart_point_and_line(111 ^ [], line_connecting(109 ^ [], 111 ^ []))), -(apart_point_and_line(109 ^ [], line_connecting(109 ^ [], 111 ^ []))), -(apart_point_and_line(109 ^ [], line_connecting(109 ^ [], 110 ^ [])))],extension(62 ^ 1,bind([[_25769, _25771, _25773, _25775], [line_connecting(109 ^ [], 110 ^ []), line_connecting(109 ^ [], 111 ^ []), 109 ^ [], 111 ^ []]]))).
% 0.35/1.38 ncf('1.1.1',plain,[-(distinct_points(111 ^ [], 109 ^ [])), distinct_points(111 ^ [], 109 ^ []), -(distinct_points(109 ^ [], 109 ^ []))],extension(8 ^ 2,bind([[_23972, _23974, _23976], [109 ^ [], 109 ^ [], 111 ^ []]]))).
% 0.35/1.38 ncf('1.1.1.1',plain,[-(distinct_points(111 ^ [], 109 ^ [])), distinct_points(109 ^ [], 111 ^ []), -(distinct_points(109 ^ [], 109 ^ []))],extension(8 ^ 3,bind([[_23972, _23974, _23976], [109 ^ [], 111 ^ [], 109 ^ []]]))).
% 0.35/1.38 ncf('1.1.1.1.1',plain,[-(distinct_points(109 ^ [], 111 ^ []))],extension(115 ^ 4)).
% 0.35/1.38 ncf('1.1.1.1.2',plain,[distinct_points(109 ^ [], 109 ^ [])],extension(2 ^ 4,bind([[_23697], [109 ^ []]]))).
% 0.35/1.38 ncf('1.1.1.2',plain,[distinct_points(109 ^ [], 109 ^ [])],extension(2 ^ 3,bind([[_23697], [109 ^ []]]))).
% 0.35/1.38 ncf('1.1.2',plain,[-(distinct_lines(line_connecting(109 ^ [], 111 ^ []), line_connecting(109 ^ [], 110 ^ []))), apart_point_and_line(110 ^ [], line_connecting(109 ^ [], 111 ^ [])), -(apart_point_and_line(110 ^ [], line_connecting(109 ^ [], 110 ^ [])))],extension(94 ^ 2,bind([[_26722, _26724, _26726], [line_connecting(109 ^ [], 110 ^ []), line_connecting(109 ^ [], 111 ^ []), 110 ^ []]]))).
% 0.35/1.38 ncf('1.1.2.1',plain,[-(apart_point_and_line(110 ^ [], line_connecting(109 ^ [], 111 ^ [])))],extension(121 ^ 3)).
% 0.35/1.38 ncf('1.1.2.2',plain,[apart_point_and_line(110 ^ [], line_connecting(109 ^ [], 110 ^ [])), distinct_points(109 ^ [], 110 ^ []), 48 : -(distinct_points(110 ^ [], 110 ^ []))],extension(38 ^ 3,bind([[_24944, _24946, _24948], [110 ^ [], 110 ^ [], 109 ^ []]]))).
% 0.35/1.38 ncf('1.1.2.2.1',plain,[-(distinct_points(109 ^ [], 110 ^ []))],extension(113 ^ 4)).
% 0.35/1.38 ncf('1.1.2.2.2',plain,[distinct_points(110 ^ [], 110 ^ [])],extension(2 ^ 6,bind([[_23697], [110 ^ []]]))).
% 0.35/1.38 ncf('1.1.3',plain,[apart_point_and_line(111 ^ [], line_connecting(109 ^ [], 111 ^ [])), distinct_points(109 ^ [], 111 ^ []), 46 : -(distinct_points(111 ^ [], 109 ^ []))],extension(38 ^ 2,bind([[_24944, _24946, _24948], [111 ^ [], 111 ^ [], 109 ^ []]]))).
% 0.35/1.38 ncf('1.1.3.1',plain,[-(distinct_points(109 ^ [], 111 ^ []))],extension(115 ^ 3)).
% 0.35/1.38 ncf('1.1.3.2',plain,[distinct_points(111 ^ [], 109 ^ []), -(distinct_points(111 ^ [], 111 ^ [])), -(distinct_points(109 ^ [], 111 ^ []))],extension(8 ^ 5,bind([[_23972, _23974, _23976], [111 ^ [], 109 ^ [], 111 ^ []]]))).
% 0.35/1.38 ncf('1.1.3.2.1',plain,[distinct_points(111 ^ [], 111 ^ [])],extension(2 ^ 6,bind([[_23697], [111 ^ []]]))).
% 0.35/1.38 ncf('1.1.3.2.2',plain,[distinct_points(109 ^ [], 111 ^ []), apart_point_and_line(111 ^ [], line_connecting(109 ^ [], 111 ^ [])), 48 : -(distinct_points(111 ^ [], 111 ^ []))],extension(38 ^ 6,bind([[_24944, _24946, _24948], [111 ^ [], 111 ^ [], 109 ^ []]]))).
% 0.35/1.38 ncf('1.1.3.2.2.1',plain,[-(apart_point_and_line(111 ^ [], line_connecting(109 ^ [], 111 ^ [])))],reduction('1.1')).
% 0.35/1.38 ncf('1.1.3.2.2.2',plain,[distinct_points(111 ^ [], 111 ^ [])],lemmata('[3, 1, 1].x')).
% 0.35/1.38 ncf('1.1.4',plain,[apart_point_and_line(109 ^ [], line_connecting(109 ^ [], 111 ^ [])), distinct_points(109 ^ [], 111 ^ []), 46 : -(distinct_points(109 ^ [], 109 ^ []))],extension(38 ^ 2,bind([[_24944, _24946, _24948], [109 ^ [], 111 ^ [], 109 ^ []]]))).
% 0.35/1.38 ncf('1.1.4.1',plain,[-(distinct_points(109 ^ [], 111 ^ []))],extension(115 ^ 3)).
% 0.35/1.38 ncf('1.1.4.2',plain,[distinct_points(109 ^ [], 109 ^ [])],extension(2 ^ 5,bind([[_23697], [109 ^ []]]))).
% 0.35/1.38 ncf('1.1.5',plain,[apart_point_and_line(109 ^ [], line_connecting(109 ^ [], 110 ^ [])), distinct_points(109 ^ [], 110 ^ []), 46 : -(distinct_points(109 ^ [], 109 ^ []))],extension(38 ^ 2,bind([[_24944, _24946, _24948], [109 ^ [], 110 ^ [], 109 ^ []]]))).
% 0.35/1.38 ncf('1.1.5.1',plain,[-(distinct_points(109 ^ [], 110 ^ []))],extension(113 ^ 3)).
% 0.35/1.38 ncf('1.1.5.2',plain,[distinct_points(109 ^ [], 109 ^ [])],extension(2 ^ 5,bind([[_23697], [109 ^ []]]))).
% 0.35/1.38 %-----------------------------------------------------
% 0.35/1.38 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------