
Time bar (total: 24.2s)
| 1× | search |
| Probability | Valid | Unknown | Precondition | Infinite | Domain | Can't | Iter |
|---|---|---|---|---|---|---|---|
| 0% | 0% | 99.8% | 0.2% | 0% | 0% | 0% | 0 |
| 0% | 0% | 99.8% | 0.2% | 0% | 0% | 0% | 1 |
| 0% | 0% | 99.8% | 0.2% | 0% | 0% | 0% | 2 |
| 0% | 0% | 99.8% | 0.2% | 0% | 0% | 0% | 3 |
| 0% | 0% | 99.8% | 0.2% | 0% | 0% | 0% | 4 |
| 25% | 25% | 74.9% | 0.2% | 0% | 0% | 0% | 5 |
| 25% | 25% | 74.9% | 0.2% | 0% | 0% | 0% | 6 |
| 25% | 25% | 74.9% | 0.2% | 0% | 0% | 0% | 7 |
| 37.5% | 37.4% | 62.4% | 0.2% | 0% | 0% | 0% | 8 |
| 56.3% | 56.1% | 43.7% | 0.2% | 0% | 0% | 0% | 9 |
| 56.3% | 56.1% | 43.7% | 0.2% | 0% | 0% | 0% | 10 |
| 56.3% | 56.1% | 43.7% | 0.2% | 0% | 0% | 0% | 11 |
| 65.6% | 65.5% | 34.3% | 0.2% | 0% | 0% | 0% | 12 |
Compiled 12 to 8 computations (33.3% saved)
| 2.2s | 8256× | 0 | valid |
| 973.0ms | 8206× | 0 | valid-sollya |
| 41.0ms | 50× | 0 | exit-sollya |
| Pt | Rival-out | Sollya-interval | Sollya-point | status | Sollya status | Rival iter | sollya-time | check |
|---|---|---|---|---|---|---|---|---|
| (-1.3027767190091439e+163 -3.4605893204963e-185 6.268269213965368e+275 1.2352690051178037e-108) | 5.822518367356108e-190 | (5.822518367356108e-190 5.822518367356108e-190) | +nan.0 | valid | exit | 0 | 0.291811 | #f |
| (-4.357546516082745e+152 -1.624994514888149e-197 -1.9765991139987287e-199 -1.6982071604354034e+175) | 2.1095249539891103e-21 | (2.1095249539891103e-21 2.1095249539891103e-21) | +nan.0 | valid | exit | 0 | 0.23287000000000002 | #f |
| (1.073720945693644e+166 6.960395232857756e-290 35894741646473840.0 -7670488.7764558485) | -2.7143850550257534e-147 | (-2.7143850550257534e-147 -2.7143850550257534e-147) | +nan.0 | valid | exit | 0 | 0.13592300000000002 | #f |
| (1.5530472818389237e+252 -1.0906604908404645e-305 -179063869084.60587 -5.777422255956158e+301) | -0.0 | (-0.0 -0.0) | +nan.0 | valid | exit | 0 | 0.327307 | #f |
| (-4.1979435054761085e-127 -6.545273750325459e+183 -7.19201985713931e+119 -6.722660193249322e-115) | 5.682930795105491e+51 | (5.682930795105491e+51 5.682930795105491e+51) | +nan.0 | valid | exit | 0 | 0.171215 | #f |
| (2.617317214827248e+41 -2.0942008698096907e-304 8.355055099437551e-93 -5.717867063005764e-68) | 1.1473378605640094e-103 | (+nan.0 +nan.0) | +nan.0 | valid | exit | 0 | 5.0 | #f |
| (4.539248124937455e+194 -1.6094103363819995e+295 -7.708849807881155e+152 -1.0316184192584105e-284) | -inf.0 | (-inf.0 -inf.0) | +nan.0 | valid | exit | 0 | 0.273116 | #f |
| (-3.4083589212415997e+274 1.1185277523538645e-185 -1.7983386101770274e+131 1.1242391431832984e+80) | 1.8856536042043564e-122 | (1.8856536042043564e-122 1.8856536042043564e-122) | +nan.0 | valid | exit | 0 | 0.142991 | #f |
| (-6.929307168485637e-105 -6.874786622043223e-81 -2.6005616758661195e+206 -3.3741497261101795e-288) | 5.4289710820467625e-104 | (5.4289710820467625e-104 5.4289710820467625e-104) | +nan.0 | valid | exit | 0 | 0.295922 | #f |
| (-3.560434571990756e-53 -2.616335177542473e+173 -1.2667175508325409e-140 -2.0038769890538478e-125) | +inf.0 | (+inf.0 +inf.0) | +nan.0 | valid | exit | 0 | 0.29046099999999997 | #f |
| (-3.3835178792505724e+298 -4.28845981883674e-159 2.6659622679246012e-114 7.224272594090164e+240) | 7533932028832.224 | (+nan.0 +nan.0) | +nan.0 | valid | exit | 0 | 5.0 | #f |
| (-5.8005263617751265e-273 4.946697588813493e-8 -5.773163576420197e+59 6.506748301257397e-129) | 7.638443940072067e-212 | (7.638443940072067e-212 7.638443940072067e-212) | +nan.0 | valid | exit | 0 | 0.243857 | #f |
| (2.0076585441402345e-13 -1.268812417421627e+76 -3.257745128442959e-97 -1.0564060179051175e+179) | -7.401833320298562e-20 | (-7.401833320298562e-20 -7.401833320298562e-20) | +nan.0 | valid | exit | 0 | 0.329405 | #f |
| (-2.968556600581127e+49 13416068246.174978 1.8644137811554864e+88 -1.1952171575728254e-247) | 1.7872342123354777e+218 | (1.7872342123354777e+218 1.7872342123354777e+218) | +nan.0 | valid | exit | 0 | 0.20410799999999998 | #f |
| (-1.482775801549807e-158 -2.9050602046233626e+299 4.027139836020804e+151 1.2938284514086335e+307) | 8.267176e-318 | (8.267176e-318 8.267176e-318) | +nan.0 | valid | exit | 0 | 0.237703 | #f |
| (2.1678592182081286e+302 1.4051930933833821e+191 -1.86289582169636e+128 2.0719507885729466e-200) | -inf.0 | (+nan.0 +nan.0) | +nan.0 | valid | exit | 0 | 5.0 | #f |
| (2.405054055956383e+19 -1.0125790573767589e+56 5.143945064579287e-169 7.665924037871182e-249) | -inf.0 | (-inf.0 -inf.0) | +nan.0 | valid | exit | 0 | 0.28103500000000003 | #f |
| (-4.321163413507758e+99 -1.8460363831341459e+62 1.563029975906824e+169 1.7688835327464306e-182) | 2.885189882456976e+174 | (2.885189882456976e+174 2.885189882456976e+174) | +nan.0 | valid | exit | 0 | 0.146284 | #f |
| (-1.6425357759555788e-164 1.256271890442801e+34 -2.1323280188698605e+298 -5.4316663537998653e-269) | -1.7816048298938974e-160 | (-1.7816048298938974e-160 -1.7816048298938974e-160) | +nan.0 | valid | exit | 0 | 0.242192 | #f |
| (-1.1521729404649909e+188 2.885402372264276e-96 -5.947347171817231e-234 -3.3318378474967656e-141) | -inf.0 | (-inf.0 -inf.0) | +nan.0 | valid | exit | 0 | 0.34502099999999997 | #f |
| (4.55586560859188e+32 1.1824839894625634e+82 1.8606297618638283e+306 1.0839334632307701e+102) | 2.6711826563192642e-294 | (2.6711826563192642e-294 2.6711826563192642e-294) | +nan.0 | valid | exit | 0 | 0.142378 | #f |
| (-1.0506413648721402e-73 1.6951150388251178e-222 4.5095303606076085e+131 9.474035052023773e+116) | -0.0 | (-0.0 -0.0) | +nan.0 | valid | exit | 0 | 0.15118 | #f |
| (1.0645351074825966e-239 4.999481325664281e+90 -3.560632818749133e+117 6.04688538739031e+174) | -0.0 | (-0.0 -0.0) | +nan.0 | valid | exit | 0 | 0.27687700000000004 | #f |
| (-1.2645205082943793e-229 -1.3872318490942577e-257 -7.240162008394178e-32 3.7302969597334266e-191) | -6.495061053651638e-265 | (-6.495061053651638e-265 -6.495061053651638e-265) | +nan.0 | valid | exit | 0 | 0.22545900000000002 | #f |
| (-4.612885928712139e+109 -1.1029675340300085e-252 7.867369483870775e+235 1.4528593511167066e-302) | 4.4512534610170576e-77 | (4.4512534610170576e-77 4.4512534610170576e-77) | +nan.0 | valid | exit | 0 | 0.278758 | #f |
| (-9.184503357623994e+285 -1.6759992432285994e-34 -2.3069569626254364e-304 1.1681977689625798e-207) | -inf.0 | (-inf.0 -inf.0) | +nan.0 | valid | exit | 0 | 0.23387200000000002 | #f |
| (-1.9792824991214042e+33 1.604216170214917e-172 2.09377595387476e+135 2.465786195671836e-84) | -6.150140672629305e-191 | (-6.150140672629305e-191 -6.150140672629305e-191) | +nan.0 | valid | exit | 0 | 0.137665 | #f |
| (1.6300954740746283e+219 -2.2790266915953634e-86 -5.185598692461319e-86 -1.3854968797461835e-15) | -5.170803057990607e+233 | (-5.170803057990607e+233 -5.170803057990607e+233) | +nan.0 | valid | exit | 0 | 0.23797200000000002 | #f |
| (-4.536111047884912e-71 -6.899403366407233e+125 3.0265782916119986e+277 -4.815012537544176e-164) | -2.1475628327390735e-59 | (-2.1475628327390735e-59 -2.1475628327390735e-59) | +nan.0 | valid | exit | 0 | 0.148159 | #f |
| (-2.3006949438366844e-123 6.889820368451317e-155 2.3130692228284313e+187 3.149037430687076e+84) | -0.0 | (-0.0 -0.0) | +nan.0 | valid | exit | 0 | 0.20921399999999998 | #f |
| (-1.8308367629770926e+96 4.415239735413748e-91 -1.572091601047663e-35 8.591607018678297e-103) | 5.984827845638361e+142 | (5.984827845638361e+142 5.984827845638361e+142) | +nan.0 | valid | exit | 0 | 0.268872 | #f |
| (-4.881142472418995e-137 4.231362104234234e+83 4.585500429859725e+130 3.7686242596735423e+261) | -0.0 | (-0.0 -0.0) | +nan.0 | valid | exit | 0 | 0.316066 | #f |
| (-1.0045573678171174e+303 2.3136934101885994e+269 -4.6351404364424365e+206 1.0260072868095172e+160) | 4.887279882416357e+205 | (+nan.0 +nan.0) | +nan.0 | valid | exit | 0 | 5.0 | #f |
| (-4.401603435634084e+150 1.8962222850833104e+168 8.947916632617553e+59 4.195041933642893e-117) | -inf.0 | (-inf.0 -inf.0) | +nan.0 | valid | exit | 0 | 0.297904 | #f |
| (-8.707018232876891e+241 8.473408871413832e+138 1.5257516923147307e-234 6.0544206004278374e+44) | -inf.0 | (-inf.0 -inf.0) | +nan.0 | valid | exit | 0 | 0.284337 | #f |
| (0.29867343054094314 -4.554216389587352e+285 3.8353148338465756e+40 2.589650385073522e-118) | -inf.0 | (-inf.0 -inf.0) | +nan.0 | valid | exit | 0 | 0.301355 | #f |
| (1.7937023373993904e-32 4.8459129480089994e-179 2.2031274837052077e-142 -1.1290068760765859e-38) | -3.4945379972010007e-31 | (-3.4945379972010007e-31 -3.4945379972010007e-31) | +nan.0 | valid | exit | 0 | 0.25112700000000004 | #f |
| (1.2731405661645887e+224 -9.605778141572085e+206 -6.009198949175199e-146 -3.7936984917657314e+216) | -inf.0 | (-inf.0 -inf.0) | +nan.0 | valid | exit | 0 | 0.25693299999999997 | #f |
| (2.8749114770448545e+100 -2.1406637134279834e+160 -4.6851756301499986e+54 -9.08388297350347e-299) | -inf.0 | (-inf.0 -inf.0) | +nan.0 | valid | exit | 0 | 0.311121 | #f |
| (5.088013485037604e+260 -1.7739631358401172e+176 5.713084342922489e-242 -1.1396949991638154e-204) | +inf.0 | (+nan.0 +nan.0) | +nan.0 | valid | exit | 0 | 5.0 | #f |
| (1.3900772044267745e-254 8.407045680668998e-217 7.197130892761022e-292 -8.816458969208288e+297) | -0.0 | (+nan.0 +nan.0) | +nan.0 | valid | exit | 0 | 5.0 | #f |
| (9.667411343399424e-37 -7.077407479958513e-104 -1.3289702468273663e-138 4352053.321842688) | 1.1829732737336466e-8 | (1.1829732737336466e-8 1.1829732737336466e-8) | +nan.0 | valid | exit | 0 | 0.251305 | #f |
| (-5.563828333249245e+260 -6.782266822401644e+208 -6.601572877259247e+182 -7.456566394100035e+201) | 7.665884684409468e+84 | (7.665884684409468e+84 7.665884684409468e+84) | +nan.0 | valid | exit | 0 | 0.308916 | #f |
| (1.1763773444809426e+238 2.015561578253032e+86 -2.023442110025886e-223 -2.641140038433685e-153) | +inf.0 | (+inf.0 +inf.0) | +nan.0 | valid | exit | 0 | 0.281411 | #f |
| (1.0649665719722055e+200 4.636584939637131e-202 -1.7718656248597215e-227 -1.3264223390081663e-31) | 2.1009783932706875e+256 | (2.1009783932706875e+256 2.1009783932706875e+256) | +nan.0 | valid | exit | 0 | 0.288612 | #f |
| (-7.226510981669396e-259 1.3909723679916952e+217 7.322078612405577e-117 5.1196809643203934e-284) | -inf.0 | (-inf.0 -inf.0) | +nan.0 | valid | exit | 0 | 0.317285 | #f |
| (-1.792286041356109e+68 3.1483599296692366e-112 -8.524025663571054e-300 1.4131612522106594e-56) | +inf.0 | (+inf.0 +inf.0) | +nan.0 | valid | exit | 0 | 0.146176 | #f |
| (-1.6323621251794832e+251 -2.9977234473522907e+264 -2.14211134261383e-293 3.7306259557653486e-250) | -inf.0 | (-inf.0 -inf.0) | +nan.0 | valid | exit | 0 | 0.322594 | #f |
| (-32304.07880544994 5.352481755003207e+156 5.9975347290289356e-195 -2.4557036931689786e+255) | 1.1739884434940402e+100 | (1.1739884434940402e+100 1.1739884434940402e+100) | +nan.0 | valid | exit | 0 | 0.23843399999999998 | #f |
| (2.1926079340995736e+226 1.119462013939959e-26 -1.1884906185325906e+231 -2.8951782945498094e+280) | 7.133444237776e-312 | (7.133444237776e-312 7.133444237776e-312) | +nan.0 | valid | exit | 0 | 0.160376 | #f |
| 1× | egg-herbie |
| 1205× | fma-define |
| 591× | div-sub |
| 554× | unsub-neg |
| 342× | times-frac |
| 320× | associate-/r* |
Useful iterations: 0 (0.0ms)
| Iter | Nodes | Cost |
|---|---|---|
| 0 | 45 | 512 |
| 1 | 143 | 512 |
| 2 | 419 | 512 |
| 3 | 1300 | 512 |
| 4 | 3246 | 512 |
| 5 | 6593 | 512 |
| 1× | node limit |
| Inputs |
|---|
(/.f64 (*.f64 a1 a2) (*.f64 b1 b2)) |
(/.f64 (*.f64 a1 a2) (*.f64 b1 b2)) |
(/.f64 (*.f64 (neg.f64 a1) a2) (*.f64 b1 b2)) |
(/.f64 (*.f64 a1 (neg.f64 a2)) (*.f64 b1 b2)) |
(/.f64 (*.f64 a1 a2) (*.f64 (neg.f64 b1) b2)) |
(/.f64 (*.f64 a1 a2) (*.f64 b1 (neg.f64 b2))) |
(neg.f64 (/.f64 (*.f64 (neg.f64 a1) a2) (*.f64 b1 b2))) |
(neg.f64 (/.f64 (*.f64 a1 (neg.f64 a2)) (*.f64 b1 b2))) |
(neg.f64 (/.f64 (*.f64 a1 a2) (*.f64 (neg.f64 b1) b2))) |
(neg.f64 (/.f64 (*.f64 a1 a2) (*.f64 b1 (neg.f64 b2)))) |
(/.f64 (*.f64 a2 a1) (*.f64 b1 b2)) |
(/.f64 (*.f64 b1 a2) (*.f64 a1 b2)) |
(/.f64 (*.f64 b2 a2) (*.f64 b1 a1)) |
(/.f64 (*.f64 a1 b1) (*.f64 a2 b2)) |
(/.f64 (*.f64 a1 b2) (*.f64 b1 a2)) |
(/.f64 (*.f64 a1 a2) (*.f64 b2 b1)) |
| Outputs |
|---|
(/.f64 (*.f64 a1 a2) (*.f64 b1 b2)) |
(*.f64 (/.f64 a1 b1) (/.f64 a2 b2)) |
(*.f64 a1 (/.f64 a2 (*.f64 b1 b2))) |
(*.f64 a1 (/.f64 (/.f64 a2 b1) b2)) |
(/.f64 (*.f64 a1 a2) (*.f64 b1 b2)) |
(*.f64 (/.f64 a1 b1) (/.f64 a2 b2)) |
(*.f64 a1 (/.f64 a2 (*.f64 b1 b2))) |
(*.f64 a1 (/.f64 (/.f64 a2 b1) b2)) |
(/.f64 (*.f64 (neg.f64 a1) a2) (*.f64 b1 b2)) |
(*.f64 (neg.f64 a1) (/.f64 a2 (*.f64 b1 b2))) |
(*.f64 (neg.f64 a2) (/.f64 (/.f64 a1 b2) b1)) |
(*.f64 (neg.f64 a1) (/.f64 (/.f64 a2 b1) b2)) |
(/.f64 (*.f64 a1 (neg.f64 a2)) (*.f64 b1 b2)) |
(*.f64 (neg.f64 a1) (/.f64 a2 (*.f64 b1 b2))) |
(*.f64 (neg.f64 a2) (/.f64 (/.f64 a1 b2) b1)) |
(*.f64 (neg.f64 a1) (/.f64 (/.f64 a2 b1) b2)) |
(/.f64 (*.f64 a1 a2) (*.f64 (neg.f64 b1) b2)) |
(*.f64 (neg.f64 a1) (/.f64 a2 (*.f64 b1 b2))) |
(*.f64 (neg.f64 a2) (/.f64 (/.f64 a1 b2) b1)) |
(*.f64 (neg.f64 a1) (/.f64 (/.f64 a2 b1) b2)) |
(/.f64 (*.f64 a1 a2) (*.f64 b1 (neg.f64 b2))) |
(*.f64 (neg.f64 a1) (/.f64 a2 (*.f64 b1 b2))) |
(*.f64 (neg.f64 a2) (/.f64 (/.f64 a1 b2) b1)) |
(*.f64 (neg.f64 a1) (/.f64 (/.f64 a2 b1) b2)) |
(neg.f64 (/.f64 (*.f64 (neg.f64 a1) a2) (*.f64 b1 b2))) |
(*.f64 (/.f64 a1 b1) (/.f64 a2 b2)) |
(*.f64 a1 (/.f64 a2 (*.f64 b1 b2))) |
(*.f64 a1 (/.f64 (/.f64 a2 b1) b2)) |
(neg.f64 (/.f64 (*.f64 a1 (neg.f64 a2)) (*.f64 b1 b2))) |
(*.f64 (/.f64 a1 b1) (/.f64 a2 b2)) |
(*.f64 a1 (/.f64 a2 (*.f64 b1 b2))) |
(*.f64 a1 (/.f64 (/.f64 a2 b1) b2)) |
(neg.f64 (/.f64 (*.f64 a1 a2) (*.f64 (neg.f64 b1) b2))) |
(*.f64 (/.f64 a1 b1) (/.f64 a2 b2)) |
(*.f64 a1 (/.f64 a2 (*.f64 b1 b2))) |
(*.f64 a1 (/.f64 (/.f64 a2 b1) b2)) |
(neg.f64 (/.f64 (*.f64 a1 a2) (*.f64 b1 (neg.f64 b2)))) |
(*.f64 (/.f64 a1 b1) (/.f64 a2 b2)) |
(*.f64 a1 (/.f64 a2 (*.f64 b1 b2))) |
(*.f64 a1 (/.f64 (/.f64 a2 b1) b2)) |
(/.f64 (*.f64 a2 a1) (*.f64 b1 b2)) |
(*.f64 (/.f64 a1 b1) (/.f64 a2 b2)) |
(*.f64 a1 (/.f64 a2 (*.f64 b1 b2))) |
(*.f64 a1 (/.f64 (/.f64 a2 b1) b2)) |
(/.f64 (*.f64 b1 a2) (*.f64 a1 b2)) |
(*.f64 b1 (/.f64 a2 (*.f64 a1 b2))) |
(*.f64 b1 (/.f64 (/.f64 a2 b2) a1)) |
(*.f64 a2 (/.f64 b1 (*.f64 a1 b2))) |
(/.f64 (*.f64 b2 a2) (*.f64 b1 a1)) |
(*.f64 (/.f64 b2 b1) (/.f64 a2 a1)) |
(/.f64 (*.f64 a2 b2) (*.f64 a1 b1)) |
(*.f64 b2 (/.f64 a2 (*.f64 a1 b1))) |
(*.f64 b2 (/.f64 (/.f64 a2 b1) a1)) |
(/.f64 (*.f64 a1 b1) (*.f64 a2 b2)) |
(*.f64 (/.f64 a1 a2) (/.f64 b1 b2)) |
(*.f64 a1 (/.f64 b1 (*.f64 a2 b2))) |
(*.f64 b1 (/.f64 a1 (*.f64 a2 b2))) |
(/.f64 (*.f64 a1 b2) (*.f64 b1 a2)) |
(*.f64 (/.f64 a1 b1) (/.f64 b2 a2)) |
(*.f64 a1 (/.f64 (/.f64 b2 b1) a2)) |
(*.f64 a1 (/.f64 b2 (*.f64 a2 b1))) |
(/.f64 (*.f64 a1 a2) (*.f64 b2 b1)) |
(*.f64 (/.f64 a1 b1) (/.f64 a2 b2)) |
(*.f64 a1 (/.f64 a2 (*.f64 b1 b2))) |
(*.f64 a1 (/.f64 (/.f64 a2 b1) b2)) |
(negabs a1)
(negabs a2)
(negabs b1)
(negabs b2)
(sort a1 a2)
(sort b1 b2)
Compiled 11 to 7 computations (36.4% saved)
Compiled 4 to 4 computations (0% saved)
| Status | Accuracy | Program |
|---|---|---|
| 84.1% | (/.f64 (*.f64 a1 a2) (*.f64 b1 b2)) |
Compiled 22 to 14 computations (36.4% saved)
| 1× | egg-herbie |
| 2× | *-commutative |
Useful iterations: 0 (0.0ms)
| Iter | Nodes | Cost |
|---|---|---|
| 0 | 14 | 31 |
| 1 | 16 | 31 |
| 1× | saturated |
| Inputs |
|---|
(/.f64 (*.f64 a1 a2) (*.f64 b1 b2)) |
| Outputs |
|---|
(/.f64 (*.f64 a1 a2) (*.f64 b1 b2)) |
| 1× | fuel |
Compiled 11 to 7 computations (36.4% saved)
(sort b1 b2)
(sort a1 a2)
(negabs b2)
(negabs b1)
(negabs a2)
(negabs a1)
Compiled 330 to 210 computations (36.4% saved)
Loading profile data...