; The game has probably two bugs: ; 1. (sum 0 0 ?x) is not defined. ; 2. There are situations with two crissscores/2 fluents in a state. ;crisscross ; (role red) (role teal) (init (cell a3 red)) (init (cell a4 red)) (init (cell b3 red)) (init (cell b4 red)) (init (cell c1 teal)) (init (cell c2 teal)) (init (cell c3 blank)) (init (cell c4 blank)) (init (cell c5 blank)) (init (cell c6 blank)) (init (cell d1 teal)) (init (cell d2 teal)) (init (cell d3 blank)) (init (cell d4 blank)) (init (cell d5 blank)) (init (cell d6 blank)) (init (cell e3 blank)) (init (cell e4 blank)) (init (cell f3 blank)) (init (cell f4 blank)) (init (control red)) (init (first nobody)) (init (step 1)) (<= (next (cell ?e ?player)) (does ?player (move ?b ?e)) (not reseted)) (<= (next (cell ?b blank)) (does ?player (move ?b ?e)) (not reseted)) (<= (next (cell ?x ?z)) (true (cell ?x ?z)) (does ?player (move ?b ?e)) (distinct ?x ?b) (distinct ?x ?e) (not reseted)) (<= (next (cell ?x ?z)) (true (cell ?x ?z)) (does red noop) (does teal noop) (not reseted)) (<= (next (control teal)) (true (control red)) (not reseted)) (<= (next (control red)) (true (control teal)) (not reseted)) (<= (next (first red)) (stones red all) (not (stones teal all)) (not reseted)) (<= (next (first teal)) (stones teal all) (not (stones red all)) (not reseted)) (<= (next (first ?player)) (role ?player) (true (first ?player)) (not reseted)) (<= (next (step ?y)) (true (step ?x)) (succ ?x ?y) (not reseted)) (<= reseted (does ?player reset)) ; when reset occurs, next state is the init state of racetrack and the scores ; for crisscross (<= (next ?x) (init2 ?x) reseted) (<= (next (crissscores ?x ?y)) reseted (crissfinished ?x ?y)) (<= (next (crissscores ?x ?y)) (true (crissscores ?x ?y))) (<= crissscorz (true (crissscores ?x ?y))) (<= (legal ?player (move ?b ?e)) (true (control ?player)) (movable ?player ?b ?e) (not crissfin)) (<= (legal ?player noop) (true (control ?player2)) (distinct ?player ?player2) (role ?player) (not crissfin)) (<= (legal ?player noop) (true (control ?player)) (true (cell ?b1 ?player)) (stuck ?b1 ?player) (true (cell ?b2 ?player)) (distinct ?b1 ?b2) (stuck ?b2 ?player) (true (cell ?b3 ?player)) (distinct ?b2 ?b3) (distinct ?b3 ?b1) (stuck ?b3 ?player) (true (cell ?b4 ?player)) (distinct ?b1 ?b4) (distinct ?b2 ?b4) (distinct ?b3 ?b4) (stuck ?b4 ?player) (not crissfin)) (<= (legal ?player reset) (role ?player) crissfin) (<= (stuck ?b ?player) (not (movableplayer ?player ?b)) (role ?player) (location ?b)) (<= (movableplayer ?player ?b) (movable ?player ?b ?e)) (<= (movable ?player ?b ?e) (true (cell ?b ?player)) (car ?player ?b ?c) (true (cell ?c ?p1)) (distinct ?p1 blank) (car ?player ?c ?x) (true (cell ?x blank)) (car ?player ?x ?d) (true (cell ?d ?p2)) (distinct ?p2 blank) (car ?player ?d ?e) (true (cell ?e blank))) (<= (movable ?player ?b ?e) (true (cell ?b ?player)) (car ?player ?b ?c) (true (cell ?c ?p)) (distinct ?p blank) (car ?player ?c ?e) (true (cell ?e blank))) (<= (movable ?player ?b ?e) (true (cell ?b ?player)) (car ?player ?b ?e) (true (cell ?e blank))) (<= (car red ?b ?e) (carred ?b ?e)) (<= (car teal ?b ?e) (carteal ?b ?e)) (<= (crissgoal ?player 50) (true (first ?player))) (<= (crissgoal ?player 12) (stones ?player all) (true (first ?player2)) (distinct ?player ?player2)) (<= (crissgoal ?player 7) (stones ?player 75) (true (first ?player2)) (distinct ?player ?player2)) (<= (crissgoal ?player 5) (stones ?player 50) (true (first ?player2)) (distinct ?player ?player2)) (<= (crissgoal ?player 2) (stones ?player 25) (true (first ?player2)) (distinct ?player ?player2)) (<= (crissgoal ?player 0) (stones ?player 0) (true (first ?player2)) (distinct ?player ?player2)) (<= (crissgoal ?player 50) (true (step 40)) (stones ?player all) (not finished)) (<= (crissgoal ?player 38) (true (step 40)) (stones ?player 75) (not finished)) (<= (crissgoal ?player 25) (true (step 40)) (stones ?player 50) (not finished)) (<= (crissgoal ?player 12) (true (step 40)) (stones ?player 25) (not finished)) (<= (crissgoal ?player 0) (true (step 40)) (stones ?player 0) (not finished)) (<= finished (true (first ?player))) (<= (stones red ?payoff) (count e3 e4 f3 f4 red ?payoff)) (<= (stones teal ?payoff) (count c5 d5 c6 d6 teal ?payoff)) (<= (count ?x ?y ?z ?w ?player all) (true (cell ?x ?player)) (true (cell ?y ?player)) (true (cell ?z ?player)) (true (cell ?w ?player))) (<= (count ?x ?y ?z ?w ?player 75) (true (cell ?x ?player)) (devoid ?y ?player) (true (cell ?z ?player)) (true (cell ?w ?player))) (<= (count ?x ?y ?z ?w ?player 75) (devoid ?x ?player) (true (cell ?y ?player)) (true (cell ?z ?player)) (true (cell ?w ?player))) (<= (count ?x ?y ?z ?w ?player 50) (true (cell ?x ?player)) (true (cell ?y ?player)) (true (cell ?z ?player)) (devoid ?w ?player)) (<= (count ?x ?y ?z ?w ?player 50) (true (cell ?x ?player)) (true (cell ?y ?player)) (true (cell ?w ?player)) (devoid ?z ?player)) (<= (count ?x ?y ?z ?w ?player 25) (devoid ?x ?player) (devoid ?y ?player) (true (cell ?z ?player)) (true (cell ?w ?player))) (<= (count ?x ?y ?z ?w ?player 0) (devoid ?x ?player) (devoid ?z ?player) (location ?y) (location ?w)) (<= (count ?x ?y ?z ?w ?player 0) (devoid ?y ?player) (devoid ?z ?player) (location ?x) (location ?w)) (<= (count ?x ?y ?z ?w ?player 0) (devoid ?x ?player) (devoid ?w ?player) (location ?y) (location ?z)) (<= (count ?x ?y ?z ?w ?player 0) (devoid ?y ?player) (devoid ?w ?player) (location ?x) (location ?z)) (<= (count ?x ?y ?z ?w ?player 0) (devoid ?z ?player) (devoid ?w ?player) (location ?x) (location ?y)) (<= (devoid ?x ?player) (true (cell ?x ?person)) (role ?person) (distinct ?person ?player) (role ?player)) (<= (devoid ?x ?player) (true (cell ?x blank)) (role ?player)) (<= crissfin (crissfinished ?x ?y)) (<= (crissfinished ?x ?y) (true (step 40)) (crissgoal red ?x) (crissgoal teal ?y)) (<= (crissfinished ?x ?y) (true (first ?player)) (stones ?player2 all) (distinct ?player ?player2) (crissgoal red ?x) (crissgoal teal ?y)) (carred a3 b3) (carred a4 b4) (carred b3 c3) (carred b4 c4) (carred c1 d1) (carred c2 d2) (carred c3 d3) (carred c4 d4) (carred c5 d5) (carred c6 d6) (carred d3 e3) (carred d4 e4) (carred e3 f3) (carred e4 f4) (carteal a3 a4) (carteal b3 b4) (carteal c1 c2) (carteal c2 c3) (carteal c3 c4) (carteal c4 c5) (carteal c5 c6) (carteal d1 d2) (carteal d2 d3) (carteal d3 d4) (carteal d4 d5) (carteal d5 d6) (carteal e3 e4) (carteal f3 f4) (succ 1 2) (succ 2 3) (succ 3 4) (succ 4 5) (succ 5 6) (succ 6 7) (succ 7 8) (succ 8 9) (succ 9 10) (succ 10 11) (succ 11 12) (succ 12 13) (succ 13 14) (succ 14 15) (succ 15 16) (succ 16 17) (succ 17 18) (succ 18 19) (succ 19 20) (succ 20 21) (succ 21 22) (succ 22 23) (succ 23 24) (succ 24 25) (succ 25 26) (succ 26 27) (succ 27 28) (succ 28 29) (succ 29 30) (succ 30 31) (succ 31 32) (succ 32 33) (succ 33 34) (succ 34 35) (succ 35 36) (succ 36 37) (succ 37 38) (succ 38 39) (succ 39 40) (location a3) (location a4) (location b3) (location b4) (location c1) (location c2) (location c3) (location c4) (location c5) (location c6) (location d1) (location d2) (location d3) (location d4) (location d5) (location d6) (location e3) (location e4) (location f3) (location f4) ;;;;;;;;;;; racetrack ;;;;;;;;;;;; (init2 (cellr wlane a 1 b)) (init2 (cellr wlane a 2 b)) (init2 (cellr wlane a 3 red)) (init2 (cellr wlane b 1 b)) (init2 (cellr wlane b 2 b)) (init2 (cellr wlane b 3 b)) (init2 (cellr wlane c 1 b)) (init2 (cellr wlane c 2 b)) (init2 (cellr wlane c 3 b)) (init2 (cellr wlane d 1 b)) (init2 (cellr wlane d 2 b)) (init2 (cellr wlane d 3 b)) (init2 (cellr wlane e 1 b)) (init2 (cellr wlane e 2 b)) (init2 (cellr wlane e 3 b)) (init2 (cellr blane a 1 b)) (init2 (cellr blane a 2 b)) (init2 (cellr blane a 3 teal)) (init2 (cellr blane b 1 b)) (init2 (cellr blane b 2 b)) (init2 (cellr blane b 3 b)) (init2 (cellr blane c 1 b)) (init2 (cellr blane c 2 b)) (init2 (cellr blane c 3 b)) (init2 (cellr blane d 1 b)) (init2 (cellr blane d 2 b)) (init2 (cellr blane d 3 b)) (init2 (cellr blane e 1 b)) (init2 (cellr blane e 2 b)) (init2 (cellr blane e 3 b)) (init2 (wall wlane a none)) (init2 (wall wlane b none)) (init2 (wall wlane c none)) (init2 (wall wlane d none)) (init2 (wall blane a none)) (init2 (wall blane b none)) (init2 (wall blane c none)) (init2 (wall blane d none)) (init2 (walls red 4)) (init2 (walls teal 4)) (init2 (stepr 0)) (<= (next (cellr ?lane ?x ?y ?q)) (true (cellr ?lane ?x ?y ?q)) (playerlane ?player ?lane) (does ?player (place ?row ?side))) (<= (next (cellr ?lane ?x ?y ?p)) (playerlane ?player ?lane) (does ?player (mover ?p ?u ?v ?x ?y))) (<= (next (cellr ?lane ?u ?v b)) (playerlane ?player ?lane) (does ?player (mover ?p ?u ?v ?x ?y))) (<= (next (cellr ?lane ?w ?z b)) (playerlane ?player ?lane) (does ?player (mover ?p ?u ?v ?x ?y)) (true (cellr ?lane ?w ?z b)) (distinct ?z ?y)) (<= (next (cellr ?lane ?w ?z b)) (playerlane ?player ?lane) (does ?player (mover ?p ?u ?v ?x ?y)) (true (cellr ?lane ?w ?z b)) (distinct ?w ?x)) (<= (next (wall ?lane ?r ?s)) (does ?player (mover ?p ?u ?v ?x ?y)) (opponentlane ?player ?lane) (true (wall ?lane ?r ?s))) (<= (next (wall ?lane ?row ?side)) (does ?player (place ?row ?side)) (opponentlane ?player ?lane) (true (wall ?lane ?row none))) (<= (next (wall ?lane ?row ?side)) (does ?player (place ?row1 ?side1)) (opponentlane ?player ?lane) (true (wall ?lane ?row ?side)) (distinct ?row ?row1)) (<= (next (wall ?lane ?row none)) (does ?player (place ?r1 ?s1)) (opponentlane ?player ?lane) (true (wall ?lane ?row none)) (distinct ?r1 ?row)) (<= (next (walls ?player ?walls)) (does ?player (mover ?p ?u ?v ?x ?y)) (true (walls ?player ?walls))) (<= (next (walls ?player ?walls)) (does ?player (place ?row ?side)) (true (walls ?player ?pwalls)) (succr ?walls ?pwalls)) (<= (next (stepr ?y)) (true (stepr ?x)) (succr ?x ?y)) (<= (legal ?player (mover ?player ?u ?v ?x ?y)) (playerlane ?player ?lane) (true (cellr ?lane ?u ?v ?player)) (pawnmover ?lane ?u ?v ?x ?y) (true (cellr ?lane ?x ?y b))) (<= (legal ?player (place ?row left)) (true (walls ?player ?n)) (greaterthan ?n 0) (opponentlane ?player ?lane) (true (wall ?lane ?row none))) (<= (legal ?player (place ?row right)) (true (walls ?player ?n)) (greaterthan ?n 0) (opponentlane ?player ?lane) (true (wall ?lane ?row none))) (playerlane red wlane) (playerlane teal blane) (opponentlane red blane) (opponentlane teal wlane) (<= (pawnmover ?lane ?r1 1 ?r2 1) (nrow ?r1 ?r2) (true (wall ?lane ?r1 none))) (<= (pawnmover ?lane ?r1 1 ?r2 1) (nrow ?r1 ?r2) (true (wall ?lane ?r1 right))) (<= (pawnmover ?lane ?r1 2 ?r2 2) (nrow ?r1 ?r2) (true (wall ?lane ?r1 none))) (<= (pawnmover ?lane ?r1 3 ?r2 3) (nrow ?r1 ?r2) (true (wall ?lane ?r1 none))) (<= (pawnmover ?lane ?r1 3 ?r2 3) (nrow ?r1 ?r2) (true (wall ?lane ?r1 left))) (<= (pawnmover ?lane ?r 1 ?r 2) (playerlane ?c ?lane) (coordinate ?r)) (<= (pawnmover ?lane ?r 2 ?r 1) (playerlane ?c ?lane) (coordinate ?r)) (<= (pawnmover ?lane ?r 2 ?r 3) (playerlane ?c ?lane) (coordinate ?r)) (<= (pawnmover ?lane ?r 3 ?r 2) (playerlane ?c ?lane) (coordinate ?r)) (nrow a b) (nrow b c) (nrow c d) (nrow d e) (succr 0 1) (succr 1 2) (succr 2 3) (succr 3 4) (succr 4 5) (succr 5 6) (succr 6 7) (succr 7 8) (succr 8 9) (succr 9 10) (succr 10 11) (succr 11 12) (succr 12 13) (succr 13 14) (succr 14 15) (succr 15 16) (succr 16 17) (succr 17 18) (succr 18 19) (succr 19 20) (<= (greaterthan ?larger ?smaller) (succr ?smaller ?larger)) (<= (greaterthan ?larger ?smaller) (succr ?next ?larger) (greaterthan ?next ?smaller)) (coordinate a) (coordinate b) (coordinate c) (coordinate d) (coordinate e) (coordinate 1) (coordinate 2) (coordinate 3) (<= (racegoal red 50) (true (cellr wlane e ?x red)) (true (cellr blane ?r ?x1 teal)) (distinct ?r e)) (<= (racegoal red 50) (true (cellr wlane e ?x red)) (true (cellr blane e ?x1 teal)) (true (walls red ?wn)) (true (walls teal ?bn)) (greaterthan ?wn ?bn)) (<= (racegoal red 25) (true (cellr wlane e ?x red)) (true (cellr blane e ?x1 teal)) (true (walls red ?wn)) (true (walls teal ?bn)) (greaterthan ?bn ?wn)) (<= (racegoal red 5) (true (cellr blane e ?x teal)) (true (cellr wlane ?r ?x1 red)) (distinct ?r e)) (<= (racegoal teal 50) (true (cellr blane e ?x teal)) (true (cellr wlane ?r ?x1 red)) (distinct ?r e)) (<= (racegoal teal 50) (true (cellr wlane e ?x red)) (true (cellr blane e ?x1 teal)) (true (walls red ?wn)) (true (walls teal ?bn)) (greaterthan ?bn ?wn)) (<= (racegoal teal 25) (true (cellr wlane e ?x red)) (true (cellr blane e ?x1 teal)) (true (walls red ?wn)) (true (walls teal ?bn)) (greaterthan ?wn ?bn)) (<= (racegoal teal 5) (true (cellr wlane e ?x red)) (true (cellr blane ?r ?x1 teal)) (distinct ?r e)) (<= (racegoal ?role 0) (true (cellr wlane e ?x red)) (true (cellr blane e ?x1 teal)) (true (walls red ?n)) (true (walls teal ?n)) (role ?role)) (<= (racegoal ?role 2) (true (stepr 20)) (true (cellr wlane ?r1 ?x1 red)) (true (cellr blane ?r2 ?x2 teal)) (distinct ?r1 e) (distinct ?r2 e) (role ?role)) (<= terminal crissscorz (true (stepr 20))) (<= terminal crissscorz (true (cellr ?lane e ?r ?p)) (distinct ?p b)) (<= (goal red ?sum) (true (crissscores ?x ?y)) (racegoal red ?z) (sum ?x ?z ?sum)) (<= (goal teal ?sum) (true (crissscores ?x ?y)) (racegoal teal ?z) (sum ?y ?z ?sum)) (sum 0 2 2) (sum 0 5 5) (sum 0 7 7) (sum 0 12 12) (sum 0 25 25) (sum 0 38 38) (sum 0 50 50) (sum 2 0 2) (sum 2 2 4) (sum 2 5 7) (sum 2 7 9) (sum 2 12 14) (sum 2 25 27) (sum 2 38 40) (sum 2 50 52) (sum 5 0 5) (sum 5 2 7) (sum 5 5 10) (sum 5 7 12) (sum 5 12 17) (sum 5 25 30) (sum 5 38 43) (sum 5 50 55) (sum 7 0 7) (sum 7 2 9) (sum 7 5 12) (sum 7 7 14) (sum 7 12 19) (sum 7 25 32) (sum 7 38 45) (sum 7 50 57) (sum 12 0 12) (sum 12 2 14) (sum 12 5 17) (sum 12 7 19) (sum 12 12 24) (sum 12 25 37) (sum 12 38 50) (sum 12 50 62) (sum 25 0 25) (sum 25 2 27) (sum 25 5 30) (sum 25 7 32) (sum 25 12 37) (sum 25 25 50) (sum 25 38 63) (sum 25 50 75) (sum 38 0 38) (sum 38 2 40) (sum 38 5 43) (sum 38 7 45) (sum 38 12 50) (sum 38 25 63) (sum 38 38 76) (sum 38 50 88) (sum 50 0 50) (sum 50 2 52) (sum 50 5 55) (sum 50 7 57) (sum 50 12 62) (sum 50 25 75) (sum 50 38 88) (sum 50 50 100)