MAYBE
Time: 0.185425
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))}
    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