>>> sat $ \x y z -> length x .== 5 .&& length y .== 1 .&& x ++ y ++ z .== [1 .. 12] Satisfiable. Model: s0 = [1,2,3,4,5] :: [Integer] s1 = [6] :: [Integer] s2 = [7,8,9,10,11,12] :: [Integer]
>>> sat $ \x y z -> length x .== 5 .&& length y .== 1 .&& x ++ y ++ z .== "Hello world!" Satisfiable. Model: s0 = "Hello" :: String s1 = " " :: String s2 = "world!" :: String