Expression 1, p15

Time bar (total: 5.6s)

analyze0.0ms (0%)

Algorithm
1×search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%0%100%0%0%0%0
100%0%0%100%0%0%0%1
Compiler

Compiled 53 to 38 computations (28.3% saved)

Precisions
Click to see histograms. Total time spent on operations: 0.0ms
Operation ival-add, time spent: 0.0ms, 0.0% of total-time
Operation ival-and, time spent: 0.0ms, 0.0% of total-time
Operation ival-<=, time spent: 0.0ms, 0.0% of total-time
Operation const, time spent: 0.0ms, 0.0% of total-time

sample3.9s (69.4%)

Results
3.6s8255×0valid
0.0ms1×0valid
Precisions
Click to see histograms. Total time spent on operations: 1.6s
Operation ival-add, time spent: 826.0ms, 53.0% of total-time
Operation ival-<=, time spent: 588.0ms, 37.0% of total-time
Operation ival-and, time spent: 96.0ms, 6.0% of total-time
Operation const, time spent: 60.0ms, 4.0% of total-time
Bogosity

preprocess295.0ms (5.2%)

Algorithm
1×egg-herbie
Rules
1428×sub-neg
1366×distribute-neg-in
1222×distribute-rgt-in
846×associate-+r+
842×fma-neg
FPErrors
Click to see full error table
Ground TruthOverpredictionsExampleUnderpredictionsExampleSubexpression
00-0-b
00-0-(+.f64 (+.f64 (+.f64 (+.f64 e d) c) b) a)
00-0-c
00-0-e
00-0-d
00-0-(+.f64 e d)
00-0-a
00-0-(+.f64 (+.f64 e d) c)
00-0-(+.f64 (+.f64 (+.f64 e d) c) b)
Iterations

Useful iterations: 2 (0.0ms)

