Time bar (total: 42.3s)
| 253.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)) b) |
| 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)) a) |
| 0.2b | (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) |
| 5× | sub-neg |
| 4× | p16-flip-- |
| 1× | distribute-rgt-in distribute-lft-in associate-*l/ associate-*r/ *-commutative |
| 66.0ms | (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) |
| 49.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) |
| 47.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) |
| 46.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) |
| 0.0ms | (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) 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)) a) |
| 380.0ms | (*.p16 (+.p16 (+.p16 a b) c) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) |
| 321.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))) |
| 298.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))) |
| 191.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))) |
| 191.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 (4 fresh and 1 done)
Merged error: 0.1b
Found 4 expressions with local error:
| 1.0b | (/.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)) a)) |
| 0.5b | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) |
| 0.5b | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) |
| 0.4b | (-.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 a a)) |
| 4× | p16-flip-- |
| 3× | sub-neg |
| 2× | associate-/l/ |
| 1× | associate-*l/ associate-*r/ associate-/l* difference-of-squares |
| 120.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)) a)) |
| 41.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) |
| 23.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 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)) 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)) b) |
| 0.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) |
| 263.0ms | (*.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)))) |
| 209.0ms | (*.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))) |
| 160.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) |
| 28.0ms | (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) |
| 28.0ms | (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) |
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 a b) c) (real->posit16 2)) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) |
| 0.5b | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) |
| 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)) a) |
| 4× | p16-flip-- |
| 3× | sub-neg |
| 2× | associate-*r/ associate-/l/ |
| 1× | associate-*l/ associate-/l* |
| 97.0ms | (/.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) |
| 47.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) |
| 46.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) |
| 34.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 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a))) (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) |
| 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)) a) |
| 0.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) |
| 237.0ms | (*.p16 (+.p16 (+.p16 a b) c) (*.p16 (+.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a))) |
| 200.0ms | (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (*.p16 (+.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 a a)))) |
| 128.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) |
| 80.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) |
| 80.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a) |
5 alts after pruning (4 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)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (neg.p16 a))) |
| 0.5b | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) |
| 0.5b | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) |
| 0.2b | (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) |
| 2× | sub-neg p16-flip-- |
| 1× | +-commutative p16-distribute-lft-out associate-*l/ associate-*r/ *-commutative distribute-lft-out |
| 29.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b) |
| 23.0ms | (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c) |
| 14.0ms | (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) |
| 6.0ms | (+.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)) (neg.p16 a))) |
| 0.0ms | (+.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)) (neg.p16 a))) |
| 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) |
| 0.0ms | (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) |
| 146.0ms | (*.p16 (+.p16 (+.p16 a b) c) (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2))) |
| 50.0ms | (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (neg.p16 a)) |
| 50.0ms | (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (neg.p16 a)) |
| 49.0ms | (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (neg.p16 a)) |
| 37.0ms | (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (neg.p16 a)) |
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