No, it is not a contradiction since in predicate logic, you can do bounded renaming which means you can rename bounded variables as you like. Hence, the above formula is equivalent to

∀t1.(t0 ≤ t1 → (∃t3.t1 ≤ t3 ∧ (∀t2. (t1 ≤ t2 ∧ t2 < t3 → c[t2])) ∧ b[t3] ) ∨ a[t1])