(benchmark circus_po_2
  :logic UNKNOWN
  :extrafuns ((secondp Int))
  :extrapreds ((inrange Int Int Int))
  :status unknown
  :formula
  (not 
   (implies (forall (?x Int) (?l Int) (?h Int)
		    (iff (inrange ?x ?l ?h) 
			 (and (<= ?l ?x) (<= ?x ?h))))
	    (iff (and (and (and (and (inrange secondp 0 59)
				     true)
				true)
			   true)
		      (= secondp 0))
		 (= secondp 0))))
)
