Toniolo and Linder, Equation (7)

Time bar (total: 29.8s)

analyze433.0ms (1.5%)

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)

sample29.1s (97.8%)

Results
1.6s5336×0valid
543.0ms5327×0valid-sollya
802.0ms2714×0invalid
437.0ms2690×0invalid-sollya
1.5s2168×1valid
303.0ms2162×1valid-sollya
653.0ms1242×1invalid
207.0ms1230×1invalid-sollya
678.0ms752×2valid
127.0ms749×2valid-sollya
330.0ms524×2invalid
92.0ms518×2invalid-sollya
6.0ms33×0exit-sollya
8.0ms18×1exit-sollya
1.0ms2exit-sollya
Sollya Eval
PtRival-outSollya-intervalSollya-pointstatusSollya statusRival itersollya-timecheck
(-5.20669923130458e-18 -3.1825546419214414e+245 4.206144815561353e+219)#f(+nan.0 +nan.0)+nan.0invalidexit00.188363#f
(4.008083269259686e-59 -6.1882534956467445e+81 3.509808003917725e+56)#f(+nan.0 +nan.0)+nan.0invalidexit00.10817700000000001#f
(-1.0394753454354162e+89 -1.905290025257624e+253 -1.2236941274959625e-168)#f(+nan.0 +nan.0)+nan.0invalidexit10.239913#f
(1.5623859105571175e-6 1.2277243471246236e-136 1.7197528873374646e-295)#f(+nan.0 +nan.0)+nan.0invalidexit00.17973899999999998#f
(-7.8704154884342e+157 -4.9142994044003626e+54 -5.177928581031458e-262)#f(+nan.0 +nan.0)+nan.0invalidexit10.22908#f
(-9.797396438606611e+110 3.738584828233843e+206 -1.122473662197442e-106)#f(+nan.0 +nan.0)+nan.0invalidexit10.195718#f
(-4.375894757978086e-26 8.41753763944704e-181 3.4529771162453505e-9)#f(+nan.0 +nan.0)+nan.0invalidexit00.204902#f
(1.5346315106109066e-68 -1.6374417615815958e+258 4.1263199502886675e-6)#f(+nan.0 +nan.0)+nan.0invalidexit00.23952#f
(-6.744285968654362e-23 -2.2621324638980172e-291 2.5963262328913317e-153)#f(+nan.0 +nan.0)+nan.0invalidexit00.108637#f
(-6.166800148664245e+304 -6.324420296113991e+246 1.0652362532353923e+75)#f(+nan.0 +nan.0)+nan.0invalidexit20.21161#f
(1.5656094178027918e-10 2.3613333389789643e+266 4.927832464561768e+202)#f(+nan.0 +nan.0)+nan.0invalidexit00.165208#f
(-1.8026850118316348e+194 3.026999474280908e+287 -1.8458337240724695e-263)#f(+nan.0 +nan.0)+nan.0invalidexit10.11602#f
(1.2089013755699376e-68 6.50107732488993e-111 -4.2898822958057435e-165)#f(+nan.0 +nan.0)+nan.0invalidexit00.166501#f
(-1.0823415260532426e+20 -6.012088667355016e-68 -8.790792478677492e+115)-1.0(-1.0 -1.0)+nan.0validexit00.156544#f
(-2.635934305284033e+263 4.56397884249293e+59 -1.2353678296916734e-188)#f(+nan.0 +nan.0)+nan.0invalidexit20.10998#f
(-3.5527390293322105e+205 1.1865046637875508e+284 -2.5759686428724677e-251)#f(+nan.0 +nan.0)+nan.0invalidexit10.109979#f
(7.20032092291941e-14 -17686623892081248.0 5.107281291206248e-295)#f(+nan.0 +nan.0)+nan.0invalidexit00.085859#f
(-4.1181043728458856e+175 9.093754089943286e+288 -8.360590588609859e-253)#f(+nan.0 +nan.0)+nan.0invalidexit10.194628#f
(4.12809062317013e+148 7.554295902863506e-96 5.871949401901202e-29)1.0(1.0 1.0)+nan.0validexit00.359912#f
(-6.581123442270188e+294 -4.8565699652075225e+30 -8.297752458247283e-219)#f(+nan.0 +nan.0)+nan.0invalidexit20.180613#f
(8.621196456776336e+295 -8144250812.7463045 -0.0002229611215599984)-1.0(+nan.0 +nan.0)+nan.0validexit10.167646#f
(-271529775244694720.0 7.12367629715004e+30 2.885255216610757e-127)#f(+nan.0 +nan.0)+nan.0invalidexit00.20733500000000002#f
(-1.7053326871265159e+186 -3.41978658045777e+251 5.2763977890095934e+51)#f(+nan.0 +nan.0)+nan.0invalidexit10.11368400000000001#f
(2.1734125287927485e+26 -3.3424432439052105e+209 -1.3644417793019774e+125)-6.018136732243952e-72(+nan.0 +nan.0)+nan.0validexit10.185802#f
(-2.6310392972306747e-47 40010845813437555000.0 1.237317519464795e-66)#f(+nan.0 +nan.0)+nan.0invalidexit00.164246#f
(1.6039522265376775e-53 5.57275977615387e-19 -211.52513064510742)#f(+nan.0 +nan.0)+nan.0invalidexit00.21516300000000002#f
(3.5160569907900376e+196 4.785857385116308e+112 -7.523478318459332e-115)-2.947724382800576e-129(+nan.0 +nan.0)+nan.0validexit20.113284#f
(7.863591853604385e-17 6.049890618367802e+220 3.3556049162232076)#f(+nan.0 +nan.0)+nan.0invalidexit00.10861699999999999#f
(-2.52725652628011e-46 2.7800341318774824e+101 3.2863610520160264e-110)#f(+nan.0 +nan.0)+nan.0invalidexit00.171981#f
(-2.8313132118976256e+20 1.218816541292324e-37 -1.2894292196388365e-86)#f(+nan.0 +nan.0)+nan.0invalidexit00.16855599999999998#f
(2.26066024245683e+297 -1.607340265506143e-151 -5.564903742189911e-47)-1.0(-1.0 -1.0)+nan.0validexit00.250511#f
(-8887.594697959958 -6.1858504041899874e+258 -1.7177843899915374e+28)#f(+nan.0 +nan.0)+nan.0invalidexit00.256659#f
(6.729986594496843e+233 5.627822820290544e-240 -7.658842215410442e-156)-1.0(-1.0 -1.0)+nan.0validexit00.26866999999999996#f
(3.1969721253229174e+239 8.926974777044527e-126 1.4182037058328892e-231)1.0(+nan.0 +nan.0)+nan.0validexit20.2109#f
(3.4918092570486913e-72 5.660685873642967e+226 3.2425989936580864e+59)#f(+nan.0 +nan.0)+nan.0invalidexit00.143338#f
(-1.0202199470322472e+38 -1.9449566868042645e+206 4.3236126832777797e-26)#f(+nan.0 +nan.0)+nan.0invalidexit10.198457#f
(-2.0996041232579914e+117 1.5600712087107295e+208 -4.404062748972083e-135)#f(+nan.0 +nan.0)+nan.0invalidexit10.10983#f
(-4.3863154033015036e+46 1.1741622418812446e+168 3.5799010519077197e-25)#f(+nan.0 +nan.0)+nan.0invalidexit10.19467299999999998#f
(8.446422976517055e+100 -1.1168601338443147e-150 -1.9106881087817774e+211)-1.0(-1.0 -1.0)+nan.0validexit00.257125#f
(-5.2797929103040794e+182 5.215913759874858e+144 8.239160672631863e+70)1.0(+nan.0 +nan.0)+nan.0validexit10.23394#f
(-3.703630633799456e+62 -5.105188153079547e-163 -1.2679813257537424e+293)-1.0(-1.0 -1.0)+nan.0validexit00.298373#f
(-1.5786188844696267e+129 -2.956232768053208e+61 -1.9631628074133912e-206)#f(+nan.0 +nan.0)+nan.0invalidexit10.2203#f
(-0.17060821946388607 2.1017142596588437e-31 -4.7190142262468354e-45)#f(+nan.0 +nan.0)+nan.0invalidexit00.205847#f
(-2.2549655627952838e+219 7.536627434228443e+39 2.2345445181495272e+176)1.0(1.0 1.0)+nan.0validexit00.23802900000000002#f
(2.040172530325387e+170 -6.722572736002771e+180 -5.771786641735861e+149)-1.0(+nan.0 +nan.0)+nan.0validexit10.184804#f
(3.20095709618046e-51 -1.4899858725684314e-308 -5.0098605230057845e+119)#f(+nan.0 +nan.0)+nan.0invalidexit00.182203#f
(4.2166777914919116e-66 -4.805264327928281e-243 -1.9424790551931568e-187)#f(+nan.0 +nan.0)+nan.0invalidexit00.230879#f
(1.0312601013001792e+37 -5.779370258065544e+182 -9.177108179286714e-291)-0.0(+nan.0 +nan.0)+nan.0validexit10.239186#f
(-2.50400687100061e-22 9.67044157114189e+163 -5.020636068425949e+45)#f(+nan.0 +nan.0)+nan.0invalidexit00.108557#f
(1.891293021689152e+242 -1.086797553319367e+292 1.2135740074666118e-180)0.0(+nan.0 +nan.0)+nan.0validexit20.112579#f
(1.2997758589577525e-65 3.5489719431525477e-132 1.2616495447760978e+207)#f(+nan.0 +nan.0)+nan.0invalidexit00.206106#f
(-2.7728166421755756e-53 -2.854691666236447e-128 4.94521922173583e-212)#f(+nan.0 +nan.0)+nan.0invalidexit00.101934#f
(-8.612116222755236e+133 -1.6993358778864968e+170 3.229834497416504e-278)#f(+nan.0 +nan.0)+nan.0invalidexit10.238538#f
(-1.1930616414757294e+263 -1.5847177963707421e+43 -2.965433253984221e-206)#f(+nan.0 +nan.0)+nan.0invalidexit20.108561#f
(5.881740956715788e+102 6.047169512754462e-269 -2.483336730031976e+87)-1.0(-1.0 -1.0)+nan.0validexit00.356952#f
(7.057380108671389e+136 -1.3748926223312642e-243 8.804209581960065e-209)1.0(1.0 1.0)+nan.0validexit00.161193#f
(2.4065891283259784e+61 -1.5467107673129448e+239 -3.12942754938924e-196)-0.0(+nan.0 +nan.0)+nan.0validexit15.0#f
(-4.4804849911268243e+253 2.866094118524299e+156 1.1807289779250182e-44)#f(+nan.0 +nan.0)+nan.0invalidexit20.117372#f
(-2.382969365251064e-40 2.4551257395573674e+281 -2.3349090046324766e-207)#f(+nan.0 +nan.0)+nan.0invalidexit00.10268#f
(-5.454315508376397e+267 9.19692611652329e+155 -7.082208997542134e-275)#f(+nan.0 +nan.0)+nan.0invalidexit20.225181#f
Sollya timings
Total time spent in Sollya 1.7s
Bogosity

preprocess163.0ms (0.5%)

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
37.8%
(/.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)

simplify5.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))))

soundness1.0ms (0%)

Stop Event
fuel
Compiler

Compiled 30 to 19 computations (36.7% saved)

preprocess53.0ms (0.2%)

Remove

(negabs t)

(abs l)

Compiler

Compiled 360 to 226 computations (37.2% saved)

end0.0ms (0%)

Profiling

Loading profile data...