Details

Time bar (total: 14.3s)

analyze238.0ms (1.7%)

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
12.5%87.4%0.1%4
12.5%87.4%0.1%5
15.6%84.3%0.1%6
32.8%67.1%0.1%7
38.2%61.6%0.1%8
46%53.8%0.1%9
62.6%37.3%0.1%10
67.2%32.7%0.1%11
71.1%28.8%0.1%12
81.6%18.2%0.1%13
84.1%15.7%0.1%14
Compiler

Compiled 10 to 9 computations (10% saved)

sample21.0ms (0.1%)

Algorithm
intervals
Results
11.0ms256×body128valid
Compiler

Compiled 19 to 20 computations (-5.3% saved)

simplify660.0ms (4.6%)

Algorithm
egg-herbie
Rules
749×exp-prod_binary64_26046
552×associate-/l*_binary64_25939
279×swap-sqr_binary64_25961
257×associate-*r/_binary64_25936
244×*-commutative_binary64_25925
231×cancel-sign-sub-inv_binary64_25960
228×times-frac_binary64_26000
215×distribute-neg-frac_binary64_25958
185×associate-/l/_binary64_25941
180×associate-+r+_binary64_25926
168×unsub-neg_binary64_25988
167×associate-/r*_binary64_25938
140×associate-+r-_binary64_25928
125×distribute-rgt1-in_binary64_25950
116×associate--l+_binary64_25931 associate-+l+_binary64_25927
107×associate--r+_binary64_25930 associate-+l-_binary64_25929
93×distribute-rgt-neg-out_binary64_25954
92×pow-plus_binary64_26057
88×distribute-lft-neg-out_binary64_25953 distribute-lft-neg-in_binary64_25951
84×exp-sum_binary64_26040
81×associate--r-_binary64_25933
80×associate--l-_binary64_25932
77×distribute-rgt-neg-in_binary64_25952
73×associate-/r/_binary64_25940
56×distribute-rgt-in_binary64_25944
55×sub-neg_binary64_25987
54×exp-diff_binary64_26042
49×neg-mul-1_binary64_25990 distribute-frac-neg_binary64_25957
48×distribute-neg-in_binary64_25955
44×neg-sub0_binary64_25989
33×div-sub_binary64_25999
31×sqr-pow_binary64_25966
28×distribute-lft-in_binary64_25943
24×associate-*r*_binary64_25934
23×pow-sqr_binary64_25967 +-commutative_binary64_25924
20×pow-base-1_binary64_26054
19×unswap-sqr_binary64_25962 distribute-rgt-out_binary64_25947
13×distribute-neg-out_binary64_25956
12×sqr-neg_binary64_26008 /-rgt-identity_binary64_25985 remove-double-neg_binary64_25982
11×difference-of-squares_binary64_25963 associate-*l*_binary64_25935
10×distribute-rgt-out--_binary64_25948
exp-lft-sqr_binary64_26049
exp-neg_binary64_26041 cube-unmult_binary64_26031 *-rgt-identity_binary64_25984 sub0-neg_binary64_25981
*-lft-identity_binary64_25983 distribute-lft1-in_binary64_25949
mul0-lft_binary64_25976 count-2_binary64_25942
mul0-rgt_binary64_25977
cube-prod_binary64_26022 --rgt-identity_binary64_25980 +-rgt-identity_binary64_25979 +-lft-identity_binary64_25978
unpow3_binary64_26060 div0_binary64_25975 +-inverses_binary64_25973 distribute-lft-out--_binary64_25946 distribute-lft-out_binary64_25945 associate-*l/_binary64_25937
exp-sqrt_binary64_26047 cube-div_binary64_26023 difference-of-sqr--1_binary64_25965 cancel-sign-sub_binary64_25959
1-exp_binary64_26038 exp-1-e_binary64_26037 cube-neg_binary64_26021 *-inverses_binary64_25974
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_26257 erf-erfc_binary64_26256 erf-odd_binary64_26255 if-if-and-not_binary64_26254 if-if-and_binary64_26253 if-if-or-not_binary64_26252 if-if-or_binary64_26251 if-not_binary64_26250 if-same_binary64_26249 if-false_binary64_26248 if-true_binary64_26247 not-gte_binary64_26246 not-lte_binary64_26245 not-gt_binary64_26244 not-lt_binary64_26243 gte-same_binary64_26242 lte-same_binary64_26241 gt-same_binary64_26240 lt-same_binary64_26239 sinh---cosh_binary64_26186 sinh-+-cosh_binary64_26185 sinh-cosh_binary64_26184 tanh-def-c_binary64_26183 tanh-def-b_binary64_26182 tanh-def-a_binary64_26181 cosh-def_binary64_26180 sinh-def_binary64_26179 tan-neg_binary64_26126 cos-neg_binary64_26125 sin-neg_binary64_26124 tan-0_binary64_26123 cos-0_binary64_26122 sin-0_binary64_26121 hang-m-tan_binary64_26120 hang-p-tan_binary64_26119 hang-m0-tan_binary64_26118 hang-p0-tan_binary64_26117 hang-0m-tan_binary64_26116 hang-0p-tan_binary64_26115 tan-+PI/2_binary64_26114 tan-+PI_binary64_26113 tan-PI_binary64_26112 tan-PI/3_binary64_26111 tan-PI/4_binary64_26110 tan-PI/6_binary64_26109 cos-+PI/2_binary64_26108 cos-+PI_binary64_26107 cos-PI_binary64_26106 cos-PI/2_binary64_26105 cos-PI/3_binary64_26104 cos-PI/4_binary64_26103 cos-PI/6_binary64_26102 sin-+PI/2_binary64_26101 sin-+PI_binary64_26100 sin-PI_binary64_26099 sin-PI/2_binary64_26098 sin-PI/3_binary64_26097 sin-PI/4_binary64_26096 sin-PI/6_binary64_26095 sub-1-sin_binary64_26094 sub-1-cos_binary64_26093 -1-add-sin_binary64_26092 -1-add-cos_binary64_26091 1-sub-sin_binary64_26090 1-sub-cos_binary64_26089 cos-sin-sum_binary64_26088 log-E_binary64_26084 log-pow_binary64_26083 log-rec_binary64_26082 log-div_binary64_26081 log-prod_binary64_26080 pow-base-0_binary64_26078 unpow1/3_binary64_26061 unpow2_binary64_26059 unpow1/2_binary64_26058 exp-to-pow_binary64_26056 unpow0_binary64_26053 unpow1_binary64_26052 unpow-1_binary64_26051 exp-lft-cube_binary64_26050 exp-cbrt_binary64_26048 div-exp_binary64_26045 rec-exp_binary64_26044 prod-exp_binary64_26043 e-exp-1_binary64_26039 exp-0_binary64_26036 rem-log-exp_binary64_26035 rem-exp-log_binary64_26034 cube-mult_binary64_26024 rem-3cbrt-rft_binary64_26020 rem-3cbrt-lft_binary64_26019 rem-cbrt-cube_binary64_26018 rem-cube-cbrt_binary64_26017 sqr-abs_binary64_26009 rem-sqrt-square_binary64_26007 rem-square-sqrt_binary64_26006 mul-1-neg_binary64_25986 lft-mult-inverse_binary64_25972 rgt-mult-inverse_binary64_25971 remove-double-div_binary64_25970 difference-of-sqr-1_binary64_25964
Counts
1 → 0
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
0913
11413
22013
32813
44213
56113
611413
734613
8204213
9437013

