Quelle  los_graph.prf

(los_graph
 (los_graphic 0
  (los_graphic-2 "informal" 3349093821
   ("" (skosimp*)
    (("" (case "NOT P!1(x!2,x!1)")
      (("1" (case "NOT P!1(x!1,y!2)")
        (("1" (copy -5)
          (("1" (inst -1 "x!1" "y!2")
            (("1" (copy -6)
              (("1" (inst -1 "x!2" "x!1")
                (("1" (inst -5 "x!2" "x!1" "y!2")
                  (("1" (prop) nil nil)) nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (case "NOT P!1(y!1,y!2)")
          (("1" (copy -6)
            (("1" (inst -1 "y!1" "y!2")
              (("1" (copy -7)
                (("1" (inst -1 "x!2" "x!1")
                  (("1" (copy -8)
                    (("1" (inst -1 "x!1" "y!1")
                      (("1" (prop)
                        (("1" (copy -7)
                          (("1" (inst -1 "x!2" "x!1" "y!2")
                            (("1" (prop)
                              (("1"
                                (inst -7 "x!1" "y!1" "y!2")
                                (("1" (prop) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (inst -4 "y!1" "y!2")
            (("2" (prop)
              (("2" (inst -4 "x!1" "y!2" "y!1") (("2" (prop) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (case "NOT P!1(x!2,y!1)")
        (("1" (case "NOT P!1(y!1,y!2)")
          (("1" (copy -6)
            (("1" (inst -1 "x!2" "y!1")
              (("1" (inst -7 "y!1" "y!2")
                (("1" (prop)
                  (("1" (inst -6 "x!2" "y!1" "y!2")
                    (("1" (prop) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (inst -7 "x!2" "y!2")
            (("2" (prop)
              (("2" (inst -5 "y!1" "y!2")
                (("2" (prop)
                  (("2" (inst -5 "x!2" "y!2" "y!1")
                    (("2" (prop) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (inst -4 "x!2" "x!1")
          (("2" (inst -3 "x!1" "x!2" "y!1") (("2" (prop) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil los_graph nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak)
  (los_graphic-1 nil 3328254156
   ("" (skosimp*)
    (("" (case "P!1(x!2,x!1)&P!1(x!2,y!1)")
      (("1" (inst -3 "x!2" "x!1")
        (("1" (inst -2 "x!1" "x!2" "y!1") (("1" (prop) nil nil)) nil))
        nil)
       ("2" (case "P!1(x!1,y!2)&P!1(y!1,y!2)")
        (("1" (inst -3 "y!1" "y!2")
          (("1" (inst -2 "x!1" "y!2" "y!1") (("1" (prop) nil nil))
            nil))
          nil)
         ("2" (inst-cp -5 "x!1" "y!2")
          (("2" (inst-cp -5 "y!1" "y!2")
            (("2" (inst-cp -5 "y!1" "x!2")
              (("2" (inst-cp -5 "x!1" "x!2")
                (("2" (bddsimp)
                  (("1" (hide -6)
                    (("1" (inst -3 "y!1" "x!2") (("1" (prop) nil nil))
                      nil))
                    nil)
                   ("2" (inst -5 "y!1" "x!2")
                    (("2" (inst -4 "x!2" "y!1" "y!2")
                      (("2" (prop) nil nil)) nil))
                    nil)
                   ("3" (inst -3 "y!1" "x!2") (("3" (prop) nil nil))
                    nil)
                   ("4" (inst -5 "y!1" "x!2")
                    (("4" (inst -4 "x!2" "y!1" "y!2")
                      (("4" (prop) nil nil)) nil))
                    nil)
                   ("5" (inst -3 "y!1" "x!2")
                    (("5" (inst -2 "x!1" "x!2" "y!1")
                      (("5" (prop) nil nil)) nil))
                    nil)
                   ("6" (inst -5 "y!1" "x!2")
                    (("6" (inst -4 "x!2" "y!1" "y!2")
                      (("6" (prop) nil nil)) nil))
                    nil)
                   ("7" (inst -6 "x!2" "y!2")
                    (("7" (prop)
                      (("7" (inst -4 "x!1" "y!2")
                        (("7" (inst -3 "x!2" "y!2" "x!1")
                          (("7" (prop) nil nil)) nil))
                        nil))
                      nil))
                    nil)
                   ("8" (inst -5 "y!1" "x!2")
                    (("8" (inst -4 "x!2" "y!1" "y!2")
                      (("8" (prop) nil nil)) nil))
                    nil)
                   ("9" (inst -3 "y!1" "x!2")
                    (("9" (inst -2 "x!1" "x!2" "y!1")
                      (("9" (prop) nil nil)) nil))
                    nil)
                   ("10" (inst -6 "x!2" "y!2")
                    (("10" (prop)
                      (("10" (inst -3 "x!1" "x!2" "y!2")
                        (("10" (prop) nil nil)) nil))
                      nil))
                    nil)
                   ("11" (inst -5 "x!1" "x!2")
                    (("11" (inst -4 "x!2" "x!1" "y!2")
                      (("11" (prop) nil nil)) nil))
                    nil)
                   ("12" (inst -6 "x!1" "y!2")
                    (("12" (prop)
                      (("12" (inst -6 "x!1" "x!2")
                        (("12" (prop)
                          (("12" (inst -6 "x!2" "x!1" "y!2")
                            (("12" (prop) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("13" (inst -3 "y!1" "x!2")
                    (("13" (inst -2 "x!1" "x!2" "y!1")
                      (("13" (prop) nil nil)) nil))
                    nil)
                   ("14" (inst -3 "x!1" "x!2") (("14" (prop) nil nil))
                    nil)
                   ("15" (inst -5 "x!1" "x!2")
                    (("15" (inst -4 "x!2" "x!1" "y!2")
                      (("15" (prop) nil nil)) nil))
                    nil)
                   ("16" (inst -5 "x!1" "x!2")
                    (("16" (inst -4 "x!2" "x!1" "y!2")
                      (("16" (prop) nil nil)) nil))
                    nil)
                   ("17" (inst -2 "y!1" "x!2")
                    (("17" (inst -1 "x!1" "x!2" "y!1")
                      (("17" (prop) nil nil)) nil))
                    nil)
                   ("18" (inst -4 "y!1" "x!2")
                    (("18" (inst -3 "x!2" "y!1" "y!2")
                      (("18" (prop) nil nil)) nil))
                    nil)
                   ("19" (inst -4 "x!1" "x!2")
                    (("19" (inst -3 "x!2" "x!1" "y!2")
                      (("19" (prop) nil nil)) nil))
                    nil)
                   ("20" (inst -4 "y!1" "x!2")
                    (("20" (inst -3 "x!2" "y!1" "y!2")
                      (("20" (prop) nil nil)) nil))
                    nil)
                   ("21" (inst -2 "y!1" "x!2")
                    (("21" (inst -1 "x!1" "x!2" "y!1")
                      (("21" (prop) nil nil)) nil))
                    nil)
                   ("22" (inst -2 "x!1" "x!2") (("22" (prop) nil nil))
                    nil)
                   ("23" (inst -4 "x!1" "x!2")
                    (("23" (inst -3 "x!2" "x!1" "y!2")
                      (("23" (prop) nil nil)) nil))
                    nil)
                   ("24" (inst -4 "x!1" "x!2")
                    (("24" (inst -3 "x!2" "x!1" "y!2")
                      (("24" (prop) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   nil shostak))
 (Los 0
  (Los-1 nil 3328276414
   ("" (skolem!)
    (("" (lemma "los_graphic")
      (("" (inst -1 "(lambda x,y:P!1(x,y)&P!1(y,x))" "Q!1")
        (("" (skosimp*)
          (("" (bddsimp)
            (("1" (inst -3 "x!1" "y!1") (("1" (prop) nil nil)) nil)
             ("2" (inst -3 "x!2" "y!2") nil nil)
             ("3" (skolem! 1)
              (("3" (inst-cp -4 "x!3" "y!3")
                (("3" (inst -4 "y!3" "x!3")
                  (("3" (inst -2 "y!3" "x!3") (("3" (prop) nil nil))
                    nil))
                  nil))
                nil))
              nil)
             ("4" (skolem! 1) (("4" (prop) nil nil)) nil)
             ("5" (skolem! 1)
              (("5" (prop)
                (("1" (inst -7 "x!3" "y!3" "z!1")
                  (("1" (prop) nil nil)) nil)
                 ("2" (inst -7 "z!1" "y!3" "x!3")
                  (("2" (prop) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((los_graphic formula-decl nil los_graph nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil los_graph nil))
   shostak)))