Removing unnecessary variables from Horn clause verification conditions