Details

analyze2.0s (8.3%)

Algorithm

1×

Search

True	Other	False	Iter
0%	99.6%	0.4%	0
0%	99.6%	0.4%	1
0%	99.6%	0.4%	2
0%	99.6%	0.4%	3
0%	99.6%	0.4%	4
0%	99.6%	0.4%	5
0%	99.6%	0.4%	6
0%	99.6%	0.4%	7
0%	99.6%	0.4%	8
0%	99.6%	0.4%	9
0%	99.6%	0.4%	10
0%	99.6%	0.4%	11
0%	99.6%	0.4%	12
0%	99.6%	0.4%	13
0%	99.6%	0.4%	14

Compiler

Compiled 30 to 24 computations (20% saved)

sample94.0ms (0.4%)

Algorithm

1×

intervals

Results

27.0ms	381×	body	128	invalid
23.0ms	256×	body	128	valid

Compiler

Compiled 59 to 56 computations (5.1% saved)

simplify601.0ms (2.5%)

Algorithm

1×	egg-herbie

Rules

674×	`swap-sqr_binary64_10616`
600×	`distribute-rgt-out--_binary64_10603`
598×	`unsub-neg_binary64_10643`
355×	`sub-neg_binary64_10642`
268×	`cancel-sign-sub-inv_binary64_10615`
266×	`+-commutative_binary64_10579`
224×	`associate-+l+_binary64_10582`
210×	`neg-mul-1_binary64_10645`
199×	`neg-sub0_binary64_10644`
169×	`associate--r+_binary64_10585`
165×	`associate-+l-_binary64_10584`
155×	`associate--l+_binary64_10586`
152×	`distribute-rgt-neg-in_binary64_10607`
147×	`distribute-neg-in_binary64_10610`
142×	`distribute-rgt-in_binary64_10599` `associate-r_binary64_10589`
139×	`associate-l_binary64_10590`
137×	`distribute-neg-out_binary64_10611`
118×	`distribute-rgt-neg-out_binary64_10609`
112×	`*-commutative_binary64_10580`
111×	`distribute-lft-neg-in_binary64_10606`
99×	`associate-+r-_binary64_10583`
94×	`distribute-lft-neg-out_binary64_10608`
90×	`remove-double-neg_binary64_10637`
86×	`associate--r-_binary64_10588`
75×	`distribute-lft-in_binary64_10598`
61×	`associate-+r+_binary64_10581`
57×	`sub0-neg_binary64_10636`
55×	`associate--l-_binary64_10587`
36×	`--rgt-identity_binary64_10635` `distribute-rgt1-in_binary64_10605`
35×	`mul0-rgt_binary64_10632` `mul0-lft_binary64_10631`
29×	`+-rgt-identity_binary64_10634`
27×	`distribute-rgt-out_binary64_10602`
23×	`+-inverses_binary64_10628`
16×	`sqr-neg_binary64_10663`
9×	`distribute-lft-out_binary64_10600`
8×	`cancel-sign-sub_binary64_10614`
7×	`difference-of-squares_binary64_10618`
6×	`+-lft-identity_binary64_10633`
5×	`mul-1-neg_binary64_10641`
4×	`distribute-lft1-in_binary64_10604`
3×	`cube-unmult_binary64_10686`
1×	`pow-plus_binary64_10712` `1-exp_binary64_10693` `pow-sqr_binary64_10622` `sqr-pow_binary64_10621` `distribute-lft-out--_binary64_10601` `count-2_binary64_10597`
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_10912` `erf-erfc_binary64_10911` `erf-odd_binary64_10910` `if-if-and-not_binary64_10909` `if-if-and_binary64_10908` `if-if-or-not_binary64_10907` `if-if-or_binary64_10906` `if-not_binary64_10905` `if-same_binary64_10904` `if-false_binary64_10903` `if-true_binary64_10902` `not-gte_binary64_10901` `not-lte_binary64_10900` `not-gt_binary64_10899` `not-lt_binary64_10898` `gte-same_binary64_10897` `lte-same_binary64_10896` `gt-same_binary64_10895` `lt-same_binary64_10894` `sinh---cosh_binary64_10841` `sinh-+-cosh_binary64_10840` `sinh-cosh_binary64_10839` `tanh-def-c_binary64_10838` `tanh-def-b_binary64_10837` `tanh-def-a_binary64_10836` `cosh-def_binary64_10835` `sinh-def_binary64_10834` `tan-neg_binary64_10781` `cos-neg_binary64_10780` `sin-neg_binary64_10779` `tan-0_binary64_10778` `cos-0_binary64_10777` `sin-0_binary64_10776` `hang-m-tan_binary64_10775` `hang-p-tan_binary64_10774` `hang-m0-tan_binary64_10773` `hang-p0-tan_binary64_10772` `hang-0m-tan_binary64_10771` `hang-0p-tan_binary64_10770` `tan-+PI/2_binary64_10769` `tan-+PI_binary64_10768` `tan-PI_binary64_10767` `tan-PI/3_binary64_10766` `tan-PI/4_binary64_10765` `tan-PI/6_binary64_10764` `cos-+PI/2_binary64_10763` `cos-+PI_binary64_10762` `cos-PI_binary64_10761` `cos-PI/2_binary64_10760` `cos-PI/3_binary64_10759` `cos-PI/4_binary64_10758` `cos-PI/6_binary64_10757` `sin-+PI/2_binary64_10756` `sin-+PI_binary64_10755` `sin-PI_binary64_10754` `sin-PI/2_binary64_10753` `sin-PI/3_binary64_10752` `sin-PI/4_binary64_10751` `sin-PI/6_binary64_10750` `sub-1-sin_binary64_10749` `sub-1-cos_binary64_10748` `-1-add-sin_binary64_10747` `-1-add-cos_binary64_10746` `1-sub-sin_binary64_10745` `1-sub-cos_binary64_10744` `cos-sin-sum_binary64_10743` `log-E_binary64_10739` `log-pow_binary64_10738` `log-rec_binary64_10737` `log-div_binary64_10736` `log-prod_binary64_10735` `pow-base-0_binary64_10733` `unpow1/3_binary64_10716` `unpow3_binary64_10715` `unpow2_binary64_10714` `unpow1/2_binary64_10713` `exp-to-pow_binary64_10711` `pow-base-1_binary64_10709` `unpow0_binary64_10708` `unpow1_binary64_10707` `unpow-1_binary64_10706` `exp-lft-cube_binary64_10705` `exp-lft-sqr_binary64_10704` `exp-cbrt_binary64_10703` `exp-sqrt_binary64_10702` `exp-prod_binary64_10701` `div-exp_binary64_10700` `rec-exp_binary64_10699` `prod-exp_binary64_10698` `exp-diff_binary64_10697` `exp-neg_binary64_10696` `exp-sum_binary64_10695` `e-exp-1_binary64_10694` `exp-1-e_binary64_10692` `exp-0_binary64_10691` `rem-log-exp_binary64_10690` `rem-exp-log_binary64_10689` `cube-mult_binary64_10679` `cube-div_binary64_10678` `cube-prod_binary64_10677` `cube-neg_binary64_10676` `rem-3cbrt-rft_binary64_10675` `rem-3cbrt-lft_binary64_10674` `rem-cbrt-cube_binary64_10673` `rem-cube-cbrt_binary64_10672` `sqr-abs_binary64_10664` `rem-sqrt-square_binary64_10662` `rem-square-sqrt_binary64_10661` `times-frac_binary64_10655` `div-sub_binary64_10654` `/-rgt-identity_binary64_10640` `-rgt-identity_binary64_10639` `-lft-identity_binary64_10638` `div0_binary64_10630` `-inverses_binary64_10629` `lft-mult-inverse_binary64_10627` `rgt-mult-inverse_binary64_10626` `remove-double-div_binary64_10625` `difference-of-sqr--1_binary64_10620` `difference-of-sqr-1_binary64_10619` `unswap-sqr_binary64_10617` `distribute-neg-frac_binary64_10613` `distribute-frac-neg_binary64_10612` `associate-/l/_binary64_10596` `associate-/r/_binary64_10595` `associate-/l_binary64_10594` `associate-/r_binary64_10593` `associate-l/_binary64_10592` `associate-*r/_binary64_10591`

Counts

1 → 4

Iterations

Useful iterations: 0 (0.0ms)

Iter	Nodes	Cost
0	24	43
1	55	43
2	125	43
3	407	43
4	1015	43
5	2401	43
6	3925	43

prune10.0ms (0%)

Pruning

2 alts after pruning (2 fresh and 0 done)

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

Error

2.1b

Counts

5 → 2

Compiler

Compiled 174 to 89 computations (48.9% saved)

localize25.0ms (0.1%)

Local error

Found 4 expressions with local error:

0.0b	(-.f64 (.f64 c z) (.f64 i a))
4.1b	(.f64 b (-.f64 (.f64 c z) (*.f64 i a)))
4.9b	(.f64 x (-.f64 (.f64 y z) (*.f64 t a)))
5.1b	(.f64 j (-.f64 (.f64 c t) (*.f64 i y)))

rewrite161.0ms (0.7%)

Algorithm

1×	rewrite-expression-head

Error

2.1b

Rules

16×	`add-sqr-sqrt_binary64_10671`
10×	`pow1_binary64_10710` `add-exp-log_binary64_10687` `add-cbrt-cube_binary64_10685` `add-cube-cbrt_binary64_10684` `*-un-lft-identity_binary64_10649`
9×	`associate-l_binary64_10590` `associate-r_binary64_10589`
7×	`sub-neg_binary64_10642` `cancel-sign-sub-inv_binary64_10615`
6×	`add-log-exp_binary64_10688` `distribute-rgt-in_binary64_10599` `distribute-lft-in_binary64_10598` `associate-*r/_binary64_10591`
4×	`flip3--_binary64_10653` `flip--_binary64_10624`
3×	`pow-prod-down_binary64_10720` `prod-exp_binary64_10698` `cbrt-unprod_binary64_10682` `unswap-sqr_binary64_10617` `*-commutative_binary64_10580`
1×	`diff-log_binary64_10741`

Counts

4 → 84

Calls

4 calls:

7.0ms	(.f64 j (-.f64 (.f64 c t) (*.f64 i y)))
6.0ms	(.f64 x (-.f64 (.f64 y z) (*.f64 t a)))
6.0ms	(.f64 b (-.f64 (.f64 c z) (*.f64 i a)))
4.0ms	(-.f64 (.f64 c z) (.f64 i a))

Compiler

Compiled 3151 to 437 computations (86.1% saved)

series1.7s (7%)

Error

0.1b

Counts

4 → 105

Calls

4 calls:

444.0ms	(.f64 x (-.f64 (.f64 y z) (*.f64 t a)))
430.0ms	(.f64 b (-.f64 (.f64 c z) (*.f64 i a)))
424.0ms	(.f64 j (-.f64 (.f64 c t) (*.f64 i y)))
260.0ms	(-.f64 (.f64 c z) (.f64 i a))

Compiler

Compiled 7671 to 3922 computations (48.9% saved)

simplify273.0ms (1.1%)

Algorithm

1×	egg-herbie

Rules

371×	`distribute-rgt-in_binary64_10599`
365×	`distribute-lft-in_binary64_10598`
292×	`cancel-sign-sub-inv_binary64_10615`
290×	`associate-l_binary64_10590`
255×	`associate-r_binary64_10589`
211×	`exp-prod_binary64_10701`
152×	`unsub-neg_binary64_10643`
141×	`distribute-rgt-neg-in_binary64_10607`
139×	`sqr-pow_binary64_10621`
138×	`neg-sub0_binary64_10644`
135×	`neg-mul-1_binary64_10645`
119×	`distribute-lft-neg-in_binary64_10606`
111×	`*-lft-identity_binary64_10638`
108×	`*-rgt-identity_binary64_10639` `difference-of-squares_binary64_10618`
103×	`sub-neg_binary64_10642`
100×	`*-commutative_binary64_10580`
78×	`unswap-sqr_binary64_10617`
72×	`pow-sqr_binary64_10622`
67×	`swap-sqr_binary64_10616`
63×	`cube-prod_binary64_10677`
60×	`exp-sum_binary64_10695`
52×	`distribute-lft-neg-out_binary64_10608`
35×	`mul0-rgt_binary64_10632` `mul0-lft_binary64_10631` `distribute-rgt-neg-out_binary64_10609`
34×	`log-prod_binary64_10735`
32×	`+-commutative_binary64_10579`
25×	`exp-diff_binary64_10697`
18×	`distribute-rgt-out_binary64_10602`
17×	`associate-+r-_binary64_10583`
13×	`unpow3_binary64_10715` `associate-+r+_binary64_10581`
12×	`cube-mult_binary64_10679` `div-sub_binary64_10654` `sub0-neg_binary64_10636` `+-rgt-identity_binary64_10634` `associate-+l-_binary64_10584`
11×	`times-frac_binary64_10655` `associate-+l+_binary64_10582`
9×	`cube-unmult_binary64_10686`
8×	`distribute-lft-out_binary64_10600`
6×	`mul-1-neg_binary64_10641`
3×	`sqr-neg_binary64_10663`
2×	`distribute-rgt-out--_binary64_10603`
1×	`div-exp_binary64_10700` `prod-exp_binary64_10698` `1-exp_binary64_10693` `exp-1-e_binary64_10692` `rem-log-exp_binary64_10690` `associate-/l/_binary64_10596` `associate-/l_binary64_10594` `associate-/r_binary64_10593` `associate-*r/_binary64_10591`
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_10912` `erf-erfc_binary64_10911` `erf-odd_binary64_10910` `if-if-and-not_binary64_10909` `if-if-and_binary64_10908` `if-if-or-not_binary64_10907` `if-if-or_binary64_10906` `if-not_binary64_10905` `if-same_binary64_10904` `if-false_binary64_10903` `if-true_binary64_10902` `not-gte_binary64_10901` `not-lte_binary64_10900` `not-gt_binary64_10899` `not-lt_binary64_10898` `gte-same_binary64_10897` `lte-same_binary64_10896` `gt-same_binary64_10895` `lt-same_binary64_10894` `sinh---cosh_binary64_10841` `sinh-+-cosh_binary64_10840` `sinh-cosh_binary64_10839` `tanh-def-c_binary64_10838` `tanh-def-b_binary64_10837` `tanh-def-a_binary64_10836` `cosh-def_binary64_10835` `sinh-def_binary64_10834` `tan-neg_binary64_10781` `cos-neg_binary64_10780` `sin-neg_binary64_10779` `tan-0_binary64_10778` `cos-0_binary64_10777` `sin-0_binary64_10776` `hang-m-tan_binary64_10775` `hang-p-tan_binary64_10774` `hang-m0-tan_binary64_10773` `hang-p0-tan_binary64_10772` `hang-0m-tan_binary64_10771` `hang-0p-tan_binary64_10770` `tan-+PI/2_binary64_10769` `tan-+PI_binary64_10768` `tan-PI_binary64_10767` `tan-PI/3_binary64_10766` `tan-PI/4_binary64_10765` `tan-PI/6_binary64_10764` `cos-+PI/2_binary64_10763` `cos-+PI_binary64_10762` `cos-PI_binary64_10761` `cos-PI/2_binary64_10760` `cos-PI/3_binary64_10759` `cos-PI/4_binary64_10758` `cos-PI/6_binary64_10757` `sin-+PI/2_binary64_10756` `sin-+PI_binary64_10755` `sin-PI_binary64_10754` `sin-PI/2_binary64_10753` `sin-PI/3_binary64_10752` `sin-PI/4_binary64_10751` `sin-PI/6_binary64_10750` `sub-1-sin_binary64_10749` `sub-1-cos_binary64_10748` `-1-add-sin_binary64_10747` `-1-add-cos_binary64_10746` `1-sub-sin_binary64_10745` `1-sub-cos_binary64_10744` `cos-sin-sum_binary64_10743` `log-E_binary64_10739` `log-pow_binary64_10738` `log-rec_binary64_10737` `log-div_binary64_10736` `pow-base-0_binary64_10733` `unpow1/3_binary64_10716` `unpow2_binary64_10714` `unpow1/2_binary64_10713` `pow-plus_binary64_10712` `exp-to-pow_binary64_10711` `pow-base-1_binary64_10709` `unpow0_binary64_10708` `unpow1_binary64_10707` `unpow-1_binary64_10706` `exp-lft-cube_binary64_10705` `exp-lft-sqr_binary64_10704` `exp-cbrt_binary64_10703` `exp-sqrt_binary64_10702` `rec-exp_binary64_10699` `exp-neg_binary64_10696` `e-exp-1_binary64_10694` `exp-0_binary64_10691` `rem-exp-log_binary64_10689` `cube-div_binary64_10678` `cube-neg_binary64_10676` `rem-3cbrt-rft_binary64_10675` `rem-3cbrt-lft_binary64_10674` `rem-cbrt-cube_binary64_10673` `rem-cube-cbrt_binary64_10672` `sqr-abs_binary64_10664` `rem-sqrt-square_binary64_10662` `rem-square-sqrt_binary64_10661` `/-rgt-identity_binary64_10640` `remove-double-neg_binary64_10637` `--rgt-identity_binary64_10635` `+-lft-identity_binary64_10633` `div0_binary64_10630` `-inverses_binary64_10629` `+-inverses_binary64_10628` `lft-mult-inverse_binary64_10627` `rgt-mult-inverse_binary64_10626` `remove-double-div_binary64_10625` `difference-of-sqr--1_binary64_10620` `difference-of-sqr-1_binary64_10619` `cancel-sign-sub_binary64_10614` `distribute-neg-frac_binary64_10613` `distribute-frac-neg_binary64_10612` `distribute-neg-out_binary64_10611` `distribute-neg-in_binary64_10610` `distribute-rgt1-in_binary64_10605` `distribute-lft1-in_binary64_10604` `distribute-lft-out--_binary64_10601` `count-2_binary64_10597` `associate-/r/_binary64_10595` `associate-l/_binary64_10592` `associate--r-_binary64_10588` `associate--l-_binary64_10587` `associate--l+_binary64_10586` `associate--r+_binary64_10585`

