code: def closed_domain_demo():
      lexpr = Expression.fromstring
  
      p1 = lexpr(r"exists x.walk(x)")
      p2 = lexpr(r"man(Socrates)")
      c = lexpr(r"walk(Socrates)")
      prover = Prover9Command(c, [p1, p2])
      print(prover.prove())
      cdp = ClosedDomainProver(prover)
      print("assumptions:")
      for a in cdp.assumptions():
          print("   ", a)
      print("goal:", cdp.goal())
      print(cdp.prove())
  
      p1 = lexpr(r"exists x.walk(x)")
      p2 = lexpr(r"man(Socrates)")
      p3 = lexpr(r"-walk(Bill)")
      c = lexpr(r"walk(Socrates)")
      prover = Prover9Command(c, [p1, p2, p3])
      print(prover.prove())
      cdp = ClosedDomainProver(prover)
      print("assumptions:")
      for a in cdp.assumptions():
          print("   ", a)
      print("goal:", cdp.goal())
      print(cdp.prove())
  
      p1 = lexpr(r"exists x.walk(x)")
      p2 = lexpr(r"man(Socrates)")
      p3 = lexpr(r"-walk(Bill)")
      c = lexpr(r"walk(Socrates)")
      prover = Prover9Command(c, [p1, p2, p3])
      print(prover.prove())
      cdp = ClosedDomainProver(prover)
      print("assumptions:")
      for a in cdp.assumptions():
          print("   ", a)
      print("goal:", cdp.goal())
      print(cdp.prove())
  
      p1 = lexpr(r"walk(Socrates)")
      p2 = lexpr(r"walk(Bill)")
      c = lexpr(r"all x.walk(x)")
      prover = Prover9Command(c, [p1, p2])
      print(prover.prove())
      cdp = ClosedDomainProver(prover)
      print("assumptions:")
      for a in cdp.assumptions():
          print("   ", a)
      print("goal:", cdp.goal())
      print(cdp.prove())
  
      p1 = lexpr(r"girl(mary)")
      p2 = lexpr(r"dog(rover)")
      p3 = lexpr(r"all x.(girl(x) -> -dog(x))")
      p4 = lexpr(r"all x.(dog(x) -> -girl(x))")
      p5 = lexpr(r"chase(mary, rover)")
      c = lexpr(r"exists y.(dog(y) & all x.(girl(x) -> chase(x,y)))")
      prover = Prover9Command(c, [p1, p2, p3, p4, p5])
      print(prover.prove())
      cdp = ClosedDomainProver(prover)
      print("assumptions:")
      for a in cdp.assumptions():
          print("   ", a)
      print("goal:", cdp.goal())
      print(cdp.prove())
  
imports: from collections import defaultdict
  from functools import reduce
  from nltk.inference.api import Prover, ProverCommandDecorator
  from nltk.inference.prover9 import Prover9, Prover9Command
  from nltk.sem.logic import AbstractVariableExpression, AllExpression, AndExpression, ApplicationExpression, BooleanExpression, EqualityExpression, ExistsExpression, Expression, ImpExpression, NegatedExpression, Variable, VariableExpression, operator, unique_variable
label_desc: Use image node_id 2 for calling a global function with example usage: closed_domain_demo() without return types