sympy-ask

suite trig · 2026-10-13 16:39:13 · CAS sympy 1.14.0, mode fork · machine pi5 · dialect sympy · case set 1e4dbd2f7d86

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	no verdict
identities	5	0	5
inverse	4	0	4
periodicity	4	1	3
total	13	1	12

Setup (run once per start, not counted in the per-query times)

measured setup time: 0.406 s

setup — not timed

from sympy import *
import sympy

SympyVersion = sympy.__version__
# warm-up: a fixed generic expression, never case content
W = Symbol('W')
Warmup = ask(Q.positive(W**2 + 1), Q.real(W))
# every query then runs in its own forked process, starting from this state:
# the expression caches are dropped (imported and lazily loaded modules stay)
sympy.core.cache.clear_cache()

sympy	`sympy.__version__`	→	`1.14.0`
warm-up	`ask(Q.positive(W**2 + 1), Q.real(W))`	→	`True`

Cases

case category outcome query (as sent) answer steps (from the trace) s detail

trig-double-01 true identities no verdict Q.complex(z) ⊢ Eq(sin((2*z)), (2*(sin(z)*cos(z)))) null difference → -2*sin(z)*cos(z) + sin(2*z) · ask → None 0.138 null

code

setup — not timed

from sympy import *
import sympy

SympyVersion = sympy.__version__
# warm-up: a fixed generic expression, never case content
W = Symbol('W')
Warmup = ask(Q.positive(W**2 + 1), Q.real(W))
# every query then runs in its own forked process, starting from this state:
# the expression caches are dropped (imported and lazily loaded modules stay)
sympy.core.cache.clear_cache()

z = Symbol('z', complex=True)
Assum = And(Q.complex(z))
Residual = sin(2 * z) - (2 * (sin(z) * cos(z)))
# not Q.eq: in SymPy 1.14 ask(Q.eq(x**2, x), Q.real(x)) is wrongly False
Answer = ask(Q.zero(Residual), Assum)
print(Residual, Answer, sep='\n')

difference	`sin(2 * z) - (2 * (sin(z) * cos(z)))`	→	`-2sin(z)cos(z) + sin(2*z)`
ask	`Q.zero(Residual)`	→	`None`
answer			`null`

trig-double-02 false identities no verdict Q.real(x) ∧ Q.positive(x) ∧ (x < 1) ⊢ Eq(sin((2*x)), (2*sin(x))) null difference → -2*sin(x) + sin(2*x) · ask → None 0.089 null

code

setup — not timed

from sympy import *
import sympy

SympyVersion = sympy.__version__
# warm-up: a fixed generic expression, never case content
W = Symbol('W')
Warmup = ask(Q.positive(W**2 + 1), Q.real(W))
# every query then runs in its own forked process, starting from this state:
# the expression caches are dropped (imported and lazily loaded modules stay)
sympy.core.cache.clear_cache()

x = Symbol('x', real=True)
Assum = And(Q.real(x), Q.positive(x), x < 1)
Residual = sin(2 * x) - (2 * sin(x))
# not Q.eq: in SymPy 1.14 ask(Q.eq(x**2, x), Q.real(x)) is wrongly False
Answer = ask(Q.zero(Residual), Assum)
print(Residual, Answer, sep='\n')

difference	`sin(2 * x) - (2 * sin(x))`	→	`-2sin(x) + sin(2x)`
ask	`Q.zero(Residual)`	→	`None`
answer			`null`

trig-pyth-01 true identities no verdict Q.complex(z) ⊢ Eq(((sin(z)*sin(z)) + (cos(z)*cos(z))), 1) null difference → sin(z)**2 + cos(z)**2 - 1 · ask → None 0.088 null

code

setup — not timed

from sympy import *
import sympy

SympyVersion = sympy.__version__
# warm-up: a fixed generic expression, never case content
W = Symbol('W')
Warmup = ask(Q.positive(W**2 + 1), Q.real(W))
# every query then runs in its own forked process, starting from this state:
# the expression caches are dropped (imported and lazily loaded modules stay)
sympy.core.cache.clear_cache()

