MAYBE
Time: 0.043636
TRS:
 {app(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app(app(cons(), app(app(f, x), h)), app(app(app(app(insert(), f), g), t), app(app(g, x), h))),
                   app(app(app(app(insert(), f), g), nil()), x) -> app(app(cons(), x), nil()),
            app(app(app(sort(), f), g), app(app(cons(), h), t)) -> app(app(app(app(insert(), f), g), app(app(app(sort(), f), g), t)), h),
                             app(app(app(sort(), f), g), nil()) -> nil(),
                                        app(app(max(), x), 0()) -> x,
                      app(app(max(), app(s(), x)), app(s(), y)) -> app(app(max(), x), y),
                                        app(app(max(), 0()), x) -> x,
                                        app(app(min(), x), 0()) -> 0(),
                      app(app(min(), app(s(), x)), app(s(), y)) -> app(app(min(), x), y),
                                        app(app(min(), 0()), x) -> 0(),
                                       app(ascending_sort(), l) -> app(app(app(sort(), min()), max()), l),
                                      app(descending_sort(), l) -> app(app(app(sort(), max()), min()), l)}
 DP:
  DP:
   {app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(f, x),
    app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(g, x),
    app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(f, x), h),
    app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(g, x), h),
    app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(app(app(insert(), f), g), t), app(app(g, x), h)),
    app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(app(insert(), f), g), t),
    app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(cons(), app(app(f, x), h)), app(app(app(app(insert(), f), g), t), app(app(g, x), h))),
    app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(cons(), app(app(f, x), h)),
                     app#(app(app(app(insert(), f), g), nil()), x) -> app#(app(cons(), x), nil()),
                     app#(app(app(app(insert(), f), g), nil()), x) -> app#(cons(), x),
              app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(app(insert(), f), g), app(app(app(sort(), f), g), t)), h),
              app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(insert(), f), g), app(app(app(sort(), f), g), t)),
              app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(sort(), f), g), t),
              app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(insert(), f), g),
              app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(insert(), f),
                        app#(app(max(), app(s(), x)), app(s(), y)) -> app#(app(max(), x), y),
                        app#(app(max(), app(s(), x)), app(s(), y)) -> app#(max(), x),
                        app#(app(min(), app(s(), x)), app(s(), y)) -> app#(app(min(), x), y),
                        app#(app(min(), app(s(), x)), app(s(), y)) -> app#(min(), x),
                                         app#(ascending_sort(), l) -> app#(app(app(sort(), min()), max()), l),
                                         app#(ascending_sort(), l) -> app#(app(sort(), min()), max()),
                                         app#(ascending_sort(), l) -> app#(sort(), min()),
                                        app#(descending_sort(), l) -> app#(app(app(sort(), max()), min()), l),
                                        app#(descending_sort(), l) -> app#(app(sort(), max()), min()),
                                        app#(descending_sort(), l) -> app#(sort(), max())}
  TRS:
  {app(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app(app(cons(), app(app(f, x), h)), app(app(app(app(insert(), f), g), t), app(app(g, x), h))),
                    app(app(app(app(insert(), f), g), nil()), x) -> app(app(cons(), x), nil()),
             app(app(app(sort(), f), g), app(app(cons(), h), t)) -> app(app(app(app(insert(), f), g), app(app(app(sort(), f), g), t)), h),
                              app(app(app(sort(), f), g), nil()) -> nil(),
                                         app(app(max(), x), 0()) -> x,
                       app(app(max(), app(s(), x)), app(s(), y)) -> app(app(max(), x), y),
                                         app(app(max(), 0()), x) -> x,
                                         app(app(min(), x), 0()) -> 0(),
                       app(app(min(), app(s(), x)), app(s(), y)) -> app(app(min(), x), y),
                                         app(app(min(), 0()), x) -> 0(),
                                        app(ascending_sort(), l) -> app(app(app(sort(), min()), max()), l),
                                       app(descending_sort(), l) -> app(app(app(sort(), max()), min()), l)}
  UR:
   {app(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app(app(cons(), app(app(f, x), h)), app(app(app(app(insert(), f), g), t), app(app(g, x), h))),
                     app(app(app(app(insert(), f), g), nil()), x) -> app(app(cons(), x), nil()),
              app(app(app(sort(), f), g), app(app(cons(), h), t)) -> app(app(app(app(insert(), f), g), app(app(app(sort(), f), g), t)), h),
                               app(app(app(sort(), f), g), nil()) -> nil(),
                                          app(app(max(), x), 0()) -> x,
                        app(app(max(), app(s(), x)), app(s(), y)) -> app(app(max(), x), y),
                                          app(app(max(), 0()), x) -> x,
                                          app(app(min(), x), 0()) -> 0(),
                        app(app(min(), app(s(), x)), app(s(), y)) -> app(app(min(), x), y),
                                          app(app(min(), 0()), x) -> 0(),
                                         app(ascending_sort(), l) -> app(app(app(sort(), min()), max()), l),
                                        app(descending_sort(), l) -> app(app(app(sort(), max()), min()), l),
                                                          a(z, w) -> z,
                                                          a(z, w) -> w}
   EDG:
    {
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(g, x), app#(descending_sort(), l) -> app#(sort(), max()))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(g, x), app#(descending_sort(), l) -> app#(app(sort(), max()), min()))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(g, x), app#(descending_sort(), l) -> app#(app(app(sort(), max()), min()), l))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(g, x), app#(ascending_sort(), l) -> app#(sort(), min()))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(g, x), app#(ascending_sort(), l) -> app#(app(sort(), min()), max()))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(g, x), app#(ascending_sort(), l) -> app#(app(app(sort(), min()), max()), l))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(g, x), app#(app(min(), app(s(), x)), app(s(), y)) -> app#(min(), x))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(g, x), app#(app(min(), app(s(), x)), app(s(), y)) -> app#(app(min(), x), y))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(g, x), app#(app(max(), app(s(), x)), app(s(), y)) -> app#(max(), x))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(g, x), app#(app(max(), app(s(), x)), app(s(), y)) -> app#(app(max(), x), y))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(g, x), app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(insert(), f))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(g, x), app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(insert(), f), g))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(g, x), app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(sort(), f), g), t))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(g, x), app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(insert(), f), g), app(app(app(sort(), f), g), t)))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(g, x), app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(app(insert(), f), g), app(app(app(sort(), f), g), t)), h))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(g, x), app#(app(app(app(insert(), f), g), nil()), x) -> app#(cons(), x))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(g, x), app#(app(app(app(insert(), f), g), nil()), x) -> app#(app(cons(), x), nil()))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(g, x), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(cons(), app(app(f, x), h)))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(g, x), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(cons(), app(app(f, x), h)), app(app(app(app(insert(), f), g), t), app(app(g, x), h))))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(g, x), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(app(insert(), f), g), t))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(g, x), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(app(app(insert(), f), g), t), app(app(g, x), h)))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(g, x), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(g, x), h))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(g, x), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(f, x), h))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(g, x), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(g, x))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(g, x), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(f, x))
     (app#(descending_sort(), l) -> app#(app(app(sort(), max()), min()), l), app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(insert(), f))
     (app#(descending_sort(), l) -> app#(app(app(sort(), max()), min()), l), app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(insert(), f), g))
     (app#(descending_sort(), l) -> app#(app(app(sort(), max()), min()), l), app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(sort(), f), g), t))
     (app#(descending_sort(), l) -> app#(app(app(sort(), max()), min()), l), app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(insert(), f), g), app(app(app(sort(), f), g), t)))
     (app#(descending_sort(), l) -> app#(app(app(sort(), max()), min()), l), app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(app(insert(), f), g), app(app(app(sort(), f), g), t)), h))
     (app#(app(max(), app(s(), x)), app(s(), y)) -> app#(app(max(), x), y), app#(app(max(), app(s(), x)), app(s(), y)) -> app#(max(), x))
     (app#(app(max(), app(s(), x)), app(s(), y)) -> app#(app(max(), x), y), app#(app(max(), app(s(), x)), app(s(), y)) -> app#(app(max(), x), y))
     (app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(sort(), f), g), t), app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(insert(), f))
     (app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(sort(), f), g), t), app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(insert(), f), g))
     (app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(sort(), f), g), t), app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(sort(), f), g), t))
     (app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(sort(), f), g), t), app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(insert(), f), g), app(app(app(sort(), f), g), t)))
     (app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(sort(), f), g), t), app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(app(insert(), f), g), app(app(app(sort(), f), g), t)), h))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(f, x), h), app#(descending_sort(), l) -> app#(sort(), max()))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(f, x), h), app#(descending_sort(), l) -> app#(app(sort(), max()), min()))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(f, x), h), app#(descending_sort(), l) -> app#(app(app(sort(), max()), min()), l))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(f, x), h), app#(ascending_sort(), l) -> app#(sort(), min()))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(f, x), h), app#(ascending_sort(), l) -> app#(app(sort(), min()), max()))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(f, x), h), app#(ascending_sort(), l) -> app#(app(app(sort(), min()), max()), l))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(f, x), h), app#(app(min(), app(s(), x)), app(s(), y)) -> app#(min(), x))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(f, x), h), app#(app(min(), app(s(), x)), app(s(), y)) -> app#(app(min(), x), y))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(f, x), h), app#(app(max(), app(s(), x)), app(s(), y)) -> app#(max(), x))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(f, x), h), app#(app(max(), app(s(), x)), app(s(), y)) -> app#(app(max(), x), y))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(f, x), h), app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(insert(), f))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(f, x), h), app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(insert(), f), g))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(f, x), h), app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(sort(), f), g), t))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(f, x), h), app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(insert(), f), g), app(app(app(sort(), f), g), t)))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(f, x), h), app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(app(insert(), f), g), app(app(app(sort(), f), g), t)), h))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(f, x), h), app#(app(app(app(insert(), f), g), nil()), x) -> app#(cons(), x))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(f, x), h), app#(app(app(app(insert(), f), g), nil()), x) -> app#(app(cons(), x), nil()))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(f, x), h), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(cons(), app(app(f, x), h)))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(f, x), h), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(cons(), app(app(f, x), h)), app(app(app(app(insert(), f), g), t), app(app(g, x), h))))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(f, x), h), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(app(insert(), f), g), t))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(f, x), h), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(app(app(insert(), f), g), t), app(app(g, x), h)))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(f, x), h), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(g, x), h))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(f, x), h), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(f, x), h))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(f, x), h), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(g, x))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(f, x), h), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(f, x))
     (app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(app(insert(), f), g), app(app(app(sort(), f), g), t)), h), app#(app(app(app(insert(), f), g), nil()), x) -> app#(cons(), x))
     (app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(app(insert(), f), g), app(app(app(sort(), f), g), t)), h), app#(app(app(app(insert(), f), g), nil()), x) -> app#(app(cons(), x), nil()))
     (app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(app(insert(), f), g), app(app(app(sort(), f), g), t)), h), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(cons(), app(app(f, x), h)))
     (app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(app(insert(), f), g), app(app(app(sort(), f), g), t)), h), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(cons(), app(app(f, x), h)), app(app(app(app(insert(), f), g), t), app(app(g, x), h))))
     (app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(app(insert(), f), g), app(app(app(sort(), f), g), t)), h), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(app(insert(), f), g), t))
     (app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(app(insert(), f), g), app(app(app(sort(), f), g), t)), h), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(app(app(insert(), f), g), t), app(app(g, x), h)))
     (app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(app(insert(), f), g), app(app(app(sort(), f), g), t)), h), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(g, x), h))
     (app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(app(insert(), f), g), app(app(app(sort(), f), g), t)), h), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(f, x), h))
     (app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(app(insert(), f), g), app(app(app(sort(), f), g), t)), h), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(g, x))
     (app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(app(insert(), f), g), app(app(app(sort(), f), g), t)), h), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(f, x))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(g, x), h), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(f, x))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(g, x), h), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(g, x))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(g, x), h), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(f, x), h))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(g, x), h), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(g, x), h))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(g, x), h), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(app(app(insert(), f), g), t), app(app(g, x), h)))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(g, x), h), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(app(insert(), f), g), t))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(g, x), h), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(cons(), app(app(f, x), h)), app(app(app(app(insert(), f), g), t), app(app(g, x), h))))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(g, x), h), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(cons(), app(app(f, x), h)))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(g, x), h), app#(app(app(app(insert(), f), g), nil()), x) -> app#(app(cons(), x), nil()))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(g, x), h), app#(app(app(app(insert(), f), g), nil()), x) -> app#(cons(), x))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(g, x), h), app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(app(insert(), f), g), app(app(app(sort(), f), g), t)), h))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(g, x), h), app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(insert(), f), g), app(app(app(sort(), f), g), t)))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(g, x), h), app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(sort(), f), g), t))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(g, x), h), app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(insert(), f), g))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(g, x), h), app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(insert(), f))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(g, x), h), app#(app(max(), app(s(), x)), app(s(), y)) -> app#(app(max(), x), y))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(g, x), h), app#(app(max(), app(s(), x)), app(s(), y)) -> app#(max(), x))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(g, x), h), app#(app(min(), app(s(), x)), app(s(), y)) -> app#(app(min(), x), y))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(g, x), h), app#(app(min(), app(s(), x)), app(s(), y)) -> app#(min(), x))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(g, x), h), app#(ascending_sort(), l) -> app#(app(app(sort(), min()), max()), l))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(g, x), h), app#(ascending_sort(), l) -> app#(app(sort(), min()), max()))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(g, x), h), app#(ascending_sort(), l) -> app#(sort(), min()))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(g, x), h), app#(descending_sort(), l) -> app#(app(app(sort(), max()), min()), l))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(g, x), h), app#(descending_sort(), l) -> app#(app(sort(), max()), min()))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(g, x), h), app#(descending_sort(), l) -> app#(sort(), max()))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(app(app(insert(), f), g), t), app(app(g, x), h)), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(f, x))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(app(app(insert(), f), g), t), app(app(g, x), h)), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(g, x))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(app(app(insert(), f), g), t), app(app(g, x), h)), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(f, x), h))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(app(app(insert(), f), g), t), app(app(g, x), h)), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(g, x), h))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(app(app(insert(), f), g), t), app(app(g, x), h)), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(app(app(insert(), f), g), t), app(app(g, x), h)))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(app(app(insert(), f), g), t), app(app(g, x), h)), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(app(insert(), f), g), t))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(app(app(insert(), f), g), t), app(app(g, x), h)), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(cons(), app(app(f, x), h)), app(app(app(app(insert(), f), g), t), app(app(g, x), h))))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(app(app(insert(), f), g), t), app(app(g, x), h)), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(cons(), app(app(f, x), h)))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(app(app(insert(), f), g), t), app(app(g, x), h)), app#(app(app(app(insert(), f), g), nil()), x) -> app#(app(cons(), x), nil()))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(app(app(insert(), f), g), t), app(app(g, x), h)), app#(app(app(app(insert(), f), g), nil()), x) -> app#(cons(), x))
     (app#(app(min(), app(s(), x)), app(s(), y)) -> app#(app(min(), x), y), app#(app(min(), app(s(), x)), app(s(), y)) -> app#(app(min(), x), y))
     (app#(app(min(), app(s(), x)), app(s(), y)) -> app#(app(min(), x), y), app#(app(min(), app(s(), x)), app(s(), y)) -> app#(min(), x))
     (app#(ascending_sort(), l) -> app#(app(app(sort(), min()), max()), l), app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(app(insert(), f), g), app(app(app(sort(), f), g), t)), h))
     (app#(ascending_sort(), l) -> app#(app(app(sort(), min()), max()), l), app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(insert(), f), g), app(app(app(sort(), f), g), t)))
     (app#(ascending_sort(), l) -> app#(app(app(sort(), min()), max()), l), app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(sort(), f), g), t))
     (app#(ascending_sort(), l) -> app#(app(app(sort(), min()), max()), l), app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(insert(), f), g))
     (app#(ascending_sort(), l) -> app#(app(app(sort(), min()), max()), l), app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(insert(), f))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(f, x), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(f, x))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(f, x), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(g, x))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(f, x), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(f, x), h))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(f, x), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(g, x), h))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(f, x), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(app(app(insert(), f), g), t), app(app(g, x), h)))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(f, x), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(app(insert(), f), g), t))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(f, x), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(cons(), app(app(f, x), h)), app(app(app(app(insert(), f), g), t), app(app(g, x), h))))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(f, x), app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(cons(), app(app(f, x), h)))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(f, x), app#(app(app(app(insert(), f), g), nil()), x) -> app#(app(cons(), x), nil()))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(f, x), app#(app(app(app(insert(), f), g), nil()), x) -> app#(cons(), x))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(f, x), app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(app(insert(), f), g), app(app(app(sort(), f), g), t)), h))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(f, x), app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(insert(), f), g), app(app(app(sort(), f), g), t)))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(f, x), app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(sort(), f), g), t))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(f, x), app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(insert(), f), g))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(f, x), app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(insert(), f))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(f, x), app#(app(max(), app(s(), x)), app(s(), y)) -> app#(app(max(), x), y))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(f, x), app#(app(max(), app(s(), x)), app(s(), y)) -> app#(max(), x))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(f, x), app#(app(min(), app(s(), x)), app(s(), y)) -> app#(app(min(), x), y))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(f, x), app#(app(min(), app(s(), x)), app(s(), y)) -> app#(min(), x))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(f, x), app#(ascending_sort(), l) -> app#(app(app(sort(), min()), max()), l))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(f, x), app#(ascending_sort(), l) -> app#(app(sort(), min()), max()))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(f, x), app#(ascending_sort(), l) -> app#(sort(), min()))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(f, x), app#(descending_sort(), l) -> app#(app(app(sort(), max()), min()), l))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(f, x), app#(descending_sort(), l) -> app#(app(sort(), max()), min()))
     (app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(f, x), app#(descending_sort(), l) -> app#(sort(), max()))
    }
    STATUS:
     arrows: 0.777600
     SCCS (3):
      Scc:
       {app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(f, x),
        app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(g, x),
        app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(f, x), h),
        app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(g, x), h),
        app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(app(app(insert(), f), g), t), app(app(g, x), h)),
                  app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(app(insert(), f), g), app(app(app(sort(), f), g), t)), h),
                  app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(sort(), f), g), t),
                                             app#(ascending_sort(), l) -> app#(app(app(sort(), min()), max()), l),
                                            app#(descending_sort(), l) -> app#(app(app(sort(), max()), min()), l)}
      Scc:
       {app#(app(min(), app(s(), x)), app(s(), y)) -> app#(app(min(), x), y)}
      Scc:
       {app#(app(max(), app(s(), x)), app(s(), y)) -> app#(app(max(), x), y)}
      
      SCC (9):
       Strict:
        {app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(f, x),
         app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(g, x),
         app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(f, x), h),
         app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(g, x), h),
         app#(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app#(app(app(app(insert(), f), g), t), app(app(g, x), h)),
                   app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(app(insert(), f), g), app(app(app(sort(), f), g), t)), h),
                   app#(app(app(sort(), f), g), app(app(cons(), h), t)) -> app#(app(app(sort(), f), g), t),
                                              app#(ascending_sort(), l) -> app#(app(app(sort(), min()), max()), l),
                                             app#(descending_sort(), l) -> app#(app(app(sort(), max()), min()), l)}
       Weak:
       {app(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app(app(cons(), app(app(f, x), h)), app(app(app(app(insert(), f), g), t), app(app(g, x), h))),
                         app(app(app(app(insert(), f), g), nil()), x) -> app(app(cons(), x), nil()),
                  app(app(app(sort(), f), g), app(app(cons(), h), t)) -> app(app(app(app(insert(), f), g), app(app(app(sort(), f), g), t)), h),
                                   app(app(app(sort(), f), g), nil()) -> nil(),
                                              app(app(max(), x), 0()) -> x,
                            app(app(max(), app(s(), x)), app(s(), y)) -> app(app(max(), x), y),
                                              app(app(max(), 0()), x) -> x,
                                              app(app(min(), x), 0()) -> 0(),
                            app(app(min(), app(s(), x)), app(s(), y)) -> app(app(min(), x), y),
                                              app(app(min(), 0()), x) -> 0(),
                                             app(ascending_sort(), l) -> app(app(app(sort(), min()), max()), l),
                                            app(descending_sort(), l) -> app(app(app(sort(), max()), min()), l)}
       Open
      
      
      
      
      SCC (1):
       Strict:
        {app#(app(min(), app(s(), x)), app(s(), y)) -> app#(app(min(), x), y)}
       Weak:
       {app(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app(app(cons(), app(app(f, x), h)), app(app(app(app(insert(), f), g), t), app(app(g, x), h))),
                         app(app(app(app(insert(), f), g), nil()), x) -> app(app(cons(), x), nil()),
                  app(app(app(sort(), f), g), app(app(cons(), h), t)) -> app(app(app(app(insert(), f), g), app(app(app(sort(), f), g), t)), h),
                                   app(app(app(sort(), f), g), nil()) -> nil(),
                                              app(app(max(), x), 0()) -> x,
                            app(app(max(), app(s(), x)), app(s(), y)) -> app(app(max(), x), y),
                                              app(app(max(), 0()), x) -> x,
                                              app(app(min(), x), 0()) -> 0(),
                            app(app(min(), app(s(), x)), app(s(), y)) -> app(app(min(), x), y),
                                              app(app(min(), 0()), x) -> 0(),
                                             app(ascending_sort(), l) -> app(app(app(sort(), min()), max()), l),
                                            app(descending_sort(), l) -> app(app(app(sort(), max()), min()), l)}
       Open
      
      SCC (1):
       Strict:
        {app#(app(max(), app(s(), x)), app(s(), y)) -> app#(app(max(), x), y)}
       Weak:
       {app(app(app(app(insert(), f), g), app(app(cons(), h), t)), x) -> app(app(cons(), app(app(f, x), h)), app(app(app(app(insert(), f), g), t), app(app(g, x), h))),
                         app(app(app(app(insert(), f), g), nil()), x) -> app(app(cons(), x), nil()),
                  app(app(app(sort(), f), g), app(app(cons(), h), t)) -> app(app(app(app(insert(), f), g), app(app(app(sort(), f), g), t)), h),
                                   app(app(app(sort(), f), g), nil()) -> nil(),
                                              app(app(max(), x), 0()) -> x,
                            app(app(max(), app(s(), x)), app(s(), y)) -> app(app(max(), x), y),
                                              app(app(max(), 0()), x) -> x,
                                              app(app(min(), x), 0()) -> 0(),
                            app(app(min(), app(s(), x)), app(s(), y)) -> app(app(min(), x), y),
                                              app(app(min(), 0()), x) -> 0(),
                                             app(ascending_sort(), l) -> app(app(app(sort(), min()), max()), l),
                                            app(descending_sort(), l) -> app(app(app(sort(), max()), min()), l)}
       Open