Herbie run

Date:Thursday, May 15th, 2025
Commit:1b7c2246 on main
Seed:2025135
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:133 783.7 MB

Time bar (total: 2.4min)

sample1.6min (65.1%)

Memory
1 540.9MiB live, 84 562.4MiB allocated; 28.7s collecting garbage
Samples
24.6s44 630×2valid
16.4s96 856×1valid
15.0s145 899×0invalid
10.8s5 834×5exit
7.4s86 034×0valid
2.7s3 641×3valid
299.0ms4 171×0exit
222.0ms1 074×1exit
156.0ms153×4exit
8.0ms7×4valid
Precisions
Click to see histograms. Total time spent on operations: 1.1min
ival-tan: 12.5s (19.5% of total)
ival-pow: 10.9s (17% of total)
adjust: 6.6s (10.2% of total)
ival-mult!: 4.9s (7.7% of total)
ival-cos: 3.9s (6.1% of total)
ival-sin: 3.9s (6% of total)
ival-log: 3.5s (5.4% of total)
ival-div!: 3.0s (4.7% of total)
ival-fabs: 2.3s (3.6% of total)
ival-sub!: 2.2s (3.4% of total)
ival-exp: 2.0s (3.1% of total)
ival-add!: 1.9s (2.9% of total)
ival-expm1: 1.7s (2.6% of total)
ival-sqrt: 1.3s (2.1% of total)
ival-log1p: 1.1s (1.7% of total)
ival-neg: 557.0ms (0.9% of total)
ival-atan: 482.0ms (0.7% of total)
ival-<: 449.0ms (0.7% of total)
ival-and: 328.0ms (0.5% of total)
ival-<=: 307.0ms (0.5% of total)
ival-cbrt: 286.0ms (0.4% of total)
ival-fmin: 87.0ms (0.1% of total)
ival-assert: 65.0ms (0.1% of total)
ival->: 8.0ms (0% of total)
exact: 0.0ms (0% of total)
Bogosity

rewrite22.6s (15.7%)

Memory
156.6MiB live, 18 916.4MiB allocated; 8.5s collecting garbage
Stop Event
248×iter-limit
105×node-limit
1×saturated
Counts
10 763 → 28 591

derivations5.7s (4%)

Memory
80.5MiB live, 4 885.9MiB allocated; 642ms collecting garbage
Stop Event
20×fuel
8×done
Compiler

Compiled 2 907 to 1 784 computations (38.6% saved)

eval4.7s (3.2%)

Memory
84.2MiB live, 5 730.5MiB allocated; 1.8s collecting garbage
Compiler

Compiled 436 318 to 148 406 computations (66% saved)

preprocess4.4s (3%)

Memory
-391.2MiB live, 4 407.8MiB allocated; 1.0s collecting garbage
Stop Event
28×node-limit
1×iter-limit
Compiler

Compiled 5 643 to 4 119 computations (27% saved)

series4.2s (2.9%)

Memory
226.3MiB live, 5 417.4MiB allocated; 847ms collecting garbage
Counts
2 414 → 8 349
Calls

495 calls:

