Details

Time bar (total: 34.8s)

analyze3.9s (11.2%)

Algorithm
search
Search
TrueOtherFalseIter
0%99.7%0.3%0
0%99.7%0.3%1
0%99.7%0.3%2
0%99.7%0.3%3
0%99.7%0.3%4
0%99.7%0.3%5
0%99.7%0.3%6
0%98.1%1.9%7
0%98.1%1.9%8
0%97.8%2.2%9
0%96.8%3.2%10
0%96.3%3.7%11
0%94.3%5.7%12
0.4%92.1%7.5%13
0.6%90.8%8.6%14
Compiler

Compiled 29 to 24 computations (17.2% saved)

sample456.0ms (1.3%)

Algorithm
intervals
Results
289.0ms425×body128nan
61.0ms256×body128valid
5.0ms44×body128invalid
Compiler

Compiled 57 to 53 computations (7% saved)

simplify467.0ms (1.3%)

Algorithm
egg-herbie
Rules
450×associate-/l*_binary64_364
385×distribute-rgt-neg-out_binary64_379
361×unsub-neg_binary64_413
360×cancel-sign-sub-inv_binary64_385
356×distribute-lft-neg-out_binary64_378
323×distribute-neg-frac_binary64_383
282×distribute-rgt-in_binary64_369
276×distribute-lft-in_binary64_368
264×associate-*r/_binary64_361
259×associate-*l/_binary64_362
237×distribute-rgt-neg-in_binary64_377
214×associate-/r/_binary64_365
208×times-frac_binary64_425
195×distribute-lft-neg-in_binary64_376
185×*-commutative_binary64_350
151×neg-sub0_binary64_414
145×neg-mul-1_binary64_415
117×distribute-neg-in_binary64_380
94×associate-/l/_binary64_366 associate-*r*_binary64_359
90×associate-*l*_binary64_360
89×sub-neg_binary64_412
84×distribute-neg-out_binary64_381
37×associate-+r+_binary64_351
34×remove-double-neg_binary64_407
30×distribute-rgt-out_binary64_372 distribute-lft-out_binary64_370
29×associate-+l+_binary64_352
27×div-sub_binary64_424
23×mul0-rgt_binary64_402 mul0-lft_binary64_401
20×associate--r+_binary64_355
19×+-commutative_binary64_349
16×associate-+l-_binary64_354 associate-+r-_binary64_353
13×distribute-rgt-out--_binary64_373
11×unswap-sqr_binary64_387 distribute-lft-out--_binary64_371
10×associate-/r*_binary64_363
sub0-neg_binary64_406
sqr-pow_binary64_391
associate--l+_binary64_356
+-rgt-identity_binary64_404 associate--r-_binary64_358
pow-plus_binary64_482 associate--l-_binary64_357
cube-unmult_binary64_456 --rgt-identity_binary64_405 pow-sqr_binary64_392
/-rgt-identity_binary64_410
div0_binary64_400 swap-sqr_binary64_386 distribute-rgt1-in_binary64_375
unpow2_binary64_484 unpow1_binary64_477 div-exp_binary64_470 rec-exp_binary64_469 prod-exp_binary64_468 1-exp_binary64_463 *-rgt-identity_binary64_409 *-inverses_binary64_399 rgt-mult-inverse_binary64_396 cancel-sign-sub_binary64_384 distribute-frac-neg_binary64_382 distribute-lft1-in_binary64_374 count-2_binary64_367
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_682 erf-erfc_binary64_681 erf-odd_binary64_680 if-if-and-not_binary64_679 if-if-and_binary64_678 if-if-or-not_binary64_677 if-if-or_binary64_676 if-not_binary64_675 if-same_binary64_674 if-false_binary64_673 if-true_binary64_672 not-gte_binary64_671 not-lte_binary64_670 not-gt_binary64_669 not-lt_binary64_668 gte-same_binary64_667 lte-same_binary64_666 gt-same_binary64_665 lt-same_binary64_664 sinh---cosh_binary64_611 sinh-+-cosh_binary64_610 sinh-cosh_binary64_609 tanh-def-c_binary64_608 tanh-def-b_binary64_607 tanh-def-a_binary64_606 cosh-def_binary64_605 sinh-def_binary64_604 tan-neg_binary64_551 cos-neg_binary64_550 sin-neg_binary64_549 tan-0_binary64_548 cos-0_binary64_547 sin-0_binary64_546 hang-m-tan_binary64_545 hang-p-tan_binary64_544 hang-m0-tan_binary64_543 hang-p0-tan_binary64_542 hang-0m-tan_binary64_541 hang-0p-tan_binary64_540 tan-+PI/2_binary64_539 tan-+PI_binary64_538 tan-PI_binary64_537 tan-PI/3_binary64_536 tan-PI/4_binary64_535 tan-PI/6_binary64_534 cos-+PI/2_binary64_533 cos-+PI_binary64_532 cos-PI_binary64_531 cos-PI/2_binary64_530 cos-PI/3_binary64_529 cos-PI/4_binary64_528 cos-PI/6_binary64_527 sin-+PI/2_binary64_526 sin-+PI_binary64_525 sin-PI_binary64_524 sin-PI/2_binary64_523 sin-PI/3_binary64_522 sin-PI/4_binary64_521 sin-PI/6_binary64_520 sub-1-sin_binary64_519 sub-1-cos_binary64_518 -1-add-sin_binary64_517 -1-add-cos_binary64_516 1-sub-sin_binary64_515 1-sub-cos_binary64_514 cos-sin-sum_binary64_513 log-E_binary64_509 log-pow_binary64_508 log-rec_binary64_507 log-div_binary64_506 log-prod_binary64_505 pow-base-0_binary64_503 unpow1/3_binary64_486 unpow3_binary64_485 unpow1/2_binary64_483 exp-to-pow_binary64_481 pow-base-1_binary64_479 unpow0_binary64_478 unpow-1_binary64_476 exp-lft-cube_binary64_475 exp-lft-sqr_binary64_474 exp-cbrt_binary64_473 exp-sqrt_binary64_472 exp-prod_binary64_471 exp-diff_binary64_467 exp-neg_binary64_466 exp-sum_binary64_465 e-exp-1_binary64_464 exp-1-e_binary64_462 exp-0_binary64_461 rem-log-exp_binary64_460 rem-exp-log_binary64_459 cube-mult_binary64_449 cube-div_binary64_448 cube-prod_binary64_447 cube-neg_binary64_446 rem-3cbrt-rft_binary64_445 rem-3cbrt-lft_binary64_444 rem-cbrt-cube_binary64_443 rem-cube-cbrt_binary64_442 sqr-abs_binary64_434 sqr-neg_binary64_433 rem-sqrt-square_binary64_432 rem-square-sqrt_binary64_431 mul-1-neg_binary64_411 *-lft-identity_binary64_408 +-lft-identity_binary64_403 +-inverses_binary64_398 lft-mult-inverse_binary64_397 remove-double-div_binary64_395 difference-of-sqr--1_binary64_390 difference-of-sqr-1_binary64_389 difference-of-squares_binary64_388
Counts
1 → 5
Iterations

Useful iterations: 3 (0.0ms)

IterNodesCost
02242
15642
218742
374039
4274639

prune11.0ms (0%)

Pruning

3 alts after pruning (3 fresh and 0 done)

PrunedKeptTotal
New325
Fresh011
Picked000
Done000
Total336
Error
28.2b
Counts
6 → 3
Compiler

Compiled 218 to 141 computations (35.3% saved)

localize17.0ms (0%)

Local error

Found 4 expressions with local error:

5.0b
(*.f64 n (/.f64 l Om))
6.0b
(*.f64 U (*.f64 (*.f64 2 n) (-.f64 t (*.f64 (/.f64 l Om) (-.f64 (*.f64 2 l) (*.f64 (-.f64 U* U) (*.f64 n (/.f64 l Om))))))))
8.2b
(*.f64 (-.f64 U* U) (*.f64 n (/.f64 l Om)))
21.5b
(sqrt.f64 (*.f64 U (*.f64 (*.f64 2 n) (-.f64 t (*.f64 (/.f64 l Om) (-.f64 (*.f64 2 l) (*.f64 (-.f64 U* U) (*.f64 n (/.f64 l Om)))))))))

rewrite702.0ms (2%)

Algorithm
rewrite-expression-head
Error
23.3b
Rules
30×pow1_binary64_480
27×add-exp-log_binary64_457 add-cbrt-cube_binary64_455
21×add-sqr-sqrt_binary64_441
16×pow-prod-down_binary64_490 *-un-lft-identity_binary64_419
15×associate-*r*_binary64_359
14×add-cube-cbrt_binary64_454
13×associate-*r/_binary64_361 prod-exp_binary64_468 cbrt-unprod_binary64_452
11×associate-*l*_binary64_360
10×times-frac_binary64_425
distribute-rgt-in_binary64_369 distribute-lft-in_binary64_368
add-log-exp_binary64_458 sqrt-pow1_binary64_437 flip3--_binary64_423 flip--_binary64_394 sub-neg_binary64_412 cancel-sign-sub-inv_binary64_385
*-commutative_binary64_350
sqrt-div_binary64_436 div-exp_binary64_470 cbrt-undiv_binary64_453 frac-times_binary64_429 associate-*l/_binary64_362 unswap-sqr_binary64_387
pow1/2_binary64_499 sqrt-prod_binary64_435 difference-of-squares_binary64_388 distribute-lft-out--_binary64_371 div-inv_binary64_416
Counts
4 → 105
Calls

4 calls:

32.0ms
(sqrt.f64 (*.f64 U (*.f64 (*.f64 2 n) (-.f64 t (*.f64 (/.f64 l Om) (-.f64 (*.f64 2 l) (*.f64 (-.f64 U* U) (*.f64 n (/.f64 l Om)))))))))
9.0ms
(*.f64 (-.f64 U* U) (*.f64 n (/.f64 l Om)))
8.0ms
(*.f64 U (*.f64 (*.f64 2 n) (-.f64 t (*.f64 (/.f64 l Om) (-.f64 (*.f64 2 l) (*.f64 (-.f64 U* U) (*.f64 n (/.f64 l Om))))))))
6.0ms
(*.f64 n (/.f64 l Om))
Compiler

