%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM329+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n028.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:25 EDT 2023
% Result : Theorem 0.37s 1.39s
% Output : Proof 0.37s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.12 % Problem : NUM329+1 : TPTP v8.1.2. Released v3.1.0.
% 0.08/0.13 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n028.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu May 18 17:42:03 EDT 2023
% 0.13/0.34 % CPUTime :
% 0.37/1.39
% 0.37/1.39 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.37/1.39 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.37/1.39 %-----------------------------------------------------
% 0.37/1.39 ncf(matrix, plain, [(1312 ^ _332312) ^ [_373895] : [sum(_373895, _373895, _373895)], (176 ^ _332312) ^ [_338248, _338250] : [_338250 = _338248, -(rdn_neg(_338250) = rdn_neg(_338248))], (182 ^ _332312) ^ [_338466, _338468] : [_338468 = _338466, -(rdn_pos(_338468) = rdn_pos(_338466))], (198 ^ _332312) ^ [_339023, _339025] : [_339025 = _339023, -(rdnn(_339025) = rdnn(_339023))], (188 ^ _332312) ^ [_338712, _338714, _338716, _338718] : [-(rdn(_338718, _338714) = rdn(_338716, _338712)), _338718 = _338716, _338714 = _338712], (2 ^ _332312) ^ [_332456] : [-(_332456 = _332456)], (4 ^ _332312) ^ [_332563, _332565] : [_332565 = _332563, -(_332563 = _332565)], (10 ^ _332312) ^ [_332767, _332769, _332771] : [-(_332771 = _332767), _332771 = _332769, _332769 = _332767], (20 ^ _332312) ^ [_333080, _333082] : [-(rdn_non_zero_digit(_333080)), _333082 = _333080, rdn_non_zero_digit(_333082)], (30 ^ _332312) ^ [_333403, _333405, _333407, _333409] : [-(less(_333407, _333403)), less(_333409, _333405), _333409 = _333407, _333405 = _333403], (44 ^ _332312) ^ [_333847, _333849, _333851, _333853] : [-(less_or_equal(_333851, _333847)), less_or_equal(_333853, _333849), _333853 = _333851, _333849 = _333847], (58 ^ _332312) ^ [_334291, _334293, _334295, _334297] : [-(rdn_positive_less(_334295, _334291)), rdn_positive_less(_334297, _334293), _334297 = _334295, _334293 = _334291], (72 ^ _332312) ^ [_334735, _334737, _334739, _334741] : [-(rdn_translate(_334739, _334735)), rdn_translate(_334741, _334737), _334741 = _334739, _334737 = _334735], (86 ^ _332312) ^ [_335207, _335209, _335211, _335213, _335215, _335217] : [-(difference(_335215, _335211, _335207)), difference(_335217, _335213, _335209), _335217 = _335215, _335213 = _335211, _335209 = _335207], (104 ^ _332312) ^ [_335760, _335762] : [-(rdn_non_zero(_335760)), _335762 = _335760, rdn_non_zero(_335762)], (114 ^ _332312) ^ [_336139, _336141, _336143, _336145, _336147, _336149, _336151, _336153] : [-(rdn_add_with_carry(_336151, _336147, _336143, _336139)), rdn_add_with_carry(_336153, _336149, _336145, _336141), _336153 = _336151, _336149 = _336147, _336145 = _336143, _336141 = _336139], (158 ^ _332312) ^ [_337671, _337673, _337675, _337677, _337679, _337681] : [-(sum(_337679, _337675, _337671)), sum(_337681, _337677, _337673), _337681 = _337679, _337677 = _337675, _337673 = _337671], (136 ^ _332312) ^ [_336929, _336931, _336933, _336935, _336937, _336939, _336941, _336943] : [-(rdn_digit_add(_336941, _336937, _336933, _336929)), rdn_digit_add(_336943, _336939, _336935, _336931), _336943 = _336941, _336939 = _336937, _336935 = _336933, _336931 = _336929], (204 ^ _332312) ^ [] : [-(rdn_translate(n0, rdn_pos(rdnn(n0))))], (206 ^ _332312) ^ [] : [-(rdn_translate(n1, rdn_pos(rdnn(n1))))], (208 ^ _332312) ^ [] : [-(rdn_translate(n2, rdn_pos(rdnn(n2))))], (210 ^ _332312) ^ [] : [-(rdn_translate(n3, rdn_pos(rdnn(n3))))], (212 ^ _332312) ^ [] : [-(rdn_translate(n4, rdn_pos(rdnn(n4))))], (214 ^ _332312) ^ [] : [-(rdn_translate(n5, rdn_pos(rdnn(n5))))], (216 ^ _332312) ^ [] : [-(rdn_translate(n6, rdn_pos(rdnn(n6))))], (218 ^ _332312) ^ [] : [-(rdn_translate(n7, rdn_pos(rdnn(n7))))], (220 ^ _332312) ^ [] : [-(rdn_translate(n8, rdn_pos(rdnn(n8))))], (222 ^ _332312) ^ [] : [-(rdn_translate(n9, rdn_pos(rdnn(n9))))], (224 ^ _332312) ^ [] : [-(rdn_translate(n10, rdn_pos(rdn(rdnn(n0), rdnn(n1)))))], (226 ^ _332312) ^ [] : [-(rdn_translate(n11, rdn_pos(rdn(rdnn(n1), rdnn(n1)))))], (228 ^ _332312) ^ [] : [-(rdn_translate(n12, rdn_pos(rdn(rdnn(n2), rdnn(n1)))))], (230 ^ _332312) ^ [] : [-(rdn_translate(n13, rdn_pos(rdn(rdnn(n3), rdnn(n1)))))], (232 ^ _332312) ^ [] : [-(rdn_translate(n14, rdn_pos(rdn(rdnn(n4), rdnn(n1)))))], (234 ^ _332312) ^ [] : [-(rdn_translate(n15, rdn_pos(rdn(rdnn(n5), rdnn(n1)))))], (236 ^ _332312) ^ [] : [-(rdn_translate(n16, rdn_pos(rdn(rdnn(n6), rdnn(n1)))))], (238 ^ _332312) ^ [] : [-(rdn_translate(n17, rdn_pos(rdn(rdnn(n7), rdnn(n1)))))], (240 ^ _332312) ^ [] : [-(rdn_translate(n18, rdn_pos(rdn(rdnn(n8), rdnn(n1)))))], (242 ^ _332312) ^ [] : [-(rdn_translate(n19, rdn_pos(rdn(rdnn(n9), rdnn(n1)))))], (244 ^ _332312) ^ [] : [-(rdn_translate(n20, rdn_pos(rdn(rdnn(n0), rdnn(n2)))))], (246 ^ _332312) ^ [] : [-(rdn_translate(n21, rdn_pos(rdn(rdnn(n1), rdnn(n2)))))], (248 ^ _332312) ^ [] : [-(rdn_translate(n22, rdn_pos(rdn(rdnn(n2), rdnn(n2)))))], (250 ^ _332312) ^ [] : [-(rdn_translate(n23, rdn_pos(rdn(rdnn(n3), rdnn(n2)))))], (252 ^ _332312) ^ [] : [-(rdn_translate(n24, rdn_pos(rdn(rdnn(n4), rdnn(n2)))))], (254 ^ _332312) ^ [] : [-(rdn_translate(n25, rdn_pos(rdn(rdnn(n5), rdnn(n2)))))], (256 ^ _332312) ^ [] : [-(rdn_translate(n26, rdn_pos(rdn(rdnn(n6), rdnn(n2)))))], (258 ^ _332312) ^ [] : [-(rdn_translate(n27, rdn_pos(rdn(rdnn(n7), rdnn(n2)))))], (260 ^ _332312) ^ [] : [-(rdn_translate(n28, rdn_pos(rdn(rdnn(n8), rdnn(n2)))))], (262 ^ _332312) ^ [] : [-(rdn_translate(n29, rdn_pos(rdn(rdnn(n9), rdnn(n2)))))], (264 ^ _332312) ^ [] : [-(rdn_translate(n30, rdn_pos(rdn(rdnn(n0), rdnn(n3)))))], (266 ^ _332312) ^ [] : [-(rdn_translate(n31, rdn_pos(rdn(rdnn(n1), rdnn(n3)))))], (268 ^ _332312) ^ [] : [-(rdn_translate(n32, rdn_pos(rdn(rdnn(n2), rdnn(n3)))))], (270 ^ _332312) ^ [] : [-(rdn_translate(n33, rdn_pos(rdn(rdnn(n3), rdnn(n3)))))], (272 ^ _332312) ^ [] : [-(rdn_translate(n34, rdn_pos(rdn(rdnn(n4), rdnn(n3)))))], (274 ^ _332312) ^ [] : [-(rdn_translate(n35, rdn_pos(rdn(rdnn(n5), rdnn(n3)))))], (276 ^ _332312) ^ [] : [-(rdn_translate(n36, rdn_pos(rdn(rdnn(n6), rdnn(n3)))))], (278 ^ _332312) ^ [] : [-(rdn_translate(n37, rdn_pos(rdn(rdnn(n7), rdnn(n3)))))], (280 ^ _332312) ^ [] : [-(rdn_translate(n38, rdn_pos(rdn(rdnn(n8), rdnn(n3)))))], (282 ^ _332312) ^ [] : [-(rdn_translate(n39, rdn_pos(rdn(rdnn(n9), rdnn(n3)))))], (284 ^ _332312) ^ [] : [-(rdn_translate(n40, rdn_pos(rdn(rdnn(n0), rdnn(n4)))))], (286 ^ _332312) ^ [] : [-(rdn_translate(n41, rdn_pos(rdn(rdnn(n1), rdnn(n4)))))], (288 ^ _332312) ^ [] : [-(rdn_translate(n42, rdn_pos(rdn(rdnn(n2), rdnn(n4)))))], (290 ^ _332312) ^ [] : [-(rdn_translate(n43, rdn_pos(rdn(rdnn(n3), rdnn(n4)))))], (292 ^ _332312) ^ [] : [-(rdn_translate(n44, rdn_pos(rdn(rdnn(n4), rdnn(n4)))))], (294 ^ _332312) ^ [] : [-(rdn_translate(n45, rdn_pos(rdn(rdnn(n5), rdnn(n4)))))], (296 ^ _332312) ^ [] : [-(rdn_translate(n46, rdn_pos(rdn(rdnn(n6), rdnn(n4)))))], (298 ^ _332312) ^ [] : [-(rdn_translate(n47, rdn_pos(rdn(rdnn(n7), rdnn(n4)))))], (300 ^ _332312) ^ [] : [-(rdn_translate(n48, rdn_pos(rdn(rdnn(n8), rdnn(n4)))))], (302 ^ _332312) ^ [] : [-(rdn_translate(n49, rdn_pos(rdn(rdnn(n9), rdnn(n4)))))], (304 ^ _332312) ^ [] : [-(rdn_translate(n50, rdn_pos(rdn(rdnn(n0), rdnn(n5)))))], (306 ^ _332312) ^ [] : [-(rdn_translate(n51, rdn_pos(rdn(rdnn(n1), rdnn(n5)))))], (308 ^ _332312) ^ [] : [-(rdn_translate(n52, rdn_pos(rdn(rdnn(n2), rdnn(n5)))))], (310 ^ _332312) ^ [] : [-(rdn_translate(n53, rdn_pos(rdn(rdnn(n3), rdnn(n5)))))], (312 ^ _332312) ^ [] : [-(rdn_translate(n54, rdn_pos(rdn(rdnn(n4), rdnn(n5)))))], (314 ^ _332312) ^ [] : [-(rdn_translate(n55, rdn_pos(rdn(rdnn(n5), rdnn(n5)))))], (316 ^ _332312) ^ [] : [-(rdn_translate(n56, rdn_pos(rdn(rdnn(n6), rdnn(n5)))))], (318 ^ _332312) ^ [] : [-(rdn_translate(n57, rdn_pos(rdn(rdnn(n7), rdnn(n5)))))], (320 ^ _332312) ^ [] : [-(rdn_translate(n58, rdn_pos(rdn(rdnn(n8), rdnn(n5)))))], (322 ^ _332312) ^ [] : [-(rdn_translate(n59, rdn_pos(rdn(rdnn(n9), rdnn(n5)))))], (324 ^ _332312) ^ [] : [-(rdn_translate(n60, rdn_pos(rdn(rdnn(n0), rdnn(n6)))))], (326 ^ _332312) ^ [] : [-(rdn_translate(n61, rdn_pos(rdn(rdnn(n1), rdnn(n6)))))], (328 ^ _332312) ^ [] : [-(rdn_translate(n62, rdn_pos(rdn(rdnn(n2), rdnn(n6)))))], (330 ^ _332312) ^ [] : [-(rdn_translate(n63, rdn_pos(rdn(rdnn(n3), rdnn(n6)))))], (332 ^ _332312) ^ [] : [-(rdn_translate(n64, rdn_pos(rdn(rdnn(n4), rdnn(n6)))))], (334 ^ _332312) ^ [] : [-(rdn_translate(n65, rdn_pos(rdn(rdnn(n5), rdnn(n6)))))], (336 ^ _332312) ^ [] : [-(rdn_translate(n66, rdn_pos(rdn(rdnn(n6), rdnn(n6)))))], (338 ^ _332312) ^ [] : [-(rdn_translate(n67, rdn_pos(rdn(rdnn(n7), rdnn(n6)))))], (340 ^ _332312) ^ [] : [-(rdn_translate(n68, rdn_pos(rdn(rdnn(n8), rdnn(n6)))))], (342 ^ _332312) ^ [] : [-(rdn_translate(n69, rdn_pos(rdn(rdnn(n9), rdnn(n6)))))], (344 ^ _332312) ^ [] : [-(rdn_translate(n70, rdn_pos(rdn(rdnn(n0), rdnn(n7)))))], (346 ^ _332312) ^ [] : [-(rdn_translate(n71, rdn_pos(rdn(rdnn(n1), rdnn(n7)))))], (348 ^ _332312) ^ [] : [-(rdn_translate(n72, rdn_pos(rdn(rdnn(n2), rdnn(n7)))))], (350 ^ _332312) ^ [] : [-(rdn_translate(n73, rdn_pos(rdn(rdnn(n3), rdnn(n7)))))], (352 ^ _332312) ^ [] : [-(rdn_translate(n74, rdn_pos(rdn(rdnn(n4), rdnn(n7)))))], (354 ^ _332312) ^ [] : [-(rdn_translate(n75, rdn_pos(rdn(rdnn(n5), rdnn(n7)))))], (356 ^ _332312) ^ [] : [-(rdn_translate(n76, rdn_pos(rdn(rdnn(n6), rdnn(n7)))))], (358 ^ _332312) ^ [] : [-(rdn_translate(n77, rdn_pos(rdn(rdnn(n7), rdnn(n7)))))], (360 ^ _332312) ^ [] : [-(rdn_translate(n78, rdn_pos(rdn(rdnn(n8), rdnn(n7)))))], (362 ^ _332312) ^ [] : [-(rdn_translate(n79, rdn_pos(rdn(rdnn(n9), rdnn(n7)))))], (364 ^ _332312) ^ [] : [-(rdn_translate(n80, rdn_pos(rdn(rdnn(n0), rdnn(n8)))))], (366 ^ _332312) ^ [] : [-(rdn_translate(n81, rdn_pos(rdn(rdnn(n1), rdnn(n8)))))], (368 ^ _332312) ^ [] : [-(rdn_translate(n82, rdn_pos(rdn(rdnn(n2), rdnn(n8)))))], (370 ^ _332312) ^ [] : [-(rdn_translate(n83, rdn_pos(rdn(rdnn(n3), rdnn(n8)))))], (372 ^ _332312) ^ [] : [-(rdn_translate(n84, rdn_pos(rdn(rdnn(n4), rdnn(n8)))))], (374 ^ _332312) ^ [] : [-(rdn_translate(n85, rdn_pos(rdn(rdnn(n5), rdnn(n8)))))], (376 ^ _332312) ^ [] : [-(rdn_translate(n86, rdn_pos(rdn(rdnn(n6), rdnn(n8)))))], (378 ^ _332312) ^ [] : [-(rdn_translate(n87, rdn_pos(rdn(rdnn(n7), rdnn(n8)))))], (380 ^ _332312) ^ [] : [-(rdn_translate(n88, rdn_pos(rdn(rdnn(n8), rdnn(n8)))))], (382 ^ _332312) ^ [] : [-(rdn_translate(n89, rdn_pos(rdn(rdnn(n9), rdnn(n8)))))], (384 ^ _332312) ^ [] : [-(rdn_translate(n90, rdn_pos(rdn(rdnn(n0), rdnn(n9)))))], (386 ^ _332312) ^ [] : [-(rdn_translate(n91, rdn_pos(rdn(rdnn(n1), rdnn(n9)))))], (388 ^ _332312) ^ [] : [-(rdn_translate(n92, rdn_pos(rdn(rdnn(n2), rdnn(n9)))))], (390 ^ _332312) ^ [] : [-(rdn_translate(n93, rdn_pos(rdn(rdnn(n3), rdnn(n9)))))], (392 ^ _332312) ^ [] : [-(rdn_translate(n94, rdn_pos(rdn(rdnn(n4), rdnn(n9)))))], (394 ^ _332312) ^ [] : [-(rdn_translate(n95, rdn_pos(rdn(rdnn(n5), rdnn(n9)))))], (396 ^ _332312) ^ [] : [-(rdn_translate(n96, rdn_pos(rdn(rdnn(n6), rdnn(n9)))))], (398 ^ _332312) ^ [] : [-(rdn_translate(n97, rdn_pos(rdn(rdnn(n7), rdnn(n9)))))], (400 ^ _332312) ^ [] : [-(rdn_translate(n98, rdn_pos(rdn(rdnn(n8), rdnn(n9)))))], (402 ^ _332312) ^ [] : [-(rdn_translate(n99, rdn_pos(rdn(rdnn(n9), rdnn(n9)))))], (404 ^ _332312) ^ [] : [-(rdn_translate(n100, rdn_pos(rdn(rdnn(n0), rdn(rdnn(n0), rdnn(n1))))))], (406 ^ _332312) ^ [] : [-(rdn_translate(n101, rdn_pos(rdn(rdnn(n1), rdn(rdnn(n0), rdnn(n1))))))], (408 ^ _332312) ^ [] : [-(rdn_translate(n102, rdn_pos(rdn(rdnn(n2), rdn(rdnn(n0), rdnn(n1))))))], (410 ^ _332312) ^ [] : [-(rdn_translate(n103, rdn_pos(rdn(rdnn(n3), rdn(rdnn(n0), rdnn(n1))))))], (412 ^ _332312) ^ [] : [-(rdn_translate(n104, rdn_pos(rdn(rdnn(n4), rdn(rdnn(n0), rdnn(n1))))))], (414 ^ _332312) ^ [] : [-(rdn_translate(n105, rdn_pos(rdn(rdnn(n5), rdn(rdnn(n0), rdnn(n1))))))], (416 ^ _332312) ^ [] : [-(rdn_translate(n106, rdn_pos(rdn(rdnn(n6), rdn(rdnn(n0), rdnn(n1))))))], (418 ^ _332312) ^ [] : [-(rdn_translate(n107, rdn_pos(rdn(rdnn(n7), rdn(rdnn(n0), rdnn(n1))))))], (420 ^ _332312) ^ [] : [-(rdn_translate(n108, rdn_pos(rdn(rdnn(n8), rdn(rdnn(n0), rdnn(n1))))))], (422 ^ _332312) ^ [] : [-(rdn_translate(n109, rdn_pos(rdn(rdnn(n9), rdn(rdnn(n0), rdnn(n1))))))], (424 ^ _332312) ^ [] : [-(rdn_translate(n110, rdn_pos(rdn(rdnn(n0), rdn(rdnn(n1), rdnn(n1))))))], (426 ^ _332312) ^ [] : [-(rdn_translate(n111, rdn_pos(rdn(rdnn(n1), rdn(rdnn(n1), rdnn(n1))))))], (428 ^ _332312) ^ [] : [-(rdn_translate(n112, rdn_pos(rdn(rdnn(n2), rdn(rdnn(n1), rdnn(n1))))))], (430 ^ _332312) ^ [] : [-(rdn_translate(n113, rdn_pos(rdn(rdnn(n3), rdn(rdnn(n1), rdnn(n1))))))], (432 ^ _332312) ^ [] : [-(rdn_translate(n114, rdn_pos(rdn(rdnn(n4), rdn(rdnn(n1), rdnn(n1))))))], (434 ^ _332312) ^ [] : [-(rdn_translate(n115, rdn_pos(rdn(rdnn(n5), rdn(rdnn(n1), rdnn(n1))))))], (436 ^ _332312) ^ [] : [-(rdn_translate(n116, rdn_pos(rdn(rdnn(n6), rdn(rdnn(n1), rdnn(n1))))))], (438 ^ _332312) ^ [] : [-(rdn_translate(n117, rdn_pos(rdn(rdnn(n7), rdn(rdnn(n1), rdnn(n1))))))], (440 ^ _332312) ^ [] : [-(rdn_translate(n118, rdn_pos(rdn(rdnn(n8), rdn(rdnn(n1), rdnn(n1))))))], (442 ^ _332312) ^ [] : [-(rdn_translate(n119, rdn_pos(rdn(rdnn(n9), rdn(rdnn(n1), rdnn(n1))))))], (444 ^ _332312) ^ [] : [-(rdn_translate(n120, rdn_pos(rdn(rdnn(n0), rdn(rdnn(n2), rdnn(n1))))))], (446 ^ _332312) ^ [] : [-(rdn_translate(n121, rdn_pos(rdn(rdnn(n1), rdn(rdnn(n2), rdnn(n1))))))], (448 ^ _332312) ^ [] : [-(rdn_translate(n122, rdn_pos(rdn(rdnn(n2), rdn(rdnn(n2), rdnn(n1))))))], (450 ^ _332312) ^ [] : [-(rdn_translate(n123, rdn_pos(rdn(rdnn(n3), rdn(rdnn(n2), rdnn(n1))))))], (452 ^ _332312) ^ [] : [-(rdn_translate(n124, rdn_pos(rdn(rdnn(n4), rdn(rdnn(n2), rdnn(n1))))))], (454 ^ _332312) ^ [] : [-(rdn_translate(n125, rdn_pos(rdn(rdnn(n5), rdn(rdnn(n2), rdnn(n1))))))], (456 ^ _332312) ^ [] : [-(rdn_translate(n126, rdn_pos(rdn(rdnn(n6), rdn(rdnn(n2), rdnn(n1))))))], (458 ^ _332312) ^ [] : [-(rdn_translate(n127, rdn_pos(rdn(rdnn(n7), rdn(rdnn(n2), rdnn(n1))))))], (460 ^ _332312) ^ [] : [-(rdn_translate(nn1, rdn_neg(rdnn(n1))))], (462 ^ _332312) ^ [] : [-(rdn_translate(nn2, rdn_neg(rdnn(n2))))], (464 ^ _332312) ^ [] : [-(rdn_translate(nn3, rdn_neg(rdnn(n3))))], (466 ^ _332312) ^ [] : [-(rdn_translate(nn4, rdn_neg(rdnn(n4))))], (468 ^ _332312) ^ [] : [-(rdn_translate(nn5, rdn_neg(rdnn(n5))))], (470 ^ _332312) ^ [] : [-(rdn_translate(nn6, rdn_neg(rdnn(n6))))], (472 ^ _332312) ^ [] : [-(rdn_translate(nn7, rdn_neg(rdnn(n7))))], (474 ^ _332312) ^ [] : [-(rdn_translate(nn8, rdn_neg(rdnn(n8))))], (476 ^ _332312) ^ [] : [-(rdn_translate(nn9, rdn_neg(rdnn(n9))))], (478 ^ _332312) ^ [] : [-(rdn_translate(nn10, rdn_neg(rdn(rdnn(n0), rdnn(n1)))))], (480 ^ _332312) ^ [] : [-(rdn_translate(nn11, rdn_neg(rdn(rdnn(n1), rdnn(n1)))))], (482 ^ _332312) ^ [] : [-(rdn_translate(nn12, rdn_neg(rdn(rdnn(n2), rdnn(n1)))))], (484 ^ _332312) ^ [] : [-(rdn_translate(nn13, rdn_neg(rdn(rdnn(n3), rdnn(n1)))))], (486 ^ _332312) ^ [] : [-(rdn_translate(nn14, rdn_neg(rdn(rdnn(n4), rdnn(n1)))))], (488 ^ _332312) ^ [] : [-(rdn_translate(nn15, rdn_neg(rdn(rdnn(n5), rdnn(n1)))))], (490 ^ _332312) ^ [] : [-(rdn_translate(nn16, rdn_neg(rdn(rdnn(n6), rdnn(n1)))))], (492 ^ _332312) ^ [] : [-(rdn_translate(nn17, rdn_neg(rdn(rdnn(n7), rdnn(n1)))))], (494 ^ _332312) ^ [] : [-(rdn_translate(nn18, rdn_neg(rdn(rdnn(n8), rdnn(n1)))))], (496 ^ _332312) ^ [] : [-(rdn_translate(nn19, rdn_neg(rdn(rdnn(n9), rdnn(n1)))))], (498 ^ _332312) ^ [] : [-(rdn_translate(nn20, rdn_neg(rdn(rdnn(n0), rdnn(n2)))))], (500 ^ _332312) ^ [] : [-(rdn_translate(nn21, rdn_neg(rdn(rdnn(n1), rdnn(n2)))))], (502 ^ _332312) ^ [] : [-(rdn_translate(nn22, rdn_neg(rdn(rdnn(n2), rdnn(n2)))))], (504 ^ _332312) ^ [] : [-(rdn_translate(nn23, rdn_neg(rdn(rdnn(n3), rdnn(n2)))))], (506 ^ _332312) ^ [] : [-(rdn_translate(nn24, rdn_neg(rdn(rdnn(n4), rdnn(n2)))))], (508 ^ _332312) ^ [] : [-(rdn_translate(nn25, rdn_neg(rdn(rdnn(n5), rdnn(n2)))))], (510 ^ _332312) ^ [] : [-(rdn_translate(nn26, rdn_neg(rdn(rdnn(n6), rdnn(n2)))))], (512 ^ _332312) ^ [] : [-(rdn_translate(nn27, rdn_neg(rdn(rdnn(n7), rdnn(n2)))))], (514 ^ _332312) ^ [] : [-(rdn_translate(nn28, rdn_neg(rdn(rdnn(n8), rdnn(n2)))))], (516 ^ _332312) ^ [] : [-(rdn_translate(nn29, rdn_neg(rdn(rdnn(n9), rdnn(n2)))))], (518 ^ _332312) ^ [] : [-(rdn_translate(nn30, rdn_neg(rdn(rdnn(n0), rdnn(n3)))))], (520 ^ _332312) ^ [] : [-(rdn_translate(nn31, rdn_neg(rdn(rdnn(n1), rdnn(n3)))))], (522 ^ _332312) ^ [] : [-(rdn_translate(nn32, rdn_neg(rdn(rdnn(n2), rdnn(n3)))))], (524 ^ _332312) ^ [] : [-(rdn_translate(nn33, rdn_neg(rdn(rdnn(n3), rdnn(n3)))))], (526 ^ _332312) ^ [] : [-(rdn_translate(nn34, rdn_neg(rdn(rdnn(n4), rdnn(n3)))))], (528 ^ _332312) ^ [] : [-(rdn_translate(nn35, rdn_neg(rdn(rdnn(n5), rdnn(n3)))))], (530 ^ _332312) ^ [] : [-(rdn_translate(nn36, rdn_neg(rdn(rdnn(n6), rdnn(n3)))))], (532 ^ _332312) ^ [] : [-(rdn_translate(nn37, rdn_neg(rdn(rdnn(n7), rdnn(n3)))))], (534 ^ _332312) ^ [] : [-(rdn_translate(nn38, rdn_neg(rdn(rdnn(n8), rdnn(n3)))))], (536 ^ _332312) ^ [] : [-(rdn_translate(nn39, rdn_neg(rdn(rdnn(n9), rdnn(n3)))))], (538 ^ _332312) ^ [] : [-(rdn_translate(nn40, rdn_neg(rdn(rdnn(n0), rdnn(n4)))))], (540 ^ _332312) ^ [] : [-(rdn_translate(nn41, rdn_neg(rdn(rdnn(n1), rdnn(n4)))))], (542 ^ _332312) ^ [] : [-(rdn_translate(nn42, rdn_neg(rdn(rdnn(n2), rdnn(n4)))))], (544 ^ _332312) ^ [] : [-(rdn_translate(nn43, rdn_neg(rdn(rdnn(n3), rdnn(n4)))))], (546 ^ _332312) ^ [] : [-(rdn_translate(nn44, rdn_neg(rdn(rdnn(n4), rdnn(n4)))))], (548 ^ _332312) ^ [] : [-(rdn_translate(nn45, rdn_neg(rdn(rdnn(n5), rdnn(n4)))))], (550 ^ _332312) ^ [] : [-(rdn_translate(nn46, rdn_neg(rdn(rdnn(n6), rdnn(n4)))))], (552 ^ _332312) ^ [] : [-(rdn_translate(nn47, rdn_neg(rdn(rdnn(n7), rdnn(n4)))))], (554 ^ _332312) ^ [] : [-(rdn_translate(nn48, rdn_neg(rdn(rdnn(n8), rdnn(n4)))))], (556 ^ _332312) ^ [] : [-(rdn_translate(nn49, rdn_neg(rdn(rdnn(n9), rdnn(n4)))))], (558 ^ _332312) ^ [] : [-(rdn_translate(nn50, rdn_neg(rdn(rdnn(n0), rdnn(n5)))))], (560 ^ _332312) ^ [] : [-(rdn_translate(nn51, rdn_neg(rdn(rdnn(n1), rdnn(n5)))))], (562 ^ _332312) ^ [] : [-(rdn_translate(nn52, rdn_neg(rdn(rdnn(n2), rdnn(n5)))))], (564 ^ _332312) ^ [] : [-(rdn_translate(nn53, rdn_neg(rdn(rdnn(n3), rdnn(n5)))))], (566 ^ _332312) ^ [] : [-(rdn_translate(nn54, rdn_neg(rdn(rdnn(n4), rdnn(n5)))))], (568 ^ _332312) ^ [] : [-(rdn_translate(nn55, rdn_neg(rdn(rdnn(n5), rdnn(n5)))))], (570 ^ _332312) ^ [] : [-(rdn_translate(nn56, rdn_neg(rdn(rdnn(n6), rdnn(n5)))))], (572 ^ _332312) ^ [] : [-(rdn_translate(nn57, rdn_neg(rdn(rdnn(n7), rdnn(n5)))))], (574 ^ _332312) ^ [] : [-(rdn_translate(nn58, rdn_neg(rdn(rdnn(n8), rdnn(n5)))))], (576 ^ _332312) ^ [] : [-(rdn_translate(nn59, rdn_neg(rdn(rdnn(n9), rdnn(n5)))))], (578 ^ _332312) ^ [] : [-(rdn_translate(nn60, rdn_neg(rdn(rdnn(n0), rdnn(n6)))))], (580 ^ _332312) ^ [] : [-(rdn_translate(nn61, rdn_neg(rdn(rdnn(n1), rdnn(n6)))))], (582 ^ _332312) ^ [] : [-(rdn_translate(nn62, rdn_neg(rdn(rdnn(n2), rdnn(n6)))))], (584 ^ _332312) ^ [] : [-(rdn_translate(nn63, rdn_neg(rdn(rdnn(n3), rdnn(n6)))))], (586 ^ _332312) ^ [] : [-(rdn_translate(nn64, rdn_neg(rdn(rdnn(n4), rdnn(n6)))))], (588 ^ _332312) ^ [] : [-(rdn_translate(nn65, rdn_neg(rdn(rdnn(n5), rdnn(n6)))))], (590 ^ _332312) ^ [] : [-(rdn_translate(nn66, rdn_neg(rdn(rdnn(n6), rdnn(n6)))))], (592 ^ _332312) ^ [] : [-(rdn_translate(nn67, rdn_neg(rdn(rdnn(n7), rdnn(n6)))))], (594 ^ _332312) ^ [] : [-(rdn_translate(nn68, rdn_neg(rdn(rdnn(n8), rdnn(n6)))))], (596 ^ _332312) ^ [] : [-(rdn_translate(nn69, rdn_neg(rdn(rdnn(n9), rdnn(n6)))))], (598 ^ _332312) ^ [] : [-(rdn_translate(nn70, rdn_neg(rdn(rdnn(n0), rdnn(n7)))))], (600 ^ _332312) ^ [] : [-(rdn_translate(nn71, rdn_neg(rdn(rdnn(n1), rdnn(n7)))))], (602 ^ _332312) ^ [] : [-(rdn_translate(nn72, rdn_neg(rdn(rdnn(n2), rdnn(n7)))))], (604 ^ _332312) ^ [] : [-(rdn_translate(nn73, rdn_neg(rdn(rdnn(n3), rdnn(n7)))))], (606 ^ _332312) ^ [] : [-(rdn_translate(nn74, rdn_neg(rdn(rdnn(n4), rdnn(n7)))))], (608 ^ _332312) ^ [] : [-(rdn_translate(nn75, rdn_neg(rdn(rdnn(n5), rdnn(n7)))))], (610 ^ _332312) ^ [] : [-(rdn_translate(nn76, rdn_neg(rdn(rdnn(n6), rdnn(n7)))))], (612 ^ _332312) ^ [] : [-(rdn_translate(nn77, rdn_neg(rdn(rdnn(n7), rdnn(n7)))))], (614 ^ _332312) ^ [] : [-(rdn_translate(nn78, rdn_neg(rdn(rdnn(n8), rdnn(n7)))))], (616 ^ _332312) ^ [] : [-(rdn_translate(nn79, rdn_neg(rdn(rdnn(n9), rdnn(n7)))))], (618 ^ _332312) ^ [] : [-(rdn_translate(nn80, rdn_neg(rdn(rdnn(n0), rdnn(n8)))))], (620 ^ _332312) ^ [] : [-(rdn_translate(nn81, rdn_neg(rdn(rdnn(n1), rdnn(n8)))))], (622 ^ _332312) ^ [] : [-(rdn_translate(nn82, rdn_neg(rdn(rdnn(n2), rdnn(n8)))))], (624 ^ _332312) ^ [] : [-(rdn_translate(nn83, rdn_neg(rdn(rdnn(n3), rdnn(n8)))))], (626 ^ _332312) ^ [] : [-(rdn_translate(nn84, rdn_neg(rdn(rdnn(n4), rdnn(n8)))))], (628 ^ _332312) ^ [] : [-(rdn_translate(nn85, rdn_neg(rdn(rdnn(n5), rdnn(n8)))))], (630 ^ _332312) ^ [] : [-(rdn_translate(nn86, rdn_neg(rdn(rdnn(n6), rdnn(n8)))))], (632 ^ _332312) ^ [] : [-(rdn_translate(nn87, rdn_neg(rdn(rdnn(n7), rdnn(n8)))))], (634 ^ _332312) ^ [] : [-(rdn_translate(nn88, rdn_neg(rdn(rdnn(n8), rdnn(n8)))))], (636 ^ _332312) ^ [] : [-(rdn_translate(nn89, rdn_neg(rdn(rdnn(n9), rdnn(n8)))))], (638 ^ _332312) ^ [] : [-(rdn_translate(nn90, rdn_neg(rdn(rdnn(n0), rdnn(n9)))))], (640 ^ _332312) ^ [] : [-(rdn_translate(nn91, rdn_neg(rdn(rdnn(n1), rdnn(n9)))))], (642 ^ _332312) ^ [] : [-(rdn_translate(nn92, rdn_neg(rdn(rdnn(n2), rdnn(n9)))))], (644 ^ _332312) ^ [] : [-(rdn_translate(nn93, rdn_neg(rdn(rdnn(n3), rdnn(n9)))))], (646 ^ _332312) ^ [] : [-(rdn_translate(nn94, rdn_neg(rdn(rdnn(n4), rdnn(n9)))))], (648 ^ _332312) ^ [] : [-(rdn_translate(nn95, rdn_neg(rdn(rdnn(n5), rdnn(n9)))))], (650 ^ _332312) ^ [] : [-(rdn_translate(nn96, rdn_neg(rdn(rdnn(n6), rdnn(n9)))))], (652 ^ _332312) ^ [] : [-(rdn_translate(nn97, rdn_neg(rdn(rdnn(n7), rdnn(n9)))))], (654 ^ _332312) ^ [] : [-(rdn_translate(nn98, rdn_neg(rdn(rdnn(n8), rdnn(n9)))))], (656 ^ _332312) ^ [] : [-(rdn_translate(nn99, rdn_neg(rdn(rdnn(n9), rdnn(n9)))))], (658 ^ _332312) ^ [] : [-(rdn_translate(nn100, rdn_neg(rdn(rdnn(n0), rdn(rdnn(n0), rdnn(n1))))))], (660 ^ _332312) ^ [] : [-(rdn_translate(nn101, rdn_neg(rdn(rdnn(n1), rdn(rdnn(n0), rdnn(n1))))))], (662 ^ _332312) ^ [] : [-(rdn_translate(nn102, rdn_neg(rdn(rdnn(n2), rdn(rdnn(n0), rdnn(n1))))))], (664 ^ _332312) ^ [] : [-(rdn_translate(nn103, rdn_neg(rdn(rdnn(n3), rdn(rdnn(n0), rdnn(n1))))))], (666 ^ _332312) ^ [] : [-(rdn_translate(nn104, rdn_neg(rdn(rdnn(n4), rdn(rdnn(n0), rdnn(n1))))))], (668 ^ _332312) ^ [] : [-(rdn_translate(nn105, rdn_neg(rdn(rdnn(n5), rdn(rdnn(n0), rdnn(n1))))))], (670 ^ _332312) ^ [] : [-(rdn_translate(nn106, rdn_neg(rdn(rdnn(n6), rdn(rdnn(n0), rdnn(n1))))))], (672 ^ _332312) ^ [] : [-(rdn_translate(nn107, rdn_neg(rdn(rdnn(n7), rdn(rdnn(n0), rdnn(n1))))))], (674 ^ _332312) ^ [] : [-(rdn_translate(nn108, rdn_neg(rdn(rdnn(n8), rdn(rdnn(n0), rdnn(n1))))))], (676 ^ _332312) ^ [] : [-(rdn_translate(nn109, rdn_neg(rdn(rdnn(n9), rdn(rdnn(n0), rdnn(n1))))))], (678 ^ _332312) ^ [] : [-(rdn_translate(nn110, rdn_neg(rdn(rdnn(n0), rdn(rdnn(n1), rdnn(n1))))))], (680 ^ _332312) ^ [] : [-(rdn_translate(nn111, rdn_neg(rdn(rdnn(n1), rdn(rdnn(n1), rdnn(n1))))))], (682 ^ _332312) ^ [] : [-(rdn_translate(nn112, rdn_neg(rdn(rdnn(n2), rdn(rdnn(n1), rdnn(n1))))))], (684 ^ _332312) ^ [] : [-(rdn_translate(nn113, rdn_neg(rdn(rdnn(n3), rdn(rdnn(n1), rdnn(n1))))))], (686 ^ _332312) ^ [] : [-(rdn_translate(nn114, rdn_neg(rdn(rdnn(n4), rdn(rdnn(n1), rdnn(n1))))))], (688 ^ _332312) ^ [] : [-(rdn_translate(nn115, rdn_neg(rdn(rdnn(n5), rdn(rdnn(n1), rdnn(n1))))))], (690 ^ _332312) ^ [] : [-(rdn_translate(nn116, rdn_neg(rdn(rdnn(n6), rdn(rdnn(n1), rdnn(n1))))))], (692 ^ _332312) ^ [] : [-(rdn_translate(nn117, rdn_neg(rdn(rdnn(n7), rdn(rdnn(n1), rdnn(n1))))))], (694 ^ _332312) ^ [] : [-(rdn_translate(nn118, rdn_neg(rdn(rdnn(n8), rdn(rdnn(n1), rdnn(n1))))))], (696 ^ _332312) ^ [] : [-(rdn_translate(nn119, rdn_neg(rdn(rdnn(n9), rdn(rdnn(n1), rdnn(n1))))))], (698 ^ _332312) ^ [] : [-(rdn_translate(nn120, rdn_neg(rdn(rdnn(n0), rdn(rdnn(n2), rdnn(n1))))))], (700 ^ _332312) ^ [] : [-(rdn_translate(nn121, rdn_neg(rdn(rdnn(n1), rdn(rdnn(n2), rdnn(n1))))))], (702 ^ _332312) ^ [] : [-(rdn_translate(nn122, rdn_neg(rdn(rdnn(n2), rdn(rdnn(n2), rdnn(n1))))))], (704 ^ _332312) ^ [] : [-(rdn_translate(nn123, rdn_neg(rdn(rdnn(n3), rdn(rdnn(n2), rdnn(n1))))))], (706 ^ _332312) ^ [] : [-(rdn_translate(nn124, rdn_neg(rdn(rdnn(n4), rdn(rdnn(n2), rdnn(n1))))))], (708 ^ _332312) ^ [] : [-(rdn_translate(nn125, rdn_neg(rdn(rdnn(n5), rdn(rdnn(n2), rdnn(n1))))))], (710 ^ _332312) ^ [] : [-(rdn_translate(nn126, rdn_neg(rdn(rdnn(n6), rdn(rdnn(n2), rdnn(n1))))))], (712 ^ _332312) ^ [] : [-(rdn_translate(nn127, rdn_neg(rdn(rdnn(n7), rdn(rdnn(n2), rdnn(n1))))))], (714 ^ _332312) ^ [] : [-(rdn_translate(nn128, rdn_neg(rdn(rdnn(n8), rdn(rdnn(n2), rdnn(n1))))))], (716 ^ _332312) ^ [] : [-(rdn_non_zero_digit(rdnn(n1)))], (718 ^ _332312) ^ [] : [-(rdn_non_zero_digit(rdnn(n2)))], (720 ^ _332312) ^ [] : [-(rdn_non_zero_digit(rdnn(n3)))], (722 ^ _332312) ^ [] : [-(rdn_non_zero_digit(rdnn(n4)))], (724 ^ _332312) ^ [] : [-(rdn_non_zero_digit(rdnn(n5)))], (726 ^ _332312) ^ [] : [-(rdn_non_zero_digit(rdnn(n6)))], (728 ^ _332312) ^ [] : [-(rdn_non_zero_digit(rdnn(n7)))], (730 ^ _332312) ^ [] : [-(rdn_non_zero_digit(rdnn(n8)))], (732 ^ _332312) ^ [] : [-(rdn_non_zero_digit(rdnn(n9)))], (734 ^ _332312) ^ [] : [-(rdn_positive_less(rdnn(n0), rdnn(n1)))], (736 ^ _332312) ^ [] : [-(rdn_positive_less(rdnn(n1), rdnn(n2)))], (738 ^ _332312) ^ [] : [-(rdn_positive_less(rdnn(n2), rdnn(n3)))], (740 ^ _332312) ^ [] : [-(rdn_positive_less(rdnn(n3), rdnn(n4)))], (742 ^ _332312) ^ [] : [-(rdn_positive_less(rdnn(n4), rdnn(n5)))], (744 ^ _332312) ^ [] : [-(rdn_positive_less(rdnn(n5), rdnn(n6)))], (746 ^ _332312) ^ [] : [-(rdn_positive_less(rdnn(n6), rdnn(n7)))], (748 ^ _332312) ^ [] : [-(rdn_positive_less(rdnn(n7), rdnn(n8)))], (750 ^ _332312) ^ [] : [-(rdn_positive_less(rdnn(n8), rdnn(n9)))], (752 ^ _332312) ^ [_354321, _354323, _354325] : [-(rdn_positive_less(rdnn(_354325), rdnn(_354321))), rdn_positive_less(rdnn(_354325), rdnn(_354323)), rdn_positive_less(rdnn(_354323), rdnn(_354321))], (762 ^ _332312) ^ [_354682, _354684, _354686, _354688] : [rdn_positive_less(_354686, _354682), -(rdn_positive_less(rdn(rdnn(_354688), _354686), rdn(rdnn(_354684), _354682)))], (768 ^ _332312) ^ [_354938, _354940, _354942] : [-(rdn_positive_less(rdn(rdnn(_354942), _354940), rdn(rdnn(_354938), _354940))), rdn_positive_less(rdnn(_354942), rdnn(_354938)), rdn_non_zero(_354940)], (778 ^ _332312) ^ [_355287, _355289, _355291] : [rdn_non_zero(_355287), -(rdn_positive_less(rdnn(_355291), rdn(rdnn(_355289), _355287)))], (784 ^ _332312) ^ [_355501] : [rdn_non_zero_digit(rdnn(_355501)), -(rdn_non_zero(rdnn(_355501)))], (790 ^ _332312) ^ [_355709, _355711] : [rdn_non_zero(_355709), -(rdn_non_zero(rdn(rdnn(_355711), _355709)))], (796 ^ _332312) ^ [_355953, _355955, _355957, _355959] : [-(less(_355959, _355957)), rdn_translate(_355959, rdn_pos(_355955)), rdn_translate(_355957, rdn_pos(_355953)), rdn_positive_less(_355955, _355953)], (810 ^ _332312) ^ [_356405, _356407, _356409, _356411] : [-(less(_356411, _356409)), rdn_translate(_356411, rdn_neg(_356407)), rdn_translate(_356409, rdn_pos(_356405))], (820 ^ _332312) ^ [_356760, _356762, _356764, _356766] : [-(less(_356766, _356764)), rdn_translate(_356766, rdn_neg(_356762)), rdn_translate(_356764, rdn_neg(_356760)), rdn_positive_less(_356760, _356762)], (834 ^ _332312) ^ [_357213, _357215] : [less(_357215, _357213), 837 ^ _332312 : [(838 ^ _332312) ^ [] : [less(_357213, _357215)], (840 ^ _332312) ^ [] : [_357213 = _357215]]], (842 ^ _332312) ^ [_357452, _357454] : [-(less(_357454, _357452)), -(less(_357452, _357454)), -(_357452 = _357454)], (870 ^ _332312) ^ [_358320, _358322, _358324] : [-(less_or_equal(_358320, _358324)), sum(_358324, n1, _358322), less(_358320, _358322)], (862 ^ _332312) ^ [_358040, _358042] : [863 ^ _332312 : [(864 ^ _332312) ^ [] : [less(_358042, _358040)], (866 ^ _332312) ^ [] : [_358042 = _358040]], -(less_or_equal(_358042, _358040))], (852 ^ _332312) ^ [_357788, _357790] : [less_or_equal(_357790, _357788), -(less(_357790, _357788)), -(_357790 = _357788)], (880 ^ _332312) ^ [_358747, _358749, _358751, _358753, _358755, _358757] : [-(sum(_358757, _358755, _358753)), rdn_translate(_358757, rdn_pos(_358751)), rdn_translate(_358755, rdn_pos(_358749)), rdn_add_with_carry(rdnn(n0), _358751, _358749, _358747), rdn_translate(_358753, rdn_pos(_358747))], (898 ^ _332312) ^ [_359370, _359372, _359374, _359376, _359378, _359380] : [-(sum(_359380, _359378, _359376)), rdn_translate(_359380, rdn_neg(_359374)), rdn_translate(_359378, rdn_neg(_359372)), rdn_add_with_carry(rdnn(n0), _359374, _359372, _359370), rdn_translate(_359376, rdn_neg(_359370))], (916 ^ _332312) ^ [_359993, _359995, _359997, _359999, _360001, _360003] : [-(sum(_360003, _360001, _359999)), rdn_translate(_360003, rdn_pos(_359997)), rdn_translate(_360001, rdn_neg(_359995)), rdn_positive_less(_359997, _359995), rdn_add_with_carry(rdnn(n0), _359997, _359993, _359995), rdn_translate(_359999, rdn_neg(_359993))], (938 ^ _332312) ^ [_360721, _360723, _360725, _360727, _360729, _360731] : [-(sum(_360731, _360729, _360727)), rdn_translate(_360731, rdn_pos(_360725)), rdn_translate(_360729, rdn_neg(_360723)), rdn_positive_less(_360723, _360725), rdn_add_with_carry(rdnn(n0), _360723, _360721, _360725), rdn_translate(_360727, rdn_pos(_360721))], (960 ^ _332312) ^ [_361407, _361409, _361411] : [-(sum(_361411, _361409, n0)), rdn_translate(_361411, rdn_pos(_361407)), rdn_translate(_361409, rdn_neg(_361407))], (970 ^ _332312) ^ [_361768, _361770, _361772, _361774, _361776] : [-(sum(_361776, _361774, _361772)), rdn_translate(_361776, rdn_neg(_361770)), rdn_translate(_361774, rdn_pos(_361768)), sum(_361774, _361776, _361772)], (984 ^ _332312) ^ [_362238, _362240, _362242, _362244] : [-(_362240 = _362238), sum(_362244, _362242, _362240), sum(_362244, _362242, _362238)], (994 ^ _332312) ^ [_362589, _362591, _362593, _362595] : [-(_362595 = _362593), sum(_362595, _362591, _362589), sum(_362593, _362591, _362589)], (1004 ^ _332312) ^ [_362940, _362942, _362944, _362946] : [-(_362944 = _362942), sum(_362946, _362944, _362940), sum(_362946, _362942, _362940)], (1014 ^ _332312) ^ [_363306, _363308, _363310] : [sum(_363308, _363306, _363310), -(difference(_363310, _363308, _363306))], (1020 ^ _332312) ^ [_363478, _363480, _363482] : [difference(_363482, _363480, _363478), -(sum(_363480, _363478, _363482))], (1026 ^ _332312) ^ [_363742, _363744, _363746, _363748, _363750] : [-(rdn_add_with_carry(rdnn(_363750), rdnn(_363748), rdnn(_363746), rdnn(_363744))), rdn_digit_add(rdnn(_363748), rdnn(_363746), rdnn(_363742), rdnn(n0)), rdn_digit_add(rdnn(_363742), rdnn(_363750), rdnn(_363744), rdnn(n0))], (1036 ^ _332312) ^ [_364193, _364195, _364197, _364199, _364201, _364203, _364205] : [-(rdn_add_with_carry(rdnn(_364205), rdnn(_364203), rdnn(_364201), rdn(rdnn(_364197), rdnn(n1)))), rdn_digit_add(rdnn(_364203), rdnn(_364201), rdnn(_364199), rdnn(_364195)), rdn_digit_add(rdnn(_364199), rdnn(_364205), rdnn(_364197), rdnn(_364193)), rdn_digit_add(rdnn(_364195), rdnn(_364193), rdnn(n1), rdnn(n0))], (1050 ^ _332312) ^ [_364841, _364843, _364845, _364847, _364849, _364851, _364853, _364855, _364857, _364859] : [-(rdn_add_with_carry(rdnn(_364859), rdnn(_364857), rdn(rdnn(_364855), _364853), rdn(rdnn(_364851), _364849))), rdn_digit_add(rdnn(_364857), rdnn(_364855), rdnn(_364847), rdnn(_364845)), rdn_digit_add(rdnn(_364847), rdnn(_364859), rdnn(_364851), rdnn(_364843)), rdn_digit_add(rdnn(_364845), rdnn(_364843), rdnn(_364841), rdnn(n0)), rdn_add_with_carry(rdnn(_364841), rdnn(n0), _364853, _364849), rdn_non_zero(_364853), rdn_non_zero(_364849)], (1112 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n0), rdnn(n0), rdnn(n0), rdnn(n0)))], (1114 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n0), rdnn(n1), rdnn(n1), rdnn(n0)))], (1116 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n0), rdnn(n2), rdnn(n2), rdnn(n0)))], (1118 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n0), rdnn(n3), rdnn(n3), rdnn(n0)))], (1120 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n0), rdnn(n4), rdnn(n4), rdnn(n0)))], (1122 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n0), rdnn(n5), rdnn(n5), rdnn(n0)))], (1124 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n0), rdnn(n6), rdnn(n6), rdnn(n0)))], (1126 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n0), rdnn(n7), rdnn(n7), rdnn(n0)))], (1128 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n0), rdnn(n8), rdnn(n8), rdnn(n0)))], (1130 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n0), rdnn(n9), rdnn(n9), rdnn(n0)))], (1132 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n1), rdnn(n0), rdnn(n1), rdnn(n0)))], (1134 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n1), rdnn(n1), rdnn(n2), rdnn(n0)))], (1136 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n1), rdnn(n2), rdnn(n3), rdnn(n0)))], (1138 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n1), rdnn(n3), rdnn(n4), rdnn(n0)))], (1140 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n1), rdnn(n4), rdnn(n5), rdnn(n0)))], (1142 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n1), rdnn(n5), rdnn(n6), rdnn(n0)))], (1144 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n1), rdnn(n6), rdnn(n7), rdnn(n0)))], (1146 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n1), rdnn(n7), rdnn(n8), rdnn(n0)))], (1148 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n1), rdnn(n8), rdnn(n9), rdnn(n0)))], (1150 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n1), rdnn(n9), rdnn(n0), rdnn(n1)))], (1152 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n2), rdnn(n0), rdnn(n2), rdnn(n0)))], (1154 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n2), rdnn(n1), rdnn(n3), rdnn(n0)))], (1156 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n2), rdnn(n2), rdnn(n4), rdnn(n0)))], (1158 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n2), rdnn(n3), rdnn(n5), rdnn(n0)))], (1160 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n2), rdnn(n4), rdnn(n6), rdnn(n0)))], (1162 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n2), rdnn(n5), rdnn(n7), rdnn(n0)))], (1164 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n2), rdnn(n6), rdnn(n8), rdnn(n0)))], (1166 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n2), rdnn(n7), rdnn(n9), rdnn(n0)))], (1168 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n2), rdnn(n8), rdnn(n0), rdnn(n1)))], (1170 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n2), rdnn(n9), rdnn(n1), rdnn(n1)))], (1172 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n3), rdnn(n0), rdnn(n3), rdnn(n0)))], (1174 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n3), rdnn(n1), rdnn(n4), rdnn(n0)))], (1176 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n3), rdnn(n2), rdnn(n5), rdnn(n0)))], (1178 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n3), rdnn(n3), rdnn(n6), rdnn(n0)))], (1180 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n3), rdnn(n4), rdnn(n7), rdnn(n0)))], (1182 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n3), rdnn(n5), rdnn(n8), rdnn(n0)))], (1184 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n3), rdnn(n6), rdnn(n9), rdnn(n0)))], (1186 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n3), rdnn(n7), rdnn(n0), rdnn(n1)))], (1188 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n3), rdnn(n8), rdnn(n1), rdnn(n1)))], (1190 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n3), rdnn(n9), rdnn(n2), rdnn(n1)))], (1192 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n4), rdnn(n0), rdnn(n4), rdnn(n0)))], (1194 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n4), rdnn(n1), rdnn(n5), rdnn(n0)))], (1196 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n4), rdnn(n2), rdnn(n6), rdnn(n0)))], (1198 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n4), rdnn(n3), rdnn(n7), rdnn(n0)))], (1200 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n4), rdnn(n4), rdnn(n8), rdnn(n0)))], (1202 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n4), rdnn(n5), rdnn(n9), rdnn(n0)))], (1204 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n4), rdnn(n6), rdnn(n0), rdnn(n1)))], (1206 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n4), rdnn(n7), rdnn(n1), rdnn(n1)))], (1208 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n4), rdnn(n8), rdnn(n2), rdnn(n1)))], (1210 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n4), rdnn(n9), rdnn(n3), rdnn(n1)))], (1212 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n5), rdnn(n0), rdnn(n5), rdnn(n0)))], (1214 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n5), rdnn(n1), rdnn(n6), rdnn(n0)))], (1216 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n5), rdnn(n2), rdnn(n7), rdnn(n0)))], (1218 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n5), rdnn(n3), rdnn(n8), rdnn(n0)))], (1220 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n5), rdnn(n4), rdnn(n9), rdnn(n0)))], (1222 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n5), rdnn(n5), rdnn(n0), rdnn(n1)))], (1224 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n5), rdnn(n6), rdnn(n1), rdnn(n1)))], (1226 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n5), rdnn(n7), rdnn(n2), rdnn(n1)))], (1228 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n5), rdnn(n8), rdnn(n3), rdnn(n1)))], (1230 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n5), rdnn(n9), rdnn(n4), rdnn(n1)))], (1232 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n6), rdnn(n0), rdnn(n6), rdnn(n0)))], (1234 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n6), rdnn(n1), rdnn(n7), rdnn(n0)))], (1236 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n6), rdnn(n2), rdnn(n8), rdnn(n0)))], (1238 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n6), rdnn(n3), rdnn(n9), rdnn(n0)))], (1240 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n6), rdnn(n4), rdnn(n0), rdnn(n1)))], (1242 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n6), rdnn(n5), rdnn(n1), rdnn(n1)))], (1244 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n6), rdnn(n6), rdnn(n2), rdnn(n1)))], (1246 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n6), rdnn(n7), rdnn(n3), rdnn(n1)))], (1248 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n6), rdnn(n8), rdnn(n4), rdnn(n1)))], (1250 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n6), rdnn(n9), rdnn(n5), rdnn(n1)))], (1252 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n7), rdnn(n0), rdnn(n7), rdnn(n0)))], (1254 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n7), rdnn(n1), rdnn(n8), rdnn(n0)))], (1256 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n7), rdnn(n2), rdnn(n9), rdnn(n0)))], (1258 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n7), rdnn(n3), rdnn(n0), rdnn(n1)))], (1260 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n7), rdnn(n4), rdnn(n1), rdnn(n1)))], (1262 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n7), rdnn(n5), rdnn(n2), rdnn(n1)))], (1264 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n7), rdnn(n6), rdnn(n3), rdnn(n1)))], (1266 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n7), rdnn(n7), rdnn(n4), rdnn(n1)))], (1268 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n7), rdnn(n8), rdnn(n5), rdnn(n1)))], (1270 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n7), rdnn(n9), rdnn(n6), rdnn(n1)))], (1272 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n8), rdnn(n0), rdnn(n8), rdnn(n0)))], (1274 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n8), rdnn(n1), rdnn(n9), rdnn(n0)))], (1276 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n8), rdnn(n2), rdnn(n0), rdnn(n1)))], (1278 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n8), rdnn(n3), rdnn(n1), rdnn(n1)))], (1280 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n8), rdnn(n4), rdnn(n2), rdnn(n1)))], (1282 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n8), rdnn(n5), rdnn(n3), rdnn(n1)))], (1284 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n8), rdnn(n6), rdnn(n4), rdnn(n1)))], (1286 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n8), rdnn(n7), rdnn(n5), rdnn(n1)))], (1288 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n8), rdnn(n8), rdnn(n6), rdnn(n1)))], (1290 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n8), rdnn(n9), rdnn(n7), rdnn(n1)))], (1292 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n9), rdnn(n0), rdnn(n9), rdnn(n0)))], (1294 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n9), rdnn(n1), rdnn(n0), rdnn(n1)))], (1296 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n9), rdnn(n2), rdnn(n1), rdnn(n1)))], (1298 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n9), rdnn(n3), rdnn(n2), rdnn(n1)))], (1300 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n9), rdnn(n4), rdnn(n3), rdnn(n1)))], (1302 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n9), rdnn(n5), rdnn(n4), rdnn(n1)))], (1304 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n9), rdnn(n6), rdnn(n5), rdnn(n1)))], (1306 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n9), rdnn(n7), rdnn(n6), rdnn(n1)))], (1308 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n9), rdnn(n8), rdnn(n7), rdnn(n1)))], (1310 ^ _332312) ^ [] : [-(rdn_digit_add(rdnn(n9), rdnn(n9), rdnn(n8), rdnn(n1)))], (1106 ^ _332312) ^ [_367088, _367090, _367092, _367094, _367096, _367098] : [rdn_add_with_carry(rdnn(_367098), rdnn(_367092), rdn(rdnn(_367096), _367094), rdn(rdnn(_367090), _367088)), -(rdn_add_with_carry(rdnn(_367098), rdn(rdnn(_367096), _367094), rdnn(_367092), rdn(rdnn(_367090), _367088)))], (1076 ^ _332312) ^ [_365922, _365924, _365926, _365928, _365930, _365932, _365934, _365936, _365938, _365940, _365942] : [-(rdn_add_with_carry(rdnn(_365942), rdn(rdnn(_365940), _365938), rdn(rdnn(_365936), _365934), rdn(rdnn(_365932), _365930))), rdn_digit_add(rdnn(_365940), rdnn(_365936), rdnn(_365928), rdnn(_365926)), rdn_digit_add(rdnn(_365928), rdnn(_365942), rdnn(_365932), rdnn(_365924)), rdn_digit_add(rdnn(_365926), rdnn(_365924), rdnn(_365922), rdnn(n0)), rdn_add_with_carry(rdnn(_365922), _365938, _365934, _365930), rdn_non_zero(_365938), rdn_non_zero(_365934), rdn_non_zero(_365930)]], input).
% 0.37/1.39 ncf('1',plain,[sum(n0, n0, n0)],start(1312 ^ 0,bind([[_373895], [n0]]))).
% 0.37/1.39 ncf('1.1',plain,[-(sum(n0, n0, n0)), rdn_translate(n0, rdn_pos(rdnn(n0))), rdn_translate(n0, rdn_pos(rdnn(n0))), rdn_add_with_carry(rdnn(n0), rdnn(n0), rdnn(n0), rdnn(n0)), rdn_translate(n0, rdn_pos(rdnn(n0)))],extension(880 ^ 1,bind([[_358747, _358749, _358751, _358753, _358755, _358757], [rdnn(n0), rdnn(n0), rdnn(n0), n0, n0, n0]]))).
% 0.37/1.39 ncf('1.1.1',plain,[-(rdn_translate(n0, rdn_pos(rdnn(n0))))],extension(204 ^ 2)).
% 0.37/1.39 ncf('1.1.2',plain,[-(rdn_translate(n0, rdn_pos(rdnn(n0))))],extension(204 ^ 2)).
% 0.37/1.39 ncf('1.1.3',plain,[-(rdn_add_with_carry(rdnn(n0), rdnn(n0), rdnn(n0), rdnn(n0))), rdn_digit_add(rdnn(n0), rdnn(n0), rdnn(n0), rdnn(n0)), rdn_digit_add(rdnn(n0), rdnn(n0), rdnn(n0), rdnn(n0))],extension(1026 ^ 2,bind([[_363742, _363744, _363746, _363748, _363750], [n0, n0, n0, n0, n0]]))).
% 0.37/1.39 ncf('1.1.3.1',plain,[-(rdn_digit_add(rdnn(n0), rdnn(n0), rdnn(n0), rdnn(n0)))],extension(1112 ^ 3)).
% 0.37/1.39 ncf('1.1.3.2',plain,[-(rdn_digit_add(rdnn(n0), rdnn(n0), rdnn(n0), rdnn(n0)))],extension(1112 ^ 3)).
% 0.37/1.39 ncf('1.1.4',plain,[-(rdn_translate(n0, rdn_pos(rdnn(n0))))],lemmata('[1].x')).
% 0.37/1.39 %-----------------------------------------------------
% 0.37/1.39 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------