(benchmark list_1
  :logic UNKNOWN
  :extrasorts (U)
  :extrafuns ((l1 U) (l2 U) (car U U) (cdr U U))
  :formula
  (and (forall (?x U) (?y U) 
	       (implies (and (= (car ?x) (car ?y))
			     (= (cdr ?x) (cdr ?y)))
			(= ?x ?y)))
       (= (car l1) (car l2))
       (= (cdr l1) (cdr l2))
       (not (= l1 l2)))
  :status unsat
)