Compiled 3926 to 1618 computations (58.8% saved)

series3.1s (8.9%)

Error
20.9b
Counts
4 → 94
Calls

4 calls:

1.8s
(sqrt.f64 (*.f64 U (*.f64 (*.f64 2 n) (-.f64 t (*.f64 (/.f64 l Om) (-.f64 (*.f64 2 l) (*.f64 (-.f64 U* U) (*.f64 n (/.f64 l Om)))))))))
1.0s
(*.f64 U (*.f64 (*.f64 2 n) (-.f64 t (*.f64 (/.f64 l Om) (-.f64 (*.f64 2 l) (*.f64 (-.f64 U* U) (*.f64 n (/.f64 l Om))))))))
126.0ms
(*.f64 (-.f64 U* U) (*.f64 n (/.f64 l Om)))
50.0ms
(*.f64 n (/.f64 l Om))
Compiler

Compiled 11079 to 8316 computations (24.9% saved)

simplify806.0ms (2.3%)

Algorithm
egg-herbie
Rules
687×associate-*r*_binary64_359
664×associate-*l*_binary64_360
296×associate-/l*_binary64_364
239×times-frac_binary64_425
196×associate-*r/_binary64_361
192×*-commutative_binary64_350
176×associate-*l/_binary64_362
153×associate-/r*_binary64_363
84×cancel-sign-sub-inv_binary64_385
72×distribute-rgt-in_binary64_369
67×distribute-lft-in_binary64_368
61×sub-neg_binary64_412
60×distribute-rgt-neg-in_binary64_377
56×associate-/r/_binary64_365
49×neg-sub0_binary64_414
44×associate-/l/_binary64_366
43×neg-mul-1_binary64_415
41×distribute-lft-neg-in_binary64_376
33×sqr-pow_binary64_391
27×+-commutative_binary64_349
24×distribute-lft-neg-out_binary64_378
23×unswap-sqr_binary64_387
18×distribute-neg-frac_binary64_383
17×swap-sqr_binary64_386
16×distribute-neg-in_binary64_380
11×log-prod_binary64_505 exp-prod_binary64_471
10×unpow3_binary64_485 cube-unmult_binary64_456 mul-1-neg_binary64_411
cube-mult_binary64_449 div-sub_binary64_424 pow-sqr_binary64_392
distribute-rgt-out_binary64_372 associate--l+_binary64_356 associate--r+_binary64_355
distribute-rgt-neg-out_binary64_379 distribute-lft-out--_binary64_371 associate-+r+_binary64_351
difference-of-squares_binary64_388
unpow2_binary64_484 pow-plus_binary64_482
log-div_binary64_506 cube-prod_binary64_447
cube-div_binary64_448 /-rgt-identity_binary64_410 distribute-rgt-out--_binary64_373 distribute-lft-out_binary64_370
*-rgt-identity_binary64_409
div-exp_binary64_470 rec-exp_binary64_469 exp-diff_binary64_467 exp-sum_binary64_465 1-exp_binary64_463 rem-sqrt-square_binary64_432 rem-square-sqrt_binary64_431 unsub-neg_binary64_413 *-inverses_binary64_399 associate-+r-_binary64_353 associate-+l+_binary64_352
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_682 erf-erfc_binary64_681 erf-odd_binary64_680 if-if-and-not_binary64_679 if-if-and_binary64_678 if-if-or-not_binary64_677 if-if-or_binary64_676 if-not_binary64_675 if-same_binary64_674 if-false_binary64_673 if-true_binary64_672 not-gte_binary64_671 not-lte_binary64_670 not-gt_binary64_669 not-lt_binary64_668 gte-same_binary64_667 lte-same_binary64_666 gt-same_binary64_665 lt-same_binary64_664 sinh---cosh_binary64_611 sinh-+-cosh_binary64_610 sinh-cosh_binary64_609 tanh-def-c_binary64_608 tanh-def-b_binary64_607 tanh-def-a_binary64_606 cosh-def_binary64_605 sinh-def_binary64_604 tan-neg_binary64_551 cos-neg_binary64_550 sin-neg_binary64_549 tan-0_binary64_548 cos-0_binary64_547 sin-0_binary64_546 hang-m-tan_binary64_545 hang-p-tan_binary64_544 hang-m0-tan_binary64_543 hang-p0-tan_binary64_542 hang-0m-tan_binary64_541 hang-0p-tan_binary64_540 tan-+PI/2_binary64_539 tan-+PI_binary64_538 tan-PI_binary64_537 tan-PI/3_binary64_536 tan-PI/4_binary64_535 tan-PI/6_binary64_534 cos-+PI/2_binary64_533 cos-+PI_binary64_532 cos-PI_binary64_531 cos-PI/2_binary64_530 cos-PI/3_binary64_529 cos-PI/4_binary64_528 cos-PI/6_binary64_527 sin-+PI/2_binary64_526 sin-+PI_binary64_525 sin-PI_binary64_524 sin-PI/2_binary64_523 sin-PI/3_binary64_522 sin-PI/4_binary64_521 sin-PI/6_binary64_520 sub-1-sin_binary64_519 sub-1-cos_binary64_518 -1-add-sin_binary64_517 -1-add-cos_binary64_516 1-sub-sin_binary64_515 1-sub-cos_binary64_514 cos-sin-sum_binary64_513 log-E_binary64_509 log-pow_binary64_508 log-rec_binary64_507 pow-base-0_binary64_503 unpow1/3_binary64_486 unpow1/2_binary64_483 exp-to-pow_binary64_481 pow-base-1_binary64_479 unpow0_binary64_478 unpow1_binary64_477 unpow-1_binary64_476 exp-lft-cube_binary64_475 exp-lft-sqr_binary64_474 exp-cbrt_binary64_473 exp-sqrt_binary64_472 prod-exp_binary64_468 exp-neg_binary64_466 e-exp-1_binary64_464 exp-1-e_binary64_462 exp-0_binary64_461 rem-log-exp_binary64_460 rem-exp-log_binary64_459 cube-neg_binary64_446 rem-3cbrt-rft_binary64_445 rem-3cbrt-lft_binary64_444 rem-cbrt-cube_binary64_443 rem-cube-cbrt_binary64_442 sqr-abs_binary64_434 sqr-neg_binary64_433 *-lft-identity_binary64_408 remove-double-neg_binary64_407 sub0-neg_binary64_406 --rgt-identity_binary64_405 +-rgt-identity_binary64_404 +-lft-identity_binary64_403 mul0-rgt_binary64_402 mul0-lft_binary64_401 div0_binary64_400 +-inverses_binary64_398 lft-mult-inverse_binary64_397 rgt-mult-inverse_binary64_396 remove-double-div_binary64_395 difference-of-sqr--1_binary64_390 difference-of-sqr-1_binary64_389 cancel-sign-sub_binary64_384 distribute-frac-neg_binary64_382 distribute-neg-out_binary64_381 distribute-rgt1-in_binary64_375 distribute-lft1-in_binary64_374 count-2_binary64_367 associate--r-_binary64_358 associate--l-_binary64_357 associate-+l-_binary64_354
Counts
199 → 433
Iterations

Useful iterations: 1 (0.0ms)

IterNodesCost
04817371
113316761

prune425.0ms (1.2%)

Pruning

28 alts after pruning (27 fresh and 1 done)

PrunedKeptTotal
New40726433
Fresh112
Picked011
Done000
Total40828436
Error
13.0b
Counts
436 → 28
Compiler

Compiled 18346 to 7028 computations (61.7% saved)

localize25.0ms (0.1%)

Local error

Found 4 expressions with local error:

6.1b
(/.f64 (*.f64 n l) Om)
6.9b
(*.f64 U (*.f64 (*.f64 (*.f64 n 2) (/.f64 (neg.f64 l) Om)) (-.f64 (*.f64 2 l) (*.f64 (-.f64 U* U) (/.f64 (*.f64 n l) Om)))))
8.2b
(*.f64 (-.f64 U* U) (/.f64 (*.f64 n l) Om))
21.5b
(sqrt.f64 (+.f64 (*.f64 (*.f64 t (*.f64 2 n)) U) (*.f64 U (*.f64 (*.f64 (*.f64 n 2) (/.f64 (neg.f64 l) Om)) (-.f64 (*.f64 2 l) (*.f64 (-.f64 U* U) (/.f64 (*.f64 n l) Om)))))))

rewrite159.0ms (0.5%)

Algorithm
rewrite-expression-head
Error
12.3b
Rules
43×add-exp-log_binary64_457 add-cbrt-cube_binary64_455
22×prod-exp_binary64_468 cbrt-unprod_binary64_452
21×pow1_binary64_480
16×add-sqr-sqrt_binary64_441
13×*-un-lft-identity_binary64_419
11×add-cube-cbrt_binary64_454 pow-prod-down_binary64_490 associate-*r/_binary64_361
associate-*l*_binary64_360 associate-*r*_binary64_359 distribute-rgt-in_binary64_369 distribute-lft-in_binary64_368
div-exp_binary64_470 cbrt-undiv_binary64_453 times-frac_binary64_425
add-log-exp_binary64_458 flip3--_binary64_423 frac-times_binary64_429 flip--_binary64_394 sub-neg_binary64_412 cancel-sign-sub-inv_binary64_385
sqrt-prod_binary64_435 associate-*l/_binary64_362 associate-/r*_binary64_363
sqrt-div_binary64_436 div-inv_binary64_416 *-commutative_binary64_350 distribute-rgt-neg-out_binary64_379
pow1/2_binary64_499 sqrt-pow1_binary64_437 flip3-+_binary64_422 flip-+_binary64_393 rem-sqrt-square_binary64_432 unswap-sqr_binary64_387 difference-of-squares_binary64_388 distribute-lft-out--_binary64_371 distribute-frac-neg_binary64_382 distribute-lft-neg-out_binary64_378 frac-2neg_binary64_430 clear-num_binary64_418 associate-/l*_binary64_364
Counts
4 → 111
Calls

