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

(0) Obligation:

Clauses:

mult(X1, 0, 0).
mult(X, s(Y), Z) :- ','(mult(X, Y, W), sum(W, X, Z)).
sum(X, 0, X).
sum(X, s(Y), s(Z)) :- sum(X, Y, Z).

Query: mult(g,g,a)

(1) LPReorderTransformerProof (EQUIVALENT transformation)

Reordered facts before rules in definite LP [PROLOG].

(2) Obligation:

Clauses:

mult(X1, 0, 0).
sum(X, 0, X).
mult(X, s(Y), Z) :- ','(mult(X, Y, W), sum(W, X, Z)).
sum(X, s(Y), s(Z)) :- sum(X, Y, Z).

Query: mult(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: mult(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: mult(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | mult(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: true | mult(T6, 0, T3), SCOPE: 1, CLAUSE: 2\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: mult(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nT2 is ground\nX4 is free\nmult(T1, T2, T3) !=? mult(X4, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: mult(T6, 0, T3), SCOPE: 1, CLAUSE: 2\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: ','(mult(T14, T15, X18), sum(X18, T14, T17))\n\nT14 is ground\nT15 is ground\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: mult(T14, T15, X18)\n\nT14 is ground\nT15 is ground\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: sum(T20, T14, T17)\n\nT14 is ground\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: mult(T14, T15, X18), SCOPE: 2, CLAUSE: 0 | mult(T14, T15, X18), SCOPE: 2, CLAUSE: 2\n\nT14 is ground\nT15 is ground\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: true | mult(T25, 0, X18), SCOPE: 2, CLAUSE: 2\n\nT25 is ground\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: mult(T14, T15, X18), SCOPE: 2, CLAUSE: 2\n\nT14 is ground\nT15 is ground\nX18 is free\nX25 is free\nmult(T14, T15, X18) !=? mult(X25, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: mult(T25, 0, X18), SCOPE: 2, CLAUSE: 2\n\nT25 is ground\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: ','(mult(T31, T32, X41), sum(X41, T31, X42))\n\nT31 is ground\nT32 is ground\nX42 is free\nX41 is free", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: mult(T31, T32, X41)\n\nT31 is ground\nT32 is ground\nX41 is free", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: sum(T35, T31, X42)\n\nT31 is ground\nT35 is ground\nX42 is free", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: sum(T35, T31, X42), SCOPE: 3, CLAUSE: 1 | sum(T35, T31, X42), SCOPE: 3, CLAUSE: 3\n\nT31 is ground\nT35 is ground\nX42 is free", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: true | sum(T42, 0, X42), SCOPE: 3, CLAUSE: 3\n\nT42 is ground\nX42 is free", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: sum(T35, T31, X42), SCOPE: 3, CLAUSE: 3\n\nT31 is ground\nT35 is ground\nX42 is free\nX51 is free\nsum(T35, T31, X42) !=? sum(X51, 0, X51)", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: sum(T42, 0, X42), SCOPE: 3, CLAUSE: 3\n\nT42 is ground\nX42 is free", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: sum(T48, T49, X66)\n\nT48 is ground\nT49 is ground\nX66 is free", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: sum(T20, T14, T17), SCOPE: 4, CLAUSE: 1 | sum(T20, T14, T17), SCOPE: 4, CLAUSE: 3\n\nT14 is ground\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: true | sum(T56, 0, T17), SCOPE: 4, CLAUSE: 3\n\nT56 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: sum(T20, T14, T17), SCOPE: 4, CLAUSE: 3\n\nT14 is ground\nT20 is ground\nX73 is free\nsum(T20, T14, T17) !=? sum(X73, 0, X73)", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: sum(T56, 0, T17), SCOPE: 4, CLAUSE: 3\n\nT56 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: sum(T64, T65, T67)\n\nT64 is ground\nT65 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 68 [arrowhead = none ];
68 -> 4;

69 [label="EVAL with clause\nmult(X4, 0, 0).\nand substitutionT1 -> T6,\nX4 -> T6,\nT2 -> 0,\nT3 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 69 [arrowhead = none ];
69 -> 6;

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

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

72 [label="EVAL with clause\nmult(X15, s(X16), X17) :- ','(mult(X15, X16, X18), sum(X18, X15, X17)).\nand substitutionT1 -> T14,\nX15 -> T14,\nX16 -> T15,\nT2 -> s(T15),\nT3 -> T17,\nX17 -> T17,\nT16 -> T17", fontsize=14, style = filled, fillcolor = lightblue];
8 -> 72 [arrowhead = none ];
72 -> 14;

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

74 [label="BACKTRACK\nfor clause: mult(X, s(Y), Z) :- ','(mult(X, Y, W), sum(W, X, Z))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
9 -> 74 [arrowhead = none ];
74 -> 11;

75 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
14 -> 75 [arrowhead = none ];
75 -> 22;

76 [label="SPLIT 2\nnew knowledge:\nT14 is ground\nT15 is ground\nT20 is ground\nreplacements:X18 -> T20", fontsize=14, style = filled, fillcolor = violet];
14 -> 76 [arrowhead = none ];
76 -> 23;

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

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

79 [label="EVAL with clause\nmult(X25, 0, 0).\nand substitutionT14 -> T25,\nX25 -> T25,\nT15 -> 0,\nX18 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
29 -> 79 [arrowhead = none ];
79 -> 30;

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

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

82 [label="EVAL with clause\nmult(X38, s(X39), X40) :- ','(mult(X38, X39, X41), sum(X41, X38, X40)).\nand substitutionT14 -> T31,\nX38 -> T31,\nX39 -> T32,\nT15 -> s(T32),\nX18 -> X42,\nX40 -> X42", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 82 [arrowhead = none ];
82 -> 36;

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

84 [label="BACKTRACK\nfor clause: mult(X, s(Y), Z) :- ','(mult(X, Y, W), sum(W, X, Z))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
32 -> 84 [arrowhead = none ];
84 -> 34;

85 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
36 -> 85 [arrowhead = none ];
85 -> 39;

86 [label="SPLIT 2\nnew knowledge:\nT31 is ground\nT32 is ground\nT35 is ground\nreplacements:X41 -> T35", fontsize=14, style = filled, fillcolor = violet];
36 -> 86 [arrowhead = none ];
86 -> 40;

87 [label="INSTANCE with matching:\nT14 -> T31\nT15 -> T32\nX18 -> X41", fontsize=14, style = filled, fillcolor = lightgrey];
39 -> 87 [arrowhead = none , style=dashed];
87 -> 22[style=dashed];

88 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
40 -> 88 [arrowhead = none ];
88 -> 43;

89 [label="EVAL with clause\nsum(X51, 0, X51).\nand substitutionT35 -> T42,\nX51 -> T42,\nT31 -> 0,\nX42 -> T42", fontsize=14, style = filled, fillcolor = lightblue];
43 -> 89 [arrowhead = none ];
89 -> 44;

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

91 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
44 -> 91 [arrowhead = none ];
91 -> 48;

92 [label="EVAL with clause\nsum(X63, s(X64), s(X65)) :- sum(X63, X64, X65).\nand substitutionT35 -> T48,\nX63 -> T48,\nX64 -> T49,\nT31 -> s(T49),\nX65 -> X66,\nX42 -> s(X66)", fontsize=14, style = filled, fillcolor = lightblue];
47 -> 92 [arrowhead = none ];
92 -> 55;

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

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

95 [label="INSTANCE with matching:\nT35 -> T48\nT31 -> T49\nX42 -> X66", fontsize=14, style = filled, fillcolor = lightgrey];
55 -> 95 [arrowhead = none , style=dashed];
95 -> 40[style=dashed];

96 [label="EVAL with clause\nsum(X73, 0, X73).\nand substitutionT20 -> T56,\nX73 -> T56,\nT14 -> 0,\nT17 -> T56", fontsize=14, style = filled, fillcolor = lightblue];
57 -> 96 [arrowhead = none ];
96 -> 59;

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

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

99 [label="EVAL with clause\nsum(X83, s(X84), s(X85)) :- sum(X83, X84, X85).\nand substitutionT20 -> T64,\nX83 -> T64,\nX84 -> T65,\nT14 -> s(T65),\nX85 -> T67,\nT17 -> s(T67),\nT66 -> T67", fontsize=14, style = filled, fillcolor = lightblue];
61 -> 99 [arrowhead = none ];
99 -> 66;

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

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

102 [label="INSTANCE with matching:\nT20 -> T64\nT14 -> T65\nT17 -> T67", fontsize=14, style = filled, fillcolor = lightgrey];
66 -> 102 [arrowhead = none , style=dashed];
102 -> 23[style=dashed];

}

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, 0) → f2_out1(0)
f2_in(z0, s(z1)) → U1(f14_in(z0, z1), z0, s(z1))
U1(f14_out1(z0, z1), z2, s(z3)) → f2_out1(z1)
f23_in(z0, 0) → f23_out1(z0)
f23_in(z0, s(z1)) → U2(f23_in(z0, z1), z0, s(z1))
U2(f23_out1(z0), z1, s(z2)) → f23_out1(s(z0))
f22_in(z0, 0) → f22_out1(0)
f22_in(z0, s(z1)) → U3(f36_in(z0, z1), z0, s(z1))
U3(f36_out1(z0, z1), z2, s(z3)) → f22_out1(z1)
f40_in(z0, 0) → f40_out1(z0)
f40_in(z0, s(z1)) → U4(f40_in(z0, z1), z0, s(z1))
U4(f40_out1(z0), z1, s(z2)) → f40_out1(s(z0))
f14_in(z0, z1) → U5(f22_in(z0, z1), z0, z1)
U5(f22_out1(z0), z1, z2) → U6(f23_in(z0, z1), z1, z2, z0)
U6(f23_out1(z0), z1, z2, z3) → f14_out1(z3, z0)
f36_in(z0, z1) → U7(f22_in(z0, z1), z0, z1)
U7(f22_out1(z0), z1, z2) → U8(f40_in(z0, z1), z1, z2, z0)
U8(f40_out1(z0), z1, z2, z3) → f36_out1(z3, z0)

Tuples:

F2_IN(z0, s(z1)) → c1(U1'(f14_in(z0, z1), z0, s(z1)), F14_IN(z0, z1))
F23_IN(z0, s(z1)) → c4(U2'(f23_in(z0, z1), z0, s(z1)), F23_IN(z0, z1))
F22_IN(z0, s(z1)) → c7(U3'(f36_in(z0, z1), z0, s(z1)), F36_IN(z0, z1))
F40_IN(z0, s(z1)) → c10(U4'(f40_in(z0, z1), z0, s(z1)), F40_IN(z0, z1))
F14_IN(z0, z1) → c12(U5'(f22_in(z0, z1), z0, z1), F22_IN(z0, z1))
U5'(f22_out1(z0), z1, z2) → c13(U6'(f23_in(z0, z1), z1, z2, z0), F23_IN(z0, z1))
F36_IN(z0, z1) → c15(U7'(f22_in(z0, z1), z0, z1), F22_IN(z0, z1))
U7'(f22_out1(z0), z1, z2) → c16(U8'(f40_in(z0, z1), z1, z2, z0), F40_IN(z0, z1))

S tuples:

F2_IN(z0, s(z1)) → c1(U1'(f14_in(z0, z1), z0, s(z1)), F14_IN(z0, z1))
F23_IN(z0, s(z1)) → c4(U2'(f23_in(z0, z1), z0, s(z1)), F23_IN(z0, z1))
F22_IN(z0, s(z1)) → c7(U3'(f36_in(z0, z1), z0, s(z1)), F36_IN(z0, z1))
F40_IN(z0, s(z1)) → c10(U4'(f40_in(z0, z1), z0, s(z1)), F40_IN(z0, z1))
F14_IN(z0, z1) → c12(U5'(f22_in(z0, z1), z0, z1), F22_IN(z0, z1))
U5'(f22_out1(z0), z1, z2) → c13(U6'(f23_in(z0, z1), z1, z2, z0), F23_IN(z0, z1))
F36_IN(z0, z1) → c15(U7'(f22_in(z0, z1), z0, z1), F22_IN(z0, z1))
U7'(f22_out1(z0), z1, z2) → c16(U8'(f40_in(z0, z1), z1, z2, z0), F40_IN(z0, z1))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f23_in, U2, f22_in, U3, f40_in, U4, f14_in, U5, U6, f36_in, U7, U8

Defined Pair Symbols:

F2_IN, F23_IN, F22_IN, F40_IN, F14_IN, U5', F36_IN, U7'

Compound Symbols:

c1, c4, c7, c10, c12, c13, c15, c16

(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, 0) → f2_out1(0)
f2_in(z0, s(z1)) → U1(f14_in(z0, z1), z0, s(z1))
U1(f14_out1(z0, z1), z2, s(z3)) → f2_out1(z1)
f23_in(z0, 0) → f23_out1(z0)
f23_in(z0, s(z1)) → U2(f23_in(z0, z1), z0, s(z1))
U2(f23_out1(z0), z1, s(z2)) → f23_out1(s(z0))
f22_in(z0, 0) → f22_out1(0)
f22_in(z0, s(z1)) → U3(f36_in(z0, z1), z0, s(z1))
U3(f36_out1(z0, z1), z2, s(z3)) → f22_out1(z1)
f40_in(z0, 0) → f40_out1(z0)
f40_in(z0, s(z1)) → U4(f40_in(z0, z1), z0, s(z1))
U4(f40_out1(z0), z1, s(z2)) → f40_out1(s(z0))
f14_in(z0, z1) → U5(f22_in(z0, z1), z0, z1)
U5(f22_out1(z0), z1, z2) → U6(f23_in(z0, z1), z1, z2, z0)
U6(f23_out1(z0), z1, z2, z3) → f14_out1(z3, z0)
f36_in(z0, z1) → U7(f22_in(z0, z1), z0, z1)
U7(f22_out1(z0), z1, z2) → U8(f40_in(z0, z1), z1, z2, z0)
U8(f40_out1(z0), z1, z2, z3) → f36_out1(z3, z0)

Tuples:

F23_IN(z0, s(z1)) → c4(U2'(f23_in(z0, z1), z0, s(z1)), F23_IN(z0, z1))
F22_IN(z0, s(z1)) → c7(U3'(f36_in(z0, z1), z0, s(z1)), F36_IN(z0, z1))
F40_IN(z0, s(z1)) → c10(U4'(f40_in(z0, z1), z0, s(z1)), F40_IN(z0, z1))
F36_IN(z0, z1) → c15(U7'(f22_in(z0, z1), z0, z1), F22_IN(z0, z1))
F2_IN(z0, s(z1)) → c(U1'(f14_in(z0, z1), z0, s(z1)))
F2_IN(z0, s(z1)) → c(F14_IN(z0, z1))
F14_IN(z0, z1) → c(U5'(f22_in(z0, z1), z0, z1))
F14_IN(z0, z1) → c(F22_IN(z0, z1))
U5'(f22_out1(z0), z1, z2) → c(U6'(f23_in(z0, z1), z1, z2, z0))
U5'(f22_out1(z0), z1, z2) → c(F23_IN(z0, z1))
U7'(f22_out1(z0), z1, z2) → c(U8'(f40_in(z0, z1), z1, z2, z0))
U7'(f22_out1(z0), z1, z2) → c(F40_IN(z0, z1))

S tuples:

F23_IN(z0, s(z1)) → c4(U2'(f23_in(z0, z1), z0, s(z1)), F23_IN(z0, z1))
F22_IN(z0, s(z1)) → c7(U3'(f36_in(z0, z1), z0, s(z1)), F36_IN(z0, z1))
F40_IN(z0, s(z1)) → c10(U4'(f40_in(z0, z1), z0, s(z1)), F40_IN(z0, z1))
F36_IN(z0, z1) → c15(U7'(f22_in(z0, z1), z0, z1), F22_IN(z0, z1))
F2_IN(z0, s(z1)) → c(U1'(f14_in(z0, z1), z0, s(z1)))
F2_IN(z0, s(z1)) → c(F14_IN(z0, z1))
F14_IN(z0, z1) → c(U5'(f22_in(z0, z1), z0, z1))
F14_IN(z0, z1) → c(F22_IN(z0, z1))
U5'(f22_out1(z0), z1, z2) → c(U6'(f23_in(z0, z1), z1, z2, z0))
U5'(f22_out1(z0), z1, z2) → c(F23_IN(z0, z1))
U7'(f22_out1(z0), z1, z2) → c(U8'(f40_in(z0, z1), z1, z2, z0))
U7'(f22_out1(z0), z1, z2) → c(F40_IN(z0, z1))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f23_in, U2, f22_in, U3, f40_in, U4, f14_in, U5, U6, f36_in, U7, U8

Defined Pair Symbols:

F23_IN, F22_IN, F40_IN, F36_IN, F2_IN, F14_IN, U5', U7'

Compound Symbols:

c4, c7, c10, c15, c

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

Removed 6 trailing tuple parts

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, 0) → f2_out1(0)
f2_in(z0, s(z1)) → U1(f14_in(z0, z1), z0, s(z1))
U1(f14_out1(z0, z1), z2, s(z3)) → f2_out1(z1)
f23_in(z0, 0) → f23_out1(z0)
f23_in(z0, s(z1)) → U2(f23_in(z0, z1), z0, s(z1))
U2(f23_out1(z0), z1, s(z2)) → f23_out1(s(z0))
f22_in(z0, 0) → f22_out1(0)
f22_in(z0, s(z1)) → U3(f36_in(z0, z1), z0, s(z1))
U3(f36_out1(z0, z1), z2, s(z3)) → f22_out1(z1)
f40_in(z0, 0) → f40_out1(z0)
f40_in(z0, s(z1)) → U4(f40_in(z0, z1), z0, s(z1))
U4(f40_out1(z0), z1, s(z2)) → f40_out1(s(z0))
f14_in(z0, z1) → U5(f22_in(z0, z1), z0, z1)
U5(f22_out1(z0), z1, z2) → U6(f23_in(z0, z1), z1, z2, z0)
U6(f23_out1(z0), z1, z2, z3) → f14_out1(z3, z0)
f36_in(z0, z1) → U7(f22_in(z0, z1), z0, z1)
U7(f22_out1(z0), z1, z2) → U8(f40_in(z0, z1), z1, z2, z0)
U8(f40_out1(z0), z1, z2, z3) → f36_out1(z3, z0)

Tuples:

F36_IN(z0, z1) → c15(U7'(f22_in(z0, z1), z0, z1), F22_IN(z0, z1))
F2_IN(z0, s(z1)) → c(F14_IN(z0, z1))
F14_IN(z0, z1) → c(U5'(f22_in(z0, z1), z0, z1))
F14_IN(z0, z1) → c(F22_IN(z0, z1))
U5'(f22_out1(z0), z1, z2) → c(F23_IN(z0, z1))
U7'(f22_out1(z0), z1, z2) → c(F40_IN(z0, z1))
F23_IN(z0, s(z1)) → c4(F23_IN(z0, z1))
F22_IN(z0, s(z1)) → c7(F36_IN(z0, z1))
F40_IN(z0, s(z1)) → c10(F40_IN(z0, z1))
F2_IN(z0, s(z1)) → c
U5'(f22_out1(z0), z1, z2) → c
U7'(f22_out1(z0), z1, z2) → c

S tuples:

F36_IN(z0, z1) → c15(U7'(f22_in(z0, z1), z0, z1), F22_IN(z0, z1))
F2_IN(z0, s(z1)) → c(F14_IN(z0, z1))
F14_IN(z0, z1) → c(U5'(f22_in(z0, z1), z0, z1))
F14_IN(z0, z1) → c(F22_IN(z0, z1))
U5'(f22_out1(z0), z1, z2) → c(F23_IN(z0, z1))
U7'(f22_out1(z0), z1, z2) → c(F40_IN(z0, z1))
F23_IN(z0, s(z1)) → c4(F23_IN(z0, z1))
F22_IN(z0, s(z1)) → c7(F36_IN(z0, z1))
F40_IN(z0, s(z1)) → c10(F40_IN(z0, z1))
F2_IN(z0, s(z1)) → c
U5'(f22_out1(z0), z1, z2) → c
U7'(f22_out1(z0), z1, z2) → c

K tuples:none
Defined Rule Symbols:

f2_in, U1, f23_in, U2, f22_in, U3, f40_in, U4, f14_in, U5, U6, f36_in, U7, U8

Defined Pair Symbols:

F36_IN, F2_IN, F14_IN, U5', U7', F23_IN, F22_IN, F40_IN

Compound Symbols:

c15, c, c4, c7, c10, c

(9) CdtKnowledgeProof (EQUIVALENT transformation)

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

F2_IN(z0, s(z1)) → c(F14_IN(z0, z1))
F14_IN(z0, z1) → c(U5'(f22_in(z0, z1), z0, z1))
F14_IN(z0, z1) → c(F22_IN(z0, z1))
U5'(f22_out1(z0), z1, z2) → c(F23_IN(z0, z1))
F2_IN(z0, s(z1)) → c
U5'(f22_out1(z0), z1, z2) → c
F14_IN(z0, z1) → c(U5'(f22_in(z0, z1), z0, z1))
F14_IN(z0, z1) → c(F22_IN(z0, z1))
U5'(f22_out1(z0), z1, z2) → c(F23_IN(z0, z1))
U5'(f22_out1(z0), z1, z2) → c

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, 0) → f2_out1(0)
f2_in(z0, s(z1)) → U1(f14_in(z0, z1), z0, s(z1))
U1(f14_out1(z0, z1), z2, s(z3)) → f2_out1(z1)
f23_in(z0, 0) → f23_out1(z0)
f23_in(z0, s(z1)) → U2(f23_in(z0, z1), z0, s(z1))
U2(f23_out1(z0), z1, s(z2)) → f23_out1(s(z0))
f22_in(z0, 0) → f22_out1(0)
f22_in(z0, s(z1)) → U3(f36_in(z0, z1), z0, s(z1))
U3(f36_out1(z0, z1), z2, s(z3)) → f22_out1(z1)
f40_in(z0, 0) → f40_out1(z0)
f40_in(z0, s(z1)) → U4(f40_in(z0, z1), z0, s(z1))
U4(f40_out1(z0), z1, s(z2)) → f40_out1(s(z0))
f14_in(z0, z1) → U5(f22_in(z0, z1), z0, z1)
U5(f22_out1(z0), z1, z2) → U6(f23_in(z0, z1), z1, z2, z0)
U6(f23_out1(z0), z1, z2, z3) → f14_out1(z3, z0)
f36_in(z0, z1) → U7(f22_in(z0, z1), z0, z1)
U7(f22_out1(z0), z1, z2) → U8(f40_in(z0, z1), z1, z2, z0)
U8(f40_out1(z0), z1, z2, z3) → f36_out1(z3, z0)

Tuples:

F36_IN(z0, z1) → c15(U7'(f22_in(z0, z1), z0, z1), F22_IN(z0, z1))
F2_IN(z0, s(z1)) → c(F14_IN(z0, z1))
F14_IN(z0, z1) → c(U5'(f22_in(z0, z1), z0, z1))
F14_IN(z0, z1) → c(F22_IN(z0, z1))
U5'(f22_out1(z0), z1, z2) → c(F23_IN(z0, z1))
U7'(f22_out1(z0), z1, z2) → c(F40_IN(z0, z1))
F23_IN(z0, s(z1)) → c4(F23_IN(z0, z1))
F22_IN(z0, s(z1)) → c7(F36_IN(z0, z1))
F40_IN(z0, s(z1)) → c10(F40_IN(z0, z1))
F2_IN(z0, s(z1)) → c
U5'(f22_out1(z0), z1, z2) → c
U7'(f22_out1(z0), z1, z2) → c

S tuples:

F36_IN(z0, z1) → c15(U7'(f22_in(z0, z1), z0, z1), F22_IN(z0, z1))
U7'(f22_out1(z0), z1, z2) → c(F40_IN(z0, z1))
F23_IN(z0, s(z1)) → c4(F23_IN(z0, z1))
F22_IN(z0, s(z1)) → c7(F36_IN(z0, z1))
F40_IN(z0, s(z1)) → c10(F40_IN(z0, z1))
U7'(f22_out1(z0), z1, z2) → c

K tuples:

F2_IN(z0, s(z1)) → c(F14_IN(z0, z1))
F14_IN(z0, z1) → c(U5'(f22_in(z0, z1), z0, z1))
F14_IN(z0, z1) → c(F22_IN(z0, z1))
U5'(f22_out1(z0), z1, z2) → c(F23_IN(z0, z1))
F2_IN(z0, s(z1)) → c
U5'(f22_out1(z0), z1, z2) → c

Defined Rule Symbols:

f2_in, U1, f23_in, U2, f22_in, U3, f40_in, U4, f14_in, U5, U6, f36_in, U7, U8

Defined Pair Symbols:

F36_IN, F2_IN, F14_IN, U5', U7', F23_IN, F22_IN, F40_IN

Compound Symbols:

c15, c, c4, c7, c10, c

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

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

We considered the (Usable) Rules:

f22_in(z0, 0) → f22_out1(0)
f22_in(z0, s(z1)) → U3(f36_in(z0, z1), z0, s(z1))
f36_in(z0, z1) → U7(f22_in(z0, z1), z0, z1)
U3(f36_out1(z0, z1), z2, s(z3)) → f22_out1(z1)
U7(f22_out1(z0), z1, z2) → U8(f40_in(z0, z1), z1, z2, z0)
f40_in(z0, 0) → f40_out1(z0)
f40_in(z0, s(z1)) → U4(f40_in(z0, z1), z0, s(z1))
U8(f40_out1(z0), z1, z2, z3) → f36_out1(z3, z0)
U4(f40_out1(z0), z1, s(z2)) → f40_out1(s(z0))

And the Tuples:

F36_IN(z0, z1) → c15(U7'(f22_in(z0, z1), z0, z1), F22_IN(z0, z1))
F2_IN(z0, s(z1)) → c(F14_IN(z0, z1))
F14_IN(z0, z1) → c(U5'(f22_in(z0, z1), z0, z1))
F14_IN(z0, z1) → c(F22_IN(z0, z1))
U5'(f22_out1(z0), z1, z2) → c(F23_IN(z0, z1))
U7'(f22_out1(z0), z1, z2) → c(F40_IN(z0, z1))
F23_IN(z0, s(z1)) → c4(F23_IN(z0, z1))
F22_IN(z0, s(z1)) → c7(F36_IN(z0, z1))
F40_IN(z0, s(z1)) → c10(F40_IN(z0, z1))
F2_IN(z0, s(z1)) → c
U5'(f22_out1(z0), z1, z2) → c
U7'(f22_out1(z0), z1, z2) → c

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

POL(0) = 0   
POL(F14_IN(x₁, x₂)) = [1] + [3]x₁ + [3]x₂   
POL(F22_IN(x₁, x₂)) = 0   
POL(F23_IN(x₁, x₂)) = x₂   
POL(F2_IN(x₁, x₂)) = [3]x₁ + [3]x₂   
POL(F36_IN(x₁, x₂)) = 0   
POL(F40_IN(x₁, x₂)) = 0   
POL(U3(x₁, x₂, x₃)) = 0   
POL(U4(x₁, x₂, x₃)) = 0   
POL(U5'(x₁, x₂, x₃)) = [1] + [2]x₂ + x₃   
POL(U7(x₁, x₂, x₃)) = 0   
POL(U7'(x₁, x₂, x₃)) = 0   
POL(U8(x₁, x₂, x₃, x₄)) = 0   
POL(c) = 0   
POL(c(x₁)) = x₁   
POL(c10(x₁)) = x₁   
POL(c15(x₁, x₂)) = x₁ + x₂   
POL(c4(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(f22_in(x₁, x₂)) = 0   
POL(f22_out1(x₁)) = 0   
POL(f36_in(x₁, x₂)) = 0   
POL(f36_out1(x₁, x₂)) = 0   
POL(f40_in(x₁, x₂)) = x₁ + [3]x₂   
POL(f40_out1(x₁)) = 0   
POL(s(x₁)) = [1] + x₁   

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, 0) → f2_out1(0)
f2_in(z0, s(z1)) → U1(f14_in(z0, z1), z0, s(z1))
U1(f14_out1(z0, z1), z2, s(z3)) → f2_out1(z1)
f23_in(z0, 0) → f23_out1(z0)
f23_in(z0, s(z1)) → U2(f23_in(z0, z1), z0, s(z1))
U2(f23_out1(z0), z1, s(z2)) → f23_out1(s(z0))
f22_in(z0, 0) → f22_out1(0)
f22_in(z0, s(z1)) → U3(f36_in(z0, z1), z0, s(z1))
U3(f36_out1(z0, z1), z2, s(z3)) → f22_out1(z1)
f40_in(z0, 0) → f40_out1(z0)
f40_in(z0, s(z1)) → U4(f40_in(z0, z1), z0, s(z1))
U4(f40_out1(z0), z1, s(z2)) → f40_out1(s(z0))
f14_in(z0, z1) → U5(f22_in(z0, z1), z0, z1)
U5(f22_out1(z0), z1, z2) → U6(f23_in(z0, z1), z1, z2, z0)
U6(f23_out1(z0), z1, z2, z3) → f14_out1(z3, z0)
f36_in(z0, z1) → U7(f22_in(z0, z1), z0, z1)
U7(f22_out1(z0), z1, z2) → U8(f40_in(z0, z1), z1, z2, z0)
U8(f40_out1(z0), z1, z2, z3) → f36_out1(z3, z0)

Tuples:

F36_IN(z0, z1) → c15(U7'(f22_in(z0, z1), z0, z1), F22_IN(z0, z1))
F2_IN(z0, s(z1)) → c(F14_IN(z0, z1))
F14_IN(z0, z1) → c(U5'(f22_in(z0, z1), z0, z1))
F14_IN(z0, z1) → c(F22_IN(z0, z1))
U5'(f22_out1(z0), z1, z2) → c(F23_IN(z0, z1))
U7'(f22_out1(z0), z1, z2) → c(F40_IN(z0, z1))
F23_IN(z0, s(z1)) → c4(F23_IN(z0, z1))
F22_IN(z0, s(z1)) → c7(F36_IN(z0, z1))
F40_IN(z0, s(z1)) → c10(F40_IN(z0, z1))
F2_IN(z0, s(z1)) → c
U5'(f22_out1(z0), z1, z2) → c
U7'(f22_out1(z0), z1, z2) → c

S tuples:

F36_IN(z0, z1) → c15(U7'(f22_in(z0, z1), z0, z1), F22_IN(z0, z1))
U7'(f22_out1(z0), z1, z2) → c(F40_IN(z0, z1))
F22_IN(z0, s(z1)) → c7(F36_IN(z0, z1))
F40_IN(z0, s(z1)) → c10(F40_IN(z0, z1))
U7'(f22_out1(z0), z1, z2) → c

K tuples:

F2_IN(z0, s(z1)) → c(F14_IN(z0, z1))
F14_IN(z0, z1) → c(U5'(f22_in(z0, z1), z0, z1))
F14_IN(z0, z1) → c(F22_IN(z0, z1))
U5'(f22_out1(z0), z1, z2) → c(F23_IN(z0, z1))
F2_IN(z0, s(z1)) → c
U5'(f22_out1(z0), z1, z2) → c
F23_IN(z0, s(z1)) → c4(F23_IN(z0, z1))

Defined Rule Symbols:

f2_in, U1, f23_in, U2, f22_in, U3, f40_in, U4, f14_in, U5, U6, f36_in, U7, U8

Defined Pair Symbols:

F36_IN, F2_IN, F14_IN, U5', U7', F23_IN, F22_IN, F40_IN

Compound Symbols:

c15, c, c4, c7, c10, c

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

F36_IN(z0, z1) → c15(U7'(f22_in(z0, z1), z0, z1), F22_IN(z0, z1))
F22_IN(z0, s(z1)) → c7(F36_IN(z0, z1))

We considered the (Usable) Rules:

f22_in(z0, 0) → f22_out1(0)
f22_in(z0, s(z1)) → U3(f36_in(z0, z1), z0, s(z1))
f36_in(z0, z1) → U7(f22_in(z0, z1), z0, z1)
U3(f36_out1(z0, z1), z2, s(z3)) → f22_out1(z1)
U7(f22_out1(z0), z1, z2) → U8(f40_in(z0, z1), z1, z2, z0)
f40_in(z0, 0) → f40_out1(z0)
f40_in(z0, s(z1)) → U4(f40_in(z0, z1), z0, s(z1))
U8(f40_out1(z0), z1, z2, z3) → f36_out1(z3, z0)
U4(f40_out1(z0), z1, s(z2)) → f40_out1(s(z0))

And the Tuples:

F36_IN(z0, z1) → c15(U7'(f22_in(z0, z1), z0, z1), F22_IN(z0, z1))
F2_IN(z0, s(z1)) → c(F14_IN(z0, z1))
F14_IN(z0, z1) → c(U5'(f22_in(z0, z1), z0, z1))
F14_IN(z0, z1) → c(F22_IN(z0, z1))
U5'(f22_out1(z0), z1, z2) → c(F23_IN(z0, z1))
U7'(f22_out1(z0), z1, z2) → c(F40_IN(z0, z1))
F23_IN(z0, s(z1)) → c4(F23_IN(z0, z1))
F22_IN(z0, s(z1)) → c7(F36_IN(z0, z1))
F40_IN(z0, s(z1)) → c10(F40_IN(z0, z1))
F2_IN(z0, s(z1)) → c
U5'(f22_out1(z0), z1, z2) → c
U7'(f22_out1(z0), z1, z2) → c

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

POL(0) = 0   
POL(F14_IN(x₁, x₂)) = [2]x₂   
POL(F22_IN(x₁, x₂)) = [2]x₂   
POL(F23_IN(x₁, x₂)) = 0   
POL(F2_IN(x₁, x₂)) = x₁ + [2]x₂   
POL(F36_IN(x₁, x₂)) = [3] + [2]x₂   
POL(F40_IN(x₁, x₂)) = 0   
POL(U3(x₁, x₂, x₃)) = 0   
POL(U4(x₁, x₂, x₃)) = 0   
POL(U5'(x₁, x₂, x₃)) = x₃   
POL(U7(x₁, x₂, x₃)) = 0   
POL(U7'(x₁, x₂, x₃)) = 0   
POL(U8(x₁, x₂, x₃, x₄)) = 0   
POL(c) = 0   
POL(c(x₁)) = x₁   
POL(c10(x₁)) = x₁   
POL(c15(x₁, x₂)) = x₁ + x₂   
POL(c4(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(f22_in(x₁, x₂)) = 0   
POL(f22_out1(x₁)) = 0   
POL(f36_in(x₁, x₂)) = 0   
POL(f36_out1(x₁, x₂)) = 0   
POL(f40_in(x₁, x₂)) = 0   
POL(f40_out1(x₁)) = 0   
POL(s(x₁)) = [2] + x₁   

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, 0) → f2_out1(0)
f2_in(z0, s(z1)) → U1(f14_in(z0, z1), z0, s(z1))
U1(f14_out1(z0, z1), z2, s(z3)) → f2_out1(z1)
f23_in(z0, 0) → f23_out1(z0)
f23_in(z0, s(z1)) → U2(f23_in(z0, z1), z0, s(z1))
U2(f23_out1(z0), z1, s(z2)) → f23_out1(s(z0))
f22_in(z0, 0) → f22_out1(0)
f22_in(z0, s(z1)) → U3(f36_in(z0, z1), z0, s(z1))
U3(f36_out1(z0, z1), z2, s(z3)) → f22_out1(z1)
f40_in(z0, 0) → f40_out1(z0)
f40_in(z0, s(z1)) → U4(f40_in(z0, z1), z0, s(z1))
U4(f40_out1(z0), z1, s(z2)) → f40_out1(s(z0))
f14_in(z0, z1) → U5(f22_in(z0, z1), z0, z1)
U5(f22_out1(z0), z1, z2) → U6(f23_in(z0, z1), z1, z2, z0)
U6(f23_out1(z0), z1, z2, z3) → f14_out1(z3, z0)
f36_in(z0, z1) → U7(f22_in(z0, z1), z0, z1)
U7(f22_out1(z0), z1, z2) → U8(f40_in(z0, z1), z1, z2, z0)
U8(f40_out1(z0), z1, z2, z3) → f36_out1(z3, z0)

Tuples:

F36_IN(z0, z1) → c15(U7'(f22_in(z0, z1), z0, z1), F22_IN(z0, z1))
F2_IN(z0, s(z1)) → c(F14_IN(z0, z1))
F14_IN(z0, z1) → c(U5'(f22_in(z0, z1), z0, z1))
F14_IN(z0, z1) → c(F22_IN(z0, z1))
U5'(f22_out1(z0), z1, z2) → c(F23_IN(z0, z1))
U7'(f22_out1(z0), z1, z2) → c(F40_IN(z0, z1))
F23_IN(z0, s(z1)) → c4(F23_IN(z0, z1))
F22_IN(z0, s(z1)) → c7(F36_IN(z0, z1))
F40_IN(z0, s(z1)) → c10(F40_IN(z0, z1))
F2_IN(z0, s(z1)) → c
U5'(f22_out1(z0), z1, z2) → c
U7'(f22_out1(z0), z1, z2) → c

S tuples:

U7'(f22_out1(z0), z1, z2) → c(F40_IN(z0, z1))
F40_IN(z0, s(z1)) → c10(F40_IN(z0, z1))
U7'(f22_out1(z0), z1, z2) → c

K tuples:

F2_IN(z0, s(z1)) → c(F14_IN(z0, z1))
F14_IN(z0, z1) → c(U5'(f22_in(z0, z1), z0, z1))
F14_IN(z0, z1) → c(F22_IN(z0, z1))
U5'(f22_out1(z0), z1, z2) → c(F23_IN(z0, z1))
F2_IN(z0, s(z1)) → c
U5'(f22_out1(z0), z1, z2) → c
F23_IN(z0, s(z1)) → c4(F23_IN(z0, z1))
F36_IN(z0, z1) → c15(U7'(f22_in(z0, z1), z0, z1), F22_IN(z0, z1))
F22_IN(z0, s(z1)) → c7(F36_IN(z0, z1))

Defined Rule Symbols:

f2_in, U1, f23_in, U2, f22_in, U3, f40_in, U4, f14_in, U5, U6, f36_in, U7, U8

Defined Pair Symbols:

F36_IN, F2_IN, F14_IN, U5', U7', F23_IN, F22_IN, F40_IN

Compound Symbols:

c15, c, c4, c7, c10, c

(15) CdtKnowledgeProof (EQUIVALENT transformation)

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

U7'(f22_out1(z0), z1, z2) → c(F40_IN(z0, z1))
U7'(f22_out1(z0), z1, z2) → c

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, 0) → f2_out1(0)
f2_in(z0, s(z1)) → U1(f14_in(z0, z1), z0, s(z1))
U1(f14_out1(z0, z1), z2, s(z3)) → f2_out1(z1)
f23_in(z0, 0) → f23_out1(z0)
f23_in(z0, s(z1)) → U2(f23_in(z0, z1), z0, s(z1))
U2(f23_out1(z0), z1, s(z2)) → f23_out1(s(z0))
f22_in(z0, 0) → f22_out1(0)
f22_in(z0, s(z1)) → U3(f36_in(z0, z1), z0, s(z1))
U3(f36_out1(z0, z1), z2, s(z3)) → f22_out1(z1)
f40_in(z0, 0) → f40_out1(z0)
f40_in(z0, s(z1)) → U4(f40_in(z0, z1), z0, s(z1))
U4(f40_out1(z0), z1, s(z2)) → f40_out1(s(z0))
f14_in(z0, z1) → U5(f22_in(z0, z1), z0, z1)
U5(f22_out1(z0), z1, z2) → U6(f23_in(z0, z1), z1, z2, z0)
U6(f23_out1(z0), z1, z2, z3) → f14_out1(z3, z0)
f36_in(z0, z1) → U7(f22_in(z0, z1), z0, z1)
U7(f22_out1(z0), z1, z2) → U8(f40_in(z0, z1), z1, z2, z0)
U8(f40_out1(z0), z1, z2, z3) → f36_out1(z3, z0)

Tuples:

F36_IN(z0, z1) → c15(U7'(f22_in(z0, z1), z0, z1), F22_IN(z0, z1))
F2_IN(z0, s(z1)) → c(F14_IN(z0, z1))
F14_IN(z0, z1) → c(U5'(f22_in(z0, z1), z0, z1))
F14_IN(z0, z1) → c(F22_IN(z0, z1))
U5'(f22_out1(z0), z1, z2) → c(F23_IN(z0, z1))
U7'(f22_out1(z0), z1, z2) → c(F40_IN(z0, z1))
F23_IN(z0, s(z1)) → c4(F23_IN(z0, z1))
F22_IN(z0, s(z1)) → c7(F36_IN(z0, z1))
F40_IN(z0, s(z1)) → c10(F40_IN(z0, z1))
F2_IN(z0, s(z1)) → c
U5'(f22_out1(z0), z1, z2) → c
U7'(f22_out1(z0), z1, z2) → c

S tuples:

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

K tuples:

F2_IN(z0, s(z1)) → c(F14_IN(z0, z1))
F14_IN(z0, z1) → c(U5'(f22_in(z0, z1), z0, z1))
F14_IN(z0, z1) → c(F22_IN(z0, z1))
U5'(f22_out1(z0), z1, z2) → c(F23_IN(z0, z1))
F2_IN(z0, s(z1)) → c
U5'(f22_out1(z0), z1, z2) → c
F23_IN(z0, s(z1)) → c4(F23_IN(z0, z1))
F36_IN(z0, z1) → c15(U7'(f22_in(z0, z1), z0, z1), F22_IN(z0, z1))
F22_IN(z0, s(z1)) → c7(F36_IN(z0, z1))
U7'(f22_out1(z0), z1, z2) → c(F40_IN(z0, z1))
U7'(f22_out1(z0), z1, z2) → c

Defined Rule Symbols:

f2_in, U1, f23_in, U2, f22_in, U3, f40_in, U4, f14_in, U5, U6, f36_in, U7, U8

Defined Pair Symbols:

F36_IN, F2_IN, F14_IN, U5', U7', F23_IN, F22_IN, F40_IN

Compound Symbols:

c15, c, c4, c7, c10, c

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

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

We considered the (Usable) Rules:

f22_in(z0, 0) → f22_out1(0)
f22_in(z0, s(z1)) → U3(f36_in(z0, z1), z0, s(z1))
f36_in(z0, z1) → U7(f22_in(z0, z1), z0, z1)
U3(f36_out1(z0, z1), z2, s(z3)) → f22_out1(z1)
U7(f22_out1(z0), z1, z2) → U8(f40_in(z0, z1), z1, z2, z0)
f40_in(z0, 0) → f40_out1(z0)
f40_in(z0, s(z1)) → U4(f40_in(z0, z1), z0, s(z1))
U8(f40_out1(z0), z1, z2, z3) → f36_out1(z3, z0)
U4(f40_out1(z0), z1, s(z2)) → f40_out1(s(z0))

And the Tuples:

F36_IN(z0, z1) → c15(U7'(f22_in(z0, z1), z0, z1), F22_IN(z0, z1))
F2_IN(z0, s(z1)) → c(F14_IN(z0, z1))
F14_IN(z0, z1) → c(U5'(f22_in(z0, z1), z0, z1))
F14_IN(z0, z1) → c(F22_IN(z0, z1))
U5'(f22_out1(z0), z1, z2) → c(F23_IN(z0, z1))
U7'(f22_out1(z0), z1, z2) → c(F40_IN(z0, z1))
F23_IN(z0, s(z1)) → c4(F23_IN(z0, z1))
F22_IN(z0, s(z1)) → c7(F36_IN(z0, z1))
F40_IN(z0, s(z1)) → c10(F40_IN(z0, z1))
F2_IN(z0, s(z1)) → c
U5'(f22_out1(z0), z1, z2) → c
U7'(f22_out1(z0), z1, z2) → c

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

POL(0) = 0   
POL(F14_IN(x₁, x₂)) = [1] + x₁ + x₂ + x₂² + x₁·x₂ + x₁²   
POL(F22_IN(x₁, x₂)) = x₁·x₂   
POL(F23_IN(x₁, x₂)) = 0   
POL(F2_IN(x₁, x₂)) = x₁ + x₂² + x₁·x₂ + x₁²   
POL(F36_IN(x₁, x₂)) = x₁ + x₁·x₂   
POL(F40_IN(x₁, x₂)) = x₂   
POL(U3(x₁, x₂, x₃)) = 0   
POL(U4(x₁, x₂, x₃)) = 0   
POL(U5'(x₁, x₂, x₃)) = x₃²   
POL(U7(x₁, x₂, x₃)) = 0   
POL(U7'(x₁, x₂, x₃)) = x₂   
POL(U8(x₁, x₂, x₃, x₄)) = 0   
POL(c) = 0   
POL(c(x₁)) = x₁   
POL(c10(x₁)) = x₁   
POL(c15(x₁, x₂)) = x₁ + x₂   
POL(c4(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(f22_in(x₁, x₂)) = 0   
POL(f22_out1(x₁)) = 0   
POL(f36_in(x₁, x₂)) = 0   
POL(f36_out1(x₁, x₂)) = x₂   
POL(f40_in(x₁, x₂)) = 0   
POL(f40_out1(x₁)) = 0   
POL(s(x₁)) = [1] + x₁   

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, 0) → f2_out1(0)
f2_in(z0, s(z1)) → U1(f14_in(z0, z1), z0, s(z1))
U1(f14_out1(z0, z1), z2, s(z3)) → f2_out1(z1)
f23_in(z0, 0) → f23_out1(z0)
f23_in(z0, s(z1)) → U2(f23_in(z0, z1), z0, s(z1))
U2(f23_out1(z0), z1, s(z2)) → f23_out1(s(z0))
f22_in(z0, 0) → f22_out1(0)
f22_in(z0, s(z1)) → U3(f36_in(z0, z1), z0, s(z1))
U3(f36_out1(z0, z1), z2, s(z3)) → f22_out1(z1)
f40_in(z0, 0) → f40_out1(z0)
f40_in(z0, s(z1)) → U4(f40_in(z0, z1), z0, s(z1))
U4(f40_out1(z0), z1, s(z2)) → f40_out1(s(z0))
f14_in(z0, z1) → U5(f22_in(z0, z1), z0, z1)
U5(f22_out1(z0), z1, z2) → U6(f23_in(z0, z1), z1, z2, z0)
U6(f23_out1(z0), z1, z2, z3) → f14_out1(z3, z0)
f36_in(z0, z1) → U7(f22_in(z0, z1), z0, z1)
U7(f22_out1(z0), z1, z2) → U8(f40_in(z0, z1), z1, z2, z0)
U8(f40_out1(z0), z1, z2, z3) → f36_out1(z3, z0)

Tuples:

F36_IN(z0, z1) → c15(U7'(f22_in(z0, z1), z0, z1), F22_IN(z0, z1))
F2_IN(z0, s(z1)) → c(F14_IN(z0, z1))
F14_IN(z0, z1) → c(U5'(f22_in(z0, z1), z0, z1))
F14_IN(z0, z1) → c(F22_IN(z0, z1))
U5'(f22_out1(z0), z1, z2) → c(F23_IN(z0, z1))
U7'(f22_out1(z0), z1, z2) → c(F40_IN(z0, z1))
F23_IN(z0, s(z1)) → c4(F23_IN(z0, z1))
F22_IN(z0, s(z1)) → c7(F36_IN(z0, z1))
F40_IN(z0, s(z1)) → c10(F40_IN(z0, z1))
F2_IN(z0, s(z1)) → c
U5'(f22_out1(z0), z1, z2) → c
U7'(f22_out1(z0), z1, z2) → c

S tuples:none
K tuples:

F2_IN(z0, s(z1)) → c(F14_IN(z0, z1))
F14_IN(z0, z1) → c(U5'(f22_in(z0, z1), z0, z1))
F14_IN(z0, z1) → c(F22_IN(z0, z1))
U5'(f22_out1(z0), z1, z2) → c(F23_IN(z0, z1))
F2_IN(z0, s(z1)) → c
U5'(f22_out1(z0), z1, z2) → c
F23_IN(z0, s(z1)) → c4(F23_IN(z0, z1))
F36_IN(z0, z1) → c15(U7'(f22_in(z0, z1), z0, z1), F22_IN(z0, z1))
F22_IN(z0, s(z1)) → c7(F36_IN(z0, z1))
U7'(f22_out1(z0), z1, z2) → c(F40_IN(z0, z1))
U7'(f22_out1(z0), z1, z2) → c
F40_IN(z0, s(z1)) → c10(F40_IN(z0, z1))

Defined Rule Symbols:

f2_in, U1, f23_in, U2, f22_in, U3, f40_in, U4, f14_in, U5, U6, f36_in, U7, U8

Defined Pair Symbols:

F36_IN, F2_IN, F14_IN, U5', U7', F23_IN, F22_IN, F40_IN

Compound Symbols:

c15, c, c4, c7, c10, c

(19) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(20) BOUNDS(O(1), O(1))

(21) 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: mult(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
3 [label="3: mult(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | mult(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: true | mult(T5, 0, T3), SCOPE: 1, CLAUSE: 2\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: mult(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nT2 is ground\nX3 is free\nmult(T1, T2, T3) !=? mult(X3, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: mult(T5, 0, T3), SCOPE: 1, CLAUSE: 2\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(mult(T10, T11, X13), sum(X13, T10, T13))\n\nT10 is ground\nT11 is ground\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ','(mult(T10, T11, X13), sum(X13, T10, T13)), SCOPE: 2, CLAUSE: 0 | ','(mult(T10, T11, X13), sum(X13, T10, T13)), SCOPE: 2, CLAUSE: 2\n\nT10 is ground\nT11 is ground\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: sum(0, T16, T13) | ','(mult(T16, 0, X13), sum(X13, T16, T13)), SCOPE: 2, CLAUSE: 2\n\nT16 is ground\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(mult(T10, T11, X13), sum(X13, T10, T13)), SCOPE: 2, CLAUSE: 2\n\nT10 is ground\nT11 is ground\nX13 is free\nX16 is free\nmult(T10, T11, X13) !=? mult(X16, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: sum(0, T16, T13)\n\nT16 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: ','(mult(T16, 0, X13), sum(X13, T16, T13)), SCOPE: 2, CLAUSE: 2\n\nT16 is ground\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: sum(0, T16, T13), SCOPE: 3, CLAUSE: 1 | sum(0, T16, T13), SCOPE: 3, CLAUSE: 3\n\nT16 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: true | sum(0, 0, T13), SCOPE: 3, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: sum(0, T16, T13), SCOPE: 3, CLAUSE: 3\n\nT16 is ground\nX23 is free\nsum(0, T16, T13) !=? sum(X23, 0, X23)", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: sum(0, 0, T13), SCOPE: 3, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: sum(0, T21, T23)\n\nT21 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: ','(','(mult(T29, T30, X53), sum(X53, T29, X54)), sum(X54, T29, T13))\n\nT29 is ground\nT30 is ground\nX54 is free\nX53 is free", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: mult(T29, T30, X53)\n\nT29 is ground\nT30 is ground\nX53 is free", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: ','(sum(T33, T29, X54), sum(X54, T29, T13))\n\nT29 is ground\nT33 is ground\nX54 is free", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: mult(T29, T30, X53), SCOPE: 4, CLAUSE: 0 | mult(T29, T30, X53), SCOPE: 4, CLAUSE: 2\n\nT29 is ground\nT30 is ground\nX53 is free", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: true | mult(T38, 0, X53), SCOPE: 4, CLAUSE: 2\n\nT38 is ground\nX53 is free", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: mult(T29, T30, X53), SCOPE: 4, CLAUSE: 2\n\nT29 is ground\nT30 is ground\nX53 is free\nX61 is free\nmult(T29, T30, X53) !=? mult(X61, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: mult(T38, 0, X53), SCOPE: 4, CLAUSE: 2\n\nT38 is ground\nX53 is free", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: ','(mult(T44, T45, X77), sum(X77, T44, X78))\n\nT44 is ground\nT45 is ground\nX78 is free\nX77 is free", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: mult(T44, T45, X77)\n\nT44 is ground\nT45 is ground\nX77 is free", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: sum(T48, T44, X78)\n\nT44 is ground\nT48 is ground\nX78 is free", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: sum(T48, T44, X78), SCOPE: 5, CLAUSE: 1 | sum(T48, T44, X78), SCOPE: 5, CLAUSE: 3\n\nT44 is ground\nT48 is ground\nX78 is free", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: true | sum(T55, 0, X78), SCOPE: 5, CLAUSE: 3\n\nT55 is ground\nX78 is free", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: sum(T48, T44, X78), SCOPE: 5, CLAUSE: 3\n\nT44 is ground\nT48 is ground\nX78 is free\nX87 is free\nsum(T48, T44, X78) !=? sum(X87, 0, X87)", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: sum(T55, 0, X78), SCOPE: 5, CLAUSE: 3\n\nT55 is ground\nX78 is free", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: sum(T61, T62, X102)\n\nT61 is ground\nT62 is ground\nX102 is free", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: sum(T33, T29, X54)\n\nT29 is ground\nT33 is ground\nX54 is free", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: sum(T67, T29, T13)\n\nT29 is ground\nT67 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: sum(T67, T29, T13), SCOPE: 6, CLAUSE: 1 | sum(T67, T29, T13), SCOPE: 6, CLAUSE: 3\n\nT29 is ground\nT67 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: true | sum(T74, 0, T13), SCOPE: 6, CLAUSE: 3\n\nT74 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: sum(T67, T29, T13), SCOPE: 6, CLAUSE: 3\n\nT29 is ground\nT67 is ground\nX113 is free\nsum(T67, T29, T13) !=? sum(X113, 0, X113)", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: sum(T74, 0, T13), SCOPE: 6, CLAUSE: 3\n\nT74 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: sum(T82, T83, T85)\n\nT82 is ground\nT83 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 84 [arrowhead = none ];
84 -> 3;

85 [label="EVAL with clause\nmult(X3, 0, 0).\nand substitutionT1 -> T5,\nX3 -> T5,\nT2 -> 0,\nT3 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
3 -> 85 [arrowhead = none ];
85 -> 5;

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

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

88 [label="EVAL with clause\nmult(X10, s(X11), X12) :- ','(mult(X10, X11, X13), sum(X13, X10, X12)).\nand substitutionT1 -> T10,\nX10 -> T10,\nX11 -> T11,\nT2 -> s(T11),\nT3 -> T13,\nX12 -> T13,\nT12 -> T13", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 88 [arrowhead = none ];
88 -> 13;

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

90 [label="BACKTRACK\nfor clause: mult(X, s(Y), Z) :- ','(mult(X, Y, W), sum(W, X, Z))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
10 -> 90 [arrowhead = none ];
90 -> 12;

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

92 [label="EVAL with clause\nmult(X16, 0, 0).\nand substitutionT10 -> T16,\nX16 -> T16,\nT11 -> 0,\nX13 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 92 [arrowhead = none ];
92 -> 18;

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

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

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

96 [label="EVAL with clause\nmult(X50, s(X51), X52) :- ','(mult(X50, X51, X53), sum(X53, X50, X52)).\nand substitutionT10 -> T29,\nX50 -> T29,\nX51 -> T30,\nT11 -> s(T30),\nX13 -> X54,\nX52 -> X54", fontsize=14, style = filled, fillcolor = lightblue];
19 -> 96 [arrowhead = none ];
96 -> 41;

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

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

99 [label="BACKTRACK\nfor clause: mult(X, s(Y), Z) :- ','(mult(X, Y, W), sum(W, X, Z))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
21 -> 99 [arrowhead = none ];
99 -> 37;

100 [label="EVAL with clause\nsum(X23, 0, X23).\nand substitutionX23 -> 0,\nT16 -> 0,\nT13 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
24 -> 100 [arrowhead = none ];
100 -> 25;

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

102 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
25 -> 102 [arrowhead = none ];
102 -> 27;

103 [label="EVAL with clause\nsum(X33, s(X34), s(X35)) :- sum(X33, X34, X35).\nand substitutionX33 -> 0,\nX34 -> T21,\nT16 -> s(T21),\nX35 -> T23,\nT13 -> s(T23),\nT22 -> T23", fontsize=14, style = filled, fillcolor = lightblue];
26 -> 103 [arrowhead = none ];
103 -> 33;

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

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

106 [label="INSTANCE with matching:\nT16 -> T21\nT13 -> T23", fontsize=14, style = filled, fillcolor = lightgrey];
33 -> 106 [arrowhead = none , style=dashed];
106 -> 20[style=dashed];

107 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
41 -> 107 [arrowhead = none ];
107 -> 45;

108 [label="SPLIT 2\nnew knowledge:\nT29 is ground\nT30 is ground\nT33 is ground\nreplacements:X53 -> T33", fontsize=14, style = filled, fillcolor = violet];
41 -> 108 [arrowhead = none ];
108 -> 46;

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

110 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
46 -> 110 [arrowhead = none ];
110 -> 75;

111 [label="SPLIT 2\nnew knowledge:\nT33 is ground\nT29 is ground\nT67 is ground\nreplacements:X54 -> T67", fontsize=14, style = filled, fillcolor = violet];
46 -> 111 [arrowhead = none ];
111 -> 76;

112 [label="EVAL with clause\nmult(X61, 0, 0).\nand substitutionT29 -> T38,\nX61 -> T38,\nT30 -> 0,\nX53 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
50 -> 112 [arrowhead = none ];
112 -> 51;

113 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
50 -> 113 [arrowhead = none ];
113 -> 52;

114 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
51 -> 114 [arrowhead = none ];
114 -> 53;

115 [label="EVAL with clause\nmult(X74, s(X75), X76) :- ','(mult(X74, X75, X77), sum(X77, X74, X76)).\nand substitutionT29 -> T44,\nX74 -> T44,\nX75 -> T45,\nT30 -> s(T45),\nX53 -> X78,\nX76 -> X78", fontsize=14, style = filled, fillcolor = lightblue];
52 -> 115 [arrowhead = none ];
115 -> 58;

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

117 [label="BACKTRACK\nfor clause: mult(X, s(Y), Z) :- ','(mult(X, Y, W), sum(W, X, Z))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
53 -> 117 [arrowhead = none ];
117 -> 54;

118 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
58 -> 118 [arrowhead = none ];
118 -> 64;

119 [label="SPLIT 2\nnew knowledge:\nT44 is ground\nT45 is ground\nT48 is ground\nreplacements:X77 -> T48", fontsize=14, style = filled, fillcolor = violet];
58 -> 119 [arrowhead = none ];
119 -> 65;

120 [label="INSTANCE with matching:\nT29 -> T44\nT30 -> T45\nX53 -> X77", fontsize=14, style = filled, fillcolor = lightgrey];
64 -> 120 [arrowhead = none , style=dashed];
120 -> 45[style=dashed];

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

122 [label="EVAL with clause\nsum(X87, 0, X87).\nand substitutionT48 -> T55,\nX87 -> T55,\nT44 -> 0,\nX78 -> T55", fontsize=14, style = filled, fillcolor = lightblue];
68 -> 122 [arrowhead = none ];
122 -> 69;

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

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

125 [label="EVAL with clause\nsum(X99, s(X100), s(X101)) :- sum(X99, X100, X101).\nand substitutionT48 -> T61,\nX99 -> T61,\nX100 -> T62,\nT44 -> s(T62),\nX101 -> X102,\nX78 -> s(X102)", fontsize=14, style = filled, fillcolor = lightblue];
70 -> 125 [arrowhead = none ];
125 -> 73;

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

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

128 [label="INSTANCE with matching:\nT48 -> T61\nT44 -> T62\nX78 -> X102", fontsize=14, style = filled, fillcolor = lightgrey];
73 -> 128 [arrowhead = none , style=dashed];
128 -> 65[style=dashed];

129 [label="INSTANCE with matching:\nT48 -> T33\nT44 -> T29\nX78 -> X54", fontsize=14, style = filled, fillcolor = lightgrey];
75 -> 129 [arrowhead = none , style=dashed];
129 -> 65[style=dashed];

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

131 [label="EVAL with clause\nsum(X113, 0, X113).\nand substitutionT67 -> T74,\nX113 -> T74,\nT29 -> 0,\nT13 -> T74", fontsize=14, style = filled, fillcolor = lightblue];
77 -> 131 [arrowhead = none ];
131 -> 78;

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

133 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
78 -> 133 [arrowhead = none ];
133 -> 80;

134 [label="EVAL with clause\nsum(X123, s(X124), s(X125)) :- sum(X123, X124, X125).\nand substitutionT67 -> T82,\nX123 -> T82,\nX124 -> T83,\nT29 -> s(T83),\nX125 -> T85,\nT13 -> s(T85),\nT84 -> T85", fontsize=14, style = filled, fillcolor = lightblue];
79 -> 134 [arrowhead = none ];
134 -> 82;

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

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

137 [label="INSTANCE with matching:\nT67 -> T82\nT29 -> T83\nT13 -> T85", fontsize=14, style = filled, fillcolor = lightgrey];
82 -> 137 [arrowhead = none , style=dashed];
137 -> 76[style=dashed];

}

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, 0) → f1_out1(0)
f1_in(z0, s(0)) → U1(f18_in(z0), z0, s(0))
f1_in(z0, s(s(z1))) → U2(f41_in(z0, z1), z0, s(s(z1)))
U1(f18_out1(z0), z1, s(0)) → f1_out1(z0)
U1(f18_out2(z0, z1), z2, s(0)) → f1_out1(z1)
U2(f41_out1(z0, z1, z2), z3, s(s(z4))) → f1_out1(z2)
f65_in(z0, 0) → f65_out1(z0)
f65_in(z0, s(z1)) → U3(f65_in(z0, z1), z0, s(z1))
U3(f65_out1(z0), z1, s(z2)) → f65_out1(s(z0))
f20_in(0) → f20_out1(0)
f20_in(s(z0)) → U4(f20_in(z0), s(z0))
U4(f20_out1(z0), s(z1)) → f20_out1(s(z0))
f45_in(z0, 0) → f45_out1(0)
f45_in(z0, s(z1)) → U5(f58_in(z0, z1), z0, s(z1))
U5(f58_out1(z0, z1), z2, s(z3)) → f45_out1(z1)
f76_in(z0, 0) → f76_out1(z0)
f76_in(z0, s(z1)) → U6(f76_in(z0, z1), z0, s(z1))
U6(f76_out1(z0), z1, s(z2)) → f76_out1(s(z0))
f41_in(z0, z1) → U7(f45_in(z0, z1), z0, z1)
U7(f45_out1(z0), z1, z2) → U8(f46_in(z0, z1), z1, z2, z0)
U8(f46_out1(z0, z1), z2, z3, z4) → f41_out1(z4, z0, z1)
f46_in(z0, z1) → U9(f65_in(z0, z1), z0, z1)
U9(f65_out1(z0), z1, z2) → U10(f76_in(z0, z2), z1, z2, z0)
U10(f76_out1(z0), z1, z2, z3) → f46_out1(z3, z0)
f58_in(z0, z1) → U11(f45_in(z0, z1), z0, z1)
U11(f45_out1(z0), z1, z2) → U12(f65_in(z0, z1), z1, z2, z0)
U12(f65_out1(z0), z1, z2, z3) → f58_out1(z3, z0)
f18_in(z0) → U13(f20_in(z0), f21_in(z0), z0)
U13(f20_out1(z0), z1, z2) → f18_out1(z0)
U13(z0, f21_out1(z1, z2), z3) → f18_out2(z1, z2)

Tuples:

F1_IN(z0, s(0)) → c1(U1'(f18_in(z0), z0, s(0)), F18_IN(z0))
F1_IN(z0, s(s(z1))) → c2(U2'(f41_in(z0, z1), z0, s(s(z1))), F41_IN(z0, z1))
F65_IN(z0, s(z1)) → c7(U3'(f65_in(z0, z1), z0, s(z1)), F65_IN(z0, z1))
F20_IN(s(z0)) → c10(U4'(f20_in(z0), s(z0)), F20_IN(z0))
F45_IN(z0, s(z1)) → c13(U5'(f58_in(z0, z1), z0, s(z1)), F58_IN(z0, z1))
F76_IN(z0, s(z1)) → c16(U6'(f76_in(z0, z1), z0, s(z1)), F76_IN(z0, z1))
F41_IN(z0, z1) → c18(U7'(f45_in(z0, z1), z0, z1), F45_IN(z0, z1))
U7'(f45_out1(z0), z1, z2) → c19(U8'(f46_in(z0, z1), z1, z2, z0), F46_IN(z0, z1))
F46_IN(z0, z1) → c21(U9'(f65_in(z0, z1), z0, z1), F65_IN(z0, z1))
U9'(f65_out1(z0), z1, z2) → c22(U10'(f76_in(z0, z2), z1, z2, z0), F76_IN(z0, z2))
F58_IN(z0, z1) → c24(U11'(f45_in(z0, z1), z0, z1), F45_IN(z0, z1))
U11'(f45_out1(z0), z1, z2) → c25(U12'(f65_in(z0, z1), z1, z2, z0), F65_IN(z0, z1))
F18_IN(z0) → c27(U13'(f20_in(z0), f21_in(z0), z0), F20_IN(z0))

S tuples:

F1_IN(z0, s(0)) → c1(U1'(f18_in(z0), z0, s(0)), F18_IN(z0))
F1_IN(z0, s(s(z1))) → c2(U2'(f41_in(z0, z1), z0, s(s(z1))), F41_IN(z0, z1))
F65_IN(z0, s(z1)) → c7(U3'(f65_in(z0, z1), z0, s(z1)), F65_IN(z0, z1))
F20_IN(s(z0)) → c10(U4'(f20_in(z0), s(z0)), F20_IN(z0))
F45_IN(z0, s(z1)) → c13(U5'(f58_in(z0, z1), z0, s(z1)), F58_IN(z0, z1))
F76_IN(z0, s(z1)) → c16(U6'(f76_in(z0, z1), z0, s(z1)), F76_IN(z0, z1))
F41_IN(z0, z1) → c18(U7'(f45_in(z0, z1), z0, z1), F45_IN(z0, z1))
U7'(f45_out1(z0), z1, z2) → c19(U8'(f46_in(z0, z1), z1, z2, z0), F46_IN(z0, z1))
F46_IN(z0, z1) → c21(U9'(f65_in(z0, z1), z0, z1), F65_IN(z0, z1))
U9'(f65_out1(z0), z1, z2) → c22(U10'(f76_in(z0, z2), z1, z2, z0), F76_IN(z0, z2))
F58_IN(z0, z1) → c24(U11'(f45_in(z0, z1), z0, z1), F45_IN(z0, z1))
U11'(f45_out1(z0), z1, z2) → c25(U12'(f65_in(z0, z1), z1, z2, z0), F65_IN(z0, z1))
F18_IN(z0) → c27(U13'(f20_in(z0), f21_in(z0), z0), F20_IN(z0))

K tuples:none
Defined Rule Symbols:

f1_in, U1, U2, f65_in, U3, f20_in, U4, f45_in, U5, f76_in, U6, f41_in, U7, U8, f46_in, U9, U10, f58_in, U11, U12, f18_in, U13

Defined Pair Symbols:

F1_IN, F65_IN, F20_IN, F45_IN, F76_IN, F41_IN, U7', F46_IN, U9', F58_IN, U11', F18_IN

Compound Symbols:

c1, c2, c7, c10, c13, c16, c18, c19, c21, c22, c24, c25, c27

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

Split RHS of tuples not part of any SCC

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, 0) → f1_out1(0)
f1_in(z0, s(0)) → U1(f18_in(z0), z0, s(0))
f1_in(z0, s(s(z1))) → U2(f41_in(z0, z1), z0, s(s(z1)))
U1(f18_out1(z0), z1, s(0)) → f1_out1(z0)
U1(f18_out2(z0, z1), z2, s(0)) → f1_out1(z1)
U2(f41_out1(z0, z1, z2), z3, s(s(z4))) → f1_out1(z2)
f65_in(z0, 0) → f65_out1(z0)
f65_in(z0, s(z1)) → U3(f65_in(z0, z1), z0, s(z1))
U3(f65_out1(z0), z1, s(z2)) → f65_out1(s(z0))
f20_in(0) → f20_out1(0)
f20_in(s(z0)) → U4(f20_in(z0), s(z0))
U4(f20_out1(z0), s(z1)) → f20_out1(s(z0))
f45_in(z0, 0) → f45_out1(0)
f45_in(z0, s(z1)) → U5(f58_in(z0, z1), z0, s(z1))
U5(f58_out1(z0, z1), z2, s(z3)) → f45_out1(z1)
f76_in(z0, 0) → f76_out1(z0)
f76_in(z0, s(z1)) → U6(f76_in(z0, z1), z0, s(z1))
U6(f76_out1(z0), z1, s(z2)) → f76_out1(s(z0))
f41_in(z0, z1) → U7(f45_in(z0, z1), z0, z1)
U7(f45_out1(z0), z1, z2) → U8(f46_in(z0, z1), z1, z2, z0)
U8(f46_out1(z0, z1), z2, z3, z4) → f41_out1(z4, z0, z1)
f46_in(z0, z1) → U9(f65_in(z0, z1), z0, z1)
U9(f65_out1(z0), z1, z2) → U10(f76_in(z0, z2), z1, z2, z0)
U10(f76_out1(z0), z1, z2, z3) → f46_out1(z3, z0)
f58_in(z0, z1) → U11(f45_in(z0, z1), z0, z1)
U11(f45_out1(z0), z1, z2) → U12(f65_in(z0, z1), z1, z2, z0)
U12(f65_out1(z0), z1, z2, z3) → f58_out1(z3, z0)
f18_in(z0) → U13(f20_in(z0), f21_in(z0), z0)
U13(f20_out1(z0), z1, z2) → f18_out1(z0)
U13(z0, f21_out1(z1, z2), z3) → f18_out2(z1, z2)

Tuples:

F65_IN(z0, s(z1)) → c7(U3'(f65_in(z0, z1), z0, s(z1)), F65_IN(z0, z1))
F20_IN(s(z0)) → c10(U4'(f20_in(z0), s(z0)), F20_IN(z0))
F45_IN(z0, s(z1)) → c13(U5'(f58_in(z0, z1), z0, s(z1)), F58_IN(z0, z1))
F76_IN(z0, s(z1)) → c16(U6'(f76_in(z0, z1), z0, s(z1)), F76_IN(z0, z1))
F58_IN(z0, z1) → c24(U11'(f45_in(z0, z1), z0, z1), F45_IN(z0, z1))
F1_IN(z0, s(0)) → c(U1'(f18_in(z0), z0, s(0)))
F1_IN(z0, s(0)) → c(F18_IN(z0))
F1_IN(z0, s(s(z1))) → c(U2'(f41_in(z0, z1), z0, s(s(z1))))
F1_IN(z0, s(s(z1))) → c(F41_IN(z0, z1))
F41_IN(z0, z1) → c(U7'(f45_in(z0, z1), z0, z1))
F41_IN(z0, z1) → c(F45_IN(z0, z1))
U7'(f45_out1(z0), z1, z2) → c(U8'(f46_in(z0, z1), z1, z2, z0))
U7'(f45_out1(z0), z1, z2) → c(F46_IN(z0, z1))
F46_IN(z0, z1) → c(U9'(f65_in(z0, z1), z0, z1))
F46_IN(z0, z1) → c(F65_IN(z0, z1))
U9'(f65_out1(z0), z1, z2) → c(U10'(f76_in(z0, z2), z1, z2, z0))
U9'(f65_out1(z0), z1, z2) → c(F76_IN(z0, z2))
U11'(f45_out1(z0), z1, z2) → c(U12'(f65_in(z0, z1), z1, z2, z0))
U11'(f45_out1(z0), z1, z2) → c(F65_IN(z0, z1))
F18_IN(z0) → c(U13'(f20_in(z0), f21_in(z0), z0))
F18_IN(z0) → c(F20_IN(z0))

S tuples:

F65_IN(z0, s(z1)) → c7(U3'(f65_in(z0, z1), z0, s(z1)), F65_IN(z0, z1))
F20_IN(s(z0)) → c10(U4'(f20_in(z0), s(z0)), F20_IN(z0))
F45_IN(z0, s(z1)) → c13(U5'(f58_in(z0, z1), z0, s(z1)), F58_IN(z0, z1))
F76_IN(z0, s(z1)) → c16(U6'(f76_in(z0, z1), z0, s(z1)), F76_IN(z0, z1))
F58_IN(z0, z1) → c24(U11'(f45_in(z0, z1), z0, z1), F45_IN(z0, z1))
F1_IN(z0, s(0)) → c(U1'(f18_in(z0), z0, s(0)))
F1_IN(z0, s(0)) → c(F18_IN(z0))
F1_IN(z0, s(s(z1))) → c(U2'(f41_in(z0, z1), z0, s(s(z1))))
F1_IN(z0, s(s(z1))) → c(F41_IN(z0, z1))
F41_IN(z0, z1) → c(U7'(f45_in(z0, z1), z0, z1))
F41_IN(z0, z1) → c(F45_IN(z0, z1))
U7'(f45_out1(z0), z1, z2) → c(U8'(f46_in(z0, z1), z1, z2, z0))
U7'(f45_out1(z0), z1, z2) → c(F46_IN(z0, z1))
F46_IN(z0, z1) → c(U9'(f65_in(z0, z1), z0, z1))
F46_IN(z0, z1) → c(F65_IN(z0, z1))
U9'(f65_out1(z0), z1, z2) → c(U10'(f76_in(z0, z2), z1, z2, z0))
U9'(f65_out1(z0), z1, z2) → c(F76_IN(z0, z2))
U11'(f45_out1(z0), z1, z2) → c(U12'(f65_in(z0, z1), z1, z2, z0))
U11'(f45_out1(z0), z1, z2) → c(F65_IN(z0, z1))
F18_IN(z0) → c(U13'(f20_in(z0), f21_in(z0), z0))
F18_IN(z0) → c(F20_IN(z0))

K tuples:none
Defined Rule Symbols:

f1_in, U1, U2, f65_in, U3, f20_in, U4, f45_in, U5, f76_in, U6, f41_in, U7, U8, f46_in, U9, U10, f58_in, U11, U12, f18_in, U13

Defined Pair Symbols:

F65_IN, F20_IN, F45_IN, F76_IN, F58_IN, F1_IN, F41_IN, U7', F46_IN, U9', U11', F18_IN

Compound Symbols:

c7, c10, c13, c16, c24, c

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

Removed 10 trailing tuple parts

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, 0) → f1_out1(0)
f1_in(z0, s(0)) → U1(f18_in(z0), z0, s(0))
f1_in(z0, s(s(z1))) → U2(f41_in(z0, z1), z0, s(s(z1)))
U1(f18_out1(z0), z1, s(0)) → f1_out1(z0)
U1(f18_out2(z0, z1), z2, s(0)) → f1_out1(z1)
U2(f41_out1(z0, z1, z2), z3, s(s(z4))) → f1_out1(z2)
f65_in(z0, 0) → f65_out1(z0)
f65_in(z0, s(z1)) → U3(f65_in(z0, z1), z0, s(z1))
U3(f65_out1(z0), z1, s(z2)) → f65_out1(s(z0))
f20_in(0) → f20_out1(0)
f20_in(s(z0)) → U4(f20_in(z0), s(z0))
U4(f20_out1(z0), s(z1)) → f20_out1(s(z0))
f45_in(z0, 0) → f45_out1(0)
f45_in(z0, s(z1)) → U5(f58_in(z0, z1), z0, s(z1))
U5(f58_out1(z0, z1), z2, s(z3)) → f45_out1(z1)
f76_in(z0, 0) → f76_out1(z0)
f76_in(z0, s(z1)) → U6(f76_in(z0, z1), z0, s(z1))
U6(f76_out1(z0), z1, s(z2)) → f76_out1(s(z0))
f41_in(z0, z1) → U7(f45_in(z0, z1), z0, z1)
U7(f45_out1(z0), z1, z2) → U8(f46_in(z0, z1), z1, z2, z0)
U8(f46_out1(z0, z1), z2, z3, z4) → f41_out1(z4, z0, z1)
f46_in(z0, z1) → U9(f65_in(z0, z1), z0, z1)
U9(f65_out1(z0), z1, z2) → U10(f76_in(z0, z2), z1, z2, z0)
U10(f76_out1(z0), z1, z2, z3) → f46_out1(z3, z0)
f58_in(z0, z1) → U11(f45_in(z0, z1), z0, z1)
U11(f45_out1(z0), z1, z2) → U12(f65_in(z0, z1), z1, z2, z0)
U12(f65_out1(z0), z1, z2, z3) → f58_out1(z3, z0)
f18_in(z0) → U13(f20_in(z0), f21_in(z0), z0)
U13(f20_out1(z0), z1, z2) → f18_out1(z0)
U13(z0, f21_out1(z1, z2), z3) → f18_out2(z1, z2)

Tuples:

F58_IN(z0, z1) → c24(U11'(f45_in(z0, z1), z0, z1), F45_IN(z0, z1))
F1_IN(z0, s(0)) → c(F18_IN(z0))
F1_IN(z0, s(s(z1))) → c(F41_IN(z0, z1))
F41_IN(z0, z1) → c(U7'(f45_in(z0, z1), z0, z1))
F41_IN(z0, z1) → c(F45_IN(z0, z1))
U7'(f45_out1(z0), z1, z2) → c(F46_IN(z0, z1))
F46_IN(z0, z1) → c(U9'(f65_in(z0, z1), z0, z1))
F46_IN(z0, z1) → c(F65_IN(z0, z1))
U9'(f65_out1(z0), z1, z2) → c(F76_IN(z0, z2))
U11'(f45_out1(z0), z1, z2) → c(F65_IN(z0, z1))
F18_IN(z0) → c(F20_IN(z0))
F65_IN(z0, s(z1)) → c7(F65_IN(z0, z1))
F20_IN(s(z0)) → c10(F20_IN(z0))
F45_IN(z0, s(z1)) → c13(F58_IN(z0, z1))
F76_IN(z0, s(z1)) → c16(F76_IN(z0, z1))
F1_IN(z0, s(0)) → c
F1_IN(z0, s(s(z1))) → c
U7'(f45_out1(z0), z1, z2) → c
U9'(f65_out1(z0), z1, z2) → c
U11'(f45_out1(z0), z1, z2) → c
F18_IN(z0) → c

S tuples:

F58_IN(z0, z1) → c24(U11'(f45_in(z0, z1), z0, z1), F45_IN(z0, z1))
F1_IN(z0, s(0)) → c(F18_IN(z0))
F1_IN(z0, s(s(z1))) → c(F41_IN(z0, z1))
F41_IN(z0, z1) → c(U7'(f45_in(z0, z1), z0, z1))
F41_IN(z0, z1) → c(F45_IN(z0, z1))
U7'(f45_out1(z0), z1, z2) → c(F46_IN(z0, z1))
F46_IN(z0, z1) → c(U9'(f65_in(z0, z1), z0, z1))
F46_IN(z0, z1) → c(F65_IN(z0, z1))
U9'(f65_out1(z0), z1, z2) → c(F76_IN(z0, z2))
U11'(f45_out1(z0), z1, z2) → c(F65_IN(z0, z1))
F18_IN(z0) → c(F20_IN(z0))
F65_IN(z0, s(z1)) → c7(F65_IN(z0, z1))
F20_IN(s(z0)) → c10(F20_IN(z0))
F45_IN(z0, s(z1)) → c13(F58_IN(z0, z1))
F76_IN(z0, s(z1)) → c16(F76_IN(z0, z1))
F1_IN(z0, s(0)) → c
F1_IN(z0, s(s(z1))) → c
U7'(f45_out1(z0), z1, z2) → c
U9'(f65_out1(z0), z1, z2) → c
U11'(f45_out1(z0), z1, z2) → c
F18_IN(z0) → c

K tuples:none
Defined Rule Symbols:

f1_in, U1, U2, f65_in, U3, f20_in, U4, f45_in, U5, f76_in, U6, f41_in, U7, U8, f46_in, U9, U10, f58_in, U11, U12, f18_in, U13

Defined Pair Symbols:

F58_IN, F1_IN, F41_IN, U7', F46_IN, U9', U11', F18_IN, F65_IN, F20_IN, F45_IN, F76_IN

Compound Symbols:

c24, c, c7, c10, c13, c16, c

(27) CdtKnowledgeProof (EQUIVALENT transformation)

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

F1_IN(z0, s(0)) → c(F18_IN(z0))
F1_IN(z0, s(s(z1))) → c(F41_IN(z0, z1))
F41_IN(z0, z1) → c(U7'(f45_in(z0, z1), z0, z1))
F41_IN(z0, z1) → c(F45_IN(z0, z1))
U7'(f45_out1(z0), z1, z2) → c(F46_IN(z0, z1))
F46_IN(z0, z1) → c(U9'(f65_in(z0, z1), z0, z1))
F46_IN(z0, z1) → c(F65_IN(z0, z1))
U9'(f65_out1(z0), z1, z2) → c(F76_IN(z0, z2))
F18_IN(z0) → c(F20_IN(z0))
F1_IN(z0, s(0)) → c
F1_IN(z0, s(s(z1))) → c
U7'(f45_out1(z0), z1, z2) → c
U9'(f65_out1(z0), z1, z2) → c
F18_IN(z0) → c
F18_IN(z0) → c(F20_IN(z0))
F18_IN(z0) → c
F41_IN(z0, z1) → c(U7'(f45_in(z0, z1), z0, z1))
F41_IN(z0, z1) → c(F45_IN(z0, z1))
U7'(f45_out1(z0), z1, z2) → c(F46_IN(z0, z1))
U7'(f45_out1(z0), z1, z2) → c
F46_IN(z0, z1) → c(U9'(f65_in(z0, z1), z0, z1))
F46_IN(z0, z1) → c(F65_IN(z0, z1))
U9'(f65_out1(z0), z1, z2) → c(F76_IN(z0, z2))
U9'(f65_out1(z0), z1, z2) → c

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, 0) → f1_out1(0)
f1_in(z0, s(0)) → U1(f18_in(z0), z0, s(0))
f1_in(z0, s(s(z1))) → U2(f41_in(z0, z1), z0, s(s(z1)))
U1(f18_out1(z0), z1, s(0)) → f1_out1(z0)
U1(f18_out2(z0, z1), z2, s(0)) → f1_out1(z1)
U2(f41_out1(z0, z1, z2), z3, s(s(z4))) → f1_out1(z2)
f65_in(z0, 0) → f65_out1(z0)
f65_in(z0, s(z1)) → U3(f65_in(z0, z1), z0, s(z1))
U3(f65_out1(z0), z1, s(z2)) → f65_out1(s(z0))
f20_in(0) → f20_out1(0)
f20_in(s(z0)) → U4(f20_in(z0), s(z0))
U4(f20_out1(z0), s(z1)) → f20_out1(s(z0))
f45_in(z0, 0) → f45_out1(0)
f45_in(z0, s(z1)) → U5(f58_in(z0, z1), z0, s(z1))
U5(f58_out1(z0, z1), z2, s(z3)) → f45_out1(z1)
f76_in(z0, 0) → f76_out1(z0)
f76_in(z0, s(z1)) → U6(f76_in(z0, z1), z0, s(z1))
U6(f76_out1(z0), z1, s(z2)) → f76_out1(s(z0))
f41_in(z0, z1) → U7(f45_in(z0, z1), z0, z1)
U7(f45_out1(z0), z1, z2) → U8(f46_in(z0, z1), z1, z2, z0)
U8(f46_out1(z0, z1), z2, z3, z4) → f41_out1(z4, z0, z1)
f46_in(z0, z1) → U9(f65_in(z0, z1), z0, z1)
U9(f65_out1(z0), z1, z2) → U10(f76_in(z0, z2), z1, z2, z0)
U10(f76_out1(z0), z1, z2, z3) → f46_out1(z3, z0)
f58_in(z0, z1) → U11(f45_in(z0, z1), z0, z1)
U11(f45_out1(z0), z1, z2) → U12(f65_in(z0, z1), z1, z2, z0)
U12(f65_out1(z0), z1, z2, z3) → f58_out1(z3, z0)
f18_in(z0) → U13(f20_in(z0), f21_in(z0), z0)
U13(f20_out1(z0), z1, z2) → f18_out1(z0)
U13(z0, f21_out1(z1, z2), z3) → f18_out2(z1, z2)

Tuples:

F58_IN(z0, z1) → c24(U11'(f45_in(z0, z1), z0, z1), F45_IN(z0, z1))
F1_IN(z0, s(0)) → c(F18_IN(z0))
F1_IN(z0, s(s(z1))) → c(F41_IN(z0, z1))
F41_IN(z0, z1) → c(U7'(f45_in(z0, z1), z0, z1))
F41_IN(z0, z1) → c(F45_IN(z0, z1))
U7'(f45_out1(z0), z1, z2) → c(F46_IN(z0, z1))
F46_IN(z0, z1) → c(U9'(f65_in(z0, z1), z0, z1))
F46_IN(z0, z1) → c(F65_IN(z0, z1))
U9'(f65_out1(z0), z1, z2) → c(F76_IN(z0, z2))
U11'(f45_out1(z0), z1, z2) → c(F65_IN(z0, z1))
F18_IN(z0) → c(F20_IN(z0))
F65_IN(z0, s(z1)) → c7(F65_IN(z0, z1))
F20_IN(s(z0)) → c10(F20_IN(z0))
F45_IN(z0, s(z1)) → c13(F58_IN(z0, z1))
F76_IN(z0, s(z1)) → c16(F76_IN(z0, z1))
F1_IN(z0, s(0)) → c
F1_IN(z0, s(s(z1))) → c
U7'(f45_out1(z0), z1, z2) → c
U9'(f65_out1(z0), z1, z2) → c
U11'(f45_out1(z0), z1, z2) → c
F18_IN(z0) → c

S tuples:

F58_IN(z0, z1) → c24(U11'(f45_in(z0, z1), z0, z1), F45_IN(z0, z1))
U11'(f45_out1(z0), z1, z2) → c(F65_IN(z0, z1))
F65_IN(z0, s(z1)) → c7(F65_IN(z0, z1))
F20_IN(s(z0)) → c10(F20_IN(z0))
F45_IN(z0, s(z1)) → c13(F58_IN(z0, z1))
F76_IN(z0, s(z1)) → c16(F76_IN(z0, z1))
U11'(f45_out1(z0), z1, z2) → c

K tuples:

F1_IN(z0, s(0)) → c(F18_IN(z0))
F1_IN(z0, s(s(z1))) → c(F41_IN(z0, z1))
F41_IN(z0, z1) → c(U7'(f45_in(z0, z1), z0, z1))
F41_IN(z0, z1) → c(F45_IN(z0, z1))
U7'(f45_out1(z0), z1, z2) → c(F46_IN(z0, z1))
F46_IN(z0, z1) → c(U9'(f65_in(z0, z1), z0, z1))
F46_IN(z0, z1) → c(F65_IN(z0, z1))
U9'(f65_out1(z0), z1, z2) → c(F76_IN(z0, z2))
F18_IN(z0) → c(F20_IN(z0))
F1_IN(z0, s(0)) → c
F1_IN(z0, s(s(z1))) → c
U7'(f45_out1(z0), z1, z2) → c
U9'(f65_out1(z0), z1, z2) → c
F18_IN(z0) → c

Defined Rule Symbols:

f1_in, U1, U2, f65_in, U3, f20_in, U4, f45_in, U5, f76_in, U6, f41_in, U7, U8, f46_in, U9, U10, f58_in, U11, U12, f18_in, U13

Defined Pair Symbols:

F58_IN, F1_IN, F41_IN, U7', F46_IN, U9', U11', F18_IN, F65_IN, F20_IN, F45_IN, F76_IN

Compound Symbols:

c24, c, c7, c10, c13, c16, c

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

F58_IN(z0, z1) → c24(U11'(f45_in(z0, z1), z0, z1), F45_IN(z0, z1))
F20_IN(s(z0)) → c10(F20_IN(z0))
F45_IN(z0, s(z1)) → c13(F58_IN(z0, z1))

We considered the (Usable) Rules:

f65_in(z0, 0) → f65_out1(z0)
f65_in(z0, s(z1)) → U3(f65_in(z0, z1), z0, s(z1))
U3(f65_out1(z0), z1, s(z2)) → f65_out1(s(z0))
f45_in(z0, 0) → f45_out1(0)
f45_in(z0, s(z1)) → U5(f58_in(z0, z1), z0, s(z1))
f58_in(z0, z1) → U11(f45_in(z0, z1), z0, z1)
U5(f58_out1(z0, z1), z2, s(z3)) → f45_out1(z1)
U11(f45_out1(z0), z1, z2) → U12(f65_in(z0, z1), z1, z2, z0)
U12(f65_out1(z0), z1, z2, z3) → f58_out1(z3, z0)

And the Tuples:

F58_IN(z0, z1) → c24(U11'(f45_in(z0, z1), z0, z1), F45_IN(z0, z1))
F1_IN(z0, s(0)) → c(F18_IN(z0))
F1_IN(z0, s(s(z1))) → c(F41_IN(z0, z1))
F41_IN(z0, z1) → c(U7'(f45_in(z0, z1), z0, z1))
F41_IN(z0, z1) → c(F45_IN(z0, z1))
U7'(f45_out1(z0), z1, z2) → c(F46_IN(z0, z1))
F46_IN(z0, z1) → c(U9'(f65_in(z0, z1), z0, z1))
F46_IN(z0, z1) → c(F65_IN(z0, z1))
U9'(f65_out1(z0), z1, z2) → c(F76_IN(z0, z2))
U11'(f45_out1(z0), z1, z2) → c(F65_IN(z0, z1))
F18_IN(z0) → c(F20_IN(z0))
F65_IN(z0, s(z1)) → c7(F65_IN(z0, z1))
F20_IN(s(z0)) → c10(F20_IN(z0))
F45_IN(z0, s(z1)) → c13(F58_IN(z0, z1))
F76_IN(z0, s(z1)) → c16(F76_IN(z0, z1))
F1_IN(z0, s(0)) → c
F1_IN(z0, s(s(z1))) → c
U7'(f45_out1(z0), z1, z2) → c
U9'(f65_out1(z0), z1, z2) → c
U11'(f45_out1(z0), z1, z2) → c
F18_IN(z0) → c

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

POL(0) = 0   
POL(F18_IN(x₁)) = [2] + [3]x₁   
POL(F1_IN(x₁, x₂)) = [1] + [3]x₁ + [2]x₂   
POL(F20_IN(x₁)) = [2] + [2]x₁   
POL(F41_IN(x₁, x₂)) = x₁ + [2]x₂   
POL(F45_IN(x₁, x₂)) = x₂   
POL(F46_IN(x₁, x₂)) = x₂   
POL(F58_IN(x₁, x₂)) = [1] + x₂   
POL(F65_IN(x₁, x₂)) = 0   
POL(F76_IN(x₁, x₂)) = 0   
POL(U11(x₁, x₂, x₃)) = 0   
POL(U11'(x₁, x₂, x₃)) = 0   
POL(U12(x₁, x₂, x₃, x₄)) = 0   
POL(U3(x₁, x₂, x₃)) = 0   
POL(U5(x₁, x₂, x₃)) = 0   
POL(U7'(x₁, x₂, x₃)) = x₂ + [2]x₃   
POL(U9'(x₁, x₂, x₃)) = 0   
POL(c) = 0   
POL(c(x₁)) = x₁   
POL(c10(x₁)) = x₁   
POL(c13(x₁)) = x₁   
POL(c16(x₁)) = x₁   
POL(c24(x₁, x₂)) = x₁ + x₂   
POL(c7(x₁)) = x₁   
POL(f45_in(x₁, x₂)) = 0   
POL(f45_out1(x₁)) = 0   
POL(f58_in(x₁, x₂)) = 0   
POL(f58_out1(x₁, x₂)) = 0   
POL(f65_in(x₁, x₂)) = 0   
POL(f65_out1(x₁)) = 0   
POL(s(x₁)) = [2] + x₁   

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, 0) → f1_out1(0)
f1_in(z0, s(0)) → U1(f18_in(z0), z0, s(0))
f1_in(z0, s(s(z1))) → U2(f41_in(z0, z1), z0, s(s(z1)))
U1(f18_out1(z0), z1, s(0)) → f1_out1(z0)
U1(f18_out2(z0, z1), z2, s(0)) → f1_out1(z1)
U2(f41_out1(z0, z1, z2), z3, s(s(z4))) → f1_out1(z2)
f65_in(z0, 0) → f65_out1(z0)
f65_in(z0, s(z1)) → U3(f65_in(z0, z1), z0, s(z1))
U3(f65_out1(z0), z1, s(z2)) → f65_out1(s(z0))
f20_in(0) → f20_out1(0)
f20_in(s(z0)) → U4(f20_in(z0), s(z0))
U4(f20_out1(z0), s(z1)) → f20_out1(s(z0))
f45_in(z0, 0) → f45_out1(0)
f45_in(z0, s(z1)) → U5(f58_in(z0, z1), z0, s(z1))
U5(f58_out1(z0, z1), z2, s(z3)) → f45_out1(z1)
f76_in(z0, 0) → f76_out1(z0)
f76_in(z0, s(z1)) → U6(f76_in(z0, z1), z0, s(z1))
U6(f76_out1(z0), z1, s(z2)) → f76_out1(s(z0))
f41_in(z0, z1) → U7(f45_in(z0, z1), z0, z1)
U7(f45_out1(z0), z1, z2) → U8(f46_in(z0, z1), z1, z2, z0)
U8(f46_out1(z0, z1), z2, z3, z4) → f41_out1(z4, z0, z1)
f46_in(z0, z1) → U9(f65_in(z0, z1), z0, z1)
U9(f65_out1(z0), z1, z2) → U10(f76_in(z0, z2), z1, z2, z0)
U10(f76_out1(z0), z1, z2, z3) → f46_out1(z3, z0)
f58_in(z0, z1) → U11(f45_in(z0, z1), z0, z1)
U11(f45_out1(z0), z1, z2) → U12(f65_in(z0, z1), z1, z2, z0)
U12(f65_out1(z0), z1, z2, z3) → f58_out1(z3, z0)
f18_in(z0) → U13(f20_in(z0), f21_in(z0), z0)
U13(f20_out1(z0), z1, z2) → f18_out1(z0)
U13(z0, f21_out1(z1, z2), z3) → f18_out2(z1, z2)

Tuples:

F58_IN(z0, z1) → c24(U11'(f45_in(z0, z1), z0, z1), F45_IN(z0, z1))
F1_IN(z0, s(0)) → c(F18_IN(z0))
F1_IN(z0, s(s(z1))) → c(F41_IN(z0, z1))
F41_IN(z0, z1) → c(U7'(f45_in(z0, z1), z0, z1))
F41_IN(z0, z1) → c(F45_IN(z0, z1))
U7'(f45_out1(z0), z1, z2) → c(F46_IN(z0, z1))
F46_IN(z0, z1) → c(U9'(f65_in(z0, z1), z0, z1))
F46_IN(z0, z1) → c(F65_IN(z0, z1))
U9'(f65_out1(z0), z1, z2) → c(F76_IN(z0, z2))
U11'(f45_out1(z0), z1, z2) → c(F65_IN(z0, z1))
F18_IN(z0) → c(F20_IN(z0))
F65_IN(z0, s(z1)) → c7(F65_IN(z0, z1))
F20_IN(s(z0)) → c10(F20_IN(z0))
F45_IN(z0, s(z1)) → c13(F58_IN(z0, z1))
F76_IN(z0, s(z1)) → c16(F76_IN(z0, z1))
F1_IN(z0, s(0)) → c
F1_IN(z0, s(s(z1))) → c
U7'(f45_out1(z0), z1, z2) → c
U9'(f65_out1(z0), z1, z2) → c
U11'(f45_out1(z0), z1, z2) → c
F18_IN(z0) → c

S tuples:

U11'(f45_out1(z0), z1, z2) → c(F65_IN(z0, z1))
F65_IN(z0, s(z1)) → c7(F65_IN(z0, z1))
F76_IN(z0, s(z1)) → c16(F76_IN(z0, z1))
U11'(f45_out1(z0), z1, z2) → c

K tuples:

F1_IN(z0, s(0)) → c(F18_IN(z0))
F1_IN(z0, s(s(z1))) → c(F41_IN(z0, z1))
F41_IN(z0, z1) → c(U7'(f45_in(z0, z1), z0, z1))
F41_IN(z0, z1) → c(F45_IN(z0, z1))
U7'(f45_out1(z0), z1, z2) → c(F46_IN(z0, z1))
F46_IN(z0, z1) → c(U9'(f65_in(z0, z1), z0, z1))
F46_IN(z0, z1) → c(F65_IN(z0, z1))
U9'(f65_out1(z0), z1, z2) → c(F76_IN(z0, z2))
F18_IN(z0) → c(F20_IN(z0))
F1_IN(z0, s(0)) → c
F1_IN(z0, s(s(z1))) → c
U7'(f45_out1(z0), z1, z2) → c
U9'(f65_out1(z0), z1, z2) → c
F18_IN(z0) → c
F58_IN(z0, z1) → c24(U11'(f45_in(z0, z1), z0, z1), F45_IN(z0, z1))
F20_IN(s(z0)) → c10(F20_IN(z0))
F45_IN(z0, s(z1)) → c13(F58_IN(z0, z1))

Defined Rule Symbols:

f1_in, U1, U2, f65_in, U3, f20_in, U4, f45_in, U5, f76_in, U6, f41_in, U7, U8, f46_in, U9, U10, f58_in, U11, U12, f18_in, U13

Defined Pair Symbols:

F58_IN, F1_IN, F41_IN, U7', F46_IN, U9', U11', F18_IN, F65_IN, F20_IN, F45_IN, F76_IN

Compound Symbols:

c24, c, c7, c10, c13, c16, c

(31) CdtKnowledgeProof (EQUIVALENT transformation)

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

U11'(f45_out1(z0), z1, z2) → c(F65_IN(z0, z1))
U11'(f45_out1(z0), z1, z2) → c

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, 0) → f1_out1(0)
f1_in(z0, s(0)) → U1(f18_in(z0), z0, s(0))
f1_in(z0, s(s(z1))) → U2(f41_in(z0, z1), z0, s(s(z1)))
U1(f18_out1(z0), z1, s(0)) → f1_out1(z0)
U1(f18_out2(z0, z1), z2, s(0)) → f1_out1(z1)
U2(f41_out1(z0, z1, z2), z3, s(s(z4))) → f1_out1(z2)
f65_in(z0, 0) → f65_out1(z0)
f65_in(z0, s(z1)) → U3(f65_in(z0, z1), z0, s(z1))
U3(f65_out1(z0), z1, s(z2)) → f65_out1(s(z0))
f20_in(0) → f20_out1(0)
f20_in(s(z0)) → U4(f20_in(z0), s(z0))
U4(f20_out1(z0), s(z1)) → f20_out1(s(z0))
f45_in(z0, 0) → f45_out1(0)
f45_in(z0, s(z1)) → U5(f58_in(z0, z1), z0, s(z1))
U5(f58_out1(z0, z1), z2, s(z3)) → f45_out1(z1)
f76_in(z0, 0) → f76_out1(z0)
f76_in(z0, s(z1)) → U6(f76_in(z0, z1), z0, s(z1))
U6(f76_out1(z0), z1, s(z2)) → f76_out1(s(z0))
f41_in(z0, z1) → U7(f45_in(z0, z1), z0, z1)
U7(f45_out1(z0), z1, z2) → U8(f46_in(z0, z1), z1, z2, z0)
U8(f46_out1(z0, z1), z2, z3, z4) → f41_out1(z4, z0, z1)
f46_in(z0, z1) → U9(f65_in(z0, z1), z0, z1)
U9(f65_out1(z0), z1, z2) → U10(f76_in(z0, z2), z1, z2, z0)
U10(f76_out1(z0), z1, z2, z3) → f46_out1(z3, z0)
f58_in(z0, z1) → U11(f45_in(z0, z1), z0, z1)
U11(f45_out1(z0), z1, z2) → U12(f65_in(z0, z1), z1, z2, z0)
U12(f65_out1(z0), z1, z2, z3) → f58_out1(z3, z0)
f18_in(z0) → U13(f20_in(z0), f21_in(z0), z0)
U13(f20_out1(z0), z1, z2) → f18_out1(z0)
U13(z0, f21_out1(z1, z2), z3) → f18_out2(z1, z2)

Tuples:

F58_IN(z0, z1) → c24(U11'(f45_in(z0, z1), z0, z1), F45_IN(z0, z1))
F1_IN(z0, s(0)) → c(F18_IN(z0))
F1_IN(z0, s(s(z1))) → c(F41_IN(z0, z1))
F41_IN(z0, z1) → c(U7'(f45_in(z0, z1), z0, z1))
F41_IN(z0, z1) → c(F45_IN(z0, z1))
U7'(f45_out1(z0), z1, z2) → c(F46_IN(z0, z1))
F46_IN(z0, z1) → c(U9'(f65_in(z0, z1), z0, z1))
F46_IN(z0, z1) → c(F65_IN(z0, z1))
U9'(f65_out1(z0), z1, z2) → c(F76_IN(z0, z2))
U11'(f45_out1(z0), z1, z2) → c(F65_IN(z0, z1))
F18_IN(z0) → c(F20_IN(z0))
F65_IN(z0, s(z1)) → c7(F65_IN(z0, z1))
F20_IN(s(z0)) → c10(F20_IN(z0))
F45_IN(z0, s(z1)) → c13(F58_IN(z0, z1))
F76_IN(z0, s(z1)) → c16(F76_IN(z0, z1))
F1_IN(z0, s(0)) → c
F1_IN(z0, s(s(z1))) → c
U7'(f45_out1(z0), z1, z2) → c
U9'(f65_out1(z0), z1, z2) → c
U11'(f45_out1(z0), z1, z2) → c
F18_IN(z0) → c

S tuples:

F65_IN(z0, s(z1)) → c7(F65_IN(z0, z1))
F76_IN(z0, s(z1)) → c16(F76_IN(z0, z1))

K tuples:

F1_IN(z0, s(0)) → c(F18_IN(z0))
F1_IN(z0, s(s(z1))) → c(F41_IN(z0, z1))
F41_IN(z0, z1) → c(U7'(f45_in(z0, z1), z0, z1))
F41_IN(z0, z1) → c(F45_IN(z0, z1))
U7'(f45_out1(z0), z1, z2) → c(F46_IN(z0, z1))
F46_IN(z0, z1) → c(U9'(f65_in(z0, z1), z0, z1))
F46_IN(z0, z1) → c(F65_IN(z0, z1))
U9'(f65_out1(z0), z1, z2) → c(F76_IN(z0, z2))
F18_IN(z0) → c(F20_IN(z0))
F1_IN(z0, s(0)) → c
F1_IN(z0, s(s(z1))) → c
U7'(f45_out1(z0), z1, z2) → c
U9'(f65_out1(z0), z1, z2) → c
F18_IN(z0) → c
F58_IN(z0, z1) → c24(U11'(f45_in(z0, z1), z0, z1), F45_IN(z0, z1))
F20_IN(s(z0)) → c10(F20_IN(z0))
F45_IN(z0, s(z1)) → c13(F58_IN(z0, z1))
U11'(f45_out1(z0), z1, z2) → c(F65_IN(z0, z1))
U11'(f45_out1(z0), z1, z2) → c

Defined Rule Symbols:

f1_in, U1, U2, f65_in, U3, f20_in, U4, f45_in, U5, f76_in, U6, f41_in, U7, U8, f46_in, U9, U10, f58_in, U11, U12, f18_in, U13

Defined Pair Symbols:

F58_IN, F1_IN, F41_IN, U7', F46_IN, U9', U11', F18_IN, F65_IN, F20_IN, F45_IN, F76_IN

Compound Symbols:

c24, c, c7, c10, c13, c16, c

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

F76_IN(z0, s(z1)) → c16(F76_IN(z0, z1))

We considered the (Usable) Rules:

f65_in(z0, 0) → f65_out1(z0)
f65_in(z0, s(z1)) → U3(f65_in(z0, z1), z0, s(z1))
U3(f65_out1(z0), z1, s(z2)) → f65_out1(s(z0))
f45_in(z0, 0) → f45_out1(0)
f45_in(z0, s(z1)) → U5(f58_in(z0, z1), z0, s(z1))
f58_in(z0, z1) → U11(f45_in(z0, z1), z0, z1)
U5(f58_out1(z0, z1), z2, s(z3)) → f45_out1(z1)
U11(f45_out1(z0), z1, z2) → U12(f65_in(z0, z1), z1, z2, z0)
U12(f65_out1(z0), z1, z2, z3) → f58_out1(z3, z0)

And the Tuples:

F58_IN(z0, z1) → c24(U11'(f45_in(z0, z1), z0, z1), F45_IN(z0, z1))
F1_IN(z0, s(0)) → c(F18_IN(z0))
F1_IN(z0, s(s(z1))) → c(F41_IN(z0, z1))
F41_IN(z0, z1) → c(U7'(f45_in(z0, z1), z0, z1))
F41_IN(z0, z1) → c(F45_IN(z0, z1))
U7'(f45_out1(z0), z1, z2) → c(F46_IN(z0, z1))
F46_IN(z0, z1) → c(U9'(f65_in(z0, z1), z0, z1))
F46_IN(z0, z1) → c(F65_IN(z0, z1))
U9'(f65_out1(z0), z1, z2) → c(F76_IN(z0, z2))
U11'(f45_out1(z0), z1, z2) → c(F65_IN(z0, z1))
F18_IN(z0) → c(F20_IN(z0))
F65_IN(z0, s(z1)) → c7(F65_IN(z0, z1))
F20_IN(s(z0)) → c10(F20_IN(z0))
F45_IN(z0, s(z1)) → c13(F58_IN(z0, z1))
F76_IN(z0, s(z1)) → c16(F76_IN(z0, z1))
F1_IN(z0, s(0)) → c
F1_IN(z0, s(s(z1))) → c
U7'(f45_out1(z0), z1, z2) → c
U9'(f65_out1(z0), z1, z2) → c
U11'(f45_out1(z0), z1, z2) → c
F18_IN(z0) → c

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

POL(0) = 0   
POL(F18_IN(x₁)) = 0   
POL(F1_IN(x₁, x₂)) = [2]x₁   
POL(F20_IN(x₁)) = 0   
POL(F41_IN(x₁, x₂)) = [2]x₁   
POL(F45_IN(x₁, x₂)) = 0   
POL(F46_IN(x₁, x₂)) = [2]x₂   
POL(F58_IN(x₁, x₂)) = 0   
POL(F65_IN(x₁, x₂)) = 0   
POL(F76_IN(x₁, x₂)) = x₂   
POL(U11(x₁, x₂, x₃)) = [1] + [2]x₁   
POL(U11'(x₁, x₂, x₃)) = 0   
POL(U12(x₁, x₂, x₃, x₄)) = x₁ + x₄   
POL(U3(x₁, x₂, x₃)) = 0   
POL(U5(x₁, x₂, x₃)) = 0   
POL(U7'(x₁, x₂, x₃)) = [2]x₂   
POL(U9'(x₁, x₂, x₃)) = x₃   
POL(c) = 0   
POL(c(x₁)) = x₁   
POL(c10(x₁)) = x₁   
POL(c13(x₁)) = x₁   
POL(c16(x₁)) = x₁   
POL(c24(x₁, x₂)) = x₁ + x₂   
POL(c7(x₁)) = x₁   
POL(f45_in(x₁, x₂)) = 0   
POL(f45_out1(x₁)) = x₁   
POL(f58_in(x₁, x₂)) = [1] + x₁   
POL(f58_out1(x₁, x₂)) = 0   
POL(f65_in(x₁, x₂)) = 0   
POL(f65_out1(x₁)) = x₁   
POL(s(x₁)) = [1] + x₁   

(34) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, 0) → f1_out1(0)
f1_in(z0, s(0)) → U1(f18_in(z0), z0, s(0))
f1_in(z0, s(s(z1))) → U2(f41_in(z0, z1), z0, s(s(z1)))
U1(f18_out1(z0), z1, s(0)) → f1_out1(z0)
U1(f18_out2(z0, z1), z2, s(0)) → f1_out1(z1)
U2(f41_out1(z0, z1, z2), z3, s(s(z4))) → f1_out1(z2)
f65_in(z0, 0) → f65_out1(z0)
f65_in(z0, s(z1)) → U3(f65_in(z0, z1), z0, s(z1))
U3(f65_out1(z0), z1, s(z2)) → f65_out1(s(z0))
f20_in(0) → f20_out1(0)
f20_in(s(z0)) → U4(f20_in(z0), s(z0))
U4(f20_out1(z0), s(z1)) → f20_out1(s(z0))
f45_in(z0, 0) → f45_out1(0)
f45_in(z0, s(z1)) → U5(f58_in(z0, z1), z0, s(z1))
U5(f58_out1(z0, z1), z2, s(z3)) → f45_out1(z1)
f76_in(z0, 0) → f76_out1(z0)
f76_in(z0, s(z1)) → U6(f76_in(z0, z1), z0, s(z1))
U6(f76_out1(z0), z1, s(z2)) → f76_out1(s(z0))
f41_in(z0, z1) → U7(f45_in(z0, z1), z0, z1)
U7(f45_out1(z0), z1, z2) → U8(f46_in(z0, z1), z1, z2, z0)
U8(f46_out1(z0, z1), z2, z3, z4) → f41_out1(z4, z0, z1)
f46_in(z0, z1) → U9(f65_in(z0, z1), z0, z1)
U9(f65_out1(z0), z1, z2) → U10(f76_in(z0, z2), z1, z2, z0)
U10(f76_out1(z0), z1, z2, z3) → f46_out1(z3, z0)
f58_in(z0, z1) → U11(f45_in(z0, z1), z0, z1)
U11(f45_out1(z0), z1, z2) → U12(f65_in(z0, z1), z1, z2, z0)
U12(f65_out1(z0), z1, z2, z3) → f58_out1(z3, z0)
f18_in(z0) → U13(f20_in(z0), f21_in(z0), z0)
U13(f20_out1(z0), z1, z2) → f18_out1(z0)
U13(z0, f21_out1(z1, z2), z3) → f18_out2(z1, z2)

Tuples:

F58_IN(z0, z1) → c24(U11'(f45_in(z0, z1), z0, z1), F45_IN(z0, z1))
F1_IN(z0, s(0)) → c(F18_IN(z0))
F1_IN(z0, s(s(z1))) → c(F41_IN(z0, z1))
F41_IN(z0, z1) → c(U7'(f45_in(z0, z1), z0, z1))
F41_IN(z0, z1) → c(F45_IN(z0, z1))
U7'(f45_out1(z0), z1, z2) → c(F46_IN(z0, z1))
F46_IN(z0, z1) → c(U9'(f65_in(z0, z1), z0, z1))
F46_IN(z0, z1) → c(F65_IN(z0, z1))
U9'(f65_out1(z0), z1, z2) → c(F76_IN(z0, z2))
U11'(f45_out1(z0), z1, z2) → c(F65_IN(z0, z1))
F18_IN(z0) → c(F20_IN(z0))
F65_IN(z0, s(z1)) → c7(F65_IN(z0, z1))
F20_IN(s(z0)) → c10(F20_IN(z0))
F45_IN(z0, s(z1)) → c13(F58_IN(z0, z1))
F76_IN(z0, s(z1)) → c16(F76_IN(z0, z1))
F1_IN(z0, s(0)) → c
F1_IN(z0, s(s(z1))) → c
U7'(f45_out1(z0), z1, z2) → c
U9'(f65_out1(z0), z1, z2) → c
U11'(f45_out1(z0), z1, z2) → c
F18_IN(z0) → c

S tuples:

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

K tuples:

F1_IN(z0, s(0)) → c(F18_IN(z0))
F1_IN(z0, s(s(z1))) → c(F41_IN(z0, z1))
F41_IN(z0, z1) → c(U7'(f45_in(z0, z1), z0, z1))
F41_IN(z0, z1) → c(F45_IN(z0, z1))
U7'(f45_out1(z0), z1, z2) → c(F46_IN(z0, z1))
F46_IN(z0, z1) → c(U9'(f65_in(z0, z1), z0, z1))
F46_IN(z0, z1) → c(F65_IN(z0, z1))
U9'(f65_out1(z0), z1, z2) → c(F76_IN(z0, z2))
F18_IN(z0) → c(F20_IN(z0))
F1_IN(z0, s(0)) → c
F1_IN(z0, s(s(z1))) → c
U7'(f45_out1(z0), z1, z2) → c
U9'(f65_out1(z0), z1, z2) → c
F18_IN(z0) → c
F58_IN(z0, z1) → c24(U11'(f45_in(z0, z1), z0, z1), F45_IN(z0, z1))
F20_IN(s(z0)) → c10(F20_IN(z0))
F45_IN(z0, s(z1)) → c13(F58_IN(z0, z1))
U11'(f45_out1(z0), z1, z2) → c(F65_IN(z0, z1))
U11'(f45_out1(z0), z1, z2) → c
F76_IN(z0, s(z1)) → c16(F76_IN(z0, z1))

Defined Rule Symbols:

f1_in, U1, U2, f65_in, U3, f20_in, U4, f45_in, U5, f76_in, U6, f41_in, U7, U8, f46_in, U9, U10, f58_in, U11, U12, f18_in, U13

Defined Pair Symbols:

F58_IN, F1_IN, F41_IN, U7', F46_IN, U9', U11', F18_IN, F65_IN, F20_IN, F45_IN, F76_IN

Compound Symbols:

c24, c, c7, c10, c13, c16, c