Details

analyze877.0ms (6.7%)

Algorithm

1×

Search

True	Other	False	Iter
0%	99.8%	0.2%	0
0%	99.8%	0.2%	1
0%	99.8%	0.2%	2
0%	99.8%	0.2%	3
0%	99.8%	0.2%	4
0%	99.8%	0.2%	5
0%	99.8%	0.2%	6
0%	99.8%	0.2%	7
0%	99.8%	0.2%	8
6.2%	93.6%	0.2%	9
6.2%	82.7%	11.1%	10
12.5%	73.7%	13.8%	11
15.6%	59.5%	25%	12
17.9%	53.3%	28.8%	13
22.4%	47.2%	30.4%	14

Compiler

Compiled 14 to 12 computations (14.3% saved)

sample28.0ms (0.2%)

Algorithm

1×

intervals

Results

9.0ms	256×	body	128	valid
4.0ms	100×	body	128	invalid

Compiler

Compiled 27 to 27 computations (0% saved)

simplify970.0ms (7.4%)

Algorithm

1×	egg-herbie

Rules

755×	`exp-prod_binary64_11724`
754×	`cube-prod_binary64_11700`
598×	`unsub-neg_binary64_11666`
327×	`swap-sqr_binary64_11639`
261×	`*-commutative_binary64_11603`
253×	`distribute-rgt-out_binary64_11625`
226×	`distribute-rgt-neg-in_binary64_11630`
212×	`distribute-rgt-out--_binary64_11626`
182×	`associate--r+_binary64_11608`
163×	`associate--l-_binary64_11610`
157×	`associate--l+_binary64_11609`
152×	`associate--r-_binary64_11611` `associate-+l-_binary64_11607`
141×	`distribute-neg-out_binary64_11634`
134×	`distribute-rgt1-in_binary64_11628`
133×	`associate-l_binary64_11613`
121×	`distribute-rgt-in_binary64_11622`
119×	`associate-r_binary64_11612`
112×	`distribute-rgt-neg-out_binary64_11632`
110×	`sub-neg_binary64_11665`
105×	`distribute-lft-neg-in_binary64_11629`
80×	`+-commutative_binary64_11602`
76×	`associate-+r+_binary64_11604`
73×	`neg-sub0_binary64_11667`
67×	`associate-+l+_binary64_11605`
66×	`neg-mul-1_binary64_11668`
65×	`cancel-sign-sub-inv_binary64_11638`
61×	`distribute-lft-in_binary64_11621`
59×	`associate-+r-_binary64_11606`
46×	`distribute-lft-neg-out_binary64_11631`
43×	`distribute-neg-in_binary64_11633`
39×	`remove-double-neg_binary64_11660`
23×	`mul0-rgt_binary64_11655` `mul0-lft_binary64_11654`
18×	`exp-diff_binary64_11720` `distribute-lft1-in_binary64_11627`
16×	`difference-of-squares_binary64_11641`
15×	`count-2_binary64_11620`
14×	`exp-sum_binary64_11718` `+-inverses_binary64_11651`
13×	`sqr-neg_binary64_11686`
11×	`sub0-neg_binary64_11659`
7×	`--rgt-identity_binary64_11658` `unswap-sqr_binary64_11640`
5×	`pow-plus_binary64_11735` `+-rgt-identity_binary64_11657` `difference-of-sqr--1_binary64_11643`
4×	`+-lft-identity_binary64_11656`
3×	`cube-unmult_binary64_11709`
1×	`exp-lft-sqr_binary64_11727` `1-exp_binary64_11716` `mul-1-neg_binary64_11664` `pow-sqr_binary64_11645` `sqr-pow_binary64_11644` `distribute-lft-out--_binary64_11624` `distribute-lft-out_binary64_11623`
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_11935` `erf-erfc_binary64_11934` `erf-odd_binary64_11933` `if-if-and-not_binary64_11932` `if-if-and_binary64_11931` `if-if-or-not_binary64_11930` `if-if-or_binary64_11929` `if-not_binary64_11928` `if-same_binary64_11927` `if-false_binary64_11926` `if-true_binary64_11925` `not-gte_binary64_11924` `not-lte_binary64_11923` `not-gt_binary64_11922` `not-lt_binary64_11921` `gte-same_binary64_11920` `lte-same_binary64_11919` `gt-same_binary64_11918` `lt-same_binary64_11917` `sinh---cosh_binary64_11864` `sinh-+-cosh_binary64_11863` `sinh-cosh_binary64_11862` `tanh-def-c_binary64_11861` `tanh-def-b_binary64_11860` `tanh-def-a_binary64_11859` `cosh-def_binary64_11858` `sinh-def_binary64_11857` `tan-neg_binary64_11804` `cos-neg_binary64_11803` `sin-neg_binary64_11802` `tan-0_binary64_11801` `cos-0_binary64_11800` `sin-0_binary64_11799` `hang-m-tan_binary64_11798` `hang-p-tan_binary64_11797` `hang-m0-tan_binary64_11796` `hang-p0-tan_binary64_11795` `hang-0m-tan_binary64_11794` `hang-0p-tan_binary64_11793` `tan-+PI/2_binary64_11792` `tan-+PI_binary64_11791` `tan-PI_binary64_11790` `tan-PI/3_binary64_11789` `tan-PI/4_binary64_11788` `tan-PI/6_binary64_11787` `cos-+PI/2_binary64_11786` `cos-+PI_binary64_11785` `cos-PI_binary64_11784` `cos-PI/2_binary64_11783` `cos-PI/3_binary64_11782` `cos-PI/4_binary64_11781` `cos-PI/6_binary64_11780` `sin-+PI/2_binary64_11779` `sin-+PI_binary64_11778` `sin-PI_binary64_11777` `sin-PI/2_binary64_11776` `sin-PI/3_binary64_11775` `sin-PI/4_binary64_11774` `sin-PI/6_binary64_11773` `sub-1-sin_binary64_11772` `sub-1-cos_binary64_11771` `-1-add-sin_binary64_11770` `-1-add-cos_binary64_11769` `1-sub-sin_binary64_11768` `1-sub-cos_binary64_11767` `cos-sin-sum_binary64_11766` `log-E_binary64_11762` `log-pow_binary64_11761` `log-rec_binary64_11760` `log-div_binary64_11759` `log-prod_binary64_11758` `pow-base-0_binary64_11756` `unpow1/3_binary64_11739` `unpow3_binary64_11738` `unpow2_binary64_11737` `unpow1/2_binary64_11736` `exp-to-pow_binary64_11734` `pow-base-1_binary64_11732` `unpow0_binary64_11731` `unpow1_binary64_11730` `unpow-1_binary64_11729` `exp-lft-cube_binary64_11728` `exp-cbrt_binary64_11726` `exp-sqrt_binary64_11725` `div-exp_binary64_11723` `rec-exp_binary64_11722` `prod-exp_binary64_11721` `exp-neg_binary64_11719` `e-exp-1_binary64_11717` `exp-1-e_binary64_11715` `exp-0_binary64_11714` `rem-log-exp_binary64_11713` `rem-exp-log_binary64_11712` `cube-mult_binary64_11702` `cube-div_binary64_11701` `cube-neg_binary64_11699` `rem-3cbrt-rft_binary64_11698` `rem-3cbrt-lft_binary64_11697` `rem-cbrt-cube_binary64_11696` `rem-cube-cbrt_binary64_11695` `sqr-abs_binary64_11687` `rem-sqrt-square_binary64_11685` `rem-square-sqrt_binary64_11684` `times-frac_binary64_11678` `div-sub_binary64_11677` `/-rgt-identity_binary64_11663` `-rgt-identity_binary64_11662` `-lft-identity_binary64_11661` `div0_binary64_11653` `-inverses_binary64_11652` `lft-mult-inverse_binary64_11650` `rgt-mult-inverse_binary64_11649` `remove-double-div_binary64_11648` `difference-of-sqr-1_binary64_11642` `cancel-sign-sub_binary64_11637` `distribute-neg-frac_binary64_11636` `distribute-frac-neg_binary64_11635` `associate-/l/_binary64_11619` `associate-/r/_binary64_11618` `associate-/l_binary64_11617` `associate-/r_binary64_11616` `associate-l/_binary64_11615` `associate-*r/_binary64_11614`

Counts

1 → 4

Iterations

Useful iterations: 0 (0.0ms)

Iter	Nodes	Cost
0	12	19
1	23	19
2	69	19
3	221	19
4	437	19
5	680	19
6	1677	19
7	3414	19

prune5.0ms (0%)

Pruning

1 alts after pruning (1 fresh and 0 done)

	Pruned	Kept	Total
New	4	0	4
Fresh	0	1	1
Picked	0	0	0
Done	0	0	0
Total	4	1	5

Error

5.9b

Counts

5 → 1

Compiler

Compiled 65 to 35 computations (46.2% saved)

localize13.0ms (0.1%)

Local error

Found 3 expressions with local error:

0.0b	(-.f64 (.f64 x x) (.f64 (.f64 y 4) (-.f64 (.f64 z z) t)))
0.0b	(-.f64 (*.f64 z z) t)
5.5b	(.f64 (.f64 y 4) (-.f64 (*.f64 z z) t))

rewrite99.0ms (0.7%)

Algorithm

1×	rewrite-expression-head

Error

2.3b

Rules

16×	`cancel-sign-sub-inv_binary64_11638`
11×	`add-sqr-sqrt_binary64_11694`
9×	`add-cube-cbrt_binary64_11707` `*-un-lft-identity_binary64_11672`
8×	`pow1_binary64_11733` `add-exp-log_binary64_11710` `add-cbrt-cube_binary64_11708` `distribute-rgt-in_binary64_11622` `distribute-lft-in_binary64_11621` `associate--r+_binary64_11608`
7×	`add-log-exp_binary64_11711`
6×	`sub-neg_binary64_11665`
4×	`associate-r_binary64_11612`
3×	`pow-prod-down_binary64_11743` `prod-exp_binary64_11721` `cbrt-unprod_binary64_11705` `flip3--_binary64_11676` `flip--_binary64_11647`
2×	`associate-*r/_binary64_11614` `difference-of-squares_binary64_11641` `diff-log_binary64_11764`
1×	`associate-l_binary64_11613` `*-commutative_binary64_11603`

Counts

3 → 64

Calls

3 calls:

9.0ms	(.f64 (.f64 y 4) (-.f64 (*.f64 z z) t))
5.0ms	(-.f64 (.f64 x x) (.f64 (.f64 y 4) (-.f64 (.f64 z z) t)))
4.0ms	(-.f64 (*.f64 z z) t)

Compiler

Compiled 1409 to 532 computations (62.2% saved)

series1.0s (7.7%)

Error

5.2b

Counts

3 → 51

Calls

3 calls:

588.0ms	(-.f64 (.f64 x x) (.f64 (.f64 y 4) (-.f64 (.f64 z z) t)))
282.0ms	(.f64 (.f64 y 4) (-.f64 (*.f64 z z) t))
99.0ms	(-.f64 (*.f64 z z) t)

Compiler

Compiled 1707 to 1400 computations (18% saved)

simplify376.0ms (2.9%)

Algorithm

1×	egg-herbie

Rules

360×	`distribute-rgt-in_binary64_11622`
355×	`distribute-lft-in_binary64_11621`
335×	`*-commutative_binary64_11603`
284×	`times-frac_binary64_11678`
268×	`exp-prod_binary64_11724`
226×	`associate-l_binary64_11613`
202×	`distribute-rgt-neg-in_binary64_11630`
198×	`associate-r_binary64_11612`
188×	`cancel-sign-sub-inv_binary64_11638`
172×	`neg-sub0_binary64_11667`
170×	`distribute-lft-neg-in_binary64_11629`
169×	`neg-mul-1_binary64_11668`
149×	`exp-sum_binary64_11718`
62×	`distribute-lft-neg-out_binary64_11631`
61×	`cube-prod_binary64_11700`
57×	`sqr-pow_binary64_11644`
50×	`exp-diff_binary64_11720`
49×	`distribute-rgt-neg-out_binary64_11632`
44×	`sub-neg_binary64_11665`
43×	`+-commutative_binary64_11602`
42×	`associate-l/_binary64_11615` `associate-r/_binary64_11614`
40×	`exp-sqrt_binary64_11725`
39×	`unswap-sqr_binary64_11640`
35×	`distribute-rgt-out_binary64_11625`
31×	`log-prod_binary64_11758`
30×	`associate-+r+_binary64_11604`
29×	`pow-plus_binary64_11735`
27×	`associate-+l+_binary64_11605`
25×	`pow-sqr_binary64_11645`
23×	`cube-div_binary64_11701`
21×	`exp-neg_binary64_11719`
20×	`distribute-lft-out_binary64_11623` `associate-+r-_binary64_11606`
19×	`*-rgt-identity_binary64_11662` `swap-sqr_binary64_11639`
18×	`unpow3_binary64_11738`
17×	`*-lft-identity_binary64_11661` `distribute-neg-in_binary64_11633`
14×	`associate-+l-_binary64_11607`
13×	`log-div_binary64_11759`
12×	`difference-of-squares_binary64_11641` `associate--r+_binary64_11608`
9×	`cube-unmult_binary64_11709` `div-sub_binary64_11677`
8×	`cube-mult_binary64_11702`
4×	`distribute-rgt-out--_binary64_11626` `distribute-lft-out--_binary64_11624`
3×	`unsub-neg_binary64_11666` `+-rgt-identity_binary64_11657`
2×	`unpow2_binary64_11737` `pow-base-1_binary64_11732` `unpow1_binary64_11730` `div-exp_binary64_11723` `sqr-neg_binary64_11686` `rem-sqrt-square_binary64_11685` `associate-/l/_binary64_11619` `associate-/l*_binary64_11617` `associate--l+_binary64_11609`
1×	`log-pow_binary64_11761` `exp-lft-sqr_binary64_11727` `prod-exp_binary64_11721` `1-exp_binary64_11716` `exp-1-e_binary64_11715` `rem-log-exp_binary64_11713` `cube-neg_binary64_11699` `rem-3cbrt-lft_binary64_11697` `rem-square-sqrt_binary64_11684` `mul-1-neg_binary64_11664` `remove-double-neg_binary64_11660` `-inverses_binary64_11652` `distribute-neg-frac_binary64_11636` `associate-/r_binary64_11616` `associate--r-_binary64_11611`
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_11935` `erf-erfc_binary64_11934` `erf-odd_binary64_11933` `if-if-and-not_binary64_11932` `if-if-and_binary64_11931` `if-if-or-not_binary64_11930` `if-if-or_binary64_11929` `if-not_binary64_11928` `if-same_binary64_11927` `if-false_binary64_11926` `if-true_binary64_11925` `not-gte_binary64_11924` `not-lte_binary64_11923` `not-gt_binary64_11922` `not-lt_binary64_11921` `gte-same_binary64_11920` `lte-same_binary64_11919` `gt-same_binary64_11918` `lt-same_binary64_11917` `sinh---cosh_binary64_11864` `sinh-+-cosh_binary64_11863` `sinh-cosh_binary64_11862` `tanh-def-c_binary64_11861` `tanh-def-b_binary64_11860` `tanh-def-a_binary64_11859` `cosh-def_binary64_11858` `sinh-def_binary64_11857` `tan-neg_binary64_11804` `cos-neg_binary64_11803` `sin-neg_binary64_11802` `tan-0_binary64_11801` `cos-0_binary64_11800` `sin-0_binary64_11799` `hang-m-tan_binary64_11798` `hang-p-tan_binary64_11797` `hang-m0-tan_binary64_11796` `hang-p0-tan_binary64_11795` `hang-0m-tan_binary64_11794` `hang-0p-tan_binary64_11793` `tan-+PI/2_binary64_11792` `tan-+PI_binary64_11791` `tan-PI_binary64_11790` `tan-PI/3_binary64_11789` `tan-PI/4_binary64_11788` `tan-PI/6_binary64_11787` `cos-+PI/2_binary64_11786` `cos-+PI_binary64_11785` `cos-PI_binary64_11784` `cos-PI/2_binary64_11783` `cos-PI/3_binary64_11782` `cos-PI/4_binary64_11781` `cos-PI/6_binary64_11780` `sin-+PI/2_binary64_11779` `sin-+PI_binary64_11778` `sin-PI_binary64_11777` `sin-PI/2_binary64_11776` `sin-PI/3_binary64_11775` `sin-PI/4_binary64_11774` `sin-PI/6_binary64_11773` `sub-1-sin_binary64_11772` `sub-1-cos_binary64_11771` `-1-add-sin_binary64_11770` `-1-add-cos_binary64_11769` `1-sub-sin_binary64_11768` `1-sub-cos_binary64_11767` `cos-sin-sum_binary64_11766` `log-E_binary64_11762` `log-rec_binary64_11760` `pow-base-0_binary64_11756` `unpow1/3_binary64_11739` `unpow1/2_binary64_11736` `exp-to-pow_binary64_11734` `unpow0_binary64_11731` `unpow-1_binary64_11729` `exp-lft-cube_binary64_11728` `exp-cbrt_binary64_11726` `rec-exp_binary64_11722` `e-exp-1_binary64_11717` `exp-0_binary64_11714` `rem-exp-log_binary64_11712` `rem-3cbrt-rft_binary64_11698` `rem-cbrt-cube_binary64_11696` `rem-cube-cbrt_binary64_11695` `sqr-abs_binary64_11687` `/-rgt-identity_binary64_11663` `sub0-neg_binary64_11659` `--rgt-identity_binary64_11658` `+-lft-identity_binary64_11656` `mul0-rgt_binary64_11655` `mul0-lft_binary64_11654` `div0_binary64_11653` `+-inverses_binary64_11651` `lft-mult-inverse_binary64_11650` `rgt-mult-inverse_binary64_11649` `remove-double-div_binary64_11648` `difference-of-sqr--1_binary64_11643` `difference-of-sqr-1_binary64_11642` `cancel-sign-sub_binary64_11637` `distribute-frac-neg_binary64_11635` `distribute-neg-out_binary64_11634` `distribute-rgt1-in_binary64_11628` `distribute-lft1-in_binary64_11627` `count-2_binary64_11620` `associate-/r/_binary64_11618` `associate--l-_binary64_11610`

