%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM924+2 : TPTP v8.1.2. Released v5.3.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:45:55 EDT 2023
% Result : Theorem 101.32s 98.59s
% Output : Proof 101.32s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : NUM924+2 : TPTP v8.1.2. Released v5.3.0.
% 0.07/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n028.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 18:00:18 EDT 2023
% 0.12/0.33 % CPUTime :
% 101.32/98.59
% 101.32/98.59 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 101.32/98.59 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 101.32/98.59 %-----------------------------------------------------
% 101.32/98.59 ncf(matrix, plain, [(5784 ^ _614856) ^ [] : [ord_less_int(plus_plus_int(power_power_int(s, number_number_of_nat(bit0(bit1(pls)))), one_one_int), zero_zero_int)], (208 ^ _614856) ^ [_621570, _621572] : [_621572 = _621570, -(undefined_int(_621572) = undefined_int(_621570))], (214 ^ _614856) ^ [_621816, _621818, _621820, _621822] : [-(legendre(_621822, _621818) = legendre(_621820, _621816)), _621822 = _621820, _621818 = _621816], (224 ^ _614856) ^ [_622147, _622149] : [_622149 = _622147, -(number_number_of_int(_622149) = number_number_of_int(_622147))], (230 ^ _614856) ^ [_622393, _622395, _622397, _622399] : [-(plus_plus_real(_622399, _622395) = plus_plus_real(_622397, _622393)), _622399 = _622397, _622395 = _622393], (240 ^ _614856) ^ [_622752, _622754, _622756, _622758] : [-(minus_minus_real(_622758, _622754) = minus_minus_real(_622756, _622752)), _622758 = _622756, _622754 = _622752], (250 ^ _614856) ^ [_623111, _623113, _623115, _623117] : [-(minus_minus_int(_623117, _623113) = minus_minus_int(_623115, _623111)), _623117 = _623115, _623113 = _623111], (260 ^ _614856) ^ [_623442, _623444] : [_623444 = _623442, -(number267125858f_real(_623444) = number267125858f_real(_623442))], (266 ^ _614856) ^ [_623688, _623690, _623692, _623694] : [-(minus_minus_nat(_623694, _623690) = minus_minus_nat(_623692, _623688)), _623694 = _623692, _623690 = _623688], (276 ^ _614856) ^ [_624047, _624049, _624051, _624053] : [-(times_times_real(_624053, _624049) = times_times_real(_624051, _624047)), _624053 = _624051, _624049 = _624047], (286 ^ _614856) ^ [_624406, _624408, _624410, _624412] : [-(times_times_int(_624412, _624408) = times_times_int(_624410, _624406)), _624412 = _624410, _624408 = _624406], (296 ^ _614856) ^ [_624765, _624767, _624769, _624771] : [-(power_power_real(_624771, _624767) = power_power_real(_624769, _624765)), _624771 = _624769, _624767 = _624765], (306 ^ _614856) ^ [_625124, _625126, _625128, _625130] : [-(plus_plus_nat(_625130, _625126) = plus_plus_nat(_625128, _625124)), _625130 = _625128, _625126 = _625124], (316 ^ _614856) ^ [_625483, _625485, _625487, _625489] : [-(power_power_nat(_625489, _625485) = power_power_nat(_625487, _625483)), _625489 = _625487, _625485 = _625483], (326 ^ _614856) ^ [_625842, _625844, _625846, _625848] : [-(times_times_nat(_625848, _625844) = times_times_nat(_625846, _625842)), _625848 = _625846, _625844 = _625842], (336 ^ _614856) ^ [_626201, _626203, _626205, _626207] : [-(plus_plus_int(_626207, _626203) = plus_plus_int(_626205, _626201)), _626207 = _626205, _626203 = _626201], (346 ^ _614856) ^ [_626560, _626562, _626564, _626566] : [-(power_power_int(_626566, _626562) = power_power_int(_626564, _626560)), _626566 = _626564, _626562 = _626560], (356 ^ _614856) ^ [_626891, _626893] : [_626893 = _626891, -(number_number_of_nat(_626893) = number_number_of_nat(_626891))], (362 ^ _614856) ^ [_627109, _627111] : [_627111 = _627109, -(bit0(_627111) = bit0(_627109))], (368 ^ _614856) ^ [_627307, _627309] : [_627309 = _627307, -(bit1(_627309) = bit1(_627307))], (2 ^ _614856) ^ [_615000] : [-(_615000 = _615000)], (4 ^ _614856) ^ [_615107, _615109] : [_615109 = _615107, -(_615107 = _615109)], (10 ^ _614856) ^ [_615311, _615313, _615315] : [-(_615315 = _615311), _615315 = _615313, _615313 = _615311], (20 ^ _614856) ^ [_615624, _615626] : [-(twoSqu142715416sum2sq(_615624)), _615626 = _615624, twoSqu142715416sum2sq(_615626)], (30 ^ _614856) ^ [_615919, _615921] : [-(zprime(_615919)), _615921 = _615919, zprime(_615921)], (40 ^ _614856) ^ [_616242, _616244, _616246, _616248] : [-(quadRes(_616246, _616242)), quadRes(_616248, _616244), _616248 = _616246, _616244 = _616242], (54 ^ _614856) ^ [_616714, _616716, _616718, _616720, _616722, _616724] : [-(zcong(_616722, _616718, _616714)), zcong(_616724, _616720, _616716), _616724 = _616722, _616720 = _616718, _616716 = _616714], (72 ^ _614856) ^ [_617267, _617269] : [-(is_int(_617267)), _617269 = _617267, is_int(_617269)], (82 ^ _614856) ^ [_617590, _617592, _617594, _617596] : [-(dvd_dvd_int(_617594, _617590)), dvd_dvd_int(_617596, _617592), _617596 = _617594, _617592 = _617590], (96 ^ _614856) ^ [_618034, _618036, _618038, _618040] : [-(dvd_dvd_real(_618038, _618034)), dvd_dvd_real(_618040, _618036), _618040 = _618038, _618036 = _618034], (110 ^ _614856) ^ [_618478, _618480, _618482, _618484] : [-(ord_less_eq_real(_618482, _618478)), ord_less_eq_real(_618484, _618480), _618484 = _618482, _618480 = _618478], (124 ^ _614856) ^ [_618922, _618924, _618926, _618928] : [-(ord_less_eq_int(_618926, _618922)), ord_less_eq_int(_618928, _618924), _618928 = _618926, _618924 = _618922], (138 ^ _614856) ^ [_619366, _619368, _619370, _619372] : [-(ord_less_real(_619370, _619366)), ord_less_real(_619372, _619368), _619372 = _619370, _619368 = _619366], (152 ^ _614856) ^ [_619810, _619812, _619814, _619816] : [-(ord_less_nat(_619814, _619810)), ord_less_nat(_619816, _619812), _619816 = _619814, _619812 = _619810], (166 ^ _614856) ^ [_620254, _620256, _620258, _620260] : [-(dvd_dvd_nat(_620258, _620254)), dvd_dvd_nat(_620260, _620256), _620260 = _620258, _620256 = _620254], (180 ^ _614856) ^ [_620698, _620700, _620702, _620704] : [-(ord_less_eq_nat(_620702, _620698)), ord_less_eq_nat(_620704, _620700), _620704 = _620702, _620700 = _620698], (194 ^ _614856) ^ [_621122, _621124, _621126, _621128] : [-(ord_less_int(_621126, _621122)), ord_less_int(_621128, _621124), _621128 = _621126, _621124 = _621122], (374 ^ _614856) ^ [_627631, _627633] : [-(is_int(minus_minus_int(_627633, _627631))), is_int(_627633), is_int(_627631)], (384 ^ _614856) ^ [] : [-(is_int(one_one_int))], (386 ^ _614856) ^ [_627983, _627985] : [-(is_int(plus_plus_int(_627985, _627983))), is_int(_627985), is_int(_627983)], (396 ^ _614856) ^ [_628282, _628284] : [-(is_int(times_times_int(_628284, _628282))), is_int(_628284), is_int(_628282)], (406 ^ _614856) ^ [] : [-(is_int(zero_zero_int))], (408 ^ _614856) ^ [] : [-(is_int(undefined_int(int)))], (410 ^ _614856) ^ [_628673] : [is_int(_628673), -(is_int(bit0(_628673)))], (416 ^ _614856) ^ [_628863] : [is_int(_628863), -(is_int(bit1(_628863)))], (422 ^ _614856) ^ [] : [-(is_int(min))], (424 ^ _614856) ^ [] : [-(is_int(pls))], (426 ^ _614856) ^ [_629159] : [is_int(_629159), -(is_int(number_number_of_int(_629159)))], (432 ^ _614856) ^ [_629363, _629365] : [is_int(_629365), -(is_int(power_power_int(_629365, _629363)))], (438 ^ _614856) ^ [_629575, _629577] : [-(is_int(legendre(_629577, _629575))), is_int(_629577), is_int(_629575)], (448 ^ _614856) ^ [] : [-(is_int(m))], (450 ^ _614856) ^ [] : [-(is_int(s1))], (452 ^ _614856) ^ [] : [-(is_int(s))], (454 ^ _614856) ^ [] : [-(is_int(t))], (456 ^ _614856) ^ [] : [-(ord_less_int(t, zero_zero_int))], (458 ^ _614856) ^ [] : [-(ord_less_int(t, one_one_int))], (460 ^ _614856) ^ [] : [-(ord_less_int(times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), m), one_one_int), t), times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), m), one_one_int), zero_zero_int)))], (462 ^ _614856) ^ [] : [-(plus_plus_int(power_power_int(s, number_number_of_nat(bit0(bit1(pls)))), one_one_int) = times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), m), one_one_int), t))], (464 ^ _614856) ^ [] : [t = zero_zero_int, -(plus_plus_int(power_power_int(s, number_number_of_nat(bit0(bit1(pls)))), one_one_int) = zero_zero_int)], (470 ^ _614856) ^ [] : [ord_less_eq_int(one_one_int, t)], (472 ^ _614856) ^ [] : [-(ord_less_int(zero_zero_int, plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), m), one_one_int)))], (474 ^ _614856) ^ [_630506, _630508] : [ord_less_real(plus_plus_real(power_power_real(_630508, number_number_of_nat(bit0(bit1(pls)))), power_power_real(_630506, number_number_of_nat(bit0(bit1(pls))))), zero_zero_real)], (476 ^ _614856) ^ [_630608, _630610] : [ord_less_int(plus_plus_int(power_power_int(_630610, number_number_of_nat(bit0(bit1(pls)))), power_power_int(_630608, number_number_of_nat(bit0(bit1(pls))))), zero_zero_int)], (488 ^ _614856) ^ [_631027, _631029] : [489 ^ _614856 : [(490 ^ _614856) ^ [] : [-(_631029 = zero_zero_real)], (492 ^ _614856) ^ [] : [-(_631027 = zero_zero_real)]], -(ord_less_real(zero_zero_real, plus_plus_real(power_power_real(_631029, number_number_of_nat(bit0(bit1(pls)))), power_power_real(_631027, number_number_of_nat(bit0(bit1(pls)))))))], (478 ^ _614856) ^ [_630755, _630757] : [ord_less_real(zero_zero_real, plus_plus_real(power_power_real(_630757, number_number_of_nat(bit0(bit1(pls)))), power_power_real(_630755, number_number_of_nat(bit0(bit1(pls)))))), _630757 = zero_zero_real, _630755 = zero_zero_real], (496 ^ _614856) ^ [_631337, _631339] : [is_int(_631339), is_int(_631337), 503 ^ _614856 : [(514 ^ _614856) ^ [] : [515 ^ _614856 : [(516 ^ _614856) ^ [] : [-(_631339 = zero_zero_int)], (518 ^ _614856) ^ [] : [-(_631337 = zero_zero_int)]], -(ord_less_int(zero_zero_int, plus_plus_int(power_power_int(_631339, number_number_of_nat(bit0(bit1(pls)))), power_power_int(_631337, number_number_of_nat(bit0(bit1(pls)))))))], (504 ^ _614856) ^ [] : [ord_less_int(zero_zero_int, plus_plus_int(power_power_int(_631339, number_number_of_nat(bit0(bit1(pls)))), power_power_int(_631337, number_number_of_nat(bit0(bit1(pls)))))), _631339 = zero_zero_int, _631337 = zero_zero_int]]], (522 ^ _614856) ^ [_632102, _632104] : [plus_plus_real(power_power_real(_632104, number_number_of_nat(bit0(bit1(pls)))), power_power_real(_632102, number_number_of_nat(bit0(bit1(pls))))) = zero_zero_real, 525 ^ _614856 : [(526 ^ _614856) ^ [] : [-(_632104 = zero_zero_real)], (528 ^ _614856) ^ [] : [-(_632102 = zero_zero_real)]]], (530 ^ _614856) ^ [_632357, _632359] : [-(plus_plus_real(power_power_real(_632359, number_number_of_nat(bit0(bit1(pls)))), power_power_real(_632357, number_number_of_nat(bit0(bit1(pls))))) = zero_zero_real), _632359 = zero_zero_real, _632357 = zero_zero_real], (540 ^ _614856) ^ [_632676, _632678] : [is_int(_632678), is_int(_632676), 547 ^ _614856 : [(548 ^ _614856) ^ [] : [plus_plus_int(power_power_int(_632678, number_number_of_nat(bit0(bit1(pls)))), power_power_int(_632676, number_number_of_nat(bit0(bit1(pls))))) = zero_zero_int, 551 ^ _614856 : [(552 ^ _614856) ^ [] : [-(_632678 = zero_zero_int)], (554 ^ _614856) ^ [] : [-(_632676 = zero_zero_int)]]], (556 ^ _614856) ^ [] : [-(plus_plus_int(power_power_int(_632678, number_number_of_nat(bit0(bit1(pls)))), power_power_int(_632676, number_number_of_nat(bit0(bit1(pls))))) = zero_zero_int), _632678 = zero_zero_int, _632676 = zero_zero_int]]], (566 ^ _614856) ^ [_633378] : [ord_less_real(power_power_real(_633378, number_number_of_nat(bit0(bit1(pls)))), zero_zero_real)], (568 ^ _614856) ^ [_633458] : [ord_less_int(power_power_int(_633458, number_number_of_nat(bit0(bit1(pls)))), zero_zero_int)], (570 ^ _614856) ^ [_633583] : [ord_less_real(zero_zero_real, power_power_real(_633583, number_number_of_nat(bit0(bit1(pls))))), _633583 = zero_zero_real], (576 ^ _614856) ^ [_633746] : [-(_633746 = zero_zero_real), -(ord_less_real(zero_zero_real, power_power_real(_633746, number_number_of_nat(bit0(bit1(pls))))))], (582 ^ _614856) ^ [_633947] : [is_int(_633947), 585 ^ _614856 : [(586 ^ _614856) ^ [] : [ord_less_int(zero_zero_int, power_power_int(_633947, number_number_of_nat(bit0(bit1(pls))))), _633947 = zero_zero_int], (592 ^ _614856) ^ [] : [-(_633947 = zero_zero_int), -(ord_less_int(zero_zero_int, power_power_int(_633947, number_number_of_nat(bit0(bit1(pls))))))]]], (598 ^ _614856) ^ [] : [-(power_power_real(one_one_real, number_number_of_nat(bit0(bit1(pls)))) = one_one_real)], (600 ^ _614856) ^ [] : [-(power_power_nat(one_one_nat, number_number_of_nat(bit0(bit1(pls)))) = one_one_nat)], (602 ^ _614856) ^ [] : [-(power_power_int(one_one_int, number_number_of_nat(bit0(bit1(pls)))) = one_one_int)], (604 ^ _614856) ^ [] : [-(power_power_real(zero_zero_real, number_number_of_nat(bit0(bit1(pls)))) = zero_zero_real)], (606 ^ _614856) ^ [] : [-(power_power_nat(zero_zero_nat, number_number_of_nat(bit0(bit1(pls)))) = zero_zero_nat)], (608 ^ _614856) ^ [] : [-(power_power_int(zero_zero_int, number_number_of_nat(bit0(bit1(pls)))) = zero_zero_int)], (610 ^ _614856) ^ [_634733] : [power_power_real(_634733, number_number_of_nat(bit0(bit1(pls)))) = zero_zero_real, -(_634733 = zero_zero_real)], (616 ^ _614856) ^ [_634895] : [_634895 = zero_zero_real, -(power_power_real(_634895, number_number_of_nat(bit0(bit1(pls)))) = zero_zero_real)], (622 ^ _614856) ^ [_635093] : [is_int(_635093), 625 ^ _614856 : [(626 ^ _614856) ^ [] : [power_power_int(_635093, number_number_of_nat(bit0(bit1(pls)))) = zero_zero_int, -(_635093 = zero_zero_int)], (632 ^ _614856) ^ [] : [_635093 = zero_zero_int, -(power_power_int(_635093, number_number_of_nat(bit0(bit1(pls)))) = zero_zero_int)]]], (638 ^ _614856) ^ [_635515] : [-(plus_plus_real(one_one_real, number267125858f_real(_635515)) = number267125858f_real(plus_plus_int(bit1(pls), _635515)))], (640 ^ _614856) ^ [_635603] : [-(plus_plus_int(one_one_int, number_number_of_int(_635603)) = number_number_of_int(plus_plus_int(bit1(pls), _635603)))], (642 ^ _614856) ^ [_635691] : [-(plus_plus_real(number267125858f_real(_635691), one_one_real) = number267125858f_real(plus_plus_int(_635691, bit1(pls))))], (644 ^ _614856) ^ [_635779] : [-(plus_plus_int(number_number_of_int(_635779), one_one_int) = number_number_of_int(plus_plus_int(_635779, bit1(pls))))], (646 ^ _614856) ^ [] : [-(ord_less_int(t, plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), m), one_one_int)))], (649 ^ _614856) ^ [] : [-(is_int(647 ^ []))], (651 ^ _614856) ^ [] : [-(plus_plus_int(power_power_int(s, number_number_of_nat(bit0(bit1(pls)))), one_one_int) = times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), m), one_one_int), 647 ^ []))], (653 ^ _614856) ^ [] : [-(zprime(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), m), one_one_int)))], (655 ^ _614856) ^ [] : [-(twoSqu142715416sum2sq(times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), m), one_one_int), t)))], (657 ^ _614856) ^ [_636181] : [-(ord_less_eq_int(_636181, _636181))], (659 ^ _614856) ^ [_636274] : [is_int(_636274), -(number_number_of_int(_636274) = _636274)], (665 ^ _614856) ^ [_636465, _636467] : [-(times_times_int(_636467, _636465) = times_times_int(_636465, _636467))], (667 ^ _614856) ^ [_636580, _636582] : [-(ord_less_eq_int(_636582, _636580)), -(ord_less_eq_int(_636580, _636582))], (673 ^ _614856) ^ [_636776, _636778] : [-(times_times_int(number_number_of_int(_636778), number_number_of_int(_636776)) = number_number_of_int(times_times_int(_636778, _636776)))], (675 ^ _614856) ^ [_636926, _636928] : [ord_less_eq_int(number_number_of_int(_636928), number_number_of_int(_636926)), -(ord_less_eq_int(_636928, _636926))], (681 ^ _614856) ^ [_637096, _637098] : [ord_less_eq_int(_637098, _637096), -(ord_less_eq_int(number_number_of_int(_637098), number_number_of_int(_637096)))], (687 ^ _614856) ^ [_637345, _637347] : [ord_less_eq_real(number267125858f_real(_637347), number267125858f_real(_637345)), -(ord_less_eq_int(_637347, _637345))], (693 ^ _614856) ^ [_637515, _637517] : [ord_less_eq_int(_637517, _637515), -(ord_less_eq_real(number267125858f_real(_637517), number267125858f_real(_637515)))], (699 ^ _614856) ^ [_637764, _637766] : [ord_less_eq_int(number_number_of_int(_637766), number_number_of_int(_637764)), -(ord_less_eq_int(_637766, _637764))], (705 ^ _614856) ^ [_637934, _637936] : [ord_less_eq_int(_637936, _637934), -(ord_less_eq_int(number_number_of_int(_637936), number_number_of_int(_637934)))], (711 ^ _614856) ^ [_638153, _638155, _638157] : [-(times_times_int(times_times_int(_638157, _638155), _638153) = times_times_int(_638157, times_times_int(_638155, _638153)))], (713 ^ _614856) ^ [_638290, _638292, _638294] : [ord_less_eq_int(_638292, _638290), ord_less_eq_int(_638290, _638294), -(ord_less_eq_int(_638292, _638294))], (723 ^ _614856) ^ [_638599, _638601] : [is_int(_638601), is_int(_638599), ord_less_eq_int(_638601, _638599), ord_less_eq_int(_638599, _638601), -(_638601 = _638599)], (741 ^ _614856) ^ [_639073, _639075, _639077] : [-(power_power_int(_639077, plus_plus_nat(_639075, _639073)) = times_times_int(power_power_int(_639077, _639075), power_power_int(_639077, _639073)))], (743 ^ _614856) ^ [_639228, _639230] : [ord_less_eq_int(bit1(_639230), bit1(_639228)), -(ord_less_eq_int(_639230, _639228))], (749 ^ _614856) ^ [_639398, _639400] : [ord_less_eq_int(_639400, _639398), -(ord_less_eq_int(bit1(_639400), bit1(_639398)))], (755 ^ _614856) ^ [_639647, _639649] : [ord_less_eq_int(bit1(_639649), bit1(_639647)), -(ord_less_eq_int(_639649, _639647))], (761 ^ _614856) ^ [_639817, _639819] : [ord_less_eq_int(_639819, _639817), -(ord_less_eq_int(bit1(_639819), bit1(_639817)))], (767 ^ _614856) ^ [] : [-(ord_less_eq_int(pls, pls))], (769 ^ _614856) ^ [_640119, _640121] : [ord_less_eq_int(bit0(_640121), bit0(_640119)), -(ord_less_eq_int(_640121, _640119))], (775 ^ _614856) ^ [_640289, _640291] : [ord_less_eq_int(_640291, _640289), -(ord_less_eq_int(bit0(_640291), bit0(_640289)))], (781 ^ _614856) ^ [_640538, _640540] : [ord_less_eq_int(bit0(_640540), bit0(_640538)), -(ord_less_eq_int(_640540, _640538))], (787 ^ _614856) ^ [_640708, _640710] : [ord_less_eq_int(_640710, _640708), -(ord_less_eq_int(bit0(_640710), bit0(_640708)))], (793 ^ _614856) ^ [_640928, _640930] : [is_int(_640930), is_int(_640928), 800 ^ _614856 : [(801 ^ _614856) ^ [] : [ord_less_int(_640930, _640928), 804 ^ _614856 : [(805 ^ _614856) ^ [] : [-(ord_less_eq_int(_640930, _640928))], (807 ^ _614856) ^ [] : [_640930 = _640928]]], (809 ^ _614856) ^ [] : [-(ord_less_int(_640930, _640928)), ord_less_eq_int(_640930, _640928), -(_640930 = _640928)]]], (819 ^ _614856) ^ [_641649, _641651, _641653] : [ord_less_eq_int(_641651, _641649), -(ord_less_eq_int(plus_plus_int(_641653, _641651), plus_plus_int(_641653, _641649)))], (825 ^ _614856) ^ [_641892] : [number_number_of_nat(_641892) = zero_zero_nat, -(ord_less_eq_int(_641892, pls))], (831 ^ _614856) ^ [_642052] : [ord_less_eq_int(_642052, pls), -(number_number_of_nat(_642052) = zero_zero_nat)], (837 ^ _614856) ^ [_642277] : [zero_zero_nat = number_number_of_nat(_642277), -(ord_less_eq_int(_642277, pls))], (843 ^ _614856) ^ [_642437] : [ord_less_eq_int(_642437, pls), -(zero_zero_nat = number_number_of_nat(_642437))], (849 ^ _614856) ^ [_642647, _642649] : [ord_less_eq_int(pls, _642647), ord_less_eq_int(pls, _642649), -(times_times_real(number267125858f_real(_642647), number267125858f_real(_642649)) = number267125858f_real(times_times_int(_642647, _642649)))], (859 ^ _614856) ^ [_642970, _642972] : [ord_less_eq_int(pls, _642970), ord_less_eq_int(pls, _642972), -(times_times_nat(number_number_of_nat(_642970), number_number_of_nat(_642972)) = number_number_of_nat(times_times_int(_642970, _642972)))], (869 ^ _614856) ^ [_643293, _643295] : [ord_less_eq_int(pls, _643293), ord_less_eq_int(pls, _643295), -(times_times_int(number_number_of_int(_643293), number_number_of_int(_643295)) = number_number_of_int(times_times_int(_643293, _643295)))], (879 ^ _614856) ^ [_643615, _643617, _643619] : [-(times_times_real(number267125858f_real(_643619), times_times_real(number267125858f_real(_643617), _643615)) = times_times_real(number267125858f_real(times_times_int(_643619, _643617)), _643615))], (881 ^ _614856) ^ [_643743, _643745, _643747] : [-(times_times_int(number_number_of_int(_643747), times_times_int(number_number_of_int(_643745), _643743)) = times_times_int(number_number_of_int(times_times_int(_643747, _643745)), _643743))], (883 ^ _614856) ^ [_643857, _643859] : [-(times_times_real(number267125858f_real(_643859), number267125858f_real(_643857)) = number267125858f_real(times_times_int(_643859, _643857)))], (885 ^ _614856) ^ [_643963, _643965] : [-(times_times_int(number_number_of_int(_643965), number_number_of_int(_643963)) = number_number_of_int(times_times_int(_643965, _643963)))], (887 ^ _614856) ^ [_644069, _644071] : [-(number267125858f_real(times_times_int(_644071, _644069)) = times_times_real(number267125858f_real(_644071), number267125858f_real(_644069)))], (889 ^ _614856) ^ [_644175, _644177] : [-(number_number_of_int(times_times_int(_644177, _644175)) = times_times_int(number_number_of_int(_644177), number_number_of_int(_644175)))], (891 ^ _614856) ^ [_644325, _644327] : [ord_less_eq_real(plus_plus_real(times_times_real(_644327, _644327), times_times_real(_644325, _644325)), zero_zero_real), 894 ^ _614856 : [(895 ^ _614856) ^ [] : [-(_644327 = zero_zero_real)], (897 ^ _614856) ^ [] : [-(_644325 = zero_zero_real)]]], (899 ^ _614856) ^ [_644580, _644582] : [-(ord_less_eq_real(plus_plus_real(times_times_real(_644582, _644582), times_times_real(_644580, _644580)), zero_zero_real)), _644582 = zero_zero_real, _644580 = zero_zero_real], (909 ^ _614856) ^ [_644899, _644901] : [is_int(_644901), is_int(_644899), 916 ^ _614856 : [(917 ^ _614856) ^ [] : [ord_less_eq_int(plus_plus_int(times_times_int(_644901, _644901), times_times_int(_644899, _644899)), zero_zero_int), 920 ^ _614856 : [(921 ^ _614856) ^ [] : [-(_644901 = zero_zero_int)], (923 ^ _614856) ^ [] : [-(_644899 = zero_zero_int)]]], (925 ^ _614856) ^ [] : [-(ord_less_eq_int(plus_plus_int(times_times_int(_644901, _644901), times_times_int(_644899, _644899)), zero_zero_int)), _644901 = zero_zero_int, _644899 = zero_zero_int]]], (935 ^ _614856) ^ [_645616, _645618] : [-(ord_less_eq_real(zero_zero_real, plus_plus_real(times_times_real(_645618, _645618), times_times_real(_645616, _645616))))], (937 ^ _614856) ^ [_645719, _645721] : [-(ord_less_eq_int(zero_zero_int, plus_plus_int(times_times_int(_645721, _645721), times_times_int(_645719, _645719))))], (939 ^ _614856) ^ [_645852] : [ord_less_eq_real(number267125858f_real(_645852), zero_zero_real), -(ord_less_eq_int(_645852, pls))], (945 ^ _614856) ^ [_646012] : [ord_less_eq_int(_646012, pls), -(ord_less_eq_real(number267125858f_real(_646012), zero_zero_real))], (951 ^ _614856) ^ [_646237] : [ord_less_eq_int(number_number_of_int(_646237), zero_zero_int), -(ord_less_eq_int(_646237, pls))], (957 ^ _614856) ^ [_646397] : [ord_less_eq_int(_646397, pls), -(ord_less_eq_int(number_number_of_int(_646397), zero_zero_int))], (963 ^ _614856) ^ [_646622] : [ord_less_eq_real(zero_zero_real, number267125858f_real(_646622)), -(ord_less_eq_int(pls, _646622))], (969 ^ _614856) ^ [_646782] : [ord_less_eq_int(pls, _646782), -(ord_less_eq_real(zero_zero_real, number267125858f_real(_646782)))], (975 ^ _614856) ^ [_647007] : [ord_less_eq_int(zero_zero_int, number_number_of_int(_647007)), -(ord_less_eq_int(pls, _647007))], (981 ^ _614856) ^ [_647167] : [ord_less_eq_int(pls, _647167), -(ord_less_eq_int(zero_zero_int, number_number_of_int(_647167)))], (987 ^ _614856) ^ [_647392] : [ord_less_nat(zero_zero_nat, number_number_of_nat(_647392)), -(ord_less_int(pls, _647392))], (993 ^ _614856) ^ [_647552] : [ord_less_int(pls, _647552), -(ord_less_nat(zero_zero_nat, number_number_of_nat(_647552)))], (999 ^ _614856) ^ [_647791, _647793] : [ord_less_eq_real(number267125858f_real(_647793), number267125858f_real(_647791)), ord_less_real(number267125858f_real(_647791), number267125858f_real(_647793))], (1005 ^ _614856) ^ [_647970, _647972] : [-(ord_less_real(number267125858f_real(_647970), number267125858f_real(_647972))), -(ord_less_eq_real(number267125858f_real(_647972), number267125858f_real(_647970)))], (1011 ^ _614856) ^ [_648230, _648232] : [ord_less_eq_nat(number_number_of_nat(_648232), number_number_of_nat(_648230)), ord_less_nat(number_number_of_nat(_648230), number_number_of_nat(_648232))], (1017 ^ _614856) ^ [_648409, _648411] : [-(ord_less_nat(number_number_of_nat(_648409), number_number_of_nat(_648411))), -(ord_less_eq_nat(number_number_of_nat(_648411), number_number_of_nat(_648409)))], (1023 ^ _614856) ^ [_648669, _648671] : [ord_less_eq_int(number_number_of_int(_648671), number_number_of_int(_648669)), ord_less_int(number_number_of_int(_648669), number_number_of_int(_648671))], (1029 ^ _614856) ^ [_648848, _648850] : [-(ord_less_int(number_number_of_int(_648848), number_number_of_int(_648850))), -(ord_less_eq_int(number_number_of_int(_648850), number_number_of_int(_648848)))], (1035 ^ _614856) ^ [_649094] : [ord_less_eq_int(pls, bit1(_649094)), -(ord_less_eq_int(pls, _649094))], (1041 ^ _614856) ^ [_649254] : [ord_less_eq_int(pls, _649254), -(ord_less_eq_int(pls, bit1(_649254)))], (1047 ^ _614856) ^ [_649493, _649495] : [ord_less_eq_int(bit0(_649495), bit1(_649493)), -(ord_less_eq_int(_649495, _649493))], (1053 ^ _614856) ^ [_649663, _649665] : [ord_less_eq_int(_649665, _649663), -(ord_less_eq_int(bit0(_649665), bit1(_649663)))], (1059 ^ _614856) ^ [_649912, _649914] : [ord_less_eq_int(bit0(_649914), bit1(_649912)), -(ord_less_eq_int(_649914, _649912))], (1065 ^ _614856) ^ [_650082, _650084] : [ord_less_eq_int(_650084, _650082), -(ord_less_eq_int(bit0(_650084), bit1(_650082)))], (1071 ^ _614856) ^ [_650317] : [ord_less_eq_int(bit0(_650317), pls), -(ord_less_eq_int(_650317, pls))], (1077 ^ _614856) ^ [_650477] : [ord_less_eq_int(_650477, pls), -(ord_less_eq_int(bit0(_650477), pls))], (1083 ^ _614856) ^ [_650702] : [ord_less_eq_int(pls, bit0(_650702)), -(ord_less_eq_int(pls, _650702))], (1089 ^ _614856) ^ [_650862] : [ord_less_eq_int(pls, _650862), -(ord_less_eq_int(pls, bit0(_650862)))], (1095 ^ _614856) ^ [_651100, _651102, _651104, _651106] : [ord_less_int(_651102, _651100), ord_less_eq_int(_651106, _651104), -(ord_less_int(plus_plus_int(_651102, _651106), plus_plus_int(_651100, _651104)))], (1105 ^ _614856) ^ [] : [-(number_number_of_nat(pls) = zero_zero_nat)], (1107 ^ _614856) ^ [] : [-(zero_zero_nat = number_number_of_nat(pls))], (1109 ^ _614856) ^ [_651552] : [ord_less_eq_real(number267125858f_real(_651552), one_one_real), -(ord_less_eq_int(_651552, bit1(pls)))], (1115 ^ _614856) ^ [_651712] : [ord_less_eq_int(_651712, bit1(pls)), -(ord_less_eq_real(number267125858f_real(_651712), one_one_real))], (1121 ^ _614856) ^ [_651937] : [ord_less_eq_int(number_number_of_int(_651937), one_one_int), -(ord_less_eq_int(_651937, bit1(pls)))], (1127 ^ _614856) ^ [_652097] : [ord_less_eq_int(_652097, bit1(pls)), -(ord_less_eq_int(number_number_of_int(_652097), one_one_int))], (1133 ^ _614856) ^ [_652322] : [ord_less_eq_real(one_one_real, number267125858f_real(_652322)), -(ord_less_eq_int(bit1(pls), _652322))], (1139 ^ _614856) ^ [_652482] : [ord_less_eq_int(bit1(pls), _652482), -(ord_less_eq_real(one_one_real, number267125858f_real(_652482)))], (1145 ^ _614856) ^ [_652707] : [ord_less_eq_int(one_one_int, number_number_of_int(_652707)), -(ord_less_eq_int(bit1(pls), _652707))], (1151 ^ _614856) ^ [_652867] : [ord_less_eq_int(bit1(pls), _652867), -(ord_less_eq_int(one_one_int, number_number_of_int(_652867)))], (1157 ^ _614856) ^ [] : [-(plus_plus_nat(one_one_nat, one_one_nat) = number_number_of_nat(bit0(bit1(pls))))], (1159 ^ _614856) ^ [_653101] : [-(times_times_int(pls, _653101) = pls)], (1161 ^ _614856) ^ [_653196, _653198] : [-(times_times_int(bit0(_653198), _653196) = bit0(times_times_int(_653198, _653196)))], (1163 ^ _614856) ^ [_653344, _653346] : [ord_less_int(number_number_of_int(_653346), number_number_of_int(_653344)), -(ord_less_int(_653346, _653344))], (1169 ^ _614856) ^ [_653514, _653516] : [ord_less_int(_653516, _653514), -(ord_less_int(number_number_of_int(_653516), number_number_of_int(_653514)))], (1175 ^ _614856) ^ [_653720] : [is_int(_653720), -(times_times_int(_653720, one_one_int) = _653720)], (1181 ^ _614856) ^ [_653914] : [is_int(_653914), -(times_times_int(one_one_int, _653914) = _653914)], (1187 ^ _614856) ^ [_654107, _654109] : [-(plus_plus_int(number_number_of_int(_654109), number_number_of_int(_654107)) = number_number_of_int(plus_plus_int(_654109, _654107)))], (1189 ^ _614856) ^ [_654227, _654229, _654231] : [-(times_times_int(plus_plus_int(_654231, _654229), _654227) = plus_plus_int(times_times_int(_654231, _654227), times_times_int(_654229, _654227)))], (1191 ^ _614856) ^ [_654352, _654354, _654356] : [-(times_times_int(_654356, plus_plus_int(_654354, _654352)) = plus_plus_int(times_times_int(_654356, _654354), times_times_int(_654356, _654352)))], (1193 ^ _614856) ^ [_654493] : [ord_less_eq_int(bit1(_654493), pls), -(ord_less_int(_654493, pls))], (1199 ^ _614856) ^ [_654653] : [ord_less_int(_654653, pls), -(ord_less_eq_int(bit1(_654653), pls))], (1205 ^ _614856) ^ [_654878] : [ord_less_int(pls, bit1(_654878)), -(ord_less_eq_int(pls, _654878))], (1211 ^ _614856) ^ [_655038] : [ord_less_eq_int(pls, _655038), -(ord_less_int(pls, bit1(_655038)))], (1217 ^ _614856) ^ [_655277, _655279] : [ord_less_eq_int(bit1(_655279), bit0(_655277)), -(ord_less_int(_655279, _655277))], (1223 ^ _614856) ^ [_655447, _655449] : [ord_less_int(_655449, _655447), -(ord_less_eq_int(bit1(_655449), bit0(_655447)))], (1229 ^ _614856) ^ [_655696, _655698] : [ord_less_eq_int(bit1(_655698), bit0(_655696)), -(ord_less_int(_655698, _655696))], (1235 ^ _614856) ^ [_655866, _655868] : [ord_less_int(_655868, _655866), -(ord_less_eq_int(bit1(_655868), bit0(_655866)))], (1241 ^ _614856) ^ [_656115, _656117] : [ord_less_int(bit0(_656117), bit1(_656115)), -(ord_less_eq_int(_656117, _656115))], (1247 ^ _614856) ^ [_656285, _656287] : [ord_less_eq_int(_656287, _656285), -(ord_less_int(bit0(_656287), bit1(_656285)))], (1253 ^ _614856) ^ [_656534, _656536] : [ord_less_int(bit0(_656536), bit1(_656534)), -(ord_less_eq_int(_656536, _656534))], (1259 ^ _614856) ^ [_656704, _656706] : [ord_less_eq_int(_656706, _656704), -(ord_less_int(bit0(_656706), bit1(_656704)))], (1265 ^ _614856) ^ [_656953, _656955] : [ord_less_nat(number_number_of_nat(_656955), number_number_of_nat(_656953)), 1268 ^ _614856 : [(1275 ^ _614856) ^ [] : [-(ord_less_int(_656955, _656953))], (1269 ^ _614856) ^ [] : [ord_less_int(_656955, _656953), -(ord_less_int(pls, _656953))]]], (1277 ^ _614856) ^ [_657287, _657289] : [-(ord_less_nat(number_number_of_nat(_657289), number_number_of_nat(_657287))), 1280 ^ _614856 : [(1281 ^ _614856) ^ [] : [-(ord_less_int(_657289, _657287))], (1283 ^ _614856) ^ [] : [ord_less_int(pls, _657287)]], ord_less_int(_657289, _657287)], (1289 ^ _614856) ^ [_657686] : [ord_less_eq_int(one_one_int, _657686), -(ord_less_int(zero_zero_int, _657686))], (1295 ^ _614856) ^ [_657842] : [ord_less_int(zero_zero_int, _657842), -(ord_less_eq_int(one_one_int, _657842))], (1301 ^ _614856) ^ [] : [-(number_number_of_nat(bit1(pls)) = one_one_nat)], (1303 ^ _614856) ^ [] : [-(one_one_nat = number_number_of_nat(bit1(pls)))], (1305 ^ _614856) ^ [_658154, _658156] : [ord_less_int(_658156, _658154), -(ord_less_eq_int(plus_plus_int(_658156, one_one_int), _658154))], (1311 ^ _614856) ^ [_658399, _658401] : [ord_less_eq_int(plus_plus_int(_658401, one_one_int), _658399), -(ord_less_int(_658401, _658399))], (1317 ^ _614856) ^ [_658567, _658569] : [ord_less_int(_658569, _658567), -(ord_less_eq_int(plus_plus_int(_658569, one_one_int), _658567))], (1323 ^ _614856) ^ [_658814, _658816] : [ord_less_int(_658816, plus_plus_int(_658814, one_one_int)), -(ord_less_eq_int(_658816, _658814))], (1329 ^ _614856) ^ [_658982, _658984] : [ord_less_eq_int(_658984, _658982), -(ord_less_int(_658984, plus_plus_int(_658982, one_one_int)))], (1335 ^ _614856) ^ [_659200, _659202] : [ord_less_eq_int(pls, _659200), ord_less_eq_int(pls, _659202), -(plus_plus_real(number267125858f_real(_659200), number267125858f_real(_659202)) = number267125858f_real(plus_plus_int(_659200, _659202)))], (1345 ^ _614856) ^ [_659523, _659525] : [ord_less_eq_int(pls, _659523), ord_less_eq_int(pls, _659525), -(plus_plus_nat(number_number_of_nat(_659523), number_number_of_nat(_659525)) = number_number_of_nat(plus_plus_int(_659523, _659525)))], (1355 ^ _614856) ^ [_659846, _659848] : [ord_less_eq_int(pls, _659846), ord_less_eq_int(pls, _659848), -(plus_plus_int(number_number_of_int(_659846), number_number_of_int(_659848)) = number_number_of_int(plus_plus_int(_659846, _659848)))], (1365 ^ _614856) ^ [_660189, _660191] : [ord_less_int(_660189, pls), -(plus_plus_nat(number_number_of_nat(_660189), number_number_of_nat(_660191)) = number_number_of_nat(_660191))], (1371 ^ _614856) ^ [_660369, _660371] : [-(ord_less_int(_660369, pls)), 1374 ^ _614856 : [(1375 ^ _614856) ^ [] : [ord_less_int(_660371, pls), -(plus_plus_nat(number_number_of_nat(_660369), number_number_of_nat(_660371)) = number_number_of_nat(_660369))], (1381 ^ _614856) ^ [] : [-(ord_less_int(_660371, pls)), -(plus_plus_nat(number_number_of_nat(_660369), number_number_of_nat(_660371)) = number_number_of_nat(plus_plus_int(_660369, _660371)))]]], (1387 ^ _614856) ^ [_660868] : [ord_less_eq_int(zero_zero_int, _660868), -(ord_less_int(zero_zero_int, plus_plus_int(one_one_int, _660868)))], (1393 ^ _614856) ^ [_661078, _661080] : [is_int(_661080), is_int(_661078), 1400 ^ _614856 : [(1401 ^ _614856) ^ [] : [number267125858f_real(_661080) = number267125858f_real(_661078), -(_661080 = _661078)], (1407 ^ _614856) ^ [] : [_661080 = _661078, -(number267125858f_real(_661080) = number267125858f_real(_661078))]]], (1413 ^ _614856) ^ [_661637, _661639] : [is_int(_661639), is_int(_661637), 1420 ^ _614856 : [(1421 ^ _614856) ^ [] : [number_number_of_int(_661639) = number_number_of_int(_661637), -(_661639 = _661637)], (1427 ^ _614856) ^ [] : [_661639 = _661637, -(number_number_of_int(_661639) = number_number_of_int(_661637))]]], (1433 ^ _614856) ^ [_662225, _662227] : [number267125858f_real(_662227) = _662225, -(_662225 = number267125858f_real(_662227))], (1439 ^ _614856) ^ [_662395, _662397] : [_662395 = number267125858f_real(_662397), -(number267125858f_real(_662397) = _662395)], (1445 ^ _614856) ^ [_662615, _662617] : [is_int(_662615), 1448 ^ _614856 : [(1449 ^ _614856) ^ [] : [number_number_of_int(_662617) = _662615, -(_662615 = number_number_of_int(_662617))], (1455 ^ _614856) ^ [] : [_662615 = number_number_of_int(_662617), -(number_number_of_int(_662617) = _662615)]]], (1461 ^ _614856) ^ [_663114, _663116] : [number_number_of_nat(_663116) = _663114, -(_663114 = number_number_of_nat(_663116))], (1467 ^ _614856) ^ [_663284, _663286] : [_663284 = number_number_of_nat(_663286), -(number_number_of_nat(_663286) = _663284)], (1473 ^ _614856) ^ [_663504, _663506] : [is_int(_663506), is_int(_663504), 1480 ^ _614856 : [(1481 ^ _614856) ^ [] : [bit1(_663506) = bit1(_663504), -(_663506 = _663504)], (1487 ^ _614856) ^ [] : [_663506 = _663504, -(bit1(_663506) = bit1(_663504))]]], (1493 ^ _614856) ^ [_664063, _664065] : [is_int(_664065), is_int(_664063), 1500 ^ _614856 : [(1501 ^ _614856) ^ [] : [bit0(_664065) = bit0(_664063), -(_664065 = _664063)], (1507 ^ _614856) ^ [] : [_664065 = _664063, -(bit0(_664065) = bit0(_664063))]]], (1513 ^ _614856) ^ [_664622, _664624] : [is_int(_664624), is_int(_664622), -(ord_less_int(_664624, _664622)), -(_664624 = _664622), -(ord_less_int(_664622, _664624))], (1531 ^ _614856) ^ [_665128, _665130] : [plus_plus_real(times_times_real(_665130, _665130), times_times_real(_665128, _665128)) = zero_zero_real, 1534 ^ _614856 : [(1535 ^ _614856) ^ [] : [-(_665130 = zero_zero_real)], (1537 ^ _614856) ^ [] : [-(_665128 = zero_zero_real)]]], (1539 ^ _614856) ^ [_665383, _665385] : [-(plus_plus_real(times_times_real(_665385, _665385), times_times_real(_665383, _665383)) = zero_zero_real), _665385 = zero_zero_real, _665383 = zero_zero_real], (1549 ^ _614856) ^ [_665702, _665704] : [is_int(_665704), is_int(_665702), 1556 ^ _614856 : [(1557 ^ _614856) ^ [] : [plus_plus_int(times_times_int(_665704, _665704), times_times_int(_665702, _665702)) = zero_zero_int, 1560 ^ _614856 : [(1561 ^ _614856) ^ [] : [-(_665704 = zero_zero_int)], (1563 ^ _614856) ^ [] : [-(_665702 = zero_zero_int)]]], (1565 ^ _614856) ^ [] : [-(plus_plus_int(times_times_int(_665704, _665704), times_times_int(_665702, _665702)) = zero_zero_int), _665704 = zero_zero_int, _665702 = zero_zero_int]]], (1575 ^ _614856) ^ [_666433, _666435, _666437] : [-(times_times_real(plus_plus_real(_666437, _666435), number267125858f_real(_666433)) = plus_plus_real(times_times_real(_666437, number267125858f_real(_666433)), times_times_real(_666435, number267125858f_real(_666433))))], (1577 ^ _614856) ^ [_666564, _666566, _666568] : [-(times_times_nat(plus_plus_nat(_666568, _666566), number_number_of_nat(_666564)) = plus_plus_nat(times_times_nat(_666568, number_number_of_nat(_666564)), times_times_nat(_666566, number_number_of_nat(_666564))))], (1579 ^ _614856) ^ [_666695, _666697, _666699] : [-(times_times_int(plus_plus_int(_666699, _666697), number_number_of_int(_666695)) = plus_plus_int(times_times_int(_666699, number_number_of_int(_666695)), times_times_int(_666697, number_number_of_int(_666695))))], (1581 ^ _614856) ^ [_666826, _666828, _666830] : [-(times_times_real(number267125858f_real(_666830), plus_plus_real(_666828, _666826)) = plus_plus_real(times_times_real(number267125858f_real(_666830), _666828), times_times_real(number267125858f_real(_666830), _666826)))], (1583 ^ _614856) ^ [_666957, _666959, _666961] : [-(times_times_nat(number_number_of_nat(_666961), plus_plus_nat(_666959, _666957)) = plus_plus_nat(times_times_nat(number_number_of_nat(_666961), _666959), times_times_nat(number_number_of_nat(_666961), _666957)))], (1585 ^ _614856) ^ [_667088, _667090, _667092] : [-(times_times_int(number_number_of_int(_667092), plus_plus_int(_667090, _667088)) = plus_plus_int(times_times_int(number_number_of_int(_667092), _667090), times_times_int(number_number_of_int(_667092), _667088)))], (1587 ^ _614856) ^ [_667219, _667221, _667223] : [-(plus_plus_int(plus_plus_int(_667223, _667221), _667219) = plus_plus_int(_667223, plus_plus_int(_667221, _667219)))], (1589 ^ _614856) ^ [_667341, _667343, _667345] : [-(plus_plus_int(_667345, plus_plus_int(_667343, _667341)) = plus_plus_int(_667343, plus_plus_int(_667345, _667341)))], (1591 ^ _614856) ^ [_667449, _667451] : [-(plus_plus_int(_667451, _667449) = plus_plus_int(_667449, _667451))], (1593 ^ _614856) ^ [] : [-(zero_zero_int = number_number_of_int(pls))], (1595 ^ _614856) ^ [_667631, _667633, _667635] : [ord_less_int(_667633, _667631), ord_less_int(zero_zero_int, _667635), -(ord_less_int(times_times_int(_667635, _667633), times_times_int(_667635, _667631)))], (1605 ^ _614856) ^ [_667952, _667954] : [power_power_real(_667954, number_number_of_nat(bit0(bit1(pls)))) = power_power_real(_667952, number_number_of_nat(bit0(bit1(pls)))), ord_less_eq_real(zero_zero_real, _667954), ord_less_eq_real(zero_zero_real, _667952), -(_667954 = _667952)], (1619 ^ _614856) ^ [_668352, _668354] : [power_power_nat(_668354, number_number_of_nat(bit0(bit1(pls)))) = power_power_nat(_668352, number_number_of_nat(bit0(bit1(pls)))), ord_less_eq_nat(zero_zero_nat, _668354), ord_less_eq_nat(zero_zero_nat, _668352), -(_668354 = _668352)], (1633 ^ _614856) ^ [_668752, _668754] : [is_int(_668754), is_int(_668752), power_power_int(_668754, number_number_of_nat(bit0(bit1(pls)))) = power_power_int(_668752, number_number_of_nat(bit0(bit1(pls)))), ord_less_eq_int(zero_zero_int, _668754), ord_less_eq_int(zero_zero_int, _668752), -(_668754 = _668752)], (1655 ^ _614856) ^ [_669328, _669330] : [ord_less_eq_real(power_power_real(_669330, number_number_of_nat(bit0(bit1(pls)))), power_power_real(_669328, number_number_of_nat(bit0(bit1(pls))))), ord_less_eq_real(zero_zero_real, _669328), -(ord_less_eq_real(_669330, _669328))], (1665 ^ _614856) ^ [_669639, _669641] : [ord_less_eq_nat(power_power_nat(_669641, number_number_of_nat(bit0(bit1(pls)))), power_power_nat(_669639, number_number_of_nat(bit0(bit1(pls))))), ord_less_eq_nat(zero_zero_nat, _669639), -(ord_less_eq_nat(_669641, _669639))], (1675 ^ _614856) ^ [_669950, _669952] : [ord_less_eq_int(power_power_int(_669952, number_number_of_nat(bit0(bit1(pls)))), power_power_int(_669950, number_number_of_nat(bit0(bit1(pls))))), ord_less_eq_int(zero_zero_int, _669950), -(ord_less_eq_int(_669952, _669950))], (1685 ^ _614856) ^ [_670232] : [-(ord_less_eq_real(zero_zero_real, power_power_real(_670232, number_number_of_nat(bit0(bit1(pls))))))], (1687 ^ _614856) ^ [_670313] : [-(ord_less_eq_int(zero_zero_int, power_power_int(_670313, number_number_of_nat(bit0(bit1(pls))))))], (1689 ^ _614856) ^ [_670423, _670425] : [ord_less_real(power_power_real(_670425, number_number_of_nat(bit0(bit1(pls)))), power_power_real(_670423, number_number_of_nat(bit0(bit1(pls))))), ord_less_eq_real(zero_zero_real, _670423), -(ord_less_real(_670425, _670423))], (1699 ^ _614856) ^ [_670734, _670736] : [ord_less_nat(power_power_nat(_670736, number_number_of_nat(bit0(bit1(pls)))), power_power_nat(_670734, number_number_of_nat(bit0(bit1(pls))))), ord_less_eq_nat(zero_zero_nat, _670734), -(ord_less_nat(_670736, _670734))], (1709 ^ _614856) ^ [_671045, _671047] : [ord_less_int(power_power_int(_671047, number_number_of_nat(bit0(bit1(pls)))), power_power_int(_671045, number_number_of_nat(bit0(bit1(pls))))), ord_less_eq_int(zero_zero_int, _671045), -(ord_less_int(_671047, _671045))], (1719 ^ _614856) ^ [_671385, _671387] : [ord_less_eq_real(plus_plus_real(power_power_real(_671387, number_number_of_nat(bit0(bit1(pls)))), power_power_real(_671385, number_number_of_nat(bit0(bit1(pls))))), zero_zero_real), 1722 ^ _614856 : [(1723 ^ _614856) ^ [] : [-(_671387 = zero_zero_real)], (1725 ^ _614856) ^ [] : [-(_671385 = zero_zero_real)]]], (1727 ^ _614856) ^ [_671640, _671642] : [-(ord_less_eq_real(plus_plus_real(power_power_real(_671642, number_number_of_nat(bit0(bit1(pls)))), power_power_real(_671640, number_number_of_nat(bit0(bit1(pls))))), zero_zero_real)), _671642 = zero_zero_real, _671640 = zero_zero_real], (1737 ^ _614856) ^ [_671959, _671961] : [is_int(_671961), is_int(_671959), 1744 ^ _614856 : [(1745 ^ _614856) ^ [] : [ord_less_eq_int(plus_plus_int(power_power_int(_671961, number_number_of_nat(bit0(bit1(pls)))), power_power_int(_671959, number_number_of_nat(bit0(bit1(pls))))), zero_zero_int), 1748 ^ _614856 : [(1749 ^ _614856) ^ [] : [-(_671961 = zero_zero_int)], (1751 ^ _614856) ^ [] : [-(_671959 = zero_zero_int)]]], (1753 ^ _614856) ^ [] : [-(ord_less_eq_int(plus_plus_int(power_power_int(_671961, number_number_of_nat(bit0(bit1(pls)))), power_power_int(_671959, number_number_of_nat(bit0(bit1(pls))))), zero_zero_int)), _671961 = zero_zero_int, _671959 = zero_zero_int]]], (1763 ^ _614856) ^ [_672676, _672678] : [-(ord_less_eq_real(zero_zero_real, plus_plus_real(power_power_real(_672678, number_number_of_nat(bit0(bit1(pls)))), power_power_real(_672676, number_number_of_nat(bit0(bit1(pls)))))))], (1765 ^ _614856) ^ [_672779, _672781] : [-(ord_less_eq_int(zero_zero_int, plus_plus_int(power_power_int(_672781, number_number_of_nat(bit0(bit1(pls)))), power_power_int(_672779, number_number_of_nat(bit0(bit1(pls)))))))], (1777 ^ _614856) ^ [_673198, _673200] : [1778 ^ _614856 : [(1779 ^ _614856) ^ [] : [-(_673200 = zero_zero_real)], (1781 ^ _614856) ^ [] : [-(_673198 = zero_zero_real)]], -(ord_less_real(zero_zero_real, plus_plus_real(times_times_real(_673200, _673200), times_times_real(_673198, _673198))))], (1767 ^ _614856) ^ [_672926, _672928] : [ord_less_real(zero_zero_real, plus_plus_real(times_times_real(_672928, _672928), times_times_real(_672926, _672926))), _672928 = zero_zero_real, _672926 = zero_zero_real], (1785 ^ _614856) ^ [_673508, _673510] : [is_int(_673510), is_int(_673508), 1792 ^ _614856 : [(1803 ^ _614856) ^ [] : [1804 ^ _614856 : [(1805 ^ _614856) ^ [] : [-(_673510 = zero_zero_int)], (1807 ^ _614856) ^ [] : [-(_673508 = zero_zero_int)]], -(ord_less_int(zero_zero_int, plus_plus_int(times_times_int(_673510, _673510), times_times_int(_673508, _673508))))], (1793 ^ _614856) ^ [] : [ord_less_int(zero_zero_int, plus_plus_int(times_times_int(_673510, _673510), times_times_int(_673508, _673508))), _673510 = zero_zero_int, _673508 = zero_zero_int]]], (1811 ^ _614856) ^ [_674228, _674230] : [ord_less_real(plus_plus_real(times_times_real(_674230, _674230), times_times_real(_674228, _674228)), zero_zero_real)], (1813 ^ _614856) ^ [_674330, _674332] : [ord_less_int(plus_plus_int(times_times_int(_674332, _674332), times_times_int(_674330, _674330)), zero_zero_int)], (1815 ^ _614856) ^ [_674419] : [-(times_times_real(number267125858f_real(bit1(pls)), _674419) = _674419)], (1817 ^ _614856) ^ [_674515] : [is_int(_674515), -(times_times_int(number_number_of_int(bit1(pls)), _674515) = _674515)], (1823 ^ _614856) ^ [_674694] : [-(times_times_real(_674694, number267125858f_real(bit1(pls))) = _674694)], (1825 ^ _614856) ^ [_674790] : [is_int(_674790), -(times_times_int(_674790, number_number_of_int(bit1(pls))) = _674790)], (1831 ^ _614856) ^ [] : [-(one_one_int = number_number_of_int(bit1(pls)))], (1833 ^ _614856) ^ [_675036, _675038] : [-(times_times_int(bit1(_675038), _675036) = plus_plus_int(bit0(times_times_int(_675038, _675036)), _675036))], (1835 ^ _614856) ^ [_675158, _675160] : [is_int(_675160), is_int(_675158), ord_less_int(zero_zero_int, _675158), 1846 ^ _614856 : [(1847 ^ _614856) ^ [] : [times_times_int(_675158, _675160) = one_one_int, 1850 ^ _614856 : [(1851 ^ _614856) ^ [] : [-(_675158 = one_one_int)], (1853 ^ _614856) ^ [] : [-(_675160 = one_one_int)]]], (1855 ^ _614856) ^ [] : [-(times_times_int(_675158, _675160) = one_one_int), _675158 = one_one_int, _675160 = one_one_int]]], (1865 ^ _614856) ^ [_675976] : [plus_plus_real(_675976, _675976) = zero_zero_real, -(_675976 = zero_zero_real)], (1871 ^ _614856) ^ [_676138] : [_676138 = zero_zero_real, -(plus_plus_real(_676138, _676138) = zero_zero_real)], (1877 ^ _614856) ^ [_676336] : [is_int(_676336), 1880 ^ _614856 : [(1881 ^ _614856) ^ [] : [plus_plus_int(_676336, _676336) = zero_zero_int, -(_676336 = zero_zero_int)], (1887 ^ _614856) ^ [] : [_676336 = zero_zero_int, -(plus_plus_int(_676336, _676336) = zero_zero_int)]]], (1893 ^ _614856) ^ [_676757] : [bit1(_676757) = pls], (1895 ^ _614856) ^ [_676836] : [pls = bit1(_676836)], (1897 ^ _614856) ^ [_676929, _676931] : [bit1(_676931) = bit0(_676929)], (1899 ^ _614856) ^ [_677026, _677028] : [bit0(_677028) = bit1(_677026)], (1901 ^ _614856) ^ [_677125] : [is_int(_677125), 1904 ^ _614856 : [(1905 ^ _614856) ^ [] : [bit0(_677125) = pls, -(_677125 = pls)], (1911 ^ _614856) ^ [] : [_677125 = pls, -(bit0(_677125) = pls)]]], (1917 ^ _614856) ^ [_677559] : [is_int(_677559), 1920 ^ _614856 : [(1921 ^ _614856) ^ [] : [pls = bit0(_677559), -(pls = _677559)], (1927 ^ _614856) ^ [] : [pls = _677559, -(pls = bit0(_677559))]]], (1933 ^ _614856) ^ [] : [-(bit0(pls) = pls)], (1935 ^ _614856) ^ [] : [-(pls = zero_zero_int)], (1937 ^ _614856) ^ [_678142, _678144] : [ord_less_int(bit1(_678144), bit1(_678142)), -(ord_less_int(_678144, _678142))], (1943 ^ _614856) ^ [_678312, _678314] : [ord_less_int(_678314, _678312), -(ord_less_int(bit1(_678314), bit1(_678312)))], (1949 ^ _614856) ^ [_678561, _678563] : [ord_less_int(bit1(_678563), bit1(_678561)), -(ord_less_int(_678563, _678561))], (1955 ^ _614856) ^ [_678731, _678733] : [ord_less_int(_678733, _678731), -(ord_less_int(bit1(_678733), bit1(_678731)))], (1961 ^ _614856) ^ [] : [ord_less_int(pls, pls)], (1963 ^ _614856) ^ [_679032, _679034] : [ord_less_int(bit0(_679034), bit0(_679032)), -(ord_less_int(_679034, _679032))], (1969 ^ _614856) ^ [_679202, _679204] : [ord_less_int(_679204, _679202), -(ord_less_int(bit0(_679204), bit0(_679202)))], (1975 ^ _614856) ^ [_679451, _679453] : [ord_less_int(bit0(_679453), bit0(_679451)), -(ord_less_int(_679453, _679451))], (1981 ^ _614856) ^ [_679621, _679623] : [ord_less_int(_679623, _679621), -(ord_less_int(bit0(_679623), bit0(_679621)))], (1987 ^ _614856) ^ [] : [zero_zero_int = one_one_int], (1989 ^ _614856) ^ [_679879] : [is_int(_679879), -(plus_plus_int(_679879, pls) = _679879)], (1995 ^ _614856) ^ [_680073] : [is_int(_680073), -(plus_plus_int(pls, _680073) = _680073)], (2001 ^ _614856) ^ [_680266, _680268] : [-(plus_plus_int(bit0(_680268), bit0(_680266)) = bit0(plus_plus_int(_680268, _680266)))], (2003 ^ _614856) ^ [_680358] : [-(bit0(_680358) = plus_plus_int(_680358, _680358))], (2005 ^ _614856) ^ [_680456] : [is_int(_680456), -(plus_plus_int(_680456, zero_zero_int) = _680456)], (2011 ^ _614856) ^ [_680650] : [is_int(_680650), -(plus_plus_int(zero_zero_int, _680650) = _680650)], (2017 ^ _614856) ^ [_680872, _680874, _680876] : [ord_less_int(_680874, _680872), -(ord_less_int(plus_plus_int(_680874, _680876), plus_plus_int(_680872, _680876)))], (2023 ^ _614856) ^ [_681071] : [-(times_times_real(plus_plus_real(one_one_real, one_one_real), number267125858f_real(_681071)) = number267125858f_real(bit0(_681071)))], (2025 ^ _614856) ^ [_681158] : [-(times_times_int(plus_plus_int(one_one_int, one_one_int), number_number_of_int(_681158)) = number_number_of_int(bit0(_681158)))], (2027 ^ _614856) ^ [_681245] : [-(power_power_real(_681245, number_number_of_nat(bit1(bit1(pls)))) = times_times_real(times_times_real(_681245, _681245), _681245))], (2029 ^ _614856) ^ [_681332] : [-(power_power_nat(_681332, number_number_of_nat(bit1(bit1(pls)))) = times_times_nat(times_times_nat(_681332, _681332), _681332))], (2031 ^ _614856) ^ [_681419] : [-(power_power_int(_681419, number_number_of_nat(bit1(bit1(pls)))) = times_times_int(times_times_int(_681419, _681419), _681419))], (2033 ^ _614856) ^ [_681506] : [-(times_times_real(number267125858f_real(bit0(bit1(pls))), _681506) = plus_plus_real(_681506, _681506))], (2035 ^ _614856) ^ [_681590] : [-(times_times_nat(number_number_of_nat(bit0(bit1(pls))), _681590) = plus_plus_nat(_681590, _681590))], (2037 ^ _614856) ^ [_681674] : [-(times_times_int(number_number_of_int(bit0(bit1(pls))), _681674) = plus_plus_int(_681674, _681674))], (2039 ^ _614856) ^ [_681758] : [-(times_times_real(number267125858f_real(bit0(bit1(pls))), _681758) = plus_plus_real(_681758, _681758))], (2041 ^ _614856) ^ [_681842] : [-(times_times_int(number_number_of_int(bit0(bit1(pls))), _681842) = plus_plus_int(_681842, _681842))], (2043 ^ _614856) ^ [_681926] : [-(times_times_real(_681926, number267125858f_real(bit0(bit1(pls)))) = plus_plus_real(_681926, _681926))], (2045 ^ _614856) ^ [_682010] : [-(times_times_nat(_682010, number_number_of_nat(bit0(bit1(pls)))) = plus_plus_nat(_682010, _682010))], (2047 ^ _614856) ^ [_682094] : [-(times_times_int(_682094, number_number_of_int(bit0(bit1(pls)))) = plus_plus_int(_682094, _682094))], (2049 ^ _614856) ^ [_682178] : [-(times_times_real(_682178, number267125858f_real(bit0(bit1(pls)))) = plus_plus_real(_682178, _682178))], (2051 ^ _614856) ^ [_682262] : [-(times_times_int(_682262, number_number_of_int(bit0(bit1(pls)))) = plus_plus_int(_682262, _682262))], (2053 ^ _614856) ^ [_682346] : [-(power_power_real(_682346, number_number_of_nat(bit0(bit1(pls)))) = times_times_real(_682346, _682346))], (2055 ^ _614856) ^ [_682430] : [-(power_power_nat(_682430, number_number_of_nat(bit0(bit1(pls)))) = times_times_nat(_682430, _682430))], (2057 ^ _614856) ^ [_682514] : [-(power_power_int(_682514, number_number_of_nat(bit0(bit1(pls)))) = times_times_int(_682514, _682514))], (2059 ^ _614856) ^ [_682642] : [ord_less_real(plus_plus_real(_682642, _682642), zero_zero_real), -(ord_less_real(_682642, zero_zero_real))], (2065 ^ _614856) ^ [_682804] : [ord_less_real(_682804, zero_zero_real), -(ord_less_real(plus_plus_real(_682804, _682804), zero_zero_real))], (2071 ^ _614856) ^ [_683031] : [ord_less_int(plus_plus_int(_683031, _683031), zero_zero_int), -(ord_less_int(_683031, zero_zero_int))], (2077 ^ _614856) ^ [_683193] : [ord_less_int(_683193, zero_zero_int), -(ord_less_int(plus_plus_int(_683193, _683193), zero_zero_int))], (2083 ^ _614856) ^ [] : [-(number267125858f_real(pls) = zero_zero_real)], (2085 ^ _614856) ^ [] : [-(number_number_of_nat(pls) = zero_zero_nat)], (2087 ^ _614856) ^ [] : [-(number_number_of_int(pls) = zero_zero_int)], (2089 ^ _614856) ^ [] : [-(number267125858f_real(pls) = zero_zero_real)], (2091 ^ _614856) ^ [] : [-(number_number_of_int(pls) = zero_zero_int)], (2093 ^ _614856) ^ [] : [-(zero_zero_real = number267125858f_real(pls))], (2095 ^ _614856) ^ [] : [-(zero_zero_int = number_number_of_int(pls))], (2097 ^ _614856) ^ [_683747] : [-(plus_plus_real(number267125858f_real(pls), _683747) = _683747)], (2099 ^ _614856) ^ [_683843] : [is_int(_683843), -(plus_plus_int(number_number_of_int(pls), _683843) = _683843)], (2105 ^ _614856) ^ [_684022] : [-(plus_plus_real(_684022, number267125858f_real(pls)) = _684022)], (2107 ^ _614856) ^ [_684118] : [is_int(_684118), -(plus_plus_int(_684118, number_number_of_int(pls)) = _684118)], (2113 ^ _614856) ^ [_684355, _684357] : [ord_less_real(number267125858f_real(_684357), number267125858f_real(_684355)), -(ord_less_int(_684357, _684355))], (2119 ^ _614856) ^ [_684525, _684527] : [ord_less_int(_684527, _684525), -(ord_less_real(number267125858f_real(_684527), number267125858f_real(_684525)))], (2125 ^ _614856) ^ [_684774, _684776] : [ord_less_int(number_number_of_int(_684776), number_number_of_int(_684774)), -(ord_less_int(_684776, _684774))], (2131 ^ _614856) ^ [_684944, _684946] : [ord_less_int(_684946, _684944), -(ord_less_int(number_number_of_int(_684946), number_number_of_int(_684944)))], (2137 ^ _614856) ^ [_685163, _685165, _685167] : [-(plus_plus_real(number267125858f_real(_685167), plus_plus_real(number267125858f_real(_685165), _685163)) = plus_plus_real(number267125858f_real(plus_plus_int(_685167, _685165)), _685163))], (2139 ^ _614856) ^ [_685291, _685293, _685295] : [-(plus_plus_int(number_number_of_int(_685295), plus_plus_int(number_number_of_int(_685293), _685291)) = plus_plus_int(number_number_of_int(plus_plus_int(_685295, _685293)), _685291))], (2141 ^ _614856) ^ [_685405, _685407] : [-(plus_plus_real(number267125858f_real(_685407), number267125858f_real(_685405)) = number267125858f_real(plus_plus_int(_685407, _685405)))], (2143 ^ _614856) ^ [_685511, _685513] : [-(plus_plus_int(number_number_of_int(_685513), number_number_of_int(_685511)) = number_number_of_int(plus_plus_int(_685513, _685511)))], (2145 ^ _614856) ^ [_685617, _685619] : [-(number267125858f_real(plus_plus_int(_685619, _685617)) = plus_plus_real(number267125858f_real(_685619), number267125858f_real(_685617)))], (2147 ^ _614856) ^ [_685723, _685725] : [-(number_number_of_int(plus_plus_int(_685725, _685723)) = plus_plus_int(number_number_of_int(_685725), number_number_of_int(_685723)))], (2149 ^ _614856) ^ [_685859] : [ord_less_int(bit1(_685859), pls), -(ord_less_int(_685859, pls))], (2155 ^ _614856) ^ [_686019] : [ord_less_int(_686019, pls), -(ord_less_int(bit1(_686019), pls))], (2161 ^ _614856) ^ [_686258, _686260] : [ord_less_int(bit1(_686260), bit0(_686258)), -(ord_less_int(_686260, _686258))], (2167 ^ _614856) ^ [_686428, _686430] : [ord_less_int(_686430, _686428), -(ord_less_int(bit1(_686430), bit0(_686428)))], (2173 ^ _614856) ^ [_686677, _686679] : [ord_less_int(bit1(_686679), bit0(_686677)), -(ord_less_int(_686679, _686677))], (2179 ^ _614856) ^ [_686847, _686849] : [ord_less_int(_686849, _686847), -(ord_less_int(bit1(_686849), bit0(_686847)))], (2185 ^ _614856) ^ [_687082] : [ord_less_int(bit1(_687082), zero_zero_int), -(ord_less_int(_687082, zero_zero_int))], (2191 ^ _614856) ^ [_687242] : [ord_less_int(_687242, zero_zero_int), -(ord_less_int(bit1(_687242), zero_zero_int))], (2197 ^ _614856) ^ [_687467] : [ord_less_int(bit0(_687467), pls), -(ord_less_int(_687467, pls))], (2203 ^ _614856) ^ [_687627] : [ord_less_int(_687627, pls), -(ord_less_int(bit0(_687627), pls))], (2209 ^ _614856) ^ [_687852] : [ord_less_int(pls, bit0(_687852)), -(ord_less_int(pls, _687852))], (2215 ^ _614856) ^ [_688012] : [ord_less_int(pls, _688012), -(ord_less_int(pls, bit0(_688012)))], (2221 ^ _614856) ^ [] : [ord_less_int(pls, zero_zero_int)], (2223 ^ _614856) ^ [_688289] : [ord_less_int(bit0(_688289), zero_zero_int), -(ord_less_int(_688289, zero_zero_int))], (2229 ^ _614856) ^ [_688449] : [ord_less_int(_688449, zero_zero_int), -(ord_less_int(bit0(_688449), zero_zero_int))], (2235 ^ _614856) ^ [_688644, _688646] : [-(plus_plus_int(bit1(_688646), bit0(_688644)) = bit1(plus_plus_int(_688646, _688644)))], (2237 ^ _614856) ^ [_688750, _688752] : [-(plus_plus_int(bit0(_688752), bit1(_688750)) = bit1(plus_plus_int(_688752, _688750)))], (2239 ^ _614856) ^ [] : [-(ord_less_int(zero_zero_int, one_one_int))], (2241 ^ _614856) ^ [_688895] : [-(bit1(_688895) = plus_plus_int(plus_plus_int(one_one_int, _688895), _688895))], (2243 ^ _614856) ^ [_688980] : [plus_plus_int(plus_plus_int(one_one_int, _688980), _688980) = zero_zero_int], (2245 ^ _614856) ^ [_689093, _689095] : [is_int(_689095), is_int(_689093), 2252 ^ _614856 : [(2263 ^ _614856) ^ [] : [2264 ^ _614856 : [(2265 ^ _614856) ^ [] : [ord_less_int(_689095, _689093)], (2267 ^ _614856) ^ [] : [_689095 = _689093]], -(ord_less_int(_689095, plus_plus_int(_689093, one_one_int)))], (2253 ^ _614856) ^ [] : [ord_less_int(_689095, plus_plus_int(_689093, one_one_int)), -(ord_less_int(_689095, _689093)), -(_689095 = _689093)]]], (2271 ^ _614856) ^ [_689778] : [-(power_power_real(number267125858f_real(_689778), number_number_of_nat(bit0(bit1(pls)))) = times_times_real(number267125858f_real(_689778), number267125858f_real(_689778)))], (2273 ^ _614856) ^ [_689868] : [-(power_power_nat(number_number_of_nat(_689868), number_number_of_nat(bit0(bit1(pls)))) = times_times_nat(number_number_of_nat(_689868), number_number_of_nat(_689868)))], (2275 ^ _614856) ^ [_689958] : [-(power_power_int(number_number_of_int(_689958), number_number_of_nat(bit0(bit1(pls)))) = times_times_int(number_number_of_int(_689958), number_number_of_int(_689958)))], (2277 ^ _614856) ^ [_690062, _690064] : [-(power_power_real(plus_plus_real(_690064, _690062), number_number_of_nat(bit0(bit1(pls)))) = plus_plus_real(plus_plus_real(power_power_real(_690064, number_number_of_nat(bit0(bit1(pls)))), power_power_real(_690062, number_number_of_nat(bit0(bit1(pls))))), times_times_real(times_times_real(number267125858f_real(bit0(bit1(pls))), _690064), _690062)))], (2279 ^ _614856) ^ [_690180, _690182] : [-(power_power_nat(plus_plus_nat(_690182, _690180), number_number_of_nat(bit0(bit1(pls)))) = plus_plus_nat(plus_plus_nat(power_power_nat(_690182, number_number_of_nat(bit0(bit1(pls)))), power_power_nat(_690180, number_number_of_nat(bit0(bit1(pls))))), times_times_nat(times_times_nat(number_number_of_nat(bit0(bit1(pls))), _690182), _690180)))], (2281 ^ _614856) ^ [_690298, _690300] : [-(power_power_int(plus_plus_int(_690300, _690298), number_number_of_nat(bit0(bit1(pls)))) = plus_plus_int(plus_plus_int(power_power_int(_690300, number_number_of_nat(bit0(bit1(pls)))), power_power_int(_690298, number_number_of_nat(bit0(bit1(pls))))), times_times_int(times_times_int(number_number_of_int(bit0(bit1(pls))), _690300), _690298)))], (2283 ^ _614856) ^ [_690402] : [-(number267125858f_real(bit0(_690402)) = plus_plus_real(plus_plus_real(zero_zero_real, number267125858f_real(_690402)), number267125858f_real(_690402)))], (2285 ^ _614856) ^ [_690494] : [-(number_number_of_int(bit0(_690494)) = plus_plus_int(plus_plus_int(zero_zero_int, number_number_of_int(_690494)), number_number_of_int(_690494)))], (2287 ^ _614856) ^ [_690586] : [-(number267125858f_real(bit1(_690586)) = plus_plus_real(plus_plus_real(one_one_real, number267125858f_real(_690586)), number267125858f_real(_690586)))], (2289 ^ _614856) ^ [_690678] : [-(number_number_of_int(bit1(_690678)) = plus_plus_int(plus_plus_int(one_one_int, number_number_of_int(_690678)), number_number_of_int(_690678)))], (2291 ^ _614856) ^ [] : [-(number267125858f_real(bit1(pls)) = one_one_real)], (2293 ^ _614856) ^ [] : [-(number_number_of_nat(bit1(pls)) = one_one_nat)], (2295 ^ _614856) ^ [] : [-(number_number_of_int(bit1(pls)) = one_one_int)], (2297 ^ _614856) ^ [] : [-(number267125858f_real(bit1(pls)) = one_one_real)], (2299 ^ _614856) ^ [] : [-(number_number_of_int(bit1(pls)) = one_one_int)], (2301 ^ _614856) ^ [] : [-(one_one_real = number267125858f_real(bit1(pls)))], (2303 ^ _614856) ^ [] : [-(one_one_int = number_number_of_int(bit1(pls)))], (2305 ^ _614856) ^ [_691185] : [ord_less_int(plus_plus_int(plus_plus_int(one_one_int, _691185), _691185), zero_zero_int), -(ord_less_int(_691185, zero_zero_int))], (2311 ^ _614856) ^ [_691353] : [ord_less_int(_691353, zero_zero_int), -(ord_less_int(plus_plus_int(plus_plus_int(one_one_int, _691353), _691353), zero_zero_int))], (2317 ^ _614856) ^ [_691586] : [ord_less_real(number267125858f_real(_691586), zero_zero_real), -(ord_less_int(_691586, pls))], (2323 ^ _614856) ^ [_691746] : [ord_less_int(_691746, pls), -(ord_less_real(number267125858f_real(_691746), zero_zero_real))], (2329 ^ _614856) ^ [_691971] : [ord_less_int(number_number_of_int(_691971), zero_zero_int), -(ord_less_int(_691971, pls))], (2335 ^ _614856) ^ [_692131] : [ord_less_int(_692131, pls), -(ord_less_int(number_number_of_int(_692131), zero_zero_int))], (2341 ^ _614856) ^ [_692356] : [ord_less_real(zero_zero_real, number267125858f_real(_692356)), -(ord_less_int(pls, _692356))], (2347 ^ _614856) ^ [_692516] : [ord_less_int(pls, _692516), -(ord_less_real(zero_zero_real, number267125858f_real(_692516)))], (2353 ^ _614856) ^ [_692741] : [ord_less_int(zero_zero_int, number_number_of_int(_692741)), -(ord_less_int(pls, _692741))], (2359 ^ _614856) ^ [_692901] : [ord_less_int(pls, _692901), -(ord_less_int(zero_zero_int, number_number_of_int(_692901)))], (2365 ^ _614856) ^ [] : [-(plus_plus_real(one_one_real, one_one_real) = number267125858f_real(bit0(bit1(pls))))], (2367 ^ _614856) ^ [] : [-(plus_plus_nat(one_one_nat, one_one_nat) = number_number_of_nat(bit0(bit1(pls))))], (2369 ^ _614856) ^ [] : [-(plus_plus_int(one_one_int, one_one_int) = number_number_of_int(bit0(bit1(pls))))], (2371 ^ _614856) ^ [] : [-(plus_plus_real(one_one_real, one_one_real) = number267125858f_real(bit0(bit1(pls))))], (2373 ^ _614856) ^ [] : [-(plus_plus_int(one_one_int, one_one_int) = number_number_of_int(bit0(bit1(pls))))], (2375 ^ _614856) ^ [_693391] : [ord_less_real(number267125858f_real(_693391), one_one_real), -(ord_less_int(_693391, bit1(pls)))], (2381 ^ _614856) ^ [_693551] : [ord_less_int(_693551, bit1(pls)), -(ord_less_real(number267125858f_real(_693551), one_one_real))], (2387 ^ _614856) ^ [_693776] : [ord_less_int(number_number_of_int(_693776), one_one_int), -(ord_less_int(_693776, bit1(pls)))], (2393 ^ _614856) ^ [_693936] : [ord_less_int(_693936, bit1(pls)), -(ord_less_int(number_number_of_int(_693936), one_one_int))], (2399 ^ _614856) ^ [_694161] : [ord_less_real(one_one_real, number267125858f_real(_694161)), -(ord_less_int(bit1(pls), _694161))], (2405 ^ _614856) ^ [_694321] : [ord_less_int(bit1(pls), _694321), -(ord_less_real(one_one_real, number267125858f_real(_694321)))], (2411 ^ _614856) ^ [_694546] : [ord_less_int(one_one_int, number_number_of_int(_694546)), -(ord_less_int(bit1(pls), _694546))], (2417 ^ _614856) ^ [_694706] : [ord_less_int(bit1(pls), _694706), -(ord_less_int(one_one_int, number_number_of_int(_694706)))], (2423 ^ _614856) ^ [] : [-(dvd_dvd_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), m), one_one_int), plus_plus_int(power_power_int(s, number_number_of_nat(bit0(bit1(pls)))), one_one_int)))], (2425 ^ _614856) ^ [_694954, _694956] : [-(power_power_int(plus_plus_int(_694956, _694954), number_number_of_nat(bit1(bit1(pls)))) = plus_plus_int(plus_plus_int(plus_plus_int(power_power_int(_694956, number_number_of_nat(bit1(bit1(pls)))), times_times_int(times_times_int(number_number_of_int(bit1(bit1(pls))), power_power_int(_694956, number_number_of_nat(bit0(bit1(pls))))), _694954)), times_times_int(times_times_int(number_number_of_int(bit1(bit1(pls))), _694956), power_power_int(_694954, number_number_of_nat(bit0(bit1(pls)))))), power_power_int(_694954, number_number_of_nat(bit1(bit1(pls))))))], (2427 ^ _614856) ^ [_695087, _695089] : [-(power_power_int(plus_plus_int(_695089, _695087), number_number_of_nat(bit0(bit1(pls)))) = plus_plus_int(plus_plus_int(power_power_int(_695089, number_number_of_nat(bit0(bit1(pls)))), times_times_int(times_times_int(number_number_of_int(bit0(bit1(pls))), _695089), _695087)), power_power_int(_695087, number_number_of_nat(bit0(bit1(pls))))))], (2429 ^ _614856) ^ [_695206] : [is_int(_695206), ord_less_eq_int(zero_zero_int, _695206), ord_less_int(_695206, number_number_of_int(bit0(bit1(pls)))), -(_695206 = zero_zero_int), -(_695206 = one_one_int)], (2447 ^ _614856) ^ [] : [-(ord_less_eq_int(zero_zero_int, s))], (2449 ^ _614856) ^ [] : [-(ord_less_int(s, plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), m), one_one_int)))], (2451 ^ _614856) ^ [] : [-(zcong(s1, s, plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), m), one_one_int)))], (2453 ^ _614856) ^ [_695798] : [-(times_times_int(_695798, power_power_int(_695798, number_number_of_nat(bit0(bit1(pls))))) = power_power_int(_695798, number_number_of_nat(bit1(bit1(pls)))))], (2455 ^ _614856) ^ [_695885] : [-(ord_less_eq_int(_695885, power_power_int(_695885, number_number_of_nat(bit0(bit1(pls))))))], (2457 ^ _614856) ^ [_696009, _696011, _696013] : [ord_less_int(zero_zero_int, _696009), _696009 = plus_plus_int(_696013, times_times_int(_696009, _696011)), ord_less_int(_696013, _696009), -(ord_less_eq_int(one_one_int, _696011))], (2471 ^ _614856) ^ [_696437, _696439, _696441] : [ord_less_int(zero_zero_int, _696437), _696437 = plus_plus_int(_696441, times_times_int(_696437, _696439)), ord_less_eq_int(zero_zero_int, _696441), -(ord_less_eq_int(_696439, one_one_int))], (2485 ^ _614856) ^ [] : [-(ord_less_eq_int(zero_zero_int, number_number_of_int(bit0(bit1(pls)))))], (2487 ^ _614856) ^ [_696889, _696891] : [-(power_power_real(_696891, times_times_nat(number_number_of_nat(bit0(bit1(pls))), _696889)) = times_times_real(power_power_real(_696891, _696889), power_power_real(_696891, _696889)))], (2489 ^ _614856) ^ [_696998, _697000] : [-(power_power_nat(_697000, times_times_nat(number_number_of_nat(bit0(bit1(pls))), _696998)) = times_times_nat(power_power_nat(_697000, _696998), power_power_nat(_697000, _696998)))], (2491 ^ _614856) ^ [_697107, _697109] : [-(power_power_int(_697109, times_times_nat(number_number_of_nat(bit0(bit1(pls))), _697107)) = times_times_int(power_power_int(_697109, _697107), power_power_int(_697109, _697107)))], (2493 ^ _614856) ^ [] : [-(zcong(power_power_int(s, number_number_of_nat(bit0(bit1(pls)))), power_power_int(s1, number_number_of_nat(bit0(bit1(pls)))), plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), m), one_one_int)))], (2496 ^ _614856) ^ [] : [-(is_int(2494 ^ []))], (2498 ^ _614856) ^ [] : [-(ord_less_eq_int(zero_zero_int, 2494 ^ []))], (2500 ^ _614856) ^ [] : [-(ord_less_int(2494 ^ [], plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), m), one_one_int)))], (2502 ^ _614856) ^ [] : [-(zcong(s1, 2494 ^ [], plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), m), one_one_int)))], (2504 ^ _614856) ^ [_697572] : [is_int(_697572), -(_697572 = 2494 ^ []), ord_less_eq_int(zero_zero_int, _697572), ord_less_int(_697572, plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), m), one_one_int)), zcong(s1, _697572, plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), m), one_one_int))], (2523 ^ _614856) ^ [] : [-(is_int(2521 ^ []))], (2525 ^ _614856) ^ [] : [-(ord_less_eq_int(zero_zero_int, 2521 ^ []))], (2527 ^ _614856) ^ [] : [-(ord_less_int(2521 ^ [], plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), m), one_one_int)))], (2529 ^ _614856) ^ [] : [-(zcong(s1, 2521 ^ [], plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), m), one_one_int)))], (2531 ^ _614856) ^ [] : [-(zcong(power_power_int(s1, number_number_of_nat(bit0(bit1(pls)))), number_number_of_int(min), plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), m), one_one_int)))], (2543 ^ _614856) ^ [_698654, _698656] : [2544 ^ _614856 : [(2545 ^ _614856) ^ [] : [_698654 = zero_zero_nat], (2547 ^ _614856) ^ [] : [ord_less_nat(zero_zero_nat, _698656)]], -(ord_less_nat(zero_zero_nat, power_power_nat(_698656, _698654)))], (2533 ^ _614856) ^ [_698396, _698398] : [ord_less_nat(zero_zero_nat, power_power_nat(_698398, _698396)), -(_698396 = zero_zero_nat), -(ord_less_nat(zero_zero_nat, _698398))], (2551 ^ _614856) ^ [_698960, _698962, _698964] : [zprime(_698960), dvd_dvd_int(_698960, power_power_int(_698964, _698962)), -(dvd_dvd_int(_698960, _698964))], (2561 ^ _614856) ^ [_699272, _699274, _699276] : [-(power_power_real(power_power_real(_699276, _699274), _699272) = power_power_real(_699276, times_times_nat(_699274, _699272)))], (2563 ^ _614856) ^ [_699394, _699396, _699398] : [-(power_power_nat(power_power_nat(_699398, _699396), _699394) = power_power_nat(_699398, times_times_nat(_699396, _699394)))], (2565 ^ _614856) ^ [_699516, _699518, _699520] : [-(power_power_int(power_power_int(_699520, _699518), _699516) = power_power_int(_699520, times_times_nat(_699518, _699516)))], (2567 ^ _614856) ^ [_699667, _699669, _699671, _699673] : [zprime(_699667), -(dvd_dvd_int(_699667, _699669)), dvd_dvd_int(power_power_int(_699667, _699673), times_times_int(_699671, _699669)), -(dvd_dvd_int(power_power_int(_699667, _699673), _699671))], (2581 ^ _614856) ^ [_700130, _700132, _700134, _700136] : [zprime(_700130), -(dvd_dvd_int(_700130, _700132)), dvd_dvd_int(power_power_int(_700130, _700136), times_times_int(_700132, _700134)), -(dvd_dvd_int(power_power_int(_700130, _700136), _700134))], (2595 ^ _614856) ^ [_700564, _700566, _700568] : [-(power_power_int(power_power_int(_700568, _700566), _700564) = power_power_int(_700568, times_times_nat(_700566, _700564)))], (2597 ^ _614856) ^ [_700687, _700689] : [ord_less_int(zero_zero_int, _700687), ord_less_int(_700687, _700689), dvd_dvd_int(_700689, _700687)], (2607 ^ _614856) ^ [_700987, _700989] : [is_int(_700989), is_int(_700987), ord_less_eq_int(zero_zero_int, _700987), ord_less_eq_int(zero_zero_int, _700989), dvd_dvd_int(_700987, _700989), dvd_dvd_int(_700989, _700987), -(_700987 = _700989)], (2633 ^ _614856) ^ [_701654, _701656, _701658] : [is_int(_701658), dvd_dvd_int(times_times_int(_701658, _701656), times_times_int(_701658, _701654)), -(_701658 = zero_zero_int), -(dvd_dvd_int(_701656, _701654))], (2647 ^ _614856) ^ [_702112, _702114, _702116] : [dvd_dvd_int(_702116, plus_plus_int(_702114, times_times_int(_702116, _702112))), -(dvd_dvd_int(_702116, _702114))], (2653 ^ _614856) ^ [_702292, _702294, _702296] : [dvd_dvd_int(_702296, _702294), -(dvd_dvd_int(_702296, plus_plus_int(_702294, times_times_int(_702296, _702292))))], (2659 ^ _614856) ^ [_702564, _702566, _702568, _702570, _702572] : [dvd_dvd_int(_702566, _702564), 2662 ^ _614856 : [(2663 ^ _614856) ^ [] : [dvd_dvd_int(_702566, plus_plus_int(_702570, _702568)), -(dvd_dvd_int(_702566, plus_plus_int(plus_plus_int(_702570, times_times_int(_702572, _702564)), _702568)))], (2669 ^ _614856) ^ [] : [dvd_dvd_int(_702566, plus_plus_int(plus_plus_int(_702570, times_times_int(_702572, _702564)), _702568)), -(dvd_dvd_int(_702566, plus_plus_int(_702570, _702568)))]]], (2675 ^ _614856) ^ [] : [-(zprime(number_number_of_int(bit0(bit1(pls)))))], (2677 ^ _614856) ^ [_703161, _703163] : [dvd_dvd_int(_703163, _703161), ord_less_int(zero_zero_int, _703161), -(ord_less_eq_int(_703163, _703161))], (2687 ^ _614856) ^ [_703460, _703462] : [twoSqu142715416sum2sq(_703460), twoSqu142715416sum2sq(_703462), -(twoSqu142715416sum2sq(times_times_int(_703460, _703462)))], (2707 ^ _614856) ^ [_704050, _704052] : [2708 ^ _614856 : [(2709 ^ _614856) ^ [] : [ord_less_eq_int(_704052, _704050)], (2711 ^ _614856) ^ [] : [ord_less_eq_int(_704052, pls)]], -(ord_less_eq_nat(number_number_of_nat(_704052), number_number_of_nat(_704050)))], (2697 ^ _614856) ^ [_703788, _703790] : [ord_less_eq_nat(number_number_of_nat(_703790), number_number_of_nat(_703788)), -(ord_less_eq_int(_703790, _703788)), -(ord_less_eq_int(_703790, pls))], (2715 ^ _614856) ^ [_704359, _704361, _704363, _704365] : [-(times_times_real(times_times_real(_704365, _704363), times_times_real(_704361, _704359)) = times_times_real(times_times_real(_704365, _704361), times_times_real(_704363, _704359)))], (2717 ^ _614856) ^ [_704503, _704505, _704507, _704509] : [-(times_times_nat(times_times_nat(_704509, _704507), times_times_nat(_704505, _704503)) = times_times_nat(times_times_nat(_704509, _704505), times_times_nat(_704507, _704503)))], (2719 ^ _614856) ^ [_704647, _704649, _704651, _704653] : [-(times_times_int(times_times_int(_704653, _704651), times_times_int(_704649, _704647)) = times_times_int(times_times_int(_704653, _704649), times_times_int(_704651, _704647)))], (2721 ^ _614856) ^ [_704791, _704793, _704795, _704797] : [-(times_times_real(times_times_real(_704797, _704795), times_times_real(_704793, _704791)) = times_times_real(_704793, times_times_real(times_times_real(_704797, _704795), _704791)))], (2723 ^ _614856) ^ [_704935, _704937, _704939, _704941] : [-(times_times_nat(times_times_nat(_704941, _704939), times_times_nat(_704937, _704935)) = times_times_nat(_704937, times_times_nat(times_times_nat(_704941, _704939), _704935)))], (2725 ^ _614856) ^ [_705079, _705081, _705083, _705085] : [-(times_times_int(times_times_int(_705085, _705083), times_times_int(_705081, _705079)) = times_times_int(_705081, times_times_int(times_times_int(_705085, _705083), _705079)))], (2727 ^ _614856) ^ [_705223, _705225, _705227, _705229] : [-(times_times_real(times_times_real(_705229, _705227), times_times_real(_705225, _705223)) = times_times_real(_705229, times_times_real(_705227, times_times_real(_705225, _705223))))], (2729 ^ _614856) ^ [_705367, _705369, _705371, _705373] : [-(times_times_nat(times_times_nat(_705373, _705371), times_times_nat(_705369, _705367)) = times_times_nat(_705373, times_times_nat(_705371, times_times_nat(_705369, _705367))))], (2731 ^ _614856) ^ [_705511, _705513, _705515, _705517] : [-(times_times_int(times_times_int(_705517, _705515), times_times_int(_705513, _705511)) = times_times_int(_705517, times_times_int(_705515, times_times_int(_705513, _705511))))], (2733 ^ _614856) ^ [_705641, _705643, _705645] : [-(times_times_real(times_times_real(_705645, _705643), _705641) = times_times_real(times_times_real(_705645, _705641), _705643))], (2735 ^ _614856) ^ [_705763, _705765, _705767] : [-(times_times_nat(times_times_nat(_705767, _705765), _705763) = times_times_nat(times_times_nat(_705767, _705763), _705765))], (2737 ^ _614856) ^ [_705885, _705887, _705889] : [-(times_times_int(times_times_int(_705889, _705887), _705885) = times_times_int(times_times_int(_705889, _705885), _705887))], (2739 ^ _614856) ^ [_706007, _706009, _706011] : [-(times_times_real(times_times_real(_706011, _706009), _706007) = times_times_real(_706011, times_times_real(_706009, _706007)))], (2741 ^ _614856) ^ [_706129, _706131, _706133] : [-(times_times_nat(times_times_nat(_706133, _706131), _706129) = times_times_nat(_706133, times_times_nat(_706131, _706129)))], (2743 ^ _614856) ^ [_706251, _706253, _706255] : [-(times_times_int(times_times_int(_706255, _706253), _706251) = times_times_int(_706255, times_times_int(_706253, _706251)))], (2745 ^ _614856) ^ [_706373, _706375, _706377] : [-(times_times_real(_706377, times_times_real(_706375, _706373)) = times_times_real(times_times_real(_706377, _706375), _706373))], (2747 ^ _614856) ^ [_706495, _706497, _706499] : [-(times_times_nat(_706499, times_times_nat(_706497, _706495)) = times_times_nat(times_times_nat(_706499, _706497), _706495))], (2749 ^ _614856) ^ [_706617, _706619, _706621] : [-(times_times_int(_706621, times_times_int(_706619, _706617)) = times_times_int(times_times_int(_706621, _706619), _706617))], (2751 ^ _614856) ^ [_706739, _706741, _706743] : [-(times_times_real(_706743, times_times_real(_706741, _706739)) = times_times_real(_706741, times_times_real(_706743, _706739)))], (2753 ^ _614856) ^ [_706861, _706863, _706865] : [-(times_times_nat(_706865, times_times_nat(_706863, _706861)) = times_times_nat(_706863, times_times_nat(_706865, _706861)))], (2755 ^ _614856) ^ [_706983, _706985, _706987] : [-(times_times_int(_706987, times_times_int(_706985, _706983)) = times_times_int(_706985, times_times_int(_706987, _706983)))], (2757 ^ _614856) ^ [_707091, _707093] : [-(times_times_real(_707093, _707091) = times_times_real(_707091, _707093))], (2759 ^ _614856) ^ [_707191, _707193] : [-(times_times_nat(_707193, _707191) = times_times_nat(_707191, _707193))], (2761 ^ _614856) ^ [_707291, _707293] : [-(times_times_int(_707293, _707291) = times_times_int(_707291, _707293))], (2763 ^ _614856) ^ [_707391, _707393] : [-(plus_plus_real(_707393, _707391) = plus_plus_real(_707391, _707393))], (2765 ^ _614856) ^ [_707491, _707493] : [-(plus_plus_nat(_707493, _707491) = plus_plus_nat(_707491, _707493))], (2767 ^ _614856) ^ [_707591, _707593] : [-(plus_plus_int(_707593, _707591) = plus_plus_int(_707591, _707593))], (2769 ^ _614856) ^ [_707705, _707707, _707709] : [-(plus_plus_real(_707709, plus_plus_real(_707707, _707705)) = plus_plus_real(_707707, plus_plus_real(_707709, _707705)))], (2771 ^ _614856) ^ [_707827, _707829, _707831] : [-(plus_plus_nat(_707831, plus_plus_nat(_707829, _707827)) = plus_plus_nat(_707829, plus_plus_nat(_707831, _707827)))], (2773 ^ _614856) ^ [_707949, _707951, _707953] : [-(plus_plus_int(_707953, plus_plus_int(_707951, _707949)) = plus_plus_int(_707951, plus_plus_int(_707953, _707949)))], (2775 ^ _614856) ^ [_708071, _708073, _708075] : [-(plus_plus_real(_708075, plus_plus_real(_708073, _708071)) = plus_plus_real(plus_plus_real(_708075, _708073), _708071))], (2777 ^ _614856) ^ [_708193, _708195, _708197] : [-(plus_plus_nat(_708197, plus_plus_nat(_708195, _708193)) = plus_plus_nat(plus_plus_nat(_708197, _708195), _708193))], (2779 ^ _614856) ^ [_708315, _708317, _708319] : [-(plus_plus_int(_708319, plus_plus_int(_708317, _708315)) = plus_plus_int(plus_plus_int(_708319, _708317), _708315))], (2781 ^ _614856) ^ [_708437, _708439, _708441] : [-(plus_plus_real(plus_plus_real(_708441, _708439), _708437) = plus_plus_real(_708441, plus_plus_real(_708439, _708437)))], (2783 ^ _614856) ^ [_708559, _708561, _708563] : [-(plus_plus_nat(plus_plus_nat(_708563, _708561), _708559) = plus_plus_nat(_708563, plus_plus_nat(_708561, _708559)))], (2785 ^ _614856) ^ [_708681, _708683, _708685] : [-(plus_plus_int(plus_plus_int(_708685, _708683), _708681) = plus_plus_int(_708685, plus_plus_int(_708683, _708681)))], (2787 ^ _614856) ^ [_708803, _708805, _708807] : [-(plus_plus_real(plus_plus_real(_708807, _708805), _708803) = plus_plus_real(plus_plus_real(_708807, _708803), _708805))], (2789 ^ _614856) ^ [_708925, _708927, _708929] : [-(plus_plus_nat(plus_plus_nat(_708929, _708927), _708925) = plus_plus_nat(plus_plus_nat(_708929, _708925), _708927))], (2791 ^ _614856) ^ [_709047, _709049, _709051] : [-(plus_plus_int(plus_plus_int(_709051, _709049), _709047) = plus_plus_int(plus_plus_int(_709051, _709047), _709049))], (2793 ^ _614856) ^ [_709183, _709185, _709187, _709189] : [-(plus_plus_real(plus_plus_real(_709189, _709187), plus_plus_real(_709185, _709183)) = plus_plus_real(plus_plus_real(_709189, _709185), plus_plus_real(_709187, _709183)))], (2795 ^ _614856) ^ [_709327, _709329, _709331, _709333] : [-(plus_plus_nat(plus_plus_nat(_709333, _709331), plus_plus_nat(_709329, _709327)) = plus_plus_nat(plus_plus_nat(_709333, _709329), plus_plus_nat(_709331, _709327)))], (2797 ^ _614856) ^ [_709471, _709473, _709475, _709477] : [-(plus_plus_int(plus_plus_int(_709477, _709475), plus_plus_int(_709473, _709471)) = plus_plus_int(plus_plus_int(_709477, _709473), plus_plus_int(_709475, _709471)))], (2799 ^ _614856) ^ [_709573] : [-(power_power_real(_709573, one_one_nat) = _709573)], (2801 ^ _614856) ^ [_709654] : [-(power_power_nat(_709654, one_one_nat) = _709654)], (2803 ^ _614856) ^ [_709750] : [is_int(_709750), -(power_power_int(_709750, one_one_nat) = _709750)], (2819 ^ _614856) ^ [_710253, _710255] : [2820 ^ _614856 : [(2821 ^ _614856) ^ [] : [number_number_of_nat(_710253) = zero_zero_nat], (2823 ^ _614856) ^ [] : [ord_less_nat(zero_zero_nat, _710255)]], -(ord_less_nat(zero_zero_nat, power_power_nat(_710255, number_number_of_nat(_710253))))], (2809 ^ _614856) ^ [_709987, _709989] : [ord_less_nat(zero_zero_nat, power_power_nat(_709989, number_number_of_nat(_709987))), -(number_number_of_nat(_709987) = zero_zero_nat), -(ord_less_nat(zero_zero_nat, _709989))], (2827 ^ _614856) ^ [_710524] : [-(times_times_nat(_710524, number_number_of_nat(bit0(bit1(pls)))) = plus_plus_nat(_710524, _710524))], (2829 ^ _614856) ^ [_710608] : [-(times_times_nat(number_number_of_nat(bit0(bit1(pls))), _710608) = plus_plus_nat(_710608, _710608))], (2831 ^ _614856) ^ [_710741, _710743] : [ord_less_int(_710741, pls), -(times_times_nat(number_number_of_nat(_710741), number_number_of_nat(_710743)) = zero_zero_nat)], (2837 ^ _614856) ^ [_710917, _710919] : [-(ord_less_int(_710917, pls)), -(times_times_nat(number_number_of_nat(_710917), number_number_of_nat(_710919)) = number_number_of_nat(times_times_int(_710917, _710919)))], (2843 ^ _614856) ^ [_711190, _711192, _711194] : [ord_less_int(_711190, pls), -(times_times_nat(number_number_of_nat(_711190), times_times_nat(number_number_of_nat(_711194), _711192)) = zero_zero_nat)], (2849 ^ _614856) ^ [_711378, _711380, _711382] : [-(ord_less_int(_711378, pls)), -(times_times_nat(number_number_of_nat(_711378), times_times_nat(number_number_of_nat(_711382), _711380)) = times_times_nat(number_number_of_nat(times_times_int(_711378, _711382)), _711380))], (2855 ^ _614856) ^ [_711620, _711622] : [-(power_power_real(_711622, times_times_nat(number_number_of_nat(bit0(bit1(pls))), _711620)) = power_power_real(power_power_real(_711622, _711620), number_number_of_nat(bit0(bit1(pls)))))], (2857 ^ _614856) ^ [_711726, _711728] : [-(power_power_nat(_711728, times_times_nat(number_number_of_nat(bit0(bit1(pls))), _711726)) = power_power_nat(power_power_nat(_711728, _711726), number_number_of_nat(bit0(bit1(pls)))))], (2859 ^ _614856) ^ [_711832, _711834] : [-(power_power_int(_711834, times_times_nat(number_number_of_nat(bit0(bit1(pls))), _711832)) = power_power_int(power_power_int(_711834, _711832), number_number_of_nat(bit0(bit1(pls)))))], (2861 ^ _614856) ^ [_711953, _711955] : [ord_less_eq_real(power_power_real(_711955, times_times_nat(number_number_of_nat(bit0(bit1(pls))), _711953)), zero_zero_real), -(_711955 = zero_zero_real)], (2867 ^ _614856) ^ [_712175, _712177] : [is_int(_712177), ord_less_eq_int(power_power_int(_712177, times_times_nat(number_number_of_nat(bit0(bit1(pls))), _712175)), zero_zero_int), -(_712177 = zero_zero_int)], (2877 ^ _614856) ^ [_712455] : [-(times_times_real(zero_zero_real, _712455) = zero_zero_real)], (2879 ^ _614856) ^ [_712536] : [-(times_times_nat(zero_zero_nat, _712536) = zero_zero_nat)], (2881 ^ _614856) ^ [_712617] : [-(times_times_int(zero_zero_int, _712617) = zero_zero_int)], (2883 ^ _614856) ^ [_712698] : [-(times_times_real(_712698, zero_zero_real) = zero_zero_real)], (2885 ^ _614856) ^ [_712779] : [-(times_times_nat(_712779, zero_zero_nat) = zero_zero_nat)], (2887 ^ _614856) ^ [_712860] : [-(times_times_int(_712860, zero_zero_int) = zero_zero_int)], (2889 ^ _614856) ^ [_712941] : [-(plus_plus_real(zero_zero_real, _712941) = _712941)], (2891 ^ _614856) ^ [_713022] : [-(plus_plus_nat(zero_zero_nat, _713022) = _713022)], (2893 ^ _614856) ^ [_713118] : [is_int(_713118), -(plus_plus_int(zero_zero_int, _713118) = _713118)], (2899 ^ _614856) ^ [_713297] : [-(plus_plus_real(_713297, zero_zero_real) = _713297)], (2901 ^ _614856) ^ [_713378] : [-(plus_plus_nat(_713378, zero_zero_nat) = _713378)], (2903 ^ _614856) ^ [_713474] : [is_int(_713474), -(plus_plus_int(_713474, zero_zero_int) = _713474)], (2909 ^ _614856) ^ [_713711, _713713] : [_713713 = plus_plus_real(_713713, _713711), -(_713711 = zero_zero_real)], (2915 ^ _614856) ^ [_713879, _713881] : [_713879 = zero_zero_real, -(_713881 = plus_plus_real(_713881, _713879))], (2921 ^ _614856) ^ [_714126, _714128] : [_714128 = plus_plus_nat(_714128, _714126), -(_714126 = zero_zero_nat)], (2927 ^ _614856) ^ [_714294, _714296] : [_714294 = zero_zero_nat, -(_714296 = plus_plus_nat(_714296, _714294))], (2933 ^ _614856) ^ [_714512, _714514] : [is_int(_714514), is_int(_714512), 2940 ^ _614856 : [(2941 ^ _614856) ^ [] : [_714514 = plus_plus_int(_714514, _714512), -(_714512 = zero_zero_int)], (2947 ^ _614856) ^ [] : [_714512 = zero_zero_int, -(_714514 = plus_plus_int(_714514, _714512))]]], (2953 ^ _614856) ^ [_715067, _715069, _715071] : [-(times_times_real(_715071, plus_plus_real(_715069, _715067)) = plus_plus_real(times_times_real(_715071, _715069), times_times_real(_715071, _715067)))], (2955 ^ _614856) ^ [_715192, _715194, _715196] : [-(times_times_nat(_715196, plus_plus_nat(_715194, _715192)) = plus_plus_nat(times_times_nat(_715196, _715194), times_times_nat(_715196, _715192)))], (2957 ^ _614856) ^ [_715317, _715319, _715321] : [-(times_times_int(_715321, plus_plus_int(_715319, _715317)) = plus_plus_int(times_times_int(_715321, _715319), times_times_int(_715321, _715317)))], (2969 ^ _614856) ^ [_715814, _715816, _715818, _715820] : [-(plus_plus_real(times_times_real(_715816, _715820), times_times_real(_715814, _715818)) = plus_plus_real(times_times_real(_715816, _715818), times_times_real(_715814, _715820))), 2972 ^ _614856 : [(2973 ^ _614856) ^ [] : [_715816 = _715814], (2975 ^ _614856) ^ [] : [_715820 = _715818]]], (2959 ^ _614856) ^ [_715500, _715502, _715504, _715506] : [plus_plus_real(times_times_real(_715502, _715506), times_times_real(_715500, _715504)) = plus_plus_real(times_times_real(_715502, _715504), times_times_real(_715500, _715506)), -(_715502 = _715500), -(_715506 = _715504)], (2987 ^ _614856) ^ [_716529, _716531, _716533, _716535] : [-(plus_plus_nat(times_times_nat(_716531, _716535), times_times_nat(_716529, _716533)) = plus_plus_nat(times_times_nat(_716531, _716533), times_times_nat(_716529, _716535))), 2990 ^ _614856 : [(2991 ^ _614856) ^ [] : [_716531 = _716529], (2993 ^ _614856) ^ [] : [_716535 = _716533]]], (2977 ^ _614856) ^ [_716215, _716217, _716219, _716221] : [plus_plus_nat(times_times_nat(_716217, _716221), times_times_nat(_716215, _716219)) = plus_plus_nat(times_times_nat(_716217, _716219), times_times_nat(_716215, _716221)), -(_716217 = _716215), -(_716221 = _716219)], (2995 ^ _614856) ^ [_716901, _716903, _716905, _716907] : [is_int(_716907), is_int(_716905), is_int(_716903), is_int(_716901), 3010 ^ _614856 : [(3021 ^ _614856) ^ [] : [-(plus_plus_int(times_times_int(_716903, _716907), times_times_int(_716901, _716905)) = plus_plus_int(times_times_int(_716903, _716905), times_times_int(_716901, _716907))), 3024 ^ _614856 : [(3025 ^ _614856) ^ [] : [_716903 = _716901], (3027 ^ _614856) ^ [] : [_716907 = _716905]]], (3011 ^ _614856) ^ [] : [plus_plus_int(times_times_int(_716903, _716907), times_times_int(_716901, _716905)) = plus_plus_int(times_times_int(_716903, _716905), times_times_int(_716901, _716907)), -(_716903 = _716901), -(_716907 = _716905)]]], (3029 ^ _614856) ^ [_717911, _717913, _717915] : [-(times_times_real(plus_plus_real(_717915, _717913), _717911) = plus_plus_real(times_times_real(_717915, _717911), times_times_real(_717913, _717911)))], (3031 ^ _614856) ^ [_718036, _718038, _718040] : [-(times_times_nat(plus_plus_nat(_718040, _718038), _718036) = plus_plus_nat(times_times_nat(_718040, _718036), times_times_nat(_718038, _718036)))], (3033 ^ _614856) ^ [_718161, _718163, _718165] : [-(times_times_int(plus_plus_int(_718165, _718163), _718161) = plus_plus_int(times_times_int(_718165, _718161), times_times_int(_718163, _718161)))], (3035 ^ _614856) ^ [_718286, _718288, _718290] : [-(plus_plus_real(times_times_real(_718290, _718288), times_times_real(_718286, _718288)) = times_times_real(plus_plus_real(_718290, _718286), _718288))], (3037 ^ _614856) ^ [_718411, _718413, _718415] : [-(plus_plus_nat(times_times_nat(_718415, _718413), times_times_nat(_718411, _718413)) = times_times_nat(plus_plus_nat(_718415, _718411), _718413))], (3039 ^ _614856) ^ [_718536, _718538, _718540] : [-(plus_plus_int(times_times_int(_718540, _718538), times_times_int(_718536, _718538)) = times_times_int(plus_plus_int(_718540, _718536), _718538))], (3051 ^ _614856) ^ [_719027, _719029, _719031, _719033] : [3052 ^ _614856 : [(3053 ^ _614856) ^ [] : [_719033 = _719029], (3055 ^ _614856) ^ [] : [_719031 = _719027]], -(plus_plus_real(times_times_real(_719033, _719031), times_times_real(_719029, _719027)) = plus_plus_real(times_times_real(_719033, _719027), times_times_real(_719029, _719031)))], (3041 ^ _614856) ^ [_718719, _718721, _718723, _718725] : [plus_plus_real(times_times_real(_718725, _718723), times_times_real(_718721, _718719)) = plus_plus_real(times_times_real(_718725, _718719), times_times_real(_718721, _718723)), -(_718725 = _718721), -(_718723 = _718719)], (3069 ^ _614856) ^ [_719730, _719732, _719734, _719736] : [3070 ^ _614856 : [(3071 ^ _614856) ^ [] : [_719736 = _719732], (3073 ^ _614856) ^ [] : [_719734 = _719730]], -(plus_plus_nat(times_times_nat(_719736, _719734), times_times_nat(_719732, _719730)) = plus_plus_nat(times_times_nat(_719736, _719730), times_times_nat(_719732, _719734)))], (3059 ^ _614856) ^ [_719422, _719424, _719426, _719428] : [plus_plus_nat(times_times_nat(_719428, _719426), times_times_nat(_719424, _719422)) = plus_plus_nat(times_times_nat(_719428, _719422), times_times_nat(_719424, _719426)), -(_719428 = _719424), -(_719426 = _719422)], (3077 ^ _614856) ^ [_720096, _720098, _720100, _720102] : [is_int(_720102), is_int(_720100), is_int(_720098), is_int(_720096), 3092 ^ _614856 : [(3103 ^ _614856) ^ [] : [3104 ^ _614856 : [(3105 ^ _614856) ^ [] : [_720102 = _720098], (3107 ^ _614856) ^ [] : [_720100 = _720096]], -(plus_plus_int(times_times_int(_720102, _720100), times_times_int(_720098, _720096)) = plus_plus_int(times_times_int(_720102, _720096), times_times_int(_720098, _720100)))], (3093 ^ _614856) ^ [] : [plus_plus_int(times_times_int(_720102, _720100), times_times_int(_720098, _720096)) = plus_plus_int(times_times_int(_720102, _720096), times_times_int(_720098, _720100)), -(_720102 = _720098), -(_720100 = _720096)]]], (3111 ^ _614856) ^ [_721072] : [-(times_times_real(one_one_real, _721072) = _721072)], (3113 ^ _614856) ^ [_721153] : [-(times_times_nat(one_one_nat, _721153) = _721153)], (3115 ^ _614856) ^ [_721249] : [is_int(_721249), -(times_times_int(one_one_int, _721249) = _721249)], (3121 ^ _614856) ^ [_721428] : [-(times_times_real(_721428, one_one_real) = _721428)], (3123 ^ _614856) ^ [_721509] : [-(times_times_nat(_721509, one_one_nat) = _721509)], (3125 ^ _614856) ^ [_721605] : [is_int(_721605), -(times_times_int(_721605, one_one_int) = _721605)], (3131 ^ _614856) ^ [_721812, _721814, _721816] : [-(power_power_real(times_times_real(_721816, _721814), _721812) = times_times_real(power_power_real(_721816, _721812), power_power_real(_721814, _721812)))], (3133 ^ _614856) ^ [_721937, _721939, _721941] : [-(power_power_nat(times_times_nat(_721941, _721939), _721937) = times_times_nat(power_power_nat(_721941, _721937), power_power_nat(_721939, _721937)))], (3135 ^ _614856) ^ [_722062, _722064, _722066] : [-(power_power_int(times_times_int(_722066, _722064), _722062) = times_times_int(power_power_int(_722066, _722062), power_power_int(_722064, _722062)))], (3137 ^ _614856) ^ [_722187, _722189, _722191] : [-(times_times_real(power_power_real(_722191, _722189), power_power_real(_722191, _722187)) = power_power_real(_722191, plus_plus_nat(_722189, _722187)))], (3139 ^ _614856) ^ [_722312, _722314, _722316] : [-(times_times_nat(power_power_nat(_722316, _722314), power_power_nat(_722316, _722312)) = power_power_nat(_722316, plus_plus_nat(_722314, _722312)))], (3141 ^ _614856) ^ [_722437, _722439, _722441] : [-(times_times_int(power_power_int(_722441, _722439), power_power_int(_722441, _722437)) = power_power_int(_722441, plus_plus_nat(_722439, _722437)))], (3143 ^ _614856) ^ [_722534] : [-(power_power_real(_722534, zero_zero_nat) = one_one_real)], (3145 ^ _614856) ^ [_722615] : [-(power_power_nat(_722615, zero_zero_nat) = one_one_nat)], (3147 ^ _614856) ^ [_722696] : [-(power_power_int(_722696, zero_zero_nat) = one_one_int)], (3149 ^ _614856) ^ [] : [-(ord_less_eq_int(zero_zero_int, zero_zero_int))], (3151 ^ _614856) ^ [_722844, _722846] : [-(ord_less_eq_real(zero_zero_real, power_power_real(_722846, times_times_nat(number_number_of_nat(bit0(bit1(pls))), _722844))))], (3153 ^ _614856) ^ [_722944, _722946] : [-(ord_less_eq_int(zero_zero_int, power_power_int(_722946, times_times_nat(number_number_of_nat(bit0(bit1(pls))), _722944))))], (3155 ^ _614856) ^ [_723101, _723103, _723105, _723107, _723109] : [-(_723101 = zero_zero_real), plus_plus_real(_723105, times_times_real(_723101, _723109)) = plus_plus_real(_723103, times_times_real(_723101, _723107)), _723105 = _723103, -(_723109 = _723107)], (3169 ^ _614856) ^ [_723604, _723606, _723608, _723610, _723612] : [-(_723604 = zero_zero_nat), plus_plus_nat(_723608, times_times_nat(_723604, _723612)) = plus_plus_nat(_723606, times_times_nat(_723604, _723610)), _723608 = _723606, -(_723612 = _723610)], (3183 ^ _614856) ^ [_724107, _724109, _724111, _724113, _724115] : [is_int(_724115), is_int(_724113), is_int(_724107), -(_724107 = zero_zero_int), plus_plus_int(_724111, times_times_int(_724107, _724115)) = plus_plus_int(_724109, times_times_int(_724107, _724113)), _724111 = _724109, -(_724115 = _724113)], (3209 ^ _614856) ^ [_724840] : [-(plus_plus_real(_724840, _724840) = times_times_real(plus_plus_real(one_one_real, one_one_real), _724840))], (3211 ^ _614856) ^ [_724924] : [-(plus_plus_nat(_724924, _724924) = times_times_nat(plus_plus_nat(one_one_nat, one_one_nat), _724924))], (3213 ^ _614856) ^ [_725008] : [-(plus_plus_int(_725008, _725008) = times_times_int(plus_plus_int(one_one_int, one_one_int), _725008))], (3215 ^ _614856) ^ [_725106, _725108] : [-(plus_plus_real(_725108, times_times_real(_725106, _725108)) = times_times_real(plus_plus_real(_725106, one_one_real), _725108))], (3217 ^ _614856) ^ [_725212, _725214] : [-(plus_plus_nat(_725214, times_times_nat(_725212, _725214)) = times_times_nat(plus_plus_nat(_725212, one_one_nat), _725214))], (3219 ^ _614856) ^ [_725318, _725320] : [-(plus_plus_int(_725320, times_times_int(_725318, _725320)) = times_times_int(plus_plus_int(_725318, one_one_int), _725320))], (3221 ^ _614856) ^ [_725424, _725426] : [-(plus_plus_real(times_times_real(_725426, _725424), _725424) = times_times_real(plus_plus_real(_725426, one_one_real), _725424))], (3223 ^ _614856) ^ [_725530, _725532] : [-(plus_plus_nat(times_times_nat(_725532, _725530), _725530) = times_times_nat(plus_plus_nat(_725532, one_one_nat), _725530))], (3225 ^ _614856) ^ [_725636, _725638] : [-(plus_plus_int(times_times_int(_725638, _725636), _725636) = times_times_int(plus_plus_int(_725638, one_one_int), _725636))], (3227 ^ _614856) ^ [_725786, _725788] : [power_power_real(_725788, number_number_of_nat(_725786)) = zero_zero_real, 3230 ^ _614856 : [(3231 ^ _614856) ^ [] : [-(_725788 = zero_zero_real)], (3233 ^ _614856) ^ [] : [number_number_of_nat(_725786) = zero_zero_nat]]], (3235 ^ _614856) ^ [_726038, _726040] : [-(power_power_real(_726040, number_number_of_nat(_726038)) = zero_zero_real), _726040 = zero_zero_real, -(number_number_of_nat(_726038) = zero_zero_nat)], (3245 ^ _614856) ^ [_726385, _726387] : [power_power_nat(_726387, number_number_of_nat(_726385)) = zero_zero_nat, 3248 ^ _614856 : [(3249 ^ _614856) ^ [] : [-(_726387 = zero_zero_nat)], (3251 ^ _614856) ^ [] : [number_number_of_nat(_726385) = zero_zero_nat]]], (3253 ^ _614856) ^ [_726637, _726639] : [-(power_power_nat(_726639, number_number_of_nat(_726637)) = zero_zero_nat), _726639 = zero_zero_nat, -(number_number_of_nat(_726637) = zero_zero_nat)], (3263 ^ _614856) ^ [_726955, _726957] : [is_int(_726957), 3266 ^ _614856 : [(3267 ^ _614856) ^ [] : [power_power_int(_726957, number_number_of_nat(_726955)) = zero_zero_int, 3270 ^ _614856 : [(3271 ^ _614856) ^ [] : [-(_726957 = zero_zero_int)], (3273 ^ _614856) ^ [] : [number_number_of_nat(_726955) = zero_zero_nat]]], (3275 ^ _614856) ^ [] : [-(power_power_int(_726957, number_number_of_nat(_726955)) = zero_zero_int), _726957 = zero_zero_int, -(number_number_of_nat(_726955) = zero_zero_nat)]]], (3285 ^ _614856) ^ [_727594, _727596] : [ord_less_int(zero_zero_int, _727594), ord_less_int(zero_zero_int, times_times_int(_727594, _727596)), -(ord_less_int(zero_zero_int, _727596))], (3295 ^ _614856) ^ [] : [-(ord_less_eq_int(zero_zero_int, one_one_int))], (3297 ^ _614856) ^ [_727952, _727954] : [ord_less_eq_int(zero_zero_int, _727952), ord_less_eq_int(zero_zero_int, _727954), -(ord_less_eq_int(zero_zero_int, times_times_int(_727952, _727954)))], (3307 ^ _614856) ^ [_728257, _728259] : [ord_less_eq_int(zero_zero_int, _728257), ord_less_eq_int(zero_zero_int, _728259), -(ord_less_eq_int(zero_zero_int, plus_plus_int(_728257, _728259)))], (3317 ^ _614856) ^ [_728562, _728564] : [ord_less_eq_int(zero_zero_int, _728562), -(ord_less_eq_int(zero_zero_int, power_power_int(_728562, _728564)))], (3323 ^ _614856) ^ [_728784] : [number_number_of_nat(_728784) = zero_zero_nat, -(power_power_real(zero_zero_real, number_number_of_nat(_728784)) = one_one_real)], (3329 ^ _614856) ^ [_728954] : [-(number_number_of_nat(_728954) = zero_zero_nat), -(power_power_real(zero_zero_real, number_number_of_nat(_728954)) = zero_zero_real)], (3335 ^ _614856) ^ [_729183] : [number_number_of_nat(_729183) = zero_zero_nat, -(power_power_nat(zero_zero_nat, number_number_of_nat(_729183)) = one_one_nat)], (3341 ^ _614856) ^ [_729353] : [-(number_number_of_nat(_729353) = zero_zero_nat), -(power_power_nat(zero_zero_nat, number_number_of_nat(_729353)) = zero_zero_nat)], (3347 ^ _614856) ^ [_729582] : [number_number_of_nat(_729582) = zero_zero_nat, -(power_power_int(zero_zero_int, number_number_of_nat(_729582)) = one_one_int)], (3353 ^ _614856) ^ [_729752] : [-(number_number_of_nat(_729752) = zero_zero_nat), -(power_power_int(zero_zero_int, number_number_of_nat(_729752)) = zero_zero_int)], (3359 ^ _614856) ^ [] : [-(ord_less_eq_int(zero_zero_int, number_number_of_int(bit1(bit1(pls)))))], (3361 ^ _614856) ^ [_730042, _730044, _730046] : [ord_less_eq_int(zero_zero_int, plus_plus_int(times_times_int(_730046, _730044), _730042)), ord_less_int(_730042, _730046), ord_less_int(zero_zero_int, _730046), -(ord_less_eq_int(zero_zero_int, _730044))], (3375 ^ _614856) ^ [_730470, _730472, _730474] : [ord_less_int(plus_plus_int(times_times_int(_730474, _730472), _730470), zero_zero_int), ord_less_eq_int(zero_zero_int, _730470), ord_less_int(zero_zero_int, _730474), -(ord_less_eq_int(_730472, zero_zero_int))], (3389 ^ _614856) ^ [_730926, _730928, _730930, _730932, _730934] : [ord_less_eq_int(plus_plus_int(times_times_int(_730934, _730932), _730930), plus_plus_int(times_times_int(_730934, _730928), _730926)), ord_less_eq_int(zero_zero_int, _730930), ord_less_int(_730930, _730934), ord_less_int(_730926, _730934), -(ord_less_eq_int(_730932, _730928))], (3407 ^ _614856) ^ [_731537, _731539, _731541, _731543, _731545, _731547] : [plus_plus_int(times_times_int(_731547, _731545), _731543) = plus_plus_int(times_times_int(_731541, _731539), _731537), ord_less_eq_int(zero_zero_int, plus_plus_int(times_times_int(_731541, _731539), _731537)), ord_less_int(_731537, _731541), ord_less_eq_int(zero_zero_int, _731543), ord_less_int(zero_zero_int, _731541), ord_less_eq_int(_731541, _731547), -(ord_less_eq_int(_731545, _731539))], (3433 ^ _614856) ^ [_732374, _732376, _732378, _732380, _732382] : [ord_less_eq_int(plus_plus_int(times_times_int(_732382, _732380), _732378), plus_plus_int(times_times_int(_732382, _732376), _732374)), ord_less_eq_int(_732374, zero_zero_int), ord_less_int(_732382, _732374), ord_less_int(_732382, _732378), -(ord_less_eq_int(_732376, _732380))], (3451 ^ _614856) ^ [_732985, _732987, _732989, _732991, _732993, _732995] : [plus_plus_int(times_times_int(_732995, _732993), _732991) = plus_plus_int(times_times_int(_732989, _732987), _732985), ord_less_int(plus_plus_int(times_times_int(_732989, _732987), _732985), zero_zero_int), ord_less_int(_732991, _732995), ord_less_eq_int(zero_zero_int, _732985), ord_less_int(zero_zero_int, _732989), ord_less_eq_int(_732989, _732995), -(ord_less_eq_int(_732987, _732993))], (3477 ^ _614856) ^ [_733751] : [-(power_power_int(power_power_int(_733751, number_number_of_nat(bit0(bit1(pls)))), number_number_of_nat(bit0(bit1(pls)))) = power_power_int(_733751, number_number_of_nat(bit0(bit0(bit1(pls))))))], (3479 ^ _614856) ^ [_733838] : [-(times_times_real(_733838, _733838) = power_power_real(_733838, number_number_of_nat(bit0(bit1(pls)))))], (3481 ^ _614856) ^ [_733922] : [-(times_times_nat(_733922, _733922) = power_power_nat(_733922, number_number_of_nat(bit0(bit1(pls)))))], (3483 ^ _614856) ^ [_734006] : [-(times_times_int(_734006, _734006) = power_power_int(_734006, number_number_of_nat(bit0(bit1(pls)))))], (3485 ^ _614856) ^ [] : [-(zcong(power_power_int(s, number_number_of_nat(bit0(bit1(pls)))), number_number_of_int(min), plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), m), one_one_int)))], (3487 ^ _614856) ^ [_734186, _734188, _734190] : [-(zcong(_734188, zero_zero_int, _734186)), zcong(power_power_int(_734190, number_number_of_nat(bit0(bit1(pls)))), _734188, _734186), dvd_dvd_int(_734186, _734190)], (3497 ^ _614856) ^ [_734495] : [is_int(_734495), 3500 ^ _614856 : [(3525 ^ _614856) ^ [] : [-(zprime(_734495)), ord_less_int(one_one_int, _734495), 3531 ^ _614856 : [(3532 ^ _614856) ^ [] : [-(is_int(3530 ^ [_734495]))], (3534 ^ _614856) ^ [] : [-(ord_less_eq_int(zero_zero_int, 3530 ^ [_734495]))], (3536 ^ _614856) ^ [] : [-(dvd_dvd_int(3530 ^ [_734495], _734495))], (3538 ^ _614856) ^ [] : [3530 ^ [_734495] = one_one_int], (3540 ^ _614856) ^ [] : [3530 ^ [_734495] = _734495]]], (3501 ^ _614856) ^ [] : [zprime(_734495), 3504 ^ _614856 : [(3505 ^ _614856) ^ [] : [-(ord_less_int(one_one_int, _734495))], (3507 ^ _614856) ^ [_734821] : [is_int(_734821), ord_less_eq_int(zero_zero_int, _734821), dvd_dvd_int(_734821, _734495), -(_734821 = one_one_int), -(_734821 = _734495)]]]]], (3544 ^ _614856) ^ [_735856] : [is_int(_735856), zprime(_735856), -(_735856 = number_number_of_int(bit0(bit1(pls)))), -(_735856 = number_number_of_int(bit1(bit1(pls)))), -(ord_less_eq_int(number_number_of_int(bit1(bit0(bit1(pls)))), _735856))], (3562 ^ _614856) ^ [] : [-(ord_less_nat(zero_zero_nat, number_number_of_nat(bit0(bit1(pls)))))], (3565 ^ _614856) ^ [] : [-(is_int(3563 ^ []))], (3567 ^ _614856) ^ [] : [-(zcong(power_power_int(3563 ^ [], number_number_of_nat(bit0(bit1(pls)))), number_number_of_int(min), plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), m), one_one_int)))], (3569 ^ _614856) ^ [] : [-(legendre(number_number_of_int(min), plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), m), one_one_int)) = one_one_int)], (3571 ^ _614856) ^ [] : [-(bit1(min) = min)], (3573 ^ _614856) ^ [_736618] : [is_int(_736618), 3576 ^ _614856 : [(3577 ^ _614856) ^ [] : [min = bit1(_736618), -(min = _736618)], (3583 ^ _614856) ^ [] : [min = _736618, -(min = bit1(_736618))]]], (3589 ^ _614856) ^ [_737052] : [is_int(_737052), 3592 ^ _614856 : [(3593 ^ _614856) ^ [] : [bit1(_737052) = min, -(_737052 = min)], (3599 ^ _614856) ^ [] : [_737052 = min, -(bit1(_737052) = min)]]], (3605 ^ _614856) ^ [] : [min = pls], (3607 ^ _614856) ^ [] : [pls = min], (3609 ^ _614856) ^ [_737574] : [min = bit0(_737574)], (3611 ^ _614856) ^ [_737653] : [bit0(_737653) = min], (3613 ^ _614856) ^ [] : [ord_less_int(min, min)], (3615 ^ _614856) ^ [] : [-(ord_less_eq_int(min, min))], (3617 ^ _614856) ^ [_737882] : [ord_less_int(bit1(_737882), min), -(ord_less_int(_737882, min))], (3623 ^ _614856) ^ [_738042] : [ord_less_int(_738042, min), -(ord_less_int(bit1(_738042), min))], (3629 ^ _614856) ^ [_738267] : [ord_less_int(min, bit1(_738267)), -(ord_less_int(min, _738267))], (3635 ^ _614856) ^ [_738427] : [ord_less_int(min, _738427), -(ord_less_int(min, bit1(_738427)))], (3641 ^ _614856) ^ [] : [ord_less_int(pls, min)], (3643 ^ _614856) ^ [] : [-(ord_less_int(min, pls))], (3645 ^ _614856) ^ [_738757] : [ord_less_int(min, bit0(_738757)), -(ord_less_int(min, _738757))], (3651 ^ _614856) ^ [_738917] : [ord_less_int(min, _738917), -(ord_less_int(min, bit0(_738917)))], (3657 ^ _614856) ^ [] : [-(ord_less_int(min, zero_zero_int))], (3659 ^ _614856) ^ [_739195] : [ord_less_eq_int(min, bit1(_739195)), -(ord_less_eq_int(min, _739195))], (3665 ^ _614856) ^ [_739355] : [ord_less_eq_int(min, _739355), -(ord_less_eq_int(min, bit1(_739355)))], (3671 ^ _614856) ^ [_739580] : [ord_less_eq_int(bit1(_739580), min), -(ord_less_eq_int(_739580, min))], (3677 ^ _614856) ^ [_739740] : [ord_less_eq_int(_739740, min), -(ord_less_eq_int(bit1(_739740), min))], (3683 ^ _614856) ^ [] : [-(ord_less_eq_int(min, pls))], (3685 ^ _614856) ^ [] : [ord_less_eq_int(pls, min)], (3687 ^ _614856) ^ [_740070] : [ord_less_eq_int(bit0(_740070), min), -(ord_less_eq_int(_740070, min))], (3693 ^ _614856) ^ [_740230] : [ord_less_eq_int(_740230, min), -(ord_less_eq_int(bit0(_740230), min))], (3699 ^ _614856) ^ [] : [number_number_of_int(pls) = number_number_of_int(min)], (3701 ^ _614856) ^ [_740507] : [ord_less_int(bit0(_740507), min), -(ord_less_eq_int(_740507, min))], (3707 ^ _614856) ^ [_740667] : [ord_less_eq_int(_740667, min), -(ord_less_int(bit0(_740667), min))], (3713 ^ _614856) ^ [_740892] : [ord_less_eq_int(min, bit0(_740892)), -(ord_less_int(min, _740892))], (3719 ^ _614856) ^ [_741052] : [ord_less_int(min, _741052), -(ord_less_eq_int(min, bit0(_741052)))], (3725 ^ _614856) ^ [_741262, _741264] : [is_int(_741264), is_int(_741262), 3732 ^ _614856 : [(3733 ^ _614856) ^ [] : [times_times_int(_741264, _741262) = one_one_int, 3738 ^ _614856 : [(3739 ^ _614856) ^ [] : [-(_741264 = one_one_int)], (3741 ^ _614856) ^ [] : [-(_741262 = one_one_int)]], 3742 ^ _614856 : [(3743 ^ _614856) ^ [] : [-(_741264 = number_number_of_int(min))], (3745 ^ _614856) ^ [] : [-(_741262 = number_number_of_int(min))]]], (3747 ^ _614856) ^ [] : [-(times_times_int(_741264, _741262) = one_one_int), 3748 ^ _614856 : [(3749 ^ _614856) ^ [] : [_741264 = one_one_int, _741262 = one_one_int], (3755 ^ _614856) ^ [] : [_741264 = number_number_of_int(min), _741262 = number_number_of_int(min)]]]]], (3763 ^ _614856) ^ [_742292, _742294] : [is_int(_742294), times_times_int(_742294, _742292) = one_one_int, -(_742294 = one_one_int), -(_742294 = number_number_of_int(min))], (3777 ^ _614856) ^ [_742728, _742730, _742732] : [zcong(_742732, _742730, _742728), -(zcong(_742730, _742732, _742728))], (3783 ^ _614856) ^ [_742900, _742902, _742904] : [zcong(_742902, _742904, _742900), -(zcong(_742904, _742902, _742900))], (3789 ^ _614856) ^ [_743107, _743109] : [-(zcong(_743109, _743109, _743107))], (3791 ^ _614856) ^ [_743245, _743247, _743249, _743251] : [zcong(_743249, _743247, _743245), zcong(_743247, _743251, _743245), -(zcong(_743249, _743251, _743245))], (3801 ^ _614856) ^ [_743570, _743572] : [ord_less_eq_real(_743572, _743570), -(_743572 = _743570), -(ord_less_real(_743572, _743570))], (3811 ^ _614856) ^ [_743872, _743874] : [ord_less_eq_nat(_743874, _743872), -(_743874 = _743872), -(ord_less_nat(_743874, _743872))], (3821 ^ _614856) ^ [_744174, _744176] : [is_int(_744176), is_int(_744174), ord_less_eq_int(_744176, _744174), -(_744176 = _744174), -(ord_less_int(_744176, _744174))], (3839 ^ _614856) ^ [_744666, _744668, _744670] : [ord_less_int(_744668, _744666), ord_less_int(_744670, _744666), -(ord_less_eq_int(_744668, _744670)), -(ord_less_eq_int(_744670, _744668))], (3853 ^ _614856) ^ [_745069, _745071] : [is_int(_745071), is_int(_745069), 3860 ^ _614856 : [(3861 ^ _614856) ^ [] : [zcong(_745071, _745069, zero_zero_int), -(_745071 = _745069)], (3867 ^ _614856) ^ [] : [_745071 = _745069, -(zcong(_745071, _745069, zero_zero_int))]]], (3873 ^ _614856) ^ [_745604, _745606] : [-(zcong(_745606, _745604, one_one_int))], (3875 ^ _614856) ^ [_745713, _745715, _745717] : [-(zcong(times_times_int(_745717, _745715), times_times_int(_745713, _745715), _745715))], (3877 ^ _614856) ^ [_745859, _745861, _745863, _745865] : [zcong(_745863, _745861, _745859), -(zcong(times_times_int(_745863, _745865), times_times_int(_745861, _745865), _745859))], (3883 ^ _614856) ^ [_746125, _746127, _746129, _746131] : [zcong(_746129, _746127, _746125), -(zcong(times_times_int(_746131, _746129), times_times_int(_746131, _746127), _746125))], (3889 ^ _614856) ^ [_746405, _746407, _746409, _746411, _746413] : [zcong(_746409, _746407, _746405), zcong(_746413, _746411, _746405), -(zcong(times_times_int(_746409, _746413), times_times_int(_746407, _746411), _746405))], (3899 ^ _614856) ^ [_746794, _746796, _746798, _746800, _746802] : [zcong(_746798, _746796, _746794), zcong(_746802, _746800, _746794), -(zcong(plus_plus_int(_746798, _746802), plus_plus_int(_746796, _746800), _746794))], (3909 ^ _614856) ^ [_747112] : [-(power_power_real(number267125858f_real(min), times_times_nat(number_number_of_nat(bit0(bit1(pls))), _747112)) = one_one_real)], (3911 ^ _614856) ^ [_747196] : [-(power_power_int(number_number_of_int(min), times_times_nat(number_number_of_nat(bit0(bit1(pls))), _747196)) = one_one_int)], (3913 ^ _614856) ^ [_747323, _747325, _747327] : [ord_less_int(zero_zero_int, _747323), ord_less_int(_747323, _747325), ord_less_int(zero_zero_int, _747327), ord_less_int(_747327, _747323), zcong(_747323, _747327, _747325)], (3931 ^ _614856) ^ [_747835, _747837, _747839] : [is_int(_747837), 3934 ^ _614856 : [(3935 ^ _614856) ^ [] : [zcong(_747839, _747837, _747835), 3939 ^ _614856 : [(3940 ^ _614856) ^ [] : [-(is_int(3938 ^ [_747835, _747837, _747839]))], (3942 ^ _614856) ^ [] : [-(_747837 = plus_plus_int(_747839, times_times_int(_747835, 3938 ^ [_747835, _747837, _747839])))]]], (3944 ^ _614856) ^ [] : [-(zcong(_747839, _747837, _747835)), 3945 ^ _614856 : [(3946 ^ _614856) ^ [_748341] : [is_int(_748341), _747837 = plus_plus_int(_747839, times_times_int(_747835, _748341))]]]]], (3954 ^ _614856) ^ [_748610] : [-(times_times_real(number267125858f_real(bit0(bit0(bit1(pls)))), power_power_real(_748610, number_number_of_nat(bit0(bit1(pls))))) = power_power_real(times_times_real(number267125858f_real(bit0(bit1(pls))), _748610), number_number_of_nat(bit0(bit1(pls)))))], (3956 ^ _614856) ^ [_748729, _748731] : [is_int(_748729), ord_less_eq_int(zero_zero_int, _748729), ord_less_int(_748729, _748731), zcong(_748729, zero_zero_int, _748731), -(_748729 = zero_zero_int)], (3974 ^ _614856) ^ [_749220, _749222, _749224] : [is_int(_749224), is_int(_749220), ord_less_eq_int(zero_zero_int, _749220), ord_less_int(_749220, _749222), ord_less_eq_int(zero_zero_int, _749224), ord_less_int(_749224, _749222), zcong(_749220, _749224, _749222), -(_749220 = _749224)], (4004 ^ _614856) ^ [_750022, _750024, _750026, _750028] : [zcong(power_power_int(_750026, _750024), one_one_int, _750022), -(zcong(power_power_int(_750026, times_times_nat(_750024, _750028)), one_one_int, _750022))], (4010 ^ _614856) ^ [_750280, _750282, _750284] : [ord_less_eq_int(zero_zero_int, _750280), zprime(_750282), dvd_dvd_int(_750282, times_times_int(_750280, _750284)), -(dvd_dvd_int(_750282, _750280)), -(dvd_dvd_int(_750282, _750284))], (4028 ^ _614856) ^ [] : [-(quadRes(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), m), one_one_int), number_number_of_int(min)))], (4030 ^ _614856) ^ [] : [-(dvd_dvd_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), m), one_one_int), minus_minus_int(power_power_int(s, number_number_of_nat(bit0(bit1(pls)))), number_number_of_int(min))))], (4032 ^ _614856) ^ [_750900, _750902, _750904] : [ord_less_int(number_number_of_int(bit0(bit1(pls))), _750900), zcong(power_power_int(number_number_of_int(min), _750904), power_power_int(number_number_of_int(min), _750902), _750900), -(power_power_int(number_number_of_int(min), _750904) = power_power_int(number_number_of_int(min), _750902))], (4042 ^ _614856) ^ [_751235, _751237] : [ord_less_int(number_number_of_int(bit0(bit1(pls))), _751235), zcong(_751237, number_number_of_int(min), _751235), zcong(_751237, one_one_int, _751235)], (4052 ^ _614856) ^ [] : [-(minus_minus_int(power_power_int(s, number_number_of_nat(bit0(bit1(pls)))), number_number_of_int(min)) = plus_plus_int(power_power_int(s, number_number_of_nat(bit0(bit1(pls)))), one_one_int))], (4054 ^ _614856) ^ [] : [-(quadRes(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), m), one_one_int), number_number_of_int(min))), legendre(number_number_of_int(min), plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), m), one_one_int)) = one_one_int], (4060 ^ _614856) ^ [_751726] : [-(ord_less_real(zero_zero_real, times_times_real(_751726, _751726))), -(_751726 = zero_zero_real)], (4066 ^ _614856) ^ [_751891] : [_751891 = zero_zero_real, ord_less_real(zero_zero_real, times_times_real(_751891, _751891))], (4072 ^ _614856) ^ [_752146, _752148, _752150, _752152, _752154] : [zcong(_752150, _752148, _752146), zcong(_752154, _752152, _752146), -(zcong(minus_minus_int(_752150, _752154), minus_minus_int(_752148, _752152), _752146))], (4082 ^ _614856) ^ [_752507, _752509, _752511] : [dvd_dvd_int(_752511, minus_minus_int(_752509, _752507)), dvd_dvd_int(_752511, _752507), -(dvd_dvd_int(_752511, _752509))], (4092 ^ _614856) ^ [_752821, _752823, _752825] : [-(times_times_int(_752825, minus_minus_int(_752823, _752821)) = minus_minus_int(times_times_int(_752825, _752823), times_times_int(_752825, _752821)))], (4094 ^ _614856) ^ [_752946, _752948, _752950] : [-(times_times_int(minus_minus_int(_752950, _752948), _752946) = minus_minus_int(times_times_int(_752950, _752946), times_times_int(_752948, _752946)))], (4096 ^ _614856) ^ [_753057, _753059] : [-(minus_minus_int(bit0(_753059), bit0(_753057)) = bit0(minus_minus_int(_753059, _753057)))], (4098 ^ _614856) ^ [_753164] : [is_int(_753164), -(minus_minus_int(_753164, pls) = _753164)], (4104 ^ _614856) ^ [_753386, _753388, _753390] : [is_int(_753390), minus_minus_int(_753390, _753388) = _753386, -(_753390 = plus_plus_int(_753386, _753388))], (4114 ^ _614856) ^ [_753690, _753692] : [-(number267125858f_real(minus_minus_int(_753692, _753690)) = minus_minus_real(number267125858f_real(_753692), number267125858f_real(_753690)))], (4116 ^ _614856) ^ [_753796, _753798] : [-(number_number_of_int(minus_minus_int(_753798, _753796)) = minus_minus_int(number_number_of_int(_753798), number_number_of_int(_753796)))], (4118 ^ _614856) ^ [_753916, _753918, _753920] : [-(times_times_real(number267125858f_real(_753920), minus_minus_real(_753918, _753916)) = minus_minus_real(times_times_real(number267125858f_real(_753920), _753918), times_times_real(number267125858f_real(_753920), _753916)))], (4120 ^ _614856) ^ [_754047, _754049, _754051] : [-(times_times_int(number_number_of_int(_754051), minus_minus_int(_754049, _754047)) = minus_minus_int(times_times_int(number_number_of_int(_754051), _754049), times_times_int(number_number_of_int(_754051), _754047)))], (4122 ^ _614856) ^ [_754178, _754180, _754182] : [-(times_times_real(minus_minus_real(_754182, _754180), number267125858f_real(_754178)) = minus_minus_real(times_times_real(_754182, number267125858f_real(_754178)), times_times_real(_754180, number267125858f_real(_754178))))], (4124 ^ _614856) ^ [_754309, _754311, _754313] : [-(times_times_int(minus_minus_int(_754313, _754311), number_number_of_int(_754309)) = minus_minus_int(times_times_int(_754313, number_number_of_int(_754309)), times_times_int(_754311, number_number_of_int(_754309))))], (4126 ^ _614856) ^ [_754426, _754428] : [-(minus_minus_int(bit1(_754428), bit0(_754426)) = bit1(minus_minus_int(_754428, _754426)))], (4128 ^ _614856) ^ [_754532, _754534] : [-(minus_minus_int(bit1(_754534), bit1(_754532)) = bit0(minus_minus_int(_754534, _754532)))], (4130 ^ _614856) ^ [_754624] : [-(minus_minus_int(pls, bit0(_754624)) = bit0(minus_minus_int(pls, _754624)))], (4132 ^ _614856) ^ [_754770, _754772] : [ord_less_int(_754772, _754770), -(ord_less_int(minus_minus_int(_754772, _754770), zero_zero_int))], (4138 ^ _614856) ^ [_754938, _754940] : [ord_less_int(minus_minus_int(_754940, _754938), zero_zero_int), -(ord_less_int(_754940, _754938))], (4144 ^ _614856) ^ [_755211, _755213, _755215, _755217, _755219, _755221, _755223] : [-(plus_plus_int(times_times_int(minus_minus_int(_755223, times_times_int(_755221, _755219)), _755217), times_times_int(minus_minus_int(_755215, times_times_int(_755221, _755213)), _755211)) = minus_minus_int(plus_plus_int(times_times_int(_755223, _755217), times_times_int(_755215, _755211)), times_times_int(_755221, plus_plus_int(times_times_int(_755219, _755217), times_times_int(_755213, _755211)))))], (4146 ^ _614856) ^ [_755418, _755420, _755422] : [zcong(_755422, _755420, _755418), -(dvd_dvd_int(_755418, minus_minus_int(_755422, _755420)))], (4152 ^ _614856) ^ [_755594, _755596, _755598] : [dvd_dvd_int(_755594, minus_minus_int(_755598, _755596)), -(zcong(_755598, _755596, _755594))], (4158 ^ _614856) ^ [_755819, _755821, _755823] : [-(plus_plus_real(number267125858f_real(_755823), minus_minus_real(number267125858f_real(_755821), _755819)) = minus_minus_real(number267125858f_real(plus_plus_int(_755823, _755821)), _755819))], (4160 ^ _614856) ^ [_755947, _755949, _755951] : [-(plus_plus_int(number_number_of_int(_755951), minus_minus_int(number_number_of_int(_755949), _755947)) = minus_minus_int(number_number_of_int(plus_plus_int(_755951, _755949)), _755947))], (4162 ^ _614856) ^ [_756076, _756078] : [is_int(_756076), ord_less_int(zero_zero_int, _756076), ord_less_int(_756076, _756078), -(_756076 = minus_minus_int(_756078, one_one_int)), -(ord_less_int(_756076, minus_minus_int(_756078, one_one_int)))], (4180 ^ _614856) ^ [_756595, _756597] : [ord_less_eq_int(_756597, minus_minus_int(_756595, one_one_int)), -(ord_less_int(_756597, _756595))], (4186 ^ _614856) ^ [_756763, _756765] : [ord_less_int(_756765, _756763), -(ord_less_eq_int(_756765, minus_minus_int(_756763, one_one_int)))], (4192 ^ _614856) ^ [_756952] : [-(minus_minus_int(pls, bit1(_756952)) = bit1(minus_minus_int(min, _756952)))], (4194 ^ _614856) ^ [_757040] : [-(minus_minus_int(min, bit1(_757040)) = bit0(minus_minus_int(min, _757040)))], (4196 ^ _614856) ^ [_757128] : [-(minus_minus_int(min, bit0(_757128)) = bit1(minus_minus_int(min, _757128)))], (4198 ^ _614856) ^ [_757274, _757276] : [zcong(times_times_int(_757276, minus_minus_int(_757274, one_one_int)), one_one_int, _757274), -(zcong(_757276, minus_minus_int(_757274, one_one_int), _757274))], (4204 ^ _614856) ^ [_757458, _757460] : [zcong(_757460, minus_minus_int(_757458, one_one_int), _757458), -(zcong(times_times_int(_757460, minus_minus_int(_757458, one_one_int)), one_one_int, _757458))], (4210 ^ _614856) ^ [_757734, _757736, _757738, _757740, _757742] : [zcong(_757738, _757736, _757734), _757736 = _757740, zcong(_757740, _757742, _757734), -(zcong(_757738, _757742, _757734))], (4224 ^ _614856) ^ [_758170, _758172] : [is_int(_758172), zprime(_758170), ord_less_int(zero_zero_int, _758172), ord_less_int(_758172, _758170), zcong(times_times_int(_758172, _758172), one_one_int, _758170), -(_758172 = one_one_int), -(_758172 = minus_minus_int(_758170, one_one_int))], (4250 ^ _614856) ^ [_758836, _758838] : [zprime(_758836), ord_less_int(zero_zero_int, _758838), zcong(times_times_int(_758838, _758838), one_one_int, _758836), -(zcong(_758838, one_one_int, _758836)), -(zcong(_758838, minus_minus_int(_758836, one_one_int), _758836))], (4268 ^ _614856) ^ [_759315, _759317] : [-(times_times_int(plus_plus_int(_759317, _759315), minus_minus_int(_759317, _759315)) = minus_minus_int(power_power_int(_759317, number_number_of_nat(bit0(bit1(pls)))), power_power_int(_759315, number_number_of_nat(bit0(bit1(pls))))))], (4270 ^ _614856) ^ [_759413] : [-(zcong(_759413, zero_zero_int, _759413))], (4272 ^ _614856) ^ [_759563, _759565, _759567, _759569, _759571] : [zcong(_759567, _759565, _759563), 4275 ^ _614856 : [(4276 ^ _614856) ^ [] : [zcong(_759571, times_times_int(_759569, _759567), _759563), -(zcong(_759571, times_times_int(_759569, _759565), _759563))], (4282 ^ _614856) ^ [] : [zcong(_759571, times_times_int(_759569, _759565), _759563), -(zcong(_759571, times_times_int(_759569, _759567), _759563))]]], (4288 ^ _614856) ^ [_760139, _760141, _760143, _760145, _760147] : [zcong(_760143, _760141, _760139), 4291 ^ _614856 : [(4292 ^ _614856) ^ [] : [zcong(_760147, times_times_int(_760143, _760145), _760139), -(zcong(_760147, times_times_int(_760141, _760145), _760139))], (4298 ^ _614856) ^ [] : [zcong(_760147, times_times_int(_760141, _760145), _760139), -(zcong(_760147, times_times_int(_760143, _760145), _760139))]]], (4304 ^ _614856) ^ [_760701, _760703, _760705, _760707] : [zcong(_760705, _760703, _760701), -(zcong(plus_plus_int(_760705, _760707), plus_plus_int(_760703, _760707), _760701))], (4310 ^ _614856) ^ [_760967, _760969, _760971, _760973] : [zcong(_760971, _760969, _760967), -(zcong(power_power_int(_760971, _760973), power_power_int(_760969, _760973), _760967))], (4316 ^ _614856) ^ [_761190, _761192] : [-(power_power_real(minus_minus_real(_761192, _761190), number_number_of_nat(bit0(bit1(pls)))) = minus_minus_real(plus_plus_real(power_power_real(_761192, number_number_of_nat(bit0(bit1(pls)))), power_power_real(_761190, number_number_of_nat(bit0(bit1(pls))))), times_times_real(times_times_real(number267125858f_real(bit0(bit1(pls))), _761192), _761190)))], (4318 ^ _614856) ^ [_761308, _761310] : [-(power_power_int(minus_minus_int(_761310, _761308), number_number_of_nat(bit0(bit1(pls)))) = minus_minus_int(plus_plus_int(power_power_int(_761310, number_number_of_nat(bit0(bit1(pls)))), power_power_int(_761308, number_number_of_nat(bit0(bit1(pls))))), times_times_int(times_times_int(number_number_of_int(bit0(bit1(pls))), _761310), _761308)))], (4320 ^ _614856) ^ [_761426, _761428] : [-(power_power_int(minus_minus_int(_761428, _761426), number_number_of_nat(bit0(bit1(pls)))) = plus_plus_int(minus_minus_int(power_power_int(_761428, number_number_of_nat(bit0(bit1(pls)))), times_times_int(times_times_int(number_number_of_int(bit0(bit1(pls))), _761428), _761426)), power_power_int(_761426, number_number_of_nat(bit0(bit1(pls))))))], (4322 ^ _614856) ^ [_761544, _761546] : [-(power_power_int(minus_minus_int(_761546, _761544), number_number_of_nat(bit1(bit1(pls)))) = minus_minus_int(plus_plus_int(minus_minus_int(power_power_int(_761546, number_number_of_nat(bit1(bit1(pls)))), times_times_int(times_times_int(number_number_of_int(bit1(bit1(pls))), power_power_int(_761546, number_number_of_nat(bit0(bit1(pls))))), _761544)), times_times_int(times_times_int(number_number_of_int(bit1(bit1(pls))), _761546), power_power_int(_761544, number_number_of_nat(bit0(bit1(pls)))))), power_power_int(_761544, number_number_of_nat(bit1(bit1(pls))))))], (4324 ^ _614856) ^ [_761706, _761708, _761710] : [is_int(_761708), is_int(_761706), ord_less_int(zero_zero_int, _761706), ord_less_int(zero_zero_int, _761708), ord_less_int(zero_zero_int, _761710), zcong(_761706, _761708, _761710), ord_less_int(_761706, _761710), ord_less_int(_761708, _761710), -(_761706 = _761708)], (4358 ^ _614856) ^ [_762573, _762575] : [ord_less_int(zero_zero_int, _762573), ord_less_int(_762573, _762575), zcong(_762573, zero_zero_int, _762575)], (4368 ^ _614856) ^ [_762875, _762877] : [dvd_dvd_int(_762877, _762875), -(ord_less_eq_int(_762875, zero_zero_int)), -(ord_less_eq_int(_762877, _762875))], (4378 ^ _614856) ^ [_763204, _763206] : [zcong(_763206, zero_zero_int, _763204), -(dvd_dvd_int(_763204, _763206))], (4384 ^ _614856) ^ [_763368, _763370] : [dvd_dvd_int(_763368, _763370), -(zcong(_763370, zero_zero_int, _763368))], (4390 ^ _614856) ^ [_763611, _763613] : [zcong(_763613, zero_zero_int, _763611), -(dvd_dvd_int(_763611, _763613))], (4396 ^ _614856) ^ [_763775, _763777] : [dvd_dvd_int(_763775, _763777), -(zcong(_763777, zero_zero_int, _763775))], (4402 ^ _614856) ^ [_764003, _764005, _764007] : [zprime(_764003), dvd_dvd_int(_764003, times_times_int(_764007, _764005)), -(dvd_dvd_int(_764003, _764007)), -(dvd_dvd_int(_764003, _764005))], (4416 ^ _614856) ^ [_764410, _764412] : [is_int(_764410), ord_less_eq_int(zero_zero_int, _764410), ord_less_int(_764410, _764412), zcong(_764410, zero_zero_int, _764412), -(_764410 = zero_zero_int)], (4434 ^ _614856) ^ [_764901, _764903, _764905] : [ord_less_nat(zero_zero_nat, _764901), dvd_dvd_int(_764905, _764903), -(dvd_dvd_int(_764905, power_power_int(_764903, _764901)))], (4444 ^ _614856) ^ [_765202] : [-(power_power_int(number_number_of_int(min), _765202) = one_one_int), -(power_power_int(number_number_of_int(min), _765202) = number_number_of_int(min))], (4450 ^ _614856) ^ [_765433, _765435, _765437] : [zprime(_765433), -(zcong(_765435, zero_zero_int, _765433)), -(zcong(_765437, zero_zero_int, _765433)), zcong(times_times_int(_765435, _765437), zero_zero_int, _765433)], (4464 ^ _614856) ^ [_765866, _765868, _765870] : [zprime(_765866), ord_less_int(zero_zero_int, _765868), zcong(times_times_int(_765868, _765870), zero_zero_int, _765866), -(zcong(_765868, zero_zero_int, _765866)), -(zcong(_765870, zero_zero_int, _765866))], (4482 ^ _614856) ^ [_766392, _766394, _766396] : [zprime(_766392), ord_less_int(zero_zero_int, _766394), zcong(times_times_int(_766394, _766396), zero_zero_int, _766392), -(zcong(_766394, zero_zero_int, _766392)), -(zcong(_766396, zero_zero_int, _766392))], (4500 ^ _614856) ^ [_766912, _766914, _766916] : [zprime(_766912), dvd_dvd_int(_766912, power_power_int(_766916, _766914)), ord_less_nat(zero_zero_nat, _766914), -(dvd_dvd_int(_766912, _766916))], (4514 ^ _614856) ^ [_767304] : [zprime(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), _767304), one_one_int)), -(legendre(number_number_of_int(min), plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), _767304), one_one_int)) = one_one_int)], (4520 ^ _614856) ^ [_767522] : [ord_less_int(number_number_of_int(bit0(bit1(pls))), _767522), zcong(one_one_int, number_number_of_int(min), _767522)], (4526 ^ _614856) ^ [_767749, _767751] : [zcong(_767751, zero_zero_int, _767749), -(legendre(_767751, _767749) = zero_zero_int)], (4532 ^ _614856) ^ [_767919, _767921] : [-(zcong(_767921, zero_zero_int, _767919)), 4535 ^ _614856 : [(4536 ^ _614856) ^ [] : [quadRes(_767919, _767921), -(legendre(_767921, _767919) = one_one_int)], (4542 ^ _614856) ^ [] : [-(quadRes(_767919, _767921)), -(legendre(_767921, _767919) = number_number_of_int(min))]]], (4548 ^ _614856) ^ [_768433, _768435] : [quadRes(_768435, _768433), 4552 ^ _614856 : [(4553 ^ _614856) ^ [] : [-(is_int(4551 ^ [_768433, _768435]))], (4555 ^ _614856) ^ [] : [-(zcong(power_power_int(4551 ^ [_768433, _768435], number_number_of_nat(bit0(bit1(pls)))), _768433, _768435))]]], (4557 ^ _614856) ^ [_768749, _768751] : [-(quadRes(_768751, _768749)), 4558 ^ _614856 : [(4559 ^ _614856) ^ [_768844] : [is_int(_768844), zcong(power_power_int(_768844, number_number_of_nat(bit0(bit1(pls)))), _768749, _768751)]]], (4567 ^ _614856) ^ [_769107, _769109] : [-(power_power_real(plus_plus_real(_769109, _769107), number_number_of_nat(bit0(bit1(pls)))) = plus_plus_real(plus_plus_real(power_power_real(_769109, number_number_of_nat(bit0(bit1(pls)))), power_power_real(_769107, number_number_of_nat(bit0(bit1(pls))))), times_times_real(times_times_real(number267125858f_real(bit0(bit1(pls))), _769109), _769107)))], (4569 ^ _614856) ^ [_769260, _769262] : [_769260 = zero_zero_nat, -(times_times_nat(_769260, _769262) = zero_zero_nat)], (4575 ^ _614856) ^ [_769428, _769430] : [-(_769428 = zero_zero_nat), -(times_times_nat(_769428, _769430) = plus_plus_nat(_769430, times_times_nat(minus_minus_nat(_769428, one_one_nat), _769430)))], (4581 ^ _614856) ^ [_769687, _769689] : [_769687 = zero_zero_nat, -(power_power_nat(_769689, _769687) = one_one_nat)], (4587 ^ _614856) ^ [_769855, _769857] : [-(_769855 = zero_zero_nat), -(power_power_nat(_769857, _769855) = times_times_nat(_769857, power_power_nat(_769857, minus_minus_nat(_769855, one_one_nat))))], (4593 ^ _614856) ^ [_770079, _770081] : [-(minus_minus_nat(power_power_nat(_770081, number_number_of_nat(bit0(bit1(pls)))), power_power_nat(_770079, number_number_of_nat(bit0(bit1(pls))))) = times_times_nat(plus_plus_nat(_770081, _770079), minus_minus_nat(_770081, _770079)))], (4595 ^ _614856) ^ [_770235, _770237] : [plus_plus_real(power_power_real(_770237, number_number_of_nat(bit0(bit1(pls)))), power_power_real(_770235, number_number_of_nat(bit0(bit1(pls))))) = zero_zero_real, 4598 ^ _614856 : [(4599 ^ _614856) ^ [] : [-(_770237 = zero_zero_real)], (4601 ^ _614856) ^ [] : [-(_770235 = zero_zero_real)]]], (4603 ^ _614856) ^ [_770490, _770492] : [-(plus_plus_real(power_power_real(_770492, number_number_of_nat(bit0(bit1(pls)))), power_power_real(_770490, number_number_of_nat(bit0(bit1(pls))))) = zero_zero_real), _770492 = zero_zero_real, _770490 = zero_zero_real], (4613 ^ _614856) ^ [] : [zero_zero_real = one_one_real], (4615 ^ _614856) ^ [_770890, _770892] : [ord_less_eq_real(_770892, _770890), -(ord_less_eq_real(minus_minus_real(_770892, _770890), zero_zero_real))], (4621 ^ _614856) ^ [_771058, _771060] : [ord_less_eq_real(minus_minus_real(_771060, _771058), zero_zero_real), -(ord_less_eq_real(_771060, _771058))], (4627 ^ _614856) ^ [_771305, _771307] : [ord_less_real(_771307, _771305), 4630 ^ _614856 : [(4631 ^ _614856) ^ [] : [-(ord_less_eq_real(_771307, _771305))], (4633 ^ _614856) ^ [] : [_771307 = _771305]]], (4635 ^ _614856) ^ [_771543, _771545] : [-(ord_less_real(_771545, _771543)), ord_less_eq_real(_771545, _771543), -(_771545 = _771543)], (4655 ^ _614856) ^ [_772128, _772130] : [4656 ^ _614856 : [(4657 ^ _614856) ^ [] : [ord_less_real(_772130, _772128)], (4659 ^ _614856) ^ [] : [_772130 = _772128]], -(ord_less_eq_real(_772130, _772128))], (4645 ^ _614856) ^ [_771876, _771878] : [ord_less_eq_real(_771878, _771876), -(ord_less_real(_771878, _771876)), -(_771878 = _771876)], (4663 ^ _614856) ^ [_772413, _772415, _772417] : [-(times_times_real(times_times_real(_772417, _772415), _772413) = times_times_real(_772417, times_times_real(_772415, _772413)))], (4665 ^ _614856) ^ [_772521, _772523] : [-(times_times_real(_772523, _772521) = times_times_real(_772521, _772523))], (4667 ^ _614856) ^ [_772607] : [-(times_times_real(one_one_real, _772607) = _772607)], (4669 ^ _614856) ^ [_772731, _772733, _772735] : [ord_less_eq_real(_772733, _772731), -(ord_less_eq_real(plus_plus_real(_772735, _772733), plus_plus_real(_772735, _772731)))], (4675 ^ _614856) ^ [_772972, _772974, _772976, _772978] : [-(minus_minus_real(plus_plus_real(_772978, _772976), plus_plus_real(_772974, _772972)) = plus_plus_real(minus_minus_real(_772978, _772974), minus_minus_real(_772976, _772972)))], (4677 ^ _614856) ^ [_773116, _773118, _773120, _773122] : [-(minus_minus_int(plus_plus_int(_773122, _773120), plus_plus_int(_773118, _773116)) = plus_plus_int(minus_minus_int(_773122, _773118), minus_minus_int(_773120, _773116)))], (4679 ^ _614856) ^ [_773261, _773263, _773265] : [-(_773261 = zero_zero_real), 4682 ^ _614856 : [(4683 ^ _614856) ^ [] : [times_times_real(_773261, _773265) = times_times_real(_773261, _773263), -(_773265 = _773263)], (4689 ^ _614856) ^ [] : [_773265 = _773263, -(times_times_real(_773261, _773265) = times_times_real(_773261, _773263))]]], (4695 ^ _614856) ^ [_773772, _773774, _773776] : [-(_773772 = zero_zero_real), 4698 ^ _614856 : [(4699 ^ _614856) ^ [] : [times_times_real(_773776, _773772) = times_times_real(_773774, _773772), -(_773776 = _773774)], (4705 ^ _614856) ^ [] : [_773776 = _773774, -(times_times_real(_773776, _773772) = times_times_real(_773774, _773772))]]], (4711 ^ _614856) ^ [_774298, _774300] : [times_times_nat(_774300, _774298) = one_one_nat, 4714 ^ _614856 : [(4715 ^ _614856) ^ [] : [-(_774300 = one_one_nat)], (4717 ^ _614856) ^ [] : [-(_774298 = one_one_nat)]]], (4719 ^ _614856) ^ [_774541, _774543] : [-(times_times_nat(_774543, _774541) = one_one_nat), _774543 = one_one_nat, _774541 = one_one_nat], (4729 ^ _614856) ^ [_774847, _774849, _774851] : [-(times_times_real(plus_plus_real(_774851, _774849), _774847) = plus_plus_real(times_times_real(_774851, _774847), times_times_real(_774849, _774847)))], (4731 ^ _614856) ^ [_775002, _775004] : [power_power_nat(_775004, _775002) = zero_zero_nat, 4734 ^ _614856 : [(4735 ^ _614856) ^ [] : [_775002 = zero_zero_nat], (4737 ^ _614856) ^ [] : [-(_775004 = zero_zero_nat)]]], (4739 ^ _614856) ^ [_775246, _775248] : [-(power_power_nat(_775248, _775246) = zero_zero_nat), -(_775246 = zero_zero_nat), _775248 = zero_zero_nat], (4749 ^ _614856) ^ [_775569, _775571, _775573, _775575] : [-(minus_minus_real(times_times_real(_775575, _775573), times_times_real(_775571, _775569)) = plus_plus_real(times_times_real(_775575, minus_minus_real(_775573, _775569)), times_times_real(minus_minus_real(_775575, _775571), _775569)))], (4751 ^ _614856) ^ [_775719, _775721, _775723, _775725] : [-(minus_minus_int(times_times_int(_775725, _775723), times_times_int(_775721, _775719)) = plus_plus_int(times_times_int(_775725, minus_minus_int(_775723, _775719)), times_times_int(minus_minus_int(_775725, _775721), _775719)))], (4753 ^ _614856) ^ [_775870, _775872, _775874] : [ord_less_real(zero_zero_real, _775870), 4756 ^ _614856 : [(4757 ^ _614856) ^ [] : [ord_less_eq_real(times_times_real(_775874, _775870), times_times_real(_775872, _775870)), -(ord_less_eq_real(_775874, _775872))], (4763 ^ _614856) ^ [] : [ord_less_eq_real(_775874, _775872), -(ord_less_eq_real(times_times_real(_775874, _775870), times_times_real(_775872, _775870)))]]], (4769 ^ _614856) ^ [_776378, _776380, _776382] : [ord_less_real(zero_zero_real, _776378), 4772 ^ _614856 : [(4773 ^ _614856) ^ [] : [ord_less_eq_real(times_times_real(_776378, _776382), times_times_real(_776378, _776380)), -(ord_less_eq_real(_776382, _776380))], (4779 ^ _614856) ^ [] : [ord_less_eq_real(_776382, _776380), -(ord_less_eq_real(times_times_real(_776378, _776382), times_times_real(_776378, _776380)))]]], (4785 ^ _614856) ^ [_776886, _776888, _776890] : [ord_less_real(zero_zero_real, _776886), ord_less_real(_776890, _776888), -(ord_less_real(times_times_real(_776886, _776890), times_times_real(_776886, _776888)))], (4795 ^ _614856) ^ [_777207, _777209] : [ord_less_real(zero_zero_real, _777207), ord_less_real(zero_zero_real, _777209), -(ord_less_real(zero_zero_real, times_times_real(_777207, _777209)))], (4805 ^ _614856) ^ [_777526, _777528, _777530] : [ord_less_real(zero_zero_real, _777526), 4808 ^ _614856 : [(4809 ^ _614856) ^ [] : [ord_less_real(times_times_real(_777530, _777526), times_times_real(_777528, _777526)), -(ord_less_real(_777530, _777528))], (4815 ^ _614856) ^ [] : [ord_less_real(_777530, _777528), -(ord_less_real(times_times_real(_777530, _777526), times_times_real(_777528, _777526)))]]], (4821 ^ _614856) ^ [_778049, _778051] : [plus_plus_real(times_times_real(_778051, _778051), times_times_real(_778049, _778049)) = zero_zero_real, 4824 ^ _614856 : [(4825 ^ _614856) ^ [] : [-(_778051 = zero_zero_real)], (4827 ^ _614856) ^ [] : [-(_778049 = zero_zero_real)]]], (4829 ^ _614856) ^ [_778304, _778306] : [-(plus_plus_real(times_times_real(_778306, _778306), times_times_real(_778304, _778304)) = zero_zero_real), _778306 = zero_zero_real, _778304 = zero_zero_real], (4849 ^ _614856) ^ [_778910, _778912] : [4850 ^ _614856 : [(4851 ^ _614856) ^ [] : [_778912 = one_one_nat], (4853 ^ _614856) ^ [] : [_778910 = zero_zero_nat]], -(power_power_nat(_778912, _778910) = one_one_nat)], (4839 ^ _614856) ^ [_778652, _778654] : [power_power_nat(_778654, _778652) = one_one_nat, -(_778654 = one_one_nat), -(_778652 = zero_zero_nat)], (4857 ^ _614856) ^ [_779173] : [-(minus_minus_real(times_times_real(_779173, _779173), one_one_real) = times_times_real(plus_plus_real(_779173, one_one_real), minus_minus_real(_779173, one_one_real)))], (4859 ^ _614856) ^ [_779266] : [-(minus_minus_int(times_times_int(_779266, _779266), one_one_int) = times_times_int(plus_plus_int(_779266, one_one_int), minus_minus_int(_779266, one_one_int)))], (4861 ^ _614856) ^ [_779388, _779390] : [ord_less_nat(zero_zero_nat, _779388), -(times_times_real(power_power_real(_779390, minus_minus_nat(_779388, one_one_nat)), _779390) = power_power_real(_779390, _779388))], (4867 ^ _614856) ^ [_779622, _779624] : [ord_less_nat(zero_zero_nat, _779622), -(times_times_nat(power_power_nat(_779624, minus_minus_nat(_779622, one_one_nat)), _779624) = power_power_nat(_779624, _779622))], (4873 ^ _614856) ^ [_779856, _779858] : [ord_less_nat(zero_zero_nat, _779856), -(times_times_int(power_power_int(_779858, minus_minus_nat(_779856, one_one_nat)), _779858) = power_power_int(_779858, _779856))], (4879 ^ _614856) ^ [_780061] : [-(ord_less_eq_real(one_one_real, power_power_real(number267125858f_real(bit0(bit1(pls))), _780061)))], (4881 ^ _614856) ^ [_780191, _780193] : [_780191 = zero_zero_nat, -(power_power_real(_780193, _780191) = one_one_real)], (4887 ^ _614856) ^ [_780359, _780361] : [-(_780359 = zero_zero_nat), -(power_power_real(_780361, _780359) = times_times_real(_780361, power_power_real(_780361, minus_minus_nat(_780359, one_one_nat))))], (4893 ^ _614856) ^ [_780618, _780620] : [_780618 = zero_zero_nat, -(power_power_nat(_780620, _780618) = one_one_nat)], (4899 ^ _614856) ^ [_780786, _780788] : [-(_780786 = zero_zero_nat), -(power_power_nat(_780788, _780786) = times_times_nat(_780788, power_power_nat(_780788, minus_minus_nat(_780786, one_one_nat))))], (4905 ^ _614856) ^ [_781045, _781047] : [_781045 = zero_zero_nat, -(power_power_int(_781047, _781045) = one_one_int)], (4911 ^ _614856) ^ [_781213, _781215] : [-(_781213 = zero_zero_nat), -(power_power_int(_781215, _781213) = times_times_int(_781215, power_power_int(_781215, minus_minus_nat(_781213, one_one_nat))))], (4917 ^ _614856) ^ [_781466, _781468, _781470] : [ord_less_real(_781468, _781466), ord_less_eq_real(zero_zero_real, _781468), ord_less_nat(zero_zero_nat, _781470), -(ord_less_real(power_power_real(_781468, _781470), power_power_real(_781466, _781470)))], (4931 ^ _614856) ^ [_781894, _781896, _781898] : [ord_less_nat(_781896, _781894), ord_less_eq_nat(zero_zero_nat, _781896), ord_less_nat(zero_zero_nat, _781898), -(ord_less_nat(power_power_nat(_781896, _781898), power_power_nat(_781894, _781898)))], (4945 ^ _614856) ^ [_782322, _782324, _782326] : [ord_less_int(_782324, _782322), ord_less_eq_int(zero_zero_int, _782324), ord_less_nat(zero_zero_nat, _782326), -(ord_less_int(power_power_int(_782324, _782326), power_power_int(_782322, _782326)))], (4959 ^ _614856) ^ [_782707] : [-(ord_less_eq_real(_782707, _782707))], (4961 ^ _614856) ^ [_782814, _782816] : [-(ord_less_eq_real(_782816, _782814)), -(ord_less_eq_real(_782814, _782816))], (4967 ^ _614856) ^ [_783039, _783041, _783043] : [ord_less_eq_real(_783041, _783039), ord_less_eq_real(_783039, _783043), -(ord_less_eq_real(_783041, _783043))], (4977 ^ _614856) ^ [_783348, _783350] : [ord_less_eq_real(_783350, _783348), ord_less_eq_real(_783348, _783350), -(_783350 = _783348)], (4987 ^ _614856) ^ [_783647, _783649] : [-(_783647 = zero_zero_real), power_power_real(_783647, _783649) = zero_zero_real], (4993 ^ _614856) ^ [_783867, _783869] : [is_int(_783867), -(_783867 = zero_zero_int), power_power_int(_783867, _783869) = zero_zero_int], (5003 ^ _614856) ^ [_784173, _784175, _784177] : [-(power_power_real(times_times_real(_784177, _784175), _784173) = times_times_real(power_power_real(_784177, _784173), power_power_real(_784175, _784173)))], (5005 ^ _614856) ^ [_784298, _784300, _784302] : [-(power_power_nat(times_times_nat(_784302, _784300), _784298) = times_times_nat(power_power_nat(_784302, _784298), power_power_nat(_784300, _784298)))], (5007 ^ _614856) ^ [_784423, _784425, _784427] : [-(power_power_int(times_times_int(_784427, _784425), _784423) = times_times_int(power_power_int(_784427, _784423), power_power_int(_784425, _784423)))], (5009 ^ _614856) ^ [_784534, _784536] : [-(times_times_real(power_power_real(_784536, _784534), _784536) = times_times_real(_784536, power_power_real(_784536, _784534)))], (5011 ^ _614856) ^ [_784640, _784642] : [-(times_times_nat(power_power_nat(_784642, _784640), _784642) = times_times_nat(_784642, power_power_nat(_784642, _784640)))], (5013 ^ _614856) ^ [_784746, _784748] : [-(times_times_int(power_power_int(_784748, _784746), _784748) = times_times_int(_784748, power_power_int(_784748, _784746)))], (5015 ^ _614856) ^ [_784838] : [-(power_power_real(one_one_real, _784838) = one_one_real)], (5017 ^ _614856) ^ [_784919] : [-(power_power_nat(one_one_nat, _784919) = one_one_nat)], (5019 ^ _614856) ^ [_785000] : [-(power_power_int(one_one_int, _785000) = one_one_int)], (5021 ^ _614856) ^ [_785124, _785126, _785128] : [dvd_dvd_nat(_785126, _785124), -(dvd_dvd_nat(power_power_nat(_785126, _785128), power_power_nat(_785124, _785128)))], (5027 ^ _614856) ^ [_785366, _785368, _785370] : [dvd_dvd_int(_785368, _785366), -(dvd_dvd_int(power_power_int(_785368, _785370), power_power_int(_785366, _785370)))], (5033 ^ _614856) ^ [_785608, _785610, _785612] : [dvd_dvd_real(_785610, _785608), -(dvd_dvd_real(power_power_real(_785610, _785612), power_power_real(_785608, _785612)))], (5039 ^ _614856) ^ [_785835, _785837, _785839] : [-(power_power_real(_785839, times_times_nat(_785837, _785835)) = power_power_real(power_power_real(_785839, _785837), _785835))], (5041 ^ _614856) ^ [_785957, _785959, _785961] : [-(power_power_nat(_785961, times_times_nat(_785959, _785957)) = power_power_nat(power_power_nat(_785961, _785959), _785957))], (5043 ^ _614856) ^ [_786079, _786081, _786083] : [-(power_power_int(_786083, times_times_nat(_786081, _786079)) = power_power_int(power_power_int(_786083, _786081), _786079))], (5045 ^ _614856) ^ [_786173] : [-(power_power_real(_786173, one_one_nat) = _786173)], (5047 ^ _614856) ^ [_786254] : [-(power_power_nat(_786254, one_one_nat) = _786254)], (5049 ^ _614856) ^ [_786350] : [is_int(_786350), -(power_power_int(_786350, one_one_nat) = _786350)], (5055 ^ _614856) ^ [_786572, _786574, _786576] : [ord_less_eq_real(_786574, _786572), ord_less_eq_real(zero_zero_real, _786574), -(ord_less_eq_real(power_power_real(_786574, _786576), power_power_real(_786572, _786576)))], (5065 ^ _614856) ^ [_786907, _786909, _786911] : [ord_less_eq_nat(_786909, _786907), ord_less_eq_nat(zero_zero_nat, _786909), -(ord_less_eq_nat(power_power_nat(_786909, _786911), power_power_nat(_786907, _786911)))], (5075 ^ _614856) ^ [_787242, _787244, _787246] : [ord_less_eq_int(_787244, _787242), ord_less_eq_int(zero_zero_int, _787244), -(ord_less_eq_int(power_power_int(_787244, _787246), power_power_int(_787242, _787246)))], (5085 ^ _614856) ^ [_787563, _787565] : [ord_less_eq_real(zero_zero_real, _787563), -(ord_less_eq_real(zero_zero_real, power_power_real(_787563, _787565)))], (5091 ^ _614856) ^ [_787779, _787781] : [ord_less_eq_nat(zero_zero_nat, _787779), -(ord_less_eq_nat(zero_zero_nat, power_power_nat(_787779, _787781)))], (5097 ^ _614856) ^ [_787995, _787997] : [ord_less_eq_int(zero_zero_int, _787995), -(ord_less_eq_int(zero_zero_int, power_power_int(_787995, _787997)))], (5103 ^ _614856) ^ [_788211, _788213] : [ord_less_real(zero_zero_real, _788211), -(ord_less_real(zero_zero_real, power_power_real(_788211, _788213)))], (5109 ^ _614856) ^ [_788427, _788429] : [ord_less_nat(zero_zero_nat, _788427), -(ord_less_nat(zero_zero_nat, power_power_nat(_788427, _788429)))], (5115 ^ _614856) ^ [_788643, _788645] : [ord_less_int(zero_zero_int, _788643), -(ord_less_int(zero_zero_int, power_power_int(_788643, _788645)))], (5121 ^ _614856) ^ [_788859, _788861] : [ord_less_eq_real(one_one_real, _788859), -(ord_less_eq_real(one_one_real, power_power_real(_788859, _788861)))], (5127 ^ _614856) ^ [_789075, _789077] : [ord_less_eq_nat(one_one_nat, _789075), -(ord_less_eq_nat(one_one_nat, power_power_nat(_789075, _789077)))], (5133 ^ _614856) ^ [_789291, _789293] : [ord_less_eq_int(one_one_int, _789291), -(ord_less_eq_int(one_one_int, power_power_int(_789291, _789293)))], (5139 ^ _614856) ^ [_789521, _789523, _789525] : [ord_less_real(one_one_real, _789521), 5142 ^ _614856 : [(5143 ^ _614856) ^ [] : [power_power_real(_789521, _789525) = power_power_real(_789521, _789523), -(_789525 = _789523)], (5149 ^ _614856) ^ [] : [_789525 = _789523, -(power_power_real(_789521, _789525) = power_power_real(_789521, _789523))]]], (5155 ^ _614856) ^ [_790029, _790031, _790033] : [ord_less_nat(one_one_nat, _790029), 5158 ^ _614856 : [(5159 ^ _614856) ^ [] : [power_power_nat(_790029, _790033) = power_power_nat(_790029, _790031), -(_790033 = _790031)], (5165 ^ _614856) ^ [] : [_790033 = _790031, -(power_power_nat(_790029, _790033) = power_power_nat(_790029, _790031))]]], (5171 ^ _614856) ^ [_790537, _790539, _790541] : [ord_less_int(one_one_int, _790537), 5174 ^ _614856 : [(5175 ^ _614856) ^ [] : [power_power_int(_790537, _790541) = power_power_int(_790537, _790539), -(_790541 = _790539)], (5181 ^ _614856) ^ [] : [_790541 = _790539, -(power_power_int(_790537, _790541) = power_power_int(_790537, _790539))]]], (5187 ^ _614856) ^ [_791060, _791062] : [power_power_real(_791062, _791060) = zero_zero_real, 5190 ^ _614856 : [(5191 ^ _614856) ^ [] : [-(_791062 = zero_zero_real)], (5193 ^ _614856) ^ [] : [_791060 = zero_zero_nat]]], (5195 ^ _614856) ^ [_791304, _791306] : [-(power_power_real(_791306, _791304) = zero_zero_real), _791306 = zero_zero_real, -(_791304 = zero_zero_nat)], (5205 ^ _614856) ^ [_791643, _791645] : [power_power_nat(_791645, _791643) = zero_zero_nat, 5208 ^ _614856 : [(5209 ^ _614856) ^ [] : [-(_791645 = zero_zero_nat)], (5211 ^ _614856) ^ [] : [_791643 = zero_zero_nat]]], (5213 ^ _614856) ^ [_791887, _791889] : [-(power_power_nat(_791889, _791887) = zero_zero_nat), _791889 = zero_zero_nat, -(_791887 = zero_zero_nat)], (5223 ^ _614856) ^ [_792197, _792199] : [is_int(_792199), 5226 ^ _614856 : [(5227 ^ _614856) ^ [] : [power_power_int(_792199, _792197) = zero_zero_int, 5230 ^ _614856 : [(5231 ^ _614856) ^ [] : [-(_792199 = zero_zero_int)], (5233 ^ _614856) ^ [] : [_792197 = zero_zero_nat]]], (5235 ^ _614856) ^ [] : [-(power_power_int(_792199, _792197) = zero_zero_int), _792199 = zero_zero_int, -(_792197 = zero_zero_nat)]]], (5245 ^ _614856) ^ [_792795] : [-(power_power_real(_792795, zero_zero_nat) = one_one_real)], (5247 ^ _614856) ^ [_792876] : [-(power_power_nat(_792876, zero_zero_nat) = one_one_nat)], (5249 ^ _614856) ^ [_792957] : [-(power_power_int(_792957, zero_zero_nat) = one_one_int)], (5251 ^ _614856) ^ [_793066, _793068, _793070] : [-(power_power_real(_793070, plus_plus_nat(_793068, _793066)) = times_times_real(power_power_real(_793070, _793068), power_power_real(_793070, _793066)))], (5253 ^ _614856) ^ [_793191, _793193, _793195] : [-(power_power_nat(_793195, plus_plus_nat(_793193, _793191)) = times_times_nat(power_power_nat(_793195, _793193), power_power_nat(_793195, _793191)))], (5255 ^ _614856) ^ [_793316, _793318, _793320] : [-(power_power_int(_793320, plus_plus_nat(_793318, _793316)) = times_times_int(power_power_int(_793320, _793318), power_power_int(_793320, _793316)))], (5257 ^ _614856) ^ [_793470, _793472, _793474, _793476] : [dvd_dvd_nat(power_power_nat(_793474, _793472), _793470), ord_less_eq_nat(_793476, _793472), -(dvd_dvd_nat(power_power_nat(_793474, _793476), _793470))], (5267 ^ _614856) ^ [_793829, _793831, _793833, _793835] : [dvd_dvd_int(power_power_int(_793833, _793831), _793829), ord_less_eq_nat(_793835, _793831), -(dvd_dvd_int(power_power_int(_793833, _793835), _793829))], (5277 ^ _614856) ^ [_794188, _794190, _794192, _794194] : [dvd_dvd_real(power_power_real(_794192, _794190), _794188), ord_less_eq_nat(_794194, _794190), -(dvd_dvd_real(power_power_real(_794192, _794194), _794188))], (5287 ^ _614856) ^ [_794547, _794549, _794551, _794553] : [dvd_dvd_nat(_794549, _794547), ord_less_eq_nat(_794553, _794551), -(dvd_dvd_nat(power_power_nat(_794549, _794553), power_power_nat(_794547, _794551)))], (5297 ^ _614856) ^ [_794906, _794908, _794910, _794912] : [dvd_dvd_int(_794908, _794906), ord_less_eq_nat(_794912, _794910), -(dvd_dvd_int(power_power_int(_794908, _794912), power_power_int(_794906, _794910)))], (5307 ^ _614856) ^ [_795265, _795267, _795269, _795271] : [dvd_dvd_real(_795267, _795265), ord_less_eq_nat(_795271, _795269), -(dvd_dvd_real(power_power_real(_795267, _795271), power_power_real(_795265, _795269)))], (5317 ^ _614856) ^ [_795610, _795612, _795614] : [ord_less_eq_nat(_795612, _795610), -(dvd_dvd_nat(power_power_nat(_795614, _795612), power_power_nat(_795614, _795610)))], (5323 ^ _614856) ^ [_795852, _795854, _795856] : [ord_less_eq_nat(_795854, _795852), -(dvd_dvd_int(power_power_int(_795856, _795854), power_power_int(_795856, _795852)))], (5329 ^ _614856) ^ [_796094, _796096, _796098] : [ord_less_eq_nat(_796096, _796094), -(dvd_dvd_real(power_power_real(_796098, _796096), power_power_real(_796098, _796094)))], (5335 ^ _614856) ^ [_796336, _796338, _796340] : [ord_less_nat(zero_zero_nat, _796336), ord_less_nat(power_power_nat(_796336, _796340), power_power_nat(_796336, _796338)), -(ord_less_nat(_796340, _796338))], (5355 ^ _614856) ^ [_796944, _796946] : [5356 ^ _614856 : [(5357 ^ _614856) ^ [] : [ord_less_nat(zero_zero_nat, _796946)], (5359 ^ _614856) ^ [] : [_796944 = zero_zero_nat]], -(ord_less_nat(zero_zero_nat, power_power_nat(_796946, _796944)))], (5345 ^ _614856) ^ [_796686, _796688] : [ord_less_nat(zero_zero_nat, power_power_nat(_796688, _796686)), -(ord_less_nat(zero_zero_nat, _796688)), -(_796686 = zero_zero_nat)], (5363 ^ _614856) ^ [_797250, _797252, _797254] : [ord_less_real(power_power_real(_797254, _797252), power_power_real(_797250, _797252)), ord_less_eq_real(zero_zero_real, _797250), -(ord_less_real(_797254, _797250))], (5373 ^ _614856) ^ [_797585, _797587, _797589] : [ord_less_nat(power_power_nat(_797589, _797587), power_power_nat(_797585, _797587)), ord_less_eq_nat(zero_zero_nat, _797585), -(ord_less_nat(_797589, _797585))], (5383 ^ _614856) ^ [_797920, _797922, _797924] : [ord_less_int(power_power_int(_797924, _797922), power_power_int(_797920, _797922)), ord_less_eq_int(zero_zero_int, _797920), -(ord_less_int(_797924, _797920))], (5393 ^ _614856) ^ [_798241, _798243] : [ord_less_real(one_one_real, _798241), -(ord_less_real(power_power_real(_798241, _798243), times_times_real(_798241, power_power_real(_798241, _798243))))], (5399 ^ _614856) ^ [_798469, _798471] : [ord_less_nat(one_one_nat, _798469), -(ord_less_nat(power_power_nat(_798469, _798471), times_times_nat(_798469, power_power_nat(_798469, _798471))))], (5405 ^ _614856) ^ [_798697, _798699] : [ord_less_int(one_one_int, _798697), -(ord_less_int(power_power_int(_798697, _798699), times_times_int(_798697, power_power_int(_798697, _798699))))], (5411 ^ _614856) ^ [_798925, _798927] : [ord_less_real(one_one_real, _798925), -(ord_less_real(one_one_real, times_times_real(_798925, power_power_real(_798925, _798927))))], (5417 ^ _614856) ^ [_799147, _799149] : [ord_less_nat(one_one_nat, _799147), -(ord_less_nat(one_one_nat, times_times_nat(_799147, power_power_nat(_799147, _799149))))], (5423 ^ _614856) ^ [_799369, _799371] : [ord_less_int(one_one_int, _799369), -(ord_less_int(one_one_int, times_times_int(_799369, power_power_int(_799369, _799371))))], (5429 ^ _614856) ^ [_799597] : [_799597 = zero_zero_nat, -(power_power_real(zero_zero_real, _799597) = one_one_real)], (5435 ^ _614856) ^ [_799759] : [-(_799759 = zero_zero_nat), -(power_power_real(zero_zero_real, _799759) = zero_zero_real)], (5441 ^ _614856) ^ [_799980] : [_799980 = zero_zero_nat, -(power_power_nat(zero_zero_nat, _799980) = one_one_nat)], (5447 ^ _614856) ^ [_800142] : [-(_800142 = zero_zero_nat), -(power_power_nat(zero_zero_nat, _800142) = zero_zero_nat)], (5453 ^ _614856) ^ [_800363] : [_800363 = zero_zero_nat, -(power_power_int(zero_zero_int, _800363) = one_one_int)], (5459 ^ _614856) ^ [_800525] : [-(_800525 = zero_zero_nat), -(power_power_int(zero_zero_int, _800525) = zero_zero_int)], (5465 ^ _614856) ^ [_800754, _800756, _800758] : [ord_less_nat(_800756, _800754), ord_less_real(one_one_real, _800758), -(ord_less_real(power_power_real(_800758, _800756), power_power_real(_800758, _800754)))], (5475 ^ _614856) ^ [_801089, _801091, _801093] : [ord_less_nat(_801091, _801089), ord_less_nat(one_one_nat, _801093), -(ord_less_nat(power_power_nat(_801093, _801091), power_power_nat(_801093, _801089)))], (5485 ^ _614856) ^ [_801424, _801426, _801428] : [ord_less_nat(_801426, _801424), ord_less_int(one_one_int, _801428), -(ord_less_int(power_power_int(_801428, _801426), power_power_int(_801428, _801424)))], (5495 ^ _614856) ^ [_801759, _801761, _801763] : [ord_less_real(one_one_real, _801759), ord_less_real(power_power_real(_801759, _801763), power_power_real(_801759, _801761)), -(ord_less_nat(_801763, _801761))], (5505 ^ _614856) ^ [_802094, _802096, _802098] : [ord_less_nat(one_one_nat, _802094), ord_less_nat(power_power_nat(_802094, _802098), power_power_nat(_802094, _802096)), -(ord_less_nat(_802098, _802096))], (5515 ^ _614856) ^ [_802429, _802431, _802433] : [ord_less_int(one_one_int, _802429), ord_less_int(power_power_int(_802429, _802433), power_power_int(_802429, _802431)), -(ord_less_nat(_802433, _802431))], (5525 ^ _614856) ^ [_802764, _802766, _802768] : [ord_less_real(one_one_real, _802764), 5528 ^ _614856 : [(5529 ^ _614856) ^ [] : [ord_less_real(power_power_real(_802764, _802768), power_power_real(_802764, _802766)), -(ord_less_nat(_802768, _802766))], (5535 ^ _614856) ^ [] : [ord_less_nat(_802768, _802766), -(ord_less_real(power_power_real(_802764, _802768), power_power_real(_802764, _802766)))]]], (5541 ^ _614856) ^ [_803272, _803274, _803276] : [ord_less_nat(one_one_nat, _803272), 5544 ^ _614856 : [(5545 ^ _614856) ^ [] : [ord_less_nat(power_power_nat(_803272, _803276), power_power_nat(_803272, _803274)), -(ord_less_nat(_803276, _803274))], (5551 ^ _614856) ^ [] : [ord_less_nat(_803276, _803274), -(ord_less_nat(power_power_nat(_803272, _803276), power_power_nat(_803272, _803274)))]]], (5557 ^ _614856) ^ [_803780, _803782, _803784] : [ord_less_int(one_one_int, _803780), 5560 ^ _614856 : [(5561 ^ _614856) ^ [] : [ord_less_int(power_power_int(_803780, _803784), power_power_int(_803780, _803782)), -(ord_less_nat(_803784, _803782))], (5567 ^ _614856) ^ [] : [ord_less_nat(_803784, _803782), -(ord_less_int(power_power_int(_803780, _803784), power_power_int(_803780, _803782)))]]], (5573 ^ _614856) ^ [_804288, _804290, _804292] : [ord_less_eq_nat(_804290, _804288), ord_less_eq_real(one_one_real, _804292), -(ord_less_eq_real(power_power_real(_804292, _804290), power_power_real(_804292, _804288)))], (5583 ^ _614856) ^ [_804623, _804625, _804627] : [ord_less_eq_nat(_804625, _804623), ord_less_eq_nat(one_one_nat, _804627), -(ord_less_eq_nat(power_power_nat(_804627, _804625), power_power_nat(_804627, _804623)))], (5593 ^ _614856) ^ [_804958, _804960, _804962] : [ord_less_eq_nat(_804960, _804958), ord_less_eq_int(one_one_int, _804962), -(ord_less_eq_int(power_power_int(_804962, _804960), power_power_int(_804962, _804958)))], (5603 ^ _614856) ^ [_805279, _805281] : [ord_less_real(zero_zero_real, _805279), ord_less_real(_805279, one_one_real), -(ord_less_real(times_times_real(_805279, power_power_real(_805279, _805281)), power_power_real(_805279, _805281)))], (5613 ^ _614856) ^ [_805596, _805598] : [ord_less_nat(zero_zero_nat, _805596), ord_less_nat(_805596, one_one_nat), -(ord_less_nat(times_times_nat(_805596, power_power_nat(_805596, _805598)), power_power_nat(_805596, _805598)))], (5623 ^ _614856) ^ [_805913, _805915] : [ord_less_int(zero_zero_int, _805913), ord_less_int(_805913, one_one_int), -(ord_less_int(times_times_int(_805913, power_power_int(_805913, _805915)), power_power_int(_805913, _805915)))], (5633 ^ _614856) ^ [_806244, _806246, _806248] : [ord_less_nat(_806246, _806244), ord_less_int(zero_zero_int, _806248), ord_less_int(_806248, one_one_int), -(ord_less_int(power_power_int(_806248, _806244), power_power_int(_806248, _806246)))], (5647 ^ _614856) ^ [_806658, _806660] : [ord_less_nat(zero_zero_nat, _806658), ord_less_real(zero_zero_real, _806660), 5655 ^ _614856 : [(5656 ^ _614856) ^ [] : [-(ord_less_real(zero_zero_real, 5654 ^ [_806658, _806660]))], (5658 ^ _614856) ^ [] : [-(power_power_real(5654 ^ [_806658, _806660], _806658) = _806660)], (5660 ^ _614856) ^ [_807138] : [-(_807138 = 5654 ^ [_806658, _806660]), ord_less_real(zero_zero_real, _807138), power_power_real(_807138, _806658) = _806660]]], (5670 ^ _614856) ^ [_807484, _807486] : [dvd_dvd_nat(_807486, _807484), -(_807484 = zero_zero_nat), -(ord_less_eq_nat(_807486, _807484))], (5680 ^ _614856) ^ [_807798, _807800, _807802] : [dvd_dvd_nat(_807800, _807798), -(dvd_dvd_nat(power_power_nat(_807800, _807802), power_power_nat(_807798, _807802)))], (5686 ^ _614856) ^ [_808040, _808042, _808044] : [dvd_dvd_nat(_808042, _808040), -(dvd_dvd_nat(times_times_nat(_808044, _808042), times_times_nat(_808044, _808040)))], (5692 ^ _614856) ^ [_808282, _808284, _808286] : [dvd_dvd_nat(_808284, _808282), -(dvd_dvd_nat(times_times_nat(_808284, _808286), times_times_nat(_808282, _808286)))], (5698 ^ _614856) ^ [_808524, _808526, _808528] : [dvd_dvd_nat(_808526, _808524), dvd_dvd_nat(_808526, plus_plus_nat(_808524, _808528)), -(dvd_dvd_nat(_808526, _808528))], (5718 ^ _614856) ^ [_809156, _809158, _809160] : [5719 ^ _614856 : [(5720 ^ _614856) ^ [] : [_809158 = zero_zero_nat], (5722 ^ _614856) ^ [] : [dvd_dvd_nat(_809160, _809156)]], -(dvd_dvd_nat(times_times_nat(_809160, _809158), times_times_nat(_809156, _809158)))], (5708 ^ _614856) ^ [_808882, _808884, _808886] : [dvd_dvd_nat(times_times_nat(_808886, _808884), times_times_nat(_808882, _808884)), -(_808884 = zero_zero_nat), -(dvd_dvd_nat(_808886, _808882))], (5726 ^ _614856) ^ [_809476, _809478, _809480] : [dvd_dvd_nat(power_power_nat(_809480, _809478), power_power_nat(_809476, _809478)), -(_809478 = zero_zero_nat), -(dvd_dvd_nat(_809480, _809476))], (5736 ^ _614856) ^ [_809814, _809816, _809818] : [-(_809814 = zero_zero_nat), dvd_dvd_nat(power_power_nat(_809818, _809814), _809816), -(dvd_dvd_nat(_809818, _809816))], (5746 ^ _614856) ^ [_810160, _810162, _810164, _810166] : [_810166 = plus_plus_nat(times_times_nat(_810164, _810162), _810160), ord_less_nat(zero_zero_nat, _810160), ord_less_nat(_810160, _810162), dvd_dvd_nat(_810162, _810166)], (5760 ^ _614856) ^ [_810603, _810605, _810607] : [dvd_dvd_nat(power_power_nat(_810607, _810605), power_power_nat(_810607, _810603)), ord_less_nat(one_one_nat, _810607), -(ord_less_eq_nat(_810605, _810603))], (5770 ^ _614856) ^ [_810904, _810906] : [dvd_dvd_nat(_810906, _810904), -(_810904 = zero_zero_nat), -(_810904 = _810906), -(ord_less_eq_nat(times_times_nat(number_number_of_nat(bit0(bit1(pls))), _810906), _810904))]], input).
% 101.32/98.59 ncf('1',plain,[ord_less_int(plus_plus_int(power_power_int(s, number_number_of_nat(bit0(bit1(pls)))), one_one_int), zero_zero_int)],start(5784 ^ 0)).
% 101.32/98.59 ncf('1.1',plain,[-(ord_less_int(plus_plus_int(power_power_int(s, number_number_of_nat(bit0(bit1(pls)))), one_one_int), zero_zero_int)), ord_less_int(times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), m), one_one_int), t), times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), m), one_one_int), zero_zero_int)), times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), m), one_one_int), t) = plus_plus_int(power_power_int(s, number_number_of_nat(bit0(bit1(pls)))), one_one_int), times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), m), one_one_int), zero_zero_int) = zero_zero_int],extension(194 ^ 1,bind([[_621122, _621124, _621126, _621128], [zero_zero_int, times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), m), one_one_int), zero_zero_int), plus_plus_int(power_power_int(s, number_number_of_nat(bit0(bit1(pls)))), one_one_int), times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), m), one_one_int), t)]]))).
% 101.32/98.59 ncf('1.1.1',plain,[-(ord_less_int(times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), m), one_one_int), t), times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), m), one_one_int), zero_zero_int)))],extension(460 ^ 2)).
% 101.32/98.59 ncf('1.1.2',plain,[-(times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), m), one_one_int), t) = plus_plus_int(power_power_int(s, number_number_of_nat(bit0(bit1(pls)))), one_one_int)), plus_plus_int(power_power_int(s, number_number_of_nat(bit0(bit1(pls)))), one_one_int) = times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), m), one_one_int), t)],extension(4 ^ 2,bind([[_615107, _615109], [times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), m), one_one_int), t), plus_plus_int(power_power_int(s, number_number_of_nat(bit0(bit1(pls)))), one_one_int)]]))).
% 101.32/98.59 ncf('1.1.2.1',plain,[-(plus_plus_int(power_power_int(s, number_number_of_nat(bit0(bit1(pls)))), one_one_int) = times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), m), one_one_int), t))],extension(462 ^ 3)).
% 101.32/98.59 ncf('1.1.3',plain,[-(times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), m), one_one_int), zero_zero_int) = zero_zero_int)],extension(2887 ^ 2,bind([[_712860], [plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))), m), one_one_int)]]))).
% 101.32/98.59 %-----------------------------------------------------
% 101.32/98.59 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------