4 calls:

16.0ms
(*.f64 U (*.f64 (*.f64 (*.f64 n 2) (/.f64 (neg.f64 l) Om)) (-.f64 (*.f64 2 l) (*.f64 (-.f64 U* U) (/.f64 (*.f64 n l) Om)))))
11.0ms
(*.f64 (-.f64 U* U) (/.f64 (*.f64 n l) Om))
6.0ms
(sqrt.f64 (+.f64 (*.f64 (*.f64 t (*.f64 2 n)) U) (*.f64 U (*.f64 (*.f64 (*.f64 n 2) (/.f64 (neg.f64 l) Om)) (-.f64 (*.f64 2 l) (*.f64 (-.f64 U* U) (/.f64 (*.f64 n l) Om)))))))
5.0ms
(/.f64 (*.f64 n l) Om)
Compiler

Compiled 5254 to 2259 computations (57% saved)

series1.4s (4%)

Error
10.8b
Counts
4 → 80
Calls

4 calls:

616.0ms
(*.f64 U (*.f64 (*.f64 (*.f64 n 2) (/.f64 (neg.f64 l) Om)) (-.f64 (*.f64 2 l) (*.f64 (-.f64 U* U) (/.f64 (*.f64 n l) Om)))))
484.0ms
(sqrt.f64 (+.f64 (*.f64 (*.f64 t (*.f64 2 n)) U) (*.f64 U (*.f64 (*.f64 (*.f64 n 2) (/.f64 (neg.f64 l) Om)) (-.f64 (*.f64 2 l) (*.f64 (-.f64 U* U) (/.f64 (*.f64 n l) Om)))))))
163.0ms
(*.f64 (-.f64 U* U) (/.f64 (*.f64 n l) Om))
50.0ms
(/.f64 (*.f64 n l) Om)
Compiler

Compiled 9492 to 7003 computations (26.2% saved)

simplify644.0ms (1.9%)

Algorithm
egg-herbie
Rules
731×associate-*l*_binary64_360
287×associate-/l*_binary64_364
228×times-frac_binary64_425
219×associate-*r/_binary64_361
199×associate-*l/_binary64_362
167×*-commutative_binary64_350
142×associate-/r*_binary64_363
95×associate-*r*_binary64_359
88×cancel-sign-sub-inv_binary64_385
86×distribute-rgt-in_binary64_369
83×distribute-lft-in_binary64_368
69×distribute-rgt-neg-in_binary64_377
65×distribute-rgt-neg-out_binary64_379
63×sub-neg_binary64_412
61×distribute-lft-neg-out_binary64_378
53×neg-sub0_binary64_414
52×distribute-lft-neg-in_binary64_376
48×neg-mul-1_binary64_415
46×associate-/r/_binary64_365
42×unswap-sqr_binary64_387
33×associate-/l/_binary64_366
30×sqr-pow_binary64_391
27×swap-sqr_binary64_386
25×distribute-neg-frac_binary64_383
24×distribute-frac-neg_binary64_382
21×+-commutative_binary64_349
17×cube-prod_binary64_447
13×unpow3_binary64_485
12×log-prod_binary64_505
11×pow-sqr_binary64_392
10×log-div_binary64_506 div-sub_binary64_424 distribute-neg-in_binary64_380
distribute-lft-out--_binary64_371
cube-unmult_binary64_456 cube-mult_binary64_449
exp-prod_binary64_471 mul-1-neg_binary64_411 distribute-rgt-out--_binary64_373
cube-div_binary64_448 difference-of-squares_binary64_388 associate--r+_binary64_355
associate--l+_binary64_356
unpow2_binary64_484 pow-plus_binary64_482 distribute-rgt-out_binary64_372
associate-+r-_binary64_353
exp-diff_binary64_467 exp-sum_binary64_465 sqr-neg_binary64_433 rem-sqrt-square_binary64_432 /-rgt-identity_binary64_410 associate-+l+_binary64_352 associate-+r+_binary64_351
1-exp_binary64_463 rem-square-sqrt_binary64_431 *-rgt-identity_binary64_409 *-lft-identity_binary64_408 *-inverses_binary64_399 distribute-lft-out_binary64_370
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_682 erf-erfc_binary64_681 erf-odd_binary64_680 if-if-and-not_binary64_679 if-if-and_binary64_678 if-if-or-not_binary64_677 if-if-or_binary64_676 if-not_binary64_675 if-same_binary64_674 if-false_binary64_673 if-true_binary64_672 not-gte_binary64_671 not-lte_binary64_670 not-gt_binary64_669 not-lt_binary64_668 gte-same_binary64_667 lte-same_binary64_666 gt-same_binary64_665 lt-same_binary64_664 sinh---cosh_binary64_611 sinh-+-cosh_binary64_610 sinh-cosh_binary64_609 tanh-def-c_binary64_608 tanh-def-b_binary64_607 tanh-def-a_binary64_606 cosh-def_binary64_605 sinh-def_binary64_604 tan-neg_binary64_551 cos-neg_binary64_550 sin-neg_binary64_549 tan-0_binary64_548 cos-0_binary64_547 sin-0_binary64_546 hang-m-tan_binary64_545 hang-p-tan_binary64_544 hang-m0-tan_binary64_543 hang-p0-tan_binary64_542 hang-0m-tan_binary64_541 hang-0p-tan_binary64_540 tan-+PI/2_binary64_539 tan-+PI_binary64_538 tan-PI_binary64_537 tan-PI/3_binary64_536 tan-PI/4_binary64_535 tan-PI/6_binary64_534 cos-+PI/2_binary64_533 cos-+PI_binary64_532 cos-PI_binary64_531 cos-PI/2_binary64_530 cos-PI/3_binary64_529 cos-PI/4_binary64_528 cos-PI/6_binary64_527 sin-+PI/2_binary64_526 sin-+PI_binary64_525 sin-PI_binary64_524 sin-PI/2_binary64_523 sin-PI/3_binary64_522 sin-PI/4_binary64_521 sin-PI/6_binary64_520 sub-1-sin_binary64_519 sub-1-cos_binary64_518 -1-add-sin_binary64_517 -1-add-cos_binary64_516 1-sub-sin_binary64_515 1-sub-cos_binary64_514 cos-sin-sum_binary64_513 log-E_binary64_509 log-pow_binary64_508 log-rec_binary64_507 pow-base-0_binary64_503 unpow1/3_binary64_486 unpow1/2_binary64_483 exp-to-pow_binary64_481 pow-base-1_binary64_479 unpow0_binary64_478 unpow1_binary64_477 unpow-1_binary64_476 exp-lft-cube_binary64_475 exp-lft-sqr_binary64_474 exp-cbrt_binary64_473 exp-sqrt_binary64_472 div-exp_binary64_470 rec-exp_binary64_469 prod-exp_binary64_468 exp-neg_binary64_466 e-exp-1_binary64_464 exp-1-e_binary64_462 exp-0_binary64_461 rem-log-exp_binary64_460 rem-exp-log_binary64_459 cube-neg_binary64_446 rem-3cbrt-rft_binary64_445 rem-3cbrt-lft_binary64_444 rem-cbrt-cube_binary64_443 rem-cube-cbrt_binary64_442 sqr-abs_binary64_434 unsub-neg_binary64_413 remove-double-neg_binary64_407 sub0-neg_binary64_406 --rgt-identity_binary64_405 +-rgt-identity_binary64_404 +-lft-identity_binary64_403 mul0-rgt_binary64_402 mul0-lft_binary64_401 div0_binary64_400 +-inverses_binary64_398 lft-mult-inverse_binary64_397 rgt-mult-inverse_binary64_396 remove-double-div_binary64_395 difference-of-sqr--1_binary64_390 difference-of-sqr-1_binary64_389 cancel-sign-sub_binary64_384 distribute-neg-out_binary64_381 distribute-rgt1-in_binary64_375 distribute-lft1-in_binary64_374 count-2_binary64_367 associate--r-_binary64_358 associate--l-_binary64_357 associate-+l-_binary64_354
Counts
191 → 467
Iterations

Useful iterations: 1 (0.0ms)

IterNodesCost
04566495
112926066

prune515.0ms (1.5%)

Pruning

29 alts after pruning (28 fresh and 1 done)

PrunedKeptTotal
New45512467
Fresh101626
Picked101
Done011
Total46629495
Error
9.6b
Counts
495 → 29
Compiler

Compiled 22419 to 9504 computations (57.6% saved)

localize20.0ms (0.1%)

Local error

Found 4 expressions with local error:

5.0b
(/.f64 Om (*.f64 n (*.f64 l U)))
5.1b
(/.f64 Om (*.f64 l U))
6.9b
(/.f64 n (/.f64 Om (*.f64 l U)))
16.4b
(sqrt.f64 (+.f64 (*.f64 (*.f64 t (*.f64 2 n)) U) (*.f64 -2 (/.f64 (+.f64 (/.f64 n (/.f64 Om (*.f64 l U))) (*.f64 2 l)) (/.f64 Om (*.f64 n (*.f64 l U)))))))

rewrite116.0ms (0.3%)

Algorithm
rewrite-expression-head
Error
9.6b
Rules
39×times-frac_binary64_425
27×add-exp-log_binary64_457 add-cbrt-cube_binary64_455
26×add-sqr-sqrt_binary64_441
25×add-cube-cbrt_binary64_454 *-un-lft-identity_binary64_419
10×div-exp_binary64_470 cbrt-undiv_binary64_453
associate-/l*_binary64_364 associate-/r*_binary64_363
div-inv_binary64_416
pow1_binary64_480 prod-exp_binary64_468 cbrt-unprod_binary64_452
add-log-exp_binary64_458
sqrt-prod_binary64_435 frac-2neg_binary64_430 clear-num_binary64_418
sqrt-div_binary64_436
pow1/2_binary64_499 sqrt-pow1_binary64_437 flip3-+_binary64_422 flip-+_binary64_393 rem-sqrt-square_binary64_432 associate-/r/_binary64_365
Counts
4 → 107
Calls