Counts

115 → 385

Iterations

Useful iterations: 1 (0.0ms)

Iter	Nodes	Cost
0	135	1791
1	401	1671
2	1339	1671
3	3757	1671

prune427.0ms (3.2%)

Pruning

5 alts after pruning (4 fresh and 1 done)

	Pruned	Kept	Total
New	381	4	385
Fresh	0	0	0
Picked	0	1	1
Done	0	0	0
Total	381	5	386

Error

0.0b

Counts

386 → 5

Compiler

Compiled 8239 to 3324 computations (59.7% saved)

localize19.0ms (0.1%)

Local error

Found 4 expressions with local error:

4.3b	(cbrt.f64 (.f64 y (.f64 4 (-.f64 (*.f64 z z) t))))
5.5b	(.f64 (.f64 y 4) (-.f64 (*.f64 z z) t))
5.5b	(.f64 (.f64 y 4) (-.f64 (*.f64 z z) t))
5.7b	(.f64 y (.f64 4 (-.f64 (*.f64 z z) t)))

rewrite261.0ms (2%)

Algorithm

1×	rewrite-expression-head

Error

0.0b

Rules

24×	`distribute-rgt-in_binary64_11622` `cancel-sign-sub-inv_binary64_11638` `distribute-lft-in_binary64_11621`
19×	`pow1_binary64_11733` `add-exp-log_binary64_11710` `add-cbrt-cube_binary64_11708`
17×	`add-sqr-sqrt_binary64_11694`
15×	`add-cube-cbrt_binary64_11707` `*-un-lft-identity_binary64_11672`
12×	`associate-*r/_binary64_11614`
9×	`pow-prod-down_binary64_11743` `prod-exp_binary64_11721` `cbrt-unprod_binary64_11705` `associate-r_binary64_11612`
8×	`sub-neg_binary64_11665`
5×	`associate-l_binary64_11613`
4×	`add-log-exp_binary64_11711` `flip3--_binary64_11676` `flip--_binary64_11647`
3×	`*-commutative_binary64_11603`
2×	`difference-of-squares_binary64_11641` `cbrt-div_binary64_11704`
1×	`pow1/3_binary64_11754` `cbrt-prod_binary64_11703`

