MAYBE
Time: 0.005295
TRS:
 {               le(0(), y) -> true(),
               le(s x, 0()) -> false(),
               le(s x, s y) -> le(x, y),
                   pred s x -> x,
              minus(x, 0()) -> x,
              minus(x, s y) -> pred minus(x, y),
                gcd(0(), y) -> y,
              gcd(s x, 0()) -> s x,
              gcd(s x, s y) -> if_gcd(le(y, x), s x, s y),
   if_gcd(true(), s x, s y) -> gcd(minus(x, y), s y),
  if_gcd(false(), s x, s y) -> gcd(minus(y, x), s x)}
 DP:
  DP:
   {             le#(s x, s y) -> le#(x, y),
                minus#(x, s y) -> pred# minus(x, y),
                minus#(x, s y) -> minus#(x, y),
                gcd#(s x, s y) -> le#(y, x),
                gcd#(s x, s y) -> if_gcd#(le(y, x), s x, s y),
     if_gcd#(true(), s x, s y) -> minus#(x, y),
     if_gcd#(true(), s x, s y) -> gcd#(minus(x, y), s y),
    if_gcd#(false(), s x, s y) -> minus#(y, x),
    if_gcd#(false(), s x, s y) -> gcd#(minus(y, x), s x)}
  TRS:
  {               le(0(), y) -> true(),
                le(s x, 0()) -> false(),
                le(s x, s y) -> le(x, y),
                    pred s x -> x,
               minus(x, 0()) -> x,
               minus(x, s y) -> pred minus(x, y),
                 gcd(0(), y) -> y,
               gcd(s x, 0()) -> s x,
               gcd(s x, s y) -> if_gcd(le(y, x), s x, s y),
    if_gcd(true(), s x, s y) -> gcd(minus(x, y), s y),
   if_gcd(false(), s x, s y) -> gcd(minus(y, x), s x)}
  UR:
   {   le(0(), y) -> true(),
     le(s x, 0()) -> false(),
     le(s x, s y) -> le(x, y),
         pred s x -> x,
    minus(x, 0()) -> x,
    minus(x, s y) -> pred minus(x, y),
          a(z, w) -> z,
          a(z, w) -> w}
   EDG:
    {(if_gcd#(false(), s x, s y) -> minus#(y, x), minus#(x, s y) -> minus#(x, y))
     (if_gcd#(false(), s x, s y) -> minus#(y, x), minus#(x, s y) -> pred# minus(x, y))
     (minus#(x, s y) -> minus#(x, y), minus#(x, s y) -> minus#(x, y))
     (minus#(x, s y) -> minus#(x, y), minus#(x, s y) -> pred# minus(x, y))
     (if_gcd#(true(), s x, s y) -> gcd#(minus(x, y), s y), gcd#(s x, s y) -> if_gcd#(le(y, x), s x, s y))
     (if_gcd#(true(), s x, s y) -> gcd#(minus(x, y), s y), gcd#(s x, s y) -> le#(y, x))
     (if_gcd#(false(), s x, s y) -> gcd#(minus(y, x), s x), gcd#(s x, s y) -> le#(y, x))
     (if_gcd#(false(), s x, s y) -> gcd#(minus(y, x), s x), gcd#(s x, s y) -> if_gcd#(le(y, x), s x, s y))
     (gcd#(s x, s y) -> if_gcd#(le(y, x), s x, s y), if_gcd#(true(), s x, s y) -> minus#(x, y))
     (gcd#(s x, s y) -> if_gcd#(le(y, x), s x, s y), if_gcd#(true(), s x, s y) -> gcd#(minus(x, y), s y))
     (gcd#(s x, s y) -> if_gcd#(le(y, x), s x, s y), if_gcd#(false(), s x, s y) -> minus#(y, x))
     (gcd#(s x, s y) -> if_gcd#(le(y, x), s x, s y), if_gcd#(false(), s x, s y) -> gcd#(minus(y, x), s x))
     (if_gcd#(true(), s x, s y) -> minus#(x, y), minus#(x, s y) -> pred# minus(x, y))
     (if_gcd#(true(), s x, s y) -> minus#(x, y), minus#(x, s y) -> minus#(x, y))
     (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
     (gcd#(s x, s y) -> le#(y, x), le#(s x, s y) -> le#(x, y))}
    EDG:
     {(if_gcd#(false(), s x, s y) -> minus#(y, x), minus#(x, s y) -> minus#(x, y))
      (if_gcd#(false(), s x, s y) -> minus#(y, x), minus#(x, s y) -> pred# minus(x, y))
      (minus#(x, s y) -> minus#(x, y), minus#(x, s y) -> minus#(x, y))
      (minus#(x, s y) -> minus#(x, y), minus#(x, s y) -> pred# minus(x, y))
      (if_gcd#(true(), s x, s y) -> gcd#(minus(x, y), s y), gcd#(s x, s y) -> if_gcd#(le(y, x), s x, s y))
      (if_gcd#(true(), s x, s y) -> gcd#(minus(x, y), s y), gcd#(s x, s y) -> le#(y, x))
      (if_gcd#(false(), s x, s y) -> gcd#(minus(y, x), s x), gcd#(s x, s y) -> le#(y, x))
      (if_gcd#(false(), s x, s y) -> gcd#(minus(y, x), s x), gcd#(s x, s y) -> if_gcd#(le(y, x), s x, s y))
      (gcd#(s x, s y) -> if_gcd#(le(y, x), s x, s y), if_gcd#(true(), s x, s y) -> minus#(x, y))
      (gcd#(s x, s y) -> if_gcd#(le(y, x), s x, s y), if_gcd#(true(), s x, s y) -> gcd#(minus(x, y), s y))
      (gcd#(s x, s y) -> if_gcd#(le(y, x), s x, s y), if_gcd#(false(), s x, s y) -> minus#(y, x))
      (gcd#(s x, s y) -> if_gcd#(le(y, x), s x, s y), if_gcd#(false(), s x, s y) -> gcd#(minus(y, x), s x))
      (if_gcd#(true(), s x, s y) -> minus#(x, y), minus#(x, s y) -> pred# minus(x, y))
      (if_gcd#(true(), s x, s y) -> minus#(x, y), minus#(x, s y) -> minus#(x, y))
      (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
      (gcd#(s x, s y) -> le#(y, x), le#(s x, s y) -> le#(x, y))}
     EDG:
      {(if_gcd#(false(), s x, s y) -> minus#(y, x), minus#(x, s y) -> minus#(x, y))
       (if_gcd#(false(), s x, s y) -> minus#(y, x), minus#(x, s y) -> pred# minus(x, y))
       (minus#(x, s y) -> minus#(x, y), minus#(x, s y) -> minus#(x, y))
       (minus#(x, s y) -> minus#(x, y), minus#(x, s y) -> pred# minus(x, y))
       (if_gcd#(true(), s x, s y) -> gcd#(minus(x, y), s y), gcd#(s x, s y) -> if_gcd#(le(y, x), s x, s y))
       (if_gcd#(true(), s x, s y) -> gcd#(minus(x, y), s y), gcd#(s x, s y) -> le#(y, x))
       (if_gcd#(false(), s x, s y) -> gcd#(minus(y, x), s x), gcd#(s x, s y) -> le#(y, x))
       (if_gcd#(false(), s x, s y) -> gcd#(minus(y, x), s x), gcd#(s x, s y) -> if_gcd#(le(y, x), s x, s y))
       (gcd#(s x, s y) -> if_gcd#(le(y, x), s x, s y), if_gcd#(true(), s x, s y) -> minus#(x, y))
       (gcd#(s x, s y) -> if_gcd#(le(y, x), s x, s y), if_gcd#(true(), s x, s y) -> gcd#(minus(x, y), s y))
       (gcd#(s x, s y) -> if_gcd#(le(y, x), s x, s y), if_gcd#(false(), s x, s y) -> minus#(y, x))
       (gcd#(s x, s y) -> if_gcd#(le(y, x), s x, s y), if_gcd#(false(), s x, s y) -> gcd#(minus(y, x), s x))
       (if_gcd#(true(), s x, s y) -> minus#(x, y), minus#(x, s y) -> pred# minus(x, y))
       (if_gcd#(true(), s x, s y) -> minus#(x, y), minus#(x, s y) -> minus#(x, y))
       (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
       (gcd#(s x, s y) -> le#(y, x), le#(s x, s y) -> le#(x, y))}
      EDG:
       {(if_gcd#(false(), s x, s y) -> minus#(y, x), minus#(x, s y) -> minus#(x, y))
        (if_gcd#(false(), s x, s y) -> minus#(y, x), minus#(x, s y) -> pred# minus(x, y))
        (minus#(x, s y) -> minus#(x, y), minus#(x, s y) -> minus#(x, y))
        (minus#(x, s y) -> minus#(x, y), minus#(x, s y) -> pred# minus(x, y))
        (if_gcd#(true(), s x, s y) -> gcd#(minus(x, y), s y), gcd#(s x, s y) -> if_gcd#(le(y, x), s x, s y))
        (if_gcd#(true(), s x, s y) -> gcd#(minus(x, y), s y), gcd#(s x, s y) -> le#(y, x))
        (if_gcd#(false(), s x, s y) -> gcd#(minus(y, x), s x), gcd#(s x, s y) -> le#(y, x))
        (if_gcd#(false(), s x, s y) -> gcd#(minus(y, x), s x), gcd#(s x, s y) -> if_gcd#(le(y, x), s x, s y))
        (gcd#(s x, s y) -> if_gcd#(le(y, x), s x, s y), if_gcd#(true(), s x, s y) -> minus#(x, y))
        (gcd#(s x, s y) -> if_gcd#(le(y, x), s x, s y), if_gcd#(true(), s x, s y) -> gcd#(minus(x, y), s y))
        (gcd#(s x, s y) -> if_gcd#(le(y, x), s x, s y), if_gcd#(false(), s x, s y) -> minus#(y, x))
        (gcd#(s x, s y) -> if_gcd#(le(y, x), s x, s y), if_gcd#(false(), s x, s y) -> gcd#(minus(y, x), s x))
        (if_gcd#(true(), s x, s y) -> minus#(x, y), minus#(x, s y) -> pred# minus(x, y))
        (if_gcd#(true(), s x, s y) -> minus#(x, y), minus#(x, s y) -> minus#(x, y))
        (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
        (gcd#(s x, s y) -> le#(y, x), le#(s x, s y) -> le#(x, y))}
       STATUS:
        arrows: 0.802469
        SCCS (3):
         Scc:
          {            gcd#(s x, s y) -> if_gcd#(le(y, x), s x, s y),
            if_gcd#(true(), s x, s y) -> gcd#(minus(x, y), s y),
           if_gcd#(false(), s x, s y) -> gcd#(minus(y, x), s x)}
         Scc:
          {minus#(x, s y) -> minus#(x, y)}
         Scc:
          {le#(s x, s y) -> le#(x, y)}
         
         SCC (3):
          Strict:
           {            gcd#(s x, s y) -> if_gcd#(le(y, x), s x, s y),
             if_gcd#(true(), s x, s y) -> gcd#(minus(x, y), s y),
            if_gcd#(false(), s x, s y) -> gcd#(minus(y, x), s x)}
          Weak:
          {               le(0(), y) -> true(),
                        le(s x, 0()) -> false(),
                        le(s x, s y) -> le(x, y),
                            pred s x -> x,
                       minus(x, 0()) -> x,
                       minus(x, s y) -> pred minus(x, y),
                         gcd(0(), y) -> y,
                       gcd(s x, 0()) -> s x,
                       gcd(s x, s y) -> if_gcd(le(y, x), s x, s y),
            if_gcd(true(), s x, s y) -> gcd(minus(x, y), s y),
           if_gcd(false(), s x, s y) -> gcd(minus(y, x), s x)}
          Open
         
         
         SCC (1):
          Strict:
           {minus#(x, s y) -> minus#(x, y)}
          Weak:
          {               le(0(), y) -> true(),
                        le(s x, 0()) -> false(),
                        le(s x, s y) -> le(x, y),
                            pred s x -> x,
                       minus(x, 0()) -> x,
                       minus(x, s y) -> pred minus(x, y),
                         gcd(0(), y) -> y,
                       gcd(s x, 0()) -> s x,
                       gcd(s x, s y) -> if_gcd(le(y, x), s x, s y),
            if_gcd(true(), s x, s y) -> gcd(minus(x, y), s y),
           if_gcd(false(), s x, s y) -> gcd(minus(y, x), s x)}
          Open
         
         
         SCC (1):
          Strict:
           {le#(s x, s y) -> le#(x, y)}
          Weak:
          {               le(0(), y) -> true(),
                        le(s x, 0()) -> false(),
                        le(s x, s y) -> le(x, y),
                            pred s x -> x,
                       minus(x, 0()) -> x,
                       minus(x, s y) -> pred minus(x, y),
                         gcd(0(), y) -> y,
                       gcd(s x, 0()) -> s x,
                       gcd(s x, s y) -> if_gcd(le(y, x), s x, s y),
            if_gcd(true(), s x, s y) -> gcd(minus(x, y), s y),
           if_gcd(false(), s x, s y) -> gcd(minus(y, x), s x)}
          Open