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

(0) Obligation:

Clauses:

bin_tree(void).
bin_tree(T) :- ','(no(empty(T)), ','(left(T, L), ','(right(T, R), ','(bin_tree(L), bin_tree(R))))).
left(void, void).
left(tree(X1, L, X2), L).
right(void, void).
right(tree(X3, X4, R), R).
empty(void).
no(X) :- ','(X, ','(!, failure(a))).
no(X5).
failure(b).

Query: bin_tree(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: bin_tree(T1)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: bin_tree(T1), SCOPE: 1, CLAUSE: 0 | bin_tree(T1), SCOPE: 1, CLAUSE: 1\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: true | bin_tree(void), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: bin_tree(T1), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nbin_tree(T1) !=? bin_tree(void)", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: bin_tree(void), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(no(empty(void)), ','(left(void, X11), ','(right(void, X12), ','(bin_tree(X11), bin_tree(X12)))))\n\nX11 is free\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: ','(no(empty(void)), ','(left(void, X11), ','(right(void, X12), ','(bin_tree(X11), bin_tree(X12))))), SCOPE: 2, CLAUSE: 7 | ','(no(empty(void)), ','(left(void, X11), ','(right(void, X12), ','(bin_tree(X11), bin_tree(X12))))), SCOPE: 2, CLAUSE: 8\n\nX11 is free\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ','(','(call(empty(void)), ','(!_2, failure(a))), ','(left(void, X11), ','(right(void, X12), ','(bin_tree(X11), bin_tree(X12))))) | ','(no(empty(void)), ','(left(void, X11), ','(right(void, X12), ','(bin_tree(X11), bin_tree(X12))))), SCOPE: 2, CLAUSE: 8\n\nX11 is free\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: ','(empty(void), ','(','(!_2, failure(a)), ','(left(void, X11), ','(right(void, X12), ','(bin_tree(X11), bin_tree(X12)))))) | ?_3 | ','(no(empty(void)), ','(left(void, X11), ','(right(void, X12), ','(bin_tree(X11), bin_tree(X12))))), SCOPE: 2, CLAUSE: 8\n\nX11 is free\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ','(empty(void), ','(','(!_2, failure(a)), ','(left(void, X11), ','(right(void, X12), ','(bin_tree(X11), bin_tree(X12)))))), SCOPE: 4, CLAUSE: 6 | ?_4 | ?_3 | ','(no(empty(void)), ','(left(void, X11), ','(right(void, X12), ','(bin_tree(X11), bin_tree(X12))))), SCOPE: 2, CLAUSE: 8\n\nX11 is free\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: ','(','(!_2, failure(a)), ','(left(void, X11), ','(right(void, X12), ','(bin_tree(X11), bin_tree(X12))))) | ?_4 | ?_3 | ','(no(empty(void)), ','(left(void, X11), ','(right(void, X12), ','(bin_tree(X11), bin_tree(X12))))), SCOPE: 2, CLAUSE: 8\n\nX11 is free\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: ','(failure(a), ','(left(void, X11), ','(right(void, X12), ','(bin_tree(X11), bin_tree(X12)))))\n\nX11 is free\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: ','(failure(a), ','(left(void, X11), ','(right(void, X12), ','(bin_tree(X11), bin_tree(X12))))), SCOPE: 5, CLAUSE: 9\n\nX11 is free\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: ','(no(empty(T4)), ','(left(T4, X21), ','(right(T4, X22), ','(bin_tree(X21), bin_tree(X22)))))\n\nT4 is ground\nX21 is free\nX22 is free\nbin_tree(T4) !=? bin_tree(void)", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: ','(no(empty(T4)), ','(left(T4, X21), ','(right(T4, X22), ','(bin_tree(X21), bin_tree(X22))))), SCOPE: 6, CLAUSE: 7 | ','(no(empty(T4)), ','(left(T4, X21), ','(right(T4, X22), ','(bin_tree(X21), bin_tree(X22))))), SCOPE: 6, CLAUSE: 8\n\nT4 is ground\nX21 is free\nX22 is free\nbin_tree(T4) !=? bin_tree(void)", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: ','(','(call(empty(T7)), ','(!_6, failure(a))), ','(left(T7, X21), ','(right(T7, X22), ','(bin_tree(X21), bin_tree(X22))))) | ','(no(empty(T7)), ','(left(T7, X21), ','(right(T7, X22), ','(bin_tree(X21), bin_tree(X22))))), SCOPE: 6, CLAUSE: 8\n\nT7 is ground\nX21 is free\nX22 is free\nbin_tree(T7) !=? bin_tree(void)", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: ','(empty(T7), ','(','(!_6, failure(a)), ','(left(T7, X21), ','(right(T7, X22), ','(bin_tree(X21), bin_tree(X22)))))) | ?_7 | ','(no(empty(T7)), ','(left(T7, X21), ','(right(T7, X22), ','(bin_tree(X21), bin_tree(X22))))), SCOPE: 6, CLAUSE: 8\n\nT7 is ground\nX21 is free\nX22 is free\nbin_tree(T7) !=? bin_tree(void)", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: ','(empty(T7), ','(','(!_6, failure(a)), ','(left(T7, X21), ','(right(T7, X22), ','(bin_tree(X21), bin_tree(X22)))))), SCOPE: 8, CLAUSE: 6 | ?_8 | ?_7 | ','(no(empty(T7)), ','(left(T7, X21), ','(right(T7, X22), ','(bin_tree(X21), bin_tree(X22))))), SCOPE: 6, CLAUSE: 8\n\nT7 is ground\nX21 is free\nX22 is free\nbin_tree(T7) !=? bin_tree(void)", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: ?_8 | ?_7 | ','(no(empty(T7)), ','(left(T7, X21), ','(right(T7, X22), ','(bin_tree(X21), bin_tree(X22))))), SCOPE: 6, CLAUSE: 8\n\nT7 is ground\nX21 is free\nX22 is free\nbin_tree(T7) !=? bin_tree(void)", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: ?_7 | ','(no(empty(T7)), ','(left(T7, X21), ','(right(T7, X22), ','(bin_tree(X21), bin_tree(X22))))), SCOPE: 6, CLAUSE: 8\n\nT7 is ground\nX21 is free\nX22 is free\nbin_tree(T7) !=? bin_tree(void)", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: ','(no(empty(T7)), ','(left(T7, X21), ','(right(T7, X22), ','(bin_tree(X21), bin_tree(X22))))), SCOPE: 6, CLAUSE: 8\n\nT7 is ground\nX21 is free\nX22 is free\nbin_tree(T7) !=? bin_tree(void)", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: ','(left(T10, X21), ','(right(T10, X22), ','(bin_tree(X21), bin_tree(X22))))\n\nT10 is ground\nX21 is free\nX22 is free\nbin_tree(T10) !=? bin_tree(void)", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ','(left(T10, X21), ','(right(T10, X22), ','(bin_tree(X21), bin_tree(X22)))), SCOPE: 9, CLAUSE: 2 | ','(left(T10, X21), ','(right(T10, X22), ','(bin_tree(X21), bin_tree(X22)))), SCOPE: 9, CLAUSE: 3\n\nT10 is ground\nX21 is free\nX22 is free\nbin_tree(T10) !=? bin_tree(void)", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: ','(left(T10, X21), ','(right(T10, X22), ','(bin_tree(X21), bin_tree(X22)))), SCOPE: 9, CLAUSE: 3\n\nT10 is ground\nX21 is free\nX22 is free\nbin_tree(T10) !=? bin_tree(void)", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: ','(right(tree(T17, T18, T19), X22), ','(bin_tree(T18), bin_tree(X22)))\n\nT17 is ground\nT18 is ground\nT19 is ground\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: ','(right(tree(T17, T18, T19), X22), ','(bin_tree(T18), bin_tree(X22))), SCOPE: 10, CLAUSE: 4 | ','(right(tree(T17, T18, T19), X22), ','(bin_tree(T18), bin_tree(X22))), SCOPE: 10, CLAUSE: 5\n\nT17 is ground\nT18 is ground\nT19 is ground\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: ','(right(tree(T17, T18, T19), X22), ','(bin_tree(T18), bin_tree(X22))), SCOPE: 10, CLAUSE: 5\n\nT17 is ground\nT18 is ground\nT19 is ground\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: ','(bin_tree(T27), bin_tree(T28))\n\nT27 is ground\nT28 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: bin_tree(T27)\n\nT27 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: bin_tree(T28)\n\nT28 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 64 [arrowhead = none ];
64 -> 4;

65 [label="EVAL with clause\nbin_tree(void).\nand substitutionT1 -> void", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 65 [arrowhead = none ];
65 -> 6;

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

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

68 [label="ONLY EVAL with clause\nbin_tree(X20) :- ','(no(empty(X20)), ','(left(X20, X21), ','(right(X20, X22), ','(bin_tree(X21), bin_tree(X22))))).\nand substitutionT1 -> T4,\nX20 -> T4", fontsize=14, style = filled, fillcolor = lightblue];
8 -> 68 [arrowhead = none ];
68 -> 31;

69 [label="ONLY EVAL with clause\nbin_tree(X10) :- ','(no(empty(X10)), ','(left(X10, X11), ','(right(X10, X12), ','(bin_tree(X11), bin_tree(X12))))).\nand substitutionX10 -> void", fontsize=14, style = filled, fillcolor = lightblue];
9 -> 69 [arrowhead = none ];
69 -> 13;

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

71 [label="ONLY EVAL with clause\nno(X15) :- ','(call(X15), ','(!_2, failure(a))).\nand substitutionX15 -> empty(void)", fontsize=14, style = filled, fillcolor = lightblue];
14 -> 71 [arrowhead = none ];
71 -> 17;

72 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
17 -> 72 [arrowhead = none ];
72 -> 18;

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

74 [label="ONLY EVAL with clause\nempty(void).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
20 -> 74 [arrowhead = none ];
74 -> 23;

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

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

77 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
25 -> 77 [arrowhead = none ];
77 -> 27;

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

79 [label="ONLY EVAL with clause\nno(X25) :- ','(call(X25), ','(!_6, failure(a))).\nand substitutionT4 -> T7,\nX25 -> empty(T7)", fontsize=14, style = filled, fillcolor = lightblue];
33 -> 79 [arrowhead = none ];
79 -> 37;

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

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

82 [label="BACKTRACK\nfor clause: empty(void)\nwith clash: (bin_tree(T7), bin_tree(void))", fontsize=14, style = filled, fillcolor = lightgreen];
41 -> 82 [arrowhead = none ];
82 -> 42;

83 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
42 -> 83 [arrowhead = none ];
83 -> 43;

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

85 [label="ONLY EVAL with clause\nno(X28).\nand substitutionT7 -> T10,\nX28 -> empty(T10)", fontsize=14, style = filled, fillcolor = lightblue];
44 -> 85 [arrowhead = none ];
85 -> 47;

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

87 [label="BACKTRACK\nfor clause: left(void, void)\nwith clash: (bin_tree(T10), bin_tree(void))", fontsize=14, style = filled, fillcolor = lightgreen];
49 -> 87 [arrowhead = none ];
87 -> 50;

88 [label="EVAL with clause\nleft(tree(X35, X36, X37), X36).\nand substitutionX35 -> T17,\nX36 -> T18,\nX37 -> T19,\nT10 -> tree(T17, T18, T19),\nX21 -> T18", fontsize=14, style = filled, fillcolor = lightblue];
50 -> 88 [arrowhead = none ];
88 -> 55;

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

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

91 [label="BACKTRACK\nfor clause: right(void, void)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
57 -> 91 [arrowhead = none ];
91 -> 58;

92 [label="ONLY EVAL with clause\nright(tree(X44, X45, X46), X46).\nand substitutionT17 -> T26,\nX44 -> T26,\nT18 -> T27,\nX45 -> T27,\nT19 -> T28,\nX46 -> T28,\nX22 -> T28", fontsize=14, style = filled, fillcolor = lightblue];
58 -> 92 [arrowhead = none ];
92 -> 60;

93 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
60 -> 93 [arrowhead = none ];
93 -> 61;

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

95 [label="INSTANCE with matching:\nT1 -> T27", fontsize=14, style = filled, fillcolor = lightgrey];
61 -> 95 [arrowhead = none , style=dashed];
95 -> 1[style=dashed];

96 [label="INSTANCE with matching:\nT1 -> T28", fontsize=14, style = filled, fillcolor = lightgrey];
63 -> 96 [arrowhead = none , style=dashed];
96 -> 1[style=dashed];

}

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(void) → f1_out1
f1_in(tree(z0, z1, z2)) → U1(f60_in(z1, z2), tree(z0, z1, z2))
U1(f60_out1, tree(z0, z1, z2)) → f1_out1
f60_in(z0, z1) → U2(f1_in(z0), z0, z1)
U2(f1_out1, z0, z1) → U3(f1_in(z1), z0, z1)
U3(f1_out1, z0, z1) → f60_out1

Tuples:

F1_IN(tree(z0, z1, z2)) → c1(U1'(f60_in(z1, z2), tree(z0, z1, z2)), F60_IN(z1, z2))
F60_IN(z0, z1) → c3(U2'(f1_in(z0), z0, z1), F1_IN(z0))
U2'(f1_out1, z0, z1) → c4(U3'(f1_in(z1), z0, z1), F1_IN(z1))

S tuples:

F1_IN(tree(z0, z1, z2)) → c1(U1'(f60_in(z1, z2), tree(z0, z1, z2)), F60_IN(z1, z2))
F60_IN(z0, z1) → c3(U2'(f1_in(z0), z0, z1), F1_IN(z0))
U2'(f1_out1, z0, z1) → c4(U3'(f1_in(z1), z0, z1), F1_IN(z1))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f60_in, U2, U3

Defined Pair Symbols:

F1_IN, F60_IN, U2'

Compound Symbols:

c1, c3, c4

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

Removed 2 trailing tuple parts

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(void) → f1_out1
f1_in(tree(z0, z1, z2)) → U1(f60_in(z1, z2), tree(z0, z1, z2))
U1(f60_out1, tree(z0, z1, z2)) → f1_out1
f60_in(z0, z1) → U2(f1_in(z0), z0, z1)
U2(f1_out1, z0, z1) → U3(f1_in(z1), z0, z1)
U3(f1_out1, z0, z1) → f60_out1

Tuples:

F60_IN(z0, z1) → c3(U2'(f1_in(z0), z0, z1), F1_IN(z0))
F1_IN(tree(z0, z1, z2)) → c1(F60_IN(z1, z2))
U2'(f1_out1, z0, z1) → c4(F1_IN(z1))

S tuples:

F60_IN(z0, z1) → c3(U2'(f1_in(z0), z0, z1), F1_IN(z0))
F1_IN(tree(z0, z1, z2)) → c1(F60_IN(z1, z2))
U2'(f1_out1, z0, z1) → c4(F1_IN(z1))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f60_in, U2, U3

Defined Pair Symbols:

F60_IN, F1_IN, U2'

Compound Symbols:

c3, c1, c4

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

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

U2'(f1_out1, z0, z1) → c4(F1_IN(z1))

We considered the (Usable) Rules:

f1_in(void) → f1_out1
f1_in(tree(z0, z1, z2)) → U1(f60_in(z1, z2), tree(z0, z1, z2))
f60_in(z0, z1) → U2(f1_in(z0), z0, z1)
U1(f60_out1, tree(z0, z1, z2)) → f1_out1
U2(f1_out1, z0, z1) → U3(f1_in(z1), z0, z1)
U3(f1_out1, z0, z1) → f60_out1

And the Tuples:

F60_IN(z0, z1) → c3(U2'(f1_in(z0), z0, z1), F1_IN(z0))
F1_IN(tree(z0, z1, z2)) → c1(F60_IN(z1, z2))
U2'(f1_out1, z0, z1) → c4(F1_IN(z1))

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

POL(F1_IN(x₁)) = x₁   
POL(F60_IN(x₁, x₂)) = [2] + x₁ + x₂   
POL(U1(x₁, x₂)) = 0   
POL(U2(x₁, x₂, x₃)) = 0   
POL(U2'(x₁, x₂, x₃)) = [2] + x₃   
POL(U3(x₁, x₂, x₃)) = 0   
POL(c1(x₁)) = x₁   
POL(c3(x₁, x₂)) = x₁ + x₂   
POL(c4(x₁)) = x₁   
POL(f1_in(x₁)) = 0   
POL(f1_out1) = 0   
POL(f60_in(x₁, x₂)) = 0   
POL(f60_out1) = 0   
POL(tree(x₁, x₂, x₃)) = [2] + x₂ + x₃   
POL(void) = 0   

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(void) → f1_out1
f1_in(tree(z0, z1, z2)) → U1(f60_in(z1, z2), tree(z0, z1, z2))
U1(f60_out1, tree(z0, z1, z2)) → f1_out1
f60_in(z0, z1) → U2(f1_in(z0), z0, z1)
U2(f1_out1, z0, z1) → U3(f1_in(z1), z0, z1)
U3(f1_out1, z0, z1) → f60_out1

Tuples:

F60_IN(z0, z1) → c3(U2'(f1_in(z0), z0, z1), F1_IN(z0))
F1_IN(tree(z0, z1, z2)) → c1(F60_IN(z1, z2))
U2'(f1_out1, z0, z1) → c4(F1_IN(z1))

S tuples:

F60_IN(z0, z1) → c3(U2'(f1_in(z0), z0, z1), F1_IN(z0))
F1_IN(tree(z0, z1, z2)) → c1(F60_IN(z1, z2))

K tuples:

U2'(f1_out1, z0, z1) → c4(F1_IN(z1))

Defined Rule Symbols:

f1_in, U1, f60_in, U2, U3

Defined Pair Symbols:

F60_IN, F1_IN, U2'

Compound Symbols:

c3, c1, c4

(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(F60_IN(z1, z2))

We considered the (Usable) Rules:

f1_in(void) → f1_out1
f1_in(tree(z0, z1, z2)) → U1(f60_in(z1, z2), tree(z0, z1, z2))
f60_in(z0, z1) → U2(f1_in(z0), z0, z1)
U1(f60_out1, tree(z0, z1, z2)) → f1_out1
U2(f1_out1, z0, z1) → U3(f1_in(z1), z0, z1)
U3(f1_out1, z0, z1) → f60_out1

And the Tuples:

F60_IN(z0, z1) → c3(U2'(f1_in(z0), z0, z1), F1_IN(z0))
F1_IN(tree(z0, z1, z2)) → c1(F60_IN(z1, z2))
U2'(f1_out1, z0, z1) → c4(F1_IN(z1))

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

POL(F1_IN(x₁)) = [2]x₁   
POL(F60_IN(x₁, x₂)) = [2]x₁ + [2]x₂   
POL(U1(x₁, x₂)) = 0   
POL(U2(x₁, x₂, x₃)) = [3] + [3]x₁ + x₃   
POL(U2'(x₁, x₂, x₃)) = [2]x₃   
POL(U3(x₁, x₂, x₃)) = x₃   
POL(c1(x₁)) = x₁   
POL(c3(x₁, x₂)) = x₁ + x₂   
POL(c4(x₁)) = x₁   
POL(f1_in(x₁)) = 0   
POL(f1_out1) = [2]   
POL(f60_in(x₁, x₂)) = [3] + x₁ + [2]x₂   
POL(f60_out1) = 0   
POL(tree(x₁, x₂, x₃)) = [1] + x₂ + x₃   
POL(void) = 0   

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(void) → f1_out1
f1_in(tree(z0, z1, z2)) → U1(f60_in(z1, z2), tree(z0, z1, z2))
U1(f60_out1, tree(z0, z1, z2)) → f1_out1
f60_in(z0, z1) → U2(f1_in(z0), z0, z1)
U2(f1_out1, z0, z1) → U3(f1_in(z1), z0, z1)
U3(f1_out1, z0, z1) → f60_out1

Tuples:

F60_IN(z0, z1) → c3(U2'(f1_in(z0), z0, z1), F1_IN(z0))
F1_IN(tree(z0, z1, z2)) → c1(F60_IN(z1, z2))
U2'(f1_out1, z0, z1) → c4(F1_IN(z1))

S tuples:

F60_IN(z0, z1) → c3(U2'(f1_in(z0), z0, z1), F1_IN(z0))

K tuples:

U2'(f1_out1, z0, z1) → c4(F1_IN(z1))
F1_IN(tree(z0, z1, z2)) → c1(F60_IN(z1, z2))

Defined Rule Symbols:

f1_in, U1, f60_in, U2, U3

Defined Pair Symbols:

F60_IN, F1_IN, U2'

Compound Symbols:

c3, c1, c4

(9) CdtKnowledgeProof (EQUIVALENT transformation)

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

F60_IN(z0, z1) → c3(U2'(f1_in(z0), z0, z1), F1_IN(z0))
F1_IN(tree(z0, z1, z2)) → c1(F60_IN(z1, z2))
U2'(f1_out1, z0, z1) → c4(F1_IN(z1))

Now 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: bin_tree(T1)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
3 [label="3: bin_tree(T1), SCOPE: 1, CLAUSE: 0 | bin_tree(T1), SCOPE: 1, CLAUSE: 1\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: true | bin_tree(void), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: bin_tree(T1), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nbin_tree(T1) !=? bin_tree(void)", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: bin_tree(void), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: ','(no(empty(void)), ','(left(void, X8), ','(right(void, X9), ','(bin_tree(X8), bin_tree(X9)))))\n\nX8 is free\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: ','(no(empty(void)), ','(left(void, X8), ','(right(void, X9), ','(bin_tree(X8), bin_tree(X9))))), SCOPE: 2, CLAUSE: 7 | ','(no(empty(void)), ','(left(void, X8), ','(right(void, X9), ','(bin_tree(X8), bin_tree(X9))))), SCOPE: 2, CLAUSE: 8\n\nX8 is free\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(','(call(empty(void)), ','(!_2, failure(a))), ','(left(void, X8), ','(right(void, X9), ','(bin_tree(X8), bin_tree(X9))))) | ','(no(empty(void)), ','(left(void, X8), ','(right(void, X9), ','(bin_tree(X8), bin_tree(X9))))), SCOPE: 2, CLAUSE: 8\n\nX8 is free\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ','(empty(void), ','(','(!_2, failure(a)), ','(left(void, X8), ','(right(void, X9), ','(bin_tree(X8), bin_tree(X9)))))) | ?_3 | ','(no(empty(void)), ','(left(void, X8), ','(right(void, X9), ','(bin_tree(X8), bin_tree(X9))))), SCOPE: 2, CLAUSE: 8\n\nX8 is free\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(empty(void), ','(','(!_2, failure(a)), ','(left(void, X8), ','(right(void, X9), ','(bin_tree(X8), bin_tree(X9)))))), SCOPE: 4, CLAUSE: 6 | ?_4 | ?_3 | ','(no(empty(void)), ','(left(void, X8), ','(right(void, X9), ','(bin_tree(X8), bin_tree(X9))))), SCOPE: 2, CLAUSE: 8\n\nX8 is free\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: ','(','(!_2, failure(a)), ','(left(void, X8), ','(right(void, X9), ','(bin_tree(X8), bin_tree(X9))))) | ?_4 | ?_3 | ','(no(empty(void)), ','(left(void, X8), ','(right(void, X9), ','(bin_tree(X8), bin_tree(X9))))), SCOPE: 2, CLAUSE: 8\n\nX8 is free\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: ','(failure(a), ','(left(void, X8), ','(right(void, X9), ','(bin_tree(X8), bin_tree(X9)))))\n\nX8 is free\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ','(failure(a), ','(left(void, X8), ','(right(void, X9), ','(bin_tree(X8), bin_tree(X9))))), SCOPE: 5, CLAUSE: 9\n\nX8 is free\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: ','(no(empty(T3)), ','(left(T3, X15), ','(right(T3, X16), ','(bin_tree(X15), bin_tree(X16)))))\n\nT3 is ground\nX15 is free\nX16 is free\nbin_tree(T3) !=? bin_tree(void)", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: ','(no(empty(T3)), ','(left(T3, X15), ','(right(T3, X16), ','(bin_tree(X15), bin_tree(X16))))), SCOPE: 6, CLAUSE: 7 | ','(no(empty(T3)), ','(left(T3, X15), ','(right(T3, X16), ','(bin_tree(X15), bin_tree(X16))))), SCOPE: 6, CLAUSE: 8\n\nT3 is ground\nX15 is free\nX16 is free\nbin_tree(T3) !=? bin_tree(void)", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: ','(','(call(empty(T6)), ','(!_6, failure(a))), ','(left(T6, X15), ','(right(T6, X16), ','(bin_tree(X15), bin_tree(X16))))) | ','(no(empty(T6)), ','(left(T6, X15), ','(right(T6, X16), ','(bin_tree(X15), bin_tree(X16))))), SCOPE: 6, CLAUSE: 8\n\nT6 is ground\nX15 is free\nX16 is free\nbin_tree(T6) !=? bin_tree(void)", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: ','(empty(T6), ','(','(!_6, failure(a)), ','(left(T6, X15), ','(right(T6, X16), ','(bin_tree(X15), bin_tree(X16)))))) | ?_7 | ','(no(empty(T6)), ','(left(T6, X15), ','(right(T6, X16), ','(bin_tree(X15), bin_tree(X16))))), SCOPE: 6, CLAUSE: 8\n\nT6 is ground\nX15 is free\nX16 is free\nbin_tree(T6) !=? bin_tree(void)", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: ','(empty(T6), ','(','(!_6, failure(a)), ','(left(T6, X15), ','(right(T6, X16), ','(bin_tree(X15), bin_tree(X16)))))), SCOPE: 8, CLAUSE: 6 | ?_8 | ?_7 | ','(no(empty(T6)), ','(left(T6, X15), ','(right(T6, X16), ','(bin_tree(X15), bin_tree(X16))))), SCOPE: 6, CLAUSE: 8\n\nT6 is ground\nX15 is free\nX16 is free\nbin_tree(T6) !=? bin_tree(void)", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: ?_8 | ?_7 | ','(no(empty(T6)), ','(left(T6, X15), ','(right(T6, X16), ','(bin_tree(X15), bin_tree(X16))))), SCOPE: 6, CLAUSE: 8\n\nT6 is ground\nX15 is free\nX16 is free\nbin_tree(T6) !=? bin_tree(void)", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: ?_7 | ','(no(empty(T6)), ','(left(T6, X15), ','(right(T6, X16), ','(bin_tree(X15), bin_tree(X16))))), SCOPE: 6, CLAUSE: 8\n\nT6 is ground\nX15 is free\nX16 is free\nbin_tree(T6) !=? bin_tree(void)", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: ','(no(empty(T6)), ','(left(T6, X15), ','(right(T6, X16), ','(bin_tree(X15), bin_tree(X16))))), SCOPE: 6, CLAUSE: 8\n\nT6 is ground\nX15 is free\nX16 is free\nbin_tree(T6) !=? bin_tree(void)", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: ','(left(T9, X15), ','(right(T9, X16), ','(bin_tree(X15), bin_tree(X16))))\n\nT9 is ground\nX15 is free\nX16 is free\nbin_tree(T9) !=? bin_tree(void)", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: ','(left(T9, X15), ','(right(T9, X16), ','(bin_tree(X15), bin_tree(X16)))), SCOPE: 9, CLAUSE: 2 | ','(left(T9, X15), ','(right(T9, X16), ','(bin_tree(X15), bin_tree(X16)))), SCOPE: 9, CLAUSE: 3\n\nT9 is ground\nX15 is free\nX16 is free\nbin_tree(T9) !=? bin_tree(void)", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: ','(left(T9, X15), ','(right(T9, X16), ','(bin_tree(X15), bin_tree(X16)))), SCOPE: 9, CLAUSE: 3\n\nT9 is ground\nX15 is free\nX16 is free\nbin_tree(T9) !=? bin_tree(void)", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: ','(right(tree(T16, T17, T18), X16), ','(bin_tree(T17), bin_tree(X16)))\n\nT16 is ground\nT17 is ground\nT18 is ground\nX16 is free", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: ','(right(tree(T16, T17, T18), X16), ','(bin_tree(T17), bin_tree(X16))), SCOPE: 10, CLAUSE: 4 | ','(right(tree(T16, T17, T18), X16), ','(bin_tree(T17), bin_tree(X16))), SCOPE: 10, CLAUSE: 5\n\nT16 is ground\nT17 is ground\nT18 is ground\nX16 is free", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: ','(right(tree(T16, T17, T18), X16), ','(bin_tree(T17), bin_tree(X16))), SCOPE: 10, CLAUSE: 5\n\nT16 is ground\nT17 is ground\nT18 is ground\nX16 is free", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: ','(bin_tree(T26), bin_tree(T27))\n\nT26 is ground\nT27 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: bin_tree(T26)\n\nT26 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: bin_tree(T27)\n\nT27 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 65 [arrowhead = none ];
65 -> 3;

66 [label="EVAL with clause\nbin_tree(void).\nand substitutionT1 -> void", fontsize=14, style = filled, fillcolor = lightblue];
3 -> 66 [arrowhead = none ];
66 -> 5;

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

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

69 [label="ONLY EVAL with clause\nbin_tree(X14) :- ','(no(empty(X14)), ','(left(X14, X15), ','(right(X14, X16), ','(bin_tree(X15), bin_tree(X16))))).\nand substitutionT1 -> T3,\nX14 -> T3", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 69 [arrowhead = none ];
69 -> 29;

70 [label="ONLY EVAL with clause\nbin_tree(X7) :- ','(no(empty(X7)), ','(left(X7, X8), ','(right(X7, X9), ','(bin_tree(X8), bin_tree(X9))))).\nand substitutionX7 -> void", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 70 [arrowhead = none ];
70 -> 11;

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

72 [label="ONLY EVAL with clause\nno(X12) :- ','(call(X12), ','(!_2, failure(a))).\nand substitutionX12 -> empty(void)", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 72 [arrowhead = none ];
72 -> 15;

73 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
15 -> 73 [arrowhead = none ];
73 -> 16;

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

75 [label="ONLY EVAL with clause\nempty(void).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
19 -> 75 [arrowhead = none ];
75 -> 21;

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

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

78 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
26 -> 78 [arrowhead = none ];
78 -> 28;

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

80 [label="ONLY EVAL with clause\nno(X19) :- ','(call(X19), ','(!_6, failure(a))).\nand substitutionT3 -> T6,\nX19 -> empty(T6)", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 80 [arrowhead = none ];
80 -> 32;

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

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

83 [label="BACKTRACK\nfor clause: empty(void)\nwith clash: (bin_tree(T6), bin_tree(void))", fontsize=14, style = filled, fillcolor = lightgreen];
35 -> 83 [arrowhead = none ];
83 -> 36;

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

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

86 [label="ONLY EVAL with clause\nno(X22).\nand substitutionT6 -> T9,\nX22 -> empty(T9)", fontsize=14, style = filled, fillcolor = lightblue];
40 -> 86 [arrowhead = none ];
86 -> 45;

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

88 [label="BACKTRACK\nfor clause: left(void, void)\nwith clash: (bin_tree(T9), bin_tree(void))", fontsize=14, style = filled, fillcolor = lightgreen];
46 -> 88 [arrowhead = none ];
88 -> 48;

89 [label="EVAL with clause\nleft(tree(X29, X30, X31), X30).\nand substitutionX29 -> T16,\nX30 -> T17,\nX31 -> T18,\nT9 -> tree(T16, T17, T18),\nX15 -> T17", fontsize=14, style = filled, fillcolor = lightblue];
48 -> 89 [arrowhead = none ];
89 -> 51;

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

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

92 [label="BACKTRACK\nfor clause: right(void, void)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
53 -> 92 [arrowhead = none ];
92 -> 54;

93 [label="ONLY EVAL with clause\nright(tree(X38, X39, X40), X40).\nand substitutionT16 -> T25,\nX38 -> T25,\nT17 -> T26,\nX39 -> T26,\nT18 -> T27,\nX40 -> T27,\nX16 -> T27", fontsize=14, style = filled, fillcolor = lightblue];
54 -> 93 [arrowhead = none ];
93 -> 59;

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

95 [label="SPLIT 2\nnew knowledge:\nT26 is ground", fontsize=14, style = filled, fillcolor = violet];
59 -> 95 [arrowhead = none ];
95 -> 64;

96 [label="INSTANCE with matching:\nT1 -> T26", fontsize=14, style = filled, fillcolor = lightgrey];
62 -> 96 [arrowhead = none , style=dashed];
96 -> 2[style=dashed];

97 [label="INSTANCE with matching:\nT1 -> T27", fontsize=14, style = filled, fillcolor = lightgrey];
64 -> 97 [arrowhead = none , style=dashed];
97 -> 2[style=dashed];

}

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(void) → f2_out1
f2_in(tree(z0, z1, z2)) → U1(f59_in(z1, z2), tree(z0, z1, z2))
U1(f59_out1, tree(z0, z1, z2)) → f2_out1
f59_in(z0, z1) → U2(f2_in(z0), z0, z1)
U2(f2_out1, z0, z1) → U3(f2_in(z1), z0, z1)
U3(f2_out1, z0, z1) → f59_out1

Tuples:

F2_IN(tree(z0, z1, z2)) → c1(U1'(f59_in(z1, z2), tree(z0, z1, z2)), F59_IN(z1, z2))
F59_IN(z0, z1) → c3(U2'(f2_in(z0), z0, z1), F2_IN(z0))
U2'(f2_out1, z0, z1) → c4(U3'(f2_in(z1), z0, z1), F2_IN(z1))

S tuples:

F2_IN(tree(z0, z1, z2)) → c1(U1'(f59_in(z1, z2), tree(z0, z1, z2)), F59_IN(z1, z2))
F59_IN(z0, z1) → c3(U2'(f2_in(z0), z0, z1), F2_IN(z0))
U2'(f2_out1, z0, z1) → c4(U3'(f2_in(z1), z0, z1), F2_IN(z1))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f59_in, U2, U3

Defined Pair Symbols:

F2_IN, F59_IN, U2'

Compound Symbols:

c1, c3, c4

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

Removed 2 trailing tuple parts

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(void) → f2_out1
f2_in(tree(z0, z1, z2)) → U1(f59_in(z1, z2), tree(z0, z1, z2))
U1(f59_out1, tree(z0, z1, z2)) → f2_out1
f59_in(z0, z1) → U2(f2_in(z0), z0, z1)
U2(f2_out1, z0, z1) → U3(f2_in(z1), z0, z1)
U3(f2_out1, z0, z1) → f59_out1

Tuples:

F59_IN(z0, z1) → c3(U2'(f2_in(z0), z0, z1), F2_IN(z0))
F2_IN(tree(z0, z1, z2)) → c1(F59_IN(z1, z2))
U2'(f2_out1, z0, z1) → c4(F2_IN(z1))

S tuples:

F59_IN(z0, z1) → c3(U2'(f2_in(z0), z0, z1), F2_IN(z0))
F2_IN(tree(z0, z1, z2)) → c1(F59_IN(z1, z2))
U2'(f2_out1, z0, z1) → c4(F2_IN(z1))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f59_in, U2, U3

Defined Pair Symbols:

F59_IN, F2_IN, U2'

Compound Symbols:

c3, c1, c4

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

U2'(f2_out1, z0, z1) → c4(F2_IN(z1))

We considered the (Usable) Rules:

f2_in(void) → f2_out1
f2_in(tree(z0, z1, z2)) → U1(f59_in(z1, z2), tree(z0, z1, z2))
f59_in(z0, z1) → U2(f2_in(z0), z0, z1)
U1(f59_out1, tree(z0, z1, z2)) → f2_out1
U2(f2_out1, z0, z1) → U3(f2_in(z1), z0, z1)
U3(f2_out1, z0, z1) → f59_out1

And the Tuples:

F59_IN(z0, z1) → c3(U2'(f2_in(z0), z0, z1), F2_IN(z0))
F2_IN(tree(z0, z1, z2)) → c1(F59_IN(z1, z2))
U2'(f2_out1, z0, z1) → c4(F2_IN(z1))

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

POL(F2_IN(x₁)) = x₁   
POL(F59_IN(x₁, x₂)) = [2] + x₁ + x₂   
POL(U1(x₁, x₂)) = 0   
POL(U2(x₁, x₂, x₃)) = 0   
POL(U2'(x₁, x₂, x₃)) = [2] + x₃   
POL(U3(x₁, x₂, x₃)) = 0   
POL(c1(x₁)) = x₁   
POL(c3(x₁, x₂)) = x₁ + x₂   
POL(c4(x₁)) = x₁   
POL(f2_in(x₁)) = 0   
POL(f2_out1) = 0   
POL(f59_in(x₁, x₂)) = 0   
POL(f59_out1) = 0   
POL(tree(x₁, x₂, x₃)) = [2] + x₂ + x₃   
POL(void) = 0   

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(void) → f2_out1
f2_in(tree(z0, z1, z2)) → U1(f59_in(z1, z2), tree(z0, z1, z2))
U1(f59_out1, tree(z0, z1, z2)) → f2_out1
f59_in(z0, z1) → U2(f2_in(z0), z0, z1)
U2(f2_out1, z0, z1) → U3(f2_in(z1), z0, z1)
U3(f2_out1, z0, z1) → f59_out1

Tuples:

F59_IN(z0, z1) → c3(U2'(f2_in(z0), z0, z1), F2_IN(z0))
F2_IN(tree(z0, z1, z2)) → c1(F59_IN(z1, z2))
U2'(f2_out1, z0, z1) → c4(F2_IN(z1))

S tuples:

F59_IN(z0, z1) → c3(U2'(f2_in(z0), z0, z1), F2_IN(z0))
F2_IN(tree(z0, z1, z2)) → c1(F59_IN(z1, z2))

K tuples:

U2'(f2_out1, z0, z1) → c4(F2_IN(z1))

Defined Rule Symbols:

f2_in, U1, f59_in, U2, U3

Defined Pair Symbols:

F59_IN, F2_IN, U2'

Compound Symbols:

c3, c1, c4

(17) 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, z1, z2)) → c1(F59_IN(z1, z2))

We considered the (Usable) Rules:

f2_in(void) → f2_out1
f2_in(tree(z0, z1, z2)) → U1(f59_in(z1, z2), tree(z0, z1, z2))
f59_in(z0, z1) → U2(f2_in(z0), z0, z1)
U1(f59_out1, tree(z0, z1, z2)) → f2_out1
U2(f2_out1, z0, z1) → U3(f2_in(z1), z0, z1)
U3(f2_out1, z0, z1) → f59_out1

And the Tuples:

F59_IN(z0, z1) → c3(U2'(f2_in(z0), z0, z1), F2_IN(z0))
F2_IN(tree(z0, z1, z2)) → c1(F59_IN(z1, z2))
U2'(f2_out1, z0, z1) → c4(F2_IN(z1))

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

POL(F2_IN(x₁)) = [2]x₁   
POL(F59_IN(x₁, x₂)) = [2]x₁ + [2]x₂   
POL(U1(x₁, x₂)) = 0   
POL(U2(x₁, x₂, x₃)) = [3] + [3]x₁ + x₃   
POL(U2'(x₁, x₂, x₃)) = [2]x₃   
POL(U3(x₁, x₂, x₃)) = x₃   
POL(c1(x₁)) = x₁   
POL(c3(x₁, x₂)) = x₁ + x₂   
POL(c4(x₁)) = x₁   
POL(f2_in(x₁)) = 0   
POL(f2_out1) = [2]   
POL(f59_in(x₁, x₂)) = [3] + x₁ + [2]x₂   
POL(f59_out1) = 0   
POL(tree(x₁, x₂, x₃)) = [1] + x₂ + x₃   
POL(void) = 0   

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(void) → f2_out1
f2_in(tree(z0, z1, z2)) → U1(f59_in(z1, z2), tree(z0, z1, z2))
U1(f59_out1, tree(z0, z1, z2)) → f2_out1
f59_in(z0, z1) → U2(f2_in(z0), z0, z1)
U2(f2_out1, z0, z1) → U3(f2_in(z1), z0, z1)
U3(f2_out1, z0, z1) → f59_out1

Tuples:

F59_IN(z0, z1) → c3(U2'(f2_in(z0), z0, z1), F2_IN(z0))
F2_IN(tree(z0, z1, z2)) → c1(F59_IN(z1, z2))
U2'(f2_out1, z0, z1) → c4(F2_IN(z1))

S tuples:

F59_IN(z0, z1) → c3(U2'(f2_in(z0), z0, z1), F2_IN(z0))

K tuples:

U2'(f2_out1, z0, z1) → c4(F2_IN(z1))
F2_IN(tree(z0, z1, z2)) → c1(F59_IN(z1, z2))

Defined Rule Symbols:

f2_in, U1, f59_in, U2, U3

Defined Pair Symbols:

F59_IN, F2_IN, U2'

Compound Symbols:

c3, c1, c4