%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO191+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n031.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:08 EDT 2023
% Result : Theorem 0.40s 1.38s
% Output : Proof 0.40s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : GEO191+1 : TPTP v8.1.2. Released v3.3.0.
% 0.12/0.13 % Command : nanocop.sh %s %d
% 0.12/0.34 % Computer : n031.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Fri May 19 04:21:10 EDT 2023
% 0.12/0.34 % CPUTime :
% 0.40/1.38
% 0.40/1.38 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.40/1.38 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.40/1.38 %-----------------------------------------------------
% 0.40/1.38 ncf(matrix, plain, [(128 ^ _24885) ^ [] : [apart_point_and_line(intersection_point(115 ^ [], 116 ^ []), 113 ^ [])], (130 ^ _24885) ^ [] : [apart_point_and_line(intersection_point(115 ^ [], 116 ^ []), 114 ^ [])], (118 ^ _24885) ^ [] : [-(convergent_lines(113 ^ [], 114 ^ []))], (120 ^ _24885) ^ [] : [-(convergent_lines(115 ^ [], 116 ^ []))], (122 ^ _24885) ^ [] : [-(apart_point_and_line(intersection_point(113 ^ [], 114 ^ []), 115 ^ [])), -(apart_point_and_line(intersection_point(113 ^ [], 114 ^ []), 116 ^ []))], (2 ^ _24885) ^ [_24968] : [distinct_points(_24968, _24968)], (4 ^ _24885) ^ [_25045] : [distinct_lines(_25045, _25045)], (6 ^ _24885) ^ [_25122] : [convergent_lines(_25122, _25122)], (8 ^ _24885) ^ [_25243, _25245, _25247] : [distinct_points(_25247, _25245), -(distinct_points(_25247, _25243)), -(distinct_points(_25245, _25243))], (18 ^ _24885) ^ [_25567, _25569, _25571] : [distinct_lines(_25571, _25569), -(distinct_lines(_25571, _25567)), -(distinct_lines(_25569, _25567))], (28 ^ _24885) ^ [_25891, _25893, _25895] : [convergent_lines(_25895, _25893), -(convergent_lines(_25895, _25891)), -(convergent_lines(_25893, _25891))], (38 ^ _24885) ^ [_26201, _26203] : [distinct_points(_26203, _26201), apart_point_and_line(_26203, line_connecting(_26203, _26201))], (44 ^ _24885) ^ [_26418, _26420] : [distinct_points(_26420, _26418), apart_point_and_line(_26418, line_connecting(_26420, _26418))], (50 ^ _24885) ^ [_26635, _26637] : [convergent_lines(_26637, _26635), apart_point_and_line(intersection_point(_26637, _26635), _26637)], (56 ^ _24885) ^ [_26852, _26854] : [convergent_lines(_26854, _26852), apart_point_and_line(intersection_point(_26854, _26852), _26852)], (62 ^ _24885) ^ [_27097, _27099, _27101, _27103] : [distinct_points(_27103, _27101), distinct_lines(_27099, _27097), -(apart_point_and_line(_27103, _27099)), -(apart_point_and_line(_27103, _27097)), -(apart_point_and_line(_27101, _27099)), -(apart_point_and_line(_27101, _27097))], (84 ^ _24885) ^ [_27726, _27728, _27730] : [apart_point_and_line(_27730, _27728), -(distinct_points(_27730, _27726)), -(apart_point_and_line(_27726, _27728))], (94 ^ _24885) ^ [_28050, _28052, _28054] : [apart_point_and_line(_28054, _28052), -(distinct_lines(_28052, _28050)), -(apart_point_and_line(_28054, _28050))], (104 ^ _24885) ^ [_28354, _28356, _28358] : [convergent_lines(_28358, _28356), -(distinct_lines(_28356, _28354)), -(convergent_lines(_28358, _28354))]], input).
% 0.40/1.38 ncf('1',plain,[apart_point_and_line(intersection_point(115 ^ [], 116 ^ []), 113 ^ [])],start(128 ^ 0)).
% 0.40/1.38 ncf('1.1',plain,[-(apart_point_and_line(intersection_point(115 ^ [], 116 ^ []), 113 ^ [])), distinct_points(intersection_point(113 ^ [], 114 ^ []), intersection_point(115 ^ [], 116 ^ [])), distinct_lines(113 ^ [], 114 ^ []), -(apart_point_and_line(intersection_point(113 ^ [], 114 ^ []), 113 ^ [])), -(apart_point_and_line(intersection_point(113 ^ [], 114 ^ []), 114 ^ [])), -(apart_point_and_line(intersection_point(115 ^ [], 116 ^ []), 114 ^ []))],extension(62 ^ 1,bind([[_27097, _27099, _27101, _27103], [114 ^ [], 113 ^ [], intersection_point(115 ^ [], 116 ^ []), intersection_point(113 ^ [], 114 ^ [])]]))).
% 0.40/1.38 ncf('1.1.1',plain,[-(distinct_points(intersection_point(113 ^ [], 114 ^ []), intersection_point(115 ^ [], 116 ^ []))), apart_point_and_line(intersection_point(113 ^ [], 114 ^ []), 115 ^ []), -(apart_point_and_line(intersection_point(115 ^ [], 116 ^ []), 115 ^ []))],extension(84 ^ 2,bind([[_27726, _27728, _27730], [intersection_point(115 ^ [], 116 ^ []), 115 ^ [], intersection_point(113 ^ [], 114 ^ [])]]))).
% 0.40/1.38 ncf('1.1.1.1',plain,[-(apart_point_and_line(intersection_point(113 ^ [], 114 ^ []), 115 ^ [])), -(apart_point_and_line(intersection_point(113 ^ [], 114 ^ []), 116 ^ []))],extension(122 ^ 3)).
% 0.40/1.38 ncf('1.1.1.1.1',plain,[apart_point_and_line(intersection_point(113 ^ [], 114 ^ []), 116 ^ []), -(distinct_points(intersection_point(113 ^ [], 114 ^ []), intersection_point(115 ^ [], 116 ^ []))), -(apart_point_and_line(intersection_point(115 ^ [], 116 ^ []), 116 ^ []))],extension(84 ^ 4,bind([[_27726, _27728, _27730], [intersection_point(115 ^ [], 116 ^ []), 116 ^ [], intersection_point(113 ^ [], 114 ^ [])]]))).
% 0.40/1.38 ncf('1.1.1.1.1.1',plain,[distinct_points(intersection_point(113 ^ [], 114 ^ []), intersection_point(115 ^ [], 116 ^ []))],reduction('1.1')).
% 0.40/1.38 ncf('1.1.1.1.1.2',plain,[apart_point_and_line(intersection_point(115 ^ [], 116 ^ []), 116 ^ []), convergent_lines(115 ^ [], 116 ^ [])],extension(56 ^ 5,bind([[_26852, _26854], [116 ^ [], 115 ^ []]]))).
% 0.40/1.38 ncf('1.1.1.1.1.2.1',plain,[-(convergent_lines(115 ^ [], 116 ^ []))],extension(120 ^ 6)).
% 0.40/1.38 ncf('1.1.1.2',plain,[apart_point_and_line(intersection_point(115 ^ [], 116 ^ []), 115 ^ []), convergent_lines(115 ^ [], 116 ^ [])],extension(50 ^ 3,bind([[_26635, _26637], [116 ^ [], 115 ^ []]]))).
% 0.40/1.38 ncf('1.1.1.2.1',plain,[-(convergent_lines(115 ^ [], 116 ^ []))],extension(120 ^ 4)).
% 0.40/1.38 ncf('1.1.2',plain,[-(distinct_lines(113 ^ [], 114 ^ [])), distinct_lines(113 ^ [], 114 ^ []), -(distinct_lines(114 ^ [], 114 ^ []))],extension(18 ^ 2,bind([[_25567, _25569, _25571], [114 ^ [], 114 ^ [], 113 ^ []]]))).
% 0.40/1.38 ncf('1.1.2.1',plain,[-(distinct_lines(113 ^ [], 114 ^ [])), distinct_lines(114 ^ [], 113 ^ []), -(distinct_lines(114 ^ [], 114 ^ []))],extension(18 ^ 3,bind([[_25567, _25569, _25571], [114 ^ [], 113 ^ [], 114 ^ []]]))).
% 0.40/1.38 ncf('1.1.2.1.1',plain,[-(distinct_lines(114 ^ [], 113 ^ [])), convergent_lines(113 ^ [], 114 ^ []), -(convergent_lines(113 ^ [], 113 ^ []))],extension(104 ^ 4,bind([[_28354, _28356, _28358], [113 ^ [], 114 ^ [], 113 ^ []]]))).
% 0.40/1.38 ncf('1.1.2.1.1.1',plain,[-(convergent_lines(113 ^ [], 114 ^ []))],extension(118 ^ 5)).
% 0.40/1.38 ncf('1.1.2.1.1.2',plain,[convergent_lines(113 ^ [], 113 ^ [])],extension(6 ^ 5,bind([[_25122], [113 ^ []]]))).
% 0.40/1.38 ncf('1.1.2.1.2',plain,[distinct_lines(114 ^ [], 114 ^ [])],extension(4 ^ 4,bind([[_25045], [114 ^ []]]))).
% 0.40/1.38 ncf('1.1.2.2',plain,[distinct_lines(114 ^ [], 114 ^ [])],extension(4 ^ 3,bind([[_25045], [114 ^ []]]))).
% 0.40/1.38 ncf('1.1.3',plain,[apart_point_and_line(intersection_point(113 ^ [], 114 ^ []), 113 ^ []), convergent_lines(113 ^ [], 114 ^ [])],extension(50 ^ 2,bind([[_26635, _26637], [114 ^ [], 113 ^ []]]))).
% 0.40/1.38 ncf('1.1.3.1',plain,[-(convergent_lines(113 ^ [], 114 ^ []))],extension(118 ^ 3)).
% 0.40/1.38 ncf('1.1.4',plain,[apart_point_and_line(intersection_point(113 ^ [], 114 ^ []), 114 ^ []), convergent_lines(113 ^ [], 114 ^ [])],extension(56 ^ 2,bind([[_26852, _26854], [114 ^ [], 113 ^ []]]))).
% 0.40/1.38 ncf('1.1.4.1',plain,[-(convergent_lines(113 ^ [], 114 ^ []))],extension(118 ^ 3)).
% 0.40/1.38 ncf('1.1.5',plain,[apart_point_and_line(intersection_point(115 ^ [], 116 ^ []), 114 ^ [])],extension(130 ^ 2)).
% 0.40/1.38 %-----------------------------------------------------
% 0.40/1.38 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------