%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM330+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n018.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 278.10s 269.27s
% Output : Proof 278.10s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.11 % Problem : NUM330+1 : TPTP v8.1.2. Released v3.1.0.
% 0.10/0.12 % Command : nanocop.sh %s %d
% 0.11/0.33 % Computer : n018.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Thu May 18 17:51:57 EDT 2023
% 0.11/0.33 % CPUTime :
% 278.10/269.27
% 278.10/269.27 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 278.10/269.27 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 278.10/269.27 %-----------------------------------------------------
% 278.10/269.27 ncf(matrix, plain, [(212 ^ _343593) ^ [] : [-(rdn_translate(n4, rdn_pos(rdnn(n4))))], (224 ^ _343593) ^ [] : [-(rdn_translate(n10, rdn_pos(rdn(rdnn(n0), rdnn(n1)))))], (270 ^ _343593) ^ [] : [-(rdn_translate(n33, rdn_pos(rdn(rdnn(n3), rdnn(n3)))))], (378 ^ _343593) ^ [] : [-(rdn_translate(n87, rdn_pos(rdn(rdnn(n7), rdnn(n8)))))], (466 ^ _343593) ^ [] : [-(rdn_translate(nn4, rdn_neg(rdnn(n4))))], (518 ^ _343593) ^ [] : [-(rdn_translate(nn30, rdn_neg(rdn(rdnn(n0), rdnn(n3)))))], (534 ^ _343593) ^ [] : [-(rdn_translate(nn38, rdn_neg(rdn(rdnn(n8), rdnn(n3)))))], (658 ^ _343593) ^ [] : [-(rdn_translate(nn100, rdn_neg(rdn(rdnn(n0), rdn(rdnn(n0), rdnn(n1))))))], (746 ^ _343593) ^ [] : [-(rdn_positive_less(rdnn(n6), rdnn(n7)))], (1114 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n0), rdnn(n1), rdnn(n1), rdnn(n0)))], (1140 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n1), rdnn(n4), rdnn(n5), rdnn(n0)))], (1148 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n1), rdnn(n8), rdnn(n9), rdnn(n0)))], (1194 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n4), rdnn(n1), rdnn(n5), rdnn(n0)))], (1196 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n4), rdnn(n2), rdnn(n6), rdnn(n0)))], (1206 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n4), rdnn(n7), rdnn(n1), rdnn(n1)))], (1272 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n8), rdnn(n0), rdnn(n8), rdnn(n0)))], (1292 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n9), rdnn(n0), rdnn(n9), rdnn(n0)))], (228 ^ _343593) ^ [] : [-(rdn_translate(n12, rdn_pos(rdn(rdnn(n2), rdnn(n1)))))], (440 ^ _343593) ^ [] : [-(rdn_translate(n118, rdn_pos(rdn(rdnn(n8), rdn(rdnn(n1), rdnn(n1))))))], (486 ^ _343593) ^ [] : [-(rdn_translate(nn14, rdn_neg(rdn(rdnn(n4), rdnn(n1)))))], (530 ^ _343593) ^ [] : [-(rdn_translate(nn36, rdn_neg(rdn(rdnn(n6), rdnn(n3)))))], (562 ^ _343593) ^ [] : [-(rdn_translate(nn52, rdn_neg(rdn(rdnn(n2), rdnn(n5)))))], (708 ^ _343593) ^ [] : [-(rdn_translate(nn125, rdn_neg(rdn(rdnn(n5), rdn(rdnn(n2), rdnn(n1))))))], (736 ^ _343593) ^ [] : [-(rdn_positive_less(rdnn(n1), rdnn(n2)))], (1050 ^ _343593) ^ [_376122, _376124, _376126, _376128, _376130, _376132, _376134, _376136, _376138, _376140] : [-(rdn_add_with_carry(rdnn(_376140), rdnn(_376138), rdn(rdnn(_376136), _376134), rdn(rdnn(_376132), _376130))), rdn_digit_add(rdnn(_376138), rdnn(_376136), rdnn(_376128), rdnn(_376126)), rdn_digit_add(rdnn(_376128), rdnn(_376140), rdnn(_376132), rdnn(_376124)), rdn_digit_add(rdnn(_376126), rdnn(_376124), rdnn(_376122), rdnn(n0)), rdn_add_with_carry(rdnn(_376122), rdnn(n0), _376134, _376130), rdn_non_zero(_376134), rdn_non_zero(_376130)], (1172 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n3), rdnn(n0), rdnn(n3), rdnn(n0)))], (1226 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n5), rdnn(n7), rdnn(n2), rdnn(n1)))], (1246 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n6), rdnn(n7), rdnn(n3), rdnn(n1)))], (1264 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n7), rdnn(n6), rdnn(n3), rdnn(n1)))], (1288 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n8), rdnn(n8), rdnn(n6), rdnn(n1)))], (1306 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n9), rdnn(n7), rdnn(n6), rdnn(n1)))], (214 ^ _343593) ^ [] : [-(rdn_translate(n5, rdn_pos(rdnn(n5))))], (220 ^ _343593) ^ [] : [-(rdn_translate(n8, rdn_pos(rdnn(n8))))], (294 ^ _343593) ^ [] : [-(rdn_translate(n45, rdn_pos(rdn(rdnn(n5), rdnn(n4)))))], (364 ^ _343593) ^ [] : [-(rdn_translate(n80, rdn_pos(rdn(rdnn(n0), rdnn(n8)))))], (458 ^ _343593) ^ [] : [-(rdn_translate(n127, rdn_pos(rdn(rdnn(n7), rdn(rdnn(n2), rdnn(n1))))))], (498 ^ _343593) ^ [] : [-(rdn_translate(nn20, rdn_neg(rdn(rdnn(n0), rdnn(n2)))))], (572 ^ _343593) ^ [] : [-(rdn_translate(nn57, rdn_neg(rdn(rdnn(n7), rdnn(n5)))))], (596 ^ _343593) ^ [] : [-(rdn_translate(nn69, rdn_neg(rdn(rdnn(n9), rdnn(n6)))))], (674 ^ _343593) ^ [] : [-(rdn_translate(nn108, rdn_neg(rdn(rdnn(n8), rdn(rdnn(n0), rdnn(n1))))))], (690 ^ _343593) ^ [] : [-(rdn_translate(nn116, rdn_neg(rdn(rdnn(n6), rdn(rdnn(n1), rdnn(n1))))))], (1120 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n0), rdnn(n4), rdnn(n4), rdnn(n0)))], (114 ^ _343593) ^ [_347420, _347422, _347424, _347426, _347428, _347430, _347432, _347434] : [-(rdn_add_with_carry(_347432, _347428, _347424, _347420)), rdn_add_with_carry(_347434, _347430, _347426, _347422), _347434 = _347432, _347430 = _347428, _347426 = _347424, _347422 = _347420], (218 ^ _343593) ^ [] : [-(rdn_translate(n7, rdn_pos(rdnn(n7))))], (384 ^ _343593) ^ [] : [-(rdn_translate(n90, rdn_pos(rdn(rdnn(n0), rdnn(n9)))))], (516 ^ _343593) ^ [] : [-(rdn_translate(nn29, rdn_neg(rdn(rdnn(n9), rdnn(n2)))))], (668 ^ _343593) ^ [] : [-(rdn_translate(nn105, rdn_neg(rdn(rdnn(n5), rdn(rdnn(n0), rdnn(n1))))))], (682 ^ _343593) ^ [] : [-(rdn_translate(nn112, rdn_neg(rdn(rdnn(n2), rdn(rdnn(n1), rdnn(n1))))))], (720 ^ _343593) ^ [] : [-(rdn_non_zero_digit(rdnn(n3)))], (784 ^ _343593) ^ [_366782] : [rdn_non_zero_digit(rdnn(_366782)), -(rdn_non_zero(rdnn(_366782)))], (1168 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n2), rdnn(n8), rdnn(n0), rdnn(n1)))], (1214 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n5), rdnn(n1), rdnn(n6), rdnn(n0)))], (1270 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n7), rdnn(n9), rdnn(n6), rdnn(n1)))], (208 ^ _343593) ^ [] : [-(rdn_translate(n2, rdn_pos(rdnn(n2))))], (250 ^ _343593) ^ [] : [-(rdn_translate(n23, rdn_pos(rdn(rdnn(n3), rdnn(n2)))))], (326 ^ _343593) ^ [] : [-(rdn_translate(n61, rdn_pos(rdn(rdnn(n1), rdnn(n6)))))], (346 ^ _343593) ^ [] : [-(rdn_translate(n71, rdn_pos(rdn(rdnn(n1), rdnn(n7)))))], (442 ^ _343593) ^ [] : [-(rdn_translate(n119, rdn_pos(rdn(rdnn(n9), rdn(rdnn(n1), rdnn(n1))))))], (480 ^ _343593) ^ [] : [-(rdn_translate(nn11, rdn_neg(rdn(rdnn(n1), rdnn(n1)))))], (506 ^ _343593) ^ [] : [-(rdn_translate(nn24, rdn_neg(rdn(rdnn(n4), rdnn(n2)))))], (568 ^ _343593) ^ [] : [-(rdn_translate(nn55, rdn_neg(rdn(rdnn(n5), rdnn(n5)))))], (588 ^ _343593) ^ [] : [-(rdn_translate(nn65, rdn_neg(rdn(rdnn(n5), rdnn(n6)))))], (622 ^ _343593) ^ [] : [-(rdn_translate(nn82, rdn_neg(rdn(rdnn(n2), rdnn(n8)))))], (624 ^ _343593) ^ [] : [-(rdn_translate(nn83, rdn_neg(rdn(rdnn(n3), rdnn(n8)))))], (638 ^ _343593) ^ [] : [-(rdn_translate(nn90, rdn_neg(rdn(rdnn(n0), rdnn(n9)))))], (698 ^ _343593) ^ [] : [-(rdn_translate(nn120, rdn_neg(rdn(rdnn(n0), rdn(rdnn(n2), rdnn(n1))))))], (768 ^ _343593) ^ [_366219, _366221, _366223] : [-(rdn_positive_less(rdn(rdnn(_366223), _366221), rdn(rdnn(_366219), _366221))), rdn_positive_less(rdnn(_366223), rdnn(_366219)), rdn_non_zero(_366221)], (1198 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n4), rdnn(n3), rdnn(n7), rdnn(n0)))], (86 ^ _343593) ^ [_346488, _346490, _346492, _346494, _346496, _346498] : [-(difference(_346496, _346492, _346488)), difference(_346498, _346494, _346490), _346498 = _346496, _346494 = _346492, _346490 = _346488], (246 ^ _343593) ^ [] : [-(rdn_translate(n21, rdn_pos(rdn(rdnn(n1), rdnn(n2)))))], (344 ^ _343593) ^ [] : [-(rdn_translate(n70, rdn_pos(rdn(rdnn(n0), rdnn(n7)))))], (366 ^ _343593) ^ [] : [-(rdn_translate(n81, rdn_pos(rdn(rdnn(n1), rdnn(n8)))))], (456 ^ _343593) ^ [] : [-(rdn_translate(n126, rdn_pos(rdn(rdnn(n6), rdn(rdnn(n2), rdnn(n1))))))], (478 ^ _343593) ^ [] : [-(rdn_translate(nn10, rdn_neg(rdn(rdnn(n0), rdnn(n1)))))], (542 ^ _343593) ^ [] : [-(rdn_translate(nn42, rdn_neg(rdn(rdnn(n2), rdnn(n4)))))], (570 ^ _343593) ^ [] : [-(rdn_translate(nn56, rdn_neg(rdn(rdnn(n6), rdnn(n5)))))], (664 ^ _343593) ^ [] : [-(rdn_translate(nn103, rdn_neg(rdn(rdnn(n3), rdn(rdnn(n0), rdnn(n1))))))], (710 ^ _343593) ^ [] : [-(rdn_translate(nn126, rdn_neg(rdn(rdnn(n6), rdn(rdnn(n2), rdnn(n1))))))], (738 ^ _343593) ^ [] : [-(rdn_positive_less(rdnn(n2), rdnn(n3)))], (1144 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n1), rdnn(n6), rdnn(n7), rdnn(n0)))], (1176 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n3), rdnn(n2), rdnn(n5), rdnn(n0)))], (1216 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n5), rdnn(n2), rdnn(n7), rdnn(n0)))], (1224 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n5), rdnn(n6), rdnn(n1), rdnn(n1)))], (1280 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n8), rdnn(n4), rdnn(n2), rdnn(n1)))], (30 ^ _343593) ^ [_344684, _344686, _344688, _344690] : [-(less(_344688, _344684)), less(_344690, _344686), _344690 = _344688, _344686 = _344684], (280 ^ _343593) ^ [] : [-(rdn_translate(n38, rdn_pos(rdn(rdnn(n8), rdnn(n3)))))], (290 ^ _343593) ^ [] : [-(rdn_translate(n43, rdn_pos(rdn(rdnn(n3), rdnn(n4)))))], (302 ^ _343593) ^ [] : [-(rdn_translate(n49, rdn_pos(rdn(rdnn(n9), rdnn(n4)))))], (318 ^ _343593) ^ [] : [-(rdn_translate(n57, rdn_pos(rdn(rdnn(n7), rdnn(n5)))))], (382 ^ _343593) ^ [] : [-(rdn_translate(n89, rdn_pos(rdn(rdnn(n9), rdnn(n8)))))], (416 ^ _343593) ^ [] : [-(rdn_translate(n106, rdn_pos(rdn(rdnn(n6), rdn(rdnn(n0), rdnn(n1))))))], (610 ^ _343593) ^ [] : [-(rdn_translate(nn76, rdn_neg(rdn(rdnn(n6), rdnn(n7)))))], (1136 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n1), rdnn(n2), rdnn(n3), rdnn(n0)))], (1162 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n2), rdnn(n5), rdnn(n7), rdnn(n0)))], (240 ^ _343593) ^ [] : [-(rdn_translate(n18, rdn_pos(rdn(rdnn(n8), rdnn(n1)))))], (282 ^ _343593) ^ [] : [-(rdn_translate(n39, rdn_pos(rdn(rdnn(n9), rdnn(n3)))))], (358 ^ _343593) ^ [] : [-(rdn_translate(n77, rdn_pos(rdn(rdnn(n7), rdnn(n7)))))], (390 ^ _343593) ^ [] : [-(rdn_translate(n93, rdn_pos(rdn(rdnn(n3), rdnn(n9)))))], (446 ^ _343593) ^ [] : [-(rdn_translate(n121, rdn_pos(rdn(rdnn(n1), rdn(rdnn(n2), rdnn(n1))))))], (538 ^ _343593) ^ [] : [-(rdn_translate(nn40, rdn_neg(rdn(rdnn(n0), rdnn(n4)))))], (686 ^ _343593) ^ [] : [-(rdn_translate(nn114, rdn_neg(rdn(rdnn(n4), rdn(rdnn(n1), rdnn(n1))))))], (714 ^ _343593) ^ [] : [-(rdn_translate(nn128, rdn_neg(rdn(rdnn(n8), rdn(rdnn(n2), rdnn(n1))))))], (790 ^ _343593) ^ [_366990, _366992] : [rdn_non_zero(_366990), -(rdn_non_zero(rdn(rdnn(_366992), _366990)))], (1156 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n2), rdnn(n2), rdnn(n4), rdnn(n0)))], (1240 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n6), rdnn(n4), rdnn(n0), rdnn(n1)))], (1296 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n9), rdnn(n2), rdnn(n1), rdnn(n1)))], (1310 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n9), rdnn(n9), rdnn(n8), rdnn(n1)))], (328 ^ _343593) ^ [] : [-(rdn_translate(n62, rdn_pos(rdn(rdnn(n2), rdnn(n6)))))], (460 ^ _343593) ^ [] : [-(rdn_translate(nn1, rdn_neg(rdnn(n1))))], (548 ^ _343593) ^ [] : [-(rdn_translate(nn45, rdn_neg(rdn(rdnn(n5), rdnn(n4)))))], (608 ^ _343593) ^ [] : [-(rdn_translate(nn75, rdn_neg(rdn(rdnn(n5), rdnn(n7)))))], (632 ^ _343593) ^ [] : [-(rdn_translate(nn87, rdn_neg(rdn(rdnn(n7), rdnn(n8)))))], (726 ^ _343593) ^ [] : [-(rdn_non_zero_digit(rdnn(n6)))], (842 ^ _343593) ^ [_368733, _368735] : [-(less(_368735, _368733)), -(less(_368733, _368735)), -(_368733 = _368735)], (1004 ^ _343593) ^ [_374221, _374223, _374225, _374227] : [-(_374225 = _374223), sum(_374227, _374225, _374221), sum(_374227, _374223, _374221)], (1146 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n1), rdnn(n7), rdnn(n8), rdnn(n0)))], (1178 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n3), rdnn(n3), rdnn(n6), rdnn(n0)))], (1184 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n3), rdnn(n6), rdnn(n9), rdnn(n0)))], (1286 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n8), rdnn(n7), rdnn(n5), rdnn(n1)))], (1308 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n9), rdnn(n8), rdnn(n7), rdnn(n1)))], (20 ^ _343593) ^ [_344361, _344363] : [-(rdn_non_zero_digit(_344361)), _344363 = _344361, rdn_non_zero_digit(_344363)], (58 ^ _343593) ^ [_345572, _345574, _345576, _345578] : [-(rdn_positive_less(_345576, _345572)), rdn_positive_less(_345578, _345574), _345578 = _345576, _345574 = _345572], (252 ^ _343593) ^ [] : [-(rdn_translate(n24, rdn_pos(rdn(rdnn(n4), rdnn(n2)))))], (264 ^ _343593) ^ [] : [-(rdn_translate(n30, rdn_pos(rdn(rdnn(n0), rdnn(n3)))))], (392 ^ _343593) ^ [] : [-(rdn_translate(n94, rdn_pos(rdn(rdnn(n4), rdnn(n9)))))], (472 ^ _343593) ^ [] : [-(rdn_translate(nn7, rdn_neg(rdnn(n7))))], (512 ^ _343593) ^ [] : [-(rdn_translate(nn27, rdn_neg(rdn(rdnn(n7), rdnn(n2)))))], (558 ^ _343593) ^ [] : [-(rdn_translate(nn50, rdn_neg(rdn(rdnn(n0), rdnn(n5)))))], (576 ^ _343593) ^ [] : [-(rdn_translate(nn59, rdn_neg(rdn(rdnn(n9), rdnn(n5)))))], (634 ^ _343593) ^ [] : [-(rdn_translate(nn88, rdn_neg(rdn(rdnn(n8), rdnn(n8)))))], (716 ^ _343593) ^ [] : [-(rdn_non_zero_digit(rdnn(n1)))], (810 ^ _343593) ^ [_367686, _367688, _367690, _367692] : [-(less(_367692, _367690)), rdn_translate(_367692, rdn_neg(_367688)), rdn_translate(_367690, rdn_pos(_367686))], (870 ^ _343593) ^ [_369601, _369603, _369605] : [-(less_or_equal(_369601, _369605)), sum(_369605, n1, _369603), less(_369601, _369603)], (1122 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n0), rdnn(n5), rdnn(n5), rdnn(n0)))], (1186 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n3), rdnn(n7), rdnn(n0), rdnn(n1)))], (1236 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n6), rdnn(n2), rdnn(n8), rdnn(n0)))], (1254 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n7), rdnn(n1), rdnn(n8), rdnn(n0)))], (2 ^ _343593) ^ [_343737] : [-(_343737 = _343737)], (244 ^ _343593) ^ [] : [-(rdn_translate(n20, rdn_pos(rdn(rdnn(n0), rdnn(n2)))))], (388 ^ _343593) ^ [] : [-(rdn_translate(n92, rdn_pos(rdn(rdnn(n2), rdnn(n9)))))], (432 ^ _343593) ^ [] : [-(rdn_translate(n114, rdn_pos(rdn(rdnn(n4), rdn(rdnn(n1), rdnn(n1))))))], (692 ^ _343593) ^ [] : [-(rdn_translate(nn117, rdn_neg(rdn(rdnn(n7), rdn(rdnn(n1), rdnn(n1))))))], (1036 ^ _343593) ^ [_375474, _375476, _375478, _375480, _375482, _375484, _375486] : [-(rdn_add_with_carry(rdnn(_375486), rdnn(_375484), rdnn(_375482), rdn(rdnn(_375478), rdnn(n1)))), rdn_digit_add(rdnn(_375484), rdnn(_375482), rdnn(_375480), rdnn(_375476)), rdn_digit_add(rdnn(_375480), rdnn(_375486), rdnn(_375478), rdnn(_375474)), rdn_digit_add(rdnn(_375476), rdnn(_375474), rdnn(n1), rdnn(n0))], (1128 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n0), rdnn(n8), rdnn(n8), rdnn(n0)))], (1180 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n3), rdnn(n4), rdnn(n7), rdnn(n0)))], (1260 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n7), rdnn(n4), rdnn(n1), rdnn(n1)))], (4 ^ _343593) ^ [_343844, _343846] : [_343846 = _343844, -(_343844 = _343846)], (248 ^ _343593) ^ [] : [-(rdn_translate(n22, rdn_pos(rdn(rdnn(n2), rdnn(n2)))))], (314 ^ _343593) ^ [] : [-(rdn_translate(n55, rdn_pos(rdn(rdnn(n5), rdnn(n5)))))], (362 ^ _343593) ^ [] : [-(rdn_translate(n79, rdn_pos(rdn(rdnn(n9), rdnn(n7)))))], (536 ^ _343593) ^ [] : [-(rdn_translate(nn39, rdn_neg(rdn(rdnn(n9), rdnn(n3)))))], (554 ^ _343593) ^ [] : [-(rdn_translate(nn48, rdn_neg(rdn(rdnn(n8), rdnn(n4)))))], (656 ^ _343593) ^ [] : [-(rdn_translate(nn99, rdn_neg(rdn(rdnn(n9), rdnn(n9)))))], (696 ^ _343593) ^ [] : [-(rdn_translate(nn119, rdn_neg(rdn(rdnn(n9), rdn(rdnn(n1), rdnn(n1))))))], (732 ^ _343593) ^ [] : [-(rdn_non_zero_digit(rdnn(n9)))], (778 ^ _343593) ^ [_366568, _366570, _366572] : [rdn_non_zero(_366568), -(rdn_positive_less(rdnn(_366572), rdn(rdnn(_366570), _366568)))], (862 ^ _343593) ^ [_369321, _369323] : [863 ^ _343593 : [(864 ^ _343593) ^ [] : [less(_369323, _369321)], (866 ^ _343593) ^ [] : [_369323 = _369321]], -(less_or_equal(_369323, _369321))], (1302 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n9), rdnn(n5), rdnn(n4), rdnn(n1)))], (232 ^ _343593) ^ [] : [-(rdn_translate(n14, rdn_pos(rdn(rdnn(n4), rdnn(n1)))))], (372 ^ _343593) ^ [] : [-(rdn_translate(n84, rdn_pos(rdn(rdnn(n4), rdnn(n8)))))], (410 ^ _343593) ^ [] : [-(rdn_translate(n103, rdn_pos(rdn(rdnn(n3), rdn(rdnn(n0), rdnn(n1))))))], (420 ^ _343593) ^ [] : [-(rdn_translate(n108, rdn_pos(rdn(rdnn(n8), rdn(rdnn(n0), rdnn(n1))))))], (474 ^ _343593) ^ [] : [-(rdn_translate(nn8, rdn_neg(rdnn(n8))))], (490 ^ _343593) ^ [] : [-(rdn_translate(nn16, rdn_neg(rdn(rdnn(n6), rdnn(n1)))))], (502 ^ _343593) ^ [] : [-(rdn_translate(nn22, rdn_neg(rdn(rdnn(n2), rdnn(n2)))))], (582 ^ _343593) ^ [] : [-(rdn_translate(nn62, rdn_neg(rdn(rdnn(n2), rdnn(n6)))))], (604 ^ _343593) ^ [] : [-(rdn_translate(nn73, rdn_neg(rdn(rdnn(n3), rdnn(n7)))))], (612 ^ _343593) ^ [] : [-(rdn_translate(nn77, rdn_neg(rdn(rdnn(n7), rdnn(n7)))))], (728 ^ _343593) ^ [] : [-(rdn_non_zero_digit(rdnn(n7)))], (852 ^ _343593) ^ [_369069, _369071] : [less_or_equal(_369071, _369069), -(less(_369071, _369069)), -(_369071 = _369069)], (1164 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n2), rdnn(n6), rdnn(n8), rdnn(n0)))], (1170 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n2), rdnn(n9), rdnn(n1), rdnn(n1)))], (1222 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n5), rdnn(n5), rdnn(n0), rdnn(n1)))], (1238 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n6), rdnn(n3), rdnn(n9), rdnn(n0)))], (188 ^ _343593) ^ [_349993, _349995, _349997, _349999] : [-(rdn(_349999, _349995) = rdn(_349997, _349993)), _349999 = _349997, _349995 = _349993], (234 ^ _343593) ^ [] : [-(rdn_translate(n15, rdn_pos(rdn(rdnn(n5), rdnn(n1)))))], (316 ^ _343593) ^ [] : [-(rdn_translate(n56, rdn_pos(rdn(rdnn(n6), rdnn(n5)))))], (354 ^ _343593) ^ [] : [-(rdn_translate(n75, rdn_pos(rdn(rdnn(n5), rdnn(n7)))))], (374 ^ _343593) ^ [] : [-(rdn_translate(n85, rdn_pos(rdn(rdnn(n5), rdnn(n8)))))], (406 ^ _343593) ^ [] : [-(rdn_translate(n101, rdn_pos(rdn(rdnn(n1), rdn(rdnn(n0), rdnn(n1))))))], (468 ^ _343593) ^ [] : [-(rdn_translate(nn5, rdn_neg(rdnn(n5))))], (500 ^ _343593) ^ [] : [-(rdn_translate(nn21, rdn_neg(rdn(rdnn(n1), rdnn(n2)))))], (514 ^ _343593) ^ [] : [-(rdn_translate(nn28, rdn_neg(rdn(rdnn(n8), rdnn(n2)))))], (550 ^ _343593) ^ [] : [-(rdn_translate(nn46, rdn_neg(rdn(rdnn(n6), rdnn(n4)))))], (590 ^ _343593) ^ [] : [-(rdn_translate(nn66, rdn_neg(rdn(rdnn(n6), rdnn(n6)))))], (688 ^ _343593) ^ [] : [-(rdn_translate(nn115, rdn_neg(rdn(rdnn(n5), rdn(rdnn(n1), rdnn(n1))))))], (724 ^ _343593) ^ [] : [-(rdn_non_zero_digit(rdnn(n5)))], (1190 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n3), rdnn(n9), rdnn(n2), rdnn(n1)))], (1262 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n7), rdnn(n5), rdnn(n2), rdnn(n1)))], (104 ^ _343593) ^ [_347041, _347043] : [-(rdn_non_zero(_347041)), _347043 = _347041, rdn_non_zero(_347043)], (274 ^ _343593) ^ [] : [-(rdn_translate(n35, rdn_pos(rdn(rdnn(n5), rdnn(n3)))))], (424 ^ _343593) ^ [] : [-(rdn_translate(n110, rdn_pos(rdn(rdnn(n0), rdn(rdnn(n1), rdnn(n1))))))], (578 ^ _343593) ^ [] : [-(rdn_translate(nn60, rdn_neg(rdn(rdnn(n0), rdnn(n6)))))], (614 ^ _343593) ^ [] : [-(rdn_translate(nn78, rdn_neg(rdn(rdnn(n8), rdnn(n7)))))], (694 ^ _343593) ^ [] : [-(rdn_translate(nn118, rdn_neg(rdn(rdnn(n8), rdn(rdnn(n1), rdnn(n1))))))], (796 ^ _343593) ^ [_367234, _367236, _367238, _367240] : [-(less(_367240, _367238)), rdn_translate(_367240, rdn_pos(_367236)), rdn_translate(_367238, rdn_pos(_367234)), rdn_positive_less(_367236, _367234)], (1126 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n0), rdnn(n7), rdnn(n7), rdnn(n0)))], (1174 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n3), rdnn(n1), rdnn(n4), rdnn(n0)))], (1276 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n8), rdnn(n2), rdnn(n0), rdnn(n1)))], (72 ^ _343593) ^ [_346016, _346018, _346020, _346022] : [-(rdn_translate(_346020, _346016)), rdn_translate(_346022, _346018), _346022 = _346020, _346018 = _346016], (296 ^ _343593) ^ [] : [-(rdn_translate(n46, rdn_pos(rdn(rdnn(n6), rdnn(n4)))))], (304 ^ _343593) ^ [] : [-(rdn_translate(n50, rdn_pos(rdn(rdnn(n0), rdnn(n5)))))], (342 ^ _343593) ^ [] : [-(rdn_translate(n69, rdn_pos(rdn(rdnn(n9), rdnn(n6)))))], (402 ^ _343593) ^ [] : [-(rdn_translate(n99, rdn_pos(rdn(rdnn(n9), rdnn(n9)))))], (508 ^ _343593) ^ [] : [-(rdn_translate(nn25, rdn_neg(rdn(rdnn(n5), rdnn(n2)))))], (524 ^ _343593) ^ [] : [-(rdn_translate(nn33, rdn_neg(rdn(rdnn(n3), rdnn(n3)))))], (566 ^ _343593) ^ [] : [-(rdn_translate(nn54, rdn_neg(rdn(rdnn(n4), rdnn(n5)))))], (994 ^ _343593) ^ [_373870, _373872, _373874, _373876] : [-(_373876 = _373874), sum(_373876, _373872, _373870), sum(_373874, _373872, _373870)], (1220 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n5), rdnn(n4), rdnn(n9), rdnn(n0)))], (10 ^ _343593) ^ [_344048, _344050, _344052] : [-(_344052 = _344048), _344052 = _344050, _344050 = _344048], (204 ^ _343593) ^ [] : [-(rdn_translate(n0, rdn_pos(rdnn(n0))))], (222 ^ _343593) ^ [] : [-(rdn_translate(n9, rdn_pos(rdnn(n9))))], (238 ^ _343593) ^ [] : [-(rdn_translate(n17, rdn_pos(rdn(rdnn(n7), rdnn(n1)))))], (276 ^ _343593) ^ [] : [-(rdn_translate(n36, rdn_pos(rdn(rdnn(n6), rdnn(n3)))))], (298 ^ _343593) ^ [] : [-(rdn_translate(n47, rdn_pos(rdn(rdnn(n7), rdnn(n4)))))], (430 ^ _343593) ^ [] : [-(rdn_translate(n113, rdn_pos(rdn(rdnn(n3), rdn(rdnn(n1), rdnn(n1))))))], (484 ^ _343593) ^ [] : [-(rdn_translate(nn13, rdn_neg(rdn(rdnn(n3), rdnn(n1)))))], (600 ^ _343593) ^ [] : [-(rdn_translate(nn71, rdn_neg(rdn(rdnn(n1), rdnn(n7)))))], (616 ^ _343593) ^ [] : [-(rdn_translate(nn79, rdn_neg(rdn(rdnn(n9), rdnn(n7)))))], (650 ^ _343593) ^ [] : [-(rdn_translate(nn96, rdn_neg(rdn(rdnn(n6), rdnn(n9)))))], (662 ^ _343593) ^ [] : [-(rdn_translate(nn102, rdn_neg(rdn(rdnn(n2), rdn(rdnn(n0), rdnn(n1))))))], (938 ^ _343593) ^ [_372002, _372004, _372006, _372008, _372010, _372012] : [-(sum(_372012, _372010, _372008)), rdn_translate(_372012, rdn_pos(_372006)), rdn_translate(_372010, rdn_neg(_372004)), rdn_positive_less(_372004, _372006), rdn_add_with_carry(rdnn(n0), _372004, _372002, _372006), rdn_translate(_372008, rdn_pos(_372002))], (1118 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n0), rdnn(n3), rdnn(n3), rdnn(n0)))], (1244 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n6), rdnn(n6), rdnn(n2), rdnn(n1)))], (310 ^ _343593) ^ [] : [-(rdn_translate(n53, rdn_pos(rdn(rdnn(n3), rdnn(n5)))))], (324 ^ _343593) ^ [] : [-(rdn_translate(n60, rdn_pos(rdn(rdnn(n0), rdnn(n6)))))], (520 ^ _343593) ^ [] : [-(rdn_translate(nn31, rdn_neg(rdn(rdnn(n1), rdnn(n3)))))], (594 ^ _343593) ^ [] : [-(rdn_translate(nn68, rdn_neg(rdn(rdnn(n8), rdnn(n6)))))], (762 ^ _343593) ^ [_365963, _365965, _365967, _365969] : [rdn_positive_less(_365967, _365963), -(rdn_positive_less(rdn(rdnn(_365969), _365967), rdn(rdnn(_365965), _365963)))], (880 ^ _343593) ^ [_370028, _370030, _370032, _370034, _370036, _370038] : [-(sum(_370038, _370036, _370034)), rdn_translate(_370038, rdn_pos(_370032)), rdn_translate(_370036, rdn_pos(_370030)), rdn_add_with_carry(rdnn(n0), _370032, _370030, _370028), rdn_translate(_370034, rdn_pos(_370028))], (1160 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n2), rdnn(n4), rdnn(n6), rdnn(n0)))], (1204 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n4), rdnn(n6), rdnn(n0), rdnn(n1)))], (1274 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n8), rdnn(n1), rdnn(n9), rdnn(n0)))], (1294 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n9), rdnn(n1), rdnn(n0), rdnn(n1)))], (210 ^ _343593) ^ [] : [-(rdn_translate(n3, rdn_pos(rdnn(n3))))], (266 ^ _343593) ^ [] : [-(rdn_translate(n31, rdn_pos(rdn(rdnn(n1), rdnn(n3)))))], (340 ^ _343593) ^ [] : [-(rdn_translate(n68, rdn_pos(rdn(rdnn(n8), rdnn(n6)))))], (408 ^ _343593) ^ [] : [-(rdn_translate(n102, rdn_pos(rdn(rdnn(n2), rdn(rdnn(n0), rdnn(n1))))))], (412 ^ _343593) ^ [] : [-(rdn_translate(n104, rdn_pos(rdn(rdnn(n4), rdn(rdnn(n0), rdnn(n1))))))], (586 ^ _343593) ^ [] : [-(rdn_translate(nn64, rdn_neg(rdn(rdnn(n4), rdnn(n6)))))], (642 ^ _343593) ^ [] : [-(rdn_translate(nn92, rdn_neg(rdn(rdnn(n2), rdnn(n9)))))], (684 ^ _343593) ^ [] : [-(rdn_translate(nn113, rdn_neg(rdn(rdnn(n3), rdn(rdnn(n1), rdnn(n1))))))], (702 ^ _343593) ^ [] : [-(rdn_translate(nn122, rdn_neg(rdn(rdnn(n2), rdn(rdnn(n2), rdnn(n1))))))], (718 ^ _343593) ^ [] : [-(rdn_non_zero_digit(rdnn(n2)))], (820 ^ _343593) ^ [_368041, _368043, _368045, _368047] : [-(less(_368047, _368045)), rdn_translate(_368047, rdn_neg(_368043)), rdn_translate(_368045, rdn_neg(_368041)), rdn_positive_less(_368041, _368043)], (898 ^ _343593) ^ [_370651, _370653, _370655, _370657, _370659, _370661] : [-(sum(_370661, _370659, _370657)), rdn_translate(_370661, rdn_neg(_370655)), rdn_translate(_370659, rdn_neg(_370653)), rdn_add_with_carry(rdnn(n0), _370655, _370653, _370651), rdn_translate(_370657, rdn_neg(_370651))], (1020 ^ _343593) ^ [_374759, _374761, _374763] : [difference(_374763, _374761, _374759), -(sum(_374761, _374759, _374763))], (1142 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n1), rdnn(n5), rdnn(n6), rdnn(n0)))], (1158 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n2), rdnn(n3), rdnn(n5), rdnn(n0)))], (1282 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n8), rdnn(n5), rdnn(n3), rdnn(n1)))], (312 ^ _343593) ^ [] : [-(rdn_translate(n54, rdn_pos(rdn(rdnn(n4), rdnn(n5)))))], (350 ^ _343593) ^ [] : [-(rdn_translate(n73, rdn_pos(rdn(rdnn(n3), rdnn(n7)))))], (394 ^ _343593) ^ [] : [-(rdn_translate(n95, rdn_pos(rdn(rdnn(n5), rdnn(n9)))))], (452 ^ _343593) ^ [] : [-(rdn_translate(n124, rdn_pos(rdn(rdnn(n4), rdn(rdnn(n2), rdnn(n1))))))], (592 ^ _343593) ^ [] : [-(rdn_translate(nn67, rdn_neg(rdn(rdnn(n7), rdnn(n6)))))], (640 ^ _343593) ^ [] : [-(rdn_translate(nn91, rdn_neg(rdn(rdnn(n1), rdnn(n9)))))], (700 ^ _343593) ^ [] : [-(rdn_translate(nn121, rdn_neg(rdn(rdnn(n1), rdn(rdnn(n2), rdnn(n1))))))], (722 ^ _343593) ^ [] : [-(rdn_non_zero_digit(rdnn(n4)))], (970 ^ _343593) ^ [_373049, _373051, _373053, _373055, _373057] : [-(sum(_373057, _373055, _373053)), rdn_translate(_373057, rdn_neg(_373051)), rdn_translate(_373055, rdn_pos(_373049)), sum(_373055, _373057, _373053)], (1130 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n0), rdnn(n9), rdnn(n9), rdnn(n0)))], (1150 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n1), rdnn(n9), rdnn(n0), rdnn(n1)))], (1212 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n5), rdnn(n0), rdnn(n5), rdnn(n0)))], (1228 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n5), rdnn(n8), rdnn(n3), rdnn(n1)))], (1278 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n8), rdnn(n3), rdnn(n1), rdnn(n1)))], (1284 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n8), rdnn(n6), rdnn(n4), rdnn(n1)))], (216 ^ _343593) ^ [] : [-(rdn_translate(n6, rdn_pos(rdnn(n6))))], (258 ^ _343593) ^ [] : [-(rdn_translate(n27, rdn_pos(rdn(rdnn(n7), rdnn(n2)))))], (396 ^ _343593) ^ [] : [-(rdn_translate(n96, rdn_pos(rdn(rdnn(n6), rdnn(n9)))))], (414 ^ _343593) ^ [] : [-(rdn_translate(n105, rdn_pos(rdn(rdnn(n5), rdn(rdnn(n0), rdnn(n1))))))], (436 ^ _343593) ^ [] : [-(rdn_translate(n116, rdn_pos(rdn(rdnn(n6), rdn(rdnn(n1), rdnn(n1))))))], (444 ^ _343593) ^ [] : [-(rdn_translate(n120, rdn_pos(rdn(rdnn(n0), rdn(rdnn(n2), rdnn(n1))))))], (492 ^ _343593) ^ [] : [-(rdn_translate(nn17, rdn_neg(rdn(rdnn(n7), rdnn(n1)))))], (540 ^ _343593) ^ [] : [-(rdn_translate(nn41, rdn_neg(rdn(rdnn(n1), rdnn(n4)))))], (670 ^ _343593) ^ [] : [-(rdn_translate(nn106, rdn_neg(rdn(rdnn(n6), rdn(rdnn(n0), rdnn(n1))))))], (1268 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n7), rdnn(n8), rdnn(n5), rdnn(n1)))], (1304 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n9), rdnn(n6), rdnn(n5), rdnn(n1)))], (336 ^ _343593) ^ [] : [-(rdn_translate(n66, rdn_pos(rdn(rdnn(n6), rdnn(n6)))))], (380 ^ _343593) ^ [] : [-(rdn_translate(n88, rdn_pos(rdn(rdnn(n8), rdnn(n8)))))], (496 ^ _343593) ^ [] : [-(rdn_translate(nn19, rdn_neg(rdn(rdnn(n9), rdnn(n1)))))], (522 ^ _343593) ^ [] : [-(rdn_translate(nn32, rdn_neg(rdn(rdnn(n2), rdnn(n3)))))], (560 ^ _343593) ^ [] : [-(rdn_translate(nn51, rdn_neg(rdn(rdnn(n1), rdnn(n5)))))], (628 ^ _343593) ^ [] : [-(rdn_translate(nn85, rdn_neg(rdn(rdnn(n5), rdnn(n8)))))], (984 ^ _343593) ^ [_373519, _373521, _373523, _373525] : [-(_373521 = _373519), sum(_373525, _373523, _373521), sum(_373525, _373523, _373519)], (1152 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n2), rdnn(n0), rdnn(n2), rdnn(n0)))], (1208 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n4), rdnn(n8), rdnn(n2), rdnn(n1)))], (1266 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n7), rdnn(n7), rdnn(n4), rdnn(n1)))], (182 ^ _343593) ^ [_349747, _349749] : [_349749 = _349747, -(rdn_pos(_349749) = rdn_pos(_349747))], (230 ^ _343593) ^ [] : [-(rdn_translate(n13, rdn_pos(rdn(rdnn(n3), rdnn(n1)))))], (242 ^ _343593) ^ [] : [-(rdn_translate(n19, rdn_pos(rdn(rdnn(n9), rdnn(n1)))))], (306 ^ _343593) ^ [] : [-(rdn_translate(n51, rdn_pos(rdn(rdnn(n1), rdnn(n5)))))], (352 ^ _343593) ^ [] : [-(rdn_translate(n74, rdn_pos(rdn(rdnn(n4), rdnn(n7)))))], (404 ^ _343593) ^ [] : [-(rdn_translate(n100, rdn_pos(rdn(rdnn(n0), rdn(rdnn(n0), rdnn(n1))))))], (438 ^ _343593) ^ [] : [-(rdn_translate(n117, rdn_pos(rdn(rdnn(n7), rdn(rdnn(n1), rdnn(n1))))))], (454 ^ _343593) ^ [] : [-(rdn_translate(n125, rdn_pos(rdn(rdnn(n5), rdn(rdnn(n2), rdnn(n1))))))], (526 ^ _343593) ^ [] : [-(rdn_translate(nn34, rdn_neg(rdn(rdnn(n4), rdnn(n3)))))], (528 ^ _343593) ^ [] : [-(rdn_translate(nn35, rdn_neg(rdn(rdnn(n5), rdnn(n3)))))], (556 ^ _343593) ^ [] : [-(rdn_translate(nn49, rdn_neg(rdn(rdnn(n9), rdnn(n4)))))], (620 ^ _343593) ^ [] : [-(rdn_translate(nn81, rdn_neg(rdn(rdnn(n1), rdnn(n8)))))], (644 ^ _343593) ^ [] : [-(rdn_translate(nn93, rdn_neg(rdn(rdnn(n3), rdnn(n9)))))], (960 ^ _343593) ^ [_372688, _372690, _372692] : [-(sum(_372692, _372690, n0)), rdn_translate(_372692, rdn_pos(_372688)), rdn_translate(_372690, rdn_neg(_372688))], (1250 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n6), rdnn(n9), rdnn(n5), rdnn(n1)))], (1300 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n9), rdnn(n4), rdnn(n3), rdnn(n1)))], (256 ^ _343593) ^ [] : [-(rdn_translate(n26, rdn_pos(rdn(rdnn(n6), rdnn(n2)))))], (272 ^ _343593) ^ [] : [-(rdn_translate(n34, rdn_pos(rdn(rdnn(n4), rdnn(n3)))))], (320 ^ _343593) ^ [] : [-(rdn_translate(n58, rdn_pos(rdn(rdnn(n8), rdnn(n5)))))], (332 ^ _343593) ^ [] : [-(rdn_translate(n64, rdn_pos(rdn(rdnn(n4), rdnn(n6)))))], (426 ^ _343593) ^ [] : [-(rdn_translate(n111, rdn_pos(rdn(rdnn(n1), rdn(rdnn(n1), rdnn(n1))))))], (464 ^ _343593) ^ [] : [-(rdn_translate(nn3, rdn_neg(rdnn(n3))))], (574 ^ _343593) ^ [] : [-(rdn_translate(nn58, rdn_neg(rdn(rdnn(n8), rdnn(n5)))))], (598 ^ _343593) ^ [] : [-(rdn_translate(nn70, rdn_neg(rdn(rdnn(n0), rdnn(n7)))))], (648 ^ _343593) ^ [] : [-(rdn_translate(nn95, rdn_neg(rdn(rdnn(n5), rdnn(n9)))))], (712 ^ _343593) ^ [] : [-(rdn_translate(nn127, rdn_neg(rdn(rdnn(n7), rdn(rdnn(n2), rdnn(n1))))))], (730 ^ _343593) ^ [] : [-(rdn_non_zero_digit(rdnn(n8)))], (834 ^ _343593) ^ [_368494, _368496] : [less(_368496, _368494), 837 ^ _343593 : [(838 ^ _343593) ^ [] : [less(_368494, _368496)], (840 ^ _343593) ^ [] : [_368494 = _368496]]], (916 ^ _343593) ^ [_371274, _371276, _371278, _371280, _371282, _371284] : [-(sum(_371284, _371282, _371280)), rdn_translate(_371284, rdn_pos(_371278)), rdn_translate(_371282, rdn_neg(_371276)), rdn_positive_less(_371278, _371276), rdn_add_with_carry(rdnn(n0), _371278, _371274, _371276), rdn_translate(_371280, rdn_neg(_371274))], (1192 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n4), rdnn(n0), rdnn(n4), rdnn(n0)))], (1248 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n6), rdnn(n8), rdnn(n4), rdnn(n1)))], (1312 ^ _343593) ^ [_385206, _385208] : [sum(_385208, _385206, n8), _385208 = n4, _385206 = n4], (44 ^ _343593) ^ [_345128, _345130, _345132, _345134] : [-(less_or_equal(_345132, _345128)), less_or_equal(_345134, _345130), _345134 = _345132, _345130 = _345128], (254 ^ _343593) ^ [] : [-(rdn_translate(n25, rdn_pos(rdn(rdnn(n5), rdnn(n2)))))], (356 ^ _343593) ^ [] : [-(rdn_translate(n76, rdn_pos(rdn(rdnn(n6), rdnn(n7)))))], (494 ^ _343593) ^ [] : [-(rdn_translate(nn18, rdn_neg(rdn(rdnn(n8), rdnn(n1)))))], (564 ^ _343593) ^ [] : [-(rdn_translate(nn53, rdn_neg(rdn(rdnn(n3), rdnn(n5)))))], (1124 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n0), rdnn(n6), rdnn(n6), rdnn(n0)))], (1210 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n4), rdnn(n9), rdnn(n3), rdnn(n1)))], (1256 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n7), rdnn(n2), rdnn(n9), rdnn(n0)))], (176 ^ _343593) ^ [_349529, _349531] : [_349531 = _349529, -(rdn_neg(_349531) = rdn_neg(_349529))], (136 ^ _343593) ^ [_348210, _348212, _348214, _348216, _348218, _348220, _348222, _348224] : [-(rdn_digit_add(_348222, _348218, _348214, _348210)), rdn_digit_add(_348224, _348220, _348216, _348212), _348224 = _348222, _348220 = _348218, _348216 = _348214, _348212 = _348210], (288 ^ _343593) ^ [] : [-(rdn_translate(n42, rdn_pos(rdn(rdnn(n2), rdnn(n4)))))], (338 ^ _343593) ^ [] : [-(rdn_translate(n67, rdn_pos(rdn(rdnn(n7), rdnn(n6)))))], (448 ^ _343593) ^ [] : [-(rdn_translate(n122, rdn_pos(rdn(rdnn(n2), rdn(rdnn(n2), rdnn(n1))))))], (504 ^ _343593) ^ [] : [-(rdn_translate(nn23, rdn_neg(rdn(rdnn(n3), rdnn(n2)))))], (626 ^ _343593) ^ [] : [-(rdn_translate(nn84, rdn_neg(rdn(rdnn(n4), rdnn(n8)))))], (646 ^ _343593) ^ [] : [-(rdn_translate(nn94, rdn_neg(rdn(rdnn(n4), rdnn(n9)))))], (744 ^ _343593) ^ [] : [-(rdn_positive_less(rdnn(n5), rdnn(n6)))], (1014 ^ _343593) ^ [_374587, _374589, _374591] : [sum(_374589, _374587, _374591), -(difference(_374591, _374589, _374587))], (1182 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n3), rdnn(n5), rdnn(n8), rdnn(n0)))], (1200 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n4), rdnn(n4), rdnn(n8), rdnn(n0)))], (1218 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n5), rdnn(n3), rdnn(n8), rdnn(n0)))], (236 ^ _343593) ^ [] : [-(rdn_translate(n16, rdn_pos(rdn(rdnn(n6), rdnn(n1)))))], (334 ^ _343593) ^ [] : [-(rdn_translate(n65, rdn_pos(rdn(rdnn(n5), rdnn(n6)))))], (422 ^ _343593) ^ [] : [-(rdn_translate(n109, rdn_pos(rdn(rdnn(n9), rdn(rdnn(n0), rdnn(n1))))))], (470 ^ _343593) ^ [] : [-(rdn_translate(nn6, rdn_neg(rdnn(n6))))], (546 ^ _343593) ^ [] : [-(rdn_translate(nn44, rdn_neg(rdn(rdnn(n4), rdnn(n4)))))], (630 ^ _343593) ^ [] : [-(rdn_translate(nn86, rdn_neg(rdn(rdnn(n6), rdnn(n8)))))], (660 ^ _343593) ^ [] : [-(rdn_translate(nn101, rdn_neg(rdn(rdnn(n1), rdn(rdnn(n0), rdnn(n1))))))], (680 ^ _343593) ^ [] : [-(rdn_translate(nn111, rdn_neg(rdn(rdnn(n1), rdn(rdnn(n1), rdnn(n1))))))], (706 ^ _343593) ^ [] : [-(rdn_translate(nn124, rdn_neg(rdn(rdnn(n4), rdn(rdnn(n2), rdnn(n1))))))], (748 ^ _343593) ^ [] : [-(rdn_positive_less(rdnn(n7), rdnn(n8)))], (752 ^ _343593) ^ [_365602, _365604, _365606] : [-(rdn_positive_less(rdnn(_365606), rdnn(_365602))), rdn_positive_less(rdnn(_365606), rdnn(_365604)), rdn_positive_less(rdnn(_365604), rdnn(_365602))], (1154 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n2), rdnn(n1), rdnn(n3), rdnn(n0)))], (1166 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n2), rdnn(n7), rdnn(n9), rdnn(n0)))], (1230 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n5), rdnn(n9), rdnn(n4), rdnn(n1)))], (1232 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n6), rdnn(n0), rdnn(n6), rdnn(n0)))], (1076 ^ _343593) ^ [_377203, _377205, _377207, _377209, _377211, _377213, _377215, _377217, _377219, _377221, _377223] : [-(rdn_add_with_carry(rdnn(_377223), rdn(rdnn(_377221), _377219), rdn(rdnn(_377217), _377215), rdn(rdnn(_377213), _377211))), rdn_digit_add(rdnn(_377221), rdnn(_377217), rdnn(_377209), rdnn(_377207)), rdn_digit_add(rdnn(_377209), rdnn(_377223), rdnn(_377213), rdnn(_377205)), rdn_digit_add(rdnn(_377207), rdnn(_377205), rdnn(_377203), rdnn(n0)), rdn_add_with_carry(rdnn(_377203), _377219, _377215, _377211), rdn_non_zero(_377219), rdn_non_zero(_377215), rdn_non_zero(_377211)], (198 ^ _343593) ^ [_350304, _350306] : [_350306 = _350304, -(rdnn(_350306) = rdnn(_350304))], (286 ^ _343593) ^ [] : [-(rdn_translate(n41, rdn_pos(rdn(rdnn(n1), rdnn(n4)))))], (330 ^ _343593) ^ [] : [-(rdn_translate(n63, rdn_pos(rdn(rdnn(n3), rdnn(n6)))))], (370 ^ _343593) ^ [] : [-(rdn_translate(n83, rdn_pos(rdn(rdnn(n3), rdnn(n8)))))], (434 ^ _343593) ^ [] : [-(rdn_translate(n115, rdn_pos(rdn(rdnn(n5), rdn(rdnn(n1), rdnn(n1))))))], (488 ^ _343593) ^ [] : [-(rdn_translate(nn15, rdn_neg(rdn(rdnn(n5), rdnn(n1)))))], (544 ^ _343593) ^ [] : [-(rdn_translate(nn43, rdn_neg(rdn(rdnn(n3), rdnn(n4)))))], (606 ^ _343593) ^ [] : [-(rdn_translate(nn74, rdn_neg(rdn(rdnn(n4), rdnn(n7)))))], (672 ^ _343593) ^ [] : [-(rdn_translate(nn107, rdn_neg(rdn(rdnn(n7), rdn(rdnn(n0), rdnn(n1))))))], (678 ^ _343593) ^ [] : [-(rdn_translate(nn110, rdn_neg(rdn(rdnn(n0), rdn(rdnn(n1), rdnn(n1))))))], (704 ^ _343593) ^ [] : [-(rdn_translate(nn123, rdn_neg(rdn(rdnn(n3), rdn(rdnn(n2), rdnn(n1))))))], (742 ^ _343593) ^ [] : [-(rdn_positive_less(rdnn(n4), rdnn(n5)))], (1026 ^ _343593) ^ [_375023, _375025, _375027, _375029, _375031] : [-(rdn_add_with_carry(rdnn(_375031), rdnn(_375029), rdnn(_375027), rdnn(_375025))), rdn_digit_add(rdnn(_375029), rdnn(_375027), rdnn(_375023), rdnn(n0)), rdn_digit_add(rdnn(_375023), rdnn(_375031), rdnn(_375025), rdnn(n0))], (1132 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n1), rdnn(n0), rdnn(n1), rdnn(n0)))], (1242 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n6), rdnn(n5), rdnn(n1), rdnn(n1)))], (158 ^ _343593) ^ [_348952, _348954, _348956, _348958, _348960, _348962] : [-(sum(_348960, _348956, _348952)), sum(_348962, _348958, _348954), _348962 = _348960, _348958 = _348956, _348954 = _348952], (262 ^ _343593) ^ [] : [-(rdn_translate(n29, rdn_pos(rdn(rdnn(n9), rdnn(n2)))))], (386 ^ _343593) ^ [] : [-(rdn_translate(n91, rdn_pos(rdn(rdnn(n1), rdnn(n9)))))], (552 ^ _343593) ^ [] : [-(rdn_translate(nn47, rdn_neg(rdn(rdnn(n7), rdnn(n4)))))], (654 ^ _343593) ^ [] : [-(rdn_translate(nn98, rdn_neg(rdn(rdnn(n8), rdnn(n9)))))], (676 ^ _343593) ^ [] : [-(rdn_translate(nn109, rdn_neg(rdn(rdnn(n9), rdn(rdnn(n0), rdnn(n1))))))], (1134 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n1), rdnn(n1), rdnn(n2), rdnn(n0)))], (1188 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n3), rdnn(n8), rdnn(n1), rdnn(n1)))], (1252 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n7), rdnn(n0), rdnn(n7), rdnn(n0)))], (1106 ^ _343593) ^ [_378369, _378371, _378373, _378375, _378377, _378379] : [rdn_add_with_carry(rdnn(_378379), rdnn(_378373), rdn(rdnn(_378377), _378375), rdn(rdnn(_378371), _378369)), -(rdn_add_with_carry(rdnn(_378379), rdn(rdnn(_378377), _378375), rdnn(_378373), rdn(rdnn(_378371), _378369)))], (226 ^ _343593) ^ [] : [-(rdn_translate(n11, rdn_pos(rdn(rdnn(n1), rdnn(n1)))))], (308 ^ _343593) ^ [] : [-(rdn_translate(n52, rdn_pos(rdn(rdnn(n2), rdnn(n5)))))], (398 ^ _343593) ^ [] : [-(rdn_translate(n97, rdn_pos(rdn(rdnn(n7), rdnn(n9)))))], (418 ^ _343593) ^ [] : [-(rdn_translate(n107, rdn_pos(rdn(rdnn(n7), rdn(rdnn(n0), rdnn(n1))))))], (482 ^ _343593) ^ [] : [-(rdn_translate(nn12, rdn_neg(rdn(rdnn(n2), rdnn(n1)))))], (532 ^ _343593) ^ [] : [-(rdn_translate(nn37, rdn_neg(rdn(rdnn(n7), rdnn(n3)))))], (584 ^ _343593) ^ [] : [-(rdn_translate(nn63, rdn_neg(rdn(rdnn(n3), rdnn(n6)))))], (602 ^ _343593) ^ [] : [-(rdn_translate(nn72, rdn_neg(rdn(rdnn(n2), rdnn(n7)))))], (652 ^ _343593) ^ [] : [-(rdn_translate(nn97, rdn_neg(rdn(rdnn(n7), rdnn(n9)))))], (1234 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n6), rdnn(n1), rdnn(n7), rdnn(n0)))], (1298 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n9), rdnn(n3), rdnn(n2), rdnn(n1)))], (260 ^ _343593) ^ [] : [-(rdn_translate(n28, rdn_pos(rdn(rdnn(n8), rdnn(n2)))))], (284 ^ _343593) ^ [] : [-(rdn_translate(n40, rdn_pos(rdn(rdnn(n0), rdnn(n4)))))], (292 ^ _343593) ^ [] : [-(rdn_translate(n44, rdn_pos(rdn(rdnn(n4), rdnn(n4)))))], (348 ^ _343593) ^ [] : [-(rdn_translate(n72, rdn_pos(rdn(rdnn(n2), rdnn(n7)))))], (368 ^ _343593) ^ [] : [-(rdn_translate(n82, rdn_pos(rdn(rdnn(n2), rdnn(n8)))))], (400 ^ _343593) ^ [] : [-(rdn_translate(n98, rdn_pos(rdn(rdnn(n8), rdnn(n9)))))], (450 ^ _343593) ^ [] : [-(rdn_translate(n123, rdn_pos(rdn(rdnn(n3), rdn(rdnn(n2), rdnn(n1))))))], (462 ^ _343593) ^ [] : [-(rdn_translate(nn2, rdn_neg(rdnn(n2))))], (476 ^ _343593) ^ [] : [-(rdn_translate(nn9, rdn_neg(rdnn(n9))))], (636 ^ _343593) ^ [] : [-(rdn_translate(nn89, rdn_neg(rdn(rdnn(n9), rdnn(n8)))))], (666 ^ _343593) ^ [] : [-(rdn_translate(nn104, rdn_neg(rdn(rdnn(n4), rdn(rdnn(n0), rdnn(n1))))))], (734 ^ _343593) ^ [] : [-(rdn_positive_less(rdnn(n0), rdnn(n1)))], (740 ^ _343593) ^ [] : [-(rdn_positive_less(rdnn(n3), rdnn(n4)))], (1112 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n0), rdnn(n0), rdnn(n0), rdnn(n0)))], (1116 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n0), rdnn(n2), rdnn(n2), rdnn(n0)))], (1202 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n4), rdnn(n5), rdnn(n9), rdnn(n0)))], (1290 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n8), rdnn(n9), rdnn(n7), rdnn(n1)))], (206 ^ _343593) ^ [] : [-(rdn_translate(n1, rdn_pos(rdnn(n1))))], (268 ^ _343593) ^ [] : [-(rdn_translate(n32, rdn_pos(rdn(rdnn(n2), rdnn(n3)))))], (278 ^ _343593) ^ [] : [-(rdn_translate(n37, rdn_pos(rdn(rdnn(n7), rdnn(n3)))))], (300 ^ _343593) ^ [] : [-(rdn_translate(n48, rdn_pos(rdn(rdnn(n8), rdnn(n4)))))], (322 ^ _343593) ^ [] : [-(rdn_translate(n59, rdn_pos(rdn(rdnn(n9), rdnn(n5)))))], (360 ^ _343593) ^ [] : [-(rdn_translate(n78, rdn_pos(rdn(rdnn(n8), rdnn(n7)))))], (376 ^ _343593) ^ [] : [-(rdn_translate(n86, rdn_pos(rdn(rdnn(n6), rdnn(n8)))))], (428 ^ _343593) ^ [] : [-(rdn_translate(n112, rdn_pos(rdn(rdnn(n2), rdn(rdnn(n1), rdnn(n1))))))], (510 ^ _343593) ^ [] : [-(rdn_translate(nn26, rdn_neg(rdn(rdnn(n6), rdnn(n2)))))], (580 ^ _343593) ^ [] : [-(rdn_translate(nn61, rdn_neg(rdn(rdnn(n1), rdnn(n6)))))], (618 ^ _343593) ^ [] : [-(rdn_translate(nn80, rdn_neg(rdn(rdnn(n0), rdnn(n8)))))], (750 ^ _343593) ^ [] : [-(rdn_positive_less(rdnn(n8), rdnn(n9)))], (1138 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n1), rdnn(n3), rdnn(n4), rdnn(n0)))], (1258 ^ _343593) ^ [] : [-(rdn_digit_add(rdnn(n7), rdnn(n3), rdnn(n0), rdnn(n1)))]], input).
% 278.10/269.27 ncf('1',plain,[sum(n4, n4, n8), n4 = n4, n4 = n4],start(1312 ^ 0,bind([[_385206, _385208], [n4, n4]]))).
% 278.10/269.27 ncf('1.1',plain,[-(sum(n4, n4, n8)), rdn_translate(n4, rdn_pos(rdnn(n4))), rdn_translate(n4, rdn_pos(rdnn(n4))), rdn_add_with_carry(rdnn(n0), rdnn(n4), rdnn(n4), rdnn(n8)), rdn_translate(n8, rdn_pos(rdnn(n8)))],extension(880 ^ 1,bind([[_370028, _370030, _370032, _370034, _370036, _370038], [rdnn(n8), rdnn(n4), rdnn(n4), n8, n4, n4]]))).
% 278.10/269.27 ncf('1.1.1',plain,[-(rdn_translate(n4, rdn_pos(rdnn(n4))))],extension(212 ^ 2)).
% 278.10/269.27 ncf('1.1.2',plain,[-(rdn_translate(n4, rdn_pos(rdnn(n4))))],extension(212 ^ 2)).
% 278.10/269.27 ncf('1.1.3',plain,[-(rdn_add_with_carry(rdnn(n0), rdnn(n4), rdnn(n4), rdnn(n8))), rdn_digit_add(rdnn(n4), rdnn(n4), rdnn(n8), rdnn(n0)), rdn_digit_add(rdnn(n8), rdnn(n0), rdnn(n8), rdnn(n0))],extension(1026 ^ 2,bind([[_375023, _375025, _375027, _375029, _375031], [n8, n8, n4, n4, n0]]))).
% 278.10/269.27 ncf('1.1.3.1',plain,[-(rdn_digit_add(rdnn(n4), rdnn(n4), rdnn(n8), rdnn(n0)))],extension(1200 ^ 3)).
% 278.10/269.27 ncf('1.1.3.2',plain,[-(rdn_digit_add(rdnn(n8), rdnn(n0), rdnn(n8), rdnn(n0)))],extension(1272 ^ 3)).
% 278.10/269.27 ncf('1.1.4',plain,[-(rdn_translate(n8, rdn_pos(rdnn(n8))))],extension(220 ^ 2)).
% 278.10/269.27 ncf('1.2',plain,[-(n4 = n4), -(less(n4, n4)), -(less(n4, n4))],extension(842 ^ 1,bind([[_368733, _368735], [n4, n4]]))).
% 278.10/269.27 ncf('1.2.1',plain,[less(n4, n4), 838 : less(n4, n4)],extension(834 ^ 2,bind([[_368494, _368496], [n4, n4]]))).
% 278.10/269.27 ncf('1.2.1.1',plain,[-(less(n4, n4))],reduction('1.2')).
% 278.10/269.27 ncf('1.2.2',plain,[less(n4, n4)],lemmata('[1].x')).
% 278.10/269.27 ncf('1.3',plain,[-(n4 = n4)],lemmata('x')).
% 278.10/269.27 %-----------------------------------------------------
% 278.10/269.27 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------