code: def tableau_test(c, ps=None, verbose=False):
      pc = Expression.fromstring(c)
      pps = [Expression.fromstring(p) for p in ps] if ps else []
      if not ps:
          ps = []
      print(
          "%s |- %s: %s"
          % (
              ", ".join(ps),
              pc,
              TableauProver().prove(pc, pps, verbose=verbose),
          )
      )
  
imports: from nltk.inference.api import BaseProverCommand, Prover
  from nltk.internals import Counter
  from nltk.sem.logic import AbstractVariableExpression, AllExpression, AndExpression, ApplicationExpression, EqualityExpression, ExistsExpression, Expression, FunctionVariableExpression, IffExpression, ImpExpression, LambdaExpression, NegatedExpression, OrExpression, Variable, VariableExpression, unique_variable
label_desc: Use image node_id 3 for calling a global function with example usage: tableau_test(c, ps, verbose) without return types