IterNodesCost
078908
1228896
2797880
33183880
46545880
57498880
67853880
77976880
Stop Event
1×node limit
Calls
Call 1
Inputs
(+.f64 (+.f64 (+.f64 (+.f64 e d) c) b) a)
(+.f64 (+.f64 (+.f64 (+.f64 e d) c) b) a)
(+.f64 (+.f64 (+.f64 (+.f64 e d) c) b) (neg.f64 a))
(+.f64 (+.f64 (+.f64 (+.f64 e d) c) (neg.f64 b)) a)
(+.f64 (+.f64 (+.f64 (+.f64 e d) (neg.f64 c)) b) a)
(+.f64 (+.f64 (+.f64 (+.f64 e (neg.f64 d)) c) b) a)
(+.f64 (+.f64 (+.f64 (+.f64 (neg.f64 e) d) c) b) a)
(neg.f64 (+.f64 (+.f64 (+.f64 (+.f64 e d) c) b) (neg.f64 a)))
(neg.f64 (+.f64 (+.f64 (+.f64 (+.f64 e d) c) (neg.f64 b)) a))
(neg.f64 (+.f64 (+.f64 (+.f64 (+.f64 e d) (neg.f64 c)) b) a))
(neg.f64 (+.f64 (+.f64 (+.f64 (+.f64 e (neg.f64 d)) c) b) a))
(neg.f64 (+.f64 (+.f64 (+.f64 (+.f64 (neg.f64 e) d) c) b) a))
(+.f64 (+.f64 (+.f64 (+.f64 e d) c) a) b)
(+.f64 (+.f64 (+.f64 (+.f64 e d) a) b) c)
(+.f64 (+.f64 (+.f64 (+.f64 e a) c) b) d)
(+.f64 (+.f64 (+.f64 (+.f64 a d) c) b) e)
(+.f64 (+.f64 (+.f64 (+.f64 e d) b) c) a)
(+.f64 (+.f64 (+.f64 (+.f64 e b) c) d) a)
(+.f64 (+.f64 (+.f64 (+.f64 b d) c) e) a)
(+.f64 (+.f64 (+.f64 (+.f64 e c) d) b) a)
(+.f64 (+.f64 (+.f64 (+.f64 c d) e) b) a)
(+.f64 (+.f64 (+.f64 (+.f64 d e) c) b) a)
Outputs
(+.f64 (+.f64 (+.f64 (+.f64 e d) c) b) a)
(+.f64 (+.f64 e (+.f64 d c)) (+.f64 b a))
(+.f64 d (+.f64 (+.f64 e c) (+.f64 b a)))
(+.f64 e (+.f64 (+.f64 d c) (+.f64 b a)))
(+.f64 c (+.f64 e (+.f64 d (+.f64 b a))))
(+.f64 (+.f64 (+.f64 (+.f64 e d) c) b) a)
(+.f64 (+.f64 e (+.f64 d c)) (+.f64 b a))
(+.f64 d (+.f64 (+.f64 e c) (+.f64 b a)))
(+.f64 e (+.f64 (+.f64 d c) (+.f64 b a)))
(+.f64 c (+.f64 e (+.f64 d (+.f64 b a))))
(+.f64 (+.f64 (+.f64 (+.f64 e d) c) b) (neg.f64 a))
(-.f64 (+.f64 (+.f64 e d) (+.f64 c b)) a)
(+.f64 e (+.f64 (+.f64 d c) (-.f64 b a)))
(+.f64 e (+.f64 d (+.f64 c (-.f64 b a))))
(+.f64 (+.f64 (+.f64 (+.f64 e d) c) (neg.f64 b)) a)
(+.f64 a (-.f64 (+.f64 e (+.f64 d c)) b))
(+.f64 a (+.f64 e (+.f64 d (-.f64 c b))))
(+.f64 e (+.f64 (+.f64 d a) (-.f64 c b)))
(+.f64 (+.f64 (+.f64 (+.f64 e d) (neg.f64 c)) b) a)
(+.f64 a (+.f64 b (-.f64 (+.f64 e d) c)))
(+.f64 a (+.f64 b (+.f64 e (-.f64 d c))))
(+.f64 (+.f64 d a) (+.f64 e (-.f64 b c)))
(+.f64 e (+.f64 d (-.f64 b (-.f64 c a))))
(+.f64 (+.f64 (+.f64 (+.f64 e (neg.f64 d)) c) b) a)
(+.f64 a (+.f64 b (+.f64 c (-.f64 e d))))
(+.f64 a (+.f64 b (-.f64 e (-.f64 d c))))
(+.f64 (+.f64 e (-.f64 c d)) (+.f64 b a))
(+.f64 e (+.f64 (+.f64 c (-.f64 b d)) a))
(+.f64 (+.f64 (+.f64 (+.f64 (neg.f64 e) d) c) b) a)
(+.f64 a (+.f64 b (+.f64 c (+.f64 d (neg.f64 e)))))
(+.f64 b (+.f64 (+.f64 c (-.f64 d e)) a))
(+.f64 b (+.f64 d (+.f64 (-.f64 c e) a)))
(neg.f64 (+.f64 (+.f64 (+.f64 (+.f64 e d) c) b) (neg.f64 a)))
(neg.f64 (-.f64 (+.f64 (+.f64 e d) (+.f64 c b)) a))
(-.f64 a (+.f64 e (+.f64 d (+.f64 c b))))
(-.f64 (-.f64 a (+.f64 e c)) (+.f64 d b))
(-.f64 (-.f64 a (+.f64 d b)) (+.f64 e c))
(neg.f64 (+.f64 (+.f64 (+.f64 (+.f64 e d) c) (neg.f64 b)) a))
(neg.f64 (+.f64 a (-.f64 (+.f64 e (+.f64 d c)) b)))
(-.f64 (neg.f64 a) (+.f64 e (+.f64 d (-.f64 c b))))
(-.f64 b (+.f64 e (+.f64 c (+.f64 d a))))
(-.f64 b (+.f64 d (+.f64 e (+.f64 c a))))
(neg.f64 (+.f64 (+.f64 (+.f64 (+.f64 e d) (neg.f64 c)) b) a))
(neg.f64 (+.f64 a (+.f64 b (-.f64 (+.f64 e d) c))))
(-.f64 (neg.f64 a) (+.f64 b (+.f64 e (-.f64 d c))))
(-.f64 (-.f64 (-.f64 (-.f64 c d) e) b) a)
(-.f64 c (+.f64 e (+.f64 d (+.f64 b a))))
(neg.f64 (+.f64 (+.f64 (+.f64 (+.f64 e (neg.f64 d)) c) b) a))
(neg.f64 (+.f64 a (+.f64 b (+.f64 c (-.f64 e d)))))
(-.f64 (neg.f64 a) (+.f64 b (-.f64 e (-.f64 d c))))
(-.f64 (-.f64 d e) (+.f64 c (+.f64 b a)))
(-.f64 d (+.f64 e (+.f64 c (+.f64 b a))))
(neg.f64 (+.f64 (+.f64 (+.f64 (+.f64 (neg.f64 e) d) c) b) a))
(neg.f64 (+.f64 a (+.f64 b (+.f64 c (+.f64 d (neg.f64 e))))))
(-.f64 (neg.f64 a) (+.f64 c (+.f64 (-.f64 d e) b)))
(-.f64 (-.f64 e d) (+.f64 c (+.f64 b a)))
(-.f64 e (+.f64 d (+.f64 c (+.f64 b a))))
(+.f64 (+.f64 (+.f64 (+.f64 e d) c) a) b)
(+.f64 (+.f64 e (+.f64 d c)) (+.f64 b a))
(+.f64 d (+.f64 (+.f64 e c) (+.f64 b a)))
(+.f64 e (+.f64 (+.f64 d c) (+.f64 b a)))
(+.f64 c (+.f64 e (+.f64 d (+.f64 b a))))
(+.f64 (+.f64 (+.f64 (+.f64 e d) a) b) c)
(+.f64 (+.f64 e (+.f64 d c)) (+.f64 b a))
(+.f64 d (+.f64 (+.f64 e c) (+.f64 b a)))
(+.f64 e (+.f64 (+.f64 d c) (+.f64 b a)))
(+.f64 c (+.f64 e (+.f64 d (+.f64 b a))))
(+.f64 (+.f64 (+.f64 (+.f64 e a) c) b) d)
(+.f64 (+.f64 e (+.f64 d c)) (+.f64 b a))
(+.f64 d (+.f64 (+.f64 e c) (+.f64 b a)))
(+.f64 e (+.f64 (+.f64 d c) (+.f64 b a)))
(+.f64 c (+.f64 e (+.f64 d (+.f64 b a))))
(+.f64 (+.f64 (+.f64 (+.f64 a d) c) b) e)
(+.f64 (+.f64 e (+.f64 d c)) (+.f64 b a))
(+.f64 d (+.f64 (+.f64 e c) (+.f64 b a)))
(+.f64 e (+.f64 (+.f64 d c) (+.f64 b a)))
(+.f64 c (+.f64 e (+.f64 d (+.f64 b a))))
(+.f64 (+.f64 (+.f64 (+.f64 e d) b) c) a)
(+.f64 (+.f64 e (+.f64 d c)) (+.f64 b a))
(+.f64 d (+.f64 (+.f64 e c) (+.f64 b a)))
(+.f64 e (+.f64 (+.f64 d c) (+.f64 b a)))
(+.f64 c (+.f64 e (+.f64 d (+.f64 b a))))
(+.f64 (+.f64 (+.f64 (+.f64 e b) c) d) a)
(+.f64 (+.f64 e (+.f64 d c)) (+.f64 b a))
(+.f64 d (+.f64 (+.f64 e c) (+.f64 b a)))
(+.f64 e (+.f64 (+.f64 d c) (+.f64 b a)))
(+.f64 c (+.f64 e (+.f64 d (+.f64 b a))))
(+.f64 (+.f64 (+.f64 (+.f64 b d) c) e) a)
(+.f64 (+.f64 e (+.f64 d c)) (+.f64 b a))
(+.f64 d (+.f64 (+.f64 e c) (+.f64 b a)))
(+.f64 e (+.f64 (+.f64 d c) (+.f64 b a)))
(+.f64 c (+.f64 e (+.f64 d (+.f64 b a))))
(+.f64 (+.f64 (+.f64 (+.f64 e c) d) b) a)
(+.f64 (+.f64 e (+.f64 d c)) (+.f64 b a))
(+.f64 d (+.f64 (+.f64 e c) (+.f64 b a)))
(+.f64 e (+.f64 (+.f64 d c) (+.f64 b a)))
(+.f64 c (+.f64 e (+.f64 d (+.f64 b a))))
(+.f64 (+.f64 (+.f64 (+.f64 c d) e) b) a)
(+.f64 (+.f64 e (+.f64 d c)) (+.f64 b a))
(+.f64 d (+.f64 (+.f64 e c) (+.f64 b a)))
(+.f64 e (+.f64 (+.f64 d c) (+.f64 b a)))
(+.f64 c (+.f64 e (+.f64 d (+.f64 b a))))
(+.f64 (+.f64 (+.f64 (+.f64 d e) c) b) a)
(+.f64 (+.f64 e (+.f64 d c)) (+.f64 b a))
(+.f64 d (+.f64 (+.f64 e c) (+.f64 b a)))
(+.f64 e (+.f64 (+.f64 d c) (+.f64 b a)))
(+.f64 c (+.f64 e (+.f64 d (+.f64 b a))))
Symmetry

