Details

Time bar (total: 16.1s)

analyze472.0ms (2.9%)

Algorithm
search
Search
TrueOtherFalseIter
0%99.8%0.2%0
0%99.8%0.2%1
49.9%49.9%0.2%2
49.9%49.9%0.2%3
49.9%49.9%0.2%4
49.9%49.9%0.2%5
49.9%49.9%0.2%6
49.9%49.9%0.2%7
53%46.8%0.2%8
57.7%42.1%0.2%9
61.6%38.2%0.2%10
63.5%30%6.4%11
63.5%30%6.4%12
67.6%25.9%6.4%13
68.9%24.7%6.4%14
Compiler

Compiled 16 to 15 computations (6.3% saved)

sample95.0ms (0.6%)

Algorithm
intervals
Results
20.0ms49×body1024valid
15.0ms61×body1024invalid
11.0ms48×body512valid
9.0ms139×body128valid
6.0ms101×body128invalid
6.0ms33×body512invalid
2.0ms18×body256valid
2.0ms18×body256invalid
1.0msbody2048valid
Compiler

Compiled 31 to 33 computations (-6.5% saved)

simplify944.0ms (5.9%)

Algorithm
egg-herbie
Rules
510×exp-prod_binary64_471
279×unsub-neg_binary64_413
265×div-sub_binary64_424
177×neg-mul-1_binary64_415
176×*-commutative_binary64_350
171×distribute-rgt-in_binary64_369
168×neg-sub0_binary64_414
154×distribute-rgt-neg-in_binary64_377
131×swap-sqr_binary64_386
125×sub-neg_binary64_412
102×distribute-lft-in_binary64_368
99×cancel-sign-sub-inv_binary64_385
85×associate-*l*_binary64_360
84×associate-*r*_binary64_359
82×distribute-rgt-out_binary64_372 associate-/l*_binary64_364
78×distribute-lft-neg-in_binary64_376
66×pow-plus_binary64_482
53×distribute-rgt-neg-out_binary64_379
52×distribute-lft-neg-out_binary64_378
51×exp-sum_binary64_465
49×+-commutative_binary64_349
48×sub0-neg_binary64_406
47×distribute-rgt1-in_binary64_375 associate-+l-_binary64_354
45×distribute-neg-frac_binary64_383
40×associate-+l+_binary64_352
37×exp-diff_binary64_467
36×associate-+r+_binary64_351
34×associate-*r/_binary64_361
33×sqr-pow_binary64_391
30×associate-*l/_binary64_362
29×unswap-sqr_binary64_387 distribute-neg-out_binary64_381
28×mul0-rgt_binary64_402 mul0-lft_binary64_401 distribute-neg-in_binary64_380
24×associate--r+_binary64_355
23×distribute-frac-neg_binary64_382
21×*-lft-identity_binary64_408
20×associate-/r*_binary64_363
17×div0_binary64_400 pow-sqr_binary64_392
16×sqr-neg_binary64_433
15×remove-double-neg_binary64_407 associate--l-_binary64_357
14×+-lft-identity_binary64_403
13×*-rgt-identity_binary64_409 associate-/l/_binary64_366
12×exp-lft-sqr_binary64_474 distribute-lft1-in_binary64_374
11×cube-prod_binary64_447 --rgt-identity_binary64_405
distribute-lft-out_binary64_370 count-2_binary64_367
cube-unmult_binary64_456 /-rgt-identity_binary64_410
prod-exp_binary64_468 exp-neg_binary64_466 +-rgt-identity_binary64_404
pow-base-1_binary64_479 associate-/r/_binary64_365 associate-+r-_binary64_353
exp-sqrt_binary64_472
div-exp_binary64_470 cube-div_binary64_448 rem-sqrt-square_binary64_432 mul-1-neg_binary64_411 *-inverses_binary64_399 associate--r-_binary64_358
1-exp_binary64_463 exp-1-e_binary64_462 rgt-mult-inverse_binary64_396 cancel-sign-sub_binary64_384 distribute-rgt-out--_binary64_373 associate--l+_binary64_356
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 unpow2_binary64_484 unpow1/2_binary64_483 exp-to-pow_binary64_481 unpow0_binary64_478 unpow1_binary64_477 unpow-1_binary64_476 exp-lft-cube_binary64_475 exp-cbrt_binary64_473 rec-exp_binary64_469 e-exp-1_binary64_464 exp-0_binary64_461 rem-log-exp_binary64_460 rem-exp-log_binary64_459 cube-mult_binary64_449 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 rem-square-sqrt_binary64_431 times-frac_binary64_425 +-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 distribute-lft-out--_binary64_371
Counts
1 → 3
Iterations

