YES(O(1), O(n^1)) 10.95/3.28 YES(O(1), O(n^1)) 11.32/3.36 11.32/3.36 11.32/3.36 11.32/3.36 11.32/3.36 11.32/3.36 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 11.32/3.36 11.32/3.36 11.32/3.36
11.32/3.36
11.32/3.36
11.32/3.36
The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

0 CpxTRS
11.32/3.36 
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
11.32/3.36 
↳2 CdtProblem
11.32/3.36 
↳3 CdtUnreachableProof (⇔)
11.32/3.36 
↳4 CdtProblem
11.32/3.36 
↳5 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
11.32/3.36 
↳6 CdtProblem
11.32/3.36 
↳7 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
11.32/3.36 
↳8 CdtProblem
11.32/3.36 
↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
11.32/3.36 
↳10 CdtProblem
11.32/3.36 
↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
11.32/3.36 
↳12 CdtProblem
11.32/3.36 
↳13 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
11.32/3.36 
↳14 CdtProblem
11.32/3.36 
↳15 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
11.32/3.36 
↳16 CdtProblem
11.32/3.36 
↳17 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
11.32/3.36 
↳18 CdtProblem
11.32/3.36 
↳19 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
11.32/3.36 
↳20 CdtProblem
11.32/3.36 
↳21 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
11.32/3.36 
↳22 CdtProblem
11.32/3.36 
↳23 SIsEmptyProof (BOTH BOUNDS(ID, ID))
11.32/3.36 
↳24 BOUNDS(O(1), O(1))
11.32/3.36
11.32/3.36 11.32/3.36
11.32/3.36
11.32/3.36

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x)) 11.32/3.36
rec(sent(x)) → sent(rec(x)) 11.32/3.36
rec(no(x)) → sent(rec(x)) 11.32/3.36
rec(bot) → up(sent(bot)) 11.32/3.36
rec(up(x)) → up(rec(x)) 11.32/3.36
sent(up(x)) → up(sent(x)) 11.32/3.36
no(up(x)) → up(no(x)) 11.32/3.36
top(rec(up(x))) → top(check(rec(x))) 11.32/3.36
top(sent(up(x))) → top(check(rec(x))) 11.32/3.36
top(no(up(x))) → top(check(rec(x))) 11.32/3.36
check(up(x)) → up(check(x)) 11.32/3.36
check(sent(x)) → sent(check(x)) 11.32/3.36
check(rec(x)) → rec(check(x)) 11.32/3.36
check(no(x)) → no(check(x)) 11.32/3.36
check(no(x)) → no(x)

Rewrite Strategy: INNERMOST
11.32/3.36
11.32/3.36

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT
11.32/3.36
11.32/3.36

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

rec(rec(z0)) → sent(rec(z0)) 11.32/3.36
rec(sent(z0)) → sent(rec(z0)) 11.32/3.37
rec(no(z0)) → sent(rec(z0)) 11.32/3.37
rec(bot) → up(sent(bot)) 11.32/3.37
rec(up(z0)) → up(rec(z0)) 11.32/3.37
sent(up(z0)) → up(sent(z0)) 11.32/3.37
no(up(z0)) → up(no(z0)) 11.32/3.37
top(rec(up(z0))) → top(check(rec(z0))) 11.32/3.37
top(sent(up(z0))) → top(check(rec(z0))) 11.32/3.37
top(no(up(z0))) → top(check(rec(z0))) 11.32/3.37
check(up(z0)) → up(check(z0)) 11.32/3.37
check(sent(z0)) → sent(check(z0)) 11.32/3.37
check(rec(z0)) → rec(check(z0)) 11.32/3.37
check(no(z0)) → no(check(z0)) 11.32/3.37
check(no(z0)) → no(z0)
Tuples:

REC(rec(z0)) → c(SENT(rec(z0)), REC(z0)) 11.32/3.37
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0)) 11.32/3.37
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0)) 11.32/3.37
REC(bot) → c3(SENT(bot)) 11.32/3.37
REC(up(z0)) → c4(REC(z0)) 11.32/3.37
SENT(up(z0)) → c5(SENT(z0)) 11.32/3.37
NO(up(z0)) → c6(NO(z0)) 11.32/3.37
TOP(rec(up(z0))) → c7(TOP(check(rec(z0))), CHECK(rec(z0)), REC(z0)) 11.32/3.37
TOP(sent(up(z0))) → c8(TOP(check(rec(z0))), CHECK(rec(z0)), REC(z0)) 11.32/3.37
TOP(no(up(z0))) → c9(TOP(check(rec(z0))), CHECK(rec(z0)), REC(z0)) 11.32/3.37
CHECK(up(z0)) → c10(CHECK(z0)) 11.32/3.37
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0)) 11.32/3.37
CHECK(rec(z0)) → c12(REC(check(z0)), CHECK(z0)) 11.32/3.37
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0)) 11.32/3.37
CHECK(no(z0)) → c14(NO(z0))
S tuples:

REC(rec(z0)) → c(SENT(rec(z0)), REC(z0)) 11.32/3.37
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0)) 11.32/3.37
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0)) 11.32/3.37
REC(bot) → c3(SENT(bot)) 11.32/3.37
REC(up(z0)) → c4(REC(z0)) 11.32/3.37
SENT(up(z0)) → c5(SENT(z0)) 11.32/3.37
NO(up(z0)) → c6(NO(z0)) 11.32/3.37
TOP(rec(up(z0))) → c7(TOP(check(rec(z0))), CHECK(rec(z0)), REC(z0)) 11.32/3.37
TOP(sent(up(z0))) → c8(TOP(check(rec(z0))), CHECK(rec(z0)), REC(z0)) 11.32/3.37
TOP(no(up(z0))) → c9(TOP(check(rec(z0))), CHECK(rec(z0)), REC(z0)) 11.32/3.37
CHECK(up(z0)) → c10(CHECK(z0)) 11.32/3.37
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0)) 11.32/3.37
CHECK(rec(z0)) → c12(REC(check(z0)), CHECK(z0)) 11.32/3.37
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0)) 11.32/3.37
CHECK(no(z0)) → c14(NO(z0))
K tuples:none
Defined Rule Symbols:

rec, sent, no, top, check

Defined Pair Symbols:

REC, SENT, NO, TOP, CHECK

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14

11.32/3.37
11.32/3.37

(3) CdtUnreachableProof (EQUIVALENT transformation)

The following tuples could be removed as they are not reachable from basic start terms:

TOP(rec(up(z0))) → c7(TOP(check(rec(z0))), CHECK(rec(z0)), REC(z0)) 11.32/3.37
TOP(sent(up(z0))) → c8(TOP(check(rec(z0))), CHECK(rec(z0)), REC(z0)) 11.32/3.37
TOP(no(up(z0))) → c9(TOP(check(rec(z0))), CHECK(rec(z0)), REC(z0))
11.32/3.37
11.32/3.37

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

