Input TRS:
    1: Tl(O(x),y) -> Wr(check(x),y)
    2: Tl(O(x),y) -> Wr(x,check(y))
    3: Tl(N(x),y) -> Wr(check(x),y)
    4: Tl(N(x),y) -> Wr(x,check(y))
    5: Tr(x,O(y)) -> Wl(check(x),y)
    6: Tr(x,O(y)) -> Wl(x,check(y))
    7: Tr(x,N(y)) -> Wl(check(x),y)
    8: Tr(x,N(y)) -> Wl(x,check(y))
    9: Tl(B(),y) -> Wr(check(B()),y)
    10: Tl(B(),y) -> Wr(B(),check(y))
    11: Tr(x,B()) -> Wl(check(x),B())
    12: Tr(x,B()) -> Wl(x,check(B()))
   e1: Tl(O(x),y) ->= Wl(check(x),y)	[relative]
   e2: Tl(O(x),y) ->= Wl(x,check(y))	[relative]
   e3: Tl(N(x),y) ->= Wl(check(x),y)	[relative]
   e4: Tl(N(x),y) ->= Wl(x,check(y))	[relative]
   e5: Tr(x,O(y)) ->= Wr(check(x),y)	[relative]
   e6: Tr(x,O(y)) ->= Wr(x,check(y))	[relative]
   e7: Tr(x,N(y)) ->= Wr(check(x),y)	[relative]
   e8: Tr(x,N(y)) ->= Wr(x,check(y))	[relative]
   e9: B() ->= N(B())	[relative]
   e10: check(O(x)) ->= ok(O(x))	[relative]
   e11: Wl(ok(x),y) ->= Tl(x,y)	[relative]
   e12: Wl(x,ok(y)) ->= Tl(x,y)	[relative]
   e13: Wr(ok(x),y) ->= Tr(x,y)	[relative]
   e14: Wr(x,ok(y)) ->= Tr(x,y)	[relative]
   e15: check(O(x)) ->= O(check(x))	[relative]
   e16: check(N(x)) ->= N(check(x))	[relative]
   e17: O(ok(x)) ->= ok(O(x))	[relative]
   e18: N(ok(x)) ->= ok(N(x))	[relative]
Weak rule e14 calls a strict rule