Details

Time bar (total: 939.0ms)

analyze3.0ms (0.4%)

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

Compiled 10 to 6 computations (40% saved)

sample11.0ms (1.2%)

Algorithm
1×intervals
Results
4.0ms256×body128valid
Compiler

Compiled 19 to 12 computations (36.8% saved)

simplify527.0ms (56.1%)

Algorithm
1×egg-herbie
Rules
700×exp-prod_binary64_4563
516×exp-sum_binary64_4557
505×sqr-pow_binary64_4483
391×pow-sqr_binary64_4484
359×distribute-rgt-in_binary64_4461
272×pow-plus_binary64_4574
195×associate-/r*_binary64_4455
177×associate-/l/_binary64_4458
161×distribute-rgt1-in_binary64_4467
145×associate-+l+_binary64_4444 *-commutative_binary64_4442
126×distribute-rgt-out_binary64_4464
117×associate-*r*_binary64_4451
113×pow-base-1_binary64_4571
106×unswap-sqr_binary64_4479
98×associate-*l*_binary64_4452
92×neg-mul-1_binary64_4507 neg-sub0_binary64_4506
91×cancel-sign-sub-inv_binary64_4477 distribute-lft-neg-in_binary64_4468
90×distribute-lft-in_binary64_4460
74×associate-+r+_binary64_4443
72×rem-sqrt-square_binary64_4524
62×times-frac_binary64_4517
61×distribute-rgt-neg-in_binary64_4469
58×+-commutative_binary64_4441
38×distribute-lft-out_binary64_4462
28×cube-unmult_binary64_4548
24×swap-sqr_binary64_4478 associate-/l*_binary64_4456
22×count-2_binary64_4459
20×associate-/r/_binary64_4457
19×distribute-lft1-in_binary64_4466
18×/-rgt-identity_binary64_4502
17×*-lft-identity_binary64_4500
14×*-rgt-identity_binary64_4501
13×cube-prod_binary64_4539
12×exp-lft-sqr_binary64_4566 exp-sqrt_binary64_4564 prod-exp_binary64_4560
10×distribute-neg-frac_binary64_4475
9×div-exp_binary64_4562
4×cube-div_binary64_4540
3×rec-exp_binary64_4561
1×unpow3_binary64_4577 1-exp_binary64_4555 exp-1-e_binary64_4554 sub-neg_binary64_4504 --rgt-identity_binary64_4497 +-rgt-identity_binary64_4496 div0_binary64_4492 *-inverses_binary64_4491 lft-mult-inverse_binary64_4489 rgt-mult-inverse_binary64_4488 remove-double-div_binary64_4487 associate-*r/_binary64_4453
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_4774 erf-erfc_binary64_4773 erf-odd_binary64_4772 if-if-and-not_binary64_4771 if-if-and_binary64_4770 if-if-or-not_binary64_4769 if-if-or_binary64_4768 if-not_binary64_4767 if-same_binary64_4766 if-false_binary64_4765 if-true_binary64_4764 not-gte_binary64_4763 not-lte_binary64_4762 not-gt_binary64_4761 not-lt_binary64_4760 gte-same_binary64_4759 lte-same_binary64_4758 gt-same_binary64_4757 lt-same_binary64_4756 sinh---cosh_binary64_4703 sinh-+-cosh_binary64_4702 sinh-cosh_binary64_4701 tanh-def-c_binary64_4700 tanh-def-b_binary64_4699 tanh-def-a_binary64_4698 cosh-def_binary64_4697 sinh-def_binary64_4696 tan-neg_binary64_4643 cos-neg_binary64_4642 sin-neg_binary64_4641 tan-0_binary64_4640 cos-0_binary64_4639 sin-0_binary64_4638 hang-m-tan_binary64_4637 hang-p-tan_binary64_4636 hang-m0-tan_binary64_4635 hang-p0-tan_binary64_4634 hang-0m-tan_binary64_4633 hang-0p-tan_binary64_4632 tan-+PI/2_binary64_4631 tan-+PI_binary64_4630 tan-PI_binary64_4629 tan-PI/3_binary64_4628 tan-PI/4_binary64_4627 tan-PI/6_binary64_4626 cos-+PI/2_binary64_4625 cos-+PI_binary64_4624 cos-PI_binary64_4623 cos-PI/2_binary64_4622 cos-PI/3_binary64_4621 cos-PI/4_binary64_4620 cos-PI/6_binary64_4619 sin-+PI/2_binary64_4618 sin-+PI_binary64_4617 sin-PI_binary64_4616 sin-PI/2_binary64_4615 sin-PI/3_binary64_4614 sin-PI/4_binary64_4613 sin-PI/6_binary64_4612 sub-1-sin_binary64_4611 sub-1-cos_binary64_4610 -1-add-sin_binary64_4609 -1-add-cos_binary64_4608 1-sub-sin_binary64_4607 1-sub-cos_binary64_4606 cos-sin-sum_binary64_4605 log-E_binary64_4601 log-pow_binary64_4600 log-rec_binary64_4599 log-div_binary64_4598 log-prod_binary64_4597 pow-base-0_binary64_4595 unpow1/3_binary64_4578 unpow2_binary64_4576 unpow1/2_binary64_4575 exp-to-pow_binary64_4573 unpow0_binary64_4570 unpow1_binary64_4569 unpow-1_binary64_4568 exp-lft-cube_binary64_4567 exp-cbrt_binary64_4565 exp-diff_binary64_4559 exp-neg_binary64_4558 e-exp-1_binary64_4556 exp-0_binary64_4553 rem-log-exp_binary64_4552 rem-exp-log_binary64_4551 cube-mult_binary64_4541 cube-neg_binary64_4538 rem-3cbrt-rft_binary64_4537 rem-3cbrt-lft_binary64_4536 rem-cbrt-cube_binary64_4535 rem-cube-cbrt_binary64_4534 sqr-abs_binary64_4526 sqr-neg_binary64_4525 rem-square-sqrt_binary64_4523 div-sub_binary64_4516 unsub-neg_binary64_4505 mul-1-neg_binary64_4503 remove-double-neg_binary64_4499 sub0-neg_binary64_4498 +-lft-identity_binary64_4495 mul0-rgt_binary64_4494 mul0-lft_binary64_4493 +-inverses_binary64_4490 difference-of-sqr--1_binary64_4482 difference-of-sqr-1_binary64_4481 difference-of-squares_binary64_4480 cancel-sign-sub_binary64_4476 distribute-frac-neg_binary64_4474 distribute-neg-out_binary64_4473 distribute-neg-in_binary64_4472 distribute-rgt-neg-out_binary64_4471 distribute-lft-neg-out_binary64_4470 distribute-rgt-out--_binary64_4465 distribute-lft-out--_binary64_4463 associate-*l/_binary64_4454 associate--r-_binary64_4450 associate--l-_binary64_4449 associate--l+_binary64_4448 associate--r+_binary64_4447 associate-+l-_binary64_4446 associate-+r-_binary64_4445
Counts
1 → 4
Iterations

