(benchmark circus_po_1
  :logic UNKNOWN
  :extrafuns ((secondp Int))
  :extrafuns ((minutep 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 (inrange secondp 0 59)
			   (inrange minutep 0 59)
			   true)
		      true)
		 (= secondp minutep)
		 (= minutep 0))
	    (and (= secondp 0)
		 (= minutep 0))
	    ))
   )
)
