Details

Time bar (total: 1.8min)

analyze2.1s (2%)

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
0%99.9%0.1%5
0%99.9%0.1%6
0%99.9%0.1%7
1.6%98.3%0.1%8
2.3%97.5%0.1%9
7.4%90.9%1.7%10
9.2%87.4%3.5%11
11.7%83.5%4.8%12
15.2%76%8.8%13
16.4%72%11.6%14
Compiler

Compiled 26 to 22 computations (15.4% saved)

sample113.0ms (0.1%)

Algorithm
intervals
Results
49.0ms94×body1024valid
17.0ms101×body128valid
16.0ms42×body512valid
5.0ms19×body256valid
5.0ms38×body128invalid
3.0msbody1024invalid
2.0msbody512invalid
1.0msbody256invalid
Compiler

Compiled 51 to 46 computations (9.8% saved)

simplify219.0ms (0.2%)

Algorithm
egg-herbie
Rules
701×distribute-rgt-in_binary64_710
559×times-frac_binary64_766
480×associate-/r/_binary64_706
421×associate-/r*_binary64_704
393×distribute-rgt-out_binary64_713
373×associate-/l*_binary64_705
317×distribute-lft-in_binary64_709
234×*-commutative_binary64_691
145×distribute-lft-out_binary64_711
122×associate-/l/_binary64_707
101×associate-*l/_binary64_703
94×associate-*l*_binary64_701
90×associate-*r*_binary64_700
78×associate-*r/_binary64_702
45×/-rgt-identity_binary64_751
26×*-lft-identity_binary64_749
25×unswap-sqr_binary64_728
18×*-rgt-identity_binary64_750
17×sqr-pow_binary64_732
16×distribute-rgt1-in_binary64_716
11×pow-sqr_binary64_733
remove-double-div_binary64_736 associate-+l+_binary64_693
cube-unmult_binary64_797 swap-sqr_binary64_727 distribute-lft1-in_binary64_715 associate-+r+_binary64_692
pow-plus_binary64_823
div-exp_binary64_811 prod-exp_binary64_809
rec-exp_binary64_810
unpow3_binary64_826 unpow2_binary64_825 unpow1_binary64_818 1-exp_binary64_804 cube-mult_binary64_790 +-rgt-identity_binary64_745 *-inverses_binary64_740 count-2_binary64_708 +-commutative_binary64_690
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_1023 erf-erfc_binary64_1022 erf-odd_binary64_1021 if-if-and-not_binary64_1020 if-if-and_binary64_1019 if-if-or-not_binary64_1018 if-if-or_binary64_1017 if-not_binary64_1016 if-same_binary64_1015 if-false_binary64_1014 if-true_binary64_1013 not-gte_binary64_1012 not-lte_binary64_1011 not-gt_binary64_1010 not-lt_binary64_1009 gte-same_binary64_1008 lte-same_binary64_1007 gt-same_binary64_1006 lt-same_binary64_1005 sinh---cosh_binary64_952 sinh-+-cosh_binary64_951 sinh-cosh_binary64_950 tanh-def-c_binary64_949 tanh-def-b_binary64_948 tanh-def-a_binary64_947 cosh-def_binary64_946 sinh-def_binary64_945 tan-neg_binary64_892 cos-neg_binary64_891 sin-neg_binary64_890 tan-0_binary64_889 cos-0_binary64_888 sin-0_binary64_887 hang-m-tan_binary64_886 hang-p-tan_binary64_885 hang-m0-tan_binary64_884 hang-p0-tan_binary64_883 hang-0m-tan_binary64_882 hang-0p-tan_binary64_881 tan-+PI/2_binary64_880 tan-+PI_binary64_879 tan-PI_binary64_878 tan-PI/3_binary64_877 tan-PI/4_binary64_876 tan-PI/6_binary64_875 cos-+PI/2_binary64_874 cos-+PI_binary64_873 cos-PI_binary64_872 cos-PI/2_binary64_871 cos-PI/3_binary64_870 cos-PI/4_binary64_869 cos-PI/6_binary64_868 sin-+PI/2_binary64_867 sin-+PI_binary64_866 sin-PI_binary64_865 sin-PI/2_binary64_864 sin-PI/3_binary64_863 sin-PI/4_binary64_862 sin-PI/6_binary64_861 sub-1-sin_binary64_860 sub-1-cos_binary64_859 -1-add-sin_binary64_858 -1-add-cos_binary64_857 1-sub-sin_binary64_856 1-sub-cos_binary64_855 cos-sin-sum_binary64_854 log-E_binary64_850 log-pow_binary64_849 log-rec_binary64_848 log-div_binary64_847 log-prod_binary64_846 pow-base-0_binary64_844 unpow1/3_binary64_827 unpow1/2_binary64_824 exp-to-pow_binary64_822 pow-base-1_binary64_820 unpow0_binary64_819 unpow-1_binary64_817 exp-lft-cube_binary64_816 exp-lft-sqr_binary64_815 exp-cbrt_binary64_814 exp-sqrt_binary64_813 exp-prod_binary64_812 exp-diff_binary64_808 exp-neg_binary64_807 exp-sum_binary64_806 e-exp-1_binary64_805 exp-1-e_binary64_803 exp-0_binary64_802 rem-log-exp_binary64_801 rem-exp-log_binary64_800 cube-div_binary64_789 cube-prod_binary64_788 cube-neg_binary64_787 rem-3cbrt-rft_binary64_786 rem-3cbrt-lft_binary64_785 rem-cbrt-cube_binary64_784 rem-cube-cbrt_binary64_783 sqr-abs_binary64_775 sqr-neg_binary64_774 rem-sqrt-square_binary64_773 rem-square-sqrt_binary64_772 div-sub_binary64_765 neg-mul-1_binary64_756 neg-sub0_binary64_755 unsub-neg_binary64_754 sub-neg_binary64_753 mul-1-neg_binary64_752 remove-double-neg_binary64_748 sub0-neg_binary64_747 --rgt-identity_binary64_746 +-lft-identity_binary64_744 mul0-rgt_binary64_743 mul0-lft_binary64_742 div0_binary64_741 +-inverses_binary64_739 lft-mult-inverse_binary64_738 rgt-mult-inverse_binary64_737 difference-of-sqr--1_binary64_731 difference-of-sqr-1_binary64_730 difference-of-squares_binary64_729 cancel-sign-sub-inv_binary64_726 cancel-sign-sub_binary64_725 distribute-neg-frac_binary64_724 distribute-frac-neg_binary64_723 distribute-neg-out_binary64_722 distribute-neg-in_binary64_721 distribute-rgt-neg-out_binary64_720 distribute-lft-neg-out_binary64_719 distribute-rgt-neg-in_binary64_718 distribute-lft-neg-in_binary64_717 distribute-rgt-out--_binary64_714 distribute-lft-out--_binary64_712 associate--r-_binary64_699 associate--l-_binary64_698 associate--l+_binary64_697 associate--r+_binary64_696 associate-+l-_binary64_695 associate-+r-_binary64_694
Counts
1 → 4
Iterations

Useful iterations: 2 (0.0ms)

IterNodesCost
02038
15338
217835
388235
4377335

prune19.0ms (0%)

Pruning

5 alts after pruning (5 fresh and 0 done)

PrunedKeptTotal
New044
Fresh011
Picked000
Done000
Total055
Error
29.7b
Counts
5 → 5
Compiler

Compiled 217 to 160 computations (26.3% saved)

localize25.0ms (0%)

Local error

Found 4 expressions with local error:

