(set-logic QF_UFLIA)
(declare-fun op_4 () Int)
(declare-fun op_1 (Int) Bool)
(declare-fun op_0 () Int)
(declare-fun op_2 () Int)
(declare-fun op_3 (Int) Int)
(assert (and (= op_2 op_4) (and (= op_0 op_4) (or (not (= (op_3 op_2) (op_3 op_0))) (and (op_1 op_2) (not (op_1 op_0)))))))
(check-sat)
(exit)