Hola, tengo la duda de que esta sucediendo en este caso.
Tomando:
Ts = [x],
Es = [[a,b]],
S = [x,c],
W = [b,a,c],
R = [b,a,c]
Debería satisfacer el predicado de la linea 45, y de hecho, consultando por cada parte por separado dan todas true, pero no encuentra la solución al preguntar con la Variable Q (ni poniendo [b,a,c]) . Tampoco se va por una rama infinita porque termina con false. ¿Tiene relación con el funcionamiento de \=?