z = Symbol('z', complex=True)
Assum = And(Q.complex(z))
Residual = sin(z) * sin(z) + cos(z) * cos(z) - 1
# not Q.eq: in SymPy 1.14 ask(Q.eq(x**2, x), Q.real(x)) is wrongly False
Answer = ask(Q.zero(Residual), Assum)
print(Residual, Answer, sep='\n')

difference	`sin(z) * sin(z) + cos(z) * cos(z) - 1`	→	`sin(z)2 + cos(z)2 - 1`
ask	`Q.zero(Residual)`	→	`None`
answer			`null`

trig-sqrt-01 contingent identities no verdict Q.real(x) ⊢ Eq(sqrt((1 - (sin(x)*sin(x)))), cos(x)) null difference → sqrt(1 - sin(x)**2) - cos(x) · ask → None 0.41 null

code

setup — not timed

from sympy import *
import sympy

SympyVersion = sympy.__version__
# warm-up: a fixed generic expression, never case content
W = Symbol('W')
Warmup = ask(Q.positive(W**2 + 1), Q.real(W))
# every query then runs in its own forked process, starting from this state:
# the expression caches are dropped (imported and lazily loaded modules stay)
sympy.core.cache.clear_cache()

x = Symbol('x', real=True)
Assum = And(Q.real(x))
Residual = sqrt(1 - sin(x) * sin(x)) - cos(x)
# not Q.eq: in SymPy 1.14 ask(Q.eq(x**2, x), Q.real(x)) is wrongly False
Answer = ask(Q.zero(Residual), Assum)
print(Residual, Answer, sep='\n')

difference	`sqrt(1 - sin(x) * sin(x)) - cos(x)`	→	`sqrt(1 - sin(x)**2) - cos(x)`
ask	`Q.zero(Residual)`	→	`None`
answer			`null`

trig-tan-01 true identities no verdict Q.real(x) ∧ (~Q.zero(cos(x))) ⊢ Eq(tan(x), (sin(x)/cos(x))) null difference → -sin(x)/cos(x) + tan(x) · ask → None 0.182 null

code

setup — not timed

from sympy import *
import sympy

SympyVersion = sympy.__version__
# warm-up: a fixed generic expression, never case content
W = Symbol('W')
Warmup = ask(Q.positive(W**2 + 1), Q.real(W))
# every query then runs in its own forked process, starting from this state:
# the expression caches are dropped (imported and lazily loaded modules stay)
sympy.core.cache.clear_cache()

x = Symbol('x', real=True)
Assum = And(Q.real(x), ~Q.zero(cos(x)))
Residual = tan(x) - (sin(x) / cos(x))
# not Q.eq: in SymPy 1.14 ask(Q.eq(x**2, x), Q.real(x)) is wrongly False
Answer = ask(Q.zero(Residual), Assum)
print(Residual, Answer, sep='\n')

difference	`tan(x) - (sin(x) / cos(x))`	→	`-sin(x)/cos(x) + tan(x)`
ask	`Q.zero(Residual)`	→	`None`
answer			`null`

trig-acos-01 true inverse no verdict Q.real(x) ∧ Q.positive(x) ∧ (x < 3) ⊢ Eq(acos(cos(x)), x) null difference → -x + acos(cos(x)) · ask → None 0.072 null

code

setup — not timed

from sympy import *
import sympy

SympyVersion = sympy.__version__
# warm-up: a fixed generic expression, never case content
W = Symbol('W')
Warmup = ask(Q.positive(W**2 + 1), Q.real(W))
# every query then runs in its own forked process, starting from this state:
# the expression caches are dropped (imported and lazily loaded modules stay)
sympy.core.cache.clear_cache()

x = Symbol('x', real=True)
Assum = And(Q.real(x), Q.positive(x), x < 3)
Residual = acos(cos(x)) - x
# not Q.eq: in SymPy 1.14 ask(Q.eq(x**2, x), Q.real(x)) is wrongly False
Answer = ask(Q.zero(Residual), Assum)
print(Residual, Answer, sep='\n')

