%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO199+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n009.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:10 EDT 2023
% Result : Theorem 0.36s 1.39s
% Output : Proof 0.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO199+1 : TPTP v8.1.2. Released v3.3.0.
% 0.07/0.13 % Command : nanocop.sh %s %d
% 0.14/0.34 % Computer : n009.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Fri May 19 04:09:02 EDT 2023
% 0.14/0.34 % CPUTime :
% 0.36/1.39
% 0.36/1.39 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.36/1.39 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.36/1.39 %-----------------------------------------------------
% 0.36/1.39 ncf(matrix, plain, [(117 ^ _23293) ^ [] : [-(convergent_lines(113 ^ [], 114 ^ []))], (119 ^ _23293) ^ [] : [-(convergent_lines(115 ^ [], 114 ^ []))], (121 ^ _23293) ^ [] : [-(convergent_lines(113 ^ [], 115 ^ []))], (123 ^ _23293) ^ [] : [apart_point_and_line(intersection_point(113 ^ [], 114 ^ []), 115 ^ [])], (125 ^ _23293) ^ [] : [-(apart_point_and_line(intersection_point(114 ^ [], 113 ^ []), 115 ^ []))], (2 ^ _23293) ^ [_23376] : [distinct_points(_23376, _23376)], (4 ^ _23293) ^ [_23453] : [distinct_lines(_23453, _23453)], (6 ^ _23293) ^ [_23530] : [convergent_lines(_23530, _23530)], (8 ^ _23293) ^ [_23651, _23653, _23655] : [distinct_points(_23655, _23653), -(distinct_points(_23655, _23651)), -(distinct_points(_23653, _23651))], (18 ^ _23293) ^ [_23975, _23977, _23979] : [distinct_lines(_23979, _23977), -(distinct_lines(_23979, _23975)), -(distinct_lines(_23977, _23975))], (28 ^ _23293) ^ [_24299, _24301, _24303] : [convergent_lines(_24303, _24301), -(convergent_lines(_24303, _24299)), -(convergent_lines(_24301, _24299))], (38 ^ _23293) ^ [_24609, _24611] : [distinct_points(_24611, _24609), apart_point_and_line(_24611, line_connecting(_24611, _24609))], (44 ^ _23293) ^ [_24826, _24828] : [distinct_points(_24828, _24826), apart_point_and_line(_24826, line_connecting(_24828, _24826))], (50 ^ _23293) ^ [_25043, _25045] : [convergent_lines(_25045, _25043), apart_point_and_line(intersection_point(_25045, _25043), _25045)], (56 ^ _23293) ^ [_25260, _25262] : [convergent_lines(_25262, _25260), apart_point_and_line(intersection_point(_25262, _25260), _25260)], (62 ^ _23293) ^ [_25505, _25507, _25509, _25511] : [distinct_points(_25511, _25509), distinct_lines(_25507, _25505), -(apart_point_and_line(_25511, _25507)), -(apart_point_and_line(_25511, _25505)), -(apart_point_and_line(_25509, _25507)), -(apart_point_and_line(_25509, _25505))], (84 ^ _23293) ^ [_26134, _26136, _26138] : [apart_point_and_line(_26138, _26136), -(distinct_points(_26138, _26134)), -(apart_point_and_line(_26134, _26136))], (94 ^ _23293) ^ [_26458, _26460, _26462] : [apart_point_and_line(_26462, _26460), -(distinct_lines(_26460, _26458)), -(apart_point_and_line(_26462, _26458))], (104 ^ _23293) ^ [_26762, _26764, _26766] : [convergent_lines(_26766, _26764), -(distinct_lines(_26764, _26762)), -(convergent_lines(_26766, _26762))]], input).
% 0.36/1.39 ncf('1',plain,[convergent_lines(113 ^ [], 113 ^ [])],start(6 ^ 0,bind([[_23530], [113 ^ []]]))).
% 0.36/1.39 ncf('1.1',plain,[-(convergent_lines(113 ^ [], 113 ^ [])), convergent_lines(113 ^ [], 114 ^ []), -(convergent_lines(114 ^ [], 113 ^ []))],extension(28 ^ 1,bind([[_24299, _24301, _24303], [113 ^ [], 114 ^ [], 113 ^ []]]))).
% 0.36/1.39 ncf('1.1.1',plain,[-(convergent_lines(113 ^ [], 114 ^ []))],extension(117 ^ 2)).
% 0.36/1.39 ncf('1.1.2',plain,[convergent_lines(114 ^ [], 113 ^ []), apart_point_and_line(intersection_point(114 ^ [], 113 ^ []), 114 ^ [])],extension(50 ^ 2,bind([[_25043, _25045], [113 ^ [], 114 ^ []]]))).
% 0.36/1.39 ncf('1.1.2.1',plain,[-(apart_point_and_line(intersection_point(114 ^ [], 113 ^ []), 114 ^ [])), distinct_points(intersection_point(114 ^ [], 113 ^ []), intersection_point(113 ^ [], 114 ^ [])), distinct_lines(114 ^ [], 113 ^ []), -(apart_point_and_line(intersection_point(114 ^ [], 113 ^ []), 113 ^ [])), -(apart_point_and_line(intersection_point(113 ^ [], 114 ^ []), 114 ^ [])), -(apart_point_and_line(intersection_point(113 ^ [], 114 ^ []), 113 ^ []))],extension(62 ^ 3,bind([[_25505, _25507, _25509, _25511], [113 ^ [], 114 ^ [], intersection_point(113 ^ [], 114 ^ []), intersection_point(114 ^ [], 113 ^ [])]]))).
% 0.36/1.39 ncf('1.1.2.1.1',plain,[-(distinct_points(intersection_point(114 ^ [], 113 ^ []), intersection_point(113 ^ [], 114 ^ []))), apart_point_and_line(intersection_point(114 ^ [], 113 ^ []), 115 ^ []), -(apart_point_and_line(intersection_point(113 ^ [], 114 ^ []), 115 ^ []))],extension(84 ^ 4,bind([[_26134, _26136, _26138], [intersection_point(113 ^ [], 114 ^ []), 115 ^ [], intersection_point(114 ^ [], 113 ^ [])]]))).
% 0.36/1.39 ncf('1.1.2.1.1.1',plain,[-(apart_point_and_line(intersection_point(114 ^ [], 113 ^ []), 115 ^ []))],extension(125 ^ 5)).
% 0.36/1.39 ncf('1.1.2.1.1.2',plain,[apart_point_and_line(intersection_point(113 ^ [], 114 ^ []), 115 ^ [])],extension(123 ^ 5)).
% 0.36/1.39 ncf('1.1.2.1.2',plain,[-(distinct_lines(114 ^ [], 113 ^ [])), convergent_lines(113 ^ [], 114 ^ []), -(convergent_lines(113 ^ [], 113 ^ []))],extension(104 ^ 4,bind([[_26762, _26764, _26766], [113 ^ [], 114 ^ [], 113 ^ []]]))).
% 0.36/1.39 ncf('1.1.2.1.2.1',plain,[-(convergent_lines(113 ^ [], 114 ^ []))],extension(117 ^ 5)).
% 0.36/1.39 ncf('1.1.2.1.2.2',plain,[convergent_lines(113 ^ [], 113 ^ [])],reduction('1')).
% 0.36/1.39 ncf('1.1.2.1.3',plain,[apart_point_and_line(intersection_point(114 ^ [], 113 ^ []), 113 ^ []), convergent_lines(114 ^ [], 113 ^ [])],extension(56 ^ 4,bind([[_25260, _25262], [113 ^ [], 114 ^ []]]))).
% 0.36/1.39 ncf('1.1.2.1.3.1',plain,[-(convergent_lines(114 ^ [], 113 ^ []))],reduction('1.1')).
% 0.36/1.39 ncf('1.1.2.1.4',plain,[apart_point_and_line(intersection_point(113 ^ [], 114 ^ []), 114 ^ []), convergent_lines(113 ^ [], 114 ^ [])],extension(56 ^ 4,bind([[_25260, _25262], [114 ^ [], 113 ^ []]]))).
% 0.36/1.39 ncf('1.1.2.1.4.1',plain,[-(convergent_lines(113 ^ [], 114 ^ []))],lemmata('[1].x')).
% 0.36/1.39 ncf('1.1.2.1.5',plain,[apart_point_and_line(intersection_point(113 ^ [], 114 ^ []), 113 ^ []), convergent_lines(113 ^ [], 114 ^ [])],extension(50 ^ 4,bind([[_25043, _25045], [114 ^ [], 113 ^ []]]))).
% 0.36/1.39 ncf('1.1.2.1.5.1',plain,[-(convergent_lines(113 ^ [], 114 ^ []))],lemmata('[1].x')).
% 0.36/1.39 %-----------------------------------------------------
% 0.36/1.39 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------