Counts

189 → 339

Iterations

Useful iterations: 1 (0.0ms)

Iter	Nodes	Cost
0	197	2626
1	476	2443
2	1565	2443
3	3675	2443

prune605.0ms (2.5%)

Pruning

10 alts after pruning (10 fresh and 0 done)

	Pruned	Kept	Total
New	330	9	339
Fresh	0	1	1
Picked	1	0	1
Done	0	0	0
Total	331	10	341

Error

0.1b

Counts

341 → 10

Compiler

Compiled 11013 to 846 computations (92.3% saved)

localize21.0ms (0.1%)

Local error

Found 4 expressions with local error:

0.3b	(-.f64 (.f64 x z) (.f64 i j))
3.0b	(.f64 c (-.f64 (.f64 z b) (*.f64 t j)))
5.6b	(.f64 a (-.f64 (.f64 b i) (*.f64 x t)))
5.7b	(.f64 y (-.f64 (.f64 x z) (*.f64 i j)))

rewrite148.0ms (0.6%)

Algorithm

1×	rewrite-expression-head

Error

0.0b

Rules

16×	`add-sqr-sqrt_binary64_10671`
10×	`pow1_binary64_10710` `add-exp-log_binary64_10687` `add-cbrt-cube_binary64_10685` `add-cube-cbrt_binary64_10684` `*-un-lft-identity_binary64_10649`
9×	`associate-l_binary64_10590` `associate-r_binary64_10589`
7×	`sub-neg_binary64_10642` `cancel-sign-sub-inv_binary64_10615`
6×	`add-log-exp_binary64_10688` `distribute-rgt-in_binary64_10599` `distribute-lft-in_binary64_10598` `associate-*r/_binary64_10591`
4×	`flip3--_binary64_10653` `flip--_binary64_10624`
3×	`pow-prod-down_binary64_10720` `prod-exp_binary64_10698` `cbrt-unprod_binary64_10682` `unswap-sqr_binary64_10617` `*-commutative_binary64_10580`
1×	`diff-log_binary64_10741`

Counts

4 → 84

Calls

4 calls:

