%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO213+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n013.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:14 EDT 2023
% Result : Theorem 4.54s 5.51s
% Output : Proof 4.54s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO213+1 : TPTP v8.1.2. Released v3.3.0.
% 0.07/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n013.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:06:20 EDT 2023
% 0.12/0.33 % CPUTime :
% 4.54/5.51
% 4.54/5.51 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 4.54/5.51 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.54/5.51 %-----------------------------------------------------
% 4.54/5.51 ncf(matrix, plain, [(181 ^ _43023) ^ [] : [-(unorthogonal_lines(177 ^ [], 178 ^ []))], (183 ^ _43023) ^ [] : [distinct_lines(177 ^ [], 179 ^ [])], (185 ^ _43023) ^ [] : [unorthogonal_lines(178 ^ [], 179 ^ [])], (114 ^ _43023) ^ [_46852, _46854] : [convergent_lines(parallel_through_point(_46852, _46854), _46852)], (116 ^ _43023) ^ [_46948, _46950] : [apart_point_and_line(_46950, parallel_through_point(_46948, _46950))], (118 ^ _43023) ^ [_47054, _47056, _47058] : [distinct_lines(_47056, _47054), -(apart_point_and_line(_47058, _47056)), -(apart_point_and_line(_47058, _47054)), -(convergent_lines(_47056, _47054))], (132 ^ _43023) ^ [_47462, _47464] : [-(convergent_lines(_47464, _47462)), -(unorthogonal_lines(_47464, _47462))], (138 ^ _43023) ^ [_47687, _47689, _47691] : [convergent_lines(_47691, _47689), unorthogonal_lines(_47691, _47689), 147 ^ _43023 : [(148 ^ _43023) ^ [] : [-(convergent_lines(_47691, _47687))], (150 ^ _43023) ^ [] : [-(unorthogonal_lines(_47691, _47687))]], 151 ^ _43023 : [(152 ^ _43023) ^ [] : [-(convergent_lines(_47689, _47687))], (154 ^ _43023) ^ [] : [-(unorthogonal_lines(_47689, _47687))]]], (156 ^ _43023) ^ [_48230, _48232] : [unorthogonal_lines(orthogonal_through_point(_48230, _48232), _48230)], (158 ^ _43023) ^ [_48326, _48328] : [apart_point_and_line(_48328, orthogonal_through_point(_48326, _48328))], (160 ^ _43023) ^ [_48446, _48448, _48450, _48452] : [distinct_lines(_48450, _48448), -(apart_point_and_line(_48452, _48450)), -(apart_point_and_line(_48452, _48448)), -(unorthogonal_lines(_48450, _48446)), -(unorthogonal_lines(_48448, _48446))], (2 ^ _43023) ^ [_43126] : [distinct_points(_43126, _43126)], (4 ^ _43023) ^ [_43203] : [distinct_lines(_43203, _43203)], (6 ^ _43023) ^ [_43280] : [convergent_lines(_43280, _43280)], (8 ^ _43023) ^ [_43401, _43403, _43405] : [distinct_points(_43405, _43403), -(distinct_points(_43405, _43401)), -(distinct_points(_43403, _43401))], (18 ^ _43023) ^ [_43725, _43727, _43729] : [distinct_lines(_43729, _43727), -(distinct_lines(_43729, _43725)), -(distinct_lines(_43727, _43725))], (28 ^ _43023) ^ [_44049, _44051, _44053] : [convergent_lines(_44053, _44051), -(convergent_lines(_44053, _44049)), -(convergent_lines(_44051, _44049))], (38 ^ _43023) ^ [_44359, _44361] : [distinct_points(_44361, _44359), apart_point_and_line(_44361, line_connecting(_44361, _44359))], (44 ^ _43023) ^ [_44576, _44578] : [distinct_points(_44578, _44576), apart_point_and_line(_44576, line_connecting(_44578, _44576))], (50 ^ _43023) ^ [_44793, _44795] : [convergent_lines(_44795, _44793), apart_point_and_line(intersection_point(_44795, _44793), _44795)], (56 ^ _43023) ^ [_45010, _45012] : [convergent_lines(_45012, _45010), apart_point_and_line(intersection_point(_45012, _45010), _45010)], (62 ^ _43023) ^ [_45255, _45257, _45259, _45261] : [distinct_points(_45261, _45259), distinct_lines(_45257, _45255), -(apart_point_and_line(_45261, _45257)), -(apart_point_and_line(_45261, _45255)), -(apart_point_and_line(_45259, _45257)), -(apart_point_and_line(_45259, _45255))], (84 ^ _43023) ^ [_45884, _45886, _45888] : [apart_point_and_line(_45888, _45886), -(distinct_points(_45888, _45884)), -(apart_point_and_line(_45884, _45886))], (94 ^ _43023) ^ [_46208, _46210, _46212] : [apart_point_and_line(_46212, _46210), -(distinct_lines(_46210, _46208)), -(apart_point_and_line(_46212, _46208))], (104 ^ _43023) ^ [_46512, _46514, _46516] : [convergent_lines(_46516, _46514), -(distinct_lines(_46514, _46512)), -(convergent_lines(_46516, _46512))]], input).
% 4.54/5.51 ncf('1',plain,[distinct_lines(177 ^ [], 179 ^ [])],start(183 ^ 0)).
% 4.54/5.51 ncf('1.1',plain,[-(distinct_lines(177 ^ [], 179 ^ [])), distinct_lines(179 ^ [], 177 ^ []), -(distinct_lines(179 ^ [], 179 ^ []))],extension(18 ^ 1,bind([[_43725, _43727, _43729], [179 ^ [], 177 ^ [], 179 ^ []]]))).
% 4.54/5.51 ncf('1.1.1',plain,[-(distinct_lines(179 ^ [], 177 ^ [])), distinct_lines(179 ^ [], parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ []))), -(distinct_lines(parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])), 177 ^ []))],extension(18 ^ 2,bind([[_43725, _43727, _43729], [177 ^ [], parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])), 179 ^ []]]))).
% 4.54/5.51 ncf('1.1.1.1',plain,[-(distinct_lines(179 ^ [], parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])))), distinct_lines(179 ^ [], parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ []))), -(distinct_lines(parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])), parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ []))))],extension(18 ^ 3,bind([[_43725, _43727, _43729], [parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])), parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])), 179 ^ []]]))).
% 4.54/5.51 ncf('1.1.1.1.1',plain,[-(distinct_lines(179 ^ [], parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])))), distinct_lines(179 ^ [], 178 ^ []), -(distinct_lines(178 ^ [], parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ []))))],extension(18 ^ 4,bind([[_43725, _43727, _43729], [parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])), 178 ^ [], 179 ^ []]]))).
% 4.54/5.51 ncf('1.1.1.1.1.1',plain,[-(distinct_lines(179 ^ [], 178 ^ [])), distinct_lines(179 ^ [], 178 ^ []), -(distinct_lines(178 ^ [], 178 ^ []))],extension(18 ^ 5,bind([[_43725, _43727, _43729], [178 ^ [], 178 ^ [], 179 ^ []]]))).
% 4.54/5.51 ncf('1.1.1.1.1.1.1',plain,[-(distinct_lines(179 ^ [], 178 ^ [])), convergent_lines(178 ^ [], 179 ^ []), -(convergent_lines(178 ^ [], 178 ^ []))],extension(104 ^ 6,bind([[_46512, _46514, _46516], [178 ^ [], 179 ^ [], 178 ^ []]]))).
% 4.54/5.51 ncf('1.1.1.1.1.1.1.1',plain,[-(convergent_lines(178 ^ [], 179 ^ [])), -(unorthogonal_lines(178 ^ [], 179 ^ []))],extension(132 ^ 7,bind([[_47462, _47464], [179 ^ [], 178 ^ []]]))).
% 4.54/5.51 ncf('1.1.1.1.1.1.1.1.1',plain,[unorthogonal_lines(178 ^ [], 179 ^ [])],extension(185 ^ 8)).
% 4.54/5.51 ncf('1.1.1.1.1.1.1.2',plain,[convergent_lines(178 ^ [], 178 ^ [])],extension(6 ^ 7,bind([[_43280], [178 ^ []]]))).
% 4.54/5.51 ncf('1.1.1.1.1.1.2',plain,[distinct_lines(178 ^ [], 178 ^ [])],extension(4 ^ 6,bind([[_43203], [178 ^ []]]))).
% 4.54/5.51 ncf('1.1.1.1.1.2',plain,[distinct_lines(178 ^ [], parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ []))), -(apart_point_and_line(intersection_point(178 ^ [], 179 ^ []), 178 ^ [])), -(apart_point_and_line(intersection_point(178 ^ [], 179 ^ []), parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])))), -(convergent_lines(178 ^ [], parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ []))))],extension(118 ^ 5,bind([[_47054, _47056, _47058], [parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])), 178 ^ [], intersection_point(178 ^ [], 179 ^ [])]]))).
% 4.54/5.51 ncf('1.1.1.1.1.2.1',plain,[apart_point_and_line(intersection_point(178 ^ [], 179 ^ []), 178 ^ []), convergent_lines(178 ^ [], 179 ^ [])],extension(50 ^ 6,bind([[_44793, _44795], [179 ^ [], 178 ^ []]]))).
% 4.54/5.51 ncf('1.1.1.1.1.2.1.1',plain,[-(convergent_lines(178 ^ [], 179 ^ [])), -(unorthogonal_lines(178 ^ [], 179 ^ []))],extension(132 ^ 7,bind([[_47462, _47464], [179 ^ [], 178 ^ []]]))).
% 4.54/5.51 ncf('1.1.1.1.1.2.1.1.1',plain,[unorthogonal_lines(178 ^ [], 179 ^ [])],extension(185 ^ 8)).
% 4.54/5.51 ncf('1.1.1.1.1.2.2',plain,[apart_point_and_line(intersection_point(178 ^ [], 179 ^ []), parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])))],extension(116 ^ 6,bind([[_46948, _46950], [178 ^ [], intersection_point(178 ^ [], 179 ^ [])]]))).
% 4.54/5.51 ncf('1.1.1.1.1.2.3',plain,[convergent_lines(178 ^ [], parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ []))), -(convergent_lines(178 ^ [], 178 ^ [])), -(convergent_lines(parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])), 178 ^ []))],extension(28 ^ 6,bind([[_44049, _44051, _44053], [178 ^ [], parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])), 178 ^ []]]))).
% 4.54/5.51 ncf('1.1.1.1.1.2.3.1',plain,[convergent_lines(178 ^ [], 178 ^ [])],extension(6 ^ 7,bind([[_43280], [178 ^ []]]))).
% 4.54/5.51 ncf('1.1.1.1.1.2.3.2',plain,[convergent_lines(parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])), 178 ^ [])],extension(114 ^ 7,bind([[_46852, _46854], [178 ^ [], intersection_point(178 ^ [], 179 ^ [])]]))).
% 4.54/5.51 ncf('1.1.1.1.2',plain,[distinct_lines(parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])), parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ []))), -(apart_point_and_line(intersection_point(178 ^ [], 179 ^ []), parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])))), -(apart_point_and_line(intersection_point(178 ^ [], 179 ^ []), parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])))), -(convergent_lines(parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])), parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ []))))],extension(118 ^ 4,bind([[_47054, _47056, _47058], [parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])), parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])), intersection_point(178 ^ [], 179 ^ [])]]))).
% 4.54/5.51 ncf('1.1.1.1.2.1',plain,[apart_point_and_line(intersection_point(178 ^ [], 179 ^ []), parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])))],extension(116 ^ 5,bind([[_46948, _46950], [178 ^ [], intersection_point(178 ^ [], 179 ^ [])]]))).
% 4.54/5.51 ncf('1.1.1.1.2.2',plain,[apart_point_and_line(intersection_point(178 ^ [], 179 ^ []), parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])))],extension(116 ^ 5,bind([[_46948, _46950], [178 ^ [], intersection_point(178 ^ [], 179 ^ [])]]))).
% 4.54/5.51 ncf('1.1.1.1.2.3',plain,[convergent_lines(parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])), parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ []))), unorthogonal_lines(parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])), parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ []))), 148 : -(convergent_lines(parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])), 178 ^ [])), 152 : -(convergent_lines(parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])), 178 ^ []))],extension(138 ^ 5,bind([[_47687, _47689, _47691], [178 ^ [], parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])), parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ []))]]))).
% 4.54/5.51 ncf('1.1.1.1.2.3.1',plain,[-(unorthogonal_lines(parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])), parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])))), distinct_lines(parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])), parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ []))), -(apart_point_and_line(intersection_point(178 ^ [], 179 ^ []), parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])))), -(apart_point_and_line(intersection_point(178 ^ [], 179 ^ []), parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])))), -(unorthogonal_lines(parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])), parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ []))))],extension(160 ^ 6,bind([[_48446, _48448, _48450, _48452], [parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])), parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])), parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])), intersection_point(178 ^ [], 179 ^ [])]]))).
% 4.54/5.51 ncf('1.1.1.1.2.3.1.1',plain,[-(distinct_lines(parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])), parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ []))))],reduction('1.1.1.1')).
% 4.54/5.51 ncf('1.1.1.1.2.3.1.2',plain,[apart_point_and_line(intersection_point(178 ^ [], 179 ^ []), parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])))],extension(116 ^ 7,bind([[_46948, _46950], [178 ^ [], intersection_point(178 ^ [], 179 ^ [])]]))).
% 4.54/5.51 ncf('1.1.1.1.2.3.1.3',plain,[apart_point_and_line(intersection_point(178 ^ [], 179 ^ []), parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])))],lemmata('[3, 2, 1, 1, 1, 1].x')).
% 4.54/5.51 ncf('1.1.1.1.2.3.1.4',plain,[unorthogonal_lines(parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])), parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])))],reduction('1.1.1.1.2.3')).
% 4.54/5.51 ncf('1.1.1.1.2.3.2',plain,[convergent_lines(parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])), 178 ^ [])],extension(114 ^ 8,bind([[_46852, _46854], [178 ^ [], intersection_point(178 ^ [], 179 ^ [])]]))).
% 4.54/5.51 ncf('1.1.1.1.2.3.3',plain,[convergent_lines(parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])), 178 ^ [])],extension(114 ^ 8,bind([[_46852, _46854], [178 ^ [], intersection_point(178 ^ [], 179 ^ [])]]))).
% 4.54/5.51 ncf('1.1.1.2',plain,[distinct_lines(parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])), 177 ^ []), -(apart_point_and_line(intersection_point(178 ^ [], 179 ^ []), parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])))), -(apart_point_and_line(intersection_point(178 ^ [], 179 ^ []), 177 ^ [])), -(convergent_lines(parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])), 177 ^ []))],extension(118 ^ 3,bind([[_47054, _47056, _47058], [177 ^ [], parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])), intersection_point(178 ^ [], 179 ^ [])]]))).
% 4.54/5.51 ncf('1.1.1.2.1',plain,[apart_point_and_line(intersection_point(178 ^ [], 179 ^ []), parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])))],extension(116 ^ 4,bind([[_46948, _46950], [178 ^ [], intersection_point(178 ^ [], 179 ^ [])]]))).
% 4.54/5.51 ncf('1.1.1.2.2',plain,[apart_point_and_line(intersection_point(178 ^ [], 179 ^ []), 177 ^ []), -(distinct_lines(177 ^ [], 179 ^ [])), -(apart_point_and_line(intersection_point(178 ^ [], 179 ^ []), 179 ^ []))],extension(94 ^ 4,bind([[_46208, _46210, _46212], [179 ^ [], 177 ^ [], intersection_point(178 ^ [], 179 ^ [])]]))).
% 4.54/5.51 ncf('1.1.1.2.2.1',plain,[distinct_lines(177 ^ [], 179 ^ [])],reduction('1')).
% 4.54/5.51 ncf('1.1.1.2.2.2',plain,[apart_point_and_line(intersection_point(178 ^ [], 179 ^ []), 179 ^ []), convergent_lines(178 ^ [], 179 ^ [])],extension(56 ^ 5,bind([[_45010, _45012], [179 ^ [], 178 ^ []]]))).
% 4.54/5.51 ncf('1.1.1.2.2.2.1',plain,[-(convergent_lines(178 ^ [], 179 ^ [])), -(unorthogonal_lines(178 ^ [], 179 ^ []))],extension(132 ^ 6,bind([[_47462, _47464], [179 ^ [], 178 ^ []]]))).
% 4.54/5.51 ncf('1.1.1.2.2.2.1.1',plain,[unorthogonal_lines(178 ^ [], 179 ^ [])],extension(185 ^ 7)).
% 4.54/5.51 ncf('1.1.1.2.3',plain,[convergent_lines(parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])), 177 ^ []), -(convergent_lines(parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])), 178 ^ [])), -(convergent_lines(177 ^ [], 178 ^ []))],extension(28 ^ 4,bind([[_44049, _44051, _44053], [178 ^ [], 177 ^ [], parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ []))]]))).
% 4.54/5.51 ncf('1.1.1.2.3.1',plain,[convergent_lines(parallel_through_point(178 ^ [], intersection_point(178 ^ [], 179 ^ [])), 178 ^ [])],extension(114 ^ 5,bind([[_46852, _46854], [178 ^ [], intersection_point(178 ^ [], 179 ^ [])]]))).
% 4.54/5.51 ncf('1.1.1.2.3.2',plain,[convergent_lines(177 ^ [], 178 ^ []), -(convergent_lines(177 ^ [], 177 ^ [])), -(convergent_lines(178 ^ [], 177 ^ []))],extension(28 ^ 5,bind([[_44049, _44051, _44053], [177 ^ [], 178 ^ [], 177 ^ []]]))).
% 4.54/5.51 ncf('1.1.1.2.3.2.1',plain,[convergent_lines(177 ^ [], 177 ^ [])],extension(6 ^ 6,bind([[_43280], [177 ^ []]]))).
% 4.54/5.51 ncf('1.1.1.2.3.2.2',plain,[convergent_lines(178 ^ [], 177 ^ []), unorthogonal_lines(178 ^ [], 177 ^ []), 150 : -(unorthogonal_lines(178 ^ [], 179 ^ [])), 152 : -(convergent_lines(177 ^ [], 179 ^ []))],extension(138 ^ 6,bind([[_47687, _47689, _47691], [179 ^ [], 177 ^ [], 178 ^ []]]))).
% 4.54/5.51 ncf('1.1.1.2.3.2.2.1',plain,[-(unorthogonal_lines(178 ^ [], 177 ^ [])), convergent_lines(177 ^ [], 178 ^ []), unorthogonal_lines(177 ^ [], 178 ^ []), 148 : -(convergent_lines(177 ^ [], 177 ^ []))],extension(138 ^ 7,bind([[_47687, _47689, _47691], [177 ^ [], 178 ^ [], 177 ^ []]]))).
% 4.54/5.51 ncf('1.1.1.2.3.2.2.1.1',plain,[-(convergent_lines(177 ^ [], 178 ^ []))],reduction('1.1.1.2.3')).
% 4.54/5.51 ncf('1.1.1.2.3.2.2.1.2',plain,[-(unorthogonal_lines(177 ^ [], 178 ^ []))],extension(181 ^ 8)).
% 4.54/5.51 ncf('1.1.1.2.3.2.2.1.3',plain,[convergent_lines(177 ^ [], 177 ^ [])],lemmata('[3, 2, 1, 1, 1].x')).
% 4.54/5.51 ncf('1.1.1.2.3.2.2.2',plain,[unorthogonal_lines(178 ^ [], 179 ^ [])],extension(185 ^ 9)).
% 4.54/5.51 ncf('1.1.1.2.3.2.2.3',plain,[convergent_lines(177 ^ [], 179 ^ []), -(distinct_lines(179 ^ [], 177 ^ [])), -(convergent_lines(177 ^ [], 177 ^ []))],extension(104 ^ 9,bind([[_46512, _46514, _46516], [177 ^ [], 179 ^ [], 177 ^ []]]))).
% 4.54/5.51 ncf('1.1.1.2.3.2.2.3.1',plain,[distinct_lines(179 ^ [], 177 ^ [])],reduction('1.1')).
% 4.54/5.51 ncf('1.1.1.2.3.2.2.3.2',plain,[convergent_lines(177 ^ [], 177 ^ [])],lemmata('[3, 2, 1, 1, 1].x')).
% 4.54/5.51 ncf('1.1.2',plain,[distinct_lines(179 ^ [], 179 ^ []), -(apart_point_and_line(intersection_point(179 ^ [], 179 ^ []), 179 ^ [])), -(apart_point_and_line(intersection_point(179 ^ [], 179 ^ []), 179 ^ [])), -(convergent_lines(179 ^ [], 179 ^ []))],extension(118 ^ 2,bind([[_47054, _47056, _47058], [179 ^ [], 179 ^ [], intersection_point(179 ^ [], 179 ^ [])]]))).
% 4.54/5.51 ncf('1.1.2.1',plain,[apart_point_and_line(intersection_point(179 ^ [], 179 ^ []), 179 ^ []), convergent_lines(179 ^ [], 179 ^ [])],extension(50 ^ 3,bind([[_44793, _44795], [179 ^ [], 179 ^ []]]))).
% 4.54/5.51 ncf('1.1.2.1.1',plain,[-(convergent_lines(179 ^ [], 179 ^ [])), distinct_lines(179 ^ [], 179 ^ []), -(apart_point_and_line(intersection_point(179 ^ [], 178 ^ []), 179 ^ [])), -(apart_point_and_line(intersection_point(179 ^ [], 178 ^ []), 179 ^ []))],extension(118 ^ 4,bind([[_47054, _47056, _47058], [179 ^ [], 179 ^ [], intersection_point(179 ^ [], 178 ^ [])]]))).
% 4.54/5.51 ncf('1.1.2.1.1.1',plain,[-(distinct_lines(179 ^ [], 179 ^ []))],reduction('1.1')).
% 4.54/5.51 ncf('1.1.2.1.1.2',plain,[apart_point_and_line(intersection_point(179 ^ [], 178 ^ []), 179 ^ []), convergent_lines(179 ^ [], 178 ^ [])],extension(50 ^ 5,bind([[_44793, _44795], [178 ^ [], 179 ^ []]]))).
% 4.54/5.51 ncf('1.1.2.1.1.2.1',plain,[-(convergent_lines(179 ^ [], 178 ^ [])), convergent_lines(178 ^ [], 179 ^ []), -(convergent_lines(178 ^ [], 178 ^ []))],extension(28 ^ 6,bind([[_44049, _44051, _44053], [178 ^ [], 179 ^ [], 178 ^ []]]))).
% 4.54/5.51 ncf('1.1.2.1.1.2.1.1',plain,[-(convergent_lines(178 ^ [], 179 ^ [])), -(unorthogonal_lines(178 ^ [], 179 ^ []))],extension(132 ^ 7,bind([[_47462, _47464], [179 ^ [], 178 ^ []]]))).
% 4.54/5.51 ncf('1.1.2.1.1.2.1.1.1',plain,[unorthogonal_lines(178 ^ [], 179 ^ [])],extension(185 ^ 8)).
% 4.54/5.51 ncf('1.1.2.1.1.2.1.2',plain,[convergent_lines(178 ^ [], 178 ^ [])],extension(6 ^ 7,bind([[_43280], [178 ^ []]]))).
% 4.54/5.51 ncf('1.1.2.1.1.3',plain,[apart_point_and_line(intersection_point(179 ^ [], 178 ^ []), 179 ^ [])],lemmata('[1, 2, 1, 1].x')).
% 4.54/5.51 ncf('1.1.2.2',plain,[apart_point_and_line(intersection_point(179 ^ [], 179 ^ []), 179 ^ [])],lemmata('[1, 1].x')).
% 4.54/5.51 ncf('1.1.2.3',plain,[convergent_lines(179 ^ [], 179 ^ []), unorthogonal_lines(179 ^ [], 179 ^ []), 148 : -(convergent_lines(179 ^ [], parallel_through_point(parallel_through_point(179 ^ [], _32606), _32743))), 152 : -(convergent_lines(179 ^ [], parallel_through_point(parallel_through_point(179 ^ [], _32606), _32743)))],extension(138 ^ 3,bind([[_47687, _47689, _47691], [parallel_through_point(parallel_through_point(179 ^ [], _32606), _32743), 179 ^ [], 179 ^ []]]))).
% 4.54/5.51 ncf('1.1.2.3.1',plain,[-(unorthogonal_lines(179 ^ [], 179 ^ [])), distinct_lines(179 ^ [], 179 ^ []), -(apart_point_and_line(intersection_point(179 ^ [], 179 ^ []), 179 ^ [])), -(apart_point_and_line(intersection_point(179 ^ [], 179 ^ []), 179 ^ [])), -(unorthogonal_lines(179 ^ [], 179 ^ []))],extension(160 ^ 4,bind([[_48446, _48448, _48450, _48452], [179 ^ [], 179 ^ [], 179 ^ [], intersection_point(179 ^ [], 179 ^ [])]]))).
% 4.54/5.51 ncf('1.1.2.3.1.1',plain,[-(distinct_lines(179 ^ [], 179 ^ []))],reduction('1.1')).
% 4.54/5.51 ncf('1.1.2.3.1.2',plain,[apart_point_and_line(intersection_point(179 ^ [], 179 ^ []), 179 ^ []), convergent_lines(179 ^ [], 179 ^ [])],extension(50 ^ 5,bind([[_44793, _44795], [179 ^ [], 179 ^ []]]))).
% 4.54/5.51 ncf('1.1.2.3.1.2.1',plain,[-(convergent_lines(179 ^ [], 179 ^ []))],reduction('1.1.2')).
% 4.54/5.51 ncf('1.1.2.3.1.3',plain,[apart_point_and_line(intersection_point(179 ^ [], 179 ^ []), 179 ^ [])],lemmata('[3, 2, 1, 1].x')).
% 4.54/5.51 ncf('1.1.2.3.1.4',plain,[unorthogonal_lines(179 ^ [], 179 ^ [])],reduction('1.1.2.3')).
% 4.54/5.51 ncf('1.1.2.3.2',plain,[convergent_lines(179 ^ [], parallel_through_point(parallel_through_point(179 ^ [], _32606), _32743)), unorthogonal_lines(179 ^ [], parallel_through_point(parallel_through_point(179 ^ [], _32606), _32743)), 148 : -(convergent_lines(179 ^ [], parallel_through_point(179 ^ [], _32606))), 152 : -(convergent_lines(parallel_through_point(parallel_through_point(179 ^ [], _32606), _32743), parallel_through_point(179 ^ [], _32606)))],extension(138 ^ 6,bind([[_47687, _47689, _47691], [parallel_through_point(179 ^ [], _32606), parallel_through_point(parallel_through_point(179 ^ [], _32606), _32743), 179 ^ []]]))).
% 4.54/5.51 ncf('1.1.2.3.2.1',plain,[-(unorthogonal_lines(179 ^ [], parallel_through_point(parallel_through_point(179 ^ [], _32606), _32743))), distinct_lines(179 ^ [], 179 ^ []), -(apart_point_and_line(intersection_point(179 ^ [], parallel_through_point(parallel_through_point(179 ^ [], _32606), _32743)), 179 ^ [])), -(apart_point_and_line(intersection_point(179 ^ [], parallel_through_point(parallel_through_point(179 ^ [], _32606), _32743)), 179 ^ [])), -(unorthogonal_lines(179 ^ [], parallel_through_point(parallel_through_point(179 ^ [], _32606), _32743)))],extension(160 ^ 7,bind([[_48446, _48448, _48450, _48452], [parallel_through_point(parallel_through_point(179 ^ [], _32606), _32743), 179 ^ [], 179 ^ [], intersection_point(179 ^ [], parallel_through_point(parallel_through_point(179 ^ [], _32606), _32743))]]))).
% 4.54/5.51 ncf('1.1.2.3.2.1.1',plain,[-(distinct_lines(179 ^ [], 179 ^ []))],reduction('1.1')).
% 4.54/5.51 ncf('1.1.2.3.2.1.2',plain,[apart_point_and_line(intersection_point(179 ^ [], parallel_through_point(parallel_through_point(179 ^ [], _32606), _32743)), 179 ^ []), convergent_lines(179 ^ [], parallel_through_point(parallel_through_point(179 ^ [], _32606), _32743))],extension(50 ^ 8,bind([[_44793, _44795], [parallel_through_point(parallel_through_point(179 ^ [], _32606), _32743), 179 ^ []]]))).
% 4.54/5.51 ncf('1.1.2.3.2.1.2.1',plain,[-(convergent_lines(179 ^ [], parallel_through_point(parallel_through_point(179 ^ [], _32606), _32743)))],reduction('1.1.2.3')).
% 4.54/5.51 ncf('1.1.2.3.2.1.3',plain,[apart_point_and_line(intersection_point(179 ^ [], parallel_through_point(parallel_through_point(179 ^ [], _32606), _32743)), 179 ^ [])],lemmata('[2, 3, 2, 1, 1].x')).
% 4.54/5.51 ncf('1.1.2.3.2.1.4',plain,[unorthogonal_lines(179 ^ [], parallel_through_point(parallel_through_point(179 ^ [], _32606), _32743))],reduction('1.1.2.3.2')).
% 4.54/5.51 ncf('1.1.2.3.2.2',plain,[convergent_lines(179 ^ [], parallel_through_point(179 ^ [], _32606)), unorthogonal_lines(179 ^ [], parallel_through_point(179 ^ [], _32606)), 148 : -(convergent_lines(179 ^ [], 179 ^ [])), 152 : -(convergent_lines(parallel_through_point(179 ^ [], _32606), 179 ^ []))],extension(138 ^ 9,bind([[_47687, _47689, _47691], [179 ^ [], parallel_through_point(179 ^ [], _32606), 179 ^ []]]))).
% 4.54/5.51 ncf('1.1.2.3.2.2.1',plain,[-(unorthogonal_lines(179 ^ [], parallel_through_point(179 ^ [], _32606))), distinct_lines(179 ^ [], 179 ^ []), -(apart_point_and_line(intersection_point(179 ^ [], parallel_through_point(179 ^ [], _32606)), 179 ^ [])), -(apart_point_and_line(intersection_point(179 ^ [], parallel_through_point(179 ^ [], _32606)), 179 ^ [])), -(unorthogonal_lines(179 ^ [], parallel_through_point(179 ^ [], _32606)))],extension(160 ^ 10,bind([[_48446, _48448, _48450, _48452], [parallel_through_point(179 ^ [], _32606), 179 ^ [], 179 ^ [], intersection_point(179 ^ [], parallel_through_point(179 ^ [], _32606))]]))).
% 4.54/5.51 ncf('1.1.2.3.2.2.1.1',plain,[-(distinct_lines(179 ^ [], 179 ^ []))],reduction('1.1')).
% 4.54/5.51 ncf('1.1.2.3.2.2.1.2',plain,[apart_point_and_line(intersection_point(179 ^ [], parallel_through_point(179 ^ [], _32606)), 179 ^ []), convergent_lines(179 ^ [], parallel_through_point(179 ^ [], _32606))],extension(50 ^ 11,bind([[_44793, _44795], [parallel_through_point(179 ^ [], _32606), 179 ^ []]]))).
% 4.54/5.51 ncf('1.1.2.3.2.2.1.2.1',plain,[-(convergent_lines(179 ^ [], parallel_through_point(179 ^ [], _32606)))],reduction('1.1.2.3.2')).
% 4.54/5.51 ncf('1.1.2.3.2.2.1.3',plain,[apart_point_and_line(intersection_point(179 ^ [], parallel_through_point(179 ^ [], _32606)), 179 ^ [])],lemmata('[2, 2, 3, 2, 1, 1].x')).
% 4.54/5.51 ncf('1.1.2.3.2.2.1.4',plain,[unorthogonal_lines(179 ^ [], parallel_through_point(179 ^ [], _32606))],reduction('1.1.2.3.2.2')).
% 4.54/5.51 ncf('1.1.2.3.2.2.2',plain,[convergent_lines(179 ^ [], 179 ^ [])],extension(6 ^ 12,bind([[_43280], [179 ^ []]]))).
% 4.54/5.51 ncf('1.1.2.3.2.2.3',plain,[convergent_lines(parallel_through_point(179 ^ [], _32606), 179 ^ [])],extension(114 ^ 12,bind([[_46852, _46854], [179 ^ [], _32606]]))).
% 4.54/5.51 ncf('1.1.2.3.2.3',plain,[convergent_lines(parallel_through_point(parallel_through_point(179 ^ [], _32606), _32743), parallel_through_point(179 ^ [], _32606))],extension(114 ^ 9,bind([[_46852, _46854], [parallel_through_point(179 ^ [], _32606), _32743]]))).
% 4.54/5.51 ncf('1.1.2.3.3',plain,[convergent_lines(179 ^ [], parallel_through_point(parallel_through_point(179 ^ [], _32606), _32743)), unorthogonal_lines(179 ^ [], parallel_through_point(parallel_through_point(179 ^ [], _32606), _32743)), 148 : -(convergent_lines(179 ^ [], parallel_through_point(179 ^ [], _32606))), 152 : -(convergent_lines(parallel_through_point(parallel_through_point(179 ^ [], _32606), _32743), parallel_through_point(179 ^ [], _32606)))],extension(138 ^ 6,bind([[_47687, _47689, _47691], [parallel_through_point(179 ^ [], _32606), parallel_through_point(parallel_through_point(179 ^ [], _32606), _32743), 179 ^ []]]))).
% 4.54/5.51 ncf('1.1.2.3.3.1',plain,[-(unorthogonal_lines(179 ^ [], parallel_through_point(parallel_through_point(179 ^ [], _32606), _32743))), convergent_lines(179 ^ [], 179 ^ []), unorthogonal_lines(179 ^ [], 179 ^ []), 150 : -(unorthogonal_lines(179 ^ [], parallel_through_point(parallel_through_point(179 ^ [], _32606), _32743)))],extension(138 ^ 7,bind([[_47687, _47689, _47691], [parallel_through_point(parallel_through_point(179 ^ [], _32606), _32743), 179 ^ [], 179 ^ []]]))).
% 4.54/5.51 ncf('1.1.2.3.3.1.1',plain,[-(convergent_lines(179 ^ [], 179 ^ []))],reduction('1.1.2')).
% 4.54/5.51 ncf('1.1.2.3.3.1.2',plain,[-(unorthogonal_lines(179 ^ [], 179 ^ []))],lemmata('[2, 1, 1].x')).
% 4.54/5.51 ncf('1.1.2.3.3.1.3',plain,[unorthogonal_lines(179 ^ [], parallel_through_point(parallel_through_point(179 ^ [], _32606), _32743))],reduction('1.1.2.3.3')).
% 4.54/5.51 ncf('1.1.2.3.3.2',plain,[convergent_lines(179 ^ [], parallel_through_point(179 ^ [], _32606)), unorthogonal_lines(179 ^ [], parallel_through_point(179 ^ [], _32606)), 148 : -(convergent_lines(179 ^ [], 179 ^ [])), 152 : -(convergent_lines(parallel_through_point(179 ^ [], _32606), 179 ^ []))],extension(138 ^ 9,bind([[_47687, _47689, _47691], [179 ^ [], parallel_through_point(179 ^ [], _32606), 179 ^ []]]))).
% 4.54/5.51 ncf('1.1.2.3.3.2.1',plain,[-(unorthogonal_lines(179 ^ [], parallel_through_point(179 ^ [], _32606))), distinct_lines(179 ^ [], 179 ^ []), -(apart_point_and_line(intersection_point(179 ^ [], parallel_through_point(179 ^ [], _32606)), 179 ^ [])), -(apart_point_and_line(intersection_point(179 ^ [], parallel_through_point(179 ^ [], _32606)), 179 ^ [])), -(unorthogonal_lines(179 ^ [], parallel_through_point(179 ^ [], _32606)))],extension(160 ^ 10,bind([[_48446, _48448, _48450, _48452], [parallel_through_point(179 ^ [], _32606), 179 ^ [], 179 ^ [], intersection_point(179 ^ [], parallel_through_point(179 ^ [], _32606))]]))).
% 4.54/5.51 ncf('1.1.2.3.3.2.1.1',plain,[-(distinct_lines(179 ^ [], 179 ^ []))],reduction('1.1')).
% 4.54/5.51 ncf('1.1.2.3.3.2.1.2',plain,[apart_point_and_line(intersection_point(179 ^ [], parallel_through_point(179 ^ [], _32606)), 179 ^ []), convergent_lines(179 ^ [], parallel_through_point(179 ^ [], _32606))],extension(50 ^ 11,bind([[_44793, _44795], [parallel_through_point(179 ^ [], _32606), 179 ^ []]]))).
% 4.54/5.51 ncf('1.1.2.3.3.2.1.2.1',plain,[-(convergent_lines(179 ^ [], parallel_through_point(179 ^ [], _32606)))],reduction('1.1.2.3.3')).
% 4.54/5.51 ncf('1.1.2.3.3.2.1.3',plain,[apart_point_and_line(intersection_point(179 ^ [], parallel_through_point(179 ^ [], _32606)), 179 ^ [])],lemmata('[2, 3, 3, 2, 1, 1].x')).
% 4.54/5.51 ncf('1.1.2.3.3.2.1.4',plain,[unorthogonal_lines(179 ^ [], parallel_through_point(179 ^ [], _32606))],reduction('1.1.2.3.3.2')).
% 4.54/5.51 ncf('1.1.2.3.3.2.2',plain,[convergent_lines(179 ^ [], 179 ^ [])],extension(6 ^ 12,bind([[_43280], [179 ^ []]]))).
% 4.54/5.51 ncf('1.1.2.3.3.2.3',plain,[convergent_lines(parallel_through_point(179 ^ [], _32606), 179 ^ [])],extension(114 ^ 12,bind([[_46852, _46854], [179 ^ [], _32606]]))).
% 4.54/5.51 ncf('1.1.2.3.3.3',plain,[convergent_lines(parallel_through_point(parallel_through_point(179 ^ [], _32606), _32743), parallel_through_point(179 ^ [], _32606))],extension(114 ^ 9,bind([[_46852, _46854], [parallel_through_point(179 ^ [], _32606), _32743]]))).
% 4.54/5.51 %-----------------------------------------------------
% 4.54/5.51 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------