6.7b
(*.f64 (pow.f64 t 3) (*.f64 (sin.f64 k) (tan.f64 k)))
7.2b
(*.f64 (/.f64 (/.f64 2 (+.f64 2 (pow.f64 (/.f64 k t) 2))) (*.f64 (pow.f64 t 3) (*.f64 (sin.f64 k) (tan.f64 k)))) l)
7.3b
(*.f64 l (*.f64 (/.f64 (/.f64 2 (+.f64 2 (pow.f64 (/.f64 k t) 2))) (*.f64 (pow.f64 t 3) (*.f64 (sin.f64 k) (tan.f64 k)))) l))
15.6b
(/.f64 (/.f64 2 (+.f64 2 (pow.f64 (/.f64 k t) 2))) (*.f64 (pow.f64 t 3) (*.f64 (sin.f64 k) (tan.f64 k))))

rewrite564.0ms (0.5%)

Algorithm
rewrite-expression-head
Error
23.3b
Rules
213×add-exp-log_binary64_798
109×prod-exp_binary64_809
97×add-cbrt-cube_binary64_796
72×times-frac_binary64_766
63×div-exp_binary64_811
52×*-un-lft-identity_binary64_760
43×cbrt-unprod_binary64_793
38×associate-*l*_binary64_701
36×add-sqr-sqrt_binary64_782
34×add-cube-cbrt_binary64_795
27×cbrt-undiv_binary64_794
18×associate-/l*_binary64_705
14×pow-to-exp_binary64_829 pow-exp_binary64_828
11×pow1_binary64_821
distribute-lft-out_binary64_711
associate-/r/_binary64_706
associate-*r/_binary64_702
div-inv_binary64_757 associate-*r*_binary64_700
add-log-exp_binary64_799 pow-prod-down_binary64_831
flip3-+_binary64_763 flip-+_binary64_734 tan-quot_binary64_919 *-commutative_binary64_691 unpow-prod-down_binary64_839 cube-prod_binary64_788
associate-*l/_binary64_703
frac-2neg_binary64_771 clear-num_binary64_759 associate-/l/_binary64_707 associate-/r*_binary64_704 unswap-sqr_binary64_728 unpow3_binary64_826 cube-mult_binary64_790 sqr-pow_binary64_732
Counts
4 → 197
Calls

4 calls:

27.0ms
(*.f64 (/.f64 (/.f64 2 (+.f64 2 (pow.f64 (/.f64 k t) 2))) (*.f64 (pow.f64 t 3) (*.f64 (sin.f64 k) (tan.f64 k)))) l)
25.0ms
(*.f64 l (*.f64 (/.f64 (/.f64 2 (+.f64 2 (pow.f64 (/.f64 k t) 2))) (*.f64 (pow.f64 t 3) (*.f64 (sin.f64 k) (tan.f64 k)))) l))
21.0ms
(/.f64 (/.f64 2 (+.f64 2 (pow.f64 (/.f64 k t) 2))) (*.f64 (pow.f64 t 3) (*.f64 (sin.f64 k) (tan.f64 k))))
14.0ms
(*.f64 (pow.f64 t 3) (*.f64 (sin.f64 k) (tan.f64 k)))
Compiler

Compiled 7149 to 3932 computations (45% saved)

series2.5s (2.4%)

Error
18.2b
Counts
4 → 33
Calls

4 calls:

983.0ms
(*.f64 (/.f64 (/.f64 2 (+.f64 2 (pow.f64 (/.f64 k t) 2))) (*.f64 (pow.f64 t 3) (*.f64 (sin.f64 k) (tan.f64 k)))) l)
821.0ms
(*.f64 l (*.f64 (/.f64 (/.f64 2 (+.f64 2 (pow.f64 (/.f64 k t) 2))) (*.f64 (pow.f64 t 3) (*.f64 (sin.f64 k) (tan.f64 k)))) l))
335.0ms
(*.f64 (pow.f64 t 3) (*.f64 (sin.f64 k) (tan.f64 k)))
307.0ms
(/.f64 (/.f64 2 (+.f64 2 (pow.f64 (/.f64 k t) 2))) (*.f64 (pow.f64 t 3) (*.f64 (sin.f64 k) (tan.f64 k))))
Compiler

Compiled 2474 to 1889 computations (23.6% saved)

simplify1.5s (1.4%)

Algorithm
egg-herbie
Rules
370×associate-/r*_binary64_704
341×associate-*l*_binary64_701
303×associate-*r*_binary64_700
279×times-frac_binary64_766
264×associate-/l*_binary64_705
238×unswap-sqr_binary64_728
187×associate-*l/_binary64_703
153×*-commutative_binary64_691
140×associate-*r/_binary64_702
112×associate-/l/_binary64_707
103×cancel-sign-sub-inv_binary64_726
99×log-prod_binary64_846
78×exp-prod_binary64_812 sqr-pow_binary64_732
72×sub-neg_binary64_753 associate-/r/_binary64_706
65×distribute-neg-frac_binary64_724
62×swap-sqr_binary64_727
52×log-div_binary64_847
51×cube-prod_binary64_788
45×neg-mul-1_binary64_756
44×neg-sub0_binary64_755
41×pow-sqr_binary64_733
40×cube-div_binary64_789 distribute-rgt-in_binary64_710
36×distribute-lft-in_binary64_709
27×*-rgt-identity_binary64_750
24×+-commutative_binary64_690
23×div-sub_binary64_765
20×pow-plus_binary64_823
17×cube-unmult_binary64_797
13×distribute-rgt-neg-in_binary64_718
12×associate--r+_binary64_696
11×log-pow_binary64_849 distribute-lft-neg-in_binary64_717
10×unsub-neg_binary64_754 associate-+r+_binary64_692
unpow3_binary64_826 div-exp_binary64_811 prod-exp_binary64_809 distribute-neg-in_binary64_721
*-lft-identity_binary64_749
associate-+l-_binary64_695
/-rgt-identity_binary64_751 associate--l+_binary64_697 associate-+l+_binary64_693
unpow2_binary64_825 unpow1_binary64_818 cube-mult_binary64_790 associate-+r-_binary64_694
rem-sqrt-square_binary64_773 associate--l-_binary64_698
rec-exp_binary64_810
difference-of-squares_binary64_729 distribute-lft-neg-out_binary64_719
log-rec_binary64_848 exp-sqrt_binary64_813 1-exp_binary64_804 exp-1-e_binary64_803 rem-log-exp_binary64_801 rem-cbrt-cube_binary64_784 rem-cube-cbrt_binary64_783 rem-square-sqrt_binary64_772 *-inverses_binary64_740 distribute-rgt-out--_binary64_714
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_1023 erf-erfc_binary64_1022 erf-odd_binary64_1021 if-if-and-not_binary64_1020 if-if-and_binary64_1019 if-if-or-not_binary64_1018 if-if-or_binary64_1017 if-not_binary64_1016 if-same_binary64_1015 if-false_binary64_1014 if-true_binary64_1013 not-gte_binary64_1012 not-lte_binary64_1011 not-gt_binary64_1010 not-lt_binary64_1009 gte-same_binary64_1008 lte-same_binary64_1007 gt-same_binary64_1006 lt-same_binary64_1005 sinh---cosh_binary64_952 sinh-+-cosh_binary64_951 sinh-cosh_binary64_950 tanh-def-c_binary64_949 tanh-def-b_binary64_948 tanh-def-a_binary64_947 cosh-def_binary64_946 sinh-def_binary64_945 tan-neg_binary64_892 cos-neg_binary64_891 sin-neg_binary64_890 tan-0_binary64_889 cos-0_binary64_888 sin-0_binary64_887 hang-m-tan_binary64_886 hang-p-tan_binary64_885 hang-m0-tan_binary64_884 hang-p0-tan_binary64_883 hang-0m-tan_binary64_882 hang-0p-tan_binary64_881 tan-+PI/2_binary64_880 tan-+PI_binary64_879 tan-PI_binary64_878 tan-PI/3_binary64_877 tan-PI/4_binary64_876 tan-PI/6_binary64_875 cos-+PI/2_binary64_874 cos-+PI_binary64_873 cos-PI_binary64_872 cos-PI/2_binary64_871 cos-PI/3_binary64_870 cos-PI/4_binary64_869 cos-PI/6_binary64_868 sin-+PI/2_binary64_867 sin-+PI_binary64_866 sin-PI_binary64_865 sin-PI/2_binary64_864 sin-PI/3_binary64_863 sin-PI/4_binary64_862 sin-PI/6_binary64_861 sub-1-sin_binary64_860 sub-1-cos_binary64_859 -1-add-sin_binary64_858 -1-add-cos_binary64_857 1-sub-sin_binary64_856 1-sub-cos_binary64_855 cos-sin-sum_binary64_854 log-E_binary64_850 pow-base-0_binary64_844 unpow1/3_binary64_827 unpow1/2_binary64_824 exp-to-pow_binary64_822 pow-base-1_binary64_820 unpow0_binary64_819 unpow-1_binary64_817 exp-lft-cube_binary64_816 exp-lft-sqr_binary64_815 exp-cbrt_binary64_814 exp-diff_binary64_808 exp-neg_binary64_807 exp-sum_binary64_806 e-exp-1_binary64_805 exp-0_binary64_802 rem-exp-log_binary64_800 cube-neg_binary64_787 rem-3cbrt-rft_binary64_786 rem-3cbrt-lft_binary64_785 sqr-abs_binary64_775 sqr-neg_binary64_774 mul-1-neg_binary64_752 remove-double-neg_binary64_748 sub0-neg_binary64_747 --rgt-identity_binary64_746 +-rgt-identity_binary64_745 +-lft-identity_binary64_744 mul0-rgt_binary64_743 mul0-lft_binary64_742 div0_binary64_741 +-inverses_binary64_739 lft-mult-inverse_binary64_738 rgt-mult-inverse_binary64_737 remove-double-div_binary64_736 difference-of-sqr--1_binary64_731 difference-of-sqr-1_binary64_730 cancel-sign-sub_binary64_725 distribute-frac-neg_binary64_723 distribute-neg-out_binary64_722 distribute-rgt-neg-out_binary64_720 distribute-rgt1-in_binary64_716 distribute-lft1-in_binary64_715 distribute-rgt-out_binary64_713 distribute-lft-out--_binary64_712 distribute-lft-out_binary64_711 count-2_binary64_708 associate--r-_binary64_699
Counts
230 → 480
Iterations

