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

(0) Obligation:

Clauses:

div(X, s(Y), Z) :- div_s(X, Y, Z).
div_s(0, Y, 0).
div_s(s(X), Y, 0) :- lss(X, Y).
div_s(s(X), Y, s(Z)) :- ','(sub(X, Y, R), div_s(R, Y, Z)).
lss(s(X), s(Y)) :- lss(X, Y).
lss(0, s(Y)).
sub(s(X), s(Y), Z) :- sub(X, Y, Z).
sub(X, 0, X).

Query: div(g,g,a)

(1) LPReorderTransformerProof (EQUIVALENT transformation)

Reordered facts before rules in definite LP [PROLOG].

(2) Obligation:

Clauses:

div_s(0, Y, 0).
lss(0, s(Y)).
sub(X, 0, X).
div(X, s(Y), Z) :- div_s(X, Y, Z).
div_s(s(X), Y, 0) :- lss(X, Y).
div_s(s(X), Y, s(Z)) :- ','(sub(X, Y, R), div_s(R, Y, Z)).
lss(s(X), s(Y)) :- lss(X, Y).
sub(s(X), s(Y), Z) :- sub(X, Y, Z).

Query: div(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];
2 [label="2: div(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
3 [label="3: div(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: div_s(T10, T11, T13)\n\nT10 is ground\nT11 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: div_s(T10, T11, T13), SCOPE: 2, CLAUSE: 0 | div_s(T10, T11, T13), SCOPE: 2, CLAUSE: 4 | div_s(T10, T11, T13), SCOPE: 2, CLAUSE: 5\n\nT10 is ground\nT11 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: true | div_s(0, T18, T13), SCOPE: 2, CLAUSE: 4 | div_s(0, T18, T13), SCOPE: 2, CLAUSE: 5\n\nT18 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: div_s(T10, T11, T13), SCOPE: 2, CLAUSE: 4 | div_s(T10, T11, T13), SCOPE: 2, CLAUSE: 5\n\nT10 is ground\nT11 is ground\nX14 is free\ndiv_s(T10, T11, T13) !=? div_s(0, X14, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: div_s(0, T18, T13), SCOPE: 2, CLAUSE: 4 | div_s(0, T18, T13), SCOPE: 2, CLAUSE: 5\n\nT18 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: div_s(0, T18, T13), SCOPE: 2, CLAUSE: 5\n\nT18 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: div_s(T10, T11, T13), SCOPE: 2, CLAUSE: 4\n\nT10 is ground\nT11 is ground\nX14 is free\ndiv_s(T10, T11, T13) !=? div_s(0, X14, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: div_s(T10, T11, T13), SCOPE: 2, CLAUSE: 5\n\nT10 is ground\nT11 is ground\nX14 is free\ndiv_s(T10, T11, T13) !=? div_s(0, X14, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: lss(T27, T28)\n\nT27 is ground\nT28 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: lss(T27, T28), SCOPE: 3, CLAUSE: 1 | lss(T27, T28), SCOPE: 3, CLAUSE: 6\n\nT27 is ground\nT28 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: true | lss(0, s(T33)), SCOPE: 3, CLAUSE: 6\n\nT33 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: lss(T27, T28), SCOPE: 3, CLAUSE: 6\n\nT27 is ground\nT28 is ground\nX34 is free\nlss(T27, T28) !=? lss(0, s(X34))", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: lss(0, s(T33)), SCOPE: 3, CLAUSE: 6\n\nT33 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: lss(T38, T39)\n\nT38 is ground\nT39 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: ','(sub(T48, T49, X55), div_s(X55, T49, T51))\n\nT48 is ground\nT49 is ground\nX55 is free", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: sub(T48, T49, X55)\n\nT48 is ground\nT49 is ground\nX55 is free", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: div_s(T54, T49, T51)\n\nT49 is ground\nT54 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: sub(T48, T49, X55), SCOPE: 4, CLAUSE: 2 | sub(T48, T49, X55), SCOPE: 4, CLAUSE: 7\n\nT48 is ground\nT49 is ground\nX55 is free", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: true | sub(T59, 0, X55), SCOPE: 4, CLAUSE: 7\n\nT59 is ground\nX55 is free", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: sub(T48, T49, X55), SCOPE: 4, CLAUSE: 7\n\nT48 is ground\nT49 is ground\nX55 is free\nX62 is free\nsub(T48, T49, X55) !=? sub(X62, 0, X62)", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: sub(T59, 0, X55), SCOPE: 4, CLAUSE: 7\n\nT59 is ground\nX55 is free", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: sub(T65, T66, X77)\n\nT65 is ground\nT66 is ground\nX77 is free", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 58 [arrowhead = none ];
58 -> 3;

59 [label="EVAL with clause\ndiv(X7, s(X8), X9) :- div_s(X7, X8, X9).\nand substitutionT1 -> T10,\nX7 -> T10,\nX8 -> T11,\nT2 -> s(T11),\nT3 -> T13,\nX9 -> T13,\nT12 -> T13", fontsize=14, style = filled, fillcolor = lightblue];
3 -> 59 [arrowhead = none ];
59 -> 5;

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

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

62 [label="EVAL with clause\ndiv_s(0, X14, 0).\nand substitutionT10 -> 0,\nT11 -> T18,\nX14 -> T18,\nT13 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 62 [arrowhead = none ];
62 -> 16;

63 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
15 -> 63 [arrowhead = none ];
63 -> 17;

64 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
16 -> 64 [arrowhead = none ];
64 -> 19;

65 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
17 -> 65 [arrowhead = none ];
65 -> 23;

66 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
17 -> 66 [arrowhead = none ];
66 -> 24;

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

68 [label="BACKTRACK\nfor clause: div_s(s(X), Y, s(Z)) :- ','(sub(X, Y, R), div_s(R, Y, Z))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
20 -> 68 [arrowhead = none ];
68 -> 22;

69 [label="EVAL with clause\ndiv_s(s(X28), X29, 0) :- lss(X28, X29).\nand substitutionX28 -> T27,\nT10 -> s(T27),\nT11 -> T28,\nX29 -> T28,\nT13 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
23 -> 69 [arrowhead = none ];
69 -> 27;

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

71 [label="EVAL with clause\ndiv_s(s(X52), X53, s(X54)) :- ','(sub(X52, X53, X55), div_s(X55, X53, X54)).\nand substitutionX52 -> T48,\nT10 -> s(T48),\nT11 -> T49,\nX53 -> T49,\nX54 -> T51,\nT13 -> s(T51),\nT50 -> T51", fontsize=14, style = filled, fillcolor = lightblue];
24 -> 71 [arrowhead = none ];
71 -> 43;

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

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

74 [label="EVAL with clause\nlss(0, s(X34)).\nand substitutionT27 -> 0,\nX34 -> T33,\nT28 -> s(T33)", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 74 [arrowhead = none ];
74 -> 34;

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

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

77 [label="EVAL with clause\nlss(s(X41), s(X42)) :- lss(X41, X42).\nand substitutionX41 -> T38,\nT27 -> s(T38),\nX42 -> T39,\nT28 -> s(T39)", fontsize=14, style = filled, fillcolor = lightblue];
36 -> 77 [arrowhead = none ];
77 -> 40;

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

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

80 [label="INSTANCE with matching:\nT27 -> T38\nT28 -> T39", fontsize=14, style = filled, fillcolor = lightgrey];
40 -> 80 [arrowhead = none , style=dashed];
80 -> 27[style=dashed];

81 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
43 -> 81 [arrowhead = none ];
81 -> 47;

82 [label="SPLIT 2\nnew knowledge:\nT48 is ground\nT49 is ground\nT54 is ground\nreplacements:X55 -> T54", fontsize=14, style = filled, fillcolor = violet];
43 -> 82 [arrowhead = none ];
82 -> 48;

83 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
47 -> 83 [arrowhead = none ];
83 -> 51;

84 [label="INSTANCE with matching:\nT10 -> T54\nT11 -> T49\nT13 -> T51", fontsize=14, style = filled, fillcolor = lightgrey];
48 -> 84 [arrowhead = none , style=dashed];
84 -> 5[style=dashed];

85 [label="EVAL with clause\nsub(X62, 0, X62).\nand substitutionT48 -> T59,\nX62 -> T59,\nT49 -> 0,\nX55 -> T59", fontsize=14, style = filled, fillcolor = lightblue];
51 -> 85 [arrowhead = none ];
85 -> 52;

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

87 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
52 -> 87 [arrowhead = none ];
87 -> 54;

88 [label="EVAL with clause\nsub(s(X74), s(X75), X76) :- sub(X74, X75, X76).\nand substitutionX74 -> T65,\nT48 -> s(T65),\nX75 -> T66,\nT49 -> s(T66),\nX55 -> X77,\nX76 -> X77", fontsize=14, style = filled, fillcolor = lightblue];
53 -> 88 [arrowhead = none ];
88 -> 56;

89 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
53 -> 89 [arrowhead = none ];
89 -> 57;

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

91 [label="INSTANCE with matching:\nT48 -> T65\nT49 -> T66\nX55 -> X77", fontsize=14, style = filled, fillcolor = lightgrey];
56 -> 91 [arrowhead = none , style=dashed];
91 -> 47[style=dashed];

}

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, s(z1)) → U1(f5_in(z0, z1), z0, s(z1))
U1(f5_out1(z0), z1, s(z2)) → f2_out1(z0)
f5_in(0, z0) → f5_out1(0)
f5_in(z0, z1) → U2(f17_in(z0, z1), z0, z1)
U2(f17_out1(z0), z1, z2) → f5_out1(z0)
U2(f17_out2(z0), z1, z2) → f5_out1(z0)
f27_in(0, s(z0)) → f27_out1
f27_in(s(z0), s(z1)) → U3(f27_in(z0, z1), s(z0), s(z1))
U3(f27_out1, s(z0), s(z1)) → f27_out1
f47_in(z0, 0) → f47_out1(z0)
f47_in(s(z0), s(z1)) → U4(f47_in(z0, z1), s(z0), s(z1))
U4(f47_out1(z0), s(z1), s(z2)) → f47_out1(z0)
f23_in(s(z0), z1) → U5(f27_in(z0, z1), s(z0), z1)
U5(f27_out1, s(z0), z1) → f23_out1(0)
f24_in(s(z0), z1) → U6(f43_in(z0, z1), s(z0), z1)
U6(f43_out1(z0, z1), s(z2), z3) → f24_out1(s(z1))
f43_in(z0, z1) → U7(f47_in(z0, z1), z0, z1)
U7(f47_out1(z0), z1, z2) → U8(f5_in(z0, z2), z1, z2, z0)
U8(f5_out1(z0), z1, z2, z3) → f43_out1(z3, z0)
f17_in(z0, z1) → U9(f23_in(z0, z1), f24_in(z0, z1), z0, z1)
U9(f23_out1(z0), z1, z2, z3) → f17_out1(z0)
U9(z0, f24_out1(z1), z2, z3) → f17_out2(z1)

Tuples:

F2_IN(z0, s(z1)) → c(U1'(f5_in(z0, z1), z0, s(z1)), F5_IN(z0, z1))
F5_IN(z0, z1) → c3(U2'(f17_in(z0, z1), z0, z1), F17_IN(z0, z1))
F27_IN(s(z0), s(z1)) → c7(U3'(f27_in(z0, z1), s(z0), s(z1)), F27_IN(z0, z1))
F47_IN(s(z0), s(z1)) → c10(U4'(f47_in(z0, z1), s(z0), s(z1)), F47_IN(z0, z1))
F23_IN(s(z0), z1) → c12(U5'(f27_in(z0, z1), s(z0), z1), F27_IN(z0, z1))
F24_IN(s(z0), z1) → c14(U6'(f43_in(z0, z1), s(z0), z1), F43_IN(z0, z1))
F43_IN(z0, z1) → c16(U7'(f47_in(z0, z1), z0, z1), F47_IN(z0, z1))
U7'(f47_out1(z0), z1, z2) → c17(U8'(f5_in(z0, z2), z1, z2, z0), F5_IN(z0, z2))
F17_IN(z0, z1) → c19(U9'(f23_in(z0, z1), f24_in(z0, z1), z0, z1), F23_IN(z0, z1), F24_IN(z0, z1))

S tuples:

F2_IN(z0, s(z1)) → c(U1'(f5_in(z0, z1), z0, s(z1)), F5_IN(z0, z1))
F5_IN(z0, z1) → c3(U2'(f17_in(z0, z1), z0, z1), F17_IN(z0, z1))
F27_IN(s(z0), s(z1)) → c7(U3'(f27_in(z0, z1), s(z0), s(z1)), F27_IN(z0, z1))
F47_IN(s(z0), s(z1)) → c10(U4'(f47_in(z0, z1), s(z0), s(z1)), F47_IN(z0, z1))
F23_IN(s(z0), z1) → c12(U5'(f27_in(z0, z1), s(z0), z1), F27_IN(z0, z1))
F24_IN(s(z0), z1) → c14(U6'(f43_in(z0, z1), s(z0), z1), F43_IN(z0, z1))
F43_IN(z0, z1) → c16(U7'(f47_in(z0, z1), z0, z1), F47_IN(z0, z1))
U7'(f47_out1(z0), z1, z2) → c17(U8'(f5_in(z0, z2), z1, z2, z0), F5_IN(z0, z2))
F17_IN(z0, z1) → c19(U9'(f23_in(z0, z1), f24_in(z0, z1), z0, z1), F23_IN(z0, z1), F24_IN(z0, z1))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f5_in, U2, f27_in, U3, f47_in, U4, f23_in, U5, f24_in, U6, f43_in, U7, U8, f17_in, U9

Defined Pair Symbols:

F2_IN, F5_IN, F27_IN, F47_IN, F23_IN, F24_IN, F43_IN, U7', F17_IN

Compound Symbols:

c, c3, c7, c10, c12, c14, c16, c17, c19

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

Split RHS of tuples not part of any SCC

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, s(z1)) → U1(f5_in(z0, z1), z0, s(z1))
U1(f5_out1(z0), z1, s(z2)) → f2_out1(z0)
f5_in(0, z0) → f5_out1(0)
f5_in(z0, z1) → U2(f17_in(z0, z1), z0, z1)
U2(f17_out1(z0), z1, z2) → f5_out1(z0)
U2(f17_out2(z0), z1, z2) → f5_out1(z0)
f27_in(0, s(z0)) → f27_out1
f27_in(s(z0), s(z1)) → U3(f27_in(z0, z1), s(z0), s(z1))
U3(f27_out1, s(z0), s(z1)) → f27_out1
f47_in(z0, 0) → f47_out1(z0)
f47_in(s(z0), s(z1)) → U4(f47_in(z0, z1), s(z0), s(z1))
U4(f47_out1(z0), s(z1), s(z2)) → f47_out1(z0)
f23_in(s(z0), z1) → U5(f27_in(z0, z1), s(z0), z1)
U5(f27_out1, s(z0), z1) → f23_out1(0)
f24_in(s(z0), z1) → U6(f43_in(z0, z1), s(z0), z1)
U6(f43_out1(z0, z1), s(z2), z3) → f24_out1(s(z1))
f43_in(z0, z1) → U7(f47_in(z0, z1), z0, z1)
U7(f47_out1(z0), z1, z2) → U8(f5_in(z0, z2), z1, z2, z0)
U8(f5_out1(z0), z1, z2, z3) → f43_out1(z3, z0)
f17_in(z0, z1) → U9(f23_in(z0, z1), f24_in(z0, z1), z0, z1)
U9(f23_out1(z0), z1, z2, z3) → f17_out1(z0)
U9(z0, f24_out1(z1), z2, z3) → f17_out2(z1)

Tuples:

F5_IN(z0, z1) → c3(U2'(f17_in(z0, z1), z0, z1), F17_IN(z0, z1))
F27_IN(s(z0), s(z1)) → c7(U3'(f27_in(z0, z1), s(z0), s(z1)), F27_IN(z0, z1))
F47_IN(s(z0), s(z1)) → c10(U4'(f47_in(z0, z1), s(z0), s(z1)), F47_IN(z0, z1))
F24_IN(s(z0), z1) → c14(U6'(f43_in(z0, z1), s(z0), z1), F43_IN(z0, z1))
F43_IN(z0, z1) → c16(U7'(f47_in(z0, z1), z0, z1), F47_IN(z0, z1))
U7'(f47_out1(z0), z1, z2) → c17(U8'(f5_in(z0, z2), z1, z2, z0), F5_IN(z0, z2))
F17_IN(z0, z1) → c19(U9'(f23_in(z0, z1), f24_in(z0, z1), z0, z1), F23_IN(z0, z1), F24_IN(z0, z1))
F2_IN(z0, s(z1)) → c1(U1'(f5_in(z0, z1), z0, s(z1)))
F2_IN(z0, s(z1)) → c1(F5_IN(z0, z1))
F23_IN(s(z0), z1) → c1(U5'(f27_in(z0, z1), s(z0), z1))
F23_IN(s(z0), z1) → c1(F27_IN(z0, z1))

S tuples:

F5_IN(z0, z1) → c3(U2'(f17_in(z0, z1), z0, z1), F17_IN(z0, z1))
F27_IN(s(z0), s(z1)) → c7(U3'(f27_in(z0, z1), s(z0), s(z1)), F27_IN(z0, z1))
F47_IN(s(z0), s(z1)) → c10(U4'(f47_in(z0, z1), s(z0), s(z1)), F47_IN(z0, z1))
F24_IN(s(z0), z1) → c14(U6'(f43_in(z0, z1), s(z0), z1), F43_IN(z0, z1))
F43_IN(z0, z1) → c16(U7'(f47_in(z0, z1), z0, z1), F47_IN(z0, z1))
U7'(f47_out1(z0), z1, z2) → c17(U8'(f5_in(z0, z2), z1, z2, z0), F5_IN(z0, z2))
F17_IN(z0, z1) → c19(U9'(f23_in(z0, z1), f24_in(z0, z1), z0, z1), F23_IN(z0, z1), F24_IN(z0, z1))
F2_IN(z0, s(z1)) → c1(U1'(f5_in(z0, z1), z0, s(z1)))
F2_IN(z0, s(z1)) → c1(F5_IN(z0, z1))
F23_IN(s(z0), z1) → c1(U5'(f27_in(z0, z1), s(z0), z1))
F23_IN(s(z0), z1) → c1(F27_IN(z0, z1))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f5_in, U2, f27_in, U3, f47_in, U4, f23_in, U5, f24_in, U6, f43_in, U7, U8, f17_in, U9

Defined Pair Symbols:

F5_IN, F27_IN, F47_IN, F24_IN, F43_IN, U7', F17_IN, F2_IN, F23_IN

Compound Symbols:

c3, c7, c10, c14, c16, c17, c19, c1

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

Removed 8 trailing tuple parts

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, s(z1)) → U1(f5_in(z0, z1), z0, s(z1))
U1(f5_out1(z0), z1, s(z2)) → f2_out1(z0)
f5_in(0, z0) → f5_out1(0)
f5_in(z0, z1) → U2(f17_in(z0, z1), z0, z1)
U2(f17_out1(z0), z1, z2) → f5_out1(z0)
U2(f17_out2(z0), z1, z2) → f5_out1(z0)
f27_in(0, s(z0)) → f27_out1
f27_in(s(z0), s(z1)) → U3(f27_in(z0, z1), s(z0), s(z1))
U3(f27_out1, s(z0), s(z1)) → f27_out1
f47_in(z0, 0) → f47_out1(z0)
f47_in(s(z0), s(z1)) → U4(f47_in(z0, z1), s(z0), s(z1))
U4(f47_out1(z0), s(z1), s(z2)) → f47_out1(z0)
f23_in(s(z0), z1) → U5(f27_in(z0, z1), s(z0), z1)
U5(f27_out1, s(z0), z1) → f23_out1(0)
f24_in(s(z0), z1) → U6(f43_in(z0, z1), s(z0), z1)
U6(f43_out1(z0, z1), s(z2), z3) → f24_out1(s(z1))
f43_in(z0, z1) → U7(f47_in(z0, z1), z0, z1)
U7(f47_out1(z0), z1, z2) → U8(f5_in(z0, z2), z1, z2, z0)
U8(f5_out1(z0), z1, z2, z3) → f43_out1(z3, z0)
f17_in(z0, z1) → U9(f23_in(z0, z1), f24_in(z0, z1), z0, z1)
U9(f23_out1(z0), z1, z2, z3) → f17_out1(z0)
U9(z0, f24_out1(z1), z2, z3) → f17_out2(z1)

Tuples:

F43_IN(z0, z1) → c16(U7'(f47_in(z0, z1), z0, z1), F47_IN(z0, z1))
F2_IN(z0, s(z1)) → c1(F5_IN(z0, z1))
F23_IN(s(z0), z1) → c1(F27_IN(z0, z1))
F5_IN(z0, z1) → c3(F17_IN(z0, z1))
F27_IN(s(z0), s(z1)) → c7(F27_IN(z0, z1))
F47_IN(s(z0), s(z1)) → c10(F47_IN(z0, z1))
F24_IN(s(z0), z1) → c14(F43_IN(z0, z1))
U7'(f47_out1(z0), z1, z2) → c17(F5_IN(z0, z2))
F17_IN(z0, z1) → c19(F23_IN(z0, z1), F24_IN(z0, z1))
F2_IN(z0, s(z1)) → c1
F23_IN(s(z0), z1) → c1

S tuples:

F43_IN(z0, z1) → c16(U7'(f47_in(z0, z1), z0, z1), F47_IN(z0, z1))
F2_IN(z0, s(z1)) → c1(F5_IN(z0, z1))
F23_IN(s(z0), z1) → c1(F27_IN(z0, z1))
F5_IN(z0, z1) → c3(F17_IN(z0, z1))
F27_IN(s(z0), s(z1)) → c7(F27_IN(z0, z1))
F47_IN(s(z0), s(z1)) → c10(F47_IN(z0, z1))
F24_IN(s(z0), z1) → c14(F43_IN(z0, z1))
U7'(f47_out1(z0), z1, z2) → c17(F5_IN(z0, z2))
F17_IN(z0, z1) → c19(F23_IN(z0, z1), F24_IN(z0, z1))
F2_IN(z0, s(z1)) → c1
F23_IN(s(z0), z1) → c1

K tuples:none
Defined Rule Symbols:

f2_in, U1, f5_in, U2, f27_in, U3, f47_in, U4, f23_in, U5, f24_in, U6, f43_in, U7, U8, f17_in, U9

Defined Pair Symbols:

F43_IN, F2_IN, F23_IN, F5_IN, F27_IN, F47_IN, F24_IN, U7', F17_IN

Compound Symbols:

c16, c1, c3, c7, c10, c14, c17, c19, c1

(9) CdtKnowledgeProof (EQUIVALENT transformation)

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

F2_IN(z0, s(z1)) → c1(F5_IN(z0, z1))
F2_IN(z0, s(z1)) → c1

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, s(z1)) → U1(f5_in(z0, z1), z0, s(z1))
U1(f5_out1(z0), z1, s(z2)) → f2_out1(z0)
f5_in(0, z0) → f5_out1(0)
f5_in(z0, z1) → U2(f17_in(z0, z1), z0, z1)
U2(f17_out1(z0), z1, z2) → f5_out1(z0)
U2(f17_out2(z0), z1, z2) → f5_out1(z0)
f27_in(0, s(z0)) → f27_out1
f27_in(s(z0), s(z1)) → U3(f27_in(z0, z1), s(z0), s(z1))
U3(f27_out1, s(z0), s(z1)) → f27_out1
f47_in(z0, 0) → f47_out1(z0)
f47_in(s(z0), s(z1)) → U4(f47_in(z0, z1), s(z0), s(z1))
U4(f47_out1(z0), s(z1), s(z2)) → f47_out1(z0)
f23_in(s(z0), z1) → U5(f27_in(z0, z1), s(z0), z1)
U5(f27_out1, s(z0), z1) → f23_out1(0)
f24_in(s(z0), z1) → U6(f43_in(z0, z1), s(z0), z1)
U6(f43_out1(z0, z1), s(z2), z3) → f24_out1(s(z1))
f43_in(z0, z1) → U7(f47_in(z0, z1), z0, z1)
U7(f47_out1(z0), z1, z2) → U8(f5_in(z0, z2), z1, z2, z0)
U8(f5_out1(z0), z1, z2, z3) → f43_out1(z3, z0)
f17_in(z0, z1) → U9(f23_in(z0, z1), f24_in(z0, z1), z0, z1)
U9(f23_out1(z0), z1, z2, z3) → f17_out1(z0)
U9(z0, f24_out1(z1), z2, z3) → f17_out2(z1)

Tuples:

F43_IN(z0, z1) → c16(U7'(f47_in(z0, z1), z0, z1), F47_IN(z0, z1))
F2_IN(z0, s(z1)) → c1(F5_IN(z0, z1))
F23_IN(s(z0), z1) → c1(F27_IN(z0, z1))
F5_IN(z0, z1) → c3(F17_IN(z0, z1))
F27_IN(s(z0), s(z1)) → c7(F27_IN(z0, z1))
F47_IN(s(z0), s(z1)) → c10(F47_IN(z0, z1))
F24_IN(s(z0), z1) → c14(F43_IN(z0, z1))
U7'(f47_out1(z0), z1, z2) → c17(F5_IN(z0, z2))
F17_IN(z0, z1) → c19(F23_IN(z0, z1), F24_IN(z0, z1))
F2_IN(z0, s(z1)) → c1
F23_IN(s(z0), z1) → c1

S tuples:

F43_IN(z0, z1) → c16(U7'(f47_in(z0, z1), z0, z1), F47_IN(z0, z1))
F23_IN(s(z0), z1) → c1(F27_IN(z0, z1))
F5_IN(z0, z1) → c3(F17_IN(z0, z1))
F27_IN(s(z0), s(z1)) → c7(F27_IN(z0, z1))
F47_IN(s(z0), s(z1)) → c10(F47_IN(z0, z1))
F24_IN(s(z0), z1) → c14(F43_IN(z0, z1))
U7'(f47_out1(z0), z1, z2) → c17(F5_IN(z0, z2))
F17_IN(z0, z1) → c19(F23_IN(z0, z1), F24_IN(z0, z1))
F23_IN(s(z0), z1) → c1

K tuples:

F2_IN(z0, s(z1)) → c1(F5_IN(z0, z1))
F2_IN(z0, s(z1)) → c1

Defined Rule Symbols:

f2_in, U1, f5_in, U2, f27_in, U3, f47_in, U4, f23_in, U5, f24_in, U6, f43_in, U7, U8, f17_in, U9

Defined Pair Symbols:

F43_IN, F2_IN, F23_IN, F5_IN, F27_IN, F47_IN, F24_IN, U7', F17_IN

Compound Symbols:

c16, c1, c3, c7, c10, c14, c17, c19, c1

(11) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

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

F24_IN(s(z0), z1) → c14(F43_IN(z0, z1))

We considered the (Usable) Rules:

f47_in(z0, 0) → f47_out1(z0)
f47_in(s(z0), s(z1)) → U4(f47_in(z0, z1), s(z0), s(z1))
U4(f47_out1(z0), s(z1), s(z2)) → f47_out1(z0)

And the Tuples:

F43_IN(z0, z1) → c16(U7'(f47_in(z0, z1), z0, z1), F47_IN(z0, z1))
F2_IN(z0, s(z1)) → c1(F5_IN(z0, z1))
F23_IN(s(z0), z1) → c1(F27_IN(z0, z1))
F5_IN(z0, z1) → c3(F17_IN(z0, z1))
F27_IN(s(z0), s(z1)) → c7(F27_IN(z0, z1))
F47_IN(s(z0), s(z1)) → c10(F47_IN(z0, z1))
F24_IN(s(z0), z1) → c14(F43_IN(z0, z1))
U7'(f47_out1(z0), z1, z2) → c17(F5_IN(z0, z2))
F17_IN(z0, z1) → c19(F23_IN(z0, z1), F24_IN(z0, z1))
F2_IN(z0, s(z1)) → c1
F23_IN(s(z0), z1) → c1

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

POL(0) = 0   
POL(F17_IN(x₁, x₂)) = x₁   
POL(F23_IN(x₁, x₂)) = 0   
POL(F24_IN(x₁, x₂)) = x₁   
POL(F27_IN(x₁, x₂)) = 0   
POL(F2_IN(x₁, x₂)) = [2] + [2]x₁ + [2]x₂   
POL(F43_IN(x₁, x₂)) = x₁   
POL(F47_IN(x₁, x₂)) = 0   
POL(F5_IN(x₁, x₂)) = x₁   
POL(U4(x₁, x₂, x₃)) = x₁   
POL(U7'(x₁, x₂, x₃)) = x₁   
POL(c1) = 0   
POL(c1(x₁)) = x₁   
POL(c10(x₁)) = x₁   
POL(c14(x₁)) = x₁   
POL(c16(x₁, x₂)) = x₁ + x₂   
POL(c17(x₁)) = x₁   
POL(c19(x₁, x₂)) = x₁ + x₂   
POL(c3(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(f47_in(x₁, x₂)) = x₁   
POL(f47_out1(x₁)) = x₁   
POL(s(x₁)) = [1] + x₁   

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, s(z1)) → U1(f5_in(z0, z1), z0, s(z1))
U1(f5_out1(z0), z1, s(z2)) → f2_out1(z0)
f5_in(0, z0) → f5_out1(0)
f5_in(z0, z1) → U2(f17_in(z0, z1), z0, z1)
U2(f17_out1(z0), z1, z2) → f5_out1(z0)
U2(f17_out2(z0), z1, z2) → f5_out1(z0)
f27_in(0, s(z0)) → f27_out1
f27_in(s(z0), s(z1)) → U3(f27_in(z0, z1), s(z0), s(z1))
U3(f27_out1, s(z0), s(z1)) → f27_out1
f47_in(z0, 0) → f47_out1(z0)
f47_in(s(z0), s(z1)) → U4(f47_in(z0, z1), s(z0), s(z1))
U4(f47_out1(z0), s(z1), s(z2)) → f47_out1(z0)
f23_in(s(z0), z1) → U5(f27_in(z0, z1), s(z0), z1)
U5(f27_out1, s(z0), z1) → f23_out1(0)
f24_in(s(z0), z1) → U6(f43_in(z0, z1), s(z0), z1)
U6(f43_out1(z0, z1), s(z2), z3) → f24_out1(s(z1))
f43_in(z0, z1) → U7(f47_in(z0, z1), z0, z1)
U7(f47_out1(z0), z1, z2) → U8(f5_in(z0, z2), z1, z2, z0)
U8(f5_out1(z0), z1, z2, z3) → f43_out1(z3, z0)
f17_in(z0, z1) → U9(f23_in(z0, z1), f24_in(z0, z1), z0, z1)
U9(f23_out1(z0), z1, z2, z3) → f17_out1(z0)
U9(z0, f24_out1(z1), z2, z3) → f17_out2(z1)

Tuples:

F43_IN(z0, z1) → c16(U7'(f47_in(z0, z1), z0, z1), F47_IN(z0, z1))
F2_IN(z0, s(z1)) → c1(F5_IN(z0, z1))
F23_IN(s(z0), z1) → c1(F27_IN(z0, z1))
F5_IN(z0, z1) → c3(F17_IN(z0, z1))
F27_IN(s(z0), s(z1)) → c7(F27_IN(z0, z1))
F47_IN(s(z0), s(z1)) → c10(F47_IN(z0, z1))
F24_IN(s(z0), z1) → c14(F43_IN(z0, z1))
U7'(f47_out1(z0), z1, z2) → c17(F5_IN(z0, z2))
F17_IN(z0, z1) → c19(F23_IN(z0, z1), F24_IN(z0, z1))
F2_IN(z0, s(z1)) → c1
F23_IN(s(z0), z1) → c1

S tuples:

F43_IN(z0, z1) → c16(U7'(f47_in(z0, z1), z0, z1), F47_IN(z0, z1))
F23_IN(s(z0), z1) → c1(F27_IN(z0, z1))
F5_IN(z0, z1) → c3(F17_IN(z0, z1))
F27_IN(s(z0), s(z1)) → c7(F27_IN(z0, z1))
F47_IN(s(z0), s(z1)) → c10(F47_IN(z0, z1))
U7'(f47_out1(z0), z1, z2) → c17(F5_IN(z0, z2))
F17_IN(z0, z1) → c19(F23_IN(z0, z1), F24_IN(z0, z1))
F23_IN(s(z0), z1) → c1

K tuples:

F2_IN(z0, s(z1)) → c1(F5_IN(z0, z1))
F2_IN(z0, s(z1)) → c1
F24_IN(s(z0), z1) → c14(F43_IN(z0, z1))

Defined Rule Symbols:

f2_in, U1, f5_in, U2, f27_in, U3, f47_in, U4, f23_in, U5, f24_in, U6, f43_in, U7, U8, f17_in, U9

Defined Pair Symbols:

F43_IN, F2_IN, F23_IN, F5_IN, F27_IN, F47_IN, F24_IN, U7', F17_IN

Compound Symbols:

c16, c1, c3, c7, c10, c14, c17, c19, c1

(13) CdtKnowledgeProof (EQUIVALENT transformation)

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

F43_IN(z0, z1) → c16(U7'(f47_in(z0, z1), z0, z1), F47_IN(z0, z1))
U7'(f47_out1(z0), z1, z2) → c17(F5_IN(z0, z2))
U7'(f47_out1(z0), z1, z2) → c17(F5_IN(z0, z2))
F5_IN(z0, z1) → c3(F17_IN(z0, z1))
F17_IN(z0, z1) → c19(F23_IN(z0, z1), F24_IN(z0, z1))
F23_IN(s(z0), z1) → c1(F27_IN(z0, z1))
F24_IN(s(z0), z1) → c14(F43_IN(z0, z1))
F23_IN(s(z0), z1) → c1

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, s(z1)) → U1(f5_in(z0, z1), z0, s(z1))
U1(f5_out1(z0), z1, s(z2)) → f2_out1(z0)
f5_in(0, z0) → f5_out1(0)
f5_in(z0, z1) → U2(f17_in(z0, z1), z0, z1)
U2(f17_out1(z0), z1, z2) → f5_out1(z0)
U2(f17_out2(z0), z1, z2) → f5_out1(z0)
f27_in(0, s(z0)) → f27_out1
f27_in(s(z0), s(z1)) → U3(f27_in(z0, z1), s(z0), s(z1))
U3(f27_out1, s(z0), s(z1)) → f27_out1
f47_in(z0, 0) → f47_out1(z0)
f47_in(s(z0), s(z1)) → U4(f47_in(z0, z1), s(z0), s(z1))
U4(f47_out1(z0), s(z1), s(z2)) → f47_out1(z0)
f23_in(s(z0), z1) → U5(f27_in(z0, z1), s(z0), z1)
U5(f27_out1, s(z0), z1) → f23_out1(0)
f24_in(s(z0), z1) → U6(f43_in(z0, z1), s(z0), z1)
U6(f43_out1(z0, z1), s(z2), z3) → f24_out1(s(z1))
f43_in(z0, z1) → U7(f47_in(z0, z1), z0, z1)
U7(f47_out1(z0), z1, z2) → U8(f5_in(z0, z2), z1, z2, z0)
U8(f5_out1(z0), z1, z2, z3) → f43_out1(z3, z0)
f17_in(z0, z1) → U9(f23_in(z0, z1), f24_in(z0, z1), z0, z1)
U9(f23_out1(z0), z1, z2, z3) → f17_out1(z0)
U9(z0, f24_out1(z1), z2, z3) → f17_out2(z1)

Tuples:

F43_IN(z0, z1) → c16(U7'(f47_in(z0, z1), z0, z1), F47_IN(z0, z1))
F2_IN(z0, s(z1)) → c1(F5_IN(z0, z1))
F23_IN(s(z0), z1) → c1(F27_IN(z0, z1))
F5_IN(z0, z1) → c3(F17_IN(z0, z1))
F27_IN(s(z0), s(z1)) → c7(F27_IN(z0, z1))
F47_IN(s(z0), s(z1)) → c10(F47_IN(z0, z1))
F24_IN(s(z0), z1) → c14(F43_IN(z0, z1))
U7'(f47_out1(z0), z1, z2) → c17(F5_IN(z0, z2))
F17_IN(z0, z1) → c19(F23_IN(z0, z1), F24_IN(z0, z1))
F2_IN(z0, s(z1)) → c1
F23_IN(s(z0), z1) → c1

S tuples:

F27_IN(s(z0), s(z1)) → c7(F27_IN(z0, z1))
F47_IN(s(z0), s(z1)) → c10(F47_IN(z0, z1))

K tuples:

F2_IN(z0, s(z1)) → c1(F5_IN(z0, z1))
F2_IN(z0, s(z1)) → c1
F24_IN(s(z0), z1) → c14(F43_IN(z0, z1))
F43_IN(z0, z1) → c16(U7'(f47_in(z0, z1), z0, z1), F47_IN(z0, z1))
U7'(f47_out1(z0), z1, z2) → c17(F5_IN(z0, z2))
F5_IN(z0, z1) → c3(F17_IN(z0, z1))
F17_IN(z0, z1) → c19(F23_IN(z0, z1), F24_IN(z0, z1))
F23_IN(s(z0), z1) → c1(F27_IN(z0, z1))
F23_IN(s(z0), z1) → c1

Defined Rule Symbols:

f2_in, U1, f5_in, U2, f27_in, U3, f47_in, U4, f23_in, U5, f24_in, U6, f43_in, U7, U8, f17_in, U9

Defined Pair Symbols:

F43_IN, F2_IN, F23_IN, F5_IN, F27_IN, F47_IN, F24_IN, U7', F17_IN

Compound Symbols:

c16, c1, c3, c7, c10, c14, c17, c19, c1

(15) 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))

We considered the (Usable) Rules:

f47_in(z0, 0) → f47_out1(z0)
f47_in(s(z0), s(z1)) → U4(f47_in(z0, z1), s(z0), s(z1))
U4(f47_out1(z0), s(z1), s(z2)) → f47_out1(z0)

And the Tuples:

F43_IN(z0, z1) → c16(U7'(f47_in(z0, z1), z0, z1), F47_IN(z0, z1))
F2_IN(z0, s(z1)) → c1(F5_IN(z0, z1))
F23_IN(s(z0), z1) → c1(F27_IN(z0, z1))
F5_IN(z0, z1) → c3(F17_IN(z0, z1))
F27_IN(s(z0), s(z1)) → c7(F27_IN(z0, z1))
F47_IN(s(z0), s(z1)) → c10(F47_IN(z0, z1))
F24_IN(s(z0), z1) → c14(F43_IN(z0, z1))
U7'(f47_out1(z0), z1, z2) → c17(F5_IN(z0, z2))
F17_IN(z0, z1) → c19(F23_IN(z0, z1), F24_IN(z0, z1))
F2_IN(z0, s(z1)) → c1
F23_IN(s(z0), z1) → c1

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

POL(0) = 0   
POL(F17_IN(x₁, x₂)) = x₁ + x₂ + x₁²   
POL(F23_IN(x₁, x₂)) = x₁   
POL(F24_IN(x₁, x₂)) = x₂ + x₁²   
POL(F27_IN(x₁, x₂)) = [1] + x₁   
POL(F2_IN(x₁, x₂)) = [1] + x₂ + x₂² + x₁·x₂ + x₁²   
POL(F43_IN(x₁, x₂)) = [1] + x₁ + x₂ + x₁²   
POL(F47_IN(x₁, x₂)) = 0   
POL(F5_IN(x₁, x₂)) = x₁ + x₂ + x₁²   
POL(U4(x₁, x₂, x₃)) = x₁   
POL(U7'(x₁, x₂, x₃)) = x₁ + x₃ + x₁²   
POL(c1) = 0   
POL(c1(x₁)) = x₁   
POL(c10(x₁)) = x₁   
POL(c14(x₁)) = x₁   
POL(c16(x₁, x₂)) = x₁ + x₂   
POL(c17(x₁)) = x₁   
POL(c19(x₁, x₂)) = x₁ + x₂   
POL(c3(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(f47_in(x₁, x₂)) = x₁   
POL(f47_out1(x₁)) = x₁   
POL(s(x₁)) = [1] + x₁   

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, s(z1)) → U1(f5_in(z0, z1), z0, s(z1))
U1(f5_out1(z0), z1, s(z2)) → f2_out1(z0)
f5_in(0, z0) → f5_out1(0)
f5_in(z0, z1) → U2(f17_in(z0, z1), z0, z1)
U2(f17_out1(z0), z1, z2) → f5_out1(z0)
U2(f17_out2(z0), z1, z2) → f5_out1(z0)
f27_in(0, s(z0)) → f27_out1
f27_in(s(z0), s(z1)) → U3(f27_in(z0, z1), s(z0), s(z1))
U3(f27_out1, s(z0), s(z1)) → f27_out1
f47_in(z0, 0) → f47_out1(z0)
f47_in(s(z0), s(z1)) → U4(f47_in(z0, z1), s(z0), s(z1))
U4(f47_out1(z0), s(z1), s(z2)) → f47_out1(z0)
f23_in(s(z0), z1) → U5(f27_in(z0, z1), s(z0), z1)
U5(f27_out1, s(z0), z1) → f23_out1(0)
f24_in(s(z0), z1) → U6(f43_in(z0, z1), s(z0), z1)
U6(f43_out1(z0, z1), s(z2), z3) → f24_out1(s(z1))
f43_in(z0, z1) → U7(f47_in(z0, z1), z0, z1)
U7(f47_out1(z0), z1, z2) → U8(f5_in(z0, z2), z1, z2, z0)
U8(f5_out1(z0), z1, z2, z3) → f43_out1(z3, z0)
f17_in(z0, z1) → U9(f23_in(z0, z1), f24_in(z0, z1), z0, z1)
U9(f23_out1(z0), z1, z2, z3) → f17_out1(z0)
U9(z0, f24_out1(z1), z2, z3) → f17_out2(z1)

Tuples:

F43_IN(z0, z1) → c16(U7'(f47_in(z0, z1), z0, z1), F47_IN(z0, z1))
F2_IN(z0, s(z1)) → c1(F5_IN(z0, z1))
F23_IN(s(z0), z1) → c1(F27_IN(z0, z1))
F5_IN(z0, z1) → c3(F17_IN(z0, z1))
F27_IN(s(z0), s(z1)) → c7(F27_IN(z0, z1))
F47_IN(s(z0), s(z1)) → c10(F47_IN(z0, z1))
F24_IN(s(z0), z1) → c14(F43_IN(z0, z1))
U7'(f47_out1(z0), z1, z2) → c17(F5_IN(z0, z2))
F17_IN(z0, z1) → c19(F23_IN(z0, z1), F24_IN(z0, z1))
F2_IN(z0, s(z1)) → c1
F23_IN(s(z0), z1) → c1

S tuples:

F47_IN(s(z0), s(z1)) → c10(F47_IN(z0, z1))

K tuples:

F2_IN(z0, s(z1)) → c1(F5_IN(z0, z1))
F2_IN(z0, s(z1)) → c1
F24_IN(s(z0), z1) → c14(F43_IN(z0, z1))
F43_IN(z0, z1) → c16(U7'(f47_in(z0, z1), z0, z1), F47_IN(z0, z1))
U7'(f47_out1(z0), z1, z2) → c17(F5_IN(z0, z2))
F5_IN(z0, z1) → c3(F17_IN(z0, z1))
F17_IN(z0, z1) → c19(F23_IN(z0, z1), F24_IN(z0, z1))
F23_IN(s(z0), z1) → c1(F27_IN(z0, z1))
F23_IN(s(z0), z1) → c1
F27_IN(s(z0), s(z1)) → c7(F27_IN(z0, z1))

Defined Rule Symbols:

f2_in, U1, f5_in, U2, f27_in, U3, f47_in, U4, f23_in, U5, f24_in, U6, f43_in, U7, U8, f17_in, U9

Defined Pair Symbols:

F43_IN, F2_IN, F23_IN, F5_IN, F27_IN, F47_IN, F24_IN, U7', F17_IN

Compound Symbols:

c16, c1, c3, c7, c10, c14, c17, c19, c1

(17) 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: div(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: div(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: div_s(T7, T8, T10)\n\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: div_s(T7, T8, T10), SCOPE: 2, CLAUSE: 0 | div_s(T7, T8, T10), SCOPE: 2, CLAUSE: 4 | div_s(T7, T8, T10), SCOPE: 2, CLAUSE: 5\n\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: true | div_s(0, T13, T10), SCOPE: 2, CLAUSE: 4 | div_s(0, T13, T10), SCOPE: 2, CLAUSE: 5\n\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: div_s(T7, T8, T10), SCOPE: 2, CLAUSE: 4 | div_s(T7, T8, T10), SCOPE: 2, CLAUSE: 5\n\nT7 is ground\nT8 is ground\nX9 is free\ndiv_s(T7, T8, T10) !=? div_s(0, X9, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: div_s(0, T13, T10), SCOPE: 2, CLAUSE: 4 | div_s(0, T13, T10), SCOPE: 2, CLAUSE: 5\n\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: div_s(0, T13, T10), SCOPE: 2, CLAUSE: 5\n\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: div_s(T7, T8, T10), SCOPE: 2, CLAUSE: 4\n\nT7 is ground\nT8 is ground\nX9 is free\ndiv_s(T7, T8, T10) !=? div_s(0, X9, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: div_s(T7, T8, T10), SCOPE: 2, CLAUSE: 5\n\nT7 is ground\nT8 is ground\nX9 is free\ndiv_s(T7, T8, T10) !=? div_s(0, X9, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: lss(T22, T23)\n\nT22 is ground\nT23 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: lss(T22, T23), SCOPE: 3, CLAUSE: 1 | lss(T22, T23), SCOPE: 3, CLAUSE: 6\n\nT22 is ground\nT23 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: true | lss(0, s(T28)), SCOPE: 3, CLAUSE: 6\n\nT28 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: lss(T22, T23), SCOPE: 3, CLAUSE: 6\n\nT22 is ground\nT23 is ground\nX29 is free\nlss(T22, T23) !=? lss(0, s(X29))", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: lss(0, s(T28)), SCOPE: 3, CLAUSE: 6\n\nT28 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: lss(T33, T34)\n\nT33 is ground\nT34 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: ','(sub(T43, T44, X50), div_s(X50, T44, T46))\n\nT43 is ground\nT44 is ground\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: sub(T43, T44, X50)\n\nT43 is ground\nT44 is ground\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: div_s(T49, T44, T46)\n\nT44 is ground\nT49 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: sub(T43, T44, X50), SCOPE: 4, CLAUSE: 2 | sub(T43, T44, X50), SCOPE: 4, CLAUSE: 7\n\nT43 is ground\nT44 is ground\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: true | sub(T54, 0, X50), SCOPE: 4, CLAUSE: 7\n\nT54 is ground\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: sub(T43, T44, X50), SCOPE: 4, CLAUSE: 7\n\nT43 is ground\nT44 is ground\nX50 is free\nX57 is free\nsub(T43, T44, X50) !=? sub(X57, 0, X57)", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: sub(T54, 0, X50), SCOPE: 4, CLAUSE: 7\n\nT54 is ground\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: sub(T60, T61, X72)\n\nT60 is ground\nT61 is ground\nX72 is free", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 65 [arrowhead = none ];
65 -> 4;

66 [label="EVAL with clause\ndiv(X4, s(X5), X6) :- div_s(X4, X5, X6).\nand substitutionT1 -> T7,\nX4 -> T7,\nX5 -> T8,\nT2 -> s(T8),\nT3 -> T10,\nX6 -> T10,\nT9 -> T10", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 66 [arrowhead = none ];
66 -> 6;

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

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

69 [label="EVAL with clause\ndiv_s(0, X9, 0).\nand substitutionT7 -> 0,\nT8 -> T13,\nX9 -> T13,\nT10 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
9 -> 69 [arrowhead = none ];
69 -> 10;

70 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
9 -> 70 [arrowhead = none ];
70 -> 11;

71 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
10 -> 71 [arrowhead = none ];
71 -> 12;

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

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

74 [label="BACKTRACK\nfor clause: div_s(s(X), Y, 0) :- lss(X, Y)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
12 -> 74 [arrowhead = none ];
74 -> 13;

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

76 [label="EVAL with clause\ndiv_s(s(X23), X24, 0) :- lss(X23, X24).\nand substitutionX23 -> T22,\nT7 -> s(T22),\nT8 -> T23,\nX24 -> T23,\nT10 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
18 -> 76 [arrowhead = none ];
76 -> 25;

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

78 [label="EVAL with clause\ndiv_s(s(X47), X48, s(X49)) :- ','(sub(X47, X48, X50), div_s(X50, X48, X49)).\nand substitutionX47 -> T43,\nT7 -> s(T43),\nT8 -> T44,\nX48 -> T44,\nX49 -> T46,\nT10 -> s(T46),\nT45 -> T46", fontsize=14, style = filled, fillcolor = lightblue];
21 -> 78 [arrowhead = none ];
78 -> 44;

79 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
21 -> 79 [arrowhead = none ];
79 -> 46;

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

81 [label="EVAL with clause\nlss(0, s(X29)).\nand substitutionT22 -> 0,\nX29 -> T28,\nT23 -> s(T28)", fontsize=14, style = filled, fillcolor = lightblue];
28 -> 81 [arrowhead = none ];
81 -> 30;

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

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

84 [label="EVAL with clause\nlss(s(X36), s(X37)) :- lss(X36, X37).\nand substitutionX36 -> T33,\nT22 -> s(T33),\nX37 -> T34,\nT23 -> s(T34)", fontsize=14, style = filled, fillcolor = lightblue];
32 -> 84 [arrowhead = none ];
84 -> 39;

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

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

87 [label="INSTANCE with matching:\nT22 -> T33\nT23 -> T34", fontsize=14, style = filled, fillcolor = lightgrey];
39 -> 87 [arrowhead = none , style=dashed];
87 -> 25[style=dashed];

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

89 [label="SPLIT 2\nnew knowledge:\nT43 is ground\nT44 is ground\nT49 is ground\nreplacements:X50 -> T49", fontsize=14, style = filled, fillcolor = violet];
44 -> 89 [arrowhead = none ];
89 -> 50;

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

91 [label="INSTANCE with matching:\nT7 -> T49\nT8 -> T44\nT10 -> T46", fontsize=14, style = filled, fillcolor = lightgrey];
50 -> 91 [arrowhead = none , style=dashed];
91 -> 6[style=dashed];

92 [label="EVAL with clause\nsub(X57, 0, X57).\nand substitutionT43 -> T54,\nX57 -> T54,\nT44 -> 0,\nX50 -> T54", fontsize=14, style = filled, fillcolor = lightblue];
58 -> 92 [arrowhead = none ];
92 -> 59;

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

94 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
59 -> 94 [arrowhead = none ];
94 -> 61;

95 [label="EVAL with clause\nsub(s(X69), s(X70), X71) :- sub(X69, X70, X71).\nand substitutionX69 -> T60,\nT43 -> s(T60),\nX70 -> T61,\nT44 -> s(T61),\nX50 -> X72,\nX71 -> X72", fontsize=14, style = filled, fillcolor = lightblue];
60 -> 95 [arrowhead = none ];
95 -> 63;

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

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

98 [label="INSTANCE with matching:\nT43 -> T60\nT44 -> T61\nX50 -> X72", fontsize=14, style = filled, fillcolor = lightgrey];
63 -> 98 [arrowhead = none , style=dashed];
98 -> 49[style=dashed];

}

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, s(z1)) → U1(f6_in(z0, z1), z0, s(z1))
U1(f6_out1(z0), z1, s(z2)) → f1_out1(z0)
f6_in(0, z0) → f6_out1(0)
f6_in(z0, z1) → U2(f11_in(z0, z1), z0, z1)
U2(f11_out1(z0), z1, z2) → f6_out1(z0)
U2(f11_out2(z0), z1, z2) → f6_out1(z0)
f25_in(0, s(z0)) → f25_out1
f25_in(s(z0), s(z1)) → U3(f25_in(z0, z1), s(z0), s(z1))
U3(f25_out1, s(z0), s(z1)) → f25_out1
f49_in(z0, 0) → f49_out1(z0)
f49_in(s(z0), s(z1)) → U4(f49_in(z0, z1), s(z0), s(z1))
U4(f49_out1(z0), s(z1), s(z2)) → f49_out1(z0)
f18_in(s(z0), z1) → U5(f25_in(z0, z1), s(z0), z1)
U5(f25_out1, s(z0), z1) → f18_out1(0)
f21_in(s(z0), z1) → U6(f44_in(z0, z1), s(z0), z1)
U6(f44_out1(z0, z1), s(z2), z3) → f21_out1(s(z1))
f44_in(z0, z1) → U7(f49_in(z0, z1), z0, z1)
U7(f49_out1(z0), z1, z2) → U8(f6_in(z0, z2), z1, z2, z0)
U8(f6_out1(z0), z1, z2, z3) → f44_out1(z3, z0)
f11_in(z0, z1) → U9(f18_in(z0, z1), f21_in(z0, z1), z0, z1)
U9(f18_out1(z0), z1, z2, z3) → f11_out1(z0)
U9(z0, f21_out1(z1), z2, z3) → f11_out2(z1)

Tuples:

F1_IN(z0, s(z1)) → c(U1'(f6_in(z0, z1), z0, s(z1)), F6_IN(z0, z1))
F6_IN(z0, z1) → c3(U2'(f11_in(z0, z1), z0, z1), F11_IN(z0, z1))
F25_IN(s(z0), s(z1)) → c7(U3'(f25_in(z0, z1), s(z0), s(z1)), F25_IN(z0, z1))
F49_IN(s(z0), s(z1)) → c10(U4'(f49_in(z0, z1), s(z0), s(z1)), F49_IN(z0, z1))
F18_IN(s(z0), z1) → c12(U5'(f25_in(z0, z1), s(z0), z1), F25_IN(z0, z1))
F21_IN(s(z0), z1) → c14(U6'(f44_in(z0, z1), s(z0), z1), F44_IN(z0, z1))
F44_IN(z0, z1) → c16(U7'(f49_in(z0, z1), z0, z1), F49_IN(z0, z1))
U7'(f49_out1(z0), z1, z2) → c17(U8'(f6_in(z0, z2), z1, z2, z0), F6_IN(z0, z2))
F11_IN(z0, z1) → c19(U9'(f18_in(z0, z1), f21_in(z0, z1), z0, z1), F18_IN(z0, z1), F21_IN(z0, z1))

S tuples:

F1_IN(z0, s(z1)) → c(U1'(f6_in(z0, z1), z0, s(z1)), F6_IN(z0, z1))
F6_IN(z0, z1) → c3(U2'(f11_in(z0, z1), z0, z1), F11_IN(z0, z1))
F25_IN(s(z0), s(z1)) → c7(U3'(f25_in(z0, z1), s(z0), s(z1)), F25_IN(z0, z1))
F49_IN(s(z0), s(z1)) → c10(U4'(f49_in(z0, z1), s(z0), s(z1)), F49_IN(z0, z1))
F18_IN(s(z0), z1) → c12(U5'(f25_in(z0, z1), s(z0), z1), F25_IN(z0, z1))
F21_IN(s(z0), z1) → c14(U6'(f44_in(z0, z1), s(z0), z1), F44_IN(z0, z1))
F44_IN(z0, z1) → c16(U7'(f49_in(z0, z1), z0, z1), F49_IN(z0, z1))
U7'(f49_out1(z0), z1, z2) → c17(U8'(f6_in(z0, z2), z1, z2, z0), F6_IN(z0, z2))
F11_IN(z0, z1) → c19(U9'(f18_in(z0, z1), f21_in(z0, z1), z0, z1), F18_IN(z0, z1), F21_IN(z0, z1))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f6_in, U2, f25_in, U3, f49_in, U4, f18_in, U5, f21_in, U6, f44_in, U7, U8, f11_in, U9

Defined Pair Symbols:

F1_IN, F6_IN, F25_IN, F49_IN, F18_IN, F21_IN, F44_IN, U7', F11_IN

Compound Symbols:

c, c3, c7, c10, c12, c14, c16, c17, c19

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

Split RHS of tuples not part of any SCC

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, s(z1)) → U1(f6_in(z0, z1), z0, s(z1))
U1(f6_out1(z0), z1, s(z2)) → f1_out1(z0)
f6_in(0, z0) → f6_out1(0)
f6_in(z0, z1) → U2(f11_in(z0, z1), z0, z1)
U2(f11_out1(z0), z1, z2) → f6_out1(z0)
U2(f11_out2(z0), z1, z2) → f6_out1(z0)
f25_in(0, s(z0)) → f25_out1
f25_in(s(z0), s(z1)) → U3(f25_in(z0, z1), s(z0), s(z1))
U3(f25_out1, s(z0), s(z1)) → f25_out1
f49_in(z0, 0) → f49_out1(z0)
f49_in(s(z0), s(z1)) → U4(f49_in(z0, z1), s(z0), s(z1))
U4(f49_out1(z0), s(z1), s(z2)) → f49_out1(z0)
f18_in(s(z0), z1) → U5(f25_in(z0, z1), s(z0), z1)
U5(f25_out1, s(z0), z1) → f18_out1(0)
f21_in(s(z0), z1) → U6(f44_in(z0, z1), s(z0), z1)
U6(f44_out1(z0, z1), s(z2), z3) → f21_out1(s(z1))
f44_in(z0, z1) → U7(f49_in(z0, z1), z0, z1)
U7(f49_out1(z0), z1, z2) → U8(f6_in(z0, z2), z1, z2, z0)
U8(f6_out1(z0), z1, z2, z3) → f44_out1(z3, z0)
f11_in(z0, z1) → U9(f18_in(z0, z1), f21_in(z0, z1), z0, z1)
U9(f18_out1(z0), z1, z2, z3) → f11_out1(z0)
U9(z0, f21_out1(z1), z2, z3) → f11_out2(z1)

Tuples:

F6_IN(z0, z1) → c3(U2'(f11_in(z0, z1), z0, z1), F11_IN(z0, z1))
F25_IN(s(z0), s(z1)) → c7(U3'(f25_in(z0, z1), s(z0), s(z1)), F25_IN(z0, z1))
F49_IN(s(z0), s(z1)) → c10(U4'(f49_in(z0, z1), s(z0), s(z1)), F49_IN(z0, z1))
F21_IN(s(z0), z1) → c14(U6'(f44_in(z0, z1), s(z0), z1), F44_IN(z0, z1))
F44_IN(z0, z1) → c16(U7'(f49_in(z0, z1), z0, z1), F49_IN(z0, z1))
U7'(f49_out1(z0), z1, z2) → c17(U8'(f6_in(z0, z2), z1, z2, z0), F6_IN(z0, z2))
F11_IN(z0, z1) → c19(U9'(f18_in(z0, z1), f21_in(z0, z1), z0, z1), F18_IN(z0, z1), F21_IN(z0, z1))
F1_IN(z0, s(z1)) → c1(U1'(f6_in(z0, z1), z0, s(z1)))
F1_IN(z0, s(z1)) → c1(F6_IN(z0, z1))
F18_IN(s(z0), z1) → c1(U5'(f25_in(z0, z1), s(z0), z1))
F18_IN(s(z0), z1) → c1(F25_IN(z0, z1))

S tuples:

F6_IN(z0, z1) → c3(U2'(f11_in(z0, z1), z0, z1), F11_IN(z0, z1))
F25_IN(s(z0), s(z1)) → c7(U3'(f25_in(z0, z1), s(z0), s(z1)), F25_IN(z0, z1))
F49_IN(s(z0), s(z1)) → c10(U4'(f49_in(z0, z1), s(z0), s(z1)), F49_IN(z0, z1))
F21_IN(s(z0), z1) → c14(U6'(f44_in(z0, z1), s(z0), z1), F44_IN(z0, z1))
F44_IN(z0, z1) → c16(U7'(f49_in(z0, z1), z0, z1), F49_IN(z0, z1))
U7'(f49_out1(z0), z1, z2) → c17(U8'(f6_in(z0, z2), z1, z2, z0), F6_IN(z0, z2))
F11_IN(z0, z1) → c19(U9'(f18_in(z0, z1), f21_in(z0, z1), z0, z1), F18_IN(z0, z1), F21_IN(z0, z1))
F1_IN(z0, s(z1)) → c1(U1'(f6_in(z0, z1), z0, s(z1)))
F1_IN(z0, s(z1)) → c1(F6_IN(z0, z1))
F18_IN(s(z0), z1) → c1(U5'(f25_in(z0, z1), s(z0), z1))
F18_IN(s(z0), z1) → c1(F25_IN(z0, z1))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f6_in, U2, f25_in, U3, f49_in, U4, f18_in, U5, f21_in, U6, f44_in, U7, U8, f11_in, U9

Defined Pair Symbols:

F6_IN, F25_IN, F49_IN, F21_IN, F44_IN, U7', F11_IN, F1_IN, F18_IN

Compound Symbols:

c3, c7, c10, c14, c16, c17, c19, c1

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

Removed 8 trailing tuple parts

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, s(z1)) → U1(f6_in(z0, z1), z0, s(z1))
U1(f6_out1(z0), z1, s(z2)) → f1_out1(z0)
f6_in(0, z0) → f6_out1(0)
f6_in(z0, z1) → U2(f11_in(z0, z1), z0, z1)
U2(f11_out1(z0), z1, z2) → f6_out1(z0)
U2(f11_out2(z0), z1, z2) → f6_out1(z0)
f25_in(0, s(z0)) → f25_out1
f25_in(s(z0), s(z1)) → U3(f25_in(z0, z1), s(z0), s(z1))
U3(f25_out1, s(z0), s(z1)) → f25_out1
f49_in(z0, 0) → f49_out1(z0)
f49_in(s(z0), s(z1)) → U4(f49_in(z0, z1), s(z0), s(z1))
U4(f49_out1(z0), s(z1), s(z2)) → f49_out1(z0)
f18_in(s(z0), z1) → U5(f25_in(z0, z1), s(z0), z1)
U5(f25_out1, s(z0), z1) → f18_out1(0)
f21_in(s(z0), z1) → U6(f44_in(z0, z1), s(z0), z1)
U6(f44_out1(z0, z1), s(z2), z3) → f21_out1(s(z1))
f44_in(z0, z1) → U7(f49_in(z0, z1), z0, z1)
U7(f49_out1(z0), z1, z2) → U8(f6_in(z0, z2), z1, z2, z0)
U8(f6_out1(z0), z1, z2, z3) → f44_out1(z3, z0)
f11_in(z0, z1) → U9(f18_in(z0, z1), f21_in(z0, z1), z0, z1)
U9(f18_out1(z0), z1, z2, z3) → f11_out1(z0)
U9(z0, f21_out1(z1), z2, z3) → f11_out2(z1)

Tuples:

F44_IN(z0, z1) → c16(U7'(f49_in(z0, z1), z0, z1), F49_IN(z0, z1))
F1_IN(z0, s(z1)) → c1(F6_IN(z0, z1))
F18_IN(s(z0), z1) → c1(F25_IN(z0, z1))
F6_IN(z0, z1) → c3(F11_IN(z0, z1))
F25_IN(s(z0), s(z1)) → c7(F25_IN(z0, z1))
F49_IN(s(z0), s(z1)) → c10(F49_IN(z0, z1))
F21_IN(s(z0), z1) → c14(F44_IN(z0, z1))
U7'(f49_out1(z0), z1, z2) → c17(F6_IN(z0, z2))
F11_IN(z0, z1) → c19(F18_IN(z0, z1), F21_IN(z0, z1))
F1_IN(z0, s(z1)) → c1
F18_IN(s(z0), z1) → c1

S tuples:

F44_IN(z0, z1) → c16(U7'(f49_in(z0, z1), z0, z1), F49_IN(z0, z1))
F1_IN(z0, s(z1)) → c1(F6_IN(z0, z1))
F18_IN(s(z0), z1) → c1(F25_IN(z0, z1))
F6_IN(z0, z1) → c3(F11_IN(z0, z1))
F25_IN(s(z0), s(z1)) → c7(F25_IN(z0, z1))
F49_IN(s(z0), s(z1)) → c10(F49_IN(z0, z1))
F21_IN(s(z0), z1) → c14(F44_IN(z0, z1))
U7'(f49_out1(z0), z1, z2) → c17(F6_IN(z0, z2))
F11_IN(z0, z1) → c19(F18_IN(z0, z1), F21_IN(z0, z1))
F1_IN(z0, s(z1)) → c1
F18_IN(s(z0), z1) → c1

K tuples:none
Defined Rule Symbols:

f1_in, U1, f6_in, U2, f25_in, U3, f49_in, U4, f18_in, U5, f21_in, U6, f44_in, U7, U8, f11_in, U9

Defined Pair Symbols:

F44_IN, F1_IN, F18_IN, F6_IN, F25_IN, F49_IN, F21_IN, U7', F11_IN

Compound Symbols:

c16, c1, c3, c7, c10, c14, c17, c19, c1

(23) CdtKnowledgeProof (EQUIVALENT transformation)

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

F1_IN(z0, s(z1)) → c1(F6_IN(z0, z1))
F1_IN(z0, s(z1)) → c1

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, s(z1)) → U1(f6_in(z0, z1), z0, s(z1))
U1(f6_out1(z0), z1, s(z2)) → f1_out1(z0)
f6_in(0, z0) → f6_out1(0)
f6_in(z0, z1) → U2(f11_in(z0, z1), z0, z1)
U2(f11_out1(z0), z1, z2) → f6_out1(z0)
U2(f11_out2(z0), z1, z2) → f6_out1(z0)
f25_in(0, s(z0)) → f25_out1
f25_in(s(z0), s(z1)) → U3(f25_in(z0, z1), s(z0), s(z1))
U3(f25_out1, s(z0), s(z1)) → f25_out1
f49_in(z0, 0) → f49_out1(z0)
f49_in(s(z0), s(z1)) → U4(f49_in(z0, z1), s(z0), s(z1))
U4(f49_out1(z0), s(z1), s(z2)) → f49_out1(z0)
f18_in(s(z0), z1) → U5(f25_in(z0, z1), s(z0), z1)
U5(f25_out1, s(z0), z1) → f18_out1(0)
f21_in(s(z0), z1) → U6(f44_in(z0, z1), s(z0), z1)
U6(f44_out1(z0, z1), s(z2), z3) → f21_out1(s(z1))
f44_in(z0, z1) → U7(f49_in(z0, z1), z0, z1)
U7(f49_out1(z0), z1, z2) → U8(f6_in(z0, z2), z1, z2, z0)
U8(f6_out1(z0), z1, z2, z3) → f44_out1(z3, z0)
f11_in(z0, z1) → U9(f18_in(z0, z1), f21_in(z0, z1), z0, z1)
U9(f18_out1(z0), z1, z2, z3) → f11_out1(z0)
U9(z0, f21_out1(z1), z2, z3) → f11_out2(z1)

Tuples:

F44_IN(z0, z1) → c16(U7'(f49_in(z0, z1), z0, z1), F49_IN(z0, z1))
F1_IN(z0, s(z1)) → c1(F6_IN(z0, z1))
F18_IN(s(z0), z1) → c1(F25_IN(z0, z1))
F6_IN(z0, z1) → c3(F11_IN(z0, z1))
F25_IN(s(z0), s(z1)) → c7(F25_IN(z0, z1))
F49_IN(s(z0), s(z1)) → c10(F49_IN(z0, z1))
F21_IN(s(z0), z1) → c14(F44_IN(z0, z1))
U7'(f49_out1(z0), z1, z2) → c17(F6_IN(z0, z2))
F11_IN(z0, z1) → c19(F18_IN(z0, z1), F21_IN(z0, z1))
F1_IN(z0, s(z1)) → c1
F18_IN(s(z0), z1) → c1

S tuples:

F44_IN(z0, z1) → c16(U7'(f49_in(z0, z1), z0, z1), F49_IN(z0, z1))
F18_IN(s(z0), z1) → c1(F25_IN(z0, z1))
F6_IN(z0, z1) → c3(F11_IN(z0, z1))
F25_IN(s(z0), s(z1)) → c7(F25_IN(z0, z1))
F49_IN(s(z0), s(z1)) → c10(F49_IN(z0, z1))
F21_IN(s(z0), z1) → c14(F44_IN(z0, z1))
U7'(f49_out1(z0), z1, z2) → c17(F6_IN(z0, z2))
F11_IN(z0, z1) → c19(F18_IN(z0, z1), F21_IN(z0, z1))
F18_IN(s(z0), z1) → c1

K tuples:

F1_IN(z0, s(z1)) → c1(F6_IN(z0, z1))
F1_IN(z0, s(z1)) → c1

Defined Rule Symbols:

f1_in, U1, f6_in, U2, f25_in, U3, f49_in, U4, f18_in, U5, f21_in, U6, f44_in, U7, U8, f11_in, U9

Defined Pair Symbols:

F44_IN, F1_IN, F18_IN, F6_IN, F25_IN, F49_IN, F21_IN, U7', F11_IN

Compound Symbols:

c16, c1, c3, c7, c10, c14, c17, c19, c1

(25) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

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

F21_IN(s(z0), z1) → c14(F44_IN(z0, z1))

We considered the (Usable) Rules:

f49_in(z0, 0) → f49_out1(z0)
f49_in(s(z0), s(z1)) → U4(f49_in(z0, z1), s(z0), s(z1))
U4(f49_out1(z0), s(z1), s(z2)) → f49_out1(z0)

And the Tuples:

F44_IN(z0, z1) → c16(U7'(f49_in(z0, z1), z0, z1), F49_IN(z0, z1))
F1_IN(z0, s(z1)) → c1(F6_IN(z0, z1))
F18_IN(s(z0), z1) → c1(F25_IN(z0, z1))
F6_IN(z0, z1) → c3(F11_IN(z0, z1))
F25_IN(s(z0), s(z1)) → c7(F25_IN(z0, z1))
F49_IN(s(z0), s(z1)) → c10(F49_IN(z0, z1))
F21_IN(s(z0), z1) → c14(F44_IN(z0, z1))
U7'(f49_out1(z0), z1, z2) → c17(F6_IN(z0, z2))
F11_IN(z0, z1) → c19(F18_IN(z0, z1), F21_IN(z0, z1))
F1_IN(z0, s(z1)) → c1
F18_IN(s(z0), z1) → c1

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

POL(0) = 0   
POL(F11_IN(x₁, x₂)) = x₁   
POL(F18_IN(x₁, x₂)) = 0   
POL(F1_IN(x₁, x₂)) = [2] + [2]x₁ + [2]x₂   
POL(F21_IN(x₁, x₂)) = x₁   
POL(F25_IN(x₁, x₂)) = 0   
POL(F44_IN(x₁, x₂)) = x₁   
POL(F49_IN(x₁, x₂)) = 0   
POL(F6_IN(x₁, x₂)) = x₁   
POL(U4(x₁, x₂, x₃)) = x₁   
POL(U7'(x₁, x₂, x₃)) = x₁   
POL(c1) = 0   
POL(c1(x₁)) = x₁   
POL(c10(x₁)) = x₁   
POL(c14(x₁)) = x₁   
POL(c16(x₁, x₂)) = x₁ + x₂   
POL(c17(x₁)) = x₁   
POL(c19(x₁, x₂)) = x₁ + x₂   
POL(c3(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(f49_in(x₁, x₂)) = x₁   
POL(f49_out1(x₁)) = x₁   
POL(s(x₁)) = [1] + x₁   

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, s(z1)) → U1(f6_in(z0, z1), z0, s(z1))
U1(f6_out1(z0), z1, s(z2)) → f1_out1(z0)
f6_in(0, z0) → f6_out1(0)
f6_in(z0, z1) → U2(f11_in(z0, z1), z0, z1)
U2(f11_out1(z0), z1, z2) → f6_out1(z0)
U2(f11_out2(z0), z1, z2) → f6_out1(z0)
f25_in(0, s(z0)) → f25_out1
f25_in(s(z0), s(z1)) → U3(f25_in(z0, z1), s(z0), s(z1))
U3(f25_out1, s(z0), s(z1)) → f25_out1
f49_in(z0, 0) → f49_out1(z0)
f49_in(s(z0), s(z1)) → U4(f49_in(z0, z1), s(z0), s(z1))
U4(f49_out1(z0), s(z1), s(z2)) → f49_out1(z0)
f18_in(s(z0), z1) → U5(f25_in(z0, z1), s(z0), z1)
U5(f25_out1, s(z0), z1) → f18_out1(0)
f21_in(s(z0), z1) → U6(f44_in(z0, z1), s(z0), z1)
U6(f44_out1(z0, z1), s(z2), z3) → f21_out1(s(z1))
f44_in(z0, z1) → U7(f49_in(z0, z1), z0, z1)
U7(f49_out1(z0), z1, z2) → U8(f6_in(z0, z2), z1, z2, z0)
U8(f6_out1(z0), z1, z2, z3) → f44_out1(z3, z0)
f11_in(z0, z1) → U9(f18_in(z0, z1), f21_in(z0, z1), z0, z1)
U9(f18_out1(z0), z1, z2, z3) → f11_out1(z0)
U9(z0, f21_out1(z1), z2, z3) → f11_out2(z1)

Tuples:

F44_IN(z0, z1) → c16(U7'(f49_in(z0, z1), z0, z1), F49_IN(z0, z1))
F1_IN(z0, s(z1)) → c1(F6_IN(z0, z1))
F18_IN(s(z0), z1) → c1(F25_IN(z0, z1))
F6_IN(z0, z1) → c3(F11_IN(z0, z1))
F25_IN(s(z0), s(z1)) → c7(F25_IN(z0, z1))
F49_IN(s(z0), s(z1)) → c10(F49_IN(z0, z1))
F21_IN(s(z0), z1) → c14(F44_IN(z0, z1))
U7'(f49_out1(z0), z1, z2) → c17(F6_IN(z0, z2))
F11_IN(z0, z1) → c19(F18_IN(z0, z1), F21_IN(z0, z1))
F1_IN(z0, s(z1)) → c1
F18_IN(s(z0), z1) → c1

S tuples:

F44_IN(z0, z1) → c16(U7'(f49_in(z0, z1), z0, z1), F49_IN(z0, z1))
F18_IN(s(z0), z1) → c1(F25_IN(z0, z1))
F6_IN(z0, z1) → c3(F11_IN(z0, z1))
F25_IN(s(z0), s(z1)) → c7(F25_IN(z0, z1))
F49_IN(s(z0), s(z1)) → c10(F49_IN(z0, z1))
U7'(f49_out1(z0), z1, z2) → c17(F6_IN(z0, z2))
F11_IN(z0, z1) → c19(F18_IN(z0, z1), F21_IN(z0, z1))
F18_IN(s(z0), z1) → c1

K tuples:

F1_IN(z0, s(z1)) → c1(F6_IN(z0, z1))
F1_IN(z0, s(z1)) → c1
F21_IN(s(z0), z1) → c14(F44_IN(z0, z1))

Defined Rule Symbols:

f1_in, U1, f6_in, U2, f25_in, U3, f49_in, U4, f18_in, U5, f21_in, U6, f44_in, U7, U8, f11_in, U9

Defined Pair Symbols:

F44_IN, F1_IN, F18_IN, F6_IN, F25_IN, F49_IN, F21_IN, U7', F11_IN

Compound Symbols:

c16, c1, c3, c7, c10, c14, c17, c19, c1

(27) CdtKnowledgeProof (EQUIVALENT transformation)

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

F44_IN(z0, z1) → c16(U7'(f49_in(z0, z1), z0, z1), F49_IN(z0, z1))
U7'(f49_out1(z0), z1, z2) → c17(F6_IN(z0, z2))
U7'(f49_out1(z0), z1, z2) → c17(F6_IN(z0, z2))
F6_IN(z0, z1) → c3(F11_IN(z0, z1))
F11_IN(z0, z1) → c19(F18_IN(z0, z1), F21_IN(z0, z1))
F18_IN(s(z0), z1) → c1(F25_IN(z0, z1))
F21_IN(s(z0), z1) → c14(F44_IN(z0, z1))
F18_IN(s(z0), z1) → c1

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, s(z1)) → U1(f6_in(z0, z1), z0, s(z1))
U1(f6_out1(z0), z1, s(z2)) → f1_out1(z0)
f6_in(0, z0) → f6_out1(0)
f6_in(z0, z1) → U2(f11_in(z0, z1), z0, z1)
U2(f11_out1(z0), z1, z2) → f6_out1(z0)
U2(f11_out2(z0), z1, z2) → f6_out1(z0)
f25_in(0, s(z0)) → f25_out1
f25_in(s(z0), s(z1)) → U3(f25_in(z0, z1), s(z0), s(z1))
U3(f25_out1, s(z0), s(z1)) → f25_out1
f49_in(z0, 0) → f49_out1(z0)
f49_in(s(z0), s(z1)) → U4(f49_in(z0, z1), s(z0), s(z1))
U4(f49_out1(z0), s(z1), s(z2)) → f49_out1(z0)
f18_in(s(z0), z1) → U5(f25_in(z0, z1), s(z0), z1)
U5(f25_out1, s(z0), z1) → f18_out1(0)
f21_in(s(z0), z1) → U6(f44_in(z0, z1), s(z0), z1)
U6(f44_out1(z0, z1), s(z2), z3) → f21_out1(s(z1))
f44_in(z0, z1) → U7(f49_in(z0, z1), z0, z1)
U7(f49_out1(z0), z1, z2) → U8(f6_in(z0, z2), z1, z2, z0)
U8(f6_out1(z0), z1, z2, z3) → f44_out1(z3, z0)
f11_in(z0, z1) → U9(f18_in(z0, z1), f21_in(z0, z1), z0, z1)
U9(f18_out1(z0), z1, z2, z3) → f11_out1(z0)
U9(z0, f21_out1(z1), z2, z3) → f11_out2(z1)

Tuples:

F44_IN(z0, z1) → c16(U7'(f49_in(z0, z1), z0, z1), F49_IN(z0, z1))
F1_IN(z0, s(z1)) → c1(F6_IN(z0, z1))
F18_IN(s(z0), z1) → c1(F25_IN(z0, z1))
F6_IN(z0, z1) → c3(F11_IN(z0, z1))
F25_IN(s(z0), s(z1)) → c7(F25_IN(z0, z1))
F49_IN(s(z0), s(z1)) → c10(F49_IN(z0, z1))
F21_IN(s(z0), z1) → c14(F44_IN(z0, z1))
U7'(f49_out1(z0), z1, z2) → c17(F6_IN(z0, z2))
F11_IN(z0, z1) → c19(F18_IN(z0, z1), F21_IN(z0, z1))
F1_IN(z0, s(z1)) → c1
F18_IN(s(z0), z1) → c1

S tuples:

F25_IN(s(z0), s(z1)) → c7(F25_IN(z0, z1))
F49_IN(s(z0), s(z1)) → c10(F49_IN(z0, z1))

K tuples:

F1_IN(z0, s(z1)) → c1(F6_IN(z0, z1))
F1_IN(z0, s(z1)) → c1
F21_IN(s(z0), z1) → c14(F44_IN(z0, z1))
F44_IN(z0, z1) → c16(U7'(f49_in(z0, z1), z0, z1), F49_IN(z0, z1))
U7'(f49_out1(z0), z1, z2) → c17(F6_IN(z0, z2))
F6_IN(z0, z1) → c3(F11_IN(z0, z1))
F11_IN(z0, z1) → c19(F18_IN(z0, z1), F21_IN(z0, z1))
F18_IN(s(z0), z1) → c1(F25_IN(z0, z1))
F18_IN(s(z0), z1) → c1

Defined Rule Symbols:

f1_in, U1, f6_in, U2, f25_in, U3, f49_in, U4, f18_in, U5, f21_in, U6, f44_in, U7, U8, f11_in, U9

Defined Pair Symbols:

F44_IN, F1_IN, F18_IN, F6_IN, F25_IN, F49_IN, F21_IN, U7', F11_IN

Compound Symbols:

c16, c1, c3, c7, c10, c14, c17, c19, 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.

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

We considered the (Usable) Rules:

f49_in(z0, 0) → f49_out1(z0)
f49_in(s(z0), s(z1)) → U4(f49_in(z0, z1), s(z0), s(z1))
U4(f49_out1(z0), s(z1), s(z2)) → f49_out1(z0)

And the Tuples:

F44_IN(z0, z1) → c16(U7'(f49_in(z0, z1), z0, z1), F49_IN(z0, z1))
F1_IN(z0, s(z1)) → c1(F6_IN(z0, z1))
F18_IN(s(z0), z1) → c1(F25_IN(z0, z1))
F6_IN(z0, z1) → c3(F11_IN(z0, z1))
F25_IN(s(z0), s(z1)) → c7(F25_IN(z0, z1))
F49_IN(s(z0), s(z1)) → c10(F49_IN(z0, z1))
F21_IN(s(z0), z1) → c14(F44_IN(z0, z1))
U7'(f49_out1(z0), z1, z2) → c17(F6_IN(z0, z2))
F11_IN(z0, z1) → c19(F18_IN(z0, z1), F21_IN(z0, z1))
F1_IN(z0, s(z1)) → c1
F18_IN(s(z0), 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(F18_IN(x₁, x₂)) = x₁   
POL(F1_IN(x₁, x₂)) = [1] + x₂ + x₂² + x₁·x₂ + x₁²   
POL(F21_IN(x₁, x₂)) = x₂ + x₁²   
POL(F25_IN(x₁, x₂)) = [1] + x₁   
POL(F44_IN(x₁, x₂)) = [1] + x₁ + x₂ + x₁²   
POL(F49_IN(x₁, x₂)) = 0   
POL(F6_IN(x₁, x₂)) = x₁ + x₂ + x₁²   
POL(U4(x₁, x₂, x₃)) = x₁   
POL(U7'(x₁, x₂, x₃)) = x₁ + x₃ + x₁²   
POL(c1) = 0   
POL(c1(x₁)) = x₁   
POL(c10(x₁)) = x₁   
POL(c14(x₁)) = x₁   
POL(c16(x₁, x₂)) = x₁ + x₂   
POL(c17(x₁)) = x₁   
POL(c19(x₁, x₂)) = x₁ + x₂   
POL(c3(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(f49_in(x₁, x₂)) = x₁   
POL(f49_out1(x₁)) = x₁   
POL(s(x₁)) = [1] + x₁   

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, s(z1)) → U1(f6_in(z0, z1), z0, s(z1))
U1(f6_out1(z0), z1, s(z2)) → f1_out1(z0)
f6_in(0, z0) → f6_out1(0)
f6_in(z0, z1) → U2(f11_in(z0, z1), z0, z1)
U2(f11_out1(z0), z1, z2) → f6_out1(z0)
U2(f11_out2(z0), z1, z2) → f6_out1(z0)
f25_in(0, s(z0)) → f25_out1
f25_in(s(z0), s(z1)) → U3(f25_in(z0, z1), s(z0), s(z1))
U3(f25_out1, s(z0), s(z1)) → f25_out1
f49_in(z0, 0) → f49_out1(z0)
f49_in(s(z0), s(z1)) → U4(f49_in(z0, z1), s(z0), s(z1))
U4(f49_out1(z0), s(z1), s(z2)) → f49_out1(z0)
f18_in(s(z0), z1) → U5(f25_in(z0, z1), s(z0), z1)
U5(f25_out1, s(z0), z1) → f18_out1(0)
f21_in(s(z0), z1) → U6(f44_in(z0, z1), s(z0), z1)
U6(f44_out1(z0, z1), s(z2), z3) → f21_out1(s(z1))
f44_in(z0, z1) → U7(f49_in(z0, z1), z0, z1)
U7(f49_out1(z0), z1, z2) → U8(f6_in(z0, z2), z1, z2, z0)
U8(f6_out1(z0), z1, z2, z3) → f44_out1(z3, z0)
f11_in(z0, z1) → U9(f18_in(z0, z1), f21_in(z0, z1), z0, z1)
U9(f18_out1(z0), z1, z2, z3) → f11_out1(z0)
U9(z0, f21_out1(z1), z2, z3) → f11_out2(z1)

Tuples:

F44_IN(z0, z1) → c16(U7'(f49_in(z0, z1), z0, z1), F49_IN(z0, z1))
F1_IN(z0, s(z1)) → c1(F6_IN(z0, z1))
F18_IN(s(z0), z1) → c1(F25_IN(z0, z1))
F6_IN(z0, z1) → c3(F11_IN(z0, z1))
F25_IN(s(z0), s(z1)) → c7(F25_IN(z0, z1))
F49_IN(s(z0), s(z1)) → c10(F49_IN(z0, z1))
F21_IN(s(z0), z1) → c14(F44_IN(z0, z1))
U7'(f49_out1(z0), z1, z2) → c17(F6_IN(z0, z2))
F11_IN(z0, z1) → c19(F18_IN(z0, z1), F21_IN(z0, z1))
F1_IN(z0, s(z1)) → c1
F18_IN(s(z0), z1) → c1

S tuples:

F49_IN(s(z0), s(z1)) → c10(F49_IN(z0, z1))

K tuples:

F1_IN(z0, s(z1)) → c1(F6_IN(z0, z1))
F1_IN(z0, s(z1)) → c1
F21_IN(s(z0), z1) → c14(F44_IN(z0, z1))
F44_IN(z0, z1) → c16(U7'(f49_in(z0, z1), z0, z1), F49_IN(z0, z1))
U7'(f49_out1(z0), z1, z2) → c17(F6_IN(z0, z2))
F6_IN(z0, z1) → c3(F11_IN(z0, z1))
F11_IN(z0, z1) → c19(F18_IN(z0, z1), F21_IN(z0, z1))
F18_IN(s(z0), z1) → c1(F25_IN(z0, z1))
F18_IN(s(z0), z1) → c1
F25_IN(s(z0), s(z1)) → c7(F25_IN(z0, z1))

Defined Rule Symbols:

f1_in, U1, f6_in, U2, f25_in, U3, f49_in, U4, f18_in, U5, f21_in, U6, f44_in, U7, U8, f11_in, U9

Defined Pair Symbols:

F44_IN, F1_IN, F18_IN, F6_IN, F25_IN, F49_IN, F21_IN, U7', F11_IN

Compound Symbols:

c16, c1, c3, c7, c10, c14, c17, c19, c1

(31) 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.

F49_IN(s(z0), s(z1)) → c10(F49_IN(z0, z1))

We considered the (Usable) Rules:

f49_in(z0, 0) → f49_out1(z0)
f49_in(s(z0), s(z1)) → U4(f49_in(z0, z1), s(z0), s(z1))
U4(f49_out1(z0), s(z1), s(z2)) → f49_out1(z0)

And the Tuples:

F44_IN(z0, z1) → c16(U7'(f49_in(z0, z1), z0, z1), F49_IN(z0, z1))
F1_IN(z0, s(z1)) → c1(F6_IN(z0, z1))
F18_IN(s(z0), z1) → c1(F25_IN(z0, z1))
F6_IN(z0, z1) → c3(F11_IN(z0, z1))
F25_IN(s(z0), s(z1)) → c7(F25_IN(z0, z1))
F49_IN(s(z0), s(z1)) → c10(F49_IN(z0, z1))
F21_IN(s(z0), z1) → c14(F44_IN(z0, z1))
U7'(f49_out1(z0), z1, z2) → c17(F6_IN(z0, z2))
F11_IN(z0, z1) → c19(F18_IN(z0, z1), F21_IN(z0, z1))
F1_IN(z0, s(z1)) → c1
F18_IN(s(z0), z1) → c1

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

POL(0) = 0   
POL(F11_IN(x₁, x₂)) = [1] + x₁ + x₁·x₂   
POL(F18_IN(x₁, x₂)) = 0   
POL(F1_IN(x₁, x₂)) = x₂ + x₂² + x₁·x₂   
POL(F21_IN(x₁, x₂)) = x₁ + x₁·x₂   
POL(F25_IN(x₁, x₂)) = 0   
POL(F44_IN(x₁, x₂)) = [1] + x₁ + x₂ + x₁·x₂   
POL(F49_IN(x₁, x₂)) = x₂   
POL(F6_IN(x₁, x₂)) = [1] + x₁ + x₁·x₂   
POL(U4(x₁, x₂, x₃)) = [1] + x₁   
POL(U7'(x₁, x₂, x₃)) = [1] + x₁ + x₁·x₃   
POL(c1) = 0   
POL(c1(x₁)) = x₁   
POL(c10(x₁)) = x₁   
POL(c14(x₁)) = x₁   
POL(c16(x₁, x₂)) = x₁ + x₂   
POL(c17(x₁)) = x₁   
POL(c19(x₁, x₂)) = x₁ + x₂   
POL(c3(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(f49_in(x₁, x₂)) = x₁   
POL(f49_out1(x₁)) = x₁   
POL(s(x₁)) = [1] + x₁   

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, s(z1)) → U1(f6_in(z0, z1), z0, s(z1))
U1(f6_out1(z0), z1, s(z2)) → f1_out1(z0)
f6_in(0, z0) → f6_out1(0)
f6_in(z0, z1) → U2(f11_in(z0, z1), z0, z1)
U2(f11_out1(z0), z1, z2) → f6_out1(z0)
U2(f11_out2(z0), z1, z2) → f6_out1(z0)
f25_in(0, s(z0)) → f25_out1
f25_in(s(z0), s(z1)) → U3(f25_in(z0, z1), s(z0), s(z1))
U3(f25_out1, s(z0), s(z1)) → f25_out1
f49_in(z0, 0) → f49_out1(z0)
f49_in(s(z0), s(z1)) → U4(f49_in(z0, z1), s(z0), s(z1))
U4(f49_out1(z0), s(z1), s(z2)) → f49_out1(z0)
f18_in(s(z0), z1) → U5(f25_in(z0, z1), s(z0), z1)
U5(f25_out1, s(z0), z1) → f18_out1(0)
f21_in(s(z0), z1) → U6(f44_in(z0, z1), s(z0), z1)
U6(f44_out1(z0, z1), s(z2), z3) → f21_out1(s(z1))
f44_in(z0, z1) → U7(f49_in(z0, z1), z0, z1)
U7(f49_out1(z0), z1, z2) → U8(f6_in(z0, z2), z1, z2, z0)
U8(f6_out1(z0), z1, z2, z3) → f44_out1(z3, z0)
f11_in(z0, z1) → U9(f18_in(z0, z1), f21_in(z0, z1), z0, z1)
U9(f18_out1(z0), z1, z2, z3) → f11_out1(z0)
U9(z0, f21_out1(z1), z2, z3) → f11_out2(z1)

Tuples:

F44_IN(z0, z1) → c16(U7'(f49_in(z0, z1), z0, z1), F49_IN(z0, z1))
F1_IN(z0, s(z1)) → c1(F6_IN(z0, z1))
F18_IN(s(z0), z1) → c1(F25_IN(z0, z1))
F6_IN(z0, z1) → c3(F11_IN(z0, z1))
F25_IN(s(z0), s(z1)) → c7(F25_IN(z0, z1))
F49_IN(s(z0), s(z1)) → c10(F49_IN(z0, z1))
F21_IN(s(z0), z1) → c14(F44_IN(z0, z1))
U7'(f49_out1(z0), z1, z2) → c17(F6_IN(z0, z2))
F11_IN(z0, z1) → c19(F18_IN(z0, z1), F21_IN(z0, z1))
F1_IN(z0, s(z1)) → c1
F18_IN(s(z0), z1) → c1

S tuples:none
K tuples:

F1_IN(z0, s(z1)) → c1(F6_IN(z0, z1))
F1_IN(z0, s(z1)) → c1
F21_IN(s(z0), z1) → c14(F44_IN(z0, z1))
F44_IN(z0, z1) → c16(U7'(f49_in(z0, z1), z0, z1), F49_IN(z0, z1))
U7'(f49_out1(z0), z1, z2) → c17(F6_IN(z0, z2))
F6_IN(z0, z1) → c3(F11_IN(z0, z1))
F11_IN(z0, z1) → c19(F18_IN(z0, z1), F21_IN(z0, z1))
F18_IN(s(z0), z1) → c1(F25_IN(z0, z1))
F18_IN(s(z0), z1) → c1
F25_IN(s(z0), s(z1)) → c7(F25_IN(z0, z1))
F49_IN(s(z0), s(z1)) → c10(F49_IN(z0, z1))

Defined Rule Symbols:

f1_in, U1, f6_in, U2, f25_in, U3, f49_in, U4, f18_in, U5, f21_in, U6, f44_in, U7, U8, f11_in, U9

Defined Pair Symbols:

F44_IN, F1_IN, F18_IN, F6_IN, F25_IN, F49_IN, F21_IN, U7', F11_IN

Compound Symbols:

c16, c1, c3, c7, c10, c14, c17, c19, c1

(33) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(34) BOUNDS(O(1), O(1))