code: def check_satisfiability(prop, _prop, factbase):
      sat_true = factbase.copy()
      sat_false = factbase.copy()
      sat_true.add_from_cnf(prop)
      sat_false.add_from_cnf(_prop)
      can_be_true = satisfiable(sat_true)
      can_be_false = satisfiable(sat_false)
  
      if can_be_true and can_be_false:
          return None
  
      if can_be_true and not can_be_false:
          return True
  
      if not can_be_true and can_be_false:
          return False
  
      if not can_be_true and not can_be_false:
          # TODO: Run additional checks to see which combination of the
          # assumptions, global_assumptions, and relevant_facts are
          # inconsistent.
          raise ValueError("Inconsistent assumptions")
  
file_path: sympy/sympy/assumptions/satask.py
imports: from sympy.core.singleton import S
  from sympy.core.symbol import Symbol
  from sympy.core.kind import NumberKind, UndefinedKind
  from sympy.assumptions.ask_generated import get_all_known_matrix_facts, get_all_known_number_facts
  from sympy.assumptions.assume import global_assumptions, AppliedPredicate
  from sympy.assumptions.sathandlers import class_fact_registry
  from sympy.core import oo
  from sympy.logic.inference import satisfiable
  from sympy.assumptions.cnf import CNF, EncodedCNF
  from sympy.matrices.kind import MatrixKind
label_desc: Use image node_id 2 for calling a global function with example usage: check_satisfiability(prop, _prop, factbase) and returns: None, True, False