quad2p (problem 3.2.1, positive)
Time bar (total: 23.5s)
| 1× | search |
| Probability | Valid | Unknown | Precondition | Infinite | Domain | Can't | Iter |
|---|---|---|---|---|---|---|---|
| 0% | 0% | 99.9% | 0.1% | 0% | 0% | 0% | 0 |
| 0% | 0% | 99.9% | 0.1% | 0% | 0% | 0% | 1 |
| 0% | 0% | 99.9% | 0.1% | 0% | 0% | 0% | 2 |
| 0% | 0% | 99.9% | 0.1% | 0% | 0% | 0% | 3 |
| 25% | 25% | 74.9% | 0.1% | 0% | 0% | 0% | 4 |
| 37.5% | 37.4% | 62.4% | 0.1% | 0% | 0% | 0% | 5 |
| 37.5% | 37.4% | 62.4% | 0.1% | 0% | 0% | 0% | 6 |
| 42.6% | 40.6% | 54.6% | 0.1% | 0% | 4.7% | 0% | 7 |
| 51.2% | 48.4% | 46% | 0.1% | 0% | 5.5% | 0% | 8 |
| 54.5% | 49.9% | 41.7% | 0.1% | 0% | 8.2% | 0% | 9 |
| 60.2% | 53.4% | 35.3% | 0.1% | 0% | 11.1% | 0% | 10 |
| 67.6% | 58.7% | 28.2% | 0.1% | 0% | 13% | 0% | 11 |
| 71.4% | 60.6% | 24.2% | 0.1% | 0% | 15.1% | 0% | 12 |
Compiled 17 to 11 computations (35.3% saved)
| 1.3s | 5594× | 0 | valid |
| 610.0ms | 5577× | 0 | valid-sollya |
| 1.3s | 1871× | 2 | valid |
| 349.0ms | 1866× | 2 | valid-sollya |
| 205.0ms | 1110× | 0 | invalid |
| 134.0ms | 1098× | 0 | invalid-sollya |
| 286.0ms | 791× | 1 | valid |
| 106.0ms | 786× | 1 | valid-sollya |
| 24.0ms | 29× | 0 | exit-sollya |
| 1.0ms | 5× | 2 | exit-sollya |
| 6.0ms | 5× | 1 | exit-sollya |
| Pt | Rival-out | Sollya-interval | Sollya-point | status | Sollya status | Rival iter | sollya-time | check |
|---|---|---|---|---|---|---|---|---|
| (1.3319041680807543e-213 -2.0557236328708423e-216 5.061035450004805e-159) | #f | (+nan.0 +nan.0) | +nan.0 | invalid | exit | 0 | 0.122563 | #f |
| (-1.544655484825699e+84 1.7340612132245873e-279 -3.4710282240421e-167) | #f | (+nan.0 +nan.0) | +nan.0 | invalid | exit | 0 | 0.106121 | #f |
| (-5.120266703132051e+180 -6.801159003479864e+234 -7.994472356583317e+237) | -2.6565643540871086e+54 | (-2.6565643540871086e+54 -2.6565643540871086e+54) | +nan.0 | valid | exit | 0 | 0.125147 | #f |
| (1.2657006212103886e+158 1.0760576961979851e+82 4.717293972592518e-174) | -2.1919335688318788e-256 | (-6.500370347245351e-96 6.500370347245351e-96) | +nan.0 | valid | exit | 1 | 0.252474 | #f |
| (-7.679015328690285e-74 -1.2721400727338138e-229 1.0422363169735937e+154) | -3.684090870685964e+113 | (+nan.0 +nan.0) | +nan.0 | valid | exit | 0 | 5.0 | #f |
| (-7.855485306998535e-67 2.931460474375019e-110 -7.478184031170531e-281) | 1.275504837356687e-171 | (-3.672982260545371e-63 3.672982260545371e-63) | +nan.0 | valid | exit | 1 | 0.19483799999999998 | #f |
| (-4.07545440009543e-296 -2.4297120049561984e-185 -0.02465054648642911) | #f | (+nan.0 +nan.0) | +nan.0 | invalid | exit | 0 | 0.14551 | #f |
| (-3.6560860738996825e+235 -7.05206268633625e+89 1.2560236327341208e+193) | -5.861256126125789e-22 | (+nan.0 +nan.0) | +nan.0 | valid | exit | 0 | 5.0 | #f |
| (-7.334216492230725e-160 -2987245009290726400.0 -2.9029036327030903e+228) | #f | (+nan.0 +nan.0) | +nan.0 | invalid | exit | 0 | 0.07923999999999999 | #f |
| (-7.463558972202246e+177 1.038838967688943e-111 6.588718570976484e+84) | -2.9711699529403033e-47 | (+nan.0 +nan.0) | +nan.0 | valid | exit | 0 | 5.0 | #f |
| (1.6039522265376775e-53 -3.237823553938436e-213 -1.6412715583564408e-306) | 3.1988546533601335e-127 | (3.1988546533601335e-127 3.1988546533601335e-127) | +nan.0 | valid | exit | 0 | 0.214367 | #f |
| (-8.248895229137677e+279 8.510195381579233e-71 -4.717740743742586e-182) | #f | (+nan.0 +nan.0) | +nan.0 | invalid | exit | 0 | 0.169375 | #f |
| (5.4888669703606776e+280 -3.4117407757664206e+31 5.511198208809795e-84) | #f | (+nan.0 +nan.0) | +nan.0 | invalid | exit | 0 | 0.16574 | #f |
| (35275710070884823000.0 -1.7138280916161933e+159 3.6515605930349485e+238) | 9.716760275965184e+139 | (9.716760275965184e+139 9.716760275965184e+139) | +nan.0 | valid | exit | 0 | 0.269106 | #f |
| (4.682572992048228e+71 1.8807197066393182e+24 -1.882046176494526e-190) | 5.003526495337198e-215 | (-2.7991448338890094e-67 2.7991448338890094e-67) | +nan.0 | valid | exit | 1 | 0.128636 | #f |
| (-7.618959034013398e-181 -3.1584040811122644e-217 7.817038446598457e-226) | -3.203120705152414e-23 | (-3.203120705152414e-23 -3.203120705152414e-23) | +nan.0 | valid | exit | 0 | 0.162151 | #f |
| (-3.6273672074399637e-16 -1.7323483846970005e+257 2.1537841154680884e-55) | -9.551546814140253e+272 | (-9.551546814140253e+272 -9.551546814140253e+272) | +nan.0 | valid | exit | 0 | 0.15911899999999998 | #f |
| (-1.778763628341055e+243 -1.668772998372984e-142 2.2032947076823784e+142) | -3.519469252386384e-51 | (-3.519469252386384e-51 -3.519469252386384e-51) | +nan.0 | valid | exit | 0 | 0.13342299999999999 | #f |
| (1.1399157929228718e-293 4.540057750776026e+287 -3.554089702532226e-141) | -0.0 | (-inf.0 +inf.0) | +nan.0 | valid | exit | 2 | 0.23485899999999998 | #f |
| (1.8635618368691303e-72 -4.1283152803027597e-231 -6.375520496537353e+51) | 5.849057881188541e+61 | (+nan.0 +nan.0) | +nan.0 | valid | exit | 0 | 5.0 | #f |
| (2.3621212970132304e-30 -6.492352013384192e+187 -8.500936106507948e+26) | 5.497052180676247e+217 | (5.497052180676247e+217 5.497052180676247e+217) | +nan.0 | valid | exit | 0 | 0.225928 | #f |
| (-1.198080782032233e-8 1.3543800142160387e+169 62.44370701654385) | -2.3052506076992133e-168 | (-6.830488096019044e+157 6.830488096019044e+157) | +nan.0 | valid | exit | 2 | 0.199656 | #f |
| (-1.997933131341322e-217 -6.342142102635283e-244 8.374456803518592e+212) | -6.474225902657488e+214 | (-6.474225902657488e+214 -6.474225902657488e+214) | +nan.0 | valid | exit | 0 | 0.198252 | #f |
| (4.7684309958442e-288 6.952713012663649e+36 -2.298425773381533e+223) | 1.652898493865048e+186 | (-1.2089107566111843e+305 1.2089107566111843e+305) | +nan.0 | valid | exit | 1 | 0.252303 | #f |
| (4.814147744982346e+108 2.079924039623647e+85 -1026988387980.5916) | 2.4688122460626507e-74 | (+nan.0 +nan.0) | +nan.0 | valid | exit | 1 | 5.0 | #f |
| (5.012059522720072e+302 1.8278158071215943e-264 -4.392281167319135e+177) | 2.960308394096581e-63 | (2.960308394096581e-63 2.960308394096581e-63) | +nan.0 | valid | exit | 0 | 0.242742 | #f |
| (-1.487263602318784e-269 -1.8232559184629355e-273 -1.4004833627561538e-271) | #f | (+nan.0 +nan.0) | +nan.0 | invalid | exit | 0 | 0.120975 | #f |
| (-3.1824603933713144e-267 -1.2198464036517884e-285 -3.075103576712467e+87) | #f | (+nan.0 +nan.0) | +nan.0 | invalid | exit | 0 | 0.128841 | #f |
| (-0.17060821946388607 2.0279738521063382e-108 -4.377966470523229e-122) | #f | (+nan.0 +nan.0) | +nan.0 | invalid | exit | 0 | 0.145868 | #f |
| (-1.2989744058534463e+162 2.5377951477790133e-48 -8.103654872234866e-198) | #f | (+nan.0 +nan.0) | +nan.0 | invalid | exit | 0 | 0.142072 | #f |
| (9.011837315259782e-247 -5.019121351881415e+155 -2.4338224950602604e-33) | +inf.0 | (+inf.0 +inf.0) | +nan.0 | valid | exit | 0 | 0.182764 | #f |
| (1.997265221447325e+177 3.852527059117328e-153 1.3743137914760707e-225) | #f | (+nan.0 +nan.0) | +nan.0 | invalid | exit | 0 | 0.173596 | #f |
| (-1.0992920907882528e+287 -3.2659812612707515e+198 3.9249057539417897e+95) | -5.941971726420531e-89 | (-5.941971726420531e-89 -5.941971726420531e-89) | +nan.0 | valid | exit | 0 | 0.185337 | #f |
| (-4.152072255832615e-31 3.638515891500814e+305 -13923.118288439435) | 1.9132963416433548e-302 | (-inf.0 +inf.0) | +nan.0 | valid | exit | 2 | 0.256874 | #f |
| (-4.2508029003995874e+263 6.873695239546683e+223 1.3415043897480603e-201) | -0.0 | (-1.1801197627021373e-59 1.1801197627021373e-59) | +nan.0 | valid | exit | 2 | 0.240208 | #f |
| (-1.130390578978695e-205 3.8424158297593553e+236 5.629090887859282e-21) | -7.324937145352932e-258 | (-inf.0 +inf.0) | +nan.0 | valid | exit | 2 | 0.268675 | #f |
| (6.022297539931453e-240 -2.3697355140872667e+184 1.545882493665978e-128) | +inf.0 | (+inf.0 +inf.0) | +nan.0 | valid | exit | 0 | 0.150395 | #f |
| (-1.0873147935179088e+188 -4.0183382812581435e+115 -3.889613019632597e+80) | #f | (+nan.0 +nan.0) | +nan.0 | invalid | exit | 0 | 0.082663 | #f |
| (3.846684550521461e+304 -4.784260750137774e-166 -2.664296201455854e+298) | 0.0008322388132622413 | (0.0008322388132622413 0.0008322388132622413) | +nan.0 | valid | exit | 0 | 0.13228900000000002 | #f |
| 1× | egg-herbie |
| 1003× | fma-neg |
| 508× | div-sub |
| 395× | times-frac |
| 264× | fma-define |
| 223× | associate-/r* |
Useful iterations: 2 (0.0ms)
| Iter | Nodes | Cost |
|---|---|---|
| 0 | 55 | 631 |
| 1 | 136 | 579 |
| 2 | 281 | 571 |
| 3 | 777 | 571 |
| 4 | 2087 | 571 |
| 5 | 3954 | 571 |
| 6 | 4998 | 571 |
| 7 | 5251 | 571 |
| 8 | 5344 | 571 |
| 9 | 5376 | 571 |
| 10 | 5392 | 571 |
| 11 | 5392 | 571 |
| 1× | saturated |
| Inputs |
|---|
(/.f64 (+.f64 (neg.f64 b_2) (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)))) a) |
(/.f64 (+.f64 (neg.f64 b_2) (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)))) a) |
(/.f64 (+.f64 (neg.f64 b_2) (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 (neg.f64 a) c)))) (neg.f64 a)) |
(/.f64 (+.f64 (neg.f64 (neg.f64 b_2)) (sqrt.f64 (-.f64 (*.f64 (neg.f64 b_2) (neg.f64 b_2)) (*.f64 a c)))) a) |
(/.f64 (+.f64 (neg.f64 b_2) (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a (neg.f64 c))))) a) |
(neg.f64 (/.f64 (+.f64 (neg.f64 b_2) (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 (neg.f64 a) c)))) (neg.f64 a))) |
(neg.f64 (/.f64 (+.f64 (neg.f64 (neg.f64 b_2)) (sqrt.f64 (-.f64 (*.f64 (neg.f64 b_2) (neg.f64 b_2)) (*.f64 a c)))) a)) |
(neg.f64 (/.f64 (+.f64 (neg.f64 b_2) (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a (neg.f64 c))))) a)) |
(/.f64 (+.f64 (neg.f64 a) (sqrt.f64 (-.f64 (*.f64 a a) (*.f64 b_2 c)))) b_2) |
(/.f64 (+.f64 (neg.f64 b_2) (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 c a)))) c) |
(/.f64 (+.f64 (neg.f64 c) (sqrt.f64 (-.f64 (*.f64 c c) (*.f64 a b_2)))) a) |
| Outputs |
|---|
(/.f64 (+.f64 (neg.f64 b_2) (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)))) a) |
(/.f64 (-.f64 (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c))) b_2) a) |
(/.f64 (+.f64 (neg.f64 b_2) (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)))) a) |
(/.f64 (-.f64 (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c))) b_2) a) |
(/.f64 (+.f64 (neg.f64 b_2) (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 (neg.f64 a) c)))) (neg.f64 a)) |
(/.f64 (+.f64 (neg.f64 b_2) (sqrt.f64 (+.f64 (*.f64 b_2 b_2) (*.f64 a c)))) (neg.f64 a)) |
(/.f64 (-.f64 (sqrt.f64 (fma.f64 b_2 b_2 (*.f64 a c))) b_2) (neg.f64 a)) |
(/.f64 (-.f64 b_2 (sqrt.f64 (fma.f64 b_2 b_2 (*.f64 a c)))) a) |
(/.f64 (+.f64 (neg.f64 (neg.f64 b_2)) (sqrt.f64 (-.f64 (*.f64 (neg.f64 b_2) (neg.f64 b_2)) (*.f64 a c)))) a) |
(/.f64 (+.f64 b_2 (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)))) a) |
(/.f64 (+.f64 (neg.f64 b_2) (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a (neg.f64 c))))) a) |
(/.f64 (+.f64 (neg.f64 b_2) (sqrt.f64 (+.f64 (*.f64 b_2 b_2) (*.f64 a c)))) a) |
(/.f64 (-.f64 (sqrt.f64 (fma.f64 b_2 b_2 (*.f64 a c))) b_2) a) |
(neg.f64 (/.f64 (+.f64 (neg.f64 b_2) (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 (neg.f64 a) c)))) (neg.f64 a))) |
(/.f64 (+.f64 (neg.f64 b_2) (sqrt.f64 (+.f64 (*.f64 b_2 b_2) (*.f64 a c)))) a) |
(/.f64 (-.f64 (sqrt.f64 (fma.f64 b_2 b_2 (*.f64 a c))) b_2) a) |
(neg.f64 (/.f64 (+.f64 (neg.f64 (neg.f64 b_2)) (sqrt.f64 (-.f64 (*.f64 (neg.f64 b_2) (neg.f64 b_2)) (*.f64 a c)))) a)) |
(/.f64 (+.f64 b_2 (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)))) (neg.f64 a)) |
(neg.f64 (/.f64 (+.f64 (neg.f64 b_2) (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a (neg.f64 c))))) a)) |
(/.f64 (+.f64 (neg.f64 b_2) (sqrt.f64 (+.f64 (*.f64 b_2 b_2) (*.f64 a c)))) (neg.f64 a)) |
(/.f64 (-.f64 (sqrt.f64 (fma.f64 b_2 b_2 (*.f64 a c))) b_2) (neg.f64 a)) |
(/.f64 (-.f64 b_2 (sqrt.f64 (fma.f64 b_2 b_2 (*.f64 a c)))) a) |
(/.f64 (+.f64 (neg.f64 a) (sqrt.f64 (-.f64 (*.f64 a a) (*.f64 b_2 c)))) b_2) |
(/.f64 (-.f64 (sqrt.f64 (fma.f64 a a (*.f64 (neg.f64 b_2) c))) a) b_2) |
(/.f64 (-.f64 (sqrt.f64 (-.f64 (*.f64 a a) (*.f64 b_2 c))) a) b_2) |
(/.f64 (+.f64 (neg.f64 b_2) (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 c a)))) c) |
(/.f64 (+.f64 (neg.f64 b_2) (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)))) c) |
(/.f64 (-.f64 (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c))) b_2) c) |
(/.f64 (+.f64 (neg.f64 c) (sqrt.f64 (-.f64 (*.f64 c c) (*.f64 a b_2)))) a) |
(/.f64 (+.f64 (neg.f64 c) (sqrt.f64 (-.f64 (*.f64 c c) (*.f64 b_2 a)))) a) |
(/.f64 (-.f64 (sqrt.f64 (-.f64 (*.f64 c c) (*.f64 b_2 a))) c) a) |
(/.f64 (-.f64 (sqrt.f64 (fma.f64 (neg.f64 b_2) a (*.f64 c c))) c) a) |
Compiled 16 to 10 computations (37.5% saved)
Compiled 3 to 3 computations (0% saved)
| Status | Accuracy | Program |
|---|---|---|
| 50.4% | (/.f64 (+.f64 (neg.f64 b_2) (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)))) a) |
Compiled 32 to 20 computations (37.5% saved)
| 1× | egg-herbie |
| 6× | +-commutative |
| 5× | sub-neg |
| 5× | *-commutative |
| 4× | neg-sub0 |
| 4× | neg-mul-1 |
Useful iterations: 1 (0.0ms)
| Iter | Nodes | Cost |
|---|---|---|
| 0 | 17 | 57 |
| 1 | 28 | 53 |
| 2 | 41 | 53 |
| 3 | 48 | 53 |
| 4 | 52 | 53 |
| 5 | 53 | 53 |
| 1× | saturated |
| Inputs |
|---|
(/.f64 (+.f64 (neg.f64 b_2) (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)))) a) |
| Outputs |
|---|
(/.f64 (+.f64 (neg.f64 b_2) (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)))) a) |
(/.f64 (-.f64 (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c))) b_2) a) |
| 1× | fuel |
Compiled 15 to 9 computations (40% saved)
Compiled 246 to 90 computations (63.4% saved)
Loading profile data...