Details

Time bar (total: 997.0ms)

analyze3.0ms (0.3%)

Algorithm
1×search
Search
TrueOtherFalseIter
0%100%0%0
0%100%0%1
0%100%0%2
0%100%0%3
87.5%12.5%0%4
93.7%6.2%0%5
96.8%3.1%0%6
98.4%1.6%0%7
99.2%0.8%0%8
99.6%0.4%0%9
99.8%0.2%0%10
99.9%0.1%0%11
99.9%0%0%12
99.9%0%0%13
99.9%0%0%14
Compiler

Compiled 8 to 6 computations (25% saved)

sample12.0ms (1.2%)

Algorithm
1×intervals
Results
5.0ms256×body128valid
Compiler

Compiled 15 to 12 computations (20% saved)

simplify548.0ms (55%)

Algorithm
1×egg-herbie
Rules
527×associate-/l/_binary64_12301
511×div-sub_binary64_12359
352×distribute-rgt-out_binary64_12307
317×distribute-rgt-out--_binary64_12308
284×cancel-sign-sub-inv_binary64_12320
242×distribute-lft-out_binary64_12305
239×distribute-lft-out--_binary64_12306
224×associate-/r/_binary64_12300
116×exp-sum_binary64_12400
76×sub-neg_binary64_12347
75×exp-prod_binary64_12406
52×exp-diff_binary64_12402
45×distribute-neg-in_binary64_12315
33×distribute-rgt-in_binary64_12304
31×distribute-rgt-neg-in_binary64_12312
30×distribute-lft-in_binary64_12303
29×distribute-rgt1-in_binary64_12310 associate--l+_binary64_12291
28×swap-sqr_binary64_12321
22×unsub-neg_binary64_12348 distribute-lft-neg-in_binary64_12311
21×associate-+r+_binary64_12286
19×distribute-neg-frac_binary64_12318
17×associate-/l*_binary64_12299 associate-*r*_binary64_12294
16×distribute-rgt-neg-out_binary64_12314
14×distribute-lft-neg-out_binary64_12313 associate--l-_binary64_12292
13×associate-+r-_binary64_12288
12×associate-*l*_binary64_12295
11×associate-+l+_binary64_12287
10×associate-/r*_binary64_12298 associate-*l/_binary64_12297 associate-+l-_binary64_12289
9×neg-sub0_binary64_12349
8×neg-mul-1_binary64_12350 associate--r+_binary64_12290
7×cancel-sign-sub_binary64_12319
6×times-frac_binary64_12360 sub0-neg_binary64_12341 sqr-pow_binary64_12326 associate-*r/_binary64_12296
5×--rgt-identity_binary64_12340 +-lft-identity_binary64_12338 distribute-neg-out_binary64_12316 *-commutative_binary64_12285 +-commutative_binary64_12284
4×*-rgt-identity_binary64_12344 +-rgt-identity_binary64_12339 distribute-lft1-in_binary64_12309
3×cube-unmult_binary64_12391 *-lft-identity_binary64_12343
2×exp-neg_binary64_12401 count-2_binary64_12302
1×1-exp_binary64_12398 exp-1-e_binary64_12397 mul0-rgt_binary64_12337 div0_binary64_12335 *-inverses_binary64_12334 +-inverses_binary64_12333 difference-of-squares_binary64_12323 associate--r-_binary64_12293
0×not-true not-false not-not not-and not-or and-true-l and-true-r and-false-l and-false-r and-same or-true-l or-true-r or-false-l or-false-r or-same erfc-erf_binary64_12617 erf-erfc_binary64_12616 erf-odd_binary64_12615 if-if-and-not_binary64_12614 if-if-and_binary64_12613 if-if-or-not_binary64_12612 if-if-or_binary64_12611 if-not_binary64_12610 if-same_binary64_12609 if-false_binary64_12608 if-true_binary64_12607 not-gte_binary64_12606 not-lte_binary64_12605 not-gt_binary64_12604 not-lt_binary64_12603 gte-same_binary64_12602 lte-same_binary64_12601 gt-same_binary64_12600 lt-same_binary64_12599 sinh---cosh_binary64_12546 sinh-+-cosh_binary64_12545 sinh-cosh_binary64_12544 tanh-def-c_binary64_12543 tanh-def-b_binary64_12542 tanh-def-a_binary64_12541 cosh-def_binary64_12540 sinh-def_binary64_12539 tan-neg_binary64_12486 cos-neg_binary64_12485 sin-neg_binary64_12484 tan-0_binary64_12483 cos-0_binary64_12482 sin-0_binary64_12481 hang-m-tan_binary64_12480 hang-p-tan_binary64_12479 hang-m0-tan_binary64_12478 hang-p0-tan_binary64_12477 hang-0m-tan_binary64_12476 hang-0p-tan_binary64_12475 tan-+PI/2_binary64_12474 tan-+PI_binary64_12473 tan-PI_binary64_12472 tan-PI/3_binary64_12471 tan-PI/4_binary64_12470 tan-PI/6_binary64_12469 cos-+PI/2_binary64_12468 cos-+PI_binary64_12467 cos-PI_binary64_12466 cos-PI/2_binary64_12465 cos-PI/3_binary64_12464 cos-PI/4_binary64_12463 cos-PI/6_binary64_12462 sin-+PI/2_binary64_12461 sin-+PI_binary64_12460 sin-PI_binary64_12459 sin-PI/2_binary64_12458 sin-PI/3_binary64_12457 sin-PI/4_binary64_12456 sin-PI/6_binary64_12455 sub-1-sin_binary64_12454 sub-1-cos_binary64_12453 -1-add-sin_binary64_12452 -1-add-cos_binary64_12451 1-sub-sin_binary64_12450 1-sub-cos_binary64_12449 cos-sin-sum_binary64_12448 log-E_binary64_12444 log-pow_binary64_12443 log-rec_binary64_12442 log-div_binary64_12441 log-prod_binary64_12440 pow-base-0_binary64_12438 unpow1/3_binary64_12421 unpow3_binary64_12420 unpow2_binary64_12419 unpow1/2_binary64_12418 pow-plus_binary64_12417 exp-to-pow_binary64_12416 pow-base-1_binary64_12414 unpow0_binary64_12413 unpow1_binary64_12412 unpow-1_binary64_12411 exp-lft-cube_binary64_12410 exp-lft-sqr_binary64_12409 exp-cbrt_binary64_12408 exp-sqrt_binary64_12407 div-exp_binary64_12405 rec-exp_binary64_12404 prod-exp_binary64_12403 e-exp-1_binary64_12399 exp-0_binary64_12396 rem-log-exp_binary64_12395 rem-exp-log_binary64_12394 cube-mult_binary64_12384 cube-div_binary64_12383 cube-prod_binary64_12382 cube-neg_binary64_12381 rem-3cbrt-rft_binary64_12380 rem-3cbrt-lft_binary64_12379 rem-cbrt-cube_binary64_12378 rem-cube-cbrt_binary64_12377 sqr-abs_binary64_12369 sqr-neg_binary64_12368 rem-sqrt-square_binary64_12367 rem-square-sqrt_binary64_12366 mul-1-neg_binary64_12346 /-rgt-identity_binary64_12345 remove-double-neg_binary64_12342 mul0-lft_binary64_12336 lft-mult-inverse_binary64_12332 rgt-mult-inverse_binary64_12331 remove-double-div_binary64_12330 pow-sqr_binary64_12327 difference-of-sqr--1_binary64_12325 difference-of-sqr-1_binary64_12324 unswap-sqr_binary64_12322 distribute-frac-neg_binary64_12317
Counts
1 → 2
Iterations

