8A new generated state s2 (possibly with variables) is folded into a previously generated state s1 (possibly with variables, different from those of s2) if s2 is an instance of s1 modulo axioms and variant equations.