Mapping of variables to constants should be different from existing constants

[mudbri]

Currently, when a rule is treated as an instance, we map variables to distinct constants. Although each variable is assigned to a distinct constant, these assignments do not consider the existing constants into account. Consider the programs:

p1 = "l(3,4) :- l(1,3), k(2,1,3), l(1,5)"
p2 = "l(3,4) :- l(y,c), k(d,y,e), l(f,g)"

Clearly, p1 does not contain p2. However, if the mapping of variables in p2 happens to be something like y=1, c=3, d=2, e=3, f=1, g=5, then containment would hold. The key is that any mapping variable to distinct constants should never be equal to any other constant in the programs we want to check. This is tricky in general, since when considering program p2 as an instance, we do not know the constants of program p1, so it's not straight forward how we can make them unique

[mudbri]

Potential solution to the problem is in the first comment in this issue