SMT-LIB model for chess board with dominos problem

0model.txt

;; Output after running with d30a/d30b removed i.e. one less domino.
;; Cleaned up slightly (whitespace and variable ordering)
sat
(
  (define-fun d0a  () Int 2)
  (define-fun d0b  () Int 3)
  (define-fun d1a  () Int 4)
  (define-fun d1b  () Int 5)
  (define-fun d2a  () Int 6)
  (define-fun d2b  () Int 7)
  (define-fun d3a  () Int 8)
  (define-fun d3b  () Int 9)
  (define-fun d4a  () Int 10)
  (define-fun d4b  () Int 11)
  (define-fun d5a  () Int 12)
  (define-fun d5b  () Int 13)
  (define-fun d6a  () Int 14)
  (define-fun d6b  () Int 15)
  (define-fun d7a  () Int 16)
  (define-fun d7b  () Int 17)
  (define-fun d8a  () Int 18)
  (define-fun d8b  () Int 19)
  (define-fun d9a  () Int 20)
  (define-fun d9b  () Int 21)
  (define-fun d10a () Int 22)
  (define-fun d10b () Int 23)
  (define-fun d11a () Int 24)
  (define-fun d11b () Int 25)
  (define-fun d12a () Int 26)
  (define-fun d12b () Int 27)
  (define-fun d13a () Int 28)
  (define-fun d13b () Int 29)
  (define-fun d14a () Int 30)
  (define-fun d14b () Int 31)
  (define-fun d15a () Int 32)
  (define-fun d15b () Int 33)
  (define-fun d16a () Int 34)
  (define-fun d16b () Int 35)
  (define-fun d17a () Int 36)
  (define-fun d17b () Int 37)
  (define-fun d18a () Int 38)
  (define-fun d18b () Int 39)
  (define-fun d19a () Int 40)
  (define-fun d19b () Int 41)
  (define-fun d20a () Int 42)
  (define-fun d20b () Int 43)
  (define-fun d21a () Int 44)
  (define-fun d21b () Int 45)
  (define-fun d22a () Int 46)
  (define-fun d22b () Int 47)
  (define-fun d23a () Int 48)
  (define-fun d23b () Int 49)
  (define-fun d24a () Int 50)
  (define-fun d24b () Int 51)
  (define-fun d25a () Int 52)
  (define-fun d25b () Int 53)
  (define-fun d26a () Int 54)
  (define-fun d26b () Int 55)
  (define-fun d27a () Int 57)
  (define-fun d27b () Int 58)
  (define-fun d28a () Int 59)
  (define-fun d28b () Int 60)
  (define-fun d29a () Int 61)
  (define-fun d29b () Int 62)
)

real	0m0.043s
user	0m0.040s
sys	0m0.003s

chess.smt

(set-option :print-success false)
(set-logic QF_LIA)
(declare-fun d0a () Int)
(declare-fun d0b () Int)
(declare-fun d1a () Int)
(declare-fun d1b () Int)
(declare-fun d2a () Int)
(declare-fun d2b () Int)
(declare-fun d3a () Int)
(declare-fun d3b () Int)
(declare-fun d4a () Int)
(declare-fun d4b () Int)
(declare-fun d5a () Int)
(declare-fun d5b () Int)
(declare-fun d6a () Int)
(declare-fun d6b () Int)
(declare-fun d7a () Int)
(declare-fun d7b () Int)
(declare-fun d8a () Int)
(declare-fun d8b () Int)
(declare-fun d9a () Int)
(declare-fun d9b () Int)
(declare-fun d10a () Int)
(declare-fun d10b () Int)
(declare-fun d11a () Int)
(declare-fun d11b () Int)
(declare-fun d12a () Int)
(declare-fun d12b () Int)
(declare-fun d13a () Int)
(declare-fun d13b () Int)
(declare-fun d14a () Int)
(declare-fun d14b () Int)
(declare-fun d15a () Int)
(declare-fun d15b () Int)
(declare-fun d16a () Int)
(declare-fun d16b () Int)
(declare-fun d17a () Int)
(declare-fun d17b () Int)
(declare-fun d18a () Int)
(declare-fun d18b () Int)
(declare-fun d19a () Int)
(declare-fun d19b () Int)
(declare-fun d20a () Int)
(declare-fun d20b () Int)
(declare-fun d21a () Int)
(declare-fun d21b () Int)
(declare-fun d22a () Int)
(declare-fun d22b () Int)
(declare-fun d23a () Int)
(declare-fun d23b () Int)
(declare-fun d24a () Int)
(declare-fun d24b () Int)
(declare-fun d25a () Int)
(declare-fun d25b () Int)
(declare-fun d26a () Int)
(declare-fun d26b () Int)
(declare-fun d27a () Int)
(declare-fun d27b () Int)
(declare-fun d28a () Int)
(declare-fun d28b () Int)
(declare-fun d29a () Int)
(declare-fun d29b () Int)
(declare-fun d30a () Int)
(declare-fun d30b () Int)
(assert (< d0a d0b d1a d1b d2a d2b d3a d3b d4a d4b d5a d5b d6a d6b d7a d7b d8a d8b d9a d9b d10a d10b d11a d11b d12a d12b d13a d13b d14a d14b d15a d15b d16a d16b d17a d17b d18a d18b d19a d19b d20a d20b d21a d21b d22a d22b d23a d23b d24a d24b d25a d25b d26a d26b d27a d27b d28a d28b d29a d29b d30a d30b))
(assert (< 0 d0a 63))
(assert (< 0 d0b 63))
(assert (or (and (not (= (mod d0a 8) (- 8 1)))
                 (= d0b (+ d0a 1)))
            (and (< d0a (* 8 (- 8 1)))
                 (= d0b (+ d0a 8)))))
