Cubic critical

Time bar (total: 28.6s)

analyze314.0ms (1.1%)

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
40%37.4%56.2%0.1%0%6.2%0%7
48.3%45.2%48.4%0.1%0%6.2%0%8
53%48.4%42.9%0.1%0%8.6%0%9
58.1%50.3%36.3%0.1%0%13.3%0%10
66.1%56.8%29.1%0.1%0%14%0%11
70.4%58.8%24.7%0.1%0%16.4%0%12
Compiler

Compiled 21 to 13 computations (38.1% saved)

sample27.9s (97.6%)

Results
1.6s5552×0valid
663.0ms5528×0valid-sollya
1.4s1889×2valid
395.0ms1877×2valid-sollya
353.0ms924×0invalid
130.0ms920×0invalid-sollya
458.0ms815×1valid
123.0ms813×1valid-sollya
20.0ms28×0exit-sollya
12.0ms12×2exit-sollya
0.0ms1exit-sollya
Sollya Eval
PtRival-outSollya-intervalSollya-pointstatusSollya statusRival itersollya-timecheck
(6.653849041368586e-206 5.733654907979761e-212 2.2049690032704014e-83)#f(+nan.0 +nan.0)+nan.0invalidexit00.083096#f
(1.327049380630265e+276 -9.452949796348809e-117 -3.5195143674079313e-239)2.9732895333003036e-258(+nan.0 +nan.0)+nan.0validexit05.0#f
(-4.879606929079606e-37 -1.125925138116494e-165 2.689407998278361e-225)-4.286228296270256e-95(-4.286228296270256e-95 -4.286228296270256e-95)+nan.0validexit00.14902200000000002#f
(-6.6406178933504516e-242 -8.625769599355768e+244 4.818732734805398e-254)-inf.0(-inf.0 -inf.0)+nan.0validexit00.34312600000000004#f
(3.3381409788559216e-146 -2.8526041263359687e-100 4.3937470887093584e-126)5.696991517942899e+45(5.696991517942899e+45 5.696991517942899e+45)+nan.0validexit00.126005#f
(5.4847229503459765e-195 5.101479293448712e+263 -1.6171787646853227e+243)1.5850096331490493e-21(-inf.0 +inf.0)+nan.0validexit20.276049#f
(-3.2536018980367928e-192 -1.8786647900535035e+64 3.099246322924298e+103)-3.849405159631608e+255(-3.849405159631608e+255 -3.849405159631608e+255)+nan.0validexit00.147306#f
(-44814772.86528375 7.2965461375633e+132 -2.2519822583604054e+63)1.5431837309758042e-70(-4.579266370261197e+105 4.579266370261197e+105)+nan.0validexit20.283337#f
(2.0467367944481134e-26 4.290727661996141e+212 3.494252788377854e-69)-4.0718650350698914e-282(-5.9443443566664325e+218 5.9443443566664325e+218)+nan.0validexit20.139562#f
(-2.7566349834867688e-121 -7.552403095922946e-118 3.2353822379736143e-88)-19779373863274960.0(-19779373863274960.0 -19779373863274960.0)+nan.0validexit00.209573#f
(1.0291600800961193e+239 -9.734431115548515e-6 -2.219105942087747e-160)2.6809389522301973e-200(2.6809389522301973e-200 2.6809389522301973e-200)+nan.0validexit00.29722800000000005#f
(-5.177874486114342e+208 -2.909788396201425e-29 -1.6588649174397785e-277)-3.746438690216163e-238(-3.746438690216163e-238 -3.746438690216163e-238)+nan.0validexit00.245551#f
(-3.6560860738996825e+235 -7.05206268633625e+89 1.2560236327341208e+193)-3.3839978022080672e-22(+nan.0 +nan.0)+nan.0validexit05.0#f
(-9.685195206270882e-248 1.5917998786249962e+282 -6.399124533023035e+302)2.010027962356244e+20(-inf.0 +inf.0)+nan.0validexit20.16444499999999998#f
(3.566241976874573e+123 -3.2939921046481384e+20 -4.2230439671563723e-125)6.157727800502884e-104(6.157727800502884e-104 6.157727800502884e-104)+nan.0validexit00.257764#f
(-1.0616033474989007e-78 1.8579189845338514e+276 -287112157.9571646)7.726713606653859e-269(-inf.0 +inf.0)+nan.0validexit20.225012#f
(6.417528517650281e-11 -2.1068134244307956e+261 1.9316321998639036e-189)2.1886031033456538e+271(2.1886031033456538e+271 2.1886031033456538e+271)+nan.0validexit00.13552799999999998#f
(-2.900390809400193e+77 3.7906631045608966e+123 5.1441542195586676e-83)-6.785295972846098e-207(-6.589625234171954e+26 3.294812617085977e+26)+nan.0validexit20.163711#f
(-8.008979830681571e-138 -8.282138433535338e+58 -1.3292165346853637e-144)-6.894043609905076e+195(-6.894043609905076e+195 -6.894043609905076e+195)+nan.0validexit00.146725#f
(7.407314676701611e-13 -4.286881694461534e+271 3.1714298324066946e+92)3.858241824976201e+283(3.858241824976201e+283 3.858241824976201e+283)+nan.0validexit00.301413#f
(1.4218982369658039e-47 1.2874713124942662e+270 8.840772841495276e-15)-3.433386342553807e-285(+nan.0 +nan.0)+nan.0validexit25.0#f
(7.488043188534605e-293 3.9887546920636355e+207 -2.3308330484696294e-128)0.0(-inf.0 +inf.0)+nan.0validexit20.154635#f
(-1.974386245319551e-59 2.3040774196652177e+222 -1.300184014202643e-88)2.821485083586e-311(-2.6466328681914506e+261 2.6466328681914506e+261)+nan.0validexit20.141967#f
(5.54498734578741e-209 6.447832993291182e-205 2.6112656546258898e-51)#f(+nan.0 +nan.0)+nan.0invalidexit00.16082800000000003#f
(1.433221512346336e-280 4.6588121566251055e-169 3.4236913608116667e+89)#f(+nan.0 +nan.0)+nan.0invalidexit00.201096#f
(-6.72448741518192e-216 8.919231313339832e-207 -4.7625030275665346e-169)#f(+nan.0 +nan.0)+nan.0invalidexit00.14098100000000002#f
(2.83707837127099e+226 1.1332030568568987e+253 -7.866687415304478e-165)0.0(+nan.0 +nan.0)+nan.0validexit25.0#f
(-7.559778967928098e-245 -5.179416585119241e-55 -3.7445009601571565e-27)-4.567520300168034e+189(-4.567520300168034e+189 -4.567520300168034e+189)+nan.0validexit00.27486299999999997#f
(3.8764969197181527e-112 -4.826943929306398e-11 -3.109904753826866e+93)1.6773167526935565e+102(1.6773167526935565e+102 1.6773167526935565e+102)+nan.0validexit00.133843#f
(1.4683963484256556e-117 5.0183556409221863e+160 -2.851228133583716e+59)2.840799195590457e-102(-6.920435280607324e+257 6.920435280607324e+257)+nan.0validexit20.23793#f
(-6.161274369114447e-232 -4.9070217297215094e-242 6.926055830966945e-177)-1.9357403024216594e+27(-1.9357403024216594e+27 -1.9357403024216594e+27)+nan.0validexit00.079059#f
(-1.2037322193875425e-210 -6.251800647752252e+93 6.1069023374619625e-164)-3.4624537180055773e+303(-3.4624537180055773e+303 -3.4624537180055773e+303)+nan.0validexit00.147062#f
(-3.7974331450377905e+87 -1.0260347347325374e-220 2.8831004888715906e-219)-5.030651056086339e-154(+nan.0 +nan.0)+nan.0validexit05.0#f
(1.341340394860305e-264 -6.835334173650184e+66 -4.899600134918814e-108)+inf.0(+inf.0 +inf.0)+nan.0validexit00.29582#f
(1.1172552528563529e-203 1.0190831585379965e+267 -5.987754540956159e+161)2.9378144907950146e-106(-inf.0 +inf.0)+nan.0validexit20.161492#f
(-1.0002350655144411e+263 9.515521735598286e+135 8.886094342950876e-231)-0.0(-4.2018929408229837e-147 2.1009464704114918e-147)+nan.0validexit10.244088#f
(3.375231406763222e-80 1.5638720421033235e-232 -9.813408983587513e+269)3.1131320695762265e+174(3.1131320695762265e+174 3.1131320695762265e+174)+nan.0validexit00.28971399999999997#f
(-4.066485941736162e-15 -4.1829265821709114e-48 3.10555735691488e-83)-6.894484466928222e-34(-6.894484466928222e-34 -6.894484466928222e-34)+nan.0validexit00.282743#f
(-5.273172609735464e-137 1.5873255986872742e-97 246.12756128500268)-1.2473361327682759e+69(-1.2473361327682759e+69 -1.2473361327682759e+69)+nan.0validexit00.272964#f
(-1.2058215276862443e-41 -7.951897868590247e+262 1.1560369370375886e-216)-4.39639293544461e+303(-4.39639293544461e+303 -4.39639293544461e+303)+nan.0validexit00.232262#f
(5.7017209927837276e-61 3.032684277731472e+188 5.786016000701464e+299)-9.539430205754153e+110(-1.7650635329686053e+229 1.7650635329686053e+229)+nan.0validexit10.148547#f
(9.446928769156396e+170 -6.683930965533156e-238 -6.393255207046222e-269)1.5019486082095912e-220(1.5019486082095912e-220 1.5019486082095912e-220)+nan.0validexit00.148242#f
Sollya timings
Total time spent in Sollya 1.3s
Bogosity

