2frac (problem 3.3.1)

Time bar (total: 10.3s)

analyze4.0ms (0%)

Algorithm
search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%100%0%0%0%0%0
0%0%100%0%0%0%0%1
50%50%50%0%0%0%0%2
75%75%25%0%0%0%0%3
75%75%25%0%0%0%0%4
87.5%87.5%12.5%0%0%0%0%5
93.8%93.7%6.2%0%0%0%0%6
96.9%96.8%3.1%0%0%0%0%7
98.4%98.4%1.6%0%0%0%0%8
99.2%99.2%0.8%0%0%0%0%9
99.6%99.6%0.4%0%0%0%0%10
99.8%99.8%0.2%0%0%0%0%11
99.9%99.9%0.1%0%0%0%0%12
Compiler

Compiled 11 to 7 computations (36.4% saved)

sample10.2s (98.5%)

Results
580.0ms4297×0valid
352.0ms4281×0valid-sollya
1.1s3959×1valid
533.0ms3945×1valid-sollya
17.0ms16×0exit-sollya
7.0ms14×1exit-sollya
Sollya Eval
PtRival-outSollya-intervalSollya-pointstatusSollya statusRival itersollya-timecheck
(-2.190463452126907e-99)4.565243939719766e+98(+nan.0 +nan.0)+nan.0validexit05.0#f
(2.793910498922645e-157)-3.579212721329507e+156(-3.579212721329507e+156 -3.579212721329507e+156)+nan.0validexit00.096233#f
(-5.104641221039661e-244)1.9590015374211357e+243(1.9590015374211357e+243 1.9590015374211357e+243)+nan.0validexit00.23985900000000002#f
(-2.247791067015941e-180)4.4488120567520173e+179(4.4488120567520173e+179 4.4488120567520173e+179)+nan.0validexit00.243231#f
(4.5103539124877023e+179)-0.0(-4.180544565216833e-199 2.0902722826084166e-199)+nan.0validexit10.10478699999999999#f
(-2.9831291336848346e+146)-1.1237142622362059e-293(-5.426657103235053e-166 2.7133285516175262e-166)+nan.0validexit10.156725#f
(1.239742071347395e+212)-0.0(-1.2882297539194267e-231 6.441148769597133e-232)+nan.0validexit10.164879#f
(3.3073010140136403e-95)-3.0236135016523045e+94(+nan.0 +nan.0)+nan.0validexit05.0#f
(-4.442101751377182e+209)-0.0(-3.2978681700337323e-229 1.6489340850168661e-229)+nan.0validexit10.197639#f
(-1.0054368492257876e-253)9.945925502631277e+252(9.945925502631277e+252 9.945925502631277e+252)+nan.0validexit00.223918#f
(-9.378221364609941e-274)1.0663002728573277e+273(1.0663002728573277e+273 1.0663002728573277e+273)+nan.0validexit00.19222999999999998#f
(-5.277025868142579e+31)-3.591050841061862e-64(-2.6727647100921956e-51 1.3363823550460978e-51)+nan.0validexit10.09481300000000001#f
(-4.875555221341344e-149)2.0510484541797147e+148(2.0510484541797147e+148 2.0510484541797147e+148)+nan.0validexit00.114425#f
(2.37330516368991e+244)-0.0(+nan.0 +nan.0)+nan.0validexit15.0#f
(-1.1555557023703513e+106)-7.488903422494351e-213(-1.1818212630765742e-125 5.909106315382871e-126)+nan.0validexit10.099563#f
(1.0173048674743106e-223)-9.829894970253373e+222(-9.829894970253373e+222 -9.829894970253373e+222)+nan.0validexit00.092532#f
(-6.504520751156382e-260)1.537392281855998e+259(1.537392281855998e+259 1.537392281855998e+259)+nan.0validexit00.183871#f
(-13722251071.85252)-5.310669535171479e-21(-5.310669541581844e-21 -5.310669528960069e-21)+nan.0validexit10.17006200000000002#f
(1.639421211244804e-290)-6.099713686397318e+289(-6.099713686397318e+289 -6.099713686397318e+289)+nan.0validexit00.101455#f
(57.164080121397305)-0.0003007612746450416(-0.00030076127464504166 -0.0003007612746450416)+nan.0validexit00.159499#f
(3.2251364161149004e+70)-9.613993449686291e-142(-3.9272747722381812e-90 1.9636373861190906e-90)+nan.0validexit10.193155#f
(-8.667514563086945e+288)-0.0(-1.1125369292536007e-308 1.1125369292536007e-308)+nan.0validexit10.161958#f
(-2.0654760392318104e+68)-2.344011173035416e-137(-5.026911708464872e-88 5.026911708464872e-88)+nan.0validexit10.19288000000000002#f
(1.7418245571263292e-103)-5.741106335357937e+102(-5.741106335357937e+102 -5.741106335357937e+102)+nan.0validexit00.0944#f
(-1.772695271355507e+174)-0.0(-1.0959046745042015e-193 5.479523372521008e-194)+nan.0validexit10.099157#f
(2.018324144674823e+199)-0.0(-8.498541562088548e-219 2.8328471873628494e-219)+nan.0validexit10.198103#f
(2.504762410614697e-237)-3.992394630972559e+236(-3.992394630972559e+236 -3.992394630972559e+236)+nan.0validexit00.106899#f
(-4.089927729492021e-208)2.445030978882853e+207(+nan.0 +nan.0)+nan.0validexit05.0#f
(7.933350877014242e+292)-0.0(-2.716154612436e-312 1.35807730622e-312)+nan.0validexit10.18343600000000002#f
(5.677741605727535e-140)-1.7612636668622433e+139(-1.7612636668622433e+139 -1.7612636668622433e+139)+nan.0validexit00.181109#f
Sollya timings
Total time spent in Sollya 909.0ms
Bogosity