difference	`acos(cos(x)) - x`	→	`-x + acos(cos(x))`
ask	`Q.zero(Residual)`	→	`None`
answer			`null`

trig-asin-01 contingent inverse no verdict Q.real(x) ⊢ Eq(asin(sin(x)), x) null difference → -x + asin(sin(x)) · ask → None 0.136 null

code

setup — not timed

from sympy import *
import sympy

SympyVersion = sympy.__version__
# warm-up: a fixed generic expression, never case content
W = Symbol('W')
Warmup = ask(Q.positive(W**2 + 1), Q.real(W))
# every query then runs in its own forked process, starting from this state:
# the expression caches are dropped (imported and lazily loaded modules stay)
sympy.core.cache.clear_cache()

x = Symbol('x', real=True)
Assum = And(Q.real(x))
Residual = asin(sin(x)) - x
# not Q.eq: in SymPy 1.14 ask(Q.eq(x**2, x), Q.real(x)) is wrongly False
Answer = ask(Q.zero(Residual), Assum)
print(Residual, Answer, sep='\n')

difference	`asin(sin(x)) - x`	→	`-x + asin(sin(x))`
ask	`Q.zero(Residual)`	→	`None`
answer			`null`

trig-asin-02 true inverse no verdict Q.real(x) ∧ (x > (-1)) ∧ (x < 1) ⊢ Eq(asin(sin(x)), x) null difference → -x + asin(sin(x)) · ask → None 0.18 null

code

setup — not timed

from sympy import *
import sympy

SympyVersion = sympy.__version__
# warm-up: a fixed generic expression, never case content
W = Symbol('W')
Warmup = ask(Q.positive(W**2 + 1), Q.real(W))
# every query then runs in its own forked process, starting from this state:
# the expression caches are dropped (imported and lazily loaded modules stay)
sympy.core.cache.clear_cache()

x = Symbol('x', real=True)
Assum = And(Q.real(x), x > -1, x < 1)
Residual = asin(sin(x)) - x
# not Q.eq: in SymPy 1.14 ask(Q.eq(x**2, x), Q.real(x)) is wrongly False
Answer = ask(Q.zero(Residual), Assum)
print(Residual, Answer, sep='\n')

difference	`asin(sin(x)) - x`	→	`-x + asin(sin(x))`
ask	`Q.zero(Residual)`	→	`None`
answer			`null`

trig-atan-01 true inverse no verdict Q.real(x) ∧ (x > (-1)) ∧ (x < 1) ⊢ Eq(atan(tan(x)), x) null difference → -x + atan(tan(x)) · ask → None 0.109 null

code

setup — not timed

from sympy import *
import sympy

SympyVersion = sympy.__version__
# warm-up: a fixed generic expression, never case content
W = Symbol('W')
Warmup = ask(Q.positive(W**2 + 1), Q.real(W))
# every query then runs in its own forked process, starting from this state:
# the expression caches are dropped (imported and lazily loaded modules stay)
sympy.core.cache.clear_cache()

x = Symbol('x', real=True)
Assum = And(Q.real(x), x > -1, x < 1)
Residual = atan(tan(x)) - x
# not Q.eq: in SymPy 1.14 ask(Q.eq(x**2, x), Q.real(x)) is wrongly False
Answer = ask(Q.zero(Residual), Assum)
print(Residual, Answer, sep='\n')

difference	`atan(tan(x)) - x`	→	`-x + atan(tan(x))`
ask	`Q.zero(Residual)`	→	`None`
answer			`null`

trig-period-01 true periodicity solved Q.complex(z) ⊢ Eq(sin((z + (2*pi))), sin(z)) true difference → 0 · ask → True 0.013 true

code

setup — not timed

from sympy import *
import sympy

