(datatype Stack
          (Empty)
          (Cons i64 Stack))

(function Config (Stack Stack Stack) i64 :merge (min old new))

;; move from first stack
(rule ((= len (Config (Cons x a) b c)))
      ((set (Config a (Cons x b) c) (+ len 1))
       (set (Config a b (Cons x c)) (+ len 1))))

;; move from second stack
(rule ((= len (Config a (Cons x b) c)))
      ((set (Config (Cons x a) b c) (+ len 1))
       (set (Config a b (Cons x c)) (+ len 1))))

;; move from third stack
(rule ((= len (Config a b (Cons x c))))
      ((set (Config (Cons x a) b c) (+ len 1))
       (set (Config a (Cons x b) c) (+ len 1))))

(let e (Empty))


;; initial state [123 _ _] with path "length" 0
(set (Config (Cons 1 (Cons 2 (Cons 3 e))) e e) 0)

;; find all reachable states
(run 1000000)

;; print first 10 tuples
(print-function Config 10)
(print-size Config)

;; how to long to move to state [_ _ 123]
(query-extract (Config e e (Cons 1 (Cons 2 (Cons 3 e)))))

;; actually do the assertion
(check (= 5 (Config e e (Cons 1 (Cons 2 (Cons 3 e))))))