MAYBE
Time: 1.052371
TRS:
 { active and(X1, X2) -> and(active X1, X2),
  active and(tt(), X) -> mark X,
  active plus(N, 0()) -> mark N,
  active plus(N, s M) -> mark s plus(N, M),
  active plus(X1, X2) -> plus(X1, active X2),
  active plus(X1, X2) -> plus(active X1, X2),
           active s X -> s active X,
     active x(N, 0()) -> mark 0(),
     active x(N, s M) -> mark plus(x(N, M), N),
     active x(X1, X2) -> x(X1, active X2),
     active x(X1, X2) -> x(active X1, X2),
     and(mark X1, X2) -> mark and(X1, X2),
    and(ok X1, ok X2) -> ok and(X1, X2),
    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),
             s mark X -> mark s X,
               s ok X -> ok s X,
       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 and(X1, X2) -> and(proper X1, proper X2),
          proper tt() -> ok tt(),
  proper plus(X1, X2) -> plus(proper X1, proper X2),
           proper 0() -> ok 0(),
           proper s X -> s proper X,
     proper x(X1, X2) -> x(proper X1, proper X2),
           top mark X -> top proper X,
             top ok X -> top active X}
 DP:
  DP:
   { active# and(X1, X2) -> active# X1,
     active# and(X1, X2) -> and#(active X1, X2),
    active# plus(N, s M) -> plus#(N, M),
    active# plus(N, s M) -> s# plus(N, M),
    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# s X -> active# X,
             active# s X -> s# active X,
       active# x(N, s M) -> plus#(x(N, M), N),
       active# x(N, s M) -> x#(N, M),
       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),
       and#(mark X1, X2) -> and#(X1, X2),
      and#(ok X1, ok X2) -> and#(X1, X2),
      plus#(X1, mark X2) -> plus#(X1, X2),
      plus#(mark X1, X2) -> plus#(X1, X2),
     plus#(ok X1, ok X2) -> plus#(X1, X2),
               s# mark X -> s# X,
                 s# ok X -> s# X,
         x#(X1, mark X2) -> x#(X1, X2),
         x#(mark X1, X2) -> x#(X1, X2),
        x#(ok X1, ok X2) -> x#(X1, X2),
     proper# and(X1, X2) -> and#(proper X1, proper X2),
     proper# and(X1, X2) -> proper# X1,
     proper# and(X1, X2) -> proper# X2,
    proper# plus(X1, X2) -> plus#(proper X1, proper X2),
    proper# plus(X1, X2) -> proper# X1,
    proper# plus(X1, X2) -> proper# X2,
             proper# s X -> s# proper X,
             proper# s X -> proper# X,
       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:
  { active and(X1, X2) -> and(active X1, X2),
   active and(tt(), X) -> mark X,
   active plus(N, 0()) -> mark N,
   active plus(N, s M) -> mark s plus(N, M),
   active plus(X1, X2) -> plus(X1, active X2),
   active plus(X1, X2) -> plus(active X1, X2),
            active s X -> s active X,
      active x(N, 0()) -> mark 0(),
      active x(N, s M) -> mark plus(x(N, M), N),
      active x(X1, X2) -> x(X1, active X2),
      active x(X1, X2) -> x(active X1, X2),
      and(mark X1, X2) -> mark and(X1, X2),
     and(ok X1, ok X2) -> ok and(X1, X2),
     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),
              s mark X -> mark s X,
                s ok X -> ok s X,
        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 and(X1, X2) -> and(proper X1, proper X2),
           proper tt() -> ok tt(),
   proper plus(X1, X2) -> plus(proper X1, proper X2),
            proper 0() -> ok 0(),
            proper s X -> s proper X,
      proper x(X1, X2) -> x(proper X1, proper X2),
            top mark X -> top proper X,
              top ok X -> top active X}
  UR:
   { active and(X1, X2) -> and(active X1, X2),
    active and(tt(), X) -> mark X,
    active plus(N, 0()) -> mark N,
    active plus(N, s M) -> mark s plus(N, M),
    active plus(X1, X2) -> plus(X1, active X2),
    active plus(X1, X2) -> plus(active X1, X2),
             active s X -> s active X,
       active x(N, 0()) -> mark 0(),
       active x(N, s M) -> mark plus(x(N, M), N),
       active x(X1, X2) -> x(X1, active X2),
       active x(X1, X2) -> x(active X1, X2),
       and(mark X1, X2) -> mark and(X1, X2),
      and(ok X1, ok X2) -> ok and(X1, X2),
      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),
               s mark X -> mark s X,
                 s ok X -> ok s X,
         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 and(X1, X2) -> and(proper X1, proper X2),
            proper tt() -> ok tt(),
    proper plus(X1, X2) -> plus(proper X1, proper X2),
             proper 0() -> ok 0(),
             proper s X -> s proper X,
       proper x(X1, X2) -> x(proper X1, proper X2)}
   EDG:
    {
     (active# x(N, s M) -> plus#(x(N, M), N), plus#(ok X1, ok X2) -> plus#(X1, X2))
     (active# x(N, s M) -> plus#(x(N, M), N), plus#(mark X1, X2) -> plus#(X1, X2))
     (active# x(N, s M) -> plus#(x(N, M), N), plus#(X1, mark X2) -> plus#(X1, X2))
     (s# ok X -> s# X, s# ok X -> s# X)
     (s# ok X -> s# X, s# mark X -> s# X)
     (top# mark X -> proper# X, proper# x(X1, X2) -> proper# X2)
     (top# mark X -> proper# X, proper# x(X1, X2) -> proper# X1)
     (top# mark X -> proper# X, proper# x(X1, X2) -> x#(proper X1, proper X2))
     (top# mark X -> proper# X, proper# s X -> proper# X)
     (top# mark X -> proper# X, proper# s X -> s# proper X)
     (top# mark X -> proper# X, proper# plus(X1, X2) -> proper# X2)
     (top# mark X -> proper# X, proper# plus(X1, X2) -> proper# X1)
     (top# mark X -> proper# X, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (top# mark X -> proper# X, proper# and(X1, X2) -> proper# X2)
     (top# mark X -> proper# X, proper# and(X1, X2) -> proper# X1)
     (top# mark X -> proper# X, proper# and(X1, X2) -> and#(proper X1, proper X2))
     (and#(mark X1, X2) -> and#(X1, X2), and#(ok X1, ok X2) -> and#(X1, X2))
     (and#(mark X1, X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2))
     (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# 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# and(X1, X2) -> and#(proper X1, proper X2), and#(ok X1, ok X2) -> and#(X1, X2))
     (proper# and(X1, X2) -> and#(proper X1, proper X2), and#(mark X1, X2) -> and#(X1, X2))
     (proper# x(X1, X2) -> x#(proper X1, proper X2), x#(ok X1, ok 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#(X1, mark X2) -> x#(X1, X2))
     (active# plus(X1, X2) -> active# X1, active# x(X1, X2) -> x#(active X1, 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) -> active# X2)
     (active# plus(X1, X2) -> active# X1, active# x(X1, X2) -> active# X1)
     (active# plus(X1, X2) -> active# X1, active# x(N, s M) -> x#(N, M))
     (active# plus(X1, X2) -> active# X1, active# x(N, s M) -> plus#(x(N, M), N))
     (active# plus(X1, X2) -> active# X1, active# s X -> s# active X)
     (active# plus(X1, X2) -> active# X1, active# s X -> active# X)
     (active# plus(X1, X2) -> active# X1, active# plus(X1, X2) -> plus#(active X1, 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) -> active# X2)
     (active# plus(X1, X2) -> active# X1, active# plus(X1, X2) -> active# X1)
     (active# plus(X1, X2) -> active# X1, active# plus(N, s M) -> s# plus(N, M))
     (active# plus(X1, X2) -> active# X1, active# plus(N, s M) -> plus#(N, M))
     (active# plus(X1, X2) -> active# X1, active# and(X1, X2) -> and#(active X1, X2))
     (active# plus(X1, X2) -> active# X1, active# and(X1, X2) -> active# X1)
     (proper# and(X1, X2) -> proper# X1, proper# x(X1, X2) -> proper# X2)
     (proper# and(X1, X2) -> proper# X1, proper# x(X1, X2) -> proper# X1)
     (proper# and(X1, X2) -> proper# X1, proper# x(X1, X2) -> x#(proper X1, proper X2))
     (proper# and(X1, X2) -> proper# X1, proper# s X -> proper# X)
     (proper# and(X1, X2) -> proper# X1, proper# s X -> s# proper X)
     (proper# and(X1, X2) -> proper# X1, proper# plus(X1, X2) -> proper# X2)
     (proper# and(X1, X2) -> proper# X1, proper# plus(X1, X2) -> proper# X1)
     (proper# and(X1, X2) -> proper# X1, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# and(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X2)
     (proper# and(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X1)
     (proper# and(X1, X2) -> proper# X1, proper# and(X1, X2) -> and#(proper X1, proper X2))
     (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# s X -> proper# X)
     (proper# x(X1, X2) -> proper# X1, proper# s X -> s# proper X)
     (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# and(X1, X2) -> proper# X2)
     (proper# x(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X1)
     (proper# x(X1, X2) -> proper# X1, proper# and(X1, X2) -> and#(proper X1, proper X2))
     (active# plus(X1, X2) -> active# X2, active# x(X1, X2) -> x#(active X1, 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) -> active# X2)
     (active# plus(X1, X2) -> active# X2, active# x(X1, X2) -> active# X1)
     (active# plus(X1, X2) -> active# X2, active# x(N, s M) -> x#(N, M))
     (active# plus(X1, X2) -> active# X2, active# x(N, s M) -> plus#(x(N, M), N))
     (active# plus(X1, X2) -> active# X2, active# s X -> s# active X)
     (active# plus(X1, X2) -> active# X2, active# s X -> active# X)
     (active# plus(X1, X2) -> active# X2, active# plus(X1, X2) -> plus#(active X1, 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) -> active# X2)
     (active# plus(X1, X2) -> active# X2, active# plus(X1, X2) -> active# X1)
     (active# plus(X1, X2) -> active# X2, active# plus(N, s M) -> s# plus(N, M))
     (active# plus(X1, X2) -> active# X2, active# plus(N, s M) -> plus#(N, M))
     (active# plus(X1, X2) -> active# X2, active# and(X1, X2) -> and#(active X1, X2))
     (active# plus(X1, X2) -> active# X2, active# and(X1, X2) -> active# X1)
     (proper# and(X1, X2) -> proper# X2, proper# x(X1, X2) -> proper# X2)
     (proper# and(X1, X2) -> proper# X2, proper# x(X1, X2) -> proper# X1)
     (proper# and(X1, X2) -> proper# X2, proper# x(X1, X2) -> x#(proper X1, proper X2))
     (proper# and(X1, X2) -> proper# X2, proper# s X -> proper# X)
     (proper# and(X1, X2) -> proper# X2, proper# s X -> s# proper X)
     (proper# and(X1, X2) -> proper# X2, proper# plus(X1, X2) -> proper# X2)
     (proper# and(X1, X2) -> proper# X2, proper# plus(X1, X2) -> proper# X1)
     (proper# and(X1, X2) -> proper# X2, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# and(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X2)
     (proper# and(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X1)
     (proper# and(X1, X2) -> proper# X2, proper# and(X1, X2) -> and#(proper X1, proper X2))
     (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# s X -> proper# X)
     (proper# x(X1, X2) -> proper# X2, proper# s X -> s# proper X)
     (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# and(X1, X2) -> proper# X2)
     (proper# x(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X1)
     (proper# x(X1, X2) -> proper# X2, proper# and(X1, X2) -> and#(proper X1, proper X2))
     (proper# s X -> s# proper X, s# ok X -> s# X)
     (proper# s X -> s# proper X, s# mark X -> s# X)
     (top# ok X -> top# active X, top# ok X -> top# active X)
     (top# ok X -> top# active X, top# ok X -> active# X)
     (top# ok X -> top# active X, top# mark X -> top# proper X)
     (top# ok X -> top# active X, top# mark X -> proper# X)
     (active# 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# plus(N, s M) -> plus#(N, M), plus#(ok X1, ok X2) -> plus#(X1, X2))
     (active# plus(N, s M) -> plus#(N, M), plus#(mark X1, X2) -> plus#(X1, X2))
     (active# plus(N, s M) -> plus#(N, M), plus#(X1, mark X2) -> plus#(X1, X2))
     (active# x(N, s M) -> x#(N, M), x#(X1, mark X2) -> x#(X1, X2))
     (active# x(N, s M) -> x#(N, M), x#(mark X1, X2) -> x#(X1, X2))
     (active# x(N, s M) -> x#(N, M), x#(ok X1, ok X2) -> x#(X1, X2))
     (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))
     (active# and(X1, X2) -> and#(active X1, X2), and#(mark X1, X2) -> and#(X1, X2))
     (active# and(X1, X2) -> and#(active X1, X2), and#(ok X1, ok X2) -> and#(X1, X2))
     (top# mark X -> top# proper X, top# mark X -> proper# X)
     (top# mark X -> top# proper X, top# mark X -> top# proper X)
     (top# mark X -> top# proper X, top# ok X -> active# X)
     (top# mark X -> top# proper X, top# ok X -> top# active X)
     (active# s X -> s# active X, s# mark X -> s# X)
     (active# s X -> s# active X, s# ok X -> s# X)
     (proper# plus(X1, X2) -> proper# X2, proper# and(X1, X2) -> and#(proper X1, proper X2))
     (proper# plus(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X1)
     (proper# plus(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X2)
     (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# s X -> s# proper X)
     (proper# plus(X1, X2) -> proper# X2, proper# s X -> proper# X)
     (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)
     (active# x(X1, X2) -> active# X2, active# and(X1, X2) -> active# X1)
     (active# x(X1, X2) -> active# X2, active# and(X1, X2) -> and#(active X1, X2))
     (active# x(X1, X2) -> active# X2, active# plus(N, s M) -> plus#(N, M))
     (active# x(X1, X2) -> active# X2, active# plus(N, s M) -> s# plus(N, M))
     (active# x(X1, X2) -> active# X2, active# plus(X1, X2) -> active# X1)
     (active# x(X1, X2) -> active# X2, active# plus(X1, X2) -> active# 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) -> plus#(active X1, X2))
     (active# x(X1, X2) -> active# X2, active# s X -> active# X)
     (active# x(X1, X2) -> active# X2, active# s X -> s# active X)
     (active# x(X1, X2) -> active# X2, active# x(N, s M) -> plus#(x(N, M), N))
     (active# x(X1, X2) -> active# X2, active# x(N, s M) -> x#(N, M))
     (active# x(X1, X2) -> active# X2, active# x(X1, X2) -> active# X1)
     (active# x(X1, X2) -> active# X2, active# x(X1, X2) -> active# 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) -> x#(active X1, X2))
     (active# plus(N, s M) -> s# plus(N, M), s# mark X -> s# X)
     (active# plus(N, s M) -> s# plus(N, M), s# ok X -> s# X)
     (proper# plus(X1, X2) -> proper# X1, proper# and(X1, X2) -> and#(proper X1, proper X2))
     (proper# plus(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X1)
     (proper# plus(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X2)
     (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# s X -> s# proper X)
     (proper# plus(X1, X2) -> proper# X1, proper# s X -> proper# X)
     (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)
     (active# x(X1, X2) -> active# X1, active# and(X1, X2) -> active# X1)
     (active# x(X1, X2) -> active# X1, active# and(X1, X2) -> and#(active X1, X2))
     (active# x(X1, X2) -> active# X1, active# plus(N, s M) -> plus#(N, M))
     (active# x(X1, X2) -> active# X1, active# plus(N, s M) -> s# plus(N, M))
     (active# x(X1, X2) -> active# X1, active# plus(X1, X2) -> active# X1)
     (active# x(X1, X2) -> active# X1, active# plus(X1, X2) -> active# 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) -> plus#(active X1, X2))
     (active# x(X1, X2) -> active# X1, active# s X -> active# X)
     (active# x(X1, X2) -> active# X1, active# s X -> s# active X)
     (active# x(X1, X2) -> active# X1, active# x(N, s M) -> plus#(x(N, M), N))
     (active# x(X1, X2) -> active# X1, active# x(N, s M) -> x#(N, M))
     (active# x(X1, X2) -> active# X1, active# x(X1, X2) -> active# X1)
     (active# x(X1, X2) -> active# X1, active# x(X1, X2) -> active# 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) -> x#(active X1, X2))
     (active# and(X1, X2) -> active# X1, active# and(X1, X2) -> active# X1)
     (active# and(X1, X2) -> active# X1, active# and(X1, X2) -> and#(active X1, X2))
     (active# and(X1, X2) -> active# X1, active# plus(N, s M) -> plus#(N, M))
     (active# and(X1, X2) -> active# X1, active# plus(N, s M) -> s# plus(N, M))
     (active# and(X1, X2) -> active# X1, active# plus(X1, X2) -> active# X1)
     (active# and(X1, X2) -> active# X1, active# plus(X1, X2) -> active# X2)
     (active# and(X1, X2) -> active# X1, active# plus(X1, X2) -> plus#(X1, active X2))
     (active# and(X1, X2) -> active# X1, active# plus(X1, X2) -> plus#(active X1, X2))
     (active# and(X1, X2) -> active# X1, active# s X -> active# X)
     (active# and(X1, X2) -> active# X1, active# s X -> s# active X)
     (active# and(X1, X2) -> active# X1, active# x(N, s M) -> plus#(x(N, M), N))
     (active# and(X1, X2) -> active# X1, active# x(N, s M) -> x#(N, M))
     (active# and(X1, X2) -> active# X1, active# x(X1, X2) -> active# X1)
     (active# and(X1, X2) -> active# X1, active# x(X1, X2) -> active# X2)
     (active# and(X1, X2) -> active# X1, active# x(X1, X2) -> x#(X1, active X2))
     (active# and(X1, X2) -> active# X1, active# x(X1, X2) -> x#(active X1, X2))
     (proper# plus(X1, X2) -> plus#(proper X1, proper X2), plus#(X1, mark 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#(ok X1, ok X2) -> plus#(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))
     (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))
     (and#(ok X1, ok X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2))
     (and#(ok X1, ok X2) -> and#(X1, X2), and#(ok X1, ok X2) -> and#(X1, X2))
     (top# ok X -> active# X, active# and(X1, X2) -> active# X1)
     (top# ok X -> active# X, active# and(X1, X2) -> and#(active X1, X2))
     (top# ok X -> active# X, active# plus(N, s M) -> plus#(N, M))
     (top# ok X -> active# X, active# plus(N, s M) -> s# plus(N, M))
     (top# ok X -> active# X, active# plus(X1, X2) -> active# X1)
     (top# ok X -> active# X, active# plus(X1, X2) -> active# X2)
     (top# ok X -> active# X, active# plus(X1, X2) -> plus#(X1, active X2))
     (top# ok X -> active# X, active# plus(X1, X2) -> plus#(active X1, X2))
     (top# ok X -> active# X, active# s X -> active# X)
     (top# ok X -> active# X, active# s X -> s# active X)
     (top# ok X -> active# X, active# x(N, s M) -> plus#(x(N, M), N))
     (top# ok X -> active# X, active# x(N, s M) -> x#(N, M))
     (top# ok X -> active# X, active# x(X1, X2) -> active# X1)
     (top# ok X -> active# X, active# x(X1, X2) -> active# X2)
     (top# ok X -> active# X, active# x(X1, X2) -> x#(X1, active X2))
     (top# ok X -> active# X, active# x(X1, X2) -> x#(active X1, X2))
     (proper# s X -> proper# X, proper# and(X1, X2) -> and#(proper X1, proper X2))
     (proper# s X -> proper# X, proper# and(X1, X2) -> proper# X1)
     (proper# s X -> proper# X, proper# and(X1, X2) -> proper# X2)
     (proper# s X -> proper# X, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# s X -> proper# X, proper# plus(X1, X2) -> proper# X1)
     (proper# s X -> proper# X, proper# plus(X1, X2) -> proper# X2)
     (proper# s X -> proper# X, proper# s X -> s# proper X)
     (proper# s X -> proper# X, proper# s X -> proper# X)
     (proper# s X -> proper# X, proper# x(X1, X2) -> x#(proper X1, proper X2))
     (proper# s X -> proper# X, proper# x(X1, X2) -> proper# X1)
     (proper# s X -> proper# X, proper# x(X1, X2) -> proper# X2)
     (s# mark X -> s# X, s# mark X -> s# X)
     (s# mark X -> s# X, s# ok X -> s# X)
     (active# s X -> active# X, active# and(X1, X2) -> active# X1)
     (active# s X -> active# X, active# and(X1, X2) -> and#(active X1, X2))
     (active# s X -> active# X, active# plus(N, s M) -> plus#(N, M))
     (active# s X -> active# X, active# plus(N, s M) -> s# plus(N, M))
     (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# s X -> active# X)
     (active# s X -> active# X, active# s X -> s# active X)
     (active# s X -> active# X, active# x(N, s M) -> plus#(x(N, M), N))
     (active# s X -> active# X, active# x(N, s M) -> x#(N, M))
     (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))
    }
    EDG:
     {
      (active# x(N, s M) -> plus#(x(N, M), N), plus#(ok X1, ok X2) -> plus#(X1, X2))
      (active# x(N, s M) -> plus#(x(N, M), N), plus#(mark X1, X2) -> plus#(X1, X2))
      (s# ok X -> s# X, s# ok X -> s# X)
      (s# ok X -> s# X, s# mark X -> s# X)
      (top# mark X -> proper# X, proper# x(X1, X2) -> proper# X2)
      (top# mark X -> proper# X, proper# x(X1, X2) -> proper# X1)
      (top# mark X -> proper# X, proper# x(X1, X2) -> x#(proper X1, proper X2))
      (top# mark X -> proper# X, proper# s X -> proper# X)
      (top# mark X -> proper# X, proper# s X -> s# proper X)
      (top# mark X -> proper# X, proper# plus(X1, X2) -> proper# X2)
      (top# mark X -> proper# X, proper# plus(X1, X2) -> proper# X1)
      (top# mark X -> proper# X, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
      (top# mark X -> proper# X, proper# and(X1, X2) -> proper# X2)
      (top# mark X -> proper# X, proper# and(X1, X2) -> proper# X1)
      (top# mark X -> proper# X, proper# and(X1, X2) -> and#(proper X1, proper X2))
      (and#(mark X1, X2) -> and#(X1, X2), and#(ok X1, ok X2) -> and#(X1, X2))
      (and#(mark X1, X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2))
      (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# 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# and(X1, X2) -> and#(proper X1, proper X2), and#(ok X1, ok X2) -> and#(X1, X2))
      (proper# and(X1, X2) -> and#(proper X1, proper X2), and#(mark X1, X2) -> and#(X1, X2))
      (proper# x(X1, X2) -> x#(proper X1, proper X2), x#(ok X1, ok 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#(X1, mark X2) -> x#(X1, X2))
      (active# plus(X1, X2) -> active# X1, active# x(X1, X2) -> x#(active X1, 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) -> active# X2)
      (active# plus(X1, X2) -> active# X1, active# x(X1, X2) -> active# X1)
      (active# plus(X1, X2) -> active# X1, active# x(N, s M) -> x#(N, M))
      (active# plus(X1, X2) -> active# X1, active# x(N, s M) -> plus#(x(N, M), N))
      (active# plus(X1, X2) -> active# X1, active# s X -> s# active X)
      (active# plus(X1, X2) -> active# X1, active# s X -> active# X)
      (active# plus(X1, X2) -> active# X1, active# plus(X1, X2) -> plus#(active X1, 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) -> active# X2)
      (active# plus(X1, X2) -> active# X1, active# plus(X1, X2) -> active# X1)
      (active# plus(X1, X2) -> active# X1, active# plus(N, s M) -> s# plus(N, M))
      (active# plus(X1, X2) -> active# X1, active# plus(N, s M) -> plus#(N, M))
      (active# plus(X1, X2) -> active# X1, active# and(X1, X2) -> and#(active X1, X2))
      (active# plus(X1, X2) -> active# X1, active# and(X1, X2) -> active# X1)
      (proper# and(X1, X2) -> proper# X1, proper# x(X1, X2) -> proper# X2)
      (proper# and(X1, X2) -> proper# X1, proper# x(X1, X2) -> proper# X1)
      (proper# and(X1, X2) -> proper# X1, proper# x(X1, X2) -> x#(proper X1, proper X2))
      (proper# and(X1, X2) -> proper# X1, proper# s X -> proper# X)
      (proper# and(X1, X2) -> proper# X1, proper# s X -> s# proper X)
      (proper# and(X1, X2) -> proper# X1, proper# plus(X1, X2) -> proper# X2)
      (proper# and(X1, X2) -> proper# X1, proper# plus(X1, X2) -> proper# X1)
      (proper# and(X1, X2) -> proper# X1, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
      (proper# and(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X2)
      (proper# and(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X1)
      (proper# and(X1, X2) -> proper# X1, proper# and(X1, X2) -> and#(proper X1, proper X2))
      (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# s X -> proper# X)
      (proper# x(X1, X2) -> proper# X1, proper# s X -> s# proper X)
      (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# and(X1, X2) -> proper# X2)
      (proper# x(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X1)
      (proper# x(X1, X2) -> proper# X1, proper# and(X1, X2) -> and#(proper X1, proper X2))
      (active# plus(X1, X2) -> active# X2, active# x(X1, X2) -> x#(active X1, 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) -> active# X2)
      (active# plus(X1, X2) -> active# X2, active# x(X1, X2) -> active# X1)
      (active# plus(X1, X2) -> active# X2, active# x(N, s M) -> x#(N, M))
      (active# plus(X1, X2) -> active# X2, active# x(N, s M) -> plus#(x(N, M), N))
      (active# plus(X1, X2) -> active# X2, active# s X -> s# active X)
      (active# plus(X1, X2) -> active# X2, active# s X -> active# X)
      (active# plus(X1, X2) -> active# X2, active# plus(X1, X2) -> plus#(active X1, 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) -> active# X2)
      (active# plus(X1, X2) -> active# X2, active# plus(X1, X2) -> active# X1)
      (active# plus(X1, X2) -> active# X2, active# plus(N, s M) -> s# plus(N, M))
      (active# plus(X1, X2) -> active# X2, active# plus(N, s M) -> plus#(N, M))
      (active# plus(X1, X2) -> active# X2, active# and(X1, X2) -> and#(active X1, X2))
      (active# plus(X1, X2) -> active# X2, active# and(X1, X2) -> active# X1)
      (proper# and(X1, X2) -> proper# X2, proper# x(X1, X2) -> proper# X2)
      (proper# and(X1, X2) -> proper# X2, proper# x(X1, X2) -> proper# X1)
      (proper# and(X1, X2) -> proper# X2, proper# x(X1, X2) -> x#(proper X1, proper X2))
      (proper# and(X1, X2) -> proper# X2, proper# s X -> proper# X)
      (proper# and(X1, X2) -> proper# X2, proper# s X -> s# proper X)
      (proper# and(X1, X2) -> proper# X2, proper# plus(X1, X2) -> proper# X2)
      (proper# and(X1, X2) -> proper# X2, proper# plus(X1, X2) -> proper# X1)
      (proper# and(X1, X2) -> proper# X2, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
      (proper# and(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X2)
      (proper# and(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X1)
      (proper# and(X1, X2) -> proper# X2, proper# and(X1, X2) -> and#(proper X1, proper X2))
      (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# s X -> proper# X)
      (proper# x(X1, X2) -> proper# X2, proper# s X -> s# proper X)
      (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# and(X1, X2) -> proper# X2)
      (proper# x(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X1)
      (proper# x(X1, X2) -> proper# X2, proper# and(X1, X2) -> and#(proper X1, proper X2))
      (proper# s X -> s# proper X, s# ok X -> s# X)
      (proper# s X -> s# proper X, s# mark X -> s# X)
      (top# ok X -> top# active X, top# ok X -> top# active X)
      (top# ok X -> top# active X, top# ok X -> active# X)
      (top# ok X -> top# active X, top# mark X -> top# proper X)
      (top# ok X -> top# active X, top# mark X -> proper# X)
      (active# 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# 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))
      (active# and(X1, X2) -> and#(active X1, X2), and#(mark X1, X2) -> and#(X1, X2))
      (active# and(X1, X2) -> and#(active X1, X2), and#(ok X1, ok X2) -> and#(X1, X2))
      (top# mark X -> top# proper X, top# mark X -> proper# X)
      (top# mark X -> top# proper X, top# mark X -> top# proper X)
      (top# mark X -> top# proper X, top# ok X -> active# X)
      (top# mark X -> top# proper X, top# ok X -> top# active X)
      (active# s X -> s# active X, s# mark X -> s# X)
      (active# s X -> s# active X, s# ok X -> s# X)
      (proper# plus(X1, X2) -> proper# X2, proper# and(X1, X2) -> and#(proper X1, proper X2))
      (proper# plus(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X1)
      (proper# plus(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X2)
      (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# s X -> s# proper X)
      (proper# plus(X1, X2) -> proper# X2, proper# s X -> proper# X)
      (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)
      (active# x(X1, X2) -> active# X2, active# and(X1, X2) -> active# X1)
      (active# x(X1, X2) -> active# X2, active# and(X1, X2) -> and#(active X1, X2))
      (active# x(X1, X2) -> active# X2, active# plus(N, s M) -> plus#(N, M))
      (active# x(X1, X2) -> active# X2, active# plus(N, s M) -> s# plus(N, M))
      (active# x(X1, X2) -> active# X2, active# plus(X1, X2) -> active# X1)
      (active# x(X1, X2) -> active# X2, active# plus(X1, X2) -> active# 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) -> plus#(active X1, X2))
      (active# x(X1, X2) -> active# X2, active# s X -> active# X)
      (active# x(X1, X2) -> active# X2, active# s X -> s# active X)
      (active# x(X1, X2) -> active# X2, active# x(N, s M) -> plus#(x(N, M), N))
      (active# x(X1, X2) -> active# X2, active# x(N, s M) -> x#(N, M))
      (active# x(X1, X2) -> active# X2, active# x(X1, X2) -> active# X1)
      (active# x(X1, X2) -> active# X2, active# x(X1, X2) -> active# 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) -> x#(active X1, X2))
      (active# plus(N, s M) -> s# plus(N, M), s# mark X -> s# X)
      (active# plus(N, s M) -> s# plus(N, M), s# ok X -> s# X)
      (proper# plus(X1, X2) -> proper# X1, proper# and(X1, X2) -> and#(proper X1, proper X2))
      (proper# plus(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X1)
      (proper# plus(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X2)
      (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# s X -> s# proper X)
      (proper# plus(X1, X2) -> proper# X1, proper# s X -> proper# X)
      (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)
      (active# x(X1, X2) -> active# X1, active# and(X1, X2) -> active# X1)
      (active# x(X1, X2) -> active# X1, active# and(X1, X2) -> and#(active X1, X2))
      (active# x(X1, X2) -> active# X1, active# plus(N, s M) -> plus#(N, M))
      (active# x(X1, X2) -> active# X1, active# plus(N, s M) -> s# plus(N, M))
      (active# x(X1, X2) -> active# X1, active# plus(X1, X2) -> active# X1)
      (active# x(X1, X2) -> active# X1, active# plus(X1, X2) -> active# 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) -> plus#(active X1, X2))
      (active# x(X1, X2) -> active# X1, active# s X -> active# X)
      (active# x(X1, X2) -> active# X1, active# s X -> s# active X)
      (active# x(X1, X2) -> active# X1, active# x(N, s M) -> plus#(x(N, M), N))
      (active# x(X1, X2) -> active# X1, active# x(N, s M) -> x#(N, M))
      (active# x(X1, X2) -> active# X1, active# x(X1, X2) -> active# X1)
      (active# x(X1, X2) -> active# X1, active# x(X1, X2) -> active# 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) -> x#(active X1, X2))
      (active# and(X1, X2) -> active# X1, active# and(X1, X2) -> active# X1)
      (active# and(X1, X2) -> active# X1, active# and(X1, X2) -> and#(active X1, X2))
      (active# and(X1, X2) -> active# X1, active# plus(N, s M) -> plus#(N, M))
      (active# and(X1, X2) -> active# X1, active# plus(N, s M) -> s# plus(N, M))
      (active# and(X1, X2) -> active# X1, active# plus(X1, X2) -> active# X1)
      (active# and(X1, X2) -> active# X1, active# plus(X1, X2) -> active# X2)
      (active# and(X1, X2) -> active# X1, active# plus(X1, X2) -> plus#(X1, active X2))
      (active# and(X1, X2) -> active# X1, active# plus(X1, X2) -> plus#(active X1, X2))
      (active# and(X1, X2) -> active# X1, active# s X -> active# X)
      (active# and(X1, X2) -> active# X1, active# s X -> s# active X)
      (active# and(X1, X2) -> active# X1, active# x(N, s M) -> plus#(x(N, M), N))
      (active# and(X1, X2) -> active# X1, active# x(N, s M) -> x#(N, M))
      (active# and(X1, X2) -> active# X1, active# x(X1, X2) -> active# X1)
      (active# and(X1, X2) -> active# X1, active# x(X1, X2) -> active# X2)
      (active# and(X1, X2) -> active# X1, active# x(X1, X2) -> x#(X1, active X2))
      (active# and(X1, X2) -> active# X1, active# x(X1, X2) -> x#(active X1, X2))
      (proper# plus(X1, X2) -> plus#(proper X1, proper X2), plus#(X1, mark 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#(ok X1, ok X2) -> plus#(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))
      (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))
      (and#(ok X1, ok X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2))
      (and#(ok X1, ok X2) -> and#(X1, X2), and#(ok X1, ok X2) -> and#(X1, X2))
      (top# ok X -> active# X, active# and(X1, X2) -> active# X1)
      (top# ok X -> active# X, active# and(X1, X2) -> and#(active X1, X2))
      (top# ok X -> active# X, active# plus(N, s M) -> plus#(N, M))
      (top# ok X -> active# X, active# plus(N, s M) -> s# plus(N, M))
      (top# ok X -> active# X, active# plus(X1, X2) -> active# X1)
      (top# ok X -> active# X, active# plus(X1, X2) -> active# X2)
      (top# ok X -> active# X, active# plus(X1, X2) -> plus#(X1, active X2))
      (top# ok X -> active# X, active# plus(X1, X2) -> plus#(active X1, X2))
      (top# ok X -> active# X, active# s X -> active# X)
      (top# ok X -> active# X, active# s X -> s# active X)
      (top# ok X -> active# X, active# x(N, s M) -> plus#(x(N, M), N))
      (top# ok X -> active# X, active# x(N, s M) -> x#(N, M))
      (top# ok X -> active# X, active# x(X1, X2) -> active# X1)
      (top# ok X -> active# X, active# x(X1, X2) -> active# X2)
      (top# ok X -> active# X, active# x(X1, X2) -> x#(X1, active X2))
      (top# ok X -> active# X, active# x(X1, X2) -> x#(active X1, X2))
      (proper# s X -> proper# X, proper# and(X1, X2) -> and#(proper X1, proper X2))
      (proper# s X -> proper# X, proper# and(X1, X2) -> proper# X1)
      (proper# s X -> proper# X, proper# and(X1, X2) -> proper# X2)
      (proper# s X -> proper# X, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
      (proper# s X -> proper# X, proper# plus(X1, X2) -> proper# X1)
      (proper# s X -> proper# X, proper# plus(X1, X2) -> proper# X2)
      (proper# s X -> proper# X, proper# s X -> s# proper X)
      (proper# s X -> proper# X, proper# s X -> proper# X)
      (proper# s X -> proper# X, proper# x(X1, X2) -> x#(proper X1, proper X2))
      (proper# s X -> proper# X, proper# x(X1, X2) -> proper# X1)
      (proper# s X -> proper# X, proper# x(X1, X2) -> proper# X2)
      (s# mark X -> s# X, s# mark X -> s# X)
      (s# mark X -> s# X, s# ok X -> s# X)
      (active# s X -> active# X, active# and(X1, X2) -> active# X1)
      (active# s X -> active# X, active# and(X1, X2) -> and#(active X1, X2))
      (active# s X -> active# X, active# plus(N, s M) -> plus#(N, M))
      (active# s X -> active# X, active# plus(N, s M) -> s# plus(N, M))
      (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# s X -> active# X)
      (active# s X -> active# X, active# s X -> s# active X)
      (active# s X -> active# X, active# x(N, s M) -> plus#(x(N, M), N))
      (active# s X -> active# X, active# x(N, s M) -> x#(N, M))
      (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))
     }
     STATUS:
      arrows: 0.845330
      SCCS (7):
       Scc:
        {top# mark X -> top# proper X,
           top# ok X -> top# active X}
       Scc:
        { proper# and(X1, X2) -> proper# X1,
          proper# and(X1, X2) -> proper# X2,
         proper# plus(X1, X2) -> proper# X1,
         proper# plus(X1, X2) -> proper# X2,
                  proper# s X -> proper# X,
            proper# x(X1, X2) -> proper# X1,
            proper# x(X1, X2) -> proper# X2}
       Scc:
        { active# and(X1, X2) -> active# X1,
         active# plus(X1, X2) -> active# X1,
         active# plus(X1, X2) -> active# X2,
                  active# s X -> active# X,
            active# x(X1, X2) -> active# X1,
            active# x(X1, X2) -> active# X2}
       Scc:
        { x#(X1, mark X2) -> x#(X1, X2),
          x#(mark X1, X2) -> x#(X1, X2),
         x#(ok X1, ok X2) -> x#(X1, X2)}
       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:
        { and#(mark X1, X2) -> and#(X1, X2),
         and#(ok X1, ok X2) -> and#(X1, X2)}
       
       SCC (2):
        Strict:
         {top# mark X -> top# proper X,
            top# ok X -> top# active X}
        Weak:
        { active and(X1, X2) -> and(active X1, X2),
         active and(tt(), X) -> mark X,
         active plus(N, 0()) -> mark N,
         active plus(N, s M) -> mark s plus(N, M),
         active plus(X1, X2) -> plus(X1, active X2),
         active plus(X1, X2) -> plus(active X1, X2),
                  active s X -> s active X,
            active x(N, 0()) -> mark 0(),
            active x(N, s M) -> mark plus(x(N, M), N),
            active x(X1, X2) -> x(X1, active X2),
            active x(X1, X2) -> x(active X1, X2),
            and(mark X1, X2) -> mark and(X1, X2),
           and(ok X1, ok X2) -> ok and(X1, X2),
           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),
                    s mark X -> mark s X,
                      s ok X -> ok s X,
              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 and(X1, X2) -> and(proper X1, proper X2),
                 proper tt() -> ok tt(),
         proper plus(X1, X2) -> plus(proper X1, proper X2),
                  proper 0() -> ok 0(),
                  proper s X -> s proper X,
            proper x(X1, X2) -> x(proper X1, proper X2),
                  top mark X -> top proper X,
                    top ok X -> top active X}
        Open
       
       
       SCC (7):
        Strict:
         { proper# and(X1, X2) -> proper# X1,
           proper# and(X1, X2) -> proper# X2,
          proper# plus(X1, X2) -> proper# X1,
          proper# plus(X1, X2) -> proper# X2,
                   proper# s X -> proper# X,
             proper# x(X1, X2) -> proper# X1,
             proper# x(X1, X2) -> proper# X2}
        Weak:
        { active and(X1, X2) -> and(active X1, X2),
         active and(tt(), X) -> mark X,
         active plus(N, 0()) -> mark N,
         active plus(N, s M) -> mark s plus(N, M),
         active plus(X1, X2) -> plus(X1, active X2),
         active plus(X1, X2) -> plus(active X1, X2),
                  active s X -> s active X,
            active x(N, 0()) -> mark 0(),
            active x(N, s M) -> mark plus(x(N, M), N),
            active x(X1, X2) -> x(X1, active X2),
            active x(X1, X2) -> x(active X1, X2),
            and(mark X1, X2) -> mark and(X1, X2),
           and(ok X1, ok X2) -> ok and(X1, X2),
           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),
                    s mark X -> mark s X,
                      s ok X -> ok s X,
              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 and(X1, X2) -> and(proper X1, proper X2),
                 proper tt() -> ok tt(),
         proper plus(X1, X2) -> plus(proper X1, proper X2),
                  proper 0() -> ok 0(),
                  proper s X -> s proper X,
            proper x(X1, X2) -> x(proper X1, proper X2),
                  top mark X -> top proper X,
                    top ok X -> top active X}
        Open
       
       
       
       
       SCC (6):
        Strict:
         { active# and(X1, X2) -> active# X1,
          active# plus(X1, X2) -> active# X1,
          active# plus(X1, X2) -> active# X2,
                   active# s X -> active# X,
             active# x(X1, X2) -> active# X1,
             active# x(X1, X2) -> active# X2}
        Weak:
        { active and(X1, X2) -> and(active X1, X2),
         active and(tt(), X) -> mark X,
         active plus(N, 0()) -> mark N,
         active plus(N, s M) -> mark s plus(N, M),
         active plus(X1, X2) -> plus(X1, active X2),
         active plus(X1, X2) -> plus(active X1, X2),
                  active s X -> s active X,
            active x(N, 0()) -> mark 0(),
            active x(N, s M) -> mark plus(x(N, M), N),
            active x(X1, X2) -> x(X1, active X2),
            active x(X1, X2) -> x(active X1, X2),
            and(mark X1, X2) -> mark and(X1, X2),
           and(ok X1, ok X2) -> ok and(X1, X2),
           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),
                    s mark X -> mark s X,
                      s ok X -> ok s X,
              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 and(X1, X2) -> and(proper X1, proper X2),
                 proper tt() -> ok tt(),
         proper plus(X1, X2) -> plus(proper X1, proper X2),
                  proper 0() -> ok 0(),
                  proper s X -> s proper X,
            proper x(X1, X2) -> x(proper X1, proper X2),
                  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:
        { active and(X1, X2) -> and(active X1, X2),
         active and(tt(), X) -> mark X,
         active plus(N, 0()) -> mark N,
         active plus(N, s M) -> mark s plus(N, M),
         active plus(X1, X2) -> plus(X1, active X2),
         active plus(X1, X2) -> plus(active X1, X2),
                  active s X -> s active X,
            active x(N, 0()) -> mark 0(),
            active x(N, s M) -> mark plus(x(N, M), N),
            active x(X1, X2) -> x(X1, active X2),
            active x(X1, X2) -> x(active X1, X2),
            and(mark X1, X2) -> mark and(X1, X2),
           and(ok X1, ok X2) -> ok and(X1, X2),
           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),
                    s mark X -> mark s X,
                      s ok X -> ok s X,
              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 and(X1, X2) -> and(proper X1, proper X2),
                 proper tt() -> ok tt(),
         proper plus(X1, X2) -> plus(proper X1, proper X2),
                  proper 0() -> ok 0(),
                  proper s X -> s proper X,
            proper x(X1, X2) -> x(proper X1, proper X2),
                  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:
        { active and(X1, X2) -> and(active X1, X2),
         active and(tt(), X) -> mark X,
         active plus(N, 0()) -> mark N,
         active plus(N, s M) -> mark s plus(N, M),
         active plus(X1, X2) -> plus(X1, active X2),
         active plus(X1, X2) -> plus(active X1, X2),
                  active s X -> s active X,
            active x(N, 0()) -> mark 0(),
            active x(N, s M) -> mark plus(x(N, M), N),
            active x(X1, X2) -> x(X1, active X2),
            active x(X1, X2) -> x(active X1, X2),
            and(mark X1, X2) -> mark and(X1, X2),
           and(ok X1, ok X2) -> ok and(X1, X2),
           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),
                    s mark X -> mark s X,
                      s ok X -> ok s X,
              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 and(X1, X2) -> and(proper X1, proper X2),
                 proper tt() -> ok tt(),
         proper plus(X1, X2) -> plus(proper X1, proper X2),
                  proper 0() -> ok 0(),
                  proper s X -> s proper X,
            proper x(X1, X2) -> x(proper X1, proper X2),
                  top mark X -> top proper X,
                    top ok X -> top active X}
        Open
       
       SCC (2):
        Strict:
         {s# mark X -> s# X,
            s# ok X -> s# X}
        Weak:
        { active and(X1, X2) -> and(active X1, X2),
         active and(tt(), X) -> mark X,
         active plus(N, 0()) -> mark N,
         active plus(N, s M) -> mark s plus(N, M),
         active plus(X1, X2) -> plus(X1, active X2),
         active plus(X1, X2) -> plus(active X1, X2),
                  active s X -> s active X,
            active x(N, 0()) -> mark 0(),
            active x(N, s M) -> mark plus(x(N, M), N),
            active x(X1, X2) -> x(X1, active X2),
            active x(X1, X2) -> x(active X1, X2),
            and(mark X1, X2) -> mark and(X1, X2),
           and(ok X1, ok X2) -> ok and(X1, X2),
           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),
                    s mark X -> mark s X,
                      s ok X -> ok s X,
              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 and(X1, X2) -> and(proper X1, proper X2),
                 proper tt() -> ok tt(),
         proper plus(X1, X2) -> plus(proper X1, proper X2),
                  proper 0() -> ok 0(),
                  proper s X -> s proper X,
            proper x(X1, X2) -> x(proper X1, proper X2),
                  top mark X -> top proper X,
                    top ok X -> top active X}
        Open
       
       
       SCC (2):
        Strict:
         { and#(mark X1, X2) -> and#(X1, X2),
          and#(ok X1, ok X2) -> and#(X1, X2)}
        Weak:
        { active and(X1, X2) -> and(active X1, X2),
         active and(tt(), X) -> mark X,
         active plus(N, 0()) -> mark N,
         active plus(N, s M) -> mark s plus(N, M),
         active plus(X1, X2) -> plus(X1, active X2),
         active plus(X1, X2) -> plus(active X1, X2),
                  active s X -> s active X,
            active x(N, 0()) -> mark 0(),
            active x(N, s M) -> mark plus(x(N, M), N),
            active x(X1, X2) -> x(X1, active X2),
            active x(X1, X2) -> x(active X1, X2),
            and(mark X1, X2) -> mark and(X1, X2),
           and(ok X1, ok X2) -> ok and(X1, X2),
           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),
                    s mark X -> mark s X,
                      s ok X -> ok s X,
              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 and(X1, X2) -> and(proper X1, proper X2),
                 proper tt() -> ok tt(),
         proper plus(X1, X2) -> plus(proper X1, proper X2),
                  proper 0() -> ok 0(),
                  proper s X -> s proper X,
            proper x(X1, X2) -> x(proper X1, proper X2),
                  top mark X -> top proper X,
                    top ok X -> top active X}
        Open