MAYBE Termination Proof using AProVETerm Rewriting System R:
[N, M, M1, N1, M2, N2, X, z, y, x]
3 -> s--osb-Nat-csb(s--osb-Nat-csb(s--osb-Nat-csb(0)))
4 -> s--osb-Nat-csb(3)
5 -> s--osb-Nat-csb(4)
8 -> -+--osb-Nat-csb-osb-Nat-csb(3, 5)
initial -> ---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(3, 0), ---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(5, 0), basin-osb-Nat-csb-osb-Nat-csb(8, 0)))
-+--osb-Nat-csb-osb-Nat-csb(0, N) -> N
-+--osb-Nat-csb-osb-Nat-csb(s--osb-Nat-csb(N), M) -> s--osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N, M))
---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, N1), basin-osb-Nat-csb-osb-Nat-csb(M2, N2)) -> U11(equal-osb-Bool-csb-osb-Bool-csb(-<=--osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2), true), M1, M2, N1, N2)
---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, N1), basin-osb-Nat-csb-osb-Nat-csb(M2, N2)) -> U21(equal-osb-Bool-csb-osb-Bool-csb(->--osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2), true), M1, M2, N1, N2)
-<=--osb-Nat-csb-osb-Nat-csb(0, N) -> true
-<=--osb-Nat-csb-osb-Nat-csb(N, N) -> true
-<=--osb-Nat-csb-osb-Nat-csb(s--osb-Nat-csb(N), 0) -> false
-<=--osb-Nat-csb-osb-Nat-csb(s--osb-Nat-csb(N), s--osb-Nat-csb(M)) -> -<=--osb-Nat-csb-osb-Nat-csb(N, M)
->--osb-Nat-csb-osb-Nat-csb(N, M) -> not-osb-Bool-csb(-<=--osb-Nat-csb-osb-Nat-csb(N, M))
U11(tt, M1, M2, N1, N2) -> ---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, 0), basin-osb-Nat-csb-osb-Nat-csb(M2, -+--osb-Nat-csb-osb-Nat-csb(N1, N2)))
U21(tt, M1, M2, N1, N2) -> ---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, sd-osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2)), basin-osb-Nat-csb-osb-Nat-csb(M2, M2))
basin-osb-Nat-csb-osb-Nat-csb(M1, N1) -> basin-osb-Nat-csb-osb-Nat-csb(M1, 0)
basin-osb-Nat-csb-osb-Nat-csb(M1, N1) -> basin-osb-Nat-csb-osb-Nat-csb(M1, M1)
equal-osb-Bool-csb-osb-Bool-csb(X, X) -> tt
not-osb-Bool-csb(false) -> true
not-osb-Bool-csb(true) -> false
sd-osb-Nat-csb-osb-Nat-csb(0, N) -> N
sd-osb-Nat-csb-osb-Nat-csb(N, 0) -> N
sd-osb-Nat-csb-osb-Nat-csb(s--osb-Nat-csb(N), s--osb-Nat-csb(M)) -> sd-osb-Nat-csb-osb-Nat-csb(N, M)
---osb-BasinSet-csb-osb-BasinSet-csb(---osb-BasinSet-csb-osb-BasinSet-csb(x, y), z) == ---osb-BasinSet-csb-osb-BasinSet-csb(x, ---osb-BasinSet-csb-osb-BasinSet-csb(y, z))
---osb-BasinSet-csb-osb-BasinSet-csb(x, y) == ---osb-BasinSet-csb-osb-BasinSet-csb(y, x)

Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