Useful iterations: 1 (0.0ms)

IterNodesCost
0613
11310
22110
33410
44810
55510
66310
75810
86010
97410
1014910
1175910
12173510
13330010

prune5.0ms (0.5%)

Pruning

1 alts after pruning (1 fresh and 0 done)

PrunedKeptTotal
New314
Fresh101
Picked000
Done000
Total415
Error
0b
Counts
5 → 1
Compiler

Compiled 37 to 25 computations (32.4% saved)

localize4.0ms (0.4%)

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.9%)

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_4774 erf-erfc_binary64_4773 erf-odd_binary64_4772 if-if-and-not_binary64_4771 if-if-and_binary64_4770 if-if-or-not_binary64_4769 if-if-or_binary64_4768 if-not_binary64_4767 if-same_binary64_4766 if-false_binary64_4765 if-true_binary64_4764 not-gte_binary64_4763 not-lte_binary64_4762 not-gt_binary64_4761 not-lt_binary64_4760 gte-same_binary64_4759 lte-same_binary64_4758 gt-same_binary64_4757 lt-same_binary64_4756 sinh---cosh_binary64_4703 sinh-+-cosh_binary64_4702 sinh-cosh_binary64_4701 tanh-def-c_binary64_4700 tanh-def-b_binary64_4699 tanh-def-a_binary64_4698 cosh-def_binary64_4697 sinh-def_binary64_4696 tan-neg_binary64_4643 cos-neg_binary64_4642 sin-neg_binary64_4641 tan-0_binary64_4640 cos-0_binary64_4639 sin-0_binary64_4638 hang-m-tan_binary64_4637 hang-p-tan_binary64_4636 hang-m0-tan_binary64_4635 hang-p0-tan_binary64_4634 hang-0m-tan_binary64_4633 hang-0p-tan_binary64_4632 tan-+PI/2_binary64_4631 tan-+PI_binary64_4630 tan-PI_binary64_4629 tan-PI/3_binary64_4628 tan-PI/4_binary64_4627 tan-PI/6_binary64_4626 cos-+PI/2_binary64_4625 cos-+PI_binary64_4624 cos-PI_binary64_4623 cos-PI/2_binary64_4622 cos-PI/3_binary64_4621 cos-PI/4_binary64_4620 cos-PI/6_binary64_4619 sin-+PI/2_binary64_4618 sin-+PI_binary64_4617 sin-PI_binary64_4616 sin-PI/2_binary64_4615 sin-PI/3_binary64_4614 sin-PI/4_binary64_4613 sin-PI/6_binary64_4612 sub-1-sin_binary64_4611 sub-1-cos_binary64_4610 -1-add-sin_binary64_4609 -1-add-cos_binary64_4608 1-sub-sin_binary64_4607 1-sub-cos_binary64_4606 cos-sin-sum_binary64_4605 log-E_binary64_4601 log-pow_binary64_4600 log-rec_binary64_4599 log-div_binary64_4598 log-prod_binary64_4597 pow-base-0_binary64_4595 unpow1/3_binary64_4578 unpow3_binary64_4577 unpow2_binary64_4576 unpow1/2_binary64_4575 pow-plus_binary64_4574 exp-to-pow_binary64_4573 pow-base-1_binary64_4571 unpow0_binary64_4570 unpow1_binary64_4569 unpow-1_binary64_4568 exp-lft-cube_binary64_4567 exp-lft-sqr_binary64_4566 exp-cbrt_binary64_4565 exp-sqrt_binary64_4564 exp-prod_binary64_4563 div-exp_binary64_4562 rec-exp_binary64_4561 prod-exp_binary64_4560 exp-diff_binary64_4559 exp-neg_binary64_4558 exp-sum_binary64_4557 e-exp-1_binary64_4556 1-exp_binary64_4555 exp-1-e_binary64_4554 exp-0_binary64_4553 rem-log-exp_binary64_4552 rem-exp-log_binary64_4551 cube-unmult_binary64_4548 cube-mult_binary64_4541 cube-div_binary64_4540 cube-prod_binary64_4539 cube-neg_binary64_4538 rem-3cbrt-rft_binary64_4537 rem-3cbrt-lft_binary64_4536 rem-cbrt-cube_binary64_4535 rem-cube-cbrt_binary64_4534 sqr-abs_binary64_4526 sqr-neg_binary64_4525 rem-sqrt-square_binary64_4524 rem-square-sqrt_binary64_4523 times-frac_binary64_4517 div-sub_binary64_4516 neg-mul-1_binary64_4507 neg-sub0_binary64_4506 unsub-neg_binary64_4505 sub-neg_binary64_4504 mul-1-neg_binary64_4503 /-rgt-identity_binary64_4502 *-rgt-identity_binary64_4501 *-lft-identity_binary64_4500 remove-double-neg_binary64_4499 sub0-neg_binary64_4498 --rgt-identity_binary64_4497 +-rgt-identity_binary64_4496 +-lft-identity_binary64_4495 mul0-rgt_binary64_4494 mul0-lft_binary64_4493 div0_binary64_4492 *-inverses_binary64_4491 +-inverses_binary64_4490 lft-mult-inverse_binary64_4489 rgt-mult-inverse_binary64_4488 remove-double-div_binary64_4487 pow-sqr_binary64_4484 sqr-pow_binary64_4483 difference-of-sqr--1_binary64_4482 difference-of-sqr-1_binary64_4481 difference-of-squares_binary64_4480 unswap-sqr_binary64_4479 swap-sqr_binary64_4478 cancel-sign-sub-inv_binary64_4477 cancel-sign-sub_binary64_4476 distribute-neg-frac_binary64_4475 distribute-frac-neg_binary64_4474 distribute-neg-out_binary64_4473 distribute-neg-in_binary64_4472 distribute-rgt-neg-out_binary64_4471 distribute-lft-neg-out_binary64_4470 distribute-rgt-neg-in_binary64_4469 distribute-lft-neg-in_binary64_4468 distribute-rgt1-in_binary64_4467 distribute-lft1-in_binary64_4466 distribute-rgt-out--_binary64_4465 distribute-rgt-out_binary64_4464 distribute-lft-out--_binary64_4463 distribute-lft-out_binary64_4462 distribute-rgt-in_binary64_4461 distribute-lft-in_binary64_4460 count-2_binary64_4459 associate-/l/_binary64_4458 associate-/r/_binary64_4457 associate-/l*_binary64_4456 associate-/r*_binary64_4455 associate-*l/_binary64_4454 associate-*r/_binary64_4453 associate-*l*_binary64_4452 associate-*r*_binary64_4451 associate--r-_binary64_4450 associate--l-_binary64_4449 associate--l+_binary64_4448 associate--r+_binary64_4447 associate-+l-_binary64_4446 associate-+r-_binary64_4445 associate-+l+_binary64_4444 associate-+r+_binary64_4443 *-commutative_binary64_4442 +-commutative_binary64_4441
Counts
0 → 0
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
000