4 calls:

8.0ms
(sqrt.f64 (+.f64 (*.f64 (*.f64 t (*.f64 2 n)) U) (*.f64 -2 (/.f64 (+.f64 (/.f64 n (/.f64 Om (*.f64 l U))) (*.f64 2 l)) (/.f64 Om (*.f64 n (*.f64 l U)))))))
7.0ms
(/.f64 Om (*.f64 n (*.f64 l U)))
6.0ms
(/.f64 n (/.f64 Om (*.f64 l U)))
4.0ms
(/.f64 Om (*.f64 l U))
Compiler

Compiled 4285 to 1791 computations (58.2% saved)

series559.0ms (1.6%)

Error
9.6b
Counts
4 → 53
Calls

4 calls:

283.0ms
(sqrt.f64 (+.f64 (*.f64 (*.f64 t (*.f64 2 n)) U) (*.f64 -2 (/.f64 (+.f64 (/.f64 n (/.f64 Om (*.f64 l U))) (*.f64 2 l)) (/.f64 Om (*.f64 n (*.f64 l U)))))))
98.0ms
(/.f64 Om (*.f64 n (*.f64 l U)))
87.0ms
(/.f64 n (/.f64 Om (*.f64 l U)))
54.0ms
(/.f64 Om (*.f64 l U))
Compiler

Compiled 5260 to 3758 computations (28.6% saved)

simplify486.0ms (1.4%)

Algorithm
egg-herbie
Rules
305×distribute-rgt-neg-in_binary64_377
276×associate-*r*_binary64_359
271×distribute-lft-neg-in_binary64_376
231×cancel-sign-sub-inv_binary64_385
223×associate-*l*_binary64_360
222×times-frac_binary64_425
194×associate-/l*_binary64_364
177×associate-/r*_binary64_363
160×distribute-neg-frac_binary64_383
129×*-commutative_binary64_350
127×associate-*l/_binary64_362
121×associate-/r/_binary64_365
101×associate-*r/_binary64_361
99×associate-/l/_binary64_366
98×distribute-rgt-in_binary64_369
96×unswap-sqr_binary64_387
89×neg-sub0_binary64_414
88×neg-mul-1_binary64_415
80×distribute-lft-in_binary64_368
77×sub-neg_binary64_412
64×sqr-pow_binary64_391
59×cube-prod_binary64_447
57×swap-sqr_binary64_386
52×log-div_binary64_506
49×unpow3_binary64_485 +-commutative_binary64_349
45×log-prod_binary64_505
41×distribute-lft-neg-out_binary64_378
37×*-rgt-identity_binary64_409
30×cube-div_binary64_448
28×associate-+r-_binary64_353
27×associate-+l-_binary64_354
25×distribute-neg-in_binary64_380
23×pow-sqr_binary64_392 associate--r+_binary64_355 associate-+l+_binary64_352
17×cube-mult_binary64_449 associate-+r+_binary64_351
16×div-sub_binary64_424
14×unsub-neg_binary64_413
13×distribute-rgt-out--_binary64_373 associate--l+_binary64_356
12×pow-plus_binary64_482 distribute-lft-out--_binary64_371
11×distribute-rgt-out_binary64_372 associate--r-_binary64_358
log-pow_binary64_508 div-exp_binary64_470 prod-exp_binary64_468 cube-unmult_binary64_456 /-rgt-identity_binary64_410
log-rec_binary64_507 exp-prod_binary64_471 *-lft-identity_binary64_408 distribute-rgt-neg-out_binary64_379 associate--l-_binary64_357
unpow2_binary64_484 unpow1_binary64_477
rem-sqrt-square_binary64_432 mul-1-neg_binary64_411 distribute-frac-neg_binary64_382
rec-exp_binary64_469
rem-square-sqrt_binary64_431 distribute-lft-out_binary64_370
1-exp_binary64_463 rem-log-exp_binary64_460 remove-double-neg_binary64_407 div0_binary64_400 *-inverses_binary64_399 remove-double-div_binary64_395 difference-of-squares_binary64_388
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_682 erf-erfc_binary64_681 erf-odd_binary64_680 if-if-and-not_binary64_679 if-if-and_binary64_678 if-if-or-not_binary64_677 if-if-or_binary64_676 if-not_binary64_675 if-same_binary64_674 if-false_binary64_673 if-true_binary64_672 not-gte_binary64_671 not-lte_binary64_670 not-gt_binary64_669 not-lt_binary64_668 gte-same_binary64_667 lte-same_binary64_666 gt-same_binary64_665 lt-same_binary64_664 sinh---cosh_binary64_611 sinh-+-cosh_binary64_610 sinh-cosh_binary64_609 tanh-def-c_binary64_608 tanh-def-b_binary64_607 tanh-def-a_binary64_606 cosh-def_binary64_605 sinh-def_binary64_604 tan-neg_binary64_551 cos-neg_binary64_550 sin-neg_binary64_549 tan-0_binary64_548 cos-0_binary64_547 sin-0_binary64_546 hang-m-tan_binary64_545 hang-p-tan_binary64_544 hang-m0-tan_binary64_543 hang-p0-tan_binary64_542 hang-0m-tan_binary64_541 hang-0p-tan_binary64_540 tan-+PI/2_binary64_539 tan-+PI_binary64_538 tan-PI_binary64_537 tan-PI/3_binary64_536 tan-PI/4_binary64_535 tan-PI/6_binary64_534 cos-+PI/2_binary64_533 cos-+PI_binary64_532 cos-PI_binary64_531 cos-PI/2_binary64_530 cos-PI/3_binary64_529 cos-PI/4_binary64_528 cos-PI/6_binary64_527 sin-+PI/2_binary64_526 sin-+PI_binary64_525 sin-PI_binary64_524 sin-PI/2_binary64_523 sin-PI/3_binary64_522 sin-PI/4_binary64_521 sin-PI/6_binary64_520 sub-1-sin_binary64_519 sub-1-cos_binary64_518 -1-add-sin_binary64_517 -1-add-cos_binary64_516 1-sub-sin_binary64_515 1-sub-cos_binary64_514 cos-sin-sum_binary64_513 log-E_binary64_509 pow-base-0_binary64_503 unpow1/3_binary64_486 unpow1/2_binary64_483 exp-to-pow_binary64_481 pow-base-1_binary64_479 unpow0_binary64_478 unpow-1_binary64_476 exp-lft-cube_binary64_475 exp-lft-sqr_binary64_474 exp-cbrt_binary64_473 exp-sqrt_binary64_472 exp-diff_binary64_467 exp-neg_binary64_466 exp-sum_binary64_465 e-exp-1_binary64_464 exp-1-e_binary64_462 exp-0_binary64_461 rem-exp-log_binary64_459 cube-neg_binary64_446 rem-3cbrt-rft_binary64_445 rem-3cbrt-lft_binary64_444 rem-cbrt-cube_binary64_443 rem-cube-cbrt_binary64_442 sqr-abs_binary64_434 sqr-neg_binary64_433 sub0-neg_binary64_406 --rgt-identity_binary64_405 +-rgt-identity_binary64_404 +-lft-identity_binary64_403 mul0-rgt_binary64_402 mul0-lft_binary64_401 +-inverses_binary64_398 lft-mult-inverse_binary64_397 rgt-mult-inverse_binary64_396 difference-of-sqr--1_binary64_390 difference-of-sqr-1_binary64_389 cancel-sign-sub_binary64_384 distribute-neg-out_binary64_381 distribute-rgt1-in_binary64_375 distribute-lft1-in_binary64_374 count-2_binary64_367
Counts
160 → 567
Iterations

Useful iterations: 2 (0.0ms)

IterNodesCost
02883582
17553309
232763201
349573201

prune562.0ms (1.6%)

Pruning

30 alts after pruning (28 fresh and 2 done)

PrunedKeptTotal
New5652567
Fresh12627
Picked011
Done011
Total56630596
Error
9.3b
Counts
596 → 30
Compiler

Compiled 25279 to 10265 computations (59.4% saved)

localize28.0ms (0.1%)

Local error

Found 4 expressions with local error:

8.2b
(*.f64 (-.f64 U* U) (*.f64 (/.f64 n Om) l))
8.2b
(*.f64 (-.f64 U* U) (*.f64 (/.f64 n Om) l))
22.7b
(cbrt.f64 (*.f64 U (+.f64 (*.f64 n (*.f64 2 (*.f64 (/.f64 (neg.f64 l) Om) (-.f64 (*.f64 2 l) (*.f64 (-.f64 U* U) (*.f64 (/.f64 n Om) l)))))) (*.f64 2 (*.f64 n t)))))
22.7b
(cbrt.f64 (*.f64 U (+.f64 (*.f64 n (*.f64 2 (*.f64 (/.f64 (neg.f64 l) Om) (-.f64 (*.f64 2 l) (*.f64 (-.f64 U* U) (*.f64 (/.f64 n Om) l)))))) (*.f64 2 (*.f64 n t)))))

rewrite170.0ms (0.5%)

Algorithm
rewrite-expression-head
Error
9.3b
Rules
22×add-exp-log_binary64_457 add-cbrt-cube_binary64_455
14×pow1_binary64_480
10×add-sqr-sqrt_binary64_441 *-un-lft-identity_binary64_419 prod-exp_binary64_468 cbrt-unprod_binary64_452 associate-*l/_binary64_362 associate-*l*_binary64_360
add-cube-cbrt_binary64_454 associate-*r/_binary64_361 pow-prod-down_binary64_490
add-log-exp_binary64_458 cbrt-div_binary64_451 flip3--_binary64_423 frac-times_binary64_429 flip--_binary64_394
pow1/3_binary64_501 flip3-+_binary64_422 flip-+_binary64_393 cbrt-prod_binary64_450 div-exp_binary64_470 cbrt-undiv_binary64_453 difference-of-squares_binary64_388 distribute-lft-out--_binary64_371 associate-*r*_binary64_359 *-commutative_binary64_350
Counts
4 → 76
Calls

