You are not logged in. login register
Game checkers-mustjump-torus
name checkers-mustjump-torus
creator admin
number of roles 2
stylesheet checkers/checkers.xsl
GDL v1
enabled
matches show matches
statistics show game statistics
description

Game Description

;*******************************************************************************
;* checkers-mustjump.kif                                                       *
;*                                                                             *
;* Last revision 7/12/06 by Nat Love                                           *
;* In this version, you have to jump if you have a jump.                       *
;*******************************************************************************

(role white)
(role black)

;*******************************************************************************
;* Initial state.                                                              *
;* Letters are columns: row c1 is WHITE side, row c8 is BLACK                  *
;* Numbers are rows:    column a is left, h is right (from white side)         *
;*******************************************************************************

(init (cell a c1 b))
(init (cell a c3 b))
(init (cell a c4 b))
(init (cell a c5 b))
(init (cell a c7 b))

(init (cell b c2 b))
(init (cell b c4 b))
(init (cell b c5 b))
(init (cell b c6 b))
(init (cell b c8 b))

(init (cell c c1 b))
(init (cell c c3 b))
(init (cell c c4 b))
(init (cell c c5 b))
(init (cell c c7 b))

(init (cell d c2 b))
(init (cell d c4 b))
(init (cell d c5 b))
(init (cell d c6 b))
(init (cell d c8 b))

(init (cell e c1 b))
(init (cell e c3 b))
(init (cell e c4 b))
(init (cell e c5 b))
(init (cell e c7 b))

(init (cell f c2 b))
(init (cell f c4 b))
(init (cell f c5 b))
(init (cell f c6 b))
(init (cell f c8 b))

(init (cell g c1 b))
(init (cell g c3 b))
(init (cell g c4 b))
(init (cell g c5 b))
(init (cell g c7 b))

(init (cell h c2 b))
(init (cell h c4 b))
(init (cell h c5 b))
(init (cell h c6 b))
(init (cell h c8 b))
 (init (cell a c2 wp))
 (init (cell b c1 wp))
 (init (cell c c2 wp))
 (init (cell d c1 wp))
 (init (cell e c2 wp))
 (init (cell f c1 wp))
 (init (cell g c2 wp))
 (init (cell h c1 wp))
 (init (cell b c3 wp))
 (init (cell d c3 wp))
 (init (cell f c3 wp))
 (init (cell h c3 wp))
 (init (cell a c8 bp))
 (init (cell c c8 bp))
 (init (cell e c8 bp))
 (init (cell g c8 bp))
 (init (cell h c7 bp))
 (init (cell f c7 bp))
 (init (cell d c7 bp))
 (init (cell b c7 bp))
 (init (cell a c6 bp))
 (init (cell c c6 bp))
 (init (cell e c6 bp))
 (init (cell g c6 bp))

(init (control white))
(init (step c1))

(init (piece_count white c12))
(init (piece_count black c12))

; End initial state

;*******************************************************************************
;* NEXT STATE AXIOMS: REGULAR MOVES                                            *
;*******************************************************************************

; MOVE SOURCE
; Piece ?p moves out of ?u ?v leaving square blank
(<= (next (cell ?u ?v b))
    (does ?player (move ?p ?u ?v ?x ?y)))

(<= (next (cell ?u ?v b))
    (does ?player (doublejump ?p ?u ?v ?x ?y ?x3 ?y3)))

(<= (next (cell ?u ?v b))
    (does ?player (triplejump ?p ?u ?v ?x ?y ?x3 ?y3 ?x4 ?y4)))

; MOVE DESTINATION: NON-KINGING MOVE
; Piece ?p moves to ?x ?y
(<= (next (cell ?x ?y ?p))
    (does ?player (move ?p ?u ?v ?x ?y))
    (or (distinct ?p wp) (distinct ?y c8))
    (or (distinct ?p bp) (distinct ?y c1)))

(<= (next (cell ?x ?y ?p))
    (does ?player (doublejump ?p ?u ?v ?x3 ?y3 ?x ?y))
    (or (distinct ?p wp) (distinct ?y c8))
    (or (distinct ?p bp) (distinct ?y c1)))

