Herbie run

Date:Saturday, April 5th, 2025
Commit:f7a7cb35 on main
Seed:2025095
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:1 067 708.8 MB

Time bar (total: 14.2min)

sample4.6min (32.7%)

Memory
4 902.9MiB live, 355 321.9MiB allocated; 1.6min collecting garbage
Samples
2.6min2 144 530×0valid
19.5s69 599×1valid
7.6s64 177×0invalid
1.5s6 029×2valid
719.0ms1 189×5exit
308.0ms1 795×1invalid
301.0ms706×3valid
262.0ms386×4exit
2.0ms21×1exit
Precisions
Click to see histograms. Total time spent on operations: 1.6min
ival-mult!: 35.1s (36.2% of total)
ival-div!: 11.4s (11.8% of total)
ival-add!: 11.0s (11.4% of total)
ival-sub!: 9.3s (9.6% of total)
ival-log: 8.6s (8.9% of total)
ival-sin: 6.1s (6.3% of total)
ival-sqrt: 4.6s (4.7% of total)
adjust: 3.9s (4% of total)
ival-cos: 3.3s (3.4% of total)
ival-exp: 1.9s (2% of total)
ival-sinh: 291.0ms (0.3% of total)
ival-cosh: 290.0ms (0.3% of total)
ival-fabs: 284.0ms (0.3% of total)
ival-tan: 270.0ms (0.3% of total)
ival-acos: 220.0ms (0.2% of total)
ival-hypot: 206.0ms (0.2% of total)
ival-tanh: 103.0ms (0.1% of total)
const: 0.0ms (0% of total)
Bogosity

rewrite3.2min (22.5%)

Memory
4 127.7MiB live, 209 319.6MiB allocated; 57.6s collecting garbage
Stop Event
2 235×iter-limit
851×node-limit
70×unsound
12×saturated
Counts
130 032 → 226 259

regimes1.1min (8.1%)

Memory
-685.6MiB live, 98 110.2MiB allocated; 22.2s collecting garbage
Counts
33 744 → 4 939
Calls

512 calls:

