MAYBE
MAYBE
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)
 }
 DUP: We consider a duplicating system.
  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)
   }
  Fail