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)
  
      all_pred, all_exprs = get_all_pred_and_expr_from_enc_cnf(sat_true)
  
      for pred in all_pred:
          if pred.function not in WHITE_LIST and pred.function != Q.ne:
              raise UnhandledInput(
                  f"LRASolver: {pred} is an unhandled predicate"
              )
      for expr in all_exprs:
          if expr.kind == MatrixKind(NumberKind):
              raise UnhandledInput(
                  f"LRASolver: {expr} is of MatrixKind"
              )
          if expr == S.NaN:
              raise UnhandledInput("LRASolver: nan")
  
      # convert old assumptions into predicates and add them to sat_true and sat_false
      # also check for unhandled predicates
      for assm in extract_pred_from_old_assum(all_exprs):
          n = len(sat_true.encoding)
          if assm not in sat_true.encoding:
              sat_true.encoding[assm] = n + 1
          sat_true.data.append([sat_true.encoding[assm]])
  
          n = len(sat_false.encoding)
          if assm not in sat_false.encoding:
              sat_false.encoding[assm] = n + 1
          sat_false.data.append([sat_false.encoding[assm]])
  
      sat_true = _preprocess(sat_true)
      sat_false = _preprocess(sat_false)
  
      can_be_true = (
          satisfiable(sat_true, use_lra_theory=True) is not False
      )
      can_be_false = (
          satisfiable(sat_false, use_lra_theory=True) is not 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:
          raise ValueError("Inconsistent assumptions")
  
file_path: sympy/sympy/assumptions/lra_satask.py
imports: from sympy.assumptions.assume import global_assumptions
  from sympy.assumptions.cnf import CNF, EncodedCNF
  from sympy.assumptions.ask import Q
  from sympy.logic.inference import satisfiable
  from sympy.logic.algorithms.lra_theory import UnhandledInput, ALLOWED_PRED
  from sympy.matrices.kind import MatrixKind
  from sympy.core.kind import NumberKind
  from sympy.assumptions.assume import AppliedPredicate
  from sympy.core.mul import Mul
  from sympy.core.singleton import S
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