Termination proof of /tmp/tmpRmxFhp/Test5.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 546 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 9 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIntTRSProof (⇒, 224 ms)

        ↳7 intTRS

        ↳8 PolynomialOrderProcessor (⇔, 0 ms)

        ↳9 YES

    ↳10 JBCTerminationSCC

        ↳11 SCCToIntTRSProof (⇒, 51 ms)

        ↳12 intTRS

        ↳13 PolynomialOrderProcessor (⇔, 0 ms)

        ↳14 YES

    ↳15 JBCTerminationSCC

        ↳16 SCCToIntTRSProof (⇒, 47 ms)

        ↳17 intTRS

        ↳18 LinearRankingProcessor (⇔, 0 ms)

        ↳19 YES

    ↳20 JBCTerminationSCC

        ↳21 SCCToIntTRSProof (⇒, 545 ms)

        ↳22 intTRS

        ↳23 PolynomialOrderProcessor (⇔, 65 ms)

        ↳24 YES

(0) Obligation:

JBC Problem based on JBC Program:

public class Test5 {
    public static void main(String[] args) {
	List l1 = List.mk(args.length);
	List l2 = List.mk(args.length + 3);
	List l3 = List.mk(args.length + 5);
	List temp;

	while (length(l1) > 0) {
	    temp = l1;
	    l1 = l2;
	    l2 = l3;
	    l3 = temp;

	    if (length(l2) % 3 == 0)
		temp = temp.getTail();

	    if (length(l3) % 5 == 0)
		l3 = l3.getTail();

	    if (length(l1) > length(l2))
		l1 = l1.getTail();
	    else if (length(l1) == length(l2))
		l2 = l2.getTail();
	    else
		l3 = l3.getTail();

	    test(l1, l2, l3);
	}
    }

    private static int length(List list) {
	int len = 0;

	while (list != null) {
	    list = list.getTail();
	    len++;
	}

	return len;
    }

    private static void test(List l1, List l2, List l3) {
	while (l1 != null) {
	    l2 = new List(l1, l2);
	    l3 = new List(l2, l3);
	    l1 = l1.getTail();
	}
    }
}

public class List {
    public Object head;
    private List tail;

    public List(Object head, List tail) {
	this.head = head;
	this.tail = tail;
    }

    public List getTail() {
	return tail;
    }

    public static List mk(int len) {
	List result = null;

	while (len-- > 0)
	    result = new List(new Object(), result);

	return result;
    }
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
Test5.main([Ljava/lang/String;)V: Graph of 291 nodes with 1 SCC.

List.mk(I)LList;: Graph of 33 nodes with 1 SCC.

Test5.length(LList;)I: Graph of 31 nodes with 1 SCC.

Test5.test(LList;LList;LList;)V: Graph of 53 nodes with 1 SCC.

(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 4 SCCss.

(4) Complex Obligation (AND)

(5) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Test5.test(LList;LList;LList;)V
SCC calls the following helper methods:
Performed SCC analyses:

Used field analysis yielded the following read fields:
- List: [tail]
Marker field analysis yielded the following relations that could be markers:

(6) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 50 IRules

P rules:
f1540_0_test_NULL(EOS, o747, java.lang.Object(o770sub), o751, o752, java.lang.Object(o770sub)) → f1541_0_test_NULL(EOS, o747, java.lang.Object(o770sub), o751, o752, java.lang.Object(o770sub))
f1541_0_test_NULL(EOS, o747, java.lang.Object(o770sub), o751, o752, java.lang.Object(o770sub)) → f1544_0_test_New(EOS, o747, java.lang.Object(o770sub), o751, o752)
f1544_0_test_New(EOS, o747, java.lang.Object(o770sub), o751, o752) → f1548_0_test_Duplicate(EOS, o747, java.lang.Object(o770sub), o751, o752, java.lang.Object(List(EOC, NULL)))
f1548_0_test_Duplicate(EOS, o747, java.lang.Object(o770sub), o751, o752, java.lang.Object(List(EOC, NULL))) → f1554_0_test_Load(EOS, o747, java.lang.Object(o770sub), o751, o752, java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)))
f1554_0_test_Load(EOS, o747, java.lang.Object(o770sub), o751, o752, java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL))) → f1559_0_test_Load(EOS, o747, java.lang.Object(o770sub), o751, o752, java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(o770sub))
f1559_0_test_Load(EOS, o747, java.lang.Object(o770sub), o751, o752, java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(o770sub)) → f1561_0_test_InvokeMethod(EOS, o747, java.lang.Object(o770sub), o752, java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(o770sub), o751)
f1561_0_test_InvokeMethod(EOS, o747, java.lang.Object(o770sub), o752, java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(o770sub), o751) → f1564_0__init__Load(EOS, o747, java.lang.Object(o770sub), o752, java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(o770sub), o751, java.lang.Object(List(EOC, NULL)), java.lang.Object(o770sub), o751)
f1564_0__init__Load(EOS, o747, java.lang.Object(o770sub), o752, java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(o770sub), o751, java.lang.Object(List(EOC, NULL)), java.lang.Object(o770sub), o751) → f1566_0__init__InvokeMethod(EOS, o747, java.lang.Object(o770sub), o752, java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(o770sub), o751, java.lang.Object(List(EOC, NULL)), java.lang.Object(o770sub), o751, java.lang.Object(List(EOC, NULL)))
f1566_0__init__InvokeMethod(EOS, o747, java.lang.Object(o770sub), o752, java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(o770sub), o751, java.lang.Object(List(EOC, NULL)), java.lang.Object(o770sub), o751, java.lang.Object(List(EOC, NULL))) → f1569_0__init__Load(EOS, o747, java.lang.Object(o770sub), o752, java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(o770sub), o751, java.lang.Object(List(EOC, NULL)), java.lang.Object(o770sub), o751)
f1569_0__init__Load(EOS, o747, java.lang.Object(o770sub), o752, java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(o770sub), o751, java.lang.Object(List(EOC, NULL)), java.lang.Object(o770sub), o751) → f1570_0__init__Load(EOS, o747, java.lang.Object(o770sub), o752, java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(o770sub), o751, java.lang.Object(List(EOC, NULL)), java.lang.Object(o770sub), o751, java.lang.Object(List(EOC, NULL)))
f1570_0__init__Load(EOS, o747, java.lang.Object(o770sub), o752, java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(o770sub), o751, java.lang.Object(List(EOC, NULL)), java.lang.Object(o770sub), o751, java.lang.Object(List(EOC, NULL))) → f1574_0__init__FieldAccess(EOS, o747, java.lang.Object(o770sub), o752, java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(o770sub), o751, java.lang.Object(List(EOC, NULL)), o751, java.lang.Object(List(EOC, NULL)), java.lang.Object(o770sub))
f1574_0__init__FieldAccess(EOS, o747, java.lang.Object(o770sub), o752, java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(o770sub), o751, java.lang.Object(List(EOC, NULL)), o751, java.lang.Object(List(EOC, NULL)), java.lang.Object(o770sub)) → f1578_0__init__Load(EOS, o747, java.lang.Object(o770sub), o752, java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(o770sub), o751, java.lang.Object(List(EOC, NULL)), o751)
f1578_0__init__Load(EOS, o747, java.lang.Object(o770sub), o752, java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(o770sub), o751, java.lang.Object(List(EOC, NULL)), o751) → f1582_0__init__Load(EOS, o747, java.lang.Object(o770sub), o752, java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(o770sub), o751, o751, java.lang.Object(List(EOC, NULL)))
f1582_0__init__Load(EOS, o747, java.lang.Object(o770sub), o752, java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(o770sub), o751, o751, java.lang.Object(List(EOC, NULL))) → f1585_0__init__FieldAccess(EOS, o747, java.lang.Object(o770sub), o752, java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(o770sub), o751, java.lang.Object(List(EOC, NULL)), o751)
f1585_0__init__FieldAccess(EOS, o747, java.lang.Object(o770sub), o752, java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(o770sub), o751, java.lang.Object(List(EOC, NULL)), o751) → f1588_0__init__Return(EOS, o747, java.lang.Object(o770sub), o752, java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, o751)), java.lang.Object(o770sub), o751)
f1588_0__init__Return(EOS, o747, java.lang.Object(o770sub), o752, java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, o751)), java.lang.Object(o770sub), o751) → f1593_0_test_Store(EOS, o747, java.lang.Object(o770sub), o752, java.lang.Object(List(EOC, o751)))
f1593_0_test_Store(EOS, o747, java.lang.Object(o770sub), o752, java.lang.Object(List(EOC, o751))) → f1596_0_test_New(EOS, o747, java.lang.Object(o770sub), java.lang.Object(List(EOC, o751)), o752)
f1596_0_test_New(EOS, o747, java.lang.Object(o770sub), java.lang.Object(List(EOC, o751)), o752) → f1603_0_test_Duplicate(EOS, o747, java.lang.Object(o770sub), java.lang.Object(List(EOC, o751)), o752, java.lang.Object(List(EOC, NULL)))
f1603_0_test_Duplicate(EOS, o747, java.lang.Object(o770sub), java.lang.Object(List(EOC, o751)), o752, java.lang.Object(List(EOC, NULL))) → f1609_0_test_Load(EOS, o747, java.lang.Object(o770sub), java.lang.Object(List(EOC, o751)), o752, java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)))
f1609_0_test_Load(EOS, o747, java.lang.Object(o770sub), java.lang.Object(List(EOC, o751)), o752, java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL))) → f1614_0_test_Load(EOS, o747, java.lang.Object(o770sub), java.lang.Object(List(EOC, o751)), o752, java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, o751)))
f1614_0_test_Load(EOS, o747, java.lang.Object(o770sub), java.lang.Object(List(EOC, o751)), o752, java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, o751))) → f1617_0_test_InvokeMethod(EOS, o747, java.lang.Object(o770sub), java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, o751)), o752)
f1617_0_test_InvokeMethod(EOS, o747, java.lang.Object(o770sub), java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, o751)), o752) → f1623_0__init__Load(EOS, o747, java.lang.Object(o770sub), java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, o751)), o752, java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, o751)), o752)
f1623_0__init__Load(EOS, o747, java.lang.Object(o770sub), java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, o751)), o752, java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, o751)), o752) → f1633_0__init__InvokeMethod(EOS, o747, java.lang.Object(o770sub), java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, o751)), o752, java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, o751)), o752, java.lang.Object(List(EOC, NULL)))
f1633_0__init__InvokeMethod(EOS, o747, java.lang.Object(o770sub), java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, o751)), o752, java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, o751)), o752, java.lang.Object(List(EOC, NULL))) → f1642_0__init__Load(EOS, o747, java.lang.Object(o770sub), java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, o751)), o752, java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, o751)), o752)
f1642_0__init__Load(EOS, o747, java.lang.Object(o770sub), java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, o751)), o752, java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, o751)), o752) → f1649_0__init__Load(EOS, o747, java.lang.Object(o770sub), java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, o751)), o752, java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, o751)), o752, java.lang.Object(List(EOC, NULL)))
f1649_0__init__Load(EOS, o747, java.lang.Object(o770sub), java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, o751)), o752, java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, o751)), o752, java.lang.Object(List(EOC, NULL))) → f1655_0__init__FieldAccess(EOS, o747, java.lang.Object(o770sub), java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, o751)), o752, java.lang.Object(List(EOC, NULL)), o752, java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, o751)))
f1655_0__init__FieldAccess(EOS, o747, java.lang.Object(o770sub), java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, o751)), o752, java.lang.Object(List(EOC, NULL)), o752, java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, o751))) → f1666_0__init__Load(EOS, o747, java.lang.Object(o770sub), java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, o751)), o752, java.lang.Object(List(EOC, NULL)), o752)
f1666_0__init__Load(EOS, o747, java.lang.Object(o770sub), java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, o751)), o752, java.lang.Object(List(EOC, NULL)), o752) → f1672_0__init__Load(EOS, o747, java.lang.Object(o770sub), java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, o751)), o752, o752, java.lang.Object(List(EOC, NULL)))
f1672_0__init__Load(EOS, o747, java.lang.Object(o770sub), java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, o751)), o752, o752, java.lang.Object(List(EOC, NULL))) → f1679_0__init__FieldAccess(EOS, o747, java.lang.Object(o770sub), java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, o751)), o752, java.lang.Object(List(EOC, NULL)), o752)
f1679_0__init__FieldAccess(EOS, o747, java.lang.Object(o770sub), java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, o751)), o752, java.lang.Object(List(EOC, NULL)), o752) → f1688_0__init__Return(EOS, o747, java.lang.Object(o770sub), java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, o752)), java.lang.Object(List(EOC, o752)), java.lang.Object(List(EOC, o751)), o752)
f1688_0__init__Return(EOS, o747, java.lang.Object(o770sub), java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, o752)), java.lang.Object(List(EOC, o752)), java.lang.Object(List(EOC, o751)), o752) → f1694_0_test_Store(EOS, o747, java.lang.Object(o770sub), java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, o752)))
f1694_0_test_Store(EOS, o747, java.lang.Object(o770sub), java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, o752))) → f1698_0_test_Load(EOS, o747, java.lang.Object(o770sub), java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, o752)))
f1698_0_test_Load(EOS, o747, java.lang.Object(o770sub), java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, o752))) → f1705_0_test_InvokeMethod(EOS, o747, java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, o752)), java.lang.Object(o770sub))
f1705_0_test_InvokeMethod(EOS, o747, java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, o752)), java.lang.Object(o770sub)) → f1710_0_getTail_Load(EOS, o747, java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, o752)), java.lang.Object(o770sub), java.lang.Object(o770sub))
f1710_0_getTail_Load(EOS, o747, java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, o752)), java.lang.Object(o770sub), java.lang.Object(o770sub)) → f1719_0_getTail_FieldAccess(EOS, o747, java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, o752)), java.lang.Object(o770sub), java.lang.Object(o770sub))
f1719_0_getTail_FieldAccess(EOS, o747, java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, o752)), java.lang.Object(o770sub), java.lang.Object(o770sub)) → f1731_0_getTail_FieldAccess(EOS, o747, java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, o752)), java.lang.Object(o770sub), java.lang.Object(o770sub))
f1719_0_getTail_FieldAccess(EOS, java.lang.Object(o980sub), java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, o752)), java.lang.Object(o980sub), java.lang.Object(o980sub)) → f1732_0_getTail_FieldAccess(EOS, java.lang.Object(o980sub), java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, o752)), java.lang.Object(o980sub), java.lang.Object(o980sub))
f1731_0_getTail_FieldAccess(EOS, o747, java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, o752)), java.lang.Object(List(EOC, o984)), java.lang.Object(List(EOC, o984))) → f1736_0_getTail_FieldAccess(EOS, o747, java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, o752)), java.lang.Object(List(EOC, o984)), java.lang.Object(List(EOC, o984)))
f1736_0_getTail_FieldAccess(EOS, o747, java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, o752)), java.lang.Object(List(EOC, o984)), java.lang.Object(List(EOC, o984))) → f1742_0_getTail_Return(EOS, o747, java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, o752)), java.lang.Object(List(EOC, o984)), o984)
f1742_0_getTail_Return(EOS, o747, java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, o752)), java.lang.Object(List(EOC, o984)), o984) → f1748_0_test_Store(EOS, o747, java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, o752)), o984)
f1748_0_test_Store(EOS, o747, java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, o752)), o984) → f1754_0_test_JMP(EOS, o747, o984, java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, o752)))
f1754_0_test_JMP(EOS, o747, o984, java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, o752))) → f1763_0_test_Load(EOS, o747, o984, java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, o752)))
f1763_0_test_Load(EOS, o747, o984, java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, o752))) → f1537_0_test_Load(EOS, o747, o984, java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, o752)))
f1537_0_test_Load(EOS, o747, o750, o751, o752) → f1540_0_test_NULL(EOS, o747, o750, o751, o752, o750)
f1732_0_getTail_FieldAccess(EOS, java.lang.Object(List(EOC, o987)), java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, o752)), java.lang.Object(List(EOC, o987)), java.lang.Object(List(EOC, o987))) → f1739_0_getTail_FieldAccess(EOS, java.lang.Object(List(EOC, o987)), java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, o752)), java.lang.Object(List(EOC, o987)), java.lang.Object(List(EOC, o987)))
f1739_0_getTail_FieldAccess(EOS, java.lang.Object(List(EOC, o987)), java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, o752)), java.lang.Object(List(EOC, o987)), java.lang.Object(List(EOC, o987))) → f1745_0_getTail_Return(EOS, java.lang.Object(List(EOC, o987)), java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, o752)), java.lang.Object(List(EOC, o987)), o987)
f1745_0_getTail_Return(EOS, java.lang.Object(List(EOC, o987)), java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, o752)), java.lang.Object(List(EOC, o987)), o987) → f1751_0_test_Store(EOS, java.lang.Object(List(EOC, o987)), java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, o752)), o987)
f1751_0_test_Store(EOS, java.lang.Object(List(EOC, o987)), java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, o752)), o987) → f1757_0_test_JMP(EOS, java.lang.Object(List(EOC, o987)), o987, java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, o752)))
f1757_0_test_JMP(EOS, java.lang.Object(List(EOC, o987)), o987, java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, o752))) → f1767_0_test_Load(EOS, java.lang.Object(List(EOC, o987)), o987, java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, o752)))
f1767_0_test_Load(EOS, java.lang.Object(List(EOC, o987)), o987, java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, o752))) → f1537_0_test_Load(EOS, java.lang.Object(List(EOC, o987)), o987, java.lang.Object(List(EOC, o751)), java.lang.Object(List(EOC, o752)))

