Формулы ЭПР с равенством и неравенством

Я кодирую множества как отношения, а операции над множествами — как универсальные квантифицированные импликации. У меня есть оператор выбора над наборами, который создает новые наборы, выбирая элементы, удовлетворяющие унарному предикату p (например: v‹4, v>4, ..). Благодаря этому оператору в моих формулах присутствуют простые арифметические предикаты. Пример кодирования Z3 такой формулы приведен ниже -

(set-option :mbqi true)
(set-option :model-compact true)                                                                                 

;; Rmem and Rmem1 are sets of Int                                                                                 
(declare-fun Rmem (Int) Bool)
(declare-fun Rmem1 (Int) Bool)
(declare-const v Int)
(declare-const v1 Int)
(declare-const x Int) 
;; Rmem = Rmem1 U {x}
(assert (forall ((n Int)) (= (Rmem n)(or (Rmem1 n) (= n x)))))
;; Select(m<v1) from Rmem1 = {}
(assert (forall ((m Int)) (= false (and (Rmem1 m) (< m v1)))))
(assert (or (< v x) (= v x)))
(assert (or (< v v) (= v v1)))

(assert (exists ((q Int)) (and (Rmem q) (< q v))))
(check-sat)
(get-model)

Как и ожидалось, Z3 возвращает UNSAT для приведенной выше формулы. Тем не менее, мои вопросы -

1. Учитывая, что я могу написать свою формулу в пренексной нормальной форме, она все еще находится в классе ЭПР?
2. Разрешимы ли такие формулы? Является ли z3 решающей процедурой для таких формул? Как мне ограничить свои предикаты, чтобы формулы были разрешимы?

Обновление. Вышеупомянутый набор формул может быть выражен в виде конъюнктивных запросов в реляционной алгебре, но с неравенством.