(declare-fun a () String)
(declare-fun b () Bool)
(declare-fun c () String)
(declare-fun d () Bool)
(declare-fun e () Bool)
(declare-fun f () Bool)
(declare-fun g () String)
(declare-fun h () Bool)
(declare-fun i () Bool)
(declare-fun j () Bool)
(declare-fun k () Bool)
(declare-fun l () String)
(declare-fun m () String)
(declare-fun n () Bool)
(declare-fun o () Bool)
(assert (= (distinct b (= "" (str.substr c 20 (str.len l)))) (= b (distinct f j)) (distinct "-" (str.substr c 10 (str.len l)))))
(assert (distinct (distinct n o) i))
(assert (distinct (= d e) (= d (distinct e (= "-" l)))))
(assert (distinct (distinct h d) (distinct "" (str.substr c 1 (str.len l)))))
(assert (= (= d k) (distinct "" (str.substr a 0 (str.len m)))))
(assert (= b (= d k)))
(assert (distinct b i))
(assert (distinct g m))
(assert (distinct n o))
(assert (distinct d (= k e)))
(assert (distinct h (distinct b e)))
(assert (= c (str.++ l m)))
(check-sat)