5' -> 4'
4' -> 3'
->--OSB-NAT-CSB-OSB-NAT-CSB(N, M) -> NOT-OSB-BOOL-CSB(-<=--osb-Nat-csb-osb-Nat-csb(N, M))
->--OSB-NAT-CSB-OSB-NAT-CSB(N, M) -> -<=--OSB-NAT-CSB-OSB-NAT-CSB(N, M)
-<=--OSB-NAT-CSB-OSB-NAT-CSB(s--osb-Nat-csb(N), s--osb-Nat-csb(M)) -> -<=--OSB-NAT-CSB-OSB-NAT-CSB(N, M)
-+--OSB-NAT-CSB-OSB-NAT-CSB(s--osb-Nat-csb(N), M) -> -+--OSB-NAT-CSB-OSB-NAT-CSB(N, M)
BASIN-OSB-NAT-CSB-OSB-NAT-CSB(M1, N1) -> BASIN-OSB-NAT-CSB-OSB-NAT-CSB(M1, M1)
BASIN-OSB-NAT-CSB-OSB-NAT-CSB(M1, N1) -> BASIN-OSB-NAT-CSB-OSB-NAT-CSB(M1, 0)
SD-OSB-NAT-CSB-OSB-NAT-CSB(s--osb-Nat-csb(N), s--osb-Nat-csb(M)) -> SD-OSB-NAT-CSB-OSB-NAT-CSB(N, M)
---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, N1), basin-osb-Nat-csb-osb-Nat-csb(M2, N2)) -> U21'(equal-osb-Bool-csb-osb-Bool-csb(->--osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2), true), M1, M2, N1, N2)
---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, N1), basin-osb-Nat-csb-osb-Nat-csb(M2, N2)) -> EQUAL-OSB-BOOL-CSB-OSB-BOOL-CSB(->--osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2), true)
---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, N1), basin-osb-Nat-csb-osb-Nat-csb(M2, N2)) -> ->--OSB-NAT-CSB-OSB-NAT-CSB(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2)
---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, N1), basin-osb-Nat-csb-osb-Nat-csb(M2, N2)) -> -+--OSB-NAT-CSB-OSB-NAT-CSB(N1, N2)
---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, N1), basin-osb-Nat-csb-osb-Nat-csb(M2, N2)) -> U11'(equal-osb-Bool-csb-osb-Bool-csb(-<=--osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2), true), M1, M2, N1, N2)
---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, N1), basin-osb-Nat-csb-osb-Nat-csb(M2, N2)) -> EQUAL-OSB-BOOL-CSB-OSB-BOOL-CSB(-<=--osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2), true)
---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, N1), basin-osb-Nat-csb-osb-Nat-csb(M2, N2)) -> -<=--OSB-NAT-CSB-OSB-NAT-CSB(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2)
---osb-BasinSet-csb-osb-BasinSet-csb(---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, N1), basin-osb-Nat-csb-osb-Nat-csb(M2, N2)), ext) -> ---osb-BasinSet-csb-osb-BasinSet-csb(U21(equal-osb-Bool-csb-osb-Bool-csb(->--osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2), true), M1, M2, N1, N2), ext)
---osb-BasinSet-csb-osb-BasinSet-csb(---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, N1), basin-osb-Nat-csb-osb-Nat-csb(M2, N2)), ext) -> U21'(equal-osb-Bool-csb-osb-Bool-csb(->--osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2), true), M1, M2, N1, N2)
---osb-BasinSet-csb-osb-BasinSet-csb(---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, N1), basin-osb-Nat-csb-osb-Nat-csb(M2, N2)), ext) -> EQUAL-OSB-BOOL-CSB-OSB-BOOL-CSB(->--osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2), true)
---osb-BasinSet-csb-osb-BasinSet-csb(---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, N1), basin-osb-Nat-csb-osb-Nat-csb(M2, N2)), ext) -> ->--OSB-NAT-CSB-OSB-NAT-CSB(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2)
---osb-BasinSet-csb-osb-BasinSet-csb(---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, N1), basin-osb-Nat-csb-osb-Nat-csb(M2, N2)), ext) -> -+--OSB-NAT-CSB-OSB-NAT-CSB(N1, N2)
---osb-BasinSet-csb-osb-BasinSet-csb(---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, N1), basin-osb-Nat-csb-osb-Nat-csb(M2, N2)), ext) -> ---osb-BasinSet-csb-osb-BasinSet-csb(U11(equal-osb-Bool-csb-osb-Bool-csb(-<=--osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2), true), M1, M2, N1, N2), ext)
---osb-BasinSet-csb-osb-BasinSet-csb(---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, N1), basin-osb-Nat-csb-osb-Nat-csb(M2, N2)), ext) -> U11'(equal-osb-Bool-csb-osb-Bool-csb(-<=--osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2), true), M1, M2, N1, N2)
---osb-BasinSet-csb-osb-BasinSet-csb(---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, N1), basin-osb-Nat-csb-osb-Nat-csb(M2, N2)), ext) -> EQUAL-OSB-BOOL-CSB-OSB-BOOL-CSB(-<=--osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2), true)
---osb-BasinSet-csb-osb-BasinSet-csb(---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, N1), basin-osb-Nat-csb-osb-Nat-csb(M2, N2)), ext) -> -<=--OSB-NAT-CSB-OSB-NAT-CSB(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2)
U21'(tt, M1, M2, N1, N2) -> ---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, sd-osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2)), basin-osb-Nat-csb-osb-Nat-csb(M2, M2))
U21'(tt, M1, M2, N1, N2) -> BASIN-OSB-NAT-CSB-OSB-NAT-CSB(M1, sd-osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2))
U21'(tt, M1, M2, N1, N2) -> SD-OSB-NAT-CSB-OSB-NAT-CSB(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2)
U21'(tt, M1, M2, N1, N2) -> -+--OSB-NAT-CSB-OSB-NAT-CSB(N1, N2)
U21'(tt, M1, M2, N1, N2) -> BASIN-OSB-NAT-CSB-OSB-NAT-CSB(M2, M2)
INITIAL -> ---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(3, 0), ---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(5, 0), basin-osb-Nat-csb-osb-Nat-csb(8, 0)))
INITIAL -> BASIN-OSB-NAT-CSB-OSB-NAT-CSB(3, 0)
INITIAL -> 3'
INITIAL -> ---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(5, 0), basin-osb-Nat-csb-osb-Nat-csb(8, 0))
INITIAL -> BASIN-OSB-NAT-CSB-OSB-NAT-CSB(5, 0)
INITIAL -> 5'
INITIAL -> BASIN-OSB-NAT-CSB-OSB-NAT-CSB(8, 0)
INITIAL -> 8'
8' -> -+--OSB-NAT-CSB-OSB-NAT-CSB(3, 5)
8' -> 3'
8' -> 5'
U11'(tt, M1, M2, N1, N2) -> ---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, 0), basin-osb-Nat-csb-osb-Nat-csb(M2, -+--osb-Nat-csb-osb-Nat-csb(N1, N2)))
U11'(tt, M1, M2, N1, N2) -> BASIN-OSB-NAT-CSB-OSB-NAT-CSB(M1, 0)
U11'(tt, M1, M2, N1, N2) -> BASIN-OSB-NAT-CSB-OSB-NAT-CSB(M2, -+--osb-Nat-csb-osb-Nat-csb(N1, N2))
U11'(tt, M1, M2, N1, N2) -> -+--OSB-NAT-CSB-OSB-NAT-CSB(N1, N2)

