Termination of the given JBC could be proven:

(0) Obligation:

JBC Problem based on JBC Program:

public class AckermannR {

    public static int ack(int m, int n) {
	if (m <= 0) return n + 1;
	else if (n <= 0) return ack(m - 1,1);
	else return ack(m - 1,ack(m,n - 1));
    }

    public static void main(String[] args) {
	Random.args = args;
	ack(Random.random(),Random.random());
    }
}

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:
AckermannR.main([Ljava/lang/String;)V: Graph of 176 nodes with 0 SCCs.

AckermannR.ack(II)I: Graph of 52 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: AckermannR.ack(II)I
SCC calls the following helper methods: AckermannR.ack(II)I
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 41 IRules

P rules:
f572_0_ack_GT(EOS, i106, i101, i106, i101, i106) → f577_0_ack_GT(EOS, i106, i101, i106, i101, i106)
f577_0_ack_GT(EOS, i106, i101, i106, i101, i106) → f584_0_ack_Load(EOS, i106, i101, i106, i101) | >(i106, 0)
f584_0_ack_Load(EOS, i106, i101, i106, i101) → f594_0_ack_GT(EOS, i106, i101, i106, i101, i101)
f594_0_ack_GT(EOS, i106, matching1, i106, matching2, matching3) → f604_0_ack_GT(EOS, i106, 0, i106, 0, 0) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f594_0_ack_GT(EOS, i106, i109, i106, i109, i109) → f605_0_ack_GT(EOS, i106, i109, i106, i109, i109)
f604_0_ack_GT(EOS, i106, matching1, i106, matching2, matching3) → f614_0_ack_Load(EOS, i106, 0, i106, 0) | &&(&&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0)), =(matching3, 0))
f614_0_ack_Load(EOS, i106, matching1, i106, matching2) → f635_0_ack_ConstantStackPush(EOS, i106, 0, i106, 0, i106) | &&(=(matching1, 0), =(matching2, 0))
f635_0_ack_ConstantStackPush(EOS, i106, matching1, i106, matching2, i106) → f716_0_ack_IntArithmetic(EOS, i106, 0, i106, 0, i106, 1) | &&(=(matching1, 0), =(matching2, 0))
f716_0_ack_IntArithmetic(EOS, i106, matching1, i106, matching2, i106, matching3) → f744_0_ack_ConstantStackPush(EOS, i106, 0, i106, 0, -(i106, 1)) | &&(&&(&&(>(i106, 0), =(matching1, 0)), =(matching2, 0)), =(matching3, 1))
f744_0_ack_ConstantStackPush(EOS, i106, matching1, i106, matching2, i147) → f752_0_ack_InvokeMethod(EOS, i106, 0, i106, 0, i147, 1) | &&(=(matching1, 0), =(matching2, 0))
f752_0_ack_InvokeMethod(EOS, i106, matching1, i106, matching2, i147, matching3) → f761_0_ack_Load(EOS, i147, 1, i147, 1) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 1))
f752_0_ack_InvokeMethod(EOS, i106, matching1, i106, matching2, i147, matching3) → f761_1_ack_Load(EOS, i106, 0, i106, 0, i147, 1, i147, 1) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 1))
f761_0_ack_Load(EOS, i147, matching1, i147, matching2) → f773_0_ack_Load(EOS, i147, 1, i147, 1) | &&(=(matching1, 1), =(matching2, 1))
f773_0_ack_Load(EOS, i147, matching1, i147, matching2) → f554_0_ack_Load(EOS, i147, 1, i147, 1) | &&(=(matching1, 1), =(matching2, 1))
f554_0_ack_Load(EOS, i100, i101, i100, i101) → f572_0_ack_GT(EOS, i100, i101, i100, i101, i100)
f605_0_ack_GT(EOS, i106, i109, i106, i109, i109) → f619_0_ack_Load(EOS, i106, i109, i106, i109) | >(i109, 0)
f619_0_ack_Load(EOS, i106, i109, i106, i109) → f642_0_ack_ConstantStackPush(EOS, i106, i109, i106, i109, i106)
f642_0_ack_ConstantStackPush(EOS, i106, i109, i106, i109, i106) → f739_0_ack_IntArithmetic(EOS, i106, i109, i106, i109, i106, 1)
f739_0_ack_IntArithmetic(EOS, i106, i109, i106, i109, i106, matching1) → f747_0_ack_Load(EOS, i106, i109, i106, i109, -(i106, 1)) | &&(>(i106, 0), =(matching1, 1))
f747_0_ack_Load(EOS, i106, i109, i106, i109, i148) → f757_0_ack_Load(EOS, i106, i109, i109, i148, i106)
f757_0_ack_Load(EOS, i106, i109, i109, i148, i106) → f767_0_ack_ConstantStackPush(EOS, i106, i109, i148, i106, i109)
f767_0_ack_ConstantStackPush(EOS, i106, i109, i148, i106, i109) → f778_0_ack_IntArithmetic(EOS, i106, i109, i148, i106, i109, 1)
f778_0_ack_IntArithmetic(EOS, i106, i109, i148, i106, i109, matching1) → f786_0_ack_InvokeMethod(EOS, i106, i109, i148, i106, -(i109, 1)) | &&(>(i109, 0), =(matching1, 1))
f786_0_ack_InvokeMethod(EOS, i106, i109, i148, i106, i151) → f815_0_ack_Load(EOS, i106, i151, i106, i151)
f786_0_ack_InvokeMethod(EOS, i106, i109, i148, i106, i151) → f815_1_ack_Load(EOS, i106, i109, i148, i106, i151, i106, i151)
f815_0_ack_Load(EOS, i106, i151, i106, i151) → f822_0_ack_Load(EOS, i106, i151, i106, i151)
f822_0_ack_Load(EOS, i106, i151, i106, i151) → f554_0_ack_Load(EOS, i106, i151, i106, i151)
f918_0_ack_Return(EOS, i184, i109, i148, i184, matching1, i184, matching2, i180) → f932_0_ack_InvokeMethod(EOS, i184, i109, i148, i180) | &&(=(matching1, 0), =(matching2, 0))
f932_0_ack_InvokeMethod(EOS, i184, i109, i148, i180) → f1071_0_ack_InvokeMethod(EOS, i184, i109, i148, i180)
f1071_0_ack_InvokeMethod(EOS, i304, i109, i148, i299) → f1074_0_ack_Load(EOS, i148, i299, i148, i299)
f1071_0_ack_InvokeMethod(EOS, i304, i109, i148, i299) → f1074_1_ack_Load(EOS, i304, i109, i148, i299, i148, i299)
f1074_0_ack_Load(EOS, i148, i299, i148, i299) → f1135_0_ack_Load(EOS, i148, i299, i148, i299)
f1135_0_ack_Load(EOS, i148, i299, i148, i299) → f554_0_ack_Load(EOS, i148, i299, i148, i299)
f1141_0_ack_Return(EOS, i381, i109, i148, i381, matching1, i381, matching2, i376) → f918_0_ack_Return(EOS, i381, i109, i148, i381, 0, i381, 0, i376) | &&(=(matching1, 0), =(matching2, 0))
f1238_0_ack_Return(EOS, i476, i109, i148, i476, i478, i472) → f1057_0_ack_Return(EOS, i476, i109, i148, i476, i478, i472)
f1057_0_ack_Return(EOS, i304, i109, i148, i304, i306, i299) → f1071_0_ack_InvokeMethod(EOS, i304, i109, i148, i299)
f1310_0_ack_Return(EOS, i564, i109, i148, i564, i566, i560) → f1057_0_ack_Return(EOS, i564, i109, i148, i564, i566, i560)
f815_1_ack_Load(EOS, i184, i109, i148, i184, matching1, i184, matching2) → f918_0_ack_Return(EOS, i184, i109, i148, i184, 0, i184, 0, i180) | &&(=(matching1, 0), =(matching2, 0))
f815_1_ack_Load(EOS, i381, i109, i148, i381, matching1, i381, matching2) → f1141_0_ack_Return(EOS, i381, i109, i148, i381, 0, i381, 0, i376) | &&(=(matching1, 0), =(matching2, 0))
f815_1_ack_Load(EOS, i476, i109, i148, i476, i478, i476, i478) → f1238_0_ack_Return(EOS, i476, i109, i148, i476, i478, i472)
f815_1_ack_Load(EOS, i564, i109, i148, i564, i566, i564, i566) → f1310_0_ack_Return(EOS, i564, i109, i148, i564, i566, i560)