(<= (next (cell ?x ?y ?p))
    (does ?player (triplejump ?p ?u ?v ?x3 ?y3 ?x4 ?y4 ?x ?y))
    (or (distinct ?p wp) (distinct ?y c8))
    (or (distinct ?p bp) (distinct ?y c1)))

; UNDISTURBED CELL: NON-CAPTURE MOVE
; Piece (or blank) ?p at ?x ?y remains unchanged if:
; c1) This move is not a capture
; c2) ?x ?y is a different cell from the move source cell
; c3) ?x ?y is a different cell from the move destination cell
(<= (next (cell ?x ?y ?p))
    (does ?player (move ?piece ?x1 ?y1 ?x2 ?y2))
    (true (cell ?x ?y ?p))
    (not (single_jump_capture ?player ?x1 ?y1 ?x ?y ?x2 ?y2))
    (different_cells ?x ?y ?x1 ?y1)
    (different_cells ?x ?y ?x2 ?y2))

(<= (next (cell ?x ?y ?p))
    (does ?player (doublejump ?piece ?x1 ?y1 ?x2 ?y2 ?x3 ?y3))
    (true (cell ?x ?y ?p))
    (not (single_jump_capture ?player ?x1 ?y1 ?x ?y ?x2 ?y2))
    (not (single_jump_capture ?player ?x2 ?y2 ?x ?y ?x3 ?y3))
    (different_cells ?x ?y ?x1 ?y1)
    (different_cells ?x ?y ?x3 ?y3))

(<= (next (cell ?x ?y ?p))
    (does ?player (triplejump ?piece ?x1 ?y1 ?x2 ?y2 ?x3 ?y3 ?x4 ?y4))
    (true (cell ?x ?y ?p))
    (not (single_jump_capture ?player ?x1 ?y1 ?x ?y ?x2 ?y2))
    (not (single_jump_capture ?player ?x2 ?y2 ?x ?y ?x3 ?y3))
    (not (single_jump_capture ?player ?x3 ?y3 ?x ?y ?x4 ?y4))
    (different_cells ?x ?y ?x1 ?y1)
    (different_cells ?x ?y ?x4 ?y4))
    
; CAPTURED CELL (single jump)
(<= (next (cell ?x ?y b))
	(does ?player (move ?piece ?x1 ?y1 ?x2 ?y2))
	(single_jump_capture ?player ?x1 ?y1 ?x ?y ?x2 ?y2))

; CAPTURED CELL (double jump)
(<= (next (cell ?x ?y b))
    (does ?player (doublejump ?piece ?x1 ?y1 ?x2 ?y2 ?x3 ?y3))
    (or (single_jump_capture ?player ?x1 ?y1 ?x ?y ?x2 ?y2)
        (single_jump_capture ?player ?x2 ?y2 ?x ?y ?x3 ?y3)))

; CAPTURED CELL (triple jump)
(<= (next (cell ?x ?y b))
    (does ?player (triplejump ?piece ?x1 ?y1 ?x2 ?y2 ?x3 ?y3 ?x4 ?y4))
    (or (single_jump_capture ?player ?x1 ?y1 ?x ?y ?x2 ?y2)
        (single_jump_capture ?player ?x2 ?y2 ?x ?y ?x3 ?y3)
        (single_jump_capture ?player ?x3 ?y3 ?x ?y ?x4 ?y4)))

; CONTROL TRANSFER
(<= (next (control white))
    (true (control black)))
(<= (next (control black))
    (true (control white)))

; MOVE COUNT
(<= (next (step ?y))
    (true (step ?x))
    (succ ?x ?y))

;*******************************************************************************
;* NEXT STATE AXIOMS: SPECIAL MOVES                                            *
;*******************************************************************************

; MOVE DESTINATION: KINGING MOVE
(<= (next (cell ?x c8 wk))
    (does white (move wp ?u ?v ?x c8)))
(<= (next (cell ?x c1 bk))
    (does black (move bp ?u ?v ?x c1)))
    
(<= (next (cell ?x c8 wk))
    (does white (doublejump wp ?u ?v ?x3 ?y3 ?x c8)))
(<= (next (cell ?x c1 bk))
    (does black (doublejump bp ?u ?v ?x3 ?y3 ?x c1)))

(<= (next (cell ?x c8 wk))
    (does white (triplejump ?p ?u ?v ?x3 ?y3 ?x4 ?y4 ?x c8)))