Furthermore, R contains five SCCs. 


   R
     ↳DPs
       →DP Problem 1
         ↳Polynomial Ordering
       →DP Problem 2
         ↳Polo
       →DP Problem 3
         ↳Remaining
       →DP Problem 4
         ↳Polo
       →DP Problem 5
         ↳Polo


Dependency Pair:

-<=--OSB-NAT-CSB-OSB-NAT-CSB(s--osb-Nat-csb(N), s--osb-Nat-csb(M)) -> -<=--OSB-NAT-CSB-OSB-NAT-CSB(N, M)


Rules:


5 -> s--osb-Nat-csb(4)
4 -> s--osb-Nat-csb(3)
->--osb-Nat-csb-osb-Nat-csb(N, M) -> not-osb-Bool-csb(-<=--osb-Nat-csb-osb-Nat-csb(N, M))
not-osb-Bool-csb(false) -> true
not-osb-Bool-csb(true) -> false
-<=--osb-Nat-csb-osb-Nat-csb(N, N) -> true
-<=--osb-Nat-csb-osb-Nat-csb(s--osb-Nat-csb(N), 0) -> false
-<=--osb-Nat-csb-osb-Nat-csb(0, N) -> true
-<=--osb-Nat-csb-osb-Nat-csb(s--osb-Nat-csb(N), s--osb-Nat-csb(M)) -> -<=--osb-Nat-csb-osb-Nat-csb(N, M)
-+--osb-Nat-csb-osb-Nat-csb(s--osb-Nat-csb(N), M) -> s--osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N, M))
-+--osb-Nat-csb-osb-Nat-csb(0, N) -> N
3 -> s--osb-Nat-csb(s--osb-Nat-csb(s--osb-Nat-csb(0)))
basin-osb-Nat-csb-osb-Nat-csb(M1, N1) -> basin-osb-Nat-csb-osb-Nat-csb(M1, M1)
basin-osb-Nat-csb-osb-Nat-csb(M1, N1) -> basin-osb-Nat-csb-osb-Nat-csb(M1, 0)
sd-osb-Nat-csb-osb-Nat-csb(s--osb-Nat-csb(N), s--osb-Nat-csb(M)) -> sd-osb-Nat-csb-osb-Nat-csb(N, M)
sd-osb-Nat-csb-osb-Nat-csb(N, 0) -> N
sd-osb-Nat-csb-osb-Nat-csb(0, N) -> N
---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, N1), basin-osb-Nat-csb-osb-Nat-csb(M2, N2)) -> U21(equal-osb-Bool-csb-osb-Bool-csb(->--osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2), true), M1, M2, N1, N2)
---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, N1), basin-osb-Nat-csb-osb-Nat-csb(M2, N2)) -> U11(equal-osb-Bool-csb-osb-Bool-csb(-<=--osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2), true), M1, M2, N1, N2)
U21(tt, M1, M2, N1, N2) -> ---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, sd-osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2)), basin-osb-Nat-csb-osb-Nat-csb(M2, M2))
equal-osb-Bool-csb-osb-Bool-csb(X, X) -> tt
initial -> ---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(3, 0), ---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(5, 0), basin-osb-Nat-csb-osb-Nat-csb(8, 0)))
8 -> -+--osb-Nat-csb-osb-Nat-csb(3, 5)
U11(tt, M1, M2, N1, N2) -> ---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, 0), basin-osb-Nat-csb-osb-Nat-csb(M2, -+--osb-Nat-csb-osb-Nat-csb(N1, N2)))