Combined rules. Obtained 7 IRules

P rules:
f1071_0_ack_InvokeMethod(EOS, i304, i109, i148, i299) → f1074_1_ack_Load(EOS, i304, i109, i148, i299, i148, i299)
f572_0_ack_GT(EOS, x0, 0, x0, 0, x0) → f761_1_ack_Load(EOS, x0, 0, x0, 0, -(x0, 1), 1, -(x0, 1), 1) | >(x0, 0)
f572_0_ack_GT(EOS, x0, 0, x0, 0, x0) → f572_0_ack_GT(EOS, -(x0, 1), 1, -(x0, 1), 1, -(x0, 1)) | >(x0, 0)
f572_0_ack_GT(EOS, x0, x1, x0, x1, x0) → f572_0_ack_GT(EOS, x0, -(x1, 1), x0, -(x1, 1), x0) | &&(>(x1, 0), >(x0, 0))
f1071_0_ack_InvokeMethod(EOS, x0, x1, x2, x3) → f572_0_ack_GT(EOS, x2, x3, x2, x3, x2)
f572_0_ack_GT(EOS, x0, 1, x0, 1, x0) → f1071_0_ack_InvokeMethod(EOS, x0, 1, -(x0, 1), x2) | >(x0, 0)
f572_0_ack_GT(EOS, x0, x1, x0, x1, x0) → f1071_0_ack_InvokeMethod(EOS, x0, x1, -(x0, 1), x2) | &&(>(x1, 0), >(x0, 0))

