A Function Elimination Method for Checking Satisfiability of Arithmetical Logics