Counts

4 → 105

Calls

4 calls:

10.0ms	(.f64 y (.f64 4 (-.f64 (*.f64 z z) t)))
10.0ms	(.f64 (.f64 y 4) (-.f64 (*.f64 z z) t))
10.0ms	(.f64 (.f64 y 4) (-.f64 (*.f64 z z) t))
7.0ms	(cbrt.f64 (.f64 y (.f64 4 (-.f64 (*.f64 z z) t))))

Compiler

Compiled 4675 to 2009 computations (57% saved)

series1.6s (12.4%)

Error

0.0b

Counts

4 → 60

Calls

4 calls:

609.0ms	(cbrt.f64 (.f64 y (.f64 4 (-.f64 (*.f64 z z) t))))
327.0ms	(.f64 (.f64 y 4) (-.f64 (*.f64 z z) t))
304.0ms	(.f64 (.f64 y 4) (-.f64 (*.f64 z z) t))
293.0ms	(.f64 y (.f64 4 (-.f64 (*.f64 z z) t)))

Compiler

Compiled 6411 to 4162 computations (35.1% saved)

simplify525.0ms (4%)

Algorithm

1×	egg-herbie

Rules

445×	`distribute-rgt-in_binary64_11622`
440×	`distribute-lft-in_binary64_11621`
383×	`times-frac_binary64_11678`
317×	`associate-l_binary64_11613`
279×	`associate-r_binary64_11612`
145×	`*-commutative_binary64_11603`
117×	`distribute-lft-neg-out_binary64_11631`
112×	`distribute-rgt-neg-in_binary64_11630`
89×	`distribute-lft-neg-in_binary64_11629`
82×	`distribute-rgt-neg-out_binary64_11632`
79×	`sqr-pow_binary64_11644`
69×	`cancel-sign-sub-inv_binary64_11638`
60×	`neg-sub0_binary64_11667`
55×	`neg-mul-1_binary64_11668` `sub-neg_binary64_11665`
46×	`exp-prod_binary64_11724`
43×	`unswap-sqr_binary64_11640`
39×	`exp-sum_binary64_11718`
37×	`distribute-neg-frac_binary64_11636`
32×	`log-prod_binary64_11758`
31×	`pow-sqr_binary64_11645`
26×	`+-commutative_binary64_11602`
24×	`associate-/l*_binary64_11617`
22×	`cube-prod_binary64_11700` `swap-sqr_binary64_11639`
19×	`associate-/r*_binary64_11616`
17×	`unsub-neg_binary64_11666` `-rgt-identity_binary64_11662` `-lft-identity_binary64_11661`
16×	`associate-*r/_binary64_11614`
15×	`div-sub_binary64_11677`
11×	`exp-diff_binary64_11720`
10×	`unpow1/3_binary64_11739` `pow-plus_binary64_11735` `cube-unmult_binary64_11709` `cancel-sign-sub_binary64_11637`
9×	`distribute-neg-out_binary64_11634` `distribute-lft-out_binary64_11623`
8×	`difference-of-squares_binary64_11641` `distribute-rgt-out_binary64_11625` `associate-*l/_binary64_11615`
7×	`log-div_binary64_11759`
6×	`distribute-frac-neg_binary64_11635` `distribute-neg-in_binary64_11633`
5×	`remove-double-neg_binary64_11660` `distribute-lft-out--_binary64_11624` `associate-/r/_binary64_11618`
4×	`unpow3_binary64_11738` `associate--r-_binary64_11611` `associate-+l+_binary64_11605`
3×	`log-rec_binary64_11760` `associate-+r+_binary64_11604`
2×	`unpow2_binary64_11737` `exp-to-pow_binary64_11734` `unpow1_binary64_11730` `cube-mult_binary64_11702` `rem-3cbrt-lft_binary64_11697` `--rgt-identity_binary64_11658` `distribute-rgt-out--_binary64_11626`
1×	`log-pow_binary64_11761` `exp-sqrt_binary64_11725` `prod-exp_binary64_11721` `1-exp_binary64_11716` `exp-1-e_binary64_11715` `rem-log-exp_binary64_11713` `rem-sqrt-square_binary64_11685` `rem-square-sqrt_binary64_11684` `mul-1-neg_binary64_11664` `+-rgt-identity_binary64_11657` `*-inverses_binary64_11652` `associate--l+_binary64_11609` `associate-+r-_binary64_11606`
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_11935` `erf-erfc_binary64_11934` `erf-odd_binary64_11933` `if-if-and-not_binary64_11932` `if-if-and_binary64_11931` `if-if-or-not_binary64_11930` `if-if-or_binary64_11929` `if-not_binary64_11928` `if-same_binary64_11927` `if-false_binary64_11926` `if-true_binary64_11925` `not-gte_binary64_11924` `not-lte_binary64_11923` `not-gt_binary64_11922` `not-lt_binary64_11921` `gte-same_binary64_11920` `lte-same_binary64_11919` `gt-same_binary64_11918` `lt-same_binary64_11917` `sinh---cosh_binary64_11864` `sinh-+-cosh_binary64_11863` `sinh-cosh_binary64_11862` `tanh-def-c_binary64_11861` `tanh-def-b_binary64_11860` `tanh-def-a_binary64_11859` `cosh-def_binary64_11858` `sinh-def_binary64_11857` `tan-neg_binary64_11804` `cos-neg_binary64_11803` `sin-neg_binary64_11802` `tan-0_binary64_11801` `cos-0_binary64_11800` `sin-0_binary64_11799` `hang-m-tan_binary64_11798` `hang-p-tan_binary64_11797` `hang-m0-tan_binary64_11796` `hang-p0-tan_binary64_11795` `hang-0m-tan_binary64_11794` `hang-0p-tan_binary64_11793` `tan-+PI/2_binary64_11792` `tan-+PI_binary64_11791` `tan-PI_binary64_11790` `tan-PI/3_binary64_11789` `tan-PI/4_binary64_11788` `tan-PI/6_binary64_11787` `cos-+PI/2_binary64_11786` `cos-+PI_binary64_11785` `cos-PI_binary64_11784` `cos-PI/2_binary64_11783` `cos-PI/3_binary64_11782` `cos-PI/4_binary64_11781` `cos-PI/6_binary64_11780` `sin-+PI/2_binary64_11779` `sin-+PI_binary64_11778` `sin-PI_binary64_11777` `sin-PI/2_binary64_11776` `sin-PI/3_binary64_11775` `sin-PI/4_binary64_11774` `sin-PI/6_binary64_11773` `sub-1-sin_binary64_11772` `sub-1-cos_binary64_11771` `-1-add-sin_binary64_11770` `-1-add-cos_binary64_11769` `1-sub-sin_binary64_11768` `1-sub-cos_binary64_11767` `cos-sin-sum_binary64_11766` `log-E_binary64_11762` `pow-base-0_binary64_11756` `unpow1/2_binary64_11736` `pow-base-1_binary64_11732` `unpow0_binary64_11731` `unpow-1_binary64_11729` `exp-lft-cube_binary64_11728` `exp-lft-sqr_binary64_11727` `exp-cbrt_binary64_11726` `div-exp_binary64_11723` `rec-exp_binary64_11722` `exp-neg_binary64_11719` `e-exp-1_binary64_11717` `exp-0_binary64_11714` `rem-exp-log_binary64_11712` `cube-div_binary64_11701` `cube-neg_binary64_11699` `rem-3cbrt-rft_binary64_11698` `rem-cbrt-cube_binary64_11696` `rem-cube-cbrt_binary64_11695` `sqr-abs_binary64_11687` `sqr-neg_binary64_11686` `/-rgt-identity_binary64_11663` `sub0-neg_binary64_11659` `+-lft-identity_binary64_11656` `mul0-rgt_binary64_11655` `mul0-lft_binary64_11654` `div0_binary64_11653` `+-inverses_binary64_11651` `lft-mult-inverse_binary64_11650` `rgt-mult-inverse_binary64_11649` `remove-double-div_binary64_11648` `difference-of-sqr--1_binary64_11643` `difference-of-sqr-1_binary64_11642` `distribute-rgt1-in_binary64_11628` `distribute-lft1-in_binary64_11627` `count-2_binary64_11620` `associate-/l/_binary64_11619` `associate--l-_binary64_11610` `associate--r+_binary64_11608` `associate-+l-_binary64_11607`

Counts

165 → 618

Iterations

Useful iterations: 2 (0.0ms)

Iter	Nodes	Cost
0	248	3023
1	619	2753
2	1910	2724

prune1.9s (14.6%)

Pruning

5 alts after pruning (3 fresh and 2 done)

	Pruned	Kept	Total
New	618	0	618
Fresh	0	3	3
Picked	0	1	1
Done	0	1	1
Total	618	5	623

Error

0.0b

Counts

623 → 5

Compiler

Compiled 26266 to 12174 computations (53.7% saved)

localize7.0ms (0.1%)

Local error

Found 1 expressions with local error:

0.2b	(.f64 z (.f64 z (*.f64 y 4)))

rewrite31.0ms (0.2%)

Algorithm

1×	rewrite-expression-head

Error

0.0b

Rules

10×	`pow1_binary64_11733` `add-exp-log_binary64_11710` `add-cbrt-cube_binary64_11708`
6×	`pow-prod-down_binary64_11743` `prod-exp_binary64_11721` `cbrt-unprod_binary64_11705`
3×	`associate-l_binary64_11613`
2×	`add-cube-cbrt_binary64_11707` `add-sqr-sqrt_binary64_11694` `*-un-lft-identity_binary64_11672`
1×	`add-log-exp_binary64_11711` `associate-r_binary64_11612` `*-commutative_binary64_11603`

Counts

1 → 21

Calls

1 calls:

8.0ms

(*.f64 z (*.f64 z (*.f64 y 4)))

Compiler

Compiled 367 to 194 computations (47.1% saved)

series130.0ms (1%)

Error

0.0b

Counts

1 → 6

Calls

1 calls:

125.0ms

(*.f64 z (*.f64 z (*.f64 y 4)))

Compiler

Compiled 198 to 173 computations (12.6% saved)

simplify226.0ms (1.7%)

Algorithm

1×	egg-herbie

Rules

487×	`times-frac_binary64_11678`
408×	`log-div_binary64_11759`
329×	`distribute-rgt-in_binary64_11622`
285×	`distribute-rgt-out_binary64_11625`
282×	`*-commutative_binary64_11603`
265×	`distribute-lft-in_binary64_11621`
208×	`associate-/l*_binary64_11617`
170×	`sqr-pow_binary64_11644`
151×	`associate-/l/_binary64_11619`
138×	`associate-/r/_binary64_11618`
135×	`swap-sqr_binary64_11639`
128×	`associate-r_binary64_11612`
124×	`associate-l_binary64_11613`
121×	`exp-prod_binary64_11724`
115×	`cube-prod_binary64_11700`
111×	`log-prod_binary64_11758`
107×	`associate-/r*_binary64_11616`
104×	`associate-*l/_binary64_11615`
99×	`associate-+l+_binary64_11605`
96×	`unswap-sqr_binary64_11640`
90×	`pow-sqr_binary64_11645`
87×	`associate-*r/_binary64_11614`
82×	`cube-div_binary64_11701`
66×	`associate-+r+_binary64_11604`
39×	`distribute-lft-out_binary64_11623`
30×	`*-lft-identity_binary64_11661`
24×	`log-rec_binary64_11760`
18×	`+-commutative_binary64_11602`
16×	`div-exp_binary64_11723` `prod-exp_binary64_11721`
15×	`pow-plus_binary64_11735` `/-rgt-identity_binary64_11663`
13×	`log-pow_binary64_11761` `exp-sqrt_binary64_11725`
11×	`cube-unmult_binary64_11709` `distribute-rgt1-in_binary64_11628`
8×	`exp-lft-sqr_binary64_11727`
7×	`count-2_binary64_11620`
6×	`unpow3_binary64_11738` `*-rgt-identity_binary64_11662`
5×	`cube-mult_binary64_11702`
4×	`rec-exp_binary64_11722` `distribute-lft1-in_binary64_11627`
1×	`unpow2_binary64_11737` `unpow1_binary64_11730` `1-exp_binary64_11716` `rem-sqrt-square_binary64_11685` `neg-mul-1_binary64_11668` `neg-sub0_binary64_11667` `sub-neg_binary64_11665` `--rgt-identity_binary64_11658` `*-inverses_binary64_11652` `rgt-mult-inverse_binary64_11649`
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_11935` `erf-erfc_binary64_11934` `erf-odd_binary64_11933` `if-if-and-not_binary64_11932` `if-if-and_binary64_11931` `if-if-or-not_binary64_11930` `if-if-or_binary64_11929` `if-not_binary64_11928` `if-same_binary64_11927` `if-false_binary64_11926` `if-true_binary64_11925` `not-gte_binary64_11924` `not-lte_binary64_11923` `not-gt_binary64_11922` `not-lt_binary64_11921` `gte-same_binary64_11920` `lte-same_binary64_11919` `gt-same_binary64_11918` `lt-same_binary64_11917` `sinh---cosh_binary64_11864` `sinh-+-cosh_binary64_11863` `sinh-cosh_binary64_11862` `tanh-def-c_binary64_11861` `tanh-def-b_binary64_11860` `tanh-def-a_binary64_11859` `cosh-def_binary64_11858` `sinh-def_binary64_11857` `tan-neg_binary64_11804` `cos-neg_binary64_11803` `sin-neg_binary64_11802` `tan-0_binary64_11801` `cos-0_binary64_11800` `sin-0_binary64_11799` `hang-m-tan_binary64_11798` `hang-p-tan_binary64_11797` `hang-m0-tan_binary64_11796` `hang-p0-tan_binary64_11795` `hang-0m-tan_binary64_11794` `hang-0p-tan_binary64_11793` `tan-+PI/2_binary64_11792` `tan-+PI_binary64_11791` `tan-PI_binary64_11790` `tan-PI/3_binary64_11789` `tan-PI/4_binary64_11788` `tan-PI/6_binary64_11787` `cos-+PI/2_binary64_11786` `cos-+PI_binary64_11785` `cos-PI_binary64_11784` `cos-PI/2_binary64_11783` `cos-PI/3_binary64_11782` `cos-PI/4_binary64_11781` `cos-PI/6_binary64_11780` `sin-+PI/2_binary64_11779` `sin-+PI_binary64_11778` `sin-PI_binary64_11777` `sin-PI/2_binary64_11776` `sin-PI/3_binary64_11775` `sin-PI/4_binary64_11774` `sin-PI/6_binary64_11773` `sub-1-sin_binary64_11772` `sub-1-cos_binary64_11771` `-1-add-sin_binary64_11770` `-1-add-cos_binary64_11769` `1-sub-sin_binary64_11768` `1-sub-cos_binary64_11767` `cos-sin-sum_binary64_11766` `log-E_binary64_11762` `pow-base-0_binary64_11756` `unpow1/3_binary64_11739` `unpow1/2_binary64_11736` `exp-to-pow_binary64_11734` `pow-base-1_binary64_11732` `unpow0_binary64_11731` `unpow-1_binary64_11729` `exp-lft-cube_binary64_11728` `exp-cbrt_binary64_11726` `exp-diff_binary64_11720` `exp-neg_binary64_11719` `exp-sum_binary64_11718` `e-exp-1_binary64_11717` `exp-1-e_binary64_11715` `exp-0_binary64_11714` `rem-log-exp_binary64_11713` `rem-exp-log_binary64_11712` `cube-neg_binary64_11699` `rem-3cbrt-rft_binary64_11698` `rem-3cbrt-lft_binary64_11697` `rem-cbrt-cube_binary64_11696` `rem-cube-cbrt_binary64_11695` `sqr-abs_binary64_11687` `sqr-neg_binary64_11686` `rem-square-sqrt_binary64_11684` `div-sub_binary64_11677` `unsub-neg_binary64_11666` `mul-1-neg_binary64_11664` `remove-double-neg_binary64_11660` `sub0-neg_binary64_11659` `+-rgt-identity_binary64_11657` `+-lft-identity_binary64_11656` `mul0-rgt_binary64_11655` `mul0-lft_binary64_11654` `div0_binary64_11653` `+-inverses_binary64_11651` `lft-mult-inverse_binary64_11650` `remove-double-div_binary64_11648` `difference-of-sqr--1_binary64_11643` `difference-of-sqr-1_binary64_11642` `difference-of-squares_binary64_11641` `cancel-sign-sub-inv_binary64_11638` `cancel-sign-sub_binary64_11637` `distribute-neg-frac_binary64_11636` `distribute-frac-neg_binary64_11635` `distribute-neg-out_binary64_11634` `distribute-neg-in_binary64_11633` `distribute-rgt-neg-out_binary64_11632` `distribute-lft-neg-out_binary64_11631` `distribute-rgt-neg-in_binary64_11630` `distribute-lft-neg-in_binary64_11629` `distribute-rgt-out--_binary64_11626` `distribute-lft-out--_binary64_11624` `associate--r-_binary64_11611` `associate--l-_binary64_11610` `associate--l+_binary64_11609` `associate--r+_binary64_11608` `associate-+l-_binary64_11607` `associate-+r-_binary64_11606`