prune0.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 0 to 0 computations (0% saved)

regimes18.0ms (1.9%)

Accuracy

Total 0b remaining (0%)

Threshold costs 0b (0%)

Compiler

Compiled 52 to 34 computations (34.6% saved)

bsearch0.0ms (0%)

simplify3.0ms (0.3%)

Algorithm
1×egg-herbie
Rules
1×*-commutative_binary64_4442 +-commutative_binary64_4441
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_4771 if-if-and_binary64_4770 if-if-or-not_binary64_4769 if-if-or_binary64_4768 if-not_binary64_4767 if-same_binary64_4766 if-false_binary64_4765 if-true_binary64_4764 tan-0_binary64_4640 cos-0_binary64_4639 sin-0_binary64_4638 unpow1_binary64_4569 e-exp-1_binary64_4556 1-exp_binary64_4555 exp-1-e_binary64_4554 exp-0_binary64_4553 sqr-abs_binary64_4526 sqr-neg_binary64_4525 neg-mul-1_binary64_4507 neg-sub0_binary64_4506 unsub-neg_binary64_4505 sub-neg_binary64_4504 mul-1-neg_binary64_4503 /-rgt-identity_binary64_4502 *-rgt-identity_binary64_4501 *-lft-identity_binary64_4500 remove-double-neg_binary64_4499 sub0-neg_binary64_4498 --rgt-identity_binary64_4497 +-rgt-identity_binary64_4496 +-lft-identity_binary64_4495 cancel-sign-sub-inv_binary64_4477 cancel-sign-sub_binary64_4476 distribute-neg-frac_binary64_4475 distribute-frac-neg_binary64_4474 distribute-neg-out_binary64_4473 distribute-neg-in_binary64_4472 distribute-rgt-neg-out_binary64_4471 distribute-lft-neg-out_binary64_4470 distribute-rgt-neg-in_binary64_4469 distribute-lft-neg-in_binary64_4468
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
0610
1810
Proof
(+ f64 h0 (* f64 h0 (+ f64 2 2)))

end0.0ms (0%)

sample359.0ms (38.2%)

Algorithm
1×intervals
Results
144.0ms8000×body128valid
0.0ms4×body128invalid
Compiler

Compiled 33 to 24 computations (27.3% saved)

Profiling

Loading profile data...