Combined rules. Obtained 2 IRules

P rules:
f1540_0_test_NULL(EOS, x0, java.lang.Object(List(EOC, x1)), x2, x3, java.lang.Object(List(EOC, x1))) → f1540_0_test_NULL(EOS, x0, x1, java.lang.Object(List(EOC, x2)), java.lang.Object(List(EOC, x3)), x1)
f1540_0_test_NULL(EOS, java.lang.Object(List(EOC, x0)), java.lang.Object(List(EOC, x0)), x1, x2, java.lang.Object(List(EOC, x0))) → f1540_0_test_NULL(EOS, java.lang.Object(List(EOC, x0)), x0, java.lang.Object(List(EOC, x1)), java.lang.Object(List(EOC, x2)), x0)

Filtered ground terms:

f1540_0_test_NULL(x1, x2, x3, x4, x5, x6) → f1540_0_test_NULL(x2, x3, x4, x5, x6)
List(x1, x2) → List(x2)

Filtered duplicate terms:

f1540_0_test_NULL(x1, x2, x3, x4, x5) → f1540_0_test_NULL(x1, x3, x4, x5)

Filtered unneeded terms:

f1540_0_test_NULL(x1, x2, x3, x4) → f1540_0_test_NULL(x1, x4)

Prepared 2 rules for path length conversion:

P rules:
f1540_0_test_NULL(x0, java.lang.Object(List(x1))) → f1540_0_test_NULL(x0, x1)
f1540_0_test_NULL(java.lang.Object(List(x0)), java.lang.Object(List(x0))) → f1540_0_test_NULL(java.lang.Object(List(x0)), x0)

Finished conversion. Obtained 2 rules.

P rules:
f1540_0_test_NULL(v5, v6) → f1540_0_test_NULL(v7, v8) | &&(&&(&&(&&(&&(>(+(v8, 1), 0), <=(+(v8, 1), v6)), >(+(v7, 1), 0)), <=(v7, v5)), >(+(v6, 1), 1)), >(+(v5, 1), 0))
f1540_0_test_NULL(v9, v10) → f1540_0_test_NULL(v11, v12) | &&(&&(&&(&&(&&(&&(&&(>=(v9, +(v12, 1)), >=(v9, v11)), >(+(v9, 1), 1)), >(+(v12, 1), 0)), <=(+(v12, 1), v10)), >(+(v11, 1), 1)), <=(v11, v10)), >(+(v10, 1), 1))

(7) Obligation:

Rules:
f1540_0_test_NULL(v5, v6) → f1540_0_test_NULL(v7, v8) | &&(&&(&&(&&(&&(>(+(v8, 1), 0), <=(+(v8, 1), v6)), >(+(v7, 1), 0)), <=(v7, v5)), >(+(v6, 1), 1)), >(+(v5, 1), 0))
f1540_0_test_NULL(v9, v10) → f1540_0_test_NULL(v11, v12) | &&(&&(&&(&&(&&(&&(&&(>=(v9, +(v12, 1)), >=(v9, v11)), >(+(v9, 1), 1)), >(+(v12, 1), 0)), <=(+(v12, 1), v10)), >(+(v11, 1), 1)), <=(v11, v10)), >(+(v10, 1), 1))