9.7s
z
8.9s
x
8.2s
y
4.6s
t
4.0s
(-.f64 (-.f64 #s(literal 1 binary64) (/.f64 #s(literal 1 binary64) (*.f64 x #s(literal 9 binary64)))) (/.f64 y (*.f64 #s(literal 3 binary64) (sqrt.f64 x))))
Compiler

Compiled 38 449 to 57 598 computations (-49.8% saved)

derivations1.0min (7.3%)

Memory
-1 434.4MiB live, 62 302.3MiB allocated; 10.8s collecting garbage
Stop Event
149×fuel
120×done
Compiler

Compiled 154 016 to 18 776 computations (87.8% saved)

series54.3s (6.4%)

Memory
3 749.1MiB live, 79 861.8MiB allocated; 15.4s collecting garbage
Counts
18 936 → 111 096
Calls

8877 calls:

TimeVariablePointExpression
1.1s
b
@0
((/ (/ (- (* (* y x) 9) (- (* (* (* 4 z) t) a) b)) z) c) (/ (- (* (* y x) 9) (- (* (* (* 4 z) t) a) b)) z) (- (* (* y x) 9) (- (* (* (* 4 z) t) a) b)) (* (* y x) 9) (* y x) y x 9 (- (* (* (* 4 z) t) a) b) (* (* (* 4 z) t) a) (* (* 4 z) t) (* 4 z) 4 z t a b c (/ (+ (- (* (* x 9) y) (* (* (* z 4) t) a)) b) (* z c)) (+ (- (* (* x 9) y) (* (* (* z 4) t) a)) b) (* z c) (/ (+ (- (* (* x 9) y) (* (* (* z 4) t) a)) b) (* z c)) (/ (/ (+ (* (* y x) 9) b) c) z) (/ (+ (* (* y x) 9) b) c) (+ (* (* y x) 9) b) (/ (+ (- (* (* x 9) y) (* (* (* z 4) t) a)) b) (* z c)) (/ (/ (+ (* -4 (* (* t z) a)) (* (* y x) 9)) c) z) (/ (+ (* -4 (* (* t z) a)) (* (* y x) 9)) c) (+ (* -4 (* (* t z) a)) (* (* y x) 9)) -4 (* (* t z) a) (* t z) (/ (+ (- (* (* x 9) y) (* (* (* z 4) t) a)) b) (* z c)) (+ (- (* (* x 9) y) (* (* (* z 4) t) a)) b) (- (* (* x 9) y) (* (* (* z 4) t) a)) (* (+ (* (/ (* y x) t) 9) (* (* a z) -4)) t) (+ (* (/ (* y x) t) 9) (* (* a z) -4)) (/ (* y x) t) (* (* a z) -4) (* a z))
827.0ms
j
@inf
((+ (- (+ (+ (- (* (- (* x y) (* z t)) (- (* a b) (* c i))) (* (- (* x j) (* z k)) (- (* y0 b) (* y1 i)))) (* (- (* x y2) (* z y3)) (- (* y0 c) (* y1 a)))) (* (- (* t j) (* y k)) (- (* y4 b) (* y5 i)))) (* (- (* t y2) (* y y3)) (- (* y4 c) (* y5 a)))) (* (- (* k y2) (* j y3)) (- (* y4 y1) (* y5 y0)))) (- (+ (+ (- (* (- (* x y) (* z t)) (- (* a b) (* c i))) (* (- (* x j) (* z k)) (- (* y0 b) (* y1 i)))) (* (- (* x y2) (* z y3)) (- (* y0 c) (* y1 a)))) (* (- (* t j) (* y k)) (- (* y4 b) (* y5 i)))) (* (- (* t y2) (* y y3)) (- (* y4 c) (* y5 a)))) (+ (+ (- (* (- (* x y) (* z t)) (- (* a b) (* c i))) (* (- (* x j) (* z k)) (- (* y0 b) (* y1 i)))) (* (- (* x y2) (* z y3)) (- (* y0 c) (* y1 a)))) (* (- (* t j) (* y k)) (- (* y4 b) (* y5 i)))) (* -1 (* y1 (- (* a (- (* x y2) (* y3 z))) (* i (- (* j x) (* k z)))))) -1 (* y1 (- (* a (- (* x y2) (* y3 z))) (* i (- (* j x) (* k z))))) y1 (- (* a (- (* x y2) (* y3 z))) (* i (- (* j x) (* k z)))) (* a (- (* x y2) (* y3 z))) a (- (* x y2) (* y3 z)) (* x y2) x y2 (* y3 z) y3 z (* i (- (* j x) (* k z))) i (- (* j x) (* k z)) (* j x) j (* k z) k (* (- (* t y2) (* y y3)) (- (* y4 c) (* y5 a))) (- (* t y2) (* y y3)) (* t y2) t (* y y3) y (- (* y4 c) (* y5 a)) (* y4 c) y4 c (* y5 a) y5 (* (- (* k y2) (* j y3)) (- (* y4 y1) (* y5 y0))) (- (* k y2) (* j y3)) (* k y2) (* j y3) (- (* y4 y1) (* y5 y0)) (* y4 y1) (* y5 y0) y0 (+ (- (+ (+ (- (* (- (* x y) (* z t)) (- (* a b) (* c i))) (* (- (* x j) (* z k)) (- (* y0 b) (* y1 i)))) (* (- (* x y2) (* z y3)) (- (* y0 c) (* y1 a)))) (* (- (* t j) (* y k)) (- (* y4 b) (* y5 i)))) (* (- (* t y2) (* y y3)) (- (* y4 c) (* y5 a)))) (* (- (* k y2) (* j y3)) (- (* y4 y1) (* y5 y0)))) (* b (- (+ (* a (- (* x y) (* t z))) (* y4 (- (* j t) (* k y)))) (* y0 (- (* j x) (* k z))))) b (- (+ (* a (- (* x y) (* t z))) (* y4 (- (* j t) (* k y)))) (* y0 (- (* j x) (* k z)))) (+ (* a (- (* x y) (* t z))) (* y4 (- (* j t) (* k y)))) (- (* x y) (* t z)) (* x y) (* t z) (* y4 (- (* j t) (* k y))) (- (* j t) (* k y)) (* j t) (* k y) (* y0 (- (* j x) (* k z))) (+ (- (+ (+ (- (* (- (* x y) (* z t)) (- (* a b) (* c i))) (* (- (* x j) (* z k)) (- (* y0 b) (* y1 i)))) (* (- (* x y2) (* z y3)) (- (* y0 c) (* y1 a)))) (* (- (* t j) (* y k)) (- (* y4 b) (* y5 i)))) (* (- (* t y2) (* y y3)) (- (* y4 c) (* y5 a)))) (* (- (* k y2) (* j y3)) (- (* y4 y1) (* y5 y0)))) (* -1 (* i (- (+ (* c (- (* x y) (* t z))) (* y5 (- (* j t) (* k y)))) (* y1 (- (* j x) (* k z)))))) (* i (- (+ (* c (- (* x y) (* t z))) (* y5 (- (* j t) (* k y)))) (* y1 (- (* j x) (* k z))))) (- (+ (* c (- (* x y) (* t z))) (* y5 (- (* j t) (* k y)))) (* y1 (- (* j x) (* k z)))) (+ (* c (- (* x y) (* t z))) (* y5 (- (* j t) (* k y)))) (* y5 (- (* j t) (* k y))) (* y1 (- (* j x) (* k z))) (+ (- (+ (+ (- (* (- (* x y) (* z t)) (- (* a b) (* c i))) (* (- (* x j) (* z k)) (- (* y0 b) (* y1 i)))) (* (- (* x y2) (* z y3)) (- (* y0 c) (* y1 a)))) (* (- (* t j) (* y k)) (- (* y4 b) (* y5 i)))) (* (- (* t y2) (* y y3)) (- (* y4 c) (* y5 a)))) (* (- (* k y2) (* j y3)) (- (* y4 y1) (* y5 y0)))) (* t (- (+ (* -1 (* z (- (* a b) (* c i)))) (* j (- (* b y4) (* i y5)))) (* y2 (- (* c y4) (* a y5))))) (- (+ (* -1 (* z (- (* a b) (* c i)))) (* j (- (* b y4) (* i y5)))) (* y2 (- (* c y4) (* a y5)))) (+ (* -1 (* z (- (* a b) (* c i)))) (* j (- (* b y4) (* i y5)))) (* z (- (* a b) (* c i))) (- (* a b) (* c i)) (* a b) (* c i) (* j (- (* b y4) (* i y5))) (- (* b y4) (* i y5)) (* b y4) (* i y5) (* y2 (- (* c y4) (* a y5))) (- (* c y4) (* a y5)) (* c y4) (* a y5) (+ (- (+ (+ (- (* (- (* x y) (* z t)) (- (* a b) (* c i))) (* (- (* x j) (* z k)) (- (* y0 b) (* y1 i)))) (* (- (* x y2) (* z y3)) (- (* y0 c) (* y1 a)))) (* (- (* t j) (* y k)) (- (* y4 b) (* y5 i)))) (* (- (* t y2) (* y y3)) (- (* y4 c) (* y5 a)))) (* (- (* k y2) (* j y3)) (- (* y4 y1) (* y5 y0)))) (- (+ (+ (- (* (- (* x y) (* z t)) (- (* a b) (* c i))) (* (- (* x j) (* z k)) (- (* y0 b) (* y1 i)))) (* (- (* x y2) (* z y3)) (- (* y0 c) (* y1 a)))) (* (- (* t j) (* y k)) (- (* y4 b) (* y5 i)))) (* (- (* t y2) (* y y3)) (- (* y4 c) (* y5 a)))) (+ (+ (- (* (- (* x y) (* z t)) (- (* a b) (* c i))) (* (- (* x j) (* z k)) (- (* y0 b) (* y1 i)))) (* (- (* x y2) (* z y3)) (- (* y0 c) (* y1 a)))) (* (- (* t j) (* y k)) (- (* y4 b) (* y5 i)))) (* y0 (- (* c (- (* x y2) (* y3 z))) (* b (- (* j x) (* k z))))) (- (* c (- (* x y2) (* y3 z))) (* b (- (* j x) (* k z)))) (* c (- (* x y2) (* y3 z))) (* b (- (* j x) (* k z))))
677.0ms
c
@-inf
((/ (/ (- (* (* y x) 9) (- (* (* (* 4 z) t) a) b)) z) c) (/ (- (* (* y x) 9) (- (* (* (* 4 z) t) a) b)) z) (- (* (* y x) 9) (- (* (* (* 4 z) t) a) b)) (* (* y x) 9) (* y x) y x 9 (- (* (* (* 4 z) t) a) b) (* (* (* 4 z) t) a) (* (* 4 z) t) (* 4 z) 4 z t a b c (/ (+ (- (* (* x 9) y) (* (* (* z 4) t) a)) b) (* z c)) (+ (- (* (* x 9) y) (* (* (* z 4) t) a)) b) (* z c) (/ (+ (- (* (* x 9) y) (* (* (* z 4) t) a)) b) (* z c)) (/ (/ (+ (* (* y x) 9) b) c) z) (/ (+ (* (* y x) 9) b) c) (+ (* (* y x) 9) b) (/ (+ (- (* (* x 9) y) (* (* (* z 4) t) a)) b) (* z c)) (/ (/ (+ (* -4 (* (* t z) a)) (* (* y x) 9)) c) z) (/ (+ (* -4 (* (* t z) a)) (* (* y x) 9)) c) (+ (* -4 (* (* t z) a)) (* (* y x) 9)) -4 (* (* t z) a) (* t z) (/ (+ (- (* (* x 9) y) (* (* (* z 4) t) a)) b) (* z c)) (+ (- (* (* x 9) y) (* (* (* z 4) t) a)) b) (- (* (* x 9) y) (* (* (* z 4) t) a)) (* (+ (* (/ (* y x) t) 9) (* (* a z) -4)) t) (+ (* (/ (* y x) t) 9) (* (* a z) -4)) (/ (* y x) t) (* (* a z) -4) (* a z))
348.0ms
y
@-inf
((* x (/ (- 0 (* (log (/ y x)) (log (/ y x)))) (+ 0 (log (/ y x))))) x (/ (- 0 (* (log (/ y x)) (log (/ y x)))) (+ 0 (log (/ y x)))) (- 0 (* (log (/ y x)) (log (/ y x)))) 0 (* (log (/ y x)) (log (/ y x))) (log (/ y x)) (/ y x) y (+ 0 (log (/ y x))) (log (pow (/ x y) x)) (pow (/ x y) x) (/ x y) (+ (* (log (/ 1 y)) x) (* (log x) x)) (log (/ 1 y)) (/ 1 y) 1 (* (log x) x) (log x) (/ (* (- (pow (log x) 2) (pow (log y) 2)) x) (log (* x y))) (* (- (pow (log x) 2) (pow (log y) 2)) x) (- (pow (log x) 2) (pow (log y) 2)) (pow (log x) 2) 2 (pow (log y) 2) (log y) (log (* x y)) (* x y) (* x (/ (+ (pow (log (neg x)) 3) (pow (log (/ -1 y)) 3)) (+ (* (log (neg x)) (log (* x y))) (pow (log (/ -1 y)) 2)))) (/ (+ (pow (log (neg x)) 3) (pow (log (/ -1 y)) 3)) (+ (* (log (neg x)) (log (* x y))) (pow (log (/ -1 y)) 2))) (+ (pow (log (neg x)) 3) (pow (log (/ -1 y)) 3)) (pow (log (neg x)) 3) (log (neg x)) (neg x) 3 (pow (log (/ -1 y)) 3) (log (/ -1 y)) (/ -1 y) -1 (+ (* (log (neg x)) (log (* x y))) (pow (log (/ -1 y)) 2)) (pow (log (/ -1 y)) 2))
246.0ms
x
@-inf
((* (sin x) (/ (sinh y) y)) (sin x) x (/ (sinh y) y) (+ (* (+ (* (+ (* 1/5040 (* y y)) 1/120) (* y y)) 1/6) (* y y)) 1) (+ (* (+ (* 1/5040 (* y y)) 1/120) (* y y)) 1/6) (* (* (+ (* (* y y) 1/5040) 1/120) y) y) (* (+ (* (* y y) 1/5040) 1/120) y) (+ (* (* y y) 1/5040) 1/120) (* y y) y 1/5040 1/120 1 (* (sin x) (/ (sinh y) y)) (sin x) (* (+ (* -1/6 (* x x)) 1) x) (+ (* -1/6 (* x x)) 1) -1/6 (* x x) (* (sin x) (/ (sinh y) y)) (sin x) (* (+ (* (+ (* (+ (* -1/5040 (* x x)) 1/120) (* x x)) -1/6) (* x x)) 1) x) (+ (* (+ (* (+ (* -1/5040 (* x x)) 1/120) (* x x)) -1/6) (* x x)) 1) (+ (* (+ (* -1/5040 (* x x)) 1/120) (* x x)) -1/6) (+ (* -1/5040 (* x x)) 1/120) -1/5040 (* (sin x) (/ (sinh y) y)) (sin x) (* (+ (* (+ (* (* x x) 1/120) -1/6) (* x x)) 1) x) (+ (* (+ (* (* x x) 1/120) -1/6) (* x x)) 1) (+ (* (* x x) 1/120) -1/6) (/ (sinh y) y) (+ (* (+ (* (* y y) 1/120) 1/6) (* y y)) 1) (+ (* (* y y) 1/120) 1/6) 1/6 (* (sin x) (/ (sinh y) y)) (/ (sinh y) y) (+ (* (+ (* (+ (* 1/5040 (* y y)) 1/120) (* y y)) 1/6) (* y y)) 1) (+ (* (+ (* 1/5040 (* y y)) 1/120) (* y y)) 1/6) (+ (* 1/5040 (* y y)) 1/120))

eval49.0s (5.8%)

Memory
522.1MiB live, 66 764.3MiB allocated; 20.7s collecting garbage
Compiler

Compiled 10 201 858 to 1 036 939 computations (89.8% saved)

explain39.7s (4.7%)

Memory
-2.6MiB live, 52 309.3MiB allocated; 13.9s collecting garbage
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
log.f64#fsensitivity15850
/.f64#fo/n11720
sqrt.f64#foflow-rescue7970
-.f64#fcancellation5856
/.f64#fo/o5600
*.f64#fn*o5330
+.f64#fnan-rescue4750
-.f64#fnan-rescue4540
cos.f64#fsensitivity3530
/.f64#fn/o3390
+.f64#fcancellation2931
/.f64#fu/n2870
sin.f64#fsensitivity2210
*.f64#fn*u1810
cos.f64#foflow-rescue1470
/.f64#fn/u1380
tan.f64(tan.f64 (/.f64 x (*.f64 y #s(literal 2 binary64))))sensitivity1070
log.f64#foflow-rescue860
/.f64#fu/u800
log.f64#fuflow-rescue740
sqrt.f64#fuflow-rescue410
tan.f64(tan.f64 (/.f64 x (*.f64 y #s(literal 2 binary64))))oflow-rescue340
(/.f64 x (*.f64 y #s(literal 2 binary64)))overflow34
sin.f64(sin.f64 (/.f64 x (*.f64 y #s(literal 2 binary64))))oflow-rescue340
(/.f64 x (*.f64 y #s(literal 2 binary64)))overflow34
*.f64#fo*u280
exp.f64(exp.f64 (-.f64 (+.f64 (*.f64 y (log.f64 z)) (*.f64 (-.f64 t #s(literal 1 binary64)) (log.f64 a))) b))sensitivity260
*.f64#fu*o30
Confusion
Predicted +Predicted -
+6061180
-171660907
Precision
0.7793493635077794
Recall
0.9711584681941996
Confusion?
Predicted +Predicted MaybePredicted -
+60612178
-1716760900
Precision?
0.7787053686103262
Recall?
0.9714789296587085
Freqs
test
numberfreq
061087
17009
2704
343
418
53
Total Confusion?
Predicted +Predicted MaybePredicted -
+13510
-30130
Precision?
0.9784172661870504
Recall?
1.0
Samples
10.7s130 418×0valid
1.5s5 912×1valid
553.0ms1 308×2valid
29.0ms84×3valid
11.0ms4valid
0.0ms5exit
Compiler

Compiled 24 442 to 8 402 computations (65.6% saved)

Precisions
Click to see histograms. Total time spent on operations: 5.9s
ival-mult!: 1.9s (33.2% of total)
ival-sub!: 724.0ms (12.4% of total)
ival-log: 665.0ms (11.4% of total)
ival-div!: 612.0ms (10.5% of total)
ival-add!: 527.0ms (9% of total)
ival-sin: 397.0ms (6.8% of total)
adjust: 336.0ms (5.7% of total)
ival-sqrt: 231.0ms (3.9% of total)
ival-cos: 200.0ms (3.4% of total)
ival-exp: 141.0ms (2.4% of total)
ival-sinh: 16.0ms (0.3% of total)
ival-tan: 13.0ms (0.2% of total)
ival-cosh: 13.0ms (0.2% of total)
ival-fabs: 12.0ms (0.2% of total)
ival-hypot: 9.0ms (0.2% of total)
ival-tanh: 7.0ms (0.1% of total)
ival-acos: 5.0ms (0.1% of total)
const: 0.0ms (0% of total)

preprocess36.9s (4.3%)

Memory
-952.5MiB live, 47 540.8MiB allocated; 8.6s collecting garbage
Stop Event
174×node-limit
95×saturated
Compiler

Compiled 528 604 to 144 864 computations (72.6% saved)

bsearch30.0s (3.5%)

Memory
28.2MiB live, 37 956.4MiB allocated; 11.2s collecting garbage
Algorithm
1 705×binary-search
1 121×left-value
Stop Event
1 671×narrow-enough
33×predicate-same
predicate-failed
Samples
17.4s138 951×0valid
841.0ms4 025×1valid
284.0ms3 582×0invalid
39.0ms172×1invalid
21.0ms148×2valid
3.0ms12×3valid
Compiler

Compiled 923 375 to 669 293 computations (27.5% saved)

Precisions
Click to see histograms. Total time spent on operations: 7.6s
ival-mult!: 3.8s (50.5% of total)
ival-sub!: 1.1s (14.3% of total)
ival-add!: 817.0ms (10.7% of total)
ival-div!: 505.0ms (6.6% of total)
ival-log: 435.0ms (5.7% of total)
ival-sin: 236.0ms (3.1% of total)
adjust: 216.0ms (2.8% of total)
ival-cos: 161.0ms (2.1% of total)
ival-exp: 157.0ms (2.1% of total)
ival-sqrt: 87.0ms (1.1% of total)
ival-sinh: 42.0ms (0.6% of total)
ival-cosh: 9.0ms (0.1% of total)
ival-tanh: 7.0ms (0.1% of total)
ival-fabs: 5.0ms (0.1% of total)

prune21.4s (2.5%)

Memory
-1 120.3MiB live, 36 005.0MiB allocated; 5.6s collecting garbage
Counts
255 719 → 12 605
Compiler

Compiled 802 163 to 437 110 computations (45.5% saved)

analyze18.6s (2.2%)

Memory
-421.4MiB live, 22 192.7MiB allocated; 8.3s collecting garbage
Algorithm
269×search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%99.9%0.1%0%0%0%0
46.8%46.8%53.1%0.1%0%0%0%1
50.5%50.1%49.2%0.1%0%0.6%0%2
58.6%57%40.3%0.1%0%2.6%0%3
65.2%62.7%33.5%0.1%0%3.6%0%4
71.2%68.2%27.5%0.1%0%4.1%0%5
75.9%72.3%23%0.1%0%4.6%0%6
79.8%75.6%19.1%0.1%0%5.1%0%7
81.7%77%17.3%0.1%0%5.6%0%8
84.3%79.3%14.7%0.1%0%5.9%0%9
85.9%80.5%13.2%0.1%0%6.2%0%10
88.5%82.8%10.8%0.1%0%6.2%0%11
89.6%83.6%9.8%0.1%0%6.5%0%12
Compiler

Compiled 3 462 to 2 977 computations (14% saved)

start10.0ms (0%)

Memory
20.3MiB live, 19.9MiB allocated; 0ms collecting garbage

end2.0ms (0%)

Memory
4.9MiB live, 4.6MiB allocated; 0ms collecting garbage

Profiling

Loading profile data...