preprocess88.0ms (0.8%)

Algorithm
egg-herbie
Rules
89×fma-neg
39×fma-define
24×distribute-lft-neg-in
23×sub-neg
20×cancel-sign-sub-inv
Iterations

Useful iterations: 2 (0.0ms)

IterNodesCost
017144
134128
270124
3138124
4236124
5334124
6411124
7456124
8473124
9475124
Stop Event
saturated
Calls
Call 1
Inputs
(-.f64 (/.f64 #s(literal 1 binary64) (+.f64 x #s(literal 1 binary64))) (/.f64 #s(literal 1 binary64) x))
(-.f64 (/.f64 #s(literal 1 binary64) (+.f64 x #s(literal 1 binary64))) (/.f64 #s(literal 1 binary64) x))
(-.f64 (/.f64 #s(literal 1 binary64) (+.f64 (neg.f64 x) #s(literal 1 binary64))) (/.f64 #s(literal 1 binary64) (neg.f64 x)))
(neg.f64 (-.f64 (/.f64 #s(literal 1 binary64) (+.f64 (neg.f64 x) #s(literal 1 binary64))) (/.f64 #s(literal 1 binary64) (neg.f64 x))))
Outputs
(-.f64 (/.f64 #s(literal 1 binary64) (+.f64 x #s(literal 1 binary64))) (/.f64 #s(literal 1 binary64) x))
(-.f64 (/.f64 #s(literal 1 binary64) (+.f64 #s(literal 1 binary64) x)) (/.f64 #s(literal 1 binary64) x))
(+.f64 (/.f64 #s(literal 1 binary64) (+.f64 #s(literal 1 binary64) x)) (/.f64 #s(literal -1 binary64) x))
(-.f64 (/.f64 #s(literal 1 binary64) (+.f64 x #s(literal 1 binary64))) (/.f64 #s(literal 1 binary64) x))
(-.f64 (/.f64 #s(literal 1 binary64) (+.f64 #s(literal 1 binary64) x)) (/.f64 #s(literal 1 binary64) x))
(+.f64 (/.f64 #s(literal 1 binary64) (+.f64 #s(literal 1 binary64) x)) (/.f64 #s(literal -1 binary64) x))
(-.f64 (/.f64 #s(literal 1 binary64) (+.f64 (neg.f64 x) #s(literal 1 binary64))) (/.f64 #s(literal 1 binary64) (neg.f64 x)))
(-.f64 (/.f64 #s(literal 1 binary64) (+.f64 #s(literal 1 binary64) (neg.f64 x))) (/.f64 #s(literal 1 binary64) (neg.f64 x)))
(+.f64 (/.f64 #s(literal 1 binary64) x) (/.f64 #s(literal 1 binary64) (-.f64 #s(literal 1 binary64) x)))
(neg.f64 (-.f64 (/.f64 #s(literal 1 binary64) (+.f64 (neg.f64 x) #s(literal 1 binary64))) (/.f64 #s(literal 1 binary64) (neg.f64 x))))
(neg.f64 (-.f64 (/.f64 #s(literal 1 binary64) (+.f64 #s(literal 1 binary64) (neg.f64 x))) (/.f64 #s(literal 1 binary64) (neg.f64 x))))
(+.f64 (neg.f64 (/.f64 #s(literal 1 binary64) (-.f64 #s(literal 1 binary64) x))) (/.f64 #s(literal -1 binary64) x))
(+.f64 (/.f64 #s(literal -1 binary64) x) (/.f64 #s(literal -1 binary64) (-.f64 #s(literal 1 binary64) x)))
(+.f64 (/.f64 #s(literal -1 binary64) x) (/.f64 #s(literal 1 binary64) (+.f64 x #s(literal -1 binary64))))
Compiler

Compiled 10 to 6 computations (40% saved)

eval0.0ms (0%)

Compiler

Compiled 1 to 1 computations (0% saved)

prune1.0ms (0%)

Alt Table
Click to see full alt table
StatusAccuracyProgram
76.4%
(-.f64 (/.f64 #s(literal 1 binary64) (+.f64 x #s(literal 1 binary64))) (/.f64 #s(literal 1 binary64) x))
Compiler

Compiled 20 to 12 computations (40% saved)

simplify19.0ms (0.2%)

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

Useful iterations: 0 (0.0ms)

IterNodesCost
01031
11931
22731
33331
44031
55231
66831
Stop Event
saturated
Calls
Call 1
Inputs
(-.f64 (/.f64 #s(literal 1 binary64) (+.f64 x #s(literal 1 binary64))) (/.f64 #s(literal 1 binary64) x))
Outputs
(-.f64 (/.f64 #s(literal 1 binary64) (+.f64 x #s(literal 1 binary64))) (/.f64 #s(literal 1 binary64) x))
(-.f64 (/.f64 #s(literal 1 binary64) (+.f64 #s(literal 1 binary64) x)) (/.f64 #s(literal 1 binary64) x))
(+.f64 (/.f64 #s(literal 1 binary64) (+.f64 #s(literal 1 binary64) x)) (/.f64 #s(literal -1 binary64) x))

soundness1.0ms (0%)

Stop Event
fuel
Compiler

Compiled 10 to 7 computations (30% saved)

preprocess38.0ms (0.4%)

Compiler

Compiled 40 to 26 computations (35% saved)

end0.0ms (0%)

Profiling

Loading profile data...