prune2.0ms (0%)

Pruning

1 alts after pruning (1 fresh and 0 done)

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

Compiled 9 to 8 computations (11.1% saved)

localize6.0ms (0%)

Local error

Found 1 expressions with local error:

7.2b
(/.f64 (+.f64 x y) (-.f64 1 (/.f64 y z)))

rewrite95.0ms (0.7%)

Algorithm
rewrite-expression-head
Error
5.7b
Rules
55×add-sqr-sqrt_binary64_26016
53×*-un-lft-identity_binary64_25994
42×times-frac_binary64_26000
20×difference-of-squares_binary64_25963
15×add-cube-cbrt_binary64_26029
distribute-lft-out_binary64_25945
associate-/r*_binary64_25938
distribute-lft-out--_binary64_25946
associate-/l*_binary64_25939
add-exp-log_binary64_26032 add-cbrt-cube_binary64_26030
associate-/l/_binary64_25941 associate-/r/_binary64_25940
pow1_binary64_26055 div-exp_binary64_26045 add-log-exp_binary64_26033 cbrt-undiv_binary64_26028 frac-2neg_binary64_26005 clear-num_binary64_25993 div-inv_binary64_25991 flip3-+_binary64_25997 flip-+_binary64_25968 flip3--_binary64_25998 flip--_binary64_25969
Counts
1 → 60
Calls

1 calls:

12.0ms
(/.f64 (+.f64 x y) (-.f64 1 (/.f64 y z)))
Compiler

Compiled 1216 to 500 computations (58.9% saved)

series305.0ms (2.1%)

Error
0.0b
Counts
1 → 21
Calls

1 calls:

280.0ms
(/.f64 (+.f64 x y) (-.f64 1 (/.f64 y z)))
Compiler

Compiled 832 to 572 computations (31.3% saved)

simplify273.0ms (1.9%)

Algorithm
egg-herbie
Rules
574×distribute-rgt-in_binary64_25944
405×cancel-sign-sub-inv_binary64_25960
185×sub-neg_binary64_25987
179×div-sub_binary64_25999
173×distribute-rgt-out_binary64_25947
169×times-frac_binary64_26000
159×associate-+l+_binary64_25927
150×associate-/l*_binary64_25939
141×distribute-neg-frac_binary64_25958
136×distribute-lft-in_binary64_25943
127×associate-/r*_binary64_25938
123×distribute-neg-in_binary64_25955 associate-+r+_binary64_25926
121×distribute-rgt-neg-in_binary64_25952
114×distribute-lft-neg-out_binary64_25953 associate-*r/_binary64_25936
112×associate-*l/_binary64_25937
110×unsub-neg_binary64_25988 distribute-rgt-neg-out_binary64_25954 distribute-lft-neg-in_binary64_25951
104×*-commutative_binary64_25925
95×associate-/l/_binary64_25941
87×neg-sub0_binary64_25989
83×distribute-rgt-out--_binary64_25948
82×associate-/r/_binary64_25940
79×associate-*l*_binary64_25935 +-commutative_binary64_25924
76×neg-mul-1_binary64_25990
68×associate-*r*_binary64_25934
66×distribute-lft-out_binary64_25945
65×associate--r+_binary64_25930
59×unswap-sqr_binary64_25962
57×distribute-neg-out_binary64_25956
54×sqr-pow_binary64_25966
39×pow-sqr_binary64_25967
36×*-rgt-identity_binary64_25984
31×associate-+l-_binary64_25929
28×*-lft-identity_binary64_25983 associate-+r-_binary64_25928
25×pow-plus_binary64_26057
24×distribute-rgt1-in_binary64_25950
22×sub0-neg_binary64_25981
21×distribute-frac-neg_binary64_25957
18×cube-div_binary64_26023 cube-prod_binary64_26022 /-rgt-identity_binary64_25985
16×div-exp_binary64_26045 prod-exp_binary64_26043 associate--l+_binary64_25931
15×log-prod_binary64_26080 +-rgt-identity_binary64_25979
14×log-pow_binary64_26083
12×log-div_binary64_26081
11×swap-sqr_binary64_25961
10×cancel-sign-sub_binary64_25959
distribute-lft-out--_binary64_25946
exp-prod_binary64_26046 cube-unmult_binary64_26031
difference-of-squares_binary64_25963
pow-base-1_binary64_26054
unpow3_binary64_26060 cube-mult_binary64_26024 associate--l-_binary64_25932
rec-exp_binary64_26044 rem-sqrt-square_binary64_26007 difference-of-sqr-1_binary64_25964 distribute-lft1-in_binary64_25949
mul-1-neg_binary64_25986 div0_binary64_25975
unpow2_binary64_26059 unpow1_binary64_26052 sqr-neg_binary64_26008 remove-double-neg_binary64_25982 --rgt-identity_binary64_25980 associate--r-_binary64_25933
log-rec_binary64_26082 exp-diff_binary64_26042 1-exp_binary64_26038 rem-log-exp_binary64_26035 cube-neg_binary64_26021 *-inverses_binary64_25974 rgt-mult-inverse_binary64_25971 difference-of-sqr--1_binary64_25965 count-2_binary64_25942
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_26257 erf-erfc_binary64_26256 erf-odd_binary64_26255 if-if-and-not_binary64_26254 if-if-and_binary64_26253 if-if-or-not_binary64_26252 if-if-or_binary64_26251 if-not_binary64_26250 if-same_binary64_26249 if-false_binary64_26248 if-true_binary64_26247 not-gte_binary64_26246 not-lte_binary64_26245 not-gt_binary64_26244 not-lt_binary64_26243 gte-same_binary64_26242 lte-same_binary64_26241 gt-same_binary64_26240 lt-same_binary64_26239 sinh---cosh_binary64_26186 sinh-+-cosh_binary64_26185 sinh-cosh_binary64_26184 tanh-def-c_binary64_26183 tanh-def-b_binary64_26182 tanh-def-a_binary64_26181 cosh-def_binary64_26180 sinh-def_binary64_26179 tan-neg_binary64_26126 cos-neg_binary64_26125 sin-neg_binary64_26124 tan-0_binary64_26123 cos-0_binary64_26122 sin-0_binary64_26121 hang-m-tan_binary64_26120 hang-p-tan_binary64_26119 hang-m0-tan_binary64_26118 hang-p0-tan_binary64_26117 hang-0m-tan_binary64_26116 hang-0p-tan_binary64_26115 tan-+PI/2_binary64_26114 tan-+PI_binary64_26113 tan-PI_binary64_26112 tan-PI/3_binary64_26111 tan-PI/4_binary64_26110 tan-PI/6_binary64_26109 cos-+PI/2_binary64_26108 cos-+PI_binary64_26107 cos-PI_binary64_26106 cos-PI/2_binary64_26105 cos-PI/3_binary64_26104 cos-PI/4_binary64_26103 cos-PI/6_binary64_26102 sin-+PI/2_binary64_26101 sin-+PI_binary64_26100 sin-PI_binary64_26099 sin-PI/2_binary64_26098 sin-PI/3_binary64_26097 sin-PI/4_binary64_26096 sin-PI/6_binary64_26095 sub-1-sin_binary64_26094 sub-1-cos_binary64_26093 -1-add-sin_binary64_26092 -1-add-cos_binary64_26091 1-sub-sin_binary64_26090 1-sub-cos_binary64_26089 cos-sin-sum_binary64_26088 log-E_binary64_26084 pow-base-0_binary64_26078 unpow1/3_binary64_26061 unpow1/2_binary64_26058 exp-to-pow_binary64_26056 unpow0_binary64_26053 unpow-1_binary64_26051 exp-lft-cube_binary64_26050 exp-lft-sqr_binary64_26049 exp-cbrt_binary64_26048 exp-sqrt_binary64_26047 exp-neg_binary64_26041 exp-sum_binary64_26040 e-exp-1_binary64_26039 exp-1-e_binary64_26037 exp-0_binary64_26036 rem-exp-log_binary64_26034 rem-3cbrt-rft_binary64_26020 rem-3cbrt-lft_binary64_26019 rem-cbrt-cube_binary64_26018 rem-cube-cbrt_binary64_26017 sqr-abs_binary64_26009 rem-square-sqrt_binary64_26006 +-lft-identity_binary64_25978 mul0-rgt_binary64_25977 mul0-lft_binary64_25976 +-inverses_binary64_25973 lft-mult-inverse_binary64_25972 remove-double-div_binary64_25970
Counts
81 → 184
Iterations