Useful iterations: 1 (0.0ms)

IterNodesCost
03288681
18777013
239247013

prune1.3s (1.3%)

Pruning

15 alts after pruning (15 fresh and 0 done)

PrunedKeptTotal
New46614480
Fresh314
Picked101
Done000
Total47015485
Error
10.7b
Counts
485 → 15
Compiler

Compiled 16687 to 9532 computations (42.9% saved)

localize16.0ms (0%)

Local error

Found 4 expressions with local error:

0.7b
(/.f64 (cos.f64 k) (/.f64 (*.f64 k k) l))
4.8b
(/.f64 (/.f64 (/.f64 (cos.f64 k) (/.f64 (*.f64 k k) l)) (pow.f64 (sin.f64 k) 2)) t)
7.0b
(*.f64 l (*.f64 2 (/.f64 (/.f64 (/.f64 (cos.f64 k) (/.f64 (*.f64 k k) l)) (pow.f64 (sin.f64 k) 2)) t)))
8.9b
(/.f64 (*.f64 k k) l)

rewrite2.5s (2.4%)

Algorithm
rewrite-expression-head
Error
7.1b
Rules
2464×times-frac_binary64_766
896×add-cube-cbrt_binary64_795 add-sqr-sqrt_binary64_782 *-un-lft-identity_binary64_760
312×unpow-prod-down_binary64_839
216×associate-/l*_binary64_705
153×add-exp-log_binary64_798
139×div-inv_binary64_757
104×unpow2_binary64_825 sqr-pow_binary64_732
87×div-exp_binary64_811
73×add-cbrt-cube_binary64_796
37×prod-exp_binary64_809
35×cbrt-undiv_binary64_794
33×associate-/r/_binary64_706
17×cbrt-unprod_binary64_793
13×associate-/r*_binary64_704
pow1_binary64_821
pow-to-exp_binary64_829 pow-exp_binary64_828
add-log-exp_binary64_799
frac-2neg_binary64_771 clear-num_binary64_759 pow-prod-down_binary64_831 associate-*l*_binary64_701
associate-*r/_binary64_702
associate-*r*_binary64_700 *-commutative_binary64_691 associate-/l/_binary64_707
Counts
4 → 986
Calls

4 calls:

77.0ms
(*.f64 l (*.f64 2 (/.f64 (/.f64 (/.f64 (cos.f64 k) (/.f64 (*.f64 k k) l)) (pow.f64 (sin.f64 k) 2)) t)))
63.0ms
(/.f64 (/.f64 (/.f64 (cos.f64 k) (/.f64 (*.f64 k k) l)) (pow.f64 (sin.f64 k) 2)) t)
12.0ms
(/.f64 (cos.f64 k) (/.f64 (*.f64 k k) l))
5.0ms
(/.f64 (*.f64 k k) l)
Compiler

Compiled 37284 to 13664 computations (63.4% saved)

series1.9s (1.8%)

Error
10.7b
Counts
4 → 33
Calls

4 calls:

834.0ms
(*.f64 l (*.f64 2 (/.f64 (/.f64 (/.f64 (cos.f64 k) (/.f64 (*.f64 k k) l)) (pow.f64 (sin.f64 k) 2)) t)))
713.0ms
(/.f64 (/.f64 (/.f64 (cos.f64 k) (/.f64 (*.f64 k k) l)) (pow.f64 (sin.f64 k) 2)) t)
181.0ms
(/.f64 (cos.f64 k) (/.f64 (*.f64 k k) l))
109.0ms
(/.f64 (*.f64 k k) l)
Compiler

Compiled 1829 to 1406 computations (23.1% saved)

simplify4.5s (4.2%)

