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

(0) Obligation:

Clauses:

delete(X, tree(X, void, Right), Right).
delete(X, tree(X, Left, void), Left).
delete(X, tree(X, Left, Right), tree(Y, Left, Right1)) :- delmin(Right, Y, Right1).
delete(X, tree(Y, Left, Right), tree(Y, Left1, Right)) :- ','(less(X, Y), delete(X, Left, Left1)).
delete(X, tree(Y, Left, Right), tree(Y, Left, Right1)) :- ','(less(Y, X), delete(X, Right, Right1)).
delmin(tree(Y, void, Right), Y, Right).
delmin(tree(X, Left, X1), Y, tree(X, Left1, X2)) :- delmin(Left, Y, Left1).
less(0, s(X3)).
less(s(X), s(Y)) :- less(X, Y).

Query: delmin(a,a,g)

(1) LPReorderTransformerProof (EQUIVALENT transformation)

Reordered facts before rules in definite LP [PROLOG].

(2) Obligation:

Clauses:

delete(X, tree(X, void, Right), Right).
delete(X, tree(X, Left, void), Left).
delmin(tree(Y, void, Right), Y, Right).
less(0, s(X3)).
delete(X, tree(X, Left, Right), tree(Y, Left, Right1)) :- delmin(Right, Y, Right1).
delete(X, tree(Y, Left, Right), tree(Y, Left1, Right)) :- ','(less(X, Y), delete(X, Left, Left1)).
delete(X, tree(Y, Left, Right), tree(Y, Left, Right1)) :- ','(less(Y, X), delete(X, Right, Right1)).
delmin(tree(X, Left, X1), Y, tree(X, Left1, X2)) :- delmin(Left, Y, Left1).
less(s(X), s(Y)) :- less(X, Y).

Query: delmin(a,a,g)

(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: delmin(T1, T2, T3)\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
3 [label="3: delmin(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | delmin(T1, T2, T3), SCOPE: 1, CLAUSE: 7\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: true | delmin(T1, T2, T9), SCOPE: 1, CLAUSE: 7\n\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: delmin(T1, T2, T3), SCOPE: 1, CLAUSE: 7\n\nT3 is ground\nX8 is free\nX9 is free\ndelmin(T1, T2, T3) !=? delmin(tree(X8, void, X9), X8, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: delmin(T1, T2, T9), SCOPE: 1, CLAUSE: 7\n\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: delmin(T28, T29, T26)\n\nT26 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: delmin(T52, T53, T50)\n\nT46 is ground\nT50 is ground\nT51 is ground\nX8 is free\nX9 is free\ndelmin(T1, T2, tree(T46, T50, T51)) !=? delmin(tree(X8, void, X9), X8, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 23 [arrowhead = none ];
23 -> 3;

24 [label="EVAL with clause\ndelmin(tree(X8, void, X9), X8, X9).\nand substitutionX8 -> T8,\nX9 -> T9,\nT1 -> tree(T8, void, T9),\nT2 -> T8,\nT3 -> T9", fontsize=14, style = filled, fillcolor = lightblue];
3 -> 24 [arrowhead = none ];
24 -> 6;

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

26 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
6 -> 26 [arrowhead = none ];
26 -> 9;

27 [label="EVAL with clause\ndelmin(tree(X44, X45, X46), X47, tree(X44, X48, X49)) :- delmin(X45, X47, X48).\nand substitutionX44 -> T46,\nX45 -> T52,\nX46 -> T48,\nT1 -> tree(T46, T52, T48),\nT2 -> T53,\nX47 -> T53,\nX48 -> T50,\nX49 -> T51,\nT3 -> tree(T46, T50, T51),\nT47 -> T52,\nT49 -> T53", fontsize=14, style = filled, fillcolor = lightblue];
8 -> 27 [arrowhead = none ];
27 -> 21;

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

29 [label="EVAL with clause\ndelmin(tree(X22, X23, X24), X25, tree(X22, X26, X27)) :- delmin(X23, X25, X26).\nand substitutionX22 -> T22,\nX23 -> T28,\nX24 -> T24,\nT1 -> tree(T22, T28, T24),\nT2 -> T29,\nX25 -> T29,\nX26 -> T26,\nX27 -> T27,\nT9 -> tree(T22, T26, T27),\nT23 -> T28,\nT25 -> T29", fontsize=14, style = filled, fillcolor = lightblue];
9 -> 29 [arrowhead = none ];
29 -> 17;

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

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

32 [label="INSTANCE with matching:\nT1 -> T52\nT2 -> T53\nT3 -> T50", fontsize=14, style = filled, fillcolor = lightgrey];
21 -> 32 [arrowhead = none , style=dashed];
32 -> 1[style=dashed];

}

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0) → f1_out1
f1_in(tree(z0, z1, z2)) → U1(f1_in(z1), tree(z0, z1, z2))
f1_in(tree(z0, z1, z2)) → U2(f1_in(z1), tree(z0, z1, z2))
U1(f1_out1, tree(z0, z1, z2)) → f1_out1
U2(f1_out1, tree(z0, z1, z2)) → f1_out1

