code: def test_satisfiable_non_symbols():
      x, y = symbols("x y")
      assumptions = Q.zero(x * y)
      facts = Implies(Q.zero(x * y), Q.zero(x) | Q.zero(y))
      query = ~Q.zero(x) & ~Q.zero(y)
      refutations = [
          {Q.zero(x): True, Q.zero(x * y): True},
          {Q.zero(y): True, Q.zero(x * y): True},
          {Q.zero(x): True, Q.zero(y): True, Q.zero(x * y): True},
          {Q.zero(x): True, Q.zero(y): False, Q.zero(x * y): True},
          {Q.zero(x): False, Q.zero(y): True, Q.zero(x * y): True},
      ]
      assert not satisfiable(
          And(assumptions, facts, query), algorithm="dpll"
      )
      assert (
          satisfiable(And(assumptions, facts, ~query), algorithm="dpll")
          in refutations
      )
      assert not satisfiable(
          And(assumptions, facts, query), algorithm="dpll2"
      )
      assert (
          satisfiable(
              And(assumptions, facts, ~query), algorithm="dpll2"
          )
          in refutations
      )
  
imports: from sympy.assumptions.ask import Q
  from sympy.core.symbol import symbols
  from sympy.core.relational import Unequality
  from sympy.logic.boolalg import And, Or, Implies, Equivalent, true, false
  from sympy.logic.inference import literal_symbol, pl_true, satisfiable, valid, entails, PropKB
  from sympy.logic.algorithms.dpll import dpll, dpll_satisfiable, find_pure_symbol, find_unit_clause, unit_propagate, find_pure_symbol_int_repr, find_unit_clause_int_repr, unit_propagate_int_repr
  from sympy.logic.algorithms.dpll2 import dpll_satisfiable
  from sympy.logic.algorithms.z3_wrapper import z3_satisfiable
  from sympy.assumptions.cnf import CNF, EncodedCNF
  from sympy.logic.tests.test_lra_theory import make_random_problem
  from sympy.core.random import randint
  from sympy.testing.pytest import raises, skip
  from sympy.external import import_module
label_desc: Use image node_id 20 for calling a global function with example usage: test_satisfiable_non_symbols() without return types