The following theory contains a comprehension axiom that is a naive like schema. This theory definitely looks inconsistent at first glance. However, I tried to find this inconsistency, but to no avail. The main idea pivotes around an acyclic membership relation $\in^*$, so an acyclic member of a set is an element of a set that doesn't contain that set in its transitive closure. Now, this theory allows free construction of sets after all formulas in the language FOL(=, $\in^*$).

Lanauge: the first order language of set theory.

Extesnionality: $\forall x \, (x \in A \leftrightarrow x \in B) \to A=B$

Transitive Closures: $\forall x \exists t: t=TC(x)$

Define: $t=TC(x) \iff trs(t) \land x \subseteq t \land \forall k (trs(k) \land x \subseteq k \to t \subseteq k)$

Where "$trs$" stands for "is transitive", that is: closure under relation $\in$

Induction: if $\phi$ is formula, then:

$$\forall y \in x (\phi) \land \forall k \, (\phi(k) \to \forall l \in k (\phi(l))) \to \\ \forall m \in TC(x)( \phi(m))$$

Define: $y \in^* x \iff y \in x \land \neg \, x \in TC(y)$

Comprehension: $\exists x \forall y \, (y \in x \iff \phi^*)$

Where $\phi^*$ is a formula not using $``x"$, whose predicates are among $=, \in^*$ symbols.

Questions:

Is there a clear inconsistency with this theory?

If not, then can this theory prove Infinity?