;(set-option :produce-proofs true)

(define-fun n () Int 4)   ; number of symbols
(define-fun len () Int 33) ; length of string
(define-fun len2 () Int 29)

(define-fun ran ((x Int)) Bool
  (and (<= 0 x) (< x len)))

(define-fun ran2 ((x Int)) Bool
  (and (<= 0 x) (<= x len2)))

(declare-fun perm (Int) Int)
(assert (forall ((x Int))
	(and (>= (perm x) 1) (<= (perm x) n))))

(define-fun subWord ((a0 Int) (a1 Int) (a2 Int) (a3 Int)) Bool
	(exists ((x Int))
		(and (ran2 x)
		     (= (perm (+ x 0)) a0)
		     (= (perm (+ x 1)) a1)
		     (= (perm (+ x 2)) a2)
		     (= (perm (+ x 3)) a3) )))

;(assert (forall ((x Int))  (not (= (perm x) (perm (+ x 1)))) ))
;(assert (forall ((x Int))  (not (= (perm x) (perm (+ x 2)))) ))

(assert (= 1 (perm 0)))
(assert (= 2 (perm 1)))
(assert (= 3 (perm 2)))
(assert (= 4 (perm 3)))

;(assert (subWord 1 2 3 4 5))
(assert (subWord 1 2 3 4))
(assert (subWord 2 1 3 4))
(assert (subWord 3 2 1 4))
(assert (subWord 2 3 1 4))
(assert (subWord 3 1 2 4))
(assert (subWord 1 3 2 4))
(assert (subWord 4 3 2 1))
(assert (subWord 3 4 2 1))
(assert (subWord 3 2 4 1))
(assert (subWord 4 2 3 1))
(assert (subWord 2 4 3 1))
(assert (subWord 2 3 4 1))
(assert (subWord 4 1 2 3))
(assert (subWord 1 4 2 3))
(assert (subWord 1 2 4 3))
(assert (subWord 4 2 1 3))
(assert (subWord 2 4 1 3))
(assert (subWord 2 1 4 3))
(assert (subWord 4 1 3 2))
(assert (subWord 1 4 3 2))
(assert (subWord 1 3 4 2))
(assert (subWord 4 3 1 2))
(assert (subWord 3 4 1 2))
(assert (subWord 3 1 4 2))

(check-sat)