MAYBE
Time: 1.461450
TRS:
 {    U12(mark X1, X2, X3) -> mark U12(X1, X2, X3),
  U12(ok X1, ok X2, ok X3) -> ok U12(X1, X2, X3),
    active U12(X1, X2, X3) -> U12(active X1, X2, X3),
    active U12(tt(), M, N) -> mark s plus(N, M),
    active U11(X1, X2, X3) -> U11(active X1, X2, X3),
    active U11(tt(), M, N) -> mark U12(tt(), M, N),
                active s X -> s active X,
       active plus(N, s M) -> mark U11(tt(), M, N),
       active plus(N, 0()) -> mark N,
       active plus(X1, X2) -> plus(X1, active X2),
       active plus(X1, X2) -> plus(active X1, X2),
    active U22(X1, X2, X3) -> U22(active X1, X2, X3),
    active U22(tt(), M, N) -> mark plus(x(N, M), N),
    active U21(X1, X2, X3) -> U21(active X1, X2, X3),
    active U21(tt(), M, N) -> mark U22(tt(), M, N),
          active x(N, s M) -> mark U21(tt(), M, N),
          active x(N, 0()) -> mark 0(),
          active x(X1, X2) -> x(X1, active X2),
          active x(X1, X2) -> x(active X1, X2),
      U11(mark X1, X2, X3) -> mark U11(X1, X2, X3),
  U11(ok X1, ok X2, ok X3) -> ok U11(X1, X2, X3),
                  s mark X -> mark s X,
                    s ok X -> ok s X,
         plus(X1, mark X2) -> mark plus(X1, X2),
         plus(mark X1, X2) -> mark plus(X1, X2),
        plus(ok X1, ok X2) -> ok plus(X1, X2),
      U22(mark X1, X2, X3) -> mark U22(X1, X2, X3),
  U22(ok X1, ok X2, ok X3) -> ok U22(X1, X2, X3),
      U21(mark X1, X2, X3) -> mark U21(X1, X2, X3),
  U21(ok X1, ok X2, ok X3) -> ok U21(X1, X2, X3),
            x(X1, mark X2) -> mark x(X1, X2),
            x(mark X1, X2) -> mark x(X1, X2),
           x(ok X1, ok X2) -> ok x(X1, X2),
    proper U12(X1, X2, X3) -> U12(proper X1, proper X2, proper X3),
               proper tt() -> ok tt(),
    proper U11(X1, X2, X3) -> U11(proper X1, proper X2, proper X3),
                proper s X -> s proper X,
       proper plus(X1, X2) -> plus(proper X1, proper X2),
    proper U22(X1, X2, X3) -> U22(proper X1, proper X2, proper X3),
    proper U21(X1, X2, X3) -> U21(proper X1, proper X2, proper X3),
          proper x(X1, X2) -> x(proper X1, proper X2),
                proper 0() -> ok 0(),
                top mark X -> top proper X,
                  top ok X -> top active X}
 DP:
  DP:
   {    U12#(mark X1, X2, X3) -> U12#(X1, X2, X3),
    U12#(ok X1, ok X2, ok X3) -> U12#(X1, X2, X3),
      active# U12(X1, X2, X3) -> U12#(active X1, X2, X3),
      active# U12(X1, X2, X3) -> active# X1,
      active# U12(tt(), M, N) -> s# plus(N, M),
      active# U12(tt(), M, N) -> plus#(N, M),
      active# U11(X1, X2, X3) -> active# X1,
      active# U11(X1, X2, X3) -> U11#(active X1, X2, X3),
      active# U11(tt(), M, N) -> U12#(tt(), M, N),
                  active# s X -> active# X,
                  active# s X -> s# active X,
         active# plus(N, s M) -> U11#(tt(), M, N),
         active# plus(X1, X2) -> active# X1,
         active# plus(X1, X2) -> active# X2,
         active# plus(X1, X2) -> plus#(X1, active X2),
         active# plus(X1, X2) -> plus#(active X1, X2),
      active# U22(X1, X2, X3) -> active# X1,
      active# U22(X1, X2, X3) -> U22#(active X1, X2, X3),
      active# U22(tt(), M, N) -> plus#(x(N, M), N),
      active# U22(tt(), M, N) -> x#(N, M),
      active# U21(X1, X2, X3) -> active# X1,
      active# U21(X1, X2, X3) -> U21#(active X1, X2, X3),
      active# U21(tt(), M, N) -> U22#(tt(), M, N),
            active# x(N, s M) -> U21#(tt(), M, N),
            active# x(X1, X2) -> active# X1,
            active# x(X1, X2) -> active# X2,
            active# x(X1, X2) -> x#(X1, active X2),
            active# x(X1, X2) -> x#(active X1, X2),
        U11#(mark X1, X2, X3) -> U11#(X1, X2, X3),
    U11#(ok X1, ok X2, ok X3) -> U11#(X1, X2, X3),
                    s# mark X -> s# X,
                      s# ok X -> s# X,
           plus#(X1, mark X2) -> plus#(X1, X2),
           plus#(mark X1, X2) -> plus#(X1, X2),
          plus#(ok X1, ok X2) -> plus#(X1, X2),
        U22#(mark X1, X2, X3) -> U22#(X1, X2, X3),
    U22#(ok X1, ok X2, ok X3) -> U22#(X1, X2, X3),
        U21#(mark X1, X2, X3) -> U21#(X1, X2, X3),
    U21#(ok X1, ok X2, ok X3) -> U21#(X1, X2, X3),
              x#(X1, mark X2) -> x#(X1, X2),
              x#(mark X1, X2) -> x#(X1, X2),
             x#(ok X1, ok X2) -> x#(X1, X2),
      proper# U12(X1, X2, X3) -> U12#(proper X1, proper X2, proper X3),
      proper# U12(X1, X2, X3) -> proper# X1,
      proper# U12(X1, X2, X3) -> proper# X2,
      proper# U12(X1, X2, X3) -> proper# X3,
      proper# U11(X1, X2, X3) -> U11#(proper X1, proper X2, proper X3),
      proper# U11(X1, X2, X3) -> proper# X1,
      proper# U11(X1, X2, X3) -> proper# X2,
      proper# U11(X1, X2, X3) -> proper# X3,
                  proper# s X -> s# proper X,
                  proper# s X -> proper# X,
         proper# plus(X1, X2) -> plus#(proper X1, proper X2),
         proper# plus(X1, X2) -> proper# X1,
         proper# plus(X1, X2) -> proper# X2,
      proper# U22(X1, X2, X3) -> U22#(proper X1, proper X2, proper X3),
      proper# U22(X1, X2, X3) -> proper# X1,
      proper# U22(X1, X2, X3) -> proper# X2,
      proper# U22(X1, X2, X3) -> proper# X3,
      proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3),
      proper# U21(X1, X2, X3) -> proper# X1,
      proper# U21(X1, X2, X3) -> proper# X2,
      proper# U21(X1, X2, X3) -> proper# X3,
            proper# x(X1, X2) -> x#(proper X1, proper X2),
            proper# x(X1, X2) -> proper# X1,
            proper# x(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:
  {    U12(mark X1, X2, X3) -> mark U12(X1, X2, X3),
   U12(ok X1, ok X2, ok X3) -> ok U12(X1, X2, X3),
     active U12(X1, X2, X3) -> U12(active X1, X2, X3),
     active U12(tt(), M, N) -> mark s plus(N, M),
     active U11(X1, X2, X3) -> U11(active X1, X2, X3),
     active U11(tt(), M, N) -> mark U12(tt(), M, N),
                 active s X -> s active X,
        active plus(N, s M) -> mark U11(tt(), M, N),
        active plus(N, 0()) -> mark N,
        active plus(X1, X2) -> plus(X1, active X2),
        active plus(X1, X2) -> plus(active X1, X2),
     active U22(X1, X2, X3) -> U22(active X1, X2, X3),
     active U22(tt(), M, N) -> mark plus(x(N, M), N),
     active U21(X1, X2, X3) -> U21(active X1, X2, X3),
     active U21(tt(), M, N) -> mark U22(tt(), M, N),
           active x(N, s M) -> mark U21(tt(), M, N),
           active x(N, 0()) -> mark 0(),
           active x(X1, X2) -> x(X1, active X2),
           active x(X1, X2) -> x(active X1, X2),
       U11(mark X1, X2, X3) -> mark U11(X1, X2, X3),
   U11(ok X1, ok X2, ok X3) -> ok U11(X1, X2, X3),
                   s mark X -> mark s X,
                     s ok X -> ok s X,
          plus(X1, mark X2) -> mark plus(X1, X2),
          plus(mark X1, X2) -> mark plus(X1, X2),
         plus(ok X1, ok X2) -> ok plus(X1, X2),
       U22(mark X1, X2, X3) -> mark U22(X1, X2, X3),
   U22(ok X1, ok X2, ok X3) -> ok U22(X1, X2, X3),
       U21(mark X1, X2, X3) -> mark U21(X1, X2, X3),
   U21(ok X1, ok X2, ok X3) -> ok U21(X1, X2, X3),
             x(X1, mark X2) -> mark x(X1, X2),
             x(mark X1, X2) -> mark x(X1, X2),
            x(ok X1, ok X2) -> ok x(X1, X2),
     proper U12(X1, X2, X3) -> U12(proper X1, proper X2, proper X3),
                proper tt() -> ok tt(),
     proper U11(X1, X2, X3) -> U11(proper X1, proper X2, proper X3),
                 proper s X -> s proper X,
        proper plus(X1, X2) -> plus(proper X1, proper X2),
     proper U22(X1, X2, X3) -> U22(proper X1, proper X2, proper X3),
     proper U21(X1, X2, X3) -> U21(proper X1, proper X2, proper X3),
           proper x(X1, X2) -> x(proper X1, proper X2),
                 proper 0() -> ok 0(),
                 top mark X -> top proper X,
                   top ok X -> top active X}
  EDG:
   {
    (active# x(X1, X2) -> active# X2, active# x(X1, X2) -> x#(active X1, X2))
    (active# x(X1, X2) -> active# X2, active# x(X1, X2) -> x#(X1, active X2))
    (active# x(X1, X2) -> active# X2, active# x(X1, X2) -> active# X2)
    (active# x(X1, X2) -> active# X2, active# x(X1, X2) -> active# X1)
    (active# x(X1, X2) -> active# X2, active# x(N, s M) -> U21#(tt(), M, N))
    (active# x(X1, X2) -> active# X2, active# U21(tt(), M, N) -> U22#(tt(), M, N))
    (active# x(X1, X2) -> active# X2, active# U21(X1, X2, X3) -> U21#(active X1, X2, X3))
    (active# x(X1, X2) -> active# X2, active# U21(X1, X2, X3) -> active# X1)
    (active# x(X1, X2) -> active# X2, active# U22(tt(), M, N) -> x#(N, M))
    (active# x(X1, X2) -> active# X2, active# U22(tt(), M, N) -> plus#(x(N, M), N))
    (active# x(X1, X2) -> active# X2, active# U22(X1, X2, X3) -> U22#(active X1, X2, X3))
    (active# x(X1, X2) -> active# X2, active# U22(X1, X2, X3) -> active# X1)
    (active# x(X1, X2) -> active# X2, active# plus(X1, X2) -> plus#(active X1, X2))
    (active# x(X1, X2) -> active# X2, active# plus(X1, X2) -> plus#(X1, active X2))
    (active# x(X1, X2) -> active# X2, active# plus(X1, X2) -> active# X2)
    (active# x(X1, X2) -> active# X2, active# plus(X1, X2) -> active# X1)
    (active# x(X1, X2) -> active# X2, active# plus(N, s M) -> U11#(tt(), M, N))
    (active# x(X1, X2) -> active# X2, active# s X -> s# active X)
    (active# x(X1, X2) -> active# X2, active# s X -> active# X)
    (active# x(X1, X2) -> active# X2, active# U11(tt(), M, N) -> U12#(tt(), M, N))
    (active# x(X1, X2) -> active# X2, active# U11(X1, X2, X3) -> U11#(active X1, X2, X3))
    (active# x(X1, X2) -> active# X2, active# U11(X1, X2, X3) -> active# X1)
    (active# x(X1, X2) -> active# X2, active# U12(tt(), M, N) -> plus#(N, M))
    (active# x(X1, X2) -> active# X2, active# U12(tt(), M, N) -> s# plus(N, M))
    (active# x(X1, X2) -> active# X2, active# U12(X1, X2, X3) -> active# X1)
    (active# x(X1, X2) -> active# X2, active# U12(X1, X2, X3) -> U12#(active X1, X2, X3))
    (proper# U11(X1, X2, X3) -> proper# X2, proper# x(X1, X2) -> proper# X2)
    (proper# U11(X1, X2, X3) -> proper# X2, proper# x(X1, X2) -> proper# X1)
    (proper# U11(X1, X2, X3) -> proper# X2, proper# x(X1, X2) -> x#(proper X1, proper X2))
    (proper# U11(X1, X2, X3) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X3)
    (proper# U11(X1, X2, X3) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X2)
    (proper# U11(X1, X2, X3) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X1)
    (proper# U11(X1, X2, X3) -> proper# X2, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
    (proper# U11(X1, X2, X3) -> proper# X2, proper# U22(X1, X2, X3) -> proper# X3)
    (proper# U11(X1, X2, X3) -> proper# X2, proper# U22(X1, X2, X3) -> proper# X2)
    (proper# U11(X1, X2, X3) -> proper# X2, proper# U22(X1, X2, X3) -> proper# X1)
    (proper# U11(X1, X2, X3) -> proper# X2, proper# U22(X1, X2, X3) -> U22#(proper X1, proper X2, proper X3))
    (proper# U11(X1, X2, X3) -> proper# X2, proper# plus(X1, X2) -> proper# X2)
    (proper# U11(X1, X2, X3) -> proper# X2, proper# plus(X1, X2) -> proper# X1)
    (proper# U11(X1, X2, X3) -> proper# X2, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
    (proper# U11(X1, X2, X3) -> proper# X2, proper# s X -> proper# X)
    (proper# U11(X1, X2, X3) -> proper# X2, proper# s X -> s# proper X)
    (proper# U11(X1, X2, X3) -> proper# X2, proper# U11(X1, X2, X3) -> proper# X3)
    (proper# U11(X1, X2, X3) -> proper# X2, proper# U11(X1, X2, X3) -> proper# X2)
    (proper# U11(X1, X2, X3) -> proper# X2, proper# U11(X1, X2, X3) -> proper# X1)
    (proper# U11(X1, X2, X3) -> proper# X2, proper# U11(X1, X2, X3) -> U11#(proper X1, proper X2, proper X3))
    (proper# U11(X1, X2, X3) -> proper# X2, proper# U12(X1, X2, X3) -> proper# X3)
    (proper# U11(X1, X2, X3) -> proper# X2, proper# U12(X1, X2, X3) -> proper# X2)
    (proper# U11(X1, X2, X3) -> proper# X2, proper# U12(X1, X2, X3) -> proper# X1)
    (proper# U11(X1, X2, X3) -> proper# X2, proper# U12(X1, X2, X3) -> U12#(proper X1, proper X2, proper X3))
    (proper# U22(X1, X2, X3) -> proper# X2, proper# x(X1, X2) -> proper# X2)
    (proper# U22(X1, X2, X3) -> proper# X2, proper# x(X1, X2) -> proper# X1)
    (proper# U22(X1, X2, X3) -> proper# X2, proper# x(X1, X2) -> x#(proper X1, proper X2))
    (proper# U22(X1, X2, X3) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X3)
    (proper# U22(X1, X2, X3) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X2)
    (proper# U22(X1, X2, X3) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X1)
    (proper# U22(X1, X2, X3) -> proper# X2, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
    (proper# U22(X1, X2, X3) -> proper# X2, proper# U22(X1, X2, X3) -> proper# X3)
    (proper# U22(X1, X2, X3) -> proper# X2, proper# U22(X1, X2, X3) -> proper# X2)
    (proper# U22(X1, X2, X3) -> proper# X2, proper# U22(X1, X2, X3) -> proper# X1)
    (proper# U22(X1, X2, X3) -> proper# X2, proper# U22(X1, X2, X3) -> U22#(proper X1, proper X2, proper X3))
    (proper# U22(X1, X2, X3) -> proper# X2, proper# plus(X1, X2) -> proper# X2)
    (proper# U22(X1, X2, X3) -> proper# X2, proper# plus(X1, X2) -> proper# X1)
    (proper# U22(X1, X2, X3) -> proper# X2, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
    (proper# U22(X1, X2, X3) -> proper# X2, proper# s X -> proper# X)
    (proper# U22(X1, X2, X3) -> proper# X2, proper# s X -> s# proper X)
    (proper# U22(X1, X2, X3) -> proper# X2, proper# U11(X1, X2, X3) -> proper# X3)
    (proper# U22(X1, X2, X3) -> proper# X2, proper# U11(X1, X2, X3) -> proper# X2)
    (proper# U22(X1, X2, X3) -> proper# X2, proper# U11(X1, X2, X3) -> proper# X1)
    (proper# U22(X1, X2, X3) -> proper# X2, proper# U11(X1, X2, X3) -> U11#(proper X1, proper X2, proper X3))
    (proper# U22(X1, X2, X3) -> proper# X2, proper# U12(X1, X2, X3) -> proper# X3)
    (proper# U22(X1, X2, X3) -> proper# X2, proper# U12(X1, X2, X3) -> proper# X2)
    (proper# U22(X1, X2, X3) -> proper# X2, proper# U12(X1, X2, X3) -> proper# X1)
    (proper# U22(X1, X2, X3) -> proper# X2, proper# U12(X1, X2, X3) -> U12#(proper X1, proper X2, proper X3))
    (proper# x(X1, X2) -> proper# X2, proper# x(X1, X2) -> proper# X2)
    (proper# x(X1, X2) -> proper# X2, proper# x(X1, X2) -> proper# X1)
    (proper# x(X1, X2) -> proper# X2, proper# x(X1, X2) -> x#(proper X1, proper X2))
    (proper# x(X1, X2) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X3)
    (proper# x(X1, X2) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X2)
    (proper# x(X1, X2) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X1)
    (proper# x(X1, X2) -> proper# X2, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
    (proper# x(X1, X2) -> proper# X2, proper# U22(X1, X2, X3) -> proper# X3)
    (proper# x(X1, X2) -> proper# X2, proper# U22(X1, X2, X3) -> proper# X2)
    (proper# x(X1, X2) -> proper# X2, proper# U22(X1, X2, X3) -> proper# X1)
    (proper# x(X1, X2) -> proper# X2, proper# U22(X1, X2, X3) -> U22#(proper X1, proper X2, proper X3))
    (proper# x(X1, X2) -> proper# X2, proper# plus(X1, X2) -> proper# X2)
    (proper# x(X1, X2) -> proper# X2, proper# plus(X1, X2) -> proper# X1)
    (proper# x(X1, X2) -> proper# X2, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
    (proper# x(X1, X2) -> proper# X2, proper# s X -> proper# X)
    (proper# x(X1, X2) -> proper# X2, proper# s X -> s# proper X)
    (proper# x(X1, X2) -> proper# X2, proper# U11(X1, X2, X3) -> proper# X3)
    (proper# x(X1, X2) -> proper# X2, proper# U11(X1, X2, X3) -> proper# X2)
    (proper# x(X1, X2) -> proper# X2, proper# U11(X1, X2, X3) -> proper# X1)
    (proper# x(X1, X2) -> proper# X2, proper# U11(X1, X2, X3) -> U11#(proper X1, proper X2, proper X3))
    (proper# x(X1, X2) -> proper# X2, proper# U12(X1, X2, X3) -> proper# X3)
    (proper# x(X1, X2) -> proper# X2, proper# U12(X1, X2, X3) -> proper# X2)
    (proper# x(X1, X2) -> proper# X2, proper# U12(X1, X2, X3) -> proper# X1)
    (proper# x(X1, X2) -> proper# X2, proper# U12(X1, X2, X3) -> U12#(proper X1, proper X2, proper X3))
    (U12#(mark X1, X2, X3) -> U12#(X1, X2, X3), U12#(ok X1, ok X2, ok X3) -> U12#(X1, X2, X3))
    (U12#(mark X1, X2, X3) -> U12#(X1, X2, X3), U12#(mark X1, X2, X3) -> U12#(X1, X2, X3))
    (active# U12(X1, X2, X3) -> U12#(active X1, X2, X3), U12#(ok X1, ok X2, ok X3) -> U12#(X1, X2, X3))
    (active# U12(X1, X2, X3) -> U12#(active X1, X2, X3), U12#(mark X1, X2, X3) -> U12#(X1, X2, X3))
    (active# U22(X1, X2, X3) -> U22#(active X1, X2, X3), U22#(ok X1, ok X2, ok X3) -> U22#(X1, X2, X3))
    (active# U22(X1, X2, X3) -> U22#(active X1, X2, X3), U22#(mark X1, X2, X3) -> U22#(X1, X2, X3))
    (U11#(mark X1, X2, X3) -> U11#(X1, X2, X3), U11#(ok X1, ok X2, ok X3) -> U11#(X1, X2, X3))
    (U11#(mark X1, X2, X3) -> U11#(X1, X2, X3), U11#(mark X1, X2, X3) -> U11#(X1, X2, X3))
    (U22#(mark X1, X2, X3) -> U22#(X1, X2, X3), U22#(ok X1, ok X2, ok X3) -> U22#(X1, X2, X3))
    (U22#(mark X1, X2, X3) -> U22#(X1, X2, X3), U22#(mark X1, X2, X3) -> U22#(X1, X2, X3))
    (U21#(mark X1, X2, X3) -> U21#(X1, X2, X3), U21#(ok X1, ok X2, ok X3) -> U21#(X1, X2, X3))
    (U21#(mark X1, X2, X3) -> U21#(X1, X2, X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3))
    (active# U12(tt(), M, N) -> plus#(N, M), plus#(ok X1, ok X2) -> plus#(X1, X2))
    (active# U12(tt(), M, N) -> plus#(N, M), plus#(mark X1, X2) -> plus#(X1, X2))
    (active# U12(tt(), M, N) -> plus#(N, M), plus#(X1, mark X2) -> plus#(X1, X2))
    (proper# U12(X1, X2, X3) -> proper# X3, proper# x(X1, X2) -> proper# X2)
    (proper# U12(X1, X2, X3) -> proper# X3, proper# x(X1, X2) -> proper# X1)
    (proper# U12(X1, X2, X3) -> proper# X3, proper# x(X1, X2) -> x#(proper X1, proper X2))
    (proper# U12(X1, X2, X3) -> proper# X3, proper# U21(X1, X2, X3) -> proper# X3)
    (proper# U12(X1, X2, X3) -> proper# X3, proper# U21(X1, X2, X3) -> proper# X2)
    (proper# U12(X1, X2, X3) -> proper# X3, proper# U21(X1, X2, X3) -> proper# X1)
    (proper# U12(X1, X2, X3) -> proper# X3, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
    (proper# U12(X1, X2, X3) -> proper# X3, proper# U22(X1, X2, X3) -> proper# X3)
    (proper# U12(X1, X2, X3) -> proper# X3, proper# U22(X1, X2, X3) -> proper# X2)
    (proper# U12(X1, X2, X3) -> proper# X3, proper# U22(X1, X2, X3) -> proper# X1)
    (proper# U12(X1, X2, X3) -> proper# X3, proper# U22(X1, X2, X3) -> U22#(proper X1, proper X2, proper X3))
    (proper# U12(X1, X2, X3) -> proper# X3, proper# plus(X1, X2) -> proper# X2)
    (proper# U12(X1, X2, X3) -> proper# X3, proper# plus(X1, X2) -> proper# X1)
    (proper# U12(X1, X2, X3) -> proper# X3, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
    (proper# U12(X1, X2, X3) -> proper# X3, proper# s X -> proper# X)
    (proper# U12(X1, X2, X3) -> proper# X3, proper# s X -> s# proper X)
    (proper# U12(X1, X2, X3) -> proper# X3, proper# U11(X1, X2, X3) -> proper# X3)
    (proper# U12(X1, X2, X3) -> proper# X3, proper# U11(X1, X2, X3) -> proper# X2)
    (proper# U12(X1, X2, X3) -> proper# X3, proper# U11(X1, X2, X3) -> proper# X1)
    (proper# U12(X1, X2, X3) -> proper# X3, proper# U11(X1, X2, X3) -> U11#(proper X1, proper X2, proper X3))
    (proper# U12(X1, X2, X3) -> proper# X3, proper# U12(X1, X2, X3) -> proper# X3)
    (proper# U12(X1, X2, X3) -> proper# X3, proper# U12(X1, X2, X3) -> proper# X2)
    (proper# U12(X1, X2, X3) -> proper# X3, proper# U12(X1, X2, X3) -> proper# X1)
    (proper# U12(X1, X2, X3) -> proper# X3, proper# U12(X1, X2, X3) -> U12#(proper X1, proper X2, proper X3))
    (proper# U22(X1, X2, X3) -> proper# X3, proper# x(X1, X2) -> proper# X2)
    (proper# U22(X1, X2, X3) -> proper# X3, proper# x(X1, X2) -> proper# X1)
    (proper# U22(X1, X2, X3) -> proper# X3, proper# x(X1, X2) -> x#(proper X1, proper X2))
    (proper# U22(X1, X2, X3) -> proper# X3, proper# U21(X1, X2, X3) -> proper# X3)
    (proper# U22(X1, X2, X3) -> proper# X3, proper# U21(X1, X2, X3) -> proper# X2)
    (proper# U22(X1, X2, X3) -> proper# X3, proper# U21(X1, X2, X3) -> proper# X1)
    (proper# U22(X1, X2, X3) -> proper# X3, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
    (proper# U22(X1, X2, X3) -> proper# X3, proper# U22(X1, X2, X3) -> proper# X3)
    (proper# U22(X1, X2, X3) -> proper# X3, proper# U22(X1, X2, X3) -> proper# X2)
    (proper# U22(X1, X2, X3) -> proper# X3, proper# U22(X1, X2, X3) -> proper# X1)
    (proper# U22(X1, X2, X3) -> proper# X3, proper# U22(X1, X2, X3) -> U22#(proper X1, proper X2, proper X3))
    (proper# U22(X1, X2, X3) -> proper# X3, proper# plus(X1, X2) -> proper# X2)
    (proper# U22(X1, X2, X3) -> proper# X3, proper# plus(X1, X2) -> proper# X1)
    (proper# U22(X1, X2, X3) -> proper# X3, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
    (proper# U22(X1, X2, X3) -> proper# X3, proper# s X -> proper# X)
    (proper# U22(X1, X2, X3) -> proper# X3, proper# s X -> s# proper X)
    (proper# U22(X1, X2, X3) -> proper# X3, proper# U11(X1, X2, X3) -> proper# X3)
    (proper# U22(X1, X2, X3) -> proper# X3, proper# U11(X1, X2, X3) -> proper# X2)
    (proper# U22(X1, X2, X3) -> proper# X3, proper# U11(X1, X2, X3) -> proper# X1)
    (proper# U22(X1, X2, X3) -> proper# X3, proper# U11(X1, X2, X3) -> U11#(proper X1, proper X2, proper X3))
    (proper# U22(X1, X2, X3) -> proper# X3, proper# U12(X1, X2, X3) -> proper# X3)
    (proper# U22(X1, X2, X3) -> proper# X3, proper# U12(X1, X2, X3) -> proper# X2)
    (proper# U22(X1, X2, X3) -> proper# X3, proper# U12(X1, X2, X3) -> proper# X1)
    (proper# U22(X1, X2, X3) -> proper# X3, proper# U12(X1, X2, X3) -> U12#(proper X1, proper X2, proper X3))
    (active# plus(X1, X2) -> plus#(X1, active X2), plus#(ok X1, ok X2) -> plus#(X1, X2))
    (active# plus(X1, X2) -> plus#(X1, active X2), plus#(mark X1, X2) -> plus#(X1, X2))
    (active# plus(X1, X2) -> plus#(X1, active X2), plus#(X1, mark X2) -> plus#(X1, X2))
    (proper# plus(X1, X2) -> plus#(proper X1, proper X2), plus#(ok X1, ok X2) -> plus#(X1, X2))
    (proper# plus(X1, X2) -> plus#(proper X1, proper X2), plus#(mark X1, X2) -> plus#(X1, X2))
    (proper# plus(X1, X2) -> plus#(proper X1, proper X2), plus#(X1, mark X2) -> plus#(X1, X2))
    (active# plus(X1, X2) -> plus#(active X1, X2), plus#(ok X1, ok X2) -> plus#(X1, X2))
    (active# plus(X1, X2) -> plus#(active X1, X2), plus#(mark X1, X2) -> plus#(X1, X2))
    (active# plus(X1, X2) -> plus#(active X1, X2), plus#(X1, mark X2) -> plus#(X1, X2))
    (active# s X -> s# active X, s# ok X -> s# X)
    (active# s X -> s# active X, s# mark X -> s# X)
    (top# mark X -> top# proper X, top# ok X -> top# active X)
    (top# mark X -> top# proper X, top# ok X -> active# X)
    (top# mark X -> top# proper X, top# mark X -> top# proper X)
    (top# mark X -> top# proper X, top# mark X -> proper# X)
    (plus#(X1, mark X2) -> plus#(X1, X2), plus#(ok X1, ok X2) -> plus#(X1, X2))
    (plus#(X1, mark X2) -> plus#(X1, X2), plus#(mark X1, X2) -> plus#(X1, X2))
    (plus#(X1, mark X2) -> plus#(X1, X2), plus#(X1, mark X2) -> plus#(X1, X2))
    (plus#(ok X1, ok X2) -> plus#(X1, X2), plus#(ok X1, ok X2) -> plus#(X1, X2))
    (plus#(ok X1, ok X2) -> plus#(X1, X2), plus#(mark X1, X2) -> plus#(X1, X2))
    (plus#(ok X1, ok X2) -> plus#(X1, X2), plus#(X1, mark X2) -> plus#(X1, X2))
    (x#(mark X1, X2) -> x#(X1, X2), x#(ok X1, ok X2) -> x#(X1, X2))
    (x#(mark X1, X2) -> x#(X1, X2), x#(mark X1, X2) -> x#(X1, X2))
    (x#(mark X1, X2) -> x#(X1, X2), x#(X1, mark X2) -> x#(X1, X2))
    (active# U22(tt(), M, N) -> plus#(x(N, M), N), plus#(ok X1, ok X2) -> plus#(X1, X2))
    (active# U22(tt(), M, N) -> plus#(x(N, M), N), plus#(mark X1, X2) -> plus#(X1, X2))
    (active# U22(tt(), M, N) -> plus#(x(N, M), N), plus#(X1, mark X2) -> plus#(X1, X2))
    (active# plus(N, s M) -> U11#(tt(), M, N), U11#(ok X1, ok X2, ok X3) -> U11#(X1, X2, X3))
    (active# plus(N, s M) -> U11#(tt(), M, N), U11#(mark X1, X2, X3) -> U11#(X1, X2, X3))
    (active# x(N, s M) -> U21#(tt(), M, N), U21#(ok X1, ok X2, ok X3) -> U21#(X1, X2, X3))
    (active# x(N, s M) -> U21#(tt(), M, N), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3))
    (s# mark X -> s# X, s# ok X -> s# X)
    (s# mark X -> s# X, s# mark X -> s# X)
    (proper# s X -> proper# X, proper# x(X1, X2) -> proper# X2)
    (proper# s X -> proper# X, proper# x(X1, X2) -> proper# X1)
    (proper# s X -> proper# X, proper# x(X1, X2) -> x#(proper X1, proper X2))
    (proper# s X -> proper# X, proper# U21(X1, X2, X3) -> proper# X3)
    (proper# s X -> proper# X, proper# U21(X1, X2, X3) -> proper# X2)
    (proper# s X -> proper# X, proper# U21(X1, X2, X3) -> proper# X1)
    (proper# s X -> proper# X, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
    (proper# s X -> proper# X, proper# U22(X1, X2, X3) -> proper# X3)
    (proper# s X -> proper# X, proper# U22(X1, X2, X3) -> proper# X2)
    (proper# s X -> proper# X, proper# U22(X1, X2, X3) -> proper# X1)
    (proper# s X -> proper# X, proper# U22(X1, X2, X3) -> U22#(proper X1, proper X2, proper X3))
    (proper# s X -> proper# X, proper# plus(X1, X2) -> proper# X2)
    (proper# s X -> proper# X, proper# plus(X1, X2) -> proper# X1)
    (proper# s X -> proper# X, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
    (proper# s X -> proper# X, proper# s X -> proper# X)
    (proper# s X -> proper# X, proper# s X -> s# proper X)
    (proper# s X -> proper# X, proper# U11(X1, X2, X3) -> proper# X3)
    (proper# s X -> proper# X, proper# U11(X1, X2, X3) -> proper# X2)
    (proper# s X -> proper# X, proper# U11(X1, X2, X3) -> proper# X1)
    (proper# s X -> proper# X, proper# U11(X1, X2, X3) -> U11#(proper X1, proper X2, proper X3))
    (proper# s X -> proper# X, proper# U12(X1, X2, X3) -> proper# X3)
    (proper# s X -> proper# X, proper# U12(X1, X2, X3) -> proper# X2)
    (proper# s X -> proper# X, proper# U12(X1, X2, X3) -> proper# X1)
    (proper# s X -> proper# X, proper# U12(X1, X2, X3) -> U12#(proper X1, proper X2, proper X3))
    (top# ok X -> active# X, active# x(X1, X2) -> x#(active X1, X2))
    (top# ok X -> active# X, active# x(X1, X2) -> x#(X1, active X2))
    (top# ok X -> active# X, active# x(X1, X2) -> active# X2)
    (top# ok X -> active# X, active# x(X1, X2) -> active# X1)
    (top# ok X -> active# X, active# x(N, s M) -> U21#(tt(), M, N))
    (top# ok X -> active# X, active# U21(tt(), M, N) -> U22#(tt(), M, N))
    (top# ok X -> active# X, active# U21(X1, X2, X3) -> U21#(active X1, X2, X3))
    (top# ok X -> active# X, active# U21(X1, X2, X3) -> active# X1)
    (top# ok X -> active# X, active# U22(tt(), M, N) -> x#(N, M))
    (top# ok X -> active# X, active# U22(tt(), M, N) -> plus#(x(N, M), N))
    (top# ok X -> active# X, active# U22(X1, X2, X3) -> U22#(active X1, X2, X3))
    (top# ok X -> active# X, active# U22(X1, X2, X3) -> active# X1)
    (top# ok X -> active# X, active# plus(X1, X2) -> plus#(active X1, X2))
    (top# ok X -> active# X, active# plus(X1, X2) -> plus#(X1, active X2))
    (top# ok X -> active# X, active# plus(X1, X2) -> active# X2)
    (top# ok X -> active# X, active# plus(X1, X2) -> active# X1)
    (top# ok X -> active# X, active# plus(N, s M) -> U11#(tt(), M, N))
    (top# ok X -> active# X, active# s X -> s# active X)
    (top# ok X -> active# X, active# s X -> active# X)
    (top# ok X -> active# X, active# U11(tt(), M, N) -> U12#(tt(), M, N))
    (top# ok X -> active# X, active# U11(X1, X2, X3) -> U11#(active X1, X2, X3))
    (top# ok X -> active# X, active# U11(X1, X2, X3) -> active# X1)
    (top# ok X -> active# X, active# U12(tt(), M, N) -> plus#(N, M))
    (top# ok X -> active# X, active# U12(tt(), M, N) -> s# plus(N, M))
    (top# ok X -> active# X, active# U12(X1, X2, X3) -> active# X1)
    (top# ok X -> active# X, active# U12(X1, X2, X3) -> U12#(active X1, X2, X3))
    (proper# U11(X1, X2, X3) -> U11#(proper X1, proper X2, proper X3), U11#(ok X1, ok X2, ok X3) -> U11#(X1, X2, X3))
    (proper# U11(X1, X2, X3) -> U11#(proper X1, proper X2, proper X3), U11#(mark X1, X2, X3) -> U11#(X1, X2, X3))
    (proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3), U21#(ok X1, ok X2, ok X3) -> U21#(X1, X2, X3))
    (proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3))
    (active# U11(X1, X2, X3) -> active# X1, active# x(X1, X2) -> x#(active X1, X2))
    (active# U11(X1, X2, X3) -> active# X1, active# x(X1, X2) -> x#(X1, active X2))
    (active# U11(X1, X2, X3) -> active# X1, active# x(X1, X2) -> active# X2)
    (active# U11(X1, X2, X3) -> active# X1, active# x(X1, X2) -> active# X1)
    (active# U11(X1, X2, X3) -> active# X1, active# x(N, s M) -> U21#(tt(), M, N))
    (active# U11(X1, X2, X3) -> active# X1, active# U21(tt(), M, N) -> U22#(tt(), M, N))
    (active# U11(X1, X2, X3) -> active# X1, active# U21(X1, X2, X3) -> U21#(active X1, X2, X3))
    (active# U11(X1, X2, X3) -> active# X1, active# U21(X1, X2, X3) -> active# X1)
    (active# U11(X1, X2, X3) -> active# X1, active# U22(tt(), M, N) -> x#(N, M))
    (active# U11(X1, X2, X3) -> active# X1, active# U22(tt(), M, N) -> plus#(x(N, M), N))
    (active# U11(X1, X2, X3) -> active# X1, active# U22(X1, X2, X3) -> U22#(active X1, X2, X3))
    (active# U11(X1, X2, X3) -> active# X1, active# U22(X1, X2, X3) -> active# X1)
    (active# U11(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> plus#(active X1, X2))
    (active# U11(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> plus#(X1, active X2))
    (active# U11(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> active# X2)
    (active# U11(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> active# X1)
    (active# U11(X1, X2, X3) -> active# X1, active# plus(N, s M) -> U11#(tt(), M, N))
    (active# U11(X1, X2, X3) -> active# X1, active# s X -> s# active X)
    (active# U11(X1, X2, X3) -> active# X1, active# s X -> active# X)
    (active# U11(X1, X2, X3) -> active# X1, active# U11(tt(), M, N) -> U12#(tt(), M, N))
    (active# U11(X1, X2, X3) -> active# X1, active# U11(X1, X2, X3) -> U11#(active X1, X2, X3))
    (active# U11(X1, X2, X3) -> active# X1, active# U11(X1, X2, X3) -> active# X1)
    (active# U11(X1, X2, X3) -> active# X1, active# U12(tt(), M, N) -> plus#(N, M))
    (active# U11(X1, X2, X3) -> active# X1, active# U12(tt(), M, N) -> s# plus(N, M))
    (active# U11(X1, X2, X3) -> active# X1, active# U12(X1, X2, X3) -> active# X1)
    (active# U11(X1, X2, X3) -> active# X1, active# U12(X1, X2, X3) -> U12#(active X1, X2, X3))
    (active# U22(X1, X2, X3) -> active# X1, active# x(X1, X2) -> x#(active X1, X2))
    (active# U22(X1, X2, X3) -> active# X1, active# x(X1, X2) -> x#(X1, active X2))
    (active# U22(X1, X2, X3) -> active# X1, active# x(X1, X2) -> active# X2)
    (active# U22(X1, X2, X3) -> active# X1, active# x(X1, X2) -> active# X1)
    (active# U22(X1, X2, X3) -> active# X1, active# x(N, s M) -> U21#(tt(), M, N))
    (active# U22(X1, X2, X3) -> active# X1, active# U21(tt(), M, N) -> U22#(tt(), M, N))
    (active# U22(X1, X2, X3) -> active# X1, active# U21(X1, X2, X3) -> U21#(active X1, X2, X3))
    (active# U22(X1, X2, X3) -> active# X1, active# U21(X1, X2, X3) -> active# X1)
    (active# U22(X1, X2, X3) -> active# X1, active# U22(tt(), M, N) -> x#(N, M))
    (active# U22(X1, X2, X3) -> active# X1, active# U22(tt(), M, N) -> plus#(x(N, M), N))
    (active# U22(X1, X2, X3) -> active# X1, active# U22(X1, X2, X3) -> U22#(active X1, X2, X3))
    (active# U22(X1, X2, X3) -> active# X1, active# U22(X1, X2, X3) -> active# X1)
    (active# U22(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> plus#(active X1, X2))
    (active# U22(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> plus#(X1, active X2))
    (active# U22(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> active# X2)
    (active# U22(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> active# X1)
    (active# U22(X1, X2, X3) -> active# X1, active# plus(N, s M) -> U11#(tt(), M, N))
    (active# U22(X1, X2, X3) -> active# X1, active# s X -> s# active X)
    (active# U22(X1, X2, X3) -> active# X1, active# s X -> active# X)
    (active# U22(X1, X2, X3) -> active# X1, active# U11(tt(), M, N) -> U12#(tt(), M, N))
    (active# U22(X1, X2, X3) -> active# X1, active# U11(X1, X2, X3) -> U11#(active X1, X2, X3))
    (active# U22(X1, X2, X3) -> active# X1, active# U11(X1, X2, X3) -> active# X1)
    (active# U22(X1, X2, X3) -> active# X1, active# U12(tt(), M, N) -> plus#(N, M))
    (active# U22(X1, X2, X3) -> active# X1, active# U12(tt(), M, N) -> s# plus(N, M))
    (active# U22(X1, X2, X3) -> active# X1, active# U12(X1, X2, X3) -> active# X1)
    (active# U22(X1, X2, X3) -> active# X1, active# U12(X1, X2, X3) -> U12#(active X1, X2, X3))
    (active# x(X1, X2) -> active# X1, active# x(X1, X2) -> x#(active X1, X2))
    (active# x(X1, X2) -> active# X1, active# x(X1, X2) -> x#(X1, active X2))
    (active# x(X1, X2) -> active# X1, active# x(X1, X2) -> active# X2)
    (active# x(X1, X2) -> active# X1, active# x(X1, X2) -> active# X1)
    (active# x(X1, X2) -> active# X1, active# x(N, s M) -> U21#(tt(), M, N))
    (active# x(X1, X2) -> active# X1, active# U21(tt(), M, N) -> U22#(tt(), M, N))
    (active# x(X1, X2) -> active# X1, active# U21(X1, X2, X3) -> U21#(active X1, X2, X3))
    (active# x(X1, X2) -> active# X1, active# U21(X1, X2, X3) -> active# X1)
    (active# x(X1, X2) -> active# X1, active# U22(tt(), M, N) -> x#(N, M))
    (active# x(X1, X2) -> active# X1, active# U22(tt(), M, N) -> plus#(x(N, M), N))
    (active# x(X1, X2) -> active# X1, active# U22(X1, X2, X3) -> U22#(active X1, X2, X3))
    (active# x(X1, X2) -> active# X1, active# U22(X1, X2, X3) -> active# X1)
    (active# x(X1, X2) -> active# X1, active# plus(X1, X2) -> plus#(active X1, X2))
    (active# x(X1, X2) -> active# X1, active# plus(X1, X2) -> plus#(X1, active X2))
    (active# x(X1, X2) -> active# X1, active# plus(X1, X2) -> active# X2)
    (active# x(X1, X2) -> active# X1, active# plus(X1, X2) -> active# X1)
    (active# x(X1, X2) -> active# X1, active# plus(N, s M) -> U11#(tt(), M, N))
    (active# x(X1, X2) -> active# X1, active# s X -> s# active X)
    (active# x(X1, X2) -> active# X1, active# s X -> active# X)
    (active# x(X1, X2) -> active# X1, active# U11(tt(), M, N) -> U12#(tt(), M, N))
    (active# x(X1, X2) -> active# X1, active# U11(X1, X2, X3) -> U11#(active X1, X2, X3))
    (active# x(X1, X2) -> active# X1, active# U11(X1, X2, X3) -> active# X1)
    (active# x(X1, X2) -> active# X1, active# U12(tt(), M, N) -> plus#(N, M))
    (active# x(X1, X2) -> active# X1, active# U12(tt(), M, N) -> s# plus(N, M))
    (active# x(X1, X2) -> active# X1, active# U12(X1, X2, X3) -> active# X1)
    (active# x(X1, X2) -> active# X1, active# U12(X1, X2, X3) -> U12#(active X1, X2, X3))
    (proper# U11(X1, X2, X3) -> proper# X1, proper# x(X1, X2) -> proper# X2)
    (proper# U11(X1, X2, X3) -> proper# X1, proper# x(X1, X2) -> proper# X1)
    (proper# U11(X1, X2, X3) -> proper# X1, proper# x(X1, X2) -> x#(proper X1, proper X2))
    (proper# U11(X1, X2, X3) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X3)
    (proper# U11(X1, X2, X3) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X2)
    (proper# U11(X1, X2, X3) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X1)
    (proper# U11(X1, X2, X3) -> proper# X1, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
    (proper# U11(X1, X2, X3) -> proper# X1, proper# U22(X1, X2, X3) -> proper# X3)
    (proper# U11(X1, X2, X3) -> proper# X1, proper# U22(X1, X2, X3) -> proper# X2)
    (proper# U11(X1, X2, X3) -> proper# X1, proper# U22(X1, X2, X3) -> proper# X1)
    (proper# U11(X1, X2, X3) -> proper# X1, proper# U22(X1, X2, X3) -> U22#(proper X1, proper X2, proper X3))
    (proper# U11(X1, X2, X3) -> proper# X1, proper# plus(X1, X2) -> proper# X2)
    (proper# U11(X1, X2, X3) -> proper# X1, proper# plus(X1, X2) -> proper# X1)
    (proper# U11(X1, X2, X3) -> proper# X1, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
    (proper# U11(X1, X2, X3) -> proper# X1, proper# s X -> proper# X)
    (proper# U11(X1, X2, X3) -> proper# X1, proper# s X -> s# proper X)
    (proper# U11(X1, X2, X3) -> proper# X1, proper# U11(X1, X2, X3) -> proper# X3)
    (proper# U11(X1, X2, X3) -> proper# X1, proper# U11(X1, X2, X3) -> proper# X2)
    (proper# U11(X1, X2, X3) -> proper# X1, proper# U11(X1, X2, X3) -> proper# X1)
    (proper# U11(X1, X2, X3) -> proper# X1, proper# U11(X1, X2, X3) -> U11#(proper X1, proper X2, proper X3))
    (proper# U11(X1, X2, X3) -> proper# X1, proper# U12(X1, X2, X3) -> proper# X3)
    (proper# U11(X1, X2, X3) -> proper# X1, proper# U12(X1, X2, X3) -> proper# X2)
    (proper# U11(X1, X2, X3) -> proper# X1, proper# U12(X1, X2, X3) -> proper# X1)
    (proper# U11(X1, X2, X3) -> proper# X1, proper# U12(X1, X2, X3) -> U12#(proper X1, proper X2, proper X3))
    (proper# U22(X1, X2, X3) -> proper# X1, proper# x(X1, X2) -> proper# X2)
    (proper# U22(X1, X2, X3) -> proper# X1, proper# x(X1, X2) -> proper# X1)
    (proper# U22(X1, X2, X3) -> proper# X1, proper# x(X1, X2) -> x#(proper X1, proper X2))
    (proper# U22(X1, X2, X3) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X3)
    (proper# U22(X1, X2, X3) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X2)
    (proper# U22(X1, X2, X3) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X1)
    (proper# U22(X1, X2, X3) -> proper# X1, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
    (proper# U22(X1, X2, X3) -> proper# X1, proper# U22(X1, X2, X3) -> proper# X3)
    (proper# U22(X1, X2, X3) -> proper# X1, proper# U22(X1, X2, X3) -> proper# X2)
    (proper# U22(X1, X2, X3) -> proper# X1, proper# U22(X1, X2, X3) -> proper# X1)
    (proper# U22(X1, X2, X3) -> proper# X1, proper# U22(X1, X2, X3) -> U22#(proper X1, proper X2, proper X3))
    (proper# U22(X1, X2, X3) -> proper# X1, proper# plus(X1, X2) -> proper# X2)
    (proper# U22(X1, X2, X3) -> proper# X1, proper# plus(X1, X2) -> proper# X1)
    (proper# U22(X1, X2, X3) -> proper# X1, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
    (proper# U22(X1, X2, X3) -> proper# X1, proper# s X -> proper# X)
    (proper# U22(X1, X2, X3) -> proper# X1, proper# s X -> s# proper X)
    (proper# U22(X1, X2, X3) -> proper# X1, proper# U11(X1, X2, X3) -> proper# X3)
    (proper# U22(X1, X2, X3) -> proper# X1, proper# U11(X1, X2, X3) -> proper# X2)
    (proper# U22(X1, X2, X3) -> proper# X1, proper# U11(X1, X2, X3) -> proper# X1)
    (proper# U22(X1, X2, X3) -> proper# X1, proper# U11(X1, X2, X3) -> U11#(proper X1, proper X2, proper X3))
    (proper# U22(X1, X2, X3) -> proper# X1, proper# U12(X1, X2, X3) -> proper# X3)
    (proper# U22(X1, X2, X3) -> proper# X1, proper# U12(X1, X2, X3) -> proper# X2)
    (proper# U22(X1, X2, X3) -> proper# X1, proper# U12(X1, X2, X3) -> proper# X1)
    (proper# U22(X1, X2, X3) -> proper# X1, proper# U12(X1, X2, X3) -> U12#(proper X1, proper X2, proper X3))
    (proper# x(X1, X2) -> proper# X1, proper# x(X1, X2) -> proper# X2)
    (proper# x(X1, X2) -> proper# X1, proper# x(X1, X2) -> proper# X1)
    (proper# x(X1, X2) -> proper# X1, proper# x(X1, X2) -> x#(proper X1, proper X2))
    (proper# x(X1, X2) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X3)
    (proper# x(X1, X2) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X2)
    (proper# x(X1, X2) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X1)
    (proper# x(X1, X2) -> proper# X1, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
    (proper# x(X1, X2) -> proper# X1, proper# U22(X1, X2, X3) -> proper# X3)
    (proper# x(X1, X2) -> proper# X1, proper# U22(X1, X2, X3) -> proper# X2)
    (proper# x(X1, X2) -> proper# X1, proper# U22(X1, X2, X3) -> proper# X1)
    (proper# x(X1, X2) -> proper# X1, proper# U22(X1, X2, X3) -> U22#(proper X1, proper X2, proper X3))
    (proper# x(X1, X2) -> proper# X1, proper# plus(X1, X2) -> proper# X2)
    (proper# x(X1, X2) -> proper# X1, proper# plus(X1, X2) -> proper# X1)
    (proper# x(X1, X2) -> proper# X1, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
    (proper# x(X1, X2) -> proper# X1, proper# s X -> proper# X)
    (proper# x(X1, X2) -> proper# X1, proper# s X -> s# proper X)
    (proper# x(X1, X2) -> proper# X1, proper# U11(X1, X2, X3) -> proper# X3)
    (proper# x(X1, X2) -> proper# X1, proper# U11(X1, X2, X3) -> proper# X2)
    (proper# x(X1, X2) -> proper# X1, proper# U11(X1, X2, X3) -> proper# X1)
    (proper# x(X1, X2) -> proper# X1, proper# U11(X1, X2, X3) -> U11#(proper X1, proper X2, proper X3))
    (proper# x(X1, X2) -> proper# X1, proper# U12(X1, X2, X3) -> proper# X3)
    (proper# x(X1, X2) -> proper# X1, proper# U12(X1, X2, X3) -> proper# X2)
    (proper# x(X1, X2) -> proper# X1, proper# U12(X1, X2, X3) -> proper# X1)
    (proper# x(X1, X2) -> proper# X1, proper# U12(X1, X2, X3) -> U12#(proper X1, proper X2, proper X3))
    (proper# U21(X1, X2, X3) -> proper# X1, proper# U12(X1, X2, X3) -> U12#(proper X1, proper X2, proper X3))
    (proper# U21(X1, X2, X3) -> proper# X1, proper# U12(X1, X2, X3) -> proper# X1)
    (proper# U21(X1, X2, X3) -> proper# X1, proper# U12(X1, X2, X3) -> proper# X2)
    (proper# U21(X1, X2, X3) -> proper# X1, proper# U12(X1, X2, X3) -> proper# X3)
    (proper# U21(X1, X2, X3) -> proper# X1, proper# U11(X1, X2, X3) -> U11#(proper X1, proper X2, proper X3))
    (proper# U21(X1, X2, X3) -> proper# X1, proper# U11(X1, X2, X3) -> proper# X1)
    (proper# U21(X1, X2, X3) -> proper# X1, proper# U11(X1, X2, X3) -> proper# X2)
    (proper# U21(X1, X2, X3) -> proper# X1, proper# U11(X1, X2, X3) -> proper# X3)
    (proper# U21(X1, X2, X3) -> proper# X1, proper# s X -> s# proper X)
    (proper# U21(X1, X2, X3) -> proper# X1, proper# s X -> proper# X)
    (proper# U21(X1, X2, X3) -> proper# X1, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
    (proper# U21(X1, X2, X3) -> proper# X1, proper# plus(X1, X2) -> proper# X1)
    (proper# U21(X1, X2, X3) -> proper# X1, proper# plus(X1, X2) -> proper# X2)
    (proper# U21(X1, X2, X3) -> proper# X1, proper# U22(X1, X2, X3) -> U22#(proper X1, proper X2, proper X3))
    (proper# U21(X1, X2, X3) -> proper# X1, proper# U22(X1, X2, X3) -> proper# X1)
    (proper# U21(X1, X2, X3) -> proper# X1, proper# U22(X1, X2, X3) -> proper# X2)
    (proper# U21(X1, X2, X3) -> proper# X1, proper# U22(X1, X2, X3) -> proper# X3)
    (proper# U21(X1, X2, X3) -> proper# X1, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
    (proper# U21(X1, X2, X3) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X1)
    (proper# U21(X1, X2, X3) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X2)
    (proper# U21(X1, X2, X3) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X3)
    (proper# U21(X1, X2, X3) -> proper# X1, proper# x(X1, X2) -> x#(proper X1, proper X2))
    (proper# U21(X1, X2, X3) -> proper# X1, proper# x(X1, X2) -> proper# X1)
    (proper# U21(X1, X2, X3) -> proper# X1, proper# x(X1, X2) -> proper# X2)
    (proper# plus(X1, X2) -> proper# X1, proper# U12(X1, X2, X3) -> U12#(proper X1, proper X2, proper X3))
    (proper# plus(X1, X2) -> proper# X1, proper# U12(X1, X2, X3) -> proper# X1)
    (proper# plus(X1, X2) -> proper# X1, proper# U12(X1, X2, X3) -> proper# X2)
    (proper# plus(X1, X2) -> proper# X1, proper# U12(X1, X2, X3) -> proper# X3)
    (proper# plus(X1, X2) -> proper# X1, proper# U11(X1, X2, X3) -> U11#(proper X1, proper X2, proper X3))
    (proper# plus(X1, X2) -> proper# X1, proper# U11(X1, X2, X3) -> proper# X1)
    (proper# plus(X1, X2) -> proper# X1, proper# U11(X1, X2, X3) -> proper# X2)
    (proper# plus(X1, X2) -> proper# X1, proper# U11(X1, X2, X3) -> proper# X3)
    (proper# plus(X1, X2) -> proper# X1, proper# s X -> s# proper X)
    (proper# plus(X1, X2) -> proper# X1, proper# s X -> proper# X)
    (proper# plus(X1, X2) -> proper# X1, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
    (proper# plus(X1, X2) -> proper# X1, proper# plus(X1, X2) -> proper# X1)
    (proper# plus(X1, X2) -> proper# X1, proper# plus(X1, X2) -> proper# X2)
    (proper# plus(X1, X2) -> proper# X1, proper# U22(X1, X2, X3) -> U22#(proper X1, proper X2, proper X3))
    (proper# plus(X1, X2) -> proper# X1, proper# U22(X1, X2, X3) -> proper# X1)
    (proper# plus(X1, X2) -> proper# X1, proper# U22(X1, X2, X3) -> proper# X2)
    (proper# plus(X1, X2) -> proper# X1, proper# U22(X1, X2, X3) -> proper# X3)
    (proper# plus(X1, X2) -> proper# X1, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
    (proper# plus(X1, X2) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X1)
    (proper# plus(X1, X2) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X2)
    (proper# plus(X1, X2) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X3)
    (proper# plus(X1, X2) -> proper# X1, proper# x(X1, X2) -> x#(proper X1, proper X2))
    (proper# plus(X1, X2) -> proper# X1, proper# x(X1, X2) -> proper# X1)
    (proper# plus(X1, X2) -> proper# X1, proper# x(X1, X2) -> proper# X2)
    (proper# U12(X1, X2, X3) -> proper# X1, proper# U12(X1, X2, X3) -> U12#(proper X1, proper X2, proper X3))
    (proper# U12(X1, X2, X3) -> proper# X1, proper# U12(X1, X2, X3) -> proper# X1)
    (proper# U12(X1, X2, X3) -> proper# X1, proper# U12(X1, X2, X3) -> proper# X2)
    (proper# U12(X1, X2, X3) -> proper# X1, proper# U12(X1, X2, X3) -> proper# X3)
    (proper# U12(X1, X2, X3) -> proper# X1, proper# U11(X1, X2, X3) -> U11#(proper X1, proper X2, proper X3))
    (proper# U12(X1, X2, X3) -> proper# X1, proper# U11(X1, X2, X3) -> proper# X1)
    (proper# U12(X1, X2, X3) -> proper# X1, proper# U11(X1, X2, X3) -> proper# X2)
    (proper# U12(X1, X2, X3) -> proper# X1, proper# U11(X1, X2, X3) -> proper# X3)
    (proper# U12(X1, X2, X3) -> proper# X1, proper# s X -> s# proper X)
    (proper# U12(X1, X2, X3) -> proper# X1, proper# s X -> proper# X)
    (proper# U12(X1, X2, X3) -> proper# X1, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
    (proper# U12(X1, X2, X3) -> proper# X1, proper# plus(X1, X2) -> proper# X1)
    (proper# U12(X1, X2, X3) -> proper# X1, proper# plus(X1, X2) -> proper# X2)
    (proper# U12(X1, X2, X3) -> proper# X1, proper# U22(X1, X2, X3) -> U22#(proper X1, proper X2, proper X3))
    (proper# U12(X1, X2, X3) -> proper# X1, proper# U22(X1, X2, X3) -> proper# X1)
    (proper# U12(X1, X2, X3) -> proper# X1, proper# U22(X1, X2, X3) -> proper# X2)
    (proper# U12(X1, X2, X3) -> proper# X1, proper# U22(X1, X2, X3) -> proper# X3)
    (proper# U12(X1, X2, X3) -> proper# X1, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
    (proper# U12(X1, X2, X3) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X1)
    (proper# U12(X1, X2, X3) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X2)
    (proper# U12(X1, X2, X3) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X3)
    (proper# U12(X1, X2, X3) -> proper# X1, proper# x(X1, X2) -> x#(proper X1, proper X2))
    (proper# U12(X1, X2, X3) -> proper# X1, proper# x(X1, X2) -> proper# X1)
    (proper# U12(X1, X2, X3) -> proper# X1, proper# x(X1, X2) -> proper# X2)
    (active# U21(X1, X2, X3) -> active# X1, active# U12(X1, X2, X3) -> U12#(active X1, X2, X3))
    (active# U21(X1, X2, X3) -> active# X1, active# U12(X1, X2, X3) -> active# X1)
    (active# U21(X1, X2, X3) -> active# X1, active# U12(tt(), M, N) -> s# plus(N, M))
    (active# U21(X1, X2, X3) -> active# X1, active# U12(tt(), M, N) -> plus#(N, M))
    (active# U21(X1, X2, X3) -> active# X1, active# U11(X1, X2, X3) -> active# X1)
    (active# U21(X1, X2, X3) -> active# X1, active# U11(X1, X2, X3) -> U11#(active X1, X2, X3))
    (active# U21(X1, X2, X3) -> active# X1, active# U11(tt(), M, N) -> U12#(tt(), M, N))
    (active# U21(X1, X2, X3) -> active# X1, active# s X -> active# X)
    (active# U21(X1, X2, X3) -> active# X1, active# s X -> s# active X)
    (active# U21(X1, X2, X3) -> active# X1, active# plus(N, s M) -> U11#(tt(), M, N))
    (active# U21(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> active# X1)
    (active# U21(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> active# X2)
    (active# U21(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> plus#(X1, active X2))
    (active# U21(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> plus#(active X1, X2))
    (active# U21(X1, X2, X3) -> active# X1, active# U22(X1, X2, X3) -> active# X1)
    (active# U21(X1, X2, X3) -> active# X1, active# U22(X1, X2, X3) -> U22#(active X1, X2, X3))
    (active# U21(X1, X2, X3) -> active# X1, active# U22(tt(), M, N) -> plus#(x(N, M), N))
    (active# U21(X1, X2, X3) -> active# X1, active# U22(tt(), M, N) -> x#(N, M))
    (active# U21(X1, X2, X3) -> active# X1, active# U21(X1, X2, X3) -> active# X1)
    (active# U21(X1, X2, X3) -> active# X1, active# U21(X1, X2, X3) -> U21#(active X1, X2, X3))
    (active# U21(X1, X2, X3) -> active# X1, active# U21(tt(), M, N) -> U22#(tt(), M, N))
    (active# U21(X1, X2, X3) -> active# X1, active# x(N, s M) -> U21#(tt(), M, N))
    (active# U21(X1, X2, X3) -> active# X1, active# x(X1, X2) -> active# X1)
    (active# U21(X1, X2, X3) -> active# X1, active# x(X1, X2) -> active# X2)
    (active# U21(X1, X2, X3) -> active# X1, active# x(X1, X2) -> x#(X1, active X2))
    (active# U21(X1, X2, X3) -> active# X1, active# x(X1, X2) -> x#(active X1, X2))
    (active# plus(X1, X2) -> active# X1, active# U12(X1, X2, X3) -> U12#(active X1, X2, X3))
    (active# plus(X1, X2) -> active# X1, active# U12(X1, X2, X3) -> active# X1)
    (active# plus(X1, X2) -> active# X1, active# U12(tt(), M, N) -> s# plus(N, M))
    (active# plus(X1, X2) -> active# X1, active# U12(tt(), M, N) -> plus#(N, M))
    (active# plus(X1, X2) -> active# X1, active# U11(X1, X2, X3) -> active# X1)
    (active# plus(X1, X2) -> active# X1, active# U11(X1, X2, X3) -> U11#(active X1, X2, X3))
    (active# plus(X1, X2) -> active# X1, active# U11(tt(), M, N) -> U12#(tt(), M, N))
    (active# plus(X1, X2) -> active# X1, active# s X -> active# X)
    (active# plus(X1, X2) -> active# X1, active# s X -> s# active X)
    (active# plus(X1, X2) -> active# X1, active# plus(N, s M) -> U11#(tt(), M, N))
    (active# plus(X1, X2) -> active# X1, active# plus(X1, X2) -> active# X1)
    (active# plus(X1, X2) -> active# X1, active# plus(X1, X2) -> active# X2)
    (active# plus(X1, X2) -> active# X1, active# plus(X1, X2) -> plus#(X1, active X2))
    (active# plus(X1, X2) -> active# X1, active# plus(X1, X2) -> plus#(active X1, X2))
    (active# plus(X1, X2) -> active# X1, active# U22(X1, X2, X3) -> active# X1)
    (active# plus(X1, X2) -> active# X1, active# U22(X1, X2, X3) -> U22#(active X1, X2, X3))
    (active# plus(X1, X2) -> active# X1, active# U22(tt(), M, N) -> plus#(x(N, M), N))
    (active# plus(X1, X2) -> active# X1, active# U22(tt(), M, N) -> x#(N, M))
    (active# plus(X1, X2) -> active# X1, active# U21(X1, X2, X3) -> active# X1)
    (active# plus(X1, X2) -> active# X1, active# U21(X1, X2, X3) -> U21#(active X1, X2, X3))
    (active# plus(X1, X2) -> active# X1, active# U21(tt(), M, N) -> U22#(tt(), M, N))
    (active# plus(X1, X2) -> active# X1, active# x(N, s M) -> U21#(tt(), M, N))
    (active# plus(X1, X2) -> active# X1, active# x(X1, X2) -> active# X1)
    (active# plus(X1, X2) -> active# X1, active# x(X1, X2) -> active# X2)
    (active# plus(X1, X2) -> active# X1, active# x(X1, X2) -> x#(X1, active X2))
    (active# plus(X1, X2) -> active# X1, active# x(X1, X2) -> x#(active X1, X2))
    (active# U12(X1, X2, X3) -> active# X1, active# U12(X1, X2, X3) -> U12#(active X1, X2, X3))
    (active# U12(X1, X2, X3) -> active# X1, active# U12(X1, X2, X3) -> active# X1)
    (active# U12(X1, X2, X3) -> active# X1, active# U12(tt(), M, N) -> s# plus(N, M))
    (active# U12(X1, X2, X3) -> active# X1, active# U12(tt(), M, N) -> plus#(N, M))
    (active# U12(X1, X2, X3) -> active# X1, active# U11(X1, X2, X3) -> active# X1)
    (active# U12(X1, X2, X3) -> active# X1, active# U11(X1, X2, X3) -> U11#(active X1, X2, X3))
    (active# U12(X1, X2, X3) -> active# X1, active# U11(tt(), M, N) -> U12#(tt(), M, N))
    (active# U12(X1, X2, X3) -> active# X1, active# s X -> active# X)
    (active# U12(X1, X2, X3) -> active# X1, active# s X -> s# active X)
    (active# U12(X1, X2, X3) -> active# X1, active# plus(N, s M) -> U11#(tt(), M, N))
    (active# U12(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> active# X1)
    (active# U12(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> active# X2)
    (active# U12(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> plus#(X1, active X2))
    (active# U12(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> plus#(active X1, X2))
    (active# U12(X1, X2, X3) -> active# X1, active# U22(X1, X2, X3) -> active# X1)
    (active# U12(X1, X2, X3) -> active# X1, active# U22(X1, X2, X3) -> U22#(active X1, X2, X3))
    (active# U12(X1, X2, X3) -> active# X1, active# U22(tt(), M, N) -> plus#(x(N, M), N))
    (active# U12(X1, X2, X3) -> active# X1, active# U22(tt(), M, N) -> x#(N, M))
    (active# U12(X1, X2, X3) -> active# X1, active# U21(X1, X2, X3) -> active# X1)
    (active# U12(X1, X2, X3) -> active# X1, active# U21(X1, X2, X3) -> U21#(active X1, X2, X3))
    (active# U12(X1, X2, X3) -> active# X1, active# U21(tt(), M, N) -> U22#(tt(), M, N))
    (active# U12(X1, X2, X3) -> active# X1, active# x(N, s M) -> U21#(tt(), M, N))
    (active# U12(X1, X2, X3) -> active# X1, active# x(X1, X2) -> active# X1)
    (active# U12(X1, X2, X3) -> active# X1, active# x(X1, X2) -> active# X2)
    (active# U12(X1, X2, X3) -> active# X1, active# x(X1, X2) -> x#(X1, active X2))
    (active# U12(X1, X2, X3) -> active# X1, active# x(X1, X2) -> x#(active X1, X2))
    (proper# U22(X1, X2, X3) -> U22#(proper X1, proper X2, proper X3), U22#(mark X1, X2, X3) -> U22#(X1, X2, X3))
    (proper# U22(X1, X2, X3) -> U22#(proper X1, proper X2, proper X3), U22#(ok X1, ok X2, ok X3) -> U22#(X1, X2, X3))
    (proper# U12(X1, X2, X3) -> U12#(proper X1, proper X2, proper X3), U12#(mark X1, X2, X3) -> U12#(X1, X2, X3))
    (proper# U12(X1, X2, X3) -> U12#(proper X1, proper X2, proper X3), U12#(ok X1, ok X2, ok X3) -> U12#(X1, X2, X3))
    (top# mark X -> proper# X, proper# U12(X1, X2, X3) -> U12#(proper X1, proper X2, proper X3))
    (top# mark X -> proper# X, proper# U12(X1, X2, X3) -> proper# X1)
    (top# mark X -> proper# X, proper# U12(X1, X2, X3) -> proper# X2)
    (top# mark X -> proper# X, proper# U12(X1, X2, X3) -> proper# X3)
    (top# mark X -> proper# X, proper# U11(X1, X2, X3) -> U11#(proper X1, proper X2, proper X3))
    (top# mark X -> proper# X, proper# U11(X1, X2, X3) -> proper# X1)
    (top# mark X -> proper# X, proper# U11(X1, X2, X3) -> proper# X2)
    (top# mark X -> proper# X, proper# U11(X1, X2, X3) -> proper# X3)
    (top# mark X -> proper# X, proper# s X -> s# proper X)
    (top# mark X -> proper# X, proper# s X -> proper# X)
    (top# mark X -> proper# X, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
    (top# mark X -> proper# X, proper# plus(X1, X2) -> proper# X1)
    (top# mark X -> proper# X, proper# plus(X1, X2) -> proper# X2)
    (top# mark X -> proper# X, proper# U22(X1, X2, X3) -> U22#(proper X1, proper X2, proper X3))
    (top# mark X -> proper# X, proper# U22(X1, X2, X3) -> proper# X1)
    (top# mark X -> proper# X, proper# U22(X1, X2, X3) -> proper# X2)
    (top# mark X -> proper# X, proper# U22(X1, X2, X3) -> proper# X3)
    (top# mark X -> proper# X, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
    (top# mark X -> proper# X, proper# U21(X1, X2, X3) -> proper# X1)
    (top# mark X -> proper# X, proper# U21(X1, X2, X3) -> proper# X2)
    (top# mark X -> proper# X, proper# U21(X1, X2, X3) -> proper# X3)
    (top# mark X -> proper# X, proper# x(X1, X2) -> x#(proper X1, proper X2))
    (top# mark X -> proper# X, proper# x(X1, X2) -> proper# X1)
    (top# mark X -> proper# X, proper# x(X1, X2) -> proper# X2)
    (s# ok X -> s# X, s# mark X -> s# X)
    (s# ok X -> s# X, s# ok X -> s# X)
    (active# s X -> active# X, active# U12(X1, X2, X3) -> U12#(active X1, X2, X3))
    (active# s X -> active# X, active# U12(X1, X2, X3) -> active# X1)
    (active# s X -> active# X, active# U12(tt(), M, N) -> s# plus(N, M))
    (active# s X -> active# X, active# U12(tt(), M, N) -> plus#(N, M))
    (active# s X -> active# X, active# U11(X1, X2, X3) -> active# X1)
    (active# s X -> active# X, active# U11(X1, X2, X3) -> U11#(active X1, X2, X3))
    (active# s X -> active# X, active# U11(tt(), M, N) -> U12#(tt(), M, N))
    (active# s X -> active# X, active# s X -> active# X)
    (active# s X -> active# X, active# s X -> s# active X)
    (active# s X -> active# X, active# plus(N, s M) -> U11#(tt(), M, N))
    (active# s X -> active# X, active# plus(X1, X2) -> active# X1)
    (active# s X -> active# X, active# plus(X1, X2) -> active# X2)
    (active# s X -> active# X, active# plus(X1, X2) -> plus#(X1, active X2))
    (active# s X -> active# X, active# plus(X1, X2) -> plus#(active X1, X2))
    (active# s X -> active# X, active# U22(X1, X2, X3) -> active# X1)
    (active# s X -> active# X, active# U22(X1, X2, X3) -> U22#(active X1, X2, X3))
    (active# s X -> active# X, active# U22(tt(), M, N) -> plus#(x(N, M), N))
    (active# s X -> active# X, active# U22(tt(), M, N) -> x#(N, M))
    (active# s X -> active# X, active# U21(X1, X2, X3) -> active# X1)
    (active# s X -> active# X, active# U21(X1, X2, X3) -> U21#(active X1, X2, X3))
    (active# s X -> active# X, active# U21(tt(), M, N) -> U22#(tt(), M, N))
    (active# s X -> active# X, active# x(N, s M) -> U21#(tt(), M, N))
    (active# s X -> active# X, active# x(X1, X2) -> active# X1)
    (active# s X -> active# X, active# x(X1, X2) -> active# X2)
    (active# s X -> active# X, active# x(X1, X2) -> x#(X1, active X2))
    (active# s X -> active# X, active# x(X1, X2) -> x#(active X1, X2))
    (active# U21(tt(), M, N) -> U22#(tt(), M, N), U22#(mark X1, X2, X3) -> U22#(X1, X2, X3))
    (active# U21(tt(), M, N) -> U22#(tt(), M, N), U22#(ok X1, ok X2, ok X3) -> U22#(X1, X2, X3))
    (active# U11(tt(), M, N) -> U12#(tt(), M, N), U12#(mark X1, X2, X3) -> U12#(X1, X2, X3))
    (active# U11(tt(), M, N) -> U12#(tt(), M, N), U12#(ok X1, ok X2, ok X3) -> U12#(X1, X2, X3))
    (x#(ok X1, ok X2) -> x#(X1, X2), x#(X1, mark X2) -> x#(X1, X2))
    (x#(ok X1, ok X2) -> x#(X1, X2), x#(mark X1, X2) -> x#(X1, X2))
    (x#(ok X1, ok X2) -> x#(X1, X2), x#(ok X1, ok X2) -> x#(X1, X2))
    (x#(X1, mark X2) -> x#(X1, X2), x#(X1, mark X2) -> x#(X1, X2))
    (x#(X1, mark X2) -> x#(X1, X2), x#(mark X1, X2) -> x#(X1, X2))
    (x#(X1, mark X2) -> x#(X1, X2), x#(ok X1, ok X2) -> x#(X1, X2))
    (plus#(mark X1, X2) -> plus#(X1, X2), plus#(X1, mark X2) -> plus#(X1, X2))
    (plus#(mark X1, X2) -> plus#(X1, X2), plus#(mark X1, X2) -> plus#(X1, X2))
    (plus#(mark X1, X2) -> plus#(X1, X2), plus#(ok X1, ok X2) -> plus#(X1, X2))
    (top# ok X -> top# active X, top# mark X -> proper# X)
    (top# ok X -> top# active X, top# mark X -> top# proper X)
    (top# ok X -> top# active X, top# ok X -> active# X)
    (top# ok X -> top# active X, top# ok X -> top# active X)
    (proper# s X -> s# proper X, s# mark X -> s# X)
    (proper# s X -> s# proper X, s# ok X -> s# X)
    (active# x(X1, X2) -> x#(active X1, X2), x#(X1, mark X2) -> x#(X1, X2))
    (active# x(X1, X2) -> x#(active X1, X2), x#(mark X1, X2) -> x#(X1, X2))
    (active# x(X1, X2) -> x#(active X1, X2), x#(ok X1, ok X2) -> x#(X1, X2))
    (proper# x(X1, X2) -> x#(proper X1, proper X2), x#(X1, mark X2) -> x#(X1, X2))
    (proper# x(X1, X2) -> x#(proper X1, proper X2), x#(mark X1, X2) -> x#(X1, X2))
    (proper# x(X1, X2) -> x#(proper X1, proper X2), x#(ok X1, ok X2) -> x#(X1, X2))
    (active# x(X1, X2) -> x#(X1, active X2), x#(X1, mark X2) -> x#(X1, X2))
    (active# x(X1, X2) -> x#(X1, active X2), x#(mark X1, X2) -> x#(X1, X2))
    (active# x(X1, X2) -> x#(X1, active X2), x#(ok X1, ok X2) -> x#(X1, X2))
    (proper# U21(X1, X2, X3) -> proper# X3, proper# U12(X1, X2, X3) -> U12#(proper X1, proper X2, proper X3))
    (proper# U21(X1, X2, X3) -> proper# X3, proper# U12(X1, X2, X3) -> proper# X1)
    (proper# U21(X1, X2, X3) -> proper# X3, proper# U12(X1, X2, X3) -> proper# X2)
    (proper# U21(X1, X2, X3) -> proper# X3, proper# U12(X1, X2, X3) -> proper# X3)
    (proper# U21(X1, X2, X3) -> proper# X3, proper# U11(X1, X2, X3) -> U11#(proper X1, proper X2, proper X3))
    (proper# U21(X1, X2, X3) -> proper# X3, proper# U11(X1, X2, X3) -> proper# X1)
    (proper# U21(X1, X2, X3) -> proper# X3, proper# U11(X1, X2, X3) -> proper# X2)
    (proper# U21(X1, X2, X3) -> proper# X3, proper# U11(X1, X2, X3) -> proper# X3)
    (proper# U21(X1, X2, X3) -> proper# X3, proper# s X -> s# proper X)
    (proper# U21(X1, X2, X3) -> proper# X3, proper# s X -> proper# X)
    (proper# U21(X1, X2, X3) -> proper# X3, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
    (proper# U21(X1, X2, X3) -> proper# X3, proper# plus(X1, X2) -> proper# X1)
    (proper# U21(X1, X2, X3) -> proper# X3, proper# plus(X1, X2) -> proper# X2)
    (proper# U21(X1, X2, X3) -> proper# X3, proper# U22(X1, X2, X3) -> U22#(proper X1, proper X2, proper X3))
    (proper# U21(X1, X2, X3) -> proper# X3, proper# U22(X1, X2, X3) -> proper# X1)
    (proper# U21(X1, X2, X3) -> proper# X3, proper# U22(X1, X2, X3) -> proper# X2)
    (proper# U21(X1, X2, X3) -> proper# X3, proper# U22(X1, X2, X3) -> proper# X3)
    (proper# U21(X1, X2, X3) -> proper# X3, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
    (proper# U21(X1, X2, X3) -> proper# X3, proper# U21(X1, X2, X3) -> proper# X1)
    (proper# U21(X1, X2, X3) -> proper# X3, proper# U21(X1, X2, X3) -> proper# X2)
    (proper# U21(X1, X2, X3) -> proper# X3, proper# U21(X1, X2, X3) -> proper# X3)
    (proper# U21(X1, X2, X3) -> proper# X3, proper# x(X1, X2) -> x#(proper X1, proper X2))
    (proper# U21(X1, X2, X3) -> proper# X3, proper# x(X1, X2) -> proper# X1)
    (proper# U21(X1, X2, X3) -> proper# X3, proper# x(X1, X2) -> proper# X2)
    (proper# U11(X1, X2, X3) -> proper# X3, proper# U12(X1, X2, X3) -> U12#(proper X1, proper X2, proper X3))
    (proper# U11(X1, X2, X3) -> proper# X3, proper# U12(X1, X2, X3) -> proper# X1)
    (proper# U11(X1, X2, X3) -> proper# X3, proper# U12(X1, X2, X3) -> proper# X2)
    (proper# U11(X1, X2, X3) -> proper# X3, proper# U12(X1, X2, X3) -> proper# X3)
    (proper# U11(X1, X2, X3) -> proper# X3, proper# U11(X1, X2, X3) -> U11#(proper X1, proper X2, proper X3))
    (proper# U11(X1, X2, X3) -> proper# X3, proper# U11(X1, X2, X3) -> proper# X1)
    (proper# U11(X1, X2, X3) -> proper# X3, proper# U11(X1, X2, X3) -> proper# X2)
    (proper# U11(X1, X2, X3) -> proper# X3, proper# U11(X1, X2, X3) -> proper# X3)
    (proper# U11(X1, X2, X3) -> proper# X3, proper# s X -> s# proper X)
    (proper# U11(X1, X2, X3) -> proper# X3, proper# s X -> proper# X)
    (proper# U11(X1, X2, X3) -> proper# X3, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
    (proper# U11(X1, X2, X3) -> proper# X3, proper# plus(X1, X2) -> proper# X1)
    (proper# U11(X1, X2, X3) -> proper# X3, proper# plus(X1, X2) -> proper# X2)
    (proper# U11(X1, X2, X3) -> proper# X3, proper# U22(X1, X2, X3) -> U22#(proper X1, proper X2, proper X3))
    (proper# U11(X1, X2, X3) -> proper# X3, proper# U22(X1, X2, X3) -> proper# X1)
    (proper# U11(X1, X2, X3) -> proper# X3, proper# U22(X1, X2, X3) -> proper# X2)
    (proper# U11(X1, X2, X3) -> proper# X3, proper# U22(X1, X2, X3) -> proper# X3)
    (proper# U11(X1, X2, X3) -> proper# X3, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
    (proper# U11(X1, X2, X3) -> proper# X3, proper# U21(X1, X2, X3) -> proper# X1)
    (proper# U11(X1, X2, X3) -> proper# X3, proper# U21(X1, X2, X3) -> proper# X2)
    (proper# U11(X1, X2, X3) -> proper# X3, proper# U21(X1, X2, X3) -> proper# X3)
    (proper# U11(X1, X2, X3) -> proper# X3, proper# x(X1, X2) -> x#(proper X1, proper X2))
    (proper# U11(X1, X2, X3) -> proper# X3, proper# x(X1, X2) -> proper# X1)
    (proper# U11(X1, X2, X3) -> proper# X3, proper# x(X1, X2) -> proper# X2)
    (active# U22(tt(), M, N) -> x#(N, M), x#(X1, mark X2) -> x#(X1, X2))
    (active# U22(tt(), M, N) -> x#(N, M), x#(mark X1, X2) -> x#(X1, X2))
    (active# U22(tt(), M, N) -> x#(N, M), x#(ok X1, ok X2) -> x#(X1, X2))
    (U21#(ok X1, ok X2, ok X3) -> U21#(X1, X2, X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3))
    (U21#(ok X1, ok X2, ok X3) -> U21#(X1, X2, X3), U21#(ok X1, ok X2, ok X3) -> U21#(X1, X2, X3))
    (U22#(ok X1, ok X2, ok X3) -> U22#(X1, X2, X3), U22#(mark X1, X2, X3) -> U22#(X1, X2, X3))
    (U22#(ok X1, ok X2, ok X3) -> U22#(X1, X2, X3), U22#(ok X1, ok X2, ok X3) -> U22#(X1, X2, X3))
    (U11#(ok X1, ok X2, ok X3) -> U11#(X1, X2, X3), U11#(mark X1, X2, X3) -> U11#(X1, X2, X3))
    (U11#(ok X1, ok X2, ok X3) -> U11#(X1, X2, X3), U11#(ok X1, ok X2, ok X3) -> U11#(X1, X2, X3))
    (active# U21(X1, X2, X3) -> U21#(active X1, X2, X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3))
    (active# U21(X1, X2, X3) -> U21#(active X1, X2, X3), U21#(ok X1, ok X2, ok X3) -> U21#(X1, X2, X3))
    (active# U11(X1, X2, X3) -> U11#(active X1, X2, X3), U11#(mark X1, X2, X3) -> U11#(X1, X2, X3))
    (active# U11(X1, X2, X3) -> U11#(active X1, X2, X3), U11#(ok X1, ok X2, ok X3) -> U11#(X1, X2, X3))
    (U12#(ok X1, ok X2, ok X3) -> U12#(X1, X2, X3), U12#(mark X1, X2, X3) -> U12#(X1, X2, X3))
    (U12#(ok X1, ok X2, ok X3) -> U12#(X1, X2, X3), U12#(ok X1, ok X2, ok X3) -> U12#(X1, X2, X3))
    (active# U12(tt(), M, N) -> s# plus(N, M), s# mark X -> s# X)
    (active# U12(tt(), M, N) -> s# plus(N, M), s# ok X -> s# X)
    (proper# U21(X1, X2, X3) -> proper# X2, proper# U12(X1, X2, X3) -> U12#(proper X1, proper X2, proper X3))
    (proper# U21(X1, X2, X3) -> proper# X2, proper# U12(X1, X2, X3) -> proper# X1)
    (proper# U21(X1, X2, X3) -> proper# X2, proper# U12(X1, X2, X3) -> proper# X2)
    (proper# U21(X1, X2, X3) -> proper# X2, proper# U12(X1, X2, X3) -> proper# X3)
    (proper# U21(X1, X2, X3) -> proper# X2, proper# U11(X1, X2, X3) -> U11#(proper X1, proper X2, proper X3))
    (proper# U21(X1, X2, X3) -> proper# X2, proper# U11(X1, X2, X3) -> proper# X1)
    (proper# U21(X1, X2, X3) -> proper# X2, proper# U11(X1, X2, X3) -> proper# X2)
    (proper# U21(X1, X2, X3) -> proper# X2, proper# U11(X1, X2, X3) -> proper# X3)
    (proper# U21(X1, X2, X3) -> proper# X2, proper# s X -> s# proper X)
    (proper# U21(X1, X2, X3) -> proper# X2, proper# s X -> proper# X)
    (proper# U21(X1, X2, X3) -> proper# X2, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
    (proper# U21(X1, X2, X3) -> proper# X2, proper# plus(X1, X2) -> proper# X1)
    (proper# U21(X1, X2, X3) -> proper# X2, proper# plus(X1, X2) -> proper# X2)
    (proper# U21(X1, X2, X3) -> proper# X2, proper# U22(X1, X2, X3) -> U22#(proper X1, proper X2, proper X3))
    (proper# U21(X1, X2, X3) -> proper# X2, proper# U22(X1, X2, X3) -> proper# X1)
    (proper# U21(X1, X2, X3) -> proper# X2, proper# U22(X1, X2, X3) -> proper# X2)
    (proper# U21(X1, X2, X3) -> proper# X2, proper# U22(X1, X2, X3) -> proper# X3)
    (proper# U21(X1, X2, X3) -> proper# X2, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
    (proper# U21(X1, X2, X3) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X1)
    (proper# U21(X1, X2, X3) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X2)
    (proper# U21(X1, X2, X3) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X3)
    (proper# U21(X1, X2, X3) -> proper# X2, proper# x(X1, X2) -> x#(proper X1, proper X2))
    (proper# U21(X1, X2, X3) -> proper# X2, proper# x(X1, X2) -> proper# X1)
    (proper# U21(X1, X2, X3) -> proper# X2, proper# x(X1, X2) -> proper# X2)
    (proper# plus(X1, X2) -> proper# X2, proper# U12(X1, X2, X3) -> U12#(proper X1, proper X2, proper X3))
    (proper# plus(X1, X2) -> proper# X2, proper# U12(X1, X2, X3) -> proper# X1)
    (proper# plus(X1, X2) -> proper# X2, proper# U12(X1, X2, X3) -> proper# X2)
    (proper# plus(X1, X2) -> proper# X2, proper# U12(X1, X2, X3) -> proper# X3)
    (proper# plus(X1, X2) -> proper# X2, proper# U11(X1, X2, X3) -> U11#(proper X1, proper X2, proper X3))
    (proper# plus(X1, X2) -> proper# X2, proper# U11(X1, X2, X3) -> proper# X1)
    (proper# plus(X1, X2) -> proper# X2, proper# U11(X1, X2, X3) -> proper# X2)
    (proper# plus(X1, X2) -> proper# X2, proper# U11(X1, X2, X3) -> proper# X3)
    (proper# plus(X1, X2) -> proper# X2, proper# s X -> s# proper X)
    (proper# plus(X1, X2) -> proper# X2, proper# s X -> proper# X)
    (proper# plus(X1, X2) -> proper# X2, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
    (proper# plus(X1, X2) -> proper# X2, proper# plus(X1, X2) -> proper# X1)
    (proper# plus(X1, X2) -> proper# X2, proper# plus(X1, X2) -> proper# X2)
    (proper# plus(X1, X2) -> proper# X2, proper# U22(X1, X2, X3) -> U22#(proper X1, proper X2, proper X3))
    (proper# plus(X1, X2) -> proper# X2, proper# U22(X1, X2, X3) -> proper# X1)
    (proper# plus(X1, X2) -> proper# X2, proper# U22(X1, X2, X3) -> proper# X2)
    (proper# plus(X1, X2) -> proper# X2, proper# U22(X1, X2, X3) -> proper# X3)
    (proper# plus(X1, X2) -> proper# X2, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
    (proper# plus(X1, X2) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X1)
    (proper# plus(X1, X2) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X2)
    (proper# plus(X1, X2) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X3)
    (proper# plus(X1, X2) -> proper# X2, proper# x(X1, X2) -> x#(proper X1, proper X2))
    (proper# plus(X1, X2) -> proper# X2, proper# x(X1, X2) -> proper# X1)
    (proper# plus(X1, X2) -> proper# X2, proper# x(X1, X2) -> proper# X2)
    (proper# U12(X1, X2, X3) -> proper# X2, proper# U12(X1, X2, X3) -> U12#(proper X1, proper X2, proper X3))
    (proper# U12(X1, X2, X3) -> proper# X2, proper# U12(X1, X2, X3) -> proper# X1)
    (proper# U12(X1, X2, X3) -> proper# X2, proper# U12(X1, X2, X3) -> proper# X2)
    (proper# U12(X1, X2, X3) -> proper# X2, proper# U12(X1, X2, X3) -> proper# X3)
    (proper# U12(X1, X2, X3) -> proper# X2, proper# U11(X1, X2, X3) -> U11#(proper X1, proper X2, proper X3))
    (proper# U12(X1, X2, X3) -> proper# X2, proper# U11(X1, X2, X3) -> proper# X1)
    (proper# U12(X1, X2, X3) -> proper# X2, proper# U11(X1, X2, X3) -> proper# X2)
    (proper# U12(X1, X2, X3) -> proper# X2, proper# U11(X1, X2, X3) -> proper# X3)
    (proper# U12(X1, X2, X3) -> proper# X2, proper# s X -> s# proper X)
    (proper# U12(X1, X2, X3) -> proper# X2, proper# s X -> proper# X)
    (proper# U12(X1, X2, X3) -> proper# X2, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
    (proper# U12(X1, X2, X3) -> proper# X2, proper# plus(X1, X2) -> proper# X1)
    (proper# U12(X1, X2, X3) -> proper# X2, proper# plus(X1, X2) -> proper# X2)
    (proper# U12(X1, X2, X3) -> proper# X2, proper# U22(X1, X2, X3) -> U22#(proper X1, proper X2, proper X3))
    (proper# U12(X1, X2, X3) -> proper# X2, proper# U22(X1, X2, X3) -> proper# X1)
    (proper# U12(X1, X2, X3) -> proper# X2, proper# U22(X1, X2, X3) -> proper# X2)
    (proper# U12(X1, X2, X3) -> proper# X2, proper# U22(X1, X2, X3) -> proper# X3)
    (proper# U12(X1, X2, X3) -> proper# X2, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
    (proper# U12(X1, X2, X3) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X1)
    (proper# U12(X1, X2, X3) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X2)
    (proper# U12(X1, X2, X3) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X3)
    (proper# U12(X1, X2, X3) -> proper# X2, proper# x(X1, X2) -> x#(proper X1, proper X2))
    (proper# U12(X1, X2, X3) -> proper# X2, proper# x(X1, X2) -> proper# X1)
    (proper# U12(X1, X2, X3) -> proper# X2, proper# x(X1, X2) -> proper# X2)
    (active# plus(X1, X2) -> active# X2, active# U12(X1, X2, X3) -> U12#(active X1, X2, X3))
    (active# plus(X1, X2) -> active# X2, active# U12(X1, X2, X3) -> active# X1)
    (active# plus(X1, X2) -> active# X2, active# U12(tt(), M, N) -> s# plus(N, M))
    (active# plus(X1, X2) -> active# X2, active# U12(tt(), M, N) -> plus#(N, M))
    (active# plus(X1, X2) -> active# X2, active# U11(X1, X2, X3) -> active# X1)
    (active# plus(X1, X2) -> active# X2, active# U11(X1, X2, X3) -> U11#(active X1, X2, X3))
    (active# plus(X1, X2) -> active# X2, active# U11(tt(), M, N) -> U12#(tt(), M, N))
    (active# plus(X1, X2) -> active# X2, active# s X -> active# X)
    (active# plus(X1, X2) -> active# X2, active# s X -> s# active X)
    (active# plus(X1, X2) -> active# X2, active# plus(N, s M) -> U11#(tt(), M, N))
    (active# plus(X1, X2) -> active# X2, active# plus(X1, X2) -> active# X1)
    (active# plus(X1, X2) -> active# X2, active# plus(X1, X2) -> active# X2)
    (active# plus(X1, X2) -> active# X2, active# plus(X1, X2) -> plus#(X1, active X2))
    (active# plus(X1, X2) -> active# X2, active# plus(X1, X2) -> plus#(active X1, X2))
    (active# plus(X1, X2) -> active# X2, active# U22(X1, X2, X3) -> active# X1)
    (active# plus(X1, X2) -> active# X2, active# U22(X1, X2, X3) -> U22#(active X1, X2, X3))
    (active# plus(X1, X2) -> active# X2, active# U22(tt(), M, N) -> plus#(x(N, M), N))
    (active# plus(X1, X2) -> active# X2, active# U22(tt(), M, N) -> x#(N, M))
    (active# plus(X1, X2) -> active# X2, active# U21(X1, X2, X3) -> active# X1)
    (active# plus(X1, X2) -> active# X2, active# U21(X1, X2, X3) -> U21#(active X1, X2, X3))
    (active# plus(X1, X2) -> active# X2, active# U21(tt(), M, N) -> U22#(tt(), M, N))
    (active# plus(X1, X2) -> active# X2, active# x(N, s M) -> U21#(tt(), M, N))
    (active# plus(X1, X2) -> active# X2, active# x(X1, X2) -> active# X1)
    (active# plus(X1, X2) -> active# X2, active# x(X1, X2) -> active# X2)
    (active# plus(X1, X2) -> active# X2, active# x(X1, X2) -> x#(X1, active X2))
    (active# plus(X1, X2) -> active# X2, active# x(X1, X2) -> x#(active X1, X2))
   }
   EDG:
    {
     (active# x(X1, X2) -> active# X2, active# x(X1, X2) -> x#(active X1, X2))
     (active# x(X1, X2) -> active# X2, active# x(X1, X2) -> x#(X1, active X2))
     (active# x(X1, X2) -> active# X2, active# x(X1, X2) -> active# X2)
     (active# x(X1, X2) -> active# X2, active# x(X1, X2) -> active# X1)
     (active# x(X1, X2) -> active# X2, active# x(N, s M) -> U21#(tt(), M, N))
     (active# x(X1, X2) -> active# X2, active# U21(tt(), M, N) -> U22#(tt(), M, N))
     (active# x(X1, X2) -> active# X2, active# U21(X1, X2, X3) -> U21#(active X1, X2, X3))
     (active# x(X1, X2) -> active# X2, active# U21(X1, X2, X3) -> active# X1)
     (active# x(X1, X2) -> active# X2, active# U22(tt(), M, N) -> x#(N, M))
     (active# x(X1, X2) -> active# X2, active# U22(tt(), M, N) -> plus#(x(N, M), N))
     (active# x(X1, X2) -> active# X2, active# U22(X1, X2, X3) -> U22#(active X1, X2, X3))
     (active# x(X1, X2) -> active# X2, active# U22(X1, X2, X3) -> active# X1)
     (active# x(X1, X2) -> active# X2, active# plus(X1, X2) -> plus#(active X1, X2))
     (active# x(X1, X2) -> active# X2, active# plus(X1, X2) -> plus#(X1, active X2))
     (active# x(X1, X2) -> active# X2, active# plus(X1, X2) -> active# X2)
     (active# x(X1, X2) -> active# X2, active# plus(X1, X2) -> active# X1)
     (active# x(X1, X2) -> active# X2, active# plus(N, s M) -> U11#(tt(), M, N))
     (active# x(X1, X2) -> active# X2, active# s X -> s# active X)
     (active# x(X1, X2) -> active# X2, active# s X -> active# X)
     (active# x(X1, X2) -> active# X2, active# U11(tt(), M, N) -> U12#(tt(), M, N))
     (active# x(X1, X2) -> active# X2, active# U11(X1, X2, X3) -> U11#(active X1, X2, X3))
     (active# x(X1, X2) -> active# X2, active# U11(X1, X2, X3) -> active# X1)
     (active# x(X1, X2) -> active# X2, active# U12(tt(), M, N) -> plus#(N, M))
     (active# x(X1, X2) -> active# X2, active# U12(tt(), M, N) -> s# plus(N, M))
     (active# x(X1, X2) -> active# X2, active# U12(X1, X2, X3) -> active# X1)
     (active# x(X1, X2) -> active# X2, active# U12(X1, X2, X3) -> U12#(active X1, X2, X3))
     (proper# U11(X1, X2, X3) -> proper# X2, proper# x(X1, X2) -> proper# X2)
     (proper# U11(X1, X2, X3) -> proper# X2, proper# x(X1, X2) -> proper# X1)
     (proper# U11(X1, X2, X3) -> proper# X2, proper# x(X1, X2) -> x#(proper X1, proper X2))
     (proper# U11(X1, X2, X3) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X3)
     (proper# U11(X1, X2, X3) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X2)
     (proper# U11(X1, X2, X3) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X1)
     (proper# U11(X1, X2, X3) -> proper# X2, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
     (proper# U11(X1, X2, X3) -> proper# X2, proper# U22(X1, X2, X3) -> proper# X3)
     (proper# U11(X1, X2, X3) -> proper# X2, proper# U22(X1, X2, X3) -> proper# X2)
     (proper# U11(X1, X2, X3) -> proper# X2, proper# U22(X1, X2, X3) -> proper# X1)
     (proper# U11(X1, X2, X3) -> proper# X2, proper# U22(X1, X2, X3) -> U22#(proper X1, proper X2, proper X3))
     (proper# U11(X1, X2, X3) -> proper# X2, proper# plus(X1, X2) -> proper# X2)
     (proper# U11(X1, X2, X3) -> proper# X2, proper# plus(X1, X2) -> proper# X1)
     (proper# U11(X1, X2, X3) -> proper# X2, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# U11(X1, X2, X3) -> proper# X2, proper# s X -> proper# X)
     (proper# U11(X1, X2, X3) -> proper# X2, proper# s X -> s# proper X)
     (proper# U11(X1, X2, X3) -> proper# X2, proper# U11(X1, X2, X3) -> proper# X3)
     (proper# U11(X1, X2, X3) -> proper# X2, proper# U11(X1, X2, X3) -> proper# X2)
     (proper# U11(X1, X2, X3) -> proper# X2, proper# U11(X1, X2, X3) -> proper# X1)
     (proper# U11(X1, X2, X3) -> proper# X2, proper# U11(X1, X2, X3) -> U11#(proper X1, proper X2, proper X3))
     (proper# U11(X1, X2, X3) -> proper# X2, proper# U12(X1, X2, X3) -> proper# X3)
     (proper# U11(X1, X2, X3) -> proper# X2, proper# U12(X1, X2, X3) -> proper# X2)
     (proper# U11(X1, X2, X3) -> proper# X2, proper# U12(X1, X2, X3) -> proper# X1)
     (proper# U11(X1, X2, X3) -> proper# X2, proper# U12(X1, X2, X3) -> U12#(proper X1, proper X2, proper X3))
     (proper# U22(X1, X2, X3) -> proper# X2, proper# x(X1, X2) -> proper# X2)
     (proper# U22(X1, X2, X3) -> proper# X2, proper# x(X1, X2) -> proper# X1)
     (proper# U22(X1, X2, X3) -> proper# X2, proper# x(X1, X2) -> x#(proper X1, proper X2))
     (proper# U22(X1, X2, X3) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X3)
     (proper# U22(X1, X2, X3) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X2)
     (proper# U22(X1, X2, X3) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X1)
     (proper# U22(X1, X2, X3) -> proper# X2, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
     (proper# U22(X1, X2, X3) -> proper# X2, proper# U22(X1, X2, X3) -> proper# X3)
     (proper# U22(X1, X2, X3) -> proper# X2, proper# U22(X1, X2, X3) -> proper# X2)
     (proper# U22(X1, X2, X3) -> proper# X2, proper# U22(X1, X2, X3) -> proper# X1)
     (proper# U22(X1, X2, X3) -> proper# X2, proper# U22(X1, X2, X3) -> U22#(proper X1, proper X2, proper X3))
     (proper# U22(X1, X2, X3) -> proper# X2, proper# plus(X1, X2) -> proper# X2)
     (proper# U22(X1, X2, X3) -> proper# X2, proper# plus(X1, X2) -> proper# X1)
     (proper# U22(X1, X2, X3) -> proper# X2, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# U22(X1, X2, X3) -> proper# X2, proper# s X -> proper# X)
     (proper# U22(X1, X2, X3) -> proper# X2, proper# s X -> s# proper X)
     (proper# U22(X1, X2, X3) -> proper# X2, proper# U11(X1, X2, X3) -> proper# X3)
     (proper# U22(X1, X2, X3) -> proper# X2, proper# U11(X1, X2, X3) -> proper# X2)
     (proper# U22(X1, X2, X3) -> proper# X2, proper# U11(X1, X2, X3) -> proper# X1)
     (proper# U22(X1, X2, X3) -> proper# X2, proper# U11(X1, X2, X3) -> U11#(proper X1, proper X2, proper X3))
     (proper# U22(X1, X2, X3) -> proper# X2, proper# U12(X1, X2, X3) -> proper# X3)
     (proper# U22(X1, X2, X3) -> proper# X2, proper# U12(X1, X2, X3) -> proper# X2)
     (proper# U22(X1, X2, X3) -> proper# X2, proper# U12(X1, X2, X3) -> proper# X1)
     (proper# U22(X1, X2, X3) -> proper# X2, proper# U12(X1, X2, X3) -> U12#(proper X1, proper X2, proper X3))
     (proper# x(X1, X2) -> proper# X2, proper# x(X1, X2) -> proper# X2)
     (proper# x(X1, X2) -> proper# X2, proper# x(X1, X2) -> proper# X1)
     (proper# x(X1, X2) -> proper# X2, proper# x(X1, X2) -> x#(proper X1, proper X2))
     (proper# x(X1, X2) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X3)
     (proper# x(X1, X2) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X2)
     (proper# x(X1, X2) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X1)
     (proper# x(X1, X2) -> proper# X2, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
     (proper# x(X1, X2) -> proper# X2, proper# U22(X1, X2, X3) -> proper# X3)
     (proper# x(X1, X2) -> proper# X2, proper# U22(X1, X2, X3) -> proper# X2)
     (proper# x(X1, X2) -> proper# X2, proper# U22(X1, X2, X3) -> proper# X1)
     (proper# x(X1, X2) -> proper# X2, proper# U22(X1, X2, X3) -> U22#(proper X1, proper X2, proper X3))
     (proper# x(X1, X2) -> proper# X2, proper# plus(X1, X2) -> proper# X2)
     (proper# x(X1, X2) -> proper# X2, proper# plus(X1, X2) -> proper# X1)
     (proper# x(X1, X2) -> proper# X2, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# x(X1, X2) -> proper# X2, proper# s X -> proper# X)
     (proper# x(X1, X2) -> proper# X2, proper# s X -> s# proper X)
     (proper# x(X1, X2) -> proper# X2, proper# U11(X1, X2, X3) -> proper# X3)
     (proper# x(X1, X2) -> proper# X2, proper# U11(X1, X2, X3) -> proper# X2)
     (proper# x(X1, X2) -> proper# X2, proper# U11(X1, X2, X3) -> proper# X1)
     (proper# x(X1, X2) -> proper# X2, proper# U11(X1, X2, X3) -> U11#(proper X1, proper X2, proper X3))
     (proper# x(X1, X2) -> proper# X2, proper# U12(X1, X2, X3) -> proper# X3)
     (proper# x(X1, X2) -> proper# X2, proper# U12(X1, X2, X3) -> proper# X2)
     (proper# x(X1, X2) -> proper# X2, proper# U12(X1, X2, X3) -> proper# X1)
     (proper# x(X1, X2) -> proper# X2, proper# U12(X1, X2, X3) -> U12#(proper X1, proper X2, proper X3))
     (U12#(mark X1, X2, X3) -> U12#(X1, X2, X3), U12#(ok X1, ok X2, ok X3) -> U12#(X1, X2, X3))
     (U12#(mark X1, X2, X3) -> U12#(X1, X2, X3), U12#(mark X1, X2, X3) -> U12#(X1, X2, X3))
     (active# U12(X1, X2, X3) -> U12#(active X1, X2, X3), U12#(ok X1, ok X2, ok X3) -> U12#(X1, X2, X3))
     (active# U12(X1, X2, X3) -> U12#(active X1, X2, X3), U12#(mark X1, X2, X3) -> U12#(X1, X2, X3))
     (active# U22(X1, X2, X3) -> U22#(active X1, X2, X3), U22#(ok X1, ok X2, ok X3) -> U22#(X1, X2, X3))
     (active# U22(X1, X2, X3) -> U22#(active X1, X2, X3), U22#(mark X1, X2, X3) -> U22#(X1, X2, X3))
     (U11#(mark X1, X2, X3) -> U11#(X1, X2, X3), U11#(ok X1, ok X2, ok X3) -> U11#(X1, X2, X3))
     (U11#(mark X1, X2, X3) -> U11#(X1, X2, X3), U11#(mark X1, X2, X3) -> U11#(X1, X2, X3))
     (U22#(mark X1, X2, X3) -> U22#(X1, X2, X3), U22#(ok X1, ok X2, ok X3) -> U22#(X1, X2, X3))
     (U22#(mark X1, X2, X3) -> U22#(X1, X2, X3), U22#(mark X1, X2, X3) -> U22#(X1, X2, X3))
     (U21#(mark X1, X2, X3) -> U21#(X1, X2, X3), U21#(ok X1, ok X2, ok X3) -> U21#(X1, X2, X3))
     (U21#(mark X1, X2, X3) -> U21#(X1, X2, X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3))
     (active# U12(tt(), M, N) -> plus#(N, M), plus#(ok X1, ok X2) -> plus#(X1, X2))
     (active# U12(tt(), M, N) -> plus#(N, M), plus#(mark X1, X2) -> plus#(X1, X2))
     (active# U12(tt(), M, N) -> plus#(N, M), plus#(X1, mark X2) -> plus#(X1, X2))
     (proper# U12(X1, X2, X3) -> proper# X3, proper# x(X1, X2) -> proper# X2)
     (proper# U12(X1, X2, X3) -> proper# X3, proper# x(X1, X2) -> proper# X1)
     (proper# U12(X1, X2, X3) -> proper# X3, proper# x(X1, X2) -> x#(proper X1, proper X2))
     (proper# U12(X1, X2, X3) -> proper# X3, proper# U21(X1, X2, X3) -> proper# X3)
     (proper# U12(X1, X2, X3) -> proper# X3, proper# U21(X1, X2, X3) -> proper# X2)
     (proper# U12(X1, X2, X3) -> proper# X3, proper# U21(X1, X2, X3) -> proper# X1)
     (proper# U12(X1, X2, X3) -> proper# X3, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
     (proper# U12(X1, X2, X3) -> proper# X3, proper# U22(X1, X2, X3) -> proper# X3)
     (proper# U12(X1, X2, X3) -> proper# X3, proper# U22(X1, X2, X3) -> proper# X2)
     (proper# U12(X1, X2, X3) -> proper# X3, proper# U22(X1, X2, X3) -> proper# X1)
     (proper# U12(X1, X2, X3) -> proper# X3, proper# U22(X1, X2, X3) -> U22#(proper X1, proper X2, proper X3))
     (proper# U12(X1, X2, X3) -> proper# X3, proper# plus(X1, X2) -> proper# X2)
     (proper# U12(X1, X2, X3) -> proper# X3, proper# plus(X1, X2) -> proper# X1)
     (proper# U12(X1, X2, X3) -> proper# X3, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# U12(X1, X2, X3) -> proper# X3, proper# s X -> proper# X)
     (proper# U12(X1, X2, X3) -> proper# X3, proper# s X -> s# proper X)
     (proper# U12(X1, X2, X3) -> proper# X3, proper# U11(X1, X2, X3) -> proper# X3)
     (proper# U12(X1, X2, X3) -> proper# X3, proper# U11(X1, X2, X3) -> proper# X2)
     (proper# U12(X1, X2, X3) -> proper# X3, proper# U11(X1, X2, X3) -> proper# X1)
     (proper# U12(X1, X2, X3) -> proper# X3, proper# U11(X1, X2, X3) -> U11#(proper X1, proper X2, proper X3))
     (proper# U12(X1, X2, X3) -> proper# X3, proper# U12(X1, X2, X3) -> proper# X3)
     (proper# U12(X1, X2, X3) -> proper# X3, proper# U12(X1, X2, X3) -> proper# X2)
     (proper# U12(X1, X2, X3) -> proper# X3, proper# U12(X1, X2, X3) -> proper# X1)
     (proper# U12(X1, X2, X3) -> proper# X3, proper# U12(X1, X2, X3) -> U12#(proper X1, proper X2, proper X3))
     (proper# U22(X1, X2, X3) -> proper# X3, proper# x(X1, X2) -> proper# X2)
     (proper# U22(X1, X2, X3) -> proper# X3, proper# x(X1, X2) -> proper# X1)
     (proper# U22(X1, X2, X3) -> proper# X3, proper# x(X1, X2) -> x#(proper X1, proper X2))
     (proper# U22(X1, X2, X3) -> proper# X3, proper# U21(X1, X2, X3) -> proper# X3)
     (proper# U22(X1, X2, X3) -> proper# X3, proper# U21(X1, X2, X3) -> proper# X2)
     (proper# U22(X1, X2, X3) -> proper# X3, proper# U21(X1, X2, X3) -> proper# X1)
     (proper# U22(X1, X2, X3) -> proper# X3, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
     (proper# U22(X1, X2, X3) -> proper# X3, proper# U22(X1, X2, X3) -> proper# X3)
     (proper# U22(X1, X2, X3) -> proper# X3, proper# U22(X1, X2, X3) -> proper# X2)
     (proper# U22(X1, X2, X3) -> proper# X3, proper# U22(X1, X2, X3) -> proper# X1)
     (proper# U22(X1, X2, X3) -> proper# X3, proper# U22(X1, X2, X3) -> U22#(proper X1, proper X2, proper X3))
     (proper# U22(X1, X2, X3) -> proper# X3, proper# plus(X1, X2) -> proper# X2)
     (proper# U22(X1, X2, X3) -> proper# X3, proper# plus(X1, X2) -> proper# X1)
     (proper# U22(X1, X2, X3) -> proper# X3, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# U22(X1, X2, X3) -> proper# X3, proper# s X -> proper# X)
     (proper# U22(X1, X2, X3) -> proper# X3, proper# s X -> s# proper X)
     (proper# U22(X1, X2, X3) -> proper# X3, proper# U11(X1, X2, X3) -> proper# X3)
     (proper# U22(X1, X2, X3) -> proper# X3, proper# U11(X1, X2, X3) -> proper# X2)
     (proper# U22(X1, X2, X3) -> proper# X3, proper# U11(X1, X2, X3) -> proper# X1)
     (proper# U22(X1, X2, X3) -> proper# X3, proper# U11(X1, X2, X3) -> U11#(proper X1, proper X2, proper X3))
     (proper# U22(X1, X2, X3) -> proper# X3, proper# U12(X1, X2, X3) -> proper# X3)
     (proper# U22(X1, X2, X3) -> proper# X3, proper# U12(X1, X2, X3) -> proper# X2)
     (proper# U22(X1, X2, X3) -> proper# X3, proper# U12(X1, X2, X3) -> proper# X1)
     (proper# U22(X1, X2, X3) -> proper# X3, proper# U12(X1, X2, X3) -> U12#(proper X1, proper X2, proper X3))
     (active# plus(X1, X2) -> plus#(X1, active X2), plus#(ok X1, ok X2) -> plus#(X1, X2))
     (active# plus(X1, X2) -> plus#(X1, active X2), plus#(X1, mark X2) -> plus#(X1, X2))
     (proper# plus(X1, X2) -> plus#(proper X1, proper X2), plus#(ok X1, ok X2) -> plus#(X1, X2))
     (proper# plus(X1, X2) -> plus#(proper X1, proper X2), plus#(mark X1, X2) -> plus#(X1, X2))
     (proper# plus(X1, X2) -> plus#(proper X1, proper X2), plus#(X1, mark X2) -> plus#(X1, X2))
     (active# plus(X1, X2) -> plus#(active X1, X2), plus#(ok X1, ok X2) -> plus#(X1, X2))
     (active# plus(X1, X2) -> plus#(active X1, X2), plus#(mark X1, X2) -> plus#(X1, X2))
     (active# s X -> s# active X, s# ok X -> s# X)
     (active# s X -> s# active X, s# mark X -> s# X)
     (top# mark X -> top# proper X, top# ok X -> top# active X)
     (top# mark X -> top# proper X, top# ok X -> active# X)
     (top# mark X -> top# proper X, top# mark X -> top# proper X)
     (top# mark X -> top# proper X, top# mark X -> proper# X)
     (plus#(X1, mark X2) -> plus#(X1, X2), plus#(ok X1, ok X2) -> plus#(X1, X2))
     (plus#(X1, mark X2) -> plus#(X1, X2), plus#(mark X1, X2) -> plus#(X1, X2))
     (plus#(X1, mark X2) -> plus#(X1, X2), plus#(X1, mark X2) -> plus#(X1, X2))
     (plus#(ok X1, ok X2) -> plus#(X1, X2), plus#(ok X1, ok X2) -> plus#(X1, X2))
     (plus#(ok X1, ok X2) -> plus#(X1, X2), plus#(mark X1, X2) -> plus#(X1, X2))
     (plus#(ok X1, ok X2) -> plus#(X1, X2), plus#(X1, mark X2) -> plus#(X1, X2))
     (x#(mark X1, X2) -> x#(X1, X2), x#(ok X1, ok X2) -> x#(X1, X2))
     (x#(mark X1, X2) -> x#(X1, X2), x#(mark X1, X2) -> x#(X1, X2))
     (x#(mark X1, X2) -> x#(X1, X2), x#(X1, mark X2) -> x#(X1, X2))
     (active# U22(tt(), M, N) -> plus#(x(N, M), N), plus#(ok X1, ok X2) -> plus#(X1, X2))
     (active# U22(tt(), M, N) -> plus#(x(N, M), N), plus#(mark X1, X2) -> plus#(X1, X2))
     (active# U22(tt(), M, N) -> plus#(x(N, M), N), plus#(X1, mark X2) -> plus#(X1, X2))
     (s# mark X -> s# X, s# ok X -> s# X)
     (s# mark X -> s# X, s# mark X -> s# X)
     (proper# s X -> proper# X, proper# x(X1, X2) -> proper# X2)
     (proper# s X -> proper# X, proper# x(X1, X2) -> proper# X1)
     (proper# s X -> proper# X, proper# x(X1, X2) -> x#(proper X1, proper X2))
     (proper# s X -> proper# X, proper# U21(X1, X2, X3) -> proper# X3)
     (proper# s X -> proper# X, proper# U21(X1, X2, X3) -> proper# X2)
     (proper# s X -> proper# X, proper# U21(X1, X2, X3) -> proper# X1)
     (proper# s X -> proper# X, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
     (proper# s X -> proper# X, proper# U22(X1, X2, X3) -> proper# X3)
     (proper# s X -> proper# X, proper# U22(X1, X2, X3) -> proper# X2)
     (proper# s X -> proper# X, proper# U22(X1, X2, X3) -> proper# X1)
     (proper# s X -> proper# X, proper# U22(X1, X2, X3) -> U22#(proper X1, proper X2, proper X3))
     (proper# s X -> proper# X, proper# plus(X1, X2) -> proper# X2)
     (proper# s X -> proper# X, proper# plus(X1, X2) -> proper# X1)
     (proper# s X -> proper# X, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# s X -> proper# X, proper# s X -> proper# X)
     (proper# s X -> proper# X, proper# s X -> s# proper X)
     (proper# s X -> proper# X, proper# U11(X1, X2, X3) -> proper# X3)
     (proper# s X -> proper# X, proper# U11(X1, X2, X3) -> proper# X2)
     (proper# s X -> proper# X, proper# U11(X1, X2, X3) -> proper# X1)
     (proper# s X -> proper# X, proper# U11(X1, X2, X3) -> U11#(proper X1, proper X2, proper X3))
     (proper# s X -> proper# X, proper# U12(X1, X2, X3) -> proper# X3)
     (proper# s X -> proper# X, proper# U12(X1, X2, X3) -> proper# X2)
     (proper# s X -> proper# X, proper# U12(X1, X2, X3) -> proper# X1)
     (proper# s X -> proper# X, proper# U12(X1, X2, X3) -> U12#(proper X1, proper X2, proper X3))
     (top# ok X -> active# X, active# x(X1, X2) -> x#(active X1, X2))
     (top# ok X -> active# X, active# x(X1, X2) -> x#(X1, active X2))
     (top# ok X -> active# X, active# x(X1, X2) -> active# X2)
     (top# ok X -> active# X, active# x(X1, X2) -> active# X1)
     (top# ok X -> active# X, active# x(N, s M) -> U21#(tt(), M, N))
     (top# ok X -> active# X, active# U21(tt(), M, N) -> U22#(tt(), M, N))
     (top# ok X -> active# X, active# U21(X1, X2, X3) -> U21#(active X1, X2, X3))
     (top# ok X -> active# X, active# U21(X1, X2, X3) -> active# X1)
     (top# ok X -> active# X, active# U22(tt(), M, N) -> x#(N, M))
     (top# ok X -> active# X, active# U22(tt(), M, N) -> plus#(x(N, M), N))
     (top# ok X -> active# X, active# U22(X1, X2, X3) -> U22#(active X1, X2, X3))
     (top# ok X -> active# X, active# U22(X1, X2, X3) -> active# X1)
     (top# ok X -> active# X, active# plus(X1, X2) -> plus#(active X1, X2))
     (top# ok X -> active# X, active# plus(X1, X2) -> plus#(X1, active X2))
     (top# ok X -> active# X, active# plus(X1, X2) -> active# X2)
     (top# ok X -> active# X, active# plus(X1, X2) -> active# X1)
     (top# ok X -> active# X, active# plus(N, s M) -> U11#(tt(), M, N))
     (top# ok X -> active# X, active# s X -> s# active X)
     (top# ok X -> active# X, active# s X -> active# X)
     (top# ok X -> active# X, active# U11(tt(), M, N) -> U12#(tt(), M, N))
     (top# ok X -> active# X, active# U11(X1, X2, X3) -> U11#(active X1, X2, X3))
     (top# ok X -> active# X, active# U11(X1, X2, X3) -> active# X1)
     (top# ok X -> active# X, active# U12(tt(), M, N) -> plus#(N, M))
     (top# ok X -> active# X, active# U12(tt(), M, N) -> s# plus(N, M))
     (top# ok X -> active# X, active# U12(X1, X2, X3) -> active# X1)
     (top# ok X -> active# X, active# U12(X1, X2, X3) -> U12#(active X1, X2, X3))
     (proper# U11(X1, X2, X3) -> U11#(proper X1, proper X2, proper X3), U11#(ok X1, ok X2, ok X3) -> U11#(X1, X2, X3))
     (proper# U11(X1, X2, X3) -> U11#(proper X1, proper X2, proper X3), U11#(mark X1, X2, X3) -> U11#(X1, X2, X3))
     (proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3), U21#(ok X1, ok X2, ok X3) -> U21#(X1, X2, X3))
     (proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3))
     (active# U11(X1, X2, X3) -> active# X1, active# x(X1, X2) -> x#(active X1, X2))
     (active# U11(X1, X2, X3) -> active# X1, active# x(X1, X2) -> x#(X1, active X2))
     (active# U11(X1, X2, X3) -> active# X1, active# x(X1, X2) -> active# X2)
     (active# U11(X1, X2, X3) -> active# X1, active# x(X1, X2) -> active# X1)
     (active# U11(X1, X2, X3) -> active# X1, active# x(N, s M) -> U21#(tt(), M, N))
     (active# U11(X1, X2, X3) -> active# X1, active# U21(tt(), M, N) -> U22#(tt(), M, N))
     (active# U11(X1, X2, X3) -> active# X1, active# U21(X1, X2, X3) -> U21#(active X1, X2, X3))
     (active# U11(X1, X2, X3) -> active# X1, active# U21(X1, X2, X3) -> active# X1)
     (active# U11(X1, X2, X3) -> active# X1, active# U22(tt(), M, N) -> x#(N, M))
     (active# U11(X1, X2, X3) -> active# X1, active# U22(tt(), M, N) -> plus#(x(N, M), N))
     (active# U11(X1, X2, X3) -> active# X1, active# U22(X1, X2, X3) -> U22#(active X1, X2, X3))
     (active# U11(X1, X2, X3) -> active# X1, active# U22(X1, X2, X3) -> active# X1)
     (active# U11(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> plus#(active X1, X2))
     (active# U11(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> plus#(X1, active X2))
     (active# U11(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> active# X2)
     (active# U11(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> active# X1)
     (active# U11(X1, X2, X3) -> active# X1, active# plus(N, s M) -> U11#(tt(), M, N))
     (active# U11(X1, X2, X3) -> active# X1, active# s X -> s# active X)
     (active# U11(X1, X2, X3) -> active# X1, active# s X -> active# X)
     (active# U11(X1, X2, X3) -> active# X1, active# U11(tt(), M, N) -> U12#(tt(), M, N))
     (active# U11(X1, X2, X3) -> active# X1, active# U11(X1, X2, X3) -> U11#(active X1, X2, X3))
     (active# U11(X1, X2, X3) -> active# X1, active# U11(X1, X2, X3) -> active# X1)
     (active# U11(X1, X2, X3) -> active# X1, active# U12(tt(), M, N) -> plus#(N, M))
     (active# U11(X1, X2, X3) -> active# X1, active# U12(tt(), M, N) -> s# plus(N, M))
     (active# U11(X1, X2, X3) -> active# X1, active# U12(X1, X2, X3) -> active# X1)
     (active# U11(X1, X2, X3) -> active# X1, active# U12(X1, X2, X3) -> U12#(active X1, X2, X3))
     (active# U22(X1, X2, X3) -> active# X1, active# x(X1, X2) -> x#(active X1, X2))
     (active# U22(X1, X2, X3) -> active# X1, active# x(X1, X2) -> x#(X1, active X2))
     (active# U22(X1, X2, X3) -> active# X1, active# x(X1, X2) -> active# X2)
     (active# U22(X1, X2, X3) -> active# X1, active# x(X1, X2) -> active# X1)
     (active# U22(X1, X2, X3) -> active# X1, active# x(N, s M) -> U21#(tt(), M, N))
     (active# U22(X1, X2, X3) -> active# X1, active# U21(tt(), M, N) -> U22#(tt(), M, N))
     (active# U22(X1, X2, X3) -> active# X1, active# U21(X1, X2, X3) -> U21#(active X1, X2, X3))
     (active# U22(X1, X2, X3) -> active# X1, active# U21(X1, X2, X3) -> active# X1)
     (active# U22(X1, X2, X3) -> active# X1, active# U22(tt(), M, N) -> x#(N, M))
     (active# U22(X1, X2, X3) -> active# X1, active# U22(tt(), M, N) -> plus#(x(N, M), N))
     (active# U22(X1, X2, X3) -> active# X1, active# U22(X1, X2, X3) -> U22#(active X1, X2, X3))
     (active# U22(X1, X2, X3) -> active# X1, active# U22(X1, X2, X3) -> active# X1)
     (active# U22(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> plus#(active X1, X2))
     (active# U22(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> plus#(X1, active X2))
     (active# U22(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> active# X2)
     (active# U22(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> active# X1)
     (active# U22(X1, X2, X3) -> active# X1, active# plus(N, s M) -> U11#(tt(), M, N))
     (active# U22(X1, X2, X3) -> active# X1, active# s X -> s# active X)
     (active# U22(X1, X2, X3) -> active# X1, active# s X -> active# X)
     (active# U22(X1, X2, X3) -> active# X1, active# U11(tt(), M, N) -> U12#(tt(), M, N))
     (active# U22(X1, X2, X3) -> active# X1, active# U11(X1, X2, X3) -> U11#(active X1, X2, X3))
     (active# U22(X1, X2, X3) -> active# X1, active# U11(X1, X2, X3) -> active# X1)
     (active# U22(X1, X2, X3) -> active# X1, active# U12(tt(), M, N) -> plus#(N, M))
     (active# U22(X1, X2, X3) -> active# X1, active# U12(tt(), M, N) -> s# plus(N, M))
     (active# U22(X1, X2, X3) -> active# X1, active# U12(X1, X2, X3) -> active# X1)
     (active# U22(X1, X2, X3) -> active# X1, active# U12(X1, X2, X3) -> U12#(active X1, X2, X3))
     (active# x(X1, X2) -> active# X1, active# x(X1, X2) -> x#(active X1, X2))
     (active# x(X1, X2) -> active# X1, active# x(X1, X2) -> x#(X1, active X2))
     (active# x(X1, X2) -> active# X1, active# x(X1, X2) -> active# X2)
     (active# x(X1, X2) -> active# X1, active# x(X1, X2) -> active# X1)
     (active# x(X1, X2) -> active# X1, active# x(N, s M) -> U21#(tt(), M, N))
     (active# x(X1, X2) -> active# X1, active# U21(tt(), M, N) -> U22#(tt(), M, N))
     (active# x(X1, X2) -> active# X1, active# U21(X1, X2, X3) -> U21#(active X1, X2, X3))
     (active# x(X1, X2) -> active# X1, active# U21(X1, X2, X3) -> active# X1)
     (active# x(X1, X2) -> active# X1, active# U22(tt(), M, N) -> x#(N, M))
     (active# x(X1, X2) -> active# X1, active# U22(tt(), M, N) -> plus#(x(N, M), N))
     (active# x(X1, X2) -> active# X1, active# U22(X1, X2, X3) -> U22#(active X1, X2, X3))
     (active# x(X1, X2) -> active# X1, active# U22(X1, X2, X3) -> active# X1)
     (active# x(X1, X2) -> active# X1, active# plus(X1, X2) -> plus#(active X1, X2))
     (active# x(X1, X2) -> active# X1, active# plus(X1, X2) -> plus#(X1, active X2))
     (active# x(X1, X2) -> active# X1, active# plus(X1, X2) -> active# X2)
     (active# x(X1, X2) -> active# X1, active# plus(X1, X2) -> active# X1)
     (active# x(X1, X2) -> active# X1, active# plus(N, s M) -> U11#(tt(), M, N))
     (active# x(X1, X2) -> active# X1, active# s X -> s# active X)
     (active# x(X1, X2) -> active# X1, active# s X -> active# X)
     (active# x(X1, X2) -> active# X1, active# U11(tt(), M, N) -> U12#(tt(), M, N))
     (active# x(X1, X2) -> active# X1, active# U11(X1, X2, X3) -> U11#(active X1, X2, X3))
     (active# x(X1, X2) -> active# X1, active# U11(X1, X2, X3) -> active# X1)
     (active# x(X1, X2) -> active# X1, active# U12(tt(), M, N) -> plus#(N, M))
     (active# x(X1, X2) -> active# X1, active# U12(tt(), M, N) -> s# plus(N, M))
     (active# x(X1, X2) -> active# X1, active# U12(X1, X2, X3) -> active# X1)
     (active# x(X1, X2) -> active# X1, active# U12(X1, X2, X3) -> U12#(active X1, X2, X3))
     (proper# U11(X1, X2, X3) -> proper# X1, proper# x(X1, X2) -> proper# X2)
     (proper# U11(X1, X2, X3) -> proper# X1, proper# x(X1, X2) -> proper# X1)
     (proper# U11(X1, X2, X3) -> proper# X1, proper# x(X1, X2) -> x#(proper X1, proper X2))
     (proper# U11(X1, X2, X3) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X3)
     (proper# U11(X1, X2, X3) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X2)
     (proper# U11(X1, X2, X3) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X1)
     (proper# U11(X1, X2, X3) -> proper# X1, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
     (proper# U11(X1, X2, X3) -> proper# X1, proper# U22(X1, X2, X3) -> proper# X3)
     (proper# U11(X1, X2, X3) -> proper# X1, proper# U22(X1, X2, X3) -> proper# X2)
     (proper# U11(X1, X2, X3) -> proper# X1, proper# U22(X1, X2, X3) -> proper# X1)
     (proper# U11(X1, X2, X3) -> proper# X1, proper# U22(X1, X2, X3) -> U22#(proper X1, proper X2, proper X3))
     (proper# U11(X1, X2, X3) -> proper# X1, proper# plus(X1, X2) -> proper# X2)
     (proper# U11(X1, X2, X3) -> proper# X1, proper# plus(X1, X2) -> proper# X1)
     (proper# U11(X1, X2, X3) -> proper# X1, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# U11(X1, X2, X3) -> proper# X1, proper# s X -> proper# X)
     (proper# U11(X1, X2, X3) -> proper# X1, proper# s X -> s# proper X)
     (proper# U11(X1, X2, X3) -> proper# X1, proper# U11(X1, X2, X3) -> proper# X3)
     (proper# U11(X1, X2, X3) -> proper# X1, proper# U11(X1, X2, X3) -> proper# X2)
     (proper# U11(X1, X2, X3) -> proper# X1, proper# U11(X1, X2, X3) -> proper# X1)
     (proper# U11(X1, X2, X3) -> proper# X1, proper# U11(X1, X2, X3) -> U11#(proper X1, proper X2, proper X3))
     (proper# U11(X1, X2, X3) -> proper# X1, proper# U12(X1, X2, X3) -> proper# X3)
     (proper# U11(X1, X2, X3) -> proper# X1, proper# U12(X1, X2, X3) -> proper# X2)
     (proper# U11(X1, X2, X3) -> proper# X1, proper# U12(X1, X2, X3) -> proper# X1)
     (proper# U11(X1, X2, X3) -> proper# X1, proper# U12(X1, X2, X3) -> U12#(proper X1, proper X2, proper X3))
     (proper# U22(X1, X2, X3) -> proper# X1, proper# x(X1, X2) -> proper# X2)
     (proper# U22(X1, X2, X3) -> proper# X1, proper# x(X1, X2) -> proper# X1)
     (proper# U22(X1, X2, X3) -> proper# X1, proper# x(X1, X2) -> x#(proper X1, proper X2))
     (proper# U22(X1, X2, X3) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X3)
     (proper# U22(X1, X2, X3) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X2)
     (proper# U22(X1, X2, X3) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X1)
     (proper# U22(X1, X2, X3) -> proper# X1, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
     (proper# U22(X1, X2, X3) -> proper# X1, proper# U22(X1, X2, X3) -> proper# X3)
     (proper# U22(X1, X2, X3) -> proper# X1, proper# U22(X1, X2, X3) -> proper# X2)
     (proper# U22(X1, X2, X3) -> proper# X1, proper# U22(X1, X2, X3) -> proper# X1)
     (proper# U22(X1, X2, X3) -> proper# X1, proper# U22(X1, X2, X3) -> U22#(proper X1, proper X2, proper X3))
     (proper# U22(X1, X2, X3) -> proper# X1, proper# plus(X1, X2) -> proper# X2)
     (proper# U22(X1, X2, X3) -> proper# X1, proper# plus(X1, X2) -> proper# X1)
     (proper# U22(X1, X2, X3) -> proper# X1, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# U22(X1, X2, X3) -> proper# X1, proper# s X -> proper# X)
     (proper# U22(X1, X2, X3) -> proper# X1, proper# s X -> s# proper X)
     (proper# U22(X1, X2, X3) -> proper# X1, proper# U11(X1, X2, X3) -> proper# X3)
     (proper# U22(X1, X2, X3) -> proper# X1, proper# U11(X1, X2, X3) -> proper# X2)
     (proper# U22(X1, X2, X3) -> proper# X1, proper# U11(X1, X2, X3) -> proper# X1)
     (proper# U22(X1, X2, X3) -> proper# X1, proper# U11(X1, X2, X3) -> U11#(proper X1, proper X2, proper X3))
     (proper# U22(X1, X2, X3) -> proper# X1, proper# U12(X1, X2, X3) -> proper# X3)
     (proper# U22(X1, X2, X3) -> proper# X1, proper# U12(X1, X2, X3) -> proper# X2)
     (proper# U22(X1, X2, X3) -> proper# X1, proper# U12(X1, X2, X3) -> proper# X1)
     (proper# U22(X1, X2, X3) -> proper# X1, proper# U12(X1, X2, X3) -> U12#(proper X1, proper X2, proper X3))
     (proper# x(X1, X2) -> proper# X1, proper# x(X1, X2) -> proper# X2)
     (proper# x(X1, X2) -> proper# X1, proper# x(X1, X2) -> proper# X1)
     (proper# x(X1, X2) -> proper# X1, proper# x(X1, X2) -> x#(proper X1, proper X2))
     (proper# x(X1, X2) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X3)
     (proper# x(X1, X2) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X2)
     (proper# x(X1, X2) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X1)
     (proper# x(X1, X2) -> proper# X1, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
     (proper# x(X1, X2) -> proper# X1, proper# U22(X1, X2, X3) -> proper# X3)
     (proper# x(X1, X2) -> proper# X1, proper# U22(X1, X2, X3) -> proper# X2)
     (proper# x(X1, X2) -> proper# X1, proper# U22(X1, X2, X3) -> proper# X1)
     (proper# x(X1, X2) -> proper# X1, proper# U22(X1, X2, X3) -> U22#(proper X1, proper X2, proper X3))
     (proper# x(X1, X2) -> proper# X1, proper# plus(X1, X2) -> proper# X2)
     (proper# x(X1, X2) -> proper# X1, proper# plus(X1, X2) -> proper# X1)
     (proper# x(X1, X2) -> proper# X1, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# x(X1, X2) -> proper# X1, proper# s X -> proper# X)
     (proper# x(X1, X2) -> proper# X1, proper# s X -> s# proper X)
     (proper# x(X1, X2) -> proper# X1, proper# U11(X1, X2, X3) -> proper# X3)
     (proper# x(X1, X2) -> proper# X1, proper# U11(X1, X2, X3) -> proper# X2)
     (proper# x(X1, X2) -> proper# X1, proper# U11(X1, X2, X3) -> proper# X1)
     (proper# x(X1, X2) -> proper# X1, proper# U11(X1, X2, X3) -> U11#(proper X1, proper X2, proper X3))
     (proper# x(X1, X2) -> proper# X1, proper# U12(X1, X2, X3) -> proper# X3)
     (proper# x(X1, X2) -> proper# X1, proper# U12(X1, X2, X3) -> proper# X2)
     (proper# x(X1, X2) -> proper# X1, proper# U12(X1, X2, X3) -> proper# X1)
     (proper# x(X1, X2) -> proper# X1, proper# U12(X1, X2, X3) -> U12#(proper X1, proper X2, proper X3))
     (proper# U21(X1, X2, X3) -> proper# X1, proper# U12(X1, X2, X3) -> U12#(proper X1, proper X2, proper X3))
     (proper# U21(X1, X2, X3) -> proper# X1, proper# U12(X1, X2, X3) -> proper# X1)
     (proper# U21(X1, X2, X3) -> proper# X1, proper# U12(X1, X2, X3) -> proper# X2)
     (proper# U21(X1, X2, X3) -> proper# X1, proper# U12(X1, X2, X3) -> proper# X3)
     (proper# U21(X1, X2, X3) -> proper# X1, proper# U11(X1, X2, X3) -> U11#(proper X1, proper X2, proper X3))
     (proper# U21(X1, X2, X3) -> proper# X1, proper# U11(X1, X2, X3) -> proper# X1)
     (proper# U21(X1, X2, X3) -> proper# X1, proper# U11(X1, X2, X3) -> proper# X2)
     (proper# U21(X1, X2, X3) -> proper# X1, proper# U11(X1, X2, X3) -> proper# X3)
     (proper# U21(X1, X2, X3) -> proper# X1, proper# s X -> s# proper X)
     (proper# U21(X1, X2, X3) -> proper# X1, proper# s X -> proper# X)
     (proper# U21(X1, X2, X3) -> proper# X1, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# U21(X1, X2, X3) -> proper# X1, proper# plus(X1, X2) -> proper# X1)
     (proper# U21(X1, X2, X3) -> proper# X1, proper# plus(X1, X2) -> proper# X2)
     (proper# U21(X1, X2, X3) -> proper# X1, proper# U22(X1, X2, X3) -> U22#(proper X1, proper X2, proper X3))
     (proper# U21(X1, X2, X3) -> proper# X1, proper# U22(X1, X2, X3) -> proper# X1)
     (proper# U21(X1, X2, X3) -> proper# X1, proper# U22(X1, X2, X3) -> proper# X2)
     (proper# U21(X1, X2, X3) -> proper# X1, proper# U22(X1, X2, X3) -> proper# X3)
     (proper# U21(X1, X2, X3) -> proper# X1, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
     (proper# U21(X1, X2, X3) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X1)
     (proper# U21(X1, X2, X3) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X2)
     (proper# U21(X1, X2, X3) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X3)
     (proper# U21(X1, X2, X3) -> proper# X1, proper# x(X1, X2) -> x#(proper X1, proper X2))
     (proper# U21(X1, X2, X3) -> proper# X1, proper# x(X1, X2) -> proper# X1)
     (proper# U21(X1, X2, X3) -> proper# X1, proper# x(X1, X2) -> proper# X2)
     (proper# plus(X1, X2) -> proper# X1, proper# U12(X1, X2, X3) -> U12#(proper X1, proper X2, proper X3))
     (proper# plus(X1, X2) -> proper# X1, proper# U12(X1, X2, X3) -> proper# X1)
     (proper# plus(X1, X2) -> proper# X1, proper# U12(X1, X2, X3) -> proper# X2)
     (proper# plus(X1, X2) -> proper# X1, proper# U12(X1, X2, X3) -> proper# X3)
     (proper# plus(X1, X2) -> proper# X1, proper# U11(X1, X2, X3) -> U11#(proper X1, proper X2, proper X3))
     (proper# plus(X1, X2) -> proper# X1, proper# U11(X1, X2, X3) -> proper# X1)
     (proper# plus(X1, X2) -> proper# X1, proper# U11(X1, X2, X3) -> proper# X2)
     (proper# plus(X1, X2) -> proper# X1, proper# U11(X1, X2, X3) -> proper# X3)
     (proper# plus(X1, X2) -> proper# X1, proper# s X -> s# proper X)
     (proper# plus(X1, X2) -> proper# X1, proper# s X -> proper# X)
     (proper# plus(X1, X2) -> proper# X1, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# plus(X1, X2) -> proper# X1, proper# plus(X1, X2) -> proper# X1)
     (proper# plus(X1, X2) -> proper# X1, proper# plus(X1, X2) -> proper# X2)
     (proper# plus(X1, X2) -> proper# X1, proper# U22(X1, X2, X3) -> U22#(proper X1, proper X2, proper X3))
     (proper# plus(X1, X2) -> proper# X1, proper# U22(X1, X2, X3) -> proper# X1)
     (proper# plus(X1, X2) -> proper# X1, proper# U22(X1, X2, X3) -> proper# X2)
     (proper# plus(X1, X2) -> proper# X1, proper# U22(X1, X2, X3) -> proper# X3)
     (proper# plus(X1, X2) -> proper# X1, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
     (proper# plus(X1, X2) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X1)
     (proper# plus(X1, X2) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X2)
     (proper# plus(X1, X2) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X3)
     (proper# plus(X1, X2) -> proper# X1, proper# x(X1, X2) -> x#(proper X1, proper X2))
     (proper# plus(X1, X2) -> proper# X1, proper# x(X1, X2) -> proper# X1)
     (proper# plus(X1, X2) -> proper# X1, proper# x(X1, X2) -> proper# X2)
     (proper# U12(X1, X2, X3) -> proper# X1, proper# U12(X1, X2, X3) -> U12#(proper X1, proper X2, proper X3))
     (proper# U12(X1, X2, X3) -> proper# X1, proper# U12(X1, X2, X3) -> proper# X1)
     (proper# U12(X1, X2, X3) -> proper# X1, proper# U12(X1, X2, X3) -> proper# X2)
     (proper# U12(X1, X2, X3) -> proper# X1, proper# U12(X1, X2, X3) -> proper# X3)
     (proper# U12(X1, X2, X3) -> proper# X1, proper# U11(X1, X2, X3) -> U11#(proper X1, proper X2, proper X3))
     (proper# U12(X1, X2, X3) -> proper# X1, proper# U11(X1, X2, X3) -> proper# X1)
     (proper# U12(X1, X2, X3) -> proper# X1, proper# U11(X1, X2, X3) -> proper# X2)
     (proper# U12(X1, X2, X3) -> proper# X1, proper# U11(X1, X2, X3) -> proper# X3)
     (proper# U12(X1, X2, X3) -> proper# X1, proper# s X -> s# proper X)
     (proper# U12(X1, X2, X3) -> proper# X1, proper# s X -> proper# X)
     (proper# U12(X1, X2, X3) -> proper# X1, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# U12(X1, X2, X3) -> proper# X1, proper# plus(X1, X2) -> proper# X1)
     (proper# U12(X1, X2, X3) -> proper# X1, proper# plus(X1, X2) -> proper# X2)
     (proper# U12(X1, X2, X3) -> proper# X1, proper# U22(X1, X2, X3) -> U22#(proper X1, proper X2, proper X3))
     (proper# U12(X1, X2, X3) -> proper# X1, proper# U22(X1, X2, X3) -> proper# X1)
     (proper# U12(X1, X2, X3) -> proper# X1, proper# U22(X1, X2, X3) -> proper# X2)
     (proper# U12(X1, X2, X3) -> proper# X1, proper# U22(X1, X2, X3) -> proper# X3)
     (proper# U12(X1, X2, X3) -> proper# X1, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
     (proper# U12(X1, X2, X3) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X1)
     (proper# U12(X1, X2, X3) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X2)
     (proper# U12(X1, X2, X3) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X3)
     (proper# U12(X1, X2, X3) -> proper# X1, proper# x(X1, X2) -> x#(proper X1, proper X2))
     (proper# U12(X1, X2, X3) -> proper# X1, proper# x(X1, X2) -> proper# X1)
     (proper# U12(X1, X2, X3) -> proper# X1, proper# x(X1, X2) -> proper# X2)
     (active# U21(X1, X2, X3) -> active# X1, active# U12(X1, X2, X3) -> U12#(active X1, X2, X3))
     (active# U21(X1, X2, X3) -> active# X1, active# U12(X1, X2, X3) -> active# X1)
     (active# U21(X1, X2, X3) -> active# X1, active# U12(tt(), M, N) -> s# plus(N, M))
     (active# U21(X1, X2, X3) -> active# X1, active# U12(tt(), M, N) -> plus#(N, M))
     (active# U21(X1, X2, X3) -> active# X1, active# U11(X1, X2, X3) -> active# X1)
     (active# U21(X1, X2, X3) -> active# X1, active# U11(X1, X2, X3) -> U11#(active X1, X2, X3))
     (active# U21(X1, X2, X3) -> active# X1, active# U11(tt(), M, N) -> U12#(tt(), M, N))
     (active# U21(X1, X2, X3) -> active# X1, active# s X -> active# X)
     (active# U21(X1, X2, X3) -> active# X1, active# s X -> s# active X)
     (active# U21(X1, X2, X3) -> active# X1, active# plus(N, s M) -> U11#(tt(), M, N))
     (active# U21(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> active# X1)
     (active# U21(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> active# X2)
     (active# U21(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> plus#(X1, active X2))
     (active# U21(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> plus#(active X1, X2))
     (active# U21(X1, X2, X3) -> active# X1, active# U22(X1, X2, X3) -> active# X1)
     (active# U21(X1, X2, X3) -> active# X1, active# U22(X1, X2, X3) -> U22#(active X1, X2, X3))
     (active# U21(X1, X2, X3) -> active# X1, active# U22(tt(), M, N) -> plus#(x(N, M), N))
     (active# U21(X1, X2, X3) -> active# X1, active# U22(tt(), M, N) -> x#(N, M))
     (active# U21(X1, X2, X3) -> active# X1, active# U21(X1, X2, X3) -> active# X1)
     (active# U21(X1, X2, X3) -> active# X1, active# U21(X1, X2, X3) -> U21#(active X1, X2, X3))
     (active# U21(X1, X2, X3) -> active# X1, active# U21(tt(), M, N) -> U22#(tt(), M, N))
     (active# U21(X1, X2, X3) -> active# X1, active# x(N, s M) -> U21#(tt(), M, N))
     (active# U21(X1, X2, X3) -> active# X1, active# x(X1, X2) -> active# X1)
     (active# U21(X1, X2, X3) -> active# X1, active# x(X1, X2) -> active# X2)
     (active# U21(X1, X2, X3) -> active# X1, active# x(X1, X2) -> x#(X1, active X2))
     (active# U21(X1, X2, X3) -> active# X1, active# x(X1, X2) -> x#(active X1, X2))
     (active# plus(X1, X2) -> active# X1, active# U12(X1, X2, X3) -> U12#(active X1, X2, X3))
     (active# plus(X1, X2) -> active# X1, active# U12(X1, X2, X3) -> active# X1)
     (active# plus(X1, X2) -> active# X1, active# U12(tt(), M, N) -> s# plus(N, M))
     (active# plus(X1, X2) -> active# X1, active# U12(tt(), M, N) -> plus#(N, M))
     (active# plus(X1, X2) -> active# X1, active# U11(X1, X2, X3) -> active# X1)
     (active# plus(X1, X2) -> active# X1, active# U11(X1, X2, X3) -> U11#(active X1, X2, X3))
     (active# plus(X1, X2) -> active# X1, active# U11(tt(), M, N) -> U12#(tt(), M, N))
     (active# plus(X1, X2) -> active# X1, active# s X -> active# X)
     (active# plus(X1, X2) -> active# X1, active# s X -> s# active X)
     (active# plus(X1, X2) -> active# X1, active# plus(N, s M) -> U11#(tt(), M, N))
     (active# plus(X1, X2) -> active# X1, active# plus(X1, X2) -> active# X1)
     (active# plus(X1, X2) -> active# X1, active# plus(X1, X2) -> active# X2)
     (active# plus(X1, X2) -> active# X1, active# plus(X1, X2) -> plus#(X1, active X2))
     (active# plus(X1, X2) -> active# X1, active# plus(X1, X2) -> plus#(active X1, X2))
     (active# plus(X1, X2) -> active# X1, active# U22(X1, X2, X3) -> active# X1)
     (active# plus(X1, X2) -> active# X1, active# U22(X1, X2, X3) -> U22#(active X1, X2, X3))
     (active# plus(X1, X2) -> active# X1, active# U22(tt(), M, N) -> plus#(x(N, M), N))
     (active# plus(X1, X2) -> active# X1, active# U22(tt(), M, N) -> x#(N, M))
     (active# plus(X1, X2) -> active# X1, active# U21(X1, X2, X3) -> active# X1)
     (active# plus(X1, X2) -> active# X1, active# U21(X1, X2, X3) -> U21#(active X1, X2, X3))
     (active# plus(X1, X2) -> active# X1, active# U21(tt(), M, N) -> U22#(tt(), M, N))
     (active# plus(X1, X2) -> active# X1, active# x(N, s M) -> U21#(tt(), M, N))
     (active# plus(X1, X2) -> active# X1, active# x(X1, X2) -> active# X1)
     (active# plus(X1, X2) -> active# X1, active# x(X1, X2) -> active# X2)
     (active# plus(X1, X2) -> active# X1, active# x(X1, X2) -> x#(X1, active X2))
     (active# plus(X1, X2) -> active# X1, active# x(X1, X2) -> x#(active X1, X2))
     (active# U12(X1, X2, X3) -> active# X1, active# U12(X1, X2, X3) -> U12#(active X1, X2, X3))
     (active# U12(X1, X2, X3) -> active# X1, active# U12(X1, X2, X3) -> active# X1)
     (active# U12(X1, X2, X3) -> active# X1, active# U12(tt(), M, N) -> s# plus(N, M))
     (active# U12(X1, X2, X3) -> active# X1, active# U12(tt(), M, N) -> plus#(N, M))
     (active# U12(X1, X2, X3) -> active# X1, active# U11(X1, X2, X3) -> active# X1)
     (active# U12(X1, X2, X3) -> active# X1, active# U11(X1, X2, X3) -> U11#(active X1, X2, X3))
     (active# U12(X1, X2, X3) -> active# X1, active# U11(tt(), M, N) -> U12#(tt(), M, N))
     (active# U12(X1, X2, X3) -> active# X1, active# s X -> active# X)
     (active# U12(X1, X2, X3) -> active# X1, active# s X -> s# active X)
     (active# U12(X1, X2, X3) -> active# X1, active# plus(N, s M) -> U11#(tt(), M, N))
     (active# U12(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> active# X1)
     (active# U12(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> active# X2)
     (active# U12(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> plus#(X1, active X2))
     (active# U12(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> plus#(active X1, X2))
     (active# U12(X1, X2, X3) -> active# X1, active# U22(X1, X2, X3) -> active# X1)
     (active# U12(X1, X2, X3) -> active# X1, active# U22(X1, X2, X3) -> U22#(active X1, X2, X3))
     (active# U12(X1, X2, X3) -> active# X1, active# U22(tt(), M, N) -> plus#(x(N, M), N))
     (active# U12(X1, X2, X3) -> active# X1, active# U22(tt(), M, N) -> x#(N, M))
     (active# U12(X1, X2, X3) -> active# X1, active# U21(X1, X2, X3) -> active# X1)
     (active# U12(X1, X2, X3) -> active# X1, active# U21(X1, X2, X3) -> U21#(active X1, X2, X3))
     (active# U12(X1, X2, X3) -> active# X1, active# U21(tt(), M, N) -> U22#(tt(), M, N))
     (active# U12(X1, X2, X3) -> active# X1, active# x(N, s M) -> U21#(tt(), M, N))
     (active# U12(X1, X2, X3) -> active# X1, active# x(X1, X2) -> active# X1)
     (active# U12(X1, X2, X3) -> active# X1, active# x(X1, X2) -> active# X2)
     (active# U12(X1, X2, X3) -> active# X1, active# x(X1, X2) -> x#(X1, active X2))
     (active# U12(X1, X2, X3) -> active# X1, active# x(X1, X2) -> x#(active X1, X2))
     (proper# U22(X1, X2, X3) -> U22#(proper X1, proper X2, proper X3), U22#(mark X1, X2, X3) -> U22#(X1, X2, X3))
     (proper# U22(X1, X2, X3) -> U22#(proper X1, proper X2, proper X3), U22#(ok X1, ok X2, ok X3) -> U22#(X1, X2, X3))
     (proper# U12(X1, X2, X3) -> U12#(proper X1, proper X2, proper X3), U12#(mark X1, X2, X3) -> U12#(X1, X2, X3))
     (proper# U12(X1, X2, X3) -> U12#(proper X1, proper X2, proper X3), U12#(ok X1, ok X2, ok X3) -> U12#(X1, X2, X3))
     (top# mark X -> proper# X, proper# U12(X1, X2, X3) -> U12#(proper X1, proper X2, proper X3))
     (top# mark X -> proper# X, proper# U12(X1, X2, X3) -> proper# X1)
     (top# mark X -> proper# X, proper# U12(X1, X2, X3) -> proper# X2)
     (top# mark X -> proper# X, proper# U12(X1, X2, X3) -> proper# X3)
     (top# mark X -> proper# X, proper# U11(X1, X2, X3) -> U11#(proper X1, proper X2, proper X3))
     (top# mark X -> proper# X, proper# U11(X1, X2, X3) -> proper# X1)
     (top# mark X -> proper# X, proper# U11(X1, X2, X3) -> proper# X2)
     (top# mark X -> proper# X, proper# U11(X1, X2, X3) -> proper# X3)
     (top# mark X -> proper# X, proper# s X -> s# proper X)
     (top# mark X -> proper# X, proper# s X -> proper# X)
     (top# mark X -> proper# X, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (top# mark X -> proper# X, proper# plus(X1, X2) -> proper# X1)
     (top# mark X -> proper# X, proper# plus(X1, X2) -> proper# X2)
     (top# mark X -> proper# X, proper# U22(X1, X2, X3) -> U22#(proper X1, proper X2, proper X3))
     (top# mark X -> proper# X, proper# U22(X1, X2, X3) -> proper# X1)
     (top# mark X -> proper# X, proper# U22(X1, X2, X3) -> proper# X2)
     (top# mark X -> proper# X, proper# U22(X1, X2, X3) -> proper# X3)
     (top# mark X -> proper# X, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
     (top# mark X -> proper# X, proper# U21(X1, X2, X3) -> proper# X1)
     (top# mark X -> proper# X, proper# U21(X1, X2, X3) -> proper# X2)
     (top# mark X -> proper# X, proper# U21(X1, X2, X3) -> proper# X3)
     (top# mark X -> proper# X, proper# x(X1, X2) -> x#(proper X1, proper X2))
     (top# mark X -> proper# X, proper# x(X1, X2) -> proper# X1)
     (top# mark X -> proper# X, proper# x(X1, X2) -> proper# X2)
     (s# ok X -> s# X, s# mark X -> s# X)
     (s# ok X -> s# X, s# ok X -> s# X)
     (active# s X -> active# X, active# U12(X1, X2, X3) -> U12#(active X1, X2, X3))
     (active# s X -> active# X, active# U12(X1, X2, X3) -> active# X1)
     (active# s X -> active# X, active# U12(tt(), M, N) -> s# plus(N, M))
     (active# s X -> active# X, active# U12(tt(), M, N) -> plus#(N, M))
     (active# s X -> active# X, active# U11(X1, X2, X3) -> active# X1)
     (active# s X -> active# X, active# U11(X1, X2, X3) -> U11#(active X1, X2, X3))
     (active# s X -> active# X, active# U11(tt(), M, N) -> U12#(tt(), M, N))
     (active# s X -> active# X, active# s X -> active# X)
     (active# s X -> active# X, active# s X -> s# active X)
     (active# s X -> active# X, active# plus(N, s M) -> U11#(tt(), M, N))
     (active# s X -> active# X, active# plus(X1, X2) -> active# X1)
     (active# s X -> active# X, active# plus(X1, X2) -> active# X2)
     (active# s X -> active# X, active# plus(X1, X2) -> plus#(X1, active X2))
     (active# s X -> active# X, active# plus(X1, X2) -> plus#(active X1, X2))
     (active# s X -> active# X, active# U22(X1, X2, X3) -> active# X1)
     (active# s X -> active# X, active# U22(X1, X2, X3) -> U22#(active X1, X2, X3))
     (active# s X -> active# X, active# U22(tt(), M, N) -> plus#(x(N, M), N))
     (active# s X -> active# X, active# U22(tt(), M, N) -> x#(N, M))
     (active# s X -> active# X, active# U21(X1, X2, X3) -> active# X1)
     (active# s X -> active# X, active# U21(X1, X2, X3) -> U21#(active X1, X2, X3))
     (active# s X -> active# X, active# U21(tt(), M, N) -> U22#(tt(), M, N))
     (active# s X -> active# X, active# x(N, s M) -> U21#(tt(), M, N))
     (active# s X -> active# X, active# x(X1, X2) -> active# X1)
     (active# s X -> active# X, active# x(X1, X2) -> active# X2)
     (active# s X -> active# X, active# x(X1, X2) -> x#(X1, active X2))
     (active# s X -> active# X, active# x(X1, X2) -> x#(active X1, X2))
     (x#(ok X1, ok X2) -> x#(X1, X2), x#(X1, mark X2) -> x#(X1, X2))
     (x#(ok X1, ok X2) -> x#(X1, X2), x#(mark X1, X2) -> x#(X1, X2))
     (x#(ok X1, ok X2) -> x#(X1, X2), x#(ok X1, ok X2) -> x#(X1, X2))
     (x#(X1, mark X2) -> x#(X1, X2), x#(X1, mark X2) -> x#(X1, X2))
     (x#(X1, mark X2) -> x#(X1, X2), x#(mark X1, X2) -> x#(X1, X2))
     (x#(X1, mark X2) -> x#(X1, X2), x#(ok X1, ok X2) -> x#(X1, X2))
     (plus#(mark X1, X2) -> plus#(X1, X2), plus#(X1, mark X2) -> plus#(X1, X2))
     (plus#(mark X1, X2) -> plus#(X1, X2), plus#(mark X1, X2) -> plus#(X1, X2))
     (plus#(mark X1, X2) -> plus#(X1, X2), plus#(ok X1, ok X2) -> plus#(X1, X2))
     (top# ok X -> top# active X, top# mark X -> proper# X)
     (top# ok X -> top# active X, top# mark X -> top# proper X)
     (top# ok X -> top# active X, top# ok X -> active# X)
     (top# ok X -> top# active X, top# ok X -> top# active X)
     (proper# s X -> s# proper X, s# mark X -> s# X)
     (proper# s X -> s# proper X, s# ok X -> s# X)
     (active# x(X1, X2) -> x#(active X1, X2), x#(mark X1, X2) -> x#(X1, X2))
     (active# x(X1, X2) -> x#(active X1, X2), x#(ok X1, ok X2) -> x#(X1, X2))
     (proper# x(X1, X2) -> x#(proper X1, proper X2), x#(X1, mark X2) -> x#(X1, X2))
     (proper# x(X1, X2) -> x#(proper X1, proper X2), x#(mark X1, X2) -> x#(X1, X2))
     (proper# x(X1, X2) -> x#(proper X1, proper X2), x#(ok X1, ok X2) -> x#(X1, X2))
     (active# x(X1, X2) -> x#(X1, active X2), x#(X1, mark X2) -> x#(X1, X2))
     (active# x(X1, X2) -> x#(X1, active X2), x#(ok X1, ok X2) -> x#(X1, X2))
     (proper# U21(X1, X2, X3) -> proper# X3, proper# U12(X1, X2, X3) -> U12#(proper X1, proper X2, proper X3))
     (proper# U21(X1, X2, X3) -> proper# X3, proper# U12(X1, X2, X3) -> proper# X1)
     (proper# U21(X1, X2, X3) -> proper# X3, proper# U12(X1, X2, X3) -> proper# X2)
     (proper# U21(X1, X2, X3) -> proper# X3, proper# U12(X1, X2, X3) -> proper# X3)
     (proper# U21(X1, X2, X3) -> proper# X3, proper# U11(X1, X2, X3) -> U11#(proper X1, proper X2, proper X3))
     (proper# U21(X1, X2, X3) -> proper# X3, proper# U11(X1, X2, X3) -> proper# X1)
     (proper# U21(X1, X2, X3) -> proper# X3, proper# U11(X1, X2, X3) -> proper# X2)
     (proper# U21(X1, X2, X3) -> proper# X3, proper# U11(X1, X2, X3) -> proper# X3)
     (proper# U21(X1, X2, X3) -> proper# X3, proper# s X -> s# proper X)
     (proper# U21(X1, X2, X3) -> proper# X3, proper# s X -> proper# X)
     (proper# U21(X1, X2, X3) -> proper# X3, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# U21(X1, X2, X3) -> proper# X3, proper# plus(X1, X2) -> proper# X1)
     (proper# U21(X1, X2, X3) -> proper# X3, proper# plus(X1, X2) -> proper# X2)
     (proper# U21(X1, X2, X3) -> proper# X3, proper# U22(X1, X2, X3) -> U22#(proper X1, proper X2, proper X3))
     (proper# U21(X1, X2, X3) -> proper# X3, proper# U22(X1, X2, X3) -> proper# X1)
     (proper# U21(X1, X2, X3) -> proper# X3, proper# U22(X1, X2, X3) -> proper# X2)
     (proper# U21(X1, X2, X3) -> proper# X3, proper# U22(X1, X2, X3) -> proper# X3)
     (proper# U21(X1, X2, X3) -> proper# X3, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
     (proper# U21(X1, X2, X3) -> proper# X3, proper# U21(X1, X2, X3) -> proper# X1)
     (proper# U21(X1, X2, X3) -> proper# X3, proper# U21(X1, X2, X3) -> proper# X2)
     (proper# U21(X1, X2, X3) -> proper# X3, proper# U21(X1, X2, X3) -> proper# X3)
     (proper# U21(X1, X2, X3) -> proper# X3, proper# x(X1, X2) -> x#(proper X1, proper X2))
     (proper# U21(X1, X2, X3) -> proper# X3, proper# x(X1, X2) -> proper# X1)
     (proper# U21(X1, X2, X3) -> proper# X3, proper# x(X1, X2) -> proper# X2)
     (proper# U11(X1, X2, X3) -> proper# X3, proper# U12(X1, X2, X3) -> U12#(proper X1, proper X2, proper X3))
     (proper# U11(X1, X2, X3) -> proper# X3, proper# U12(X1, X2, X3) -> proper# X1)
     (proper# U11(X1, X2, X3) -> proper# X3, proper# U12(X1, X2, X3) -> proper# X2)
     (proper# U11(X1, X2, X3) -> proper# X3, proper# U12(X1, X2, X3) -> proper# X3)
     (proper# U11(X1, X2, X3) -> proper# X3, proper# U11(X1, X2, X3) -> U11#(proper X1, proper X2, proper X3))
     (proper# U11(X1, X2, X3) -> proper# X3, proper# U11(X1, X2, X3) -> proper# X1)
     (proper# U11(X1, X2, X3) -> proper# X3, proper# U11(X1, X2, X3) -> proper# X2)
     (proper# U11(X1, X2, X3) -> proper# X3, proper# U11(X1, X2, X3) -> proper# X3)
     (proper# U11(X1, X2, X3) -> proper# X3, proper# s X -> s# proper X)
     (proper# U11(X1, X2, X3) -> proper# X3, proper# s X -> proper# X)
     (proper# U11(X1, X2, X3) -> proper# X3, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# U11(X1, X2, X3) -> proper# X3, proper# plus(X1, X2) -> proper# X1)
     (proper# U11(X1, X2, X3) -> proper# X3, proper# plus(X1, X2) -> proper# X2)
     (proper# U11(X1, X2, X3) -> proper# X3, proper# U22(X1, X2, X3) -> U22#(proper X1, proper X2, proper X3))
     (proper# U11(X1, X2, X3) -> proper# X3, proper# U22(X1, X2, X3) -> proper# X1)
     (proper# U11(X1, X2, X3) -> proper# X3, proper# U22(X1, X2, X3) -> proper# X2)
     (proper# U11(X1, X2, X3) -> proper# X3, proper# U22(X1, X2, X3) -> proper# X3)
     (proper# U11(X1, X2, X3) -> proper# X3, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
     (proper# U11(X1, X2, X3) -> proper# X3, proper# U21(X1, X2, X3) -> proper# X1)
     (proper# U11(X1, X2, X3) -> proper# X3, proper# U21(X1, X2, X3) -> proper# X2)
     (proper# U11(X1, X2, X3) -> proper# X3, proper# U21(X1, X2, X3) -> proper# X3)
     (proper# U11(X1, X2, X3) -> proper# X3, proper# x(X1, X2) -> x#(proper X1, proper X2))
     (proper# U11(X1, X2, X3) -> proper# X3, proper# x(X1, X2) -> proper# X1)
     (proper# U11(X1, X2, X3) -> proper# X3, proper# x(X1, X2) -> proper# X2)
     (active# U22(tt(), M, N) -> x#(N, M), x#(X1, mark X2) -> x#(X1, X2))
     (active# U22(tt(), M, N) -> x#(N, M), x#(mark X1, X2) -> x#(X1, X2))
     (active# U22(tt(), M, N) -> x#(N, M), x#(ok X1, ok X2) -> x#(X1, X2))
     (U21#(ok X1, ok X2, ok X3) -> U21#(X1, X2, X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3))
     (U21#(ok X1, ok X2, ok X3) -> U21#(X1, X2, X3), U21#(ok X1, ok X2, ok X3) -> U21#(X1, X2, X3))
     (U22#(ok X1, ok X2, ok X3) -> U22#(X1, X2, X3), U22#(mark X1, X2, X3) -> U22#(X1, X2, X3))
     (U22#(ok X1, ok X2, ok X3) -> U22#(X1, X2, X3), U22#(ok X1, ok X2, ok X3) -> U22#(X1, X2, X3))
     (U11#(ok X1, ok X2, ok X3) -> U11#(X1, X2, X3), U11#(mark X1, X2, X3) -> U11#(X1, X2, X3))
     (U11#(ok X1, ok X2, ok X3) -> U11#(X1, X2, X3), U11#(ok X1, ok X2, ok X3) -> U11#(X1, X2, X3))
     (active# U21(X1, X2, X3) -> U21#(active X1, X2, X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3))
     (active# U21(X1, X2, X3) -> U21#(active X1, X2, X3), U21#(ok X1, ok X2, ok X3) -> U21#(X1, X2, X3))
     (active# U11(X1, X2, X3) -> U11#(active X1, X2, X3), U11#(mark X1, X2, X3) -> U11#(X1, X2, X3))
     (active# U11(X1, X2, X3) -> U11#(active X1, X2, X3), U11#(ok X1, ok X2, ok X3) -> U11#(X1, X2, X3))
     (U12#(ok X1, ok X2, ok X3) -> U12#(X1, X2, X3), U12#(mark X1, X2, X3) -> U12#(X1, X2, X3))
     (U12#(ok X1, ok X2, ok X3) -> U12#(X1, X2, X3), U12#(ok X1, ok X2, ok X3) -> U12#(X1, X2, X3))
     (active# U12(tt(), M, N) -> s# plus(N, M), s# mark X -> s# X)
     (active# U12(tt(), M, N) -> s# plus(N, M), s# ok X -> s# X)
     (proper# U21(X1, X2, X3) -> proper# X2, proper# U12(X1, X2, X3) -> U12#(proper X1, proper X2, proper X3))
     (proper# U21(X1, X2, X3) -> proper# X2, proper# U12(X1, X2, X3) -> proper# X1)
     (proper# U21(X1, X2, X3) -> proper# X2, proper# U12(X1, X2, X3) -> proper# X2)
     (proper# U21(X1, X2, X3) -> proper# X2, proper# U12(X1, X2, X3) -> proper# X3)
     (proper# U21(X1, X2, X3) -> proper# X2, proper# U11(X1, X2, X3) -> U11#(proper X1, proper X2, proper X3))
     (proper# U21(X1, X2, X3) -> proper# X2, proper# U11(X1, X2, X3) -> proper# X1)
     (proper# U21(X1, X2, X3) -> proper# X2, proper# U11(X1, X2, X3) -> proper# X2)
     (proper# U21(X1, X2, X3) -> proper# X2, proper# U11(X1, X2, X3) -> proper# X3)
     (proper# U21(X1, X2, X3) -> proper# X2, proper# s X -> s# proper X)
     (proper# U21(X1, X2, X3) -> proper# X2, proper# s X -> proper# X)
     (proper# U21(X1, X2, X3) -> proper# X2, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# U21(X1, X2, X3) -> proper# X2, proper# plus(X1, X2) -> proper# X1)
     (proper# U21(X1, X2, X3) -> proper# X2, proper# plus(X1, X2) -> proper# X2)
     (proper# U21(X1, X2, X3) -> proper# X2, proper# U22(X1, X2, X3) -> U22#(proper X1, proper X2, proper X3))
     (proper# U21(X1, X2, X3) -> proper# X2, proper# U22(X1, X2, X3) -> proper# X1)
     (proper# U21(X1, X2, X3) -> proper# X2, proper# U22(X1, X2, X3) -> proper# X2)
     (proper# U21(X1, X2, X3) -> proper# X2, proper# U22(X1, X2, X3) -> proper# X3)
     (proper# U21(X1, X2, X3) -> proper# X2, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
     (proper# U21(X1, X2, X3) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X1)
     (proper# U21(X1, X2, X3) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X2)
     (proper# U21(X1, X2, X3) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X3)
     (proper# U21(X1, X2, X3) -> proper# X2, proper# x(X1, X2) -> x#(proper X1, proper X2))
     (proper# U21(X1, X2, X3) -> proper# X2, proper# x(X1, X2) -> proper# X1)
     (proper# U21(X1, X2, X3) -> proper# X2, proper# x(X1, X2) -> proper# X2)
     (proper# plus(X1, X2) -> proper# X2, proper# U12(X1, X2, X3) -> U12#(proper X1, proper X2, proper X3))
     (proper# plus(X1, X2) -> proper# X2, proper# U12(X1, X2, X3) -> proper# X1)
     (proper# plus(X1, X2) -> proper# X2, proper# U12(X1, X2, X3) -> proper# X2)
     (proper# plus(X1, X2) -> proper# X2, proper# U12(X1, X2, X3) -> proper# X3)
     (proper# plus(X1, X2) -> proper# X2, proper# U11(X1, X2, X3) -> U11#(proper X1, proper X2, proper X3))
     (proper# plus(X1, X2) -> proper# X2, proper# U11(X1, X2, X3) -> proper# X1)
     (proper# plus(X1, X2) -> proper# X2, proper# U11(X1, X2, X3) -> proper# X2)
     (proper# plus(X1, X2) -> proper# X2, proper# U11(X1, X2, X3) -> proper# X3)
     (proper# plus(X1, X2) -> proper# X2, proper# s X -> s# proper X)
     (proper# plus(X1, X2) -> proper# X2, proper# s X -> proper# X)
     (proper# plus(X1, X2) -> proper# X2, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# plus(X1, X2) -> proper# X2, proper# plus(X1, X2) -> proper# X1)
     (proper# plus(X1, X2) -> proper# X2, proper# plus(X1, X2) -> proper# X2)
     (proper# plus(X1, X2) -> proper# X2, proper# U22(X1, X2, X3) -> U22#(proper X1, proper X2, proper X3))
     (proper# plus(X1, X2) -> proper# X2, proper# U22(X1, X2, X3) -> proper# X1)
     (proper# plus(X1, X2) -> proper# X2, proper# U22(X1, X2, X3) -> proper# X2)
     (proper# plus(X1, X2) -> proper# X2, proper# U22(X1, X2, X3) -> proper# X3)
     (proper# plus(X1, X2) -> proper# X2, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
     (proper# plus(X1, X2) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X1)
     (proper# plus(X1, X2) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X2)
     (proper# plus(X1, X2) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X3)
     (proper# plus(X1, X2) -> proper# X2, proper# x(X1, X2) -> x#(proper X1, proper X2))
     (proper# plus(X1, X2) -> proper# X2, proper# x(X1, X2) -> proper# X1)
     (proper# plus(X1, X2) -> proper# X2, proper# x(X1, X2) -> proper# X2)
     (proper# U12(X1, X2, X3) -> proper# X2, proper# U12(X1, X2, X3) -> U12#(proper X1, proper X2, proper X3))
     (proper# U12(X1, X2, X3) -> proper# X2, proper# U12(X1, X2, X3) -> proper# X1)
     (proper# U12(X1, X2, X3) -> proper# X2, proper# U12(X1, X2, X3) -> proper# X2)
     (proper# U12(X1, X2, X3) -> proper# X2, proper# U12(X1, X2, X3) -> proper# X3)
     (proper# U12(X1, X2, X3) -> proper# X2, proper# U11(X1, X2, X3) -> U11#(proper X1, proper X2, proper X3))
     (proper# U12(X1, X2, X3) -> proper# X2, proper# U11(X1, X2, X3) -> proper# X1)
     (proper# U12(X1, X2, X3) -> proper# X2, proper# U11(X1, X2, X3) -> proper# X2)
     (proper# U12(X1, X2, X3) -> proper# X2, proper# U11(X1, X2, X3) -> proper# X3)
     (proper# U12(X1, X2, X3) -> proper# X2, proper# s X -> s# proper X)
     (proper# U12(X1, X2, X3) -> proper# X2, proper# s X -> proper# X)
     (proper# U12(X1, X2, X3) -> proper# X2, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# U12(X1, X2, X3) -> proper# X2, proper# plus(X1, X2) -> proper# X1)
     (proper# U12(X1, X2, X3) -> proper# X2, proper# plus(X1, X2) -> proper# X2)
     (proper# U12(X1, X2, X3) -> proper# X2, proper# U22(X1, X2, X3) -> U22#(proper X1, proper X2, proper X3))
     (proper# U12(X1, X2, X3) -> proper# X2, proper# U22(X1, X2, X3) -> proper# X1)
     (proper# U12(X1, X2, X3) -> proper# X2, proper# U22(X1, X2, X3) -> proper# X2)
     (proper# U12(X1, X2, X3) -> proper# X2, proper# U22(X1, X2, X3) -> proper# X3)
     (proper# U12(X1, X2, X3) -> proper# X2, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
     (proper# U12(X1, X2, X3) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X1)
     (proper# U12(X1, X2, X3) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X2)
     (proper# U12(X1, X2, X3) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X3)
     (proper# U12(X1, X2, X3) -> proper# X2, proper# x(X1, X2) -> x#(proper X1, proper X2))
     (proper# U12(X1, X2, X3) -> proper# X2, proper# x(X1, X2) -> proper# X1)
     (proper# U12(X1, X2, X3) -> proper# X2, proper# x(X1, X2) -> proper# X2)
     (active# plus(X1, X2) -> active# X2, active# U12(X1, X2, X3) -> U12#(active X1, X2, X3))
     (active# plus(X1, X2) -> active# X2, active# U12(X1, X2, X3) -> active# X1)
     (active# plus(X1, X2) -> active# X2, active# U12(tt(), M, N) -> s# plus(N, M))
     (active# plus(X1, X2) -> active# X2, active# U12(tt(), M, N) -> plus#(N, M))
     (active# plus(X1, X2) -> active# X2, active# U11(X1, X2, X3) -> active# X1)
     (active# plus(X1, X2) -> active# X2, active# U11(X1, X2, X3) -> U11#(active X1, X2, X3))
     (active# plus(X1, X2) -> active# X2, active# U11(tt(), M, N) -> U12#(tt(), M, N))
     (active# plus(X1, X2) -> active# X2, active# s X -> active# X)
     (active# plus(X1, X2) -> active# X2, active# s X -> s# active X)
     (active# plus(X1, X2) -> active# X2, active# plus(N, s M) -> U11#(tt(), M, N))
     (active# plus(X1, X2) -> active# X2, active# plus(X1, X2) -> active# X1)
     (active# plus(X1, X2) -> active# X2, active# plus(X1, X2) -> active# X2)
     (active# plus(X1, X2) -> active# X2, active# plus(X1, X2) -> plus#(X1, active X2))
     (active# plus(X1, X2) -> active# X2, active# plus(X1, X2) -> plus#(active X1, X2))
     (active# plus(X1, X2) -> active# X2, active# U22(X1, X2, X3) -> active# X1)
     (active# plus(X1, X2) -> active# X2, active# U22(X1, X2, X3) -> U22#(active X1, X2, X3))
     (active# plus(X1, X2) -> active# X2, active# U22(tt(), M, N) -> plus#(x(N, M), N))
     (active# plus(X1, X2) -> active# X2, active# U22(tt(), M, N) -> x#(N, M))
     (active# plus(X1, X2) -> active# X2, active# U21(X1, X2, X3) -> active# X1)
     (active# plus(X1, X2) -> active# X2, active# U21(X1, X2, X3) -> U21#(active X1, X2, X3))
     (active# plus(X1, X2) -> active# X2, active# U21(tt(), M, N) -> U22#(tt(), M, N))
     (active# plus(X1, X2) -> active# X2, active# x(N, s M) -> U21#(tt(), M, N))
     (active# plus(X1, X2) -> active# X2, active# x(X1, X2) -> active# X1)
     (active# plus(X1, X2) -> active# X2, active# x(X1, X2) -> active# X2)
     (active# plus(X1, X2) -> active# X2, active# x(X1, X2) -> x#(X1, active X2))
     (active# plus(X1, X2) -> active# X2, active# x(X1, X2) -> x#(active X1, X2))
    }
    STATUS:
     arrows: 0.840204
     SCCS (10):
      Scc:
       {top# mark X -> top# proper X,
          top# ok X -> top# active X}
      Scc:
       {proper# U12(X1, X2, X3) -> proper# X1,
        proper# U12(X1, X2, X3) -> proper# X2,
        proper# U12(X1, X2, X3) -> proper# X3,
        proper# U11(X1, X2, X3) -> proper# X1,
        proper# U11(X1, X2, X3) -> proper# X2,
        proper# U11(X1, X2, X3) -> proper# X3,
                    proper# s X -> proper# X,
           proper# plus(X1, X2) -> proper# X1,
           proper# plus(X1, X2) -> proper# X2,
        proper# U22(X1, X2, X3) -> proper# X1,
        proper# U22(X1, X2, X3) -> proper# X2,
        proper# U22(X1, X2, X3) -> proper# X3,
        proper# U21(X1, X2, X3) -> proper# X1,
        proper# U21(X1, X2, X3) -> proper# X2,
        proper# U21(X1, X2, X3) -> proper# X3,
              proper# x(X1, X2) -> proper# X1,
              proper# x(X1, X2) -> proper# X2}
      Scc:
       {active# U12(X1, X2, X3) -> active# X1,
        active# U11(X1, X2, X3) -> active# X1,
                    active# s X -> active# X,
           active# plus(X1, X2) -> active# X1,
           active# plus(X1, X2) -> active# X2,
        active# U22(X1, X2, X3) -> active# X1,
        active# U21(X1, X2, X3) -> active# X1,
              active# x(X1, X2) -> active# X1,
              active# x(X1, X2) -> active# X2}
      Scc:
       {    U21#(mark X1, X2, X3) -> U21#(X1, X2, X3),
        U21#(ok X1, ok X2, ok X3) -> U21#(X1, X2, X3)}
      Scc:
       { x#(X1, mark X2) -> x#(X1, X2),
         x#(mark X1, X2) -> x#(X1, X2),
        x#(ok X1, ok X2) -> x#(X1, X2)}
      Scc:
       {    U22#(mark X1, X2, X3) -> U22#(X1, X2, X3),
        U22#(ok X1, ok X2, ok X3) -> U22#(X1, X2, X3)}
      Scc:
       {    U11#(mark X1, X2, X3) -> U11#(X1, X2, X3),
        U11#(ok X1, ok X2, ok X3) -> U11#(X1, X2, X3)}
      Scc:
       { plus#(X1, mark X2) -> plus#(X1, X2),
         plus#(mark X1, X2) -> plus#(X1, X2),
        plus#(ok X1, ok X2) -> plus#(X1, X2)}
      Scc:
       {s# mark X -> s# X,
          s# ok X -> s# X}
      Scc:
       {    U12#(mark X1, X2, X3) -> U12#(X1, X2, X3),
        U12#(ok X1, ok X2, ok X3) -> U12#(X1, X2, X3)}
      
      SCC (2):
       Strict:
        {top# mark X -> top# proper X,
           top# ok X -> top# active X}
       Weak:
       {    U12(mark X1, X2, X3) -> mark U12(X1, X2, X3),
        U12(ok X1, ok X2, ok X3) -> ok U12(X1, X2, X3),
          active U12(X1, X2, X3) -> U12(active X1, X2, X3),
          active U12(tt(), M, N) -> mark s plus(N, M),
          active U11(X1, X2, X3) -> U11(active X1, X2, X3),
          active U11(tt(), M, N) -> mark U12(tt(), M, N),
                      active s X -> s active X,
             active plus(N, s M) -> mark U11(tt(), M, N),
             active plus(N, 0()) -> mark N,
             active plus(X1, X2) -> plus(X1, active X2),
             active plus(X1, X2) -> plus(active X1, X2),
          active U22(X1, X2, X3) -> U22(active X1, X2, X3),
          active U22(tt(), M, N) -> mark plus(x(N, M), N),
          active U21(X1, X2, X3) -> U21(active X1, X2, X3),
          active U21(tt(), M, N) -> mark U22(tt(), M, N),
                active x(N, s M) -> mark U21(tt(), M, N),
                active x(N, 0()) -> mark 0(),
                active x(X1, X2) -> x(X1, active X2),
                active x(X1, X2) -> x(active X1, X2),
            U11(mark X1, X2, X3) -> mark U11(X1, X2, X3),
        U11(ok X1, ok X2, ok X3) -> ok U11(X1, X2, X3),
                        s mark X -> mark s X,
                          s ok X -> ok s X,
               plus(X1, mark X2) -> mark plus(X1, X2),
               plus(mark X1, X2) -> mark plus(X1, X2),
              plus(ok X1, ok X2) -> ok plus(X1, X2),
            U22(mark X1, X2, X3) -> mark U22(X1, X2, X3),
        U22(ok X1, ok X2, ok X3) -> ok U22(X1, X2, X3),
            U21(mark X1, X2, X3) -> mark U21(X1, X2, X3),
        U21(ok X1, ok X2, ok X3) -> ok U21(X1, X2, X3),
                  x(X1, mark X2) -> mark x(X1, X2),
                  x(mark X1, X2) -> mark x(X1, X2),
                 x(ok X1, ok X2) -> ok x(X1, X2),
          proper U12(X1, X2, X3) -> U12(proper X1, proper X2, proper X3),
                     proper tt() -> ok tt(),
          proper U11(X1, X2, X3) -> U11(proper X1, proper X2, proper X3),
                      proper s X -> s proper X,
             proper plus(X1, X2) -> plus(proper X1, proper X2),
          proper U22(X1, X2, X3) -> U22(proper X1, proper X2, proper X3),
          proper U21(X1, X2, X3) -> U21(proper X1, proper X2, proper X3),
                proper x(X1, X2) -> x(proper X1, proper X2),
                      proper 0() -> ok 0(),
                      top mark X -> top proper X,
                        top ok X -> top active X}
       Open
      
      
      SCC (17):
       Strict:
        {proper# U12(X1, X2, X3) -> proper# X1,
         proper# U12(X1, X2, X3) -> proper# X2,
         proper# U12(X1, X2, X3) -> proper# X3,
         proper# U11(X1, X2, X3) -> proper# X1,
         proper# U11(X1, X2, X3) -> proper# X2,
         proper# U11(X1, X2, X3) -> proper# X3,
                     proper# s X -> proper# X,
            proper# plus(X1, X2) -> proper# X1,
            proper# plus(X1, X2) -> proper# X2,
         proper# U22(X1, X2, X3) -> proper# X1,
         proper# U22(X1, X2, X3) -> proper# X2,
         proper# U22(X1, X2, X3) -> proper# X3,
         proper# U21(X1, X2, X3) -> proper# X1,
         proper# U21(X1, X2, X3) -> proper# X2,
         proper# U21(X1, X2, X3) -> proper# X3,
               proper# x(X1, X2) -> proper# X1,
               proper# x(X1, X2) -> proper# X2}
       Weak:
       {    U12(mark X1, X2, X3) -> mark U12(X1, X2, X3),
        U12(ok X1, ok X2, ok X3) -> ok U12(X1, X2, X3),
          active U12(X1, X2, X3) -> U12(active X1, X2, X3),
          active U12(tt(), M, N) -> mark s plus(N, M),
          active U11(X1, X2, X3) -> U11(active X1, X2, X3),
          active U11(tt(), M, N) -> mark U12(tt(), M, N),
                      active s X -> s active X,
             active plus(N, s M) -> mark U11(tt(), M, N),
             active plus(N, 0()) -> mark N,
             active plus(X1, X2) -> plus(X1, active X2),
             active plus(X1, X2) -> plus(active X1, X2),
          active U22(X1, X2, X3) -> U22(active X1, X2, X3),
          active U22(tt(), M, N) -> mark plus(x(N, M), N),
          active U21(X1, X2, X3) -> U21(active X1, X2, X3),
          active U21(tt(), M, N) -> mark U22(tt(), M, N),
                active x(N, s M) -> mark U21(tt(), M, N),
                active x(N, 0()) -> mark 0(),
                active x(X1, X2) -> x(X1, active X2),
                active x(X1, X2) -> x(active X1, X2),
            U11(mark X1, X2, X3) -> mark U11(X1, X2, X3),
        U11(ok X1, ok X2, ok X3) -> ok U11(X1, X2, X3),
                        s mark X -> mark s X,
                          s ok X -> ok s X,
               plus(X1, mark X2) -> mark plus(X1, X2),
               plus(mark X1, X2) -> mark plus(X1, X2),
              plus(ok X1, ok X2) -> ok plus(X1, X2),
            U22(mark X1, X2, X3) -> mark U22(X1, X2, X3),
        U22(ok X1, ok X2, ok X3) -> ok U22(X1, X2, X3),
            U21(mark X1, X2, X3) -> mark U21(X1, X2, X3),
        U21(ok X1, ok X2, ok X3) -> ok U21(X1, X2, X3),
                  x(X1, mark X2) -> mark x(X1, X2),
                  x(mark X1, X2) -> mark x(X1, X2),
                 x(ok X1, ok X2) -> ok x(X1, X2),
          proper U12(X1, X2, X3) -> U12(proper X1, proper X2, proper X3),
                     proper tt() -> ok tt(),
          proper U11(X1, X2, X3) -> U11(proper X1, proper X2, proper X3),
                      proper s X -> s proper X,
             proper plus(X1, X2) -> plus(proper X1, proper X2),
          proper U22(X1, X2, X3) -> U22(proper X1, proper X2, proper X3),
          proper U21(X1, X2, X3) -> U21(proper X1, proper X2, proper X3),
                proper x(X1, X2) -> x(proper X1, proper X2),
                      proper 0() -> ok 0(),
                      top mark X -> top proper X,
                        top ok X -> top active X}
       Open
      
      
      
      
      
      
      
      SCC (9):
       Strict:
        {active# U12(X1, X2, X3) -> active# X1,
         active# U11(X1, X2, X3) -> active# X1,
                     active# s X -> active# X,
            active# plus(X1, X2) -> active# X1,
            active# plus(X1, X2) -> active# X2,
         active# U22(X1, X2, X3) -> active# X1,
         active# U21(X1, X2, X3) -> active# X1,
               active# x(X1, X2) -> active# X1,
               active# x(X1, X2) -> active# X2}
       Weak:
       {    U12(mark X1, X2, X3) -> mark U12(X1, X2, X3),
        U12(ok X1, ok X2, ok X3) -> ok U12(X1, X2, X3),
          active U12(X1, X2, X3) -> U12(active X1, X2, X3),
          active U12(tt(), M, N) -> mark s plus(N, M),
          active U11(X1, X2, X3) -> U11(active X1, X2, X3),
          active U11(tt(), M, N) -> mark U12(tt(), M, N),
                      active s X -> s active X,
             active plus(N, s M) -> mark U11(tt(), M, N),
             active plus(N, 0()) -> mark N,
             active plus(X1, X2) -> plus(X1, active X2),
             active plus(X1, X2) -> plus(active X1, X2),
          active U22(X1, X2, X3) -> U22(active X1, X2, X3),
          active U22(tt(), M, N) -> mark plus(x(N, M), N),
          active U21(X1, X2, X3) -> U21(active X1, X2, X3),
          active U21(tt(), M, N) -> mark U22(tt(), M, N),
                active x(N, s M) -> mark U21(tt(), M, N),
                active x(N, 0()) -> mark 0(),
                active x(X1, X2) -> x(X1, active X2),
                active x(X1, X2) -> x(active X1, X2),
            U11(mark X1, X2, X3) -> mark U11(X1, X2, X3),
        U11(ok X1, ok X2, ok X3) -> ok U11(X1, X2, X3),
                        s mark X -> mark s X,
                          s ok X -> ok s X,
               plus(X1, mark X2) -> mark plus(X1, X2),
               plus(mark X1, X2) -> mark plus(X1, X2),
              plus(ok X1, ok X2) -> ok plus(X1, X2),
            U22(mark X1, X2, X3) -> mark U22(X1, X2, X3),
        U22(ok X1, ok X2, ok X3) -> ok U22(X1, X2, X3),
            U21(mark X1, X2, X3) -> mark U21(X1, X2, X3),
        U21(ok X1, ok X2, ok X3) -> ok U21(X1, X2, X3),
                  x(X1, mark X2) -> mark x(X1, X2),
                  x(mark X1, X2) -> mark x(X1, X2),
                 x(ok X1, ok X2) -> ok x(X1, X2),
          proper U12(X1, X2, X3) -> U12(proper X1, proper X2, proper X3),
                     proper tt() -> ok tt(),
          proper U11(X1, X2, X3) -> U11(proper X1, proper X2, proper X3),
                      proper s X -> s proper X,
             proper plus(X1, X2) -> plus(proper X1, proper X2),
          proper U22(X1, X2, X3) -> U22(proper X1, proper X2, proper X3),
          proper U21(X1, X2, X3) -> U21(proper X1, proper X2, proper X3),
                proper x(X1, X2) -> x(proper X1, proper X2),
                      proper 0() -> ok 0(),
                      top mark X -> top proper X,
                        top ok X -> top active X}
       Open
      
      
      
      
      
      SCC (2):
       Strict:
        {    U21#(mark X1, X2, X3) -> U21#(X1, X2, X3),
         U21#(ok X1, ok X2, ok X3) -> U21#(X1, X2, X3)}
       Weak:
       {    U12(mark X1, X2, X3) -> mark U12(X1, X2, X3),
        U12(ok X1, ok X2, ok X3) -> ok U12(X1, X2, X3),
          active U12(X1, X2, X3) -> U12(active X1, X2, X3),
          active U12(tt(), M, N) -> mark s plus(N, M),
          active U11(X1, X2, X3) -> U11(active X1, X2, X3),
          active U11(tt(), M, N) -> mark U12(tt(), M, N),
                      active s X -> s active X,
             active plus(N, s M) -> mark U11(tt(), M, N),
             active plus(N, 0()) -> mark N,
             active plus(X1, X2) -> plus(X1, active X2),
             active plus(X1, X2) -> plus(active X1, X2),
          active U22(X1, X2, X3) -> U22(active X1, X2, X3),
          active U22(tt(), M, N) -> mark plus(x(N, M), N),
          active U21(X1, X2, X3) -> U21(active X1, X2, X3),
          active U21(tt(), M, N) -> mark U22(tt(), M, N),
                active x(N, s M) -> mark U21(tt(), M, N),
                active x(N, 0()) -> mark 0(),
                active x(X1, X2) -> x(X1, active X2),
                active x(X1, X2) -> x(active X1, X2),
            U11(mark X1, X2, X3) -> mark U11(X1, X2, X3),
        U11(ok X1, ok X2, ok X3) -> ok U11(X1, X2, X3),
                        s mark X -> mark s X,
                          s ok X -> ok s X,
               plus(X1, mark X2) -> mark plus(X1, X2),
               plus(mark X1, X2) -> mark plus(X1, X2),
              plus(ok X1, ok X2) -> ok plus(X1, X2),
            U22(mark X1, X2, X3) -> mark U22(X1, X2, X3),
        U22(ok X1, ok X2, ok X3) -> ok U22(X1, X2, X3),
            U21(mark X1, X2, X3) -> mark U21(X1, X2, X3),
        U21(ok X1, ok X2, ok X3) -> ok U21(X1, X2, X3),
                  x(X1, mark X2) -> mark x(X1, X2),
                  x(mark X1, X2) -> mark x(X1, X2),
                 x(ok X1, ok X2) -> ok x(X1, X2),
          proper U12(X1, X2, X3) -> U12(proper X1, proper X2, proper X3),
                     proper tt() -> ok tt(),
          proper U11(X1, X2, X3) -> U11(proper X1, proper X2, proper X3),
                      proper s X -> s proper X,
             proper plus(X1, X2) -> plus(proper X1, proper X2),
          proper U22(X1, X2, X3) -> U22(proper X1, proper X2, proper X3),
          proper U21(X1, X2, X3) -> U21(proper X1, proper X2, proper X3),
                proper x(X1, X2) -> x(proper X1, proper X2),
                      proper 0() -> ok 0(),
                      top mark X -> top proper X,
                        top ok X -> top active X}
       Open
      
      SCC (3):
       Strict:
        { x#(X1, mark X2) -> x#(X1, X2),
          x#(mark X1, X2) -> x#(X1, X2),
         x#(ok X1, ok X2) -> x#(X1, X2)}
       Weak:
       {    U12(mark X1, X2, X3) -> mark U12(X1, X2, X3),
        U12(ok X1, ok X2, ok X3) -> ok U12(X1, X2, X3),
          active U12(X1, X2, X3) -> U12(active X1, X2, X3),
          active U12(tt(), M, N) -> mark s plus(N, M),
          active U11(X1, X2, X3) -> U11(active X1, X2, X3),
          active U11(tt(), M, N) -> mark U12(tt(), M, N),
                      active s X -> s active X,
             active plus(N, s M) -> mark U11(tt(), M, N),
             active plus(N, 0()) -> mark N,
             active plus(X1, X2) -> plus(X1, active X2),
             active plus(X1, X2) -> plus(active X1, X2),
          active U22(X1, X2, X3) -> U22(active X1, X2, X3),
          active U22(tt(), M, N) -> mark plus(x(N, M), N),
          active U21(X1, X2, X3) -> U21(active X1, X2, X3),
          active U21(tt(), M, N) -> mark U22(tt(), M, N),
                active x(N, s M) -> mark U21(tt(), M, N),
                active x(N, 0()) -> mark 0(),
                active x(X1, X2) -> x(X1, active X2),
                active x(X1, X2) -> x(active X1, X2),
            U11(mark X1, X2, X3) -> mark U11(X1, X2, X3),
        U11(ok X1, ok X2, ok X3) -> ok U11(X1, X2, X3),
                        s mark X -> mark s X,
                          s ok X -> ok s X,
               plus(X1, mark X2) -> mark plus(X1, X2),
               plus(mark X1, X2) -> mark plus(X1, X2),
              plus(ok X1, ok X2) -> ok plus(X1, X2),
            U22(mark X1, X2, X3) -> mark U22(X1, X2, X3),
        U22(ok X1, ok X2, ok X3) -> ok U22(X1, X2, X3),
            U21(mark X1, X2, X3) -> mark U21(X1, X2, X3),
        U21(ok X1, ok X2, ok X3) -> ok U21(X1, X2, X3),
                  x(X1, mark X2) -> mark x(X1, X2),
                  x(mark X1, X2) -> mark x(X1, X2),
                 x(ok X1, ok X2) -> ok x(X1, X2),
          proper U12(X1, X2, X3) -> U12(proper X1, proper X2, proper X3),
                     proper tt() -> ok tt(),
          proper U11(X1, X2, X3) -> U11(proper X1, proper X2, proper X3),
                      proper s X -> s proper X,
             proper plus(X1, X2) -> plus(proper X1, proper X2),
          proper U22(X1, X2, X3) -> U22(proper X1, proper X2, proper X3),
          proper U21(X1, X2, X3) -> U21(proper X1, proper X2, proper X3),
                proper x(X1, X2) -> x(proper X1, proper X2),
                      proper 0() -> ok 0(),
                      top mark X -> top proper X,
                        top ok X -> top active X}
       Open
      
      
      SCC (2):
       Strict:
        {    U22#(mark X1, X2, X3) -> U22#(X1, X2, X3),
         U22#(ok X1, ok X2, ok X3) -> U22#(X1, X2, X3)}
       Weak:
       {    U12(mark X1, X2, X3) -> mark U12(X1, X2, X3),
        U12(ok X1, ok X2, ok X3) -> ok U12(X1, X2, X3),
          active U12(X1, X2, X3) -> U12(active X1, X2, X3),
          active U12(tt(), M, N) -> mark s plus(N, M),
          active U11(X1, X2, X3) -> U11(active X1, X2, X3),
          active U11(tt(), M, N) -> mark U12(tt(), M, N),
                      active s X -> s active X,
             active plus(N, s M) -> mark U11(tt(), M, N),
             active plus(N, 0()) -> mark N,
             active plus(X1, X2) -> plus(X1, active X2),
             active plus(X1, X2) -> plus(active X1, X2),
          active U22(X1, X2, X3) -> U22(active X1, X2, X3),
          active U22(tt(), M, N) -> mark plus(x(N, M), N),
          active U21(X1, X2, X3) -> U21(active X1, X2, X3),
          active U21(tt(), M, N) -> mark U22(tt(), M, N),
                active x(N, s M) -> mark U21(tt(), M, N),
                active x(N, 0()) -> mark 0(),
                active x(X1, X2) -> x(X1, active X2),
                active x(X1, X2) -> x(active X1, X2),
            U11(mark X1, X2, X3) -> mark U11(X1, X2, X3),
        U11(ok X1, ok X2, ok X3) -> ok U11(X1, X2, X3),
                        s mark X -> mark s X,
                          s ok X -> ok s X,
               plus(X1, mark X2) -> mark plus(X1, X2),
               plus(mark X1, X2) -> mark plus(X1, X2),
              plus(ok X1, ok X2) -> ok plus(X1, X2),
            U22(mark X1, X2, X3) -> mark U22(X1, X2, X3),
        U22(ok X1, ok X2, ok X3) -> ok U22(X1, X2, X3),
            U21(mark X1, X2, X3) -> mark U21(X1, X2, X3),
        U21(ok X1, ok X2, ok X3) -> ok U21(X1, X2, X3),
                  x(X1, mark X2) -> mark x(X1, X2),
                  x(mark X1, X2) -> mark x(X1, X2),
                 x(ok X1, ok X2) -> ok x(X1, X2),
          proper U12(X1, X2, X3) -> U12(proper X1, proper X2, proper X3),
                     proper tt() -> ok tt(),
          proper U11(X1, X2, X3) -> U11(proper X1, proper X2, proper X3),
                      proper s X -> s proper X,
             proper plus(X1, X2) -> plus(proper X1, proper X2),
          proper U22(X1, X2, X3) -> U22(proper X1, proper X2, proper X3),
          proper U21(X1, X2, X3) -> U21(proper X1, proper X2, proper X3),
                proper x(X1, X2) -> x(proper X1, proper X2),
                      proper 0() -> ok 0(),
                      top mark X -> top proper X,
                        top ok X -> top active X}
       Open
      
      
      
      
      
      
      SCC (2):
       Strict:
        {    U11#(mark X1, X2, X3) -> U11#(X1, X2, X3),
         U11#(ok X1, ok X2, ok X3) -> U11#(X1, X2, X3)}
       Weak:
       {    U12(mark X1, X2, X3) -> mark U12(X1, X2, X3),
        U12(ok X1, ok X2, ok X3) -> ok U12(X1, X2, X3),
          active U12(X1, X2, X3) -> U12(active X1, X2, X3),
          active U12(tt(), M, N) -> mark s plus(N, M),
          active U11(X1, X2, X3) -> U11(active X1, X2, X3),
          active U11(tt(), M, N) -> mark U12(tt(), M, N),
                      active s X -> s active X,
             active plus(N, s M) -> mark U11(tt(), M, N),
             active plus(N, 0()) -> mark N,
             active plus(X1, X2) -> plus(X1, active X2),
             active plus(X1, X2) -> plus(active X1, X2),
          active U22(X1, X2, X3) -> U22(active X1, X2, X3),
          active U22(tt(), M, N) -> mark plus(x(N, M), N),
          active U21(X1, X2, X3) -> U21(active X1, X2, X3),
          active U21(tt(), M, N) -> mark U22(tt(), M, N),
                active x(N, s M) -> mark U21(tt(), M, N),
                active x(N, 0()) -> mark 0(),
                active x(X1, X2) -> x(X1, active X2),
                active x(X1, X2) -> x(active X1, X2),
            U11(mark X1, X2, X3) -> mark U11(X1, X2, X3),
        U11(ok X1, ok X2, ok X3) -> ok U11(X1, X2, X3),
                        s mark X -> mark s X,
                          s ok X -> ok s X,
               plus(X1, mark X2) -> mark plus(X1, X2),
               plus(mark X1, X2) -> mark plus(X1, X2),
              plus(ok X1, ok X2) -> ok plus(X1, X2),
            U22(mark X1, X2, X3) -> mark U22(X1, X2, X3),
        U22(ok X1, ok X2, ok X3) -> ok U22(X1, X2, X3),
            U21(mark X1, X2, X3) -> mark U21(X1, X2, X3),
        U21(ok X1, ok X2, ok X3) -> ok U21(X1, X2, X3),
                  x(X1, mark X2) -> mark x(X1, X2),
                  x(mark X1, X2) -> mark x(X1, X2),
                 x(ok X1, ok X2) -> ok x(X1, X2),
          proper U12(X1, X2, X3) -> U12(proper X1, proper X2, proper X3),
                     proper tt() -> ok tt(),
          proper U11(X1, X2, X3) -> U11(proper X1, proper X2, proper X3),
                      proper s X -> s proper X,
             proper plus(X1, X2) -> plus(proper X1, proper X2),
          proper U22(X1, X2, X3) -> U22(proper X1, proper X2, proper X3),
          proper U21(X1, X2, X3) -> U21(proper X1, proper X2, proper X3),
                proper x(X1, X2) -> x(proper X1, proper X2),
                      proper 0() -> ok 0(),
                      top mark X -> top proper X,
                        top ok X -> top active X}
       Open
      
      SCC (3):
       Strict:
        { plus#(X1, mark X2) -> plus#(X1, X2),
          plus#(mark X1, X2) -> plus#(X1, X2),
         plus#(ok X1, ok X2) -> plus#(X1, X2)}
       Weak:
       {    U12(mark X1, X2, X3) -> mark U12(X1, X2, X3),
        U12(ok X1, ok X2, ok X3) -> ok U12(X1, X2, X3),
          active U12(X1, X2, X3) -> U12(active X1, X2, X3),
          active U12(tt(), M, N) -> mark s plus(N, M),
          active U11(X1, X2, X3) -> U11(active X1, X2, X3),
          active U11(tt(), M, N) -> mark U12(tt(), M, N),
                      active s X -> s active X,
             active plus(N, s M) -> mark U11(tt(), M, N),
             active plus(N, 0()) -> mark N,
             active plus(X1, X2) -> plus(X1, active X2),
             active plus(X1, X2) -> plus(active X1, X2),
          active U22(X1, X2, X3) -> U22(active X1, X2, X3),
          active U22(tt(), M, N) -> mark plus(x(N, M), N),
          active U21(X1, X2, X3) -> U21(active X1, X2, X3),
          active U21(tt(), M, N) -> mark U22(tt(), M, N),
                active x(N, s M) -> mark U21(tt(), M, N),
                active x(N, 0()) -> mark 0(),
                active x(X1, X2) -> x(X1, active X2),
                active x(X1, X2) -> x(active X1, X2),
            U11(mark X1, X2, X3) -> mark U11(X1, X2, X3),
        U11(ok X1, ok X2, ok X3) -> ok U11(X1, X2, X3),
                        s mark X -> mark s X,
                          s ok X -> ok s X,
               plus(X1, mark X2) -> mark plus(X1, X2),
               plus(mark X1, X2) -> mark plus(X1, X2),
              plus(ok X1, ok X2) -> ok plus(X1, X2),
            U22(mark X1, X2, X3) -> mark U22(X1, X2, X3),
        U22(ok X1, ok X2, ok X3) -> ok U22(X1, X2, X3),
            U21(mark X1, X2, X3) -> mark U21(X1, X2, X3),
        U21(ok X1, ok X2, ok X3) -> ok U21(X1, X2, X3),
                  x(X1, mark X2) -> mark x(X1, X2),
                  x(mark X1, X2) -> mark x(X1, X2),
                 x(ok X1, ok X2) -> ok x(X1, X2),
          proper U12(X1, X2, X3) -> U12(proper X1, proper X2, proper X3),
                     proper tt() -> ok tt(),
          proper U11(X1, X2, X3) -> U11(proper X1, proper X2, proper X3),
                      proper s X -> s proper X,
             proper plus(X1, X2) -> plus(proper X1, proper X2),
          proper U22(X1, X2, X3) -> U22(proper X1, proper X2, proper X3),
          proper U21(X1, X2, X3) -> U21(proper X1, proper X2, proper X3),
                proper x(X1, X2) -> x(proper X1, proper X2),
                      proper 0() -> ok 0(),
                      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:
       {    U12(mark X1, X2, X3) -> mark U12(X1, X2, X3),
        U12(ok X1, ok X2, ok X3) -> ok U12(X1, X2, X3),
          active U12(X1, X2, X3) -> U12(active X1, X2, X3),
          active U12(tt(), M, N) -> mark s plus(N, M),
          active U11(X1, X2, X3) -> U11(active X1, X2, X3),
          active U11(tt(), M, N) -> mark U12(tt(), M, N),
                      active s X -> s active X,
             active plus(N, s M) -> mark U11(tt(), M, N),
             active plus(N, 0()) -> mark N,
             active plus(X1, X2) -> plus(X1, active X2),
             active plus(X1, X2) -> plus(active X1, X2),
          active U22(X1, X2, X3) -> U22(active X1, X2, X3),
          active U22(tt(), M, N) -> mark plus(x(N, M), N),
          active U21(X1, X2, X3) -> U21(active X1, X2, X3),
          active U21(tt(), M, N) -> mark U22(tt(), M, N),
                active x(N, s M) -> mark U21(tt(), M, N),
                active x(N, 0()) -> mark 0(),
                active x(X1, X2) -> x(X1, active X2),
                active x(X1, X2) -> x(active X1, X2),
            U11(mark X1, X2, X3) -> mark U11(X1, X2, X3),
        U11(ok X1, ok X2, ok X3) -> ok U11(X1, X2, X3),
                        s mark X -> mark s X,
                          s ok X -> ok s X,
               plus(X1, mark X2) -> mark plus(X1, X2),
               plus(mark X1, X2) -> mark plus(X1, X2),
              plus(ok X1, ok X2) -> ok plus(X1, X2),
            U22(mark X1, X2, X3) -> mark U22(X1, X2, X3),
        U22(ok X1, ok X2, ok X3) -> ok U22(X1, X2, X3),
            U21(mark X1, X2, X3) -> mark U21(X1, X2, X3),
        U21(ok X1, ok X2, ok X3) -> ok U21(X1, X2, X3),
                  x(X1, mark X2) -> mark x(X1, X2),
                  x(mark X1, X2) -> mark x(X1, X2),
                 x(ok X1, ok X2) -> ok x(X1, X2),
          proper U12(X1, X2, X3) -> U12(proper X1, proper X2, proper X3),
                     proper tt() -> ok tt(),
          proper U11(X1, X2, X3) -> U11(proper X1, proper X2, proper X3),
                      proper s X -> s proper X,
             proper plus(X1, X2) -> plus(proper X1, proper X2),
          proper U22(X1, X2, X3) -> U22(proper X1, proper X2, proper X3),
          proper U21(X1, X2, X3) -> U21(proper X1, proper X2, proper X3),
                proper x(X1, X2) -> x(proper X1, proper X2),
                      proper 0() -> ok 0(),
                      top mark X -> top proper X,
                        top ok X -> top active X}
       Open
      
      SCC (2):
       Strict:
        {    U12#(mark X1, X2, X3) -> U12#(X1, X2, X3),
         U12#(ok X1, ok X2, ok X3) -> U12#(X1, X2, X3)}
       Weak:
       {    U12(mark X1, X2, X3) -> mark U12(X1, X2, X3),
        U12(ok X1, ok X2, ok X3) -> ok U12(X1, X2, X3),
          active U12(X1, X2, X3) -> U12(active X1, X2, X3),
          active U12(tt(), M, N) -> mark s plus(N, M),
          active U11(X1, X2, X3) -> U11(active X1, X2, X3),
          active U11(tt(), M, N) -> mark U12(tt(), M, N),
                      active s X -> s active X,
             active plus(N, s M) -> mark U11(tt(), M, N),
             active plus(N, 0()) -> mark N,
             active plus(X1, X2) -> plus(X1, active X2),
             active plus(X1, X2) -> plus(active X1, X2),
          active U22(X1, X2, X3) -> U22(active X1, X2, X3),
          active U22(tt(), M, N) -> mark plus(x(N, M), N),
          active U21(X1, X2, X3) -> U21(active X1, X2, X3),
          active U21(tt(), M, N) -> mark U22(tt(), M, N),
                active x(N, s M) -> mark U21(tt(), M, N),
                active x(N, 0()) -> mark 0(),
                active x(X1, X2) -> x(X1, active X2),
                active x(X1, X2) -> x(active X1, X2),
            U11(mark X1, X2, X3) -> mark U11(X1, X2, X3),
        U11(ok X1, ok X2, ok X3) -> ok U11(X1, X2, X3),
                        s mark X -> mark s X,
                          s ok X -> ok s X,
               plus(X1, mark X2) -> mark plus(X1, X2),
               plus(mark X1, X2) -> mark plus(X1, X2),
              plus(ok X1, ok X2) -> ok plus(X1, X2),
            U22(mark X1, X2, X3) -> mark U22(X1, X2, X3),
        U22(ok X1, ok X2, ok X3) -> ok U22(X1, X2, X3),
            U21(mark X1, X2, X3) -> mark U21(X1, X2, X3),
        U21(ok X1, ok X2, ok X3) -> ok U21(X1, X2, X3),
                  x(X1, mark X2) -> mark x(X1, X2),
                  x(mark X1, X2) -> mark x(X1, X2),
                 x(ok X1, ok X2) -> ok x(X1, X2),
          proper U12(X1, X2, X3) -> U12(proper X1, proper X2, proper X3),
                     proper tt() -> ok tt(),
          proper U11(X1, X2, X3) -> U11(proper X1, proper X2, proper X3),
                      proper s X -> s proper X,
             proper plus(X1, X2) -> plus(proper X1, proper X2),
          proper U22(X1, X2, X3) -> U22(proper X1, proper X2, proper X3),
          proper U21(X1, X2, X3) -> U21(proper X1, proper X2, proper X3),
                proper x(X1, X2) -> x(proper X1, proper X2),
                      proper 0() -> ok 0(),
                      top mark X -> top proper X,
                        top ok X -> top active X}
       Open