Runtime Complexity proof of /tmp/tmpQMbKg9/reminder.pl

Runtime Complexity of the query pattern
rem(g,g,a)
w.r.t. the given Prolog program could be shown to be BOUNDS(O(1), O(n^2)).

0 Prolog

↳1 LPReorderTransformerProof (⇔, 0 ms)

↳2 Prolog

↳3 PrologToCdtProblemTransformerProof (UPPER BOUND (ID), 157 ms)

↳4 CdtProblem

    ↳5 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳6 CdtProblem

    ↳7 CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳8 CdtProblem

    ↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))), 692 ms)

    ↳10 CdtProblem

    ↳11 CdtKnowledgeProof (⇔, 0 ms)

    ↳12 CdtProblem

    ↳13 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳14 CdtProblem

    ↳15 CdtGraphRemoveDanglingProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳16 CdtProblem

    ↳17 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳18 CdtProblem

    ↳19 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))), 735 ms)

    ↳20 CdtProblem

    ↳21 SIsEmptyProof (⇔, 0 ms)

    ↳22 BOUNDS(O(1), O(1))

↳23 PrologToCdtProblemTransformerProof (UPPER BOUND (ID), 154 ms)

↳24 CdtProblem

    ↳25 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳26 CdtProblem

    ↳27 CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳28 CdtProblem

    ↳29 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))), 730 ms)

    ↳30 CdtProblem

    ↳31 CdtKnowledgeProof (⇔, 0 ms)

    ↳32 CdtProblem

    ↳33 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳34 CdtProblem

    ↳35 CdtGraphRemoveDanglingProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳36 CdtProblem

    ↳37 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳38 CdtProblem

(0) Obligation:

Clauses:

rem(X, Y, R) :- ','(notZero(Y), ','(sub(X, Y, Z), rem(Z, Y, R))).
rem(X, Y, X) :- ','(notZero(Y), geq(X, Y)).
sub(s(X), s(Y), Z) :- sub(X, Y, Z).
sub(X, 0, X).
notZero(s(X)).
geq(s(X), s(Y)) :- geq(X, Y).
geq(X, 0).

Query: rem(g,g,a)

(1) LPReorderTransformerProof (EQUIVALENT transformation)

Reordered facts before rules in definite LP [PROLOG].

(2) Obligation:

Clauses:

sub(X, 0, X).
notZero(s(X)).
geq(X, 0).
rem(X, Y, R) :- ','(notZero(Y), ','(sub(X, Y, Z), rem(Z, Y, R))).
rem(X, Y, X) :- ','(notZero(Y), geq(X, Y)).
sub(s(X), s(Y), Z) :- sub(X, Y, Z).
geq(s(X), s(Y)) :- geq(X, Y).

Query: rem(g,g,a)

(3) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)