Counts

27 → 96

Iterations

Useful iterations: 1 (0.0ms)

Iter	Nodes	Cost
0	49	386
1	129	302
2	466	302
3	704	302
4	1189	302
5	2398	302
6	4827	302

prune101.0ms (0.8%)

Pruning

8 alts after pruning (5 fresh and 3 done)

	Pruned	Kept	Total
New	92	4	96
Fresh	1	1	2
Picked	0	1	1
Done	0	2	2
Total	93	8	101

Error

0.0b

Counts

101 → 8

Compiler

Compiled 1789 to 862 computations (51.8% saved)

localize11.0ms (0.1%)

Local error

Found 4 expressions with local error:

0.5b	(*.f64 (cbrt.f64 z) (cbrt.f64 z))
0.6b	(cbrt.f64 z)
0.6b	(cbrt.f64 z)
0.6b	(cbrt.f64 z)

rewrite99.0ms (0.8%)

Algorithm

1×	rewrite-expression-head

Error

0.0b

Rules

25×	`cbrt-prod_binary64_11703`
23×	`add-sqr-sqrt_binary64_11694`
15×	`add-cube-cbrt_binary64_11707` `*-un-lft-identity_binary64_11672`
11×	`pow1_binary64_11733`
9×	`pow1/3_binary64_11754`
6×	`add-exp-log_binary64_11710` `swap-sqr_binary64_11639` `associate-l_binary64_11613` `associate-r_binary64_11612`
4×	`add-log-exp_binary64_11711` `add-cbrt-cube_binary64_11708` `unswap-sqr_binary64_11640`
2×	`pow-prod-down_binary64_11743` `pow-prod-up_binary64_11742` `pow-sqr_binary64_11645`
1×	`pow2_binary64_11753` `pow-plus_binary64_11735` `prod-exp_binary64_11721` `cbrt-unprod_binary64_11705` `*-commutative_binary64_11603`