4 calls:

18.0ms
(cbrt.f64 (*.f64 U (+.f64 (*.f64 n (*.f64 2 (*.f64 (/.f64 (neg.f64 l) Om) (-.f64 (*.f64 2 l) (*.f64 (-.f64 U* U) (*.f64 (/.f64 n Om) l)))))) (*.f64 2 (*.f64 n t)))))
16.0ms
(cbrt.f64 (*.f64 U (+.f64 (*.f64 n (*.f64 2 (*.f64 (/.f64 (neg.f64 l) Om) (-.f64 (*.f64 2 l) (*.f64 (-.f64 U* U) (*.f64 (/.f64 n Om) l)))))) (*.f64 2 (*.f64 n t)))))
9.0ms
(*.f64 (-.f64 U* U) (*.f64 (/.f64 n Om) l))
9.0ms
(*.f64 (-.f64 U* U) (*.f64 (/.f64 n Om) l))
Compiler

Compiled 6034 to 2480 computations (58.9% saved)

series4.7s (13.5%)

Error
9.3b
Counts
4 → 79
Calls

4 calls:

3.2s
(cbrt.f64 (*.f64 U (+.f64 (*.f64 n (*.f64 2 (*.f64 (/.f64 (neg.f64 l) Om) (-.f64 (*.f64 2 l) (*.f64 (-.f64 U* U) (*.f64 (/.f64 n Om) l)))))) (*.f64 2 (*.f64 n t)))))
1.1s
(cbrt.f64 (*.f64 U (+.f64 (*.f64 n (*.f64 2 (*.f64 (/.f64 (neg.f64 l) Om) (-.f64 (*.f64 2 l) (*.f64 (-.f64 U* U) (*.f64 (/.f64 n Om) l)))))) (*.f64 2 (*.f64 n t)))))
169.0ms
(*.f64 (-.f64 U* U) (*.f64 (/.f64 n Om) l))
154.0ms
(*.f64 (-.f64 U* U) (*.f64 (/.f64 n Om) l))
Compiler

Compiled 18660 to 12628 computations (32.3% saved)

simplify656.0ms (1.9%)

Algorithm
egg-herbie
Rules
347×cancel-sign-sub-inv_binary64_385
300×associate-*r*_binary64_359
248×associate-*l*_binary64_360
192×*-commutative_binary64_350
156×times-frac_binary64_425
153×associate-/l*_binary64_364
152×sub-neg_binary64_412
146×log-prod_binary64_505
126×sqr-pow_binary64_391
114×distribute-neg-frac_binary64_383
113×neg-mul-1_binary64_415
112×neg-sub0_binary64_414
91×exp-sum_binary64_465 associate-/r*_binary64_363
87×associate-*r/_binary64_361
76×log-div_binary64_506 distribute-rgt-neg-out_binary64_379 associate-*l/_binary64_362
61×+-commutative_binary64_349
58×distribute-rgt-neg-in_binary64_377
50×pow-sqr_binary64_392
49×distribute-rgt-in_binary64_369
48×distribute-lft-in_binary64_368
45×exp-prod_binary64_471
44×unswap-sqr_binary64_387
40×swap-sqr_binary64_386
37×distribute-lft-neg-in_binary64_376
35×cube-prod_binary64_447 distribute-neg-in_binary64_380
32×unsub-neg_binary64_413
26×distribute-lft-neg-out_binary64_378
21×div-sub_binary64_424 associate--l+_binary64_356
20×associate-/r/_binary64_365
19×unpow1/3_binary64_486 associate-+l+_binary64_352
16×cube-div_binary64_448
15×exp-diff_binary64_467
14×associate--r+_binary64_355
13×unpow3_binary64_485
12×cube-mult_binary64_449 remove-double-neg_binary64_407
pow-plus_binary64_482 distribute-lft-out--_binary64_371
cube-unmult_binary64_456
distribute-rgt-out--_binary64_373 associate-+r+_binary64_351
log-rec_binary64_507 cancel-sign-sub_binary64_384
log-pow_binary64_508 unpow2_binary64_484 exp-to-pow_binary64_481 unpow1_binary64_477 mul-1-neg_binary64_411 difference-of-squares_binary64_388 associate--r-_binary64_358 associate-+r-_binary64_353
cube-neg_binary64_446 sqr-neg_binary64_433 distribute-frac-neg_binary64_382 distribute-rgt-out_binary64_372 associate-+l-_binary64_354
--rgt-identity_binary64_405 distribute-lft-out_binary64_370
1-exp_binary64_463 rem-log-exp_binary64_460 rem-3cbrt-lft_binary64_444 *-rgt-identity_binary64_409 div0_binary64_400 *-inverses_binary64_399
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_682 erf-erfc_binary64_681 erf-odd_binary64_680 if-if-and-not_binary64_679 if-if-and_binary64_678 if-if-or-not_binary64_677 if-if-or_binary64_676 if-not_binary64_675 if-same_binary64_674 if-false_binary64_673 if-true_binary64_672 not-gte_binary64_671 not-lte_binary64_670 not-gt_binary64_669 not-lt_binary64_668 gte-same_binary64_667 lte-same_binary64_666 gt-same_binary64_665 lt-same_binary64_664 sinh---cosh_binary64_611 sinh-+-cosh_binary64_610 sinh-cosh_binary64_609 tanh-def-c_binary64_608 tanh-def-b_binary64_607 tanh-def-a_binary64_606 cosh-def_binary64_605 sinh-def_binary64_604 tan-neg_binary64_551 cos-neg_binary64_550 sin-neg_binary64_549 tan-0_binary64_548 cos-0_binary64_547 sin-0_binary64_546 hang-m-tan_binary64_545 hang-p-tan_binary64_544 hang-m0-tan_binary64_543 hang-p0-tan_binary64_542 hang-0m-tan_binary64_541 hang-0p-tan_binary64_540 tan-+PI/2_binary64_539 tan-+PI_binary64_538 tan-PI_binary64_537 tan-PI/3_binary64_536 tan-PI/4_binary64_535 tan-PI/6_binary64_534 cos-+PI/2_binary64_533 cos-+PI_binary64_532 cos-PI_binary64_531 cos-PI/2_binary64_530 cos-PI/3_binary64_529 cos-PI/4_binary64_528 cos-PI/6_binary64_527 sin-+PI/2_binary64_526 sin-+PI_binary64_525 sin-PI_binary64_524 sin-PI/2_binary64_523 sin-PI/3_binary64_522 sin-PI/4_binary64_521 sin-PI/6_binary64_520 sub-1-sin_binary64_519 sub-1-cos_binary64_518 -1-add-sin_binary64_517 -1-add-cos_binary64_516 1-sub-sin_binary64_515 1-sub-cos_binary64_514 cos-sin-sum_binary64_513 log-E_binary64_509 pow-base-0_binary64_503 unpow1/2_binary64_483 pow-base-1_binary64_479 unpow0_binary64_478 unpow-1_binary64_476 exp-lft-cube_binary64_475 exp-lft-sqr_binary64_474 exp-cbrt_binary64_473 exp-sqrt_binary64_472 div-exp_binary64_470 rec-exp_binary64_469 prod-exp_binary64_468 exp-neg_binary64_466 e-exp-1_binary64_464 exp-1-e_binary64_462 exp-0_binary64_461 rem-exp-log_binary64_459 rem-3cbrt-rft_binary64_445 rem-cbrt-cube_binary64_443 rem-cube-cbrt_binary64_442 sqr-abs_binary64_434 rem-sqrt-square_binary64_432 rem-square-sqrt_binary64_431 /-rgt-identity_binary64_410 *-lft-identity_binary64_408 sub0-neg_binary64_406 +-rgt-identity_binary64_404 +-lft-identity_binary64_403 mul0-rgt_binary64_402 mul0-lft_binary64_401 +-inverses_binary64_398 lft-mult-inverse_binary64_397 rgt-mult-inverse_binary64_396 remove-double-div_binary64_395 difference-of-sqr--1_binary64_390 difference-of-sqr-1_binary64_389 distribute-neg-out_binary64_381 distribute-rgt1-in_binary64_375 distribute-lft1-in_binary64_374 count-2_binary64_367 associate-/l/_binary64_366 associate--l-_binary64_357
Counts
155 → 551
Iterations

Useful iterations: 2 (0.0ms)

IterNodesCost
03285066
19604692
234884634

prune1.2s (3.5%)

Pruning

30 alts after pruning (28 fresh and 2 done)

PrunedKeptTotal
New5501551
Fresh02727
Picked011
Done112
Total55130581
Error
9.3b
Counts
581 → 30
Compiler

Compiled 44615 to 18562 computations (58.4% saved)

regimes3.3s (9.4%)

Accuracy

Total 19.6b remaining (70.1%)

Threshold costs 0b (0%)

Compiler

Compiled 51194 to 36586 computations (28.5% saved)

bsearch172.0ms (0.5%)

Steps
ItersRangePoint
6
4.793679950587205e+134
2.8026176026947286e+135
2.772988692385023e+135
6
-3.7926419831087285e+225
-7.369337618295341e+224
-1.8141662603144044e+225
Compiler

Compiled 1 to 6 computations (-500% saved)

simplify74.0ms (0.2%)