Tuples:

F1_IN(tree(z0, z1, z2)) → c1(U1'(f1_in(z1), tree(z0, z1, z2)), F1_IN(z1))
F1_IN(tree(z0, z1, z2)) → c2(U2'(f1_in(z1), tree(z0, z1, z2)), F1_IN(z1))

S tuples:

F1_IN(tree(z0, z1, z2)) → c1(U1'(f1_in(z1), tree(z0, z1, z2)), F1_IN(z1))
F1_IN(tree(z0, z1, z2)) → c2(U2'(f1_in(z1), tree(z0, z1, z2)), F1_IN(z1))

K tuples:none
Defined Rule Symbols:

f1_in, U1, U2

Defined Pair Symbols:

F1_IN

Compound Symbols:

c1, c2

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

Removed 2 trailing tuple parts

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0) → f1_out1
f1_in(tree(z0, z1, z2)) → U1(f1_in(z1), tree(z0, z1, z2))
f1_in(tree(z0, z1, z2)) → U2(f1_in(z1), tree(z0, z1, z2))
U1(f1_out1, tree(z0, z1, z2)) → f1_out1
U2(f1_out1, tree(z0, z1, z2)) → f1_out1

Tuples:

F1_IN(tree(z0, z1, z2)) → c1(F1_IN(z1))
F1_IN(tree(z0, z1, z2)) → c2(F1_IN(z1))

S tuples:

F1_IN(tree(z0, z1, z2)) → c1(F1_IN(z1))
F1_IN(tree(z0, z1, z2)) → c2(F1_IN(z1))

K tuples:none
Defined Rule Symbols:

f1_in, U1, U2

Defined Pair Symbols:

F1_IN

Compound Symbols:

c1, c2

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

F1_IN(tree(z0, z1, z2)) → c1(F1_IN(z1))
F1_IN(tree(z0, z1, z2)) → c2(F1_IN(z1))

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

F1_IN(tree(z0, z1, z2)) → c1(F1_IN(z1))
F1_IN(tree(z0, z1, z2)) → c2(F1_IN(z1))

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

POL(F1_IN(x₁)) = x₁   
POL(c1(x₁)) = x₁   
POL(c2(x₁)) = x₁   
POL(tree(x₁, x₂, x₃)) = [2] + x₂   

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0) → f1_out1
f1_in(tree(z0, z1, z2)) → U1(f1_in(z1), tree(z0, z1, z2))
f1_in(tree(z0, z1, z2)) → U2(f1_in(z1), tree(z0, z1, z2))
U1(f1_out1, tree(z0, z1, z2)) → f1_out1
U2(f1_out1, tree(z0, z1, z2)) → f1_out1

Tuples:

F1_IN(tree(z0, z1, z2)) → c1(F1_IN(z1))
F1_IN(tree(z0, z1, z2)) → c2(F1_IN(z1))

S tuples:none
K tuples:

F1_IN(tree(z0, z1, z2)) → c1(F1_IN(z1))
F1_IN(tree(z0, z1, z2)) → c2(F1_IN(z1))

Defined Rule Symbols:

f1_in, U1, U2

Defined Pair Symbols:

F1_IN

Compound Symbols:

c1, c2

(9) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(10) BOUNDS(O(1), O(1))

(11) 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: delmin(T1, T2, T3)\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: delmin(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | delmin(T1, T2, T3), SCOPE: 1, CLAUSE: 7\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: true | delmin(T1, T2, T7), SCOPE: 1, CLAUSE: 7\n\nT7 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: delmin(T1, T2, T3), SCOPE: 1, CLAUSE: 7\n\nT3 is ground\nX6 is free\nX7 is free\ndelmin(T1, T2, T3) !=? delmin(tree(X6, void, X7), X6, X7)", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: delmin(T1, T2, T7), SCOPE: 1, CLAUSE: 7\n\nT7 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: delmin(T20, T21, T18)\n\nT18 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: delmin(T20, T21, T18), SCOPE: 2, CLAUSE: 2 | delmin(T20, T21, T18), SCOPE: 2, CLAUSE: 7\n\nT18 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: true | delmin(T20, T21, T27), SCOPE: 2, CLAUSE: 7\n\nT27 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: delmin(T20, T21, T18), SCOPE: 2, CLAUSE: 7\n\nT18 is ground\nX24 is free\nX25 is free\ndelmin(T20, T21, T18) !=? delmin(tree(X24, void, X25), X24, X25)", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: delmin(T20, T21, T27), SCOPE: 2, CLAUSE: 7\n\nT27 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: delmin(T46, T47, T44)\n\nT44 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: delmin(T70, T71, T68)\n\nT64 is ground\nT68 is ground\nT69 is ground\nX24 is free\nX25 is free\ndelmin(T20, T21, tree(T64, T68, T69)) !=? delmin(tree(X24, void, X25), X24, X25)", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: delmin(T88, T89, T86)\n\nT82 is ground\nT86 is ground\nT87 is ground\nX6 is free\nX7 is free\ndelmin(T1, T2, tree(T82, T86, T87)) !=? delmin(tree(X6, void, X7), X6, X7)", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: delmin(T88, T89, T86), SCOPE: 3, CLAUSE: 2 | delmin(T88, T89, T86), SCOPE: 3, CLAUSE: 7\n\nT82 is ground\nT86 is ground\nT87 is ground\nX6 is free\nX7 is free\ndelmin(T1, T2, tree(T82, T86, T87)) !=? delmin(tree(X6, void, X7), X6, X7)", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: true | delmin(T88, T89, T95), SCOPE: 3, CLAUSE: 7\n\nT82 is ground\nT87 is ground\nT95 is ground\nX6 is free\nX7 is free\ndelmin(T1, T2, tree(T82, T95, T87)) !=? delmin(tree(X6, void, X7), X6, X7)", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: delmin(T88, T89, T86), SCOPE: 3, CLAUSE: 7\n\nT82 is ground\nT86 is ground\nT87 is ground\nX6 is free\nX7 is free\nX86 is free\nX87 is free\ndelmin(T1, T2, tree(T82, T86, T87)) !=? delmin(tree(X6, void, X7), X6, X7)\ndelmin(T88, T89, T86) !=? delmin(tree(X86, void, X87), X86, X87)", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: delmin(T88, T89, T95), SCOPE: 3, CLAUSE: 7\n\nT82 is ground\nT87 is ground\nT95 is ground\nX6 is free\nX7 is free\ndelmin(T1, T2, tree(T82, T95, T87)) !=? delmin(tree(X6, void, X7), X6, X7)", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: delmin(T114, T115, T112)\n\nT82 is ground\nT87 is ground\nT108 is ground\nT112 is ground\nT113 is ground\nX6 is free\nX7 is free\ndelmin(T1, T2, tree(T82, tree(T108, T112, T113), T87)) !=? delmin(tree(X6, void, X7), X6, X7)", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: delmin(T138, T139, T136)\n\nT82 is ground\nT87 is ground\nT132 is ground\nT136 is ground\nT137 is ground\nX6 is free\nX7 is free\nX86 is free\nX87 is free\ndelmin(T1, T2, tree(T82, tree(T132, T136, T137), T87)) !=? delmin(tree(X6, void, X7), X6, X7)\ndelmin(T88, T89, tree(T132, T136, T137)) !=? delmin(tree(X86, void, X87), X86, X87)", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 41 [arrowhead = none ];
41 -> 4;

42 [label="EVAL with clause\ndelmin(tree(X6, void, X7), X6, X7).\nand substitutionX6 -> T6,\nX7 -> T7,\nT1 -> tree(T6, void, T7),\nT2 -> T6,\nT3 -> T7", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 42 [arrowhead = none ];
42 -> 5;

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

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

45 [label="EVAL with clause\ndelmin(tree(X76, X77, X78), X79, tree(X76, X80, X81)) :- delmin(X77, X79, X80).\nand substitutionX76 -> T82,\nX77 -> T88,\nX78 -> T84,\nT1 -> tree(T82, T88, T84),\nT2 -> T89,\nX79 -> T89,\nX80 -> T86,\nX81 -> T87,\nT3 -> tree(T82, T86, T87),\nT83 -> T88,\nT85 -> T89", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 45 [arrowhead = none ];
45 -> 25;

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

47 [label="EVAL with clause\ndelmin(tree(X14, X15, X16), X17, tree(X14, X18, X19)) :- delmin(X15, X17, X18).\nand substitutionX14 -> T14,\nX15 -> T20,\nX16 -> T16,\nT1 -> tree(T14, T20, T16),\nT2 -> T21,\nX17 -> T21,\nX18 -> T18,\nX19 -> T19,\nT7 -> tree(T14, T18, T19),\nT15 -> T20,\nT17 -> T21", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 47 [arrowhead = none ];
47 -> 11;

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

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

50 [label="EVAL with clause\ndelmin(tree(X24, void, X25), X24, X25).\nand substitutionX24 -> T26,\nX25 -> T27,\nT20 -> tree(T26, void, T27),\nT21 -> T26,\nT18 -> T27", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 50 [arrowhead = none ];
50 -> 14;

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

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

53 [label="EVAL with clause\ndelmin(tree(X60, X61, X62), X63, tree(X60, X64, X65)) :- delmin(X61, X63, X64).\nand substitutionX60 -> T64,\nX61 -> T70,\nX62 -> T66,\nT20 -> tree(T64, T70, T66),\nT21 -> T71,\nX63 -> T71,\nX64 -> T68,\nX65 -> T69,\nT18 -> tree(T64, T68, T69),\nT65 -> T70,\nT67 -> T71", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 53 [arrowhead = none ];
53 -> 23;

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

55 [label="EVAL with clause\ndelmin(tree(X38, X39, X40), X41, tree(X38, X42, X43)) :- delmin(X39, X41, X42).\nand substitutionX38 -> T40,\nX39 -> T46,\nX40 -> T42,\nT20 -> tree(T40, T46, T42),\nT21 -> T47,\nX41 -> T47,\nX42 -> T44,\nX43 -> T45,\nT27 -> tree(T40, T44, T45),\nT41 -> T46,\nT43 -> T47", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 55 [arrowhead = none ];
55 -> 19;

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

57 [label="INSTANCE with matching:\nT1 -> T46\nT2 -> T47\nT3 -> T44", fontsize=14, style = filled, fillcolor = lightgrey];
19 -> 57 [arrowhead = none , style=dashed];
57 -> 2[style=dashed];

58 [label="INSTANCE with matching:\nT1 -> T70\nT2 -> T71\nT3 -> T68", fontsize=14, style = filled, fillcolor = lightgrey];
23 -> 58 [arrowhead = none , style=dashed];
58 -> 2[style=dashed];

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

60 [label="EVAL with clause\ndelmin(tree(X86, void, X87), X86, X87).\nand substitutionX86 -> T94,\nX87 -> T95,\nT88 -> tree(T94, void, T95),\nT89 -> T94,\nT86 -> T95", fontsize=14, style = filled, fillcolor = lightblue];
27 -> 60 [arrowhead = none ];
60 -> 28;

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

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

63 [label="EVAL with clause\ndelmin(tree(X122, X123, X124), X125, tree(X122, X126, X127)) :- delmin(X123, X125, X126).\nand substitutionX122 -> T132,\nX123 -> T138,\nX124 -> T134,\nT88 -> tree(T132, T138, T134),\nT89 -> T139,\nX125 -> T139,\nX126 -> T136,\nX127 -> T137,\nT86 -> tree(T132, T136, T137),\nT133 -> T138,\nT135 -> T139", fontsize=14, style = filled, fillcolor = lightblue];
29 -> 63 [arrowhead = none ];
63 -> 39;

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

65 [label="EVAL with clause\ndelmin(tree(X100, X101, X102), X103, tree(X100, X104, X105)) :- delmin(X101, X103, X104).\nand substitutionX100 -> T108,\nX101 -> T114,\nX102 -> T110,\nT88 -> tree(T108, T114, T110),\nT89 -> T115,\nX103 -> T115,\nX104 -> T112,\nX105 -> T113,\nT95 -> tree(T108, T112, T113),\nT109 -> T114,\nT111 -> T115", fontsize=14, style = filled, fillcolor = lightblue];
32 -> 65 [arrowhead = none ];
65 -> 33;

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

67 [label="INSTANCE with matching:\nT1 -> T114\nT2 -> T115\nT3 -> T112", fontsize=14, style = filled, fillcolor = lightgrey];
33 -> 67 [arrowhead = none , style=dashed];
67 -> 2[style=dashed];

68 [label="INSTANCE with matching:\nT1 -> T138\nT2 -> T139\nT3 -> T136", fontsize=14, style = filled, fillcolor = lightgrey];
39 -> 68 [arrowhead = none , style=dashed];
68 -> 2[style=dashed];

}

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0) → f2_out1
f2_in(tree(z0, z1, z2)) → f2_out1
f2_in(tree(z0, tree(z1, z2, z3), z4)) → U1(f2_in(z2), tree(z0, tree(z1, z2, z3), z4))
f2_in(tree(z0, tree(z1, z2, z3), z4)) → U2(f2_in(z2), tree(z0, tree(z1, z2, z3), z4))
f2_in(tree(z0, tree(z1, z2, z3), z4)) → U3(f2_in(z2), tree(z0, tree(z1, z2, z3), z4))
f2_in(tree(z0, tree(z1, z2, z3), z4)) → U4(f2_in(z2), tree(z0, tree(z1, z2, z3), z4))
U1(f2_out1, tree(z0, tree(z1, z2, z3), z4)) → f2_out1
U2(f2_out1, tree(z0, tree(z1, z2, z3), z4)) → f2_out1
U3(f2_out1, tree(z0, tree(z1, z2, z3), z4)) → f2_out1
U4(f2_out1, tree(z0, tree(z1, z2, z3), z4)) → f2_out1

Tuples:

F2_IN(tree(z0, tree(z1, z2, z3), z4)) → c2(U1'(f2_in(z2), tree(z0, tree(z1, z2, z3), z4)), F2_IN(z2))
F2_IN(tree(z0, tree(z1, z2, z3), z4)) → c3(U2'(f2_in(z2), tree(z0, tree(z1, z2, z3), z4)), F2_IN(z2))
F2_IN(tree(z0, tree(z1, z2, z3), z4)) → c4(U3'(f2_in(z2), tree(z0, tree(z1, z2, z3), z4)), F2_IN(z2))
F2_IN(tree(z0, tree(z1, z2, z3), z4)) → c5(U4'(f2_in(z2), tree(z0, tree(z1, z2, z3), z4)), F2_IN(z2))

S tuples:

F2_IN(tree(z0, tree(z1, z2, z3), z4)) → c2(U1'(f2_in(z2), tree(z0, tree(z1, z2, z3), z4)), F2_IN(z2))
F2_IN(tree(z0, tree(z1, z2, z3), z4)) → c3(U2'(f2_in(z2), tree(z0, tree(z1, z2, z3), z4)), F2_IN(z2))
F2_IN(tree(z0, tree(z1, z2, z3), z4)) → c4(U3'(f2_in(z2), tree(z0, tree(z1, z2, z3), z4)), F2_IN(z2))
F2_IN(tree(z0, tree(z1, z2, z3), z4)) → c5(U4'(f2_in(z2), tree(z0, tree(z1, z2, z3), z4)), F2_IN(z2))

K tuples:none
Defined Rule Symbols:

f2_in, U1, U2, U3, U4

Defined Pair Symbols:

F2_IN

Compound Symbols:

c2, c3, c4, c5

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

Removed 4 trailing tuple parts

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0) → f2_out1
f2_in(tree(z0, z1, z2)) → f2_out1
f2_in(tree(z0, tree(z1, z2, z3), z4)) → U1(f2_in(z2), tree(z0, tree(z1, z2, z3), z4))
f2_in(tree(z0, tree(z1, z2, z3), z4)) → U2(f2_in(z2), tree(z0, tree(z1, z2, z3), z4))
f2_in(tree(z0, tree(z1, z2, z3), z4)) → U3(f2_in(z2), tree(z0, tree(z1, z2, z3), z4))
f2_in(tree(z0, tree(z1, z2, z3), z4)) → U4(f2_in(z2), tree(z0, tree(z1, z2, z3), z4))
U1(f2_out1, tree(z0, tree(z1, z2, z3), z4)) → f2_out1
U2(f2_out1, tree(z0, tree(z1, z2, z3), z4)) → f2_out1
U3(f2_out1, tree(z0, tree(z1, z2, z3), z4)) → f2_out1
U4(f2_out1, tree(z0, tree(z1, z2, z3), z4)) → f2_out1

Tuples:

F2_IN(tree(z0, tree(z1, z2, z3), z4)) → c2(F2_IN(z2))
F2_IN(tree(z0, tree(z1, z2, z3), z4)) → c3(F2_IN(z2))
F2_IN(tree(z0, tree(z1, z2, z3), z4)) → c4(F2_IN(z2))
F2_IN(tree(z0, tree(z1, z2, z3), z4)) → c5(F2_IN(z2))

S tuples:

F2_IN(tree(z0, tree(z1, z2, z3), z4)) → c2(F2_IN(z2))
F2_IN(tree(z0, tree(z1, z2, z3), z4)) → c3(F2_IN(z2))
F2_IN(tree(z0, tree(z1, z2, z3), z4)) → c4(F2_IN(z2))
F2_IN(tree(z0, tree(z1, z2, z3), z4)) → c5(F2_IN(z2))

K tuples:none
Defined Rule Symbols:

f2_in, U1, U2, U3, U4

Defined Pair Symbols:

F2_IN

Compound Symbols:

c2, c3, c4, c5

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

F2_IN(tree(z0, tree(z1, z2, z3), z4)) → c2(F2_IN(z2))
F2_IN(tree(z0, tree(z1, z2, z3), z4)) → c3(F2_IN(z2))
F2_IN(tree(z0, tree(z1, z2, z3), z4)) → c4(F2_IN(z2))
F2_IN(tree(z0, tree(z1, z2, z3), z4)) → c5(F2_IN(z2))

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

F2_IN(tree(z0, tree(z1, z2, z3), z4)) → c2(F2_IN(z2))
F2_IN(tree(z0, tree(z1, z2, z3), z4)) → c3(F2_IN(z2))
F2_IN(tree(z0, tree(z1, z2, z3), z4)) → c4(F2_IN(z2))
F2_IN(tree(z0, tree(z1, z2, z3), z4)) → c5(F2_IN(z2))

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

POL(F2_IN(x₁)) = x₁   
POL(c2(x₁)) = x₁   
POL(c3(x₁)) = x₁   
POL(c4(x₁)) = x₁   
POL(c5(x₁)) = x₁   
POL(tree(x₁, x₂, x₃)) = [2] + x₂   

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0) → f2_out1
f2_in(tree(z0, z1, z2)) → f2_out1
f2_in(tree(z0, tree(z1, z2, z3), z4)) → U1(f2_in(z2), tree(z0, tree(z1, z2, z3), z4))
f2_in(tree(z0, tree(z1, z2, z3), z4)) → U2(f2_in(z2), tree(z0, tree(z1, z2, z3), z4))
f2_in(tree(z0, tree(z1, z2, z3), z4)) → U3(f2_in(z2), tree(z0, tree(z1, z2, z3), z4))
f2_in(tree(z0, tree(z1, z2, z3), z4)) → U4(f2_in(z2), tree(z0, tree(z1, z2, z3), z4))
U1(f2_out1, tree(z0, tree(z1, z2, z3), z4)) → f2_out1
U2(f2_out1, tree(z0, tree(z1, z2, z3), z4)) → f2_out1
U3(f2_out1, tree(z0, tree(z1, z2, z3), z4)) → f2_out1
U4(f2_out1, tree(z0, tree(z1, z2, z3), z4)) → f2_out1

Tuples:

F2_IN(tree(z0, tree(z1, z2, z3), z4)) → c2(F2_IN(z2))
F2_IN(tree(z0, tree(z1, z2, z3), z4)) → c3(F2_IN(z2))
F2_IN(tree(z0, tree(z1, z2, z3), z4)) → c4(F2_IN(z2))
F2_IN(tree(z0, tree(z1, z2, z3), z4)) → c5(F2_IN(z2))

S tuples:none
K tuples:

F2_IN(tree(z0, tree(z1, z2, z3), z4)) → c2(F2_IN(z2))
F2_IN(tree(z0, tree(z1, z2, z3), z4)) → c3(F2_IN(z2))
F2_IN(tree(z0, tree(z1, z2, z3), z4)) → c4(F2_IN(z2))
F2_IN(tree(z0, tree(z1, z2, z3), z4)) → c5(F2_IN(z2))

Defined Rule Symbols:

f2_in, U1, U2, U3, U4

Defined Pair Symbols:

F2_IN

Compound Symbols:

c2, c3, c4, c5