(<= (next (cell ?x c1 bk))
    (does black (triplejump ?p ?u ?v ?x3 ?y3 ?x4 ?y4 ?x c1)))

;; NEXT for PIECE COUNTER
(<= (next (piece_count ?player ?n))
    (or (does ?player (move ?p ?u ?v ?x ?y))
        (does ?player (doublejump ?p ?u ?v ?x3 ?y3 ?x ?y))
        (does ?player (triplejump ?p ?u ?v ?x3 ?y3 ?x4 ?y4 ?x ?y)))
    (true (piece_count ?player ?n)))

(<= (next (piece_count white ?n))
    (does black (move ?p ?x1 ?y1 ?x2 ?y2))
    (kingmove black ?x1 ?y1 ?x2 ?y2)
    (true (piece_count white ?n)))

(<= (next (piece_count white ?lower))
    (does black (move ?p ?x1 ?y1 ?x2 ?y2))
    (single_jump_capture black ?x1 ?y1 ?x ?y ?x2 ?y2)
    (true (piece_count white ?higher))
    (minus1 ?higher ?lower))

(<= (next (piece_count white ?lower))
    (does black (doublejump ?p ?u ?v ?x3 ?y3 ?x ?y))
    (true (piece_count white ?higher))
    (minus2 ?higher ?lower))

(<= (next (piece_count white ?lower))
    (does black (triplejump ?p ?u ?v ?x3 ?y3 ?x4 ?y4 ?x ?y))
    (true (piece_count white ?higher))
    (minus3 ?higher ?lower))

(<= (next (piece_count black ?n))
    (does white (move ?p ?x1 ?y1 ?x2 ?y2))
    (kingmove white ?x1 ?y1 ?x2 ?y2)
    (true (piece_count black ?n)))

(<= (next (piece_count black ?lower))
    (does white (move ?p ?x1 ?y1 ?x2 ?y2))
    (single_jump_capture white ?x1 ?y1 ?x ?y ?x2 ?y2)
    (true (piece_count black ?higher))
    (minus1 ?higher ?lower))

(<= (next (piece_count black ?lower))
    (does white (doublejump ?p ?u ?v ?x3 ?y3 ?x ?y))
    (true (piece_count black ?higher))
    (minus2 ?higher ?lower))

(<= (next (piece_count black ?lower))
    (does white (triplejump ?p ?u ?v ?x3 ?y3 ?x4 ?y4 ?x ?y))
    (true (piece_count black ?higher))
    (minus3 ?higher ?lower))

; End next state axioms

;*******************************************************************************
;* LEGAL MOVES and their auxilliary axioms                                     *
;*******************************************************************************

; Legal Move when you are not jumping (pawn):
(<= (legal ?player (move ?piece ?u ?v ?x ?y))
    (true (control ?player))
    (piece_owner_type ?piece ?player pawn)
    (true (cell ?u ?v ?piece))
    (not (singlejumpavailable ?player))
    (pawnmove ?player ?u ?v ?x ?y)
    (true (cell ?x ?y b)))

; Legal Move when you are not jumping (king):
(<= (legal ?player (move ?piece ?u ?v ?x ?y))
    (true (control ?player))
    (piece_owner_type ?piece ?player king)
    (true (cell ?u ?v ?piece))
    (not (singlejumpavailable ?player))
    (kingmove ?player ?u ?v ?x ?y)
    (true (cell ?x ?y b)))

; Legal Move when you are single jumping (pawn):
(<= (legal ?player (move ?piece ?u ?v ?x ?y))
    (true (control ?player))
    (piece_owner_type ?piece ?player pawn)
    (true (cell ?u ?v ?piece))
    (not (doublejumpavailable ?player))
    (pawnjump ?player ?u ?v ?x ?y)
    (true (cell ?x ?y b))
    (single_jump_capture ?player ?u ?v ?c ?d ?x ?y))

; Legal Move when you are single jumping (king):
(<= (legal ?player (move ?piece ?u ?v ?x ?y))
    (true (control ?player))
    (piece_owner_type ?piece ?player king)
    (true (cell ?u ?v ?piece))
    (not (doublejumpavailable ?player))
    (kingjump ?player ?u ?v ?x ?y)
    (true (cell ?x ?y b))
    (single_jump_capture ?player ?u ?v ?c ?d ?x ?y))

