Time bar (total: 1.4m)Debug log
| 275.0ms | 135× | body | 1280 | valid |
| 210.0ms | 84× | body | 640 | valid |
| 194.0ms | 61× | body | 2560 | valid |
| 176.0ms | 30× | body | 5120 | valid |
| 25.0ms | 26× | body | 320 | valid |
| 24.0ms | 78× | body | 80 | valid |
| 7.0ms | 11× | body | 160 | valid |
| 113.0ms | (/ 2 (* (* (* (/ (pow t 3) (* l l)) (sin k)) (tan k)) (- (+ 1 (pow (/ k t) 2)) 1))) |
1 alts after pruning (1 fresh and 0 done)
Merged error: 46.7b
Found 4 expressions with local error:
| 34.5b | (* (* (* (/ (pow t 3) (* l l)) (sin k)) (tan k)) (- (+ 1 (pow (/ k t) 2)) 1)) |
| 14.0b | (/ (pow t 3) (* l l)) |
| 1.0b | (* (/ (pow t 3) (* l l)) (sin k)) |
| 0.9b | (- (+ 1 (pow (/ k t) 2)) 1) |
| 32× | add-exp-log |
| 25× | add-cbrt-cube |
| 15× | prod-exp |
| 15× | pow1 |
| 13× | associate-*l/ |
| 12× | add-sqr-sqrt |
| 11× | cbrt-unprod |
| 10× | add-cube-cbrt |
| 10× | associate-*l* |
| 10× | times-frac |
| 10× | *-un-lft-identity |
| 9× | frac-times |
| 7× | pow-prod-down |
| 7× | associate-*r* |
| 6× | tan-quot |
| 6× | div-exp |
| 5× | associate-/l* |
| 5× | flip-- |
| 5× | associate-*r/ |
| 5× | flip3-- |
| 4× | add-log-exp |
| 3× | associate--l+ |
| 3× | unpow3 |
| 3× | distribute-lft-in |
| 3× | sub-neg |
| 3× | cbrt-undiv |
| 3× | pow-to-exp |
| 3× | cube-mult |
| 3× | distribute-rgt-in |
| 2× | div-inv |
| 2× | *-commutative |
| 2× | difference-of-sqr-1 |
| 1× | frac-2neg |
| 1× | associate-/r* |
| 1× | clear-num |
| 58.0ms | (* (* (* (/ (pow t 3) (* l l)) (sin k)) (tan k)) (- (+ 1 (pow (/ k t) 2)) 1)) |
| 9.0ms | (* (/ (pow t 3) (* l l)) (sin k)) |
| 8.0ms | (- (+ 1 (pow (/ k t) 2)) 1) |
| 5.0ms | (/ (pow t 3) (* l l)) |
| 325.0ms | (* (* (* (/ (pow t 3) (* l l)) (sin k)) (tan k)) (- (+ 1 (pow (/ k t) 2)) 1)) |
| 78.0ms | (* (/ (pow t 3) (* l l)) (sin k)) |
| 27.0ms | (/ (pow t 3) (* l l)) |
| 21.0ms | (- (+ 1 (pow (/ k t) 2)) 1) |
| 855.0ms | (* (* (* (pow t 3) (sin k)) (sin k)) (- (+ 1 (pow (/ k t) 2)) 1)) |
| 825.0ms | (* (* (* (pow t 3) (sin k)) (tan k)) (- (+ 1 (pow (/ k t) 2)) 1)) |
| 664.0ms | (* (* (* (pow t 3) (sin k)) (tan k)) (- (pow (+ 1 (pow (/ k t) 2)) 3) (pow 1 3))) |
| 580.0ms | (- (+ 1 (pow (/ k t) 2)) 1) |
| 573.0ms | (* (* (* (/ (* (* (pow t 3) (pow t 3)) (pow t 3)) (* (* (* l l) (* l l)) (* l l))) (* (* (sin k) (sin k)) (sin k))) (* (* (tan k) (tan k)) (tan k))) (* (* (- (+ 1 (pow (/ k t) 2)) 1) (- (+ 1 (pow (/ k t) 2)) 1)) (- (+ 1 (pow (/ k t) 2)) 1))) |
10 alts after pruning (10 fresh and 0 done)
Merged error: 18.8b
Found 4 expressions with local error:
| 19.6b | (/ (* t (* (pow k 2) (pow (sin k) 2))) (* (pow l 2) (cos k))) |
| 5.0b | (* t (* (pow k 2) (pow (sin k) 2))) |
| 0.4b | (* (pow k 2) (pow (sin k) 2)) |
| 0.4b | (pow (sin k) 2) |
| 19× | add-exp-log |
| 11× | add-cbrt-cube |
| 8× | add-cube-cbrt |
| 8× | prod-exp |
| 8× | associate-*r* |
| 8× | *-un-lft-identity |
| 8× | add-sqr-sqrt |
| 7× | pow-to-exp |
| 6× | unpow-prod-down |
| 5× | pow1 |
| 4× | add-log-exp |
| 4× | associate-*l* |
| 3× | unpow2 |
| 3× | pow-exp |
| 3× | div-exp |
| 2× | cbrt-unprod |
| 2× | *-commutative |
| 2× | cbrt-undiv |
| 1× | associate-/l* |
| 1× | div-inv |
| 1× | pow-prod-down |
| 1× | times-frac |
| 1× | frac-2neg |
| 1× | pow-pow |
| 1× | associate-/r* |
| 1× | clear-num |
| 9.0ms | (/ (* t (* (pow k 2) (pow (sin k) 2))) (* (pow l 2) (cos k))) |
| 7.0ms | (* (pow k 2) (pow (sin k) 2)) |
| 7.0ms | (* t (* (pow k 2) (pow (sin k) 2))) |
| 2.0ms | (pow (sin k) 2) |
| 196.0ms | (/ (* t (* (pow k 2) (pow (sin k) 2))) (* (pow l 2) (cos k))) |
| 96.0ms | (* t (* (pow k 2) (pow (sin k) 2))) |
| 43.0ms | (* (pow k 2) (pow (sin k) 2)) |
| 25.0ms | (pow (sin k) 2) |
| 551.0ms | (/ (* (* (* t (* (pow k 2) (pow (sin k) 2))) (* t (* (pow k 2) (pow (sin k) 2)))) (* t (* (pow k 2) (pow (sin k) 2)))) (* (* (* (pow l 2) (pow l 2)) (pow l 2)) (* (* (cos k) (cos k)) (cos k)))) |
| 492.0ms | (/ (* t (* (pow k 2) (pow (sin k) 2))) (* (pow l 2) (cos k))) |
| 454.0ms | (/ (* (* (* t (* (pow k 2) (pow (sin k) 2))) (* t (* (pow k 2) (pow (sin k) 2)))) (* t (* (pow k 2) (pow (sin k) 2)))) (* (* (* (pow l 2) (cos k)) (* (pow l 2) (cos k))) (* (pow l 2) (cos k)))) |
| 437.0ms | (/ (* t (* (pow k 2) (pow (sin k) 2))) (* (pow l 2) (cos k))) |
| 425.0ms | (- (log (* t (* (pow k 2) (pow (sin k) 2)))) (log (* (pow l 2) (cos k)))) |
15 alts after pruning (15 fresh and 0 done)
Merged error: 15.2b
Found 4 expressions with local error:
| 19.6b | (/ (* (* t (pow k 2)) (pow (sin k) 2)) (* (pow l 2) (cos k))) |
| 4.7b | (* t (pow k 2)) |
| 0.4b | (pow (sin k) 2) |
| 0.4b | (/ 2 (/ (* (* t (pow k 2)) (pow (sin k) 2)) (* (pow l 2) (cos k)))) |
| 39× | add-exp-log |
| 17× | prod-exp |
| 16× | add-cbrt-cube |
| 12× | div-exp |
| 8× | pow-to-exp |
| 7× | add-cube-cbrt |
| 7× | *-un-lft-identity |
| 7× | add-sqr-sqrt |
| 6× | associate-/r* |
| 5× | pow1 |
| 4× | add-log-exp |
| 4× | cbrt-unprod |
| 4× | pow-exp |
| 4× | associate-*r* |
| 4× | cbrt-undiv |
| 3× | div-inv |
| 3× | unpow-prod-down |
| 2× | unpow2 |
| 2× | times-frac |
| 2× | frac-2neg |
| 2× | clear-num |
| 1× | associate-/l* |
| 1× | *-commutative |
| 1× | associate-/r/ |
| 1× | pow-pow |
| 12.0ms | (/ (* (* t (pow k 2)) (pow (sin k) 2)) (* (pow l 2) (cos k))) |
| 2.0ms | (/ 2 (/ (* (* t (pow k 2)) (pow (sin k) 2)) (* (pow l 2) (cos k)))) |
| 2.0ms | (* t (pow k 2)) |
| 2.0ms | (pow (sin k) 2) |
| 266.0ms | (/ 2 (/ (* (* t (pow k 2)) (pow (sin k) 2)) (* (pow l 2) (cos k)))) |
| 229.0ms | (/ (* (* t (pow k 2)) (pow (sin k) 2)) (* (pow l 2) (cos k))) |
| 21.0ms | (pow (sin k) 2) |
| 18.0ms | (* t (pow k 2)) |
| 888.0ms | (/ (* (* (* (* t (pow k 2)) (* t (pow k 2))) (* t (pow k 2))) (* (* (pow (sin k) 2) (pow (sin k) 2)) (pow (sin k) 2))) (* (* (* (pow l 2) (cos k)) (* (pow l 2) (cos k))) (* (pow l 2) (cos k)))) |
| 600.0ms | (- (+ (log (* t (pow k 2))) (* (log (sin k)) 2)) (log (* (pow l 2) (cos k)))) |
| 543.0ms | (- (+ (log (* t (pow k 2))) (* (log (sin k)) 2)) (log (* (pow l 2) (cos k)))) |
| 516.0ms | (/ (* (* (* (* t (pow k 2)) (* t (pow k 2))) (* t (pow k 2))) (* (* (pow (sin k) 2) (pow (sin k) 2)) (pow (sin k) 2))) (* (* (* (pow l 2) (pow l 2)) (pow l 2)) (* (* (cos k) (cos k)) (cos k)))) |
| 499.0ms | (/ (* (* (* (* t (pow k 2)) (pow (sin k) 2)) (* (* t (pow k 2)) (pow (sin k) 2))) (* (* t (pow k 2)) (pow (sin k) 2))) (* (* (* (pow l 2) (pow l 2)) (pow l 2)) (* (* (cos k) (cos k)) (cos k)))) |
16 alts after pruning (16 fresh and 0 done)
Merged error: 13.1b
Found 4 expressions with local error:
| 19.6b | (/ (* (* (* t k) k) (pow (sin k) 2)) (* (pow l 2) (cos k))) |
| 0.4b | (pow (sin k) 2) |
| 0.4b | (/ 2 (/ (* (* (* t k) k) (pow (sin k) 2)) (* (pow l 2) (cos k)))) |
| 0.4b | (* (* (* t k) k) (pow (sin k) 2)) |
| 44× | add-exp-log |
| 20× | prod-exp |
| 18× | add-cbrt-cube |
| 12× | div-exp |
| 9× | pow-to-exp |
| 8× | add-cube-cbrt |
| 8× | *-un-lft-identity |
| 8× | add-sqr-sqrt |
| 7× | associate-*r* |
| 6× | unpow-prod-down |
| 6× | associate-/r* |
| 5× | cbrt-unprod |
| 5× | pow-exp |
| 5× | pow1 |
| 4× | add-log-exp |
| 4× | cbrt-undiv |
| 3× | div-inv |
| 2× | unpow2 |
| 2× | times-frac |
| 2× | frac-2neg |
| 2× | clear-num |
| 1× | associate-/l* |
| 1× | *-commutative |
| 1× | associate-/r/ |
| 1× | associate-*l* |
| 1× | pow-pow |
| 19.0ms | (/ (* (* (* t k) k) (pow (sin k) 2)) (* (pow l 2) (cos k))) |
| 8.0ms | (* (* (* t k) k) (pow (sin k) 2)) |
| 1.0ms | (/ 2 (/ (* (* (* t k) k) (pow (sin k) 2)) (* (pow l 2) (cos k)))) |
| 1.0ms | (pow (sin k) 2) |
| 232.0ms | (/ 2 (/ (* (* (* t k) k) (pow (sin k) 2)) (* (pow l 2) (cos k)))) |
| 202.0ms | (/ (* (* (* t k) k) (pow (sin k) 2)) (* (pow l 2) (cos k))) |
| 84.0ms | (* (* (* t k) k) (pow (sin k) 2)) |
| 17.0ms | (pow (sin k) 2) |
| 601.0ms | (/ (* (* (* (* (* t k) k) (pow (sin k) 2)) (* (* (* t k) k) (pow (sin k) 2))) (* (* (* t k) k) (pow (sin k) 2))) (* (* (* (pow l 2) (pow l 2)) (pow l 2)) (* (* (cos k) (cos k)) (cos k)))) |
| 592.0ms | (* (* (* (* (* t k) k) (* (* t k) k)) (* (* t k) k)) (* (* (pow (sin k) 2) (pow (sin k) 2)) (pow (sin k) 2))) |
| 576.0ms | (/ (* (* (* (* (* t k) k) (* (* t k) k)) (* (* t k) k)) (* (* (pow (sin k) 2) (pow (sin k) 2)) (pow (sin k) 2))) (* (* (* (pow l 2) (cos k)) (* (pow l 2) (cos k))) (* (pow l 2) (cos k)))) |
| 543.0ms | (/ (* (* (* (* (* t k) k) (* (* t k) k)) (* (* t k) k)) (* (* (pow (sin k) 2) (pow (sin k) 2)) (pow (sin k) 2))) (* (* (* (pow l 2) (pow l 2)) (pow l 2)) (* (* (cos k) (cos k)) (cos k)))) |
| 536.0ms | (/ (* t (* (pow k 2) (pow (sin k) 2))) (* (pow l 2) (cos k))) |
20 alts after pruning (20 fresh and 0 done)
Merged error: 12.5b
17.1% (6.1b remaining)
Error of 18.7b against oracle of 12.6b and baseline of 20.0b
| 11.5s | 2187× | body | 2560 | valid |
| 11.2s | 4121× | body | 1280 | valid |
| 9.4s | 995× | body | 5120 | valid |
| 5.1s | 2526× | body | 640 | valid |
| 1.5s | 1023× | body | 320 | valid |
| 863.0ms | 2059× | body | 80 | valid |
| 374.0ms | 451× | body | 160 | valid |