The following dependency pair can be strictly oriented:

-<=--OSB-NAT-CSB-OSB-NAT-CSB(s--osb-Nat-csb(N), s--osb-Nat-csb(M)) -> -<=--OSB-NAT-CSB-OSB-NAT-CSB(N, M)


There are no usable rules w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(s--osb-Nat-csb(x1))=  1 + x1  
  POL(-<=--OSB-NAT-CSB-OSB-NAT-CSB(x1, x2))=  1 + x1  

resulting in one new DP problem. 



   R
     ↳DPs
       →DP Problem 1
         ↳Polo
           →DP Problem 6
             ↳Dependency Graph
       →DP Problem 2
         ↳Polo
       →DP Problem 3
         ↳Remaining
       →DP Problem 4
         ↳Polo
       →DP Problem 5
         ↳Polo


Dependency Pair:


Rules:


5 -> s--osb-Nat-csb(4)
4 -> s--osb-Nat-csb(3)
->--osb-Nat-csb-osb-Nat-csb(N, M) -> not-osb-Bool-csb(-<=--osb-Nat-csb-osb-Nat-csb(N, M))
not-osb-Bool-csb(false) -> true
not-osb-Bool-csb(true) -> false
-<=--osb-Nat-csb-osb-Nat-csb(N, N) -> true
-<=--osb-Nat-csb-osb-Nat-csb(s--osb-Nat-csb(N), 0) -> false
-<=--osb-Nat-csb-osb-Nat-csb(0, N) -> true
-<=--osb-Nat-csb-osb-Nat-csb(s--osb-Nat-csb(N), s--osb-Nat-csb(M)) -> -<=--osb-Nat-csb-osb-Nat-csb(N, M)
-+--osb-Nat-csb-osb-Nat-csb(s--osb-Nat-csb(N), M) -> s--osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N, M))
-+--osb-Nat-csb-osb-Nat-csb(0, N) -> N
3 -> s--osb-Nat-csb(s--osb-Nat-csb(s--osb-Nat-csb(0)))
basin-osb-Nat-csb-osb-Nat-csb(M1, N1) -> basin-osb-Nat-csb-osb-Nat-csb(M1, M1)
basin-osb-Nat-csb-osb-Nat-csb(M1, N1) -> basin-osb-Nat-csb-osb-Nat-csb(M1, 0)
sd-osb-Nat-csb-osb-Nat-csb(s--osb-Nat-csb(N), s--osb-Nat-csb(M)) -> sd-osb-Nat-csb-osb-Nat-csb(N, M)
sd-osb-Nat-csb-osb-Nat-csb(N, 0) -> N
sd-osb-Nat-csb-osb-Nat-csb(0, N) -> N
---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, N1), basin-osb-Nat-csb-osb-Nat-csb(M2, N2)) -> U21(equal-osb-Bool-csb-osb-Bool-csb(->--osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2), true), M1, M2, N1, N2)
---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, N1), basin-osb-Nat-csb-osb-Nat-csb(M2, N2)) -> U11(equal-osb-Bool-csb-osb-Bool-csb(-<=--osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2), true), M1, M2, N1, N2)
U21(tt, M1, M2, N1, N2) -> ---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, sd-osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2)), basin-osb-Nat-csb-osb-Nat-csb(M2, M2))
equal-osb-Bool-csb-osb-Bool-csb(X, X) -> tt
initial -> ---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(3, 0), ---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(5, 0), basin-osb-Nat-csb-osb-Nat-csb(8, 0)))
8 -> -+--osb-Nat-csb-osb-Nat-csb(3, 5)
U11(tt, M1, M2, N1, N2) -> ---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, 0), basin-osb-Nat-csb-osb-Nat-csb(M2, -+--osb-Nat-csb-osb-Nat-csb(N1, N2)))





Using the Dependency Graph resulted in no new DP problems.


   R
     ↳DPs
       →DP Problem 1
         ↳Polo
       →DP Problem 2
         ↳Polynomial Ordering
       →DP Problem 3
         ↳Remaining
       →DP Problem 4
         ↳Polo
       →DP Problem 5
         ↳Polo


Dependency Pair:

