
| Date: | Wednesday, April 30th, 2025 |
|---|---|
| Commit: | 77680327 on prove-soundness |
| Seed: | 2025120 |
| 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: | 474 798.0 MB |
Time bar (total: 6.8min)
| 47.5s | 118 666× | 1 | valid |
| 34.5s | 281 928× | 0 | valid |
| 19.1s | 3 872× | 4 | exit |
| 14.8s | 25 472× | 2 | valid |
| 8.8s | 11 549× | 5 | exit |
| 8.4s | 3 220× | 3 | valid |
| 5.4s | 34 658× | 0 | exit |
| 2.9s | 20 082× | 0 | invalid |
| 2.8s | 12 083× | 1 | invalid |
| 330.0ms | 904× | 2 | invalid |
| 299.0ms | 2 653× | 1 | exit |
| 127.0ms | 26× | 4 | valid |
ival-pow: 22.1s (17.9% of total)adjust: 14.1s (11.4% of total)ival-mult!: 12.1s (9.8% of total)ival-cos: 11.5s (9.3% of total)ival-sin: 10.1s (8.1% of total)ival-pow2: 8.8s (7.1% of total)ival-div!: 8.2s (6.6% of total)ival-cosu: 5.9s (4.8% of total)ival-sinu: 5.7s (4.6% of total)ival-exp: 5.6s (4.6% of total)ival-log: 4.0s (3.2% of total)ival-sqrt: 3.5s (2.8% of total)ival-add!: 3.0s (2.5% of total)ival-sub!: 3.0s (2.5% of total)ival-neg: 2.0s (1.6% of total)ival-hypot: 924.0ms (0.7% of total)ival-atan2: 801.0ms (0.6% of total)ival-tan: 729.0ms (0.6% of total)ival-acos: 437.0ms (0.4% of total)ival-cbrt: 303.0ms (0.2% of total)ival-atan: 289.0ms (0.2% of total)ival-fabs: 207.0ms (0.2% of total)ival-log1p: 129.0ms (0.1% of total)ival-asin: 105.0ms (0.1% of total)ival-<: 94.0ms (0.1% of total)ival-and: 48.0ms (0% of total)ival-assert: 8.0ms (0% of total)ival-<=: 6.0ms (0% of total)ival-==: 1.0ms (0% of total)ival-pi: 0.0ms (0% of total)ival-or: 0.0ms (0% of total)| 455× | iter-limit |
| 188× | node-limit |
| 7× | unsound |
| 3× | saturated |
1620 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 4.3s | ew | @ | 0 | ((fabs (- (* (* ew (cos t)) (cos (atan (/ (* (neg eh) (tan t)) ew)))) (* (* eh (sin t)) (sin (atan (/ (* (neg eh) (tan t)) ew)))))) (- (* (* ew (cos t)) (cos (atan (/ (* (neg eh) (tan t)) ew)))) (* (* eh (sin t)) (sin (atan (/ (* (neg eh) (tan t)) ew))))) (neg (* (+ (* eh (/ (* (tanh (asinh (neg (* (/ eh ew) (tan t))))) (sin t)) ew)) (neg (* (/ 1 (sqrt (+ 1 (pow (neg (* (/ eh ew) (tan t))) 2)))) (cos t)))) ew)) (* (+ (* eh (/ (* (tanh (asinh (neg (* (/ eh ew) (tan t))))) (sin t)) ew)) (neg (* (/ 1 (sqrt (+ 1 (pow (neg (* (/ eh ew) (tan t))) 2)))) (cos t)))) ew) (+ (* eh (/ (* (tanh (asinh (neg (* (/ eh ew) (tan t))))) (sin t)) ew)) (neg (* (/ 1 (sqrt (+ 1 (pow (neg (* (/ eh ew) (tan t))) 2)))) (cos t)))) eh (/ (* (tanh (asinh (neg (* (/ eh ew) (tan t))))) (sin t)) ew) (* (tanh (asinh (neg (* (/ eh ew) (tan t))))) (sin t)) (tanh (asinh (neg (* (/ eh ew) (tan t))))) (asinh (neg (* (/ eh ew) (tan t)))) (neg (* (/ eh ew) (tan t))) (* (/ eh ew) (tan t)) (/ eh ew) ew (tan t) t (sin t) (neg (* (/ 1 (sqrt (+ 1 (pow (neg (* (/ eh ew) (tan t))) 2)))) (cos t))) (* (/ 1 (sqrt (+ 1 (pow (neg (* (/ eh ew) (tan t))) 2)))) (cos t)) (/ 1 (sqrt (+ 1 (pow (neg (* (/ eh ew) (tan t))) 2)))) 1 (sqrt (+ 1 (pow (neg (* (/ eh ew) (tan t))) 2))) (+ 1 (pow (neg (* (/ eh ew) (tan t))) 2)) (pow (neg (* (/ eh ew) (tan t))) 2) 2 (cos t) (fabs (- (* (* ew (cos t)) (cos (atan (/ (* (neg eh) (tan t)) ew)))) (* (* eh (sin t)) (sin (atan (/ (* (neg eh) (tan t)) ew)))))) (- (* (* ew (cos t)) (cos (atan (/ (* (neg eh) (tan t)) ew)))) (* (* eh (sin t)) (sin (atan (/ (* (neg eh) (tan t)) ew))))) (* (/ 1 (sqrt (+ 1 (pow (neg (* (/ eh ew) (tan t))) 2)))) ew) (fabs (- (* (* ew (cos t)) (cos (atan (/ (* (neg eh) (tan t)) ew)))) (* (* eh (sin t)) (sin (atan (/ (* (neg eh) (tan t)) ew)))))) (- (* (* ew (cos t)) (cos (atan (/ (* (neg eh) (tan t)) ew)))) (* (* eh (sin t)) (sin (atan (/ (* (neg eh) (tan t)) ew))))) (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (neg (* (/ eh ew) (tan t))) 2))))) (* (cos t) ew) (fabs (- (* (* ew (cos t)) (cos (atan (/ (* (neg eh) (tan t)) ew)))) (* (* eh (sin t)) (sin (atan (/ (* (neg eh) (tan t)) ew)))))) (- (* (* ew (cos t)) (cos (atan (/ (* (neg eh) (tan t)) ew)))) (* (* eh (sin t)) (sin (atan (/ (* (neg eh) (tan t)) ew))))) (* (* ew (cos t)) (cos (atan (/ (* (neg eh) (tan t)) ew)))) (* ew (cos t)) (cos (atan (/ (* (neg eh) (tan t)) ew))) (atan (/ (* (neg eh) (tan t)) ew)) (/ (* (neg eh) (tan t)) ew) (* (neg eh) (tan t)) (neg eh) (* (* eh (sin t)) (sin (atan (/ (* (neg eh) (tan t)) ew)))) (* (* eh t) (tanh (asinh (neg (* (/ eh ew) (tan t)))))) (* eh t) (fabs (/ (- (pow (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) 3) (pow (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew))))) 3)) (+ (pow (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) 2) (+ (pow (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew))))) 2) (* (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew)))))))))) (/ (- (pow (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) 3) (pow (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew))))) 3)) (+ (pow (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) 2) (+ (pow (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew))))) 2) (* (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew))))))))) (- (pow (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) 3) (pow (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew))))) 3)) (pow (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) 3) (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2)))) (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))) (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2)) (pow (* (neg eh) (/ (tan t) ew)) 2) (* (neg eh) (/ (tan t) ew)) (/ (tan t) ew) 3 (pow (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew))))) 3) (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew))))) (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew)))) (asinh (* (neg eh) (/ (tan t) ew))) (+ (pow (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) 2) (+ (pow (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew))))) 2) (* (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew)))))))) (pow (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) 2) (+ (pow (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew))))) 2) (* (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew))))))) (pow (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew))))) 2) (* (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew))))))) |
| 1.2s | t | @ | -inf | ((/ (* (pow (/ 1 (+ 1 (exp (neg s)))) c_p) (pow (- 1 (/ 1 (+ 1 (exp (neg s))))) c_n)) (* (pow (/ 1 (+ 1 (exp (neg t)))) c_p) (pow (- 1 (/ 1 (+ 1 (exp (neg t))))) c_n))) (exp (- (* (neg (log (+ (exp (neg s)) 1))) c_p) (* (neg (log (+ (exp (neg t)) 1))) c_p))) (- (* (neg (log (+ (exp (neg s)) 1))) c_p) (* (neg (log (+ (exp (neg t)) 1))) c_p)) (* (neg (log (+ (exp (neg s)) 1))) c_p) (neg (log (+ (exp (neg s)) 1))) (- (* 1/2 s) (log 2)) (* 1/2 s) 1/2 s (log 2) 2 c_p (* (neg (log (+ (exp (neg t)) 1))) c_p) (neg (log (+ (exp (neg t)) 1))) (log (+ (exp (neg t)) 1)) (+ (exp (neg t)) 1) (exp (neg t)) (neg t) t 1 (/ (* (pow (/ 1 (+ 1 (exp (neg s)))) c_p) (pow (- 1 (/ 1 (+ 1 (exp (neg s))))) c_n)) (* (pow (/ 1 (+ 1 (exp (neg t)))) c_p) (pow (- 1 (/ 1 (+ 1 (exp (neg t))))) c_n))) (exp (- (* (neg (log (+ (exp (neg s)) 1))) c_p) (* (neg (log (+ (exp (neg t)) 1))) c_p))) (/ (* (pow (/ 1 (+ 1 (exp (neg s)))) c_p) (pow (- 1 (/ 1 (+ 1 (exp (neg s))))) c_n)) (* (pow (/ 1 (+ 1 (exp (neg t)))) c_p) (pow (- 1 (/ 1 (+ 1 (exp (neg t))))) c_n))) (exp (- (* (neg (log (+ (exp (neg s)) 1))) c_p) (* (neg (log (+ (exp (neg t)) 1))) c_p))) (- (* (neg (log (+ (exp (neg s)) 1))) c_p) (* (neg (log (+ (exp (neg t)) 1))) c_p)) (* (neg (log (+ (exp (neg s)) 1))) c_p) (neg (log (+ (exp (neg s)) 1))) (log 1/2) (/ (* (pow (/ 1 (+ 1 (exp (neg s)))) c_p) (pow (- 1 (/ 1 (+ 1 (exp (neg s))))) c_n)) (* (pow (/ 1 (+ 1 (exp (neg t)))) c_p) (pow (- 1 (/ 1 (+ 1 (exp (neg t))))) c_n))) (exp (- (* (neg (log (+ (exp (neg s)) 1))) c_p) (* (neg (log (+ (exp (neg t)) 1))) c_p))) (- (* (neg (log (+ (exp (neg s)) 1))) c_p) (* (neg (log (+ (exp (neg t)) 1))) c_p)) (* (neg (log (+ (exp (neg s)) 1))) c_p) (neg (log (+ (exp (neg s)) 1))) (log (+ (exp (neg s)) 1)) (+ (exp (neg s)) 1) (exp (neg s)) (neg s) (* (neg (log (+ (exp (neg t)) 1))) c_p) (neg (log (+ (exp (neg t)) 1))) (/ (* (pow (/ 1 (+ 1 (exp (neg s)))) c_p) (pow (- 1 (/ 1 (+ 1 (exp (neg s))))) c_n)) (* (pow (/ 1 (+ 1 (exp (neg t)))) c_p) (pow (- 1 (/ 1 (+ 1 (exp (neg t))))) c_n))) (exp (- (* (neg (log (+ (exp (neg s)) 1))) c_p) (* (neg (log (+ (exp (neg t)) 1))) c_p))) (+ 1 (* c_p (- (neg (log (+ 1 (exp (neg s))))) (neg (log (+ 1 (exp (neg t)))))))) (* c_p (- (neg (log (+ 1 (exp (neg s))))) (neg (log (+ 1 (exp (neg t))))))) (- (neg (log (+ 1 (exp (neg s))))) (neg (log (+ 1 (exp (neg t)))))) (neg (log (+ 1 (exp (neg s))))) (log (+ 1 (exp (neg s)))) (+ 1 (exp (neg s))) (neg (log (+ 1 (exp (neg t))))) (log (+ 1 (exp (neg t)))) (+ 1 (exp (neg t)))) |
| 1.1s | y-scale | @ | inf | ((* 180 (/ (atan (/ (- (- (/ (/ (+ (pow (* a (cos (* (/ angle 180) (PI)))) 2) (pow (* b (sin (* (/ angle 180) (PI)))) 2)) y-scale) y-scale) (/ (/ (+ (pow (* a (sin (* (/ angle 180) (PI)))) 2) (pow (* b (cos (* (/ angle 180) (PI)))) 2)) x-scale) x-scale)) (sqrt (+ (pow (- (/ (/ (+ (pow (* a (sin (* (/ angle 180) (PI)))) 2) (pow (* b (cos (* (/ angle 180) (PI)))) 2)) x-scale) x-scale) (/ (/ (+ (pow (* a (cos (* (/ angle 180) (PI)))) 2) (pow (* b (sin (* (/ angle 180) (PI)))) 2)) y-scale) y-scale)) 2) (pow (/ (/ (* (* (* 2 (- (pow b 2) (pow a 2))) (sin (* (/ angle 180) (PI)))) (cos (* (/ angle 180) (PI)))) x-scale) y-scale) 2)))) (/ (/ (* (* (* 2 (- (pow b 2) (pow a 2))) (sin (* (/ angle 180) (PI)))) (cos (* (/ angle 180) (PI)))) x-scale) y-scale))) (PI))) 180 (/ (atan (/ (- (- (/ (/ (+ (pow (* a (cos (* (/ angle 180) (PI)))) 2) (pow (* b (sin (* (/ angle 180) (PI)))) 2)) y-scale) y-scale) (/ (/ (+ (pow (* a (sin (* (/ angle 180) (PI)))) 2) (pow (* b (cos (* (/ angle 180) (PI)))) 2)) x-scale) x-scale)) (sqrt (+ (pow (- (/ (/ (+ (pow (* a (sin (* (/ angle 180) (PI)))) 2) (pow (* b (cos (* (/ angle 180) (PI)))) 2)) x-scale) x-scale) (/ (/ (+ (pow (* a (cos (* (/ angle 180) (PI)))) 2) (pow (* b (sin (* (/ angle 180) (PI)))) 2)) y-scale) y-scale)) 2) (pow (/ (/ (* (* (* 2 (- (pow b 2) (pow a 2))) (sin (* (/ angle 180) (PI)))) (cos (* (/ angle 180) (PI)))) x-scale) y-scale) 2)))) (/ (/ (* (* (* 2 (- (pow b 2) (pow a 2))) (sin (* (/ angle 180) (PI)))) (cos (* (/ angle 180) (PI)))) x-scale) y-scale))) (PI)) (atan (/ (- (- (/ (/ (+ (pow (* a (cos (* (/ angle 180) (PI)))) 2) (pow (* b (sin (* (/ angle 180) (PI)))) 2)) y-scale) y-scale) (/ (/ (+ (pow (* a (sin (* (/ angle 180) (PI)))) 2) (pow (* b (cos (* (/ angle 180) (PI)))) 2)) x-scale) x-scale)) (sqrt (+ (pow (- (/ (/ (+ (pow (* a (sin (* (/ angle 180) (PI)))) 2) (pow (* b (cos (* (/ angle 180) (PI)))) 2)) x-scale) x-scale) (/ (/ (+ (pow (* a (cos (* (/ angle 180) (PI)))) 2) (pow (* b (sin (* (/ angle 180) (PI)))) 2)) y-scale) y-scale)) 2) (pow (/ (/ (* (* (* 2 (- (pow b 2) (pow a 2))) (sin (* (/ angle 180) (PI)))) (cos (* (/ angle 180) (PI)))) x-scale) y-scale) 2)))) (/ (/ (* (* (* 2 (- (pow b 2) (pow a 2))) (sin (* (/ angle 180) (PI)))) (cos (* (/ angle 180) (PI)))) x-scale) y-scale))) (/ (- (- (/ (/ (+ (pow (* a (cos (* (/ angle 180) (PI)))) 2) (pow (* b (sin (* (/ angle 180) (PI)))) 2)) y-scale) y-scale) (/ (/ (+ (pow (* a (sin (* (/ angle 180) (PI)))) 2) (pow (* b (cos (* (/ angle 180) (PI)))) 2)) x-scale) x-scale)) (sqrt (+ (pow (- (/ (/ (+ (pow (* a (sin (* (/ angle 180) (PI)))) 2) (pow (* b (cos (* (/ angle 180) (PI)))) 2)) x-scale) x-scale) (/ (/ (+ (pow (* a (cos (* (/ angle 180) (PI)))) 2) (pow (* b (sin (* (/ angle 180) (PI)))) 2)) y-scale) y-scale)) 2) (pow (/ (/ (* (* (* 2 (- (pow b 2) (pow a 2))) (sin (* (/ angle 180) (PI)))) (cos (* (/ angle 180) (PI)))) x-scale) y-scale) 2)))) (/ (/ (* (* (* 2 (- (pow b 2) (pow a 2))) (sin (* (/ angle 180) (PI)))) (cos (* (/ angle 180) (PI)))) x-scale) y-scale)) (- (- (/ (/ (+ (pow (* a (cos (* (/ angle 180) (PI)))) 2) (pow (* b (sin (* (/ angle 180) (PI)))) 2)) y-scale) y-scale) (/ (/ (+ (pow (* a (sin (* (/ angle 180) (PI)))) 2) (pow (* b (cos (* (/ angle 180) (PI)))) 2)) x-scale) x-scale)) (sqrt (+ (pow (- (/ (/ (+ (pow (* a (sin (* (/ angle 180) (PI)))) 2) (pow (* b (cos (* (/ angle 180) (PI)))) 2)) x-scale) x-scale) (/ (/ (+ (pow (* a (cos (* (/ angle 180) (PI)))) 2) (pow (* b (sin (* (/ angle 180) (PI)))) 2)) y-scale) y-scale)) 2) (pow (/ (/ (* (* (* 2 (- (pow b 2) (pow a 2))) (sin (* (/ angle 180) (PI)))) (cos (* (/ angle 180) (PI)))) x-scale) y-scale) 2)))) (- (/ (/ (+ (pow (* a (cos (* (/ angle 180) (PI)))) 2) (pow (* b (sin (* (/ angle 180) (PI)))) 2)) y-scale) y-scale) (/ (/ (+ (pow (* a (sin (* (/ angle 180) (PI)))) 2) (pow (* b (cos (* (/ angle 180) (PI)))) 2)) x-scale) x-scale)) (/ (/ (+ (pow (* a (cos (* (/ angle 180) (PI)))) 2) (pow (* b (sin (* (/ angle 180) (PI)))) 2)) y-scale) y-scale) (/ (+ (pow (* a (cos (* (/ angle 180) (PI)))) 2) (pow (* b (sin (* (/ angle 180) (PI)))) 2)) y-scale) (+ (pow (* a (cos (* (/ angle 180) (PI)))) 2) (pow (* b (sin (* (/ angle 180) (PI)))) 2)) (pow (* a (cos (* (/ angle 180) (PI)))) 2) (* a (cos (* (/ angle 180) (PI)))) a (cos (* (/ angle 180) (PI))) (* (/ angle 180) (PI)) (/ angle 180) angle (PI) 2 (pow (* b (sin (* (/ angle 180) (PI)))) 2) (* b (sin (* (/ angle 180) (PI)))) b (sin (* (/ angle 180) (PI))) y-scale (/ (/ (+ (pow (* a (sin (* (/ angle 180) (PI)))) 2) (pow (* b (cos (* (/ angle 180) (PI)))) 2)) x-scale) x-scale) (/ (+ (pow (* a (sin (* (/ angle 180) (PI)))) 2) (pow (* b (cos (* (/ angle 180) (PI)))) 2)) x-scale) (+ (pow (* a (sin (* (/ angle 180) (PI)))) 2) (pow (* b (cos (* (/ angle 180) (PI)))) 2)) (pow (* a (sin (* (/ angle 180) (PI)))) 2) (* a (sin (* (/ angle 180) (PI)))) (pow (* b (cos (* (/ angle 180) (PI)))) 2) (* b (cos (* (/ angle 180) (PI)))) x-scale (sqrt (+ (pow (- (/ (/ (+ (pow (* a (sin (* (/ angle 180) (PI)))) 2) (pow (* b (cos (* (/ angle 180) (PI)))) 2)) x-scale) x-scale) (/ (/ (+ (pow (* a (cos (* (/ angle 180) (PI)))) 2) (pow (* b (sin (* (/ angle 180) (PI)))) 2)) y-scale) y-scale)) 2) (pow (/ (/ (* (* (* 2 (- (pow b 2) (pow a 2))) (sin (* (/ angle 180) (PI)))) (cos (* (/ angle 180) (PI)))) x-scale) y-scale) 2))) (+ (pow (- (/ (/ (+ (pow (* a (sin (* (/ angle 180) (PI)))) 2) (pow (* b (cos (* (/ angle 180) (PI)))) 2)) x-scale) x-scale) (/ (/ (+ (pow (* a (cos (* (/ angle 180) (PI)))) 2) (pow (* b (sin (* (/ angle 180) (PI)))) 2)) y-scale) y-scale)) 2) (pow (/ (/ (* (* (* 2 (- (pow b 2) (pow a 2))) (sin (* (/ angle 180) (PI)))) (cos (* (/ angle 180) (PI)))) x-scale) y-scale) 2)) (pow (- (/ (/ (+ (pow (* a (sin (* (/ angle 180) (PI)))) 2) (pow (* b (cos (* (/ angle 180) (PI)))) 2)) x-scale) x-scale) (/ (/ (+ (pow (* a (cos (* (/ angle 180) (PI)))) 2) (pow (* b (sin (* (/ angle 180) (PI)))) 2)) y-scale) y-scale)) 2) (- (/ (/ (+ (pow (* a (sin (* (/ angle 180) (PI)))) 2) (pow (* b (cos (* (/ angle 180) (PI)))) 2)) x-scale) x-scale) (/ (/ (+ (pow (* a (cos (* (/ angle 180) (PI)))) 2) (pow (* b (sin (* (/ angle 180) (PI)))) 2)) y-scale) y-scale)) (pow (/ (/ (* (* (* 2 (- (pow b 2) (pow a 2))) (sin (* (/ angle 180) (PI)))) (cos (* (/ angle 180) (PI)))) x-scale) y-scale) 2) (/ (/ (* (* (* 2 (- (pow b 2) (pow a 2))) (sin (* (/ angle 180) (PI)))) (cos (* (/ angle 180) (PI)))) x-scale) y-scale) (/ (* (* (* 2 (- (pow b 2) (pow a 2))) (sin (* (/ angle 180) (PI)))) (cos (* (/ angle 180) (PI)))) x-scale) (* (* (* 2 (- (pow b 2) (pow a 2))) (sin (* (/ angle 180) (PI)))) (cos (* (/ angle 180) (PI)))) (* (* 2 (- (pow b 2) (pow a 2))) (sin (* (/ angle 180) (PI)))) (* 2 (- (pow b 2) (pow a 2))) (- (pow b 2) (pow a 2)) (pow b 2) (pow a 2)) |
| 252.0ms | ew | @ | 0 | ((fabs (- (* (* ew (cos t)) (cos (atan (/ (* (neg eh) (tan t)) ew)))) (* (* eh (sin t)) (sin (atan (/ (* (neg eh) (tan t)) ew)))))) (- (* (* ew (cos t)) (cos (atan (/ (* (neg eh) (tan t)) ew)))) (* (* eh (sin t)) (sin (atan (/ (* (neg eh) (tan t)) ew))))) (neg (* (+ (* eh (/ (* (tanh (asinh (neg (* (/ eh ew) (tan t))))) (sin t)) ew)) (neg (* (/ 1 (sqrt (+ 1 (pow (neg (* (/ eh ew) (tan t))) 2)))) (cos t)))) ew)) (* (+ (* eh (/ (* (tanh (asinh (neg (* (/ eh ew) (tan t))))) (sin t)) ew)) (neg (* (/ 1 (sqrt (+ 1 (pow (neg (* (/ eh ew) (tan t))) 2)))) (cos t)))) ew) (+ (* eh (/ (* (tanh (asinh (neg (* (/ eh ew) (tan t))))) (sin t)) ew)) (neg (* (/ 1 (sqrt (+ 1 (pow (neg (* (/ eh ew) (tan t))) 2)))) (cos t)))) eh (/ (* (tanh (asinh (neg (* (/ eh ew) (tan t))))) (sin t)) ew) (* (tanh (asinh (neg (* (/ eh ew) (tan t))))) (sin t)) (tanh (asinh (neg (* (/ eh ew) (tan t))))) (asinh (neg (* (/ eh ew) (tan t)))) (neg (* (/ eh ew) (tan t))) (* (/ eh ew) (tan t)) (/ eh ew) ew (tan t) t (sin t) (neg (* (/ 1 (sqrt (+ 1 (pow (neg (* (/ eh ew) (tan t))) 2)))) (cos t))) (* (/ 1 (sqrt (+ 1 (pow (neg (* (/ eh ew) (tan t))) 2)))) (cos t)) (/ 1 (sqrt (+ 1 (pow (neg (* (/ eh ew) (tan t))) 2)))) 1 (sqrt (+ 1 (pow (neg (* (/ eh ew) (tan t))) 2))) (+ 1 (pow (neg (* (/ eh ew) (tan t))) 2)) (pow (neg (* (/ eh ew) (tan t))) 2) 2 (cos t) (fabs (/ (- (pow (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) 3) (pow (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew))))) 3)) (+ (pow (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) 2) (+ (pow (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew))))) 2) (* (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew)))))))))) (/ (- (pow (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) 3) (pow (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew))))) 3)) (+ (pow (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) 2) (+ (pow (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew))))) 2) (* (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew))))))))) (fabs (/ (- (pow (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) 3) (pow (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew))))) 3)) (+ (pow (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) 2) (+ (pow (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew))))) 2) (* (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew)))))))))) (/ (- (pow (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) 3) (pow (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew))))) 3)) (+ (pow (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) 2) (+ (pow (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew))))) 2) (* (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew))))))))) (* ew (cos t)) (fabs (- (* (* ew (cos t)) (cos (atan (/ (* (neg eh) (tan t)) ew)))) (* (* eh (sin t)) (sin (atan (/ (* (neg eh) (tan t)) ew)))))) (- (* (* ew (cos t)) (cos (atan (/ (* (neg eh) (tan t)) ew)))) (* (* eh (sin t)) (sin (atan (/ (* (neg eh) (tan t)) ew))))) (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (neg (* (/ eh ew) (tan t))) 2))))) (* (cos t) ew) (+ ew (* (* t t) (+ (* -1/2 ew) (* 1/24 (* ew (* t t)))))) (* (* t t) (+ (* -1/2 ew) (* 1/24 (* ew (* t t))))) (* t t) (+ (* -1/2 ew) (* 1/24 (* ew (* t t)))) -1/2 (* 1/24 (* ew (* t t))) 1/24 (* ew (* t t)) (/ 1 (sqrt (+ 1 (pow (neg (* (/ eh ew) (tan t))) 2)))) (sqrt (+ 1 (pow (neg (* (/ eh ew) (tan t))) 2))) (+ 1 (pow (neg (* (/ eh ew) (tan t))) 2)) (pow (neg (* (/ eh ew) (tan t))) 2) (neg (* (/ eh ew) (tan t))) (* (/ eh ew) (tan t)) (tan t) (* (sqrt (- (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew))))))) (sqrt (- (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew)))))))) (sqrt (- (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew))))))) (- (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew)))))) (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2)))) (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))) (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2)) (pow (* (neg eh) (/ (tan t) ew)) 2) (* (neg eh) (/ (tan t) ew)) (neg eh) (/ (tan t) ew) (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew))))) (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew)))) (asinh (* (neg eh) (/ (tan t) ew)))) |
| 247.0ms | eh | @ | inf | ((fabs (- (* (* ew (cos t)) (cos (atan (/ (* (neg eh) (tan t)) ew)))) (* (* eh (sin t)) (sin (atan (/ (* (neg eh) (tan t)) ew)))))) (- (* (* ew (cos t)) (cos (atan (/ (* (neg eh) (tan t)) ew)))) (* (* eh (sin t)) (sin (atan (/ (* (neg eh) (tan t)) ew))))) (neg (* (+ (* eh (/ (* (tanh (asinh (neg (* (/ eh ew) (tan t))))) (sin t)) ew)) (neg (* (/ 1 (sqrt (+ 1 (pow (neg (* (/ eh ew) (tan t))) 2)))) (cos t)))) ew)) (* (+ (* eh (/ (* (tanh (asinh (neg (* (/ eh ew) (tan t))))) (sin t)) ew)) (neg (* (/ 1 (sqrt (+ 1 (pow (neg (* (/ eh ew) (tan t))) 2)))) (cos t)))) ew) (+ (* eh (/ (* (tanh (asinh (neg (* (/ eh ew) (tan t))))) (sin t)) ew)) (neg (* (/ 1 (sqrt (+ 1 (pow (neg (* (/ eh ew) (tan t))) 2)))) (cos t)))) eh (/ (* (tanh (asinh (neg (* (/ eh ew) (tan t))))) (sin t)) ew) (* (tanh (asinh (neg (* (/ eh ew) (tan t))))) (sin t)) (tanh (asinh (neg (* (/ eh ew) (tan t))))) (asinh (neg (* (/ eh ew) (tan t)))) (neg (* (/ eh ew) (tan t))) (* (/ eh ew) (tan t)) (/ eh ew) ew (tan t) t (sin t) (neg (* (/ 1 (sqrt (+ 1 (pow (neg (* (/ eh ew) (tan t))) 2)))) (cos t))) (* (/ 1 (sqrt (+ 1 (pow (neg (* (/ eh ew) (tan t))) 2)))) (cos t)) (/ 1 (sqrt (+ 1 (pow (neg (* (/ eh ew) (tan t))) 2)))) 1 (sqrt (+ 1 (pow (neg (* (/ eh ew) (tan t))) 2))) (+ 1 (pow (neg (* (/ eh ew) (tan t))) 2)) (pow (neg (* (/ eh ew) (tan t))) 2) 2 (cos t) (fabs (- (* (* ew (cos t)) (cos (atan (/ (* (neg eh) (tan t)) ew)))) (* (* eh (sin t)) (sin (atan (/ (* (neg eh) (tan t)) ew)))))) (- (* (* ew (cos t)) (cos (atan (/ (* (neg eh) (tan t)) ew)))) (* (* eh (sin t)) (sin (atan (/ (* (neg eh) (tan t)) ew))))) (* (/ 1 (sqrt (+ 1 (pow (neg (* (/ eh ew) (tan t))) 2)))) ew) (fabs (- (* (* ew (cos t)) (cos (atan (/ (* (neg eh) (tan t)) ew)))) (* (* eh (sin t)) (sin (atan (/ (* (neg eh) (tan t)) ew)))))) (- (* (* ew (cos t)) (cos (atan (/ (* (neg eh) (tan t)) ew)))) (* (* eh (sin t)) (sin (atan (/ (* (neg eh) (tan t)) ew))))) (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (neg (* (/ eh ew) (tan t))) 2))))) (* (cos t) ew) (fabs (- (* (* ew (cos t)) (cos (atan (/ (* (neg eh) (tan t)) ew)))) (* (* eh (sin t)) (sin (atan (/ (* (neg eh) (tan t)) ew)))))) (- (* (* ew (cos t)) (cos (atan (/ (* (neg eh) (tan t)) ew)))) (* (* eh (sin t)) (sin (atan (/ (* (neg eh) (tan t)) ew))))) (* (* ew (cos t)) (cos (atan (/ (* (neg eh) (tan t)) ew)))) (* ew (cos t)) (cos (atan (/ (* (neg eh) (tan t)) ew))) (atan (/ (* (neg eh) (tan t)) ew)) (/ (* (neg eh) (tan t)) ew) (* (neg eh) (tan t)) (neg eh) (* (* eh (sin t)) (sin (atan (/ (* (neg eh) (tan t)) ew)))) (* (* eh t) (tanh (asinh (neg (* (/ eh ew) (tan t)))))) (* eh t) (fabs (/ (- (pow (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) 3) (pow (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew))))) 3)) (+ (pow (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) 2) (+ (pow (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew))))) 2) (* (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew)))))))))) (/ (- (pow (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) 3) (pow (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew))))) 3)) (+ (pow (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) 2) (+ (pow (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew))))) 2) (* (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew))))))))) (- (pow (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) 3) (pow (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew))))) 3)) (pow (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) 3) (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2)))) (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))) (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2)) (pow (* (neg eh) (/ (tan t) ew)) 2) (* (neg eh) (/ (tan t) ew)) (/ (tan t) ew) 3 (pow (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew))))) 3) (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew))))) (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew)))) (asinh (* (neg eh) (/ (tan t) ew))) (+ (pow (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) 2) (+ (pow (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew))))) 2) (* (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew)))))))) (pow (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) 2) (+ (pow (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew))))) 2) (* (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew))))))) (pow (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew))))) 2) (* (* (* (cos t) ew) (/ 1 (sqrt (+ 1 (pow (* (neg eh) (/ (tan t) ew)) 2))))) (* (* (sin t) eh) (tanh (asinh (* (neg eh) (/ (tan t) ew))))))) |
155 calls:
| 3.8s | phi2 |
| 2.5s | lambda1 |
| 2.5s | phi1 |
| 1.8s | lambda2 |
| 1.3s | (-.f64 lambda1 lambda2) |
Compiled 15 082 to 14 535 computations (3.6% saved)
Compiled 4 632 479 to 526 679 computations (88.6% saved)
Compiled 627 787 to 391 689 computations (37.6% saved)
| 53× | search |
| Probability | Valid | Unknown | Precondition | Infinite | Domain | Can't | Iter |
|---|---|---|---|---|---|---|---|
| 0% | 0% | 79.4% | 20.6% | 0% | 0% | 0% | 0 |
| 17.2% | 13.7% | 65.7% | 20.6% | 0% | 0% | 0% | 1 |
| 25% | 19.6% | 58.5% | 20.6% | 0% | 1.3% | 0% | 2 |
| 35.2% | 26.6% | 48.9% | 20.6% | 0% | 3.8% | 0% | 3 |
| 42.3% | 31.7% | 43.1% | 20.6% | 0% | 4.5% | 0% | 4 |
| 47.9% | 35.6% | 38.7% | 20.6% | 0% | 5.1% | 0% | 5 |
| 51% | 37.6% | 36.1% | 20.6% | 0% | 5.7% | 0% | 6 |
| 54.4% | 39.7% | 33.2% | 20.6% | 0% | 6.5% | 0% | 7 |
| 56.2% | 40.7% | 31.8% | 20.6% | 0% | 6.8% | 0% | 8 |
| 59% | 42.5% | 29.5% | 20.6% | 0% | 7.4% | 0% | 9 |
| 60.3% | 43.2% | 28.4% | 20.6% | 0% | 7.7% | 0% | 10 |
| 62.1% | 44.3% | 27% | 20.6% | 0% | 8.1% | 0% | 11 |
| 63.6% | 45.1% | 25.8% | 20.6% | 0% | 8.5% | 0% | 12 |
Compiled 1 826 to 963 computations (47.3% saved)
| 39× | fuel |
| 13× | done |
Compiled 11 832 to 5 979 computations (49.5% saved)
| 335× | binary-search |
| 80× | left-value |
| 329× | narrow-enough |
| 6× | predicate-same |
| 5.8s | 8 493× | 1 | valid |
| 1.9s | 1 125× | 5 | exit |
| 1.7s | 13 077× | 0 | valid |
| 459.0ms | 680× | 2 | valid |
| 186.0ms | 86× | 3 | valid |
| 61.0ms | 872× | 0 | invalid |
| 0.0ms | 2× | 1 | invalid |
Compiled 206 933 to 156 694 computations (24.3% saved)
ival-cos: 2.0s (21.9% of total)ival-sin: 1.8s (20.2% of total)adjust: 1.1s (11.7% of total)ival-pow: 1.0s (11.3% of total)ival-mult!: 794.0ms (8.8% of total)ival-pow2: 525.0ms (5.8% of total)ival-div!: 301.0ms (3.3% of total)ival-cosu: 275.0ms (3% of total)ival-sub!: 237.0ms (2.6% of total)ival-sinu: 202.0ms (2.2% of total)ival-atan2: 180.0ms (2% of total)ival-sqrt: 179.0ms (2% of total)ival-exp: 138.0ms (1.5% of total)ival-add!: 106.0ms (1.2% of total)ival-acos: 59.0ms (0.7% of total)ival-neg: 49.0ms (0.5% of total)ival-hypot: 27.0ms (0.3% of total)ival-atan: 26.0ms (0.3% of total)ival-log: 18.0ms (0.2% of total)ival-tan: 18.0ms (0.2% of total)ival-asin: 7.0ms (0.1% of total)ival-fabs: 4.0ms (0% of total)ival-log1p: 2.0ms (0% of total)| 51× | node-limit |
| 1× | saturated |
Compiled 138 942 to 77 203 computations (44.4% saved)
Loading profile data...