Useful iterations: 7 (0.0ms)

IterNodesCost
01524
12824
25024
310424
422224
552524
6109624
722811
8641

prune6.0ms (0%)

Pruning

1 alts after pruning (1 fresh and 0 done)

PrunedKeptTotal
New213
Fresh101
Picked000
Done000
Total314
Error
17.3b
Counts
4 → 1
Compiler

Compiled 46 to 34 computations (26.1% saved)

localize12.0ms (0.1%)

Local error

Found 4 expressions with local error:

0.0b
(+.f64 (*.f64 J (*.f64 (-.f64 (exp.f64 l) (exp.f64 (neg.f64 l))) (cos.f64 (/.f64 K 2)))) U)
0.0b
(*.f64 (-.f64 (exp.f64 l) (exp.f64 (neg.f64 l))) (cos.f64 (/.f64 K 2)))
0.0b
(*.f64 J (*.f64 (-.f64 (exp.f64 l) (exp.f64 (neg.f64 l))) (cos.f64 (/.f64 K 2))))
7.0b
(-.f64 (exp.f64 l) (exp.f64 (neg.f64 l)))

rewrite135.0ms (0.8%)

Algorithm
rewrite-expression-head
Error
0.1b
Rules
14×add-sqr-sqrt_binary64_441
12×*-un-lft-identity_binary64_419
11×pow1_binary64_480 add-exp-log_binary64_457 add-cbrt-cube_binary64_455
associate-*l*_binary64_360
add-log-exp_binary64_458 add-cube-cbrt_binary64_454
pow-prod-down_binary64_490 prod-exp_binary64_468 cbrt-unprod_binary64_452 associate-*l/_binary64_362 associate-*r*_binary64_359
flip3--_binary64_423 flip--_binary64_394 cancel-sign-sub-inv_binary64_385
sinh-undef_binary64_612 difference-of-squares_binary64_388 distribute-lft-out--_binary64_371 associate-*r/_binary64_361 *-commutative_binary64_350
diff-log_binary64_511 sub-neg_binary64_412 unswap-sqr_binary64_387 sum-log_binary64_510 flip3-+_binary64_422 flip-+_binary64_393 +-commutative_binary64_349
Counts
4 → 71
Calls

4 calls:

11.0ms
(+.f64 (*.f64 J (*.f64 (-.f64 (exp.f64 l) (exp.f64 (neg.f64 l))) (cos.f64 (/.f64 K 2)))) U)
10.0ms
(*.f64 J (*.f64 (-.f64 (exp.f64 l) (exp.f64 (neg.f64 l))) (cos.f64 (/.f64 K 2))))
8.0ms
(*.f64 (-.f64 (exp.f64 l) (exp.f64 (neg.f64 l))) (cos.f64 (/.f64 K 2)))
5.0ms
(-.f64 (exp.f64 l) (exp.f64 (neg.f64 l)))
Compiler

Compiled 1796 to 765 computations (57.4% saved)

series1.6s (10.2%)

Error
0.0b
Counts
4 → 51
Calls

4 calls:

920.0ms
(+.f64 (*.f64 J (*.f64 (-.f64 (exp.f64 l) (exp.f64 (neg.f64 l))) (cos.f64 (/.f64 K 2)))) U)
427.0ms
(*.f64 J (*.f64 (-.f64 (exp.f64 l) (exp.f64 (neg.f64 l))) (cos.f64 (/.f64 K 2))))
202.0ms
(*.f64 (-.f64 (exp.f64 l) (exp.f64 (neg.f64 l))) (cos.f64 (/.f64 K 2)))
43.0ms
(-.f64 (exp.f64 l) (exp.f64 (neg.f64 l)))
Compiler

Compiled 2620 to 1972 computations (24.7% saved)

simplify453.0ms (2.8%)

