Termination of the given JBC could be proven:

(0) Obligation:

JBC Problem based on JBC Program:

public class HanoiR {
    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) {
	Random.args = args;
	new HanoiR().solve(Random.random(),1,2,3);
    }
}


public class Random {
  static String[] args;
  static int index = 0;

  public static int random() {
      if (index >= args.length)
	  return 0;

      String string = args[index];
      index++;
      return string.length();
  }
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

HanoiR.solve(IIII)V: Graph of 43 nodes with 0 SCCs.

(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 1 SCCs.

(4) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: HanoiR.solve(IIII)V
SCC calls the following helper methods: HanoiR.solve(IIII)V
Performed SCC analyses:

• Used field analysis yielded the following read fields:
  
• Marker field analysis yielded the following relations that could be markers:
  

(5) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 35 IRules

P rules:
f830_0_solve_ConstantStackPush(EOS, i202, i202, i202) → f833_0_solve_GE(EOS, i202, i202, i202, 1)
f833_0_solve_GE(EOS, i212, i212, i212, matching1) → f837_0_solve_GE(EOS, i212, i212, i212, 1) | =(matching1, 1)
f837_0_solve_GE(EOS, i212, i212, i212, matching1) → f840_0_solve_Load(EOS, i212, i212) | &&(>=(i212, 1), =(matching1, 1))
f840_0_solve_Load(EOS, i212, i212) → f844_0_solve_ConstantStackPush(EOS, i212, i212, i212)
f844_0_solve_ConstantStackPush(EOS, i212, i212, i212) → f898_0_solve_NE(EOS, i212, i212, i212, 1)
f898_0_solve_NE(EOS, i241, i241, i241, matching1) → f908_0_solve_NE(EOS, i241, i241, i241, 1) | =(matching1, 1)
f908_0_solve_NE(EOS, i241, i241, i241, matching1) → f920_0_solve_Load(EOS, i241, i241) | &&(>(i241, 1), =(matching1, 1))
f920_0_solve_Load(EOS, i241, i241) → f924_0_solve_Load(EOS, i241, i241)
f924_0_solve_Load(EOS, i241, i241) → f927_0_solve_ConstantStackPush(EOS, i241, i241, i241)
f927_0_solve_ConstantStackPush(EOS, i241, i241, i241) → f956_0_solve_IntArithmetic(EOS, i241, i241, i241, 1)
f956_0_solve_IntArithmetic(EOS, i241, i241, i241, matching1) → f963_0_solve_Load(EOS, i241, i241, -(i241, 1)) | &&(>(i241, 0), =(matching1, 1))
f963_0_solve_Load(EOS, i241, i241, i260) → f965_0_solve_Load(EOS, i241, i241, i260)
f965_0_solve_Load(EOS, i241, i241, i260) → f966_0_solve_Load(EOS, i241, i241, i260)
f966_0_solve_Load(EOS, i241, i241, i260) → f968_0_solve_InvokeMethod(EOS, i241, i241, i260)
f968_0_solve_InvokeMethod(EOS, i241, i241, i260) → f969_0_solve_Load(EOS, i260, i260)
f968_0_solve_InvokeMethod(EOS, i241, i241, i260) → f969_1_solve_Load(EOS, i241, i241, i260, i260)
f969_0_solve_Load(EOS, i260, i260) → f971_0_solve_Load(EOS, i260, i260)
f971_0_solve_Load(EOS, i260, i260) → f828_0_solve_Load(EOS, i260, i260)
f828_0_solve_Load(EOS, i202, i202) → f830_0_solve_ConstantStackPush(EOS, i202, i202, i202)
f997_0_solve_Return(EOS, i241, i241, matching1) → f1121_0_solve_Return(EOS, i241, i241, 1) | =(matching1, 1)
f1121_0_solve_Return(EOS, i241, i241, i418) → f1124_0_solve_Load(EOS, i241, i241)
f1124_0_solve_Load(EOS, i241, i241) → f1126_0_solve_Load(EOS, i241, i241)
f1126_0_solve_Load(EOS, i241, i241) → f1127_0_solve_ConstantStackPush(EOS, i241, i241)
f1127_0_solve_ConstantStackPush(EOS, i241, i241) → f1129_0_solve_IntArithmetic(EOS, i241, i241, 1)
f1129_0_solve_IntArithmetic(EOS, i241, i241, matching1) → f1130_0_solve_Load(EOS, i241, -(i241, 1)) | &&(>(i241, 0), =(matching1, 1))
f1130_0_solve_Load(EOS, i241, i428) → f1132_0_solve_Load(EOS, i241, i428)
f1132_0_solve_Load(EOS, i241, i428) → f1133_0_solve_Load(EOS, i241, i428)
f1133_0_solve_Load(EOS, i241, i428) → f1135_0_solve_InvokeMethod(EOS, i241, i428)
f1135_0_solve_InvokeMethod(EOS, i241, i428) → f1136_0_solve_Load(EOS, i428, i428)
f1135_0_solve_InvokeMethod(EOS, i241, i428) → f1136_1_solve_Load(EOS, i241, i428, i428)
f1136_0_solve_Load(EOS, i428, i428) → f1138_0_solve_Load(EOS, i428, i428)
f1138_0_solve_Load(EOS, i428, i428) → f828_0_solve_Load(EOS, i428, i428)
f1307_0_solve_Return(EOS, i241, i241, i602) → f1121_0_solve_Return(EOS, i241, i241, i602)
f969_1_solve_Load(EOS, i241, i241, matching1, matching2) → f997_0_solve_Return(EOS, i241, i241, 1) | &&(=(matching1, 1), =(matching2, 1))
f969_1_solve_Load(EOS, i241, i241, i602, i602) → f1307_0_solve_Return(EOS, i241, i241, i602)

Combined rules. Obtained 5 IRules

P rules:
f1135_0_solve_InvokeMethod(EOS, i241, i428) → f1136_1_solve_Load(EOS, i241, i428, i428)
f830_0_solve_ConstantStackPush(EOS, x0, x0, x0) → f830_0_solve_ConstantStackPush(EOS, -(x0, 1), -(x0, 1), -(x0, 1)) | >(x0, 1)
f1135_0_solve_InvokeMethod(EOS, x0, x1) → f830_0_solve_ConstantStackPush(EOS, x1, x1, x1)
f830_0_solve_ConstantStackPush(EOS, 2, 2, 2) → f1135_0_solve_InvokeMethod(EOS, 2, 1)
f830_0_solve_ConstantStackPush(EOS, x0, x0, x0) → f1135_0_solve_InvokeMethod(EOS, x0, -(x0, 1)) | >(x0, 1)

Filtered ground terms:

f1135_0_solve_InvokeMethod(x1, x2, x3) → f1135_0_solve_InvokeMethod(x2, x3)
f1136_1_solve_Load(x1, x2, x3, x4) → f1136_1_solve_Load(x2, x3, x4)
f830_0_solve_ConstantStackPush(x1, x2, x3, x4) → f830_0_solve_ConstantStackPush(x2, x3, x4)
Cond_f830_0_solve_ConstantStackPush(x1, x2, x3, x4, x5) → Cond_f830_0_solve_ConstantStackPush(x1, x3, x4, x5)
Cond_f830_0_solve_ConstantStackPush1(x1, x2, x3, x4, x5) → Cond_f830_0_solve_ConstantStackPush1(x1, x3, x4, x5)

Filtered duplicate terms:

f1136_1_solve_Load(x1, x2, x3) → f1136_1_solve_Load(x1, x3)
f830_0_solve_ConstantStackPush(x1, x2, x3) → f830_0_solve_ConstantStackPush(x3)
Cond_f830_0_solve_ConstantStackPush(x1, x2, x3, x4) → Cond_f830_0_solve_ConstantStackPush(x1, x4)
Cond_f830_0_solve_ConstantStackPush1(x1, x2, x3, x4) → Cond_f830_0_solve_ConstantStackPush1(x1, x4)

Filtered unneeded terms:

f1135_0_solve_InvokeMethod(x1, x2) → f1135_0_solve_InvokeMethod(x2)

Prepared 5 rules for path length conversion:

P rules:
f1135_0_solve_InvokeMethod(i428) → f1136_1_solve_Load(i241, i428)
f830_0_solve_ConstantStackPush(x0) → f830_0_solve_ConstantStackPush(-(x0, 1)) | >(x0, 1)
f1135_0_solve_InvokeMethod(x1) → f830_0_solve_ConstantStackPush(x1)
f830_0_solve_ConstantStackPush(2) → f1135_0_solve_InvokeMethod(1)
f830_0_solve_ConstantStackPush(x0) → f1135_0_solve_InvokeMethod(-(x0, 1)) | >(x0, 1)

Finished conversion. Obtained 4 rules.

P rules:
f830_0_solve_ConstantStackPush(x2) → f830_0_solve_ConstantStackPush(-(x2, 1)) | >(x2, 1)
f1135_0_solve_InvokeMethod(x3) → f830_0_solve_ConstantStackPush(x3)
f830_0_solve_ConstantStackPush(c2) → f1135_0_solve_InvokeMethod(1) | =(2, c2)
f830_0_solve_ConstantStackPush(x4) → f1135_0_solve_InvokeMethod(-(x4, 1)) | >(x4, 1)

(6) Obligation:

Rules:
f830_0_solve_ConstantStackPush(x2) → f830_0_solve_ConstantStackPush(-(x2, 1)) | >(x2, 1)
f1135_0_solve_InvokeMethod(x3) → f830_0_solve_ConstantStackPush(x3)
f830_0_solve_ConstantStackPush(c2) → f1135_0_solve_InvokeMethod(1) | =(2, c2)
f830_0_solve_ConstantStackPush(x4) → f1135_0_solve_InvokeMethod(-(x4, 1)) | >(x4, 1)

(7) PolynomialOrderProcessor (SOUND transformation)

Found the following polynomial interpretation:

[f830_0_solve_ConstantStackPush(x5)] = -1 + x5
[f1135_0_solve_InvokeMethod(x8)] = -1 + x8

Therefore the following rule(s) have been dropped:

f830_0_solve_ConstantStackPush(x0) → f830_0_solve_ConstantStackPush(-(x0, 1)) | >(x0, 1)
f830_0_solve_ConstantStackPush(x2) → f1135_0_solve_InvokeMethod(1) | =(2, x2)
f830_0_solve_ConstantStackPush(x3) → f1135_0_solve_InvokeMethod(-(x3, 1)) | >(x3, 1)

(8) Obligation:

Rules:
f1135_0_solve_InvokeMethod(x1) → f830_0_solve_ConstantStackPush(x1) | TRUE

(9) TerminationGraphProcessor (EQUIVALENT transformation)

Constructed the termination graph and obtained no non-trivial SCC(s).

(10) YES