SSL skolemization.prf   Sprache: unbekannt

(skolemization
 (skolemize_exists 0
  (skolemize_exists-1 nil 3314540935
   ("" (skolem!)
    (("" (prop)
      (("1" (inst + "LAMBDA d: epsilon(LAMBDA r: p!1(d, r))")
        (("1" (skolem!)
          (("1" (inst?)
            (("1" (use "epsilon_ax[R]")
              (("1" (replace*) nil nil)
               ("2" (skolem!) (("2" (inst?) nil nil)) nil))
              nil))
            nil))
          nil)
         ("2" (skolem!)
          (("2" (inst - "d!1")
            (("2" (skolem!) (("2" (inst?) nil nil)) nil)) nil))
          nil))
        nil)
       ("2" (skosimp*) (("2" (inst?) (("2" (inst?) nil nil)) nil))
        nil))
      nil))
    nil)
   ((epsilon_ax formula-decl nil epsilons nil)
    (epsilon const-decl "T" epsilons nil)
    (pred type-eq-decl nil defined_types nil)
    (D formal-type-decl nil skolemization nil)
    (R formal-type-decl nil skolemization nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (TRUE const-decl "bool" booleans nil))
   shostak))
 (skolemize_forall 0
  (skolemize_forall-1 nil 3314541090
   ("" (skolem!)
    (("" (prop)
      (("1" (skosimp*) (("1" (inst?) (("1" (inst?) nil nil)) nil)) nil)
       ("2" (inst - "LAMBDA d: epsilon(LAMBDA r: NOT p!1(d, r))")
        (("1" (skolem!)
          (("1" (inst?)
            (("1" (use "epsilon_ax[R]")
              (("1" (prop)
                (("1" (hide -1)
                  (("1" (skolem!) (("1" (inst?) nil nil)) nil)) nil))
                nil)
               ("2" (hide -1)
                (("2" (skolem!) (("2" (inst?) nil nil)) nil)) nil))
              nil))
            nil))
          nil)
         ("2" (skolem!)
          (("2" (inst 2 "d!1")
            (("2" (skolem!) (("2" (inst?) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((D formal-type-decl nil skolemization nil)
    (R formal-type-decl nil skolemization nil)
    (epsilon_ax formula-decl nil epsilons nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (epsilon const-decl "T" epsilons nil)
    (pred type-eq-decl nil defined_types nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (TRUE const-decl "bool" booleans nil))
   shostak)))