7.0ms	(.f64 c (-.f64 (.f64 z b) (*.f64 t j)))
6.0ms	(.f64 a (-.f64 (.f64 b i) (*.f64 x t)))
6.0ms	(.f64 y (-.f64 (.f64 x z) (*.f64 i j)))
4.0ms	(-.f64 (.f64 x z) (.f64 i j))

Compiler

Compiled 3151 to 426 computations (86.5% saved)

series1.6s (6.6%)

Error

0.0b

Counts

4 → 105

Calls

4 calls:

430.0ms	(.f64 y (-.f64 (.f64 x z) (*.f64 i j)))
417.0ms	(.f64 c (-.f64 (.f64 z b) (*.f64 t j)))
383.0ms	(.f64 a (-.f64 (.f64 b i) (*.f64 x t)))
254.0ms	(-.f64 (.f64 x z) (.f64 i j))

Compiler

Compiled 7671 to 3901 computations (49.1% saved)

simplify236.0ms (1%)

Algorithm

1×	egg-herbie

Rules

407×	`distribute-rgt-in_binary64_10599`
401×	`distribute-lft-in_binary64_10598`
291×	`associate-l_binary64_10590`
241×	`associate-r_binary64_10589`
240×	`exp-prod_binary64_10701`
172×	`sqr-pow_binary64_10621`
168×	`unsub-neg_binary64_10643`
146×	`cancel-sign-sub-inv_binary64_10615`
145×	`neg-sub0_binary64_10644`
142×	`neg-mul-1_binary64_10645`
133×	`distribute-rgt-neg-in_binary64_10607`
121×	`*-lft-identity_binary64_10638`
117×	`*-rgt-identity_binary64_10639`
108×	`difference-of-squares_binary64_10618` `distribute-lft-neg-in_binary64_10606`
101×	`sub-neg_binary64_10642`
100×	`*-commutative_binary64_10580`
91×	`swap-sqr_binary64_10616`
78×	`unswap-sqr_binary64_10617`
72×	`pow-sqr_binary64_10622`
71×	`exp-sum_binary64_10695`
61×	`cube-prod_binary64_10677`
58×	`distribute-lft-neg-out_binary64_10608`
39×	`distribute-rgt-neg-out_binary64_10609`
38×	`mul0-rgt_binary64_10632` `mul0-lft_binary64_10631`
34×	`log-prod_binary64_10735` `+-commutative_binary64_10579`
29×	`exp-diff_binary64_10697`
18×	`associate-+r-_binary64_10583`
17×	`distribute-rgt-out_binary64_10602`
14×	`associate-+r+_binary64_10581`
13×	`unpow3_binary64_10715`
12×	`cube-mult_binary64_10679` `div-sub_binary64_10654` `sub0-neg_binary64_10636` `+-rgt-identity_binary64_10634` `associate-+l-_binary64_10584`
11×	`times-frac_binary64_10655` `associate-+l+_binary64_10582`
9×	`cube-unmult_binary64_10686`
8×	`distribute-lft-out_binary64_10600`
4×	`sqr-neg_binary64_10663`
3×	`mul-1-neg_binary64_10641`
2×	`distribute-rgt-out--_binary64_10603`
1×	`div-exp_binary64_10700` `prod-exp_binary64_10698` `exp-neg_binary64_10696` `1-exp_binary64_10693` `exp-1-e_binary64_10692` `rem-log-exp_binary64_10690` `distribute-lft-out--_binary64_10601` `associate-/l/_binary64_10596` `associate-/l_binary64_10594` `associate-/r_binary64_10593` `associate-*r/_binary64_10591`
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_10912` `erf-erfc_binary64_10911` `erf-odd_binary64_10910` `if-if-and-not_binary64_10909` `if-if-and_binary64_10908` `if-if-or-not_binary64_10907` `if-if-or_binary64_10906` `if-not_binary64_10905` `if-same_binary64_10904` `if-false_binary64_10903` `if-true_binary64_10902` `not-gte_binary64_10901` `not-lte_binary64_10900` `not-gt_binary64_10899` `not-lt_binary64_10898` `gte-same_binary64_10897` `lte-same_binary64_10896` `gt-same_binary64_10895` `lt-same_binary64_10894` `sinh---cosh_binary64_10841` `sinh-+-cosh_binary64_10840` `sinh-cosh_binary64_10839` `tanh-def-c_binary64_10838` `tanh-def-b_binary64_10837` `tanh-def-a_binary64_10836` `cosh-def_binary64_10835` `sinh-def_binary64_10834` `tan-neg_binary64_10781` `cos-neg_binary64_10780` `sin-neg_binary64_10779` `tan-0_binary64_10778` `cos-0_binary64_10777` `sin-0_binary64_10776` `hang-m-tan_binary64_10775` `hang-p-tan_binary64_10774` `hang-m0-tan_binary64_10773` `hang-p0-tan_binary64_10772` `hang-0m-tan_binary64_10771` `hang-0p-tan_binary64_10770` `tan-+PI/2_binary64_10769` `tan-+PI_binary64_10768` `tan-PI_binary64_10767` `tan-PI/3_binary64_10766` `tan-PI/4_binary64_10765` `tan-PI/6_binary64_10764` `cos-+PI/2_binary64_10763` `cos-+PI_binary64_10762` `cos-PI_binary64_10761` `cos-PI/2_binary64_10760` `cos-PI/3_binary64_10759` `cos-PI/4_binary64_10758` `cos-PI/6_binary64_10757` `sin-+PI/2_binary64_10756` `sin-+PI_binary64_10755` `sin-PI_binary64_10754` `sin-PI/2_binary64_10753` `sin-PI/3_binary64_10752` `sin-PI/4_binary64_10751` `sin-PI/6_binary64_10750` `sub-1-sin_binary64_10749` `sub-1-cos_binary64_10748` `-1-add-sin_binary64_10747` `-1-add-cos_binary64_10746` `1-sub-sin_binary64_10745` `1-sub-cos_binary64_10744` `cos-sin-sum_binary64_10743` `log-E_binary64_10739` `log-pow_binary64_10738` `log-rec_binary64_10737` `log-div_binary64_10736` `pow-base-0_binary64_10733` `unpow1/3_binary64_10716` `unpow2_binary64_10714` `unpow1/2_binary64_10713` `pow-plus_binary64_10712` `exp-to-pow_binary64_10711` `pow-base-1_binary64_10709` `unpow0_binary64_10708` `unpow1_binary64_10707` `unpow-1_binary64_10706` `exp-lft-cube_binary64_10705` `exp-lft-sqr_binary64_10704` `exp-cbrt_binary64_10703` `exp-sqrt_binary64_10702` `rec-exp_binary64_10699` `e-exp-1_binary64_10694` `exp-0_binary64_10691` `rem-exp-log_binary64_10689` `cube-div_binary64_10678` `cube-neg_binary64_10676` `rem-3cbrt-rft_binary64_10675` `rem-3cbrt-lft_binary64_10674` `rem-cbrt-cube_binary64_10673` `rem-cube-cbrt_binary64_10672` `sqr-abs_binary64_10664` `rem-sqrt-square_binary64_10662` `rem-square-sqrt_binary64_10661` `/-rgt-identity_binary64_10640` `remove-double-neg_binary64_10637` `--rgt-identity_binary64_10635` `+-lft-identity_binary64_10633` `div0_binary64_10630` `-inverses_binary64_10629` `+-inverses_binary64_10628` `lft-mult-inverse_binary64_10627` `rgt-mult-inverse_binary64_10626` `remove-double-div_binary64_10625` `difference-of-sqr--1_binary64_10620` `difference-of-sqr-1_binary64_10619` `cancel-sign-sub_binary64_10614` `distribute-neg-frac_binary64_10613` `distribute-frac-neg_binary64_10612` `distribute-neg-out_binary64_10611` `distribute-neg-in_binary64_10610` `distribute-rgt1-in_binary64_10605` `distribute-lft1-in_binary64_10604` `count-2_binary64_10597` `associate-/r/_binary64_10595` `associate-l/_binary64_10592` `associate--r-_binary64_10588` `associate--l-_binary64_10587` `associate--l+_binary64_10586` `associate--r+_binary64_10585`

Counts

189 → 276

Iterations

Useful iterations: 1 (0.0ms)

Iter	Nodes	Cost
0	187	2626
1	459	2443
2	1580	2443
3	3895	2443

prune329.0ms (1.4%)

Pruning

13 alts after pruning (13 fresh and 0 done)

	Pruned	Kept	Total
New	268	8	276
Fresh	4	5	9
Picked	1	0	1
Done	0	0	0
Total	273	13	286

Error

0.0b

Counts

286 → 13

Compiler

Compiled 9506 to 946 computations (90% saved)

localize30.0ms (0.1%)

Local error

Found 4 expressions with local error:

5.1b	(.f64 (-.f64 (.f64 t c) (*.f64 i y)) j)
6.8b	(cbrt.f64 (.f64 (-.f64 (.f64 t c) (*.f64 i y)) j))
6.8b	(cbrt.f64 (.f64 j (-.f64 (.f64 c t) (*.f64 i y))))
6.8b	(cbrt.f64 (.f64 j (-.f64 (.f64 c t) (*.f64 i y))))

rewrite126.0ms (0.5%)

Algorithm

1×	rewrite-expression-head

Error

0.0b

Rules

8×	`add-sqr-sqrt_binary64_10671`
6×	`pow1_binary64_10710` `add-exp-log_binary64_10687` `add-cbrt-cube_binary64_10685` `add-cube-cbrt_binary64_10684` `cbrt-div_binary64_10681` `*-un-lft-identity_binary64_10649`
4×	`add-log-exp_binary64_10688` `flip3--_binary64_10653` `associate-r/_binary64_10591` `flip--_binary64_10624` `associate-l/_binary64_10592`
3×	`pow1/3_binary64_10731` `cbrt-prod_binary64_10680` `associate-l_binary64_10590` `associate-r_binary64_10589`
1×	`pow-prod-down_binary64_10720` `prod-exp_binary64_10698` `cbrt-unprod_binary64_10682` `unswap-sqr_binary64_10617` `*-commutative_binary64_10580`

Counts

4 → 53

Calls

4 calls:

7.0ms	(cbrt.f64 (.f64 j (-.f64 (.f64 c t) (*.f64 i y))))
7.0ms	(.f64 (-.f64 (.f64 t c) (*.f64 i y)) j)
5.0ms	(cbrt.f64 (.f64 j (-.f64 (.f64 c t) (*.f64 i y))))
5.0ms	(cbrt.f64 (.f64 (-.f64 (.f64 t c) (*.f64 i y)) j))

Compiler

Compiled 3299 to 319 computations (90.3% saved)

series2.9s (12%)

Error

0.0b

Counts

4 → 96

Calls

4 calls:

762.0ms	(cbrt.f64 (.f64 j (-.f64 (.f64 c t) (*.f64 i y))))
750.0ms	(cbrt.f64 (.f64 j (-.f64 (.f64 c t) (*.f64 i y))))
738.0ms	(cbrt.f64 (.f64 (-.f64 (.f64 t c) (*.f64 i y)) j))
441.0ms	(.f64 (-.f64 (.f64 t c) (*.f64 i y)) j)

Compiler

Compiled 16341 to 8137 computations (50.2% saved)

simplify484.0ms (2%)

Algorithm

1×	egg-herbie

Rules

520×	`associate-/l*_binary64_10594`
472×	`times-frac_binary64_10655`
322×	`associate-/r*_binary64_10593`
194×	`associate-/r/_binary64_10595`
180×	`distribute-rgt-neg-in_binary64_10607`
174×	`distribute-rgt-in_binary64_10599`
172×	`distribute-lft-in_binary64_10598`
161×	`distribute-lft-neg-in_binary64_10606`
148×	`cancel-sign-sub-inv_binary64_10615`
145×	`associate-r_binary64_10589`
126×	`associate-l_binary64_10590`
114×	`distribute-neg-frac_binary64_10613`
94×	`*-commutative_binary64_10580`
76×	`exp-sum_binary64_10695`
72×	`sub-neg_binary64_10642`
65×	`sqr-pow_binary64_10621`
56×	`associate-*r/_binary64_10591`
52×	`distribute-lft-neg-out_binary64_10608`
50×	`neg-mul-1_binary64_10645`
49×	`neg-sub0_binary64_10644`
48×	`exp-prod_binary64_10701`
38×	`log-prod_binary64_10735`
32×	`associate-*l/_binary64_10592`
29×	`unsub-neg_binary64_10643`
26×	`associate-/l/_binary64_10596` `+-commutative_binary64_10579`
23×	`pow-sqr_binary64_10622`
21×	`distribute-rgt-neg-out_binary64_10609`
17×	`distribute-lft-out_binary64_10600`
16×	`distribute-rgt-out_binary64_10602`
13×	`unpow1/3_binary64_10716` `exp-diff_binary64_10697` `distribute-neg-out_binary64_10611`
12×	`cube-prod_binary64_10677`
10×	`log-div_binary64_10736` `div-sub_binary64_10654` `swap-sqr_binary64_10616` `distribute-neg-in_binary64_10610` `associate--r-_binary64_10588` `associate-+l+_binary64_10582`
9×	`*-rgt-identity_binary64_10639`
8×	`*-lft-identity_binary64_10638` `associate--l+_binary64_10586`
7×	`unpow3_binary64_10715` `cube-mult_binary64_10679`
6×	`unswap-sqr_binary64_10617`
5×	`log-rec_binary64_10737` `cube-unmult_binary64_10686` `mul-1-neg_binary64_10641` `remove-double-neg_binary64_10637` `--rgt-identity_binary64_10635` `associate-+r+_binary64_10581`
4×	`difference-of-squares_binary64_10618`
3×	`exp-to-pow_binary64_10711`
2×	`rem-3cbrt-lft_binary64_10674` `distribute-lft-out--_binary64_10601`
1×	`log-pow_binary64_10738` `pow-plus_binary64_10712` `prod-exp_binary64_10698` `1-exp_binary64_10693` `exp-1-e_binary64_10692` `rem-log-exp_binary64_10690` `rem-exp-log_binary64_10689`
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_10912` `erf-erfc_binary64_10911` `erf-odd_binary64_10910` `if-if-and-not_binary64_10909` `if-if-and_binary64_10908` `if-if-or-not_binary64_10907` `if-if-or_binary64_10906` `if-not_binary64_10905` `if-same_binary64_10904` `if-false_binary64_10903` `if-true_binary64_10902` `not-gte_binary64_10901` `not-lte_binary64_10900` `not-gt_binary64_10899` `not-lt_binary64_10898` `gte-same_binary64_10897` `lte-same_binary64_10896` `gt-same_binary64_10895` `lt-same_binary64_10894` `sinh---cosh_binary64_10841` `sinh-+-cosh_binary64_10840` `sinh-cosh_binary64_10839` `tanh-def-c_binary64_10838` `tanh-def-b_binary64_10837` `tanh-def-a_binary64_10836` `cosh-def_binary64_10835` `sinh-def_binary64_10834` `tan-neg_binary64_10781` `cos-neg_binary64_10780` `sin-neg_binary64_10779` `tan-0_binary64_10778` `cos-0_binary64_10777` `sin-0_binary64_10776` `hang-m-tan_binary64_10775` `hang-p-tan_binary64_10774` `hang-m0-tan_binary64_10773` `hang-p0-tan_binary64_10772` `hang-0m-tan_binary64_10771` `hang-0p-tan_binary64_10770` `tan-+PI/2_binary64_10769` `tan-+PI_binary64_10768` `tan-PI_binary64_10767` `tan-PI/3_binary64_10766` `tan-PI/4_binary64_10765` `tan-PI/6_binary64_10764` `cos-+PI/2_binary64_10763` `cos-+PI_binary64_10762` `cos-PI_binary64_10761` `cos-PI/2_binary64_10760` `cos-PI/3_binary64_10759` `cos-PI/4_binary64_10758` `cos-PI/6_binary64_10757` `sin-+PI/2_binary64_10756` `sin-+PI_binary64_10755` `sin-PI_binary64_10754` `sin-PI/2_binary64_10753` `sin-PI/3_binary64_10752` `sin-PI/4_binary64_10751` `sin-PI/6_binary64_10750` `sub-1-sin_binary64_10749` `sub-1-cos_binary64_10748` `-1-add-sin_binary64_10747` `-1-add-cos_binary64_10746` `1-sub-sin_binary64_10745` `1-sub-cos_binary64_10744` `cos-sin-sum_binary64_10743` `log-E_binary64_10739` `pow-base-0_binary64_10733` `unpow2_binary64_10714` `unpow1/2_binary64_10713` `pow-base-1_binary64_10709` `unpow0_binary64_10708` `unpow1_binary64_10707` `unpow-1_binary64_10706` `exp-lft-cube_binary64_10705` `exp-lft-sqr_binary64_10704` `exp-cbrt_binary64_10703` `exp-sqrt_binary64_10702` `div-exp_binary64_10700` `rec-exp_binary64_10699` `exp-neg_binary64_10696` `e-exp-1_binary64_10694` `exp-0_binary64_10691` `cube-div_binary64_10678` `cube-neg_binary64_10676` `rem-3cbrt-rft_binary64_10675` `rem-cbrt-cube_binary64_10673` `rem-cube-cbrt_binary64_10672` `sqr-abs_binary64_10664` `sqr-neg_binary64_10663` `rem-sqrt-square_binary64_10662` `rem-square-sqrt_binary64_10661` `/-rgt-identity_binary64_10640` `sub0-neg_binary64_10636` `+-rgt-identity_binary64_10634` `+-lft-identity_binary64_10633` `mul0-rgt_binary64_10632` `mul0-lft_binary64_10631` `div0_binary64_10630` `*-inverses_binary64_10629` `+-inverses_binary64_10628` `lft-mult-inverse_binary64_10627` `rgt-mult-inverse_binary64_10626` `remove-double-div_binary64_10625` `difference-of-sqr--1_binary64_10620` `difference-of-sqr-1_binary64_10619` `cancel-sign-sub_binary64_10614` `distribute-frac-neg_binary64_10612` `distribute-rgt1-in_binary64_10605` `distribute-lft1-in_binary64_10604` `distribute-rgt-out--_binary64_10603` `count-2_binary64_10597` `associate--l-_binary64_10587` `associate--r+_binary64_10585` `associate-+l-_binary64_10584` `associate-+r-_binary64_10583`