Algorithm
egg-herbie
Rules
573×associate-/r/_binary64_706
346×associate-/l*_binary64_705
267×times-frac_binary64_766
258×associate-*l/_binary64_703
230×associate-/r*_binary64_704
208×*-commutative_binary64_691
206×/-rgt-identity_binary64_751
204×associate-*r*_binary64_700
131×associate-*l*_binary64_701
110×associate-*r/_binary64_702
62×sub-neg_binary64_753
51×log-prod_binary64_846
37×log-div_binary64_847
33×neg-mul-1_binary64_756
31×neg-sub0_binary64_755
30×cube-prod_binary64_788
26×pow-plus_binary64_823
24×exp-prod_binary64_812
19×sqr-pow_binary64_732
18×cube-unmult_binary64_797
16×div-exp_binary64_811 prod-exp_binary64_809 +-commutative_binary64_690
15×log-pow_binary64_849
14×cube-div_binary64_789
13×pow-sqr_binary64_733 distribute-neg-frac_binary64_724
10×div-sub_binary64_765 distribute-rgt-neg-in_binary64_718
cancel-sign-sub-inv_binary64_726
associate-+r-_binary64_694 associate-+l+_binary64_693
unpow2_binary64_825 associate-+l-_binary64_695
unpow1_binary64_818 swap-sqr_binary64_727 distribute-lft-neg-in_binary64_717 associate--l-_binary64_698 associate--l+_binary64_697
exp-lft-sqr_binary64_815 unsub-neg_binary64_754 associate-+r+_binary64_692
rec-exp_binary64_810 rem-sqrt-square_binary64_773 unswap-sqr_binary64_728 distribute-lft-neg-out_binary64_719
pow-base-1_binary64_820 associate--r+_binary64_696
log-rec_binary64_848 distribute-neg-in_binary64_721
1-exp_binary64_804 rem-log-exp_binary64_801 rem-3cbrt-rft_binary64_786 rem-3cbrt-lft_binary64_785 rem-square-sqrt_binary64_772 *-inverses_binary64_740 count-2_binary64_708 associate--r-_binary64_699
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_1023 erf-erfc_binary64_1022 erf-odd_binary64_1021 if-if-and-not_binary64_1020 if-if-and_binary64_1019 if-if-or-not_binary64_1018 if-if-or_binary64_1017 if-not_binary64_1016 if-same_binary64_1015 if-false_binary64_1014 if-true_binary64_1013 not-gte_binary64_1012 not-lte_binary64_1011 not-gt_binary64_1010 not-lt_binary64_1009 gte-same_binary64_1008 lte-same_binary64_1007 gt-same_binary64_1006 lt-same_binary64_1005 sinh---cosh_binary64_952 sinh-+-cosh_binary64_951 sinh-cosh_binary64_950 tanh-def-c_binary64_949 tanh-def-b_binary64_948 tanh-def-a_binary64_947 cosh-def_binary64_946 sinh-def_binary64_945 tan-neg_binary64_892 cos-neg_binary64_891 sin-neg_binary64_890 tan-0_binary64_889 cos-0_binary64_888 sin-0_binary64_887 hang-m-tan_binary64_886 hang-p-tan_binary64_885 hang-m0-tan_binary64_884 hang-p0-tan_binary64_883 hang-0m-tan_binary64_882 hang-0p-tan_binary64_881 tan-+PI/2_binary64_880 tan-+PI_binary64_879 tan-PI_binary64_878 tan-PI/3_binary64_877 tan-PI/4_binary64_876 tan-PI/6_binary64_875 cos-+PI/2_binary64_874 cos-+PI_binary64_873 cos-PI_binary64_872 cos-PI/2_binary64_871 cos-PI/3_binary64_870 cos-PI/4_binary64_869 cos-PI/6_binary64_868 sin-+PI/2_binary64_867 sin-+PI_binary64_866 sin-PI_binary64_865 sin-PI/2_binary64_864 sin-PI/3_binary64_863 sin-PI/4_binary64_862 sin-PI/6_binary64_861 sub-1-sin_binary64_860 sub-1-cos_binary64_859 -1-add-sin_binary64_858 -1-add-cos_binary64_857 1-sub-sin_binary64_856 1-sub-cos_binary64_855 cos-sin-sum_binary64_854 log-E_binary64_850 pow-base-0_binary64_844 unpow1/3_binary64_827 unpow3_binary64_826 unpow1/2_binary64_824 exp-to-pow_binary64_822 unpow0_binary64_819 unpow-1_binary64_817 exp-lft-cube_binary64_816 exp-cbrt_binary64_814 exp-sqrt_binary64_813 exp-diff_binary64_808 exp-neg_binary64_807 exp-sum_binary64_806 e-exp-1_binary64_805 exp-1-e_binary64_803 exp-0_binary64_802 rem-exp-log_binary64_800 cube-mult_binary64_790 cube-neg_binary64_787 rem-cbrt-cube_binary64_784 rem-cube-cbrt_binary64_783 sqr-abs_binary64_775 sqr-neg_binary64_774 mul-1-neg_binary64_752 *-rgt-identity_binary64_750 *-lft-identity_binary64_749 remove-double-neg_binary64_748 sub0-neg_binary64_747 --rgt-identity_binary64_746 +-rgt-identity_binary64_745 +-lft-identity_binary64_744 mul0-rgt_binary64_743 mul0-lft_binary64_742 div0_binary64_741 +-inverses_binary64_739 lft-mult-inverse_binary64_738 rgt-mult-inverse_binary64_737 remove-double-div_binary64_736 difference-of-sqr--1_binary64_731 difference-of-sqr-1_binary64_730 difference-of-squares_binary64_729 cancel-sign-sub_binary64_725 distribute-frac-neg_binary64_723 distribute-neg-out_binary64_722 distribute-rgt-neg-out_binary64_720 distribute-rgt1-in_binary64_716 distribute-lft1-in_binary64_715 distribute-rgt-out--_binary64_714 distribute-rgt-out_binary64_713 distribute-lft-out--_binary64_712 distribute-lft-out_binary64_711 distribute-rgt-in_binary64_710 distribute-lft-in_binary64_709 associate-/l/_binary64_707
Counts
1019 → 5033
Iterations

Useful iterations: 2 (0.0ms)

IterNodesCost
0197244227
1274239929
2470639851

prune14.1s (13.4%)

Pruning

19 alts after pruning (19 fresh and 0 done)

PrunedKeptTotal
New5022115033
Fresh6814
Picked101
Done000
Total5029195048
Error
7.2b
Counts
5048 → 19
Compiler

Compiled 189858 to 58666 computations (69.1% saved)

localize15.0ms (0%)

Local error

Found 4 expressions with local error:

0.5b
(/.f64 (cos.f64 k) (/.f64 k l))
0.9b
(/.f64 (/.f64 (cos.f64 k) (/.f64 k l)) (pow.f64 (sin.f64 k) 2))
7.0b
(*.f64 l (*.f64 2 (*.f64 (/.f64 1 k) (/.f64 (/.f64 (/.f64 (cos.f64 k) (/.f64 k l)) (pow.f64 (sin.f64 k) 2)) t))))
9.3b
(/.f64 (/.f64 (/.f64 (cos.f64 k) (/.f64 k l)) (pow.f64 (sin.f64 k) 2)) t)

rewrite7.4s (7.1%)

Algorithm
rewrite-expression-head
Error
4.8b
Rules
5609×times-frac_binary64_766
2285×add-cube-cbrt_binary64_795 add-sqr-sqrt_binary64_782 *-un-lft-identity_binary64_760
663×unpow-prod-down_binary64_839
403×associate-/l*_binary64_705
360×add-exp-log_binary64_798
221×unpow2_binary64_825 sqr-pow_binary64_732
183×div-exp_binary64_811
175×div-inv_binary64_757
135×prod-exp_binary64_809
102×add-cbrt-cube_binary64_796
44×cbrt-undiv_binary64_794
42×associate-/r/_binary64_706
33×cbrt-unprod_binary64_793
24×associate-/r*_binary64_704
18×pow-to-exp_binary64_829 pow-exp_binary64_828
13×pow1_binary64_821
11×1-exp_binary64_804 rec-exp_binary64_810
associate-*r/_binary64_702
pow-prod-down_binary64_831
add-log-exp_binary64_799
frac-2neg_binary64_771 clear-num_binary64_759 associate-*l*_binary64_701
associate-/l/_binary64_707
frac-times_binary64_770 associate-*l/_binary64_703 associate-*r*_binary64_700 *-commutative_binary64_691
Counts
4 → 2025
Calls

4 calls:

