Time bar (total: 46.1s)
| 310.0ms | (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))) |
1 alts after pruning (1 fresh and 0 done)
Merged error: 0.1b
Found 4 expressions with local error:
| 0.5b | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) |
| 0.5b | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) |
| 0.4b | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) |
| 0.2b | (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)) |
| 6× | associate-*l/ p16-flip-- |
| 5× | sub-neg |
| 3× | associate-*r/ |
| 1× | distribute-rgt-in distribute-lft-in associate-*l* *-commutative |
| 27.0ms | (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)) |
| 25.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) |
| 24.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) |
| 22.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) |
| 0.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) |
| 0.0ms | (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)) |
| 0.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) |
| 0.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) |
| 765.0ms | (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))) |
| 382.0ms | (*.p16 (*.p16 (*.p16 (+.p16 (+.p16 a b) c) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)) |
| 362.0ms | (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 a a))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)) |
| 317.0ms | (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)) |
| 303.0ms | (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))) |
3 alts after pruning (2 fresh and 1 done)
Merged error: 0.1b
Found 4 expressions with local error:
| 1.4b | (/.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 a a))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) |
| 0.5b | (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 a a)) |
| 0.5b | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) |
| 0.4b | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) |
| 6× | associate-*l/ p16-flip-- |
| 4× | associate-/l/ |
| 3× | sub-neg associate-*r/ |
| 1× | associate-/l* difference-of-squares |
| 88.0ms | (/.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 a a))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) |
| 42.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) |
| 22.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) |
| 3.0ms | (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 a a)) |
| 0.0ms | (/.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 a a))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) |
| 0.0ms | (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 a a)) |
| 0.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) |
| 0.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) |
| 560.0ms | (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 a a))) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)) |
| 505.0ms | (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)))) (*.p16 (*.p16 a a) (*.p16 a a)))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)) |
| 442.0ms | (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 a a))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c))) |
| 423.0ms | (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 a a))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)) |
| 368.0ms | (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 a a))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)) |
4 alts after pruning (3 fresh and 1 done)
Merged error: 0.1b
Found 4 expressions with local error:
| 0.8b | (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)) |
| 0.5b | (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 a a)) |
| 0.5b | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) |
| 0.4b | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) |
| 4× | p16-flip-- |
| 3× | sub-neg |
| 1× | associate-/r/ difference-of-squares |
| 88.0ms | (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)) |
| 31.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) |
| 22.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) |
| 3.0ms | (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 a a)) |
| 0.0ms | (/.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)) |
| 0.0ms | (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 a a)) |
| 0.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) |
| 0.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) |
| 229.0ms | (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 a a))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) |
| 217.0ms | (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 a a))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) |
| 195.0ms | (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 a a))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) |
| 191.0ms | (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 a a))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) |
| 86.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) |
4 alts after pruning (2 fresh and 2 done)
Merged error: 0.1b
Found 4 expressions with local error:
| 1.7b | (/.p16 (*.p16 (*.p16 (*.p16 (+.p16 (+.p16 a b) c) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 a a))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) (real->posit16 2))) |
| 0.5b | (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 a a)) |
| 0.5b | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) |
| 0.4b | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) |
| 6× | p16-flip-- |
| 3× | sub-neg associate-*l/ associate-*r/ associate-/l/ |
| 1× | associate-/r* p16-times-frac associate-/l* difference-of-squares |
| 43.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) |
| 24.0ms | (/.p16 (*.p16 (*.p16 (*.p16 (+.p16 (+.p16 a b) c) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 a a))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) (real->posit16 2))) |
| 23.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) |
| 5.0ms | (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 a a)) |
| 0.0ms | (/.p16 (*.p16 (*.p16 (*.p16 (+.p16 (+.p16 a b) c) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 a a))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) (real->posit16 2))) |
| 0.0ms | (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 a a)) |
| 0.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) |
| 0.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) |
| 696.0ms | (/.p16 (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) (real->posit16 2)) |
| 561.0ms | (*.p16 (*.p16 (*.p16 (+.p16 (+.p16 a b) c) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 a a))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c))) |
| 527.0ms | (*.p16 (*.p16 (*.p16 (+.p16 (+.p16 a b) c) (-.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)))) (*.p16 (*.p16 a a) (*.p16 a a)))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)) |
| 501.0ms | (*.p16 (*.p16 (*.p16 (+.p16 (+.p16 a b) c) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 a a))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)) |
| 488.0ms | (*.p16 (*.p16 (*.p16 (+.p16 (+.p16 a b) c) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 a a))) (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b))) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)) |
5 alts after pruning (3 fresh and 2 done)
Merged error: 0.1b
-∞% (-63.8b remaining)
Error of 0.2b against oracle of 64.0b and baseline of 64.0b