ENA, Section 1.4, Mentioned, A

Time bar (total: 35.1s)

analyze4.0ms (0%)

Algorithm
search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%49.6%50.4%0%0%0%0
0%0%49.6%50.4%0%0%0%1
0%0%49.6%50.4%0%0%0%2
50%24.8%24.8%50.4%0%0%0%3
75%37.2%12.4%50.4%0%0%0%4
87.5%43.4%6.2%50.4%0%0%0%5
93.8%46.5%3.1%50.4%0%0%0%6
96.9%48.1%1.6%50.4%0%0%0%7
98.4%48.8%0.8%50.4%0%0%0%8
99.2%49.2%0.4%50.4%0%0%0%9
99.6%49.4%0.2%50.4%0%0%0%10
99.8%49.5%0.1%50.4%0%0%0%11
99.9%49.6%0%50.4%0%0%0%12
Compiler

Compiled 12 to 9 computations (25% saved)

sample34.6s (98.6%)

Results
8.4s8225×1valid
1.0s8094×1valid-sollya
22.0ms131×1exit-sollya
45.0ms31×0valid
3.0ms31×0valid-sollya
Sollya Eval
PtRival-outSollya-intervalSollya-pointstatusSollya statusRival itersollya-timecheck
(-1.6744436158951103e-178)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.13466699999999998#f
(1.0861126026749965e-168)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.137399#f
(1.2364919835900938e-276)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.150918#f
(1.8583123741477365e-206)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.146321#f
(1.1857326614307978e-108)7.0298097219188145e-217(0.0 5.421010862427522e-20)+nan.0validexit10.083867#f
(8.889647154593259e-15)3.951291326658401e-29(0.0 5.421010862427522e-20)+nan.0validexit10.074194#f
(1.0978769197088855e-145)6.026668654147353e-291(0.0 5.421010862427522e-20)+nan.0validexit10.142043#f
(-4.219856154985385e-77)8.903592984384017e-154(0.0 5.421010862427522e-20)+nan.0validexit10.14432#f
(-1.9452111915289187e-200)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.075339#f
(1.3416570989070883e-178)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.172074#f
(1.5210855061096695e-291)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.09415499999999999#f
(1.6935403382925588e-264)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.138302#f
(1.0883944979580257e-241)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.136485#f
(2.6791422358943944e-191)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.148926#f
(-2.8964204925337912e-295)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.163057#f
(3.648961330904921e-266)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.06990500000000001#f
(-1.870099658477282e-239)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.143072#f
(-1.4803424565241537e-305)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.07519#f
(-2.101999797525572e-65)2.209201574398773e-130(0.0 5.421010862427522e-20)+nan.0validexit10.07501000000000001#f
(-2.1975505137615657e-202)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.11692#f
(7.584139801546723e-107)2.8759588264702585e-213(0.0 5.421010862427522e-20)+nan.0validexit10.075918#f
(-7.647397517330312e-39)2.924134439403491e-77(0.0 5.421010862427522e-20)+nan.0validexit10.1325#f
(-7.90964137398124e-284)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.132932#f
(-1.6733281055540374e-55)1.400013474418532e-110(0.0 5.421010862427522e-20)+nan.0validexit10.110415#f
(7.690065717202844e-226)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.067327#f
(-8.297457392578683e-261)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.12173#f
(1.7278088981908425e-248)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.13106#f
(-1.4551225412157304e-296)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.080485#f
(4.041510527948795e-232)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.14849700000000002#f
(1.2492061192207818e-243)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.157542#f
(2.8146021338495732e-67)3.9609925859352853e-134(0.0 5.421010862427522e-20)+nan.0validexit10.144716#f
(-4.466896081871266e-237)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.146655#f
(-2.3250614779316982e-241)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.13986#f
(6.023888761648948e-164)0.0(0.0 5.421010862427522e-20)+nan.0validexit10.131588#f
(3.888309429528285e-195)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.12291400000000001#f
(-3.1411615340156807e-270)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.142313#f
(-1.6013423218227457e-66)1.282148615830331e-132(0.0 5.421010862427522e-20)+nan.0validexit10.134932#f
(-3.6638301345241345e-308)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.07730500000000001#f
(-3.601117804482481e-139)6.484024720880361e-278(0.0 5.421010862427522e-20)+nan.0validexit10.135442#f
(1.8033971320987115e-149)1.6261206080309287e-298(0.0 5.421010862427522e-20)+nan.0validexit10.118665#f
(1.2094977672716362e-304)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.10991400000000001#f
(-3.8547163370856417e-199)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.140812#f
(6.655322269450247e-107)2.2146657255120193e-213(0.0 5.421010862427522e-20)+nan.0validexit10.14718399999999998#f
(4.849959751492115e-132)1.1761054795546729e-263(0.0 5.421010862427522e-20)+nan.0validexit10.154469#f
(-6.321355342908465e-204)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.140372#f
(-4.4922098854306015e-291)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.149731#f
(3.707637391663345e-164)0.0(0.0 5.421010862427522e-20)+nan.0validexit10.135572#f
(7.055299604553213e-218)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.13643#f
(2.0610296747821374e-290)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.076057#f
(1.5977931604038262e-183)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.112692#f
(2.365253849010628e-232)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.138539#f
(-3.5005776994832636e-92)6.127022115059769e-184(0.0 5.421010862427522e-20)+nan.0validexit10.17317#f
(-1.679434364885183e-301)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.108684#f
(8.674396237454356e-187)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.13748300000000002#f
(1.4388202732013415e-273)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.145983#f
(-6.508068112343273e-250)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.144262#f
(-2.1450052695148675e-290)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.148554#f
(-3.8913086082154245e-212)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.144816#f
(4.737888060303965e-155)1.122379163598544e-309(0.0 5.421010862427522e-20)+nan.0validexit10.076814#f
(-1.5472268989229774e-298)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.151853#f
(1.2114248923011617e-255)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.13748#f
(1.5548957319528716e-233)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.145941#f
(2.996855730887923e-171)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.133068#f
(9.12561020913937e-197)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.141098#f
(-2.4072590293253094e-105)2.8974480171341154e-210(0.0 5.421010862427522e-20)+nan.0validexit10.132736#f
(-3.0219087882927556e-228)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.132716#f
(1.3872465774673514e-271)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.13485#f
(-6.995364024406251e-275)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.174946#f
(1.0391042295924186e-222)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.14568599999999998#f
(-6.110573653722474e-261)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.067944#f
(-1.5055934989420396e-215)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.139925#f
(1.2798972286003159e-233)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.143045#f
(3.3310389857779494e-223)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.13956400000000002#f
(3.1435285840218627e-94)4.9408859792812486e-188(0.0 5.421010862427522e-20)+nan.0validexit10.143794#f
(9.586090035628696e-287)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.13925200000000001#f
(-5.943453877443393e-94)1.7662321996648453e-187(0.0 5.421010862427522e-20)+nan.0validexit10.139636#f
(3.251983079011689e-55)5.287696973089173e-110(0.0 5.421010862427522e-20)+nan.0validexit10.13252#f
(-2.8287411691767466e-300)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.142191#f
(-2.535890428805892e-233)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.13764300000000002#f
(1.5255557949633994e-209)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.147523#f
(-3.589617743796158e-294)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.080071#f
(1.71776762030442e-165)0.0(0.0 5.421010862427522e-20)+nan.0validexit10.134078#f
(1.2896608849387834e-293)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.144027#f
(9.135414067556101e-221)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.122239#f
(-1.1022399264867348e-215)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.080109#f
(6.900564888249276e-14)2.3808897888469374e-27(0.0 5.421010862427522e-20)+nan.0validexit10.062641#f
(8.004767934218891e-100)3.203815484034948e-199(0.0 5.421010862427522e-20)+nan.0validexit10.146914#f
(5.878505120117978e-308)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.13302999999999998#f
(-1.3475683515529738e-151)9.079702310535996e-303(0.0 5.421010862427522e-20)+nan.0validexit10.148099#f
(3.069143473104269e-162)5e-324(0.0 5.421010862427522e-20)+nan.0validexit10.07341700000000001#f
(-1.950740835383771e-95)1.9026949034168864e-190(0.0 5.421010862427522e-20)+nan.0validexit10.109163#f
(2.1082918503937468e-279)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.135592#f
(1.3295151881865879e-298)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.140383#f
(-8.099333324615514e-38)3.2799600151613694e-75(0.0 5.421010862427522e-20)+nan.0validexit10.14519#f
(1.1074171718482954e-159)6.13185e-319(0.0 5.421010862427522e-20)+nan.0validexit10.14467200000000002#f
(2.7894320112970507e-308)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.143158#f
(2.4478626018065953e-210)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.118311#f
(-1.6493735860807078e-158)1.36021663e-316(0.0 5.421010862427522e-20)+nan.0validexit10.138599#f
(1.6305590338643828e-189)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.132905#f
(-2.440592618406445e-286)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.099434#f
(1.1569951901946668e-186)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.132907#f
(-1.822156108783895e-157)1.6601264423e-314(0.0 5.421010862427522e-20)+nan.0validexit10.08052#f
(5.625298304296878e-190)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.129133#f
(3.543719960585134e-148)6.278975579524752e-296(0.0 5.421010862427522e-20)+nan.0validexit10.163955#f
(3.809593427595659e-237)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.12924#f
(5.924744658602038e-256)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.139349#f
(-8.0132685559875e-275)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.150734#f
(7.14016533674736e-288)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.15049200000000001#f
(-3.0439035035273396e-165)0.0(0.0 5.421010862427522e-20)+nan.0validexit10.148951#f
(-2.588194219647119e-232)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.156583#f
(1.7098468882914587e-195)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.13759500000000002#f
(-2.444378631812157e-278)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.14790699999999998#f
(-1.6950651023172433e-154)1.436622850546883e-308(0.0 5.421010862427522e-20)+nan.0validexit10.138504#f
(-9.93933765380947e-166)0.0(0.0 5.421010862427522e-20)+nan.0validexit10.140735#f
(2.0685653778727868e-80)2.1394813612669925e-160(0.0 5.421010862427522e-20)+nan.0validexit10.134945#f
(3.4848643926530475e-292)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.157905#f
(7.082042128068748e-265)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.090962#f
(-1.10910518573774e-219)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.14030299999999998#f
(4.885528708467108e-250)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.10415400000000001#f
(8.230055780630591e-108)3.3866909076145505e-215(0.0 5.421010862427522e-20)+nan.0validexit10.15846#f
(9.654825922601257e-194)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.136687#f
(-3.158228080606615e-91)4.987202304566072e-182(0.0 5.421010862427522e-20)+nan.0validexit10.14613199999999998#f
(-9.688576669279787e-307)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.139261#f
(6.098133574873792e-202)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.132906#f
(4.637232033046599e-290)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.097994#f
(1.924811062740243e-96)1.852448813623612e-192(0.0 5.421010862427522e-20)+nan.0validexit10.117895#f
(3.3046283167844107e-221)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.134839#f
(3.8074174678504306e-68)7.248213887246293e-136(+nan.0 +nan.0)+nan.0validexit15.0#f
(-1.889967162596871e-275)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.14168899999999998#f
(-1.8273850086208675e-130)1.669667984866144e-260(0.0 5.421010862427522e-20)+nan.0validexit10.142191#f
(-6.742874475122701e-215)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.145406#f
Sollya timings
Total time spent in Sollya 1.1s
Bogosity

