Details

Time bar (total: 773.0ms)

analyze74.0ms (9.5%)

Algorithm
search
Search
TrueOtherFalseIter
0%99.9%0.1%0
0%99.9%0.1%1
0%99.9%0.1%2
0%99.9%0.1%3
0%99.9%0.1%4
25%74.9%0.1%5
25%62.4%12.6%6
25%50%25.1%7
31.2%37.5%31.3%8
39%24.2%36.8%9
42.9%18.3%38.7%10
47.2%11.9%40.9%11
49.4%9.1%41.6%12
51.6%5.9%42.5%13
52.7%4.5%42.8%14
Compiler

Compiled 8 to 6 computations (25% saved)

sample13.0ms (1.6%)

Algorithm
intervals
Results
5.0ms256×body128valid
0.0msbody128invalid
Compiler

Compiled 15 to 13 computations (13.3% saved)

simplify245.0ms (31.7%)

Algorithm
egg-herbie
Rules
800×unsub-neg_binary64_3482
443×sub-neg_binary64_3481
423×unswap-sqr_binary64_3456
382×*-commutative_binary64_3419
364×distribute-neg-out_binary64_3450
316×+-commutative_binary64_3418
288×distribute-lft-neg-out_binary64_3447
287×neg-sub0_binary64_3483 distribute-rgt-in_binary64_3438
269×distribute-rgt-neg-out_binary64_3448
258×cancel-sign-sub-inv_binary64_3454
251×sqr-pow_binary64_3460
248×pow-sqr_binary64_3461
238×distribute-rgt-neg-in_binary64_3446
226×neg-mul-1_binary64_3484
220×distribute-lft-out_binary64_3439
203×distribute-neg-in_binary64_3449
193×cube-prod_binary64_3516
159×distribute-lft-neg-in_binary64_3445
153×pow-plus_binary64_3551
144×distribute-rgt-out--_binary64_3442
139×associate-+r-_binary64_3422
116×distribute-rgt-out_binary64_3441
114×distribute-lft-in_binary64_3437
103×associate-+l+_binary64_3421
95×distribute-lft-out--_binary64_3440
89×associate--r-_binary64_3427
86×associate--l-_binary64_3426
84×associate-+l-_binary64_3423
76×associate-+r+_binary64_3420
71×difference-of-squares_binary64_3457
70×associate-*r*_binary64_3428
62×associate--r+_binary64_3424
51×remove-double-neg_binary64_3476
50×unpow3_binary64_3554
49×distribute-rgt1-in_binary64_3444
44×cube-mult_binary64_3518
39×sub0-neg_binary64_3475
35×associate-*l*_binary64_3429
31×associate--l+_binary64_3425
30×mul0-rgt_binary64_3471 mul0-lft_binary64_3470
28×distribute-lft1-in_binary64_3443
27×associate-/l/_binary64_3435
21×associate-/l*_binary64_3433
20×times-frac_binary64_3494
19×associate-*r/_binary64_3430
17×cube-neg_binary64_3515
12×+-lft-identity_binary64_3472
count-2_binary64_3436
cube-unmult_binary64_3525 +-rgt-identity_binary64_3473 +-inverses_binary64_3467 cancel-sign-sub_binary64_3453
swap-sqr_binary64_3455
sqr-neg_binary64_3502 mul-1-neg_binary64_3480
associate-/r/_binary64_3434
/-rgt-identity_binary64_3479
*-rgt-identity_binary64_3478
*-lft-identity_binary64_3477 --rgt-identity_binary64_3474 difference-of-sqr--1_binary64_3459 associate-/r*_binary64_3432
1-exp_binary64_3532 *-inverses_binary64_3468
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_3751 erf-erfc_binary64_3750 erf-odd_binary64_3749 if-if-and-not_binary64_3748 if-if-and_binary64_3747 if-if-or-not_binary64_3746 if-if-or_binary64_3745 if-not_binary64_3744 if-same_binary64_3743 if-false_binary64_3742 if-true_binary64_3741 not-gte_binary64_3740 not-lte_binary64_3739 not-gt_binary64_3738 not-lt_binary64_3737 gte-same_binary64_3736 lte-same_binary64_3735 gt-same_binary64_3734 lt-same_binary64_3733 sinh---cosh_binary64_3680 sinh-+-cosh_binary64_3679 sinh-cosh_binary64_3678 tanh-def-c_binary64_3677 tanh-def-b_binary64_3676 tanh-def-a_binary64_3675 cosh-def_binary64_3674 sinh-def_binary64_3673 tan-neg_binary64_3620 cos-neg_binary64_3619 sin-neg_binary64_3618 tan-0_binary64_3617 cos-0_binary64_3616 sin-0_binary64_3615 hang-m-tan_binary64_3614 hang-p-tan_binary64_3613 hang-m0-tan_binary64_3612 hang-p0-tan_binary64_3611 hang-0m-tan_binary64_3610 hang-0p-tan_binary64_3609 tan-+PI/2_binary64_3608 tan-+PI_binary64_3607 tan-PI_binary64_3606 tan-PI/3_binary64_3605 tan-PI/4_binary64_3604 tan-PI/6_binary64_3603 cos-+PI/2_binary64_3602 cos-+PI_binary64_3601 cos-PI_binary64_3600 cos-PI/2_binary64_3599 cos-PI/3_binary64_3598 cos-PI/4_binary64_3597 cos-PI/6_binary64_3596 sin-+PI/2_binary64_3595 sin-+PI_binary64_3594 sin-PI_binary64_3593 sin-PI/2_binary64_3592 sin-PI/3_binary64_3591 sin-PI/4_binary64_3590 sin-PI/6_binary64_3589 sub-1-sin_binary64_3588 sub-1-cos_binary64_3587 -1-add-sin_binary64_3586 -1-add-cos_binary64_3585 1-sub-sin_binary64_3584 1-sub-cos_binary64_3583 cos-sin-sum_binary64_3582 log-E_binary64_3578 log-pow_binary64_3577 log-rec_binary64_3576 log-div_binary64_3575 log-prod_binary64_3574 pow-base-0_binary64_3572 unpow1/3_binary64_3555 unpow2_binary64_3553 unpow1/2_binary64_3552 exp-to-pow_binary64_3550 pow-base-1_binary64_3548 unpow0_binary64_3547 unpow1_binary64_3546 unpow-1_binary64_3545 exp-lft-cube_binary64_3544 exp-lft-sqr_binary64_3543 exp-cbrt_binary64_3542 exp-sqrt_binary64_3541 exp-prod_binary64_3540 div-exp_binary64_3539 rec-exp_binary64_3538 prod-exp_binary64_3537 exp-diff_binary64_3536 exp-neg_binary64_3535 exp-sum_binary64_3534 e-exp-1_binary64_3533 exp-1-e_binary64_3531 exp-0_binary64_3530 rem-log-exp_binary64_3529 rem-exp-log_binary64_3528 cube-div_binary64_3517 rem-3cbrt-rft_binary64_3514 rem-3cbrt-lft_binary64_3513 rem-cbrt-cube_binary64_3512 rem-cube-cbrt_binary64_3511 sqr-abs_binary64_3503 rem-sqrt-square_binary64_3501 rem-square-sqrt_binary64_3500 div-sub_binary64_3493 div0_binary64_3469 lft-mult-inverse_binary64_3466 rgt-mult-inverse_binary64_3465 remove-double-div_binary64_3464 difference-of-sqr-1_binary64_3458 distribute-neg-frac_binary64_3452 distribute-frac-neg_binary64_3451 associate-*l/_binary64_3431
Counts
1 → 0
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
0610
11410
22410
34910
410310
522710
635310
774210
8109810
9196710
10242710
11277310
12355010
13372910
14427010