Useful iterations: 3 (0.0ms)

IterNodesCost
01521924
13481870
210461838
328691778

prune188.0ms (1.3%)

Pruning

5 alts after pruning (4 fresh and 1 done)

PrunedKeptTotal
New1804184
Fresh000
Picked011
Done000
Total1805185
Error
0.0b
Counts
185 → 5
Compiler

Compiled 3923 to 1345 computations (65.7% saved)

localize7.0ms (0.1%)

Local error

Found 2 expressions with local error:

0.2b
(/.f64 1 (/.f64 (-.f64 1 (/.f64 y z)) (+.f64 y x)))
7.2b
(/.f64 (-.f64 1 (/.f64 y z)) (+.f64 y x))

rewrite584.0ms (4.1%)

Algorithm
rewrite-expression-head
Error
0.0b
Rules
316×times-frac_binary64_26000
275×add-sqr-sqrt_binary64_26016
273×*-un-lft-identity_binary64_25994
107×add-cube-cbrt_binary64_26029
84×difference-of-squares_binary64_25963
42×associate-/r*_binary64_25938
41×distribute-lft-out_binary64_25945
21×distribute-lft-out--_binary64_25946
15×add-exp-log_binary64_26032
11×associate-/r/_binary64_25940 associate-/l*_binary64_25939
add-cbrt-cube_binary64_26030
div-exp_binary64_26045
div-inv_binary64_25991
flip3-+_binary64_25997 flip-+_binary64_25968
cbrt-undiv_binary64_26028
pow1_binary64_26055
add-log-exp_binary64_26033 frac-2neg_binary64_26005 clear-num_binary64_25993 associate-/l/_binary64_25941 1-exp_binary64_26038 rec-exp_binary64_26044
div-sub_binary64_25999 flip3--_binary64_25998 flip--_binary64_25969 inv-pow_binary64_26079 pow-flip_binary64_26068
Counts
2 → 237
Calls

2 calls:

17.0ms
(/.f64 1 (/.f64 (-.f64 1 (/.f64 y z)) (+.f64 y x)))
13.0ms
(/.f64 (-.f64 1 (/.f64 y z)) (+.f64 y x))
Compiler

Compiled 5936 to 2948 computations (50.3% saved)

series595.0ms (4.2%)

Error
0b
Counts
2 → 47
Calls

2 calls:

285.0ms
(/.f64 1 (/.f64 (-.f64 1 (/.f64 y z)) (+.f64 y x)))
259.0ms
(/.f64 (-.f64 1 (/.f64 y z)) (+.f64 y x))
Compiler

Compiled 2214 to 1556 computations (29.7% saved)

simplify1.1s (7.8%)

