(benchmark circus_po_5
  :logic UNKNOWN
  :extrafuns ((second Int))
  :extrafuns ((minute Int))
  :extrafuns ((secondp Int))
  :extrafuns ((minutep Int))
  :extrafuns ((mod Int Int 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 (= minutep (mod (+ minute 1) 60))
			   (= secondp second))
		      (and (and (and (inrange secondp 0 59)
				     true)
				true)
			   (and (inrange minutep 0 59) true)
			   true))
		 (and (= secondp (mod (+ second 1) 60))
		      (= minutep minute)))))
)