(sort a b c d e)

Compiler

Compiled 84 to 29 computations (65.5% saved)

Precisions
Click to see histograms. Total time spent on operations: 36.0ms
Operation ival-add, time spent: 35.0ms, 96.0% of total-time
Operation const, time spent: 1.0ms, 3.0% of total-time

eval1.0ms (0%)

Compiler

Compiled 41 to 17 computations (58.5% saved)

prune4.0ms (0.1%)

Alt Table
Click to see full alt table
StatusAccuracyProgram
▶99.4%
(+.f64 (+.f64 (+.f64 (+.f64 e d) c) b) a)
▶99.5%
(+.f64 (+.f64 e (+.f64 d c)) (+.f64 b a))
▶99.6%
(+.f64 e (+.f64 (+.f64 d c) (+.f64 b a)))
▶99.6%
(+.f64 d (+.f64 (+.f64 e c) (+.f64 b a)))
▶99.5%
(+.f64 c (+.f64 e (+.f64 d (+.f64 b a))))
Compiler

Compiled 140 to 90 computations (35.7% saved)

localize772.0ms (13.7%)

Compiler

Compiled 143 to 22 computations (84.6% saved)

Precisions
Click to see histograms. Total time spent on operations: 455.0ms
Operation ival-add, time spent: 452.0ms, 99.0% of total-time
Operation const, time spent: 3.0ms, 1.0% of total-time

