MAYBE
Time: 10.809759
TRS:
 {                 app(app(app(app(insert(), f), g), nil()), y) -> app(app(cons(), y), nil()),
  app(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app(app(cons(), app(app(f, x), y)), app(app(app(app(insert(), f), g), z), app(app(g, x), y))),
                             app(app(app(sort(), f), g), nil()) -> nil(),
            app(app(app(sort(), f), g), app(app(cons(), x), y)) -> app(app(app(app(insert(), f), g), app(app(app(sort(), f), g), y)), x),
                                        app(app(max(), x), 0()) -> x,
                      app(app(max(), app(s(), x)), app(s(), y)) -> app(app(max(), x), y),
                                        app(app(max(), 0()), y) -> y,
                                        app(app(min(), x), 0()) -> 0(),
                      app(app(min(), app(s(), x)), app(s(), y)) -> app(app(min(), x), y),
                                        app(app(min(), 0()), y) -> 0(),
                                                app(asort(), z) -> app(app(app(sort(), min()), max()), z),
                                                app(dsort(), z) -> app(app(app(sort(), max()), min()), z)}
 DP:
  DP:
   {                 app#(app(app(app(insert(), f), g), nil()), y) -> app#(app(cons(), y), nil()),
                     app#(app(app(app(insert(), f), g), nil()), y) -> app#(cons(), y),
    app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(f, x),
    app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(g, x),
    app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(f, x), y),
    app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(g, x), y),
    app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(app(app(insert(), f), g), z), app(app(g, x), y)),
    app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(app(insert(), f), g), z),
    app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(cons(), app(app(f, x), y)), app(app(app(app(insert(), f), g), z), app(app(g, x), y))),
    app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(cons(), app(app(f, x), y)),
              app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(app(insert(), f), g), app(app(app(sort(), f), g), y)), x),
              app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(sort(), f), g), y),
              app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(insert(), f), g), app(app(app(sort(), f), g), y)),
              app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(insert(), f), g),
              app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> 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#(asort(), z) -> app#(app(app(sort(), min()), max()), z),
                                                  app#(asort(), z) -> app#(app(sort(), min()), max()),
                                                  app#(asort(), z) -> app#(sort(), min()),
                                                  app#(dsort(), z) -> app#(app(app(sort(), max()), min()), z),
                                                  app#(dsort(), z) -> app#(app(sort(), max()), min()),
                                                  app#(dsort(), z) -> app#(sort(), max())}
  TRS:
  {                 app(app(app(app(insert(), f), g), nil()), y) -> app(app(cons(), y), nil()),
   app(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app(app(cons(), app(app(f, x), y)), app(app(app(app(insert(), f), g), z), app(app(g, x), y))),
                              app(app(app(sort(), f), g), nil()) -> nil(),
             app(app(app(sort(), f), g), app(app(cons(), x), y)) -> app(app(app(app(insert(), f), g), app(app(app(sort(), f), g), y)), x),
                                         app(app(max(), x), 0()) -> x,
                       app(app(max(), app(s(), x)), app(s(), y)) -> app(app(max(), x), y),
                                         app(app(max(), 0()), y) -> y,
                                         app(app(min(), x), 0()) -> 0(),
                       app(app(min(), app(s(), x)), app(s(), y)) -> app(app(min(), x), y),
                                         app(app(min(), 0()), y) -> 0(),
                                                 app(asort(), z) -> app(app(app(sort(), min()), max()), z),
                                                 app(dsort(), z) -> app(app(app(sort(), max()), min()), z)}
  EDG:
   {
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(f, x), y), app#(dsort(), z) -> app#(sort(), max()))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(f, x), y), app#(dsort(), z) -> app#(app(sort(), max()), min()))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(f, x), y), app#(dsort(), z) -> app#(app(app(sort(), max()), min()), z))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(f, x), y), app#(asort(), z) -> app#(sort(), min()))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(f, x), y), app#(asort(), z) -> app#(app(sort(), min()), max()))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(f, x), y), app#(asort(), z) -> app#(app(app(sort(), min()), max()), z))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(f, x), y), app#(app(min(), app(s(), x)), app(s(), y)) -> app#(min(), x))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(f, x), y), app#(app(min(), app(s(), x)), app(s(), y)) -> app#(app(min(), x), y))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(f, x), y), app#(app(max(), app(s(), x)), app(s(), y)) -> app#(max(), x))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(f, x), y), app#(app(max(), app(s(), x)), app(s(), y)) -> app#(app(max(), x), y))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(f, x), y), app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(insert(), f))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(f, x), y), app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(insert(), f), g))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(f, x), y), app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(insert(), f), g), app(app(app(sort(), f), g), y)))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(f, x), y), app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(sort(), f), g), y))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(f, x), y), app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(app(insert(), f), g), app(app(app(sort(), f), g), y)), x))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(f, x), y), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(cons(), app(app(f, x), y)))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(f, x), y), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(cons(), app(app(f, x), y)), app(app(app(app(insert(), f), g), z), app(app(g, x), y))))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(f, x), y), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(app(insert(), f), g), z))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(f, x), y), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(app(app(insert(), f), g), z), app(app(g, x), y)))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(f, x), y), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(g, x), y))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(f, x), y), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(f, x), y))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(f, x), y), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(g, x))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(f, x), y), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(f, x))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(f, x), y), app#(app(app(app(insert(), f), g), nil()), y) -> app#(cons(), y))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(f, x), y), app#(app(app(app(insert(), f), g), nil()), y) -> app#(app(cons(), y), nil()))
    (app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(sort(), f), g), y), app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(insert(), f))
    (app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(sort(), f), g), y), app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(insert(), f), g))
    (app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(sort(), f), g), y), app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(insert(), f), g), app(app(app(sort(), f), g), y)))
    (app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(sort(), f), g), y), app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(sort(), f), g), y))
    (app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(sort(), f), g), y), app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(app(insert(), f), g), app(app(app(sort(), f), g), y)), 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#(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(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(f, x), app#(dsort(), z) -> app#(sort(), max()))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(f, x), app#(dsort(), z) -> app#(app(sort(), max()), min()))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(f, x), app#(dsort(), z) -> app#(app(app(sort(), max()), min()), z))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(f, x), app#(asort(), z) -> app#(sort(), min()))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(f, x), app#(asort(), z) -> app#(app(sort(), min()), max()))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(f, x), app#(asort(), z) -> app#(app(app(sort(), min()), max()), z))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> 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(), x), z)), y) -> 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(), x), z)), y) -> 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(), x), z)), y) -> 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(), x), z)), y) -> app#(f, x), app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(insert(), f))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(f, x), app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(insert(), f), g))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(f, x), app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(insert(), f), g), app(app(app(sort(), f), g), y)))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(f, x), app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(sort(), f), g), y))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(f, x), app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(app(insert(), f), g), app(app(app(sort(), f), g), y)), x))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(f, x), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(cons(), app(app(f, x), y)))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(f, x), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(cons(), app(app(f, x), y)), app(app(app(app(insert(), f), g), z), app(app(g, x), y))))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(f, x), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(app(insert(), f), g), z))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(f, x), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(app(app(insert(), f), g), z), app(app(g, x), y)))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(f, x), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(g, x), y))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(f, x), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(f, x), y))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(f, x), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(g, x))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(f, x), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(f, x))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(f, x), app#(app(app(app(insert(), f), g), nil()), y) -> app#(cons(), y))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(f, x), app#(app(app(app(insert(), f), g), nil()), y) -> app#(app(cons(), y), nil()))
    (app#(dsort(), z) -> app#(app(app(sort(), max()), min()), z), app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(insert(), f))
    (app#(dsort(), z) -> app#(app(app(sort(), max()), min()), z), app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(insert(), f), g))
    (app#(dsort(), z) -> app#(app(app(sort(), max()), min()), z), app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(insert(), f), g), app(app(app(sort(), f), g), y)))
    (app#(dsort(), z) -> app#(app(app(sort(), max()), min()), z), app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(sort(), f), g), y))
    (app#(dsort(), z) -> app#(app(app(sort(), max()), min()), z), app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(app(insert(), f), g), app(app(app(sort(), f), g), y)), x))
    (app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(app(insert(), f), g), app(app(app(sort(), f), g), y)), x), app#(app(app(app(insert(), f), g), nil()), y) -> app#(app(cons(), y), nil()))
    (app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(app(insert(), f), g), app(app(app(sort(), f), g), y)), x), app#(app(app(app(insert(), f), g), nil()), y) -> app#(cons(), y))
    (app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(app(insert(), f), g), app(app(app(sort(), f), g), y)), x), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(f, x))
    (app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(app(insert(), f), g), app(app(app(sort(), f), g), y)), x), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(g, x))
    (app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(app(insert(), f), g), app(app(app(sort(), f), g), y)), x), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(f, x), y))
    (app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(app(insert(), f), g), app(app(app(sort(), f), g), y)), x), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(g, x), y))
    (app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(app(insert(), f), g), app(app(app(sort(), f), g), y)), x), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(app(app(insert(), f), g), z), app(app(g, x), y)))
    (app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(app(insert(), f), g), app(app(app(sort(), f), g), y)), x), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(app(insert(), f), g), z))
    (app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(app(insert(), f), g), app(app(app(sort(), f), g), y)), x), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(cons(), app(app(f, x), y)), app(app(app(app(insert(), f), g), z), app(app(g, x), y))))
    (app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(app(insert(), f), g), app(app(app(sort(), f), g), y)), x), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(cons(), app(app(f, x), y)))
    (app#(asort(), z) -> app#(app(app(sort(), min()), max()), z), app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(app(insert(), f), g), app(app(app(sort(), f), g), y)), x))
    (app#(asort(), z) -> app#(app(app(sort(), min()), max()), z), app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(sort(), f), g), y))
    (app#(asort(), z) -> app#(app(app(sort(), min()), max()), z), app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(insert(), f), g), app(app(app(sort(), f), g), y)))
    (app#(asort(), z) -> app#(app(app(sort(), min()), max()), z), app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(insert(), f), g))
    (app#(asort(), z) -> app#(app(app(sort(), min()), max()), z), app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(insert(), f))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(app(app(insert(), f), g), z), app(app(g, x), y)), app#(app(app(app(insert(), f), g), nil()), y) -> app#(app(cons(), y), nil()))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(app(app(insert(), f), g), z), app(app(g, x), y)), app#(app(app(app(insert(), f), g), nil()), y) -> app#(cons(), y))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(app(app(insert(), f), g), z), app(app(g, x), y)), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(f, x))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(app(app(insert(), f), g), z), app(app(g, x), y)), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(g, x))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(app(app(insert(), f), g), z), app(app(g, x), y)), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(f, x), y))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(app(app(insert(), f), g), z), app(app(g, x), y)), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(g, x), y))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(app(app(insert(), f), g), z), app(app(g, x), y)), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(app(app(insert(), f), g), z), app(app(g, x), y)))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(app(app(insert(), f), g), z), app(app(g, x), y)), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(app(insert(), f), g), z))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(app(app(insert(), f), g), z), app(app(g, x), y)), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(cons(), app(app(f, x), y)), app(app(app(app(insert(), f), g), z), app(app(g, x), y))))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(app(app(insert(), f), g), z), app(app(g, x), y)), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(cons(), app(app(f, x), y)))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(g, x), app#(app(app(app(insert(), f), g), nil()), y) -> app#(app(cons(), y), nil()))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(g, x), app#(app(app(app(insert(), f), g), nil()), y) -> app#(cons(), y))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(g, x), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(f, x))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(g, x), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(g, x))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(g, x), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(f, x), y))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(g, x), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(g, x), y))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(g, x), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(app(app(insert(), f), g), z), app(app(g, x), y)))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(g, x), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(app(insert(), f), g), z))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(g, x), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(cons(), app(app(f, x), y)), app(app(app(app(insert(), f), g), z), app(app(g, x), y))))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(g, x), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(cons(), app(app(f, x), y)))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(g, x), app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(app(insert(), f), g), app(app(app(sort(), f), g), y)), x))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(g, x), app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(sort(), f), g), y))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(g, x), app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(insert(), f), g), app(app(app(sort(), f), g), y)))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(g, x), app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(insert(), f), g))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(g, x), app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(insert(), f))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> 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(), x), z)), y) -> 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(), x), z)), y) -> 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(), x), z)), y) -> 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(), x), z)), y) -> app#(g, x), app#(asort(), z) -> app#(app(app(sort(), min()), max()), z))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(g, x), app#(asort(), z) -> app#(app(sort(), min()), max()))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(g, x), app#(asort(), z) -> app#(sort(), min()))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(g, x), app#(dsort(), z) -> app#(app(app(sort(), max()), min()), z))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(g, x), app#(dsort(), z) -> app#(app(sort(), max()), min()))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(g, x), app#(dsort(), z) -> app#(sort(), max()))
    (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(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(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(g, x), y), app#(app(app(app(insert(), f), g), nil()), y) -> app#(app(cons(), y), nil()))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(g, x), y), app#(app(app(app(insert(), f), g), nil()), y) -> app#(cons(), y))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(g, x), y), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(f, x))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(g, x), y), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(g, x))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(g, x), y), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(f, x), y))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(g, x), y), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(g, x), y))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(g, x), y), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(app(app(insert(), f), g), z), app(app(g, x), y)))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(g, x), y), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(app(insert(), f), g), z))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(g, x), y), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(cons(), app(app(f, x), y)), app(app(app(app(insert(), f), g), z), app(app(g, x), y))))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(g, x), y), app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(cons(), app(app(f, x), y)))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(g, x), y), app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(app(insert(), f), g), app(app(app(sort(), f), g), y)), x))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(g, x), y), app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(sort(), f), g), y))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(g, x), y), app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(insert(), f), g), app(app(app(sort(), f), g), y)))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(g, x), y), app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(insert(), f), g))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(g, x), y), app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(insert(), f))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(g, x), y), app#(app(max(), app(s(), x)), app(s(), y)) -> app#(app(max(), x), y))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(g, x), y), app#(app(max(), app(s(), x)), app(s(), y)) -> app#(max(), x))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(g, x), y), app#(app(min(), app(s(), x)), app(s(), y)) -> app#(app(min(), x), y))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(g, x), y), app#(app(min(), app(s(), x)), app(s(), y)) -> app#(min(), x))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(g, x), y), app#(asort(), z) -> app#(app(app(sort(), min()), max()), z))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(g, x), y), app#(asort(), z) -> app#(app(sort(), min()), max()))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(g, x), y), app#(asort(), z) -> app#(sort(), min()))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(g, x), y), app#(dsort(), z) -> app#(app(app(sort(), max()), min()), z))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(g, x), y), app#(dsort(), z) -> app#(app(sort(), max()), min()))
    (app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(g, x), y), app#(dsort(), z) -> app#(sort(), max()))
   }
   STATUS:
    arrows: 0.777600
    SCCS (3):
     Scc:
      {app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(f, x),
       app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(g, x),
       app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(f, x), y),
       app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(g, x), y),
       app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(app(app(insert(), f), g), z), app(app(g, x), y)),
                 app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(app(insert(), f), g), app(app(app(sort(), f), g), y)), x),
                 app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(sort(), f), g), y),
                                                     app#(asort(), z) -> app#(app(app(sort(), min()), max()), z),
                                                     app#(dsort(), z) -> app#(app(app(sort(), max()), min()), z)}
     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(), x), z)), y) -> app#(f, x),
        app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(g, x),
        app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(f, x), y),
        app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(g, x), y),
        app#(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app#(app(app(app(insert(), f), g), z), app(app(g, x), y)),
                  app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(app(insert(), f), g), app(app(app(sort(), f), g), y)), x),
                  app#(app(app(sort(), f), g), app(app(cons(), x), y)) -> app#(app(app(sort(), f), g), y),
                                                      app#(asort(), z) -> app#(app(app(sort(), min()), max()), z),
                                                      app#(dsort(), z) -> app#(app(app(sort(), max()), min()), z)}
      Weak:
      {                 app(app(app(app(insert(), f), g), nil()), y) -> app(app(cons(), y), nil()),
       app(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app(app(cons(), app(app(f, x), y)), app(app(app(app(insert(), f), g), z), app(app(g, x), y))),
                                  app(app(app(sort(), f), g), nil()) -> nil(),
                 app(app(app(sort(), f), g), app(app(cons(), x), y)) -> app(app(app(app(insert(), f), g), app(app(app(sort(), f), g), y)), x),
                                             app(app(max(), x), 0()) -> x,
                           app(app(max(), app(s(), x)), app(s(), y)) -> app(app(max(), x), y),
                                             app(app(max(), 0()), y) -> y,
                                             app(app(min(), x), 0()) -> 0(),
                           app(app(min(), app(s(), x)), app(s(), y)) -> app(app(min(), x), y),
                                             app(app(min(), 0()), y) -> 0(),
                                                     app(asort(), z) -> app(app(app(sort(), min()), max()), z),
                                                     app(dsort(), z) -> app(app(app(sort(), max()), min()), z)}
      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), nil()), y) -> app(app(cons(), y), nil()),
       app(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app(app(cons(), app(app(f, x), y)), app(app(app(app(insert(), f), g), z), app(app(g, x), y))),
                                  app(app(app(sort(), f), g), nil()) -> nil(),
                 app(app(app(sort(), f), g), app(app(cons(), x), y)) -> app(app(app(app(insert(), f), g), app(app(app(sort(), f), g), y)), x),
                                             app(app(max(), x), 0()) -> x,
                           app(app(max(), app(s(), x)), app(s(), y)) -> app(app(max(), x), y),
                                             app(app(max(), 0()), y) -> y,
                                             app(app(min(), x), 0()) -> 0(),
                           app(app(min(), app(s(), x)), app(s(), y)) -> app(app(min(), x), y),
                                             app(app(min(), 0()), y) -> 0(),
                                                     app(asort(), z) -> app(app(app(sort(), min()), max()), z),
                                                     app(dsort(), z) -> app(app(app(sort(), max()), min()), z)}
      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), nil()), y) -> app(app(cons(), y), nil()),
       app(app(app(app(insert(), f), g), app(app(cons(), x), z)), y) -> app(app(cons(), app(app(f, x), y)), app(app(app(app(insert(), f), g), z), app(app(g, x), y))),
                                  app(app(app(sort(), f), g), nil()) -> nil(),
                 app(app(app(sort(), f), g), app(app(cons(), x), y)) -> app(app(app(app(insert(), f), g), app(app(app(sort(), f), g), y)), x),
                                             app(app(max(), x), 0()) -> x,
                           app(app(max(), app(s(), x)), app(s(), y)) -> app(app(max(), x), y),
                                             app(app(max(), 0()), y) -> y,
                                             app(app(min(), x), 0()) -> 0(),
                           app(app(min(), app(s(), x)), app(s(), y)) -> app(app(min(), x), y),
                                             app(app(min(), 0()), y) -> 0(),
                                                     app(asort(), z) -> app(app(app(sort(), min()), max()), z),
                                                     app(dsort(), z) -> app(app(app(sort(), max()), min()), z)}
      Open