Useful iterations: 1 (0.0ms)

IterNodesCost
067
1141
2271
3891
45351

prune4.0ms (0.4%)

Pruning

1 alts after pruning (1 fresh and 0 done)

PrunedKeptTotal
New112
Fresh101
Picked000
Done000
Total213
Error
0b
Counts
3 → 1
Compiler

Compiled 7 to 8 computations (-14.3% saved)

localize0.0ms (0%)

rewrite0.0ms (0%)

Algorithm
1×rewrite-expression-head
Error
0b
Counts
0 → 0
Compiler

Compiled 0 to 0 computations (0% saved)

series0.0ms (0%)

Error
0b
Counts
0 → 0
Compiler

Compiled 0 to 0 computations (0% saved)

simplify8.0ms (0.8%)

Algorithm
1×egg-herbie
Rules
0×not-true not-false not-not not-and not-or and-true-l and-true-r and-false-l and-false-r and-same or-true-l or-true-r or-false-l or-false-r or-same erfc-erf_binary64_12617 erf-erfc_binary64_12616 erf-odd_binary64_12615 if-if-and-not_binary64_12614 if-if-and_binary64_12613 if-if-or-not_binary64_12612 if-if-or_binary64_12611 if-not_binary64_12610 if-same_binary64_12609 if-false_binary64_12608 if-true_binary64_12607 not-gte_binary64_12606 not-lte_binary64_12605 not-gt_binary64_12604 not-lt_binary64_12603 gte-same_binary64_12602 lte-same_binary64_12601 gt-same_binary64_12600 lt-same_binary64_12599 sinh---cosh_binary64_12546 sinh-+-cosh_binary64_12545 sinh-cosh_binary64_12544 tanh-def-c_binary64_12543 tanh-def-b_binary64_12542 tanh-def-a_binary64_12541 cosh-def_binary64_12540 sinh-def_binary64_12539 tan-neg_binary64_12486 cos-neg_binary64_12485 sin-neg_binary64_12484 tan-0_binary64_12483 cos-0_binary64_12482 sin-0_binary64_12481 hang-m-tan_binary64_12480 hang-p-tan_binary64_12479 hang-m0-tan_binary64_12478 hang-p0-tan_binary64_12477 hang-0m-tan_binary64_12476 hang-0p-tan_binary64_12475 tan-+PI/2_binary64_12474 tan-+PI_binary64_12473 tan-PI_binary64_12472 tan-PI/3_binary64_12471 tan-PI/4_binary64_12470 tan-PI/6_binary64_12469 cos-+PI/2_binary64_12468 cos-+PI_binary64_12467 cos-PI_binary64_12466 cos-PI/2_binary64_12465 cos-PI/3_binary64_12464 cos-PI/4_binary64_12463 cos-PI/6_binary64_12462 sin-+PI/2_binary64_12461 sin-+PI_binary64_12460 sin-PI_binary64_12459 sin-PI/2_binary64_12458 sin-PI/3_binary64_12457 sin-PI/4_binary64_12456 sin-PI/6_binary64_12455 sub-1-sin_binary64_12454 sub-1-cos_binary64_12453 -1-add-sin_binary64_12452 -1-add-cos_binary64_12451 1-sub-sin_binary64_12450 1-sub-cos_binary64_12449 cos-sin-sum_binary64_12448 log-E_binary64_12444 log-pow_binary64_12443 log-rec_binary64_12442 log-div_binary64_12441 log-prod_binary64_12440 pow-base-0_binary64_12438 unpow1/3_binary64_12421 unpow3_binary64_12420 unpow2_binary64_12419 unpow1/2_binary64_12418 pow-plus_binary64_12417 exp-to-pow_binary64_12416 pow-base-1_binary64_12414 unpow0_binary64_12413 unpow1_binary64_12412 unpow-1_binary64_12411 exp-lft-cube_binary64_12410 exp-lft-sqr_binary64_12409 exp-cbrt_binary64_12408 exp-sqrt_binary64_12407 exp-prod_binary64_12406 div-exp_binary64_12405 rec-exp_binary64_12404 prod-exp_binary64_12403 exp-diff_binary64_12402 exp-neg_binary64_12401 exp-sum_binary64_12400 e-exp-1_binary64_12399 1-exp_binary64_12398 exp-1-e_binary64_12397 exp-0_binary64_12396 rem-log-exp_binary64_12395 rem-exp-log_binary64_12394 cube-unmult_binary64_12391 cube-mult_binary64_12384 cube-div_binary64_12383 cube-prod_binary64_12382 cube-neg_binary64_12381 rem-3cbrt-rft_binary64_12380 rem-3cbrt-lft_binary64_12379 rem-cbrt-cube_binary64_12378 rem-cube-cbrt_binary64_12377 sqr-abs_binary64_12369 sqr-neg_binary64_12368 rem-sqrt-square_binary64_12367 rem-square-sqrt_binary64_12366 times-frac_binary64_12360 div-sub_binary64_12359 neg-mul-1_binary64_12350 neg-sub0_binary64_12349 unsub-neg_binary64_12348 sub-neg_binary64_12347 mul-1-neg_binary64_12346 /-rgt-identity_binary64_12345 *-rgt-identity_binary64_12344 *-lft-identity_binary64_12343 remove-double-neg_binary64_12342 sub0-neg_binary64_12341 --rgt-identity_binary64_12340 +-rgt-identity_binary64_12339 +-lft-identity_binary64_12338 mul0-rgt_binary64_12337 mul0-lft_binary64_12336 div0_binary64_12335 *-inverses_binary64_12334 +-inverses_binary64_12333 lft-mult-inverse_binary64_12332 rgt-mult-inverse_binary64_12331 remove-double-div_binary64_12330 pow-sqr_binary64_12327 sqr-pow_binary64_12326 difference-of-sqr--1_binary64_12325 difference-of-sqr-1_binary64_12324 difference-of-squares_binary64_12323 unswap-sqr_binary64_12322 swap-sqr_binary64_12321 cancel-sign-sub-inv_binary64_12320 cancel-sign-sub_binary64_12319 distribute-neg-frac_binary64_12318 distribute-frac-neg_binary64_12317 distribute-neg-out_binary64_12316 distribute-neg-in_binary64_12315 distribute-rgt-neg-out_binary64_12314 distribute-lft-neg-out_binary64_12313 distribute-rgt-neg-in_binary64_12312 distribute-lft-neg-in_binary64_12311 distribute-rgt1-in_binary64_12310 distribute-lft1-in_binary64_12309 distribute-rgt-out--_binary64_12308 distribute-rgt-out_binary64_12307 distribute-lft-out--_binary64_12306 distribute-lft-out_binary64_12305 distribute-rgt-in_binary64_12304 distribute-lft-in_binary64_12303 count-2_binary64_12302 associate-/l/_binary64_12301 associate-/r/_binary64_12300 associate-/l*_binary64_12299 associate-/r*_binary64_12298 associate-*l/_binary64_12297 associate-*r/_binary64_12296 associate-*l*_binary64_12295 associate-*r*_binary64_12294 associate--r-_binary64_12293 associate--l-_binary64_12292 associate--l+_binary64_12291 associate--r+_binary64_12290 associate-+l-_binary64_12289 associate-+r-_binary64_12288 associate-+l+_binary64_12287 associate-+r+_binary64_12286 *-commutative_binary64_12285 +-commutative_binary64_12284
Counts
0 → 0
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
000

