Input TRS:
    1: Tl(O(x),y) -> Tr(check(x),y)
    2: Tl(O(x),y) -> Tr(x,check(y))
    3: Tl(N(x),y) -> Tr(check(x),y)
    4: Tl(N(x),y) -> Tr(x,check(y))
    5: Tr(x,O(y)) -> Tl(check(x),y)
    6: Tr(x,O(y)) -> Tl(x,check(y))
    7: Tr(x,N(y)) -> Tl(check(x),y)
    8: Tr(x,N(y)) -> Tl(x,check(y))
    9: Tl(B(),y) -> Tr(check(B()),y)
    10: Tl(B(),y) -> Tr(B(),check(y))
    11: Tr(x,B()) -> Tl(check(x),B())
    12: Tr(x,B()) -> Tl(x,check(B()))
   e1: Tl(O(x),y) ->= Tl(check(x),y)	[relative]
   e2: Tl(O(x),y) ->= Tl(x,check(y))	[relative]
   e3: Tl(N(x),y) ->= Tl(check(x),y)	[relative]
   e4: Tl(N(x),y) ->= Tl(x,check(y))	[relative]
   e5: Tr(x,O(y)) ->= Tr(check(x),y)	[relative]
   e6: Tr(x,O(y)) ->= Tr(x,check(y))	[relative]
   e7: Tr(x,N(y)) ->= Tr(check(x),y)	[relative]
   e8: Tr(x,N(y)) ->= Tr(x,check(y))	[relative]
   e9: B() ->= N(B())	[relative]
   e10: check(O(x)) ->= O(x)	[relative]
   e11: check(O(x)) ->= O(check(x))	[relative]
   e12: check(N(x)) ->= N(check(x))	[relative]
Dependency Pairs:
   #1: # Tl(O(x),y) -> # Tr(x,check(y))
   #2: # Tr(x,O(y)) -> # Tl(x,check(y))
   #3: # Tr(x,O(y)) -> # Tr(x,check(y))	[relative]
   #4: # Tl(B(),y) -> # Tr(check(B()),y)
   #5: # Tr(x,B()) -> # Tl(check(x),B())
   #6: # Tr(x,B()) -> # Tl(x,check(B()))
   #7: # Tl(O(x),y) -> # Tl(x,check(y))	[relative]
   #8: # Tl(O(x),y) -> # Tl(check(x),y)	[relative]
   #9: # Tr(x,N(y)) -> # Tl(check(x),y)
   #10: # Tl(B(),y) -> # Tr(B(),check(y))
   #11: # Tr(x,O(y)) -> # Tl(check(x),y)
   #12: # Tl(N(x),y) -> # Tl(check(x),y)	[relative]
   #13: # Tl(N(x),y) -> # Tl(x,check(y))	[relative]
   #14: # Tr(x,N(y)) -> # Tr(check(x),y)	[relative]
   #15: # Tl(N(x),y) -> # Tr(check(x),y)
   #16: # Tl(O(x),y) -> # Tr(check(x),y)
   #17: # Tr(x,N(y)) -> # Tl(x,check(y))
   #18: # Tr(x,N(y)) -> # Tr(x,check(y))	[relative]
   #19: # Tl(N(x),y) -> # Tr(x,check(y))
   #20: # Tr(x,O(y)) -> # Tr(check(x),y)	[relative]
Number of SCCs: 1
  SCC { #1..20 }
    POLO(Sum)... removes: #2 #3 #11 #20
	I(# Tr) = max(x2 - 1, 0)
	I(Tl) = 0
	I(O) = max(x1 + 2, 0)
	I(B) = 2
	I(check) = max(x1, 0)
	I(# Tl) = max(x2 - 1, 0)
	I(Tr) = 0
	I(N) = max(x1, 0)
Number of SCCs: 1
  SCC { #1 #4..10 #12..19 }
    POLO(Sum)... removes: #6
	I(# Tr) = max(x2 - 1, 0)
	I(Tl) = 0
	I(O) = 0
	I(B) = 2
	I(check) = 0
	I(# Tl) = max(x2 - 1, 0)
	I(Tr) = 0
	I(N) = max(x1, 0)
Number of SCCs: 1
  SCC { #1 #4 #5 #7..10 #12..19 }
    POLO(Sum)... removes: #1 #7 #8 #16
	I(# Tr) = max(x1 + x2 + 1, 0)
	I(Tl) = max(x2, 0)
	I(O) = max(x1 + 1, 0)
	I(B) = 1
	I(check) = max(x1, 0)
	I(# Tl) = max(x1 + x2 + 1, 0)
	I(Tr) = max(x2, 0)
	I(N) = max(x1, 0)
Number of SCCs: 1
  SCC { #4 #5 #9 #10 #12..15 #17..19 }
    POLO(Sum)... removes: #4
	I(# Tr) = max(x1 - 2, 0)
	I(Tl) = 0
	I(O) = 0
	I(B) = 3
	I(check) = 1
	I(# Tl) = max(x1 - 2, 0)
	I(Tr) = 0
	I(N) = max(x1, 0)
Number of SCCs: 1
  SCC { #5 #9 #10 #12..15 #17..19 }
    POLO(Sum)... QLPOS... QWPOpS(mSum)... Mat2b... failed.