(benchmark list_3
  :logic UNKNOWN
  :extrasorts (U)
  :extrafuns ((a U) (b U) (l1 U) (l2 U) (nil 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) a)
       (= (cdr l1) nil)
       (= (car l2) b)
       (= (cdr l2) nil)
       (= a b)
       (not (= l1 l2)))
  :status unsat
)
