Any ideas what causes this exception?
exception THM 1 raised (line 700 of "drule.ML"): COMP S :000 :001 [S :000 :001] ?r ?a ?b ⟹ ?r⇧+⇧+ ?a ?b
The problem is that there are multiple unifiers. I am not yet sure how to fix it.
Hmm. Is first-order matching enough for you, perhaps? Otherwise you could try instantiating things manually.
Last updated: Dec 07 2023 at 12:30 UTC