(set-option :produce-models true)
(set-logic QF_UF)
(declare-sort Tom 0)
(declare-sort Queen 0)
(declare-sort Activities 0)
(declare-sort NumKittens 0)

(declare-const Batman Tom)
(declare-const Jake Tom)
(declare-const Dibii Tom)

(declare-const Ruby Queen)
(declare-const Spot Queen)
(declare-const Starbuck Queen)

(declare-const Lazer Activities)
(declare-const Sleep Activities)
(declare-const Ball Activities)

(declare-const OneKitten NumKittens)
(declare-const TwoKittens NumKittens)
(declare-const ThreeKittens NumKittens)

(declare-fun QueenPartner (Queen) Tom)
(declare-fun QueenActivity (Queen) Activities)
(declare-fun QueenKittens (Queen) NumKittens)
(declare-fun TomPartner (Tom) Queen)

; All cats, num kittens,  and activities are unique
(assert (and
    (not (= Ruby Spot))
    (not (= Ruby Starbuck))
    (not (= Spot Starbuck))
    (not (= Batman Jake))
    (not (= Batman Dibii))
    (not (= Jake Dibii))
    (not (= Lazer Sleep))
    (not (= Lazer Ball))
    (not (= Sleep Ball))
    (not (= OneKitten TwoKittens))
    (not (= OneKitten ThreeKittens))
    (not (= TwoKittens ThreeKittens))))

; "Do not conjure values besides the declared constants" consistency check.
(assert (and
    (or (= (QueenPartner Ruby) Batman) (= (QueenPartner Ruby) Jake) (= (QueenPartner Ruby) Dibii))
    (or (= (QueenPartner Spot) Batman) (= (QueenPartner Spot) Jake) (= (QueenPartner Spot) Dibii))
    (or (= (QueenPartner Starbuck) Batman) (= (QueenPartner Starbuck) Jake) (= (QueenPartner Starbuck) Dibii))
    (or (= (QueenActivity Ruby) Lazer) (= (QueenActivity Ruby) Sleep) (= (QueenActivity Ruby) Ball))
    (or (= (QueenActivity Spot) Lazer) (= (QueenActivity Spot) Sleep) (= (QueenActivity Spot) Ball))
    (or (= (QueenActivity Starbuck) Lazer) (= (QueenActivity Starbuck) Sleep) (= (QueenActivity Starbuck) Ball))
    (or (= (QueenKittens Ruby) OneKitten) (= (QueenKittens Ruby) TwoKittens) (= (QueenKittens Ruby) ThreeKittens))
    (or (= (QueenKittens Spot) OneKitten) (= (QueenKittens Spot) TwoKittens) (= (QueenKittens Spot) ThreeKittens))
    (or (= (QueenKittens Starbuck) OneKitten) (= (QueenKittens Starbuck) TwoKittens) (= (QueenKittens Starbuck) ThreeKittens))
))

; "Only one dot in each row/col" consistency check.
(assert (and
    (not (= (QueenPartner Ruby) (QueenPartner Spot)))
    (not (= (QueenPartner Ruby) (QueenPartner Starbuck)))
    (not (= (QueenPartner Spot) (QueenPartner Starbuck)))
    (not (= (QueenKittens Ruby) (QueenKittens Spot)))
    (not (= (QueenKittens Ruby) (QueenKittens Starbuck)))
    (not (= (QueenKittens Spot) (QueenKittens Starbuck)))
    (not (= (QueenActivity Ruby) (QueenActivity Spot)))
    (not (= (QueenActivity Ruby) (QueenActivity Starbuck)))
    (not (= (QueenActivity Spot) (QueenActivity Starbuck)))))

; All other constraints for Tom are implied if the partner of the partner is the same.
(assert (and
    (or (= (TomPartner Batman) Ruby) (= (TomPartner Batman) Spot) (= (TomPartner Batman) Starbuck))
    (or (= (TomPartner Jake) Ruby) (= (TomPartner Jake) Spot) (= (TomPartner Jake) Starbuck))
    (or (= (TomPartner Dibii) Ruby) (= (TomPartner Dibii) Spot) (= (TomPartner Dibii) Starbuck))
))
(assert (and
    (= (QueenPartner (TomPartner Batman)) Batman)
    (= (QueenPartner (TomPartner Jake)) Jake)
    (= (QueenPartner (TomPartner Dibii)) Dibii)))

; 1. Batman chose the female who liked to chase a ball, but she was not Starbuck.
(assert (= (QueenActivity (TomPartner Batman)) Ball))
(assert (not (= (TomPartner Batman) Starbuck)))

; 2. Dibii's companion liked to chase the laser light.
(assert (= (QueenActivity (TomPartner Dibii)) Lazer))

; 3. Ruby loved to cuddle up to her male for a long afternoon nap in the sun.
(assert (= (QueenActivity Ruby) Sleep))

; 4. Starbuck had two more kittens than Batman's companion.
(assert (and (= (QueenKittens Starbuck) ThreeKittens)
             (= (QueenKittens (TomPartner Batman)) OneKitten)))

(check-sat)

(echo "
Toms:")
(get-value (Batman Jake Dibii))

(echo "
Queens:")
(get-value (Ruby Spot Starbuck))

(echo "
Activities:")
(get-value (Lazer Sleep Ball))

(echo "
NumKittens:")
(get-value (OneKitten TwoKittens ThreeKittens))

(echo "
Spot:")
(get-value ((QueenPartner Spot)
            (QueenKittens Spot)
            (QueenActivity Spot)))

(echo "
Ruby:")
(get-value ((QueenPartner Ruby)
            (QueenKittens Ruby)
            (QueenActivity Ruby)))

(echo "
Starbuck:")
(get-value ((QueenPartner Starbuck)
            (QueenKittens Starbuck)
            (QueenActivity Starbuck)))