Algorithm
egg-herbie
Rules
333×distribute-rgt-in_binary64_369
306×distribute-lft-in_binary64_368
219×cancel-sign-sub-inv_binary64_385
214×associate-*r*_binary64_359
182×associate-*l*_binary64_360
141×associate-+l+_binary64_352
120×+-commutative_binary64_349
119×*-commutative_binary64_350
105×exp-prod_binary64_471
103×associate-+r+_binary64_351
100×associate-*r/_binary64_361
90×distribute-rgt-neg-in_binary64_377 associate-*l/_binary64_362
81×sub-neg_binary64_412
73×exp-sum_binary64_465
69×distribute-lft-neg-in_binary64_376
56×distribute-lft-neg-out_binary64_378
53×sqr-pow_binary64_391 associate-/l*_binary64_364
51×distribute-rgt-out_binary64_372
46×associate--l+_binary64_356
45×log-prod_binary64_505
42×cube-div_binary64_448 cube-prod_binary64_447 associate-+l-_binary64_354
41×log-div_binary64_506
39×prod-exp_binary64_468 associate-+r-_binary64_353
37×neg-sub0_binary64_414
36×div-sub_binary64_424
34×neg-mul-1_binary64_415
28×distribute-rgt-neg-out_binary64_379 distribute-lft-out_binary64_370
23×pow-sqr_binary64_392
22×unswap-sqr_binary64_387 distribute-rgt-out--_binary64_373
21×exp-sqrt_binary64_472 *-rgt-identity_binary64_409
20×associate--r+_binary64_355
19×exp-diff_binary64_467
18×swap-sqr_binary64_386
15×unpow3_binary64_485
14×exp-neg_binary64_466 *-lft-identity_binary64_408
13×unsub-neg_binary64_413
11×div-exp_binary64_470 distribute-neg-in_binary64_380 associate-/l/_binary64_366
10×cube-mult_binary64_449 distribute-lft-out--_binary64_371
log-pow_binary64_508 pow-plus_binary64_482 distribute-neg-frac_binary64_383
cube-unmult_binary64_456
associate-/r*_binary64_363
+-rgt-identity_binary64_404 difference-of-squares_binary64_388 distribute-neg-out_binary64_381 distribute-rgt1-in_binary64_375 associate-/r/_binary64_365
log-rec_binary64_507 rem-log-exp_binary64_460 rem-sqrt-square_binary64_432 distribute-lft1-in_binary64_374 count-2_binary64_367
pow-base-1_binary64_479 mul-1-neg_binary64_411
sinh-def_binary64_604 unpow2_binary64_484 unpow1_binary64_477 exp-lft-sqr_binary64_474 1-exp_binary64_463 exp-1-e_binary64_462 rem-3cbrt-lft_binary64_444 sqr-neg_binary64_433 rem-square-sqrt_binary64_431 /-rgt-identity_binary64_410 sub0-neg_binary64_406 *-inverses_binary64_399 lft-mult-inverse_binary64_397 cancel-sign-sub_binary64_384 associate--r-_binary64_358
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 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 unpow0_binary64_478 unpow-1_binary64_476 exp-lft-cube_binary64_475 exp-cbrt_binary64_473 rec-exp_binary64_469 e-exp-1_binary64_464 exp-0_binary64_461 rem-exp-log_binary64_459 cube-neg_binary64_446 rem-3cbrt-rft_binary64_445 rem-cbrt-cube_binary64_443 rem-cube-cbrt_binary64_442 sqr-abs_binary64_434 times-frac_binary64_425 remove-double-neg_binary64_407 --rgt-identity_binary64_405 +-lft-identity_binary64_403 mul0-rgt_binary64_402 mul0-lft_binary64_401 div0_binary64_400 +-inverses_binary64_398 rgt-mult-inverse_binary64_396 remove-double-div_binary64_395 difference-of-sqr--1_binary64_390 difference-of-sqr-1_binary64_389 distribute-frac-neg_binary64_382 associate--l-_binary64_357
Counts
122 → 194
Iterations

Useful iterations: 2 (0.0ms)

IterNodesCost
02303110
15752837
216632674
344812674

prune268.0ms (1.7%)

Pruning

4 alts after pruning (3 fresh and 1 done)

PrunedKeptTotal
New1913194
Fresh000
Picked011
Done000
Total1914195
Error
0.0b
Counts
195 → 4
Compiler

Compiled 5105 to 2535 computations (50.3% saved)

