Runtime Complexity proof of /tmp/tmp8xvQfM/minus3.pl

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

0 Prolog

↳1 PrologToCdtProblemTransformerProof (UPPER BOUND (ID), 162 ms)

↳2 CdtProblem

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

    ↳4 CdtProblem

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

    ↳6 CdtProblem

    ↳7 CdtKnowledgeProof (⇔, 0 ms)

    ↳8 CdtProblem

    ↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 162 ms)

    ↳10 CdtProblem

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

    ↳12 CdtProblem

    ↳13 SIsEmptyProof (⇔, 0 ms)

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

↳15 PrologToCdtProblemTransformerProof (UPPER BOUND (ID), 163 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))), 170 ms)

    ↳24 CdtProblem

(0) Obligation:

Clauses:

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

Query: q(g,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: q(T1, T2)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: q(T1, T2), SCOPE: 1, CLAUSE: 0\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: m(T9, T10, X10)\n\nT9 is ground\nT10 is ground\nX10 is free", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: m(T9, T10, X10), SCOPE: 2, CLAUSE: 1 | m(T9, T10, X10), SCOPE: 2, CLAUSE: 2 | m(T9, T10, X10), SCOPE: 2, CLAUSE: 3\n\nT9 is ground\nT10 is ground\nX10 is free", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: true | m(T15, 0, X10), SCOPE: 2, CLAUSE: 2 | m(T15, 0, X10), SCOPE: 2, CLAUSE: 3\n\nT15 is ground\nX10 is free", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: m(T9, T10, X10), SCOPE: 2, CLAUSE: 2 | m(T9, T10, X10), SCOPE: 2, CLAUSE: 3\n\nT9 is ground\nT10 is ground\nX10 is free\nX15 is free\nm(T9, T10, X10) !=? m(X15, 0, X15)", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: m(T15, 0, X10), SCOPE: 2, CLAUSE: 2 | m(T15, 0, X10), SCOPE: 2, CLAUSE: 3\n\nT15 is ground\nX10 is free", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: !_2 | m(0, 0, X10), SCOPE: 2, CLAUSE: 3\n\nX10 is free", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: m(T15, 0, X10), SCOPE: 2, CLAUSE: 3\n\nT15 is ground\nX10 is free\nX18 is free\nm(T15, 0, X10) !=? m(0, X18, 0)", 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: ','(p(T18, X34), ','(p(0, X35), m(X34, X35, X36)))\n\nT18 is ground\nX10 is free\nX18 is free\nX36 is free\nX34 is free\nX35 is free\nm(T18, 0, X10) !=? m(0, X18, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: ','(p(T18, X34), ','(p(0, X35), m(X34, X35, X36))), SCOPE: 3, CLAUSE: 4 | ','(p(T18, X34), ','(p(0, X35), m(X34, X35, X36))), SCOPE: 3, CLAUSE: 5\n\nT18 is ground\nX10 is free\nX18 is free\nX36 is free\nX34 is free\nX35 is free\nm(T18, 0, X10) !=? m(0, X18, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: ','(p(T18, X34), ','(p(0, X35), m(X34, X35, X36))), SCOPE: 3, CLAUSE: 5\n\nT18 is ground\nX10 is free\nX18 is free\nX36 is free\nX34 is free\nX35 is free\nm(T18, 0, X10) !=? m(0, X18, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: ','(p(0, X35), m(T21, X35, X36))\n\nT21 is ground\nX36 is free\nX35 is free", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: ','(p(0, X35), m(T21, X35, X36)), SCOPE: 4, CLAUSE: 4 | ','(p(0, X35), m(T21, X35, X36)), SCOPE: 4, CLAUSE: 5\n\nT21 is ground\nX36 is free\nX35 is free", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: m(T21, 0, X36) | ','(p(0, X35), m(T21, X35, X36)), SCOPE: 4, CLAUSE: 5\n\nT21 is ground\nX36 is free\nX35 is free", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: m(T21, 0, X36)\n\nT21 is ground\nX36 is free", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: ','(p(0, X35), m(T21, X35, X36)), SCOPE: 4, CLAUSE: 5\n\nT21 is ground\nX36 is free\nX35 is free", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: m(T21, 0, X36), SCOPE: 5, CLAUSE: 1 | m(T21, 0, X36), SCOPE: 5, CLAUSE: 2 | m(T21, 0, X36), SCOPE: 5, CLAUSE: 3\n\nT21 is ground\nX36 is free", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: true | m(T28, 0, X36), SCOPE: 5, CLAUSE: 2 | m(T28, 0, X36), SCOPE: 5, CLAUSE: 3\n\nT28 is ground\nX36 is free", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: m(T28, 0, X36), SCOPE: 5, CLAUSE: 2 | m(T28, 0, X36), SCOPE: 5, CLAUSE: 3\n\nT28 is ground\nX36 is free", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: !_5 | m(0, 0, X36), SCOPE: 5, CLAUSE: 3\n\nX36 is free", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: m(T28, 0, X36), SCOPE: 5, CLAUSE: 3\n\nT28 is ground\nX36 is free\nX51 is free\nm(T28, 0, X36) !=? m(0, X51, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: ','(p(T31, X67), ','(p(0, X68), m(X67, X68, X69)))\n\nT31 is ground\nX36 is free\nX51 is free\nX69 is free\nX67 is free\nX68 is free\nm(T31, 0, X36) !=? m(0, X51, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: ','(p(T31, X67), ','(p(0, X68), m(X67, X68, X69))), SCOPE: 6, CLAUSE: 4 | ','(p(T31, X67), ','(p(0, X68), m(X67, X68, X69))), SCOPE: 6, CLAUSE: 5\n\nT31 is ground\nX36 is free\nX51 is free\nX69 is free\nX67 is free\nX68 is free\nm(T31, 0, X36) !=? m(0, X51, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: ','(p(T31, X67), ','(p(0, X68), m(X67, X68, X69))), SCOPE: 6, CLAUSE: 5\n\nT31 is ground\nX36 is free\nX51 is free\nX69 is free\nX67 is free\nX68 is free\nm(T31, 0, X36) !=? m(0, X51, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: ','(p(0, X68), m(T34, X68, X69))\n\nT34 is ground\nX69 is free\nX68 is free", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: ','(p(0, X68), m(T34, X68, X69)), SCOPE: 7, CLAUSE: 4 | ','(p(0, X68), m(T34, X68, X69)), SCOPE: 7, CLAUSE: 5\n\nT34 is ground\nX69 is free\nX68 is free", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: m(T34, 0, X69) | ','(p(0, X68), m(T34, X68, X69)), SCOPE: 7, CLAUSE: 5\n\nT34 is ground\nX69 is free\nX68 is free", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: m(T34, 0, X69)\n\nT34 is ground\nX69 is free", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: ','(p(0, X68), m(T34, X68, X69)), SCOPE: 7, CLAUSE: 5\n\nT34 is ground\nX69 is free\nX68 is free", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: !_2 | m(0, T41, X10), SCOPE: 2, CLAUSE: 3\n\nT41 is ground\nX10 is free\nX15 is free\nm(0, T41, X10) !=? m(X15, 0, X15)", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: m(T9, T10, X10), SCOPE: 2, CLAUSE: 3\n\nT9 is ground\nT10 is ground\nX10 is free\nX15 is free\nX83 is free\nm(T9, T10, X10) !=? m(X15, 0, X15)\nm(T9, T10, X10) !=? m(0, X83, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: ','(p(T46, X99), ','(p(T47, X100), m(X99, X100, X101)))\n\nT46 is ground\nT47 is ground\nX10 is free\nX15 is free\nX83 is free\nX101 is free\nX99 is free\nX100 is free\nm(T46, T47, X10) !=? m(X15, 0, X15)\nm(T46, T47, X10) !=? m(0, X83, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: ','(p(T46, X99), ','(p(T47, X100), m(X99, X100, X101))), SCOPE: 8, CLAUSE: 4 | ','(p(T46, X99), ','(p(T47, X100), m(X99, X100, X101))), SCOPE: 8, CLAUSE: 5\n\nT46 is ground\nT47 is ground\nX10 is free\nX15 is free\nX83 is free\nX101 is free\nX99 is free\nX100 is free\nm(T46, T47, X10) !=? m(X15, 0, X15)\nm(T46, T47, X10) !=? m(0, X83, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: ','(p(T46, X99), ','(p(T47, X100), m(X99, X100, X101))), SCOPE: 8, CLAUSE: 5\n\nT46 is ground\nT47 is ground\nX10 is free\nX15 is free\nX83 is free\nX101 is free\nX99 is free\nX100 is free\nm(T46, T47, X10) !=? m(X15, 0, X15)\nm(T46, T47, X10) !=? m(0, X83, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: ','(p(T47, X100), m(T50, X100, X101))\n\nT47 is ground\nT50 is ground\nX10 is free\nX15 is free\nX101 is free\nX100 is free\nm(s(T50), T47, X10) !=? m(X15, 0, X15)", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: ','(p(T47, X100), m(T50, X100, X101)), SCOPE: 9, CLAUSE: 4 | ','(p(T47, X100), m(T50, X100, X101)), SCOPE: 9, CLAUSE: 5\n\nT47 is ground\nT50 is ground\nX10 is free\nX15 is free\nX101 is free\nX100 is free\nm(s(T50), T47, X10) !=? m(X15, 0, X15)", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: ','(p(T47, X100), m(T50, X100, X101)), SCOPE: 9, CLAUSE: 5\n\nT47 is ground\nT50 is ground\nX10 is free\nX15 is free\nX101 is free\nX100 is free\nm(s(T50), T47, X10) !=? m(X15, 0, X15)", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: m(T50, T54, X101)\n\nT50 is ground\nT54 is ground\nX101 is free", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 103 [arrowhead = none ];
103 -> 4;

104 [label="ONLY EVAL with clause\nq(X8, X9) :- m(X8, X9, X10).\nand substitutionT1 -> T9,\nX8 -> T9,\nT2 -> T10,\nX9 -> T10", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 104 [arrowhead = none ];
104 -> 7;

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

106 [label="EVAL with clause\nm(X15, 0, X15).\nand substitutionT9 -> T15,\nX15 -> T15,\nT10 -> 0,\nX10 -> T15", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 106 [arrowhead = none ];
106 -> 16;

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

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

109 [label="EVAL with clause\nm(0, X83, 0) :- !_2.\nand substitutionT9 -> 0,\nT10 -> T41,\nX83 -> T41,\nX10 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
17 -> 109 [arrowhead = none ];
109 -> 86;

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

111 [label="EVAL with clause\nm(0, X18, 0) :- !_2.\nand substitutionT15 -> 0,\nX18 -> 0,\nX10 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
18 -> 111 [arrowhead = none ];
111 -> 20;

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

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

114 [label="ONLY EVAL with clause\nm(X31, X32, X33) :- ','(p(X31, X34), ','(p(X32, X35), m(X34, X35, X33))).\nand substitutionT15 -> T18,\nX31 -> T18,\nX32 -> 0,\nX10 -> X36,\nX33 -> X36", fontsize=14, style = filled, fillcolor = lightblue];
21 -> 114 [arrowhead = none ];
114 -> 28;

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

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

117 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (m(T18, 0, X10), m(0, X18, 0))", fontsize=14, style = filled, fillcolor = lightgreen];
31 -> 117 [arrowhead = none ];
117 -> 35;

118 [label="EVAL with clause\np(s(X41), X41).\nand substitutionX41 -> T21,\nT18 -> s(T21),\nX34 -> T21", fontsize=14, style = filled, fillcolor = lightblue];
35 -> 118 [arrowhead = none ];
118 -> 38;

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

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

121 [label="ONLY EVAL with clause\np(0, 0).\nand substitutionX35 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
43 -> 121 [arrowhead = none ];
121 -> 45;

122 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
45 -> 122 [arrowhead = none ];
122 -> 46;

123 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
45 -> 123 [arrowhead = none ];
123 -> 47;

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

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

126 [label="ONLY EVAL with clause\nm(X48, 0, X48).\nand substitutionT21 -> T28,\nX48 -> T28,\nX36 -> T28", fontsize=14, style = filled, fillcolor = lightblue];
54 -> 126 [arrowhead = none ];
126 -> 56;

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

128 [label="EVAL with clause\nm(0, X51, 0) :- !_5.\nand substitutionT28 -> 0,\nX51 -> 0,\nX36 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
57 -> 128 [arrowhead = none ];
128 -> 60;

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

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

131 [label="ONLY EVAL with clause\nm(X64, X65, X66) :- ','(p(X64, X67), ','(p(X65, X68), m(X67, X68, X66))).\nand substitutionT28 -> T31,\nX64 -> T31,\nX65 -> 0,\nX36 -> X69,\nX66 -> X69", fontsize=14, style = filled, fillcolor = lightblue];
61 -> 131 [arrowhead = none ];
131 -> 70;

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

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

134 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (m(T31, 0, X36), m(0, X51, 0))", fontsize=14, style = filled, fillcolor = lightgreen];
71 -> 134 [arrowhead = none ];
134 -> 72;

135 [label="EVAL with clause\np(s(X74), X74).\nand substitutionX74 -> T34,\nT31 -> s(T34),\nX67 -> T34", fontsize=14, style = filled, fillcolor = lightblue];
72 -> 135 [arrowhead = none ];
135 -> 73;

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

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

138 [label="ONLY EVAL with clause\np(0, 0).\nand substitutionX68 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
75 -> 138 [arrowhead = none ];
138 -> 77;

139 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
77 -> 139 [arrowhead = none ];
139 -> 78;

140 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
77 -> 140 [arrowhead = none ];
140 -> 79;

141 [label="INSTANCE with matching:\nT21 -> T34\nX36 -> X69", fontsize=14, style = filled, fillcolor = lightgrey];
78 -> 141 [arrowhead = none , style=dashed];
141 -> 46[style=dashed];

142 [label="BACKTRACK\nfor clause: p(s(X), X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
79 -> 142 [arrowhead = none ];
142 -> 82;

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

144 [label="ONLY EVAL with clause\nm(X96, X97, X98) :- ','(p(X96, X99), ','(p(X97, X100), m(X99, X100, X98))).\nand substitutionT9 -> T46,\nX96 -> T46,\nT10 -> T47,\nX97 -> T47,\nX10 -> X101,\nX98 -> X101", fontsize=14, style = filled, fillcolor = lightblue];
87 -> 144 [arrowhead = none ];
144 -> 94;

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

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

147 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (m(T46, T47, X10), m(0, X83, 0))", fontsize=14, style = filled, fillcolor = lightgreen];
95 -> 147 [arrowhead = none ];
147 -> 96;

148 [label="EVAL with clause\np(s(X106), X106).\nand substitutionX106 -> T50,\nT46 -> s(T50),\nX99 -> T50", fontsize=14, style = filled, fillcolor = lightblue];
96 -> 148 [arrowhead = none ];
148 -> 97;

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

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

151 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (m(s(T50), T47, X10), m(X15, 0, X15))", fontsize=14, style = filled, fillcolor = lightgreen];
99 -> 151 [arrowhead = none ];
151 -> 100;

152 [label="EVAL with clause\np(s(X110), X110).\nand substitutionX110 -> T54,\nT47 -> s(T54),\nX100 -> T54", fontsize=14, style = filled, fillcolor = lightblue];
100 -> 152 [arrowhead = none ];
152 -> 101;

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

154 [label="INSTANCE with matching:\nT9 -> T50\nT10 -> T54\nX10 -> X101", fontsize=14, style = filled, fillcolor = lightgrey];
101 -> 154 [arrowhead = none , style=dashed];
154 -> 7[style=dashed];

}

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f7_in(z0, z1), z0, z1)
U1(f7_out1(z0), z1, z2) → f1_out1
f7_in(z0, 0) → f7_out1(z0)
f7_in(0, 0) → f7_out1(0)
f7_in(s(z0), 0) → U2(f45_in(z0), s(z0), 0)
f7_in(0, z0) → f7_out1(0)
f7_in(s(z0), s(z1)) → U3(f7_in(z0, z1), s(z0), s(z1))
U2(f45_out1(z0), s(z1), 0) → f7_out1(z0)
U2(f45_out2(z0, z1), s(z2), 0) → f7_out1(z1)
U3(f7_out1(z0), s(z1), s(z2)) → f7_out1(z0)
f46_in(z0) → f46_out1(z0)
f46_in(0) → f46_out1(0)
f46_in(s(z0)) → U4(f77_in(z0), s(z0))
U4(f77_out1(z0), s(z1)) → f46_out1(z0)
U4(f77_out2(z0, z1), s(z2)) → f46_out1(z1)
f45_in(z0) → U5(f46_in(z0), f47_in(z0), z0)
U5(f46_out1(z0), z1, z2) → f45_out1(z0)
U5(z0, f47_out1(z1, z2), z3) → f45_out2(z1, z2)
f77_in(z0) → U6(f46_in(z0), f79_in(z0), z0)
U6(f46_out1(z0), z1, z2) → f77_out1(z0)
U6(z0, f79_out1(z1, z2), z3) → f77_out2(z1, z2)

Tuples:

F1_IN(z0, z1) → c(U1'(f7_in(z0, z1), z0, z1), F7_IN(z0, z1))
F7_IN(s(z0), 0) → c4(U2'(f45_in(z0), s(z0), 0), F45_IN(z0))
F7_IN(s(z0), s(z1)) → c6(U3'(f7_in(z0, z1), s(z0), s(z1)), F7_IN(z0, z1))
F46_IN(s(z0)) → c12(U4'(f77_in(z0), s(z0)), F77_IN(z0))
F45_IN(z0) → c15(U5'(f46_in(z0), f47_in(z0), z0), F46_IN(z0))
F77_IN(z0) → c18(U6'(f46_in(z0), f79_in(z0), z0), F46_IN(z0))

S tuples:

F1_IN(z0, z1) → c(U1'(f7_in(z0, z1), z0, z1), F7_IN(z0, z1))
F7_IN(s(z0), 0) → c4(U2'(f45_in(z0), s(z0), 0), F45_IN(z0))
F7_IN(s(z0), s(z1)) → c6(U3'(f7_in(z0, z1), s(z0), s(z1)), F7_IN(z0, z1))
F46_IN(s(z0)) → c12(U4'(f77_in(z0), s(z0)), F77_IN(z0))
F45_IN(z0) → c15(U5'(f46_in(z0), f47_in(z0), z0), F46_IN(z0))
F77_IN(z0) → c18(U6'(f46_in(z0), f79_in(z0), z0), F46_IN(z0))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f7_in, U2, U3, f46_in, U4, f45_in, U5, f77_in, U6

Defined Pair Symbols:

F1_IN, F7_IN, F46_IN, F45_IN, F77_IN

Compound Symbols:

c, c4, c6, c12, c15, c18

(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, z1) → U1(f7_in(z0, z1), z0, z1)
U1(f7_out1(z0), z1, z2) → f1_out1
f7_in(z0, 0) → f7_out1(z0)
f7_in(0, 0) → f7_out1(0)
f7_in(s(z0), 0) → U2(f45_in(z0), s(z0), 0)
f7_in(0, z0) → f7_out1(0)
f7_in(s(z0), s(z1)) → U3(f7_in(z0, z1), s(z0), s(z1))
U2(f45_out1(z0), s(z1), 0) → f7_out1(z0)
U2(f45_out2(z0, z1), s(z2), 0) → f7_out1(z1)
U3(f7_out1(z0), s(z1), s(z2)) → f7_out1(z0)
f46_in(z0) → f46_out1(z0)
f46_in(0) → f46_out1(0)
f46_in(s(z0)) → U4(f77_in(z0), s(z0))
U4(f77_out1(z0), s(z1)) → f46_out1(z0)
U4(f77_out2(z0, z1), s(z2)) → f46_out1(z1)
f45_in(z0) → U5(f46_in(z0), f47_in(z0), z0)
U5(f46_out1(z0), z1, z2) → f45_out1(z0)
U5(z0, f47_out1(z1, z2), z3) → f45_out2(z1, z2)
f77_in(z0) → U6(f46_in(z0), f79_in(z0), z0)
U6(f46_out1(z0), z1, z2) → f77_out1(z0)
U6(z0, f79_out1(z1, z2), z3) → f77_out2(z1, z2)

Tuples:

F7_IN(s(z0), s(z1)) → c6(U3'(f7_in(z0, z1), s(z0), s(z1)), F7_IN(z0, z1))
F46_IN(s(z0)) → c12(U4'(f77_in(z0), s(z0)), F77_IN(z0))
F77_IN(z0) → c18(U6'(f46_in(z0), f79_in(z0), z0), F46_IN(z0))
F1_IN(z0, z1) → c1(U1'(f7_in(z0, z1), z0, z1))
F1_IN(z0, z1) → c1(F7_IN(z0, z1))
F7_IN(s(z0), 0) → c1(U2'(f45_in(z0), s(z0), 0))
F7_IN(s(z0), 0) → c1(F45_IN(z0))
F45_IN(z0) → c1(U5'(f46_in(z0), f47_in(z0), z0))
F45_IN(z0) → c1(F46_IN(z0))

S tuples:

F7_IN(s(z0), s(z1)) → c6(U3'(f7_in(z0, z1), s(z0), s(z1)), F7_IN(z0, z1))
F46_IN(s(z0)) → c12(U4'(f77_in(z0), s(z0)), F77_IN(z0))
F77_IN(z0) → c18(U6'(f46_in(z0), f79_in(z0), z0), F46_IN(z0))
F1_IN(z0, z1) → c1(U1'(f7_in(z0, z1), z0, z1))
F1_IN(z0, z1) → c1(F7_IN(z0, z1))
F7_IN(s(z0), 0) → c1(U2'(f45_in(z0), s(z0), 0))
F7_IN(s(z0), 0) → c1(F45_IN(z0))
F45_IN(z0) → c1(U5'(f46_in(z0), f47_in(z0), z0))
F45_IN(z0) → c1(F46_IN(z0))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f7_in, U2, U3, f46_in, U4, f45_in, U5, f77_in, U6

Defined Pair Symbols:

F7_IN, F46_IN, F77_IN, F1_IN, F45_IN

Compound Symbols:

c6, c12, c18, c1

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

Removed 6 trailing tuple parts

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f7_in(z0, z1), z0, z1)
U1(f7_out1(z0), z1, z2) → f1_out1
f7_in(z0, 0) → f7_out1(z0)
f7_in(0, 0) → f7_out1(0)
f7_in(s(z0), 0) → U2(f45_in(z0), s(z0), 0)
f7_in(0, z0) → f7_out1(0)
f7_in(s(z0), s(z1)) → U3(f7_in(z0, z1), s(z0), s(z1))
U2(f45_out1(z0), s(z1), 0) → f7_out1(z0)
U2(f45_out2(z0, z1), s(z2), 0) → f7_out1(z1)
U3(f7_out1(z0), s(z1), s(z2)) → f7_out1(z0)
f46_in(z0) → f46_out1(z0)
f46_in(0) → f46_out1(0)
f46_in(s(z0)) → U4(f77_in(z0), s(z0))
U4(f77_out1(z0), s(z1)) → f46_out1(z0)
U4(f77_out2(z0, z1), s(z2)) → f46_out1(z1)
f45_in(z0) → U5(f46_in(z0), f47_in(z0), z0)
U5(f46_out1(z0), z1, z2) → f45_out1(z0)
U5(z0, f47_out1(z1, z2), z3) → f45_out2(z1, z2)
f77_in(z0) → U6(f46_in(z0), f79_in(z0), z0)
U6(f46_out1(z0), z1, z2) → f77_out1(z0)
U6(z0, f79_out1(z1, z2), z3) → f77_out2(z1, z2)

Tuples:

F1_IN(z0, z1) → c1(F7_IN(z0, z1))
F7_IN(s(z0), 0) → c1(F45_IN(z0))
F45_IN(z0) → c1(F46_IN(z0))
F7_IN(s(z0), s(z1)) → c6(F7_IN(z0, z1))
F46_IN(s(z0)) → c12(F77_IN(z0))
F77_IN(z0) → c18(F46_IN(z0))
F1_IN(z0, z1) → c1
F7_IN(s(z0), 0) → c1
F45_IN(z0) → c1

S tuples:

F1_IN(z0, z1) → c1(F7_IN(z0, z1))
F7_IN(s(z0), 0) → c1(F45_IN(z0))
F45_IN(z0) → c1(F46_IN(z0))
F7_IN(s(z0), s(z1)) → c6(F7_IN(z0, z1))
F46_IN(s(z0)) → c12(F77_IN(z0))
F77_IN(z0) → c18(F46_IN(z0))
F1_IN(z0, z1) → c1
F7_IN(s(z0), 0) → c1
F45_IN(z0) → c1

K tuples:none
Defined Rule Symbols:

f1_in, U1, f7_in, U2, U3, f46_in, U4, f45_in, U5, f77_in, U6

Defined Pair Symbols:

F1_IN, F7_IN, F45_IN, F46_IN, F77_IN

Compound Symbols:

c1, c6, c12, c18, c1

(7) CdtKnowledgeProof (EQUIVALENT transformation)

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

F1_IN(z0, z1) → c1(F7_IN(z0, z1))
F1_IN(z0, z1) → c1

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f7_in(z0, z1), z0, z1)
U1(f7_out1(z0), z1, z2) → f1_out1
f7_in(z0, 0) → f7_out1(z0)
f7_in(0, 0) → f7_out1(0)
f7_in(s(z0), 0) → U2(f45_in(z0), s(z0), 0)
f7_in(0, z0) → f7_out1(0)
f7_in(s(z0), s(z1)) → U3(f7_in(z0, z1), s(z0), s(z1))
U2(f45_out1(z0), s(z1), 0) → f7_out1(z0)
U2(f45_out2(z0, z1), s(z2), 0) → f7_out1(z1)
U3(f7_out1(z0), s(z1), s(z2)) → f7_out1(z0)
f46_in(z0) → f46_out1(z0)
f46_in(0) → f46_out1(0)
f46_in(s(z0)) → U4(f77_in(z0), s(z0))
U4(f77_out1(z0), s(z1)) → f46_out1(z0)
U4(f77_out2(z0, z1), s(z2)) → f46_out1(z1)
f45_in(z0) → U5(f46_in(z0), f47_in(z0), z0)
U5(f46_out1(z0), z1, z2) → f45_out1(z0)
U5(z0, f47_out1(z1, z2), z3) → f45_out2(z1, z2)
f77_in(z0) → U6(f46_in(z0), f79_in(z0), z0)
U6(f46_out1(z0), z1, z2) → f77_out1(z0)
U6(z0, f79_out1(z1, z2), z3) → f77_out2(z1, z2)

Tuples:

F1_IN(z0, z1) → c1(F7_IN(z0, z1))
F7_IN(s(z0), 0) → c1(F45_IN(z0))
F45_IN(z0) → c1(F46_IN(z0))
F7_IN(s(z0), s(z1)) → c6(F7_IN(z0, z1))
F46_IN(s(z0)) → c12(F77_IN(z0))
F77_IN(z0) → c18(F46_IN(z0))
F1_IN(z0, z1) → c1
F7_IN(s(z0), 0) → c1
F45_IN(z0) → c1

S tuples:

F7_IN(s(z0), 0) → c1(F45_IN(z0))
F45_IN(z0) → c1(F46_IN(z0))
F7_IN(s(z0), s(z1)) → c6(F7_IN(z0, z1))
F46_IN(s(z0)) → c12(F77_IN(z0))
F77_IN(z0) → c18(F46_IN(z0))
F7_IN(s(z0), 0) → c1
F45_IN(z0) → c1

K tuples:

F1_IN(z0, z1) → c1(F7_IN(z0, z1))
F1_IN(z0, z1) → c1

Defined Rule Symbols:

f1_in, U1, f7_in, U2, U3, f46_in, U4, f45_in, U5, f77_in, U6

Defined Pair Symbols:

F1_IN, F7_IN, F45_IN, F46_IN, F77_IN

Compound Symbols:

c1, c6, c12, c18, c1

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

F7_IN(s(z0), 0) → c1(F45_IN(z0))
F45_IN(z0) → c1(F46_IN(z0))
F7_IN(s(z0), 0) → c1
F45_IN(z0) → c1

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

F1_IN(z0, z1) → c1(F7_IN(z0, z1))
F7_IN(s(z0), 0) → c1(F45_IN(z0))
F45_IN(z0) → c1(F46_IN(z0))
F7_IN(s(z0), s(z1)) → c6(F7_IN(z0, z1))
F46_IN(s(z0)) → c12(F77_IN(z0))
F77_IN(z0) → c18(F46_IN(z0))
F1_IN(z0, z1) → c1
F7_IN(s(z0), 0) → c1
F45_IN(z0) → c1

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

POL(0) = [3]
POL(F1_IN(x₁, x₂)) = [1] + [3]x₁ + [2]x₂
POL(F45_IN(x₁)) = [3] + [3]x₁
POL(F46_IN(x₁)) = [1]
POL(F77_IN(x₁)) = [1]
POL(F7_IN(x₁, x₂)) = [1] + [3]x₁ + x₂
POL(c1) = 0
POL(c1(x₁)) = x₁
POL(c12(x₁)) = x₁
POL(c18(x₁)) = x₁
POL(c6(x₁)) = x₁
POL(s(x₁)) = x₁

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f7_in(z0, z1), z0, z1)
U1(f7_out1(z0), z1, z2) → f1_out1
f7_in(z0, 0) → f7_out1(z0)
f7_in(0, 0) → f7_out1(0)
f7_in(s(z0), 0) → U2(f45_in(z0), s(z0), 0)
f7_in(0, z0) → f7_out1(0)
f7_in(s(z0), s(z1)) → U3(f7_in(z0, z1), s(z0), s(z1))
U2(f45_out1(z0), s(z1), 0) → f7_out1(z0)
U2(f45_out2(z0, z1), s(z2), 0) → f7_out1(z1)
U3(f7_out1(z0), s(z1), s(z2)) → f7_out1(z0)
f46_in(z0) → f46_out1(z0)
f46_in(0) → f46_out1(0)
f46_in(s(z0)) → U4(f77_in(z0), s(z0))
U4(f77_out1(z0), s(z1)) → f46_out1(z0)
U4(f77_out2(z0, z1), s(z2)) → f46_out1(z1)
f45_in(z0) → U5(f46_in(z0), f47_in(z0), z0)
U5(f46_out1(z0), z1, z2) → f45_out1(z0)
U5(z0, f47_out1(z1, z2), z3) → f45_out2(z1, z2)
f77_in(z0) → U6(f46_in(z0), f79_in(z0), z0)
U6(f46_out1(z0), z1, z2) → f77_out1(z0)
U6(z0, f79_out1(z1, z2), z3) → f77_out2(z1, z2)

Tuples:

F1_IN(z0, z1) → c1(F7_IN(z0, z1))
F7_IN(s(z0), 0) → c1(F45_IN(z0))
F45_IN(z0) → c1(F46_IN(z0))
F7_IN(s(z0), s(z1)) → c6(F7_IN(z0, z1))
F46_IN(s(z0)) → c12(F77_IN(z0))
F77_IN(z0) → c18(F46_IN(z0))
F1_IN(z0, z1) → c1
F7_IN(s(z0), 0) → c1
F45_IN(z0) → c1

S tuples:

F7_IN(s(z0), s(z1)) → c6(F7_IN(z0, z1))
F46_IN(s(z0)) → c12(F77_IN(z0))
F77_IN(z0) → c18(F46_IN(z0))

K tuples:

F1_IN(z0, z1) → c1(F7_IN(z0, z1))
F1_IN(z0, z1) → c1
F7_IN(s(z0), 0) → c1(F45_IN(z0))
F45_IN(z0) → c1(F46_IN(z0))
F7_IN(s(z0), 0) → c1
F45_IN(z0) → c1

Defined Rule Symbols:

f1_in, U1, f7_in, U2, U3, f46_in, U4, f45_in, U5, f77_in, U6

Defined Pair Symbols:

F1_IN, F7_IN, F45_IN, F46_IN, F77_IN

Compound Symbols:

c1, c6, c12, c18, 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.

F7_IN(s(z0), s(z1)) → c6(F7_IN(z0, z1))
F46_IN(s(z0)) → c12(F77_IN(z0))
F77_IN(z0) → c18(F46_IN(z0))

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

F1_IN(z0, z1) → c1(F7_IN(z0, z1))
F7_IN(s(z0), 0) → c1(F45_IN(z0))
F45_IN(z0) → c1(F46_IN(z0))
F7_IN(s(z0), s(z1)) → c6(F7_IN(z0, z1))
F46_IN(s(z0)) → c12(F77_IN(z0))
F77_IN(z0) → c18(F46_IN(z0))
F1_IN(z0, z1) → c1
F7_IN(s(z0), 0) → c1
F45_IN(z0) → c1

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

POL(0) = 0
POL(F1_IN(x₁, x₂)) = [2] + [3]x₁
POL(F45_IN(x₁)) = [3] + [3]x₁
POL(F46_IN(x₁)) = [3]x₁
POL(F77_IN(x₁)) = [1] + [3]x₁
POL(F7_IN(x₁, x₂)) = [2] + [3]x₁
POL(c1) = 0
POL(c1(x₁)) = x₁
POL(c12(x₁)) = x₁
POL(c18(x₁)) = x₁
POL(c6(x₁)) = x₁
POL(s(x₁)) = [2] + x₁

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, z1) → U1(f7_in(z0, z1), z0, z1)
U1(f7_out1(z0), z1, z2) → f1_out1
f7_in(z0, 0) → f7_out1(z0)
f7_in(0, 0) → f7_out1(0)
f7_in(s(z0), 0) → U2(f45_in(z0), s(z0), 0)
f7_in(0, z0) → f7_out1(0)
f7_in(s(z0), s(z1)) → U3(f7_in(z0, z1), s(z0), s(z1))
U2(f45_out1(z0), s(z1), 0) → f7_out1(z0)
U2(f45_out2(z0, z1), s(z2), 0) → f7_out1(z1)
U3(f7_out1(z0), s(z1), s(z2)) → f7_out1(z0)
f46_in(z0) → f46_out1(z0)
f46_in(0) → f46_out1(0)
f46_in(s(z0)) → U4(f77_in(z0), s(z0))
U4(f77_out1(z0), s(z1)) → f46_out1(z0)
U4(f77_out2(z0, z1), s(z2)) → f46_out1(z1)
f45_in(z0) → U5(f46_in(z0), f47_in(z0), z0)
U5(f46_out1(z0), z1, z2) → f45_out1(z0)
U5(z0, f47_out1(z1, z2), z3) → f45_out2(z1, z2)
f77_in(z0) → U6(f46_in(z0), f79_in(z0), z0)
U6(f46_out1(z0), z1, z2) → f77_out1(z0)
U6(z0, f79_out1(z1, z2), z3) → f77_out2(z1, z2)

Tuples:

F1_IN(z0, z1) → c1(F7_IN(z0, z1))
F7_IN(s(z0), 0) → c1(F45_IN(z0))
F45_IN(z0) → c1(F46_IN(z0))
F7_IN(s(z0), s(z1)) → c6(F7_IN(z0, z1))
F46_IN(s(z0)) → c12(F77_IN(z0))
F77_IN(z0) → c18(F46_IN(z0))
F1_IN(z0, z1) → c1
F7_IN(s(z0), 0) → c1
F45_IN(z0) → c1

S tuples:none
K tuples:

F1_IN(z0, z1) → c1(F7_IN(z0, z1))
F1_IN(z0, z1) → c1
F7_IN(s(z0), 0) → c1(F45_IN(z0))
F45_IN(z0) → c1(F46_IN(z0))
F7_IN(s(z0), 0) → c1
F45_IN(z0) → c1
F7_IN(s(z0), s(z1)) → c6(F7_IN(z0, z1))
F46_IN(s(z0)) → c12(F77_IN(z0))
F77_IN(z0) → c18(F46_IN(z0))

Defined Rule Symbols:

f1_in, U1, f7_in, U2, U3, f46_in, U4, f45_in, U5, f77_in, U6

Defined Pair Symbols:

F1_IN, F7_IN, F45_IN, F46_IN, F77_IN

Compound Symbols:

c1, c6, c12, c18, 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)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
3 [label="3: q(T1, T2), SCOPE: 1, CLAUSE: 0\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: m(T5, T6, X5)\n\nT5 is ground\nT6 is ground\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: m(T5, T6, X5), SCOPE: 2, CLAUSE: 1 | m(T5, T6, X5), SCOPE: 2, CLAUSE: 2 | m(T5, T6, X5), SCOPE: 2, CLAUSE: 3\n\nT5 is ground\nT6 is ground\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: true | m(T9, 0, X5), SCOPE: 2, CLAUSE: 2 | m(T9, 0, X5), SCOPE: 2, CLAUSE: 3\n\nT9 is ground\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: m(T5, T6, X5), SCOPE: 2, CLAUSE: 2 | m(T5, T6, X5), SCOPE: 2, CLAUSE: 3\n\nT5 is ground\nT6 is ground\nX5 is free\nX8 is free\nm(T5, T6, X5) !=? m(X8, 0, X8)", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: m(T9, 0, X5), SCOPE: 2, CLAUSE: 2 | m(T9, 0, X5), SCOPE: 2, CLAUSE: 3\n\nT9 is ground\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: !_2 | m(0, 0, X5), SCOPE: 2, CLAUSE: 3\n\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: m(T9, 0, X5), SCOPE: 2, CLAUSE: 3\n\nT9 is ground\nX5 is free\nX11 is free\nm(T9, 0, X5) !=? m(0, X11, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(p(T12, X27), ','(p(0, X28), m(X27, X28, X29)))\n\nT12 is ground\nX5 is free\nX11 is free\nX29 is free\nX27 is free\nX28 is free\nm(T12, 0, X5) !=? m(0, X11, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: ','(p(T12, X27), ','(p(0, X28), m(X27, X28, X29))), SCOPE: 3, CLAUSE: 4 | ','(p(T12, X27), ','(p(0, X28), m(X27, X28, X29))), SCOPE: 3, CLAUSE: 5\n\nT12 is ground\nX5 is free\nX11 is free\nX29 is free\nX27 is free\nX28 is free\nm(T12, 0, X5) !=? m(0, X11, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: ','(p(T12, X27), ','(p(0, X28), m(X27, X28, X29))), SCOPE: 3, CLAUSE: 5\n\nT12 is ground\nX5 is free\nX11 is free\nX29 is free\nX27 is free\nX28 is free\nm(T12, 0, X5) !=? m(0, X11, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ','(p(0, X28), m(T15, X28, X29))\n\nT15 is ground\nX29 is free\nX28 is free", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: ','(p(0, X28), m(T15, X28, X29)), SCOPE: 4, CLAUSE: 4 | ','(p(0, X28), m(T15, X28, X29)), SCOPE: 4, CLAUSE: 5\n\nT15 is ground\nX29 is free\nX28 is free", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: m(T15, 0, X29) | ','(p(0, X28), m(T15, X28, X29)), SCOPE: 4, CLAUSE: 5\n\nT15 is ground\nX29 is free\nX28 is free", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: m(T15, 0, X29)\n\nT15 is ground\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: ','(p(0, X28), m(T15, X28, X29)), SCOPE: 4, CLAUSE: 5\n\nT15 is ground\nX29 is free\nX28 is free", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: m(T15, 0, X29), SCOPE: 5, CLAUSE: 1 | m(T15, 0, X29), SCOPE: 5, CLAUSE: 2 | m(T15, 0, X29), SCOPE: 5, CLAUSE: 3\n\nT15 is ground\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: true | m(T22, 0, X29), SCOPE: 5, CLAUSE: 2 | m(T22, 0, X29), SCOPE: 5, CLAUSE: 3\n\nT22 is ground\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: m(T22, 0, X29), SCOPE: 5, CLAUSE: 2 | m(T22, 0, X29), SCOPE: 5, CLAUSE: 3\n\nT22 is ground\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: !_5 | m(0, 0, X29), SCOPE: 5, CLAUSE: 3\n\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: m(T22, 0, X29), SCOPE: 5, CLAUSE: 3\n\nT22 is ground\nX29 is free\nX44 is free\nm(T22, 0, X29) !=? m(0, X44, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: ','(p(T25, X60), ','(p(0, X61), m(X60, X61, X62)))\n\nT25 is ground\nX29 is free\nX44 is free\nX62 is free\nX60 is free\nX61 is free\nm(T25, 0, X29) !=? m(0, X44, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ','(p(T25, X60), ','(p(0, X61), m(X60, X61, X62))), SCOPE: 6, CLAUSE: 4 | ','(p(T25, X60), ','(p(0, X61), m(X60, X61, X62))), SCOPE: 6, CLAUSE: 5\n\nT25 is ground\nX29 is free\nX44 is free\nX62 is free\nX60 is free\nX61 is free\nm(T25, 0, X29) !=? m(0, X44, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: ','(p(T25, X60), ','(p(0, X61), m(X60, X61, X62))), SCOPE: 6, CLAUSE: 5\n\nT25 is ground\nX29 is free\nX44 is free\nX62 is free\nX60 is free\nX61 is free\nm(T25, 0, X29) !=? m(0, X44, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: ','(p(0, X61), m(T28, X61, X62))\n\nT28 is ground\nX62 is free\nX61 is free", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: ','(p(0, X61), m(T28, X61, X62)), SCOPE: 7, CLAUSE: 4 | ','(p(0, X61), m(T28, X61, X62)), SCOPE: 7, CLAUSE: 5\n\nT28 is ground\nX62 is free\nX61 is free", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: m(T28, 0, X62) | ','(p(0, X61), m(T28, X61, X62)), SCOPE: 7, CLAUSE: 5\n\nT28 is ground\nX62 is free\nX61 is free", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: m(T28, 0, X62)\n\nT28 is ground\nX62 is free", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: ','(p(0, X61), m(T28, X61, X62)), SCOPE: 7, CLAUSE: 5\n\nT28 is ground\nX62 is free\nX61 is free", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: !_2 | m(0, T35, X5), SCOPE: 2, CLAUSE: 3\n\nT35 is ground\nX5 is free\nX8 is free\nm(0, T35, X5) !=? m(X8, 0, X8)", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: m(T5, T6, X5), SCOPE: 2, CLAUSE: 3\n\nT5 is ground\nT6 is ground\nX5 is free\nX8 is free\nX76 is free\nm(T5, T6, X5) !=? m(X8, 0, X8)\nm(T5, T6, X5) !=? m(0, X76, 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];
76 [label="76: ','(p(T40, X92), ','(p(T41, X93), m(X92, X93, X94)))\n\nT40 is ground\nT41 is ground\nX5 is free\nX8 is free\nX76 is free\nX94 is free\nX92 is free\nX93 is free\nm(T40, T41, X5) !=? m(X8, 0, X8)\nm(T40, T41, X5) !=? m(0, X76, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: ','(p(T40, X92), ','(p(T41, X93), m(X92, X93, X94))), SCOPE: 8, CLAUSE: 4 | ','(p(T40, X92), ','(p(T41, X93), m(X92, X93, X94))), SCOPE: 8, CLAUSE: 5\n\nT40 is ground\nT41 is ground\nX5 is free\nX8 is free\nX76 is free\nX94 is free\nX92 is free\nX93 is free\nm(T40, T41, X5) !=? m(X8, 0, X8)\nm(T40, T41, X5) !=? m(0, X76, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: ','(p(T40, X92), ','(p(T41, X93), m(X92, X93, X94))), SCOPE: 8, CLAUSE: 5\n\nT40 is ground\nT41 is ground\nX5 is free\nX8 is free\nX76 is free\nX94 is free\nX92 is free\nX93 is free\nm(T40, T41, X5) !=? m(X8, 0, X8)\nm(T40, T41, X5) !=? m(0, X76, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: ','(p(T41, X93), m(T44, X93, X94))\n\nT41 is ground\nT44 is ground\nX5 is free\nX8 is free\nX94 is free\nX93 is free\nm(s(T44), T41, X5) !=? m(X8, 0, X8)", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: ','(p(T41, X93), m(T44, X93, X94)), SCOPE: 9, CLAUSE: 4 | ','(p(T41, X93), m(T44, X93, X94)), SCOPE: 9, CLAUSE: 5\n\nT41 is ground\nT44 is ground\nX5 is free\nX8 is free\nX94 is free\nX93 is free\nm(s(T44), T41, X5) !=? m(X8, 0, X8)", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: ','(p(T41, X93), m(T44, X93, X94)), SCOPE: 9, CLAUSE: 5\n\nT41 is ground\nT44 is ground\nX5 is free\nX8 is free\nX94 is free\nX93 is free\nm(s(T44), T41, X5) !=? m(X8, 0, X8)", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: m(T44, T48, X94)\n\nT44 is ground\nT48 is ground\nX94 is free", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 94 [arrowhead = none ];
94 -> 3;

95 [label="ONLY EVAL with clause\nq(X3, X4) :- m(X3, X4, X5).\nand substitutionT1 -> T5,\nX3 -> T5,\nT2 -> T6,\nX4 -> T6", fontsize=14, style = filled, fillcolor = lightblue];
3 -> 95 [arrowhead = none ];
95 -> 5;

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

97 [label="EVAL with clause\nm(X8, 0, X8).\nand substitutionT5 -> T9,\nX8 -> T9,\nT6 -> 0,\nX5 -> T9", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 97 [arrowhead = none ];
97 -> 8;

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

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

100 [label="EVAL with clause\nm(0, X76, 0) :- !_2.\nand substitutionT5 -> 0,\nT6 -> T35,\nX76 -> T35,\nX5 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
9 -> 100 [arrowhead = none ];
100 -> 66;

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

102 [label="EVAL with clause\nm(0, X11, 0) :- !_2.\nand substitutionT9 -> 0,\nX11 -> 0,\nX5 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 102 [arrowhead = none ];
102 -> 11;

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

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

105 [label="ONLY EVAL with clause\nm(X24, X25, X26) :- ','(p(X24, X27), ','(p(X25, X28), m(X27, X28, X26))).\nand substitutionT9 -> T12,\nX24 -> T12,\nX25 -> 0,\nX5 -> X29,\nX26 -> X29", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 105 [arrowhead = none ];
105 -> 19;

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

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

108 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (m(T12, 0, X5), m(0, X11, 0))", fontsize=14, style = filled, fillcolor = lightgreen];
24 -> 108 [arrowhead = none ];
108 -> 25;

109 [label="EVAL with clause\np(s(X34), X34).\nand substitutionX34 -> T15,\nT12 -> s(T15),\nX27 -> T15", fontsize=14, style = filled, fillcolor = lightblue];
25 -> 109 [arrowhead = none ];
109 -> 26;

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

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

112 [label="ONLY EVAL with clause\np(0, 0).\nand substitutionX28 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
29 -> 112 [arrowhead = none ];
112 -> 30;

113 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
30 -> 113 [arrowhead = none ];
113 -> 32;

114 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
30 -> 114 [arrowhead = none ];
114 -> 33;

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

116 [label="BACKTRACK\nfor clause: p(s(X), X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
33 -> 116 [arrowhead = none ];
116 -> 65;

117 [label="ONLY EVAL with clause\nm(X41, 0, X41).\nand substitutionT15 -> T22,\nX41 -> T22,\nX29 -> T22", fontsize=14, style = filled, fillcolor = lightblue];
34 -> 117 [arrowhead = none ];
117 -> 36;

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

119 [label="EVAL with clause\nm(0, X44, 0) :- !_5.\nand substitutionT22 -> 0,\nX44 -> 0,\nX29 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
37 -> 119 [arrowhead = none ];
119 -> 40;

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

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

122 [label="ONLY EVAL with clause\nm(X57, X58, X59) :- ','(p(X57, X60), ','(p(X58, X61), m(X60, X61, X59))).\nand substitutionT22 -> T25,\nX57 -> T25,\nX58 -> 0,\nX29 -> X62,\nX59 -> X62", fontsize=14, style = filled, fillcolor = lightblue];
41 -> 122 [arrowhead = none ];
122 -> 48;

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

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

125 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (m(T25, 0, X29), m(0, X44, 0))", fontsize=14, style = filled, fillcolor = lightgreen];
49 -> 125 [arrowhead = none ];
125 -> 50;

126 [label="EVAL with clause\np(s(X67), X67).\nand substitutionX67 -> T28,\nT25 -> s(T28),\nX60 -> T28", fontsize=14, style = filled, fillcolor = lightblue];
50 -> 126 [arrowhead = none ];
126 -> 51;

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

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

129 [label="ONLY EVAL with clause\np(0, 0).\nand substitutionX61 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
53 -> 129 [arrowhead = none ];
129 -> 55;

130 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
55 -> 130 [arrowhead = none ];
130 -> 58;

131 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
55 -> 131 [arrowhead = none ];
131 -> 59;

132 [label="INSTANCE with matching:\nT15 -> T28\nX29 -> X62", fontsize=14, style = filled, fillcolor = lightgrey];
58 -> 132 [arrowhead = none , style=dashed];
132 -> 32[style=dashed];

133 [label="BACKTRACK\nfor clause: p(s(X), X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
59 -> 133 [arrowhead = none ];
133 -> 64;

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

135 [label="ONLY EVAL with clause\nm(X89, X90, X91) :- ','(p(X89, X92), ','(p(X90, X93), m(X92, X93, X91))).\nand substitutionT5 -> T40,\nX89 -> T40,\nT6 -> T41,\nX90 -> T41,\nX5 -> X94,\nX91 -> X94", fontsize=14, style = filled, fillcolor = lightblue];
67 -> 135 [arrowhead = none ];
135 -> 76;

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

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

138 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (m(T40, T41, X5), m(0, X76, 0))", fontsize=14, style = filled, fillcolor = lightgreen];
80 -> 138 [arrowhead = none ];
138 -> 81;

139 [label="EVAL with clause\np(s(X99), X99).\nand substitutionX99 -> T44,\nT40 -> s(T44),\nX92 -> T44", fontsize=14, style = filled, fillcolor = lightblue];
81 -> 139 [arrowhead = none ];
139 -> 84;

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

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

142 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (m(s(T44), T41, X5), m(X8, 0, X8))", fontsize=14, style = filled, fillcolor = lightgreen];
90 -> 142 [arrowhead = none ];
142 -> 91;

143 [label="EVAL with clause\np(s(X103), X103).\nand substitutionX103 -> T48,\nT41 -> s(T48),\nX93 -> T48", fontsize=14, style = filled, fillcolor = lightblue];
91 -> 143 [arrowhead = none ];
143 -> 92;

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

145 [label="INSTANCE with matching:\nT5 -> T44\nT6 -> T48\nX5 -> X94", fontsize=14, style = filled, fillcolor = lightgrey];
92 -> 145 [arrowhead = none , style=dashed];
145 -> 5[style=dashed];

}

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, z1) → U1(f5_in(z0, z1), z0, z1)
U1(f5_out1(z0), z1, z2) → f2_out1
f5_in(z0, 0) → f5_out1(z0)
f5_in(0, 0) → f5_out1(0)
f5_in(s(z0), 0) → U2(f30_in(z0), s(z0), 0)
f5_in(0, z0) → f5_out1(0)
f5_in(s(z0), s(z1)) → U3(f5_in(z0, z1), s(z0), s(z1))
U2(f30_out1(z0), s(z1), 0) → f5_out1(z0)
U2(f30_out2(z0, z1), s(z2), 0) → f5_out1(z1)
U3(f5_out1(z0), s(z1), s(z2)) → f5_out1(z0)
f32_in(z0) → f32_out1(z0)
f32_in(0) → f32_out1(0)
f32_in(s(z0)) → U4(f55_in(z0), s(z0))
U4(f55_out1(z0), s(z1)) → f32_out1(z0)
U4(f55_out2(z0, z1), s(z2)) → f32_out1(z1)
f30_in(z0) → U5(f32_in(z0), f33_in(z0), z0)
U5(f32_out1(z0), z1, z2) → f30_out1(z0)
U5(z0, f33_out1(z1, z2), z3) → f30_out2(z1, z2)
f55_in(z0) → U6(f32_in(z0), f59_in(z0), z0)
U6(f32_out1(z0), z1, z2) → f55_out1(z0)
U6(z0, f59_out1(z1, z2), z3) → f55_out2(z1, z2)

Tuples:

F2_IN(z0, z1) → c(U1'(f5_in(z0, z1), z0, z1), F5_IN(z0, z1))
F5_IN(s(z0), 0) → c4(U2'(f30_in(z0), s(z0), 0), F30_IN(z0))
F5_IN(s(z0), s(z1)) → c6(U3'(f5_in(z0, z1), s(z0), s(z1)), F5_IN(z0, z1))
F32_IN(s(z0)) → c12(U4'(f55_in(z0), s(z0)), F55_IN(z0))
F30_IN(z0) → c15(U5'(f32_in(z0), f33_in(z0), z0), F32_IN(z0))
F55_IN(z0) → c18(U6'(f32_in(z0), f59_in(z0), z0), F32_IN(z0))

S tuples:

F2_IN(z0, z1) → c(U1'(f5_in(z0, z1), z0, z1), F5_IN(z0, z1))
F5_IN(s(z0), 0) → c4(U2'(f30_in(z0), s(z0), 0), F30_IN(z0))
F5_IN(s(z0), s(z1)) → c6(U3'(f5_in(z0, z1), s(z0), s(z1)), F5_IN(z0, z1))
F32_IN(s(z0)) → c12(U4'(f55_in(z0), s(z0)), F55_IN(z0))
F30_IN(z0) → c15(U5'(f32_in(z0), f33_in(z0), z0), F32_IN(z0))
F55_IN(z0) → c18(U6'(f32_in(z0), f59_in(z0), z0), F32_IN(z0))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f5_in, U2, U3, f32_in, U4, f30_in, U5, f55_in, U6

Defined Pair Symbols:

F2_IN, F5_IN, F32_IN, F30_IN, F55_IN

Compound Symbols:

c, c4, c6, c12, c15, c18

(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, z1) → U1(f5_in(z0, z1), z0, z1)
U1(f5_out1(z0), z1, z2) → f2_out1
f5_in(z0, 0) → f5_out1(z0)
f5_in(0, 0) → f5_out1(0)
f5_in(s(z0), 0) → U2(f30_in(z0), s(z0), 0)
f5_in(0, z0) → f5_out1(0)
f5_in(s(z0), s(z1)) → U3(f5_in(z0, z1), s(z0), s(z1))
U2(f30_out1(z0), s(z1), 0) → f5_out1(z0)
U2(f30_out2(z0, z1), s(z2), 0) → f5_out1(z1)
U3(f5_out1(z0), s(z1), s(z2)) → f5_out1(z0)
f32_in(z0) → f32_out1(z0)
f32_in(0) → f32_out1(0)
f32_in(s(z0)) → U4(f55_in(z0), s(z0))
U4(f55_out1(z0), s(z1)) → f32_out1(z0)
U4(f55_out2(z0, z1), s(z2)) → f32_out1(z1)
f30_in(z0) → U5(f32_in(z0), f33_in(z0), z0)
U5(f32_out1(z0), z1, z2) → f30_out1(z0)
U5(z0, f33_out1(z1, z2), z3) → f30_out2(z1, z2)
f55_in(z0) → U6(f32_in(z0), f59_in(z0), z0)
U6(f32_out1(z0), z1, z2) → f55_out1(z0)
U6(z0, f59_out1(z1, z2), z3) → f55_out2(z1, z2)

Tuples:

F5_IN(s(z0), s(z1)) → c6(U3'(f5_in(z0, z1), s(z0), s(z1)), F5_IN(z0, z1))
F32_IN(s(z0)) → c12(U4'(f55_in(z0), s(z0)), F55_IN(z0))
F55_IN(z0) → c18(U6'(f32_in(z0), f59_in(z0), z0), F32_IN(z0))
F2_IN(z0, z1) → c1(U1'(f5_in(z0, z1), z0, z1))
F2_IN(z0, z1) → c1(F5_IN(z0, z1))
F5_IN(s(z0), 0) → c1(U2'(f30_in(z0), s(z0), 0))
F5_IN(s(z0), 0) → c1(F30_IN(z0))
F30_IN(z0) → c1(U5'(f32_in(z0), f33_in(z0), z0))
F30_IN(z0) → c1(F32_IN(z0))

S tuples:

F5_IN(s(z0), s(z1)) → c6(U3'(f5_in(z0, z1), s(z0), s(z1)), F5_IN(z0, z1))
F32_IN(s(z0)) → c12(U4'(f55_in(z0), s(z0)), F55_IN(z0))
F55_IN(z0) → c18(U6'(f32_in(z0), f59_in(z0), z0), F32_IN(z0))
F2_IN(z0, z1) → c1(U1'(f5_in(z0, z1), z0, z1))
F2_IN(z0, z1) → c1(F5_IN(z0, z1))
F5_IN(s(z0), 0) → c1(U2'(f30_in(z0), s(z0), 0))
F5_IN(s(z0), 0) → c1(F30_IN(z0))
F30_IN(z0) → c1(U5'(f32_in(z0), f33_in(z0), z0))
F30_IN(z0) → c1(F32_IN(z0))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f5_in, U2, U3, f32_in, U4, f30_in, U5, f55_in, U6

Defined Pair Symbols:

F5_IN, F32_IN, F55_IN, F2_IN, F30_IN

Compound Symbols:

c6, c12, c18, c1

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

Removed 6 trailing tuple parts

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, z1) → U1(f5_in(z0, z1), z0, z1)
U1(f5_out1(z0), z1, z2) → f2_out1
f5_in(z0, 0) → f5_out1(z0)
f5_in(0, 0) → f5_out1(0)
f5_in(s(z0), 0) → U2(f30_in(z0), s(z0), 0)
f5_in(0, z0) → f5_out1(0)
f5_in(s(z0), s(z1)) → U3(f5_in(z0, z1), s(z0), s(z1))
U2(f30_out1(z0), s(z1), 0) → f5_out1(z0)
U2(f30_out2(z0, z1), s(z2), 0) → f5_out1(z1)
U3(f5_out1(z0), s(z1), s(z2)) → f5_out1(z0)
f32_in(z0) → f32_out1(z0)
f32_in(0) → f32_out1(0)
f32_in(s(z0)) → U4(f55_in(z0), s(z0))
U4(f55_out1(z0), s(z1)) → f32_out1(z0)
U4(f55_out2(z0, z1), s(z2)) → f32_out1(z1)
f30_in(z0) → U5(f32_in(z0), f33_in(z0), z0)
U5(f32_out1(z0), z1, z2) → f30_out1(z0)
U5(z0, f33_out1(z1, z2), z3) → f30_out2(z1, z2)
f55_in(z0) → U6(f32_in(z0), f59_in(z0), z0)
U6(f32_out1(z0), z1, z2) → f55_out1(z0)
U6(z0, f59_out1(z1, z2), z3) → f55_out2(z1, z2)

Tuples:

F2_IN(z0, z1) → c1(F5_IN(z0, z1))
F5_IN(s(z0), 0) → c1(F30_IN(z0))
F30_IN(z0) → c1(F32_IN(z0))
F5_IN(s(z0), s(z1)) → c6(F5_IN(z0, z1))
F32_IN(s(z0)) → c12(F55_IN(z0))
F55_IN(z0) → c18(F32_IN(z0))
F2_IN(z0, z1) → c1
F5_IN(s(z0), 0) → c1
F30_IN(z0) → c1

S tuples:

F2_IN(z0, z1) → c1(F5_IN(z0, z1))
F5_IN(s(z0), 0) → c1(F30_IN(z0))
F30_IN(z0) → c1(F32_IN(z0))
F5_IN(s(z0), s(z1)) → c6(F5_IN(z0, z1))
F32_IN(s(z0)) → c12(F55_IN(z0))
F55_IN(z0) → c18(F32_IN(z0))
F2_IN(z0, z1) → c1
F5_IN(s(z0), 0) → c1
F30_IN(z0) → c1

K tuples:none
Defined Rule Symbols:

f2_in, U1, f5_in, U2, U3, f32_in, U4, f30_in, U5, f55_in, U6

Defined Pair Symbols:

F2_IN, F5_IN, F30_IN, F32_IN, F55_IN

Compound Symbols:

c1, c6, c12, c18, c1

(21) CdtKnowledgeProof (EQUIVALENT transformation)

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

F2_IN(z0, z1) → c1(F5_IN(z0, z1))
F2_IN(z0, z1) → c1

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, z1) → U1(f5_in(z0, z1), z0, z1)
U1(f5_out1(z0), z1, z2) → f2_out1
f5_in(z0, 0) → f5_out1(z0)
f5_in(0, 0) → f5_out1(0)
f5_in(s(z0), 0) → U2(f30_in(z0), s(z0), 0)
f5_in(0, z0) → f5_out1(0)
f5_in(s(z0), s(z1)) → U3(f5_in(z0, z1), s(z0), s(z1))
U2(f30_out1(z0), s(z1), 0) → f5_out1(z0)
U2(f30_out2(z0, z1), s(z2), 0) → f5_out1(z1)
U3(f5_out1(z0), s(z1), s(z2)) → f5_out1(z0)
f32_in(z0) → f32_out1(z0)
f32_in(0) → f32_out1(0)
f32_in(s(z0)) → U4(f55_in(z0), s(z0))
U4(f55_out1(z0), s(z1)) → f32_out1(z0)
U4(f55_out2(z0, z1), s(z2)) → f32_out1(z1)
f30_in(z0) → U5(f32_in(z0), f33_in(z0), z0)
U5(f32_out1(z0), z1, z2) → f30_out1(z0)
U5(z0, f33_out1(z1, z2), z3) → f30_out2(z1, z2)
f55_in(z0) → U6(f32_in(z0), f59_in(z0), z0)
U6(f32_out1(z0), z1, z2) → f55_out1(z0)
U6(z0, f59_out1(z1, z2), z3) → f55_out2(z1, z2)

Tuples:

F2_IN(z0, z1) → c1(F5_IN(z0, z1))
F5_IN(s(z0), 0) → c1(F30_IN(z0))
F30_IN(z0) → c1(F32_IN(z0))
F5_IN(s(z0), s(z1)) → c6(F5_IN(z0, z1))
F32_IN(s(z0)) → c12(F55_IN(z0))
F55_IN(z0) → c18(F32_IN(z0))
F2_IN(z0, z1) → c1
F5_IN(s(z0), 0) → c1
F30_IN(z0) → c1

S tuples:

F5_IN(s(z0), 0) → c1(F30_IN(z0))
F30_IN(z0) → c1(F32_IN(z0))
F5_IN(s(z0), s(z1)) → c6(F5_IN(z0, z1))
F32_IN(s(z0)) → c12(F55_IN(z0))
F55_IN(z0) → c18(F32_IN(z0))
F5_IN(s(z0), 0) → c1
F30_IN(z0) → c1

K tuples:

F2_IN(z0, z1) → c1(F5_IN(z0, z1))
F2_IN(z0, z1) → c1

Defined Rule Symbols:

f2_in, U1, f5_in, U2, U3, f32_in, U4, f30_in, U5, f55_in, U6

Defined Pair Symbols:

F2_IN, F5_IN, F30_IN, F32_IN, F55_IN

Compound Symbols:

c1, c6, c12, c18, 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.

F5_IN(s(z0), 0) → c1(F30_IN(z0))
F30_IN(z0) → c1(F32_IN(z0))
F5_IN(s(z0), 0) → c1
F30_IN(z0) → c1

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

F2_IN(z0, z1) → c1(F5_IN(z0, z1))
F5_IN(s(z0), 0) → c1(F30_IN(z0))
F30_IN(z0) → c1(F32_IN(z0))
F5_IN(s(z0), s(z1)) → c6(F5_IN(z0, z1))
F32_IN(s(z0)) → c12(F55_IN(z0))
F55_IN(z0) → c18(F32_IN(z0))
F2_IN(z0, z1) → c1
F5_IN(s(z0), 0) → c1
F30_IN(z0) → c1

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

POL(0) = [3]
POL(F2_IN(x₁, x₂)) = [1] + [3]x₁ + [2]x₂
POL(F30_IN(x₁)) = [3] + [3]x₁
POL(F32_IN(x₁)) = [1]
POL(F55_IN(x₁)) = [1]
POL(F5_IN(x₁, x₂)) = [1] + [3]x₁ + x₂
POL(c1) = 0
POL(c1(x₁)) = x₁
POL(c12(x₁)) = x₁
POL(c18(x₁)) = x₁
POL(c6(x₁)) = x₁
POL(s(x₁)) = x₁

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, z1) → U1(f5_in(z0, z1), z0, z1)
U1(f5_out1(z0), z1, z2) → f2_out1
f5_in(z0, 0) → f5_out1(z0)
f5_in(0, 0) → f5_out1(0)
f5_in(s(z0), 0) → U2(f30_in(z0), s(z0), 0)
f5_in(0, z0) → f5_out1(0)
f5_in(s(z0), s(z1)) → U3(f5_in(z0, z1), s(z0), s(z1))
U2(f30_out1(z0), s(z1), 0) → f5_out1(z0)
U2(f30_out2(z0, z1), s(z2), 0) → f5_out1(z1)
U3(f5_out1(z0), s(z1), s(z2)) → f5_out1(z0)
f32_in(z0) → f32_out1(z0)
f32_in(0) → f32_out1(0)
f32_in(s(z0)) → U4(f55_in(z0), s(z0))
U4(f55_out1(z0), s(z1)) → f32_out1(z0)
U4(f55_out2(z0, z1), s(z2)) → f32_out1(z1)
f30_in(z0) → U5(f32_in(z0), f33_in(z0), z0)
U5(f32_out1(z0), z1, z2) → f30_out1(z0)
U5(z0, f33_out1(z1, z2), z3) → f30_out2(z1, z2)
f55_in(z0) → U6(f32_in(z0), f59_in(z0), z0)
U6(f32_out1(z0), z1, z2) → f55_out1(z0)
U6(z0, f59_out1(z1, z2), z3) → f55_out2(z1, z2)

Tuples:

F2_IN(z0, z1) → c1(F5_IN(z0, z1))
F5_IN(s(z0), 0) → c1(F30_IN(z0))
F30_IN(z0) → c1(F32_IN(z0))
F5_IN(s(z0), s(z1)) → c6(F5_IN(z0, z1))
F32_IN(s(z0)) → c12(F55_IN(z0))
F55_IN(z0) → c18(F32_IN(z0))
F2_IN(z0, z1) → c1
F5_IN(s(z0), 0) → c1
F30_IN(z0) → c1

S tuples:

F5_IN(s(z0), s(z1)) → c6(F5_IN(z0, z1))
F32_IN(s(z0)) → c12(F55_IN(z0))
F55_IN(z0) → c18(F32_IN(z0))

K tuples:

F2_IN(z0, z1) → c1(F5_IN(z0, z1))
F2_IN(z0, z1) → c1
F5_IN(s(z0), 0) → c1(F30_IN(z0))
F30_IN(z0) → c1(F32_IN(z0))
F5_IN(s(z0), 0) → c1
F30_IN(z0) → c1

Defined Rule Symbols:

f2_in, U1, f5_in, U2, U3, f32_in, U4, f30_in, U5, f55_in, U6

Defined Pair Symbols:

F2_IN, F5_IN, F30_IN, F32_IN, F55_IN

Compound Symbols:

c1, c6, c12, c18, c1