Clause ewffs are restricted to clause variables.
Having additional variables in ewffs makes no sense, but could make subsumption tests incomplete. For safety, the constructor ensures that the ewff mentions no additional variables now.
Loading
Please register or sign in to comment