localize13.0ms (0.1%)

Local error

Found 4 expressions with local error:

0.0b
(*.f64 l (+.f64 2 (*.f64 1/3 (*.f64 l l))))
0.1b
(*.f64 (*.f64 l (+.f64 2 (*.f64 1/3 (*.f64 l l)))) (cos.f64 (/.f64 K 2)))
0.1b
(*.f64 J (*.f64 (*.f64 l (+.f64 2 (*.f64 1/3 (*.f64 l l)))) (cos.f64 (/.f64 K 2))))
0.2b
(*.f64 1/3 (*.f64 l l))

rewrite166.0ms (1%)

Algorithm
rewrite-expression-head
Error
0b
Rules
25×pow1_binary64_480 add-exp-log_binary64_457 add-cbrt-cube_binary64_455
13×pow-prod-down_binary64_490 prod-exp_binary64_468 cbrt-unprod_binary64_452
12×add-sqr-sqrt_binary64_441
10×associate-*l*_binary64_360
add-cube-cbrt_binary64_454 *-un-lft-identity_binary64_419
associate-*r*_binary64_359 associate-*r/_binary64_361
add-log-exp_binary64_458 *-commutative_binary64_350 associate-*l/_binary64_362
flip3-+_binary64_422 flip-+_binary64_393
unswap-sqr_binary64_387
distribute-rgt-in_binary64_369 distribute-lft-in_binary64_368
Counts
4 → 84
Calls

4 calls:

12.0ms
(*.f64 J (*.f64 (*.f64 l (+.f64 2 (*.f64 1/3 (*.f64 l l)))) (cos.f64 (/.f64 K 2))))
7.0ms
(*.f64 (*.f64 l (+.f64 2 (*.f64 1/3 (*.f64 l l)))) (cos.f64 (/.f64 K 2)))
6.0ms
(*.f64 l (+.f64 2 (*.f64 1/3 (*.f64 l l))))
6.0ms
(*.f64 1/3 (*.f64 l l))
Compiler

Compiled 2313 to 1474 computations (36.3% saved)

series1.1s (6.6%)

Error
0.0b
Counts
4 → 32
Calls

4 calls:

557.0ms
(*.f64 J (*.f64 (*.f64 l (+.f64 2 (*.f64 1/3 (*.f64 l l)))) (cos.f64 (/.f64 K 2))))
329.0ms
(*.f64 (*.f64 l (+.f64 2 (*.f64 1/3 (*.f64 l l)))) (cos.f64 (/.f64 K 2)))
96.0ms
(*.f64 l (+.f64 2 (*.f64 1/3 (*.f64 l l))))
42.0ms
(*.f64 1/3 (*.f64 l l))
Compiler

Compiled 1685 to 1423 computations (15.5% saved)

simplify393.0ms (2.4%)

