Toniolo and Linder, Equation (7)

Time bar (total: 21.1s)

analyze356.0ms (1.7%)

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
0%0%99.9%0.1%0%0%0%7
0%0%74.9%0.1%0%25%0%8
4.2%3.1%71.8%0.1%0%25%0%9
6.3%4.7%70.2%0.1%0%25%0%10
11.3%7%55.4%0.1%0%37.4%0%11
16.9%10.5%51.9%0.1%0%37.4%0%12
Compiler

Compiled 31 to 19 computations (38.7% saved)

sample20.6s (97.5%)

Results
1.2s5302×0valid
532.0ms5293×0valid-sollya
543.0ms2678×0invalid
433.0ms2650×0invalid-sollya
855.0ms2216×1valid
308.0ms2210×1valid-sollya
393.0ms1151×1invalid
191.0ms1144×1invalid-sollya
455.0ms738×2valid
126.0ms737×2valid-sollya
433.0ms489×2invalid
87.0ms483×2invalid-sollya
12.0ms37×0exit-sollya
2.0ms13×1exit-sollya
1.0ms2exit-sollya
Sollya Eval
PtRival-outSollya-intervalSollya-pointstatusSollya statusRival itersollya-timecheck
(-3.380965955160656e-70 2.740713478217599e-177 3.878275472006805e-289)#f(+nan.0 +nan.0)+nan.0invalidexit00.121964#f
(-1.1323463103372095e+114 -4.740078011017948e+20 6.046232910794732e+197)1.0(1.0 1.0)+nan.0validexit00.319963#f
(-4.0923905988356405e+300 1.6836945438807768e+298 7.796021930045784e-105)#f(+nan.0 +nan.0)+nan.0invalidexit20.24232#f
(-2.674247013258289e+241 2.9375658849902445e+81 1.1249888140231323e-169)#f(+nan.0 +nan.0)+nan.0invalidexit20.20540399999999998#f
(1.741638253036901e+140 7.006007562514305e+56 -8.155230141136778e+208)-1.0(-1.0 -1.0)+nan.0validexit00.338928#f
(1.3765786126633647e+243 -8.528769857557208e+257 -1.492004456269634e-259)-0.0(+nan.0 +nan.0)+nan.0validexit20.251047#f
(7.796172495336584e-9 -4.150651599890974e-287 1.8407223045500223e-30)#f(+nan.0 +nan.0)+nan.0invalidexit00.099258#f
(3.9379953030621183e-72 -1.8586301679903056e+183 -9.419193866861593e+38)#f(+nan.0 +nan.0)+nan.0invalidexit00.224283#f
(-1.2826877862880822e+45 -9.322805891216606e-58 8.21397191097912e+130)1.0(1.0 1.0)+nan.0validexit00.27097200000000005#f
(-1.4144126537958653e-11 5.888802714737221e-124 4.2066529537192616e-159)#f(+nan.0 +nan.0)+nan.0invalidexit00.205099#f
(4.59160114932089e+259 5.092565201023266e-53 -4.875935499634594e-52)-1.0(-1.0 -1.0)+nan.0validexit00.31373399999999996#f
(-6.048384023383111e-27 -1.1073527278714566e+201 -3.6863380092352964e-264)#f(+nan.0 +nan.0)+nan.0invalidexit00.125856#f
(0.005277807747124217 3.1021763378069536e-208 -7.712264471070785e-63)#f(+nan.0 +nan.0)+nan.0invalidexit00.19514900000000002#f
(2.1044094922014965e-30 8.650219309556901e+191 1.7035355064470535e-273)#f(+nan.0 +nan.0)+nan.0invalidexit00.106613#f
(-8.476517362039332e-8 5.654937697105062e-221 6.775167224484469e-99)#f(+nan.0 +nan.0)+nan.0invalidexit00.20539700000000002#f
(3.3064223127894026e+70 -2.7649368440586046e+167 -1.0807361514034748e+52)-7.107446920191535e-81(+nan.0 +nan.0)+nan.0validexit10.205384#f
(-4.557229391831899e+231 5.1631605055692385e-65 -8.145636225032511e-265)#f(+nan.0 +nan.0)+nan.0invalidexit20.11140599999999999#f
(3.9364438515425713e-13 -2.4057795092110466e+249 -6.742479018448641e+202)#f(+nan.0 +nan.0)+nan.0invalidexit00.156525#f
(-28917596.818750303 7.253183053038345e-202 -5.936376900141327e-293)#f(+nan.0 +nan.0)+nan.0invalidexit00.172641#f
(5.423449306346955e+68 5.222187509530124e+255 -4.156309894762708e+148)-1.8535028237129173e-73(+nan.0 +nan.0)+nan.0validexit10.11225700000000001#f
(2.35479023928434e+281 -8.460382709443017e-194 -2.515267595667316e+117)-1.0(-1.0 -1.0)+nan.0validexit00.335631#f
(-1.5275448785516204e+175 -1.6193351764554357e-6 -2.4336667507938627e-200)#f(+nan.0 +nan.0)+nan.0invalidexit10.167614#f
(-1.126990187338535e-39 1.4771928576695826e-230 3.2899758736931567e-223)#f(+nan.0 +nan.0)+nan.0invalidexit00.098934#f
(2.704845946010758e-28 7.226309690347294e+296 -2.266609897155442e-290)#f(+nan.0 +nan.0)+nan.0invalidexit00.178691#f
(-4.68372089690421e+196 -8.129418970914112e+235 -1.5340869687437722e+168)-1.0(+nan.0 +nan.0)+nan.0validexit10.11536500000000001#f
(-1.3055378172316917e+236 -5.281712594150469e-79 -5.3766577757257504e-304)#f(+nan.0 +nan.0)+nan.0invalidexit20.10331900000000001#f
(-54964440.174985476 3.20080625775373e+206 4.27434662683169e-262)#f(+nan.0 +nan.0)+nan.0invalidexit00.16683900000000002#f
(-3.8111548081849557e+171 -1.2342886069137601e+97 2.983607310373483e-289)#f(+nan.0 +nan.0)+nan.0invalidexit10.111651#f
(-1.799928372674053e+182 -1.9280220213762566e-96 -2.3906018804608732e-91)-1.0(-1.0 -1.0)+nan.0validexit00.31964899999999996#f
(-2.9028788095430703e+209 -1.1401993087796605e-42 -6.058885562531988e-301)#f(+nan.0 +nan.0)+nan.0invalidexit10.201227#f
(-227113382029.72726 2.2946434640537403e-173 1.5798784707706038e+193)1.0000000000044031(1.0000000000044031 1.0000000000044031)+nan.0validexit00.157076#f
(-9.836556845115967e+210 5.3757774109306355e+91 6.218574083023141e-118)#f(+nan.0 +nan.0)+nan.0invalidexit20.12914299999999998#f
(-2.706452074969248e+116 -8.126343437413273e+103 3.1041822806354657e-25)#f(+nan.0 +nan.0)+nan.0invalidexit10.11212899999999999#f
(-6.640496124586235e-40 -4.010406494174309e-247 1.1568477411752131e-291)#f(+nan.0 +nan.0)+nan.0invalidexit00.114845#f
(-4.0176143723060147e-53 -5.513861865598235e+143 -1.945805458183028e+134)#f(+nan.0 +nan.0)+nan.0invalidexit00.219025#f
(2.8120657203686722e+138 -1.996548753651265e-183 3.945217361708495e-292)3.3136279831359592e-40(+nan.0 +nan.0)+nan.0validexit10.174733#f
(4.827487763474579e-41 -7.056106125783316e-123 -1.5818148156952353e+109)#f(+nan.0 +nan.0)+nan.0invalidexit00.106155#f
(-6.287946197183152e+121 -8.236701180461546e+300 6.219503088197789e+190)#f(+nan.0 +nan.0)+nan.0invalidexit10.115804#f
(-7.265330987525702e-65 -2.292851215608743e-226 -3.323985169298461e-259)#f(+nan.0 +nan.0)+nan.0invalidexit00.10346999999999999#f
(1.1585356549231961e+167 1.9273116813455524e+169 6.7129457007796225e+115)1.0(+nan.0 +nan.0)+nan.0validexit10.23619900000000002#f
(-1.758378931368378e+244 -7.957920685136166e+228 -2.662182057896322e-274)#f(+nan.0 +nan.0)+nan.0invalidexit20.242421#f
(2.4978418004595155e-20 2.318522671740723e+25 -145659648447988.8)#f(+nan.0 +nan.0)+nan.0invalidexit00.202397#f
(-8.06959578477835e-12 4.154037698676917e-110 -1.2294992156465788e+301)#f(+nan.0 +nan.0)+nan.0invalidexit00.11071299999999999#f
(0.00026007058157266193 2.671693063971789e+69 6.394692271889172e-225)#f(+nan.0 +nan.0)+nan.0invalidexit00.17715999999999998#f
(3.734875695285639e-65 3.8466187033072256e+55 3.527729000742922e-286)#f(+nan.0 +nan.0)+nan.0invalidexit00.137502#f
(-4.128318303658776e-52 2.0497342058605495e+28 -8.183694178922533e-243)#f(+nan.0 +nan.0)+nan.0invalidexit00.09568600000000001#f
(-3.269265908859669e+103 7170538.482742458 1.4951641845436812e-179)#f(+nan.0 +nan.0)+nan.0invalidexit10.174548#f
(2.123280591385353e+188 1.1735633873286293e+264 3.711624970823966e-6)4.608517392628623e-176(+nan.0 +nan.0)+nan.0validexit10.126003#f
(1.8073947716273048e-13 -4.992544151935004e+182 -2.4259450537572694e+146)#f(+nan.0 +nan.0)+nan.0invalidexit00.16502899999999998#f
(6.376458395066962e-6 1.1090522809155191e-95 -1.441890080603766e+155)#f(+nan.0 +nan.0)+nan.0invalidexit05.0#f
(-1.3285334920185942e-29 4.6471375931607685e+118 1.0762685905980334e-204)#f(+nan.0 +nan.0)+nan.0invalidexit00.188419#f
(2.5909229266449332e-42 -4.7967407998968e-102 9.025790873022948e+157)#f(+nan.0 +nan.0)+nan.0invalidexit00.160616#f
(2.258780145502088e+292 -1.2770308122781662e-161 1.6946413661050625e+83)1.0(1.0 1.0)+nan.0validexit00.156011#f
(1.0414125807113765e-61 -3.7675767016770866e-6 -5.436173441762925e-28)#f(+nan.0 +nan.0)+nan.0invalidexit00.195827#f
(-5.569699729930199e+238 4.879103249583639e+110 -4.846366941974053e+156)-1.0(-1.0 -1.0)+nan.0validexit00.157865#f
(3.7285763691921885e-22 -6.764928703884485e-129 3.729264103921825e-309)#f(+nan.0 +nan.0)+nan.0invalidexit00.178216#f
(-2.0661942790227789e+93 7.255785678864888e-142 3.1474641494709618e-257)#f(+nan.0 +nan.0)+nan.0invalidexit10.144957#f
Sollya timings
Total time spent in Sollya 1.7s
Bogosity

