%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO204+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n011.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.32s 1.37s
% Output : Proof 0.32s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : GEO204+1 : TPTP v8.1.2. Released v3.3.0.
% 0.12/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n011.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Fri May 19 04:23:18 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.32/1.37
% 0.32/1.37 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.32/1.37 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.32/1.37 %-----------------------------------------------------
% 0.32/1.37 ncf(matrix, plain, [(117 ^ _23420) ^ [] : [-(distinct_points(113 ^ [], 114 ^ []))], (119 ^ _23420) ^ [] : [distinct_points(114 ^ [], 115 ^ [])], (121 ^ _23420) ^ [] : [distinct_points(113 ^ [], 115 ^ []), -(distinct_lines(line_connecting(113 ^ [], 114 ^ []), line_connecting(113 ^ [], 115 ^ [])))], (2 ^ _23420) ^ [_23503] : [distinct_points(_23503, _23503)], (4 ^ _23420) ^ [_23580] : [distinct_lines(_23580, _23580)], (6 ^ _23420) ^ [_23657] : [convergent_lines(_23657, _23657)], (8 ^ _23420) ^ [_23778, _23780, _23782] : [distinct_points(_23782, _23780), -(distinct_points(_23782, _23778)), -(distinct_points(_23780, _23778))], (18 ^ _23420) ^ [_24102, _24104, _24106] : [distinct_lines(_24106, _24104), -(distinct_lines(_24106, _24102)), -(distinct_lines(_24104, _24102))], (28 ^ _23420) ^ [_24426, _24428, _24430] : [convergent_lines(_24430, _24428), -(convergent_lines(_24430, _24426)), -(convergent_lines(_24428, _24426))], (38 ^ _23420) ^ [_24736, _24738] : [distinct_points(_24738, _24736), apart_point_and_line(_24738, line_connecting(_24738, _24736))], (44 ^ _23420) ^ [_24953, _24955] : [distinct_points(_24955, _24953), apart_point_and_line(_24953, line_connecting(_24955, _24953))], (50 ^ _23420) ^ [_25170, _25172] : [convergent_lines(_25172, _25170), apart_point_and_line(intersection_point(_25172, _25170), _25172)], (56 ^ _23420) ^ [_25387, _25389] : [convergent_lines(_25389, _25387), apart_point_and_line(intersection_point(_25389, _25387), _25387)], (62 ^ _23420) ^ [_25632, _25634, _25636, _25638] : [distinct_points(_25638, _25636), distinct_lines(_25634, _25632), -(apart_point_and_line(_25638, _25634)), -(apart_point_and_line(_25638, _25632)), -(apart_point_and_line(_25636, _25634)), -(apart_point_and_line(_25636, _25632))], (84 ^ _23420) ^ [_26261, _26263, _26265] : [apart_point_and_line(_26265, _26263), -(distinct_points(_26265, _26261)), -(apart_point_and_line(_26261, _26263))], (94 ^ _23420) ^ [_26585, _26587, _26589] : [apart_point_and_line(_26589, _26587), -(distinct_lines(_26587, _26585)), -(apart_point_and_line(_26589, _26585))], (104 ^ _23420) ^ [_26889, _26891, _26893] : [convergent_lines(_26893, _26891), -(distinct_lines(_26891, _26889)), -(convergent_lines(_26893, _26889))]], input).
% 0.32/1.37 ncf('1',plain,[distinct_points(114 ^ [], 115 ^ [])],start(119 ^ 0)).
% 0.32/1.37 ncf('1.1',plain,[-(distinct_points(114 ^ [], 115 ^ [])), apart_point_and_line(114 ^ [], line_connecting(113 ^ [], 115 ^ [])), -(apart_point_and_line(115 ^ [], line_connecting(113 ^ [], 115 ^ [])))],extension(84 ^ 1,bind([[_26261, _26263, _26265], [115 ^ [], line_connecting(113 ^ [], 115 ^ []), 114 ^ []]]))).
% 0.32/1.37 ncf('1.1.1',plain,[-(apart_point_and_line(114 ^ [], line_connecting(113 ^ [], 115 ^ []))), distinct_points(114 ^ [], 113 ^ []), distinct_lines(line_connecting(113 ^ [], 114 ^ []), line_connecting(113 ^ [], 115 ^ [])), -(apart_point_and_line(114 ^ [], line_connecting(113 ^ [], 114 ^ []))), -(apart_point_and_line(113 ^ [], line_connecting(113 ^ [], 114 ^ []))), -(apart_point_and_line(113 ^ [], line_connecting(113 ^ [], 115 ^ [])))],extension(62 ^ 2,bind([[_25632, _25634, _25636, _25638], [line_connecting(113 ^ [], 115 ^ []), line_connecting(113 ^ [], 114 ^ []), 113 ^ [], 114 ^ []]]))).
% 0.32/1.37 ncf('1.1.1.1',plain,[-(distinct_points(114 ^ [], 113 ^ [])), distinct_points(113 ^ [], 114 ^ []), -(distinct_points(113 ^ [], 113 ^ []))],extension(8 ^ 3,bind([[_23778, _23780, _23782], [113 ^ [], 114 ^ [], 113 ^ []]]))).
% 0.32/1.37 ncf('1.1.1.1.1',plain,[-(distinct_points(113 ^ [], 114 ^ []))],extension(117 ^ 4)).
% 0.32/1.37 ncf('1.1.1.1.2',plain,[distinct_points(113 ^ [], 113 ^ [])],extension(2 ^ 4,bind([[_23503], [113 ^ []]]))).
% 0.32/1.37 ncf('1.1.1.2',plain,[-(distinct_lines(line_connecting(113 ^ [], 114 ^ []), line_connecting(113 ^ [], 115 ^ []))), distinct_points(113 ^ [], 115 ^ [])],extension(121 ^ 3)).
% 0.32/1.37 ncf('1.1.1.2.1',plain,[-(distinct_points(113 ^ [], 115 ^ [])), distinct_points(113 ^ [], 114 ^ []), -(distinct_points(114 ^ [], 115 ^ []))],extension(8 ^ 4,bind([[_23778, _23780, _23782], [115 ^ [], 114 ^ [], 113 ^ []]]))).
% 0.32/1.37 ncf('1.1.1.2.1.1',plain,[-(distinct_points(113 ^ [], 114 ^ []))],extension(117 ^ 5)).
% 0.32/1.37 ncf('1.1.1.2.1.2',plain,[distinct_points(114 ^ [], 115 ^ [])],reduction('1')).
% 0.32/1.37 ncf('1.1.1.3',plain,[apart_point_and_line(114 ^ [], line_connecting(113 ^ [], 114 ^ [])), distinct_points(113 ^ [], 114 ^ [])],extension(44 ^ 3,bind([[_24953, _24955], [114 ^ [], 113 ^ []]]))).
% 0.32/1.37 ncf('1.1.1.3.1',plain,[-(distinct_points(113 ^ [], 114 ^ []))],extension(117 ^ 4)).
% 0.32/1.37 ncf('1.1.1.4',plain,[apart_point_and_line(113 ^ [], line_connecting(113 ^ [], 114 ^ [])), distinct_points(113 ^ [], 114 ^ [])],extension(38 ^ 3,bind([[_24736, _24738], [114 ^ [], 113 ^ []]]))).
% 0.32/1.37 ncf('1.1.1.4.1',plain,[-(distinct_points(113 ^ [], 114 ^ []))],extension(117 ^ 4)).
% 0.32/1.37 ncf('1.1.1.5',plain,[apart_point_and_line(113 ^ [], line_connecting(113 ^ [], 115 ^ [])), distinct_points(113 ^ [], 115 ^ [])],extension(38 ^ 3,bind([[_24736, _24738], [115 ^ [], 113 ^ []]]))).
% 0.32/1.37 ncf('1.1.1.5.1',plain,[-(distinct_points(113 ^ [], 115 ^ [])), distinct_points(113 ^ [], 114 ^ []), -(distinct_points(114 ^ [], 115 ^ []))],extension(8 ^ 4,bind([[_23778, _23780, _23782], [115 ^ [], 114 ^ [], 113 ^ []]]))).
% 0.32/1.37 ncf('1.1.1.5.1.1',plain,[-(distinct_points(113 ^ [], 114 ^ []))],extension(117 ^ 5)).
% 0.32/1.37 ncf('1.1.1.5.1.2',plain,[distinct_points(114 ^ [], 115 ^ [])],reduction('1')).
% 0.32/1.37 ncf('1.1.2',plain,[apart_point_and_line(115 ^ [], line_connecting(113 ^ [], 115 ^ [])), distinct_points(113 ^ [], 115 ^ [])],extension(44 ^ 2,bind([[_24953, _24955], [115 ^ [], 113 ^ []]]))).
% 0.32/1.37 ncf('1.1.2.1',plain,[-(distinct_points(113 ^ [], 115 ^ [])), distinct_points(113 ^ [], 114 ^ []), -(distinct_points(114 ^ [], 115 ^ []))],extension(8 ^ 3,bind([[_23778, _23780, _23782], [115 ^ [], 114 ^ [], 113 ^ []]]))).
% 0.32/1.37 ncf('1.1.2.1.1',plain,[-(distinct_points(113 ^ [], 114 ^ []))],extension(117 ^ 4)).
% 0.32/1.37 ncf('1.1.2.1.2',plain,[distinct_points(114 ^ [], 115 ^ [])],reduction('1')).
% 0.32/1.37 %-----------------------------------------------------
% 0.32/1.37 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------