Herbie run
| Date: | Tuesday, May 20th, 2025 |
|---|---|
| Commit: | cd6c75cb on new-rules-taylor-LAST |
| Seed: | 2025140 |
| Parameters: | 256 points for 4 iterations |
| Flags: | reduce:regimesreduce:binary-searchreduce:branch-expressionssetup:searchrules:arithmeticrules:polynomialsrules:fractionsrules:exponentsrules:trigonometryrules:hyperbolicrules:numericsrules:specialrules:boolsrules:branchesgenerate:rrgenerate:taylorgenerate:proofs default |
| Memory: | 149 209.0 MB |
Time bar (total: 2.1min)
| 21.8s | 292 918× | 0 | valid |
| 8.4s | 35 731× | 1 | valid |
| 7.1s | 17 701× | 2 | valid |
| 349.0ms | 4 153× | 0 | invalid |
| 212.0ms | 402× | 3 | valid |
| 105.0ms | 1 016× | 0 | exit |
| 50.0ms | 101× | 4 | exit |
| 50.0ms | 101× | 3 | exit |
| 4.0ms | 32× | 1 | exit |
ival-mult!: 5.6s (21.6% of total)ival-pow: 4.6s (17.9% of total)ival-div!: 2.7s (10.4% of total)adjust: 2.4s (9.1% of total)ival-sub!: 2.3s (9% of total)ival-add!: 2.1s (8.2% of total)ival-cos: 1.9s (7.3% of total)ival-sin: 1.9s (7.2% of total)ival-exp: 631.0ms (2.4% of total)ival-sqrt: 589.0ms (2.3% of total)ival-neg: 385.0ms (1.5% of total)ival-pow2: 323.0ms (1.3% of total)ival-expm1: 132.0ms (0.5% of total)ival-log1p: 87.0ms (0.3% of total)ival-tan: 84.0ms (0.3% of total)ival-atan: 83.0ms (0.3% of total)ival-hypot: 18.0ms (0.1% of total)ival-<=: 14.0ms (0.1% of total)ival-and: 8.0ms (0% of total)ival-if: 4.0ms (0% of total)ival-fabs: 4.0ms (0% of total)ival-==: 2.0ms (0% of total)ival-assert: 1.0ms (0% of total)const: 0.0ms (0% of total)ival-<: 0.0ms (0% of total)| 372× | iter-limit |
| 112× | node-limit |
| 22× | unsound |
| 11× | saturated |
Compiled 1 304 723 to 292 065 computations (77.6% saved)
| 25× | fuel |
| 17× | done |
Compiled 3 974 to 2 107 computations (47% saved)
| 37× | node-limit |
| 5× | saturated |
Compiled 11 838 to 8 671 computations (26.8% saved)
| 43× | search |
| 2× | random |
| Probability | Valid | Unknown | Precondition | Infinite | Domain | Can't | Iter |
|---|---|---|---|---|---|---|---|
| 0% | 0% | 54.5% | 45.5% | 0% | 0% | 0% | 0 |
| 21.4% | 11.7% | 42.9% | 45.5% | 0% | 0% | 0% | 1 |
| 37.4% | 20.4% | 34.1% | 45.5% | 0% | 0% | 0% | 2 |
| 48.7% | 26.2% | 27.7% | 45.5% | 0% | 0.6% | 0% | 3 |
| 57.7% | 30.7% | 22.6% | 45.5% | 0% | 1.2% | 0% | 4 |
| 71.2% | 37.7% | 15.3% | 45.5% | 0% | 1.6% | 0% | 5 |
| 72.9% | 38.4% | 14.3% | 45.5% | 0% | 1.8% | 0% | 6 |
| 77.9% | 40.7% | 11.6% | 45.5% | 0% | 2.2% | 0% | 7 |
| 81.5% | 42.6% | 9.7% | 45.5% | 0% | 2.3% | 0% | 8 |
| 84.1% | 43.8% | 8.3% | 45.5% | 0% | 2.5% | 0% | 9 |
| 86.2% | 44.6% | 7.2% | 45.5% | 0% | 2.7% | 0% | 10 |
| 88.2% | 45.6% | 6.1% | 45.5% | 0% | 2.8% | 0% | 11 |
| 89.1% | 45.9% | 5.6% | 45.5% | 0% | 2.9% | 0% | 12 |
Compiled 1 402 to 721 computations (48.6% saved)
Compiled 64 053 to 44 860 computations (30% saved)
96 calls:
| 550.0ms | b |
| 398.0ms | x |
| 287.0ms | a |
| 206.0ms | v |
| 187.0ms | c |
Compiled 3 956 to 3 540 computations (10.5% saved)
| 184× | binary-search |
| 36× | left-value |
| 176× | narrow-enough |
| 8× | predicate-same |
| 926.0ms | 10 245× | 0 | valid |
| 411.0ms | 1 359× | 1 | valid |
| 329.0ms | 518× | 2 | valid |
| 198.0ms | 1 526× | 0 | invalid |
| 24.0ms | 22× | 3 | valid |
Compiled 74 656 to 66 944 computations (10.3% saved)
ival-mult!: 408.0ms (29.3% of total)ival-pow: 398.0ms (28.6% of total)ival-neg: 167.0ms (12% of total)ival-div!: 127.0ms (9.1% of total)ival-add!: 91.0ms (6.5% of total)adjust: 75.0ms (5.4% of total)ival-sub!: 57.0ms (4.1% of total)ival-exp: 41.0ms (2.9% of total)ival-sqrt: 29.0ms (2.1% of total)162 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 132.0ms | i | @ | inf | ((/ (* (- (exp (* (log (+ 1 (/ (/ 1 n) (/ 1 i)))) n)) 1) 100) (/ (/ 1 n) (/ 1 i))) (* (- (exp (* (log (+ 1 (/ (/ 1 n) (/ 1 i)))) n)) 1) 100) (- (exp (* (log (+ 1 (/ (/ 1 n) (/ 1 i)))) n)) 1) (* (log (+ 1 (/ (/ 1 n) (/ 1 i)))) n) (log (+ 1 (/ (/ 1 n) (/ 1 i)))) (/ (/ 1 n) (/ 1 i)) (/ 1 n) 1 n (/ 1 i) i 100 (* (* (- (exp (* (log (- (/ i n) -1)) n)) 1) n) (/ 100 i)) (* (- (exp (* (log (- (/ i n) -1)) n)) 1) n) (- (exp (* (log (- (/ i n) -1)) n)) 1) (* (log (- (/ i n) -1)) n) (log (- (/ i n) -1)) (- (/ i n) -1) (/ i n) -1 (/ 100 i) (* (* (/ n i) 100) (- (exp (* (log (- (/ i n) -1)) n)) 1)) (* (/ n i) 100) (/ n i) (* (* (- (exp (* (log (fabs (- (/ i n) -1))) n)) 1) (/ 100 i)) n) (* (- (exp (* (log (fabs (- (/ i n) -1))) n)) 1) (/ 100 i)) (- (exp (* (log (fabs (- (/ i n) -1))) n)) 1) (* (log (fabs (- (/ i n) -1))) n) (log (fabs (- (/ i n) -1))) (fabs (- (/ i n) -1)) (/ (* (- (exp (* (log (fabs (- (/ i n) -1))) n)) 1) 100) (/ i n)) (* (- (exp (* (log (fabs (- (/ i n) -1))) n)) 1) 100)) |
| 88.0ms | x | @ | inf | ((/ (/ (- 1 (* (/ (neg (* (+ (* 1/8 (pow (cos (+ x x)) 3)) 1/8) (cos x))) (+ (* (+ (* (cos (+ x x)) 1/2) -1/2) (* 1/2 (cos (+ x x)))) 1/4)) (/ (neg (* (+ (* 1/8 (pow (cos (+ x x)) 3)) 1/8) (cos x))) (+ (* (+ (* (cos (+ x x)) 1/2) -1/2) (* 1/2 (cos (+ x x)))) 1/4)))) (- 1 (/ (neg (* (+ (* 1/8 (pow (cos (+ x x)) 3)) 1/8) (cos x))) (+ (* (+ (* (cos (+ x x)) 1/2) -1/2) (* 1/2 (cos (+ x x)))) 1/4)))) (+ 1 (- (+ 1/2 (* 1/2 (cos (* 2 x)))) (* 1 (neg (cos x)))))) (/ (- 1 (* (/ (neg (* (+ (* 1/8 (pow (cos (+ x x)) 3)) 1/8) (cos x))) (+ (* (+ (* (cos (+ x x)) 1/2) -1/2) (* 1/2 (cos (+ x x)))) 1/4)) (/ (neg (* (+ (* 1/8 (pow (cos (+ x x)) 3)) 1/8) (cos x))) (+ (* (+ (* (cos (+ x x)) 1/2) -1/2) (* 1/2 (cos (+ x x)))) 1/4)))) (- 1 (/ (neg (* (+ (* 1/8 (pow (cos (+ x x)) 3)) 1/8) (cos x))) (+ (* (+ (* (cos (+ x x)) 1/2) -1/2) (* 1/2 (cos (+ x x)))) 1/4)))) (- 1 (* (/ (neg (* (+ (* 1/8 (pow (cos (+ x x)) 3)) 1/8) (cos x))) (+ (* (+ (* (cos (+ x x)) 1/2) -1/2) (* 1/2 (cos (+ x x)))) 1/4)) (/ (neg (* (+ (* 1/8 (pow (cos (+ x x)) 3)) 1/8) (cos x))) (+ (* (+ (* (cos (+ x x)) 1/2) -1/2) (* 1/2 (cos (+ x x)))) 1/4)))) 1 (* (/ (neg (* (+ (* 1/8 (pow (cos (+ x x)) 3)) 1/8) (cos x))) (+ (* (+ (* (cos (+ x x)) 1/2) -1/2) (* 1/2 (cos (+ x x)))) 1/4)) (/ (neg (* (+ (* 1/8 (pow (cos (+ x x)) 3)) 1/8) (cos x))) (+ (* (+ (* (cos (+ x x)) 1/2) -1/2) (* 1/2 (cos (+ x x)))) 1/4))) (/ (neg (* (+ (* 1/8 (pow (cos (+ x x)) 3)) 1/8) (cos x))) (+ (* (+ (* (cos (+ x x)) 1/2) -1/2) (* 1/2 (cos (+ x x)))) 1/4)) (neg (* (+ (* 1/8 (pow (cos (+ x x)) 3)) 1/8) (cos x))) (* (+ (* 1/8 (pow (cos (+ x x)) 3)) 1/8) (cos x)) (+ (* 1/8 (pow (cos (+ x x)) 3)) 1/8) 1/8 (pow (cos (+ x x)) 3) (cos (+ x x)) (+ x x) x 3 (cos x) (+ (* (+ (* (cos (+ x x)) 1/2) -1/2) (* 1/2 (cos (+ x x)))) 1/4) (+ (* (cos (+ x x)) 1/2) -1/2) 1/2 -1/2 (* 1/2 (cos (+ x x))) 1/4 (- 1 (/ (neg (* (+ (* 1/8 (pow (cos (+ x x)) 3)) 1/8) (cos x))) (+ (* (+ (* (cos (+ x x)) 1/2) -1/2) (* 1/2 (cos (+ x x)))) 1/4))) (+ 1 (- (+ 1/2 (* 1/2 (cos (* 2 x)))) (* 1 (neg (cos x))))) (- (+ 1/2 (* 1/2 (cos (* 2 x)))) (* 1 (neg (cos x)))) (+ 1/2 (* 1/2 (cos (* 2 x)))) (* 1/2 (cos (* 2 x))) (cos (* 2 x)) (* 2 x) 2 (* 1 (neg (cos x))) (neg (cos x)) (/ (- (pow (cos x) 3) -1) (+ (* (- (cos x) -1) (cos x)) 1)) (- (pow (cos x) 3) -1) (pow (cos x) 3) -1 (+ (* (- (cos x) -1) (cos x)) 1) (- (cos x) -1) (* (- 1 (pow (cos x) 3)) (/ 1 (+ (* (cos x) (+ (cos x) 1)) 1))) (- 1 (pow (cos x) 3)) (/ 1 (+ (* (cos x) (+ (cos x) 1)) 1)) (+ (* (cos x) (+ (cos x) 1)) 1) (+ (cos x) 1) (/ (- (- 1 (cosh (* (log (cos x)) 3))) (sinh (* (log (cos x)) 3))) (+ (* (cos x) (+ (cos x) 1)) 1)) (- (- 1 (cosh (* (log (cos x)) 3))) (sinh (* (log (cos x)) 3))) (- 1 (cosh (* (log (cos x)) 3))) (cosh (* (log (cos x)) 3)) (* (log (cos x)) 3) (log (cos x)) (sinh (* (log (cos x)) 3)) (/ (+ 1 (pow (neg (cos x)) 3)) (+ 1 (/ (* (- 1 (neg (/ (cos x) (+ (* (cos (+ x x)) 1/2) 1/2)))) (- 1/4 (pow (* (cos (+ x x)) 1/2) 2))) (- 1/2 (* (cos (+ x x)) 1/2))))) (+ 1 (pow (neg (cos x)) 3)) (pow (neg (cos x)) 3) (+ 1 (/ (* (- 1 (neg (/ (cos x) (+ (* (cos (+ x x)) 1/2) 1/2)))) (- 1/4 (pow (* (cos (+ x x)) 1/2) 2))) (- 1/2 (* (cos (+ x x)) 1/2)))) (/ (* (- 1 (neg (/ (cos x) (+ (* (cos (+ x x)) 1/2) 1/2)))) (- 1/4 (pow (* (cos (+ x x)) 1/2) 2))) (- 1/2 (* (cos (+ x x)) 1/2))) (* (- 1 (neg (/ (cos x) (+ (* (cos (+ x x)) 1/2) 1/2)))) (- 1/4 (pow (* (cos (+ x x)) 1/2) 2))) (- 1 (neg (/ (cos x) (+ (* (cos (+ x x)) 1/2) 1/2)))) (neg (/ (cos x) (+ (* (cos (+ x x)) 1/2) 1/2))) (/ (cos x) (+ (* (cos (+ x x)) 1/2) 1/2)) (+ (* (cos (+ x x)) 1/2) 1/2) (- 1/4 (pow (* (cos (+ x x)) 1/2) 2)) (pow (* (cos (+ x x)) 1/2) 2) (* (cos (+ x x)) 1/2) (- 1/2 (* (cos (+ x x)) 1/2))) |
| 82.0ms | a | @ | inf | ((+ (/ b (+ (* (/ d c) d) c)) (/ a (- (neg d) (/ (* c c) d)))) (/ b (+ (* (/ d c) d) c)) b (+ (* (/ d c) d) c) (/ d c) d c (/ a (- (neg d) (/ (* c c) d))) a (- (neg d) (/ (* c c) d)) (neg d) (/ (* c c) d) (* c c) (* (/ 1 (+ (* d d) (* c c))) (- (* c b) (* d a))) (/ 1 (+ (* d d) (* c c))) 1 (+ (* d d) (* c c)) (- (* c b) (* d a)) (* c b) (* d a) (* (/ (- (* b c) (* d a)) (+ (* (/ d c) d) c)) (/ 1 c)) (/ (- (* b c) (* d a)) (+ (* (/ d c) d) c)) (- (* b c) (* d a)) (* b c) (/ 1 c) (/ (/ (- (* c b) (* a d)) (* (+ (* (/ d (* c c)) d) 1) c)) c) (/ (- (* c b) (* a d)) (* (+ (* (/ d (* c c)) d) 1) c)) (- (* c b) (* a d)) (* a d) (* (+ (* (/ d (* c c)) d) 1) c) (+ (* (/ d (* c c)) d) 1) (/ d (* c c)) (+ (* a (/ (neg d) (* (* (+ (* c (/ c (* d d))) 1) d) d))) (/ b (+ c (/ (* d d) c)))) (/ (neg d) (* (* (+ (* c (/ c (* d d))) 1) d) d)) (* (* (+ (* c (/ c (* d d))) 1) d) d) (* (+ (* c (/ c (* d d))) 1) d) (+ (* c (/ c (* d d))) 1) (/ c (* d d)) (* d d) (/ b (+ c (/ (* d d) c))) (+ c (/ (* d d) c)) (/ (* d d) c)) |
| 82.0ms | x | @ | inf | ((/ (- (* (+ 1 (/ 1 eps)) (exp (neg (* (- 1 eps) x)))) (* (- (exp (neg (log eps))) 1) (exp (neg (* (+ 1 eps) x))))) 2) (- (* (+ 1 (/ 1 eps)) (exp (neg (* (- 1 eps) x)))) (* (- (exp (neg (log eps))) 1) (exp (neg (* (+ 1 eps) x))))) (* (+ 1 (/ 1 eps)) (exp (neg (* (- 1 eps) x)))) (+ 1 (/ 1 eps)) 1 (/ 1 eps) eps (exp (neg (* (- 1 eps) x))) (neg (* (- 1 eps) x)) (* (- 1 eps) x) (- 1 eps) x (* (- (exp (neg (log eps))) 1) (exp (neg (* (+ 1 eps) x)))) (- (exp (neg (log eps))) 1) (neg (log eps)) (log eps) (exp (neg (* (+ 1 eps) x))) (neg (* (+ 1 eps) x)) (* (+ 1 eps) x) (+ 1 eps) 2 (* (+ (* (exp (* (- eps 1) x)) (- (/ 1 eps) -1)) (* (/ (- eps 1) (* eps eps)) (* eps (exp (* (- -1 eps) x))))) 1/2) (+ (* (exp (* (- eps 1) x)) (- (/ 1 eps) -1)) (* (/ (- eps 1) (* eps eps)) (* eps (exp (* (- -1 eps) x))))) (exp (* (- eps 1) x)) (* (- eps 1) x) (- eps 1) (- (/ 1 eps) -1) -1 (* (/ (- eps 1) (* eps eps)) (* eps (exp (* (- -1 eps) x)))) (/ (- eps 1) (* eps eps)) (* eps eps) (* eps (exp (* (- -1 eps) x))) (exp (* (- -1 eps) x)) (* (- -1 eps) x) (- -1 eps) 1/2 (* (+ (* (exp (* (- eps 1) x)) (- (/ 1 eps) -1)) (* (exp (* x (- -1 eps))) (/ eps (* (/ 1 (- eps 1)) (* eps eps))))) 1/2) (+ (* (exp (* (- eps 1) x)) (- (/ 1 eps) -1)) (* (exp (* x (- -1 eps))) (/ eps (* (/ 1 (- eps 1)) (* eps eps))))) (* (exp (* x (- -1 eps))) (/ eps (* (/ 1 (- eps 1)) (* eps eps)))) (exp (* x (- -1 eps))) (* x (- -1 eps)) (/ eps (* (/ 1 (- eps 1)) (* eps eps))) (* (/ 1 (- eps 1)) (* eps eps)) (/ 1 (- eps 1)) (* (+ (* (- 1 (/ 1 (* eps eps))) (* (exp (* (- eps 1) x)) (/ eps (- eps 1)))) (* (exp (* (- -1 eps) x)) (- 1 (/ 1 eps)))) 1/2) (+ (* (- 1 (/ 1 (* eps eps))) (* (exp (* (- eps 1) x)) (/ eps (- eps 1)))) (* (exp (* (- -1 eps) x)) (- 1 (/ 1 eps)))) (- 1 (/ 1 (* eps eps))) (/ 1 (* eps eps)) (* (exp (* (- eps 1) x)) (/ eps (- eps 1))) (/ eps (- eps 1)) (* (exp (* (- -1 eps) x)) (- 1 (/ 1 eps))) (- 1 (/ 1 eps)) (* (+ (* (exp (* (- eps 1) x)) (/ (* (+ (* eps eps) -1) (/ eps (- eps 1))) (* eps eps))) (/ (- 1 (/ 1 eps)) (exp (* (- eps -1) x)))) 1/2) (+ (* (exp (* (- eps 1) x)) (/ (* (+ (* eps eps) -1) (/ eps (- eps 1))) (* eps eps))) (/ (- 1 (/ 1 eps)) (exp (* (- eps -1) x)))) (/ (* (+ (* eps eps) -1) (/ eps (- eps 1))) (* eps eps)) (* (+ (* eps eps) -1) (/ eps (- eps 1))) (+ (* eps eps) -1) (/ (- 1 (/ 1 eps)) (exp (* (- eps -1) x))) (exp (* (- eps -1) x)) (* (- eps -1) x) (- eps -1)) |
| 79.0ms | c | @ | inf | ((/ (+ (* (sqrt (- 1 (* (* a 4) (/ (/ c b) b)))) (fabs b)) (neg b)) (+ a a)) (+ (* (sqrt (- 1 (* (* a 4) (/ (/ c b) b)))) (fabs b)) (neg b)) (sqrt (- 1 (* (* a 4) (/ (/ c b) b)))) (- 1 (* (* a 4) (/ (/ c b) b))) 1 (* (* a 4) (/ (/ c b) b)) (* a 4) a 4 (/ (/ c b) b) (/ c b) c b (fabs b) (neg b) (+ a a) (* (- (sqrt (+ (* -4 (* c a)) (* b b))) b) (/ 1/2 a)) (- (sqrt (+ (* -4 (* c a)) (* b b))) b) (sqrt (+ (* -4 (* c a)) (* b b))) (+ (* -4 (* c a)) (* b b)) -4 (* c a) (* b b) (/ 1/2 a) 1/2 (/ (+ (* (sqrt (- 1 (* (* a 4) (/ 1 (/ (* b b) c))))) (fabs b)) (neg b)) (* 2 a)) (+ (* (sqrt (- 1 (* (* a 4) (/ 1 (/ (* b b) c))))) (fabs b)) (neg b)) (sqrt (- 1 (* (* a 4) (/ 1 (/ (* b b) c))))) (- 1 (* (* a 4) (/ 1 (/ (* b b) c)))) (* (* a 4) (/ 1 (/ (* b b) c))) (/ 1 (/ (* b b) c)) (/ (* b b) c) (* 2 a) 2 (/ (/ (+ (* (+ a a) (neg b)) (* (sqrt (+ (* (* c a) -4) (* b b))) (+ a a))) (+ a a)) (+ a a)) (/ (+ (* (+ a a) (neg b)) (* (sqrt (+ (* (* c a) -4) (* b b))) (+ a a))) (+ a a)) (+ (* (+ a a) (neg b)) (* (sqrt (+ (* (* c a) -4) (* b b))) (+ a a))) (* (sqrt (+ (* (* c a) -4) (* b b))) (+ a a)) (sqrt (+ (* (* c a) -4) (* b b))) (+ (* (* c a) -4) (* b b)) (/ (- (/ (* b b) (- (neg b) (sqrt (+ (* -4 (* c a)) (* b b))))) (/ (+ (* -4 (* c a)) (* b b)) (- (neg b) (sqrt (+ (* -4 (* c a)) (* b b)))))) (+ a a)) (- (/ (* b b) (- (neg b) (sqrt (+ (* -4 (* c a)) (* b b))))) (/ (+ (* -4 (* c a)) (* b b)) (- (neg b) (sqrt (+ (* -4 (* c a)) (* b b)))))) (/ (* b b) (- (neg b) (sqrt (+ (* -4 (* c a)) (* b b))))) (- (neg b) (sqrt (+ (* -4 (* c a)) (* b b)))) (/ (+ (* -4 (* c a)) (* b b)) (- (neg b) (sqrt (+ (* -4 (* c a)) (* b b)))))) |
Loading profile data...