Migdal et al, Equation (64)

Time bar (total: 43.6s)

analyze0.0ms (0%)

Algorithm
search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%99.9%0.1%0%0%0%0
100%99.9%0%0.1%0%0%0%1
Compiler

Compiled 23 to 13 computations (43.5% saved)

sample43.1s (98.8%)

Results
8.6s8256×0valid
1.2s8214×0valid-sollya
57.0ms42×0exit-sollya
Sollya Eval
PtRival-outSollya-intervalSollya-pointstatusSollya statusRival itersollya-timecheck
(2.3918212489668453e-284 -3.7333081535240677e+65 -5.537190762486889e+178)-6.690322381058745e+130(-6.690322381058745e+130 -6.690322381058745e+130)+nan.0validexit00.507716#f
(-3.7724134318527817e+130 4.274508265742814e+122 -5.958067898232295e-119)1.0062909506357048e+261(1.0062909506357048e+261 1.0062909506357048e+261)+nan.0validexit00.416406#f
(-7.561221934370717e-235 1.4868776604375739e-80 2.999310533772771e+279)2.554250725369848e-161(2.554250725369848e-161 2.554250725369848e-161)+nan.0validexit00.41929700000000003#f
(-8.172013103096689e+272 6.2109444712021e-123 -93943815365037.67)+inf.0(+inf.0 +inf.0)+nan.0validexit00.34562200000000004#f
(4.8022433945375076e-85 -7.562591995629734e+263 2.3632515484782536e-176)+inf.0(+inf.0 +inf.0)+nan.0validexit00.468813#f
(-5.552511745110463e-110 -5.178740408448048e-47 1.0240545008438356e+281)3.088688837356237e-94(+nan.0 +nan.0)+nan.0validexit05.0#f
(-1.0497634706433124e+149 2.557060924767502e-25 -3.0313326183993265e-264)7.792340376427279e+297(+nan.0 +nan.0)+nan.0validexit05.0#f
(5.64626216734988e-231 2.1365940245800207e-246 4.7071658852944154e-201)0.0(0.0 0.0)+nan.0validexit00.34917#f
(1.0935971623864544e+268 -1.136382771730197e+117 1.729697289573379e-23)+inf.0(+inf.0 +inf.0)+nan.0validexit00.298245#f
(-5.021867192399543e+141 5.0935501979863816e+299 -7.68990249451972e+224)-inf.0(-inf.0 -inf.0)+nan.0validexit00.404237#f
(-1.186475512885387e+199 -5.409127473017922e+228 4.144276919288959e+208)-inf.0(-inf.0 -inf.0)+nan.0validexit00.344999#f
(1.3060046086344422e-114 1.1205238574837265e-79 -1.769847079793119e-141)8.878246882905848e-159(8.878246882905848e-159 8.878246882905848e-159)+nan.0validexit00.28899600000000003#f
(-1.627948927959424e-167 -3.27479164940653e-297 -3.8247144528037e+122)0.0(0.0 0.0)+nan.0validexit00.436166#f
(8.695233115841004e+95 -5.586558552266026e-272 4.004131063390474e-183)5.346227822334484e+191(+nan.0 +nan.0)+nan.0validexit05.0#f
(-3.6771835230294755e-177 5.763468412682909e+44 3.748398737439644e+259)1.0491593741643192e+88(1.0491593741643192e+88 1.0491593741643192e+88)+nan.0validexit00.507038#f
(8.57715551326533e-133 1.1943356721442714e-265 -1.0302053526166644e+129)-5.130544745928004e-265(-5.130544745928004e-265 -5.130544745928004e-265)+nan.0validexit00.266112#f
(1.1130526981170967e+213 6.914892352139873e-197 -2.2679053035907904e+288)+inf.0(+inf.0 +inf.0)+nan.0validexit00.527376#f
(1.2640742611611449e+92 -3.915609187457244e+25 4.1370906163267856e-86)1.1298744264966566e+184(1.1298744264966566e+184 1.1298744264966566e+184)+nan.0validexit00.4623#f
(-4.5757132933765965e+30 6.972179594558633e+162 -2.109664831294873e+205)+inf.0(+inf.0 +inf.0)+nan.0validexit00.497872#f
(-4.354526809741427e-35 1.3929457224074745e+209 2.1485884321007163e-97)+inf.0(+nan.0 +nan.0)+nan.0validexit05.0#f
(3.1774663319092703e-233 1.9243874316801472e+136 -8.111361244954405e+129)2.5992342768190022e+272(2.5992342768190022e+272 2.5992342768190022e+272)+nan.0validexit00.375778#f
(-4.785902912071715e+23 -5.625049918869544e-60 -3.2173642287951653e+130)4.0610666742220655e+46(4.0610666742220655e+46 4.0610666742220655e+46)+nan.0validexit00.341533#f
(-2.684723114043904e+187 1.5862423308217312e+307 6.4820041989231064e+268)+inf.0(+nan.0 +nan.0)+nan.0validexit05.0#f
(1.070893681055797e-8 -2.940032503176998e+257 -2.1807350975856714e+213)+inf.0(+inf.0 +inf.0)+nan.0validexit00.458957#f
(5.5129933371576766e-18 -4.684793401763006e+99 1.5298062340025007e-63)1.5519077034146067e+199(+nan.0 +nan.0)+nan.0validexit05.0#f
(2282234303649655.5 2.6290853263145723e-114 -1.5264571942617127e-11)3.6830317254312307e+30(3.6830317254312307e+30 3.6830317254312307e+30)+nan.0validexit00.143787#f
(-3.3590739363595904e+95 3.8626146202272466e+287 -1.0669339372677265e+306)-inf.0(-inf.0 -inf.0)+nan.0validexit00.446245#f
(2.2528849192288565e-89 -1.701593161895149e-202 -3.455531455929267e-194)3.588913721610743e-178(+nan.0 +nan.0)+nan.0validexit05.0#f
(8.599019494135666e-222 5.351499796715444e-60 5.713423235956542e-258)2.0250512960849454e-119(+nan.0 +nan.0)+nan.0validexit05.0#f
(4.5347017029865014e+271 -34.70755556311055 -6.762659589799109e+48)+inf.0(+inf.0 +inf.0)+nan.0validexit00.382026#f
(-2.247422031505005e+73 -9.440227753711621e+226 -1.4640323836123418e-60)+inf.0(+nan.0 +nan.0)+nan.0validexit05.0#f
(2.5374411997234133e+238 -4.480752738855576e+144 -4.1954108861409625e-292)+inf.0(+inf.0 +inf.0)+nan.0validexit00.44223999999999997#f
(-4.00396769779009e-90 -4.2571742212400986e+170 -3.7297658223821704e-231)+inf.0(+inf.0 +inf.0)+nan.0validexit00.3484#f
(6.576388079928187e-17 -9.194827718184708e-216 5.032671399477074e-165)3.058157645246207e-33(3.058157645246207e-33 3.058157645246207e-33)+nan.0validexit00.45201399999999997#f
(6.278592363274324e-6 -3.2957412197668284e+155 -6.495177708307251e-69)+inf.0(+inf.0 +inf.0)+nan.0validexit00.220238#f
(-5.593414698424968e+162 -1.3226904261287404e+187 2.891484160947054e+239)-inf.0(-inf.0 -inf.0)+nan.0validexit00.348017#f
(-2.2469774587594985e+67 -5.268958890863483e+196 1.3971388030014644e-11)+inf.0(+inf.0 +inf.0)+nan.0validexit00.203031#f
(-1.3982552551216575e-115 -6.012948566779609e+175 -1.2372723323133135e+49)-inf.0(-inf.0 -inf.0)+nan.0validexit00.30948#f
(-4.358637330863906e-64 -1.2683859945879908e-147 -7.405306382752398e+288)-1.3324675454165525e-127(-1.3324675454165525e-127 -1.3324675454165525e-127)+nan.0validexit00.290556#f
(2.637714403128698e-296 8.497216934893444e-236 2.68937032261728e+150)-0.0(-0.0 -0.0)+nan.0validexit00.367883#f
(-1.4408994895411127e+103 1.5381699958588536e+51 -2.1449749353650675e-107)1.4680889748192801e+206(1.4680889748192801e+206 1.4680889748192801e+206)+nan.0validexit00.203697#f
(2.3240667781120494e-55 1.54522380007836e+45 1.7849061918635674e+27)-1.4320000534411981e+90(-1.4320000534411981e+90 -1.4320000534411981e+90)+nan.0validexit00.256303#f
Sollya timings
Total time spent in Sollya 1.3s
Bogosity