Built complexity over-approximating cdt problems from derivation graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: rem(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: rem(T1, T2, T3), SCOPE: 1, CLAUSE: 3 | rem(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: rem(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: rem(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(notZero(T23), ','(sub(T22, T23, X22), rem(X22, T23, T25)))\n\nT22 is ground\nT23 is ground\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: ','(notZero(T23), ','(sub(T22, T23, X22), rem(X22, T23, T25))), SCOPE: 2, CLAUSE: 1\n\nT22 is ground\nT23 is ground\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ','(sub(T22, s(T30), X22), rem(X22, s(T30), T25))\n\nT22 is ground\nT30 is ground\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: sub(T22, s(T30), X22)\n\nT22 is ground\nT30 is ground\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: rem(T33, s(T30), T25)\n\nT30 is ground\nT33 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: sub(T22, s(T30), X22), SCOPE: 3, CLAUSE: 0 | sub(T22, s(T30), X22), SCOPE: 3, CLAUSE: 5\n\nT22 is ground\nT30 is ground\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: sub(T22, s(T30), X22), SCOPE: 3, CLAUSE: 5\n\nT22 is ground\nT30 is ground\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: sub(T41, T42, X44)\n\nT41 is ground\nT42 is ground\nX44 is free", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: sub(T41, T42, X44), SCOPE: 4, CLAUSE: 0 | sub(T41, T42, X44), SCOPE: 4, CLAUSE: 5\n\nT41 is ground\nT42 is ground\nX44 is free", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: true | sub(T47, 0, X44), SCOPE: 4, CLAUSE: 5\n\nT47 is ground\nX44 is free", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: sub(T41, T42, X44), SCOPE: 4, CLAUSE: 5\n\nT41 is ground\nT42 is ground\nX44 is free\nX49 is free\nsub(T41, T42, X44) !=? sub(X49, 0, X49)", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: sub(T47, 0, X44), SCOPE: 4, CLAUSE: 5\n\nT47 is ground\nX44 is free", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: sub(T53, T54, X64)\n\nT53 is ground\nT54 is ground\nX64 is free", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: ','(notZero(T65), geq(T64, T65))\n\nT64 is ground\nT65 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: ','(notZero(T65), geq(T64, T65)), SCOPE: 5, CLAUSE: 1\n\nT64 is ground\nT65 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: geq(T64, s(T70))\n\nT64 is ground\nT70 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: geq(T64, s(T70)), SCOPE: 6, CLAUSE: 2 | geq(T64, s(T70)), SCOPE: 6, CLAUSE: 6\n\nT64 is ground\nT70 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: geq(T64, s(T70)), SCOPE: 6, CLAUSE: 6\n\nT64 is ground\nT70 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: geq(T78, T79)\n\nT78 is ground\nT79 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: geq(T78, T79), SCOPE: 7, CLAUSE: 2 | geq(T78, T79), SCOPE: 7, CLAUSE: 6\n\nT78 is ground\nT79 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: true | geq(T84, 0), SCOPE: 7, CLAUSE: 6\n\nT84 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: geq(T78, T79), SCOPE: 7, CLAUSE: 6\n\nT78 is ground\nT79 is ground\nX95 is free\ngeq(T78, T79) !=? geq(X95, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: geq(T84, 0), SCOPE: 7, CLAUSE: 6\n\nT84 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: geq(T90, T91)\n\nT90 is ground\nT91 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 73 [arrowhead = none ];
73 -> 4;

74 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
4 -> 74 [arrowhead = none ];
74 -> 11;

75 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
4 -> 75 [arrowhead = none ];
75 -> 12;

76 [label="ONLY EVAL with clause\nrem(X19, X20, X21) :- ','(notZero(X20), ','(sub(X19, X20, X22), rem(X22, X20, X21))).\nand substitutionT1 -> T22,\nX19 -> T22,\nT2 -> T23,\nX20 -> T23,\nT3 -> T25,\nX21 -> T25,\nT24 -> T25", fontsize=14, style = filled, fillcolor = lightblue];
11 -> 76 [arrowhead = none ];
76 -> 13;

77 [label="EVAL with clause\nrem(X75, X76, X75) :- ','(notZero(X76), geq(X75, X76)).\nand substitutionT1 -> T64,\nX75 -> T64,\nT2 -> T65,\nX76 -> T65,\nT3 -> T64", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 77 [arrowhead = none ];
77 -> 44;

78 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
12 -> 78 [arrowhead = none ];
78 -> 45;

79 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
13 -> 79 [arrowhead = none ];
79 -> 14;

80 [label="EVAL with clause\nnotZero(s(X27)).\nand substitutionX27 -> T30,\nT23 -> s(T30)", fontsize=14, style = filled, fillcolor = lightblue];
14 -> 80 [arrowhead = none ];
80 -> 17;

81 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
14 -> 81 [arrowhead = none ];
81 -> 18;

82 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
17 -> 82 [arrowhead = none ];
82 -> 19;

83 [label="SPLIT 2\nnew knowledge:\nT22 is ground\nT30 is ground\nT33 is ground\nreplacements:X22 -> T33", fontsize=14, style = filled, fillcolor = violet];
17 -> 83 [arrowhead = none ];
83 -> 21;

84 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
19 -> 84 [arrowhead = none ];
84 -> 23;

85 [label="INSTANCE with matching:\nT1 -> T33\nT2 -> s(T30)\nT3 -> T25", fontsize=14, style = filled, fillcolor = lightgrey];
21 -> 85 [arrowhead = none , style=dashed];
85 -> 1[style=dashed];

86 [label="BACKTRACK\nfor clause: sub(X, 0, X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
23 -> 86 [arrowhead = none ];
86 -> 24;

87 [label="EVAL with clause\nsub(s(X41), s(X42), X43) :- sub(X41, X42, X43).\nand substitutionX41 -> T41,\nT22 -> s(T41),\nT30 -> T42,\nX42 -> T42,\nX22 -> X44,\nX43 -> X44", fontsize=14, style = filled, fillcolor = lightblue];
24 -> 87 [arrowhead = none ];
87 -> 27;

88 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
24 -> 88 [arrowhead = none ];
88 -> 28;

89 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
27 -> 89 [arrowhead = none ];
89 -> 30;

90 [label="EVAL with clause\nsub(X49, 0, X49).\nand substitutionT41 -> T47,\nX49 -> T47,\nT42 -> 0,\nX44 -> T47", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 90 [arrowhead = none ];
90 -> 34;

91 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
30 -> 91 [arrowhead = none ];
91 -> 35;

92 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
34 -> 92 [arrowhead = none ];
92 -> 36;

93 [label="EVAL with clause\nsub(s(X61), s(X62), X63) :- sub(X61, X62, X63).\nand substitutionX61 -> T53,\nT41 -> s(T53),\nX62 -> T54,\nT42 -> s(T54),\nX44 -> X64,\nX63 -> X64", fontsize=14, style = filled, fillcolor = lightblue];
35 -> 93 [arrowhead = none ];
93 -> 41;

94 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
35 -> 94 [arrowhead = none ];
94 -> 42;

95 [label="BACKTRACK\nfor clause: sub(s(X), s(Y), Z) :- sub(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
36 -> 95 [arrowhead = none ];
95 -> 38;

96 [label="INSTANCE with matching:\nT41 -> T53\nT42 -> T54\nX44 -> X64", fontsize=14, style = filled, fillcolor = lightgrey];
41 -> 96 [arrowhead = none , style=dashed];
96 -> 27[style=dashed];

97 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
44 -> 97 [arrowhead = none ];
97 -> 48;

98 [label="EVAL with clause\nnotZero(s(X81)).\nand substitutionX81 -> T70,\nT65 -> s(T70)", fontsize=14, style = filled, fillcolor = lightblue];
48 -> 98 [arrowhead = none ];
98 -> 50;

99 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
48 -> 99 [arrowhead = none ];
99 -> 51;

100 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
50 -> 100 [arrowhead = none ];
100 -> 53;

101 [label="BACKTRACK\nfor clause: geq(X, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
53 -> 101 [arrowhead = none ];
101 -> 54;

102 [label="EVAL with clause\ngeq(s(X89), s(X90)) :- geq(X89, X90).\nand substitutionX89 -> T78,\nT64 -> s(T78),\nT70 -> T79,\nX90 -> T79", fontsize=14, style = filled, fillcolor = lightblue];
54 -> 102 [arrowhead = none ];
102 -> 57;

103 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
54 -> 103 [arrowhead = none ];
103 -> 58;

104 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
57 -> 104 [arrowhead = none ];
104 -> 61;

105 [label="EVAL with clause\ngeq(X95, 0).\nand substitutionT78 -> T84,\nX95 -> T84,\nT79 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
61 -> 105 [arrowhead = none ];
105 -> 63;

106 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
61 -> 106 [arrowhead = none ];
106 -> 64;

107 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
63 -> 107 [arrowhead = none ];
107 -> 65;

108 [label="EVAL with clause\ngeq(s(X102), s(X103)) :- geq(X102, X103).\nand substitutionX102 -> T90,\nT78 -> s(T90),\nX103 -> T91,\nT79 -> s(T91)", fontsize=14, style = filled, fillcolor = lightblue];
64 -> 108 [arrowhead = none ];
108 -> 71;

109 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
64 -> 109 [arrowhead = none ];
109 -> 72;

110 [label="BACKTRACK\nfor clause: geq(s(X), s(Y)) :- geq(X, Y)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
65 -> 110 [arrowhead = none ];
110 -> 67;

111 [label="INSTANCE with matching:\nT78 -> T90\nT79 -> T91", fontsize=14, style = filled, fillcolor = lightgrey];
71 -> 111 [arrowhead = none , style=dashed];
111 -> 57[style=dashed];

}

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f4_in(z0, z1), z0, z1)
U1(f4_out1(z0), z1, z2) → f1_out1(z0)
U1(f4_out2(z0), z1, z2) → f1_out1(z0)
f57_in(z0, 0) → f57_out1
f57_in(s(z0), s(z1)) → U2(f57_in(z0, z1), s(z0), s(z1))
U2(f57_out1, s(z0), s(z1)) → f57_out1
f27_in(z0, 0) → f27_out1(z0)
f27_in(s(z0), s(z1)) → U3(f27_in(z0, z1), s(z0), s(z1))
U3(f27_out1(z0), s(z1), s(z2)) → f27_out1(z0)
f19_in(s(z0), z1) → U4(f27_in(z0, z1), s(z0), z1)
U4(f27_out1(z0), s(z1), z2) → f19_out1(z0)
f11_in(z0, s(z1)) → U5(f17_in(z0, z1), z0, s(z1))
U5(f17_out1(z0, z1), z2, s(z3)) → f11_out1(z1)
f12_in(s(z0), s(z1)) → U6(f57_in(z0, z1), s(z0), s(z1))
U6(f57_out1, s(z0), s(z1)) → f12_out1(s(z0))
f17_in(z0, z1) → U7(f19_in(z0, z1), z0, z1)
U7(f19_out1(z0), z1, z2) → U8(f1_in(z0, s(z2)), z1, z2, z0)
U8(f1_out1(z0), z1, z2, z3) → f17_out1(z3, z0)
f4_in(z0, z1) → U9(f11_in(z0, z1), f12_in(z0, z1), z0, z1)
U9(f11_out1(z0), z1, z2, z3) → f4_out1(z0)
U9(z0, f12_out1(z1), z2, z3) → f4_out2(z1)

Tuples:

F1_IN(z0, z1) → c(U1'(f4_in(z0, z1), z0, z1), F4_IN(z0, z1))
F57_IN(s(z0), s(z1)) → c4(U2'(f57_in(z0, z1), s(z0), s(z1)), F57_IN(z0, z1))
F27_IN(s(z0), s(z1)) → c7(U3'(f27_in(z0, z1), s(z0), s(z1)), F27_IN(z0, z1))
F19_IN(s(z0), z1) → c9(U4'(f27_in(z0, z1), s(z0), z1), F27_IN(z0, z1))
F11_IN(z0, s(z1)) → c11(U5'(f17_in(z0, z1), z0, s(z1)), F17_IN(z0, z1))
F12_IN(s(z0), s(z1)) → c13(U6'(f57_in(z0, z1), s(z0), s(z1)), F57_IN(z0, z1))
F17_IN(z0, z1) → c15(U7'(f19_in(z0, z1), z0, z1), F19_IN(z0, z1))
U7'(f19_out1(z0), z1, z2) → c16(U8'(f1_in(z0, s(z2)), z1, z2, z0), F1_IN(z0, s(z2)))
F4_IN(z0, z1) → c18(U9'(f11_in(z0, z1), f12_in(z0, z1), z0, z1), F11_IN(z0, z1), F12_IN(z0, z1))

S tuples:

F1_IN(z0, z1) → c(U1'(f4_in(z0, z1), z0, z1), F4_IN(z0, z1))
F57_IN(s(z0), s(z1)) → c4(U2'(f57_in(z0, z1), s(z0), s(z1)), F57_IN(z0, z1))
F27_IN(s(z0), s(z1)) → c7(U3'(f27_in(z0, z1), s(z0), s(z1)), F27_IN(z0, z1))
F19_IN(s(z0), z1) → c9(U4'(f27_in(z0, z1), s(z0), z1), F27_IN(z0, z1))
F11_IN(z0, s(z1)) → c11(U5'(f17_in(z0, z1), z0, s(z1)), F17_IN(z0, z1))
F12_IN(s(z0), s(z1)) → c13(U6'(f57_in(z0, z1), s(z0), s(z1)), F57_IN(z0, z1))
F17_IN(z0, z1) → c15(U7'(f19_in(z0, z1), z0, z1), F19_IN(z0, z1))
U7'(f19_out1(z0), z1, z2) → c16(U8'(f1_in(z0, s(z2)), z1, z2, z0), F1_IN(z0, s(z2)))
F4_IN(z0, z1) → c18(U9'(f11_in(z0, z1), f12_in(z0, z1), z0, z1), F11_IN(z0, z1), F12_IN(z0, z1))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f57_in, U2, f27_in, U3, f19_in, U4, f11_in, U5, f12_in, U6, f17_in, U7, U8, f4_in, U9

Defined Pair Symbols:

F1_IN, F57_IN, F27_IN, F19_IN, F11_IN, F12_IN, F17_IN, U7', F4_IN

Compound Symbols:

c, c4, c7, c9, c11, c13, c15, c16, c18

(5) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f4_in(z0, z1), z0, z1)
U1(f4_out1(z0), z1, z2) → f1_out1(z0)
U1(f4_out2(z0), z1, z2) → f1_out1(z0)
f57_in(z0, 0) → f57_out1
f57_in(s(z0), s(z1)) → U2(f57_in(z0, z1), s(z0), s(z1))
U2(f57_out1, s(z0), s(z1)) → f57_out1
f27_in(z0, 0) → f27_out1(z0)
f27_in(s(z0), s(z1)) → U3(f27_in(z0, z1), s(z0), s(z1))
U3(f27_out1(z0), s(z1), s(z2)) → f27_out1(z0)
f19_in(s(z0), z1) → U4(f27_in(z0, z1), s(z0), z1)
U4(f27_out1(z0), s(z1), z2) → f19_out1(z0)
f11_in(z0, s(z1)) → U5(f17_in(z0, z1), z0, s(z1))
U5(f17_out1(z0, z1), z2, s(z3)) → f11_out1(z1)
f12_in(s(z0), s(z1)) → U6(f57_in(z0, z1), s(z0), s(z1))
U6(f57_out1, s(z0), s(z1)) → f12_out1(s(z0))
f17_in(z0, z1) → U7(f19_in(z0, z1), z0, z1)
U7(f19_out1(z0), z1, z2) → U8(f1_in(z0, s(z2)), z1, z2, z0)
U8(f1_out1(z0), z1, z2, z3) → f17_out1(z3, z0)
f4_in(z0, z1) → U9(f11_in(z0, z1), f12_in(z0, z1), z0, z1)
U9(f11_out1(z0), z1, z2, z3) → f4_out1(z0)
U9(z0, f12_out1(z1), z2, z3) → f4_out2(z1)

Tuples:

F1_IN(z0, z1) → c(U1'(f4_in(z0, z1), z0, z1), F4_IN(z0, z1))
F57_IN(s(z0), s(z1)) → c4(U2'(f57_in(z0, z1), s(z0), s(z1)), F57_IN(z0, z1))
F27_IN(s(z0), s(z1)) → c7(U3'(f27_in(z0, z1), s(z0), s(z1)), F27_IN(z0, z1))
F11_IN(z0, s(z1)) → c11(U5'(f17_in(z0, z1), z0, s(z1)), F17_IN(z0, z1))
F17_IN(z0, z1) → c15(U7'(f19_in(z0, z1), z0, z1), F19_IN(z0, z1))
U7'(f19_out1(z0), z1, z2) → c16(U8'(f1_in(z0, s(z2)), z1, z2, z0), F1_IN(z0, s(z2)))
F4_IN(z0, z1) → c18(U9'(f11_in(z0, z1), f12_in(z0, z1), z0, z1), F11_IN(z0, z1), F12_IN(z0, z1))
F19_IN(s(z0), z1) → c1(U4'(f27_in(z0, z1), s(z0), z1))
F19_IN(s(z0), z1) → c1(F27_IN(z0, z1))
F12_IN(s(z0), s(z1)) → c1(U6'(f57_in(z0, z1), s(z0), s(z1)))
F12_IN(s(z0), s(z1)) → c1(F57_IN(z0, z1))

S tuples:

F1_IN(z0, z1) → c(U1'(f4_in(z0, z1), z0, z1), F4_IN(z0, z1))
F57_IN(s(z0), s(z1)) → c4(U2'(f57_in(z0, z1), s(z0), s(z1)), F57_IN(z0, z1))
F27_IN(s(z0), s(z1)) → c7(U3'(f27_in(z0, z1), s(z0), s(z1)), F27_IN(z0, z1))
F11_IN(z0, s(z1)) → c11(U5'(f17_in(z0, z1), z0, s(z1)), F17_IN(z0, z1))
F17_IN(z0, z1) → c15(U7'(f19_in(z0, z1), z0, z1), F19_IN(z0, z1))
U7'(f19_out1(z0), z1, z2) → c16(U8'(f1_in(z0, s(z2)), z1, z2, z0), F1_IN(z0, s(z2)))
F4_IN(z0, z1) → c18(U9'(f11_in(z0, z1), f12_in(z0, z1), z0, z1), F11_IN(z0, z1), F12_IN(z0, z1))
F19_IN(s(z0), z1) → c1(U4'(f27_in(z0, z1), s(z0), z1))
F19_IN(s(z0), z1) → c1(F27_IN(z0, z1))
F12_IN(s(z0), s(z1)) → c1(U6'(f57_in(z0, z1), s(z0), s(z1)))
F12_IN(s(z0), s(z1)) → c1(F57_IN(z0, z1))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f57_in, U2, f27_in, U3, f19_in, U4, f11_in, U5, f12_in, U6, f17_in, U7, U8, f4_in, U9

Defined Pair Symbols:

F1_IN, F57_IN, F27_IN, F11_IN, F17_IN, U7', F4_IN, F19_IN, F12_IN

Compound Symbols:

c, c4, c7, c11, c15, c16, c18, c1

(7) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)

Removed 8 trailing tuple parts

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f4_in(z0, z1), z0, z1)
U1(f4_out1(z0), z1, z2) → f1_out1(z0)
U1(f4_out2(z0), z1, z2) → f1_out1(z0)
f57_in(z0, 0) → f57_out1
f57_in(s(z0), s(z1)) → U2(f57_in(z0, z1), s(z0), s(z1))
U2(f57_out1, s(z0), s(z1)) → f57_out1
f27_in(z0, 0) → f27_out1(z0)
f27_in(s(z0), s(z1)) → U3(f27_in(z0, z1), s(z0), s(z1))
U3(f27_out1(z0), s(z1), s(z2)) → f27_out1(z0)
f19_in(s(z0), z1) → U4(f27_in(z0, z1), s(z0), z1)
U4(f27_out1(z0), s(z1), z2) → f19_out1(z0)
f11_in(z0, s(z1)) → U5(f17_in(z0, z1), z0, s(z1))
U5(f17_out1(z0, z1), z2, s(z3)) → f11_out1(z1)
f12_in(s(z0), s(z1)) → U6(f57_in(z0, z1), s(z0), s(z1))
U6(f57_out1, s(z0), s(z1)) → f12_out1(s(z0))
f17_in(z0, z1) → U7(f19_in(z0, z1), z0, z1)
U7(f19_out1(z0), z1, z2) → U8(f1_in(z0, s(z2)), z1, z2, z0)
U8(f1_out1(z0), z1, z2, z3) → f17_out1(z3, z0)
f4_in(z0, z1) → U9(f11_in(z0, z1), f12_in(z0, z1), z0, z1)
U9(f11_out1(z0), z1, z2, z3) → f4_out1(z0)
U9(z0, f12_out1(z1), z2, z3) → f4_out2(z1)

Tuples:

F17_IN(z0, z1) → c15(U7'(f19_in(z0, z1), z0, z1), F19_IN(z0, z1))
F19_IN(s(z0), z1) → c1(F27_IN(z0, z1))
F12_IN(s(z0), s(z1)) → c1(F57_IN(z0, z1))
F1_IN(z0, z1) → c(F4_IN(z0, z1))
F57_IN(s(z0), s(z1)) → c4(F57_IN(z0, z1))
F27_IN(s(z0), s(z1)) → c7(F27_IN(z0, z1))
F11_IN(z0, s(z1)) → c11(F17_IN(z0, z1))
U7'(f19_out1(z0), z1, z2) → c16(F1_IN(z0, s(z2)))
F4_IN(z0, z1) → c18(F11_IN(z0, z1), F12_IN(z0, z1))
F19_IN(s(z0), z1) → c1
F12_IN(s(z0), s(z1)) → c1

S tuples:

F17_IN(z0, z1) → c15(U7'(f19_in(z0, z1), z0, z1), F19_IN(z0, z1))
F19_IN(s(z0), z1) → c1(F27_IN(z0, z1))
F12_IN(s(z0), s(z1)) → c1(F57_IN(z0, z1))
F1_IN(z0, z1) → c(F4_IN(z0, z1))
F57_IN(s(z0), s(z1)) → c4(F57_IN(z0, z1))
F27_IN(s(z0), s(z1)) → c7(F27_IN(z0, z1))
F11_IN(z0, s(z1)) → c11(F17_IN(z0, z1))
U7'(f19_out1(z0), z1, z2) → c16(F1_IN(z0, s(z2)))
F4_IN(z0, z1) → c18(F11_IN(z0, z1), F12_IN(z0, z1))
F19_IN(s(z0), z1) → c1
F12_IN(s(z0), s(z1)) → c1

K tuples:none
Defined Rule Symbols:

f1_in, U1, f57_in, U2, f27_in, U3, f19_in, U4, f11_in, U5, f12_in, U6, f17_in, U7, U8, f4_in, U9

Defined Pair Symbols:

F17_IN, F19_IN, F12_IN, F1_IN, F57_IN, F27_IN, F11_IN, U7', F4_IN

Compound Symbols:

c15, c1, c, c4, c7, c11, c16, c18, c1

(9) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F27_IN(s(z0), s(z1)) → c7(F27_IN(z0, z1))
U7'(f19_out1(z0), z1, z2) → c16(F1_IN(z0, s(z2)))
F19_IN(s(z0), z1) → c1

We considered the (Usable) Rules:

f19_in(s(z0), z1) → U4(f27_in(z0, z1), s(z0), z1)
f27_in(z0, 0) → f27_out1(z0)
f27_in(s(z0), s(z1)) → U3(f27_in(z0, z1), s(z0), s(z1))
U4(f27_out1(z0), s(z1), z2) → f19_out1(z0)
U3(f27_out1(z0), s(z1), s(z2)) → f27_out1(z0)

And the Tuples:

F17_IN(z0, z1) → c15(U7'(f19_in(z0, z1), z0, z1), F19_IN(z0, z1))
F19_IN(s(z0), z1) → c1(F27_IN(z0, z1))
F12_IN(s(z0), s(z1)) → c1(F57_IN(z0, z1))
F1_IN(z0, z1) → c(F4_IN(z0, z1))
F57_IN(s(z0), s(z1)) → c4(F57_IN(z0, z1))
F27_IN(s(z0), s(z1)) → c7(F27_IN(z0, z1))
F11_IN(z0, s(z1)) → c11(F17_IN(z0, z1))
U7'(f19_out1(z0), z1, z2) → c16(F1_IN(z0, s(z2)))
F4_IN(z0, z1) → c18(F11_IN(z0, z1), F12_IN(z0, z1))
F19_IN(s(z0), z1) → c1
F12_IN(s(z0), s(z1)) → c1

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0
POL(F11_IN(x₁, x₂)) = x₁·x₂ + x₁²
POL(F12_IN(x₁, x₂)) = 0
POL(F17_IN(x₁, x₂)) = x₁ + x₁·x₂ + x₁²
POL(F19_IN(x₁, x₂)) = x₁
POL(F1_IN(x₁, x₂)) = x₁·x₂ + x₁²
POL(F27_IN(x₁, x₂)) = [1] + x₁
POL(F4_IN(x₁, x₂)) = x₁·x₂ + x₁²
POL(F57_IN(x₁, x₂)) = 0
POL(U3(x₁, x₂, x₃)) = x₁
POL(U4(x₁, x₂, x₃)) = x₁
POL(U7'(x₁, x₂, x₃)) = x₁·x₃ + x₁²
POL(c(x₁)) = x₁
POL(c1) = 0
POL(c1(x₁)) = x₁
POL(c11(x₁)) = x₁
POL(c15(x₁, x₂)) = x₁ + x₂
POL(c16(x₁)) = x₁
POL(c18(x₁, x₂)) = x₁ + x₂
POL(c4(x₁)) = x₁
POL(c7(x₁)) = x₁
POL(f19_in(x₁, x₂)) = x₁
POL(f19_out1(x₁)) = [1] + x₁
POL(f27_in(x₁, x₂)) = [1] + x₁
POL(f27_out1(x₁)) = [1] + x₁
POL(s(x₁)) = [1] + x₁

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f4_in(z0, z1), z0, z1)
U1(f4_out1(z0), z1, z2) → f1_out1(z0)
U1(f4_out2(z0), z1, z2) → f1_out1(z0)
f57_in(z0, 0) → f57_out1
f57_in(s(z0), s(z1)) → U2(f57_in(z0, z1), s(z0), s(z1))
U2(f57_out1, s(z0), s(z1)) → f57_out1
f27_in(z0, 0) → f27_out1(z0)
f27_in(s(z0), s(z1)) → U3(f27_in(z0, z1), s(z0), s(z1))
U3(f27_out1(z0), s(z1), s(z2)) → f27_out1(z0)
f19_in(s(z0), z1) → U4(f27_in(z0, z1), s(z0), z1)
U4(f27_out1(z0), s(z1), z2) → f19_out1(z0)
f11_in(z0, s(z1)) → U5(f17_in(z0, z1), z0, s(z1))
U5(f17_out1(z0, z1), z2, s(z3)) → f11_out1(z1)
f12_in(s(z0), s(z1)) → U6(f57_in(z0, z1), s(z0), s(z1))
U6(f57_out1, s(z0), s(z1)) → f12_out1(s(z0))
f17_in(z0, z1) → U7(f19_in(z0, z1), z0, z1)
U7(f19_out1(z0), z1, z2) → U8(f1_in(z0, s(z2)), z1, z2, z0)
U8(f1_out1(z0), z1, z2, z3) → f17_out1(z3, z0)
f4_in(z0, z1) → U9(f11_in(z0, z1), f12_in(z0, z1), z0, z1)
U9(f11_out1(z0), z1, z2, z3) → f4_out1(z0)
U9(z0, f12_out1(z1), z2, z3) → f4_out2(z1)

Tuples:

F17_IN(z0, z1) → c15(U7'(f19_in(z0, z1), z0, z1), F19_IN(z0, z1))
F19_IN(s(z0), z1) → c1(F27_IN(z0, z1))
F12_IN(s(z0), s(z1)) → c1(F57_IN(z0, z1))
F1_IN(z0, z1) → c(F4_IN(z0, z1))
F57_IN(s(z0), s(z1)) → c4(F57_IN(z0, z1))
F27_IN(s(z0), s(z1)) → c7(F27_IN(z0, z1))
F11_IN(z0, s(z1)) → c11(F17_IN(z0, z1))
U7'(f19_out1(z0), z1, z2) → c16(F1_IN(z0, s(z2)))
F4_IN(z0, z1) → c18(F11_IN(z0, z1), F12_IN(z0, z1))
F19_IN(s(z0), z1) → c1
F12_IN(s(z0), s(z1)) → c1

S tuples:

F17_IN(z0, z1) → c15(U7'(f19_in(z0, z1), z0, z1), F19_IN(z0, z1))
F19_IN(s(z0), z1) → c1(F27_IN(z0, z1))
F12_IN(s(z0), s(z1)) → c1(F57_IN(z0, z1))
F1_IN(z0, z1) → c(F4_IN(z0, z1))
F57_IN(s(z0), s(z1)) → c4(F57_IN(z0, z1))
F11_IN(z0, s(z1)) → c11(F17_IN(z0, z1))
F4_IN(z0, z1) → c18(F11_IN(z0, z1), F12_IN(z0, z1))
F12_IN(s(z0), s(z1)) → c1

K tuples:

F27_IN(s(z0), s(z1)) → c7(F27_IN(z0, z1))
U7'(f19_out1(z0), z1, z2) → c16(F1_IN(z0, s(z2)))
F19_IN(s(z0), z1) → c1

Defined Rule Symbols:

f1_in, U1, f57_in, U2, f27_in, U3, f19_in, U4, f11_in, U5, f12_in, U6, f17_in, U7, U8, f4_in, U9

Defined Pair Symbols:

F17_IN, F19_IN, F12_IN, F1_IN, F57_IN, F27_IN, F11_IN, U7', F4_IN

Compound Symbols:

c15, c1, c, c4, c7, c11, c16, c18, c1

(11) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

F1_IN(z0, z1) → c(F4_IN(z0, z1))
F4_IN(z0, z1) → c18(F11_IN(z0, z1), F12_IN(z0, z1))
F12_IN(s(z0), s(z1)) → c1
F4_IN(z0, z1) → c18(F11_IN(z0, z1), F12_IN(z0, z1))
F12_IN(s(z0), s(z1)) → c1(F57_IN(z0, z1))
F11_IN(z0, s(z1)) → c11(F17_IN(z0, z1))
F12_IN(s(z0), s(z1)) → c1
F17_IN(z0, z1) → c15(U7'(f19_in(z0, z1), z0, z1), F19_IN(z0, z1))
F19_IN(s(z0), z1) → c1(F27_IN(z0, z1))
U7'(f19_out1(z0), z1, z2) → c16(F1_IN(z0, s(z2)))
F19_IN(s(z0), z1) → c1
F27_IN(s(z0), s(z1)) → c7(F27_IN(z0, z1))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f4_in(z0, z1), z0, z1)
U1(f4_out1(z0), z1, z2) → f1_out1(z0)
U1(f4_out2(z0), z1, z2) → f1_out1(z0)
f57_in(z0, 0) → f57_out1
f57_in(s(z0), s(z1)) → U2(f57_in(z0, z1), s(z0), s(z1))
U2(f57_out1, s(z0), s(z1)) → f57_out1
f27_in(z0, 0) → f27_out1(z0)
f27_in(s(z0), s(z1)) → U3(f27_in(z0, z1), s(z0), s(z1))
U3(f27_out1(z0), s(z1), s(z2)) → f27_out1(z0)
f19_in(s(z0), z1) → U4(f27_in(z0, z1), s(z0), z1)
U4(f27_out1(z0), s(z1), z2) → f19_out1(z0)
f11_in(z0, s(z1)) → U5(f17_in(z0, z1), z0, s(z1))
U5(f17_out1(z0, z1), z2, s(z3)) → f11_out1(z1)
f12_in(s(z0), s(z1)) → U6(f57_in(z0, z1), s(z0), s(z1))
U6(f57_out1, s(z0), s(z1)) → f12_out1(s(z0))
f17_in(z0, z1) → U7(f19_in(z0, z1), z0, z1)
U7(f19_out1(z0), z1, z2) → U8(f1_in(z0, s(z2)), z1, z2, z0)
U8(f1_out1(z0), z1, z2, z3) → f17_out1(z3, z0)
f4_in(z0, z1) → U9(f11_in(z0, z1), f12_in(z0, z1), z0, z1)
U9(f11_out1(z0), z1, z2, z3) → f4_out1(z0)
U9(z0, f12_out1(z1), z2, z3) → f4_out2(z1)

Tuples:

F17_IN(z0, z1) → c15(U7'(f19_in(z0, z1), z0, z1), F19_IN(z0, z1))
F19_IN(s(z0), z1) → c1(F27_IN(z0, z1))
F12_IN(s(z0), s(z1)) → c1(F57_IN(z0, z1))
F1_IN(z0, z1) → c(F4_IN(z0, z1))
F57_IN(s(z0), s(z1)) → c4(F57_IN(z0, z1))
F27_IN(s(z0), s(z1)) → c7(F27_IN(z0, z1))
F11_IN(z0, s(z1)) → c11(F17_IN(z0, z1))
U7'(f19_out1(z0), z1, z2) → c16(F1_IN(z0, s(z2)))
F4_IN(z0, z1) → c18(F11_IN(z0, z1), F12_IN(z0, z1))
F19_IN(s(z0), z1) → c1
F12_IN(s(z0), s(z1)) → c1

S tuples:

F57_IN(s(z0), s(z1)) → c4(F57_IN(z0, z1))

K tuples:

F27_IN(s(z0), s(z1)) → c7(F27_IN(z0, z1))
U7'(f19_out1(z0), z1, z2) → c16(F1_IN(z0, s(z2)))
F19_IN(s(z0), z1) → c1
F1_IN(z0, z1) → c(F4_IN(z0, z1))
F4_IN(z0, z1) → c18(F11_IN(z0, z1), F12_IN(z0, z1))
F12_IN(s(z0), s(z1)) → c1
F12_IN(s(z0), s(z1)) → c1(F57_IN(z0, z1))
F11_IN(z0, s(z1)) → c11(F17_IN(z0, z1))
F17_IN(z0, z1) → c15(U7'(f19_in(z0, z1), z0, z1), F19_IN(z0, z1))
F19_IN(s(z0), z1) → c1(F27_IN(z0, z1))

Defined Rule Symbols:

f1_in, U1, f57_in, U2, f27_in, U3, f19_in, U4, f11_in, U5, f12_in, U6, f17_in, U7, U8, f4_in, U9

Defined Pair Symbols:

F17_IN, F19_IN, F12_IN, F1_IN, F57_IN, F27_IN, F11_IN, U7', F4_IN

Compound Symbols:

c15, c1, c, c4, c7, c11, c16, c18, c1

(13) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace F17_IN(z0, z1) → c15(U7'(f19_in(z0, z1), z0, z1), F19_IN(z0, z1)) by

F17_IN(s(z0), z1) → c15(U7'(U4(f27_in(z0, z1), s(z0), z1), s(z0), z1), F19_IN(s(z0), z1))

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f4_in(z0, z1), z0, z1)
U1(f4_out1(z0), z1, z2) → f1_out1(z0)
U1(f4_out2(z0), z1, z2) → f1_out1(z0)
f57_in(z0, 0) → f57_out1
f57_in(s(z0), s(z1)) → U2(f57_in(z0, z1), s(z0), s(z1))
U2(f57_out1, s(z0), s(z1)) → f57_out1
f27_in(z0, 0) → f27_out1(z0)
f27_in(s(z0), s(z1)) → U3(f27_in(z0, z1), s(z0), s(z1))
U3(f27_out1(z0), s(z1), s(z2)) → f27_out1(z0)
f19_in(s(z0), z1) → U4(f27_in(z0, z1), s(z0), z1)
U4(f27_out1(z0), s(z1), z2) → f19_out1(z0)
f11_in(z0, s(z1)) → U5(f17_in(z0, z1), z0, s(z1))
U5(f17_out1(z0, z1), z2, s(z3)) → f11_out1(z1)
f12_in(s(z0), s(z1)) → U6(f57_in(z0, z1), s(z0), s(z1))
U6(f57_out1, s(z0), s(z1)) → f12_out1(s(z0))
f17_in(z0, z1) → U7(f19_in(z0, z1), z0, z1)
U7(f19_out1(z0), z1, z2) → U8(f1_in(z0, s(z2)), z1, z2, z0)
U8(f1_out1(z0), z1, z2, z3) → f17_out1(z3, z0)
f4_in(z0, z1) → U9(f11_in(z0, z1), f12_in(z0, z1), z0, z1)
U9(f11_out1(z0), z1, z2, z3) → f4_out1(z0)
U9(z0, f12_out1(z1), z2, z3) → f4_out2(z1)

Tuples:

F19_IN(s(z0), z1) → c1(F27_IN(z0, z1))
F12_IN(s(z0), s(z1)) → c1(F57_IN(z0, z1))
F1_IN(z0, z1) → c(F4_IN(z0, z1))
F57_IN(s(z0), s(z1)) → c4(F57_IN(z0, z1))
F27_IN(s(z0), s(z1)) → c7(F27_IN(z0, z1))
F11_IN(z0, s(z1)) → c11(F17_IN(z0, z1))
U7'(f19_out1(z0), z1, z2) → c16(F1_IN(z0, s(z2)))
F4_IN(z0, z1) → c18(F11_IN(z0, z1), F12_IN(z0, z1))
F19_IN(s(z0), z1) → c1
F12_IN(s(z0), s(z1)) → c1
F17_IN(s(z0), z1) → c15(U7'(U4(f27_in(z0, z1), s(z0), z1), s(z0), z1), F19_IN(s(z0), z1))

S tuples:

F57_IN(s(z0), s(z1)) → c4(F57_IN(z0, z1))

K tuples:

F27_IN(s(z0), s(z1)) → c7(F27_IN(z0, z1))
U7'(f19_out1(z0), z1, z2) → c16(F1_IN(z0, s(z2)))
F19_IN(s(z0), z1) → c1
F1_IN(z0, z1) → c(F4_IN(z0, z1))
F4_IN(z0, z1) → c18(F11_IN(z0, z1), F12_IN(z0, z1))
F12_IN(s(z0), s(z1)) → c1
F12_IN(s(z0), s(z1)) → c1(F57_IN(z0, z1))
F11_IN(z0, s(z1)) → c11(F17_IN(z0, z1))
F17_IN(z0, z1) → c15(U7'(f19_in(z0, z1), z0, z1), F19_IN(z0, z1))
F19_IN(s(z0), z1) → c1(F27_IN(z0, z1))

Defined Rule Symbols:

f1_in, U1, f57_in, U2, f27_in, U3, f19_in, U4, f11_in, U5, f12_in, U6, f17_in, U7, U8, f4_in, U9

Defined Pair Symbols:

F19_IN, F12_IN, F1_IN, F57_IN, F27_IN, F11_IN, U7', F4_IN, F17_IN

Compound Symbols:

c1, c, c4, c7, c11, c16, c18, c1, c15

(15) CdtGraphRemoveDanglingProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 of 11 dangling nodes:

F12_IN(s(z0), s(z1)) → c1

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f4_in(z0, z1), z0, z1)
U1(f4_out1(z0), z1, z2) → f1_out1(z0)
U1(f4_out2(z0), z1, z2) → f1_out1(z0)
f57_in(z0, 0) → f57_out1
f57_in(s(z0), s(z1)) → U2(f57_in(z0, z1), s(z0), s(z1))
U2(f57_out1, s(z0), s(z1)) → f57_out1
f27_in(z0, 0) → f27_out1(z0)
f27_in(s(z0), s(z1)) → U3(f27_in(z0, z1), s(z0), s(z1))
U3(f27_out1(z0), s(z1), s(z2)) → f27_out1(z0)
f19_in(s(z0), z1) → U4(f27_in(z0, z1), s(z0), z1)
U4(f27_out1(z0), s(z1), z2) → f19_out1(z0)
f11_in(z0, s(z1)) → U5(f17_in(z0, z1), z0, s(z1))
U5(f17_out1(z0, z1), z2, s(z3)) → f11_out1(z1)
f12_in(s(z0), s(z1)) → U6(f57_in(z0, z1), s(z0), s(z1))
U6(f57_out1, s(z0), s(z1)) → f12_out1(s(z0))
f17_in(z0, z1) → U7(f19_in(z0, z1), z0, z1)
U7(f19_out1(z0), z1, z2) → U8(f1_in(z0, s(z2)), z1, z2, z0)
U8(f1_out1(z0), z1, z2, z3) → f17_out1(z3, z0)
f4_in(z0, z1) → U9(f11_in(z0, z1), f12_in(z0, z1), z0, z1)
U9(f11_out1(z0), z1, z2, z3) → f4_out1(z0)
U9(z0, f12_out1(z1), z2, z3) → f4_out2(z1)

Tuples:

F19_IN(s(z0), z1) → c1(F27_IN(z0, z1))
F12_IN(s(z0), s(z1)) → c1(F57_IN(z0, z1))
F1_IN(z0, z1) → c(F4_IN(z0, z1))
F57_IN(s(z0), s(z1)) → c4(F57_IN(z0, z1))
F27_IN(s(z0), s(z1)) → c7(F27_IN(z0, z1))
F11_IN(z0, s(z1)) → c11(F17_IN(z0, z1))
U7'(f19_out1(z0), z1, z2) → c16(F1_IN(z0, s(z2)))
F4_IN(z0, z1) → c18(F11_IN(z0, z1), F12_IN(z0, z1))
F19_IN(s(z0), z1) → c1
F17_IN(s(z0), z1) → c15(U7'(U4(f27_in(z0, z1), s(z0), z1), s(z0), z1), F19_IN(s(z0), z1))

S tuples:

F57_IN(s(z0), s(z1)) → c4(F57_IN(z0, z1))

K tuples:

F27_IN(s(z0), s(z1)) → c7(F27_IN(z0, z1))
U7'(f19_out1(z0), z1, z2) → c16(F1_IN(z0, s(z2)))
F19_IN(s(z0), z1) → c1
F1_IN(z0, z1) → c(F4_IN(z0, z1))
F4_IN(z0, z1) → c18(F11_IN(z0, z1), F12_IN(z0, z1))
F12_IN(s(z0), s(z1)) → c1(F57_IN(z0, z1))
F11_IN(z0, s(z1)) → c11(F17_IN(z0, z1))
F19_IN(s(z0), z1) → c1(F27_IN(z0, z1))

Defined Rule Symbols:

f1_in, U1, f57_in, U2, f27_in, U3, f19_in, U4, f11_in, U5, f12_in, U6, f17_in, U7, U8, f4_in, U9

Defined Pair Symbols:

F19_IN, F12_IN, F1_IN, F57_IN, F27_IN, F11_IN, U7', F4_IN, F17_IN

Compound Symbols:

c1, c, c4, c7, c11, c16, c18, c1, c15

(17) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f4_in(z0, z1), z0, z1)
U1(f4_out1(z0), z1, z2) → f1_out1(z0)
U1(f4_out2(z0), z1, z2) → f1_out1(z0)
f57_in(z0, 0) → f57_out1
f57_in(s(z0), s(z1)) → U2(f57_in(z0, z1), s(z0), s(z1))
U2(f57_out1, s(z0), s(z1)) → f57_out1
f27_in(z0, 0) → f27_out1(z0)
f27_in(s(z0), s(z1)) → U3(f27_in(z0, z1), s(z0), s(z1))
U3(f27_out1(z0), s(z1), s(z2)) → f27_out1(z0)
f19_in(s(z0), z1) → U4(f27_in(z0, z1), s(z0), z1)
U4(f27_out1(z0), s(z1), z2) → f19_out1(z0)
f11_in(z0, s(z1)) → U5(f17_in(z0, z1), z0, s(z1))
U5(f17_out1(z0, z1), z2, s(z3)) → f11_out1(z1)
f12_in(s(z0), s(z1)) → U6(f57_in(z0, z1), s(z0), s(z1))
U6(f57_out1, s(z0), s(z1)) → f12_out1(s(z0))
f17_in(z0, z1) → U7(f19_in(z0, z1), z0, z1)
U7(f19_out1(z0), z1, z2) → U8(f1_in(z0, s(z2)), z1, z2, z0)
U8(f1_out1(z0), z1, z2, z3) → f17_out1(z3, z0)
f4_in(z0, z1) → U9(f11_in(z0, z1), f12_in(z0, z1), z0, z1)
U9(f11_out1(z0), z1, z2, z3) → f4_out1(z0)
U9(z0, f12_out1(z1), z2, z3) → f4_out2(z1)

Tuples:

F19_IN(s(z0), z1) → c1(F27_IN(z0, z1))
F12_IN(s(z0), s(z1)) → c1(F57_IN(z0, z1))
F1_IN(z0, z1) → c(F4_IN(z0, z1))
F57_IN(s(z0), s(z1)) → c4(F57_IN(z0, z1))
F27_IN(s(z0), s(z1)) → c7(F27_IN(z0, z1))
F11_IN(z0, s(z1)) → c11(F17_IN(z0, z1))
U7'(f19_out1(z0), z1, z2) → c16(F1_IN(z0, s(z2)))
F4_IN(z0, z1) → c18(F11_IN(z0, z1), F12_IN(z0, z1))
F17_IN(s(z0), z1) → c15(U7'(U4(f27_in(z0, z1), s(z0), z1), s(z0), z1), F19_IN(s(z0), z1))

S tuples:

F57_IN(s(z0), s(z1)) → c4(F57_IN(z0, z1))

K tuples:

F27_IN(s(z0), s(z1)) → c7(F27_IN(z0, z1))
U7'(f19_out1(z0), z1, z2) → c16(F1_IN(z0, s(z2)))
F1_IN(z0, z1) → c(F4_IN(z0, z1))
F4_IN(z0, z1) → c18(F11_IN(z0, z1), F12_IN(z0, z1))
F12_IN(s(z0), s(z1)) → c1(F57_IN(z0, z1))
F11_IN(z0, s(z1)) → c11(F17_IN(z0, z1))
F19_IN(s(z0), z1) → c1(F27_IN(z0, z1))

Defined Rule Symbols:

f1_in, U1, f57_in, U2, f27_in, U3, f19_in, U4, f11_in, U5, f12_in, U6, f17_in, U7, U8, f4_in, U9

Defined Pair Symbols:

F19_IN, F12_IN, F1_IN, F57_IN, F27_IN, F11_IN, U7', F4_IN, F17_IN

Compound Symbols:

c1, c, c4, c7, c11, c16, c18, c15

(19) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F57_IN(s(z0), s(z1)) → c4(F57_IN(z0, z1))

We considered the (Usable) Rules:

f27_in(z0, 0) → f27_out1(z0)
f27_in(s(z0), s(z1)) → U3(f27_in(z0, z1), s(z0), s(z1))
U4(f27_out1(z0), s(z1), z2) → f19_out1(z0)
U3(f27_out1(z0), s(z1), s(z2)) → f27_out1(z0)

And the Tuples:

F19_IN(s(z0), z1) → c1(F27_IN(z0, z1))
F12_IN(s(z0), s(z1)) → c1(F57_IN(z0, z1))
F1_IN(z0, z1) → c(F4_IN(z0, z1))
F57_IN(s(z0), s(z1)) → c4(F57_IN(z0, z1))
F27_IN(s(z0), s(z1)) → c7(F27_IN(z0, z1))
F11_IN(z0, s(z1)) → c11(F17_IN(z0, z1))
U7'(f19_out1(z0), z1, z2) → c16(F1_IN(z0, s(z2)))
F4_IN(z0, z1) → c18(F11_IN(z0, z1), F12_IN(z0, z1))
F17_IN(s(z0), z1) → c15(U7'(U4(f27_in(z0, z1), s(z0), z1), s(z0), z1), F19_IN(s(z0), z1))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0
POL(F11_IN(x₁, x₂)) = x₁²
POL(F12_IN(x₁, x₂)) = x₁
POL(F17_IN(x₁, x₂)) = x₁²
POL(F19_IN(x₁, x₂)) = 0
POL(F1_IN(x₁, x₂)) = [1] + x₁ + x₁²
POL(F27_IN(x₁, x₂)) = 0
POL(F4_IN(x₁, x₂)) = [1] + x₁ + x₁²
POL(F57_IN(x₁, x₂)) = [1] + x₁
POL(U3(x₁, x₂, x₃)) = x₁
POL(U4(x₁, x₂, x₃)) = [1] + x₁
POL(U7'(x₁, x₂, x₃)) = x₁²
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c11(x₁)) = x₁
POL(c15(x₁, x₂)) = x₁ + x₂
POL(c16(x₁)) = x₁
POL(c18(x₁, x₂)) = x₁ + x₂
POL(c4(x₁)) = x₁
POL(c7(x₁)) = x₁
POL(f19_out1(x₁)) = [1] + x₁
POL(f27_in(x₁, x₂)) = x₁
POL(f27_out1(x₁)) = x₁
POL(s(x₁)) = [1] + x₁

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f4_in(z0, z1), z0, z1)
U1(f4_out1(z0), z1, z2) → f1_out1(z0)
U1(f4_out2(z0), z1, z2) → f1_out1(z0)
f57_in(z0, 0) → f57_out1
f57_in(s(z0), s(z1)) → U2(f57_in(z0, z1), s(z0), s(z1))
U2(f57_out1, s(z0), s(z1)) → f57_out1
f27_in(z0, 0) → f27_out1(z0)
f27_in(s(z0), s(z1)) → U3(f27_in(z0, z1), s(z0), s(z1))
U3(f27_out1(z0), s(z1), s(z2)) → f27_out1(z0)
f19_in(s(z0), z1) → U4(f27_in(z0, z1), s(z0), z1)
U4(f27_out1(z0), s(z1), z2) → f19_out1(z0)
f11_in(z0, s(z1)) → U5(f17_in(z0, z1), z0, s(z1))
U5(f17_out1(z0, z1), z2, s(z3)) → f11_out1(z1)
f12_in(s(z0), s(z1)) → U6(f57_in(z0, z1), s(z0), s(z1))
U6(f57_out1, s(z0), s(z1)) → f12_out1(s(z0))
f17_in(z0, z1) → U7(f19_in(z0, z1), z0, z1)
U7(f19_out1(z0), z1, z2) → U8(f1_in(z0, s(z2)), z1, z2, z0)
U8(f1_out1(z0), z1, z2, z3) → f17_out1(z3, z0)
f4_in(z0, z1) → U9(f11_in(z0, z1), f12_in(z0, z1), z0, z1)
U9(f11_out1(z0), z1, z2, z3) → f4_out1(z0)
U9(z0, f12_out1(z1), z2, z3) → f4_out2(z1)

Tuples:

F19_IN(s(z0), z1) → c1(F27_IN(z0, z1))
F12_IN(s(z0), s(z1)) → c1(F57_IN(z0, z1))
F1_IN(z0, z1) → c(F4_IN(z0, z1))
F57_IN(s(z0), s(z1)) → c4(F57_IN(z0, z1))
F27_IN(s(z0), s(z1)) → c7(F27_IN(z0, z1))
F11_IN(z0, s(z1)) → c11(F17_IN(z0, z1))
U7'(f19_out1(z0), z1, z2) → c16(F1_IN(z0, s(z2)))
F4_IN(z0, z1) → c18(F11_IN(z0, z1), F12_IN(z0, z1))
F17_IN(s(z0), z1) → c15(U7'(U4(f27_in(z0, z1), s(z0), z1), s(z0), z1), F19_IN(s(z0), z1))

S tuples:none
K tuples:

F27_IN(s(z0), s(z1)) → c7(F27_IN(z0, z1))
U7'(f19_out1(z0), z1, z2) → c16(F1_IN(z0, s(z2)))
F1_IN(z0, z1) → c(F4_IN(z0, z1))
F4_IN(z0, z1) → c18(F11_IN(z0, z1), F12_IN(z0, z1))
F12_IN(s(z0), s(z1)) → c1(F57_IN(z0, z1))
F11_IN(z0, s(z1)) → c11(F17_IN(z0, z1))
F19_IN(s(z0), z1) → c1(F27_IN(z0, z1))
F57_IN(s(z0), s(z1)) → c4(F57_IN(z0, z1))

Defined Rule Symbols:

f1_in, U1, f57_in, U2, f27_in, U3, f19_in, U4, f11_in, U5, f12_in, U6, f17_in, U7, U8, f4_in, U9

Defined Pair Symbols:

F19_IN, F12_IN, F1_IN, F57_IN, F27_IN, F11_IN, U7', F4_IN, F17_IN

Compound Symbols:

c1, c, c4, c7, c11, c16, c18, c15

(21) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(22) BOUNDS(O(1), O(1))

(23) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)

Built complexity over-approximating cdt problems from derivation graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="2: rem(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
3 [label="3: rem(T1, T2, T3), SCOPE: 1, CLAUSE: 3 | rem(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: ','(notZero(T8), ','(sub(T7, T8, X7), rem(X7, T8, T10))) | rem(T7, T8, T3), SCOPE: 1, CLAUSE: 4\n\nT7 is ground\nT8 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: ','(notZero(T8), ','(sub(T7, T8, X7), rem(X7, T8, T10))), SCOPE: 2, CLAUSE: 1 | ?_2 | rem(T7, T8, T3), SCOPE: 1, CLAUSE: 4\n\nT7 is ground\nT8 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: ','(sub(T7, s(T13), X7), rem(X7, s(T13), T10)) | ?_2 | rem(T7, s(T13), T3), SCOPE: 1, CLAUSE: 4\n\nT7 is ground\nT13 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: ?_2 | rem(T7, T8, T3), SCOPE: 1, CLAUSE: 4\n\nT7 is ground\nT8 is ground\nX10 is free\nnotZero(T8) !=? notZero(s(X10))", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: ','(sub(T7, s(T13), X7), rem(X7, s(T13), T10))\n\nT7 is ground\nT13 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ?_2 | rem(T7, s(T13), T3), SCOPE: 1, CLAUSE: 4\n\nT7 is ground\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: sub(T7, s(T13), X7)\n\nT7 is ground\nT13 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: rem(T18, s(T13), T10)\n\nT13 is ground\nT18 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: sub(T7, s(T13), X7), SCOPE: 3, CLAUSE: 0 | sub(T7, s(T13), X7), SCOPE: 3, CLAUSE: 5\n\nT7 is ground\nT13 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: sub(T7, s(T13), X7), SCOPE: 3, CLAUSE: 5\n\nT7 is ground\nT13 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: sub(T26, T27, X29)\n\nT26 is ground\nT27 is ground\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: sub(T26, T27, X29), SCOPE: 4, CLAUSE: 0 | sub(T26, T27, X29), SCOPE: 4, CLAUSE: 5\n\nT26 is ground\nT27 is ground\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: true | sub(T32, 0, X29), SCOPE: 4, CLAUSE: 5\n\nT32 is ground\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: sub(T26, T27, X29), SCOPE: 4, CLAUSE: 5\n\nT26 is ground\nT27 is ground\nX29 is free\nX34 is free\nsub(T26, T27, X29) !=? sub(X34, 0, X34)", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: sub(T32, 0, X29), SCOPE: 4, CLAUSE: 5\n\nT32 is ground\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: sub(T38, T39, X49)\n\nT38 is ground\nT39 is ground\nX49 is free", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: rem(T7, s(T13), T3), SCOPE: 1, CLAUSE: 4\n\nT7 is ground\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: ','(notZero(s(T50)), geq(T49, s(T50)))\n\nT49 is ground\nT50 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ','(notZero(s(T50)), geq(T49, s(T50))), SCOPE: 5, CLAUSE: 1\n\nT49 is ground\nT50 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: geq(T49, s(T57))\n\nT49 is ground\nT57 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: geq(T49, s(T57)), SCOPE: 6, CLAUSE: 2 | geq(T49, s(T57)), SCOPE: 6, CLAUSE: 6\n\nT49 is ground\nT57 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: geq(T49, s(T57)), SCOPE: 6, CLAUSE: 6\n\nT49 is ground\nT57 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: geq(T65, T66)\n\nT65 is ground\nT66 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: geq(T65, T66), SCOPE: 7, CLAUSE: 2 | geq(T65, T66), SCOPE: 7, CLAUSE: 6\n\nT65 is ground\nT66 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: true | geq(T71, 0), SCOPE: 7, CLAUSE: 6\n\nT71 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: geq(T65, T66), SCOPE: 7, CLAUSE: 6\n\nT65 is ground\nT66 is ground\nX82 is free\ngeq(T65, T66) !=? geq(X82, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: geq(T71, 0), SCOPE: 7, CLAUSE: 6\n\nT71 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: geq(T77, T78)\n\nT77 is ground\nT78 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: rem(T7, T8, T3), SCOPE: 1, CLAUSE: 4\n\nT7 is ground\nT8 is ground\nX10 is free\nnotZero(T8) !=? notZero(s(X10))", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: ','(notZero(T86), geq(T85, T86))\n\nT85 is ground\nT86 is ground\nX10 is free\nnotZero(T86) !=? notZero(s(X10))", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: ','(notZero(T86), geq(T85, T86)), SCOPE: 8, CLAUSE: 1\n\nT85 is ground\nT86 is ground\nX10 is free\nnotZero(T86) !=? notZero(s(X10))", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 80 [arrowhead = none ];
80 -> 3;

81 [label="ONLY EVAL with clause\nrem(X4, X5, X6) :- ','(notZero(X5), ','(sub(X4, X5, X7), rem(X7, X5, X6))).\nand substitutionT1 -> T7,\nX4 -> T7,\nT2 -> T8,\nX5 -> T8,\nT3 -> T10,\nX6 -> T10,\nT9 -> T10", fontsize=14, style = filled, fillcolor = lightblue];
3 -> 81 [arrowhead = none ];
81 -> 5;

82 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
5 -> 82 [arrowhead = none ];
82 -> 6;

83 [label="EVAL with clause\nnotZero(s(X10)).\nand substitutionX10 -> T13,\nT8 -> s(T13)", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 83 [arrowhead = none ];
83 -> 7;

84 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
6 -> 84 [arrowhead = none ];
84 -> 8;

85 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
7 -> 85 [arrowhead = none ];
85 -> 9;

86 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
7 -> 86 [arrowhead = none ];
86 -> 10;

87 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
8 -> 87 [arrowhead = none ];
87 -> 75;

88 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
9 -> 88 [arrowhead = none ];
88 -> 15;

89 [label="SPLIT 2\nnew knowledge:\nT7 is ground\nT13 is ground\nT18 is ground\nreplacements:X7 -> T18", fontsize=14, style = filled, fillcolor = violet];
9 -> 89 [arrowhead = none ];
89 -> 16;

90 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
10 -> 90 [arrowhead = none ];
90 -> 43;

91 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
15 -> 91 [arrowhead = none ];
91 -> 20;

92 [label="INSTANCE with matching:\nT1 -> T18\nT2 -> s(T13)\nT3 -> T10", fontsize=14, style = filled, fillcolor = lightgrey];
16 -> 92 [arrowhead = none , style=dashed];
92 -> 2[style=dashed];

93 [label="BACKTRACK\nfor clause: sub(X, 0, X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
20 -> 93 [arrowhead = none ];
93 -> 22;

94 [label="EVAL with clause\nsub(s(X26), s(X27), X28) :- sub(X26, X27, X28).\nand substitutionX26 -> T26,\nT7 -> s(T26),\nT13 -> T27,\nX27 -> T27,\nX7 -> X29,\nX28 -> X29", fontsize=14, style = filled, fillcolor = lightblue];
22 -> 94 [arrowhead = none ];
94 -> 25;

95 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
22 -> 95 [arrowhead = none ];
95 -> 26;

96 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
25 -> 96 [arrowhead = none ];
96 -> 29;

97 [label="EVAL with clause\nsub(X34, 0, X34).\nand substitutionT26 -> T32,\nX34 -> T32,\nT27 -> 0,\nX29 -> T32", fontsize=14, style = filled, fillcolor = lightblue];
29 -> 97 [arrowhead = none ];
97 -> 31;

98 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
29 -> 98 [arrowhead = none ];
98 -> 32;

99 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
31 -> 99 [arrowhead = none ];
99 -> 33;

100 [label="EVAL with clause\nsub(s(X46), s(X47), X48) :- sub(X46, X47, X48).\nand substitutionX46 -> T38,\nT26 -> s(T38),\nX47 -> T39,\nT27 -> s(T39),\nX29 -> X49,\nX48 -> X49", fontsize=14, style = filled, fillcolor = lightblue];
32 -> 100 [arrowhead = none ];
100 -> 39;

101 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
32 -> 101 [arrowhead = none ];
101 -> 40;

102 [label="BACKTRACK\nfor clause: sub(s(X), s(Y), Z) :- sub(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
33 -> 102 [arrowhead = none ];
102 -> 37;

103 [label="INSTANCE with matching:\nT26 -> T38\nT27 -> T39\nX29 -> X49", fontsize=14, style = filled, fillcolor = lightgrey];
39 -> 103 [arrowhead = none , style=dashed];
103 -> 25[style=dashed];

104 [label="EVAL with clause\nrem(X60, X61, X60) :- ','(notZero(X61), geq(X60, X61)).\nand substitutionT7 -> T49,\nX60 -> T49,\nT13 -> T50,\nX61 -> s(T50),\nT3 -> T49", fontsize=14, style = filled, fillcolor = lightblue];
43 -> 104 [arrowhead = none ];
104 -> 46;

105 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
43 -> 105 [arrowhead = none ];
105 -> 47;

106 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
46 -> 106 [arrowhead = none ];
106 -> 49;

107 [label="ONLY EVAL with clause\nnotZero(s(X68)).\nand substitutionT50 -> T57,\nX68 -> T57", fontsize=14, style = filled, fillcolor = lightblue];
49 -> 107 [arrowhead = none ];
107 -> 52;

108 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
52 -> 108 [arrowhead = none ];
108 -> 55;

109 [label="BACKTRACK\nfor clause: geq(X, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
55 -> 109 [arrowhead = none ];
109 -> 56;

110 [label="EVAL with clause\ngeq(s(X76), s(X77)) :- geq(X76, X77).\nand substitutionX76 -> T65,\nT49 -> s(T65),\nT57 -> T66,\nX77 -> T66", fontsize=14, style = filled, fillcolor = lightblue];
56 -> 110 [arrowhead = none ];
110 -> 59;

111 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
56 -> 111 [arrowhead = none ];
111 -> 60;

112 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
59 -> 112 [arrowhead = none ];
112 -> 62;

113 [label="EVAL with clause\ngeq(X82, 0).\nand substitutionT65 -> T71,\nX82 -> T71,\nT66 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
62 -> 113 [arrowhead = none ];
113 -> 66;

114 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
62 -> 114 [arrowhead = none ];
114 -> 68;

115 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
66 -> 115 [arrowhead = none ];
115 -> 69;

116 [label="EVAL with clause\ngeq(s(X89), s(X90)) :- geq(X89, X90).\nand substitutionX89 -> T77,\nT65 -> s(T77),\nX90 -> T78,\nT66 -> s(T78)", fontsize=14, style = filled, fillcolor = lightblue];
68 -> 116 [arrowhead = none ];
116 -> 73;

117 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
68 -> 117 [arrowhead = none ];
117 -> 74;

118 [label="BACKTRACK\nfor clause: geq(s(X), s(Y)) :- geq(X, Y)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
69 -> 118 [arrowhead = none ];
118 -> 70;

119 [label="INSTANCE with matching:\nT65 -> T77\nT66 -> T78", fontsize=14, style = filled, fillcolor = lightgrey];
73 -> 119 [arrowhead = none , style=dashed];
119 -> 59[style=dashed];

120 [label="EVAL with clause\nrem(X97, X98, X97) :- ','(notZero(X98), geq(X97, X98)).\nand substitutionT7 -> T85,\nX97 -> T85,\nT8 -> T86,\nX98 -> T86,\nT3 -> T85", fontsize=14, style = filled, fillcolor = lightblue];
75 -> 120 [arrowhead = none ];
120 -> 76;

121 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
75 -> 121 [arrowhead = none ];
121 -> 77;

122 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
76 -> 122 [arrowhead = none ];
122 -> 78;

123 [label="BACKTRACK\nfor clause: notZero(s(X))\nwith clash: (notZero(T86), notZero(s(X10)))", fontsize=14, style = filled, fillcolor = lightgreen];
78 -> 123 [arrowhead = none ];
123 -> 79;

}

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, s(z1)) → U1(f7_in(z0, z1), z0, s(z1))
U1(f7_out1(z0, z1), z2, s(z3)) → f2_out1(z1)
U1(f7_out3(z0), z1, s(z2)) → f2_out1(z0)
f25_in(z0, 0) → f25_out1(z0)
f25_in(s(z0), s(z1)) → U2(f25_in(z0, z1), s(z0), s(z1))
U2(f25_out1(z0), s(z1), s(z2)) → f25_out1(z0)
f59_in(z0, 0) → f59_out1
f59_in(s(z0), s(z1)) → U3(f59_in(z0, z1), s(z0), s(z1))
U3(f59_out1, s(z0), s(z1)) → f59_out1
f15_in(s(z0), z1) → U4(f25_in(z0, z1), s(z0), z1)
U4(f25_out1(z0), s(z1), z2) → f15_out1(z0)
f10_in(s(z0), z1) → U5(f59_in(z0, z1), s(z0), z1)
U5(f59_out1, s(z0), z1) → f10_out2(s(z0))
f9_in(z0, z1) → U6(f15_in(z0, z1), z0, z1)
U6(f15_out1(z0), z1, z2) → U7(f2_in(z0, s(z2)), z1, z2, z0)
U7(f2_out1(z0), z1, z2, z3) → f9_out1(z3, z0)
f7_in(z0, z1) → U8(f9_in(z0, z1), f10_in(z0, z1), z0, z1)
U8(f9_out1(z0, z1), z2, z3, z4) → f7_out1(z0, z1)
U8(z0, f10_out2(z1), z2, z3) → f7_out3(z1)

Tuples:

F2_IN(z0, s(z1)) → c(U1'(f7_in(z0, z1), z0, s(z1)), F7_IN(z0, z1))
F25_IN(s(z0), s(z1)) → c4(U2'(f25_in(z0, z1), s(z0), s(z1)), F25_IN(z0, z1))
F59_IN(s(z0), s(z1)) → c7(U3'(f59_in(z0, z1), s(z0), s(z1)), F59_IN(z0, z1))
F15_IN(s(z0), z1) → c9(U4'(f25_in(z0, z1), s(z0), z1), F25_IN(z0, z1))
F10_IN(s(z0), z1) → c11(U5'(f59_in(z0, z1), s(z0), z1), F59_IN(z0, z1))
F9_IN(z0, z1) → c13(U6'(f15_in(z0, z1), z0, z1), F15_IN(z0, z1))
U6'(f15_out1(z0), z1, z2) → c14(U7'(f2_in(z0, s(z2)), z1, z2, z0), F2_IN(z0, s(z2)))
F7_IN(z0, z1) → c16(U8'(f9_in(z0, z1), f10_in(z0, z1), z0, z1), F9_IN(z0, z1), F10_IN(z0, z1))

S tuples:

F2_IN(z0, s(z1)) → c(U1'(f7_in(z0, z1), z0, s(z1)), F7_IN(z0, z1))
F25_IN(s(z0), s(z1)) → c4(U2'(f25_in(z0, z1), s(z0), s(z1)), F25_IN(z0, z1))
F59_IN(s(z0), s(z1)) → c7(U3'(f59_in(z0, z1), s(z0), s(z1)), F59_IN(z0, z1))
F15_IN(s(z0), z1) → c9(U4'(f25_in(z0, z1), s(z0), z1), F25_IN(z0, z1))
F10_IN(s(z0), z1) → c11(U5'(f59_in(z0, z1), s(z0), z1), F59_IN(z0, z1))
F9_IN(z0, z1) → c13(U6'(f15_in(z0, z1), z0, z1), F15_IN(z0, z1))
U6'(f15_out1(z0), z1, z2) → c14(U7'(f2_in(z0, s(z2)), z1, z2, z0), F2_IN(z0, s(z2)))
F7_IN(z0, z1) → c16(U8'(f9_in(z0, z1), f10_in(z0, z1), z0, z1), F9_IN(z0, z1), F10_IN(z0, z1))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f25_in, U2, f59_in, U3, f15_in, U4, f10_in, U5, f9_in, U6, U7, f7_in, U8

Defined Pair Symbols:

F2_IN, F25_IN, F59_IN, F15_IN, F10_IN, F9_IN, U6', F7_IN

Compound Symbols:

c, c4, c7, c9, c11, c13, c14, c16

(25) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, s(z1)) → U1(f7_in(z0, z1), z0, s(z1))
U1(f7_out1(z0, z1), z2, s(z3)) → f2_out1(z1)
U1(f7_out3(z0), z1, s(z2)) → f2_out1(z0)
f25_in(z0, 0) → f25_out1(z0)
f25_in(s(z0), s(z1)) → U2(f25_in(z0, z1), s(z0), s(z1))
U2(f25_out1(z0), s(z1), s(z2)) → f25_out1(z0)
f59_in(z0, 0) → f59_out1
f59_in(s(z0), s(z1)) → U3(f59_in(z0, z1), s(z0), s(z1))
U3(f59_out1, s(z0), s(z1)) → f59_out1
f15_in(s(z0), z1) → U4(f25_in(z0, z1), s(z0), z1)
U4(f25_out1(z0), s(z1), z2) → f15_out1(z0)
f10_in(s(z0), z1) → U5(f59_in(z0, z1), s(z0), z1)
U5(f59_out1, s(z0), z1) → f10_out2(s(z0))
f9_in(z0, z1) → U6(f15_in(z0, z1), z0, z1)
U6(f15_out1(z0), z1, z2) → U7(f2_in(z0, s(z2)), z1, z2, z0)
U7(f2_out1(z0), z1, z2, z3) → f9_out1(z3, z0)
f7_in(z0, z1) → U8(f9_in(z0, z1), f10_in(z0, z1), z0, z1)
U8(f9_out1(z0, z1), z2, z3, z4) → f7_out1(z0, z1)
U8(z0, f10_out2(z1), z2, z3) → f7_out3(z1)

Tuples:

F2_IN(z0, s(z1)) → c(U1'(f7_in(z0, z1), z0, s(z1)), F7_IN(z0, z1))
F25_IN(s(z0), s(z1)) → c4(U2'(f25_in(z0, z1), s(z0), s(z1)), F25_IN(z0, z1))
F59_IN(s(z0), s(z1)) → c7(U3'(f59_in(z0, z1), s(z0), s(z1)), F59_IN(z0, z1))
F9_IN(z0, z1) → c13(U6'(f15_in(z0, z1), z0, z1), F15_IN(z0, z1))
U6'(f15_out1(z0), z1, z2) → c14(U7'(f2_in(z0, s(z2)), z1, z2, z0), F2_IN(z0, s(z2)))
F7_IN(z0, z1) → c16(U8'(f9_in(z0, z1), f10_in(z0, z1), z0, z1), F9_IN(z0, z1), F10_IN(z0, z1))
F15_IN(s(z0), z1) → c1(U4'(f25_in(z0, z1), s(z0), z1))
F15_IN(s(z0), z1) → c1(F25_IN(z0, z1))
F10_IN(s(z0), z1) → c1(U5'(f59_in(z0, z1), s(z0), z1))
F10_IN(s(z0), z1) → c1(F59_IN(z0, z1))

S tuples:

F2_IN(z0, s(z1)) → c(U1'(f7_in(z0, z1), z0, s(z1)), F7_IN(z0, z1))
F25_IN(s(z0), s(z1)) → c4(U2'(f25_in(z0, z1), s(z0), s(z1)), F25_IN(z0, z1))
F59_IN(s(z0), s(z1)) → c7(U3'(f59_in(z0, z1), s(z0), s(z1)), F59_IN(z0, z1))
F9_IN(z0, z1) → c13(U6'(f15_in(z0, z1), z0, z1), F15_IN(z0, z1))
U6'(f15_out1(z0), z1, z2) → c14(U7'(f2_in(z0, s(z2)), z1, z2, z0), F2_IN(z0, s(z2)))
F7_IN(z0, z1) → c16(U8'(f9_in(z0, z1), f10_in(z0, z1), z0, z1), F9_IN(z0, z1), F10_IN(z0, z1))
F15_IN(s(z0), z1) → c1(U4'(f25_in(z0, z1), s(z0), z1))
F15_IN(s(z0), z1) → c1(F25_IN(z0, z1))
F10_IN(s(z0), z1) → c1(U5'(f59_in(z0, z1), s(z0), z1))
F10_IN(s(z0), z1) → c1(F59_IN(z0, z1))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f25_in, U2, f59_in, U3, f15_in, U4, f10_in, U5, f9_in, U6, U7, f7_in, U8

Defined Pair Symbols:

F2_IN, F25_IN, F59_IN, F9_IN, U6', F7_IN, F15_IN, F10_IN

Compound Symbols:

c, c4, c7, c13, c14, c16, c1

(27) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)

Removed 7 trailing tuple parts

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, s(z1)) → U1(f7_in(z0, z1), z0, s(z1))
U1(f7_out1(z0, z1), z2, s(z3)) → f2_out1(z1)
U1(f7_out3(z0), z1, s(z2)) → f2_out1(z0)
f25_in(z0, 0) → f25_out1(z0)
f25_in(s(z0), s(z1)) → U2(f25_in(z0, z1), s(z0), s(z1))
U2(f25_out1(z0), s(z1), s(z2)) → f25_out1(z0)
f59_in(z0, 0) → f59_out1
f59_in(s(z0), s(z1)) → U3(f59_in(z0, z1), s(z0), s(z1))
U3(f59_out1, s(z0), s(z1)) → f59_out1
f15_in(s(z0), z1) → U4(f25_in(z0, z1), s(z0), z1)
U4(f25_out1(z0), s(z1), z2) → f15_out1(z0)
f10_in(s(z0), z1) → U5(f59_in(z0, z1), s(z0), z1)
U5(f59_out1, s(z0), z1) → f10_out2(s(z0))
f9_in(z0, z1) → U6(f15_in(z0, z1), z0, z1)
U6(f15_out1(z0), z1, z2) → U7(f2_in(z0, s(z2)), z1, z2, z0)
U7(f2_out1(z0), z1, z2, z3) → f9_out1(z3, z0)
f7_in(z0, z1) → U8(f9_in(z0, z1), f10_in(z0, z1), z0, z1)
U8(f9_out1(z0, z1), z2, z3, z4) → f7_out1(z0, z1)
U8(z0, f10_out2(z1), z2, z3) → f7_out3(z1)

Tuples:

F9_IN(z0, z1) → c13(U6'(f15_in(z0, z1), z0, z1), F15_IN(z0, z1))
F15_IN(s(z0), z1) → c1(F25_IN(z0, z1))
F10_IN(s(z0), z1) → c1(F59_IN(z0, z1))
F2_IN(z0, s(z1)) → c(F7_IN(z0, z1))
F25_IN(s(z0), s(z1)) → c4(F25_IN(z0, z1))
F59_IN(s(z0), s(z1)) → c7(F59_IN(z0, z1))
U6'(f15_out1(z0), z1, z2) → c14(F2_IN(z0, s(z2)))
F7_IN(z0, z1) → c16(F9_IN(z0, z1), F10_IN(z0, z1))
F15_IN(s(z0), z1) → c1
F10_IN(s(z0), z1) → c1

S tuples:

F9_IN(z0, z1) → c13(U6'(f15_in(z0, z1), z0, z1), F15_IN(z0, z1))
F15_IN(s(z0), z1) → c1(F25_IN(z0, z1))
F10_IN(s(z0), z1) → c1(F59_IN(z0, z1))
F2_IN(z0, s(z1)) → c(F7_IN(z0, z1))
F25_IN(s(z0), s(z1)) → c4(F25_IN(z0, z1))
F59_IN(s(z0), s(z1)) → c7(F59_IN(z0, z1))
U6'(f15_out1(z0), z1, z2) → c14(F2_IN(z0, s(z2)))
F7_IN(z0, z1) → c16(F9_IN(z0, z1), F10_IN(z0, z1))
F15_IN(s(z0), z1) → c1
F10_IN(s(z0), z1) → c1

K tuples:none
Defined Rule Symbols:

f2_in, U1, f25_in, U2, f59_in, U3, f15_in, U4, f10_in, U5, f9_in, U6, U7, f7_in, U8

Defined Pair Symbols:

F9_IN, F15_IN, F10_IN, F2_IN, F25_IN, F59_IN, U6', F7_IN

Compound Symbols:

c13, c1, c, c4, c7, c14, c16, c1

(29) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

U6'(f15_out1(z0), z1, z2) → c14(F2_IN(z0, s(z2)))

We considered the (Usable) Rules:

f15_in(s(z0), z1) → U4(f25_in(z0, z1), s(z0), z1)
f25_in(z0, 0) → f25_out1(z0)
f25_in(s(z0), s(z1)) → U2(f25_in(z0, z1), s(z0), s(z1))
U4(f25_out1(z0), s(z1), z2) → f15_out1(z0)
U2(f25_out1(z0), s(z1), s(z2)) → f25_out1(z0)

And the Tuples:

F9_IN(z0, z1) → c13(U6'(f15_in(z0, z1), z0, z1), F15_IN(z0, z1))
F15_IN(s(z0), z1) → c1(F25_IN(z0, z1))
F10_IN(s(z0), z1) → c1(F59_IN(z0, z1))
F2_IN(z0, s(z1)) → c(F7_IN(z0, z1))
F25_IN(s(z0), s(z1)) → c4(F25_IN(z0, z1))
F59_IN(s(z0), s(z1)) → c7(F59_IN(z0, z1))
U6'(f15_out1(z0), z1, z2) → c14(F2_IN(z0, s(z2)))
F7_IN(z0, z1) → c16(F9_IN(z0, z1), F10_IN(z0, z1))
F15_IN(s(z0), z1) → c1
F10_IN(s(z0), z1) → c1

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0
POL(F10_IN(x₁, x₂)) = 0
POL(F15_IN(x₁, x₂)) = 0
POL(F25_IN(x₁, x₂)) = 0
POL(F2_IN(x₁, x₂)) = [1] + x₁²
POL(F59_IN(x₁, x₂)) = 0
POL(F7_IN(x₁, x₂)) = [1] + x₁²
POL(F9_IN(x₁, x₂)) = [1] + x₁²
POL(U2(x₁, x₂, x₃)) = x₁
POL(U4(x₁, x₂, x₃)) = [1] + x₁
POL(U6'(x₁, x₂, x₃)) = [1] + x₁²
POL(c(x₁)) = x₁
POL(c1) = 0
POL(c1(x₁)) = x₁
POL(c13(x₁, x₂)) = x₁ + x₂
POL(c14(x₁)) = x₁
POL(c16(x₁, x₂)) = x₁ + x₂
POL(c4(x₁)) = x₁
POL(c7(x₁)) = x₁
POL(f15_in(x₁, x₂)) = x₁
POL(f15_out1(x₁)) = [1] + x₁
POL(f25_in(x₁, x₂)) = x₁
POL(f25_out1(x₁)) = x₁
POL(s(x₁)) = [1] + x₁

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, s(z1)) → U1(f7_in(z0, z1), z0, s(z1))
U1(f7_out1(z0, z1), z2, s(z3)) → f2_out1(z1)
U1(f7_out3(z0), z1, s(z2)) → f2_out1(z0)
f25_in(z0, 0) → f25_out1(z0)
f25_in(s(z0), s(z1)) → U2(f25_in(z0, z1), s(z0), s(z1))
U2(f25_out1(z0), s(z1), s(z2)) → f25_out1(z0)
f59_in(z0, 0) → f59_out1
f59_in(s(z0), s(z1)) → U3(f59_in(z0, z1), s(z0), s(z1))
U3(f59_out1, s(z0), s(z1)) → f59_out1
f15_in(s(z0), z1) → U4(f25_in(z0, z1), s(z0), z1)
U4(f25_out1(z0), s(z1), z2) → f15_out1(z0)
f10_in(s(z0), z1) → U5(f59_in(z0, z1), s(z0), z1)
U5(f59_out1, s(z0), z1) → f10_out2(s(z0))
f9_in(z0, z1) → U6(f15_in(z0, z1), z0, z1)
U6(f15_out1(z0), z1, z2) → U7(f2_in(z0, s(z2)), z1, z2, z0)
U7(f2_out1(z0), z1, z2, z3) → f9_out1(z3, z0)
f7_in(z0, z1) → U8(f9_in(z0, z1), f10_in(z0, z1), z0, z1)
U8(f9_out1(z0, z1), z2, z3, z4) → f7_out1(z0, z1)
U8(z0, f10_out2(z1), z2, z3) → f7_out3(z1)

Tuples:

F9_IN(z0, z1) → c13(U6'(f15_in(z0, z1), z0, z1), F15_IN(z0, z1))
F15_IN(s(z0), z1) → c1(F25_IN(z0, z1))
F10_IN(s(z0), z1) → c1(F59_IN(z0, z1))
F2_IN(z0, s(z1)) → c(F7_IN(z0, z1))
F25_IN(s(z0), s(z1)) → c4(F25_IN(z0, z1))
F59_IN(s(z0), s(z1)) → c7(F59_IN(z0, z1))
U6'(f15_out1(z0), z1, z2) → c14(F2_IN(z0, s(z2)))
F7_IN(z0, z1) → c16(F9_IN(z0, z1), F10_IN(z0, z1))
F15_IN(s(z0), z1) → c1
F10_IN(s(z0), z1) → c1

S tuples:

F9_IN(z0, z1) → c13(U6'(f15_in(z0, z1), z0, z1), F15_IN(z0, z1))
F15_IN(s(z0), z1) → c1(F25_IN(z0, z1))
F10_IN(s(z0), z1) → c1(F59_IN(z0, z1))
F2_IN(z0, s(z1)) → c(F7_IN(z0, z1))
F25_IN(s(z0), s(z1)) → c4(F25_IN(z0, z1))
F59_IN(s(z0), s(z1)) → c7(F59_IN(z0, z1))
F7_IN(z0, z1) → c16(F9_IN(z0, z1), F10_IN(z0, z1))
F15_IN(s(z0), z1) → c1
F10_IN(s(z0), z1) → c1

K tuples:

U6'(f15_out1(z0), z1, z2) → c14(F2_IN(z0, s(z2)))

Defined Rule Symbols:

f2_in, U1, f25_in, U2, f59_in, U3, f15_in, U4, f10_in, U5, f9_in, U6, U7, f7_in, U8

Defined Pair Symbols:

F9_IN, F15_IN, F10_IN, F2_IN, F25_IN, F59_IN, U6', F7_IN

Compound Symbols:

c13, c1, c, c4, c7, c14, c16, c1

(31) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

F2_IN(z0, s(z1)) → c(F7_IN(z0, z1))
F7_IN(z0, z1) → c16(F9_IN(z0, z1), F10_IN(z0, z1))
F10_IN(s(z0), z1) → c1
F7_IN(z0, z1) → c16(F9_IN(z0, z1), F10_IN(z0, z1))
F9_IN(z0, z1) → c13(U6'(f15_in(z0, z1), z0, z1), F15_IN(z0, z1))
F10_IN(s(z0), z1) → c1(F59_IN(z0, z1))
F10_IN(s(z0), z1) → c1
F15_IN(s(z0), z1) → c1(F25_IN(z0, z1))
U6'(f15_out1(z0), z1, z2) → c14(F2_IN(z0, s(z2)))
F15_IN(s(z0), z1) → c1

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, s(z1)) → U1(f7_in(z0, z1), z0, s(z1))
U1(f7_out1(z0, z1), z2, s(z3)) → f2_out1(z1)
U1(f7_out3(z0), z1, s(z2)) → f2_out1(z0)
f25_in(z0, 0) → f25_out1(z0)
f25_in(s(z0), s(z1)) → U2(f25_in(z0, z1), s(z0), s(z1))
U2(f25_out1(z0), s(z1), s(z2)) → f25_out1(z0)
f59_in(z0, 0) → f59_out1
f59_in(s(z0), s(z1)) → U3(f59_in(z0, z1), s(z0), s(z1))
U3(f59_out1, s(z0), s(z1)) → f59_out1
f15_in(s(z0), z1) → U4(f25_in(z0, z1), s(z0), z1)
U4(f25_out1(z0), s(z1), z2) → f15_out1(z0)
f10_in(s(z0), z1) → U5(f59_in(z0, z1), s(z0), z1)
U5(f59_out1, s(z0), z1) → f10_out2(s(z0))
f9_in(z0, z1) → U6(f15_in(z0, z1), z0, z1)
U6(f15_out1(z0), z1, z2) → U7(f2_in(z0, s(z2)), z1, z2, z0)
U7(f2_out1(z0), z1, z2, z3) → f9_out1(z3, z0)
f7_in(z0, z1) → U8(f9_in(z0, z1), f10_in(z0, z1), z0, z1)
U8(f9_out1(z0, z1), z2, z3, z4) → f7_out1(z0, z1)
U8(z0, f10_out2(z1), z2, z3) → f7_out3(z1)

Tuples:

F9_IN(z0, z1) → c13(U6'(f15_in(z0, z1), z0, z1), F15_IN(z0, z1))
F15_IN(s(z0), z1) → c1(F25_IN(z0, z1))
F10_IN(s(z0), z1) → c1(F59_IN(z0, z1))
F2_IN(z0, s(z1)) → c(F7_IN(z0, z1))
F25_IN(s(z0), s(z1)) → c4(F25_IN(z0, z1))
F59_IN(s(z0), s(z1)) → c7(F59_IN(z0, z1))
U6'(f15_out1(z0), z1, z2) → c14(F2_IN(z0, s(z2)))
F7_IN(z0, z1) → c16(F9_IN(z0, z1), F10_IN(z0, z1))
F15_IN(s(z0), z1) → c1
F10_IN(s(z0), z1) → c1

S tuples:

F25_IN(s(z0), s(z1)) → c4(F25_IN(z0, z1))
F59_IN(s(z0), s(z1)) → c7(F59_IN(z0, z1))

K tuples:

U6'(f15_out1(z0), z1, z2) → c14(F2_IN(z0, s(z2)))
F2_IN(z0, s(z1)) → c(F7_IN(z0, z1))
F7_IN(z0, z1) → c16(F9_IN(z0, z1), F10_IN(z0, z1))
F10_IN(s(z0), z1) → c1
F9_IN(z0, z1) → c13(U6'(f15_in(z0, z1), z0, z1), F15_IN(z0, z1))
F10_IN(s(z0), z1) → c1(F59_IN(z0, z1))
F15_IN(s(z0), z1) → c1(F25_IN(z0, z1))
F15_IN(s(z0), z1) → c1

Defined Rule Symbols:

f2_in, U1, f25_in, U2, f59_in, U3, f15_in, U4, f10_in, U5, f9_in, U6, U7, f7_in, U8

Defined Pair Symbols:

F9_IN, F15_IN, F10_IN, F2_IN, F25_IN, F59_IN, U6', F7_IN

Compound Symbols:

c13, c1, c, c4, c7, c14, c16, c1

(33) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace F9_IN(z0, z1) → c13(U6'(f15_in(z0, z1), z0, z1), F15_IN(z0, z1)) by

F9_IN(s(z0), z1) → c13(U6'(U4(f25_in(z0, z1), s(z0), z1), s(z0), z1), F15_IN(s(z0), z1))

(34) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, s(z1)) → U1(f7_in(z0, z1), z0, s(z1))
U1(f7_out1(z0, z1), z2, s(z3)) → f2_out1(z1)
U1(f7_out3(z0), z1, s(z2)) → f2_out1(z0)
f25_in(z0, 0) → f25_out1(z0)
f25_in(s(z0), s(z1)) → U2(f25_in(z0, z1), s(z0), s(z1))
U2(f25_out1(z0), s(z1), s(z2)) → f25_out1(z0)
f59_in(z0, 0) → f59_out1
f59_in(s(z0), s(z1)) → U3(f59_in(z0, z1), s(z0), s(z1))
U3(f59_out1, s(z0), s(z1)) → f59_out1
f15_in(s(z0), z1) → U4(f25_in(z0, z1), s(z0), z1)
U4(f25_out1(z0), s(z1), z2) → f15_out1(z0)
f10_in(s(z0), z1) → U5(f59_in(z0, z1), s(z0), z1)
U5(f59_out1, s(z0), z1) → f10_out2(s(z0))
f9_in(z0, z1) → U6(f15_in(z0, z1), z0, z1)
U6(f15_out1(z0), z1, z2) → U7(f2_in(z0, s(z2)), z1, z2, z0)
U7(f2_out1(z0), z1, z2, z3) → f9_out1(z3, z0)
f7_in(z0, z1) → U8(f9_in(z0, z1), f10_in(z0, z1), z0, z1)
U8(f9_out1(z0, z1), z2, z3, z4) → f7_out1(z0, z1)
U8(z0, f10_out2(z1), z2, z3) → f7_out3(z1)

Tuples:

F15_IN(s(z0), z1) → c1(F25_IN(z0, z1))
F10_IN(s(z0), z1) → c1(F59_IN(z0, z1))
F2_IN(z0, s(z1)) → c(F7_IN(z0, z1))
F25_IN(s(z0), s(z1)) → c4(F25_IN(z0, z1))
F59_IN(s(z0), s(z1)) → c7(F59_IN(z0, z1))
U6'(f15_out1(z0), z1, z2) → c14(F2_IN(z0, s(z2)))
F7_IN(z0, z1) → c16(F9_IN(z0, z1), F10_IN(z0, z1))
F15_IN(s(z0), z1) → c1
F10_IN(s(z0), z1) → c1
F9_IN(s(z0), z1) → c13(U6'(U4(f25_in(z0, z1), s(z0), z1), s(z0), z1), F15_IN(s(z0), z1))

S tuples:

F25_IN(s(z0), s(z1)) → c4(F25_IN(z0, z1))
F59_IN(s(z0), s(z1)) → c7(F59_IN(z0, z1))

K tuples:

U6'(f15_out1(z0), z1, z2) → c14(F2_IN(z0, s(z2)))
F2_IN(z0, s(z1)) → c(F7_IN(z0, z1))
F7_IN(z0, z1) → c16(F9_IN(z0, z1), F10_IN(z0, z1))
F10_IN(s(z0), z1) → c1
F9_IN(z0, z1) → c13(U6'(f15_in(z0, z1), z0, z1), F15_IN(z0, z1))
F10_IN(s(z0), z1) → c1(F59_IN(z0, z1))
F15_IN(s(z0), z1) → c1(F25_IN(z0, z1))
F15_IN(s(z0), z1) → c1

Defined Rule Symbols:

f2_in, U1, f25_in, U2, f59_in, U3, f15_in, U4, f10_in, U5, f9_in, U6, U7, f7_in, U8

Defined Pair Symbols:

F15_IN, F10_IN, F2_IN, F25_IN, F59_IN, U6', F7_IN, F9_IN

Compound Symbols:

c1, c, c4, c7, c14, c16, c1, c13

(35) CdtGraphRemoveDanglingProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 of 10 dangling nodes:

F10_IN(s(z0), z1) → c1

(36) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, s(z1)) → U1(f7_in(z0, z1), z0, s(z1))
U1(f7_out1(z0, z1), z2, s(z3)) → f2_out1(z1)
U1(f7_out3(z0), z1, s(z2)) → f2_out1(z0)
f25_in(z0, 0) → f25_out1(z0)
f25_in(s(z0), s(z1)) → U2(f25_in(z0, z1), s(z0), s(z1))
U2(f25_out1(z0), s(z1), s(z2)) → f25_out1(z0)
f59_in(z0, 0) → f59_out1
f59_in(s(z0), s(z1)) → U3(f59_in(z0, z1), s(z0), s(z1))
U3(f59_out1, s(z0), s(z1)) → f59_out1
f15_in(s(z0), z1) → U4(f25_in(z0, z1), s(z0), z1)
U4(f25_out1(z0), s(z1), z2) → f15_out1(z0)
f10_in(s(z0), z1) → U5(f59_in(z0, z1), s(z0), z1)
U5(f59_out1, s(z0), z1) → f10_out2(s(z0))
f9_in(z0, z1) → U6(f15_in(z0, z1), z0, z1)
U6(f15_out1(z0), z1, z2) → U7(f2_in(z0, s(z2)), z1, z2, z0)
U7(f2_out1(z0), z1, z2, z3) → f9_out1(z3, z0)
f7_in(z0, z1) → U8(f9_in(z0, z1), f10_in(z0, z1), z0, z1)
U8(f9_out1(z0, z1), z2, z3, z4) → f7_out1(z0, z1)
U8(z0, f10_out2(z1), z2, z3) → f7_out3(z1)

Tuples:

F15_IN(s(z0), z1) → c1(F25_IN(z0, z1))
F10_IN(s(z0), z1) → c1(F59_IN(z0, z1))
F2_IN(z0, s(z1)) → c(F7_IN(z0, z1))
F25_IN(s(z0), s(z1)) → c4(F25_IN(z0, z1))
F59_IN(s(z0), s(z1)) → c7(F59_IN(z0, z1))
U6'(f15_out1(z0), z1, z2) → c14(F2_IN(z0, s(z2)))
F7_IN(z0, z1) → c16(F9_IN(z0, z1), F10_IN(z0, z1))
F15_IN(s(z0), z1) → c1
F9_IN(s(z0), z1) → c13(U6'(U4(f25_in(z0, z1), s(z0), z1), s(z0), z1), F15_IN(s(z0), z1))

S tuples:

F25_IN(s(z0), s(z1)) → c4(F25_IN(z0, z1))
F59_IN(s(z0), s(z1)) → c7(F59_IN(z0, z1))

K tuples:

U6'(f15_out1(z0), z1, z2) → c14(F2_IN(z0, s(z2)))
F2_IN(z0, s(z1)) → c(F7_IN(z0, z1))
F7_IN(z0, z1) → c16(F9_IN(z0, z1), F10_IN(z0, z1))
F10_IN(s(z0), z1) → c1(F59_IN(z0, z1))
F15_IN(s(z0), z1) → c1(F25_IN(z0, z1))
F15_IN(s(z0), z1) → c1

Defined Rule Symbols:

f2_in, U1, f25_in, U2, f59_in, U3, f15_in, U4, f10_in, U5, f9_in, U6, U7, f7_in, U8

Defined Pair Symbols:

F15_IN, F10_IN, F2_IN, F25_IN, F59_IN, U6', F7_IN, F9_IN

Compound Symbols:

c1, c, c4, c7, c14, c16, c1, c13

(37) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(38) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, s(z1)) → U1(f7_in(z0, z1), z0, s(z1))
U1(f7_out1(z0, z1), z2, s(z3)) → f2_out1(z1)
U1(f7_out3(z0), z1, s(z2)) → f2_out1(z0)
f25_in(z0, 0) → f25_out1(z0)
f25_in(s(z0), s(z1)) → U2(f25_in(z0, z1), s(z0), s(z1))
U2(f25_out1(z0), s(z1), s(z2)) → f25_out1(z0)
f59_in(z0, 0) → f59_out1
f59_in(s(z0), s(z1)) → U3(f59_in(z0, z1), s(z0), s(z1))
U3(f59_out1, s(z0), s(z1)) → f59_out1
f15_in(s(z0), z1) → U4(f25_in(z0, z1), s(z0), z1)
U4(f25_out1(z0), s(z1), z2) → f15_out1(z0)
f10_in(s(z0), z1) → U5(f59_in(z0, z1), s(z0), z1)
U5(f59_out1, s(z0), z1) → f10_out2(s(z0))
f9_in(z0, z1) → U6(f15_in(z0, z1), z0, z1)
U6(f15_out1(z0), z1, z2) → U7(f2_in(z0, s(z2)), z1, z2, z0)
U7(f2_out1(z0), z1, z2, z3) → f9_out1(z3, z0)
f7_in(z0, z1) → U8(f9_in(z0, z1), f10_in(z0, z1), z0, z1)
U8(f9_out1(z0, z1), z2, z3, z4) → f7_out1(z0, z1)
U8(z0, f10_out2(z1), z2, z3) → f7_out3(z1)

Tuples:

F15_IN(s(z0), z1) → c1(F25_IN(z0, z1))
F10_IN(s(z0), z1) → c1(F59_IN(z0, z1))
F2_IN(z0, s(z1)) → c(F7_IN(z0, z1))
F25_IN(s(z0), s(z1)) → c4(F25_IN(z0, z1))
F59_IN(s(z0), s(z1)) → c7(F59_IN(z0, z1))
U6'(f15_out1(z0), z1, z2) → c14(F2_IN(z0, s(z2)))
F7_IN(z0, z1) → c16(F9_IN(z0, z1), F10_IN(z0, z1))
F9_IN(s(z0), z1) → c13(U6'(U4(f25_in(z0, z1), s(z0), z1), s(z0), z1), F15_IN(s(z0), z1))

S tuples:

F25_IN(s(z0), s(z1)) → c4(F25_IN(z0, z1))
F59_IN(s(z0), s(z1)) → c7(F59_IN(z0, z1))

K tuples:

U6'(f15_out1(z0), z1, z2) → c14(F2_IN(z0, s(z2)))
F2_IN(z0, s(z1)) → c(F7_IN(z0, z1))
F7_IN(z0, z1) → c16(F9_IN(z0, z1), F10_IN(z0, z1))
F10_IN(s(z0), z1) → c1(F59_IN(z0, z1))
F15_IN(s(z0), z1) → c1(F25_IN(z0, z1))

Defined Rule Symbols:

f2_in, U1, f25_in, U2, f59_in, U3, f15_in, U4, f10_in, U5, f9_in, U6, U7, f7_in, U8

Defined Pair Symbols:

F15_IN, F10_IN, F2_IN, F25_IN, F59_IN, U6', F7_IN, F9_IN

Compound Symbols:

c1, c, c4, c7, c14, c16, c13