Input TRS:
    1: T(ok(sys(x,P(d,b),R(b),y))) -> T(check(sys(x,bot(),R(not(b)),y)))
   e1: T(ok(sys(S(b,c(d,ds)),bot(),y,z))) ->= T(check(sys(S(b,c(d,ds)),P(d,b),y,z)))	[relative]
   e2: T(ok(sys(S(b,c(d,ds)),x,y,F(b)))) ->= T(check(sys(S(not(b),ds),x,y,bot())))	[relative]
   e3: T(ok(sys(x,y,R(b),bot()))) ->= T(check(sys(x,y,R(b),F(not(b)))))	[relative]
   e4: not(1()) ->= 0()	[relative]
   e5: not(0()) ->= 1()	[relative]
   e6: nils() ->= c(new(),nils())	[relative]
   e7: p(d,b) ->= bot()	[relative]
   e8: f(b) ->= bot()	[relative]
   e9: check(old()) ->= ok(old())	[relative]
   e10: check(f(v1)) ->= f(check(v1))	[relative]
   e11: f(ok(v1)) ->= ok(f(v1))	[relative]
   e12: check(p(v1,v2())) ->= p(v1,check(v2()))	[relative]
   e13: check(p(v1,v2())) ->= p(check(v1),v2())	[relative]
   e14: p(v1,ok(v2())) ->= ok(p(v1,v2()))	[relative]
   e15: p(ok(v1),v2()) ->= ok(p(v1,v2()))	[relative]
   e16: check(R(v1)) ->= R(check(v1))	[relative]
   e17: R(ok(v1)) ->= ok(R(v1))	[relative]
   e18: check(not(v1)) ->= not(check(v1))	[relative]
   e19: not(ok(v1)) ->= ok(not(v1))	[relative]
   e20: check(F(v1)) ->= F(check(v1))	[relative]
   e21: F(ok(v1)) ->= ok(F(v1))	[relative]
   e22: check(P(v1,v2())) ->= P(v1,check(v2()))	[relative]
   e23: check(P(v1,v2())) ->= P(check(v1),v2())	[relative]
   e24: P(v1,ok(v2())) ->= ok(P(v1,v2()))	[relative]
   e25: P(ok(v1),v2()) ->= ok(P(v1,v2()))	[relative]
   e26: check(c(v1,v2())) ->= c(v1,check(v2()))	[relative]
   e27: check(c(v1,v2())) ->= c(check(v1),v2())	[relative]
   e28: c(v1,ok(v2())) ->= ok(c(v1,v2()))	[relative]
   e29: c(ok(v1),v2()) ->= ok(c(v1,v2()))	[relative]
   e30: check(S(v1,v2())) ->= S(v1,check(v2()))	[relative]
   e31: check(S(v1,v2())) ->= S(check(v1),v2())	[relative]
   e32: S(v1,ok(v2())) ->= ok(S(v1,v2()))	[relative]
   e33: S(ok(v1),v2()) ->= ok(S(v1,v2()))	[relative]
   e34: check(sys(v1,v2(),v3(),v4)) ->= sys(v1,v2(),v3(),check(v4))	[relative]
   e35: check(sys(v1,v2(),v3(),v4)) ->= sys(v1,v2(),check(v3()),v4)	[relative]
   e36: check(sys(v1,v2(),v3(),v4)) ->= sys(v1,check(v2()),v3(),v4)	[relative]
   e37: check(sys(v1,v2(),v3(),v4)) ->= sys(check(v1),v2(),v3(),v4)	[relative]
   e38: sys(v1,v2(),v3(),ok(v4)) ->= ok(sys(v1,v2(),v3(),v4))	[relative]
   e39: sys(v1,v2(),ok(v3()),v4) ->= ok(sys(v1,v2(),v3(),v4))	[relative]
   e40: sys(v1,ok(v2()),v3(),v4) ->= ok(sys(v1,v2(),v3(),v4))	[relative]
   e41: sys(ok(v1),v2(),v3(),v4) ->= ok(sys(v1,v2(),v3(),v4))	[relative]
Weak rule e2 calls a strict rule