(benchmark circus_po_1 ; circus_po_1 é o nome do exemplo, tirei da minha
cabeça
 :logic UNKNOWN         ; indica se usamos alguma teoria
pré-definida, não é nosso caso
 :extrafuns ((secondp Int))   ; cada constante é declarada como uma
função sem parâmetro que retorna um Int
 :extrafuns ((minutep Int))
 :extrapreds ((inrange Int Int Int)) ; declarei um predicado
"inrange", que é ternário, e definido abaixo.
 :status unknown    ; indica qual o resultado que esperamos da
verificação - útil para testar o provador - não é de interesse aqui
 :formula          ; a fórmula que vamos tentar mostrar
insatisfatível (que é a negação do que queremos provar válido)
 (not
  (implies
      (forall (?x Int) (?l Int) (?h Int)    ; aqui introduzo a
definição de "inrange", como não é predefinido
       (iff (inrange ?x ?l ?h)
            (and (<= ?l ?x) (<= ?x ?h))))
      (iff (and (and (and (inrange secondp 0 59) ; aqui vem a primeira PO.
                          (inrange minutep 0 59)
                          true)
                     true)
                (= secondp minutep)
                (= minutep 0))
           (and (= secondp 0)
                (= minutep 0))
           ))
  )
)