Variable value not found

[flexoron]

v2.39.2

$ tpl
?- X = [Z,1|Z],append([Z],[Z|Z],[X,Z,Z,Y|Z]),write(Y),nl.
_2                           % unexpected
   X = [Z,1|Z], Z = [Z,1|Z]. % Y = 1 not found
?-

Howto find Y = 1

?- X = [Z,1|Z],append([Z],[Z|Z],[X,A,A,Y|Z]),write(Y),nl.
_3
   X = [Z,1|Z], Z = [Z,1|Z], A = [Z,1|Z]. % Not yet

?- X = [Z,1|Z],append([Z],[Z|Z],[X,A,B,Y|Z]),write(Y),nl.
1
   X = [Z,1|Z], Z = [Z,1|Z], A = [Z,1|Z], B = [Z,1|Z], Y = 1. % Now, involving Z = A = B (= valuable scrap)

?- X = [Z,1|Z],append([Z],[Z|Z],[X,_,_,Y|Z]),write(Y),nl. % scrap scrapped
1
   X = [Z,1|Z], Z = [Z,1|Z], Y = 1.

[infradig]

Simplifying

?- append([Z],[Z|Z],[[Z,1|Z],Z,Z,Y|Z]).
Z = [Z,1|Z].

Then changing the definition of

append([], R, R).
append([X|L], R, [X|S]) :- append(L, R, S).

to

append([], R, R).
append([X1|L], R, [X2|S]) :- append(L, R, S), X1 = X2.

gives

?- append([Z],[Z|Z],[[Z,1|Z],Z,Z,Y|Z]).
Z = [Z,1|Z], Y = 1.

So something in unification involving, you guessed it, cyclic terms it seems.