; Legal Move when you are double jumping (pawn):
(<= (legal ?player (doublejump ?piece ?u ?v ?x1 ?y1 ?x2 ?y2))
    (true (control ?player))
    (piece_owner_type ?piece ?player pawn)
    (true (cell ?u ?v ?piece))
    (not (triplejumpavailable ?player))
    (pawnjump ?player ?u ?v ?x1 ?y1)
    (true (cell ?x1 ?y1 b))
    (pawnjump ?player ?x1 ?y1 ?x2 ?y2)
    (true (cell ?x2 ?y2 b))
    (different_cells ?u ?v ?x2 ?y2)
    (single_jump_capture ?player ?u ?v ?c ?d ?x1 ?y1)
    (single_jump_capture ?player ?x1 ?y1 ?c1 ?d1 ?x2 ?y2))

; Legal Move when you are double jumping (king):
(<= (legal ?player (doublejump ?piece ?u ?v ?x1 ?y1 ?x2 ?y2))
    (true (control ?player))
    (piece_owner_type ?piece ?player king)
    (true (cell ?u ?v ?piece))
    (not (triplejumpavailable ?player))
    (kingjump ?player ?u ?v ?x1 ?y1)
    (true (cell ?x1 ?y1 b))
    (kingjump ?player ?x1 ?y1 ?x2 ?y2)
    (true (cell ?x2 ?y2 b))
    (different_cells ?u ?v ?x2 ?y2)
    (single_jump_capture ?player ?u ?v ?c ?d ?x1 ?y1)
    (single_jump_capture ?player ?x1 ?y1 ?c1 ?d1 ?x2 ?y2))

; Legal Move when you are triple jumping (pawn):
(<= (legal ?player (triplejump ?piece ?u ?v ?x1 ?y1 ?x2 ?y2 ?x3 ?y3))
    (true (control ?player))
    (piece_owner_type ?piece ?player pawn)
    (true (cell ?u ?v ?piece))
    (pawnjump ?player ?u ?v ?x1 ?y1)
    (true (cell ?x1 ?y1 b))
    (pawnjump ?player ?x1 ?y1 ?x2 ?y2)
    (true (cell ?x2 ?y2 b))
    (different_cells ?u ?v ?x2 ?y2)
    (pawnjump ?player ?x2 ?y2 ?x3 ?y3)
    (true (cell ?x3 ?y3 b))
    (different_cells ?x1 ?y1 ?x3 ?y3)
    (single_jump_capture ?player ?u ?v ?c ?d ?x1 ?y1)
    (single_jump_capture ?player ?x1 ?y1 ?c1 ?d1 ?x2 ?y2)
    (single_jump_capture ?player ?x2 ?y2 ?c2 ?d2 ?x3 ?y3))

; Legal Move when you are triple jumping (king):
(<= (legal ?player (triplejump ?piece ?u ?v ?x1 ?y1 ?x2 ?y2 ?x3 ?y3))
    (true (control ?player))
    (piece_owner_type ?piece ?player king)
    (true (cell ?u ?v ?piece))
    (kingjump ?player ?u ?v ?x1 ?y1)
    (true (cell ?x1 ?y1 b))
    (kingjump ?player ?x1 ?y1 ?x2 ?y2)
    (true (cell ?x2 ?y2 b))
    (different_cells ?u ?v ?x2 ?y2)
    (kingjump ?player ?x2 ?y2 ?x3 ?y3)
    (true (cell ?x3 ?y3 b))
    (different_cells ?x1 ?y1 ?x3 ?y3)
    (single_jump_capture ?player ?u ?v ?c ?d ?x1 ?y1)
    (single_jump_capture ?player ?x1 ?y1 ?c1 ?d1 ?x2 ?y2)
    (single_jump_capture ?player ?x2 ?y2 ?c2 ?d2 ?x3 ?y3))

; NO-OPs for player not moving
(<= (legal white noop)
    (true (control black)))
(<= (legal black noop)
    (true (control white)))

; Need relations to determine whether or not you have jumps available.

(<= (singlejumpavailable ?player)
    (piece_owner_type ?piece ?player pawn)
    (true (cell ?u ?v ?piece))
    (pawnjump ?player ?u ?v ?x ?y)
    (true (cell ?x ?y b))
    (single_jump_capture ?player ?u ?v ?c ?d ?x ?y))