TimeVariablePointExpression
73.0ms
n
@0
((- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (neg (/ (+ (+ (neg (/ (+ (neg (/ (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3))) n)) (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x))))) n)) (neg (log (+ 1 x)))) (log x)) n)) (/ (+ (+ (neg (/ (+ (neg (/ (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3))) n)) (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x))))) n)) (neg (log (+ 1 x)))) (log x)) n) (+ (+ (neg (/ (+ (neg (/ (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3))) n)) (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x))))) n)) (neg (log (+ 1 x)))) (log x)) (+ (neg (/ (+ (neg (/ (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3))) n)) (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x))))) n)) (neg (log (+ 1 x)))) (neg (/ (+ (neg (/ (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3))) n)) (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x))))) n)) (/ (+ (neg (/ (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3))) n)) (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x))))) n) (+ (neg (/ (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3))) n)) (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x))))) (neg (/ (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3))) n)) (/ (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3))) n) (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3))) -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3)) (pow (log (+ 1 x)) 3) (log (+ 1 x)) (+ 1 x) 1 x 3 (pow (log x) 3) (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 x) (log x)) (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)) (+ (/ (log x) n) 1) (/ (log x) n) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (pow (+ x 1) (/ 1 n)) (+ (* (+ (* (- (+ (* (+ (/ 1/6 (* (* n n) n)) (- (/ 1/3 n) (/ 1/2 (* n n)))) x) (/ 1/2 (* n n))) (/ 1/2 n)) x) (/ 1 n)) x) 1) (+ (* (- (+ (* (+ (/ 1/6 (* (* n n) n)) (- (/ 1/3 n) (/ 1/2 (* n n)))) x) (/ 1/2 (* n n))) (/ 1/2 n)) x) (/ 1 n)) (- (+ (* (+ (/ 1/6 (* (* n n) n)) (- (/ 1/3 n) (/ 1/2 (* n n)))) x) (/ 1/2 (* n n))) (/ 1/2 n)) (+ (* (+ (/ 1/6 (* (* n n) n)) (- (/ 1/3 n) (/ 1/2 (* n n)))) x) (/ 1/2 (* n n))) (+ (/ 1/6 (* (* n n) n)) (- (/ 1/3 n) (/ 1/2 (* n n)))) (/ 1/6 (* (* n n) n)) 1/6 (* (* n n) n) (* n n) (- (/ 1/3 n) (/ 1/2 (* n n))) (/ 1/3 n) 1/3 (/ 1/2 (* n n)) (/ 1/2 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))) (/ (+ (/ 1/6 (* (* n n) n)) (- (/ 1/3 n) (/ 1/2 (* n n)))) (* x 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))) (/ (+ (/ 1/6 (* (* n n) n)) (- (/ 1/3 n) (/ 1/2 (* n n)))) (* x x)))) (/ (exp (neg (/ (neg (log x)) n))) n)) (+ (* (exp (neg (/ (neg (log x)) n))) (/ (- (/ 1/2 (* n n)) (/ 1/2 n)) x)) (* (exp (neg (/ (neg (log x)) n))) (/ (+ (/ 1/6 (* (* n n) n)) (- (/ 1/3 n) (/ 1/2 (* n n)))) (* x x)))) (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)) (* (exp (neg (/ (neg (log x)) n))) (/ (+ (/ 1/6 (* (* n n) n)) (- (/ 1/3 n) (/ 1/2 (* n n)))) (* x x))) (/ (+ (/ 1/6 (* (* n n) n)) (- (/ 1/3 n) (/ 1/2 (* n n)))) (* x x)) (* x x) (/ (exp (neg (/ (neg (log x)) n))) n))
67.0ms
N
@inf
((log (+ 1 (* (pow N -1/2) (pow N -1/2)))) (* (pow N -1/2) (pow N -1/2)) (pow N -1/2) N -1/2 (- (log (+ N 1)) (log N)) (/ (- N 1/2) (* N N)) (- N 1/2) 1/2 (* N N) (- (log (+ N 1)) (log N)) (* (pow N -1/2) (pow N -1/2)) (pow N -1/2) (sqrt (/ 1 N)) (/ 1 N) 1 (- (log (+ N 1)) (log N)) (/ (- (- (/ 1/3 (* N N)) -1) (/ 1/2 N)) N) (- (- (/ 1/3 (* N N)) -1) (/ 1/2 N)) (- 1 (/ (- 1/2 (/ 1/3 N)) N)) (/ (- 1/2 (/ 1/3 N)) N) (- 1/2 (/ 1/3 N)) (/ 1/3 N) 1/3 (log (+ 1 (exp (neg (log N))))) (exp (neg (log N))) (neg (log N)) (log N))
67.0ms
eps
@inf
((log (/ (- 1 eps) (+ 1 eps))) (* (+ (* (* eps eps) -2/3) -2) eps) (+ (* (* eps eps) -2/3) -2) (* eps eps) eps -2/3 -2 (log (/ (- 1 eps) (+ 1 eps))) (* -2 eps) (log (/ (- 1 eps) (- eps -1))) (/ (- 1 eps) (- eps -1)) (- 1 eps) 1 (- eps -1) -1 (- (log (- 1 eps)) (log (- eps -1))) (log (- 1 eps)) (log (- eps -1)) (/ (- (pow (log (- 1 eps)) 3) (pow (log (- eps -1)) 3)) (+ (* (log (- 1 eps)) (log (- 1 eps))) (+ (* (log (- eps -1)) (log (- eps -1))) (* (log (- 1 eps)) (log (- eps -1)))))) (- (pow (log (- 1 eps)) 3) (pow (log (- eps -1)) 3)) (pow (log (- 1 eps)) 3) 3 (pow (log (- eps -1)) 3) (+ (* (log (- 1 eps)) (log (- 1 eps))) (+ (* (log (- eps -1)) (log (- eps -1))) (* (log (- 1 eps)) (log (- eps -1))))) (+ (* (log (- eps -1)) (log (- eps -1))) (* (log (- 1 eps)) (log (- eps -1)))) (* (log (- 1 eps)) (log (- eps -1))))
66.0ms
n
@-inf
((- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (neg (/ (+ (+ (neg (/ (+ (neg (/ (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3))) n)) (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x))))) n)) (neg (log (+ 1 x)))) (log x)) n)) (/ (+ (+ (neg (/ (+ (neg (/ (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3))) n)) (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x))))) n)) (neg (log (+ 1 x)))) (log x)) n) (+ (+ (neg (/ (+ (neg (/ (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3))) n)) (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x))))) n)) (neg (log (+ 1 x)))) (log x)) (+ (neg (/ (+ (neg (/ (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3))) n)) (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x))))) n)) (neg (log (+ 1 x)))) (neg (/ (+ (neg (/ (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3))) n)) (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x))))) n)) (/ (+ (neg (/ (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3))) n)) (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x))))) n) (+ (neg (/ (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3))) n)) (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x))))) (neg (/ (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3))) n)) (/ (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3))) n) (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3))) -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3)) (pow (log (+ 1 x)) 3) (log (+ 1 x)) (+ 1 x) 1 x 3 (pow (log x) 3) (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 x) (log x)) (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)) (+ (/ (log x) n) 1) (/ (log x) n) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (pow (+ x 1) (/ 1 n)) (+ (* (+ (* (- (+ (* (+ (/ 1/6 (* (* n n) n)) (- (/ 1/3 n) (/ 1/2 (* n n)))) x) (/ 1/2 (* n n))) (/ 1/2 n)) x) (/ 1 n)) x) 1) (+ (* (- (+ (* (+ (/ 1/6 (* (* n n) n)) (- (/ 1/3 n) (/ 1/2 (* n n)))) x) (/ 1/2 (* n n))) (/ 1/2 n)) x) (/ 1 n)) (- (+ (* (+ (/ 1/6 (* (* n n) n)) (- (/ 1/3 n) (/ 1/2 (* n n)))) x) (/ 1/2 (* n n))) (/ 1/2 n)) (+ (* (+ (/ 1/6 (* (* n n) n)) (- (/ 1/3 n) (/ 1/2 (* n n)))) x) (/ 1/2 (* n n))) (+ (/ 1/6 (* (* n n) n)) (- (/ 1/3 n) (/ 1/2 (* n n)))) (/ 1/6 (* (* n n) n)) 1/6 (* (* n n) n) (* n n) (- (/ 1/3 n) (/ 1/2 (* n n))) (/ 1/3 n) 1/3 (/ 1/2 (* n n)) (/ 1/2 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))) (/ (+ (/ 1/6 (* (* n n) n)) (- (/ 1/3 n) (/ 1/2 (* n n)))) (* x 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))) (/ (+ (/ 1/6 (* (* n n) n)) (- (/ 1/3 n) (/ 1/2 (* n n)))) (* x x)))) (/ (exp (neg (/ (neg (log x)) n))) n)) (+ (* (exp (neg (/ (neg (log x)) n))) (/ (- (/ 1/2 (* n n)) (/ 1/2 n)) x)) (* (exp (neg (/ (neg (log x)) n))) (/ (+ (/ 1/6 (* (* n n) n)) (- (/ 1/3 n) (/ 1/2 (* n n)))) (* x x)))) (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)) (* (exp (neg (/ (neg (log x)) n))) (/ (+ (/ 1/6 (* (* n n) n)) (- (/ 1/3 n) (/ 1/2 (* n n)))) (* x x))) (/ (+ (/ 1/6 (* (* n n) n)) (- (/ 1/3 n) (/ 1/2 (* n n)))) (* x x)) (* x x) (/ (exp (neg (/ (neg (log x)) n))) n))
66.0ms
N
@0
((log (+ 1 (* (pow N -1/2) (pow N -1/2)))) (* (pow N -1/2) (pow N -1/2)) (pow N -1/2) N -1/2 (- (log (+ N 1)) (log N)) (/ (- N 1/2) (* N N)) (- N 1/2) 1/2 (* N N) (- (log (+ N 1)) (log N)) (* (pow N -1/2) (pow N -1/2)) (pow N -1/2) (sqrt (/ 1 N)) (/ 1 N) 1 (- (log (+ N 1)) (log N)) (/ (- (- (/ 1/3 (* N N)) -1) (/ 1/2 N)) N) (- (- (/ 1/3 (* N N)) -1) (/ 1/2 N)) (- 1 (/ (- 1/2 (/ 1/3 N)) N)) (/ (- 1/2 (/ 1/3 N)) N) (- 1/2 (/ 1/3 N)) (/ 1/3 N) 1/3 (log (+ 1 (exp (neg (log N))))) (exp (neg (log N))) (neg (log N)) (log N))

