; f:fox, g:goose, b:beans
; l: left bank, r: right bank, b: on boat

(declare-const fl Bool)
(declare-const fb Bool)
(declare-const fr Bool)

(declare-const gl Bool)
(declare-const gb Bool)
(declare-const gr Bool)

(declare-const bl Bool)
(declare-const bb Bool)
(declare-const br Bool)



; initial setup

(assert fl)
(assert gl)
(assert bl)

; ... more to do in the initial setup

; move 1


(declare-const fl1 Bool)
(declare-const fb1 Bool)
(declare-const fr1 Bool)

(declare-const gl1 Bool)
(declare-const gb1 Bool)
(declare-const gr1 Bool)

(declare-const bl1 Bool)
(declare-const bb1 Bool)
(declare-const br1 Bool)

; fox, goose, and beans will end up in precisely one location


(assert (xor fl1 fb1 fr1))
(assert (xor gl1 gb1 gr1))
(assert (xor bl1 bb1 br1))
(assert (not (and bl1 bb1 br1)))
(assert (not (and fl1 fb1 fr1)))
(assert (not (and gl1 gb1 gr1)))

; constraints for preventaion of carnage 

(assert (not (and fl1 gl1)))
(assert (not (and gl1 bl1)))
(assert (or (and fr1 gr1 br1)         ; we are done!
           (and (not (and fr1 gr1))
                (not (and gr1 br1)))))

; only one item on the boat


(assert (=> fb1 (and (not gb1) (not bb1))))
(assert (=> gb1 (and (not fb1) (not bb1))))
(assert (=> bb1 (and (not gb1) (not fb1))))

; moves 

(assert (=> fl (or fl1 fb1)))
(assert (=> fr (or fr1 fb1)))
(assert (=> fb (or fb1 fl1 fr1)))


(assert (=> gl (or gl1 gb1)))
(assert (=> gr (or gr1 gb1)))
(assert (=> gb (or gb1 gl1 gr1)))


(assert (=> bl (or bl1 bb1)))
(assert (=> br (or br1 bb1)))
(assert (=> bb (or bb1 bl1 br1)))

; move 2


(declare-const fl2 Bool)
(declare-const fb2 Bool)
(declare-const fr2 Bool)

(declare-const gl2 Bool)
(declare-const gb2 Bool)
(declare-const gr2 Bool)

(declare-const bl2 Bool)
(declare-const bb2 Bool)
(declare-const br2 Bool)

;consistency

(assert (xor fl2 fb2 fr2))
(assert (xor gl2 gb2 gr2))
(assert (xor bl2 bb2 br2))
(assert (not (and bl2 bb2 br2)))
(assert (not (and fl2 fb2 fr2)))
(assert (not (and gl2 gb2 gr2)))

(assert (=> fb2 (and (not gb2) (not bb2))))
(assert (=> gb2 (and (not fb2) (not bb2))))
(assert (=> bb2 (and (not gb2) (not fb2))))

; preventaion of carnage

(assert (not (and fl2 gl2)))
(assert (not (and gl2 bl2)))
(assert (or (and fr2 gr2 br2)
           (and (not (and fr2 gr2))
                (not (and gr2 br2)))))

; possible moves

(assert (=> fl1 (or fl2 fb2)))
(assert (=> fb1 (or fb2 fl2 fr2)))
(assert (=> fr1 (or fr2 fb2)))

(assert (=> gl1 (or gl2 gb2)))
(assert (=> gb1 (or gb2 gl2 gr2)))
(assert (=> gr1 (or gr2 gb2)))

(assert (=> bl1 (or bl2 bb2)))
(assert (=> bb1 (or bb2 bl2 br2)))
(assert (=> br1 (or br2 bb2)))

; move 3


(declare-const fl3 Bool)
(declare-const fb3 Bool)
(declare-const fr3 Bool)

(declare-const gl3 Bool)
(declare-const gb3 Bool)
(declare-const gr3 Bool)

(declare-const bl3 Bool)
(declare-const bb3 Bool)
(declare-const br3 Bool)

;consistency

(assert (xor fl3 fb3 fr3))
(assert (xor gl3 gb3 gr3))
(assert (xor bl3 bb3 br3))
(assert (not (and bl3 bb3 br3)))
(assert (not (and fl3 fb3 fr3)))
(assert (not (and gl3 gb3 gr3)))

(assert (=> fb3 (and (not gb3) (not bb3))))
(assert (=> gb3 (and (not fb3) (not bb3))))
(assert (=> bb3 (and (not gb3) (not fb3))))

; preventaion of carnage

(assert (not (and fl3 gl3)))
(assert (not (and gl3 bl3)))
(assert (or (and fr3 gr3 br3)
           (and (not (and fr3 gr3))
                (not (and gr3 br3)))))

; possible moves

(assert (=> fl2 (or fl3 fb3)))
(assert (=> fb2 (or fb3 fl3 fr3)))
(assert (=> fr2 (or fr3 fb3)))

(assert (=> gl2 (or gl3 gb3)))
(assert (=> gb2 (or gb3 gl3 gr3)))
(assert (=> gr2 (or gr3 gb3)))