(<= (singlejumpavailable ?player)
    (piece_owner_type ?piece ?player king)
    (true (cell ?u ?v ?piece))
    (kingjump ?player ?u ?v ?x ?y)
    (true (cell ?x ?y b))
    (single_jump_capture ?player ?u ?v ?c ?d ?x ?y))

(<= (doublejumpavailable ?player)
    (piece_owner_type ?piece ?player pawn)
    (true (cell ?u ?v ?piece))
    (pawnjump ?player ?u ?v ?x1 ?y1)
    (true (cell ?x1 ?y1 b))
    (pawnjump ?player ?x1 ?y1 ?x2 ?y2)
    (true (cell ?x2 ?y2 b))
    (different_cells ?u ?v ?x2 ?y2)
    (single_jump_capture ?player ?u ?v ?c ?d ?x1 ?y1)
    (single_jump_capture ?player ?x1 ?y1 ?c1 ?d1 ?x2 ?y2))

(<= (doublejumpavailable ?player)
    (piece_owner_type ?piece ?player king)
    (true (cell ?u ?v ?piece))
    (kingjump ?player ?u ?v ?x1 ?y1)
    (true (cell ?x1 ?y1 b))
    (kingjump ?player ?x1 ?y1 ?x2 ?y2)
    (true (cell ?x2 ?y2 b))
    (different_cells ?u ?v ?x2 ?y2)
    (single_jump_capture ?player ?u ?v ?c ?d ?x1 ?y1)
    (single_jump_capture ?player ?x1 ?y1 ?c1 ?d1 ?x2 ?y2))

(<= (triplejumpavailable ?player)
    (piece_owner_type ?piece ?player pawn)
    (true (cell ?u ?v ?piece))
    (pawnjump ?player ?u ?v ?x1 ?y1)
    (true (cell ?x1 ?y1 b))
    (pawnjump ?player ?x1 ?y1 ?x2 ?y2)
    (true (cell ?x2 ?y2 b))
    (different_cells ?u ?v ?x2 ?y2)
    (pawnjump ?player ?x2 ?y2 ?x3 ?y3)
    (true (cell ?x3 ?y3 b))
    (different_cells ?x1 ?y1 ?x3 ?y3)
    (single_jump_capture ?player ?u ?v ?c ?d ?x1 ?y1)
    (single_jump_capture ?player ?x1 ?y1 ?c1 ?d1 ?x2 ?y2)
    (single_jump_capture ?player ?x2 ?y2 ?c2 ?d2 ?x3 ?y3))

(<= (triplejumpavailable ?player)
    (piece_owner_type ?piece ?player king)
    (true (cell ?u ?v ?piece))
    (kingjump ?player ?u ?v ?x1 ?y1)
    (true (cell ?x1 ?y1 b))
    (kingjump ?player ?x1 ?y1 ?x2 ?y2)
    (true (cell ?x2 ?y2 b))
    (different_cells ?u ?v ?x2 ?y2)
    (kingjump ?player ?x2 ?y2 ?x3 ?y3)
    (true (cell ?x3 ?y3 b))
    (different_cells ?x1 ?y1 ?x3 ?y3)
    (single_jump_capture ?player ?u ?v ?c ?d ?x1 ?y1)
    (single_jump_capture ?player ?x1 ?y1 ?c1 ?d1 ?x2 ?y2)
    (single_jump_capture ?player ?x2 ?y2 ?c2 ?d2 ?x3 ?y3))
    
; pawnmove

(<= (pawnmove white ?u ?v ?x ?y)
    (next_rank ?v ?y)
    (or (next_file ?u ?x) (next_file ?x ?u)))
	
(<= (pawnmove black ?u ?v ?x ?y)
    (next_rank ?y ?v)
    (or (next_file ?u ?x) (next_file ?x ?u)))

; kingmove is a pawnmove by any player

(<= (kingmove ?player ?u ?v ?x ?y)
    (role ?player)
    (role ?player2)
    (pawnmove ?player2 ?u ?v ?x ?y))

; pawnjump

(<= (pawnjump white ?u ?v ?x ?y)
    (next_rank ?v ?v1)
    (next_rank ?v1 ?y)
    (next_file ?u ?x1)
    (next_file ?x1 ?x))