Algorithm
egg-herbie
Rules
842×distribute-rgt-in_binary64_369
838×distribute-lft-in_binary64_368
385×associate-*r*_binary64_359
362×associate-*l*_binary64_360
192×cancel-sign-sub-inv_binary64_385
124×distribute-rgt-neg-in_binary64_377
123×*-commutative_binary64_350
107×distribute-lft-neg-in_binary64_376
79×exp-prod_binary64_471
60×log-prod_binary64_505
58×unswap-sqr_binary64_387
53×sqr-pow_binary64_391
39×cube-prod_binary64_447 swap-sqr_binary64_386
28×sub-neg_binary64_412 *-rgt-identity_binary64_409
26×*-lft-identity_binary64_408
24×neg-mul-1_binary64_415 neg-sub0_binary64_414 distribute-rgt-out--_binary64_373
20×pow-sqr_binary64_392 +-commutative_binary64_349
17×distribute-lft-neg-out_binary64_378
14×exp-sum_binary64_465
11×distribute-rgt-out_binary64_372
10×pow-plus_binary64_482
unpow3_binary64_485 associate--l+_binary64_356 associate--r+_binary64_355 associate-+l+_binary64_352 associate-+r+_binary64_351
cube-unmult_binary64_456
unsub-neg_binary64_413 distribute-lft-out_binary64_370
cube-mult_binary64_449
distribute-neg-in_binary64_380
log-pow_binary64_508 unpow2_binary64_484 unpow1_binary64_477
log-div_binary64_506 unpow1/3_binary64_486 pow-base-1_binary64_479 exp-lft-sqr_binary64_474 exp-sqrt_binary64_472 prod-exp_binary64_468 1-exp_binary64_463 exp-1-e_binary64_462 rem-log-exp_binary64_460 cube-div_binary64_448 *-inverses_binary64_399 difference-of-squares_binary64_388 distribute-rgt-neg-out_binary64_379 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-rec_binary64_507 pow-base-0_binary64_503 unpow1/2_binary64_483 exp-to-pow_binary64_481 unpow0_binary64_478 unpow-1_binary64_476 exp-lft-cube_binary64_475 exp-cbrt_binary64_473 div-exp_binary64_470 rec-exp_binary64_469 exp-diff_binary64_467 exp-neg_binary64_466 e-exp-1_binary64_464 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 rem-sqrt-square_binary64_432 rem-square-sqrt_binary64_431 times-frac_binary64_425 div-sub_binary64_424 mul-1-neg_binary64_411 /-rgt-identity_binary64_410 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-frac_binary64_383 distribute-frac-neg_binary64_382 distribute-neg-out_binary64_381 distribute-rgt1-in_binary64_375 distribute-lft1-in_binary64_374 distribute-lft-out--_binary64_371 associate-/l/_binary64_366 associate-/r/_binary64_365 associate-/l*_binary64_364 associate-/r*_binary64_363 associate-*l/_binary64_362 associate-*r/_binary64_361 associate--r-_binary64_358 associate--l-_binary64_357 associate-+l-_binary64_354 associate-+r-_binary64_353
Counts
116 → 232
Iterations

Useful iterations: 2 (0.0ms)

IterNodesCost
01702656
14432170
218852154

prune420.0ms (2.6%)

Pruning

8 alts after pruning (7 fresh and 1 done)

PrunedKeptTotal
New2275232
Fresh022
Picked101
Done011
Total2288236
Error
0b
Counts
236 → 8
Compiler

Compiled 6607 to 4434 computations (32.9% saved)

localize13.0ms (0.1%)

Local error

Found 4 expressions with local error:

0.0b
(+.f64 (*.f64 J (*.f64 (+.f64 (*.f64 2 l) (*.f64 1/3 (pow.f64 l 3))) (cos.f64 (/.f64 K 2)))) U)
0.1b
(*.f64 (+.f64 (*.f64 2 l) (*.f64 1/3 (pow.f64 l 3))) (cos.f64 (/.f64 K 2)))
0.1b
(*.f64 J (*.f64 (+.f64 (*.f64 2 l) (*.f64 1/3 (pow.f64 l 3))) (cos.f64 (/.f64 K 2))))
0.1b
(*.f64 1/3 (pow.f64 l 3))

rewrite183.0ms (1.1%)

Algorithm
rewrite-expression-head
Error
0b
Rules
20×add-sqr-sqrt_binary64_441
16×add-exp-log_binary64_457 associate-*r*_binary64_359
13×add-cbrt-cube_binary64_455
11×pow1_binary64_480 add-cube-cbrt_binary64_454 *-un-lft-identity_binary64_419
associate-*l*_binary64_360
prod-exp_binary64_468
add-log-exp_binary64_458
cbrt-unprod_binary64_452 unswap-sqr_binary64_387
unpow-prod-down_binary64_498 cube-prod_binary64_447 pow-prod-down_binary64_490 associate-*l/_binary64_362
*-commutative_binary64_350 flip3-+_binary64_422 flip-+_binary64_393
sqr-pow_binary64_391 associate-*r/_binary64_361
pow-to-exp_binary64_488 pow-exp_binary64_487 unpow3_binary64_485 cube-mult_binary64_449 sum-log_binary64_510 +-commutative_binary64_349
Counts
4 → 82
Calls

4 calls:

11.0ms
(*.f64 J (*.f64 (+.f64 (*.f64 2 l) (*.f64 1/3 (pow.f64 l 3))) (cos.f64 (/.f64 K 2))))
9.0ms
(+.f64 (*.f64 J (*.f64 (+.f64 (*.f64 2 l) (*.f64 1/3 (pow.f64 l 3))) (cos.f64 (/.f64 K 2)))) U)
7.0ms
(*.f64 1/3 (pow.f64 l 3))
7.0ms
(*.f64 (+.f64 (*.f64 2 l) (*.f64 1/3 (pow.f64 l 3))) (cos.f64 (/.f64 K 2)))
Compiler

