%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM296+1 : TPTP v8.1.2. Released v3.1.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:44:21 EDT 2023
% Result : Theorem 0.35s 1.37s
% Output : Proof 0.35s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : NUM296+1 : TPTP v8.1.2. Released v3.1.0.
% 0.04/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n010.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 : Thu May 18 16:31:42 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.35/1.37
% 0.35/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.35/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.35/1.37 %-----------------------------------------------------
% 0.35/1.37 ncf(matrix, plain, [(1312 ^ _328343) ^ [] : [less(nn2, n2)], (176 ^ _328343) ^ [_334279, _334281] : [_334281 = _334279, -(rdn_neg(_334281) = rdn_neg(_334279))], (182 ^ _328343) ^ [_334497, _334499] : [_334499 = _334497, -(rdn_pos(_334499) = rdn_pos(_334497))], (198 ^ _328343) ^ [_335054, _335056] : [_335056 = _335054, -(rdnn(_335056) = rdnn(_335054))], (188 ^ _328343) ^ [_334743, _334745, _334747, _334749] : [-(rdn(_334749, _334745) = rdn(_334747, _334743)), _334749 = _334747, _334745 = _334743], (2 ^ _328343) ^ [_328487] : [-(_328487 = _328487)], (4 ^ _328343) ^ [_328594, _328596] : [_328596 = _328594, -(_328594 = _328596)], (10 ^ _328343) ^ [_328798, _328800, _328802] : [-(_328802 = _328798), _328802 = _328800, _328800 = _328798], (20 ^ _328343) ^ [_329111, _329113] : [-(rdn_non_zero_digit(_329111)), _329113 = _329111, rdn_non_zero_digit(_329113)], (30 ^ _328343) ^ [_329434, _329436, _329438, _329440] : [-(less_or_equal(_329438, _329434)), less_or_equal(_329440, _329436), _329440 = _329438, _329436 = _329434], (44 ^ _328343) ^ [_329878, _329880, _329882, _329884] : [-(rdn_positive_less(_329882, _329878)), rdn_positive_less(_329884, _329880), _329884 = _329882, _329880 = _329878], (58 ^ _328343) ^ [_330322, _330324, _330326, _330328] : [-(rdn_translate(_330326, _330322)), rdn_translate(_330328, _330324), _330328 = _330326, _330324 = _330322], (72 ^ _328343) ^ [_330794, _330796, _330798, _330800, _330802, _330804] : [-(sum(_330802, _330798, _330794)), sum(_330804, _330800, _330796), _330804 = _330802, _330800 = _330798, _330796 = _330794], (90 ^ _328343) ^ [_331403, _331405, _331407, _331409, _331411, _331413] : [-(difference(_331411, _331407, _331403)), difference(_331413, _331409, _331405), _331413 = _331411, _331409 = _331407, _331405 = _331403], (108 ^ _328343) ^ [_331956, _331958] : [-(rdn_non_zero(_331956)), _331958 = _331956, rdn_non_zero(_331958)], (118 ^ _328343) ^ [_332335, _332337, _332339, _332341, _332343, _332345, _332347, _332349] : [-(rdn_add_with_carry(_332347, _332343, _332339, _332335)), rdn_add_with_carry(_332349, _332345, _332341, _332337), _332349 = _332347, _332345 = _332343, _332341 = _332339, _332337 = _332335], (162 ^ _328343) ^ [_333839, _333841, _333843, _333845] : [-(less(_333843, _333839)), less(_333845, _333841), _333845 = _333843, _333841 = _333839], (140 ^ _328343) ^ [_333125, _333127, _333129, _333131, _333133, _333135, _333137, _333139] : [-(rdn_digit_add(_333137, _333133, _333129, _333125)), rdn_digit_add(_333139, _333135, _333131, _333127), _333139 = _333137, _333135 = _333133, _333131 = _333129, _333127 = _333125], (204 ^ _328343) ^ [] : [-(rdn_translate(n0, rdn_pos(rdnn(n0))))], (206 ^ _328343) ^ [] : [-(rdn_translate(n1, rdn_pos(rdnn(n1))))], (208 ^ _328343) ^ [] : [-(rdn_translate(n2, rdn_pos(rdnn(n2))))], (210 ^ _328343) ^ [] : [-(rdn_translate(n3, rdn_pos(rdnn(n3))))], (212 ^ _328343) ^ [] : [-(rdn_translate(n4, rdn_pos(rdnn(n4))))], (214 ^ _328343) ^ [] : [-(rdn_translate(n5, rdn_pos(rdnn(n5))))], (216 ^ _328343) ^ [] : [-(rdn_translate(n6, rdn_pos(rdnn(n6))))], (218 ^ _328343) ^ [] : [-(rdn_translate(n7, rdn_pos(rdnn(n7))))], (220 ^ _328343) ^ [] : [-(rdn_translate(n8, rdn_pos(rdnn(n8))))], (222 ^ _328343) ^ [] : [-(rdn_translate(n9, rdn_pos(rdnn(n9))))], (224 ^ _328343) ^ [] : [-(rdn_translate(n10, rdn_pos(rdn(rdnn(n0), rdnn(n1)))))], (226 ^ _328343) ^ [] : [-(rdn_translate(n11, rdn_pos(rdn(rdnn(n1), rdnn(n1)))))], (228 ^ _328343) ^ [] : [-(rdn_translate(n12, rdn_pos(rdn(rdnn(n2), rdnn(n1)))))], (230 ^ _328343) ^ [] : [-(rdn_translate(n13, rdn_pos(rdn(rdnn(n3), rdnn(n1)))))], (232 ^ _328343) ^ [] : [-(rdn_translate(n14, rdn_pos(rdn(rdnn(n4), rdnn(n1)))))], (234 ^ _328343) ^ [] : [-(rdn_translate(n15, rdn_pos(rdn(rdnn(n5), rdnn(n1)))))], (236 ^ _328343) ^ [] : [-(rdn_translate(n16, rdn_pos(rdn(rdnn(n6), rdnn(n1)))))], (238 ^ _328343) ^ [] : [-(rdn_translate(n17, rdn_pos(rdn(rdnn(n7), rdnn(n1)))))], (240 ^ _328343) ^ [] : [-(rdn_translate(n18, rdn_pos(rdn(rdnn(n8), rdnn(n1)))))], (242 ^ _328343) ^ [] : [-(rdn_translate(n19, rdn_pos(rdn(rdnn(n9), rdnn(n1)))))], (244 ^ _328343) ^ [] : [-(rdn_translate(n20, rdn_pos(rdn(rdnn(n0), rdnn(n2)))))], (246 ^ _328343) ^ [] : [-(rdn_translate(n21, rdn_pos(rdn(rdnn(n1), rdnn(n2)))))], (248 ^ _328343) ^ [] : [-(rdn_translate(n22, rdn_pos(rdn(rdnn(n2), rdnn(n2)))))], (250 ^ _328343) ^ [] : [-(rdn_translate(n23, rdn_pos(rdn(rdnn(n3), rdnn(n2)))))], (252 ^ _328343) ^ [] : [-(rdn_translate(n24, rdn_pos(rdn(rdnn(n4), rdnn(n2)))))], (254 ^ _328343) ^ [] : [-(rdn_translate(n25, rdn_pos(rdn(rdnn(n5), rdnn(n2)))))], (256 ^ _328343) ^ [] : [-(rdn_translate(n26, rdn_pos(rdn(rdnn(n6), rdnn(n2)))))], (258 ^ _328343) ^ [] : [-(rdn_translate(n27, rdn_pos(rdn(rdnn(n7), rdnn(n2)))))], (260 ^ _328343) ^ [] : [-(rdn_translate(n28, rdn_pos(rdn(rdnn(n8), rdnn(n2)))))], (262 ^ _328343) ^ [] : [-(rdn_translate(n29, rdn_pos(rdn(rdnn(n9), rdnn(n2)))))], (264 ^ _328343) ^ [] : [-(rdn_translate(n30, rdn_pos(rdn(rdnn(n0), rdnn(n3)))))], (266 ^ _328343) ^ [] : [-(rdn_translate(n31, rdn_pos(rdn(rdnn(n1), rdnn(n3)))))], (268 ^ _328343) ^ [] : [-(rdn_translate(n32, rdn_pos(rdn(rdnn(n2), rdnn(n3)))))], (270 ^ _328343) ^ [] : [-(rdn_translate(n33, rdn_pos(rdn(rdnn(n3), rdnn(n3)))))], (272 ^ _328343) ^ [] : [-(rdn_translate(n34, rdn_pos(rdn(rdnn(n4), rdnn(n3)))))], (274 ^ _328343) ^ [] : [-(rdn_translate(n35, rdn_pos(rdn(rdnn(n5), rdnn(n3)))))], (276 ^ _328343) ^ [] : [-(rdn_translate(n36, rdn_pos(rdn(rdnn(n6), rdnn(n3)))))], (278 ^ _328343) ^ [] : [-(rdn_translate(n37, rdn_pos(rdn(rdnn(n7), rdnn(n3)))))], (280 ^ _328343) ^ [] : [-(rdn_translate(n38, rdn_pos(rdn(rdnn(n8), rdnn(n3)))))], (282 ^ _328343) ^ [] : [-(rdn_translate(n39, rdn_pos(rdn(rdnn(n9), rdnn(n3)))))], (284 ^ _328343) ^ [] : [-(rdn_translate(n40, rdn_pos(rdn(rdnn(n0), rdnn(n4)))))], (286 ^ _328343) ^ [] : [-(rdn_translate(n41, rdn_pos(rdn(rdnn(n1), rdnn(n4)))))], (288 ^ _328343) ^ [] : [-(rdn_translate(n42, rdn_pos(rdn(rdnn(n2), rdnn(n4)))))], (290 ^ _328343) ^ [] : [-(rdn_translate(n43, rdn_pos(rdn(rdnn(n3), rdnn(n4)))))], (292 ^ _328343) ^ [] : [-(rdn_translate(n44, rdn_pos(rdn(rdnn(n4), rdnn(n4)))))], (294 ^ _328343) ^ [] : [-(rdn_translate(n45, rdn_pos(rdn(rdnn(n5), rdnn(n4)))))], (296 ^ _328343) ^ [] : [-(rdn_translate(n46, rdn_pos(rdn(rdnn(n6), rdnn(n4)))))], (298 ^ _328343) ^ [] : [-(rdn_translate(n47, rdn_pos(rdn(rdnn(n7), rdnn(n4)))))], (300 ^ _328343) ^ [] : [-(rdn_translate(n48, rdn_pos(rdn(rdnn(n8), rdnn(n4)))))], (302 ^ _328343) ^ [] : [-(rdn_translate(n49, rdn_pos(rdn(rdnn(n9), rdnn(n4)))))], (304 ^ _328343) ^ [] : [-(rdn_translate(n50, rdn_pos(rdn(rdnn(n0), rdnn(n5)))))], (306 ^ _328343) ^ [] : [-(rdn_translate(n51, rdn_pos(rdn(rdnn(n1), rdnn(n5)))))], (308 ^ _328343) ^ [] : [-(rdn_translate(n52, rdn_pos(rdn(rdnn(n2), rdnn(n5)))))], (310 ^ _328343) ^ [] : [-(rdn_translate(n53, rdn_pos(rdn(rdnn(n3), rdnn(n5)))))], (312 ^ _328343) ^ [] : [-(rdn_translate(n54, rdn_pos(rdn(rdnn(n4), rdnn(n5)))))], (314 ^ _328343) ^ [] : [-(rdn_translate(n55, rdn_pos(rdn(rdnn(n5), rdnn(n5)))))], (316 ^ _328343) ^ [] : [-(rdn_translate(n56, rdn_pos(rdn(rdnn(n6), rdnn(n5)))))], (318 ^ _328343) ^ [] : [-(rdn_translate(n57, rdn_pos(rdn(rdnn(n7), rdnn(n5)))))], (320 ^ _328343) ^ [] : [-(rdn_translate(n58, rdn_pos(rdn(rdnn(n8), rdnn(n5)))))], (322 ^ _328343) ^ [] : [-(rdn_translate(n59, rdn_pos(rdn(rdnn(n9), rdnn(n5)))))], (324 ^ _328343) ^ [] : [-(rdn_translate(n60, rdn_pos(rdn(rdnn(n0), rdnn(n6)))))], (326 ^ _328343) ^ [] : [-(rdn_translate(n61, rdn_pos(rdn(rdnn(n1), rdnn(n6)))))], (328 ^ _328343) ^ [] : [-(rdn_translate(n62, rdn_pos(rdn(rdnn(n2), rdnn(n6)))))], (330 ^ _328343) ^ [] : [-(rdn_translate(n63, rdn_pos(rdn(rdnn(n3), rdnn(n6)))))], (332 ^ _328343) ^ [] : [-(rdn_translate(n64, rdn_pos(rdn(rdnn(n4), rdnn(n6)))))], (334 ^ _328343) ^ [] : [-(rdn_translate(n65, rdn_pos(rdn(rdnn(n5), rdnn(n6)))))], (336 ^ _328343) ^ [] : [-(rdn_translate(n66, rdn_pos(rdn(rdnn(n6), rdnn(n6)))))], (338 ^ _328343) ^ [] : [-(rdn_translate(n67, rdn_pos(rdn(rdnn(n7), rdnn(n6)))))], (340 ^ _328343) ^ [] : [-(rdn_translate(n68, rdn_pos(rdn(rdnn(n8), rdnn(n6)))))], (342 ^ _328343) ^ [] : [-(rdn_translate(n69, rdn_pos(rdn(rdnn(n9), rdnn(n6)))))], (344 ^ _328343) ^ [] : [-(rdn_translate(n70, rdn_pos(rdn(rdnn(n0), rdnn(n7)))))], (346 ^ _328343) ^ [] : [-(rdn_translate(n71, rdn_pos(rdn(rdnn(n1), rdnn(n7)))))], (348 ^ _328343) ^ [] : [-(rdn_translate(n72, rdn_pos(rdn(rdnn(n2), rdnn(n7)))))], (350 ^ _328343) ^ [] : [-(rdn_translate(n73, rdn_pos(rdn(rdnn(n3), rdnn(n7)))))], (352 ^ _328343) ^ [] : [-(rdn_translate(n74, rdn_pos(rdn(rdnn(n4), rdnn(n7)))))], (354 ^ _328343) ^ [] : [-(rdn_translate(n75, rdn_pos(rdn(rdnn(n5), rdnn(n7)))))], (356 ^ _328343) ^ [] : [-(rdn_translate(n76, rdn_pos(rdn(rdnn(n6), rdnn(n7)))))], (358 ^ _328343) ^ [] : [-(rdn_translate(n77, rdn_pos(rdn(rdnn(n7), rdnn(n7)))))], (360 ^ _328343) ^ [] : [-(rdn_translate(n78, rdn_pos(rdn(rdnn(n8), rdnn(n7)))))], (362 ^ _328343) ^ [] : [-(rdn_translate(n79, rdn_pos(rdn(rdnn(n9), rdnn(n7)))))], (364 ^ _328343) ^ [] : [-(rdn_translate(n80, rdn_pos(rdn(rdnn(n0), rdnn(n8)))))], (366 ^ _328343) ^ [] : [-(rdn_translate(n81, rdn_pos(rdn(rdnn(n1), rdnn(n8)))))], (368 ^ _328343) ^ [] : [-(rdn_translate(n82, rdn_pos(rdn(rdnn(n2), rdnn(n8)))))], (370 ^ _328343) ^ [] : [-(rdn_translate(n83, rdn_pos(rdn(rdnn(n3), rdnn(n8)))))], (372 ^ _328343) ^ [] : [-(rdn_translate(n84, rdn_pos(rdn(rdnn(n4), rdnn(n8)))))], (374 ^ _328343) ^ [] : [-(rdn_translate(n85, rdn_pos(rdn(rdnn(n5), rdnn(n8)))))], (376 ^ _328343) ^ [] : [-(rdn_translate(n86, rdn_pos(rdn(rdnn(n6), rdnn(n8)))))], (378 ^ _328343) ^ [] : [-(rdn_translate(n87, rdn_pos(rdn(rdnn(n7), rdnn(n8)))))], (380 ^ _328343) ^ [] : [-(rdn_translate(n88, rdn_pos(rdn(rdnn(n8), rdnn(n8)))))], (382 ^ _328343) ^ [] : [-(rdn_translate(n89, rdn_pos(rdn(rdnn(n9), rdnn(n8)))))], (384 ^ _328343) ^ [] : [-(rdn_translate(n90, rdn_pos(rdn(rdnn(n0), rdnn(n9)))))], (386 ^ _328343) ^ [] : [-(rdn_translate(n91, rdn_pos(rdn(rdnn(n1), rdnn(n9)))))], (388 ^ _328343) ^ [] : [-(rdn_translate(n92, rdn_pos(rdn(rdnn(n2), rdnn(n9)))))], (390 ^ _328343) ^ [] : [-(rdn_translate(n93, rdn_pos(rdn(rdnn(n3), rdnn(n9)))))], (392 ^ _328343) ^ [] : [-(rdn_translate(n94, rdn_pos(rdn(rdnn(n4), rdnn(n9)))))], (394 ^ _328343) ^ [] : [-(rdn_translate(n95, rdn_pos(rdn(rdnn(n5), rdnn(n9)))))], (396 ^ _328343) ^ [] : [-(rdn_translate(n96, rdn_pos(rdn(rdnn(n6), rdnn(n9)))))], (398 ^ _328343) ^ [] : [-(rdn_translate(n97, rdn_pos(rdn(rdnn(n7), rdnn(n9)))))], (400 ^ _328343) ^ [] : [-(rdn_translate(n98, rdn_pos(rdn(rdnn(n8), rdnn(n9)))))], (402 ^ _328343) ^ [] : [-(rdn_translate(n99, rdn_pos(rdn(rdnn(n9), rdnn(n9)))))], (404 ^ _328343) ^ [] : [-(rdn_translate(n100, rdn_pos(rdn(rdnn(n0), rdn(rdnn(n0), rdnn(n1))))))], (406 ^ _328343) ^ [] : [-(rdn_translate(n101, rdn_pos(rdn(rdnn(n1), rdn(rdnn(n0), rdnn(n1))))))], (408 ^ _328343) ^ [] : [-(rdn_translate(n102, rdn_pos(rdn(rdnn(n2), rdn(rdnn(n0), rdnn(n1))))))], (410 ^ _328343) ^ [] : [-(rdn_translate(n103, rdn_pos(rdn(rdnn(n3), rdn(rdnn(n0), rdnn(n1))))))], (412 ^ _328343) ^ [] : [-(rdn_translate(n104, rdn_pos(rdn(rdnn(n4), rdn(rdnn(n0), rdnn(n1))))))], (414 ^ _328343) ^ [] : [-(rdn_translate(n105, rdn_pos(rdn(rdnn(n5), rdn(rdnn(n0), rdnn(n1))))))], (416 ^ _328343) ^ [] : [-(rdn_translate(n106, rdn_pos(rdn(rdnn(n6), rdn(rdnn(n0), rdnn(n1))))))], (418 ^ _328343) ^ [] : [-(rdn_translate(n107, rdn_pos(rdn(rdnn(n7), rdn(rdnn(n0), rdnn(n1))))))], (420 ^ _328343) ^ [] : [-(rdn_translate(n108, rdn_pos(rdn(rdnn(n8), rdn(rdnn(n0), rdnn(n1))))))], (422 ^ _328343) ^ [] : [-(rdn_translate(n109, rdn_pos(rdn(rdnn(n9), rdn(rdnn(n0), rdnn(n1))))))], (424 ^ _328343) ^ [] : [-(rdn_translate(n110, rdn_pos(rdn(rdnn(n0), rdn(rdnn(n1), rdnn(n1))))))], (426 ^ _328343) ^ [] : [-(rdn_translate(n111, rdn_pos(rdn(rdnn(n1), rdn(rdnn(n1), rdnn(n1))))))], (428 ^ _328343) ^ [] : [-(rdn_translate(n112, rdn_pos(rdn(rdnn(n2), rdn(rdnn(n1), rdnn(n1))))))], (430 ^ _328343) ^ [] : [-(rdn_translate(n113, rdn_pos(rdn(rdnn(n3), rdn(rdnn(n1), rdnn(n1))))))], (432 ^ _328343) ^ [] : [-(rdn_translate(n114, rdn_pos(rdn(rdnn(n4), rdn(rdnn(n1), rdnn(n1))))))], (434 ^ _328343) ^ [] : [-(rdn_translate(n115, rdn_pos(rdn(rdnn(n5), rdn(rdnn(n1), rdnn(n1))))))], (436 ^ _328343) ^ [] : [-(rdn_translate(n116, rdn_pos(rdn(rdnn(n6), rdn(rdnn(n1), rdnn(n1))))))], (438 ^ _328343) ^ [] : [-(rdn_translate(n117, rdn_pos(rdn(rdnn(n7), rdn(rdnn(n1), rdnn(n1))))))], (440 ^ _328343) ^ [] : [-(rdn_translate(n118, rdn_pos(rdn(rdnn(n8), rdn(rdnn(n1), rdnn(n1))))))], (442 ^ _328343) ^ [] : [-(rdn_translate(n119, rdn_pos(rdn(rdnn(n9), rdn(rdnn(n1), rdnn(n1))))))], (444 ^ _328343) ^ [] : [-(rdn_translate(n120, rdn_pos(rdn(rdnn(n0), rdn(rdnn(n2), rdnn(n1))))))], (446 ^ _328343) ^ [] : [-(rdn_translate(n121, rdn_pos(rdn(rdnn(n1), rdn(rdnn(n2), rdnn(n1))))))], (448 ^ _328343) ^ [] : [-(rdn_translate(n122, rdn_pos(rdn(rdnn(n2), rdn(rdnn(n2), rdnn(n1))))))], (450 ^ _328343) ^ [] : [-(rdn_translate(n123, rdn_pos(rdn(rdnn(n3), rdn(rdnn(n2), rdnn(n1))))))], (452 ^ _328343) ^ [] : [-(rdn_translate(n124, rdn_pos(rdn(rdnn(n4), rdn(rdnn(n2), rdnn(n1))))))], (454 ^ _328343) ^ [] : [-(rdn_translate(n125, rdn_pos(rdn(rdnn(n5), rdn(rdnn(n2), rdnn(n1))))))], (456 ^ _328343) ^ [] : [-(rdn_translate(n126, rdn_pos(rdn(rdnn(n6), rdn(rdnn(n2), rdnn(n1))))))], (458 ^ _328343) ^ [] : [-(rdn_translate(n127, rdn_pos(rdn(rdnn(n7), rdn(rdnn(n2), rdnn(n1))))))], (460 ^ _328343) ^ [] : [-(rdn_translate(nn1, rdn_neg(rdnn(n1))))], (462 ^ _328343) ^ [] : [-(rdn_translate(nn2, rdn_neg(rdnn(n2))))], (464 ^ _328343) ^ [] : [-(rdn_translate(nn3, rdn_neg(rdnn(n3))))], (466 ^ _328343) ^ [] : [-(rdn_translate(nn4, rdn_neg(rdnn(n4))))], (468 ^ _328343) ^ [] : [-(rdn_translate(nn5, rdn_neg(rdnn(n5))))], (470 ^ _328343) ^ [] : [-(rdn_translate(nn6, rdn_neg(rdnn(n6))))], (472 ^ _328343) ^ [] : [-(rdn_translate(nn7, rdn_neg(rdnn(n7))))], (474 ^ _328343) ^ [] : [-(rdn_translate(nn8, rdn_neg(rdnn(n8))))], (476 ^ _328343) ^ [] : [-(rdn_translate(nn9, rdn_neg(rdnn(n9))))], (478 ^ _328343) ^ [] : [-(rdn_translate(nn10, rdn_neg(rdn(rdnn(n0), rdnn(n1)))))], (480 ^ _328343) ^ [] : [-(rdn_translate(nn11, rdn_neg(rdn(rdnn(n1), rdnn(n1)))))], (482 ^ _328343) ^ [] : [-(rdn_translate(nn12, rdn_neg(rdn(rdnn(n2), rdnn(n1)))))], (484 ^ _328343) ^ [] : [-(rdn_translate(nn13, rdn_neg(rdn(rdnn(n3), rdnn(n1)))))], (486 ^ _328343) ^ [] : [-(rdn_translate(nn14, rdn_neg(rdn(rdnn(n4), rdnn(n1)))))], (488 ^ _328343) ^ [] : [-(rdn_translate(nn15, rdn_neg(rdn(rdnn(n5), rdnn(n1)))))], (490 ^ _328343) ^ [] : [-(rdn_translate(nn16, rdn_neg(rdn(rdnn(n6), rdnn(n1)))))], (492 ^ _328343) ^ [] : [-(rdn_translate(nn17, rdn_neg(rdn(rdnn(n7), rdnn(n1)))))], (494 ^ _328343) ^ [] : [-(rdn_translate(nn18, rdn_neg(rdn(rdnn(n8), rdnn(n1)))))], (496 ^ _328343) ^ [] : [-(rdn_translate(nn19, rdn_neg(rdn(rdnn(n9), rdnn(n1)))))], (498 ^ _328343) ^ [] : [-(rdn_translate(nn20, rdn_neg(rdn(rdnn(n0), rdnn(n2)))))], (500 ^ _328343) ^ [] : [-(rdn_translate(nn21, rdn_neg(rdn(rdnn(n1), rdnn(n2)))))], (502 ^ _328343) ^ [] : [-(rdn_translate(nn22, rdn_neg(rdn(rdnn(n2), rdnn(n2)))))], (504 ^ _328343) ^ [] : [-(rdn_translate(nn23, rdn_neg(rdn(rdnn(n3), rdnn(n2)))))], (506 ^ _328343) ^ [] : [-(rdn_translate(nn24, rdn_neg(rdn(rdnn(n4), rdnn(n2)))))], (508 ^ _328343) ^ [] : [-(rdn_translate(nn25, rdn_neg(rdn(rdnn(n5), rdnn(n2)))))], (510 ^ _328343) ^ [] : [-(rdn_translate(nn26, rdn_neg(rdn(rdnn(n6), rdnn(n2)))))], (512 ^ _328343) ^ [] : [-(rdn_translate(nn27, rdn_neg(rdn(rdnn(n7), rdnn(n2)))))], (514 ^ _328343) ^ [] : [-(rdn_translate(nn28, rdn_neg(rdn(rdnn(n8), rdnn(n2)))))], (516 ^ _328343) ^ [] : [-(rdn_translate(nn29, rdn_neg(rdn(rdnn(n9), rdnn(n2)))))], (518 ^ _328343) ^ [] : [-(rdn_translate(nn30, rdn_neg(rdn(rdnn(n0), rdnn(n3)))))], (520 ^ _328343) ^ [] : [-(rdn_translate(nn31, rdn_neg(rdn(rdnn(n1), rdnn(n3)))))], (522 ^ _328343) ^ [] : [-(rdn_translate(nn32, rdn_neg(rdn(rdnn(n2), rdnn(n3)))))], (524 ^ _328343) ^ [] : [-(rdn_translate(nn33, rdn_neg(rdn(rdnn(n3), rdnn(n3)))))], (526 ^ _328343) ^ [] : [-(rdn_translate(nn34, rdn_neg(rdn(rdnn(n4), rdnn(n3)))))], (528 ^ _328343) ^ [] : [-(rdn_translate(nn35, rdn_neg(rdn(rdnn(n5), rdnn(n3)))))], (530 ^ _328343) ^ [] : [-(rdn_translate(nn36, rdn_neg(rdn(rdnn(n6), rdnn(n3)))))], (532 ^ _328343) ^ [] : [-(rdn_translate(nn37, rdn_neg(rdn(rdnn(n7), rdnn(n3)))))], (534 ^ _328343) ^ [] : [-(rdn_translate(nn38, rdn_neg(rdn(rdnn(n8), rdnn(n3)))))], (536 ^ _328343) ^ [] : [-(rdn_translate(nn39, rdn_neg(rdn(rdnn(n9), rdnn(n3)))))], (538 ^ _328343) ^ [] : [-(rdn_translate(nn40, rdn_neg(rdn(rdnn(n0), rdnn(n4)))))], (540 ^ _328343) ^ [] : [-(rdn_translate(nn41, rdn_neg(rdn(rdnn(n1), rdnn(n4)))))], (542 ^ _328343) ^ [] : [-(rdn_translate(nn42, rdn_neg(rdn(rdnn(n2), rdnn(n4)))))], (544 ^ _328343) ^ [] : [-(rdn_translate(nn43, rdn_neg(rdn(rdnn(n3), rdnn(n4)))))], (546 ^ _328343) ^ [] : [-(rdn_translate(nn44, rdn_neg(rdn(rdnn(n4), rdnn(n4)))))], (548 ^ _328343) ^ [] : [-(rdn_translate(nn45, rdn_neg(rdn(rdnn(n5), rdnn(n4)))))], (550 ^ _328343) ^ [] : [-(rdn_translate(nn46, rdn_neg(rdn(rdnn(n6), rdnn(n4)))))], (552 ^ _328343) ^ [] : [-(rdn_translate(nn47, rdn_neg(rdn(rdnn(n7), rdnn(n4)))))], (554 ^ _328343) ^ [] : [-(rdn_translate(nn48, rdn_neg(rdn(rdnn(n8), rdnn(n4)))))], (556 ^ _328343) ^ [] : [-(rdn_translate(nn49, rdn_neg(rdn(rdnn(n9), rdnn(n4)))))], (558 ^ _328343) ^ [] : [-(rdn_translate(nn50, rdn_neg(rdn(rdnn(n0), rdnn(n5)))))], (560 ^ _328343) ^ [] : [-(rdn_translate(nn51, rdn_neg(rdn(rdnn(n1), rdnn(n5)))))], (562 ^ _328343) ^ [] : [-(rdn_translate(nn52, rdn_neg(rdn(rdnn(n2), rdnn(n5)))))], (564 ^ _328343) ^ [] : [-(rdn_translate(nn53, rdn_neg(rdn(rdnn(n3), rdnn(n5)))))], (566 ^ _328343) ^ [] : [-(rdn_translate(nn54, rdn_neg(rdn(rdnn(n4), rdnn(n5)))))], (568 ^ _328343) ^ [] : [-(rdn_translate(nn55, rdn_neg(rdn(rdnn(n5), rdnn(n5)))))], (570 ^ _328343) ^ [] : [-(rdn_translate(nn56, rdn_neg(rdn(rdnn(n6), rdnn(n5)))))], (572 ^ _328343) ^ [] : [-(rdn_translate(nn57, rdn_neg(rdn(rdnn(n7), rdnn(n5)))))], (574 ^ _328343) ^ [] : [-(rdn_translate(nn58, rdn_neg(rdn(rdnn(n8), rdnn(n5)))))], (576 ^ _328343) ^ [] : [-(rdn_translate(nn59, rdn_neg(rdn(rdnn(n9), rdnn(n5)))))], (578 ^ _328343) ^ [] : [-(rdn_translate(nn60, rdn_neg(rdn(rdnn(n0), rdnn(n6)))))], (580 ^ _328343) ^ [] : [-(rdn_translate(nn61, rdn_neg(rdn(rdnn(n1), rdnn(n6)))))], (582 ^ _328343) ^ [] : [-(rdn_translate(nn62, rdn_neg(rdn(rdnn(n2), rdnn(n6)))))], (584 ^ _328343) ^ [] : [-(rdn_translate(nn63, rdn_neg(rdn(rdnn(n3), rdnn(n6)))))], (586 ^ _328343) ^ [] : [-(rdn_translate(nn64, rdn_neg(rdn(rdnn(n4), rdnn(n6)))))], (588 ^ _328343) ^ [] : [-(rdn_translate(nn65, rdn_neg(rdn(rdnn(n5), rdnn(n6)))))], (590 ^ _328343) ^ [] : [-(rdn_translate(nn66, rdn_neg(rdn(rdnn(n6), rdnn(n6)))))], (592 ^ _328343) ^ [] : [-(rdn_translate(nn67, rdn_neg(rdn(rdnn(n7), rdnn(n6)))))], (594 ^ _328343) ^ [] : [-(rdn_translate(nn68, rdn_neg(rdn(rdnn(n8), rdnn(n6)))))], (596 ^ _328343) ^ [] : [-(rdn_translate(nn69, rdn_neg(rdn(rdnn(n9), rdnn(n6)))))], (598 ^ _328343) ^ [] : [-(rdn_translate(nn70, rdn_neg(rdn(rdnn(n0), rdnn(n7)))))], (600 ^ _328343) ^ [] : [-(rdn_translate(nn71, rdn_neg(rdn(rdnn(n1), rdnn(n7)))))], (602 ^ _328343) ^ [] : [-(rdn_translate(nn72, rdn_neg(rdn(rdnn(n2), rdnn(n7)))))], (604 ^ _328343) ^ [] : [-(rdn_translate(nn73, rdn_neg(rdn(rdnn(n3), rdnn(n7)))))], (606 ^ _328343) ^ [] : [-(rdn_translate(nn74, rdn_neg(rdn(rdnn(n4), rdnn(n7)))))], (608 ^ _328343) ^ [] : [-(rdn_translate(nn75, rdn_neg(rdn(rdnn(n5), rdnn(n7)))))], (610 ^ _328343) ^ [] : [-(rdn_translate(nn76, rdn_neg(rdn(rdnn(n6), rdnn(n7)))))], (612 ^ _328343) ^ [] : [-(rdn_translate(nn77, rdn_neg(rdn(rdnn(n7), rdnn(n7)))))], (614 ^ _328343) ^ [] : [-(rdn_translate(nn78, rdn_neg(rdn(rdnn(n8), rdnn(n7)))))], (616 ^ _328343) ^ [] : [-(rdn_translate(nn79, rdn_neg(rdn(rdnn(n9), rdnn(n7)))))], (618 ^ _328343) ^ [] : [-(rdn_translate(nn80, rdn_neg(rdn(rdnn(n0), rdnn(n8)))))], (620 ^ _328343) ^ [] : [-(rdn_translate(nn81, rdn_neg(rdn(rdnn(n1), rdnn(n8)))))], (622 ^ _328343) ^ [] : [-(rdn_translate(nn82, rdn_neg(rdn(rdnn(n2), rdnn(n8)))))], (624 ^ _328343) ^ [] : [-(rdn_translate(nn83, rdn_neg(rdn(rdnn(n3), rdnn(n8)))))], (626 ^ _328343) ^ [] : [-(rdn_translate(nn84, rdn_neg(rdn(rdnn(n4), rdnn(n8)))))], (628 ^ _328343) ^ [] : [-(rdn_translate(nn85, rdn_neg(rdn(rdnn(n5), rdnn(n8)))))], (630 ^ _328343) ^ [] : [-(rdn_translate(nn86, rdn_neg(rdn(rdnn(n6), rdnn(n8)))))], (632 ^ _328343) ^ [] : [-(rdn_translate(nn87, rdn_neg(rdn(rdnn(n7), rdnn(n8)))))], (634 ^ _328343) ^ [] : [-(rdn_translate(nn88, rdn_neg(rdn(rdnn(n8), rdnn(n8)))))], (636 ^ _328343) ^ [] : [-(rdn_translate(nn89, rdn_neg(rdn(rdnn(n9), rdnn(n8)))))], (638 ^ _328343) ^ [] : [-(rdn_translate(nn90, rdn_neg(rdn(rdnn(n0), rdnn(n9)))))], (640 ^ _328343) ^ [] : [-(rdn_translate(nn91, rdn_neg(rdn(rdnn(n1), rdnn(n9)))))], (642 ^ _328343) ^ [] : [-(rdn_translate(nn92, rdn_neg(rdn(rdnn(n2), rdnn(n9)))))], (644 ^ _328343) ^ [] : [-(rdn_translate(nn93, rdn_neg(rdn(rdnn(n3), rdnn(n9)))))], (646 ^ _328343) ^ [] : [-(rdn_translate(nn94, rdn_neg(rdn(rdnn(n4), rdnn(n9)))))], (648 ^ _328343) ^ [] : [-(rdn_translate(nn95, rdn_neg(rdn(rdnn(n5), rdnn(n9)))))], (650 ^ _328343) ^ [] : [-(rdn_translate(nn96, rdn_neg(rdn(rdnn(n6), rdnn(n9)))))], (652 ^ _328343) ^ [] : [-(rdn_translate(nn97, rdn_neg(rdn(rdnn(n7), rdnn(n9)))))], (654 ^ _328343) ^ [] : [-(rdn_translate(nn98, rdn_neg(rdn(rdnn(n8), rdnn(n9)))))], (656 ^ _328343) ^ [] : [-(rdn_translate(nn99, rdn_neg(rdn(rdnn(n9), rdnn(n9)))))], (658 ^ _328343) ^ [] : [-(rdn_translate(nn100, rdn_neg(rdn(rdnn(n0), rdn(rdnn(n0), rdnn(n1))))))], (660 ^ _328343) ^ [] : [-(rdn_translate(nn101, rdn_neg(rdn(rdnn(n1), rdn(rdnn(n0), rdnn(n1))))))], (662 ^ _328343) ^ [] : [-(rdn_translate(nn102, rdn_neg(rdn(rdnn(n2), rdn(rdnn(n0), rdnn(n1))))))], (664 ^ _328343) ^ [] : [-(rdn_translate(nn103, rdn_neg(rdn(rdnn(n3), rdn(rdnn(n0), rdnn(n1))))))], (666 ^ _328343) ^ [] : [-(rdn_translate(nn104, rdn_neg(rdn(rdnn(n4), rdn(rdnn(n0), rdnn(n1))))))], (668 ^ _328343) ^ [] : [-(rdn_translate(nn105, rdn_neg(rdn(rdnn(n5), rdn(rdnn(n0), rdnn(n1))))))], (670 ^ _328343) ^ [] : [-(rdn_translate(nn106, rdn_neg(rdn(rdnn(n6), rdn(rdnn(n0), rdnn(n1))))))], (672 ^ _328343) ^ [] : [-(rdn_translate(nn107, rdn_neg(rdn(rdnn(n7), rdn(rdnn(n0), rdnn(n1))))))], (674 ^ _328343) ^ [] : [-(rdn_translate(nn108, rdn_neg(rdn(rdnn(n8), rdn(rdnn(n0), rdnn(n1))))))], (676 ^ _328343) ^ [] : [-(rdn_translate(nn109, rdn_neg(rdn(rdnn(n9), rdn(rdnn(n0), rdnn(n1))))))], (678 ^ _328343) ^ [] : [-(rdn_translate(nn110, rdn_neg(rdn(rdnn(n0), rdn(rdnn(n1), rdnn(n1))))))], (680 ^ _328343) ^ [] : [-(rdn_translate(nn111, rdn_neg(rdn(rdnn(n1), rdn(rdnn(n1), rdnn(n1))))))], (682 ^ _328343) ^ [] : [-(rdn_translate(nn112, rdn_neg(rdn(rdnn(n2), rdn(rdnn(n1), rdnn(n1))))))], (684 ^ _328343) ^ [] : [-(rdn_translate(nn113, rdn_neg(rdn(rdnn(n3), rdn(rdnn(n1), rdnn(n1))))))], (686 ^ _328343) ^ [] : [-(rdn_translate(nn114, rdn_neg(rdn(rdnn(n4), rdn(rdnn(n1), rdnn(n1))))))], (688 ^ _328343) ^ [] : [-(rdn_translate(nn115, rdn_neg(rdn(rdnn(n5), rdn(rdnn(n1), rdnn(n1))))))], (690 ^ _328343) ^ [] : [-(rdn_translate(nn116, rdn_neg(rdn(rdnn(n6), rdn(rdnn(n1), rdnn(n1))))))], (692 ^ _328343) ^ [] : [-(rdn_translate(nn117, rdn_neg(rdn(rdnn(n7), rdn(rdnn(n1), rdnn(n1))))))], (694 ^ _328343) ^ [] : [-(rdn_translate(nn118, rdn_neg(rdn(rdnn(n8), rdn(rdnn(n1), rdnn(n1))))))], (696 ^ _328343) ^ [] : [-(rdn_translate(nn119, rdn_neg(rdn(rdnn(n9), rdn(rdnn(n1), rdnn(n1))))))], (698 ^ _328343) ^ [] : [-(rdn_translate(nn120, rdn_neg(rdn(rdnn(n0), rdn(rdnn(n2), rdnn(n1))))))], (700 ^ _328343) ^ [] : [-(rdn_translate(nn121, rdn_neg(rdn(rdnn(n1), rdn(rdnn(n2), rdnn(n1))))))], (702 ^ _328343) ^ [] : [-(rdn_translate(nn122, rdn_neg(rdn(rdnn(n2), rdn(rdnn(n2), rdnn(n1))))))], (704 ^ _328343) ^ [] : [-(rdn_translate(nn123, rdn_neg(rdn(rdnn(n3), rdn(rdnn(n2), rdnn(n1))))))], (706 ^ _328343) ^ [] : [-(rdn_translate(nn124, rdn_neg(rdn(rdnn(n4), rdn(rdnn(n2), rdnn(n1))))))], (708 ^ _328343) ^ [] : [-(rdn_translate(nn125, rdn_neg(rdn(rdnn(n5), rdn(rdnn(n2), rdnn(n1))))))], (710 ^ _328343) ^ [] : [-(rdn_translate(nn126, rdn_neg(rdn(rdnn(n6), rdn(rdnn(n2), rdnn(n1))))))], (712 ^ _328343) ^ [] : [-(rdn_translate(nn127, rdn_neg(rdn(rdnn(n7), rdn(rdnn(n2), rdnn(n1))))))], (714 ^ _328343) ^ [] : [-(rdn_translate(nn128, rdn_neg(rdn(rdnn(n8), rdn(rdnn(n2), rdnn(n1))))))], (716 ^ _328343) ^ [] : [-(rdn_non_zero_digit(rdnn(n1)))], (718 ^ _328343) ^ [] : [-(rdn_non_zero_digit(rdnn(n2)))], (720 ^ _328343) ^ [] : [-(rdn_non_zero_digit(rdnn(n3)))], (722 ^ _328343) ^ [] : [-(rdn_non_zero_digit(rdnn(n4)))], (724 ^ _328343) ^ [] : [-(rdn_non_zero_digit(rdnn(n5)))], (726 ^ _328343) ^ [] : [-(rdn_non_zero_digit(rdnn(n6)))], (728 ^ _328343) ^ [] : [-(rdn_non_zero_digit(rdnn(n7)))], (730 ^ _328343) ^ [] : [-(rdn_non_zero_digit(rdnn(n8)))], (732 ^ _328343) ^ [] : [-(rdn_non_zero_digit(rdnn(n9)))], (734 ^ _328343) ^ [] : [-(rdn_positive_less(rdnn(n0), rdnn(n1)))], (736 ^ _328343) ^ [] : [-(rdn_positive_less(rdnn(n1), rdnn(n2)))], (738 ^ _328343) ^ [] : [-(rdn_positive_less(rdnn(n2), rdnn(n3)))], (740 ^ _328343) ^ [] : [-(rdn_positive_less(rdnn(n3), rdnn(n4)))], (742 ^ _328343) ^ [] : [-(rdn_positive_less(rdnn(n4), rdnn(n5)))], (744 ^ _328343) ^ [] : [-(rdn_positive_less(rdnn(n5), rdnn(n6)))], (746 ^ _328343) ^ [] : [-(rdn_positive_less(rdnn(n6), rdnn(n7)))], (748 ^ _328343) ^ [] : [-(rdn_positive_less(rdnn(n7), rdnn(n8)))], (750 ^ _328343) ^ [] : [-(rdn_positive_less(rdnn(n8), rdnn(n9)))], (752 ^ _328343) ^ [_350352, _350354, _350356] : [-(rdn_positive_less(rdnn(_350356), rdnn(_350352))), rdn_positive_less(rdnn(_350356), rdnn(_350354)), rdn_positive_less(rdnn(_350354), rdnn(_350352))], (762 ^ _328343) ^ [_350713, _350715, _350717, _350719] : [rdn_positive_less(_350717, _350713), -(rdn_positive_less(rdn(rdnn(_350719), _350717), rdn(rdnn(_350715), _350713)))], (768 ^ _328343) ^ [_350969, _350971, _350973] : [-(rdn_positive_less(rdn(rdnn(_350973), _350971), rdn(rdnn(_350969), _350971))), rdn_positive_less(rdnn(_350973), rdnn(_350969)), rdn_non_zero(_350971)], (778 ^ _328343) ^ [_351318, _351320, _351322] : [rdn_non_zero(_351318), -(rdn_positive_less(rdnn(_351322), rdn(rdnn(_351320), _351318)))], (784 ^ _328343) ^ [_351532] : [rdn_non_zero_digit(rdnn(_351532)), -(rdn_non_zero(rdnn(_351532)))], (790 ^ _328343) ^ [_351740, _351742] : [rdn_non_zero(_351740), -(rdn_non_zero(rdn(rdnn(_351742), _351740)))], (796 ^ _328343) ^ [_351984, _351986, _351988, _351990] : [-(less(_351990, _351988)), rdn_translate(_351990, rdn_pos(_351986)), rdn_translate(_351988, rdn_pos(_351984)), rdn_positive_less(_351986, _351984)], (810 ^ _328343) ^ [_352436, _352438, _352440, _352442] : [-(less(_352442, _352440)), rdn_translate(_352442, rdn_neg(_352438)), rdn_translate(_352440, rdn_pos(_352436))], (820 ^ _328343) ^ [_352791, _352793, _352795, _352797] : [-(less(_352797, _352795)), rdn_translate(_352797, rdn_neg(_352793)), rdn_translate(_352795, rdn_neg(_352791)), rdn_positive_less(_352791, _352793)], (834 ^ _328343) ^ [_353244, _353246] : [less(_353246, _353244), 837 ^ _328343 : [(838 ^ _328343) ^ [] : [less(_353244, _353246)], (840 ^ _328343) ^ [] : [_353244 = _353246]]], (842 ^ _328343) ^ [_353483, _353485] : [-(less(_353485, _353483)), -(less(_353483, _353485)), -(_353483 = _353485)], (870 ^ _328343) ^ [_354351, _354353, _354355] : [-(less_or_equal(_354351, _354355)), sum(_354355, n1, _354353), less(_354351, _354353)], (862 ^ _328343) ^ [_354071, _354073] : [863 ^ _328343 : [(864 ^ _328343) ^ [] : [less(_354073, _354071)], (866 ^ _328343) ^ [] : [_354073 = _354071]], -(less_or_equal(_354073, _354071))], (852 ^ _328343) ^ [_353819, _353821] : [less_or_equal(_353821, _353819), -(less(_353821, _353819)), -(_353821 = _353819)], (880 ^ _328343) ^ [_354778, _354780, _354782, _354784, _354786, _354788] : [-(sum(_354788, _354786, _354784)), rdn_translate(_354788, rdn_pos(_354782)), rdn_translate(_354786, rdn_pos(_354780)), rdn_add_with_carry(rdnn(n0), _354782, _354780, _354778), rdn_translate(_354784, rdn_pos(_354778))], (898 ^ _328343) ^ [_355401, _355403, _355405, _355407, _355409, _355411] : [-(sum(_355411, _355409, _355407)), rdn_translate(_355411, rdn_neg(_355405)), rdn_translate(_355409, rdn_neg(_355403)), rdn_add_with_carry(rdnn(n0), _355405, _355403, _355401), rdn_translate(_355407, rdn_neg(_355401))], (916 ^ _328343) ^ [_356024, _356026, _356028, _356030, _356032, _356034] : [-(sum(_356034, _356032, _356030)), rdn_translate(_356034, rdn_pos(_356028)), rdn_translate(_356032, rdn_neg(_356026)), rdn_positive_less(_356028, _356026), rdn_add_with_carry(rdnn(n0), _356028, _356024, _356026), rdn_translate(_356030, rdn_neg(_356024))], (938 ^ _328343) ^ [_356752, _356754, _356756, _356758, _356760, _356762] : [-(sum(_356762, _356760, _356758)), rdn_translate(_356762, rdn_pos(_356756)), rdn_translate(_356760, rdn_neg(_356754)), rdn_positive_less(_356754, _356756), rdn_add_with_carry(rdnn(n0), _356754, _356752, _356756), rdn_translate(_356758, rdn_pos(_356752))], (960 ^ _328343) ^ [_357438, _357440, _357442] : [-(sum(_357442, _357440, n0)), rdn_translate(_357442, rdn_pos(_357438)), rdn_translate(_357440, rdn_neg(_357438))], (970 ^ _328343) ^ [_357799, _357801, _357803, _357805, _357807] : [-(sum(_357807, _357805, _357803)), rdn_translate(_357807, rdn_neg(_357801)), rdn_translate(_357805, rdn_pos(_357799)), sum(_357805, _357807, _357803)], (984 ^ _328343) ^ [_358269, _358271, _358273, _358275] : [-(_358271 = _358269), sum(_358275, _358273, _358271), sum(_358275, _358273, _358269)], (994 ^ _328343) ^ [_358620, _358622, _358624, _358626] : [-(_358626 = _358624), sum(_358626, _358622, _358620), sum(_358624, _358622, _358620)], (1004 ^ _328343) ^ [_358971, _358973, _358975, _358977] : [-(_358975 = _358973), sum(_358977, _358975, _358971), sum(_358977, _358973, _358971)], (1014 ^ _328343) ^ [_359337, _359339, _359341] : [sum(_359339, _359337, _359341), -(difference(_359341, _359339, _359337))], (1020 ^ _328343) ^ [_359509, _359511, _359513] : [difference(_359513, _359511, _359509), -(sum(_359511, _359509, _359513))], (1026 ^ _328343) ^ [_359773, _359775, _359777, _359779, _359781] : [-(rdn_add_with_carry(rdnn(_359781), rdnn(_359779), rdnn(_359777), rdnn(_359775))), rdn_digit_add(rdnn(_359779), rdnn(_359777), rdnn(_359773), rdnn(n0)), rdn_digit_add(rdnn(_359773), rdnn(_359781), rdnn(_359775), rdnn(n0))], (1036 ^ _328343) ^ [_360224, _360226, _360228, _360230, _360232, _360234, _360236] : [-(rdn_add_with_carry(rdnn(_360236), rdnn(_360234), rdnn(_360232), rdn(rdnn(_360228), rdnn(n1)))), rdn_digit_add(rdnn(_360234), rdnn(_360232), rdnn(_360230), rdnn(_360226)), rdn_digit_add(rdnn(_360230), rdnn(_360236), rdnn(_360228), rdnn(_360224)), rdn_digit_add(rdnn(_360226), rdnn(_360224), rdnn(n1), rdnn(n0))], (1050 ^ _328343) ^ [_360872, _360874, _360876, _360878, _360880, _360882, _360884, _360886, _360888, _360890] : [-(rdn_add_with_carry(rdnn(_360890), rdnn(_360888), rdn(rdnn(_360886), _360884), rdn(rdnn(_360882), _360880))), rdn_digit_add(rdnn(_360888), rdnn(_360886), rdnn(_360878), rdnn(_360876)), rdn_digit_add(rdnn(_360878), rdnn(_360890), rdnn(_360882), rdnn(_360874)), rdn_digit_add(rdnn(_360876), rdnn(_360874), rdnn(_360872), rdnn(n0)), rdn_add_with_carry(rdnn(_360872), rdnn(n0), _360884, _360880), rdn_non_zero(_360884), rdn_non_zero(_360880)], (1112 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n0), rdnn(n0), rdnn(n0), rdnn(n0)))], (1114 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n0), rdnn(n1), rdnn(n1), rdnn(n0)))], (1116 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n0), rdnn(n2), rdnn(n2), rdnn(n0)))], (1118 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n0), rdnn(n3), rdnn(n3), rdnn(n0)))], (1120 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n0), rdnn(n4), rdnn(n4), rdnn(n0)))], (1122 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n0), rdnn(n5), rdnn(n5), rdnn(n0)))], (1124 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n0), rdnn(n6), rdnn(n6), rdnn(n0)))], (1126 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n0), rdnn(n7), rdnn(n7), rdnn(n0)))], (1128 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n0), rdnn(n8), rdnn(n8), rdnn(n0)))], (1130 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n0), rdnn(n9), rdnn(n9), rdnn(n0)))], (1132 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n1), rdnn(n0), rdnn(n1), rdnn(n0)))], (1134 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n1), rdnn(n1), rdnn(n2), rdnn(n0)))], (1136 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n1), rdnn(n2), rdnn(n3), rdnn(n0)))], (1138 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n1), rdnn(n3), rdnn(n4), rdnn(n0)))], (1140 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n1), rdnn(n4), rdnn(n5), rdnn(n0)))], (1142 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n1), rdnn(n5), rdnn(n6), rdnn(n0)))], (1144 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n1), rdnn(n6), rdnn(n7), rdnn(n0)))], (1146 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n1), rdnn(n7), rdnn(n8), rdnn(n0)))], (1148 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n1), rdnn(n8), rdnn(n9), rdnn(n0)))], (1150 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n1), rdnn(n9), rdnn(n0), rdnn(n1)))], (1152 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n2), rdnn(n0), rdnn(n2), rdnn(n0)))], (1154 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n2), rdnn(n1), rdnn(n3), rdnn(n0)))], (1156 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n2), rdnn(n2), rdnn(n4), rdnn(n0)))], (1158 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n2), rdnn(n3), rdnn(n5), rdnn(n0)))], (1160 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n2), rdnn(n4), rdnn(n6), rdnn(n0)))], (1162 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n2), rdnn(n5), rdnn(n7), rdnn(n0)))], (1164 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n2), rdnn(n6), rdnn(n8), rdnn(n0)))], (1166 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n2), rdnn(n7), rdnn(n9), rdnn(n0)))], (1168 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n2), rdnn(n8), rdnn(n0), rdnn(n1)))], (1170 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n2), rdnn(n9), rdnn(n1), rdnn(n1)))], (1172 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n3), rdnn(n0), rdnn(n3), rdnn(n0)))], (1174 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n3), rdnn(n1), rdnn(n4), rdnn(n0)))], (1176 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n3), rdnn(n2), rdnn(n5), rdnn(n0)))], (1178 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n3), rdnn(n3), rdnn(n6), rdnn(n0)))], (1180 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n3), rdnn(n4), rdnn(n7), rdnn(n0)))], (1182 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n3), rdnn(n5), rdnn(n8), rdnn(n0)))], (1184 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n3), rdnn(n6), rdnn(n9), rdnn(n0)))], (1186 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n3), rdnn(n7), rdnn(n0), rdnn(n1)))], (1188 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n3), rdnn(n8), rdnn(n1), rdnn(n1)))], (1190 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n3), rdnn(n9), rdnn(n2), rdnn(n1)))], (1192 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n4), rdnn(n0), rdnn(n4), rdnn(n0)))], (1194 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n4), rdnn(n1), rdnn(n5), rdnn(n0)))], (1196 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n4), rdnn(n2), rdnn(n6), rdnn(n0)))], (1198 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n4), rdnn(n3), rdnn(n7), rdnn(n0)))], (1200 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n4), rdnn(n4), rdnn(n8), rdnn(n0)))], (1202 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n4), rdnn(n5), rdnn(n9), rdnn(n0)))], (1204 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n4), rdnn(n6), rdnn(n0), rdnn(n1)))], (1206 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n4), rdnn(n7), rdnn(n1), rdnn(n1)))], (1208 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n4), rdnn(n8), rdnn(n2), rdnn(n1)))], (1210 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n4), rdnn(n9), rdnn(n3), rdnn(n1)))], (1212 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n5), rdnn(n0), rdnn(n5), rdnn(n0)))], (1214 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n5), rdnn(n1), rdnn(n6), rdnn(n0)))], (1216 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n5), rdnn(n2), rdnn(n7), rdnn(n0)))], (1218 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n5), rdnn(n3), rdnn(n8), rdnn(n0)))], (1220 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n5), rdnn(n4), rdnn(n9), rdnn(n0)))], (1222 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n5), rdnn(n5), rdnn(n0), rdnn(n1)))], (1224 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n5), rdnn(n6), rdnn(n1), rdnn(n1)))], (1226 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n5), rdnn(n7), rdnn(n2), rdnn(n1)))], (1228 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n5), rdnn(n8), rdnn(n3), rdnn(n1)))], (1230 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n5), rdnn(n9), rdnn(n4), rdnn(n1)))], (1232 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n6), rdnn(n0), rdnn(n6), rdnn(n0)))], (1234 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n6), rdnn(n1), rdnn(n7), rdnn(n0)))], (1236 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n6), rdnn(n2), rdnn(n8), rdnn(n0)))], (1238 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n6), rdnn(n3), rdnn(n9), rdnn(n0)))], (1240 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n6), rdnn(n4), rdnn(n0), rdnn(n1)))], (1242 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n6), rdnn(n5), rdnn(n1), rdnn(n1)))], (1244 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n6), rdnn(n6), rdnn(n2), rdnn(n1)))], (1246 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n6), rdnn(n7), rdnn(n3), rdnn(n1)))], (1248 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n6), rdnn(n8), rdnn(n4), rdnn(n1)))], (1250 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n6), rdnn(n9), rdnn(n5), rdnn(n1)))], (1252 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n7), rdnn(n0), rdnn(n7), rdnn(n0)))], (1254 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n7), rdnn(n1), rdnn(n8), rdnn(n0)))], (1256 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n7), rdnn(n2), rdnn(n9), rdnn(n0)))], (1258 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n7), rdnn(n3), rdnn(n0), rdnn(n1)))], (1260 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n7), rdnn(n4), rdnn(n1), rdnn(n1)))], (1262 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n7), rdnn(n5), rdnn(n2), rdnn(n1)))], (1264 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n7), rdnn(n6), rdnn(n3), rdnn(n1)))], (1266 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n7), rdnn(n7), rdnn(n4), rdnn(n1)))], (1268 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n7), rdnn(n8), rdnn(n5), rdnn(n1)))], (1270 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n7), rdnn(n9), rdnn(n6), rdnn(n1)))], (1272 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n8), rdnn(n0), rdnn(n8), rdnn(n0)))], (1274 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n8), rdnn(n1), rdnn(n9), rdnn(n0)))], (1276 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n8), rdnn(n2), rdnn(n0), rdnn(n1)))], (1278 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n8), rdnn(n3), rdnn(n1), rdnn(n1)))], (1280 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n8), rdnn(n4), rdnn(n2), rdnn(n1)))], (1282 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n8), rdnn(n5), rdnn(n3), rdnn(n1)))], (1284 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n8), rdnn(n6), rdnn(n4), rdnn(n1)))], (1286 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n8), rdnn(n7), rdnn(n5), rdnn(n1)))], (1288 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n8), rdnn(n8), rdnn(n6), rdnn(n1)))], (1290 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n8), rdnn(n9), rdnn(n7), rdnn(n1)))], (1292 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n9), rdnn(n0), rdnn(n9), rdnn(n0)))], (1294 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n9), rdnn(n1), rdnn(n0), rdnn(n1)))], (1296 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n9), rdnn(n2), rdnn(n1), rdnn(n1)))], (1298 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n9), rdnn(n3), rdnn(n2), rdnn(n1)))], (1300 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n9), rdnn(n4), rdnn(n3), rdnn(n1)))], (1302 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n9), rdnn(n5), rdnn(n4), rdnn(n1)))], (1304 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n9), rdnn(n6), rdnn(n5), rdnn(n1)))], (1306 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n9), rdnn(n7), rdnn(n6), rdnn(n1)))], (1308 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n9), rdnn(n8), rdnn(n7), rdnn(n1)))], (1310 ^ _328343) ^ [] : [-(rdn_digit_add(rdnn(n9), rdnn(n9), rdnn(n8), rdnn(n1)))], (1106 ^ _328343) ^ [_363119, _363121, _363123, _363125, _363127, _363129] : [rdn_add_with_carry(rdnn(_363129), rdnn(_363123), rdn(rdnn(_363127), _363125), rdn(rdnn(_363121), _363119)), -(rdn_add_with_carry(rdnn(_363129), rdn(rdnn(_363127), _363125), rdnn(_363123), rdn(rdnn(_363121), _363119)))], (1076 ^ _328343) ^ [_361953, _361955, _361957, _361959, _361961, _361963, _361965, _361967, _361969, _361971, _361973] : [-(rdn_add_with_carry(rdnn(_361973), rdn(rdnn(_361971), _361969), rdn(rdnn(_361967), _361965), rdn(rdnn(_361963), _361961))), rdn_digit_add(rdnn(_361971), rdnn(_361967), rdnn(_361959), rdnn(_361957)), rdn_digit_add(rdnn(_361959), rdnn(_361973), rdnn(_361963), rdnn(_361955)), rdn_digit_add(rdnn(_361957), rdnn(_361955), rdnn(_361953), rdnn(n0)), rdn_add_with_carry(rdnn(_361953), _361969, _361965, _361961), rdn_non_zero(_361969), rdn_non_zero(_361965), rdn_non_zero(_361961)]], input).
% 0.35/1.37 ncf('1',plain,[less(nn2, n2)],start(1312 ^ 0)).
% 0.35/1.37 ncf('1.1',plain,[-(less(nn2, n2)), rdn_translate(nn2, rdn_neg(rdnn(n2))), rdn_translate(n2, rdn_pos(rdnn(n2)))],extension(810 ^ 1,bind([[_352436, _352438, _352440, _352442], [rdnn(n2), rdnn(n2), n2, nn2]]))).
% 0.35/1.37 ncf('1.1.1',plain,[-(rdn_translate(nn2, rdn_neg(rdnn(n2))))],extension(462 ^ 2)).
% 0.35/1.37 ncf('1.1.2',plain,[-(rdn_translate(n2, rdn_pos(rdnn(n2))))],extension(208 ^ 2)).
% 0.35/1.37 %-----------------------------------------------------
% 0.35/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------