(<= (pawnjump white ?u ?v ?x ?y)
    (next_rank ?v ?v1)
    (next_rank ?v1 ?y)
    (next_file ?x ?x1)
    (next_file ?x1 ?u))

(<= (pawnjump black ?u ?v ?x ?y)
    (next_rank ?y ?v1)
    (next_rank ?v1 ?v)
    (next_file ?u ?x1)
    (next_file ?x1 ?x))

(<= (pawnjump black ?u ?v ?x ?y)
    (next_rank ?y ?v1)
    (next_rank ?v1 ?v)
    (next_file ?x ?x1)
    (next_file ?x1 ?u))

; kingjump is a pawnjump by any player

(<= (kingjump ?player ?u ?v ?x ?y)
    (role ?player)
    (role ?player2)
    (pawnjump ?player2 ?u ?v ?x ?y))

; single jump capture ?player means player is jumping from 
; u v to x y over c d, and an opponent's piece is at c d.

(<= (single_jump_capture ?player ?u ?v ?c ?d ?x ?y)
    (kingjump ?player ?u ?v ?x ?y)
    (kingmove ?player ?u ?v ?c ?d)
    (kingmove ?player ?c ?d ?x ?y)
    (true (cell ?c ?d ?piece))
    (opponent ?player ?opponent)
    (piece_owner_type ?piece ?opponent ?type))

;; Goals and Terminal
(<= (has_legal_move ?player)
    (piece_owner_type ?piece ?player ?type)
    (or (legal ?player (move ?piece ?u ?v ?x ?y))
   		(legal ?player (doublejump ?piece ?u ?v ?a ?b ?x ?y))
   		(legal ?player (triplejump ?piece ?u ?v ?a ?b ?c ?d ?x ?y))))

(<= (stuck ?player)
    (role ?player)
    (not (has_legal_move ?player)))

(<= terminal
    (true (control ?player))
    (stuck ?player))
	
(<= terminal
    (true (piece_count ?player c0)))

(<= terminal
    (true (step c50)))

;; In the case of a tie, we award black more points because
;; white gets to go last-- white has control on odd steps, and c99
;; will be the last move made.

(<= (goal white 45)
    (true (piece_count white ?x))
    (true (piece_count black ?x)))

(<= (goal black 55)
    (true (piece_count white ?x))
    (true (piece_count black ?x)))

(<= (goal black ?blackgoal)
    (true (piece_count white ?rc))
    (true (piece_count black ?bc))
    (maptogoals ?rc ?bc ?whitegoal ?blackgoal))

(<= (goal black ?blackgoal)
    (true (piece_count white ?rc))
    (true (piece_count black ?bc))
    (maptogoals ?bc ?rc ?blackgoal ?whitegoal))

(<= (goal white ?whitegoal)
    (true (piece_count white ?rc))
    (true (piece_count black ?bc))
    (maptogoals ?rc ?bc ?whitegoal ?blackgoal))

(<= (goal white ?whitegoal)
    (true (piece_count white ?rc))
    (true (piece_count black ?bc))
    (maptogoals ?bc ?rc ?blackgoal ?whitegoal))

;*******************************************************************************
; AUXILIARY PREDICATES                                                         *
;*******************************************************************************

;;;  DIFFERENT CELLS
;;;  True iff ?x1 ?y1 is a different cell from ?x2 ?y2

(<= (adjacent ?x1 ?x2)
    (next_file ?x1 ?x2))

(<= (adjacent ?x1 ?x2)
    (next_file ?x2 ?x1))

(<= (adjacent ?y1 ?y2)
    (next_rank ?y1 ?y2))

(<= (adjacent ?y1 ?y2)
    (next_rank ?y2 ?y1))

(<= (different_cells ?x1 ?y1 ?x2 ?y2)
    (distinct ?x1 ?x2)
    (coordinate ?x1)
    (coordinate ?x2)
    (coordinate ?y1)
    (coordinate ?y2))

(<= (different_cells ?x1 ?y1 ?x2 ?y2)
    (distinct ?y1 ?y2)
    (coordinate ?x1)
    (coordinate ?x2)
    (coordinate ?y1)
    (coordinate ?y2))

; PLAYER OPPONENTS
(opponent white black)
(opponent black white)