rec(rec(z0)) → sent(rec(z0)) 11.32/3.37
rec(sent(z0)) → sent(rec(z0)) 11.32/3.37
rec(no(z0)) → sent(rec(z0)) 11.32/3.37
rec(bot) → up(sent(bot)) 11.32/3.37
rec(up(z0)) → up(rec(z0)) 11.32/3.37
sent(up(z0)) → up(sent(z0)) 11.32/3.37
no(up(z0)) → up(no(z0)) 11.32/3.37
top(rec(up(z0))) → top(check(rec(z0))) 11.32/3.37
top(sent(up(z0))) → top(check(rec(z0))) 11.32/3.37
top(no(up(z0))) → top(check(rec(z0))) 11.32/3.37
check(up(z0)) → up(check(z0)) 11.32/3.37
check(sent(z0)) → sent(check(z0)) 11.32/3.37
check(rec(z0)) → rec(check(z0)) 11.32/3.37
check(no(z0)) → no(check(z0)) 11.32/3.37
check(no(z0)) → no(z0)
Tuples:

REC(bot) → c3(SENT(bot)) 11.32/3.37
REC(up(z0)) → c4(REC(z0)) 11.32/3.37
SENT(up(z0)) → c5(SENT(z0)) 11.32/3.37
NO(up(z0)) → c6(NO(z0)) 11.32/3.37
CHECK(up(z0)) → c10(CHECK(z0)) 11.32/3.37
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0)) 11.32/3.37
CHECK(rec(z0)) → c12(REC(check(z0)), CHECK(z0)) 11.32/3.37
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0)) 11.32/3.37
CHECK(no(z0)) → c14(NO(z0)) 11.32/3.37
REC(rec(z0)) → c(SENT(rec(z0)), REC(z0)) 11.32/3.37
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0)) 11.32/3.37
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0))
S tuples:

REC(rec(z0)) → c(SENT(rec(z0)), REC(z0)) 11.32/3.37
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0)) 11.32/3.37
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0)) 11.32/3.37
REC(bot) → c3(SENT(bot)) 11.32/3.37
REC(up(z0)) → c4(REC(z0)) 11.32/3.37
SENT(up(z0)) → c5(SENT(z0)) 11.32/3.37
NO(up(z0)) → c6(NO(z0)) 11.32/3.37
CHECK(up(z0)) → c10(CHECK(z0)) 11.32/3.37
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0)) 11.32/3.37
CHECK(rec(z0)) → c12(REC(check(z0)), CHECK(z0)) 11.32/3.37
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0)) 11.32/3.37
CHECK(no(z0)) → c14(NO(z0))
K tuples:none
Defined Rule Symbols:

rec, sent, no, top, check

Defined Pair Symbols:

REC, SENT, NO, CHECK

Compound Symbols:

c3, c4, c5, c6, c10, c11, c12, c13, c14, c, c1, c2

11.71/3.42
11.71/3.42

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

Removed 3 trailing tuple parts
11.71/3.42
11.71/3.42

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

rec(rec(z0)) → sent(rec(z0)) 11.71/3.42
rec(sent(z0)) → sent(rec(z0)) 11.71/3.42
rec(no(z0)) → sent(rec(z0)) 11.71/3.42
rec(bot) → up(sent(bot)) 11.71/3.42
rec(up(z0)) → up(rec(z0)) 11.71/3.42
sent(up(z0)) → up(sent(z0)) 11.71/3.42
no(up(z0)) → up(no(z0)) 11.71/3.42
top(rec(up(z0))) → top(check(rec(z0))) 11.71/3.42
top(sent(up(z0))) → top(check(rec(z0))) 11.71/3.42
top(no(up(z0))) → top(check(rec(z0))) 11.71/3.42
check(up(z0)) → up(check(z0)) 11.71/3.42
check(sent(z0)) → sent(check(z0)) 11.71/3.42
check(rec(z0)) → rec(check(z0)) 11.71/3.42
check(no(z0)) → no(check(z0)) 11.71/3.42
check(no(z0)) → no(z0)
Tuples:

REC(up(z0)) → c4(REC(z0)) 11.71/3.42
SENT(up(z0)) → c5(SENT(z0)) 11.71/3.42
NO(up(z0)) → c6(NO(z0)) 11.71/3.42
CHECK(up(z0)) → c10(CHECK(z0)) 11.71/3.42
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0)) 11.71/3.42
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0)) 11.71/3.42
CHECK(no(z0)) → c14(NO(z0)) 11.71/3.42
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0)) 11.71/3.42
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0)) 11.71/3.42
REC(bot) → c3 11.71/3.42
CHECK(rec(z0)) → c12(CHECK(z0)) 11.71/3.42
REC(rec(z0)) → c(REC(z0))
S tuples:

REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0)) 11.71/3.42
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0)) 11.71/3.42
REC(up(z0)) → c4(REC(z0)) 11.71/3.42
SENT(up(z0)) → c5(SENT(z0)) 11.71/3.42
NO(up(z0)) → c6(NO(z0)) 11.71/3.42
CHECK(up(z0)) → c10(CHECK(z0)) 11.71/3.42
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0)) 11.71/3.42
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0)) 11.71/3.42
CHECK(no(z0)) → c14(NO(z0)) 11.71/3.42
REC(bot) → c3 11.71/3.42
CHECK(rec(z0)) → c12(CHECK(z0)) 11.71/3.42
REC(rec(z0)) → c(REC(z0))
K tuples:none
Defined Rule Symbols:

rec, sent, no, top, check

Defined Pair Symbols:

REC, SENT, NO, CHECK

Compound Symbols:

c4, c5, c6, c10, c11, c13, c14, c1, c2, c3, c12, c

11.71/3.42
11.71/3.42

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

Removed 1 trailing nodes:

REC(bot) → c3
11.71/3.42
11.71/3.42

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

rec(rec(z0)) → sent(rec(z0)) 11.71/3.42
rec(sent(z0)) → sent(rec(z0)) 11.71/3.42
rec(no(z0)) → sent(rec(z0)) 11.71/3.42
rec(bot) → up(sent(bot)) 11.71/3.42
rec(up(z0)) → up(rec(z0)) 11.71/3.42
sent(up(z0)) → up(sent(z0)) 11.71/3.42
no(up(z0)) → up(no(z0)) 11.71/3.42
top(rec(up(z0))) → top(check(rec(z0))) 11.71/3.42
top(sent(up(z0))) → top(check(rec(z0))) 11.71/3.42
top(no(up(z0))) → top(check(rec(z0))) 11.71/3.42
check(up(z0)) → up(check(z0)) 11.71/3.42
check(sent(z0)) → sent(check(z0)) 11.71/3.42
check(rec(z0)) → rec(check(z0)) 11.71/3.42
check(no(z0)) → no(check(z0)) 11.71/3.42
check(no(z0)) → no(z0)
Tuples:

REC(up(z0)) → c4(REC(z0)) 11.71/3.42
SENT(up(z0)) → c5(SENT(z0)) 11.71/3.42
NO(up(z0)) → c6(NO(z0)) 11.71/3.42
CHECK(up(z0)) → c10(CHECK(z0)) 11.71/3.42
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0)) 11.71/3.42
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0)) 11.71/3.42
CHECK(no(z0)) → c14(NO(z0)) 11.71/3.42
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0)) 11.71/3.42
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0)) 11.71/3.42
REC(bot) → c3 11.71/3.42
CHECK(rec(z0)) → c12(CHECK(z0)) 11.71/3.42
REC(rec(z0)) → c(REC(z0))
S tuples:

REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0)) 11.71/3.42
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0)) 11.71/3.42
REC(up(z0)) → c4(REC(z0)) 11.71/3.42
SENT(up(z0)) → c5(SENT(z0)) 11.71/3.42
NO(up(z0)) → c6(NO(z0)) 11.71/3.42
CHECK(up(z0)) → c10(CHECK(z0)) 11.71/3.42
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0)) 11.71/3.42
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0)) 11.71/3.42
CHECK(no(z0)) → c14(NO(z0)) 11.71/3.42
REC(bot) → c3 11.71/3.42
CHECK(rec(z0)) → c12(CHECK(z0)) 11.71/3.42
REC(rec(z0)) → c(REC(z0))
K tuples:none
Defined Rule Symbols:

rec, sent, no, top, check

Defined Pair Symbols:

REC, SENT, NO, CHECK

Compound Symbols:

c4, c5, c6, c10, c11, c13, c14, c1, c2, c3, c12, c

11.71/3.42
11.71/3.42

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

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

CHECK(no(z0)) → c14(NO(z0)) 11.71/3.42
REC(bot) → c3
We considered the (Usable) Rules:

rec(rec(z0)) → sent(rec(z0)) 11.71/3.42
rec(sent(z0)) → sent(rec(z0)) 11.71/3.42
rec(no(z0)) → sent(rec(z0)) 11.71/3.42
rec(bot) → up(sent(bot)) 11.71/3.42
sent(up(z0)) → up(sent(z0)) 11.71/3.42
check(sent(z0)) → sent(check(z0)) 11.71/3.42
check(rec(z0)) → rec(check(z0)) 11.71/3.42
check(no(z0)) → no(check(z0)) 11.71/3.42
check(no(z0)) → no(z0) 11.71/3.42
no(up(z0)) → up(no(z0))
And the Tuples:

REC(up(z0)) → c4(REC(z0)) 11.71/3.42
SENT(up(z0)) → c5(SENT(z0)) 11.71/3.42
NO(up(z0)) → c6(NO(z0)) 11.71/3.42
CHECK(up(z0)) → c10(CHECK(z0)) 11.71/3.42
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0)) 11.71/3.42
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0)) 11.71/3.42
CHECK(no(z0)) → c14(NO(z0)) 11.71/3.42
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0)) 11.71/3.42
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0)) 11.71/3.42
REC(bot) → c3 11.71/3.42
CHECK(rec(z0)) → c12(CHECK(z0)) 11.71/3.42
REC(rec(z0)) → c(REC(z0))
The order we found is given by the following interpretation:
Polynomial interpretation : 11.71/3.42

POL(CHECK(x1)) = [1]    11.71/3.42
POL(NO(x1)) = 0    11.71/3.42
POL(REC(x1)) = [3]    11.71/3.42
POL(SENT(x1)) = 0    11.71/3.42
POL(bot) = 0    11.71/3.42
POL(c(x1)) = x1    11.71/3.42
POL(c1(x1, x2)) = x1 + x2    11.71/3.42
POL(c10(x1)) = x1    11.71/3.42
POL(c11(x1, x2)) = x1 + x2    11.71/3.42
POL(c12(x1)) = x1    11.71/3.42
POL(c13(x1, x2)) = x1 + x2    11.71/3.42
POL(c14(x1)) = x1    11.71/3.42
POL(c2(x1, x2)) = x1 + x2    11.71/3.42
POL(c3) = 0    11.71/3.42
POL(c4(x1)) = x1    11.71/3.42
POL(c5(x1)) = x1    11.71/3.42
POL(c6(x1)) = x1    11.71/3.42
POL(check(x1)) = 0    11.71/3.42
POL(no(x1)) = [4]    11.71/3.42
POL(rec(x1)) = [3]x1    11.71/3.42
POL(sent(x1)) = 0    11.71/3.42
POL(up(x1)) = 0   
11.71/3.42
11.71/3.42

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

rec(rec(z0)) → sent(rec(z0)) 11.71/3.42
rec(sent(z0)) → sent(rec(z0)) 11.71/3.42
rec(no(z0)) → sent(rec(z0)) 11.71/3.42
rec(bot) → up(sent(bot)) 11.71/3.42
rec(up(z0)) → up(rec(z0)) 11.71/3.42
sent(up(z0)) → up(sent(z0)) 11.71/3.42
no(up(z0)) → up(no(z0)) 11.71/3.42
top(rec(up(z0))) → top(check(rec(z0))) 11.71/3.42
top(sent(up(z0))) → top(check(rec(z0))) 11.71/3.42
top(no(up(z0))) → top(check(rec(z0))) 11.71/3.42
check(up(z0)) → up(check(z0)) 11.71/3.42
check(sent(z0)) → sent(check(z0)) 11.71/3.42
check(rec(z0)) → rec(check(z0)) 11.71/3.42
check(no(z0)) → no(check(z0)) 11.71/3.42
check(no(z0)) → no(z0)
Tuples:

REC(up(z0)) → c4(REC(z0)) 11.71/3.42
SENT(up(z0)) → c5(SENT(z0)) 11.71/3.42
NO(up(z0)) → c6(NO(z0)) 11.71/3.42
CHECK(up(z0)) → c10(CHECK(z0)) 11.71/3.42
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0)) 11.71/3.42
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0)) 11.71/3.42
CHECK(no(z0)) → c14(NO(z0)) 11.71/3.42
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0)) 11.71/3.42
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0)) 11.71/3.42
REC(bot) → c3 11.71/3.42
CHECK(rec(z0)) → c12(CHECK(z0)) 11.71/3.42
REC(rec(z0)) → c(REC(z0))
S tuples:

REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0)) 11.71/3.42
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0)) 11.71/3.42
REC(up(z0)) → c4(REC(z0)) 11.71/3.42
SENT(up(z0)) → c5(SENT(z0)) 11.71/3.42
NO(up(z0)) → c6(NO(z0)) 11.71/3.42
CHECK(up(z0)) → c10(CHECK(z0)) 11.71/3.42
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0)) 11.71/3.42
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0)) 11.71/3.42
CHECK(rec(z0)) → c12(CHECK(z0)) 11.71/3.42
REC(rec(z0)) → c(REC(z0))
K tuples:

CHECK(no(z0)) → c14(NO(z0)) 11.71/3.42
REC(bot) → c3
Defined Rule Symbols:

rec, sent, no, top, check

Defined Pair Symbols:

REC, SENT, NO, CHECK

Compound Symbols:

c4, c5, c6, c10, c11, c13, c14, c1, c2, c3, c12, c

11.71/3.42
11.71/3.42

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

REC(rec(z0)) → c(REC(z0))
We considered the (Usable) Rules:

rec(rec(z0)) → sent(rec(z0)) 11.71/3.42
rec(sent(z0)) → sent(rec(z0)) 11.71/3.42
rec(no(z0)) → sent(rec(z0)) 11.71/3.42
rec(bot) → up(sent(bot)) 11.71/3.42
sent(up(z0)) → up(sent(z0)) 11.71/3.42
check(sent(z0)) → sent(check(z0)) 11.71/3.42
check(rec(z0)) → rec(check(z0)) 11.71/3.42
check(no(z0)) → no(check(z0)) 11.71/3.42
check(no(z0)) → no(z0) 11.71/3.42
no(up(z0)) → up(no(z0))
And the Tuples:

REC(up(z0)) → c4(REC(z0)) 11.71/3.42
SENT(up(z0)) → c5(SENT(z0)) 11.71/3.42
NO(up(z0)) → c6(NO(z0)) 11.71/3.42
CHECK(up(z0)) → c10(CHECK(z0)) 11.71/3.42
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0)) 11.71/3.42
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0)) 11.71/3.42
CHECK(no(z0)) → c14(NO(z0)) 11.71/3.42
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0)) 11.71/3.42
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0)) 11.71/3.42
REC(bot) → c3 11.71/3.42
CHECK(rec(z0)) → c12(CHECK(z0)) 11.71/3.42
REC(rec(z0)) → c(REC(z0))
The order we found is given by the following interpretation:
Polynomial interpretation : 11.71/3.42

POL(CHECK(x1)) = [1]    11.71/3.42
POL(NO(x1)) = 0    11.71/3.42
POL(REC(x1)) = [2]x1    11.71/3.42
POL(SENT(x1)) = 0    11.71/3.42
POL(bot) = [4]    11.71/3.42
POL(c(x1)) = x1    11.71/3.42
POL(c1(x1, x2)) = x1 + x2    11.71/3.42
POL(c10(x1)) = x1    11.71/3.42
POL(c11(x1, x2)) = x1 + x2    11.71/3.42
POL(c12(x1)) = x1    11.71/3.42
POL(c13(x1, x2)) = x1 + x2    11.71/3.42
POL(c14(x1)) = x1    11.71/3.42
POL(c2(x1, x2)) = x1 + x2    11.71/3.42
POL(c3) = 0    11.71/3.42
POL(c4(x1)) = x1    11.71/3.42
POL(c5(x1)) = x1    11.71/3.42
POL(c6(x1)) = x1    11.71/3.42
POL(check(x1)) = [4]x1    11.71/3.42
POL(no(x1)) = [4]x1    11.71/3.42
POL(rec(x1)) = [2] + [4]x1    11.71/3.42
POL(sent(x1)) = x1    11.71/3.42
POL(up(x1)) = x1   
11.71/3.42
11.71/3.42

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

rec(rec(z0)) → sent(rec(z0)) 11.71/3.42
rec(sent(z0)) → sent(rec(z0)) 11.71/3.42
rec(no(z0)) → sent(rec(z0)) 11.71/3.42
rec(bot) → up(sent(bot)) 11.71/3.42
rec(up(z0)) → up(rec(z0)) 11.71/3.42
sent(up(z0)) → up(sent(z0)) 11.71/3.42
no(up(z0)) → up(no(z0)) 11.71/3.42
top(rec(up(z0))) → top(check(rec(z0))) 11.71/3.42
top(sent(up(z0))) → top(check(rec(z0))) 11.71/3.42
top(no(up(z0))) → top(check(rec(z0))) 11.71/3.42
check(up(z0)) → up(check(z0)) 11.71/3.42
check(sent(z0)) → sent(check(z0)) 11.71/3.42
check(rec(z0)) → rec(check(z0)) 11.71/3.42
check(no(z0)) → no(check(z0)) 11.71/3.42
check(no(z0)) → no(z0)
Tuples:

REC(up(z0)) → c4(REC(z0)) 11.71/3.42
SENT(up(z0)) → c5(SENT(z0)) 11.71/3.42
NO(up(z0)) → c6(NO(z0)) 11.71/3.42
CHECK(up(z0)) → c10(CHECK(z0)) 11.71/3.42
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0)) 11.71/3.42
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0)) 11.71/3.42
CHECK(no(z0)) → c14(NO(z0)) 11.71/3.42
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0)) 11.71/3.42
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0)) 11.71/3.42
REC(bot) → c3 11.71/3.42
CHECK(rec(z0)) → c12(CHECK(z0)) 11.71/3.42
REC(rec(z0)) → c(REC(z0))
S tuples:

REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0)) 11.71/3.42
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0)) 11.71/3.42
REC(up(z0)) → c4(REC(z0)) 11.71/3.42
SENT(up(z0)) → c5(SENT(z0)) 11.71/3.42
NO(up(z0)) → c6(NO(z0)) 11.71/3.42
CHECK(up(z0)) → c10(CHECK(z0)) 11.71/3.42
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0)) 11.71/3.42
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0)) 11.71/3.42
CHECK(rec(z0)) → c12(CHECK(z0))
K tuples:

CHECK(no(z0)) → c14(NO(z0)) 11.71/3.42
REC(bot) → c3 11.71/3.42
REC(rec(z0)) → c(REC(z0))
Defined Rule Symbols:

rec, sent, no, top, check

Defined Pair Symbols:

REC, SENT, NO, CHECK

Compound Symbols:

c4, c5, c6, c10, c11, c13, c14, c1, c2, c3, c12, c

11.71/3.42
11.71/3.42

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

CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0)) 11.71/3.42
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0)) 11.71/3.42
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0)) 11.71/3.42
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0)) 11.71/3.42
CHECK(rec(z0)) → c12(CHECK(z0))
We considered the (Usable) Rules:

rec(rec(z0)) → sent(rec(z0)) 11.71/3.42
rec(sent(z0)) → sent(rec(z0)) 11.71/3.42
rec(no(z0)) → sent(rec(z0)) 11.71/3.42
rec(bot) → up(sent(bot)) 11.71/3.42
sent(up(z0)) → up(sent(z0)) 11.71/3.42
check(sent(z0)) → sent(check(z0)) 11.71/3.42
check(rec(z0)) → rec(check(z0)) 11.71/3.42
check(no(z0)) → no(check(z0)) 11.71/3.42
check(no(z0)) → no(z0) 11.71/3.42
no(up(z0)) → up(no(z0))
And the Tuples:

REC(up(z0)) → c4(REC(z0)) 11.71/3.42
SENT(up(z0)) → c5(SENT(z0)) 11.71/3.42
NO(up(z0)) → c6(NO(z0)) 11.71/3.42
CHECK(up(z0)) → c10(CHECK(z0)) 11.71/3.42
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0)) 11.71/3.42
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0)) 11.71/3.42
CHECK(no(z0)) → c14(NO(z0)) 11.71/3.42
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0)) 11.71/3.42
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0)) 11.71/3.42
REC(bot) → c3 11.71/3.42
CHECK(rec(z0)) → c12(CHECK(z0)) 11.71/3.42
REC(rec(z0)) → c(REC(z0))
The order we found is given by the following interpretation:
Polynomial interpretation : 11.71/3.42

POL(CHECK(x1)) = [1] + x1    11.71/3.42
POL(NO(x1)) = 0    11.71/3.42
POL(REC(x1)) = [4]x1    11.71/3.42
POL(SENT(x1)) = [1]    11.71/3.42
POL(bot) = [4]    11.71/3.42
POL(c(x1)) = x1    11.71/3.42
POL(c1(x1, x2)) = x1 + x2    11.71/3.42
POL(c10(x1)) = x1    11.71/3.42
POL(c11(x1, x2)) = x1 + x2    11.71/3.42
POL(c12(x1)) = x1    11.71/3.42
POL(c13(x1, x2)) = x1 + x2    11.71/3.42
POL(c14(x1)) = x1    11.71/3.42
POL(c2(x1, x2)) = x1 + x2    11.71/3.42
POL(c3) = 0    11.71/3.42
POL(c4(x1)) = x1    11.71/3.42
POL(c5(x1)) = x1    11.71/3.42
POL(c6(x1)) = x1    11.71/3.42
POL(check(x1)) = 0    11.71/3.42
POL(no(x1)) = [2] + [5]x1    11.71/3.42
POL(rec(x1)) = [2] + [4]x1    11.71/3.42
POL(sent(x1)) = [4] + [2]x1    11.71/3.42
POL(up(x1)) = x1   
11.71/3.42
11.71/3.42

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

rec(rec(z0)) → sent(rec(z0)) 11.71/3.42
rec(sent(z0)) → sent(rec(z0)) 11.71/3.42
rec(no(z0)) → sent(rec(z0)) 11.71/3.42
rec(bot) → up(sent(bot)) 11.71/3.42
rec(up(z0)) → up(rec(z0)) 11.71/3.42
sent(up(z0)) → up(sent(z0)) 11.71/3.42
no(up(z0)) → up(no(z0)) 11.71/3.42
top(rec(up(z0))) → top(check(rec(z0))) 11.71/3.42
top(sent(up(z0))) → top(check(rec(z0))) 11.71/3.42
top(no(up(z0))) → top(check(rec(z0))) 11.71/3.42
check(up(z0)) → up(check(z0)) 11.71/3.42
check(sent(z0)) → sent(check(z0)) 11.71/3.42
check(rec(z0)) → rec(check(z0)) 11.71/3.42
check(no(z0)) → no(check(z0)) 11.71/3.42
check(no(z0)) → no(z0)
Tuples:

REC(up(z0)) → c4(REC(z0)) 11.71/3.42
SENT(up(z0)) → c5(SENT(z0)) 11.71/3.42
NO(up(z0)) → c6(NO(z0)) 11.71/3.42
CHECK(up(z0)) → c10(CHECK(z0)) 11.71/3.42
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0)) 11.71/3.42
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0)) 11.71/3.42
CHECK(no(z0)) → c14(NO(z0)) 11.71/3.42
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0)) 11.71/3.42
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0)) 11.71/3.42
REC(bot) → c3 11.71/3.42
CHECK(rec(z0)) → c12(CHECK(z0)) 11.71/3.42
REC(rec(z0)) → c(REC(z0))
S tuples:

REC(up(z0)) → c4(REC(z0)) 11.71/3.42
SENT(up(z0)) → c5(SENT(z0)) 11.71/3.42
NO(up(z0)) → c6(NO(z0)) 11.71/3.42
CHECK(up(z0)) → c10(CHECK(z0))
K tuples:

CHECK(no(z0)) → c14(NO(z0)) 11.71/3.42
REC(bot) → c3 11.71/3.42
REC(rec(z0)) → c(REC(z0)) 11.71/3.42
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0)) 11.71/3.42
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0)) 11.71/3.42
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0)) 11.71/3.42
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0)) 11.71/3.42
CHECK(rec(z0)) → c12(CHECK(z0))
Defined Rule Symbols:

rec, sent, no, top, check

Defined Pair Symbols:

REC, SENT, NO, CHECK

Compound Symbols:

c4, c5, c6, c10, c11, c13, c14, c1, c2, c3, c12, c

11.71/3.42
11.71/3.42

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

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

REC(up(z0)) → c4(REC(z0))
We considered the (Usable) Rules:

rec(rec(z0)) → sent(rec(z0)) 11.71/3.42
rec(sent(z0)) → sent(rec(z0)) 11.71/3.42
rec(no(z0)) → sent(rec(z0)) 11.71/3.42
rec(bot) → up(sent(bot)) 11.71/3.42
sent(up(z0)) → up(sent(z0)) 11.71/3.42
check(sent(z0)) → sent(check(z0)) 11.71/3.42
check(rec(z0)) → rec(check(z0)) 11.71/3.42
check(no(z0)) → no(check(z0)) 11.71/3.42
check(no(z0)) → no(z0) 11.71/3.42
no(up(z0)) → up(no(z0))
And the Tuples:

REC(up(z0)) → c4(REC(z0)) 11.71/3.42
SENT(up(z0)) → c5(SENT(z0)) 11.71/3.42
NO(up(z0)) → c6(NO(z0)) 11.71/3.42
CHECK(up(z0)) → c10(CHECK(z0)) 11.71/3.42
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0)) 11.71/3.42
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0)) 11.71/3.42
CHECK(no(z0)) → c14(NO(z0)) 11.71/3.42
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0)) 11.71/3.42
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0)) 11.71/3.42
REC(bot) → c3 11.71/3.42
CHECK(rec(z0)) → c12(CHECK(z0)) 11.71/3.42
REC(rec(z0)) → c(REC(z0))
The order we found is given by the following interpretation:
Polynomial interpretation : 11.71/3.42