Compiled 2381 to 1786 computations (25% saved)

series2.2s (13.6%)

Error
0b
Counts
4 → 51
Calls

4 calls:

1.2s
(+.f64 (*.f64 J (*.f64 (+.f64 (*.f64 2 l) (*.f64 1/3 (pow.f64 l 3))) (cos.f64 (/.f64 K 2)))) U)
572.0ms
(*.f64 J (*.f64 (+.f64 (*.f64 2 l) (*.f64 1/3 (pow.f64 l 3))) (cos.f64 (/.f64 K 2))))
337.0ms
(*.f64 (+.f64 (*.f64 2 l) (*.f64 1/3 (pow.f64 l 3))) (cos.f64 (/.f64 K 2)))
57.0ms
(*.f64 1/3 (pow.f64 l 3))
Compiler

Compiled 2733 to 2267 computations (17.1% saved)

simplify523.0ms (3.2%)

Algorithm
egg-herbie
Rules
447×distribute-rgt-in_binary64_369
434×distribute-lft-in_binary64_368
326×cancel-sign-sub-inv_binary64_385
280×associate-*r*_binary64_359
272×associate-*l*_binary64_360
156×distribute-rgt-neg-in_binary64_377
144×exp-prod_binary64_471
138×distribute-lft-neg-in_binary64_376
135×unswap-sqr_binary64_387
124×log-prod_binary64_505
106×*-commutative_binary64_350
74×sqr-pow_binary64_391
66×associate-+l+_binary64_352
62×+-commutative_binary64_349
55×associate-+r+_binary64_351
51×associate-*l/_binary64_362
50×sub-neg_binary64_412 associate-*r/_binary64_361
45×cube-prod_binary64_447
41×pow-sqr_binary64_392 distribute-rgt-out_binary64_372
40×associate--l+_binary64_356
32×exp-sqrt_binary64_472
31×log-pow_binary64_508 neg-mul-1_binary64_415 neg-sub0_binary64_414
30×log-div_binary64_506 swap-sqr_binary64_386
29×unpow3_binary64_485 distribute-rgt-out--_binary64_373
28×pow-plus_binary64_482
23×*-rgt-identity_binary64_409
21×*-lft-identity_binary64_408 associate-+l-_binary64_354
20×distribute-lft-neg-out_binary64_378
18×associate--r+_binary64_355
16×associate-+r-_binary64_353
14×distribute-lft-out_binary64_370
12×exp-sum_binary64_465 associate-/l*_binary64_364
11×cube-mult_binary64_449
10×distribute-neg-in_binary64_380
unsub-neg_binary64_413
pow-base-1_binary64_479 prod-exp_binary64_468 cube-unmult_binary64_456
associate-/l/_binary64_366
rem-sqrt-square_binary64_432 distribute-rgt-neg-out_binary64_379 distribute-lft-out--_binary64_371
unpow1/3_binary64_486 exp-lft-sqr_binary64_474 difference-of-squares_binary64_388 count-2_binary64_367
unpow2_binary64_484 unpow1_binary64_477 1-exp_binary64_463 exp-1-e_binary64_462 rem-log-exp_binary64_460 cube-div_binary64_448 rem-cbrt-cube_binary64_443 rem-cube-cbrt_binary64_442 rem-square-sqrt_binary64_431 *-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 log-rec_binary64_507 pow-base-0_binary64_503 unpow1/2_binary64_483 exp-to-pow_binary64_481 unpow0_binary64_478 unpow-1_binary64_476 exp-lft-cube_binary64_475 exp-cbrt_binary64_473 div-exp_binary64_470 rec-exp_binary64_469 exp-diff_binary64_467 exp-neg_binary64_466 e-exp-1_binary64_464 exp-0_binary64_461 rem-exp-log_binary64_459 cube-neg_binary64_446 rem-3cbrt-rft_binary64_445 rem-3cbrt-lft_binary64_444 sqr-abs_binary64_434 sqr-neg_binary64_433 times-frac_binary64_425 div-sub_binary64_424 mul-1-neg_binary64_411 /-rgt-identity_binary64_410 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-frac_binary64_383 distribute-frac-neg_binary64_382 distribute-neg-out_binary64_381 distribute-rgt1-in_binary64_375 distribute-lft1-in_binary64_374 associate-/r/_binary64_365 associate-/r*_binary64_363 associate--r-_binary64_358 associate--l-_binary64_357
Counts
133 → 348
Iterations