SympyVersion = sympy.__version__
# warm-up: a fixed generic expression, never case content
W = Symbol('W')
Warmup = ask(Q.positive(W**2 + 1), Q.real(W))
# every query then runs in its own forked process, starting from this state:
# the expression caches are dropped (imported and lazily loaded modules stay)
sympy.core.cache.clear_cache()

z = Symbol('z', complex=True)
Assum = And(Q.complex(z))
Residual = sin(z + 2 * pi) - sin(z)
# not Q.eq: in SymPy 1.14 ask(Q.eq(x**2, x), Q.real(x)) is wrongly False
Answer = ask(Q.zero(Residual), Assum)
print(Residual, Answer, sep='\n')

difference	`sin(z + 2 * pi) - sin(z)`	→	`0`
ask	`Q.zero(Residual)`	→	`True`
answer			`true`

trig-period-02 contingent periodicity no verdict Q.real(x) ⊢ Eq(cos((x + pi)), cos(x)) null difference → -2*cos(x) · ask → None 0.033 null

code

setup — not timed

from sympy import *
import sympy

SympyVersion = sympy.__version__
# warm-up: a fixed generic expression, never case content
W = Symbol('W')
Warmup = ask(Q.positive(W**2 + 1), Q.real(W))
# every query then runs in its own forked process, starting from this state:
# the expression caches are dropped (imported and lazily loaded modules stay)
sympy.core.cache.clear_cache()

x = Symbol('x', real=True)
Assum = And(Q.real(x))
Residual = cos(x + pi) - cos(x)
# not Q.eq: in SymPy 1.14 ask(Q.eq(x**2, x), Q.real(x)) is wrongly False
Answer = ask(Q.zero(Residual), Assum)
print(Residual, Answer, sep='\n')

difference	`cos(x + pi) - cos(x)`	→	`-2*cos(x)`
ask	`Q.zero(Residual)`	→	`None`
answer			`null`

trig-period-03 contingent periodicity no verdict Q.real(x) ∧ Q.positive(x) ⊢ Eq(cos((x + pi)), cos(x)) null difference → -2*cos(x) · ask → None 0.034 null

code

setup — not timed

from sympy import *
import sympy

SympyVersion = sympy.__version__
# warm-up: a fixed generic expression, never case content
W = Symbol('W')
Warmup = ask(Q.positive(W**2 + 1), Q.real(W))
# every query then runs in its own forked process, starting from this state:
# the expression caches are dropped (imported and lazily loaded modules stay)
sympy.core.cache.clear_cache()

x = Symbol('x', real=True)
Assum = And(Q.real(x), Q.positive(x))
Residual = cos(x + pi) - cos(x)
# not Q.eq: in SymPy 1.14 ask(Q.eq(x**2, x), Q.real(x)) is wrongly False
Answer = ask(Q.zero(Residual), Assum)
print(Residual, Answer, sep='\n')

difference	`cos(x + pi) - cos(x)`	→	`-2*cos(x)`
ask	`Q.zero(Residual)`	→	`None`
answer			`null`

trig-shift-01 contingent periodicity no verdict Q.real(x) ⊢ Eq(sin((x + pi)), sin(x)) null difference → -2*sin(x) · ask → None 0.033 null

code

setup — not timed

from sympy import *
import sympy

SympyVersion = sympy.__version__
# warm-up: a fixed generic expression, never case content
W = Symbol('W')
Warmup = ask(Q.positive(W**2 + 1), Q.real(W))
# every query then runs in its own forked process, starting from this state:
# the expression caches are dropped (imported and lazily loaded modules stay)
sympy.core.cache.clear_cache()

x = Symbol('x', real=True)
Assum = And(Q.real(x))
Residual = sin(x + pi) - sin(x)
# not Q.eq: in SymPy 1.14 ask(Q.eq(x**2, x), Q.real(x)) is wrongly False
Answer = ask(Q.zero(Residual), Assum)
print(Residual, Answer, sep='\n')

difference	`sin(x + pi) - sin(x)`	→	`-2*sin(x)`
ask	`Q.zero(Residual)`	→	`None`
answer			`null`