; PIECE OWNERSHIP AND TYPE 
(piece_owner_type wk white king)
(piece_owner_type wp white pawn)

(piece_owner_type bk black king)
(piece_owner_type bp black pawn)

; BOARD TOPOLOGY
(next_rank c1 c2)
(next_rank c2 c3)
(next_rank c3 c4)
(next_rank c4 c5)
(next_rank c5 c6)
(next_rank c6 c7)
(next_rank c7 c8)
(next_rank c8 c1)

(next_file a b)
(next_file b c)
(next_file c d)
(next_file d e)
(next_file e f)
(next_file f g)
(next_file g h)
(next_file h a)

; BOARD COORDINATES

(coordinate c1)
(coordinate c2)
(coordinate c3)
(coordinate c4)
(coordinate c5)
(coordinate c6)
(coordinate c7)
(coordinate c8)
(coordinate a)
(coordinate b)
(coordinate c)
(coordinate d)
(coordinate e)
(coordinate f)
(coordinate g)
(coordinate h)

(<= (greater ?a ?b)
    (succ ?b ?a))
(<= (greater ?a ?b)
    (distinct ?a ?b)
    (succ ?c ?a)
    (greater ?c ?b))

;; Mapping differentials to goals
;; Note that you can't have more than c12 pieces.

;; Winning by 5 or more
(maptogoals c12 c7 100 0)
(maptogoals c12 c6 100 0)
(maptogoals c12 c5 100 0)
(maptogoals c12 c4 100 0)
(maptogoals c12 c3 100 0)
(maptogoals c12 c2 100 0)
(maptogoals c12 c1 100 0)
(maptogoals c12 c0 100 0)
(maptogoals c11 c6 100 0)
(maptogoals c11 c5 100 0)
(maptogoals c11 c4 100 0)
(maptogoals c11 c3 100 0)
(maptogoals c11 c2 100 0)
(maptogoals c11 c1 100 0)
(maptogoals c11 c0 100 0)
(maptogoals c10 c5 100 0)
(maptogoals c10 c4 100 0)
(maptogoals c10 c3 100 0)
(maptogoals c10 c2 100 0)
(maptogoals c10 c1 100 0)
(maptogoals c10 c0 100 0)
(maptogoals c9 c4 100 0)
(maptogoals c9 c3 100 0)
(maptogoals c9 c2 100 0)
(maptogoals c9 c1 100 0)
(maptogoals c9 c0 100 0)
(maptogoals c8 c3 100 0)
(maptogoals c8 c2 100 0)
(maptogoals c8 c1 100 0)
(maptogoals c8 c0 100 0)
(maptogoals c7 c2 100 0)
(maptogoals c7 c1 100 0)
(maptogoals c7 c0 100 0)
(maptogoals c6 c1 100 0)
(maptogoals c6 c0 100 0)
(maptogoals c5 c0 100 0)

;; Winning by 4

(maptogoals c12 c8 90 10)
(maptogoals c11 c7 90 10)
(maptogoals c10 c6 90 10)
(maptogoals c9 c5 90 10)
(maptogoals c8 c4 90 10)
(maptogoals c7 c3 90 10)
(maptogoals c6 c2 90 10)
(maptogoals c5 c1 90 10)
(maptogoals c4 c0 90 10)

;; Winning by 3

(maptogoals c12 c9 80 20)
(maptogoals c11 c8 80 20)
(maptogoals c10 c7 80 20)
(maptogoals c9 c6 80 20)
(maptogoals c8 c5 80 20)
(maptogoals c7 c4 80 20)
(maptogoals c6 c3 80 20)
(maptogoals c5 c2 80 20)
(maptogoals c4 c1 80 20)
(maptogoals c3 c0 80 20)

;; Winning by 2

(maptogoals c12 c10 70 30)
(maptogoals c11 c9 70 30)
(maptogoals c10 c8 70 30)
(maptogoals c9 c7 70 30)
(maptogoals c8 c6 70 30)
(maptogoals c7 c5 70 30)
(maptogoals c6 c4 70 30)
(maptogoals c5 c3 70 30)
(maptogoals c4 c2 70 30)
(maptogoals c3 c1 70 30)
(maptogoals c2 c0 70 30)

;; Winning by 1