Filtered ground terms:

f1071_0_ack_InvokeMethod(x1, x2, x3, x4, x5) → f1071_0_ack_InvokeMethod(x2, x3, x4, x5)
f1074_1_ack_Load(x1, x2, x3, x4, x5, x6, x7) → f1074_1_ack_Load(x2, x3, x4, x5, x6, x7)
f572_0_ack_GT(x1, x2, x3, x4, x5, x6) → f572_0_ack_GT(x2, x3, x4, x5, x6)
Cond_f572_0_ack_GT(x1, x2, x3, x4, x5, x6, x7) → Cond_f572_0_ack_GT(x1, x3, x5, x7)
f761_1_ack_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9) → f761_1_ack_Load(x2, x4, x6, x8)
Cond_f572_0_ack_GT1(x1, x2, x3, x4, x5, x6, x7) → Cond_f572_0_ack_GT1(x1, x3, x5, x7)
Cond_f572_0_ack_GT2(x1, x2, x3, x4, x5, x6, x7) → Cond_f572_0_ack_GT2(x1, x3, x4, x5, x6, x7)
Cond_f572_0_ack_GT3(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f572_0_ack_GT3(x1, x3, x5, x7, x8)
Cond_f572_0_ack_GT4(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f572_0_ack_GT4(x1, x3, x4, x5, x6, x7, x8)

Filtered duplicate terms:

f1074_1_ack_Load(x1, x2, x3, x4, x5, x6) → f1074_1_ack_Load(x1, x2, x5, x6)
f572_0_ack_GT(x1, x2, x3, x4, x5) → f572_0_ack_GT(x4, x5)
Cond_f572_0_ack_GT(x1, x2, x3, x4) → Cond_f572_0_ack_GT(x1, x4)
f761_1_ack_Load(x1, x2, x3, x4) → f761_1_ack_Load(x4)
Cond_f572_0_ack_GT1(x1, x2, x3, x4) → Cond_f572_0_ack_GT1(x1, x4)
Cond_f572_0_ack_GT2(x1, x2, x3, x4, x5, x6) → Cond_f572_0_ack_GT2(x1, x5, x6)
Cond_f572_0_ack_GT3(x1, x2, x3, x4, x5) → Cond_f572_0_ack_GT3(x1, x4, x5)
Cond_f572_0_ack_GT4(x1, x2, x3, x4, x5, x6, x7) → Cond_f572_0_ack_GT4(x1, x5, x6, x7)

Filtered unneeded terms:

Cond_f572_0_ack_GT(x1, x2) → Cond_f572_0_ack_GT(x1)
f1071_0_ack_InvokeMethod(x1, x2, x3, x4) → f1071_0_ack_InvokeMethod(x3, x4)
Cond_f572_0_ack_GT4(x1, x2, x3, x4) → Cond_f572_0_ack_GT4(x1, x3, x4)

Prepared 7 rules for path length conversion:

P rules:
f1071_0_ack_InvokeMethod(i148, i299) → f1074_1_ack_Load(i304, i109, i148, i299)
f572_0_ack_GT(0, x0) → f761_1_ack_Load(-(x0, 1)) | >(x0, 0)
f572_0_ack_GT(0, x0) → f572_0_ack_GT(1, -(x0, 1)) | >(x0, 0)
f572_0_ack_GT(x1, x0) → f572_0_ack_GT(-(x1, 1), x0) | &&(>(x1, 0), >(x0, 0))
f1071_0_ack_InvokeMethod(x2, x3) → f572_0_ack_GT(x3, x2)
f572_0_ack_GT(1, x0) → f1071_0_ack_InvokeMethod(-(x0, 1), x2) | >(x0, 0)
f572_0_ack_GT(x1, x0) → f1071_0_ack_InvokeMethod(-(x0, 1), x2) | &&(>(x1, 0), >(x0, 0))

Finished conversion. Obtained 5 rules.

P rules:
f572_0_ack_GT(c0, x5) → f572_0_ack_GT(1, -(x5, 1)) | &&(>(x5, 0), =(0, c0))
f572_0_ack_GT(x6, x7) → f572_0_ack_GT(-(x6, 1), x7) | &&(>(x6, 0), >(x7, 0))
f1071_0_ack_InvokeMethod(x8, x9) → f572_0_ack_GT(x9, x8)
f572_0_ack_GT(c1, x10) → f1071_0_ack_InvokeMethod(-(x10, 1), x11) | &&(>(x10, 0), =(1, c1))
f572_0_ack_GT(x12, x13) → f1071_0_ack_InvokeMethod(-(x13, 1), x14) | &&(>(x12, 0), >(x13, 0))

(6) Obligation:

Rules:
f572_0_ack_GT(c0, x5) → f572_0_ack_GT(1, -(x5, 1)) | &&(>(x5, 0), =(0, c0))
f572_0_ack_GT(x6, x7) → f572_0_ack_GT(-(x6, 1), x7) | &&(>(x6, 0), >(x7, 0))
f1071_0_ack_InvokeMethod(x8, x9) → f572_0_ack_GT(x9, x8)
f572_0_ack_GT(c1, x10) → f1071_0_ack_InvokeMethod(-(x10, 1), x11) | &&(>(x10, 0), =(1, c1))
f572_0_ack_GT(x12, x13) → f1071_0_ack_InvokeMethod(-(x13, 1), x14) | &&(>(x12, 0), >(x13, 0))

(7) PolynomialOrderProcessor (SOUND transformation)

Found the following polynomial interpretation:

[f572_0_ack_GT(x13, x15)] = -1 + x15
[f1071_0_ack_InvokeMethod(x18, x20)] = x18

Therefore the following rule(s) have been dropped:

f572_0_ack_GT(x0, x1) → f572_0_ack_GT(1, -(x1, 1)) | &&(>(x1, 0), =(0, x0))

(8) Obligation:

Rules:
f572_0_ack_GT(x2, x3) → f572_0_ack_GT(-(x2, 1), x3) | &&(>(x2, 0), >(x3, 0))
f1071_0_ack_InvokeMethod(x4, x5) → f572_0_ack_GT(x5, x4) | TRUE
f572_0_ack_GT(x6, x7) → f1071_0_ack_InvokeMethod(-(x7, 1), x8) | &&(>(x7, 0), =(1, x6))
f572_0_ack_GT(x9, x10) → f1071_0_ack_InvokeMethod(-(x10, 1), x11) | &&(>(x9, 0), >(x10, 0))

(9) PolynomialOrderProcessor (SOUND transformation)

Found the following polynomial interpretation:

[f572_0_ack_GT(x11, x13)] = -1 + x13
[f1071_0_ack_InvokeMethod(x16, x18)] = -1 + x16

Therefore the following rule(s) have been dropped:

f572_0_ack_GT(x4, x5) → f1071_0_ack_InvokeMethod(-(x5, 1), x6) | &&(>(x5, 0), =(1, x4))
f572_0_ack_GT(x7, x8) → f1071_0_ack_InvokeMethod(-(x8, 1), x9) | &&(>(x7, 0), >(x8, 0))

(10) Obligation:

Rules:
f572_0_ack_GT(x0, x1) → f572_0_ack_GT(-(x0, 1), x1) | &&(>(x0, 0), >(x1, 0))
f1071_0_ack_InvokeMethod(x2, x3) → f572_0_ack_GT(x3, x2) | TRUE

(11) TerminationGraphProcessor (SOUND transformation)

Constructed the termination graph and obtained one non-trivial SCC.

(12) Obligation:

Rules:
f572_0_ack_GT(x0, x1) → f572_0_ack_GT(-(x0, 1), x1) | &&(>(x0, 0), >(x1, 0))

(13) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f572_0_ack_GT(x3, x5)] = x3

Therefore the following rule(s) have been dropped:

f572_0_ack_GT(x0, x1) → f572_0_ack_GT(-(x0, 1), x1) | &&(>(x0, 0), >(x1, 0))

(14) YES