Counts

4 → 73

Calls

4 calls:

6.0ms	(*.f64 (cbrt.f64 z) (cbrt.f64 z))
1.0ms	(cbrt.f64 z)
1.0ms	(cbrt.f64 z)
1.0ms	(cbrt.f64 z)

Compiler

Compiled 1670 to 601 computations (64% saved)

series533.0ms (4%)

Error

0.0b

Counts

4 → 12

Calls

4 calls:

147.0ms	(*.f64 (cbrt.f64 z) (cbrt.f64 z))
128.0ms	(cbrt.f64 z)
127.0ms	(cbrt.f64 z)
117.0ms	(cbrt.f64 z)

Compiler

Compiled 735 to 541 computations (26.4% saved)

simplify355.0ms (2.7%)

Algorithm

1×	egg-herbie

Rules

545×	`log-prod_binary64_11758`
427×	`log-div_binary64_11759`
416×	`associate-/l*_binary64_11617`
347×	`associate-l_binary64_11613`
293×	`associate-/r*_binary64_11616`
231×	`associate-r_binary64_11612`
203×	`*-commutative_binary64_11603`
184×	`associate-/r/_binary64_11618`
150×	`distribute-rgt-neg-in_binary64_11630`
144×	`distribute-lft-neg-in_binary64_11629`
140×	`exp-prod_binary64_11724`
128×	`distribute-rgt-in_binary64_11622`
123×	`unswap-sqr_binary64_11640`
112×	`cube-prod_binary64_11700`
95×	`distribute-lft-in_binary64_11621`
86×	`swap-sqr_binary64_11639`
80×	`associate-/l/_binary64_11619`
77×	`sqr-pow_binary64_11644`
55×	`log-pow_binary64_11761` `distribute-rgt-out_binary64_11625`
52×	`times-frac_binary64_11678`
47×	`cancel-sign-sub-inv_binary64_11638`
42×	`associate-+l+_binary64_11605`
39×	`associate-+r+_binary64_11604`
38×	`associate-*l/_binary64_11615`
37×	`pow-sqr_binary64_11645`
30×	`distribute-lft-out_binary64_11623`
29×	`cube-div_binary64_11701`
28×	`distribute-neg-frac_binary64_11636`
24×	`log-rec_binary64_11760` `*-rgt-identity_binary64_11662`
23×	`*-lft-identity_binary64_11661`
22×	`pow-plus_binary64_11735`
21×	`associate-*r/_binary64_11614`
19×	`exp-sqrt_binary64_11725`
18×	`rem-sqrt-square_binary64_11685`
15×	`cube-unmult_binary64_11709`
13×	`neg-mul-1_binary64_11668` `neg-sub0_binary64_11667`
12×	`associate-+l-_binary64_11607`
9×	`exp-lft-sqr_binary64_11727` `distribute-rgt-neg-out_binary64_11632` `distribute-lft-neg-out_binary64_11631`
8×	`distribute-rgt1-in_binary64_11628` `count-2_binary64_11620`
6×	`unpow3_binary64_11738` `associate--l-_binary64_11610` `associate--l+_binary64_11609`
5×	`associate-+r-_binary64_11606` `+-commutative_binary64_11602`
4×	`div-exp_binary64_11723` `prod-exp_binary64_11721` `distribute-rgt-out--_binary64_11626`
3×	`unpow1/3_binary64_11739` `unpow2_binary64_11737` `sub-neg_binary64_11665` `distribute-lft-out--_binary64_11624`
2×	`unpow1_binary64_11730` `rec-exp_binary64_11722` `exp-sum_binary64_11718` `cube-mult_binary64_11702` `rem-3cbrt-lft_binary64_11697` `rem-cbrt-cube_binary64_11696` `/-rgt-identity_binary64_11663` `distribute-lft1-in_binary64_11627`
1×	`pow-base-1_binary64_11732` `exp-diff_binary64_11720` `1-exp_binary64_11716` `exp-1-e_binary64_11715` `rem-log-exp_binary64_11713` `rem-3cbrt-rft_binary64_11698` `rem-square-sqrt_binary64_11684` `mul-1-neg_binary64_11664` `mul0-lft_binary64_11654` `*-inverses_binary64_11652` `distribute-neg-out_binary64_11634`
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_11935` `erf-erfc_binary64_11934` `erf-odd_binary64_11933` `if-if-and-not_binary64_11932` `if-if-and_binary64_11931` `if-if-or-not_binary64_11930` `if-if-or_binary64_11929` `if-not_binary64_11928` `if-same_binary64_11927` `if-false_binary64_11926` `if-true_binary64_11925` `not-gte_binary64_11924` `not-lte_binary64_11923` `not-gt_binary64_11922` `not-lt_binary64_11921` `gte-same_binary64_11920` `lte-same_binary64_11919` `gt-same_binary64_11918` `lt-same_binary64_11917` `sinh---cosh_binary64_11864` `sinh-+-cosh_binary64_11863` `sinh-cosh_binary64_11862` `tanh-def-c_binary64_11861` `tanh-def-b_binary64_11860` `tanh-def-a_binary64_11859` `cosh-def_binary64_11858` `sinh-def_binary64_11857` `tan-neg_binary64_11804` `cos-neg_binary64_11803` `sin-neg_binary64_11802` `tan-0_binary64_11801` `cos-0_binary64_11800` `sin-0_binary64_11799` `hang-m-tan_binary64_11798` `hang-p-tan_binary64_11797` `hang-m0-tan_binary64_11796` `hang-p0-tan_binary64_11795` `hang-0m-tan_binary64_11794` `hang-0p-tan_binary64_11793` `tan-+PI/2_binary64_11792` `tan-+PI_binary64_11791` `tan-PI_binary64_11790` `tan-PI/3_binary64_11789` `tan-PI/4_binary64_11788` `tan-PI/6_binary64_11787` `cos-+PI/2_binary64_11786` `cos-+PI_binary64_11785` `cos-PI_binary64_11784` `cos-PI/2_binary64_11783` `cos-PI/3_binary64_11782` `cos-PI/4_binary64_11781` `cos-PI/6_binary64_11780` `sin-+PI/2_binary64_11779` `sin-+PI_binary64_11778` `sin-PI_binary64_11777` `sin-PI/2_binary64_11776` `sin-PI/3_binary64_11775` `sin-PI/4_binary64_11774` `sin-PI/6_binary64_11773` `sub-1-sin_binary64_11772` `sub-1-cos_binary64_11771` `-1-add-sin_binary64_11770` `-1-add-cos_binary64_11769` `1-sub-sin_binary64_11768` `1-sub-cos_binary64_11767` `cos-sin-sum_binary64_11766` `log-E_binary64_11762` `pow-base-0_binary64_11756` `unpow1/2_binary64_11736` `exp-to-pow_binary64_11734` `unpow0_binary64_11731` `unpow-1_binary64_11729` `exp-lft-cube_binary64_11728` `exp-cbrt_binary64_11726` `exp-neg_binary64_11719` `e-exp-1_binary64_11717` `exp-0_binary64_11714` `rem-exp-log_binary64_11712` `cube-neg_binary64_11699` `rem-cube-cbrt_binary64_11695` `sqr-abs_binary64_11687` `sqr-neg_binary64_11686` `div-sub_binary64_11677` `unsub-neg_binary64_11666` `remove-double-neg_binary64_11660` `sub0-neg_binary64_11659` `--rgt-identity_binary64_11658` `+-rgt-identity_binary64_11657` `+-lft-identity_binary64_11656` `mul0-rgt_binary64_11655` `div0_binary64_11653` `+-inverses_binary64_11651` `lft-mult-inverse_binary64_11650` `rgt-mult-inverse_binary64_11649` `remove-double-div_binary64_11648` `difference-of-sqr--1_binary64_11643` `difference-of-sqr-1_binary64_11642` `difference-of-squares_binary64_11641` `cancel-sign-sub_binary64_11637` `distribute-frac-neg_binary64_11635` `distribute-neg-in_binary64_11633` `associate--r-_binary64_11611` `associate--r+_binary64_11608`

Counts

85 → 83

Iterations

Useful iterations: 3 (0.0ms)

Iter	Nodes	Cost
0	55	718
1	97	656
2	345	636
3	1343	633
4	4059	633

prune94.0ms (0.7%)

Pruning

8 alts after pruning (4 fresh and 4 done)

	Pruned	Kept	Total
New	83	0	83
Fresh	0	4	4
Picked	0	1	1
Done	0	3	3
Total	83	8	91

Error

0.0b

Counts

91 → 8

Compiler

Compiled 1911 to 744 computations (61.1% saved)

regimes1.5s (11.4%)

Accuracy

Total 0.2b remaining (92.5%)

Threshold costs 0.2b (92.5%)

Compiler

Compiled 11669 to 8843 computations (24.2% saved)

bsearch68.0ms (0.5%)

Steps

Iters	Range		Point
7	4.303874232271115e+139	5.6102373350381264e+141	5.023950248753564e+141
8	-2.824106208069882e+109	-2.820556740478204e+106	-3.855894969108078e+108

Compiler

Compiled 1 to 4 computations (-300% saved)

simplify20.0ms (0.2%)

Algorithm

1×	egg-herbie

Rules

98×	`neg-mul-1_binary64_11668` `neg-sub0_binary64_11667`
73×	`unsub-neg_binary64_11666`
59×	`distribute-neg-out_binary64_11634`
47×	`distribute-rgt-neg-out_binary64_11632`
41×	`distribute-rgt-neg-in_binary64_11630`
36×	`distribute-lft-neg-out_binary64_11631`
24×	`remove-double-neg_binary64_11660`
21×	`distribute-lft-neg-in_binary64_11629`
17×	`sub-neg_binary64_11665`
15×	`*-commutative_binary64_11603`
14×	`+-commutative_binary64_11602`
10×	`cancel-sign-sub-inv_binary64_11638`
9×	`+-rgt-identity_binary64_11657` `+-lft-identity_binary64_11656`
6×	`distribute-neg-in_binary64_11633`
1×	`if-if-or-not_binary64_11930` `sqr-neg_binary64_11686` `--rgt-identity_binary64_11658`
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_11932` `if-if-and_binary64_11931` `if-if-or_binary64_11929` `if-not_binary64_11928` `if-same_binary64_11927` `if-false_binary64_11926` `if-true_binary64_11925` `tan-0_binary64_11801` `cos-0_binary64_11800` `sin-0_binary64_11799` `unpow1_binary64_11730` `e-exp-1_binary64_11717` `1-exp_binary64_11716` `exp-1-e_binary64_11715` `exp-0_binary64_11714` `sqr-abs_binary64_11687` `mul-1-neg_binary64_11664` `/-rgt-identity_binary64_11663` `-rgt-identity_binary64_11662` `-lft-identity_binary64_11661` `sub0-neg_binary64_11659` `cancel-sign-sub_binary64_11637` `distribute-neg-frac_binary64_11636` `distribute-frac-neg_binary64_11635`

