always-none
suite simplipy · 2026-10-12 21:55:00 · CAS none · machine pi5 · dialect sexp · case set ee702ae2fe06
By category
old report format (graded with a combined score): its nulls are shown as no verdict, because an old report cannot tell a correct decline on a contingent case from no verdict
| category | n | solved | wrong | declined correctly | no verdict | timeout | unsupported |
|---|---|---|---|---|---|---|---|
| simplipy-complex-branch | 80 | 0 | 0 | 0 | 80 | 0 | 0 |
| simplipy-conditional | 92 | 0 | 0 | 0 | 92 | 0 | 0 |
| simplipy-f64-edge | 45 | 0 | 0 | 0 | 45 | 0 | 0 |
| simplipy-ground | 20 | 0 | 0 | 0 | 20 | 0 | 0 |
| simplipy-real | 70 | 0 | 0 | 0 | 70 | 0 | 0 |
| total | 307 | 0 | 0 | 0 | 307 | 0 | 0 |
Setup (run once per start, not counted in the per-query times)
measured setup time: 0.024 s
The system sent no setup code.
Cases
| case | category | outcome | query (as sent) | answer | steps (from the trace) | s | detail |
|---|---|---|---|---|---|---|---|
| sp-acj4-0-complex contingent | simplipy-complex-branch | no verdict | (= (acosh (cosh x)) (abs x)) | null | 0.0 | null | |
| sp-acj4-102-complex true | simplipy-complex-branch | no verdict | (= (/ (abs x) 6) (abs (/ x -6))) | null | 0.0 | null | |
| sp-acj4-108-complex contingent | simplipy-complex-branch | no verdict | (nonzero x) ∧ (nonzero (abs x)) ⊢ (= (/ (abs x) x) (/ x (abs x))) | null | 0.0 | null | |
| sp-acj4-120-complex true | simplipy-complex-branch | no verdict | (nonzero (abs x)) ∧ (nonzero x) ⊢ (= (/ pi (abs x)) (abs (/ pi x))) | null | 0.0 | null | |
| sp-acj4-130-complex contingent | simplipy-complex-branch | no verdict | (nonzero (cos x)) ∧ (nonzero (/ (cos x))) ⊢ (= (abs (log (cos x))) (log (/ (cos x)))) | null | 0.0 | null | |
| sp-acj4-131-complex contingent | simplipy-complex-branch | no verdict | (nonzero (cosh x)) ⊢ (= (abs (log (cosh x))) (log (cosh x))) | null | 0.0 | null | |
| sp-acj4-132-complex contingent | simplipy-complex-branch | no verdict | (nonzero (sin x)) ⊢ (= (abs (log (sin x))) (- (log (sin x)))) | null | 0.0 | null | |
| sp-acj4-133-complex contingent | simplipy-complex-branch | no verdict | (nonzero (cosh x)) ∧ (nonzero (tanh x)) ⊢ (= (abs (log (tanh x))) (- (log (tanh x)))) | null | 0.0 | null | |
| sp-acj4-137-complex contingent | simplipy-complex-branch | no verdict | (or (nonzero x) (> (re pi) 0)) ⊢ (= (abs (pow x pi)) (pow x pi)) | null | 0.0 | null | |
| sp-acj4-147-complex contingent | simplipy-complex-branch | no verdict | (nonzero (cosh (asinh x))) ∧ (nonzero x) ∧ (!= (/ x) i) ∧ (!= (/ x) (- i)) ⊢ (= (abs (tanh (asinh x))) (cos (atan (/ x)))) | null | 0.0 | null | |
| sp-acj4-151-complex contingent | simplipy-complex-branch | no verdict | (= (acos (cos (asin x))) (abs (asin x))) | null | 0.0 | null | |
| sp-acj4-153-complex contingent | simplipy-complex-branch | no verdict | (= (acos (cos (cos x))) (abs (cos x))) | null | 0.0 | null | |
| sp-acj4-154-complex contingent | simplipy-complex-branch | no verdict | (= (acos (cos (sin x))) (abs (sin x))) | null | 0.0 | null | |
| sp-acj4-165-complex contingent | simplipy-complex-branch | no verdict | (!= x i) ∧ (!= x (- i)) ∧ (nonzero x) ∧ (!= (/ x) i) ∧ (!= (/ x) (- i)) ⊢ (= (asin (cos (atan x))) (abs (atan (/ x)))) | null | 0.0 | null | |
| sp-acj4-173-complex contingent | simplipy-complex-branch | no verdict | (nonzero (cosh x)) ⊢ (= (asin (tanh (abs x))) (acos (/ (cosh x)))) | null | 0.0 | null | |
| sp-acj4-176-complex contingent | simplipy-complex-branch | no verdict | (nonzero (cosh x)) ⊢ (= (atan (abs (sinh x))) (acos (/ (cosh x)))) | null | 0.0 | null | |
| sp-acj4-177-complex contingent | simplipy-complex-branch | no verdict | (nonzero (cos x)) ⊢ (= (atan (abs (tan x))) (abs (asin (sin x)))) | null | 0.0 | null | |
| sp-acj4-180-complex contingent | simplipy-complex-branch | no verdict | (!= (sinh (acosh x)) i) ∧ (!= (sinh (acosh x)) (- i)) ∧ (nonzero (cosh (acosh x))) ⊢ (= (atan (sinh (acosh x))) (asin (tanh (acosh x)))) | null | 0.0 | null | |
| sp-acj4-183-complex contingent | simplipy-complex-branch | no verdict | (nonzero x) ∧ (!= (sinh (log x)) i) ∧ (!= (sinh (log x)) (- i)) ∧ (nonzero (cosh (log x))) ⊢ (= (atan (sinh (log x))) (asin (tanh (log x)))) | null | 0.0 | null | |
| sp-acj4-189-complex contingent | simplipy-complex-branch | no verdict | (!= (cos (asin x)) 1) ∧ (!= (cos (asin x)) -1) ∧ (nonzero x) ⊢ (= (atanh (cos (asin x))) (acosh (abs (/ x)))) | null | 0.0 | null | |
| sp-acj4-190-complex contingent | simplipy-complex-branch | no verdict | (!= x i) ∧ (!= x (- i)) ∧ (!= (cos (atan x)) 1) ∧ (!= (cos (atan x)) -1) ∧ (nonzero x) ⊢ (= (atanh (cos (atan x))) (abs (asinh (/ x)))) | null | 0.0 | null | |
| sp-acj4-191-complex contingent | simplipy-complex-branch | no verdict | (!= (sin (acos x)) 1) ∧ (!= (sin (acos x)) -1) ∧ (nonzero x) ⊢ (= (atanh (sin (acos x))) (acosh (abs (/ x)))) | null | 0.0 | null | |
| sp-acj4-20-complex contingent | simplipy-complex-branch | no verdict | (= (sinh (abs x)) (abs (sinh x))) | null | 0.0 | null | |
| sp-acj4-203-complex contingent | simplipy-complex-branch | no verdict | (nonzero x) ∧ (nonzero (/ x)) ⊢ (= (cos (log (/ x))) (cos (log x))) | null | 0.0 | null | |
| sp-acj4-213-complex true | simplipy-complex-branch | no verdict | (nonzero x) ∧ (nonzero (/ -10 x)) ⊢ (= (/ (/ -10 x)) (/ x -10)) | null | 0.0 | null | |
| sp-acj4-216-complex true | simplipy-complex-branch | no verdict | (nonzero x) ∧ (nonzero (/ -4 x)) ⊢ (= (/ (/ -4 x)) (/ x -4)) | null | 0.0 | null | |
| sp-acj4-22-complex contingent | simplipy-complex-branch | no verdict | (nonzero (cosh x)) ⊢ (= (tanh (abs x)) (abs (tanh x))) | null | 0.0 | null | |
| sp-acj4-234-complex contingent | simplipy-complex-branch | no verdict | (or (nonzero x) (> (re x) 0)) ∧ (nonzero (pow x x)) ∧ (nonzero x) ∧ (or (nonzero (/ x)) (> (re x) 0)) ⊢ (= (/ (pow x x)) (pow (/ x) x)) | null | 0.0 | null | |
| sp-acj4-252-complex contingent | simplipy-complex-branch | no verdict | (= (- (abs (sinh x))) (sinh (- (abs x)))) | null | 0.0 | null | |
| sp-acj4-253-complex contingent | simplipy-complex-branch | no verdict | (nonzero (cosh x)) ⊢ (= (- (abs (tanh x))) (tanh (- (abs x)))) | null | 0.0 | null | |
| sp-acj4-260-complex contingent | simplipy-complex-branch | no verdict | (nonzero (cos x)) ∧ (nonzero (/ (cos x))) ⊢ (= (- (log (cos x))) (log (/ (cos x)))) | null | 0.0 | null | |
| sp-acj4-261-complex contingent | simplipy-complex-branch | no verdict | (nonzero (cosh x)) ∧ (nonzero (/ (cosh x))) ⊢ (= (- (log (cosh x))) (log (/ (cosh x)))) | null | 0.0 | null | |
| sp-acj4-266-complex contingent | simplipy-complex-branch | no verdict | (nonzero x) ∧ (nonzero (/ x)) ⊢ (= (- (sin (log x))) (sin (log (/ x)))) | null | 0.0 | null | |
| sp-acj4-267-complex contingent | simplipy-complex-branch | no verdict | (nonzero x) ∧ (nonzero (cos (log x))) ∧ (nonzero (/ x)) ∧ (nonzero (cos (log (/ x)))) ⊢ (= (- (tan (log x))) (tan (log (/ x)))) | null | 0.0 | null | |
| sp-acj4-274-complex contingent | simplipy-complex-branch | no verdict | (nonzero (abs x)) ∧ (nonzero x) ⊢ (= (pow (abs x) -2) (pow x -2)) | null | 0.0 | null | |
| sp-acj4-278-complex contingent | simplipy-complex-branch | no verdict | (nonzero (abs x)) ∧ (nonzero x) ⊢ (= (pow (abs x) -6) (pow x -6)) | null | 0.0 | null | |
| sp-acj4-283-complex contingent | simplipy-complex-branch | no verdict | (= (pow (abs x) 2) (* x x)) | null | 0.0 | null | |
| sp-acj4-284-complex true | simplipy-complex-branch | no verdict | (= (pow (abs x) 3) (abs (pow x 3))) | null | 0.0 | null | |
| sp-acj4-288-complex true | simplipy-complex-branch | no verdict | (= (pow (abs x) 7) (abs (pow x 7))) | null | 0.0 | null | |
| sp-acj4-30-complex true | simplipy-complex-branch | no verdict | (= (* 4 (abs x)) (abs (* -4 x))) | null | 0.0 | null | |
| sp-acj4-334-complex contingent | simplipy-complex-branch | no verdict | (or (nonzero (exp x)) (> (re (exp 1)) 0)) ⊢ (= (pow (exp x) (exp 1)) (exp (* (exp 1) x))) | null | 0.0 | null | |
| sp-acj4-335-complex contingent | simplipy-complex-branch | no verdict | (or (nonzero (exp x)) (> (re pi) 0)) ⊢ (= (pow (exp x) pi) (exp (* pi x))) | null | 0.0 | null | |
| sp-acj4-336-complex contingent | simplipy-complex-branch | no verdict | (or (nonzero (exp x)) (> (re x) 0)) ⊢ (= (pow (exp x) x) (exp (* x x))) | null | 0.0 | null | |
| sp-acj4-343-complex true | simplipy-complex-branch | no verdict | (= (pow (/ pi) x) (pow pi (- x))) | null | 0.0 | null | |
| sp-acj4-344-complex contingent | simplipy-complex-branch | no verdict | (nonzero x) ∧ (or (nonzero (/ x)) (> (re x) 0)) ∧ (or (nonzero x) (> (re (- x)) 0)) ⊢ (= (pow (/ x) x) (pow x (- x))) | null | 0.0 | null | |
| sp-acj4-368-complex true | simplipy-complex-branch | no verdict | (real (acos x)) ∧ (nonzero (acos x)) ⊢ (= (surd (acos x) -5) (pow (acos x) -1/5)) | null | 0.0 | null | |
| sp-acj4-369-complex true | simplipy-complex-branch | no verdict | (real (acos x)) ⊢ (= (surd (acos x) 5) (pow (acos x) 1/5)) | null | 0.0 | null | |
| sp-acj4-370-complex true | simplipy-complex-branch | no verdict | (real (acosh x)) ∧ (nonzero (acosh x)) ⊢ (= (surd (acosh x) -5) (pow (acosh x) -1/5)) | null | 0.0 | null | |
| sp-acj4-371-complex true | simplipy-complex-branch | no verdict | (real (acosh x)) ⊢ (= (surd (acosh x) 5) (pow (acosh x) 1/5)) | null | 0.0 | null | |
| sp-acj4-372-complex contingent | simplipy-complex-branch | no verdict | (real (cosh x)) ∧ (nonzero (cosh x)) ⊢ (= (surd (cosh x) -5) (pow (cosh x) -1/5)) | null | 0.0 | null | |
| sp-acj4-373-complex contingent | simplipy-complex-branch | no verdict | (real (cosh x)) ⊢ (= (surd (cosh x) 5) (pow (cosh x) 1/5)) | null | 0.0 | null | |
| sp-acj4-387-complex contingent | simplipy-complex-branch | no verdict | (real (exp x)) ⊢ (= (surd (exp x) 5) (exp (/ x 5))) | null | 0.0 | null | |
| sp-acj4-389-complex contingent | simplipy-complex-branch | no verdict | (real (exp x)) ⊢ (= (surd (exp x) 7) (exp (/ x 7))) | null | 0.0 | null | |
| sp-acj4-396-complex contingent | simplipy-complex-branch | no verdict | (= (sin (abs (sin x))) (abs (sin (sin x)))) | null | 0.0 | null | |
| sp-acj4-40-complex true | simplipy-complex-branch | no verdict | (= (* (abs x) pi) (abs (* pi x))) | null | 0.0 | null | |
| sp-acj4-403-complex contingent | simplipy-complex-branch | no verdict | (nonzero x) ∧ (nonzero (/ x)) ⊢ (= (sin (- (log x))) (sin (log (/ x)))) | null | 0.0 | null | |
| sp-acj4-404-complex contingent | simplipy-complex-branch | no verdict | (nonzero (cosh x)) ⊢ (= (sin (tanh (abs x))) (abs (sin (tanh x)))) | null | 0.0 | null | |
| sp-acj4-414-complex contingent | simplipy-complex-branch | no verdict | (nonzero (cos (abs (sin x)))) ∧ (nonzero (cos (sin x))) ⊢ (= (tan (abs (sin x))) (abs (tan (sin x)))) | null | 0.0 | null | |
| sp-acj4-415-complex contingent | simplipy-complex-branch | no verdict | (nonzero (cosh x)) ∧ (nonzero (cos (abs (tanh x)))) ∧ (nonzero (cos (tanh x))) ⊢ (= (tan (abs (tanh x))) (abs (tan (tanh x)))) | null | 0.0 | null | |
| sp-acj4-420-complex contingent | simplipy-complex-branch | no verdict | (nonzero x) ∧ (nonzero (cos (- (log x)))) ∧ (nonzero (/ x)) ∧ (nonzero (cos (log (/ x)))) ⊢ (= (tan (- (log x))) (tan (log (/ x)))) | null | 0.0 | null | |
| sp-acj4-421-complex contingent | simplipy-complex-branch | no verdict | (nonzero (cos (tanh (abs x)))) ∧ (nonzero (cosh x)) ∧ (nonzero (cos (tanh x))) ⊢ (= (tan (tanh (abs x))) (abs (tan (tanh x)))) | null | 0.0 | null | |
| sp-acj4-422-complex contingent | simplipy-complex-branch | no verdict | (nonzero x) ∧ (!= (/ x) i) ∧ (!= (/ x) (- i)) ⊢ (= (tanh (abs (asinh x))) (cos (atan (/ x)))) | null | 0.0 | null | |
| sp-acj4-423-complex contingent | simplipy-complex-branch | no verdict | (nonzero (cosh (acosh (abs x)))) ∧ (nonzero x) ⊢ (= (tanh (acosh (abs x))) (cos (asin (/ x)))) | null | 0.0 | null | |
| sp-acj4-424-complex contingent | simplipy-complex-branch | no verdict | (nonzero x) ∧ (!= (/ x) i) ∧ (!= (/ x) (- i)) ⊢ (= (tanh (asinh (abs x))) (cos (atan (/ x)))) | null | 0.0 | null | |
| sp-acj4-430-complex contingent | simplipy-complex-branch | no verdict | (nonzero x) ∧ (or (nonzero x) (> (re x) 0)) ∧ (nonzero (pow x x)) ⊢ (= (* (log x) x) (log (pow x x))) | null | 0.0 | null | |
| sp-acj4-433-complex contingent | simplipy-complex-branch | no verdict | (nonzero x) ∧ (!= (- (log x)) i) ∧ (!= (- (log x)) (- i)) ∧ (nonzero (/ x)) ∧ (!= (log (/ x)) i) ∧ (!= (log (/ x)) (- i)) ⊢ (= (atan (- (log x))) (atan (log (/ x)))) | null | 0.0 | null | |
| sp-acj4-442-complex contingent | simplipy-complex-branch | no verdict | (nonzero x) ∧ (nonzero (log x)) ∧ (nonzero (/ (log x))) ⊢ (= (- (log (log x))) (log (/ (log x)))) | null | 0.0 | null | |
| sp-acj4-446-complex contingent | simplipy-complex-branch | no verdict | (!= x i) ∧ (!= x (- i)) ∧ (nonzero (cos (abs (atan x)))) ⊢ (= (tan (abs (atan x))) (abs x)) | null | 0.0 | null | |
| sp-acj4-450-complex true | simplipy-complex-branch | no verdict | (nonzero x) ⊢ (= (/ x x) 1) | null | 0.0 | null | |
| sp-acj4-451-complex true | simplipy-complex-branch | no verdict | (nonzero x) ⊢ (= (/ 0 x) 0) | null | 0.0 | null | |
| sp-acj4-50-complex contingent | simplipy-complex-branch | no verdict | (nonzero (pow 6 x)) ⊢ (= (* (log 6) x) (log (pow 6 x))) | null | 0.0 | null | |
| sp-acj4-51-complex contingent | simplipy-complex-branch | no verdict | (nonzero (pow 7 x)) ⊢ (= (* (log 7) x) (log (pow 7 x))) | null | 0.0 | null | |
| sp-acj4-55-complex contingent | simplipy-complex-branch | no verdict | (nonzero x) ∧ (or (nonzero x) (> (re (exp 1)) 0)) ∧ (nonzero (pow x (exp 1))) ⊢ (= (* (log x) (exp 1)) (log (pow x (exp 1)))) | null | 0.0 | null | |
| sp-acj4-56-complex contingent | simplipy-complex-branch | no verdict | (nonzero x) ∧ (or (nonzero x) (> (re pi) 0)) ∧ (nonzero (pow x pi)) ⊢ (= (* (log x) pi) (log (pow x pi))) | null | 0.0 | null | |
| sp-acj4-6-complex contingent | simplipy-complex-branch | no verdict | (nonzero (cosh x)) ∧ (!= (tanh x) 1) ∧ (!= (tanh x) -1) ⊢ (= (atanh (tanh x)) x) | null | 0.0 | null | |
| sp-acj4-7-complex true | simplipy-complex-branch | no verdict | (nonzero (abs x)) ∧ (nonzero x) ⊢ (= (/ (abs x)) (abs (/ x))) | null | 0.0 | null | |
| sp-acj4-9-complex contingent | simplipy-complex-branch | no verdict | (nonzero (exp x)) ⊢ (= (log (exp x)) x) | null | 0.0 | null | |
| sp-acj4-90-complex true | simplipy-complex-branch | no verdict | (nonzero (abs x)) ∧ (nonzero x) ⊢ (= (/ 3 (abs x)) (abs (/ -3 x))) | null | 0.0 | null | |
| sp-acj4-94-complex true | simplipy-complex-branch | no verdict | (nonzero (abs x)) ∧ (nonzero x) ⊢ (= (/ 7 (abs x)) (abs (/ -7 x))) | null | 0.0 | null | |
| sp-acj4-99-complex true | simplipy-complex-branch | no verdict | (= (/ (abs x) 3) (abs (/ x -3))) | null | 0.0 | null | |
| sp-acj4-1-cond true | simplipy-conditional | no verdict | (real x) ∧ (<= (abs x) 1) ⊢ (= (asin (abs x)) (abs (asin x))) | null | 0.0 | null | |
| sp-acj4-108-condf false | simplipy-conditional | no verdict | (imaginary x) ∧ (nonzero x) ∧ (nonzero (abs x)) ⊢ (= (/ (abs x) x) (/ x (abs x))) | null | 0.0 | null | |
| sp-acj4-124-condf contingent | simplipy-conditional | no verdict | (imaginary x) ∧ (nonzero (cosh x)) ⊢ (= (abs (asin (tanh x))) (acos (/ (cosh x)))) | null | 0.0 | null | |
| sp-acj4-127-condf false | simplipy-conditional | no verdict | (>= (re x) 0) ∧ (!= (exp x) 1) ∧ (!= (exp x) -1) ⊢ (= (abs (atanh (exp x))) (atanh (exp x))) | null | 0.0 | null | |
| sp-acj4-128-cond2 true | simplipy-conditional | no verdict | (real x) ∧ (<= (abs x) 1) ⊢ (= (abs (cos (asin x))) (cos (asin x))) | null | 0.0 | null | |
| sp-acj4-128-condf false | simplipy-conditional | no verdict | (real x) ∧ (> x 1) ⊢ (= (abs (cos (asin x))) (cos (asin x))) | null | 0.0 | null | |
| sp-acj4-129-cond contingent | simplipy-conditional | no verdict | (imaginary x) ∧ (!= x i) ∧ (!= x (- i)) ⊢ (= (abs (cos (atan x))) (cos (atan x))) | null | 0.0 | null | |
| sp-acj4-130-cond true | simplipy-conditional | no verdict | (real x) ∧ (< (abs x) (/ pi 2)) ∧ (nonzero (cos x)) ∧ (nonzero (/ (cos x))) ⊢ (= (abs (log (cos x))) (log (/ (cos x)))) | null | 0.0 | null | |
| sp-acj4-131-condf contingent | simplipy-conditional | no verdict | (imaginary x) ∧ (nonzero (cosh x)) ⊢ (= (abs (log (cosh x))) (log (cosh x))) | null | 0.0 | null | |
| sp-acj4-132-cond true | simplipy-conditional | no verdict | (real x) ∧ (>= x 0) ∧ (<= x pi) ∧ (nonzero (sin x)) ⊢ (= (abs (log (sin x))) (- (log (sin x)))) | null | 0.0 | null | |
| sp-acj4-133-condf false | simplipy-conditional | no verdict | (imaginary x) ∧ (nonzero (cosh x)) ∧ (nonzero (tanh x)) ⊢ (= (abs (log (tanh x))) (- (log (tanh x)))) | null | 0.0 | null | |
| sp-acj4-136-cond true | simplipy-conditional | no verdict | (real x) ∧ (nonnegative x) ∧ (or (nonzero x) (> (re (exp 1)) 0)) ⊢ (= (abs (pow x (exp 1))) (pow x (exp 1))) | null | 0.0 | null | |
| sp-acj4-137-cond true | simplipy-conditional | no verdict | (real x) ∧ (nonnegative x) ∧ (or (nonzero x) (> (re pi) 0)) ⊢ (= (abs (pow x pi)) (pow x pi)) | null | 0.0 | null | |
| sp-acj4-145-cond2 true | simplipy-conditional | no verdict | (real x) ∧ (<= (abs x) 1) ⊢ (= (abs (sin (acos x))) (cos (asin x))) | null | 0.0 | null | |
| sp-acj4-145-condf false | simplipy-conditional | no verdict | (real x) ∧ (> x 1) ⊢ (= (abs (sin (acos x))) (cos (asin x))) | null | 0.0 | null | |
| sp-acj4-147-cond contingent | simplipy-conditional | no verdict | (imaginary x) ∧ (nonzero (cosh (asinh x))) ∧ (nonzero x) ∧ (!= (/ x) i) ∧ (!= (/ x) (- i)) ⊢ (= (abs (tanh (asinh x))) (cos (atan (/ x)))) | null | 0.0 | null | |
| sp-acj4-151-cond true | simplipy-conditional | no verdict | (real x) ∧ (<= (abs x) 1) ⊢ (= (acos (cos (asin x))) (abs (asin x))) | null | 0.0 | null | |
| sp-acj4-156-cond true | simplipy-conditional | no verdict | (real x) ∧ (<= (abs x) 1) ⊢ (= (acos (sin (acos x))) (abs (asin x))) | null | 0.0 | null | |
| sp-acj4-159-cond2 true | simplipy-conditional | no verdict | (real x) ∧ (<= x 1) ∧ (nonzero (cosh x)) ⊢ (= (acos (tanh (abs x))) (asin (/ (cosh x)))) | null | 0.0 | null | |
| sp-acj4-159-cond3 true | simplipy-conditional | no verdict | (real x) ∧ (<= (abs x) (/ pi 2)) ∧ (nonzero (cosh x)) ⊢ (= (acos (tanh (abs x))) (asin (/ (cosh x)))) | null | 0.0 | null | |
| sp-acj4-162-cond true | simplipy-conditional | no verdict | (>= (re x) 0) ∧ (real x) ⊢ (= (acosh (surd x 5)) (acosh (pow x 1/5))) | null | 0.0 | null | |
| sp-acj4-162-condf false | simplipy-conditional | no verdict | (real x) ∧ (negative x) ⊢ (= (acosh (surd x 5)) (acosh (pow x 1/5))) | null | 0.0 | null | |
| sp-acj4-171-cond contingent | simplipy-conditional | no verdict | (< (abs (im x)) pi) ∧ (nonzero (cosh x)) ⊢ (= (asin (sin (tanh x))) (tanh x)) | null | 0.0 | null | |
| sp-acj4-171-cond2 true | simplipy-conditional | no verdict | (imaginary x) ∧ (nonzero (cosh x)) ⊢ (= (asin (sin (tanh x))) (tanh x)) | null | 0.0 | null | |
| sp-acj4-179-cond true | simplipy-conditional | no verdict | (real x) ∧ (<= (abs x) (/ pi 2)) ∧ (!= (sinh (acos x)) i) ∧ (!= (sinh (acos x)) (- i)) ∧ (nonzero (cosh (acos x))) ⊢ (= (atan (sinh (acos x))) (asin (tanh (acos x)))) | null | 0.0 | null | |
| sp-acj4-180-cond true | simplipy-conditional | no verdict | (>= (re x) 0) ∧ (!= (sinh (acosh x)) i) ∧ (!= (sinh (acosh x)) (- i)) ∧ (nonzero (cosh (acosh x))) ⊢ (= (atan (sinh (acosh x))) (asin (tanh (acosh x)))) | null | 0.0 | null | |
| sp-acj4-181-cond true | simplipy-conditional | no verdict | (real x) ∧ (<= (abs x) (/ pi 2)) ∧ (!= (sinh (asin x)) i) ∧ (!= (sinh (asin x)) (- i)) ∧ (nonzero (cosh (asin x))) ⊢ (= (atan (sinh (asin x))) (asin (tanh (asin x)))) | null | 0.0 | null | |
| sp-acj4-183-cond true | simplipy-conditional | no verdict | (>= (re x) 0) ∧ (nonzero x) ∧ (!= (sinh (log x)) i) ∧ (!= (sinh (log x)) (- i)) ∧ (nonzero (cosh (log x))) ⊢ (= (atan (sinh (log x))) (asin (tanh (log x)))) | null | 0.0 | null | |
| sp-acj4-186-cond true | simplipy-conditional | no verdict | (imaginary x) ∧ (nonzero (cos (sin x))) ∧ (!= (tan (sin x)) i) ∧ (!= (tan (sin x)) (- i)) ⊢ (= (atan (tan (sin x))) (sin x)) | null | 0.0 | null | |
| sp-acj4-187-cond true | simplipy-conditional | no verdict | (imaginary x) ∧ (nonzero (cosh x)) ∧ (nonzero (cos (tanh x))) ∧ (!= (tan (tanh x)) i) ∧ (!= (tan (tanh x)) (- i)) ⊢ (= (atan (tan (tanh x))) (tanh x)) | null | 0.0 | null | |
| sp-acj4-190-condf false | simplipy-conditional | no verdict | (imaginary x) ∧ (!= x i) ∧ (!= x (- i)) ∧ (!= (cos (atan x)) 1) ∧ (!= (cos (atan x)) -1) ∧ (nonzero x) ⊢ (= (atanh (cos (atan x))) (abs (asinh (/ x)))) | null | 0.0 | null | |
| sp-acj4-191-condf false | simplipy-conditional | no verdict | (imaginary x) ∧ (!= (sin (acos x)) 1) ∧ (!= (sin (acos x)) -1) ∧ (nonzero x) ⊢ (= (atanh (sin (acos x))) (acosh (abs (/ x)))) | null | 0.0 | null | |
| sp-acj4-196-cond2 true | simplipy-conditional | no verdict | (imaginary x) ∧ (nonzero (cosh x)) ∧ (!= (sin (tanh x)) 1) ∧ (!= (sin (tanh x)) -1) ∧ (nonzero (cos (tanh x))) ⊢ (= (atanh (sin (tanh x))) (asinh (tan (tanh x)))) | null | 0.0 | null | |
| sp-acj4-20-condf false | simplipy-conditional | no verdict | (imaginary x) ⊢ (= (sinh (abs x)) (abs (sinh x))) | null | 0.0 | null | |
| sp-acj4-200-cond true | simplipy-conditional | no verdict | (imaginary x) ⊢ (= (cos (asin (sin x))) (abs (cos x))) | null | 0.0 | null | |
| sp-acj4-202-cond true | simplipy-conditional | no verdict | (imaginary x) ∧ (nonzero (cos x)) ∧ (!= (tan x) i) ∧ (!= (tan x) (- i)) ⊢ (= (cos (atan (tan x))) (abs (cos x))) | null | 0.0 | null | |
| sp-acj4-203-cond true | simplipy-conditional | no verdict | (>= (re x) 0) ∧ (nonzero x) ∧ (nonzero (/ x)) ⊢ (= (cos (log (/ x))) (cos (log x))) | null | 0.0 | null | |
| sp-acj4-205-cond true | simplipy-conditional | no verdict | (imaginary x) ∧ (nonzero (cos x)) ⊢ (= (cosh (asinh (tan x))) (abs (/ (cos x)))) | null | 0.0 | null | |
| sp-acj4-234-cond true | simplipy-conditional | no verdict | (>= (re x) 0) ∧ (or (nonzero x) (> (re x) 0)) ∧ (nonzero (pow x x)) ∧ (nonzero x) ∧ (or (nonzero (/ x)) (> (re x) 0)) ⊢ (= (/ (pow x x)) (pow (/ x) x)) | null | 0.0 | null | |
| sp-acj4-234-cond2 true | simplipy-conditional | no verdict | (integer x) ∧ (or (nonzero x) (> (re x) 0)) ∧ (nonzero (pow x x)) ∧ (nonzero x) ∧ (or (nonzero (/ x)) (> (re x) 0)) ⊢ (= (/ (pow x x)) (pow (/ x) x)) | null | 0.0 | null | |
| sp-acj4-243-cond true | simplipy-conditional | no verdict | (> (re x) 0) ∧ (real x) ∧ (nonzero (surd x 5)) ∧ (nonzero x) ⊢ (= (log (surd x 5)) (/ (log x) 5)) | null | 0.0 | null | |
| sp-acj4-245-cond true | simplipy-conditional | no verdict | (> (re x) 0) ∧ (real x) ∧ (nonzero (surd x 7)) ∧ (nonzero x) ⊢ (= (log (surd x 7)) (/ (log x) 7)) | null | 0.0 | null | |
| sp-acj4-248-cond true | simplipy-conditional | no verdict | (real x) ∧ (<= (abs x) 1) ⊢ (= (- (abs (asin x))) (asin (- (abs x)))) | null | 0.0 | null | |
| sp-acj4-251-cond true | simplipy-conditional | no verdict | (real x) ∧ (< (abs x) 1) ∧ (!= x 1) ∧ (!= x -1) ∧ (!= (- (abs x)) 1) ∧ (!= (- (abs x)) -1) ⊢ (= (- (abs (atanh x))) (atanh (- (abs x)))) | null | 0.0 | null | |
| sp-acj4-260-cond true | simplipy-conditional | no verdict | (< (abs (re x)) (/ pi 2)) ∧ (nonzero (cos x)) ∧ (nonzero (/ (cos x))) ⊢ (= (- (log (cos x))) (log (/ (cos x)))) | null | 0.0 | null | |
| sp-acj4-261-cond contingent | simplipy-conditional | no verdict | (> (re x) 0) ∧ (nonzero (cosh x)) ∧ (nonzero (/ (cosh x))) ⊢ (= (- (log (cosh x))) (log (/ (cosh x)))) | null | 0.0 | null | |
| sp-acj4-266-cond true | simplipy-conditional | no verdict | (>= (re x) 0) ∧ (nonzero x) ∧ (nonzero (/ x)) ⊢ (= (- (sin (log x))) (sin (log (/ x)))) | null | 0.0 | null | |
| sp-acj4-266-condf contingent | simplipy-conditional | no verdict | (real x) ∧ (negative x) ∧ (nonzero x) ∧ (nonzero (/ x)) ⊢ (= (- (sin (log x))) (sin (log (/ x)))) | null | 0.0 | null | |
| sp-acj4-267-cond true | simplipy-conditional | no verdict | (>= (re x) 0) ∧ (nonzero x) ∧ (nonzero (cos (log x))) ∧ (nonzero (/ x)) ∧ (nonzero (cos (log (/ x)))) ⊢ (= (- (tan (log x))) (tan (log (/ x)))) | null | 0.0 | null | |
| sp-acj4-267-condf false | simplipy-conditional | no verdict | (real x) ∧ (negative x) ∧ (nonzero x) ∧ (nonzero (cos (log x))) ∧ (nonzero (/ x)) ∧ (nonzero (cos (log (/ x)))) ⊢ (= (- (tan (log x))) (tan (log (/ x)))) | null | 0.0 | null | |
| sp-acj4-283-condf false | simplipy-conditional | no verdict | (imaginary x) ⊢ (= (pow (abs x) 2) (* x x)) | null | 0.0 | null | |
| sp-acj4-287-condf false | simplipy-conditional | no verdict | (imaginary x) ⊢ (= (pow (abs x) 6) (pow x 6)) | null | 0.0 | null | |
| sp-acj4-289-cond true | simplipy-conditional | no verdict | (imaginary x) ⊢ (= (pow (abs x) 8) (pow x 8)) | null | 0.0 | null | |
| sp-acj4-29-cond true | simplipy-conditional | no verdict | (real x) ∧ (positive x) ∧ (nonzero x) ∧ (nonzero (pow x 3)) ⊢ (= (* 3 (log x)) (log (pow x 3))) | null | 0.0 | null | |
| sp-acj4-29-condf false | simplipy-conditional | no verdict | (imaginary x) ∧ (nonzero x) ∧ (nonzero (pow x 3)) ⊢ (= (* 3 (log x)) (log (pow x 3))) | null | 0.0 | null | |
| sp-acj4-334-cond true | simplipy-conditional | no verdict | (and (> (im x) (- pi)) (<= (im x) pi)) ∧ (or (nonzero (exp x)) (> (re (exp 1)) 0)) ⊢ (= (pow (exp x) (exp 1)) (exp (* (exp 1) x))) | null | 0.0 | null | |
| sp-acj4-335-cond true | simplipy-conditional | no verdict | (and (> (im x) (- pi)) (<= (im x) pi)) ∧ (or (nonzero (exp x)) (> (re pi) 0)) ⊢ (= (pow (exp x) pi) (exp (* pi x))) | null | 0.0 | null | |
| sp-acj4-336-cond true | simplipy-conditional | no verdict | (and (> (im x) (- pi)) (<= (im x) pi)) ∧ (or (nonzero (exp x)) (> (re x) 0)) ⊢ (= (pow (exp x) x) (exp (* x x))) | null | 0.0 | null | |
| sp-acj4-344-cond true | simplipy-conditional | no verdict | (>= (re x) 0) ∧ (nonzero x) ∧ (or (nonzero (/ x)) (> (re x) 0)) ∧ (or (nonzero x) (> (re (- x)) 0)) ⊢ (= (pow (/ x) x) (pow x (- x))) | null | 0.0 | null | |
| sp-acj4-344-cond2 true | simplipy-conditional | no verdict | (integer x) ∧ (nonzero x) ∧ (or (nonzero (/ x)) (> (re x) 0)) ∧ (or (nonzero x) (> (re (- x)) 0)) ⊢ (= (pow (/ x) x) (pow x (- x))) | null | 0.0 | null | |
| sp-acj4-372-cond contingent | simplipy-conditional | no verdict | (> (re x) 0) ∧ (real (cosh x)) ∧ (nonzero (cosh x)) ⊢ (= (surd (cosh x) -5) (pow (cosh x) -1/5)) | null | 0.0 | null | |
| sp-acj4-373-cond contingent | simplipy-conditional | no verdict | (> (re x) 0) ∧ (real (cosh x)) ⊢ (= (surd (cosh x) 5) (pow (cosh x) 1/5)) | null | 0.0 | null | |
| sp-acj4-376-cond2 true | simplipy-conditional | no verdict | (< (abs (im x)) pi) ∧ (real (exp x)) ∧ (nonzero (exp x)) ⊢ (= (surd (exp x) -3) (exp (/ x -3))) | null | 0.0 | null | |
| sp-acj4-385-cond contingent | simplipy-conditional | no verdict | (> (re x) 0) ∧ (real (exp x)) ⊢ (= (surd (exp x) 3) (exp (/ x 3))) | null | 0.0 | null | |
| sp-acj4-392-cond true | simplipy-conditional | no verdict | (real x) ∧ (<= (abs x) 1) ⊢ (= (sin (abs (asin x))) (abs (cos (acos x)))) | null | 0.0 | null | |
| sp-acj4-394-cond contingent | simplipy-conditional | no verdict | (real x) ∧ (< (abs x) 1) ∧ (!= x 1) ∧ (!= x -1) ⊢ (= (sin (abs (atanh x))) (abs (sin (atanh x)))) | null | 0.0 | null | |
| sp-acj4-399-cond true | simplipy-conditional | no verdict | (imaginary x) ⊢ (= (sin (acos (sin x))) (abs (cos x))) | null | 0.0 | null | |
| sp-acj4-402-cond contingent | simplipy-conditional | no verdict | (real x) ∧ (< (abs x) 1) ∧ (!= (abs x) 1) ∧ (!= x 1) ∧ (!= x -1) ⊢ (= (sin (atanh (abs x))) (abs (sin (atanh x)))) | null | 0.0 | null | |
| sp-acj4-403-cond true | simplipy-conditional | no verdict | (>= (re x) 0) ∧ (nonzero x) ∧ (nonzero (/ x)) ⊢ (= (sin (- (log x))) (sin (log (/ x)))) | null | 0.0 | null | |
| sp-acj4-403-condf contingent | simplipy-conditional | no verdict | (real x) ∧ (negative x) ∧ (nonzero x) ∧ (nonzero (/ x)) ⊢ (= (sin (- (log x))) (sin (log (/ x)))) | null | 0.0 | null | |
| sp-acj4-412-cond true | simplipy-conditional | no verdict | (real x) ∧ (< (abs x) 1) ∧ (nonzero (cos (abs (asin x)))) ∧ (nonzero (cos (asin x))) ⊢ (= (tan (abs (asin x))) (abs (tan (asin x)))) | null | 0.0 | null | |
| sp-acj4-416-cond true | simplipy-conditional | no verdict | (real x) ∧ (<= (abs x) 1) ∧ (nonzero (cos (acos (abs x)))) ∧ (nonzero (cos (acos x))) ⊢ (= (tan (acos (abs x))) (abs (tan (acos x)))) | null | 0.0 | null | |
| sp-acj4-417-cond true | simplipy-conditional | no verdict | (real x) ∧ (< (abs x) 1) ∧ (nonzero (cos (asin (abs x)))) ∧ (nonzero (cos (asin x))) ⊢ (= (tan (asin (abs x))) (abs (tan (asin x)))) | null | 0.0 | null | |
| sp-acj4-420-cond true | simplipy-conditional | no verdict | (>= (re x) 0) ∧ (nonzero x) ∧ (nonzero (cos (- (log x)))) ∧ (nonzero (/ x)) ∧ (nonzero (cos (log (/ x)))) ⊢ (= (tan (- (log x))) (tan (log (/ x)))) | null | 0.0 | null | |
| sp-acj4-420-condf false | simplipy-conditional | no verdict | (real x) ∧ (negative x) ∧ (nonzero x) ∧ (nonzero (cos (- (log x)))) ∧ (nonzero (/ x)) ∧ (nonzero (cos (log (/ x)))) ⊢ (= (tan (- (log x))) (tan (log (/ x)))) | null | 0.0 | null | |
| sp-acj4-422-condf false | simplipy-conditional | no verdict | (imaginary x) ∧ (nonzero x) ∧ (!= (/ x) i) ∧ (!= (/ x) (- i)) ⊢ (= (tanh (abs (asinh x))) (cos (atan (/ x)))) | null | 0.0 | null | |
| sp-acj4-424-condf false | simplipy-conditional | no verdict | (imaginary x) ∧ (nonzero x) ∧ (!= (/ x) i) ∧ (!= (/ x) (- i)) ⊢ (= (tanh (asinh (abs x))) (cos (atan (/ x)))) | null | 0.0 | null | |
| sp-acj4-428-cond true | simplipy-conditional | no verdict | (real x) ∧ (<= x 1) ⊢ (= (atan (sinh x)) (asin (tanh x))) | null | 0.0 | null | |
| sp-acj4-428-cond3 true | simplipy-conditional | no verdict | (real x) ∧ (>= x 0) ∧ (<= x pi) ⊢ (= (atan (sinh x)) (asin (tanh x))) | null | 0.0 | null | |
| sp-acj4-430-cond true | simplipy-conditional | no verdict | (real x) ∧ (positive x) ∧ (nonzero x) ∧ (or (nonzero x) (> (re x) 0)) ∧ (nonzero (pow x x)) ⊢ (= (* (log x) x) (log (pow x x))) | null | 0.0 | null | |
| sp-acj4-430-cond2 true | simplipy-conditional | no verdict | (real x) ∧ (< (abs x) 1) ∧ (nonzero x) ∧ (or (nonzero x) (> (re x) 0)) ∧ (nonzero (pow x x)) ⊢ (= (* (log x) x) (log (pow x x))) | null | 0.0 | null | |
| sp-acj4-432-cond3 true | simplipy-conditional | no verdict | (real x) ∧ (<= (abs x) (/ pi 2)) ∧ (nonzero (cosh x)) ⊢ (= (acos (abs (tanh x))) (asin (/ (cosh x)))) | null | 0.0 | null | |
| sp-acj4-433-cond true | simplipy-conditional | no verdict | (>= (re x) 0) ∧ (nonzero x) ∧ (!= (- (log x)) i) ∧ (!= (- (log x)) (- i)) ∧ (nonzero (/ x)) ∧ (!= (log (/ x)) i) ∧ (!= (log (/ x)) (- i)) ⊢ (= (atan (- (log x))) (atan (log (/ x)))) | null | 0.0 | null | |
| sp-acj4-433-condf false | simplipy-conditional | no verdict | (real x) ∧ (negative x) ∧ (nonzero x) ∧ (!= (- (log x)) i) ∧ (!= (- (log x)) (- i)) ∧ (nonzero (/ x)) ∧ (!= (log (/ x)) i) ∧ (!= (log (/ x)) (- i)) ⊢ (= (atan (- (log x))) (atan (log (/ x)))) | null | 0.0 | null | |
| sp-acj4-442-cond true | simplipy-conditional | no verdict | (imaginary x) ∧ (nonzero x) ∧ (nonzero (log x)) ∧ (nonzero (/ (log x))) ⊢ (= (- (log (log x))) (log (/ (log x)))) | null | 0.0 | null | |
| sp-acj4-442-cond4 true | simplipy-conditional | no verdict | (integer x) ∧ (nonzero x) ∧ (nonzero (log x)) ∧ (nonzero (/ (log x))) ⊢ (= (- (log (log x))) (log (/ (log x)))) | null | 0.0 | null | |
| sp-acj4-46-cond true | simplipy-conditional | no verdict | (and (> (im x) (- pi)) (<= (im x) pi)) ∧ (nonzero (pow 2 x)) ⊢ (= (* (log 2) x) (log (pow 2 x))) | null | 0.0 | null | |
| sp-acj4-5-cond true | simplipy-conditional | no verdict | (real x) ∧ (< (abs x) 1) ∧ (!= (abs x) 1) ∧ (!= x 1) ∧ (!= x -1) ⊢ (= (atanh (abs x)) (abs (atanh x))) | null | 0.0 | null | |
| sp-acj4-55-cond true | simplipy-conditional | no verdict | (real x) ∧ (positive x) ∧ (nonzero x) ∧ (or (nonzero x) (> (re (exp 1)) 0)) ∧ (nonzero (pow x (exp 1))) ⊢ (= (* (log x) (exp 1)) (log (pow x (exp 1)))) | null | 0.0 | null | |
| sp-acj4-56-cond true | simplipy-conditional | no verdict | (real x) ∧ (positive x) ∧ (nonzero x) ∧ (or (nonzero x) (> (re pi) 0)) ∧ (nonzero (pow x pi)) ⊢ (= (* (log x) pi) (log (pow x pi))) | null | 0.0 | null | |
| sp-acj4-56-condf false | simplipy-conditional | no verdict | (imaginary x) ∧ (nonzero x) ∧ (or (nonzero x) (> (re pi) 0)) ∧ (nonzero (pow x pi)) ⊢ (= (* (log x) pi) (log (pow x pi))) | null | 0.0 | null | |
| sp-acj4-9-cond true | simplipy-conditional | no verdict | (and (> (im x) (- pi)) (<= (im x) pi)) ∧ (nonzero (exp x)) ⊢ (= (log (exp x)) x) | null | 0.0 | null | |
| sp-acj4-0-real true | simplipy-f64-edge | no verdict | (real x) ⊢ (= (acosh (cosh x)) (abs x)) | null | 0.0 | null | |
| sp-acj4-115-real true | simplipy-f64-edge | no verdict | (real x) ∧ (nonzero x) ∧ (> x 0) ∧ (nonzero (surd x -4)) ⊢ (= (/ (log x) -4) (log (surd x -4))) | null | 0.0 | null | |
| sp-acj4-116-real true | simplipy-f64-edge | no verdict | (real x) ∧ (nonzero x) ∧ (> x 0) ∧ (nonzero (surd x -6)) ⊢ (= (/ (log x) -6) (log (surd x -6))) | null | 0.0 | null | |
| sp-acj4-130-real contingent | simplipy-f64-edge | no verdict | (real x) ∧ (nonzero (cos x)) ∧ (nonzero (/ (cos x))) ⊢ (= (abs (log (cos x))) (log (/ (cos x)))) | null | 0.0 | null | |
| sp-acj4-151-real contingent | simplipy-f64-edge | no verdict | (real x) ⊢ (= (acos (cos (asin x))) (abs (asin x))) | null | 0.0 | null | |
| sp-acj4-154-real true | simplipy-f64-edge | no verdict | (real x) ⊢ (= (acos (cos (sin x))) (abs (sin x))) | null | 0.0 | null | |
| sp-acj4-156-real contingent | simplipy-f64-edge | no verdict | (real x) ⊢ (= (acos (sin (acos x))) (abs (asin x))) | null | 0.0 | null | |
| sp-acj4-180-real contingent | simplipy-f64-edge | no verdict | (real x) ∧ (!= (sinh (acosh x)) i) ∧ (!= (sinh (acosh x)) (- i)) ∧ (nonzero (cosh (acosh x))) ⊢ (= (atan (sinh (acosh x))) (asin (tanh (acosh x)))) | null | 0.0 | null | |
| sp-acj4-183-real contingent | simplipy-f64-edge | no verdict | (real x) ∧ (nonzero x) ∧ (!= (sinh (log x)) i) ∧ (!= (sinh (log x)) (- i)) ∧ (nonzero (cosh (log x))) ⊢ (= (atan (sinh (log x))) (asin (tanh (log x)))) | null | 0.0 | null | |
| sp-acj4-189-real true | simplipy-f64-edge | no verdict | (real x) ∧ (!= (cos (asin x)) 1) ∧ (!= (cos (asin x)) -1) ∧ (nonzero x) ⊢ (= (atanh (cos (asin x))) (acosh (abs (/ x)))) | null | 0.0 | null | |
| sp-acj4-190-real true | simplipy-f64-edge | no verdict | (real x) ∧ (!= (cos (atan x)) 1) ∧ (!= (cos (atan x)) -1) ∧ (nonzero x) ⊢ (= (atanh (cos (atan x))) (abs (asinh (/ x)))) | null | 0.0 | null | |
| sp-acj4-191-real true | simplipy-f64-edge | no verdict | (real x) ∧ (!= (sin (acos x)) 1) ∧ (!= (sin (acos x)) -1) ∧ (nonzero x) ⊢ (= (atanh (sin (acos x))) (acosh (abs (/ x)))) | null | 0.0 | null | |
| sp-acj4-203-real contingent | simplipy-f64-edge | no verdict | (real x) ∧ (nonzero x) ∧ (nonzero (/ x)) ⊢ (= (cos (log (/ x))) (cos (log x))) | null | 0.0 | null | |
| sp-acj4-229-real true | simplipy-f64-edge | no verdict | (real x) ∧ (nonzero (pow pi x)) ⊢ (= (/ (pow pi x)) (pow (/ pi) x)) | null | 0.0 | null | |
| sp-acj4-234-real contingent | simplipy-f64-edge | no verdict | (real x) ∧ (or (nonzero x) (> (re x) 0)) ∧ (nonzero (pow x x)) ∧ (nonzero x) ∧ (or (nonzero (/ x)) (> (re x) 0)) ⊢ (= (/ (pow x x)) (pow (/ x) x)) | null | 0.0 | null | |
| sp-acj4-241-real contingent | simplipy-f64-edge | no verdict | (real x) ∧ (nonzero (surd x 3)) ∧ (nonzero x) ⊢ (= (log (surd x 3)) (/ (log x) 3)) | null | 0.0 | null | |
| sp-acj4-247-real contingent | simplipy-f64-edge | no verdict | (real x) ∧ (nonzero (surd x 9)) ∧ (nonzero x) ⊢ (= (log (surd x 9)) (/ (log x) 9)) | null | 0.0 | null | |
| sp-acj4-260-real contingent | simplipy-f64-edge | no verdict | (real x) ∧ (nonzero (cos x)) ∧ (nonzero (/ (cos x))) ⊢ (= (- (log (cos x))) (log (/ (cos x)))) | null | 0.0 | null | |
| sp-acj4-261-real true | simplipy-f64-edge | no verdict | (real x) ∧ (nonzero (cosh x)) ∧ (nonzero (/ (cosh x))) ⊢ (= (- (log (cosh x))) (log (/ (cosh x)))) | null | 0.0 | null | |
| sp-acj4-266-real contingent | simplipy-f64-edge | no verdict | (real x) ∧ (nonzero x) ∧ (nonzero (/ x)) ⊢ (= (- (sin (log x))) (sin (log (/ x)))) | null | 0.0 | null | |
| sp-acj4-267-real contingent | simplipy-f64-edge | no verdict | (real x) ∧ (nonzero x) ∧ (nonzero (cos (log x))) ∧ (nonzero (/ x)) ∧ (nonzero (cos (log (/ x)))) ⊢ (= (- (tan (log x))) (tan (log (/ x)))) | null | 0.0 | null | |
| sp-acj4-29-real contingent | simplipy-f64-edge | no verdict | (real x) ∧ (nonzero x) ∧ (nonzero (pow x 3)) ⊢ (= (* 3 (log x)) (log (pow x 3))) | null | 0.0 | null | |
| sp-acj4-3-real true | simplipy-f64-edge | no verdict | (real x) ⊢ (= (asinh (sinh x)) x) | null | 0.0 | null | |
| sp-acj4-343-real true | simplipy-f64-edge | no verdict | (real x) ⊢ (= (pow (/ pi) x) (pow pi (- x))) | null | 0.0 | null | |
| sp-acj4-344-real contingent | simplipy-f64-edge | no verdict | (real x) ∧ (nonzero x) ∧ (or (nonzero (/ x)) (> (re x) 0)) ∧ (or (nonzero x) (> (re (- x)) 0)) ⊢ (= (pow (/ x) x) (pow x (- x))) | null | 0.0 | null | |
| sp-acj4-378-real true | simplipy-f64-edge | no verdict | (real x) ∧ (nonzero (exp x)) ⊢ (= (surd (exp x) -5) (exp (/ x -5))) | null | 0.0 | null | |
| sp-acj4-380-real true | simplipy-f64-edge | no verdict | (real x) ∧ (nonzero (exp x)) ⊢ (= (surd (exp x) -7) (exp (/ x -7))) | null | 0.0 | null | |
| sp-acj4-392-real contingent | simplipy-f64-edge | no verdict | (real x) ⊢ (= (sin (abs (asin x))) (abs (cos (acos x)))) | null | 0.0 | null | |
| sp-acj4-403-real contingent | simplipy-f64-edge | no verdict | (real x) ∧ (nonzero x) ∧ (nonzero (/ x)) ⊢ (= (sin (- (log x))) (sin (log (/ x)))) | null | 0.0 | null | |
| sp-acj4-410-real true | simplipy-f64-edge | no verdict | (real x) ∧ (nonzero x) ∧ (nonzero (sinh x)) ⊢ (= (sinh (exp (log x))) (exp (log (sinh x)))) | null | 0.0 | null | |
| sp-acj4-416-real contingent | simplipy-f64-edge | no verdict | (real x) ∧ (nonzero (cos (acos (abs x)))) ∧ (nonzero (cos (acos x))) ⊢ (= (tan (acos (abs x))) (abs (tan (acos x)))) | null | 0.0 | null | |
| sp-acj4-420-real contingent | simplipy-f64-edge | no verdict | (real x) ∧ (nonzero x) ∧ (nonzero (cos (- (log x)))) ∧ (nonzero (/ x)) ∧ (nonzero (cos (log (/ x)))) ⊢ (= (tan (- (log x))) (tan (log (/ x)))) | null | 0.0 | null | |
| sp-acj4-430-real contingent | simplipy-f64-edge | no verdict | (real x) ∧ (nonzero x) ∧ (or (nonzero x) (> (re x) 0)) ∧ (nonzero (pow x x)) ⊢ (= (* (log x) x) (log (pow x x))) | null | 0.0 | null | |
| sp-acj4-433-real contingent | simplipy-f64-edge | no verdict | (real x) ∧ (nonzero x) ∧ (!= (- (log x)) i) ∧ (!= (- (log x)) (- i)) ∧ (nonzero (/ x)) ∧ (!= (log (/ x)) i) ∧ (!= (log (/ x)) (- i)) ⊢ (= (atan (- (log x))) (atan (log (/ x)))) | null | 0.0 | null | |
| sp-acj4-442-real contingent | simplipy-f64-edge | no verdict | (real x) ∧ (nonzero x) ∧ (nonzero (log x)) ∧ (nonzero (/ (log x))) ⊢ (= (- (log (log x))) (log (/ (log x)))) | null | 0.0 | null | |
| sp-acj4-449-real true | simplipy-f64-edge | no verdict | (real x) ∧ (nonzero x) ∧ (nonzero (cosh (- (log x)))) ∧ (nonzero (/ x)) ∧ (nonzero (cosh (log (/ x)))) ⊢ (= (tanh (- (log x))) (tanh (log (/ x)))) | null | 0.0 | null | |
| sp-acj4-450-real true | simplipy-f64-edge | no verdict | (real x) ∧ (nonzero x) ⊢ (= (/ x x) 1) | null | 0.0 | null | |
| sp-acj4-451-real true | simplipy-f64-edge | no verdict | (real x) ∧ (nonzero x) ⊢ (= (/ 0 x) 0) | null | 0.0 | null | |
| sp-acj4-50-real true | simplipy-f64-edge | no verdict | (real x) ∧ (nonzero (pow 6 x)) ⊢ (= (* (log 6) x) (log (pow 6 x))) | null | 0.0 | null | |
| sp-acj4-55-real contingent | simplipy-f64-edge | no verdict | (real x) ∧ (nonzero x) ∧ (or (nonzero x) (> (re (exp 1)) 0)) ∧ (nonzero (pow x (exp 1))) ⊢ (= (* (log x) (exp 1)) (log (pow x (exp 1)))) | null | 0.0 | null | |
| sp-acj4-56-real contingent | simplipy-f64-edge | no verdict | (real x) ∧ (nonzero x) ∧ (or (nonzero x) (> (re pi) 0)) ∧ (nonzero (pow x pi)) ⊢ (= (* (log x) pi) (log (pow x pi))) | null | 0.0 | null | |
| sp-acj4-6-real true | simplipy-f64-edge | no verdict | (real x) ∧ (!= (tanh x) 1) ∧ (!= (tanh x) -1) ⊢ (= (atanh (tanh x)) x) | null | 0.0 | null | |
| sp-acj4-806-ground true | simplipy-f64-edge | no verdict | (= (cosh 0) 1) | null | 0.0 | null | |
| sp-acj4-813-ground true | simplipy-f64-edge | no verdict | (= (sinh 0) 0) | null | 0.0 | null | |
| sp-acj4-816-ground true | simplipy-f64-edge | no verdict | (= (tanh 0) 0) | null | 0.0 | null | |
| sp-acj4-1007-ground true | simplipy-ground | no verdict | (= (/ 0 (sin 5)) 0) | null | 0.0 | null | |
| sp-acj4-1107-ground true | simplipy-ground | no verdict | (= (asin (sin (/ 10))) 1/10) | null | 0.0 | null | |
| sp-acj4-1148-ground true | simplipy-ground | no verdict | (= (cosh (log (/ 4))) 17/8) | null | 0.0 | null | |
| sp-acj4-1149-ground true | simplipy-ground | no verdict | (= (exp (abs (log 2))) 2) | null | 0.0 | null | |
| sp-acj4-1177-ground true | simplipy-ground | no verdict | (= (pow 0 (asinh 10)) 0) | null | 0.0 | null | |
| sp-acj4-1195-ground true | simplipy-ground | no verdict | (= (pow 0 (atan 7)) 0) | null | 0.0 | null | |
| sp-acj4-1217-ground true | simplipy-ground | no verdict | (= (pow 0 (exp -1)) 0) | null | 0.0 | null | |
| sp-acj4-1238-ground true | simplipy-ground | no verdict | (= (pow 0 (/ pi)) 0) | null | 0.0 | null | |
| sp-acj4-1247-ground true | simplipy-ground | no verdict | (= (pow 0 (log 9)) 0) | null | 0.0 | null | |
| sp-acj4-1254-ground true | simplipy-ground | no verdict | (= (pow 0 (sin 2)) 0) | null | 0.0 | null | |
| sp-acj4-1258-ground true | simplipy-ground | no verdict | (= (pow 0 (sin 9)) 0) | null | 0.0 | null | |
| sp-acj4-5372-ground true | simplipy-ground | no verdict | (= (sin (asin (/ -4))) -1/4) | null | 0.0 | null | |
| sp-acj4-5382-ground true | simplipy-ground | no verdict | (= (sinh (log (/ 4))) -15/8) | null | 0.0 | null | |
| sp-acj4-5385-ground true | simplipy-ground | no verdict | (= (sinh (- (log 4))) -15/8) | null | 0.0 | null | |
| sp-acj4-819-ground true | simplipy-ground | no verdict | (= (/ 0 pi) 0) | null | 0.0 | null | |
| sp-acj4-837-ground true | simplipy-ground | no verdict | (= (pow 0 pi) 0) | null | 0.0 | null | |
| sp-acj4-848-ground true | simplipy-ground | no verdict | (= (sinh (log 4)) 15/8) | null | 0.0 | null | |
| sp-acj4-868-ground true | simplipy-ground | no verdict | (= (* 0 (acosh 7)) 0) | null | 0.0 | null | |
| sp-acj4-911-ground true | simplipy-ground | no verdict | (= (/ 0 (asin -1)) 0) | null | 0.0 | null | |
| sp-acj4-927-ground true | simplipy-ground | no verdict | (= (/ 0 (asinh 4)) 0) | null | 0.0 | null | |
| sp-acj4-1-real contingent | simplipy-real | no verdict | (real x) ⊢ (= (asin (abs x)) (abs (asin x))) | null | 0.0 | null | |
| sp-acj4-102-real true | simplipy-real | no verdict | (real x) ⊢ (= (/ (abs x) 6) (abs (/ x -6))) | null | 0.0 | null | |
| sp-acj4-108-real true | simplipy-real | no verdict | (real x) ∧ (nonzero x) ∧ (nonzero (abs x)) ⊢ (= (/ (abs x) x) (/ x (abs x))) | null | 0.0 | null | |
| sp-acj4-120-real true | simplipy-real | no verdict | (real x) ∧ (nonzero (abs x)) ∧ (nonzero x) ⊢ (= (/ pi (abs x)) (abs (/ pi x))) | null | 0.0 | null | |
| sp-acj4-127-real contingent | simplipy-real | no verdict | (real x) ∧ (!= (exp x) 1) ∧ (!= (exp x) -1) ⊢ (= (abs (atanh (exp x))) (atanh (exp x))) | null | 0.0 | null | |
| sp-acj4-128-real contingent | simplipy-real | no verdict | (real x) ⊢ (= (abs (cos (asin x))) (cos (asin x))) | null | 0.0 | null | |
| sp-acj4-131-real true | simplipy-real | no verdict | (real x) ∧ (nonzero (cosh x)) ⊢ (= (abs (log (cosh x))) (log (cosh x))) | null | 0.0 | null | |
| sp-acj4-132-real contingent | simplipy-real | no verdict | (real x) ∧ (nonzero (sin x)) ⊢ (= (abs (log (sin x))) (- (log (sin x)))) | null | 0.0 | null | |
| sp-acj4-133-real contingent | simplipy-real | no verdict | (real x) ∧ (nonzero (tanh x)) ⊢ (= (abs (log (tanh x))) (- (log (tanh x)))) | null | 0.0 | null | |
| sp-acj4-136-real contingent | simplipy-real | no verdict | (real x) ∧ (or (nonzero x) (> (re (exp 1)) 0)) ⊢ (= (abs (pow x (exp 1))) (pow x (exp 1))) | null | 0.0 | null | |
| sp-acj4-137-real contingent | simplipy-real | no verdict | (real x) ∧ (or (nonzero x) (> (re pi) 0)) ⊢ (= (abs (pow x pi)) (pow x pi)) | null | 0.0 | null | |
| sp-acj4-14-real true | simplipy-real | no verdict | (real x) ⊢ (= (- (sin x)) (sin (- x))) | null | 0.0 | null | |
| sp-acj4-145-real contingent | simplipy-real | no verdict | (real x) ⊢ (= (abs (sin (acos x))) (cos (asin x))) | null | 0.0 | null | |
| sp-acj4-162-real contingent | simplipy-real | no verdict | (real x) ⊢ (= (acosh (surd x 5)) (acosh (pow x 1/5))) | null | 0.0 | null | |
| sp-acj4-179-real contingent | simplipy-real | no verdict | (real x) ∧ (!= (sinh (acos x)) i) ∧ (!= (sinh (acos x)) (- i)) ∧ (nonzero (cosh (acos x))) ⊢ (= (atan (sinh (acos x))) (asin (tanh (acos x)))) | null | 0.0 | null | |
| sp-acj4-181-real contingent | simplipy-real | no verdict | (real x) ∧ (!= (sinh (asin x)) i) ∧ (!= (sinh (asin x)) (- i)) ∧ (nonzero (cosh (asin x))) ⊢ (= (atan (sinh (asin x))) (asin (tanh (asin x)))) | null | 0.0 | null | |
| sp-acj4-185-real true | simplipy-real | no verdict | (real x) ∧ (nonzero (cos (cos x))) ∧ (!= (tan (cos x)) i) ∧ (!= (tan (cos x)) (- i)) ⊢ (= (atan (tan (cos x))) (cos x)) | null | 0.0 | null | |
| sp-acj4-194-real true | simplipy-real | no verdict | (real x) ∧ (!= (sin (cos x)) 1) ∧ (!= (sin (cos x)) -1) ∧ (nonzero (cos (cos x))) ⊢ (= (atanh (sin (cos x))) (asinh (tan (cos x)))) | null | 0.0 | null | |
| sp-acj4-195-real true | simplipy-real | no verdict | (real x) ∧ (!= (sin (sin x)) 1) ∧ (!= (sin (sin x)) -1) ∧ (nonzero (cos (sin x))) ⊢ (= (atanh (sin (sin x))) (asinh (tan (sin x)))) | null | 0.0 | null | |
| sp-acj4-196-real true | simplipy-real | no verdict | (real x) ∧ (!= (sin (tanh x)) 1) ∧ (!= (sin (tanh x)) -1) ∧ (nonzero (cos (tanh x))) ⊢ (= (atanh (sin (tanh x))) (asinh (tan (tanh x)))) | null | 0.0 | null | |
| sp-acj4-218-real true | simplipy-real | no verdict | (real x) ∧ (nonzero x) ∧ (nonzero (/ -6 x)) ⊢ (= (/ (/ -6 x)) (/ x -6)) | null | 0.0 | null | |
| sp-acj4-22-real true | simplipy-real | no verdict | (real x) ⊢ (= (tanh (abs x)) (abs (tanh x))) | null | 0.0 | null | |
| sp-acj4-220-real true | simplipy-real | no verdict | (real x) ∧ (nonzero x) ∧ (nonzero (/ -8 x)) ⊢ (= (/ (/ -8 x)) (/ x -8)) | null | 0.0 | null | |
| sp-acj4-233-real true | simplipy-real | no verdict | (real x) ∧ (or (nonzero x) (> (re pi) 0)) ∧ (nonzero (pow x pi)) ∧ (or (nonzero x) (> (re (- pi)) 0)) ⊢ (= (/ (pow x pi)) (pow x (- pi))) | null | 0.0 | null | |
| sp-acj4-248-real contingent | simplipy-real | no verdict | (real x) ⊢ (= (- (abs (asin x))) (asin (- (abs x)))) | null | 0.0 | null | |
| sp-acj4-249-real true | simplipy-real | no verdict | (real x) ⊢ (= (- (abs (asinh x))) (asinh (- (abs x)))) | null | 0.0 | null | |
| sp-acj4-251-real contingent | simplipy-real | no verdict | (real x) ∧ (!= x 1) ∧ (!= x -1) ∧ (!= (- (abs x)) 1) ∧ (!= (- (abs x)) -1) ⊢ (= (- (abs (atanh x))) (atanh (- (abs x)))) | null | 0.0 | null | |
| sp-acj4-252-real true | simplipy-real | no verdict | (real x) ⊢ (= (- (abs (sinh x))) (sinh (- (abs x)))) | null | 0.0 | null | |
| sp-acj4-253-real true | simplipy-real | no verdict | (real x) ⊢ (= (- (abs (tanh x))) (tanh (- (abs x)))) | null | 0.0 | null | |
| sp-acj4-256-real true | simplipy-real | no verdict | (real x) ∧ (nonzero (- (exp x))) ⊢ (= (- (exp (- x))) (/ (- (exp x)))) | null | 0.0 | null | |
| sp-acj4-275-real true | simplipy-real | no verdict | (real x) ∧ (nonzero (abs x)) ∧ (nonzero x) ⊢ (= (pow (abs x) -3) (abs (pow x -3))) | null | 0.0 | null | |
| sp-acj4-276-real true | simplipy-real | no verdict | (real x) ∧ (nonzero (abs x)) ∧ (nonzero x) ⊢ (= (pow (abs x) -4) (pow x -4)) | null | 0.0 | null | |
| sp-acj4-283-real true | simplipy-real | no verdict | (real x) ⊢ (= (pow (abs x) 2) (* x x)) | null | 0.0 | null | |
| sp-acj4-286-real true | simplipy-real | no verdict | (real x) ⊢ (= (pow (abs x) 5) (abs (pow x 5))) | null | 0.0 | null | |
| sp-acj4-289-real true | simplipy-real | no verdict | (real x) ⊢ (= (pow (abs x) 8) (pow x 8)) | null | 0.0 | null | |
| sp-acj4-31-real true | simplipy-real | no verdict | (real x) ⊢ (= (* 5 (abs x)) (abs (* -5 x))) | null | 0.0 | null | |
| sp-acj4-326-real true | simplipy-real | no verdict | (real x) ⊢ (= (pow (exp x) 2) (exp (* 2 x))) | null | 0.0 | null | |
| sp-acj4-33-real true | simplipy-real | no verdict | (real x) ⊢ (= (* 6 (abs x)) (abs (* -6 x))) | null | 0.0 | null | |
| sp-acj4-35-real contingent | simplipy-real | no verdict | (real x) ∧ (nonzero x) ∧ (nonzero (pow x 7)) ⊢ (= (* 7 (log x)) (log (pow x 7))) | null | 0.0 | null | |
| sp-acj4-354-real true | simplipy-real | no verdict | (real x) ∧ (or (nonzero x) (> (re (log 5)) 0)) ∧ (nonzero x) ⊢ (= (pow x (log 5)) (pow 5 (log x))) | null | 0.0 | null | |
| sp-acj4-356-real true | simplipy-real | no verdict | (real x) ∧ (or (nonzero x) (> (re (log 7)) 0)) ∧ (nonzero x) ⊢ (= (pow x (log 7)) (pow 7 (log x))) | null | 0.0 | null | |
| sp-acj4-359-real true | simplipy-real | no verdict | (real x) ∧ (or (nonzero x) (> (re (log pi)) 0)) ∧ (nonzero x) ⊢ (= (pow x (log pi)) (pow pi (log x))) | null | 0.0 | null | |
| sp-acj4-364-real true | simplipy-real | no verdict | (real x) ⊢ (= (surd (abs x) 3) (abs (surd x 3))) | null | 0.0 | null | |
| sp-acj4-367-real true | simplipy-real | no verdict | (real x) ⊢ (= (surd (abs x) 9) (abs (surd x 9))) | null | 0.0 | null | |
| sp-acj4-368-real true | simplipy-real | no verdict | (real x) ∧ (real (acos x)) ∧ (nonzero (acos x)) ⊢ (= (surd (acos x) -5) (pow (acos x) -1/5)) | null | 0.0 | null | |
| sp-acj4-369-real true | simplipy-real | no verdict | (real x) ∧ (real (acos x)) ⊢ (= (surd (acos x) 5) (pow (acos x) 1/5)) | null | 0.0 | null | |
| sp-acj4-370-real true | simplipy-real | no verdict | (real x) ∧ (real (acosh x)) ∧ (nonzero (acosh x)) ⊢ (= (surd (acosh x) -5) (pow (acosh x) -1/5)) | null | 0.0 | null | |
| sp-acj4-371-real true | simplipy-real | no verdict | (real x) ∧ (real (acosh x)) ⊢ (= (surd (acosh x) 5) (pow (acosh x) 1/5)) | null | 0.0 | null | |
| sp-acj4-372-real true | simplipy-real | no verdict | (real x) ∧ (nonzero (cosh x)) ⊢ (= (surd (cosh x) -5) (pow (cosh x) -1/5)) | null | 0.0 | null | |
| sp-acj4-373-real true | simplipy-real | no verdict | (real x) ⊢ (= (surd (cosh x) 5) (pow (cosh x) 1/5)) | null | 0.0 | null | |
| sp-acj4-38-real contingent | simplipy-real | no verdict | (real x) ∧ (nonzero x) ∧ (nonzero (pow x 9)) ⊢ (= (* 9 (log x)) (log (pow x 9))) | null | 0.0 | null | |
| sp-acj4-394-real contingent | simplipy-real | no verdict | (real x) ∧ (!= x 1) ∧ (!= x -1) ⊢ (= (sin (abs (atanh x))) (abs (sin (atanh x)))) | null | 0.0 | null | |
| sp-acj4-395-real true | simplipy-real | no verdict | (real x) ⊢ (= (sin (abs (cos x))) (abs (sin (cos x)))) | null | 0.0 | null | |
| sp-acj4-396-real true | simplipy-real | no verdict | (real x) ⊢ (= (sin (abs (sin x))) (abs (sin (sin x)))) | null | 0.0 | null | |
| sp-acj4-397-real true | simplipy-real | no verdict | (real x) ⊢ (= (sin (abs (tanh x))) (abs (sin (tanh x)))) | null | 0.0 | null | |
| sp-acj4-402-real contingent | simplipy-real | no verdict | (real x) ∧ (!= (abs x) 1) ∧ (!= x 1) ∧ (!= x -1) ⊢ (= (sin (atanh (abs x))) (abs (sin (atanh x)))) | null | 0.0 | null | |
| sp-acj4-404-real true | simplipy-real | no verdict | (real x) ⊢ (= (sin (tanh (abs x))) (abs (sin (tanh x)))) | null | 0.0 | null | |
| sp-acj4-412-real contingent | simplipy-real | no verdict | (real x) ∧ (nonzero (cos (abs (asin x)))) ∧ (nonzero (cos (asin x))) ⊢ (= (tan (abs (asin x))) (abs (tan (asin x)))) | null | 0.0 | null | |
| sp-acj4-413-real true | simplipy-real | no verdict | (real x) ∧ (nonzero (cos (abs (cos x)))) ∧ (nonzero (cos (cos x))) ⊢ (= (tan (abs (cos x))) (abs (tan (cos x)))) | null | 0.0 | null | |
| sp-acj4-414-real true | simplipy-real | no verdict | (real x) ∧ (nonzero (cos (abs (sin x)))) ∧ (nonzero (cos (sin x))) ⊢ (= (tan (abs (sin x))) (abs (tan (sin x)))) | null | 0.0 | null | |
| sp-acj4-415-real true | simplipy-real | no verdict | (real x) ∧ (nonzero (cos (abs (tanh x)))) ∧ (nonzero (cos (tanh x))) ⊢ (= (tan (abs (tanh x))) (abs (tan (tanh x)))) | null | 0.0 | null | |
| sp-acj4-417-real contingent | simplipy-real | no verdict | (real x) ∧ (nonzero (cos (asin (abs x)))) ∧ (nonzero (cos (asin x))) ⊢ (= (tan (asin (abs x))) (abs (tan (asin x)))) | null | 0.0 | null | |
| sp-acj4-421-real true | simplipy-real | no verdict | (real x) ∧ (nonzero (cos (tanh (abs x)))) ∧ (nonzero (cos (tanh x))) ⊢ (= (tan (tanh (abs x))) (abs (tan (tanh x)))) | null | 0.0 | null | |
| sp-acj4-5-real contingent | simplipy-real | no verdict | (real x) ∧ (!= (abs x) 1) ∧ (!= x 1) ∧ (!= x -1) ⊢ (= (atanh (abs x)) (abs (atanh x))) | null | 0.0 | null | |
| sp-acj4-73-real true | simplipy-real | no verdict | (real x) ∧ (nonzero (abs x)) ∧ (nonzero (- (abs x))) ⊢ (= (/ -1 (abs x)) (/ (- (abs x)))) | null | 0.0 | null | |
| sp-acj4-80-real true | simplipy-real | no verdict | (real x) ∧ (nonzero (cos x)) ∧ (nonzero (- (cos x))) ⊢ (= (/ -1 (cos x)) (/ (- (cos x)))) | null | 0.0 | null | |
| sp-acj4-83-real true | simplipy-real | no verdict | (real x) ∧ (nonzero x) ∧ (nonzero (log x)) ∧ (nonzero (- (log x))) ⊢ (= (/ -1 (log x)) (/ (- (log x)))) | null | 0.0 | null | |
| sp-acj4-86-real true | simplipy-real | no verdict | (real x) ∧ (nonzero (cos x)) ∧ (nonzero (tan x)) ∧ (nonzero (- (tan x))) ⊢ (= (/ -1 (tan x)) (/ (- (tan x)))) | null | 0.0 | null | |
| sp-acj4-90-real true | simplipy-real | no verdict | (real x) ∧ (nonzero (abs x)) ∧ (nonzero x) ⊢ (= (/ 3 (abs x)) (abs (/ -3 x))) | null | 0.0 | null | |
| sp-acj4-99-real true | simplipy-real | no verdict | (real x) ⊢ (= (/ (abs x) 3) (abs (/ x -3))) | null | 0.0 | null |