-+--OSB-NAT-CSB-OSB-NAT-CSB(s--osb-Nat-csb(N), M) -> -+--OSB-NAT-CSB-OSB-NAT-CSB(N, M)


Rules:


5 -> s--osb-Nat-csb(4)
4 -> s--osb-Nat-csb(3)
->--osb-Nat-csb-osb-Nat-csb(N, M) -> not-osb-Bool-csb(-<=--osb-Nat-csb-osb-Nat-csb(N, M))
not-osb-Bool-csb(false) -> true
not-osb-Bool-csb(true) -> false
-<=--osb-Nat-csb-osb-Nat-csb(N, N) -> true
-<=--osb-Nat-csb-osb-Nat-csb(s--osb-Nat-csb(N), 0) -> false
-<=--osb-Nat-csb-osb-Nat-csb(0, N) -> true
-<=--osb-Nat-csb-osb-Nat-csb(s--osb-Nat-csb(N), s--osb-Nat-csb(M)) -> -<=--osb-Nat-csb-osb-Nat-csb(N, M)
-+--osb-Nat-csb-osb-Nat-csb(s--osb-Nat-csb(N), M) -> s--osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N, M))
-+--osb-Nat-csb-osb-Nat-csb(0, N) -> N
3 -> s--osb-Nat-csb(s--osb-Nat-csb(s--osb-Nat-csb(0)))
basin-osb-Nat-csb-osb-Nat-csb(M1, N1) -> basin-osb-Nat-csb-osb-Nat-csb(M1, M1)
basin-osb-Nat-csb-osb-Nat-csb(M1, N1) -> basin-osb-Nat-csb-osb-Nat-csb(M1, 0)
sd-osb-Nat-csb-osb-Nat-csb(s--osb-Nat-csb(N), s--osb-Nat-csb(M)) -> sd-osb-Nat-csb-osb-Nat-csb(N, M)
sd-osb-Nat-csb-osb-Nat-csb(N, 0) -> N
sd-osb-Nat-csb-osb-Nat-csb(0, N) -> N
---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, N1), basin-osb-Nat-csb-osb-Nat-csb(M2, N2)) -> U21(equal-osb-Bool-csb-osb-Bool-csb(->--osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2), true), M1, M2, N1, N2)
---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, N1), basin-osb-Nat-csb-osb-Nat-csb(M2, N2)) -> U11(equal-osb-Bool-csb-osb-Bool-csb(-<=--osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2), true), M1, M2, N1, N2)
U21(tt, M1, M2, N1, N2) -> ---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, sd-osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2)), basin-osb-Nat-csb-osb-Nat-csb(M2, M2))
equal-osb-Bool-csb-osb-Bool-csb(X, X) -> tt
initial -> ---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(3, 0), ---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(5, 0), basin-osb-Nat-csb-osb-Nat-csb(8, 0)))
8 -> -+--osb-Nat-csb-osb-Nat-csb(3, 5)
U11(tt, M1, M2, N1, N2) -> ---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, 0), basin-osb-Nat-csb-osb-Nat-csb(M2, -+--osb-Nat-csb-osb-Nat-csb(N1, N2)))





The following dependency pair can be strictly oriented:

-+--OSB-NAT-CSB-OSB-NAT-CSB(s--osb-Nat-csb(N), M) -> -+--OSB-NAT-CSB-OSB-NAT-CSB(N, M)


There are no usable rules w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(s--osb-Nat-csb(x1))=  1 + x1  
  POL(-+--OSB-NAT-CSB-OSB-NAT-CSB(x1, x2))=  1 + x1 + x2  

resulting in one new DP problem. 



   R
     ↳DPs
       →DP Problem 1
         ↳Polo
       →DP Problem 2
         ↳Polo
       →DP Problem 3
         ↳Remaining Obligation(s)
       →DP Problem 4
         ↳Polo
       →DP Problem 5
         ↳Polo
           →DP Problem 9
             ↳Remaining Obligation(s)




The following remains to be proven:


   R
     ↳DPs
       →DP Problem 1
         ↳Polo
       →DP Problem 2
         ↳Polo
       →DP Problem 3
         ↳Remaining
       →DP Problem 4
         ↳Polynomial Ordering
       →DP Problem 5
         ↳Polo


Dependency Pair:

SD-OSB-NAT-CSB-OSB-NAT-CSB(s--osb-Nat-csb(N), s--osb-Nat-csb(M)) -> SD-OSB-NAT-CSB-OSB-NAT-CSB(N, M)


Rules:


5 -> s--osb-Nat-csb(4)
4 -> s--osb-Nat-csb(3)
->--osb-Nat-csb-osb-Nat-csb(N, M) -> not-osb-Bool-csb(-<=--osb-Nat-csb-osb-Nat-csb(N, M))
not-osb-Bool-csb(false) -> true
not-osb-Bool-csb(true) -> false
-<=--osb-Nat-csb-osb-Nat-csb(N, N) -> true
-<=--osb-Nat-csb-osb-Nat-csb(s--osb-Nat-csb(N), 0) -> false
-<=--osb-Nat-csb-osb-Nat-csb(0, N) -> true
-<=--osb-Nat-csb-osb-Nat-csb(s--osb-Nat-csb(N), s--osb-Nat-csb(M)) -> -<=--osb-Nat-csb-osb-Nat-csb(N, M)
-+--osb-Nat-csb-osb-Nat-csb(s--osb-Nat-csb(N), M) -> s--osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N, M))
-+--osb-Nat-csb-osb-Nat-csb(0, N) -> N
3 -> s--osb-Nat-csb(s--osb-Nat-csb(s--osb-Nat-csb(0)))
basin-osb-Nat-csb-osb-Nat-csb(M1, N1) -> basin-osb-Nat-csb-osb-Nat-csb(M1, M1)
basin-osb-Nat-csb-osb-Nat-csb(M1, N1) -> basin-osb-Nat-csb-osb-Nat-csb(M1, 0)
sd-osb-Nat-csb-osb-Nat-csb(s--osb-Nat-csb(N), s--osb-Nat-csb(M)) -> sd-osb-Nat-csb-osb-Nat-csb(N, M)
sd-osb-Nat-csb-osb-Nat-csb(N, 0) -> N
sd-osb-Nat-csb-osb-Nat-csb(0, N) -> N
---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, N1), basin-osb-Nat-csb-osb-Nat-csb(M2, N2)) -> U21(equal-osb-Bool-csb-osb-Bool-csb(->--osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2), true), M1, M2, N1, N2)
---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, N1), basin-osb-Nat-csb-osb-Nat-csb(M2, N2)) -> U11(equal-osb-Bool-csb-osb-Bool-csb(-<=--osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2), true), M1, M2, N1, N2)
U21(tt, M1, M2, N1, N2) -> ---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, sd-osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2)), basin-osb-Nat-csb-osb-Nat-csb(M2, M2))
equal-osb-Bool-csb-osb-Bool-csb(X, X) -> tt
initial -> ---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(3, 0), ---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(5, 0), basin-osb-Nat-csb-osb-Nat-csb(8, 0)))
8 -> -+--osb-Nat-csb-osb-Nat-csb(3, 5)
U11(tt, M1, M2, N1, N2) -> ---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, 0), basin-osb-Nat-csb-osb-Nat-csb(M2, -+--osb-Nat-csb-osb-Nat-csb(N1, N2)))





The following dependency pair can be strictly oriented:

SD-OSB-NAT-CSB-OSB-NAT-CSB(s--osb-Nat-csb(N), s--osb-Nat-csb(M)) -> SD-OSB-NAT-CSB-OSB-NAT-CSB(N, M)


There are no usable rules w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(s--osb-Nat-csb(x1))=  1 + x1  
  POL(SD-OSB-NAT-CSB-OSB-NAT-CSB(x1, x2))=  1 + x1  

resulting in one new DP problem. 



   R
     ↳DPs
       →DP Problem 1
         ↳Polo
       →DP Problem 2
         ↳Polo
       →DP Problem 3
         ↳Remaining
       →DP Problem 4
         ↳Polo
       →DP Problem 5
         ↳Polynomial Ordering


Dependency Pairs:

---osb-BasinSet-csb-osb-BasinSet-csb(---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, N1), basin-osb-Nat-csb-osb-Nat-csb(M2, N2)), ext) -> U11'(equal-osb-Bool-csb-osb-Bool-csb(-<=--osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2), true), M1, M2, N1, N2)
---osb-BasinSet-csb-osb-BasinSet-csb(---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, N1), basin-osb-Nat-csb-osb-Nat-csb(M2, N2)), ext) -> ---osb-BasinSet-csb-osb-BasinSet-csb(U11(equal-osb-Bool-csb-osb-Bool-csb(-<=--osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2), true), M1, M2, N1, N2), ext)
---osb-BasinSet-csb-osb-BasinSet-csb(---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, N1), basin-osb-Nat-csb-osb-Nat-csb(M2, N2)), ext) -> U21'(equal-osb-Bool-csb-osb-Bool-csb(->--osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2), true), M1, M2, N1, N2)
---osb-BasinSet-csb-osb-BasinSet-csb(---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, N1), basin-osb-Nat-csb-osb-Nat-csb(M2, N2)), ext) -> ---osb-BasinSet-csb-osb-BasinSet-csb(U21(equal-osb-Bool-csb-osb-Bool-csb(->--osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2), true), M1, M2, N1, N2), ext)
U11'(tt, M1, M2, N1, N2) -> ---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, 0), basin-osb-Nat-csb-osb-Nat-csb(M2, -+--osb-Nat-csb-osb-Nat-csb(N1, N2)))
---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, N1), basin-osb-Nat-csb-osb-Nat-csb(M2, N2)) -> U11'(equal-osb-Bool-csb-osb-Bool-csb(-<=--osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2), true), M1, M2, N1, N2)
U21'(tt, M1, M2, N1, N2) -> ---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, sd-osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2)), basin-osb-Nat-csb-osb-Nat-csb(M2, M2))
---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, N1), basin-osb-Nat-csb-osb-Nat-csb(M2, N2)) -> U21'(equal-osb-Bool-csb-osb-Bool-csb(->--osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2), true), M1, M2, N1, N2)


