Context: suppose $\phi$ is a formula in the Guarded Fragment of First Order Logic, $\phi$ is without constants and without function symbols. Let $I$ be a finite set, $(R_i)_{i \in I}$ relation symbols and $C$ a finite set of constants. Let $A = \{R_i(a_1,...a_{n_i}) \ | \ i \in I, a_j \in C\}$, that is, $A$ is is a finite set of assertions (suppose arities of relation symbols are of course respected). The expression $\phi \wedge \bigwedge_{\varphi \in A}\varphi$ is inconsistent if no model of it exists.
The question is: let $\phi$ be such a formula, can we compute a bound $M$ such that if $A$ is a finite set of assertions and $\phi \wedge \bigwedge_{\varphi \in A}\varphi$ is inconsistent then there exists $A' \subseteq A$ with $|A'| \le M$ and $\phi \wedge \bigwedge_{\varphi \in A'}\varphi$ inconsistent.