(assert (< 0 d1a 63))
(assert (< 0 d1b 63))
(assert (or (and (not (= (mod d1a 8) (- 8 1)))
                 (= d1b (+ d1a 1)))
            (and (< d1a (* 8 (- 8 1)))
                 (= d1b (+ d1a 8)))))
(assert (< 0 d2a 63))
(assert (< 0 d2b 63))
(assert (or (and (not (= (mod d2a 8) (- 8 1)))
                 (= d2b (+ d2a 1)))
            (and (< d2a (* 8 (- 8 1)))
                 (= d2b (+ d2a 8)))))
(assert (< 0 d3a 63))
(assert (< 0 d3b 63))
(assert (or (and (not (= (mod d3a 8) (- 8 1)))
                 (= d3b (+ d3a 1)))
            (and (< d3a (* 8 (- 8 1)))
                 (= d3b (+ d3a 8)))))
(assert (< 0 d4a 63))
(assert (< 0 d4b 63))
(assert (or (and (not (= (mod d4a 8) (- 8 1)))
                 (= d4b (+ d4a 1)))
            (and (< d4a (* 8 (- 8 1)))
                 (= d4b (+ d4a 8)))))
(assert (< 0 d5a 63))
(assert (< 0 d5b 63))
(assert (or (and (not (= (mod d5a 8) (- 8 1)))
                 (= d5b (+ d5a 1)))
            (and (< d5a (* 8 (- 8 1)))
                 (= d5b (+ d5a 8)))))
(assert (< 0 d6a 63))
(assert (< 0 d6b 63))
(assert (or (and (not (= (mod d6a 8) (- 8 1)))
                 (= d6b (+ d6a 1)))
            (and (< d6a (* 8 (- 8 1)))
                 (= d6b (+ d6a 8)))))
(assert (< 0 d7a 63))
(assert (< 0 d7b 63))
(assert (or (and (not (= (mod d7a 8) (- 8 1)))
                 (= d7b (+ d7a 1)))
            (and (< d7a (* 8 (- 8 1)))
                 (= d7b (+ d7a 8)))))
(assert (< 0 d8a 63))
(assert (< 0 d8b 63))
(assert (or (and (not (= (mod d8a 8) (- 8 1)))
                 (= d8b (+ d8a 1)))
            (and (< d8a (* 8 (- 8 1)))
                 (= d8b (+ d8a 8)))))
(assert (< 0 d9a 63))
(assert (< 0 d9b 63))
(assert (or (and (not (= (mod d9a 8) (- 8 1)))
                 (= d9b (+ d9a 1)))
            (and (< d9a (* 8 (- 8 1)))
                 (= d9b (+ d9a 8)))))
(assert (< 0 d10a 63))
(assert (< 0 d10b 63))
(assert (or (and (not (= (mod d10a 8) (- 8 1)))
                 (= d10b (+ d10a 1)))
            (and (< d10a (* 8 (- 8 1)))
                 (= d10b (+ d10a 8)))))
(assert (< 0 d11a 63))
(assert (< 0 d11b 63))
(assert (or (and (not (= (mod d11a 8) (- 8 1)))
                 (= d11b (+ d11a 1)))
            (and (< d11a (* 8 (- 8 1)))
                 (= d11b (+ d11a 8)))))
(assert (< 0 d12a 63))
(assert (< 0 d12b 63))
(assert (or (and (not (= (mod d12a 8) (- 8 1)))
                 (= d12b (+ d12a 1)))
            (and (< d12a (* 8 (- 8 1)))
                 (= d12b (+ d12a 8)))))
(assert (< 0 d13a 63))
(assert (< 0 d13b 63))
(assert (or (and (not (= (mod d13a 8) (- 8 1)))
                 (= d13b (+ d13a 1)))
            (and (< d13a (* 8 (- 8 1)))
                 (= d13b (+ d13a 8)))))
(assert (< 0 d14a 63))
(assert (< 0 d14b 63))
(assert (or (and (not (= (mod d14a 8) (- 8 1)))
                 (= d14b (+ d14a 1)))
            (and (< d14a (* 8 (- 8 1)))
                 (= d14b (+ d14a 8)))))
