prolog - When is the Redo-port called with new variables in Trace/0 and when not?

Question

During my implementation of the Adventure game in Prolog I was wondering when the redo-port is called with new variables during backtracking and when it is called with the same ones?

For example, I have the following knowledge base:

location(desk,office).
location(apple,kitchen).
location(flashlight,desk).
location('washing machine',cellar).
location(nani,'washing machine').
location(broccoli,kitchen).
location(crackers,kitchen).
location(computer,office).

door(office,hall).
door(kitchen,office).
door(hall,'dining room').
door(kitchen,cellar).
door('dining room',kitchen).

When tracing the query ?-(location(X,Y),door(kitchen,Y)). I get this:

   Call: (9) location(_7998, _8000) ? creep
   Exit: (9) location(desk, office) ? creep
   Call: (9) door(kitchen, office) ? creep
   Exit: (9) door(kitchen, office) ? creep
X = desk,
Y = office ;
   Redo: (9) door(kitchen, office) ? creep      <==== 1
   Fail: (9) door(kitchen, office) ? creep
   Redo: (9) location(_7998, _8000) ? creep
   Exit: (9) location(apple, kitchen) ? creep
   Call: (9) door(kitchen, kitchen) ? creep
   Fail: (9) door(kitchen, kitchen) ? creep
   Redo: (9) location(_7998, _8000) ? creep
   Exit: (9) location(flashlight, desk) ? creep
   Call: (9) door(kitchen, desk) ? creep
   Fail: (9) door(kitchen, desk) ? creep
   Redo: (9) location(_7998, _8000) ? creep
   Exit: (9) location('washing machine', cellar) ? creep
   Call: (9) door(kitchen, cellar) ? creep
   Exit: (9) door(kitchen, cellar) ? creep
X = 'washing machine',
Y = cellar ;
   Redo: (9) location(_7998, _8000) ? creep    <==== 2
   Exit: (9) location(nani, 'washing machine') ? creep
   Call: (9) door(kitchen, 'washing machine') ? creep
   Fail: (9) door(kitchen, 'washing machine') ? creep
   Redo: (9) location(_7998, _8000) ? creep
   Exit: (9) location(broccoli, kitchen) ? creep

   Call: (9) door(kitchen, kitchen) ? creep
   Fail: (9) door(kitchen, kitchen) ? creep
   Redo: (9) location(_7998, _8000) ? creep
   Exit: (9) location(crackers, kitchen) ? creep
   Call: (9) door(kitchen, kitchen) ? creep
   Fail: (9) door(kitchen, kitchen) ? creep
   Redo: (9) location(_7998, _8000) ? creep
   Exit: (9) location(computer, office) ? creep
   Call: (9) door(kitchen, office) ? creep
   Exit: (9) door(kitchen, office) ? creep
X = computer,
Y = office ;
   Redo: (9) door(kitchen, office) ? creep    <==== 3
   Fail: (9) door(kitchen, office) ? creep
false.

I understand how the binding of the variables works, but I do not understand why Prolog returns

Redo: (9) door(kitchen, office) ? creep <==== 1
Redo: (9) door(kitchen, office) ? creep <==== 3

after finding the first solution (and the same for the last solution),

while it immediately looks for a new binding of X and Y after the second solution

Redo: (9) location(_7998, _8000) ? creep <==== 2

Why does it not immediately continue to look for a new binding of X and Y after the first and last solution, instead of resorting to

Redo: (9) door(kitchen, office) ? creep <==== 3

(which fails anyway)?

(I found a similar question here, but unfortunately my reputation does not allow me to comment over there and I think this particular issue does not have to do with my Prolog version (as I tried it with SWI-Prolog and GNUProlog))

Thanks in advance for offering any clarity.

Answer 1

This is just a comment posted as a answer because it has a picture.

If you use the graphical debugger you can see when choice points are created.

?- gtrace.
true.

[trace] ?- (location(X,Y),door(kitchen,Y)).

In the following image of the debugger I highlighted the choice point with a green rectangle.

To exit out of trace mode in top-level enter nodebug.

[trace] ?- nodebug.
true.

?- 

Note: It is the choice points that lead to using the redo port.
Note: Another way to debug prolog is via use of failure slice. Also read questions tagged with failure slice