Time bar (total: 41.7s)
| 364.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.2b
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.5b | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) |
| 0.2b | (*.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)) |
| 5× | sub-neg p16-flip-- |
| 3× | associate-*l/ |
| 2× | associate-*r/ |
| 1× | distribute-rgt-in distribute-lft-in associate-*l* *-commutative |
| 52.0ms | (*.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)) |
| 46.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) |
| 46.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) |
| 44.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) |
| 0.0ms | (-.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 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) |
| 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) |
| 633.0ms | (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (neg.p16 b)) |
| 534.0ms | (*.p16 (neg.p16 b) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a))) |
| 306.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)) |
| 246.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))) |
| 229.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))) |
5 alts after pruning (5 fresh and 0 done)
Merged error: 0.1b
Found 4 expressions with local error:
| 1.0b | (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)) |
| 0.5b | (-.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 c c)) |
| 0.5b | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) |
| 4× | p16-flip-- |
| 3× | sub-neg |
| 2× | difference-of-squares |
| 1× | associate-/l* associate-/l/ |
| 111.0ms | (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c)) |
| 43.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) |
| 28.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 c c)) |
| 0.0ms | (/.p16 (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) (+.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 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 c c)) |
| 0.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) |
| 91.0ms | (-.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 c c) (*.p16 c c))) |
| 79.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) |
| 13.0ms | (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) |
| 13.0ms | (+.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:
| 1.0b | (/.p16 (-.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)) a)) |
| 0.6b | (-.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.5b | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) |
| 4× | p16-flip-- |
| 3× | sub-neg |
| 2× | difference-of-squares |
| 1× | associate-/l* associate-/l/ |
| 119.0ms | (/.p16 (-.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)) a)) |
| 42.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) |
| 29.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) |
| 6.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) (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)) 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) |
| 94.0ms | (-.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))) |
| 80.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) |
| 14.0ms | (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) |
| 13.0ms | (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) |
4 alts after pruning (3 fresh and 1 done)
Merged error: 0.1b
Found 4 expressions with local error:
| 1.1b | (/.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)) b)) |
| 0.5b | (-.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 b b)) |
| 0.5b | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) |
| 5× | p16-flip-- |
| 3× | sub-neg associate-*l/ associate-/l/ |
| 2× | associate-*r/ |
| 1× | associate-/l* difference-of-squares |
| 60.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)) b)) |
| 38.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) |
| 32.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) |
| 5.0ms | (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) |
| 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 (+.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)) b)) |
| 0.0ms | (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b)) |
| 0.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) |
| 0.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) |
| 302.0ms | (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) |
| 297.0ms | (*.p16 (*.p16 (+.p16 (+.p16 a b) c) (-.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))) |
| 290.0ms | (*.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 (+.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 b b) (*.p16 b b)))) |
| 272.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 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 b b))) |
| 112.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) |
6 alts after pruning (5 fresh and 1 done)
Merged error: 0.1b
-∞% (-63.7b remaining)
Error of 0.3b against oracle of 64.0b and baseline of 64.0b