Rules:


5 -> s--osb-Nat-csb(4)
4 -> s--osb-Nat-csb(3)
->--osb-Nat-csb-osb-Nat-csb(N, M) -> not-osb-Bool-csb(-<=--osb-Nat-csb-osb-Nat-csb(N, M))
not-osb-Bool-csb(false) -> true
not-osb-Bool-csb(true) -> false
-<=--osb-Nat-csb-osb-Nat-csb(N, N) -> true
-<=--osb-Nat-csb-osb-Nat-csb(s--osb-Nat-csb(N), 0) -> false
-<=--osb-Nat-csb-osb-Nat-csb(0, N) -> true
-<=--osb-Nat-csb-osb-Nat-csb(s--osb-Nat-csb(N), s--osb-Nat-csb(M)) -> -<=--osb-Nat-csb-osb-Nat-csb(N, M)
-+--osb-Nat-csb-osb-Nat-csb(s--osb-Nat-csb(N), M) -> s--osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N, M))
-+--osb-Nat-csb-osb-Nat-csb(0, N) -> N
3 -> s--osb-Nat-csb(s--osb-Nat-csb(s--osb-Nat-csb(0)))
basin-osb-Nat-csb-osb-Nat-csb(M1, N1) -> basin-osb-Nat-csb-osb-Nat-csb(M1, M1)
basin-osb-Nat-csb-osb-Nat-csb(M1, N1) -> basin-osb-Nat-csb-osb-Nat-csb(M1, 0)
sd-osb-Nat-csb-osb-Nat-csb(s--osb-Nat-csb(N), s--osb-Nat-csb(M)) -> sd-osb-Nat-csb-osb-Nat-csb(N, M)
sd-osb-Nat-csb-osb-Nat-csb(N, 0) -> N
sd-osb-Nat-csb-osb-Nat-csb(0, N) -> N
---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, N1), basin-osb-Nat-csb-osb-Nat-csb(M2, N2)) -> U21(equal-osb-Bool-csb-osb-Bool-csb(->--osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2), true), M1, M2, N1, N2)
---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, N1), basin-osb-Nat-csb-osb-Nat-csb(M2, N2)) -> U11(equal-osb-Bool-csb-osb-Bool-csb(-<=--osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2), true), M1, M2, N1, N2)
U21(tt, M1, M2, N1, N2) -> ---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, sd-osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2)), basin-osb-Nat-csb-osb-Nat-csb(M2, M2))
equal-osb-Bool-csb-osb-Bool-csb(X, X) -> tt
initial -> ---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(3, 0), ---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(5, 0), basin-osb-Nat-csb-osb-Nat-csb(8, 0)))
8 -> -+--osb-Nat-csb-osb-Nat-csb(3, 5)
U11(tt, M1, M2, N1, N2) -> ---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, 0), basin-osb-Nat-csb-osb-Nat-csb(M2, -+--osb-Nat-csb-osb-Nat-csb(N1, N2)))





The following dependency pairs can be strictly oriented:

---osb-BasinSet-csb-osb-BasinSet-csb(---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, N1), basin-osb-Nat-csb-osb-Nat-csb(M2, N2)), ext) -> U11'(equal-osb-Bool-csb-osb-Bool-csb(-<=--osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2), true), M1, M2, N1, N2)
---osb-BasinSet-csb-osb-BasinSet-csb(---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, N1), basin-osb-Nat-csb-osb-Nat-csb(M2, N2)), ext) -> U21'(equal-osb-Bool-csb-osb-Bool-csb(->--osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2), true), M1, M2, N1, N2)


Additionally, the following usable rules w.r.t. the implicit AFS can be oriented:

sd-osb-Nat-csb-osb-Nat-csb(s--osb-Nat-csb(N), s--osb-Nat-csb(M)) -> sd-osb-Nat-csb-osb-Nat-csb(N, M)
sd-osb-Nat-csb-osb-Nat-csb(N, 0) -> N
sd-osb-Nat-csb-osb-Nat-csb(0, N) -> N
U11(tt, M1, M2, N1, N2) -> ---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, 0), basin-osb-Nat-csb-osb-Nat-csb(M2, -+--osb-Nat-csb-osb-Nat-csb(N1, N2)))
U21(tt, M1, M2, N1, N2) -> ---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, sd-osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2)), basin-osb-Nat-csb-osb-Nat-csb(M2, M2))
-+--osb-Nat-csb-osb-Nat-csb(s--osb-Nat-csb(N), M) -> s--osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N, M))
-+--osb-Nat-csb-osb-Nat-csb(0, N) -> N
equal-osb-Bool-csb-osb-Bool-csb(X, X) -> tt
->--osb-Nat-csb-osb-Nat-csb(N, M) -> not-osb-Bool-csb(-<=--osb-Nat-csb-osb-Nat-csb(N, M))
---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, N1), basin-osb-Nat-csb-osb-Nat-csb(M2, N2)) -> U21(equal-osb-Bool-csb-osb-Bool-csb(->--osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2), true), M1, M2, N1, N2)
---osb-BasinSet-csb-osb-BasinSet-csb(basin-osb-Nat-csb-osb-Nat-csb(M1, N1), basin-osb-Nat-csb-osb-Nat-csb(M2, N2)) -> U11(equal-osb-Bool-csb-osb-Bool-csb(-<=--osb-Nat-csb-osb-Nat-csb(-+--osb-Nat-csb-osb-Nat-csb(N1, N2), M2), true), M1, M2, N1, N2)
not-osb-Bool-csb(false) -> true
not-osb-Bool-csb(true) -> false
basin-osb-Nat-csb-osb-Nat-csb(M1, N1) -> basin-osb-Nat-csb-osb-Nat-csb(M1, M1)
basin-osb-Nat-csb-osb-Nat-csb(M1, N1) -> basin-osb-Nat-csb-osb-Nat-csb(M1, 0)
-<=--osb-Nat-csb-osb-Nat-csb(N, N) -> true
-<=--osb-Nat-csb-osb-Nat-csb(s--osb-Nat-csb(N), 0) -> false
-<=--osb-Nat-csb-osb-Nat-csb(0, N) -> true
-<=--osb-Nat-csb-osb-Nat-csb(s--osb-Nat-csb(N), s--osb-Nat-csb(M)) -> -<=--osb-Nat-csb-osb-Nat-csb(N, M)

Oriented Equations:

---osb-BasinSet-csb-osb-BasinSet-csb(---osb-BasinSet-csb-osb-BasinSet-csb(x, y), z) == ---osb-BasinSet-csb-osb-BasinSet-csb(x, ---osb-BasinSet-csb-osb-BasinSet-csb(y, z))
---osb-BasinSet-csb-osb-BasinSet-csb(x, y) == ---osb-BasinSet-csb-osb-BasinSet-csb(y, x)


Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(U11(x1, x2, x3, x4, x5))=  1  
  POL(U21(x1, x2, x3, x4, x5))=  1  
  POL(true)=  0  
  POL(0)=  0  
  POL(->--osb-Nat-csb-osb-Nat-csb(x1, x2))=  0  
  POL(---osb-BasinSet-csb-osb-BasinSet-csb(x1, x2))=  1 + x1 + x2  
  POL(not-osb-Bool-csb(x1))=  0  
  POL(U11'(x1, x2, x3, x4, x5))=  1  
  POL(sd-osb-Nat-csb-osb-Nat-csb(x1, x2))=  x1 + x2  
  POL(U21'(x1, x2, x3, x4, x5))=  1  
  POL(s--osb-Nat-csb(x1))=  x1  
  POL(false)=  0  
  POL(-+--osb-Nat-csb-osb-Nat-csb(x1, x2))=  x2  
  POL(equal-osb-Bool-csb-osb-Bool-csb(x1, x2))=  0  
  POL(basin-osb-Nat-csb-osb-Nat-csb(x1, x2))=  0  
  POL(tt)=  0  
  POL(-<=--osb-Nat-csb-osb-Nat-csb(x1, x2))=  0  

resulting in one new DP problem. 



   R
     ↳DPs
       →DP Problem 1
         ↳Polo
       →DP Problem 2
         ↳Polo
       →DP Problem 3
         ↳Remaining Obligation(s)
       →DP Problem 4
         ↳Polo
       →DP Problem 5
         ↳Polo
           →DP Problem 9
             ↳Remaining Obligation(s)




The following remains to be proven:

The Proof could not be continued due to a Timeout.
Termination of R could not be shown.
Duration:
10:00 minutes