Counts

149 → 339

Iterations

Useful iterations: 2 (0.0ms)

Iter	Nodes	Cost
0	209	3656
1	525	3442
2	1714	3360

prune671.0ms (2.8%)

Pruning

13 alts after pruning (12 fresh and 1 done)

	Pruned	Kept	Total
New	339	0	339
Fresh	0	12	12
Picked	0	1	1
Done	0	0	0
Total	339	13	352

Error

0.0b

Counts

352 → 13

Compiler

Compiled 21416 to 2897 computations (86.5% saved)

localize25.0ms (0.1%)

Local error

Found 4 expressions with local error:

1.6b	(.f64 (.f64 (cbrt.f64 c) (cbrt.f64 c)) (.f64 (-.f64 (.f64 z b) (*.f64 j t)) (cbrt.f64 c)))
1.8b	(.f64 (-.f64 (.f64 z b) (*.f64 j t)) (cbrt.f64 c))
5.6b	(.f64 a (-.f64 (.f64 b i) (*.f64 x t)))
5.7b	(.f64 y (-.f64 (.f64 x z) (*.f64 i j)))

rewrite195.0ms (0.8%)

Algorithm

1×	rewrite-expression-head

Error

0.0b

Rules

22×	`pow1_binary64_10710` `add-exp-log_binary64_10687`
19×	`add-sqr-sqrt_binary64_10671`
15×	`add-cbrt-cube_binary64_10685`
13×	`associate-r_binary64_10589`
11×	`pow-prod-down_binary64_10720` `prod-exp_binary64_10698` `add-cube-cbrt_binary64_10684` `cbrt-unprod_binary64_10682` `*-un-lft-identity_binary64_10649`
10×	`associate-l_binary64_10590`
6×	`associate-*r/_binary64_10591`
4×	`add-log-exp_binary64_10688` `unswap-sqr_binary64_10617` `sub-neg_binary64_10642` `distribute-rgt-in_binary64_10599` `cancel-sign-sub-inv_binary64_10615` `distribute-lft-in_binary64_10598` `flip3--_binary64_10653` `flip--_binary64_10624` `-commutative_binary64_10580` `cbrt-prod_binary64_10680` `associate-l/_binary64_10592`