(8) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f1540_0_test_NULL(x9, x11)] = x11

Therefore the following rule(s) have been dropped:

f1540_0_test_NULL(x0, x1) → f1540_0_test_NULL(x2, x3) | &&(&&(&&(&&(&&(>(+(x3, 1), 0), <=(+(x3, 1), x1)), >(+(x2, 1), 0)), <=(x2, x0)), >(+(x1, 1), 1)), >(+(x0, 1), 0))
f1540_0_test_NULL(x4, x5) → f1540_0_test_NULL(x6, x7) | &&(&&(&&(&&(&&(&&(&&(>=(x4, +(x7, 1)), >=(x4, x6)), >(+(x4, 1), 1)), >(+(x7, 1), 0)), <=(+(x7, 1), x5)), >(+(x6, 1), 1)), <=(x6, x5)), >(+(x5, 1), 1))

(9) YES

(10) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Test5.length(LList;)I
SCC calls the following helper methods:
Performed SCC analyses:

Used field analysis yielded the following read fields:
- List: [tail]
Marker field analysis yielded the following relations that could be markers:

(11) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 22 IRules

P rules:
f993_0_length_NULL(EOS, o327, java.lang.Object(o336sub), java.lang.Object(o336sub)) → f996_0_length_NULL(EOS, o327, java.lang.Object(o336sub), java.lang.Object(o336sub))
f996_0_length_NULL(EOS, o327, java.lang.Object(o336sub), java.lang.Object(o336sub)) → f1000_0_length_Load(EOS, o327, java.lang.Object(o336sub))
f1000_0_length_Load(EOS, o327, java.lang.Object(o336sub)) → f1004_0_length_InvokeMethod(EOS, o327, java.lang.Object(o336sub))
f1004_0_length_InvokeMethod(EOS, o327, java.lang.Object(o336sub)) → f1008_0_getTail_Load(EOS, o327, java.lang.Object(o336sub), java.lang.Object(o336sub))
f1008_0_getTail_Load(EOS, o327, java.lang.Object(o336sub), java.lang.Object(o336sub)) → f1024_0_getTail_FieldAccess(EOS, o327, java.lang.Object(o336sub), java.lang.Object(o336sub))
f1024_0_getTail_FieldAccess(EOS, o327, java.lang.Object(o336sub), java.lang.Object(o336sub)) → f1027_0_getTail_FieldAccess(EOS, o327, java.lang.Object(o336sub), java.lang.Object(o336sub))
f1024_0_getTail_FieldAccess(EOS, java.lang.Object(o358sub), java.lang.Object(o358sub), java.lang.Object(o358sub)) → f1028_0_getTail_FieldAccess(EOS, java.lang.Object(o358sub), java.lang.Object(o358sub), java.lang.Object(o358sub))
f1027_0_getTail_FieldAccess(EOS, o327, java.lang.Object(List(EOC, o361)), java.lang.Object(List(EOC, o361))) → f1032_0_getTail_FieldAccess(EOS, o327, java.lang.Object(List(EOC, o361)), java.lang.Object(List(EOC, o361)))
f1032_0_getTail_FieldAccess(EOS, o327, java.lang.Object(List(EOC, o361)), java.lang.Object(List(EOC, o361))) → f1039_0_getTail_Return(EOS, o327, java.lang.Object(List(EOC, o361)), o361)
f1039_0_getTail_Return(EOS, o327, java.lang.Object(List(EOC, o361)), o361) → f1046_0_length_Store(EOS, o327, o361)
f1046_0_length_Store(EOS, o327, o361) → f1053_0_length_Inc(EOS, o327, o361)
f1053_0_length_Inc(EOS, o327, o361) → f1058_0_length_JMP(EOS, o327, o361)
f1058_0_length_JMP(EOS, o327, o361) → f1067_0_length_Load(EOS, o327, o361)
f1067_0_length_Load(EOS, o327, o361) → f987_0_length_Load(EOS, o327, o361)
f987_0_length_Load(EOS, o327, o328) → f993_0_length_NULL(EOS, o327, o328, o328)
f1028_0_getTail_FieldAccess(EOS, java.lang.Object(List(EOC, o364)), java.lang.Object(List(EOC, o364)), java.lang.Object(List(EOC, o364))) → f1035_0_getTail_FieldAccess(EOS, java.lang.Object(List(EOC, o364)), java.lang.Object(List(EOC, o364)), java.lang.Object(List(EOC, o364)))
f1035_0_getTail_FieldAccess(EOS, java.lang.Object(List(EOC, o364)), java.lang.Object(List(EOC, o364)), java.lang.Object(List(EOC, o364))) → f1043_0_getTail_Return(EOS, java.lang.Object(List(EOC, o364)), java.lang.Object(List(EOC, o364)), o364)
f1043_0_getTail_Return(EOS, java.lang.Object(List(EOC, o364)), java.lang.Object(List(EOC, o364)), o364) → f1050_0_length_Store(EOS, java.lang.Object(List(EOC, o364)), o364)
f1050_0_length_Store(EOS, java.lang.Object(List(EOC, o364)), o364) → f1055_0_length_Inc(EOS, java.lang.Object(List(EOC, o364)), o364)
f1055_0_length_Inc(EOS, java.lang.Object(List(EOC, o364)), o364) → f1062_0_length_JMP(EOS, java.lang.Object(List(EOC, o364)), o364)
f1062_0_length_JMP(EOS, java.lang.Object(List(EOC, o364)), o364) → f1072_0_length_Load(EOS, java.lang.Object(List(EOC, o364)), o364)
f1072_0_length_Load(EOS, java.lang.Object(List(EOC, o364)), o364) → f987_0_length_Load(EOS, java.lang.Object(List(EOC, o364)), o364)

Combined rules. Obtained 2 IRules

P rules:
f993_0_length_NULL(EOS, x0, java.lang.Object(List(EOC, x1)), java.lang.Object(List(EOC, x1))) → f993_0_length_NULL(EOS, x0, x1, x1)
f993_0_length_NULL(EOS, java.lang.Object(List(EOC, x0)), java.lang.Object(List(EOC, x0)), java.lang.Object(List(EOC, x0))) → f993_0_length_NULL(EOS, java.lang.Object(List(EOC, x0)), x0, x0)

Filtered ground terms:

f993_0_length_NULL(x1, x2, x3, x4) → f993_0_length_NULL(x2, x3, x4)
List(x1, x2) → List(x2)

Filtered duplicate terms:

f993_0_length_NULL(x1, x2, x3) → f993_0_length_NULL(x1, x3)

Prepared 2 rules for path length conversion:

P rules:
f993_0_length_NULL(x0, java.lang.Object(List(x1))) → f993_0_length_NULL(x0, x1)
f993_0_length_NULL(java.lang.Object(List(x0)), java.lang.Object(List(x0))) → f993_0_length_NULL(java.lang.Object(List(x0)), x0)

Finished conversion. Obtained 2 rules.

P rules:
f993_0_length_NULL(v5, v6) → f993_0_length_NULL(v7, v8) | &&(&&(&&(&&(&&(>(+(v8, 1), 0), <=(+(v8, 1), v6)), >(+(v7, 1), 0)), <=(v7, v5)), >(+(v6, 1), 1)), >(+(v5, 1), 0))
f993_0_length_NULL(v9, v10) → f993_0_length_NULL(v11, v12) | &&(&&(&&(&&(&&(&&(&&(>=(v9, +(v12, 1)), >=(v9, v11)), >(+(v9, 1), 1)), >(+(v12, 1), 0)), <=(+(v12, 1), v10)), >(+(v11, 1), 1)), <=(v11, v10)), >(+(v10, 1), 1))

(12) Obligation:

Rules:
f993_0_length_NULL(v5, v6) → f993_0_length_NULL(v7, v8) | &&(&&(&&(&&(&&(>(+(v8, 1), 0), <=(+(v8, 1), v6)), >(+(v7, 1), 0)), <=(v7, v5)), >(+(v6, 1), 1)), >(+(v5, 1), 0))
f993_0_length_NULL(v9, v10) → f993_0_length_NULL(v11, v12) | &&(&&(&&(&&(&&(&&(&&(>=(v9, +(v12, 1)), >=(v9, v11)), >(+(v9, 1), 1)), >(+(v12, 1), 0)), <=(+(v12, 1), v10)), >(+(v11, 1), 1)), <=(v11, v10)), >(+(v10, 1), 1))

(13) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f993_0_length_NULL(x9, x11)] = x11

Therefore the following rule(s) have been dropped:

f993_0_length_NULL(x0, x1) → f993_0_length_NULL(x2, x3) | &&(&&(&&(&&(&&(>(+(x3, 1), 0), <=(+(x3, 1), x1)), >(+(x2, 1), 0)), <=(x2, x0)), >(+(x1, 1), 1)), >(+(x0, 1), 0))
f993_0_length_NULL(x4, x5) → f993_0_length_NULL(x6, x7) | &&(&&(&&(&&(&&(&&(&&(>=(x4, +(x7, 1)), >=(x4, x6)), >(+(x4, 1), 1)), >(+(x7, 1), 0)), <=(+(x7, 1), x5)), >(+(x6, 1), 1)), <=(x6, x5)), >(+(x5, 1), 1))

(14) YES

(15) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: List.mk(I)LList;
SCC calls the following helper methods:
Performed SCC analyses:

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

(16) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 23 IRules

