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

(0) Obligation:

Clauses:

h(X) :- ','(f(X), g(X)).
f(c(0, X1)) :- !.
f(c(X, Y)) :- ','(p(X, P), f(c(P, s(Y)))).
g(c(X2, 0)) :- !.
g(c(X, Y)) :- ','(p(Y, P), g(c(s(X), P))).
p(0, 0).
p(s(X), X).

Query: h(g)

(1) 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: h(T1)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
3 [label="3: h(T1), SCOPE: 1, CLAUSE: 0\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: ','(f(T5), g(T5))\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: f(T5)\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: g(T5)\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: f(T5), SCOPE: 2, CLAUSE: 1 | f(T5), SCOPE: 2, CLAUSE: 2\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: !_2 | f(c(0, T10)), SCOPE: 2, CLAUSE: 2\n\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: f(T5), SCOPE: 2, CLAUSE: 2\n\nT5 is ground\nX11 is free\nf(T5) !=? f(c(0, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ','(p(T15, X19), f(c(X19, s(T16))))\n\nT15 is ground\nT16 is ground\nX11 is free\nX19 is free\nf(c(T15, T16)) !=? f(c(0, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: ','(p(T15, X19), f(c(X19, s(T16)))), SCOPE: 3, CLAUSE: 5 | ','(p(T15, X19), f(c(X19, s(T16)))), SCOPE: 3, CLAUSE: 6\n\nT15 is ground\nT16 is ground\nX11 is free\nX19 is free\nf(c(T15, T16)) !=? f(c(0, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: ','(p(T15, X19), f(c(X19, s(T16)))), SCOPE: 3, CLAUSE: 6\n\nT15 is ground\nT16 is ground\nX11 is free\nX19 is free\nf(c(T15, T16)) !=? f(c(0, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: f(c(T20, s(T16)))\n\nT16 is ground\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: g(T5), SCOPE: 4, CLAUSE: 3 | g(T5), SCOPE: 4, CLAUSE: 4\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: !_4 | g(c(T25, 0)), SCOPE: 4, CLAUSE: 4\n\nT25 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: g(T5), SCOPE: 4, CLAUSE: 4\n\nT5 is ground\nX28 is free\ng(T5) !=? g(c(X28, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ','(p(T31, X36), g(c(s(T30), X36)))\n\nT30 is ground\nT31 is ground\nX28 is free\nX36 is free\ng(c(T30, T31)) !=? g(c(X28, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: ','(p(T31, X36), g(c(s(T30), X36))), SCOPE: 5, CLAUSE: 5 | ','(p(T31, X36), g(c(s(T30), X36))), SCOPE: 5, CLAUSE: 6\n\nT30 is ground\nT31 is ground\nX28 is free\nX36 is free\ng(c(T30, T31)) !=? g(c(X28, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: ','(p(T31, X36), g(c(s(T30), X36))), SCOPE: 5, CLAUSE: 6\n\nT30 is ground\nT31 is ground\nX28 is free\nX36 is free\ng(c(T30, T31)) !=? g(c(X28, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: g(c(s(T30), T35))\n\nT30 is ground\nT35 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 60 [arrowhead = none ];
60 -> 3;

61 [label="ONLY EVAL with clause\nh(X6) :- ','(f(X6), g(X6)).\nand substitutionT1 -> T5,\nX6 -> T5", fontsize=14, style = filled, fillcolor = lightblue];
3 -> 61 [arrowhead = none ];
61 -> 7;

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

63 [label="SPLIT 2\nnew knowledge:\nT5 is ground", fontsize=14, style = filled, fillcolor = violet];
7 -> 63 [arrowhead = none ];
63 -> 13;

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

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

66 [label="EVAL with clause\nf(c(0, X11)) :- !_2.\nand substitutionX11 -> T10,\nT5 -> c(0, T10)", fontsize=14, style = filled, fillcolor = lightblue];
18 -> 66 [arrowhead = none ];
66 -> 19;

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

68 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
19 -> 68 [arrowhead = none ];
68 -> 22;

69 [label="EVAL with clause\nf(c(X17, X18)) :- ','(p(X17, X19), f(c(X19, s(X18)))).\nand substitutionX17 -> T15,\nX18 -> T16,\nT5 -> c(T15, T16)", fontsize=14, style = filled, fillcolor = lightblue];
21 -> 69 [arrowhead = none ];
69 -> 26;

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

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

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

73 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (f(c(T15, T16)), f(c(0, X11)))", fontsize=14, style = filled, fillcolor = lightgreen];
30 -> 73 [arrowhead = none ];
73 -> 31;

74 [label="EVAL with clause\np(s(X23), X23).\nand substitutionX23 -> T20,\nT15 -> s(T20),\nX19 -> T20", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 74 [arrowhead = none ];
74 -> 33;

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

76 [label="INSTANCE with matching:\nT5 -> c(T20, s(T16))", fontsize=14, style = filled, fillcolor = lightgrey];
33 -> 76 [arrowhead = none , style=dashed];
76 -> 12[style=dashed];

77 [label="EVAL with clause\ng(c(X28, 0)) :- !_4.\nand substitutionX28 -> T25,\nT5 -> c(T25, 0)", fontsize=14, style = filled, fillcolor = lightblue];
39 -> 77 [arrowhead = none ];
77 -> 41;

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

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

80 [label="EVAL with clause\ng(c(X34, X35)) :- ','(p(X35, X36), g(c(s(X34), X36))).\nand substitutionX34 -> T30,\nX35 -> T31,\nT5 -> c(T30, T31)", fontsize=14, style = filled, fillcolor = lightblue];
42 -> 80 [arrowhead = none ];
80 -> 49;

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

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

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

84 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (g(c(T30, T31)), g(c(X28, 0)))", fontsize=14, style = filled, fillcolor = lightgreen];
52 -> 84 [arrowhead = none ];
84 -> 53;

85 [label="EVAL with clause\np(s(X40), X40).\nand substitutionX40 -> T35,\nT31 -> s(T35),\nX36 -> T35", fontsize=14, style = filled, fillcolor = lightblue];
53 -> 85 [arrowhead = none ];
85 -> 58;

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

87 [label="INSTANCE with matching:\nT5 -> c(s(T30), T35)", fontsize=14, style = filled, fillcolor = lightgrey];
58 -> 87 [arrowhead = none , style=dashed];
87 -> 13[style=dashed];

}

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0) → U1(f7_in(z0), z0)
U1(f7_out1, z0) → f1_out1
f12_in(c(0, z0)) → f12_out1
f12_in(c(s(z0), z1)) → U2(f12_in(c(z0, s(z1))), c(s(z0), z1))
U2(f12_out1, c(s(z0), z1)) → f12_out1
f13_in(c(z0, 0)) → f13_out1
f13_in(c(z0, s(z1))) → U3(f13_in(c(s(z0), z1)), c(z0, s(z1)))
U3(f13_out1, c(z0, s(z1))) → f13_out1
f7_in(z0) → U4(f12_in(z0), z0)
U4(f12_out1, z0) → U5(f13_in(z0), z0)
U5(f13_out1, z0) → f7_out1

Tuples:

F1_IN(z0) → c1(U1'(f7_in(z0), z0), F7_IN(z0))
F12_IN(c(s(z0), z1)) → c4(U2'(f12_in(c(z0, s(z1))), c(s(z0), z1)), F12_IN(c(z0, s(z1))))
F13_IN(c(z0, s(z1))) → c7(U3'(f13_in(c(s(z0), z1)), c(z0, s(z1))), F13_IN(c(s(z0), z1)))
F7_IN(z0) → c9(U4'(f12_in(z0), z0), F12_IN(z0))
U4'(f12_out1, z0) → c10(U5'(f13_in(z0), z0), F13_IN(z0))

S tuples:

F1_IN(z0) → c1(U1'(f7_in(z0), z0), F7_IN(z0))
F12_IN(c(s(z0), z1)) → c4(U2'(f12_in(c(z0, s(z1))), c(s(z0), z1)), F12_IN(c(z0, s(z1))))
F13_IN(c(z0, s(z1))) → c7(U3'(f13_in(c(s(z0), z1)), c(z0, s(z1))), F13_IN(c(s(z0), z1)))
F7_IN(z0) → c9(U4'(f12_in(z0), z0), F12_IN(z0))
U4'(f12_out1, z0) → c10(U5'(f13_in(z0), z0), F13_IN(z0))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f12_in, U2, f13_in, U3, f7_in, U4, U5

Defined Pair Symbols:

F1_IN, F12_IN, F13_IN, F7_IN, U4'

Compound Symbols:

c1, c4, c7, c9, c10

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

Split RHS of tuples not part of any SCC

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0) → U1(f7_in(z0), z0)
U1(f7_out1, z0) → f1_out1
f12_in(c(0, z0)) → f12_out1
f12_in(c(s(z0), z1)) → U2(f12_in(c(z0, s(z1))), c(s(z0), z1))
U2(f12_out1, c(s(z0), z1)) → f12_out1
f13_in(c(z0, 0)) → f13_out1
f13_in(c(z0, s(z1))) → U3(f13_in(c(s(z0), z1)), c(z0, s(z1)))
U3(f13_out1, c(z0, s(z1))) → f13_out1
f7_in(z0) → U4(f12_in(z0), z0)
U4(f12_out1, z0) → U5(f13_in(z0), z0)
U5(f13_out1, z0) → f7_out1

Tuples:

F12_IN(c(s(z0), z1)) → c4(U2'(f12_in(c(z0, s(z1))), c(s(z0), z1)), F12_IN(c(z0, s(z1))))
F13_IN(c(z0, s(z1))) → c7(U3'(f13_in(c(s(z0), z1)), c(z0, s(z1))), F13_IN(c(s(z0), z1)))
F1_IN(z0) → c2(U1'(f7_in(z0), z0))
F1_IN(z0) → c2(F7_IN(z0))
F7_IN(z0) → c2(U4'(f12_in(z0), z0))
F7_IN(z0) → c2(F12_IN(z0))
U4'(f12_out1, z0) → c2(U5'(f13_in(z0), z0))
U4'(f12_out1, z0) → c2(F13_IN(z0))

S tuples:

F12_IN(c(s(z0), z1)) → c4(U2'(f12_in(c(z0, s(z1))), c(s(z0), z1)), F12_IN(c(z0, s(z1))))
F13_IN(c(z0, s(z1))) → c7(U3'(f13_in(c(s(z0), z1)), c(z0, s(z1))), F13_IN(c(s(z0), z1)))
F1_IN(z0) → c2(U1'(f7_in(z0), z0))
F1_IN(z0) → c2(F7_IN(z0))
F7_IN(z0) → c2(U4'(f12_in(z0), z0))
F7_IN(z0) → c2(F12_IN(z0))
U4'(f12_out1, z0) → c2(U5'(f13_in(z0), z0))
U4'(f12_out1, z0) → c2(F13_IN(z0))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f12_in, U2, f13_in, U3, f7_in, U4, U5

Defined Pair Symbols:

F12_IN, F13_IN, F1_IN, F7_IN, U4'

Compound Symbols:

c4, c7, c2

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

Removed 4 trailing tuple parts

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0) → U1(f7_in(z0), z0)
U1(f7_out1, z0) → f1_out1
f12_in(c(0, z0)) → f12_out1
f12_in(c(s(z0), z1)) → U2(f12_in(c(z0, s(z1))), c(s(z0), z1))
U2(f12_out1, c(s(z0), z1)) → f12_out1
f13_in(c(z0, 0)) → f13_out1
f13_in(c(z0, s(z1))) → U3(f13_in(c(s(z0), z1)), c(z0, s(z1)))
U3(f13_out1, c(z0, s(z1))) → f13_out1
f7_in(z0) → U4(f12_in(z0), z0)
U4(f12_out1, z0) → U5(f13_in(z0), z0)
U5(f13_out1, z0) → f7_out1

Tuples:

F1_IN(z0) → c2(F7_IN(z0))
F7_IN(z0) → c2(U4'(f12_in(z0), z0))
F7_IN(z0) → c2(F12_IN(z0))
U4'(f12_out1, z0) → c2(F13_IN(z0))
F12_IN(c(s(z0), z1)) → c4(F12_IN(c(z0, s(z1))))
F13_IN(c(z0, s(z1))) → c7(F13_IN(c(s(z0), z1)))
F1_IN(z0) → c2
U4'(f12_out1, z0) → c2

S tuples:

F1_IN(z0) → c2(F7_IN(z0))
F7_IN(z0) → c2(U4'(f12_in(z0), z0))
F7_IN(z0) → c2(F12_IN(z0))
U4'(f12_out1, z0) → c2(F13_IN(z0))
F12_IN(c(s(z0), z1)) → c4(F12_IN(c(z0, s(z1))))
F13_IN(c(z0, s(z1))) → c7(F13_IN(c(s(z0), z1)))
F1_IN(z0) → c2
U4'(f12_out1, z0) → c2

K tuples:none
Defined Rule Symbols:

f1_in, U1, f12_in, U2, f13_in, U3, f7_in, U4, U5

Defined Pair Symbols:

F1_IN, F7_IN, U4', F12_IN, F13_IN

Compound Symbols:

c2, c4, c7, c2

(7) CdtKnowledgeProof (EQUIVALENT transformation)

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

F1_IN(z0) → c2(F7_IN(z0))
F7_IN(z0) → c2(U4'(f12_in(z0), z0))
F7_IN(z0) → c2(F12_IN(z0))
U4'(f12_out1, z0) → c2(F13_IN(z0))
F1_IN(z0) → c2
U4'(f12_out1, z0) → c2
F7_IN(z0) → c2(U4'(f12_in(z0), z0))
F7_IN(z0) → c2(F12_IN(z0))
U4'(f12_out1, z0) → c2(F13_IN(z0))
U4'(f12_out1, z0) → c2

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0) → U1(f7_in(z0), z0)
U1(f7_out1, z0) → f1_out1
f12_in(c(0, z0)) → f12_out1
f12_in(c(s(z0), z1)) → U2(f12_in(c(z0, s(z1))), c(s(z0), z1))
U2(f12_out1, c(s(z0), z1)) → f12_out1
f13_in(c(z0, 0)) → f13_out1
f13_in(c(z0, s(z1))) → U3(f13_in(c(s(z0), z1)), c(z0, s(z1)))
U3(f13_out1, c(z0, s(z1))) → f13_out1
f7_in(z0) → U4(f12_in(z0), z0)
U4(f12_out1, z0) → U5(f13_in(z0), z0)
U5(f13_out1, z0) → f7_out1

Tuples:

F1_IN(z0) → c2(F7_IN(z0))
F7_IN(z0) → c2(U4'(f12_in(z0), z0))
F7_IN(z0) → c2(F12_IN(z0))
U4'(f12_out1, z0) → c2(F13_IN(z0))
F12_IN(c(s(z0), z1)) → c4(F12_IN(c(z0, s(z1))))
F13_IN(c(z0, s(z1))) → c7(F13_IN(c(s(z0), z1)))
F1_IN(z0) → c2
U4'(f12_out1, z0) → c2

S tuples:

F12_IN(c(s(z0), z1)) → c4(F12_IN(c(z0, s(z1))))
F13_IN(c(z0, s(z1))) → c7(F13_IN(c(s(z0), z1)))

K tuples:

F1_IN(z0) → c2(F7_IN(z0))
F7_IN(z0) → c2(U4'(f12_in(z0), z0))
F7_IN(z0) → c2(F12_IN(z0))
U4'(f12_out1, z0) → c2(F13_IN(z0))
F1_IN(z0) → c2
U4'(f12_out1, z0) → c2

Defined Rule Symbols:

f1_in, U1, f12_in, U2, f13_in, U3, f7_in, U4, U5

Defined Pair Symbols:

F1_IN, F7_IN, U4', F12_IN, F13_IN

Compound Symbols:

c2, c4, c7, c2

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

F13_IN(c(z0, s(z1))) → c7(F13_IN(c(s(z0), z1)))

We considered the (Usable) Rules:

f12_in(c(0, z0)) → f12_out1
f12_in(c(s(z0), z1)) → U2(f12_in(c(z0, s(z1))), c(s(z0), z1))
U2(f12_out1, c(s(z0), z1)) → f12_out1

And the Tuples:

F1_IN(z0) → c2(F7_IN(z0))
F7_IN(z0) → c2(U4'(f12_in(z0), z0))
F7_IN(z0) → c2(F12_IN(z0))
U4'(f12_out1, z0) → c2(F13_IN(z0))
F12_IN(c(s(z0), z1)) → c4(F12_IN(c(z0, s(z1))))
F13_IN(c(z0, s(z1))) → c7(F13_IN(c(s(z0), z1)))
F1_IN(z0) → c2
U4'(f12_out1, z0) → c2

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

POL(0) = 0   
POL(F12_IN(x₁)) = [2]   
POL(F13_IN(x₁)) = [2] + x₁   
POL(F1_IN(x₁)) = [3] + [3]x₁   
POL(F7_IN(x₁)) = [3] + [3]x₁   
POL(U2(x₁, x₂)) = 0   
POL(U4'(x₁, x₂)) = [2] + [2]x₂   
POL(c(x₁, x₂)) = x₂   
POL(c2) = 0   
POL(c2(x₁)) = x₁   
POL(c4(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(f12_in(x₁)) = 0   
POL(f12_out1) = 0   
POL(s(x₁)) = [1] + x₁   

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0) → U1(f7_in(z0), z0)
U1(f7_out1, z0) → f1_out1
f12_in(c(0, z0)) → f12_out1
f12_in(c(s(z0), z1)) → U2(f12_in(c(z0, s(z1))), c(s(z0), z1))
U2(f12_out1, c(s(z0), z1)) → f12_out1
f13_in(c(z0, 0)) → f13_out1
f13_in(c(z0, s(z1))) → U3(f13_in(c(s(z0), z1)), c(z0, s(z1)))
U3(f13_out1, c(z0, s(z1))) → f13_out1
f7_in(z0) → U4(f12_in(z0), z0)
U4(f12_out1, z0) → U5(f13_in(z0), z0)
U5(f13_out1, z0) → f7_out1

Tuples:

F1_IN(z0) → c2(F7_IN(z0))
F7_IN(z0) → c2(U4'(f12_in(z0), z0))
F7_IN(z0) → c2(F12_IN(z0))
U4'(f12_out1, z0) → c2(F13_IN(z0))
F12_IN(c(s(z0), z1)) → c4(F12_IN(c(z0, s(z1))))
F13_IN(c(z0, s(z1))) → c7(F13_IN(c(s(z0), z1)))
F1_IN(z0) → c2
U4'(f12_out1, z0) → c2

S tuples:

F12_IN(c(s(z0), z1)) → c4(F12_IN(c(z0, s(z1))))

K tuples:

F1_IN(z0) → c2(F7_IN(z0))
F7_IN(z0) → c2(U4'(f12_in(z0), z0))
F7_IN(z0) → c2(F12_IN(z0))
U4'(f12_out1, z0) → c2(F13_IN(z0))
F1_IN(z0) → c2
U4'(f12_out1, z0) → c2
F13_IN(c(z0, s(z1))) → c7(F13_IN(c(s(z0), z1)))

Defined Rule Symbols:

f1_in, U1, f12_in, U2, f13_in, U3, f7_in, U4, U5

Defined Pair Symbols:

F1_IN, F7_IN, U4', F12_IN, F13_IN

Compound Symbols:

c2, c4, c7, c2

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

F12_IN(c(s(z0), z1)) → c4(F12_IN(c(z0, s(z1))))

We considered the (Usable) Rules:

f12_in(c(0, z0)) → f12_out1
f12_in(c(s(z0), z1)) → U2(f12_in(c(z0, s(z1))), c(s(z0), z1))
U2(f12_out1, c(s(z0), z1)) → f12_out1

And the Tuples:

F1_IN(z0) → c2(F7_IN(z0))
F7_IN(z0) → c2(U4'(f12_in(z0), z0))
F7_IN(z0) → c2(F12_IN(z0))
U4'(f12_out1, z0) → c2(F13_IN(z0))
F12_IN(c(s(z0), z1)) → c4(F12_IN(c(z0, s(z1))))
F13_IN(c(z0, s(z1))) → c7(F13_IN(c(s(z0), z1)))
F1_IN(z0) → c2
U4'(f12_out1, z0) → c2

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

POL(0) = 0   
POL(F12_IN(x₁)) = [1] + x₁   
POL(F13_IN(x₁)) = 0   
POL(F1_IN(x₁)) = [1] + [2]x₁   
POL(F7_IN(x₁)) = [1] + [2]x₁   
POL(U2(x₁, x₂)) = 0   
POL(U4'(x₁, x₂)) = 0   
POL(c(x₁, x₂)) = x₁   
POL(c2) = 0   
POL(c2(x₁)) = x₁   
POL(c4(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(f12_in(x₁)) = 0   
POL(f12_out1) = 0   
POL(s(x₁)) = [1] + x₁   

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0) → U1(f7_in(z0), z0)
U1(f7_out1, z0) → f1_out1
f12_in(c(0, z0)) → f12_out1
f12_in(c(s(z0), z1)) → U2(f12_in(c(z0, s(z1))), c(s(z0), z1))
U2(f12_out1, c(s(z0), z1)) → f12_out1
f13_in(c(z0, 0)) → f13_out1
f13_in(c(z0, s(z1))) → U3(f13_in(c(s(z0), z1)), c(z0, s(z1)))
U3(f13_out1, c(z0, s(z1))) → f13_out1
f7_in(z0) → U4(f12_in(z0), z0)
U4(f12_out1, z0) → U5(f13_in(z0), z0)
U5(f13_out1, z0) → f7_out1

Tuples:

F1_IN(z0) → c2(F7_IN(z0))
F7_IN(z0) → c2(U4'(f12_in(z0), z0))
F7_IN(z0) → c2(F12_IN(z0))
U4'(f12_out1, z0) → c2(F13_IN(z0))
F12_IN(c(s(z0), z1)) → c4(F12_IN(c(z0, s(z1))))
F13_IN(c(z0, s(z1))) → c7(F13_IN(c(s(z0), z1)))
F1_IN(z0) → c2
U4'(f12_out1, z0) → c2

S tuples:none
K tuples:

F1_IN(z0) → c2(F7_IN(z0))
F7_IN(z0) → c2(U4'(f12_in(z0), z0))
F7_IN(z0) → c2(F12_IN(z0))
U4'(f12_out1, z0) → c2(F13_IN(z0))
F1_IN(z0) → c2
U4'(f12_out1, z0) → c2
F13_IN(c(z0, s(z1))) → c7(F13_IN(c(s(z0), z1)))
F12_IN(c(s(z0), z1)) → c4(F12_IN(c(z0, s(z1))))

Defined Rule Symbols:

f1_in, U1, f12_in, U2, f13_in, U3, f7_in, U4, U5

Defined Pair Symbols:

F1_IN, F7_IN, U4', F12_IN, F13_IN

Compound Symbols:

c2, c4, c7, c2

(13) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(14) BOUNDS(O(1), O(1))

(15) 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: h(T1)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: h(T1), SCOPE: 1, CLAUSE: 0\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: ','(f(T3), g(T3))\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: ','(f(T3), g(T3)), SCOPE: 2, CLAUSE: 1 | ','(f(T3), g(T3)), SCOPE: 2, CLAUSE: 2\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: ','(!_2, g(c(0, T6))) | ','(f(c(0, T6)), g(c(0, T6))), SCOPE: 2, CLAUSE: 2\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: ','(f(T3), g(T3)), SCOPE: 2, CLAUSE: 2\n\nT3 is ground\nX7 is free\nf(T3) !=? f(c(0, X7))", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: g(c(0, T6))\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: g(c(0, T6)), SCOPE: 3, CLAUSE: 3 | g(c(0, T6)), SCOPE: 3, CLAUSE: 4\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: !_3 | g(c(0, 0)), SCOPE: 3, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: g(c(0, T6)), SCOPE: 3, CLAUSE: 4\n\nT6 is ground\nX11 is free\ng(c(0, T6)) !=? g(c(X11, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ','(p(T9, X20), g(c(s(0), X20)))\n\nT9 is ground\nX11 is free\nX20 is free\ng(c(0, T9)) !=? g(c(X11, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: ','(p(T9, X20), g(c(s(0), X20))), SCOPE: 4, CLAUSE: 5 | ','(p(T9, X20), g(c(s(0), X20))), SCOPE: 4, CLAUSE: 6\n\nT9 is ground\nX11 is free\nX20 is free\ng(c(0, T9)) !=? g(c(X11, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: ','(p(T9, X20), g(c(s(0), X20))), SCOPE: 4, CLAUSE: 6\n\nT9 is ground\nX11 is free\nX20 is free\ng(c(0, T9)) !=? g(c(X11, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: g(c(s(0), T12))\n\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: g(c(s(0), T12)), SCOPE: 5, CLAUSE: 3 | g(c(s(0), T12)), SCOPE: 5, CLAUSE: 4\n\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: !_5 | g(c(s(0), 0)), SCOPE: 5, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: g(c(s(0), T12)), SCOPE: 5, CLAUSE: 4\n\nT12 is ground\nX28 is free\ng(c(s(0), T12)) !=? g(c(X28, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: ','(p(T15, X37), g(c(s(s(0)), X37)))\n\nT15 is ground\nX28 is free\nX37 is free\ng(c(s(0), T15)) !=? g(c(X28, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: ','(p(T15, X37), g(c(s(s(0)), X37))), SCOPE: 6, CLAUSE: 5 | ','(p(T15, X37), g(c(s(s(0)), X37))), SCOPE: 6, CLAUSE: 6\n\nT15 is ground\nX28 is free\nX37 is free\ng(c(s(0), T15)) !=? g(c(X28, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: ','(p(T15, X37), g(c(s(s(0)), X37))), SCOPE: 6, CLAUSE: 6\n\nT15 is ground\nX28 is free\nX37 is free\ng(c(s(0), T15)) !=? g(c(X28, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: g(c(s(s(0)), T18))\n\nT18 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: g(c(s(s(0)), T18)), SCOPE: 7, CLAUSE: 3 | g(c(s(s(0)), T18)), SCOPE: 7, CLAUSE: 4\n\nT18 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: !_7 | g(c(s(s(0)), 0)), SCOPE: 7, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: g(c(s(s(0)), T18)), SCOPE: 7, CLAUSE: 4\n\nT18 is ground\nX45 is free\ng(c(s(s(0)), T18)) !=? g(c(X45, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: ','(p(T21, X54), g(c(s(s(s(0))), X54)))\n\nT21 is ground\nX45 is free\nX54 is free\ng(c(s(s(0)), T21)) !=? g(c(X45, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: ','(p(T21, X54), g(c(s(s(s(0))), X54))), SCOPE: 8, CLAUSE: 5 | ','(p(T21, X54), g(c(s(s(s(0))), X54))), SCOPE: 8, CLAUSE: 6\n\nT21 is ground\nX45 is free\nX54 is free\ng(c(s(s(0)), T21)) !=? g(c(X45, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: ','(p(T21, X54), g(c(s(s(s(0))), X54))), SCOPE: 8, CLAUSE: 6\n\nT21 is ground\nX45 is free\nX54 is free\ng(c(s(s(0)), T21)) !=? g(c(X45, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: g(c(s(s(s(0))), T24))\n\nT24 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: g(c(s(s(s(0))), T24)), SCOPE: 9, CLAUSE: 3 | g(c(s(s(s(0))), T24)), SCOPE: 9, CLAUSE: 4\n\nT24 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: !_9 | g(c(s(s(s(0))), 0)), SCOPE: 9, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: g(c(s(s(s(0))), T24)), SCOPE: 9, CLAUSE: 4\n\nT24 is ground\nX62 is free\ng(c(s(s(s(0))), T24)) !=? g(c(X62, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: ','(p(T27, X71), g(c(s(s(s(s(0)))), X71)))\n\nT27 is ground\nX62 is free\nX71 is free\ng(c(s(s(s(0))), T27)) !=? g(c(X62, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: ','(p(T27, X71), g(c(s(s(s(s(0)))), X71))), SCOPE: 10, CLAUSE: 5 | ','(p(T27, X71), g(c(s(s(s(s(0)))), X71))), SCOPE: 10, CLAUSE: 6\n\nT27 is ground\nX62 is free\nX71 is free\ng(c(s(s(s(0))), T27)) !=? g(c(X62, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: ','(p(T27, X71), g(c(s(s(s(s(0)))), X71))), SCOPE: 10, CLAUSE: 6\n\nT27 is ground\nX62 is free\nX71 is free\ng(c(s(s(s(0))), T27)) !=? g(c(X62, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: g(c(s(s(s(s(0)))), T30))\n\nT30 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: g(c(s(s(s(s(0)))), T30)), SCOPE: 11, CLAUSE: 3 | g(c(s(s(s(s(0)))), T30)), SCOPE: 11, CLAUSE: 4\n\nT30 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: !_11 | g(c(s(s(s(s(0)))), 0)), SCOPE: 11, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: g(c(s(s(s(s(0)))), T30)), SCOPE: 11, CLAUSE: 4\n\nT30 is ground\nX79 is free\ng(c(s(s(s(s(0)))), T30)) !=? g(c(X79, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: ','(p(T33, X88), g(c(s(s(s(s(s(0))))), X88)))\n\nT33 is ground\nX79 is free\nX88 is free\ng(c(s(s(s(s(0)))), T33)) !=? g(c(X79, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: ','(p(T33, X88), g(c(s(s(s(s(s(0))))), X88))), SCOPE: 12, CLAUSE: 5 | ','(p(T33, X88), g(c(s(s(s(s(s(0))))), X88))), SCOPE: 12, CLAUSE: 6\n\nT33 is ground\nX79 is free\nX88 is free\ng(c(s(s(s(s(0)))), T33)) !=? g(c(X79, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: ','(p(T33, X88), g(c(s(s(s(s(s(0))))), X88))), SCOPE: 12, CLAUSE: 6\n\nT33 is ground\nX79 is free\nX88 is free\ng(c(s(s(s(s(0)))), T33)) !=? g(c(X79, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: g(c(s(s(s(s(s(0))))), T36))\n\nT36 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: g(c(s(s(s(s(s(0))))), T36)), SCOPE: 13, CLAUSE: 3 | g(c(s(s(s(s(s(0))))), T36)), SCOPE: 13, CLAUSE: 4\n\nT36 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: !_13 | g(c(s(s(s(s(s(0))))), 0)), SCOPE: 13, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: g(c(s(s(s(s(s(0))))), T36)), SCOPE: 13, CLAUSE: 4\n\nT36 is ground\nX96 is free\ng(c(s(s(s(s(s(0))))), T36)) !=? g(c(X96, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: ','(p(T39, X105), g(c(s(s(s(s(s(s(0)))))), X105)))\n\nT39 is ground\nX96 is free\nX105 is free\ng(c(s(s(s(s(s(0))))), T39)) !=? g(c(X96, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: ','(p(T39, X105), g(c(s(s(s(s(s(s(0)))))), X105))), SCOPE: 14, CLAUSE: 5 | ','(p(T39, X105), g(c(s(s(s(s(s(s(0)))))), X105))), SCOPE: 14, CLAUSE: 6\n\nT39 is ground\nX96 is free\nX105 is free\ng(c(s(s(s(s(s(0))))), T39)) !=? g(c(X96, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: ','(p(T39, X105), g(c(s(s(s(s(s(s(0)))))), X105))), SCOPE: 14, CLAUSE: 6\n\nT39 is ground\nX96 is free\nX105 is free\ng(c(s(s(s(s(s(0))))), T39)) !=? g(c(X96, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: g(c(s(s(s(s(s(s(0)))))), T42))\n\nT42 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: g(c(s(s(s(s(s(s(0)))))), T42)), SCOPE: 15, CLAUSE: 3 | g(c(s(s(s(s(s(s(0)))))), T42)), SCOPE: 15, CLAUSE: 4\n\nT42 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: !_15 | g(c(s(s(s(s(s(s(0)))))), 0)), SCOPE: 15, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: g(c(s(s(s(s(s(s(0)))))), T42)), SCOPE: 15, CLAUSE: 4\n\nT42 is ground\nX113 is free\ng(c(s(s(s(s(s(s(0)))))), T42)) !=? g(c(X113, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: ','(p(T45, X122), g(c(s(s(s(s(s(s(s(0))))))), X122)))\n\nT45 is ground\nX113 is free\nX122 is free\ng(c(s(s(s(s(s(s(0)))))), T45)) !=? g(c(X113, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: ','(p(T45, X122), g(c(s(s(s(s(s(s(s(0))))))), X122))), SCOPE: 16, CLAUSE: 5 | ','(p(T45, X122), g(c(s(s(s(s(s(s(s(0))))))), X122))), SCOPE: 16, CLAUSE: 6\n\nT45 is ground\nX113 is free\nX122 is free\ng(c(s(s(s(s(s(s(0)))))), T45)) !=? g(c(X113, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: ','(p(T45, X122), g(c(s(s(s(s(s(s(s(0))))))), X122))), SCOPE: 16, CLAUSE: 6\n\nT45 is ground\nX113 is free\nX122 is free\ng(c(s(s(s(s(s(s(0)))))), T45)) !=? g(c(X113, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: g(c(s(s(s(s(s(s(s(0))))))), T48))\n\nT48 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: g(c(s(s(s(s(s(s(s(0))))))), T48)), SCOPE: 17, CLAUSE: 3 | g(c(s(s(s(s(s(s(s(0))))))), T48)), SCOPE: 17, CLAUSE: 4\n\nT48 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: !_17 | g(c(s(s(s(s(s(s(s(0))))))), 0)), SCOPE: 17, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: g(c(s(s(s(s(s(s(s(0))))))), T48)), SCOPE: 17, CLAUSE: 4\n\nT48 is ground\nX130 is free\ng(c(s(s(s(s(s(s(s(0))))))), T48)) !=? g(c(X130, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: ','(p(T51, X139), g(c(s(s(s(s(s(s(s(s(0)))))))), X139)))\n\nT51 is ground\nX130 is free\nX139 is free\ng(c(s(s(s(s(s(s(s(0))))))), T51)) !=? g(c(X130, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: ','(p(T51, X139), g(c(s(s(s(s(s(s(s(s(0)))))))), X139))), SCOPE: 18, CLAUSE: 5 | ','(p(T51, X139), g(c(s(s(s(s(s(s(s(s(0)))))))), X139))), SCOPE: 18, CLAUSE: 6\n\nT51 is ground\nX130 is free\nX139 is free\ng(c(s(s(s(s(s(s(s(0))))))), T51)) !=? g(c(X130, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: ','(p(T51, X139), g(c(s(s(s(s(s(s(s(s(0)))))))), X139))), SCOPE: 18, CLAUSE: 6\n\nT51 is ground\nX130 is free\nX139 is free\ng(c(s(s(s(s(s(s(s(0))))))), T51)) !=? g(c(X130, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: g(c(s(s(s(s(s(s(s(s(0)))))))), T54))\n\nT54 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: g(c(s(T55), T54))\n\nT54 is ground\nT55 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: g(c(s(T55), T54)), SCOPE: 19, CLAUSE: 3 | g(c(s(T55), T54)), SCOPE: 19, CLAUSE: 4\n\nT54 is ground\nT55 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: !_19 | g(c(s(T59), 0)), SCOPE: 19, CLAUSE: 4\n\nT59 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: g(c(s(T55), T54)), SCOPE: 19, CLAUSE: 4\n\nT54 is ground\nT55 is ground\nX148 is free\ng(c(s(T55), T54)) !=? g(c(X148, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: ','(p(T66, X157), g(c(s(s(T65)), X157)))\n\nT65 is ground\nT66 is ground\nX148 is free\nX157 is free\ng(c(s(T65), T66)) !=? g(c(X148, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: ','(p(T66, X157), g(c(s(s(T65)), X157))), SCOPE: 20, CLAUSE: 5 | ','(p(T66, X157), g(c(s(s(T65)), X157))), SCOPE: 20, CLAUSE: 6\n\nT65 is ground\nT66 is ground\nX148 is free\nX157 is free\ng(c(s(T65), T66)) !=? g(c(X148, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: ','(p(T66, X157), g(c(s(s(T65)), X157))), SCOPE: 20, CLAUSE: 6\n\nT65 is ground\nT66 is ground\nX148 is free\nX157 is free\ng(c(s(T65), T66)) !=? g(c(X148, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: g(c(s(s(T65)), T70))\n\nT65 is ground\nT70 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: ','(','(p(T76, X170), f(c(X170, s(T77)))), g(c(T76, T77)))\n\nT76 is ground\nT77 is ground\nX7 is free\nX170 is free\nf(c(T76, T77)) !=? f(c(0, X7))", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: ','(','(p(T76, X170), f(c(X170, s(T77)))), g(c(T76, T77))), SCOPE: 21, CLAUSE: 5 | ','(','(p(T76, X170), f(c(X170, s(T77)))), g(c(T76, T77))), SCOPE: 21, CLAUSE: 6\n\nT76 is ground\nT77 is ground\nX7 is free\nX170 is free\nf(c(T76, T77)) !=? f(c(0, X7))", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: ','(','(p(T76, X170), f(c(X170, s(T77)))), g(c(T76, T77))), SCOPE: 21, CLAUSE: 6\n\nT76 is ground\nT77 is ground\nX7 is free\nX170 is free\nf(c(T76, T77)) !=? f(c(0, X7))", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: ','(f(c(T81, s(T77))), g(c(s(T81), T77)))\n\nT77 is ground\nT81 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: f(c(T81, s(T77)))\n\nT77 is ground\nT81 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: g(c(s(T81), T77))\n\nT77 is ground\nT81 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: f(c(T81, s(T77))), SCOPE: 22, CLAUSE: 1 | f(c(T81, s(T77))), SCOPE: 22, CLAUSE: 2\n\nT77 is ground\nT81 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: !_22 | f(c(0, s(T86))), SCOPE: 22, CLAUSE: 2\n\nT86 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: f(c(T81, s(T77))), SCOPE: 22, CLAUSE: 2\n\nT77 is ground\nT81 is ground\nX179 is free\nf(c(T81, s(T77))) !=? f(c(0, X179))", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: ','(p(T92, X188), f(c(X188, s(s(T93)))))\n\nT92 is ground\nT93 is ground\nX179 is free\nX188 is free\nf(c(T92, s(T93))) !=? f(c(0, X179))", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: ','(p(T92, X188), f(c(X188, s(s(T93))))), SCOPE: 23, CLAUSE: 5 | ','(p(T92, X188), f(c(X188, s(s(T93))))), SCOPE: 23, CLAUSE: 6\n\nT92 is ground\nT93 is ground\nX179 is free\nX188 is free\nf(c(T92, s(T93))) !=? f(c(0, X179))", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: ','(p(T92, X188), f(c(X188, s(s(T93))))), SCOPE: 23, CLAUSE: 6\n\nT92 is ground\nT93 is ground\nX179 is free\nX188 is free\nf(c(T92, s(T93))) !=? f(c(0, X179))", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: f(c(T97, s(s(T93))))\n\nT93 is ground\nT97 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 164 [arrowhead = none ];
164 -> 4;

165 [label="ONLY EVAL with clause\nh(X4) :- ','(f(X4), g(X4)).\nand substitutionT1 -> T3,\nX4 -> T3", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 165 [arrowhead = none ];
165 -> 5;

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

167 [label="EVAL with clause\nf(c(0, X7)) :- !_2.\nand substitutionX7 -> T6,\nT3 -> c(0, T6)", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 167 [arrowhead = none ];
167 -> 8;

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

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

170 [label="EVAL with clause\nf(c(X168, X169)) :- ','(p(X168, X170), f(c(X170, s(X169)))).\nand substitutionX168 -> T76,\nX169 -> T77,\nT3 -> c(T76, T77)", fontsize=14, style = filled, fillcolor = lightblue];
9 -> 170 [arrowhead = none ];
170 -> 146;

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

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

173 [label="EVAL with clause\ng(c(X11, 0)) :- !_3.\nand substitutionX11 -> 0,\nT6 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
11 -> 173 [arrowhead = none ];
173 -> 14;

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

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

176 [label="ONLY EVAL with clause\ng(c(X18, X19)) :- ','(p(X19, X20), g(c(s(X18), X20))).\nand substitutionX18 -> 0,\nT6 -> T9,\nX19 -> T9", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 176 [arrowhead = none ];
176 -> 20;

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

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

179 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (g(c(0, T9)), g(c(X11, 0)))", fontsize=14, style = filled, fillcolor = lightgreen];
24 -> 179 [arrowhead = none ];
179 -> 25;

180 [label="EVAL with clause\np(s(X24), X24).\nand substitutionX24 -> T12,\nT9 -> s(T12),\nX20 -> T12", fontsize=14, style = filled, fillcolor = lightblue];
25 -> 180 [arrowhead = none ];
180 -> 28;

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

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

183 [label="EVAL with clause\ng(c(X28, 0)) :- !_5.\nand substitutionX28 -> s(0),\nT12 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
32 -> 183 [arrowhead = none ];
183 -> 34;

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

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

186 [label="ONLY EVAL with clause\ng(c(X35, X36)) :- ','(p(X36, X37), g(c(s(X35), X37))).\nand substitutionX35 -> s(0),\nT12 -> T15,\nX36 -> T15", fontsize=14, style = filled, fillcolor = lightblue];
36 -> 186 [arrowhead = none ];
186 -> 40;

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

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

189 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (g(c(s(0), T15)), g(c(X28, 0)))", fontsize=14, style = filled, fillcolor = lightgreen];
43 -> 189 [arrowhead = none ];
189 -> 46;

190 [label="EVAL with clause\np(s(X41), X41).\nand substitutionX41 -> T18,\nT15 -> s(T18),\nX37 -> T18", fontsize=14, style = filled, fillcolor = lightblue];
46 -> 190 [arrowhead = none ];
190 -> 47;

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

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

193 [label="EVAL with clause\ng(c(X45, 0)) :- !_7.\nand substitutionX45 -> s(s(0)),\nT18 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
51 -> 193 [arrowhead = none ];
193 -> 54;

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

195 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
54 -> 195 [arrowhead = none ];
195 -> 56;

196 [label="ONLY EVAL with clause\ng(c(X52, X53)) :- ','(p(X53, X54), g(c(s(X52), X54))).\nand substitutionX52 -> s(s(0)),\nT18 -> T21,\nX53 -> T21", fontsize=14, style = filled, fillcolor = lightblue];
55 -> 196 [arrowhead = none ];
196 -> 60;

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

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

199 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (g(c(s(s(0)), T21)), g(c(X45, 0)))", fontsize=14, style = filled, fillcolor = lightgreen];
61 -> 199 [arrowhead = none ];
199 -> 62;

200 [label="EVAL with clause\np(s(X58), X58).\nand substitutionX58 -> T24,\nT21 -> s(T24),\nX54 -> T24", fontsize=14, style = filled, fillcolor = lightblue];
62 -> 200 [arrowhead = none ];
200 -> 63;

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

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

203 [label="EVAL with clause\ng(c(X62, 0)) :- !_9.\nand substitutionX62 -> s(s(s(0))),\nT24 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
65 -> 203 [arrowhead = none ];
203 -> 66;

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

205 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
66 -> 205 [arrowhead = none ];
205 -> 68;

206 [label="ONLY EVAL with clause\ng(c(X69, X70)) :- ','(p(X70, X71), g(c(s(X69), X71))).\nand substitutionX69 -> s(s(s(0))),\nT24 -> T27,\nX70 -> T27", fontsize=14, style = filled, fillcolor = lightblue];
67 -> 206 [arrowhead = none ];
206 -> 70;

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

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

209 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (g(c(s(s(s(0))), T27)), g(c(X62, 0)))", fontsize=14, style = filled, fillcolor = lightgreen];
71 -> 209 [arrowhead = none ];
209 -> 72;

210 [label="EVAL with clause\np(s(X75), X75).\nand substitutionX75 -> T30,\nT27 -> s(T30),\nX71 -> T30", fontsize=14, style = filled, fillcolor = lightblue];
72 -> 210 [arrowhead = none ];
210 -> 73;

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

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

213 [label="EVAL with clause\ng(c(X79, 0)) :- !_11.\nand substitutionX79 -> s(s(s(s(0)))),\nT30 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
75 -> 213 [arrowhead = none ];
213 -> 76;

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

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

216 [label="ONLY EVAL with clause\ng(c(X86, X87)) :- ','(p(X87, X88), g(c(s(X86), X88))).\nand substitutionX86 -> s(s(s(s(0)))),\nT30 -> T33,\nX87 -> T33", fontsize=14, style = filled, fillcolor = lightblue];
77 -> 216 [arrowhead = none ];
216 -> 80;

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

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

219 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (g(c(s(s(s(s(0)))), T33)), g(c(X79, 0)))", fontsize=14, style = filled, fillcolor = lightgreen];
81 -> 219 [arrowhead = none ];
219 -> 82;

220 [label="EVAL with clause\np(s(X92), X92).\nand substitutionX92 -> T36,\nT33 -> s(T36),\nX88 -> T36", fontsize=14, style = filled, fillcolor = lightblue];
82 -> 220 [arrowhead = none ];
220 -> 83;

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

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

223 [label="EVAL with clause\ng(c(X96, 0)) :- !_13.\nand substitutionX96 -> s(s(s(s(s(0))))),\nT36 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
85 -> 223 [arrowhead = none ];
223 -> 86;

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

225 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
86 -> 225 [arrowhead = none ];
225 -> 93;

226 [label="ONLY EVAL with clause\ng(c(X103, X104)) :- ','(p(X104, X105), g(c(s(X103), X105))).\nand substitutionX103 -> s(s(s(s(s(0))))),\nT36 -> T39,\nX104 -> T39", fontsize=14, style = filled, fillcolor = lightblue];
91 -> 226 [arrowhead = none ];
226 -> 95;

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

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

229 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (g(c(s(s(s(s(s(0))))), T39)), g(c(X96, 0)))", fontsize=14, style = filled, fillcolor = lightgreen];
96 -> 229 [arrowhead = none ];
229 -> 97;

230 [label="EVAL with clause\np(s(X109), X109).\nand substitutionX109 -> T42,\nT39 -> s(T42),\nX105 -> T42", fontsize=14, style = filled, fillcolor = lightblue];
97 -> 230 [arrowhead = none ];
230 -> 98;

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

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

233 [label="EVAL with clause\ng(c(X113, 0)) :- !_15.\nand substitutionX113 -> s(s(s(s(s(s(0)))))),\nT42 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
100 -> 233 [arrowhead = none ];
233 -> 101;

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

235 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
101 -> 235 [arrowhead = none ];
235 -> 103;

236 [label="ONLY EVAL with clause\ng(c(X120, X121)) :- ','(p(X121, X122), g(c(s(X120), X122))).\nand substitutionX120 -> s(s(s(s(s(s(0)))))),\nT42 -> T45,\nX121 -> T45", fontsize=14, style = filled, fillcolor = lightblue];
102 -> 236 [arrowhead = none ];
236 -> 105;

237 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
103 -> 237 [arrowhead = none ];
237 -> 104;

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

239 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (g(c(s(s(s(s(s(s(0)))))), T45)), g(c(X113, 0)))", fontsize=14, style = filled, fillcolor = lightgreen];
106 -> 239 [arrowhead = none ];
239 -> 107;

240 [label="EVAL with clause\np(s(X126), X126).\nand substitutionX126 -> T48,\nT45 -> s(T48),\nX122 -> T48", fontsize=14, style = filled, fillcolor = lightblue];
107 -> 240 [arrowhead = none ];
240 -> 108;

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

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

243 [label="EVAL with clause\ng(c(X130, 0)) :- !_17.\nand substitutionX130 -> s(s(s(s(s(s(s(0))))))),\nT48 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
115 -> 243 [arrowhead = none ];
243 -> 119;

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

245 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
119 -> 245 [arrowhead = none ];
245 -> 122;

246 [label="ONLY EVAL with clause\ng(c(X137, X138)) :- ','(p(X138, X139), g(c(s(X137), X139))).\nand substitutionX137 -> s(s(s(s(s(s(s(0))))))),\nT48 -> T51,\nX138 -> T51", fontsize=14, style = filled, fillcolor = lightblue];
121 -> 246 [arrowhead = none ];
246 -> 126;

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

248 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
126 -> 248 [arrowhead = none ];
248 -> 127;

249 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (g(c(s(s(s(s(s(s(s(0))))))), T51)), g(c(X130, 0)))", fontsize=14, style = filled, fillcolor = lightgreen];
127 -> 249 [arrowhead = none ];
249 -> 129;

250 [label="EVAL with clause\np(s(X143), X143).\nand substitutionX143 -> T54,\nT51 -> s(T54),\nX139 -> T54", fontsize=14, style = filled, fillcolor = lightblue];
129 -> 250 [arrowhead = none ];
250 -> 133;

251 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
129 -> 251 [arrowhead = none ];
251 -> 134;

252 [label="GENERALIZATION\nT55 <-- s(s(s(s(s(s(s(0)))))))\n\nNew Knowledge:\nT55 is ground", fontsize=14, style = filled, fillcolor = violet];
133 -> 252 [arrowhead = none ];
252 -> 135;

253 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
135 -> 253 [arrowhead = none ];
253 -> 136;

254 [label="EVAL with clause\ng(c(X148, 0)) :- !_19.\nand substitutionT55 -> T59,\nX148 -> s(T59),\nT54 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
136 -> 254 [arrowhead = none ];
254 -> 137;

255 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
136 -> 255 [arrowhead = none ];
255 -> 138;

256 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
137 -> 256 [arrowhead = none ];
256 -> 139;

257 [label="ONLY EVAL with clause\ng(c(X155, X156)) :- ','(p(X156, X157), g(c(s(X155), X157))).\nand substitutionT55 -> T65,\nX155 -> s(T65),\nT54 -> T66,\nX156 -> T66", fontsize=14, style = filled, fillcolor = lightblue];
138 -> 257 [arrowhead = none ];
257 -> 141;

258 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
139 -> 258 [arrowhead = none ];
258 -> 140;

259 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
141 -> 259 [arrowhead = none ];
259 -> 142;

260 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (g(c(s(T65), T66)), g(c(X148, 0)))", fontsize=14, style = filled, fillcolor = lightgreen];
142 -> 260 [arrowhead = none ];
260 -> 143;

261 [label="EVAL with clause\np(s(X161), X161).\nand substitutionX161 -> T70,\nT66 -> s(T70),\nX157 -> T70", fontsize=14, style = filled, fillcolor = lightblue];
143 -> 261 [arrowhead = none ];
261 -> 144;

262 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
143 -> 262 [arrowhead = none ];
262 -> 145;

263 [label="INSTANCE with matching:\nT55 -> s(T65)\nT54 -> T70", fontsize=14, style = filled, fillcolor = lightgrey];
144 -> 263 [arrowhead = none , style=dashed];
263 -> 135[style=dashed];

264 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
146 -> 264 [arrowhead = none ];
264 -> 148;

265 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (f(c(T76, T77)), f(c(0, X7)))", fontsize=14, style = filled, fillcolor = lightgreen];
148 -> 265 [arrowhead = none ];
265 -> 149;

266 [label="EVAL with clause\np(s(X174), X174).\nand substitutionX174 -> T81,\nT76 -> s(T81),\nX170 -> T81", fontsize=14, style = filled, fillcolor = lightblue];
149 -> 266 [arrowhead = none ];
266 -> 150;

267 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
149 -> 267 [arrowhead = none ];
267 -> 151;

268 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
150 -> 268 [arrowhead = none ];
268 -> 152;

269 [label="SPLIT 2\nnew knowledge:\nT81 is ground\nT77 is ground", fontsize=14, style = filled, fillcolor = violet];
150 -> 269 [arrowhead = none ];
269 -> 153;

270 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
152 -> 270 [arrowhead = none ];
270 -> 154;

271 [label="INSTANCE with matching:\nT55 -> T81\nT54 -> T77", fontsize=14, style = filled, fillcolor = lightgrey];
153 -> 271 [arrowhead = none , style=dashed];
271 -> 135[style=dashed];

272 [label="EVAL with clause\nf(c(0, X179)) :- !_22.\nand substitutionT81 -> 0,\nT77 -> T86,\nX179 -> s(T86)", fontsize=14, style = filled, fillcolor = lightblue];
154 -> 272 [arrowhead = none ];
272 -> 155;

273 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
154 -> 273 [arrowhead = none ];
273 -> 156;

274 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
155 -> 274 [arrowhead = none ];
274 -> 157;

275 [label="ONLY EVAL with clause\nf(c(X186, X187)) :- ','(p(X186, X188), f(c(X188, s(X187)))).\nand substitutionT81 -> T92,\nX186 -> T92,\nT77 -> T93,\nX187 -> s(T93)", fontsize=14, style = filled, fillcolor = lightblue];
156 -> 275 [arrowhead = none ];
275 -> 159;

276 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
157 -> 276 [arrowhead = none ];
276 -> 158;

277 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
159 -> 277 [arrowhead = none ];
277 -> 160;

278 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (f(c(T92, s(T93))), f(c(0, X179)))", fontsize=14, style = filled, fillcolor = lightgreen];
160 -> 278 [arrowhead = none ];
278 -> 161;

279 [label="EVAL with clause\np(s(X192), X192).\nand substitutionX192 -> T97,\nT92 -> s(T97),\nX188 -> T97", fontsize=14, style = filled, fillcolor = lightblue];
161 -> 279 [arrowhead = none ];
279 -> 162;

280 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
161 -> 280 [arrowhead = none ];
280 -> 163;

281 [label="INSTANCE with matching:\nT81 -> T97\nT77 -> s(T93)", fontsize=14, style = filled, fillcolor = lightgrey];
162 -> 281 [arrowhead = none , style=dashed];
281 -> 152[style=dashed];

}

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(c(0, 0)) → f2_out1
f2_in(c(0, s(0))) → f2_out1
f2_in(c(0, s(s(0)))) → f2_out1
f2_in(c(0, s(s(s(0))))) → f2_out1
f2_in(c(0, s(s(s(s(0)))))) → f2_out1
f2_in(c(0, s(s(s(s(s(0))))))) → f2_out1
f2_in(c(0, s(s(s(s(s(s(0)))))))) → f2_out1
f2_in(c(0, s(s(s(s(s(s(s(0))))))))) → f2_out1
f2_in(c(0, s(s(s(s(s(s(s(s(z0)))))))))) → U1(f135_in(s(s(s(s(s(s(s(0))))))), z0), c(0, s(s(s(s(s(s(s(s(z0))))))))))
f2_in(c(s(z0), z1)) → U2(f150_in(z0, z1), c(s(z0), z1))
U1(f135_out1, c(0, s(s(s(s(s(s(s(s(z0)))))))))) → f2_out1
U2(f150_out1, c(s(z0), z1)) → f2_out1
f135_in(z0, 0) → f135_out1
f135_in(z0, s(z1)) → U3(f135_in(s(z0), z1), z0, s(z1))
U3(f135_out1, z0, s(z1)) → f135_out1
f152_in(0, z0) → f152_out1
f152_in(s(z0), z1) → U4(f152_in(z0, s(z1)), s(z0), z1)
U4(f152_out1, s(z0), z1) → f152_out1
f150_in(z0, z1) → U5(f152_in(z0, z1), z0, z1)
U5(f152_out1, z0, z1) → U6(f135_in(z0, z1), z0, z1)
U6(f135_out1, z0, z1) → f150_out1

Tuples:

F2_IN(c(0, s(s(s(s(s(s(s(s(z0)))))))))) → c9(U1'(f135_in(s(s(s(s(s(s(s(0))))))), z0), c(0, s(s(s(s(s(s(s(s(z0)))))))))), F135_IN(s(s(s(s(s(s(s(0))))))), z0))
F2_IN(c(s(z0), z1)) → c10(U2'(f150_in(z0, z1), c(s(z0), z1)), F150_IN(z0, z1))
F135_IN(z0, s(z1)) → c14(U3'(f135_in(s(z0), z1), z0, s(z1)), F135_IN(s(z0), z1))
F152_IN(s(z0), z1) → c17(U4'(f152_in(z0, s(z1)), s(z0), z1), F152_IN(z0, s(z1)))
F150_IN(z0, z1) → c19(U5'(f152_in(z0, z1), z0, z1), F152_IN(z0, z1))
U5'(f152_out1, z0, z1) → c20(U6'(f135_in(z0, z1), z0, z1), F135_IN(z0, z1))

S tuples:

F2_IN(c(0, s(s(s(s(s(s(s(s(z0)))))))))) → c9(U1'(f135_in(s(s(s(s(s(s(s(0))))))), z0), c(0, s(s(s(s(s(s(s(s(z0)))))))))), F135_IN(s(s(s(s(s(s(s(0))))))), z0))
F2_IN(c(s(z0), z1)) → c10(U2'(f150_in(z0, z1), c(s(z0), z1)), F150_IN(z0, z1))
F135_IN(z0, s(z1)) → c14(U3'(f135_in(s(z0), z1), z0, s(z1)), F135_IN(s(z0), z1))
F152_IN(s(z0), z1) → c17(U4'(f152_in(z0, s(z1)), s(z0), z1), F152_IN(z0, s(z1)))
F150_IN(z0, z1) → c19(U5'(f152_in(z0, z1), z0, z1), F152_IN(z0, z1))
U5'(f152_out1, z0, z1) → c20(U6'(f135_in(z0, z1), z0, z1), F135_IN(z0, z1))

K tuples:none
Defined Rule Symbols:

f2_in, U1, U2, f135_in, U3, f152_in, U4, f150_in, U5, U6

Defined Pair Symbols:

F2_IN, F135_IN, F152_IN, F150_IN, U5'

Compound Symbols:

c9, c10, c14, c17, c19, c20

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

Split RHS of tuples not part of any SCC

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(c(0, 0)) → f2_out1
f2_in(c(0, s(0))) → f2_out1
f2_in(c(0, s(s(0)))) → f2_out1
f2_in(c(0, s(s(s(0))))) → f2_out1
f2_in(c(0, s(s(s(s(0)))))) → f2_out1
f2_in(c(0, s(s(s(s(s(0))))))) → f2_out1
f2_in(c(0, s(s(s(s(s(s(0)))))))) → f2_out1
f2_in(c(0, s(s(s(s(s(s(s(0))))))))) → f2_out1
f2_in(c(0, s(s(s(s(s(s(s(s(z0)))))))))) → U1(f135_in(s(s(s(s(s(s(s(0))))))), z0), c(0, s(s(s(s(s(s(s(s(z0))))))))))
f2_in(c(s(z0), z1)) → U2(f150_in(z0, z1), c(s(z0), z1))
U1(f135_out1, c(0, s(s(s(s(s(s(s(s(z0)))))))))) → f2_out1
U2(f150_out1, c(s(z0), z1)) → f2_out1
f135_in(z0, 0) → f135_out1
f135_in(z0, s(z1)) → U3(f135_in(s(z0), z1), z0, s(z1))
U3(f135_out1, z0, s(z1)) → f135_out1
f152_in(0, z0) → f152_out1
f152_in(s(z0), z1) → U4(f152_in(z0, s(z1)), s(z0), z1)
U4(f152_out1, s(z0), z1) → f152_out1
f150_in(z0, z1) → U5(f152_in(z0, z1), z0, z1)
U5(f152_out1, z0, z1) → U6(f135_in(z0, z1), z0, z1)
U6(f135_out1, z0, z1) → f150_out1

Tuples:

F135_IN(z0, s(z1)) → c14(U3'(f135_in(s(z0), z1), z0, s(z1)), F135_IN(s(z0), z1))
F152_IN(s(z0), z1) → c17(U4'(f152_in(z0, s(z1)), s(z0), z1), F152_IN(z0, s(z1)))
F2_IN(c(0, s(s(s(s(s(s(s(s(z0)))))))))) → c1(U1'(f135_in(s(s(s(s(s(s(s(0))))))), z0), c(0, s(s(s(s(s(s(s(s(z0)))))))))))
F2_IN(c(0, s(s(s(s(s(s(s(s(z0)))))))))) → c1(F135_IN(s(s(s(s(s(s(s(0))))))), z0))
F2_IN(c(s(z0), z1)) → c1(U2'(f150_in(z0, z1), c(s(z0), z1)))
F2_IN(c(s(z0), z1)) → c1(F150_IN(z0, z1))
F150_IN(z0, z1) → c1(U5'(f152_in(z0, z1), z0, z1))
F150_IN(z0, z1) → c1(F152_IN(z0, z1))
U5'(f152_out1, z0, z1) → c1(U6'(f135_in(z0, z1), z0, z1))
U5'(f152_out1, z0, z1) → c1(F135_IN(z0, z1))

S tuples:

F135_IN(z0, s(z1)) → c14(U3'(f135_in(s(z0), z1), z0, s(z1)), F135_IN(s(z0), z1))
F152_IN(s(z0), z1) → c17(U4'(f152_in(z0, s(z1)), s(z0), z1), F152_IN(z0, s(z1)))
F2_IN(c(0, s(s(s(s(s(s(s(s(z0)))))))))) → c1(U1'(f135_in(s(s(s(s(s(s(s(0))))))), z0), c(0, s(s(s(s(s(s(s(s(z0)))))))))))
F2_IN(c(0, s(s(s(s(s(s(s(s(z0)))))))))) → c1(F135_IN(s(s(s(s(s(s(s(0))))))), z0))
F2_IN(c(s(z0), z1)) → c1(U2'(f150_in(z0, z1), c(s(z0), z1)))
F2_IN(c(s(z0), z1)) → c1(F150_IN(z0, z1))
F150_IN(z0, z1) → c1(U5'(f152_in(z0, z1), z0, z1))
F150_IN(z0, z1) → c1(F152_IN(z0, z1))
U5'(f152_out1, z0, z1) → c1(U6'(f135_in(z0, z1), z0, z1))
U5'(f152_out1, z0, z1) → c1(F135_IN(z0, z1))

K tuples:none
Defined Rule Symbols:

f2_in, U1, U2, f135_in, U3, f152_in, U4, f150_in, U5, U6

Defined Pair Symbols:

F135_IN, F152_IN, F2_IN, F150_IN, U5'

Compound Symbols:

c14, c17, c1

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

Removed 5 trailing tuple parts

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(c(0, 0)) → f2_out1
f2_in(c(0, s(0))) → f2_out1
f2_in(c(0, s(s(0)))) → f2_out1
f2_in(c(0, s(s(s(0))))) → f2_out1
f2_in(c(0, s(s(s(s(0)))))) → f2_out1
f2_in(c(0, s(s(s(s(s(0))))))) → f2_out1
f2_in(c(0, s(s(s(s(s(s(0)))))))) → f2_out1
f2_in(c(0, s(s(s(s(s(s(s(0))))))))) → f2_out1
f2_in(c(0, s(s(s(s(s(s(s(s(z0)))))))))) → U1(f135_in(s(s(s(s(s(s(s(0))))))), z0), c(0, s(s(s(s(s(s(s(s(z0))))))))))
f2_in(c(s(z0), z1)) → U2(f150_in(z0, z1), c(s(z0), z1))
U1(f135_out1, c(0, s(s(s(s(s(s(s(s(z0)))))))))) → f2_out1
U2(f150_out1, c(s(z0), z1)) → f2_out1
f135_in(z0, 0) → f135_out1
f135_in(z0, s(z1)) → U3(f135_in(s(z0), z1), z0, s(z1))
U3(f135_out1, z0, s(z1)) → f135_out1
f152_in(0, z0) → f152_out1
f152_in(s(z0), z1) → U4(f152_in(z0, s(z1)), s(z0), z1)
U4(f152_out1, s(z0), z1) → f152_out1
f150_in(z0, z1) → U5(f152_in(z0, z1), z0, z1)
U5(f152_out1, z0, z1) → U6(f135_in(z0, z1), z0, z1)
U6(f135_out1, z0, z1) → f150_out1

Tuples:

F2_IN(c(0, s(s(s(s(s(s(s(s(z0)))))))))) → c1(F135_IN(s(s(s(s(s(s(s(0))))))), z0))
F2_IN(c(s(z0), z1)) → c1(F150_IN(z0, z1))
F150_IN(z0, z1) → c1(U5'(f152_in(z0, z1), z0, z1))
F150_IN(z0, z1) → c1(F152_IN(z0, z1))
U5'(f152_out1, z0, z1) → c1(F135_IN(z0, z1))
F135_IN(z0, s(z1)) → c14(F135_IN(s(z0), z1))
F152_IN(s(z0), z1) → c17(F152_IN(z0, s(z1)))
F2_IN(c(0, s(s(s(s(s(s(s(s(z0)))))))))) → c1
F2_IN(c(s(z0), z1)) → c1
U5'(f152_out1, z0, z1) → c1

S tuples:

F2_IN(c(0, s(s(s(s(s(s(s(s(z0)))))))))) → c1(F135_IN(s(s(s(s(s(s(s(0))))))), z0))
F2_IN(c(s(z0), z1)) → c1(F150_IN(z0, z1))
F150_IN(z0, z1) → c1(U5'(f152_in(z0, z1), z0, z1))
F150_IN(z0, z1) → c1(F152_IN(z0, z1))
U5'(f152_out1, z0, z1) → c1(F135_IN(z0, z1))
F135_IN(z0, s(z1)) → c14(F135_IN(s(z0), z1))
F152_IN(s(z0), z1) → c17(F152_IN(z0, s(z1)))
F2_IN(c(0, s(s(s(s(s(s(s(s(z0)))))))))) → c1
F2_IN(c(s(z0), z1)) → c1
U5'(f152_out1, z0, z1) → c1

K tuples:none
Defined Rule Symbols:

f2_in, U1, U2, f135_in, U3, f152_in, U4, f150_in, U5, U6

Defined Pair Symbols:

F2_IN, F150_IN, U5', F135_IN, F152_IN

Compound Symbols:

c1, c14, c17, c1

(21) CdtKnowledgeProof (EQUIVALENT transformation)

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

F2_IN(c(0, s(s(s(s(s(s(s(s(z0)))))))))) → c1(F135_IN(s(s(s(s(s(s(s(0))))))), z0))
F2_IN(c(s(z0), z1)) → c1(F150_IN(z0, z1))
F150_IN(z0, z1) → c1(U5'(f152_in(z0, z1), z0, z1))
F150_IN(z0, z1) → c1(F152_IN(z0, z1))
U5'(f152_out1, z0, z1) → c1(F135_IN(z0, z1))
F2_IN(c(0, s(s(s(s(s(s(s(s(z0)))))))))) → c1
F2_IN(c(s(z0), z1)) → c1
U5'(f152_out1, z0, z1) → c1
F150_IN(z0, z1) → c1(U5'(f152_in(z0, z1), z0, z1))
F150_IN(z0, z1) → c1(F152_IN(z0, z1))
U5'(f152_out1, z0, z1) → c1(F135_IN(z0, z1))
U5'(f152_out1, z0, z1) → c1

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(c(0, 0)) → f2_out1
f2_in(c(0, s(0))) → f2_out1
f2_in(c(0, s(s(0)))) → f2_out1
f2_in(c(0, s(s(s(0))))) → f2_out1
f2_in(c(0, s(s(s(s(0)))))) → f2_out1
f2_in(c(0, s(s(s(s(s(0))))))) → f2_out1
f2_in(c(0, s(s(s(s(s(s(0)))))))) → f2_out1
f2_in(c(0, s(s(s(s(s(s(s(0))))))))) → f2_out1
f2_in(c(0, s(s(s(s(s(s(s(s(z0)))))))))) → U1(f135_in(s(s(s(s(s(s(s(0))))))), z0), c(0, s(s(s(s(s(s(s(s(z0))))))))))
f2_in(c(s(z0), z1)) → U2(f150_in(z0, z1), c(s(z0), z1))
U1(f135_out1, c(0, s(s(s(s(s(s(s(s(z0)))))))))) → f2_out1
U2(f150_out1, c(s(z0), z1)) → f2_out1
f135_in(z0, 0) → f135_out1
f135_in(z0, s(z1)) → U3(f135_in(s(z0), z1), z0, s(z1))
U3(f135_out1, z0, s(z1)) → f135_out1
f152_in(0, z0) → f152_out1
f152_in(s(z0), z1) → U4(f152_in(z0, s(z1)), s(z0), z1)
U4(f152_out1, s(z0), z1) → f152_out1
f150_in(z0, z1) → U5(f152_in(z0, z1), z0, z1)
U5(f152_out1, z0, z1) → U6(f135_in(z0, z1), z0, z1)
U6(f135_out1, z0, z1) → f150_out1

Tuples:

F2_IN(c(0, s(s(s(s(s(s(s(s(z0)))))))))) → c1(F135_IN(s(s(s(s(s(s(s(0))))))), z0))
F2_IN(c(s(z0), z1)) → c1(F150_IN(z0, z1))
F150_IN(z0, z1) → c1(U5'(f152_in(z0, z1), z0, z1))
F150_IN(z0, z1) → c1(F152_IN(z0, z1))
U5'(f152_out1, z0, z1) → c1(F135_IN(z0, z1))
F135_IN(z0, s(z1)) → c14(F135_IN(s(z0), z1))
F152_IN(s(z0), z1) → c17(F152_IN(z0, s(z1)))
F2_IN(c(0, s(s(s(s(s(s(s(s(z0)))))))))) → c1
F2_IN(c(s(z0), z1)) → c1
U5'(f152_out1, z0, z1) → c1

S tuples:

F135_IN(z0, s(z1)) → c14(F135_IN(s(z0), z1))
F152_IN(s(z0), z1) → c17(F152_IN(z0, s(z1)))

K tuples:

F2_IN(c(0, s(s(s(s(s(s(s(s(z0)))))))))) → c1(F135_IN(s(s(s(s(s(s(s(0))))))), z0))
F2_IN(c(s(z0), z1)) → c1(F150_IN(z0, z1))
F150_IN(z0, z1) → c1(U5'(f152_in(z0, z1), z0, z1))
F150_IN(z0, z1) → c1(F152_IN(z0, z1))
U5'(f152_out1, z0, z1) → c1(F135_IN(z0, z1))
F2_IN(c(0, s(s(s(s(s(s(s(s(z0)))))))))) → c1
F2_IN(c(s(z0), z1)) → c1
U5'(f152_out1, z0, z1) → c1

Defined Rule Symbols:

f2_in, U1, U2, f135_in, U3, f152_in, U4, f150_in, U5, U6

Defined Pair Symbols:

F2_IN, F150_IN, U5', F135_IN, F152_IN

Compound Symbols:

c1, c14, c17, c1

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

F152_IN(s(z0), z1) → c17(F152_IN(z0, s(z1)))

We considered the (Usable) Rules:

f152_in(0, z0) → f152_out1
f152_in(s(z0), z1) → U4(f152_in(z0, s(z1)), s(z0), z1)
U4(f152_out1, s(z0), z1) → f152_out1

And the Tuples:

F2_IN(c(0, s(s(s(s(s(s(s(s(z0)))))))))) → c1(F135_IN(s(s(s(s(s(s(s(0))))))), z0))
F2_IN(c(s(z0), z1)) → c1(F150_IN(z0, z1))
F150_IN(z0, z1) → c1(U5'(f152_in(z0, z1), z0, z1))
F150_IN(z0, z1) → c1(F152_IN(z0, z1))
U5'(f152_out1, z0, z1) → c1(F135_IN(z0, z1))
F135_IN(z0, s(z1)) → c14(F135_IN(s(z0), z1))
F152_IN(s(z0), z1) → c17(F152_IN(z0, s(z1)))
F2_IN(c(0, s(s(s(s(s(s(s(s(z0)))))))))) → c1
F2_IN(c(s(z0), z1)) → c1
U5'(f152_out1, z0, z1) → c1

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

POL(0) = 0   
POL(F135_IN(x₁, x₂)) = 0   
POL(F150_IN(x₁, x₂)) = [1] + [2]x₁   
POL(F152_IN(x₁, x₂)) = [1] + x₁   
POL(F2_IN(x₁)) = [2]x₁   
POL(U4(x₁, x₂, x₃)) = 0   
POL(U5'(x₁, x₂, x₃)) = 0   
POL(c(x₁, x₂)) = x₁   
POL(c1) = 0   
POL(c1(x₁)) = x₁   
POL(c14(x₁)) = x₁   
POL(c17(x₁)) = x₁   
POL(f152_in(x₁, x₂)) = [3] + [2]x₁   
POL(f152_out1) = 0   
POL(s(x₁)) = [1] + x₁   

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(c(0, 0)) → f2_out1
f2_in(c(0, s(0))) → f2_out1
f2_in(c(0, s(s(0)))) → f2_out1
f2_in(c(0, s(s(s(0))))) → f2_out1
f2_in(c(0, s(s(s(s(0)))))) → f2_out1
f2_in(c(0, s(s(s(s(s(0))))))) → f2_out1
f2_in(c(0, s(s(s(s(s(s(0)))))))) → f2_out1
f2_in(c(0, s(s(s(s(s(s(s(0))))))))) → f2_out1
f2_in(c(0, s(s(s(s(s(s(s(s(z0)))))))))) → U1(f135_in(s(s(s(s(s(s(s(0))))))), z0), c(0, s(s(s(s(s(s(s(s(z0))))))))))
f2_in(c(s(z0), z1)) → U2(f150_in(z0, z1), c(s(z0), z1))
U1(f135_out1, c(0, s(s(s(s(s(s(s(s(z0)))))))))) → f2_out1
U2(f150_out1, c(s(z0), z1)) → f2_out1
f135_in(z0, 0) → f135_out1
f135_in(z0, s(z1)) → U3(f135_in(s(z0), z1), z0, s(z1))
U3(f135_out1, z0, s(z1)) → f135_out1
f152_in(0, z0) → f152_out1
f152_in(s(z0), z1) → U4(f152_in(z0, s(z1)), s(z0), z1)
U4(f152_out1, s(z0), z1) → f152_out1
f150_in(z0, z1) → U5(f152_in(z0, z1), z0, z1)
U5(f152_out1, z0, z1) → U6(f135_in(z0, z1), z0, z1)
U6(f135_out1, z0, z1) → f150_out1

Tuples:

F2_IN(c(0, s(s(s(s(s(s(s(s(z0)))))))))) → c1(F135_IN(s(s(s(s(s(s(s(0))))))), z0))
F2_IN(c(s(z0), z1)) → c1(F150_IN(z0, z1))
F150_IN(z0, z1) → c1(U5'(f152_in(z0, z1), z0, z1))
F150_IN(z0, z1) → c1(F152_IN(z0, z1))
U5'(f152_out1, z0, z1) → c1(F135_IN(z0, z1))
F135_IN(z0, s(z1)) → c14(F135_IN(s(z0), z1))
F152_IN(s(z0), z1) → c17(F152_IN(z0, s(z1)))
F2_IN(c(0, s(s(s(s(s(s(s(s(z0)))))))))) → c1
F2_IN(c(s(z0), z1)) → c1
U5'(f152_out1, z0, z1) → c1

S tuples:

F135_IN(z0, s(z1)) → c14(F135_IN(s(z0), z1))

K tuples:

F2_IN(c(0, s(s(s(s(s(s(s(s(z0)))))))))) → c1(F135_IN(s(s(s(s(s(s(s(0))))))), z0))
F2_IN(c(s(z0), z1)) → c1(F150_IN(z0, z1))
F150_IN(z0, z1) → c1(U5'(f152_in(z0, z1), z0, z1))
F150_IN(z0, z1) → c1(F152_IN(z0, z1))
U5'(f152_out1, z0, z1) → c1(F135_IN(z0, z1))
F2_IN(c(0, s(s(s(s(s(s(s(s(z0)))))))))) → c1
F2_IN(c(s(z0), z1)) → c1
U5'(f152_out1, z0, z1) → c1
F152_IN(s(z0), z1) → c17(F152_IN(z0, s(z1)))

Defined Rule Symbols:

f2_in, U1, U2, f135_in, U3, f152_in, U4, f150_in, U5, U6

Defined Pair Symbols:

F2_IN, F150_IN, U5', F135_IN, F152_IN

Compound Symbols:

c1, c14, c17, c1