Counts

4 → 96

Calls

4 calls:

12.0ms	(.f64 (.f64 (cbrt.f64 c) (cbrt.f64 c)) (.f64 (-.f64 (.f64 z b) (*.f64 j t)) (cbrt.f64 c)))
10.0ms	(.f64 (-.f64 (.f64 z b) (*.f64 j t)) (cbrt.f64 c))
7.0ms	(.f64 a (-.f64 (.f64 b i) (*.f64 x t)))
6.0ms	(.f64 y (-.f64 (.f64 x z) (*.f64 i j)))

Compiler

Compiled 4356 to 512 computations (88.2% saved)

series2.4s (10%)

Error

0.0b

Counts

4 → 108

Calls

4 calls:

993.0ms	(.f64 (-.f64 (.f64 z b) (*.f64 j t)) (cbrt.f64 c))
446.0ms	(.f64 (.f64 (cbrt.f64 c) (cbrt.f64 c)) (.f64 (-.f64 (.f64 z b) (*.f64 j t)) (cbrt.f64 c)))
428.0ms	(.f64 a (-.f64 (.f64 b i) (*.f64 x t)))
410.0ms	(.f64 y (-.f64 (.f64 x z) (*.f64 i j)))

Compiler

Compiled 9630 to 4813 computations (50% saved)

simplify464.0ms (1.9%)

Algorithm

1×	egg-herbie

Rules

711×	`distribute-rgt-in_binary64_10599`
705×	`distribute-lft-in_binary64_10598`
404×	`associate-l_binary64_10590`
351×	`associate-r_binary64_10589`
175×	`distribute-rgt-neg-in_binary64_10607`
168×	`cancel-sign-sub-inv_binary64_10615`
149×	`exp-prod_binary64_10701`
148×	`distribute-lft-neg-in_binary64_10606`
118×	`*-commutative_binary64_10580`
92×	`unswap-sqr_binary64_10617`
81×	`sqr-pow_binary64_10621`
79×	`distribute-lft-neg-out_binary64_10608`
59×	`distribute-rgt-neg-out_binary64_10609`
58×	`log-prod_binary64_10735`
50×	`neg-sub0_binary64_10644`
49×	`cube-prod_binary64_10677`
43×	`*-lft-identity_binary64_10638`
42×	`neg-mul-1_binary64_10645` `*-rgt-identity_binary64_10639`
41×	`sub-neg_binary64_10642`
37×	`swap-sqr_binary64_10616`
32×	`pow-sqr_binary64_10622`
27×	`exp-sum_binary64_10695`
21×	`+-commutative_binary64_10579`
13×	`unpow3_binary64_10715` `cube-unmult_binary64_10686` `cube-mult_binary64_10679`
12×	`exp-diff_binary64_10697`
10×	`distribute-neg-in_binary64_10610`
9×	`mul-1-neg_binary64_10641` `difference-of-squares_binary64_10618`
5×	`log-pow_binary64_10738` `pow-plus_binary64_10712` `div-sub_binary64_10654`
4×	`distribute-rgt-out--_binary64_10603` `associate-+l+_binary64_10582` `associate-+r+_binary64_10581`
3×	`rem-sqrt-square_binary64_10662` `remove-double-neg_binary64_10637` `distribute-rgt-out_binary64_10602`
2×	`unpow1/3_binary64_10716` `+-rgt-identity_binary64_10634` `distribute-lft-out--_binary64_10601` `associate-+r-_binary64_10583`
1×	`prod-exp_binary64_10698` `1-exp_binary64_10693` `exp-1-e_binary64_10692` `rem-log-exp_binary64_10690` `rem-3cbrt-rft_binary64_10675` `rem-3cbrt-lft_binary64_10674` `rem-cube-cbrt_binary64_10672` `unsub-neg_binary64_10643` `distribute-rgt1-in_binary64_10605` `distribute-lft-out_binary64_10600` `count-2_binary64_10597`
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_10912` `erf-erfc_binary64_10911` `erf-odd_binary64_10910` `if-if-and-not_binary64_10909` `if-if-and_binary64_10908` `if-if-or-not_binary64_10907` `if-if-or_binary64_10906` `if-not_binary64_10905` `if-same_binary64_10904` `if-false_binary64_10903` `if-true_binary64_10902` `not-gte_binary64_10901` `not-lte_binary64_10900` `not-gt_binary64_10899` `not-lt_binary64_10898` `gte-same_binary64_10897` `lte-same_binary64_10896` `gt-same_binary64_10895` `lt-same_binary64_10894` `sinh---cosh_binary64_10841` `sinh-+-cosh_binary64_10840` `sinh-cosh_binary64_10839` `tanh-def-c_binary64_10838` `tanh-def-b_binary64_10837` `tanh-def-a_binary64_10836` `cosh-def_binary64_10835` `sinh-def_binary64_10834` `tan-neg_binary64_10781` `cos-neg_binary64_10780` `sin-neg_binary64_10779` `tan-0_binary64_10778` `cos-0_binary64_10777` `sin-0_binary64_10776` `hang-m-tan_binary64_10775` `hang-p-tan_binary64_10774` `hang-m0-tan_binary64_10773` `hang-p0-tan_binary64_10772` `hang-0m-tan_binary64_10771` `hang-0p-tan_binary64_10770` `tan-+PI/2_binary64_10769` `tan-+PI_binary64_10768` `tan-PI_binary64_10767` `tan-PI/3_binary64_10766` `tan-PI/4_binary64_10765` `tan-PI/6_binary64_10764` `cos-+PI/2_binary64_10763` `cos-+PI_binary64_10762` `cos-PI_binary64_10761` `cos-PI/2_binary64_10760` `cos-PI/3_binary64_10759` `cos-PI/4_binary64_10758` `cos-PI/6_binary64_10757` `sin-+PI/2_binary64_10756` `sin-+PI_binary64_10755` `sin-PI_binary64_10754` `sin-PI/2_binary64_10753` `sin-PI/3_binary64_10752` `sin-PI/4_binary64_10751` `sin-PI/6_binary64_10750` `sub-1-sin_binary64_10749` `sub-1-cos_binary64_10748` `-1-add-sin_binary64_10747` `-1-add-cos_binary64_10746` `1-sub-sin_binary64_10745` `1-sub-cos_binary64_10744` `cos-sin-sum_binary64_10743` `log-E_binary64_10739` `log-rec_binary64_10737` `log-div_binary64_10736` `pow-base-0_binary64_10733` `unpow2_binary64_10714` `unpow1/2_binary64_10713` `exp-to-pow_binary64_10711` `pow-base-1_binary64_10709` `unpow0_binary64_10708` `unpow1_binary64_10707` `unpow-1_binary64_10706` `exp-lft-cube_binary64_10705` `exp-lft-sqr_binary64_10704` `exp-cbrt_binary64_10703` `exp-sqrt_binary64_10702` `div-exp_binary64_10700` `rec-exp_binary64_10699` `exp-neg_binary64_10696` `e-exp-1_binary64_10694` `exp-0_binary64_10691` `rem-exp-log_binary64_10689` `cube-div_binary64_10678` `cube-neg_binary64_10676` `rem-cbrt-cube_binary64_10673` `sqr-abs_binary64_10664` `sqr-neg_binary64_10663` `rem-square-sqrt_binary64_10661` `times-frac_binary64_10655` `/-rgt-identity_binary64_10640` `sub0-neg_binary64_10636` `--rgt-identity_binary64_10635` `+-lft-identity_binary64_10633` `mul0-rgt_binary64_10632` `mul0-lft_binary64_10631` `div0_binary64_10630` `-inverses_binary64_10629` `+-inverses_binary64_10628` `lft-mult-inverse_binary64_10627` `rgt-mult-inverse_binary64_10626` `remove-double-div_binary64_10625` `difference-of-sqr--1_binary64_10620` `difference-of-sqr-1_binary64_10619` `cancel-sign-sub_binary64_10614` `distribute-neg-frac_binary64_10613` `distribute-frac-neg_binary64_10612` `distribute-neg-out_binary64_10611` `distribute-lft1-in_binary64_10604` `associate-/l/_binary64_10596` `associate-/r/_binary64_10595` `associate-/l_binary64_10594` `associate-/r_binary64_10593` `associate-l/_binary64_10592` `associate-*r/_binary64_10591` `associate--r-_binary64_10588` `associate--l-_binary64_10587` `associate--l+_binary64_10586` `associate--r+_binary64_10585` `associate-+l-_binary64_10584`

Counts

204 → 320

Iterations

Useful iterations: 1 (0.0ms)

Iter	Nodes	Cost
0	220	3510
1	567	2862
2	2165	2862

prune393.0ms (1.6%)

Pruning

13 alts after pruning (11 fresh and 2 done)

	Pruned	Kept	Total
New	320	0	320
Fresh	0	11	11
Picked	0	1	1
Done	0	1	1
Total	320	13	333

Error

0.0b

Counts

333 → 13

Compiler

Compiled 12381 to 702 computations (94.3% saved)

regimes3.8s (15.9%)

Accuracy

Total 3.5b remaining (97.2%)

Threshold costs 0b (0%)

Compiler

Compiled 34856 to 24638 computations (29.3% saved)

bsearch9.0ms (0%)

Compiler: Compiled 29 to 23 computations (20.7% saved)

simplify170.0ms (0.7%)

Algorithm

1×	egg-herbie

Rules

214×	`unsub-neg_binary64_10643`
202×	`neg-sub0_binary64_10644`
201×	`neg-mul-1_binary64_10645`
174×	`distribute-rgt-neg-in_binary64_10607`
165×	`distribute-rgt-neg-out_binary64_10609`
140×	`distribute-neg-out_binary64_10611`
123×	`distribute-lft-neg-out_binary64_10608`
109×	`cancel-sign-sub-inv_binary64_10615` `distribute-lft-neg-in_binary64_10606`
72×	`sub-neg_binary64_10642`
65×	`*-commutative_binary64_10580`
63×	`remove-double-neg_binary64_10637`
59×	`+-commutative_binary64_10579`
46×	`distribute-neg-in_binary64_10610`
9×	`+-lft-identity_binary64_10633`
8×	`+-rgt-identity_binary64_10634`
1×	`sqr-neg_binary64_10663` `mul-1-neg_binary64_10641` `--rgt-identity_binary64_10635`
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_10909` `if-if-and_binary64_10908` `if-if-or-not_binary64_10907` `if-if-or_binary64_10906` `if-not_binary64_10905` `if-same_binary64_10904` `if-false_binary64_10903` `if-true_binary64_10902` `tan-0_binary64_10778` `cos-0_binary64_10777` `sin-0_binary64_10776` `unpow1_binary64_10707` `e-exp-1_binary64_10694` `1-exp_binary64_10693` `exp-1-e_binary64_10692` `exp-0_binary64_10691` `sqr-abs_binary64_10664` `/-rgt-identity_binary64_10640` `-rgt-identity_binary64_10639` `-lft-identity_binary64_10638` `sub0-neg_binary64_10636` `cancel-sign-sub_binary64_10614` `distribute-neg-frac_binary64_10613` `distribute-frac-neg_binary64_10612`

