%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO198+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n018.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.35s 1.40s
% Output : Proof 0.35s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : GEO198+1 : TPTP v8.1.2. Released v3.3.0.
% 0.08/0.14 % Command : nanocop.sh %s %d
% 0.14/0.35 % Computer : n018.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Fri May 19 04:47:13 EDT 2023
% 0.14/0.35 % CPUTime :
% 0.35/1.40
% 0.35/1.40 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.35/1.40 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.35/1.40 %-----------------------------------------------------
% 0.35/1.40 ncf(matrix, plain, [(117 ^ _23303) ^ [] : [-(convergent_lines(113 ^ [], 114 ^ []))], (119 ^ _23303) ^ [] : [-(convergent_lines(115 ^ [], 114 ^ []))], (121 ^ _23303) ^ [] : [-(convergent_lines(113 ^ [], 115 ^ []))], (123 ^ _23303) ^ [] : [apart_point_and_line(intersection_point(113 ^ [], 114 ^ []), 115 ^ [])], (125 ^ _23303) ^ [] : [-(apart_point_and_line(intersection_point(113 ^ [], 115 ^ []), 114 ^ []))], (2 ^ _23303) ^ [_23386] : [distinct_points(_23386, _23386)], (4 ^ _23303) ^ [_23463] : [distinct_lines(_23463, _23463)], (6 ^ _23303) ^ [_23540] : [convergent_lines(_23540, _23540)], (8 ^ _23303) ^ [_23661, _23663, _23665] : [distinct_points(_23665, _23663), -(distinct_points(_23665, _23661)), -(distinct_points(_23663, _23661))], (18 ^ _23303) ^ [_23985, _23987, _23989] : [distinct_lines(_23989, _23987), -(distinct_lines(_23989, _23985)), -(distinct_lines(_23987, _23985))], (28 ^ _23303) ^ [_24309, _24311, _24313] : [convergent_lines(_24313, _24311), -(convergent_lines(_24313, _24309)), -(convergent_lines(_24311, _24309))], (38 ^ _23303) ^ [_24619, _24621] : [distinct_points(_24621, _24619), apart_point_and_line(_24621, line_connecting(_24621, _24619))], (44 ^ _23303) ^ [_24836, _24838] : [distinct_points(_24838, _24836), apart_point_and_line(_24836, line_connecting(_24838, _24836))], (50 ^ _23303) ^ [_25053, _25055] : [convergent_lines(_25055, _25053), apart_point_and_line(intersection_point(_25055, _25053), _25055)], (56 ^ _23303) ^ [_25270, _25272] : [convergent_lines(_25272, _25270), apart_point_and_line(intersection_point(_25272, _25270), _25270)], (62 ^ _23303) ^ [_25515, _25517, _25519, _25521] : [distinct_points(_25521, _25519), distinct_lines(_25517, _25515), -(apart_point_and_line(_25521, _25517)), -(apart_point_and_line(_25521, _25515)), -(apart_point_and_line(_25519, _25517)), -(apart_point_and_line(_25519, _25515))], (84 ^ _23303) ^ [_26144, _26146, _26148] : [apart_point_and_line(_26148, _26146), -(distinct_points(_26148, _26144)), -(apart_point_and_line(_26144, _26146))], (94 ^ _23303) ^ [_26468, _26470, _26472] : [apart_point_and_line(_26472, _26470), -(distinct_lines(_26470, _26468)), -(apart_point_and_line(_26472, _26468))], (104 ^ _23303) ^ [_26772, _26774, _26776] : [convergent_lines(_26776, _26774), -(distinct_lines(_26774, _26772)), -(convergent_lines(_26776, _26772))]], input).
% 0.35/1.40 ncf('1',plain,[apart_point_and_line(intersection_point(113 ^ [], 114 ^ []), 115 ^ [])],start(123 ^ 0)).
% 0.35/1.40 ncf('1.1',plain,[-(apart_point_and_line(intersection_point(113 ^ [], 114 ^ []), 115 ^ [])), distinct_points(intersection_point(113 ^ [], 115 ^ []), intersection_point(113 ^ [], 114 ^ [])), distinct_lines(115 ^ [], 113 ^ []), -(apart_point_and_line(intersection_point(113 ^ [], 115 ^ []), 115 ^ [])), -(apart_point_and_line(intersection_point(113 ^ [], 115 ^ []), 113 ^ [])), -(apart_point_and_line(intersection_point(113 ^ [], 114 ^ []), 113 ^ []))],extension(62 ^ 1,bind([[_25515, _25517, _25519, _25521], [113 ^ [], 115 ^ [], intersection_point(113 ^ [], 114 ^ []), intersection_point(113 ^ [], 115 ^ [])]]))).
% 0.35/1.40 ncf('1.1.1',plain,[-(distinct_points(intersection_point(113 ^ [], 115 ^ []), intersection_point(113 ^ [], 114 ^ []))), apart_point_and_line(intersection_point(113 ^ [], 115 ^ []), 114 ^ []), -(apart_point_and_line(intersection_point(113 ^ [], 114 ^ []), 114 ^ []))],extension(84 ^ 2,bind([[_26144, _26146, _26148], [intersection_point(113 ^ [], 114 ^ []), 114 ^ [], intersection_point(113 ^ [], 115 ^ [])]]))).
% 0.35/1.40 ncf('1.1.1.1',plain,[-(apart_point_and_line(intersection_point(113 ^ [], 115 ^ []), 114 ^ []))],extension(125 ^ 3)).
% 0.35/1.40 ncf('1.1.1.2',plain,[apart_point_and_line(intersection_point(113 ^ [], 114 ^ []), 114 ^ []), convergent_lines(113 ^ [], 114 ^ [])],extension(56 ^ 3,bind([[_25270, _25272], [114 ^ [], 113 ^ []]]))).
% 0.35/1.40 ncf('1.1.1.2.1',plain,[-(convergent_lines(113 ^ [], 114 ^ []))],extension(117 ^ 4)).
% 0.35/1.40 ncf('1.1.2',plain,[-(distinct_lines(115 ^ [], 113 ^ [])), convergent_lines(113 ^ [], 115 ^ []), -(convergent_lines(113 ^ [], 113 ^ []))],extension(104 ^ 2,bind([[_26772, _26774, _26776], [113 ^ [], 115 ^ [], 113 ^ []]]))).
% 0.35/1.40 ncf('1.1.2.1',plain,[-(convergent_lines(113 ^ [], 115 ^ []))],extension(121 ^ 3)).
% 0.35/1.40 ncf('1.1.2.2',plain,[convergent_lines(113 ^ [], 113 ^ [])],extension(6 ^ 3,bind([[_23540], [113 ^ []]]))).
% 0.35/1.40 ncf('1.1.3',plain,[apart_point_and_line(intersection_point(113 ^ [], 115 ^ []), 115 ^ []), convergent_lines(113 ^ [], 115 ^ [])],extension(56 ^ 2,bind([[_25270, _25272], [115 ^ [], 113 ^ []]]))).
% 0.35/1.40 ncf('1.1.3.1',plain,[-(convergent_lines(113 ^ [], 115 ^ []))],extension(121 ^ 3)).
% 0.35/1.40 ncf('1.1.4',plain,[apart_point_and_line(intersection_point(113 ^ [], 115 ^ []), 113 ^ []), convergent_lines(113 ^ [], 115 ^ [])],extension(50 ^ 2,bind([[_25053, _25055], [115 ^ [], 113 ^ []]]))).
% 0.35/1.40 ncf('1.1.4.1',plain,[-(convergent_lines(113 ^ [], 115 ^ []))],extension(121 ^ 3)).
% 0.35/1.40 ncf('1.1.5',plain,[apart_point_and_line(intersection_point(113 ^ [], 114 ^ []), 113 ^ []), convergent_lines(113 ^ [], 114 ^ [])],extension(50 ^ 2,bind([[_25053, _25055], [114 ^ [], 113 ^ []]]))).
% 0.35/1.40 ncf('1.1.5.1',plain,[-(convergent_lines(113 ^ [], 114 ^ []))],extension(117 ^ 3)).
% 0.35/1.40 %-----------------------------------------------------
% 0.35/1.40 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------