P rules:
f688_0_mk_Inc(EOS, i97, i97) → f694_0_mk_LE(EOS, +(i97, -1), i97)
f694_0_mk_LE(EOS, i99, i104) → f701_0_mk_LE(EOS, i99, i104)
f701_0_mk_LE(EOS, i99, i104) → f723_0_mk_New(EOS, i99) | >(i104, 0)
f723_0_mk_New(EOS, i99) → f732_0_mk_Duplicate(EOS, i99)
f732_0_mk_Duplicate(EOS, i99) → f743_0_mk_New(EOS, i99)
f743_0_mk_New(EOS, i99) → f778_0_mk_Duplicate(EOS, i99)
f778_0_mk_Duplicate(EOS, i99) → f784_0_mk_InvokeMethod(EOS, i99)
f784_0_mk_InvokeMethod(EOS, i99) → f786_0_mk_Load(EOS, i99)
f786_0_mk_Load(EOS, i99) → f793_0_mk_InvokeMethod(EOS, i99)
f793_0_mk_InvokeMethod(EOS, i99) → f816_0__init__Load(EOS, i99)
f816_0__init__Load(EOS, i99) → f830_0__init__InvokeMethod(EOS, i99)
f830_0__init__InvokeMethod(EOS, i99) → f838_0__init__Load(EOS, i99)
f838_0__init__Load(EOS, i99) → f843_0__init__Load(EOS, i99)
f843_0__init__Load(EOS, i99) → f849_0__init__FieldAccess(EOS, i99)
f849_0__init__FieldAccess(EOS, i99) → f856_0__init__Load(EOS, i99)
f856_0__init__Load(EOS, i99) → f861_0__init__Load(EOS, i99)
f861_0__init__Load(EOS, i99) → f867_0__init__FieldAccess(EOS, i99)
f867_0__init__FieldAccess(EOS, i99) → f874_0__init__Return(EOS, i99)
f874_0__init__Return(EOS, i99) → f878_0_mk_Store(EOS, i99)
f878_0_mk_Store(EOS, i99) → f882_0_mk_JMP(EOS, i99)
f882_0_mk_JMP(EOS, i99) → f887_0_mk_Load(EOS, i99)
f887_0_mk_Load(EOS, i99) → f681_0_mk_Load(EOS, i99)
f681_0_mk_Load(EOS, i97) → f688_0_mk_Inc(EOS, i97, i97)

Combined rules. Obtained 1 IRules

P rules:
f688_0_mk_Inc(EOS, x0, x0) → f688_0_mk_Inc(EOS, -(x0, 1), -(x0, 1)) | >(x0, 0)

Filtered ground terms:

f688_0_mk_Inc(x1, x2, x3) → f688_0_mk_Inc(x2, x3)
Cond_f688_0_mk_Inc(x1, x2, x3, x4) → Cond_f688_0_mk_Inc(x1, x3, x4)

Filtered duplicate terms:

f688_0_mk_Inc(x1, x2) → f688_0_mk_Inc(x2)
Cond_f688_0_mk_Inc(x1, x2, x3) → Cond_f688_0_mk_Inc(x1, x3)

Prepared 1 rules for path length conversion:

P rules:
f688_0_mk_Inc(x0) → f688_0_mk_Inc(-(x0, 1)) | >(x0, 0)

Finished conversion. Obtained 1 rules.

P rules:
f688_0_mk_Inc(x0) → f688_0_mk_Inc(-(x0, 1)) | >(x0, 0)

(17) Obligation:

Rules:
f688_0_mk_Inc(x0) → f688_0_mk_Inc(-(x0, 1)) | >(x0, 0)

(18) LinearRankingProcessor (EQUIVALENT transformation)

Linear ranking:

[f688_0_mk_Inc(x)] = 1·x₁

where x = (x₁, ... ,x_n).

Therefore the following rule(s) have been dropped:

f688_0_mk_Inc(x0) → f688_0_mk_Inc(-(x0, 1)) | >(x0, 0)

(19) YES

