quad2m (problem 3.2.1, negative)

Time bar (total: 15.5s)

analyze218.0ms (1.4%)

Algorithm
search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
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
Compiler

Compiled 17 to 11 computations (35.3% saved)

sample15.0s (96.6%)

Results
1.1s5512×0valid
594.0ms5481×0valid-sollya
992.0ms1895×2valid
351.0ms1883×2valid-sollya
193.0ms1071×0invalid
126.0ms1063×0invalid-sollya
277.0ms849×1valid
115.0ms845×1valid-sollya
17.0ms39×0exit-sollya
7.0ms12×2exit-sollya
6.0ms1exit-sollya
Sollya Eval
PtRival-outSollya-intervalSollya-pointstatusSollya statusRival itersollya-timecheck
(1.4004090535574676e+218 -2.7961531644665123e+56 -2.1893658405521046e-136)-3.9149605042644747e-193(-1.5186739816150374e-181 1.5186739816150374e-181)+nan.0validexit10.213305#f
(-7.709970393151155e+190 -5.76154786308353e-238 -1.7132224088588195e-293)#f(+nan.0 +nan.0)+nan.0invalidexit00.078806#f
(-4.649778358802337e+237 -2.989921926225615e-73 1.759992900655097e-96)1.945536271989895e-167(1.945536271989895e-167 1.945536271989895e-167)+nan.0validexit00.27760799999999997#f
(-2.430465706166346e+212 -7.629217867654938e-302 2.7504999544676228e-160)1.0638026608376874e-186(1.0638026608376874e-186 1.0638026608376874e-186)+nan.0validexit00.25540799999999997#f
(-1.0176411558750572e-129 -2.75660516633602e-261 1.3495836101676619e+143)1.1516024135279914e+136(1.1516024135279914e+136 1.1516024135279914e+136)+nan.0validexit00.26664#f
(1.9829882632919127e-131 -2.9491560661626422e+245 -6.319115375883013e+232)-1.0713429934051042e-13(+nan.0 +nan.0)+nan.0validexit25.0#f
(-5.319039046616061e+137 -3.9838199819029903e+70 -3.280570545454748e+89)#f(+nan.0 +nan.0)+nan.0invalidexit00.13588#f
(-5.7926871953909756e-61 -1.0226228680262768e-214 2.3156011182262985e+99)6.322543654920511e+79(6.322543654920511e+79 6.322543654920511e+79)+nan.0validexit00.245655#f
(-1.3774825908059274e-271 1.2335468660073636e+122 2.622455121932084e+204)+inf.0(+inf.0 +inf.0)+nan.0validexit00.148015#f
(-1.702922276485511e-140 -6.518300076946018e-183 -9.058263134334583e-247)-6.9483324083006925e-65(+nan.0 +nan.0)+nan.0validexit15.0#f
(-7.395018471524956e+296 -6.700375810903034e+135 -4.0794872495782115e-93)-3.0442227157915222e-229(-8.525091608220254e-181 8.525091608220254e-181)+nan.0validexit10.24676800000000002#f
(-1.812245343932438e-299 -2.4311965052791786e+153 -5.215953866355621e+180)-1.0727133440323581e+27(-inf.0 +inf.0)+nan.0validexit20.22445#f
(-4.814311751413644e-128 8.96891732660477e+192 -9.038368025600914e-87)+inf.0(+inf.0 +inf.0)+nan.0validexit00.21314899999999998#f
(-4.5111279679621216e-290 3.052658538178195e-187 8.181445443628032e-226)1.3533903537465898e+103(1.3533903537465898e+103 1.3533903537465898e+103)+nan.0validexit00.25375400000000004#f
(1.3103875394358235e+229 2.2211574511827673e+250 -2.7672402046214166e+85)-3.3900771860804907e+21(-3.3900771860804907e+21 -3.3900771860804907e+21)+nan.0validexit00.089048#f
(5.439540244504849e+198 -3.654505836189021e-107 -1.4447225976195967e+143)-1.629713022288214e-28(-1.629713022288214e-28 -1.629713022288214e-28)+nan.0validexit00.130387#f
(-2.145744881540693e-45 -1.4355402753110357e+218 4.663649284864316e+70)1.624353341063124e-148(-4.45911885818294e+243 4.45911885818294e+243)+nan.0validexit20.20929999999999999#f
(5.2917276095223696e+191 -2.5201407654525892e+123 8.940200393919998e+134)#f(+nan.0 +nan.0)+nan.0invalidexit00.173274#f
(-8607452929552573.0 1.5346468526441697e+225 1.8963481527913335e+257)3.5658559278904884e+209(3.5658559278904884e+209 3.5658559278904884e+209)+nan.0validexit00.13997099999999998#f
(-2.016851217839339e+273 2.5883014004011455e+150 -5.641698465800005e-176)2.566675595608885e-123(2.566675595608885e-123 2.566675595608885e-123)+nan.0validexit00.268072#f
(7.644047792008348e+174 1.5439573908536998e+35 1.5531613816149328e+97)#f(+nan.0 +nan.0)+nan.0invalidexit05.0#f
(1.8241667802126902e-242 5.789119632440267e-113 -1.0599870018250295e-297)-6.347138534959265e+129(-6.347138534959265e+129 -6.347138534959265e+129)+nan.0validexit00.25563199999999997#f
(1.7364954571211263e+98 -7.917569251876326e+249 1.9098811620023391e+199)1.206103225146866e-51(-4.470262464361908e+132 4.470262464361908e+132)+nan.0validexit20.348036#f
(-6.186260852084322e+283 2.2043739894937902e+71 -1.474189406438593e-251)7.126676492314661e-213(7.126676492314661e-213 7.126676492314661e-213)+nan.0validexit00.169189#f
(-4.4315884949674477e+145 8.818132625976682e+256 -3.3395630333943625e+60)3.979671233459801e+111(3.979671233459801e+111 3.979671233459801e+111)+nan.0validexit00.12526099999999998#f
(1.6080757674656623e-260 -1.6814920044630702e+256 8.248340267867126e-120)0.0(-inf.0 +inf.0)+nan.0validexit20.141098#f
(6.081629986521083e+112 -4.039665620795972e+118 -9.443803092132282e+98)-1.168884256597392e-20(-7.192975335989488e-14 7.192975335989488e-14)+nan.0validexit10.21479299999999998#f
(-1.544064633772343e-172 9.00779871620336e-49 -3.3907919262595366e+193)#f(+nan.0 +nan.0)+nan.0invalidexit00.127021#f
(3.139562682068715e+84 -9.062090584421392e+300 -2.8613236655525337e-68)-0.0(-1.8501493319171156e+197 1.8501493319171156e+197)+nan.0validexit20.129837#f
(8.385622122565632e-257 8.32191257085842e-283 -2.397033053696697e-290)-1.6907109584687055e-17(-1.6907109584687055e-17 -1.6907109584687055e-17)+nan.0validexit00.207495#f
(-7.06460773407842e+267 -6.957183344489851e-164 2.9049461240857676e+302)202779951531115000.0(202779951531115000.0 202779951531115000.0)+nan.0validexit00.142449#f
(-3.8731181386348226e-249 -1.2129928120828435e-45 -2.8560101710220736e+299)#f(+nan.0 +nan.0)+nan.0invalidexit00.075219#f
(1.1326293093860148e-35 -4.0950843476739305e-97 -2.108642370153494e+204)-4.314769165596459e+119(-4.314769165596459e+119 -4.314769165596459e+119)+nan.0validexit00.230173#f
(8.01321522511516e-137 -794700749008315.5 -9.678716776393018e-262)-6.089535456252441e-277(-7.616812295107529e+131 7.616812295107529e+131)+nan.0validexit20.21575899999999998#f
(2.479606432226705e-167 9.725061398901106e+225 6.1323546807452586e+181)-inf.0(+nan.0 +nan.0)+nan.0validexit05.0#f
(-6.112439824732069e-267 -1.806431518056495e+255 2.1546182137421317e-113)0.0(-inf.0 +inf.0)+nan.0validexit20.29143#f
(-1.439316945500913e+292 5.548832708905767e-252 1.2474933349967738e-145)2.944020960696263e-219(2.944020960696263e-219 2.944020960696263e-219)+nan.0validexit00.210873#f
(-5.544085000643866e-225 -3.2462787170676513e-223 1.4291820326329584e+198)1.605568480519052e+211(1.605568480519052e+211 1.605568480519052e+211)+nan.0validexit00.13334800000000002#f
(-1.0463689812229607e+35 1.3387320273955345e+151 2.8172714361013063e-301)2.5588144362438377e+116(2.5588144362438377e+116 2.5588144362438377e+116)+nan.0validexit00.213312#f
(-1.1886354363132558e-91 1.4881237975865982e-101 -3.796561232843995e-154)2.503919624342101e-10(2.503919624342101e-10 2.503919624342101e-10)+nan.0validexit00.186298#f
(-1.3868435775565697e+94 -5.0863605452277695e+292 1.9567197942854563e-62)0.0(-3.120603411300607e+179 3.120603411300607e+179)+nan.0validexit20.134149#f
(-1.4130036974952945e-121 -4.254365666212363e+296 7.057759593884554e-140)0.0(-inf.0 +inf.0)+nan.0validexit20.140416#f
(1.016868943705101e-302 2.0293532091512264e-114 -1.1225193122195712e-76)-3.99137611924109e+188(-3.99137611924109e+188 -3.99137611924109e+188)+nan.0validexit00.124542#f
(3.8724430269193752e+233 4.272104448766786e+89 -1.3687461361409065e-148)-2.206413067445618e-144(-2.206413067445618e-144 -2.206413067445618e-144)+nan.0validexit00.225803#f
(1.2618497657083013e+229 1.5390323048813936e+290 -2.9865225871688998e+153)-2.439327322008899e+61(-2.439327322008899e+61 -2.439327322008899e+61)+nan.0validexit00.256641#f
(-41066034184539.59 3.985232794967856e+155 4.757885816485364e+184)1.9408900197468803e+142(1.9408900197468803e+142 1.9408900197468803e+142)+nan.0validexit00.191565#f
(-5.015712871298642e-269 6.990454639430953e+192 3.8597741943990097e+93)+inf.0(+inf.0 +inf.0)+nan.0validexit00.292197#f
(8.719991874621502e-51 2.417022165047079e-131 -6.991121784623799e+159)-8.953965024931596e+104(-8.953965024931596e+104 -8.953965024931596e+104)+nan.0validexit00.139615#f
(-4.6202873851613333e+23 1.834924955946769e+158 -3.9534871003900916e+177)7.942903992681816e+134(7.942903992681816e+134 7.942903992681816e+134)+nan.0validexit00.13503#f
(-1.4315978032118404e-48 -8.651197566634003e+251 -4.290539861185424e+290)-2.4797375323696265e+38(-3.4702888508324436e+280 3.4702888508324436e+280)+nan.0validexit20.140039#f
(-9.659637447044511e-304 -2.632357078135985e-247 -2.5306675503603124e+101)#f(+nan.0 +nan.0)+nan.0invalidexit00.13609900000000003#f
(-4.606934259643825e-181 1.547629945907391e-32 -8.115953899732527e-69)6.718697765950073e+148(6.718697765950073e+148 6.718697765950073e+148)+nan.0validexit00.253115#f
(-4.052806986325048e+291 -1.1541033628450447e-271 1.3560160932300543e-155)5.784348640517531e-224(5.784348640517531e-224 5.784348640517531e-224)+nan.0validexit00.25690799999999997#f
(-1.2017225610058615e-220 -2.804132840909948e+137 -5.2302661574316785e+230)-9.3259956895167e+92(-inf.0 +inf.0)+nan.0validexit20.257537#f
(1.1064428589186171e+133 -28012.894800398557 2.1755062440524935e+34)#f(+nan.0 +nan.0)+nan.0invalidexit00.157367#f
Sollya timings
Total time spent in Sollya 1.2s
Bogosity