Useful iterations: 2 (0.0ms)

IterNodesCost
01793303
14782860
217152812
346562812

prune835.0ms (5.2%)

Pruning

8 alts after pruning (6 fresh and 2 done)

PrunedKeptTotal
New3480348
Fresh066
Picked011
Done011
Total3488356
Error
0b
Counts
356 → 8
Compiler

Compiled 11000 to 7818 computations (28.9% saved)

localize14.0ms (0.1%)

Local error

Found 4 expressions with local error:

0.0b
(*.f64 l (+.f64 2 (*.f64 1/3 (*.f64 l l))))
0.1b
(*.f64 (*.f64 l (+.f64 2 (*.f64 1/3 (*.f64 l l)))) (*.f64 (cos.f64 (/.f64 K 2)) J))
0.2b
(*.f64 (cos.f64 (/.f64 K 2)) J)
0.2b
(*.f64 1/3 (*.f64 l l))

rewrite155.0ms (1%)

Algorithm
rewrite-expression-head
Error
0b
Rules
25×pow1_binary64_480 add-exp-log_binary64_457 add-cbrt-cube_binary64_455
14×add-sqr-sqrt_binary64_441
13×pow-prod-down_binary64_490 prod-exp_binary64_468 cbrt-unprod_binary64_452
10×associate-*l*_binary64_360
add-cube-cbrt_binary64_454 *-un-lft-identity_binary64_419
associate-*r*_binary64_359
add-log-exp_binary64_458 *-commutative_binary64_350 associate-*r/_binary64_361
unswap-sqr_binary64_387
flip3-+_binary64_422 associate-*l/_binary64_362 flip-+_binary64_393
distribute-rgt-in_binary64_369 distribute-lft-in_binary64_368
Counts
4 → 83
Calls

4 calls:

9.0ms
(*.f64 (*.f64 l (+.f64 2 (*.f64 1/3 (*.f64 l l)))) (*.f64 (cos.f64 (/.f64 K 2)) J))
6.0ms
(*.f64 1/3 (*.f64 l l))
6.0ms
(*.f64 l (+.f64 2 (*.f64 1/3 (*.f64 l l))))
4.0ms
(*.f64 (cos.f64 (/.f64 K 2)) J)
Compiler

Compiled 2376 to 1574 computations (33.8% saved)

series881.0ms (5.5%)

Error
0b
Counts
4 → 29
Calls

4 calls:

568.0ms
(*.f64 (*.f64 l (+.f64 2 (*.f64 1/3 (*.f64 l l)))) (*.f64 (cos.f64 (/.f64 K 2)) J))
133.0ms
(*.f64 (cos.f64 (/.f64 K 2)) J)
96.0ms
(*.f64 l (+.f64 2 (*.f64 1/3 (*.f64 l l))))
45.0ms
(*.f64 1/3 (*.f64 l l))
Compiler

Compiled 1678 to 1419 computations (15.4% saved)

simplify367.0ms (2.3%)