prune1.0ms (0.2%)

Pruning

1 alts after pruning (1 fresh and 0 done)

PrunedKeptTotal
New000
Fresh011
Picked000
Done000
Total011
Error
0b
Counts
1 → 1
Compiler

Compiled 7 to 5 computations (28.6% saved)

localize4.0ms (0.5%)

rewrite0.0ms (0.1%)

Algorithm
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)

simplify9.0ms (1.1%)

Algorithm
egg-herbie
Rules
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_3751 erf-erfc_binary64_3750 erf-odd_binary64_3749 if-if-and-not_binary64_3748 if-if-and_binary64_3747 if-if-or-not_binary64_3746 if-if-or_binary64_3745 if-not_binary64_3744 if-same_binary64_3743 if-false_binary64_3742 if-true_binary64_3741 not-gte_binary64_3740 not-lte_binary64_3739 not-gt_binary64_3738 not-lt_binary64_3737 gte-same_binary64_3736 lte-same_binary64_3735 gt-same_binary64_3734 lt-same_binary64_3733 sinh---cosh_binary64_3680 sinh-+-cosh_binary64_3679 sinh-cosh_binary64_3678 tanh-def-c_binary64_3677 tanh-def-b_binary64_3676 tanh-def-a_binary64_3675 cosh-def_binary64_3674 sinh-def_binary64_3673 tan-neg_binary64_3620 cos-neg_binary64_3619 sin-neg_binary64_3618 tan-0_binary64_3617 cos-0_binary64_3616 sin-0_binary64_3615 hang-m-tan_binary64_3614 hang-p-tan_binary64_3613 hang-m0-tan_binary64_3612 hang-p0-tan_binary64_3611 hang-0m-tan_binary64_3610 hang-0p-tan_binary64_3609 tan-+PI/2_binary64_3608 tan-+PI_binary64_3607 tan-PI_binary64_3606 tan-PI/3_binary64_3605 tan-PI/4_binary64_3604 tan-PI/6_binary64_3603 cos-+PI/2_binary64_3602 cos-+PI_binary64_3601 cos-PI_binary64_3600 cos-PI/2_binary64_3599 cos-PI/3_binary64_3598 cos-PI/4_binary64_3597 cos-PI/6_binary64_3596 sin-+PI/2_binary64_3595 sin-+PI_binary64_3594 sin-PI_binary64_3593 sin-PI/2_binary64_3592 sin-PI/3_binary64_3591 sin-PI/4_binary64_3590 sin-PI/6_binary64_3589 sub-1-sin_binary64_3588 sub-1-cos_binary64_3587 -1-add-sin_binary64_3586 -1-add-cos_binary64_3585 1-sub-sin_binary64_3584 1-sub-cos_binary64_3583 cos-sin-sum_binary64_3582 log-E_binary64_3578 log-pow_binary64_3577 log-rec_binary64_3576 log-div_binary64_3575 log-prod_binary64_3574 pow-base-0_binary64_3572 unpow1/3_binary64_3555 unpow3_binary64_3554 unpow2_binary64_3553 unpow1/2_binary64_3552 pow-plus_binary64_3551 exp-to-pow_binary64_3550 pow-base-1_binary64_3548 unpow0_binary64_3547 unpow1_binary64_3546 unpow-1_binary64_3545 exp-lft-cube_binary64_3544 exp-lft-sqr_binary64_3543 exp-cbrt_binary64_3542 exp-sqrt_binary64_3541 exp-prod_binary64_3540 div-exp_binary64_3539 rec-exp_binary64_3538 prod-exp_binary64_3537 exp-diff_binary64_3536 exp-neg_binary64_3535 exp-sum_binary64_3534 e-exp-1_binary64_3533 1-exp_binary64_3532 exp-1-e_binary64_3531 exp-0_binary64_3530 rem-log-exp_binary64_3529 rem-exp-log_binary64_3528 cube-unmult_binary64_3525 cube-mult_binary64_3518 cube-div_binary64_3517 cube-prod_binary64_3516 cube-neg_binary64_3515 rem-3cbrt-rft_binary64_3514 rem-3cbrt-lft_binary64_3513 rem-cbrt-cube_binary64_3512 rem-cube-cbrt_binary64_3511 sqr-abs_binary64_3503 sqr-neg_binary64_3502 rem-sqrt-square_binary64_3501 rem-square-sqrt_binary64_3500 times-frac_binary64_3494 div-sub_binary64_3493 neg-mul-1_binary64_3484 neg-sub0_binary64_3483 unsub-neg_binary64_3482 sub-neg_binary64_3481 mul-1-neg_binary64_3480 /-rgt-identity_binary64_3479 *-rgt-identity_binary64_3478 *-lft-identity_binary64_3477 remove-double-neg_binary64_3476 sub0-neg_binary64_3475 --rgt-identity_binary64_3474 +-rgt-identity_binary64_3473 +-lft-identity_binary64_3472 mul0-rgt_binary64_3471 mul0-lft_binary64_3470 div0_binary64_3469 *-inverses_binary64_3468 +-inverses_binary64_3467 lft-mult-inverse_binary64_3466 rgt-mult-inverse_binary64_3465 remove-double-div_binary64_3464 pow-sqr_binary64_3461 sqr-pow_binary64_3460 difference-of-sqr--1_binary64_3459 difference-of-sqr-1_binary64_3458 difference-of-squares_binary64_3457 unswap-sqr_binary64_3456 swap-sqr_binary64_3455 cancel-sign-sub-inv_binary64_3454 cancel-sign-sub_binary64_3453 distribute-neg-frac_binary64_3452 distribute-frac-neg_binary64_3451 distribute-neg-out_binary64_3450 distribute-neg-in_binary64_3449 distribute-rgt-neg-out_binary64_3448 distribute-lft-neg-out_binary64_3447 distribute-rgt-neg-in_binary64_3446 distribute-lft-neg-in_binary64_3445 distribute-rgt1-in_binary64_3444 distribute-lft1-in_binary64_3443 distribute-rgt-out--_binary64_3442 distribute-rgt-out_binary64_3441 distribute-lft-out--_binary64_3440 distribute-lft-out_binary64_3439 distribute-rgt-in_binary64_3438 distribute-lft-in_binary64_3437 count-2_binary64_3436 associate-/l/_binary64_3435 associate-/r/_binary64_3434 associate-/l*_binary64_3433 associate-/r*_binary64_3432 associate-*l/_binary64_3431 associate-*r/_binary64_3430 associate-*l*_binary64_3429 associate-*r*_binary64_3428 associate--r-_binary64_3427 associate--l-_binary64_3426 associate--l+_binary64_3425 associate--r+_binary64_3424 associate-+l-_binary64_3423 associate-+r-_binary64_3422 associate-+l+_binary64_3421 associate-+r+_binary64_3420 *-commutative_binary64_3419 +-commutative_binary64_3418
Counts
0 → 0
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
000

