%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : NUM925+4 : TPTP v9.2.1. Released v5.3.0. % Transfm : none % Format : tptp % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n025.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 : Thu May 7 07:30:52 PM UTC 2026 % Result : Unknown 1.51s 0.88s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : NUM925+4 : TPTP v9.2.1. Released v5.3.0. % 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.17/0.34 % Computer : n025.cluster.edu % 0.17/0.34 % Model : x86_64 x86_64 % 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.34 % Memory : 8042.1875MB % 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.34 % CPULimit : 300 % 0.17/0.34 % WCLimit : 300 % 0.17/0.34 % DateTime : Thu May 7 12:54:14 EDT 2026 % 0.17/0.34 % CPUTime : % 0.17/0.34 SPASS-SCL-FOL version: % 0.20/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 1.51/0.84 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 1.51/0.84 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 1.51/0.84 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 1.51/0.84 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 1.51/0.84 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 1.51/0.84 Execution normal ended with status: gaveup % 1.51/0.84 Execution resolution_1 ended with status: gaveup % 1.51/0.84 Execution resolution_2 ended with status: gaveup % 1.51/0.84 Execution resolution_3 ended with status: gaveup % 1.51/0.84 Execution lmodel_grow ended with status: gaveup % 1.51/0.84 No successful execution. % 1.51/0.84 % 1.51/0.84 Input Clauses: % 1.51/0.87 % 1.51/0.87 Predicates: is_int is_bool hBOOL = ren1 ren2 ren3 ren4 ren5 ren6 ren7 ren8 ren9 ren10 ren11 ren12 ren13 ren14 ren15 ren16 ren17 ren18 ren19 ren20 ren21 ren22 ren23 ren24 ren25 ren26 ren27 ren28 ren29 ren30 ren31 ren32 ren33 ren34 ren35 ren36 ren37 ren38 ren39 ren40 ren41 ren42 ren43 ren44 ren45 ren46 ren47 ren48 ren49 ren50 ren51 ren52 ren53 ren54 ren55 ren56 ren57 ren58 ren59 ren60 ren61 ren62 ren63 ren64 ren65 ren66 ren67 ren68 ren69 ren70 ren71 ren72 ren73 ren74 ren75 ren76 ren77 ren78 ren79 ren80 ren81 ren82 ren83 ren84 ren85 ren86 ren87 ren88 ren89 ren90 ren91 ren92 ren93 ren94 ren95 ren96 ren97 ren98 ren99 ren100 ren101 ren102 ren103 ren104 ren105 ren106 ren107 ren108 ren109 ren110 ren111 ren112 ren113 ren114 ren115 ren116 ren117 ren118 ren119 ren120 ren121 ren122 ren123 ren124 ren125 ren126 ren127 ren128 ren129 ren130 ren131 ren132 ren133 ren134 ren135 ren136 ren137 ren138 ren139 ren140 ren141 ren142 ren143 ren144 ren145 ren146 ren147 ren148 ren149 ren150 ren151 ren152 ren153 ren154 ren155 ren156 ren157 ren158 ren159 ren160 ren161 ren162 ren163 ren164 ren165 ren166 ren167 ren168 ren169 ren170 ren171 ren172 ren173 ren174 ren175 ren176 ren177 ren178 ren179 ren180 ren181 ren182 ren183 ren184 ren185 ren186 ren187 ren188 ren189 ren190 ren191 ren192 ren193 ren194 ren195 ren196 ren197 ren198 ren199 ren200 ren201 ren202 ren203 ren204 ren205 ren206 ren207 ren208 ren209 ren210 ren211 ren212 ren213 ren214 ren215 ren216 ren217 ren218 ren219 ren220 ren221 ren222 ren223 ren224 ren225 ren226 ren227 ren228 ren229 ren230 ren231 ren232 ren233 ren234 ren235 ren236 ren237 ren238 ren239 ren240 ren241 ren242 ren243 ren244 ren245 ren246 ren247 ren248 ren249 ren250 ren251 ren252 ren253 ren254 ren255 ren256 ren257 ren258 ren259 ren260 ren261 ren262 ren263 ren264 ren265 ren266 ren267 ren268 ren269 ren270 ren271 ren272 ren273 ren274 ren275 ren276 ren277 ren278 ren279 ren280 ren281 ren282 ren283 ren284 ren285 ren286 ren287 ren288 ren289 ren290 ren291 ren292 ren293 ren294 ren295 ren296 ren297 ren298 ren299 ren300 ren301 ren302 ren303 ren304 ren305 ren306 ren307 ren308 ren309 ren310 ren311 ren312 ren313 ren314 ren315 ren316 ren317 ren318 ren319 ren320 ren321 ren322 ren323 ren324 ren325 ren326 ren327 ren328 ren329 ren330 ren331 ren332 ren333 ren334 ren335 ren336 ren337 ren338 ren339 ren340 ren341 ren342 ren343 ren344 ren345 ren346 ren347 ren348 ren349 ren350 ren351 ren352 ren353 ren354 ren355 ren356 ren357 ren358 ren359 ren360 ren361 ren362 ren363 ren364 ren365 ren366 ren367 ren368 ren369 ren370 ren371 ren372 ren373 ren374 ren375 ren376 ren377 ren378 ren379 ren380 ren381 ren382 ren383 ren384 ren385 ren386 ren387 ren388 ren389 ren390 ren391 ren392 ren393 ren394 ren395 ren396 ren397 ren398 ren399 ren400 ren401 ren402 ren403 ren404 ren405 ren406 ren407 ren408 ren409 ren410 ren411 ren412 ren413 ren414 ren415 ren416 ren417 ren418 ren419 ren420 ren421 ren422 ren423 ren424 ren425 ren426 ren427 ren428 ren429 ren430 ren431 ren432 ren433 ren434 ren435 ren436 ren437 ren438 ren439 ren440 ren441 ren442 ren443 ren444 ren445 ren446 ren447 ren448 ren449 ren450 ren451 ren452 ren453 ren454 ren455 ren456 ren457 ren458 ren459 ren460 ren461 ren462 ren463 ren464 ren465 ren466 ren467 ren468 ren469 ren470 ren471 ren472 ren473 ren474 ren475 ren476 ren477 ren478 ren479 ren480 ren481 ren482 ren483 ren484 ren485 ren486 ren487 ren488 ren489 ren490 ren491 ren492 ren493 ren494 ren495 ren496 ren497 ren498 ren499 ren500 ren501 ren502 ren503 ren504 ren505 ren506 ren507 ren508 ren509 ren510 ren511 ren512 ren513 ren514 ren515 ren516 ren517 ren518 ren519 ren520 ren521 ren522 ren523 ren524 ren525 ren526 ren527 ren528 ren529 ren530 ren531 ren532 ren533 ren534 ren535 ren536 ren537 ren538 ren539 ren540 ren541 ren542 ren543 ren544 ren545 ren546 ren547 ren548 ren549 ren550 ren551 ren552 ren553 ren554 ren555 ren556 ren557 ren558 ren559 ren560 ren561 ren562 ren563 ren564 ren565 ren566 ren567 ren568 ren569 ren570 ren571 ren572 ren573 ren574 ren575 ren576 ren577 ren578 ren579 ren580 ren581 ren582 ren583 ren584 ren585 ren586 ren587 ren588 ren589 ren590 ren591 ren592 ren593 ren594 ren595 ren596 ren597 ren598 ren599 ren600 ren601 ren602 ren603 ren604 ren605 ren606 ren607 ren608 ren609 ren610 ren611 ren612 ren613 ren614 ren615 ren616 ren617 ren618 ren619 ren620 ren621 ren622 ren623 ren624 ren625 ren626 ren627 ren628 ren629 ren630 ren631 ren632 ren633 ren634 ren635 ren636 ren637 ren638 ren639 ren640 ren641 ren642 ren643 ren644 ren645 ren646 ren647 ren648 ren649 ren650 ren651 ren652 ren653 ren654 ren655 ren656 ren657 ren658 ren659 ren660 ren661 ren662 ren663 ren664 ren665 ren666 ren667 ren668 ren669 ren670 ren671 ren672 ren673 ren674 ren675 ren676 ren677 ren678 ren679 ren680 ren681 ren682 ren683 ren684 ren685 ren686 ren687 ren688 ren689 ren690 ren691 ren692 ren693 ren694 ren695 ren696 ren697 ren698 ren699 ren700 ren701 ren702 ren703 ren704 ren705 ren706 ren707 ren708 ren709 ren710 ren711 ren712 ren713 ren714 ren715 ren716 ren717 ren718 ren719 ren720 ren721 ren722 ren723 ren724 ren725 ren726 ren727 ren728 ren729 ren730 ren731 ren732 ren733 ren734 ren735 ren736 ren737 ren738 ren739 ren740 ren741 ren742 ren743 ren744 ren745 ren746 ren747 ren748 ren749 ren750 ren751 ren752 ren753 ren754 ren755 ren756 ren757 ren758 ren759 ren760 ren761 ren762 ren763 ren764 ren765 ren766 ren767 ren768 ren769 ren770 ren771 ren772 ren773 ren774 ren775 ren776 ren777 ren778 ren779 ren780 ren781 ren782 ren783 ren784 ren785 ren786 ren787 ren788 ren789 ren790 ren791 ren792 ren793 ren794 ren795 ren796 ren797 ren798 ren799 ren800 ren801 ren802 ren803 ren804 ren805 ren806 ren807 ren808 ren809 ren810 ren811 ren812 ren813 ren814 ren815 ren816 ren817 ren818 ren819 ren820 ren821 ren822 ren823 ren824 ren825 ren826 ren827 ren828 ren829 ren830 ren831 ren832 ren833 ren834 ren835 ren836 % 1.51/0.87 Fol Constants: one_one_int zero_zero_int int min pls fFalse fTrue m m1 r s1 s sa t v w x y ord_less_int plus_plus_int semiri1621563631at_int n plus_plus_rat power_power_rat number_number_of_nat bit0 bit1 zero_zero_rat plus_plus_real power_power_real zero_zero_real power_power_int one_one_rat power_881366806de_int one_on1684967323de_int power_power_complex one_one_complex power_2100829034umeral one_on1645066479umeral one_one_real power_power_nat one_one_nat zero_z891286103de_int zero_zero_complex zero_z126310315umeral zero_zero_nat number_number_of_rat plus_plus_complex number528085621omplex number267125858f_real number_number_of_int plus_plus_nat ord_less_nat ord_less_rat ord_less_real number1226105091de_int number1443263063umeral member308914164t_bool member2143287562nt_int member_real member_nat member_fun_int_bool member180897546at_nat member_int semiri151668891at_rat semiri2020571505omplex semiri132038758t_real semiri984289939at_nat ord_le1860547276de_int semiri1424489471de_int ord_le1304079648umeral semiri1619134803umeral plus_p1446045655de_int plus_p1627245867umeral tn if_nat ord_less_eq_int succ ord_less_eq_rat ord_less_eq_real ord_less_eq_nat ord_le258702272de_int ord_le565307924umeral ord_le951220754t_bool ord_le1568362934t_bool times_times_int times_times_rat times_123202395de_int times_times_complex times_times_real times_times_nat times_1655362735umeral ord_less_eq_bool ord_le1912455174t_bool ord_le382113706t_bool twoSqu1770640450sum2sq zprime quadRes dvd_dvd_int minus_minus_int dvd_dvd_nat dvd_dvd_rat dvd_dv1760642554de_int dvd_dvd_complex dvd_dv174992974umeral dvd_dvd_real minus_minus_rat minus_minus_complex minus_minus_real minus_minus_nat nat abs_abs_int twoSqu1907779896sum2sq product_Pair_int_int if_int abs_abs_rat abs_abs_real zfact div_div_int div_div_nat d22set zOdd sr cOMBS_int_bool_bool cOMBB_1652995168ol_int fconj cOMBC_int_int_bool suc sRStar nat_neg even_odd_even_int negDivAlg_rel posDivAlg_rel finite_card_int div_di1218280263umeral minus_1690775515umeral finite1876863882t_bool zEven ln inverse_divide_real exp_real uminus_uminus_real norm_norm_complex norm_norm_real uminus_uminus_int uminus473333897omplex fequal_int sqrt arctan pi arcsin sgn_sgn_real cos sin arccos sgn_sgn_int tan real_nat fact_fact_nat even_odd_even_nat if_real sin_coeff cos_coeff inverse_inverse_real root finite_finite_int finite1395289673t_bool complex invers1449016382omplex invers1025623611omplex size_size_complex ii sgn_sgn_complex coprime pred nat_size size_size_nat cnj size_s945831648umeral im re prime negateSnd produc2136830103umeral produc282740534nt_int product_Pair_nat_nat product_fst_int_int product_snd_int_int product_fst_nat_nat product_snd_nat_nat produc556554744l_real produc1935615926l_real produc865579683l_real div_di1430059507de_int produc1318306967de_int quickc1265749348ro_rel fact_fact_int size_size_list_int gcd_gcd_nat real_int powr produc494345619at_nat pair_less pair_leq fact quickcheck_of_int minus_534354567de_int norm_frac_rel upto_rel lazy_small_lazy_rel norRRset ring_1_of_int_real ring_1_of_int_int ring_11397209091omplex finite_finite_nat finite_card_nat nat_nat_set field_1210416355s_real iszero_rat iszero_int inverse_divide_rat sgn_sgn_rat uminus_uminus_rat inverse_inverse_rat nat_gcd_rel int_gcd produc883642259nt_int ratrel fract ring_1_of_int_rat ring_1_Ints_real if_Pro1731782967nt_int cOMBS_real_real_real cOMBB_882763271l_real cOMBC_real_nat_real cOMBB_599996122l_real cOMBB_real_real_real cOMBC_nat_nat_bool cOMBC_real_real_real cOMBB_nat_bool_int cOMBB_722610049al_nat cOMBB_117013006ex_nat cOMBS_nat_bool_bool cOMBB_1015721476ol_nat cOMBC_226598744l_bool cOMBB_1146692694ol_nat cOMBB_int_bool_nat cOMBC_int_int_int cOMBS_nat_real_real cOMBB_1308947378al_nat cOMBB_real_real_nat cOMBB_nat_real_nat cOMBC_nat_nat_nat cOMBB_963856155at_nat cOMBS_real_bool_bool cOMBB_624415285l_real cOMBB_real_bool_real fequal_real cOMBC_real_real_bool cOMBI_int suminf_real cOMBB_1896127834l_real cOMBB_1948233853l_real cOMBC_1329014627t_real cOMBB_421464275l_real cOMBB_nat_nat_nat cOMBC_nat_real_real cOMBB_782625832nt_int cOMBC_1683390479t_bool cOMBB_389152643ol_int cOMBB_793166024ol_int cOMBB_1290694363ol_int cOMBB_int_bool_int cOMBB_1496585939nt_int cOMBB_bool_bool_int fNot cOMBC_736024425nt_int cOMBB_1875755114nt_int cOMBB_int_int_int cOMBC_int_nat_int cOMBS_1470252563nt_int cOMBB_735549356nt_int cOMBB_1389251822nt_int cOMBC_707974837nt_int cOMBB_662120866nt_int cOMBS_2011279539nt_int cOMBB_1657320178nt_int cOMBC_1964283556nt_int cOMBB_1102189010nt_int cOMBB_638531587nt_int cOMBS_1891347093nt_int cOMBB_222539774nt_int cOMBS_1640193733nt_int cOMBC_1805044090nt_int cOMBB_320287386nt_int cOMBB_1846624359nt_int frac cOMBB_591320580ol_int cOMBC_241247961t_bool cOMBB_562416518ol_int cOMBB_550562460ol_int cOMBB_118231410ol_int suminf_complex cOMBS_1610675060t_bool cOMBB_595786433nt_int cOMBB_1344650379nt_int cOMBB_1550063917nt_int cOMBC_33652895t_bool cOMBB_182850971nt_int cOMBB_2086486755nt_int cOMBS_400904860l_bool cOMBS_1676841879t_bool cOMBB_650041899nt_int cOMBS_480885903t_bool cOMBB_773384995nt_int cOMBC_2037038898nt_int cOMBB_563965291nt_int cOMBB_47643171nt_int cOMBB_1506897658nt_int cOMBB_866192175nt_int cOMBC_1417754532nt_int cOMBB_348438404at_nat cOMBS_163651580l_real cOMBB_3698607l_real cOMBS_902912708l_real cOMBS_107495110l_real cOMBB_520243667l_real cOMBS_794971624l_real cOMBB_731595089l_real cOMBB_415306361l_real if_Pro313124157l_real cOMBB_421479067l_real cOMBB_1795223523l_real cOMBS_193881978l_real cOMBB_422423973l_real cOMBB_2107848501l_real cOMBC_1508019322l_real cOMBB_1768400739l_real cOMBB_2092576745l_real cOMBC_467724138l_real cOMBB_44084907l_real cOMBS_511527878l_real cOMBB_557258983l_real cOMBB_237479429l_real cOMBI_real cOMBB_1484610687nt_int cOMBS_1720984575t_bool cOMBB_1211207212ol_int cOMBC_746811033l_real cOMBB_1480366270al_nat cOMBS_337378985l_real cOMBI_nat cOMBB_430461877l_real cOMBC_int_real_bool cOMBB_1317819104ol_int cOMBB_real_bool_int cOMBB_int_real_int cOMBC_int_rat_bool cOMBB_214503962ol_int cOMBB_rat_bool_int cOMBB_int_rat_int cOMBC_94739984l_bool big_co604158596t_real cOMBB_800536526ol_nat cOMBC_2010481033l_real cOMBB_1934313333l_real cOMBB_1419615765al_nat big_co230513141nt_int big_co1024481617at_int cOMBB_int_int_nat cOMBC_nat_int_int cOMBB_859312247nt_nat ord_lessThan_nat big_co387207925at_nat cOMBS_nat_nat_nat ord_lessThan_real gcd_gcd_int cOMBB_569260360nt_int fequal_rat cOMBS_549334880nt_rat cOMBB_170828966nt_int cOMBB_798864284nt_int cOMBS_2019229620nt_int big_co1758102091ol_nat cOMBB_1418110531ol_int fEx_int cOMBC_983868720t_bool cOMBB_2027861294ol_int cOMBB_1121934354l_real cOMBB_1453147152l_real cOMBC_412863505t_bool cOMBB_690122963l_real cOMBB_2138578194l_real cOMBB_188663909l_real cOMBC_243356514t_bool cOMBB_1459832681l_real cOMBB_95956018ol_int cOMBB_1247074793l_real cOMBC_824100275t_real cOMBB_2129825580al_int cOMBB_real_real_int cOMBB_1946221070al_int sequentially cOMBB_1533963633al_nat cOMBB_1159313332l_real cOMBB_1593174431ol_int fEx_nat cOMBC_1801450329t_bool cOMBB_172850899l_real cOMBC_678732631t_bool cOMBB_2125215742l_real cOMBB_2087181719ol_int cOMBB_270132509l_real cOMBB_2046938128ol_int cOMBC_1113900202t_bool cOMBB_984071017l_real cOMBB_1647910634ol_int cOMBB_2050079537l_real cOMBB_real_bool_nat cOMBC_295337211t_real cOMBB_929094628al_int cOMBB_bool_bool_nat fequal_nat cOMBS_696648398omplex cOMBB_1714920583ex_nat cOMBB_64450052al_nat pred_nat ord_min_nat cOMBS_nat_rat_rat cOMBB_1926947at_nat nat_is_nat cOMBB_rat_rat_nat produc713279741t_bool ord_atMost_nat ord_max_nat ord_atMost_real skc21 skc22 skc23 skc24 skc25 skc29 skc30 skc31 skc52 skc53 skc54 skc55 skc80 skc149 skc226 skc227 skc228 skc230 skc231 skc232 skc233 skc234 skc235 % 1.51/0.87 Fol Functions: archim856651990g_real archim791455193or_rat archim1246769320r_real big_co1548731110nt_int code_int_of the_int undefined_int hilbert_Eps_int tendst1507391555omplex tendsto_complex_real tendsto_nat_complex tendsto_nat_real tendsto_real_real trivial_limit_nat quickcheck_int_of vanishes bseq_real cauchy_complex cauchy_real monoseq_real summable_complex summable_real fdisj hAPP_C24501650l_bool hAPP_complex_bool hAPP_bool_bool hAPP_int_bool hAPP_int_int hAPP_nat_bool hAPP_nat_int hAPP_Q2096512830t_bool hAPP_rat_bool hAPP_real_bool hAPP_f448129468l_bool hAPP_f1594865479ol_int hAPP_f54304608l_bool hAPP_f659380387ol_int hAPP_f1501066425l_bool hAPP_f215623910l_bool hAPP_f1469637905l_bool hAPP_f526364711l_bool hAPP_f115998247l_bool hAPP_P603027463t_bool hAPP_P1175774780nt_int hAPP_P1555980039t_bool hAPP_P1333854989l_bool hAPP_P880235623l_bool hAPP_P62333565t_bool hAPP_P1463840893t_bool hAPP_i1948725293t_bool hAPP_int_fun_int_int hAPP_rat_fun_nat_rat hAPP_int_nat hAPP_nat_rat hAPP_rat_fun_rat_rat hAPP_rat_rat hAPP_r474017924t_real hAPP_nat_real hAPP_r1250527377l_real hAPP_real_real hAPP_int_fun_nat_int hAPP_Q125967240de_int hAPP_n522471361de_int hAPP_c1088319240omplex hAPP_nat_complex hAPP_C471253896umeral hAPP_n1108039445umeral hAPP_nat_fun_nat_nat hAPP_nat_nat hAPP_int_rat hAPP_c172932010omplex hAPP_int_complex hAPP_complex_complex hAPP_int_real hAPP_n1699378549t_bool hAPP_r2115560837t_bool hAPP_r1134773055l_bool hAPP_i1732201573de_int hAPP_i769753017umeral hAPP_P1681069257l_bool hAPP_P1062890741l_bool hAPP_r1130899993l_bool hAPP_n215258509l_bool hAPP_f628503027l_bool hAPP_P1876494581l_bool hAPP_i2112223885l_bool collec1979865426at_nat collect_real collec1347809874nt_int collec50511176nt_int collect_nat collect_int hAPP_Q1010094925t_bool hAPP_C10902773l_bool hAPP_Q1729056540de_int hAPP_Q1762011733de_int hAPP_C1594335432umeral hAPP_C498520661umeral hAPP_b992065680at_nat hAPP_f284875647l_bool hAPP_f103356543l_bool hAPP_b589554111l_bool legendre zcong hAPP_c1403687985x_bool hAPP_i1584592887nt_int hAPP_i1524277240nt_int hAPP_b1463609396nt_int nat_aux inv multInv wset phi hAPP_f1734373249l_bool hAPP_f2144054103l_bool hAPP_f727283836t_bool hAPP_f428220345t_bool hAPP_f1805168059t_bool div_mod_int nat_tr876908586nt_nat standardRes nat_tsub div_mod_nat pdivmod divmod_int_rel negDivAlg adjust hAPP_P1975530577nt_int posDivAlg natceiling accp_P2006205492nt_int natfloor hAPP_f957591787ol_nat multInvPair setS div_mo1740067990umeral hAPP_f521865025ol_nat comple219730294t_bool code_nat_of_aux log hAPP_complex_real z3mod z3div hAPP_b646336293l_real deriv_real hAPP_n546711566l_real hAPP_r265291036omplex hAPP_real_complex complex_size arg hAPP_complex_nat of_real_complex expi resSet code_c271388182l_size code_S1047413653umeral hAPP_C2129356693al_nat cis bezw divmod_int code_d418564891umeral hAPP_C1614127039umeral hAPP_C2132160860umeral xzgcd hAPP_i1730167831nt_int hAPP_P408881810nt_int xzgcda divmod_nat hAPP_n1865633855at_nat hAPP_n1289843868at_nat divmod_nat_rel hAPP_P1654798560at_nat bolzano_bisect hAPP_n332733730l_real hAPP_P731461727l_real hAPP_r2019696015l_real hAPP_r1195171167l_real div_mo231679042de_int rcis quickc495462417de_int hAPP_Q952608535de_int hAPP_Q1256397320de_int quickcheck_nat_of accp_int quickc666637781d_zero hAPP_list_int_nat bnorRset legacy_zgcd hAPP_P402336767at_nat hAPP_P369611207at_nat dist_dist_real dist_dist_complex noXRRset is_RRset rRset2norRR rsetR image_int_int image_nat_int hAPP_f22106695ol_nat image_int_nat image_275383677t_bool ord_gr1297742076an_int int_lcm nat_lcm ord_gr660468384an_nat ord_gr788844697n_real comple124823625p_real frct quotient_of nat_gcd normalize accp_P490777396at_nat hAPP_P941956607nt_int hAPP_P230595783nt_int hAPP_int_fun_int_rat ratreal hAPP_b40753821nt_int hAPP_P1145851913nt_int hAPP_f1960414057l_real hAPP_f1796904975t_real hAPP_f1992866895l_real hAPP_f1950183573l_real hAPP_f556082547l_real hAPP_f2069516469l_real hAPP_f1407095736t_real hAPP_f248847589l_real hAPP_f229349961t_bool hAPP_f203520653l_real hAPP_f696844121t_bool hAPP_f1448486952t_bool hAPP_f327026105t_real hAPP_f1290670424t_real hAPP_f1457396693omplex hAPP_f1646117269omplex hAPP_f1080886329l_bool hAPP_f1146629647l_bool hAPP_f561022312t_bool hAPP_f800510211t_bool hAPP_f2037783381l_bool hAPP_f66927821l_bool hAPP_f1722879237t_bool nat_tr160667106at_int cOMBK_bool_nat hAPP_f1361476881t_bool hAPP_f1154658180t_bool hAPP_f2135977429nt_int norm_frac hAPP_f1092742621l_real hAPP_f1690286043t_real hAPP_f1566856189t_real hAPP_f1731313045at_nat hAPP_f416620757at_nat hAPP_f1639111240at_nat hAPP_f1676298106t_real hAPP_f1888375463t_real hAPP_f451358433l_real hAPP_f197615720t_real hAPP_f1485493409l_bool hAPP_f824790735l_bool hAPP_f1402056515l_bool hAPP_f60716669l_bool hAPP_f1010710745l_bool hAPP_f695504873l_bool hAPP_f1861673493l_bool hilbert_Eps_real hAPP_f352196356l_real hAPP_f1786887945l_real hAPP_f895854793t_real hAPP_f1998755145t_real hAPP_f1163894827t_real hAPP_f1135648319t_real hAPP_f1501741374t_real hAPP_f1993765077t_real hAPP_f1122023986l_real hAPP_f1585078997at_nat hAPP_f1914919701at_nat hAPP_f42270917t_real produc1298267108nt_int hAPP_f2054677283nt_int hAPP_f1574055885nt_int produc1518849193nt_int hAPP_f85237525t_bool hAPP_f1830214065l_bool hAPP_f1512942609t_bool hAPP_f908327869t_bool hAPP_f1629352853nt_int hAPP_f1760145644nt_int hAPP_f720654810t_bool hAPP_f1344929775l_bool hAPP_f1545556668t_bool hAPP_f472159229t_bool fimplies hAPP_f627970963t_bool hAPP_f1048215610t_bool produc93441119t_bool hAPP_f888249301nt_int hAPP_f2105620693nt_int hAPP_nat_fun_int_int hAPP_f836602773nt_int hAPP_f808647893nt_int hAPP_f1731308757nt_int hAPP_f279307923nt_int hAPP_f251264923nt_int hAPP_f1582586579nt_int hAPP_P621635040nt_int hAPP_f400200275nt_int hAPP_f1081447804nt_int hAPP_f534361363nt_int hAPP_f1228585167nt_int hAPP_f2004554147nt_int hAPP_f2094497995nt_int hAPP_f434654626nt_int hAPP_f465821005nt_int hAPP_f197974549nt_int hAPP_f429935748t_bool hAPP_f1311564564nt_int hAPP_f747475781nt_int hAPP_f1377453843nt_int hAPP_f142232355nt_int hAPP_f960630521nt_int hAPP_f55007289nt_int hAPP_f617310012nt_int hAPP_f654702867t_bool hAPP_f847817363t_bool hAPP_f1399575567t_bool hAPP_f983569339t_bool hAPP_f725770969t_bool hAPP_f791698359t_bool hAPP_i345030060t_bool hAPP_f213450978omplex hAPP_f1273270095t_bool hAPP_f1961001761l_bool hAPP_f513299955t_bool hAPP_f214467655t_bool hAPP_f291087797t_bool hAPP_f2018027565t_bool hAPP_i119638232t_bool hAPP_f237669397t_bool hAPP_f365317245l_bool hAPP_f1965248563t_bool hAPP_f125837377t_bool hAPP_f461489489t_bool hAPP_f326728547t_bool hAPP_f1815301987t_bool hAPP_f2042071795t_bool hAPP_f1151807883nt_int hAPP_f1038672605nt_int hAPP_f1855025978nt_int hAPP_f301246617nt_int hAPP_f1769710159nt_int hAPP_f167782601nt_int hAPP_f1198736473t_bool hAPP_f223623489t_bool hAPP_f11709033t_bool hAPP_f578362681nt_int hAPP_f400538607nt_int hAPP_f1187443546t_bool hAPP_f1781059817t_bool produc973645403t_bool hAPP_f999082675at_nat hAPP_f837737749at_nat produc1391996073at_nat hAPP_P1586233937at_nat hAPP_f774948957l_real hAPP_f328572565l_real hAPP_f1076489843l_real hAPP_f1879982819l_real hAPP_f940061907l_bool hAPP_f172451459l_bool hAPP_f555557763l_real hAPP_f1119546819l_real hAPP_f850851693l_real hAPP_f1874145443l_real hAPP_f1310479593l_real hAPP_f1732848529l_real hAPP_f1644353557l_real hAPP_r337325687l_real hAPP_f320596107l_real hAPP_f1884005689l_bool hAPP_f517738447l_real hAPP_f1161935955l_real hAPP_f677014621l_real hAPP_f1109256153l_real hAPP_f2114902373l_real hAPP_f1040184293l_real hAPP_f823702159l_real hAPP_f1108539711l_real hAPP_f644105375l_real hAPP_f1591894897l_real hAPP_f324002831l_real hAPP_f1663701695l_real hAPP_f1763467369l_real hAPP_f2072293513l_real produc595218619l_real hAPP_P1860904029l_real produc713050258nt_int hAPP_f334321603nt_int hAPP_f1148171384nt_int int_ge_less_than2 int_ge_less_than hAPP_f538565589t_bool hAPP_f1315737299t_bool hAPP_f1878066172t_bool sums_real hAPP_f264196187l_real hAPP_f1129044203l_real hAPP_f2126667875l_real hAPP_r195310020l_real hAPP_f335634176l_real sums_complex diffs_real nat_case_bool nat_case_nat hAPP_f1900646853l_bool hAPP_f1393328161l_bool the_real the_Pr588456374at_nat hAPP_f499530369l_bool hAPP_f801032407l_bool hAPP_f1845081853t_bool hAPP_r481142414t_bool hAPP_f1173902867t_bool hAPP_f134192053t_real hAPP_f563293398t_real hAPP_f429384717t_bool hAPP_f857296063t_bool hAPP_f601898971t_bool hAPP_f1480506641t_bool hAPP_r1900510169t_bool hAPP_f1131424617t_bool hAPP_f1270196437nt_rat hAPP_f1900950721nt_rat hAPP_f1241350704t_bool hAPP_f202917053t_bool hAPP_f1509287679l_real ord_at4362885an_nat hAPP_f1406902706l_real hAPP_f1505651103t_bool hAPP_f618557131t_bool image_nat_nat ord_at641636577an_int ord_at1496968948n_real hAPP_f1067681227l_real hAPP_f224989205l_real hAPP_f1904307534l_real hAPP_f1523861863l_real hAPP_f59594445l_real hAPP_f2119584768l_real hAPP_f1926459811ol_int hAPP_f1431025877at_int hAPP_f125788821nt_int hAPP_f1935805932nt_int hAPP_f1673103573at_int hAPP_f1139079189at_int hAPP_f1599440987ol_int hAPP_f782000547ol_nat hAPP_f1408247010at_nat hAPP_f374502857t_bool hAPP_f382317021nt_rat hAPP_f1547007718nt_rat hAPP_f1120137083nt_rat hAPP_f1065357839nt_rat hAPP_f1084724746t_bool hAPP_f492612297t_bool hAPP_f892584630t_bool hAPP_f1914742907nt_int hAPP_f521271395nt_int the_Pr2103884470nt_int hAPP_f93439879ol_nat cOMBK_1643584600t_bool hAPP_f423804115t_bool hAPP_f1475822739t_bool hAPP_f1251097615t_bool hAPP_f735247205t_bool hAPP_f1791153283t_bool hAPP_f2119767738t_bool hAPP_f1925507189l_bool hAPP_f340152631t_bool hAPP_f1456711209t_bool hAPP_f2050994651t_bool hAPP_f512004221l_bool hAPP_f1177545951t_bool hAPP_f866672739t_bool hAPP_f1920544743t_bool hAPP_f332806115t_bool hAPP_f422375781t_bool hAPP_f1169087445t_real hAPP_f318350629l_real hAPP_f1352333353l_real hAPP_f74147283t_real hAPP_f352226557t_real hAPP_f1323932638t_real hAPP_f956464319t_bool hAPP_f381769257l_bool hAPP_f1063001928t_bool hAPP_f704188951t_bool hAPP_f1990636069t_bool hAPP_f1832844496t_bool hAPP_f1625314454t_bool hAPP_f101635158l_bool hAPP_f1607377819t_real hAPP_f292751352t_real hAPP_f389116883t_bool hAPP_f571820015t_bool hAPP_f1261108921t_bool hAPP_f1182713365t_bool hAPP_f1121609875t_bool hAPP_f643658017l_bool hAPP_f848516149l_bool hAPP_f403082607t_bool hAPP_f1083049571t_bool hAPP_f1840085295t_bool hAPP_f77155443t_bool hAPP_f693283245t_bool hAPP_f212164053t_real hAPP_f1295083291t_real hAPP_f1720068861t_real hAPP_f1613846310t_real hAPP_f1459420095t_bool hAPP_f834119977l_bool hAPP_f2084827628t_bool hAPP_f1927674023t_bool hAPP_f271976045t_bool hAPP_f894608603t_bool hAPP_f1115375056t_bool hAPP_f1341793266t_bool hAPP_f406530075omplex hAPP_f23851874omplex hAPP_f1052840010omplex hAPP_f219720582omplex hAPP_f918606171t_real hAPP_f73570213t_real ord_at1589558736t_real ord_at238088361st_nat ord_at875362053st_int big_co1705425894at_nat at_complex at_real scaleR1652505878omplex scaleR_scaleR_real produc1922581855t_bool hAPP_f1073644437at_rat hAPP_f1830834240at_rat hAPP_f1131305186at_rat hAPP_f2062659861at_rat hAPP_f1082758869at_rat cOMBK_rat_nat zcongm hAPP_f1418982953t_bool hAPP_f538843494t_bool bijR_int_int isCont_real_real isCont156215680omplex isCont_complex_real hAPP_f747162069nt_int hAPP_f1356864277nt_int hAPP_nat_fun_rat_rat hAPP_b1482221219l_real hAPP_P1982799375l_real hAPP_i16292313t_bool hAPP_i68813070l_bool hAPP_n1006566506l_bool hAPP_f605995867t_bool hAPP_f737665877t_bool hAPP_i688218208l_bool hAPP_r1938957037l_bool hAPP_f766218899t_real hAPP_f269654879t_real hAPP_n1983812447omplex hAPP_f11151005nt_int hAPP_f2002277285nt_int hAPP_f883232462nt_int hAPP_i61245889nt_int hAPP_P2110489235nt_int hAPP_P1853363688nt_rat hAPP_P507092031nt_rat hAPP_f41603166t_bool hAPP_i418383825t_bool hAPP_P252494982t_bool hAPP_f1325804733t_bool hAPP_P921862901l_bool hAPP_r1409264866l_real hAPP_i371647666l_real hAPP_n682674106l_real hAPP_f330985925l_bool hAPP_f800361423l_real hAPP_f617735571l_real hAPP_f1730463541l_real hAPP_i744251628nt_int hAPP_i872162435t_bool hAPP_i1778081398nt_int hAPP_f151095827nt_int hAPP_f1735705551nt_int hAPP_i1529485324t_bool hAPP_f729588221t_bool hAPP_f289318786t_bool hAPP_i1796122964t_bool hAPP_f713949180nt_int hAPP_i1216375074nt_int hAPP_f1576199059t_bool hAPP_f351634443t_bool hAPP_i627165055t_real hAPP_f743790483t_bool hAPP_f1222178131t_bool hAPP_i157317923t_real hAPP_i1671359920t_real hAPP_i447943416t_real hAPP_r50993370t_real hAPP_i998473677nt_int hAPP_f1908301369l_real hAPP_f1736103445l_real hAPP_r938550413l_real hAPP_P1668131738nt_int hAPP_i1823918693l_bool hAPP_f252743847l_bool hAPP_i614188481l_bool hAPP_r632163725t_bool hAPP_r373117745t_bool hAPP_r1623423338t_bool hAPP_r653725362t_bool hAPP_i1836591008nt_int hAPP_i2104874254nt_int hAPP_f1375227553nt_int hAPP_r712953929l_real hAPP_r1392521531t_bool hAPP_r2052264067t_bool hAPP_r847664445t_bool hAPP_r279757445t_bool hAPP_i1153444985nt_int hAPP_P752050971nt_int hAPP_f1902329768t_bool hAPP_P989584703t_bool hAPP_P1400155668t_bool hAPP_P877703507t_bool hAPP_r1150855451l_bool hAPP_r285062775l_bool hAPP_r579619957l_real hAPP_r224952523l_real hAPP_f183342685l_real hAPP_f1293550189l_real hAPP_r931665397l_real hAPP_P2053772734t_bool hAPP_f1607917947l_real hAPP_r1962736578t_bool hAPP_r1562208522t_bool hAPP_r1230691443l_real hAPP_r1043989325l_real hAPP_r794344869l_real skf1 skf2 skf3 skf4 skf5 skf6 skf7 skf8 skf9 skf10 skf11 skf12 skf13 skf14 skf15 skf16 skf17 skf18 skf19 skf20 skf26 skf27 skf28 skf32 skf33 skf34 skf35 skf36 skf37 skf38 skf39 skf40 skf41 skf42 skf43 skf44 skf45 skf46 skf47 skf48 skf49 skf50 skf51 skf56 skf57 skf58 skf59 skf60 skf61 skf62 skf63 skf64 skf65 skf66 skf67 skf68 skf69 skf70 skf71 skf72 skf73 skf74 skf75 skf76 skf77 skf78 skf79 skf81 skf82 skf83 skf84 skf85 skf86 skf87 skf88 skf89 skf90 skf91 skf92 skf93 skf94 skf95 skf96 skf97 skf98 skf99 skf100 skf101 skf102 skf103 skf104 skf105 skf106 skf107 skf108 skf109 skf110 skf111 skf112 skf113 skf114 skf115 skf116 skf117 skf118 skf119 skf120 skf121 skf122 skf123 skf124 skf125 skf126 skf127 skf128 skf129 skf130 skf131 skf132 skf133 skf134 skf135 skf136 skf137 skf138 skf139 skf140 skf141 skf142 skf143 skf144 skf145 skf146 skf147 skf148 skf150 skf151 skf152 skf153 skf154 skf155 skf156 skf157 skf158 skf159 skf160 skf161 skf162 skf163 skf164 skf165 skf166 skf167 skf168 skf169 skf170 skf171 skf172 skf173 skf174 skf175 skf176 skf177 skf178 skf179 skf180 skf181 skf182 skf183 skf184 skf185 skf186 skf187 skf188 skf189 skf190 skf191 skf192 skf193 skf194 skf195 skf196 skf197 skf198 skf199 skf200 skf201 skf202 skf203 skf204 skf205 skf206 skf207 skf208 skf209 skf210 skf211 skf212 skf213 skf214 skf215 skf216 skf217 skf218 skf219 skf220 skf221 skf222 skf223 skf224 skf225 skf229 skf236 skf237 skf238 skf239 skf240 skf241 skf242 skf243 skf244 skf245 skf246 skf247 skf248 skf249 skf250 skf251 skf252 skf253 skf254 skf255 skf256 skf257 skf258 skf259 skf260 skf261 skf262 skf263 skf264 skf265 skf266 skf267 skf268 skf269 skf270 skf271 skf272 skf273 skf274 skf275 skf276 skf277 skf278 skf279 skf280 skf281 skf282 skf283 skf284 skf285 skf286 skf287 skf288 skf289 skf290 skf291 skf292 skf293 skf294 skf295 skf296 skf297 skf298 skf299 skf300 skf301 skf302 skf303 skf304 skf305 skf306 skf307 skf308 skf309 skf310 skf311 skf312 skf313 skf314 skf315 skf316 skf317 skf318 skf319 skf320 skf321 skf322 skf323 skf324 skf325 skf326 skf327 skf328 skf329 skf330 skf331 skf332 skf333 skf334 skf335 skf336 skf337 skf338 skf339 skf340 skf341 skf342 skf343 skf344 skf345 skf346 skf347 skf348 skf349 skf350 skf351 skf352 skf353 skf354 skf355 skf356 skf357 skf358 skf359 skf360 skf361 skf362 skf363 skf364 skf365 skf366 skf367 skf368 skf369 skf370 skf371 skf372 skf373 skf374 skf375 skf376 skf377 skf378 skf379 skf380 skf381 skf382 skf383 skf384 skf385 skf386 skf387 skf388 skf389 skf390 skf391 skf392 skf393 skf394 skf395 skf396 skf397 skf398 skf399 skf400 skf401 skf402 skf403 skf404 skf405 skf406 skf407 skf408 skf409 skf410 skf411 skf412 skf413 skf414 skf415 skf416 skf417 skf418 skf419 skf420 skf421 skf422 skf423 skf424 skf425 skf426 skf427 skf428 skf429 skf430 skf431 skf432 skf433 skf434 skf435 skf436 skf437 skf438 skf439 skf440 skf441 skf442 skf443 skf444 skf445 skf446 skf447 skf448 skf449 skf450 skf451 skf452 skf453 skf454 skf455 skf456 skf457 skf458 skf459 skf460 skf461 skf462 skf463 skf464 skf465 skf466 skf467 skf468 skf469 skf470 skf471 skf472 skf473 skf474 skf475 skf476 skf477 skf478 skf479 skf480 skf481 skf482 skf483 skf484 skf485 skf486 skf487 skf488 skf489 skf490 skf491 skf492 skf493 skf494 skf495 skf496 skf497 skf498 skf499 skf500 skf501 skf502 skf503 skf504 skf505 skf506 skf507 skf508 skf509 skf510 skf511 skf512 skf513 skf514 skf515 skf516 skf517 skf518 skf519 skf520 skf521 skf522 skf523 skf524 skf525 skf526 skf527 skf528 skf529 skf530 skf531 skf532 skf533 skf534 skf535 skf536 skf537 skf538 skf539 skf540 skf541 skf542 skf543 skf544 skf545 skf546 skf547 skf548 skf549 % 1.51/0.87 Problem Properties: % 1.51/0.87 This is a full first-order problem with equality. % 1.51/0.87 SZS status GaveUp % 1.51/0.87 SPASS beiseite: SPASS does currently not support non-BS equality problems. % 1.51/0.87 %------------------------------------------------------------------------------