(maptogoals c12 c11 60 40)
(maptogoals c11 c10 60 40)
(maptogoals c10 c9 60 40)
(maptogoals c9 c8 60 40)
(maptogoals c8 c7 60 40)
(maptogoals c7 c6 60 40)
(maptogoals c6 c5 60 40)
(maptogoals c5 c4 60 40)
(maptogoals c4 c3 60 40)
(maptogoals c3 c2 60 40)
(maptogoals c2 c1 60 40)
(maptogoals c1 c0 60 40)


(minus3 c12 c9)
(minus3 c11 c8)
(minus3 c10 c7)
(minus3 c9 c6)
(minus3 c8 c5)
(minus3 c7 c4)
(minus3 c6 c3)
(minus3 c5 c2)
(minus3 c4 c1)
(minus3 c3 c0)
(minus2 c12 c10)
(minus2 c11 c9)
(minus2 c10 c8)
(minus2 c9 c7)
(minus2 c8 c6)
(minus2 c7 c5)
(minus2 c6 c4)
(minus2 c5 c3)
(minus2 c4 c2)
(minus2 c3 c1)
(minus2 c2 c0)
(minus1 c12 c11)
(minus1 c11 c10)
(minus1 c10 c9)
(minus1 c9 c8)
(minus1 c8 c7)
(minus1 c7 c6)
(minus1 c6 c5)
(minus1 c5 c4)
(minus1 c4 c3)
(minus1 c3 c2)
(minus1 c2 c1)
(minus1 c1 c0)


; MOVE COUNT SUCCESSOR
(succ c0 c1)
(succ c1 c2)
(succ c2 c3)
(succ c3 c4)
(succ c4 c5)
(succ c5 c6)
(succ c6 c7)
(succ c7 c8)
(succ c8 c9)
(succ c9 c10)
(succ c10 c11)
(succ c11 c12)
(succ c12 c13)
(succ c13 c14)
(succ c14 c15)
(succ c15 c16)
(succ c16 c17)
(succ c17 c18)
(succ c18 c19)
(succ c19 c20)
(succ c20 c21)
(succ c21 c22)
(succ c22 c23)
(succ c23 c24)
(succ c24 c25)
(succ c25 c26)
(succ c26 c27)
(succ c27 c28)
(succ c28 c29)
(succ c29 c30)
(succ c30 c31)
(succ c31 c32)
(succ c32 c33)
(succ c33 c34)
(succ c34 c35)
(succ c35 c36)
(succ c36 c37)
(succ c37 c38)
(succ c38 c39)
(succ c39 c40)
(succ c40 c41)
(succ c41 c42)
(succ c42 c43)
(succ c43 c44)
(succ c44 c45)
(succ c45 c46)
(succ c46 c47)
(succ c47 c48)
(succ c48 c49)
(succ c49 c50)
(succ c50 c51)
(succ c51 c52)
(succ c52 c53)
(succ c53 c54)
(succ c54 c55)
(succ c55 c56)
(succ c56 c57)
(succ c57 c58)
(succ c58 c59)
(succ c59 c60)
(succ c60 c61)
(succ c61 c62)
(succ c62 c63)
(succ c63 c64)
(succ c64 c65)
(succ c65 c66)
(succ c66 c67)
(succ c67 c68)
(succ c68 c69)
(succ c69 c70)
(succ c70 c71)
(succ c71 c72)
(succ c72 c73)
(succ c73 c74)
(succ c74 c75)
(succ c75 c76)
(succ c76 c77)
(succ c77 c78)
(succ c78 c79)
(succ c79 c80)
(succ c80 c81)
(succ c81 c82)
(succ c82 c83)
(succ c83 c84)
(succ c84 c85)
(succ c85 c86)
(succ c86 c87)
(succ c87 c88)
(succ c88 c89)
(succ c89 c90)
(succ c90 c91)
(succ c91 c92)
(succ c92 c93)
(succ c93 c94)
(succ c94 c95)
(succ c95 c96)
(succ c96 c97)
(succ c97 c98)
(succ c98 c99)
(succ c99 c100)
(succ c100 c101)
(succ c101 c102)
(succ c102 c103)

; END of checkers.kif

sees_XML(...) rules

(<= (sees_xml random ?t) (true ?t))
(<= (sees_xml ?p ?t) (role ?p) (distinct ?p random) (true ?t))