VandenBroeck and Keller, Equation (6)

Time bar (total: 20.1s)

analyze251.0ms (1.2%)

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
0%0%99.9%0.1%0%0%0%4
0%0%99.9%0.1%0%0%0%5
0%0%99.9%0.1%0%0%0%6
21.9%21.9%78%0.1%0%0%0%7
23.4%23.4%76.5%0.1%0%0%0%8
35.2%35.1%64.8%0.1%0%0%0%9
36.3%36.3%63.6%0.1%0%0%0%10
42.4%42.3%57.6%0.1%0%0%0%11
43.1%43%56.9%0.1%0%0%0%12
Compiler

Compiled 17 to 11 computations (35.3% saved)

sample19.5s (97%)

Results
872.0ms4430×0valid
475.0ms4421×0valid-sollya
5.5s3716×1valid
539.0ms3693×1valid-sollya
335.0ms110×2valid
17.0ms107×2valid-sollya
4.0ms23×1exit-sollya
2.0ms0exit-sollya
0.0ms2exit-sollya
2.0ms5exit
0.0ms5exit-sollya
Sollya Eval
PtRival-outSollya-intervalSollya-pointstatusSollya statusRival itersollya-timecheck
(-2.799716995586697e-113 -4.890535972497031e-273)1.960099252559225e-47(1.960099252559225e-47 1.960099252559225e-47)+nan.0validexit00.18837800000000002#f
(-3.1038994016371267e-87 -1.0692301237930477e-75)3.4866293694493667e+98(3.4866293694493667e+98 3.4866293694493667e+98)+nan.0validexit00.181357#f
(7.178787696076411e-211 -2.7564237245049986e+113)-8.65956052308552e+113(-inf.0 +inf.0)+nan.0validexit10.124927#f
(1.585185340533517e+105 -4.0009310078048245e+96)-1.2569295461639245e+97(-inf.0 +inf.0)+nan.0validexit10.144183#f
(-3.492644712880914e-170 1.013974757284637e+205)3.185495648410909e+205(-inf.0 +inf.0)+nan.0validexit10.190173#f
(-3.730405230951145e+167 7.042968819949353e-137)2.2126139104214863e-136(2.2126139104214863e-136 2.2126139104214863e-136)+nan.0validexit00.12265200000000001#f
(1.3032493158359997e+306 3.309078791880391e-95)1.0395777622721225e-94(1.0395777622721225e-94 1.0395777622721225e-94)+nan.0validexit00.192601#f
(-2.211234256794581e+74 -1.4860580818945643e-18)-4.668589152887703e-18(-4.668589152887703e-18 -4.668589152887703e-18)+nan.0validexit00.179824#f
(6.673636284619872e-96 -2.143874197788501e+142)-6.735179429993066e+142(-inf.0 +inf.0)+nan.0validexit10.132772#f
(-5.857574651400348e+265 3.1752503824368605e+299)9.975343274771822e+299(-inf.0 +inf.0)+nan.0validexit10.219801#f
(6.063590375492147e-212 -9.686106220483632e+73)-3.0429800144161776e+74(-inf.0 +inf.0)+nan.0validexit10.154604#f
(1.0866559023780029e-293 -1.6594045891538225e+103)-5.213173266618838e+103(-inf.0 +inf.0)+nan.0validexit20.160359#f
(4.918983574765761e+244 1.1354149538715085e-98)3.567011277858725e-98(3.567011277858725e-98 3.567011277858725e-98)+nan.0validexit00.122337#f
(1.1482561491741256e-56 2.646888685941472e+125)8.31544605062367e+125(-inf.0 +inf.0)+nan.0validexit10.081436#f
(-4.0051273755976293e-249 1.2400389408024658e+177)3.895697226590295e+177(-inf.0 +inf.0)+nan.0validexit10.089183#f
(-1.071848765896411e-304 1.892141631182914e+289)5.944338248075651e+289(-inf.0 +inf.0)+nan.0validexit10.166673#f
(2.9118179448746997e-307 -1.905362429124258e-287)+inf.0(+inf.0 +inf.0)+nan.0validexit00.25489399999999995#f
(6.966302183064785e+19 -2.291879564828041e-5)-7.200152003776347e-5(-7.200152003776347e-5 -7.200152003776347e-5)+nan.0validexit00.219807#f
(-1.1170052819607512e-207 -7.046498509448773e+249)-2.2137227950815694e+250(-inf.0 +inf.0)+nan.0validexit10.165623#f
(3.2077674843987507e-156 3.8657442984019734e+272)1.214459388851627e+273(-inf.0 +inf.0)+nan.0validexit10.19466199999999997#f
(1.2034807600733975e-302 1.1667149343880222e+21)3.665343066706908e+21(-inf.0 +inf.0)+nan.0validexit20.10951#f
(-2.397501991344753e-113 -736025289386500600.0)-2312291641992932000.0(-4.266659827785495e+224 4.618718057209834e+224)+nan.0validexit10.1862#f
(-4.562547290453756e-269 4.5439947714664155e+49)1.4275380591989322e+50(-inf.0 +inf.0)+nan.0validexit20.136991#f
(-3.073940055106892e-259 -1.5925166972482828e-77)+inf.0(+inf.0 +inf.0)+nan.0validexit00.127916#f
(9.106754259027182e-287 -1.537587539705045e+131)-4.830473718988574e+131(-inf.0 +inf.0)+nan.0validexit10.13483#f
(-7.605956765459926e+102 1.0078856166658331e+281)3.1663660489762e+281(-inf.0 +inf.0)+nan.0validexit10.171701#f
(-3.543555330126567e+279 -7.300647319590181e+272)-2.293565998567453e+273(-inf.0 +inf.0)+nan.0validexit10.11541#f
(7.393310466489808e+72 3.111462725215774e+212)9.774948439456354e+212(-inf.0 +inf.0)+nan.0validexit10.193589#f
(2.1477777990328306e-19 -1.6105426433007435e+42)-5.0596689364867024e+42(-inf.0 +inf.0)+nan.0validexit10.14424800000000002#f
(2.238313507343342e-179 6.415648590403252e+106)2.015535447962457e+107(-inf.0 +inf.0)+nan.0validexit10.161947#f
(-1.0275703416418161e+183 7.386127002908123e+184)2.3204202330817357e+185(-inf.0 +inf.0)+nan.0validexit10.18671000000000001#f
(8.849076991200207e-36 -5.297677629782683e+144)-1.6643145122812267e+145(-inf.0 +inf.0)+nan.0validexit10.129706#f
(-1.4258479991048446e-257 -4.454705648276126e+47)-1.3994870538529235e+48(-inf.0 +inf.0)+nan.0validexit10.127916#f
(8.580393053779348e-178 5.3465657552712025e+143)1.6796731698694775e+144(-inf.0 +inf.0)+nan.0validexit10.117598#f
(-7.696222760580015e+289 8.486754432616306e+117)2.6661925378328e+118(-inf.0 +inf.0)+nan.0validexit10.174566#f
Sollya timings
Total time spent in Sollya 1.0s
Bogosity

