MAYBE
Time: 0.035153
TRS:
 {                      eq(0(), 0()) -> true(),
                        eq(0(), s x) -> false(),
                        eq(s x, 0()) -> false(),
                        eq(s x, s y) -> eq(x, y),
                          le(0(), y) -> true(),
                        le(s x, 0()) -> false(),
                        le(s x, s y) -> le(x, y),
                       app(nil(), y) -> y,
                   app(add(n, x), y) -> add(n, app(x, y)),
                   min add(n, nil()) -> n,
               min add(n, add(m, x)) -> if_min(le(n, m), add(n, add(m, x))),
   if_min(true(), add(n, add(m, x))) -> min add(n, x),
  if_min(false(), add(n, add(m, x))) -> min add(m, x),
                      head add(n, x) -> n,
                          tail nil() -> nil(),
                      tail add(n, x) -> x,
                          null nil() -> true(),
                      null add(n, x) -> false(),
                        rm(n, nil()) -> nil(),
                    rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)),
         if_rm(true(), n, add(m, x)) -> rm(n, x),
        if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)),
                       mins(x, y, z) -> if(null x, x, y, z),
                           minsort x -> mins(x, nil(), nil()),
                 if(true(), x, y, z) -> z,
                if(false(), x, y, z) -> if2(eq(head x, min x), x, y, z),
                if2(true(), x, y, z) -> mins(app(rm(head x, tail x), y), nil(), app(z, add(head x, nil()))),
               if2(false(), x, y, z) -> mins(tail x, add(head x, y), z)}
 DP:
  DP:
   {                      eq#(s x, s y) -> eq#(x, y),
                          le#(s x, s y) -> le#(x, y),
                     app#(add(n, x), y) -> app#(x, y),
                 min# add(n, add(m, x)) -> le#(n, m),
                 min# add(n, add(m, x)) -> if_min#(le(n, m), add(n, add(m, x))),
     if_min#(true(), add(n, add(m, x))) -> min# add(n, x),
    if_min#(false(), add(n, add(m, x))) -> min# add(m, x),
                      rm#(n, add(m, x)) -> eq#(n, m),
                      rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)),
           if_rm#(true(), n, add(m, x)) -> rm#(n, x),
          if_rm#(false(), n, add(m, x)) -> rm#(n, x),
                         mins#(x, y, z) -> null# x,
                         mins#(x, y, z) -> if#(null x, x, y, z),
                             minsort# x -> mins#(x, nil(), nil()),
                  if#(false(), x, y, z) -> eq#(head x, min x),
                  if#(false(), x, y, z) -> min# x,
                  if#(false(), x, y, z) -> head# x,
                  if#(false(), x, y, z) -> if2#(eq(head x, min x), x, y, z),
                  if2#(true(), x, y, z) -> app#(z, add(head x, nil())),
                  if2#(true(), x, y, z) -> app#(rm(head x, tail x), y),
                  if2#(true(), x, y, z) -> head# x,
                  if2#(true(), x, y, z) -> tail# x,
                  if2#(true(), x, y, z) -> rm#(head x, tail x),
                  if2#(true(), x, y, z) -> mins#(app(rm(head x, tail x), y), nil(), app(z, add(head x, nil()))),
                 if2#(false(), x, y, z) -> head# x,
                 if2#(false(), x, y, z) -> tail# x,
                 if2#(false(), x, y, z) -> mins#(tail x, add(head x, y), z)}
  TRS:
  {                      eq(0(), 0()) -> true(),
                         eq(0(), s x) -> false(),
                         eq(s x, 0()) -> false(),
                         eq(s x, s y) -> eq(x, y),
                           le(0(), y) -> true(),
                         le(s x, 0()) -> false(),
                         le(s x, s y) -> le(x, y),
                        app(nil(), y) -> y,
                    app(add(n, x), y) -> add(n, app(x, y)),
                    min add(n, nil()) -> n,
                min add(n, add(m, x)) -> if_min(le(n, m), add(n, add(m, x))),
    if_min(true(), add(n, add(m, x))) -> min add(n, x),
   if_min(false(), add(n, add(m, x))) -> min add(m, x),
                       head add(n, x) -> n,
                           tail nil() -> nil(),
                       tail add(n, x) -> x,
                           null nil() -> true(),
                       null add(n, x) -> false(),
                         rm(n, nil()) -> nil(),
                     rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)),
          if_rm(true(), n, add(m, x)) -> rm(n, x),
         if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)),
                        mins(x, y, z) -> if(null x, x, y, z),
                            minsort x -> mins(x, nil(), nil()),
                  if(true(), x, y, z) -> z,
                 if(false(), x, y, z) -> if2(eq(head x, min x), x, y, z),
                 if2(true(), x, y, z) -> mins(app(rm(head x, tail x), y), nil(), app(z, add(head x, nil()))),
                if2(false(), x, y, z) -> mins(tail x, add(head x, y), z)}
  EDG:
   {(min# add(n, add(m, x)) -> le#(n, m), le#(s x, s y) -> le#(x, y))
    (if2#(true(), x, y, z) -> app#(rm(head x, tail x), y), app#(add(n, x), y) -> app#(x, y))
    (if_rm#(false(), n, add(m, x)) -> rm#(n, x), rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)))
    (if_rm#(false(), n, add(m, x)) -> rm#(n, x), rm#(n, add(m, x)) -> eq#(n, m))
    (rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)), if_rm#(false(), n, add(m, x)) -> rm#(n, x))
    (rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)), if_rm#(true(), n, add(m, x)) -> rm#(n, x))
    (if2#(true(), x, y, z) -> rm#(head x, tail x), rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)))
    (if2#(true(), x, y, z) -> rm#(head x, tail x), rm#(n, add(m, x)) -> eq#(n, m))
    (if#(false(), x, y, z) -> min# x, min# add(n, add(m, x)) -> if_min#(le(n, m), add(n, add(m, x))))
    (if#(false(), x, y, z) -> min# x, min# add(n, add(m, x)) -> le#(n, m))
    (eq#(s x, s y) -> eq#(x, y), eq#(s x, s y) -> eq#(x, y))
    (app#(add(n, x), y) -> app#(x, y), app#(add(n, x), y) -> app#(x, y))
    (min# add(n, add(m, x)) -> if_min#(le(n, m), add(n, add(m, x))), if_min#(false(), add(n, add(m, x))) -> min# add(m, x))
    (min# add(n, add(m, x)) -> if_min#(le(n, m), add(n, add(m, x))), if_min#(true(), add(n, add(m, x))) -> min# add(n, x))
    (if_min#(false(), add(n, add(m, x))) -> min# add(m, x), min# add(n, add(m, x)) -> if_min#(le(n, m), add(n, add(m, x))))
    (if_min#(false(), add(n, add(m, x))) -> min# add(m, x), min# add(n, add(m, x)) -> le#(n, m))
    (mins#(x, y, z) -> if#(null x, x, y, z), if#(false(), x, y, z) -> if2#(eq(head x, min x), x, y, z))
    (mins#(x, y, z) -> if#(null x, x, y, z), if#(false(), x, y, z) -> head# x)
    (mins#(x, y, z) -> if#(null x, x, y, z), if#(false(), x, y, z) -> min# x)
    (mins#(x, y, z) -> if#(null x, x, y, z), if#(false(), x, y, z) -> eq#(head x, min x))
    (if#(false(), x, y, z) -> if2#(eq(head x, min x), x, y, z), if2#(true(), x, y, z) -> app#(z, add(head x, nil())))
    (if#(false(), x, y, z) -> if2#(eq(head x, min x), x, y, z), if2#(true(), x, y, z) -> app#(rm(head x, tail x), y))
    (if#(false(), x, y, z) -> if2#(eq(head x, min x), x, y, z), if2#(true(), x, y, z) -> head# x)
    (if#(false(), x, y, z) -> if2#(eq(head x, min x), x, y, z), if2#(true(), x, y, z) -> tail# x)
    (if#(false(), x, y, z) -> if2#(eq(head x, min x), x, y, z), if2#(true(), x, y, z) -> rm#(head x, tail x))
    (if#(false(), x, y, z) -> if2#(eq(head x, min x), x, y, z), if2#(true(), x, y, z) -> mins#(app(rm(head x, tail x), y), nil(), app(z, add(head x, nil()))))
    (if#(false(), x, y, z) -> if2#(eq(head x, min x), x, y, z), if2#(false(), x, y, z) -> head# x)
    (if#(false(), x, y, z) -> if2#(eq(head x, min x), x, y, z), if2#(false(), x, y, z) -> tail# x)
    (if#(false(), x, y, z) -> if2#(eq(head x, min x), x, y, z), if2#(false(), x, y, z) -> mins#(tail x, add(head x, y), z))
    (minsort# x -> mins#(x, nil(), nil()), mins#(x, y, z) -> null# x)
    (minsort# x -> mins#(x, nil(), nil()), mins#(x, y, z) -> if#(null x, x, y, z))
    (if_min#(true(), add(n, add(m, x))) -> min# add(n, x), min# add(n, add(m, x)) -> le#(n, m))
    (if_min#(true(), add(n, add(m, x))) -> min# add(n, x), min# add(n, add(m, x)) -> if_min#(le(n, m), add(n, add(m, x))))
    (if2#(true(), x, y, z) -> app#(z, add(head x, nil())), app#(add(n, x), y) -> app#(x, y))
    (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
    (if#(false(), x, y, z) -> eq#(head x, min x), eq#(s x, s y) -> eq#(x, y))
    (if2#(true(), x, y, z) -> mins#(app(rm(head x, tail x), y), nil(), app(z, add(head x, nil()))), mins#(x, y, z) -> null# x)
    (if2#(true(), x, y, z) -> mins#(app(rm(head x, tail x), y), nil(), app(z, add(head x, nil()))), mins#(x, y, z) -> if#(null x, x, y, z))
    (if_rm#(true(), n, add(m, x)) -> rm#(n, x), rm#(n, add(m, x)) -> eq#(n, m))
    (if_rm#(true(), n, add(m, x)) -> rm#(n, x), rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)))
    (rm#(n, add(m, x)) -> eq#(n, m), eq#(s x, s y) -> eq#(x, y))
    (if2#(false(), x, y, z) -> mins#(tail x, add(head x, y), z), mins#(x, y, z) -> null# x)
    (if2#(false(), x, y, z) -> mins#(tail x, add(head x, y), z), mins#(x, y, z) -> if#(null x, x, y, z))}
   EDG:
    {(min# add(n, add(m, x)) -> le#(n, m), le#(s x, s y) -> le#(x, y))
     (if2#(true(), x, y, z) -> app#(rm(head x, tail x), y), app#(add(n, x), y) -> app#(x, y))
     (if_rm#(false(), n, add(m, x)) -> rm#(n, x), rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)))
     (if_rm#(false(), n, add(m, x)) -> rm#(n, x), rm#(n, add(m, x)) -> eq#(n, m))
     (rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)), if_rm#(false(), n, add(m, x)) -> rm#(n, x))
     (rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)), if_rm#(true(), n, add(m, x)) -> rm#(n, x))
     (if2#(true(), x, y, z) -> rm#(head x, tail x), rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)))
     (if2#(true(), x, y, z) -> rm#(head x, tail x), rm#(n, add(m, x)) -> eq#(n, m))
     (if#(false(), x, y, z) -> min# x, min# add(n, add(m, x)) -> if_min#(le(n, m), add(n, add(m, x))))
     (if#(false(), x, y, z) -> min# x, min# add(n, add(m, x)) -> le#(n, m))
     (eq#(s x, s y) -> eq#(x, y), eq#(s x, s y) -> eq#(x, y))
     (app#(add(n, x), y) -> app#(x, y), app#(add(n, x), y) -> app#(x, y))
     (min# add(n, add(m, x)) -> if_min#(le(n, m), add(n, add(m, x))), if_min#(false(), add(n, add(m, x))) -> min# add(m, x))
     (min# add(n, add(m, x)) -> if_min#(le(n, m), add(n, add(m, x))), if_min#(true(), add(n, add(m, x))) -> min# add(n, x))
     (if_min#(false(), add(n, add(m, x))) -> min# add(m, x), min# add(n, add(m, x)) -> if_min#(le(n, m), add(n, add(m, x))))
     (if_min#(false(), add(n, add(m, x))) -> min# add(m, x), min# add(n, add(m, x)) -> le#(n, m))
     (mins#(x, y, z) -> if#(null x, x, y, z), if#(false(), x, y, z) -> if2#(eq(head x, min x), x, y, z))
     (mins#(x, y, z) -> if#(null x, x, y, z), if#(false(), x, y, z) -> head# x)
     (mins#(x, y, z) -> if#(null x, x, y, z), if#(false(), x, y, z) -> min# x)
     (mins#(x, y, z) -> if#(null x, x, y, z), if#(false(), x, y, z) -> eq#(head x, min x))
     (if#(false(), x, y, z) -> if2#(eq(head x, min x), x, y, z), if2#(true(), x, y, z) -> app#(z, add(head x, nil())))
     (if#(false(), x, y, z) -> if2#(eq(head x, min x), x, y, z), if2#(true(), x, y, z) -> app#(rm(head x, tail x), y))
     (if#(false(), x, y, z) -> if2#(eq(head x, min x), x, y, z), if2#(true(), x, y, z) -> head# x)
     (if#(false(), x, y, z) -> if2#(eq(head x, min x), x, y, z), if2#(true(), x, y, z) -> tail# x)
     (if#(false(), x, y, z) -> if2#(eq(head x, min x), x, y, z), if2#(true(), x, y, z) -> rm#(head x, tail x))
     (if#(false(), x, y, z) -> if2#(eq(head x, min x), x, y, z), if2#(true(), x, y, z) -> mins#(app(rm(head x, tail x), y), nil(), app(z, add(head x, nil()))))
     (if#(false(), x, y, z) -> if2#(eq(head x, min x), x, y, z), if2#(false(), x, y, z) -> head# x)
     (if#(false(), x, y, z) -> if2#(eq(head x, min x), x, y, z), if2#(false(), x, y, z) -> tail# x)
     (if#(false(), x, y, z) -> if2#(eq(head x, min x), x, y, z), if2#(false(), x, y, z) -> mins#(tail x, add(head x, y), z))
     (minsort# x -> mins#(x, nil(), nil()), mins#(x, y, z) -> null# x)
     (minsort# x -> mins#(x, nil(), nil()), mins#(x, y, z) -> if#(null x, x, y, z))
     (if_min#(true(), add(n, add(m, x))) -> min# add(n, x), min# add(n, add(m, x)) -> le#(n, m))
     (if_min#(true(), add(n, add(m, x))) -> min# add(n, x), min# add(n, add(m, x)) -> if_min#(le(n, m), add(n, add(m, x))))
     (if2#(true(), x, y, z) -> app#(z, add(head x, nil())), app#(add(n, x), y) -> app#(x, y))
     (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
     (if#(false(), x, y, z) -> eq#(head x, min x), eq#(s x, s y) -> eq#(x, y))
     (if2#(true(), x, y, z) -> mins#(app(rm(head x, tail x), y), nil(), app(z, add(head x, nil()))), mins#(x, y, z) -> null# x)
     (if2#(true(), x, y, z) -> mins#(app(rm(head x, tail x), y), nil(), app(z, add(head x, nil()))), mins#(x, y, z) -> if#(null x, x, y, z))
     (if_rm#(true(), n, add(m, x)) -> rm#(n, x), rm#(n, add(m, x)) -> eq#(n, m))
     (if_rm#(true(), n, add(m, x)) -> rm#(n, x), rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)))
     (rm#(n, add(m, x)) -> eq#(n, m), eq#(s x, s y) -> eq#(x, y))
     (if2#(false(), x, y, z) -> mins#(tail x, add(head x, y), z), mins#(x, y, z) -> null# x)
     (if2#(false(), x, y, z) -> mins#(tail x, add(head x, y), z), mins#(x, y, z) -> if#(null x, x, y, z))}
    EDG:
     {(min# add(n, add(m, x)) -> le#(n, m), le#(s x, s y) -> le#(x, y))
      (if2#(true(), x, y, z) -> app#(rm(head x, tail x), y), app#(add(n, x), y) -> app#(x, y))
      (if_rm#(false(), n, add(m, x)) -> rm#(n, x), rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)))
      (if_rm#(false(), n, add(m, x)) -> rm#(n, x), rm#(n, add(m, x)) -> eq#(n, m))
      (rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)), if_rm#(false(), n, add(m, x)) -> rm#(n, x))
      (rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)), if_rm#(true(), n, add(m, x)) -> rm#(n, x))
      (if2#(true(), x, y, z) -> rm#(head x, tail x), rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)))
      (if2#(true(), x, y, z) -> rm#(head x, tail x), rm#(n, add(m, x)) -> eq#(n, m))
      (if#(false(), x, y, z) -> min# x, min# add(n, add(m, x)) -> if_min#(le(n, m), add(n, add(m, x))))
      (if#(false(), x, y, z) -> min# x, min# add(n, add(m, x)) -> le#(n, m))
      (eq#(s x, s y) -> eq#(x, y), eq#(s x, s y) -> eq#(x, y))
      (app#(add(n, x), y) -> app#(x, y), app#(add(n, x), y) -> app#(x, y))
      (min# add(n, add(m, x)) -> if_min#(le(n, m), add(n, add(m, x))), if_min#(false(), add(n, add(m, x))) -> min# add(m, x))
      (min# add(n, add(m, x)) -> if_min#(le(n, m), add(n, add(m, x))), if_min#(true(), add(n, add(m, x))) -> min# add(n, x))
      (if_min#(false(), add(n, add(m, x))) -> min# add(m, x), min# add(n, add(m, x)) -> if_min#(le(n, m), add(n, add(m, x))))
      (if_min#(false(), add(n, add(m, x))) -> min# add(m, x), min# add(n, add(m, x)) -> le#(n, m))
      (mins#(x, y, z) -> if#(null x, x, y, z), if#(false(), x, y, z) -> if2#(eq(head x, min x), x, y, z))
      (mins#(x, y, z) -> if#(null x, x, y, z), if#(false(), x, y, z) -> head# x)
      (mins#(x, y, z) -> if#(null x, x, y, z), if#(false(), x, y, z) -> min# x)
      (mins#(x, y, z) -> if#(null x, x, y, z), if#(false(), x, y, z) -> eq#(head x, min x))
      (if#(false(), x, y, z) -> if2#(eq(head x, min x), x, y, z), if2#(true(), x, y, z) -> app#(z, add(head x, nil())))
      (if#(false(), x, y, z) -> if2#(eq(head x, min x), x, y, z), if2#(true(), x, y, z) -> app#(rm(head x, tail x), y))
      (if#(false(), x, y, z) -> if2#(eq(head x, min x), x, y, z), if2#(true(), x, y, z) -> head# x)
      (if#(false(), x, y, z) -> if2#(eq(head x, min x), x, y, z), if2#(true(), x, y, z) -> tail# x)
      (if#(false(), x, y, z) -> if2#(eq(head x, min x), x, y, z), if2#(true(), x, y, z) -> rm#(head x, tail x))
      (if#(false(), x, y, z) -> if2#(eq(head x, min x), x, y, z), if2#(true(), x, y, z) -> mins#(app(rm(head x, tail x), y), nil(), app(z, add(head x, nil()))))
      (if#(false(), x, y, z) -> if2#(eq(head x, min x), x, y, z), if2#(false(), x, y, z) -> head# x)
      (if#(false(), x, y, z) -> if2#(eq(head x, min x), x, y, z), if2#(false(), x, y, z) -> tail# x)
      (if#(false(), x, y, z) -> if2#(eq(head x, min x), x, y, z), if2#(false(), x, y, z) -> mins#(tail x, add(head x, y), z))
      (minsort# x -> mins#(x, nil(), nil()), mins#(x, y, z) -> null# x)
      (minsort# x -> mins#(x, nil(), nil()), mins#(x, y, z) -> if#(null x, x, y, z))
      (if_min#(true(), add(n, add(m, x))) -> min# add(n, x), min# add(n, add(m, x)) -> le#(n, m))
      (if_min#(true(), add(n, add(m, x))) -> min# add(n, x), min# add(n, add(m, x)) -> if_min#(le(n, m), add(n, add(m, x))))
      (if2#(true(), x, y, z) -> app#(z, add(head x, nil())), app#(add(n, x), y) -> app#(x, y))
      (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
      (if#(false(), x, y, z) -> eq#(head x, min x), eq#(s x, s y) -> eq#(x, y))
      (if2#(true(), x, y, z) -> mins#(app(rm(head x, tail x), y), nil(), app(z, add(head x, nil()))), mins#(x, y, z) -> null# x)
      (if2#(true(), x, y, z) -> mins#(app(rm(head x, tail x), y), nil(), app(z, add(head x, nil()))), mins#(x, y, z) -> if#(null x, x, y, z))
      (if_rm#(true(), n, add(m, x)) -> rm#(n, x), rm#(n, add(m, x)) -> eq#(n, m))
      (if_rm#(true(), n, add(m, x)) -> rm#(n, x), rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)))
      (rm#(n, add(m, x)) -> eq#(n, m), eq#(s x, s y) -> eq#(x, y))
      (if2#(false(), x, y, z) -> mins#(tail x, add(head x, y), z), mins#(x, y, z) -> null# x)
      (if2#(false(), x, y, z) -> mins#(tail x, add(head x, y), z), mins#(x, y, z) -> if#(null x, x, y, z))}
     STATUS:
      arrows: 0.941015
      SCCS (6):
       Scc:
        {        mins#(x, y, z) -> if#(null x, x, y, z),
          if#(false(), x, y, z) -> if2#(eq(head x, min x), x, y, z),
          if2#(true(), x, y, z) -> mins#(app(rm(head x, tail x), y), nil(), app(z, add(head x, nil()))),
         if2#(false(), x, y, z) -> mins#(tail x, add(head x, y), z)}
       Scc:
        {            rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)),
          if_rm#(true(), n, add(m, x)) -> rm#(n, x),
         if_rm#(false(), n, add(m, x)) -> rm#(n, x)}
       Scc:
        {app#(add(n, x), y) -> app#(x, y)}
       Scc:
        {             min# add(n, add(m, x)) -> if_min#(le(n, m), add(n, add(m, x))),
          if_min#(true(), add(n, add(m, x))) -> min# add(n, x),
         if_min#(false(), add(n, add(m, x))) -> min# add(m, x)}
       Scc:
        {le#(s x, s y) -> le#(x, y)}
       Scc:
        {eq#(s x, s y) -> eq#(x, y)}
       
       
       SCC (4):
        Strict:
         {        mins#(x, y, z) -> if#(null x, x, y, z),
           if#(false(), x, y, z) -> if2#(eq(head x, min x), x, y, z),
           if2#(true(), x, y, z) -> mins#(app(rm(head x, tail x), y), nil(), app(z, add(head x, nil()))),
          if2#(false(), x, y, z) -> mins#(tail x, add(head x, y), z)}
        Weak:
        {                      eq(0(), 0()) -> true(),
                               eq(0(), s x) -> false(),
                               eq(s x, 0()) -> false(),
                               eq(s x, s y) -> eq(x, y),
                                 le(0(), y) -> true(),
                               le(s x, 0()) -> false(),
                               le(s x, s y) -> le(x, y),
                              app(nil(), y) -> y,
                          app(add(n, x), y) -> add(n, app(x, y)),
                          min add(n, nil()) -> n,
                      min add(n, add(m, x)) -> if_min(le(n, m), add(n, add(m, x))),
          if_min(true(), add(n, add(m, x))) -> min add(n, x),
         if_min(false(), add(n, add(m, x))) -> min add(m, x),
                             head add(n, x) -> n,
                                 tail nil() -> nil(),
                             tail add(n, x) -> x,
                                 null nil() -> true(),
                             null add(n, x) -> false(),
                               rm(n, nil()) -> nil(),
                           rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)),
                if_rm(true(), n, add(m, x)) -> rm(n, x),
               if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)),
                              mins(x, y, z) -> if(null x, x, y, z),
                                  minsort x -> mins(x, nil(), nil()),
                        if(true(), x, y, z) -> z,
                       if(false(), x, y, z) -> if2(eq(head x, min x), x, y, z),
                       if2(true(), x, y, z) -> mins(app(rm(head x, tail x), y), nil(), app(z, add(head x, nil()))),
                      if2(false(), x, y, z) -> mins(tail x, add(head x, y), z)}
        Open
       
       
       
       SCC (3):
        Strict:
         {            rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)),
           if_rm#(true(), n, add(m, x)) -> rm#(n, x),
          if_rm#(false(), n, add(m, x)) -> rm#(n, x)}
        Weak:
        {                      eq(0(), 0()) -> true(),
                               eq(0(), s x) -> false(),
                               eq(s x, 0()) -> false(),
                               eq(s x, s y) -> eq(x, y),
                                 le(0(), y) -> true(),
                               le(s x, 0()) -> false(),
                               le(s x, s y) -> le(x, y),
                              app(nil(), y) -> y,
                          app(add(n, x), y) -> add(n, app(x, y)),
                          min add(n, nil()) -> n,
                      min add(n, add(m, x)) -> if_min(le(n, m), add(n, add(m, x))),
          if_min(true(), add(n, add(m, x))) -> min add(n, x),
         if_min(false(), add(n, add(m, x))) -> min add(m, x),
                             head add(n, x) -> n,
                                 tail nil() -> nil(),
                             tail add(n, x) -> x,
                                 null nil() -> true(),
                             null add(n, x) -> false(),
                               rm(n, nil()) -> nil(),
                           rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)),
                if_rm(true(), n, add(m, x)) -> rm(n, x),
               if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)),
                              mins(x, y, z) -> if(null x, x, y, z),
                                  minsort x -> mins(x, nil(), nil()),
                        if(true(), x, y, z) -> z,
                       if(false(), x, y, z) -> if2(eq(head x, min x), x, y, z),
                       if2(true(), x, y, z) -> mins(app(rm(head x, tail x), y), nil(), app(z, add(head x, nil()))),
                      if2(false(), x, y, z) -> mins(tail x, add(head x, y), z)}
        Open
       
       
       
       
       
       SCC (1):
        Strict:
         {app#(add(n, x), y) -> app#(x, y)}
        Weak:
        {                      eq(0(), 0()) -> true(),
                               eq(0(), s x) -> false(),
                               eq(s x, 0()) -> false(),
                               eq(s x, s y) -> eq(x, y),
                                 le(0(), y) -> true(),
                               le(s x, 0()) -> false(),
                               le(s x, s y) -> le(x, y),
                              app(nil(), y) -> y,
                          app(add(n, x), y) -> add(n, app(x, y)),
                          min add(n, nil()) -> n,
                      min add(n, add(m, x)) -> if_min(le(n, m), add(n, add(m, x))),
          if_min(true(), add(n, add(m, x))) -> min add(n, x),
         if_min(false(), add(n, add(m, x))) -> min add(m, x),
                             head add(n, x) -> n,
                                 tail nil() -> nil(),
                             tail add(n, x) -> x,
                                 null nil() -> true(),
                             null add(n, x) -> false(),
                               rm(n, nil()) -> nil(),
                           rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)),
                if_rm(true(), n, add(m, x)) -> rm(n, x),
               if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)),
                              mins(x, y, z) -> if(null x, x, y, z),
                                  minsort x -> mins(x, nil(), nil()),
                        if(true(), x, y, z) -> z,
                       if(false(), x, y, z) -> if2(eq(head x, min x), x, y, z),
                       if2(true(), x, y, z) -> mins(app(rm(head x, tail x), y), nil(), app(z, add(head x, nil()))),
                      if2(false(), x, y, z) -> mins(tail x, add(head x, y), z)}
        Open
       
       
       SCC (3):
        Strict:
         {             min# add(n, add(m, x)) -> if_min#(le(n, m), add(n, add(m, x))),
           if_min#(true(), add(n, add(m, x))) -> min# add(n, x),
          if_min#(false(), add(n, add(m, x))) -> min# add(m, x)}
        Weak:
        {                      eq(0(), 0()) -> true(),
                               eq(0(), s x) -> false(),
                               eq(s x, 0()) -> false(),
                               eq(s x, s y) -> eq(x, y),
                                 le(0(), y) -> true(),
                               le(s x, 0()) -> false(),
                               le(s x, s y) -> le(x, y),
                              app(nil(), y) -> y,
                          app(add(n, x), y) -> add(n, app(x, y)),
                          min add(n, nil()) -> n,
                      min add(n, add(m, x)) -> if_min(le(n, m), add(n, add(m, x))),
          if_min(true(), add(n, add(m, x))) -> min add(n, x),
         if_min(false(), add(n, add(m, x))) -> min add(m, x),
                             head add(n, x) -> n,
                                 tail nil() -> nil(),
                             tail add(n, x) -> x,
                                 null nil() -> true(),
                             null add(n, x) -> false(),
                               rm(n, nil()) -> nil(),
                           rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)),
                if_rm(true(), n, add(m, x)) -> rm(n, x),
               if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)),
                              mins(x, y, z) -> if(null x, x, y, z),
                                  minsort x -> mins(x, nil(), nil()),
                        if(true(), x, y, z) -> z,
                       if(false(), x, y, z) -> if2(eq(head x, min x), x, y, z),
                       if2(true(), x, y, z) -> mins(app(rm(head x, tail x), y), nil(), app(z, add(head x, nil()))),
                      if2(false(), x, y, z) -> mins(tail x, add(head x, y), z)}
        Open
       
       SCC (1):
        Strict:
         {le#(s x, s y) -> le#(x, y)}
        Weak:
        {                      eq(0(), 0()) -> true(),
                               eq(0(), s x) -> false(),
                               eq(s x, 0()) -> false(),
                               eq(s x, s y) -> eq(x, y),
                                 le(0(), y) -> true(),
                               le(s x, 0()) -> false(),
                               le(s x, s y) -> le(x, y),
                              app(nil(), y) -> y,
                          app(add(n, x), y) -> add(n, app(x, y)),
                          min add(n, nil()) -> n,
                      min add(n, add(m, x)) -> if_min(le(n, m), add(n, add(m, x))),
          if_min(true(), add(n, add(m, x))) -> min add(n, x),
         if_min(false(), add(n, add(m, x))) -> min add(m, x),
                             head add(n, x) -> n,
                                 tail nil() -> nil(),
                             tail add(n, x) -> x,
                                 null nil() -> true(),
                             null add(n, x) -> false(),
                               rm(n, nil()) -> nil(),
                           rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)),
                if_rm(true(), n, add(m, x)) -> rm(n, x),
               if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)),
                              mins(x, y, z) -> if(null x, x, y, z),
                                  minsort x -> mins(x, nil(), nil()),
                        if(true(), x, y, z) -> z,
                       if(false(), x, y, z) -> if2(eq(head x, min x), x, y, z),
                       if2(true(), x, y, z) -> mins(app(rm(head x, tail x), y), nil(), app(z, add(head x, nil()))),
                      if2(false(), x, y, z) -> mins(tail x, add(head x, y), z)}
        Open
       
       SCC (1):
        Strict:
         {eq#(s x, s y) -> eq#(x, y)}
        Weak:
        {                      eq(0(), 0()) -> true(),
                               eq(0(), s x) -> false(),
                               eq(s x, 0()) -> false(),
                               eq(s x, s y) -> eq(x, y),
                                 le(0(), y) -> true(),
                               le(s x, 0()) -> false(),
                               le(s x, s y) -> le(x, y),
                              app(nil(), y) -> y,
                          app(add(n, x), y) -> add(n, app(x, y)),
                          min add(n, nil()) -> n,
                      min add(n, add(m, x)) -> if_min(le(n, m), add(n, add(m, x))),
          if_min(true(), add(n, add(m, x))) -> min add(n, x),
         if_min(false(), add(n, add(m, x))) -> min add(m, x),
                             head add(n, x) -> n,
                                 tail nil() -> nil(),
                             tail add(n, x) -> x,
                                 null nil() -> true(),
                             null add(n, x) -> false(),
                               rm(n, nil()) -> nil(),
                           rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)),
                if_rm(true(), n, add(m, x)) -> rm(n, x),
               if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)),
                              mins(x, y, z) -> if(null x, x, y, z),
                                  minsort x -> mins(x, nil(), nil()),
                        if(true(), x, y, z) -> z,
                       if(false(), x, y, z) -> if2(eq(head x, min x), x, y, z),
                       if2(true(), x, y, z) -> mins(app(rm(head x, tail x), y), nil(), app(z, add(head x, nil()))),
                      if2(false(), x, y, z) -> mins(tail x, add(head x, y), z)}
        Open