preprocess471.0ms (1.1%)

Algorithm
egg-herbie
Rules
1241×fma-define
680×times-frac
547×fma-neg
460×div-sub
356×associate-/r*
Iterations

Useful iterations: 1 (0.0ms)

IterNodesCost
048606
1145562
2421562
31139562
42837562
55639562
66583562
77394562
87471562
97487562
Stop Event
node limit
Calls
Call 1
Inputs
(+.f64 (*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (*.f64 a1 a1)) (*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (*.f64 a2 a2)))
(+.f64 (*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (*.f64 a1 a1)) (*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (*.f64 a2 a2)))
(+.f64 (*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (*.f64 (neg.f64 a1) (neg.f64 a1))) (*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (*.f64 a2 a2)))
(+.f64 (*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (*.f64 a1 a1)) (*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (*.f64 (neg.f64 a2) (neg.f64 a2))))
(+.f64 (*.f64 (/.f64 (cos.f64 (neg.f64 th)) (sqrt.f64 #s(literal 2 binary64))) (*.f64 a1 a1)) (*.f64 (/.f64 (cos.f64 (neg.f64 th)) (sqrt.f64 #s(literal 2 binary64))) (*.f64 a2 a2)))
(neg.f64 (+.f64 (*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (*.f64 (neg.f64 a1) (neg.f64 a1))) (*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (*.f64 a2 a2))))
(neg.f64 (+.f64 (*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (*.f64 a1 a1)) (*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (*.f64 (neg.f64 a2) (neg.f64 a2)))))
(neg.f64 (+.f64 (*.f64 (/.f64 (cos.f64 (neg.f64 th)) (sqrt.f64 #s(literal 2 binary64))) (*.f64 a1 a1)) (*.f64 (/.f64 (cos.f64 (neg.f64 th)) (sqrt.f64 #s(literal 2 binary64))) (*.f64 a2 a2))))
(+.f64 (*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (*.f64 a2 a2)) (*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (*.f64 a1 a1)))
(+.f64 (*.f64 (/.f64 (cos.f64 a1) (sqrt.f64 #s(literal 2 binary64))) (*.f64 th th)) (*.f64 (/.f64 (cos.f64 a1) (sqrt.f64 #s(literal 2 binary64))) (*.f64 a2 a2)))
(+.f64 (*.f64 (/.f64 (cos.f64 a2) (sqrt.f64 #s(literal 2 binary64))) (*.f64 a1 a1)) (*.f64 (/.f64 (cos.f64 a2) (sqrt.f64 #s(literal 2 binary64))) (*.f64 th th)))
Outputs
(+.f64 (*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (*.f64 a1 a1)) (*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (*.f64 a2 a2)))
(*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (+.f64 (*.f64 a1 a1) (*.f64 a2 a2)))
(*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (fma.f64 a1 a1 (*.f64 a2 a2)))
(*.f64 (cos.f64 th) (/.f64 (fma.f64 a2 a2 (*.f64 a1 a1)) (sqrt.f64 #s(literal 2 binary64))))
(+.f64 (*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (*.f64 a1 a1)) (*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (*.f64 a2 a2)))
(*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (+.f64 (*.f64 a1 a1) (*.f64 a2 a2)))
(*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (fma.f64 a1 a1 (*.f64 a2 a2)))
(*.f64 (cos.f64 th) (/.f64 (fma.f64 a2 a2 (*.f64 a1 a1)) (sqrt.f64 #s(literal 2 binary64))))
(+.f64 (*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (*.f64 (neg.f64 a1) (neg.f64 a1))) (*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (*.f64 a2 a2)))
(*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (+.f64 (*.f64 a1 a1) (*.f64 a2 a2)))
(*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (fma.f64 a1 a1 (*.f64 a2 a2)))
(*.f64 (cos.f64 th) (/.f64 (fma.f64 a2 a2 (*.f64 a1 a1)) (sqrt.f64 #s(literal 2 binary64))))
(+.f64 (*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (*.f64 a1 a1)) (*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (*.f64 (neg.f64 a2) (neg.f64 a2))))
(*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (+.f64 (*.f64 a1 a1) (*.f64 a2 a2)))
(*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (fma.f64 a1 a1 (*.f64 a2 a2)))
(*.f64 (cos.f64 th) (/.f64 (fma.f64 a2 a2 (*.f64 a1 a1)) (sqrt.f64 #s(literal 2 binary64))))
(+.f64 (*.f64 (/.f64 (cos.f64 (neg.f64 th)) (sqrt.f64 #s(literal 2 binary64))) (*.f64 a1 a1)) (*.f64 (/.f64 (cos.f64 (neg.f64 th)) (sqrt.f64 #s(literal 2 binary64))) (*.f64 a2 a2)))
(*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (+.f64 (*.f64 a1 a1) (*.f64 a2 a2)))
(*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (fma.f64 a1 a1 (*.f64 a2 a2)))
(*.f64 (cos.f64 th) (/.f64 (fma.f64 a2 a2 (*.f64 a1 a1)) (sqrt.f64 #s(literal 2 binary64))))
(neg.f64 (+.f64 (*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (*.f64 (neg.f64 a1) (neg.f64 a1))) (*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (*.f64 a2 a2))))
(neg.f64 (*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (+.f64 (*.f64 a1 a1) (*.f64 a2 a2))))
(*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (neg.f64 (fma.f64 a1 a1 (*.f64 a2 a2))))
(*.f64 (fma.f64 a1 a1 (*.f64 a2 a2)) (/.f64 (cos.f64 th) (neg.f64 (sqrt.f64 #s(literal 2 binary64)))))
(*.f64 (cos.f64 th) (/.f64 (fma.f64 a2 a2 (*.f64 a1 a1)) (neg.f64 (sqrt.f64 #s(literal 2 binary64)))))
(neg.f64 (+.f64 (*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (*.f64 a1 a1)) (*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (*.f64 (neg.f64 a2) (neg.f64 a2)))))
(neg.f64 (*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (+.f64 (*.f64 a1 a1) (*.f64 a2 a2))))
(*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (neg.f64 (fma.f64 a1 a1 (*.f64 a2 a2))))
(*.f64 (fma.f64 a1 a1 (*.f64 a2 a2)) (/.f64 (cos.f64 th) (neg.f64 (sqrt.f64 #s(literal 2 binary64)))))
(*.f64 (cos.f64 th) (/.f64 (fma.f64 a2 a2 (*.f64 a1 a1)) (neg.f64 (sqrt.f64 #s(literal 2 binary64)))))
(neg.f64 (+.f64 (*.f64 (/.f64 (cos.f64 (neg.f64 th)) (sqrt.f64 #s(literal 2 binary64))) (*.f64 a1 a1)) (*.f64 (/.f64 (cos.f64 (neg.f64 th)) (sqrt.f64 #s(literal 2 binary64))) (*.f64 a2 a2))))
(neg.f64 (*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (+.f64 (*.f64 a1 a1) (*.f64 a2 a2))))
(*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (neg.f64 (fma.f64 a1 a1 (*.f64 a2 a2))))
(*.f64 (fma.f64 a1 a1 (*.f64 a2 a2)) (/.f64 (cos.f64 th) (neg.f64 (sqrt.f64 #s(literal 2 binary64)))))
(*.f64 (cos.f64 th) (/.f64 (fma.f64 a2 a2 (*.f64 a1 a1)) (neg.f64 (sqrt.f64 #s(literal 2 binary64)))))
(+.f64 (*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (*.f64 a2 a2)) (*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (*.f64 a1 a1)))
(*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (+.f64 (*.f64 a1 a1) (*.f64 a2 a2)))
(*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (fma.f64 a1 a1 (*.f64 a2 a2)))
(*.f64 (cos.f64 th) (/.f64 (fma.f64 a2 a2 (*.f64 a1 a1)) (sqrt.f64 #s(literal 2 binary64))))
(+.f64 (*.f64 (/.f64 (cos.f64 a1) (sqrt.f64 #s(literal 2 binary64))) (*.f64 th th)) (*.f64 (/.f64 (cos.f64 a1) (sqrt.f64 #s(literal 2 binary64))) (*.f64 a2 a2)))
(*.f64 (/.f64 (cos.f64 a1) (sqrt.f64 #s(literal 2 binary64))) (+.f64 (*.f64 th th) (*.f64 a2 a2)))
(*.f64 (/.f64 (cos.f64 a1) (sqrt.f64 #s(literal 2 binary64))) (fma.f64 th th (*.f64 a2 a2)))
(*.f64 (cos.f64 a1) (/.f64 (fma.f64 th th (*.f64 a2 a2)) (sqrt.f64 #s(literal 2 binary64))))
(+.f64 (*.f64 (/.f64 (cos.f64 a2) (sqrt.f64 #s(literal 2 binary64))) (*.f64 a1 a1)) (*.f64 (/.f64 (cos.f64 a2) (sqrt.f64 #s(literal 2 binary64))) (*.f64 th th)))
(*.f64 (/.f64 (cos.f64 a2) (sqrt.f64 #s(literal 2 binary64))) (+.f64 (*.f64 a1 a1) (*.f64 th th)))
(*.f64 (/.f64 (cos.f64 a2) (sqrt.f64 #s(literal 2 binary64))) (fma.f64 a1 a1 (*.f64 th th)))
(*.f64 (cos.f64 a2) (/.f64 (fma.f64 th th (*.f64 a1 a1)) (sqrt.f64 #s(literal 2 binary64))))
(*.f64 (/.f64 (cos.f64 a2) (sqrt.f64 #s(literal 2 binary64))) (fma.f64 th th (*.f64 a1 a1)))
Symmetry

(abs a1)

(abs a2)

(abs th)

(sort a1 a2)

Compiler

Compiled 22 to 12 computations (45.5% saved)

eval0.0ms (0%)

Compiler

Compiled 3 to 3 computations (0% saved)

prune1.0ms (0%)

Alt Table
Click to see full alt table
StatusAccuracyProgram
99.6%
(+.f64 (*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (*.f64 a1 a1)) (*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (*.f64 a2 a2)))
Compiler

Compiled 44 to 24 computations (45.5% saved)

simplify3.0ms (0%)

Algorithm
egg-herbie
Rules
*-commutative
+-commutative
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
01977
12277
Stop Event
saturated
Calls
Call 1
Inputs
(+.f64 (*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (*.f64 a1 a1)) (*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (*.f64 a2 a2)))
Outputs
(+.f64 (*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (*.f64 a1 a1)) (*.f64 (/.f64 (cos.f64 th) (sqrt.f64 #s(literal 2 binary64))) (*.f64 a2 a2)))

soundness1.0ms (0%)

Stop Event
fuel
Compiler

Compiled 22 to 12 computations (45.5% saved)

preprocess40.0ms (0.1%)

Remove

(sort a1 a2)

(abs th)

(abs a2)

(abs a1)

Compiler

Compiled 440 to 240 computations (45.5% saved)

end0.0ms (0%)

Profiling

Loading profile data...