Input TRS:
    1: top(ok(left(car(x,y),z))) -> top(check(right(y,z)))
    2: top(ok(right(x,car(y,z)))) -> top(check(left(x,z)))
    3: top(ok(left(bot(),x))) -> top(check(right(bot(),x)))
    4: top(ok(right(x,bot()))) -> top(check(left(x,bot())))
   e1: top(ok(left(car(x,y),z))) ->= top(check(left(y,z)))	[relative]
   e2: top(ok(right(x,car(y,z)))) ->= top(check(right(x,z)))	[relative]
   e3: bot() ->= car(new(),bot())	[relative]
   e4: check(old()) ->= ok(old())	[relative]
   e5: check(car(x,y)) ->= car(check(x),y)	[relative]
   e6: check(car(x,y)) ->= car(x,check(y))	[relative]
   e7: check(left(x,y)) ->= left(check(x),y)	[relative]
   e8: check(left(x,y)) ->= left(x,check(y))	[relative]
   e9: check(right(x,y)) ->= right(check(x),y)	[relative]
   e10: check(right(x,y)) ->= right(x,check(y))	[relative]
   e11: car(ok(x),y) ->= ok(car(x,y))	[relative]
   e12: car(x,ok(y)) ->= ok(car(x,y))	[relative]
   e13: left(ok(x),y) ->= ok(left(x,y))	[relative]
   e14: left(x,ok(y)) ->= ok(left(x,y))	[relative]
   e15: right(ok(x),y) ->= ok(right(x,y))	[relative]
   e16: right(x,ok(y)) ->= ok(right(x,y))	[relative]
Dependency Pairs:
   #1: # top(ok(right(x,car(y,z)))) -> # top(check(left(x,z)))
   #2: # top(ok(left(car(x,y),z))) -> # top(check(left(y,z)))	[relative]
   #3: # top(ok(right(x,car(y,z)))) -> # top(check(right(x,z)))	[relative]
   #4: # top(ok(left(bot(),x))) -> # top(check(right(bot(),x)))
   #5: # top(ok(left(car(x,y),z))) -> # top(check(right(y,z)))
   #6: # top(ok(right(x,bot()))) -> # top(check(left(x,bot())))
Number of SCCs: 1
  SCC { #1..6 }
    POLO(Sum)... QLPOS... QWPOpS(mSum)... Mat2b... failed.