Algorithm
egg-herbie
Rules
232×neg-mul-1_binary64_415 neg-sub0_binary64_414
194×unsub-neg_binary64_413
191×distribute-rgt-neg-in_binary64_377
179×distribute-rgt-neg-out_binary64_379
152×distribute-neg-out_binary64_381
131×distribute-lft-neg-out_binary64_378
126×distribute-lft-neg-in_binary64_376
99×cancel-sign-sub-inv_binary64_385
75×remove-double-neg_binary64_407
74×sub-neg_binary64_412
70×*-commutative_binary64_350
63×distribute-neg-in_binary64_380
56×+-commutative_binary64_349
14×distribute-frac-neg_binary64_382
distribute-neg-frac_binary64_383
sqr-neg_binary64_433
--rgt-identity_binary64_405
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_679 if-if-and_binary64_678 if-if-or-not_binary64_677 if-if-or_binary64_676 if-not_binary64_675 if-same_binary64_674 if-false_binary64_673 if-true_binary64_672 tan-0_binary64_548 cos-0_binary64_547 sin-0_binary64_546 unpow1_binary64_477 e-exp-1_binary64_464 1-exp_binary64_463 exp-1-e_binary64_462 exp-0_binary64_461 sqr-abs_binary64_434 mul-1-neg_binary64_411 /-rgt-identity_binary64_410 *-rgt-identity_binary64_409 *-lft-identity_binary64_408 sub0-neg_binary64_406 +-rgt-identity_binary64_404 +-lft-identity_binary64_403 cancel-sign-sub_binary64_384
Iterations

Useful iterations: 4 (0.0ms)

