import Yices.Painless.Language

main = print =<< solve p

data S = S1 | S2 | S3
    deriving (Show, Enum)

p x1 x2 x3 x4 = 
    and 
      [ (/=*) x1 x2
      , (/=*) x1 x3
      , (/=*) x1 x4
      , (/=*) x2 x3
      , (/=*) x2 x4
      , (/=*) x3 x4
      ]