MAYBE
Time: 0.002654
TRS:
 { cond1(true(), x, y) -> 0(),
  cond1(false(), x, y) -> cond2(gt(x, y), x, y),
       equal(0(), 0()) -> true(),
       equal(0(), s y) -> false(),
       equal(s x, 0()) -> false(),
       equal(s x, s y) -> equal(x, y),
            diff(x, y) -> cond1(equal(x, y), x, y),
   cond2(true(), x, y) -> s diff(x, s y),
  cond2(false(), x, y) -> s diff(s x, y),
            gt(0(), v) -> false(),
          gt(s u, 0()) -> true(),
          gt(s u, s v) -> gt(u, v)}
 DP:
  DP:
   {cond1#(false(), x, y) -> cond2#(gt(x, y), x, y),
    cond1#(false(), x, y) -> gt#(x, y),
         equal#(s x, s y) -> equal#(x, y),
              diff#(x, y) -> cond1#(equal(x, y), x, y),
              diff#(x, y) -> equal#(x, y),
     cond2#(true(), x, y) -> diff#(x, s y),
    cond2#(false(), x, y) -> diff#(s x, y),
            gt#(s u, s v) -> gt#(u, v)}
  TRS:
  { cond1(true(), x, y) -> 0(),
   cond1(false(), x, y) -> cond2(gt(x, y), x, y),
        equal(0(), 0()) -> true(),
        equal(0(), s y) -> false(),
        equal(s x, 0()) -> false(),
        equal(s x, s y) -> equal(x, y),
             diff(x, y) -> cond1(equal(x, y), x, y),
    cond2(true(), x, y) -> s diff(x, s y),
   cond2(false(), x, y) -> s diff(s x, y),
             gt(0(), v) -> false(),
           gt(s u, 0()) -> true(),
           gt(s u, s v) -> gt(u, v)}
  UR:
   {equal(0(), 0()) -> true(),
    equal(0(), s y) -> false(),
    equal(s x, 0()) -> false(),
    equal(s x, s y) -> equal(x, y),
         gt(0(), v) -> false(),
       gt(s u, 0()) -> true(),
       gt(s u, s v) -> gt(u, v),
            a(z, w) -> z,
            a(z, w) -> w}
   EDG:
    {(diff#(x, y) -> cond1#(equal(x, y), x, y), cond1#(false(), x, y) -> gt#(x, y))
     (diff#(x, y) -> cond1#(equal(x, y), x, y), cond1#(false(), x, y) -> cond2#(gt(x, y), x, y))
     (cond1#(false(), x, y) -> gt#(x, y), gt#(s u, s v) -> gt#(u, v))
     (diff#(x, y) -> equal#(x, y), equal#(s x, s y) -> equal#(x, y))
     (gt#(s u, s v) -> gt#(u, v), gt#(s u, s v) -> gt#(u, v))
     (cond2#(true(), x, y) -> diff#(x, s y), diff#(x, y) -> cond1#(equal(x, y), x, y))
     (cond2#(true(), x, y) -> diff#(x, s y), diff#(x, y) -> equal#(x, y))
     (equal#(s x, s y) -> equal#(x, y), equal#(s x, s y) -> equal#(x, y))
     (cond2#(false(), x, y) -> diff#(s x, y), diff#(x, y) -> cond1#(equal(x, y), x, y))
     (cond2#(false(), x, y) -> diff#(s x, y), diff#(x, y) -> equal#(x, y))
     (cond1#(false(), x, y) -> cond2#(gt(x, y), x, y), cond2#(true(), x, y) -> diff#(x, s y))
     (cond1#(false(), x, y) -> cond2#(gt(x, y), x, y), cond2#(false(), x, y) -> diff#(s x, y))}
    STATUS:
     arrows: 0.812500
     SCCS (3):
      Scc:
       {cond1#(false(), x, y) -> cond2#(gt(x, y), x, y),
                  diff#(x, y) -> cond1#(equal(x, y), x, y),
         cond2#(true(), x, y) -> diff#(x, s y),
        cond2#(false(), x, y) -> diff#(s x, y)}
      Scc:
       {equal#(s x, s y) -> equal#(x, y)}
      Scc:
       {gt#(s u, s v) -> gt#(u, v)}
      
      SCC (4):
       Strict:
        {cond1#(false(), x, y) -> cond2#(gt(x, y), x, y),
                   diff#(x, y) -> cond1#(equal(x, y), x, y),
          cond2#(true(), x, y) -> diff#(x, s y),
         cond2#(false(), x, y) -> diff#(s x, y)}
       Weak:
       { cond1(true(), x, y) -> 0(),
        cond1(false(), x, y) -> cond2(gt(x, y), x, y),
             equal(0(), 0()) -> true(),
             equal(0(), s y) -> false(),
             equal(s x, 0()) -> false(),
             equal(s x, s y) -> equal(x, y),
                  diff(x, y) -> cond1(equal(x, y), x, y),
         cond2(true(), x, y) -> s diff(x, s y),
        cond2(false(), x, y) -> s diff(s x, y),
                  gt(0(), v) -> false(),
                gt(s u, 0()) -> true(),
                gt(s u, s v) -> gt(u, v)}
       Open
      
      SCC (1):
       Strict:
        {equal#(s x, s y) -> equal#(x, y)}
       Weak:
       { cond1(true(), x, y) -> 0(),
        cond1(false(), x, y) -> cond2(gt(x, y), x, y),
             equal(0(), 0()) -> true(),
             equal(0(), s y) -> false(),
             equal(s x, 0()) -> false(),
             equal(s x, s y) -> equal(x, y),
                  diff(x, y) -> cond1(equal(x, y), x, y),
         cond2(true(), x, y) -> s diff(x, s y),
        cond2(false(), x, y) -> s diff(s x, y),
                  gt(0(), v) -> false(),
                gt(s u, 0()) -> true(),
                gt(s u, s v) -> gt(u, v)}
       Open
      
      SCC (1):
       Strict:
        {gt#(s u, s v) -> gt#(u, v)}
       Weak:
       { cond1(true(), x, y) -> 0(),
        cond1(false(), x, y) -> cond2(gt(x, y), x, y),
             equal(0(), 0()) -> true(),
             equal(0(), s y) -> false(),
             equal(s x, 0()) -> false(),
             equal(s x, s y) -> equal(x, y),
                  diff(x, y) -> cond1(equal(x, y), x, y),
         cond2(true(), x, y) -> s diff(x, s y),
        cond2(false(), x, y) -> s diff(s x, y),
                  gt(0(), v) -> false(),
                gt(s u, 0()) -> true(),
                gt(s u, s v) -> gt(u, v)}
       Open