IterNodesCost
063162
1112162
2165162
3235162
4324160
5412160
6598160
7941160
8887160
9933160
10972160
111018160
121056160
131086160
141101160
151105160
161105160
Proof
(if real (<= f64 h0 -1814166260314404422947506509472034874826589041472300679717874962722517490483781621807946692596512301534408456805020279248906501522976269774510795590322468755848152374207171914118282888081140328818338822119409949039069086351360) (* f64 (sqrt f64 (* f64 (* f64 h1 h2) (- f64 (* f64 (/ f64 h1 h3) (/ f64 h4 h3)) (+ f64 (/ f64 2 h3) (* f64 (/ f64 h1 (* f64 h3 h3)) h2))))) (neg f64 (* f64 (sqrt f64 2) h0))) (if real (<= f64 h0 2772988692385023087469996441391698009735755660052512759581547813830841443968204856060581660343635181422519447361689608799692542493851648) (sqrt f64 (+ f64 (* f64 (* f64 h5 (* f64 2 h1)) h2) (* f64 h2 (* f64 (* f64 (* f64 h1 2) (=> (/ f64 (neg f64 h0) h3))) (- f64 (* f64 2 h0) (* f64 (- f64 h4 h2) (/ f64 (* f64 h1 h0) h3))))))) (* f64 h0 (sqrt f64 (- f64 (* f64 2 (- f64 (/ f64 (/ f64 (* f64 h1 h1) (/ f64 (/ f64 h3 h2) h4)) h3) (/ f64 (* f64 h1 h1) (* f64 (/ f64 h3 h2) (/ f64 h3 h2))))) (* f64 4 (* f64 (/ f64 h1 h3) h2))))))) distribute-frac-neg_binary64_382 => (if real (<= f64 h0 -1814166260314404422947506509472034874826589041472300679717874962722517490483781621807946692596512301534408456805020279248906501522976269774510795590322468755848152374207171914118282888081140328818338822119409949039069086351360) (* f64 (sqrt f64 (* f64 (* f64 h1 h2) (- f64 (* f64 (/ f64 h1 h3) (/ f64 h4 h3)) (+ f64 (/ f64 2 h3) (* f64 (/ f64 h1 (* f64 h3 h3)) h2))))) (=> (neg f64 (* f64 (sqrt f64 2) h0)))) (if real (<= f64 h0 2772988692385023087469996441391698009735755660052512759581547813830841443968204856060581660343635181422519447361689608799692542493851648) (sqrt f64 (+ f64 (* f64 (* f64 h5 (* f64 2 h1)) h2) (* f64 h2 (* f64 (* f64 (* f64 h1 2) (neg f64 (/ f64 h0 h3))) (- f64 (* f64 2 h0) (* f64 (- f64 h4 h2) (/ f64 (* f64 h1 h0) h3))))))) (* f64 h0 (sqrt f64 (- f64 (* f64 2 (- f64 (/ f64 (/ f64 (* f64 h1 h1) (/ f64 (/ f64 h3 h2) h4)) h3) (/ f64 (* f64 h1 h1) (* f64 (/ f64 h3 h2) (/ f64 h3 h2))))) (* f64 4 (* f64 (/ f64 h1 h3) h2))))))) distribute-rgt-neg-in_binary64_377 => (if real (<= f64 h0 -1814166260314404422947506509472034874826589041472300679717874962722517490483781621807946692596512301534408456805020279248906501522976269774510795590322468755848152374207171914118282888081140328818338822119409949039069086351360) (* f64 (sqrt f64 (* f64 (* f64 h1 h2) (- f64 (* f64 (/ f64 h1 h3) (/ f64 h4 h3)) (+ f64 (/ f64 2 h3) (* f64 (/ f64 h1 (* f64 h3 h3)) h2))))) (* f64 (sqrt f64 2) (neg f64 h0))) (if real (<= f64 h0 2772988692385023087469996441391698009735755660052512759581547813830841443968204856060581660343635181422519447361689608799692542493851648) (sqrt f64 (+ f64 (* f64 (* f64 h5 (* f64 2 h1)) h2) (* f64 h2 (* f64 (* f64 (=> (* f64 h1 2)) (neg f64 (/ f64 h0 h3))) (- f64 (* f64 2 h0) (* f64 (- f64 h4 h2) (/ f64 (* f64 h1 h0) h3))))))) (* f64 h0 (sqrt f64 (- f64 (* f64 2 (- f64 (/ f64 (/ f64 (* f64 h1 h1) (/ f64 (/ f64 h3 h2) h4)) h3) (/ f64 (* f64 h1 h1) (* f64 (/ f64 h3 h2) (/ f64 h3 h2))))) (* f64 4 (* f64 (/ f64 h1 h3) h2))))))) *-commutative_binary64_350 => (if real (<= f64 h0 -1814166260314404422947506509472034874826589041472300679717874962722517490483781621807946692596512301534408456805020279248906501522976269774510795590322468755848152374207171914118282888081140328818338822119409949039069086351360) (* f64 (sqrt f64 (* f64 (* f64 h1 h2) (- f64 (* f64 (/ f64 h1 h3) (/ f64 h4 h3)) (+ f64 (/ f64 2 h3) (=> (* f64 (/ f64 h1 (* f64 h3 h3)) h2)))))) (* f64 (sqrt f64 2) (neg f64 h0))) (if real (<= f64 h0 2772988692385023087469996441391698009735755660052512759581547813830841443968204856060581660343635181422519447361689608799692542493851648) (sqrt f64 (+ f64 (* f64 (* f64 h5 (* f64 2 h1)) h2) (* f64 h2 (* f64 (* f64 (* f64 2 h1) (neg f64 (/ f64 h0 h3))) (- f64 (* f64 2 h0) (* f64 (- f64 h4 h2) (/ f64 (* f64 h1 h0) h3))))))) (* f64 h0 (sqrt f64 (- f64 (* f64 2 (- f64 (/ f64 (/ f64 (* f64 h1 h1) (/ f64 (/ f64 h3 h2) h4)) h3) (/ f64 (* f64 h1 h1) (* f64 (/ f64 h3 h2) (/ f64 h3 h2))))) (* f64 4 (* f64 (/ f64 h1 h3) h2))))))) *-commutative_binary64_350 => (if real (<= f64 h0 -1814166260314404422947506509472034874826589041472300679717874962722517490483781621807946692596512301534408456805020279248906501522976269774510795590322468755848152374207171914118282888081140328818338822119409949039069086351360) (* f64 (sqrt f64 (* f64 (* f64 h1 h2) (- f64 (* f64 (/ f64 h1 h3) (/ f64 h4 h3)) (+ f64 (/ f64 2 h3) (* f64 h2 (/ f64 h1 (* f64 h3 h3))))))) (* f64 (sqrt f64 2) (neg f64 h0))) (if real (<= f64 h0 2772988692385023087469996441391698009735755660052512759581547813830841443968204856060581660343635181422519447361689608799692542493851648) (sqrt f64 (+ f64 (=> (* f64 (* f64 h5 (* f64 2 h1)) h2)) (* f64 h2 (* f64 (* f64 (* f64 2 h1) (neg f64 (/ f64 h0 h3))) (- f64 (* f64 2 h0) (* f64 (- f64 h4 h2) (/ f64 (* f64 h1 h0) h3))))))) (* f64 h0 (sqrt f64 (- f64 (* f64 2 (- f64 (/ f64 (/ f64 (* f64 h1 h1) (/ f64 (/ f64 h3 h2) h4)) h3) (/ f64 (* f64 h1 h1) (* f64 (/ f64 h3 h2) (/ f64 h3 h2))))) (* f64 4 (* f64 (/ f64 h1 h3) h2))))))) *-commutative_binary64_350 => (if real (<= f64 h0 -1814166260314404422947506509472034874826589041472300679717874962722517490483781621807946692596512301534408456805020279248906501522976269774510795590322468755848152374207171914118282888081140328818338822119409949039069086351360) (* f64 (sqrt f64 (* f64 (* f64 h1 h2) (- f64 (* f64 (/ f64 h1 h3) (/ f64 h4 h3)) (+ f64 (/ f64 2 h3) (* f64 h2 (/ f64 h1 (* f64 h3 h3))))))) (* f64 (sqrt f64 2) (neg f64 h0))) (if real (<= f64 h0 2772988692385023087469996441391698009735755660052512759581547813830841443968204856060581660343635181422519447361689608799692542493851648) (sqrt f64 (+ f64 (* f64 h2 (* f64 h5 (* f64 2 h1))) (* f64 h2 (* f64 (* f64 (* f64 2 h1) (neg f64 (/ f64 h0 h3))) (- f64 (* f64 2 h0) (* f64 (- f64 h4 h2) (/ f64 (* f64 h1 h0) h3))))))) (* f64 h0 (sqrt f64 (- f64 (* f64 2 (- f64 (/ f64 (/ f64 (* f64 h1 h1) (/ f64 (/ f64 h3 h2) h4)) h3) (/ f64 (* f64 h1 h1) (* f64 (/ f64 h3 h2) (/ f64 h3 h2))))) (* f64 4 (* f64 (/ f64 h1 h3) h2))))))) <= *-commutative_binary64_350 (if real (<= f64 h0 -1814166260314404422947506509472034874826589041472300679717874962722517490483781621807946692596512301534408456805020279248906501522976269774510795590322468755848152374207171914118282888081140328818338822119409949039069086351360) (* f64 (sqrt f64 (* f64 (* f64 h1 h2) (- f64 (* f64 (/ f64 h1 h3) (/ f64 h4 h3)) (+ f64 (/ f64 2 h3) (* f64 h2 (/ f64 h1 (* f64 h3 h3))))))) (* f64 (sqrt f64 2) (neg f64 h0))) (if real (<= f64 h0 2772988692385023087469996441391698009735755660052512759581547813830841443968204856060581660343635181422519447361689608799692542493851648) (sqrt f64 (+ f64 (* f64 h2 (* f64 h5 (<= (* f64 h1 2)))) (* f64 h2 (* f64 (* f64 (* f64 2 h1) (neg f64 (/ f64 h0 h3))) (- f64 (* f64 2 h0) (* f64 (- f64 h4 h2) (/ f64 (* f64 h1 h0) h3))))))) (* f64 h0 (sqrt f64 (- f64 (* f64 2 (- f64 (/ f64 (/ f64 (* f64 h1 h1) (/ f64 (/ f64 h3 h2) h4)) h3) (/ f64 (* f64 h1 h1) (* f64 (/ f64 h3 h2) (/ f64 h3 h2))))) (* f64 4 (=> (* f64 (/ f64 h1 h3) h2)))))))) *-commutative_binary64_350 => (if real (<= f64 h0 -1814166260314404422947506509472034874826589041472300679717874962722517490483781621807946692596512301534408456805020279248906501522976269774510795590322468755848152374207171914118282888081140328818338822119409949039069086351360) (* f64 (sqrt f64 (* f64 (* f64 h1 h2) (- f64 (* f64 (/ f64 h1 h3) (/ f64 h4 h3)) (+ f64 (/ f64 2 h3) (* f64 h2 (/ f64 h1 (* f64 h3 h3))))))) (* f64 (sqrt f64 2) (neg f64 h0))) (if real (<= f64 h0 2772988692385023087469996441391698009735755660052512759581547813830841443968204856060581660343635181422519447361689608799692542493851648) (sqrt f64 (+ f64 (* f64 h2 (* f64 h5 (* f64 h1 2))) (* f64 h2 (* f64 (=> (* f64 (* f64 2 h1) (neg f64 (/ f64 h0 h3)))) (- f64 (* f64 2 h0) (* f64 (- f64 h4 h2) (/ f64 (* f64 h1 h0) h3))))))) (* f64 h0 (sqrt f64 (- f64 (* f64 2 (- f64 (/ f64 (/ f64 (* f64 h1 h1) (/ f64 (/ f64 h3 h2) h4)) h3) (/ f64 (* f64 h1 h1) (* f64 (/ f64 h3 h2) (/ f64 h3 h2))))) (* f64 4 (* f64 h2 (/ f64 h1 h3)))))))) distribute-rgt-neg-out_binary64_379 => (if real (<= f64 h0 -1814166260314404422947506509472034874826589041472300679717874962722517490483781621807946692596512301534408456805020279248906501522976269774510795590322468755848152374207171914118282888081140328818338822119409949039069086351360) (* f64 (sqrt f64 (* f64 (* f64 h1 h2) (- f64 (* f64 (/ f64 h1 h3) (/ f64 h4 h3)) (+ f64 (/ f64 2 h3) (* f64 h2 (/ f64 h1 (* f64 h3 h3))))))) (* f64 (sqrt f64 2) (neg f64 h0))) (if real (<= f64 h0 2772988692385023087469996441391698009735755660052512759581547813830841443968204856060581660343635181422519447361689608799692542493851648) (sqrt f64 (+ f64 (* f64 h2 (* f64 h5 (* f64 h1 2))) (* f64 h2 (=> (* f64 (neg f64 (* f64 (* f64 2 h1) (/ f64 h0 h3))) (- f64 (* f64 2 h0) (* f64 (- f64 h4 h2) (/ f64 (* f64 h1 h0) h3)))))))) (* f64 h0 (sqrt f64 (- f64 (* f64 2 (- f64 (/ f64 (/ f64 (* f64 h1 h1) (/ f64 (/ f64 h3 h2) h4)) h3) (/ f64 (* f64 h1 h1) (* f64 (/ f64 h3 h2) (/ f64 h3 h2))))) (* f64 4 (* f64 h2 (/ f64 h1 h3)))))))) distribute-lft-neg-out_binary64_378 => (if real (<= f64 h0 -1814166260314404422947506509472034874826589041472300679717874962722517490483781621807946692596512301534408456805020279248906501522976269774510795590322468755848152374207171914118282888081140328818338822119409949039069086351360) (* f64 (sqrt f64 (* f64 (* f64 h1 h2) (- f64 (* f64 (/ f64 h1 h3) (/ f64 h4 h3)) (+ f64 (/ f64 2 h3) (* f64 h2 (/ f64 h1 (* f64 h3 h3))))))) (* f64 (sqrt f64 2) (neg f64 h0))) (if real (<= f64 h0 2772988692385023087469996441391698009735755660052512759581547813830841443968204856060581660343635181422519447361689608799692542493851648) (sqrt f64 (+ f64 (* f64 h2 (* f64 h5 (* f64 h1 2))) (* f64 h2 (=> (neg f64 (* f64 (* f64 (* f64 2 h1) (/ f64 h0 h3)) (- f64 (* f64 2 h0) (* f64 (- f64 h4 h2) (/ f64 (* f64 h1 h0) h3))))))))) (* f64 h0 (sqrt f64 (- f64 (* f64 2 (- f64 (/ f64 (/ f64 (* f64 h1 h1) (/ f64 (/ f64 h3 h2) h4)) h3) (/ f64 (* f64 h1 h1) (* f64 (/ f64 h3 h2) (/ f64 h3 h2))))) (* f64 4 (* f64 h2 (/ f64 h1 h3)))))))) distribute-rgt-neg-in_binary64_377 => (if real (<= f64 h0 -1814166260314404422947506509472034874826589041472300679717874962722517490483781621807946692596512301534408456805020279248906501522976269774510795590322468755848152374207171914118282888081140328818338822119409949039069086351360) (* f64 (sqrt f64 (* f64 (* f64 h1 h2) (- f64 (* f64 (/ f64 h1 h3) (/ f64 h4 h3)) (+ f64 (/ f64 2 h3) (* f64 h2 (/ f64 h1 (* f64 h3 h3))))))) (* f64 (sqrt f64 2) (neg f64 h0))) (if real (<= f64 h0 2772988692385023087469996441391698009735755660052512759581547813830841443968204856060581660343635181422519447361689608799692542493851648) (sqrt f64 (+ f64 (* f64 h2 (* f64 h5 (* f64 h1 2))) (* f64 h2 (* f64 (* f64 (* f64 2 h1) (/ f64 h0 h3)) (neg f64 (=> (- f64 (* f64 2 h0) (* f64 (- f64 h4 h2) (/ f64 (* f64 h1 h0) h3))))))))) (* f64 h0 (sqrt f64 (- f64 (* f64 2 (- f64 (/ f64 (/ f64 (* f64 h1 h1) (/ f64 (/ f64 h3 h2) h4)) h3) (/ f64 (* f64 h1 h1) (* f64 (/ f64 h3 h2) (/ f64 h3 h2))))) (* f64 4 (* f64 h2 (/ f64 h1 h3)))))))) sub-neg_binary64_412 => (if real (<= f64 h0 -1814166260314404422947506509472034874826589041472300679717874962722517490483781621807946692596512301534408456805020279248906501522976269774510795590322468755848152374207171914118282888081140328818338822119409949039069086351360) (* f64 (sqrt f64 (* f64 (* f64 h1 h2) (- f64 (* f64 (/ f64 h1 h3) (/ f64 h4 h3)) (+ f64 (/ f64 2 h3) (* f64 h2 (/ f64 h1 (* f64 h3 h3))))))) (* f64 (sqrt f64 2) (neg f64 h0))) (if real (<= f64 h0 2772988692385023087469996441391698009735755660052512759581547813830841443968204856060581660343635181422519447361689608799692542493851648) (sqrt f64 (+ f64 (* f64 h2 (* f64 h5 (* f64 h1 2))) (* f64 h2 (* f64 (* f64 (* f64 2 h1) (/ f64 h0 h3)) (neg f64 (+ f64 (* f64 2 h0) (neg f64 (* f64 (- f64 h4 h2) (/ f64 (* f64 h1 h0) h3))))))))) (* f64 h0 (sqrt f64 (- f64 (* f64 2 (- f64 (/ f64 (/ f64 (* f64 h1 h1) (/ f64 (/ f64 h3 h2) h4)) h3) (/ f64 (* f64 h1 h1) (* f64 (/ f64 h3 h2) (/ f64 h3 h2))))) (* f64 4 (* f64 h2 (/ f64 h1 h3)))))))) <= *-commutative_binary64_350 (if real (<= f64 h0 -1814166260314404422947506509472034874826589041472300679717874962722517490483781621807946692596512301534408456805020279248906501522976269774510795590322468755848152374207171914118282888081140328818338822119409949039069086351360) (* f64 (sqrt f64 (* f64 (* f64 h1 h2) (- f64 (* f64 (/ f64 h1 h3) (/ f64 h4 h3)) (+ f64 (/ f64 2 h3) (* f64 h2 (/ f64 h1 (* f64 h3 h3))))))) (* f64 (sqrt f64 2) (neg f64 h0))) (if real (<= f64 h0 2772988692385023087469996441391698009735755660052512759581547813830841443968204856060581660343635181422519447361689608799692542493851648) (sqrt f64 (+ f64 (* f64 h2 (* f64 h5 (* f64 h1 2))) (* f64 h2 (* f64 (* f64 (<= (* f64 h1 2)) (/ f64 h0 h3)) (neg f64 (=> (+ f64 (* f64 2 h0) (neg f64 (* f64 (- f64 h4 h2) (/ f64 (* f64 h1 h0) h3)))))))))) (* f64 h0 (sqrt f64 (- f64 (* f64 2 (- f64 (/ f64 (/ f64 (* f64 h1 h1) (/ f64 (/ f64 h3 h2) h4)) h3) (/ f64 (* f64 h1 h1) (* f64 (/ f64 h3 h2) (/ f64 h3 h2))))) (* f64 4 (* f64 h2 (/ f64 h1 h3)))))))) +-commutative_binary64_349 => (if real (<= f64 h0 -1814166260314404422947506509472034874826589041472300679717874962722517490483781621807946692596512301534408456805020279248906501522976269774510795590322468755848152374207171914118282888081140328818338822119409949039069086351360) (* f64 (sqrt f64 (* f64 (* f64 h1 h2) (- f64 (* f64 (/ f64 h1 h3) (/ f64 h4 h3)) (+ f64 (/ f64 2 h3) (* f64 h2 (/ f64 h1 (* f64 h3 h3))))))) (* f64 (sqrt f64 2) (neg f64 h0))) (if real (<= f64 h0 2772988692385023087469996441391698009735755660052512759581547813830841443968204856060581660343635181422519447361689608799692542493851648) (sqrt f64 (+ f64 (* f64 h2 (* f64 h5 (* f64 h1 2))) (* f64 h2 (* f64 (* f64 (* f64 h1 2) (/ f64 h0 h3)) (=> (neg f64 (+ f64 (neg f64 (* f64 (- f64 h4 h2) (/ f64 (* f64 h1 h0) h3))) (* f64 2 h0)))))))) (* f64 h0 (sqrt f64 (- f64 (* f64 2 (- f64 (/ f64 (/ f64 (* f64 h1 h1) (/ f64 (/ f64 h3 h2) h4)) h3) (/ f64 (* f64 h1 h1) (* f64 (/ f64 h3 h2) (/ f64 h3 h2))))) (* f64 4 (* f64 h2 (/ f64 h1 h3)))))))) distribute-neg-in_binary64_380 => (if real (<= f64 h0 -1814166260314404422947506509472034874826589041472300679717874962722517490483781621807946692596512301534408456805020279248906501522976269774510795590322468755848152374207171914118282888081140328818338822119409949039069086351360) (* f64 (sqrt f64 (* f64 (* f64 h1 h2) (- f64 (* f64 (/ f64 h1 h3) (/ f64 h4 h3)) (+ f64 (/ f64 2 h3) (* f64 h2 (/ f64 h1 (* f64 h3 h3))))))) (* f64 (sqrt f64 2) (neg f64 h0))) (if real (<= f64 h0 2772988692385023087469996441391698009735755660052512759581547813830841443968204856060581660343635181422519447361689608799692542493851648) (sqrt f64 (+ f64 (* f64 h2 (* f64 h5 (* f64 h1 2))) (* f64 h2 (* f64 (* f64 (* f64 h1 2) (/ f64 h0 h3)) (=> (+ f64 (neg f64 (neg f64 (* f64 (- f64 h4 h2) (/ f64 (* f64 h1 h0) h3)))) (neg f64 (* f64 2 h0)))))))) (* f64 h0 (sqrt f64 (- f64 (* f64 2 (- f64 (/ f64 (/ f64 (* f64 h1 h1) (/ f64 (/ f64 h3 h2) h4)) h3) (/ f64 (* f64 h1 h1) (* f64 (/ f64 h3 h2) (/ f64 h3 h2))))) (* f64 4 (* f64 h2 (/ f64 h1 h3)))))))) unsub-neg_binary64_413 => (if real (<= f64 h0 -1814166260314404422947506509472034874826589041472300679717874962722517490483781621807946692596512301534408456805020279248906501522976269774510795590322468755848152374207171914118282888081140328818338822119409949039069086351360) (* f64 (sqrt f64 (* f64 (* f64 h1 h2) (- f64 (* f64 (/ f64 h1 h3) (/ f64 h4 h3)) (+ f64 (/ f64 2 h3) (* f64 h2 (/ f64 h1 (* f64 h3 h3))))))) (* f64 (sqrt f64 2) (neg f64 h0))) (if real (<= f64 h0 2772988692385023087469996441391698009735755660052512759581547813830841443968204856060581660343635181422519447361689608799692542493851648) (sqrt f64 (+ f64 (* f64 h2 (* f64 h5 (* f64 h1 2))) (* f64 h2 (* f64 (* f64 (* f64 h1 2) (/ f64 h0 h3)) (- f64 (neg f64 (neg f64 (* f64 (- f64 h4 h2) (/ f64 (* f64 h1 h0) h3)))) (=> (* f64 2 h0))))))) (* f64 h0 (sqrt f64 (- f64 (* f64 2 (- f64 (/ f64 (/ f64 (* f64 h1 h1) (/ f64 (/ f64 h3 h2) h4)) h3) (/ f64 (* f64 h1 h1) (* f64 (/ f64 h3 h2) (/ f64 h3 h2))))) (* f64 4 (* f64 h2 (/ f64 h1 h3)))))))) *-commutative_binary64_350 => (if real (<= f64 h0 -1814166260314404422947506509472034874826589041472300679717874962722517490483781621807946692596512301534408456805020279248906501522976269774510795590322468755848152374207171914118282888081140328818338822119409949039069086351360) (* f64 (sqrt f64 (* f64 (* f64 h1 h2) (- f64 (* f64 (/ f64 h1 h3) (/ f64 h4 h3)) (+ f64 (/ f64 2 h3) (* f64 h2 (/ f64 h1 (* f64 h3 h3))))))) (* f64 (sqrt f64 2) (neg f64 h0))) (if real (<= f64 h0 2772988692385023087469996441391698009735755660052512759581547813830841443968204856060581660343635181422519447361689608799692542493851648) (sqrt f64 (+ f64 (* f64 h2 (* f64 h5 (* f64 h1 2))) (* f64 h2 (* f64 (* f64 (* f64 h1 2) (/ f64 h0 h3)) (- f64 (=> (neg f64 (neg f64 (* f64 (- f64 h4 h2) (/ f64 (* f64 h1 h0) h3))))) (* f64 h0 2)))))) (* f64 h0 (sqrt f64 (- f64 (* f64 2 (- f64 (/ f64 (/ f64 (* f64 h1 h1) (/ f64 (/ f64 h3 h2) h4)) h3) (/ f64 (* f64 h1 h1) (* f64 (/ f64 h3 h2) (/ f64 h3 h2))))) (* f64 4 (* f64 h2 (/ f64 h1 h3)))))))) remove-double-neg_binary64_407 => (if real (<= f64 h0 -1814166260314404422947506509472034874826589041472300679717874962722517490483781621807946692596512301534408456805020279248906501522976269774510795590322468755848152374207171914118282888081140328818338822119409949039069086351360) (* f64 (sqrt f64 (* f64 (* f64 h1 h2) (- f64 (* f64 (/ f64 h1 h3) (/ f64 h4 h3)) (+ f64 (/ f64 2 h3) (* f64 h2 (/ f64 h1 (* f64 h3 h3))))))) (* f64 (sqrt f64 2) (neg f64 h0))) (if real (<= f64 h0 2772988692385023087469996441391698009735755660052512759581547813830841443968204856060581660343635181422519447361689608799692542493851648) (sqrt f64 (+ f64 (* f64 h2 (* f64 h5 (* f64 h1 2))) (* f64 h2 (* f64 (* f64 (* f64 h1 2) (/ f64 h0 h3)) (- f64 (* f64 (- f64 h4 h2) (/ f64 (=> (* f64 h1 h0)) h3)) (* f64 h0 2)))))) (* f64 h0 (sqrt f64 (- f64 (* f64 2 (- f64 (/ f64 (/ f64 (* f64 h1 h1) (/ f64 (/ f64 h3 h2) h4)) h3) (/ f64 (* f64 h1 h1) (* f64 (/ f64 h3 h2) (/ f64 h3 h2))))) (* f64 4 (* f64 h2 (/ f64 h1 h3)))))))) *-commutative_binary64_350 => (if real (<= f64 h0 -1814166260314404422947506509472034874826589041472300679717874962722517490483781621807946692596512301534408456805020279248906501522976269774510795590322468755848152374207171914118282888081140328818338822119409949039069086351360) (* f64 (sqrt f64 (* f64 (* f64 h1 h2) (- f64 (* f64 (/ f64 h1 h3) (/ f64 h4 h3)) (+ f64 (/ f64 2 h3) (* f64 h2 (/ f64 h1 (* f64 h3 h3))))))) (* f64 (sqrt f64 2) (neg f64 h0))) (if real (<= f64 h0 2772988692385023087469996441391698009735755660052512759581547813830841443968204856060581660343635181422519447361689608799692542493851648) (sqrt f64 (+ f64 (* f64 h2 (* f64 h5 (* f64 h1 2))) (* f64 h2 (* f64 (* f64 (* f64 h1 2) (/ f64 h0 h3)) (- f64 (* f64 (- f64 h4 h2) (/ f64 (* f64 h0 h1) h3)) (* f64 h0 2)))))) (* f64 h0 (sqrt f64 (- f64 (* f64 2 (- f64 (/ f64 (/ f64 (* f64 h1 h1) (/ f64 (/ f64 h3 h2) h4)) h3) (/ f64 (* f64 h1 h1) (* f64 (/ f64 h3 h2) (/ f64 h3 h2))))) (* f64 4 (* f64 h2 (/ f64 h1 h3))))))))

end0.0ms (0%)

sample10.1s (29.2%)

Algorithm
intervals
Results
2.2s12760×body128nan
1.5s8000×body128valid
368.0ms1197×body128invalid
Compiler

Compiled 6519 to 4648 computations (28.7% saved)

Profiling

Loading profile data...