136.0ms
(*.f64 l (*.f64 2 (*.f64 (/.f64 1 k) (/.f64 (/.f64 (/.f64 (cos.f64 k) (/.f64 k l)) (pow.f64 (sin.f64 k) 2)) t))))
93.0ms
(/.f64 (/.f64 (/.f64 (cos.f64 k) (/.f64 k l)) (pow.f64 (sin.f64 k) 2)) t)
24.0ms
(/.f64 (/.f64 (cos.f64 k) (/.f64 k l)) (pow.f64 (sin.f64 k) 2))
8.0ms
(/.f64 (cos.f64 k) (/.f64 k l))
Compiler

Compiled 83394 to 34773 computations (58.3% saved)

series2.1s (2%)

Error
7.2b
Counts
4 → 34
Calls

4 calls:

837.0ms
(*.f64 l (*.f64 2 (*.f64 (/.f64 1 k) (/.f64 (/.f64 (/.f64 (cos.f64 k) (/.f64 k l)) (pow.f64 (sin.f64 k) 2)) t))))
703.0ms
(/.f64 (/.f64 (/.f64 (cos.f64 k) (/.f64 k l)) (pow.f64 (sin.f64 k) 2)) t)
339.0ms
(/.f64 (/.f64 (cos.f64 k) (/.f64 k l)) (pow.f64 (sin.f64 k) 2))
169.0ms
(/.f64 (cos.f64 k) (/.f64 k l))
Compiler

Compiled 2011 to 1499 computations (25.5% saved)

simplify6.2s (5.9%)

Algorithm
egg-herbie
Rules
701×associate-/l*_binary64_705
500×times-frac_binary64_766
446×associate-*l/_binary64_703
383×associate-/r/_binary64_706
359×/-rgt-identity_binary64_751
349×associate-/r*_binary64_704
67×*-commutative_binary64_691
44×associate-*l*_binary64_701 associate-*r*_binary64_700
27×associate-*r/_binary64_702
24×sub-neg_binary64_753
21×sqr-pow_binary64_732
20×neg-mul-1_binary64_756 neg-sub0_binary64_755
17×log-div_binary64_847 cancel-sign-sub-inv_binary64_726 distribute-rgt-neg-in_binary64_718
16×log-prod_binary64_846
15×swap-sqr_binary64_727
14×cube-unmult_binary64_797
12×distribute-neg-frac_binary64_724 distribute-lft-neg-in_binary64_717
exp-prod_binary64_812
unpow2_binary64_825
unpow1_binary64_818 pow-sqr_binary64_733
*-lft-identity_binary64_749 unswap-sqr_binary64_728 distribute-lft-neg-out_binary64_719
associate--l-_binary64_698 associate-+l-_binary64_695 associate-+r+_binary64_692
pow-plus_binary64_823 *-rgt-identity_binary64_750 +-commutative_binary64_690
log-pow_binary64_849 log-rec_binary64_848 pow-base-1_binary64_820 div-sub_binary64_765 remove-double-div_binary64_736 associate-+r-_binary64_694
unpow3_binary64_826 div-exp_binary64_811 rec-exp_binary64_810 prod-exp_binary64_809 1-exp_binary64_804 rem-log-exp_binary64_801 cube-mult_binary64_790 rem-sqrt-square_binary64_773 rem-square-sqrt_binary64_772 unsub-neg_binary64_754 sub0-neg_binary64_747 *-inverses_binary64_740 distribute-neg-in_binary64_721 associate--r-_binary64_699
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_1023 erf-erfc_binary64_1022 erf-odd_binary64_1021 if-if-and-not_binary64_1020 if-if-and_binary64_1019 if-if-or-not_binary64_1018 if-if-or_binary64_1017 if-not_binary64_1016 if-same_binary64_1015 if-false_binary64_1014 if-true_binary64_1013 not-gte_binary64_1012 not-lte_binary64_1011 not-gt_binary64_1010 not-lt_binary64_1009 gte-same_binary64_1008 lte-same_binary64_1007 gt-same_binary64_1006 lt-same_binary64_1005 sinh---cosh_binary64_952 sinh-+-cosh_binary64_951 sinh-cosh_binary64_950 tanh-def-c_binary64_949 tanh-def-b_binary64_948 tanh-def-a_binary64_947 cosh-def_binary64_946 sinh-def_binary64_945 tan-neg_binary64_892 cos-neg_binary64_891 sin-neg_binary64_890 tan-0_binary64_889 cos-0_binary64_888 sin-0_binary64_887 hang-m-tan_binary64_886 hang-p-tan_binary64_885 hang-m0-tan_binary64_884 hang-p0-tan_binary64_883 hang-0m-tan_binary64_882 hang-0p-tan_binary64_881 tan-+PI/2_binary64_880 tan-+PI_binary64_879 tan-PI_binary64_878 tan-PI/3_binary64_877 tan-PI/4_binary64_876 tan-PI/6_binary64_875 cos-+PI/2_binary64_874 cos-+PI_binary64_873 cos-PI_binary64_872 cos-PI/2_binary64_871 cos-PI/3_binary64_870 cos-PI/4_binary64_869 cos-PI/6_binary64_868 sin-+PI/2_binary64_867 sin-+PI_binary64_866 sin-PI_binary64_865 sin-PI/2_binary64_864 sin-PI/3_binary64_863 sin-PI/4_binary64_862 sin-PI/6_binary64_861 sub-1-sin_binary64_860 sub-1-cos_binary64_859 -1-add-sin_binary64_858 -1-add-cos_binary64_857 1-sub-sin_binary64_856 1-sub-cos_binary64_855 cos-sin-sum_binary64_854 log-E_binary64_850 pow-base-0_binary64_844 unpow1/3_binary64_827 unpow1/2_binary64_824 exp-to-pow_binary64_822 unpow0_binary64_819 unpow-1_binary64_817 exp-lft-cube_binary64_816 exp-lft-sqr_binary64_815 exp-cbrt_binary64_814 exp-sqrt_binary64_813 exp-diff_binary64_808 exp-neg_binary64_807 exp-sum_binary64_806 e-exp-1_binary64_805 exp-1-e_binary64_803 exp-0_binary64_802 rem-exp-log_binary64_800 cube-div_binary64_789 cube-prod_binary64_788 cube-neg_binary64_787 rem-3cbrt-rft_binary64_786 rem-3cbrt-lft_binary64_785 rem-cbrt-cube_binary64_784 rem-cube-cbrt_binary64_783 sqr-abs_binary64_775 sqr-neg_binary64_774 mul-1-neg_binary64_752 remove-double-neg_binary64_748 --rgt-identity_binary64_746 +-rgt-identity_binary64_745 +-lft-identity_binary64_744 mul0-rgt_binary64_743 mul0-lft_binary64_742 div0_binary64_741 +-inverses_binary64_739 lft-mult-inverse_binary64_738 rgt-mult-inverse_binary64_737 difference-of-sqr--1_binary64_731 difference-of-sqr-1_binary64_730 difference-of-squares_binary64_729 cancel-sign-sub_binary64_725 distribute-frac-neg_binary64_723 distribute-neg-out_binary64_722 distribute-rgt-neg-out_binary64_720 distribute-rgt1-in_binary64_716 distribute-lft1-in_binary64_715 distribute-rgt-out--_binary64_714 distribute-rgt-out_binary64_713 distribute-lft-out--_binary64_712 distribute-lft-out_binary64_711 distribute-rgt-in_binary64_710 distribute-lft-in_binary64_709 count-2_binary64_708 associate-/l/_binary64_707 associate--l+_binary64_697 associate--r+_binary64_696 associate-+l+_binary64_693
Counts
2059 → 7233
Iterations

