(los_graph"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" "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 )nil los_graph nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))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))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 )nil los_graph nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil los_graph nil ))quality 100%
¤ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