POL(CHECK(x1)) = 0    11.71/3.42
POL(NO(x1)) = 0    11.71/3.42
POL(REC(x1)) = [4]x1    11.71/3.42
POL(SENT(x1)) = 0    11.71/3.42
POL(bot) = [3]    11.71/3.42
POL(c(x1)) = x1    11.71/3.42
POL(c1(x1, x2)) = x1 + x2    11.71/3.42
POL(c10(x1)) = x1    11.71/3.42
POL(c11(x1, x2)) = x1 + x2    11.71/3.42
POL(c12(x1)) = x1    11.71/3.42
POL(c13(x1, x2)) = x1 + x2    11.71/3.42
POL(c14(x1)) = x1    11.71/3.42
POL(c2(x1, x2)) = x1 + x2    11.71/3.42
POL(c3) = 0    11.71/3.42
POL(c4(x1)) = x1    11.71/3.42
POL(c5(x1)) = x1    11.71/3.42
POL(c6(x1)) = x1    11.71/3.42
POL(check(x1)) = x1    11.71/3.42
POL(no(x1)) = [4]x1    11.71/3.42
POL(rec(x1)) = x1    11.71/3.42
POL(sent(x1)) = [4]x1    11.71/3.42
POL(up(x1)) = [4] + x1   
11.71/3.42
11.71/3.42

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

rec(rec(z0)) → sent(rec(z0)) 11.71/3.42
rec(sent(z0)) → sent(rec(z0)) 11.71/3.42
rec(no(z0)) → sent(rec(z0)) 11.71/3.42
rec(bot) → up(sent(bot)) 11.71/3.42
rec(up(z0)) → up(rec(z0)) 11.71/3.42
sent(up(z0)) → up(sent(z0)) 11.71/3.42
no(up(z0)) → up(no(z0)) 11.71/3.42
top(rec(up(z0))) → top(check(rec(z0))) 11.71/3.42
top(sent(up(z0))) → top(check(rec(z0))) 11.71/3.42
top(no(up(z0))) → top(check(rec(z0))) 11.71/3.42
check(up(z0)) → up(check(z0)) 11.71/3.42
check(sent(z0)) → sent(check(z0)) 11.71/3.42
check(rec(z0)) → rec(check(z0)) 11.71/3.42
check(no(z0)) → no(check(z0)) 11.71/3.42
check(no(z0)) → no(z0)
Tuples:

REC(up(z0)) → c4(REC(z0)) 11.71/3.42
SENT(up(z0)) → c5(SENT(z0)) 11.71/3.43
NO(up(z0)) → c6(NO(z0)) 11.71/3.43
CHECK(up(z0)) → c10(CHECK(z0)) 11.71/3.43
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0)) 11.71/3.43
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0)) 11.71/3.43
CHECK(no(z0)) → c14(NO(z0)) 11.71/3.43
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0)) 11.71/3.43
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0)) 11.71/3.43
REC(bot) → c3 11.71/3.43
CHECK(rec(z0)) → c12(CHECK(z0)) 11.71/3.43
REC(rec(z0)) → c(REC(z0))
S tuples:

SENT(up(z0)) → c5(SENT(z0)) 11.71/3.43
NO(up(z0)) → c6(NO(z0)) 11.71/3.43
CHECK(up(z0)) → c10(CHECK(z0))
K tuples:

CHECK(no(z0)) → c14(NO(z0)) 11.71/3.43
REC(bot) → c3 11.71/3.43
REC(rec(z0)) → c(REC(z0)) 11.71/3.43
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0)) 11.71/3.43
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0)) 11.71/3.43
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0)) 11.71/3.43
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0)) 11.71/3.43
CHECK(rec(z0)) → c12(CHECK(z0)) 11.71/3.43
REC(up(z0)) → c4(REC(z0))
Defined Rule Symbols:

rec, sent, no, top, check

Defined Pair Symbols:

REC, SENT, NO, CHECK

Compound Symbols:

c4, c5, c6, c10, c11, c13, c14, c1, c2, c3, c12, c

11.71/3.43
11.71/3.43

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

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

CHECK(up(z0)) → c10(CHECK(z0))
We considered the (Usable) Rules:

rec(rec(z0)) → sent(rec(z0)) 11.71/3.43
rec(sent(z0)) → sent(rec(z0)) 11.71/3.43
rec(no(z0)) → sent(rec(z0)) 11.71/3.43
rec(bot) → up(sent(bot)) 11.71/3.43
sent(up(z0)) → up(sent(z0)) 11.71/3.43
check(sent(z0)) → sent(check(z0)) 11.71/3.43
check(rec(z0)) → rec(check(z0)) 11.71/3.43
check(no(z0)) → no(check(z0)) 11.71/3.43
check(no(z0)) → no(z0) 11.71/3.43
no(up(z0)) → up(no(z0))
And the Tuples:

REC(up(z0)) → c4(REC(z0)) 11.71/3.43
SENT(up(z0)) → c5(SENT(z0)) 11.71/3.43
NO(up(z0)) → c6(NO(z0)) 11.71/3.43
CHECK(up(z0)) → c10(CHECK(z0)) 11.71/3.43
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0)) 11.71/3.43
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0)) 11.71/3.43
CHECK(no(z0)) → c14(NO(z0)) 11.71/3.43
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0)) 11.71/3.43
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0)) 11.71/3.43
REC(bot) → c3 11.71/3.43
CHECK(rec(z0)) → c12(CHECK(z0)) 11.71/3.43
REC(rec(z0)) → c(REC(z0))
The order we found is given by the following interpretation:
Polynomial interpretation : 11.71/3.43

POL(CHECK(x1)) = [1] + [4]x1    11.71/3.43
POL(NO(x1)) = [2]    11.71/3.43
POL(REC(x1)) = 0    11.71/3.43
POL(SENT(x1)) = 0    11.71/3.43
POL(bot) = [4]    11.71/3.43
POL(c(x1)) = x1    11.71/3.43
POL(c1(x1, x2)) = x1 + x2    11.71/3.43
POL(c10(x1)) = x1    11.71/3.43
POL(c11(x1, x2)) = x1 + x2    11.71/3.43
POL(c12(x1)) = x1    11.71/3.43
POL(c13(x1, x2)) = x1 + x2    11.71/3.43
POL(c14(x1)) = x1    11.71/3.43
POL(c2(x1, x2)) = x1 + x2    11.71/3.43
POL(c3) = 0    11.71/3.43
POL(c4(x1)) = x1    11.71/3.43
POL(c5(x1)) = x1    11.71/3.43
POL(c6(x1)) = x1    11.71/3.43
POL(check(x1)) = [4]x1    11.71/3.43
POL(no(x1)) = [3] + [2]x1    11.71/3.43
POL(rec(x1)) = [2] + [4]x1    11.71/3.43
POL(sent(x1)) = [3] + [2]x1    11.71/3.43
POL(up(x1)) = [1] + x1   
11.71/3.43
11.71/3.43

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

rec(rec(z0)) → sent(rec(z0)) 11.71/3.43
rec(sent(z0)) → sent(rec(z0)) 11.71/3.43
rec(no(z0)) → sent(rec(z0)) 11.71/3.43
rec(bot) → up(sent(bot)) 11.71/3.43
rec(up(z0)) → up(rec(z0)) 11.71/3.43
sent(up(z0)) → up(sent(z0)) 11.71/3.43
no(up(z0)) → up(no(z0)) 11.71/3.43
top(rec(up(z0))) → top(check(rec(z0))) 11.71/3.43
top(sent(up(z0))) → top(check(rec(z0))) 11.71/3.43
top(no(up(z0))) → top(check(rec(z0))) 11.71/3.43
check(up(z0)) → up(check(z0)) 11.71/3.43
check(sent(z0)) → sent(check(z0)) 11.71/3.43
check(rec(z0)) → rec(check(z0)) 11.71/3.43
check(no(z0)) → no(check(z0)) 11.71/3.43
check(no(z0)) → no(z0)
Tuples:

REC(up(z0)) → c4(REC(z0)) 11.71/3.43
SENT(up(z0)) → c5(SENT(z0)) 11.71/3.43
NO(up(z0)) → c6(NO(z0)) 11.71/3.43
CHECK(up(z0)) → c10(CHECK(z0)) 11.71/3.43
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0)) 11.71/3.43
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0)) 11.71/3.43
CHECK(no(z0)) → c14(NO(z0)) 11.71/3.43
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0)) 11.71/3.43
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0)) 11.71/3.43
REC(bot) → c3 11.71/3.43
CHECK(rec(z0)) → c12(CHECK(z0)) 11.71/3.43
REC(rec(z0)) → c(REC(z0))
S tuples:

SENT(up(z0)) → c5(SENT(z0)) 11.71/3.43
NO(up(z0)) → c6(NO(z0))
K tuples:

CHECK(no(z0)) → c14(NO(z0)) 11.71/3.43
REC(bot) → c3 11.71/3.43
REC(rec(z0)) → c(REC(z0)) 11.71/3.43
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0)) 11.71/3.43
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0)) 11.71/3.43
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0)) 11.71/3.43
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0)) 11.71/3.43
CHECK(rec(z0)) → c12(CHECK(z0)) 11.71/3.43
REC(up(z0)) → c4(REC(z0)) 11.71/3.43
CHECK(up(z0)) → c10(CHECK(z0))
Defined Rule Symbols:

rec, sent, no, top, check

Defined Pair Symbols:

REC, SENT, NO, CHECK

Compound Symbols:

c4, c5, c6, c10, c11, c13, c14, c1, c2, c3, c12, c

11.71/3.43
11.71/3.43

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

SENT(up(z0)) → c5(SENT(z0))
We considered the (Usable) Rules:

rec(rec(z0)) → sent(rec(z0)) 11.71/3.43
rec(sent(z0)) → sent(rec(z0)) 11.71/3.43
rec(no(z0)) → sent(rec(z0)) 11.71/3.43
rec(bot) → up(sent(bot)) 11.71/3.43
sent(up(z0)) → up(sent(z0)) 11.71/3.43
check(sent(z0)) → sent(check(z0)) 11.71/3.43
check(rec(z0)) → rec(check(z0)) 11.71/3.43
check(no(z0)) → no(check(z0)) 11.71/3.43
check(no(z0)) → no(z0) 11.71/3.43
no(up(z0)) → up(no(z0))
And the Tuples:

REC(up(z0)) → c4(REC(z0)) 11.71/3.43
SENT(up(z0)) → c5(SENT(z0)) 11.71/3.43
NO(up(z0)) → c6(NO(z0)) 11.71/3.43
CHECK(up(z0)) → c10(CHECK(z0)) 11.71/3.43
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0)) 11.71/3.43
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0)) 11.71/3.43
CHECK(no(z0)) → c14(NO(z0)) 11.71/3.43
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0)) 11.71/3.43
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0)) 11.71/3.43
REC(bot) → c3 11.71/3.43
CHECK(rec(z0)) → c12(CHECK(z0)) 11.71/3.43
REC(rec(z0)) → c(REC(z0))
The order we found is given by the following interpretation:
Polynomial interpretation : 11.71/3.43

POL(CHECK(x1)) = [1] + [5]x1    11.71/3.43
POL(NO(x1)) = [2]    11.71/3.43
POL(REC(x1)) = [4]x1    11.71/3.43
POL(SENT(x1)) = [4] + x1    11.71/3.43
POL(bot) = [4]    11.71/3.43
POL(c(x1)) = x1    11.71/3.43
POL(c1(x1, x2)) = x1 + x2    11.71/3.43
POL(c10(x1)) = x1    11.71/3.43
POL(c11(x1, x2)) = x1 + x2    11.71/3.43
POL(c12(x1)) = x1    11.71/3.43
POL(c13(x1, x2)) = x1 + x2    11.71/3.43
POL(c14(x1)) = x1    11.71/3.43
POL(c2(x1, x2)) = x1 + x2    11.71/3.43
POL(c3) = 0    11.71/3.43
POL(c4(x1)) = x1    11.71/3.43
POL(c5(x1)) = x1    11.71/3.43
POL(c6(x1)) = x1    11.71/3.43
POL(check(x1)) = [2] + [4]x1    11.71/3.43
POL(no(x1)) = [4] + [4]x1    11.71/3.43
POL(rec(x1)) = [2] + [4]x1    11.71/3.43
POL(sent(x1)) = [3] + [2]x1    11.71/3.43
POL(up(x1)) = [1] + x1   
11.71/3.43
11.71/3.43

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

rec(rec(z0)) → sent(rec(z0)) 11.71/3.43
rec(sent(z0)) → sent(rec(z0)) 11.71/3.43
rec(no(z0)) → sent(rec(z0)) 11.71/3.43
rec(bot) → up(sent(bot)) 11.71/3.43
rec(up(z0)) → up(rec(z0)) 11.71/3.43
sent(up(z0)) → up(sent(z0)) 11.71/3.43
no(up(z0)) → up(no(z0)) 11.71/3.43
top(rec(up(z0))) → top(check(rec(z0))) 11.71/3.43
top(sent(up(z0))) → top(check(rec(z0))) 11.71/3.43
top(no(up(z0))) → top(check(rec(z0))) 11.71/3.43
check(up(z0)) → up(check(z0)) 11.71/3.43
check(sent(z0)) → sent(check(z0)) 11.71/3.43
check(rec(z0)) → rec(check(z0)) 11.71/3.43
check(no(z0)) → no(check(z0)) 11.71/3.43
check(no(z0)) → no(z0)
Tuples:

REC(up(z0)) → c4(REC(z0)) 11.71/3.43
SENT(up(z0)) → c5(SENT(z0)) 11.71/3.43
NO(up(z0)) → c6(NO(z0)) 11.71/3.43
CHECK(up(z0)) → c10(CHECK(z0)) 11.71/3.43
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0)) 11.71/3.43
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0)) 11.71/3.43
CHECK(no(z0)) → c14(NO(z0)) 11.71/3.43
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0)) 11.71/3.43
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0)) 11.71/3.43
REC(bot) → c3 11.71/3.43
CHECK(rec(z0)) → c12(CHECK(z0)) 11.71/3.43
REC(rec(z0)) → c(REC(z0))
S tuples:

NO(up(z0)) → c6(NO(z0))
K tuples:

CHECK(no(z0)) → c14(NO(z0)) 11.71/3.43
REC(bot) → c3 11.71/3.43
REC(rec(z0)) → c(REC(z0)) 11.71/3.43
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0)) 11.71/3.43
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0)) 11.71/3.43
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0)) 11.71/3.44
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0)) 11.71/3.44
CHECK(rec(z0)) → c12(CHECK(z0)) 11.71/3.44
REC(up(z0)) → c4(REC(z0)) 11.71/3.44
CHECK(up(z0)) → c10(CHECK(z0)) 11.71/3.44
SENT(up(z0)) → c5(SENT(z0))
Defined Rule Symbols:

rec, sent, no, top, check

Defined Pair Symbols:

REC, SENT, NO, CHECK

Compound Symbols:

c4, c5, c6, c10, c11, c13, c14, c1, c2, c3, c12, c

11.71/3.44
11.71/3.44

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

NO(up(z0)) → c6(NO(z0))
We considered the (Usable) Rules:

rec(rec(z0)) → sent(rec(z0)) 11.71/3.44
rec(sent(z0)) → sent(rec(z0)) 11.71/3.44
rec(no(z0)) → sent(rec(z0)) 11.71/3.44
rec(bot) → up(sent(bot)) 11.71/3.44
sent(up(z0)) → up(sent(z0)) 11.71/3.44
check(sent(z0)) → sent(check(z0)) 11.71/3.44
check(rec(z0)) → rec(check(z0)) 11.71/3.44
check(no(z0)) → no(check(z0)) 11.71/3.44
check(no(z0)) → no(z0) 11.71/3.44
no(up(z0)) → up(no(z0))
And the Tuples:

REC(up(z0)) → c4(REC(z0)) 11.71/3.44
SENT(up(z0)) → c5(SENT(z0)) 11.71/3.44
NO(up(z0)) → c6(NO(z0)) 11.71/3.44
CHECK(up(z0)) → c10(CHECK(z0)) 11.71/3.44
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0)) 11.71/3.44
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0)) 11.71/3.44
CHECK(no(z0)) → c14(NO(z0)) 11.71/3.44
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0)) 11.71/3.44
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0)) 11.71/3.44
REC(bot) → c3 11.71/3.44
CHECK(rec(z0)) → c12(CHECK(z0)) 11.71/3.44
REC(rec(z0)) → c(REC(z0))
The order we found is given by the following interpretation:
Polynomial interpretation : 11.71/3.44

POL(CHECK(x1)) = [4] + [2]x1    11.71/3.44
POL(NO(x1)) = [2]x1    11.71/3.44
POL(REC(x1)) = 0    11.71/3.44
POL(SENT(x1)) = 0    11.71/3.44
POL(bot) = [3]    11.71/3.44
POL(c(x1)) = x1    11.71/3.44
POL(c1(x1, x2)) = x1 + x2    11.71/3.44
POL(c10(x1)) = x1    11.71/3.44
POL(c11(x1, x2)) = x1 + x2    11.71/3.44
POL(c12(x1)) = x1    11.71/3.44
POL(c13(x1, x2)) = x1 + x2    11.71/3.44
POL(c14(x1)) = x1    11.71/3.44
POL(c2(x1, x2)) = x1 + x2    11.71/3.44
POL(c3) = 0    11.71/3.44
POL(c4(x1)) = x1    11.71/3.44
POL(c5(x1)) = x1    11.71/3.44
POL(c6(x1)) = x1    11.71/3.44
POL(check(x1)) = [4]x1    11.71/3.44
POL(no(x1)) = [5]x1    11.71/3.44
POL(rec(x1)) = [2] + x1    11.71/3.44
POL(sent(x1)) = [2]x1    11.71/3.44
POL(up(x1)) = [1] + x1   
11.71/3.44
11.71/3.44

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

rec(rec(z0)) → sent(rec(z0)) 11.71/3.44
rec(sent(z0)) → sent(rec(z0)) 11.71/3.44
rec(no(z0)) → sent(rec(z0)) 11.71/3.44
rec(bot) → up(sent(bot)) 11.71/3.44
rec(up(z0)) → up(rec(z0)) 11.71/3.44
sent(up(z0)) → up(sent(z0)) 11.71/3.44
no(up(z0)) → up(no(z0)) 11.71/3.44
top(rec(up(z0))) → top(check(rec(z0))) 11.71/3.44
top(sent(up(z0))) → top(check(rec(z0))) 11.71/3.44
top(no(up(z0))) → top(check(rec(z0))) 11.71/3.44
check(up(z0)) → up(check(z0)) 11.71/3.44
check(sent(z0)) → sent(check(z0)) 11.71/3.44
check(rec(z0)) → rec(check(z0)) 11.71/3.44
check(no(z0)) → no(check(z0)) 11.71/3.44
check(no(z0)) → no(z0)
Tuples:

REC(up(z0)) → c4(REC(z0)) 11.71/3.44
SENT(up(z0)) → c5(SENT(z0)) 11.71/3.44
NO(up(z0)) → c6(NO(z0)) 11.71/3.44
CHECK(up(z0)) → c10(CHECK(z0)) 11.71/3.44
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0)) 11.71/3.44
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0)) 11.71/3.44
CHECK(no(z0)) → c14(NO(z0)) 11.71/3.44
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0)) 11.71/3.44
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0)) 11.71/3.44
REC(bot) → c3 11.71/3.44
CHECK(rec(z0)) → c12(CHECK(z0)) 11.71/3.44
REC(rec(z0)) → c(REC(z0))
S tuples:none
K tuples:

CHECK(no(z0)) → c14(NO(z0)) 11.71/3.44
REC(bot) → c3 11.71/3.44
REC(rec(z0)) → c(REC(z0)) 11.71/3.44
CHECK(sent(z0)) → c11(SENT(check(z0)), CHECK(z0)) 11.71/3.44
CHECK(no(z0)) → c13(NO(check(z0)), CHECK(z0)) 11.71/3.44
REC(sent(z0)) → c1(SENT(rec(z0)), REC(z0)) 11.71/3.44
REC(no(z0)) → c2(SENT(rec(z0)), REC(z0)) 11.71/3.44
CHECK(rec(z0)) → c12(CHECK(z0)) 11.71/3.44
REC(up(z0)) → c4(REC(z0)) 11.71/3.44
CHECK(up(z0)) → c10(CHECK(z0)) 11.71/3.44
SENT(up(z0)) → c5(SENT(z0)) 11.71/3.44
NO(up(z0)) → c6(NO(z0))
Defined Rule Symbols:

rec, sent, no, top, check

Defined Pair Symbols:

REC, SENT, NO, CHECK

Compound Symbols:

c4, c5, c6, c10, c11, c13, c14, c1, c2, c3, c12, c

11.71/3.44
11.71/3.44

(23) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

The set S is empty
11.71/3.44
11.71/3.44

(24) BOUNDS(O(1), O(1))

11.71/3.44
11.71/3.44
11.96/3.52 EOF