regimes3.1s (2.2%)

Memory
-53.0MiB live, 4 097.8MiB allocated; 908ms collecting garbage
Counts
3 150 → 332
Calls

43 calls:

792.0ms
x
280.0ms
eps
252.0ms
(-.f64 (/.f64 #s(literal 1 binary64) (sqrt.f64 x)) (/.f64 #s(literal 1 binary64) (sqrt.f64 (+.f64 x #s(literal 1 binary64)))))
202.0ms
(-.f64 (sin.f64 (+.f64 x eps)) (sin.f64 x))
146.0ms
b
Compiler

Compiled 1 674 to 1 850 computations (-10.5% saved)

prune2.0s (1.4%)

Memory
-94.5MiB live, 2 606.3MiB allocated; 466ms collecting garbage
Counts
29 763 → 1 567
Compiler

Compiled 54 640 to 45 979 computations (15.9% saved)

bsearch1.8s (1.2%)

Memory
-59.2MiB live, 1 287.0MiB allocated; 1.1s collecting garbage
Algorithm
97×binary-search
33×left-value
Stop Event
96×narrow-enough
1×predicate-same
Samples
531.0ms499×2valid
394.0ms6 021×0valid
160.0ms1 843×0invalid
98.0ms820×1valid
4.0ms20×3valid
2.0ms21×0exit
Compiler

Compiled 33 554 to 33 116 computations (1.3% saved)

Precisions
Click to see histograms. Total time spent on operations: 924.0ms
ival-pow: 479.0ms (51.9% of total)
ival-mult!: 151.0ms (16.3% of total)
ival-div!: 71.0ms (7.7% of total)
ival-sqrt: 68.0ms (7.4% of total)
ival-neg: 48.0ms (5.2% of total)
adjust: 38.0ms (4.1% of total)
ival-sub!: 33.0ms (3.6% of total)
ival-add!: 15.0ms (1.6% of total)
ival-cos: 15.0ms (1.6% of total)
ival-cbrt: 3.0ms (0.3% of total)
ival-expm1: 3.0ms (0.3% of total)
ival-log1p: 0.0ms (0% of total)
ival-log: 0.0ms (0% of total)

analyze1.7s (1.2%)

Memory
-246.6MiB live, 1 869.9MiB allocated; 612ms collecting garbage
Algorithm
28×search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
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
Compiler

Compiled 483 to 337 computations (30.2% saved)

start1.0ms (0%)

Memory
1.9MiB live, 1.9MiB allocated; 0ms collecting garbage

end0.0ms (0%)

Memory
0.3MiB live, 0.3MiB allocated; 0ms collecting garbage

Profiling

Loading profile data...