eval0.0ms (0%)

Compiler

Compiled 5 to 5 computations (0% saved)

prune3.0ms (0.1%)

Pruning

5 alts after pruning (0 fresh and 5 done)

PrunedKeptTotal
New000
Fresh000
Picked055
Done000
Total055
Accuracy
100.0%
Counts
5 → 5
Alt Table
Click to see full alt table
StatusAccuracyProgram
✓99.4%
(+.f64 (+.f64 (+.f64 (+.f64 e d) c) b) a)
✓99.5%
(+.f64 (+.f64 e (+.f64 d c)) (+.f64 b a))
✓99.6%
(+.f64 e (+.f64 (+.f64 d c) (+.f64 b a)))
✓99.6%
(+.f64 d (+.f64 (+.f64 e c) (+.f64 b a)))
✓99.5%
(+.f64 c (+.f64 e (+.f64 d (+.f64 b a))))
Compiler

Compiled 120 to 66 computations (45% saved)

regimes43.0ms (0.8%)

Counts
5 → 1
Calls
Call 1
Inputs
(+.f64 c (+.f64 e (+.f64 d (+.f64 b a))))
(+.f64 d (+.f64 (+.f64 e c) (+.f64 b a)))
(+.f64 e (+.f64 (+.f64 d c) (+.f64 b a)))
(+.f64 (+.f64 e (+.f64 d c)) (+.f64 b a))
(+.f64 (+.f64 (+.f64 (+.f64 e d) c) b) a)
Outputs
(+.f64 e (+.f64 (+.f64 d c) (+.f64 b a)))
Calls

