Question: Given $\Sigma = \lbrace c , R_1^2, ... , R_k^2 \rbrace $ when c is a constant. Prove / disprove that exists an finite time algorithm for deciding satisfiability of a universal statement A.
My proof: True: Due to Herbrand's theorem, a universal statement is satisfiable $\iff$ all of it's ground instances are satisfiable. Since there are no function symbols then this just means checking $c$ in every ground instance of the statement A and this is finite as the statement is of finite length.
I want to make sure that this argument is indeed true.