Termination of the given JBC could be proven:

(0) Obligation:

JBC Problem based on JBC Program:

public class Hanoi {
    private void solve(int h, int from, int to, int support) {
	if (h < 1) return;
	else if (h == 1) {
	    //System.out.println("from " + from + " to " + to + "\n");
	}
	else {
	    solve(h - 1, from, support, to);
	    //System.out.println("from " + from + " to " + to + "\n");
	    solve(h - 1, support, to, from);
	}
    }

    public static void main(String[] args) {
	new Hanoi().solve(5,1,2,3);
    }
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
Hanoi.main([Ljava/lang/String;)V: Graph of 509 nodes with 0 SCCs.

(3) TerminationGraphToSCCProof (SOUND transformation)

Proven termination by absence of SCCs

(4) TRUE