Iterations

Useful iterations: 0 (0.0ms)

Iter	Nodes	Cost
0	22	49
1	41	49
2	68	49
3	94	49
4	121	49
5	141	49
6	144	49
7	230	49
8	338	49
9	270	49

Proof

(=> (if real (<= f64 h0 -3855894969108077847881864253420004636647840727621100301181179175196200484088133642263662612961966660220092416) (- f64 (* f64 h1 h1) (* f64 h0 (* f64 h0 (* f64 h2 4)))) (if real (<= f64 h0 5023950248753564293974536098360929411551944926746739379058661416107802157820118820411716841524460987362598166551644156808605387237916149809152) (- f64 (* f64 h1 h1) (* f64 (* f64 h2 4) (- f64 (* f64 h0 h0) h3))) (- f64 (* f64 h1 h1) (* f64 h0 (* f64 h0 (* f64 h2 4)))))))
if-if-or-not_binary64_11930 =>
(if real (or real (<= f64 h0 -3855894969108077847881864253420004636647840727621100301181179175196200484088133642263662612961966660220092416) (not real (<= f64 h0 5023950248753564293974536098360929411551944926746739379058661416107802157820118820411716841524460987362598166551644156808605387237916149809152))) (- f64 (* f64 h1 h1) (* f64 h0 (* f64 h0 (* f64 h2 4)))) (=> (- f64 (* f64 h1 h1) (* f64 (* f64 h2 4) (- f64 (* f64 h0 h0) h3)))))
sub-neg_binary64_11665 =>
(if real (or real (<= f64 h0 -3855894969108077847881864253420004636647840727621100301181179175196200484088133642263662612961966660220092416) (not real (<= f64 h0 5023950248753564293974536098360929411551944926746739379058661416107802157820118820411716841524460987362598166551644156808605387237916149809152))) (- f64 (* f64 h1 h1) (* f64 h0 (* f64 h0 (* f64 h2 4)))) (+ f64 (* f64 h1 h1) (=> (neg f64 (* f64 (* f64 h2 4) (- f64 (* f64 h0 h0) h3))))))
distribute-rgt-neg-in_binary64_11630 =>
(if real (or real (<= f64 h0 -3855894969108077847881864253420004636647840727621100301181179175196200484088133642263662612961966660220092416) (not real (<= f64 h0 5023950248753564293974536098360929411551944926746739379058661416107802157820118820411716841524460987362598166551644156808605387237916149809152))) (- f64 (* f64 h1 h1) (* f64 h0 (* f64 h0 (* f64 h2 4)))) (+ f64 (* f64 h1 h1) (* f64 (* f64 h2 4) (neg f64 (=> (- f64 (* f64 h0 h0) h3))))))
sub-neg_binary64_11665 =>
(if real (or real (<= f64 h0 -3855894969108077847881864253420004636647840727621100301181179175196200484088133642263662612961966660220092416) (not real (<= f64 h0 5023950248753564293974536098360929411551944926746739379058661416107802157820118820411716841524460987362598166551644156808605387237916149809152))) (- f64 (* f64 h1 h1) (* f64 h0 (* f64 h0 (* f64 h2 4)))) (+ f64 (* f64 h1 h1) (* f64 (* f64 h2 4) (neg f64 (=> (+ f64 (* f64 h0 h0) (neg f64 h3)))))))
+-commutative_binary64_11602 =>
(if real (or real (<= f64 h0 -3855894969108077847881864253420004636647840727621100301181179175196200484088133642263662612961966660220092416) (not real (<= f64 h0 5023950248753564293974536098360929411551944926746739379058661416107802157820118820411716841524460987362598166551644156808605387237916149809152))) (- f64 (* f64 h1 h1) (* f64 h0 (* f64 h0 (* f64 h2 4)))) (+ f64 (* f64 h1 h1) (* f64 (* f64 h2 4) (=> (neg f64 (+ f64 (neg f64 h3) (* f64 h0 h0)))))))
distribute-neg-in_binary64_11633 =>
(if real (or real (<= f64 h0 -3855894969108077847881864253420004636647840727621100301181179175196200484088133642263662612961966660220092416) (not real (<= f64 h0 5023950248753564293974536098360929411551944926746739379058661416107802157820118820411716841524460987362598166551644156808605387237916149809152))) (- f64 (* f64 h1 h1) (* f64 h0 (* f64 h0 (* f64 h2 4)))) (+ f64 (* f64 h1 h1) (* f64 (* f64 h2 4) (=> (+ f64 (neg f64 (neg f64 h3)) (neg f64 (* f64 h0 h0)))))))
unsub-neg_binary64_11666 =>
(if real (or real (<= f64 h0 -3855894969108077847881864253420004636647840727621100301181179175196200484088133642263662612961966660220092416) (not real (<= f64 h0 5023950248753564293974536098360929411551944926746739379058661416107802157820118820411716841524460987362598166551644156808605387237916149809152))) (- f64 (* f64 h1 h1) (* f64 h0 (* f64 h0 (* f64 h2 4)))) (+ f64 (* f64 h1 h1) (* f64 (* f64 h2 4) (- f64 (=> (neg f64 (neg f64 h3))) (* f64 h0 h0)))))
remove-double-neg_binary64_11660 =>
(if real (or real (<= f64 h0 -3855894969108077847881864253420004636647840727621100301181179175196200484088133642263662612961966660220092416) (not real (<= f64 h0 5023950248753564293974536098360929411551944926746739379058661416107802157820118820411716841524460987362598166551644156808605387237916149809152))) (- f64 (* f64 h1 h1) (* f64 h0 (* f64 h0 (* f64 h2 4)))) (+ f64 (* f64 h1 h1) (* f64 (* f64 h2 4) (- f64 h3 (* f64 h0 h0)))))

