sympy-refine

suite examples · 2026-10-13 16:38:59 · CAS sympy 1.14.0, mode fork · machine pi5 · dialect sympy · case set 03f5149718d0

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
branch-cuts	5	2	3
conventions	2	0	2
log-exp	2	2	0
parity	5	4	1
primes	2	0	2
radicals	6	4	2
sign	5	2	3
trig	2	0	2
total	29	14	15

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

measured setup time: 0.35 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 = refine(Abs(W), Q.positive(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	`refine(Abs(W), Q.positive(W))`	→	`W`

Cases

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

demo-atan2-01 true branch-cuts solved Q.real(x) ∧ Q.real(y) ∧ Q.positive(x) ⊢ Eq(atan2(y, x), atan((y/x))) true difference → -atan(y/x) + atan2(y, x) · refine → 0 0.043 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 = refine(Abs(W), Q.positive(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)
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`atan2(y, x) - atan(y / x)`	→	`-atan(y/x) + atan2(y, x)`
refine	`refine(Residual, Assum)`	→	`0`
answer			`true`

demo-atan2-02 false branch-cuts solved Q.real(x) ∧ Q.real(y) ∧ Q.negative(x) ∧ Q.positive(y) ⊢ Eq(atan2(y, x), atan((y/x))) false difference → -atan(y/x) + atan2(y, x) · refine → pi 0.046 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 = refine(Abs(W), Q.positive(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)
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`atan2(y, x) - atan(y / x)`	→	`-atan(y/x) + atan2(y, x)`
refine	`refine(Residual, Assum)`	→	`pi`
answer			`false`

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) · refine → -log(x) - log(y) + log(x*y) 0.043 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 = refine(Abs(W), Q.positive(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))
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`log(x * y) - (log(x) + log(y))`	→	`-log(x) - log(y) + log(x*y)`
refine	`refine(Residual, Assum)`	→	`-log(x) - log(y) + log(x*y)`
answer			`null`

demo-log-02 contingent branch-cuts no verdict 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) · refine → -log(w) - log(z) + log(w*z) 0.046 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 = refine(Abs(W), Q.positive(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))
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`log(z * w) - (log(z) + log(w))`	→	`-log(w) - log(z) + log(w*z)`
refine	`refine(Residual, Assum)`	→	`-log(w) - log(z) + log(w*z)`
answer			`null`

demo-log-03 false branch-cuts no verdict Q.real(x) ∧ Q.negative(x) ⊢ Eq(log(x), log((-x))) null difference → -log(-x) + log(x) · refine → -log(-x) + log(x) 0.041 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 = refine(Abs(W), Q.positive(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)
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`log(x) - log(-x)`	→	`-log(-x) + log(x)`
refine	`refine(Residual, Assum)`	→	`-log(-x) + log(x)`
answer			`null`

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) · refine → acot(x) - atan(1/x) 0.038 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 = refine(Abs(W), Q.positive(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)
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`acot(x) - atan(1 / x)`	→	`acot(x) - atan(1/x)`
refine	`refine(Residual, Assum)`	→	`acot(x) - atan(1/x)`
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 · refine → Heaviside(-x) + Heaviside(x) - 1 0.036 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 = refine(Abs(W), Q.positive(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
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`Heaviside(x) + Heaviside(-x) - 1`	→	`Heaviside(-x) + Heaviside(x) - 1`
refine	`refine(Residual, Assum)`	→	`Heaviside(-x) + Heaviside(x) - 1`
answer			`null`

demo-eq-log-01 true log-exp solved Q.real(x) ∧ Q.positive(x) ⊢ Eq(log(exp(x)), x) true difference → 0 · refine → 0 0.034 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 = refine(Abs(W), Q.positive(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
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`log(exp(x)) - x`	→	`0`
refine	`refine(Residual, Assum)`	→	`0`
answer			`true`

demo-eq-pow-01 true log-exp solved Q.integer(n) ⊢ Eq(Pow((-1), (2*n)), 1) true difference → 0 · refine → 0 0.008 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 = refine(Abs(W), Q.positive(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
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`Pow(-1, 2 * n) - 1`	→	`0`
refine	`refine(Residual, Assum)`	→	`0`
answer			`true`

demo-parity-01 true parity solved Q.integer(n) ∧ Q.odd(n) ⊢ Eq(Pow((-1), (n + 1)), 1) true difference → (-1)**(n + 1) - 1 · refine → 0 0.041 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 = refine(Abs(W), Q.positive(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
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`Pow(-1, n + 1) - 1`	→	`(-1)**(n + 1) - 1`
refine	`refine(Residual, Assum)`	→	`0`
answer			`true`

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 · refine → -2 0.051 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 = refine(Abs(W), Q.positive(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
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`Pow(-1, n * m) - 1`	→	`(-1)*(mn) - 1`
refine	`refine(Residual, Assum)`	→	`-2`
answer			`false`

demo-parity-03 true parity solved Q.integer(n) ⊢ Eq(Pow((-1), (n*(n + 1))), 1) true difference → 0 · refine → 0 0.036 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 = refine(Abs(W), Q.positive(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
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`Pow(-1, n * (n + 1)) - 1`	→	`0`
refine	`refine(Residual, Assum)`	→	`0`
answer			`true`

demo-parity-04 contingent parity no verdict Q.integer(n) ∧ Q.even(n) ⊢ Eq(Pow(I, n), 1) null difference → I**n - 1 · refine → I**n - 1 0.037 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 = refine(Abs(W), Q.positive(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
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`Pow(I, n) - 1`	→	`I**n - 1`
refine	`refine(Residual, Assum)`	→	`I**n - 1`
answer			`null`

demo-parity-05 true parity solved Q.integer(n) ∧ Q.integer(m) ∧ Q.odd(n) ∧ Q.odd(m) ⊢ Eq(Pow((-1), (n*m)), (-1)) true difference → (-1)**(m*n) + 1 · refine → 0 0.051 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 = refine(Abs(W), Q.positive(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)
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`Pow(-1, n * m) - (-1)`	→	`(-1)*(mn) + 1`
refine	`refine(Residual, Assum)`	→	`0`
answer			`true`

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 · refine → (-1)**p + 1 0.057 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 = refine(Abs(W), Q.positive(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)
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`Pow(-1, p) - (-1)`	→	`(-1)**p + 1`
refine	`refine(Residual, Assum)`	→	`(-1)**p + 1`
answer			`null`

demo-prime-02 contingent primes no verdict Q.integer(p) ∧ Q.prime(p) ⊢ Eq(Pow((-1), p), (-1)) null difference → (-1)**p + 1 · refine → (-1)**p + 1 0.05 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 = refine(Abs(W), Q.positive(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)
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`Pow(-1, p) - (-1)`	→	`(-1)**p + 1`
refine	`refine(Residual, Assum)`	→	`(-1)**p + 1`
answer			`null`

demo-eq-abs-01 true radicals solved Q.real(x) ∧ Q.negative(x) ⊢ Eq(Abs(x), (-x)) true difference → x + Abs(x) · refine → 0 0.038 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 = refine(Abs(W), Q.positive(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)
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`Abs(x) - (-x)`	→	`x + Abs(x)`
refine	`refine(Residual, Assum)`	→	`0`
answer			`true`

demo-eq-abs-02 false radicals no verdict Q.real(x) ∧ Q.negative(x) ⊢ Eq(Abs(x), x) null difference → -x + Abs(x) · refine → -2*x 0.038 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 = refine(Abs(W), Q.positive(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
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`Abs(x) - x`	→	`-x + Abs(x)`
refine	`refine(Residual, Assum)`	→	`-2*x`
answer			`null`

demo-eq-sqrt-01 true radicals solved Q.real(x) ∧ Q.positive(x) ⊢ Eq(sqrt(Pow(x, 2)), x) true difference → -x + Abs(x) · refine → 0 0.038 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 = refine(Abs(W), Q.positive(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
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`sqrt(Pow(x, 2)) - x`	→	`-x + Abs(x)`
refine	`refine(Residual, Assum)`	→	`0`
answer			`true`

demo-eq-sqrt-02 true radicals solved Q.real(x) ⊢ Eq(sqrt(Pow(x, 2)), Abs(x)) true difference → 0 · refine → 0 0.034 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 = refine(Abs(W), Q.positive(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)
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`sqrt(Pow(x, 2)) - Abs(x)`	→	`0`
refine	`refine(Residual, Assum)`	→	`0`
answer			`true`

demo-eq-sqrt-03 contingent radicals no verdict Q.real(x) ⊢ Eq(sqrt(Pow(x, 2)), x) null difference → -x + Abs(x) · refine → -x + Abs(x) 0.046 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 = refine(Abs(W), Q.positive(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
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`sqrt(Pow(x, 2)) - x`	→	`-x + Abs(x)`
refine	`refine(Residual, Assum)`	→	`-x + Abs(x)`
answer			`null`

demo-eq-sqrt-04 false radicals solved Q.real(x) ∧ Q.positive(x) ⊢ Eq((sqrt(Pow(x, 2)) + 1), x) false difference → -x + Abs(x) + 1 · refine → 1 0.038 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 = refine(Abs(W), Q.positive(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
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`sqrt(Pow(x, 2)) + 1 - x`	→	`-x + Abs(x) + 1`
refine	`refine(Residual, Assum)`	→	`1`
answer			`false`

demo-nonzero-01 true sign no verdict Q.complex(z) ∧ Q.imaginary(z) ⊢ Eq(Abs(sign(z)), 1) null difference → Abs(sign(z)) - 1 · refine → Abs(sign(z)) - 1 0.046 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 = refine(Abs(W), Q.positive(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
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`Abs(sign(z)) - 1`	→	`Abs(sign(z)) - 1`
refine	`refine(Residual, Assum)`	→	`Abs(sign(z)) - 1`
answer			`null`

demo-sign-02 true sign solved Q.real(x) ∧ (~Q.zero(x)) ⊢ Eq(sign(Pow(x, 2)), 1) true difference → sign(x**2) - 1 · refine → 0 0.066 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 = refine(Abs(W), Q.positive(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
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`sign(Pow(x, 2)) - 1`	→	`sign(x**2) - 1`
refine	`refine(Residual, Assum)`	→	`0`
answer			`true`

demo-sign-03 contingent sign no verdict Q.complex(x) ∧ (~Q.zero(x)) ⊢ Eq(sign(Pow(x, 2)), 1) null difference → sign(x**2) - 1 · refine → sign(x**2) - 1 0.079 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 = refine(Abs(W), Q.positive(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
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`sign(Pow(x, 2)) - 1`	→	`sign(x**2) - 1`
refine	`refine(Residual, Assum)`	→	`sign(x**2) - 1`
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)) · refine → -z*conjugate(z) + Abs(z**2) 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 = refine(Abs(W), Q.positive(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))
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`Abs(z * conjugate(z)) - (z * conjugate(z))`	→	`-zconjugate(z) + Abs(zconjugate(z))`
refine	`refine(Residual, Assum)`	→	`-zconjugate(z) + Abs(z*2)`
answer			`null`

demo-sign-05 true sign solved Q.real(x) ∧ Q.real(y) ∧ Q.positive(x) ∧ Q.negative(y) ⊢ Eq(Abs((x - y)), (x - y)) true difference → -x + y + Abs(x - y) · refine → 0 0.065 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 = refine(Abs(W), Q.positive(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)
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`Abs(x - y) - (x - y)`	→	`-x + y + Abs(x - y)`
refine	`refine(Residual, Assum)`	→	`0`
answer			`true`

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 · refine → sin(x)**2 + cos(x)**2 - 1 0.047 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 = refine(Abs(W), Q.positive(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
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`Pow(sin(x), 2) + Pow(cos(x), 2) - 1`	→	`sin(x)2 + cos(x)2 - 1`
refine	`refine(Residual, Assum)`	→	`sin(x)2 + cos(x)2 - 1`
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) · refine → 2*sin(x)*cos(x) - sin(2*x) 0.037 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 = refine(Abs(W), Q.positive(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)
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`2 * sin(x) * cos(x) - sin(2 * x)`	→	`2sin(x)cos(x) - sin(2*x)`
refine	`refine(Residual, Assum)`	→	`2sin(x)cos(x) - sin(2*x)`
answer			`null`