is from x  to x , so the next variable instantiated in BT at this node is x . Under such an ordering, BT avoids instantiating x  and visits fewer nodes than CBJ. Then BT instantiates x  to 2, x  to 0, and x  to 0, and finds the first solution.

a priori 4. Maintaining Consistency and Backjumping k:
backjump level k:
l k k