code: def lra_satask(
      proposition, assumptions=True, context=global_assumptions
  ):
      """
      Function to evaluate the proposition with assumptions using SAT algorithm
      in conjunction with an Linear Real Arithmetic theory solver.
  
      Used to handle inequalities. Should eventually be depreciated and combined
      into satask, but infinity handling and other things need to be implemented
      before that can happen.
      """
      props = CNF.from_prop(proposition)
      _props = CNF.from_prop(~proposition)
  
      cnf = CNF.from_prop(assumptions)
      assumptions = EncodedCNF()
      assumptions.from_cnf(cnf)
  
      context_cnf = CNF()
      if context:
          context_cnf = context_cnf.extend(context)
  
      assumptions.add_from_cnf(context_cnf)
  
      return check_satisfiability(props, _props, 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 1 for calling a global function with example usage: lra_satask(proposition, assumptions, context) and returns: check_satisfiability