preprocess255.0ms (1.6%)

Algorithm
egg-herbie
Rules
939×fma-neg
770×fma-define
418×times-frac
370×div-sub
193×associate-/r*
Iterations

Useful iterations: 2 (0.0ms)

IterNodesCost
055631
1168615
2395595
31218595
43047595
54634595
64940595
75075595
85287595
95287595
105287595
Stop Event
saturated
Calls
Call 1
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 (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 b_2) (sqrt.f64 (+.f64 (*.f64 b_2 b_2) (*.f64 a c)))) (neg.f64 a))
(/.f64 (-.f64 (neg.f64 b_2) (sqrt.f64 (fma.f64 b_2 b_2 (*.f64 a c)))) (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 (neg.f64 b_2) (sqrt.f64 (fma.f64 b_2 b_2 (*.f64 a 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)))
(/.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 (fma.f64 b_2 b_2 (*.f64 a c)))) 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))
(/.f64 (-.f64 (sqrt.f64 (-.f64 (*.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 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 (neg.f64 b_2) (sqrt.f64 (fma.f64 b_2 b_2 (*.f64 a c)))) (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 (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 (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 (neg.f64 c) (sqrt.f64 (fma.f64 c c (*.f64 (neg.f64 b_2) a)))) a)
(/.f64 (-.f64 (neg.f64 c) (sqrt.f64 (fma.f64 (neg.f64 b_2) a (*.f64 c c)))) a)
Compiler

Compiled 16 to 10 computations (37.5% saved)

eval0.0ms (0%)

Compiler

Compiled 3 to 3 computations (0% saved)

prune2.0ms (0%)

Alt Table
Click to see full alt table
StatusAccuracyProgram
56.5%
(/.f64 (-.f64 (neg.f64 b_2) (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)))) a)
Compiler

Compiled 32 to 20 computations (37.5% saved)

simplify4.0ms (0%)

Algorithm
egg-herbie
Rules
10×+-commutative
sub-neg
*-commutative
neg-sub0
neg-mul-1
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
01757
12957
24657
36257
47257
57657
67757
Stop Event
saturated
Calls
Call 1
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)

soundness0.0ms (0%)

Stop Event
fuel
Compiler

Compiled 16 to 10 computations (37.5% saved)

preprocess52.0ms (0.3%)

Compiler

Compiled 248 to 92 computations (62.9% saved)

end0.0ms (0%)

Profiling

Loading profile data...