large expression to convert to cnf

gistfile1.txt

In [2]: from sympy.assumptions.satask import get_all_relevant_facts

In [3]: A = get_all_relevant_facts(Q.positive(x*y + 1), Q.positive(x) & Q.positive(y))

In [4]: print(A)
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(1), Q.integer(x*y)), Q.integer(x*y + 1)), 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(1), Q.positive(x*y)), Q.positive(x*y + 1)), 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(1), Q.rational(x*y)), Q.rational(x*y + 1)), Implies(And(Q.rational(x), Q.rational(y)), Q.rational(x*y)), Implies(And(Q.real(1), Q.real(x*y)), Implies(Or(And(Not(Q.irrational(1)), Q.irrational(x*y)), And(Not(Q.irrational(x*y)), Q.irrational(1))), Q.irrational(x*y + 1))), Implies(And(Q.real(1), Q.real(x*y)), Q.real(x*y + 1)), 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.integer(1)), Q.integer(x*y)), And(Not(Q.integer(x*y)), Q.integer(1))), Not(Q.integer(x*y + 1))), Implies(Or(And(Not(Q.rational(x)), Q.rational(y)), And(Not(Q.rational(y)), Q.rational(x))), Not(Q.integer(x*y))), Not(Q.even(1)), Not(Q.imaginary(1)), Not(Q.irrational(1)), Not(Q.negative(1)), Not(Q.nonpositive(1)), Not(Q.prime(1)), Not(Q.zero(1)), Or(Not(Q.algebraic(1)), Q.complex(1)), Or(Not(Q.algebraic(x)), Q.complex(x)), Or(Not(Q.algebraic(x*y + 1)), Q.complex(x*y + 1)), Or(Not(Q.algebraic(x*y)), Q.complex(x*y)), Or(Not(Q.algebraic(y)), Q.complex(y)), Or(Not(Q.antihermitian(1)), Not(Q.hermitian(1))), Or(Not(Q.antihermitian(x)), Not(Q.hermitian(x))), Or(Not(Q.antihermitian(x*y + 1)), Not(Q.hermitian(x*y + 1))), Or(Not(Q.antihermitian(x*y)), Not(Q.hermitian(x*y))), Or(Not(Q.antihermitian(y)), Not(Q.hermitian(y))), Or(Not(Q.composite(1)), Not(Q.prime(1))), Or(Not(Q.composite(x)), Not(Q.prime(x))), Or(Not(Q.composite(x*y + 1)), Not(Q.prime(x*y + 1))), Or(Not(Q.composite(x*y)), Not(Q.prime(x*y))), Or(Not(Q.composite(y)), Not(Q.prime(y))), Or(Not(Q.diagonal(1)), Q.lower_triangular(1)), Or(Not(Q.diagonal(1)), Q.normal(1)), Or(Not(Q.diagonal(1)), Q.symmetric(1)), Or(Not(Q.diagonal(1)), Q.upper_triangular(1)), 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 + 1)), Q.lower_triangular(x*y + 1)), Or(Not(Q.diagonal(x*y + 1)), Q.normal(x*y + 1)), Or(Not(Q.diagonal(x*y + 1)), Q.symmetric(x*y + 1)), Or(Not(Q.diagonal(x*y + 1)), Q.upper_triangular(x*y + 1)), 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(1)), Not(Q.odd(1))), Or(Not(Q.even(1)), Q.integer(1)), Or(Not(Q.even(x)), Not(Q.odd(x))), Or(Not(Q.even(x)), Q.integer(x)), Or(Not(Q.even(x*y + 1)), Not(Q.odd(x*y + 1))), Or(Not(Q.even(x*y + 1)), Q.integer(x*y + 1)), 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(1)), Q.infinity(1), Q.real(1)), Or(Not(Q.extended_real(x)), Q.infinity(x), Q.real(x)), Or(Not(Q.extended_real(x*y + 1)), Q.infinity(x*y + 1), Q.real(x*y + 1)), 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(1)), Not(Q.square(1)), Q.invertible(1)), Or(Not(Q.fullrank(x)), Not(Q.square(x)), Q.invertible(x)), Or(Not(Q.fullrank(x*y + 1)), Not(Q.square(x*y + 1)), Q.invertible(x*y + 1)), 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(1)), Not(Q.real(1))), Or(Not(Q.imaginary(1)), Q.antihermitian(1)), Or(Not(Q.imaginary(1)), Q.complex(1)), 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 + 1)), Not(Q.real(x*y + 1))), Or(Not(Q.imaginary(x*y + 1)), Q.antihermitian(x*y + 1)), Or(Not(Q.imaginary(x*y + 1)), Q.complex(x*y + 1)), 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(1)), Q.extended_real(1)), Or(Not(Q.infinity(x)), Q.extended_real(x)), Or(Not(Q.infinity(x*y + 1)), Q.extended_real(x*y + 1)), Or(Not(Q.infinity(x*y)), Q.extended_real(x*y)), Or(Not(Q.infinity(y)), Q.extended_real(y)), Or(Not(Q.integer(1)), Not(Q.positive(1)), Q.composite(1), Q.prime(1)), Or(Not(Q.integer(1)), Q.even(1), Q.odd(1)), Or(Not(Q.integer(1)), Q.rational(1)), 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 + 1)), Not(Q.positive(x*y + 1)), Q.composite(x*y + 1), Q.prime(x*y + 1)), Or(Not(Q.integer(x*y + 1)), Q.even(x*y + 1), Q.odd(x*y + 1)), Or(Not(Q.integer(x*y + 1)), Q.rational(x*y + 1)), 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(1)), Q.real_elements(1)), Or(Not(Q.integer_elements(x)), Q.real_elements(x)), Or(Not(Q.integer_elements(x*y + 1)), Q.real_elements(x*y + 1)), 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(1)), Not(Q.singular(1))), Or(Not(Q.invertible(1)), Q.fullrank(1)), Or(Not(Q.invertible(1)), Q.square(1)), 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 + 1)), Not(Q.singular(x*y + 1))), Or(Not(Q.invertible(x*y + 1)), Q.fullrank(x*y + 1)), Or(Not(Q.invertible(x*y + 1)), Q.square(x*y + 1)), 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(1)), Not(Q.rational(1))), Or(Not(Q.irrational(1)), Q.real(1)), Or(Not(Q.irrational(x)), Not(Q.rational(x))), Or(Not(Q.irrational(x)), Q.real(x)), Or(Not(Q.irrational(x*y + 1)), Not(Q.rational(x*y + 1))), Or(Not(Q.irrational(x*y + 1)), Q.real(x*y + 1)), 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(1)), Not(Q.upper_triangular(1)), Q.diagonal(1)), Or(Not(Q.lower_triangular(1)), Q.triangular(1)), 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 + 1)), Not(Q.upper_triangular(x*y + 1)), Q.diagonal(x*y + 1)), Or(Not(Q.lower_triangular(x*y + 1)), Q.triangular(x*y + 1)), 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(1)), Not(Q.nonnegative(1))), Or(Not(Q.negative(1)), Not(Q.positive(1))), Or(Not(Q.negative(1)), Q.nonzero(1)), 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 + 1)), Not(Q.nonnegative(x*y + 1))), Or(Not(Q.negative(x*y + 1)), Not(Q.positive(x*y + 1))), Or(Not(Q.negative(x*y + 1)), Q.nonzero(x*y + 1)), 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(1)), Q.real(1)), Or(Not(Q.nonnegative(x)), Q.real(x)), Or(Not(Q.nonnegative(x*y + 1)), Q.real(x*y + 1)), Or(Not(Q.nonnegative(x*y)), Q.real(x*y)), Or(Not(Q.nonnegative(y)), Q.real(y)), Or(Not(Q.nonpositive(1)), Not(Q.positive(1))), Or(Not(Q.nonpositive(1)), Q.real(1)), Or(Not(Q.nonpositive(x)), Not(Q.positive(x))), Or(Not(Q.nonpositive(x)), Q.real(x)), Or(Not(Q.nonpositive(x*y + 1)), Not(Q.positive(x*y + 1))), Or(Not(Q.nonpositive(x*y + 1)), Q.real(x*y + 1)), 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(1)), Not(Q.zero(1))), Or(Not(Q.nonzero(1)), Q.negative(1), Q.positive(1)), Or(Not(Q.nonzero(1)), Q.real(1)), 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 + 1)), Not(Q.zero(x*y + 1))), Or(Not(Q.nonzero(x*y + 1)), Q.negative(x*y + 1), Q.positive(x*y + 1)), Or(Not(Q.nonzero(x*y + 1)), Q.real(x*y + 1)), 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(1)), Q.square(1)), Or(Not(Q.normal(x)), Q.square(x)), Or(Not(Q.normal(x*y + 1)), Q.square(x*y + 1)), Or(Not(Q.normal(x*y)), Q.square(x*y)), Or(Not(Q.normal(y)), Q.square(y)), Or(Not(Q.odd(1)), Q.integer(1)), Or(Not(Q.odd(x)), Q.integer(x)), Or(Not(Q.odd(x*y + 1)), Q.integer(x*y + 1)), Or(Not(Q.odd(x*y)), Q.integer(x*y)), Or(Not(Q.odd(y)), Q.integer(y)), Or(Not(Q.orthogonal(1)), Q.positive_definite(1)), Or(Not(Q.orthogonal(1)), Q.unitary(1)), Or(Not(Q.orthogonal(x)), Q.positive_definite(x)), Or(Not(Q.orthogonal(x)), Q.unitary(x)), Or(Not(Q.orthogonal(x*y + 1)), Q.positive_definite(x*y + 1)), Or(Not(Q.orthogonal(x*y + 1)), Q.unitary(x*y + 1)), 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(1)), Q.nonzero(1)), Or(Not(Q.positive(x)), Q.nonzero(x)), Or(Not(Q.positive(x*y + 1)), Q.nonzero(x*y + 1)), Or(Not(Q.positive(x*y)), Q.nonzero(x*y)), Or(Not(Q.positive(y)), Q.nonzero(y)), Or(Not(Q.positive_definite(1)), Q.invertible(1)), Or(Not(Q.positive_definite(x)), Q.invertible(x)), Or(Not(Q.positive_definite(x*y + 1)), Q.invertible(x*y + 1)), Or(Not(Q.positive_definite(x*y)), Q.invertible(x*y)), Or(Not(Q.positive_definite(y)), Q.invertible(y)), Or(Not(Q.prime(1)), Q.integer(1)), Or(Not(Q.prime(1)), Q.positive(1)), Or(Not(Q.prime(x)), Q.integer(x)), Or(Not(Q.prime(x)), Q.positive(x)), Or(Not(Q.prime(x*y + 1)), Q.integer(x*y + 1)), Or(Not(Q.prime(x*y + 1)), Q.positive(x*y + 1)), 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(1)), Q.algebraic(1)), Or(Not(Q.rational(1)), Q.real(1)), Or(Not(Q.rational(x)), Q.algebraic(x)), Or(Not(Q.rational(x)), Q.real(x)), Or(Not(Q.rational(x*y + 1)), Q.algebraic(x*y + 1)), Or(Not(Q.rational(x*y + 1)), Q.real(x*y + 1)), 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(1)), Not(Q.unitary(1)), Q.orthogonal(1)), Or(Not(Q.real(1)), Q.complex(1)), Or(Not(Q.real(1)), Q.extended_real(1)), Or(Not(Q.real(1)), Q.hermitian(1)), Or(Not(Q.real(1)), Q.irrational(1), Q.rational(1)), Or(Not(Q.real(1)), Q.negative(1), Q.nonnegative(1)), Or(Not(Q.real(1)), Q.nonpositive(1), Q.positive(1)), Or(Not(Q.real(1)), Q.nonzero(1), Q.zero(1)), 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 + 1)), Not(Q.unitary(x*y + 1)), Q.orthogonal(x*y + 1)), Or(Not(Q.real(x*y + 1)), Q.complex(x*y + 1)), Or(Not(Q.real(x*y + 1)), Q.extended_real(x*y + 1)), Or(Not(Q.real(x*y + 1)), Q.hermitian(x*y + 1)), Or(Not(Q.real(x*y + 1)), Q.irrational(x*y + 1), Q.rational(x*y + 1)), Or(Not(Q.real(x*y + 1)), Q.negative(x*y + 1), Q.nonnegative(x*y + 1)), Or(Not(Q.real(x*y + 1)), Q.nonpositive(x*y + 1), Q.positive(x*y + 1)), Or(Not(Q.real(x*y + 1)), Q.nonzero(x*y + 1), Q.zero(x*y + 1)), 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(1)), Q.complex_elements(1)), Or(Not(Q.real_elements(x)), Q.complex_elements(x)), Or(Not(Q.real_elements(x*y + 1)), Q.complex_elements(x*y + 1)), 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(1)), Q.square(1)), Or(Not(Q.symmetric(x)), Q.square(x)), Or(Not(Q.symmetric(x*y + 1)), Q.square(x*y + 1)), Or(Not(Q.symmetric(x*y)), Q.square(x*y)), Or(Not(Q.symmetric(y)), Q.square(y)), Or(Not(Q.triangular(1)), Q.lower_triangular(1), Q.upper_triangular(1)), Or(Not(Q.triangular(x)), Q.lower_triangular(x), Q.upper_triangular(x)), Or(Not(Q.triangular(x*y + 1)), Q.lower_triangular(x*y + 1), Q.upper_triangular(x*y + 1)), 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(1)), Q.triangular(1)), Or(Not(Q.unit_triangular(x)), Q.triangular(x)), Or(Not(Q.unit_triangular(x*y + 1)), Q.triangular(x*y + 1)), Or(Not(Q.unit_triangular(x*y)), Q.triangular(x*y)), Or(Not(Q.unit_triangular(y)), Q.triangular(y)), Or(Not(Q.unitary(1)), Q.invertible(1)), Or(Not(Q.unitary(1)), Q.normal(1)), Or(Not(Q.unitary(x)), Q.invertible(x)), Or(Not(Q.unitary(x)), Q.normal(x)), Or(Not(Q.unitary(x*y + 1)), Q.invertible(x*y + 1)), Or(Not(Q.unitary(x*y + 1)), Q.normal(x*y + 1)), 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(1)), Q.triangular(1)), Or(Not(Q.upper_triangular(x)), Q.triangular(x)), Or(Not(Q.upper_triangular(x*y + 1)), Q.triangular(x*y + 1)), Or(Not(Q.upper_triangular(x*y)), Q.triangular(x*y)), Or(Not(Q.upper_triangular(y)), Q.triangular(y)), Or(Not(Q.zero(1)), Q.even(1)), Or(Not(Q.zero(1)), Q.real(1)), Or(Not(Q.zero(x)), Q.even(x)), Or(Not(Q.zero(x)), Q.real(x)), Or(Not(Q.zero(x*y + 1)), Q.even(x*y + 1)), Or(Not(Q.zero(x*y + 1)), Q.real(x*y + 1)), 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(1), Q.singular(1)), Or(Q.invertible(x), Q.singular(x)), Or(Q.invertible(x*y + 1), Q.singular(x*y + 1)), Or(Q.invertible(x*y), Q.singular(x*y)), Or(Q.invertible(y), Q.singular(y)), Q.integer(1), Q.nonnegative(1), Q.nonzero(1), Q.odd(1), Q.positive(1), Q.rational(1))