Time bar (total: 31.8s)
| 182.0ms | 126× | body | 1280 | valid |
| 40.0ms | 55× | body | 640 | valid |
| 13.0ms | 256× | pre | 80 | true |
| 10.0ms | 19× | body | 320 | valid |
| 6.0ms | 46× | body | 80 | valid |
| 3.0ms | 10× | body | 160 | valid |
| Iter | Nodes |
|---|---|
| done | 5000 |
| 296 | 4996 |
| 295 | 4982 |
| 294 | 4965 |
| 293 | 4949 |
| 292 | 4933 |
| 291 | 4913 |
| 290 | 4898 |
| 289 | 4882 |
| 288 | 4860 |
| 287 | 4846 |
| 286 | 4831 |
| 285 | 4813 |
| 284 | 4797 |
| 283 | 4783 |
| 282 | 4766 |
| 281 | 4750 |
| 280 | 4734 |
| 279 | 4714 |
| 278 | 4699 |
| 277 | 4683 |
| 276 | 4663 |
| 275 | 4649 |
| 274 | 4634 |
| 273 | 4616 |
| 272 | 4600 |
| 271 | 4586 |
| 270 | 4569 |
| 269 | 4553 |
| 268 | 4537 |
| 267 | 4517 |
| 266 | 4502 |
| 265 | 4486 |
| 264 | 4466 |
| 263 | 4452 |
| 262 | 4437 |
| 261 | 4419 |
| 260 | 4403 |
| 259 | 4389 |
| 258 | 4372 |
| 257 | 4356 |
| 256 | 4340 |
| 255 | 4320 |
| 254 | 4305 |
| 253 | 4289 |
| 252 | 4269 |
| 251 | 4255 |
| 250 | 4240 |
| 249 | 4222 |
| 248 | 4206 |
| 247 | 4192 |
| 246 | 4175 |
| 245 | 4159 |
| 244 | 4143 |
| 243 | 4125 |
| 242 | 4110 |
| 241 | 4094 |
| 240 | 4074 |
| 239 | 4060 |
| 238 | 4045 |
| 237 | 4027 |
| 236 | 4011 |
| 235 | 3997 |
| 234 | 3980 |
| 233 | 3964 |
| 232 | 3948 |
| 231 | 3930 |
| 230 | 3915 |
| 229 | 3899 |
| 228 | 3879 |
| 227 | 3865 |
| 226 | 3850 |
| 225 | 3832 |
| 224 | 3816 |
| 223 | 3802 |
| 222 | 3785 |
| 221 | 3769 |
| 220 | 3753 |
| 219 | 3735 |
| 218 | 3720 |
| 217 | 3704 |
| 216 | 3684 |
| 215 | 3670 |
| 214 | 3655 |
| 213 | 3637 |
| 212 | 3621 |
| 211 | 3607 |
| 210 | 3590 |
| 209 | 3574 |
| 208 | 3558 |
| 207 | 3540 |
| 206 | 3525 |
| 205 | 3509 |
| 204 | 3489 |
| 203 | 3475 |
| 202 | 3460 |
| 201 | 3442 |
| 200 | 3426 |
| 199 | 3412 |
| 198 | 3395 |
| 197 | 3379 |
| 196 | 3363 |
| 195 | 3345 |
| 194 | 3330 |
| 193 | 3314 |
| 192 | 3294 |
| 191 | 3280 |
| 190 | 3265 |
| 189 | 3247 |
| 188 | 3231 |
| 187 | 3217 |
| 186 | 3200 |
| 185 | 3184 |
| 184 | 3168 |
| 183 | 3148 |
| 182 | 3133 |
| 181 | 3117 |
| 180 | 3097 |
| 179 | 3083 |
| 178 | 3068 |
| 177 | 3050 |
| 176 | 3034 |
| 175 | 3020 |
| 174 | 3003 |
| 173 | 2987 |
| 172 | 2971 |
| 171 | 2951 |
| 170 | 2936 |
| 169 | 2920 |
| 168 | 2898 |
| 167 | 2884 |
| 166 | 2869 |
| 165 | 2851 |
| 164 | 2835 |
| 163 | 2821 |
| 162 | 2804 |
| 161 | 2788 |
| 160 | 2772 |
| 159 | 2754 |
| 158 | 2739 |
| 157 | 2723 |
| 156 | 2701 |
| 155 | 2687 |
| 154 | 2672 |
| 153 | 2654 |
| 152 | 2638 |
| 151 | 2624 |
| 150 | 2607 |
| 149 | 2591 |
| 148 | 2575 |
| 147 | 2557 |
| 146 | 2542 |
| 145 | 2526 |
| 144 | 2504 |
| 143 | 2490 |
| 142 | 2475 |
| 141 | 2457 |
| 140 | 2441 |
| 139 | 2427 |
| 138 | 2410 |
| 137 | 2394 |
| 136 | 2378 |
| 135 | 2358 |
| 134 | 2343 |
| 133 | 2327 |
| 132 | 2307 |
| 131 | 2293 |
| 130 | 2278 |
| 129 | 2260 |
| 128 | 2244 |
| 127 | 2230 |
| 126 | 2213 |
| 125 | 2197 |
| 124 | 2181 |
| 123 | 2163 |
| 122 | 2148 |
| 121 | 2132 |
| 120 | 2112 |
| 119 | 2098 |
| 118 | 2083 |
| 117 | 2065 |
| 116 | 2049 |
| 115 | 2035 |
| 114 | 2018 |
| 113 | 2002 |
| 112 | 1986 |
| 111 | 1968 |
| 110 | 1953 |
| 109 | 1937 |
| 108 | 1917 |
| 107 | 1903 |
| 106 | 1888 |
| 105 | 1870 |
| 104 | 1854 |
| 103 | 1840 |
| 102 | 1823 |
| 101 | 1807 |
| 100 | 1791 |
| 99 | 1771 |
| 98 | 1756 |
| 97 | 1740 |
| 96 | 1720 |
| 95 | 1706 |
| 94 | 1691 |
| 93 | 1673 |
| 92 | 1657 |
| 91 | 1643 |
| 90 | 1626 |
| 89 | 1610 |
| 88 | 1594 |
| 87 | 1574 |
| 86 | 1559 |
| 85 | 1543 |
| 84 | 1521 |
| 83 | 1507 |
| 82 | 1492 |
| 81 | 1474 |
| 80 | 1458 |
| 79 | 1444 |
| 78 | 1427 |
| 77 | 1411 |
| 76 | 1395 |
| 75 | 1377 |
| 74 | 1362 |
| 73 | 1346 |
| 72 | 1324 |
| 71 | 1310 |
| 70 | 1295 |
| 69 | 1277 |
| 68 | 1261 |
| 67 | 1247 |
| 66 | 1230 |
| 65 | 1214 |
| 64 | 1198 |
| 63 | 1178 |
| 62 | 1163 |
| 61 | 1147 |
| 60 | 1127 |
| 59 | 1113 |
| 58 | 1098 |
| 57 | 1080 |
| 56 | 1064 |
| 55 | 1050 |
| 54 | 1033 |
| 53 | 1017 |
| 52 | 1001 |
| 51 | 983 |
| 50 | 968 |
| 49 | 952 |
| 48 | 932 |
| 47 | 918 |
| 46 | 903 |
| 45 | 885 |
| 44 | 869 |
| 43 | 855 |
| 42 | 838 |
| 41 | 822 |
| 40 | 806 |
| 39 | 786 |
| 38 | 771 |
| 37 | 755 |
| 36 | 733 |
| 35 | 719 |
| 34 | 704 |
| 33 | 686 |
| 32 | 670 |
| 31 | 656 |
| 30 | 639 |
| 29 | 623 |
| 28 | 607 |
| 27 | 587 |
| 26 | 572 |
| 25 | 556 |
| 24 | 534 |
| 23 | 520 |
| 22 | 505 |
| 21 | 487 |
| 20 | 471 |
| 19 | 457 |
| 18 | 440 |
| 17 | 424 |
| 16 | 408 |
| 15 | 386 |
| 14 | 370 |
| 13 | 360 |
| 12 | 330 |
| 11 | 270 |
| 10 | 178 |
| 9 | 126 |
| 8 | 93 |
| 7 | 78 |
| 6 | 58 |
| 5 | 46 |
| 4 | 35 |
| 3 | 29 |
| 2 | 22 |
| 1 | 15 |
| 0 | 9 |
1 alts after pruning (1 fresh and 0 done)
Merged error: 12.2b
Found 3 expressions with local error:
| 0.1b | (+ x (- (tan (+ y z)) (tan a))) |
| 0.1b | (- (tan (+ y z)) (tan a)) |
| 2.9b | (tan (+ y z)) |
| 24× | *-un-lft-identity |
| 19× | add-sqr-sqrt |
| 18× | prod-diff |
| 17× | add-cube-cbrt |
| 11× | associate-+r+ |
| 10× | add-log-exp |
| 4× | tan-quot |
| 3× | expm1-log1p-u pow1 fma-def add-cbrt-cube fma-neg add-exp-log log1p-expm1-u |
| 2× | tan-sum sum-log sub-neg diff-log frac-sub distribute-lft-out distribute-lft-out-- |
| 1× | +-commutative associate-+r- flip3-+ flip3-- flip-+ flip-- difference-of-squares |
| 16.0ms | (+ x (- (tan (+ y z)) (tan a))) |
| 19.0ms | (- (tan (+ y z)) (tan a)) |
| 5.0ms | (tan (+ y z)) |
| 181.0ms | (+ x (- (tan (+ y z)) (tan a))) |
| 159.0ms | (- (tan (+ y z)) (tan a)) |
| 73.0ms | (tan (+ y z)) |
| Iter | Nodes |
|---|---|
| done | 5036 |
| 3 | 1932 |
| 2 | 642 |
| 1 | 283 |
| 0 | 128 |
7 alts after pruning (7 fresh and 0 done)
Merged error: 0.1b
Found 4 expressions with local error:
| 0.1b | (/ (+ (tan y) (tan z)) (- 1 (* (tan y) (tan z)))) |
| 0.1b | (+ x (- (/ (+ (tan y) (tan z)) (- 1 (* (tan y) (tan z)))) (tan a))) |
| 0.1b | (- (/ (+ (tan y) (tan z)) (- 1 (* (tan y) (tan z)))) (tan a)) |
| 0.2b | (* (tan y) (tan z)) |
| 165× | *-un-lft-identity |
| 115× | add-sqr-sqrt |
| 108× | prod-diff add-cube-cbrt |
| 97× | times-frac |
| 56× | associate-+r+ |
| 27× | distribute-lft-out |
| 18× | fma-neg |
| 16× | associate-/r/ |
| 11× | add-log-exp |
| 9× | flip3-- flip-- |
| 8× | add-cbrt-cube add-exp-log div-inv |
| 7× | tan-quot |
| 6× | pow1 |
| 4× | expm1-log1p-u log1p-expm1-u associate-/l* |
| 3× | associate-/r* fma-def associate-*r* associate-*l* associate-/l/ |
| 2× | sum-log sub-neg flip3-+ diff-log flip-+ distribute-lft-out-- difference-of-squares |
| 1× | frac-times cbrt-undiv +-commutative clear-num associate-+r- frac-2neg div-exp pow-prod-down associate-*l/ frac-add prod-exp associate-*r/ *-commutative frac-sub cbrt-unprod unswap-sqr |
| 26.0ms | (/ (+ (tan y) (tan z)) (- 1 (* (tan y) (tan z)))) |
| 170.0ms | (+ x (- (/ (+ (tan y) (tan z)) (- 1 (* (tan y) (tan z)))) (tan a))) |
| 107.0ms | (- (/ (+ (tan y) (tan z)) (- 1 (* (tan y) (tan z)))) (tan a)) |
| 24.0ms | (* (tan y) (tan z)) |
| 279.0ms | (/ (+ (tan y) (tan z)) (- 1 (* (tan y) (tan z)))) |
| 626.0ms | (+ x (- (/ (+ (tan y) (tan z)) (- 1 (* (tan y) (tan z)))) (tan a))) |
| 545.0ms | (- (/ (+ (tan y) (tan z)) (- 1 (* (tan y) (tan z)))) (tan a)) |
| 144.0ms | (* (tan y) (tan z)) |
| Iter | Nodes |
|---|---|
| done | 5002 |
| 2 | 1830 |
| 1 | 717 |
| 0 | 304 |
8 alts after pruning (8 fresh and 0 done)
Merged error: 0.0b
Found 4 expressions with local error:
| 0.7b | (cbrt (tan a)) |
| 0.7b | (cbrt (tan a)) |
| 0.7b | (cbrt (tan a)) |
| 60.5b | (fma (- (cbrt (tan a))) (* (cbrt (tan a)) (cbrt (tan a))) (* (cbrt (tan a)) (* (cbrt (tan a)) (cbrt (tan a))))) |
| 9× | cbrt-prod |
| 7× | add-sqr-sqrt *-un-lft-identity add-cube-cbrt |
| 4× | expm1-log1p-u pow1 add-cbrt-cube add-exp-log log1p-expm1-u add-log-exp |
| 3× | cbrt-div pow1/3 tan-quot |
| 1× | fma-udef |
| 1.0ms | (cbrt (tan a)) |
| 2.0ms | (cbrt (tan a)) |
| 2.0ms | (cbrt (tan a)) |
| 3.0ms | (fma (- (cbrt (tan a))) (* (cbrt (tan a)) (cbrt (tan a))) (* (cbrt (tan a)) (* (cbrt (tan a)) (cbrt (tan a))))) |
| 127.0ms | (cbrt (tan a)) |
| 127.0ms | (cbrt (tan a)) |
| 127.0ms | (cbrt (tan a)) |
| 199.0ms | (fma (- (cbrt (tan a))) (* (cbrt (tan a)) (cbrt (tan a))) (* (cbrt (tan a)) (* (cbrt (tan a)) (cbrt (tan a))))) |
| Iter | Nodes |
|---|---|
| done | 5000 |
| 4 | 2247 |
| 3 | 661 |
| 2 | 231 |
| 1 | 107 |
| 0 | 55 |
8 alts after pruning (7 fresh and 1 done)
Merged error: 0.0b
Found 4 expressions with local error:
| 0.7b | (cbrt (tan a)) |
| 0.7b | (cbrt (tan a)) |
| 0.7b | (cbrt (tan a)) |
| 60.5b | (fma (- (cbrt (tan a))) (* (cbrt (tan a)) (cbrt (tan a))) (* (cbrt (tan a)) (* (cbrt (tan a)) (cbrt (tan a))))) |
| 9× | cbrt-prod |
| 7× | add-sqr-sqrt *-un-lft-identity add-cube-cbrt |
| 4× | expm1-log1p-u pow1 add-cbrt-cube add-exp-log log1p-expm1-u add-log-exp |
| 3× | cbrt-div pow1/3 tan-quot |
| 1× | fma-udef |
| 1.0ms | (cbrt (tan a)) |
| 1.0ms | (cbrt (tan a)) |
| 1.0ms | (cbrt (tan a)) |
| 0.0ms | (fma (- (cbrt (tan a))) (* (cbrt (tan a)) (cbrt (tan a))) (* (cbrt (tan a)) (* (cbrt (tan a)) (cbrt (tan a))))) |
| 120.0ms | (cbrt (tan a)) |
| 124.0ms | (cbrt (tan a)) |
| 127.0ms | (cbrt (tan a)) |
| 197.0ms | (fma (- (cbrt (tan a))) (* (cbrt (tan a)) (cbrt (tan a))) (* (cbrt (tan a)) (* (cbrt (tan a)) (cbrt (tan a))))) |
| Iter | Nodes |
|---|---|
| done | 5000 |
| 4 | 2247 |
| 3 | 661 |
| 2 | 231 |
| 1 | 107 |
| 0 | 55 |
8 alts after pruning (6 fresh and 2 done)
Merged error: 0.0b
0% (0.2b remaining)
Error of 0.3b against oracle of 0.1b and baseline of 0.3b
| Iter | Nodes |
|---|---|
| done | 31 |
| 1 | 31 |
| 0 | 24 |
| 4.9s | 3940× | body | 1280 | valid |
| 1.7s | 1944× | body | 640 | valid |
| 504.0ms | 8000× | pre | 80 | true |
| 337.0ms | 725× | body | 320 | valid |
| 159.0ms | 1104× | body | 80 | valid |
| 105.0ms | 287× | body | 160 | valid |