preprocess140.0ms (0.7%)

Algorithm
egg-herbie
Rules
502×distribute-lft-in
493×fma-neg
435×distribute-rgt-in
308×distribute-lft-neg-out
308×div-sub
Iterations

Useful iterations: 2 (0.0ms)

IterNodesCost
0781172
12561160
27401156
325661156
478161156
Stop Event
node limit
Calls
Call 1
Inputs
(/.f64 (*.f64 (sqrt.f64 #s(literal 2 binary64)) t) (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 x #s(literal 1 binary64)) (-.f64 x #s(literal 1 binary64))) (+.f64 (*.f64 l l) (*.f64 #s(literal 2 binary64) (*.f64 t t)))) (*.f64 l l))))
(/.f64 (*.f64 (sqrt.f64 #s(literal 2 binary64)) t) (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 x #s(literal 1 binary64)) (-.f64 x #s(literal 1 binary64))) (+.f64 (*.f64 l l) (*.f64 #s(literal 2 binary64) (*.f64 t t)))) (*.f64 l l))))
(/.f64 (*.f64 (sqrt.f64 #s(literal 2 binary64)) t) (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 (neg.f64 x) #s(literal 1 binary64)) (-.f64 (neg.f64 x) #s(literal 1 binary64))) (+.f64 (*.f64 l l) (*.f64 #s(literal 2 binary64) (*.f64 t t)))) (*.f64 l l))))
(/.f64 (*.f64 (sqrt.f64 #s(literal 2 binary64)) t) (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 x #s(literal 1 binary64)) (-.f64 x #s(literal 1 binary64))) (+.f64 (*.f64 (neg.f64 l) (neg.f64 l)) (*.f64 #s(literal 2 binary64) (*.f64 t t)))) (*.f64 (neg.f64 l) (neg.f64 l)))))
(/.f64 (*.f64 (sqrt.f64 #s(literal 2 binary64)) (neg.f64 t)) (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 x #s(literal 1 binary64)) (-.f64 x #s(literal 1 binary64))) (+.f64 (*.f64 l l) (*.f64 #s(literal 2 binary64) (*.f64 (neg.f64 t) (neg.f64 t))))) (*.f64 l l))))
(neg.f64 (/.f64 (*.f64 (sqrt.f64 #s(literal 2 binary64)) t) (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 (neg.f64 x) #s(literal 1 binary64)) (-.f64 (neg.f64 x) #s(literal 1 binary64))) (+.f64 (*.f64 l l) (*.f64 #s(literal 2 binary64) (*.f64 t t)))) (*.f64 l l)))))
(neg.f64 (/.f64 (*.f64 (sqrt.f64 #s(literal 2 binary64)) t) (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 x #s(literal 1 binary64)) (-.f64 x #s(literal 1 binary64))) (+.f64 (*.f64 (neg.f64 l) (neg.f64 l)) (*.f64 #s(literal 2 binary64) (*.f64 t t)))) (*.f64 (neg.f64 l) (neg.f64 l))))))
(neg.f64 (/.f64 (*.f64 (sqrt.f64 #s(literal 2 binary64)) (neg.f64 t)) (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 x #s(literal 1 binary64)) (-.f64 x #s(literal 1 binary64))) (+.f64 (*.f64 l l) (*.f64 #s(literal 2 binary64) (*.f64 (neg.f64 t) (neg.f64 t))))) (*.f64 l l)))))
(/.f64 (*.f64 (sqrt.f64 #s(literal 2 binary64)) t) (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 l #s(literal 1 binary64)) (-.f64 l #s(literal 1 binary64))) (+.f64 (*.f64 x x) (*.f64 #s(literal 2 binary64) (*.f64 t t)))) (*.f64 x x))))
(/.f64 (*.f64 (sqrt.f64 #s(literal 2 binary64)) x) (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 t #s(literal 1 binary64)) (-.f64 t #s(literal 1 binary64))) (+.f64 (*.f64 l l) (*.f64 #s(literal 2 binary64) (*.f64 x x)))) (*.f64 l l))))
(/.f64 (*.f64 (sqrt.f64 #s(literal 2 binary64)) l) (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 x #s(literal 1 binary64)) (-.f64 x #s(literal 1 binary64))) (+.f64 (*.f64 t t) (*.f64 #s(literal 2 binary64) (*.f64 l l)))) (*.f64 t t))))
Outputs
(/.f64 (*.f64 (sqrt.f64 #s(literal 2 binary64)) t) (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 x #s(literal 1 binary64)) (-.f64 x #s(literal 1 binary64))) (+.f64 (*.f64 l l) (*.f64 #s(literal 2 binary64) (*.f64 t t)))) (*.f64 l l))))
(*.f64 (sqrt.f64 #s(literal 2 binary64)) (/.f64 t (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 x #s(literal 1 binary64)) (+.f64 x #s(literal -1 binary64))) (fma.f64 l l (*.f64 #s(literal 2 binary64) (*.f64 t t)))) (*.f64 l l)))))
(*.f64 (sqrt.f64 #s(literal 2 binary64)) (/.f64 t (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 x #s(literal 1 binary64)) (+.f64 x #s(literal -1 binary64))) (fma.f64 #s(literal 2 binary64) (*.f64 t t) (*.f64 l l))) (*.f64 l l)))))
(*.f64 (sqrt.f64 #s(literal 2 binary64)) (/.f64 t (sqrt.f64 (fma.f64 (+.f64 x #s(literal 1 binary64)) (/.f64 (fma.f64 #s(literal 2 binary64) (*.f64 t t) (*.f64 l l)) (+.f64 x #s(literal -1 binary64))) (neg.f64 (*.f64 l l))))))
(/.f64 (*.f64 (sqrt.f64 #s(literal 2 binary64)) t) (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 x #s(literal 1 binary64)) (-.f64 x #s(literal 1 binary64))) (+.f64 (*.f64 l l) (*.f64 #s(literal 2 binary64) (*.f64 t t)))) (*.f64 l l))))
(*.f64 (sqrt.f64 #s(literal 2 binary64)) (/.f64 t (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 x #s(literal 1 binary64)) (+.f64 x #s(literal -1 binary64))) (fma.f64 l l (*.f64 #s(literal 2 binary64) (*.f64 t t)))) (*.f64 l l)))))
(*.f64 (sqrt.f64 #s(literal 2 binary64)) (/.f64 t (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 x #s(literal 1 binary64)) (+.f64 x #s(literal -1 binary64))) (fma.f64 #s(literal 2 binary64) (*.f64 t t) (*.f64 l l))) (*.f64 l l)))))
(*.f64 (sqrt.f64 #s(literal 2 binary64)) (/.f64 t (sqrt.f64 (fma.f64 (+.f64 x #s(literal 1 binary64)) (/.f64 (fma.f64 #s(literal 2 binary64) (*.f64 t t) (*.f64 l l)) (+.f64 x #s(literal -1 binary64))) (neg.f64 (*.f64 l l))))))
(/.f64 (*.f64 (sqrt.f64 #s(literal 2 binary64)) t) (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 (neg.f64 x) #s(literal 1 binary64)) (-.f64 (neg.f64 x) #s(literal 1 binary64))) (+.f64 (*.f64 l l) (*.f64 #s(literal 2 binary64) (*.f64 t t)))) (*.f64 l l))))
(/.f64 (*.f64 (sqrt.f64 #s(literal 2 binary64)) t) (sqrt.f64 (fma.f64 (/.f64 (+.f64 #s(literal 1 binary64) (neg.f64 x)) (+.f64 (neg.f64 x) #s(literal -1 binary64))) (fma.f64 l l (*.f64 #s(literal 2 binary64) (*.f64 t t))) (neg.f64 (*.f64 l l)))))
(/.f64 (*.f64 (sqrt.f64 #s(literal 2 binary64)) t) (sqrt.f64 (-.f64 (*.f64 (fma.f64 #s(literal 2 binary64) (*.f64 t t) (*.f64 l l)) (/.f64 (-.f64 #s(literal 1 binary64) x) (fma.f64 #s(literal -1 binary64) x #s(literal -1 binary64)))) (*.f64 l l))))
(*.f64 (sqrt.f64 #s(literal 2 binary64)) (/.f64 t (sqrt.f64 (fma.f64 (fma.f64 #s(literal 2 binary64) (*.f64 t t) (*.f64 l l)) (/.f64 (-.f64 #s(literal 1 binary64) x) (-.f64 #s(literal -1 binary64) x)) (neg.f64 (*.f64 l l))))))
(*.f64 t (/.f64 (sqrt.f64 #s(literal 2 binary64)) (sqrt.f64 (fma.f64 (fma.f64 #s(literal 2 binary64) (*.f64 t t) (*.f64 l l)) (/.f64 (-.f64 #s(literal 1 binary64) x) (-.f64 #s(literal -1 binary64) x)) (*.f64 l (neg.f64 l))))))
(/.f64 (*.f64 (sqrt.f64 #s(literal 2 binary64)) t) (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 x #s(literal 1 binary64)) (-.f64 x #s(literal 1 binary64))) (+.f64 (*.f64 (neg.f64 l) (neg.f64 l)) (*.f64 #s(literal 2 binary64) (*.f64 t t)))) (*.f64 (neg.f64 l) (neg.f64 l)))))
(*.f64 (sqrt.f64 #s(literal 2 binary64)) (/.f64 t (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 x #s(literal 1 binary64)) (+.f64 x #s(literal -1 binary64))) (fma.f64 l l (*.f64 #s(literal 2 binary64) (*.f64 t t)))) (*.f64 l l)))))
(*.f64 (sqrt.f64 #s(literal 2 binary64)) (/.f64 t (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 x #s(literal 1 binary64)) (+.f64 x #s(literal -1 binary64))) (fma.f64 #s(literal 2 binary64) (*.f64 t t) (*.f64 l l))) (*.f64 l l)))))
(*.f64 (sqrt.f64 #s(literal 2 binary64)) (/.f64 t (sqrt.f64 (fma.f64 (+.f64 x #s(literal 1 binary64)) (/.f64 (fma.f64 #s(literal 2 binary64) (*.f64 t t) (*.f64 l l)) (+.f64 x #s(literal -1 binary64))) (neg.f64 (*.f64 l l))))))
(/.f64 (*.f64 (sqrt.f64 #s(literal 2 binary64)) (neg.f64 t)) (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 x #s(literal 1 binary64)) (-.f64 x #s(literal 1 binary64))) (+.f64 (*.f64 l l) (*.f64 #s(literal 2 binary64) (*.f64 (neg.f64 t) (neg.f64 t))))) (*.f64 l l))))
(*.f64 (sqrt.f64 #s(literal 2 binary64)) (/.f64 (neg.f64 t) (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 x #s(literal 1 binary64)) (+.f64 x #s(literal -1 binary64))) (fma.f64 l l (*.f64 #s(literal 2 binary64) (*.f64 t t)))) (*.f64 l l)))))
(*.f64 (sqrt.f64 #s(literal 2 binary64)) (/.f64 (neg.f64 t) (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 x #s(literal 1 binary64)) (+.f64 x #s(literal -1 binary64))) (fma.f64 #s(literal 2 binary64) (*.f64 t t) (*.f64 l l))) (*.f64 l l)))))
(*.f64 (sqrt.f64 #s(literal 2 binary64)) (/.f64 (neg.f64 t) (sqrt.f64 (fma.f64 (+.f64 x #s(literal 1 binary64)) (/.f64 (fma.f64 #s(literal 2 binary64) (*.f64 t t) (*.f64 l l)) (+.f64 x #s(literal -1 binary64))) (neg.f64 (*.f64 l l))))))
(*.f64 t (/.f64 (neg.f64 (sqrt.f64 #s(literal 2 binary64))) (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 x #s(literal 1 binary64)) (+.f64 x #s(literal -1 binary64))) (fma.f64 #s(literal 2 binary64) (*.f64 t t) (*.f64 l l))) (*.f64 l l)))))
(neg.f64 (/.f64 (*.f64 (sqrt.f64 #s(literal 2 binary64)) t) (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 (neg.f64 x) #s(literal 1 binary64)) (-.f64 (neg.f64 x) #s(literal 1 binary64))) (+.f64 (*.f64 l l) (*.f64 #s(literal 2 binary64) (*.f64 t t)))) (*.f64 l l)))))
(/.f64 (*.f64 (sqrt.f64 #s(literal 2 binary64)) t) (neg.f64 (sqrt.f64 (fma.f64 (/.f64 (+.f64 #s(literal 1 binary64) (neg.f64 x)) (+.f64 (neg.f64 x) #s(literal -1 binary64))) (fma.f64 l l (*.f64 #s(literal 2 binary64) (*.f64 t t))) (neg.f64 (*.f64 l l))))))
(/.f64 (*.f64 (sqrt.f64 #s(literal 2 binary64)) (neg.f64 t)) (sqrt.f64 (-.f64 (*.f64 (fma.f64 #s(literal 2 binary64) (*.f64 t t) (*.f64 l l)) (/.f64 (-.f64 #s(literal 1 binary64) x) (fma.f64 #s(literal -1 binary64) x #s(literal -1 binary64)))) (*.f64 l l))))
(*.f64 t (/.f64 (neg.f64 (sqrt.f64 #s(literal 2 binary64))) (sqrt.f64 (fma.f64 (fma.f64 #s(literal 2 binary64) (*.f64 t t) (*.f64 l l)) (/.f64 (-.f64 #s(literal 1 binary64) x) (-.f64 #s(literal -1 binary64) x)) (neg.f64 (*.f64 l l))))))
(*.f64 (sqrt.f64 #s(literal 2 binary64)) (/.f64 (neg.f64 t) (sqrt.f64 (fma.f64 (fma.f64 #s(literal 2 binary64) (*.f64 t t) (*.f64 l l)) (/.f64 (-.f64 #s(literal 1 binary64) x) (-.f64 #s(literal -1 binary64) x)) (*.f64 l (neg.f64 l))))))
(neg.f64 (/.f64 (*.f64 (sqrt.f64 #s(literal 2 binary64)) t) (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 x #s(literal 1 binary64)) (-.f64 x #s(literal 1 binary64))) (+.f64 (*.f64 (neg.f64 l) (neg.f64 l)) (*.f64 #s(literal 2 binary64) (*.f64 t t)))) (*.f64 (neg.f64 l) (neg.f64 l))))))
(*.f64 (sqrt.f64 #s(literal 2 binary64)) (/.f64 (neg.f64 t) (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 x #s(literal 1 binary64)) (+.f64 x #s(literal -1 binary64))) (fma.f64 l l (*.f64 #s(literal 2 binary64) (*.f64 t t)))) (*.f64 l l)))))
(*.f64 (sqrt.f64 #s(literal 2 binary64)) (/.f64 (neg.f64 t) (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 x #s(literal 1 binary64)) (+.f64 x #s(literal -1 binary64))) (fma.f64 #s(literal 2 binary64) (*.f64 t t) (*.f64 l l))) (*.f64 l l)))))
(*.f64 (sqrt.f64 #s(literal 2 binary64)) (/.f64 (neg.f64 t) (sqrt.f64 (fma.f64 (+.f64 x #s(literal 1 binary64)) (/.f64 (fma.f64 #s(literal 2 binary64) (*.f64 t t) (*.f64 l l)) (+.f64 x #s(literal -1 binary64))) (neg.f64 (*.f64 l l))))))
(*.f64 t (/.f64 (neg.f64 (sqrt.f64 #s(literal 2 binary64))) (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 x #s(literal 1 binary64)) (+.f64 x #s(literal -1 binary64))) (fma.f64 #s(literal 2 binary64) (*.f64 t t) (*.f64 l l))) (*.f64 l l)))))
(neg.f64 (/.f64 (*.f64 (sqrt.f64 #s(literal 2 binary64)) (neg.f64 t)) (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 x #s(literal 1 binary64)) (-.f64 x #s(literal 1 binary64))) (+.f64 (*.f64 l l) (*.f64 #s(literal 2 binary64) (*.f64 (neg.f64 t) (neg.f64 t))))) (*.f64 l l)))))
(*.f64 (sqrt.f64 #s(literal 2 binary64)) (/.f64 t (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 x #s(literal 1 binary64)) (+.f64 x #s(literal -1 binary64))) (fma.f64 l l (*.f64 #s(literal 2 binary64) (*.f64 t t)))) (*.f64 l l)))))
(*.f64 (sqrt.f64 #s(literal 2 binary64)) (/.f64 t (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 x #s(literal 1 binary64)) (+.f64 x #s(literal -1 binary64))) (fma.f64 #s(literal 2 binary64) (*.f64 t t) (*.f64 l l))) (*.f64 l l)))))
(*.f64 (sqrt.f64 #s(literal 2 binary64)) (/.f64 t (sqrt.f64 (fma.f64 (+.f64 x #s(literal 1 binary64)) (/.f64 (fma.f64 #s(literal 2 binary64) (*.f64 t t) (*.f64 l l)) (+.f64 x #s(literal -1 binary64))) (neg.f64 (*.f64 l l))))))
(/.f64 (*.f64 (sqrt.f64 #s(literal 2 binary64)) t) (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 l #s(literal 1 binary64)) (-.f64 l #s(literal 1 binary64))) (+.f64 (*.f64 x x) (*.f64 #s(literal 2 binary64) (*.f64 t t)))) (*.f64 x x))))
(*.f64 (sqrt.f64 #s(literal 2 binary64)) (/.f64 t (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 #s(literal 1 binary64) l) (+.f64 l #s(literal -1 binary64))) (fma.f64 x x (*.f64 #s(literal 2 binary64) (*.f64 t t)))) (*.f64 x x)))))
(/.f64 (*.f64 (sqrt.f64 #s(literal 2 binary64)) t) (sqrt.f64 (-.f64 (/.f64 (*.f64 (+.f64 #s(literal 1 binary64) l) (fma.f64 #s(literal 2 binary64) (*.f64 t t) (*.f64 x x))) (+.f64 l #s(literal -1 binary64))) (*.f64 x x))))
(*.f64 t (/.f64 (sqrt.f64 #s(literal 2 binary64)) (sqrt.f64 (fma.f64 (+.f64 #s(literal 1 binary64) l) (/.f64 (fma.f64 #s(literal 2 binary64) (*.f64 t t) (*.f64 x x)) (+.f64 l #s(literal -1 binary64))) (neg.f64 (*.f64 x x))))))
(*.f64 t (/.f64 (sqrt.f64 #s(literal 2 binary64)) (sqrt.f64 (fma.f64 (+.f64 #s(literal 1 binary64) l) (/.f64 (fma.f64 #s(literal 2 binary64) (*.f64 t t) (*.f64 x x)) (+.f64 l #s(literal -1 binary64))) (*.f64 x (neg.f64 x))))))
(/.f64 (*.f64 (sqrt.f64 #s(literal 2 binary64)) x) (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 t #s(literal 1 binary64)) (-.f64 t #s(literal 1 binary64))) (+.f64 (*.f64 l l) (*.f64 #s(literal 2 binary64) (*.f64 x x)))) (*.f64 l l))))
(/.f64 (*.f64 (sqrt.f64 #s(literal 2 binary64)) x) (sqrt.f64 (fma.f64 (/.f64 (+.f64 t #s(literal 1 binary64)) (+.f64 t #s(literal -1 binary64))) (fma.f64 l l (*.f64 #s(literal 2 binary64) (*.f64 x x))) (neg.f64 (*.f64 l l)))))
(*.f64 x (/.f64 (sqrt.f64 #s(literal 2 binary64)) (sqrt.f64 (-.f64 (/.f64 (*.f64 (+.f64 t #s(literal 1 binary64)) (fma.f64 #s(literal 2 binary64) (*.f64 x x) (*.f64 l l))) (+.f64 t #s(literal -1 binary64))) (*.f64 l l)))))
(*.f64 x (/.f64 (sqrt.f64 #s(literal 2 binary64)) (sqrt.f64 (fma.f64 (/.f64 (+.f64 t #s(literal 1 binary64)) (+.f64 t #s(literal -1 binary64))) (fma.f64 #s(literal 2 binary64) (*.f64 x x) (*.f64 l l)) (neg.f64 (*.f64 l l))))))
(/.f64 (*.f64 (sqrt.f64 #s(literal 2 binary64)) x) (sqrt.f64 (fma.f64 (+.f64 t #s(literal 1 binary64)) (/.f64 (fma.f64 #s(literal 2 binary64) (*.f64 x x) (*.f64 l l)) (+.f64 t #s(literal -1 binary64))) (*.f64 l (neg.f64 l)))))
(/.f64 (*.f64 (sqrt.f64 #s(literal 2 binary64)) l) (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 x #s(literal 1 binary64)) (-.f64 x #s(literal 1 binary64))) (+.f64 (*.f64 t t) (*.f64 #s(literal 2 binary64) (*.f64 l l)))) (*.f64 t t))))
(/.f64 (*.f64 (sqrt.f64 #s(literal 2 binary64)) l) (sqrt.f64 (fma.f64 (/.f64 (+.f64 x #s(literal 1 binary64)) (+.f64 x #s(literal -1 binary64))) (fma.f64 t t (*.f64 #s(literal 2 binary64) (*.f64 l l))) (neg.f64 (*.f64 t t)))))
(/.f64 (*.f64 (sqrt.f64 #s(literal 2 binary64)) l) (sqrt.f64 (-.f64 (*.f64 (+.f64 x #s(literal 1 binary64)) (/.f64 (fma.f64 #s(literal 2 binary64) (*.f64 l l) (*.f64 t t)) (+.f64 x #s(literal -1 binary64)))) (*.f64 t t))))
(*.f64 l (/.f64 (sqrt.f64 #s(literal 2 binary64)) (sqrt.f64 (-.f64 (*.f64 (+.f64 x #s(literal 1 binary64)) (/.f64 (fma.f64 #s(literal 2 binary64) (*.f64 l l) (*.f64 t t)) (+.f64 x #s(literal -1 binary64)))) (*.f64 t t)))))
Symmetry

(abs l)

(negabs t)

Compiler

Compiled 30 to 18 computations (40% saved)

eval0.0ms (0%)

Compiler

Compiled 3 to 3 computations (0% saved)

prune1.0ms (0%)

Alt Table
Click to see full alt table
StatusAccuracyProgram
36.2%
(/.f64 (*.f64 (sqrt.f64 #s(literal 2 binary64)) t) (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 x #s(literal 1 binary64)) (-.f64 x #s(literal 1 binary64))) (+.f64 (*.f64 l l) (*.f64 #s(literal 2 binary64) (*.f64 t t)))) (*.f64 l l))))
Compiler

Compiled 60 to 36 computations (40% saved)

simplify4.0ms (0%)

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

Useful iterations: 0 (0.0ms)

IterNodesCost
025108
142108
252108
361108
474108
591108
Stop Event
saturated
Calls
Call 1
Inputs
(/.f64 (*.f64 (sqrt.f64 #s(literal 2 binary64)) t) (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 x #s(literal 1 binary64)) (-.f64 x #s(literal 1 binary64))) (+.f64 (*.f64 l l) (*.f64 #s(literal 2 binary64) (*.f64 t t)))) (*.f64 l l))))
Outputs
(/.f64 (*.f64 (sqrt.f64 #s(literal 2 binary64)) t) (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 x #s(literal 1 binary64)) (-.f64 x #s(literal 1 binary64))) (+.f64 (*.f64 l l) (*.f64 #s(literal 2 binary64) (*.f64 t t)))) (*.f64 l l))))
(/.f64 (*.f64 (sqrt.f64 #s(literal 2 binary64)) t) (sqrt.f64 (-.f64 (*.f64 (/.f64 (+.f64 x #s(literal 1 binary64)) (+.f64 x #s(literal -1 binary64))) (+.f64 (*.f64 l l) (*.f64 #s(literal 2 binary64) (*.f64 t t)))) (*.f64 l l))))

soundness0.0ms (0%)

Stop Event
fuel
Compiler

Compiled 30 to 19 computations (36.7% saved)

preprocess29.0ms (0.1%)

Remove

(negabs t)

(abs l)

Compiler

Compiled 360 to 226 computations (37.2% saved)

end0.0ms (0%)

Profiling

Loading profile data...