Useful iterations: 1 (0.0ms)

IterNodesCost
0327989539
1440580711

prune31.6s (30%)

Pruning

20 alts after pruning (19 fresh and 1 done)

PrunedKeptTotal
New722677233
Fresh61218
Picked011
Done000
Total7232207252
Error
4.8b
Counts
7252 → 20
Compiler

Compiled 284288 to 102283 computations (64% saved)

localize18.0ms (0%)

Local error

Found 4 expressions with local error:

2.2b
(/.f64 (*.f64 (*.f64 l 2) (/.f64 (*.f64 (/.f64 (cos.f64 k) k) (/.f64 l (pow.f64 (sin.f64 k) 2))) t)) k)
3.3b
(*.f64 (*.f64 l 2) (/.f64 (*.f64 (/.f64 (cos.f64 k) k) (/.f64 l (pow.f64 (sin.f64 k) 2))) t))
3.6b
(/.f64 l (pow.f64 (sin.f64 k) 2))
9.3b
(/.f64 (*.f64 (/.f64 (cos.f64 k) k) (/.f64 l (pow.f64 (sin.f64 k) 2))) t)

rewrite352.0ms (0.3%)

Algorithm
rewrite-expression-head
Error
4.8b
Rules
265×add-exp-log_binary64_798
150×add-cbrt-cube_binary64_796
119×div-exp_binary64_811
100×prod-exp_binary64_809
59×cbrt-undiv_binary64_794
56×cbrt-unprod_binary64_793
33×times-frac_binary64_766
27×add-cube-cbrt_binary64_795 add-sqr-sqrt_binary64_782 *-un-lft-identity_binary64_760
14×associate-/r*_binary64_704
12×unpow-prod-down_binary64_839
11×pow-to-exp_binary64_829 pow-exp_binary64_828
pow1_binary64_821
associate-*r*_binary64_700
associate-/l*_binary64_705
add-log-exp_binary64_799 div-inv_binary64_757 associate-/l/_binary64_707 unpow2_binary64_825 sqr-pow_binary64_732
frac-2neg_binary64_771 clear-num_binary64_759 associate-*r/_binary64_702 pow-prod-down_binary64_831
frac-times_binary64_770 associate-*l/_binary64_703 associate-*l*_binary64_701 *-commutative_binary64_691
Counts
4 → 186
Calls

4 calls:

18.0ms
(/.f64 (*.f64 (*.f64 l 2) (/.f64 (*.f64 (/.f64 (cos.f64 k) k) (/.f64 l (pow.f64 (sin.f64 k) 2))) t)) k)
16.0ms
(*.f64 (*.f64 l 2) (/.f64 (*.f64 (/.f64 (cos.f64 k) k) (/.f64 l (pow.f64 (sin.f64 k) 2))) t))
12.0ms
(/.f64 (*.f64 (/.f64 (cos.f64 k) k) (/.f64 l (pow.f64 (sin.f64 k) 2))) t)
6.0ms
(/.f64 l (pow.f64 (sin.f64 k) 2))
Compiler

Compiled 5818 to 2679 computations (54% saved)

series2.6s (2.4%)

Error
4.8b
Counts
4 → 37
Calls

4 calls:

813.0ms
(/.f64 (*.f64 (*.f64 l 2) (/.f64 (*.f64 (/.f64 (cos.f64 k) k) (/.f64 l (pow.f64 (sin.f64 k) 2))) t)) k)
782.0ms
(*.f64 (*.f64 l 2) (/.f64 (*.f64 (/.f64 (cos.f64 k) k) (/.f64 l (pow.f64 (sin.f64 k) 2))) t))
711.0ms
(/.f64 (*.f64 (/.f64 (cos.f64 k) k) (/.f64 l (pow.f64 (sin.f64 k) 2))) t)
212.0ms
(/.f64 l (pow.f64 (sin.f64 k) 2))
Compiler

Compiled 2064 to 1533 computations (25.7% saved)

simplify1.7s (1.6%)

Algorithm
egg-herbie
Rules
419×times-frac_binary64_766
302×associate-/l*_binary64_705
230×associate-*l*_binary64_701
221×log-div_binary64_847
220×associate-*r/_binary64_702
195×associate-/r*_binary64_704
187×associate-*l/_binary64_703
177×associate-/l/_binary64_707
163×associate-*r*_binary64_700
119×associate-+l+_binary64_693
116×associate-+l-_binary64_695
105×distribute-neg-frac_binary64_724
99×associate--l+_binary64_697 associate-+r+_binary64_692
98×*-commutative_binary64_691
94×associate-/r/_binary64_706
87×distribute-rgt-neg-in_binary64_718
86×log-prod_binary64_846
83×distribute-lft-neg-in_binary64_717
82×associate-+r-_binary64_694
75×cube-div_binary64_789
67×cancel-sign-sub-inv_binary64_726
66×unswap-sqr_binary64_728
65×sub-neg_binary64_753
61×associate--l-_binary64_698
60×+-commutative_binary64_690
54×sqr-pow_binary64_732
48×cube-prod_binary64_788
44×exp-prod_binary64_812 swap-sqr_binary64_727
43×*-rgt-identity_binary64_750
35×neg-mul-1_binary64_756
33×neg-sub0_binary64_755
31×log-pow_binary64_849
26×/-rgt-identity_binary64_751
19×*-lft-identity_binary64_749
18×pow-plus_binary64_823
17×log-rec_binary64_848 prod-exp_binary64_809
16×div-exp_binary64_811 cube-unmult_binary64_797
14×pow-sqr_binary64_733 associate--r-_binary64_699 associate--r+_binary64_696
12×distribute-lft-neg-out_binary64_719
11×div-sub_binary64_765
exp-lft-sqr_binary64_815
unpow2_binary64_825
unpow1_binary64_818
rem-sqrt-square_binary64_773 distribute-neg-in_binary64_721
rec-exp_binary64_810
pow-base-1_binary64_820 exp-sqrt_binary64_813 unsub-neg_binary64_754 distribute-rgt-neg-out_binary64_720 distribute-rgt-in_binary64_710
distribute-rgt-out--_binary64_714 distribute-rgt-out_binary64_713
unpow3_binary64_826 1-exp_binary64_804 exp-1-e_binary64_803 rem-log-exp_binary64_801 cube-mult_binary64_790 rem-3cbrt-rft_binary64_786 rem-3cbrt-lft_binary64_785 rem-square-sqrt_binary64_772 *-inverses_binary64_740 rgt-mult-inverse_binary64_737 distribute-rgt1-in_binary64_716 distribute-lft1-in_binary64_715
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_1023 erf-erfc_binary64_1022 erf-odd_binary64_1021 if-if-and-not_binary64_1020 if-if-and_binary64_1019 if-if-or-not_binary64_1018 if-if-or_binary64_1017 if-not_binary64_1016 if-same_binary64_1015 if-false_binary64_1014 if-true_binary64_1013 not-gte_binary64_1012 not-lte_binary64_1011 not-gt_binary64_1010 not-lt_binary64_1009 gte-same_binary64_1008 lte-same_binary64_1007 gt-same_binary64_1006 lt-same_binary64_1005 sinh---cosh_binary64_952 sinh-+-cosh_binary64_951 sinh-cosh_binary64_950 tanh-def-c_binary64_949 tanh-def-b_binary64_948 tanh-def-a_binary64_947 cosh-def_binary64_946 sinh-def_binary64_945 tan-neg_binary64_892 cos-neg_binary64_891 sin-neg_binary64_890 tan-0_binary64_889 cos-0_binary64_888 sin-0_binary64_887 hang-m-tan_binary64_886 hang-p-tan_binary64_885 hang-m0-tan_binary64_884 hang-p0-tan_binary64_883 hang-0m-tan_binary64_882 hang-0p-tan_binary64_881 tan-+PI/2_binary64_880 tan-+PI_binary64_879 tan-PI_binary64_878 tan-PI/3_binary64_877 tan-PI/4_binary64_876 tan-PI/6_binary64_875 cos-+PI/2_binary64_874 cos-+PI_binary64_873 cos-PI_binary64_872 cos-PI/2_binary64_871 cos-PI/3_binary64_870 cos-PI/4_binary64_869 cos-PI/6_binary64_868 sin-+PI/2_binary64_867 sin-+PI_binary64_866 sin-PI_binary64_865 sin-PI/2_binary64_864 sin-PI/3_binary64_863 sin-PI/4_binary64_862 sin-PI/6_binary64_861 sub-1-sin_binary64_860 sub-1-cos_binary64_859 -1-add-sin_binary64_858 -1-add-cos_binary64_857 1-sub-sin_binary64_856 1-sub-cos_binary64_855 cos-sin-sum_binary64_854 log-E_binary64_850 pow-base-0_binary64_844 unpow1/3_binary64_827 unpow1/2_binary64_824 exp-to-pow_binary64_822 unpow0_binary64_819 unpow-1_binary64_817 exp-lft-cube_binary64_816 exp-cbrt_binary64_814 exp-diff_binary64_808 exp-neg_binary64_807 exp-sum_binary64_806 e-exp-1_binary64_805 exp-0_binary64_802 rem-exp-log_binary64_800 cube-neg_binary64_787 rem-cbrt-cube_binary64_784 rem-cube-cbrt_binary64_783 sqr-abs_binary64_775 sqr-neg_binary64_774 mul-1-neg_binary64_752 remove-double-neg_binary64_748 sub0-neg_binary64_747 --rgt-identity_binary64_746 +-rgt-identity_binary64_745 +-lft-identity_binary64_744 mul0-rgt_binary64_743 mul0-lft_binary64_742 div0_binary64_741 +-inverses_binary64_739 lft-mult-inverse_binary64_738 remove-double-div_binary64_736 difference-of-sqr--1_binary64_731 difference-of-sqr-1_binary64_730 difference-of-squares_binary64_729 cancel-sign-sub_binary64_725 distribute-frac-neg_binary64_723 distribute-neg-out_binary64_722 distribute-lft-out--_binary64_712 distribute-lft-out_binary64_711 distribute-lft-in_binary64_709 count-2_binary64_708
Counts
223 → 495
Iterations

