2cos (problem 3.3.5)

Time bar (total: 25.0s)

analyze97.0ms (0.4%)

Algorithm
search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%50.6%49.4%0%0%0%0
0%0%50.6%49.4%0%0%0%1
0%0%50.6%49.4%0%0%0%2
0%0%25.3%74.7%0%0%0%3
0%0%25.3%74.7%0%0%0%4
0%0%19%81%0%0%0%5
0%0%15.8%84.2%0%0%0%6
0%0%11.1%88.9%0%0%0%7
0%0%8.7%91.3%0%0%0%8
0%0%5.9%94.1%0%0%0%9
0%0%4.5%95.5%0%0%0%10
0%0%3.1%96.9%0%0%0%11
0%0%2.7%97.3%0%0%0%12
Compiler

Compiled 28 to 18 computations (35.7% saved)

sample24.7s (98.8%)

Results
5.5s25998×0precondition
4.6s5661×2valid
744.0ms5604×2valid-sollya
916.0ms2514×1valid
270.0ms2504×1valid-sollya
7.0ms81×0valid-sollya
31.0ms81×0valid
27.0ms57×2exit-sollya
1.0ms10×1exit-sollya
Sollya Eval
PtRival-outSollya-intervalSollya-pointstatusSollya statusRival itersollya-timecheck
(4.8883862174861266e-96 2.4590997270038543e-109)-1.202102921290984e-204(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.094071#f
(4.4560381427019545e-61 6.036105496026396e-76)-2.6897116323666542e-136(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit10.094529#f
(3.0635444873708954e-288 4.2683995693008867e-293)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.094308#f
(-3.021831686279984e-77 2.7720025786280728e-77)4.5345260785877904e-154(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit10.09429#f
(-1.3634242766788605e-56 7.359305525910907e-61)1.00335850166347e-116(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit10.093571#f
(1.2694309224555467e-261 5.132672487895899e-270)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.09647299999999999#f
(-2.980061431047342e-235 4.818631278431528e-239)0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.096139#f
(1.798283640567314e-171 1.6236296177146858e-177)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.093289#f
(7.492534652210252e-285 2.038468836536141e-290)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.095364#f
(-6.459716721784773e-157 3.567728965417373e-159)2.2982875e-315(+nan.0 +nan.0)+nan.0validexit25.0#f
(-1.0744461544947203e-302 1.2616261440493847e-307)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.09675600000000001#f
(-1.135333570276281e-126 1.664412093469216e-129)1.8882777906809809e-255(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.094888#f
(1.44711926722329e-205 6.170491286230579e-211)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.093432#f
(3.2354831047609225e-300 1.7521235159414864e-306)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.095283#f
(-8.75652893318579e-89 1.2007105513927463e-91)1.0506848154510918e-179(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit10.09594899999999999#f
(5.5431554590209675e-285 1.5309409666463991e-293)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.095302#f
(-2.0380949923125828e-209 1.055772481306959e-223)0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.096017#f
(3.4389237662186965e-131 1.6498976314303296e-140)-5.673872177914777e-271(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.094638#f
(1.7758830760734058e-292 1.0371828279450969e-292)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.095074#f
(1.9961097524198373e-240 6.534304716205227e-246)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.17567400000000002#f
(4.525211857461731e-187 6.470236974277802e-195)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.197014#f
(-2.5124814935029822e-285 1.2884291926929991e-288)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.159074#f
(2.1114748168509356e-32 8.122571690511304e-43)-1.715060557291083e-74(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit10.156628#f
(2.9021824130461115e-195 3.686721716231093e-198)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.09736500000000001#f
(-1.4071690894951866e-272 4.4762056915604996e-277)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.097#f
(-7.550033565496144e-305 1.125536794602187e-306)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.19050999999999998#f
(-6.855410996383827e-222 4.530724864349292e-236)0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.163449#f
(-4.4724937383468976e-111 1.9569468538218723e-111)6.837612055654324e-222(+nan.0 +nan.0)+nan.0validexit25.0#f
(8.654868751926237e-292 2.3905924868816436e-295)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.097166#f
(-1.5999713224089508e-91 3.985689069711551e-103)6.376988211569349e-194(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.11333#f
(-4.61548471710057e-267 2.858990020315193e-281)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.17612899999999998#f
(-3.3004765732769933e-202 2.3969684060672808e-214)0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.18129499999999998#f
(-8.756933140499357e-110 5.310243761134236e-115)4.650130858256233e-224(+nan.0 +nan.0)+nan.0validexit25.0#f
(-4.1442049786604e-36 3.478518351552731e-49)1.441569307086579e-84(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit10.095058#f
(3.55219197787639e-199 1.0867983098028339e-213)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.147155#f
(5.054367213264704e-119 1.1870853456366272e-134)-5.999965250332768e-253(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.147615#f
(-6.504229657669281e-242 3.2037615352371146e-257)0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.185846#f
(-1.943099042810529e-238 5.254018226298867e-242)0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.154197#f
(-3.9503522909026106e-255 3.0262816996038224e-260)0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.15898#f
(-1.2202559076814599e-154 2.5928748374033814e-157)3.160609338259e-311(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.191363#f
(8.275744777677632e-114 2.313054731243408e-126)-1.9142250612572847e-239(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.09810300000000001#f
(5.870177628937895e-220 5.397813071150497e-233)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.096034#f
(-7.294384042733576e-62 3.6288482635283614e-63)2.5811785880997084e-124(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit10.17508700000000002#f
(-7.033580833405284e-260 2.644582500894003e-272)0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.207531#f
(7.800322376077262e-294 5.718366069294957e-307)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.208804#f
(1.6973392691285513e-137 4.464338389608853e-152)-7.577496859361234e-289(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.192853#f
(1.374564097029941e-272 1.2222139059888868e-287)-0.0(+nan.0 +nan.0)+nan.0validexit25.0#f
(1.3483427131761639e-276 6.629130991122738e-288)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.159895#f
(2.797534148609935e-286 4.201664042482271e-299)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.200966#f
(4.902955113235831e-298 3.5151922953325185e-306)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.097666#f
(-4.249504632744749e-271 5.308749783868451e-281)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.098927#f
(-4.72488594729948e-300 4.070225865751039e-306)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.09951700000000001#f
(3.1648944763555614e-232 6.8486205849313275e-242)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.16532799999999997#f
(-9.1681519861061e-45 4.3739152034740197e-47)4.00050636887541e-91(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit10.185818#f
(-3.3464810464278154e-157 4.265394196830109e-164)1.4274e-320(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.197512#f
(-7.997015011769462e-187 3.906890833490271e-194)0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.163432#f
(-1.550111057503159e-292 2.0583053204380546e-305)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.208839#f
(1.2599277981749111e-160 6.644150965566698e-166)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.15181#f
(1.0016512705820012e-110 4.340756857781715e-112)-4.4421354723764847e-222(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.09754199999999999#f
(1.7079921347313197e-222 2.244266188443572e-238)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.162995#f
(-8.498671877063067e-126 3.3637665013013387e-136)2.858754776505077e-261(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.099675#f
(8.576042795300948e-73 1.5525347121785556e-82)-1.3314604134038714e-154(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit10.179691#f
(-3.9064141353912488e-149 4.9618276435982404e-154)1.9382830545659394e-302(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.152917#f
(-1.7788792409661228e-26 1.3809841286773262e-33)2.456603903251926e-59(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit10.14435199999999998#f
(-3.6590716329501766e-286 1.2175972188400772e-291)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.162879#f
(8.931977604457146e-229 5.366137273468033e-240)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.097887#f
(-1.4669340637861986e-258 2.0556548276593103e-274)0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.172977#f
Sollya timings
Total time spent in Sollya 1.0s
Bogosity

preprocess130.0ms (0.5%)

Algorithm
egg-herbie
Rules
158×fma-neg
91×fma-define
54×sub-neg
41×associate--r+
36×cancel-sign-sub-inv
Iterations

Useful iterations: 2 (0.0ms)

IterNodesCost
027234
149218
296210
3184210
4349210
5486210
6636210
7761210
8795210
9821210
10827210
Stop Event
saturated
Calls
Call 1
Inputs
(-.f64 (cos.f64 (+.f64 x eps)) (cos.f64 x))
(-.f64 (cos.f64 (+.f64 x eps)) (cos.f64 x))
(-.f64 (cos.f64 (+.f64 (neg.f64 x) eps)) (cos.f64 (neg.f64 x)))
(-.f64 (cos.f64 (+.f64 x (neg.f64 eps))) (cos.f64 x))
(neg.f64 (-.f64 (cos.f64 (+.f64 (neg.f64 x) eps)) (cos.f64 (neg.f64 x))))
(neg.f64 (-.f64 (cos.f64 (+.f64 x (neg.f64 eps))) (cos.f64 x)))
(-.f64 (cos.f64 (+.f64 eps x)) (cos.f64 eps))
Outputs
(-.f64 (cos.f64 (+.f64 x eps)) (cos.f64 x))
(-.f64 (cos.f64 (+.f64 x eps)) (cos.f64 x))
(-.f64 (cos.f64 (+.f64 (neg.f64 x) eps)) (cos.f64 (neg.f64 x)))
(-.f64 (cos.f64 (+.f64 eps (neg.f64 x))) (cos.f64 x))
(-.f64 (cos.f64 (-.f64 eps x)) (cos.f64 x))
(-.f64 (cos.f64 (+.f64 x (neg.f64 eps))) (cos.f64 x))
(-.f64 (cos.f64 (+.f64 eps (neg.f64 x))) (cos.f64 x))
(-.f64 (cos.f64 (-.f64 eps x)) (cos.f64 x))
(neg.f64 (-.f64 (cos.f64 (+.f64 (neg.f64 x) eps)) (cos.f64 (neg.f64 x))))
(neg.f64 (-.f64 (cos.f64 (+.f64 eps (neg.f64 x))) (cos.f64 x)))
(neg.f64 (-.f64 (cos.f64 (-.f64 eps x)) (cos.f64 x)))
(-.f64 (cos.f64 x) (cos.f64 (-.f64 eps x)))
(neg.f64 (-.f64 (cos.f64 (+.f64 x (neg.f64 eps))) (cos.f64 x)))
(neg.f64 (-.f64 (cos.f64 (+.f64 eps (neg.f64 x))) (cos.f64 x)))
(neg.f64 (-.f64 (cos.f64 (-.f64 eps x)) (cos.f64 x)))
(-.f64 (cos.f64 x) (cos.f64 (-.f64 eps x)))
(-.f64 (cos.f64 (+.f64 eps x)) (cos.f64 eps))
(-.f64 (cos.f64 (+.f64 x eps)) (cos.f64 eps))
Compiler

Compiled 9 to 6 computations (33.3% saved)

eval0.0ms (0%)

Compiler

Compiled 2 to 2 computations (0% saved)

prune1.0ms (0%)

Alt Table
Click to see full alt table
StatusAccuracyProgram
53.3%
(-.f64 (cos.f64 (+.f64 x eps)) (cos.f64 x))
Compiler

Compiled 18 to 12 computations (33.3% saved)

simplify10.0ms (0%)

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

Useful iterations: 0 (0.0ms)

IterNodesCost
01230
11530
22030
32230
42330
Stop Event
saturated
Calls
Call 1
Inputs
(-.f64 (cos.f64 (+.f64 x eps)) (cos.f64 x))
Outputs
(-.f64 (cos.f64 (+.f64 x eps)) (cos.f64 x))

soundness1.0ms (0%)

Stop Event
fuel
Compiler

Compiled 9 to 6 computations (33.3% saved)

preprocess55.0ms (0.2%)

Compiler

Compiled 66 to 44 computations (33.3% saved)

end0.0ms (0%)

Profiling

Loading profile data...