always-none
suite examples · 2026-10-13 17:20:05 · CAS none · machine pi5 · dialect sexp · case set df65d778fc5c
By category
| category | n | solved | wrong | declined correctly | no verdict | timeout | unsupported |
|---|---|---|---|---|---|---|---|
| branch-cuts | 5 | 0 | 0 | 1 | 4 | 0 | 0 |
| conventions | 2 | 0 | 0 | 0 | 2 | 0 | 0 |
| log-exp | 2 | 0 | 0 | 0 | 2 | 0 | 0 |
| parity | 5 | 0 | 0 | 1 | 4 | 0 | 0 |
| primes | 2 | 0 | 0 | 1 | 1 | 0 | 0 |
| radicals | 6 | 0 | 0 | 1 | 5 | 0 | 0 |
| sign | 5 | 0 | 0 | 1 | 4 | 0 | 0 |
| trig | 2 | 0 | 0 | 0 | 2 | 0 | 0 |
| total | 29 | 0 | 0 | 5 | 24 | 0 | 0 |
Setup (run once per start, not counted in the per-query times)
measured setup time: 0.018 s
The system sent no setup code.
Cases
| case | category | outcome | query (as sent) | answer | steps (from the trace) | s | detail |
|---|---|---|---|---|---|---|---|
| demo-atan2-01 true | branch-cuts | no verdict | (real x) ∧ (real y) ∧ (positive x) ⊢ (= (atan2 y x) (atan (/ y x))) | null | 0.0 | null | |
| demo-atan2-02 false | branch-cuts | no verdict | (real x) ∧ (real y) ∧ (negative x) ∧ (positive y) ⊢ (= (atan2 y x) (atan (/ y x))) | null | 0.0 | null | |
| demo-log-01 true | branch-cuts | no verdict | (real x) ∧ (real y) ∧ (positive x) ∧ (positive y) ⊢ (= (log (* x y)) (+ (log x) (log y))) | null | 0.0 | null | |
| demo-log-02 contingent | branch-cuts | declined correctly | (nonzero z) ∧ (nonzero w) ⊢ (= (log (* z w)) (+ (log z) (log w))) | null | 0.0 | null (correct: contingent) | |
| demo-log-03 false | branch-cuts | no verdict | (real x) ∧ (negative x) ⊢ (= (log x) (log (- x))) | null | 0.0 | null | |
| demo-acot-01 true | conventions | no verdict | (real x) ∧ (positive x) ⊢ (= (acot x) (atan (/ 1 x))) | null | 0.0 | null | |
| demo-heaviside-01 true | conventions | no verdict | (real x) ∧ (nonzero x) ⊢ (= (+ (heaviside x) (heaviside (- x))) 1) | null | 0.0 | null | |
| demo-eq-log-01 true | log-exp | no verdict | (real x) ∧ (positive x) ⊢ (= (log (exp x)) x) | null | 0.0 | null | |
| demo-eq-pow-01 true | log-exp | no verdict | (integer n) ⊢ (= (pow -1 (* 2 n)) 1) | null | 0.0 | null | |
| demo-parity-01 true | parity | no verdict | (integer n) ∧ (odd n) ⊢ (= (pow -1 (+ n 1)) 1) | null | 0.0 | null | |
| demo-parity-02 false | parity | no verdict | (integer n) ∧ (integer m) ∧ (odd n) ∧ (odd m) ⊢ (= (pow -1 (* n m)) 1) | null | 0.0 | null | |
| demo-parity-03 true | parity | no verdict | (integer n) ⊢ (= (pow -1 (* n (+ n 1))) 1) | null | 0.0 | null | |
| demo-parity-04 contingent | parity | declined correctly | (integer n) ∧ (even n) ⊢ (= (pow i n) 1) | null | 0.0 | null (correct: contingent) | |
| demo-parity-05 true | parity | no verdict | (integer n) ∧ (integer m) ∧ (odd n) ∧ (odd m) ⊢ (= (pow -1 (* n m)) -1) | null | 0.0 | null | |
| demo-prime-01 true | primes | no verdict | (integer p) ∧ (prime p) ∧ (> p 2) ⊢ (= (pow -1 p) -1) | null | 0.0 | null | |
| demo-prime-02 contingent | primes | declined correctly | (integer p) ∧ (prime p) ⊢ (= (pow -1 p) -1) | null | 0.0 | null (correct: contingent) | |
| demo-eq-abs-01 true | radicals | no verdict | (real x) ∧ (negative x) ⊢ (= (abs x) (- x)) | null | 0.0 | null | |
| demo-eq-abs-02 false | radicals | no verdict | (real x) ∧ (negative x) ⊢ (= (abs x) x) | null | 0.0 | null | |
| demo-eq-sqrt-01 true | radicals | no verdict | (real x) ∧ (positive x) ⊢ (= (sqrt (pow x 2)) x) | null | 0.0 | null | |
| demo-eq-sqrt-02 true | radicals | no verdict | (real x) ⊢ (= (sqrt (pow x 2)) (abs x)) | null | 0.0 | null | |
| demo-eq-sqrt-03 contingent | radicals | declined correctly | (real x) ⊢ (= (sqrt (pow x 2)) x) | null | 0.0 | null (correct: contingent) | |
| demo-eq-sqrt-04 false | radicals | no verdict | (real x) ∧ (positive x) ⊢ (= (+ (sqrt (pow x 2)) 1) x) | null | 0.0 | null | |
| demo-nonzero-01 true | sign | no verdict | (imaginary z) ⊢ (= (abs (sign z)) 1) | null | 0.0 | null | |
| demo-sign-02 true | sign | no verdict | (real x) ∧ (nonzero x) ⊢ (= (sign (pow x 2)) 1) | null | 0.0 | null | |
| demo-sign-03 contingent | sign | declined correctly | (nonzero x) ⊢ (= (sign (pow x 2)) 1) | null | 0.0 | null (correct: contingent) | |
| demo-sign-04 true | sign | no verdict | (= (abs (* z (conj z))) (* z (conj z))) | null | 0.0 | null | |
| demo-sign-05 true | sign | no verdict | (real x) ∧ (real y) ∧ (positive x) ∧ (negative y) ⊢ (= (abs (- x y)) (- x y)) | null | 0.0 | null | |
| demo-eq-trig-01 true | trig | no verdict | (= (+ (pow (sin x) 2) (pow (cos x) 2)) 1) | null | 0.0 | null | |
| demo-eq-trig-02 true | trig | no verdict | (= (* 2 (sin x) (cos x)) (sin (* 2 x))) | null | 0.0 | null |