Algorithm
egg-herbie
Rules
431×distribute-rgt-in_binary64_25944
360×distribute-lft-in_binary64_25943
275×associate--r+_binary64_25930
267×associate-/l/_binary64_25941
262×associate-/r/_binary64_25940
258×associate--l+_binary64_25931
246×associate-/l*_binary64_25939
178×sub-neg_binary64_25987
166×*-commutative_binary64_25925
158×associate-*l/_binary64_25937
138×cancel-sign-sub-inv_binary64_25960
118×times-frac_binary64_26000
117×associate-*r/_binary64_25936
114×div-sub_binary64_25999
94×associate-/r*_binary64_25938
93×distribute-neg-in_binary64_25955
92×+-commutative_binary64_25924
87×distribute-neg-frac_binary64_25958
86×associate-*r*_binary64_25934
74×*-rgt-identity_binary64_25984
67×neg-sub0_binary64_25989 associate-+l+_binary64_25927
66×neg-mul-1_binary64_25990
63×distribute-rgt-neg-in_binary64_25952 associate-+r+_binary64_25926
58×associate--l-_binary64_25932
52×distribute-lft-neg-in_binary64_25951
49×/-rgt-identity_binary64_25985
43×distribute-lft-neg-out_binary64_25953
42×unsub-neg_binary64_25988
40×associate-*l*_binary64_25935
38×sqr-pow_binary64_25966
33×distribute-rgt-neg-out_binary64_25954
17×pow-sqr_binary64_25967 distribute-rgt-out--_binary64_25948 distribute-rgt-out_binary64_25947
15×exp-prod_binary64_26046 *-lft-identity_binary64_25983
12×log-div_binary64_26081
10×log-prod_binary64_26080 pow-plus_binary64_26057 cube-prod_binary64_26022 distribute-neg-out_binary64_25956
swap-sqr_binary64_25961 distribute-rgt1-in_binary64_25950
cube-div_binary64_26023
log-rec_binary64_26082 associate--r-_binary64_25933
exp-sum_binary64_26040 cube-unmult_binary64_26031 difference-of-squares_binary64_25963 unswap-sqr_binary64_25962
remove-double-div_binary64_25970
mul-1-neg_binary64_25986
unpow3_binary64_26060 unpow2_binary64_26059 unpow1_binary64_26052 exp-diff_binary64_26042 cube-mult_binary64_26024 distribute-lft-out--_binary64_25946 distribute-lft-out_binary64_25945
remove-double-neg_binary64_25982 cancel-sign-sub_binary64_25959 associate-+r-_binary64_25928
log-pow_binary64_26083 div-exp_binary64_26045 rec-exp_binary64_26044 prod-exp_binary64_26043 1-exp_binary64_26038 rem-log-exp_binary64_26035 rem-cbrt-cube_binary64_26018 rem-sqrt-square_binary64_26007 sub0-neg_binary64_25981 +-rgt-identity_binary64_25979 div0_binary64_25975 *-inverses_binary64_25974 distribute-frac-neg_binary64_25957 distribute-lft1-in_binary64_25949 count-2_binary64_25942 associate-+l-_binary64_25929
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_26257 erf-erfc_binary64_26256 erf-odd_binary64_26255 if-if-and-not_binary64_26254 if-if-and_binary64_26253 if-if-or-not_binary64_26252 if-if-or_binary64_26251 if-not_binary64_26250 if-same_binary64_26249 if-false_binary64_26248 if-true_binary64_26247 not-gte_binary64_26246 not-lte_binary64_26245 not-gt_binary64_26244 not-lt_binary64_26243 gte-same_binary64_26242 lte-same_binary64_26241 gt-same_binary64_26240 lt-same_binary64_26239 sinh---cosh_binary64_26186 sinh-+-cosh_binary64_26185 sinh-cosh_binary64_26184 tanh-def-c_binary64_26183 tanh-def-b_binary64_26182 tanh-def-a_binary64_26181 cosh-def_binary64_26180 sinh-def_binary64_26179 tan-neg_binary64_26126 cos-neg_binary64_26125 sin-neg_binary64_26124 tan-0_binary64_26123 cos-0_binary64_26122 sin-0_binary64_26121 hang-m-tan_binary64_26120 hang-p-tan_binary64_26119 hang-m0-tan_binary64_26118 hang-p0-tan_binary64_26117 hang-0m-tan_binary64_26116 hang-0p-tan_binary64_26115 tan-+PI/2_binary64_26114 tan-+PI_binary64_26113 tan-PI_binary64_26112 tan-PI/3_binary64_26111 tan-PI/4_binary64_26110 tan-PI/6_binary64_26109 cos-+PI/2_binary64_26108 cos-+PI_binary64_26107 cos-PI_binary64_26106 cos-PI/2_binary64_26105 cos-PI/3_binary64_26104 cos-PI/4_binary64_26103 cos-PI/6_binary64_26102 sin-+PI/2_binary64_26101 sin-+PI_binary64_26100 sin-PI_binary64_26099 sin-PI/2_binary64_26098 sin-PI/3_binary64_26097 sin-PI/4_binary64_26096 sin-PI/6_binary64_26095 sub-1-sin_binary64_26094 sub-1-cos_binary64_26093 -1-add-sin_binary64_26092 -1-add-cos_binary64_26091 1-sub-sin_binary64_26090 1-sub-cos_binary64_26089 cos-sin-sum_binary64_26088 log-E_binary64_26084 pow-base-0_binary64_26078 unpow1/3_binary64_26061 unpow1/2_binary64_26058 exp-to-pow_binary64_26056 pow-base-1_binary64_26054 unpow0_binary64_26053 unpow-1_binary64_26051 exp-lft-cube_binary64_26050 exp-lft-sqr_binary64_26049 exp-cbrt_binary64_26048 exp-sqrt_binary64_26047 exp-neg_binary64_26041 e-exp-1_binary64_26039 exp-1-e_binary64_26037 exp-0_binary64_26036 rem-exp-log_binary64_26034 cube-neg_binary64_26021 rem-3cbrt-rft_binary64_26020 rem-3cbrt-lft_binary64_26019 rem-cube-cbrt_binary64_26017 sqr-abs_binary64_26009 sqr-neg_binary64_26008 rem-square-sqrt_binary64_26006 --rgt-identity_binary64_25980 +-lft-identity_binary64_25978 mul0-rgt_binary64_25977 mul0-lft_binary64_25976 +-inverses_binary64_25973 lft-mult-inverse_binary64_25972 rgt-mult-inverse_binary64_25971 difference-of-sqr--1_binary64_25965 difference-of-sqr-1_binary64_25964
Counts
284 → 1372
Iterations

Useful iterations: 2 (0.0ms)

IterNodesCost
03938846
19568617
235657466

prune3.0s (21.1%)

Pruning

5 alts after pruning (4 fresh and 1 done)

PrunedKeptTotal
New137111372
Fresh033
Picked101
Done011
Total137251377
Error
0b
Counts
1377 → 5
Compiler

Compiled 37754 to 17659 computations (53.2% saved)

localize10.0ms (0.1%)

Local error

Found 4 expressions with local error:

0.1b
(/.f64 (+.f64 y x) (sqrt.f64 (-.f64 1 (/.f64 y z))))
0.1b
(*.f64 (/.f64 1 (sqrt.f64 (-.f64 1 (/.f64 y z)))) (/.f64 (+.f64 y x) (sqrt.f64 (-.f64 1 (/.f64 y z)))))
4.3b
(sqrt.f64 (-.f64 1 (/.f64 y z)))
4.3b
(sqrt.f64 (-.f64 1 (/.f64 y z)))

rewrite558.0ms (3.9%)