prune0.0ms (0%)

Pruning

1 alts after pruning (0 fresh and 1 done)

PrunedKeptTotal
New000
Fresh000
Picked011
Done000
Total011
Error
0b
Counts
1 → 1
Compiler

Compiled 0 to 0 computations (0% saved)

regimes18.0ms (1.8%)

Accuracy

Total 0b remaining (0%)

Threshold costs 0b (0%)

Compiler

Compiled 65 to 54 computations (16.9% saved)

bsearch0.0ms (0%)

simplify3.0ms (0.3%)

Algorithm
1×egg-herbie
Rules
0×not-true not-false not-not not-and not-or and-true-l and-true-r and-false-l and-false-r and-same or-true-l or-true-r or-false-l or-false-r or-same if-if-and-not_binary64_12614 if-if-and_binary64_12613 if-if-or-not_binary64_12612 if-if-or_binary64_12611 if-not_binary64_12610 if-same_binary64_12609 if-false_binary64_12608 if-true_binary64_12607 tan-0_binary64_12483 cos-0_binary64_12482 sin-0_binary64_12481 unpow1_binary64_12412 e-exp-1_binary64_12399 1-exp_binary64_12398 exp-1-e_binary64_12397 exp-0_binary64_12396 sqr-abs_binary64_12369 sqr-neg_binary64_12368 neg-mul-1_binary64_12350 neg-sub0_binary64_12349 unsub-neg_binary64_12348 sub-neg_binary64_12347 mul-1-neg_binary64_12346 /-rgt-identity_binary64_12345 *-rgt-identity_binary64_12344 *-lft-identity_binary64_12343 remove-double-neg_binary64_12342 sub0-neg_binary64_12341 --rgt-identity_binary64_12340 +-rgt-identity_binary64_12339 +-lft-identity_binary64_12338 cancel-sign-sub-inv_binary64_12320 cancel-sign-sub_binary64_12319 distribute-neg-frac_binary64_12318 distribute-frac-neg_binary64_12317 distribute-neg-out_binary64_12316 distribute-neg-in_binary64_12315 distribute-rgt-neg-out_binary64_12314 distribute-lft-neg-out_binary64_12313 distribute-rgt-neg-in_binary64_12312 distribute-lft-neg-in_binary64_12311 *-commutative_binary64_12285 +-commutative_binary64_12284
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
011
Proof
0

end0.0ms (0%)

sample399.0ms (40%)

Algorithm
1×intervals
Results
163.0ms8000×body128valid
Compiler

Compiled 23 to 23 computations (0% saved)

Profiling

Loading profile data...