always-none
suite trig · 2026-10-13 17:21:03 · CAS none · machine pi5 · dialect sexp · case set 7a1dcfa636ed
By category
| category | n | solved | wrong | declined correctly | no verdict | timeout | unsupported |
|---|---|---|---|---|---|---|---|
| identities | 5 | 0 | 0 | 1 | 4 | 0 | 0 |
| inverse | 4 | 0 | 0 | 1 | 3 | 0 | 0 |
| periodicity | 4 | 0 | 0 | 3 | 1 | 0 | 0 |
| total | 13 | 0 | 0 | 5 | 8 | 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 |
|---|---|---|---|---|---|---|---|
| trig-double-01 true | identities | no verdict | (= (sin (* 2 z)) (* 2 (* (sin z) (cos z)))) | null | 0.0 | null | |
| trig-double-02 false | identities | no verdict | (real x) ∧ (positive x) ∧ (< x 1) ⊢ (= (sin (* 2 x)) (* 2 (sin x))) | null | 0.0 | null | |
| trig-pyth-01 true | identities | no verdict | (= (+ (* (sin z) (sin z)) (* (cos z) (cos z))) 1) | null | 0.0 | null | |
| trig-sqrt-01 contingent | identities | declined correctly | (real x) ⊢ (= (sqrt (- 1 (* (sin x) (sin x)))) (cos x)) | null | 0.0 | null (correct: contingent) | |
| trig-tan-01 true | identities | no verdict | (real x) ∧ (nonzero (cos x)) ⊢ (= (tan x) (/ (sin x) (cos x))) | null | 0.0 | null | |
| trig-acos-01 true | inverse | no verdict | (real x) ∧ (positive x) ∧ (< x 3) ⊢ (= (acos (cos x)) x) | null | 0.0 | null | |
| trig-asin-01 contingent | inverse | declined correctly | (real x) ⊢ (= (asin (sin x)) x) | null | 0.0 | null (correct: contingent) | |
| trig-asin-02 true | inverse | no verdict | (real x) ∧ (> x -1) ∧ (< x 1) ⊢ (= (asin (sin x)) x) | null | 0.0 | null | |
| trig-atan-01 true | inverse | no verdict | (real x) ∧ (> x -1) ∧ (< x 1) ⊢ (= (atan (tan x)) x) | null | 0.0 | null | |
| trig-period-01 true | periodicity | no verdict | (= (sin (+ z (* 2 pi))) (sin z)) | null | 0.0 | null | |
| trig-period-02 contingent | periodicity | declined correctly | (real x) ⊢ (= (cos (+ x pi)) (cos x)) | null | 0.0 | null (correct: contingent) | |
| trig-period-03 contingent | periodicity | declined correctly | (real x) ∧ (positive x) ⊢ (= (cos (+ x pi)) (cos x)) | null | 0.0 | null (correct: contingent) | |
| trig-shift-01 contingent | periodicity | declined correctly | (real x) ⊢ (= (sin (+ x pi)) (sin x)) | null | 0.0 | null (correct: contingent) |