(20) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Test5.main([Ljava/lang/String;)V
SCC calls the following helper methods: Test5.length(LList;)I, Test5.test(LList;LList;LList;)V
Performed SCC analyses:

Used field analysis yielded the following read fields:
- List: [tail]
Marker field analysis yielded the following relations that could be markers:

(21) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 137 IRules

P rules:
f417_0_main_InvokeMethod(EOS, o39, o49, o73, o39) → f421_0_length_ConstantStackPush(EOS, o39, o39)
f417_0_main_InvokeMethod(EOS, o39, o49, o73, o39) → f421_1_length_ConstantStackPush(EOS, o39, o49, o73, o39, o39)
f421_0_length_ConstantStackPush(EOS, o39, o39) → f424_0_length_ConstantStackPush(EOS, o39, o39)
f1023_0_length_Return(EOS, o342, o49, o73, o342, i155) → f935_0_length_Return(EOS, o342, o49, o73, o342, i155)
f935_0_length_Return(EOS, o299, o300, o301, o299, i143) → f945_0_main_LE(EOS, o299, o300, o301, i143)
f945_0_main_LE(EOS, o299, o300, o301, i147) → f950_0_main_LE(EOS, o299, o300, o301, i147)
f950_0_main_LE(EOS, o299, o300, o301, i147) → f957_0_main_Load(EOS, o299, o300, o301) | >(i147, 0)
f957_0_main_Load(EOS, o299, o300, o301) → f964_0_main_Store(EOS, o300, o301, o299)
f964_0_main_Store(EOS, o300, o301, o299) → f967_0_main_Load(EOS, o300, o301, o299)
f967_0_main_Load(EOS, o300, o301, o299) → f970_0_main_Store(EOS, o301, o299, o300)
f970_0_main_Store(EOS, o301, o299, o300) → f974_0_main_Load(EOS, o300, o301, o299)
f974_0_main_Load(EOS, o300, o301, o299) → f977_0_main_Store(EOS, o300, o299, o301)
f977_0_main_Store(EOS, o300, o299, o301) → f980_0_main_Load(EOS, o300, o301, o299)
f980_0_main_Load(EOS, o300, o301, o299) → f989_0_main_Store(EOS, o300, o301, o299, o299)
f989_0_main_Store(EOS, o300, o301, o299, o299) → f991_0_main_Load(EOS, o300, o301, o299, o299)
f991_0_main_Load(EOS, o300, o301, o299, o299) → f994_0_main_InvokeMethod(EOS, o300, o301, o299, o299, o301)
f994_0_main_InvokeMethod(EOS, o300, o301, o299, o299, o301) → f999_0_length_ConstantStackPush(EOS, o301, o301)
f994_0_main_InvokeMethod(EOS, o300, o301, o299, o299, o301) → f999_1_length_ConstantStackPush(EOS, o300, o301, o299, o299, o301, o301)
f999_0_length_ConstantStackPush(EOS, o301, o301) → f1002_0_length_ConstantStackPush(EOS, o301, o301)
f1025_0_length_Return(EOS, o300, o350, o299, o299, o350, i156) → f1030_0_main_ConstantStackPush(EOS, o300, o350, o299, o299, i156)
f1030_0_main_ConstantStackPush(EOS, o300, o350, o299, o299, i156) → f1033_0_main_IntArithmetic(EOS, o300, o350, o299, o299, i156, 3)
f1033_0_main_IntArithmetic(EOS, o300, o350, o299, o299, i156, matching1) → f1037_0_main_NE(EOS, o300, o350, o299, o299, %(i156, 3)) | =(matching1, 3)
f1037_0_main_NE(EOS, o300, o350, o299, o299, i161) → f1040_0_main_NE(EOS, o300, o350, o299, o299, i161)
f1037_0_main_NE(EOS, o300, o350, o299, o299, matching1) → f1041_0_main_NE(EOS, o300, o350, o299, o299, 0) | =(matching1, 0)
f1040_0_main_NE(EOS, o300, o350, o299, o299, i161) → f1045_0_main_Load(EOS, o300, o350, o299) | >(i161, 0)
f1045_0_main_Load(EOS, o300, o350, o299) → f1051_0_main_InvokeMethod(EOS, o300, o350, o299, o299)
f1051_0_main_InvokeMethod(EOS, o300, o350, o299, o299) → f1056_0_length_ConstantStackPush(EOS, o299, o299)
f1051_0_main_InvokeMethod(EOS, o300, o350, o299, o299) → f1056_1_length_ConstantStackPush(EOS, o300, o350, o299, o299, o299)
f1056_0_length_ConstantStackPush(EOS, o299, o299) → f1064_0_length_ConstantStackPush(EOS, o299, o299)
f1084_0_length_Return(EOS, o300, o350, o391, o391, i166) → f1088_0_main_ConstantStackPush(EOS, o300, o350, o391, i166)
f1088_0_main_ConstantStackPush(EOS, o300, o350, o391, i166) → f1091_0_main_IntArithmetic(EOS, o300, o350, o391, i166, 5)
f1091_0_main_IntArithmetic(EOS, o300, o350, o391, i166, matching1) → f1094_0_main_NE(EOS, o300, o350, o391, %(i166, 5)) | =(matching1, 5)
f1094_0_main_NE(EOS, o300, o350, o391, i169) → f1099_0_main_NE(EOS, o300, o350, o391, i169)
f1094_0_main_NE(EOS, o300, o350, o391, matching1) → f1100_0_main_NE(EOS, o300, o350, o391, 0) | =(matching1, 0)
f1099_0_main_NE(EOS, o300, o350, o391, i169) → f1104_0_main_Load(EOS, o300, o350, o391) | >(i169, 0)
f1104_0_main_Load(EOS, o300, o350, o391) → f1178_0_main_Load(EOS, o300, o350, o391)
f1178_0_main_Load(EOS, o300, o350, o442) → f1184_0_main_InvokeMethod(EOS, o300, o350, o442, o300)
f1184_0_main_InvokeMethod(EOS, o300, o350, o442, o300) → f1189_0_length_ConstantStackPush(EOS, o300, o300)
f1184_0_main_InvokeMethod(EOS, o300, o350, o442, o300) → f1189_1_length_ConstantStackPush(EOS, o300, o350, o442, o300, o300)
f1189_0_length_ConstantStackPush(EOS, o300, o300) → f1193_0_length_ConstantStackPush(EOS, o300, o300)
f1210_0_length_Return(EOS, o468, o350, o442, o468, i182) → f1215_0_main_Load(EOS, o468, o350, o442, i182)
f1215_0_main_Load(EOS, o468, o350, o442, i182) → f1221_0_main_InvokeMethod(EOS, o468, o350, o442, i182, o350)
f1221_0_main_InvokeMethod(EOS, o468, o350, o442, i182, o350) → f1225_0_length_ConstantStackPush(EOS, o350, o350)
f1221_0_main_InvokeMethod(EOS, o468, o350, o442, i182, o350) → f1225_1_length_ConstantStackPush(EOS, o468, o350, o442, i182, o350, o350)
f1225_0_length_ConstantStackPush(EOS, o350, o350) → f1229_0_length_ConstantStackPush(EOS, o350, o350)
f1244_0_length_Return(EOS, o468, o491, o442, i182, o491, i185) → f1250_0_main_LE(EOS, o468, o491, o442, i182, i185)
f1250_0_main_LE(EOS, o468, o491, o442, i182, i185) → f1254_0_main_LE(EOS, o468, o491, o442, i182, i185)
f1250_0_main_LE(EOS, o468, o491, o442, i182, i185) → f1255_0_main_LE(EOS, o468, o491, o442, i182, i185)
f1254_0_main_LE(EOS, o468, o491, o442, i182, i185) → f1259_0_main_Load(EOS, o468, o491, o442) | <=(i182, i185)
f1259_0_main_Load(EOS, o468, o491, o442) → f1262_0_main_InvokeMethod(EOS, o468, o491, o442, o468)
f1262_0_main_InvokeMethod(EOS, o468, o491, o442, o468) → f1267_0_length_ConstantStackPush(EOS, o468, o468)
f1262_0_main_InvokeMethod(EOS, o468, o491, o442, o468) → f1267_1_length_ConstantStackPush(EOS, o468, o491, o442, o468, o468)
f1267_0_length_ConstantStackPush(EOS, o468, o468) → f1273_0_length_ConstantStackPush(EOS, o468, o468)
f1287_0_length_Return(EOS, o516, o491, o442, o516, i187) → f1294_0_main_Load(EOS, o516, o491, o442, i187)
f1294_0_main_Load(EOS, o516, o491, o442, i187) → f1299_0_main_InvokeMethod(EOS, o516, o491, o442, i187, o491)
f1299_0_main_InvokeMethod(EOS, o516, o491, o442, i187, o491) → f1302_0_length_ConstantStackPush(EOS, o491, o491)
f1299_0_main_InvokeMethod(EOS, o516, o491, o442, i187, o491) → f1302_1_length_ConstantStackPush(EOS, o516, o491, o442, i187, o491, o491)
f1302_0_length_ConstantStackPush(EOS, o491, o491) → f1308_0_length_ConstantStackPush(EOS, o491, o491)
f1323_0_length_Return(EOS, o516, o552, o442, i187, o552, i188) → f1327_0_main_NE(EOS, o516, o552, o442, i187, i188)
f1327_0_main_NE(EOS, o516, o552, o442, i187, i188) → f1329_0_main_NE(EOS, o516, o552, o442, i187, i188)
f1327_0_main_NE(EOS, o516, o552, o442, i188, i188) → f1330_0_main_NE(EOS, o516, o552, o442, i188, i188)
f1329_0_main_NE(EOS, o516, o552, o442, i187, i188) → f1337_0_main_Load(EOS, o516, o552, o442) | !(=(i187, i188))
f1337_0_main_Load(EOS, o516, o552, o442) → f1344_0_main_InvokeMethod(EOS, o516, o552, o442)
f1344_0_main_InvokeMethod(EOS, o516, o552, java.lang.Object(o576sub)) → f1354_0_main_InvokeMethod(EOS, o516, o552, java.lang.Object(o576sub))
f1354_0_main_InvokeMethod(EOS, o516, o552, java.lang.Object(o576sub)) → f1369_0_getTail_Load(EOS, o516, o552, java.lang.Object(o576sub), java.lang.Object(o576sub))
f1369_0_getTail_Load(EOS, o516, o552, java.lang.Object(o576sub), java.lang.Object(o576sub)) → f1410_0_getTail_FieldAccess(EOS, o516, o552, java.lang.Object(o576sub), java.lang.Object(o576sub))
f1410_0_getTail_FieldAccess(EOS, o516, o552, java.lang.Object(List(EOC, o643)), java.lang.Object(List(EOC, o643))) → f1434_0_getTail_FieldAccess(EOS, o516, o552, java.lang.Object(List(EOC, o643)), java.lang.Object(List(EOC, o643)))
f1434_0_getTail_FieldAccess(EOS, o516, o552, java.lang.Object(List(EOC, o643)), java.lang.Object(List(EOC, o643))) → f1462_0_getTail_Return(EOS, o516, o552, java.lang.Object(List(EOC, o643)), o643)
f1462_0_getTail_Return(EOS, o516, o552, java.lang.Object(List(EOC, o643)), o643) → f1477_0_main_Store(EOS, o516, o552, o643)
f1477_0_main_Store(EOS, o516, o552, o643) → f1495_0_main_Load(EOS, o516, o552, o643)
f1495_0_main_Load(EOS, o516, o552, o643) → f1523_0_main_Load(EOS, o516, o552, o643)
f1523_0_main_Load(EOS, o516, o653, o442) → f1543_0_main_Load(EOS, o516, o653, o442, o516)
f1543_0_main_Load(EOS, o516, o653, o442, o516) → f1553_0_main_Load(EOS, o516, o653, o442, o516, o653)
f1553_0_main_Load(EOS, o516, o653, o442, o516, o653) → f1562_0_main_InvokeMethod(EOS, o516, o653, o442, o516, o653, o442)
f1562_0_main_InvokeMethod(EOS, o516, o653, o442, o516, o653, o442) → f1567_0_test_Load(EOS, o516, o653, o442, o516, o653, o442)
f1562_0_main_InvokeMethod(EOS, o516, o653, o442, o516, o653, o442) → f1567_1_test_Load(EOS, o516, o653, o442, o516, o653, o442, o516, o653, o442)
f1567_0_test_Load(EOS, o516, o653, o442, o516, o653, o442) → f1576_0_test_Load(EOS, o516, o653, o442, o516, o653, o442)
f1615_0_test_Return(EOS, o833, o837, o831, o833, o837, o831) → f1631_0_main_JMP(EOS, o833, o837, o831)
f1631_0_main_JMP(EOS, o833, o837, o831) → f1652_0_main_Load(EOS, o833, o837, o831)
f1652_0_main_Load(EOS, o833, o837, o831) → f414_0_main_Load(EOS, o833, o837, o831)
f414_0_main_Load(EOS, o39, o49, o73) → f417_0_main_InvokeMethod(EOS, o39, o49, o73, o39)
f1330_0_main_NE(EOS, o516, o552, o442, i188, i188) → f1338_0_main_Load(EOS, o516, o552, o442)
f1338_0_main_Load(EOS, o516, o552, o442) → f1346_0_main_InvokeMethod(EOS, o516, o442, o552)
f1346_0_main_InvokeMethod(EOS, o516, o442, java.lang.Object(o578sub)) → f1359_0_main_InvokeMethod(EOS, o516, o442, java.lang.Object(o578sub))
f1359_0_main_InvokeMethod(EOS, o516, o442, java.lang.Object(o578sub)) → f1375_0_getTail_Load(EOS, o516, o442, java.lang.Object(o578sub), java.lang.Object(o578sub))
f1375_0_getTail_Load(EOS, o516, o442, java.lang.Object(o578sub), java.lang.Object(o578sub)) → f1420_0_getTail_FieldAccess(EOS, o516, o442, java.lang.Object(o578sub), java.lang.Object(o578sub))
f1420_0_getTail_FieldAccess(EOS, o516, o442, java.lang.Object(List(EOC, o653)), java.lang.Object(List(EOC, o653))) → f1442_0_getTail_FieldAccess(EOS, o516, o442, java.lang.Object(List(EOC, o653)), java.lang.Object(List(EOC, o653)))
f1442_0_getTail_FieldAccess(EOS, o516, o442, java.lang.Object(List(EOC, o653)), java.lang.Object(List(EOC, o653))) → f1468_0_getTail_Return(EOS, o516, o442, java.lang.Object(List(EOC, o653)), o653)
f1468_0_getTail_Return(EOS, o516, o442, java.lang.Object(List(EOC, o653)), o653) → f1482_0_main_Store(EOS, o516, o442, o653)
f1482_0_main_Store(EOS, o516, o442, o653) → f1503_0_main_JMP(EOS, o516, o653, o442)
f1503_0_main_JMP(EOS, o516, o653, o442) → f1523_0_main_Load(EOS, o516, o653, o442)
f1255_0_main_LE(EOS, o468, o491, o442, i182, i185) → f1260_0_main_Load(EOS, o468, o491, o442) | >(i182, i185)
f1260_0_main_Load(EOS, o468, o491, o442) → f1263_0_main_InvokeMethod(EOS, o491, o442, o468)
f1263_0_main_InvokeMethod(EOS, o491, o442, java.lang.Object(o505sub)) → f1269_0_main_InvokeMethod(EOS, o491, o442, java.lang.Object(o505sub))
f1269_0_main_InvokeMethod(EOS, o491, o442, java.lang.Object(o505sub)) → f1274_0_getTail_Load(EOS, o491, o442, java.lang.Object(o505sub), java.lang.Object(o505sub))
f1274_0_getTail_Load(EOS, o491, o442, java.lang.Object(o505sub), java.lang.Object(o505sub)) → f1286_0_getTail_FieldAccess(EOS, o491, o442, java.lang.Object(o505sub), java.lang.Object(o505sub))
f1286_0_getTail_FieldAccess(EOS, o491, o442, java.lang.Object(List(EOC, o532)), java.lang.Object(List(EOC, o532))) → f1289_0_getTail_FieldAccess(EOS, o491, o442, java.lang.Object(List(EOC, o532)), java.lang.Object(List(EOC, o532)))
f1289_0_getTail_FieldAccess(EOS, o491, o442, java.lang.Object(List(EOC, o532)), java.lang.Object(List(EOC, o532))) → f1296_0_getTail_Return(EOS, o491, o442, java.lang.Object(List(EOC, o532)), o532)
f1296_0_getTail_Return(EOS, o491, o442, java.lang.Object(List(EOC, o532)), o532) → f1301_0_main_Store(EOS, o491, o442, o532)
f1301_0_main_Store(EOS, o491, o442, o532) → f1304_0_main_JMP(EOS, o532, o491, o442)
f1304_0_main_JMP(EOS, o532, o491, o442) → f1309_0_main_Load(EOS, o532, o491, o442)
f1309_0_main_Load(EOS, o532, o491, o442) → f1495_0_main_Load(EOS, o532, o491, o442)
f1100_0_main_NE(EOS, o300, o350, o391, matching1) → f1105_0_main_Load(EOS, o300, o350, o391) | =(matching1, 0)
f1105_0_main_Load(EOS, o300, o350, o391) → f1110_0_main_InvokeMethod(EOS, o300, o350, o391)
f1110_0_main_InvokeMethod(EOS, o300, o350, java.lang.Object(o411sub)) → f1117_0_main_InvokeMethod(EOS, o300, o350, java.lang.Object(o411sub))
f1117_0_main_InvokeMethod(EOS, o300, o350, java.lang.Object(o411sub)) → f1122_0_getTail_Load(EOS, o300, o350, java.lang.Object(o411sub), java.lang.Object(o411sub))
f1122_0_getTail_Load(EOS, o300, o350, java.lang.Object(o411sub), java.lang.Object(o411sub)) → f1143_0_getTail_FieldAccess(EOS, o300, o350, java.lang.Object(o411sub), java.lang.Object(o411sub))
f1143_0_getTail_FieldAccess(EOS, o300, o350, java.lang.Object(List(EOC, o442)), java.lang.Object(List(EOC, o442))) → f1149_0_getTail_FieldAccess(EOS, o300, o350, java.lang.Object(List(EOC, o442)), java.lang.Object(List(EOC, o442)))
f1149_0_getTail_FieldAccess(EOS, o300, o350, java.lang.Object(List(EOC, o442)), java.lang.Object(List(EOC, o442))) → f1159_0_getTail_Return(EOS, o300, o350, java.lang.Object(List(EOC, o442)), o442)
f1159_0_getTail_Return(EOS, o300, o350, java.lang.Object(List(EOC, o442)), o442) → f1170_0_main_Store(EOS, o300, o350, o442)
f1170_0_main_Store(EOS, o300, o350, o442) → f1178_0_main_Load(EOS, o300, o350, o442)
f1041_0_main_NE(EOS, o300, o350, o299, o299, matching1) → f1048_0_main_Load(EOS, o300, o350, o299, o299) | =(matching1, 0)
f1048_0_main_Load(EOS, o300, o350, o299, o299) → f1054_0_main_InvokeMethod(EOS, o300, o350, o299, o299)
f1054_0_main_InvokeMethod(EOS, o300, o350, java.lang.Object(o374sub), java.lang.Object(o374sub)) → f1059_0_main_InvokeMethod(EOS, o300, o350, java.lang.Object(o374sub), java.lang.Object(o374sub))
f1059_0_main_InvokeMethod(EOS, o300, o350, java.lang.Object(o374sub), java.lang.Object(o374sub)) → f1069_0_getTail_Load(EOS, o300, o350, java.lang.Object(o374sub), java.lang.Object(o374sub), java.lang.Object(o374sub))
f1069_0_getTail_Load(EOS, o300, o350, java.lang.Object(o374sub), java.lang.Object(o374sub), java.lang.Object(o374sub)) → f1082_0_getTail_FieldAccess(EOS, o300, o350, java.lang.Object(o374sub), java.lang.Object(o374sub), java.lang.Object(o374sub))
f1082_0_getTail_FieldAccess(EOS, o300, o350, java.lang.Object(List(EOC, o400)), java.lang.Object(List(EOC, o400)), java.lang.Object(List(EOC, o400))) → f1085_0_getTail_FieldAccess(EOS, o300, o350, java.lang.Object(List(EOC, o400)), java.lang.Object(List(EOC, o400)), java.lang.Object(List(EOC, o400)))
f1085_0_getTail_FieldAccess(EOS, o300, o350, java.lang.Object(List(EOC, o400)), java.lang.Object(List(EOC, o400)), java.lang.Object(List(EOC, o400))) → f1089_0_getTail_Return(EOS, o300, o350, java.lang.Object(List(EOC, o400)), java.lang.Object(List(EOC, o400)))
f1089_0_getTail_Return(EOS, o300, o350, java.lang.Object(List(EOC, o400)), java.lang.Object(List(EOC, o400))) → f1092_0_main_Store(EOS, o300, o350, java.lang.Object(List(EOC, o400)))
f1092_0_main_Store(EOS, o300, o350, java.lang.Object(List(EOC, o400))) → f1096_0_main_Load(EOS, o300, o350, java.lang.Object(List(EOC, o400)))
f1096_0_main_Load(EOS, o300, o350, java.lang.Object(List(EOC, o400))) → f1101_0_main_InvokeMethod(EOS, o300, o350, java.lang.Object(List(EOC, o400)), java.lang.Object(List(EOC, o400)))
f1101_0_main_InvokeMethod(EOS, o300, o350, java.lang.Object(List(EOC, o400)), java.lang.Object(List(EOC, o400))) → f1107_0_length_ConstantStackPush(EOS, java.lang.Object(List(EOC, o400)), java.lang.Object(List(EOC, o400)))
f1101_0_main_InvokeMethod(EOS, o300, o350, java.lang.Object(List(EOC, o400)), java.lang.Object(List(EOC, o400))) → f1107_1_length_ConstantStackPush(EOS, o300, o350, java.lang.Object(List(EOC, o400)), java.lang.Object(List(EOC, o400)), java.lang.Object(List(EOC, o400)))
f1107_0_length_ConstantStackPush(EOS, java.lang.Object(List(EOC, o400)), java.lang.Object(List(EOC, o400))) → f1112_0_length_ConstantStackPush(EOS, java.lang.Object(List(EOC, o400)), java.lang.Object(List(EOC, o400)))
f1133_0_length_Return(EOS, o300, o350, java.lang.Object(List(EOC, o400)), java.lang.Object(List(EOC, o400)), i170) → f1145_0_main_ConstantStackPush(EOS, o300, o350, java.lang.Object(List(EOC, o400)), i170)
f1145_0_main_ConstantStackPush(EOS, o300, o350, java.lang.Object(List(EOC, o400)), i170) → f1154_0_main_IntArithmetic(EOS, o300, o350, java.lang.Object(List(EOC, o400)), i170, 5)
f1154_0_main_IntArithmetic(EOS, o300, o350, java.lang.Object(List(EOC, o400)), i170, matching1) → f1165_0_main_NE(EOS, o300, o350, java.lang.Object(List(EOC, o400)), %(i170, 5)) | =(matching1, 5)
f1165_0_main_NE(EOS, o300, o350, java.lang.Object(List(EOC, o400)), i173) → f1094_0_main_NE(EOS, o300, o350, java.lang.Object(List(EOC, o400)), i173)
f421_1_length_ConstantStackPush(EOS, o342, o49, o73, o342, o342) → f1023_0_length_Return(EOS, o342, o49, o73, o342, i155)
f999_1_length_ConstantStackPush(EOS, o300, o350, o299, o299, o350, o350) → f1025_0_length_Return(EOS, o300, o350, o299, o299, o350, i156)
f1056_1_length_ConstantStackPush(EOS, o300, o350, o391, o391, o391) → f1084_0_length_Return(EOS, o300, o350, o391, o391, i166)
f1189_1_length_ConstantStackPush(EOS, o468, o350, o442, o468, o468) → f1210_0_length_Return(EOS, o468, o350, o442, o468, i182)
f1225_1_length_ConstantStackPush(EOS, o468, o491, o442, i182, o491, o491) → f1244_0_length_Return(EOS, o468, o491, o442, i182, o491, i185)
f1267_1_length_ConstantStackPush(EOS, o516, o491, o442, o516, o516) → f1287_0_length_Return(EOS, o516, o491, o442, o516, i187)
f1302_1_length_ConstantStackPush(EOS, o516, o552, o442, i187, o552, o552) → f1323_0_length_Return(EOS, o516, o552, o442, i187, o552, i188)
f1567_1_test_Load(EOS, o833, o837, o831, o833, o837, o831, o833, o837, o831) → f1615_0_test_Return(EOS, o833, o837, o831, o833, o837, o831)
f1107_1_length_ConstantStackPush(EOS, o300, o350, java.lang.Object(List(EOC, o400)), java.lang.Object(List(EOC, o400)), java.lang.Object(List(EOC, o400))) → f1133_0_length_Return(EOS, o300, o350, java.lang.Object(List(EOC, o400)), java.lang.Object(List(EOC, o400)), i170)

Combined rules. Obtained 16 IRules

P rules:
f1094_0_main_NE(EOS, x0, x1, x2, x3) → f1184_0_main_InvokeMethod(EOS, x0, x1, x2, x0) | >(x3, 0)
f1184_0_main_InvokeMethod(EOS, x0, x1, x2, x0) → f1193_0_length_ConstantStackPush(EOS, x0, x0)
f1562_0_main_InvokeMethod(EOS, x0, x1, x2, x0, x1, x2) → f1576_0_test_Load(EOS, x0, x1, x2, x0, x1, x2)
f1094_0_main_NE(EOS, x0, x1, java.lang.Object(List(EOC, x2)), 0) → f1184_0_main_InvokeMethod(EOS, x0, x1, x2, x0)
f1184_0_main_InvokeMethod(EOS, x0, x1, x2, x0) → f1229_0_length_ConstantStackPush(EOS, x1, x1)
f1184_0_main_InvokeMethod(EOS, x0, x1, x2, x0) → f1273_0_length_ConstantStackPush(EOS, x0, x0)
f1184_0_main_InvokeMethod(EOS, java.lang.Object(List(EOC, x0)), x1, x2, java.lang.Object(List(EOC, x0))) → f1562_0_main_InvokeMethod(EOS, x0, x1, x2, x0, x1, x2)
f1184_0_main_InvokeMethod(EOS, x0, x1, x2, x0) → f1308_0_length_ConstantStackPush(EOS, x1, x1)
f1184_0_main_InvokeMethod(EOS, x0, x1, java.lang.Object(List(EOC, x2)), x0) → f1562_0_main_InvokeMethod(EOS, x0, x1, x2, x0, x1, x2)
f1184_0_main_InvokeMethod(EOS, x0, java.lang.Object(List(EOC, x1)), x2, x0) → f1562_0_main_InvokeMethod(EOS, x0, x1, x2, x0, x1, x2)
f1562_0_main_InvokeMethod(EOS, x0, x1, x2, x0, x1, x2) → f424_0_length_ConstantStackPush(EOS, x0, x0)
f1562_0_main_InvokeMethod(EOS, x0, x1, x2, x0, x1, x2) → f1002_0_length_ConstantStackPush(EOS, x2, x2)
f1562_0_main_InvokeMethod(EOS, x0, x1, x2, x0, x1, x2) → f1064_0_length_ConstantStackPush(EOS, x0, x0)
f1562_0_main_InvokeMethod(EOS, java.lang.Object(List(EOC, x0)), x1, x2, java.lang.Object(List(EOC, x0)), x1, x2) → f1112_0_length_ConstantStackPush(EOS, java.lang.Object(List(EOC, x0)), java.lang.Object(List(EOC, x0)))
f1562_0_main_InvokeMethod(EOS, x0, x1, x2, x0, x1, x2) → f1094_0_main_NE(EOS, x1, x2, x0, %(x3, 5))
f1562_0_main_InvokeMethod(EOS, java.lang.Object(List(EOC, x0)), x1, x2, java.lang.Object(List(EOC, x0)), x1, x2) → f1094_0_main_NE(EOS, x1, x2, java.lang.Object(List(EOC, x0)), %(x3, 5))

Filtered ground terms:

f1094_0_main_NE(x1, x2, x3, x4, x5) → f1094_0_main_NE(x2, x3, x4, x5)
Cond_f1094_0_main_NE(x1, x2, x3, x4, x5, x6) → Cond_f1094_0_main_NE(x1, x3, x4, x5, x6)
f1184_0_main_InvokeMethod(x1, x2, x3, x4, x5) → f1184_0_main_InvokeMethod(x2, x3, x4, x5)
f1193_0_length_ConstantStackPush(x1, x2, x3) → f1193_0_length_ConstantStackPush(x2, x3)
f1562_0_main_InvokeMethod(x1, x2, x3, x4, x5, x6, x7) → f1562_0_main_InvokeMethod(x2, x3, x4, x5, x6, x7)
f1576_0_test_Load(x1, x2, x3, x4, x5, x6, x7) → f1576_0_test_Load(x2, x3, x4, x5, x6, x7)
f1229_0_length_ConstantStackPush(x1, x2, x3) → f1229_0_length_ConstantStackPush(x2, x3)
f1273_0_length_ConstantStackPush(x1, x2, x3) → f1273_0_length_ConstantStackPush(x2, x3)
f1308_0_length_ConstantStackPush(x1, x2, x3) → f1308_0_length_ConstantStackPush(x2, x3)
f424_0_length_ConstantStackPush(x1, x2, x3) → f424_0_length_ConstantStackPush(x2, x3)
f1002_0_length_ConstantStackPush(x1, x2, x3) → f1002_0_length_ConstantStackPush(x2, x3)
f1064_0_length_ConstantStackPush(x1, x2, x3) → f1064_0_length_ConstantStackPush(x2, x3)
f1112_0_length_ConstantStackPush(x1, x2, x3) → f1112_0_length_ConstantStackPush(x2, x3)
List(x1, x2) → List(x2)

Filtered duplicate terms:

f1184_0_main_InvokeMethod(x1, x2, x3, x4) → f1184_0_main_InvokeMethod(x2, x3, x4)
f1193_0_length_ConstantStackPush(x1, x2) → f1193_0_length_ConstantStackPush(x2)
f1562_0_main_InvokeMethod(x1, x2, x3, x4, x5, x6) → f1562_0_main_InvokeMethod(x4, x5, x6)
f1576_0_test_Load(x1, x2, x3, x4, x5, x6) → f1576_0_test_Load(x4, x5, x6)
f1229_0_length_ConstantStackPush(x1, x2) → f1229_0_length_ConstantStackPush(x2)
f1273_0_length_ConstantStackPush(x1, x2) → f1273_0_length_ConstantStackPush(x2)
f1308_0_length_ConstantStackPush(x1, x2) → f1308_0_length_ConstantStackPush(x2)
f424_0_length_ConstantStackPush(x1, x2) → f424_0_length_ConstantStackPush(x2)
f1002_0_length_ConstantStackPush(x1, x2) → f1002_0_length_ConstantStackPush(x2)
f1064_0_length_ConstantStackPush(x1, x2) → f1064_0_length_ConstantStackPush(x2)
f1112_0_length_ConstantStackPush(x1, x2) → f1112_0_length_ConstantStackPush(x2)

Filtered unneeded terms:

Cond_f1094_0_main_NE(x1, x2, x3, x4, x5) → Cond_f1094_0_main_NE(x1, x2, x3, x4)

Prepared 16 rules for path length conversion:

P rules:
f1094_0_main_NE(x0, x1, x2, x3) → f1184_0_main_InvokeMethod(x1, x2, x0) | >(x3, 0)
f1184_0_main_InvokeMethod(x1, x2, x0) → f1193_0_length_ConstantStackPush(x0)
f1562_0_main_InvokeMethod(x0, x1, x2) → f1576_0_test_Load(x0, x1, x2)
f1094_0_main_NE(x0, x1, java.lang.Object(List(x2)), 0) → f1184_0_main_InvokeMethod(x1, x2, x0)
f1184_0_main_InvokeMethod(x1, x2, x0) → f1229_0_length_ConstantStackPush(x1)
f1184_0_main_InvokeMethod(x1, x2, x0) → f1273_0_length_ConstantStackPush(x0)
f1184_0_main_InvokeMethod(x1, x2, java.lang.Object(List(x0))) → f1562_0_main_InvokeMethod(x0, x1, x2)
f1184_0_main_InvokeMethod(x1, x2, x0) → f1308_0_length_ConstantStackPush(x1)
f1184_0_main_InvokeMethod(x1, java.lang.Object(List(x2)), x0) → f1562_0_main_InvokeMethod(x0, x1, x2)
f1184_0_main_InvokeMethod(java.lang.Object(List(x1)), x2, x0) → f1562_0_main_InvokeMethod(x0, x1, x2)
f1562_0_main_InvokeMethod(x0, x1, x2) → f424_0_length_ConstantStackPush(x0)
f1562_0_main_InvokeMethod(x0, x1, x2) → f1002_0_length_ConstantStackPush(x2)
f1562_0_main_InvokeMethod(x0, x1, x2) → f1064_0_length_ConstantStackPush(x0)
f1562_0_main_InvokeMethod(java.lang.Object(List(x0)), x1, x2) → f1112_0_length_ConstantStackPush(java.lang.Object(List(x0)))
f1562_0_main_InvokeMethod(x0, x1, x2) → f1094_0_main_NE(x1, x2, x0, %(x3, 5))
f1562_0_main_InvokeMethod(java.lang.Object(List(x0)), x1, x2) → f1094_0_main_NE(x1, x2, java.lang.Object(List(x0)), %(x3, 5))

Finished conversion. Obtained 9 rules.

P rules:
f1094_0_main_NE(v61, v62, v63, x3) → f1184_0_main_InvokeMethod(v64, v65, v66) | &&(&&(&&(&&(&&(&&(&&(&&(&&(>(x3, 0), >(+(v66, 1), 0)), <=(v66, v61)), >(+(v65, 1), 0)), <=(v65, v63)), >(+(v64, 1), 0)), <=(v64, v62)), >(+(v63, 1), 0)), >(+(v62, 1), 0)), >(+(v61, 1), 0))
f1094_0_main_NE(v67, v68, v69, c0) → f1184_0_main_InvokeMethod(v70, v71, v72) | &&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v72, 1), 0), <=(v72, v67)), >(+(v71, 1), 0)), <=(+(v71, 1), v69)), >(+(v70, 1), 0)), <=(v70, v68)), >(+(v69, 1), 1)), >(+(v68, 1), 0)), >(+(v67, 1), 0)), =(0, c0))
f1184_0_main_InvokeMethod(v73, v74, v75) → f1562_0_main_InvokeMethod(v76, v77, v78) | &&(&&(&&(&&(&&(&&(&&(&&(>(+(v78, 1), 0), <=(v78, v74)), >(+(v77, 1), 0)), <=(v77, v73)), >(+(v76, 1), 0)), <=(+(v76, 1), v75)), >(+(v75, 1), 1)), >(+(v74, 1), 0)), >(+(v73, 1), 0))
f1184_0_main_InvokeMethod(v79, v80, v81) → f1562_0_main_InvokeMethod(v82, v83, v84) | &&(&&(&&(&&(&&(&&(&&(&&(>(+(v84, 1), 0), <=(+(v84, 1), v80)), >(+(v83, 1), 0)), <=(v83, v79)), >(+(v82, 1), 0)), <=(v82, v81)), >(+(v81, 1), 0)), >(+(v80, 1), 1)), >(+(v79, 1), 0))
f1184_0_main_InvokeMethod(v85, v86, v87) → f1562_0_main_InvokeMethod(v88, v89, v90) | &&(&&(&&(&&(&&(&&(&&(&&(>(+(v90, 1), 0), <=(v90, v86)), >(+(v89, 1), 0)), <=(+(v89, 1), v85)), >(+(v88, 1), 0)), <=(v88, v87)), >(+(v87, 1), 0)), >(+(v86, 1), 0)), >(+(v85, 1), 1))
f1562_0_main_InvokeMethod(v91, v92, v93) → f1562_0_main_InvokeMethod'(v91, v92, v93) | &&(&&(&&(&&(&&(&&(&&(&&(>(+(v96, 1), 0), <=(v96, v91)), >(+(v95, 1), 0)), <=(v95, v93)), >(+(v94, 1), 0)), <=(v94, v92)), >(+(v93, 1), 0)), >(+(v92, 1), 0)), >(+(v91, 1), 0))
f1562_0_main_InvokeMethod'(v91, v92, v93) → f1094_0_main_NE(v94, v95, v96, -(x46, *(5, div))) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>=(-(x46, *(5, div)), 0), <(-(x46, *(5, div)), 5)), >(+(v96, 1), 0)), <=(v96, v91)), >(+(v95, 1), 0)), <=(v95, v93)), >(+(v94, 1), 0)), <=(v94, v92)), >(+(v93, 1), 0)), >(+(v92, 1), 0)), >(+(v91, 1), 0))
f1562_0_main_InvokeMethod(v97, v98, v99) → f1562_0_main_InvokeMethod'(v97, v98, v99) | &&(&&(&&(&&(&&(&&(&&(&&(>=(v99, v101), >(+(v99, 1), 0)), >=(v98, v100)), >(+(v98, 1), 0)), >=(v97, v102)), >(+(v97, 1), 1)), >(+(v102, 1), 1)), >(+(v100, 1), 0)), >(+(v101, 1), 0))
f1562_0_main_InvokeMethod'(v97, v98, v99) → f1094_0_main_NE(v100, v101, v102, -(x50, *(5, div))) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>=(-(x50, *(5, div)), 0), <(-(x50, *(5, div)), 5)), >=(v99, v101)), >(+(v99, 1), 0)), >=(v98, v100)), >(+(v98, 1), 0)), >=(v97, v102)), >(+(v97, 1), 1)), >(+(v102, 1), 1)), >(+(v100, 1), 0)), >(+(v101, 1), 0))

