;; 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