Algorithm
rewrite-expression-head
Error
0b
Rules
226×add-sqr-sqrt_binary64_26016
174×*-un-lft-identity_binary64_25994
171×times-frac_binary64_26000
123×sqrt-prod_binary64_26010
66×add-cube-cbrt_binary64_26029
56×difference-of-squares_binary64_25963
50×associate-*r*_binary64_25934
39×associate-*l*_binary64_25935
28×add-exp-log_binary64_26032
23×distribute-lft-out_binary64_25945
18×add-cbrt-cube_binary64_26030
15×unswap-sqr_binary64_25962
14×distribute-lft-out--_binary64_25946
11×associate-/r*_binary64_25938
10×sqrt-div_binary64_26011
div-exp_binary64_26045
pow1_binary64_26055 prod-exp_binary64_26043
associate-/r/_binary64_25940
flip3--_binary64_25998 flip--_binary64_25969 cbrt-undiv_binary64_26028
add-log-exp_binary64_26033 cbrt-unprod_binary64_26027 associate-/l*_binary64_25939
div-inv_binary64_25991
pow1/2_binary64_26074 sqrt-pow1_binary64_26012 rem-sqrt-square_binary64_26007 1-exp_binary64_26038 rec-exp_binary64_26044 associate-/l/_binary64_25941
pow-prod-down_binary64_26065 frac-times_binary64_26004 associate-*l/_binary64_25937 associate-*r/_binary64_25936 *-commutative_binary64_25925 frac-2neg_binary64_26005 clear-num_binary64_25993 flip3-+_binary64_25997 flip-+_binary64_25968
Counts
4 → 243
Calls

4 calls:

62.0ms
(*.f64 (/.f64 1 (sqrt.f64 (-.f64 1 (/.f64 y z)))) (/.f64 (+.f64 y x) (sqrt.f64 (-.f64 1 (/.f64 y z)))))
14.0ms
(/.f64 (+.f64 y x) (sqrt.f64 (-.f64 1 (/.f64 y z))))
7.0ms
(sqrt.f64 (-.f64 1 (/.f64 y z)))
7.0ms
(sqrt.f64 (-.f64 1 (/.f64 y z)))
Compiler

Compiled 7820 to 4257 computations (45.6% saved)

series877.0ms (6.1%)

Error
0b
Counts
4 → 72
Calls

4 calls:

326.0ms
(/.f64 (+.f64 y x) (sqrt.f64 (-.f64 1 (/.f64 y z))))
283.0ms
(*.f64 (/.f64 1 (sqrt.f64 (-.f64 1 (/.f64 y z)))) (/.f64 (+.f64 y x) (sqrt.f64 (-.f64 1 (/.f64 y z)))))
93.0ms
(sqrt.f64 (-.f64 1 (/.f64 y z)))
81.0ms
(sqrt.f64 (-.f64 1 (/.f64 y z)))
Compiler

Compiled 3976 to 2837 computations (28.6% saved)

simplify751.0ms (5.3%)

Algorithm
egg-herbie
Rules
612×distribute-rgt-in_binary64_25944
569×distribute-lft-in_binary64_25943
289×associate-/l*_binary64_25939
272×associate-*r*_binary64_25934
236×associate-*l/_binary64_25937
207×associate-*r/_binary64_25936
186×*-commutative_binary64_25925
184×associate-*l*_binary64_25935
132×associate-/l/_binary64_25941
106×times-frac_binary64_26000
105×associate-+r+_binary64_25926
100×cancel-sign-sub-inv_binary64_25960
91×+-commutative_binary64_25924
76×associate-+l+_binary64_25927
71×distribute-neg-in_binary64_25955
68×distribute-rgt-neg-in_binary64_25952
66×sub-neg_binary64_25987
64×*-lft-identity_binary64_25983 associate-/r*_binary64_25938
51×distribute-neg-frac_binary64_25958
50×distribute-lft-neg-in_binary64_25951
48×neg-sub0_binary64_25989 *-rgt-identity_binary64_25984
45×neg-mul-1_binary64_25990
44×sqr-pow_binary64_25966
29×distribute-rgt-out_binary64_25947
26×associate-/r/_binary64_25940
24×exp-prod_binary64_26046 /-rgt-identity_binary64_25985
22×log-div_binary64_26081
20×cube-div_binary64_26023 unsub-neg_binary64_25988
19×pow-sqr_binary64_25967
17×swap-sqr_binary64_25961
16×distribute-lft-out_binary64_25945
15×associate--r+_binary64_25930
14×div-sub_binary64_25999
13×log-prod_binary64_26080
11×pow-plus_binary64_26057 distribute-neg-out_binary64_25956 distribute-lft-neg-out_binary64_25953 distribute-rgt1-in_binary64_25950
log-rec_binary64_26082 unswap-sqr_binary64_25962 distribute-rgt-out--_binary64_25948
exp-sum_binary64_26040 cube-prod_binary64_26022
cube-unmult_binary64_26031
log-pow_binary64_26083 mul-1-neg_binary64_25986 associate-+l-_binary64_25929
unpow3_binary64_26060 cube-mult_binary64_26024 rem-sqrt-square_binary64_26007 difference-of-squares_binary64_25963 distribute-rgt-neg-out_binary64_25954
pow-base-1_binary64_26054 associate-+r-_binary64_25928
unpow2_binary64_26059 unpow1_binary64_26052 sub0-neg_binary64_25981 remove-double-div_binary64_25970 associate--l+_binary64_25931
exp-sqrt_binary64_26047 div-exp_binary64_26045 rec-exp_binary64_26044 prod-exp_binary64_26043 1-exp_binary64_26038 exp-1-e_binary64_26037 rem-log-exp_binary64_26035 rem-cbrt-cube_binary64_26018 rem-square-sqrt_binary64_26006 +-rgt-identity_binary64_25979 *-inverses_binary64_25974 distribute-lft1-in_binary64_25949 associate--r-_binary64_25933
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_26257 erf-erfc_binary64_26256 erf-odd_binary64_26255 if-if-and-not_binary64_26254 if-if-and_binary64_26253 if-if-or-not_binary64_26252 if-if-or_binary64_26251 if-not_binary64_26250 if-same_binary64_26249 if-false_binary64_26248 if-true_binary64_26247 not-gte_binary64_26246 not-lte_binary64_26245 not-gt_binary64_26244 not-lt_binary64_26243 gte-same_binary64_26242 lte-same_binary64_26241 gt-same_binary64_26240 lt-same_binary64_26239 sinh---cosh_binary64_26186 sinh-+-cosh_binary64_26185 sinh-cosh_binary64_26184 tanh-def-c_binary64_26183 tanh-def-b_binary64_26182 tanh-def-a_binary64_26181 cosh-def_binary64_26180 sinh-def_binary64_26179 tan-neg_binary64_26126 cos-neg_binary64_26125 sin-neg_binary64_26124 tan-0_binary64_26123 cos-0_binary64_26122 sin-0_binary64_26121 hang-m-tan_binary64_26120 hang-p-tan_binary64_26119 hang-m0-tan_binary64_26118 hang-p0-tan_binary64_26117 hang-0m-tan_binary64_26116 hang-0p-tan_binary64_26115 tan-+PI/2_binary64_26114 tan-+PI_binary64_26113 tan-PI_binary64_26112 tan-PI/3_binary64_26111 tan-PI/4_binary64_26110 tan-PI/6_binary64_26109 cos-+PI/2_binary64_26108 cos-+PI_binary64_26107 cos-PI_binary64_26106 cos-PI/2_binary64_26105 cos-PI/3_binary64_26104 cos-PI/4_binary64_26103 cos-PI/6_binary64_26102 sin-+PI/2_binary64_26101 sin-+PI_binary64_26100 sin-PI_binary64_26099 sin-PI/2_binary64_26098 sin-PI/3_binary64_26097 sin-PI/4_binary64_26096 sin-PI/6_binary64_26095 sub-1-sin_binary64_26094 sub-1-cos_binary64_26093 -1-add-sin_binary64_26092 -1-add-cos_binary64_26091 1-sub-sin_binary64_26090 1-sub-cos_binary64_26089 cos-sin-sum_binary64_26088 log-E_binary64_26084 pow-base-0_binary64_26078 unpow1/3_binary64_26061 unpow1/2_binary64_26058 exp-to-pow_binary64_26056 unpow0_binary64_26053 unpow-1_binary64_26051 exp-lft-cube_binary64_26050 exp-lft-sqr_binary64_26049 exp-cbrt_binary64_26048 exp-diff_binary64_26042 exp-neg_binary64_26041 e-exp-1_binary64_26039 exp-0_binary64_26036 rem-exp-log_binary64_26034 cube-neg_binary64_26021 rem-3cbrt-rft_binary64_26020 rem-3cbrt-lft_binary64_26019 rem-cube-cbrt_binary64_26017 sqr-abs_binary64_26009 sqr-neg_binary64_26008 remove-double-neg_binary64_25982 --rgt-identity_binary64_25980 +-lft-identity_binary64_25978 mul0-rgt_binary64_25977 mul0-lft_binary64_25976 div0_binary64_25975 +-inverses_binary64_25973 lft-mult-inverse_binary64_25972 rgt-mult-inverse_binary64_25971 difference-of-sqr--1_binary64_25965 difference-of-sqr-1_binary64_25964 cancel-sign-sub_binary64_25959 distribute-frac-neg_binary64_25957 distribute-lft-out--_binary64_25946 count-2_binary64_25942 associate--l-_binary64_25932
Counts
315 → 462
Iterations

