(benchmark list_6
  :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 (or (not (= (car ?x) (car ?y)))
			    (not (= (cdr ?x) (cdr ?y))))
			(not (= ?x ?y))))
       (= (car l1) a)
       (= (cdr l1) nil)
       (= (car l2) b)
       (= (cdr l2) nil)
       (not (= a b))
       (not (= l1 l2)))
  :status sat
)
