
| Date: | Tuesday, January 7th, 2025 |
|---|---|
| Commit: | ff95bebb on main |
| Seed: | 2025007 |
| Parameters: | 256 points for 4 iterations |
| Flags: | localize:costslocalize:errorsreduce:regimesreduce:binary-searchreduce:branch-expressionssetup:simplifysetup:searchrules:arithmeticrules:polynomialsrules:fractionsrules:exponentsrules:trigonometryrules:hyperbolicrules:numericsrules:specialrules:boolsrules:branchesgenerate:rrgenerate:taylorgenerate:simplifygenerate:proofs default |
| Memory: | 372 640.2 MB |
Time bar (total: 5.8min)
| 51.7s | 433 801× | 0 | valid |
| 10.0s | 26 644× | 1 | valid |
| 4.5s | 9 270× | 2 | valid |
| 2.1s | 4 343× | 0 | invalid |
| 1.3s | 8 339× | 0 | exit |
| 349.0ms | 880× | 3 | valid |
ival-mult: 13.6s (27% of total)ival-add: 6.8s (13.4% of total)const: 4.4s (8.8% of total)ival-div: 3.8s (7.5% of total)ival-exp: 3.4s (6.7% of total)adjust: 3.3s (6.5% of total)ival-hypot: 2.3s (4.5% of total)ival-sub: 2.1s (4.1% of total)ival-log: 1.8s (3.6% of total)ival-asin: 1.2s (2.4% of total)ival-cos: 1.1s (2.1% of total)ival-sin: 1.0s (2% of total)ival-sqrt: 883.0ms (1.7% of total)ival-atan2: 711.0ms (1.4% of total)ival-pi: 381.0ms (0.8% of total)ival-sinu: 367.0ms (0.7% of total)ival->: 365.0ms (0.7% of total)exact: 361.0ms (0.7% of total)ival-pow: 321.0ms (0.6% of total)ival-acosh: 313.0ms (0.6% of total)ival-atanh: 290.0ms (0.6% of total)ival-neg: 289.0ms (0.6% of total)ival-true: 270.0ms (0.5% of total)ival-asinh: 248.0ms (0.5% of total)ival-<=: 236.0ms (0.5% of total)ival-fabs: 232.0ms (0.5% of total)ival-assert: 190.0ms (0.4% of total)ival-cosu: 133.0ms (0.3% of total)ival->=: 113.0ms (0.2% of total)ival-and: 81.0ms (0.2% of total)| 613× | iter limit |
| 385× | node limit |
| 73× | saturated |
| 1× | unsound |
| 476× | iter limit |
| 208× | node limit |
| 33× | fuel |
| 28× | unsound |
| 24× | done |
| 1× | saturated |
Compiled 30 664 to 4 285 computations (86% saved)
| 12.0s | 40 785× | 0 | valid |
| 6.9s | 5 456× | 1 | valid |
| 3.8s | 1 867× | 2 | valid |
| 1.0s | 2 555× | 0 | invalid |
| 398.0ms | 78× | 5 | exit |
| 227.0ms | 571× | 0 | exit |
| 176.0ms | 136× | 3 | valid |
| 8.0ms | 8× | 4 | valid |
Compiled 67 043 to 6 175 computations (90.8% saved)
ival-mult: 4.7s (26.2% of total)ival-add: 2.2s (12.3% of total)adjust: 2.2s (12.2% of total)ival-div: 1.5s (8.5% of total)const: 1.4s (7.9% of total)ival-sub: 905.0ms (5.1% of total)ival-pow: 837.0ms (4.7% of total)ival-exp: 736.0ms (4.1% of total)ival-log: 618.0ms (3.5% of total)ival-hypot: 515.0ms (2.9% of total)ival-sqrt: 297.0ms (1.7% of total)ival-asin: 220.0ms (1.2% of total)ival-cos: 209.0ms (1.2% of total)ival-sin: 205.0ms (1.1% of total)ival-atan2: 188.0ms (1.1% of total)ival-neg: 185.0ms (1% of total)ival-acos: 163.0ms (0.9% of total)ival-pow2: 156.0ms (0.9% of total)ival-cosh: 156.0ms (0.9% of total)ival-pi: 130.0ms (0.7% of total)exact: 79.0ms (0.4% of total)ival-fabs: 53.0ms (0.3% of total)ival-log1p: 48.0ms (0.3% of total)ival-copysign: 46.0ms (0.3% of total)ival-asinh: 43.0ms (0.2% of total)ival-true: 41.0ms (0.2% of total)ival-assert: 21.0ms (0.1% of total)ival-sinh: 20.0ms (0.1% of total)ival-sinu: 14.0ms (0.1% of total)ival-cosu: 11.0ms (0.1% of total)ival-acosh: 7.0ms (0% of total)ival->: 1.0ms (0% of total)ival-then: 0.0ms (0% of total)| 605× | iter limit |
| 155× | node limit |
| 43× | unsound |
| 3× | saturated |
| Operator | Subexpression | Explanation | Count | |
|---|---|---|---|---|
sqrt.f64 | #f | oflow-rescue | 1229 | 0 |
-.f64 | #f | cancellation | 762 | 3 |
/.f64 | #f | o/o | 640 | 0 |
/.f64 | #f | o/n | 196 | 0 |
sin.f64 | #f | sensitivity | 182 | 0 |
cos.f64 | (cos.f64 (+.f64 (*.f64 (log.f64 (sqrt.f64 (+.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)))) y.im) (*.f64 (atan2.f64 x.im x.re) y.re))) | sensitivity | 181 | 0 |
sqrt.f32 | #f | oflow-rescue | 179 | 0 |
+.f64 | #f | cancellation | 153 | 0 |
sqrt.f64 | #f | uflow-rescue | 141 | 0 |
log.f64 | (log.f64 (+.f64 (fabs.f64 x) (sqrt.f64 (+.f64 (*.f64 x x) #s(literal 1 binary64))))) | sensitivity | 118 | 2 |
-.f64 | #f | nan-rescue | 106 | 0 |
log.f32 | (log.f32 (+.f32 (fabs.f32 x) (sqrt.f32 (+.f32 (*.f32 x x) #s(literal 1 binary32))))) | sensitivity | 103 | 4 |
/.f64 | #f | n/o | 92 | 0 |
*.f64 | #f | n*u | 64 | 0 |
/.f64 | #f | u/u | 60 | 0 |
+.f64 | #f | nan-rescue | 38 | 0 |
/.f64 | #f | u/n | 36 | 0 |
*.f64 | #f | n*o | 30 | 0 |
/.f64 | #f | n/u | 9 | 0 |
*.f64 | (*.f64 (*.f64 (sqrt.f64 (*.f64 (PI.f64) #s(literal 2 binary64))) (pow.f64 (+.f64 (+.f64 (-.f64 (-.f64 #s(literal 1 binary64) z) #s(literal 1 binary64)) #s(literal 7 binary64)) #s(literal 1/2 binary64)) (+.f64 (-.f64 (-.f64 #s(literal 1 binary64) z) #s(literal 1 binary64)) #s(literal 1/2 binary64)))) (exp.f64 (neg.f64 (+.f64 (+.f64 (-.f64 (-.f64 #s(literal 1 binary64) z) #s(literal 1 binary64)) #s(literal 7 binary64)) #s(literal 1/2 binary64))))) | o*u | 2 | 0 |
| ↳ | (*.f64 (sqrt.f64 (*.f64 (PI.f64) #s(literal 2 binary64))) (pow.f64 (+.f64 (+.f64 (-.f64 (-.f64 #s(literal 1 binary64) z) #s(literal 1 binary64)) #s(literal 7 binary64)) #s(literal 1/2 binary64)) (+.f64 (-.f64 (-.f64 #s(literal 1 binary64) z) #s(literal 1 binary64)) #s(literal 1/2 binary64)))) | overflow | 3 | |
| ↳ | (pow.f64 (+.f64 (+.f64 (-.f64 (-.f64 #s(literal 1 binary64) z) #s(literal 1 binary64)) #s(literal 7 binary64)) #s(literal 1/2 binary64)) (+.f64 (-.f64 (-.f64 #s(literal 1 binary64) z) #s(literal 1 binary64)) #s(literal 1/2 binary64))) | overflow | 3 | |
| ↳ | (exp.f64 (neg.f64 (+.f64 (+.f64 (-.f64 (-.f64 #s(literal 1 binary64) z) #s(literal 1 binary64)) #s(literal 7 binary64)) #s(literal 1/2 binary64)))) | underflow | 2 | |
cos.f64 | (cos.f64 (+.f64 (*.f64 (log.f64 (sqrt.f64 (+.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)))) y.im) (*.f64 (atan2.f64 x.im x.re) y.re))) | oflow-rescue | 1 | 0 |
| ↳ | (+.f64 (*.f64 (log.f64 (sqrt.f64 (+.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)))) y.im) (*.f64 (atan2.f64 x.im x.re) y.re)) | overflow | 1 | |
| ↳ | (*.f64 x.re x.re) | overflow | 61 | |
| ↳ | (+.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)) | overflow | 113 | |
| ↳ | (*.f64 (log.f64 (sqrt.f64 (+.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)))) y.im) | overflow | 1 | |
| ↳ | (*.f64 x.im x.im) | overflow | 65 | |
log.f32 | (log.f32 (+.f32 x (sqrt.f32 (-.f32 (*.f32 x x) #s(literal 1 binary32))))) | oflow-rescue | 1 | 0 |
| ↳ | (+.f32 x (sqrt.f32 (-.f32 (*.f32 x x) #s(literal 1 binary32)))) | overflow | 1 | |
| ↳ | (*.f32 x x) | overflow | 113 | |
| ↳ | (-.f32 (*.f32 x x) #s(literal 1 binary32)) | overflow | 113 | |
exp.f64 | (exp.f64 (neg.f64 (+.f64 (+.f64 (-.f64 (-.f64 #s(literal 1 binary64) z) #s(literal 1 binary64)) #s(literal 7 binary64)) #s(literal 1/2 binary64)))) | sensitivity | 1 | 0 |
sin.f64 | (sin.f64 (+.f64 (*.f64 (log.f64 (sqrt.f64 (+.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)))) y.im) (*.f64 (atan2.f64 x.im x.re) y.re))) | oflow-rescue | 1 | 0 |
| ↳ | (+.f64 (*.f64 (log.f64 (sqrt.f64 (+.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)))) y.im) (*.f64 (atan2.f64 x.im x.re) y.re)) | overflow | 1 | |
| ↳ | (*.f64 x.re x.re) | overflow | 61 | |
| ↳ | (+.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)) | overflow | 113 | |
| ↳ | (*.f64 (log.f64 (sqrt.f64 (+.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)))) y.im) | overflow | 1 | |
| ↳ | (*.f64 x.im x.im) | overflow | 65 | |
log.f64 | (log.f64 (+.f64 x (sqrt.f64 (-.f64 (*.f64 x x) #s(literal 1 binary64))))) | oflow-rescue | 1 | 0 |
| ↳ | (+.f64 x (sqrt.f64 (-.f64 (*.f64 x x) #s(literal 1 binary64)))) | overflow | 1 | |
| ↳ | (-.f64 (*.f64 x x) #s(literal 1 binary64)) | overflow | 126 | |
| ↳ | (*.f64 x x) | overflow | 126 |
| Predicted + | Predicted - | |
|---|---|---|
| + | 3584 | 44 |
| - | 181 | 10783 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 3584 | 4 | 40 |
| - | 181 | 6 | 10777 |
| number | freq |
|---|---|
| 0 | 10827 |
| 1 | 3205 |
| 2 | 559 |
| 3 | 1 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 37 | 0 | 1 |
| - | 1 | 0 | 18 |
| 3.2s | 25 556× | 0 | valid |
| 1.4s | 2 652× | 1 | valid |
| 914.0ms | 904× | 2 | valid |
| 55.0ms | 68× | 3 | valid |
| 2.0ms | 4× | 5 | exit |
Compiled 13 558 to 2 283 computations (83.2% saved)
ival-mult: 1.0s (26% of total)ival-add: 523.0ms (13.2% of total)adjust: 422.0ms (10.7% of total)ival-exp: 269.0ms (6.8% of total)ival-hypot: 227.0ms (5.7% of total)ival-log: 219.0ms (5.5% of total)ival-sub: 218.0ms (5.5% of total)const: 217.0ms (5.5% of total)ival-div: 208.0ms (5.3% of total)ival-sin: 117.0ms (3% of total)ival-sqrt: 91.0ms (2.3% of total)ival-atan2: 88.0ms (2.2% of total)ival-asin: 72.0ms (1.8% of total)ival-cos: 51.0ms (1.3% of total)ival-pow: 45.0ms (1.1% of total)ival-pi: 41.0ms (1% of total)ival-true: 25.0ms (0.6% of total)exact: 20.0ms (0.5% of total)ival-fabs: 18.0ms (0.5% of total)ival-neg: 16.0ms (0.4% of total)ival-copysign: 12.0ms (0.3% of total)ival-assert: 12.0ms (0.3% of total)ival-log1p: 7.0ms (0.2% of total)ival-sinu: 7.0ms (0.2% of total)ival-cosu: 6.0ms (0.2% of total)Compiled 4 339 241 to 322 099 computations (92.6% saved)
| 114× | iter limit |
| 72× | node limit |
| 42× | saturated |
Compiled 70 096 to 13 093 computations (81.3% saved)
132 calls:
| 933.0ms | i |
| 769.0ms | im |
| 748.0ms | re |
| 498.0ms | y.im |
| 493.0ms | y.re |
Compiled 12 975 to 9 481 computations (26.9% saved)
1269 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 269.0ms | x | @ | -inf | ((log (* (log x) x)) (* (log x) x) (log x) (log (/ x (log x))) (/ x (log x)) (neg (log (* (log x) x))) (+ (* (sqrt (neg (log (log x)))) (sqrt (neg (log (log x))))) (log x)) (sqrt (neg (log (log x)))) (neg (log (log x))) (log (log x))) |
| 152.0ms | x.re | @ | 0 | ((sqrt (+ (* x.re x.re) (* x.im x.im))) (exp (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im))) (+ (* x.re x.re) (* x.im x.im)) (* (exp (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im))) (cos (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re)))) (* (exp (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im))) (cos (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re)))) (exp (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im))) (pow (sqrt (+ (* x.im x.im) (* x.re x.re))) y.re) (sqrt (+ (* x.im x.im) (* x.re x.re))) (exp (neg (+ (* (neg (log x.im)) y.re) (* (atan2 x.im x.re) y.im)))) (neg (+ (* (neg (log x.im)) y.re) (* (atan2 x.im x.re) y.im))) (* (exp (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im))) (cos (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re)))) (exp (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im))) (* (exp (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im))) (cos (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re)))) (* (cos (* (log (sqrt (+ (* x.im x.im) (* x.re x.re)))) y.im)) (pow (exp (neg y.im)) (atan2 x.im x.re))) (cos (* (log (sqrt (+ (* x.im x.im) (* x.re x.re)))) y.im)) (* (log (sqrt (+ (* x.im x.im) (* x.re x.re)))) y.im) (* (cos (+ (* (neg y.im) (log (/ -1 x.re))) (* (atan2 x.im x.re) y.re))) (exp (neg (+ (* (log (/ -1 x.re)) y.re) (* (atan2 x.im x.re) y.im))))) (* (exp (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im))) (cos (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re)))) (cos (+ (* (neg y.im) (log (/ -1 x.re))) (* (atan2 x.im x.re) y.re))) (+ (* (neg y.im) (log (/ -1 x.re))) (* (atan2 x.im x.re) y.re)) (cos (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re))) (cos (* (atan2 x.im x.re) y.re)) (* (atan2 x.im x.re) y.im) (cos (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re))) (cos (* (atan2 x.im x.re) y.re)) (* (atan2 x.im x.re) y.re) (pow (exp (neg y.im)) (atan2 x.im x.re))) |
| 112.0ms | im | @ | 0 | ((/ (* 1/2 (log (+ (* im im) (* re re)))) (log 10)) (* 1/2 (log (+ (* im im) (* re re)))) (log (+ (* im im) (* re re))) (+ (* (/ re im) (/ re im)) (* 2 (log im))) (/ (neg (log (sqrt (+ (* re re) (* im im))))) (log 1/10)) (neg (log (sqrt (+ (* re re) (* im im))))) (log (sqrt (+ (* re re) (* im im)))) (log im) (/ (* 1/2 (log (+ (* im im) (* re re)))) (log 10)) (* (log (* im im)) (/ 1/2 (log 10))) (log (* im im)) (* im im) (/ (* (log (+ (* im im) (* re re))) -1/2) (log 1/10)) (* (log (+ (* im im) (* re re))) -1/2) (log (+ (* im im) (* re re))) (+ (* im im) (* re re)) (/ (* 1/2 (- (log (+ (pow im 6) (pow re 6))) (log (+ (- (pow re 4) (pow (* im re) 2)) (pow im 4))))) (log 10)) (* 1/2 (- (log (+ (pow im 6) (pow re 6))) (log (+ (- (pow re 4) (pow (* im re) 2)) (pow im 4))))) (- (log (+ (pow im 6) (pow re 6))) (log (+ (- (pow re 4) (pow (* im re) 2)) (pow im 4)))) (log (+ (pow im 6) (pow re 6))) (log 10) (log 1/10) (/ 1/2 (log 10)) (* re re) (log (+ (- (pow re 4) (pow (* im re) 2)) (pow im 4))) (+ (- (pow re 4) (pow (* im re) 2)) (pow im 4)) (- (pow re 4) (pow (* im re) 2))) |
| 111.0ms | base | @ | inf | ((* (log (sqrt (+ (* im im) (* re re)))) (/ (log base) (pow (log base) 2))) (log (sqrt (+ (* im im) (* re re)))) (sqrt (+ (* im im) (* re re))) (/ (log base) (pow (log base) 2)) (/ (log base) (pow (log base) 2)) (* (log (sqrt (+ (* im im) (* re re)))) (/ (log base) (pow (log base) 2))) (log (sqrt (+ (* im im) (* re re)))) (log im) (* (/ (* (log base) (log (sqrt (+ (* im im) (* re re))))) (pow (log base) 6)) (pow (log base) 4)) (/ (* (log base) (log (sqrt (+ (* im im) (* re re))))) (pow (log base) 6)) (/ (log im) (pow (log base) 5)) (* (/ (* (log base) (log (sqrt (+ (* im im) (* re re))))) (pow (log base) 6)) (pow (log base) 4)) (/ (* (log base) (log (sqrt (+ (* im im) (* re re))))) (pow (log base) 6)) (* (log base) (log (sqrt (+ (* im im) (* re re))))) (log base) (/ (pow (* (log base) (log (sqrt (+ (* im im) (* re re))))) 3) (* (pow (* (log base) (log (sqrt (+ (* im im) (* re re))))) 2) (pow (log base) 2))) (* (pow (* (log base) (log (sqrt (+ (* im im) (* re re))))) 2) (pow (log base) 2)) (pow (* (log base) (log (sqrt (+ (* im im) (* re re))))) 3) (* (log base) (log (sqrt (+ (* im im) (* re re))))) (/ 1 (log base)) (pow (log base) 2) (pow (log base) 5) (pow (log base) 4) (pow (log base) 6) (pow (* (log base) (log (sqrt (+ (* im im) (* re re))))) 2)) |
| 109.0ms | x.re | @ | 0 | ((- (* x.im (/ y.re (+ (* y.im y.im) (* y.re y.re)))) (* x.re (/ y.im (+ (* y.im y.im) (* y.re y.re))))) (* x.im (/ y.re (+ (* y.im y.im) (* y.re y.re)))) (/ y.re (+ (* y.im y.im) (* y.re y.re))) (+ (* y.im y.im) (* y.re y.re)) (/ (- (* x.im y.re) (* x.re y.im)) (+ (* y.re y.re) (* y.im y.im))) (/ x.im y.re) (/ (- (* x.im y.re) (* x.re y.im)) (+ (* y.re y.re) (* y.im y.im))) (* (neg x.re) (/ y.im (+ (* y.im y.im) (* y.re y.re)))) (neg x.re) (/ y.im (+ (* y.im y.im) (* y.re y.re))) (/ (- (* x.im y.re) (* x.re y.im)) (+ (* y.re y.re) (* y.im y.im))) (/ (- x.im (/ (* x.re y.im) y.re)) y.re) (- x.im (/ (* x.re y.im) y.re)) (/ (* x.re y.im) y.re) (* (/ (+ (* (/ y.re x.re) x.im) (neg y.im)) (+ (* y.im y.im) (* y.re y.re))) x.re) (/ (- (* x.im y.re) (* x.re y.im)) (+ (* y.re y.re) (* y.im y.im))) (/ (+ (* (/ y.re x.re) x.im) (neg y.im)) (+ (* y.im y.im) (* y.re y.re))) (+ (* (/ y.re x.re) x.im) (neg y.im)) (* x.re (/ y.im (+ (* y.im y.im) (* y.re y.re))))) |
Compiled 237 902 to 103 806 computations (56.4% saved)
| 259× | binary-search |
| 199× | left-value |
| 249× | narrow-enough |
| 10× | predicate-same |
| 2.0s | 17 918× | 0 | valid |
| 686.0ms | 1 549× | 1 | valid |
| 98.0ms | 222× | 2 | valid |
| 36.0ms | 39× | 3 | valid |
Compiled 140 922 to 81 968 computations (41.8% saved)
ival-mult: 720.0ms (36.2% of total)ival-add: 184.0ms (9.3% of total)ival-hypot: 165.0ms (8.3% of total)ival-sin: 136.0ms (6.8% of total)const: 114.0ms (5.7% of total)adjust: 111.0ms (5.6% of total)ival-sub: 110.0ms (5.5% of total)ival-exp: 109.0ms (5.5% of total)ival-div: 88.0ms (4.4% of total)ival-log: 79.0ms (4% of total)ival-cos: 74.0ms (3.7% of total)ival-atan2: 41.0ms (2.1% of total)ival-sqrt: 19.0ms (1% of total)ival-true: 14.0ms (0.7% of total)ival-assert: 7.0ms (0.4% of total)exact: 6.0ms (0.3% of total)ival-fabs: 5.0ms (0.3% of total)ival-neg: 4.0ms (0.2% of total)ival-pi: 1.0ms (0.1% of total)| 58× | search |
| Probability | Valid | Unknown | Precondition | Infinite | Domain | Can't | Iter |
|---|---|---|---|---|---|---|---|
| 0% | 0% | 86.3% | 13.7% | 0% | 0% | 0% | 0 |
| 55.4% | 47.8% | 38.5% | 13.7% | 0% | 0% | 0% | 1 |
| 65.9% | 55.7% | 28.9% | 13.7% | 0% | 1.7% | 0% | 2 |
| 71.2% | 58.4% | 23.6% | 13.7% | 0% | 4.3% | 0% | 3 |
| 77.4% | 62% | 18.1% | 13.7% | 0% | 6.2% | 0% | 4 |
| 83.5% | 66.8% | 13.2% | 13.7% | 0% | 6.3% | 0% | 5 |
| 85.8% | 68.3% | 11.3% | 13.7% | 0% | 6.6% | 0% | 6 |
| 88.3% | 70.3% | 9.4% | 13.7% | 0% | 6.6% | 0% | 7 |
| 89.9% | 71.5% | 8% | 13.7% | 0% | 6.8% | 0% | 8 |
| 91.1% | 72.5% | 7.1% | 13.7% | 0% | 6.8% | 0% | 9 |
| 92.6% | 73.6% | 5.9% | 13.7% | 0% | 6.8% | 0% | 10 |
| 94% | 74.7% | 4.8% | 13.7% | 0% | 6.8% | 0% | 11 |
| 94.5% | 75.1% | 4.4% | 13.7% | 0% | 6.9% | 0% | 12 |
Compiled 1 498 to 816 computations (45.5% saved)
Loading profile data...