(assert (=> bl2 (or bl3 bb3)))
(assert (=> bb2 (or bb3 bl3 br3)))
(assert (=> br2 (or br3 bb3)))

; move 4


(declare-const fl4 Bool)
(declare-const fb4 Bool)
(declare-const fr4 Bool)

(declare-const gl4 Bool)
(declare-const gb4 Bool)
(declare-const gr4 Bool)

(declare-const bl4 Bool)
(declare-const bb4 Bool)
(declare-const br4 Bool)

;consistency

(assert (xor fl4 fb4 fr4))
(assert (xor gl4 gb4 gr4))
(assert (xor bl4 bb4 br4))
(assert (not (and bl4 bb4 br4)))
(assert (not (and fl4 fb4 fr4)))
(assert (not (and gl4 gb4 gr4)))

(assert (=> fb4 (and (not gb4) (not bb4))))
(assert (=> gb4 (and (not fb4) (not bb4))))
(assert (=> bb4 (and (not gb4) (not fb4))))

; preventaion of carnage

(assert (not (and fl4 gl4)))
(assert (not (and gl4 bl4)))
(assert (or (and fr4 gr4 br4)
           (and (not (and fr4 gr4))
                (not (and gr4 br4)))))

; possible moves

(assert (=> fl3 (or fl4 fb4)))
(assert (=> fb3 (or fb4 fl4 fr4)))
(assert (=> fr3 (or fr4 fb4)))

(assert (=> gl3 (or gl4 gb4)))
(assert (=> gb3 (or gb4 gl4 gr4)))
(assert (=> gr3 (or gr4 gb4)))

(assert (=> bl3 (or bl4 bb4)))
(assert (=> bb3 (or bb4 bl4 br4)))
(assert (=> br3 (or br4 bb4)))

; move 5


(declare-const fl5 Bool)
(declare-const fb5 Bool)
(declare-const fr5 Bool)

(declare-const gl5 Bool)
(declare-const gb5 Bool)
(declare-const gr5 Bool)

(declare-const bl5 Bool)
(declare-const bb5 Bool)
(declare-const br5 Bool)

;consistency

(assert (xor fl5 fb5 fr5))
(assert (xor gl5 gb5 gr5))
(assert (xor bl5 bb5 br5))
(assert (not (and bl5 bb5 br5)))
(assert (not (and fl5 fb5 fr5)))
(assert (not (and gl5 gb5 gr5)))

(assert (=> fb5 (and (not gb5) (not bb5))))
(assert (=> gb5 (and (not fb5) (not bb5))))
(assert (=> bb5 (and (not gb5) (not fb5))))

; preventaion of carnage

(assert (not (and fl5 gl5)))
(assert (not (and gl5 bl5)))
(assert (or (and fr5 gr5 br5)
           (and (not (and fr5 gr5))
                (not (and gr5 br5)))))

; possible moves

(assert (=> fl4 (or fl5 fb5)))
(assert (=> fb4 (or fb5 fl5 fr5)))
(assert (=> fr4 (or fr5 fb5)))

(assert (=> gl4 (or gl5 gb5)))
(assert (=> gb4 (or gb5 gl5 gr5)))
(assert (=> gr4 (or gr5 gb5)))

(assert (=> bl4 (or bl5 bb5)))
(assert (=> bb4 (or bb5 bl5 br5)))
(assert (=> br4 (or br5 bb5)))

; move 6


(declare-const fl6 Bool)
(declare-const fb6 Bool)
(declare-const fr6 Bool)

(declare-const gl6 Bool)
(declare-const gb6 Bool)
(declare-const gr6 Bool)

(declare-const bl6 Bool)
(declare-const bb6 Bool)
(declare-const br6 Bool)

;consistency

(assert (xor fl6 fb6 fr6))
(assert (xor gl6 gb6 gr6))
(assert (xor bl6 bb6 br6))
(assert (not (and bl6 bb6 br6)))
(assert (not (and fl6 fb6 fr6)))
(assert (not (and gl6 gb6 gr6)))

(assert (=> fb6 (and (not gb6) (not bb6))))
(assert (=> gb6 (and (not fb6) (not bb6))))
(assert (=> bb6 (and (not gb6) (not fb6))))

; preventaion of carnage

(assert (not (and fl6 gl6)))
(assert (not (and gl6 bl6)))
(assert (or (and fr6 gr6 br6)
           (and (not (and fr6 gr6))
                (not (and gr6 br6)))))

; possible moves

(assert (=> fl5 (or fl6 fb6)))
(assert (=> fb5 (or fb6 fl6 fr6)))
(assert (=> fr5 (or fr6 fb6)))

(assert (=> gl5 (or gl6 gb6)))
(assert (=> gb5 (or gb6 gl6 gr6)))
(assert (=> gr5 (or gr6 gb6)))

(assert (=> bl5 (or bl6 bb6)))
(assert (=> bb5 (or bb6 bl6 br6)))
(assert (=> br5 (or br6 bb6)))

; goal 

(assert (and fr5 gr5 br5))

(check-sat)
(get-model)