%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO179+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n003.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:05 EDT 2023
% Result : Theorem 0.44s 1.37s
% Output : Proof 0.44s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : GEO179+1 : TPTP v8.1.2. Released v3.3.0.
% 0.06/0.12 % Command : nanocop.sh %s %d
% 0.11/0.32 % Computer : n003.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.33 % DateTime : Fri May 19 04:00:15 EDT 2023
% 0.11/0.33 % CPUTime :
% 0.44/1.37
% 0.44/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.44/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.44/1.37 %-----------------------------------------------------
% 0.44/1.37 ncf(matrix, plain, [(117 ^ _24499) ^ [] : [-(distinct_points(113 ^ [], 114 ^ []))], (119 ^ _24499) ^ [] : [-(apart_point_and_line(115 ^ [], line_connecting(113 ^ [], 114 ^ [])))], (121 ^ _24499) ^ [] : [distinct_lines(line_connecting(113 ^ [], 114 ^ []), line_connecting(115 ^ [], 113 ^ [])), distinct_lines(line_connecting(113 ^ [], 114 ^ []), line_connecting(115 ^ [], 114 ^ []))], (2 ^ _24499) ^ [_24582] : [distinct_points(_24582, _24582)], (4 ^ _24499) ^ [_24659] : [distinct_lines(_24659, _24659)], (6 ^ _24499) ^ [_24736] : [convergent_lines(_24736, _24736)], (8 ^ _24499) ^ [_24857, _24859, _24861] : [distinct_points(_24861, _24859), -(distinct_points(_24861, _24857)), -(distinct_points(_24859, _24857))], (18 ^ _24499) ^ [_25181, _25183, _25185] : [distinct_lines(_25185, _25183), -(distinct_lines(_25185, _25181)), -(distinct_lines(_25183, _25181))], (28 ^ _24499) ^ [_25505, _25507, _25509] : [convergent_lines(_25509, _25507), -(convergent_lines(_25509, _25505)), -(convergent_lines(_25507, _25505))], (38 ^ _24499) ^ [_25815, _25817] : [distinct_points(_25817, _25815), apart_point_and_line(_25817, line_connecting(_25817, _25815))], (44 ^ _24499) ^ [_26032, _26034] : [distinct_points(_26034, _26032), apart_point_and_line(_26032, line_connecting(_26034, _26032))], (50 ^ _24499) ^ [_26249, _26251] : [convergent_lines(_26251, _26249), apart_point_and_line(intersection_point(_26251, _26249), _26251)], (56 ^ _24499) ^ [_26466, _26468] : [convergent_lines(_26468, _26466), apart_point_and_line(intersection_point(_26468, _26466), _26466)], (62 ^ _24499) ^ [_26711, _26713, _26715, _26717] : [distinct_points(_26717, _26715), distinct_lines(_26713, _26711), -(apart_point_and_line(_26717, _26713)), -(apart_point_and_line(_26717, _26711)), -(apart_point_and_line(_26715, _26713)), -(apart_point_and_line(_26715, _26711))], (84 ^ _24499) ^ [_27340, _27342, _27344] : [apart_point_and_line(_27344, _27342), -(distinct_points(_27344, _27340)), -(apart_point_and_line(_27340, _27342))], (94 ^ _24499) ^ [_27664, _27666, _27668] : [apart_point_and_line(_27668, _27666), -(distinct_lines(_27666, _27664)), -(apart_point_and_line(_27668, _27664))], (104 ^ _24499) ^ [_27968, _27970, _27972] : [convergent_lines(_27972, _27970), -(distinct_lines(_27970, _27968)), -(convergent_lines(_27972, _27968))]], input).
% 0.44/1.37 ncf('1',plain,[distinct_lines(line_connecting(113 ^ [], 114 ^ []), line_connecting(115 ^ [], 113 ^ [])), distinct_lines(line_connecting(113 ^ [], 114 ^ []), line_connecting(115 ^ [], 114 ^ []))],start(121 ^ 0)).
% 0.44/1.37 ncf('1.1',plain,[-(distinct_lines(line_connecting(113 ^ [], 114 ^ []), line_connecting(115 ^ [], 113 ^ []))), apart_point_and_line(115 ^ [], line_connecting(113 ^ [], 114 ^ [])), -(apart_point_and_line(115 ^ [], line_connecting(115 ^ [], 113 ^ [])))],extension(94 ^ 1,bind([[_27664, _27666, _27668], [line_connecting(115 ^ [], 113 ^ []), line_connecting(113 ^ [], 114 ^ []), 115 ^ []]]))).
% 0.44/1.37 ncf('1.1.1',plain,[-(apart_point_and_line(115 ^ [], line_connecting(113 ^ [], 114 ^ [])))],extension(119 ^ 2)).
% 0.44/1.37 ncf('1.1.2',plain,[apart_point_and_line(115 ^ [], line_connecting(115 ^ [], 113 ^ [])), distinct_points(115 ^ [], 113 ^ [])],extension(38 ^ 2,bind([[_25815, _25817], [113 ^ [], 115 ^ []]]))).
% 0.44/1.37 ncf('1.1.2.1',plain,[-(distinct_points(115 ^ [], 113 ^ [])), distinct_points(114 ^ [], 115 ^ []), -(distinct_points(114 ^ [], 113 ^ []))],extension(8 ^ 3,bind([[_24857, _24859, _24861], [113 ^ [], 115 ^ [], 114 ^ []]]))).
% 0.44/1.37 ncf('1.1.2.1.1',plain,[-(distinct_points(114 ^ [], 115 ^ [])), distinct_points(113 ^ [], 114 ^ []), -(distinct_points(113 ^ [], 115 ^ []))],extension(8 ^ 4,bind([[_24857, _24859, _24861], [115 ^ [], 114 ^ [], 113 ^ []]]))).
% 0.44/1.37 ncf('1.1.2.1.1.1',plain,[-(distinct_points(113 ^ [], 114 ^ []))],extension(117 ^ 5)).
% 0.44/1.37 ncf('1.1.2.1.1.2',plain,[distinct_points(113 ^ [], 115 ^ []), -(distinct_points(113 ^ [], 113 ^ [])), -(distinct_points(115 ^ [], 113 ^ []))],extension(8 ^ 5,bind([[_24857, _24859, _24861], [113 ^ [], 115 ^ [], 113 ^ []]]))).
% 0.44/1.37 ncf('1.1.2.1.1.2.1',plain,[distinct_points(113 ^ [], 113 ^ [])],extension(2 ^ 6,bind([[_24582], [113 ^ []]]))).
% 0.44/1.37 ncf('1.1.2.1.1.2.2',plain,[distinct_points(115 ^ [], 113 ^ [])],reduction('1.1.2')).
% 0.44/1.37 ncf('1.1.2.1.2',plain,[distinct_points(114 ^ [], 113 ^ []), -(distinct_points(114 ^ [], 114 ^ [])), -(distinct_points(113 ^ [], 114 ^ []))],extension(8 ^ 4,bind([[_24857, _24859, _24861], [114 ^ [], 113 ^ [], 114 ^ []]]))).
% 0.44/1.37 ncf('1.1.2.1.2.1',plain,[distinct_points(114 ^ [], 114 ^ [])],extension(2 ^ 5,bind([[_24582], [114 ^ []]]))).
% 0.44/1.37 ncf('1.1.2.1.2.2',plain,[distinct_points(113 ^ [], 114 ^ []), apart_point_and_line(113 ^ [], line_connecting(113 ^ [], 114 ^ []))],extension(38 ^ 5,bind([[_25815, _25817], [114 ^ [], 113 ^ []]]))).
% 0.44/1.37 ncf('1.1.2.1.2.2.1',plain,[-(apart_point_and_line(113 ^ [], line_connecting(113 ^ [], 114 ^ []))), apart_point_and_line(115 ^ [], line_connecting(113 ^ [], 114 ^ [])), -(distinct_points(115 ^ [], 113 ^ []))],extension(84 ^ 6,bind([[_27340, _27342, _27344], [113 ^ [], line_connecting(113 ^ [], 114 ^ []), 115 ^ []]]))).
% 0.44/1.37 ncf('1.1.2.1.2.2.1.1',plain,[-(apart_point_and_line(115 ^ [], line_connecting(113 ^ [], 114 ^ [])))],extension(119 ^ 7)).
% 0.44/1.37 ncf('1.1.2.1.2.2.1.2',plain,[distinct_points(115 ^ [], 113 ^ [])],reduction('1.1.2')).
% 0.44/1.37 ncf('1.2',plain,[-(distinct_lines(line_connecting(113 ^ [], 114 ^ []), line_connecting(115 ^ [], 114 ^ []))), apart_point_and_line(115 ^ [], line_connecting(113 ^ [], 114 ^ [])), -(apart_point_and_line(115 ^ [], line_connecting(115 ^ [], 114 ^ [])))],extension(94 ^ 1,bind([[_27664, _27666, _27668], [line_connecting(115 ^ [], 114 ^ []), line_connecting(113 ^ [], 114 ^ []), 115 ^ []]]))).
% 0.44/1.37 ncf('1.2.1',plain,[-(apart_point_and_line(115 ^ [], line_connecting(113 ^ [], 114 ^ [])))],extension(119 ^ 2)).
% 0.44/1.37 ncf('1.2.2',plain,[apart_point_and_line(115 ^ [], line_connecting(115 ^ [], 114 ^ [])), distinct_points(115 ^ [], 114 ^ [])],extension(38 ^ 2,bind([[_25815, _25817], [114 ^ [], 115 ^ []]]))).
% 0.44/1.37 ncf('1.2.2.1',plain,[-(distinct_points(115 ^ [], 114 ^ [])), distinct_points(113 ^ [], 115 ^ []), -(distinct_points(113 ^ [], 114 ^ []))],extension(8 ^ 3,bind([[_24857, _24859, _24861], [114 ^ [], 115 ^ [], 113 ^ []]]))).
% 0.44/1.37 ncf('1.2.2.1.1',plain,[-(distinct_points(113 ^ [], 115 ^ [])), distinct_points(113 ^ [], 114 ^ []), -(distinct_points(114 ^ [], 115 ^ []))],extension(8 ^ 4,bind([[_24857, _24859, _24861], [115 ^ [], 114 ^ [], 113 ^ []]]))).
% 0.44/1.37 ncf('1.2.2.1.1.1',plain,[-(distinct_points(113 ^ [], 114 ^ []))],extension(117 ^ 5)).
% 0.44/1.37 ncf('1.2.2.1.1.2',plain,[distinct_points(114 ^ [], 115 ^ []), -(distinct_points(114 ^ [], 114 ^ [])), -(distinct_points(115 ^ [], 114 ^ []))],extension(8 ^ 5,bind([[_24857, _24859, _24861], [114 ^ [], 115 ^ [], 114 ^ []]]))).
% 0.44/1.37 ncf('1.2.2.1.1.2.1',plain,[distinct_points(114 ^ [], 114 ^ [])],extension(2 ^ 6,bind([[_24582], [114 ^ []]]))).
% 0.44/1.37 ncf('1.2.2.1.1.2.2',plain,[distinct_points(115 ^ [], 114 ^ [])],reduction('1.2.2')).
% 0.44/1.37 ncf('1.2.2.1.2',plain,[distinct_points(113 ^ [], 114 ^ []), apart_point_and_line(114 ^ [], line_connecting(113 ^ [], 114 ^ []))],extension(44 ^ 4,bind([[_26032, _26034], [114 ^ [], 113 ^ []]]))).
% 0.44/1.37 ncf('1.2.2.1.2.1',plain,[-(apart_point_and_line(114 ^ [], line_connecting(113 ^ [], 114 ^ []))), apart_point_and_line(115 ^ [], line_connecting(113 ^ [], 114 ^ [])), -(distinct_points(115 ^ [], 114 ^ []))],extension(84 ^ 5,bind([[_27340, _27342, _27344], [114 ^ [], line_connecting(113 ^ [], 114 ^ []), 115 ^ []]]))).
% 0.44/1.37 ncf('1.2.2.1.2.1.1',plain,[-(apart_point_and_line(115 ^ [], line_connecting(113 ^ [], 114 ^ [])))],extension(119 ^ 6)).
% 0.44/1.37 ncf('1.2.2.1.2.1.2',plain,[distinct_points(115 ^ [], 114 ^ [])],reduction('1.2.2')).
% 0.44/1.37 %-----------------------------------------------------
% 0.44/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------