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

0 Prolog
↳1 PrologToCdtProblemTransformerProof (UPPER BOUND (ID), 820 ms)
↳2 CdtProblem
    ↳3 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳4 CdtProblem
    ↳5 CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID), 42 ms)
    ↳6 CdtProblem
    ↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))), 688 ms)
    ↳8 CdtProblem
    ↳9 CdtKnowledgeProof (⇔, 0 ms)
    ↳10 CdtProblem
    ↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 537 ms)
    ↳12 CdtProblem
    ↳13 CdtKnowledgeProof (⇔, 0 ms)
    ↳14 CdtProblem
↳15 PrologToCdtProblemTransformerProof (UPPER BOUND (ID), 805 ms)
↳16 CdtProblem
    ↳17 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳18 CdtProblem
    ↳19 CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID), 51 ms)
    ↳20 CdtProblem
    ↳21 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))), 736 ms)
    ↳22 CdtProblem
    ↳23 CdtKnowledgeProof (⇔, 0 ms)
    ↳24 CdtProblem
    ↳25 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 531 ms)
    ↳26 CdtProblem
    ↳27 CdtKnowledgeProof (⇔, 0 ms)
    ↳28 CdtProblem
    ↳29 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))), 494 ms)
    ↳30 CdtProblem
    ↳31 CdtKnowledgeProof (⇔, 1 ms)
    ↳32 BOUNDS(O(1), O(1))

(0) Obligation:

Clauses:

select(X, Y, Zs) :- ','(no(empty(Y)), ','(head(Y, X), tail(Y, Zs))).
select(X, Y, Z) :- ','(no(empty(Y)), ','(head(Y, H), ','(head(Z, H), ','(tail(Y, T), ','(tail(Z, Zs), select(X, T, Zs)))))).
head([], X1).
head(.(H, X2), H).
tail([], []).
tail(.(X3, T), T).
empty([]).
no(X) :- ','(X, ','(!, failure(a))).
no(X4).
failure(b).

Query: select(g,g,a)

(1) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)

Built complexity over-approximating cdt problems from derivation graph.

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, .(z0, z1)) → f1_out1
f1_in(z0, .(z0, z1)) → U1(f114_in(z0, z1), z0, .(z0, z1))
f1_in(z0, .(z0, z1)) → U2(f1_in(z0, z1), z0, .(z0, z1))
f1_in(z0, .(z0, z1)) → U3(f476_in(z0, z1), z0, .(z0, z1))
f1_in(z0, .(z0, z1)) → U4(f1_in(z0, z1), z0, .(z0, z1))
f1_in(z0, .(z1, z2)) → U5(f565_in(z0, z2, z1), z0, .(z1, z2))
f1_in(z0, .(z1, z2)) → U6(f1_in(z0, z2), z0, .(z1, z2))
U1(f114_out1, z0, .(z0, z1)) → f1_out1
U1(f114_out2(z0), z1, .(z1, z2)) → f1_out1
U1(f114_out5(z0), z1, .(z1, z2)) → f1_out1
U2(f1_out1, z0, .(z0, z1)) → f1_out1
U3(f476_out1, z0, .(z0, z1)) → f1_out1
U3(f476_out2(z0), z1, .(z1, z2)) → f1_out1
U3(f476_out5(z0), z1, .(z1, z2)) → f1_out1
U4(f1_out1, z0, .(z0, z1)) → f1_out1
U5(f565_out1, z0, .(z1, z2)) → f1_out1
U5(f565_out2(z0), z1, .(z2, z3)) → f1_out1
U5(f565_out5(z0), z1, .(z2, z3)) → f1_out1
U6(f1_out1, z0, .(z1, z2)) → f1_out1
f115_in(z0, .(z0, [])) → f115_out1
f115_in(z0, .(z0, [])) → U7(f227_in(z0), z0, .(z0, []))
f115_in(z0, .(z0, z1)) → U8(f324_in(z0, z1), z0, .(z0, z1))
f115_in(z0, .(z1, z2)) → U9(f379_in(z0, z2, z1), z0, .(z1, z2))
U7(f227_out1, z0, .(z0, [])) → f115_out1
U7(f227_out2(z0), z1, .(z1, [])) → f115_out1
U7(f227_out5(z0, z1), z2, .(z2, [])) → f115_out1
U8(f324_out1, z0, .(z0, z1)) → f115_out1
U8(f324_out2(z0), z1, .(z1, z2)) → f115_out1
U8(f324_out5(z0, z1), z2, .(z2, z3)) → f115_out1
U9(f379_out1, z0, .(z1, z2)) → f115_out1
U9(f379_out2(z0), z1, .(z2, z3)) → f115_out1
U9(f379_out5(z0, z1), z2, .(z3, z4)) → f115_out1
f568_in(z0, z1, z2) → U10(f1_in(z0, z1), z0, z1, z2)
U10(f1_out1, z0, z1, z2) → f568_out4(z1)
f480_in(z0, z1) → U11(f1_in(z0, z1), z0, z1)
U11(f1_out1, z0, z1) → f480_out4(z1)
f117_in(z0, z1) → U12(f1_in(z0, z1), z0, z1)
U12(f1_out1, z0, z1) → f117_out4(z1)
f114_in(z0, z1) → U13(f115_in(z0, z1), f117_in(z0, z1), z0, z1)
U13(f115_out1, z0, z1, z2) → f114_out1
U13(z0, f117_out1(z1), z2, z3) → f114_out2(z1)
U13(z0, f117_out4(z1), z2, z3) → f114_out5(z1)
f227_in(z0) → U14(f229_in(z0), f230_in(z0), z0)
U14(f229_out1, z0, z1) → f227_out1
U14(z0, f230_out1(z1), z2) → f227_out2(z1)
U14(z0, f230_out4(z1, z2), z3) → f227_out5(z1, z2)
f324_in(z0, z1) → U15(f115_in(z0, z1), f328_in(z0, z1), z0, z1)
U15(f115_out1, z0, z1, z2) → f324_out1
U15(z0, f328_out1(z1), z2, z3) → f324_out2(z1)
U15(z0, f328_out4(z1, z2), z3, z4) → f324_out5(z1, z2)
f379_in(z0, z1, z2) → U16(f115_in(z0, z1), f382_in(z0, z1, z2), z0, z1, z2)
U16(f115_out1, z0, z1, z2, z3) → f379_out1
U16(z0, f382_out1(z1), z2, z3, z4) → f379_out2(z1)
U16(z0, f382_out4(z1, z2), z3, z4, z5) → f379_out5(z1, z2)
f476_in(z0, z1) → U17(f115_in(z0, z1), f480_in(z0, z1), z0, z1)
U17(f115_out1, z0, z1, z2) → f476_out1
U17(z0, f480_out1(z1), z2, z3) → f476_out2(z1)
U17(z0, f480_out4(z1), z2, z3) → f476_out5(z1)
f565_in(z0, z1, z2) → U18(f115_in(z0, z1), f568_in(z0, z1, z2), z0, z1, z2)
U18(f115_out1, z0, z1, z2, z3) → f565_out1
U18(z0, f568_out1(z1), z2, z3, z4) → f565_out2(z1)
U18(z0, f568_out4(z1), z2, z3, z4) → f565_out5(z1)
Tuples:

F1_IN(z0, .(z0, z1)) → c1(U1'(f114_in(z0, z1), z0, .(z0, z1)), F114_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c2(U2'(f1_in(z0, z1), z0, .(z0, z1)), F1_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c3(U3'(f476_in(z0, z1), z0, .(z0, z1)), F476_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c4(U4'(f1_in(z0, z1), z0, .(z0, z1)), F1_IN(z0, z1))
F1_IN(z0, .(z1, z2)) → c5(U5'(f565_in(z0, z2, z1), z0, .(z1, z2)), F565_IN(z0, z2, z1))
F1_IN(z0, .(z1, z2)) → c6(U6'(f1_in(z0, z2), z0, .(z1, z2)), F1_IN(z0, z2))
F115_IN(z0, .(z0, [])) → c20(U7'(f227_in(z0), z0, .(z0, [])), F227_IN(z0))
F115_IN(z0, .(z0, z1)) → c21(U8'(f324_in(z0, z1), z0, .(z0, z1)), F324_IN(z0, z1))
F115_IN(z0, .(z1, z2)) → c22(U9'(f379_in(z0, z2, z1), z0, .(z1, z2)), F379_IN(z0, z2, z1))
F568_IN(z0, z1, z2) → c32(U10'(f1_in(z0, z1), z0, z1, z2), F1_IN(z0, z1))
F480_IN(z0, z1) → c34(U11'(f1_in(z0, z1), z0, z1), F1_IN(z0, z1))
F117_IN(z0, z1) → c36(U12'(f1_in(z0, z1), z0, z1), F1_IN(z0, z1))
F114_IN(z0, z1) → c38(U13'(f115_in(z0, z1), f117_in(z0, z1), z0, z1), F115_IN(z0, z1), F117_IN(z0, z1))
F227_IN(z0) → c42(U14'(f229_in(z0), f230_in(z0), z0))
F324_IN(z0, z1) → c46(U15'(f115_in(z0, z1), f328_in(z0, z1), z0, z1), F115_IN(z0, z1))
F379_IN(z0, z1, z2) → c50(U16'(f115_in(z0, z1), f382_in(z0, z1, z2), z0, z1, z2), F115_IN(z0, z1))
F476_IN(z0, z1) → c54(U17'(f115_in(z0, z1), f480_in(z0, z1), z0, z1), F115_IN(z0, z1), F480_IN(z0, z1))
F565_IN(z0, z1, z2) → c58(U18'(f115_in(z0, z1), f568_in(z0, z1, z2), z0, z1, z2), F115_IN(z0, z1), F568_IN(z0, z1, z2))
S tuples:

F1_IN(z0, .(z0, z1)) → c1(U1'(f114_in(z0, z1), z0, .(z0, z1)), F114_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c2(U2'(f1_in(z0, z1), z0, .(z0, z1)), F1_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c3(U3'(f476_in(z0, z1), z0, .(z0, z1)), F476_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c4(U4'(f1_in(z0, z1), z0, .(z0, z1)), F1_IN(z0, z1))
F1_IN(z0, .(z1, z2)) → c5(U5'(f565_in(z0, z2, z1), z0, .(z1, z2)), F565_IN(z0, z2, z1))
F1_IN(z0, .(z1, z2)) → c6(U6'(f1_in(z0, z2), z0, .(z1, z2)), F1_IN(z0, z2))
F115_IN(z0, .(z0, [])) → c20(U7'(f227_in(z0), z0, .(z0, [])), F227_IN(z0))
F115_IN(z0, .(z0, z1)) → c21(U8'(f324_in(z0, z1), z0, .(z0, z1)), F324_IN(z0, z1))
F115_IN(z0, .(z1, z2)) → c22(U9'(f379_in(z0, z2, z1), z0, .(z1, z2)), F379_IN(z0, z2, z1))
F568_IN(z0, z1, z2) → c32(U10'(f1_in(z0, z1), z0, z1, z2), F1_IN(z0, z1))
F480_IN(z0, z1) → c34(U11'(f1_in(z0, z1), z0, z1), F1_IN(z0, z1))
F117_IN(z0, z1) → c36(U12'(f1_in(z0, z1), z0, z1), F1_IN(z0, z1))
F114_IN(z0, z1) → c38(U13'(f115_in(z0, z1), f117_in(z0, z1), z0, z1), F115_IN(z0, z1), F117_IN(z0, z1))
F227_IN(z0) → c42(U14'(f229_in(z0), f230_in(z0), z0))
F324_IN(z0, z1) → c46(U15'(f115_in(z0, z1), f328_in(z0, z1), z0, z1), F115_IN(z0, z1))
F379_IN(z0, z1, z2) → c50(U16'(f115_in(z0, z1), f382_in(z0, z1, z2), z0, z1, z2), F115_IN(z0, z1))
F476_IN(z0, z1) → c54(U17'(f115_in(z0, z1), f480_in(z0, z1), z0, z1), F115_IN(z0, z1), F480_IN(z0, z1))
F565_IN(z0, z1, z2) → c58(U18'(f115_in(z0, z1), f568_in(z0, z1, z2), z0, z1, z2), F115_IN(z0, z1), F568_IN(z0, z1, z2))
K tuples:none
Defined Rule Symbols:

f1_in, U1, U2, U3, U4, U5, U6, f115_in, U7, U8, U9, f568_in, U10, f480_in, U11, f117_in, U12, f114_in, U13, f227_in, U14, f324_in, U15, f379_in, U16, f476_in, U17, f565_in, U18

Defined Pair Symbols:

F1_IN, F115_IN, F568_IN, F480_IN, F117_IN, F114_IN, F227_IN, F324_IN, F379_IN, F476_IN, F565_IN

Compound Symbols:

c1, c2, c3, c4, c5, c6, c20, c21, c22, c32, c34, c36, c38, c42, c46, c50, c54, c58

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

Split RHS of tuples not part of any SCC

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, .(z0, z1)) → f1_out1
f1_in(z0, .(z0, z1)) → U1(f114_in(z0, z1), z0, .(z0, z1))
f1_in(z0, .(z0, z1)) → U2(f1_in(z0, z1), z0, .(z0, z1))
f1_in(z0, .(z0, z1)) → U3(f476_in(z0, z1), z0, .(z0, z1))
f1_in(z0, .(z0, z1)) → U4(f1_in(z0, z1), z0, .(z0, z1))
f1_in(z0, .(z1, z2)) → U5(f565_in(z0, z2, z1), z0, .(z1, z2))
f1_in(z0, .(z1, z2)) → U6(f1_in(z0, z2), z0, .(z1, z2))
U1(f114_out1, z0, .(z0, z1)) → f1_out1
U1(f114_out2(z0), z1, .(z1, z2)) → f1_out1
U1(f114_out5(z0), z1, .(z1, z2)) → f1_out1
U2(f1_out1, z0, .(z0, z1)) → f1_out1
U3(f476_out1, z0, .(z0, z1)) → f1_out1
U3(f476_out2(z0), z1, .(z1, z2)) → f1_out1
U3(f476_out5(z0), z1, .(z1, z2)) → f1_out1
U4(f1_out1, z0, .(z0, z1)) → f1_out1
U5(f565_out1, z0, .(z1, z2)) → f1_out1
U5(f565_out2(z0), z1, .(z2, z3)) → f1_out1
U5(f565_out5(z0), z1, .(z2, z3)) → f1_out1
U6(f1_out1, z0, .(z1, z2)) → f1_out1
f115_in(z0, .(z0, [])) → f115_out1
f115_in(z0, .(z0, [])) → U7(f227_in(z0), z0, .(z0, []))
f115_in(z0, .(z0, z1)) → U8(f324_in(z0, z1), z0, .(z0, z1))
f115_in(z0, .(z1, z2)) → U9(f379_in(z0, z2, z1), z0, .(z1, z2))
U7(f227_out1, z0, .(z0, [])) → f115_out1
U7(f227_out2(z0), z1, .(z1, [])) → f115_out1
U7(f227_out5(z0, z1), z2, .(z2, [])) → f115_out1
U8(f324_out1, z0, .(z0, z1)) → f115_out1
U8(f324_out2(z0), z1, .(z1, z2)) → f115_out1
U8(f324_out5(z0, z1), z2, .(z2, z3)) → f115_out1
U9(f379_out1, z0, .(z1, z2)) → f115_out1
U9(f379_out2(z0), z1, .(z2, z3)) → f115_out1
U9(f379_out5(z0, z1), z2, .(z3, z4)) → f115_out1
f568_in(z0, z1, z2) → U10(f1_in(z0, z1), z0, z1, z2)
U10(f1_out1, z0, z1, z2) → f568_out4(z1)
f480_in(z0, z1) → U11(f1_in(z0, z1), z0, z1)
U11(f1_out1, z0, z1) → f480_out4(z1)
f117_in(z0, z1) → U12(f1_in(z0, z1), z0, z1)
U12(f1_out1, z0, z1) → f117_out4(z1)
f114_in(z0, z1) → U13(f115_in(z0, z1), f117_in(z0, z1), z0, z1)
U13(f115_out1, z0, z1, z2) → f114_out1
U13(z0, f117_out1(z1), z2, z3) → f114_out2(z1)
U13(z0, f117_out4(z1), z2, z3) → f114_out5(z1)
f227_in(z0) → U14(f229_in(z0), f230_in(z0), z0)
U14(f229_out1, z0, z1) → f227_out1
U14(z0, f230_out1(z1), z2) → f227_out2(z1)
U14(z0, f230_out4(z1, z2), z3) → f227_out5(z1, z2)
f324_in(z0, z1) → U15(f115_in(z0, z1), f328_in(z0, z1), z0, z1)
U15(f115_out1, z0, z1, z2) → f324_out1
U15(z0, f328_out1(z1), z2, z3) → f324_out2(z1)
U15(z0, f328_out4(z1, z2), z3, z4) → f324_out5(z1, z2)
f379_in(z0, z1, z2) → U16(f115_in(z0, z1), f382_in(z0, z1, z2), z0, z1, z2)
U16(f115_out1, z0, z1, z2, z3) → f379_out1
U16(z0, f382_out1(z1), z2, z3, z4) → f379_out2(z1)
U16(z0, f382_out4(z1, z2), z3, z4, z5) → f379_out5(z1, z2)
f476_in(z0, z1) → U17(f115_in(z0, z1), f480_in(z0, z1), z0, z1)
U17(f115_out1, z0, z1, z2) → f476_out1
U17(z0, f480_out1(z1), z2, z3) → f476_out2(z1)
U17(z0, f480_out4(z1), z2, z3) → f476_out5(z1)
f565_in(z0, z1, z2) → U18(f115_in(z0, z1), f568_in(z0, z1, z2), z0, z1, z2)
U18(f115_out1, z0, z1, z2, z3) → f565_out1
U18(z0, f568_out1(z1), z2, z3, z4) → f565_out2(z1)
U18(z0, f568_out4(z1), z2, z3, z4) → f565_out5(z1)
Tuples:

F1_IN(z0, .(z0, z1)) → c1(U1'(f114_in(z0, z1), z0, .(z0, z1)), F114_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c2(U2'(f1_in(z0, z1), z0, .(z0, z1)), F1_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c3(U3'(f476_in(z0, z1), z0, .(z0, z1)), F476_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c4(U4'(f1_in(z0, z1), z0, .(z0, z1)), F1_IN(z0, z1))
F1_IN(z0, .(z1, z2)) → c5(U5'(f565_in(z0, z2, z1), z0, .(z1, z2)), F565_IN(z0, z2, z1))
F1_IN(z0, .(z1, z2)) → c6(U6'(f1_in(z0, z2), z0, .(z1, z2)), F1_IN(z0, z2))
F115_IN(z0, .(z0, z1)) → c21(U8'(f324_in(z0, z1), z0, .(z0, z1)), F324_IN(z0, z1))
F115_IN(z0, .(z1, z2)) → c22(U9'(f379_in(z0, z2, z1), z0, .(z1, z2)), F379_IN(z0, z2, z1))
F568_IN(z0, z1, z2) → c32(U10'(f1_in(z0, z1), z0, z1, z2), F1_IN(z0, z1))
F480_IN(z0, z1) → c34(U11'(f1_in(z0, z1), z0, z1), F1_IN(z0, z1))
F117_IN(z0, z1) → c36(U12'(f1_in(z0, z1), z0, z1), F1_IN(z0, z1))
F114_IN(z0, z1) → c38(U13'(f115_in(z0, z1), f117_in(z0, z1), z0, z1), F115_IN(z0, z1), F117_IN(z0, z1))
F227_IN(z0) → c42(U14'(f229_in(z0), f230_in(z0), z0))
F324_IN(z0, z1) → c46(U15'(f115_in(z0, z1), f328_in(z0, z1), z0, z1), F115_IN(z0, z1))
F379_IN(z0, z1, z2) → c50(U16'(f115_in(z0, z1), f382_in(z0, z1, z2), z0, z1, z2), F115_IN(z0, z1))
F476_IN(z0, z1) → c54(U17'(f115_in(z0, z1), f480_in(z0, z1), z0, z1), F115_IN(z0, z1), F480_IN(z0, z1))
F565_IN(z0, z1, z2) → c58(U18'(f115_in(z0, z1), f568_in(z0, z1, z2), z0, z1, z2), F115_IN(z0, z1), F568_IN(z0, z1, z2))
F115_IN(z0, .(z0, [])) → c(U7'(f227_in(z0), z0, .(z0, [])))
F115_IN(z0, .(z0, [])) → c(F227_IN(z0))
S tuples:

F1_IN(z0, .(z0, z1)) → c1(U1'(f114_in(z0, z1), z0, .(z0, z1)), F114_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c2(U2'(f1_in(z0, z1), z0, .(z0, z1)), F1_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c3(U3'(f476_in(z0, z1), z0, .(z0, z1)), F476_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c4(U4'(f1_in(z0, z1), z0, .(z0, z1)), F1_IN(z0, z1))
F1_IN(z0, .(z1, z2)) → c5(U5'(f565_in(z0, z2, z1), z0, .(z1, z2)), F565_IN(z0, z2, z1))
F1_IN(z0, .(z1, z2)) → c6(U6'(f1_in(z0, z2), z0, .(z1, z2)), F1_IN(z0, z2))
F115_IN(z0, .(z0, z1)) → c21(U8'(f324_in(z0, z1), z0, .(z0, z1)), F324_IN(z0, z1))
F115_IN(z0, .(z1, z2)) → c22(U9'(f379_in(z0, z2, z1), z0, .(z1, z2)), F379_IN(z0, z2, z1))
F568_IN(z0, z1, z2) → c32(U10'(f1_in(z0, z1), z0, z1, z2), F1_IN(z0, z1))
F480_IN(z0, z1) → c34(U11'(f1_in(z0, z1), z0, z1), F1_IN(z0, z1))
F117_IN(z0, z1) → c36(U12'(f1_in(z0, z1), z0, z1), F1_IN(z0, z1))
F114_IN(z0, z1) → c38(U13'(f115_in(z0, z1), f117_in(z0, z1), z0, z1), F115_IN(z0, z1), F117_IN(z0, z1))
F227_IN(z0) → c42(U14'(f229_in(z0), f230_in(z0), z0))
F324_IN(z0, z1) → c46(U15'(f115_in(z0, z1), f328_in(z0, z1), z0, z1), F115_IN(z0, z1))
F379_IN(z0, z1, z2) → c50(U16'(f115_in(z0, z1), f382_in(z0, z1, z2), z0, z1, z2), F115_IN(z0, z1))
F476_IN(z0, z1) → c54(U17'(f115_in(z0, z1), f480_in(z0, z1), z0, z1), F115_IN(z0, z1), F480_IN(z0, z1))
F565_IN(z0, z1, z2) → c58(U18'(f115_in(z0, z1), f568_in(z0, z1, z2), z0, z1, z2), F115_IN(z0, z1), F568_IN(z0, z1, z2))
F115_IN(z0, .(z0, [])) → c(U7'(f227_in(z0), z0, .(z0, [])))
F115_IN(z0, .(z0, [])) → c(F227_IN(z0))
K tuples:none
Defined Rule Symbols:

f1_in, U1, U2, U3, U4, U5, U6, f115_in, U7, U8, U9, f568_in, U10, f480_in, U11, f117_in, U12, f114_in, U13, f227_in, U14, f324_in, U15, f379_in, U16, f476_in, U17, f565_in, U18

Defined Pair Symbols:

F1_IN, F115_IN, F568_IN, F480_IN, F117_IN, F114_IN, F227_IN, F324_IN, F379_IN, F476_IN, F565_IN

Compound Symbols:

c1, c2, c3, c4, c5, c6, c21, c22, c32, c34, c36, c38, c42, c46, c50, c54, c58, c

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

Removed 18 trailing tuple parts

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, .(z0, z1)) → f1_out1
f1_in(z0, .(z0, z1)) → U1(f114_in(z0, z1), z0, .(z0, z1))
f1_in(z0, .(z0, z1)) → U2(f1_in(z0, z1), z0, .(z0, z1))
f1_in(z0, .(z0, z1)) → U3(f476_in(z0, z1), z0, .(z0, z1))
f1_in(z0, .(z0, z1)) → U4(f1_in(z0, z1), z0, .(z0, z1))
f1_in(z0, .(z1, z2)) → U5(f565_in(z0, z2, z1), z0, .(z1, z2))
f1_in(z0, .(z1, z2)) → U6(f1_in(z0, z2), z0, .(z1, z2))
U1(f114_out1, z0, .(z0, z1)) → f1_out1
U1(f114_out2(z0), z1, .(z1, z2)) → f1_out1
U1(f114_out5(z0), z1, .(z1, z2)) → f1_out1
U2(f1_out1, z0, .(z0, z1)) → f1_out1
U3(f476_out1, z0, .(z0, z1)) → f1_out1
U3(f476_out2(z0), z1, .(z1, z2)) → f1_out1
U3(f476_out5(z0), z1, .(z1, z2)) → f1_out1
U4(f1_out1, z0, .(z0, z1)) → f1_out1
U5(f565_out1, z0, .(z1, z2)) → f1_out1
U5(f565_out2(z0), z1, .(z2, z3)) → f1_out1
U5(f565_out5(z0), z1, .(z2, z3)) → f1_out1
U6(f1_out1, z0, .(z1, z2)) → f1_out1
f115_in(z0, .(z0, [])) → f115_out1
f115_in(z0, .(z0, [])) → U7(f227_in(z0), z0, .(z0, []))
f115_in(z0, .(z0, z1)) → U8(f324_in(z0, z1), z0, .(z0, z1))
f115_in(z0, .(z1, z2)) → U9(f379_in(z0, z2, z1), z0, .(z1, z2))
U7(f227_out1, z0, .(z0, [])) → f115_out1
U7(f227_out2(z0), z1, .(z1, [])) → f115_out1
U7(f227_out5(z0, z1), z2, .(z2, [])) → f115_out1
U8(f324_out1, z0, .(z0, z1)) → f115_out1
U8(f324_out2(z0), z1, .(z1, z2)) → f115_out1
U8(f324_out5(z0, z1), z2, .(z2, z3)) → f115_out1
U9(f379_out1, z0, .(z1, z2)) → f115_out1
U9(f379_out2(z0), z1, .(z2, z3)) → f115_out1
U9(f379_out5(z0, z1), z2, .(z3, z4)) → f115_out1
f568_in(z0, z1, z2) → U10(f1_in(z0, z1), z0, z1, z2)
U10(f1_out1, z0, z1, z2) → f568_out4(z1)
f480_in(z0, z1) → U11(f1_in(z0, z1), z0, z1)
U11(f1_out1, z0, z1) → f480_out4(z1)
f117_in(z0, z1) → U12(f1_in(z0, z1), z0, z1)
U12(f1_out1, z0, z1) → f117_out4(z1)
f114_in(z0, z1) → U13(f115_in(z0, z1), f117_in(z0, z1), z0, z1)
U13(f115_out1, z0, z1, z2) → f114_out1
U13(z0, f117_out1(z1), z2, z3) → f114_out2(z1)
U13(z0, f117_out4(z1), z2, z3) → f114_out5(z1)
f227_in(z0) → U14(f229_in(z0), f230_in(z0), z0)
U14(f229_out1, z0, z1) → f227_out1
U14(z0, f230_out1(z1), z2) → f227_out2(z1)
U14(z0, f230_out4(z1, z2), z3) → f227_out5(z1, z2)
f324_in(z0, z1) → U15(f115_in(z0, z1), f328_in(z0, z1), z0, z1)
U15(f115_out1, z0, z1, z2) → f324_out1
U15(z0, f328_out1(z1), z2, z3) → f324_out2(z1)
U15(z0, f328_out4(z1, z2), z3, z4) → f324_out5(z1, z2)
f379_in(z0, z1, z2) → U16(f115_in(z0, z1), f382_in(z0, z1, z2), z0, z1, z2)
U16(f115_out1, z0, z1, z2, z3) → f379_out1
U16(z0, f382_out1(z1), z2, z3, z4) → f379_out2(z1)
U16(z0, f382_out4(z1, z2), z3, z4, z5) → f379_out5(z1, z2)
f476_in(z0, z1) → U17(f115_in(z0, z1), f480_in(z0, z1), z0, z1)
U17(f115_out1, z0, z1, z2) → f476_out1
U17(z0, f480_out1(z1), z2, z3) → f476_out2(z1)
U17(z0, f480_out4(z1), z2, z3) → f476_out5(z1)
f565_in(z0, z1, z2) → U18(f115_in(z0, z1), f568_in(z0, z1, z2), z0, z1, z2)
U18(f115_out1, z0, z1, z2, z3) → f565_out1
U18(z0, f568_out1(z1), z2, z3, z4) → f565_out2(z1)
U18(z0, f568_out4(z1), z2, z3, z4) → f565_out5(z1)
Tuples:

F115_IN(z0, .(z0, [])) → c(F227_IN(z0))
F1_IN(z0, .(z0, z1)) → c1(F114_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c2(F1_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c3(F476_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c4(F1_IN(z0, z1))
F1_IN(z0, .(z1, z2)) → c5(F565_IN(z0, z2, z1))
F1_IN(z0, .(z1, z2)) → c6(F1_IN(z0, z2))
F115_IN(z0, .(z0, z1)) → c21(F324_IN(z0, z1))
F115_IN(z0, .(z1, z2)) → c22(F379_IN(z0, z2, z1))
F568_IN(z0, z1, z2) → c32(F1_IN(z0, z1))
F480_IN(z0, z1) → c34(F1_IN(z0, z1))
F117_IN(z0, z1) → c36(F1_IN(z0, z1))
F114_IN(z0, z1) → c38(F115_IN(z0, z1), F117_IN(z0, z1))
F227_IN(z0) → c42
F324_IN(z0, z1) → c46(F115_IN(z0, z1))
F379_IN(z0, z1, z2) → c50(F115_IN(z0, z1))
F476_IN(z0, z1) → c54(F115_IN(z0, z1), F480_IN(z0, z1))
F565_IN(z0, z1, z2) → c58(F115_IN(z0, z1), F568_IN(z0, z1, z2))
F115_IN(z0, .(z0, [])) → c
S tuples:

F115_IN(z0, .(z0, [])) → c(F227_IN(z0))
F1_IN(z0, .(z0, z1)) → c1(F114_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c2(F1_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c3(F476_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c4(F1_IN(z0, z1))
F1_IN(z0, .(z1, z2)) → c5(F565_IN(z0, z2, z1))
F1_IN(z0, .(z1, z2)) → c6(F1_IN(z0, z2))
F115_IN(z0, .(z0, z1)) → c21(F324_IN(z0, z1))
F115_IN(z0, .(z1, z2)) → c22(F379_IN(z0, z2, z1))
F568_IN(z0, z1, z2) → c32(F1_IN(z0, z1))
F480_IN(z0, z1) → c34(F1_IN(z0, z1))
F117_IN(z0, z1) → c36(F1_IN(z0, z1))
F114_IN(z0, z1) → c38(F115_IN(z0, z1), F117_IN(z0, z1))
F227_IN(z0) → c42
F324_IN(z0, z1) → c46(F115_IN(z0, z1))
F379_IN(z0, z1, z2) → c50(F115_IN(z0, z1))
F476_IN(z0, z1) → c54(F115_IN(z0, z1), F480_IN(z0, z1))
F565_IN(z0, z1, z2) → c58(F115_IN(z0, z1), F568_IN(z0, z1, z2))
F115_IN(z0, .(z0, [])) → c
K tuples:none
Defined Rule Symbols:

f1_in, U1, U2, U3, U4, U5, U6, f115_in, U7, U8, U9, f568_in, U10, f480_in, U11, f117_in, U12, f114_in, U13, f227_in, U14, f324_in, U15, f379_in, U16, f476_in, U17, f565_in, U18

Defined Pair Symbols:

F115_IN, F1_IN, F568_IN, F480_IN, F117_IN, F114_IN, F227_IN, F324_IN, F379_IN, F476_IN, F565_IN

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c21, c22, c32, c34, c36, c38, c42, c46, c50, c54, c58, c

(7) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

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

F1_IN(z0, .(z0, z1)) → c1(F114_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c2(F1_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c3(F476_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c4(F1_IN(z0, z1))
F1_IN(z0, .(z1, z2)) → c5(F565_IN(z0, z2, z1))
F1_IN(z0, .(z1, z2)) → c6(F1_IN(z0, z2))
F476_IN(z0, z1) → c54(F115_IN(z0, z1), F480_IN(z0, z1))
F565_IN(z0, z1, z2) → c58(F115_IN(z0, z1), F568_IN(z0, z1, z2))
We considered the (Usable) Rules:none
And the Tuples:

F115_IN(z0, .(z0, [])) → c(F227_IN(z0))
F1_IN(z0, .(z0, z1)) → c1(F114_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c2(F1_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c3(F476_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c4(F1_IN(z0, z1))
F1_IN(z0, .(z1, z2)) → c5(F565_IN(z0, z2, z1))
F1_IN(z0, .(z1, z2)) → c6(F1_IN(z0, z2))
F115_IN(z0, .(z0, z1)) → c21(F324_IN(z0, z1))
F115_IN(z0, .(z1, z2)) → c22(F379_IN(z0, z2, z1))
F568_IN(z0, z1, z2) → c32(F1_IN(z0, z1))
F480_IN(z0, z1) → c34(F1_IN(z0, z1))
F117_IN(z0, z1) → c36(F1_IN(z0, z1))
F114_IN(z0, z1) → c38(F115_IN(z0, z1), F117_IN(z0, z1))
F227_IN(z0) → c42
F324_IN(z0, z1) → c46(F115_IN(z0, z1))
F379_IN(z0, z1, z2) → c50(F115_IN(z0, z1))
F476_IN(z0, z1) → c54(F115_IN(z0, z1), F480_IN(z0, z1))
F565_IN(z0, z1, z2) → c58(F115_IN(z0, z1), F568_IN(z0, z1, z2))
F115_IN(z0, .(z0, [])) → c
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(.(x1, x2)) = [1] + x2   
POL(F114_IN(x1, x2)) = x2 + x22   
POL(F115_IN(x1, x2)) = 0   
POL(F117_IN(x1, x2)) = x2 + x22   
POL(F1_IN(x1, x2)) = x2 + x22   
POL(F227_IN(x1)) = 0   
POL(F324_IN(x1, x2)) = 0   
POL(F379_IN(x1, x2, x3)) = 0   
POL(F476_IN(x1, x2)) = [1] + x2 + x22   
POL(F480_IN(x1, x2)) = x2 + x22   
POL(F565_IN(x1, x2, x3)) = [1] + x2 + x22   
POL(F568_IN(x1, x2, x3)) = x2 + x22   
POL([]) = 0   
POL(c) = 0   
POL(c(x1)) = x1   
POL(c1(x1)) = x1   
POL(c2(x1)) = x1   
POL(c21(x1)) = x1   
POL(c22(x1)) = x1   
POL(c3(x1)) = x1   
POL(c32(x1)) = x1   
POL(c34(x1)) = x1   
POL(c36(x1)) = x1   
POL(c38(x1, x2)) = x1 + x2   
POL(c4(x1)) = x1   
POL(c42) = 0   
POL(c46(x1)) = x1   
POL(c5(x1)) = x1   
POL(c50(x1)) = x1   
POL(c54(x1, x2)) = x1 + x2   
POL(c58(x1, x2)) = x1 + x2   
POL(c6(x1)) = x1   

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, .(z0, z1)) → f1_out1
f1_in(z0, .(z0, z1)) → U1(f114_in(z0, z1), z0, .(z0, z1))
f1_in(z0, .(z0, z1)) → U2(f1_in(z0, z1), z0, .(z0, z1))
f1_in(z0, .(z0, z1)) → U3(f476_in(z0, z1), z0, .(z0, z1))
f1_in(z0, .(z0, z1)) → U4(f1_in(z0, z1), z0, .(z0, z1))
f1_in(z0, .(z1, z2)) → U5(f565_in(z0, z2, z1), z0, .(z1, z2))
f1_in(z0, .(z1, z2)) → U6(f1_in(z0, z2), z0, .(z1, z2))
U1(f114_out1, z0, .(z0, z1)) → f1_out1
U1(f114_out2(z0), z1, .(z1, z2)) → f1_out1
U1(f114_out5(z0), z1, .(z1, z2)) → f1_out1
U2(f1_out1, z0, .(z0, z1)) → f1_out1
U3(f476_out1, z0, .(z0, z1)) → f1_out1
U3(f476_out2(z0), z1, .(z1, z2)) → f1_out1
U3(f476_out5(z0), z1, .(z1, z2)) → f1_out1
U4(f1_out1, z0, .(z0, z1)) → f1_out1
U5(f565_out1, z0, .(z1, z2)) → f1_out1
U5(f565_out2(z0), z1, .(z2, z3)) → f1_out1
U5(f565_out5(z0), z1, .(z2, z3)) → f1_out1
U6(f1_out1, z0, .(z1, z2)) → f1_out1
f115_in(z0, .(z0, [])) → f115_out1
f115_in(z0, .(z0, [])) → U7(f227_in(z0), z0, .(z0, []))
f115_in(z0, .(z0, z1)) → U8(f324_in(z0, z1), z0, .(z0, z1))
f115_in(z0, .(z1, z2)) → U9(f379_in(z0, z2, z1), z0, .(z1, z2))
U7(f227_out1, z0, .(z0, [])) → f115_out1
U7(f227_out2(z0), z1, .(z1, [])) → f115_out1
U7(f227_out5(z0, z1), z2, .(z2, [])) → f115_out1
U8(f324_out1, z0, .(z0, z1)) → f115_out1
U8(f324_out2(z0), z1, .(z1, z2)) → f115_out1
U8(f324_out5(z0, z1), z2, .(z2, z3)) → f115_out1
U9(f379_out1, z0, .(z1, z2)) → f115_out1
U9(f379_out2(z0), z1, .(z2, z3)) → f115_out1
U9(f379_out5(z0, z1), z2, .(z3, z4)) → f115_out1
f568_in(z0, z1, z2) → U10(f1_in(z0, z1), z0, z1, z2)
U10(f1_out1, z0, z1, z2) → f568_out4(z1)
f480_in(z0, z1) → U11(f1_in(z0, z1), z0, z1)
U11(f1_out1, z0, z1) → f480_out4(z1)
f117_in(z0, z1) → U12(f1_in(z0, z1), z0, z1)
U12(f1_out1, z0, z1) → f117_out4(z1)
f114_in(z0, z1) → U13(f115_in(z0, z1), f117_in(z0, z1), z0, z1)
U13(f115_out1, z0, z1, z2) → f114_out1
U13(z0, f117_out1(z1), z2, z3) → f114_out2(z1)
U13(z0, f117_out4(z1), z2, z3) → f114_out5(z1)
f227_in(z0) → U14(f229_in(z0), f230_in(z0), z0)
U14(f229_out1, z0, z1) → f227_out1
U14(z0, f230_out1(z1), z2) → f227_out2(z1)
U14(z0, f230_out4(z1, z2), z3) → f227_out5(z1, z2)
f324_in(z0, z1) → U15(f115_in(z0, z1), f328_in(z0, z1), z0, z1)
U15(f115_out1, z0, z1, z2) → f324_out1
U15(z0, f328_out1(z1), z2, z3) → f324_out2(z1)
U15(z0, f328_out4(z1, z2), z3, z4) → f324_out5(z1, z2)
f379_in(z0, z1, z2) → U16(f115_in(z0, z1), f382_in(z0, z1, z2), z0, z1, z2)
U16(f115_out1, z0, z1, z2, z3) → f379_out1
U16(z0, f382_out1(z1), z2, z3, z4) → f379_out2(z1)
U16(z0, f382_out4(z1, z2), z3, z4, z5) → f379_out5(z1, z2)
f476_in(z0, z1) → U17(f115_in(z0, z1), f480_in(z0, z1), z0, z1)
U17(f115_out1, z0, z1, z2) → f476_out1
U17(z0, f480_out1(z1), z2, z3) → f476_out2(z1)
U17(z0, f480_out4(z1), z2, z3) → f476_out5(z1)
f565_in(z0, z1, z2) → U18(f115_in(z0, z1), f568_in(z0, z1, z2), z0, z1, z2)
U18(f115_out1, z0, z1, z2, z3) → f565_out1
U18(z0, f568_out1(z1), z2, z3, z4) → f565_out2(z1)
U18(z0, f568_out4(z1), z2, z3, z4) → f565_out5(z1)
Tuples:

F115_IN(z0, .(z0, [])) → c(F227_IN(z0))
F1_IN(z0, .(z0, z1)) → c1(F114_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c2(F1_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c3(F476_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c4(F1_IN(z0, z1))
F1_IN(z0, .(z1, z2)) → c5(F565_IN(z0, z2, z1))
F1_IN(z0, .(z1, z2)) → c6(F1_IN(z0, z2))
F115_IN(z0, .(z0, z1)) → c21(F324_IN(z0, z1))
F115_IN(z0, .(z1, z2)) → c22(F379_IN(z0, z2, z1))
F568_IN(z0, z1, z2) → c32(F1_IN(z0, z1))
F480_IN(z0, z1) → c34(F1_IN(z0, z1))
F117_IN(z0, z1) → c36(F1_IN(z0, z1))
F114_IN(z0, z1) → c38(F115_IN(z0, z1), F117_IN(z0, z1))
F227_IN(z0) → c42
F324_IN(z0, z1) → c46(F115_IN(z0, z1))
F379_IN(z0, z1, z2) → c50(F115_IN(z0, z1))
F476_IN(z0, z1) → c54(F115_IN(z0, z1), F480_IN(z0, z1))
F565_IN(z0, z1, z2) → c58(F115_IN(z0, z1), F568_IN(z0, z1, z2))
F115_IN(z0, .(z0, [])) → c
S tuples:

F115_IN(z0, .(z0, [])) → c(F227_IN(z0))
F115_IN(z0, .(z0, z1)) → c21(F324_IN(z0, z1))
F115_IN(z0, .(z1, z2)) → c22(F379_IN(z0, z2, z1))
F568_IN(z0, z1, z2) → c32(F1_IN(z0, z1))
F480_IN(z0, z1) → c34(F1_IN(z0, z1))
F117_IN(z0, z1) → c36(F1_IN(z0, z1))
F114_IN(z0, z1) → c38(F115_IN(z0, z1), F117_IN(z0, z1))
F227_IN(z0) → c42
F324_IN(z0, z1) → c46(F115_IN(z0, z1))
F379_IN(z0, z1, z2) → c50(F115_IN(z0, z1))
F115_IN(z0, .(z0, [])) → c
K tuples:

F1_IN(z0, .(z0, z1)) → c1(F114_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c2(F1_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c3(F476_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c4(F1_IN(z0, z1))
F1_IN(z0, .(z1, z2)) → c5(F565_IN(z0, z2, z1))
F1_IN(z0, .(z1, z2)) → c6(F1_IN(z0, z2))
F476_IN(z0, z1) → c54(F115_IN(z0, z1), F480_IN(z0, z1))
F565_IN(z0, z1, z2) → c58(F115_IN(z0, z1), F568_IN(z0, z1, z2))
Defined Rule Symbols:

f1_in, U1, U2, U3, U4, U5, U6, f115_in, U7, U8, U9, f568_in, U10, f480_in, U11, f117_in, U12, f114_in, U13, f227_in, U14, f324_in, U15, f379_in, U16, f476_in, U17, f565_in, U18

Defined Pair Symbols:

F115_IN, F1_IN, F568_IN, F480_IN, F117_IN, F114_IN, F227_IN, F324_IN, F379_IN, F476_IN, F565_IN

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c21, c22, c32, c34, c36, c38, c42, c46, c50, c54, c58, c

(9) CdtKnowledgeProof (EQUIVALENT transformation)

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

F568_IN(z0, z1, z2) → c32(F1_IN(z0, z1))
F480_IN(z0, z1) → c34(F1_IN(z0, z1))
F114_IN(z0, z1) → c38(F115_IN(z0, z1), F117_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c1(F114_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c2(F1_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c3(F476_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c4(F1_IN(z0, z1))
F1_IN(z0, .(z1, z2)) → c5(F565_IN(z0, z2, z1))
F1_IN(z0, .(z1, z2)) → c6(F1_IN(z0, z2))
F1_IN(z0, .(z0, z1)) → c1(F114_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c2(F1_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c3(F476_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c4(F1_IN(z0, z1))
F1_IN(z0, .(z1, z2)) → c5(F565_IN(z0, z2, z1))
F1_IN(z0, .(z1, z2)) → c6(F1_IN(z0, z2))
F117_IN(z0, z1) → c36(F1_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c1(F114_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c2(F1_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c3(F476_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c4(F1_IN(z0, z1))
F1_IN(z0, .(z1, z2)) → c5(F565_IN(z0, z2, z1))
F1_IN(z0, .(z1, z2)) → c6(F1_IN(z0, z2))

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, .(z0, z1)) → f1_out1
f1_in(z0, .(z0, z1)) → U1(f114_in(z0, z1), z0, .(z0, z1))
f1_in(z0, .(z0, z1)) → U2(f1_in(z0, z1), z0, .(z0, z1))
f1_in(z0, .(z0, z1)) → U3(f476_in(z0, z1), z0, .(z0, z1))
f1_in(z0, .(z0, z1)) → U4(f1_in(z0, z1), z0, .(z0, z1))
f1_in(z0, .(z1, z2)) → U5(f565_in(z0, z2, z1), z0, .(z1, z2))
f1_in(z0, .(z1, z2)) → U6(f1_in(z0, z2), z0, .(z1, z2))
U1(f114_out1, z0, .(z0, z1)) → f1_out1
U1(f114_out2(z0), z1, .(z1, z2)) → f1_out1
U1(f114_out5(z0), z1, .(z1, z2)) → f1_out1
U2(f1_out1, z0, .(z0, z1)) → f1_out1
U3(f476_out1, z0, .(z0, z1)) → f1_out1
U3(f476_out2(z0), z1, .(z1, z2)) → f1_out1
U3(f476_out5(z0), z1, .(z1, z2)) → f1_out1
U4(f1_out1, z0, .(z0, z1)) → f1_out1
U5(f565_out1, z0, .(z1, z2)) → f1_out1
U5(f565_out2(z0), z1, .(z2, z3)) → f1_out1
U5(f565_out5(z0), z1, .(z2, z3)) → f1_out1
U6(f1_out1, z0, .(z1, z2)) → f1_out1
f115_in(z0, .(z0, [])) → f115_out1
f115_in(z0, .(z0, [])) → U7(f227_in(z0), z0, .(z0, []))
f115_in(z0, .(z0, z1)) → U8(f324_in(z0, z1), z0, .(z0, z1))
f115_in(z0, .(z1, z2)) → U9(f379_in(z0, z2, z1), z0, .(z1, z2))
U7(f227_out1, z0, .(z0, [])) → f115_out1
U7(f227_out2(z0), z1, .(z1, [])) → f115_out1
U7(f227_out5(z0, z1), z2, .(z2, [])) → f115_out1
U8(f324_out1, z0, .(z0, z1)) → f115_out1
U8(f324_out2(z0), z1, .(z1, z2)) → f115_out1
U8(f324_out5(z0, z1), z2, .(z2, z3)) → f115_out1
U9(f379_out1, z0, .(z1, z2)) → f115_out1
U9(f379_out2(z0), z1, .(z2, z3)) → f115_out1
U9(f379_out5(z0, z1), z2, .(z3, z4)) → f115_out1
f568_in(z0, z1, z2) → U10(f1_in(z0, z1), z0, z1, z2)
U10(f1_out1, z0, z1, z2) → f568_out4(z1)
f480_in(z0, z1) → U11(f1_in(z0, z1), z0, z1)
U11(f1_out1, z0, z1) → f480_out4(z1)
f117_in(z0, z1) → U12(f1_in(z0, z1), z0, z1)
U12(f1_out1, z0, z1) → f117_out4(z1)
f114_in(z0, z1) → U13(f115_in(z0, z1), f117_in(z0, z1), z0, z1)
U13(f115_out1, z0, z1, z2) → f114_out1
U13(z0, f117_out1(z1), z2, z3) → f114_out2(z1)
U13(z0, f117_out4(z1), z2, z3) → f114_out5(z1)
f227_in(z0) → U14(f229_in(z0), f230_in(z0), z0)
U14(f229_out1, z0, z1) → f227_out1
U14(z0, f230_out1(z1), z2) → f227_out2(z1)
U14(z0, f230_out4(z1, z2), z3) → f227_out5(z1, z2)
f324_in(z0, z1) → U15(f115_in(z0, z1), f328_in(z0, z1), z0, z1)
U15(f115_out1, z0, z1, z2) → f324_out1
U15(z0, f328_out1(z1), z2, z3) → f324_out2(z1)
U15(z0, f328_out4(z1, z2), z3, z4) → f324_out5(z1, z2)
f379_in(z0, z1, z2) → U16(f115_in(z0, z1), f382_in(z0, z1, z2), z0, z1, z2)
U16(f115_out1, z0, z1, z2, z3) → f379_out1
U16(z0, f382_out1(z1), z2, z3, z4) → f379_out2(z1)
U16(z0, f382_out4(z1, z2), z3, z4, z5) → f379_out5(z1, z2)
f476_in(z0, z1) → U17(f115_in(z0, z1), f480_in(z0, z1), z0, z1)
U17(f115_out1, z0, z1, z2) → f476_out1
U17(z0, f480_out1(z1), z2, z3) → f476_out2(z1)
U17(z0, f480_out4(z1), z2, z3) → f476_out5(z1)
f565_in(z0, z1, z2) → U18(f115_in(z0, z1), f568_in(z0, z1, z2), z0, z1, z2)
U18(f115_out1, z0, z1, z2, z3) → f565_out1
U18(z0, f568_out1(z1), z2, z3, z4) → f565_out2(z1)
U18(z0, f568_out4(z1), z2, z3, z4) → f565_out5(z1)
Tuples:

F115_IN(z0, .(z0, [])) → c(F227_IN(z0))
F1_IN(z0, .(z0, z1)) → c1(F114_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c2(F1_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c3(F476_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c4(F1_IN(z0, z1))
F1_IN(z0, .(z1, z2)) → c5(F565_IN(z0, z2, z1))
F1_IN(z0, .(z1, z2)) → c6(F1_IN(z0, z2))
F115_IN(z0, .(z0, z1)) → c21(F324_IN(z0, z1))
F115_IN(z0, .(z1, z2)) → c22(F379_IN(z0, z2, z1))
F568_IN(z0, z1, z2) → c32(F1_IN(z0, z1))
F480_IN(z0, z1) → c34(F1_IN(z0, z1))
F117_IN(z0, z1) → c36(F1_IN(z0, z1))
F114_IN(z0, z1) → c38(F115_IN(z0, z1), F117_IN(z0, z1))
F227_IN(z0) → c42
F324_IN(z0, z1) → c46(F115_IN(z0, z1))
F379_IN(z0, z1, z2) → c50(F115_IN(z0, z1))
F476_IN(z0, z1) → c54(F115_IN(z0, z1), F480_IN(z0, z1))
F565_IN(z0, z1, z2) → c58(F115_IN(z0, z1), F568_IN(z0, z1, z2))
F115_IN(z0, .(z0, [])) → c
S tuples:

F115_IN(z0, .(z0, [])) → c(F227_IN(z0))
F115_IN(z0, .(z0, z1)) → c21(F324_IN(z0, z1))
F115_IN(z0, .(z1, z2)) → c22(F379_IN(z0, z2, z1))
F227_IN(z0) → c42
F324_IN(z0, z1) → c46(F115_IN(z0, z1))
F379_IN(z0, z1, z2) → c50(F115_IN(z0, z1))
F115_IN(z0, .(z0, [])) → c
K tuples:

F1_IN(z0, .(z0, z1)) → c1(F114_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c2(F1_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c3(F476_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c4(F1_IN(z0, z1))
F1_IN(z0, .(z1, z2)) → c5(F565_IN(z0, z2, z1))
F1_IN(z0, .(z1, z2)) → c6(F1_IN(z0, z2))
F476_IN(z0, z1) → c54(F115_IN(z0, z1), F480_IN(z0, z1))
F565_IN(z0, z1, z2) → c58(F115_IN(z0, z1), F568_IN(z0, z1, z2))
F568_IN(z0, z1, z2) → c32(F1_IN(z0, z1))
F480_IN(z0, z1) → c34(F1_IN(z0, z1))
F114_IN(z0, z1) → c38(F115_IN(z0, z1), F117_IN(z0, z1))
F117_IN(z0, z1) → c36(F1_IN(z0, z1))
Defined Rule Symbols:

f1_in, U1, U2, U3, U4, U5, U6, f115_in, U7, U8, U9, f568_in, U10, f480_in, U11, f117_in, U12, f114_in, U13, f227_in, U14, f324_in, U15, f379_in, U16, f476_in, U17, f565_in, U18

Defined Pair Symbols:

F115_IN, F1_IN, F568_IN, F480_IN, F117_IN, F114_IN, F227_IN, F324_IN, F379_IN, F476_IN, F565_IN

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c21, c22, c32, c34, c36, c38, c42, c46, c50, c54, c58, 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.

F115_IN(z0, .(z0, [])) → c(F227_IN(z0))
F115_IN(z0, .(z0, [])) → c
We considered the (Usable) Rules:none
And the Tuples:

F115_IN(z0, .(z0, [])) → c(F227_IN(z0))
F1_IN(z0, .(z0, z1)) → c1(F114_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c2(F1_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c3(F476_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c4(F1_IN(z0, z1))
F1_IN(z0, .(z1, z2)) → c5(F565_IN(z0, z2, z1))
F1_IN(z0, .(z1, z2)) → c6(F1_IN(z0, z2))
F115_IN(z0, .(z0, z1)) → c21(F324_IN(z0, z1))
F115_IN(z0, .(z1, z2)) → c22(F379_IN(z0, z2, z1))
F568_IN(z0, z1, z2) → c32(F1_IN(z0, z1))
F480_IN(z0, z1) → c34(F1_IN(z0, z1))
F117_IN(z0, z1) → c36(F1_IN(z0, z1))
F114_IN(z0, z1) → c38(F115_IN(z0, z1), F117_IN(z0, z1))
F227_IN(z0) → c42
F324_IN(z0, z1) → c46(F115_IN(z0, z1))
F379_IN(z0, z1, z2) → c50(F115_IN(z0, z1))
F476_IN(z0, z1) → c54(F115_IN(z0, z1), F480_IN(z0, z1))
F565_IN(z0, z1, z2) → c58(F115_IN(z0, z1), F568_IN(z0, z1, z2))
F115_IN(z0, .(z0, [])) → c
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(.(x1, x2)) = [2] + x2   
POL(F114_IN(x1, x2)) = [2] + x2   
POL(F115_IN(x1, x2)) = [2]   
POL(F117_IN(x1, x2)) = x2   
POL(F1_IN(x1, x2)) = x2   
POL(F227_IN(x1)) = 0   
POL(F324_IN(x1, x2)) = [2]   
POL(F379_IN(x1, x2, x3)) = [2]   
POL(F476_IN(x1, x2)) = [2] + x2   
POL(F480_IN(x1, x2)) = x2   
POL(F565_IN(x1, x2, x3)) = [2] + x2   
POL(F568_IN(x1, x2, x3)) = x2   
POL([]) = 0   
POL(c) = 0   
POL(c(x1)) = x1   
POL(c1(x1)) = x1   
POL(c2(x1)) = x1   
POL(c21(x1)) = x1   
POL(c22(x1)) = x1   
POL(c3(x1)) = x1   
POL(c32(x1)) = x1   
POL(c34(x1)) = x1   
POL(c36(x1)) = x1   
POL(c38(x1, x2)) = x1 + x2   
POL(c4(x1)) = x1   
POL(c42) = 0   
POL(c46(x1)) = x1   
POL(c5(x1)) = x1   
POL(c50(x1)) = x1   
POL(c54(x1, x2)) = x1 + x2   
POL(c58(x1, x2)) = x1 + x2   
POL(c6(x1)) = x1   

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, .(z0, z1)) → f1_out1
f1_in(z0, .(z0, z1)) → U1(f114_in(z0, z1), z0, .(z0, z1))
f1_in(z0, .(z0, z1)) → U2(f1_in(z0, z1), z0, .(z0, z1))
f1_in(z0, .(z0, z1)) → U3(f476_in(z0, z1), z0, .(z0, z1))
f1_in(z0, .(z0, z1)) → U4(f1_in(z0, z1), z0, .(z0, z1))
f1_in(z0, .(z1, z2)) → U5(f565_in(z0, z2, z1), z0, .(z1, z2))
f1_in(z0, .(z1, z2)) → U6(f1_in(z0, z2), z0, .(z1, z2))
U1(f114_out1, z0, .(z0, z1)) → f1_out1
U1(f114_out2(z0), z1, .(z1, z2)) → f1_out1
U1(f114_out5(z0), z1, .(z1, z2)) → f1_out1
U2(f1_out1, z0, .(z0, z1)) → f1_out1
U3(f476_out1, z0, .(z0, z1)) → f1_out1
U3(f476_out2(z0), z1, .(z1, z2)) → f1_out1
U3(f476_out5(z0), z1, .(z1, z2)) → f1_out1
U4(f1_out1, z0, .(z0, z1)) → f1_out1
U5(f565_out1, z0, .(z1, z2)) → f1_out1
U5(f565_out2(z0), z1, .(z2, z3)) → f1_out1
U5(f565_out5(z0), z1, .(z2, z3)) → f1_out1
U6(f1_out1, z0, .(z1, z2)) → f1_out1
f115_in(z0, .(z0, [])) → f115_out1
f115_in(z0, .(z0, [])) → U7(f227_in(z0), z0, .(z0, []))
f115_in(z0, .(z0, z1)) → U8(f324_in(z0, z1), z0, .(z0, z1))
f115_in(z0, .(z1, z2)) → U9(f379_in(z0, z2, z1), z0, .(z1, z2))
U7(f227_out1, z0, .(z0, [])) → f115_out1
U7(f227_out2(z0), z1, .(z1, [])) → f115_out1
U7(f227_out5(z0, z1), z2, .(z2, [])) → f115_out1
U8(f324_out1, z0, .(z0, z1)) → f115_out1
U8(f324_out2(z0), z1, .(z1, z2)) → f115_out1
U8(f324_out5(z0, z1), z2, .(z2, z3)) → f115_out1
U9(f379_out1, z0, .(z1, z2)) → f115_out1
U9(f379_out2(z0), z1, .(z2, z3)) → f115_out1
U9(f379_out5(z0, z1), z2, .(z3, z4)) → f115_out1
f568_in(z0, z1, z2) → U10(f1_in(z0, z1), z0, z1, z2)
U10(f1_out1, z0, z1, z2) → f568_out4(z1)
f480_in(z0, z1) → U11(f1_in(z0, z1), z0, z1)
U11(f1_out1, z0, z1) → f480_out4(z1)
f117_in(z0, z1) → U12(f1_in(z0, z1), z0, z1)
U12(f1_out1, z0, z1) → f117_out4(z1)
f114_in(z0, z1) → U13(f115_in(z0, z1), f117_in(z0, z1), z0, z1)
U13(f115_out1, z0, z1, z2) → f114_out1
U13(z0, f117_out1(z1), z2, z3) → f114_out2(z1)
U13(z0, f117_out4(z1), z2, z3) → f114_out5(z1)
f227_in(z0) → U14(f229_in(z0), f230_in(z0), z0)
U14(f229_out1, z0, z1) → f227_out1
U14(z0, f230_out1(z1), z2) → f227_out2(z1)
U14(z0, f230_out4(z1, z2), z3) → f227_out5(z1, z2)
f324_in(z0, z1) → U15(f115_in(z0, z1), f328_in(z0, z1), z0, z1)
U15(f115_out1, z0, z1, z2) → f324_out1
U15(z0, f328_out1(z1), z2, z3) → f324_out2(z1)
U15(z0, f328_out4(z1, z2), z3, z4) → f324_out5(z1, z2)
f379_in(z0, z1, z2) → U16(f115_in(z0, z1), f382_in(z0, z1, z2), z0, z1, z2)
U16(f115_out1, z0, z1, z2, z3) → f379_out1
U16(z0, f382_out1(z1), z2, z3, z4) → f379_out2(z1)
U16(z0, f382_out4(z1, z2), z3, z4, z5) → f379_out5(z1, z2)
f476_in(z0, z1) → U17(f115_in(z0, z1), f480_in(z0, z1), z0, z1)
U17(f115_out1, z0, z1, z2) → f476_out1
U17(z0, f480_out1(z1), z2, z3) → f476_out2(z1)
U17(z0, f480_out4(z1), z2, z3) → f476_out5(z1)
f565_in(z0, z1, z2) → U18(f115_in(z0, z1), f568_in(z0, z1, z2), z0, z1, z2)
U18(f115_out1, z0, z1, z2, z3) → f565_out1
U18(z0, f568_out1(z1), z2, z3, z4) → f565_out2(z1)
U18(z0, f568_out4(z1), z2, z3, z4) → f565_out5(z1)
Tuples:

F115_IN(z0, .(z0, [])) → c(F227_IN(z0))
F1_IN(z0, .(z0, z1)) → c1(F114_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c2(F1_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c3(F476_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c4(F1_IN(z0, z1))
F1_IN(z0, .(z1, z2)) → c5(F565_IN(z0, z2, z1))
F1_IN(z0, .(z1, z2)) → c6(F1_IN(z0, z2))
F115_IN(z0, .(z0, z1)) → c21(F324_IN(z0, z1))
F115_IN(z0, .(z1, z2)) → c22(F379_IN(z0, z2, z1))
F568_IN(z0, z1, z2) → c32(F1_IN(z0, z1))
F480_IN(z0, z1) → c34(F1_IN(z0, z1))
F117_IN(z0, z1) → c36(F1_IN(z0, z1))
F114_IN(z0, z1) → c38(F115_IN(z0, z1), F117_IN(z0, z1))
F227_IN(z0) → c42
F324_IN(z0, z1) → c46(F115_IN(z0, z1))
F379_IN(z0, z1, z2) → c50(F115_IN(z0, z1))
F476_IN(z0, z1) → c54(F115_IN(z0, z1), F480_IN(z0, z1))
F565_IN(z0, z1, z2) → c58(F115_IN(z0, z1), F568_IN(z0, z1, z2))
F115_IN(z0, .(z0, [])) → c
S tuples:

F115_IN(z0, .(z0, z1)) → c21(F324_IN(z0, z1))
F115_IN(z0, .(z1, z2)) → c22(F379_IN(z0, z2, z1))
F227_IN(z0) → c42
F324_IN(z0, z1) → c46(F115_IN(z0, z1))
F379_IN(z0, z1, z2) → c50(F115_IN(z0, z1))
K tuples:

F1_IN(z0, .(z0, z1)) → c1(F114_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c2(F1_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c3(F476_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c4(F1_IN(z0, z1))
F1_IN(z0, .(z1, z2)) → c5(F565_IN(z0, z2, z1))
F1_IN(z0, .(z1, z2)) → c6(F1_IN(z0, z2))
F476_IN(z0, z1) → c54(F115_IN(z0, z1), F480_IN(z0, z1))
F565_IN(z0, z1, z2) → c58(F115_IN(z0, z1), F568_IN(z0, z1, z2))
F568_IN(z0, z1, z2) → c32(F1_IN(z0, z1))
F480_IN(z0, z1) → c34(F1_IN(z0, z1))
F114_IN(z0, z1) → c38(F115_IN(z0, z1), F117_IN(z0, z1))
F117_IN(z0, z1) → c36(F1_IN(z0, z1))
F115_IN(z0, .(z0, [])) → c(F227_IN(z0))
F115_IN(z0, .(z0, [])) → c
Defined Rule Symbols:

f1_in, U1, U2, U3, U4, U5, U6, f115_in, U7, U8, U9, f568_in, U10, f480_in, U11, f117_in, U12, f114_in, U13, f227_in, U14, f324_in, U15, f379_in, U16, f476_in, U17, f565_in, U18

Defined Pair Symbols:

F115_IN, F1_IN, F568_IN, F480_IN, F117_IN, F114_IN, F227_IN, F324_IN, F379_IN, F476_IN, F565_IN

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c21, c22, c32, c34, c36, c38, c42, c46, c50, c54, c58, c

(13) CdtKnowledgeProof (EQUIVALENT transformation)

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

F227_IN(z0) → c42

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, .(z0, z1)) → f1_out1
f1_in(z0, .(z0, z1)) → U1(f114_in(z0, z1), z0, .(z0, z1))
f1_in(z0, .(z0, z1)) → U2(f1_in(z0, z1), z0, .(z0, z1))
f1_in(z0, .(z0, z1)) → U3(f476_in(z0, z1), z0, .(z0, z1))
f1_in(z0, .(z0, z1)) → U4(f1_in(z0, z1), z0, .(z0, z1))
f1_in(z0, .(z1, z2)) → U5(f565_in(z0, z2, z1), z0, .(z1, z2))
f1_in(z0, .(z1, z2)) → U6(f1_in(z0, z2), z0, .(z1, z2))
U1(f114_out1, z0, .(z0, z1)) → f1_out1
U1(f114_out2(z0), z1, .(z1, z2)) → f1_out1
U1(f114_out5(z0), z1, .(z1, z2)) → f1_out1
U2(f1_out1, z0, .(z0, z1)) → f1_out1
U3(f476_out1, z0, .(z0, z1)) → f1_out1
U3(f476_out2(z0), z1, .(z1, z2)) → f1_out1
U3(f476_out5(z0), z1, .(z1, z2)) → f1_out1
U4(f1_out1, z0, .(z0, z1)) → f1_out1
U5(f565_out1, z0, .(z1, z2)) → f1_out1
U5(f565_out2(z0), z1, .(z2, z3)) → f1_out1
U5(f565_out5(z0), z1, .(z2, z3)) → f1_out1
U6(f1_out1, z0, .(z1, z2)) → f1_out1
f115_in(z0, .(z0, [])) → f115_out1
f115_in(z0, .(z0, [])) → U7(f227_in(z0), z0, .(z0, []))
f115_in(z0, .(z0, z1)) → U8(f324_in(z0, z1), z0, .(z0, z1))
f115_in(z0, .(z1, z2)) → U9(f379_in(z0, z2, z1), z0, .(z1, z2))
U7(f227_out1, z0, .(z0, [])) → f115_out1
U7(f227_out2(z0), z1, .(z1, [])) → f115_out1
U7(f227_out5(z0, z1), z2, .(z2, [])) → f115_out1
U8(f324_out1, z0, .(z0, z1)) → f115_out1
U8(f324_out2(z0), z1, .(z1, z2)) → f115_out1
U8(f324_out5(z0, z1), z2, .(z2, z3)) → f115_out1
U9(f379_out1, z0, .(z1, z2)) → f115_out1
U9(f379_out2(z0), z1, .(z2, z3)) → f115_out1
U9(f379_out5(z0, z1), z2, .(z3, z4)) → f115_out1
f568_in(z0, z1, z2) → U10(f1_in(z0, z1), z0, z1, z2)
U10(f1_out1, z0, z1, z2) → f568_out4(z1)
f480_in(z0, z1) → U11(f1_in(z0, z1), z0, z1)
U11(f1_out1, z0, z1) → f480_out4(z1)
f117_in(z0, z1) → U12(f1_in(z0, z1), z0, z1)
U12(f1_out1, z0, z1) → f117_out4(z1)
f114_in(z0, z1) → U13(f115_in(z0, z1), f117_in(z0, z1), z0, z1)
U13(f115_out1, z0, z1, z2) → f114_out1
U13(z0, f117_out1(z1), z2, z3) → f114_out2(z1)
U13(z0, f117_out4(z1), z2, z3) → f114_out5(z1)
f227_in(z0) → U14(f229_in(z0), f230_in(z0), z0)
U14(f229_out1, z0, z1) → f227_out1
U14(z0, f230_out1(z1), z2) → f227_out2(z1)
U14(z0, f230_out4(z1, z2), z3) → f227_out5(z1, z2)
f324_in(z0, z1) → U15(f115_in(z0, z1), f328_in(z0, z1), z0, z1)
U15(f115_out1, z0, z1, z2) → f324_out1
U15(z0, f328_out1(z1), z2, z3) → f324_out2(z1)
U15(z0, f328_out4(z1, z2), z3, z4) → f324_out5(z1, z2)
f379_in(z0, z1, z2) → U16(f115_in(z0, z1), f382_in(z0, z1, z2), z0, z1, z2)
U16(f115_out1, z0, z1, z2, z3) → f379_out1
U16(z0, f382_out1(z1), z2, z3, z4) → f379_out2(z1)
U16(z0, f382_out4(z1, z2), z3, z4, z5) → f379_out5(z1, z2)
f476_in(z0, z1) → U17(f115_in(z0, z1), f480_in(z0, z1), z0, z1)
U17(f115_out1, z0, z1, z2) → f476_out1
U17(z0, f480_out1(z1), z2, z3) → f476_out2(z1)
U17(z0, f480_out4(z1), z2, z3) → f476_out5(z1)
f565_in(z0, z1, z2) → U18(f115_in(z0, z1), f568_in(z0, z1, z2), z0, z1, z2)
U18(f115_out1, z0, z1, z2, z3) → f565_out1
U18(z0, f568_out1(z1), z2, z3, z4) → f565_out2(z1)
U18(z0, f568_out4(z1), z2, z3, z4) → f565_out5(z1)
Tuples:

F115_IN(z0, .(z0, [])) → c(F227_IN(z0))
F1_IN(z0, .(z0, z1)) → c1(F114_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c2(F1_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c3(F476_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c4(F1_IN(z0, z1))
F1_IN(z0, .(z1, z2)) → c5(F565_IN(z0, z2, z1))
F1_IN(z0, .(z1, z2)) → c6(F1_IN(z0, z2))
F115_IN(z0, .(z0, z1)) → c21(F324_IN(z0, z1))
F115_IN(z0, .(z1, z2)) → c22(F379_IN(z0, z2, z1))
F568_IN(z0, z1, z2) → c32(F1_IN(z0, z1))
F480_IN(z0, z1) → c34(F1_IN(z0, z1))
F117_IN(z0, z1) → c36(F1_IN(z0, z1))
F114_IN(z0, z1) → c38(F115_IN(z0, z1), F117_IN(z0, z1))
F227_IN(z0) → c42
F324_IN(z0, z1) → c46(F115_IN(z0, z1))
F379_IN(z0, z1, z2) → c50(F115_IN(z0, z1))
F476_IN(z0, z1) → c54(F115_IN(z0, z1), F480_IN(z0, z1))
F565_IN(z0, z1, z2) → c58(F115_IN(z0, z1), F568_IN(z0, z1, z2))
F115_IN(z0, .(z0, [])) → c
S tuples:

F115_IN(z0, .(z0, z1)) → c21(F324_IN(z0, z1))
F115_IN(z0, .(z1, z2)) → c22(F379_IN(z0, z2, z1))
F324_IN(z0, z1) → c46(F115_IN(z0, z1))
F379_IN(z0, z1, z2) → c50(F115_IN(z0, z1))
K tuples:

F1_IN(z0, .(z0, z1)) → c1(F114_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c2(F1_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c3(F476_IN(z0, z1))
F1_IN(z0, .(z0, z1)) → c4(F1_IN(z0, z1))
F1_IN(z0, .(z1, z2)) → c5(F565_IN(z0, z2, z1))
F1_IN(z0, .(z1, z2)) → c6(F1_IN(z0, z2))
F476_IN(z0, z1) → c54(F115_IN(z0, z1), F480_IN(z0, z1))
F565_IN(z0, z1, z2) → c58(F115_IN(z0, z1), F568_IN(z0, z1, z2))
F568_IN(z0, z1, z2) → c32(F1_IN(z0, z1))
F480_IN(z0, z1) → c34(F1_IN(z0, z1))
F114_IN(z0, z1) → c38(F115_IN(z0, z1), F117_IN(z0, z1))
F117_IN(z0, z1) → c36(F1_IN(z0, z1))
F115_IN(z0, .(z0, [])) → c(F227_IN(z0))
F115_IN(z0, .(z0, [])) → c
F227_IN(z0) → c42
Defined Rule Symbols:

f1_in, U1, U2, U3, U4, U5, U6, f115_in, U7, U8, U9, f568_in, U10, f480_in, U11, f117_in, U12, f114_in, U13, f227_in, U14, f324_in, U15, f379_in, U16, f476_in, U17, f565_in, U18

Defined Pair Symbols:

F115_IN, F1_IN, F568_IN, F480_IN, F117_IN, F114_IN, F227_IN, F324_IN, F379_IN, F476_IN, F565_IN

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c21, c22, c32, c34, c36, c38, c42, c46, c50, c54, c58, c

(15) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)

Built complexity over-approximating cdt problems from derivation graph.

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, .(z0, z1)) → f2_out1
f2_in(z0, .(z0, z1)) → U1(f113_in(z0, z1), z0, .(z0, z1))
f2_in(z0, .(z0, z1)) → U2(f2_in(z0, z1), z0, .(z0, z1))
f2_in(z0, .(z0, z1)) → U3(f475_in(z0, z1), z0, .(z0, z1))
f2_in(z0, .(z0, z1)) → U4(f2_in(z0, z1), z0, .(z0, z1))
f2_in(z0, .(z1, z2)) → U5(f562_in(z0, z2, z1), z0, .(z1, z2))
f2_in(z0, .(z1, z2)) → U6(f2_in(z0, z2), z0, .(z1, z2))
U1(f113_out1, z0, .(z0, z1)) → f2_out1
U1(f113_out2(z0), z1, .(z1, z2)) → f2_out1
U1(f113_out5(z0), z1, .(z1, z2)) → f2_out1
U2(f2_out1, z0, .(z0, z1)) → f2_out1
U3(f475_out1, z0, .(z0, z1)) → f2_out1
U3(f475_out2(z0), z1, .(z1, z2)) → f2_out1
U3(f475_out5(z0), z1, .(z1, z2)) → f2_out1
U4(f2_out1, z0, .(z0, z1)) → f2_out1
U5(f562_out1, z0, .(z1, z2)) → f2_out1
U5(f562_out2(z0), z1, .(z2, z3)) → f2_out1
U5(f562_out5(z0), z1, .(z2, z3)) → f2_out1
U6(f2_out1, z0, .(z1, z2)) → f2_out1
f116_in(z0, .(z0, [])) → f116_out1
f116_in(z0, .(z0, [])) → U7(f228_in(z0), z0, .(z0, []))
f116_in(z0, .(z0, z1)) → U8(f323_in(z0, z1), z0, .(z0, z1))
f116_in(z0, .(z1, z2)) → U9(f380_in(z0, z2, z1), z0, .(z1, z2))
U7(f228_out1, z0, .(z0, [])) → f116_out1
U7(f228_out2(z0), z1, .(z1, [])) → f116_out1
U7(f228_out5(z0, z1), z2, .(z2, [])) → f116_out1
U8(f323_out1, z0, .(z0, z1)) → f116_out1
U8(f323_out2(z0), z1, .(z1, z2)) → f116_out1
U8(f323_out5(z0, z1), z2, .(z2, z3)) → f116_out1
U9(f380_out1, z0, .(z1, z2)) → f116_out1
U9(f380_out2(z0), z1, .(z2, z3)) → f116_out1
U9(f380_out5(z0, z1), z2, .(z3, z4)) → f116_out1
f566_in(z0, z1, z2) → U10(f2_in(z0, z1), z0, z1, z2)
U10(f2_out1, z0, z1, z2) → f566_out4(z1)
f478_in(z0, z1) → U11(f2_in(z0, z1), z0, z1)
U11(f2_out1, z0, z1) → f478_out4(z1)
f118_in(z0, z1) → U12(f2_in(z0, z1), z0, z1)
U12(f2_out1, z0, z1) → f118_out4(z1)
f113_in(z0, z1) → U13(f116_in(z0, z1), f118_in(z0, z1), z0, z1)
U13(f116_out1, z0, z1, z2) → f113_out1
U13(z0, f118_out1(z1), z2, z3) → f113_out2(z1)
U13(z0, f118_out4(z1), z2, z3) → f113_out5(z1)
f228_in(z0) → U14(f231_in(z0), f232_in(z0), z0)
U14(f231_out1, z0, z1) → f228_out1
U14(z0, f232_out1(z1), z2) → f228_out2(z1)
U14(z0, f232_out4(z1, z2), z3) → f228_out5(z1, z2)
f323_in(z0, z1) → U15(f116_in(z0, z1), f326_in(z0, z1), z0, z1)
U15(f116_out1, z0, z1, z2) → f323_out1
U15(z0, f326_out1(z1), z2, z3) → f323_out2(z1)
U15(z0, f326_out4(z1, z2), z3, z4) → f323_out5(z1, z2)
f380_in(z0, z1, z2) → U16(f116_in(z0, z1), f384_in(z0, z1, z2), z0, z1, z2)
U16(f116_out1, z0, z1, z2, z3) → f380_out1
U16(z0, f384_out1(z1), z2, z3, z4) → f380_out2(z1)
U16(z0, f384_out4(z1, z2), z3, z4, z5) → f380_out5(z1, z2)
f475_in(z0, z1) → U17(f116_in(z0, z1), f478_in(z0, z1), z0, z1)
U17(f116_out1, z0, z1, z2) → f475_out1
U17(z0, f478_out1(z1), z2, z3) → f475_out2(z1)
U17(z0, f478_out4(z1), z2, z3) → f475_out5(z1)
f562_in(z0, z1, z2) → U18(f116_in(z0, z1), f566_in(z0, z1, z2), z0, z1, z2)
U18(f116_out1, z0, z1, z2, z3) → f562_out1
U18(z0, f566_out1(z1), z2, z3, z4) → f562_out2(z1)
U18(z0, f566_out4(z1), z2, z3, z4) → f562_out5(z1)
Tuples:

F2_IN(z0, .(z0, z1)) → c1(U1'(f113_in(z0, z1), z0, .(z0, z1)), F113_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c2(U2'(f2_in(z0, z1), z0, .(z0, z1)), F2_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c3(U3'(f475_in(z0, z1), z0, .(z0, z1)), F475_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c4(U4'(f2_in(z0, z1), z0, .(z0, z1)), F2_IN(z0, z1))
F2_IN(z0, .(z1, z2)) → c5(U5'(f562_in(z0, z2, z1), z0, .(z1, z2)), F562_IN(z0, z2, z1))
F2_IN(z0, .(z1, z2)) → c6(U6'(f2_in(z0, z2), z0, .(z1, z2)), F2_IN(z0, z2))
F116_IN(z0, .(z0, [])) → c20(U7'(f228_in(z0), z0, .(z0, [])), F228_IN(z0))
F116_IN(z0, .(z0, z1)) → c21(U8'(f323_in(z0, z1), z0, .(z0, z1)), F323_IN(z0, z1))
F116_IN(z0, .(z1, z2)) → c22(U9'(f380_in(z0, z2, z1), z0, .(z1, z2)), F380_IN(z0, z2, z1))
F566_IN(z0, z1, z2) → c32(U10'(f2_in(z0, z1), z0, z1, z2), F2_IN(z0, z1))
F478_IN(z0, z1) → c34(U11'(f2_in(z0, z1), z0, z1), F2_IN(z0, z1))
F118_IN(z0, z1) → c36(U12'(f2_in(z0, z1), z0, z1), F2_IN(z0, z1))
F113_IN(z0, z1) → c38(U13'(f116_in(z0, z1), f118_in(z0, z1), z0, z1), F116_IN(z0, z1), F118_IN(z0, z1))
F228_IN(z0) → c42(U14'(f231_in(z0), f232_in(z0), z0))
F323_IN(z0, z1) → c46(U15'(f116_in(z0, z1), f326_in(z0, z1), z0, z1), F116_IN(z0, z1))
F380_IN(z0, z1, z2) → c50(U16'(f116_in(z0, z1), f384_in(z0, z1, z2), z0, z1, z2), F116_IN(z0, z1))
F475_IN(z0, z1) → c54(U17'(f116_in(z0, z1), f478_in(z0, z1), z0, z1), F116_IN(z0, z1), F478_IN(z0, z1))
F562_IN(z0, z1, z2) → c58(U18'(f116_in(z0, z1), f566_in(z0, z1, z2), z0, z1, z2), F116_IN(z0, z1), F566_IN(z0, z1, z2))
S tuples:

F2_IN(z0, .(z0, z1)) → c1(U1'(f113_in(z0, z1), z0, .(z0, z1)), F113_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c2(U2'(f2_in(z0, z1), z0, .(z0, z1)), F2_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c3(U3'(f475_in(z0, z1), z0, .(z0, z1)), F475_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c4(U4'(f2_in(z0, z1), z0, .(z0, z1)), F2_IN(z0, z1))
F2_IN(z0, .(z1, z2)) → c5(U5'(f562_in(z0, z2, z1), z0, .(z1, z2)), F562_IN(z0, z2, z1))
F2_IN(z0, .(z1, z2)) → c6(U6'(f2_in(z0, z2), z0, .(z1, z2)), F2_IN(z0, z2))
F116_IN(z0, .(z0, [])) → c20(U7'(f228_in(z0), z0, .(z0, [])), F228_IN(z0))
F116_IN(z0, .(z0, z1)) → c21(U8'(f323_in(z0, z1), z0, .(z0, z1)), F323_IN(z0, z1))
F116_IN(z0, .(z1, z2)) → c22(U9'(f380_in(z0, z2, z1), z0, .(z1, z2)), F380_IN(z0, z2, z1))
F566_IN(z0, z1, z2) → c32(U10'(f2_in(z0, z1), z0, z1, z2), F2_IN(z0, z1))
F478_IN(z0, z1) → c34(U11'(f2_in(z0, z1), z0, z1), F2_IN(z0, z1))
F118_IN(z0, z1) → c36(U12'(f2_in(z0, z1), z0, z1), F2_IN(z0, z1))
F113_IN(z0, z1) → c38(U13'(f116_in(z0, z1), f118_in(z0, z1), z0, z1), F116_IN(z0, z1), F118_IN(z0, z1))
F228_IN(z0) → c42(U14'(f231_in(z0), f232_in(z0), z0))
F323_IN(z0, z1) → c46(U15'(f116_in(z0, z1), f326_in(z0, z1), z0, z1), F116_IN(z0, z1))
F380_IN(z0, z1, z2) → c50(U16'(f116_in(z0, z1), f384_in(z0, z1, z2), z0, z1, z2), F116_IN(z0, z1))
F475_IN(z0, z1) → c54(U17'(f116_in(z0, z1), f478_in(z0, z1), z0, z1), F116_IN(z0, z1), F478_IN(z0, z1))
F562_IN(z0, z1, z2) → c58(U18'(f116_in(z0, z1), f566_in(z0, z1, z2), z0, z1, z2), F116_IN(z0, z1), F566_IN(z0, z1, z2))
K tuples:none
Defined Rule Symbols:

f2_in, U1, U2, U3, U4, U5, U6, f116_in, U7, U8, U9, f566_in, U10, f478_in, U11, f118_in, U12, f113_in, U13, f228_in, U14, f323_in, U15, f380_in, U16, f475_in, U17, f562_in, U18

Defined Pair Symbols:

F2_IN, F116_IN, F566_IN, F478_IN, F118_IN, F113_IN, F228_IN, F323_IN, F380_IN, F475_IN, F562_IN

Compound Symbols:

c1, c2, c3, c4, c5, c6, c20, c21, c22, c32, c34, c36, c38, c42, c46, c50, c54, c58

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

Split RHS of tuples not part of any SCC

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, .(z0, z1)) → f2_out1
f2_in(z0, .(z0, z1)) → U1(f113_in(z0, z1), z0, .(z0, z1))
f2_in(z0, .(z0, z1)) → U2(f2_in(z0, z1), z0, .(z0, z1))
f2_in(z0, .(z0, z1)) → U3(f475_in(z0, z1), z0, .(z0, z1))
f2_in(z0, .(z0, z1)) → U4(f2_in(z0, z1), z0, .(z0, z1))
f2_in(z0, .(z1, z2)) → U5(f562_in(z0, z2, z1), z0, .(z1, z2))
f2_in(z0, .(z1, z2)) → U6(f2_in(z0, z2), z0, .(z1, z2))
U1(f113_out1, z0, .(z0, z1)) → f2_out1
U1(f113_out2(z0), z1, .(z1, z2)) → f2_out1
U1(f113_out5(z0), z1, .(z1, z2)) → f2_out1
U2(f2_out1, z0, .(z0, z1)) → f2_out1
U3(f475_out1, z0, .(z0, z1)) → f2_out1
U3(f475_out2(z0), z1, .(z1, z2)) → f2_out1
U3(f475_out5(z0), z1, .(z1, z2)) → f2_out1
U4(f2_out1, z0, .(z0, z1)) → f2_out1
U5(f562_out1, z0, .(z1, z2)) → f2_out1
U5(f562_out2(z0), z1, .(z2, z3)) → f2_out1
U5(f562_out5(z0), z1, .(z2, z3)) → f2_out1
U6(f2_out1, z0, .(z1, z2)) → f2_out1
f116_in(z0, .(z0, [])) → f116_out1
f116_in(z0, .(z0, [])) → U7(f228_in(z0), z0, .(z0, []))
f116_in(z0, .(z0, z1)) → U8(f323_in(z0, z1), z0, .(z0, z1))
f116_in(z0, .(z1, z2)) → U9(f380_in(z0, z2, z1), z0, .(z1, z2))
U7(f228_out1, z0, .(z0, [])) → f116_out1
U7(f228_out2(z0), z1, .(z1, [])) → f116_out1
U7(f228_out5(z0, z1), z2, .(z2, [])) → f116_out1
U8(f323_out1, z0, .(z0, z1)) → f116_out1
U8(f323_out2(z0), z1, .(z1, z2)) → f116_out1
U8(f323_out5(z0, z1), z2, .(z2, z3)) → f116_out1
U9(f380_out1, z0, .(z1, z2)) → f116_out1
U9(f380_out2(z0), z1, .(z2, z3)) → f116_out1
U9(f380_out5(z0, z1), z2, .(z3, z4)) → f116_out1
f566_in(z0, z1, z2) → U10(f2_in(z0, z1), z0, z1, z2)
U10(f2_out1, z0, z1, z2) → f566_out4(z1)
f478_in(z0, z1) → U11(f2_in(z0, z1), z0, z1)
U11(f2_out1, z0, z1) → f478_out4(z1)
f118_in(z0, z1) → U12(f2_in(z0, z1), z0, z1)
U12(f2_out1, z0, z1) → f118_out4(z1)
f113_in(z0, z1) → U13(f116_in(z0, z1), f118_in(z0, z1), z0, z1)
U13(f116_out1, z0, z1, z2) → f113_out1
U13(z0, f118_out1(z1), z2, z3) → f113_out2(z1)
U13(z0, f118_out4(z1), z2, z3) → f113_out5(z1)
f228_in(z0) → U14(f231_in(z0), f232_in(z0), z0)
U14(f231_out1, z0, z1) → f228_out1
U14(z0, f232_out1(z1), z2) → f228_out2(z1)
U14(z0, f232_out4(z1, z2), z3) → f228_out5(z1, z2)
f323_in(z0, z1) → U15(f116_in(z0, z1), f326_in(z0, z1), z0, z1)
U15(f116_out1, z0, z1, z2) → f323_out1
U15(z0, f326_out1(z1), z2, z3) → f323_out2(z1)
U15(z0, f326_out4(z1, z2), z3, z4) → f323_out5(z1, z2)
f380_in(z0, z1, z2) → U16(f116_in(z0, z1), f384_in(z0, z1, z2), z0, z1, z2)
U16(f116_out1, z0, z1, z2, z3) → f380_out1
U16(z0, f384_out1(z1), z2, z3, z4) → f380_out2(z1)
U16(z0, f384_out4(z1, z2), z3, z4, z5) → f380_out5(z1, z2)
f475_in(z0, z1) → U17(f116_in(z0, z1), f478_in(z0, z1), z0, z1)
U17(f116_out1, z0, z1, z2) → f475_out1
U17(z0, f478_out1(z1), z2, z3) → f475_out2(z1)
U17(z0, f478_out4(z1), z2, z3) → f475_out5(z1)
f562_in(z0, z1, z2) → U18(f116_in(z0, z1), f566_in(z0, z1, z2), z0, z1, z2)
U18(f116_out1, z0, z1, z2, z3) → f562_out1
U18(z0, f566_out1(z1), z2, z3, z4) → f562_out2(z1)
U18(z0, f566_out4(z1), z2, z3, z4) → f562_out5(z1)
Tuples:

F2_IN(z0, .(z0, z1)) → c1(U1'(f113_in(z0, z1), z0, .(z0, z1)), F113_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c2(U2'(f2_in(z0, z1), z0, .(z0, z1)), F2_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c3(U3'(f475_in(z0, z1), z0, .(z0, z1)), F475_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c4(U4'(f2_in(z0, z1), z0, .(z0, z1)), F2_IN(z0, z1))
F2_IN(z0, .(z1, z2)) → c5(U5'(f562_in(z0, z2, z1), z0, .(z1, z2)), F562_IN(z0, z2, z1))
F2_IN(z0, .(z1, z2)) → c6(U6'(f2_in(z0, z2), z0, .(z1, z2)), F2_IN(z0, z2))
F116_IN(z0, .(z0, z1)) → c21(U8'(f323_in(z0, z1), z0, .(z0, z1)), F323_IN(z0, z1))
F116_IN(z0, .(z1, z2)) → c22(U9'(f380_in(z0, z2, z1), z0, .(z1, z2)), F380_IN(z0, z2, z1))
F566_IN(z0, z1, z2) → c32(U10'(f2_in(z0, z1), z0, z1, z2), F2_IN(z0, z1))
F478_IN(z0, z1) → c34(U11'(f2_in(z0, z1), z0, z1), F2_IN(z0, z1))
F118_IN(z0, z1) → c36(U12'(f2_in(z0, z1), z0, z1), F2_IN(z0, z1))
F113_IN(z0, z1) → c38(U13'(f116_in(z0, z1), f118_in(z0, z1), z0, z1), F116_IN(z0, z1), F118_IN(z0, z1))
F228_IN(z0) → c42(U14'(f231_in(z0), f232_in(z0), z0))
F323_IN(z0, z1) → c46(U15'(f116_in(z0, z1), f326_in(z0, z1), z0, z1), F116_IN(z0, z1))
F380_IN(z0, z1, z2) → c50(U16'(f116_in(z0, z1), f384_in(z0, z1, z2), z0, z1, z2), F116_IN(z0, z1))
F475_IN(z0, z1) → c54(U17'(f116_in(z0, z1), f478_in(z0, z1), z0, z1), F116_IN(z0, z1), F478_IN(z0, z1))
F562_IN(z0, z1, z2) → c58(U18'(f116_in(z0, z1), f566_in(z0, z1, z2), z0, z1, z2), F116_IN(z0, z1), F566_IN(z0, z1, z2))
F116_IN(z0, .(z0, [])) → c(U7'(f228_in(z0), z0, .(z0, [])))
F116_IN(z0, .(z0, [])) → c(F228_IN(z0))
S tuples:

F2_IN(z0, .(z0, z1)) → c1(U1'(f113_in(z0, z1), z0, .(z0, z1)), F113_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c2(U2'(f2_in(z0, z1), z0, .(z0, z1)), F2_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c3(U3'(f475_in(z0, z1), z0, .(z0, z1)), F475_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c4(U4'(f2_in(z0, z1), z0, .(z0, z1)), F2_IN(z0, z1))
F2_IN(z0, .(z1, z2)) → c5(U5'(f562_in(z0, z2, z1), z0, .(z1, z2)), F562_IN(z0, z2, z1))
F2_IN(z0, .(z1, z2)) → c6(U6'(f2_in(z0, z2), z0, .(z1, z2)), F2_IN(z0, z2))
F116_IN(z0, .(z0, z1)) → c21(U8'(f323_in(z0, z1), z0, .(z0, z1)), F323_IN(z0, z1))
F116_IN(z0, .(z1, z2)) → c22(U9'(f380_in(z0, z2, z1), z0, .(z1, z2)), F380_IN(z0, z2, z1))
F566_IN(z0, z1, z2) → c32(U10'(f2_in(z0, z1), z0, z1, z2), F2_IN(z0, z1))
F478_IN(z0, z1) → c34(U11'(f2_in(z0, z1), z0, z1), F2_IN(z0, z1))
F118_IN(z0, z1) → c36(U12'(f2_in(z0, z1), z0, z1), F2_IN(z0, z1))
F113_IN(z0, z1) → c38(U13'(f116_in(z0, z1), f118_in(z0, z1), z0, z1), F116_IN(z0, z1), F118_IN(z0, z1))
F228_IN(z0) → c42(U14'(f231_in(z0), f232_in(z0), z0))
F323_IN(z0, z1) → c46(U15'(f116_in(z0, z1), f326_in(z0, z1), z0, z1), F116_IN(z0, z1))
F380_IN(z0, z1, z2) → c50(U16'(f116_in(z0, z1), f384_in(z0, z1, z2), z0, z1, z2), F116_IN(z0, z1))
F475_IN(z0, z1) → c54(U17'(f116_in(z0, z1), f478_in(z0, z1), z0, z1), F116_IN(z0, z1), F478_IN(z0, z1))
F562_IN(z0, z1, z2) → c58(U18'(f116_in(z0, z1), f566_in(z0, z1, z2), z0, z1, z2), F116_IN(z0, z1), F566_IN(z0, z1, z2))
F116_IN(z0, .(z0, [])) → c(U7'(f228_in(z0), z0, .(z0, [])))
F116_IN(z0, .(z0, [])) → c(F228_IN(z0))
K tuples:none
Defined Rule Symbols:

f2_in, U1, U2, U3, U4, U5, U6, f116_in, U7, U8, U9, f566_in, U10, f478_in, U11, f118_in, U12, f113_in, U13, f228_in, U14, f323_in, U15, f380_in, U16, f475_in, U17, f562_in, U18

Defined Pair Symbols:

F2_IN, F116_IN, F566_IN, F478_IN, F118_IN, F113_IN, F228_IN, F323_IN, F380_IN, F475_IN, F562_IN

Compound Symbols:

c1, c2, c3, c4, c5, c6, c21, c22, c32, c34, c36, c38, c42, c46, c50, c54, c58, c

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

Removed 18 trailing tuple parts

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, .(z0, z1)) → f2_out1
f2_in(z0, .(z0, z1)) → U1(f113_in(z0, z1), z0, .(z0, z1))
f2_in(z0, .(z0, z1)) → U2(f2_in(z0, z1), z0, .(z0, z1))
f2_in(z0, .(z0, z1)) → U3(f475_in(z0, z1), z0, .(z0, z1))
f2_in(z0, .(z0, z1)) → U4(f2_in(z0, z1), z0, .(z0, z1))
f2_in(z0, .(z1, z2)) → U5(f562_in(z0, z2, z1), z0, .(z1, z2))
f2_in(z0, .(z1, z2)) → U6(f2_in(z0, z2), z0, .(z1, z2))
U1(f113_out1, z0, .(z0, z1)) → f2_out1
U1(f113_out2(z0), z1, .(z1, z2)) → f2_out1
U1(f113_out5(z0), z1, .(z1, z2)) → f2_out1
U2(f2_out1, z0, .(z0, z1)) → f2_out1
U3(f475_out1, z0, .(z0, z1)) → f2_out1
U3(f475_out2(z0), z1, .(z1, z2)) → f2_out1
U3(f475_out5(z0), z1, .(z1, z2)) → f2_out1
U4(f2_out1, z0, .(z0, z1)) → f2_out1
U5(f562_out1, z0, .(z1, z2)) → f2_out1
U5(f562_out2(z0), z1, .(z2, z3)) → f2_out1
U5(f562_out5(z0), z1, .(z2, z3)) → f2_out1
U6(f2_out1, z0, .(z1, z2)) → f2_out1
f116_in(z0, .(z0, [])) → f116_out1
f116_in(z0, .(z0, [])) → U7(f228_in(z0), z0, .(z0, []))
f116_in(z0, .(z0, z1)) → U8(f323_in(z0, z1), z0, .(z0, z1))
f116_in(z0, .(z1, z2)) → U9(f380_in(z0, z2, z1), z0, .(z1, z2))
U7(f228_out1, z0, .(z0, [])) → f116_out1
U7(f228_out2(z0), z1, .(z1, [])) → f116_out1
U7(f228_out5(z0, z1), z2, .(z2, [])) → f116_out1
U8(f323_out1, z0, .(z0, z1)) → f116_out1
U8(f323_out2(z0), z1, .(z1, z2)) → f116_out1
U8(f323_out5(z0, z1), z2, .(z2, z3)) → f116_out1
U9(f380_out1, z0, .(z1, z2)) → f116_out1
U9(f380_out2(z0), z1, .(z2, z3)) → f116_out1
U9(f380_out5(z0, z1), z2, .(z3, z4)) → f116_out1
f566_in(z0, z1, z2) → U10(f2_in(z0, z1), z0, z1, z2)
U10(f2_out1, z0, z1, z2) → f566_out4(z1)
f478_in(z0, z1) → U11(f2_in(z0, z1), z0, z1)
U11(f2_out1, z0, z1) → f478_out4(z1)
f118_in(z0, z1) → U12(f2_in(z0, z1), z0, z1)
U12(f2_out1, z0, z1) → f118_out4(z1)
f113_in(z0, z1) → U13(f116_in(z0, z1), f118_in(z0, z1), z0, z1)
U13(f116_out1, z0, z1, z2) → f113_out1
U13(z0, f118_out1(z1), z2, z3) → f113_out2(z1)
U13(z0, f118_out4(z1), z2, z3) → f113_out5(z1)
f228_in(z0) → U14(f231_in(z0), f232_in(z0), z0)
U14(f231_out1, z0, z1) → f228_out1
U14(z0, f232_out1(z1), z2) → f228_out2(z1)
U14(z0, f232_out4(z1, z2), z3) → f228_out5(z1, z2)
f323_in(z0, z1) → U15(f116_in(z0, z1), f326_in(z0, z1), z0, z1)
U15(f116_out1, z0, z1, z2) → f323_out1
U15(z0, f326_out1(z1), z2, z3) → f323_out2(z1)
U15(z0, f326_out4(z1, z2), z3, z4) → f323_out5(z1, z2)
f380_in(z0, z1, z2) → U16(f116_in(z0, z1), f384_in(z0, z1, z2), z0, z1, z2)
U16(f116_out1, z0, z1, z2, z3) → f380_out1
U16(z0, f384_out1(z1), z2, z3, z4) → f380_out2(z1)
U16(z0, f384_out4(z1, z2), z3, z4, z5) → f380_out5(z1, z2)
f475_in(z0, z1) → U17(f116_in(z0, z1), f478_in(z0, z1), z0, z1)
U17(f116_out1, z0, z1, z2) → f475_out1
U17(z0, f478_out1(z1), z2, z3) → f475_out2(z1)
U17(z0, f478_out4(z1), z2, z3) → f475_out5(z1)
f562_in(z0, z1, z2) → U18(f116_in(z0, z1), f566_in(z0, z1, z2), z0, z1, z2)
U18(f116_out1, z0, z1, z2, z3) → f562_out1
U18(z0, f566_out1(z1), z2, z3, z4) → f562_out2(z1)
U18(z0, f566_out4(z1), z2, z3, z4) → f562_out5(z1)
Tuples:

F116_IN(z0, .(z0, [])) → c(F228_IN(z0))
F2_IN(z0, .(z0, z1)) → c1(F113_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c2(F2_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c3(F475_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c4(F2_IN(z0, z1))
F2_IN(z0, .(z1, z2)) → c5(F562_IN(z0, z2, z1))
F2_IN(z0, .(z1, z2)) → c6(F2_IN(z0, z2))
F116_IN(z0, .(z0, z1)) → c21(F323_IN(z0, z1))
F116_IN(z0, .(z1, z2)) → c22(F380_IN(z0, z2, z1))
F566_IN(z0, z1, z2) → c32(F2_IN(z0, z1))
F478_IN(z0, z1) → c34(F2_IN(z0, z1))
F118_IN(z0, z1) → c36(F2_IN(z0, z1))
F113_IN(z0, z1) → c38(F116_IN(z0, z1), F118_IN(z0, z1))
F228_IN(z0) → c42
F323_IN(z0, z1) → c46(F116_IN(z0, z1))
F380_IN(z0, z1, z2) → c50(F116_IN(z0, z1))
F475_IN(z0, z1) → c54(F116_IN(z0, z1), F478_IN(z0, z1))
F562_IN(z0, z1, z2) → c58(F116_IN(z0, z1), F566_IN(z0, z1, z2))
F116_IN(z0, .(z0, [])) → c
S tuples:

F116_IN(z0, .(z0, [])) → c(F228_IN(z0))
F2_IN(z0, .(z0, z1)) → c1(F113_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c2(F2_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c3(F475_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c4(F2_IN(z0, z1))
F2_IN(z0, .(z1, z2)) → c5(F562_IN(z0, z2, z1))
F2_IN(z0, .(z1, z2)) → c6(F2_IN(z0, z2))
F116_IN(z0, .(z0, z1)) → c21(F323_IN(z0, z1))
F116_IN(z0, .(z1, z2)) → c22(F380_IN(z0, z2, z1))
F566_IN(z0, z1, z2) → c32(F2_IN(z0, z1))
F478_IN(z0, z1) → c34(F2_IN(z0, z1))
F118_IN(z0, z1) → c36(F2_IN(z0, z1))
F113_IN(z0, z1) → c38(F116_IN(z0, z1), F118_IN(z0, z1))
F228_IN(z0) → c42
F323_IN(z0, z1) → c46(F116_IN(z0, z1))
F380_IN(z0, z1, z2) → c50(F116_IN(z0, z1))
F475_IN(z0, z1) → c54(F116_IN(z0, z1), F478_IN(z0, z1))
F562_IN(z0, z1, z2) → c58(F116_IN(z0, z1), F566_IN(z0, z1, z2))
F116_IN(z0, .(z0, [])) → c
K tuples:none
Defined Rule Symbols:

f2_in, U1, U2, U3, U4, U5, U6, f116_in, U7, U8, U9, f566_in, U10, f478_in, U11, f118_in, U12, f113_in, U13, f228_in, U14, f323_in, U15, f380_in, U16, f475_in, U17, f562_in, U18

Defined Pair Symbols:

F116_IN, F2_IN, F566_IN, F478_IN, F118_IN, F113_IN, F228_IN, F323_IN, F380_IN, F475_IN, F562_IN

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c21, c22, c32, c34, c36, c38, c42, c46, c50, c54, c58, c

(21) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

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

F2_IN(z0, .(z0, z1)) → c1(F113_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c2(F2_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c3(F475_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c4(F2_IN(z0, z1))
F2_IN(z0, .(z1, z2)) → c5(F562_IN(z0, z2, z1))
F2_IN(z0, .(z1, z2)) → c6(F2_IN(z0, z2))
F475_IN(z0, z1) → c54(F116_IN(z0, z1), F478_IN(z0, z1))
F562_IN(z0, z1, z2) → c58(F116_IN(z0, z1), F566_IN(z0, z1, z2))
We considered the (Usable) Rules:none
And the Tuples:

F116_IN(z0, .(z0, [])) → c(F228_IN(z0))
F2_IN(z0, .(z0, z1)) → c1(F113_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c2(F2_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c3(F475_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c4(F2_IN(z0, z1))
F2_IN(z0, .(z1, z2)) → c5(F562_IN(z0, z2, z1))
F2_IN(z0, .(z1, z2)) → c6(F2_IN(z0, z2))
F116_IN(z0, .(z0, z1)) → c21(F323_IN(z0, z1))
F116_IN(z0, .(z1, z2)) → c22(F380_IN(z0, z2, z1))
F566_IN(z0, z1, z2) → c32(F2_IN(z0, z1))
F478_IN(z0, z1) → c34(F2_IN(z0, z1))
F118_IN(z0, z1) → c36(F2_IN(z0, z1))
F113_IN(z0, z1) → c38(F116_IN(z0, z1), F118_IN(z0, z1))
F228_IN(z0) → c42
F323_IN(z0, z1) → c46(F116_IN(z0, z1))
F380_IN(z0, z1, z2) → c50(F116_IN(z0, z1))
F475_IN(z0, z1) → c54(F116_IN(z0, z1), F478_IN(z0, z1))
F562_IN(z0, z1, z2) → c58(F116_IN(z0, z1), F566_IN(z0, z1, z2))
F116_IN(z0, .(z0, [])) → c
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(.(x1, x2)) = [1] + x2   
POL(F113_IN(x1, x2)) = x2 + x22   
POL(F116_IN(x1, x2)) = 0   
POL(F118_IN(x1, x2)) = x2 + x22   
POL(F228_IN(x1)) = 0   
POL(F2_IN(x1, x2)) = x2 + x22   
POL(F323_IN(x1, x2)) = 0   
POL(F380_IN(x1, x2, x3)) = 0   
POL(F475_IN(x1, x2)) = [1] + x2 + x22   
POL(F478_IN(x1, x2)) = x2 + x22   
POL(F562_IN(x1, x2, x3)) = [1] + x2 + x22   
POL(F566_IN(x1, x2, x3)) = x2 + x22   
POL([]) = 0   
POL(c) = 0   
POL(c(x1)) = x1   
POL(c1(x1)) = x1   
POL(c2(x1)) = x1   
POL(c21(x1)) = x1   
POL(c22(x1)) = x1   
POL(c3(x1)) = x1   
POL(c32(x1)) = x1   
POL(c34(x1)) = x1   
POL(c36(x1)) = x1   
POL(c38(x1, x2)) = x1 + x2   
POL(c4(x1)) = x1   
POL(c42) = 0   
POL(c46(x1)) = x1   
POL(c5(x1)) = x1   
POL(c50(x1)) = x1   
POL(c54(x1, x2)) = x1 + x2   
POL(c58(x1, x2)) = x1 + x2   
POL(c6(x1)) = x1   

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, .(z0, z1)) → f2_out1
f2_in(z0, .(z0, z1)) → U1(f113_in(z0, z1), z0, .(z0, z1))
f2_in(z0, .(z0, z1)) → U2(f2_in(z0, z1), z0, .(z0, z1))
f2_in(z0, .(z0, z1)) → U3(f475_in(z0, z1), z0, .(z0, z1))
f2_in(z0, .(z0, z1)) → U4(f2_in(z0, z1), z0, .(z0, z1))
f2_in(z0, .(z1, z2)) → U5(f562_in(z0, z2, z1), z0, .(z1, z2))
f2_in(z0, .(z1, z2)) → U6(f2_in(z0, z2), z0, .(z1, z2))
U1(f113_out1, z0, .(z0, z1)) → f2_out1
U1(f113_out2(z0), z1, .(z1, z2)) → f2_out1
U1(f113_out5(z0), z1, .(z1, z2)) → f2_out1
U2(f2_out1, z0, .(z0, z1)) → f2_out1
U3(f475_out1, z0, .(z0, z1)) → f2_out1
U3(f475_out2(z0), z1, .(z1, z2)) → f2_out1
U3(f475_out5(z0), z1, .(z1, z2)) → f2_out1
U4(f2_out1, z0, .(z0, z1)) → f2_out1
U5(f562_out1, z0, .(z1, z2)) → f2_out1
U5(f562_out2(z0), z1, .(z2, z3)) → f2_out1
U5(f562_out5(z0), z1, .(z2, z3)) → f2_out1
U6(f2_out1, z0, .(z1, z2)) → f2_out1
f116_in(z0, .(z0, [])) → f116_out1
f116_in(z0, .(z0, [])) → U7(f228_in(z0), z0, .(z0, []))
f116_in(z0, .(z0, z1)) → U8(f323_in(z0, z1), z0, .(z0, z1))
f116_in(z0, .(z1, z2)) → U9(f380_in(z0, z2, z1), z0, .(z1, z2))
U7(f228_out1, z0, .(z0, [])) → f116_out1
U7(f228_out2(z0), z1, .(z1, [])) → f116_out1
U7(f228_out5(z0, z1), z2, .(z2, [])) → f116_out1
U8(f323_out1, z0, .(z0, z1)) → f116_out1
U8(f323_out2(z0), z1, .(z1, z2)) → f116_out1
U8(f323_out5(z0, z1), z2, .(z2, z3)) → f116_out1
U9(f380_out1, z0, .(z1, z2)) → f116_out1
U9(f380_out2(z0), z1, .(z2, z3)) → f116_out1
U9(f380_out5(z0, z1), z2, .(z3, z4)) → f116_out1
f566_in(z0, z1, z2) → U10(f2_in(z0, z1), z0, z1, z2)
U10(f2_out1, z0, z1, z2) → f566_out4(z1)
f478_in(z0, z1) → U11(f2_in(z0, z1), z0, z1)
U11(f2_out1, z0, z1) → f478_out4(z1)
f118_in(z0, z1) → U12(f2_in(z0, z1), z0, z1)
U12(f2_out1, z0, z1) → f118_out4(z1)
f113_in(z0, z1) → U13(f116_in(z0, z1), f118_in(z0, z1), z0, z1)
U13(f116_out1, z0, z1, z2) → f113_out1
U13(z0, f118_out1(z1), z2, z3) → f113_out2(z1)
U13(z0, f118_out4(z1), z2, z3) → f113_out5(z1)
f228_in(z0) → U14(f231_in(z0), f232_in(z0), z0)
U14(f231_out1, z0, z1) → f228_out1
U14(z0, f232_out1(z1), z2) → f228_out2(z1)
U14(z0, f232_out4(z1, z2), z3) → f228_out5(z1, z2)
f323_in(z0, z1) → U15(f116_in(z0, z1), f326_in(z0, z1), z0, z1)
U15(f116_out1, z0, z1, z2) → f323_out1
U15(z0, f326_out1(z1), z2, z3) → f323_out2(z1)
U15(z0, f326_out4(z1, z2), z3, z4) → f323_out5(z1, z2)
f380_in(z0, z1, z2) → U16(f116_in(z0, z1), f384_in(z0, z1, z2), z0, z1, z2)
U16(f116_out1, z0, z1, z2, z3) → f380_out1
U16(z0, f384_out1(z1), z2, z3, z4) → f380_out2(z1)
U16(z0, f384_out4(z1, z2), z3, z4, z5) → f380_out5(z1, z2)
f475_in(z0, z1) → U17(f116_in(z0, z1), f478_in(z0, z1), z0, z1)
U17(f116_out1, z0, z1, z2) → f475_out1
U17(z0, f478_out1(z1), z2, z3) → f475_out2(z1)
U17(z0, f478_out4(z1), z2, z3) → f475_out5(z1)
f562_in(z0, z1, z2) → U18(f116_in(z0, z1), f566_in(z0, z1, z2), z0, z1, z2)
U18(f116_out1, z0, z1, z2, z3) → f562_out1
U18(z0, f566_out1(z1), z2, z3, z4) → f562_out2(z1)
U18(z0, f566_out4(z1), z2, z3, z4) → f562_out5(z1)
Tuples:

F116_IN(z0, .(z0, [])) → c(F228_IN(z0))
F2_IN(z0, .(z0, z1)) → c1(F113_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c2(F2_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c3(F475_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c4(F2_IN(z0, z1))
F2_IN(z0, .(z1, z2)) → c5(F562_IN(z0, z2, z1))
F2_IN(z0, .(z1, z2)) → c6(F2_IN(z0, z2))
F116_IN(z0, .(z0, z1)) → c21(F323_IN(z0, z1))
F116_IN(z0, .(z1, z2)) → c22(F380_IN(z0, z2, z1))
F566_IN(z0, z1, z2) → c32(F2_IN(z0, z1))
F478_IN(z0, z1) → c34(F2_IN(z0, z1))
F118_IN(z0, z1) → c36(F2_IN(z0, z1))
F113_IN(z0, z1) → c38(F116_IN(z0, z1), F118_IN(z0, z1))
F228_IN(z0) → c42
F323_IN(z0, z1) → c46(F116_IN(z0, z1))
F380_IN(z0, z1, z2) → c50(F116_IN(z0, z1))
F475_IN(z0, z1) → c54(F116_IN(z0, z1), F478_IN(z0, z1))
F562_IN(z0, z1, z2) → c58(F116_IN(z0, z1), F566_IN(z0, z1, z2))
F116_IN(z0, .(z0, [])) → c
S tuples:

F116_IN(z0, .(z0, [])) → c(F228_IN(z0))
F116_IN(z0, .(z0, z1)) → c21(F323_IN(z0, z1))
F116_IN(z0, .(z1, z2)) → c22(F380_IN(z0, z2, z1))
F566_IN(z0, z1, z2) → c32(F2_IN(z0, z1))
F478_IN(z0, z1) → c34(F2_IN(z0, z1))
F118_IN(z0, z1) → c36(F2_IN(z0, z1))
F113_IN(z0, z1) → c38(F116_IN(z0, z1), F118_IN(z0, z1))
F228_IN(z0) → c42
F323_IN(z0, z1) → c46(F116_IN(z0, z1))
F380_IN(z0, z1, z2) → c50(F116_IN(z0, z1))
F116_IN(z0, .(z0, [])) → c
K tuples:

F2_IN(z0, .(z0, z1)) → c1(F113_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c2(F2_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c3(F475_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c4(F2_IN(z0, z1))
F2_IN(z0, .(z1, z2)) → c5(F562_IN(z0, z2, z1))
F2_IN(z0, .(z1, z2)) → c6(F2_IN(z0, z2))
F475_IN(z0, z1) → c54(F116_IN(z0, z1), F478_IN(z0, z1))
F562_IN(z0, z1, z2) → c58(F116_IN(z0, z1), F566_IN(z0, z1, z2))
Defined Rule Symbols:

f2_in, U1, U2, U3, U4, U5, U6, f116_in, U7, U8, U9, f566_in, U10, f478_in, U11, f118_in, U12, f113_in, U13, f228_in, U14, f323_in, U15, f380_in, U16, f475_in, U17, f562_in, U18

Defined Pair Symbols:

F116_IN, F2_IN, F566_IN, F478_IN, F118_IN, F113_IN, F228_IN, F323_IN, F380_IN, F475_IN, F562_IN

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c21, c22, c32, c34, c36, c38, c42, c46, c50, c54, c58, c

(23) CdtKnowledgeProof (EQUIVALENT transformation)

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

F566_IN(z0, z1, z2) → c32(F2_IN(z0, z1))
F478_IN(z0, z1) → c34(F2_IN(z0, z1))
F113_IN(z0, z1) → c38(F116_IN(z0, z1), F118_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c1(F113_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c2(F2_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c3(F475_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c4(F2_IN(z0, z1))
F2_IN(z0, .(z1, z2)) → c5(F562_IN(z0, z2, z1))
F2_IN(z0, .(z1, z2)) → c6(F2_IN(z0, z2))
F2_IN(z0, .(z0, z1)) → c1(F113_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c2(F2_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c3(F475_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c4(F2_IN(z0, z1))
F2_IN(z0, .(z1, z2)) → c5(F562_IN(z0, z2, z1))
F2_IN(z0, .(z1, z2)) → c6(F2_IN(z0, z2))
F118_IN(z0, z1) → c36(F2_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c1(F113_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c2(F2_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c3(F475_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c4(F2_IN(z0, z1))
F2_IN(z0, .(z1, z2)) → c5(F562_IN(z0, z2, z1))
F2_IN(z0, .(z1, z2)) → c6(F2_IN(z0, z2))

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, .(z0, z1)) → f2_out1
f2_in(z0, .(z0, z1)) → U1(f113_in(z0, z1), z0, .(z0, z1))
f2_in(z0, .(z0, z1)) → U2(f2_in(z0, z1), z0, .(z0, z1))
f2_in(z0, .(z0, z1)) → U3(f475_in(z0, z1), z0, .(z0, z1))
f2_in(z0, .(z0, z1)) → U4(f2_in(z0, z1), z0, .(z0, z1))
f2_in(z0, .(z1, z2)) → U5(f562_in(z0, z2, z1), z0, .(z1, z2))
f2_in(z0, .(z1, z2)) → U6(f2_in(z0, z2), z0, .(z1, z2))
U1(f113_out1, z0, .(z0, z1)) → f2_out1
U1(f113_out2(z0), z1, .(z1, z2)) → f2_out1
U1(f113_out5(z0), z1, .(z1, z2)) → f2_out1
U2(f2_out1, z0, .(z0, z1)) → f2_out1
U3(f475_out1, z0, .(z0, z1)) → f2_out1
U3(f475_out2(z0), z1, .(z1, z2)) → f2_out1
U3(f475_out5(z0), z1, .(z1, z2)) → f2_out1
U4(f2_out1, z0, .(z0, z1)) → f2_out1
U5(f562_out1, z0, .(z1, z2)) → f2_out1
U5(f562_out2(z0), z1, .(z2, z3)) → f2_out1
U5(f562_out5(z0), z1, .(z2, z3)) → f2_out1
U6(f2_out1, z0, .(z1, z2)) → f2_out1
f116_in(z0, .(z0, [])) → f116_out1
f116_in(z0, .(z0, [])) → U7(f228_in(z0), z0, .(z0, []))
f116_in(z0, .(z0, z1)) → U8(f323_in(z0, z1), z0, .(z0, z1))
f116_in(z0, .(z1, z2)) → U9(f380_in(z0, z2, z1), z0, .(z1, z2))
U7(f228_out1, z0, .(z0, [])) → f116_out1
U7(f228_out2(z0), z1, .(z1, [])) → f116_out1
U7(f228_out5(z0, z1), z2, .(z2, [])) → f116_out1
U8(f323_out1, z0, .(z0, z1)) → f116_out1
U8(f323_out2(z0), z1, .(z1, z2)) → f116_out1
U8(f323_out5(z0, z1), z2, .(z2, z3)) → f116_out1
U9(f380_out1, z0, .(z1, z2)) → f116_out1
U9(f380_out2(z0), z1, .(z2, z3)) → f116_out1
U9(f380_out5(z0, z1), z2, .(z3, z4)) → f116_out1
f566_in(z0, z1, z2) → U10(f2_in(z0, z1), z0, z1, z2)
U10(f2_out1, z0, z1, z2) → f566_out4(z1)
f478_in(z0, z1) → U11(f2_in(z0, z1), z0, z1)
U11(f2_out1, z0, z1) → f478_out4(z1)
f118_in(z0, z1) → U12(f2_in(z0, z1), z0, z1)
U12(f2_out1, z0, z1) → f118_out4(z1)
f113_in(z0, z1) → U13(f116_in(z0, z1), f118_in(z0, z1), z0, z1)
U13(f116_out1, z0, z1, z2) → f113_out1
U13(z0, f118_out1(z1), z2, z3) → f113_out2(z1)
U13(z0, f118_out4(z1), z2, z3) → f113_out5(z1)
f228_in(z0) → U14(f231_in(z0), f232_in(z0), z0)
U14(f231_out1, z0, z1) → f228_out1
U14(z0, f232_out1(z1), z2) → f228_out2(z1)
U14(z0, f232_out4(z1, z2), z3) → f228_out5(z1, z2)
f323_in(z0, z1) → U15(f116_in(z0, z1), f326_in(z0, z1), z0, z1)
U15(f116_out1, z0, z1, z2) → f323_out1
U15(z0, f326_out1(z1), z2, z3) → f323_out2(z1)
U15(z0, f326_out4(z1, z2), z3, z4) → f323_out5(z1, z2)
f380_in(z0, z1, z2) → U16(f116_in(z0, z1), f384_in(z0, z1, z2), z0, z1, z2)
U16(f116_out1, z0, z1, z2, z3) → f380_out1
U16(z0, f384_out1(z1), z2, z3, z4) → f380_out2(z1)
U16(z0, f384_out4(z1, z2), z3, z4, z5) → f380_out5(z1, z2)
f475_in(z0, z1) → U17(f116_in(z0, z1), f478_in(z0, z1), z0, z1)
U17(f116_out1, z0, z1, z2) → f475_out1
U17(z0, f478_out1(z1), z2, z3) → f475_out2(z1)
U17(z0, f478_out4(z1), z2, z3) → f475_out5(z1)
f562_in(z0, z1, z2) → U18(f116_in(z0, z1), f566_in(z0, z1, z2), z0, z1, z2)
U18(f116_out1, z0, z1, z2, z3) → f562_out1
U18(z0, f566_out1(z1), z2, z3, z4) → f562_out2(z1)
U18(z0, f566_out4(z1), z2, z3, z4) → f562_out5(z1)
Tuples:

F116_IN(z0, .(z0, [])) → c(F228_IN(z0))
F2_IN(z0, .(z0, z1)) → c1(F113_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c2(F2_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c3(F475_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c4(F2_IN(z0, z1))
F2_IN(z0, .(z1, z2)) → c5(F562_IN(z0, z2, z1))
F2_IN(z0, .(z1, z2)) → c6(F2_IN(z0, z2))
F116_IN(z0, .(z0, z1)) → c21(F323_IN(z0, z1))
F116_IN(z0, .(z1, z2)) → c22(F380_IN(z0, z2, z1))
F566_IN(z0, z1, z2) → c32(F2_IN(z0, z1))
F478_IN(z0, z1) → c34(F2_IN(z0, z1))
F118_IN(z0, z1) → c36(F2_IN(z0, z1))
F113_IN(z0, z1) → c38(F116_IN(z0, z1), F118_IN(z0, z1))
F228_IN(z0) → c42
F323_IN(z0, z1) → c46(F116_IN(z0, z1))
F380_IN(z0, z1, z2) → c50(F116_IN(z0, z1))
F475_IN(z0, z1) → c54(F116_IN(z0, z1), F478_IN(z0, z1))
F562_IN(z0, z1, z2) → c58(F116_IN(z0, z1), F566_IN(z0, z1, z2))
F116_IN(z0, .(z0, [])) → c
S tuples:

F116_IN(z0, .(z0, [])) → c(F228_IN(z0))
F116_IN(z0, .(z0, z1)) → c21(F323_IN(z0, z1))
F116_IN(z0, .(z1, z2)) → c22(F380_IN(z0, z2, z1))
F228_IN(z0) → c42
F323_IN(z0, z1) → c46(F116_IN(z0, z1))
F380_IN(z0, z1, z2) → c50(F116_IN(z0, z1))
F116_IN(z0, .(z0, [])) → c
K tuples:

F2_IN(z0, .(z0, z1)) → c1(F113_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c2(F2_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c3(F475_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c4(F2_IN(z0, z1))
F2_IN(z0, .(z1, z2)) → c5(F562_IN(z0, z2, z1))
F2_IN(z0, .(z1, z2)) → c6(F2_IN(z0, z2))
F475_IN(z0, z1) → c54(F116_IN(z0, z1), F478_IN(z0, z1))
F562_IN(z0, z1, z2) → c58(F116_IN(z0, z1), F566_IN(z0, z1, z2))
F566_IN(z0, z1, z2) → c32(F2_IN(z0, z1))
F478_IN(z0, z1) → c34(F2_IN(z0, z1))
F113_IN(z0, z1) → c38(F116_IN(z0, z1), F118_IN(z0, z1))
F118_IN(z0, z1) → c36(F2_IN(z0, z1))
Defined Rule Symbols:

f2_in, U1, U2, U3, U4, U5, U6, f116_in, U7, U8, U9, f566_in, U10, f478_in, U11, f118_in, U12, f113_in, U13, f228_in, U14, f323_in, U15, f380_in, U16, f475_in, U17, f562_in, U18

Defined Pair Symbols:

F116_IN, F2_IN, F566_IN, F478_IN, F118_IN, F113_IN, F228_IN, F323_IN, F380_IN, F475_IN, F562_IN

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c21, c22, c32, c34, c36, c38, c42, c46, c50, c54, c58, 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.

F116_IN(z0, .(z0, [])) → c(F228_IN(z0))
F116_IN(z0, .(z0, [])) → c
We considered the (Usable) Rules:none
And the Tuples:

F116_IN(z0, .(z0, [])) → c(F228_IN(z0))
F2_IN(z0, .(z0, z1)) → c1(F113_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c2(F2_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c3(F475_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c4(F2_IN(z0, z1))
F2_IN(z0, .(z1, z2)) → c5(F562_IN(z0, z2, z1))
F2_IN(z0, .(z1, z2)) → c6(F2_IN(z0, z2))
F116_IN(z0, .(z0, z1)) → c21(F323_IN(z0, z1))
F116_IN(z0, .(z1, z2)) → c22(F380_IN(z0, z2, z1))
F566_IN(z0, z1, z2) → c32(F2_IN(z0, z1))
F478_IN(z0, z1) → c34(F2_IN(z0, z1))
F118_IN(z0, z1) → c36(F2_IN(z0, z1))
F113_IN(z0, z1) → c38(F116_IN(z0, z1), F118_IN(z0, z1))
F228_IN(z0) → c42
F323_IN(z0, z1) → c46(F116_IN(z0, z1))
F380_IN(z0, z1, z2) → c50(F116_IN(z0, z1))
F475_IN(z0, z1) → c54(F116_IN(z0, z1), F478_IN(z0, z1))
F562_IN(z0, z1, z2) → c58(F116_IN(z0, z1), F566_IN(z0, z1, z2))
F116_IN(z0, .(z0, [])) → c
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(.(x1, x2)) = [2] + x2   
POL(F113_IN(x1, x2)) = [2] + x2   
POL(F116_IN(x1, x2)) = [2]   
POL(F118_IN(x1, x2)) = x2   
POL(F228_IN(x1)) = 0   
POL(F2_IN(x1, x2)) = x2   
POL(F323_IN(x1, x2)) = [2]   
POL(F380_IN(x1, x2, x3)) = [2]   
POL(F475_IN(x1, x2)) = [2] + x2   
POL(F478_IN(x1, x2)) = x2   
POL(F562_IN(x1, x2, x3)) = [2] + x2   
POL(F566_IN(x1, x2, x3)) = x2   
POL([]) = 0   
POL(c) = 0   
POL(c(x1)) = x1   
POL(c1(x1)) = x1   
POL(c2(x1)) = x1   
POL(c21(x1)) = x1   
POL(c22(x1)) = x1   
POL(c3(x1)) = x1   
POL(c32(x1)) = x1   
POL(c34(x1)) = x1   
POL(c36(x1)) = x1   
POL(c38(x1, x2)) = x1 + x2   
POL(c4(x1)) = x1   
POL(c42) = 0   
POL(c46(x1)) = x1   
POL(c5(x1)) = x1   
POL(c50(x1)) = x1   
POL(c54(x1, x2)) = x1 + x2   
POL(c58(x1, x2)) = x1 + x2   
POL(c6(x1)) = x1   

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, .(z0, z1)) → f2_out1
f2_in(z0, .(z0, z1)) → U1(f113_in(z0, z1), z0, .(z0, z1))
f2_in(z0, .(z0, z1)) → U2(f2_in(z0, z1), z0, .(z0, z1))
f2_in(z0, .(z0, z1)) → U3(f475_in(z0, z1), z0, .(z0, z1))
f2_in(z0, .(z0, z1)) → U4(f2_in(z0, z1), z0, .(z0, z1))
f2_in(z0, .(z1, z2)) → U5(f562_in(z0, z2, z1), z0, .(z1, z2))
f2_in(z0, .(z1, z2)) → U6(f2_in(z0, z2), z0, .(z1, z2))
U1(f113_out1, z0, .(z0, z1)) → f2_out1
U1(f113_out2(z0), z1, .(z1, z2)) → f2_out1
U1(f113_out5(z0), z1, .(z1, z2)) → f2_out1
U2(f2_out1, z0, .(z0, z1)) → f2_out1
U3(f475_out1, z0, .(z0, z1)) → f2_out1
U3(f475_out2(z0), z1, .(z1, z2)) → f2_out1
U3(f475_out5(z0), z1, .(z1, z2)) → f2_out1
U4(f2_out1, z0, .(z0, z1)) → f2_out1
U5(f562_out1, z0, .(z1, z2)) → f2_out1
U5(f562_out2(z0), z1, .(z2, z3)) → f2_out1
U5(f562_out5(z0), z1, .(z2, z3)) → f2_out1
U6(f2_out1, z0, .(z1, z2)) → f2_out1
f116_in(z0, .(z0, [])) → f116_out1
f116_in(z0, .(z0, [])) → U7(f228_in(z0), z0, .(z0, []))
f116_in(z0, .(z0, z1)) → U8(f323_in(z0, z1), z0, .(z0, z1))
f116_in(z0, .(z1, z2)) → U9(f380_in(z0, z2, z1), z0, .(z1, z2))
U7(f228_out1, z0, .(z0, [])) → f116_out1
U7(f228_out2(z0), z1, .(z1, [])) → f116_out1
U7(f228_out5(z0, z1), z2, .(z2, [])) → f116_out1
U8(f323_out1, z0, .(z0, z1)) → f116_out1
U8(f323_out2(z0), z1, .(z1, z2)) → f116_out1
U8(f323_out5(z0, z1), z2, .(z2, z3)) → f116_out1
U9(f380_out1, z0, .(z1, z2)) → f116_out1
U9(f380_out2(z0), z1, .(z2, z3)) → f116_out1
U9(f380_out5(z0, z1), z2, .(z3, z4)) → f116_out1
f566_in(z0, z1, z2) → U10(f2_in(z0, z1), z0, z1, z2)
U10(f2_out1, z0, z1, z2) → f566_out4(z1)
f478_in(z0, z1) → U11(f2_in(z0, z1), z0, z1)
U11(f2_out1, z0, z1) → f478_out4(z1)
f118_in(z0, z1) → U12(f2_in(z0, z1), z0, z1)
U12(f2_out1, z0, z1) → f118_out4(z1)
f113_in(z0, z1) → U13(f116_in(z0, z1), f118_in(z0, z1), z0, z1)
U13(f116_out1, z0, z1, z2) → f113_out1
U13(z0, f118_out1(z1), z2, z3) → f113_out2(z1)
U13(z0, f118_out4(z1), z2, z3) → f113_out5(z1)
f228_in(z0) → U14(f231_in(z0), f232_in(z0), z0)
U14(f231_out1, z0, z1) → f228_out1
U14(z0, f232_out1(z1), z2) → f228_out2(z1)
U14(z0, f232_out4(z1, z2), z3) → f228_out5(z1, z2)
f323_in(z0, z1) → U15(f116_in(z0, z1), f326_in(z0, z1), z0, z1)
U15(f116_out1, z0, z1, z2) → f323_out1
U15(z0, f326_out1(z1), z2, z3) → f323_out2(z1)
U15(z0, f326_out4(z1, z2), z3, z4) → f323_out5(z1, z2)
f380_in(z0, z1, z2) → U16(f116_in(z0, z1), f384_in(z0, z1, z2), z0, z1, z2)
U16(f116_out1, z0, z1, z2, z3) → f380_out1
U16(z0, f384_out1(z1), z2, z3, z4) → f380_out2(z1)
U16(z0, f384_out4(z1, z2), z3, z4, z5) → f380_out5(z1, z2)
f475_in(z0, z1) → U17(f116_in(z0, z1), f478_in(z0, z1), z0, z1)
U17(f116_out1, z0, z1, z2) → f475_out1
U17(z0, f478_out1(z1), z2, z3) → f475_out2(z1)
U17(z0, f478_out4(z1), z2, z3) → f475_out5(z1)
f562_in(z0, z1, z2) → U18(f116_in(z0, z1), f566_in(z0, z1, z2), z0, z1, z2)
U18(f116_out1, z0, z1, z2, z3) → f562_out1
U18(z0, f566_out1(z1), z2, z3, z4) → f562_out2(z1)
U18(z0, f566_out4(z1), z2, z3, z4) → f562_out5(z1)
Tuples:

F116_IN(z0, .(z0, [])) → c(F228_IN(z0))
F2_IN(z0, .(z0, z1)) → c1(F113_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c2(F2_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c3(F475_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c4(F2_IN(z0, z1))
F2_IN(z0, .(z1, z2)) → c5(F562_IN(z0, z2, z1))
F2_IN(z0, .(z1, z2)) → c6(F2_IN(z0, z2))
F116_IN(z0, .(z0, z1)) → c21(F323_IN(z0, z1))
F116_IN(z0, .(z1, z2)) → c22(F380_IN(z0, z2, z1))
F566_IN(z0, z1, z2) → c32(F2_IN(z0, z1))
F478_IN(z0, z1) → c34(F2_IN(z0, z1))
F118_IN(z0, z1) → c36(F2_IN(z0, z1))
F113_IN(z0, z1) → c38(F116_IN(z0, z1), F118_IN(z0, z1))
F228_IN(z0) → c42
F323_IN(z0, z1) → c46(F116_IN(z0, z1))
F380_IN(z0, z1, z2) → c50(F116_IN(z0, z1))
F475_IN(z0, z1) → c54(F116_IN(z0, z1), F478_IN(z0, z1))
F562_IN(z0, z1, z2) → c58(F116_IN(z0, z1), F566_IN(z0, z1, z2))
F116_IN(z0, .(z0, [])) → c
S tuples:

F116_IN(z0, .(z0, z1)) → c21(F323_IN(z0, z1))
F116_IN(z0, .(z1, z2)) → c22(F380_IN(z0, z2, z1))
F228_IN(z0) → c42
F323_IN(z0, z1) → c46(F116_IN(z0, z1))
F380_IN(z0, z1, z2) → c50(F116_IN(z0, z1))
K tuples:

F2_IN(z0, .(z0, z1)) → c1(F113_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c2(F2_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c3(F475_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c4(F2_IN(z0, z1))
F2_IN(z0, .(z1, z2)) → c5(F562_IN(z0, z2, z1))
F2_IN(z0, .(z1, z2)) → c6(F2_IN(z0, z2))
F475_IN(z0, z1) → c54(F116_IN(z0, z1), F478_IN(z0, z1))
F562_IN(z0, z1, z2) → c58(F116_IN(z0, z1), F566_IN(z0, z1, z2))
F566_IN(z0, z1, z2) → c32(F2_IN(z0, z1))
F478_IN(z0, z1) → c34(F2_IN(z0, z1))
F113_IN(z0, z1) → c38(F116_IN(z0, z1), F118_IN(z0, z1))
F118_IN(z0, z1) → c36(F2_IN(z0, z1))
F116_IN(z0, .(z0, [])) → c(F228_IN(z0))
F116_IN(z0, .(z0, [])) → c
Defined Rule Symbols:

f2_in, U1, U2, U3, U4, U5, U6, f116_in, U7, U8, U9, f566_in, U10, f478_in, U11, f118_in, U12, f113_in, U13, f228_in, U14, f323_in, U15, f380_in, U16, f475_in, U17, f562_in, U18

Defined Pair Symbols:

F116_IN, F2_IN, F566_IN, F478_IN, F118_IN, F113_IN, F228_IN, F323_IN, F380_IN, F475_IN, F562_IN

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c21, c22, c32, c34, c36, c38, c42, c46, c50, c54, c58, c

(27) CdtKnowledgeProof (EQUIVALENT transformation)

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

F228_IN(z0) → c42

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, .(z0, z1)) → f2_out1
f2_in(z0, .(z0, z1)) → U1(f113_in(z0, z1), z0, .(z0, z1))
f2_in(z0, .(z0, z1)) → U2(f2_in(z0, z1), z0, .(z0, z1))
f2_in(z0, .(z0, z1)) → U3(f475_in(z0, z1), z0, .(z0, z1))
f2_in(z0, .(z0, z1)) → U4(f2_in(z0, z1), z0, .(z0, z1))
f2_in(z0, .(z1, z2)) → U5(f562_in(z0, z2, z1), z0, .(z1, z2))
f2_in(z0, .(z1, z2)) → U6(f2_in(z0, z2), z0, .(z1, z2))
U1(f113_out1, z0, .(z0, z1)) → f2_out1
U1(f113_out2(z0), z1, .(z1, z2)) → f2_out1
U1(f113_out5(z0), z1, .(z1, z2)) → f2_out1
U2(f2_out1, z0, .(z0, z1)) → f2_out1
U3(f475_out1, z0, .(z0, z1)) → f2_out1
U3(f475_out2(z0), z1, .(z1, z2)) → f2_out1
U3(f475_out5(z0), z1, .(z1, z2)) → f2_out1
U4(f2_out1, z0, .(z0, z1)) → f2_out1
U5(f562_out1, z0, .(z1, z2)) → f2_out1
U5(f562_out2(z0), z1, .(z2, z3)) → f2_out1
U5(f562_out5(z0), z1, .(z2, z3)) → f2_out1
U6(f2_out1, z0, .(z1, z2)) → f2_out1
f116_in(z0, .(z0, [])) → f116_out1
f116_in(z0, .(z0, [])) → U7(f228_in(z0), z0, .(z0, []))
f116_in(z0, .(z0, z1)) → U8(f323_in(z0, z1), z0, .(z0, z1))
f116_in(z0, .(z1, z2)) → U9(f380_in(z0, z2, z1), z0, .(z1, z2))
U7(f228_out1, z0, .(z0, [])) → f116_out1
U7(f228_out2(z0), z1, .(z1, [])) → f116_out1
U7(f228_out5(z0, z1), z2, .(z2, [])) → f116_out1
U8(f323_out1, z0, .(z0, z1)) → f116_out1
U8(f323_out2(z0), z1, .(z1, z2)) → f116_out1
U8(f323_out5(z0, z1), z2, .(z2, z3)) → f116_out1
U9(f380_out1, z0, .(z1, z2)) → f116_out1
U9(f380_out2(z0), z1, .(z2, z3)) → f116_out1
U9(f380_out5(z0, z1), z2, .(z3, z4)) → f116_out1
f566_in(z0, z1, z2) → U10(f2_in(z0, z1), z0, z1, z2)
U10(f2_out1, z0, z1, z2) → f566_out4(z1)
f478_in(z0, z1) → U11(f2_in(z0, z1), z0, z1)
U11(f2_out1, z0, z1) → f478_out4(z1)
f118_in(z0, z1) → U12(f2_in(z0, z1), z0, z1)
U12(f2_out1, z0, z1) → f118_out4(z1)
f113_in(z0, z1) → U13(f116_in(z0, z1), f118_in(z0, z1), z0, z1)
U13(f116_out1, z0, z1, z2) → f113_out1
U13(z0, f118_out1(z1), z2, z3) → f113_out2(z1)
U13(z0, f118_out4(z1), z2, z3) → f113_out5(z1)
f228_in(z0) → U14(f231_in(z0), f232_in(z0), z0)
U14(f231_out1, z0, z1) → f228_out1
U14(z0, f232_out1(z1), z2) → f228_out2(z1)
U14(z0, f232_out4(z1, z2), z3) → f228_out5(z1, z2)
f323_in(z0, z1) → U15(f116_in(z0, z1), f326_in(z0, z1), z0, z1)
U15(f116_out1, z0, z1, z2) → f323_out1
U15(z0, f326_out1(z1), z2, z3) → f323_out2(z1)
U15(z0, f326_out4(z1, z2), z3, z4) → f323_out5(z1, z2)
f380_in(z0, z1, z2) → U16(f116_in(z0, z1), f384_in(z0, z1, z2), z0, z1, z2)
U16(f116_out1, z0, z1, z2, z3) → f380_out1
U16(z0, f384_out1(z1), z2, z3, z4) → f380_out2(z1)
U16(z0, f384_out4(z1, z2), z3, z4, z5) → f380_out5(z1, z2)
f475_in(z0, z1) → U17(f116_in(z0, z1), f478_in(z0, z1), z0, z1)
U17(f116_out1, z0, z1, z2) → f475_out1
U17(z0, f478_out1(z1), z2, z3) → f475_out2(z1)
U17(z0, f478_out4(z1), z2, z3) → f475_out5(z1)
f562_in(z0, z1, z2) → U18(f116_in(z0, z1), f566_in(z0, z1, z2), z0, z1, z2)
U18(f116_out1, z0, z1, z2, z3) → f562_out1
U18(z0, f566_out1(z1), z2, z3, z4) → f562_out2(z1)
U18(z0, f566_out4(z1), z2, z3, z4) → f562_out5(z1)
Tuples:

F116_IN(z0, .(z0, [])) → c(F228_IN(z0))
F2_IN(z0, .(z0, z1)) → c1(F113_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c2(F2_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c3(F475_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c4(F2_IN(z0, z1))
F2_IN(z0, .(z1, z2)) → c5(F562_IN(z0, z2, z1))
F2_IN(z0, .(z1, z2)) → c6(F2_IN(z0, z2))
F116_IN(z0, .(z0, z1)) → c21(F323_IN(z0, z1))
F116_IN(z0, .(z1, z2)) → c22(F380_IN(z0, z2, z1))
F566_IN(z0, z1, z2) → c32(F2_IN(z0, z1))
F478_IN(z0, z1) → c34(F2_IN(z0, z1))
F118_IN(z0, z1) → c36(F2_IN(z0, z1))
F113_IN(z0, z1) → c38(F116_IN(z0, z1), F118_IN(z0, z1))
F228_IN(z0) → c42
F323_IN(z0, z1) → c46(F116_IN(z0, z1))
F380_IN(z0, z1, z2) → c50(F116_IN(z0, z1))
F475_IN(z0, z1) → c54(F116_IN(z0, z1), F478_IN(z0, z1))
F562_IN(z0, z1, z2) → c58(F116_IN(z0, z1), F566_IN(z0, z1, z2))
F116_IN(z0, .(z0, [])) → c
S tuples:

F116_IN(z0, .(z0, z1)) → c21(F323_IN(z0, z1))
F116_IN(z0, .(z1, z2)) → c22(F380_IN(z0, z2, z1))
F323_IN(z0, z1) → c46(F116_IN(z0, z1))
F380_IN(z0, z1, z2) → c50(F116_IN(z0, z1))
K tuples:

F2_IN(z0, .(z0, z1)) → c1(F113_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c2(F2_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c3(F475_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c4(F2_IN(z0, z1))
F2_IN(z0, .(z1, z2)) → c5(F562_IN(z0, z2, z1))
F2_IN(z0, .(z1, z2)) → c6(F2_IN(z0, z2))
F475_IN(z0, z1) → c54(F116_IN(z0, z1), F478_IN(z0, z1))
F562_IN(z0, z1, z2) → c58(F116_IN(z0, z1), F566_IN(z0, z1, z2))
F566_IN(z0, z1, z2) → c32(F2_IN(z0, z1))
F478_IN(z0, z1) → c34(F2_IN(z0, z1))
F113_IN(z0, z1) → c38(F116_IN(z0, z1), F118_IN(z0, z1))
F118_IN(z0, z1) → c36(F2_IN(z0, z1))
F116_IN(z0, .(z0, [])) → c(F228_IN(z0))
F116_IN(z0, .(z0, [])) → c
F228_IN(z0) → c42
Defined Rule Symbols:

f2_in, U1, U2, U3, U4, U5, U6, f116_in, U7, U8, U9, f566_in, U10, f478_in, U11, f118_in, U12, f113_in, U13, f228_in, U14, f323_in, U15, f380_in, U16, f475_in, U17, f562_in, U18

Defined Pair Symbols:

F116_IN, F2_IN, F566_IN, F478_IN, F118_IN, F113_IN, F228_IN, F323_IN, F380_IN, F475_IN, F562_IN

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c21, c22, c32, c34, c36, c38, c42, c46, c50, c54, c58, c

(29) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

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

F116_IN(z0, .(z0, z1)) → c21(F323_IN(z0, z1))
F380_IN(z0, z1, z2) → c50(F116_IN(z0, z1))
We considered the (Usable) Rules:none
And the Tuples:

F116_IN(z0, .(z0, [])) → c(F228_IN(z0))
F2_IN(z0, .(z0, z1)) → c1(F113_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c2(F2_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c3(F475_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c4(F2_IN(z0, z1))
F2_IN(z0, .(z1, z2)) → c5(F562_IN(z0, z2, z1))
F2_IN(z0, .(z1, z2)) → c6(F2_IN(z0, z2))
F116_IN(z0, .(z0, z1)) → c21(F323_IN(z0, z1))
F116_IN(z0, .(z1, z2)) → c22(F380_IN(z0, z2, z1))
F566_IN(z0, z1, z2) → c32(F2_IN(z0, z1))
F478_IN(z0, z1) → c34(F2_IN(z0, z1))
F118_IN(z0, z1) → c36(F2_IN(z0, z1))
F113_IN(z0, z1) → c38(F116_IN(z0, z1), F118_IN(z0, z1))
F228_IN(z0) → c42
F323_IN(z0, z1) → c46(F116_IN(z0, z1))
F380_IN(z0, z1, z2) → c50(F116_IN(z0, z1))
F475_IN(z0, z1) → c54(F116_IN(z0, z1), F478_IN(z0, z1))
F562_IN(z0, z1, z2) → c58(F116_IN(z0, z1), F566_IN(z0, z1, z2))
F116_IN(z0, .(z0, [])) → c
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(.(x1, x2)) = [1] + x2   
POL(F113_IN(x1, x2)) = [1] + x2 + x22   
POL(F116_IN(x1, x2)) = x2   
POL(F118_IN(x1, x2)) = [1] + x22   
POL(F228_IN(x1)) = [1]   
POL(F2_IN(x1, x2)) = x22   
POL(F323_IN(x1, x2)) = x2   
POL(F380_IN(x1, x2, x3)) = [1] + x2   
POL(F475_IN(x1, x2)) = [1] + x2 + x22   
POL(F478_IN(x1, x2)) = x22   
POL(F562_IN(x1, x2, x3)) = [1] + x2 + x22   
POL(F566_IN(x1, x2, x3)) = [1] + x22   
POL([]) = 0   
POL(c) = 0   
POL(c(x1)) = x1   
POL(c1(x1)) = x1   
POL(c2(x1)) = x1   
POL(c21(x1)) = x1   
POL(c22(x1)) = x1   
POL(c3(x1)) = x1   
POL(c32(x1)) = x1   
POL(c34(x1)) = x1   
POL(c36(x1)) = x1   
POL(c38(x1, x2)) = x1 + x2   
POL(c4(x1)) = x1   
POL(c42) = 0   
POL(c46(x1)) = x1   
POL(c5(x1)) = x1   
POL(c50(x1)) = x1   
POL(c54(x1, x2)) = x1 + x2   
POL(c58(x1, x2)) = x1 + x2   
POL(c6(x1)) = x1   

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0, .(z0, z1)) → f2_out1
f2_in(z0, .(z0, z1)) → U1(f113_in(z0, z1), z0, .(z0, z1))
f2_in(z0, .(z0, z1)) → U2(f2_in(z0, z1), z0, .(z0, z1))
f2_in(z0, .(z0, z1)) → U3(f475_in(z0, z1), z0, .(z0, z1))
f2_in(z0, .(z0, z1)) → U4(f2_in(z0, z1), z0, .(z0, z1))
f2_in(z0, .(z1, z2)) → U5(f562_in(z0, z2, z1), z0, .(z1, z2))
f2_in(z0, .(z1, z2)) → U6(f2_in(z0, z2), z0, .(z1, z2))
U1(f113_out1, z0, .(z0, z1)) → f2_out1
U1(f113_out2(z0), z1, .(z1, z2)) → f2_out1
U1(f113_out5(z0), z1, .(z1, z2)) → f2_out1
U2(f2_out1, z0, .(z0, z1)) → f2_out1
U3(f475_out1, z0, .(z0, z1)) → f2_out1
U3(f475_out2(z0), z1, .(z1, z2)) → f2_out1
U3(f475_out5(z0), z1, .(z1, z2)) → f2_out1
U4(f2_out1, z0, .(z0, z1)) → f2_out1
U5(f562_out1, z0, .(z1, z2)) → f2_out1
U5(f562_out2(z0), z1, .(z2, z3)) → f2_out1
U5(f562_out5(z0), z1, .(z2, z3)) → f2_out1
U6(f2_out1, z0, .(z1, z2)) → f2_out1
f116_in(z0, .(z0, [])) → f116_out1
f116_in(z0, .(z0, [])) → U7(f228_in(z0), z0, .(z0, []))
f116_in(z0, .(z0, z1)) → U8(f323_in(z0, z1), z0, .(z0, z1))
f116_in(z0, .(z1, z2)) → U9(f380_in(z0, z2, z1), z0, .(z1, z2))
U7(f228_out1, z0, .(z0, [])) → f116_out1
U7(f228_out2(z0), z1, .(z1, [])) → f116_out1
U7(f228_out5(z0, z1), z2, .(z2, [])) → f116_out1
U8(f323_out1, z0, .(z0, z1)) → f116_out1
U8(f323_out2(z0), z1, .(z1, z2)) → f116_out1
U8(f323_out5(z0, z1), z2, .(z2, z3)) → f116_out1
U9(f380_out1, z0, .(z1, z2)) → f116_out1
U9(f380_out2(z0), z1, .(z2, z3)) → f116_out1
U9(f380_out5(z0, z1), z2, .(z3, z4)) → f116_out1
f566_in(z0, z1, z2) → U10(f2_in(z0, z1), z0, z1, z2)
U10(f2_out1, z0, z1, z2) → f566_out4(z1)
f478_in(z0, z1) → U11(f2_in(z0, z1), z0, z1)
U11(f2_out1, z0, z1) → f478_out4(z1)
f118_in(z0, z1) → U12(f2_in(z0, z1), z0, z1)
U12(f2_out1, z0, z1) → f118_out4(z1)
f113_in(z0, z1) → U13(f116_in(z0, z1), f118_in(z0, z1), z0, z1)
U13(f116_out1, z0, z1, z2) → f113_out1
U13(z0, f118_out1(z1), z2, z3) → f113_out2(z1)
U13(z0, f118_out4(z1), z2, z3) → f113_out5(z1)
f228_in(z0) → U14(f231_in(z0), f232_in(z0), z0)
U14(f231_out1, z0, z1) → f228_out1
U14(z0, f232_out1(z1), z2) → f228_out2(z1)
U14(z0, f232_out4(z1, z2), z3) → f228_out5(z1, z2)
f323_in(z0, z1) → U15(f116_in(z0, z1), f326_in(z0, z1), z0, z1)
U15(f116_out1, z0, z1, z2) → f323_out1
U15(z0, f326_out1(z1), z2, z3) → f323_out2(z1)
U15(z0, f326_out4(z1, z2), z3, z4) → f323_out5(z1, z2)
f380_in(z0, z1, z2) → U16(f116_in(z0, z1), f384_in(z0, z1, z2), z0, z1, z2)
U16(f116_out1, z0, z1, z2, z3) → f380_out1
U16(z0, f384_out1(z1), z2, z3, z4) → f380_out2(z1)
U16(z0, f384_out4(z1, z2), z3, z4, z5) → f380_out5(z1, z2)
f475_in(z0, z1) → U17(f116_in(z0, z1), f478_in(z0, z1), z0, z1)
U17(f116_out1, z0, z1, z2) → f475_out1
U17(z0, f478_out1(z1), z2, z3) → f475_out2(z1)
U17(z0, f478_out4(z1), z2, z3) → f475_out5(z1)
f562_in(z0, z1, z2) → U18(f116_in(z0, z1), f566_in(z0, z1, z2), z0, z1, z2)
U18(f116_out1, z0, z1, z2, z3) → f562_out1
U18(z0, f566_out1(z1), z2, z3, z4) → f562_out2(z1)
U18(z0, f566_out4(z1), z2, z3, z4) → f562_out5(z1)
Tuples:

F116_IN(z0, .(z0, [])) → c(F228_IN(z0))
F2_IN(z0, .(z0, z1)) → c1(F113_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c2(F2_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c3(F475_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c4(F2_IN(z0, z1))
F2_IN(z0, .(z1, z2)) → c5(F562_IN(z0, z2, z1))
F2_IN(z0, .(z1, z2)) → c6(F2_IN(z0, z2))
F116_IN(z0, .(z0, z1)) → c21(F323_IN(z0, z1))
F116_IN(z0, .(z1, z2)) → c22(F380_IN(z0, z2, z1))
F566_IN(z0, z1, z2) → c32(F2_IN(z0, z1))
F478_IN(z0, z1) → c34(F2_IN(z0, z1))
F118_IN(z0, z1) → c36(F2_IN(z0, z1))
F113_IN(z0, z1) → c38(F116_IN(z0, z1), F118_IN(z0, z1))
F228_IN(z0) → c42
F323_IN(z0, z1) → c46(F116_IN(z0, z1))
F380_IN(z0, z1, z2) → c50(F116_IN(z0, z1))
F475_IN(z0, z1) → c54(F116_IN(z0, z1), F478_IN(z0, z1))
F562_IN(z0, z1, z2) → c58(F116_IN(z0, z1), F566_IN(z0, z1, z2))
F116_IN(z0, .(z0, [])) → c
S tuples:

F116_IN(z0, .(z1, z2)) → c22(F380_IN(z0, z2, z1))
F323_IN(z0, z1) → c46(F116_IN(z0, z1))
K tuples:

F2_IN(z0, .(z0, z1)) → c1(F113_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c2(F2_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c3(F475_IN(z0, z1))
F2_IN(z0, .(z0, z1)) → c4(F2_IN(z0, z1))
F2_IN(z0, .(z1, z2)) → c5(F562_IN(z0, z2, z1))
F2_IN(z0, .(z1, z2)) → c6(F2_IN(z0, z2))
F475_IN(z0, z1) → c54(F116_IN(z0, z1), F478_IN(z0, z1))
F562_IN(z0, z1, z2) → c58(F116_IN(z0, z1), F566_IN(z0, z1, z2))
F566_IN(z0, z1, z2) → c32(F2_IN(z0, z1))
F478_IN(z0, z1) → c34(F2_IN(z0, z1))
F113_IN(z0, z1) → c38(F116_IN(z0, z1), F118_IN(z0, z1))
F118_IN(z0, z1) → c36(F2_IN(z0, z1))
F116_IN(z0, .(z0, [])) → c(F228_IN(z0))
F116_IN(z0, .(z0, [])) → c
F228_IN(z0) → c42
F116_IN(z0, .(z0, z1)) → c21(F323_IN(z0, z1))
F380_IN(z0, z1, z2) → c50(F116_IN(z0, z1))
Defined Rule Symbols:

f2_in, U1, U2, U3, U4, U5, U6, f116_in, U7, U8, U9, f566_in, U10, f478_in, U11, f118_in, U12, f113_in, U13, f228_in, U14, f323_in, U15, f380_in, U16, f475_in, U17, f562_in, U18

Defined Pair Symbols:

F116_IN, F2_IN, F566_IN, F478_IN, F118_IN, F113_IN, F228_IN, F323_IN, F380_IN, F475_IN, F562_IN

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c21, c22, c32, c34, c36, c38, c42, c46, c50, c54, c58, c

(31) CdtKnowledgeProof (EQUIVALENT transformation)

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

F323_IN(z0, z1) → c46(F116_IN(z0, z1))
F116_IN(z0, .(z0, [])) → c(F228_IN(z0))
F116_IN(z0, .(z0, z1)) → c21(F323_IN(z0, z1))
F116_IN(z0, .(z1, z2)) → c22(F380_IN(z0, z2, z1))
F116_IN(z0, .(z0, [])) → c
F380_IN(z0, z1, z2) → c50(F116_IN(z0, z1))
Now S is empty

(32) BOUNDS(O(1), O(1))