code: def default_reasoning_demo():
      lexpr = Expression.fromstring
  
      premises = []
  
      # define taxonomy
      premises.append(lexpr(r"all x.(elephant(x)        -> animal(x))"))
      premises.append(lexpr(r"all x.(bird(x)            -> animal(x))"))
      premises.append(lexpr(r"all x.(dove(x)            -> bird(x))"))
      premises.append(lexpr(r"all x.(ostrich(x)         -> bird(x))"))
      premises.append(
          lexpr(r"all x.(flying_ostrich(x)  -> ostrich(x))")
      )
  
      # default properties
      premises.append(
          lexpr(r"all x.((animal(x)  & -Ab1(x)) -> -fly(x))")
      )  # normal animals don't fly
      premises.append(
          lexpr(r"all x.((bird(x)    & -Ab2(x)) -> fly(x))")
      )  # normal birds fly
      premises.append(
          lexpr(r"all x.((ostrich(x) & -Ab3(x)) -> -fly(x))")
      )  # normal ostriches don't fly
  
      # specify abnormal entities
      premises.append(
          lexpr(r"all x.(bird(x)           -> Ab1(x))")
      )  # flight
      premises.append(
          lexpr(r"all x.(ostrich(x)        -> Ab2(x))")
      )  # non-flying bird
      premises.append(
          lexpr(r"all x.(flying_ostrich(x) -> Ab3(x))")
      )  # flying ostrich
  
      # define entities
      premises.append(lexpr(r"elephant(E)"))
      premises.append(lexpr(r"dove(D)"))
      premises.append(lexpr(r"ostrich(O)"))
  
      # print the assumptions
      prover = Prover9Command(None, premises)
      command = UniqueNamesProver(ClosedWorldProver(prover))
      for a in command.assumptions():
          print(a)
  
      print_proof("-fly(E)", premises)
      print_proof("fly(D)", premises)
      print_proof("-fly(O)", premises)
  
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 6 for calling a global function with example usage: default_reasoning_demo() without return types