(22) Obligation:

Rules:
f1094_0_main_NE(v61, v62, v63, x3) → f1184_0_main_InvokeMethod(v64, v65, v66) | &&(&&(&&(&&(&&(&&(&&(&&(&&(>(x3, 0), >(+(v66, 1), 0)), <=(v66, v61)), >(+(v65, 1), 0)), <=(v65, v63)), >(+(v64, 1), 0)), <=(v64, v62)), >(+(v63, 1), 0)), >(+(v62, 1), 0)), >(+(v61, 1), 0))
f1094_0_main_NE(v67, v68, v69, c0) → f1184_0_main_InvokeMethod(v70, v71, v72) | &&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v72, 1), 0), <=(v72, v67)), >(+(v71, 1), 0)), <=(+(v71, 1), v69)), >(+(v70, 1), 0)), <=(v70, v68)), >(+(v69, 1), 1)), >(+(v68, 1), 0)), >(+(v67, 1), 0)), =(0, c0))
f1184_0_main_InvokeMethod(v73, v74, v75) → f1562_0_main_InvokeMethod(v76, v77, v78) | &&(&&(&&(&&(&&(&&(&&(&&(>(+(v78, 1), 0), <=(v78, v74)), >(+(v77, 1), 0)), <=(v77, v73)), >(+(v76, 1), 0)), <=(+(v76, 1), v75)), >(+(v75, 1), 1)), >(+(v74, 1), 0)), >(+(v73, 1), 0))
f1184_0_main_InvokeMethod(v79, v80, v81) → f1562_0_main_InvokeMethod(v82, v83, v84) | &&(&&(&&(&&(&&(&&(&&(&&(>(+(v84, 1), 0), <=(+(v84, 1), v80)), >(+(v83, 1), 0)), <=(v83, v79)), >(+(v82, 1), 0)), <=(v82, v81)), >(+(v81, 1), 0)), >(+(v80, 1), 1)), >(+(v79, 1), 0))
f1184_0_main_InvokeMethod(v85, v86, v87) → f1562_0_main_InvokeMethod(v88, v89, v90) | &&(&&(&&(&&(&&(&&(&&(&&(>(+(v90, 1), 0), <=(v90, v86)), >(+(v89, 1), 0)), <=(+(v89, 1), v85)), >(+(v88, 1), 0)), <=(v88, v87)), >(+(v87, 1), 0)), >(+(v86, 1), 0)), >(+(v85, 1), 1))
f1562_0_main_InvokeMethod(v91, v92, v93) → f1562_0_main_InvokeMethod'(v91, v92, v93) | &&(&&(&&(&&(&&(&&(&&(&&(>(+(v96, 1), 0), <=(v96, v91)), >(+(v95, 1), 0)), <=(v95, v93)), >(+(v94, 1), 0)), <=(v94, v92)), >(+(v93, 1), 0)), >(+(v92, 1), 0)), >(+(v91, 1), 0))
f1562_0_main_InvokeMethod'(v91, v92, v93) → f1094_0_main_NE(v94, v95, v96, -(x46, *(5, div))) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>=(-(x46, *(5, div)), 0), <(-(x46, *(5, div)), 5)), >(+(v96, 1), 0)), <=(v96, v91)), >(+(v95, 1), 0)), <=(v95, v93)), >(+(v94, 1), 0)), <=(v94, v92)), >(+(v93, 1), 0)), >(+(v92, 1), 0)), >(+(v91, 1), 0))
f1562_0_main_InvokeMethod(v97, v98, v99) → f1562_0_main_InvokeMethod'(v97, v98, v99) | &&(&&(&&(&&(&&(&&(&&(&&(>=(v99, v101), >(+(v99, 1), 0)), >=(v98, v100)), >(+(v98, 1), 0)), >=(v97, v102)), >(+(v97, 1), 1)), >(+(v102, 1), 1)), >(+(v100, 1), 0)), >(+(v101, 1), 0))
f1562_0_main_InvokeMethod'(v97, v98, v99) → f1094_0_main_NE(v100, v101, v102, -(x50, *(5, div))) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>=(-(x50, *(5, div)), 0), <(-(x50, *(5, div)), 5)), >=(v99, v101)), >(+(v99, 1), 0)), >=(v98, v100)), >(+(v98, 1), 0)), >=(v97, v102)), >(+(v97, 1), 1)), >(+(v102, 1), 1)), >(+(v100, 1), 0)), >(+(v101, 1), 0))

