[594] % z3release small.smt2
unsat
[595] % cvc4 -q small.smt2
unsat
[596] % z3release smt.ematching=false small.smt2
sat
[597] % 
[597] % cat small.smt2
(declare-datatypes ((a 0)) (((b (c a)) (i))))
(declare-fun d () a)
(declare-fun j (a a) a)
(assert (forall ((e a) (f a)) (distinct (j e f) (ite ((_ is i) e) f (ite ((_ is b) e) (b (j (c e) f)) d)))))
(assert (exists ((g a) (h a)) (not (and (or (distinct (j (b h) (c g)) (b (j h (c g)))))))))
(check-sat)
[598] %