Как удалить некоторые повторяющиеся выражения, используя тактику упрощения в Z3

Я использую следующую тактику, чтобы упростить выражение

(apply (then  (! simplify :eq2ineq true) ctx-solver-simplify propagate-values ctx-solver-simplify (par-then (repeat (or-else split-clause skip)) propagate-ineqs) tseitin-cnf))

Исходное выражение:

( 0 > t_DS or 1 > t_FS or 1 > t_PS) And 
(true) And 
(( 0 > t_DS or 0 > t_FS or 0 > t_PS) or (t_DS <= 3)) And 
(( 0 > t_DS or 0 > t_FS or 0 > t_PS or t_FS <= 1) or ( t_DS+t_FS <= 3)) And
((0 > t_DS or 0 > t_PS or 1 > t_FS or t_PS > 1) or ( t_DS+t_PS <= 2)) And
(t_DS >=0) And (t_FS >= 0) And (t_PS >=0)

После применения тактики упрощенный результат:

(goals
(goal
  (>= t_FS 0.0)
  (not (>= t_FS 1.0))
  (<= (+ t_DS t_FS) 3.0)
  (>= t_DS 0.0)
  (<= t_DS 3.0)
  (>= t_User 0.0)
  (>= t_PS 0.0))
(goal
  (>= t_FS 0.0)
  (not (>= t_FS 1.0))
  (<= (+ t_DS t_FS) 3.0)
  (>= t_DS 0.0)
  (<= t_DS 3.0)
  (not (<= t_PS 1.0))
  (>= t_User 0.0))
(goal
  (>= t_FS 0.0)
  (not (>= t_FS 1.0))
  (>= t_DS 0.0)
  (<= t_DS 2.0)
  (<= (+ t_DS t_PS) 2.0)
  (>= t_PS 0.0)
  (<= t_PS 2.0)
  (>= t_User 0.0))
(goal
  (>= t_PS 0.0)
  (not (>= t_PS 1.0))
  (not (<= t_FS 1.0))
  (<= (+ t_DS t_PS) 2.0)
  (>= t_DS 0.0)
  (<= t_DS 2.0)
  (>= t_User 0.0))
(goal
  (>= t_PS 0.0)
  (not (>= t_PS 1.0))
  (<= (+ t_DS t_FS) 3.0)
  (>= t_DS 0.0)
  (<= t_DS 3.0)
  (>= t_FS 0.0)
  (not (>= t_FS 1.0))
  (>= t_User 0.0))
(goal
  (>= t_PS 0.0)
  (not (>= t_PS 1.0))
  (<= (+ t_DS t_FS) 3.0)
  (>= t_DS 0.0)
  (<= t_DS 2.0)
  (>= t_FS 0.0)
  (<= t_FS 3.0)
  (<= (+ t_DS t_PS) 2.0)
  (>= t_User 0.0))
) 

Однако, думаю, второй гол можно убрать, так как он сильнее первого. Итак, как использовать z3, чтобы получить более простой результат?

(goal
  (>= t_FS 0.0)
  (not (>= t_FS 1.0))
  (<= (+ t_DS t_FS) 3.0)
  (>= t_DS 0.0)
  (<= t_DS 3.0)
  (>= t_User 0.0)
  (>= t_PS 0.0))
(goal
  (>= t_FS 0.0)
  (not (>= t_FS 1.0))
  (<= (+ t_DS t_FS) 3.0)
  (>= t_DS 0.0)
  (<= t_DS 3.0)
  (not (<= t_PS 1.0))
  (>= t_User 0.0))