Useful iterations: 2 (0.0ms)

IterNodesCost
03719026
19738083
235607971

prune1.1s (7.5%)

Pruning

5 alts after pruning (3 fresh and 2 done)

PrunedKeptTotal
New4620462
Fresh033
Picked011
Done011
Total4625467
Error
0b
Counts
467 → 5
Compiler

Compiled 14813 to 7590 computations (48.8% saved)

localize9.0ms (0.1%)

Local error

Found 4 expressions with local error:

0.0b
(+.f64 z (/.f64 (*.f64 z z) y))
2.6b
(-.f64 (neg.f64 (*.f64 (/.f64 x y) z)) (+.f64 z (/.f64 (*.f64 z z) y)))
6.0b
(*.f64 (/.f64 x y) z)
9.1b
(/.f64 (*.f64 z z) y)

rewrite115.0ms (0.8%)

Algorithm
rewrite-expression-head
Error
0b
Rules
24×*-un-lft-identity_binary64_25994
22×add-sqr-sqrt_binary64_26016
16×add-log-exp_binary64_26033
15×add-cube-cbrt_binary64_26029
14×add-exp-log_binary64_26032 add-cbrt-cube_binary64_26030
13×times-frac_binary64_26000 associate-*l*_binary64_25935
pow1_binary64_26055
diff-log_binary64_26086 cancel-sign-sub-inv_binary64_25960
prod-exp_binary64_26043 div-exp_binary64_26045 cbrt-undiv_binary64_26028 cbrt-unprod_binary64_26027 associate-/r*_binary64_25938 associate-*l/_binary64_25937 associate-*r*_binary64_25934 sum-log_binary64_26085 distribute-lft-out_binary64_25945
div-inv_binary64_25991 unswap-sqr_binary64_25962 neg-log_binary64_26087 flip3-+_binary64_25997 distribute-neg-frac_binary64_25958 frac-sub_binary64_26003 flip-+_binary64_25968 distribute-lft-out--_binary64_25946
frac-2neg_binary64_26005 clear-num_binary64_25993 associate-/l*_binary64_25939 pow-prod-down_binary64_26065 *-commutative_binary64_25925 flip3--_binary64_25998 sub-neg_binary64_25987 flip--_binary64_25969 difference-of-squares_binary64_25963 neg-sub0_binary64_25989 associate--l-_binary64_25932 associate--r+_binary64_25930 +-commutative_binary64_25924
Counts
4 → 90
Calls

4 calls:

10.0ms
(-.f64 (neg.f64 (*.f64 (/.f64 x y) z)) (+.f64 z (/.f64 (*.f64 z z) y)))
6.0ms
(*.f64 (/.f64 x y) z)
5.0ms
(+.f64 z (/.f64 (*.f64 z z) y))
5.0ms
(/.f64 (*.f64 z z) y)
Compiler

Compiled 2011 to 419 computations (79.2% saved)

series748.0ms (5.2%)

Error
0b
Counts
4 → 45
Calls

4 calls:

337.0ms
(-.f64 (neg.f64 (*.f64 (/.f64 x y) z)) (+.f64 z (/.f64 (*.f64 z z) y)))
152.0ms
(*.f64 (/.f64 x y) z)
122.0ms
(+.f64 z (/.f64 (*.f64 z z) y))
109.0ms
(/.f64 (*.f64 z z) y)
Compiler

Compiled 1506 to 936 computations (37.8% saved)

simplify436.0ms (3%)