9 calls:

5.0ms
(+.f64 (+.f64 (+.f64 e d) c) b)
5.0ms
d
5.0ms
a
4.0ms
(+.f64 (+.f64 (+.f64 (+.f64 e d) c) b) a)
4.0ms
(+.f64 (+.f64 e d) c)
Results
AccuracySegmentsBranch
99.6%1a
99.6%1b
99.6%1c
99.6%1d
99.6%1e
99.6%1(+.f64 (+.f64 (+.f64 (+.f64 e d) c) b) a)
99.6%1(+.f64 (+.f64 (+.f64 e d) c) b)
99.6%1(+.f64 (+.f64 e d) c)
99.6%1(+.f64 e d)
Compiler

Compiled 74 to 55 computations (25.7% saved)

regimes17.0ms (0.3%)

Counts
2 → 1
Calls
Call 1
Inputs
(+.f64 c (+.f64 e (+.f64 d (+.f64 b a))))
(+.f64 d (+.f64 (+.f64 e c) (+.f64 b a)))
Outputs
(+.f64 d (+.f64 (+.f64 e c) (+.f64 b a)))
Calls

5 calls:

4.0ms
a
3.0ms
b
3.0ms
d
3.0ms
c
3.0ms
e
Results
AccuracySegmentsBranch
99.6%1a
99.6%1b
99.6%1c
99.6%1d
99.6%1e
Compiler

Compiled 30 to 25 computations (16.7% saved)

regimes14.0ms (0.2%)

Accuracy

Total 0.0b remaining (0%)

Threshold costs 0b (0%)

Counts
1 → 1
Calls
Call 1
Inputs
(+.f64 c (+.f64 e (+.f64 d (+.f64 b a))))
Outputs
(+.f64 c (+.f64 e (+.f64 d (+.f64 b a))))
Calls

5 calls:

3.0ms
a
3.0ms
d
3.0ms
e
3.0ms
b
3.0ms
c
Results
AccuracySegmentsBranch
99.5%1a
99.5%1b
99.5%1c
99.5%1d
99.5%1e
Compiler

Compiled 30 to 25 computations (16.7% saved)

simplify3.0ms (0.1%)

Algorithm
1×egg-herbie
Rules
20×+-commutative
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
023120
133120
Stop Event
1×done
1×saturated
Calls
Call 1
Inputs
(+.f64 e (+.f64 (+.f64 d c) (+.f64 b a)))
(+.f64 d (+.f64 (+.f64 e c) (+.f64 b a)))
(+.f64 c (+.f64 e (+.f64 d (+.f64 b a))))
Outputs
(+.f64 e (+.f64 (+.f64 d c) (+.f64 b a)))
(+.f64 d (+.f64 (+.f64 e c) (+.f64 b a)))
(+.f64 d (+.f64 (+.f64 b a) (+.f64 e c)))
(+.f64 c (+.f64 e (+.f64 d (+.f64 b a))))
Compiler

Compiled 42 to 27 computations (35.7% saved)

soundness523.0ms (9.3%)

Rules
1428×sub-neg
1428×sub-neg
1428×sub-neg
1366×distribute-neg-in
1366×distribute-neg-in
Iterations

Useful iterations: 2 (0.0ms)

IterNodesCost
078908
1228896
2797880
33183880
46545880
57498880
67853880
77976880
078908
1228896
2797880
33183880
46545880
57498880
67853880
77976880
078908
1228896
2797880
33183880
46545880
57498880
67853880
77976880
Stop Event
1×node limit
1×node limit
1×node limit
Compiler

Compiled 177 to 63 computations (64.4% saved)

end0.0ms (0%)

preprocess52.0ms (0.9%)

Remove

(sort a b c d e)

Compiler

Compiled 232 to 138 computations (40.5% saved)

Profiling

Loading profile data...