end0.0ms (0%)

sample1.8s (13.8%)

Algorithm

1×

intervals

Results

311.0ms	8000×	body	128	valid
106.0ms	2889×	body	128	invalid

Compiler

Compiled 1107 to 842 computations (23.9% saved)

Details

analyze877.0ms (6.7%)

sample28.0ms (0.2%)

simplify970.0ms (7.4%)

prune5.0ms (0%)

localize13.0ms (0.1%)

rewrite99.0ms (0.7%)

series1.0s (7.7%)

simplify376.0ms (2.9%)

prune427.0ms (3.2%)

localize19.0ms (0.1%)

rewrite261.0ms (2%)

series1.6s (12.4%)

simplify525.0ms (4%)

prune1.9s (14.6%)

localize7.0ms (0.1%)

rewrite31.0ms (0.2%)

series130.0ms (1%)

simplify226.0ms (1.7%)

prune101.0ms (0.8%)

localize11.0ms (0.1%)

rewrite99.0ms (0.8%)

series533.0ms (4%)

simplify355.0ms (2.7%)

prune94.0ms (0.7%)

regimes1.5s (11.4%)

bsearch68.0ms (0.5%)

simplify20.0ms (0.2%)

end0.0ms (0%)

sample1.8s (13.8%)

Profiling