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, Z) :- ','(!, eq(Z, 0)).
f(X, Y, Z) :- ','(p(X, P), ','(f(P, Y, U), f(U, Y, Z))).
p(0, 0).
p(s(X), X).
eq(X, X).

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];
5 [label="5: ','(!_1, eq(T10, 0)) | f(0, T2, T3), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: f(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nX5 is free\nX6 is free\nf(T1, T2, T3) !=? f(0, X5, X6)", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: eq(T10, 0)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: eq(T10, 0), SCOPE: 2, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ','(p(T23, X24), ','(f(X24, T26, X25), f(X25, T26, T27)))\n\nT23 is ground\nX5 is free\nX6 is free\nX24 is free\nX25 is free\nf(T23, T2, T3) !=? f(0, X5, X6)", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: ','(p(T23, X24), ','(f(X24, T26, X25), f(X25, T26, T27))), SCOPE: 3, CLAUSE: 2 | ','(p(T23, X24), ','(f(X24, T26, X25), f(X25, T26, T27))), SCOPE: 3, CLAUSE: 3\n\nT23 is ground\nX5 is free\nX6 is free\nX24 is free\nX25 is free\nf(T23, T2, T3) !=? f(0, X5, X6)", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: ','(p(T23, X24), ','(f(X24, T26, X25), f(X25, T26, T27))), SCOPE: 3, CLAUSE: 3\n\nT23 is ground\nX5 is free\nX6 is free\nX24 is free\nX25 is free\nf(T23, T2, T3) !=? f(0, X5, X6)", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: ','(f(T31, T26, X25), f(X25, T26, T27))\n\nT31 is ground\nX25 is free", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: f(T31, T26, X25)\n\nT31 is ground\nX25 is free", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: f(T33, T34, T35)\n\nT33 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: f(T31, T26, X25), SCOPE: 4, CLAUSE: 0 | f(T31, T26, X25), SCOPE: 4, CLAUSE: 1\n\nT31 is ground\nX25 is free", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: ','(!_4, eq(X46, 0)) | f(0, T26, X25), SCOPE: 4, CLAUSE: 1\n\nX25 is free\nX46 is free", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: f(T31, T26, X25), SCOPE: 4, CLAUSE: 1\n\nT31 is ground\nX25 is free\nX44 is free\nX45 is free\nf(T31, T26, X25) !=? f(0, X44, X45)", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: eq(X46, 0)\n\nX46 is free", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: eq(X46, 0), SCOPE: 5, CLAUSE: 4\n\nX46 is free", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: ','(p(T46, X69), ','(f(X69, T48, X70), f(X70, T48, X71)))\n\nT46 is ground\nX25 is free\nX44 is free\nX45 is free\nX71 is free\nX69 is free\nX70 is free\nf(T46, T26, X25) !=? f(0, X44, X45)", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: ','(p(T46, X69), ','(f(X69, T48, X70), f(X70, T48, X71))), SCOPE: 6, CLAUSE: 2 | ','(p(T46, X69), ','(f(X69, T48, X70), f(X70, T48, X71))), SCOPE: 6, CLAUSE: 3\n\nT46 is ground\nX25 is free\nX44 is free\nX45 is free\nX71 is free\nX69 is free\nX70 is free\nf(T46, T26, X25) !=? f(0, X44, X45)", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: ','(p(T46, X69), ','(f(X69, T48, X70), f(X70, T48, X71))), SCOPE: 6, CLAUSE: 3\n\nT46 is ground\nX25 is free\nX44 is free\nX45 is free\nX71 is free\nX69 is free\nX70 is free\nf(T46, T26, X25) !=? f(0, X44, X45)", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: ','(f(T52, T48, X70), f(X70, T48, X71))\n\nT52 is ground\nX71 is free\nX70 is free", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: f(T52, T48, X70)\n\nT52 is ground\nX70 is free", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: f(T54, T55, X71)\n\nT54 is ground\nX71 is free", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 61 [arrowhead = none ];
61 -> 3;

62 [label="EVAL with clause\nf(0, X5, X6) :- ','(!_1, eq(X6, 0)).\nand substitutionT1 -> 0,\nT2 -> T8,\nX5 -> T8,\nT3 -> T10,\nX6 -> T10,\nT9 -> T10", fontsize=14, style = filled, fillcolor = lightblue];
3 -> 62 [arrowhead = none ];
62 -> 5;

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

64 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
5 -> 64 [arrowhead = none ];
64 -> 8;

65 [label="ONLY EVAL with clause\nf(X21, X22, X23) :- ','(p(X21, X24), ','(f(X24, X22, X25), f(X25, X22, X23))).\nand substitutionT1 -> T23,\nX21 -> T23,\nT2 -> T26,\nX22 -> T26,\nT3 -> T27,\nX23 -> T27,\nT24 -> T26,\nT25 -> T27", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 65 [arrowhead = none ];
65 -> 20;

66 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
8 -> 66 [arrowhead = none ];
66 -> 10;

67 [label="EVAL with clause\neq(X9, X9).\nand substitutionT10 -> 0,\nX9 -> 0,\nT13 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 67 [arrowhead = none ];
67 -> 13;

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

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

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

71 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (f(T23, T2, T3), f(0, X5, X6))", fontsize=14, style = filled, fillcolor = lightgreen];
23 -> 71 [arrowhead = none ];
71 -> 24;

72 [label="EVAL with clause\np(s(X31), X31).\nand substitutionX31 -> T31,\nT23 -> s(T31),\nX24 -> T31", fontsize=14, style = filled, fillcolor = lightblue];
24 -> 72 [arrowhead = none ];
72 -> 27;

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

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

75 [label="SPLIT 2\nnew knowledge:\nT31 is ground\nT33 is ground\nreplacements:X25 -> T33,\nT26 -> T34,\nT27 -> T35", fontsize=14, style = filled, fillcolor = violet];
27 -> 75 [arrowhead = none ];
75 -> 32;

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

77 [label="INSTANCE with matching:\nT1 -> T33\nT2 -> T34\nT3 -> T35", fontsize=14, style = filled, fillcolor = lightgrey];
32 -> 77 [arrowhead = none , style=dashed];
77 -> 2[style=dashed];

78 [label="EVAL with clause\nf(0, X44, X45) :- ','(!_4, eq(X45, 0)).\nand substitutionT31 -> 0,\nT26 -> T39,\nX44 -> T39,\nX25 -> X46,\nX45 -> X46", fontsize=14, style = filled, fillcolor = lightblue];
34 -> 78 [arrowhead = none ];
78 -> 37;

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

80 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
37 -> 80 [arrowhead = none ];
80 -> 41;

81 [label="ONLY EVAL with clause\nf(X66, X67, X68) :- ','(p(X66, X69), ','(f(X69, X67, X70), f(X70, X67, X68))).\nand substitutionT31 -> T46,\nX66 -> T46,\nT26 -> T48,\nX67 -> T48,\nX25 -> X71,\nX68 -> X71,\nT47 -> T48", fontsize=14, style = filled, fillcolor = lightblue];
40 -> 81 [arrowhead = none ];
81 -> 48;

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

83 [label="ONLY EVAL with clause\neq(X51, X51).\nand substitutionX46 -> 0,\nX51 -> 0,\nX52 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
42 -> 83 [arrowhead = none ];
83 -> 45;

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

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

86 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (f(T46, T26, X25), f(0, X44, X45))", fontsize=14, style = filled, fillcolor = lightgreen];
51 -> 86 [arrowhead = none ];
86 -> 52;

87 [label="EVAL with clause\np(s(X77), X77).\nand substitutionX77 -> T52,\nT46 -> s(T52),\nX69 -> T52", fontsize=14, style = filled, fillcolor = lightblue];
52 -> 87 [arrowhead = none ];
87 -> 55;

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

89 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
55 -> 89 [arrowhead = none ];
89 -> 59;

90 [label="SPLIT 2\nnew knowledge:\nT52 is ground\nT54 is ground\nreplacements:X70 -> T54,\nT48 -> T55", fontsize=14, style = filled, fillcolor = violet];
55 -> 90 [arrowhead = none ];
90 -> 60;

91 [label="INSTANCE with matching:\nT31 -> T52\nT26 -> T48\nX25 -> X70", fontsize=14, style = filled, fillcolor = lightgrey];
59 -> 91 [arrowhead = none , style=dashed];
91 -> 30[style=dashed];

92 [label="INSTANCE with matching:\nT31 -> T54\nT26 -> T55\nX25 -> X71", fontsize=14, style = filled, fillcolor = lightgrey];
60 -> 92 [arrowhead = none , style=dashed];
92 -> 30[style=dashed];

}

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(0) → f2_out1(0)
f2_in(s(z0)) → U1(f27_in(z0), s(z0))
U1(f27_out1(z0, z1), s(z2)) → f2_out1(z1)
f30_in(0) → f30_out1(0)
f30_in(s(z0)) → U2(f55_in(z0), s(z0))
U2(f55_out1(z0, z1), s(z2)) → f30_out1(z1)
f27_in(z0) → U3(f30_in(z0), z0)
U3(f30_out1(z0), z1) → U4(f2_in(z0), z1, z0)
U4(f2_out1(z0), z1, z2) → f27_out1(z2, z0)
f55_in(z0) → U5(f30_in(z0), z0)
U5(f30_out1(z0), z1) → U6(f30_in(z0), z1, z0)
U6(f30_out1(z0), z1, z2) → f55_out1(z2, z0)

Tuples:

F2_IN(s(z0)) → c1(U1'(f27_in(z0), s(z0)), F27_IN(z0))
F30_IN(s(z0)) → c4(U2'(f55_in(z0), s(z0)), F55_IN(z0))
F27_IN(z0) → c6(U3'(f30_in(z0), z0), F30_IN(z0))
U3'(f30_out1(z0), z1) → c7(U4'(f2_in(z0), z1, z0), F2_IN(z0))
F55_IN(z0) → c9(U5'(f30_in(z0), z0), F30_IN(z0))
U5'(f30_out1(z0), z1) → c10(U6'(f30_in(z0), z1, z0), F30_IN(z0))

S tuples:

F2_IN(s(z0)) → c1(U1'(f27_in(z0), s(z0)), F27_IN(z0))
F30_IN(s(z0)) → c4(U2'(f55_in(z0), s(z0)), F55_IN(z0))
F27_IN(z0) → c6(U3'(f30_in(z0), z0), F30_IN(z0))
U3'(f30_out1(z0), z1) → c7(U4'(f2_in(z0), z1, z0), F2_IN(z0))
F55_IN(z0) → c9(U5'(f30_in(z0), z0), F30_IN(z0))
U5'(f30_out1(z0), z1) → c10(U6'(f30_in(z0), z1, z0), F30_IN(z0))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f30_in, U2, f27_in, U3, U4, f55_in, U5, U6

Defined Pair Symbols:

F2_IN, F30_IN, F27_IN, U3', F55_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(f27_in(z0), s(z0))
U1(f27_out1(z0, z1), s(z2)) → f2_out1(z1)
f30_in(0) → f30_out1(0)
f30_in(s(z0)) → U2(f55_in(z0), s(z0))
U2(f55_out1(z0, z1), s(z2)) → f30_out1(z1)
f27_in(z0) → U3(f30_in(z0), z0)
U3(f30_out1(z0), z1) → U4(f2_in(z0), z1, z0)
U4(f2_out1(z0), z1, z2) → f27_out1(z2, z0)
f55_in(z0) → U5(f30_in(z0), z0)
U5(f30_out1(z0), z1) → U6(f30_in(z0), z1, z0)
U6(f30_out1(z0), z1, z2) → f55_out1(z2, z0)

Tuples:

F27_IN(z0) → c6(U3'(f30_in(z0), z0), F30_IN(z0))
F55_IN(z0) → c9(U5'(f30_in(z0), z0), F30_IN(z0))
F2_IN(s(z0)) → c1(F27_IN(z0))
F30_IN(s(z0)) → c4(F55_IN(z0))
U3'(f30_out1(z0), z1) → c7(F2_IN(z0))
U5'(f30_out1(z0), z1) → c10(F30_IN(z0))

S tuples:

F27_IN(z0) → c6(U3'(f30_in(z0), z0), F30_IN(z0))
F55_IN(z0) → c9(U5'(f30_in(z0), z0), F30_IN(z0))
F2_IN(s(z0)) → c1(F27_IN(z0))
F30_IN(s(z0)) → c4(F55_IN(z0))
U3'(f30_out1(z0), z1) → c7(F2_IN(z0))
U5'(f30_out1(z0), z1) → c10(F30_IN(z0))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f30_in, U2, f27_in, U3, U4, f55_in, U5, U6

Defined Pair Symbols:

F27_IN, F55_IN, F2_IN, F30_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.

F27_IN(z0) → c6(U3'(f30_in(z0), z0), F30_IN(z0))
F55_IN(z0) → c9(U5'(f30_in(z0), z0), F30_IN(z0))
F2_IN(s(z0)) → c1(F27_IN(z0))
F30_IN(s(z0)) → c4(F55_IN(z0))

We considered the (Usable) Rules:

f30_in(0) → f30_out1(0)
f30_in(s(z0)) → U2(f55_in(z0), s(z0))
f55_in(z0) → U5(f30_in(z0), z0)
U2(f55_out1(z0, z1), s(z2)) → f30_out1(z1)
U5(f30_out1(z0), z1) → U6(f30_in(z0), z1, z0)
U6(f30_out1(z0), z1, z2) → f55_out1(z2, z0)

And the Tuples:

F27_IN(z0) → c6(U3'(f30_in(z0), z0), F30_IN(z0))
F55_IN(z0) → c9(U5'(f30_in(z0), z0), F30_IN(z0))
F2_IN(s(z0)) → c1(F27_IN(z0))
F30_IN(s(z0)) → c4(F55_IN(z0))
U3'(f30_out1(z0), z1) → c7(F2_IN(z0))
U5'(f30_out1(z0), z1) → c10(F30_IN(z0))

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

POL(0) = 0   
POL(F27_IN(x₁)) = [1] + [2]x₁   
POL(F2_IN(x₁)) = [2]x₁   
POL(F30_IN(x₁)) = x₁   
POL(F55_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(f30_in(x₁)) = 0   
POL(f30_out1(x₁)) = x₁   
POL(f55_in(x₁)) = 0   
POL(f55_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(f27_in(z0), s(z0))
U1(f27_out1(z0, z1), s(z2)) → f2_out1(z1)
f30_in(0) → f30_out1(0)
f30_in(s(z0)) → U2(f55_in(z0), s(z0))
U2(f55_out1(z0, z1), s(z2)) → f30_out1(z1)
f27_in(z0) → U3(f30_in(z0), z0)
U3(f30_out1(z0), z1) → U4(f2_in(z0), z1, z0)
U4(f2_out1(z0), z1, z2) → f27_out1(z2, z0)
f55_in(z0) → U5(f30_in(z0), z0)
U5(f30_out1(z0), z1) → U6(f30_in(z0), z1, z0)
U6(f30_out1(z0), z1, z2) → f55_out1(z2, z0)

Tuples:

F27_IN(z0) → c6(U3'(f30_in(z0), z0), F30_IN(z0))
F55_IN(z0) → c9(U5'(f30_in(z0), z0), F30_IN(z0))
F2_IN(s(z0)) → c1(F27_IN(z0))
F30_IN(s(z0)) → c4(F55_IN(z0))
U3'(f30_out1(z0), z1) → c7(F2_IN(z0))
U5'(f30_out1(z0), z1) → c10(F30_IN(z0))

S tuples:

U3'(f30_out1(z0), z1) → c7(F2_IN(z0))
U5'(f30_out1(z0), z1) → c10(F30_IN(z0))

K tuples:

F27_IN(z0) → c6(U3'(f30_in(z0), z0), F30_IN(z0))
F55_IN(z0) → c9(U5'(f30_in(z0), z0), F30_IN(z0))
F2_IN(s(z0)) → c1(F27_IN(z0))
F30_IN(s(z0)) → c4(F55_IN(z0))

Defined Rule Symbols:

f2_in, U1, f30_in, U2, f27_in, U3, U4, f55_in, U5, U6

Defined Pair Symbols:

F27_IN, F55_IN, F2_IN, F30_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'(f30_out1(z0), z1) → c7(F2_IN(z0))
U5'(f30_out1(z0), z1) → c10(F30_IN(z0))
F2_IN(s(z0)) → c1(F27_IN(z0))
F30_IN(s(z0)) → c4(F55_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];
6 [label="6: ','(!_1, eq(T8, 0)) | f(0, T2, T3), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: f(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nX3 is free\nX4 is free\nf(T1, T2, T3) !=? f(0, X3, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: eq(T8, 0)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: eq(T8, 0), SCOPE: 2, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(p(T15, X14), ','(f(X14, T18, X15), f(X15, T18, T19)))\n\nT15 is ground\nX3 is free\nX4 is free\nX14 is free\nX15 is free\nf(T15, T2, T3) !=? f(0, X3, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: ','(p(T15, X14), ','(f(X14, T18, X15), f(X15, T18, T19))), SCOPE: 3, CLAUSE: 2 | ','(p(T15, X14), ','(f(X14, T18, X15), f(X15, T18, T19))), SCOPE: 3, CLAUSE: 3\n\nT15 is ground\nX3 is free\nX4 is free\nX14 is free\nX15 is free\nf(T15, T2, T3) !=? f(0, X3, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: ','(p(T15, X14), ','(f(X14, T18, X15), f(X15, T18, T19))), SCOPE: 3, CLAUSE: 3\n\nT15 is ground\nX3 is free\nX4 is free\nX14 is free\nX15 is free\nf(T15, T2, T3) !=? f(0, X3, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: ','(f(T22, T18, X15), f(X15, T18, T19))\n\nT22 is ground\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: f(T22, T18, X15)\n\nT22 is ground\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: f(T24, T25, T26)\n\nT24 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: f(T22, T18, X15), SCOPE: 4, CLAUSE: 0 | f(T22, T18, X15), SCOPE: 4, CLAUSE: 1\n\nT22 is ground\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: ','(!_4, eq(X33, 0)) | f(0, T18, X15), SCOPE: 4, CLAUSE: 1\n\nX15 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: f(T22, T18, X15), SCOPE: 4, CLAUSE: 1\n\nT22 is ground\nX15 is free\nX31 is free\nX32 is free\nf(T22, T18, X15) !=? f(0, X31, X32)", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: eq(X33, 0)\n\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: eq(X33, 0), SCOPE: 5, CLAUSE: 4\n\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: ','(p(T37, X56), ','(f(X56, T39, X57), f(X57, T39, X58)))\n\nT37 is ground\nX15 is free\nX31 is free\nX32 is free\nX58 is free\nX56 is free\nX57 is free\nf(T37, T18, X15) !=? f(0, X31, X32)", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ','(p(T37, X56), ','(f(X56, T39, X57), f(X57, T39, X58))), SCOPE: 6, CLAUSE: 2 | ','(p(T37, X56), ','(f(X56, T39, X57), f(X57, T39, X58))), SCOPE: 6, CLAUSE: 3\n\nT37 is ground\nX15 is free\nX31 is free\nX32 is free\nX58 is free\nX56 is free\nX57 is free\nf(T37, T18, X15) !=? f(0, X31, X32)", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: ','(p(T37, X56), ','(f(X56, T39, X57), f(X57, T39, X58))), SCOPE: 6, CLAUSE: 3\n\nT37 is ground\nX15 is free\nX31 is free\nX32 is free\nX58 is free\nX56 is free\nX57 is free\nf(T37, T18, X15) !=? f(0, X31, X32)", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: ','(f(T43, T39, X57), f(X57, T39, X58))\n\nT43 is ground\nX58 is free\nX57 is free", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: f(T43, T39, X57)\n\nT43 is ground\nX57 is free", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: f(T45, T46, X58)\n\nT45 is ground\nX58 is free", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 59 [arrowhead = none ];
59 -> 4;

60 [label="EVAL with clause\nf(0, X3, X4) :- ','(!_1, eq(X4, 0)).\nand substitutionT1 -> 0,\nT2 -> T6,\nX3 -> T6,\nT3 -> T8,\nX4 -> T8,\nT7 -> T8", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 60 [arrowhead = none ];
60 -> 6;

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

62 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
6 -> 62 [arrowhead = none ];
62 -> 11;

63 [label="ONLY EVAL with clause\nf(X11, X12, X13) :- ','(p(X11, X14), ','(f(X14, X12, X15), f(X15, X12, X13))).\nand substitutionT1 -> T15,\nX11 -> T15,\nT2 -> T18,\nX12 -> T18,\nT3 -> T19,\nX13 -> T19,\nT16 -> T18,\nT17 -> T19", fontsize=14, style = filled, fillcolor = lightblue];
9 -> 63 [arrowhead = none ];
63 -> 19;

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

65 [label="EVAL with clause\neq(X7, X7).\nand substitutionT8 -> 0,\nX7 -> 0,\nT11 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 65 [arrowhead = none ];
65 -> 15;

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

67 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
15 -> 67 [arrowhead = none ];
67 -> 18;

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

69 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (f(T15, T2, T3), f(0, X3, X4))", fontsize=14, style = filled, fillcolor = lightgreen];
21 -> 69 [arrowhead = none ];
69 -> 22;

70 [label="EVAL with clause\np(s(X18), X18).\nand substitutionX18 -> T22,\nT15 -> s(T22),\nX14 -> T22", fontsize=14, style = filled, fillcolor = lightblue];
22 -> 70 [arrowhead = none ];
70 -> 25;

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

72 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
25 -> 72 [arrowhead = none ];
72 -> 29;

73 [label="SPLIT 2\nnew knowledge:\nT22 is ground\nT24 is ground\nreplacements:X15 -> T24,\nT18 -> T25,\nT19 -> T26", fontsize=14, style = filled, fillcolor = violet];
25 -> 73 [arrowhead = none ];
73 -> 31;

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

75 [label="INSTANCE with matching:\nT1 -> T24\nT2 -> T25\nT3 -> T26", fontsize=14, style = filled, fillcolor = lightgrey];
31 -> 75 [arrowhead = none , style=dashed];
75 -> 1[style=dashed];

76 [label="EVAL with clause\nf(0, X31, X32) :- ','(!_4, eq(X32, 0)).\nand substitutionT22 -> 0,\nT18 -> T30,\nX31 -> T30,\nX15 -> X33,\nX32 -> X33", fontsize=14, style = filled, fillcolor = lightblue];
33 -> 76 [arrowhead = none ];
76 -> 35;

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

78 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
35 -> 78 [arrowhead = none ];
78 -> 38;

79 [label="ONLY EVAL with clause\nf(X53, X54, X55) :- ','(p(X53, X56), ','(f(X56, X54, X57), f(X57, X54, X55))).\nand substitutionT22 -> T37,\nX53 -> T37,\nT18 -> T39,\nX54 -> T39,\nX15 -> X58,\nX55 -> X58,\nT38 -> T39", fontsize=14, style = filled, fillcolor = lightblue];
36 -> 79 [arrowhead = none ];
79 -> 47;

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

81 [label="ONLY EVAL with clause\neq(X38, X38).\nand substitutionX33 -> 0,\nX38 -> 0,\nX39 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
39 -> 81 [arrowhead = none ];
81 -> 43;

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

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

84 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (f(T37, T18, X15), f(0, X31, X32))", fontsize=14, style = filled, fillcolor = lightgreen];
49 -> 84 [arrowhead = none ];
84 -> 50;

85 [label="EVAL with clause\np(s(X64), X64).\nand substitutionX64 -> T43,\nT37 -> s(T43),\nX56 -> T43", fontsize=14, style = filled, fillcolor = lightblue];
50 -> 85 [arrowhead = none ];
85 -> 53;

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

87 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
53 -> 87 [arrowhead = none ];
87 -> 57;

88 [label="SPLIT 2\nnew knowledge:\nT43 is ground\nT45 is ground\nreplacements:X57 -> T45,\nT39 -> T46", fontsize=14, style = filled, fillcolor = violet];
53 -> 88 [arrowhead = none ];
88 -> 58;

89 [label="INSTANCE with matching:\nT22 -> T43\nT18 -> T39\nX15 -> X57", fontsize=14, style = filled, fillcolor = lightgrey];
57 -> 89 [arrowhead = none , style=dashed];
89 -> 29[style=dashed];

90 [label="INSTANCE with matching:\nT22 -> T45\nT18 -> T46\nX15 -> X58", fontsize=14, style = filled, fillcolor = lightgrey];
58 -> 90 [arrowhead = none , style=dashed];
90 -> 29[style=dashed];

}

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0) → f1_out1(0)
f1_in(s(z0)) → U1(f25_in(z0), s(z0))
U1(f25_out1(z0, z1), s(z2)) → f1_out1(z1)
f29_in(0) → f29_out1(0)
f29_in(s(z0)) → U2(f53_in(z0), s(z0))
U2(f53_out1(z0, z1), s(z2)) → f29_out1(z1)
f25_in(z0) → U3(f29_in(z0), z0)
U3(f29_out1(z0), z1) → U4(f1_in(z0), z1, z0)
U4(f1_out1(z0), z1, z2) → f25_out1(z2, z0)
f53_in(z0) → U5(f29_in(z0), z0)
U5(f29_out1(z0), z1) → U6(f29_in(z0), z1, z0)
U6(f29_out1(z0), z1, z2) → f53_out1(z2, z0)

Tuples:

F1_IN(s(z0)) → c1(U1'(f25_in(z0), s(z0)), F25_IN(z0))
F29_IN(s(z0)) → c4(U2'(f53_in(z0), s(z0)), F53_IN(z0))
F25_IN(z0) → c6(U3'(f29_in(z0), z0), F29_IN(z0))
U3'(f29_out1(z0), z1) → c7(U4'(f1_in(z0), z1, z0), F1_IN(z0))
F53_IN(z0) → c9(U5'(f29_in(z0), z0), F29_IN(z0))
U5'(f29_out1(z0), z1) → c10(U6'(f29_in(z0), z1, z0), F29_IN(z0))

S tuples:

F1_IN(s(z0)) → c1(U1'(f25_in(z0), s(z0)), F25_IN(z0))
F29_IN(s(z0)) → c4(U2'(f53_in(z0), s(z0)), F53_IN(z0))
F25_IN(z0) → c6(U3'(f29_in(z0), z0), F29_IN(z0))
U3'(f29_out1(z0), z1) → c7(U4'(f1_in(z0), z1, z0), F1_IN(z0))
F53_IN(z0) → c9(U5'(f29_in(z0), z0), F29_IN(z0))
U5'(f29_out1(z0), z1) → c10(U6'(f29_in(z0), z1, z0), F29_IN(z0))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f29_in, U2, f25_in, U3, U4, f53_in, U5, U6

Defined Pair Symbols:

F1_IN, F29_IN, F25_IN, U3', F53_IN, U5'

Compound Symbols:

c1, c4, c6, c7, c9, c10

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

Removed 4 trailing tuple parts

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0) → f1_out1(0)
f1_in(s(z0)) → U1(f25_in(z0), s(z0))
U1(f25_out1(z0, z1), s(z2)) → f1_out1(z1)
f29_in(0) → f29_out1(0)
f29_in(s(z0)) → U2(f53_in(z0), s(z0))
U2(f53_out1(z0, z1), s(z2)) → f29_out1(z1)
f25_in(z0) → U3(f29_in(z0), z0)
U3(f29_out1(z0), z1) → U4(f1_in(z0), z1, z0)
U4(f1_out1(z0), z1, z2) → f25_out1(z2, z0)
f53_in(z0) → U5(f29_in(z0), z0)
U5(f29_out1(z0), z1) → U6(f29_in(z0), z1, z0)
U6(f29_out1(z0), z1, z2) → f53_out1(z2, z0)

Tuples:

F25_IN(z0) → c6(U3'(f29_in(z0), z0), F29_IN(z0))
F53_IN(z0) → c9(U5'(f29_in(z0), z0), F29_IN(z0))
F1_IN(s(z0)) → c1(F25_IN(z0))
F29_IN(s(z0)) → c4(F53_IN(z0))
U3'(f29_out1(z0), z1) → c7(F1_IN(z0))
U5'(f29_out1(z0), z1) → c10(F29_IN(z0))

S tuples:

F25_IN(z0) → c6(U3'(f29_in(z0), z0), F29_IN(z0))
F53_IN(z0) → c9(U5'(f29_in(z0), z0), F29_IN(z0))
F1_IN(s(z0)) → c1(F25_IN(z0))
F29_IN(s(z0)) → c4(F53_IN(z0))
U3'(f29_out1(z0), z1) → c7(F1_IN(z0))
U5'(f29_out1(z0), z1) → c10(F29_IN(z0))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f29_in, U2, f25_in, U3, U4, f53_in, U5, U6

Defined Pair Symbols:

F25_IN, F53_IN, F1_IN, F29_IN, U3', U5'

Compound Symbols:

c6, c9, c1, c4, c7, c10

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

F25_IN(z0) → c6(U3'(f29_in(z0), z0), F29_IN(z0))
F53_IN(z0) → c9(U5'(f29_in(z0), z0), F29_IN(z0))
F1_IN(s(z0)) → c1(F25_IN(z0))
F29_IN(s(z0)) → c4(F53_IN(z0))

We considered the (Usable) Rules:

f29_in(0) → f29_out1(0)
f29_in(s(z0)) → U2(f53_in(z0), s(z0))
f53_in(z0) → U5(f29_in(z0), z0)
U2(f53_out1(z0, z1), s(z2)) → f29_out1(z1)
U5(f29_out1(z0), z1) → U6(f29_in(z0), z1, z0)
U6(f29_out1(z0), z1, z2) → f53_out1(z2, z0)

And the Tuples:

F25_IN(z0) → c6(U3'(f29_in(z0), z0), F29_IN(z0))
F53_IN(z0) → c9(U5'(f29_in(z0), z0), F29_IN(z0))
F1_IN(s(z0)) → c1(F25_IN(z0))
F29_IN(s(z0)) → c4(F53_IN(z0))
U3'(f29_out1(z0), z1) → c7(F1_IN(z0))
U5'(f29_out1(z0), z1) → c10(F29_IN(z0))

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

POL(0) = 0   
POL(F1_IN(x₁)) = [2]x₁   
POL(F25_IN(x₁)) = [1] + [2]x₁   
POL(F29_IN(x₁)) = x₁   
POL(F53_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(f29_in(x₁)) = 0   
POL(f29_out1(x₁)) = x₁   
POL(f53_in(x₁)) = 0   
POL(f53_out1(x₁, x₂)) = x₂   
POL(s(x₁)) = [2] + x₁   

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0) → f1_out1(0)
f1_in(s(z0)) → U1(f25_in(z0), s(z0))
U1(f25_out1(z0, z1), s(z2)) → f1_out1(z1)
f29_in(0) → f29_out1(0)
f29_in(s(z0)) → U2(f53_in(z0), s(z0))
U2(f53_out1(z0, z1), s(z2)) → f29_out1(z1)
f25_in(z0) → U3(f29_in(z0), z0)
U3(f29_out1(z0), z1) → U4(f1_in(z0), z1, z0)
U4(f1_out1(z0), z1, z2) → f25_out1(z2, z0)
f53_in(z0) → U5(f29_in(z0), z0)
U5(f29_out1(z0), z1) → U6(f29_in(z0), z1, z0)
U6(f29_out1(z0), z1, z2) → f53_out1(z2, z0)

Tuples:

F25_IN(z0) → c6(U3'(f29_in(z0), z0), F29_IN(z0))
F53_IN(z0) → c9(U5'(f29_in(z0), z0), F29_IN(z0))
F1_IN(s(z0)) → c1(F25_IN(z0))
F29_IN(s(z0)) → c4(F53_IN(z0))
U3'(f29_out1(z0), z1) → c7(F1_IN(z0))
U5'(f29_out1(z0), z1) → c10(F29_IN(z0))

S tuples:

U3'(f29_out1(z0), z1) → c7(F1_IN(z0))
U5'(f29_out1(z0), z1) → c10(F29_IN(z0))

K tuples:

F25_IN(z0) → c6(U3'(f29_in(z0), z0), F29_IN(z0))
F53_IN(z0) → c9(U5'(f29_in(z0), z0), F29_IN(z0))
F1_IN(s(z0)) → c1(F25_IN(z0))
F29_IN(s(z0)) → c4(F53_IN(z0))

Defined Rule Symbols:

f1_in, U1, f29_in, U2, f25_in, U3, U4, f53_in, U5, U6

Defined Pair Symbols:

F25_IN, F53_IN, F1_IN, F29_IN, U3', U5'

Compound Symbols:

c6, c9, c1, c4, c7, c10