Algorithm
egg-herbie
Rules
605×associate-/l*_binary64_25939
397×times-frac_binary64_26000
343×distribute-rgt-in_binary64_25944
311×distribute-lft-in_binary64_25943
218×associate-/l/_binary64_25941
141×associate-/r/_binary64_25940
132×associate-*l*_binary64_25935
123×distribute-rgt-neg-in_binary64_25952 associate-*r*_binary64_25934
117×distribute-rgt-neg-out_binary64_25954
116×distribute-lft-neg-out_binary64_25953
114×cancel-sign-sub-inv_binary64_25960
110×associate-*l/_binary64_25937
99×distribute-lft-neg-in_binary64_25951
79×*-commutative_binary64_25925
77×distribute-neg-frac_binary64_25958 associate-*r/_binary64_25936
74×sub-neg_binary64_25987
68×neg-sub0_binary64_25989
66×distribute-rgt-out_binary64_25947
55×neg-mul-1_binary64_25990
53×exp-prod_binary64_26046
50×sqr-pow_binary64_25966
46×cube-prod_binary64_26022
44×unsub-neg_binary64_25988
43×distribute-neg-in_binary64_25955
36×unswap-sqr_binary64_25962
28×log-prod_binary64_26080
27×cube-div_binary64_26023
26×+-commutative_binary64_25924
23×log-div_binary64_26081 associate-/r*_binary64_25938
21×distribute-rgt-out--_binary64_25948
19×exp-sum_binary64_26040 swap-sqr_binary64_25961 distribute-neg-out_binary64_25956
18×pow-sqr_binary64_25967 distribute-lft-out_binary64_25945
17×div-sub_binary64_25999
16×unpow3_binary64_26060
13×*-rgt-identity_binary64_25984 associate-+l+_binary64_25927 associate-+r+_binary64_25926
12×cube-mult_binary64_26024
10×associate--r+_binary64_25930
pow-plus_binary64_26057 *-lft-identity_binary64_25983
exp-diff_binary64_26042
mul-1-neg_binary64_25986
cube-unmult_binary64_26031 difference-of-squares_binary64_25963 distribute-frac-neg_binary64_25957 associate-+l-_binary64_25929
prod-exp_binary64_26043 cube-neg_binary64_26021 sqr-neg_binary64_26008 associate-+r-_binary64_25928
div-exp_binary64_26045 sub0-neg_binary64_25981 distribute-rgt1-in_binary64_25950
/-rgt-identity_binary64_25985 +-rgt-identity_binary64_25979 distribute-lft1-in_binary64_25949 associate--l+_binary64_25931
log-pow_binary64_26083
log-rec_binary64_26082 unpow2_binary64_26059 pow-base-1_binary64_26054 unpow1_binary64_26052 exp-sqrt_binary64_26047 rec-exp_binary64_26044 1-exp_binary64_26038 exp-1-e_binary64_26037 rem-log-exp_binary64_26035 rem-3cbrt-lft_binary64_26019 rem-sqrt-square_binary64_26007 rem-square-sqrt_binary64_26006 remove-double-neg_binary64_25982 div0_binary64_25975 *-inverses_binary64_25974 cancel-sign-sub_binary64_25959 distribute-lft-out--_binary64_25946 count-2_binary64_25942
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_26257 erf-erfc_binary64_26256 erf-odd_binary64_26255 if-if-and-not_binary64_26254 if-if-and_binary64_26253 if-if-or-not_binary64_26252 if-if-or_binary64_26251 if-not_binary64_26250 if-same_binary64_26249 if-false_binary64_26248 if-true_binary64_26247 not-gte_binary64_26246 not-lte_binary64_26245 not-gt_binary64_26244 not-lt_binary64_26243 gte-same_binary64_26242 lte-same_binary64_26241 gt-same_binary64_26240 lt-same_binary64_26239 sinh---cosh_binary64_26186 sinh-+-cosh_binary64_26185 sinh-cosh_binary64_26184 tanh-def-c_binary64_26183 tanh-def-b_binary64_26182 tanh-def-a_binary64_26181 cosh-def_binary64_26180 sinh-def_binary64_26179 tan-neg_binary64_26126 cos-neg_binary64_26125 sin-neg_binary64_26124 tan-0_binary64_26123 cos-0_binary64_26122 sin-0_binary64_26121 hang-m-tan_binary64_26120 hang-p-tan_binary64_26119 hang-m0-tan_binary64_26118 hang-p0-tan_binary64_26117 hang-0m-tan_binary64_26116 hang-0p-tan_binary64_26115 tan-+PI/2_binary64_26114 tan-+PI_binary64_26113 tan-PI_binary64_26112 tan-PI/3_binary64_26111 tan-PI/4_binary64_26110 tan-PI/6_binary64_26109 cos-+PI/2_binary64_26108 cos-+PI_binary64_26107 cos-PI_binary64_26106 cos-PI/2_binary64_26105 cos-PI/3_binary64_26104 cos-PI/4_binary64_26103 cos-PI/6_binary64_26102 sin-+PI/2_binary64_26101 sin-+PI_binary64_26100 sin-PI_binary64_26099 sin-PI/2_binary64_26098 sin-PI/3_binary64_26097 sin-PI/4_binary64_26096 sin-PI/6_binary64_26095 sub-1-sin_binary64_26094 sub-1-cos_binary64_26093 -1-add-sin_binary64_26092 -1-add-cos_binary64_26091 1-sub-sin_binary64_26090 1-sub-cos_binary64_26089 cos-sin-sum_binary64_26088 log-E_binary64_26084 pow-base-0_binary64_26078 unpow1/3_binary64_26061 unpow1/2_binary64_26058 exp-to-pow_binary64_26056 unpow0_binary64_26053 unpow-1_binary64_26051 exp-lft-cube_binary64_26050 exp-lft-sqr_binary64_26049 exp-cbrt_binary64_26048 exp-neg_binary64_26041 e-exp-1_binary64_26039 exp-0_binary64_26036 rem-exp-log_binary64_26034 rem-3cbrt-rft_binary64_26020 rem-cbrt-cube_binary64_26018 rem-cube-cbrt_binary64_26017 sqr-abs_binary64_26009 --rgt-identity_binary64_25980 +-lft-identity_binary64_25978 mul0-rgt_binary64_25977 mul0-lft_binary64_25976 +-inverses_binary64_25973 lft-mult-inverse_binary64_25972 rgt-mult-inverse_binary64_25971 remove-double-div_binary64_25970 difference-of-sqr--1_binary64_25965 difference-of-sqr-1_binary64_25964 associate--r-_binary64_25933 associate--l-_binary64_25932
Counts
135 → 424
Iterations

Useful iterations: 2 (0.0ms)

IterNodesCost
01791995
14881894
217221787

prune396.0ms (2.8%)

Pruning

5 alts after pruning (2 fresh and 3 done)

PrunedKeptTotal
New4240424
Fresh022
Picked011
Done022
Total4245429
Error
0b
Counts
429 → 5
Compiler

Compiled 10326 to 1534 computations (85.1% saved)

regimes736.0ms (5.1%)

Accuracy

Total 0.2b remaining (99.5%)

Threshold costs 0.2b (99.5%)

Compiler

Compiled 4172 to 3144 computations (24.6% saved)

bsearch3.0ms (0%)

Compiler

Compiled 9 to 8 computations (11.1% saved)

simplify12.0ms (0.1%)