(assert (< 0 d15a 63))
(assert (< 0 d15b 63))
(assert (or (and (not (= (mod d15a 8) (- 8 1)))
                 (= d15b (+ d15a 1)))
            (and (< d15a (* 8 (- 8 1)))
                 (= d15b (+ d15a 8)))))
(assert (< 0 d16a 63))
(assert (< 0 d16b 63))
(assert (or (and (not (= (mod d16a 8) (- 8 1)))
                 (= d16b (+ d16a 1)))
            (and (< d16a (* 8 (- 8 1)))
                 (= d16b (+ d16a 8)))))
(assert (< 0 d17a 63))
(assert (< 0 d17b 63))
(assert (or (and (not (= (mod d17a 8) (- 8 1)))
                 (= d17b (+ d17a 1)))
            (and (< d17a (* 8 (- 8 1)))
                 (= d17b (+ d17a 8)))))
(assert (< 0 d18a 63))
(assert (< 0 d18b 63))
(assert (or (and (not (= (mod d18a 8) (- 8 1)))
                 (= d18b (+ d18a 1)))
            (and (< d18a (* 8 (- 8 1)))
                 (= d18b (+ d18a 8)))))
(assert (< 0 d19a 63))
(assert (< 0 d19b 63))
(assert (or (and (not (= (mod d19a 8) (- 8 1)))
                 (= d19b (+ d19a 1)))
            (and (< d19a (* 8 (- 8 1)))
                 (= d19b (+ d19a 8)))))
(assert (< 0 d20a 63))
(assert (< 0 d20b 63))
(assert (or (and (not (= (mod d20a 8) (- 8 1)))
                 (= d20b (+ d20a 1)))
            (and (< d20a (* 8 (- 8 1)))
                 (= d20b (+ d20a 8)))))
(assert (< 0 d21a 63))
(assert (< 0 d21b 63))
(assert (or (and (not (= (mod d21a 8) (- 8 1)))
                 (= d21b (+ d21a 1)))
            (and (< d21a (* 8 (- 8 1)))
                 (= d21b (+ d21a 8)))))
(assert (< 0 d22a 63))
(assert (< 0 d22b 63))
(assert (or (and (not (= (mod d22a 8) (- 8 1)))
                 (= d22b (+ d22a 1)))
            (and (< d22a (* 8 (- 8 1)))
                 (= d22b (+ d22a 8)))))
(assert (< 0 d23a 63))
(assert (< 0 d23b 63))
(assert (or (and (not (= (mod d23a 8) (- 8 1)))
                 (= d23b (+ d23a 1)))
            (and (< d23a (* 8 (- 8 1)))
                 (= d23b (+ d23a 8)))))
(assert (< 0 d24a 63))
(assert (< 0 d24b 63))
(assert (or (and (not (= (mod d24a 8) (- 8 1)))
                 (= d24b (+ d24a 1)))
            (and (< d24a (* 8 (- 8 1)))
                 (= d24b (+ d24a 8)))))
(assert (< 0 d25a 63))
(assert (< 0 d25b 63))
(assert (or (and (not (= (mod d25a 8) (- 8 1)))
                 (= d25b (+ d25a 1)))
            (and (< d25a (* 8 (- 8 1)))
                 (= d25b (+ d25a 8)))))
(assert (< 0 d26a 63))
(assert (< 0 d26b 63))
(assert (or (and (not (= (mod d26a 8) (- 8 1)))
                 (= d26b (+ d26a 1)))
            (and (< d26a (* 8 (- 8 1)))
                 (= d26b (+ d26a 8)))))
(assert (< 0 d27a 63))
(assert (< 0 d27b 63))
(assert (or (and (not (= (mod d27a 8) (- 8 1)))
                 (= d27b (+ d27a 1)))
            (and (< d27a (* 8 (- 8 1)))
                 (= d27b (+ d27a 8)))))
(assert (< 0 d28a 63))
(assert (< 0 d28b 63))
(assert (or (and (not (= (mod d28a 8) (- 8 1)))
                 (= d28b (+ d28a 1)))
            (and (< d28a (* 8 (- 8 1)))
                 (= d28b (+ d28a 8)))))
(assert (< 0 d29a 63))
(assert (< 0 d29b 63))
(assert (or (and (not (= (mod d29a 8) (- 8 1)))
                 (= d29b (+ d29a 1)))
            (and (< d29a (* 8 (- 8 1)))
                 (= d29b (+ d29a 8)))))
(assert (< 0 d30a 63))
(assert (< 0 d30b 63))
(assert (or (and (not (= (mod d30a 8) (- 8 1)))
                 (= d30b (+ d30a 1)))
            (and (< d30a (* 8 (- 8 1)))
                 (= d30b (+ d30a 8)))))
(check-sat)
(get-model)