prune1.0ms (0.1%)

Pruning

1 alts after pruning (0 fresh and 1 done)

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

Compiled 7 to 5 computations (28.6% saved)

simplify3.0ms (0.4%)

Algorithm
egg-herbie
Rules
sub-neg_binary64_3481 +-commutative_binary64_3418
neg-mul-1_binary64_3484 neg-sub0_binary64_3483 *-commutative_binary64_3419
cancel-sign-sub-inv_binary64_3454 distribute-lft-neg-out_binary64_3447 distribute-rgt-neg-in_binary64_3446
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_3748 if-if-and_binary64_3747 if-if-or-not_binary64_3746 if-if-or_binary64_3745 if-not_binary64_3744 if-same_binary64_3743 if-false_binary64_3742 if-true_binary64_3741 tan-0_binary64_3617 cos-0_binary64_3616 sin-0_binary64_3615 unpow1_binary64_3546 e-exp-1_binary64_3533 1-exp_binary64_3532 exp-1-e_binary64_3531 exp-0_binary64_3530 sqr-abs_binary64_3503 sqr-neg_binary64_3502 unsub-neg_binary64_3482 mul-1-neg_binary64_3480 /-rgt-identity_binary64_3479 *-rgt-identity_binary64_3478 *-lft-identity_binary64_3477 remove-double-neg_binary64_3476 sub0-neg_binary64_3475 --rgt-identity_binary64_3474 +-rgt-identity_binary64_3473 +-lft-identity_binary64_3472 cancel-sign-sub_binary64_3453 distribute-neg-frac_binary64_3452 distribute-frac-neg_binary64_3451 distribute-neg-out_binary64_3450 distribute-neg-in_binary64_3449 distribute-rgt-neg-out_binary64_3448 distribute-lft-neg-in_binary64_3445
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
0610
11110
21810
32210
42410
Proof
(- f64 (* f64 h0 h0) (* f64 h1 h1))

end0.0ms (0%)

sample422.0ms (54.6%)

Algorithm
intervals
Results
168.0ms8000×body128valid
3.0ms146×body128invalid
Compiler

Compiled 29 to 23 computations (20.7% saved)

Profiling

Loading profile data...