Algorithm
egg-herbie
Rules
15×+-commutative_binary64_25924
11×sub-neg_binary64_25987 *-commutative_binary64_25925
10×neg-mul-1_binary64_25990 neg-sub0_binary64_25989
unsub-neg_binary64_25988 distribute-neg-in_binary64_25955
distribute-neg-frac_binary64_25958
distribute-rgt-neg-in_binary64_25952 distribute-lft-neg-in_binary64_25951
if-if-or-not_binary64_26252 1-exp_binary64_26038
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_26254 if-if-and_binary64_26253 if-if-or_binary64_26251 if-not_binary64_26250 if-same_binary64_26249 if-false_binary64_26248 if-true_binary64_26247 tan-0_binary64_26123 cos-0_binary64_26122 sin-0_binary64_26121 unpow1_binary64_26052 e-exp-1_binary64_26039 exp-1-e_binary64_26037 exp-0_binary64_26036 sqr-abs_binary64_26009 sqr-neg_binary64_26008 mul-1-neg_binary64_25986 /-rgt-identity_binary64_25985 *-rgt-identity_binary64_25984 *-lft-identity_binary64_25983 remove-double-neg_binary64_25982 sub0-neg_binary64_25981 --rgt-identity_binary64_25980 +-rgt-identity_binary64_25979 +-lft-identity_binary64_25978 cancel-sign-sub-inv_binary64_25960 cancel-sign-sub_binary64_25959 distribute-frac-neg_binary64_25957 distribute-neg-out_binary64_25956 distribute-rgt-neg-out_binary64_25954 distribute-lft-neg-out_binary64_25953
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
02781
14481
26381
38881
410381
511181
611381
Proof
(=> (if real (<= f64 (/ f64 (+ f64 h0 h1) (- f64 1 (/ f64 h1 h2))) -2618853769398055/159667224762777584932509817042947085285396100834836603320203779394976951349517125262796637239410856087147395747535399619517795039071487492859133743862786513625600453836086854121403017715549038974612268539563513919466464836409669631111108421475843532600569672550060483331388679618427520794230784) (+ f64 (/ f64 h1 (- f64 1 (/ f64 h1 h2))) (/ f64 h0 (- f64 1 (/ f64 h1 h2)))) (if real (<= f64 (/ f64 (+ f64 h0 h1) (- f64 1 (/ f64 h1 h2))) 0) (neg f64 (+ f64 (/ f64 (* f64 h0 h2) h1) (+ f64 h2 (/ f64 (pow f64 h2 2) h1)))) (+ f64 (/ f64 h1 (- f64 1 (/ f64 h1 h2))) (/ f64 h0 (- f64 1 (/ f64 h1 h2))))))) if-if-or-not_binary64_26252 => (if real (or real (<= f64 (/ f64 (+ f64 h0 h1) (- f64 1 (/ f64 h1 h2))) -2618853769398055/159667224762777584932509817042947085285396100834836603320203779394976951349517125262796637239410856087147395747535399619517795039071487492859133743862786513625600453836086854121403017715549038974612268539563513919466464836409669631111108421475843532600569672550060483331388679618427520794230784) (not real (<= f64 (/ f64 (+ f64 h0 h1) (- f64 1 (/ f64 h1 h2))) 0))) (+ f64 (/ f64 h1 (- f64 1 (/ f64 h1 h2))) (/ f64 h0 (- f64 1 (/ f64 h1 h2)))) (=> (neg f64 (+ f64 (/ f64 (* f64 h0 h2) h1) (+ f64 h2 (/ f64 (pow f64 h2 2) h1)))))) distribute-neg-in_binary64_25955 => (if real (or real (<= f64 (/ f64 (+ f64 h0 h1) (- f64 1 (/ f64 h1 h2))) -2618853769398055/159667224762777584932509817042947085285396100834836603320203779394976951349517125262796637239410856087147395747535399619517795039071487492859133743862786513625600453836086854121403017715549038974612268539563513919466464836409669631111108421475843532600569672550060483331388679618427520794230784) (not real (<= f64 (/ f64 (+ f64 h0 h1) (- f64 1 (/ f64 h1 h2))) 0))) (+ f64 (/ f64 h1 (- f64 1 (/ f64 h1 h2))) (/ f64 h0 (- f64 1 (/ f64 h1 h2)))) (=> (+ f64 (neg f64 (/ f64 (* f64 h0 h2) h1)) (neg f64 (+ f64 h2 (/ f64 (pow f64 h2 2) h1)))))) unsub-neg_binary64_25988 => (if real (or real (<= f64 (/ f64 (+ f64 h0 h1) (- f64 1 (/ f64 h1 h2))) -2618853769398055/159667224762777584932509817042947085285396100834836603320203779394976951349517125262796637239410856087147395747535399619517795039071487492859133743862786513625600453836086854121403017715549038974612268539563513919466464836409669631111108421475843532600569672550060483331388679618427520794230784) (not real (<= f64 (/ f64 (+ f64 h0 h1) (- f64 1 (/ f64 h1 h2))) 0))) (+ f64 (/ f64 h1 (- f64 1 (/ f64 h1 h2))) (/ f64 h0 (- f64 1 (/ f64 h1 h2)))) (- f64 (=> (neg f64 (/ f64 (* f64 h0 h2) h1))) (+ f64 h2 (/ f64 (pow f64 h2 2) h1)))) distribute-neg-frac_binary64_25958 => (if real (or real (<= f64 (/ f64 (+ f64 h0 h1) (- f64 1 (/ f64 h1 h2))) -2618853769398055/159667224762777584932509817042947085285396100834836603320203779394976951349517125262796637239410856087147395747535399619517795039071487492859133743862786513625600453836086854121403017715549038974612268539563513919466464836409669631111108421475843532600569672550060483331388679618427520794230784) (not real (<= f64 (/ f64 (+ f64 h0 h1) (- f64 1 (/ f64 h1 h2))) 0))) (+ f64 (/ f64 h1 (- f64 1 (/ f64 h1 h2))) (/ f64 h0 (- f64 1 (/ f64 h1 h2)))) (- f64 (/ f64 (=> (neg f64 (* f64 h0 h2))) h1) (+ f64 h2 (/ f64 (pow f64 h2 2) h1)))) distribute-rgt-neg-in_binary64_25952 => (if real (or real (<= f64 (/ f64 (+ f64 h0 h1) (- f64 1 (/ f64 h1 h2))) -2618853769398055/159667224762777584932509817042947085285396100834836603320203779394976951349517125262796637239410856087147395747535399619517795039071487492859133743862786513625600453836086854121403017715549038974612268539563513919466464836409669631111108421475843532600569672550060483331388679618427520794230784) (not real (<= f64 (/ f64 (+ f64 h0 h1) (- f64 1 (/ f64 h1 h2))) 0))) (+ f64 (/ f64 h1 (- f64 1 (/ f64 h1 h2))) (/ f64 h0 (- f64 1 (/ f64 h1 h2)))) (- f64 (/ f64 (* f64 h0 (neg f64 h2)) h1) (+ f64 h2 (/ f64 (pow f64 h2 2) h1))))

end0.0ms (0%)

sample1.5s (10.4%)

Algorithm
intervals
Results
250.0ms7999×body128valid
0.0msbody512valid
Compiler

Compiled 1122 to 831 computations (25.9% saved)

Profiling

Loading profile data...