preprocess258.0ms (0.9%)

Algorithm
egg-herbie
Rules
838×div-sub
712×fma-neg
592×fma-define
501×sub-neg
393×associate-/r*
Iterations

Useful iterations: 1 (0.0ms)

IterNodesCost
060779
1176671
2482671
31308671
43657671
57636671
Stop Event
node limit
Calls
Call 1
Inputs
(/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 #s(literal 3 binary64) a) c)))) (*.f64 #s(literal 3 binary64) a))
(/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 #s(literal 3 binary64) a) c)))) (*.f64 #s(literal 3 binary64) a))
(/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 #s(literal 3 binary64) (neg.f64 a)) c)))) (*.f64 #s(literal 3 binary64) (neg.f64 a)))
(/.f64 (+.f64 (neg.f64 (neg.f64 b)) (sqrt.f64 (-.f64 (*.f64 (neg.f64 b) (neg.f64 b)) (*.f64 (*.f64 #s(literal 3 binary64) a) c)))) (*.f64 #s(literal 3 binary64) a))
(/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 #s(literal 3 binary64) a) (neg.f64 c))))) (*.f64 #s(literal 3 binary64) a))
(neg.f64 (/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 #s(literal 3 binary64) (neg.f64 a)) c)))) (*.f64 #s(literal 3 binary64) (neg.f64 a))))
(neg.f64 (/.f64 (+.f64 (neg.f64 (neg.f64 b)) (sqrt.f64 (-.f64 (*.f64 (neg.f64 b) (neg.f64 b)) (*.f64 (*.f64 #s(literal 3 binary64) a) c)))) (*.f64 #s(literal 3 binary64) a)))
(neg.f64 (/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 #s(literal 3 binary64) a) (neg.f64 c))))) (*.f64 #s(literal 3 binary64) a)))
(/.f64 (+.f64 (neg.f64 a) (sqrt.f64 (-.f64 (*.f64 a a) (*.f64 (*.f64 #s(literal 3 binary64) b) c)))) (*.f64 #s(literal 3 binary64) b))
(/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 #s(literal 3 binary64) c) a)))) (*.f64 #s(literal 3 binary64) c))
(/.f64 (+.f64 (neg.f64 c) (sqrt.f64 (-.f64 (*.f64 c c) (*.f64 (*.f64 #s(literal 3 binary64) a) b)))) (*.f64 #s(literal 3 binary64) a))
Outputs
(/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 #s(literal 3 binary64) a) c)))) (*.f64 #s(literal 3 binary64) a))
(/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 #s(literal 3 binary64) (*.f64 a c))))) (*.f64 #s(literal 3 binary64) a))
(/.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c #s(literal -3 binary64))))) b) (*.f64 #s(literal 3 binary64) a))
(/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 #s(literal 3 binary64) a) c)))) (*.f64 #s(literal 3 binary64) a))
(/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 #s(literal 3 binary64) (*.f64 a c))))) (*.f64 #s(literal 3 binary64) a))
(/.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c #s(literal -3 binary64))))) b) (*.f64 #s(literal 3 binary64) a))
(/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 #s(literal 3 binary64) (neg.f64 a)) c)))) (*.f64 #s(literal 3 binary64) (neg.f64 a)))
(/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 #s(literal 3 binary64) (*.f64 (neg.f64 a) c))))) (*.f64 #s(literal 3 binary64) (neg.f64 a)))
(/.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 #s(literal 3 binary64) (*.f64 a c)))) b) (*.f64 a #s(literal -3 binary64)))
(*.f64 #s(literal -1/3 binary64) (/.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 #s(literal 3 binary64) c)))) b) a))
(*.f64 (/.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 #s(literal 3 binary64) c)))) b) a) #s(literal -1/3 binary64))
(/.f64 (+.f64 (neg.f64 (neg.f64 b)) (sqrt.f64 (-.f64 (*.f64 (neg.f64 b) (neg.f64 b)) (*.f64 (*.f64 #s(literal 3 binary64) a) c)))) (*.f64 #s(literal 3 binary64) a))
(/.f64 (+.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 #s(literal 3 binary64) (*.f64 a c))))) (*.f64 #s(literal 3 binary64) a))
(/.f64 (+.f64 b (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c #s(literal -3 binary64)))))) (*.f64 #s(literal 3 binary64) a))
(/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 #s(literal 3 binary64) a) (neg.f64 c))))) (*.f64 #s(literal 3 binary64) a))
(/.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 #s(literal 3 binary64) (*.f64 a c)))) b) (*.f64 #s(literal 3 binary64) a))
(*.f64 #s(literal 1/3 binary64) (/.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 #s(literal 3 binary64) c)))) b) a))
(*.f64 (/.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 #s(literal 3 binary64) c)))) b) a) #s(literal 1/3 binary64))
(neg.f64 (/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 #s(literal 3 binary64) (neg.f64 a)) c)))) (*.f64 #s(literal 3 binary64) (neg.f64 a))))
(/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 #s(literal 3 binary64) a) (neg.f64 c))))) (*.f64 #s(literal 3 binary64) a))
(/.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 #s(literal 3 binary64) (*.f64 a c)))) b) (*.f64 #s(literal 3 binary64) a))
(*.f64 #s(literal 1/3 binary64) (/.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 #s(literal 3 binary64) c)))) b) a))
(*.f64 (/.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 #s(literal 3 binary64) c)))) b) a) #s(literal 1/3 binary64))
(neg.f64 (/.f64 (+.f64 (neg.f64 (neg.f64 b)) (sqrt.f64 (-.f64 (*.f64 (neg.f64 b) (neg.f64 b)) (*.f64 (*.f64 #s(literal 3 binary64) a) c)))) (*.f64 #s(literal 3 binary64) a)))
(/.f64 (+.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 #s(literal 3 binary64) (*.f64 a c))))) (*.f64 #s(literal 3 binary64) (neg.f64 a)))
(/.f64 (+.f64 b (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c #s(literal -3 binary64)))))) (*.f64 a #s(literal -3 binary64)))
(neg.f64 (/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 #s(literal 3 binary64) a) (neg.f64 c))))) (*.f64 #s(literal 3 binary64) a)))
(/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 #s(literal 3 binary64) (*.f64 (neg.f64 a) c))))) (*.f64 #s(literal 3 binary64) (neg.f64 a)))
(/.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 #s(literal 3 binary64) (*.f64 a c)))) b) (*.f64 a #s(literal -3 binary64)))
(*.f64 #s(literal -1/3 binary64) (/.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 #s(literal 3 binary64) c)))) b) a))
(*.f64 (/.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 #s(literal 3 binary64) c)))) b) a) #s(literal -1/3 binary64))
(/.f64 (+.f64 (neg.f64 a) (sqrt.f64 (-.f64 (*.f64 a a) (*.f64 (*.f64 #s(literal 3 binary64) b) c)))) (*.f64 #s(literal 3 binary64) b))
(/.f64 (+.f64 (neg.f64 a) (sqrt.f64 (-.f64 (*.f64 a a) (*.f64 #s(literal 3 binary64) (*.f64 b c))))) (*.f64 b #s(literal 3 binary64)))
(/.f64 (-.f64 (sqrt.f64 (fma.f64 a a (*.f64 c (*.f64 b #s(literal -3 binary64))))) a) (*.f64 b #s(literal 3 binary64)))
(/.f64 (-.f64 (sqrt.f64 (fma.f64 a a (*.f64 b (*.f64 c #s(literal -3 binary64))))) a) (*.f64 b #s(literal 3 binary64)))
(/.f64 (-.f64 (sqrt.f64 (fma.f64 b (*.f64 c #s(literal -3 binary64)) (*.f64 a a))) a) (*.f64 b #s(literal 3 binary64)))
(/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 #s(literal 3 binary64) c) a)))) (*.f64 #s(literal 3 binary64) c))
(/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 #s(literal 3 binary64) (*.f64 c a))))) (*.f64 #s(literal 3 binary64) c))
(/.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c #s(literal -3 binary64))))) b) (*.f64 #s(literal 3 binary64) c))
(/.f64 (+.f64 (neg.f64 c) (sqrt.f64 (-.f64 (*.f64 c c) (*.f64 (*.f64 #s(literal 3 binary64) a) b)))) (*.f64 #s(literal 3 binary64) a))
(/.f64 (+.f64 (neg.f64 c) (sqrt.f64 (-.f64 (*.f64 c c) (*.f64 b (*.f64 #s(literal 3 binary64) a))))) (*.f64 #s(literal 3 binary64) a))
(/.f64 (-.f64 (sqrt.f64 (fma.f64 c c (*.f64 b (*.f64 a #s(literal -3 binary64))))) c) (*.f64 #s(literal 3 binary64) a))
(/.f64 (-.f64 (sqrt.f64 (fma.f64 b (*.f64 a #s(literal -3 binary64)) (*.f64 c c))) c) (*.f64 #s(literal 3 binary64) a))
(/.f64 (-.f64 c (sqrt.f64 (fma.f64 b (*.f64 a #s(literal -3 binary64)) (*.f64 c c)))) (*.f64 a #s(literal -3 binary64)))
Compiler

Compiled 20 to 12 computations (40% saved)

eval0.0ms (0%)

Compiler

Compiled 3 to 3 computations (0% saved)

prune3.0ms (0%)

Alt Table
Click to see full alt table
StatusAccuracyProgram
53.9%
(/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 #s(literal 3 binary64) a) c)))) (*.f64 #s(literal 3 binary64) a))
Compiler

Compiled 40 to 24 computations (40% saved)

simplify19.0ms (0.1%)

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

Useful iterations: 1 (0.0ms)

IterNodesCost
01969
13165
25065
36165
46965
57265
Stop Event
saturated
Calls
Call 1
Inputs
(/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 #s(literal 3 binary64) a) c)))) (*.f64 #s(literal 3 binary64) a))
Outputs
(/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 #s(literal 3 binary64) a) c)))) (*.f64 #s(literal 3 binary64) a))
(/.f64 (-.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 #s(literal 3 binary64) a) c))) b) (*.f64 #s(literal 3 binary64) a))

soundness1.0ms (0%)

Stop Event
fuel
Compiler

Compiled 19 to 11 computations (42.1% saved)

preprocess102.0ms (0.4%)

Compiler

Compiled 78 to 46 computations (41% saved)

end0.0ms (0%)

Profiling

Loading profile data...