example sympy satask fact

gistfile1.txt

And(Equivalent(Q.zero(x*y), Or(Q.zero(x), Q.zero(y))), Implies(And(Or(Q.imaginary(x), Q.real(x)), Or(Q.imaginary(y), Q.real(y))), Implies(Or(And(Not(Q.imaginary(x)), Q.imaginary(y)), And(Not(Q.imaginary(y)), Q.imaginary(x))), Q.imaginary(x*y))), Implies(And(Q.commutative(x), Q.commutative(y)), Q.commutative(x*y)), Implies(And(Q.integer(x), Q.integer(y)), Equivalent(Q.even(x*y), Or(Q.even(x), Q.even(y)))), Implies(And(Q.integer(x), Q.integer(y)), Q.integer(x*y)), Implies(And(Q.positive(x), Q.positive(y)), Q.positive(x*y)), Implies(And(Q.prime(x), Q.prime(y)), Not(Q.prime(x*y))), Implies(And(Q.rational(x), Q.rational(y)), Q.rational(x*y)), Implies(And(Q.real(x), Q.real(y)), Implies(Or(And(Not(Q.irrational(x)), Q.irrational(y)), And(Not(Q.irrational(y)), Q.irrational(x))), Q.irrational(x*y))), Implies(And(Q.real(x), Q.real(y)), Q.commutative(x*y)), Implies(And(Q.real(x), Q.real(y)), Q.real(x*y)), Implies(Or(And(Not(Q.rational(x)), Q.rational(y)), And(Not(Q.rational(y)), Q.rational(x))), Not(Q.integer(x*y))), Or(Not(Q.algebraic(x)), Q.complex(x)), Or(Not(Q.algebraic(x*y)), Q.complex(x*y)), Or(Not(Q.algebraic(y)), Q.complex(y)), Or(Not(Q.antihermitian(x)), Not(Q.hermitian(x))), Or(Not(Q.antihermitian(x*y)), Not(Q.hermitian(x*y))), Or(Not(Q.antihermitian(y)), Not(Q.hermitian(y))), Or(Not(Q.composite(x)), Not(Q.prime(x))), Or(Not(Q.composite(x*y)), Not(Q.prime(x*y))), Or(Not(Q.composite(y)), Not(Q.prime(y))), Or(Not(Q.diagonal(x)), Q.lower_triangular(x)), Or(Not(Q.diagonal(x)), Q.normal(x)), Or(Not(Q.diagonal(x)), Q.symmetric(x)), Or(Not(Q.diagonal(x)), Q.upper_triangular(x)), Or(Not(Q.diagonal(x*y)), Q.lower_triangular(x*y)), Or(Not(Q.diagonal(x*y)), Q.normal(x*y)), Or(Not(Q.diagonal(x*y)), Q.symmetric(x*y)), Or(Not(Q.diagonal(x*y)), Q.upper_triangular(x*y)), Or(Not(Q.diagonal(y)), Q.lower_triangular(y)), Or(Not(Q.diagonal(y)), Q.normal(y)), Or(Not(Q.diagonal(y)), Q.symmetric(y)), Or(Not(Q.diagonal(y)), Q.upper_triangular(y)), Or(Not(Q.even(x)), Not(Q.odd(x))), Or(Not(Q.even(x)), Q.integer(x)), Or(Not(Q.even(x*y)), Not(Q.odd(x*y))), Or(Not(Q.even(x*y)), Q.integer(x*y)), Or(Not(Q.even(y)), Not(Q.odd(y))), Or(Not(Q.even(y)), Q.integer(y)), Or(Not(Q.extended_real(x)), Q.infinity(x), Q.real(x)), Or(Not(Q.extended_real(x*y)), Q.infinity(x*y), Q.real(x*y)), Or(Not(Q.extended_real(y)), Q.infinity(y), Q.real(y)), Or(Not(Q.fullrank(x)), Not(Q.square(x)), Q.invertible(x)), Or(Not(Q.fullrank(x*y)), Not(Q.square(x*y)), Q.invertible(x*y)), Or(Not(Q.fullrank(y)), Not(Q.square(y)), Q.invertible(y)), Or(Not(Q.imaginary(x)), Not(Q.real(x))), Or(Not(Q.imaginary(x)), Q.antihermitian(x)), Or(Not(Q.imaginary(x)), Q.complex(x)), Or(Not(Q.imaginary(x*y)), Not(Q.real(x*y))), Or(Not(Q.imaginary(x*y)), Q.antihermitian(x*y)), Or(Not(Q.imaginary(x*y)), Q.complex(x*y)), Or(Not(Q.imaginary(y)), Not(Q.real(y))), Or(Not(Q.imaginary(y)), Q.antihermitian(y)), Or(Not(Q.imaginary(y)), Q.complex(y)), Or(Not(Q.infinity(x)), Q.extended_real(x)), Or(Not(Q.infinity(x*y)), Q.extended_real(x*y)), Or(Not(Q.infinity(y)), Q.extended_real(y)), Or(Not(Q.integer(x)), Not(Q.positive(x)), Q.composite(x), Q.prime(x)), Or(Not(Q.integer(x)), Q.even(x), Q.odd(x)), Or(Not(Q.integer(x)), Q.rational(x)), Or(Not(Q.integer(x*y)), Not(Q.positive(x*y)), Q.composite(x*y), Q.prime(x*y)), Or(Not(Q.integer(x*y)), Q.even(x*y), Q.odd(x*y)), Or(Not(Q.integer(x*y)), Q.rational(x*y)), Or(Not(Q.integer(y)), Not(Q.positive(y)), Q.composite(y), Q.prime(y)), Or(Not(Q.integer(y)), Q.even(y), Q.odd(y)), Or(Not(Q.integer(y)), Q.rational(y)), Or(Not(Q.integer_elements(x)), Q.real_elements(x)), Or(Not(Q.integer_elements(x*y)), Q.real_elements(x*y)), Or(Not(Q.integer_elements(y)), Q.real_elements(y)), Or(Not(Q.invertible(x)), Not(Q.singular(x))), Or(Not(Q.invertible(x)), Q.fullrank(x)), Or(Not(Q.invertible(x)), Q.square(x)), Or(Not(Q.invertible(x*y)), Not(Q.singular(x*y))), Or(Not(Q.invertible(x*y)), Q.fullrank(x*y)), Or(Not(Q.invertible(x*y)), Q.square(x*y)), Or(Not(Q.invertible(y)), Not(Q.singular(y))), Or(Not(Q.invertible(y)), Q.fullrank(y)), Or(Not(Q.invertible(y)), Q.square(y)), Or(Not(Q.irrational(x)), Not(Q.rational(x))), Or(Not(Q.irrational(x)), Q.real(x)), Or(Not(Q.irrational(x*y)), Not(Q.rational(x*y))), Or(Not(Q.irrational(x*y)), Q.real(x*y)), Or(Not(Q.irrational(y)), Not(Q.rational(y))), Or(Not(Q.irrational(y)), Q.real(y)), Or(Not(Q.lower_triangular(x)), Not(Q.upper_triangular(x)), Q.diagonal(x)), Or(Not(Q.lower_triangular(x)), Q.triangular(x)), Or(Not(Q.lower_triangular(x*y)), Not(Q.upper_triangular(x*y)), Q.diagonal(x*y)), Or(Not(Q.lower_triangular(x*y)), Q.triangular(x*y)), Or(Not(Q.lower_triangular(y)), Not(Q.upper_triangular(y)), Q.diagonal(y)), Or(Not(Q.lower_triangular(y)), Q.triangular(y)), Or(Not(Q.negative(x)), Not(Q.nonnegative(x))), Or(Not(Q.negative(x)), Not(Q.positive(x))), Or(Not(Q.negative(x)), Q.nonzero(x)), Or(Not(Q.negative(x*y)), Not(Q.nonnegative(x*y))), Or(Not(Q.negative(x*y)), Not(Q.positive(x*y))), Or(Not(Q.negative(x*y)), Q.nonzero(x*y)), Or(Not(Q.negative(y)), Not(Q.nonnegative(y))), Or(Not(Q.negative(y)), Not(Q.positive(y))), Or(Not(Q.negative(y)), Q.nonzero(y)), Or(Not(Q.nonnegative(x)), Q.real(x)), Or(Not(Q.nonnegative(x*y)), Q.real(x*y)), Or(Not(Q.nonnegative(y)), Q.real(y)), Or(Not(Q.nonpositive(x)), Not(Q.positive(x))), Or(Not(Q.nonpositive(x)), Q.real(x)), Or(Not(Q.nonpositive(x*y)), Not(Q.positive(x*y))), Or(Not(Q.nonpositive(x*y)), Q.real(x*y)), Or(Not(Q.nonpositive(y)), Not(Q.positive(y))), Or(Not(Q.nonpositive(y)), Q.real(y)), Or(Not(Q.nonzero(x)), Not(Q.zero(x))), Or(Not(Q.nonzero(x)), Q.negative(x), Q.positive(x)), Or(Not(Q.nonzero(x)), Q.real(x)), Or(Not(Q.nonzero(x*y)), Not(Q.zero(x*y))), Or(Not(Q.nonzero(x*y)), Q.negative(x*y), Q.positive(x*y)), Or(Not(Q.nonzero(x*y)), Q.real(x*y)), Or(Not(Q.nonzero(y)), Not(Q.zero(y))), Or(Not(Q.nonzero(y)), Q.negative(y), Q.positive(y)), Or(Not(Q.nonzero(y)), Q.real(y)), Or(Not(Q.normal(x)), Q.square(x)), Or(Not(Q.normal(x*y)), Q.square(x*y)), Or(Not(Q.normal(y)), Q.square(y)), Or(Not(Q.odd(x)), Q.integer(x)), Or(Not(Q.odd(x*y)), Q.integer(x*y)), Or(Not(Q.odd(y)), Q.integer(y)), Or(Not(Q.orthogonal(x)), Q.positive_definite(x)), Or(Not(Q.orthogonal(x)), Q.unitary(x)), Or(Not(Q.orthogonal(x*y)), Q.positive_definite(x*y)), Or(Not(Q.orthogonal(x*y)), Q.unitary(x*y)), Or(Not(Q.orthogonal(y)), Q.positive_definite(y)), Or(Not(Q.orthogonal(y)), Q.unitary(y)), Or(Not(Q.positive(x)), Q.nonzero(x)), Or(Not(Q.positive(x*y)), Q.nonzero(x*y)), Or(Not(Q.positive(y)), Q.nonzero(y)), Or(Not(Q.positive_definite(x)), Q.invertible(x)), Or(Not(Q.positive_definite(x*y)), Q.invertible(x*y)), Or(Not(Q.positive_definite(y)), Q.invertible(y)), Or(Not(Q.prime(x)), Q.integer(x)), Or(Not(Q.prime(x)), Q.positive(x)), Or(Not(Q.prime(x*y)), Q.integer(x*y)), Or(Not(Q.prime(x*y)), Q.positive(x*y)), Or(Not(Q.prime(y)), Q.integer(y)), Or(Not(Q.prime(y)), Q.positive(y)), Or(Not(Q.rational(x)), Q.algebraic(x)), Or(Not(Q.rational(x)), Q.real(x)), Or(Not(Q.rational(x*y)), Q.algebraic(x*y)), Or(Not(Q.rational(x*y)), Q.real(x*y)), Or(Not(Q.rational(y)), Q.algebraic(y)), Or(Not(Q.rational(y)), Q.real(y)), Or(Not(Q.real(x)), Not(Q.unitary(x)), Q.orthogonal(x)), Or(Not(Q.real(x)), Q.complex(x)), Or(Not(Q.real(x)), Q.extended_real(x)), Or(Not(Q.real(x)), Q.hermitian(x)), Or(Not(Q.real(x)), Q.irrational(x), Q.rational(x)), Or(Not(Q.real(x)), Q.negative(x), Q.nonnegative(x)), Or(Not(Q.real(x)), Q.nonpositive(x), Q.positive(x)), Or(Not(Q.real(x)), Q.nonzero(x), Q.zero(x)), Or(Not(Q.real(x*y)), Not(Q.unitary(x*y)), Q.orthogonal(x*y)), Or(Not(Q.real(x*y)), Q.complex(x*y)), Or(Not(Q.real(x*y)), Q.extended_real(x*y)), Or(Not(Q.real(x*y)), Q.hermitian(x*y)), Or(Not(Q.real(x*y)), Q.irrational(x*y), Q.rational(x*y)), Or(Not(Q.real(x*y)), Q.negative(x*y), Q.nonnegative(x*y)), Or(Not(Q.real(x*y)), Q.nonpositive(x*y), Q.positive(x*y)), Or(Not(Q.real(x*y)), Q.nonzero(x*y), Q.zero(x*y)), Or(Not(Q.real(y)), Not(Q.unitary(y)), Q.orthogonal(y)), Or(Not(Q.real(y)), Q.complex(y)), Or(Not(Q.real(y)), Q.extended_real(y)), Or(Not(Q.real(y)), Q.hermitian(y)), Or(Not(Q.real(y)), Q.irrational(y), Q.rational(y)), Or(Not(Q.real(y)), Q.negative(y), Q.nonnegative(y)), Or(Not(Q.real(y)), Q.nonpositive(y), Q.positive(y)), Or(Not(Q.real(y)), Q.nonzero(y), Q.zero(y)), Or(Not(Q.real_elements(x)), Q.complex_elements(x)), Or(Not(Q.real_elements(x*y)), Q.complex_elements(x*y)), Or(Not(Q.real_elements(y)), Q.complex_elements(y)), Or(Not(Q.symmetric(x)), Q.square(x)), Or(Not(Q.symmetric(x*y)), Q.square(x*y)), Or(Not(Q.symmetric(y)), Q.square(y)), Or(Not(Q.triangular(x)), Q.lower_triangular(x), Q.upper_triangular(x)), Or(Not(Q.triangular(x*y)), Q.lower_triangular(x*y), Q.upper_triangular(x*y)), Or(Not(Q.triangular(y)), Q.lower_triangular(y), Q.upper_triangular(y)), Or(Not(Q.unit_triangular(x)), Q.triangular(x)), Or(Not(Q.unit_triangular(x*y)), Q.triangular(x*y)), Or(Not(Q.unit_triangular(y)), Q.triangular(y)), Or(Not(Q.unitary(x)), Q.invertible(x)), Or(Not(Q.unitary(x)), Q.normal(x)), Or(Not(Q.unitary(x*y)), Q.invertible(x*y)), Or(Not(Q.unitary(x*y)), Q.normal(x*y)), Or(Not(Q.unitary(y)), Q.invertible(y)), Or(Not(Q.unitary(y)), Q.normal(y)), Or(Not(Q.upper_triangular(x)), Q.triangular(x)), Or(Not(Q.upper_triangular(x*y)), Q.triangular(x*y)), Or(Not(Q.upper_triangular(y)), Q.triangular(y)), Or(Not(Q.zero(x)), Q.even(x)), Or(Not(Q.zero(x)), Q.real(x)), Or(Not(Q.zero(x*y)), Q.even(x*y)), Or(Not(Q.zero(x*y)), Q.real(x*y)), Or(Not(Q.zero(y)), Q.even(y)), Or(Not(Q.zero(y)), Q.real(y)), Or(Q.invertible(x), Q.singular(x)), Or(Q.invertible(x*y), Q.singular(x*y)), Or(Q.invertible(y), Q.singular(y)))