MAYBE
Time: 0.016972
TRS:
 {              active p X -> p active X,
              active p 0() -> mark 0(),
              active p s X -> mark X,
                active s X -> s active X,
        active leq(X1, X2) -> leq(X1, active X2),
        active leq(X1, X2) -> leq(active X1, X2),
        active leq(0(), Y) -> mark true(),
      active leq(s X, 0()) -> mark false(),
      active leq(s X, s Y) -> mark leq(X, Y),
     active if(X1, X2, X3) -> if(active X1, X2, X3),
   active if(true(), X, Y) -> mark X,
  active if(false(), X, Y) -> mark Y,
         active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)),
       active diff(X1, X2) -> diff(X1, active X2),
       active diff(X1, X2) -> diff(active X1, X2),
                  p mark X -> mark p X,
                    p ok X -> ok p X,
                  s mark X -> mark s X,
                    s ok X -> ok s X,
          leq(X1, mark X2) -> mark leq(X1, X2),
          leq(mark X1, X2) -> mark leq(X1, X2),
         leq(ok X1, ok X2) -> ok leq(X1, X2),
       if(mark X1, X2, X3) -> mark if(X1, X2, X3),
   if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
         diff(X1, mark X2) -> mark diff(X1, X2),
         diff(mark X1, X2) -> mark diff(X1, X2),
        diff(ok X1, ok X2) -> ok diff(X1, X2),
                proper 0() -> ok 0(),
                proper p X -> p proper X,
                proper s X -> s proper X,
             proper true() -> ok true(),
        proper leq(X1, X2) -> leq(proper X1, proper X2),
            proper false() -> ok false(),
     proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
       proper diff(X1, X2) -> diff(proper X1, proper X2),
                top mark X -> top proper X,
                  top ok X -> top active X}
 DP:
  DP:
   {             active# p X -> active# X,
                 active# p X -> p# active X,
                 active# s X -> active# X,
                 active# s X -> s# active X,
         active# leq(X1, X2) -> active# X1,
         active# leq(X1, X2) -> active# X2,
         active# leq(X1, X2) -> leq#(X1, active X2),
         active# leq(X1, X2) -> leq#(active X1, X2),
       active# leq(s X, s Y) -> leq#(X, Y),
      active# if(X1, X2, X3) -> active# X1,
      active# if(X1, X2, X3) -> if#(active X1, X2, X3),
          active# diff(X, Y) -> p# X,
          active# diff(X, Y) -> s# diff(p X, Y),
          active# diff(X, Y) -> leq#(X, Y),
          active# diff(X, Y) -> if#(leq(X, Y), 0(), s diff(p X, Y)),
          active# diff(X, Y) -> diff#(p X, Y),
        active# diff(X1, X2) -> active# X1,
        active# diff(X1, X2) -> active# X2,
        active# diff(X1, X2) -> diff#(X1, active X2),
        active# diff(X1, X2) -> diff#(active X1, X2),
                   p# mark X -> p# X,
                     p# ok X -> p# X,
                   s# mark X -> s# X,
                     s# ok X -> s# X,
           leq#(X1, mark X2) -> leq#(X1, X2),
           leq#(mark X1, X2) -> leq#(X1, X2),
          leq#(ok X1, ok X2) -> leq#(X1, X2),
        if#(mark X1, X2, X3) -> if#(X1, X2, X3),
    if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3),
          diff#(X1, mark X2) -> diff#(X1, X2),
          diff#(mark X1, X2) -> diff#(X1, X2),
         diff#(ok X1, ok X2) -> diff#(X1, X2),
                 proper# p X -> p# proper X,
                 proper# p X -> proper# X,
                 proper# s X -> s# proper X,
                 proper# s X -> proper# X,
         proper# leq(X1, X2) -> leq#(proper X1, proper X2),
         proper# leq(X1, X2) -> proper# X1,
         proper# leq(X1, X2) -> proper# X2,
      proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3),
      proper# if(X1, X2, X3) -> proper# X1,
      proper# if(X1, X2, X3) -> proper# X2,
      proper# if(X1, X2, X3) -> proper# X3,
        proper# diff(X1, X2) -> diff#(proper X1, proper X2),
        proper# diff(X1, X2) -> proper# X1,
        proper# diff(X1, X2) -> proper# X2,
                 top# mark X -> proper# X,
                 top# mark X -> top# proper X,
                   top# ok X -> active# X,
                   top# ok X -> top# active X}
  TRS:
  {              active p X -> p active X,
               active p 0() -> mark 0(),
               active p s X -> mark X,
                 active s X -> s active X,
         active leq(X1, X2) -> leq(X1, active X2),
         active leq(X1, X2) -> leq(active X1, X2),
         active leq(0(), Y) -> mark true(),
       active leq(s X, 0()) -> mark false(),
       active leq(s X, s Y) -> mark leq(X, Y),
      active if(X1, X2, X3) -> if(active X1, X2, X3),
    active if(true(), X, Y) -> mark X,
   active if(false(), X, Y) -> mark Y,
          active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)),
        active diff(X1, X2) -> diff(X1, active X2),
        active diff(X1, X2) -> diff(active X1, X2),
                   p mark X -> mark p X,
                     p ok X -> ok p X,
                   s mark X -> mark s X,
                     s ok X -> ok s X,
           leq(X1, mark X2) -> mark leq(X1, X2),
           leq(mark X1, X2) -> mark leq(X1, X2),
          leq(ok X1, ok X2) -> ok leq(X1, X2),
        if(mark X1, X2, X3) -> mark if(X1, X2, X3),
    if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
          diff(X1, mark X2) -> mark diff(X1, X2),
          diff(mark X1, X2) -> mark diff(X1, X2),
         diff(ok X1, ok X2) -> ok diff(X1, X2),
                 proper 0() -> ok 0(),
                 proper p X -> p proper X,
                 proper s X -> s proper X,
              proper true() -> ok true(),
         proper leq(X1, X2) -> leq(proper X1, proper X2),
             proper false() -> ok false(),
      proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
        proper diff(X1, X2) -> diff(proper X1, proper X2),
                 top mark X -> top proper X,
                   top ok X -> top active X}
  EDG:
   {
    (active# if(X1, X2, X3) -> if#(active X1, X2, X3), if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3))
    (active# if(X1, X2, X3) -> if#(active X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
    (if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3), if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3))
    (if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
    (active# leq(X1, X2) -> active# X2, active# diff(X1, X2) -> diff#(active X1, X2))
    (active# leq(X1, X2) -> active# X2, active# diff(X1, X2) -> diff#(X1, active X2))
    (active# leq(X1, X2) -> active# X2, active# diff(X1, X2) -> active# X2)
    (active# leq(X1, X2) -> active# X2, active# diff(X1, X2) -> active# X1)
    (active# leq(X1, X2) -> active# X2, active# diff(X, Y) -> diff#(p X, Y))
    (active# leq(X1, X2) -> active# X2, active# diff(X, Y) -> if#(leq(X, Y), 0(), s diff(p X, Y)))
    (active# leq(X1, X2) -> active# X2, active# diff(X, Y) -> leq#(X, Y))
    (active# leq(X1, X2) -> active# X2, active# diff(X, Y) -> s# diff(p X, Y))
    (active# leq(X1, X2) -> active# X2, active# diff(X, Y) -> p# X)
    (active# leq(X1, X2) -> active# X2, active# if(X1, X2, X3) -> if#(active X1, X2, X3))
    (active# leq(X1, X2) -> active# X2, active# if(X1, X2, X3) -> active# X1)
    (active# leq(X1, X2) -> active# X2, active# leq(s X, s Y) -> leq#(X, Y))
    (active# leq(X1, X2) -> active# X2, active# leq(X1, X2) -> leq#(active X1, X2))
    (active# leq(X1, X2) -> active# X2, active# leq(X1, X2) -> leq#(X1, active X2))
    (active# leq(X1, X2) -> active# X2, active# leq(X1, X2) -> active# X2)
    (active# leq(X1, X2) -> active# X2, active# leq(X1, X2) -> active# X1)
    (active# leq(X1, X2) -> active# X2, active# s X -> s# active X)
    (active# leq(X1, X2) -> active# X2, active# s X -> active# X)
    (active# leq(X1, X2) -> active# X2, active# p X -> p# active X)
    (active# leq(X1, X2) -> active# X2, active# p X -> active# X)
    (proper# leq(X1, X2) -> proper# X2, proper# diff(X1, X2) -> proper# X2)
    (proper# leq(X1, X2) -> proper# X2, proper# diff(X1, X2) -> proper# X1)
    (proper# leq(X1, X2) -> proper# X2, proper# diff(X1, X2) -> diff#(proper X1, proper X2))
    (proper# leq(X1, X2) -> proper# X2, proper# if(X1, X2, X3) -> proper# X3)
    (proper# leq(X1, X2) -> proper# X2, proper# if(X1, X2, X3) -> proper# X2)
    (proper# leq(X1, X2) -> proper# X2, proper# if(X1, X2, X3) -> proper# X1)
    (proper# leq(X1, X2) -> proper# X2, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
    (proper# leq(X1, X2) -> proper# X2, proper# leq(X1, X2) -> proper# X2)
    (proper# leq(X1, X2) -> proper# X2, proper# leq(X1, X2) -> proper# X1)
    (proper# leq(X1, X2) -> proper# X2, proper# leq(X1, X2) -> leq#(proper X1, proper X2))
    (proper# leq(X1, X2) -> proper# X2, proper# s X -> proper# X)
    (proper# leq(X1, X2) -> proper# X2, proper# s X -> s# proper X)
    (proper# leq(X1, X2) -> proper# X2, proper# p X -> proper# X)
    (proper# leq(X1, X2) -> proper# X2, proper# p X -> p# proper X)
    (proper# diff(X1, X2) -> proper# X2, proper# diff(X1, X2) -> proper# X2)
    (proper# diff(X1, X2) -> proper# X2, proper# diff(X1, X2) -> proper# X1)
    (proper# diff(X1, X2) -> proper# X2, proper# diff(X1, X2) -> diff#(proper X1, proper X2))
    (proper# diff(X1, X2) -> proper# X2, proper# if(X1, X2, X3) -> proper# X3)
    (proper# diff(X1, X2) -> proper# X2, proper# if(X1, X2, X3) -> proper# X2)
    (proper# diff(X1, X2) -> proper# X2, proper# if(X1, X2, X3) -> proper# X1)
    (proper# diff(X1, X2) -> proper# X2, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
    (proper# diff(X1, X2) -> proper# X2, proper# leq(X1, X2) -> proper# X2)
    (proper# diff(X1, X2) -> proper# X2, proper# leq(X1, X2) -> proper# X1)
    (proper# diff(X1, X2) -> proper# X2, proper# leq(X1, X2) -> leq#(proper X1, proper X2))
    (proper# diff(X1, X2) -> proper# X2, proper# s X -> proper# X)
    (proper# diff(X1, X2) -> proper# X2, proper# s X -> s# proper X)
    (proper# diff(X1, X2) -> proper# X2, proper# p X -> proper# X)
    (proper# diff(X1, X2) -> proper# X2, proper# p X -> p# proper X)
    (active# s X -> s# active X, s# ok X -> s# X)
    (active# s X -> s# active X, s# mark X -> s# X)
    (proper# s X -> s# proper X, s# ok X -> s# X)
    (proper# s X -> s# proper X, s# mark X -> s# X)
    (top# ok X -> top# active X, top# ok X -> top# active X)
    (top# ok X -> top# active X, top# ok X -> active# X)
    (top# ok X -> top# active X, top# mark X -> top# proper X)
    (top# ok X -> top# active X, top# mark X -> proper# X)
    (active# diff(X1, X2) -> diff#(active X1, X2), diff#(ok X1, ok X2) -> diff#(X1, X2))
    (active# diff(X1, X2) -> diff#(active X1, X2), diff#(mark X1, X2) -> diff#(X1, X2))
    (active# diff(X1, X2) -> diff#(active X1, X2), diff#(X1, mark X2) -> diff#(X1, X2))
    (active# diff(X, Y) -> s# diff(p X, Y), s# ok X -> s# X)
    (active# diff(X, Y) -> s# diff(p X, Y), s# mark X -> s# X)
    (active# s X -> active# X, active# diff(X1, X2) -> diff#(active X1, X2))
    (active# s X -> active# X, active# diff(X1, X2) -> diff#(X1, active X2))
    (active# s X -> active# X, active# diff(X1, X2) -> active# X2)
    (active# s X -> active# X, active# diff(X1, X2) -> active# X1)
    (active# s X -> active# X, active# diff(X, Y) -> diff#(p X, Y))
    (active# s X -> active# X, active# diff(X, Y) -> if#(leq(X, Y), 0(), s diff(p X, Y)))
    (active# s X -> active# X, active# diff(X, Y) -> leq#(X, Y))
    (active# s X -> active# X, active# diff(X, Y) -> s# diff(p X, Y))
    (active# s X -> active# X, active# diff(X, Y) -> p# X)
    (active# s X -> active# X, active# if(X1, X2, X3) -> if#(active X1, X2, X3))
    (active# s X -> active# X, active# if(X1, X2, X3) -> active# X1)
    (active# s X -> active# X, active# leq(s X, s Y) -> leq#(X, Y))
    (active# s X -> active# X, active# leq(X1, X2) -> leq#(active X1, X2))
    (active# s X -> active# X, active# leq(X1, X2) -> leq#(X1, active X2))
    (active# s X -> active# X, active# leq(X1, X2) -> active# X2)
    (active# s X -> active# X, active# leq(X1, X2) -> active# X1)
    (active# s X -> active# X, active# s X -> s# active X)
    (active# s X -> active# X, active# s X -> active# X)
    (active# s X -> active# X, active# p X -> p# active X)
    (active# s X -> active# X, active# p X -> active# X)
    (p# mark X -> p# X, p# ok X -> p# X)
    (p# mark X -> p# X, p# mark X -> p# X)
    (s# mark X -> s# X, s# ok X -> s# X)
    (s# mark X -> s# X, s# mark X -> s# X)
    (proper# p X -> proper# X, proper# diff(X1, X2) -> proper# X2)
    (proper# p X -> proper# X, proper# diff(X1, X2) -> proper# X1)
    (proper# p X -> proper# X, proper# diff(X1, X2) -> diff#(proper X1, proper X2))
    (proper# p X -> proper# X, proper# if(X1, X2, X3) -> proper# X3)
    (proper# p X -> proper# X, proper# if(X1, X2, X3) -> proper# X2)
    (proper# p X -> proper# X, proper# if(X1, X2, X3) -> proper# X1)
    (proper# p X -> proper# X, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
    (proper# p X -> proper# X, proper# leq(X1, X2) -> proper# X2)
    (proper# p X -> proper# X, proper# leq(X1, X2) -> proper# X1)
    (proper# p X -> proper# X, proper# leq(X1, X2) -> leq#(proper X1, proper X2))
    (proper# p X -> proper# X, proper# s X -> proper# X)
    (proper# p X -> proper# X, proper# s X -> s# proper X)
    (proper# p X -> proper# X, proper# p X -> proper# X)
    (proper# p X -> proper# X, proper# p X -> p# proper X)
    (top# mark X -> proper# X, proper# diff(X1, X2) -> proper# X2)
    (top# mark X -> proper# X, proper# diff(X1, X2) -> proper# X1)
    (top# mark X -> proper# X, proper# diff(X1, X2) -> diff#(proper X1, proper X2))
    (top# mark X -> proper# X, proper# if(X1, X2, X3) -> proper# X3)
    (top# mark X -> proper# X, proper# if(X1, X2, X3) -> proper# X2)
    (top# mark X -> proper# X, proper# if(X1, X2, X3) -> proper# X1)
    (top# mark X -> proper# X, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
    (top# mark X -> proper# X, proper# leq(X1, X2) -> proper# X2)
    (top# mark X -> proper# X, proper# leq(X1, X2) -> proper# X1)
    (top# mark X -> proper# X, proper# leq(X1, X2) -> leq#(proper X1, proper X2))
    (top# mark X -> proper# X, proper# s X -> proper# X)
    (top# mark X -> proper# X, proper# s X -> s# proper X)
    (top# mark X -> proper# X, proper# p X -> proper# X)
    (top# mark X -> proper# X, proper# p X -> p# proper X)
    (active# leq(X1, X2) -> leq#(X1, active X2), leq#(ok X1, ok X2) -> leq#(X1, X2))
    (active# leq(X1, X2) -> leq#(X1, active X2), leq#(mark X1, X2) -> leq#(X1, X2))
    (active# leq(X1, X2) -> leq#(X1, active X2), leq#(X1, mark X2) -> leq#(X1, X2))
    (proper# leq(X1, X2) -> leq#(proper X1, proper X2), leq#(ok X1, ok X2) -> leq#(X1, X2))
    (proper# leq(X1, X2) -> leq#(proper X1, proper X2), leq#(mark X1, X2) -> leq#(X1, X2))
    (proper# leq(X1, X2) -> leq#(proper X1, proper X2), leq#(X1, mark X2) -> leq#(X1, X2))
    (leq#(X1, mark X2) -> leq#(X1, X2), leq#(ok X1, ok X2) -> leq#(X1, X2))
    (leq#(X1, mark X2) -> leq#(X1, X2), leq#(mark X1, X2) -> leq#(X1, X2))
    (leq#(X1, mark X2) -> leq#(X1, X2), leq#(X1, mark X2) -> leq#(X1, X2))
    (leq#(ok X1, ok X2) -> leq#(X1, X2), leq#(ok X1, ok X2) -> leq#(X1, X2))
    (leq#(ok X1, ok X2) -> leq#(X1, X2), leq#(mark X1, X2) -> leq#(X1, X2))
    (leq#(ok X1, ok X2) -> leq#(X1, X2), leq#(X1, mark X2) -> leq#(X1, X2))
    (diff#(mark X1, X2) -> diff#(X1, X2), diff#(ok X1, ok X2) -> diff#(X1, X2))
    (diff#(mark X1, X2) -> diff#(X1, X2), diff#(mark X1, X2) -> diff#(X1, X2))
    (diff#(mark X1, X2) -> diff#(X1, X2), diff#(X1, mark X2) -> diff#(X1, X2))
    (active# diff(X, Y) -> diff#(p X, Y), diff#(ok X1, ok X2) -> diff#(X1, X2))
    (active# diff(X, Y) -> diff#(p X, Y), diff#(mark X1, X2) -> diff#(X1, X2))
    (active# diff(X, Y) -> diff#(p X, Y), diff#(X1, mark X2) -> diff#(X1, X2))
    (active# if(X1, X2, X3) -> active# X1, active# diff(X1, X2) -> diff#(active X1, X2))
    (active# if(X1, X2, X3) -> active# X1, active# diff(X1, X2) -> diff#(X1, active X2))
    (active# if(X1, X2, X3) -> active# X1, active# diff(X1, X2) -> active# X2)
    (active# if(X1, X2, X3) -> active# X1, active# diff(X1, X2) -> active# X1)
    (active# if(X1, X2, X3) -> active# X1, active# diff(X, Y) -> diff#(p X, Y))
    (active# if(X1, X2, X3) -> active# X1, active# diff(X, Y) -> if#(leq(X, Y), 0(), s diff(p X, Y)))
    (active# if(X1, X2, X3) -> active# X1, active# diff(X, Y) -> leq#(X, Y))
    (active# if(X1, X2, X3) -> active# X1, active# diff(X, Y) -> s# diff(p X, Y))
    (active# if(X1, X2, X3) -> active# X1, active# diff(X, Y) -> p# X)
    (active# if(X1, X2, X3) -> active# X1, active# if(X1, X2, X3) -> if#(active X1, X2, X3))
    (active# if(X1, X2, X3) -> active# X1, active# if(X1, X2, X3) -> active# X1)
    (active# if(X1, X2, X3) -> active# X1, active# leq(s X, s Y) -> leq#(X, Y))
    (active# if(X1, X2, X3) -> active# X1, active# leq(X1, X2) -> leq#(active X1, X2))
    (active# if(X1, X2, X3) -> active# X1, active# leq(X1, X2) -> leq#(X1, active X2))
    (active# if(X1, X2, X3) -> active# X1, active# leq(X1, X2) -> active# X2)
    (active# if(X1, X2, X3) -> active# X1, active# leq(X1, X2) -> active# X1)
    (active# if(X1, X2, X3) -> active# X1, active# s X -> s# active X)
    (active# if(X1, X2, X3) -> active# X1, active# s X -> active# X)
    (active# if(X1, X2, X3) -> active# X1, active# p X -> p# active X)
    (active# if(X1, X2, X3) -> active# X1, active# p X -> active# X)
    (proper# leq(X1, X2) -> proper# X1, proper# diff(X1, X2) -> proper# X2)
    (proper# leq(X1, X2) -> proper# X1, proper# diff(X1, X2) -> proper# X1)
    (proper# leq(X1, X2) -> proper# X1, proper# diff(X1, X2) -> diff#(proper X1, proper X2))
    (proper# leq(X1, X2) -> proper# X1, proper# if(X1, X2, X3) -> proper# X3)
    (proper# leq(X1, X2) -> proper# X1, proper# if(X1, X2, X3) -> proper# X2)
    (proper# leq(X1, X2) -> proper# X1, proper# if(X1, X2, X3) -> proper# X1)
    (proper# leq(X1, X2) -> proper# X1, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
    (proper# leq(X1, X2) -> proper# X1, proper# leq(X1, X2) -> proper# X2)
    (proper# leq(X1, X2) -> proper# X1, proper# leq(X1, X2) -> proper# X1)
    (proper# leq(X1, X2) -> proper# X1, proper# leq(X1, X2) -> leq#(proper X1, proper X2))
    (proper# leq(X1, X2) -> proper# X1, proper# s X -> proper# X)
    (proper# leq(X1, X2) -> proper# X1, proper# s X -> s# proper X)
    (proper# leq(X1, X2) -> proper# X1, proper# p X -> proper# X)
    (proper# leq(X1, X2) -> proper# X1, proper# p X -> p# proper X)
    (proper# diff(X1, X2) -> proper# X1, proper# diff(X1, X2) -> proper# X2)
    (proper# diff(X1, X2) -> proper# X1, proper# diff(X1, X2) -> proper# X1)
    (proper# diff(X1, X2) -> proper# X1, proper# diff(X1, X2) -> diff#(proper X1, proper X2))
    (proper# diff(X1, X2) -> proper# X1, proper# if(X1, X2, X3) -> proper# X3)
    (proper# diff(X1, X2) -> proper# X1, proper# if(X1, X2, X3) -> proper# X2)
    (proper# diff(X1, X2) -> proper# X1, proper# if(X1, X2, X3) -> proper# X1)
    (proper# diff(X1, X2) -> proper# X1, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
    (proper# diff(X1, X2) -> proper# X1, proper# leq(X1, X2) -> proper# X2)
    (proper# diff(X1, X2) -> proper# X1, proper# leq(X1, X2) -> proper# X1)
    (proper# diff(X1, X2) -> proper# X1, proper# leq(X1, X2) -> leq#(proper X1, proper X2))
    (proper# diff(X1, X2) -> proper# X1, proper# s X -> proper# X)
    (proper# diff(X1, X2) -> proper# X1, proper# s X -> s# proper X)
    (proper# diff(X1, X2) -> proper# X1, proper# p X -> proper# X)
    (proper# diff(X1, X2) -> proper# X1, proper# p X -> p# proper X)
    (active# diff(X, Y) -> leq#(X, Y), leq#(ok X1, ok X2) -> leq#(X1, X2))
    (active# diff(X, Y) -> leq#(X, Y), leq#(mark X1, X2) -> leq#(X1, X2))
    (active# diff(X, Y) -> leq#(X, Y), leq#(X1, mark X2) -> leq#(X1, X2))
    (active# leq(s X, s Y) -> leq#(X, Y), leq#(X1, mark X2) -> leq#(X1, X2))
    (active# leq(s X, s Y) -> leq#(X, Y), leq#(mark X1, X2) -> leq#(X1, X2))
    (active# leq(s X, s Y) -> leq#(X, Y), leq#(ok X1, ok X2) -> leq#(X1, X2))
    (proper# if(X1, X2, X3) -> proper# X1, proper# p X -> p# proper X)
    (proper# if(X1, X2, X3) -> proper# X1, proper# p X -> proper# X)
    (proper# if(X1, X2, X3) -> proper# X1, proper# s X -> s# proper X)
    (proper# if(X1, X2, X3) -> proper# X1, proper# s X -> proper# X)
    (proper# if(X1, X2, X3) -> proper# X1, proper# leq(X1, X2) -> leq#(proper X1, proper X2))
    (proper# if(X1, X2, X3) -> proper# X1, proper# leq(X1, X2) -> proper# X1)
    (proper# if(X1, X2, X3) -> proper# X1, proper# leq(X1, X2) -> proper# X2)
    (proper# if(X1, X2, X3) -> proper# X1, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
    (proper# if(X1, X2, X3) -> proper# X1, proper# if(X1, X2, X3) -> proper# X1)
    (proper# if(X1, X2, X3) -> proper# X1, proper# if(X1, X2, X3) -> proper# X2)
    (proper# if(X1, X2, X3) -> proper# X1, proper# if(X1, X2, X3) -> proper# X3)
    (proper# if(X1, X2, X3) -> proper# X1, proper# diff(X1, X2) -> diff#(proper X1, proper X2))
    (proper# if(X1, X2, X3) -> proper# X1, proper# diff(X1, X2) -> proper# X1)
    (proper# if(X1, X2, X3) -> proper# X1, proper# diff(X1, X2) -> proper# X2)
    (active# diff(X1, X2) -> active# X1, active# p X -> active# X)
    (active# diff(X1, X2) -> active# X1, active# p X -> p# active X)
    (active# diff(X1, X2) -> active# X1, active# s X -> active# X)
    (active# diff(X1, X2) -> active# X1, active# s X -> s# active X)
    (active# diff(X1, X2) -> active# X1, active# leq(X1, X2) -> active# X1)
    (active# diff(X1, X2) -> active# X1, active# leq(X1, X2) -> active# X2)
    (active# diff(X1, X2) -> active# X1, active# leq(X1, X2) -> leq#(X1, active X2))
    (active# diff(X1, X2) -> active# X1, active# leq(X1, X2) -> leq#(active X1, X2))
    (active# diff(X1, X2) -> active# X1, active# leq(s X, s Y) -> leq#(X, Y))
    (active# diff(X1, X2) -> active# X1, active# if(X1, X2, X3) -> active# X1)
    (active# diff(X1, X2) -> active# X1, active# if(X1, X2, X3) -> if#(active X1, X2, X3))
    (active# diff(X1, X2) -> active# X1, active# diff(X, Y) -> p# X)
    (active# diff(X1, X2) -> active# X1, active# diff(X, Y) -> s# diff(p X, Y))
    (active# diff(X1, X2) -> active# X1, active# diff(X, Y) -> leq#(X, Y))
    (active# diff(X1, X2) -> active# X1, active# diff(X, Y) -> if#(leq(X, Y), 0(), s diff(p X, Y)))
    (active# diff(X1, X2) -> active# X1, active# diff(X, Y) -> diff#(p X, Y))
    (active# diff(X1, X2) -> active# X1, active# diff(X1, X2) -> active# X1)
    (active# diff(X1, X2) -> active# X1, active# diff(X1, X2) -> active# X2)
    (active# diff(X1, X2) -> active# X1, active# diff(X1, X2) -> diff#(X1, active X2))
    (active# diff(X1, X2) -> active# X1, active# diff(X1, X2) -> diff#(active X1, X2))
    (active# leq(X1, X2) -> active# X1, active# p X -> active# X)
    (active# leq(X1, X2) -> active# X1, active# p X -> p# active X)
    (active# leq(X1, X2) -> active# X1, active# s X -> active# X)
    (active# leq(X1, X2) -> active# X1, active# s X -> s# active X)
    (active# leq(X1, X2) -> active# X1, active# leq(X1, X2) -> active# X1)
    (active# leq(X1, X2) -> active# X1, active# leq(X1, X2) -> active# X2)
    (active# leq(X1, X2) -> active# X1, active# leq(X1, X2) -> leq#(X1, active X2))
    (active# leq(X1, X2) -> active# X1, active# leq(X1, X2) -> leq#(active X1, X2))
    (active# leq(X1, X2) -> active# X1, active# leq(s X, s Y) -> leq#(X, Y))
    (active# leq(X1, X2) -> active# X1, active# if(X1, X2, X3) -> active# X1)
    (active# leq(X1, X2) -> active# X1, active# if(X1, X2, X3) -> if#(active X1, X2, X3))
    (active# leq(X1, X2) -> active# X1, active# diff(X, Y) -> p# X)
    (active# leq(X1, X2) -> active# X1, active# diff(X, Y) -> s# diff(p X, Y))
    (active# leq(X1, X2) -> active# X1, active# diff(X, Y) -> leq#(X, Y))
    (active# leq(X1, X2) -> active# X1, active# diff(X, Y) -> if#(leq(X, Y), 0(), s diff(p X, Y)))
    (active# leq(X1, X2) -> active# X1, active# diff(X, Y) -> diff#(p X, Y))
    (active# leq(X1, X2) -> active# X1, active# diff(X1, X2) -> active# X1)
    (active# leq(X1, X2) -> active# X1, active# diff(X1, X2) -> active# X2)
    (active# leq(X1, X2) -> active# X1, active# diff(X1, X2) -> diff#(X1, active X2))
    (active# leq(X1, X2) -> active# X1, active# diff(X1, X2) -> diff#(active X1, X2))
    (diff#(ok X1, ok X2) -> diff#(X1, X2), diff#(X1, mark X2) -> diff#(X1, X2))
    (diff#(ok X1, ok X2) -> diff#(X1, X2), diff#(mark X1, X2) -> diff#(X1, X2))
    (diff#(ok X1, ok X2) -> diff#(X1, X2), diff#(ok X1, ok X2) -> diff#(X1, X2))
    (diff#(X1, mark X2) -> diff#(X1, X2), diff#(X1, mark X2) -> diff#(X1, X2))
    (diff#(X1, mark X2) -> diff#(X1, X2), diff#(mark X1, X2) -> diff#(X1, X2))
    (diff#(X1, mark X2) -> diff#(X1, X2), diff#(ok X1, ok X2) -> diff#(X1, X2))
    (leq#(mark X1, X2) -> leq#(X1, X2), leq#(X1, mark X2) -> leq#(X1, X2))
    (leq#(mark X1, X2) -> leq#(X1, X2), leq#(mark X1, X2) -> leq#(X1, X2))
    (leq#(mark X1, X2) -> leq#(X1, X2), leq#(ok X1, ok X2) -> leq#(X1, X2))
    (proper# diff(X1, X2) -> diff#(proper X1, proper X2), diff#(X1, mark X2) -> diff#(X1, X2))
    (proper# diff(X1, X2) -> diff#(proper X1, proper X2), diff#(mark X1, X2) -> diff#(X1, X2))
    (proper# diff(X1, X2) -> diff#(proper X1, proper X2), diff#(ok X1, ok X2) -> diff#(X1, X2))
    (active# diff(X1, X2) -> diff#(X1, active X2), diff#(X1, mark X2) -> diff#(X1, X2))
    (active# diff(X1, X2) -> diff#(X1, active X2), diff#(mark X1, X2) -> diff#(X1, X2))
    (active# diff(X1, X2) -> diff#(X1, active X2), diff#(ok X1, ok X2) -> diff#(X1, X2))
    (top# ok X -> active# X, active# p X -> active# X)
    (top# ok X -> active# X, active# p X -> p# active X)
    (top# ok X -> active# X, active# s X -> active# X)
    (top# ok X -> active# X, active# s X -> s# active X)
    (top# ok X -> active# X, active# leq(X1, X2) -> active# X1)
    (top# ok X -> active# X, active# leq(X1, X2) -> active# X2)
    (top# ok X -> active# X, active# leq(X1, X2) -> leq#(X1, active X2))
    (top# ok X -> active# X, active# leq(X1, X2) -> leq#(active X1, X2))
    (top# ok X -> active# X, active# leq(s X, s Y) -> leq#(X, Y))
    (top# ok X -> active# X, active# if(X1, X2, X3) -> active# X1)
    (top# ok X -> active# X, active# if(X1, X2, X3) -> if#(active X1, X2, X3))
    (top# ok X -> active# X, active# diff(X, Y) -> p# X)
    (top# ok X -> active# X, active# diff(X, Y) -> s# diff(p X, Y))
    (top# ok X -> active# X, active# diff(X, Y) -> leq#(X, Y))
    (top# ok X -> active# X, active# diff(X, Y) -> if#(leq(X, Y), 0(), s diff(p X, Y)))
    (top# ok X -> active# X, active# diff(X, Y) -> diff#(p X, Y))
    (top# ok X -> active# X, active# diff(X1, X2) -> active# X1)
    (top# ok X -> active# X, active# diff(X1, X2) -> active# X2)
    (top# ok X -> active# X, active# diff(X1, X2) -> diff#(X1, active X2))
    (top# ok X -> active# X, active# diff(X1, X2) -> diff#(active X1, X2))
    (proper# s X -> proper# X, proper# p X -> p# proper X)
    (proper# s X -> proper# X, proper# p X -> proper# X)
    (proper# s X -> proper# X, proper# s X -> s# proper X)
    (proper# s X -> proper# X, proper# s X -> proper# X)
    (proper# s X -> proper# X, proper# leq(X1, X2) -> leq#(proper X1, proper X2))
    (proper# s X -> proper# X, proper# leq(X1, X2) -> proper# X1)
    (proper# s X -> proper# X, proper# leq(X1, X2) -> proper# X2)
    (proper# s X -> proper# X, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
    (proper# s X -> proper# X, proper# if(X1, X2, X3) -> proper# X1)
    (proper# s X -> proper# X, proper# if(X1, X2, X3) -> proper# X2)
    (proper# s X -> proper# X, proper# if(X1, X2, X3) -> proper# X3)
    (proper# s X -> proper# X, proper# diff(X1, X2) -> diff#(proper X1, proper X2))
    (proper# s X -> proper# X, proper# diff(X1, X2) -> proper# X1)
    (proper# s X -> proper# X, proper# diff(X1, X2) -> proper# X2)
    (s# ok X -> s# X, s# mark X -> s# X)
    (s# ok X -> s# X, s# ok X -> s# X)
    (p# ok X -> p# X, p# mark X -> p# X)
    (p# ok X -> p# X, p# ok X -> p# X)
    (active# diff(X, Y) -> p# X, p# mark X -> p# X)
    (active# diff(X, Y) -> p# X, p# ok X -> p# X)
    (active# p X -> active# X, active# p X -> active# X)
    (active# p X -> active# X, active# p X -> p# active X)
    (active# p X -> active# X, active# s X -> active# X)
    (active# p X -> active# X, active# s X -> s# active X)
    (active# p X -> active# X, active# leq(X1, X2) -> active# X1)
    (active# p X -> active# X, active# leq(X1, X2) -> active# X2)
    (active# p X -> active# X, active# leq(X1, X2) -> leq#(X1, active X2))
    (active# p X -> active# X, active# leq(X1, X2) -> leq#(active X1, X2))
    (active# p X -> active# X, active# leq(s X, s Y) -> leq#(X, Y))
    (active# p X -> active# X, active# if(X1, X2, X3) -> active# X1)
    (active# p X -> active# X, active# if(X1, X2, X3) -> if#(active X1, X2, X3))
    (active# p X -> active# X, active# diff(X, Y) -> p# X)
    (active# p X -> active# X, active# diff(X, Y) -> s# diff(p X, Y))
    (active# p X -> active# X, active# diff(X, Y) -> leq#(X, Y))
    (active# p X -> active# X, active# diff(X, Y) -> if#(leq(X, Y), 0(), s diff(p X, Y)))
    (active# p X -> active# X, active# diff(X, Y) -> diff#(p X, Y))
    (active# p X -> active# X, active# diff(X1, X2) -> active# X1)
    (active# p X -> active# X, active# diff(X1, X2) -> active# X2)
    (active# p X -> active# X, active# diff(X1, X2) -> diff#(X1, active X2))
    (active# p X -> active# X, active# diff(X1, X2) -> diff#(active X1, X2))
    (proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
    (proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3), if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3))
    (active# leq(X1, X2) -> leq#(active X1, X2), leq#(X1, mark X2) -> leq#(X1, X2))
    (active# leq(X1, X2) -> leq#(active X1, X2), leq#(mark X1, X2) -> leq#(X1, X2))
    (active# leq(X1, X2) -> leq#(active X1, X2), leq#(ok X1, ok X2) -> leq#(X1, X2))
    (top# mark X -> top# proper X, top# mark X -> proper# X)
    (top# mark X -> top# proper X, top# mark X -> top# proper X)
    (top# mark X -> top# proper X, top# ok X -> active# X)
    (top# mark X -> top# proper X, top# ok X -> top# active X)
    (proper# p X -> p# proper X, p# mark X -> p# X)
    (proper# p X -> p# proper X, p# ok X -> p# X)
    (active# p X -> p# active X, p# mark X -> p# X)
    (active# p X -> p# active X, p# ok X -> p# X)
    (proper# if(X1, X2, X3) -> proper# X2, proper# p X -> p# proper X)
    (proper# if(X1, X2, X3) -> proper# X2, proper# p X -> proper# X)
    (proper# if(X1, X2, X3) -> proper# X2, proper# s X -> s# proper X)
    (proper# if(X1, X2, X3) -> proper# X2, proper# s X -> proper# X)
    (proper# if(X1, X2, X3) -> proper# X2, proper# leq(X1, X2) -> leq#(proper X1, proper X2))
    (proper# if(X1, X2, X3) -> proper# X2, proper# leq(X1, X2) -> proper# X1)
    (proper# if(X1, X2, X3) -> proper# X2, proper# leq(X1, X2) -> proper# X2)
    (proper# if(X1, X2, X3) -> proper# X2, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
    (proper# if(X1, X2, X3) -> proper# X2, proper# if(X1, X2, X3) -> proper# X1)
    (proper# if(X1, X2, X3) -> proper# X2, proper# if(X1, X2, X3) -> proper# X2)
    (proper# if(X1, X2, X3) -> proper# X2, proper# if(X1, X2, X3) -> proper# X3)
    (proper# if(X1, X2, X3) -> proper# X2, proper# diff(X1, X2) -> diff#(proper X1, proper X2))
    (proper# if(X1, X2, X3) -> proper# X2, proper# diff(X1, X2) -> proper# X1)
    (proper# if(X1, X2, X3) -> proper# X2, proper# diff(X1, X2) -> proper# X2)
    (active# diff(X1, X2) -> active# X2, active# p X -> active# X)
    (active# diff(X1, X2) -> active# X2, active# p X -> p# active X)
    (active# diff(X1, X2) -> active# X2, active# s X -> active# X)
    (active# diff(X1, X2) -> active# X2, active# s X -> s# active X)
    (active# diff(X1, X2) -> active# X2, active# leq(X1, X2) -> active# X1)
    (active# diff(X1, X2) -> active# X2, active# leq(X1, X2) -> active# X2)
    (active# diff(X1, X2) -> active# X2, active# leq(X1, X2) -> leq#(X1, active X2))
    (active# diff(X1, X2) -> active# X2, active# leq(X1, X2) -> leq#(active X1, X2))
    (active# diff(X1, X2) -> active# X2, active# leq(s X, s Y) -> leq#(X, Y))
    (active# diff(X1, X2) -> active# X2, active# if(X1, X2, X3) -> active# X1)
    (active# diff(X1, X2) -> active# X2, active# if(X1, X2, X3) -> if#(active X1, X2, X3))
    (active# diff(X1, X2) -> active# X2, active# diff(X, Y) -> p# X)
    (active# diff(X1, X2) -> active# X2, active# diff(X, Y) -> s# diff(p X, Y))
    (active# diff(X1, X2) -> active# X2, active# diff(X, Y) -> leq#(X, Y))
    (active# diff(X1, X2) -> active# X2, active# diff(X, Y) -> if#(leq(X, Y), 0(), s diff(p X, Y)))
    (active# diff(X1, X2) -> active# X2, active# diff(X, Y) -> diff#(p X, Y))
    (active# diff(X1, X2) -> active# X2, active# diff(X1, X2) -> active# X1)
    (active# diff(X1, X2) -> active# X2, active# diff(X1, X2) -> active# X2)
    (active# diff(X1, X2) -> active# X2, active# diff(X1, X2) -> diff#(X1, active X2))
    (active# diff(X1, X2) -> active# X2, active# diff(X1, X2) -> diff#(active X1, X2))
    (active# diff(X, Y) -> if#(leq(X, Y), 0(), s diff(p X, Y)), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
    (active# diff(X, Y) -> if#(leq(X, Y), 0(), s diff(p X, Y)), if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3))
    (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
    (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3))
    (proper# if(X1, X2, X3) -> proper# X3, proper# p X -> p# proper X)
    (proper# if(X1, X2, X3) -> proper# X3, proper# p X -> proper# X)
    (proper# if(X1, X2, X3) -> proper# X3, proper# s X -> s# proper X)
    (proper# if(X1, X2, X3) -> proper# X3, proper# s X -> proper# X)
    (proper# if(X1, X2, X3) -> proper# X3, proper# leq(X1, X2) -> leq#(proper X1, proper X2))
    (proper# if(X1, X2, X3) -> proper# X3, proper# leq(X1, X2) -> proper# X1)
    (proper# if(X1, X2, X3) -> proper# X3, proper# leq(X1, X2) -> proper# X2)
    (proper# if(X1, X2, X3) -> proper# X3, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
    (proper# if(X1, X2, X3) -> proper# X3, proper# if(X1, X2, X3) -> proper# X1)
    (proper# if(X1, X2, X3) -> proper# X3, proper# if(X1, X2, X3) -> proper# X2)
    (proper# if(X1, X2, X3) -> proper# X3, proper# if(X1, X2, X3) -> proper# X3)
    (proper# if(X1, X2, X3) -> proper# X3, proper# diff(X1, X2) -> diff#(proper X1, proper X2))
    (proper# if(X1, X2, X3) -> proper# X3, proper# diff(X1, X2) -> proper# X1)
    (proper# if(X1, X2, X3) -> proper# X3, proper# diff(X1, X2) -> proper# X2)
   }
   STATUS:
    arrows: 0.846800
    SCCS (8):
     Scc:
      {top# mark X -> top# proper X,
         top# ok X -> top# active X}
     Scc:
      {           active# p X -> active# X,
                  active# s X -> active# X,
          active# leq(X1, X2) -> active# X1,
          active# leq(X1, X2) -> active# X2,
       active# if(X1, X2, X3) -> active# X1,
         active# diff(X1, X2) -> active# X1,
         active# diff(X1, X2) -> active# X2}
     Scc:
      {           proper# p X -> proper# X,
                  proper# s X -> proper# X,
          proper# leq(X1, X2) -> proper# X1,
          proper# leq(X1, X2) -> proper# X2,
       proper# if(X1, X2, X3) -> proper# X1,
       proper# if(X1, X2, X3) -> proper# X2,
       proper# if(X1, X2, X3) -> proper# X3,
         proper# diff(X1, X2) -> proper# X1,
         proper# diff(X1, X2) -> proper# X2}
     Scc:
      { diff#(X1, mark X2) -> diff#(X1, X2),
        diff#(mark X1, X2) -> diff#(X1, X2),
       diff#(ok X1, ok X2) -> diff#(X1, X2)}
     Scc:
      {    if#(mark X1, X2, X3) -> if#(X1, X2, X3),
       if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3)}
     Scc:
      { leq#(X1, mark X2) -> leq#(X1, X2),
        leq#(mark X1, X2) -> leq#(X1, X2),
       leq#(ok X1, ok X2) -> leq#(X1, X2)}
     Scc:
      {s# mark X -> s# X,
         s# ok X -> s# X}
     Scc:
      {p# mark X -> p# X,
         p# ok X -> p# X}
     
     SCC (2):
      Strict:
       {top# mark X -> top# proper X,
          top# ok X -> top# active X}
      Weak:
      {              active p X -> p active X,
                   active p 0() -> mark 0(),
                   active p s X -> mark X,
                     active s X -> s active X,
             active leq(X1, X2) -> leq(X1, active X2),
             active leq(X1, X2) -> leq(active X1, X2),
             active leq(0(), Y) -> mark true(),
           active leq(s X, 0()) -> mark false(),
           active leq(s X, s Y) -> mark leq(X, Y),
          active if(X1, X2, X3) -> if(active X1, X2, X3),
        active if(true(), X, Y) -> mark X,
       active if(false(), X, Y) -> mark Y,
              active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)),
            active diff(X1, X2) -> diff(X1, active X2),
            active diff(X1, X2) -> diff(active X1, X2),
                       p mark X -> mark p X,
                         p ok X -> ok p X,
                       s mark X -> mark s X,
                         s ok X -> ok s X,
               leq(X1, mark X2) -> mark leq(X1, X2),
               leq(mark X1, X2) -> mark leq(X1, X2),
              leq(ok X1, ok X2) -> ok leq(X1, X2),
            if(mark X1, X2, X3) -> mark if(X1, X2, X3),
        if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
              diff(X1, mark X2) -> mark diff(X1, X2),
              diff(mark X1, X2) -> mark diff(X1, X2),
             diff(ok X1, ok X2) -> ok diff(X1, X2),
                     proper 0() -> ok 0(),
                     proper p X -> p proper X,
                     proper s X -> s proper X,
                  proper true() -> ok true(),
             proper leq(X1, X2) -> leq(proper X1, proper X2),
                 proper false() -> ok false(),
          proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
            proper diff(X1, X2) -> diff(proper X1, proper X2),
                     top mark X -> top proper X,
                       top ok X -> top active X}
      Open
     
     
     SCC (7):
      Strict:
       {           active# p X -> active# X,
                   active# s X -> active# X,
           active# leq(X1, X2) -> active# X1,
           active# leq(X1, X2) -> active# X2,
        active# if(X1, X2, X3) -> active# X1,
          active# diff(X1, X2) -> active# X1,
          active# diff(X1, X2) -> active# X2}
      Weak:
      {              active p X -> p active X,
                   active p 0() -> mark 0(),
                   active p s X -> mark X,
                     active s X -> s active X,
             active leq(X1, X2) -> leq(X1, active X2),
             active leq(X1, X2) -> leq(active X1, X2),
             active leq(0(), Y) -> mark true(),
           active leq(s X, 0()) -> mark false(),
           active leq(s X, s Y) -> mark leq(X, Y),
          active if(X1, X2, X3) -> if(active X1, X2, X3),
        active if(true(), X, Y) -> mark X,
       active if(false(), X, Y) -> mark Y,
              active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)),
            active diff(X1, X2) -> diff(X1, active X2),
            active diff(X1, X2) -> diff(active X1, X2),
                       p mark X -> mark p X,
                         p ok X -> ok p X,
                       s mark X -> mark s X,
                         s ok X -> ok s X,
               leq(X1, mark X2) -> mark leq(X1, X2),
               leq(mark X1, X2) -> mark leq(X1, X2),
              leq(ok X1, ok X2) -> ok leq(X1, X2),
            if(mark X1, X2, X3) -> mark if(X1, X2, X3),
        if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
              diff(X1, mark X2) -> mark diff(X1, X2),
              diff(mark X1, X2) -> mark diff(X1, X2),
             diff(ok X1, ok X2) -> ok diff(X1, X2),
                     proper 0() -> ok 0(),
                     proper p X -> p proper X,
                     proper s X -> s proper X,
                  proper true() -> ok true(),
             proper leq(X1, X2) -> leq(proper X1, proper X2),
                 proper false() -> ok false(),
          proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
            proper diff(X1, X2) -> diff(proper X1, proper X2),
                     top mark X -> top proper X,
                       top ok X -> top active X}
      Open
     
     
     
     
     
     
     
     
     
     
     
     
     
     SCC (9):
      Strict:
       {           proper# p X -> proper# X,
                   proper# s X -> proper# X,
           proper# leq(X1, X2) -> proper# X1,
           proper# leq(X1, X2) -> proper# X2,
        proper# if(X1, X2, X3) -> proper# X1,
        proper# if(X1, X2, X3) -> proper# X2,
        proper# if(X1, X2, X3) -> proper# X3,
          proper# diff(X1, X2) -> proper# X1,
          proper# diff(X1, X2) -> proper# X2}
      Weak:
      {              active p X -> p active X,
                   active p 0() -> mark 0(),
                   active p s X -> mark X,
                     active s X -> s active X,
             active leq(X1, X2) -> leq(X1, active X2),
             active leq(X1, X2) -> leq(active X1, X2),
             active leq(0(), Y) -> mark true(),
           active leq(s X, 0()) -> mark false(),
           active leq(s X, s Y) -> mark leq(X, Y),
          active if(X1, X2, X3) -> if(active X1, X2, X3),
        active if(true(), X, Y) -> mark X,
       active if(false(), X, Y) -> mark Y,
              active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)),
            active diff(X1, X2) -> diff(X1, active X2),
            active diff(X1, X2) -> diff(active X1, X2),
                       p mark X -> mark p X,
                         p ok X -> ok p X,
                       s mark X -> mark s X,
                         s ok X -> ok s X,
               leq(X1, mark X2) -> mark leq(X1, X2),
               leq(mark X1, X2) -> mark leq(X1, X2),
              leq(ok X1, ok X2) -> ok leq(X1, X2),
            if(mark X1, X2, X3) -> mark if(X1, X2, X3),
        if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
              diff(X1, mark X2) -> mark diff(X1, X2),
              diff(mark X1, X2) -> mark diff(X1, X2),
             diff(ok X1, ok X2) -> ok diff(X1, X2),
                     proper 0() -> ok 0(),
                     proper p X -> p proper X,
                     proper s X -> s proper X,
                  proper true() -> ok true(),
             proper leq(X1, X2) -> leq(proper X1, proper X2),
                 proper false() -> ok false(),
          proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
            proper diff(X1, X2) -> diff(proper X1, proper X2),
                     top mark X -> top proper X,
                       top ok X -> top active X}
      Open
     
     SCC (3):
      Strict:
       { diff#(X1, mark X2) -> diff#(X1, X2),
         diff#(mark X1, X2) -> diff#(X1, X2),
        diff#(ok X1, ok X2) -> diff#(X1, X2)}
      Weak:
      {              active p X -> p active X,
                   active p 0() -> mark 0(),
                   active p s X -> mark X,
                     active s X -> s active X,
             active leq(X1, X2) -> leq(X1, active X2),
             active leq(X1, X2) -> leq(active X1, X2),
             active leq(0(), Y) -> mark true(),
           active leq(s X, 0()) -> mark false(),
           active leq(s X, s Y) -> mark leq(X, Y),
          active if(X1, X2, X3) -> if(active X1, X2, X3),
        active if(true(), X, Y) -> mark X,
       active if(false(), X, Y) -> mark Y,
              active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)),
            active diff(X1, X2) -> diff(X1, active X2),
            active diff(X1, X2) -> diff(active X1, X2),
                       p mark X -> mark p X,
                         p ok X -> ok p X,
                       s mark X -> mark s X,
                         s ok X -> ok s X,
               leq(X1, mark X2) -> mark leq(X1, X2),
               leq(mark X1, X2) -> mark leq(X1, X2),
              leq(ok X1, ok X2) -> ok leq(X1, X2),
            if(mark X1, X2, X3) -> mark if(X1, X2, X3),
        if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
              diff(X1, mark X2) -> mark diff(X1, X2),
              diff(mark X1, X2) -> mark diff(X1, X2),
             diff(ok X1, ok X2) -> ok diff(X1, X2),
                     proper 0() -> ok 0(),
                     proper p X -> p proper X,
                     proper s X -> s proper X,
                  proper true() -> ok true(),
             proper leq(X1, X2) -> leq(proper X1, proper X2),
                 proper false() -> ok false(),
          proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
            proper diff(X1, X2) -> diff(proper X1, proper X2),
                     top mark X -> top proper X,
                       top ok X -> top active X}
      Open
     
     SCC (2):
      Strict:
       {    if#(mark X1, X2, X3) -> if#(X1, X2, X3),
        if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3)}
      Weak:
      {              active p X -> p active X,
                   active p 0() -> mark 0(),
                   active p s X -> mark X,
                     active s X -> s active X,
             active leq(X1, X2) -> leq(X1, active X2),
             active leq(X1, X2) -> leq(active X1, X2),
             active leq(0(), Y) -> mark true(),
           active leq(s X, 0()) -> mark false(),
           active leq(s X, s Y) -> mark leq(X, Y),
          active if(X1, X2, X3) -> if(active X1, X2, X3),
        active if(true(), X, Y) -> mark X,
       active if(false(), X, Y) -> mark Y,
              active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)),
            active diff(X1, X2) -> diff(X1, active X2),
            active diff(X1, X2) -> diff(active X1, X2),
                       p mark X -> mark p X,
                         p ok X -> ok p X,
                       s mark X -> mark s X,
                         s ok X -> ok s X,
               leq(X1, mark X2) -> mark leq(X1, X2),
               leq(mark X1, X2) -> mark leq(X1, X2),
              leq(ok X1, ok X2) -> ok leq(X1, X2),
            if(mark X1, X2, X3) -> mark if(X1, X2, X3),
        if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
              diff(X1, mark X2) -> mark diff(X1, X2),
              diff(mark X1, X2) -> mark diff(X1, X2),
             diff(ok X1, ok X2) -> ok diff(X1, X2),
                     proper 0() -> ok 0(),
                     proper p X -> p proper X,
                     proper s X -> s proper X,
                  proper true() -> ok true(),
             proper leq(X1, X2) -> leq(proper X1, proper X2),
                 proper false() -> ok false(),
          proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
            proper diff(X1, X2) -> diff(proper X1, proper X2),
                     top mark X -> top proper X,
                       top ok X -> top active X}
      Open
     
     SCC (3):
      Strict:
       { leq#(X1, mark X2) -> leq#(X1, X2),
         leq#(mark X1, X2) -> leq#(X1, X2),
        leq#(ok X1, ok X2) -> leq#(X1, X2)}
      Weak:
      {              active p X -> p active X,
                   active p 0() -> mark 0(),
                   active p s X -> mark X,
                     active s X -> s active X,
             active leq(X1, X2) -> leq(X1, active X2),
             active leq(X1, X2) -> leq(active X1, X2),
             active leq(0(), Y) -> mark true(),
           active leq(s X, 0()) -> mark false(),
           active leq(s X, s Y) -> mark leq(X, Y),
          active if(X1, X2, X3) -> if(active X1, X2, X3),
        active if(true(), X, Y) -> mark X,
       active if(false(), X, Y) -> mark Y,
              active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)),
            active diff(X1, X2) -> diff(X1, active X2),
            active diff(X1, X2) -> diff(active X1, X2),
                       p mark X -> mark p X,
                         p ok X -> ok p X,
                       s mark X -> mark s X,
                         s ok X -> ok s X,
               leq(X1, mark X2) -> mark leq(X1, X2),
               leq(mark X1, X2) -> mark leq(X1, X2),
              leq(ok X1, ok X2) -> ok leq(X1, X2),
            if(mark X1, X2, X3) -> mark if(X1, X2, X3),
        if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
              diff(X1, mark X2) -> mark diff(X1, X2),
              diff(mark X1, X2) -> mark diff(X1, X2),
             diff(ok X1, ok X2) -> ok diff(X1, X2),
                     proper 0() -> ok 0(),
                     proper p X -> p proper X,
                     proper s X -> s proper X,
                  proper true() -> ok true(),
             proper leq(X1, X2) -> leq(proper X1, proper X2),
                 proper false() -> ok false(),
          proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
            proper diff(X1, X2) -> diff(proper X1, proper X2),
                     top mark X -> top proper X,
                       top ok X -> top active X}
      Open
     
     SCC (2):
      Strict:
       {s# mark X -> s# X,
          s# ok X -> s# X}
      Weak:
      {              active p X -> p active X,
                   active p 0() -> mark 0(),
                   active p s X -> mark X,
                     active s X -> s active X,
             active leq(X1, X2) -> leq(X1, active X2),
             active leq(X1, X2) -> leq(active X1, X2),
             active leq(0(), Y) -> mark true(),
           active leq(s X, 0()) -> mark false(),
           active leq(s X, s Y) -> mark leq(X, Y),
          active if(X1, X2, X3) -> if(active X1, X2, X3),
        active if(true(), X, Y) -> mark X,
       active if(false(), X, Y) -> mark Y,
              active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)),
            active diff(X1, X2) -> diff(X1, active X2),
            active diff(X1, X2) -> diff(active X1, X2),
                       p mark X -> mark p X,
                         p ok X -> ok p X,
                       s mark X -> mark s X,
                         s ok X -> ok s X,
               leq(X1, mark X2) -> mark leq(X1, X2),
               leq(mark X1, X2) -> mark leq(X1, X2),
              leq(ok X1, ok X2) -> ok leq(X1, X2),
            if(mark X1, X2, X3) -> mark if(X1, X2, X3),
        if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
              diff(X1, mark X2) -> mark diff(X1, X2),
              diff(mark X1, X2) -> mark diff(X1, X2),
             diff(ok X1, ok X2) -> ok diff(X1, X2),
                     proper 0() -> ok 0(),
                     proper p X -> p proper X,
                     proper s X -> s proper X,
                  proper true() -> ok true(),
             proper leq(X1, X2) -> leq(proper X1, proper X2),
                 proper false() -> ok false(),
          proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
            proper diff(X1, X2) -> diff(proper X1, proper X2),
                     top mark X -> top proper X,
                       top ok X -> top active X}
      Open
     
     SCC (2):
      Strict:
       {p# mark X -> p# X,
          p# ok X -> p# X}
      Weak:
      {              active p X -> p active X,
                   active p 0() -> mark 0(),
                   active p s X -> mark X,
                     active s X -> s active X,
             active leq(X1, X2) -> leq(X1, active X2),
             active leq(X1, X2) -> leq(active X1, X2),
             active leq(0(), Y) -> mark true(),
           active leq(s X, 0()) -> mark false(),
           active leq(s X, s Y) -> mark leq(X, Y),
          active if(X1, X2, X3) -> if(active X1, X2, X3),
        active if(true(), X, Y) -> mark X,
       active if(false(), X, Y) -> mark Y,
              active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)),
            active diff(X1, X2) -> diff(X1, active X2),
            active diff(X1, X2) -> diff(active X1, X2),
                       p mark X -> mark p X,
                         p ok X -> ok p X,
                       s mark X -> mark s X,
                         s ok X -> ok s X,
               leq(X1, mark X2) -> mark leq(X1, X2),
               leq(mark X1, X2) -> mark leq(X1, X2),
              leq(ok X1, ok X2) -> ok leq(X1, X2),
            if(mark X1, X2, X3) -> mark if(X1, X2, X3),
        if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
              diff(X1, mark X2) -> mark diff(X1, X2),
              diff(mark X1, X2) -> mark diff(X1, X2),
             diff(ok X1, ok X2) -> ok diff(X1, X2),
                     proper 0() -> ok 0(),
                     proper p X -> p proper X,
                     proper s X -> s proper X,
                  proper true() -> ok true(),
             proper leq(X1, X2) -> leq(proper X1, proper X2),
                 proper false() -> ok false(),
          proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
            proper diff(X1, X2) -> diff(proper X1, proper X2),
                     top mark X -> top proper X,
                       top ok X -> top active X}
      Open