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

0 Prolog
↳1 LPReorderTransformerProof (⇔, 0 ms)
↳2 Prolog
↳3 PrologToCdtProblemTransformerProof (UPPER BOUND (ID), 375 ms)
↳4 CdtProblem
    ↳5 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID), 5 ms)
    ↳6 CdtProblem
    ↳7 CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳8 CdtProblem
    ↳9 CdtKnowledgeProof (⇔, 0 ms)
    ↳10 CdtProblem
    ↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 910 ms)
    ↳12 CdtProblem
    ↳13 CdtKnowledgeProof (⇔, 0 ms)
    ↳14 CdtProblem
    ↳15 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 341 ms)
    ↳16 CdtProblem
↳17 PrologToCdtProblemTransformerProof (UPPER BOUND (ID), 350 ms)
↳18 CdtProblem
    ↳19 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID), 4 ms)
    ↳20 CdtProblem
    ↳21 CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳22 CdtProblem
    ↳23 CdtKnowledgeProof (⇔, 0 ms)
    ↳24 CdtProblem
    ↳25 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 851 ms)
    ↳26 CdtProblem
    ↳27 CdtKnowledgeProof (⇔, 0 ms)
    ↳28 CdtProblem
    ↳29 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 326 ms)
    ↳30 CdtProblem
    ↳31 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 284 ms)
    ↳32 CdtProblem
    ↳33 SIsEmptyProof (⇔, 0 ms)
    ↳34 BOUNDS(O(1), O(1))

(0) Obligation:

Clauses:

balance(T, TB) :- balance(T, -(I, []), -(.(','(TB, -(I, [])), X), X), -(Rest, []), -(Rest, [])).
balance(nil, -(X, X), -(A, B), -(A, B), -(.(','(nil, -(C, C)), T), T)).
balance(tree(L, V, R), -(IH, IT), -(.(','(tree(LB, VB, RB), -(A, D)), H), .(','(LB, -(A, .(VB, X))), .(','(RB, -(X, D)), T))), -(HR, TR), -(NH, NT)) :- ','(balance(L, -(IH, .(V, IT1)), -(H, T), -(HR1, TR1), -(NH, NT1)), balance(R, -(IT1, IT), -(HR1, TR1), -(HR, TR), -(NT1, NT))).

Query: balance(g,a)

(1) LPReorderTransformerProof (EQUIVALENT transformation)

Reordered facts before rules in definite LP [PROLOG].

(2) Obligation:

Clauses:

balance(nil, -(X, X), -(A, B), -(A, B), -(.(','(nil, -(C, C)), T), T)).
balance(T, TB) :- balance(T, -(I, []), -(.(','(TB, -(I, [])), X), X), -(Rest, []), -(Rest, [])).
balance(tree(L, V, R), -(IH, IT), -(.(','(tree(LB, VB, RB), -(A, D)), H), .(','(LB, -(A, .(VB, X))), .(','(RB, -(X, D)), T))), -(HR, TR), -(NH, NT)) :- ','(balance(L, -(IH, .(V, IT1)), -(H, T), -(HR1, TR1), -(NH, NT1)), balance(R, -(IT1, IT), -(HR1, TR1), -(HR, TR), -(NT1, NT))).

Query: balance(g,a)

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

Built complexity over-approximating cdt problems from derivation graph.

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(nil) → f1_out1
f1_in(tree(z0, z1, z2)) → U1(f19_in(z0, z1, z2), tree(z0, z1, z2))
U1(f19_out1, tree(z0, z1, z2)) → f1_out1
f42_in(nil, z0) → f42_out1
f42_in(tree(z0, z1, z2), z3) → U2(f53_in(z0, z1, z2, z3), tree(z0, z1, z2), z3)
U2(f53_out1, tree(z0, z1, z2), z3) → f42_out1
f24_in(nil) → f24_out1
f24_in(tree(z0, z1, z2)) → U3(f71_in(z0, z1, z2), tree(z0, z1, z2))
U3(f71_out1, tree(z0, z1, z2)) → f24_out1
f23_in(nil, z0) → f23_out1
f23_in(tree(z0, z1, z2), z3) → U4(f36_in(z0, z1, z2, z3), tree(z0, z1, z2), z3)
U4(f36_out1, tree(z0, z1, z2), z3) → f23_out1
f19_in(z0, z1, z2) → U5(f23_in(z0, z1), z0, z1, z2)
U5(f23_out1, z0, z1, z2) → U6(f24_in(z2), z0, z1, z2)
U6(f24_out1, z0, z1, z2) → f19_out1
f36_in(z0, z1, z2, z3) → U7(f42_in(z0, z1), z0, z1, z2, z3)
U7(f42_out1, z0, z1, z2, z3) → U8(f42_in(z2, z3), z0, z1, z2, z3)
U8(f42_out1, z0, z1, z2, z3) → f36_out1
f53_in(z0, z1, z2, z3) → U9(f42_in(z0, z1), z0, z1, z2, z3)
U9(f42_out1, z0, z1, z2, z3) → U10(f42_in(z2, z3), z0, z1, z2, z3)
U10(f42_out1, z0, z1, z2, z3) → f53_out1
f71_in(z0, z1, z2) → U11(f42_in(z0, z1), z0, z1, z2)
U11(f42_out1, z0, z1, z2) → U12(f24_in(z2), z0, z1, z2)
U12(f24_out1, z0, z1, z2) → f71_out1
Tuples:

F1_IN(tree(z0, z1, z2)) → c1(U1'(f19_in(z0, z1, z2), tree(z0, z1, z2)), F19_IN(z0, z1, z2))
F42_IN(tree(z0, z1, z2), z3) → c4(U2'(f53_in(z0, z1, z2, z3), tree(z0, z1, z2), z3), F53_IN(z0, z1, z2, z3))
F24_IN(tree(z0, z1, z2)) → c7(U3'(f71_in(z0, z1, z2), tree(z0, z1, z2)), F71_IN(z0, z1, z2))
F23_IN(tree(z0, z1, z2), z3) → c10(U4'(f36_in(z0, z1, z2, z3), tree(z0, z1, z2), z3), F36_IN(z0, z1, z2, z3))
F19_IN(z0, z1, z2) → c12(U5'(f23_in(z0, z1), z0, z1, z2), F23_IN(z0, z1))
U5'(f23_out1, z0, z1, z2) → c13(U6'(f24_in(z2), z0, z1, z2), F24_IN(z2))
F36_IN(z0, z1, z2, z3) → c15(U7'(f42_in(z0, z1), z0, z1, z2, z3), F42_IN(z0, z1))
U7'(f42_out1, z0, z1, z2, z3) → c16(U8'(f42_in(z2, z3), z0, z1, z2, z3), F42_IN(z2, z3))
F53_IN(z0, z1, z2, z3) → c18(U9'(f42_in(z0, z1), z0, z1, z2, z3), F42_IN(z0, z1))
U9'(f42_out1, z0, z1, z2, z3) → c19(U10'(f42_in(z2, z3), z0, z1, z2, z3), F42_IN(z2, z3))
F71_IN(z0, z1, z2) → c21(U11'(f42_in(z0, z1), z0, z1, z2), F42_IN(z0, z1))
U11'(f42_out1, z0, z1, z2) → c22(U12'(f24_in(z2), z0, z1, z2), F24_IN(z2))
S tuples:

F1_IN(tree(z0, z1, z2)) → c1(U1'(f19_in(z0, z1, z2), tree(z0, z1, z2)), F19_IN(z0, z1, z2))
F42_IN(tree(z0, z1, z2), z3) → c4(U2'(f53_in(z0, z1, z2, z3), tree(z0, z1, z2), z3), F53_IN(z0, z1, z2, z3))
F24_IN(tree(z0, z1, z2)) → c7(U3'(f71_in(z0, z1, z2), tree(z0, z1, z2)), F71_IN(z0, z1, z2))
F23_IN(tree(z0, z1, z2), z3) → c10(U4'(f36_in(z0, z1, z2, z3), tree(z0, z1, z2), z3), F36_IN(z0, z1, z2, z3))
F19_IN(z0, z1, z2) → c12(U5'(f23_in(z0, z1), z0, z1, z2), F23_IN(z0, z1))
U5'(f23_out1, z0, z1, z2) → c13(U6'(f24_in(z2), z0, z1, z2), F24_IN(z2))
F36_IN(z0, z1, z2, z3) → c15(U7'(f42_in(z0, z1), z0, z1, z2, z3), F42_IN(z0, z1))
U7'(f42_out1, z0, z1, z2, z3) → c16(U8'(f42_in(z2, z3), z0, z1, z2, z3), F42_IN(z2, z3))
F53_IN(z0, z1, z2, z3) → c18(U9'(f42_in(z0, z1), z0, z1, z2, z3), F42_IN(z0, z1))
U9'(f42_out1, z0, z1, z2, z3) → c19(U10'(f42_in(z2, z3), z0, z1, z2, z3), F42_IN(z2, z3))
F71_IN(z0, z1, z2) → c21(U11'(f42_in(z0, z1), z0, z1, z2), F42_IN(z0, z1))
U11'(f42_out1, z0, z1, z2) → c22(U12'(f24_in(z2), z0, z1, z2), F24_IN(z2))
K tuples:none
Defined Rule Symbols:

f1_in, U1, f42_in, U2, f24_in, U3, f23_in, U4, f19_in, U5, U6, f36_in, U7, U8, f53_in, U9, U10, f71_in, U11, U12

Defined Pair Symbols:

F1_IN, F42_IN, F24_IN, F23_IN, F19_IN, U5', F36_IN, U7', F53_IN, U9', F71_IN, U11'

Compound Symbols:

c1, c4, c7, c10, c12, c13, c15, c16, c18, c19, c21, c22

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

Split RHS of tuples not part of any SCC

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(nil) → f1_out1
f1_in(tree(z0, z1, z2)) → U1(f19_in(z0, z1, z2), tree(z0, z1, z2))
U1(f19_out1, tree(z0, z1, z2)) → f1_out1
f42_in(nil, z0) → f42_out1
f42_in(tree(z0, z1, z2), z3) → U2(f53_in(z0, z1, z2, z3), tree(z0, z1, z2), z3)
U2(f53_out1, tree(z0, z1, z2), z3) → f42_out1
f24_in(nil) → f24_out1
f24_in(tree(z0, z1, z2)) → U3(f71_in(z0, z1, z2), tree(z0, z1, z2))
U3(f71_out1, tree(z0, z1, z2)) → f24_out1
f23_in(nil, z0) → f23_out1
f23_in(tree(z0, z1, z2), z3) → U4(f36_in(z0, z1, z2, z3), tree(z0, z1, z2), z3)
U4(f36_out1, tree(z0, z1, z2), z3) → f23_out1
f19_in(z0, z1, z2) → U5(f23_in(z0, z1), z0, z1, z2)
U5(f23_out1, z0, z1, z2) → U6(f24_in(z2), z0, z1, z2)
U6(f24_out1, z0, z1, z2) → f19_out1
f36_in(z0, z1, z2, z3) → U7(f42_in(z0, z1), z0, z1, z2, z3)
U7(f42_out1, z0, z1, z2, z3) → U8(f42_in(z2, z3), z0, z1, z2, z3)
U8(f42_out1, z0, z1, z2, z3) → f36_out1
f53_in(z0, z1, z2, z3) → U9(f42_in(z0, z1), z0, z1, z2, z3)
U9(f42_out1, z0, z1, z2, z3) → U10(f42_in(z2, z3), z0, z1, z2, z3)
U10(f42_out1, z0, z1, z2, z3) → f53_out1
f71_in(z0, z1, z2) → U11(f42_in(z0, z1), z0, z1, z2)
U11(f42_out1, z0, z1, z2) → U12(f24_in(z2), z0, z1, z2)
U12(f24_out1, z0, z1, z2) → f71_out1
Tuples:

F42_IN(tree(z0, z1, z2), z3) → c4(U2'(f53_in(z0, z1, z2, z3), tree(z0, z1, z2), z3), F53_IN(z0, z1, z2, z3))
F24_IN(tree(z0, z1, z2)) → c7(U3'(f71_in(z0, z1, z2), tree(z0, z1, z2)), F71_IN(z0, z1, z2))
F53_IN(z0, z1, z2, z3) → c18(U9'(f42_in(z0, z1), z0, z1, z2, z3), F42_IN(z0, z1))
U9'(f42_out1, z0, z1, z2, z3) → c19(U10'(f42_in(z2, z3), z0, z1, z2, z3), F42_IN(z2, z3))
F71_IN(z0, z1, z2) → c21(U11'(f42_in(z0, z1), z0, z1, z2), F42_IN(z0, z1))
U11'(f42_out1, z0, z1, z2) → c22(U12'(f24_in(z2), z0, z1, z2), F24_IN(z2))
F1_IN(tree(z0, z1, z2)) → c(U1'(f19_in(z0, z1, z2), tree(z0, z1, z2)))
F1_IN(tree(z0, z1, z2)) → c(F19_IN(z0, z1, z2))
F23_IN(tree(z0, z1, z2), z3) → c(U4'(f36_in(z0, z1, z2, z3), tree(z0, z1, z2), z3))
F23_IN(tree(z0, z1, z2), z3) → c(F36_IN(z0, z1, z2, z3))
F19_IN(z0, z1, z2) → c(U5'(f23_in(z0, z1), z0, z1, z2))
F19_IN(z0, z1, z2) → c(F23_IN(z0, z1))
U5'(f23_out1, z0, z1, z2) → c(U6'(f24_in(z2), z0, z1, z2))
U5'(f23_out1, z0, z1, z2) → c(F24_IN(z2))
F36_IN(z0, z1, z2, z3) → c(U7'(f42_in(z0, z1), z0, z1, z2, z3))
F36_IN(z0, z1, z2, z3) → c(F42_IN(z0, z1))
U7'(f42_out1, z0, z1, z2, z3) → c(U8'(f42_in(z2, z3), z0, z1, z2, z3))
U7'(f42_out1, z0, z1, z2, z3) → c(F42_IN(z2, z3))
S tuples:

F42_IN(tree(z0, z1, z2), z3) → c4(U2'(f53_in(z0, z1, z2, z3), tree(z0, z1, z2), z3), F53_IN(z0, z1, z2, z3))
F24_IN(tree(z0, z1, z2)) → c7(U3'(f71_in(z0, z1, z2), tree(z0, z1, z2)), F71_IN(z0, z1, z2))
F53_IN(z0, z1, z2, z3) → c18(U9'(f42_in(z0, z1), z0, z1, z2, z3), F42_IN(z0, z1))
U9'(f42_out1, z0, z1, z2, z3) → c19(U10'(f42_in(z2, z3), z0, z1, z2, z3), F42_IN(z2, z3))
F71_IN(z0, z1, z2) → c21(U11'(f42_in(z0, z1), z0, z1, z2), F42_IN(z0, z1))
U11'(f42_out1, z0, z1, z2) → c22(U12'(f24_in(z2), z0, z1, z2), F24_IN(z2))
F1_IN(tree(z0, z1, z2)) → c(U1'(f19_in(z0, z1, z2), tree(z0, z1, z2)))
F1_IN(tree(z0, z1, z2)) → c(F19_IN(z0, z1, z2))
F23_IN(tree(z0, z1, z2), z3) → c(U4'(f36_in(z0, z1, z2, z3), tree(z0, z1, z2), z3))
F23_IN(tree(z0, z1, z2), z3) → c(F36_IN(z0, z1, z2, z3))
F19_IN(z0, z1, z2) → c(U5'(f23_in(z0, z1), z0, z1, z2))
F19_IN(z0, z1, z2) → c(F23_IN(z0, z1))
U5'(f23_out1, z0, z1, z2) → c(U6'(f24_in(z2), z0, z1, z2))
U5'(f23_out1, z0, z1, z2) → c(F24_IN(z2))
F36_IN(z0, z1, z2, z3) → c(U7'(f42_in(z0, z1), z0, z1, z2, z3))
F36_IN(z0, z1, z2, z3) → c(F42_IN(z0, z1))
U7'(f42_out1, z0, z1, z2, z3) → c(U8'(f42_in(z2, z3), z0, z1, z2, z3))
U7'(f42_out1, z0, z1, z2, z3) → c(F42_IN(z2, z3))
K tuples:none
Defined Rule Symbols:

f1_in, U1, f42_in, U2, f24_in, U3, f23_in, U4, f19_in, U5, U6, f36_in, U7, U8, f53_in, U9, U10, f71_in, U11, U12

Defined Pair Symbols:

F42_IN, F24_IN, F53_IN, U9', F71_IN, U11', F1_IN, F23_IN, F19_IN, U5', F36_IN, U7'

Compound Symbols:

c4, c7, c18, c19, c21, c22, c

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

Removed 8 trailing tuple parts

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(nil) → f1_out1
f1_in(tree(z0, z1, z2)) → U1(f19_in(z0, z1, z2), tree(z0, z1, z2))
U1(f19_out1, tree(z0, z1, z2)) → f1_out1
f42_in(nil, z0) → f42_out1
f42_in(tree(z0, z1, z2), z3) → U2(f53_in(z0, z1, z2, z3), tree(z0, z1, z2), z3)
U2(f53_out1, tree(z0, z1, z2), z3) → f42_out1
f24_in(nil) → f24_out1
f24_in(tree(z0, z1, z2)) → U3(f71_in(z0, z1, z2), tree(z0, z1, z2))
U3(f71_out1, tree(z0, z1, z2)) → f24_out1
f23_in(nil, z0) → f23_out1
f23_in(tree(z0, z1, z2), z3) → U4(f36_in(z0, z1, z2, z3), tree(z0, z1, z2), z3)
U4(f36_out1, tree(z0, z1, z2), z3) → f23_out1
f19_in(z0, z1, z2) → U5(f23_in(z0, z1), z0, z1, z2)
U5(f23_out1, z0, z1, z2) → U6(f24_in(z2), z0, z1, z2)
U6(f24_out1, z0, z1, z2) → f19_out1
f36_in(z0, z1, z2, z3) → U7(f42_in(z0, z1), z0, z1, z2, z3)
U7(f42_out1, z0, z1, z2, z3) → U8(f42_in(z2, z3), z0, z1, z2, z3)
U8(f42_out1, z0, z1, z2, z3) → f36_out1
f53_in(z0, z1, z2, z3) → U9(f42_in(z0, z1), z0, z1, z2, z3)
U9(f42_out1, z0, z1, z2, z3) → U10(f42_in(z2, z3), z0, z1, z2, z3)
U10(f42_out1, z0, z1, z2, z3) → f53_out1
f71_in(z0, z1, z2) → U11(f42_in(z0, z1), z0, z1, z2)
U11(f42_out1, z0, z1, z2) → U12(f24_in(z2), z0, z1, z2)
U12(f24_out1, z0, z1, z2) → f71_out1
Tuples:

F53_IN(z0, z1, z2, z3) → c18(U9'(f42_in(z0, z1), z0, z1, z2, z3), F42_IN(z0, z1))
F71_IN(z0, z1, z2) → c21(U11'(f42_in(z0, z1), z0, z1, z2), F42_IN(z0, z1))
F1_IN(tree(z0, z1, z2)) → c(F19_IN(z0, z1, z2))
F23_IN(tree(z0, z1, z2), z3) → c(F36_IN(z0, z1, z2, z3))
F19_IN(z0, z1, z2) → c(U5'(f23_in(z0, z1), z0, z1, z2))
F19_IN(z0, z1, z2) → c(F23_IN(z0, z1))
U5'(f23_out1, z0, z1, z2) → c(F24_IN(z2))
F36_IN(z0, z1, z2, z3) → c(U7'(f42_in(z0, z1), z0, z1, z2, z3))
F36_IN(z0, z1, z2, z3) → c(F42_IN(z0, z1))
U7'(f42_out1, z0, z1, z2, z3) → c(F42_IN(z2, z3))
F42_IN(tree(z0, z1, z2), z3) → c4(F53_IN(z0, z1, z2, z3))
F24_IN(tree(z0, z1, z2)) → c7(F71_IN(z0, z1, z2))
U9'(f42_out1, z0, z1, z2, z3) → c19(F42_IN(z2, z3))
U11'(f42_out1, z0, z1, z2) → c22(F24_IN(z2))
F1_IN(tree(z0, z1, z2)) → c
F23_IN(tree(z0, z1, z2), z3) → c
U5'(f23_out1, z0, z1, z2) → c
U7'(f42_out1, z0, z1, z2, z3) → c
S tuples:

F53_IN(z0, z1, z2, z3) → c18(U9'(f42_in(z0, z1), z0, z1, z2, z3), F42_IN(z0, z1))
F71_IN(z0, z1, z2) → c21(U11'(f42_in(z0, z1), z0, z1, z2), F42_IN(z0, z1))
F1_IN(tree(z0, z1, z2)) → c(F19_IN(z0, z1, z2))
F23_IN(tree(z0, z1, z2), z3) → c(F36_IN(z0, z1, z2, z3))
F19_IN(z0, z1, z2) → c(U5'(f23_in(z0, z1), z0, z1, z2))
F19_IN(z0, z1, z2) → c(F23_IN(z0, z1))
U5'(f23_out1, z0, z1, z2) → c(F24_IN(z2))
F36_IN(z0, z1, z2, z3) → c(U7'(f42_in(z0, z1), z0, z1, z2, z3))
F36_IN(z0, z1, z2, z3) → c(F42_IN(z0, z1))
U7'(f42_out1, z0, z1, z2, z3) → c(F42_IN(z2, z3))
F42_IN(tree(z0, z1, z2), z3) → c4(F53_IN(z0, z1, z2, z3))
F24_IN(tree(z0, z1, z2)) → c7(F71_IN(z0, z1, z2))
U9'(f42_out1, z0, z1, z2, z3) → c19(F42_IN(z2, z3))
U11'(f42_out1, z0, z1, z2) → c22(F24_IN(z2))
F1_IN(tree(z0, z1, z2)) → c
F23_IN(tree(z0, z1, z2), z3) → c
U5'(f23_out1, z0, z1, z2) → c
U7'(f42_out1, z0, z1, z2, z3) → c
K tuples:none
Defined Rule Symbols:

f1_in, U1, f42_in, U2, f24_in, U3, f23_in, U4, f19_in, U5, U6, f36_in, U7, U8, f53_in, U9, U10, f71_in, U11, U12

Defined Pair Symbols:

F53_IN, F71_IN, F1_IN, F23_IN, F19_IN, U5', F36_IN, U7', F42_IN, F24_IN, U9', U11'

Compound Symbols:

c18, c21, c, c4, c7, c19, c22, c

(9) CdtKnowledgeProof (EQUIVALENT transformation)

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

F1_IN(tree(z0, z1, z2)) → c(F19_IN(z0, z1, z2))
F19_IN(z0, z1, z2) → c(U5'(f23_in(z0, z1), z0, z1, z2))
F19_IN(z0, z1, z2) → c(F23_IN(z0, z1))
U5'(f23_out1, z0, z1, z2) → c(F24_IN(z2))
F1_IN(tree(z0, z1, z2)) → c
F23_IN(tree(z0, z1, z2), z3) → c
U5'(f23_out1, z0, z1, z2) → c
F19_IN(z0, z1, z2) → c(U5'(f23_in(z0, z1), z0, z1, z2))
F19_IN(z0, z1, z2) → c(F23_IN(z0, z1))
U5'(f23_out1, z0, z1, z2) → c(F24_IN(z2))
U5'(f23_out1, z0, z1, z2) → c
F23_IN(tree(z0, z1, z2), z3) → c(F36_IN(z0, z1, z2, z3))
F23_IN(tree(z0, z1, z2), z3) → c
F36_IN(z0, z1, z2, z3) → c(U7'(f42_in(z0, z1), z0, z1, z2, z3))
F36_IN(z0, z1, z2, z3) → c(F42_IN(z0, z1))
U7'(f42_out1, z0, z1, z2, z3) → c(F42_IN(z2, z3))
U7'(f42_out1, z0, z1, z2, z3) → c

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(nil) → f1_out1
f1_in(tree(z0, z1, z2)) → U1(f19_in(z0, z1, z2), tree(z0, z1, z2))
U1(f19_out1, tree(z0, z1, z2)) → f1_out1
f42_in(nil, z0) → f42_out1
f42_in(tree(z0, z1, z2), z3) → U2(f53_in(z0, z1, z2, z3), tree(z0, z1, z2), z3)
U2(f53_out1, tree(z0, z1, z2), z3) → f42_out1
f24_in(nil) → f24_out1
f24_in(tree(z0, z1, z2)) → U3(f71_in(z0, z1, z2), tree(z0, z1, z2))
U3(f71_out1, tree(z0, z1, z2)) → f24_out1
f23_in(nil, z0) → f23_out1
f23_in(tree(z0, z1, z2), z3) → U4(f36_in(z0, z1, z2, z3), tree(z0, z1, z2), z3)
U4(f36_out1, tree(z0, z1, z2), z3) → f23_out1
f19_in(z0, z1, z2) → U5(f23_in(z0, z1), z0, z1, z2)
U5(f23_out1, z0, z1, z2) → U6(f24_in(z2), z0, z1, z2)
U6(f24_out1, z0, z1, z2) → f19_out1
f36_in(z0, z1, z2, z3) → U7(f42_in(z0, z1), z0, z1, z2, z3)
U7(f42_out1, z0, z1, z2, z3) → U8(f42_in(z2, z3), z0, z1, z2, z3)
U8(f42_out1, z0, z1, z2, z3) → f36_out1
f53_in(z0, z1, z2, z3) → U9(f42_in(z0, z1), z0, z1, z2, z3)
U9(f42_out1, z0, z1, z2, z3) → U10(f42_in(z2, z3), z0, z1, z2, z3)
U10(f42_out1, z0, z1, z2, z3) → f53_out1
f71_in(z0, z1, z2) → U11(f42_in(z0, z1), z0, z1, z2)
U11(f42_out1, z0, z1, z2) → U12(f24_in(z2), z0, z1, z2)
U12(f24_out1, z0, z1, z2) → f71_out1
Tuples:

F53_IN(z0, z1, z2, z3) → c18(U9'(f42_in(z0, z1), z0, z1, z2, z3), F42_IN(z0, z1))
F71_IN(z0, z1, z2) → c21(U11'(f42_in(z0, z1), z0, z1, z2), F42_IN(z0, z1))
F1_IN(tree(z0, z1, z2)) → c(F19_IN(z0, z1, z2))
F23_IN(tree(z0, z1, z2), z3) → c(F36_IN(z0, z1, z2, z3))
F19_IN(z0, z1, z2) → c(U5'(f23_in(z0, z1), z0, z1, z2))
F19_IN(z0, z1, z2) → c(F23_IN(z0, z1))
U5'(f23_out1, z0, z1, z2) → c(F24_IN(z2))
F36_IN(z0, z1, z2, z3) → c(U7'(f42_in(z0, z1), z0, z1, z2, z3))
F36_IN(z0, z1, z2, z3) → c(F42_IN(z0, z1))
U7'(f42_out1, z0, z1, z2, z3) → c(F42_IN(z2, z3))
F42_IN(tree(z0, z1, z2), z3) → c4(F53_IN(z0, z1, z2, z3))
F24_IN(tree(z0, z1, z2)) → c7(F71_IN(z0, z1, z2))
U9'(f42_out1, z0, z1, z2, z3) → c19(F42_IN(z2, z3))
U11'(f42_out1, z0, z1, z2) → c22(F24_IN(z2))
F1_IN(tree(z0, z1, z2)) → c
F23_IN(tree(z0, z1, z2), z3) → c
U5'(f23_out1, z0, z1, z2) → c
U7'(f42_out1, z0, z1, z2, z3) → c
S tuples:

F53_IN(z0, z1, z2, z3) → c18(U9'(f42_in(z0, z1), z0, z1, z2, z3), F42_IN(z0, z1))
F71_IN(z0, z1, z2) → c21(U11'(f42_in(z0, z1), z0, z1, z2), F42_IN(z0, z1))
F42_IN(tree(z0, z1, z2), z3) → c4(F53_IN(z0, z1, z2, z3))
F24_IN(tree(z0, z1, z2)) → c7(F71_IN(z0, z1, z2))
U9'(f42_out1, z0, z1, z2, z3) → c19(F42_IN(z2, z3))
U11'(f42_out1, z0, z1, z2) → c22(F24_IN(z2))
K tuples:

F1_IN(tree(z0, z1, z2)) → c(F19_IN(z0, z1, z2))
F19_IN(z0, z1, z2) → c(U5'(f23_in(z0, z1), z0, z1, z2))
F19_IN(z0, z1, z2) → c(F23_IN(z0, z1))
U5'(f23_out1, z0, z1, z2) → c(F24_IN(z2))
F1_IN(tree(z0, z1, z2)) → c
F23_IN(tree(z0, z1, z2), z3) → c
U5'(f23_out1, z0, z1, z2) → c
F23_IN(tree(z0, z1, z2), z3) → c(F36_IN(z0, z1, z2, z3))
F36_IN(z0, z1, z2, z3) → c(U7'(f42_in(z0, z1), z0, z1, z2, z3))
F36_IN(z0, z1, z2, z3) → c(F42_IN(z0, z1))
U7'(f42_out1, z0, z1, z2, z3) → c(F42_IN(z2, z3))
U7'(f42_out1, z0, z1, z2, z3) → c
Defined Rule Symbols:

f1_in, U1, f42_in, U2, f24_in, U3, f23_in, U4, f19_in, U5, U6, f36_in, U7, U8, f53_in, U9, U10, f71_in, U11, U12

Defined Pair Symbols:

F53_IN, F71_IN, F1_IN, F23_IN, F19_IN, U5', F36_IN, U7', F42_IN, F24_IN, U9', U11'

Compound Symbols:

c18, c21, c, c4, c7, c19, c22, c

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

F24_IN(tree(z0, z1, z2)) → c7(F71_IN(z0, z1, z2))
We considered the (Usable) Rules:

f42_in(nil, z0) → f42_out1
f42_in(tree(z0, z1, z2), z3) → U2(f53_in(z0, z1, z2, z3), tree(z0, z1, z2), z3)
f53_in(z0, z1, z2, z3) → U9(f42_in(z0, z1), z0, z1, z2, z3)
U2(f53_out1, tree(z0, z1, z2), z3) → f42_out1
U9(f42_out1, z0, z1, z2, z3) → U10(f42_in(z2, z3), z0, z1, z2, z3)
U10(f42_out1, z0, z1, z2, z3) → f53_out1
f23_in(nil, z0) → f23_out1
f23_in(tree(z0, z1, z2), z3) → U4(f36_in(z0, z1, z2, z3), tree(z0, z1, z2), z3)
f36_in(z0, z1, z2, z3) → U7(f42_in(z0, z1), z0, z1, z2, z3)
U4(f36_out1, tree(z0, z1, z2), z3) → f23_out1
U7(f42_out1, z0, z1, z2, z3) → U8(f42_in(z2, z3), z0, z1, z2, z3)
U8(f42_out1, z0, z1, z2, z3) → f36_out1
And the Tuples:

F53_IN(z0, z1, z2, z3) → c18(U9'(f42_in(z0, z1), z0, z1, z2, z3), F42_IN(z0, z1))
F71_IN(z0, z1, z2) → c21(U11'(f42_in(z0, z1), z0, z1, z2), F42_IN(z0, z1))
F1_IN(tree(z0, z1, z2)) → c(F19_IN(z0, z1, z2))
F23_IN(tree(z0, z1, z2), z3) → c(F36_IN(z0, z1, z2, z3))
F19_IN(z0, z1, z2) → c(U5'(f23_in(z0, z1), z0, z1, z2))
F19_IN(z0, z1, z2) → c(F23_IN(z0, z1))
U5'(f23_out1, z0, z1, z2) → c(F24_IN(z2))
F36_IN(z0, z1, z2, z3) → c(U7'(f42_in(z0, z1), z0, z1, z2, z3))
F36_IN(z0, z1, z2, z3) → c(F42_IN(z0, z1))
U7'(f42_out1, z0, z1, z2, z3) → c(F42_IN(z2, z3))
F42_IN(tree(z0, z1, z2), z3) → c4(F53_IN(z0, z1, z2, z3))
F24_IN(tree(z0, z1, z2)) → c7(F71_IN(z0, z1, z2))
U9'(f42_out1, z0, z1, z2, z3) → c19(F42_IN(z2, z3))
U11'(f42_out1, z0, z1, z2) → c22(F24_IN(z2))
F1_IN(tree(z0, z1, z2)) → c
F23_IN(tree(z0, z1, z2), z3) → c
U5'(f23_out1, z0, z1, z2) → c
U7'(f42_out1, z0, z1, z2, z3) → c
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(F19_IN(x1, x2, x3)) = [3] + [2]x1 + [3]x2 + [2]x3   
POL(F1_IN(x1)) = [2] + [3]x1   
POL(F23_IN(x1, x2)) = [1] + [2]x1 + [3]x2   
POL(F24_IN(x1)) = x1   
POL(F36_IN(x1, x2, x3, x4)) = [2] + [3]x4   
POL(F42_IN(x1, x2)) = 0   
POL(F53_IN(x1, x2, x3, x4)) = 0   
POL(F71_IN(x1, x2, x3)) = x1 + x2 + x3   
POL(U10(x1, x2, x3, x4, x5)) = x1   
POL(U11'(x1, x2, x3, x4)) = x4   
POL(U2(x1, x2, x3)) = 0   
POL(U4(x1, x2, x3)) = 0   
POL(U5'(x1, x2, x3, x4)) = x2 + [3]x3 + x4   
POL(U7(x1, x2, x3, x4, x5)) = [2] + x4   
POL(U7'(x1, x2, x3, x4, x5)) = x5   
POL(U8(x1, x2, x3, x4, x5)) = [1]   
POL(U9(x1, x2, x3, x4, x5)) = [3]x4 + [2]x5   
POL(U9'(x1, x2, x3, x4, x5)) = 0   
POL(c) = 0   
POL(c(x1)) = x1   
POL(c18(x1, x2)) = x1 + x2   
POL(c19(x1)) = x1   
POL(c21(x1, x2)) = x1 + x2   
POL(c22(x1)) = x1   
POL(c4(x1)) = x1   
POL(c7(x1)) = x1   
POL(f23_in(x1, x2)) = 0   
POL(f23_out1) = 0   
POL(f36_in(x1, x2, x3, x4)) = [2] + [2]x1 + [2]x2 + [2]x3   
POL(f36_out1) = 0   
POL(f42_in(x1, x2)) = [2]x2   
POL(f42_out1) = 0   
POL(f53_in(x1, x2, x3, x4)) = [3]x3 + [2]x4   
POL(f53_out1) = 0   
POL(nil) = 0   
POL(tree(x1, x2, x3)) = [2] + x1 + x2 + x3   

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(nil) → f1_out1
f1_in(tree(z0, z1, z2)) → U1(f19_in(z0, z1, z2), tree(z0, z1, z2))
U1(f19_out1, tree(z0, z1, z2)) → f1_out1
f42_in(nil, z0) → f42_out1
f42_in(tree(z0, z1, z2), z3) → U2(f53_in(z0, z1, z2, z3), tree(z0, z1, z2), z3)
U2(f53_out1, tree(z0, z1, z2), z3) → f42_out1
f24_in(nil) → f24_out1
f24_in(tree(z0, z1, z2)) → U3(f71_in(z0, z1, z2), tree(z0, z1, z2))
U3(f71_out1, tree(z0, z1, z2)) → f24_out1
f23_in(nil, z0) → f23_out1
f23_in(tree(z0, z1, z2), z3) → U4(f36_in(z0, z1, z2, z3), tree(z0, z1, z2), z3)
U4(f36_out1, tree(z0, z1, z2), z3) → f23_out1
f19_in(z0, z1, z2) → U5(f23_in(z0, z1), z0, z1, z2)
U5(f23_out1, z0, z1, z2) → U6(f24_in(z2), z0, z1, z2)
U6(f24_out1, z0, z1, z2) → f19_out1
f36_in(z0, z1, z2, z3) → U7(f42_in(z0, z1), z0, z1, z2, z3)
U7(f42_out1, z0, z1, z2, z3) → U8(f42_in(z2, z3), z0, z1, z2, z3)
U8(f42_out1, z0, z1, z2, z3) → f36_out1
f53_in(z0, z1, z2, z3) → U9(f42_in(z0, z1), z0, z1, z2, z3)
U9(f42_out1, z0, z1, z2, z3) → U10(f42_in(z2, z3), z0, z1, z2, z3)
U10(f42_out1, z0, z1, z2, z3) → f53_out1
f71_in(z0, z1, z2) → U11(f42_in(z0, z1), z0, z1, z2)
U11(f42_out1, z0, z1, z2) → U12(f24_in(z2), z0, z1, z2)
U12(f24_out1, z0, z1, z2) → f71_out1
Tuples:

F53_IN(z0, z1, z2, z3) → c18(U9'(f42_in(z0, z1), z0, z1, z2, z3), F42_IN(z0, z1))
F71_IN(z0, z1, z2) → c21(U11'(f42_in(z0, z1), z0, z1, z2), F42_IN(z0, z1))
F1_IN(tree(z0, z1, z2)) → c(F19_IN(z0, z1, z2))
F23_IN(tree(z0, z1, z2), z3) → c(F36_IN(z0, z1, z2, z3))
F19_IN(z0, z1, z2) → c(U5'(f23_in(z0, z1), z0, z1, z2))
F19_IN(z0, z1, z2) → c(F23_IN(z0, z1))
U5'(f23_out1, z0, z1, z2) → c(F24_IN(z2))
F36_IN(z0, z1, z2, z3) → c(U7'(f42_in(z0, z1), z0, z1, z2, z3))
F36_IN(z0, z1, z2, z3) → c(F42_IN(z0, z1))
U7'(f42_out1, z0, z1, z2, z3) → c(F42_IN(z2, z3))
F42_IN(tree(z0, z1, z2), z3) → c4(F53_IN(z0, z1, z2, z3))
F24_IN(tree(z0, z1, z2)) → c7(F71_IN(z0, z1, z2))
U9'(f42_out1, z0, z1, z2, z3) → c19(F42_IN(z2, z3))
U11'(f42_out1, z0, z1, z2) → c22(F24_IN(z2))
F1_IN(tree(z0, z1, z2)) → c
F23_IN(tree(z0, z1, z2), z3) → c
U5'(f23_out1, z0, z1, z2) → c
U7'(f42_out1, z0, z1, z2, z3) → c
S tuples:

F53_IN(z0, z1, z2, z3) → c18(U9'(f42_in(z0, z1), z0, z1, z2, z3), F42_IN(z0, z1))
F71_IN(z0, z1, z2) → c21(U11'(f42_in(z0, z1), z0, z1, z2), F42_IN(z0, z1))
F42_IN(tree(z0, z1, z2), z3) → c4(F53_IN(z0, z1, z2, z3))
U9'(f42_out1, z0, z1, z2, z3) → c19(F42_IN(z2, z3))
U11'(f42_out1, z0, z1, z2) → c22(F24_IN(z2))
K tuples:

F1_IN(tree(z0, z1, z2)) → c(F19_IN(z0, z1, z2))
F19_IN(z0, z1, z2) → c(U5'(f23_in(z0, z1), z0, z1, z2))
F19_IN(z0, z1, z2) → c(F23_IN(z0, z1))
U5'(f23_out1, z0, z1, z2) → c(F24_IN(z2))
F1_IN(tree(z0, z1, z2)) → c
F23_IN(tree(z0, z1, z2), z3) → c
U5'(f23_out1, z0, z1, z2) → c
F23_IN(tree(z0, z1, z2), z3) → c(F36_IN(z0, z1, z2, z3))
F36_IN(z0, z1, z2, z3) → c(U7'(f42_in(z0, z1), z0, z1, z2, z3))
F36_IN(z0, z1, z2, z3) → c(F42_IN(z0, z1))
U7'(f42_out1, z0, z1, z2, z3) → c(F42_IN(z2, z3))
U7'(f42_out1, z0, z1, z2, z3) → c
F24_IN(tree(z0, z1, z2)) → c7(F71_IN(z0, z1, z2))
Defined Rule Symbols:

f1_in, U1, f42_in, U2, f24_in, U3, f23_in, U4, f19_in, U5, U6, f36_in, U7, U8, f53_in, U9, U10, f71_in, U11, U12

Defined Pair Symbols:

F53_IN, F71_IN, F1_IN, F23_IN, F19_IN, U5', F36_IN, U7', F42_IN, F24_IN, U9', U11'

Compound Symbols:

c18, c21, c, c4, c7, c19, c22, c

(13) CdtKnowledgeProof (EQUIVALENT transformation)

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

F71_IN(z0, z1, z2) → c21(U11'(f42_in(z0, z1), z0, z1, z2), F42_IN(z0, z1))
U11'(f42_out1, z0, z1, z2) → c22(F24_IN(z2))
U11'(f42_out1, z0, z1, z2) → c22(F24_IN(z2))
F24_IN(tree(z0, z1, z2)) → c7(F71_IN(z0, z1, z2))

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(nil) → f1_out1
f1_in(tree(z0, z1, z2)) → U1(f19_in(z0, z1, z2), tree(z0, z1, z2))
U1(f19_out1, tree(z0, z1, z2)) → f1_out1
f42_in(nil, z0) → f42_out1
f42_in(tree(z0, z1, z2), z3) → U2(f53_in(z0, z1, z2, z3), tree(z0, z1, z2), z3)
U2(f53_out1, tree(z0, z1, z2), z3) → f42_out1
f24_in(nil) → f24_out1
f24_in(tree(z0, z1, z2)) → U3(f71_in(z0, z1, z2), tree(z0, z1, z2))
U3(f71_out1, tree(z0, z1, z2)) → f24_out1
f23_in(nil, z0) → f23_out1
f23_in(tree(z0, z1, z2), z3) → U4(f36_in(z0, z1, z2, z3), tree(z0, z1, z2), z3)
U4(f36_out1, tree(z0, z1, z2), z3) → f23_out1
f19_in(z0, z1, z2) → U5(f23_in(z0, z1), z0, z1, z2)
U5(f23_out1, z0, z1, z2) → U6(f24_in(z2), z0, z1, z2)
U6(f24_out1, z0, z1, z2) → f19_out1
f36_in(z0, z1, z2, z3) → U7(f42_in(z0, z1), z0, z1, z2, z3)
U7(f42_out1, z0, z1, z2, z3) → U8(f42_in(z2, z3), z0, z1, z2, z3)
U8(f42_out1, z0, z1, z2, z3) → f36_out1
f53_in(z0, z1, z2, z3) → U9(f42_in(z0, z1), z0, z1, z2, z3)
U9(f42_out1, z0, z1, z2, z3) → U10(f42_in(z2, z3), z0, z1, z2, z3)
U10(f42_out1, z0, z1, z2, z3) → f53_out1
f71_in(z0, z1, z2) → U11(f42_in(z0, z1), z0, z1, z2)
U11(f42_out1, z0, z1, z2) → U12(f24_in(z2), z0, z1, z2)
U12(f24_out1, z0, z1, z2) → f71_out1
Tuples:

F53_IN(z0, z1, z2, z3) → c18(U9'(f42_in(z0, z1), z0, z1, z2, z3), F42_IN(z0, z1))
F71_IN(z0, z1, z2) → c21(U11'(f42_in(z0, z1), z0, z1, z2), F42_IN(z0, z1))
F1_IN(tree(z0, z1, z2)) → c(F19_IN(z0, z1, z2))
F23_IN(tree(z0, z1, z2), z3) → c(F36_IN(z0, z1, z2, z3))
F19_IN(z0, z1, z2) → c(U5'(f23_in(z0, z1), z0, z1, z2))
F19_IN(z0, z1, z2) → c(F23_IN(z0, z1))
U5'(f23_out1, z0, z1, z2) → c(F24_IN(z2))
F36_IN(z0, z1, z2, z3) → c(U7'(f42_in(z0, z1), z0, z1, z2, z3))
F36_IN(z0, z1, z2, z3) → c(F42_IN(z0, z1))
U7'(f42_out1, z0, z1, z2, z3) → c(F42_IN(z2, z3))
F42_IN(tree(z0, z1, z2), z3) → c4(F53_IN(z0, z1, z2, z3))
F24_IN(tree(z0, z1, z2)) → c7(F71_IN(z0, z1, z2))
U9'(f42_out1, z0, z1, z2, z3) → c19(F42_IN(z2, z3))
U11'(f42_out1, z0, z1, z2) → c22(F24_IN(z2))
F1_IN(tree(z0, z1, z2)) → c
F23_IN(tree(z0, z1, z2), z3) → c
U5'(f23_out1, z0, z1, z2) → c
U7'(f42_out1, z0, z1, z2, z3) → c
S tuples:

F53_IN(z0, z1, z2, z3) → c18(U9'(f42_in(z0, z1), z0, z1, z2, z3), F42_IN(z0, z1))
F42_IN(tree(z0, z1, z2), z3) → c4(F53_IN(z0, z1, z2, z3))
U9'(f42_out1, z0, z1, z2, z3) → c19(F42_IN(z2, z3))
K tuples:

F1_IN(tree(z0, z1, z2)) → c(F19_IN(z0, z1, z2))
F19_IN(z0, z1, z2) → c(U5'(f23_in(z0, z1), z0, z1, z2))
F19_IN(z0, z1, z2) → c(F23_IN(z0, z1))
U5'(f23_out1, z0, z1, z2) → c(F24_IN(z2))
F1_IN(tree(z0, z1, z2)) → c
F23_IN(tree(z0, z1, z2), z3) → c
U5'(f23_out1, z0, z1, z2) → c
F23_IN(tree(z0, z1, z2), z3) → c(F36_IN(z0, z1, z2, z3))
F36_IN(z0, z1, z2, z3) → c(U7'(f42_in(z0, z1), z0, z1, z2, z3))
F36_IN(z0, z1, z2, z3) → c(F42_IN(z0, z1))
U7'(f42_out1, z0, z1, z2, z3) → c(F42_IN(z2, z3))
U7'(f42_out1, z0, z1, z2, z3) → c
F24_IN(tree(z0, z1, z2)) → c7(F71_IN(z0, z1, z2))
F71_IN(z0, z1, z2) → c21(U11'(f42_in(z0, z1), z0, z1, z2), F42_IN(z0, z1))
U11'(f42_out1, z0, z1, z2) → c22(F24_IN(z2))
Defined Rule Symbols:

f1_in, U1, f42_in, U2, f24_in, U3, f23_in, U4, f19_in, U5, U6, f36_in, U7, U8, f53_in, U9, U10, f71_in, U11, U12

Defined Pair Symbols:

F53_IN, F71_IN, F1_IN, F23_IN, F19_IN, U5', F36_IN, U7', F42_IN, F24_IN, U9', U11'

Compound Symbols:

c18, c21, c, c4, c7, c19, c22, c

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

U9'(f42_out1, z0, z1, z2, z3) → c19(F42_IN(z2, z3))
We considered the (Usable) Rules:

f42_in(nil, z0) → f42_out1
f42_in(tree(z0, z1, z2), z3) → U2(f53_in(z0, z1, z2, z3), tree(z0, z1, z2), z3)
f53_in(z0, z1, z2, z3) → U9(f42_in(z0, z1), z0, z1, z2, z3)
U2(f53_out1, tree(z0, z1, z2), z3) → f42_out1
U9(f42_out1, z0, z1, z2, z3) → U10(f42_in(z2, z3), z0, z1, z2, z3)
U10(f42_out1, z0, z1, z2, z3) → f53_out1
f23_in(nil, z0) → f23_out1
f23_in(tree(z0, z1, z2), z3) → U4(f36_in(z0, z1, z2, z3), tree(z0, z1, z2), z3)
f36_in(z0, z1, z2, z3) → U7(f42_in(z0, z1), z0, z1, z2, z3)
U4(f36_out1, tree(z0, z1, z2), z3) → f23_out1
U7(f42_out1, z0, z1, z2, z3) → U8(f42_in(z2, z3), z0, z1, z2, z3)
U8(f42_out1, z0, z1, z2, z3) → f36_out1
And the Tuples:

F53_IN(z0, z1, z2, z3) → c18(U9'(f42_in(z0, z1), z0, z1, z2, z3), F42_IN(z0, z1))
F71_IN(z0, z1, z2) → c21(U11'(f42_in(z0, z1), z0, z1, z2), F42_IN(z0, z1))
F1_IN(tree(z0, z1, z2)) → c(F19_IN(z0, z1, z2))
F23_IN(tree(z0, z1, z2), z3) → c(F36_IN(z0, z1, z2, z3))
F19_IN(z0, z1, z2) → c(U5'(f23_in(z0, z1), z0, z1, z2))
F19_IN(z0, z1, z2) → c(F23_IN(z0, z1))
U5'(f23_out1, z0, z1, z2) → c(F24_IN(z2))
F36_IN(z0, z1, z2, z3) → c(U7'(f42_in(z0, z1), z0, z1, z2, z3))
F36_IN(z0, z1, z2, z3) → c(F42_IN(z0, z1))
U7'(f42_out1, z0, z1, z2, z3) → c(F42_IN(z2, z3))
F42_IN(tree(z0, z1, z2), z3) → c4(F53_IN(z0, z1, z2, z3))
F24_IN(tree(z0, z1, z2)) → c7(F71_IN(z0, z1, z2))
U9'(f42_out1, z0, z1, z2, z3) → c19(F42_IN(z2, z3))
U11'(f42_out1, z0, z1, z2) → c22(F24_IN(z2))
F1_IN(tree(z0, z1, z2)) → c
F23_IN(tree(z0, z1, z2), z3) → c
U5'(f23_out1, z0, z1, z2) → c
U7'(f42_out1, z0, z1, z2, z3) → c
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(F19_IN(x1, x2, x3)) = [3] + [3]x1 + [3]x2 + [3]x3   
POL(F1_IN(x1)) = [2] + [3]x1   
POL(F23_IN(x1, x2)) = [2] + [3]x1 + [2]x2   
POL(F24_IN(x1)) = x1   
POL(F36_IN(x1, x2, x3, x4)) = [3] + x1 + [3]x2 + [2]x3 + x4   
POL(F42_IN(x1, x2)) = x1   
POL(F53_IN(x1, x2, x3, x4)) = [1] + x1 + x2 + x3   
POL(F71_IN(x1, x2, x3)) = x1 + x2 + x3   
POL(U10(x1, x2, x3, x4, x5)) = [1] + x3   
POL(U11'(x1, x2, x3, x4)) = x4   
POL(U2(x1, x2, x3)) = 0   
POL(U4(x1, x2, x3)) = [2] + x1 + x2   
POL(U5'(x1, x2, x3, x4)) = [3] + [3]x3 + [2]x4   
POL(U7(x1, x2, x3, x4, x5)) = x4 + x5   
POL(U7'(x1, x2, x3, x4, x5)) = [3] + [3]x3 + x4 + x5   
POL(U8(x1, x2, x3, x4, x5)) = x4   
POL(U9(x1, x2, x3, x4, x5)) = [2] + x3   
POL(U9'(x1, x2, x3, x4, x5)) = [1] + x4   
POL(c) = 0   
POL(c(x1)) = x1   
POL(c18(x1, x2)) = x1 + x2   
POL(c19(x1)) = x1   
POL(c21(x1, x2)) = x1 + x2   
POL(c22(x1)) = x1   
POL(c4(x1)) = x1   
POL(c7(x1)) = x1   
POL(f23_in(x1, x2)) = [2] + [2]x1 + [2]x2   
POL(f23_out1) = [2]   
POL(f36_in(x1, x2, x3, x4)) = x1 + x2 + x3 + [2]x4   
POL(f36_out1) = 0   
POL(f42_in(x1, x2)) = 0   
POL(f42_out1) = 0   
POL(f53_in(x1, x2, x3, x4)) = [2] + [2]x1 + [2]x2 + x4   
POL(f53_out1) = [1]   
POL(nil) = [1]   
POL(tree(x1, x2, x3)) = [1] + x1 + x2 + x3   

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(nil) → f1_out1
f1_in(tree(z0, z1, z2)) → U1(f19_in(z0, z1, z2), tree(z0, z1, z2))
U1(f19_out1, tree(z0, z1, z2)) → f1_out1
f42_in(nil, z0) → f42_out1
f42_in(tree(z0, z1, z2), z3) → U2(f53_in(z0, z1, z2, z3), tree(z0, z1, z2), z3)
U2(f53_out1, tree(z0, z1, z2), z3) → f42_out1
f24_in(nil) → f24_out1
f24_in(tree(z0, z1, z2)) → U3(f71_in(z0, z1, z2), tree(z0, z1, z2))
U3(f71_out1, tree(z0, z1, z2)) → f24_out1
f23_in(nil, z0) → f23_out1
f23_in(tree(z0, z1, z2), z3) → U4(f36_in(z0, z1, z2, z3), tree(z0, z1, z2), z3)
U4(f36_out1, tree(z0, z1, z2), z3) → f23_out1
f19_in(z0, z1, z2) → U5(f23_in(z0, z1), z0, z1, z2)
U5(f23_out1, z0, z1, z2) → U6(f24_in(z2), z0, z1, z2)
U6(f24_out1, z0, z1, z2) → f19_out1
f36_in(z0, z1, z2, z3) → U7(f42_in(z0, z1), z0, z1, z2, z3)
U7(f42_out1, z0, z1, z2, z3) → U8(f42_in(z2, z3), z0, z1, z2, z3)
U8(f42_out1, z0, z1, z2, z3) → f36_out1
f53_in(z0, z1, z2, z3) → U9(f42_in(z0, z1), z0, z1, z2, z3)
U9(f42_out1, z0, z1, z2, z3) → U10(f42_in(z2, z3), z0, z1, z2, z3)
U10(f42_out1, z0, z1, z2, z3) → f53_out1
f71_in(z0, z1, z2) → U11(f42_in(z0, z1), z0, z1, z2)
U11(f42_out1, z0, z1, z2) → U12(f24_in(z2), z0, z1, z2)
U12(f24_out1, z0, z1, z2) → f71_out1
Tuples:

F53_IN(z0, z1, z2, z3) → c18(U9'(f42_in(z0, z1), z0, z1, z2, z3), F42_IN(z0, z1))
F71_IN(z0, z1, z2) → c21(U11'(f42_in(z0, z1), z0, z1, z2), F42_IN(z0, z1))
F1_IN(tree(z0, z1, z2)) → c(F19_IN(z0, z1, z2))
F23_IN(tree(z0, z1, z2), z3) → c(F36_IN(z0, z1, z2, z3))
F19_IN(z0, z1, z2) → c(U5'(f23_in(z0, z1), z0, z1, z2))
F19_IN(z0, z1, z2) → c(F23_IN(z0, z1))
U5'(f23_out1, z0, z1, z2) → c(F24_IN(z2))
F36_IN(z0, z1, z2, z3) → c(U7'(f42_in(z0, z1), z0, z1, z2, z3))
F36_IN(z0, z1, z2, z3) → c(F42_IN(z0, z1))
U7'(f42_out1, z0, z1, z2, z3) → c(F42_IN(z2, z3))
F42_IN(tree(z0, z1, z2), z3) → c4(F53_IN(z0, z1, z2, z3))
F24_IN(tree(z0, z1, z2)) → c7(F71_IN(z0, z1, z2))
U9'(f42_out1, z0, z1, z2, z3) → c19(F42_IN(z2, z3))
U11'(f42_out1, z0, z1, z2) → c22(F24_IN(z2))
F1_IN(tree(z0, z1, z2)) → c
F23_IN(tree(z0, z1, z2), z3) → c
U5'(f23_out1, z0, z1, z2) → c
U7'(f42_out1, z0, z1, z2, z3) → c
S tuples:

F53_IN(z0, z1, z2, z3) → c18(U9'(f42_in(z0, z1), z0, z1, z2, z3), F42_IN(z0, z1))
F42_IN(tree(z0, z1, z2), z3) → c4(F53_IN(z0, z1, z2, z3))
K tuples:

F1_IN(tree(z0, z1, z2)) → c(F19_IN(z0, z1, z2))
F19_IN(z0, z1, z2) → c(U5'(f23_in(z0, z1), z0, z1, z2))
F19_IN(z0, z1, z2) → c(F23_IN(z0, z1))
U5'(f23_out1, z0, z1, z2) → c(F24_IN(z2))
F1_IN(tree(z0, z1, z2)) → c
F23_IN(tree(z0, z1, z2), z3) → c
U5'(f23_out1, z0, z1, z2) → c
F23_IN(tree(z0, z1, z2), z3) → c(F36_IN(z0, z1, z2, z3))
F36_IN(z0, z1, z2, z3) → c(U7'(f42_in(z0, z1), z0, z1, z2, z3))
F36_IN(z0, z1, z2, z3) → c(F42_IN(z0, z1))
U7'(f42_out1, z0, z1, z2, z3) → c(F42_IN(z2, z3))
U7'(f42_out1, z0, z1, z2, z3) → c
F24_IN(tree(z0, z1, z2)) → c7(F71_IN(z0, z1, z2))
F71_IN(z0, z1, z2) → c21(U11'(f42_in(z0, z1), z0, z1, z2), F42_IN(z0, z1))
U11'(f42_out1, z0, z1, z2) → c22(F24_IN(z2))
U9'(f42_out1, z0, z1, z2, z3) → c19(F42_IN(z2, z3))
Defined Rule Symbols:

f1_in, U1, f42_in, U2, f24_in, U3, f23_in, U4, f19_in, U5, U6, f36_in, U7, U8, f53_in, U9, U10, f71_in, U11, U12

Defined Pair Symbols:

F53_IN, F71_IN, F1_IN, F23_IN, F19_IN, U5', F36_IN, U7', F42_IN, F24_IN, U9', U11'

Compound Symbols:

c18, c21, c, c4, c7, c19, c22, c

(17) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)

Built complexity over-approximating cdt problems from derivation graph.

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(nil) → f2_out1
f2_in(tree(z0, z1, z2)) → U1(f17_in(z0, z1, z2), tree(z0, z1, z2))
U1(f17_out1, tree(z0, z1, z2)) → f2_out1
f40_in(nil, z0) → f40_out1
f40_in(tree(z0, z1, z2), z3) → U2(f55_in(z0, z1, z2, z3), tree(z0, z1, z2), z3)
U2(f55_out1, tree(z0, z1, z2), z3) → f40_out1
f22_in(nil) → f22_out1
f22_in(tree(z0, z1, z2)) → U3(f73_in(z0, z1, z2), tree(z0, z1, z2))
U3(f73_out1, tree(z0, z1, z2)) → f22_out1
f21_in(nil, z0) → f21_out1
f21_in(tree(z0, z1, z2), z3) → U4(f35_in(z0, z1, z2, z3), tree(z0, z1, z2), z3)
U4(f35_out1, tree(z0, z1, z2), z3) → f21_out1
f17_in(z0, z1, z2) → U5(f21_in(z0, z1), z0, z1, z2)
U5(f21_out1, z0, z1, z2) → U6(f22_in(z2), z0, z1, z2)
U6(f22_out1, z0, z1, z2) → f17_out1
f35_in(z0, z1, z2, z3) → U7(f40_in(z0, z1), z0, z1, z2, z3)
U7(f40_out1, z0, z1, z2, z3) → U8(f40_in(z2, z3), z0, z1, z2, z3)
U8(f40_out1, z0, z1, z2, z3) → f35_out1
f55_in(z0, z1, z2, z3) → U9(f40_in(z0, z1), z0, z1, z2, z3)
U9(f40_out1, z0, z1, z2, z3) → U10(f40_in(z2, z3), z0, z1, z2, z3)
U10(f40_out1, z0, z1, z2, z3) → f55_out1
f73_in(z0, z1, z2) → U11(f40_in(z0, z1), z0, z1, z2)
U11(f40_out1, z0, z1, z2) → U12(f22_in(z2), z0, z1, z2)
U12(f22_out1, z0, z1, z2) → f73_out1
Tuples:

F2_IN(tree(z0, z1, z2)) → c1(U1'(f17_in(z0, z1, z2), tree(z0, z1, z2)), F17_IN(z0, z1, z2))
F40_IN(tree(z0, z1, z2), z3) → c4(U2'(f55_in(z0, z1, z2, z3), tree(z0, z1, z2), z3), F55_IN(z0, z1, z2, z3))
F22_IN(tree(z0, z1, z2)) → c7(U3'(f73_in(z0, z1, z2), tree(z0, z1, z2)), F73_IN(z0, z1, z2))
F21_IN(tree(z0, z1, z2), z3) → c10(U4'(f35_in(z0, z1, z2, z3), tree(z0, z1, z2), z3), F35_IN(z0, z1, z2, z3))
F17_IN(z0, z1, z2) → c12(U5'(f21_in(z0, z1), z0, z1, z2), F21_IN(z0, z1))
U5'(f21_out1, z0, z1, z2) → c13(U6'(f22_in(z2), z0, z1, z2), F22_IN(z2))
F35_IN(z0, z1, z2, z3) → c15(U7'(f40_in(z0, z1), z0, z1, z2, z3), F40_IN(z0, z1))
U7'(f40_out1, z0, z1, z2, z3) → c16(U8'(f40_in(z2, z3), z0, z1, z2, z3), F40_IN(z2, z3))
F55_IN(z0, z1, z2, z3) → c18(U9'(f40_in(z0, z1), z0, z1, z2, z3), F40_IN(z0, z1))
U9'(f40_out1, z0, z1, z2, z3) → c19(U10'(f40_in(z2, z3), z0, z1, z2, z3), F40_IN(z2, z3))
F73_IN(z0, z1, z2) → c21(U11'(f40_in(z0, z1), z0, z1, z2), F40_IN(z0, z1))
U11'(f40_out1, z0, z1, z2) → c22(U12'(f22_in(z2), z0, z1, z2), F22_IN(z2))
S tuples:

F2_IN(tree(z0, z1, z2)) → c1(U1'(f17_in(z0, z1, z2), tree(z0, z1, z2)), F17_IN(z0, z1, z2))
F40_IN(tree(z0, z1, z2), z3) → c4(U2'(f55_in(z0, z1, z2, z3), tree(z0, z1, z2), z3), F55_IN(z0, z1, z2, z3))
F22_IN(tree(z0, z1, z2)) → c7(U3'(f73_in(z0, z1, z2), tree(z0, z1, z2)), F73_IN(z0, z1, z2))
F21_IN(tree(z0, z1, z2), z3) → c10(U4'(f35_in(z0, z1, z2, z3), tree(z0, z1, z2), z3), F35_IN(z0, z1, z2, z3))
F17_IN(z0, z1, z2) → c12(U5'(f21_in(z0, z1), z0, z1, z2), F21_IN(z0, z1))
U5'(f21_out1, z0, z1, z2) → c13(U6'(f22_in(z2), z0, z1, z2), F22_IN(z2))
F35_IN(z0, z1, z2, z3) → c15(U7'(f40_in(z0, z1), z0, z1, z2, z3), F40_IN(z0, z1))
U7'(f40_out1, z0, z1, z2, z3) → c16(U8'(f40_in(z2, z3), z0, z1, z2, z3), F40_IN(z2, z3))
F55_IN(z0, z1, z2, z3) → c18(U9'(f40_in(z0, z1), z0, z1, z2, z3), F40_IN(z0, z1))
U9'(f40_out1, z0, z1, z2, z3) → c19(U10'(f40_in(z2, z3), z0, z1, z2, z3), F40_IN(z2, z3))
F73_IN(z0, z1, z2) → c21(U11'(f40_in(z0, z1), z0, z1, z2), F40_IN(z0, z1))
U11'(f40_out1, z0, z1, z2) → c22(U12'(f22_in(z2), z0, z1, z2), F22_IN(z2))
K tuples:none
Defined Rule Symbols:

f2_in, U1, f40_in, U2, f22_in, U3, f21_in, U4, f17_in, U5, U6, f35_in, U7, U8, f55_in, U9, U10, f73_in, U11, U12

Defined Pair Symbols:

F2_IN, F40_IN, F22_IN, F21_IN, F17_IN, U5', F35_IN, U7', F55_IN, U9', F73_IN, U11'

Compound Symbols:

c1, c4, c7, c10, c12, c13, c15, c16, c18, c19, c21, c22

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

Split RHS of tuples not part of any SCC

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(nil) → f2_out1
f2_in(tree(z0, z1, z2)) → U1(f17_in(z0, z1, z2), tree(z0, z1, z2))
U1(f17_out1, tree(z0, z1, z2)) → f2_out1
f40_in(nil, z0) → f40_out1
f40_in(tree(z0, z1, z2), z3) → U2(f55_in(z0, z1, z2, z3), tree(z0, z1, z2), z3)
U2(f55_out1, tree(z0, z1, z2), z3) → f40_out1
f22_in(nil) → f22_out1
f22_in(tree(z0, z1, z2)) → U3(f73_in(z0, z1, z2), tree(z0, z1, z2))
U3(f73_out1, tree(z0, z1, z2)) → f22_out1
f21_in(nil, z0) → f21_out1
f21_in(tree(z0, z1, z2), z3) → U4(f35_in(z0, z1, z2, z3), tree(z0, z1, z2), z3)
U4(f35_out1, tree(z0, z1, z2), z3) → f21_out1
f17_in(z0, z1, z2) → U5(f21_in(z0, z1), z0, z1, z2)
U5(f21_out1, z0, z1, z2) → U6(f22_in(z2), z0, z1, z2)
U6(f22_out1, z0, z1, z2) → f17_out1
f35_in(z0, z1, z2, z3) → U7(f40_in(z0, z1), z0, z1, z2, z3)
U7(f40_out1, z0, z1, z2, z3) → U8(f40_in(z2, z3), z0, z1, z2, z3)
U8(f40_out1, z0, z1, z2, z3) → f35_out1
f55_in(z0, z1, z2, z3) → U9(f40_in(z0, z1), z0, z1, z2, z3)
U9(f40_out1, z0, z1, z2, z3) → U10(f40_in(z2, z3), z0, z1, z2, z3)
U10(f40_out1, z0, z1, z2, z3) → f55_out1
f73_in(z0, z1, z2) → U11(f40_in(z0, z1), z0, z1, z2)
U11(f40_out1, z0, z1, z2) → U12(f22_in(z2), z0, z1, z2)
U12(f22_out1, z0, z1, z2) → f73_out1
Tuples:

F40_IN(tree(z0, z1, z2), z3) → c4(U2'(f55_in(z0, z1, z2, z3), tree(z0, z1, z2), z3), F55_IN(z0, z1, z2, z3))
F22_IN(tree(z0, z1, z2)) → c7(U3'(f73_in(z0, z1, z2), tree(z0, z1, z2)), F73_IN(z0, z1, z2))
F55_IN(z0, z1, z2, z3) → c18(U9'(f40_in(z0, z1), z0, z1, z2, z3), F40_IN(z0, z1))
U9'(f40_out1, z0, z1, z2, z3) → c19(U10'(f40_in(z2, z3), z0, z1, z2, z3), F40_IN(z2, z3))
F73_IN(z0, z1, z2) → c21(U11'(f40_in(z0, z1), z0, z1, z2), F40_IN(z0, z1))
U11'(f40_out1, z0, z1, z2) → c22(U12'(f22_in(z2), z0, z1, z2), F22_IN(z2))
F2_IN(tree(z0, z1, z2)) → c(U1'(f17_in(z0, z1, z2), tree(z0, z1, z2)))
F2_IN(tree(z0, z1, z2)) → c(F17_IN(z0, z1, z2))
F21_IN(tree(z0, z1, z2), z3) → c(U4'(f35_in(z0, z1, z2, z3), tree(z0, z1, z2), z3))
F21_IN(tree(z0, z1, z2), z3) → c(F35_IN(z0, z1, z2, z3))
F17_IN(z0, z1, z2) → c(U5'(f21_in(z0, z1), z0, z1, z2))
F17_IN(z0, z1, z2) → c(F21_IN(z0, z1))
U5'(f21_out1, z0, z1, z2) → c(U6'(f22_in(z2), z0, z1, z2))
U5'(f21_out1, z0, z1, z2) → c(F22_IN(z2))
F35_IN(z0, z1, z2, z3) → c(U7'(f40_in(z0, z1), z0, z1, z2, z3))
F35_IN(z0, z1, z2, z3) → c(F40_IN(z0, z1))
U7'(f40_out1, z0, z1, z2, z3) → c(U8'(f40_in(z2, z3), z0, z1, z2, z3))
U7'(f40_out1, z0, z1, z2, z3) → c(F40_IN(z2, z3))
S tuples:

F40_IN(tree(z0, z1, z2), z3) → c4(U2'(f55_in(z0, z1, z2, z3), tree(z0, z1, z2), z3), F55_IN(z0, z1, z2, z3))
F22_IN(tree(z0, z1, z2)) → c7(U3'(f73_in(z0, z1, z2), tree(z0, z1, z2)), F73_IN(z0, z1, z2))
F55_IN(z0, z1, z2, z3) → c18(U9'(f40_in(z0, z1), z0, z1, z2, z3), F40_IN(z0, z1))
U9'(f40_out1, z0, z1, z2, z3) → c19(U10'(f40_in(z2, z3), z0, z1, z2, z3), F40_IN(z2, z3))
F73_IN(z0, z1, z2) → c21(U11'(f40_in(z0, z1), z0, z1, z2), F40_IN(z0, z1))
U11'(f40_out1, z0, z1, z2) → c22(U12'(f22_in(z2), z0, z1, z2), F22_IN(z2))
F2_IN(tree(z0, z1, z2)) → c(U1'(f17_in(z0, z1, z2), tree(z0, z1, z2)))
F2_IN(tree(z0, z1, z2)) → c(F17_IN(z0, z1, z2))
F21_IN(tree(z0, z1, z2), z3) → c(U4'(f35_in(z0, z1, z2, z3), tree(z0, z1, z2), z3))
F21_IN(tree(z0, z1, z2), z3) → c(F35_IN(z0, z1, z2, z3))
F17_IN(z0, z1, z2) → c(U5'(f21_in(z0, z1), z0, z1, z2))
F17_IN(z0, z1, z2) → c(F21_IN(z0, z1))
U5'(f21_out1, z0, z1, z2) → c(U6'(f22_in(z2), z0, z1, z2))
U5'(f21_out1, z0, z1, z2) → c(F22_IN(z2))
F35_IN(z0, z1, z2, z3) → c(U7'(f40_in(z0, z1), z0, z1, z2, z3))
F35_IN(z0, z1, z2, z3) → c(F40_IN(z0, z1))
U7'(f40_out1, z0, z1, z2, z3) → c(U8'(f40_in(z2, z3), z0, z1, z2, z3))
U7'(f40_out1, z0, z1, z2, z3) → c(F40_IN(z2, z3))
K tuples:none
Defined Rule Symbols:

f2_in, U1, f40_in, U2, f22_in, U3, f21_in, U4, f17_in, U5, U6, f35_in, U7, U8, f55_in, U9, U10, f73_in, U11, U12

Defined Pair Symbols:

F40_IN, F22_IN, F55_IN, U9', F73_IN, U11', F2_IN, F21_IN, F17_IN, U5', F35_IN, U7'

Compound Symbols:

c4, c7, c18, c19, c21, c22, c

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

Removed 8 trailing tuple parts

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(nil) → f2_out1
f2_in(tree(z0, z1, z2)) → U1(f17_in(z0, z1, z2), tree(z0, z1, z2))
U1(f17_out1, tree(z0, z1, z2)) → f2_out1
f40_in(nil, z0) → f40_out1
f40_in(tree(z0, z1, z2), z3) → U2(f55_in(z0, z1, z2, z3), tree(z0, z1, z2), z3)
U2(f55_out1, tree(z0, z1, z2), z3) → f40_out1
f22_in(nil) → f22_out1
f22_in(tree(z0, z1, z2)) → U3(f73_in(z0, z1, z2), tree(z0, z1, z2))
U3(f73_out1, tree(z0, z1, z2)) → f22_out1
f21_in(nil, z0) → f21_out1
f21_in(tree(z0, z1, z2), z3) → U4(f35_in(z0, z1, z2, z3), tree(z0, z1, z2), z3)
U4(f35_out1, tree(z0, z1, z2), z3) → f21_out1
f17_in(z0, z1, z2) → U5(f21_in(z0, z1), z0, z1, z2)
U5(f21_out1, z0, z1, z2) → U6(f22_in(z2), z0, z1, z2)
U6(f22_out1, z0, z1, z2) → f17_out1
f35_in(z0, z1, z2, z3) → U7(f40_in(z0, z1), z0, z1, z2, z3)
U7(f40_out1, z0, z1, z2, z3) → U8(f40_in(z2, z3), z0, z1, z2, z3)
U8(f40_out1, z0, z1, z2, z3) → f35_out1
f55_in(z0, z1, z2, z3) → U9(f40_in(z0, z1), z0, z1, z2, z3)
U9(f40_out1, z0, z1, z2, z3) → U10(f40_in(z2, z3), z0, z1, z2, z3)
U10(f40_out1, z0, z1, z2, z3) → f55_out1
f73_in(z0, z1, z2) → U11(f40_in(z0, z1), z0, z1, z2)
U11(f40_out1, z0, z1, z2) → U12(f22_in(z2), z0, z1, z2)
U12(f22_out1, z0, z1, z2) → f73_out1
Tuples:

F55_IN(z0, z1, z2, z3) → c18(U9'(f40_in(z0, z1), z0, z1, z2, z3), F40_IN(z0, z1))
F73_IN(z0, z1, z2) → c21(U11'(f40_in(z0, z1), z0, z1, z2), F40_IN(z0, z1))
F2_IN(tree(z0, z1, z2)) → c(F17_IN(z0, z1, z2))
F21_IN(tree(z0, z1, z2), z3) → c(F35_IN(z0, z1, z2, z3))
F17_IN(z0, z1, z2) → c(U5'(f21_in(z0, z1), z0, z1, z2))
F17_IN(z0, z1, z2) → c(F21_IN(z0, z1))
U5'(f21_out1, z0, z1, z2) → c(F22_IN(z2))
F35_IN(z0, z1, z2, z3) → c(U7'(f40_in(z0, z1), z0, z1, z2, z3))
F35_IN(z0, z1, z2, z3) → c(F40_IN(z0, z1))
U7'(f40_out1, z0, z1, z2, z3) → c(F40_IN(z2, z3))
F40_IN(tree(z0, z1, z2), z3) → c4(F55_IN(z0, z1, z2, z3))
F22_IN(tree(z0, z1, z2)) → c7(F73_IN(z0, z1, z2))
U9'(f40_out1, z0, z1, z2, z3) → c19(F40_IN(z2, z3))
U11'(f40_out1, z0, z1, z2) → c22(F22_IN(z2))
F2_IN(tree(z0, z1, z2)) → c
F21_IN(tree(z0, z1, z2), z3) → c
U5'(f21_out1, z0, z1, z2) → c
U7'(f40_out1, z0, z1, z2, z3) → c
S tuples:

F55_IN(z0, z1, z2, z3) → c18(U9'(f40_in(z0, z1), z0, z1, z2, z3), F40_IN(z0, z1))
F73_IN(z0, z1, z2) → c21(U11'(f40_in(z0, z1), z0, z1, z2), F40_IN(z0, z1))
F2_IN(tree(z0, z1, z2)) → c(F17_IN(z0, z1, z2))
F21_IN(tree(z0, z1, z2), z3) → c(F35_IN(z0, z1, z2, z3))
F17_IN(z0, z1, z2) → c(U5'(f21_in(z0, z1), z0, z1, z2))
F17_IN(z0, z1, z2) → c(F21_IN(z0, z1))
U5'(f21_out1, z0, z1, z2) → c(F22_IN(z2))
F35_IN(z0, z1, z2, z3) → c(U7'(f40_in(z0, z1), z0, z1, z2, z3))
F35_IN(z0, z1, z2, z3) → c(F40_IN(z0, z1))
U7'(f40_out1, z0, z1, z2, z3) → c(F40_IN(z2, z3))
F40_IN(tree(z0, z1, z2), z3) → c4(F55_IN(z0, z1, z2, z3))
F22_IN(tree(z0, z1, z2)) → c7(F73_IN(z0, z1, z2))
U9'(f40_out1, z0, z1, z2, z3) → c19(F40_IN(z2, z3))
U11'(f40_out1, z0, z1, z2) → c22(F22_IN(z2))
F2_IN(tree(z0, z1, z2)) → c
F21_IN(tree(z0, z1, z2), z3) → c
U5'(f21_out1, z0, z1, z2) → c
U7'(f40_out1, z0, z1, z2, z3) → c
K tuples:none
Defined Rule Symbols:

f2_in, U1, f40_in, U2, f22_in, U3, f21_in, U4, f17_in, U5, U6, f35_in, U7, U8, f55_in, U9, U10, f73_in, U11, U12

Defined Pair Symbols:

F55_IN, F73_IN, F2_IN, F21_IN, F17_IN, U5', F35_IN, U7', F40_IN, F22_IN, U9', U11'

Compound Symbols:

c18, c21, c, c4, c7, c19, c22, c

(23) CdtKnowledgeProof (EQUIVALENT transformation)

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

F2_IN(tree(z0, z1, z2)) → c(F17_IN(z0, z1, z2))
F17_IN(z0, z1, z2) → c(U5'(f21_in(z0, z1), z0, z1, z2))
F17_IN(z0, z1, z2) → c(F21_IN(z0, z1))
U5'(f21_out1, z0, z1, z2) → c(F22_IN(z2))
F2_IN(tree(z0, z1, z2)) → c
F21_IN(tree(z0, z1, z2), z3) → c
U5'(f21_out1, z0, z1, z2) → c
F17_IN(z0, z1, z2) → c(U5'(f21_in(z0, z1), z0, z1, z2))
F17_IN(z0, z1, z2) → c(F21_IN(z0, z1))
U5'(f21_out1, z0, z1, z2) → c(F22_IN(z2))
U5'(f21_out1, z0, z1, z2) → c
F21_IN(tree(z0, z1, z2), z3) → c(F35_IN(z0, z1, z2, z3))
F21_IN(tree(z0, z1, z2), z3) → c
F35_IN(z0, z1, z2, z3) → c(U7'(f40_in(z0, z1), z0, z1, z2, z3))
F35_IN(z0, z1, z2, z3) → c(F40_IN(z0, z1))
U7'(f40_out1, z0, z1, z2, z3) → c(F40_IN(z2, z3))
U7'(f40_out1, z0, z1, z2, z3) → c

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(nil) → f2_out1
f2_in(tree(z0, z1, z2)) → U1(f17_in(z0, z1, z2), tree(z0, z1, z2))
U1(f17_out1, tree(z0, z1, z2)) → f2_out1
f40_in(nil, z0) → f40_out1
f40_in(tree(z0, z1, z2), z3) → U2(f55_in(z0, z1, z2, z3), tree(z0, z1, z2), z3)
U2(f55_out1, tree(z0, z1, z2), z3) → f40_out1
f22_in(nil) → f22_out1
f22_in(tree(z0, z1, z2)) → U3(f73_in(z0, z1, z2), tree(z0, z1, z2))
U3(f73_out1, tree(z0, z1, z2)) → f22_out1
f21_in(nil, z0) → f21_out1
f21_in(tree(z0, z1, z2), z3) → U4(f35_in(z0, z1, z2, z3), tree(z0, z1, z2), z3)
U4(f35_out1, tree(z0, z1, z2), z3) → f21_out1
f17_in(z0, z1, z2) → U5(f21_in(z0, z1), z0, z1, z2)
U5(f21_out1, z0, z1, z2) → U6(f22_in(z2), z0, z1, z2)
U6(f22_out1, z0, z1, z2) → f17_out1
f35_in(z0, z1, z2, z3) → U7(f40_in(z0, z1), z0, z1, z2, z3)
U7(f40_out1, z0, z1, z2, z3) → U8(f40_in(z2, z3), z0, z1, z2, z3)
U8(f40_out1, z0, z1, z2, z3) → f35_out1
f55_in(z0, z1, z2, z3) → U9(f40_in(z0, z1), z0, z1, z2, z3)
U9(f40_out1, z0, z1, z2, z3) → U10(f40_in(z2, z3), z0, z1, z2, z3)
U10(f40_out1, z0, z1, z2, z3) → f55_out1
f73_in(z0, z1, z2) → U11(f40_in(z0, z1), z0, z1, z2)
U11(f40_out1, z0, z1, z2) → U12(f22_in(z2), z0, z1, z2)
U12(f22_out1, z0, z1, z2) → f73_out1
Tuples:

F55_IN(z0, z1, z2, z3) → c18(U9'(f40_in(z0, z1), z0, z1, z2, z3), F40_IN(z0, z1))
F73_IN(z0, z1, z2) → c21(U11'(f40_in(z0, z1), z0, z1, z2), F40_IN(z0, z1))
F2_IN(tree(z0, z1, z2)) → c(F17_IN(z0, z1, z2))
F21_IN(tree(z0, z1, z2), z3) → c(F35_IN(z0, z1, z2, z3))
F17_IN(z0, z1, z2) → c(U5'(f21_in(z0, z1), z0, z1, z2))
F17_IN(z0, z1, z2) → c(F21_IN(z0, z1))
U5'(f21_out1, z0, z1, z2) → c(F22_IN(z2))
F35_IN(z0, z1, z2, z3) → c(U7'(f40_in(z0, z1), z0, z1, z2, z3))
F35_IN(z0, z1, z2, z3) → c(F40_IN(z0, z1))
U7'(f40_out1, z0, z1, z2, z3) → c(F40_IN(z2, z3))
F40_IN(tree(z0, z1, z2), z3) → c4(F55_IN(z0, z1, z2, z3))
F22_IN(tree(z0, z1, z2)) → c7(F73_IN(z0, z1, z2))
U9'(f40_out1, z0, z1, z2, z3) → c19(F40_IN(z2, z3))
U11'(f40_out1, z0, z1, z2) → c22(F22_IN(z2))
F2_IN(tree(z0, z1, z2)) → c
F21_IN(tree(z0, z1, z2), z3) → c
U5'(f21_out1, z0, z1, z2) → c
U7'(f40_out1, z0, z1, z2, z3) → c
S tuples:

F55_IN(z0, z1, z2, z3) → c18(U9'(f40_in(z0, z1), z0, z1, z2, z3), F40_IN(z0, z1))
F73_IN(z0, z1, z2) → c21(U11'(f40_in(z0, z1), z0, z1, z2), F40_IN(z0, z1))
F40_IN(tree(z0, z1, z2), z3) → c4(F55_IN(z0, z1, z2, z3))
F22_IN(tree(z0, z1, z2)) → c7(F73_IN(z0, z1, z2))
U9'(f40_out1, z0, z1, z2, z3) → c19(F40_IN(z2, z3))
U11'(f40_out1, z0, z1, z2) → c22(F22_IN(z2))
K tuples:

F2_IN(tree(z0, z1, z2)) → c(F17_IN(z0, z1, z2))
F17_IN(z0, z1, z2) → c(U5'(f21_in(z0, z1), z0, z1, z2))
F17_IN(z0, z1, z2) → c(F21_IN(z0, z1))
U5'(f21_out1, z0, z1, z2) → c(F22_IN(z2))
F2_IN(tree(z0, z1, z2)) → c
F21_IN(tree(z0, z1, z2), z3) → c
U5'(f21_out1, z0, z1, z2) → c
F21_IN(tree(z0, z1, z2), z3) → c(F35_IN(z0, z1, z2, z3))
F35_IN(z0, z1, z2, z3) → c(U7'(f40_in(z0, z1), z0, z1, z2, z3))
F35_IN(z0, z1, z2, z3) → c(F40_IN(z0, z1))
U7'(f40_out1, z0, z1, z2, z3) → c(F40_IN(z2, z3))
U7'(f40_out1, z0, z1, z2, z3) → c
Defined Rule Symbols:

f2_in, U1, f40_in, U2, f22_in, U3, f21_in, U4, f17_in, U5, U6, f35_in, U7, U8, f55_in, U9, U10, f73_in, U11, U12

Defined Pair Symbols:

F55_IN, F73_IN, F2_IN, F21_IN, F17_IN, U5', F35_IN, U7', F40_IN, F22_IN, U9', U11'

Compound Symbols:

c18, c21, c, c4, c7, c19, c22, c

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

F22_IN(tree(z0, z1, z2)) → c7(F73_IN(z0, z1, z2))
We considered the (Usable) Rules:

f40_in(nil, z0) → f40_out1
f40_in(tree(z0, z1, z2), z3) → U2(f55_in(z0, z1, z2, z3), tree(z0, z1, z2), z3)
f55_in(z0, z1, z2, z3) → U9(f40_in(z0, z1), z0, z1, z2, z3)
U2(f55_out1, tree(z0, z1, z2), z3) → f40_out1
U9(f40_out1, z0, z1, z2, z3) → U10(f40_in(z2, z3), z0, z1, z2, z3)
U10(f40_out1, z0, z1, z2, z3) → f55_out1
f21_in(nil, z0) → f21_out1
f21_in(tree(z0, z1, z2), z3) → U4(f35_in(z0, z1, z2, z3), tree(z0, z1, z2), z3)
f35_in(z0, z1, z2, z3) → U7(f40_in(z0, z1), z0, z1, z2, z3)
U4(f35_out1, tree(z0, z1, z2), z3) → f21_out1
U7(f40_out1, z0, z1, z2, z3) → U8(f40_in(z2, z3), z0, z1, z2, z3)
U8(f40_out1, z0, z1, z2, z3) → f35_out1
And the Tuples:

F55_IN(z0, z1, z2, z3) → c18(U9'(f40_in(z0, z1), z0, z1, z2, z3), F40_IN(z0, z1))
F73_IN(z0, z1, z2) → c21(U11'(f40_in(z0, z1), z0, z1, z2), F40_IN(z0, z1))
F2_IN(tree(z0, z1, z2)) → c(F17_IN(z0, z1, z2))
F21_IN(tree(z0, z1, z2), z3) → c(F35_IN(z0, z1, z2, z3))
F17_IN(z0, z1, z2) → c(U5'(f21_in(z0, z1), z0, z1, z2))
F17_IN(z0, z1, z2) → c(F21_IN(z0, z1))
U5'(f21_out1, z0, z1, z2) → c(F22_IN(z2))
F35_IN(z0, z1, z2, z3) → c(U7'(f40_in(z0, z1), z0, z1, z2, z3))
F35_IN(z0, z1, z2, z3) → c(F40_IN(z0, z1))
U7'(f40_out1, z0, z1, z2, z3) → c(F40_IN(z2, z3))
F40_IN(tree(z0, z1, z2), z3) → c4(F55_IN(z0, z1, z2, z3))
F22_IN(tree(z0, z1, z2)) → c7(F73_IN(z0, z1, z2))
U9'(f40_out1, z0, z1, z2, z3) → c19(F40_IN(z2, z3))
U11'(f40_out1, z0, z1, z2) → c22(F22_IN(z2))
F2_IN(tree(z0, z1, z2)) → c
F21_IN(tree(z0, z1, z2), z3) → c
U5'(f21_out1, z0, z1, z2) → c
U7'(f40_out1, z0, z1, z2, z3) → c
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(F17_IN(x1, x2, x3)) = [3] + [2]x1 + [3]x2 + [2]x3   
POL(F21_IN(x1, x2)) = [1] + [2]x1 + [3]x2   
POL(F22_IN(x1)) = x1   
POL(F2_IN(x1)) = [2] + [3]x1   
POL(F35_IN(x1, x2, x3, x4)) = [2] + [3]x4   
POL(F40_IN(x1, x2)) = 0   
POL(F55_IN(x1, x2, x3, x4)) = 0   
POL(F73_IN(x1, x2, x3)) = x1 + x2 + x3   
POL(U10(x1, x2, x3, x4, x5)) = x1   
POL(U11'(x1, x2, x3, x4)) = x4   
POL(U2(x1, x2, x3)) = 0   
POL(U4(x1, x2, x3)) = 0   
POL(U5'(x1, x2, x3, x4)) = x2 + [3]x3 + x4   
POL(U7(x1, x2, x3, x4, x5)) = [2] + x4   
POL(U7'(x1, x2, x3, x4, x5)) = x5   
POL(U8(x1, x2, x3, x4, x5)) = [1]   
POL(U9(x1, x2, x3, x4, x5)) = [3]x4 + [2]x5   
POL(U9'(x1, x2, x3, x4, x5)) = 0   
POL(c) = 0   
POL(c(x1)) = x1   
POL(c18(x1, x2)) = x1 + x2   
POL(c19(x1)) = x1   
POL(c21(x1, x2)) = x1 + x2   
POL(c22(x1)) = x1   
POL(c4(x1)) = x1   
POL(c7(x1)) = x1   
POL(f21_in(x1, x2)) = 0   
POL(f21_out1) = 0   
POL(f35_in(x1, x2, x3, x4)) = [2] + [2]x1 + [2]x2 + [2]x3   
POL(f35_out1) = 0   
POL(f40_in(x1, x2)) = [2]x2   
POL(f40_out1) = 0   
POL(f55_in(x1, x2, x3, x4)) = [3]x3 + [2]x4   
POL(f55_out1) = 0   
POL(nil) = 0   
POL(tree(x1, x2, x3)) = [2] + x1 + x2 + x3   

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(nil) → f2_out1
f2_in(tree(z0, z1, z2)) → U1(f17_in(z0, z1, z2), tree(z0, z1, z2))
U1(f17_out1, tree(z0, z1, z2)) → f2_out1
f40_in(nil, z0) → f40_out1
f40_in(tree(z0, z1, z2), z3) → U2(f55_in(z0, z1, z2, z3), tree(z0, z1, z2), z3)
U2(f55_out1, tree(z0, z1, z2), z3) → f40_out1
f22_in(nil) → f22_out1
f22_in(tree(z0, z1, z2)) → U3(f73_in(z0, z1, z2), tree(z0, z1, z2))
U3(f73_out1, tree(z0, z1, z2)) → f22_out1
f21_in(nil, z0) → f21_out1
f21_in(tree(z0, z1, z2), z3) → U4(f35_in(z0, z1, z2, z3), tree(z0, z1, z2), z3)
U4(f35_out1, tree(z0, z1, z2), z3) → f21_out1
f17_in(z0, z1, z2) → U5(f21_in(z0, z1), z0, z1, z2)
U5(f21_out1, z0, z1, z2) → U6(f22_in(z2), z0, z1, z2)
U6(f22_out1, z0, z1, z2) → f17_out1
f35_in(z0, z1, z2, z3) → U7(f40_in(z0, z1), z0, z1, z2, z3)
U7(f40_out1, z0, z1, z2, z3) → U8(f40_in(z2, z3), z0, z1, z2, z3)
U8(f40_out1, z0, z1, z2, z3) → f35_out1
f55_in(z0, z1, z2, z3) → U9(f40_in(z0, z1), z0, z1, z2, z3)
U9(f40_out1, z0, z1, z2, z3) → U10(f40_in(z2, z3), z0, z1, z2, z3)
U10(f40_out1, z0, z1, z2, z3) → f55_out1
f73_in(z0, z1, z2) → U11(f40_in(z0, z1), z0, z1, z2)
U11(f40_out1, z0, z1, z2) → U12(f22_in(z2), z0, z1, z2)
U12(f22_out1, z0, z1, z2) → f73_out1
Tuples:

F55_IN(z0, z1, z2, z3) → c18(U9'(f40_in(z0, z1), z0, z1, z2, z3), F40_IN(z0, z1))
F73_IN(z0, z1, z2) → c21(U11'(f40_in(z0, z1), z0, z1, z2), F40_IN(z0, z1))
F2_IN(tree(z0, z1, z2)) → c(F17_IN(z0, z1, z2))
F21_IN(tree(z0, z1, z2), z3) → c(F35_IN(z0, z1, z2, z3))
F17_IN(z0, z1, z2) → c(U5'(f21_in(z0, z1), z0, z1, z2))
F17_IN(z0, z1, z2) → c(F21_IN(z0, z1))
U5'(f21_out1, z0, z1, z2) → c(F22_IN(z2))
F35_IN(z0, z1, z2, z3) → c(U7'(f40_in(z0, z1), z0, z1, z2, z3))
F35_IN(z0, z1, z2, z3) → c(F40_IN(z0, z1))
U7'(f40_out1, z0, z1, z2, z3) → c(F40_IN(z2, z3))
F40_IN(tree(z0, z1, z2), z3) → c4(F55_IN(z0, z1, z2, z3))
F22_IN(tree(z0, z1, z2)) → c7(F73_IN(z0, z1, z2))
U9'(f40_out1, z0, z1, z2, z3) → c19(F40_IN(z2, z3))
U11'(f40_out1, z0, z1, z2) → c22(F22_IN(z2))
F2_IN(tree(z0, z1, z2)) → c
F21_IN(tree(z0, z1, z2), z3) → c
U5'(f21_out1, z0, z1, z2) → c
U7'(f40_out1, z0, z1, z2, z3) → c
S tuples:

F55_IN(z0, z1, z2, z3) → c18(U9'(f40_in(z0, z1), z0, z1, z2, z3), F40_IN(z0, z1))
F73_IN(z0, z1, z2) → c21(U11'(f40_in(z0, z1), z0, z1, z2), F40_IN(z0, z1))
F40_IN(tree(z0, z1, z2), z3) → c4(F55_IN(z0, z1, z2, z3))
U9'(f40_out1, z0, z1, z2, z3) → c19(F40_IN(z2, z3))
U11'(f40_out1, z0, z1, z2) → c22(F22_IN(z2))
K tuples:

F2_IN(tree(z0, z1, z2)) → c(F17_IN(z0, z1, z2))
F17_IN(z0, z1, z2) → c(U5'(f21_in(z0, z1), z0, z1, z2))
F17_IN(z0, z1, z2) → c(F21_IN(z0, z1))
U5'(f21_out1, z0, z1, z2) → c(F22_IN(z2))
F2_IN(tree(z0, z1, z2)) → c
F21_IN(tree(z0, z1, z2), z3) → c
U5'(f21_out1, z0, z1, z2) → c
F21_IN(tree(z0, z1, z2), z3) → c(F35_IN(z0, z1, z2, z3))
F35_IN(z0, z1, z2, z3) → c(U7'(f40_in(z0, z1), z0, z1, z2, z3))
F35_IN(z0, z1, z2, z3) → c(F40_IN(z0, z1))
U7'(f40_out1, z0, z1, z2, z3) → c(F40_IN(z2, z3))
U7'(f40_out1, z0, z1, z2, z3) → c
F22_IN(tree(z0, z1, z2)) → c7(F73_IN(z0, z1, z2))
Defined Rule Symbols:

f2_in, U1, f40_in, U2, f22_in, U3, f21_in, U4, f17_in, U5, U6, f35_in, U7, U8, f55_in, U9, U10, f73_in, U11, U12

Defined Pair Symbols:

F55_IN, F73_IN, F2_IN, F21_IN, F17_IN, U5', F35_IN, U7', F40_IN, F22_IN, U9', U11'

Compound Symbols:

c18, c21, c, c4, c7, c19, c22, c

(27) CdtKnowledgeProof (EQUIVALENT transformation)

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

F73_IN(z0, z1, z2) → c21(U11'(f40_in(z0, z1), z0, z1, z2), F40_IN(z0, z1))
U11'(f40_out1, z0, z1, z2) → c22(F22_IN(z2))
U11'(f40_out1, z0, z1, z2) → c22(F22_IN(z2))
F22_IN(tree(z0, z1, z2)) → c7(F73_IN(z0, z1, z2))

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(nil) → f2_out1
f2_in(tree(z0, z1, z2)) → U1(f17_in(z0, z1, z2), tree(z0, z1, z2))
U1(f17_out1, tree(z0, z1, z2)) → f2_out1
f40_in(nil, z0) → f40_out1
f40_in(tree(z0, z1, z2), z3) → U2(f55_in(z0, z1, z2, z3), tree(z0, z1, z2), z3)
U2(f55_out1, tree(z0, z1, z2), z3) → f40_out1
f22_in(nil) → f22_out1
f22_in(tree(z0, z1, z2)) → U3(f73_in(z0, z1, z2), tree(z0, z1, z2))
U3(f73_out1, tree(z0, z1, z2)) → f22_out1
f21_in(nil, z0) → f21_out1
f21_in(tree(z0, z1, z2), z3) → U4(f35_in(z0, z1, z2, z3), tree(z0, z1, z2), z3)
U4(f35_out1, tree(z0, z1, z2), z3) → f21_out1
f17_in(z0, z1, z2) → U5(f21_in(z0, z1), z0, z1, z2)
U5(f21_out1, z0, z1, z2) → U6(f22_in(z2), z0, z1, z2)
U6(f22_out1, z0, z1, z2) → f17_out1
f35_in(z0, z1, z2, z3) → U7(f40_in(z0, z1), z0, z1, z2, z3)
U7(f40_out1, z0, z1, z2, z3) → U8(f40_in(z2, z3), z0, z1, z2, z3)
U8(f40_out1, z0, z1, z2, z3) → f35_out1
f55_in(z0, z1, z2, z3) → U9(f40_in(z0, z1), z0, z1, z2, z3)
U9(f40_out1, z0, z1, z2, z3) → U10(f40_in(z2, z3), z0, z1, z2, z3)
U10(f40_out1, z0, z1, z2, z3) → f55_out1
f73_in(z0, z1, z2) → U11(f40_in(z0, z1), z0, z1, z2)
U11(f40_out1, z0, z1, z2) → U12(f22_in(z2), z0, z1, z2)
U12(f22_out1, z0, z1, z2) → f73_out1
Tuples:

F55_IN(z0, z1, z2, z3) → c18(U9'(f40_in(z0, z1), z0, z1, z2, z3), F40_IN(z0, z1))
F73_IN(z0, z1, z2) → c21(U11'(f40_in(z0, z1), z0, z1, z2), F40_IN(z0, z1))
F2_IN(tree(z0, z1, z2)) → c(F17_IN(z0, z1, z2))
F21_IN(tree(z0, z1, z2), z3) → c(F35_IN(z0, z1, z2, z3))
F17_IN(z0, z1, z2) → c(U5'(f21_in(z0, z1), z0, z1, z2))
F17_IN(z0, z1, z2) → c(F21_IN(z0, z1))
U5'(f21_out1, z0, z1, z2) → c(F22_IN(z2))
F35_IN(z0, z1, z2, z3) → c(U7'(f40_in(z0, z1), z0, z1, z2, z3))
F35_IN(z0, z1, z2, z3) → c(F40_IN(z0, z1))
U7'(f40_out1, z0, z1, z2, z3) → c(F40_IN(z2, z3))
F40_IN(tree(z0, z1, z2), z3) → c4(F55_IN(z0, z1, z2, z3))
F22_IN(tree(z0, z1, z2)) → c7(F73_IN(z0, z1, z2))
U9'(f40_out1, z0, z1, z2, z3) → c19(F40_IN(z2, z3))
U11'(f40_out1, z0, z1, z2) → c22(F22_IN(z2))
F2_IN(tree(z0, z1, z2)) → c
F21_IN(tree(z0, z1, z2), z3) → c
U5'(f21_out1, z0, z1, z2) → c
U7'(f40_out1, z0, z1, z2, z3) → c
S tuples:

F55_IN(z0, z1, z2, z3) → c18(U9'(f40_in(z0, z1), z0, z1, z2, z3), F40_IN(z0, z1))
F40_IN(tree(z0, z1, z2), z3) → c4(F55_IN(z0, z1, z2, z3))
U9'(f40_out1, z0, z1, z2, z3) → c19(F40_IN(z2, z3))
K tuples:

F2_IN(tree(z0, z1, z2)) → c(F17_IN(z0, z1, z2))
F17_IN(z0, z1, z2) → c(U5'(f21_in(z0, z1), z0, z1, z2))
F17_IN(z0, z1, z2) → c(F21_IN(z0, z1))
U5'(f21_out1, z0, z1, z2) → c(F22_IN(z2))
F2_IN(tree(z0, z1, z2)) → c
F21_IN(tree(z0, z1, z2), z3) → c
U5'(f21_out1, z0, z1, z2) → c
F21_IN(tree(z0, z1, z2), z3) → c(F35_IN(z0, z1, z2, z3))
F35_IN(z0, z1, z2, z3) → c(U7'(f40_in(z0, z1), z0, z1, z2, z3))
F35_IN(z0, z1, z2, z3) → c(F40_IN(z0, z1))
U7'(f40_out1, z0, z1, z2, z3) → c(F40_IN(z2, z3))
U7'(f40_out1, z0, z1, z2, z3) → c
F22_IN(tree(z0, z1, z2)) → c7(F73_IN(z0, z1, z2))
F73_IN(z0, z1, z2) → c21(U11'(f40_in(z0, z1), z0, z1, z2), F40_IN(z0, z1))
U11'(f40_out1, z0, z1, z2) → c22(F22_IN(z2))
Defined Rule Symbols:

f2_in, U1, f40_in, U2, f22_in, U3, f21_in, U4, f17_in, U5, U6, f35_in, U7, U8, f55_in, U9, U10, f73_in, U11, U12

Defined Pair Symbols:

F55_IN, F73_IN, F2_IN, F21_IN, F17_IN, U5', F35_IN, U7', F40_IN, F22_IN, U9', U11'

Compound Symbols:

c18, c21, c, c4, c7, c19, c22, c

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

U9'(f40_out1, z0, z1, z2, z3) → c19(F40_IN(z2, z3))
We considered the (Usable) Rules:

f40_in(nil, z0) → f40_out1
f40_in(tree(z0, z1, z2), z3) → U2(f55_in(z0, z1, z2, z3), tree(z0, z1, z2), z3)
f55_in(z0, z1, z2, z3) → U9(f40_in(z0, z1), z0, z1, z2, z3)
U2(f55_out1, tree(z0, z1, z2), z3) → f40_out1
U9(f40_out1, z0, z1, z2, z3) → U10(f40_in(z2, z3), z0, z1, z2, z3)
U10(f40_out1, z0, z1, z2, z3) → f55_out1
f21_in(nil, z0) → f21_out1
f21_in(tree(z0, z1, z2), z3) → U4(f35_in(z0, z1, z2, z3), tree(z0, z1, z2), z3)
f35_in(z0, z1, z2, z3) → U7(f40_in(z0, z1), z0, z1, z2, z3)
U4(f35_out1, tree(z0, z1, z2), z3) → f21_out1
U7(f40_out1, z0, z1, z2, z3) → U8(f40_in(z2, z3), z0, z1, z2, z3)
U8(f40_out1, z0, z1, z2, z3) → f35_out1
And the Tuples:

F55_IN(z0, z1, z2, z3) → c18(U9'(f40_in(z0, z1), z0, z1, z2, z3), F40_IN(z0, z1))
F73_IN(z0, z1, z2) → c21(U11'(f40_in(z0, z1), z0, z1, z2), F40_IN(z0, z1))
F2_IN(tree(z0, z1, z2)) → c(F17_IN(z0, z1, z2))
F21_IN(tree(z0, z1, z2), z3) → c(F35_IN(z0, z1, z2, z3))
F17_IN(z0, z1, z2) → c(U5'(f21_in(z0, z1), z0, z1, z2))
F17_IN(z0, z1, z2) → c(F21_IN(z0, z1))
U5'(f21_out1, z0, z1, z2) → c(F22_IN(z2))
F35_IN(z0, z1, z2, z3) → c(U7'(f40_in(z0, z1), z0, z1, z2, z3))
F35_IN(z0, z1, z2, z3) → c(F40_IN(z0, z1))
U7'(f40_out1, z0, z1, z2, z3) → c(F40_IN(z2, z3))
F40_IN(tree(z0, z1, z2), z3) → c4(F55_IN(z0, z1, z2, z3))
F22_IN(tree(z0, z1, z2)) → c7(F73_IN(z0, z1, z2))
U9'(f40_out1, z0, z1, z2, z3) → c19(F40_IN(z2, z3))
U11'(f40_out1, z0, z1, z2) → c22(F22_IN(z2))
F2_IN(tree(z0, z1, z2)) → c
F21_IN(tree(z0, z1, z2), z3) → c
U5'(f21_out1, z0, z1, z2) → c
U7'(f40_out1, z0, z1, z2, z3) → c
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(F17_IN(x1, x2, x3)) = [3] + [3]x1 + [3]x2 + [3]x3   
POL(F21_IN(x1, x2)) = [2] + [3]x1 + [2]x2   
POL(F22_IN(x1)) = x1   
POL(F2_IN(x1)) = [2] + [3]x1   
POL(F35_IN(x1, x2, x3, x4)) = [3] + x1 + [3]x2 + [2]x3 + x4   
POL(F40_IN(x1, x2)) = x1   
POL(F55_IN(x1, x2, x3, x4)) = [1] + x1 + x2 + x3   
POL(F73_IN(x1, x2, x3)) = x1 + x2 + x3   
POL(U10(x1, x2, x3, x4, x5)) = [1] + x3   
POL(U11'(x1, x2, x3, x4)) = x4   
POL(U2(x1, x2, x3)) = 0   
POL(U4(x1, x2, x3)) = [2] + x1 + x2   
POL(U5'(x1, x2, x3, x4)) = [3] + [3]x3 + [2]x4   
POL(U7(x1, x2, x3, x4, x5)) = x4 + x5   
POL(U7'(x1, x2, x3, x4, x5)) = [3] + [3]x3 + x4 + x5   
POL(U8(x1, x2, x3, x4, x5)) = x4   
POL(U9(x1, x2, x3, x4, x5)) = [2] + x3   
POL(U9'(x1, x2, x3, x4, x5)) = [1] + x4   
POL(c) = 0   
POL(c(x1)) = x1   
POL(c18(x1, x2)) = x1 + x2   
POL(c19(x1)) = x1   
POL(c21(x1, x2)) = x1 + x2   
POL(c22(x1)) = x1   
POL(c4(x1)) = x1   
POL(c7(x1)) = x1   
POL(f21_in(x1, x2)) = [2] + [2]x1 + [2]x2   
POL(f21_out1) = [2]   
POL(f35_in(x1, x2, x3, x4)) = x1 + x2 + x3 + [2]x4   
POL(f35_out1) = 0   
POL(f40_in(x1, x2)) = 0   
POL(f40_out1) = 0   
POL(f55_in(x1, x2, x3, x4)) = [2] + [2]x1 + [2]x2 + x4   
POL(f55_out1) = [1]   
POL(nil) = [1]   
POL(tree(x1, x2, x3)) = [1] + x1 + x2 + x3   

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(nil) → f2_out1
f2_in(tree(z0, z1, z2)) → U1(f17_in(z0, z1, z2), tree(z0, z1, z2))
U1(f17_out1, tree(z0, z1, z2)) → f2_out1
f40_in(nil, z0) → f40_out1
f40_in(tree(z0, z1, z2), z3) → U2(f55_in(z0, z1, z2, z3), tree(z0, z1, z2), z3)
U2(f55_out1, tree(z0, z1, z2), z3) → f40_out1
f22_in(nil) → f22_out1
f22_in(tree(z0, z1, z2)) → U3(f73_in(z0, z1, z2), tree(z0, z1, z2))
U3(f73_out1, tree(z0, z1, z2)) → f22_out1
f21_in(nil, z0) → f21_out1
f21_in(tree(z0, z1, z2), z3) → U4(f35_in(z0, z1, z2, z3), tree(z0, z1, z2), z3)
U4(f35_out1, tree(z0, z1, z2), z3) → f21_out1
f17_in(z0, z1, z2) → U5(f21_in(z0, z1), z0, z1, z2)
U5(f21_out1, z0, z1, z2) → U6(f22_in(z2), z0, z1, z2)
U6(f22_out1, z0, z1, z2) → f17_out1
f35_in(z0, z1, z2, z3) → U7(f40_in(z0, z1), z0, z1, z2, z3)
U7(f40_out1, z0, z1, z2, z3) → U8(f40_in(z2, z3), z0, z1, z2, z3)
U8(f40_out1, z0, z1, z2, z3) → f35_out1
f55_in(z0, z1, z2, z3) → U9(f40_in(z0, z1), z0, z1, z2, z3)
U9(f40_out1, z0, z1, z2, z3) → U10(f40_in(z2, z3), z0, z1, z2, z3)
U10(f40_out1, z0, z1, z2, z3) → f55_out1
f73_in(z0, z1, z2) → U11(f40_in(z0, z1), z0, z1, z2)
U11(f40_out1, z0, z1, z2) → U12(f22_in(z2), z0, z1, z2)
U12(f22_out1, z0, z1, z2) → f73_out1
Tuples:

F55_IN(z0, z1, z2, z3) → c18(U9'(f40_in(z0, z1), z0, z1, z2, z3), F40_IN(z0, z1))
F73_IN(z0, z1, z2) → c21(U11'(f40_in(z0, z1), z0, z1, z2), F40_IN(z0, z1))
F2_IN(tree(z0, z1, z2)) → c(F17_IN(z0, z1, z2))
F21_IN(tree(z0, z1, z2), z3) → c(F35_IN(z0, z1, z2, z3))
F17_IN(z0, z1, z2) → c(U5'(f21_in(z0, z1), z0, z1, z2))
F17_IN(z0, z1, z2) → c(F21_IN(z0, z1))
U5'(f21_out1, z0, z1, z2) → c(F22_IN(z2))
F35_IN(z0, z1, z2, z3) → c(U7'(f40_in(z0, z1), z0, z1, z2, z3))
F35_IN(z0, z1, z2, z3) → c(F40_IN(z0, z1))
U7'(f40_out1, z0, z1, z2, z3) → c(F40_IN(z2, z3))
F40_IN(tree(z0, z1, z2), z3) → c4(F55_IN(z0, z1, z2, z3))
F22_IN(tree(z0, z1, z2)) → c7(F73_IN(z0, z1, z2))
U9'(f40_out1, z0, z1, z2, z3) → c19(F40_IN(z2, z3))
U11'(f40_out1, z0, z1, z2) → c22(F22_IN(z2))
F2_IN(tree(z0, z1, z2)) → c
F21_IN(tree(z0, z1, z2), z3) → c
U5'(f21_out1, z0, z1, z2) → c
U7'(f40_out1, z0, z1, z2, z3) → c
S tuples:

F55_IN(z0, z1, z2, z3) → c18(U9'(f40_in(z0, z1), z0, z1, z2, z3), F40_IN(z0, z1))
F40_IN(tree(z0, z1, z2), z3) → c4(F55_IN(z0, z1, z2, z3))
K tuples:

F2_IN(tree(z0, z1, z2)) → c(F17_IN(z0, z1, z2))
F17_IN(z0, z1, z2) → c(U5'(f21_in(z0, z1), z0, z1, z2))
F17_IN(z0, z1, z2) → c(F21_IN(z0, z1))
U5'(f21_out1, z0, z1, z2) → c(F22_IN(z2))
F2_IN(tree(z0, z1, z2)) → c
F21_IN(tree(z0, z1, z2), z3) → c
U5'(f21_out1, z0, z1, z2) → c
F21_IN(tree(z0, z1, z2), z3) → c(F35_IN(z0, z1, z2, z3))
F35_IN(z0, z1, z2, z3) → c(U7'(f40_in(z0, z1), z0, z1, z2, z3))
F35_IN(z0, z1, z2, z3) → c(F40_IN(z0, z1))
U7'(f40_out1, z0, z1, z2, z3) → c(F40_IN(z2, z3))
U7'(f40_out1, z0, z1, z2, z3) → c
F22_IN(tree(z0, z1, z2)) → c7(F73_IN(z0, z1, z2))
F73_IN(z0, z1, z2) → c21(U11'(f40_in(z0, z1), z0, z1, z2), F40_IN(z0, z1))
U11'(f40_out1, z0, z1, z2) → c22(F22_IN(z2))
U9'(f40_out1, z0, z1, z2, z3) → c19(F40_IN(z2, z3))
Defined Rule Symbols:

f2_in, U1, f40_in, U2, f22_in, U3, f21_in, U4, f17_in, U5, U6, f35_in, U7, U8, f55_in, U9, U10, f73_in, U11, U12

Defined Pair Symbols:

F55_IN, F73_IN, F2_IN, F21_IN, F17_IN, U5', F35_IN, U7', F40_IN, F22_IN, U9', U11'

Compound Symbols:

c18, c21, c, c4, c7, c19, c22, c

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

F55_IN(z0, z1, z2, z3) → c18(U9'(f40_in(z0, z1), z0, z1, z2, z3), F40_IN(z0, z1))
F40_IN(tree(z0, z1, z2), z3) → c4(F55_IN(z0, z1, z2, z3))
We considered the (Usable) Rules:

f40_in(nil, z0) → f40_out1
f40_in(tree(z0, z1, z2), z3) → U2(f55_in(z0, z1, z2, z3), tree(z0, z1, z2), z3)
f55_in(z0, z1, z2, z3) → U9(f40_in(z0, z1), z0, z1, z2, z3)
U2(f55_out1, tree(z0, z1, z2), z3) → f40_out1
U9(f40_out1, z0, z1, z2, z3) → U10(f40_in(z2, z3), z0, z1, z2, z3)
U10(f40_out1, z0, z1, z2, z3) → f55_out1
f21_in(nil, z0) → f21_out1
f21_in(tree(z0, z1, z2), z3) → U4(f35_in(z0, z1, z2, z3), tree(z0, z1, z2), z3)
f35_in(z0, z1, z2, z3) → U7(f40_in(z0, z1), z0, z1, z2, z3)
U4(f35_out1, tree(z0, z1, z2), z3) → f21_out1
U7(f40_out1, z0, z1, z2, z3) → U8(f40_in(z2, z3), z0, z1, z2, z3)
U8(f40_out1, z0, z1, z2, z3) → f35_out1
And the Tuples:

F55_IN(z0, z1, z2, z3) → c18(U9'(f40_in(z0, z1), z0, z1, z2, z3), F40_IN(z0, z1))
F73_IN(z0, z1, z2) → c21(U11'(f40_in(z0, z1), z0, z1, z2), F40_IN(z0, z1))
F2_IN(tree(z0, z1, z2)) → c(F17_IN(z0, z1, z2))
F21_IN(tree(z0, z1, z2), z3) → c(F35_IN(z0, z1, z2, z3))
F17_IN(z0, z1, z2) → c(U5'(f21_in(z0, z1), z0, z1, z2))
F17_IN(z0, z1, z2) → c(F21_IN(z0, z1))
U5'(f21_out1, z0, z1, z2) → c(F22_IN(z2))
F35_IN(z0, z1, z2, z3) → c(U7'(f40_in(z0, z1), z0, z1, z2, z3))
F35_IN(z0, z1, z2, z3) → c(F40_IN(z0, z1))
U7'(f40_out1, z0, z1, z2, z3) → c(F40_IN(z2, z3))
F40_IN(tree(z0, z1, z2), z3) → c4(F55_IN(z0, z1, z2, z3))
F22_IN(tree(z0, z1, z2)) → c7(F73_IN(z0, z1, z2))
U9'(f40_out1, z0, z1, z2, z3) → c19(F40_IN(z2, z3))
U11'(f40_out1, z0, z1, z2) → c22(F22_IN(z2))
F2_IN(tree(z0, z1, z2)) → c
F21_IN(tree(z0, z1, z2), z3) → c
U5'(f21_out1, z0, z1, z2) → c
U7'(f40_out1, z0, z1, z2, z3) → c
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(F17_IN(x1, x2, x3)) = [2] + [2]x1 + [2]x2 + [2]x3   
POL(F21_IN(x1, x2)) = [2] + [2]x1   
POL(F22_IN(x1)) = [2]x1   
POL(F2_IN(x1)) = [2]x1   
POL(F35_IN(x1, x2, x3, x4)) = [3] + [2]x1 + x2 + [2]x3   
POL(F40_IN(x1, x2)) = [2]x1   
POL(F55_IN(x1, x2, x3, x4)) = [3] + [2]x1 + x2 + [2]x3   
POL(F73_IN(x1, x2, x3)) = [2] + [2]x1 + [2]x2 + [2]x3   
POL(U10(x1, x2, x3, x4, x5)) = x1   
POL(U11'(x1, x2, x3, x4)) = [1] + [2]x4   
POL(U2(x1, x2, x3)) = 0   
POL(U4(x1, x2, x3)) = 0   
POL(U5'(x1, x2, x3, x4)) = [1] + [2]x2 + x3 + [2]x4   
POL(U7(x1, x2, x3, x4, x5)) = [2]x2 + [2]x4   
POL(U7'(x1, x2, x3, x4, x5)) = [1] + [2]x2 + [2]x4   
POL(U8(x1, x2, x3, x4, x5)) = [2]x2 + x4   
POL(U9(x1, x2, x3, x4, x5)) = [2]x3 + [2]x5   
POL(U9'(x1, x2, x3, x4, x5)) = [2]x4   
POL(c) = 0   
POL(c(x1)) = x1   
POL(c18(x1, x2)) = x1 + x2   
POL(c19(x1)) = x1   
POL(c21(x1, x2)) = x1 + x2   
POL(c22(x1)) = x1   
POL(c4(x1)) = x1   
POL(c7(x1)) = x1   
POL(f21_in(x1, x2)) = 0   
POL(f21_out1) = 0   
POL(f35_in(x1, x2, x3, x4)) = [2]x1 + x2 + [3]x3   
POL(f35_out1) = 0   
POL(f40_in(x1, x2)) = x2   
POL(f40_out1) = 0   
POL(f55_in(x1, x2, x3, x4)) = [3] + [2]x1 + [2]x2 + [2]x4   
POL(f55_out1) = 0   
POL(nil) = 0   
POL(tree(x1, x2, x3)) = [2] + x1 + x2 + x3   

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(nil) → f2_out1
f2_in(tree(z0, z1, z2)) → U1(f17_in(z0, z1, z2), tree(z0, z1, z2))
U1(f17_out1, tree(z0, z1, z2)) → f2_out1
f40_in(nil, z0) → f40_out1
f40_in(tree(z0, z1, z2), z3) → U2(f55_in(z0, z1, z2, z3), tree(z0, z1, z2), z3)
U2(f55_out1, tree(z0, z1, z2), z3) → f40_out1
f22_in(nil) → f22_out1
f22_in(tree(z0, z1, z2)) → U3(f73_in(z0, z1, z2), tree(z0, z1, z2))
U3(f73_out1, tree(z0, z1, z2)) → f22_out1
f21_in(nil, z0) → f21_out1
f21_in(tree(z0, z1, z2), z3) → U4(f35_in(z0, z1, z2, z3), tree(z0, z1, z2), z3)
U4(f35_out1, tree(z0, z1, z2), z3) → f21_out1
f17_in(z0, z1, z2) → U5(f21_in(z0, z1), z0, z1, z2)
U5(f21_out1, z0, z1, z2) → U6(f22_in(z2), z0, z1, z2)
U6(f22_out1, z0, z1, z2) → f17_out1
f35_in(z0, z1, z2, z3) → U7(f40_in(z0, z1), z0, z1, z2, z3)
U7(f40_out1, z0, z1, z2, z3) → U8(f40_in(z2, z3), z0, z1, z2, z3)
U8(f40_out1, z0, z1, z2, z3) → f35_out1
f55_in(z0, z1, z2, z3) → U9(f40_in(z0, z1), z0, z1, z2, z3)
U9(f40_out1, z0, z1, z2, z3) → U10(f40_in(z2, z3), z0, z1, z2, z3)
U10(f40_out1, z0, z1, z2, z3) → f55_out1
f73_in(z0, z1, z2) → U11(f40_in(z0, z1), z0, z1, z2)
U11(f40_out1, z0, z1, z2) → U12(f22_in(z2), z0, z1, z2)
U12(f22_out1, z0, z1, z2) → f73_out1
Tuples:

F55_IN(z0, z1, z2, z3) → c18(U9'(f40_in(z0, z1), z0, z1, z2, z3), F40_IN(z0, z1))
F73_IN(z0, z1, z2) → c21(U11'(f40_in(z0, z1), z0, z1, z2), F40_IN(z0, z1))
F2_IN(tree(z0, z1, z2)) → c(F17_IN(z0, z1, z2))
F21_IN(tree(z0, z1, z2), z3) → c(F35_IN(z0, z1, z2, z3))
F17_IN(z0, z1, z2) → c(U5'(f21_in(z0, z1), z0, z1, z2))
F17_IN(z0, z1, z2) → c(F21_IN(z0, z1))
U5'(f21_out1, z0, z1, z2) → c(F22_IN(z2))
F35_IN(z0, z1, z2, z3) → c(U7'(f40_in(z0, z1), z0, z1, z2, z3))
F35_IN(z0, z1, z2, z3) → c(F40_IN(z0, z1))
U7'(f40_out1, z0, z1, z2, z3) → c(F40_IN(z2, z3))
F40_IN(tree(z0, z1, z2), z3) → c4(F55_IN(z0, z1, z2, z3))
F22_IN(tree(z0, z1, z2)) → c7(F73_IN(z0, z1, z2))
U9'(f40_out1, z0, z1, z2, z3) → c19(F40_IN(z2, z3))
U11'(f40_out1, z0, z1, z2) → c22(F22_IN(z2))
F2_IN(tree(z0, z1, z2)) → c
F21_IN(tree(z0, z1, z2), z3) → c
U5'(f21_out1, z0, z1, z2) → c
U7'(f40_out1, z0, z1, z2, z3) → c
S tuples:none
K tuples:

F2_IN(tree(z0, z1, z2)) → c(F17_IN(z0, z1, z2))
F17_IN(z0, z1, z2) → c(U5'(f21_in(z0, z1), z0, z1, z2))
F17_IN(z0, z1, z2) → c(F21_IN(z0, z1))
U5'(f21_out1, z0, z1, z2) → c(F22_IN(z2))
F2_IN(tree(z0, z1, z2)) → c
F21_IN(tree(z0, z1, z2), z3) → c
U5'(f21_out1, z0, z1, z2) → c
F21_IN(tree(z0, z1, z2), z3) → c(F35_IN(z0, z1, z2, z3))
F35_IN(z0, z1, z2, z3) → c(U7'(f40_in(z0, z1), z0, z1, z2, z3))
F35_IN(z0, z1, z2, z3) → c(F40_IN(z0, z1))
U7'(f40_out1, z0, z1, z2, z3) → c(F40_IN(z2, z3))
U7'(f40_out1, z0, z1, z2, z3) → c
F22_IN(tree(z0, z1, z2)) → c7(F73_IN(z0, z1, z2))
F73_IN(z0, z1, z2) → c21(U11'(f40_in(z0, z1), z0, z1, z2), F40_IN(z0, z1))
U11'(f40_out1, z0, z1, z2) → c22(F22_IN(z2))
U9'(f40_out1, z0, z1, z2, z3) → c19(F40_IN(z2, z3))
F55_IN(z0, z1, z2, z3) → c18(U9'(f40_in(z0, z1), z0, z1, z2, z3), F40_IN(z0, z1))
F40_IN(tree(z0, z1, z2), z3) → c4(F55_IN(z0, z1, z2, z3))
Defined Rule Symbols:

f2_in, U1, f40_in, U2, f22_in, U3, f21_in, U4, f17_in, U5, U6, f35_in, U7, U8, f55_in, U9, U10, f73_in, U11, U12

Defined Pair Symbols:

F55_IN, F73_IN, F2_IN, F21_IN, F17_IN, U5', F35_IN, U7', F40_IN, F22_IN, U9', U11'

Compound Symbols:

c18, c21, c, c4, c7, c19, c22, c

(33) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(34) BOUNDS(O(1), O(1))