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

(0) Obligation:

Clauses:

f(0, Y, 0).
f(s(X), Y, Z) :- ','(f(X, Y, U), f(U, Y, Z)).

Query: f(g,a,a)

(1) 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: f(T1, T2, T3)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
3 [label="3: f(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | f(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: true | f(0, T2, T3), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: f(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nX3 is free\nf(T1, T2, T3) !=? f(0, X3, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: f(0, T2, T3), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ','(f(T13, T16, X17), f(X17, T16, T17))\n\nT13 is ground\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: f(T13, T16, X17)\n\nT13 is ground\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: f(T20, T21, T22)\n\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: f(T13, T16, X17), SCOPE: 2, CLAUSE: 0 | f(T13, T16, X17), SCOPE: 2, CLAUSE: 1\n\nT13 is ground\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: true | f(0, T16, X17), SCOPE: 2, CLAUSE: 1\n\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: f(T13, T16, X17), SCOPE: 2, CLAUSE: 1\n\nT13 is ground\nX17 is free\nX24 is free\nf(T13, T16, X17) !=? f(0, X24, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: f(0, T16, X17), SCOPE: 2, CLAUSE: 1\n\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: ','(f(T32, T34, X40), f(X40, T34, X41))\n\nT32 is ground\nX41 is free\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: f(T32, T34, X40)\n\nT32 is ground\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: f(T37, T38, X41)\n\nT37 is ground\nX41 is free", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 45 [arrowhead = none ];
45 -> 3;

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

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

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

49 [label="EVAL with clause\nf(s(X14), X15, X16) :- ','(f(X14, X15, X17), f(X17, X15, X16)).\nand substitutionX14 -> T13,\nT1 -> s(T13),\nT2 -> T16,\nX15 -> T16,\nT3 -> T17,\nX16 -> T17,\nT14 -> T16,\nT15 -> T17", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 49 [arrowhead = none ];
49 -> 20;

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

51 [label="BACKTRACK\nfor clause: f(s(X), Y, Z) :- ','(f(X, Y, U), f(U, Y, Z))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
16 -> 51 [arrowhead = none ];
51 -> 17;

52 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
20 -> 52 [arrowhead = none ];
52 -> 23;

53 [label="SPLIT 2\nnew knowledge:\nT13 is ground\nT20 is ground\nreplacements:X17 -> T20,\nT16 -> T21,\nT17 -> T22", fontsize=14, style = filled, fillcolor = violet];
20 -> 53 [arrowhead = none ];
53 -> 24;

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

55 [label="INSTANCE with matching:\nT1 -> T20\nT2 -> T21\nT3 -> T22", fontsize=14, style = filled, fillcolor = lightgrey];
24 -> 55 [arrowhead = none , style=dashed];
55 -> 2[style=dashed];

56 [label="EVAL with clause\nf(0, X24, 0).\nand substitutionT13 -> 0,\nT16 -> T27,\nX24 -> T27,\nX17 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 56 [arrowhead = none ];
56 -> 32;

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

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

59 [label="EVAL with clause\nf(s(X37), X38, X39) :- ','(f(X37, X38, X40), f(X40, X38, X39)).\nand substitutionX37 -> T32,\nT13 -> s(T32),\nT16 -> T34,\nX38 -> T34,\nX17 -> X41,\nX39 -> X41,\nT33 -> T34", fontsize=14, style = filled, fillcolor = lightblue];
33 -> 59 [arrowhead = none ];
59 -> 38;

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

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

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

63 [label="SPLIT 2\nnew knowledge:\nT32 is ground\nT37 is ground\nreplacements:X40 -> T37,\nT34 -> T38", fontsize=14, style = filled, fillcolor = violet];
38 -> 63 [arrowhead = none ];
63 -> 44;

64 [label="INSTANCE with matching:\nT13 -> T32\nT16 -> T34\nX17 -> X40", fontsize=14, style = filled, fillcolor = lightgrey];
43 -> 64 [arrowhead = none , style=dashed];
64 -> 23[style=dashed];

65 [label="INSTANCE with matching:\nT13 -> T37\nT16 -> T38\nX17 -> X41", fontsize=14, style = filled, fillcolor = lightgrey];
44 -> 65 [arrowhead = none , style=dashed];
65 -> 23[style=dashed];

}

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(0) → f2_out1(0)
f2_in(s(z0)) → U1(f20_in(z0), s(z0))
U1(f20_out1(z0, z1), s(z2)) → f2_out1(z1)
f23_in(0) → f23_out1(0)
f23_in(s(z0)) → U2(f38_in(z0), s(z0))
U2(f38_out1(z0, z1), s(z2)) → f23_out1(z1)
f20_in(z0) → U3(f23_in(z0), z0)
U3(f23_out1(z0), z1) → U4(f2_in(z0), z1, z0)
U4(f2_out1(z0), z1, z2) → f20_out1(z2, z0)
f38_in(z0) → U5(f23_in(z0), z0)
U5(f23_out1(z0), z1) → U6(f23_in(z0), z1, z0)
U6(f23_out1(z0), z1, z2) → f38_out1(z2, z0)

Tuples:

F2_IN(s(z0)) → c1(U1'(f20_in(z0), s(z0)), F20_IN(z0))
F23_IN(s(z0)) → c4(U2'(f38_in(z0), s(z0)), F38_IN(z0))
F20_IN(z0) → c6(U3'(f23_in(z0), z0), F23_IN(z0))
U3'(f23_out1(z0), z1) → c7(U4'(f2_in(z0), z1, z0), F2_IN(z0))
F38_IN(z0) → c9(U5'(f23_in(z0), z0), F23_IN(z0))
U5'(f23_out1(z0), z1) → c10(U6'(f23_in(z0), z1, z0), F23_IN(z0))

S tuples:

F2_IN(s(z0)) → c1(U1'(f20_in(z0), s(z0)), F20_IN(z0))
F23_IN(s(z0)) → c4(U2'(f38_in(z0), s(z0)), F38_IN(z0))
F20_IN(z0) → c6(U3'(f23_in(z0), z0), F23_IN(z0))
U3'(f23_out1(z0), z1) → c7(U4'(f2_in(z0), z1, z0), F2_IN(z0))
F38_IN(z0) → c9(U5'(f23_in(z0), z0), F23_IN(z0))
U5'(f23_out1(z0), z1) → c10(U6'(f23_in(z0), z1, z0), F23_IN(z0))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f23_in, U2, f20_in, U3, U4, f38_in, U5, U6

Defined Pair Symbols:

F2_IN, F23_IN, F20_IN, U3', F38_IN, U5'

Compound Symbols:

c1, c4, c6, c7, c9, c10

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

Removed 4 trailing tuple parts

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(0) → f2_out1(0)
f2_in(s(z0)) → U1(f20_in(z0), s(z0))
U1(f20_out1(z0, z1), s(z2)) → f2_out1(z1)
f23_in(0) → f23_out1(0)
f23_in(s(z0)) → U2(f38_in(z0), s(z0))
U2(f38_out1(z0, z1), s(z2)) → f23_out1(z1)
f20_in(z0) → U3(f23_in(z0), z0)
U3(f23_out1(z0), z1) → U4(f2_in(z0), z1, z0)
U4(f2_out1(z0), z1, z2) → f20_out1(z2, z0)
f38_in(z0) → U5(f23_in(z0), z0)
U5(f23_out1(z0), z1) → U6(f23_in(z0), z1, z0)
U6(f23_out1(z0), z1, z2) → f38_out1(z2, z0)

Tuples:

F20_IN(z0) → c6(U3'(f23_in(z0), z0), F23_IN(z0))
F38_IN(z0) → c9(U5'(f23_in(z0), z0), F23_IN(z0))
F2_IN(s(z0)) → c1(F20_IN(z0))
F23_IN(s(z0)) → c4(F38_IN(z0))
U3'(f23_out1(z0), z1) → c7(F2_IN(z0))
U5'(f23_out1(z0), z1) → c10(F23_IN(z0))

S tuples:

F20_IN(z0) → c6(U3'(f23_in(z0), z0), F23_IN(z0))
F38_IN(z0) → c9(U5'(f23_in(z0), z0), F23_IN(z0))
F2_IN(s(z0)) → c1(F20_IN(z0))
F23_IN(s(z0)) → c4(F38_IN(z0))
U3'(f23_out1(z0), z1) → c7(F2_IN(z0))
U5'(f23_out1(z0), z1) → c10(F23_IN(z0))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f23_in, U2, f20_in, U3, U4, f38_in, U5, U6

Defined Pair Symbols:

F20_IN, F38_IN, F2_IN, F23_IN, U3', U5'

Compound Symbols:

c6, c9, c1, c4, c7, c10

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

F20_IN(z0) → c6(U3'(f23_in(z0), z0), F23_IN(z0))
F38_IN(z0) → c9(U5'(f23_in(z0), z0), F23_IN(z0))
F2_IN(s(z0)) → c1(F20_IN(z0))
F23_IN(s(z0)) → c4(F38_IN(z0))

We considered the (Usable) Rules:

f23_in(0) → f23_out1(0)
f23_in(s(z0)) → U2(f38_in(z0), s(z0))
f38_in(z0) → U5(f23_in(z0), z0)
U2(f38_out1(z0, z1), s(z2)) → f23_out1(z1)
U5(f23_out1(z0), z1) → U6(f23_in(z0), z1, z0)
U6(f23_out1(z0), z1, z2) → f38_out1(z2, z0)

And the Tuples:

F20_IN(z0) → c6(U3'(f23_in(z0), z0), F23_IN(z0))
F38_IN(z0) → c9(U5'(f23_in(z0), z0), F23_IN(z0))
F2_IN(s(z0)) → c1(F20_IN(z0))
F23_IN(s(z0)) → c4(F38_IN(z0))
U3'(f23_out1(z0), z1) → c7(F2_IN(z0))
U5'(f23_out1(z0), z1) → c10(F23_IN(z0))

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

POL(0) = 0   
POL(F20_IN(x₁)) = [1] + [2]x₁   
POL(F23_IN(x₁)) = x₁   
POL(F2_IN(x₁)) = [2]x₁   
POL(F38_IN(x₁)) = [1] + x₁   
POL(U2(x₁, x₂)) = [2]x₁   
POL(U3'(x₁, x₂)) = [2]x₁   
POL(U5(x₁, x₂)) = [3]x₁   
POL(U5'(x₁, x₂)) = [2]x₁   
POL(U6(x₁, x₂, x₃)) = [2]x₁   
POL(c1(x₁)) = x₁   
POL(c10(x₁)) = x₁   
POL(c4(x₁)) = x₁   
POL(c6(x₁, x₂)) = x₁ + x₂   
POL(c7(x₁)) = x₁   
POL(c9(x₁, x₂)) = x₁ + x₂   
POL(f23_in(x₁)) = 0   
POL(f23_out1(x₁)) = x₁   
POL(f38_in(x₁)) = 0   
POL(f38_out1(x₁, x₂)) = x₂   
POL(s(x₁)) = [2] + x₁   

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(0) → f2_out1(0)
f2_in(s(z0)) → U1(f20_in(z0), s(z0))
U1(f20_out1(z0, z1), s(z2)) → f2_out1(z1)
f23_in(0) → f23_out1(0)
f23_in(s(z0)) → U2(f38_in(z0), s(z0))
U2(f38_out1(z0, z1), s(z2)) → f23_out1(z1)
f20_in(z0) → U3(f23_in(z0), z0)
U3(f23_out1(z0), z1) → U4(f2_in(z0), z1, z0)
U4(f2_out1(z0), z1, z2) → f20_out1(z2, z0)
f38_in(z0) → U5(f23_in(z0), z0)
U5(f23_out1(z0), z1) → U6(f23_in(z0), z1, z0)
U6(f23_out1(z0), z1, z2) → f38_out1(z2, z0)

Tuples:

F20_IN(z0) → c6(U3'(f23_in(z0), z0), F23_IN(z0))
F38_IN(z0) → c9(U5'(f23_in(z0), z0), F23_IN(z0))
F2_IN(s(z0)) → c1(F20_IN(z0))
F23_IN(s(z0)) → c4(F38_IN(z0))
U3'(f23_out1(z0), z1) → c7(F2_IN(z0))
U5'(f23_out1(z0), z1) → c10(F23_IN(z0))

S tuples:

U3'(f23_out1(z0), z1) → c7(F2_IN(z0))
U5'(f23_out1(z0), z1) → c10(F23_IN(z0))

K tuples:

F20_IN(z0) → c6(U3'(f23_in(z0), z0), F23_IN(z0))
F38_IN(z0) → c9(U5'(f23_in(z0), z0), F23_IN(z0))
F2_IN(s(z0)) → c1(F20_IN(z0))
F23_IN(s(z0)) → c4(F38_IN(z0))

Defined Rule Symbols:

f2_in, U1, f23_in, U2, f20_in, U3, U4, f38_in, U5, U6

Defined Pair Symbols:

F20_IN, F38_IN, F2_IN, F23_IN, U3', U5'

Compound Symbols:

c6, c9, c1, c4, c7, c10

(7) CdtKnowledgeProof (EQUIVALENT transformation)

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

U3'(f23_out1(z0), z1) → c7(F2_IN(z0))
U5'(f23_out1(z0), z1) → c10(F23_IN(z0))
F2_IN(s(z0)) → c1(F20_IN(z0))
F23_IN(s(z0)) → c4(F38_IN(z0))

Now S is empty

(8) BOUNDS(O(1), O(1))

(9) 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: f(T1, T2, T3)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: f(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | f(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: true | f(0, T2, T3), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: f(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nX2 is free\nf(T1, T2, T3) !=? f(0, X2, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: f(0, T2, T3), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: ','(f(T9, T12, X12), f(X12, T12, T13))\n\nT9 is ground\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: ','(f(T9, T12, X12), f(X12, T12, T13)), SCOPE: 2, CLAUSE: 0 | ','(f(T9, T12, X12), f(X12, T12, T13)), SCOPE: 2, CLAUSE: 1\n\nT9 is ground\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: f(0, T17, T18) | ','(f(0, T12, X12), f(X12, T12, T13)), SCOPE: 2, CLAUSE: 1\n\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(f(T9, T12, X12), f(X12, T12, T13)), SCOPE: 2, CLAUSE: 1\n\nT9 is ground\nX12 is free\nX15 is free\nf(T9, T12, X12) !=? f(0, X15, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: f(0, T17, T18)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(f(0, T12, X12), f(X12, T12, T13)), SCOPE: 2, CLAUSE: 1\n\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: f(0, T17, T18), SCOPE: 3, CLAUSE: 0 | f(0, T17, T18), SCOPE: 3, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: true | f(0, T17, T18), SCOPE: 3, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: f(0, T17, T18), SCOPE: 3, CLAUSE: 1\n\nX22 is free\nf(0, T17, T18) !=? f(0, X22, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: f(0, T17, T18), SCOPE: 3, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: ','(','(f(T30, T32, X44), f(X44, T32, X45)), f(X45, T32, T33))\n\nT30 is ground\nX45 is free\nX44 is free", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: f(T30, T32, X44)\n\nT30 is ground\nX44 is free", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: ','(f(T36, T37, X45), f(X45, T37, T38))\n\nT36 is ground\nX45 is free", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: f(T30, T32, X44), SCOPE: 4, CLAUSE: 0 | f(T30, T32, X44), SCOPE: 4, CLAUSE: 1\n\nT30 is ground\nX44 is free", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: true | f(0, T32, X44), SCOPE: 4, CLAUSE: 1\n\nX44 is free", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: f(T30, T32, X44), SCOPE: 4, CLAUSE: 1\n\nT30 is ground\nX44 is free\nX52 is free\nf(T30, T32, X44) !=? f(0, X52, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: f(0, T32, X44), SCOPE: 4, CLAUSE: 1\n\nX44 is free", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ','(f(T48, T50, X68), f(X68, T50, X69))\n\nT48 is ground\nX69 is free\nX68 is free", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: f(T48, T50, X68)\n\nT48 is ground\nX68 is free", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: f(T53, T54, X69)\n\nT53 is ground\nX69 is free", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 53 [arrowhead = none ];
53 -> 4;

54 [label="EVAL with clause\nf(0, X2, 0).\nand substitutionT1 -> 0,\nT2 -> T5,\nX2 -> T5,\nT3 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 54 [arrowhead = none ];
54 -> 5;

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

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

57 [label="EVAL with clause\nf(s(X9), X10, X11) :- ','(f(X9, X10, X12), f(X12, X10, X11)).\nand substitutionX9 -> T9,\nT1 -> s(T9),\nT2 -> T12,\nX10 -> T12,\nT3 -> T13,\nX11 -> T13,\nT10 -> T12,\nT11 -> T13", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 57 [arrowhead = none ];
57 -> 9;

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

59 [label="BACKTRACK\nfor clause: f(s(X), Y, Z) :- ','(f(X, Y, U), f(U, Y, Z))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
7 -> 59 [arrowhead = none ];
59 -> 8;

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

61 [label="EVAL with clause\nf(0, X15, 0).\nand substitutionT9 -> 0,\nT12 -> T17,\nX15 -> T17,\nX12 -> 0,\nT16 -> T17,\nT13 -> T18", fontsize=14, style = filled, fillcolor = lightblue];
11 -> 61 [arrowhead = none ];
61 -> 12;

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

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

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

65 [label="EVAL with clause\nf(s(X41), X42, X43) :- ','(f(X41, X42, X44), f(X44, X42, X43)).\nand substitutionX41 -> T30,\nT9 -> s(T30),\nT12 -> T32,\nX42 -> T32,\nX12 -> X45,\nX43 -> X45,\nT31 -> T32,\nT13 -> T33", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 65 [arrowhead = none ];
65 -> 36;

66 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
13 -> 66 [arrowhead = none ];
66 -> 37;

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

68 [label="BACKTRACK\nfor clause: f(s(X), Y, Z) :- ','(f(X, Y, U), f(U, Y, Z))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
19 -> 68 [arrowhead = none ];
68 -> 30;

69 [label="EVAL with clause\nf(0, X22, 0).\nand substitutionT17 -> T25,\nX22 -> T25,\nT18 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
22 -> 69 [arrowhead = none ];
69 -> 25;

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

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

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

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

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

75 [label="SPLIT 2\nnew knowledge:\nT30 is ground\nT36 is ground\nreplacements:X44 -> T36,\nT32 -> T37,\nT33 -> T38", fontsize=14, style = filled, fillcolor = violet];
36 -> 75 [arrowhead = none ];
75 -> 40;

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

77 [label="INSTANCE with matching:\nT9 -> T36\nT12 -> T37\nX12 -> X45\nT13 -> T38", fontsize=14, style = filled, fillcolor = lightgrey];
40 -> 77 [arrowhead = none , style=dashed];
77 -> 9[style=dashed];

78 [label="EVAL with clause\nf(0, X52, 0).\nand substitutionT30 -> 0,\nT32 -> T43,\nX52 -> T43,\nX44 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
42 -> 78 [arrowhead = none ];
78 -> 45;

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

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

81 [label="EVAL with clause\nf(s(X65), X66, X67) :- ','(f(X65, X66, X68), f(X68, X66, X67)).\nand substitutionX65 -> T48,\nT30 -> s(T48),\nT32 -> T50,\nX66 -> T50,\nX44 -> X69,\nX67 -> X69,\nT49 -> T50", fontsize=14, style = filled, fillcolor = lightblue];
46 -> 81 [arrowhead = none ];
81 -> 49;

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

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

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

85 [label="SPLIT 2\nnew knowledge:\nT48 is ground\nT53 is ground\nreplacements:X68 -> T53,\nT50 -> T54", fontsize=14, style = filled, fillcolor = violet];
49 -> 85 [arrowhead = none ];
85 -> 52;

86 [label="INSTANCE with matching:\nT30 -> T48\nT32 -> T50\nX44 -> X68", fontsize=14, style = filled, fillcolor = lightgrey];
51 -> 86 [arrowhead = none , style=dashed];
86 -> 39[style=dashed];

87 [label="INSTANCE with matching:\nT30 -> T53\nT32 -> T54\nX44 -> X69", fontsize=14, style = filled, fillcolor = lightgrey];
52 -> 87 [arrowhead = none , style=dashed];
87 -> 39[style=dashed];

}

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0) → f1_out1(0)
f1_in(s(z0)) → U1(f9_in(z0), s(z0))
U1(f9_out1(z0, z1), s(z2)) → f1_out1(z1)
f9_in(0) → U2(f12_in, 0)
f9_in(s(z0)) → U3(f36_in(z0), s(z0))
U2(f12_out1(z0), 0) → f9_out1(0, z0)
U2(f12_out2(z0, z1), 0) → f9_out1(z0, z1)
U3(f36_out1(z0, z1, z2), s(z3)) → f9_out1(z1, z2)
f39_in(0) → f39_out1(0)
f39_in(s(z0)) → U4(f49_in(z0), s(z0))
U4(f49_out1(z0, z1), s(z2)) → f39_out1(z1)
f18_in → f18_out1(0)
f36_in(z0) → U5(f39_in(z0), z0)
U5(f39_out1(z0), z1) → U6(f9_in(z0), z1, z0)
U6(f9_out1(z0, z1), z2, z3) → f36_out1(z3, z0, z1)
f49_in(z0) → U7(f39_in(z0), z0)
U7(f39_out1(z0), z1) → U8(f39_in(z0), z1, z0)
U8(f39_out1(z0), z1, z2) → f49_out1(z2, z0)
f12_in → U9(f18_in, f19_in)
U9(f18_out1(z0), z1) → f12_out1(z0)
U9(z0, f19_out1(z1, z2)) → f12_out2(z1, z2)

Tuples:

F1_IN(s(z0)) → c1(U1'(f9_in(z0), s(z0)), F9_IN(z0))
F9_IN(0) → c3(U2'(f12_in, 0), F12_IN)
F9_IN(s(z0)) → c4(U3'(f36_in(z0), s(z0)), F36_IN(z0))
F39_IN(s(z0)) → c9(U4'(f49_in(z0), s(z0)), F49_IN(z0))
F36_IN(z0) → c12(U5'(f39_in(z0), z0), F39_IN(z0))
U5'(f39_out1(z0), z1) → c13(U6'(f9_in(z0), z1, z0), F9_IN(z0))
F49_IN(z0) → c15(U7'(f39_in(z0), z0), F39_IN(z0))
U7'(f39_out1(z0), z1) → c16(U8'(f39_in(z0), z1, z0), F39_IN(z0))
F12_IN → c18(U9'(f18_in, f19_in), F18_IN)

S tuples:

F1_IN(s(z0)) → c1(U1'(f9_in(z0), s(z0)), F9_IN(z0))
F9_IN(0) → c3(U2'(f12_in, 0), F12_IN)
F9_IN(s(z0)) → c4(U3'(f36_in(z0), s(z0)), F36_IN(z0))
F39_IN(s(z0)) → c9(U4'(f49_in(z0), s(z0)), F49_IN(z0))
F36_IN(z0) → c12(U5'(f39_in(z0), z0), F39_IN(z0))
U5'(f39_out1(z0), z1) → c13(U6'(f9_in(z0), z1, z0), F9_IN(z0))
F49_IN(z0) → c15(U7'(f39_in(z0), z0), F39_IN(z0))
U7'(f39_out1(z0), z1) → c16(U8'(f39_in(z0), z1, z0), F39_IN(z0))
F12_IN → c18(U9'(f18_in, f19_in), F18_IN)

K tuples:none
Defined Rule Symbols:

f1_in, U1, f9_in, U2, U3, f39_in, U4, f18_in, f36_in, U5, U6, f49_in, U7, U8, f12_in, U9

Defined Pair Symbols:

F1_IN, F9_IN, F39_IN, F36_IN, U5', F49_IN, U7', F12_IN

Compound Symbols:

c1, c3, c4, c9, c12, c13, c15, c16, c18

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

Split RHS of tuples not part of any SCC

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0) → f1_out1(0)
f1_in(s(z0)) → U1(f9_in(z0), s(z0))
U1(f9_out1(z0, z1), s(z2)) → f1_out1(z1)
f9_in(0) → U2(f12_in, 0)
f9_in(s(z0)) → U3(f36_in(z0), s(z0))
U2(f12_out1(z0), 0) → f9_out1(0, z0)
U2(f12_out2(z0, z1), 0) → f9_out1(z0, z1)
U3(f36_out1(z0, z1, z2), s(z3)) → f9_out1(z1, z2)
f39_in(0) → f39_out1(0)
f39_in(s(z0)) → U4(f49_in(z0), s(z0))
U4(f49_out1(z0, z1), s(z2)) → f39_out1(z1)
f18_in → f18_out1(0)
f36_in(z0) → U5(f39_in(z0), z0)
U5(f39_out1(z0), z1) → U6(f9_in(z0), z1, z0)
U6(f9_out1(z0, z1), z2, z3) → f36_out1(z3, z0, z1)
f49_in(z0) → U7(f39_in(z0), z0)
U7(f39_out1(z0), z1) → U8(f39_in(z0), z1, z0)
U8(f39_out1(z0), z1, z2) → f49_out1(z2, z0)
f12_in → U9(f18_in, f19_in)
U9(f18_out1(z0), z1) → f12_out1(z0)
U9(z0, f19_out1(z1, z2)) → f12_out2(z1, z2)

Tuples:

F9_IN(s(z0)) → c4(U3'(f36_in(z0), s(z0)), F36_IN(z0))
F39_IN(s(z0)) → c9(U4'(f49_in(z0), s(z0)), F49_IN(z0))
F36_IN(z0) → c12(U5'(f39_in(z0), z0), F39_IN(z0))
U5'(f39_out1(z0), z1) → c13(U6'(f9_in(z0), z1, z0), F9_IN(z0))
F49_IN(z0) → c15(U7'(f39_in(z0), z0), F39_IN(z0))
U7'(f39_out1(z0), z1) → c16(U8'(f39_in(z0), z1, z0), F39_IN(z0))
F1_IN(s(z0)) → c(U1'(f9_in(z0), s(z0)))
F1_IN(s(z0)) → c(F9_IN(z0))
F9_IN(0) → c(U2'(f12_in, 0))
F9_IN(0) → c(F12_IN)
F12_IN → c(U9'(f18_in, f19_in))
F12_IN → c(F18_IN)

S tuples:

F9_IN(s(z0)) → c4(U3'(f36_in(z0), s(z0)), F36_IN(z0))
F39_IN(s(z0)) → c9(U4'(f49_in(z0), s(z0)), F49_IN(z0))
F36_IN(z0) → c12(U5'(f39_in(z0), z0), F39_IN(z0))
U5'(f39_out1(z0), z1) → c13(U6'(f9_in(z0), z1, z0), F9_IN(z0))
F49_IN(z0) → c15(U7'(f39_in(z0), z0), F39_IN(z0))
U7'(f39_out1(z0), z1) → c16(U8'(f39_in(z0), z1, z0), F39_IN(z0))
F1_IN(s(z0)) → c(U1'(f9_in(z0), s(z0)))
F1_IN(s(z0)) → c(F9_IN(z0))
F9_IN(0) → c(U2'(f12_in, 0))
F9_IN(0) → c(F12_IN)
F12_IN → c(U9'(f18_in, f19_in))
F12_IN → c(F18_IN)

K tuples:none
Defined Rule Symbols:

f1_in, U1, f9_in, U2, U3, f39_in, U4, f18_in, f36_in, U5, U6, f49_in, U7, U8, f12_in, U9

Defined Pair Symbols:

F9_IN, F39_IN, F36_IN, U5', F49_IN, U7', F1_IN, F12_IN

Compound Symbols:

c4, c9, c12, c13, c15, c16, c

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

Removed 8 trailing tuple parts

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0) → f1_out1(0)
f1_in(s(z0)) → U1(f9_in(z0), s(z0))
U1(f9_out1(z0, z1), s(z2)) → f1_out1(z1)
f9_in(0) → U2(f12_in, 0)
f9_in(s(z0)) → U3(f36_in(z0), s(z0))
U2(f12_out1(z0), 0) → f9_out1(0, z0)
U2(f12_out2(z0, z1), 0) → f9_out1(z0, z1)
U3(f36_out1(z0, z1, z2), s(z3)) → f9_out1(z1, z2)
f39_in(0) → f39_out1(0)
f39_in(s(z0)) → U4(f49_in(z0), s(z0))
U4(f49_out1(z0, z1), s(z2)) → f39_out1(z1)
f18_in → f18_out1(0)
f36_in(z0) → U5(f39_in(z0), z0)
U5(f39_out1(z0), z1) → U6(f9_in(z0), z1, z0)
U6(f9_out1(z0, z1), z2, z3) → f36_out1(z3, z0, z1)
f49_in(z0) → U7(f39_in(z0), z0)
U7(f39_out1(z0), z1) → U8(f39_in(z0), z1, z0)
U8(f39_out1(z0), z1, z2) → f49_out1(z2, z0)
f12_in → U9(f18_in, f19_in)
U9(f18_out1(z0), z1) → f12_out1(z0)
U9(z0, f19_out1(z1, z2)) → f12_out2(z1, z2)

Tuples:

F36_IN(z0) → c12(U5'(f39_in(z0), z0), F39_IN(z0))
F49_IN(z0) → c15(U7'(f39_in(z0), z0), F39_IN(z0))
F1_IN(s(z0)) → c(F9_IN(z0))
F9_IN(0) → c(F12_IN)
F9_IN(s(z0)) → c4(F36_IN(z0))
F39_IN(s(z0)) → c9(F49_IN(z0))
U5'(f39_out1(z0), z1) → c13(F9_IN(z0))
U7'(f39_out1(z0), z1) → c16(F39_IN(z0))
F1_IN(s(z0)) → c
F9_IN(0) → c
F12_IN → c

S tuples:

F36_IN(z0) → c12(U5'(f39_in(z0), z0), F39_IN(z0))
F49_IN(z0) → c15(U7'(f39_in(z0), z0), F39_IN(z0))
F1_IN(s(z0)) → c(F9_IN(z0))
F9_IN(0) → c(F12_IN)
F9_IN(s(z0)) → c4(F36_IN(z0))
F39_IN(s(z0)) → c9(F49_IN(z0))
U5'(f39_out1(z0), z1) → c13(F9_IN(z0))
U7'(f39_out1(z0), z1) → c16(F39_IN(z0))
F1_IN(s(z0)) → c
F9_IN(0) → c
F12_IN → c

K tuples:none
Defined Rule Symbols:

f1_in, U1, f9_in, U2, U3, f39_in, U4, f18_in, f36_in, U5, U6, f49_in, U7, U8, f12_in, U9

Defined Pair Symbols:

F36_IN, F49_IN, F1_IN, F9_IN, F39_IN, U5', U7', F12_IN

Compound Symbols:

c12, c15, c, c4, c9, c13, c16, c

(15) CdtKnowledgeProof (EQUIVALENT transformation)

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

F1_IN(s(z0)) → c(F9_IN(z0))
F1_IN(s(z0)) → c

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0) → f1_out1(0)
f1_in(s(z0)) → U1(f9_in(z0), s(z0))
U1(f9_out1(z0, z1), s(z2)) → f1_out1(z1)
f9_in(0) → U2(f12_in, 0)
f9_in(s(z0)) → U3(f36_in(z0), s(z0))
U2(f12_out1(z0), 0) → f9_out1(0, z0)
U2(f12_out2(z0, z1), 0) → f9_out1(z0, z1)
U3(f36_out1(z0, z1, z2), s(z3)) → f9_out1(z1, z2)
f39_in(0) → f39_out1(0)
f39_in(s(z0)) → U4(f49_in(z0), s(z0))
U4(f49_out1(z0, z1), s(z2)) → f39_out1(z1)
f18_in → f18_out1(0)
f36_in(z0) → U5(f39_in(z0), z0)
U5(f39_out1(z0), z1) → U6(f9_in(z0), z1, z0)
U6(f9_out1(z0, z1), z2, z3) → f36_out1(z3, z0, z1)
f49_in(z0) → U7(f39_in(z0), z0)
U7(f39_out1(z0), z1) → U8(f39_in(z0), z1, z0)
U8(f39_out1(z0), z1, z2) → f49_out1(z2, z0)
f12_in → U9(f18_in, f19_in)
U9(f18_out1(z0), z1) → f12_out1(z0)
U9(z0, f19_out1(z1, z2)) → f12_out2(z1, z2)

Tuples:

F36_IN(z0) → c12(U5'(f39_in(z0), z0), F39_IN(z0))
F49_IN(z0) → c15(U7'(f39_in(z0), z0), F39_IN(z0))
F1_IN(s(z0)) → c(F9_IN(z0))
F9_IN(0) → c(F12_IN)
F9_IN(s(z0)) → c4(F36_IN(z0))
F39_IN(s(z0)) → c9(F49_IN(z0))
U5'(f39_out1(z0), z1) → c13(F9_IN(z0))
U7'(f39_out1(z0), z1) → c16(F39_IN(z0))
F1_IN(s(z0)) → c
F9_IN(0) → c
F12_IN → c

S tuples:

F36_IN(z0) → c12(U5'(f39_in(z0), z0), F39_IN(z0))
F49_IN(z0) → c15(U7'(f39_in(z0), z0), F39_IN(z0))
F9_IN(0) → c(F12_IN)
F9_IN(s(z0)) → c4(F36_IN(z0))
F39_IN(s(z0)) → c9(F49_IN(z0))
U5'(f39_out1(z0), z1) → c13(F9_IN(z0))
U7'(f39_out1(z0), z1) → c16(F39_IN(z0))
F9_IN(0) → c
F12_IN → c

K tuples:

F1_IN(s(z0)) → c(F9_IN(z0))
F1_IN(s(z0)) → c

Defined Rule Symbols:

f1_in, U1, f9_in, U2, U3, f39_in, U4, f18_in, f36_in, U5, U6, f49_in, U7, U8, f12_in, U9

Defined Pair Symbols:

F36_IN, F49_IN, F1_IN, F9_IN, F39_IN, U5', U7', F12_IN

Compound Symbols:

c12, c15, c, c4, c9, c13, c16, c

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

F9_IN(0) → c(F12_IN)
F9_IN(0) → c

We considered the (Usable) Rules:

f39_in(0) → f39_out1(0)
f39_in(s(z0)) → U4(f49_in(z0), s(z0))
f49_in(z0) → U7(f39_in(z0), z0)
U4(f49_out1(z0, z1), s(z2)) → f39_out1(z1)
U7(f39_out1(z0), z1) → U8(f39_in(z0), z1, z0)
U8(f39_out1(z0), z1, z2) → f49_out1(z2, z0)

And the Tuples:

F36_IN(z0) → c12(U5'(f39_in(z0), z0), F39_IN(z0))
F49_IN(z0) → c15(U7'(f39_in(z0), z0), F39_IN(z0))
F1_IN(s(z0)) → c(F9_IN(z0))
F9_IN(0) → c(F12_IN)
F9_IN(s(z0)) → c4(F36_IN(z0))
F39_IN(s(z0)) → c9(F49_IN(z0))
U5'(f39_out1(z0), z1) → c13(F9_IN(z0))
U7'(f39_out1(z0), z1) → c16(F39_IN(z0))
F1_IN(s(z0)) → c
F9_IN(0) → c
F12_IN → c

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

POL(0) = 0   
POL(F12_IN) = 0   
POL(F1_IN(x₁)) = [1] + [2]x₁   
POL(F36_IN(x₁)) = [2]   
POL(F39_IN(x₁)) = 0   
POL(F49_IN(x₁)) = 0   
POL(F9_IN(x₁)) = [2]   
POL(U4(x₁, x₂)) = 0   
POL(U5'(x₁, x₂)) = [2]   
POL(U7(x₁, x₂)) = [3] + [2]x₂   
POL(U7'(x₁, x₂)) = 0   
POL(U8(x₁, x₂, x₃)) = [3] + [3]x₁   
POL(c) = 0   
POL(c(x₁)) = x₁   
POL(c12(x₁, x₂)) = x₁ + x₂   
POL(c13(x₁)) = x₁   
POL(c15(x₁, x₂)) = x₁ + x₂   
POL(c16(x₁)) = x₁   
POL(c4(x₁)) = x₁   
POL(c9(x₁)) = x₁   
POL(f39_in(x₁)) = 0   
POL(f39_out1(x₁)) = [3]   
POL(f49_in(x₁)) = [3] + [2]x₁   
POL(f49_out1(x₁, x₂)) = [1]   
POL(s(x₁)) = [2] + x₁   

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0) → f1_out1(0)
f1_in(s(z0)) → U1(f9_in(z0), s(z0))
U1(f9_out1(z0, z1), s(z2)) → f1_out1(z1)
f9_in(0) → U2(f12_in, 0)
f9_in(s(z0)) → U3(f36_in(z0), s(z0))
U2(f12_out1(z0), 0) → f9_out1(0, z0)
U2(f12_out2(z0, z1), 0) → f9_out1(z0, z1)
U3(f36_out1(z0, z1, z2), s(z3)) → f9_out1(z1, z2)
f39_in(0) → f39_out1(0)
f39_in(s(z0)) → U4(f49_in(z0), s(z0))
U4(f49_out1(z0, z1), s(z2)) → f39_out1(z1)
f18_in → f18_out1(0)
f36_in(z0) → U5(f39_in(z0), z0)
U5(f39_out1(z0), z1) → U6(f9_in(z0), z1, z0)
U6(f9_out1(z0, z1), z2, z3) → f36_out1(z3, z0, z1)
f49_in(z0) → U7(f39_in(z0), z0)
U7(f39_out1(z0), z1) → U8(f39_in(z0), z1, z0)
U8(f39_out1(z0), z1, z2) → f49_out1(z2, z0)
f12_in → U9(f18_in, f19_in)
U9(f18_out1(z0), z1) → f12_out1(z0)
U9(z0, f19_out1(z1, z2)) → f12_out2(z1, z2)

Tuples:

F36_IN(z0) → c12(U5'(f39_in(z0), z0), F39_IN(z0))
F49_IN(z0) → c15(U7'(f39_in(z0), z0), F39_IN(z0))
F1_IN(s(z0)) → c(F9_IN(z0))
F9_IN(0) → c(F12_IN)
F9_IN(s(z0)) → c4(F36_IN(z0))
F39_IN(s(z0)) → c9(F49_IN(z0))
U5'(f39_out1(z0), z1) → c13(F9_IN(z0))
U7'(f39_out1(z0), z1) → c16(F39_IN(z0))
F1_IN(s(z0)) → c
F9_IN(0) → c
F12_IN → c

S tuples:

F36_IN(z0) → c12(U5'(f39_in(z0), z0), F39_IN(z0))
F49_IN(z0) → c15(U7'(f39_in(z0), z0), F39_IN(z0))
F9_IN(s(z0)) → c4(F36_IN(z0))
F39_IN(s(z0)) → c9(F49_IN(z0))
U5'(f39_out1(z0), z1) → c13(F9_IN(z0))
U7'(f39_out1(z0), z1) → c16(F39_IN(z0))
F12_IN → c

K tuples:

F1_IN(s(z0)) → c(F9_IN(z0))
F1_IN(s(z0)) → c
F9_IN(0) → c(F12_IN)
F9_IN(0) → c

Defined Rule Symbols:

f1_in, U1, f9_in, U2, U3, f39_in, U4, f18_in, f36_in, U5, U6, f49_in, U7, U8, f12_in, U9

Defined Pair Symbols:

F36_IN, F49_IN, F1_IN, F9_IN, F39_IN, U5', U7', F12_IN

Compound Symbols:

c12, c15, c, c4, c9, c13, c16, c