Iterations

Useful iterations: 1 (0.0ms)

Iter	Nodes	Cost
0	50	221
1	112	219
2	175	219
3	226	219
4	299	219
5	351	219
6	411	219
7	604	219
8	779	219
9	759	219
10	837	219
11	897	219
12	947	219
13	983	219
14	1002	219
15	1007	219
16	1008	219
17	1008	219

Proof

(if real (<= f64 (+ f64 (- f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4)))) (* f64 h8 (- f64 (* f64 h6 h3) (* f64 h7 h1)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (- f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8)))) (if real (<= f64 (+ f64 (- f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4)))) (* f64 h8 (- f64 (* f64 h6 h3) (* f64 h7 h1)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (=> (- f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h6 h3) (* f64 h7 h1)))) (+ f64 (- f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (* f64 -1 (* f64 h7 (* f64 h8 h1))))))
sub-neg_binary64_10642 =>
(if real (<= f64 (+ f64 (- f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4)))) (* f64 h8 (- f64 (* f64 h6 h3) (* f64 h7 h1)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (- f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8)))) (if real (<= f64 (+ f64 (=> (- f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h6 h3) (* f64 h7 h1)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h6 h3) (* f64 h7 h1)))) (+ f64 (- f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (* f64 -1 (* f64 h7 (* f64 h8 h1))))))
sub-neg_binary64_10642 =>
(if real (<= f64 (+ f64 (=> (- f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h6 h3) (* f64 h7 h1)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (- f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8)))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h6 h3) (* f64 h7 h1)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h6 h3) (* f64 h7 h1)))) (+ f64 (- f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (* f64 -1 (* f64 h7 (* f64 h8 h1))))))
sub-neg_binary64_10642 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h6 h3) (* f64 h7 h1)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (- f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8)))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h6 h3) (* f64 h7 h1)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h6 h3) (* f64 h7 h1)))) (+ f64 (- f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (=> (* f64 -1 (* f64 h7 (* f64 h8 h1)))))))
mul-1-neg_binary64_10641 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h6 h3) (* f64 h7 h1)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (- f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8)))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h6 h3) (* f64 h7 h1)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (=> (* f64 h6 h3)) (* f64 h7 h1)))) (+ f64 (- f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (neg f64 (* f64 h7 (* f64 h8 h1))))))
*-commutative_binary64_10580 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h6 h3) (* f64 h7 h1)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (- f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8)))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (=> (* f64 h6 h3)) (* f64 h7 h1)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h7 h1)))) (+ f64 (- f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (neg f64 (* f64 h7 (* f64 h8 h1))))))
*-commutative_binary64_10580 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (=> (* f64 h6 h3)) (* f64 h7 h1)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (- f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8)))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h7 h1)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h7 h1)))) (+ f64 (- f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (neg f64 (* f64 h7 (* f64 h8 h1))))))
*-commutative_binary64_10580 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h7 h1)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (- f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8)))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h7 h1)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h3 h6) (=> (* f64 h7 h1))))) (+ f64 (- f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (neg f64 (* f64 h7 (* f64 h8 h1))))))
*-commutative_binary64_10580 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h7 h1)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (- f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8)))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h3 h6) (=> (* f64 h7 h1))))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (+ f64 (- f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (neg f64 (* f64 h7 (* f64 h8 h1))))))
*-commutative_binary64_10580 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h3 h6) (=> (* f64 h7 h1))))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (- f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8)))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (+ f64 (- f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (neg f64 (* f64 h7 (* f64 h8 h1))))))
*-commutative_binary64_10580 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (=> (+ f64 (- f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (+ f64 (- f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (neg f64 (* f64 h7 (* f64 h8 h1))))))
+-commutative_binary64_10579 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (=> (- f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (+ f64 (- f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (neg f64 (* f64 h7 (* f64 h8 h1))))))
sub-neg_binary64_10642 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (neg f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (=> (+ f64 (- f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (neg f64 (* f64 h7 (* f64 h8 h1)))))))
unsub-neg_binary64_10643 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (neg f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (=> (- f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8))))) (* f64 h7 (* f64 h8 h1)))))
sub-neg_binary64_10642 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (neg f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (neg f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8))))) (* f64 h7 (=> (* f64 h8 h1))))))
*-commutative_binary64_10580 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (neg f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (=> (neg f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))))) (* f64 h7 (* f64 h1 h8)))))
distribute-rgt-neg-in_binary64_10607 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (neg f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (neg f64 (=> (- f64 (* f64 h2 h5) (* f64 h3 h8)))))) (* f64 h7 (* f64 h1 h8)))))
sub-neg_binary64_10642 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (neg f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (=> (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4)))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (neg f64 (+ f64 (* f64 h2 h5) (neg f64 (* f64 h3 h8)))))) (* f64 h7 (* f64 h1 h8)))))
distribute-rgt-neg-in_binary64_10607 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (neg f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (neg f64 (=> (- f64 (* f64 h6 h2) (* f64 h7 h4)))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (neg f64 (+ f64 (* f64 h2 h5) (neg f64 (* f64 h3 h8)))))) (* f64 h7 (* f64 h1 h8)))))
sub-neg_binary64_10642 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (neg f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (=> (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4)))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (neg f64 (+ f64 (* f64 h6 h2) (neg f64 (* f64 h7 h4)))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (neg f64 (+ f64 (* f64 h2 h5) (neg f64 (* f64 h3 h8)))))) (* f64 h7 (* f64 h1 h8)))))
distribute-rgt-neg-in_binary64_10607 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (neg f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (neg f64 (=> (- f64 (* f64 h6 h2) (* f64 h7 h4)))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (neg f64 (+ f64 (* f64 h6 h2) (neg f64 (* f64 h7 h4)))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (neg f64 (+ f64 (* f64 h2 h5) (neg f64 (* f64 h3 h8)))))) (* f64 h7 (* f64 h1 h8)))))
sub-neg_binary64_10642 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (=> (neg f64 (* f64 h5 (- f64 (* f64 h6 h2) (* f64 h7 h4)))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (neg f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (neg f64 (+ f64 (* f64 h6 h2) (neg f64 (* f64 h7 h4)))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (neg f64 (+ f64 (* f64 h6 h2) (neg f64 (* f64 h7 h4)))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (neg f64 (+ f64 (* f64 h2 h5) (neg f64 (* f64 h3 h8)))))) (* f64 h7 (* f64 h1 h8)))))
distribute-rgt-neg-in_binary64_10607 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (neg f64 (=> (- f64 (* f64 h6 h2) (* f64 h7 h4)))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (neg f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (neg f64 (+ f64 (* f64 h6 h2) (neg f64 (* f64 h7 h4)))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (neg f64 (+ f64 (* f64 h6 h2) (neg f64 (* f64 h7 h4)))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (neg f64 (+ f64 (* f64 h2 h5) (neg f64 (* f64 h3 h8)))))) (* f64 h7 (* f64 h1 h8)))))
sub-neg_binary64_10642 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (neg f64 (+ f64 (* f64 h6 h2) (neg f64 (* f64 h7 h4)))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (neg f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (neg f64 (+ f64 (* f64 h6 h2) (neg f64 (* f64 h7 h4)))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (neg f64 (=> (+ f64 (* f64 h6 h2) (neg f64 (* f64 h7 h4))))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (neg f64 (+ f64 (* f64 h2 h5) (neg f64 (* f64 h3 h8)))))) (* f64 h7 (* f64 h1 h8)))))
+-commutative_binary64_10579 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (neg f64 (+ f64 (* f64 h6 h2) (neg f64 (* f64 h7 h4)))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (neg f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (neg f64 (=> (+ f64 (* f64 h6 h2) (neg f64 (* f64 h7 h4))))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (neg f64 (+ f64 (neg f64 (* f64 h7 h4)) (* f64 h6 h2))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (neg f64 (+ f64 (* f64 h2 h5) (neg f64 (* f64 h3 h8)))))) (* f64 h7 (* f64 h1 h8)))))
+-commutative_binary64_10579 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (neg f64 (=> (+ f64 (* f64 h6 h2) (neg f64 (* f64 h7 h4))))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (neg f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (neg f64 (+ f64 (neg f64 (* f64 h7 h4)) (* f64 h6 h2))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (neg f64 (+ f64 (neg f64 (* f64 h7 h4)) (* f64 h6 h2))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (neg f64 (+ f64 (* f64 h2 h5) (neg f64 (* f64 h3 h8)))))) (* f64 h7 (* f64 h1 h8)))))
+-commutative_binary64_10579 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (neg f64 (+ f64 (neg f64 (* f64 h7 h4)) (* f64 h6 h2))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (=> (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (neg f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8))))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (neg f64 (+ f64 (neg f64 (* f64 h7 h4)) (* f64 h6 h2))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (neg f64 (+ f64 (neg f64 (* f64 h7 h4)) (* f64 h6 h2))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (neg f64 (+ f64 (* f64 h2 h5) (neg f64 (* f64 h3 h8)))))) (* f64 h7 (* f64 h1 h8)))))
+-commutative_binary64_10579 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (neg f64 (+ f64 (neg f64 (* f64 h7 h4)) (* f64 h6 h2))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (neg f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (=> (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3)))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (neg f64 (+ f64 (neg f64 (* f64 h7 h4)) (* f64 h6 h2))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (neg f64 (+ f64 (neg f64 (* f64 h7 h4)) (* f64 h6 h2))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (neg f64 (+ f64 (* f64 h2 h5) (neg f64 (* f64 h3 h8)))))) (* f64 h7 (* f64 h1 h8)))))
*-commutative_binary64_10580 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (neg f64 (+ f64 (neg f64 (* f64 h7 h4)) (* f64 h6 h2))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (neg f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (* f64 (- f64 (* f64 h5 h7) (* f64 h0 h3)) h4))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (neg f64 (+ f64 (neg f64 (* f64 h7 h4)) (* f64 h6 h2))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (neg f64 (+ f64 (neg f64 (* f64 h7 h4)) (* f64 h6 h2))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (neg f64 (=> (+ f64 (* f64 h2 h5) (neg f64 (* f64 h3 h8))))))) (* f64 h7 (* f64 h1 h8)))))
+-commutative_binary64_10579 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (neg f64 (+ f64 (neg f64 (* f64 h7 h4)) (* f64 h6 h2))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (neg f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (* f64 (- f64 (* f64 h5 h7) (* f64 h0 h3)) h4))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (neg f64 (+ f64 (neg f64 (* f64 h7 h4)) (* f64 h6 h2))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (neg f64 (+ f64 (neg f64 (* f64 h7 h4)) (* f64 h6 h2))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (=> (neg f64 (+ f64 (neg f64 (* f64 h3 h8)) (* f64 h2 h5)))))) (* f64 h7 (* f64 h1 h8)))))
distribute-neg-in_binary64_10610 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (neg f64 (+ f64 (neg f64 (* f64 h7 h4)) (* f64 h6 h2))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (neg f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (* f64 (- f64 (* f64 h5 h7) (* f64 h0 h3)) h4))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (neg f64 (+ f64 (neg f64 (* f64 h7 h4)) (* f64 h6 h2))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (=> (neg f64 (+ f64 (neg f64 (* f64 h7 h4)) (* f64 h6 h2)))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (+ f64 (neg f64 (neg f64 (* f64 h3 h8))) (neg f64 (* f64 h2 h5))))) (* f64 h7 (* f64 h1 h8)))))
distribute-neg-in_binary64_10610 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (neg f64 (+ f64 (neg f64 (* f64 h7 h4)) (* f64 h6 h2))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (neg f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (* f64 (- f64 (* f64 h5 h7) (* f64 h0 h3)) h4))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (=> (neg f64 (+ f64 (neg f64 (* f64 h7 h4)) (* f64 h6 h2)))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (+ f64 (neg f64 (neg f64 (* f64 h7 h4))) (neg f64 (* f64 h6 h2))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (+ f64 (neg f64 (neg f64 (* f64 h3 h8))) (neg f64 (* f64 h2 h5))))) (* f64 h7 (* f64 h1 h8)))))
distribute-neg-in_binary64_10610 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (=> (neg f64 (+ f64 (neg f64 (* f64 h7 h4)) (* f64 h6 h2)))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (neg f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (* f64 (- f64 (* f64 h5 h7) (* f64 h0 h3)) h4))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (+ f64 (neg f64 (neg f64 (* f64 h7 h4))) (neg f64 (* f64 h6 h2))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (+ f64 (neg f64 (neg f64 (* f64 h7 h4))) (neg f64 (* f64 h6 h2))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (+ f64 (neg f64 (neg f64 (* f64 h3 h8))) (neg f64 (* f64 h2 h5))))) (* f64 h7 (* f64 h1 h8)))))
distribute-neg-in_binary64_10610 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (+ f64 (neg f64 (neg f64 (* f64 h7 h4))) (neg f64 (* f64 h6 h2))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (neg f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (* f64 (- f64 (* f64 h5 h7) (* f64 h0 h3)) h4))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (+ f64 (neg f64 (neg f64 (* f64 h7 h4))) (neg f64 (* f64 h6 h2))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (+ f64 (neg f64 (neg f64 (* f64 h7 h4))) (neg f64 (* f64 h6 h2))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (=> (+ f64 (neg f64 (neg f64 (* f64 h3 h8))) (neg f64 (* f64 h2 h5)))))) (* f64 h7 (* f64 h1 h8)))))
unsub-neg_binary64_10643 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (+ f64 (neg f64 (neg f64 (* f64 h7 h4))) (neg f64 (* f64 h6 h2))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (neg f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (* f64 (- f64 (* f64 h5 h7) (* f64 h0 h3)) h4))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (+ f64 (neg f64 (neg f64 (* f64 h7 h4))) (neg f64 (* f64 h6 h2))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (=> (+ f64 (neg f64 (neg f64 (* f64 h7 h4))) (neg f64 (* f64 h6 h2)))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (neg f64 (neg f64 (* f64 h3 h8))) (* f64 h2 h5)))) (* f64 h7 (* f64 h1 h8)))))
unsub-neg_binary64_10643 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (+ f64 (neg f64 (neg f64 (* f64 h7 h4))) (neg f64 (* f64 h6 h2))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (neg f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (* f64 (- f64 (* f64 h5 h7) (* f64 h0 h3)) h4))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (+ f64 (neg f64 (neg f64 (* f64 h7 h4))) (neg f64 (* f64 h6 h2))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (neg f64 (neg f64 (* f64 h7 h4))) (=> (* f64 h6 h2))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (neg f64 (neg f64 (* f64 h3 h8))) (* f64 h2 h5)))) (* f64 h7 (* f64 h1 h8)))))
*-commutative_binary64_10580 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (+ f64 (neg f64 (neg f64 (* f64 h7 h4))) (neg f64 (* f64 h6 h2))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (neg f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (* f64 (- f64 (* f64 h5 h7) (* f64 h0 h3)) h4))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (=> (+ f64 (neg f64 (neg f64 (* f64 h7 h4))) (neg f64 (* f64 h6 h2)))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (neg f64 (neg f64 (* f64 h7 h4))) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (neg f64 (neg f64 (* f64 h3 h8))) (* f64 h2 h5)))) (* f64 h7 (* f64 h1 h8)))))
unsub-neg_binary64_10643 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (+ f64 (neg f64 (neg f64 (* f64 h7 h4))) (neg f64 (* f64 h6 h2))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (neg f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (* f64 (- f64 (* f64 h5 h7) (* f64 h0 h3)) h4))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (neg f64 (neg f64 (* f64 h7 h4))) (=> (* f64 h6 h2))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (neg f64 (neg f64 (* f64 h7 h4))) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (neg f64 (neg f64 (* f64 h3 h8))) (* f64 h2 h5)))) (* f64 h7 (* f64 h1 h8)))))
*-commutative_binary64_10580 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (=> (+ f64 (neg f64 (neg f64 (* f64 h7 h4))) (neg f64 (* f64 h6 h2)))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (neg f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (* f64 (- f64 (* f64 h5 h7) (* f64 h0 h3)) h4))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (neg f64 (neg f64 (* f64 h7 h4))) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (neg f64 (neg f64 (* f64 h7 h4))) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (neg f64 (neg f64 (* f64 h3 h8))) (* f64 h2 h5)))) (* f64 h7 (* f64 h1 h8)))))
unsub-neg_binary64_10643 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (neg f64 (neg f64 (* f64 h7 h4))) (=> (* f64 h6 h2))))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (neg f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (* f64 (- f64 (* f64 h5 h7) (* f64 h0 h3)) h4))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (neg f64 (neg f64 (* f64 h7 h4))) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (neg f64 (neg f64 (* f64 h7 h4))) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (neg f64 (neg f64 (* f64 h3 h8))) (* f64 h2 h5)))) (* f64 h7 (* f64 h1 h8)))))
*-commutative_binary64_10580 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (neg f64 (neg f64 (* f64 h7 h4))) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (neg f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (* f64 (- f64 (* f64 h5 h7) (* f64 h0 h3)) h4))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (neg f64 (neg f64 (* f64 h7 h4))) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (neg f64 (neg f64 (* f64 h7 h4))) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (=> (neg f64 (neg f64 (* f64 h3 h8)))) (* f64 h2 h5)))) (* f64 h7 (* f64 h1 h8)))))
remove-double-neg_binary64_10637 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (neg f64 (neg f64 (* f64 h7 h4))) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (neg f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (* f64 (- f64 (* f64 h5 h7) (* f64 h0 h3)) h4))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (neg f64 (neg f64 (* f64 h7 h4))) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (=> (neg f64 (neg f64 (* f64 h7 h4)))) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h3 h8) (* f64 h2 h5)))) (* f64 h7 (* f64 h1 h8)))))
remove-double-neg_binary64_10637 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (neg f64 (neg f64 (* f64 h7 h4))) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (neg f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (* f64 (- f64 (* f64 h5 h7) (* f64 h0 h3)) h4))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (neg f64 (neg f64 (* f64 h7 h4))) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (=> (* f64 h7 h4)) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h3 h8) (* f64 h2 h5)))) (* f64 h7 (* f64 h1 h8)))))
*-commutative_binary64_10580 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (neg f64 (neg f64 (* f64 h7 h4))) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (neg f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (* f64 (- f64 (* f64 h5 h7) (* f64 h0 h3)) h4))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (=> (neg f64 (neg f64 (* f64 h7 h4)))) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h3 h8) (* f64 h2 h5)))) (* f64 h7 (* f64 h1 h8)))))
remove-double-neg_binary64_10637 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (neg f64 (neg f64 (* f64 h7 h4))) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (neg f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (* f64 (- f64 (* f64 h5 h7) (* f64 h0 h3)) h4))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (=> (* f64 h7 h4)) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h3 h8) (* f64 h2 h5)))) (* f64 h7 (* f64 h1 h8)))))
*-commutative_binary64_10580 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (=> (neg f64 (neg f64 (* f64 h7 h4)))) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (neg f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (* f64 (- f64 (* f64 h5 h7) (* f64 h0 h3)) h4))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h3 h8) (* f64 h2 h5)))) (* f64 h7 (* f64 h1 h8)))))
remove-double-neg_binary64_10637 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (=> (* f64 h7 h4)) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (neg f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (* f64 (- f64 (* f64 h5 h7) (* f64 h0 h3)) h4))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h3 h8) (* f64 h2 h5)))) (* f64 h7 (* f64 h1 h8)))))
*-commutative_binary64_10580 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (neg f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (* f64 (- f64 (* f64 h5 h7) (* f64 h0 h3)) h4))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h3 h8) (* f64 h2 h5)))) (* f64 h7 (* f64 h1 h8)))))
<= remove-double-neg_binary64_10637
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (neg f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (=> (* f64 (- f64 (* f64 h5 h7) (* f64 h0 h3)) (<= (neg f64 (neg f64 h4))))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h3 h8) (* f64 h2 h5)))) (* f64 h7 (* f64 h1 h8)))))
distribute-rgt-neg-out_binary64_10609 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (+ f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (=> (+ f64 (neg f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8)))) (neg f64 (* f64 (- f64 (* f64 h5 h7) (* f64 h0 h3)) (neg f64 h4)))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h3 h8) (* f64 h2 h5)))) (* f64 h7 (* f64 h1 h8)))))
distribute-neg-out_binary64_10611 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (=> (+ f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (neg f64 (+ f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8))) (* f64 (- f64 (* f64 h5 h7) (* f64 h0 h3)) (neg f64 h4)))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h3 h8) (* f64 h2 h5)))) (* f64 h7 (* f64 h1 h8)))))
unsub-neg_binary64_10643 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (- f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8))) (=> (* f64 (- f64 (* f64 h5 h7) (* f64 h0 h3)) (neg f64 h4))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h3 h8) (* f64 h2 h5)))) (* f64 h7 (* f64 h1 h8)))))
distribute-rgt-neg-out_binary64_10609 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (- f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8))) (neg f64 (* f64 (- f64 (* f64 h5 h7) (* f64 h0 h3)) h4)))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h3 h8) (* f64 h2 h5)))) (* f64 h7 (* f64 h1 h8)))))
<= *-commutative_binary64_10580
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (- f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8))) (=> (neg f64 (<= (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3)))))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h3 h8) (* f64 h2 h5)))) (* f64 h7 (* f64 h1 h8)))))
distribute-rgt-neg-in_binary64_10607 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (- f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8))) (* f64 h4 (neg f64 (=> (- f64 (* f64 h5 h7) (* f64 h0 h3))))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h3 h8) (* f64 h2 h5)))) (* f64 h7 (* f64 h1 h8)))))
sub-neg_binary64_10642 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (- f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8))) (* f64 h4 (neg f64 (+ f64 (* f64 h5 h7) (neg f64 (* f64 h0 h3))))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h3 h8) (* f64 h2 h5)))) (* f64 h7 (* f64 h1 h8)))))
<= remove-double-neg_binary64_10637
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (- f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8))) (* f64 h4 (neg f64 (+ f64 (=> (* f64 h5 (<= (neg f64 (neg f64 h7))))) (neg f64 (* f64 h0 h3))))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h3 h8) (* f64 h2 h5)))) (* f64 h7 (* f64 h1 h8)))))
distribute-rgt-neg-out_binary64_10609 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (- f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8))) (* f64 h4 (neg f64 (=> (+ f64 (neg f64 (* f64 h5 (neg f64 h7))) (neg f64 (* f64 h0 h3)))))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h3 h8) (* f64 h2 h5)))) (* f64 h7 (* f64 h1 h8)))))
distribute-neg-out_binary64_10611 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (- f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8))) (* f64 h4 (=> (neg f64 (neg f64 (+ f64 (* f64 h5 (neg f64 h7)) (* f64 h0 h3)))))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h3 h8) (* f64 h2 h5)))) (* f64 h7 (* f64 h1 h8)))))
remove-double-neg_binary64_10637 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (- f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8))) (* f64 h4 (+ f64 (* f64 h5 (neg f64 h7)) (* f64 h0 h3))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h3 h8) (* f64 h2 h5)))) (* f64 h7 (* f64 h1 h8)))))
<= remove-double-neg_binary64_10637
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (- f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8))) (* f64 h4 (<= (neg f64 (neg f64 (+ f64 (* f64 h5 (neg f64 h7)) (* f64 h0 h3)))))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h3 h8) (* f64 h2 h5)))) (* f64 h7 (* f64 h1 h8)))))
<= distribute-neg-out_binary64_10611
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (- f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8))) (* f64 h4 (neg f64 (<= (+ f64 (neg f64 (* f64 h5 (neg f64 h7))) (neg f64 (* f64 h0 h3)))))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h3 h8) (* f64 h2 h5)))) (* f64 h7 (* f64 h1 h8)))))
<= distribute-rgt-neg-out_binary64_10609
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (- f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8))) (* f64 h4 (neg f64 (+ f64 (<= (* f64 h5 (=> (neg f64 (neg f64 h7))))) (neg f64 (* f64 h0 h3))))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h3 h8) (* f64 h2 h5)))) (* f64 h7 (* f64 h1 h8)))))
remove-double-neg_binary64_10637 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (- f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8))) (* f64 h4 (neg f64 (+ f64 (* f64 h5 h7) (neg f64 (* f64 h0 h3))))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h3 h8) (* f64 h2 h5)))) (* f64 h7 (* f64 h1 h8)))))
<= sub-neg_binary64_10642
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (- f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8))) (* f64 h4 (neg f64 (<= (=> (- f64 (* f64 h5 h7) (* f64 h0 h3)))))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h3 h8) (* f64 h2 h5)))) (* f64 h7 (* f64 h1 h8)))))
sub-neg_binary64_10642 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (- f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8))) (* f64 h4 (neg f64 (=> (+ f64 (* f64 h5 h7) (neg f64 (* f64 h0 h3)))))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h3 h8) (* f64 h2 h5)))) (* f64 h7 (* f64 h1 h8)))))
+-commutative_binary64_10579 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (- f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8))) (* f64 h4 (neg f64 (+ f64 (neg f64 (* f64 h0 h3)) (* f64 h5 h7)))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h3 h8) (* f64 h2 h5)))) (* f64 h7 (* f64 h1 h8)))))
<= remove-double-neg_binary64_10637
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (- f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8))) (* f64 h4 (neg f64 (+ f64 (neg f64 (* f64 h0 h3)) (=> (* f64 h5 (<= (neg f64 (neg f64 h7)))))))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h3 h8) (* f64 h2 h5)))) (* f64 h7 (* f64 h1 h8)))))
distribute-rgt-neg-out_binary64_10609 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (- f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8))) (* f64 h4 (neg f64 (=> (+ f64 (neg f64 (* f64 h0 h3)) (neg f64 (* f64 h5 (neg f64 h7))))))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h3 h8) (* f64 h2 h5)))) (* f64 h7 (* f64 h1 h8)))))
distribute-neg-out_binary64_10611 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (- f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8))) (* f64 h4 (=> (neg f64 (neg f64 (+ f64 (* f64 h0 h3) (* f64 h5 (neg f64 h7))))))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h3 h8) (* f64 h2 h5)))) (* f64 h7 (* f64 h1 h8)))))
remove-double-neg_binary64_10637 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (- f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8))) (* f64 h4 (+ f64 (* f64 h0 h3) (=> (* f64 h5 (neg f64 h7))))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h3 h8) (* f64 h2 h5)))) (* f64 h7 (* f64 h1 h8)))))
distribute-rgt-neg-out_binary64_10609 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (- f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8))) (* f64 h4 (=> (+ f64 (* f64 h0 h3) (neg f64 (* f64 h5 h7))))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h3 h8) (* f64 h2 h5)))) (* f64 h7 (* f64 h1 h8)))))
unsub-neg_binary64_10643 =>
(if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) -54409881749699667053054092614590830909685277203216228405467069933997486154794360136103767084649971643555469392987760709821777615840059660823853216547384957034655046203911980699739802408177442833435573770734559377044559422685906974255057012400771956539610729412323647029253173659394114419830312586793833201664) (- f64 (* f64 h1 (- f64 (* f64 h0 h2) (* f64 h7 h8))) (+ f64 (* f64 h6 (- f64 (* f64 h2 h5) (* f64 h3 h8))) (* f64 h4 (- f64 (* f64 h0 h3) (* f64 h5 h7))))) (if real (<= f64 (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) 20173770445973815021804770554628269455745749194577755410748554532054434833351716509203835176552402692368868064307096201110408542009366599729692944385429627575628394025954896444366854007449992890325257416571842143303028043768610540777615888858729452452286054134160897417321375904873364547245096662783229952) (+ f64 (+ f64 (* f64 h0 (- f64 (* f64 h1 h2) (* f64 h3 h4))) (* f64 h5 (- f64 (* f64 h4 h7) (* f64 h2 h6)))) (* f64 h8 (- f64 (* f64 h3 h6) (* f64 h1 h7)))) (- f64 (+ f64 (* f64 h4 (- f64 (* f64 h5 h7) (* f64 h0 h3))) (* f64 h6 (- f64 (* f64 h3 h8) (* f64 h2 h5)))) (* f64 h7 (* f64 h1 h8)))))

end0.0ms (0%)

sample4.5s (19%)

Algorithm

1×

intervals

Results

849.0ms	10989×	body	128	invalid
588.0ms	8000×	body	128	valid

Compiler

Compiled 3840 to 2589 computations (32.6% saved)

Details

analyze2.0s (8.3%)

sample94.0ms (0.4%)

simplify601.0ms (2.5%)

prune10.0ms (0%)

localize25.0ms (0.1%)

rewrite161.0ms (0.7%)

series1.7s (7%)

simplify273.0ms (1.1%)

prune605.0ms (2.5%)

localize21.0ms (0.1%)

rewrite148.0ms (0.6%)

series1.6s (6.6%)

simplify236.0ms (1%)

prune329.0ms (1.4%)

localize30.0ms (0.1%)

rewrite126.0ms (0.5%)

series2.9s (12%)

simplify484.0ms (2%)

prune671.0ms (2.8%)

localize25.0ms (0.1%)

rewrite195.0ms (0.8%)

series2.4s (10%)

simplify464.0ms (1.9%)

prune393.0ms (1.6%)

regimes3.8s (15.9%)

bsearch9.0ms (0%)

simplify170.0ms (0.7%)

end0.0ms (0%)

sample4.5s (19%)

Profiling