exp2 (problem 3.3.7)

Time bar (total: 23.4s)

analyze0.0ms (0%)

Algorithm
search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%50.4%49.6%0%0%0%0
100%50.4%0%49.6%0%0%0%1
Compiler

Compiled 13 to 10 computations (23.1% saved)

sample23.1s (98.7%)

Results
5.9s5814×2valid
883.0ms5722×2valid-sollya
1.1s2289×1valid
289.0ms2276×1valid-sollya
63.0ms153×0valid
14.0ms153×0valid-sollya
18.0ms92×2exit-sollya
2.0ms13×1exit-sollya
Sollya Eval
PtRival-outSollya-intervalSollya-pointstatusSollya statusRival itersollya-timecheck
(-1.2120868043510722e-24)1.4691544212819945e-48(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit10.143234#f
(1.2977832202295665e-140)1.6842412867094235e-280(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.143287#f
(1.4883626143858208e-201)0.0(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.09883499999999999#f
(-4.3826679664357864e-293)-0.0(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.15379700000000002#f
(2.5865969383439843e-229)0.0(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.072371#f
(5.7679676499151615e-43)3.326945081046783e-85(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit10.156023#f
(-3.8029083562440934e-296)-0.0(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.192351#f
(-1.748767917210329e-163)0.0(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.093349#f
(1.4552308287120138e-36)2.1176967648338545e-72(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit10.139343#f
(3.153444773033013e-167)0.0(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.136469#f
(-8.742721225317289e-257)0.0(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.14569100000000001#f
(-6.065574413510174e-304)-0.0(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.21955799999999998#f
(5.417692552328809e-31)2.935139259155904e-61(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit10.168104#f
(-5.473081582325949e-49)2.995462200679551e-97(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit10.181539#f
(-7.4170196391230115e-93)5.501218032713645e-185(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.17715999999999998#f
(6.832774604625907e-201)0.0(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.16364299999999998#f
(-1.384891864233823e-256)0.0(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.184975#f
(1.6758060625295767e-308)-0.0(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.08805#f
(3.974452890555914e-204)0.0(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.170938#f
(-8.782397986339537e-220)0.0(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.187662#f
(3.8586585970390455e-246)0.0(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.081876#f
(-2.235895191007312e-257)0.0(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.123938#f
(-2.2704833535531673e-258)0.0(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.165739#f
(2.013282895300796e-289)-0.0(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.08238599999999999#f
(1.0213786975331485e-48)1.0432144437745107e-96(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit10.151652#f
(-3.168429716386377e-255)0.0(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.196627#f
(7.616591840109667e-121)5.801247125882516e-241(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.127359#f
(4.467997311746278e-48)1.996299997777197e-95(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit10.083514#f
(-8.509502086703425e-252)0.0(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.184195#f
(-8.529998027469236e-41)7.276086634862905e-81(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit10.180213#f
(-1.8732707518612013e-232)0.0(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.157499#f
(3.5332721955199976e-230)0.0(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.109093#f
(-1.7962782993931573e-112)3.226615728870773e-224(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.156163#f
(1.891915226404918e-253)0.0(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.154837#f
(2.405230766883877e-122)5.785135041964804e-244(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.080999#f
(-2.622759493275274e-290)-0.0(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.09594799999999999#f
(3.4335519724711334e-293)-0.0(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.170461#f
(-5.245540178628297e-152)2.751569176560379e-303(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.145225#f
(1.9600473152189033e-197)0.0(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.152092#f
(-7.79331746282648e-166)0.0(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.15789999999999998#f
(2.3582270160481206e-178)0.0(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.159328#f
(1.8328260466549e-234)0.0(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.201132#f
(1.531389608368886e-222)0.0(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.08671899999999999#f
(-1.182150836858883e-159)1.39748e-318(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.158025#f
(2.0088966538417628e-137)4.0356657658166314e-274(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.129464#f
(-1.019096616135701e-82)1.0385579130192364e-164(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit10.14631#f
(2.4372863098425564e-113)5.940364556145946e-226(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.08102#f
(1.4657773186024854e-288)-0.0(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.083827#f
(-2.6959976202324404e-274)-0.0(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.093372#f
(5.496336148843947e-197)0.0(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.160102#f
(6.717913637624133e-195)0.0(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.10679999999999999#f
(6.785982248878693e-158)4.604955507e-315(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.12839399999999998#f
(-3.305572087402357e-224)0.0(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.184341#f
(-1.1785066709677244e-230)0.0(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.150829#f
(-2.168129456957225e-300)-0.0(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.096494#f
(-1.4691761541647916e-227)0.0(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.216641#f
(-8.613081931674719e-273)-0.0(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.158559#f
(1.4323313703176032e-55)2.0515731543959028e-110(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit10.08115599999999999#f
(3.6685703688336655e-187)0.0(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.12758299999999997#f
(1.2589047623297723e-228)0.0(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.158918#f
(-1.583040672280222e-307)-0.0(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.17832699999999999#f
(3.1788481803980105e-252)0.0(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.16050299999999998#f
(1.2260964778360104e-237)0.0(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.168249#f
(-6.332054060576673e-193)0.0(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.174142#f
(7.696496157933485e-293)-0.0(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.153762#f
(1.5899271705366296e-186)0.0(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.15727#f
(-7.254862086070353e-260)0.0(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.19836800000000002#f
(-2.6530329548082565e-243)0.0(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.094967#f
(1.7911277884600873e-237)0.0(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.135736#f
(-8.23350306199231e-195)0.0(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.175632#f
(2.3416616649614128e-139)5.483379353149856e-278(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.163536#f
(-3.201601396515433e-309)-0.0(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.181626#f
(1.4171564209634189e-300)-0.0(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.090044#f
(-1.6132580389538114e-143)2.6026015002490973e-286(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.09377#f
(2.516852043561545e-258)0.0(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.099502#f
(4.507803823286885e-280)-0.0(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.128729#f
(-5.568818410531875e-301)-0.0(+nan.0 +nan.0)+nan.0validexit25.0#f
(-8.345359135817946e-289)-0.0(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.215982#f
(-3.130911792719188e-291)-0.0(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.188589#f
(-1.4730859335298513e-215)0.0(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.184692#f
(-1.8634932117612246e-134)3.472606950280164e-268(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.179264#f
(5.189679068074028e-288)-0.0(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.08293400000000001#f
(6.25610037134261e-183)0.0(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.128208#f
(-4.016250565214543e-293)-0.0(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.1939#f
(1.9268993085454345e-278)-0.0(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.165731#f
(-1.037727533329591e-223)0.0(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.190067#f
(-1.7660253481138965e-248)0.0(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.092019#f
(6.74220264617254e-276)-0.0(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.154999#f
(4.795859606481349e-133)2.3000269365079436e-265(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.17085399999999998#f
(-1.9683036823835526e-41)3.874219386084653e-82(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit10.14240499999999998#f
(-4.384916899009858e-280)-0.0(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.189012#f
(-1.1457677914149391e-212)0.0(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.155224#f
(-6.20094458657125e-170)0.0(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.098786#f
(-4.9341583192925965e-288)-0.0(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.18128799999999998#f
(5.108277800928503e-232)0.0(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.08176#f
(4.076392468487087e-171)0.0(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.151015#f
(4.132448694865394e-43)1.70771322156947e-85(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit10.0843#f
(2.827859910397518e-246)0.0(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.139683#f
(-3.714172454773935e-267)-0.0(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.178835#f
(-9.560919316931029e-84)9.141117818486489e-167(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit10.17996700000000002#f
(-3.565235184044243e-227)0.0(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.15312#f
(2.95046870772158e-110)8.70526559524425e-220(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.085405#f
(3.718613540364202e-205)0.0(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.09459999999999999#f
(5.140275062333968e-110)2.642242771645248e-219(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.132049#f
(6.577229563698995e-145)4.325994873359608e-289(-5.421010862427522e-20 1.0842021724855044e-19)+nan.0validexit20.152265#f
Sollya timings
Total time spent in Sollya 1.2s
Bogosity

preprocess187.0ms (0.8%)

Algorithm
egg-herbie
Rules
113×fma-neg
65×fma-define
36×sub-neg
25×associate--r+
24×cancel-sign-sub-inv
Iterations

Useful iterations: 2 (0.0ms)

IterNodesCost
017128
145128
2105124
3248124
4465124
5604124
6637124
7642124
Stop Event
saturated
Calls
Call 1
Inputs
(+.f64 (-.f64 (exp.f64 x) #s(literal 2 binary64)) (exp.f64 (neg.f64 x)))
(+.f64 (-.f64 (exp.f64 x) #s(literal 2 binary64)) (exp.f64 (neg.f64 x)))
(+.f64 (-.f64 (exp.f64 (neg.f64 x)) #s(literal 2 binary64)) (exp.f64 (neg.f64 (neg.f64 x))))
(neg.f64 (+.f64 (-.f64 (exp.f64 (neg.f64 x)) #s(literal 2 binary64)) (exp.f64 (neg.f64 (neg.f64 x)))))
Outputs
(+.f64 (-.f64 (exp.f64 x) #s(literal 2 binary64)) (exp.f64 (neg.f64 x)))
(+.f64 (+.f64 (exp.f64 x) #s(literal -2 binary64)) (exp.f64 (neg.f64 x)))
(+.f64 (exp.f64 x) (+.f64 (exp.f64 (neg.f64 x)) #s(literal -2 binary64)))
(+.f64 (-.f64 (exp.f64 x) #s(literal 2 binary64)) (exp.f64 (neg.f64 x)))
(+.f64 (+.f64 (exp.f64 x) #s(literal -2 binary64)) (exp.f64 (neg.f64 x)))
(+.f64 (exp.f64 x) (+.f64 (exp.f64 (neg.f64 x)) #s(literal -2 binary64)))
(+.f64 (-.f64 (exp.f64 (neg.f64 x)) #s(literal 2 binary64)) (exp.f64 (neg.f64 (neg.f64 x))))
(+.f64 (+.f64 (exp.f64 x) #s(literal -2 binary64)) (exp.f64 (neg.f64 x)))
(+.f64 (exp.f64 x) (+.f64 (exp.f64 (neg.f64 x)) #s(literal -2 binary64)))
(neg.f64 (+.f64 (-.f64 (exp.f64 (neg.f64 x)) #s(literal 2 binary64)) (exp.f64 (neg.f64 (neg.f64 x)))))
(neg.f64 (-.f64 (exp.f64 (neg.f64 x)) (-.f64 #s(literal 2 binary64) (exp.f64 x))))
(-.f64 (neg.f64 (exp.f64 x)) (+.f64 (exp.f64 (neg.f64 x)) #s(literal -2 binary64)))
(-.f64 (-.f64 #s(literal 2 binary64) (exp.f64 (neg.f64 x))) (exp.f64 x))
(-.f64 (-.f64 #s(literal 2 binary64) (exp.f64 x)) (exp.f64 (neg.f64 x)))
Symmetry

(abs x)

Compiler

Compiled 9 to 7 computations (22.2% saved)

eval0.0ms (0%)

Compiler

Compiled 1 to 1 computations (0% saved)

prune17.0ms (0.1%)

Alt Table
Click to see full alt table
StatusAccuracyProgram
55.8%
(+.f64 (-.f64 (exp.f64 x) #s(literal 2 binary64)) (exp.f64 (neg.f64 x)))
Compiler

Compiled 18 to 14 computations (22.2% saved)

simplify5.0ms (0%)

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

Useful iterations: 0 (0.0ms)

IterNodesCost
01231
11931
22431
32731
42831
Stop Event
saturated
Calls
Call 1
Inputs
(+.f64 (-.f64 (exp.f64 x) #s(literal 2 binary64)) (exp.f64 (neg.f64 x)))
Outputs
(+.f64 (-.f64 (exp.f64 x) #s(literal 2 binary64)) (exp.f64 (neg.f64 x)))

soundness1.0ms (0%)

Stop Event
fuel
Compiler

Compiled 9 to 7 computations (22.2% saved)

preprocess93.0ms (0.4%)

Remove

(abs x)

Compiler

Compiled 96 to 70 computations (27.1% saved)

end0.0ms (0%)

Profiling

Loading profile data...