Runtime Complexity proof of /tmp/tmp7h83wr/minus1.pl

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

0 Prolog

↳1 BuiltinConflictTransformerProof (BOTH BOUNDS(ID, ID), 0 ms)

↳2 Prolog

↳3 PrologToCdtProblemTransformerProof (UPPER BOUND (ID), 163 ms)

↳4 CdtProblem

    ↳5 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳6 CdtProblem

    ↳7 CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳8 CdtProblem

    ↳9 CdtKnowledgeProof (⇔, 0 ms)

    ↳10 CdtProblem

    ↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 181 ms)

    ↳12 CdtProblem

    ↳13 SIsEmptyProof (⇔, 0 ms)

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

↳15 PrologToCdtProblemTransformerProof (UPPER BOUND (ID), 159 ms)

↳16 CdtProblem

    ↳17 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳18 CdtProblem

    ↳19 CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳20 CdtProblem

    ↳21 CdtKnowledgeProof (⇔, 0 ms)

    ↳22 CdtProblem

    ↳23 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 165 ms)

    ↳24 CdtProblem

(0) Obligation:

Clauses:

m(X, 0, Z) :- ','(!, =(Z, X)).
m(0, Y, Z) :- ','(!, =(Z, 0)).
m(X, Y, Z) :- ','(p(X, A), ','(p(Y, B), m(A, B, Z))).
p(0, 0).
p(s(X), X).
q(X, Y, Z) :- m(X, Y, Z).
q(X, Y, Z).
=(X, X).

Query: q(g,g,a)

(1) BuiltinConflictTransformerProof (BOTH BOUNDS(ID, ID) transformation)

Renamed defined predicates conflicting with built-in predicates [PROLOG].

(2) Obligation:

Clauses:

m(X, 0, Z) :- ','(!, user_defined_=(Z, X)).
m(0, Y, Z) :- ','(!, user_defined_=(Z, 0)).
m(X, Y, Z) :- ','(p(X, A), ','(p(Y, B), m(A, B, Z))).
p(0, 0).
p(s(X), X).
q(X, Y, Z) :- m(X, Y, Z).
q(X, Y, Z).
user_defined_=(X, X).

Query: q(g,g,a)

(3) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)

