;;Proof Obligations of Module in Harvey/SMT Language (benchmark filePO0 :logic UNKNOWN :extrasorts (Int) :extrafuns ((MININT Int) (MAXINT Int)) :extrafuns ((MININT Int) (MAXINT Int)) :extrafuns ( (second' Int ) (minute' Int )) :extrafuns ((MININT Int) (MAXINT Int)) :extrapreds ((INTEGER Int) (NATURAL Int)) :extramacros ((in (lambda (?x Int) (?p (Int boolean)) . (?p ?x))) (emptyset (lambda (?v Int) . false)) (omega (lambda (?x Int) . true)) (singleton (lambda (?x Int) . (lambda (?y Int) . (= ?x ?y)))) (intersection (lambda (?p (Int boolean)) (?q (Int boolean)) . (lambda (?x Int) . (and (?p ?x) (?q ?x))))) (union (lambda (?p (Int boolean)) (?q (Int boolean)) . (lambda (?x Int) . (or (?p ?x) (?q ?x))))) (difference (lambda (?p (Int boolean)) (?q (Int boolean)) . (lambda (?x Int) . (and (?p ?x) (not (?q ?x)))))) (symmetric_difference (lambda (?p (Int boolean)) (?q (Int boolean)) . (lambda (?x Int) . (or (and (?p ?x) (not (?q ?x))) (and (?q ?x) (not (?p ?x))))))) (subset (lambda (?p (Int boolean)) (?q (Int boolean)) . (forall (?x Int) . (implies (?p ?x) (?q ?x))))) (range (lambda (?n Int) (?m Int) . (lambda (?x Int) . (and (<= ?x ?m) (<= ?n ?x)))) ) ) :assumption (= MININT (~ 2147483647) ) :assumption (= MAXINT 2147483647) :assumption (forall (?i Int) (iff (in ?i INTEGER) (and (<= MININT ?i) (<= ?i MAXINT)))) :assumption (forall (?i Int) (iff (in ?i NATURAL) (and (<= 0 ?i) (<= ?i MAXINT)))) ;;UNKOWN-PO :formula (not (iff (and (and (and (and (in second' (range 0 59)) (and (in minute' (range 0 59)) true)) true) true) (and (= second' minute') (= minute' 0))) (and (= second' 0) (= minute' 0))) ) )