MAYBE
Time: 0.009253
TRS:
 {          min(x, 0()) -> 0(),
            min(0(), y) -> 0(),
          min(s x, s y) -> s min(x, y),
            max(x, 0()) -> x,
            max(0(), y) -> y,
          max(s x, s y) -> s max(x, y),
          minus(x, 0()) -> x,
        minus(s x, s y) -> s minus(x, y),
          gcd(s x, s y) -> gcd(minus(max(x, y), min(x, transform y)), s min(x, y)),
            transform x -> s s x,
          transform s x -> s s transform x,
   transform cons(x, y) -> y,
   transform cons(x, y) -> cons(cons(x, x), x),
             cons(x, y) -> y,
  cons(x, cons(y, s z)) -> cons(y, x),
  cons(cons(x, z), s y) -> transform x}
 DP:
  DP:
   {        min#(s x, s y) -> min#(x, y),
            max#(s x, s y) -> max#(x, y),
          minus#(s x, s y) -> minus#(x, y),
            gcd#(s x, s y) -> min#(x, y),
            gcd#(s x, s y) -> min#(x, transform y),
            gcd#(s x, s y) -> max#(x, y),
            gcd#(s x, s y) -> minus#(max(x, y), min(x, transform y)),
            gcd#(s x, s y) -> gcd#(minus(max(x, y), min(x, transform y)), s min(x, y)),
            gcd#(s x, s y) -> transform# y,
            transform# s x -> transform# x,
     transform# cons(x, y) -> cons#(x, x),
     transform# cons(x, y) -> cons#(cons(x, x), x),
    cons#(x, cons(y, s z)) -> cons#(y, x),
    cons#(cons(x, z), s y) -> transform# x}
  TRS:
  {          min(x, 0()) -> 0(),
             min(0(), y) -> 0(),
           min(s x, s y) -> s min(x, y),
             max(x, 0()) -> x,
             max(0(), y) -> y,
           max(s x, s y) -> s max(x, y),
           minus(x, 0()) -> x,
         minus(s x, s y) -> s minus(x, y),
           gcd(s x, s y) -> gcd(minus(max(x, y), min(x, transform y)), s min(x, y)),
             transform x -> s s x,
           transform s x -> s s transform x,
    transform cons(x, y) -> y,
    transform cons(x, y) -> cons(cons(x, x), x),
              cons(x, y) -> y,
   cons(x, cons(y, s z)) -> cons(y, x),
   cons(cons(x, z), s y) -> transform x}
  EDG:
   {(cons#(x, cons(y, s z)) -> cons#(y, x), cons#(cons(x, z), s y) -> transform# x)
    (cons#(x, cons(y, s z)) -> cons#(y, x), cons#(x, cons(y, s z)) -> cons#(y, x))
    (gcd#(s x, s y) -> transform# y, transform# cons(x, y) -> cons#(cons(x, x), x))
    (gcd#(s x, s y) -> transform# y, transform# cons(x, y) -> cons#(x, x))
    (gcd#(s x, s y) -> transform# y, transform# s x -> transform# x)
    (max#(s x, s y) -> max#(x, y), max#(s x, s y) -> max#(x, y))
    (gcd#(s x, s y) -> min#(x, y), min#(s x, s y) -> min#(x, y))
    (gcd#(s x, s y) -> minus#(max(x, y), min(x, transform y)), minus#(s x, s y) -> minus#(x, y))
    (gcd#(s x, s y) -> min#(x, transform y), min#(s x, s y) -> min#(x, y))
    (cons#(cons(x, z), s y) -> transform# x, transform# cons(x, y) -> cons#(cons(x, x), x))
    (cons#(cons(x, z), s y) -> transform# x, transform# cons(x, y) -> cons#(x, x))
    (cons#(cons(x, z), s y) -> transform# x, transform# s x -> transform# x)
    (transform# s x -> transform# x, transform# s x -> transform# x)
    (transform# s x -> transform# x, transform# cons(x, y) -> cons#(x, x))
    (transform# s x -> transform# x, transform# cons(x, y) -> cons#(cons(x, x), x))
    (transform# cons(x, y) -> cons#(cons(x, x), x), cons#(x, cons(y, s z)) -> cons#(y, x))
    (transform# cons(x, y) -> cons#(cons(x, x), x), cons#(cons(x, z), s y) -> transform# x)
    (gcd#(s x, s y) -> max#(x, y), max#(s x, s y) -> max#(x, y))
    (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
    (min#(s x, s y) -> min#(x, y), min#(s x, s y) -> min#(x, y))
    (gcd#(s x, s y) -> gcd#(minus(max(x, y), min(x, transform y)), s min(x, y)), gcd#(s x, s y) -> min#(x, y))
    (gcd#(s x, s y) -> gcd#(minus(max(x, y), min(x, transform y)), s min(x, y)), gcd#(s x, s y) -> min#(x, transform y))
    (gcd#(s x, s y) -> gcd#(minus(max(x, y), min(x, transform y)), s min(x, y)), gcd#(s x, s y) -> max#(x, y))
    (gcd#(s x, s y) -> gcd#(minus(max(x, y), min(x, transform y)), s min(x, y)), gcd#(s x, s y) -> minus#(max(x, y), min(x, transform y)))
    (gcd#(s x, s y) -> gcd#(minus(max(x, y), min(x, transform y)), s min(x, y)), gcd#(s x, s y) -> gcd#(minus(max(x, y), min(x, transform y)), s min(x, y)))
    (gcd#(s x, s y) -> gcd#(minus(max(x, y), min(x, transform y)), s min(x, y)), gcd#(s x, s y) -> transform# y)
    (transform# cons(x, y) -> cons#(x, x), cons#(x, cons(y, s z)) -> cons#(y, x))
    (transform# cons(x, y) -> cons#(x, x), cons#(cons(x, z), s y) -> transform# x)}
   STATUS:
    arrows: 0.857143
    SCCS (5):
     Scc:
      {gcd#(s x, s y) -> gcd#(minus(max(x, y), min(x, transform y)), s min(x, y))}
     Scc:
      {minus#(s x, s y) -> minus#(x, y)}
     Scc:
      {max#(s x, s y) -> max#(x, y)}
     Scc:
      {min#(s x, s y) -> min#(x, y)}
     Scc:
      {        transform# s x -> transform# x,
        transform# cons(x, y) -> cons#(x, x),
        transform# cons(x, y) -> cons#(cons(x, x), x),
       cons#(x, cons(y, s z)) -> cons#(y, x),
       cons#(cons(x, z), s y) -> transform# x}
     
     SCC (1):
      Strict:
       {gcd#(s x, s y) -> gcd#(minus(max(x, y), min(x, transform y)), s min(x, y))}
      Weak:
      {          min(x, 0()) -> 0(),
                 min(0(), y) -> 0(),
               min(s x, s y) -> s min(x, y),
                 max(x, 0()) -> x,
                 max(0(), y) -> y,
               max(s x, s y) -> s max(x, y),
               minus(x, 0()) -> x,
             minus(s x, s y) -> s minus(x, y),
               gcd(s x, s y) -> gcd(minus(max(x, y), min(x, transform y)), s min(x, y)),
                 transform x -> s s x,
               transform s x -> s s transform x,
        transform cons(x, y) -> y,
        transform cons(x, y) -> cons(cons(x, x), x),
                  cons(x, y) -> y,
       cons(x, cons(y, s z)) -> cons(y, x),
       cons(cons(x, z), s y) -> transform x}
      Open
     
     
     SCC (1):
      Strict:
       {minus#(s x, s y) -> minus#(x, y)}
      Weak:
      {          min(x, 0()) -> 0(),
                 min(0(), y) -> 0(),
               min(s x, s y) -> s min(x, y),
                 max(x, 0()) -> x,
                 max(0(), y) -> y,
               max(s x, s y) -> s max(x, y),
               minus(x, 0()) -> x,
             minus(s x, s y) -> s minus(x, y),
               gcd(s x, s y) -> gcd(minus(max(x, y), min(x, transform y)), s min(x, y)),
                 transform x -> s s x,
               transform s x -> s s transform x,
        transform cons(x, y) -> y,
        transform cons(x, y) -> cons(cons(x, x), x),
                  cons(x, y) -> y,
       cons(x, cons(y, s z)) -> cons(y, x),
       cons(cons(x, z), s y) -> transform x}
      Open
     
     SCC (1):
      Strict:
       {max#(s x, s y) -> max#(x, y)}
      Weak:
      {          min(x, 0()) -> 0(),
                 min(0(), y) -> 0(),
               min(s x, s y) -> s min(x, y),
                 max(x, 0()) -> x,
                 max(0(), y) -> y,
               max(s x, s y) -> s max(x, y),
               minus(x, 0()) -> x,
             minus(s x, s y) -> s minus(x, y),
               gcd(s x, s y) -> gcd(minus(max(x, y), min(x, transform y)), s min(x, y)),
                 transform x -> s s x,
               transform s x -> s s transform x,
        transform cons(x, y) -> y,
        transform cons(x, y) -> cons(cons(x, x), x),
                  cons(x, y) -> y,
       cons(x, cons(y, s z)) -> cons(y, x),
       cons(cons(x, z), s y) -> transform x}
      Open
     
     
     SCC (1):
      Strict:
       {min#(s x, s y) -> min#(x, y)}
      Weak:
      {          min(x, 0()) -> 0(),
                 min(0(), y) -> 0(),
               min(s x, s y) -> s min(x, y),
                 max(x, 0()) -> x,
                 max(0(), y) -> y,
               max(s x, s y) -> s max(x, y),
               minus(x, 0()) -> x,
             minus(s x, s y) -> s minus(x, y),
               gcd(s x, s y) -> gcd(minus(max(x, y), min(x, transform y)), s min(x, y)),
                 transform x -> s s x,
               transform s x -> s s transform x,
        transform cons(x, y) -> y,
        transform cons(x, y) -> cons(cons(x, x), x),
                  cons(x, y) -> y,
       cons(x, cons(y, s z)) -> cons(y, x),
       cons(cons(x, z), s y) -> transform x}
      Open
     SCC (5):
      Strict:
       {        transform# s x -> transform# x,
         transform# cons(x, y) -> cons#(x, x),
         transform# cons(x, y) -> cons#(cons(x, x), x),
        cons#(x, cons(y, s z)) -> cons#(y, x),
        cons#(cons(x, z), s y) -> transform# x}
      Weak:
      {          min(x, 0()) -> 0(),
                 min(0(), y) -> 0(),
               min(s x, s y) -> s min(x, y),
                 max(x, 0()) -> x,
                 max(0(), y) -> y,
               max(s x, s y) -> s max(x, y),
               minus(x, 0()) -> x,
             minus(s x, s y) -> s minus(x, y),
               gcd(s x, s y) -> gcd(minus(max(x, y), min(x, transform y)), s min(x, y)),
                 transform x -> s s x,
               transform s x -> s s transform x,
        transform cons(x, y) -> y,
        transform cons(x, y) -> cons(cons(x, x), x),
                  cons(x, y) -> y,
       cons(x, cons(y, s z)) -> cons(y, x),
       cons(cons(x, z), s y) -> transform x}
      Open