;; Timeout (alors qu'il devrait trouver un contrex)
(set-logic HORN)


(declare-datatypes ((nat 0) (natlist 0)) 
	(
		(
			(z) 
			(s (pred nat))
		)
		(
			(nil)
			(cons (hd nat) (tl natlist))
		)
	)
)


(define-fun-rec append ((l1 natlist) (l2 natlist)) natlist 
	(
		match l1
		(
			(nil l2)
			((cons h1 t1) (cons h1 (append t1 l2)))
		)
	)
)

(define-fun-rec reverse ((l1 natlist)) natlist
	(
		match l1
		(
			(nil nil)
			((cons h1 t1) (append (reverse t1) (cons h1 nil)))
		)
	)
)

(define-fun-rec not_null ((l natlist)) Bool
	(
		match l
		( 
			(nil false)
			( (cons x ll) true)
		)
	)
)

(assert (forall ((l1 natlist))
				(not_null (reverse l1))))



(check-sat)