Useful iterations: 2 (0.0ms)

IterNodesCost
03097176
17815251
230435229
349695229

prune811.0ms (0.8%)

Pruning

20 alts after pruning (18 fresh and 2 done)

PrunedKeptTotal
New4896495
Fresh61218
Picked011
Done011
Total49520515
Error
4.8b
Counts
515 → 20
Compiler

Compiled 13534 to 6155 computations (54.5% saved)

regimes8.4s (8%)

Accuracy

Total 7.3b remaining (58.3%)

Threshold costs 0b (0%)

Compiler

Compiled 69958 to 48149 computations (31.2% saved)

bsearch288.0ms (0.3%)

Steps
ItersRangePoint
10
8.856294352433011e+70
1.5533381578236447e+86
1.0275830431192084e+73
6
6.494322418222212e+66
6.577715337346823e+67
6.439006299831887e+67
6
3.408944378237824e-83
2.2612485244434277e-82
8.924049272980926e-83
5
-5.673888236475523e-09
-1.6625812997540152e-09
-3.5362665831654716e-09
Compiler

Compiled 1 to 3 computations (-200% saved)

simplify13.0ms (0%)

Algorithm
egg-herbie
Rules
19×*-commutative_binary64_691
+-commutative_binary64_690
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_1020 if-if-and_binary64_1019 if-if-or-not_binary64_1018 if-if-or_binary64_1017 if-not_binary64_1016 if-same_binary64_1015 if-false_binary64_1014 if-true_binary64_1013 tan-0_binary64_889 cos-0_binary64_888 sin-0_binary64_887 unpow1_binary64_818 e-exp-1_binary64_805 1-exp_binary64_804 exp-1-e_binary64_803 exp-0_binary64_802 sqr-abs_binary64_775 sqr-neg_binary64_774 neg-mul-1_binary64_756 neg-sub0_binary64_755 unsub-neg_binary64_754 sub-neg_binary64_753 mul-1-neg_binary64_752 /-rgt-identity_binary64_751 *-rgt-identity_binary64_750 *-lft-identity_binary64_749 remove-double-neg_binary64_748 sub0-neg_binary64_747 --rgt-identity_binary64_746 +-rgt-identity_binary64_745 +-lft-identity_binary64_744 cancel-sign-sub-inv_binary64_726 cancel-sign-sub_binary64_725 distribute-neg-frac_binary64_724 distribute-frac-neg_binary64_723 distribute-neg-out_binary64_722 distribute-neg-in_binary64_721 distribute-rgt-neg-out_binary64_720 distribute-lft-neg-out_binary64_719 distribute-rgt-neg-in_binary64_718 distribute-lft-neg-in_binary64_717
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
071274
191274
Proof
(if real (<= f64 h0 -2137541988714571/604462909807314587353088) (* f64 h1 (=> (* f64 (/ f64 (/ f64 2 (+ f64 2 (pow f64 (/ f64 h2 h0) 2))) (* f64 h0 (* f64 (sin f64 h2) (* f64 (tan f64 h2) (* f64 h0 h0))))) h1))) (if real (<= f64 h0 3049864568801069/34175792574734561318320347298712833833643272357706444319152665725155515612490248800367393390985216) (* f64 (/ f64 (* f64 h1 2) (* f64 (cbrt f64 h2) (cbrt f64 h2))) (/ f64 (/ f64 (* f64 (/ f64 (cos f64 h2) h2) (/ f64 h1 (pow f64 (sin f64 h2) 2))) h0) (cbrt f64 h2))) (if real (<= f64 h0 64390062998318865313378124977189265318776997723003709669165253001216) (* f64 h1 (* f64 (/ f64 (* f64 (cbrt f64 (/ f64 2 (+ f64 2 (pow f64 (/ f64 h2 h0) 2)))) (cbrt f64 (/ f64 2 (+ f64 2 (pow f64 (/ f64 h2 h0) 2))))) (pow f64 h0 3)) (* f64 (/ f64 (cbrt f64 (/ f64 2 (+ f64 2 (pow f64 (/ f64 h2 h0) 2)))) (sin f64 h2)) (/ f64 h1 (tan f64 h2))))) (if real (<= f64 h0 10275830431192083531347455722316101648639645393848034099015047297579876352) (* f64 h1 (* f64 2 (/ f64 (/ f64 (/ f64 (cos f64 h2) (* f64 (* f64 (cbrt f64 (/ f64 h2 (/ f64 h1 h2))) (cbrt f64 (/ f64 h2 (/ f64 h1 h2)))) (cbrt f64 (/ f64 h2 (/ f64 h1 h2))))) (pow f64 (sin f64 h2) 2)) h0))) (* f64 h1 (* f64 (/ f64 (/ f64 2 (+ f64 2 (pow f64 (/ f64 h2 h0) 2))) (* f64 (pow f64 h0 (/ f64 3 2)) (* f64 (tan f64 h2) (* f64 (sin f64 h2) (pow f64 h0 (/ f64 3 2)))))) h1)))))) *-commutative_binary64_691 => (if real (<= f64 h0 -2137541988714571/604462909807314587353088) (* f64 h1 (* f64 h1 (/ f64 (/ f64 2 (+ f64 2 (pow f64 (/ f64 h2 h0) 2))) (* f64 h0 (* f64 (sin f64 h2) (* f64 (tan f64 h2) (* f64 h0 h0))))))) (if real (<= f64 h0 3049864568801069/34175792574734561318320347298712833833643272357706444319152665725155515612490248800367393390985216) (* f64 (/ f64 (* f64 h1 2) (* f64 (cbrt f64 h2) (cbrt f64 h2))) (/ f64 (/ f64 (* f64 (/ f64 (cos f64 h2) h2) (/ f64 h1 (pow f64 (sin f64 h2) 2))) h0) (cbrt f64 h2))) (if real (<= f64 h0 64390062998318865313378124977189265318776997723003709669165253001216) (* f64 h1 (* f64 (/ f64 (* f64 (cbrt f64 (/ f64 2 (+ f64 2 (pow f64 (/ f64 h2 h0) 2)))) (cbrt f64 (/ f64 2 (+ f64 2 (pow f64 (/ f64 h2 h0) 2))))) (pow f64 h0 3)) (* f64 (/ f64 (cbrt f64 (/ f64 2 (+ f64 2 (pow f64 (/ f64 h2 h0) 2)))) (sin f64 h2)) (/ f64 h1 (tan f64 h2))))) (if real (<= f64 h0 10275830431192083531347455722316101648639645393848034099015047297579876352) (* f64 h1 (* f64 2 (/ f64 (/ f64 (/ f64 (cos f64 h2) (* f64 (* f64 (cbrt f64 (/ f64 h2 (/ f64 h1 h2))) (cbrt f64 (/ f64 h2 (/ f64 h1 h2)))) (cbrt f64 (/ f64 h2 (/ f64 h1 h2))))) (pow f64 (sin f64 h2) 2)) h0))) (* f64 h1 (=> (* f64 (/ f64 (/ f64 2 (+ f64 2 (pow f64 (/ f64 h2 h0) 2))) (* f64 (pow f64 h0 (/ f64 3 2)) (* f64 (tan f64 h2) (* f64 (sin f64 h2) (pow f64 h0 (/ f64 3 2)))))) h1))))))) *-commutative_binary64_691 => (if real (<= f64 h0 -2137541988714571/604462909807314587353088) (* f64 h1 (* f64 h1 (/ f64 (/ f64 2 (+ f64 2 (pow f64 (/ f64 h2 h0) 2))) (* f64 h0 (* f64 (sin f64 h2) (* f64 (tan f64 h2) (* f64 h0 h0))))))) (if real (<= f64 h0 3049864568801069/34175792574734561318320347298712833833643272357706444319152665725155515612490248800367393390985216) (* f64 (/ f64 (* f64 h1 2) (* f64 (cbrt f64 h2) (cbrt f64 h2))) (/ f64 (/ f64 (* f64 (/ f64 (cos f64 h2) h2) (/ f64 h1 (pow f64 (sin f64 h2) 2))) h0) (cbrt f64 h2))) (if real (<= f64 h0 64390062998318865313378124977189265318776997723003709669165253001216) (* f64 h1 (* f64 (/ f64 (* f64 (cbrt f64 (/ f64 2 (+ f64 2 (pow f64 (/ f64 h2 h0) 2)))) (cbrt f64 (/ f64 2 (+ f64 2 (pow f64 (/ f64 h2 h0) 2))))) (pow f64 h0 3)) (* f64 (/ f64 (cbrt f64 (/ f64 2 (+ f64 2 (pow f64 (/ f64 h2 h0) 2)))) (sin f64 h2)) (/ f64 h1 (tan f64 h2))))) (if real (<= f64 h0 10275830431192083531347455722316101648639645393848034099015047297579876352) (* f64 h1 (* f64 2 (/ f64 (/ f64 (/ f64 (cos f64 h2) (=> (* f64 (* f64 (cbrt f64 (/ f64 h2 (/ f64 h1 h2))) (cbrt f64 (/ f64 h2 (/ f64 h1 h2)))) (cbrt f64 (/ f64 h2 (/ f64 h1 h2)))))) (pow f64 (sin f64 h2) 2)) h0))) (* f64 h1 (* f64 h1 (/ f64 (/ f64 2 (+ f64 2 (pow f64 (/ f64 h2 h0) 2))) (* f64 (pow f64 h0 (/ f64 3 2)) (* f64 (tan f64 h2) (* f64 (sin f64 h2) (pow f64 h0 (/ f64 3 2)))))))))))) *-commutative_binary64_691 => (if real (<= f64 h0 -2137541988714571/604462909807314587353088) (* f64 h1 (* f64 h1 (/ f64 (/ f64 2 (+ f64 2 (pow f64 (/ f64 h2 h0) 2))) (* f64 h0 (* f64 (sin f64 h2) (* f64 (tan f64 h2) (* f64 h0 h0))))))) (if real (<= f64 h0 3049864568801069/34175792574734561318320347298712833833643272357706444319152665725155515612490248800367393390985216) (* f64 (/ f64 (* f64 h1 2) (* f64 (cbrt f64 h2) (cbrt f64 h2))) (/ f64 (/ f64 (* f64 (/ f64 (cos f64 h2) h2) (/ f64 h1 (pow f64 (sin f64 h2) 2))) h0) (cbrt f64 h2))) (if real (<= f64 h0 64390062998318865313378124977189265318776997723003709669165253001216) (* f64 h1 (* f64 (/ f64 (* f64 (cbrt f64 (/ f64 2 (+ f64 2 (pow f64 (/ f64 h2 h0) 2)))) (cbrt f64 (/ f64 2 (+ f64 2 (pow f64 (/ f64 h2 h0) 2))))) (pow f64 h0 3)) (* f64 (/ f64 (cbrt f64 (/ f64 2 (+ f64 2 (pow f64 (/ f64 h2 h0) 2)))) (sin f64 h2)) (/ f64 h1 (tan f64 h2))))) (if real (<= f64 h0 10275830431192083531347455722316101648639645393848034099015047297579876352) (* f64 h1 (* f64 2 (/ f64 (/ f64 (/ f64 (cos f64 h2) (* f64 (cbrt f64 (/ f64 h2 (/ f64 h1 h2))) (* f64 (cbrt f64 (/ f64 h2 (/ f64 h1 h2))) (cbrt f64 (/ f64 h2 (/ f64 h1 h2)))))) (pow f64 (sin f64 h2) 2)) h0))) (* f64 h1 (* f64 h1 (/ f64 (/ f64 2 (+ f64 2 (pow f64 (/ f64 h2 h0) 2))) (* f64 (pow f64 h0 (/ f64 3 2)) (* f64 (tan f64 h2) (* f64 (sin f64 h2) (pow f64 h0 (/ f64 3 2))))))))))))

end0.0ms (0%)

sample12.3s (11.7%)

Algorithm
intervals
Results
1.4s2671×body1024valid
493.0ms1229×body512valid
449.0ms3489×body128valid
203.0ms1523×body128invalid
155.0ms604×body256valid
54.0ms133×body512invalid
35.0ms120×body256invalid
33.0ms56×body1024invalid
5.0msbody2048valid
Compiler

Compiled 11805 to 8106 computations (31.3% saved)

Profiling

Loading profile data...