
Time bar (total: 39.1s)
| 1× | search |
| Probability | Valid | Unknown | Precondition | Infinite | Domain | Can't | Iter |
|---|---|---|---|---|---|---|---|
| 0% | 0% | 12.5% | 87.5% | 0% | 0% | 0% | 0 |
| 100% | 12.5% | 0% | 87.5% | 0% | 0% | 0% | 1 |
Compiled 24 to 15 computations (37.5% saved)
| 4.9s | 8256× | 0 | valid |
| 898.0ms | 8214× | 0 | valid-sollya |
| 18.0ms | 42× | 0 | exit-sollya |
| Pt | Rival-out | Sollya-interval | Sollya-point | status | Sollya status | Rival iter | sollya-time | check |
|---|---|---|---|---|---|---|---|---|
| (4.467451109333631e-295 1.3267498048718275e-211) | -4.467451109333631e-295 | (-4.467451109333631e-295 -4.467451109333631e-295) | +nan.0 | valid | exit | 0 | 0.20069 | #f |
| (1.1106280687545495e+185 1.8272214734382e-279) | -inf.0 | (-inf.0 -inf.0) | +nan.0 | valid | exit | 0 | 0.27324499999999996 | #f |
| (9.706016517836275e-163 5.64195209726019e-27) | -9.706016517836275e-163 | (-9.706016517836275e-163 -9.706016517836275e-163) | +nan.0 | valid | exit | 0 | 0.190905 | #f |
| (3.727932235296009e-304 5.756057184541373e-172) | -3.727932235296009e-304 | (-3.727932235296009e-304 -3.727932235296009e-304) | +nan.0 | valid | exit | 0 | 0.15135600000000002 | #f |
| (7.942067012127937e-190 4.111384541020832e-184) | -7.942051670233304e-190 | (-7.942051670233304e-190 -7.942051670233304e-190) | +nan.0 | valid | exit | 0 | 0.22780599999999998 | #f |
| (658427472399401900.0 2.6480291118343506e-270) | -inf.0 | (-inf.0 -inf.0) | +nan.0 | valid | exit | 0 | 0.231893 | #f |
| (7.851123635212495e-204 9.092703267502589e-179) | -7.851123635212495e-204 | (-7.851123635212495e-204 -7.851123635212495e-204) | +nan.0 | valid | exit | 0 | 0.255164 | #f |
| (2.8490712815449342e-70 3.605053135299454e-176) | 2.2516192862299758e+36 | (2.2516192862299758e+36 2.2516192862299758e+36) | +nan.0 | valid | exit | 0 | 0.10301600000000001 | #f |
| (1.4612451835370962e-305 9.72203711717696e-266) | -1.4612451835370962e-305 | (-1.4612451835370962e-305 -1.4612451835370962e-305) | +nan.0 | valid | exit | 0 | 0.113206 | #f |
| (3.852403479508416e-145 6.115622889193158e-180) | 2.4267376909642222e-110 | (2.4267376909642222e-110 2.4267376909642222e-110) | +nan.0 | valid | exit | 0 | 0.10490200000000001 | #f |
| (3.828151107572182e+201 0.00014163539629599156) | -inf.0 | (-inf.0 -inf.0) | +nan.0 | valid | exit | 0 | 0.21884599999999998 | #f |
| (1.9476271958498846e+257 2.8674833884061105e-143) | -inf.0 | (-inf.0 -inf.0) | +nan.0 | valid | exit | 0 | 0.304234 | #f |
| (1.6787741344957435e-279 8.654542883481679e-252) | -1.6787741344957435e-279 | (-1.6787741344957435e-279 -1.6787741344957435e-279) | +nan.0 | valid | exit | 0 | 0.255405 | #f |
| (2.270262165130567e+57 9.237710111622857e-44) | -1.2666706422682247e+215 | (-1.2666706422682247e+215 -1.2666706422682247e+215) | +nan.0 | valid | exit | 0 | 0.23213699999999998 | #f |
| (4.759873563921317e+25 1.4162615147900746e-151) | -7.614524640244493e+227 | (-7.614524640244493e+227 -7.614524640244493e+227) | +nan.0 | valid | exit | 0 | 0.202955 | #f |
| (1.6686101359689502e+72 1.4223264252685314e-249) | -inf.0 | (-inf.0 -inf.0) | +nan.0 | valid | exit | 0 | 0.136436 | #f |
| (1.9678463405482766e+301 1.4727417198040398e-235) | -inf.0 | (-inf.0 -inf.0) | +nan.0 | valid | exit | 0 | 0.29433299999999996 | #f |
| (2.4397930991652333e-21 3.014577668431016e-12) | -2.4397930971906314e-21 | (-2.4397930971906314e-21 -2.4397930971906314e-21) | +nan.0 | valid | exit | 0 | 0.160708 | #f |
| (1.9974607723893246e+175 3.2439895273992706e-241) | -inf.0 | (-inf.0 -inf.0) | +nan.0 | valid | exit | 0 | 0.273928 | #f |
| (4.70322837267146e-96 5.710918974126773e-266) | 3.873344592300776e+74 | (3.873344592300776e+74 3.873344592300776e+74) | +nan.0 | valid | exit | 0 | 0.22258999999999998 | #f |
| (8.817505852793485e-50 3.2584084645885823e-83) | 2.3860854251084246e-16 | (2.3860854251084246e-16 2.3860854251084246e-16) | +nan.0 | valid | exit | 0 | 0.16688999999999998 | #f |
| (4.402861319197671e+192 1.151802526556565e-246) | -inf.0 | (-inf.0 -inf.0) | +nan.0 | valid | exit | 0 | 0.24243800000000001 | #f |
| (4.33518086158513e-118 2.0032127630656662e-245) | 9381825759.682384 | (+nan.0 +nan.0) | +nan.0 | valid | exit | 0 | 5.0 | #f |
| (8.815324099739214e-184 9.598760025227561e-44) | -8.815324099739214e-184 | (-8.815324099739214e-184 -8.815324099739214e-184) | +nan.0 | valid | exit | 0 | 0.106075 | #f |
| (1.3013696762169458e+234 9.251921190550498e-260) | -inf.0 | (-inf.0 -inf.0) | +nan.0 | valid | exit | 0 | 0.147365 | #f |
| (8.589176154470147e-176 1.6861396800230963e-298) | 4.37531646319527e-53 | (4.37531646319527e-53 4.37531646319527e-53) | +nan.0 | valid | exit | 0 | 0.23385 | #f |
| (1.8778133182333167e-284 1.3581230465416365e-278) | -1.877810721868527e-284 | (-1.877810721868527e-284 -1.877810721868527e-284) | +nan.0 | valid | exit | 0 | 0.234732 | #f |
| (4.696629881584244 3.649564667854248e-276) | -2.2342799082720974e+277 | (+nan.0 +nan.0) | +nan.0 | valid | exit | 0 | 5.0 | #f |
| (6.0854797191377e+157 8.057259055228486e-228) | -inf.0 | (-inf.0 -inf.0) | +nan.0 | valid | exit | 0 | 0.281383 | #f |
| (3.2909169465792945e-294 4.9121029612088715e-214) | -3.2909169465792945e-294 | (-3.2909169465792945e-294 -3.2909169465792945e-294) | +nan.0 | valid | exit | 0 | 0.10919000000000001 | #f |
| (1.0782545099091704e-61 1.3294367323121485e-278) | 8.7453036303384e+155 | (8.7453036303384e+155 8.7453036303384e+155) | +nan.0 | valid | exit | 0 | 0.241205 | #f |
| (3.0404504390726845e-150 3.7205890611722126e-108) | -3.0404504390726845e-150 | (-3.0404504390726845e-150 -3.0404504390726845e-150) | +nan.0 | valid | exit | 0 | 0.23759 | #f |
| (7.353191737667569e+64 2.0612606689316534e-32) | -1.9288335657738268e+226 | (-1.9288335657738268e+226 -1.9288335657738268e+226) | +nan.0 | valid | exit | 0 | 0.240612 | #f |
| (2.3523636442418328e-14 8.133359172156947e-145) | 6.803603034886119e+116 | (6.803603034886119e+116 6.803603034886119e+116) | +nan.0 | valid | exit | 0 | 0.236143 | #f |
| (2.110103856958202e+163 6.560009378641646e-9) | -inf.0 | (-inf.0 -inf.0) | +nan.0 | valid | exit | 0 | 0.12231399999999999 | #f |
| (6.796421640957155e+182 3.6975409928601268e-112) | -inf.0 | (-inf.0 -inf.0) | +nan.0 | valid | exit | 0 | 0.12966 | #f |
| (3.1576740885089763e+254 7.788812609351329e-115) | -inf.0 | (-inf.0 -inf.0) | +nan.0 | valid | exit | 0 | 0.289315 | #f |
| (2.347758899546431e-47 1.2094694502193704e-290) | 4.557346900659394e+196 | (4.557346900659394e+196 4.557346900659394e+196) | +nan.0 | valid | exit | 0 | 0.26666599999999996 | #f |
| (1.232254739355135e+39 1.3407148771610399e-191) | -1.3956131823798896e+308 | (-1.3956131823798896e+308 -1.3956131823798896e+308) | +nan.0 | valid | exit | 0 | 0.12487500000000001 | #f |
| (1.9569175497941356e-22 1.234332374724738e-246) | 3.1025081858897898e+202 | (3.1025081858897898e+202 3.1025081858897898e+202) | +nan.0 | valid | exit | 0 | 0.178293 | #f |
| (1.1517619949294266e+131 2.866808112469308e-110) | -inf.0 | (-inf.0 -inf.0) | +nan.0 | valid | exit | 0 | 0.265759 | #f |
| (1.938294007240208e+156 1.0219631614618242e-197) | -inf.0 | (-inf.0 -inf.0) | +nan.0 | valid | exit | 0 | 0.270716 | #f |
| 1× | egg-herbie |
| 2395× | fma-define |
| 608× | div-sub |
| 525× | fma-neg |
| 375× | sub-neg |
| 318× | unsub-neg |
Useful iterations: 3 (0.0ms)
| Iter | Nodes | Cost |
|---|---|---|
| 0 | 31 | 341 |
| 1 | 80 | 297 |
| 2 | 218 | 289 |
| 3 | 810 | 273 |
| 4 | 3188 | 273 |
| 5 | 4841 | 273 |
| 6 | 5769 | 273 |
| 7 | 6355 | 273 |
| 8 | 6715 | 273 |
| 9 | 6860 | 273 |
| 10 | 7003 | 273 |
| 11 | 7155 | 273 |
| 12 | 7351 | 273 |
| 13 | 7435 | 273 |
| 14 | 7435 | 273 |
| 15 | 7491 | 273 |
| 16 | 7529 | 273 |
| 1× | node limit |
| Inputs |
|---|
(*.f64 (-.f64 (/.f64 (*.f64 m (-.f64 #s(literal 1 binary64) m)) v) #s(literal 1 binary64)) m) |
(*.f64 (-.f64 (/.f64 (*.f64 m (-.f64 #s(literal 1 binary64) m)) v) #s(literal 1 binary64)) m) |
(*.f64 (-.f64 (/.f64 (*.f64 (neg.f64 m) (-.f64 #s(literal 1 binary64) (neg.f64 m))) v) #s(literal 1 binary64)) (neg.f64 m)) |
(*.f64 (-.f64 (/.f64 (*.f64 m (-.f64 #s(literal 1 binary64) m)) (neg.f64 v)) #s(literal 1 binary64)) m) |
(neg.f64 (*.f64 (-.f64 (/.f64 (*.f64 (neg.f64 m) (-.f64 #s(literal 1 binary64) (neg.f64 m))) v) #s(literal 1 binary64)) (neg.f64 m))) |
(neg.f64 (*.f64 (-.f64 (/.f64 (*.f64 m (-.f64 #s(literal 1 binary64) m)) (neg.f64 v)) #s(literal 1 binary64)) m)) |
(*.f64 (-.f64 (/.f64 (*.f64 v (-.f64 #s(literal 1 binary64) v)) m) #s(literal 1 binary64)) v) |
| Outputs |
|---|
(*.f64 (-.f64 (/.f64 (*.f64 m (-.f64 #s(literal 1 binary64) m)) v) #s(literal 1 binary64)) m) |
(*.f64 m (+.f64 (*.f64 m (/.f64 (-.f64 #s(literal 1 binary64) m) v)) #s(literal -1 binary64))) |
(*.f64 m (fma.f64 m (/.f64 (-.f64 #s(literal 1 binary64) m) v) #s(literal -1 binary64))) |
(*.f64 m (fma.f64 (-.f64 #s(literal 1 binary64) m) (/.f64 m v) #s(literal -1 binary64))) |
(*.f64 (-.f64 (/.f64 (*.f64 m (-.f64 #s(literal 1 binary64) m)) v) #s(literal 1 binary64)) m) |
(*.f64 m (+.f64 (*.f64 m (/.f64 (-.f64 #s(literal 1 binary64) m) v)) #s(literal -1 binary64))) |
(*.f64 m (fma.f64 m (/.f64 (-.f64 #s(literal 1 binary64) m) v) #s(literal -1 binary64))) |
(*.f64 m (fma.f64 (-.f64 #s(literal 1 binary64) m) (/.f64 m v) #s(literal -1 binary64))) |
(*.f64 (-.f64 (/.f64 (*.f64 (neg.f64 m) (-.f64 #s(literal 1 binary64) (neg.f64 m))) v) #s(literal 1 binary64)) (neg.f64 m)) |
(*.f64 (neg.f64 m) (+.f64 (*.f64 (neg.f64 m) (/.f64 (-.f64 #s(literal 1 binary64) (neg.f64 m)) v)) #s(literal -1 binary64))) |
(*.f64 (neg.f64 m) (fma.f64 (neg.f64 m) (/.f64 (+.f64 m #s(literal 1 binary64)) v) #s(literal -1 binary64))) |
(*.f64 m (+.f64 #s(literal 1 binary64) (*.f64 m (/.f64 (+.f64 m #s(literal 1 binary64)) v)))) |
(*.f64 m (fma.f64 m (/.f64 (+.f64 m #s(literal 1 binary64)) v) #s(literal 1 binary64))) |
(*.f64 (-.f64 (/.f64 (*.f64 m (-.f64 #s(literal 1 binary64) m)) (neg.f64 v)) #s(literal 1 binary64)) m) |
(*.f64 m (+.f64 (*.f64 m (/.f64 (-.f64 #s(literal 1 binary64) m) (neg.f64 v))) #s(literal -1 binary64))) |
(*.f64 m (fma.f64 m (/.f64 (-.f64 #s(literal 1 binary64) m) (neg.f64 v)) #s(literal -1 binary64))) |
(*.f64 m (fma.f64 (-.f64 #s(literal 1 binary64) m) (/.f64 m (neg.f64 v)) #s(literal -1 binary64))) |
(*.f64 m (fma.f64 (/.f64 m v) (+.f64 m #s(literal -1 binary64)) #s(literal -1 binary64))) |
(neg.f64 (*.f64 (-.f64 (/.f64 (*.f64 (neg.f64 m) (-.f64 #s(literal 1 binary64) (neg.f64 m))) v) #s(literal 1 binary64)) (neg.f64 m))) |
(*.f64 (+.f64 (*.f64 (neg.f64 m) (/.f64 (-.f64 #s(literal 1 binary64) (neg.f64 m)) v)) #s(literal -1 binary64)) (neg.f64 (neg.f64 m))) |
(*.f64 m (fma.f64 (neg.f64 m) (/.f64 (+.f64 m #s(literal 1 binary64)) v) #s(literal -1 binary64))) |
(*.f64 m (-.f64 #s(literal -1 binary64) (*.f64 m (/.f64 (+.f64 m #s(literal 1 binary64)) v)))) |
(*.f64 m (fma.f64 (-.f64 #s(literal -1 binary64) m) (/.f64 m v) #s(literal -1 binary64))) |
(*.f64 m (fma.f64 (/.f64 m v) (-.f64 #s(literal -1 binary64) m) #s(literal -1 binary64))) |
(neg.f64 (*.f64 (-.f64 (/.f64 (*.f64 m (-.f64 #s(literal 1 binary64) m)) (neg.f64 v)) #s(literal 1 binary64)) m)) |
(*.f64 (+.f64 (*.f64 m (/.f64 (-.f64 #s(literal 1 binary64) m) (neg.f64 v))) #s(literal -1 binary64)) (neg.f64 m)) |
(*.f64 (neg.f64 m) (fma.f64 m (/.f64 (-.f64 #s(literal 1 binary64) m) (neg.f64 v)) #s(literal -1 binary64))) |
(*.f64 m (+.f64 #s(literal 1 binary64) (*.f64 (-.f64 #s(literal 1 binary64) m) (/.f64 m v)))) |
(*.f64 m (fma.f64 (-.f64 #s(literal 1 binary64) m) (/.f64 m v) #s(literal 1 binary64))) |
(*.f64 (-.f64 (/.f64 (*.f64 v (-.f64 #s(literal 1 binary64) v)) m) #s(literal 1 binary64)) v) |
(*.f64 v (+.f64 (*.f64 v (/.f64 (-.f64 #s(literal 1 binary64) v) m)) #s(literal -1 binary64))) |
(*.f64 v (fma.f64 v (/.f64 (-.f64 #s(literal 1 binary64) v) m) #s(literal -1 binary64))) |
Compiled 13 to 8 computations (38.5% saved)
Compiled 2 to 2 computations (0% saved)
| Status | Accuracy | Program |
|---|---|---|
| 99.9% | (*.f64 (-.f64 (/.f64 (*.f64 m (-.f64 #s(literal 1 binary64) m)) v) #s(literal 1 binary64)) m) |
Compiled 26 to 16 computations (38.5% saved)
| 1× | egg-herbie |
| 6× | unsub-neg |
| 5× | neg-mul-1 |
| 4× | sub-neg |
| 4× | *-commutative |
| 4× | +-commutative |
Useful iterations: 0 (0.0ms)
| Iter | Nodes | Cost |
|---|---|---|
| 0 | 13 | 43 |
| 1 | 25 | 43 |
| 2 | 32 | 43 |
| 3 | 38 | 43 |
| 4 | 46 | 43 |
| 5 | 57 | 43 |
| 1× | saturated |
| Inputs |
|---|
(*.f64 (-.f64 (/.f64 (*.f64 m (-.f64 #s(literal 1 binary64) m)) v) #s(literal 1 binary64)) m) |
| Outputs |
|---|
(*.f64 (-.f64 (/.f64 (*.f64 m (-.f64 #s(literal 1 binary64) m)) v) #s(literal 1 binary64)) m) |
(*.f64 m (-.f64 (/.f64 (*.f64 m (-.f64 #s(literal 1 binary64) m)) v) #s(literal 1 binary64))) |
(*.f64 m (+.f64 (/.f64 (*.f64 m (-.f64 #s(literal 1 binary64) m)) v) #s(literal -1 binary64))) |
| 1× | fuel |
Compiled 13 to 9 computations (30.8% saved)
Compiled 52 to 34 computations (34.6% saved)
Loading profile data...