MAYBE
Time: 0.005405
TRS:
 {             pred s X -> X,
          minus(X, s Y) -> pred minus(X, Y),
          minus(X, 0()) -> X,
           le(s X, s Y) -> le(X, Y),
           le(s X, 0()) -> false(),
             le(0(), Y) -> true(),
          gcd(s X, s Y) -> if(le(Y, X), s X, s Y),
          gcd(s X, 0()) -> s X,
            gcd(0(), Y) -> 0(),
  if(false(), s X, s Y) -> gcd(minus(Y, X), s X),
   if(true(), s X, s Y) -> gcd(minus(X, Y), s Y)}
 DP:
  DP:
   {        minus#(X, s Y) -> pred# minus(X, Y),
            minus#(X, s Y) -> minus#(X, Y),
             le#(s X, s Y) -> le#(X, Y),
            gcd#(s X, s Y) -> le#(Y, X),
            gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y),
    if#(false(), s X, s Y) -> minus#(Y, X),
    if#(false(), s X, s Y) -> gcd#(minus(Y, X), s X),
     if#(true(), s X, s Y) -> minus#(X, Y),
     if#(true(), s X, s Y) -> gcd#(minus(X, Y), s Y)}
  TRS:
  {             pred s X -> X,
           minus(X, s Y) -> pred minus(X, Y),
           minus(X, 0()) -> X,
            le(s X, s Y) -> le(X, Y),
            le(s X, 0()) -> false(),
              le(0(), Y) -> true(),
           gcd(s X, s Y) -> if(le(Y, X), s X, s Y),
           gcd(s X, 0()) -> s X,
             gcd(0(), Y) -> 0(),
   if(false(), s X, s Y) -> gcd(minus(Y, X), s X),
    if(true(), s X, s Y) -> gcd(minus(X, Y), s Y)}
  UR:
   {     pred s X -> X,
    minus(X, s Y) -> pred minus(X, Y),
    minus(X, 0()) -> X,
     le(s X, s Y) -> le(X, Y),
     le(s X, 0()) -> false(),
       le(0(), Y) -> true(),
          a(x, y) -> x,
          a(x, y) -> y}
   EDG:
    {(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))
     (if#(false(), s X, s Y) -> gcd#(minus(Y, X), s X), gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y))
     (if#(false(), s X, s Y) -> gcd#(minus(Y, X), s X), gcd#(s X, s Y) -> le#(Y, X))
     (if#(true(), s X, s Y) -> gcd#(minus(X, Y), s Y), gcd#(s X, s Y) -> le#(Y, X))
     (if#(true(), s X, s Y) -> gcd#(minus(X, Y), s Y), gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y))
     (gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y), if#(false(), s X, s Y) -> minus#(Y, X))
     (gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y), if#(false(), s X, s Y) -> gcd#(minus(Y, X), s X))
     (gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y), if#(true(), s X, s Y) -> minus#(X, Y))
     (gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y), if#(true(), s X, s Y) -> gcd#(minus(X, Y), s Y))
     (if#(false(), s X, s Y) -> minus#(Y, X), minus#(X, s Y) -> pred# minus(X, Y))
     (if#(false(), s X, s Y) -> minus#(Y, X), minus#(X, s Y) -> minus#(X, Y))
     (if#(true(), s X, s Y) -> minus#(X, Y), minus#(X, s Y) -> pred# minus(X, Y))
     (if#(true(), s 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))
     (minus#(X, s Y) -> minus#(X, Y), minus#(X, s Y) -> minus#(X, Y))}
    EDG:
     {(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))
      (if#(false(), s X, s Y) -> gcd#(minus(Y, X), s X), gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y))
      (if#(false(), s X, s Y) -> gcd#(minus(Y, X), s X), gcd#(s X, s Y) -> le#(Y, X))
      (if#(true(), s X, s Y) -> gcd#(minus(X, Y), s Y), gcd#(s X, s Y) -> le#(Y, X))
      (if#(true(), s X, s Y) -> gcd#(minus(X, Y), s Y), gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y))
      (gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y), if#(false(), s X, s Y) -> minus#(Y, X))
      (gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y), if#(false(), s X, s Y) -> gcd#(minus(Y, X), s X))
      (gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y), if#(true(), s X, s Y) -> minus#(X, Y))
      (gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y), if#(true(), s X, s Y) -> gcd#(minus(X, Y), s Y))
      (if#(false(), s X, s Y) -> minus#(Y, X), minus#(X, s Y) -> pred# minus(X, Y))
      (if#(false(), s X, s Y) -> minus#(Y, X), minus#(X, s Y) -> minus#(X, Y))
      (if#(true(), s X, s Y) -> minus#(X, Y), minus#(X, s Y) -> pred# minus(X, Y))
      (if#(true(), s 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))
      (minus#(X, s Y) -> minus#(X, Y), minus#(X, s Y) -> minus#(X, Y))}
     EDG:
      {(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))
       (if#(false(), s X, s Y) -> gcd#(minus(Y, X), s X), gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y))
       (if#(false(), s X, s Y) -> gcd#(minus(Y, X), s X), gcd#(s X, s Y) -> le#(Y, X))
       (if#(true(), s X, s Y) -> gcd#(minus(X, Y), s Y), gcd#(s X, s Y) -> le#(Y, X))
       (if#(true(), s X, s Y) -> gcd#(minus(X, Y), s Y), gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y))
       (gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y), if#(false(), s X, s Y) -> minus#(Y, X))
       (gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y), if#(false(), s X, s Y) -> gcd#(minus(Y, X), s X))
       (gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y), if#(true(), s X, s Y) -> minus#(X, Y))
       (gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y), if#(true(), s X, s Y) -> gcd#(minus(X, Y), s Y))
       (if#(false(), s X, s Y) -> minus#(Y, X), minus#(X, s Y) -> pred# minus(X, Y))
       (if#(false(), s X, s Y) -> minus#(Y, X), minus#(X, s Y) -> minus#(X, Y))
       (if#(true(), s X, s Y) -> minus#(X, Y), minus#(X, s Y) -> pred# minus(X, Y))
       (if#(true(), s 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))
       (minus#(X, s Y) -> minus#(X, Y), minus#(X, s Y) -> minus#(X, Y))}
      EDG:
       {(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))
        (if#(false(), s X, s Y) -> gcd#(minus(Y, X), s X), gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y))
        (if#(false(), s X, s Y) -> gcd#(minus(Y, X), s X), gcd#(s X, s Y) -> le#(Y, X))
        (if#(true(), s X, s Y) -> gcd#(minus(X, Y), s Y), gcd#(s X, s Y) -> le#(Y, X))
        (if#(true(), s X, s Y) -> gcd#(minus(X, Y), s Y), gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y))
        (gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y), if#(false(), s X, s Y) -> minus#(Y, X))
        (gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y), if#(false(), s X, s Y) -> gcd#(minus(Y, X), s X))
        (gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y), if#(true(), s X, s Y) -> minus#(X, Y))
        (gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y), if#(true(), s X, s Y) -> gcd#(minus(X, Y), s Y))
        (if#(false(), s X, s Y) -> minus#(Y, X), minus#(X, s Y) -> pred# minus(X, Y))
        (if#(false(), s X, s Y) -> minus#(Y, X), minus#(X, s Y) -> minus#(X, Y))
        (if#(true(), s X, s Y) -> minus#(X, Y), minus#(X, s Y) -> pred# minus(X, Y))
        (if#(true(), s 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))
        (minus#(X, s Y) -> minus#(X, Y), minus#(X, s Y) -> minus#(X, Y))}
       STATUS:
        arrows: 0.802469
        SCCS (3):
         Scc:
          {        gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y),
           if#(false(), s X, s Y) -> gcd#(minus(Y, X), s X),
            if#(true(), s X, s Y) -> gcd#(minus(X, Y), s Y)}
         Scc:
          {le#(s X, s Y) -> le#(X, Y)}
         Scc:
          {minus#(X, s Y) -> minus#(X, Y)}
         
         SCC (3):
          Strict:
           {        gcd#(s X, s Y) -> if#(le(Y, X), s X, s Y),
            if#(false(), s X, s Y) -> gcd#(minus(Y, X), s X),
             if#(true(), s X, s Y) -> gcd#(minus(X, Y), s Y)}
          Weak:
          {             pred s X -> X,
                   minus(X, s Y) -> pred minus(X, Y),
                   minus(X, 0()) -> X,
                    le(s X, s Y) -> le(X, Y),
                    le(s X, 0()) -> false(),
                      le(0(), Y) -> true(),
                   gcd(s X, s Y) -> if(le(Y, X), s X, s Y),
                   gcd(s X, 0()) -> s X,
                     gcd(0(), Y) -> 0(),
           if(false(), s X, s Y) -> gcd(minus(Y, X), s X),
            if(true(), s X, s Y) -> gcd(minus(X, Y), s Y)}
          Open
         
         
         
         SCC (1):
          Strict:
           {le#(s X, s Y) -> le#(X, Y)}
          Weak:
          {             pred s X -> X,
                   minus(X, s Y) -> pred minus(X, Y),
                   minus(X, 0()) -> X,
                    le(s X, s Y) -> le(X, Y),
                    le(s X, 0()) -> false(),
                      le(0(), Y) -> true(),
                   gcd(s X, s Y) -> if(le(Y, X), s X, s Y),
                   gcd(s X, 0()) -> s X,
                     gcd(0(), Y) -> 0(),
           if(false(), s X, s Y) -> gcd(minus(Y, X), s X),
            if(true(), s X, s Y) -> gcd(minus(X, Y), s Y)}
          Open
         SCC (1):
          Strict:
           {minus#(X, s Y) -> minus#(X, Y)}
          Weak:
          {             pred s X -> X,
                   minus(X, s Y) -> pred minus(X, Y),
                   minus(X, 0()) -> X,
                    le(s X, s Y) -> le(X, Y),
                    le(s X, 0()) -> false(),
                      le(0(), Y) -> true(),
                   gcd(s X, s Y) -> if(le(Y, X), s X, s Y),
                   gcd(s X, 0()) -> s X,
                     gcd(0(), Y) -> 0(),
           if(false(), s X, s Y) -> gcd(minus(Y, X), s X),
            if(true(), s X, s Y) -> gcd(minus(X, Y), s Y)}
          Open