Commute and associate

Time bar (total: 8.2s)

analyze6.0ms (0.1%)

Algorithm
1×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 15 to 9 computations (40% saved)

sample7.7s (93.7%)

Results
1.4s5851×2valid
628.0ms5851×2valid-sollya
285.0ms1858×1valid
148.0ms1857×1valid-sollya
64.0ms541×3valid-sollya
170.0ms541×3valid
0.0ms6×0valid-sollya
0.0ms6×0valid
0.0ms1×1exit-sollya
Sollya Eval
PtRival-outSollya-intervalSollya-pointstatusSollya statusRival itersollya-timecheck
(2.274567762453646e-210 8.774492392293905e-152 9.331465119704529e-103)-0.0(-1.9362959574246591e-121 9.681479787123296e-122)+nan.0validexit10.17180499999999999#f
Sollya timings
Total time spent in Sollya 840.0ms
Bogosity

preprocess474.0ms (5.8%)

Algorithm
1×egg-herbie
Rules
1242×associate-+r+
1197×associate-+r-
1191×associate-+l+
848×fma-neg
670×fma-define
Iterations

Useful iterations: 1 (0.0ms)

IterNodesCost
046539
114011
255111
3174511
4320711
5391511
6392611
7393411
8393411
9431611
10431611
11431611
12431611
Stop Event
1×node limit
Calls
Call 1
Inputs
(-.f64 (+.f64 (+.f64 x y) z) (+.f64 x (+.f64 y z)))
(-.f64 (+.f64 (+.f64 x y) z) (+.f64 x (+.f64 y z)))
(-.f64 (+.f64 (+.f64 (neg.f64 x) y) z) (+.f64 (neg.f64 x) (+.f64 y z)))
(-.f64 (+.f64 (+.f64 x (neg.f64 y)) z) (+.f64 x (+.f64 (neg.f64 y) z)))
(-.f64 (+.f64 (+.f64 x y) (neg.f64 z)) (+.f64 x (+.f64 y (neg.f64 z))))
(neg.f64 (-.f64 (+.f64 (+.f64 (neg.f64 x) y) z) (+.f64 (neg.f64 x) (+.f64 y z))))
(neg.f64 (-.f64 (+.f64 (+.f64 x (neg.f64 y)) z) (+.f64 x (+.f64 (neg.f64 y) z))))
(neg.f64 (-.f64 (+.f64 (+.f64 x y) (neg.f64 z)) (+.f64 x (+.f64 y (neg.f64 z)))))
(-.f64 (+.f64 (+.f64 y x) z) (+.f64 y (+.f64 x z)))
(-.f64 (+.f64 (+.f64 z y) x) (+.f64 z (+.f64 y x)))
(-.f64 (+.f64 (+.f64 x z) y) (+.f64 x (+.f64 z y)))
Outputs
(-.f64 (+.f64 (+.f64 x y) z) (+.f64 x (+.f64 y z)))
(+.f64 (+.f64 x y) (-.f64 z (+.f64 y (+.f64 x z))))
#s(literal 0 binary64)
(-.f64 (+.f64 (+.f64 x y) z) (+.f64 x (+.f64 y z)))
(+.f64 (+.f64 x y) (-.f64 z (+.f64 y (+.f64 x z))))
#s(literal 0 binary64)
(-.f64 (+.f64 (+.f64 (neg.f64 x) y) z) (+.f64 (neg.f64 x) (+.f64 y z)))
(+.f64 (+.f64 x y) (-.f64 z (+.f64 y (+.f64 x z))))
#s(literal 0 binary64)
(-.f64 (+.f64 (+.f64 x (neg.f64 y)) z) (+.f64 x (+.f64 (neg.f64 y) z)))
(+.f64 (+.f64 x y) (-.f64 z (+.f64 y (+.f64 x z))))
#s(literal 0 binary64)
(-.f64 (+.f64 (+.f64 x y) (neg.f64 z)) (+.f64 x (+.f64 y (neg.f64 z))))
(+.f64 (+.f64 x y) (-.f64 z (+.f64 y (+.f64 x z))))
#s(literal 0 binary64)
(neg.f64 (-.f64 (+.f64 (+.f64 (neg.f64 x) y) z) (+.f64 (neg.f64 x) (+.f64 y z))))
(+.f64 (+.f64 x y) (-.f64 z (+.f64 y (+.f64 x z))))
#s(literal 0 binary64)
(neg.f64 (-.f64 (+.f64 (+.f64 x (neg.f64 y)) z) (+.f64 x (+.f64 (neg.f64 y) z))))
(+.f64 (+.f64 x y) (-.f64 z (+.f64 y (+.f64 x z))))
#s(literal 0 binary64)
(neg.f64 (-.f64 (+.f64 (+.f64 x y) (neg.f64 z)) (+.f64 x (+.f64 y (neg.f64 z)))))
(+.f64 (+.f64 x y) (-.f64 z (+.f64 y (+.f64 x z))))
#s(literal 0 binary64)
(-.f64 (+.f64 (+.f64 y x) z) (+.f64 y (+.f64 x z)))
(+.f64 (+.f64 x y) (-.f64 z (+.f64 y (+.f64 x z))))
#s(literal 0 binary64)
(-.f64 (+.f64 (+.f64 z y) x) (+.f64 z (+.f64 y x)))
(+.f64 (+.f64 x y) (-.f64 z (+.f64 y (+.f64 x z))))
#s(literal 0 binary64)
(-.f64 (+.f64 (+.f64 x z) y) (+.f64 x (+.f64 z y)))
(+.f64 (+.f64 x y) (-.f64 z (+.f64 y (+.f64 x z))))
#s(literal 0 binary64)
Symmetry

(abs x)

(abs y)

(abs z)

(negabs x)

(negabs y)

(negabs z)

(sort x y z)

Compiler

Compiled 14 to 8 computations (42.9% saved)

eval0.0ms (0%)

Compiler

Compiled 3 to 3 computations (0% saved)

prune1.0ms (0%)

Alt Table
Click to see full alt table
StatusAccuracyProgram
100.0%
(-.f64 (+.f64 (+.f64 x y) z) (+.f64 x (+.f64 y z)))
Compiler

Compiled 28 to 16 computations (42.9% saved)

simplify3.0ms (0%)

Algorithm
1×egg-herbie
Rules
10×+-commutative
6×sub-neg
5×*-commutative
5×neg-sub0
5×neg-mul-1
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
01449
12149
23049
34249
45349
55949
66149
Stop Event
1×saturated
Calls
Call 1
Inputs
(-.f64 (+.f64 (+.f64 x y) z) (+.f64 x (+.f64 y z)))
Outputs
(-.f64 (+.f64 (+.f64 x y) z) (+.f64 x (+.f64 y z)))

soundness0.0ms (0%)

Stop Event
1×fuel
Compiler

Compiled 14 to 8 computations (42.9% saved)

preprocess36.0ms (0.4%)

Remove

(sort x y z)

(negabs z)

(negabs y)

(negabs x)

(abs z)

(abs y)

(abs x)

Compiler

Compiled 448 to 256 computations (42.9% saved)

end0.0ms (0%)

Profiling

Loading profile data...