sympy-ask

suite examples · 2026-10-13 17:20:46 · CAS sympy 1.14.0, mode fork · machine pi5 · dialect sympy · case set df65d778fc5c

By category

category	n	solved	declined correctly	no verdict
branch-cuts	5	1	1	3
conventions	2	0	0	2
log-exp	2	2	0	0
parity	5	2	1	2
primes	2	0	1	1
radicals	6	2	1	3
sign	5	0	1	4
trig	2	0	0	2
total	29	7	5	17

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

measured setup time: 0.409 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

demo-atan2-01 true branch-cuts no verdict Q.real(x) ∧ Q.real(y) ∧ Q.positive(x) ⊢ Eq(atan2(y, x), atan((y/x))) null difference → -atan(y/x) + atan2(y, x) · ask → None 0.141 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)
y = Symbol('y', real=True)
Assum = And(Q.real(x), Q.real(y), Q.positive(x))
Residual = atan2(y, x) - atan(y / 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	`atan2(y, x) - atan(y / x)`	→	`-atan(y/x) + atan2(y, x)`
ask	`Q.zero(Residual)`	→	`None`
answer			`null`

demo-atan2-02 false branch-cuts no verdict Q.real(x) ∧ Q.real(y) ∧ Q.negative(x) ∧ Q.positive(y) ⊢ Eq(atan2(y, x), atan((y/x))) null difference → -atan(y/x) + atan2(y, x) · ask → None 0.112 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)
y = Symbol('y', real=True)
Assum = And(Q.real(x), Q.real(y), Q.negative(x), Q.positive(y))
Residual = atan2(y, x) - atan(y / 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	`atan2(y, x) - atan(y / x)`	→	`-atan(y/x) + atan2(y, x)`
ask	`Q.zero(Residual)`	→	`None`
answer			`null`

demo-log-01 true branch-cuts no verdict Q.real(x) ∧ Q.real(y) ∧ Q.positive(x) ∧ Q.positive(y) ⊢ Eq(log((x*y)), (log(x) + log(y))) null difference → -log(x) - log(y) + log(x*y) · ask → None 0.148 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)
y = Symbol('y', real=True)
Assum = And(Q.real(x), Q.real(y), Q.positive(x), Q.positive(y))
Residual = log(x * y) - (log(x) + log(y))
# 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	`log(x * y) - (log(x) + log(y))`	→	`-log(x) - log(y) + log(x*y)`
ask	`Q.zero(Residual)`	→	`None`
answer			`null`

demo-log-02 contingent branch-cuts declined correctly Q.complex(z) ∧ Q.complex(w) ∧ (~Q.zero(z)) ∧ (~Q.zero(w)) ⊢ Eq(log((z*w)), (log(z) + log(w))) null difference → -log(w) - log(z) + log(w*z) · ask → None 0.136 null (correct: contingent)

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)
w = Symbol('w', complex=True)
Assum = And(Q.complex(z), Q.complex(w), ~Q.zero(z), ~Q.zero(w))
Residual = log(z * w) - (log(z) + log(w))
# 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	`log(z * w) - (log(z) + log(w))`	→	`-log(w) - log(z) + log(w*z)`
ask	`Q.zero(Residual)`	→	`None`
answer			`null`

