%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO206+2 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n002.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:12 EDT 2023
% Result : Theorem 0.35s 1.37s
% Output : Proof 0.35s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : GEO206+2 : TPTP v8.1.2. Released v3.3.0.
% 0.06/0.12 % Command : nanocop.sh %s %d
% 0.13/0.33 % Computer : n002.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:13:20 EDT 2023
% 0.13/0.33 % CPUTime :
% 0.35/1.37
% 0.35/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.35/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.35/1.37 %-----------------------------------------------------
% 0.35/1.37 ncf(matrix, plain, [(131 ^ _23787) ^ [] : [apart_point_and_line(127 ^ [], 128 ^ [])], (133 ^ _23787) ^ [] : [convergent_lines(128 ^ [], 129 ^ [])], (135 ^ _23787) ^ [] : [-(distinct_lines(128 ^ [], parallel_through_point(129 ^ [], 127 ^ [])))], (110 ^ _23787) ^ [_27421, _27423] : [convergent_lines(parallel_through_point(_27421, _27423), _27421)], (112 ^ _23787) ^ [_27517, _27519] : [apart_point_and_line(_27519, parallel_through_point(_27517, _27519))], (114 ^ _23787) ^ [_27623, _27625, _27627] : [distinct_lines(_27625, _27623), -(apart_point_and_line(_27627, _27625)), -(apart_point_and_line(_27627, _27623)), -(convergent_lines(_27625, _27623))], (2 ^ _23787) ^ [_23890] : [distinct_points(_23890, _23890)], (4 ^ _23787) ^ [_23967] : [distinct_lines(_23967, _23967)], (6 ^ _23787) ^ [_24044] : [convergent_lines(_24044, _24044)], (8 ^ _23787) ^ [_24165, _24167, _24169] : [distinct_points(_24169, _24167), -(distinct_points(_24169, _24165)), -(distinct_points(_24167, _24165))], (18 ^ _23787) ^ [_24489, _24491, _24493] : [distinct_lines(_24493, _24491), -(distinct_lines(_24493, _24489)), -(distinct_lines(_24491, _24489))], (28 ^ _23787) ^ [_24813, _24815, _24817] : [convergent_lines(_24817, _24815), -(convergent_lines(_24817, _24813)), -(convergent_lines(_24815, _24813))], (38 ^ _23787) ^ [_25137, _25139, _25141] : [distinct_points(_25141, _25139), apart_point_and_line(_25137, line_connecting(_25141, _25139)), 45 ^ _23787 : [(46 ^ _23787) ^ [] : [-(distinct_points(_25137, _25141))], (48 ^ _23787) ^ [] : [-(distinct_points(_25137, _25139))]]], (50 ^ _23787) ^ [_25543, _25545, _25547] : [convergent_lines(_25547, _25545), 55 ^ _23787 : [(56 ^ _23787) ^ [] : [apart_point_and_line(_25543, _25547)], (58 ^ _23787) ^ [] : [apart_point_and_line(_25543, _25545)]], -(distinct_points(_25543, intersection_point(_25547, _25545)))], (62 ^ _23787) ^ [_25962, _25964, _25966, _25968] : [distinct_points(_25968, _25966), distinct_lines(_25964, _25962), -(apart_point_and_line(_25968, _25964)), -(apart_point_and_line(_25968, _25962)), -(apart_point_and_line(_25966, _25964)), -(apart_point_and_line(_25966, _25962))], (84 ^ _23787) ^ [_26591, _26593, _26595] : [apart_point_and_line(_26595, _26593), -(distinct_points(_26595, _26591)), -(apart_point_and_line(_26591, _26593))], (104 ^ _23787) ^ [_27205, _27207] : [convergent_lines(_27207, _27205), -(distinct_lines(_27207, _27205))], (94 ^ _23787) ^ [_26915, _26917, _26919] : [apart_point_and_line(_26919, _26917), -(distinct_lines(_26917, _26915)), -(apart_point_and_line(_26919, _26915))]], input).
% 0.35/1.37 ncf('1',plain,[apart_point_and_line(127 ^ [], 128 ^ [])],start(131 ^ 0)).
% 0.35/1.37 ncf('1.1',plain,[-(apart_point_and_line(127 ^ [], 128 ^ [])), distinct_lines(128 ^ [], parallel_through_point(129 ^ [], 127 ^ [])), -(apart_point_and_line(127 ^ [], parallel_through_point(129 ^ [], 127 ^ []))), -(convergent_lines(128 ^ [], parallel_through_point(129 ^ [], 127 ^ [])))],extension(114 ^ 1,bind([[_27623, _27625, _27627], [parallel_through_point(129 ^ [], 127 ^ []), 128 ^ [], 127 ^ []]]))).
% 0.35/1.37 ncf('1.1.1',plain,[-(distinct_lines(128 ^ [], parallel_through_point(129 ^ [], 127 ^ [])))],extension(135 ^ 2)).
% 0.35/1.37 ncf('1.1.2',plain,[apart_point_and_line(127 ^ [], parallel_through_point(129 ^ [], 127 ^ []))],extension(112 ^ 2,bind([[_27517, _27519], [129 ^ [], 127 ^ []]]))).
% 0.35/1.37 ncf('1.1.3',plain,[convergent_lines(128 ^ [], parallel_through_point(129 ^ [], 127 ^ [])), -(convergent_lines(128 ^ [], 129 ^ [])), -(convergent_lines(parallel_through_point(129 ^ [], 127 ^ []), 129 ^ []))],extension(28 ^ 2,bind([[_24813, _24815, _24817], [129 ^ [], parallel_through_point(129 ^ [], 127 ^ []), 128 ^ []]]))).
% 0.35/1.37 ncf('1.1.3.1',plain,[convergent_lines(128 ^ [], 129 ^ [])],extension(133 ^ 3)).
% 0.35/1.37 ncf('1.1.3.2',plain,[convergent_lines(parallel_through_point(129 ^ [], 127 ^ []), 129 ^ [])],extension(110 ^ 3,bind([[_27421, _27423], [129 ^ [], 127 ^ []]]))).
% 0.35/1.37 %-----------------------------------------------------
% 0.35/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------