Time bar (total: 40.6s)
| 569.0ms | 117× | body | 1280 | valid |
| 75.0ms | 66× | body | 640 | valid |
| 26.0ms | 256× | pre | 80 | true |
| 20.0ms | 23× | body | 320 | valid |
| 9.0ms | 41× | body | 80 | valid |
| 5.0ms | 9× | 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)) |
| 3.1b | (tan (+ y z)) |
| 10× | *-un-lft-identity add-log-exp |
| 5× | add-sqr-sqrt |
| 4× | tan-quot |
| 3× | pow1 add-cbrt-cube add-exp-log add-cube-cbrt insert-posit16 |
| 2× | tan-sum associate-+r+ 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 |
| 17.0ms | (+ x (- (tan (+ y z)) (tan a))) |
| 16.0ms | (- (tan (+ y z)) (tan a)) |
| 5.0ms | (tan (+ y z)) |
| 189.0ms | (+ x (- (tan (+ y z)) (tan a))) |
| 148.0ms | (- (tan (+ y z)) (tan a)) |
| 76.0ms | (tan (+ y z)) |
| Iter | Nodes |
|---|---|
| done | 5001 |
| 3 | 1509 |
| 2 | 472 |
| 1 | 200 |
| 0 | 94 |
6 alts after pruning (6 fresh and 0 done)
Merged error: 0.1b
Found 4 expressions with local error:
| 0.1b | (+ (tan y) (tan z)) |
| 0.2b | (* (tan y) (tan z)) |
| 0.2b | (* (tan y) (tan z)) |
| 0.2b | (/ (- (* (+ (tan y) (tan z)) (cos a)) (* (- 1 (* (tan y) (tan z))) (sin a))) (* (- 1 (* (tan y) (tan z))) (cos a))) |
| 16× | associate-*l/ |
| 14× | add-sqr-sqrt tan-quot |
| 13× | add-cbrt-cube add-exp-log |
| 12× | *-un-lft-identity |
| 10× | add-cube-cbrt |
| 8× | pow1 associate-/l/ |
| 6× | associate-*r* associate-*l* frac-sub add-log-exp |
| 5× | flip3-- flip-- |
| 4× | insert-posit16 |
| 3× | flip3-+ times-frac frac-add prod-exp cbrt-unprod flip-+ associate-/l* |
| 2× | frac-times cbrt-undiv div-exp pow-prod-down associate-*r/ associate-/r/ *-commutative unswap-sqr |
| 1× | +-commutative clear-num associate-/r* sum-log frac-2neg div-sub div-inv distribute-lft-out |
| 14.0ms | (+ (tan y) (tan z)) |
| 28.0ms | (* (tan y) (tan z)) |
| 28.0ms | (* (tan y) (tan z)) |
| 69.0ms | (/ (- (* (+ (tan y) (tan z)) (cos a)) (* (- 1 (* (tan y) (tan z))) (sin a))) (* (- 1 (* (tan y) (tan z))) (cos a))) |
| 161.0ms | (+ (tan y) (tan z)) |
| 154.0ms | (* (tan y) (tan z)) |
| 118.0ms | (* (tan y) (tan z)) |
| 662.0ms | (/ (- (* (+ (tan y) (tan z)) (cos a)) (* (- 1 (* (tan y) (tan z))) (sin a))) (* (- 1 (* (tan y) (tan z))) (cos a))) |
| Iter | Nodes |
|---|---|
| done | 5010 |
| 2 | 2296 |
| 1 | 554 |
| 0 | 181 |
7 alts after pruning (7 fresh and 0 done)
Merged error: 0.0b
Found 4 expressions with local error:
| 0.2b | (/ (- (/ (cos a) (/ (- 1 (* (tan y) (tan z))) (+ (tan y) (tan z)))) (sin a)) (cos a)) |
| 0.2b | (/ (- 1 (* (tan y) (tan z))) (+ (tan y) (tan z))) |
| 0.2b | (* (tan y) (tan z)) |
| 0.3b | (/ (cos a) (/ (- 1 (* (tan y) (tan z))) (+ (tan y) (tan z)))) |
| 150× | times-frac |
| 119× | *-un-lft-identity |
| 117× | add-sqr-sqrt |
| 79× | add-cube-cbrt |
| 26× | associate-/r* |
| 16× | associate-/r/ distribute-lft-out |
| 15× | add-cbrt-cube add-exp-log |
| 14× | tan-quot |
| 13× | associate-/l* |
| 12× | difference-of-squares |
| 7× | div-inv |
| 6× | pow1 |
| 5× | cbrt-undiv flip3-+ div-exp frac-add flip-+ |
| 4× | insert-posit16 distribute-lft-out-- add-log-exp associate-/l/ |
| 3× | clear-num frac-2neg associate-*r* associate-*l* |
| 2× | flip3-- div-sub flip-- |
| 1× | frac-times pow-prod-down associate-*l/ prod-exp associate-*r/ *-commutative cbrt-unprod unswap-sqr |
| 186.0ms | (/ (- (/ (cos a) (/ (- 1 (* (tan y) (tan z))) (+ (tan y) (tan z)))) (sin a)) (cos a)) |
| 19.0ms | (/ (- 1 (* (tan y) (tan z))) (+ (tan y) (tan z))) |
| 13.0ms | (* (tan y) (tan z)) |
| 24.0ms | (/ (cos a) (/ (- 1 (* (tan y) (tan z))) (+ (tan y) (tan z)))) |
| 752.0ms | (/ (- (/ (cos a) (/ (- 1 (* (tan y) (tan z))) (+ (tan y) (tan z)))) (sin a)) (cos a)) |
| 393.0ms | (/ (- 1 (* (tan y) (tan z))) (+ (tan y) (tan z))) |
| 135.0ms | (* (tan y) (tan z)) |
| 464.0ms | (/ (cos a) (/ (- 1 (* (tan y) (tan z))) (+ (tan y) (tan z)))) |
| Iter | Nodes |
|---|---|
| done | 5001 |
| 2 | 3157 |
| 1 | 954 |
| 0 | 363 |
7 alts after pruning (6 fresh and 1 done)
Merged error: 0.0b
Found 4 expressions with local error:
| 0.2b | (/ (/ (cos a) (/ (- 1 (* (tan y) (tan z))) (+ (* (sin y) (cos z)) (* (cos y) (sin z))))) (* (cos y) (cos z))) |
| 0.2b | (* (tan y) (tan z)) |
| 0.2b | (/ (- 1 (* (tan y) (tan z))) (+ (* (sin y) (cos z)) (* (cos y) (sin z)))) |
| 0.3b | (/ (cos a) (/ (- 1 (* (tan y) (tan z))) (+ (* (sin y) (cos z)) (* (cos y) (sin z))))) |
| 284× | times-frac |
| 134× | add-sqr-sqrt |
| 132× | *-un-lft-identity add-cube-cbrt |
| 56× | associate-/l* |
| 34× | add-cbrt-cube add-exp-log |
| 26× | associate-/r/ |
| 19× | associate-/r* |
| 16× | cbrt-undiv div-exp |
| 15× | div-inv |
| 11× | flip3-+ flip-+ |
| 6× | pow1 |
| 4× | prod-exp tan-quot cbrt-unprod insert-posit16 add-log-exp |
| 3× | clear-num frac-2neg associate-*r* associate-*l* associate-/l/ |
| 1× | frac-times flip3-- div-sub pow-prod-down associate-*l/ associate-*r/ cos-mult *-commutative flip-- unswap-sqr |
| 51.0ms | (/ (/ (cos a) (/ (- 1 (* (tan y) (tan z))) (+ (* (sin y) (cos z)) (* (cos y) (sin z))))) (* (cos y) (cos z))) |
| 19.0ms | (* (tan y) (tan z)) |
| 42.0ms | (/ (- 1 (* (tan y) (tan z))) (+ (* (sin y) (cos z)) (* (cos y) (sin z)))) |
| 56.0ms | (/ (cos a) (/ (- 1 (* (tan y) (tan z))) (+ (* (sin y) (cos z)) (* (cos y) (sin z))))) |
| 495.0ms | (/ (/ (cos a) (/ (- 1 (* (tan y) (tan z))) (+ (* (sin y) (cos z)) (* (cos y) (sin z))))) (* (cos y) (cos z))) |
| 110.0ms | (* (tan y) (tan z)) |
| 315.0ms | (/ (- 1 (* (tan y) (tan z))) (+ (* (sin y) (cos z)) (* (cos y) (sin z)))) |
| 396.0ms | (/ (cos a) (/ (- 1 (* (tan y) (tan z))) (+ (* (sin y) (cos z)) (* (cos y) (sin z))))) |
| Iter | Nodes |
|---|---|
| done | 5002 |
| 2 | 4702 |
| 1 | 1245 |
| 0 | 458 |
7 alts after pruning (5 fresh and 2 done)
Merged error: 0.0b
0% (0.1b remaining)
Error of 0.2b against oracle of 0.1b and baseline of 0.2b
| Iter | Nodes |
|---|---|
| done | 22 |
| 1 | 22 |
| 0 | 17 |
| 8.3s | 3873× | body | 1280 | valid |
| 2.8s | 1983× | body | 640 | valid |
| 810.0ms | 8000× | pre | 80 | true |
| 630.0ms | 714× | body | 320 | valid |
| 345.0ms | 1146× | body | 80 | valid |
| 224.0ms | 284× | body | 160 | valid |