preprocess278.0ms (0.8%)

Algorithm
egg-herbie
Rules
16×fma-neg
11×fma-define
sub-neg
associate--r+
associate-+l-
Iterations

Useful iterations: 1 (0.0ms)

IterNodesCost
01360
12556
24456
36656
410656
513156
614156
714356
Stop Event
saturated
Calls
Call 1
Inputs
(-.f64 #s(literal 1 binary64) (cos.f64 x))
(-.f64 #s(literal 1 binary64) (cos.f64 x))
(-.f64 #s(literal 1 binary64) (cos.f64 (neg.f64 x)))
(neg.f64 (-.f64 #s(literal 1 binary64) (cos.f64 (neg.f64 x))))
Outputs
(-.f64 #s(literal 1 binary64) (cos.f64 x))
(-.f64 #s(literal 1 binary64) (cos.f64 x))
(-.f64 #s(literal 1 binary64) (cos.f64 (neg.f64 x)))
(-.f64 #s(literal 1 binary64) (cos.f64 x))
(neg.f64 (-.f64 #s(literal 1 binary64) (cos.f64 (neg.f64 x))))
(neg.f64 (-.f64 #s(literal 1 binary64) (cos.f64 x)))
(+.f64 #s(literal -1 binary64) (cos.f64 x))
(+.f64 (cos.f64 x) #s(literal -1 binary64))
Symmetry

(abs x)

Compiler

Compiled 5 to 4 computations (20% saved)

eval1.0ms (0%)

Compiler

Compiled 1 to 1 computations (0% saved)

prune4.0ms (0%)

Alt Table
Click to see full alt table
StatusAccuracyProgram
53.5%
(-.f64 #s(literal 1 binary64) (cos.f64 x))
Compiler

Compiled 10 to 8 computations (20% saved)

simplify37.0ms (0.1%)

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

Useful iterations: 0 (0.0ms)

IterNodesCost
0914
11614
22014
32214
42314
Stop Event
saturated
Calls
Call 1
Inputs
(-.f64 #s(literal 1 binary64) (cos.f64 x))
Outputs
(-.f64 #s(literal 1 binary64) (cos.f64 x))

soundness2.0ms (0%)

Stop Event
fuel
Compiler

Compiled 5 to 4 computations (20% saved)

preprocess161.0ms (0.5%)

Remove

(abs x)

Compiler

Compiled 62 to 46 computations (25.8% saved)

end0.0ms (0%)

Profiling

Loading profile data...