%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM310+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n014.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:22 EDT 2023
% Result : Theorem 246.34s 238.41s
% Output : Proof 246.34s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : NUM310+1 : TPTP v8.1.2. Released v3.1.0.
% 0.07/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n014.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:58:57 EDT 2023
% 0.12/0.33 % CPUTime :
% 246.34/238.41
% 246.34/238.41 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 246.34/238.41 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 246.34/238.41 %-----------------------------------------------------
% 246.34/238.41 ncf(matrix, plain, [(942 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n1), rdnn(n6), rdnn(n7), rdnn(n0)))], (1066 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n7), rdnn(n8), rdnn(n5), rdnn(n1)))], (312 ^ _348170) ^ [] : [-(rdn_translate(nn28, rdn_neg(rdn(rdnn(n8), rdnn(n2)))))], (1056 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n7), rdnn(n3), rdnn(n0), rdnn(n1)))], (132 ^ _348170) ^ [] : [-(rdn_translate(n65, rdn_pos(rdn(rdnn(n5), rdnn(n6)))))], (824 ^ _348170) ^ [_372770, _372772, _372774, _372776, _372778] : [-(rdn_add_with_carry(rdnn(_372778), rdnn(_372776), rdnn(_372774), rdnn(_372772))), rdn_digit_add(rdnn(_372776), rdnn(_372774), rdnn(_372770), rdnn(n0)), rdn_digit_add(rdnn(_372770), rdnn(_372778), rdnn(_372772), rdnn(n0))], (990 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n4), rdnn(n0), rdnn(n4), rdnn(n0)))], (246 ^ _348170) ^ [] : [-(rdn_translate(n122, rdn_pos(rdn(rdnn(n2), rdn(rdnn(n2), rdnn(n1))))))], (386 ^ _348170) ^ [] : [-(rdn_translate(nn65, rdn_neg(rdn(rdnn(n5), rdnn(n6)))))], (530 ^ _348170) ^ [] : [-(rdn_non_zero_digit(rdnn(n9)))], (432 ^ _348170) ^ [] : [-(rdn_translate(nn88, rdn_neg(rdn(rdnn(n8), rdnn(n8)))))], (970 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n3), rdnn(n0), rdnn(n3), rdnn(n0)))], (526 ^ _348170) ^ [] : [-(rdn_non_zero_digit(rdnn(n7)))], (354 ^ _348170) ^ [] : [-(rdn_translate(nn49, rdn_neg(rdn(rdnn(n9), rdnn(n4)))))], (1042 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n6), rdnn(n6), rdnn(n2), rdnn(n1)))], (544 ^ _348170) ^ [] : [-(rdn_positive_less(rdnn(n6), rdnn(n7)))], (404 ^ _348170) ^ [] : [-(rdn_translate(nn74, rdn_neg(rdn(rdnn(n4), rdnn(n7)))))], (524 ^ _348170) ^ [] : [-(rdn_non_zero_digit(rdnn(n6)))], (70 ^ _348170) ^ [] : [-(rdn_translate(n34, rdn_pos(rdn(rdnn(n4), rdnn(n3)))))], (374 ^ _348170) ^ [] : [-(rdn_translate(nn59, rdn_neg(rdn(rdnn(n9), rdnn(n5)))))], (82 ^ _348170) ^ [] : [-(rdn_translate(n40, rdn_pos(rdn(rdnn(n0), rdnn(n4)))))], (358 ^ _348170) ^ [] : [-(rdn_translate(nn51, rdn_neg(rdn(rdnn(n1), rdnn(n5)))))], (376 ^ _348170) ^ [] : [-(rdn_translate(nn60, rdn_neg(rdn(rdnn(n0), rdnn(n6)))))], (500 ^ _348170) ^ [] : [-(rdn_translate(nn122, rdn_neg(rdn(rdnn(n2), rdn(rdnn(n2), rdnn(n1))))))], (260 ^ _348170) ^ [] : [-(rdn_translate(nn2, rdn_neg(rdnn(n2))))], (244 ^ _348170) ^ [] : [-(rdn_translate(n121, rdn_pos(rdn(rdnn(n1), rdn(rdnn(n2), rdnn(n1))))))], (334 ^ _348170) ^ [] : [-(rdn_translate(nn39, rdn_neg(rdn(rdnn(n9), rdnn(n3)))))], (1024 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n5), rdnn(n7), rdnn(n2), rdnn(n1)))], (478 ^ _348170) ^ [] : [-(rdn_translate(nn111, rdn_neg(rdn(rdnn(n1), rdn(rdnn(n1), rdnn(n1))))))], (34 ^ _348170) ^ [] : [-(rdn_translate(n16, rdn_pos(rdn(rdnn(n6), rdnn(n1)))))], (466 ^ _348170) ^ [] : [-(rdn_translate(nn105, rdn_neg(rdn(rdnn(n5), rdn(rdnn(n0), rdnn(n1))))))], (6 ^ _348170) ^ [] : [-(rdn_translate(n2, rdn_pos(rdnn(n2))))], (920 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n0), rdnn(n5), rdnn(n5), rdnn(n0)))], (224 ^ _348170) ^ [] : [-(rdn_translate(n111, rdn_pos(rdn(rdnn(n1), rdn(rdnn(n1), rdnn(n1))))))], (782 ^ _348170) ^ [_371266, _371268, _371270, _371272] : [-(_371268 = _371266), sum(_371272, _371270, _371268), sum(_371272, _371270, _371266)], (818 ^ _348170) ^ [_372506, _372508, _372510] : [difference(_372510, _372508, _372506), -(sum(_372508, _372506, _372510))], (1088 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n8), rdnn(n9), rdnn(n7), rdnn(n1)))], (184 ^ _348170) ^ [] : [-(rdn_translate(n91, rdn_pos(rdn(rdnn(n1), rdnn(n9)))))], (470 ^ _348170) ^ [] : [-(rdn_translate(nn107, rdn_neg(rdn(rdnn(n7), rdn(rdnn(n0), rdnn(n1))))))], (136 ^ _348170) ^ [] : [-(rdn_translate(n67, rdn_pos(rdn(rdnn(n7), rdnn(n6)))))], (974 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n3), rdnn(n2), rdnn(n5), rdnn(n0)))], (204 ^ _348170) ^ [] : [-(rdn_translate(n101, rdn_pos(rdn(rdnn(n1), rdn(rdnn(n0), rdnn(n1))))))], (910 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n0), rdnn(n0), rdnn(n0), rdnn(n0)))], (216 ^ _348170) ^ [] : [-(rdn_translate(n107, rdn_pos(rdn(rdnn(n7), rdn(rdnn(n0), rdnn(n1))))))], (964 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n2), rdnn(n7), rdnn(n9), rdnn(n0)))], (1052 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n7), rdnn(n1), rdnn(n8), rdnn(n0)))], (116 ^ _348170) ^ [] : [-(rdn_translate(n57, rdn_pos(rdn(rdnn(n7), rdnn(n5)))))], (1086 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n8), rdnn(n8), rdnn(n6), rdnn(n1)))], (294 ^ _348170) ^ [] : [-(rdn_translate(nn19, rdn_neg(rdn(rdnn(n9), rdnn(n1)))))], (220 ^ _348170) ^ [] : [-(rdn_translate(n109, rdn_pos(rdn(rdnn(n9), rdn(rdnn(n0), rdnn(n1))))))], (472 ^ _348170) ^ [] : [-(rdn_translate(nn108, rdn_neg(rdn(rdnn(n8), rdn(rdnn(n0), rdnn(n1))))))], (22 ^ _348170) ^ [] : [-(rdn_translate(n10, rdn_pos(rdn(rdnn(n0), rdnn(n1)))))], (282 ^ _348170) ^ [] : [-(rdn_translate(nn13, rdn_neg(rdn(rdnn(n3), rdnn(n1)))))], (58 ^ _348170) ^ [] : [-(rdn_translate(n28, rdn_pos(rdn(rdnn(n8), rdnn(n2)))))], (134 ^ _348170) ^ [] : [-(rdn_translate(n66, rdn_pos(rdn(rdnn(n6), rdnn(n6)))))], (28 ^ _348170) ^ [] : [-(rdn_translate(n13, rdn_pos(rdn(rdnn(n3), rdnn(n1)))))], (36 ^ _348170) ^ [] : [-(rdn_translate(n17, rdn_pos(rdn(rdnn(n7), rdnn(n1)))))], (276 ^ _348170) ^ [] : [-(rdn_translate(nn10, rdn_neg(rdn(rdnn(n0), rdnn(n1)))))], (218 ^ _348170) ^ [] : [-(rdn_translate(n108, rdn_pos(rdn(rdnn(n8), rdn(rdnn(n0), rdnn(n1))))))], (1008 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n4), rdnn(n9), rdnn(n3), rdnn(n1)))], (454 ^ _348170) ^ [] : [-(rdn_translate(nn99, rdn_neg(rdn(rdnn(n9), rdnn(n9)))))], (1006 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n4), rdnn(n8), rdnn(n2), rdnn(n1)))], (932 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n1), rdnn(n1), rdnn(n2), rdnn(n0)))], (320 ^ _348170) ^ [] : [-(rdn_translate(nn32, rdn_neg(rdn(rdnn(n2), rdnn(n3)))))], (424 ^ _348170) ^ [] : [-(rdn_translate(nn84, rdn_neg(rdn(rdnn(n4), rdnn(n8)))))], (426 ^ _348170) ^ [] : [-(rdn_translate(nn85, rdn_neg(rdn(rdnn(n5), rdnn(n8)))))], (678 ^ _348170) ^ [_367775, _367777, _367779, _367781, _367783, _367785] : [-(sum(_367785, _367783, _367781)), rdn_translate(_367785, rdn_pos(_367779)), rdn_translate(_367783, rdn_pos(_367777)), rdn_add_with_carry(rdnn(n0), _367779, _367777, _367775), rdn_translate(_367781, rdn_pos(_367775))], (916 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n0), rdnn(n3), rdnn(n3), rdnn(n0)))], (496 ^ _348170) ^ [] : [-(rdn_translate(nn120, rdn_neg(rdn(rdnn(n0), rdn(rdnn(n2), rdnn(n1))))))], (104 ^ _348170) ^ [] : [-(rdn_translate(n51, rdn_pos(rdn(rdnn(n1), rdnn(n5)))))], (560 ^ _348170) ^ [_363710, _363712, _363714, _363716] : [rdn_positive_less(_363714, _363710), -(rdn_positive_less(rdn(rdnn(_363716), _363714), rdn(rdnn(_363712), _363710)))], (988 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n3), rdnn(n9), rdnn(n2), rdnn(n1)))], (114 ^ _348170) ^ [] : [-(rdn_translate(n56, rdn_pos(rdn(rdnn(n6), rdnn(n5)))))], (1084 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n8), rdnn(n7), rdnn(n5), rdnn(n1)))], (166 ^ _348170) ^ [] : [-(rdn_translate(n82, rdn_pos(rdn(rdnn(n2), rdnn(n8)))))], (278 ^ _348170) ^ [] : [-(rdn_translate(nn11, rdn_neg(rdn(rdnn(n1), rdnn(n1)))))], (38 ^ _348170) ^ [] : [-(rdn_translate(n18, rdn_pos(rdn(rdnn(n8), rdnn(n1)))))], (1020 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n5), rdnn(n5), rdnn(n0), rdnn(n1)))], (588 ^ _348170) ^ [_364737, _364739] : [rdn_non_zero(_364737), -(rdn_non_zero(rdn(rdnn(_364739), _364737)))], (94 ^ _348170) ^ [] : [-(rdn_translate(n46, rdn_pos(rdn(rdnn(n6), rdnn(n4)))))], (402 ^ _348170) ^ [] : [-(rdn_translate(nn73, rdn_neg(rdn(rdnn(n3), rdnn(n7)))))], (1050 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n7), rdnn(n0), rdnn(n7), rdnn(n0)))], (128 ^ _348170) ^ [] : [-(rdn_translate(n63, rdn_pos(rdn(rdnn(n3), rdnn(n6)))))], (222 ^ _348170) ^ [] : [-(rdn_translate(n110, rdn_pos(rdn(rdnn(n0), rdn(rdnn(n1), rdnn(n1))))))], (300 ^ _348170) ^ [] : [-(rdn_translate(nn22, rdn_neg(rdn(rdnn(n2), rdnn(n2)))))], (86 ^ _348170) ^ [] : [-(rdn_translate(n42, rdn_pos(rdn(rdnn(n2), rdnn(n4)))))], (1000 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n4), rdnn(n5), rdnn(n9), rdnn(n0)))], (296 ^ _348170) ^ [] : [-(rdn_translate(nn20, rdn_neg(rdn(rdnn(n0), rdnn(n2)))))], (1046 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n6), rdnn(n8), rdnn(n4), rdnn(n1)))], (178 ^ _348170) ^ [] : [-(rdn_translate(n88, rdn_pos(rdn(rdnn(n8), rdnn(n8)))))], (962 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n2), rdnn(n6), rdnn(n8), rdnn(n0)))], (952 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n2), rdnn(n1), rdnn(n3), rdnn(n0)))], (12 ^ _348170) ^ [] : [-(rdn_translate(n5, rdn_pos(rdnn(n5))))], (834 ^ _348170) ^ [_373221, _373223, _373225, _373227, _373229, _373231, _373233] : [-(rdn_add_with_carry(rdnn(_373233), rdnn(_373231), rdnn(_373229), rdn(rdnn(_373225), rdnn(n1)))), rdn_digit_add(rdnn(_373231), rdnn(_373229), rdnn(_373227), rdnn(_373223)), rdn_digit_add(rdnn(_373227), rdnn(_373233), rdnn(_373225), rdnn(_373221)), rdn_digit_add(rdnn(_373223), rdnn(_373221), rdnn(n1), rdnn(n0))], (714 ^ _348170) ^ [_369021, _369023, _369025, _369027, _369029, _369031] : [-(sum(_369031, _369029, _369027)), rdn_translate(_369031, rdn_pos(_369025)), rdn_translate(_369029, rdn_neg(_369023)), rdn_positive_less(_369025, _369023), rdn_add_with_carry(rdnn(n0), _369025, _369021, _369023), rdn_translate(_369027, rdn_neg(_369021))], (98 ^ _348170) ^ [] : [-(rdn_translate(n48, rdn_pos(rdn(rdnn(n8), rdnn(n4)))))], (956 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n2), rdnn(n3), rdnn(n5), rdnn(n0)))], (176 ^ _348170) ^ [] : [-(rdn_translate(n87, rdn_pos(rdn(rdnn(n7), rdnn(n8)))))], (474 ^ _348170) ^ [] : [-(rdn_translate(nn109, rdn_neg(rdn(rdnn(n9), rdn(rdnn(n0), rdnn(n1))))))], (330 ^ _348170) ^ [] : [-(rdn_translate(nn37, rdn_neg(rdn(rdnn(n7), rdnn(n3)))))], (382 ^ _348170) ^ [] : [-(rdn_translate(nn63, rdn_neg(rdn(rdnn(n3), rdnn(n6)))))], (158 ^ _348170) ^ [] : [-(rdn_translate(n78, rdn_pos(rdn(rdnn(n8), rdnn(n7)))))], (230 ^ _348170) ^ [] : [-(rdn_translate(n114, rdn_pos(rdn(rdnn(n4), rdn(rdnn(n1), rdnn(n1))))))], (364 ^ _348170) ^ [] : [-(rdn_translate(nn54, rdn_neg(rdn(rdnn(n4), rdnn(n5)))))], (408 ^ _348170) ^ [] : [-(rdn_translate(nn76, rdn_neg(rdn(rdnn(n6), rdnn(n7)))))], (186 ^ _348170) ^ [] : [-(rdn_translate(n92, rdn_pos(rdn(rdnn(n2), rdnn(n9)))))], (992 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n4), rdnn(n1), rdnn(n5), rdnn(n0)))], (306 ^ _348170) ^ [] : [-(rdn_translate(nn25, rdn_neg(rdn(rdnn(n5), rdnn(n2)))))], (458 ^ _348170) ^ [] : [-(rdn_translate(nn101, rdn_neg(rdn(rdnn(n1), rdn(rdnn(n0), rdnn(n1))))))], (998 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n4), rdnn(n4), rdnn(n8), rdnn(n0)))], (292 ^ _348170) ^ [] : [-(rdn_translate(nn18, rdn_neg(rdn(rdnn(n8), rdnn(n1)))))], (1096 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n9), rdnn(n3), rdnn(n2), rdnn(n1)))], (236 ^ _348170) ^ [] : [-(rdn_translate(n117, rdn_pos(rdn(rdnn(n7), rdn(rdnn(n1), rdnn(n1))))))], (384 ^ _348170) ^ [] : [-(rdn_translate(nn64, rdn_neg(rdn(rdnn(n4), rdnn(n6)))))], (48 ^ _348170) ^ [] : [-(rdn_translate(n23, rdn_pos(rdn(rdnn(n3), rdnn(n2)))))], (266 ^ _348170) ^ [] : [-(rdn_translate(nn5, rdn_neg(rdnn(n5))))], (92 ^ _348170) ^ [] : [-(rdn_translate(n45, rdn_pos(rdn(rdnn(n5), rdnn(n4)))))], (1102 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n9), rdnn(n6), rdnn(n5), rdnn(n1)))], (168 ^ _348170) ^ [] : [-(rdn_translate(n83, rdn_pos(rdn(rdnn(n3), rdnn(n8)))))], (340 ^ _348170) ^ [] : [-(rdn_translate(nn42, rdn_neg(rdn(rdnn(n2), rdnn(n4)))))], (154 ^ _348170) ^ [] : [-(rdn_translate(n76, rdn_pos(rdn(rdnn(n6), rdnn(n7)))))], (190 ^ _348170) ^ [] : [-(rdn_translate(n94, rdn_pos(rdn(rdnn(n4), rdnn(n9)))))], (254 ^ _348170) ^ [] : [-(rdn_translate(n126, rdn_pos(rdn(rdnn(n6), rdn(rdnn(n2), rdnn(n1))))))], (206 ^ _348170) ^ [] : [-(rdn_translate(n102, rdn_pos(rdn(rdnn(n2), rdn(rdnn(n0), rdnn(n1))))))], (2 ^ _348170) ^ [] : [-(rdn_translate(n0, rdn_pos(rdnn(n0))))], (1070 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n8), rdnn(n0), rdnn(n8), rdnn(n0)))], (1110 ^ _348170) ^ [] : [-(sum(n2, n3, n6))], (428 ^ _348170) ^ [] : [-(rdn_translate(nn86, rdn_neg(rdn(rdnn(n6), rdnn(n8)))))], (406 ^ _348170) ^ [] : [-(rdn_translate(nn75, rdn_neg(rdn(rdnn(n5), rdnn(n7)))))], (170 ^ _348170) ^ [] : [-(rdn_translate(n84, rdn_pos(rdn(rdnn(n4), rdnn(n8)))))], (180 ^ _348170) ^ [] : [-(rdn_translate(n89, rdn_pos(rdn(rdnn(n9), rdnn(n8)))))], (162 ^ _348170) ^ [] : [-(rdn_translate(n80, rdn_pos(rdn(rdnn(n0), rdnn(n8)))))], (914 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n0), rdnn(n2), rdnn(n2), rdnn(n0)))], (290 ^ _348170) ^ [] : [-(rdn_translate(nn17, rdn_neg(rdn(rdnn(n7), rdnn(n1)))))], (96 ^ _348170) ^ [] : [-(rdn_translate(n47, rdn_pos(rdn(rdnn(n7), rdnn(n4)))))], (328 ^ _348170) ^ [] : [-(rdn_translate(nn36, rdn_neg(rdn(rdnn(n6), rdnn(n3)))))], (594 ^ _348170) ^ [_364981, _364983, _364985, _364987] : [-(less(_364987, _364985)), rdn_translate(_364987, rdn_pos(_364983)), rdn_translate(_364985, rdn_pos(_364981)), rdn_positive_less(_364983, _364981)], (410 ^ _348170) ^ [] : [-(rdn_translate(nn77, rdn_neg(rdn(rdnn(n7), rdnn(n7)))))], (486 ^ _348170) ^ [] : [-(rdn_translate(nn115, rdn_neg(rdn(rdnn(n5), rdn(rdnn(n1), rdnn(n1))))))], (1104 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n9), rdnn(n7), rdnn(n6), rdnn(n1)))], (16 ^ _348170) ^ [] : [-(rdn_translate(n7, rdn_pos(rdnn(n7))))], (194 ^ _348170) ^ [] : [-(rdn_translate(n96, rdn_pos(rdn(rdnn(n6), rdnn(n9)))))], (1002 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n4), rdnn(n6), rdnn(n0), rdnn(n1)))], (456 ^ _348170) ^ [] : [-(rdn_translate(nn100, rdn_neg(rdn(rdnn(n0), rdn(rdnn(n0), rdnn(n1))))))], (42 ^ _348170) ^ [] : [-(rdn_translate(n20, rdn_pos(rdn(rdnn(n0), rdnn(n2)))))], (848 ^ _348170) ^ [_373869, _373871, _373873, _373875, _373877, _373879, _373881, _373883, _373885, _373887] : [-(rdn_add_with_carry(rdnn(_373887), rdnn(_373885), rdn(rdnn(_373883), _373881), rdn(rdnn(_373879), _373877))), rdn_digit_add(rdnn(_373885), rdnn(_373883), rdnn(_373875), rdnn(_373873)), rdn_digit_add(rdnn(_373875), rdnn(_373887), rdnn(_373879), rdnn(_373871)), rdn_digit_add(rdnn(_373873), rdnn(_373871), rdnn(_373869), rdnn(n0)), rdn_add_with_carry(rdnn(_373869), rdnn(n0), _373881, _373877), rdn_non_zero(_373881), rdn_non_zero(_373877)], (1022 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n5), rdnn(n6), rdnn(n1), rdnn(n1)))], (812 ^ _348170) ^ [_372334, _372336, _372338] : [sum(_372336, _372334, _372338), -(difference(_372338, _372336, _372334))], (696 ^ _348170) ^ [_368398, _368400, _368402, _368404, _368406, _368408] : [-(sum(_368408, _368406, _368404)), rdn_translate(_368408, rdn_neg(_368402)), rdn_translate(_368406, rdn_neg(_368400)), rdn_add_with_carry(rdnn(n0), _368402, _368400, _368398), rdn_translate(_368404, rdn_neg(_368398))], (972 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n3), rdnn(n1), rdnn(n4), rdnn(n0)))], (88 ^ _348170) ^ [] : [-(rdn_translate(n43, rdn_pos(rdn(rdnn(n3), rdnn(n4)))))], (80 ^ _348170) ^ [] : [-(rdn_translate(n39, rdn_pos(rdn(rdnn(n9), rdnn(n3)))))], (258 ^ _348170) ^ [] : [-(rdn_translate(nn1, rdn_neg(rdnn(n1))))], (976 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n3), rdnn(n3), rdnn(n6), rdnn(n0)))], (74 ^ _348170) ^ [] : [-(rdn_translate(n36, rdn_pos(rdn(rdnn(n6), rdnn(n3)))))], (286 ^ _348170) ^ [] : [-(rdn_translate(nn15, rdn_neg(rdn(rdnn(n5), rdnn(n1)))))], (174 ^ _348170) ^ [] : [-(rdn_translate(n86, rdn_pos(rdn(rdnn(n6), rdnn(n8)))))], (986 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n3), rdnn(n8), rdnn(n1), rdnn(n1)))], (510 ^ _348170) ^ [] : [-(rdn_translate(nn127, rdn_neg(rdn(rdnn(n7), rdn(rdnn(n2), rdnn(n1))))))], (1016 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n5), rdnn(n3), rdnn(n8), rdnn(n0)))], (1044 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n6), rdnn(n7), rdnn(n3), rdnn(n1)))], (324 ^ _348170) ^ [] : [-(rdn_translate(nn34, rdn_neg(rdn(rdnn(n4), rdnn(n3)))))], (444 ^ _348170) ^ [] : [-(rdn_translate(nn94, rdn_neg(rdn(rdnn(n4), rdnn(n9)))))], (758 ^ _348170) ^ [_370435, _370437, _370439] : [-(sum(_370439, _370437, n0)), rdn_translate(_370439, rdn_pos(_370435)), rdn_translate(_370437, rdn_neg(_370435))], (32 ^ _348170) ^ [] : [-(rdn_translate(n15, rdn_pos(rdn(rdnn(n5), rdnn(n1)))))], (520 ^ _348170) ^ [] : [-(rdn_non_zero_digit(rdnn(n4)))], (240 ^ _348170) ^ [] : [-(rdn_translate(n119, rdn_pos(rdn(rdnn(n9), rdn(rdnn(n1), rdnn(n1))))))], (950 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n2), rdnn(n0), rdnn(n2), rdnn(n0)))], (122 ^ _348170) ^ [] : [-(rdn_translate(n60, rdn_pos(rdn(rdnn(n0), rdnn(n6)))))], (550 ^ _348170) ^ [_363349, _363351, _363353] : [-(rdn_positive_less(rdnn(_363353), rdnn(_363349))), rdn_positive_less(rdnn(_363353), rdnn(_363351)), rdn_positive_less(rdnn(_363351), rdnn(_363349))], (984 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n3), rdnn(n7), rdnn(n0), rdnn(n1)))], (378 ^ _348170) ^ [] : [-(rdn_translate(nn61, rdn_neg(rdn(rdnn(n1), rdnn(n6)))))], (338 ^ _348170) ^ [] : [-(rdn_translate(nn41, rdn_neg(rdn(rdnn(n1), rdnn(n4)))))], (960 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n2), rdnn(n5), rdnn(n7), rdnn(n0)))], (940 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n1), rdnn(n5), rdnn(n6), rdnn(n0)))], (20 ^ _348170) ^ [] : [-(rdn_translate(n9, rdn_pos(rdnn(n9))))], (90 ^ _348170) ^ [] : [-(rdn_translate(n44, rdn_pos(rdn(rdnn(n4), rdnn(n4)))))], (944 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n1), rdnn(n7), rdnn(n8), rdnn(n0)))], (1068 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n7), rdnn(n9), rdnn(n6), rdnn(n1)))], (160 ^ _348170) ^ [] : [-(rdn_translate(n79, rdn_pos(rdn(rdnn(n9), rdnn(n7)))))], (912 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n0), rdnn(n1), rdnn(n1), rdnn(n0)))], (66 ^ _348170) ^ [] : [-(rdn_translate(n32, rdn_pos(rdn(rdnn(n2), rdnn(n3)))))], (46 ^ _348170) ^ [] : [-(rdn_translate(n22, rdn_pos(rdn(rdnn(n2), rdnn(n2)))))], (288 ^ _348170) ^ [] : [-(rdn_translate(nn16, rdn_neg(rdn(rdnn(n6), rdnn(n1)))))], (264 ^ _348170) ^ [] : [-(rdn_translate(nn4, rdn_neg(rdnn(n4))))], (274 ^ _348170) ^ [] : [-(rdn_translate(nn9, rdn_neg(rdnn(n9))))], (1060 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n7), rdnn(n5), rdnn(n2), rdnn(n1)))], (1074 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n8), rdnn(n2), rdnn(n0), rdnn(n1)))], (172 ^ _348170) ^ [] : [-(rdn_translate(n85, rdn_pos(rdn(rdnn(n5), rdnn(n8)))))], (438 ^ _348170) ^ [] : [-(rdn_translate(nn91, rdn_neg(rdn(rdnn(n1), rdnn(n9)))))], (100 ^ _348170) ^ [] : [-(rdn_translate(n49, rdn_pos(rdn(rdnn(n9), rdnn(n4)))))], (1092 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n9), rdnn(n1), rdnn(n0), rdnn(n1)))], (156 ^ _348170) ^ [] : [-(rdn_translate(n77, rdn_pos(rdn(rdnn(n7), rdnn(n7)))))], (926 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n0), rdnn(n8), rdnn(n8), rdnn(n0)))], (436 ^ _348170) ^ [] : [-(rdn_translate(nn90, rdn_neg(rdn(rdnn(n0), rdnn(n9)))))], (146 ^ _348170) ^ [] : [-(rdn_translate(n72, rdn_pos(rdn(rdnn(n2), rdnn(n7)))))], (84 ^ _348170) ^ [] : [-(rdn_translate(n41, rdn_pos(rdn(rdnn(n1), rdnn(n4)))))], (668 ^ _348170) ^ [_367348, _367350, _367352] : [-(less_or_equal(_367348, _367352)), sum(_367352, n1, _367350), less(_367348, _367350)], (946 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n1), rdnn(n8), rdnn(n9), rdnn(n0)))], (938 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n1), rdnn(n4), rdnn(n5), rdnn(n0)))], (24 ^ _348170) ^ [] : [-(rdn_translate(n11, rdn_pos(rdn(rdnn(n1), rdnn(n1)))))], (538 ^ _348170) ^ [] : [-(rdn_positive_less(rdnn(n3), rdnn(n4)))], (650 ^ _348170) ^ [_366816, _366818] : [less_or_equal(_366818, _366816), -(less(_366818, _366816)), -(_366818 = _366816)], (148 ^ _348170) ^ [] : [-(rdn_translate(n73, rdn_pos(rdn(rdnn(n3), rdnn(n7)))))], (298 ^ _348170) ^ [] : [-(rdn_translate(nn21, rdn_neg(rdn(rdnn(n1), rdnn(n2)))))], (518 ^ _348170) ^ [] : [-(rdn_non_zero_digit(rdnn(n3)))], (302 ^ _348170) ^ [] : [-(rdn_translate(nn23, rdn_neg(rdn(rdnn(n3), rdnn(n2)))))], (346 ^ _348170) ^ [] : [-(rdn_translate(nn45, rdn_neg(rdn(rdnn(n5), rdnn(n4)))))], (1100 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n9), rdnn(n5), rdnn(n4), rdnn(n1)))], (528 ^ _348170) ^ [] : [-(rdn_non_zero_digit(rdnn(n8)))], (108 ^ _348170) ^ [] : [-(rdn_translate(n53, rdn_pos(rdn(rdnn(n3), rdnn(n5)))))], (968 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n2), rdnn(n9), rdnn(n1), rdnn(n1)))], (308 ^ _348170) ^ [] : [-(rdn_translate(nn26, rdn_neg(rdn(rdnn(n6), rdnn(n2)))))], (388 ^ _348170) ^ [] : [-(rdn_translate(nn66, rdn_neg(rdn(rdnn(n6), rdnn(n6)))))], (352 ^ _348170) ^ [] : [-(rdn_translate(nn48, rdn_neg(rdn(rdnn(n8), rdnn(n4)))))], (922 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n0), rdnn(n6), rdnn(n6), rdnn(n0)))], (68 ^ _348170) ^ [] : [-(rdn_translate(n33, rdn_pos(rdn(rdnn(n3), rdnn(n3)))))], (360 ^ _348170) ^ [] : [-(rdn_translate(nn52, rdn_neg(rdn(rdnn(n2), rdnn(n5)))))], (232 ^ _348170) ^ [] : [-(rdn_translate(n115, rdn_pos(rdn(rdnn(n5), rdn(rdnn(n1), rdnn(n1))))))], (4 ^ _348170) ^ [] : [-(rdn_translate(n1, rdn_pos(rdnn(n1))))], (210 ^ _348170) ^ [] : [-(rdn_translate(n104, rdn_pos(rdn(rdnn(n4), rdn(rdnn(n0), rdnn(n1))))))], (434 ^ _348170) ^ [] : [-(rdn_translate(nn89, rdn_neg(rdn(rdnn(n9), rdnn(n8)))))], (582 ^ _348170) ^ [_364529] : [rdn_non_zero_digit(rdnn(_364529)), -(rdn_non_zero(rdnn(_364529)))], (226 ^ _348170) ^ [] : [-(rdn_translate(n112, rdn_pos(rdn(rdnn(n2), rdn(rdnn(n1), rdnn(n1))))))], (50 ^ _348170) ^ [] : [-(rdn_translate(n24, rdn_pos(rdn(rdnn(n4), rdnn(n2)))))], (546 ^ _348170) ^ [] : [-(rdn_positive_less(rdnn(n7), rdnn(n8)))], (548 ^ _348170) ^ [] : [-(rdn_positive_less(rdnn(n8), rdnn(n9)))], (468 ^ _348170) ^ [] : [-(rdn_translate(nn106, rdn_neg(rdn(rdnn(n6), rdn(rdnn(n0), rdnn(n1))))))], (10 ^ _348170) ^ [] : [-(rdn_translate(n4, rdn_pos(rdnn(n4))))], (332 ^ _348170) ^ [] : [-(rdn_translate(nn38, rdn_neg(rdn(rdnn(n8), rdnn(n3)))))], (208 ^ _348170) ^ [] : [-(rdn_translate(n103, rdn_pos(rdn(rdnn(n3), rdn(rdnn(n0), rdnn(n1))))))], (448 ^ _348170) ^ [] : [-(rdn_translate(nn96, rdn_neg(rdn(rdnn(n6), rdnn(n9)))))], (18 ^ _348170) ^ [] : [-(rdn_translate(n8, rdn_pos(rdnn(n8))))], (978 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n3), rdnn(n4), rdnn(n7), rdnn(n0)))], (476 ^ _348170) ^ [] : [-(rdn_translate(nn110, rdn_neg(rdn(rdnn(n0), rdn(rdnn(n1), rdnn(n1))))))], (234 ^ _348170) ^ [] : [-(rdn_translate(n116, rdn_pos(rdn(rdnn(n6), rdn(rdnn(n1), rdnn(n1))))))], (488 ^ _348170) ^ [] : [-(rdn_translate(nn116, rdn_neg(rdn(rdnn(n6), rdn(rdnn(n1), rdnn(n1))))))], (484 ^ _348170) ^ [] : [-(rdn_translate(nn114, rdn_neg(rdn(rdnn(n4), rdn(rdnn(n1), rdnn(n1))))))], (936 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n1), rdnn(n3), rdnn(n4), rdnn(n0)))], (494 ^ _348170) ^ [] : [-(rdn_translate(nn119, rdn_neg(rdn(rdnn(n9), rdn(rdnn(n1), rdnn(n1))))))], (60 ^ _348170) ^ [] : [-(rdn_translate(n29, rdn_pos(rdn(rdnn(n9), rdnn(n2)))))], (316 ^ _348170) ^ [] : [-(rdn_translate(nn30, rdn_neg(rdn(rdnn(n0), rdnn(n3)))))], (1058 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n7), rdnn(n4), rdnn(n1), rdnn(n1)))], (130 ^ _348170) ^ [] : [-(rdn_translate(n64, rdn_pos(rdn(rdnn(n4), rdnn(n6)))))], (954 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n2), rdnn(n2), rdnn(n4), rdnn(n0)))], (1026 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n5), rdnn(n8), rdnn(n3), rdnn(n1)))], (152 ^ _348170) ^ [] : [-(rdn_translate(n75, rdn_pos(rdn(rdnn(n5), rdnn(n7)))))], (504 ^ _348170) ^ [] : [-(rdn_translate(nn124, rdn_neg(rdn(rdnn(n4), rdn(rdnn(n2), rdnn(n1))))))], (1078 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n8), rdnn(n4), rdnn(n2), rdnn(n1)))], (318 ^ _348170) ^ [] : [-(rdn_translate(nn31, rdn_neg(rdn(rdnn(n1), rdnn(n3)))))], (140 ^ _348170) ^ [] : [-(rdn_translate(n69, rdn_pos(rdn(rdnn(n9), rdnn(n6)))))], (322 ^ _348170) ^ [] : [-(rdn_translate(nn33, rdn_neg(rdn(rdnn(n3), rdnn(n3)))))], (874 ^ _348170) ^ [_374950, _374952, _374954, _374956, _374958, _374960, _374962, _374964, _374966, _374968, _374970] : [-(rdn_add_with_carry(rdnn(_374970), rdn(rdnn(_374968), _374966), rdn(rdnn(_374964), _374962), rdn(rdnn(_374960), _374958))), rdn_digit_add(rdnn(_374968), rdnn(_374964), rdnn(_374956), rdnn(_374954)), rdn_digit_add(rdnn(_374956), rdnn(_374970), rdnn(_374960), rdnn(_374952)), rdn_digit_add(rdnn(_374954), rdnn(_374952), rdnn(_374950), rdnn(n0)), rdn_add_with_carry(rdnn(_374950), _374966, _374962, _374958), rdn_non_zero(_374966), rdn_non_zero(_374962), rdn_non_zero(_374958)], (228 ^ _348170) ^ [] : [-(rdn_translate(n113, rdn_pos(rdn(rdnn(n3), rdn(rdnn(n1), rdnn(n1))))))], (506 ^ _348170) ^ [] : [-(rdn_translate(nn125, rdn_neg(rdn(rdnn(n5), rdn(rdnn(n2), rdnn(n1))))))], (326 ^ _348170) ^ [] : [-(rdn_translate(nn35, rdn_neg(rdn(rdnn(n5), rdnn(n3)))))], (924 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n0), rdnn(n7), rdnn(n7), rdnn(n0)))], (284 ^ _348170) ^ [] : [-(rdn_translate(nn14, rdn_neg(rdn(rdnn(n4), rdnn(n1)))))], (112 ^ _348170) ^ [] : [-(rdn_translate(n55, rdn_pos(rdn(rdnn(n5), rdnn(n5)))))], (52 ^ _348170) ^ [] : [-(rdn_translate(n25, rdn_pos(rdn(rdnn(n5), rdnn(n2)))))], (618 ^ _348170) ^ [_365788, _365790, _365792, _365794] : [-(less(_365794, _365792)), rdn_translate(_365794, rdn_neg(_365790)), rdn_translate(_365792, rdn_neg(_365788)), rdn_positive_less(_365788, _365790)], (414 ^ _348170) ^ [] : [-(rdn_translate(nn79, rdn_neg(rdn(rdnn(n9), rdnn(n7)))))], (532 ^ _348170) ^ [] : [-(rdn_positive_less(rdnn(n0), rdnn(n1)))], (372 ^ _348170) ^ [] : [-(rdn_translate(nn58, rdn_neg(rdn(rdnn(n8), rdnn(n5)))))], (1064 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n7), rdnn(n7), rdnn(n4), rdnn(n1)))], (534 ^ _348170) ^ [] : [-(rdn_positive_less(rdnn(n1), rdnn(n2)))], (304 ^ _348170) ^ [] : [-(rdn_translate(nn24, rdn_neg(rdn(rdnn(n4), rdnn(n2)))))], (370 ^ _348170) ^ [] : [-(rdn_translate(nn57, rdn_neg(rdn(rdnn(n7), rdnn(n5)))))], (1048 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n6), rdnn(n9), rdnn(n5), rdnn(n1)))], (416 ^ _348170) ^ [] : [-(rdn_translate(nn80, rdn_neg(rdn(rdnn(n0), rdnn(n8)))))], (768 ^ _348170) ^ [_370796, _370798, _370800, _370802, _370804] : [-(sum(_370804, _370802, _370800)), rdn_translate(_370804, rdn_neg(_370798)), rdn_translate(_370802, rdn_pos(_370796)), sum(_370802, _370804, _370800)], (460 ^ _348170) ^ [] : [-(rdn_translate(nn102, rdn_neg(rdn(rdnn(n2), rdn(rdnn(n0), rdnn(n1))))))], (110 ^ _348170) ^ [] : [-(rdn_translate(n54, rdn_pos(rdn(rdnn(n4), rdnn(n5)))))], (1004 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n4), rdnn(n7), rdnn(n1), rdnn(n1)))], (366 ^ _348170) ^ [] : [-(rdn_translate(nn55, rdn_neg(rdn(rdnn(n5), rdnn(n5)))))], (142 ^ _348170) ^ [] : [-(rdn_translate(n70, rdn_pos(rdn(rdnn(n0), rdnn(n7)))))], (492 ^ _348170) ^ [] : [-(rdn_translate(nn118, rdn_neg(rdn(rdnn(n8), rdn(rdnn(n1), rdnn(n1))))))], (440 ^ _348170) ^ [] : [-(rdn_translate(nn92, rdn_neg(rdn(rdnn(n2), rdnn(n9)))))], (462 ^ _348170) ^ [] : [-(rdn_translate(nn103, rdn_neg(rdn(rdnn(n3), rdn(rdnn(n0), rdnn(n1))))))], (14 ^ _348170) ^ [] : [-(rdn_translate(n6, rdn_pos(rdnn(n6))))], (948 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n1), rdnn(n9), rdnn(n0), rdnn(n1)))], (450 ^ _348170) ^ [] : [-(rdn_translate(nn97, rdn_neg(rdn(rdnn(n7), rdnn(n9)))))], (368 ^ _348170) ^ [] : [-(rdn_translate(nn56, rdn_neg(rdn(rdnn(n6), rdnn(n5)))))], (394 ^ _348170) ^ [] : [-(rdn_translate(nn69, rdn_neg(rdn(rdnn(n9), rdnn(n6)))))], (250 ^ _348170) ^ [] : [-(rdn_translate(n124, rdn_pos(rdn(rdnn(n4), rdn(rdnn(n2), rdnn(n1))))))], (344 ^ _348170) ^ [] : [-(rdn_translate(nn44, rdn_neg(rdn(rdnn(n4), rdnn(n4)))))], (660 ^ _348170) ^ [_367068, _367070] : [661 ^ _348170 : [(662 ^ _348170) ^ [] : [less(_367070, _367068)], (664 ^ _348170) ^ [] : [_367070 = _367068]], -(less_or_equal(_367070, _367068))], (966 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n2), rdnn(n8), rdnn(n0), rdnn(n1)))], (342 ^ _348170) ^ [] : [-(rdn_translate(nn43, rdn_neg(rdn(rdnn(n3), rdnn(n4)))))], (310 ^ _348170) ^ [] : [-(rdn_translate(nn27, rdn_neg(rdn(rdnn(n7), rdnn(n2)))))], (736 ^ _348170) ^ [_369749, _369751, _369753, _369755, _369757, _369759] : [-(sum(_369759, _369757, _369755)), rdn_translate(_369759, rdn_pos(_369753)), rdn_translate(_369757, rdn_neg(_369751)), rdn_positive_less(_369751, _369753), rdn_add_with_carry(rdnn(n0), _369751, _369749, _369753), rdn_translate(_369755, rdn_pos(_369749))], (542 ^ _348170) ^ [] : [-(rdn_positive_less(rdnn(n5), rdnn(n6)))], (422 ^ _348170) ^ [] : [-(rdn_translate(nn83, rdn_neg(rdn(rdnn(n3), rdnn(n8)))))], (480 ^ _348170) ^ [] : [-(rdn_translate(nn112, rdn_neg(rdn(rdnn(n2), rdn(rdnn(n1), rdnn(n1))))))], (256 ^ _348170) ^ [] : [-(rdn_translate(n127, rdn_pos(rdn(rdnn(n7), rdn(rdnn(n2), rdnn(n1))))))], (958 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n2), rdnn(n4), rdnn(n6), rdnn(n0)))], (918 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n0), rdnn(n4), rdnn(n4), rdnn(n0)))], (198 ^ _348170) ^ [] : [-(rdn_translate(n98, rdn_pos(rdn(rdnn(n8), rdnn(n9)))))], (1108 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n9), rdnn(n9), rdnn(n8), rdnn(n1)))], (608 ^ _348170) ^ [_365433, _365435, _365437, _365439] : [-(less(_365439, _365437)), rdn_translate(_365439, rdn_neg(_365435)), rdn_translate(_365437, rdn_pos(_365433))], (62 ^ _348170) ^ [] : [-(rdn_translate(n30, rdn_pos(rdn(rdnn(n0), rdnn(n3)))))], (212 ^ _348170) ^ [] : [-(rdn_translate(n105, rdn_pos(rdn(rdnn(n5), rdn(rdnn(n0), rdnn(n1))))))], (1094 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n9), rdnn(n2), rdnn(n1), rdnn(n1)))], (336 ^ _348170) ^ [] : [-(rdn_translate(nn40, rdn_neg(rdn(rdnn(n0), rdnn(n4)))))], (452 ^ _348170) ^ [] : [-(rdn_translate(nn98, rdn_neg(rdn(rdnn(n8), rdnn(n9)))))], (1032 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n6), rdnn(n1), rdnn(n7), rdnn(n0)))], (1014 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n5), rdnn(n2), rdnn(n7), rdnn(n0)))], (994 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n4), rdnn(n2), rdnn(n6), rdnn(n0)))], (144 ^ _348170) ^ [] : [-(rdn_translate(n71, rdn_pos(rdn(rdnn(n1), rdnn(n7)))))], (120 ^ _348170) ^ [] : [-(rdn_translate(n59, rdn_pos(rdn(rdnn(n9), rdnn(n5)))))], (138 ^ _348170) ^ [] : [-(rdn_translate(n68, rdn_pos(rdn(rdnn(n8), rdnn(n6)))))], (72 ^ _348170) ^ [] : [-(rdn_translate(n35, rdn_pos(rdn(rdnn(n5), rdnn(n3)))))], (182 ^ _348170) ^ [] : [-(rdn_translate(n90, rdn_pos(rdn(rdnn(n0), rdnn(n9)))))], (350 ^ _348170) ^ [] : [-(rdn_translate(nn47, rdn_neg(rdn(rdnn(n7), rdnn(n4)))))], (498 ^ _348170) ^ [] : [-(rdn_translate(nn121, rdn_neg(rdn(rdnn(n1), rdn(rdnn(n2), rdnn(n1))))))], (792 ^ _348170) ^ [_371617, _371619, _371621, _371623] : [-(_371623 = _371621), sum(_371623, _371619, _371617), sum(_371621, _371619, _371617)], (390 ^ _348170) ^ [] : [-(rdn_translate(nn67, rdn_neg(rdn(rdnn(n7), rdnn(n6)))))], (188 ^ _348170) ^ [] : [-(rdn_translate(n93, rdn_pos(rdn(rdnn(n3), rdnn(n9)))))], (1038 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n6), rdnn(n4), rdnn(n0), rdnn(n1)))], (1028 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n5), rdnn(n9), rdnn(n4), rdnn(n1)))], (446 ^ _348170) ^ [] : [-(rdn_translate(nn95, rdn_neg(rdn(rdnn(n5), rdnn(n9)))))], (8 ^ _348170) ^ [] : [-(rdn_translate(n3, rdn_pos(rdnn(n3))))], (150 ^ _348170) ^ [] : [-(rdn_translate(n74, rdn_pos(rdn(rdnn(n4), rdnn(n7)))))], (54 ^ _348170) ^ [] : [-(rdn_translate(n26, rdn_pos(rdn(rdnn(n6), rdnn(n2)))))], (30 ^ _348170) ^ [] : [-(rdn_translate(n14, rdn_pos(rdn(rdnn(n4), rdnn(n1)))))], (192 ^ _348170) ^ [] : [-(rdn_translate(n95, rdn_pos(rdn(rdnn(n5), rdnn(n9)))))], (980 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n3), rdnn(n5), rdnn(n8), rdnn(n0)))], (400 ^ _348170) ^ [] : [-(rdn_translate(nn72, rdn_neg(rdn(rdnn(n2), rdnn(n7)))))], (934 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n1), rdnn(n2), rdnn(n3), rdnn(n0)))], (1098 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n9), rdnn(n4), rdnn(n3), rdnn(n1)))], (1080 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n8), rdnn(n5), rdnn(n3), rdnn(n1)))], (1030 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n6), rdnn(n0), rdnn(n6), rdnn(n0)))], (392 ^ _348170) ^ [] : [-(rdn_translate(nn68, rdn_neg(rdn(rdnn(n8), rdnn(n6)))))], (1034 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n6), rdnn(n2), rdnn(n8), rdnn(n0)))], (516 ^ _348170) ^ [] : [-(rdn_non_zero_digit(rdnn(n2)))], (982 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n3), rdnn(n6), rdnn(n9), rdnn(n0)))], (362 ^ _348170) ^ [] : [-(rdn_translate(nn53, rdn_neg(rdn(rdnn(n3), rdnn(n5)))))], (1090 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n9), rdnn(n0), rdnn(n9), rdnn(n0)))], (442 ^ _348170) ^ [] : [-(rdn_translate(nn93, rdn_neg(rdn(rdnn(n3), rdnn(n9)))))], (490 ^ _348170) ^ [] : [-(rdn_translate(nn117, rdn_neg(rdn(rdnn(n7), rdn(rdnn(n1), rdnn(n1))))))], (1040 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n6), rdnn(n5), rdnn(n1), rdnn(n1)))], (928 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n0), rdnn(n9), rdnn(n9), rdnn(n0)))], (26 ^ _348170) ^ [] : [-(rdn_translate(n12, rdn_pos(rdn(rdnn(n2), rdnn(n1)))))], (482 ^ _348170) ^ [] : [-(rdn_translate(nn113, rdn_neg(rdn(rdnn(n3), rdn(rdnn(n1), rdnn(n1))))))], (1062 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n7), rdnn(n6), rdnn(n3), rdnn(n1)))], (1010 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n5), rdnn(n0), rdnn(n5), rdnn(n0)))], (248 ^ _348170) ^ [] : [-(rdn_translate(n123, rdn_pos(rdn(rdnn(n3), rdn(rdnn(n2), rdnn(n1))))))], (1036 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n6), rdnn(n3), rdnn(n9), rdnn(n0)))], (124 ^ _348170) ^ [] : [-(rdn_translate(n61, rdn_pos(rdn(rdnn(n1), rdnn(n6)))))], (566 ^ _348170) ^ [_363966, _363968, _363970] : [-(rdn_positive_less(rdn(rdnn(_363970), _363968), rdn(rdnn(_363966), _363968))), rdn_positive_less(rdnn(_363970), rdnn(_363966)), rdn_non_zero(_363968)], (540 ^ _348170) ^ [] : [-(rdn_positive_less(rdnn(n4), rdnn(n5)))], (930 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n1), rdnn(n0), rdnn(n1), rdnn(n0)))], (1012 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n5), rdnn(n1), rdnn(n6), rdnn(n0)))], (380 ^ _348170) ^ [] : [-(rdn_translate(nn62, rdn_neg(rdn(rdnn(n2), rdnn(n6)))))], (430 ^ _348170) ^ [] : [-(rdn_translate(nn87, rdn_neg(rdn(rdnn(n7), rdnn(n8)))))], (412 ^ _348170) ^ [] : [-(rdn_translate(nn78, rdn_neg(rdn(rdnn(n8), rdnn(n7)))))], (242 ^ _348170) ^ [] : [-(rdn_translate(n120, rdn_pos(rdn(rdnn(n0), rdn(rdnn(n2), rdnn(n1))))))], (348 ^ _348170) ^ [] : [-(rdn_translate(nn46, rdn_neg(rdn(rdnn(n6), rdnn(n4)))))], (1082 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n8), rdnn(n6), rdnn(n4), rdnn(n1)))], (802 ^ _348170) ^ [_371968, _371970, _371972, _371974] : [-(_371972 = _371970), sum(_371974, _371972, _371968), sum(_371974, _371970, _371968)], (512 ^ _348170) ^ [] : [-(rdn_translate(nn128, rdn_neg(rdn(rdnn(n8), rdn(rdnn(n2), rdnn(n1))))))], (904 ^ _348170) ^ [_376116, _376118, _376120, _376122, _376124, _376126] : [rdn_add_with_carry(rdnn(_376126), rdnn(_376120), rdn(rdnn(_376124), _376122), rdn(rdnn(_376118), _376116)), -(rdn_add_with_carry(rdnn(_376126), rdn(rdnn(_376124), _376122), rdnn(_376120), rdn(rdnn(_376118), _376116)))], (78 ^ _348170) ^ [] : [-(rdn_translate(n38, rdn_pos(rdn(rdnn(n8), rdnn(n3)))))], (214 ^ _348170) ^ [] : [-(rdn_translate(n106, rdn_pos(rdn(rdnn(n6), rdn(rdnn(n0), rdnn(n1))))))], (164 ^ _348170) ^ [] : [-(rdn_translate(n81, rdn_pos(rdn(rdnn(n1), rdnn(n8)))))], (270 ^ _348170) ^ [] : [-(rdn_translate(nn7, rdn_neg(rdnn(n7))))], (502 ^ _348170) ^ [] : [-(rdn_translate(nn123, rdn_neg(rdn(rdnn(n3), rdn(rdnn(n2), rdnn(n1))))))], (398 ^ _348170) ^ [] : [-(rdn_translate(nn71, rdn_neg(rdn(rdnn(n1), rdnn(n7)))))], (1106 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n9), rdnn(n8), rdnn(n7), rdnn(n1)))], (356 ^ _348170) ^ [] : [-(rdn_translate(nn50, rdn_neg(rdn(rdnn(n0), rdnn(n5)))))], (56 ^ _348170) ^ [] : [-(rdn_translate(n27, rdn_pos(rdn(rdnn(n7), rdnn(n2)))))], (1054 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n7), rdnn(n2), rdnn(n9), rdnn(n0)))], (76 ^ _348170) ^ [] : [-(rdn_translate(n37, rdn_pos(rdn(rdnn(n7), rdnn(n3)))))], (252 ^ _348170) ^ [] : [-(rdn_translate(n125, rdn_pos(rdn(rdnn(n5), rdn(rdnn(n2), rdnn(n1))))))], (64 ^ _348170) ^ [] : [-(rdn_translate(n31, rdn_pos(rdn(rdnn(n1), rdnn(n3)))))], (996 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n4), rdnn(n3), rdnn(n7), rdnn(n0)))], (196 ^ _348170) ^ [] : [-(rdn_translate(n97, rdn_pos(rdn(rdnn(n7), rdnn(n9)))))], (1018 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n5), rdnn(n4), rdnn(n9), rdnn(n0)))], (202 ^ _348170) ^ [] : [-(rdn_translate(n100, rdn_pos(rdn(rdnn(n0), rdn(rdnn(n0), rdnn(n1))))))], (420 ^ _348170) ^ [] : [-(rdn_translate(nn82, rdn_neg(rdn(rdnn(n2), rdnn(n8)))))], (268 ^ _348170) ^ [] : [-(rdn_translate(nn6, rdn_neg(rdnn(n6))))], (126 ^ _348170) ^ [] : [-(rdn_translate(n62, rdn_pos(rdn(rdnn(n2), rdnn(n6)))))], (536 ^ _348170) ^ [] : [-(rdn_positive_less(rdnn(n2), rdnn(n3)))], (514 ^ _348170) ^ [] : [-(rdn_non_zero_digit(rdnn(n1)))], (106 ^ _348170) ^ [] : [-(rdn_translate(n52, rdn_pos(rdn(rdnn(n2), rdnn(n5)))))], (1072 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n8), rdnn(n1), rdnn(n9), rdnn(n0)))], (396 ^ _348170) ^ [] : [-(rdn_translate(nn70, rdn_neg(rdn(rdnn(n0), rdnn(n7)))))], (640 ^ _348170) ^ [_366480, _366482] : [-(less(_366482, _366480)), -(less(_366480, _366482)), -(_366480 = _366482)], (464 ^ _348170) ^ [] : [-(rdn_translate(nn104, rdn_neg(rdn(rdnn(n4), rdn(rdnn(n0), rdnn(n1))))))], (200 ^ _348170) ^ [] : [-(rdn_translate(n99, rdn_pos(rdn(rdnn(n9), rdnn(n9)))))], (118 ^ _348170) ^ [] : [-(rdn_translate(n58, rdn_pos(rdn(rdnn(n8), rdnn(n5)))))], (522 ^ _348170) ^ [] : [-(rdn_non_zero_digit(rdnn(n5)))], (632 ^ _348170) ^ [_366241, _366243] : [less(_366243, _366241), 635 ^ _348170 : [(636 ^ _348170) ^ [] : [less(_366241, _366243)], (638 ^ _348170) ^ [] : [_366241 = _366243]]], (102 ^ _348170) ^ [] : [-(rdn_translate(n50, rdn_pos(rdn(rdnn(n0), rdnn(n5)))))], (280 ^ _348170) ^ [] : [-(rdn_translate(nn12, rdn_neg(rdn(rdnn(n2), rdnn(n1)))))], (238 ^ _348170) ^ [] : [-(rdn_translate(n118, rdn_pos(rdn(rdnn(n8), rdn(rdnn(n1), rdnn(n1))))))], (508 ^ _348170) ^ [] : [-(rdn_translate(nn126, rdn_neg(rdn(rdnn(n6), rdn(rdnn(n2), rdnn(n1))))))], (418 ^ _348170) ^ [] : [-(rdn_translate(nn81, rdn_neg(rdn(rdnn(n1), rdnn(n8)))))], (314 ^ _348170) ^ [] : [-(rdn_translate(nn29, rdn_neg(rdn(rdnn(n9), rdnn(n2)))))], (1076 ^ _348170) ^ [] : [-(rdn_digit_add(rdnn(n8), rdnn(n3), rdnn(n1), rdnn(n1)))], (262 ^ _348170) ^ [] : [-(rdn_translate(nn3, rdn_neg(rdnn(n3))))], (40 ^ _348170) ^ [] : [-(rdn_translate(n19, rdn_pos(rdn(rdnn(n9), rdnn(n1)))))], (576 ^ _348170) ^ [_364315, _364317, _364319] : [rdn_non_zero(_364315), -(rdn_positive_less(rdnn(_364319), rdn(rdnn(_364317), _364315)))], (44 ^ _348170) ^ [] : [-(rdn_translate(n21, rdn_pos(rdn(rdnn(n1), rdnn(n2)))))], (272 ^ _348170) ^ [] : [-(rdn_translate(nn8, rdn_neg(rdnn(n8))))]], input).
% 246.34/238.41 ncf('1',plain,[less(n6, n5), 636 : less(n5, n6)],start(632 ^ 0,bind([[_366241, _366243], [n5, n6]]))).
% 246.34/238.41 ncf('1.1',plain,[-(less(n6, n5)), less_or_equal(n6, n5), -(n6 = n5)],extension(650 ^ 1,bind([[_366816, _366818], [n5, n6]]))).
% 246.34/238.41 ncf('1.1.1',plain,[-(less_or_equal(n6, n5)), 664 : n6 = n5],extension(660 ^ 2,bind([[_367068, _367070], [n5, n6]]))).
% 246.34/238.41 ncf('1.1.1.1',plain,[-(n6 = n5), sum(n2, n3, n6), sum(n2, n3, n5)],extension(782 ^ 5,bind([[_371266, _371268, _371270, _371272], [n5, n6, n3, n2]]))).
% 246.34/238.41 ncf('1.1.1.1.1',plain,[-(sum(n2, n3, n6))],extension(1110 ^ 6)).
% 246.34/238.41 ncf('1.1.1.1.2',plain,[-(sum(n2, n3, n5)), rdn_translate(n2, rdn_pos(rdnn(n2))), rdn_translate(n3, rdn_pos(rdnn(n3))), rdn_add_with_carry(rdnn(n0), rdnn(n2), rdnn(n3), rdnn(n5)), rdn_translate(n5, rdn_pos(rdnn(n5)))],extension(678 ^ 6,bind([[_367775, _367777, _367779, _367781, _367783, _367785], [rdnn(n5), rdnn(n3), rdnn(n2), n5, n3, n2]]))).
% 246.34/238.41 ncf('1.1.1.1.2.1',plain,[-(rdn_translate(n2, rdn_pos(rdnn(n2))))],extension(6 ^ 7)).
% 246.34/238.41 ncf('1.1.1.1.2.2',plain,[-(rdn_translate(n3, rdn_pos(rdnn(n3))))],extension(8 ^ 7)).
% 246.34/238.41 ncf('1.1.1.1.2.3',plain,[-(rdn_add_with_carry(rdnn(n0), rdnn(n2), rdnn(n3), rdnn(n5))), rdn_digit_add(rdnn(n2), rdnn(n3), rdnn(n5), rdnn(n0)), rdn_digit_add(rdnn(n5), rdnn(n0), rdnn(n5), rdnn(n0))],extension(824 ^ 7,bind([[_372770, _372772, _372774, _372776, _372778], [n5, n5, n3, n2, n0]]))).
% 246.34/238.41 ncf('1.1.1.1.2.3.1',plain,[-(rdn_digit_add(rdnn(n2), rdnn(n3), rdnn(n5), rdnn(n0)))],extension(956 ^ 8)).
% 246.34/238.41 ncf('1.1.1.1.2.3.2',plain,[-(rdn_digit_add(rdnn(n5), rdnn(n0), rdnn(n5), rdnn(n0)))],extension(1010 ^ 8)).
% 246.34/238.41 ncf('1.1.1.1.2.4',plain,[-(rdn_translate(n5, rdn_pos(rdnn(n5))))],extension(12 ^ 7)).
% 246.34/238.41 ncf('1.1.2',plain,[n6 = n5, less(n5, n6)],extension(632 ^ 2,bind([[_366241, _366243], [n6, n5]]))).
% 246.34/238.41 ncf('1.1.2.1',plain,[-(less(n5, n6)), rdn_translate(n5, rdn_pos(rdnn(n5))), rdn_translate(n6, rdn_pos(rdnn(n6))), rdn_positive_less(rdnn(n5), rdnn(n6))],extension(594 ^ 3,bind([[_364981, _364983, _364985, _364987], [rdnn(n6), rdnn(n5), n6, n5]]))).
% 246.34/238.41 ncf('1.1.2.1.1',plain,[-(rdn_translate(n5, rdn_pos(rdnn(n5))))],extension(12 ^ 4)).
% 246.34/238.41 ncf('1.1.2.1.2',plain,[-(rdn_translate(n6, rdn_pos(rdnn(n6))))],extension(14 ^ 4)).
% 246.34/238.41 ncf('1.1.2.1.3',plain,[-(rdn_positive_less(rdnn(n5), rdnn(n6)))],extension(542 ^ 4)).
% 246.34/238.41 ncf('1.2',plain,[-(less(n5, n6)), rdn_translate(n5, rdn_pos(rdnn(n5))), rdn_translate(n6, rdn_pos(rdnn(n6))), rdn_positive_less(rdnn(n5), rdnn(n6))],extension(594 ^ 3,bind([[_364981, _364983, _364985, _364987], [rdnn(n6), rdnn(n5), n6, n5]]))).
% 246.34/238.41 ncf('1.2.1',plain,[-(rdn_translate(n5, rdn_pos(rdnn(n5))))],extension(12 ^ 4)).
% 246.34/238.41 ncf('1.2.2',plain,[-(rdn_translate(n6, rdn_pos(rdnn(n6))))],extension(14 ^ 4)).
% 246.34/238.41 ncf('1.2.3',plain,[-(rdn_positive_less(rdnn(n5), rdnn(n6)))],extension(542 ^ 4)).
% 246.34/238.41 %-----------------------------------------------------
% 246.34/238.41 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------