.
The resolution path I gave with templates is OK (only templates[1] eliminations and assertions appear in it).
However, this doesn't imply that the template-depth is 1 (and my answer to rjamil was incorrect).
The template-depth is 2.
No template[2] elimination appeared in my path because ?*print-templates* was set to FALSE (by default). (If TRUE, most of the time, there's a deluge of intermediate eliminations of templates[k], k>1.) If I set it to TRUE, the resolution path gives more detail:
- Code: Select all
Retracting a template[1] for digit 2 incompatible with all the templates[1] for digit 7
Retracting a template[1] for digit 2 incompatible with all the templates[1] for digit 7
Retracting a template[1] for digit 2 incompatible with all the templates[1] for digit 5
candidate in no template[1] for digit 2 ==> r9c2≠2
whip[1]: r9n2{c5 .} ==> r7c5≠2
singles ==> r7c5=1, r9c2=1
Retracting a template[1] for digit 2 incompatible with all the templates[1] for digit 5
candidate in no template[1] for digit 2 ==> r3c3≠2
singles ==> r3c3=9, r2c6=9
candidate common to all the templates[1] for digit 7 ==> r1c7=7
singles ==> r1c2=2, r2c3=6, r7c3=2, r7c2=6
candidate in no template[1] for digit 7 ==> r9c4≠7
Retracting a template[1] for digit 2 incompatible with all the templates[1] for digit 5
candidate common to all the templates[1] for digit 2 ==> r5c8=2
As for the starting point after whips[1], it's justified because any whip[1] elimination can be done by a template[1] (obvious).
.
