(set-logic QF_UFDT)
(declare-datatypes ((t 0))
  (((T0) (T1 (prev1 t)) (T2 (prev2 t)))))

(declare-const c1 t)
(declare-const c2 t)
(declare-const c3 t)
(declare-const c4 t)
(declare-const c5 t)
(declare-const c6 t)
(declare-const c7 t)
(declare-const c8 t)
(declare-const c9 t)
(declare-const c10 t)
(declare-const c11 t)
(declare-const c12 t)
(declare-const c13 t)
(declare-const c14 t)
(declare-const c15 t)
(declare-const c16 t)
(declare-const c17 t)
(declare-const c18 t)
(declare-const c19 t)
(declare-const c20 t)
(declare-const c21 t)
(declare-const c22 t)
(declare-const c23 t)
(declare-const c24 t)
(declare-const c25 t)
(declare-const c26 t)
(declare-const c27 t)
(declare-const c28 t)
(declare-const c29 t)
(declare-const c30 t)
(declare-const c31 t)
(declare-const c32 t)
(declare-const c33 t)
(declare-const c34 t)
(declare-const c35 t)
(declare-const c36 t)
(declare-const c37 t)
(declare-const c38 t)
(declare-const c39 t)
(declare-const c40 t)
(declare-const c41 t)
(declare-const c42 t)
(declare-const c43 t)
(declare-const c44 t)
(declare-const c45 t)
(declare-const c46 t)
(declare-const c47 t)
(declare-const c48 t)
(declare-const c49 t)
(declare-const c50 t)
(declare-const c51 t)
(declare-const c52 t)
(declare-const c53 t)
(declare-const c54 t)
(declare-const c55 t)
(declare-const c56 t)
(declare-const c57 t)
(declare-const c58 t)
(declare-const c59 t)
(declare-const c60 t)
(declare-const c61 t)
(declare-const c62 t)
(declare-const c63 t)
(declare-const c64 t)
(declare-const c65 t)
(declare-const c66 t)
(declare-const c67 t)
(declare-const c68 t)
(declare-const c69 t)
(declare-const c70 t)
(declare-const c71 t)
(declare-const c72 t)
(declare-const c73 t)
(declare-const c74 t)
(declare-const c75 t)
(declare-const c76 t)
(declare-const c77 t)
(declare-const c78 t)
(declare-const c79 t)
(declare-const c80 t)
(declare-const c81 t)
(declare-const c82 t)
(declare-const c83 t)
(declare-const c84 t)
(declare-const c85 t)
(declare-const c86 t)
(declare-const c87 t)
(declare-const c88 t)
(declare-const c89 t)
(declare-const c90 t)
(declare-const c91 t)
(declare-const c92 t)
(declare-const c93 t)
(declare-const c94 t)
(declare-const c95 t)
(declare-const c96 t)
(declare-const c97 t)
(declare-const c98 t)
(declare-const c99 t)
(declare-const c100 t)
(assert (= c1 c100))
(assert (not (= c1 T0)))
(assert (not (= c2 T0)))
(assert (not (= c3 T0)))
(assert (not (= c4 T0)))
(assert (not (= c5 T0)))
(assert (not (= c6 T0)))
(assert (not (= c7 T0)))
(assert (not (= c8 T0)))
(assert (not (= c9 T0)))
(assert (not (= c10 T0)))
(assert (not (= c11 T0)))
(assert (not (= c12 T0)))
(assert (not (= c13 T0)))
(assert (not (= c14 T0)))
(assert (not (= c15 T0)))
(assert (not (= c16 T0)))
(assert (not (= c17 T0)))
(assert (not (= c18 T0)))
(assert (not (= c19 T0)))
(assert (not (= c20 T0)))
(assert (not (= c21 T0)))
(assert (not (= c22 T0)))
(assert (not (= c23 T0)))
(assert (not (= c24 T0)))
(assert (not (= c25 T0)))
(assert (not (= c26 T0)))
(assert (not (= c27 T0)))
(assert (not (= c28 T0)))
(assert (not (= c29 T0)))
(assert (not (= c30 T0)))
(assert (not (= c31 T0)))
(assert (not (= c32 T0)))
(assert (not (= c33 T0)))
(assert (not (= c34 T0)))
(assert (not (= c35 T0)))
(assert (not (= c36 T0)))
(assert (not (= c37 T0)))
(assert (not (= c38 T0)))
(assert (not (= c39 T0)))
(assert (not (= c40 T0)))
(assert (not (= c41 T0)))
(assert (not (= c42 T0)))
(assert (not (= c43 T0)))
(assert (not (= c44 T0)))
(assert (not (= c45 T0)))
(assert (not (= c46 T0)))
(assert (not (= c47 T0)))
(assert (not (= c48 T0)))
(assert (not (= c49 T0)))
(assert (not (= c50 T0)))
(assert (not (= c51 T0)))
(assert (not (= c52 T0)))
(assert (not (= c53 T0)))
(assert (not (= c54 T0)))
(assert (not (= c55 T0)))
(assert (not (= c56 T0)))
(assert (not (= c57 T0)))
(assert (not (= c58 T0)))
(assert (not (= c59 T0)))
(assert (not (= c60 T0)))
(assert (not (= c61 T0)))
(assert (not (= c62 T0)))
(assert (not (= c63 T0)))
(assert (not (= c64 T0)))
(assert (not (= c65 T0)))
(assert (not (= c66 T0)))
(assert (not (= c67 T0)))
(assert (not (= c68 T0)))
(assert (not (= c69 T0)))
(assert (not (= c70 T0)))
(assert (not (= c71 T0)))
(assert (not (= c72 T0)))
(assert (not (= c73 T0)))
(assert (not (= c74 T0)))
(assert (not (= c75 T0)))
(assert (not (= c76 T0)))
(assert (not (= c77 T0)))
(assert (not (= c78 T0)))
(assert (not (= c79 T0)))
(assert (not (= c80 T0)))
(assert (not (= c81 T0)))
(assert (not (= c82 T0)))
(assert (not (= c83 T0)))
(assert (not (= c84 T0)))
(assert (not (= c85 T0)))
(assert (not (= c86 T0)))
(assert (not (= c87 T0)))
(assert (not (= c88 T0)))
(assert (not (= c89 T0)))
(assert (not (= c90 T0)))
(assert (not (= c91 T0)))
(assert (not (= c92 T0)))
(assert (not (= c93 T0)))
(assert (not (= c94 T0)))
(assert (not (= c95 T0)))
(assert (not (= c96 T0)))
(assert (not (= c97 T0)))
(assert (not (= c98 T0)))
(assert (not (= c99 T0)))
(assert (not (= c100 T0)))
(assert (or (= c1 (T1 c2)) (= c1 (T2 c2))))
(assert (or (= c2 (T1 c3)) (= c2 (T2 c3))))
(assert (or (= c3 (T1 c4)) (= c3 (T2 c4))))
(assert (or (= c4 (T1 c5)) (= c4 (T2 c5))))
(assert (or (= c5 (T1 c6)) (= c5 (T2 c6))))
(assert (or (= c6 (T1 c7)) (= c6 (T2 c7))))
(assert (or (= c7 (T1 c8)) (= c7 (T2 c8))))
(assert (or (= c8 (T1 c9)) (= c8 (T2 c9))))
(assert (or (= c9 (T1 c10)) (= c9 (T2 c10))))
(assert (or (= c10 (T1 c11)) (= c10 (T2 c11))))
(assert (or (= c11 (T1 c12)) (= c11 (T2 c12))))
(assert (or (= c12 (T1 c13)) (= c12 (T2 c13))))
(assert (or (= c13 (T1 c14)) (= c13 (T2 c14))))
(assert (or (= c14 (T1 c15)) (= c14 (T2 c15))))
(assert (or (= c15 (T1 c16)) (= c15 (T2 c16))))
(assert (or (= c16 (T1 c17)) (= c16 (T2 c17))))
(assert (or (= c17 (T1 c18)) (= c17 (T2 c18))))
(assert (or (= c18 (T1 c19)) (= c18 (T2 c19))))
(assert (or (= c19 (T1 c20)) (= c19 (T2 c20))))
(assert (or (= c20 (T1 c21)) (= c20 (T2 c21))))
(assert (or (= c21 (T1 c22)) (= c21 (T2 c22))))
(assert (or (= c22 (T1 c23)) (= c22 (T2 c23))))
(assert (or (= c23 (T1 c24)) (= c23 (T2 c24))))
(assert (or (= c24 (T1 c25)) (= c24 (T2 c25))))
(assert (or (= c25 (T1 c26)) (= c25 (T2 c26))))
(assert (or (= c26 (T1 c27)) (= c26 (T2 c27))))
(assert (or (= c27 (T1 c28)) (= c27 (T2 c28))))
(assert (or (= c28 (T1 c29)) (= c28 (T2 c29))))
(assert (or (= c29 (T1 c30)) (= c29 (T2 c30))))
(assert (or (= c30 (T1 c31)) (= c30 (T2 c31))))
(assert (or (= c31 (T1 c32)) (= c31 (T2 c32))))
(assert (or (= c32 (T1 c33)) (= c32 (T2 c33))))
(assert (or (= c33 (T1 c34)) (= c33 (T2 c34))))
(assert (or (= c34 (T1 c35)) (= c34 (T2 c35))))
(assert (or (= c35 (T1 c36)) (= c35 (T2 c36))))
(assert (or (= c36 (T1 c37)) (= c36 (T2 c37))))
(assert (or (= c37 (T1 c38)) (= c37 (T2 c38))))
(assert (or (= c38 (T1 c39)) (= c38 (T2 c39))))
(assert (or (= c39 (T1 c40)) (= c39 (T2 c40))))
(assert (or (= c40 (T1 c41)) (= c40 (T2 c41))))
(assert (or (= c41 (T1 c42)) (= c41 (T2 c42))))
(assert (or (= c42 (T1 c43)) (= c42 (T2 c43))))
(assert (or (= c43 (T1 c44)) (= c43 (T2 c44))))
(assert (or (= c44 (T1 c45)) (= c44 (T2 c45))))
(assert (or (= c45 (T1 c46)) (= c45 (T2 c46))))
(assert (or (= c46 (T1 c47)) (= c46 (T2 c47))))
(assert (or (= c47 (T1 c48)) (= c47 (T2 c48))))
(assert (or (= c48 (T1 c49)) (= c48 (T2 c49))))
(assert (or (= c49 (T1 c50)) (= c49 (T2 c50))))
(assert (or (= c50 (T1 c51)) (= c50 (T2 c51))))
(assert (or (= c51 (T1 c52)) (= c51 (T2 c52))))
(assert (or (= c52 (T1 c53)) (= c52 (T2 c53))))
(assert (or (= c53 (T1 c54)) (= c53 (T2 c54))))
(assert (or (= c54 (T1 c55)) (= c54 (T2 c55))))
(assert (or (= c55 (T1 c56)) (= c55 (T2 c56))))
(assert (or (= c56 (T1 c57)) (= c56 (T2 c57))))
(assert (or (= c57 (T1 c58)) (= c57 (T2 c58))))
(assert (or (= c58 (T1 c59)) (= c58 (T2 c59))))
(assert (or (= c59 (T1 c60)) (= c59 (T2 c60))))
(assert (or (= c60 (T1 c61)) (= c60 (T2 c61))))
(assert (or (= c61 (T1 c62)) (= c61 (T2 c62))))
(assert (or (= c62 (T1 c63)) (= c62 (T2 c63))))
(assert (or (= c63 (T1 c64)) (= c63 (T2 c64))))
(assert (or (= c64 (T1 c65)) (= c64 (T2 c65))))
(assert (or (= c65 (T1 c66)) (= c65 (T2 c66))))
(assert (or (= c66 (T1 c67)) (= c66 (T2 c67))))
(assert (or (= c67 (T1 c68)) (= c67 (T2 c68))))
(assert (or (= c68 (T1 c69)) (= c68 (T2 c69))))
(assert (or (= c69 (T1 c70)) (= c69 (T2 c70))))
(assert (or (= c70 (T1 c71)) (= c70 (T2 c71))))
(assert (or (= c71 (T1 c72)) (= c71 (T2 c72))))
(assert (or (= c72 (T1 c73)) (= c72 (T2 c73))))
(assert (or (= c73 (T1 c74)) (= c73 (T2 c74))))
(assert (or (= c74 (T1 c75)) (= c74 (T2 c75))))
(assert (or (= c75 (T1 c76)) (= c75 (T2 c76))))
(assert (or (= c76 (T1 c77)) (= c76 (T2 c77))))
(assert (or (= c77 (T1 c78)) (= c77 (T2 c78))))
(assert (or (= c78 (T1 c79)) (= c78 (T2 c79))))
(assert (or (= c79 (T1 c80)) (= c79 (T2 c80))))
(assert (or (= c80 (T1 c81)) (= c80 (T2 c81))))
(assert (or (= c81 (T1 c82)) (= c81 (T2 c82))))
(assert (or (= c82 (T1 c83)) (= c82 (T2 c83))))
(assert (or (= c83 (T1 c84)) (= c83 (T2 c84))))
(assert (or (= c84 (T1 c85)) (= c84 (T2 c85))))
(assert (or (= c85 (T1 c86)) (= c85 (T2 c86))))
(assert (or (= c86 (T1 c87)) (= c86 (T2 c87))))
(assert (or (= c87 (T1 c88)) (= c87 (T2 c88))))
(assert (or (= c88 (T1 c89)) (= c88 (T2 c89))))
(assert (or (= c89 (T1 c90)) (= c89 (T2 c90))))
(assert (or (= c90 (T1 c91)) (= c90 (T2 c91))))
(assert (or (= c91 (T1 c92)) (= c91 (T2 c92))))
(assert (or (= c92 (T1 c93)) (= c92 (T2 c93))))
(assert (or (= c93 (T1 c94)) (= c93 (T2 c94))))
(assert (or (= c94 (T1 c95)) (= c94 (T2 c95))))
(assert (or (= c95 (T1 c96)) (= c95 (T2 c96))))
(assert (or (= c96 (T1 c97)) (= c96 (T2 c97))))
(assert (or (= c97 (T1 c98)) (= c97 (T2 c98))))
(assert (or (= c98 (T1 c99)) (= c98 (T2 c99))))
(assert (or (= c99 (T1 c100)) (= c99 (T2 c100))))
(check-sat)
(exit)