MAYBE
Time: 0.001927
TRS:
 {cond(false(), x, y) -> 0(),
   cond(true(), x, y) -> s minus(x, s y),
           gt(0(), v) -> false(),
         gt(s u, 0()) -> true(),
         gt(s u, s v) -> gt(u, v),
          minus(x, y) -> cond(gt(x, y), x, y)}
 DP:
  DP:
   {cond#(true(), x, y) -> minus#(x, s y),
          gt#(s u, s v) -> gt#(u, v),
           minus#(x, y) -> cond#(gt(x, y), x, y),
           minus#(x, y) -> gt#(x, y)}
  TRS:
  {cond(false(), x, y) -> 0(),
    cond(true(), x, y) -> s minus(x, s y),
            gt(0(), v) -> false(),
          gt(s u, 0()) -> true(),
          gt(s u, s v) -> gt(u, v),
           minus(x, y) -> cond(gt(x, y), x, y)}
  UR:
   {  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:
    {(cond#(true(), x, y) -> minus#(x, s y), minus#(x, y) -> gt#(x, y))
     (cond#(true(), x, y) -> minus#(x, s y), minus#(x, y) -> cond#(gt(x, y), x, y))
     (minus#(x, y) -> gt#(x, y), gt#(s u, s v) -> gt#(u, v))
     (gt#(s u, s v) -> gt#(u, v), gt#(s u, s v) -> gt#(u, v))
     (minus#(x, y) -> cond#(gt(x, y), x, y), cond#(true(), x, y) -> minus#(x, s y))}
    EDG:
     {(cond#(true(), x, y) -> minus#(x, s y), minus#(x, y) -> gt#(x, y))
      (cond#(true(), x, y) -> minus#(x, s y), minus#(x, y) -> cond#(gt(x, y), x, y))
      (minus#(x, y) -> gt#(x, y), gt#(s u, s v) -> gt#(u, v))
      (gt#(s u, s v) -> gt#(u, v), gt#(s u, s v) -> gt#(u, v))
      (minus#(x, y) -> cond#(gt(x, y), x, y), cond#(true(), x, y) -> minus#(x, s y))}
     EDG:
      {(cond#(true(), x, y) -> minus#(x, s y), minus#(x, y) -> gt#(x, y))
       (cond#(true(), x, y) -> minus#(x, s y), minus#(x, y) -> cond#(gt(x, y), x, y))
       (minus#(x, y) -> gt#(x, y), gt#(s u, s v) -> gt#(u, v))
       (gt#(s u, s v) -> gt#(u, v), gt#(s u, s v) -> gt#(u, v))
       (minus#(x, y) -> cond#(gt(x, y), x, y), cond#(true(), x, y) -> minus#(x, s y))}
      EDG:
       {(cond#(true(), x, y) -> minus#(x, s y), minus#(x, y) -> gt#(x, y))
        (cond#(true(), x, y) -> minus#(x, s y), minus#(x, y) -> cond#(gt(x, y), x, y))
        (minus#(x, y) -> gt#(x, y), gt#(s u, s v) -> gt#(u, v))
        (gt#(s u, s v) -> gt#(u, v), gt#(s u, s v) -> gt#(u, v))
        (minus#(x, y) -> cond#(gt(x, y), x, y), cond#(true(), x, y) -> minus#(x, s y))}
       STATUS:
        arrows: 0.687500
        SCCS (2):
         Scc:
          {cond#(true(), x, y) -> minus#(x, s y),
                  minus#(x, y) -> cond#(gt(x, y), x, y)}
         Scc:
          {gt#(s u, s v) -> gt#(u, v)}
         
         SCC (2):
          Strict:
           {cond#(true(), x, y) -> minus#(x, s y),
                   minus#(x, y) -> cond#(gt(x, y), x, y)}
          Weak:
          {cond(false(), x, y) -> 0(),
            cond(true(), x, y) -> s minus(x, s y),
                    gt(0(), v) -> false(),
                  gt(s u, 0()) -> true(),
                  gt(s u, s v) -> gt(u, v),
                   minus(x, y) -> cond(gt(x, y), x, y)}
          Open
         
         SCC (1):
          Strict:
           {gt#(s u, s v) -> gt#(u, v)}
          Weak:
          {cond(false(), x, y) -> 0(),
            cond(true(), x, y) -> s minus(x, s y),
                    gt(0(), v) -> false(),
                  gt(s u, 0()) -> true(),
                  gt(s u, s v) -> gt(u, v),
                   minus(x, y) -> cond(gt(x, y), x, y)}
          Open