%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO223+3 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n010.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:17 EDT 2023
% Result : Theorem 13.58s 13.85s
% Output : Proof 13.58s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GEO223+3 : TPTP v8.1.2. Released v4.0.0.
% 0.03/0.13 % Command : nanocop.sh %s %d
% 0.12/0.34 % Computer : n010.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:28:42 EDT 2023
% 0.12/0.34 % CPUTime :
% 13.58/13.85
% 13.58/13.85 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 13.58/13.85 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.58/13.85 %-----------------------------------------------------
% 13.58/13.85 ncf(matrix, plain, [(328 ^ _58509) ^ [] : [equal_lines(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []))], (2 ^ _58509) ^ [_58612] : [distinct_points(_58612, _58612)], (4 ^ _58509) ^ [_58689] : [distinct_lines(_58689, _58689)], (6 ^ _58509) ^ [_58766] : [convergent_lines(_58766, _58766)], (8 ^ _58509) ^ [_58887, _58889, _58891] : [distinct_points(_58891, _58889), -(distinct_points(_58891, _58887)), -(distinct_points(_58889, _58887))], (18 ^ _58509) ^ [_59211, _59213, _59215] : [distinct_lines(_59215, _59213), -(distinct_lines(_59215, _59211)), -(distinct_lines(_59213, _59211))], (28 ^ _58509) ^ [_59535, _59537, _59539] : [convergent_lines(_59539, _59537), -(convergent_lines(_59539, _59535)), -(convergent_lines(_59537, _59535))], (38 ^ _58509) ^ [_59845, _59847] : [distinct_points(_59847, _59845), apart_point_and_line(_59847, line_connecting(_59847, _59845))], (44 ^ _58509) ^ [_60062, _60064] : [distinct_points(_60064, _60062), apart_point_and_line(_60062, line_connecting(_60064, _60062))], (50 ^ _58509) ^ [_60279, _60281] : [convergent_lines(_60281, _60279), apart_point_and_line(intersection_point(_60281, _60279), _60281)], (56 ^ _58509) ^ [_60496, _60498] : [convergent_lines(_60498, _60496), apart_point_and_line(intersection_point(_60498, _60496), _60496)], (62 ^ _58509) ^ [_60741, _60743, _60745, _60747] : [distinct_points(_60747, _60745), distinct_lines(_60743, _60741), -(apart_point_and_line(_60747, _60743)), -(apart_point_and_line(_60747, _60741)), -(apart_point_and_line(_60745, _60743)), -(apart_point_and_line(_60745, _60741))], (84 ^ _58509) ^ [_61370, _61372, _61374] : [apart_point_and_line(_61374, _61372), -(distinct_points(_61374, _61370)), -(apart_point_and_line(_61370, _61372))], (94 ^ _58509) ^ [_61694, _61696, _61698] : [apart_point_and_line(_61698, _61696), -(distinct_lines(_61696, _61694)), -(apart_point_and_line(_61698, _61694))], (104 ^ _58509) ^ [_61998, _62000, _62002] : [convergent_lines(_62002, _62000), -(distinct_lines(_62000, _61998)), -(convergent_lines(_62002, _61998))], (114 ^ _58509) ^ [_62334, _62336] : [distinct_lines(_62336, _62334), -(convergent_lines(_62336, _62334))], (120 ^ _58509) ^ [_62548, _62550] : [convergent_lines(parallel_through_point(_62548, _62550), _62548)], (122 ^ _58509) ^ [_62644, _62646] : [apart_point_and_line(_62646, parallel_through_point(_62644, _62646))], (124 ^ _58509) ^ [_62750, _62752, _62754] : [distinct_lines(_62752, _62750), -(apart_point_and_line(_62754, _62752)), -(apart_point_and_line(_62754, _62750)), -(convergent_lines(_62752, _62750))], (138 ^ _58509) ^ [_63178, _63180] : [-(convergent_lines(_63180, _63178)), -(unorthogonal_lines(_63180, _63178))], (144 ^ _58509) ^ [_63403, _63405, _63407] : [convergent_lines(_63407, _63405), unorthogonal_lines(_63407, _63405), 153 ^ _58509 : [(154 ^ _58509) ^ [] : [-(convergent_lines(_63407, _63403))], (156 ^ _58509) ^ [] : [-(unorthogonal_lines(_63407, _63403))]], 157 ^ _58509 : [(158 ^ _58509) ^ [] : [-(convergent_lines(_63405, _63403))], (160 ^ _58509) ^ [] : [-(unorthogonal_lines(_63405, _63403))]]], (162 ^ _58509) ^ [_63946, _63948] : [unorthogonal_lines(orthogonal_through_point(_63946, _63948), _63946)], (164 ^ _58509) ^ [_64042, _64044] : [apart_point_and_line(_64044, orthogonal_through_point(_64042, _64044))], (166 ^ _58509) ^ [_64162, _64164, _64166, _64168] : [distinct_lines(_64166, _64164), -(apart_point_and_line(_64168, _64166)), -(apart_point_and_line(_64168, _64164)), -(unorthogonal_lines(_64166, _64162)), -(unorthogonal_lines(_64164, _64162))], (184 ^ _58509) ^ [_64706, _64708] : [-(convergent_lines(_64708, _64706)), -(unorthogonal_lines(_64708, _64706))], (208 ^ _58509) ^ [_65500, _65502, _65504] : [convergent_lines(_65502, _65500), -(unorthogonal_lines(_65504, _65502)), -(unorthogonal_lines(_65504, _65500))], (190 ^ _58509) ^ [_64935, _64937, _64939] : [193 ^ _58509 : [(194 ^ _58509) ^ [] : [-(convergent_lines(_64939, _64937))], (196 ^ _58509) ^ [] : [-(unorthogonal_lines(_64939, _64937))]], 197 ^ _58509 : [(198 ^ _58509) ^ [] : [-(convergent_lines(_64939, _64935))], (200 ^ _58509) ^ [] : [-(unorthogonal_lines(_64939, _64935))]], convergent_lines(_64937, _64935), unorthogonal_lines(_64937, _64935)], (218 ^ _58509) ^ [_65840, _65842] : [-(line(line_connecting(_65842, _65840))), point(_65842), point(_65840), distinct_points(_65842, _65840)], (232 ^ _58509) ^ [_66228, _66230] : [-(point(intersection_point(_66230, _66228))), line(_66230), line(_66228), convergent_lines(_66230, _66228)], (246 ^ _58509) ^ [_66616, _66618] : [-(line(parallel_through_point(_66618, _66616))), line(_66618), point(_66616)], (256 ^ _58509) ^ [_66895, _66897] : [-(line(orthogonal_through_point(_66897, _66895))), line(_66897), point(_66895)], (266 ^ _58509) ^ [_67229, _67231] : [equal_points(_67231, _67229), distinct_points(_67231, _67229)], (272 ^ _58509) ^ [_67392, _67394] : [-(distinct_points(_67394, _67392)), -(equal_points(_67394, _67392))], (278 ^ _58509) ^ [_67636, _67638] : [equal_lines(_67638, _67636), distinct_lines(_67638, _67636)], (284 ^ _58509) ^ [_67799, _67801] : [-(distinct_lines(_67801, _67799)), -(equal_lines(_67801, _67799))], (290 ^ _58509) ^ [_68043, _68045] : [parallel_lines(_68045, _68043), convergent_lines(_68045, _68043)], (296 ^ _58509) ^ [_68206, _68208] : [-(convergent_lines(_68208, _68206)), -(parallel_lines(_68208, _68206))], (302 ^ _58509) ^ [_68450, _68452] : [incident_point_and_line(_68452, _68450), apart_point_and_line(_68452, _68450)], (308 ^ _58509) ^ [_68613, _68615] : [-(apart_point_and_line(_68615, _68613)), -(incident_point_and_line(_68615, _68613))], (314 ^ _58509) ^ [_68837, _68839] : [orthogonal_lines(_68839, _68837), unorthogonal_lines(_68839, _68837)], (320 ^ _58509) ^ [_69000, _69002] : [-(unorthogonal_lines(_69002, _69000)), -(orthogonal_lines(_69002, _69000))]], input).
% 13.58/13.85 ncf('1',plain,[convergent_lines(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ [])), apart_point_and_line(intersection_point(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ [])), parallel_through_point(326 ^ [], 325 ^ []))],start(50 ^ 0,bind([[_60279, _60281], [orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), parallel_through_point(326 ^ [], 325 ^ [])]]))).
% 13.58/13.85 ncf('1.1',plain,[-(convergent_lines(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []))), convergent_lines(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ [])), -(convergent_lines(orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ [])))],extension(28 ^ 1,bind([[_59535, _59537, _59539], [orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), parallel_through_point(326 ^ [], 325 ^ [])]]))).
% 13.58/13.85 ncf('1.1.1',plain,[-(convergent_lines(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []))), convergent_lines(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ [])), -(convergent_lines(orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ [])))],extension(28 ^ 2,bind([[_59535, _59537, _59539], [orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), parallel_through_point(326 ^ [], 325 ^ [])]]))).
% 13.58/13.85 ncf('1.1.1.1',plain,[-(convergent_lines(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []))), convergent_lines(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ [])), -(convergent_lines(orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ [])))],extension(28 ^ 3,bind([[_59535, _59537, _59539], [orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), parallel_through_point(326 ^ [], 325 ^ [])]]))).
% 13.58/13.85 ncf('1.1.1.1.1',plain,[-(convergent_lines(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []))), convergent_lines(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ [])), -(convergent_lines(orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ [])))],extension(28 ^ 4,bind([[_59535, _59537, _59539], [orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), parallel_through_point(326 ^ [], 325 ^ [])]]))).
% 13.58/13.85 ncf('1.1.1.1.1.1',plain,[-(convergent_lines(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []))), distinct_lines(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []))],extension(114 ^ 5,bind([[_62334, _62336], [orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), parallel_through_point(326 ^ [], 325 ^ [])]]))).
% 13.58/13.85 ncf('1.1.1.1.1.1.1',plain,[-(distinct_lines(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []))), -(equal_lines(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ [])))],extension(284 ^ 6,bind([[_67799, _67801], [orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), parallel_through_point(326 ^ [], 325 ^ [])]]))).
% 13.58/13.85 ncf('1.1.1.1.1.1.1.1',plain,[equal_lines(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []))],extension(328 ^ 7)).
% 13.58/13.85 ncf('1.1.1.1.1.2',plain,[convergent_lines(orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []))],extension(6 ^ 5,bind([[_58766], [orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ [])]]))).
% 13.58/13.85 ncf('1.1.1.1.2',plain,[convergent_lines(orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []))],extension(6 ^ 4,bind([[_58766], [orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ [])]]))).
% 13.58/13.85 ncf('1.1.1.2',plain,[convergent_lines(orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []))],extension(6 ^ 3,bind([[_58766], [orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ [])]]))).
% 13.58/13.85 ncf('1.1.2',plain,[convergent_lines(orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []))],extension(6 ^ 2,bind([[_58766], [orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ [])]]))).
% 13.58/13.85 ncf('1.2',plain,[-(apart_point_and_line(intersection_point(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ [])), parallel_through_point(326 ^ [], 325 ^ []))), distinct_lines(orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), parallel_through_point(326 ^ [], 325 ^ [])), -(apart_point_and_line(intersection_point(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ [])), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []))), -(unorthogonal_lines(orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ []))), -(unorthogonal_lines(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ [])))],extension(166 ^ 1,bind([[_64162, _64164, _64166, _64168], [orthogonal_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), intersection_point(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []))]]))).
% 13.58/13.85 ncf('1.2.1',plain,[-(distinct_lines(orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), parallel_through_point(326 ^ [], 325 ^ []))), distinct_lines(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ [])), -(distinct_lines(parallel_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ [])))],extension(18 ^ 2,bind([[_59211, _59213, _59215], [parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), parallel_through_point(326 ^ [], 325 ^ [])]]))).
% 13.58/13.85 ncf('1.2.1.1',plain,[-(distinct_lines(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []))), distinct_lines(parallel_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ [])), -(distinct_lines(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ [])))],extension(18 ^ 3,bind([[_59211, _59213, _59215], [orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), parallel_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ [])]]))).
% 13.58/13.85 ncf('1.2.1.1.1',plain,[-(distinct_lines(parallel_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ []))), distinct_lines(parallel_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ [])), -(distinct_lines(parallel_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ [])))],extension(18 ^ 4,bind([[_59211, _59213, _59215], [parallel_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ [])]]))).
% 13.58/13.85 ncf('1.2.1.1.1.1',plain,[-(distinct_lines(parallel_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ []))), distinct_lines(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ [])), -(distinct_lines(orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), parallel_through_point(326 ^ [], 325 ^ [])))],extension(18 ^ 5,bind([[_59211, _59213, _59215], [parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), parallel_through_point(326 ^ [], 325 ^ [])]]))).
% 13.58/13.85 ncf('1.2.1.1.1.1.1',plain,[-(distinct_lines(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []))), -(equal_lines(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ [])))],extension(284 ^ 6,bind([[_67799, _67801], [orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), parallel_through_point(326 ^ [], 325 ^ [])]]))).
% 13.58/13.85 ncf('1.2.1.1.1.1.1.1',plain,[equal_lines(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []))],extension(328 ^ 7)).
% 13.58/13.85 ncf('1.2.1.1.1.1.2',plain,[distinct_lines(orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), parallel_through_point(326 ^ [], 325 ^ []))],reduction('1.2')).
% 13.58/13.85 ncf('1.2.1.1.1.2',plain,[distinct_lines(parallel_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ []))],reduction('1.2.1.1')).
% 13.58/13.85 ncf('1.2.1.1.2',plain,[distinct_lines(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []))],reduction('1.2.1')).
% 13.58/13.85 ncf('1.2.1.2',plain,[distinct_lines(parallel_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ []))],extension(4 ^ 3,bind([[_58689], [parallel_through_point(326 ^ [], 325 ^ [])]]))).
% 13.58/13.85 ncf('1.2.2',plain,[apart_point_and_line(intersection_point(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ [])), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ [])), convergent_lines(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []))],extension(56 ^ 2,bind([[_60496, _60498], [orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), parallel_through_point(326 ^ [], 325 ^ [])]]))).
% 13.58/13.85 ncf('1.2.2.1',plain,[-(convergent_lines(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ [])))],lemmata('x')).
% 13.58/13.85 ncf('1.2.3',plain,[unorthogonal_lines(orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ [])), convergent_lines(orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ [])), 154 : -(convergent_lines(orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []))), 158 : -(convergent_lines(orthogonal_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ [])))],extension(144 ^ 2,bind([[_63403, _63405, _63407], [orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ [])]]))).
% 13.58/13.85 ncf('1.2.3.1',plain,[-(convergent_lines(orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ []))), convergent_lines(orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ [])), -(convergent_lines(orthogonal_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ [])))],extension(28 ^ 3,bind([[_59535, _59537, _59539], [orthogonal_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ [])]]))).
% 13.58/13.85 ncf('1.2.3.1.1',plain,[-(convergent_lines(orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ []))), convergent_lines(orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ [])), -(convergent_lines(orthogonal_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ [])))],extension(28 ^ 4,bind([[_59535, _59537, _59539], [orthogonal_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ [])]]))).
% 13.58/13.85 ncf('1.2.3.1.1.1',plain,[-(convergent_lines(orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ []))), -(unorthogonal_lines(orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ [])))],extension(138 ^ 5,bind([[_63178, _63180], [orthogonal_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ [])]]))).
% 13.58/13.85 ncf('1.2.3.1.1.1.1',plain,[unorthogonal_lines(orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ []))],extension(162 ^ 6,bind([[_63946, _63948], [orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []]]))).
% 13.58/13.85 ncf('1.2.3.1.1.2',plain,[convergent_lines(orthogonal_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ []))],extension(6 ^ 5,bind([[_58766], [orthogonal_through_point(326 ^ [], 325 ^ [])]]))).
% 13.58/13.85 ncf('1.2.3.1.2',plain,[convergent_lines(orthogonal_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ []))],extension(6 ^ 4,bind([[_58766], [orthogonal_through_point(326 ^ [], 325 ^ [])]]))).
% 13.58/13.85 ncf('1.2.3.2',plain,[convergent_lines(orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []))],extension(6 ^ 5,bind([[_58766], [orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ [])]]))).
% 13.58/13.85 ncf('1.2.3.3',plain,[convergent_lines(orthogonal_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ [])), -(convergent_lines(orthogonal_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ []))), -(convergent_lines(orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ [])))],extension(28 ^ 5,bind([[_59535, _59537, _59539], [orthogonal_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ [])]]))).
% 13.58/13.85 ncf('1.2.3.3.1',plain,[convergent_lines(orthogonal_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ []))],extension(6 ^ 6,bind([[_58766], [orthogonal_through_point(326 ^ [], 325 ^ [])]]))).
% 13.58/13.85 ncf('1.2.3.3.2',plain,[convergent_lines(orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ [])), unorthogonal_lines(orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ [])), 154 : -(convergent_lines(orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []))), 160 : -(unorthogonal_lines(orthogonal_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ [])))],extension(144 ^ 6,bind([[_63403, _63405, _63407], [orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ [])]]))).
% 13.58/13.85 ncf('1.2.3.3.2.1',plain,[-(unorthogonal_lines(orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ [])))],reduction('1.2')).
% 13.58/13.85 ncf('1.2.3.3.2.2',plain,[convergent_lines(orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []))],extension(6 ^ 9,bind([[_58766], [orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ [])]]))).
% 13.58/13.85 ncf('1.2.3.3.2.3',plain,[unorthogonal_lines(orthogonal_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ [])), 196 : -(unorthogonal_lines(orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ []))), 198 : -(convergent_lines(orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []))), 198 : convergent_lines(orthogonal_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []))],extension(190 ^ 9,bind([[_64935, _64937, _64939], [orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ [])]]))).
% 13.58/13.85 ncf('1.2.3.3.2.3.1',plain,[unorthogonal_lines(orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ []))],extension(162 ^ 12,bind([[_63946, _63948], [orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []]]))).
% 13.58/13.85 ncf('1.2.3.3.2.3.2',plain,[convergent_lines(orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ []))],extension(6 ^ 12,bind([[_58766], [orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ [])]]))).
% 13.58/13.85 ncf('1.2.3.3.2.3.3',plain,[-(convergent_lines(orthogonal_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(orthogonal_through_point(326 ^ [], 325 ^ []), 325 ^ [])))],reduction('1.2.3')).
% 13.58/13.85 ncf('1.2.4',plain,[unorthogonal_lines(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ [])), convergent_lines(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ [])), 154 : -(convergent_lines(parallel_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ []))), 158 : -(convergent_lines(orthogonal_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ [])))],extension(144 ^ 2,bind([[_63403, _63405, _63407], [parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ [])]]))).
% 13.58/13.85 ncf('1.2.4.1',plain,[-(convergent_lines(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ []))), 200 : -(unorthogonal_lines(parallel_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ []))), 200 : convergent_lines(orthogonal_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ [])), 200 : unorthogonal_lines(orthogonal_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ []))],extension(190 ^ 3,bind([[_64935, _64937, _64939], [parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ [])]]))).
% 13.58/13.85 ncf('1.2.4.1.1',plain,[unorthogonal_lines(parallel_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ [])), convergent_lines(parallel_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ [])), 154 : -(convergent_lines(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ []))), 158 : -(convergent_lines(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ [])))],extension(144 ^ 6,bind([[_63403, _63405, _63407], [orthogonal_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ [])]]))).
% 13.58/13.85 ncf('1.2.4.1.1.1',plain,[-(convergent_lines(parallel_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ []))), convergent_lines(parallel_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ [])), -(convergent_lines(parallel_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ [])))],extension(28 ^ 7,bind([[_59535, _59537, _59539], [parallel_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ [])]]))).
% 13.58/13.85 ncf('1.2.4.1.1.1.1',plain,[-(convergent_lines(parallel_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ [])))],extension(198 ^ 8)).
% 13.58/13.85 ncf('1.2.4.1.1.1.2',plain,[convergent_lines(parallel_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ []))],reduction('1.2.4.1.1')).
% 13.58/13.85 ncf('1.2.4.1.1.2',plain,[convergent_lines(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ []))],reduction('1.2.4')).
% 13.58/13.85 ncf('1.2.4.1.1.3',plain,[convergent_lines(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ []))],reduction('1.2.4')).
% 13.58/13.85 ncf('1.2.4.1.2',plain,[-(convergent_lines(orthogonal_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ []))), convergent_lines(orthogonal_through_point(326 ^ [], 325 ^ []), 326 ^ []), -(convergent_lines(326 ^ [], parallel_through_point(326 ^ [], 325 ^ [])))],extension(28 ^ 4,bind([[_59535, _59537, _59539], [parallel_through_point(326 ^ [], 325 ^ []), 326 ^ [], orthogonal_through_point(326 ^ [], 325 ^ [])]]))).
% 13.58/13.85 ncf('1.2.4.1.2.1',plain,[-(convergent_lines(orthogonal_through_point(326 ^ [], 325 ^ []), 326 ^ [])), -(unorthogonal_lines(orthogonal_through_point(326 ^ [], 325 ^ []), 326 ^ []))],extension(138 ^ 5,bind([[_63178, _63180], [326 ^ [], orthogonal_through_point(326 ^ [], 325 ^ [])]]))).
% 13.58/13.85 ncf('1.2.4.1.2.1.1',plain,[unorthogonal_lines(orthogonal_through_point(326 ^ [], 325 ^ []), 326 ^ [])],extension(162 ^ 6,bind([[_63946, _63948], [326 ^ [], 325 ^ []]]))).
% 13.58/13.85 ncf('1.2.4.1.2.2',plain,[convergent_lines(326 ^ [], parallel_through_point(326 ^ [], 325 ^ [])), -(convergent_lines(326 ^ [], 326 ^ [])), -(convergent_lines(parallel_through_point(326 ^ [], 325 ^ []), 326 ^ []))],extension(28 ^ 5,bind([[_59535, _59537, _59539], [326 ^ [], parallel_through_point(326 ^ [], 325 ^ []), 326 ^ []]]))).
% 13.58/13.85 ncf('1.2.4.1.2.2.1',plain,[convergent_lines(326 ^ [], 326 ^ [])],extension(6 ^ 6,bind([[_58766], [326 ^ []]]))).
% 13.58/13.85 ncf('1.2.4.1.2.2.2',plain,[convergent_lines(parallel_through_point(326 ^ [], 325 ^ []), 326 ^ [])],extension(120 ^ 6,bind([[_62548, _62550], [326 ^ [], 325 ^ []]]))).
% 13.58/13.85 ncf('1.2.4.1.3',plain,[-(unorthogonal_lines(orthogonal_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ []))), -(convergent_lines(orthogonal_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ [])))],extension(138 ^ 4,bind([[_63178, _63180], [parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ [])]]))).
% 13.58/13.85 ncf('1.2.4.1.3.1',plain,[convergent_lines(orthogonal_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ [])), -(convergent_lines(orthogonal_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ []))), -(convergent_lines(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ [])))],extension(28 ^ 5,bind([[_59535, _59537, _59539], [orthogonal_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ [])]]))).
% 13.58/13.85 ncf('1.2.4.1.3.1.1',plain,[convergent_lines(orthogonal_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ []))],extension(6 ^ 6,bind([[_58766], [orthogonal_through_point(326 ^ [], 325 ^ [])]]))).
% 13.58/13.85 ncf('1.2.4.1.3.1.2',plain,[convergent_lines(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ []))],reduction('1.2.4')).
% 13.58/13.85 ncf('1.2.4.2',plain,[convergent_lines(parallel_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ []))],extension(6 ^ 5,bind([[_58766], [parallel_through_point(326 ^ [], 325 ^ [])]]))).
% 13.58/13.85 ncf('1.2.4.3',plain,[convergent_lines(orthogonal_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ [])), -(convergent_lines(orthogonal_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ []))), -(convergent_lines(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ [])))],extension(28 ^ 5,bind([[_59535, _59537, _59539], [orthogonal_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ [])]]))).
% 13.58/13.85 ncf('1.2.4.3.1',plain,[convergent_lines(orthogonal_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ []))],extension(6 ^ 6,bind([[_58766], [orthogonal_through_point(326 ^ [], 325 ^ [])]]))).
% 13.58/13.85 ncf('1.2.4.3.2',plain,[convergent_lines(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ [])), unorthogonal_lines(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ [])), 154 : -(convergent_lines(parallel_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ []))), 160 : -(unorthogonal_lines(orthogonal_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ [])))],extension(144 ^ 6,bind([[_63403, _63405, _63407], [parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ [])]]))).
% 13.58/13.85 ncf('1.2.4.3.2.1',plain,[-(unorthogonal_lines(parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ [])))],reduction('1.2')).
% 13.58/13.85 ncf('1.2.4.3.2.2',plain,[convergent_lines(parallel_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ []))],extension(6 ^ 9,bind([[_58766], [parallel_through_point(326 ^ [], 325 ^ [])]]))).
% 13.58/13.85 ncf('1.2.4.3.2.3',plain,[unorthogonal_lines(orthogonal_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ [])), convergent_lines(orthogonal_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ [])), 156 : -(unorthogonal_lines(orthogonal_through_point(326 ^ [], 325 ^ []), 326 ^ [])), 158 : -(convergent_lines(parallel_through_point(326 ^ [], 325 ^ []), 326 ^ []))],extension(144 ^ 9,bind([[_63403, _63405, _63407], [326 ^ [], parallel_through_point(326 ^ [], 325 ^ []), orthogonal_through_point(326 ^ [], 325 ^ [])]]))).
% 13.58/13.85 ncf('1.2.4.3.2.3.1',plain,[-(convergent_lines(orthogonal_through_point(326 ^ [], 325 ^ []), parallel_through_point(326 ^ [], 325 ^ [])))],reduction('1.2.4')).
% 13.58/13.85 ncf('1.2.4.3.2.3.2',plain,[unorthogonal_lines(orthogonal_through_point(326 ^ [], 325 ^ []), 326 ^ [])],extension(162 ^ 12,bind([[_63946, _63948], [326 ^ [], 325 ^ []]]))).
% 13.58/13.85 ncf('1.2.4.3.2.3.3',plain,[convergent_lines(parallel_through_point(326 ^ [], 325 ^ []), 326 ^ [])],extension(120 ^ 12,bind([[_62548, _62550], [326 ^ [], 325 ^ []]]))).
% 13.58/13.85 %-----------------------------------------------------
% 13.58/13.85 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------