demo-log-03 false branch-cuts solved Q.real(x) ∧ Q.negative(x) ⊢ Eq(log(x), log((-x))) false difference → -log(-x) + log(x) · ask → False 0.133 false

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.negative(x))
Residual = log(x) - log(-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	`log(x) - log(-x)`	→	`-log(-x) + log(x)`
ask	`Q.zero(Residual)`	→	`False`
answer			`false`

demo-acot-01 true conventions no verdict Q.real(x) ∧ Q.positive(x) ⊢ Eq(acot(x), atan((1/x))) null difference → acot(x) - atan(1/x) · ask → None 0.078 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 = acot(x) - atan(1 / 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	`acot(x) - atan(1 / x)`	→	`acot(x) - atan(1/x)`
ask	`Q.zero(Residual)`	→	`None`
answer			`null`

demo-heaviside-01 true conventions no verdict Q.real(x) ∧ (~Q.zero(x)) ⊢ Eq((Heaviside(x) + Heaviside((-x))), 1) null difference → Heaviside(-x) + Heaviside(x) - 1 · ask → None 0.048 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(x))
Residual = Heaviside(x) + Heaviside(-x) - 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	`Heaviside(x) + Heaviside(-x) - 1`	→	`Heaviside(-x) + Heaviside(x) - 1`
ask	`Q.zero(Residual)`	→	`None`
answer			`null`

demo-eq-log-01 true log-exp solved Q.real(x) ∧ Q.positive(x) ⊢ Eq(log(exp(x)), x) true difference → 0 · ask → True 0.01 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()

x = Symbol('x', real=True)
Assum = And(Q.real(x), Q.positive(x))
Residual = log(exp(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	`log(exp(x)) - x`	→	`0`
ask	`Q.zero(Residual)`	→	`True`
answer			`true`

demo-eq-pow-01 true log-exp solved Q.integer(n) ⊢ Eq(Pow((-1), (2*n)), 1) true difference → 0 · ask → True 0.009 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()

n = Symbol('n', integer=True)
Assum = And(Q.integer(n))
Residual = Pow(-1, 2 * n) - 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	`Pow(-1, 2 * n) - 1`	→	`0`
ask	`Q.zero(Residual)`	→	`True`
answer			`true`

demo-parity-01 true parity no verdict Q.integer(n) ∧ Q.odd(n) ⊢ Eq(Pow((-1), (n + 1)), 1) null difference → (-1)**(n + 1) - 1 · ask → None 0.049 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()

n = Symbol('n', integer=True)
Assum = And(Q.integer(n), Q.odd(n))
Residual = Pow(-1, n + 1) - 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	`Pow(-1, n + 1) - 1`	→	`(-1)**(n + 1) - 1`
ask	`Q.zero(Residual)`	→	`None`
answer			`null`

demo-parity-02 false parity solved Q.integer(n) ∧ Q.integer(m) ∧ Q.odd(n) ∧ Q.odd(m) ⊢ Eq(Pow((-1), (n*m)), 1) false difference → (-1)**(m*n) - 1 · ask → False 0.037 false

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()

n = Symbol('n', integer=True)
m = Symbol('m', integer=True)
Assum = And(Q.integer(n), Q.integer(m), Q.odd(n), Q.odd(m))
Residual = Pow(-1, n * m) - 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	`Pow(-1, n * m) - 1`	→	`(-1)*(mn) - 1`
ask	`Q.zero(Residual)`	→	`False`
answer			`false`

demo-parity-03 true parity solved Q.integer(n) ⊢ Eq(Pow((-1), (n*(n + 1))), 1) true difference → 0 · ask → True 0.012 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()

n = Symbol('n', integer=True)
Assum = And(Q.integer(n))
Residual = Pow(-1, n * (n + 1)) - 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	`Pow(-1, n * (n + 1)) - 1`	→	`0`
ask	`Q.zero(Residual)`	→	`True`
answer			`true`

demo-parity-04 contingent parity declined correctly Q.integer(n) ∧ Q.even(n) ⊢ Eq(Pow(I, n), 1) null difference → I**n - 1 · ask → None 0.041 null (correct: contingent)

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()

n = Symbol('n', integer=True)
Assum = And(Q.integer(n), Q.even(n))
Residual = Pow(I, n) - 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	`Pow(I, n) - 1`	→	`I**n - 1`
ask	`Q.zero(Residual)`	→	`None`
answer			`null`

demo-parity-05 true parity no verdict Q.integer(n) ∧ Q.integer(m) ∧ Q.odd(n) ∧ Q.odd(m) ⊢ Eq(Pow((-1), (n*m)), (-1)) null difference → (-1)**(m*n) + 1 · ask → None 0.071 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()

n = Symbol('n', integer=True)
m = Symbol('m', integer=True)
Assum = And(Q.integer(n), Q.integer(m), Q.odd(n), Q.odd(m))
Residual = Pow(-1, n * m) - (-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	`Pow(-1, n * m) - (-1)`	→	`(-1)*(mn) + 1`
ask	`Q.zero(Residual)`	→	`None`
answer			`null`

demo-prime-01 true primes no verdict Q.integer(p) ∧ Q.prime(p) ∧ (p > 2) ⊢ Eq(Pow((-1), p), (-1)) null difference → (-1)**p + 1 · ask → None 0.056 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()

p = Symbol('p', integer=True)
Assum = And(Q.integer(p), Q.prime(p), p > 2)
Residual = Pow(-1, p) - (-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	`Pow(-1, p) - (-1)`	→	`(-1)**p + 1`
ask	`Q.zero(Residual)`	→	`None`
answer			`null`

demo-prime-02 contingent primes declined correctly Q.integer(p) ∧ Q.prime(p) ⊢ Eq(Pow((-1), p), (-1)) null difference → (-1)**p + 1 · ask → None 0.046 null (correct: contingent)

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()

p = Symbol('p', integer=True)
Assum = And(Q.integer(p), Q.prime(p))
Residual = Pow(-1, p) - (-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	`Pow(-1, p) - (-1)`	→	`(-1)**p + 1`
ask	`Q.zero(Residual)`	→	`None`
answer			`null`

demo-eq-abs-01 true radicals no verdict Q.real(x) ∧ Q.negative(x) ⊢ Eq(Abs(x), (-x)) null difference → x + Abs(x) · ask → None 0.032 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.negative(x))
Residual = Abs(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	`Abs(x) - (-x)`	→	`x + Abs(x)`
ask	`Q.zero(Residual)`	→	`None`
answer			`null`

demo-eq-abs-02 false radicals solved Q.real(x) ∧ Q.negative(x) ⊢ Eq(Abs(x), x) false difference → -x + Abs(x) · ask → False 0.018 false

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.negative(x))
Residual = Abs(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	`Abs(x) - x`	→	`-x + Abs(x)`
ask	`Q.zero(Residual)`	→	`False`
answer			`false`

demo-eq-sqrt-01 true radicals no verdict Q.real(x) ∧ Q.positive(x) ⊢ Eq(sqrt(Pow(x, 2)), x) null difference → -x + Abs(x) · ask → None 0.048 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 = sqrt(Pow(x, 2)) - 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(Pow(x, 2)) - x`	→	`-x + Abs(x)`
ask	`Q.zero(Residual)`	→	`None`
answer			`null`

demo-eq-sqrt-02 true radicals solved Q.real(x) ⊢ Eq(sqrt(Pow(x, 2)), Abs(x)) true difference → 0 · ask → True 0.009 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()

x = Symbol('x', real=True)
Assum = And(Q.real(x))
Residual = sqrt(Pow(x, 2)) - Abs(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(Pow(x, 2)) - Abs(x)`	→	`0`
ask	`Q.zero(Residual)`	→	`True`
answer			`true`

demo-eq-sqrt-03 contingent radicals declined correctly Q.real(x) ⊢ Eq(sqrt(Pow(x, 2)), x) null difference → -x + Abs(x) · ask → None 0.089 null (correct: contingent)

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(Pow(x, 2)) - 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(Pow(x, 2)) - x`	→	`-x + Abs(x)`
ask	`Q.zero(Residual)`	→	`None`
answer			`null`

demo-eq-sqrt-04 false radicals no verdict Q.real(x) ∧ Q.positive(x) ⊢ Eq((sqrt(Pow(x, 2)) + 1), x) null difference → -x + Abs(x) + 1 · ask → None 0.059 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 = sqrt(Pow(x, 2)) + 1 - 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(Pow(x, 2)) + 1 - x`	→	`-x + Abs(x) + 1`
ask	`Q.zero(Residual)`	→	`None`
answer			`null`

demo-nonzero-01 true sign no verdict Q.complex(z) ∧ Q.imaginary(z) ⊢ Eq(Abs(sign(z)), 1) null difference → Abs(sign(z)) - 1 · ask → None 0.03 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), Q.imaginary(z))
Residual = Abs(sign(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	`Abs(sign(z)) - 1`	→	`Abs(sign(z)) - 1`
ask	`Q.zero(Residual)`	→	`None`
answer			`null`

demo-sign-02 true sign no verdict Q.real(x) ∧ (~Q.zero(x)) ⊢ Eq(sign(Pow(x, 2)), 1) null difference → sign(x**2) - 1 · ask → None 0.029 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(x))
Residual = sign(Pow(x, 2)) - 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	`sign(Pow(x, 2)) - 1`	→	`sign(x**2) - 1`
ask	`Q.zero(Residual)`	→	`None`
answer			`null`

demo-sign-03 contingent sign declined correctly Q.complex(x) ∧ (~Q.zero(x)) ⊢ Eq(sign(Pow(x, 2)), 1) null difference → sign(x**2) - 1 · ask → None 0.037 null (correct: contingent)

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', complex=True)
Assum = And(Q.complex(x), ~Q.zero(x))
Residual = sign(Pow(x, 2)) - 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	`sign(Pow(x, 2)) - 1`	→	`sign(x**2) - 1`
ask	`Q.zero(Residual)`	→	`None`
answer			`null`

demo-sign-04 true sign no verdict Q.complex(z) ⊢ Eq(Abs((z*conjugate(z))), (z*conjugate(z))) null difference → -z*conjugate(z) + Abs(z*conjugate(z)) · ask → None 0.144 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 = Abs(z * conjugate(z)) - (z * conjugate(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	`Abs(z * conjugate(z)) - (z * conjugate(z))`	→	`-zconjugate(z) + Abs(zconjugate(z))`
ask	`Q.zero(Residual)`	→	`None`
answer			`null`

demo-sign-05 true sign no verdict Q.real(x) ∧ Q.real(y) ∧ Q.positive(x) ∧ Q.negative(y) ⊢ Eq(Abs((x - y)), (x - y)) null difference → -x + y + Abs(x - y) · ask → None 0.083 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)
y = Symbol('y', real=True)
Assum = And(Q.real(x), Q.real(y), Q.positive(x), Q.negative(y))
Residual = Abs(x - y) - (x - y)
# 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	`Abs(x - y) - (x - y)`	→	`-x + y + Abs(x - y)`
ask	`Q.zero(Residual)`	→	`None`
answer			`null`

demo-eq-trig-01 true trig no verdict Q.complex(x) ⊢ Eq((Pow(sin(x), 2) + Pow(cos(x), 2)), 1) null difference → sin(x)**2 + cos(x)**2 - 1 · ask → None 0.086 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', complex=True)
Assum = And(Q.complex(x))
Residual = Pow(sin(x), 2) + Pow(cos(x), 2) - 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	`Pow(sin(x), 2) + Pow(cos(x), 2) - 1`	→	`sin(x)2 + cos(x)2 - 1`
ask	`Q.zero(Residual)`	→	`None`
answer			`null`

demo-eq-trig-02 true trig no verdict Q.complex(x) ⊢ Eq((2*sin(x)*cos(x)), sin((2*x))) null difference → 2*sin(x)*cos(x) - sin(2*x) · ask → None 0.143 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', complex=True)
Assum = And(Q.complex(x))
Residual = 2 * sin(x) * cos(x) - sin(2 * 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	`2 * sin(x) * cos(x) - sin(2 * x)`	→	`2sin(x)cos(x) - sin(2*x)`
ask	`Q.zero(Residual)`	→	`None`
answer			`null`