answer(3, [[left, right], [left, center], [right, center], [left, right], [center, left], [center, right], [left, right]]).
why(
  answer(3, [[left, right], [left, center], [right, center], [left, right], [center, left], [center, right], [left, right]]),
  proof(
    goal(answer(3, [[left, right], [left, center], [right, center], [left, right], [center, left], [center, right], [left, right]])),
    by(rule("hanoi.pl", clause(4))),
    bindings([binding("Moves", [[left, right], [left, center], [right, center], [left, right], [center, left], [center, right], [left, right]])]),
    uses([
      proof(
        goal(hanoi(3, left, right, center, [[left, right], [left, center], [right, center], [left, right], [center, left], [center, right], [left, right]])),
        by(rule("hanoi.pl", clause(3))),
        bindings([binding("N", 3), binding("From", left), binding("To", right), binding("Via", center), binding("Moves", [[left, right], [left, center], [right, center], [left, right], [center, left], [center, right], [left, right]]), binding("N1", 2), binding("Before", [[left, right], [left, center], [right, center]]), binding("After", [[center, left], [center, right], [left, right]])]),
        uses([
          proof(
            goal(gt(3, 0)),
            by(builtin(gt, 2))
          ),
          proof(
            goal(sub(3, 1, 2)),
            by(builtin(sub, 3))
          ),
          proof(
            goal(hanoi(2, left, center, right, [[left, right], [left, center], [right, center]])),
            by(rule("hanoi.pl", clause(3))),
            bindings([binding("N", 2), binding("From", left), binding("To", center), binding("Via", right), binding("Moves", [[left, right], [left, center], [right, center]]), binding("N1", 1), binding("Before", [[left, right]]), binding("After", [[right, center]])]),
            uses([
              proof(
                goal(gt(2, 0)),
                by(builtin(gt, 2))
              ),
              proof(
                goal(sub(2, 1, 1)),
                by(builtin(sub, 3))
              ),
              proof(
                goal(hanoi(1, left, right, center, [[left, right]])),
                by(rule("hanoi.pl", clause(3))),
                bindings([binding("N", 1), binding("From", left), binding("To", right), binding("Via", center), binding("Moves", [[left, right]]), binding("N1", 0), binding("Before", []), binding("After", [])]),
                uses([
                  proof(
                    goal(gt(1, 0)),
                    by(builtin(gt, 2))
                  ),
                  proof(
                    goal(sub(1, 1, 0)),
                    by(builtin(sub, 3))
                  ),
                  proof(
                    goal(hanoi(0, left, center, right, [])),
                    by(fact("hanoi.pl", clause(2))),
                    bindings([binding("_from", left), binding("_to", center), binding("_via", right)])
                  ),
                  proof(
                    goal(hanoi(0, center, right, left, [])),
                    by(fact("hanoi.pl", clause(2))),
                    bindings([binding("_from", center), binding("_to", right), binding("_via", left)])
                  ),
                  proof(
                    goal(append([], [[left, right]], [[left, right]])),
                    by(builtin(append, 3))
                  )
                ])
              ),
              proof(
                goal(hanoi(1, right, center, left, [[right, center]])),
                by(rule("hanoi.pl", clause(3))),
                bindings([binding("N", 1), binding("From", right), binding("To", center), binding("Via", left), binding("Moves", [[right, center]]), binding("N1", 0), binding("Before", []), binding("After", [])]),
                uses([
                  proof(
                    goal(gt(1, 0)),
                    by(builtin(gt, 2))
                  ),
                  proof(
                    goal(sub(1, 1, 0)),
                    by(builtin(sub, 3))
                  ),
                  proof(
                    goal(hanoi(0, right, left, center, [])),
                    by(fact("hanoi.pl", clause(2))),
                    bindings([binding("_from", right), binding("_to", left), binding("_via", center)])
                  ),
                  proof(
                    goal(hanoi(0, left, center, right, [])),
                    by(fact("hanoi.pl", clause(2))),
                    bindings([binding("_from", left), binding("_to", center), binding("_via", right)])
                  ),
                  proof(
                    goal(append([], [[right, center]], [[right, center]])),
                    by(builtin(append, 3))
                  )
                ])
              ),
              proof(
                goal(append([[left, right]], [[left, center], [right, center]], [[left, right], [left, center], [right, center]])),
                by(builtin(append, 3))
              )
            ])
          ),
          proof(
            goal(hanoi(2, center, right, left, [[center, left], [center, right], [left, right]])),
            by(rule("hanoi.pl", clause(3))),
            bindings([binding("N", 2), binding("From", center), binding("To", right), binding("Via", left), binding("Moves", [[center, left], [center, right], [left, right]]), binding("N1", 1), binding("Before", [[center, left]]), binding("After", [[left, right]])]),
            uses([
              proof(
                goal(gt(2, 0)),
                by(builtin(gt, 2))
              ),
              proof(
                goal(sub(2, 1, 1)),
                by(builtin(sub, 3))
              ),
              proof(
                goal(hanoi(1, center, left, right, [[center, left]])),
                by(rule("hanoi.pl", clause(3))),
                bindings([binding("N", 1), binding("From", center), binding("To", left), binding("Via", right), binding("Moves", [[center, left]]), binding("N1", 0), binding("Before", []), binding("After", [])]),
                uses([
                  proof(
                    goal(gt(1, 0)),
                    by(builtin(gt, 2))
                  ),
                  proof(
                    goal(sub(1, 1, 0)),
                    by(builtin(sub, 3))
                  ),
                  proof(
                    goal(hanoi(0, center, right, left, [])),
                    by(fact("hanoi.pl", clause(2))),
                    bindings([binding("_from", center), binding("_to", right), binding("_via", left)])
                  ),
                  proof(
                    goal(hanoi(0, right, left, center, [])),
                    by(fact("hanoi.pl", clause(2))),
                    bindings([binding("_from", right), binding("_to", left), binding("_via", center)])
                  ),
                  proof(
                    goal(append([], [[center, left]], [[center, left]])),
                    by(builtin(append, 3))
                  )
                ])
              ),
              proof(
                goal(hanoi(1, left, right, center, [[left, right]])),
                by(rule("hanoi.pl", clause(3))),
                bindings([binding("N", 1), binding("From", left), binding("To", right), binding("Via", center), binding("Moves", [[left, right]]), binding("N1", 0), binding("Before", []), binding("After", [])]),
                uses([
                  proof(
                    goal(gt(1, 0)),
                    by(builtin(gt, 2))
                  ),
                  proof(
                    goal(sub(1, 1, 0)),
                    by(builtin(sub, 3))
                  ),
                  proof(
                    goal(hanoi(0, left, center, right, [])),
                    by(fact("hanoi.pl", clause(2))),
                    bindings([binding("_from", left), binding("_to", center), binding("_via", right)])
                  ),
                  proof(
                    goal(hanoi(0, center, right, left, [])),
                    by(fact("hanoi.pl", clause(2))),
                    bindings([binding("_from", center), binding("_to", right), binding("_via", left)])
                  ),
                  proof(
                    goal(append([], [[left, right]], [[left, right]])),
                    by(builtin(append, 3))
                  )
                ])
              ),
              proof(
                goal(append([[center, left]], [[center, right], [left, right]], [[center, left], [center, right], [left, right]])),
                by(builtin(append, 3))
              )
            ])
          ),
          proof(
            goal(append([[left, right], [left, center], [right, center]], [[left, right], [center, left], [center, right], [left, right]], [[left, right], [left, center], [right, center], [left, right], [center, left], [center, right], [left, right]])),
            by(builtin(append, 3))
          )
        ])
      )
    ])
  )
).