; EXIT: 0
; SCRUBBER: grep -v -E '.*'
(set-logic AUFLIA)
-(declare-sort S$ 0)
-(declare-sort Nat$ 0)
-(declare-sort Enat$ 0)
-(declare-sort Hmultiset$ 0)
-(declare-sort S_enat_fun$ 0)
-(declare-sort V_enat_fun$ 0)
-(declare-sort V_s_set_fun$ 0)
-(declare-sort S_hmultiset_fun$ 0)
-(declare-sort S_s_bool_fun_fun$ 0)
-(declare-sort Hmultiset_multiset$ 0)
-(declare-sort S_s_v_tm_s_v_tm_bool_fun_fun_s_v_tm_list_s_v_tm_list_bool_fun_fun_fun_fun$ 0)
-(declare-fun f$ () S$)
-(declare-fun one$ () Hmultiset$)
-(declare-fun enat$ (Nat$) Enat$)
-(declare-fun extf$ () S_s_v_tm_s_v_tm_bool_fun_fun_s_v_tm_list_s_v_tm_list_bool_fun_fun_fun_fun$)
-(declare-fun less$ (Enat$ Enat$) Bool)
-(declare-fun zero$ () Enat$)
-(declare-fun delta$ () Nat$)
-(declare-fun hMSet$ (Hmultiset_multiset$) Hmultiset$)
-(declare-fun less$a (Nat$ Nat$) Bool)
-(declare-fun less$b (Hmultiset$ Hmultiset$) Bool)
-(declare-fun minus$ (Nat$ Nat$) Nat$)
-(declare-fun times$ (Enat$ Enat$) Enat$)
-(declare-fun zero$a () Nat$)
-(declare-fun zero$b () Hmultiset_multiset$)
-(declare-fun zero$c () Hmultiset$)
-(declare-fun gt_sym$ () S_s_bool_fun_fun$)
-(declare-fun minus$a (Hmultiset$ Hmultiset$) Hmultiset$)
-(declare-fun of_nat$ (Nat$) Hmultiset$)
-(declare-fun times$a (Nat$ Nat$) Nat$)
-(declare-fun times$b (Hmultiset$ Hmultiset$) Hmultiset$)
-(declare-fun wt_sym$ () S_hmultiset_fun$)
-(declare-fun epsilon$ () Nat$)
-(declare-fun fun_app$ (S_enat_fun$ S$) Enat$)
-(declare-fun less_eq$ (Hmultiset$ Hmultiset$) Bool)
-(declare-fun of_nat$a (Nat$) Enat$)
-(declare-fun of_nat$b (Nat$) Nat$)
-(declare-fun add_mset$ (Hmultiset$ Hmultiset_multiset$) Hmultiset_multiset$)
-(declare-fun fun_app$a (S_hmultiset_fun$ S$) Hmultiset$)
-(declare-fun infinity$ () Enat$)
-(declare-fun the_enat$ (Enat$) Nat$)
-(declare-fun arity_sym$ () S_enat_fun$)
-(declare-fun arity_var$ () V_enat_fun$)
-(declare-fun hmset_of_enat$ (Enat$) Hmultiset$)
-(declare-fun kbo_std_basis$ (V_s_set_fun$ S_s_bool_fun_fun$ S_enat_fun$ V_enat_fun$ S_hmultiset_fun$ Nat$ Nat$ S_s_v_tm_s_v_tm_bool_fun_fun_s_v_tm_list_s_v_tm_list_bool_fun_fun_fun_fun$) Bool)
-(declare-fun ground_heads_var$ () V_s_set_fun$)
-(assert (forall ((?v0 Enat$)) (=> (=> (= ?v0 zero$) false) (less$ zero$ ?v0))))
-(assert (forall ((?v0 Nat$)) (=> (=> (= ?v0 zero$a) false) (less$a zero$a ?v0))))
-(assert (forall ((?v0 Nat$)) (= (hmset_of_enat$ (enat$ ?v0)) (of_nat$ ?v0))))
-(assert (forall ((?v0 Enat$) (?v1 Enat$)) (= (= (hmset_of_enat$ ?v0) (hmset_of_enat$ ?v1)) (= ?v0 ?v1))))
-(assert (forall ((?v0 Enat$)) (= (less$b (hmset_of_enat$ ?v0) (hMSet$ (add_mset$ one$ zero$b))) (not (= ?v0 infinity$)))))
-(assert (forall ((?v0 V_s_set_fun$) (?v1 S_s_bool_fun_fun$) (?v2 S_enat_fun$) (?v3 V_enat_fun$) (?v4 S_hmultiset_fun$) (?v5 Nat$) (?v6 Nat$) (?v7 S_s_v_tm_s_v_tm_bool_fun_fun_s_v_tm_list_s_v_tm_list_bool_fun_fun_fun_fun$) (?v8 S$)) (=> (and (kbo_std_basis$ ?v0 ?v1 ?v2 ?v3 ?v4 ?v5 ?v6 ?v7) (less$a zero$a ?v6)) (not (= (fun_app$ ?v2 ?v8) infinity$)))))
-(assert (forall ((?v0 V_s_set_fun$) (?v1 S_s_bool_fun_fun$) (?v2 S_enat_fun$) (?v3 V_enat_fun$) (?v4 S_hmultiset_fun$) (?v5 Nat$) (?v6 Nat$) (?v7 S_s_v_tm_s_v_tm_bool_fun_fun_s_v_tm_list_s_v_tm_list_bool_fun_fun_fun_fun$) (?v8 S$)) (=> (kbo_std_basis$ ?v0 ?v1 ?v2 ?v3 ?v4 ?v5 ?v6 ?v7) (less_eq$ (of_nat$ (minus$ ?v5 (the_enat$ (times$ (of_nat$a ?v6) (fun_app$ ?v2 ?v8))))) (fun_app$a ?v4 ?v8)))))
-(assert (kbo_std_basis$ ground_heads_var$ gt_sym$ arity_sym$ arity_var$ wt_sym$ epsilon$ delta$ extf$))
-(assert (forall ((?v0 Hmultiset$)) (=> (less$b ?v0 (hMSet$ (add_mset$ one$ zero$b))) (exists ((?v1 Nat$)) (= ?v0 (of_nat$ ?v1))))))
-(assert (forall ((?v0 Enat$) (?v1 Enat$)) (= (= (times$ ?v0 ?v1) zero$) (or (= ?v0 zero$) (= ?v1 zero$)))))
-(assert (forall ((?v0 Nat$) (?v1 Nat$)) (= (= (times$a ?v0 ?v1) zero$a) (or (= ?v0 zero$a) (= ?v1 zero$a)))))
-(assert (forall ((?v0 Hmultiset$) (?v1 Hmultiset$)) (= (= (times$b ?v0 ?v1) zero$c) (or (= ?v0 zero$c) (= ?v1 zero$c)))))
-(assert (= (of_nat$b zero$a) zero$a))
-(assert (= (of_nat$ zero$a) zero$c))
-(assert (= (of_nat$a zero$a) zero$))
-(assert (forall ((?v0 Nat$)) (= (of_nat$a ?v0) (enat$ ?v0))))
-(assert (forall ((?v0 Nat$) (?v1 Nat$)) (= (of_nat$ (minus$ ?v0 ?v1)) (minus$a (of_nat$ ?v0) (of_nat$ ?v1)))))
-(assert (forall ((?v0 Nat$) (?v1 Nat$)) (= (of_nat$b (times$a ?v0 ?v1)) (times$a (of_nat$b ?v0) (of_nat$b ?v1)))))
-(assert (forall ((?v0 Nat$) (?v1 Nat$)) (= (of_nat$ (times$a ?v0 ?v1)) (times$b (of_nat$ ?v0) (of_nat$ ?v1)))))
-(assert (forall ((?v0 Nat$) (?v1 Nat$)) (= (of_nat$a (times$a ?v0 ?v1)) (times$ (of_nat$a ?v0) (of_nat$a ?v1)))))
-(assert (forall ((?v0 Nat$)) (= (the_enat$ (enat$ ?v0)) ?v0)))
-(assert (not (less_eq$ (minus$a (of_nat$ epsilon$) (times$b (of_nat$ delta$) (hmset_of_enat$ (fun_app$ arity_sym$ f$)))) (fun_app$a wt_sym$ f$))))
+(declare-const x Bool)
+(declare-sort S 0)
+(declare-sort N 0)
+(declare-sort E 0)
+(declare-sort H 0)
+(declare-sort S_ 0)
+(declare-sort V 0)
+(declare-sort h 0)
+(declare-fun f () S)
+(declare-fun d () N)
+(declare-fun m (N N) N)
+(declare-fun r () N)
+(declare-fun m (H H) H)
+(declare-fun o (N) H)
+(declare-fun t (N N) N)
+(declare-fun t (H H) H)
+(declare-fun w () h)
+(declare-fun p () N)
+(declare-fun u (S_ S) E)
+(declare-fun l (H H) Bool)
+(declare-fun of (N) E)
+(declare-fun u (h S) H)
+(declare-fun t (E) N)
+(declare-fun a () S_)
+(declare-fun h (E) H)
+(assert (forall ((? N)) (= (o d) (h (of r)))))
+(assert (forall ((? E) (v E)) (= (h ?) (h v))))
+(assert (forall ((? V)) (or (l (u w f) (o (m p (t (of r))))))))
+(assert (forall ((v H)) (= x (= (o r) (t v v)))))
+(assert (forall ((v N)) (= (o (m p v)) (m (o p) (o v)))))
+(assert (forall ((v N)) (= (o (t r v)) (t (o v) (o v)))))
+(assert (forall ((v N)) (= (of r) (of (t r v)))))
+(assert (forall ((? N)) (= ? (t (of ?)))))
+(assert (not (l (u w f) (m (o p) (t (o d) (h (u a f)))))))
(check-sat)
projects / cvc5.git / commitdiff