2 (set-info :status unsat)
4 ;; don't use a datatypes for currently focusing in uf
7 (declare-fun cons (Int list) list)
8 (declare-fun nil () list)
11 (declare-fun length (list) Int)
13 (assert (= (length nil) 0))
15 (declare-fun one_cons (list) list)
17 (assert (= (length (cons 1 nil)) (+ 1 (length nil))))
18 (assert (= (one_cons nil) (cons 1 nil)))
19 (assert (not (= (length (one_cons nil)) 1)))