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]
Number of Rules: 1
Direct POLO(Sum) ...Direct Mat2b ... failed.
Dependency Pairs:
   #1: # T(ok(sys(S(b,c(d,ds)),x,y,F(b)))) -> # T(check(sys(S(not(b),ds),x,y,bot())))	[relative]
   #2: # T(ok(sys(x,y,R(b),bot()))) -> # T(check(sys(x,y,R(b),F(not(b)))))	[relative]
   #3: # T(ok(sys(x,P(d,b),R(b),y))) -> # T(check(sys(x,bot(),R(not(b)),y)))
   #4: # 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]
Number of SCCs: 1
  SCC { #1 #2 #4 }
    POLO(Sum)... removes: #4
	I(1) = 0
	I(new) = 1
	I(# T) = max(x1 - 4, 0)
	I(S) = max(x1 - 1, 0)
	I(v2) = 1
	I(T) = 1
	I(F) = 1
	I(v3) = 1
	I(bot) = 4
	I(nils) = 0
	I(c) = max(x2 - 2, 0)
	I(f) = max(x1 + 4, 0)
	I(check) = max(x1, 0)
	I(sys) = max(x1 + x2 + x3 + 2, 0)
	I(p) = 4
	I(ok) = max(x1, 0)
	I(0) = 0
	I(R) = max(x1 + 1, 0)
	I(old) = 1
	I(P) = 0
	I(not) = max(x1 - 8, 0)
Number of SCCs: 1
  SCC { #1 #2 }
    POLO(Sum)... QLPOS... QWPOpS(mSum)... Mat2b... removes: #2
	I(1) = [1;1]
	I(new) = [0;0]
	I(# T) = [1,0;1,0] * x1
	I(S) = [0,0;1,0] * x2 + [3;1]
	I(v2) = [1;0]
	I(T) = [0;0]
	I(F) = [2;1]
	I(v3) = [0;1]
	I(bot) = [1;1]
	I(nils) = [1;1]
	I(c) = [1,0;0,0] * x2
	I(f) = [2;1]
	I(check) = [3;5]
	I(sys) = [0,0;1,0] * x3 + [3;2]
	I(p) = [0,0;1,0] * x2 + [3;1]
	I(ok) = [0,1;0,1] * x1 + [1;0]
	I(0) = [2;1]
	I(R) = [2;1]
	I(old) = [1;1]
	I(P) = [0,0;1,0] * x2 + [2;0]
	I(not) = [2;1]
Number of SCCs: 1
  SCC { #1 }
    POLO(Sum)... removes: #1
	I(1) = 0
	I(new) = 0
	I(# T) = max(x1 - 19, 0)
	I(S) = max(x2 - 6, 0)
	I(v2) = 3
	I(T) = 1
	I(F) = max(x1 + 12, 0)
	I(v3) = 1
	I(bot) = 1
	I(nils) = 7
	I(c) = 7
	I(f) = max(x1 + 8, 0)
	I(check) = max(x1 + 7, 0)
	I(sys) = max(x4 + 10, 0)
	I(p) = 11
	I(ok) = max(x1 - 2, 0)
	I(0) = 0
	I(R) = 8
	I(old) = 3
	I(P) = 1
	I(not) = max(x1 - 11, 0)
Number of SCCs: 0