; breakthrough
;
; a player wins if he reaches the opposite side of the board
; or if the opponent has no pieces left
;
; the game ends if one player wins (there is no draw)

(role white)
(role black)
(init (cellholds 1 1 white))
(init (cellholds 2 1 white))
(init (cellholds 3 1 white))
(init (cellholds 4 1 white))
(init (cellholds 5 1 white))
(init (cellholds 6 1 white))
(init (cellholds 7 1 white))
(init (cellholds 8 1 white))
(init (cellholds 1 2 white))
(init (cellholds 2 2 white))
(init (cellholds 3 2 white))
(init (cellholds 4 2 white))
(init (cellholds 5 2 white))
(init (cellholds 6 2 white))
(init (cellholds 7 2 white))
(init (cellholds 8 2 white))
(init (cellholds 1 7 black))
(init (cellholds 2 7 black))
(init (cellholds 3 7 black))
(init (cellholds 4 7 black))
(init (cellholds 5 7 black))
(init (cellholds 6 7 black))
(init (cellholds 7 7 black))
(init (cellholds 8 7 black))
(init (cellholds 1 8 black))
(init (cellholds 2 8 black))
(init (cellholds 3 8 black))
(init (cellholds 4 8 black))
(init (cellholds 5 8 black))
(init (cellholds 6 8 black))
(init (cellholds 7 8 black))
(init (cellholds 8 8 black))
(init (control white))
(<= (legal white (move ?x ?y1 ?x ?y2))
    (true (control white))
    (true (cellholds ?x ?y1 white))
    (++ ?y1 ?y2)
    (cellempty ?x ?y2))
(<= (legal white (move ?x1 ?y1 ?x2 ?y2))
    (true (control white))
    (true (cellholds ?x1 ?y1 white))
    (++ ?y1 ?y2)
    (++ ?x1 ?x2)
    (not (true (cellholds ?x2 ?y2 white))))
(<= (legal white (move ?x1 ?y1 ?x2 ?y2))
    (true (control white))
    (true (cellholds ?x1 ?y1 white))
    (++ ?y1 ?y2)
    (++ ?x2 ?x1)
    (not (true (cellholds ?x2 ?y2 white))))
(<= (legal black (move ?x ?y1 ?x ?y2))
    (true (control black))
    (true (cellholds ?x ?y1 black))
    (++ ?y2 ?y1)
    (cellempty ?x ?y2))
(<= (legal black (move ?x1 ?y1 ?x2 ?y2))
    (true (control black))
    (true (cellholds ?x1 ?y1 black))
    (++ ?y2 ?y1)
    (++ ?x1 ?x2)
    (not (true (cellholds ?x2 ?y2 black))))
(<= (legal black (move ?x1 ?y1 ?x2 ?y2))
    (true (control black))
    (true (cellholds ?x1 ?y1 black))
    (++ ?y2 ?y1)
    (++ ?x2 ?x1)
    (not (true (cellholds ?x2 ?y2 black))))
(<= (legal white noop)
    (true (control black)))
(<= (legal black noop)
    (true (control white)))
(<= (next (cellholds ?x2 ?y2 ?player))
    (role ?player)
    (does ?player (move ?x1 ?y1 ?x2 ?y2)))
(<= (next (cellholds ?x3 ?y3 ?state))
    (true (cellholds ?x3 ?y3 ?state))
    (role ?player)
    (does ?player (move ?x1 ?y1 ?x2 ?y2))
    (distinctcell ?x1 ?y1 ?x3 ?y3)
    (distinctcell ?x2 ?y2 ?x3 ?y3))
(<= (next (control white))
    (true (control black)))
(<= (next (control black))
    (true (control white)))
(<= terminal
    whitewin)
(<= terminal
    blackwin)
(<= (goal white 100)
    whitewin)
(<= (goal white 0)
    (not whitewin))
(<= (goal black 100)
    blackwin)
(<= (goal black 0)
    (not blackwin))
(<= (cell ?x ?y)
    (index ?x)
    (index ?y))
(<= (cellempty ?x ?y)
    (cell ?x ?y)
    (not (true (cellholds ?x ?y white)))
    (not (true (cellholds ?x ?y black))))
(<= (distinctcell ?x1 ?y1 ?x2 ?y2)
    (cell ?x1 ?y1)
    (cell ?x2 ?y2)
    (distinct ?x1 ?x2))
(<= (distinctcell ?x1 ?y1 ?x2 ?y2)
    (cell ?x1 ?y1)
    (cell ?x2 ?y2)
    (distinct ?y1 ?y2))
(<= whitewin
    (index ?x)
    (true (cellholds ?x 8 white)))
(<= whitewin
    (not blackcell))
(<= blackwin
    (index ?x)
    (true (cellholds ?x 1 black)))
(<= blackwin
    (not whitecell))
(<= whitecell
    (cell ?x ?y)
    (true (cellholds ?x ?y white)))
(<= blackcell
    (cell ?x ?y)
    (true (cellholds ?x ?y black)))
(index 1)
(index 2)
(index 3)
(index 4)
(index 5)
(index 6)
(index 7)
(index 8)
(++ 1 2)
(++ 2 3)
(++ 3 4)
(++ 4 5)
(++ 5 6)
(++ 6 7)
(++ 7 8)