Herbie run
| Date: | Wednesday, May 7th, 2025 |
|---|---|
| Commit: | efe40450 on artem-rules-updates |
| Seed: | 2025127 |
| 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: | 131 803.1 MB |
Time bar (total: 2.3min)
| 26.0s | 44 583× | 2 | valid |
| 15.6s | 97 146× | 1 | valid |
| 14.5s | 144 874× | 0 | invalid |
| 10.7s | 6 051× | 5 | exit |
| 5.7s | 85 831× | 0 | valid |
| 2.5s | 3 600× | 3 | valid |
| 280.0ms | 4 152× | 0 | exit |
| 276.0ms | 1 064× | 1 | exit |
| 189.0ms | 170× | 4 | exit |
| 9.0ms | 8× | 4 | valid |
ival-tan: 11.7s (19% of total)ival-pow: 10.9s (17.7% of total)adjust: 7.0s (11.4% of total)ival-cos: 4.9s (7.9% of total)ival-mult!: 3.7s (6% of total)ival-log: 3.6s (5.8% of total)ival-sin: 3.3s (5.3% of total)ival-div!: 2.7s (4.4% of total)ival-exp: 2.2s (3.5% of total)ival-fabs: 1.7s (2.8% of total)ival-sub!: 1.7s (2.8% of total)ival-add!: 1.7s (2.7% of total)ival-expm1: 1.5s (2.5% of total)ival-log1p: 1.2s (2% of total)ival-sqrt: 1.2s (2% of total)ival-<=: 512.0ms (0.8% of total)ival-neg: 510.0ms (0.8% of total)ival-<: 505.0ms (0.8% of total)ival-atan: 327.0ms (0.5% of total)ival-and: 309.0ms (0.5% of total)ival-cbrt: 255.0ms (0.4% of total)ival-fmin: 101.0ms (0.2% of total)ival-assert: 58.0ms (0.1% of total)ival->: 1.0ms (0% of total)exact: 0.0ms (0% of total)| 242× | iter-limit |
| 101× | node-limit |
| 1× | unsound |
| 21× | fuel |
| 7× | done |
Compiled 3 134 to 1 927 computations (38.5% saved)
Compiled 420 241 to 147 985 computations (64.8% saved)
| 28× | node-limit |
Compiled 6 128 to 4 464 computations (27.2% saved)
486 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 87.0ms | n | @ | 0 | ((- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (neg (/ (+ (+ (neg (/ (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x)))) n)) (neg (log (+ 1 x)))) (log x)) n)) (/ (+ (+ (neg (/ (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x)))) n)) (neg (log (+ 1 x)))) (log x)) n) (+ (+ (neg (/ (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x)))) n)) (neg (log (+ 1 x)))) (log x)) (/ (- (* n (log (/ x (+ 1 x)))) (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x))))) n) (- (* n (log (/ x (+ 1 x)))) (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x))))) (* n (log (/ x (+ 1 x)))) n (log (/ x (+ 1 x))) (/ x (+ 1 x)) x (+ 1 x) 1 (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x)))) 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x))) (* (log (+ 1 x)) (log (+ 1 x))) (log (+ 1 x)) (* (log x) (log x)) (log x) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n)) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (+ (* (exp (neg (/ (neg (log x)) n))) (/ (- (/ 1/2 (* n n)) (/ 1/2 n)) x)) (/ (exp (neg (/ (neg (log x)) n))) n)) x) (+ (* (exp (neg (/ (neg (log x)) n))) (/ (- (/ 1/2 (* n n)) (/ 1/2 n)) x)) (/ (exp (neg (/ (neg (log x)) n))) n)) (/ (- 1 (* 1/2 (/ 1 x))) n) (- 1 (* 1/2 (/ 1 x))) (* 1/2 (/ 1 x)) (/ 1 x) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (neg (/ (+ (+ (neg (/ (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x)))) n)) (neg (log (+ 1 x)))) (log x)) n)) (/ (+ (+ (neg (/ (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x)))) n)) (neg (log (+ 1 x)))) (log x)) n) (+ (+ (neg (/ (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x)))) n)) (neg (log (+ 1 x)))) (log x)) (* -1 (/ (+ 1 (* -1 (/ (neg (log x)) n))) x)) -1 (/ (+ 1 (* -1 (/ (neg (log x)) n))) x) (+ 1 (* -1 (/ (neg (log x)) n))) (* -1 (/ (neg (log x)) n)) (/ (neg (log x)) n) (neg (log x)) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (neg (/ (+ (+ (neg (/ (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x)))) n)) (neg (log (+ 1 x)))) (log x)) n)) (/ (+ (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x)))) (* n (log (/ (+ 1 x) x)))) (* n n)) (+ (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x)))) (* n (log (/ (+ 1 x) x)))) (* n (log (/ (+ 1 x) x))) (log (/ (+ 1 x) x)) (/ (+ 1 x) x) (* n n)) |
| 76.0ms | x | @ | inf | ((- (cbrt (+ x 1)) (cbrt x)) (/ (+ (* -1/9 (cbrt x)) (+ (* (pow x 4/3) 1/3) (* (pow x -2/3) 5/81))) (* x x)) (+ (* (pow x -5/3) -1/9) (+ (* (pow x -8/3) 5/81) (* (pow x -2/3) 1/3))) (pow x -5/3) x -5/3 -1/9 (+ (* (pow x -8/3) 5/81) (* (pow x -2/3) 1/3)) (pow x -8/3) -8/3 5/81 (* (pow x -2/3) 1/3) (pow x -2/3) -2/3 1/3 (- (cbrt (+ x 1)) (cbrt x)) (neg (- (exp (* (log x) 1/3)) 1)) (- (exp (* (log x) 1/3)) 1) (pow x 1/3) (- (cbrt (+ x 1)) (cbrt x)) (* (pow (/ 1 x) 2/3) 1/3) (pow (/ 1 x) 2/3) (/ 1 x) 1 2/3 (- (cbrt (+ x 1)) (cbrt x)) (* (exp (log (pow x -2/3))) 1/3) (exp (log (pow x -2/3))) (log (pow x -2/3)) (- (cbrt (+ x 1)) (cbrt x)) (/ (+ (* (exp (/ (* (log x) 4) 3)) 1/3) (* -1/9 (cbrt x))) (* x x)) (+ (* (exp (/ (* (log x) 4) 3)) 1/3) (* -1/9 (cbrt x))) (exp (/ (* (log x) 4) 3)) (/ (* (log x) 4) 3) (* (log x) 4) (log x) 4 3 (* -1/9 (cbrt x)) (cbrt x) (* x x)) |
| 66.0ms | x | @ | -inf | ((/ (pow (/ (sin x) x) 2) (+ (cos x) 1)) (pow (/ (sin x) x) 2) (/ (sin x) x) (sin x) x 2 (+ (cos x) 1) (cos x) 1 (* (/ (- 1 (cos x)) x) (/ 1 x)) (/ (- 1 (cos x)) x) (* 1/2 x) 1/2 (/ 1 x) (/ (- (* (/ 1 x) (* x x)) (* x (cos x))) (* (* x x) x)) (- (* (/ 1 x) (* x x)) (* x (cos x))) (* (/ 1 x) (* x x)) (* x x) (* x (cos x)) (cos x) (* (* x x) x) (* (* (- 1 (cos x)) (/ 1 x)) (/ 1 x)) (* (- 1 (cos x)) (/ 1 x)) (- 1 (cos x)) (/ (+ (* (/ (neg (cos x)) x) x) (* (/ 1 x) x)) (* x x)) (+ (* (/ (neg (cos x)) x) x) (* (/ 1 x) x)) (/ (neg (cos x)) x) (neg (cos x)) (* (/ 1 x) x)) |
| 62.0ms | n | @ | 0 | ((- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (neg (/ (+ (+ (neg (/ (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x)))) n)) (neg (log (+ 1 x)))) (log x)) n)) (/ (+ (+ (neg (/ (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x)))) n)) (neg (log (+ 1 x)))) (log x)) n) (+ (+ (neg (/ (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x)))) n)) (neg (log (+ 1 x)))) (log x)) (+ (neg (/ (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x)))) n)) (neg (log (+ 1 x)))) (neg (/ (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x)))) n)) (/ (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x)))) n) (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x)))) 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x))) (* (log (+ 1 x)) (log (+ 1 x))) (log (+ 1 x)) (+ 1 x) 1 x (* (log x) (log x)) (log x) n (neg (log (+ 1 x))) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (log (/ (+ 1 x) x)) n) (log (/ (+ 1 x) x)) (/ (+ 1 x) x) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (pow (+ x 1) (/ 1 n)) (+ x 1) (/ 1 n) (pow x (/ 1 n)) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (pow (+ x 1) (/ 1 n)) (+ (/ x n) 1) (/ x n) (pow x (/ 1 n)) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (+ (* (exp (neg (/ (neg (log x)) n))) (/ (- (/ 1/2 (* n n)) (/ 1/2 n)) x)) (/ (exp (neg (/ (neg (log x)) n))) n)) x) (+ (* (exp (neg (/ (neg (log x)) n))) (/ (- (/ 1/2 (* n n)) (/ 1/2 n)) x)) (/ (exp (neg (/ (neg (log x)) n))) n)) (exp (neg (/ (neg (log x)) n))) (neg (/ (neg (log x)) n)) (/ (neg (log x)) n) (neg (log x)) (/ (- (/ 1/2 (* n n)) (/ 1/2 n)) x) (- (/ 1/2 (* n n)) (/ 1/2 n)) (/ 1/2 (* n n)) (* n n) (/ 1/2 n) (/ (exp (neg (/ (neg (log x)) n))) n)) |
| 51.0ms | n | @ | -inf | ((- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (neg (/ (+ (+ (neg (/ (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x)))) n)) (neg (log (+ 1 x)))) (log x)) n)) (/ (+ (+ (neg (/ (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x)))) n)) (neg (log (+ 1 x)))) (log x)) n) (+ (+ (neg (/ (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x)))) n)) (neg (log (+ 1 x)))) (log x)) (+ (neg (/ (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x)))) n)) (neg (log (+ 1 x)))) (neg (/ (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x)))) n)) (/ (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x)))) n) (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x)))) 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x))) (* (log (+ 1 x)) (log (+ 1 x))) (log (+ 1 x)) (+ 1 x) 1 x (* (log x) (log x)) (log x) n (neg (log (+ 1 x))) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (log (/ (+ 1 x) x)) n) (log (/ (+ 1 x) x)) (/ (+ 1 x) x) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (pow (+ x 1) (/ 1 n)) (+ x 1) (/ 1 n) (pow x (/ 1 n)) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (pow (+ x 1) (/ 1 n)) (+ (/ x n) 1) (/ x n) (pow x (/ 1 n)) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (+ (* (exp (neg (/ (neg (log x)) n))) (/ (- (/ 1/2 (* n n)) (/ 1/2 n)) x)) (/ (exp (neg (/ (neg (log x)) n))) n)) x) (+ (* (exp (neg (/ (neg (log x)) n))) (/ (- (/ 1/2 (* n n)) (/ 1/2 n)) x)) (/ (exp (neg (/ (neg (log x)) n))) n)) (exp (neg (/ (neg (log x)) n))) (neg (/ (neg (log x)) n)) (/ (neg (log x)) n) (neg (log x)) (/ (- (/ 1/2 (* n n)) (/ 1/2 n)) x) (- (/ 1/2 (* n n)) (/ 1/2 n)) (/ 1/2 (* n n)) (* n n) (/ 1/2 n) (/ (exp (neg (/ (neg (log x)) n))) n)) |
43 calls:
| 764.0ms | x |
| 206.0ms | eps |
| 139.0ms | N |
| 123.0ms | b |
| 113.0ms | b_2 |
Compiled 1 616 to 1 771 computations (-9.6% saved)
Compiled 55 481 to 46 068 computations (17% saved)
| 134× | binary-search |
| 14× | left-value |
| 132× | narrow-enough |
| 2× | predicate-same |
| 420.0ms | 6 264× | 0 | valid |
| 203.0ms | 1 097× | 1 | valid |
| 164.0ms | 568× | 2 | valid |
| 98.0ms | 1 462× | 0 | invalid |
| 5.0ms | 71× | 0 | exit |
| 4.0ms | 23× | 3 | valid |
Compiled 35 337 to 35 759 computations (-1.2% saved)
ival-pow: 130.0ms (20.7% of total)ival-mult!: 111.0ms (17.7% of total)ival-sqrt: 106.0ms (16.9% of total)adjust: 60.0ms (9.6% of total)ival-div!: 54.0ms (8.6% of total)ival-cos: 42.0ms (6.7% of total)ival-neg: 36.0ms (5.7% of total)ival-sub!: 33.0ms (5.3% of total)ival-add!: 30.0ms (4.8% of total)ival-exp: 9.0ms (1.4% of total)ival-expm1: 6.0ms (1% of total)ival-log1p: 4.0ms (0.6% of total)ival-log: 3.0ms (0.5% of total)ival-cbrt: 2.0ms (0.3% of total)| 28× | search |
| Probability | Valid | Unknown | Precondition | Infinite | Domain | Can't | Iter |
|---|---|---|---|---|---|---|---|
| 0% | 0% | 61.1% | 38.9% | 0% | 0% | 0% | 0 |
| 7.4% | 4.5% | 56.6% | 38.9% | 0% | 0% | 0% | 1 |
| 22.3% | 13.6% | 47.5% | 38.9% | 0% | 0% | 0% | 2 |
| 40.2% | 23.5% | 34.9% | 38.9% | 0% | 2.7% | 0% | 3 |
| 53.4% | 31.1% | 27.2% | 38.9% | 0% | 2.8% | 0% | 4 |
| 63% | 36.3% | 21.3% | 38.9% | 0% | 3.6% | 0% | 5 |
| 65.9% | 37.5% | 19.4% | 38.9% | 0% | 4.2% | 0% | 6 |
| 70.4% | 38.8% | 16.3% | 38.9% | 0% | 6% | 0% | 7 |
| 73.6% | 40.2% | 14.4% | 38.9% | 0% | 6.5% | 0% | 8 |
| 76.3% | 40.9% | 12.7% | 38.9% | 0% | 7.5% | 0% | 9 |
| 78.4% | 41.4% | 11.4% | 38.9% | 0% | 8.3% | 0% | 10 |
| 81.1% | 42.4% | 9.9% | 38.9% | 0% | 8.8% | 0% | 11 |
| 82.3% | 42.7% | 9.2% | 38.9% | 0% | 9.3% | 0% | 12 |
Compiled 483 to 337 computations (30.2% saved)
Loading profile data...