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()))
    13: Tl(O(x),y) ->= Tl(check(x),y)
    14: Tl(O(x),y) ->= Tl(x,check(y))
    15: Tl(N(x),y) ->= Tl(check(x),y)
    16: Tl(N(x),y) ->= Tl(x,check(y))
    17: Tr(x,O(y)) ->= Tr(check(x),y)
    18: Tr(x,O(y)) ->= Tr(x,check(y))
    19: Tr(x,N(y)) ->= Tr(check(x),y)
    20: Tr(x,N(y)) ->= Tr(x,check(y))
    21: B() ->= N(B())
    22: check(O(x)) ->= O(x)
    23: check(O(x)) ->= O(check(x))
    24: check(N(x)) ->= N(check(x))
Number of strict rules: 12
Direct Order(PosReal,>,Poly) ... removes: 18 1 17 5 14 13 6 2
    Tl(x1,x2)	weight: x2 + x1
     O(x1)	weight: (/ 1 8) + 2 * x1
     B()	weight: (/ 1 8)
 check(x1)	weight: x1
    Tr(x1,x2)	weight: x2 + x1
     N(x1)	weight: x1
Number of strict rules: 8
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #Tl(B(),y) -> #Tr(check(B()),y)
   #2: #Tr(x,B()) -> #Tl(check(x),B())
   #3: #Tr(x,B()) -> #Tl(x,check(B()))
   #4: #Tr(x,N(y)) ->? #Tr(x,check(y))
   #5: #Tr(x,N(y)) -> #Tl(check(x),y)
   #6: #Tl(B(),y) -> #Tr(B(),check(y))
   #7: #Tr(x,N(y)) ->? #Tr(check(x),y)
   #8: #Tl(N(x),y) ->? #Tl(x,check(y))
   #9: #Tl(N(x),y) -> #Tr(check(x),y)
   #10: #Tr(x,N(y)) -> #Tl(x,check(y))
   #11: #Tl(N(x),y) ->? #Tl(check(x),y)
   #12: #Tl(N(x),y) -> #Tr(x,check(y))
Number of SCCs: 1, DPs: 12, edges: 60
	SCC { #1..12 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
  #Tl(x1,x2)	weight: max{0, (/ 1 4) + x2}
    Tl(x1,x2)	weight: max{0, (/ 1 4) + x2}
     O(x1)	weight: 0
     B()	weight: (/ 1 4)
 check(x1)	weight: 0
    Tr(x1,x2)	weight: max{0, (/ 1 4) + x2}
     N(x1)	weight: x1
  #Tr(x1,x2)	weight: max{0, (/ 1 4) + x2}
    Removed DPs: #3
Number of SCCs: 1, DPs: 11, edges: 51
	SCC { #1 #2 #4..12 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
  #Tl(x1,x2)	weight: max{0, (/ 1 4) + x1}
    Tl(x1,x2)	weight: max{0, (/ 1 4) + x2}
     O(x1)	weight: 0
     B()	weight: (/ 1 4)
 check(x1)	weight: 0
    Tr(x1,x2)	weight: max{0, (/ 1 4) + x2}
     N(x1)	weight: x1
  #Tr(x1,x2)	weight: max{0, (/ 1 4) + x1}
    Removed DPs: #1
Number of SCCs: 1, DPs: 10, edges: 44
	SCC { #2 #4..12 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... Order(PosReal,>,Sum-Sum; PosReal,≥,Sum-Sum)... Order(PosReal,>,Sum-Sum; NegReal,≥,Sum)... Order(PosReal,>,MaxSum-Sum; NegReal,≥,Sum)... failed.
Removing edges: failed.
Finding a loop...  failed.
MAYBE