preprocess202.0ms (1%)

Algorithm
egg-herbie
Rules
394×fma-define
301×times-frac
209×fma-neg
96×associate-*r*
87×associate-/r*
Iterations

Useful iterations: 1 (0.0ms)

IterNodesCost
034415
197357
2270357
3708357
41312357
51876357
62255357
72424357
82435357
Stop Event
saturated
Calls
Call 1
Inputs
(-.f64 (*.f64 (PI.f64) l) (*.f64 (/.f64 #s(literal 1 binary64) (*.f64 F F)) (tan.f64 (*.f64 (PI.f64) l))))
(-.f64 (*.f64 (PI.f64) l) (*.f64 (/.f64 #s(literal 1 binary64) (*.f64 F F)) (tan.f64 (*.f64 (PI.f64) l))))
(-.f64 (*.f64 (PI.f64) l) (*.f64 (/.f64 #s(literal 1 binary64) (*.f64 (neg.f64 F) (neg.f64 F))) (tan.f64 (*.f64 (PI.f64) l))))
(-.f64 (*.f64 (PI.f64) (neg.f64 l)) (*.f64 (/.f64 #s(literal 1 binary64) (*.f64 F F)) (tan.f64 (*.f64 (PI.f64) (neg.f64 l)))))
(neg.f64 (-.f64 (*.f64 (PI.f64) l) (*.f64 (/.f64 #s(literal 1 binary64) (*.f64 (neg.f64 F) (neg.f64 F))) (tan.f64 (*.f64 (PI.f64) l)))))
(neg.f64 (-.f64 (*.f64 (PI.f64) (neg.f64 l)) (*.f64 (/.f64 #s(literal 1 binary64) (*.f64 F F)) (tan.f64 (*.f64 (PI.f64) (neg.f64 l))))))
(-.f64 (*.f64 (PI.f64) F) (*.f64 (/.f64 #s(literal 1 binary64) (*.f64 l l)) (tan.f64 (*.f64 (PI.f64) F))))
Outputs
(-.f64 (*.f64 (PI.f64) l) (*.f64 (/.f64 #s(literal 1 binary64) (*.f64 F F)) (tan.f64 (*.f64 (PI.f64) l))))
(-.f64 (*.f64 (PI.f64) l) (/.f64 (tan.f64 (*.f64 (PI.f64) l)) (*.f64 F F)))
(fma.f64 (PI.f64) l (/.f64 (tan.f64 (*.f64 (PI.f64) l)) (*.f64 F (neg.f64 F))))
(-.f64 (*.f64 (PI.f64) l) (*.f64 (/.f64 #s(literal 1 binary64) (*.f64 F F)) (tan.f64 (*.f64 (PI.f64) l))))
(-.f64 (*.f64 (PI.f64) l) (/.f64 (tan.f64 (*.f64 (PI.f64) l)) (*.f64 F F)))
(fma.f64 (PI.f64) l (/.f64 (tan.f64 (*.f64 (PI.f64) l)) (*.f64 F (neg.f64 F))))
(-.f64 (*.f64 (PI.f64) l) (*.f64 (/.f64 #s(literal 1 binary64) (*.f64 (neg.f64 F) (neg.f64 F))) (tan.f64 (*.f64 (PI.f64) l))))
(-.f64 (*.f64 (PI.f64) l) (*.f64 (/.f64 #s(literal 1 binary64) (*.f64 F F)) (tan.f64 (*.f64 (PI.f64) l))))
(-.f64 (*.f64 (PI.f64) l) (/.f64 (tan.f64 (*.f64 (PI.f64) l)) (*.f64 F F)))
(fma.f64 (PI.f64) l (/.f64 (tan.f64 (*.f64 (PI.f64) l)) (*.f64 F (neg.f64 F))))
(-.f64 (*.f64 (PI.f64) (neg.f64 l)) (*.f64 (/.f64 #s(literal 1 binary64) (*.f64 F F)) (tan.f64 (*.f64 (PI.f64) (neg.f64 l)))))
(fma.f64 (PI.f64) (neg.f64 l) (/.f64 (tan.f64 (*.f64 (PI.f64) l)) (*.f64 F F)))
(-.f64 (/.f64 (tan.f64 (*.f64 (PI.f64) l)) (*.f64 F F)) (*.f64 (PI.f64) l))
(neg.f64 (-.f64 (*.f64 (PI.f64) l) (*.f64 (/.f64 #s(literal 1 binary64) (*.f64 (neg.f64 F) (neg.f64 F))) (tan.f64 (*.f64 (PI.f64) l)))))
(-.f64 (*.f64 (PI.f64) (neg.f64 l)) (*.f64 (/.f64 #s(literal 1 binary64) (*.f64 F F)) (tan.f64 (*.f64 (PI.f64) (neg.f64 l)))))
(fma.f64 (PI.f64) (neg.f64 l) (/.f64 (tan.f64 (*.f64 (PI.f64) l)) (*.f64 F F)))
(-.f64 (/.f64 (tan.f64 (*.f64 (PI.f64) l)) (*.f64 F F)) (*.f64 (PI.f64) l))
(neg.f64 (-.f64 (*.f64 (PI.f64) (neg.f64 l)) (*.f64 (/.f64 #s(literal 1 binary64) (*.f64 F F)) (tan.f64 (*.f64 (PI.f64) (neg.f64 l))))))
(-.f64 (*.f64 (PI.f64) l) (*.f64 (/.f64 #s(literal 1 binary64) (*.f64 F F)) (tan.f64 (*.f64 (PI.f64) l))))
(-.f64 (*.f64 (PI.f64) l) (/.f64 (tan.f64 (*.f64 (PI.f64) l)) (*.f64 F F)))
(fma.f64 (PI.f64) l (/.f64 (tan.f64 (*.f64 (PI.f64) l)) (*.f64 F (neg.f64 F))))
(-.f64 (*.f64 (PI.f64) F) (*.f64 (/.f64 #s(literal 1 binary64) (*.f64 l l)) (tan.f64 (*.f64 (PI.f64) F))))
(-.f64 (*.f64 (PI.f64) F) (/.f64 (/.f64 (tan.f64 (*.f64 (PI.f64) F)) l) l))
(-.f64 (*.f64 (PI.f64) F) (/.f64 (tan.f64 (*.f64 (PI.f64) F)) (*.f64 l l)))
Symmetry

(abs F)

(negabs l)

Compiler

Compiled 16 to 10 computations (37.5% saved)

eval0.0ms (0%)

Compiler

Compiled 2 to 2 computations (0% saved)

prune3.0ms (0%)

Alt Table
Click to see full alt table
StatusAccuracyProgram
80.4%
(-.f64 (*.f64 (PI.f64) l) (*.f64 (/.f64 #s(literal 1 binary64) (*.f64 F F)) (tan.f64 (*.f64 (PI.f64) l))))
Compiler

Compiled 32 to 20 computations (37.5% saved)

simplify33.0ms (0.2%)

Algorithm
egg-herbie
Rules
16×neg-mul-1
12×unsub-neg
*-commutative
distribute-lft-neg-in
distribute-rgt-neg-in
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
01657
12857
24357
35657
46857
59357
612757
712957
Stop Event
saturated
Calls
Call 1
Inputs
(-.f64 (*.f64 (PI.f64) l) (*.f64 (/.f64 #s(literal 1 binary64) (*.f64 F F)) (tan.f64 (*.f64 (PI.f64) l))))
Outputs
(-.f64 (*.f64 (PI.f64) l) (*.f64 (/.f64 #s(literal 1 binary64) (*.f64 F F)) (tan.f64 (*.f64 (PI.f64) l))))
(+.f64 (*.f64 (PI.f64) l) (*.f64 (tan.f64 (*.f64 (PI.f64) l)) (/.f64 #s(literal -1 binary64) (*.f64 F F))))

soundness1.0ms (0%)

Stop Event
fuel
Compiler

Compiled 16 to 10 computations (37.5% saved)

preprocess109.0ms (0.5%)

Remove

(negabs l)

(abs F)

Compiler

Compiled 192 to 120 computations (37.5% saved)

end0.0ms (0%)

Profiling

Loading profile data...