
| Date: | Tuesday, May 20th, 2025 |
|---|---|
| Commit: | e475129d on soundness-through-fabs |
| 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: | 147 250.9 MB |
Time bar (total: 2.1min)
| 22.7s | 292 918× | 0 | valid |
| 7.5s | 35 731× | 1 | valid |
| 6.8s | 17 701× | 2 | valid |
| 316.0ms | 4 153× | 0 | invalid |
| 241.0ms | 402× | 3 | valid |
| 125.0ms | 1 016× | 0 | exit |
| 67.0ms | 101× | 3 | exit |
| 63.0ms | 101× | 4 | exit |
| 4.0ms | 32× | 1 | exit |
ival-mult!: 6.1s (24.4% of total)ival-pow: 4.2s (16.8% of total)ival-div!: 2.7s (10.8% of total)adjust: 2.4s (9.8% of total)ival-add!: 2.0s (8.1% of total)ival-sub!: 1.9s (7.8% of total)ival-sin: 1.8s (7% of total)ival-cos: 1.4s (5.8% of total)ival-exp: 605.0ms (2.4% of total)ival-sqrt: 590.0ms (2.4% of total)ival-neg: 431.0ms (1.7% of total)ival-pow2: 361.0ms (1.4% of total)ival-atan: 97.0ms (0.4% of total)ival-log1p: 91.0ms (0.4% of total)ival-expm1: 79.0ms (0.3% of total)ival-tan: 69.0ms (0.3% of total)ival-hypot: 38.0ms (0.2% of total)ival-<=: 12.0ms (0% of total)ival-and: 8.0ms (0% of total)ival-<: 5.0ms (0% of total)ival-if: 4.0ms (0% of total)ival-fabs: 4.0ms (0% of total)ival-==: 3.0ms (0% of total)ival-assert: 1.0ms (0% of total)const: 0.0ms (0% of total)| 332× | iter-limit |
| 143× | node-limit |
| 9× | saturated |
| 3× | unsound |
Compiled 646 545 to 205 668 computations (68.2% saved)
| 22× | fuel |
| 20× | done |
Compiled 5 037 to 2 520 computations (50% saved)
| 37× | node-limit |
| 5× | saturated |
Compiled 14 471 to 10 354 computations (28.5% saved)
96 calls:
| 643.0ms | x |
| 376.0ms | a |
| 345.0ms | b |
| 304.0ms | (+.f64 x1 (+.f64 (+.f64 (+.f64 (+.f64 (*.f64 (+.f64 (*.f64 (*.f64 (*.f64 #s(literal 2 binary64) x1) (/.f64 (-.f64 (+.f64 (*.f64 (*.f64 #s(literal 3 binary64) x1) x1) (*.f64 #s(literal 2 binary64) x2)) x1) (+.f64 (*.f64 x1 x1) #s(literal 1 binary64)))) (-.f64 (/.f64 (-.f64 (+.f64 (*.f64 (*.f64 #s(literal 3 binary64) x1) x1) (*.f64 #s(literal 2 binary64) x2)) x1) (+.f64 (*.f64 x1 x1) #s(literal 1 binary64))) #s(literal 3 binary64))) (*.f64 (*.f64 x1 x1) (-.f64 (*.f64 #s(literal 4 binary64) (/.f64 (-.f64 (+.f64 (*.f64 (*.f64 #s(literal 3 binary64) x1) x1) (*.f64 #s(literal 2 binary64) x2)) x1) (+.f64 (*.f64 x1 x1) #s(literal 1 binary64)))) #s(literal 6 binary64)))) (+.f64 (*.f64 x1 x1) #s(literal 1 binary64))) (*.f64 (*.f64 (*.f64 #s(literal 3 binary64) x1) x1) (/.f64 (-.f64 (+.f64 (*.f64 (*.f64 #s(literal 3 binary64) x1) x1) (*.f64 #s(literal 2 binary64) x2)) x1) (+.f64 (*.f64 x1 x1) #s(literal 1 binary64))))) (*.f64 (*.f64 x1 x1) x1)) x1) (*.f64 #s(literal 3 binary64) (/.f64 (-.f64 (-.f64 (*.f64 (*.f64 #s(literal 3 binary64) x1) x1) (*.f64 #s(literal 2 binary64) x2)) x1) (+.f64 (*.f64 x1 x1) #s(literal 1 binary64)))))) |
| 293.0ms | d |
Compiled 6 314 to 4 949 computations (21.6% saved)
882 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 445.0ms | x1 | @ | inf | ((+ x1 (+ (+ (+ (+ (* (+ (* (* (* 2 x1) (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) (- (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)) 3)) (* (* x1 x1) (- (* 4 (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) 6))) (+ (* x1 x1) 1)) (* (* (* 3 x1) x1) (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)))) (* (* x1 x1) x1)) x1) (* 3 (/ (- (- (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))))) (* (* (* x1 x1) (* x1 x1)) (+ 6 (* -1 (/ (+ 3 (* -1 (/ (+ 9 (+ (* -1 (/ (+ 1 (* -2 (+ 1 (* 3 (- (* 2 x2) 3))))) x1)) (* 4 (- (* 2 x2) 3)))) x1))) x1)))) (* (* x1 x1) (* x1 x1)) (* x1 x1) x1 (+ 6 (* -1 (/ (+ 3 (* -1 (/ (+ 9 (+ (* -1 (/ (+ 1 (* -2 (+ 1 (* 3 (- (* 2 x2) 3))))) x1)) (* 4 (- (* 2 x2) 3)))) x1))) x1))) 6 (* -1 (/ (+ 3 (* -1 (/ (+ 9 (+ (* -1 (/ (+ 1 (* -2 (+ 1 (* 3 (- (* 2 x2) 3))))) x1)) (* 4 (- (* 2 x2) 3)))) x1))) x1)) -1 (/ (+ 3 (* -1 (/ (+ 9 (+ (* -1 (/ (+ 1 (* -2 (+ 1 (* 3 (- (* 2 x2) 3))))) x1)) (* 4 (- (* 2 x2) 3)))) x1))) x1) (+ 3 (* -1 (/ (+ 9 (+ (* -1 (/ (+ 1 (* -2 (+ 1 (* 3 (- (* 2 x2) 3))))) x1)) (* 4 (- (* 2 x2) 3)))) x1))) 3 (* -1 (/ (+ 9 (+ (* -1 (/ (+ 1 (* -2 (+ 1 (* 3 (- (* 2 x2) 3))))) x1)) (* 4 (- (* 2 x2) 3)))) x1)) (/ (+ 9 (+ (* -1 (/ (+ 1 (* -2 (+ 1 (* 3 (- (* 2 x2) 3))))) x1)) (* 4 (- (* 2 x2) 3)))) x1) (+ 9 (+ (* -1 (/ (+ 1 (* -2 (+ 1 (* 3 (- (* 2 x2) 3))))) x1)) (* 4 (- (* 2 x2) 3)))) 9 (+ (* -1 (/ (+ 1 (* -2 (+ 1 (* 3 (- (* 2 x2) 3))))) x1)) (* 4 (- (* 2 x2) 3))) (/ (+ 1 (* -2 (+ 1 (* 3 (- (* 2 x2) 3))))) x1) (+ 1 (* -2 (+ 1 (* 3 (- (* 2 x2) 3))))) 1 (* -2 (+ 1 (* 3 (- (* 2 x2) 3)))) -2 (+ 1 (* 3 (- (* 2 x2) 3))) (* 3 (- (* 2 x2) 3)) (- (* 2 x2) 3) (* 2 x2) 2 x2 (* 4 (- (* 2 x2) 3)) 4 (+ x1 (+ (+ (+ (+ (* (+ (* (* (* 2 x1) (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) (- (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)) 3)) (* (* x1 x1) (- (* 4 (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) 6))) (+ (* x1 x1) 1)) (* (* (* 3 x1) x1) (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)))) (* (* x1 x1) x1)) x1) (* 3 (/ (- (- (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))))) (* (* x2 x2) (+ (* -1 (/ (+ (* -6 (/ (* x1 x1) (+ 1 (* x1 x1)))) (+ (* 6 (/ 1 (+ 1 (* x1 x1)))) (* (+ 1 (* x1 x1)) (+ (* -8 (/ (* x1 x1) (+ 1 (* x1 x1)))) (* 2 (/ (* x1 (+ (* -2 (- (* 3 (/ (* x1 x1) (+ 1 (* x1 x1)))) (+ 3 (/ x1 (+ 1 (* x1 x1)))))) (* -2 (/ (- (* 3 (* x1 x1)) x1) (+ 1 (* x1 x1)))))) (+ 1 (* x1 x1)))))))) x2)) (* 8 (/ x1 (+ 1 (* x1 x1)))))) (* 8 (* (* x1 x1) x2)) 8 (* (* x1 x1) x2) (+ x1 (+ (+ (+ (+ (* (+ (* (* (* 2 x1) (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) (- (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)) 3)) (* (* x1 x1) (* (- 1 (/ 6 (* 4 (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))))) (* 4 (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)))))) (+ (* x1 x1) 1)) (* (* (* 3 x1) x1) (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)))) (* (* x1 x1) x1)) x1) (* 3 (/ (- (- (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))))) (* 6 (pow x1 4)) (pow x1 4) (+ x1 (+ (+ (+ (+ (* (+ (* (* (* 2 x1) (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) (- (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)) 3)) (* (* x1 x1) (- (* 4 (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) 6))) (+ (* x1 x1) 1)) (* (* (* 3 x1) x1) (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)))) (* (* x1 x1) x1)) x1) (* 3 (/ (- (- (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))))) (* (* (* x1 x1) (* x1 x1)) (+ 6 (* -1 (/ (+ 3 (* -1 (/ (+ 9 (* 4 (- (* 2 x2) 3))) x1))) x1)))) (+ 6 (* -1 (/ (+ 3 (* -1 (/ (+ 9 (* 4 (- (* 2 x2) 3))) x1))) x1))) (* -1 (/ (+ 3 (* -1 (/ (+ 9 (* 4 (- (* 2 x2) 3))) x1))) x1)) (/ (+ 3 (* -1 (/ (+ 9 (* 4 (- (* 2 x2) 3))) x1))) x1) (+ 3 (* -1 (/ (+ 9 (* 4 (- (* 2 x2) 3))) x1))) (* -1 (/ (+ 9 (* 4 (- (* 2 x2) 3))) x1)) (/ (+ 9 (* 4 (- (* 2 x2) 3))) x1) (+ 9 (* 4 (- (* 2 x2) 3))) (+ x1 (+ (+ (+ (+ (* (+ (* (* (* 2 x1) (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) (- (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)) 3)) (* (* x1 x1) (- (* 4 (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) 6))) (+ (* x1 x1) 1)) (* (* (* 3 x1) x1) (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)))) (* (* x1 x1) x1)) x1) (* 3 (/ (- (- (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))))) (+ (* -6 x2) (* x1 (- (+ (* 4 (* x2 (- (* 2 x2) 3))) (* x1 (- (+ (* 2 (+ (* -2 x2) (* -1 (- (* 2 x2) 3)))) (+ (* 3 (- 3 (* -2 x2))) (+ (* 6 x2) (+ (* 8 x2) (* x1 (- (+ (* 2 (- (+ 1 (+ (* 2 (* x2 (+ 3 (* -2 x2)))) (* 3 (- (* 2 x2) 3)))) (* 2 (* x2 (- (* 2 x2) 3))))) (* 4 (* x2 (- (* 2 x2) 3)))) 3)))))) 6))) 1))) -6 (* x1 (- (+ (* 4 (* x2 (- (* 2 x2) 3))) (* x1 (- (+ (* 2 (+ (* -2 x2) (* -1 (- (* 2 x2) 3)))) (+ (* 3 (- 3 (* -2 x2))) (+ (* 6 x2) (+ (* 8 x2) (* x1 (- (+ (* 2 (- (+ 1 (+ (* 2 (* x2 (+ 3 (* -2 x2)))) (* 3 (- (* 2 x2) 3)))) (* 2 (* x2 (- (* 2 x2) 3))))) (* 4 (* x2 (- (* 2 x2) 3)))) 3)))))) 6))) 1)) (- (+ (* 4 (* x2 (- (* 2 x2) 3))) (* x1 (- (+ (* 2 (+ (* -2 x2) (* -1 (- (* 2 x2) 3)))) (+ (* 3 (- 3 (* -2 x2))) (+ (* 6 x2) (+ (* 8 x2) (* x1 (- (+ (* 2 (- (+ 1 (+ (* 2 (* x2 (+ 3 (* -2 x2)))) (* 3 (- (* 2 x2) 3)))) (* 2 (* x2 (- (* 2 x2) 3))))) (* 4 (* x2 (- (* 2 x2) 3)))) 3)))))) 6))) 1) (+ (* 4 (* x2 (- (* 2 x2) 3))) (* x1 (- (+ (* 2 (+ (* -2 x2) (* -1 (- (* 2 x2) 3)))) (+ (* 3 (- 3 (* -2 x2))) (+ (* 6 x2) (+ (* 8 x2) (* x1 (- (+ (* 2 (- (+ 1 (+ (* 2 (* x2 (+ 3 (* -2 x2)))) (* 3 (- (* 2 x2) 3)))) (* 2 (* x2 (- (* 2 x2) 3))))) (* 4 (* x2 (- (* 2 x2) 3)))) 3)))))) 6))) (* x2 (- (* 2 x2) 3)) (* x1 (- (+ (* 2 (+ (* -2 x2) (* -1 (- (* 2 x2) 3)))) (+ (* 3 (- 3 (* -2 x2))) (+ (* 6 x2) (+ (* 8 x2) (* x1 (- (+ (* 2 (- (+ 1 (+ (* 2 (* x2 (+ 3 (* -2 x2)))) (* 3 (- (* 2 x2) 3)))) (* 2 (* x2 (- (* 2 x2) 3))))) (* 4 (* x2 (- (* 2 x2) 3)))) 3)))))) 6)) (- (+ (* 2 (+ (* -2 x2) (* -1 (- (* 2 x2) 3)))) (+ (* 3 (- 3 (* -2 x2))) (+ (* 6 x2) (+ (* 8 x2) (* x1 (- (+ (* 2 (- (+ 1 (+ (* 2 (* x2 (+ 3 (* -2 x2)))) (* 3 (- (* 2 x2) 3)))) (* 2 (* x2 (- (* 2 x2) 3))))) (* 4 (* x2 (- (* 2 x2) 3)))) 3)))))) 6) (+ (* 2 (+ (* -2 x2) (* -1 (- (* 2 x2) 3)))) (+ (* 3 (- 3 (* -2 x2))) (+ (* 6 x2) (+ (* 8 x2) (* x1 (- (+ (* 2 (- (+ 1 (+ (* 2 (* x2 (+ 3 (* -2 x2)))) (* 3 (- (* 2 x2) 3)))) (* 2 (* x2 (- (* 2 x2) 3))))) (* 4 (* x2 (- (* 2 x2) 3)))) 3)))))) (+ (* -2 x2) (* -1 (- (* 2 x2) 3))) (* -1 (- (* 2 x2) 3)) (+ (* 3 (- 3 (* -2 x2))) (+ (* 6 x2) (+ (* 8 x2) (* x1 (- (+ (* 2 (- (+ 1 (+ (* 2 (* x2 (+ 3 (* -2 x2)))) (* 3 (- (* 2 x2) 3)))) (* 2 (* x2 (- (* 2 x2) 3))))) (* 4 (* x2 (- (* 2 x2) 3)))) 3))))) (- 3 (* -2 x2)) (* -2 x2) (+ (* 6 x2) (+ (* 8 x2) (* x1 (- (+ (* 2 (- (+ 1 (+ (* 2 (* x2 (+ 3 (* -2 x2)))) (* 3 (- (* 2 x2) 3)))) (* 2 (* x2 (- (* 2 x2) 3))))) (* 4 (* x2 (- (* 2 x2) 3)))) 3)))) (+ (* 8 x2) (* x1 (- (+ (* 2 (- (+ 1 (+ (* 2 (* x2 (+ 3 (* -2 x2)))) (* 3 (- (* 2 x2) 3)))) (* 2 (* x2 (- (* 2 x2) 3))))) (* 4 (* x2 (- (* 2 x2) 3)))) 3))) (* x1 (- (+ (* 2 (- (+ 1 (+ (* 2 (* x2 (+ 3 (* -2 x2)))) (* 3 (- (* 2 x2) 3)))) (* 2 (* x2 (- (* 2 x2) 3))))) (* 4 (* x2 (- (* 2 x2) 3)))) 3)) (- (+ (* 2 (- (+ 1 (+ (* 2 (* x2 (+ 3 (* -2 x2)))) (* 3 (- (* 2 x2) 3)))) (* 2 (* x2 (- (* 2 x2) 3))))) (* 4 (* x2 (- (* 2 x2) 3)))) 3) (+ (* 2 (- (+ 1 (+ (* 2 (* x2 (+ 3 (* -2 x2)))) (* 3 (- (* 2 x2) 3)))) (* 2 (* x2 (- (* 2 x2) 3))))) (* 4 (* x2 (- (* 2 x2) 3)))) (- (+ 1 (+ (* 2 (* x2 (+ 3 (* -2 x2)))) (* 3 (- (* 2 x2) 3)))) (* 2 (* x2 (- (* 2 x2) 3)))) (+ 1 (+ (* 2 (* x2 (+ 3 (* -2 x2)))) (* 3 (- (* 2 x2) 3)))) (+ (* 2 (* x2 (+ 3 (* -2 x2)))) (* 3 (- (* 2 x2) 3))) (* x2 (+ 3 (* -2 x2))) (+ 3 (* -2 x2)) (* 2 (* x2 (- (* 2 x2) 3))) (* 4 (* x2 (- (* 2 x2) 3)))) |
| 146.0ms | a | @ | inf | ((* (+ a (+ b (+ c d))) 2) (* 2 (+ c (+ (+ d b) a))) 2 (+ c (+ (+ d b) a)) c (+ (+ d b) a) (* b (/ (+ 1 (pow (/ (+ a d) b) 3)) (+ 1 (- (* (/ (+ a d) b) (/ (+ a d) b)) (* 1 (/ (+ a d) b)))))) b (/ (+ 1 (pow (/ (+ a d) b) 3)) (+ 1 (- (* (/ (+ a d) b) (/ (+ a d) b)) (* 1 (/ (+ a d) b))))) (+ 1 (pow (/ (+ a d) b) 3)) 1 (pow (/ (+ a d) b) 3) (/ (+ a d) b) (+ a d) a d 3 (+ 1 (- (* (/ (+ a d) b) (/ (+ a d) b)) (* 1 (/ (+ a d) b)))) (- (* (/ (+ a d) b) (/ (+ a d) b)) (* 1 (/ (+ a d) b))) (* (/ (+ a d) b) (/ (+ a d) b)) (* 1 (/ (+ a d) b)) (* (+ a (+ b (+ c d))) 2) (* 2 (+ c (+ (+ d b) a))) (+ c (+ (+ d b) a)) (+ (+ d b) a) (+ d b) (* (+ (* (+ (/ (+ d c) b) 1) b) a) 2) (+ (* (+ (/ (+ d c) b) 1) b) a) (+ (/ (+ d c) b) 1) (/ (+ d c) b) (+ d c) (* (+ a (+ b (+ c d))) 2) (* (+ (* (/ (+ (+ d c) a) b) 2) 2) b) (+ (* (/ (+ (+ d c) a) b) 2) 2) (/ (+ (+ d c) a) b) (+ (+ d c) a) (* d (+ 1 (/ (+ a c) d))) (+ 1 (/ (+ a c) d)) (/ (+ a c) d) (+ a c) (* (+ a (+ b (+ c d))) 2) (* (+ (* (/ (+ (+ d c) b) a) 2) 2) a) (+ (* (/ (+ (+ d c) b) a) 2) 2) (* b (+ (* 2 (/ (/ (+ c d) a) b)) (+ (* 2 (/ 1 a)) (* 2 (/ 1 b))))) (+ (* 2 (/ c a)) (* b (+ (* 2 (/ 1 a)) (+ (* 2 (/ d (* a b))) (* 2 (/ 1 b)))))) (/ c a) (* b (+ (* 2 (/ 1 a)) (+ (* 2 (/ d (* a b))) (* 2 (/ 1 b))))) (+ (* 2 (/ 1 a)) (+ (* 2 (/ d (* a b))) (* 2 (/ 1 b)))) (/ 1 a) (+ (* 2 (/ d (* a b))) (* 2 (/ 1 b))) (/ d (* a b)) (* a b) (* 2 (/ 1 b)) (/ 1 b)) |
| 104.0ms | n | @ | 0 | ((* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n)) (/ (* (- (exp i) 1) n) i) (* (- (exp i) 1) n) (- (exp i) 1) i n (* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n)) (* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n)) (- (pow (+ 1 (/ i n)) n) 1) (pow (+ 1 (/ i n)) n) (+ i 1) 1 (/ i n) (* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n)) (- (pow (+ 1 (/ i n)) n) 1) (* (log (/ i n)) n) (log (/ i n)) (/ (* 100 (- (exp (* (log (+ (/ i n) 1)) n)) 1)) (/ i n)) (* 100 (- (exp (* (log (+ (/ i n) 1)) n)) 1)) (- (exp (* (log (+ (/ i n) 1)) n)) 1) (* (log (+ (/ i n) 1)) n) (log (+ (/ i n) 1)) (+ (/ i n) 1)) |
| 92.0ms | eps | @ | 0 | ((- (pow (+ x eps) 5) (pow x 5)) (* (+ (* 5 (/ x eps)) 1) (* (* (* eps eps) (* eps eps)) eps)) (* (* (+ (* 5 x) eps) (* (* eps eps) eps)) eps) (* (+ (* 5 x) eps) (* (* eps eps) eps)) (+ (* 5 x) eps) 5 x eps (* (* eps eps) eps) (* eps eps) (- (pow (+ x eps) 5) (pow x 5)) (* (* (* (* eps eps) eps) eps) eps) (* (* (* eps eps) eps) eps) (- (pow (+ x eps) 5) (pow x 5)) (* (* (* x x) (* x x)) (* 5 eps)) (* (* x x) (* x x)) (* x x) (* 5 eps) (- (pow (+ x eps) 5) (pow x 5)) (* (+ (+ (* (/ (* eps eps) x) 2) (+ (* (/ (* eps eps) x) 8) (* 4 eps))) eps) (* (* x x) (* x x))) (* (+ (* (* eps eps) 10) (* (* 5 eps) x)) (* (* x x) x)) (+ (* (* eps eps) 10) (* (* 5 eps) x)) (* (+ (* 10 eps) (* 5 x)) eps) (+ (* 10 eps) (* 5 x)) 10 (* 5 x) (* (* x x) x) (- (pow (+ x eps) 5) (pow x 5)) (* (+ (* 5 (/ x eps)) 1) (* (* (* eps eps) (* eps eps)) eps)) (* (+ (* 5 x) eps) (exp (* (log eps) 4))) (exp (* (log eps) 4)) (* (log eps) 4) (log eps) 4) |
| 91.0ms | n | @ | inf | ((* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n)) (/ (* (- (exp i) 1) n) i) (* (- (exp i) 1) n) (- (exp i) 1) i n (* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n)) (* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n)) (- (pow (+ 1 (/ i n)) n) 1) (pow (+ 1 (/ i n)) n) (+ i 1) 1 (/ i n) (* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n)) (- (pow (+ 1 (/ i n)) n) 1) (* (log (/ i n)) n) (log (/ i n)) (/ (* 100 (- (exp (* (log (+ (/ i n) 1)) n)) 1)) (/ i n)) (* 100 (- (exp (* (log (+ (/ i n) 1)) n)) 1)) (- (exp (* (log (+ (/ i n) 1)) n)) 1) (* (log (+ (/ i n) 1)) n) (log (+ (/ i n) 1)) (+ (/ i n) 1)) |
Compiled 87 577 to 65 064 computations (25.7% 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)
| 181× | binary-search |
| 57× | left-value |
| 175× | narrow-enough |
| 5× | predicate-same |
| 1× | predicate-failed |
| 924.0ms | 9 854× | 0 | valid |
| 424.0ms | 1 617× | 1 | valid |
| 375.0ms | 513× | 2 | valid |
| 88.0ms | 1 547× | 0 | invalid |
| 21.0ms | 16× | 3 | valid |
| 1.0ms | 17× | 0 | exit |
| 1.0ms | 6× | 1 | exit |
Compiled 93 796 to 74 954 computations (20.1% saved)
ival-pow: 470.0ms (33.6% of total)ival-mult!: 384.0ms (27.4% of total)ival-div!: 190.0ms (13.6% of total)ival-sub!: 85.0ms (6.1% of total)adjust: 78.0ms (5.6% of total)ival-add!: 60.0ms (4.3% of total)ival-sqrt: 58.0ms (4.1% of total)ival-exp: 38.0ms (2.7% of total)ival-neg: 30.0ms (2.1% of total)ival-log1p: 3.0ms (0.2% of total)ival-expm1: 2.0ms (0.1% of total)Loading profile data...