R
↳Dependency Pair Analysis
REC(rec(x)) -> SENT(rec(x))
REC(sent(x)) -> SENT(rec(x))
REC(sent(x)) -> REC(x)
REC(no(x)) -> SENT(rec(x))
REC(no(x)) -> REC(x)
REC(bot) -> SENT(bot)
REC(up(x)) -> REC(x)
SENT(up(x)) -> SENT(x)
NO(up(x)) -> NO(x)
TOP(rec(up(x))) -> TOP(check(rec(x)))
TOP(rec(up(x))) -> CHECK(rec(x))
TOP(rec(up(x))) -> REC(x)
TOP(sent(up(x))) -> TOP(check(rec(x)))
TOP(sent(up(x))) -> CHECK(rec(x))
TOP(sent(up(x))) -> REC(x)
TOP(no(up(x))) -> TOP(check(rec(x)))
TOP(no(up(x))) -> CHECK(rec(x))
TOP(no(up(x))) -> REC(x)
CHECK(up(x)) -> CHECK(x)
CHECK(sent(x)) -> SENT(check(x))
CHECK(sent(x)) -> CHECK(x)
CHECK(rec(x)) -> REC(check(x))
CHECK(rec(x)) -> CHECK(x)
CHECK(no(x)) -> NO(check(x))
CHECK(no(x)) -> CHECK(x)
R
↳DPs
→DP Problem 1
↳Argument Filtering and Ordering
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
SENT(up(x)) -> SENT(x)
rec(rec(x)) -> sent(rec(x))
rec(sent(x)) -> sent(rec(x))
rec(no(x)) -> sent(rec(x))
rec(bot) -> up(sent(bot))
rec(up(x)) -> up(rec(x))
sent(up(x)) -> up(sent(x))
no(up(x)) -> up(no(x))
top(rec(up(x))) -> top(check(rec(x)))
top(sent(up(x))) -> top(check(rec(x)))
top(no(up(x))) -> top(check(rec(x)))
check(up(x)) -> up(check(x))
check(sent(x)) -> sent(check(x))
check(rec(x)) -> rec(check(x))
check(no(x)) -> no(check(x))
check(no(x)) -> no(x)
SENT(up(x)) -> SENT(x)
POL(up(x1)) = 1 + x1 POL(SENT(x1)) = x1
SENT(x1) -> SENT(x1)
up(x1) -> up(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 6
↳Dependency Graph
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
rec(rec(x)) -> sent(rec(x))
rec(sent(x)) -> sent(rec(x))
rec(no(x)) -> sent(rec(x))
rec(bot) -> up(sent(bot))
rec(up(x)) -> up(rec(x))
sent(up(x)) -> up(sent(x))
no(up(x)) -> up(no(x))
top(rec(up(x))) -> top(check(rec(x)))
top(sent(up(x))) -> top(check(rec(x)))
top(no(up(x))) -> top(check(rec(x)))
check(up(x)) -> up(check(x))
check(sent(x)) -> sent(check(x))
check(rec(x)) -> rec(check(x))
check(no(x)) -> no(check(x))
check(no(x)) -> no(x)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Argument Filtering and Ordering
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
NO(up(x)) -> NO(x)
rec(rec(x)) -> sent(rec(x))
rec(sent(x)) -> sent(rec(x))
rec(no(x)) -> sent(rec(x))
rec(bot) -> up(sent(bot))
rec(up(x)) -> up(rec(x))
sent(up(x)) -> up(sent(x))
no(up(x)) -> up(no(x))
top(rec(up(x))) -> top(check(rec(x)))
top(sent(up(x))) -> top(check(rec(x)))
top(no(up(x))) -> top(check(rec(x)))
check(up(x)) -> up(check(x))
check(sent(x)) -> sent(check(x))
check(rec(x)) -> rec(check(x))
check(no(x)) -> no(check(x))
check(no(x)) -> no(x)
NO(up(x)) -> NO(x)
POL(NO(x1)) = x1 POL(up(x1)) = 1 + x1
NO(x1) -> NO(x1)
up(x1) -> up(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 7
↳Dependency Graph
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
rec(rec(x)) -> sent(rec(x))
rec(sent(x)) -> sent(rec(x))
rec(no(x)) -> sent(rec(x))
rec(bot) -> up(sent(bot))
rec(up(x)) -> up(rec(x))
sent(up(x)) -> up(sent(x))
no(up(x)) -> up(no(x))
top(rec(up(x))) -> top(check(rec(x)))
top(sent(up(x))) -> top(check(rec(x)))
top(no(up(x))) -> top(check(rec(x)))
check(up(x)) -> up(check(x))
check(sent(x)) -> sent(check(x))
check(rec(x)) -> rec(check(x))
check(no(x)) -> no(check(x))
check(no(x)) -> no(x)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Argument Filtering and Ordering
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
REC(up(x)) -> REC(x)
REC(no(x)) -> REC(x)
REC(sent(x)) -> REC(x)
rec(rec(x)) -> sent(rec(x))
rec(sent(x)) -> sent(rec(x))
rec(no(x)) -> sent(rec(x))
rec(bot) -> up(sent(bot))
rec(up(x)) -> up(rec(x))
sent(up(x)) -> up(sent(x))
no(up(x)) -> up(no(x))
top(rec(up(x))) -> top(check(rec(x)))
top(sent(up(x))) -> top(check(rec(x)))
top(no(up(x))) -> top(check(rec(x)))
check(up(x)) -> up(check(x))
check(sent(x)) -> sent(check(x))
check(rec(x)) -> rec(check(x))
check(no(x)) -> no(check(x))
check(no(x)) -> no(x)
REC(no(x)) -> REC(x)
POL(no(x1)) = 1 + x1 POL(up(x1)) = x1 POL(REC(x1)) = x1 POL(sent(x1)) = x1
REC(x1) -> REC(x1)
no(x1) -> no(x1)
sent(x1) -> sent(x1)
up(x1) -> up(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 8
↳Argument Filtering and Ordering
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
REC(up(x)) -> REC(x)
REC(sent(x)) -> REC(x)
rec(rec(x)) -> sent(rec(x))
rec(sent(x)) -> sent(rec(x))
rec(no(x)) -> sent(rec(x))
rec(bot) -> up(sent(bot))
rec(up(x)) -> up(rec(x))
sent(up(x)) -> up(sent(x))
no(up(x)) -> up(no(x))
top(rec(up(x))) -> top(check(rec(x)))
top(sent(up(x))) -> top(check(rec(x)))
top(no(up(x))) -> top(check(rec(x)))
check(up(x)) -> up(check(x))
check(sent(x)) -> sent(check(x))
check(rec(x)) -> rec(check(x))
check(no(x)) -> no(check(x))
check(no(x)) -> no(x)
REC(sent(x)) -> REC(x)
POL(up(x1)) = x1 POL(REC(x1)) = x1 POL(sent(x1)) = 1 + x1
REC(x1) -> REC(x1)
sent(x1) -> sent(x1)
up(x1) -> up(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 8
↳AFS
...
→DP Problem 9
↳Argument Filtering and Ordering
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
REC(up(x)) -> REC(x)
rec(rec(x)) -> sent(rec(x))
rec(sent(x)) -> sent(rec(x))
rec(no(x)) -> sent(rec(x))
rec(bot) -> up(sent(bot))
rec(up(x)) -> up(rec(x))
sent(up(x)) -> up(sent(x))
no(up(x)) -> up(no(x))
top(rec(up(x))) -> top(check(rec(x)))
top(sent(up(x))) -> top(check(rec(x)))
top(no(up(x))) -> top(check(rec(x)))
check(up(x)) -> up(check(x))
check(sent(x)) -> sent(check(x))
check(rec(x)) -> rec(check(x))
check(no(x)) -> no(check(x))
check(no(x)) -> no(x)
REC(up(x)) -> REC(x)
POL(up(x1)) = 1 + x1 POL(REC(x1)) = x1
REC(x1) -> REC(x1)
up(x1) -> up(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 8
↳AFS
...
→DP Problem 10
↳Dependency Graph
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
rec(rec(x)) -> sent(rec(x))
rec(sent(x)) -> sent(rec(x))
rec(no(x)) -> sent(rec(x))
rec(bot) -> up(sent(bot))
rec(up(x)) -> up(rec(x))
sent(up(x)) -> up(sent(x))
no(up(x)) -> up(no(x))
top(rec(up(x))) -> top(check(rec(x)))
top(sent(up(x))) -> top(check(rec(x)))
top(no(up(x))) -> top(check(rec(x)))
check(up(x)) -> up(check(x))
check(sent(x)) -> sent(check(x))
check(rec(x)) -> rec(check(x))
check(no(x)) -> no(check(x))
check(no(x)) -> no(x)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳Argument Filtering and Ordering
→DP Problem 5
↳AFS
CHECK(no(x)) -> CHECK(x)
CHECK(rec(x)) -> CHECK(x)
CHECK(sent(x)) -> CHECK(x)
CHECK(up(x)) -> CHECK(x)
rec(rec(x)) -> sent(rec(x))
rec(sent(x)) -> sent(rec(x))
rec(no(x)) -> sent(rec(x))
rec(bot) -> up(sent(bot))
rec(up(x)) -> up(rec(x))
sent(up(x)) -> up(sent(x))
no(up(x)) -> up(no(x))
top(rec(up(x))) -> top(check(rec(x)))
top(sent(up(x))) -> top(check(rec(x)))
top(no(up(x))) -> top(check(rec(x)))
check(up(x)) -> up(check(x))
check(sent(x)) -> sent(check(x))
check(rec(x)) -> rec(check(x))
check(no(x)) -> no(check(x))
check(no(x)) -> no(x)
CHECK(up(x)) -> CHECK(x)
POL(no(x1)) = x1 POL(rec(x1)) = x1 POL(up(x1)) = 1 + x1 POL(CHECK(x1)) = x1 POL(sent(x1)) = x1
CHECK(x1) -> CHECK(x1)
up(x1) -> up(x1)
no(x1) -> no(x1)
sent(x1) -> sent(x1)
rec(x1) -> rec(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 11
↳Argument Filtering and Ordering
→DP Problem 5
↳AFS
CHECK(no(x)) -> CHECK(x)
CHECK(rec(x)) -> CHECK(x)
CHECK(sent(x)) -> CHECK(x)
rec(rec(x)) -> sent(rec(x))
rec(sent(x)) -> sent(rec(x))
rec(no(x)) -> sent(rec(x))
rec(bot) -> up(sent(bot))
rec(up(x)) -> up(rec(x))
sent(up(x)) -> up(sent(x))
no(up(x)) -> up(no(x))
top(rec(up(x))) -> top(check(rec(x)))
top(sent(up(x))) -> top(check(rec(x)))
top(no(up(x))) -> top(check(rec(x)))
check(up(x)) -> up(check(x))
check(sent(x)) -> sent(check(x))
check(rec(x)) -> rec(check(x))
check(no(x)) -> no(check(x))
check(no(x)) -> no(x)
CHECK(no(x)) -> CHECK(x)
POL(no(x1)) = 1 + x1 POL(rec(x1)) = x1 POL(CHECK(x1)) = x1 POL(sent(x1)) = x1
CHECK(x1) -> CHECK(x1)
no(x1) -> no(x1)
sent(x1) -> sent(x1)
rec(x1) -> rec(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 11
↳AFS
...
→DP Problem 12
↳Argument Filtering and Ordering
→DP Problem 5
↳AFS
CHECK(rec(x)) -> CHECK(x)
CHECK(sent(x)) -> CHECK(x)
rec(rec(x)) -> sent(rec(x))
rec(sent(x)) -> sent(rec(x))
rec(no(x)) -> sent(rec(x))
rec(bot) -> up(sent(bot))
rec(up(x)) -> up(rec(x))
sent(up(x)) -> up(sent(x))
no(up(x)) -> up(no(x))
top(rec(up(x))) -> top(check(rec(x)))
top(sent(up(x))) -> top(check(rec(x)))
top(no(up(x))) -> top(check(rec(x)))
check(up(x)) -> up(check(x))
check(sent(x)) -> sent(check(x))
check(rec(x)) -> rec(check(x))
check(no(x)) -> no(check(x))
check(no(x)) -> no(x)
CHECK(sent(x)) -> CHECK(x)
POL(rec(x1)) = x1 POL(CHECK(x1)) = x1 POL(sent(x1)) = 1 + x1
CHECK(x1) -> CHECK(x1)
sent(x1) -> sent(x1)
rec(x1) -> rec(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 11
↳AFS
...
→DP Problem 13
↳Argument Filtering and Ordering
→DP Problem 5
↳AFS
CHECK(rec(x)) -> CHECK(x)
rec(rec(x)) -> sent(rec(x))
rec(sent(x)) -> sent(rec(x))
rec(no(x)) -> sent(rec(x))
rec(bot) -> up(sent(bot))
rec(up(x)) -> up(rec(x))
sent(up(x)) -> up(sent(x))
no(up(x)) -> up(no(x))
top(rec(up(x))) -> top(check(rec(x)))
top(sent(up(x))) -> top(check(rec(x)))
top(no(up(x))) -> top(check(rec(x)))
check(up(x)) -> up(check(x))
check(sent(x)) -> sent(check(x))
check(rec(x)) -> rec(check(x))
check(no(x)) -> no(check(x))
check(no(x)) -> no(x)
CHECK(rec(x)) -> CHECK(x)
POL(rec(x1)) = 1 + x1 POL(CHECK(x1)) = x1
CHECK(x1) -> CHECK(x1)
rec(x1) -> rec(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 11
↳AFS
...
→DP Problem 14
↳Dependency Graph
→DP Problem 5
↳AFS
rec(rec(x)) -> sent(rec(x))
rec(sent(x)) -> sent(rec(x))
rec(no(x)) -> sent(rec(x))
rec(bot) -> up(sent(bot))
rec(up(x)) -> up(rec(x))
sent(up(x)) -> up(sent(x))
no(up(x)) -> up(no(x))
top(rec(up(x))) -> top(check(rec(x)))
top(sent(up(x))) -> top(check(rec(x)))
top(no(up(x))) -> top(check(rec(x)))
check(up(x)) -> up(check(x))
check(sent(x)) -> sent(check(x))
check(rec(x)) -> rec(check(x))
check(no(x)) -> no(check(x))
check(no(x)) -> no(x)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳Argument Filtering and Ordering
TOP(no(up(x))) -> TOP(check(rec(x)))
TOP(sent(up(x))) -> TOP(check(rec(x)))
TOP(rec(up(x))) -> TOP(check(rec(x)))
rec(rec(x)) -> sent(rec(x))
rec(sent(x)) -> sent(rec(x))
rec(no(x)) -> sent(rec(x))
rec(bot) -> up(sent(bot))
rec(up(x)) -> up(rec(x))
sent(up(x)) -> up(sent(x))
no(up(x)) -> up(no(x))
top(rec(up(x))) -> top(check(rec(x)))
top(sent(up(x))) -> top(check(rec(x)))
top(no(up(x))) -> top(check(rec(x)))
check(up(x)) -> up(check(x))
check(sent(x)) -> sent(check(x))
check(rec(x)) -> rec(check(x))
check(no(x)) -> no(check(x))
check(no(x)) -> no(x)
TOP(no(up(x))) -> TOP(check(rec(x)))
check(up(x)) -> up(check(x))
check(sent(x)) -> sent(check(x))
check(rec(x)) -> rec(check(x))
check(no(x)) -> no(check(x))
check(no(x)) -> no(x)
rec(rec(x)) -> sent(rec(x))
rec(sent(x)) -> sent(rec(x))
rec(no(x)) -> sent(rec(x))
rec(bot) -> up(sent(bot))
rec(up(x)) -> up(rec(x))
sent(up(x)) -> up(sent(x))
no(up(x)) -> up(no(x))
POL(no(x1)) = 1 + x1 POL(rec(x1)) = x1 POL(bot) = 0 POL(up(x1)) = x1 POL(check(x1)) = x1 POL(TOP(x1)) = 1 + x1 POL(sent(x1)) = x1
TOP(x1) -> TOP(x1)
no(x1) -> no(x1)
check(x1) -> check(x1)
up(x1) -> up(x1)
rec(x1) -> rec(x1)
sent(x1) -> sent(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 15
↳Argument Filtering and Ordering
TOP(sent(up(x))) -> TOP(check(rec(x)))
TOP(rec(up(x))) -> TOP(check(rec(x)))
rec(rec(x)) -> sent(rec(x))
rec(sent(x)) -> sent(rec(x))
rec(no(x)) -> sent(rec(x))
rec(bot) -> up(sent(bot))
rec(up(x)) -> up(rec(x))
sent(up(x)) -> up(sent(x))
no(up(x)) -> up(no(x))
top(rec(up(x))) -> top(check(rec(x)))
top(sent(up(x))) -> top(check(rec(x)))
top(no(up(x))) -> top(check(rec(x)))
check(up(x)) -> up(check(x))
check(sent(x)) -> sent(check(x))
check(rec(x)) -> rec(check(x))
check(no(x)) -> no(check(x))
check(no(x)) -> no(x)
TOP(rec(up(x))) -> TOP(check(rec(x)))
check(up(x)) -> up(check(x))
check(sent(x)) -> sent(check(x))
check(rec(x)) -> rec(check(x))
check(no(x)) -> no(check(x))
check(no(x)) -> no(x)
rec(rec(x)) -> sent(rec(x))
rec(sent(x)) -> sent(rec(x))
rec(no(x)) -> sent(rec(x))
rec(bot) -> up(sent(bot))
rec(up(x)) -> up(rec(x))
sent(up(x)) -> up(sent(x))
no(up(x)) -> up(no(x))
POL(rec(x1)) = 1 + x1 POL(no(x1)) = x1 POL(bot) = 0 POL(up(x1)) = 1 + x1 POL(check(x1)) = x1 POL(TOP(x1)) = 1 + x1 POL(sent(x1)) = x1
TOP(x1) -> TOP(x1)
rec(x1) -> rec(x1)
check(x1) -> check(x1)
up(x1) -> up(x1)
sent(x1) -> sent(x1)
no(x1) -> no(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 15
↳AFS
...
→DP Problem 16
↳Narrowing Transformation
TOP(sent(up(x))) -> TOP(check(rec(x)))
rec(rec(x)) -> sent(rec(x))
rec(sent(x)) -> sent(rec(x))
rec(no(x)) -> sent(rec(x))
rec(bot) -> up(sent(bot))
rec(up(x)) -> up(rec(x))
sent(up(x)) -> up(sent(x))
no(up(x)) -> up(no(x))
top(rec(up(x))) -> top(check(rec(x)))
top(sent(up(x))) -> top(check(rec(x)))
top(no(up(x))) -> top(check(rec(x)))
check(up(x)) -> up(check(x))
check(sent(x)) -> sent(check(x))
check(rec(x)) -> rec(check(x))
check(no(x)) -> no(check(x))
check(no(x)) -> no(x)
six new Dependency Pairs are created:
TOP(sent(up(x))) -> TOP(check(rec(x)))
TOP(sent(up(x''))) -> TOP(rec(check(x'')))
TOP(sent(up(rec(x'')))) -> TOP(check(sent(rec(x''))))
TOP(sent(up(sent(x'')))) -> TOP(check(sent(rec(x''))))
TOP(sent(up(no(x'')))) -> TOP(check(sent(rec(x''))))
TOP(sent(up(bot))) -> TOP(check(up(sent(bot))))
TOP(sent(up(up(x'')))) -> TOP(check(up(rec(x''))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 15
↳AFS
...
→DP Problem 17
↳Argument Filtering and Ordering
TOP(sent(up(up(x'')))) -> TOP(check(up(rec(x''))))
TOP(sent(up(bot))) -> TOP(check(up(sent(bot))))
TOP(sent(up(no(x'')))) -> TOP(check(sent(rec(x''))))
TOP(sent(up(sent(x'')))) -> TOP(check(sent(rec(x''))))
TOP(sent(up(rec(x'')))) -> TOP(check(sent(rec(x''))))
TOP(sent(up(x''))) -> TOP(rec(check(x'')))
rec(rec(x)) -> sent(rec(x))
rec(sent(x)) -> sent(rec(x))
rec(no(x)) -> sent(rec(x))
rec(bot) -> up(sent(bot))
rec(up(x)) -> up(rec(x))
sent(up(x)) -> up(sent(x))
no(up(x)) -> up(no(x))
top(rec(up(x))) -> top(check(rec(x)))
top(sent(up(x))) -> top(check(rec(x)))
top(no(up(x))) -> top(check(rec(x)))
check(up(x)) -> up(check(x))
check(sent(x)) -> sent(check(x))
check(rec(x)) -> rec(check(x))
check(no(x)) -> no(check(x))
check(no(x)) -> no(x)
TOP(sent(up(rec(x'')))) -> TOP(check(sent(rec(x''))))
rec(rec(x)) -> sent(rec(x))
rec(sent(x)) -> sent(rec(x))
rec(no(x)) -> sent(rec(x))
rec(bot) -> up(sent(bot))
rec(up(x)) -> up(rec(x))
check(up(x)) -> up(check(x))
check(sent(x)) -> sent(check(x))
check(rec(x)) -> rec(check(x))
check(no(x)) -> no(check(x))
check(no(x)) -> no(x)
sent(up(x)) -> up(sent(x))
no(up(x)) -> up(no(x))
POL(rec(x1)) = 1 + x1 POL(bot) = 0 POL(no(x1)) = x1 POL(up(x1)) = 1 + x1 POL(check(x1)) = x1 POL(TOP(x1)) = 1 + x1 POL(sent(x1)) = x1
TOP(x1) -> TOP(x1)
sent(x1) -> sent(x1)
rec(x1) -> rec(x1)
up(x1) -> up(x1)
check(x1) -> check(x1)
no(x1) -> no(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 15
↳AFS
...
→DP Problem 18
↳Argument Filtering and Ordering
TOP(sent(up(up(x'')))) -> TOP(check(up(rec(x''))))
TOP(sent(up(bot))) -> TOP(check(up(sent(bot))))
TOP(sent(up(no(x'')))) -> TOP(check(sent(rec(x''))))
TOP(sent(up(sent(x'')))) -> TOP(check(sent(rec(x''))))
TOP(sent(up(x''))) -> TOP(rec(check(x'')))
rec(rec(x)) -> sent(rec(x))
rec(sent(x)) -> sent(rec(x))
rec(no(x)) -> sent(rec(x))
rec(bot) -> up(sent(bot))
rec(up(x)) -> up(rec(x))
sent(up(x)) -> up(sent(x))
no(up(x)) -> up(no(x))
top(rec(up(x))) -> top(check(rec(x)))
top(sent(up(x))) -> top(check(rec(x)))
top(no(up(x))) -> top(check(rec(x)))
check(up(x)) -> up(check(x))
check(sent(x)) -> sent(check(x))
check(rec(x)) -> rec(check(x))
check(no(x)) -> no(check(x))
check(no(x)) -> no(x)
TOP(sent(up(no(x'')))) -> TOP(check(sent(rec(x''))))
rec(rec(x)) -> sent(rec(x))
rec(sent(x)) -> sent(rec(x))
rec(no(x)) -> sent(rec(x))
rec(bot) -> up(sent(bot))
rec(up(x)) -> up(rec(x))
check(up(x)) -> up(check(x))
check(sent(x)) -> sent(check(x))
check(rec(x)) -> rec(check(x))
check(no(x)) -> no(check(x))
check(no(x)) -> no(x)
sent(up(x)) -> up(sent(x))
no(up(x)) -> up(no(x))
POL(rec(x1)) = x1 POL(bot) = 0 POL(no(x1)) = 1 + x1 POL(up(x1)) = x1 POL(check(x1)) = x1 POL(TOP(x1)) = 1 + x1 POL(sent(x1)) = x1
TOP(x1) -> TOP(x1)
sent(x1) -> sent(x1)
rec(x1) -> rec(x1)
up(x1) -> up(x1)
check(x1) -> check(x1)
no(x1) -> no(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 15
↳AFS
...
→DP Problem 19
↳Argument Filtering and Ordering
TOP(sent(up(up(x'')))) -> TOP(check(up(rec(x''))))
TOP(sent(up(bot))) -> TOP(check(up(sent(bot))))
TOP(sent(up(sent(x'')))) -> TOP(check(sent(rec(x''))))
TOP(sent(up(x''))) -> TOP(rec(check(x'')))
rec(rec(x)) -> sent(rec(x))
rec(sent(x)) -> sent(rec(x))
rec(no(x)) -> sent(rec(x))
rec(bot) -> up(sent(bot))
rec(up(x)) -> up(rec(x))
sent(up(x)) -> up(sent(x))
no(up(x)) -> up(no(x))
top(rec(up(x))) -> top(check(rec(x)))
top(sent(up(x))) -> top(check(rec(x)))
top(no(up(x))) -> top(check(rec(x)))
check(up(x)) -> up(check(x))
check(sent(x)) -> sent(check(x))
check(rec(x)) -> rec(check(x))
check(no(x)) -> no(check(x))
check(no(x)) -> no(x)
TOP(sent(up(up(x'')))) -> TOP(check(up(rec(x''))))
TOP(sent(up(bot))) -> TOP(check(up(sent(bot))))
rec(rec(x)) -> sent(rec(x))
rec(sent(x)) -> sent(rec(x))
rec(no(x)) -> sent(rec(x))
rec(bot) -> up(sent(bot))
rec(up(x)) -> up(rec(x))
check(up(x)) -> up(check(x))
check(sent(x)) -> sent(check(x))
check(rec(x)) -> rec(check(x))
check(no(x)) -> no(check(x))
check(no(x)) -> no(x)
sent(up(x)) -> up(sent(x))
no(up(x)) -> up(no(x))
POL(rec) = 1 POL(no(x1)) = x1 POL(up) = 0 POL(check(x1)) = x1 POL(TOP(x1)) = 1 + x1 POL(sent) = 1
TOP(x1) -> TOP(x1)
sent(x1) -> sent
rec(x1) -> rec
check(x1) -> check(x1)
up(x1) -> up
no(x1) -> no(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 15
↳AFS
...
→DP Problem 20
↳Remaining Obligation(s)
TOP(sent(up(sent(x'')))) -> TOP(check(sent(rec(x''))))
TOP(sent(up(x''))) -> TOP(rec(check(x'')))
rec(rec(x)) -> sent(rec(x))
rec(sent(x)) -> sent(rec(x))
rec(no(x)) -> sent(rec(x))
rec(bot) -> up(sent(bot))
rec(up(x)) -> up(rec(x))
sent(up(x)) -> up(sent(x))
no(up(x)) -> up(no(x))
top(rec(up(x))) -> top(check(rec(x)))
top(sent(up(x))) -> top(check(rec(x)))
top(no(up(x))) -> top(check(rec(x)))
check(up(x)) -> up(check(x))
check(sent(x)) -> sent(check(x))
check(rec(x)) -> rec(check(x))
check(no(x)) -> no(check(x))
check(no(x)) -> no(x)