(23) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f1094_0_main_NE(x61, x63, x65, x67)] = 4·x61 + 4·x63 + 4·x65
[f1184_0_main_InvokeMethod(x70, x72, x74)] = -1 + 4·x70 + 4·x72 + 4·x74
[f1562_0_main_InvokeMethod(x77, x79, x81)] = 2 + 4·x77 + 4·x79 + 4·x81
[f1562_0_main_InvokeMethod'(x84, x86, x88)] = 1 + 4·x84 + 4·x86 + 4·x88

Therefore the following rule(s) have been dropped:

f1094_0_main_NE(x0, x1, x2, x3) → f1184_0_main_InvokeMethod(x4, x5, x6) | &&(&&(&&(&&(&&(&&(&&(&&(&&(>(x3, 0), >(+(x6, 1), 0)), <=(x6, x0)), >(+(x5, 1), 0)), <=(x5, x2)), >(+(x4, 1), 0)), <=(x4, x1)), >(+(x2, 1), 0)), >(+(x1, 1), 0)), >(+(x0, 1), 0))
f1094_0_main_NE(x7, x8, x9, x10) → f1184_0_main_InvokeMethod(x11, x12, x13) | &&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(x13, 1), 0), <=(x13, x7)), >(+(x12, 1), 0)), <=(+(x12, 1), x9)), >(+(x11, 1), 0)), <=(x11, x8)), >(+(x9, 1), 1)), >(+(x8, 1), 0)), >(+(x7, 1), 0)), =(0, x10))
f1184_0_main_InvokeMethod(x14, x15, x16) → f1562_0_main_InvokeMethod(x17, x18, x19) | &&(&&(&&(&&(&&(&&(&&(&&(>(+(x19, 1), 0), <=(x19, x15)), >(+(x18, 1), 0)), <=(x18, x14)), >(+(x17, 1), 0)), <=(+(x17, 1), x16)), >(+(x16, 1), 1)), >(+(x15, 1), 0)), >(+(x14, 1), 0))
f1184_0_main_InvokeMethod(x20, x21, x22) → f1562_0_main_InvokeMethod(x23, x24, x25) | &&(&&(&&(&&(&&(&&(&&(&&(>(+(x25, 1), 0), <=(+(x25, 1), x21)), >(+(x24, 1), 0)), <=(x24, x20)), >(+(x23, 1), 0)), <=(x23, x22)), >(+(x22, 1), 0)), >(+(x21, 1), 1)), >(+(x20, 1), 0))
f1184_0_main_InvokeMethod(x26, x27, x28) → f1562_0_main_InvokeMethod(x29, x30, x31) | &&(&&(&&(&&(&&(&&(&&(&&(>(+(x31, 1), 0), <=(x31, x27)), >(+(x30, 1), 0)), <=(+(x30, 1), x26)), >(+(x29, 1), 0)), <=(x29, x28)), >(+(x28, 1), 0)), >(+(x27, 1), 0)), >(+(x26, 1), 1))
f1562_0_main_InvokeMethod(x32, x33, x34) → f1562_0_main_InvokeMethod'(x32, x33, x34) | &&(&&(&&(&&(&&(&&(&&(&&(>(+(x35, 1), 0), <=(x35, x32)), >(+(x36, 1), 0)), <=(x36, x34)), >(+(x37, 1), 0)), <=(x37, x33)), >(+(x34, 1), 0)), >(+(x33, 1), 0)), >(+(x32, 1), 0))
f1562_0_main_InvokeMethod'(x38, x39, x40) → f1094_0_main_NE(x41, x42, x43, -(x44, *(5, x45))) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>=(-(x44, *(5, x45)), 0), <(-(x44, *(5, x45)), 5)), >(+(x43, 1), 0)), <=(x43, x38)), >(+(x42, 1), 0)), <=(x42, x40)), >(+(x41, 1), 0)), <=(x41, x39)), >(+(x40, 1), 0)), >(+(x39, 1), 0)), >(+(x38, 1), 0))
f1562_0_main_InvokeMethod(x46, x47, x48) → f1562_0_main_InvokeMethod'(x46, x47, x48) | &&(&&(&&(&&(&&(&&(&&(&&(>=(x48, x49), >(+(x48, 1), 0)), >=(x47, x50)), >(+(x47, 1), 0)), >=(x46, x51)), >(+(x46, 1), 1)), >(+(x51, 1), 1)), >(+(x50, 1), 0)), >(+(x49, 1), 0))
f1562_0_main_InvokeMethod'(x52, x53, x54) → f1094_0_main_NE(x55, x56, x57, -(x58, *(5, x59))) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>=(-(x58, *(5, x59)), 0), <(-(x58, *(5, x59)), 5)), >=(x54, x56)), >(+(x54, 1), 0)), >=(x53, x55)), >(+(x53, 1), 0)), >=(x52, x57)), >(+(x52, 1), 1)), >(+(x57, 1), 1)), >(+(x55, 1), 0)), >(+(x56, 1), 0))

(0) Obligation:

(1) JBCToGraph (SOUND transformation)

(2) Obligation:

(3) TerminationGraphToSCCProof (SOUND transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) SCCToIntTRSProof (SOUND transformation)

(7) Obligation:

(8) PolynomialOrderProcessor (EQUIVALENT transformation)

(9) YES

(10) Obligation:

(11) SCCToIntTRSProof (SOUND transformation)

(12) Obligation:

(13) PolynomialOrderProcessor (EQUIVALENT transformation)

(14) YES

(15) Obligation:

(16) SCCToIntTRSProof (SOUND transformation)

(17) Obligation:

(18) LinearRankingProcessor (EQUIVALENT transformation)

(19) YES

(20) Obligation:

(21) SCCToIntTRSProof (SOUND transformation)

(22) Obligation:

(23) PolynomialOrderProcessor (EQUIVALENT transformation)

(24) YES