Algorithm
egg-herbie
Rules
611×distribute-rgt-in_binary64_369
609×distribute-lft-in_binary64_368
373×associate-*r*_binary64_359
356×associate-*l*_binary64_360
128×exp-prod_binary64_471 cancel-sign-sub-inv_binary64_385
112×*-commutative_binary64_350
105×distribute-rgt-neg-in_binary64_377
91×distribute-lft-neg-in_binary64_376
86×log-prod_binary64_505
58×associate-*l/_binary64_362 associate-*r/_binary64_361
53×sqr-pow_binary64_391
50×associate-+l+_binary64_352 associate-+r+_binary64_351
48×unswap-sqr_binary64_387
39×cube-prod_binary64_447
38×swap-sqr_binary64_386
34×+-commutative_binary64_349
32×exp-sqrt_binary64_472
28×log-div_binary64_506
27×pow-plus_binary64_482
25×*-lft-identity_binary64_408
24×neg-mul-1_binary64_415 neg-sub0_binary64_414 *-rgt-identity_binary64_409
20×pow-sqr_binary64_392
19×sub-neg_binary64_412 associate--l+_binary64_356
15×unpow3_binary64_485
14×distribute-lft-neg-out_binary64_378 distribute-rgt-out--_binary64_373
12×exp-sum_binary64_465
distribute-rgt-out_binary64_372
cube-unmult_binary64_456 associate-/l*_binary64_364 associate-+l-_binary64_354
log-pow_binary64_508 associate--r+_binary64_355 associate-+r-_binary64_353
cube-mult_binary64_449
distribute-lft-out_binary64_370
unpow1/3_binary64_486 unsub-neg_binary64_413
unpow2_binary64_484 pow-base-1_binary64_479 unpow1_binary64_477 exp-lft-sqr_binary64_474 distribute-neg-in_binary64_380 associate-/l/_binary64_366
prod-exp_binary64_468 1-exp_binary64_463 exp-1-e_binary64_462 rem-log-exp_binary64_460 cube-div_binary64_448 *-inverses_binary64_399 difference-of-squares_binary64_388 distribute-rgt-neg-out_binary64_379 distribute-rgt1-in_binary64_375 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-rec_binary64_507 pow-base-0_binary64_503 unpow1/2_binary64_483 exp-to-pow_binary64_481 unpow0_binary64_478 unpow-1_binary64_476 exp-lft-cube_binary64_475 exp-cbrt_binary64_473 div-exp_binary64_470 rec-exp_binary64_469 exp-diff_binary64_467 exp-neg_binary64_466 e-exp-1_binary64_464 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 rem-sqrt-square_binary64_432 rem-square-sqrt_binary64_431 times-frac_binary64_425 div-sub_binary64_424 mul-1-neg_binary64_411 /-rgt-identity_binary64_410 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-frac_binary64_383 distribute-frac-neg_binary64_382 distribute-neg-out_binary64_381 distribute-lft1-in_binary64_374 distribute-lft-out--_binary64_371 associate-/r/_binary64_365 associate-/r*_binary64_363 associate--r-_binary64_358 associate--l-_binary64_357
Counts
112 → 195
Iterations

Useful iterations: 2 (0.0ms)

IterNodesCost
01672230
14291802
217221792
348511792

prune358.0ms (2.2%)

Pruning

8 alts after pruning (5 fresh and 3 done)

PrunedKeptTotal
New1950195
Fresh055
Picked011
Done022
Total1958203
Error
0b
Counts
203 → 8
Compiler

Compiled 5609 to 3821 computations (31.9% saved)

regimes760.0ms (4.7%)

Accuracy

Total 0.0b remaining (72.3%)

Threshold costs 0.0b (72.3%)

Compiler

Compiled 8566 to 7277 computations (15% saved)

bsearch0.0ms (0%)

simplify3.0ms (0%)

Algorithm
egg-herbie
Rules
*-commutative_binary64_350
+-commutative_binary64_349
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 sqr-neg_binary64_433 neg-mul-1_binary64_415 neg-sub0_binary64_414 unsub-neg_binary64_413 sub-neg_binary64_412 mul-1-neg_binary64_411 /-rgt-identity_binary64_410 *-rgt-identity_binary64_409 *-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 cancel-sign-sub-inv_binary64_385 cancel-sign-sub_binary64_384 distribute-neg-frac_binary64_383 distribute-frac-neg_binary64_382 distribute-neg-out_binary64_381 distribute-neg-in_binary64_380 distribute-rgt-neg-out_binary64_379 distribute-lft-neg-out_binary64_378 distribute-rgt-neg-in_binary64_377 distribute-lft-neg-in_binary64_376
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
01320
11720
Proof
(+ f64 (* f64 h0 (* f64 (* f64 2 (sinh f64 h1)) (cos f64 (/ f64 h2 2)))) h3)

end0.0ms (0%)

sample3.7s (23.2%)

Algorithm
intervals
Results
689.0ms1641×body1024valid
507.0ms1941×body1024invalid
295.0ms4426×body128valid
269.0ms1195×body512valid
237.0ms3473×body128invalid
193.0ms1015×body512invalid
96.0ms678×body256valid
60.0ms466×body256invalid
37.0ms60×body2048valid
Compiler

Compiled 860 to 729 computations (15.2% saved)

Profiling

Loading profile data...