
Time bar (total: 11.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 |
| 75% | 74.9% | 25% | 0.2% | 0% | 0% | 0% | 5 |
| 75% | 74.9% | 25% | 0.2% | 0% | 0% | 0% | 6 |
| 75% | 74.9% | 25% | 0.2% | 0% | 0% | 0% | 7 |
| 87.5% | 87.3% | 12.5% | 0.2% | 0% | 0% | 0% | 8 |
| 93.8% | 93.6% | 6.2% | 0.2% | 0% | 0% | 0% | 9 |
| 93.8% | 93.6% | 6.2% | 0.2% | 0% | 0% | 0% | 10 |
| 93.8% | 93.6% | 6.2% | 0.2% | 0% | 0% | 0% | 11 |
| 96.9% | 96.7% | 3.1% | 0.2% | 0% | 0% | 0% | 12 |
Compiled 20 to 12 computations (40% saved)
| 1.4s | 8256× | 0 | valid |
| 907.0ms | 8222× | 0 | valid-sollya |
| 16.0ms | 34× | 0 | exit-sollya |
| Pt | Rival-out | Sollya-interval | Sollya-point | status | Sollya status | Rival iter | sollya-time | check |
|---|---|---|---|---|---|---|---|---|
| (1.3261937674407727e-185 6.445488212116569e-209 -9.516625473031852e-272 -1.8070287943606885e+173) | 0.0 | (0.0 0.0) | +nan.0 | valid | exit | 0 | 0.14713199999999999 | #f |
| (-3.329843755258863e-20 -5.747937453122066e+276 2.8246164697311807e-11 3.5313348141955802e+233) | -1.3019482695942739e-201 | (-1.3019482695942739e-201 -1.3019482695942739e-201) | +nan.0 | valid | exit | 0 | 0.154346 | #f |
| (-1.5615422584092564e-187 -1.6960312299803485e+131 5.2629150551737286e-55 -3.407311561595066e-243) | -3.22260802654046e+185 | (-3.22260802654046e+185 -3.22260802654046e+185) | +nan.0 | valid | exit | 0 | 0.140898 | #f |
| (-5.071312566490147e-14 1.989830745291319e-94 5.032030952912465e-287 2.8105770912032607e+42) | 1.8043670043290018e-56 | (1.8043670043290018e-56 1.8043670043290018e-56) | +nan.0 | valid | exit | 0 | 0.135754 | #f |
| (-6.578871972789633e-241 -1.1941658495152843e+24 -4.030061045305196e-297 -7.071356320826341e+69) | -9.3035503718203e-311 | (-9.3035503718203e-311 -9.3035503718203e-311) | +nan.0 | valid | exit | 0 | 0.144016 | #f |
| (2.1030239671850807e+173 -5.4511311608258696e-185 3.3173802682817033e+120 1.6058536101962492e+131) | -1.3095988039209085e+42 | (-1.3095988039209085e+42 -1.3095988039209085e+42) | +nan.0 | valid | exit | 0 | 0.13883 | #f |
| (-6.434984163255315e+186 3.249758004185368e-12 8.981848247843932e-27 7.76741279562871e+294) | 8.284591449648137e-109 | (8.284591449648137e-109 8.284591449648137e-109) | +nan.0 | valid | exit | 0 | 0.150901 | #f |
| (7.915299113292364e-244 8.951916515853211e-14 1.7569541922492535e+267 59514361675232590.0) | 5.095133700892317e-281 | (5.095133700892317e-281 5.095133700892317e-281) | +nan.0 | valid | exit | 0 | 0.14143399999999998 | #f |
| (-6.683624666135739e-157 6.90455574728526e-169 -6.228939166536939e-104 1.753731736621866e+101) | 3.8110872527232146e-258 | (3.8110872527232146e-258 3.8110872527232146e-258) | +nan.0 | valid | exit | 0 | 0.15324300000000002 | #f |
| (4.370259213403307e-89 5.230548731567441e+267 -9.839281495515029e+105 -5.254941471529736e+38) | -5.315986471117475e+161 | (-5.315986471117475e+161 -5.315986471117475e+161) | +nan.0 | valid | exit | 0 | 0.141116 | #f |
| (3.9365291868072335e-94 2.9079454895024405e-75 -2.929956615923602e-285 2.1833740564589357e-154) | -1.802956838825693e+60 | (-1.802956838825693e+60 -1.802956838825693e+60) | +nan.0 | valid | exit | 0 | 0.13219499999999998 | #f |
| (1.8940580317668876e-133 -7.319255421975614e+162 1.8237179601798587e+71 -3.009680520200215e+132) | -1.4736141514239667e-31 | (-1.4736141514239667e-31 -1.4736141514239667e-31) | +nan.0 | valid | exit | 0 | 0.155396 | #f |
| (-2.179431046184964e+167 -1.9258069492501614e-10 3.2462712253655266e-89 -1.6430898261208494e-164) | -3.3980896719236276e+180 | (-3.3980896719236276e+180 -3.3980896719236276e+180) | +nan.0 | valid | exit | 0 | 0.143461 | #f |
| (-1.398152773077762e+277 3.2829374582096898e+87 -4.8240560384659687e-287 2.1046053807413158e+276) | 6.643301332743356 | (6.643301332743356 6.643301332743356) | +nan.0 | valid | exit | 0 | 0.288775 | #f |
| (1.9570762319632775e+201 3.237119796524235e-23 2.025041579557727e+65 5.162460995882988e-277) | 1.5985448541907117e-88 | (+nan.0 +nan.0) | +nan.0 | valid | exit | 0 | 5.0 | #f |
| (-1.5125804894715259e+301 2.718139681601014e-204 3.981951905769198e-27 1.0808999317043453e-271) | 1.0311265347442292e+83 | (1.0311265347442292e+83 1.0311265347442292e+83) | +nan.0 | valid | exit | 0 | 0.142008 | #f |
| (-5.794122948286781e-146 3.323463383350746e+184 1.101177205749489e+168 -1.4989979234460192e+295) | 1.628718572659183e-238 | (1.628718572659183e-238 1.628718572659183e-238) | +nan.0 | valid | exit | 0 | 0.30722099999999997 | #f |
| (3.007024017926502e-249 1.4128603484003612e+23 -8.607108930050584e-121 -1.4246295553108862e+33) | -5.99173553867649e-164 | (+nan.0 +nan.0) | +nan.0 | valid | exit | 0 | 5.0 | #f |
| (-3.2180832747385427e+71 7.022690191913607e-304 7.20058524355245e+69 -1.6328150671958711e+140) | -1.9708804379574628e-69 | (-1.9708804379574628e-69 -1.9708804379574628e-69) | +nan.0 | valid | exit | 0 | 0.209441 | #f |
| (-5.337340860082788e-216 6.745441175954479e+19 -1.0433891152024583e+213 -2.953956230704254e+31) | -6.46493343439336e-194 | (-6.46493343439336e-194 -6.46493343439336e-194) | +nan.0 | valid | exit | 0 | 0.209237 | #f |
| (-9.040529930926517e+268 -2.2074382365989352e+86 -3.617040640039829e-242 -5.1885838776754757e-163) | -inf.0 | (-inf.0 -inf.0) | +nan.0 | valid | exit | 0 | 0.327059 | #f |
| (5.3803256671707116e+131 -2.824698659778561e+178 6.953960528057684e-162 -1.723347277480942e+261) | 3.1220205802252826e-130 | (3.1220205802252826e-130 3.1220205802252826e-130) | +nan.0 | valid | exit | 0 | 0.149258 | #f |
| (-8.043497256728772e-233 -2.7364693022950365e+54 -2.7825938093396507e-50 5.220305612673427e-113) | 9.834239166026319e+103 | (9.834239166026319e+103 9.834239166026319e+103) | +nan.0 | valid | exit | 0 | 0.28689600000000004 | #f |
| (5.969363771564362e-244 2.5227958143436328e+36 1.4211825226696791e+211 7.284155663747371e-203) | 1.775138501988177e-175 | (1.775138501988177e-175 1.775138501988177e-175) | +nan.0 | valid | exit | 0 | 0.254305 | #f |
| (-3.2760481887028495e+93 2.0688549177620817e-148 -4.6092374962612384e-156 3.684001342630087e+86) | 8892635.70779268 | (8892635.70779268 8892635.70779268) | +nan.0 | valid | exit | 0 | 0.1472 | #f |
| (-8.39716017254542e+174 -3.25000868994865e+38 -2.250191898133805e+204 1.5389812714236548e-290) | 1.444325122956865e-166 | (1.444325122956865e-166 1.444325122956865e-166) | +nan.0 | valid | exit | 0 | 0.159528 | #f |
| (9.392096908118912e-222 -1.3699285511130528e-134 -1.6623860619242682e+281 8.215725890515788e+281) | 0.0 | (0.0 0.0) | +nan.0 | valid | exit | 0 | 0.16975900000000002 | #f |
| (3.061834661377426e-75 -1.905380927933493e-211 6.077974562682797e-31 8.453109301641088e+130) | -3.6221401523614525e-206 | (-3.6221401523614525e-206 -3.6221401523614525e-206) | +nan.0 | valid | exit | 0 | 0.28690699999999997 | #f |
| (1.1340927362926456e-32 -1.4107626871624717e-11 3.192823378754124e-186 -1.1012217337321694e+233) | 1.0298495766597998e-265 | (1.0298495766597998e-265 1.0298495766597998e-265) | +nan.0 | valid | exit | 0 | 0.167608 | #f |
| (-2.5317631581771228e+175 1.5983641180900696e-252 6.179812916442369e-274 -2.4458077721556236e+60) | -1.035143966341125e+115 | (-1.035143966341125e+115 -1.035143966341125e+115) | +nan.0 | valid | exit | 0 | 0.28589400000000004 | #f |
| (-2.890048668895932e-34 5.532894967211416e+229 -9.987953461746905e+83 609353696572.0065) | -5.539568229269368e+145 | (-5.539568229269368e+145 -5.539568229269368e+145) | +nan.0 | valid | exit | 0 | 0.150248 | #f |
| (-1.56731563836302e+301 -3.119617117277144e+105 5.919002604222885e-65 -1.2215781969912902e+94) | -1.2830252228005301e+207 | (-1.2830252228005301e+207 -1.2830252228005301e+207) | +nan.0 | valid | exit | 0 | 0.29398 | #f |
| (1940337430.9895518 1.4603136043973553e-17 5.178706376780491e+199 3.88480357418887e-90) | 2.8198424435586674e-217 | (2.8198424435586674e-217 2.8198424435586674e-217) | +nan.0 | valid | exit | 0 | 0.28615599999999997 | #f |
| (-1.3987246589151714e-10 -6.691000095431778e-279 4.3839016237549705e+302 -1.797194669835228e-254) | -0.0 | (-0.0 -0.0) | +nan.0 | valid | exit | 0 | 0.340353 | #f |
| 1× | egg-herbie |
| 1255× | fma-define |
| 795× | fma-neg |
| 518× | div-sub |
| 436× | unsub-neg |
| 415× | distribute-rgt-in |
Useful iterations: 1 (0.0ms)
| Iter | Nodes | Cost |
|---|---|---|
| 0 | 70 | 1024 |
| 1 | 237 | 992 |
| 2 | 469 | 992 |
| 3 | 1150 | 992 |
| 4 | 3391 | 992 |
| 5 | 5801 | 992 |
| 6 | 6625 | 992 |
| 7 | 6734 | 992 |
| 8 | 6754 | 992 |
| 9 | 6770 | 992 |
| 10 | 7716 | 992 |
| 1× | node limit |
| Inputs |
|---|
(/.f64 (-.f64 (*.f64 b c) (*.f64 a d)) (+.f64 (*.f64 c c) (*.f64 d d))) |
(/.f64 (-.f64 (*.f64 b c) (*.f64 a d)) (+.f64 (*.f64 c c) (*.f64 d d))) |
(/.f64 (-.f64 (*.f64 b c) (*.f64 (neg.f64 a) d)) (+.f64 (*.f64 c c) (*.f64 d d))) |
(/.f64 (-.f64 (*.f64 (neg.f64 b) c) (*.f64 a d)) (+.f64 (*.f64 c c) (*.f64 d d))) |
(/.f64 (-.f64 (*.f64 b (neg.f64 c)) (*.f64 a d)) (+.f64 (*.f64 (neg.f64 c) (neg.f64 c)) (*.f64 d d))) |
(/.f64 (-.f64 (*.f64 b c) (*.f64 a (neg.f64 d))) (+.f64 (*.f64 c c) (*.f64 (neg.f64 d) (neg.f64 d)))) |
(neg.f64 (/.f64 (-.f64 (*.f64 b c) (*.f64 (neg.f64 a) d)) (+.f64 (*.f64 c c) (*.f64 d d)))) |
(neg.f64 (/.f64 (-.f64 (*.f64 (neg.f64 b) c) (*.f64 a d)) (+.f64 (*.f64 c c) (*.f64 d d)))) |
(neg.f64 (/.f64 (-.f64 (*.f64 b (neg.f64 c)) (*.f64 a d)) (+.f64 (*.f64 (neg.f64 c) (neg.f64 c)) (*.f64 d d)))) |
(neg.f64 (/.f64 (-.f64 (*.f64 b c) (*.f64 a (neg.f64 d))) (+.f64 (*.f64 c c) (*.f64 (neg.f64 d) (neg.f64 d))))) |
(/.f64 (-.f64 (*.f64 a c) (*.f64 b d)) (+.f64 (*.f64 c c) (*.f64 d d))) |
(/.f64 (-.f64 (*.f64 b a) (*.f64 c d)) (+.f64 (*.f64 a a) (*.f64 d d))) |
(/.f64 (-.f64 (*.f64 b c) (*.f64 d a)) (+.f64 (*.f64 c c) (*.f64 a a))) |
(/.f64 (-.f64 (*.f64 c b) (*.f64 a d)) (+.f64 (*.f64 b b) (*.f64 d d))) |
(/.f64 (-.f64 (*.f64 d c) (*.f64 a b)) (+.f64 (*.f64 c c) (*.f64 b b))) |
(/.f64 (-.f64 (*.f64 b d) (*.f64 a c)) (+.f64 (*.f64 d d) (*.f64 c c))) |
| Outputs |
|---|
(/.f64 (-.f64 (*.f64 b c) (*.f64 a d)) (+.f64 (*.f64 c c) (*.f64 d d))) |
(/.f64 (-.f64 (*.f64 b c) (*.f64 a d)) (fma.f64 c c (*.f64 d d))) |
(/.f64 (fma.f64 b c (*.f64 a (neg.f64 d))) (fma.f64 d d (*.f64 c c))) |
(/.f64 (-.f64 (*.f64 b c) (*.f64 a d)) (+.f64 (*.f64 c c) (*.f64 d d))) |
(/.f64 (-.f64 (*.f64 b c) (*.f64 a d)) (fma.f64 c c (*.f64 d d))) |
(/.f64 (fma.f64 b c (*.f64 a (neg.f64 d))) (fma.f64 d d (*.f64 c c))) |
(/.f64 (-.f64 (*.f64 b c) (*.f64 (neg.f64 a) d)) (+.f64 (*.f64 c c) (*.f64 d d))) |
(/.f64 (+.f64 (*.f64 b c) (*.f64 a d)) (fma.f64 c c (*.f64 d d))) |
(/.f64 (fma.f64 b c (*.f64 a d)) (fma.f64 c c (*.f64 d d))) |
(/.f64 (fma.f64 b c (*.f64 a d)) (fma.f64 d d (*.f64 c c))) |
(/.f64 (-.f64 (*.f64 (neg.f64 b) c) (*.f64 a d)) (+.f64 (*.f64 c c) (*.f64 d d))) |
(/.f64 (-.f64 (*.f64 b (neg.f64 c)) (*.f64 a d)) (fma.f64 c c (*.f64 d d))) |
(/.f64 (neg.f64 (fma.f64 b c (*.f64 a d))) (fma.f64 c c (*.f64 d d))) |
(/.f64 (neg.f64 (fma.f64 b c (*.f64 a d))) (fma.f64 d d (*.f64 c c))) |
(/.f64 (-.f64 (*.f64 b (neg.f64 c)) (*.f64 a d)) (+.f64 (*.f64 (neg.f64 c) (neg.f64 c)) (*.f64 d d))) |
(/.f64 (-.f64 (*.f64 b (neg.f64 c)) (*.f64 a d)) (fma.f64 c c (*.f64 d d))) |
(/.f64 (neg.f64 (fma.f64 b c (*.f64 a d))) (fma.f64 c c (*.f64 d d))) |
(/.f64 (neg.f64 (fma.f64 b c (*.f64 a d))) (fma.f64 d d (*.f64 c c))) |
(/.f64 (-.f64 (*.f64 b c) (*.f64 a (neg.f64 d))) (+.f64 (*.f64 c c) (*.f64 (neg.f64 d) (neg.f64 d)))) |
(/.f64 (+.f64 (*.f64 b c) (*.f64 a d)) (fma.f64 c c (*.f64 d d))) |
(/.f64 (fma.f64 b c (*.f64 a d)) (fma.f64 c c (*.f64 d d))) |
(/.f64 (fma.f64 b c (*.f64 a d)) (fma.f64 d d (*.f64 c c))) |
(neg.f64 (/.f64 (-.f64 (*.f64 b c) (*.f64 (neg.f64 a) d)) (+.f64 (*.f64 c c) (*.f64 d d)))) |
(/.f64 (-.f64 (*.f64 b (neg.f64 c)) (*.f64 a d)) (fma.f64 c c (*.f64 d d))) |
(/.f64 (neg.f64 (fma.f64 b c (*.f64 a d))) (fma.f64 c c (*.f64 d d))) |
(/.f64 (neg.f64 (fma.f64 b c (*.f64 a d))) (fma.f64 d d (*.f64 c c))) |
(neg.f64 (/.f64 (-.f64 (*.f64 (neg.f64 b) c) (*.f64 a d)) (+.f64 (*.f64 c c) (*.f64 d d)))) |
(/.f64 (+.f64 (*.f64 b c) (*.f64 a d)) (fma.f64 c c (*.f64 d d))) |
(/.f64 (fma.f64 b c (*.f64 a d)) (fma.f64 c c (*.f64 d d))) |
(/.f64 (fma.f64 b c (*.f64 a d)) (fma.f64 d d (*.f64 c c))) |
(neg.f64 (/.f64 (-.f64 (*.f64 b (neg.f64 c)) (*.f64 a d)) (+.f64 (*.f64 (neg.f64 c) (neg.f64 c)) (*.f64 d d)))) |
(/.f64 (+.f64 (*.f64 b c) (*.f64 a d)) (fma.f64 c c (*.f64 d d))) |
(/.f64 (fma.f64 b c (*.f64 a d)) (fma.f64 c c (*.f64 d d))) |
(/.f64 (fma.f64 b c (*.f64 a d)) (fma.f64 d d (*.f64 c c))) |
(neg.f64 (/.f64 (-.f64 (*.f64 b c) (*.f64 a (neg.f64 d))) (+.f64 (*.f64 c c) (*.f64 (neg.f64 d) (neg.f64 d))))) |
(/.f64 (-.f64 (*.f64 b (neg.f64 c)) (*.f64 a d)) (fma.f64 c c (*.f64 d d))) |
(/.f64 (neg.f64 (fma.f64 b c (*.f64 a d))) (fma.f64 c c (*.f64 d d))) |
(/.f64 (neg.f64 (fma.f64 b c (*.f64 a d))) (fma.f64 d d (*.f64 c c))) |
(/.f64 (-.f64 (*.f64 a c) (*.f64 b d)) (+.f64 (*.f64 c c) (*.f64 d d))) |
(/.f64 (-.f64 (*.f64 c a) (*.f64 b d)) (fma.f64 c c (*.f64 d d))) |
(/.f64 (fma.f64 b (neg.f64 d) (*.f64 c a)) (fma.f64 d d (*.f64 c c))) |
(/.f64 (-.f64 (*.f64 b a) (*.f64 c d)) (+.f64 (*.f64 a a) (*.f64 d d))) |
(/.f64 (-.f64 (*.f64 b a) (*.f64 c d)) (fma.f64 a a (*.f64 d d))) |
(/.f64 (-.f64 (*.f64 b c) (*.f64 d a)) (+.f64 (*.f64 c c) (*.f64 a a))) |
(/.f64 (-.f64 (*.f64 b c) (*.f64 a d)) (fma.f64 c c (*.f64 a a))) |
(/.f64 (fma.f64 b c (*.f64 a (neg.f64 d))) (fma.f64 c c (*.f64 a a))) |
(/.f64 (-.f64 (*.f64 c b) (*.f64 a d)) (+.f64 (*.f64 b b) (*.f64 d d))) |
(/.f64 (-.f64 (*.f64 b c) (*.f64 a d)) (fma.f64 b b (*.f64 d d))) |
(/.f64 (fma.f64 b c (*.f64 a (neg.f64 d))) (fma.f64 b b (*.f64 d d))) |
(/.f64 (-.f64 (*.f64 d c) (*.f64 a b)) (+.f64 (*.f64 c c) (*.f64 b b))) |
(/.f64 (-.f64 (*.f64 c d) (*.f64 b a)) (fma.f64 c c (*.f64 b b))) |
(/.f64 (-.f64 (*.f64 c d) (*.f64 b a)) (fma.f64 b b (*.f64 c c))) |
(/.f64 (fma.f64 b (neg.f64 a) (*.f64 c d)) (fma.f64 b b (*.f64 c c))) |
(/.f64 (-.f64 (*.f64 b d) (*.f64 a c)) (+.f64 (*.f64 d d) (*.f64 c c))) |
(/.f64 (-.f64 (*.f64 b d) (*.f64 c a)) (fma.f64 c c (*.f64 d d))) |
(/.f64 (fma.f64 b d (*.f64 c (neg.f64 a))) (fma.f64 d d (*.f64 c c))) |
Compiled 19 to 11 computations (42.1% saved)
Compiled 4 to 4 computations (0% saved)
| Status | Accuracy | Program |
|---|---|---|
| 56.8% | (/.f64 (-.f64 (*.f64 b c) (*.f64 a d)) (+.f64 (*.f64 c c) (*.f64 d d))) |
Compiled 38 to 22 computations (42.1% saved)
| 1× | egg-herbie |
| 5× | *-commutative |
| 5× | +-commutative |
| 4× | sub-neg |
| 3× | neg-sub0 |
| 3× | neg-mul-1 |
Useful iterations: 0 (0.0ms)
| Iter | Nodes | Cost |
|---|---|---|
| 0 | 18 | 67 |
| 1 | 27 | 67 |
| 2 | 39 | 67 |
| 3 | 45 | 67 |
| 4 | 49 | 67 |
| 5 | 50 | 67 |
| 1× | saturated |
| Inputs |
|---|
(/.f64 (-.f64 (*.f64 b c) (*.f64 a d)) (+.f64 (*.f64 c c) (*.f64 d d))) |
| Outputs |
|---|
(/.f64 (-.f64 (*.f64 b c) (*.f64 a d)) (+.f64 (*.f64 c c) (*.f64 d d))) |
| 1× | fuel |
Compiled 19 to 11 computations (42.1% saved)
Compiled 158 to 86 computations (45.6% saved)
Loading profile data...