Built complexity over-approximating cdt problems from derivation graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: q(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
3 [label="3: q(T1, T2, T3), SCOPE: 1, CLAUSE: 5 | q(T1, T2, T3), SCOPE: 1, CLAUSE: 6\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: q(T1, T2, T3), SCOPE: 1, CLAUSE: 5\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: q(T1, T2, T3), SCOPE: 1, CLAUSE: 6\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: m(T22, T23, T25)\n\nT22 is ground\nT23 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: m(T22, T23, T25), SCOPE: 2, CLAUSE: 0 | m(T22, T23, T25), SCOPE: 2, CLAUSE: 1 | m(T22, T23, T25), SCOPE: 2, CLAUSE: 2\n\nT22 is ground\nT23 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: ','(!_2, user_defined_=(T34, T32)) | m(T32, 0, T25), SCOPE: 2, CLAUSE: 1 | m(T32, 0, T25), SCOPE: 2, CLAUSE: 2\n\nT32 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: m(T22, T23, T25), SCOPE: 2, CLAUSE: 1 | m(T22, T23, T25), SCOPE: 2, CLAUSE: 2\n\nT22 is ground\nT23 is ground\nX26 is free\nX27 is free\nm(T22, T23, T25) !=? m(X26, 0, X27)", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: user_defined_=(T34, T32)\n\nT32 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: user_defined_=(T34, T32), SCOPE: 3, CLAUSE: 7\n\nT32 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: ','(!_2, user_defined_=(T44, 0)) | m(0, T42, T25), SCOPE: 2, CLAUSE: 2\n\nT42 is ground\nX26 is free\nX27 is free\nm(0, T42, T25) !=? m(X26, 0, X27)", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: m(T22, T23, T25), SCOPE: 2, CLAUSE: 2\n\nT22 is ground\nT23 is ground\nX26 is free\nX27 is free\nX35 is free\nX36 is free\nm(T22, T23, T25) !=? m(X26, 0, X27)\nm(T22, T23, T25) !=? m(0, X35, X36)", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: user_defined_=(T44, 0)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: user_defined_=(T44, 0), SCOPE: 4, CLAUSE: 7\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: ','(p(T56, X54), ','(p(T57, X55), m(X54, X55, T59)))\n\nT56 is ground\nT57 is ground\nX26 is free\nX27 is free\nX35 is free\nX36 is free\nX54 is free\nX55 is free\nm(T56, T57, T25) !=? m(X26, 0, X27)\nm(T56, T57, T25) !=? m(0, X35, X36)", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: ','(p(T56, X54), ','(p(T57, X55), m(X54, X55, T59))), SCOPE: 5, CLAUSE: 3 | ','(p(T56, X54), ','(p(T57, X55), m(X54, X55, T59))), SCOPE: 5, CLAUSE: 4\n\nT56 is ground\nT57 is ground\nX26 is free\nX27 is free\nX35 is free\nX36 is free\nX54 is free\nX55 is free\nm(T56, T57, T25) !=? m(X26, 0, X27)\nm(T56, T57, T25) !=? m(0, X35, X36)", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: ','(p(T56, X54), ','(p(T57, X55), m(X54, X55, T59))), SCOPE: 5, CLAUSE: 4\n\nT56 is ground\nT57 is ground\nX26 is free\nX27 is free\nX35 is free\nX36 is free\nX54 is free\nX55 is free\nm(T56, T57, T25) !=? m(X26, 0, X27)\nm(T56, T57, T25) !=? m(0, X35, X36)", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: ','(p(T57, X55), m(T63, X55, T59))\n\nT57 is ground\nT63 is ground\nX26 is free\nX27 is free\nX55 is free\nm(s(T63), T57, T25) !=? m(X26, 0, X27)", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: ','(p(T57, X55), m(T63, X55, T59)), SCOPE: 6, CLAUSE: 3 | ','(p(T57, X55), m(T63, X55, T59)), SCOPE: 6, CLAUSE: 4\n\nT57 is ground\nT63 is ground\nX26 is free\nX27 is free\nX55 is free\nm(s(T63), T57, T25) !=? m(X26, 0, X27)", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: ','(p(T57, X55), m(T63, X55, T59)), SCOPE: 6, CLAUSE: 4\n\nT57 is ground\nT63 is ground\nX26 is free\nX27 is free\nX55 is free\nm(s(T63), T57, T25) !=? m(X26, 0, X27)", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: m(T63, T68, T59)\n\nT63 is ground\nT68 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 74 [arrowhead = none ];
74 -> 3;

75 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
3 -> 75 [arrowhead = none ];
75 -> 6;

76 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
3 -> 76 [arrowhead = none ];
76 -> 8;

77 [label="ONLY EVAL with clause\nq(X17, X18, X19) :- m(X17, X18, X19).\nand substitutionT1 -> T22,\nX17 -> T22,\nT2 -> T23,\nX18 -> T23,\nT3 -> T25,\nX19 -> T25,\nT24 -> T25", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 77 [arrowhead = none ];
77 -> 13;

78 [label="ONLY EVAL with clause\nq(X75, X76, X77).\nand substitutionT1 -> T77,\nX75 -> T77,\nT2 -> T78,\nX76 -> T78,\nT3 -> T79,\nX77 -> T79", fontsize=14, style = filled, fillcolor = lightblue];
8 -> 78 [arrowhead = none ];
78 -> 72;

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

80 [label="EVAL with clause\nm(X26, 0, X27) :- ','(!_2, user_defined_=(X27, X26)).\nand substitutionT22 -> T32,\nX26 -> T32,\nT23 -> 0,\nT25 -> T34,\nX27 -> T34,\nT33 -> T34", fontsize=14, style = filled, fillcolor = lightblue];
21 -> 80 [arrowhead = none ];
80 -> 24;

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

82 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
24 -> 82 [arrowhead = none ];
82 -> 26;

83 [label="EVAL with clause\nm(0, X35, X36) :- ','(!_2, user_defined_=(X36, 0)).\nand substitutionT22 -> 0,\nT23 -> T42,\nX35 -> T42,\nT25 -> T44,\nX36 -> T44,\nT43 -> T44", fontsize=14, style = filled, fillcolor = lightblue];
25 -> 83 [arrowhead = none ];
83 -> 42;

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

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

86 [label="EVAL with clause\nuser_defined_=(X30, X30).\nand substitutionT34 -> T37,\nX30 -> T37,\nT32 -> T37", fontsize=14, style = filled, fillcolor = lightblue];
27 -> 86 [arrowhead = none ];
86 -> 30;

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

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

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

90 [label="ONLY EVAL with clause\nm(X51, X52, X53) :- ','(p(X51, X54), ','(p(X52, X55), m(X54, X55, X53))).\nand substitutionT22 -> T56,\nX51 -> T56,\nT23 -> T57,\nX52 -> T57,\nT25 -> T59,\nX53 -> T59,\nT58 -> T59", fontsize=14, style = filled, fillcolor = lightblue];
43 -> 90 [arrowhead = none ];
90 -> 53;

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

92 [label="EVAL with clause\nuser_defined_=(X39, X39).\nand substitutionT44 -> 0,\nX39 -> 0,\nT47 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
45 -> 92 [arrowhead = none ];
92 -> 48;

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

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

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

96 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (m(T56, T57, T25), m(0, X35, X36))", fontsize=14, style = filled, fillcolor = lightgreen];
54 -> 96 [arrowhead = none ];
96 -> 55;

97 [label="EVAL with clause\np(s(X61), X61).\nand substitutionX61 -> T63,\nT56 -> s(T63),\nX54 -> T63", fontsize=14, style = filled, fillcolor = lightblue];
55 -> 97 [arrowhead = none ];
97 -> 58;

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

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

100 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (m(s(T63), T57, T25), m(X26, 0, X27))", fontsize=14, style = filled, fillcolor = lightgreen];
61 -> 100 [arrowhead = none ];
100 -> 63;

101 [label="EVAL with clause\np(s(X66), X66).\nand substitutionX66 -> T68,\nT57 -> s(T68),\nX55 -> T68", fontsize=14, style = filled, fillcolor = lightblue];
63 -> 101 [arrowhead = none ];
101 -> 65;

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

103 [label="INSTANCE with matching:\nT22 -> T63\nT23 -> T68\nT25 -> T59", fontsize=14, style = filled, fillcolor = lightgrey];
65 -> 103 [arrowhead = none , style=dashed];
103 -> 13[style=dashed];

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

}

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f3_in(z0, z1), z0, z1)
U1(f3_out1, z0, z1) → f1_out1
U1(f3_out2, z0, z1) → f1_out1
f13_in(z0, 0) → f13_out1(z0)
f13_in(0, z0) → f13_out1(0)
f13_in(s(z0), s(z1)) → U2(f13_in(z0, z1), s(z0), s(z1))
U2(f13_out1(z0), s(z1), s(z2)) → f13_out1(z0)
f6_in(z0, z1) → U3(f13_in(z0, z1), z0, z1)
U3(f13_out1(z0), z1, z2) → f6_out1
f8_in(z0, z1) → f8_out1
f3_in(z0, z1) → U4(f6_in(z0, z1), f8_in(z0, z1), z0, z1)
U4(f6_out1, z0, z1, z2) → f3_out1
U4(z0, f8_out1, z1, z2) → f3_out2

Tuples:

F1_IN(z0, z1) → c(U1'(f3_in(z0, z1), z0, z1), F3_IN(z0, z1))
F13_IN(s(z0), s(z1)) → c5(U2'(f13_in(z0, z1), s(z0), s(z1)), F13_IN(z0, z1))
F6_IN(z0, z1) → c7(U3'(f13_in(z0, z1), z0, z1), F13_IN(z0, z1))
F3_IN(z0, z1) → c10(U4'(f6_in(z0, z1), f8_in(z0, z1), z0, z1), F6_IN(z0, z1), F8_IN(z0, z1))

S tuples:

F1_IN(z0, z1) → c(U1'(f3_in(z0, z1), z0, z1), F3_IN(z0, z1))
F13_IN(s(z0), s(z1)) → c5(U2'(f13_in(z0, z1), s(z0), s(z1)), F13_IN(z0, z1))
F6_IN(z0, z1) → c7(U3'(f13_in(z0, z1), z0, z1), F13_IN(z0, z1))
F3_IN(z0, z1) → c10(U4'(f6_in(z0, z1), f8_in(z0, z1), z0, z1), F6_IN(z0, z1), F8_IN(z0, z1))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f13_in, U2, f6_in, U3, f8_in, f3_in, U4

Defined Pair Symbols:

F1_IN, F13_IN, F6_IN, F3_IN

Compound Symbols:

c, c5, c7, c10

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

Split RHS of tuples not part of any SCC

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f3_in(z0, z1), z0, z1)
U1(f3_out1, z0, z1) → f1_out1
U1(f3_out2, z0, z1) → f1_out1
f13_in(z0, 0) → f13_out1(z0)
f13_in(0, z0) → f13_out1(0)
f13_in(s(z0), s(z1)) → U2(f13_in(z0, z1), s(z0), s(z1))
U2(f13_out1(z0), s(z1), s(z2)) → f13_out1(z0)
f6_in(z0, z1) → U3(f13_in(z0, z1), z0, z1)
U3(f13_out1(z0), z1, z2) → f6_out1
f8_in(z0, z1) → f8_out1
f3_in(z0, z1) → U4(f6_in(z0, z1), f8_in(z0, z1), z0, z1)
U4(f6_out1, z0, z1, z2) → f3_out1
U4(z0, f8_out1, z1, z2) → f3_out2

Tuples:

F13_IN(s(z0), s(z1)) → c5(U2'(f13_in(z0, z1), s(z0), s(z1)), F13_IN(z0, z1))
F1_IN(z0, z1) → c1(U1'(f3_in(z0, z1), z0, z1))
F1_IN(z0, z1) → c1(F3_IN(z0, z1))
F6_IN(z0, z1) → c1(U3'(f13_in(z0, z1), z0, z1))
F6_IN(z0, z1) → c1(F13_IN(z0, z1))
F3_IN(z0, z1) → c1(U4'(f6_in(z0, z1), f8_in(z0, z1), z0, z1))
F3_IN(z0, z1) → c1(F6_IN(z0, z1))
F3_IN(z0, z1) → c1(F8_IN(z0, z1))

S tuples:

F13_IN(s(z0), s(z1)) → c5(U2'(f13_in(z0, z1), s(z0), s(z1)), F13_IN(z0, z1))
F1_IN(z0, z1) → c1(U1'(f3_in(z0, z1), z0, z1))
F1_IN(z0, z1) → c1(F3_IN(z0, z1))
F6_IN(z0, z1) → c1(U3'(f13_in(z0, z1), z0, z1))
F6_IN(z0, z1) → c1(F13_IN(z0, z1))
F3_IN(z0, z1) → c1(U4'(f6_in(z0, z1), f8_in(z0, z1), z0, z1))
F3_IN(z0, z1) → c1(F6_IN(z0, z1))
F3_IN(z0, z1) → c1(F8_IN(z0, z1))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f13_in, U2, f6_in, U3, f8_in, f3_in, U4

Defined Pair Symbols:

F13_IN, F1_IN, F6_IN, F3_IN

Compound Symbols:

c5, c1

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

Removed 5 trailing tuple parts

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f3_in(z0, z1), z0, z1)
U1(f3_out1, z0, z1) → f1_out1
U1(f3_out2, z0, z1) → f1_out1
f13_in(z0, 0) → f13_out1(z0)
f13_in(0, z0) → f13_out1(0)
f13_in(s(z0), s(z1)) → U2(f13_in(z0, z1), s(z0), s(z1))
U2(f13_out1(z0), s(z1), s(z2)) → f13_out1(z0)
f6_in(z0, z1) → U3(f13_in(z0, z1), z0, z1)
U3(f13_out1(z0), z1, z2) → f6_out1
f8_in(z0, z1) → f8_out1
f3_in(z0, z1) → U4(f6_in(z0, z1), f8_in(z0, z1), z0, z1)
U4(f6_out1, z0, z1, z2) → f3_out1
U4(z0, f8_out1, z1, z2) → f3_out2

Tuples:

F1_IN(z0, z1) → c1(F3_IN(z0, z1))
F6_IN(z0, z1) → c1(F13_IN(z0, z1))
F3_IN(z0, z1) → c1(F6_IN(z0, z1))
F13_IN(s(z0), s(z1)) → c5(F13_IN(z0, z1))
F1_IN(z0, z1) → c1
F6_IN(z0, z1) → c1
F3_IN(z0, z1) → c1

S tuples:

F1_IN(z0, z1) → c1(F3_IN(z0, z1))
F6_IN(z0, z1) → c1(F13_IN(z0, z1))
F3_IN(z0, z1) → c1(F6_IN(z0, z1))
F13_IN(s(z0), s(z1)) → c5(F13_IN(z0, z1))
F1_IN(z0, z1) → c1
F6_IN(z0, z1) → c1
F3_IN(z0, z1) → c1

K tuples:none
Defined Rule Symbols:

f1_in, U1, f13_in, U2, f6_in, U3, f8_in, f3_in, U4

Defined Pair Symbols:

F1_IN, F6_IN, F3_IN, F13_IN

Compound Symbols:

c1, c5, c1

(9) CdtKnowledgeProof (EQUIVALENT transformation)

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

F1_IN(z0, z1) → c1(F3_IN(z0, z1))
F3_IN(z0, z1) → c1(F6_IN(z0, z1))
F1_IN(z0, z1) → c1
F6_IN(z0, z1) → c1
F3_IN(z0, z1) → c1
F3_IN(z0, z1) → c1
F3_IN(z0, z1) → c1(F6_IN(z0, z1))
F3_IN(z0, z1) → c1
F3_IN(z0, z1) → c1
F6_IN(z0, z1) → c1(F13_IN(z0, z1))
F6_IN(z0, z1) → c1

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f3_in(z0, z1), z0, z1)
U1(f3_out1, z0, z1) → f1_out1
U1(f3_out2, z0, z1) → f1_out1
f13_in(z0, 0) → f13_out1(z0)
f13_in(0, z0) → f13_out1(0)
f13_in(s(z0), s(z1)) → U2(f13_in(z0, z1), s(z0), s(z1))
U2(f13_out1(z0), s(z1), s(z2)) → f13_out1(z0)
f6_in(z0, z1) → U3(f13_in(z0, z1), z0, z1)
U3(f13_out1(z0), z1, z2) → f6_out1
f8_in(z0, z1) → f8_out1
f3_in(z0, z1) → U4(f6_in(z0, z1), f8_in(z0, z1), z0, z1)
U4(f6_out1, z0, z1, z2) → f3_out1
U4(z0, f8_out1, z1, z2) → f3_out2

Tuples:

F1_IN(z0, z1) → c1(F3_IN(z0, z1))
F6_IN(z0, z1) → c1(F13_IN(z0, z1))
F3_IN(z0, z1) → c1(F6_IN(z0, z1))
F13_IN(s(z0), s(z1)) → c5(F13_IN(z0, z1))
F1_IN(z0, z1) → c1
F6_IN(z0, z1) → c1
F3_IN(z0, z1) → c1

S tuples:

F13_IN(s(z0), s(z1)) → c5(F13_IN(z0, z1))

K tuples:

F1_IN(z0, z1) → c1(F3_IN(z0, z1))
F3_IN(z0, z1) → c1(F6_IN(z0, z1))
F1_IN(z0, z1) → c1
F6_IN(z0, z1) → c1
F3_IN(z0, z1) → c1
F6_IN(z0, z1) → c1(F13_IN(z0, z1))

Defined Rule Symbols:

f1_in, U1, f13_in, U2, f6_in, U3, f8_in, f3_in, U4

Defined Pair Symbols:

F1_IN, F6_IN, F3_IN, F13_IN

Compound Symbols:

c1, c5, c1

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

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

F13_IN(s(z0), s(z1)) → c5(F13_IN(z0, z1))

We considered the (Usable) Rules:none
And the Tuples:

F1_IN(z0, z1) → c1(F3_IN(z0, z1))
F6_IN(z0, z1) → c1(F13_IN(z0, z1))
F3_IN(z0, z1) → c1(F6_IN(z0, z1))
F13_IN(s(z0), s(z1)) → c5(F13_IN(z0, z1))
F1_IN(z0, z1) → c1
F6_IN(z0, z1) → c1
F3_IN(z0, z1) → c1

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

POL(F13_IN(x₁, x₂)) = [1] + x₁
POL(F1_IN(x₁, x₂)) = [3] + x₁ + [3]x₂
POL(F3_IN(x₁, x₂)) = [2] + x₁ + [2]x₂
POL(F6_IN(x₁, x₂)) = [2] + x₁ + x₂
POL(c1) = 0
POL(c1(x₁)) = x₁
POL(c5(x₁)) = x₁
POL(s(x₁)) = [1] + x₁

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f3_in(z0, z1), z0, z1)
U1(f3_out1, z0, z1) → f1_out1
U1(f3_out2, z0, z1) → f1_out1
f13_in(z0, 0) → f13_out1(z0)
f13_in(0, z0) → f13_out1(0)
f13_in(s(z0), s(z1)) → U2(f13_in(z0, z1), s(z0), s(z1))
U2(f13_out1(z0), s(z1), s(z2)) → f13_out1(z0)
f6_in(z0, z1) → U3(f13_in(z0, z1), z0, z1)
U3(f13_out1(z0), z1, z2) → f6_out1
f8_in(z0, z1) → f8_out1
f3_in(z0, z1) → U4(f6_in(z0, z1), f8_in(z0, z1), z0, z1)
U4(f6_out1, z0, z1, z2) → f3_out1
U4(z0, f8_out1, z1, z2) → f3_out2

Tuples:

F1_IN(z0, z1) → c1(F3_IN(z0, z1))
F6_IN(z0, z1) → c1(F13_IN(z0, z1))
F3_IN(z0, z1) → c1(F6_IN(z0, z1))
F13_IN(s(z0), s(z1)) → c5(F13_IN(z0, z1))
F1_IN(z0, z1) → c1
F6_IN(z0, z1) → c1
F3_IN(z0, z1) → c1

S tuples:none
K tuples:

F1_IN(z0, z1) → c1(F3_IN(z0, z1))
F3_IN(z0, z1) → c1(F6_IN(z0, z1))
F1_IN(z0, z1) → c1
F6_IN(z0, z1) → c1
F3_IN(z0, z1) → c1
F6_IN(z0, z1) → c1(F13_IN(z0, z1))
F13_IN(s(z0), s(z1)) → c5(F13_IN(z0, z1))

Defined Rule Symbols:

f1_in, U1, f13_in, U2, f6_in, U3, f8_in, f3_in, U4

Defined Pair Symbols:

F1_IN, F6_IN, F3_IN, F13_IN

Compound Symbols:

c1, c5, c1

(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: q(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: q(T1, T2, T3), SCOPE: 1, CLAUSE: 5 | q(T1, T2, T3), SCOPE: 1, CLAUSE: 6\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: m(T7, T8, T10) | q(T7, T8, T3), SCOPE: 1, CLAUSE: 6\n\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: m(T7, T8, T10), SCOPE: 2, CLAUSE: 0 | m(T7, T8, T10), SCOPE: 2, CLAUSE: 1 | m(T7, T8, T10), SCOPE: 2, CLAUSE: 2 | ?_2 | q(T7, T8, T3), SCOPE: 1, CLAUSE: 6\n\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: ','(!_2, user_defined_=(T17, T15)) | m(T15, 0, T10), SCOPE: 2, CLAUSE: 1 | m(T15, 0, T10), SCOPE: 2, CLAUSE: 2 | ?_2 | q(T15, 0, T3), SCOPE: 1, CLAUSE: 6\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: m(T7, T8, T10), SCOPE: 2, CLAUSE: 1 | m(T7, T8, T10), SCOPE: 2, CLAUSE: 2 | ?_2 | q(T7, T8, T3), SCOPE: 1, CLAUSE: 6\n\nT7 is ground\nT8 is ground\nX11 is free\nX12 is free\nm(T7, T8, T10) !=? m(X11, 0, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: user_defined_=(T17, T15) | q(T15, 0, T3), SCOPE: 1, CLAUSE: 6\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: user_defined_=(T17, T15), SCOPE: 3, CLAUSE: 7 | ?_3 | q(T15, 0, T3), SCOPE: 1, CLAUSE: 6\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: true | ?_3 | q(T20, 0, T3), SCOPE: 1, CLAUSE: 6\n\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ?_3 | q(T15, 0, T3), SCOPE: 1, CLAUSE: 6\n\nT15 is ground\nX15 is free\nuser_defined_=(T17, T15) !=? user_defined_=(X15, X15)", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ?_3 | q(T20, 0, T3), SCOPE: 1, CLAUSE: 6\n\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: q(T20, 0, T3), SCOPE: 1, CLAUSE: 6\n\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: q(T15, 0, T3), SCOPE: 1, CLAUSE: 6\n\nT15 is ground\nX15 is free\nuser_defined_=(T17, T15) !=? user_defined_=(X15, X15)", 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];
28 [label="28: ','(!_2, user_defined_=(T39, 0)) | m(0, T37, T10), SCOPE: 2, CLAUSE: 2 | ?_2 | q(0, T37, T3), SCOPE: 1, CLAUSE: 6\n\nT37 is ground\nX11 is free\nX12 is free\nm(0, T37, T10) !=? m(X11, 0, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: m(T7, T8, T10), SCOPE: 2, CLAUSE: 2 | ?_2 | q(T7, T8, T3), SCOPE: 1, CLAUSE: 6\n\nT7 is ground\nT8 is ground\nX11 is free\nX12 is free\nX38 is free\nX39 is free\nm(T7, T8, T10) !=? m(X11, 0, X12)\nm(T7, T8, T10) !=? m(0, X38, X39)", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: user_defined_=(T39, 0) | q(0, T37, T3), SCOPE: 1, CLAUSE: 6\n\nT37 is ground\nX11 is free\nX12 is free\nm(0, T37, T10) !=? m(X11, 0, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: user_defined_=(T39, 0), SCOPE: 4, CLAUSE: 7 | ?_4 | q(0, T37, T3), SCOPE: 1, CLAUSE: 6\n\nT37 is ground\nX11 is free\nX12 is free\nm(0, T37, T10) !=? m(X11, 0, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: true | ?_4 | q(0, T37, T3), SCOPE: 1, CLAUSE: 6\n\nT37 is ground\nX11 is free\nX12 is free\nm(0, T37, T10) !=? m(X11, 0, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: ?_4 | q(0, T37, T3), SCOPE: 1, CLAUSE: 6\n\nT37 is ground\nX11 is free\nX12 is free\nm(0, T37, T10) !=? m(X11, 0, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: ?_4 | q(0, T37, T3), SCOPE: 1, CLAUSE: 6\n\nT37 is ground\nX11 is free\nX12 is free\nm(0, T37, T10) !=? m(X11, 0, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: q(0, T37, T3), SCOPE: 1, CLAUSE: 6\n\nT37 is ground\nX11 is free\nX12 is free\nm(0, T37, T10) !=? m(X11, 0, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: q(0, T37, T3), SCOPE: 1, CLAUSE: 6\n\nT37 is ground\nX11 is free\nX12 is free\nm(0, T37, T10) !=? m(X11, 0, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: m(T7, T8, T10), SCOPE: 2, CLAUSE: 2\n\nT7 is ground\nT8 is ground\nX11 is free\nX12 is free\nX38 is free\nX39 is free\nm(T7, T8, T10) !=? m(X11, 0, X12)\nm(T7, T8, T10) !=? m(0, X38, X39)", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: ?_2 | q(T7, T8, T3), SCOPE: 1, CLAUSE: 6\n\nT7 is ground\nT8 is ground\nX11 is free\nX12 is free\nX38 is free\nX39 is free\nm(T7, T8, T10) !=? m(X11, 0, X12)\nm(T7, T8, T10) !=? m(0, X38, X39)", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: ','(p(T71, X86), ','(p(T72, X87), m(X86, X87, T74)))\n\nT71 is ground\nT72 is ground\nX11 is free\nX12 is free\nX38 is free\nX39 is free\nX86 is free\nX87 is free\nm(T71, T72, T10) !=? m(X11, 0, X12)\nm(T71, T72, T10) !=? m(0, X38, X39)", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: ','(p(T71, X86), ','(p(T72, X87), m(X86, X87, T74))), SCOPE: 5, CLAUSE: 3 | ','(p(T71, X86), ','(p(T72, X87), m(X86, X87, T74))), SCOPE: 5, CLAUSE: 4\n\nT71 is ground\nT72 is ground\nX11 is free\nX12 is free\nX38 is free\nX39 is free\nX86 is free\nX87 is free\nm(T71, T72, T10) !=? m(X11, 0, X12)\nm(T71, T72, T10) !=? m(0, X38, X39)", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: ','(p(T71, X86), ','(p(T72, X87), m(X86, X87, T74))), SCOPE: 5, CLAUSE: 4\n\nT71 is ground\nT72 is ground\nX11 is free\nX12 is free\nX38 is free\nX39 is free\nX86 is free\nX87 is free\nm(T71, T72, T10) !=? m(X11, 0, X12)\nm(T71, T72, T10) !=? m(0, X38, X39)", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: ','(p(T72, X87), m(T78, X87, T74))\n\nT72 is ground\nT78 is ground\nX11 is free\nX12 is free\nX87 is free\nm(s(T78), T72, T10) !=? m(X11, 0, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: ','(p(T72, X87), m(T78, X87, T74)), SCOPE: 6, CLAUSE: 3 | ','(p(T72, X87), m(T78, X87, T74)), SCOPE: 6, CLAUSE: 4\n\nT72 is ground\nT78 is ground\nX11 is free\nX12 is free\nX87 is free\nm(s(T78), T72, T10) !=? m(X11, 0, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: ','(p(T72, X87), m(T78, X87, T74)), SCOPE: 6, CLAUSE: 4\n\nT72 is ground\nT78 is ground\nX11 is free\nX12 is free\nX87 is free\nm(s(T78), T72, T10) !=? m(X11, 0, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: m(T78, T83, T74)\n\nT78 is ground\nT83 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: m(T78, T83, T74), SCOPE: 7, CLAUSE: 0 | m(T78, T83, T74), SCOPE: 7, CLAUSE: 1 | m(T78, T83, T74), SCOPE: 7, CLAUSE: 2\n\nT78 is ground\nT83 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: ','(!_7, user_defined_=(T92, T90)) | m(T90, 0, T74), SCOPE: 7, CLAUSE: 1 | m(T90, 0, T74), SCOPE: 7, CLAUSE: 2\n\nT90 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: m(T78, T83, T74), SCOPE: 7, CLAUSE: 1 | m(T78, T83, T74), SCOPE: 7, CLAUSE: 2\n\nT78 is ground\nT83 is ground\nX105 is free\nX106 is free\nm(T78, T83, T74) !=? m(X105, 0, X106)", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: user_defined_=(T92, T90)\n\nT90 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: user_defined_=(T92, T90), SCOPE: 8, CLAUSE: 7\n\nT90 is ground", 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: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: ','(!_7, user_defined_=(T102, 0)) | m(0, T100, T74), SCOPE: 7, CLAUSE: 2\n\nT100 is ground\nX105 is free\nX106 is free\nm(0, T100, T74) !=? m(X105, 0, X106)", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: m(T78, T83, T74), SCOPE: 7, CLAUSE: 2\n\nT78 is ground\nT83 is ground\nX105 is free\nX106 is free\nX114 is free\nX115 is free\nm(T78, T83, T74) !=? m(X105, 0, X106)\nm(T78, T83, T74) !=? m(0, X114, X115)", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: user_defined_=(T102, 0)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: user_defined_=(T102, 0), SCOPE: 9, CLAUSE: 7\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: ','(p(T114, X133), ','(p(T115, X134), m(X133, X134, T117)))\n\nT114 is ground\nT115 is ground\nX105 is free\nX106 is free\nX114 is free\nX115 is free\nX133 is free\nX134 is free\nm(T114, T115, T74) !=? m(X105, 0, X106)\nm(T114, T115, T74) !=? m(0, X114, X115)", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: ','(p(T114, X133), ','(p(T115, X134), m(X133, X134, T117))), SCOPE: 10, CLAUSE: 3 | ','(p(T114, X133), ','(p(T115, X134), m(X133, X134, T117))), SCOPE: 10, CLAUSE: 4\n\nT114 is ground\nT115 is ground\nX105 is free\nX106 is free\nX114 is free\nX115 is free\nX133 is free\nX134 is free\nm(T114, T115, T74) !=? m(X105, 0, X106)\nm(T114, T115, T74) !=? m(0, X114, X115)", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: ','(p(T114, X133), ','(p(T115, X134), m(X133, X134, T117))), SCOPE: 10, CLAUSE: 4\n\nT114 is ground\nT115 is ground\nX105 is free\nX106 is free\nX114 is free\nX115 is free\nX133 is free\nX134 is free\nm(T114, T115, T74) !=? m(X105, 0, X106)\nm(T114, T115, T74) !=? m(0, X114, X115)", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: ','(p(T115, X134), m(T121, X134, T117))\n\nT115 is ground\nT121 is ground\nX105 is free\nX106 is free\nX134 is free\nm(s(T121), T115, T74) !=? m(X105, 0, X106)", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: ','(p(T115, X134), m(T121, X134, T117)), SCOPE: 11, CLAUSE: 3 | ','(p(T115, X134), m(T121, X134, T117)), SCOPE: 11, CLAUSE: 4\n\nT115 is ground\nT121 is ground\nX105 is free\nX106 is free\nX134 is free\nm(s(T121), T115, T74) !=? m(X105, 0, X106)", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: ','(p(T115, X134), m(T121, X134, T117)), SCOPE: 11, CLAUSE: 4\n\nT115 is ground\nT121 is ground\nX105 is free\nX106 is free\nX134 is free\nm(s(T121), T115, T74) !=? m(X105, 0, X106)", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: m(T121, T126, T117)\n\nT121 is ground\nT126 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: q(T7, T8, T3), SCOPE: 1, CLAUSE: 6\n\nT7 is ground\nT8 is ground\nX11 is free\nX12 is free\nX38 is free\nX39 is free\nm(T7, T8, T10) !=? m(X11, 0, X12)\nm(T7, T8, T10) !=? m(0, X38, X39)", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 100 [arrowhead = none ];
100 -> 4;

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

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

103 [label="EVAL with clause\nm(X11, 0, X12) :- ','(!_2, user_defined_=(X12, X11)).\nand substitutionT7 -> T15,\nX11 -> T15,\nT8 -> 0,\nT10 -> T17,\nX12 -> T17,\nT16 -> T17", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 103 [arrowhead = none ];
103 -> 9;

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

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

106 [label="EVAL with clause\nm(0, X38, X39) :- ','(!_2, user_defined_=(X39, 0)).\nand substitutionT7 -> 0,\nT8 -> T37,\nX38 -> T37,\nT10 -> T39,\nX39 -> T39,\nT38 -> T39", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 106 [arrowhead = none ];
106 -> 28;

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

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

109 [label="EVAL with clause\nuser_defined_=(X15, X15).\nand substitutionT17 -> T20,\nX15 -> T20,\nT15 -> T20", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 109 [arrowhead = none ];
109 -> 14;

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

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

112 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
15 -> 112 [arrowhead = none ];
112 -> 20;

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

114 [label="ONLY EVAL with clause\nq(X22, X23, X24).\nand substitutionT20 -> T25,\nX22 -> T25,\nX23 -> 0,\nT3 -> T26,\nX24 -> T26", fontsize=14, style = filled, fillcolor = lightblue];
17 -> 114 [arrowhead = none ];
114 -> 18;

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

116 [label="ONLY EVAL with clause\nq(X31, X32, X33).\nand substitutionT15 -> T31,\nX31 -> T31,\nX32 -> 0,\nT3 -> T32,\nX33 -> T32", fontsize=14, style = filled, fillcolor = lightblue];
20 -> 116 [arrowhead = none ];
116 -> 22;

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

118 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
28 -> 118 [arrowhead = none ];
118 -> 32;

119 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
29 -> 119 [arrowhead = none ];
119 -> 51;

120 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
29 -> 120 [arrowhead = none ];
120 -> 52;

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

122 [label="EVAL with clause\nuser_defined_=(X42, X42).\nand substitutionT39 -> 0,\nX42 -> 0,\nT42 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
33 -> 122 [arrowhead = none ];
122 -> 34;

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

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

125 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
36 -> 125 [arrowhead = none ];
125 -> 41;

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

127 [label="ONLY EVAL with clause\nq(X49, X50, X51).\nand substitutionX49 -> 0,\nT37 -> T47,\nX50 -> T47,\nT3 -> T48,\nX51 -> T48", fontsize=14, style = filled, fillcolor = lightblue];
38 -> 127 [arrowhead = none ];
127 -> 39;

128 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
39 -> 128 [arrowhead = none ];
128 -> 40;

129 [label="ONLY EVAL with clause\nq(X58, X59, X60).\nand substitutionX58 -> 0,\nT37 -> T53,\nX59 -> T53,\nT3 -> T54,\nX60 -> T54", fontsize=14, style = filled, fillcolor = lightblue];
41 -> 129 [arrowhead = none ];
129 -> 46;

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

131 [label="ONLY EVAL with clause\nm(X83, X84, X85) :- ','(p(X83, X86), ','(p(X84, X87), m(X86, X87, X85))).\nand substitutionT7 -> T71,\nX83 -> T71,\nT8 -> T72,\nX84 -> T72,\nT10 -> T74,\nX85 -> T74,\nT73 -> T74", fontsize=14, style = filled, fillcolor = lightblue];
51 -> 131 [arrowhead = none ];
131 -> 56;

132 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
52 -> 132 [arrowhead = none ];
132 -> 97;

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

134 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (m(T71, T72, T10), m(0, X38, X39))", fontsize=14, style = filled, fillcolor = lightgreen];
57 -> 134 [arrowhead = none ];
134 -> 59;

135 [label="EVAL with clause\np(s(X93), X93).\nand substitutionX93 -> T78,\nT71 -> s(T78),\nX86 -> T78", fontsize=14, style = filled, fillcolor = lightblue];
59 -> 135 [arrowhead = none ];
135 -> 62;

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

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

138 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (m(s(T78), T72, T10), m(X11, 0, X12))", fontsize=14, style = filled, fillcolor = lightgreen];
67 -> 138 [arrowhead = none ];
138 -> 68;

139 [label="EVAL with clause\np(s(X98), X98).\nand substitutionX98 -> T83,\nT72 -> s(T83),\nX87 -> T83", fontsize=14, style = filled, fillcolor = lightblue];
68 -> 139 [arrowhead = none ];
139 -> 69;

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

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

142 [label="EVAL with clause\nm(X105, 0, X106) :- ','(!_7, user_defined_=(X106, X105)).\nand substitutionT78 -> T90,\nX105 -> T90,\nT83 -> 0,\nT74 -> T92,\nX106 -> T92,\nT91 -> T92", fontsize=14, style = filled, fillcolor = lightblue];
71 -> 142 [arrowhead = none ];
142 -> 74;

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

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

145 [label="EVAL with clause\nm(0, X114, X115) :- ','(!_7, user_defined_=(X115, 0)).\nand substitutionT78 -> 0,\nT83 -> T100,\nX114 -> T100,\nT74 -> T102,\nX115 -> T102,\nT101 -> T102", fontsize=14, style = filled, fillcolor = lightblue];
75 -> 145 [arrowhead = none ];
145 -> 81;

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

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

148 [label="EVAL with clause\nuser_defined_=(X109, X109).\nand substitutionT92 -> T95,\nX109 -> T95,\nT90 -> T95", fontsize=14, style = filled, fillcolor = lightblue];
77 -> 148 [arrowhead = none ];
148 -> 78;

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

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

151 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
81 -> 151 [arrowhead = none ];
151 -> 83;

152 [label="ONLY EVAL with clause\nm(X130, X131, X132) :- ','(p(X130, X133), ','(p(X131, X134), m(X133, X134, X132))).\nand substitutionT78 -> T114,\nX130 -> T114,\nT83 -> T115,\nX131 -> T115,\nT74 -> T117,\nX132 -> T117,\nT116 -> T117", fontsize=14, style = filled, fillcolor = lightblue];
82 -> 152 [arrowhead = none ];
152 -> 88;

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

154 [label="EVAL with clause\nuser_defined_=(X118, X118).\nand substitutionT102 -> 0,\nX118 -> 0,\nT105 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
84 -> 154 [arrowhead = none ];
154 -> 85;

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

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

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

158 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (m(T114, T115, T74), m(0, X114, X115))", fontsize=14, style = filled, fillcolor = lightgreen];
89 -> 158 [arrowhead = none ];
158 -> 90;

159 [label="EVAL with clause\np(s(X140), X140).\nand substitutionX140 -> T121,\nT114 -> s(T121),\nX133 -> T121", fontsize=14, style = filled, fillcolor = lightblue];
90 -> 159 [arrowhead = none ];
159 -> 91;

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

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

162 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (m(s(T121), T115, T74), m(X105, 0, X106))", fontsize=14, style = filled, fillcolor = lightgreen];
93 -> 162 [arrowhead = none ];
162 -> 94;

163 [label="EVAL with clause\np(s(X145), X145).\nand substitutionX145 -> T126,\nT115 -> s(T126),\nX134 -> T126", fontsize=14, style = filled, fillcolor = lightblue];
94 -> 163 [arrowhead = none ];
163 -> 95;

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

165 [label="INSTANCE with matching:\nT78 -> T121\nT83 -> T126\nT74 -> T117", fontsize=14, style = filled, fillcolor = lightgrey];
95 -> 165 [arrowhead = none , style=dashed];
165 -> 69[style=dashed];

166 [label="ONLY EVAL with clause\nq(X154, X155, X156).\nand substitutionT7 -> T135,\nX154 -> T135,\nT8 -> T136,\nX155 -> T136,\nT3 -> T137,\nX156 -> T137", fontsize=14, style = filled, fillcolor = lightblue];
97 -> 166 [arrowhead = none ];
166 -> 98;

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

}

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, 0) → f2_out1
f2_in(0, z0) → f2_out1
f2_in(z0, z1) → U1(f29_in(z0, z1), z0, z1)
U1(f29_out1(z0), z1, z2) → f2_out1
U1(f29_out3, z0, z1) → f2_out1
f69_in(z0, 0) → f69_out1(z0)
f69_in(0, z0) → f69_out1(0)
f69_in(s(z0), s(z1)) → U2(f69_in(z0, z1), s(z0), s(z1))
U2(f69_out1(z0), s(z1), s(z2)) → f69_out1(z0)
f51_in(s(z0), s(z1)) → U3(f69_in(z0, z1), s(z0), s(z1))
U3(f69_out1(z0), s(z1), s(z2)) → f51_out1(z0)
f52_in(z0, z1) → f52_out2
f29_in(z0, z1) → U4(f51_in(z0, z1), f52_in(z0, z1), z0, z1)
U4(f51_out1(z0), z1, z2, z3) → f29_out1(z0)
U4(z0, f52_out2, z1, z2) → f29_out3

Tuples:

F2_IN(z0, z1) → c2(U1'(f29_in(z0, z1), z0, z1), F29_IN(z0, z1))
F69_IN(s(z0), s(z1)) → c7(U2'(f69_in(z0, z1), s(z0), s(z1)), F69_IN(z0, z1))
F51_IN(s(z0), s(z1)) → c9(U3'(f69_in(z0, z1), s(z0), s(z1)), F69_IN(z0, z1))
F29_IN(z0, z1) → c12(U4'(f51_in(z0, z1), f52_in(z0, z1), z0, z1), F51_IN(z0, z1), F52_IN(z0, z1))

S tuples:

F2_IN(z0, z1) → c2(U1'(f29_in(z0, z1), z0, z1), F29_IN(z0, z1))
F69_IN(s(z0), s(z1)) → c7(U2'(f69_in(z0, z1), s(z0), s(z1)), F69_IN(z0, z1))
F51_IN(s(z0), s(z1)) → c9(U3'(f69_in(z0, z1), s(z0), s(z1)), F69_IN(z0, z1))
F29_IN(z0, z1) → c12(U4'(f51_in(z0, z1), f52_in(z0, z1), z0, z1), F51_IN(z0, z1), F52_IN(z0, z1))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f69_in, U2, f51_in, U3, f52_in, f29_in, U4

Defined Pair Symbols:

F2_IN, F69_IN, F51_IN, F29_IN

Compound Symbols:

c2, c7, c9, c12

(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(z0, 0) → f2_out1
f2_in(0, z0) → f2_out1
f2_in(z0, z1) → U1(f29_in(z0, z1), z0, z1)
U1(f29_out1(z0), z1, z2) → f2_out1
U1(f29_out3, z0, z1) → f2_out1
f69_in(z0, 0) → f69_out1(z0)
f69_in(0, z0) → f69_out1(0)
f69_in(s(z0), s(z1)) → U2(f69_in(z0, z1), s(z0), s(z1))
U2(f69_out1(z0), s(z1), s(z2)) → f69_out1(z0)
f51_in(s(z0), s(z1)) → U3(f69_in(z0, z1), s(z0), s(z1))
U3(f69_out1(z0), s(z1), s(z2)) → f51_out1(z0)
f52_in(z0, z1) → f52_out2
f29_in(z0, z1) → U4(f51_in(z0, z1), f52_in(z0, z1), z0, z1)
U4(f51_out1(z0), z1, z2, z3) → f29_out1(z0)
U4(z0, f52_out2, z1, z2) → f29_out3

Tuples:

F69_IN(s(z0), s(z1)) → c7(U2'(f69_in(z0, z1), s(z0), s(z1)), F69_IN(z0, z1))
F2_IN(z0, z1) → c(U1'(f29_in(z0, z1), z0, z1))
F2_IN(z0, z1) → c(F29_IN(z0, z1))
F51_IN(s(z0), s(z1)) → c(U3'(f69_in(z0, z1), s(z0), s(z1)))
F51_IN(s(z0), s(z1)) → c(F69_IN(z0, z1))
F29_IN(z0, z1) → c(U4'(f51_in(z0, z1), f52_in(z0, z1), z0, z1))
F29_IN(z0, z1) → c(F51_IN(z0, z1))
F29_IN(z0, z1) → c(F52_IN(z0, z1))

S tuples:

F69_IN(s(z0), s(z1)) → c7(U2'(f69_in(z0, z1), s(z0), s(z1)), F69_IN(z0, z1))
F2_IN(z0, z1) → c(U1'(f29_in(z0, z1), z0, z1))
F2_IN(z0, z1) → c(F29_IN(z0, z1))
F51_IN(s(z0), s(z1)) → c(U3'(f69_in(z0, z1), s(z0), s(z1)))
F51_IN(s(z0), s(z1)) → c(F69_IN(z0, z1))
F29_IN(z0, z1) → c(U4'(f51_in(z0, z1), f52_in(z0, z1), z0, z1))
F29_IN(z0, z1) → c(F51_IN(z0, z1))
F29_IN(z0, z1) → c(F52_IN(z0, z1))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f69_in, U2, f51_in, U3, f52_in, f29_in, U4

Defined Pair Symbols:

F69_IN, F2_IN, F51_IN, F29_IN

Compound Symbols:

c7, c

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

Removed 5 trailing tuple parts

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, 0) → f2_out1
f2_in(0, z0) → f2_out1
f2_in(z0, z1) → U1(f29_in(z0, z1), z0, z1)
U1(f29_out1(z0), z1, z2) → f2_out1
U1(f29_out3, z0, z1) → f2_out1
f69_in(z0, 0) → f69_out1(z0)
f69_in(0, z0) → f69_out1(0)
f69_in(s(z0), s(z1)) → U2(f69_in(z0, z1), s(z0), s(z1))
U2(f69_out1(z0), s(z1), s(z2)) → f69_out1(z0)
f51_in(s(z0), s(z1)) → U3(f69_in(z0, z1), s(z0), s(z1))
U3(f69_out1(z0), s(z1), s(z2)) → f51_out1(z0)
f52_in(z0, z1) → f52_out2
f29_in(z0, z1) → U4(f51_in(z0, z1), f52_in(z0, z1), z0, z1)
U4(f51_out1(z0), z1, z2, z3) → f29_out1(z0)
U4(z0, f52_out2, z1, z2) → f29_out3

Tuples:

F2_IN(z0, z1) → c(F29_IN(z0, z1))
F51_IN(s(z0), s(z1)) → c(F69_IN(z0, z1))
F29_IN(z0, z1) → c(F51_IN(z0, z1))
F69_IN(s(z0), s(z1)) → c7(F69_IN(z0, z1))
F2_IN(z0, z1) → c
F51_IN(s(z0), s(z1)) → c
F29_IN(z0, z1) → c

S tuples:

F2_IN(z0, z1) → c(F29_IN(z0, z1))
F51_IN(s(z0), s(z1)) → c(F69_IN(z0, z1))
F29_IN(z0, z1) → c(F51_IN(z0, z1))
F69_IN(s(z0), s(z1)) → c7(F69_IN(z0, z1))
F2_IN(z0, z1) → c
F51_IN(s(z0), s(z1)) → c
F29_IN(z0, z1) → c

K tuples:none
Defined Rule Symbols:

f2_in, U1, f69_in, U2, f51_in, U3, f52_in, f29_in, U4

Defined Pair Symbols:

F2_IN, F51_IN, F29_IN, F69_IN

Compound Symbols:

c, c7, c

(21) CdtKnowledgeProof (EQUIVALENT transformation)

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

F2_IN(z0, z1) → c(F29_IN(z0, z1))
F29_IN(z0, z1) → c(F51_IN(z0, z1))
F2_IN(z0, z1) → c
F51_IN(s(z0), s(z1)) → c
F29_IN(z0, z1) → c
F29_IN(z0, z1) → c
F29_IN(z0, z1) → c(F51_IN(z0, z1))
F29_IN(z0, z1) → c
F29_IN(z0, z1) → c
F51_IN(s(z0), s(z1)) → c(F69_IN(z0, z1))
F51_IN(s(z0), s(z1)) → c

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, 0) → f2_out1
f2_in(0, z0) → f2_out1
f2_in(z0, z1) → U1(f29_in(z0, z1), z0, z1)
U1(f29_out1(z0), z1, z2) → f2_out1
U1(f29_out3, z0, z1) → f2_out1
f69_in(z0, 0) → f69_out1(z0)
f69_in(0, z0) → f69_out1(0)
f69_in(s(z0), s(z1)) → U2(f69_in(z0, z1), s(z0), s(z1))
U2(f69_out1(z0), s(z1), s(z2)) → f69_out1(z0)
f51_in(s(z0), s(z1)) → U3(f69_in(z0, z1), s(z0), s(z1))
U3(f69_out1(z0), s(z1), s(z2)) → f51_out1(z0)
f52_in(z0, z1) → f52_out2
f29_in(z0, z1) → U4(f51_in(z0, z1), f52_in(z0, z1), z0, z1)
U4(f51_out1(z0), z1, z2, z3) → f29_out1(z0)
U4(z0, f52_out2, z1, z2) → f29_out3

Tuples:

F2_IN(z0, z1) → c(F29_IN(z0, z1))
F51_IN(s(z0), s(z1)) → c(F69_IN(z0, z1))
F29_IN(z0, z1) → c(F51_IN(z0, z1))
F69_IN(s(z0), s(z1)) → c7(F69_IN(z0, z1))
F2_IN(z0, z1) → c
F51_IN(s(z0), s(z1)) → c
F29_IN(z0, z1) → c

S tuples:

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

K tuples:

F2_IN(z0, z1) → c(F29_IN(z0, z1))
F29_IN(z0, z1) → c(F51_IN(z0, z1))
F2_IN(z0, z1) → c
F51_IN(s(z0), s(z1)) → c
F29_IN(z0, z1) → c
F51_IN(s(z0), s(z1)) → c(F69_IN(z0, z1))

Defined Rule Symbols:

f2_in, U1, f69_in, U2, f51_in, U3, f52_in, f29_in, U4

Defined Pair Symbols:

F2_IN, F51_IN, F29_IN, F69_IN

Compound Symbols:

c, c7, c

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

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

We considered the (Usable) Rules:none
And the Tuples:

F2_IN(z0, z1) → c(F29_IN(z0, z1))
F51_IN(s(z0), s(z1)) → c(F69_IN(z0, z1))
F29_IN(z0, z1) → c(F51_IN(z0, z1))
F69_IN(s(z0), s(z1)) → c7(F69_IN(z0, z1))
F2_IN(z0, z1) → c
F51_IN(s(z0), s(z1)) → c
F29_IN(z0, z1) → c

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

POL(F29_IN(x₁, x₂)) = [1] + x₁ + [3]x₂
POL(F2_IN(x₁, x₂)) = [2] + x₁ + [3]x₂
POL(F51_IN(x₁, x₂)) = x₁
POL(F69_IN(x₁, x₂)) = [1] + x₁
POL(c) = 0
POL(c(x₁)) = x₁
POL(c7(x₁)) = x₁
POL(s(x₁)) = [1] + x₁

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, 0) → f2_out1
f2_in(0, z0) → f2_out1
f2_in(z0, z1) → U1(f29_in(z0, z1), z0, z1)
U1(f29_out1(z0), z1, z2) → f2_out1
U1(f29_out3, z0, z1) → f2_out1
f69_in(z0, 0) → f69_out1(z0)
f69_in(0, z0) → f69_out1(0)
f69_in(s(z0), s(z1)) → U2(f69_in(z0, z1), s(z0), s(z1))
U2(f69_out1(z0), s(z1), s(z2)) → f69_out1(z0)
f51_in(s(z0), s(z1)) → U3(f69_in(z0, z1), s(z0), s(z1))
U3(f69_out1(z0), s(z1), s(z2)) → f51_out1(z0)
f52_in(z0, z1) → f52_out2
f29_in(z0, z1) → U4(f51_in(z0, z1), f52_in(z0, z1), z0, z1)
U4(f51_out1(z0), z1, z2, z3) → f29_out1(z0)
U4(z0, f52_out2, z1, z2) → f29_out3

Tuples:

F2_IN(z0, z1) → c(F29_IN(z0, z1))
F51_IN(s(z0), s(z1)) → c(F69_IN(z0, z1))
F29_IN(z0, z1) → c(F51_IN(z0, z1))
F69_IN(s(z0), s(z1)) → c7(F69_IN(z0, z1))
F2_IN(z0, z1) → c
F51_IN(s(z0), s(z1)) → c
F29_IN(z0, z1) → c

S tuples:none
K tuples:

F2_IN(z0, z1) → c(F29_IN(z0, z1))
F29_IN(z0, z1) → c(F51_IN(z0, z1))
F2_IN(z0, z1) → c
F51_IN(s(z0), s(z1)) → c
F29_IN(z0, z1) → c
F51_IN(s(z0), s(z1)) → c(F69_IN(z0, z1))
F69_IN(s(z0), s(z1)) → c7(F69_IN(z0, z1))

Defined Rule Symbols:

f2_in, U1, f69_in, U2, f51_in, U3, f52_in, f29_in, U4

Defined Pair Symbols:

F2_IN, F51_IN, F29_IN, F69_IN

Compound Symbols:

c, c7, c