From 65f093e565806e8acf5b24b4c68a23dd78e29631 Mon Sep 17 00:00:00 2001 From: Gregory Bednov Date: Sun, 15 Jun 2025 04:25:00 +0300 Subject: [PATCH] prove feature, major refactoring --- Main.hs | 122 ++++++++++++++++++--------- Ternary/Statement.hs | 38 +++++---- Ternary/Vee.hs | 160 +++++++++++++++++++++++------------- Tests/syllotest | 192 +++++++++++++++++++++---------------------- 4 files changed, 307 insertions(+), 205 deletions(-) diff --git a/Main.hs b/Main.hs index a9f931a..13736c8 100644 --- a/Main.hs +++ b/Main.hs @@ -1,51 +1,99 @@ module Main (main) where -import Prelude (IO, String, getContents, lines, map, print, - otherwise, Bool(..), filter, id, unlines, - mapM_, ($), elem, notElem, (||), putStrLn, read, (.)) -import Ternary.Statement (Statement (..), st) -import Ternary.Universum (Universum (..), universum) -import Ternary.Vee (cleared, think) -import System.Environment (getArgs) -import Data.Foldable (Foldable) -main2 :: Universum -> Bool -> IO () -main2 u onlyNew = do +import Data.Foldable (Foldable, any) +import Data.List (head, tail) +import Data.Maybe (isNothing) +import GHC.Base (Maybe (..), (==)) +import System.Environment (getArgs) +import Ternary.Statement (Statement (..), st) +import Ternary.Term (Item (..), Term (..)) +import Ternary.Universum (Universum (..), universum) +import Ternary.Vee (cleared, hasContradiction, think) +import Prelude + ( Bool (..), + IO, + String, + elem, + filter, + getContents, + id, + lines, + map, + mapM_, + notElem, + otherwise, + print, + putStrLn, + read, + unlines, + ($), + (.), + (||), + ) + +mainSolve :: Universum -> Bool -> IO () +mainSolve u onlyNew = do strs <- getContents let statements = map str2vee . lines $ strs str2vee x = st (read x :: Statement String) mapM_ print . (if onlyNew then filter (`notElem` statements) else id) . cleared - . think (universum u) $ statements + . think (universum u) + $ statements -withArgs :: (String -> Bool) -> IO () +mainProve :: Universum -> Bool -> IO () +mainProve u onlyNew = do + strs <- getContents + let statements = map str2vee . tail . lines $ strs + proveThis = str2vee . head . lines $ strs + str2vee x = st (read x :: Statement String) + results = cleared . think (universum u) $ statements + anyContradictions = any (hasContradiction proveThis) results + proof = swapNothingJF $ if anyContradictions then Nothing else Just (Item recalc == Item results) + recalc = cleared . think (universum u) $ proveThis : statements + swapNothingJF x + | isNothing x = Just False + | x == Just False = Nothing + | x == Just True = Just True + + print recalc + putStrLn "" + print results + putStrLn "" + print proof + +withArgs :: (String -> Bool) -> IO () withArgs a - | a "-h" || a "--help" = putStrLn . unlines $ - ["Logical statement solver", - "Usage: solver [PARAMETERS]", - "", - "Designed according to N.P.Brousentsov works", - "and Lewis Carrol diagram. PARAMETERS:", - "", - "--aristotle, -A\tuse Aristotle logical universum VxVx' for each x", - "--new, -n\tfilters only 'new' facts, excluding defined", - "--help, -h\tshows this help", - "--version, -v\tshows this version", - "", - "Takes statement \"Socrates is a human\" in such format, e.g.", - "", - "A \"Socrates\" \"human\"", - "", - "There are A, E, O, I traditional statements exist.", - "Also there are A~, E~, O~, I~ with negated first part" - ] + | a "-h" || a "--help" = + putStrLn . unlines $ + [ "Logical statement solver", + "Usage: solver [PARAMETERS]", + "", + "Designed according to N.P.Brousentsov works", + "and Lewis Carrol diagram. PARAMETERS:", + "", + "--aristotle, -A\tuse Aristotle logical universum VxVx' for each x", + "--new, -n\tfilters only 'new' facts, excluding defined", + "--help, -h\tshows this help", + "--version, -v\tshows this version", + "", + "Takes statement \"Socrates is a human\" in such format, e.g.", + "", + "A \"Socrates\" \"human\"", + "", + "There are A, E, O, I traditional statements exist.", + "Also there are A~, E~, O~, I~ with negated first part" + ] | a "--version" || a "-v" = putStrLn "v1.0.2" - | otherwise = main2 uni onlyNew where - onlyNew = a "--new" || a "-n" - uni = - if a "-A" || a "--aristotle" - then Aristotle - else Empty + | a "--prove" = mainProve Aristotle False + | otherwise = mainSolve uni onlyNew + where + onlyNew = a "--new" || a "-n" + uni = + if a "-A" || a "--aristotle" + then Aristotle + else Empty main :: IO () main = do diff --git a/Ternary/Statement.hs b/Ternary/Statement.hs index a855150..ef8b74c 100644 --- a/Ternary/Statement.hs +++ b/Ternary/Statement.hs @@ -1,14 +1,18 @@ module Ternary.Statement (Statement(..), st) where import Ternary.Term (Vee, Term(..), Item(..)) -data Statement a = A a a -- Affirmo (general affirmative) - | I a a -- affIrmo (private affirmative) - | E a a -- nEgo (general negative) - | O a a -- negO (private negative) - | A' a a - | I' a a - | E' a a - | O' a a - deriving (Eq, Show, Read) + +data StatementKind = A | I | E | O | A' | I' | E' | O' deriving (Eq, Show, Read) +data Statement a = Statement StatementKind a a deriving (Eq, Read) + +instance Show a => Show (Statement a) where + show (Statement A x y) = "Every " ++ show x ++ " is " ++ show y + show (Statement I x y) = "Some of " ++ show x ++ " is " ++ show y + show (Statement E x y) = "None of " ++ show x ++ " is " ++ show y + show (Statement O x y) = "Some of " ++ show x ++ " isn't " ++ show y + show (Statement A' x y) = "Every non-" ++ show x ++ " is " ++ show y + show (Statement I' x y) = "Some of non-" ++ show x ++ " is " ++ show y + show (Statement E' x y) = "None of non-" ++ show x ++ " is " ++ show y + show (Statement O' x y) = "Some of non-" ++ show x ++ " isn't " ++ show y inv :: (Eq a) => Term a -> Term a inv (Term p x) = Term (not p) x @@ -20,11 +24,11 @@ i v x y | x == y = Term v . Item $ [x] st :: (Eq a) => Statement a -> Vee a -st (A x y) = i False (Term True x) (Term False y) -st (I x y) = i True (Term True x) (Term True y) -st (E x y) = i False (Term True x) (Term True y) -st (O x y) = i True (Term True x) (Term False y) -st (A' x y) = i False (Term False x) (Term False y) -st (I' x y) = i True (Term False x) (Term True y) -st (E' x y) = i False (Term False x) (Term True y) -st (O' x y) = i True (Term False x) (Term False y) +st (Statement A x y) = i False (Term True x) (Term False y) +st (Statement I x y) = i True (Term True x) (Term True y) +st (Statement E x y) = i False (Term True x) (Term True y) +st (Statement O x y) = i True (Term True x) (Term False y) +st (Statement A' x y) = i False (Term False x) (Term False y) +st (Statement I' x y) = i True (Term False x) (Term True y) +st (Statement E' x y) = i False (Term False x) (Term True y) +st (Statement O' x y) = i True (Term False x) (Term False y) diff --git a/Ternary/Vee.hs b/Ternary/Vee.hs index 19f8753..1743b9e 100644 --- a/Ternary/Vee.hs +++ b/Ternary/Vee.hs @@ -1,68 +1,118 @@ -module Ternary.Vee (isObvious, newFact, cleared, think) where -import Data.List (head, intersect, length, nub, null, union, (\\)) -import Data.Maybe (Maybe (Nothing), mapMaybe) -import Prelude (Bool (False, True), Eq, any, foldr, fst, map, - not, notElem, otherwise, return, snd, ($), (&&), - (.), (/=), (<$>), (<*>), (=<<), (==)) -import Ternary.Term (Item (..), Term (..), Vee) +module Ternary.Vee (isObvious, hasContradiction, newFact, cleared, think) where + +import Data.Foldable (concatMap) +import Data.List + ( elem, + filter, + head, + intersect, + iterate, + length, + nub, + null, + union, + (\\), + ) +import Data.Maybe (Maybe (Nothing), mapMaybe) +import GHC.Base ((<), (>)) +import GHC.Maybe (Maybe (..)) +import Ternary.Term (Item (..), Term (..), Vee) +import Prelude + ( Bool (False, True), + Eq, + any, + foldr, + fst, + map, + not, + notElem, + otherwise, + return, + snd, + ($), + (&&), + (.), + (/=), + (<$>), + (<*>), + (=<<), + (==), + ) + +type Knowledge a = [Vee a] + +type InferenceRule a = Vee a -> Vee a -> (Knowledge a, Maybe (Vee a)) + isSubsetOf :: (Eq a) => [a] -> [a] -> Bool a `isSubsetOf` b = nda && not ndb - where - nda = null $ a \\ b - ndb = null $ b \\ a + where + nda = null $ a \\ b + ndb = null $ b \\ a isObvious :: (Eq a) => Vee a -> Vee a -> Bool isObvious (Term x (Item a)) (Term y (Item b)) - | x /= y = False - | x = a `isSubsetOf` b - | not x = b `isSubsetOf` a + | x /= y = False + | x = a `isSubsetOf` b + | not x = b `isSubsetOf` a -newFact :: (Eq a) => Vee a -> Vee a -> ([Vee a], Maybe (Vee a)) +hasContradiction :: (Eq a) => Vee a -> Vee a -> Bool +hasContradiction (Term x (Item a)) (Term y (Item b)) + | a == b && x /= y = True + | a `isSubsetOf` b && x < y = True + | b `isSubsetOf` a && x > y = True + | otherwise = False + +notT :: Term a -> Term a +notT (Term x v) = Term (not x) v + +rulePosFromNeg :: (Eq a) => InferenceRule a +rulePosFromNeg (Term False (Item negSet)) positive@(Term True (Item posSet)) + | length diff /= 1 = ([], Nothing) + | missing `elem` posSet = ([], Nothing) + | otherwise = ([positive], Just (Term True (Item (missing : posSet)))) + where + diff = negSet \\ posSet + missing = notT (head diff) + +ruleNegFromNeg :: (Eq a) => InferenceRule a +ruleNegFromNeg (Term False (Item i0)) (Term False (Item i1)) + | length evidence /= 1 = ([], Nothing) + | null diff0 && null diff1 = (map (Term False . Item) [i0, i1], Just (Term False (Item result))) + | otherwise = ([], Just (Term False (Item result))) + where + evidence = map notT i0 `intersect` i1 + diff0 = (i0 \\ i1) \\ map notT evidence + diff1 = (i1 \\ i0) \\ evidence + result = (i0 `intersect` i1) `union` diff0 `union` diff1 + +newFact :: (Eq a) => InferenceRule a newFact a@(Term True _) b@(Term False _) = newFact b a -newFact (Term False (Item iF)) tT@(Term True (Item iT)) - | length ldF /= 1 = ([], Nothing) - | otherwise = - if d'F `notElem` iT - then (return tT, return (Term True (Item (d'F:iT)))) - else ([], Nothing) - where - ldF = iF \\ iT - d'F = notT . head $ ldF - notT (Term x v) = Term (not x) v -newFact (Term False (Item i0)) (Term False (Item i1)) - | length e /= 1 = ([], Nothing) - | otherwise = - if null d0 && null d1 - then (map (Term False . Item) [i0, i1], vee0) - else ([], vee0) - where - notT (Term x v) = Term (not x) v - terms = (i0 `intersect` i1) `union` d0 `union` d1 - e = map notT i0 `intersect` i1 - d0 = (i0 \\ i1) \\ map notT e - d1 = (i1 \\ i0) \\ e - vee0 = return (Term False (Item terms)) +newFact a@(Term False _) b@(Term True _) = rulePosFromNeg a b +newFact a@(Term False _) b@(Term False _) = ruleNegFromNeg a b newFact _ _ = ([], Nothing) -pseudofix :: (Eq a) => (a -> a) -> a -> a -pseudofix f x0 - | y == y' = y - | otherwise = y' - where - y = f x0 - y' = f y +next :: (Eq a) => (Knowledge a, Knowledge a) -> (Knowledge a, Knowledge a) +next (old, new) = (old `union` new \\ used, added) + where + results = [newFact o n | o <- old, n <- new] + used = concatMap fst results + added = mapMaybe snd results -next :: (Eq a) => ([Vee a], [Vee a]) -> ([Vee a], [Vee a]) -next (o,n) = (o `union` n \\ (fst =<< r), mapMaybe snd r) - where - r = newFact <$> o <*> n +applyFacts :: (Eq a) => Knowledge a -> Knowledge a -> Knowledge a +applyFacts old new = + fst . head . dropStable $ iterate next (old, new) + where + dropStable (x : y : xs) + | x == y = [x] + | otherwise = dropStable (y : xs) + dropStable _ = [] -applyFacts :: (Eq a) => [Vee a] -> [Vee a] -> [Vee a] -applyFacts old new = fst $ pseudofix next (old, new) +cleared :: (Eq a) => Knowledge a -> Knowledge a +cleared vees = nub $ filter (not . isRedundant) vees + where + isRedundant v = any (isObvious v) vees -cleared :: (Eq a) => [Vee a] -> [Vee a] -cleared vees = nub [vee | vee <- vees, not $ any (isObvious vee) vees] - -think :: (Eq a) => ([Vee a]->[Vee a]) -> [Vee a] -> [Vee a] -think addition = foldr (applyFacts . withUni . return) [] where +think :: (Eq a) => (Knowledge a -> Knowledge a) -> Knowledge a -> Knowledge a +think addition = foldr (applyFacts . withUni . return) [] + where withUni vees = applyFacts (addition vees) vees diff --git a/Tests/syllotest b/Tests/syllotest index 0458467..6aed93e 100644 --- a/Tests/syllotest +++ b/Tests/syllotest @@ -1,96 +1,96 @@ -(A "y" "z", A "x" "y", A "x" "z") -(A "y" "z", E' "x" "y", E' "x" "z") -(E "y" "z", A "x" "y", E "x" "z") -(E "y" "z", E' "x" "y", A' "x" "z") -(A "y" "z", A "x" "y", I "x" "z") -(A "y" "z", A "x" "y", I' "x" "z") -(A "y" "z", E' "x" "y", O "x" "z") -(A "y" "z", E' "x" "y", O' "x" "z") -(E "y" "z", A "x" "y", O "x" "z") -(E "y" "z", A "x" "y", O' "x" "z") -(E "y" "z", E' "x" "y", I "x" "z") -(E "y" "z", E' "x" "y", I' "x" "z") -(A "y" "z", A' "x" "y", I "x" "z") -(A "y" "z", E "x" "y", O' "x" "z") -(E "y" "z", A' "x" "y", O "x" "z") -(E "y" "z", E "x" "y", I' "x" "z") -(A "y" "z", I "x" "y", I "x" "z") -(A "y" "z", O' "x" "y", O' "x" "z") -(E "y" "z", I "x" "y", O "x" "z") -(E "y" "z", O' "x" "y", I' "x" "z") -(I "y" "z", A' "x" "y", I "x" "z") -(I "y" "z", E "x" "y", O' "x" "z") -(O "y" "z", A' "x" "y", O "x" "z") -(O "y" "z", E "x" "y", I' "x" "z") -(A "z" "y", A' "x" "y", A' "x" "z") -(A "z" "y", E "x" "y", E "x" "z") -(E "z" "y", A "x" "y", E "x" "z") -(E "z" "y", E' "x" "y", A' "x" "z") -(A "z" "y", A' "x" "y", I "x" "z") -(A "z" "y", A' "x" "y", I' "x" "z") -(A "z" "y", E "x" "y", O "x" "z") -(A "z" "y", E "x" "y", O' "x" "z") -(E "z" "y", A "x" "y", O "x" "z") -(E "z" "y", A "x" "y", O' "x" "z") -(E "z" "y", E' "x" "y", I "x" "z") -(E "z" "y", E' "x" "y", I' "x" "z") -(A "z" "y", A "x" "y", I' "x" "z") -(A "z" "y", E' "x" "y", O "x" "z") -(E "z" "y", A' "x" "y", O "x" "z") -(E "z" "y", E "x" "y", I' "x" "z") -(A "z" "y", I' "x" "y", I' "x" "z") -(A "z" "y", O "x" "y", O "x" "z") -(E "z" "y", I "x" "y", O "x" "z") -(E "z" "y", O' "x" "y", I' "x" "z") -(I "z" "y", A' "x" "y", I "x" "z") -(I "z" "y", E "x" "y", O' "x" "z") -(O "z" "y", A "x" "y", O' "x" "z") -(O "z" "y", E' "x" "y", I "x" "z") -(A "y" "z", A' "y" "x", A "x" "z") -(A "y" "z", E' "y" "x", E' "x" "z") -(E "y" "z", A' "y" "x", E "x" "z") -(E "y" "z", E' "y" "x", A' "x" "z") -(A "y" "z", A' "y" "x", I "x" "z") -(A "y" "z", A' "y" "x", I' "x" "z") -(A "y" "z", E' "y" "x", O "x" "z") -(A "y" "z", E' "y" "x", O' "x" "z") -(E "y" "z", A' "y" "x", O "x" "z") -(E "y" "z", A' "y" "x", O' "x" "z") -(E "y" "z", E' "y" "x", I "x" "z") -(E "y" "z", E' "y" "x", I' "x" "z") -(A "y" "z", A "y" "x", I "x" "z") -(A "y" "z", E "y" "x", O' "x" "z") -(E "y" "z", A "y" "x", O "x" "z") -(E "y" "z", E "y" "x", I' "x" "z") -(A "y" "z", I "y" "x", I "x" "z") -(A "y" "z", O "y" "x", O' "x" "z") -(E "y" "z", I "y" "x", O "x" "z") -(E "y" "z", O "y" "x", I' "x" "z") -(I "y" "z", A "y" "x", I "x" "z") -(I "y" "z", E "y" "x", O' "x" "z") -(O "y" "z", A "y" "x", O "x" "z") -(O "y" "z", E "y" "x", I' "x" "z") -(A "z" "y", A "y" "x", A' "x" "z") -(A "z" "y", E "y" "x", E "x" "z") -(E "z" "y", A' "y" "x", E "x" "z") -(E "z" "y", E' "y" "x", A' "x" "z") -(A "z" "y", A "y" "x", I "x" "z") -(A "z" "y", A "y" "x", I' "x" "z") -(A "z" "y", E "y" "x", O "x" "z") -(A "z" "y", E "y" "x", O' "x" "z") -(E "z" "y", A' "y" "x", O "x" "z") -(E "z" "y", A' "y" "x", O' "x" "z") -(E "z" "y", E' "y" "x", I "x" "z") -(E "z" "y", E' "y" "x", I' "x" "z") -(A "z" "y", A' "y" "x", I' "x" "z") -(A "z" "y", E' "y" "x", O "x" "z") -(E "z" "y", A "y" "x", O "x" "z") -(E "z" "y", E "y" "x", I' "x" "z") -(A "z" "y", I' "y" "x", I' "x" "z") -(A "z" "y", O' "y" "x", O "x" "z") -(E "z" "y", I "y" "x", O "x" "z") -(E "z" "y", O "y" "x", I' "x" "z") -(I "z" "y", A "y" "x", I "x" "z") -(I "z" "y", E "y" "x", O' "x" "z") -(O "z" "y", A' "y" "x", O' "x" "z") -(O "z" "y", E' "y" "x", I "x" "z") +(Statement A "y" "z", Statement A "x" "y", Statement A "x" "z") +(Statement A "y" "z", Statement E' "x" "y", Statement E' "x" "z") +(Statement E "y" "z", Statement A "x" "y", Statement E "x" "z") +(Statement E "y" "z", Statement E' "x" "y", Statement A' "x" "z") +(Statement A "y" "z", Statement A "x" "y", Statement I "x" "z") +(Statement A "y" "z", Statement A "x" "y", Statement I' "x" "z") +(Statement A "y" "z", Statement E' "x" "y", Statement O "x" "z") +(Statement A "y" "z", Statement E' "x" "y", Statement O' "x" "z") +(Statement E "y" "z", Statement A "x" "y", Statement O "x" "z") +(Statement E "y" "z", Statement A "x" "y", Statement O' "x" "z") +(Statement E "y" "z", Statement E' "x" "y", Statement I "x" "z") +(Statement E "y" "z", Statement E' "x" "y", Statement I' "x" "z") +(Statement A "y" "z", Statement A' "x" "y", Statement I "x" "z") +(Statement A "y" "z", Statement E "x" "y", Statement O' "x" "z") +(Statement E "y" "z", Statement A' "x" "y", Statement O "x" "z") +(Statement E "y" "z", Statement E "x" "y", Statement I' "x" "z") +(Statement A "y" "z", Statement I "x" "y", Statement I "x" "z") +(Statement A "y" "z", Statement O' "x" "y", Statement O' "x" "z") +(Statement E "y" "z", Statement I "x" "y", Statement O "x" "z") +(Statement E "y" "z", Statement O' "x" "y", Statement I' "x" "z") +(Statement I "y" "z", Statement A' "x" "y", Statement I "x" "z") +(Statement I "y" "z", Statement E "x" "y", Statement O' "x" "z") +(Statement O "y" "z", Statement A' "x" "y", Statement O "x" "z") +(Statement O "y" "z", Statement E "x" "y", Statement I' "x" "z") +(Statement A "z" "y", Statement A' "x" "y", Statement A' "x" "z") +(Statement A "z" "y", Statement E "x" "y", Statement E "x" "z") +(Statement E "z" "y", Statement A "x" "y", Statement E "x" "z") +(Statement E "z" "y", Statement E' "x" "y", Statement A' "x" "z") +(Statement A "z" "y", Statement A' "x" "y", Statement I "x" "z") +(Statement A "z" "y", Statement A' "x" "y", Statement I' "x" "z") +(Statement A "z" "y", Statement E "x" "y", Statement O "x" "z") +(Statement A "z" "y", Statement E "x" "y", Statement O' "x" "z") +(Statement E "z" "y", Statement A "x" "y", Statement O "x" "z") +(Statement E "z" "y", Statement A "x" "y", Statement O' "x" "z") +(Statement E "z" "y", Statement E' "x" "y", Statement I "x" "z") +(Statement E "z" "y", Statement E' "x" "y", Statement I' "x" "z") +(Statement A "z" "y", Statement A "x" "y", Statement I' "x" "z") +(Statement A "z" "y", Statement E' "x" "y", Statement O "x" "z") +(Statement E "z" "y", Statement A' "x" "y", Statement O "x" "z") +(Statement E "z" "y", Statement E "x" "y", Statement I' "x" "z") +(Statement A "z" "y", Statement I' "x" "y", Statement I' "x" "z") +(Statement A "z" "y", Statement O "x" "y", Statement O "x" "z") +(Statement E "z" "y", Statement I "x" "y", Statement O "x" "z") +(Statement E "z" "y", Statement O' "x" "y", Statement I' "x" "z") +(Statement I "z" "y", Statement A' "x" "y", Statement I "x" "z") +(Statement I "z" "y", Statement E "x" "y", Statement O' "x" "z") +(Statement O "z" "y", Statement A "x" "y", Statement O' "x" "z") +(Statement O "z" "y", Statement E' "x" "y", Statement I "x" "z") +(Statement A "y" "z", Statement A' "y" "x", Statement A "x" "z") +(Statement A "y" "z", Statement E' "y" "x", Statement E' "x" "z") +(Statement E "y" "z", Statement A' "y" "x", Statement E "x" "z") +(Statement E "y" "z", Statement E' "y" "x", Statement A' "x" "z") +(Statement A "y" "z", Statement A' "y" "x", Statement I "x" "z") +(Statement A "y" "z", Statement A' "y" "x", Statement I' "x" "z") +(Statement A "y" "z", Statement E' "y" "x", Statement O "x" "z") +(Statement A "y" "z", Statement E' "y" "x", Statement O' "x" "z") +(Statement E "y" "z", Statement A' "y" "x", Statement O "x" "z") +(Statement E "y" "z", Statement A' "y" "x", Statement O' "x" "z") +(Statement E "y" "z", Statement E' "y" "x", Statement I "x" "z") +(Statement E "y" "z", Statement E' "y" "x", Statement I' "x" "z") +(Statement A "y" "z", Statement A "y" "x", Statement I "x" "z") +(Statement A "y" "z", Statement E "y" "x", Statement O' "x" "z") +(Statement E "y" "z", Statement A "y" "x", Statement O "x" "z") +(Statement E "y" "z", Statement E "y" "x", Statement I' "x" "z") +(Statement A "y" "z", Statement I "y" "x", Statement I "x" "z") +(Statement A "y" "z", Statement O "y" "x", Statement O' "x" "z") +(Statement E "y" "z", Statement I "y" "x", Statement O "x" "z") +(Statement E "y" "z", Statement O "y" "x", Statement I' "x" "z") +(Statement I "y" "z", Statement A "y" "x", Statement I "x" "z") +(Statement I "y" "z", Statement E "y" "x", Statement O' "x" "z") +(Statement O "y" "z", Statement A "y" "x", Statement O "x" "z") +(Statement O "y" "z", Statement E "y" "x", Statement I' "x" "z") +(Statement A "z" "y", Statement A "y" "x", Statement A' "x" "z") +(Statement A "z" "y", Statement E "y" "x", Statement E "x" "z") +(Statement E "z" "y", Statement A' "y" "x", Statement E "x" "z") +(Statement E "z" "y", Statement E' "y" "x", Statement A' "x" "z") +(Statement A "z" "y", Statement A "y" "x", Statement I "x" "z") +(Statement A "z" "y", Statement A "y" "x", Statement I' "x" "z") +(Statement A "z" "y", Statement E "y" "x", Statement O "x" "z") +(Statement A "z" "y", Statement E "y" "x", Statement O' "x" "z") +(Statement E "z" "y", Statement A' "y" "x", Statement O "x" "z") +(Statement E "z" "y", Statement A' "y" "x", Statement O' "x" "z") +(Statement E "z" "y", Statement E' "y" "x", Statement I "x" "z") +(Statement E "z" "y", Statement E' "y" "x", Statement I' "x" "z") +(Statement A "z" "y", Statement A' "y" "x", Statement I' "x" "z") +(Statement A "z" "y", Statement E' "y" "x", Statement O "x" "z") +(Statement E "z" "y", Statement A "y" "x", Statement O "x" "z") +(Statement E "z" "y", Statement E "y" "x", Statement I' "x" "z") +(Statement A "z" "y", Statement I' "y" "x", Statement I' "x" "z") +(Statement A "z" "y", Statement O' "y" "x", Statement O "x" "z") +(Statement E "z" "y", Statement I "y" "x", Statement O "x" "z") +(Statement E "z" "y", Statement O "y" "x", Statement I' "x" "z") +(Statement I "z" "y", Statement A "y" "x", Statement I "x" "z") +(Statement I "z" "y", Statement E "y" "x", Statement O' "x" "z") +(Statement O "z" "y", Statement A' "y" "x", Statement O' "x" "z") +(Statement O "z" "y", Statement E' "y" "x", Statement I "x" "z")