MAYBE
Time: 0.364836
TRS:
 {  app(app(app(app(if_replace(), true()), n), m), app(app(cons(), k), x)) -> app(app(cons(), m), x),
   app(app(app(app(if_replace(), false()), n), m), app(app(cons(), k), x)) -> app(app(cons(), k), app(app(app(replace(), n), m), x)),
                           app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs)),
                          app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs),
                    app(app(app(replace(), n), m), app(app(cons(), k), x)) -> app(app(app(app(if_replace(), app(app(eq(), n), k)), n), m), app(app(cons(), k), x)),
                                     app(app(app(replace(), n), m), nil()) -> nil(),
                                  app(app(eq(), app(s(), n)), app(s(), m)) -> app(app(eq(), n), m),
                                          app(app(eq(), app(s(), n)), 0()) -> false(),
                                          app(app(eq(), 0()), app(s(), m)) -> false(),
                                                  app(app(eq(), 0()), 0()) -> true(),
                                  app(app(le(), app(s(), n)), app(s(), m)) -> app(app(le(), n), m),
                                          app(app(le(), app(s(), n)), 0()) -> false(),
                                                    app(app(le(), 0()), m) -> true(),
   app(app(if_min(), true()), app(app(cons(), n), app(app(cons(), m), x))) -> app(min(), app(app(cons(), n), x)),
  app(app(if_min(), false()), app(app(cons(), n), app(app(cons(), m), x))) -> app(min(), app(app(cons(), m), x)),
                               app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)),
                                                 app(app(map(), f), nil()) -> nil(),
                            app(app(filter(), f), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(f, x)), f), x), xs),
                                              app(app(filter(), f), nil()) -> nil(),
                   app(min(), app(app(cons(), n), app(app(cons(), m), x))) -> app(app(if_min(), app(app(le(), n), m)), app(app(cons(), n), app(app(cons(), m), x))),
                          app(min(), app(app(cons(), app(s(), n)), nil())) -> app(s(), n),
                                  app(min(), app(app(cons(), 0()), nil())) -> 0(),
                                       app(sort(), app(app(cons(), n), x)) -> app(app(cons(), app(min(), app(app(cons(), n), x))), app(sort(), app(app(app(replace(), app(min(), app(app(cons(), n), x))), n), x))),
                                                        app(sort(), nil()) -> nil()}
 DP:
  DP:
   {  app#(app(app(app(if_replace(), true()), n), m), app(app(cons(), k), x)) -> app#(app(cons(), m), x),
      app#(app(app(app(if_replace(), true()), n), m), app(app(cons(), k), x)) -> app#(cons(), m),
     app#(app(app(app(if_replace(), false()), n), m), app(app(cons(), k), x)) -> app#(app(app(replace(), n), m), x),
     app#(app(app(app(if_replace(), false()), n), m), app(app(cons(), k), x)) -> app#(app(cons(), k), app(app(app(replace(), n), m), x)),
     app#(app(app(app(if_replace(), false()), n), m), app(app(cons(), k), x)) -> app#(app(replace(), n), m),
     app#(app(app(app(if_replace(), false()), n), m), app(app(cons(), k), x)) -> app#(replace(), n),
                             app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(cons(), x), app(app(filter(), f), xs)),
                             app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(filter(), f), xs),
                             app#(app(app(app(filter2(), true()), f), x), xs) -> app#(cons(), x),
                             app#(app(app(app(filter2(), true()), f), x), xs) -> app#(filter(), f),
                            app#(app(app(app(filter2(), false()), f), x), xs) -> app#(app(filter(), f), xs),
                            app#(app(app(app(filter2(), false()), f), x), xs) -> app#(filter(), f),
                      app#(app(app(replace(), n), m), app(app(cons(), k), x)) -> app#(app(app(app(if_replace(), app(app(eq(), n), k)), n), m), app(app(cons(), k), x)),
                      app#(app(app(replace(), n), m), app(app(cons(), k), x)) -> app#(app(app(if_replace(), app(app(eq(), n), k)), n), m),
                      app#(app(app(replace(), n), m), app(app(cons(), k), x)) -> app#(app(eq(), n), k),
                      app#(app(app(replace(), n), m), app(app(cons(), k), x)) -> app#(app(if_replace(), app(app(eq(), n), k)), n),
                      app#(app(app(replace(), n), m), app(app(cons(), k), x)) -> app#(eq(), n),
                      app#(app(app(replace(), n), m), app(app(cons(), k), x)) -> app#(if_replace(), app(app(eq(), n), k)),
                                    app#(app(eq(), app(s(), n)), app(s(), m)) -> app#(app(eq(), n), m),
                                    app#(app(eq(), app(s(), n)), app(s(), m)) -> app#(eq(), n),
                                    app#(app(le(), app(s(), n)), app(s(), m)) -> app#(app(le(), n), m),
                                    app#(app(le(), app(s(), n)), app(s(), m)) -> app#(le(), n),
     app#(app(if_min(), true()), app(app(cons(), n), app(app(cons(), m), x))) -> app#(app(cons(), n), x),
     app#(app(if_min(), true()), app(app(cons(), n), app(app(cons(), m), x))) -> app#(min(), app(app(cons(), n), x)),
    app#(app(if_min(), false()), app(app(cons(), n), app(app(cons(), m), x))) -> app#(min(), app(app(cons(), m), x)),
                                 app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x),
                                 app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(cons(), app(f, x)), app(app(map(), f), xs)),
                                 app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs),
                                 app#(app(map(), f), app(app(cons(), x), xs)) -> app#(cons(), app(f, x)),
                              app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x),
                              app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(app(filter2(), app(f, x)), f), x), xs),
                              app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(filter2(), app(f, x)), f), x),
                              app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(filter2(), app(f, x)), f),
                              app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(filter2(), app(f, x)),
                     app#(min(), app(app(cons(), n), app(app(cons(), m), x))) -> app#(app(le(), n), m),
                     app#(min(), app(app(cons(), n), app(app(cons(), m), x))) -> app#(app(if_min(), app(app(le(), n), m)), app(app(cons(), n), app(app(cons(), m), x))),
                     app#(min(), app(app(cons(), n), app(app(cons(), m), x))) -> app#(le(), n),
                     app#(min(), app(app(cons(), n), app(app(cons(), m), x))) -> app#(if_min(), app(app(le(), n), m)),
                                         app#(sort(), app(app(cons(), n), x)) -> app#(app(app(replace(), app(min(), app(app(cons(), n), x))), n), x),
                                         app#(sort(), app(app(cons(), n), x)) -> app#(app(cons(), app(min(), app(app(cons(), n), x))), app(sort(), app(app(app(replace(), app(min(), app(app(cons(), n), x))), n), x))),
                                         app#(sort(), app(app(cons(), n), x)) -> app#(app(replace(), app(min(), app(app(cons(), n), x))), n),
                                         app#(sort(), app(app(cons(), n), x)) -> app#(min(), app(app(cons(), n), x)),
                                         app#(sort(), app(app(cons(), n), x)) -> app#(cons(), app(min(), app(app(cons(), n), x))),
                                         app#(sort(), app(app(cons(), n), x)) -> app#(replace(), app(min(), app(app(cons(), n), x))),
                                         app#(sort(), app(app(cons(), n), x)) -> app#(sort(), app(app(app(replace(), app(min(), app(app(cons(), n), x))), n), x))}
  TRS:
  {  app(app(app(app(if_replace(), true()), n), m), app(app(cons(), k), x)) -> app(app(cons(), m), x),
    app(app(app(app(if_replace(), false()), n), m), app(app(cons(), k), x)) -> app(app(cons(), k), app(app(app(replace(), n), m), x)),
                            app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs)),
                           app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs),
                     app(app(app(replace(), n), m), app(app(cons(), k), x)) -> app(app(app(app(if_replace(), app(app(eq(), n), k)), n), m), app(app(cons(), k), x)),
                                      app(app(app(replace(), n), m), nil()) -> nil(),
                                   app(app(eq(), app(s(), n)), app(s(), m)) -> app(app(eq(), n), m),
                                           app(app(eq(), app(s(), n)), 0()) -> false(),
                                           app(app(eq(), 0()), app(s(), m)) -> false(),
                                                   app(app(eq(), 0()), 0()) -> true(),
                                   app(app(le(), app(s(), n)), app(s(), m)) -> app(app(le(), n), m),
                                           app(app(le(), app(s(), n)), 0()) -> false(),
                                                     app(app(le(), 0()), m) -> true(),
    app(app(if_min(), true()), app(app(cons(), n), app(app(cons(), m), x))) -> app(min(), app(app(cons(), n), x)),
   app(app(if_min(), false()), app(app(cons(), n), app(app(cons(), m), x))) -> app(min(), app(app(cons(), m), x)),
                                app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)),
                                                  app(app(map(), f), nil()) -> nil(),
                             app(app(filter(), f), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(f, x)), f), x), xs),
                                               app(app(filter(), f), nil()) -> nil(),
                    app(min(), app(app(cons(), n), app(app(cons(), m), x))) -> app(app(if_min(), app(app(le(), n), m)), app(app(cons(), n), app(app(cons(), m), x))),
                           app(min(), app(app(cons(), app(s(), n)), nil())) -> app(s(), n),
                                   app(min(), app(app(cons(), 0()), nil())) -> 0(),
                                        app(sort(), app(app(cons(), n), x)) -> app(app(cons(), app(min(), app(app(cons(), n), x))), app(sort(), app(app(app(replace(), app(min(), app(app(cons(), n), x))), n), x))),
                                                         app(sort(), nil()) -> nil()}
  UR:
   {  app(app(app(app(if_replace(), true()), n), m), app(app(cons(), k), x)) -> app(app(cons(), m), x),
     app(app(app(app(if_replace(), false()), n), m), app(app(cons(), k), x)) -> app(app(cons(), k), app(app(app(replace(), n), m), x)),
                             app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs)),
                            app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs),
                      app(app(app(replace(), n), m), app(app(cons(), k), x)) -> app(app(app(app(if_replace(), app(app(eq(), n), k)), n), m), app(app(cons(), k), x)),
                                       app(app(app(replace(), n), m), nil()) -> nil(),
                                    app(app(eq(), app(s(), n)), app(s(), m)) -> app(app(eq(), n), m),
                                            app(app(eq(), app(s(), n)), 0()) -> false(),
                                            app(app(eq(), 0()), app(s(), m)) -> false(),
                                                    app(app(eq(), 0()), 0()) -> true(),
                                    app(app(le(), app(s(), n)), app(s(), m)) -> app(app(le(), n), m),
                                            app(app(le(), app(s(), n)), 0()) -> false(),
                                                      app(app(le(), 0()), m) -> true(),
     app(app(if_min(), true()), app(app(cons(), n), app(app(cons(), m), x))) -> app(min(), app(app(cons(), n), x)),
    app(app(if_min(), false()), app(app(cons(), n), app(app(cons(), m), x))) -> app(min(), app(app(cons(), m), x)),
                                 app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)),
                                                   app(app(map(), f), nil()) -> nil(),
                              app(app(filter(), f), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(f, x)), f), x), xs),
                                                app(app(filter(), f), nil()) -> nil(),
                     app(min(), app(app(cons(), n), app(app(cons(), m), x))) -> app(app(if_min(), app(app(le(), n), m)), app(app(cons(), n), app(app(cons(), m), x))),
                            app(min(), app(app(cons(), app(s(), n)), nil())) -> app(s(), n),
                                    app(min(), app(app(cons(), 0()), nil())) -> 0(),
                                         app(sort(), app(app(cons(), n), x)) -> app(app(cons(), app(min(), app(app(cons(), n), x))), app(sort(), app(app(app(replace(), app(min(), app(app(cons(), n), x))), n), x))),
                                                          app(sort(), nil()) -> nil()}
   EDG:
    {
     (app#(app(app(replace(), n), m), app(app(cons(), k), x)) -> app#(app(app(app(if_replace(), app(app(eq(), n), k)), n), m), app(app(cons(), k), x)), app#(app(app(app(if_replace(), false()), n), m), app(app(cons(), k), x)) -> app#(replace(), n))
     (app#(app(app(replace(), n), m), app(app(cons(), k), x)) -> app#(app(app(app(if_replace(), app(app(eq(), n), k)), n), m), app(app(cons(), k), x)), app#(app(app(app(if_replace(), false()), n), m), app(app(cons(), k), x)) -> app#(app(replace(), n), m))
     (app#(app(app(replace(), n), m), app(app(cons(), k), x)) -> app#(app(app(app(if_replace(), app(app(eq(), n), k)), n), m), app(app(cons(), k), x)), app#(app(app(app(if_replace(), false()), n), m), app(app(cons(), k), x)) -> app#(app(cons(), k), app(app(app(replace(), n), m), x)))
     (app#(app(app(replace(), n), m), app(app(cons(), k), x)) -> app#(app(app(app(if_replace(), app(app(eq(), n), k)), n), m), app(app(cons(), k), x)), app#(app(app(app(if_replace(), false()), n), m), app(app(cons(), k), x)) -> app#(app(app(replace(), n), m), x))
     (app#(app(app(replace(), n), m), app(app(cons(), k), x)) -> app#(app(app(app(if_replace(), app(app(eq(), n), k)), n), m), app(app(cons(), k), x)), app#(app(app(app(if_replace(), true()), n), m), app(app(cons(), k), x)) -> app#(cons(), m))
     (app#(app(app(replace(), n), m), app(app(cons(), k), x)) -> app#(app(app(app(if_replace(), app(app(eq(), n), k)), n), m), app(app(cons(), k), x)), app#(app(app(app(if_replace(), true()), n), m), app(app(cons(), k), x)) -> app#(app(cons(), m), x))
     (app#(app(if_min(), true()), app(app(cons(), n), app(app(cons(), m), x))) -> app#(min(), app(app(cons(), n), x)), app#(min(), app(app(cons(), n), app(app(cons(), m), x))) -> app#(if_min(), app(app(le(), n), m)))
     (app#(app(if_min(), true()), app(app(cons(), n), app(app(cons(), m), x))) -> app#(min(), app(app(cons(), n), x)), app#(min(), app(app(cons(), n), app(app(cons(), m), x))) -> app#(le(), n))
     (app#(app(if_min(), true()), app(app(cons(), n), app(app(cons(), m), x))) -> app#(min(), app(app(cons(), n), x)), app#(min(), app(app(cons(), n), app(app(cons(), m), x))) -> app#(app(if_min(), app(app(le(), n), m)), app(app(cons(), n), app(app(cons(), m), x))))
     (app#(app(if_min(), true()), app(app(cons(), n), app(app(cons(), m), x))) -> app#(min(), app(app(cons(), n), x)), app#(min(), app(app(cons(), n), app(app(cons(), m), x))) -> app#(app(le(), n), m))
     (app#(sort(), app(app(cons(), n), x)) -> app#(min(), app(app(cons(), n), x)), app#(min(), app(app(cons(), n), app(app(cons(), m), x))) -> app#(if_min(), app(app(le(), n), m)))
     (app#(sort(), app(app(cons(), n), x)) -> app#(min(), app(app(cons(), n), x)), app#(min(), app(app(cons(), n), app(app(cons(), m), x))) -> app#(le(), n))
     (app#(sort(), app(app(cons(), n), x)) -> app#(min(), app(app(cons(), n), x)), app#(min(), app(app(cons(), n), app(app(cons(), m), x))) -> app#(app(if_min(), app(app(le(), n), m)), app(app(cons(), n), app(app(cons(), m), x))))
     (app#(sort(), app(app(cons(), n), x)) -> app#(min(), app(app(cons(), n), x)), app#(min(), app(app(cons(), n), app(app(cons(), m), x))) -> app#(app(le(), n), m))
     (app#(app(app(app(filter2(), false()), f), x), xs) -> app#(app(filter(), f), xs), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(filter2(), app(f, x)))
     (app#(app(app(app(filter2(), false()), f), x), xs) -> app#(app(filter(), f), xs), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(filter2(), app(f, x)), f))
     (app#(app(app(app(filter2(), false()), f), x), xs) -> app#(app(filter(), f), xs), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(filter2(), app(f, x)), f), x))
     (app#(app(app(app(filter2(), false()), f), x), xs) -> app#(app(filter(), f), xs), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(app(filter2(), app(f, x)), f), x), xs))
     (app#(app(app(app(filter2(), false()), f), x), xs) -> app#(app(filter(), f), xs), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(app(filter2(), app(f, x)), f), x), xs), app#(app(app(app(filter2(), false()), f), x), xs) -> app#(filter(), f))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(app(filter2(), app(f, x)), f), x), xs), app#(app(app(app(filter2(), false()), f), x), xs) -> app#(app(filter(), f), xs))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(app(filter2(), app(f, x)), f), x), xs), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(filter(), f))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(app(filter2(), app(f, x)), f), x), xs), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(cons(), x))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(app(filter2(), app(f, x)), f), x), xs), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(filter(), f), xs))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(app(filter2(), app(f, x)), f), x), xs), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(cons(), x), app(app(filter(), f), xs)))
     (app#(app(app(replace(), n), m), app(app(cons(), k), x)) -> app#(app(eq(), n), k), app#(app(eq(), app(s(), n)), app(s(), m)) -> app#(eq(), n))
     (app#(app(app(replace(), n), m), app(app(cons(), k), x)) -> app#(app(eq(), n), k), app#(app(eq(), app(s(), n)), app(s(), m)) -> app#(app(eq(), n), m))
     (app#(app(app(app(if_replace(), false()), n), m), app(app(cons(), k), x)) -> app#(app(app(replace(), n), m), x), app#(app(app(replace(), n), m), app(app(cons(), k), x)) -> app#(if_replace(), app(app(eq(), n), k)))
     (app#(app(app(app(if_replace(), false()), n), m), app(app(cons(), k), x)) -> app#(app(app(replace(), n), m), x), app#(app(app(replace(), n), m), app(app(cons(), k), x)) -> app#(eq(), n))
     (app#(app(app(app(if_replace(), false()), n), m), app(app(cons(), k), x)) -> app#(app(app(replace(), n), m), x), app#(app(app(replace(), n), m), app(app(cons(), k), x)) -> app#(app(if_replace(), app(app(eq(), n), k)), n))
     (app#(app(app(app(if_replace(), false()), n), m), app(app(cons(), k), x)) -> app#(app(app(replace(), n), m), x), app#(app(app(replace(), n), m), app(app(cons(), k), x)) -> app#(app(eq(), n), k))
     (app#(app(app(app(if_replace(), false()), n), m), app(app(cons(), k), x)) -> app#(app(app(replace(), n), m), x), app#(app(app(replace(), n), m), app(app(cons(), k), x)) -> app#(app(app(if_replace(), app(app(eq(), n), k)), n), m))
     (app#(app(app(app(if_replace(), false()), n), m), app(app(cons(), k), x)) -> app#(app(app(replace(), n), m), x), app#(app(app(replace(), n), m), app(app(cons(), k), x)) -> app#(app(app(app(if_replace(), app(app(eq(), n), k)), n), m), app(app(cons(), k), x)))
     (app#(app(eq(), app(s(), n)), app(s(), m)) -> app#(app(eq(), n), m), app#(app(eq(), app(s(), n)), app(s(), m)) -> app#(eq(), n))
     (app#(app(eq(), app(s(), n)), app(s(), m)) -> app#(app(eq(), n), m), app#(app(eq(), app(s(), n)), app(s(), m)) -> app#(app(eq(), n), m))
     (app#(min(), app(app(cons(), n), app(app(cons(), m), x))) -> app#(app(le(), n), m), app#(app(le(), app(s(), n)), app(s(), m)) -> app#(le(), n))
     (app#(min(), app(app(cons(), n), app(app(cons(), m), x))) -> app#(app(le(), n), m), app#(app(le(), app(s(), n)), app(s(), m)) -> app#(app(le(), n), m))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(sort(), app(app(cons(), n), x)) -> app#(sort(), app(app(app(replace(), app(min(), app(app(cons(), n), x))), n), x)))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(sort(), app(app(cons(), n), x)) -> app#(replace(), app(min(), app(app(cons(), n), x))))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(sort(), app(app(cons(), n), x)) -> app#(cons(), app(min(), app(app(cons(), n), x))))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(sort(), app(app(cons(), n), x)) -> app#(min(), app(app(cons(), n), x)))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(sort(), app(app(cons(), n), x)) -> app#(app(replace(), app(min(), app(app(cons(), n), x))), n))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(sort(), app(app(cons(), n), x)) -> app#(app(cons(), app(min(), app(app(cons(), n), x))), app(sort(), app(app(app(replace(), app(min(), app(app(cons(), n), x))), n), x))))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(sort(), app(app(cons(), n), x)) -> app#(app(app(replace(), app(min(), app(app(cons(), n), x))), n), x))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(min(), app(app(cons(), n), app(app(cons(), m), x))) -> app#(if_min(), app(app(le(), n), m)))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(min(), app(app(cons(), n), app(app(cons(), m), x))) -> app#(le(), n))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(min(), app(app(cons(), n), app(app(cons(), m), x))) -> app#(app(if_min(), app(app(le(), n), m)), app(app(cons(), n), app(app(cons(), m), x))))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(min(), app(app(cons(), n), app(app(cons(), m), x))) -> app#(app(le(), n), m))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(filter2(), app(f, x)))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(filter2(), app(f, x)), f))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(filter2(), app(f, x)), f), x))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(app(filter2(), app(f, x)), f), x), xs))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(cons(), app(f, x)))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(cons(), app(f, x)), app(app(map(), f), xs)))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(if_min(), false()), app(app(cons(), n), app(app(cons(), m), x))) -> app#(min(), app(app(cons(), m), x)))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(if_min(), true()), app(app(cons(), n), app(app(cons(), m), x))) -> app#(min(), app(app(cons(), n), x)))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(if_min(), true()), app(app(cons(), n), app(app(cons(), m), x))) -> app#(app(cons(), n), x))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(le(), app(s(), n)), app(s(), m)) -> app#(le(), n))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(le(), app(s(), n)), app(s(), m)) -> app#(app(le(), n), m))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(eq(), app(s(), n)), app(s(), m)) -> app#(eq(), n))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(eq(), app(s(), n)), app(s(), m)) -> app#(app(eq(), n), m))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(replace(), n), m), app(app(cons(), k), x)) -> app#(if_replace(), app(app(eq(), n), k)))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(replace(), n), m), app(app(cons(), k), x)) -> app#(eq(), n))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(replace(), n), m), app(app(cons(), k), x)) -> app#(app(if_replace(), app(app(eq(), n), k)), n))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(replace(), n), m), app(app(cons(), k), x)) -> app#(app(eq(), n), k))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(replace(), n), m), app(app(cons(), k), x)) -> app#(app(app(if_replace(), app(app(eq(), n), k)), n), m))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(replace(), n), m), app(app(cons(), k), x)) -> app#(app(app(app(if_replace(), app(app(eq(), n), k)), n), m), app(app(cons(), k), x)))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), false()), f), x), xs) -> app#(filter(), f))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), false()), f), x), xs) -> app#(app(filter(), f), xs))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(filter(), f))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(cons(), x))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(filter(), f), xs))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(cons(), x), app(app(filter(), f), xs)))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(if_replace(), false()), n), m), app(app(cons(), k), x)) -> app#(replace(), n))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(if_replace(), false()), n), m), app(app(cons(), k), x)) -> app#(app(replace(), n), m))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(if_replace(), false()), n), m), app(app(cons(), k), x)) -> app#(app(cons(), k), app(app(app(replace(), n), m), x)))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(if_replace(), false()), n), m), app(app(cons(), k), x)) -> app#(app(app(replace(), n), m), x))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(if_replace(), true()), n), m), app(app(cons(), k), x)) -> app#(cons(), m))
     (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(if_replace(), true()), n), m), app(app(cons(), k), x)) -> app#(app(cons(), m), x))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(if_replace(), true()), n), m), app(app(cons(), k), x)) -> app#(app(cons(), m), x))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(if_replace(), true()), n), m), app(app(cons(), k), x)) -> app#(cons(), m))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(if_replace(), false()), n), m), app(app(cons(), k), x)) -> app#(app(app(replace(), n), m), x))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(if_replace(), false()), n), m), app(app(cons(), k), x)) -> app#(app(cons(), k), app(app(app(replace(), n), m), x)))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(if_replace(), false()), n), m), app(app(cons(), k), x)) -> app#(app(replace(), n), m))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(if_replace(), false()), n), m), app(app(cons(), k), x)) -> app#(replace(), n))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(cons(), x), app(app(filter(), f), xs)))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(filter(), f), xs))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(cons(), x))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(filter(), f))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), false()), f), x), xs) -> app#(app(filter(), f), xs))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), false()), f), x), xs) -> app#(filter(), f))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(replace(), n), m), app(app(cons(), k), x)) -> app#(app(app(app(if_replace(), app(app(eq(), n), k)), n), m), app(app(cons(), k), x)))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(replace(), n), m), app(app(cons(), k), x)) -> app#(app(app(if_replace(), app(app(eq(), n), k)), n), m))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(replace(), n), m), app(app(cons(), k), x)) -> app#(app(eq(), n), k))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(replace(), n), m), app(app(cons(), k), x)) -> app#(app(if_replace(), app(app(eq(), n), k)), n))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(replace(), n), m), app(app(cons(), k), x)) -> app#(eq(), n))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(replace(), n), m), app(app(cons(), k), x)) -> app#(if_replace(), app(app(eq(), n), k)))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(eq(), app(s(), n)), app(s(), m)) -> app#(app(eq(), n), m))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(eq(), app(s(), n)), app(s(), m)) -> app#(eq(), n))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(le(), app(s(), n)), app(s(), m)) -> app#(app(le(), n), m))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(le(), app(s(), n)), app(s(), m)) -> app#(le(), n))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(if_min(), true()), app(app(cons(), n), app(app(cons(), m), x))) -> app#(app(cons(), n), x))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(if_min(), true()), app(app(cons(), n), app(app(cons(), m), x))) -> app#(min(), app(app(cons(), n), x)))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(if_min(), false()), app(app(cons(), n), app(app(cons(), m), x))) -> app#(min(), app(app(cons(), m), x)))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(cons(), app(f, x)), app(app(map(), f), xs)))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(cons(), app(f, x)))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(app(filter2(), app(f, x)), f), x), xs))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(filter2(), app(f, x)), f), x))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(filter2(), app(f, x)), f))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(filter2(), app(f, x)))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(min(), app(app(cons(), n), app(app(cons(), m), x))) -> app#(app(le(), n), m))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(min(), app(app(cons(), n), app(app(cons(), m), x))) -> app#(app(if_min(), app(app(le(), n), m)), app(app(cons(), n), app(app(cons(), m), x))))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(min(), app(app(cons(), n), app(app(cons(), m), x))) -> app#(le(), n))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(min(), app(app(cons(), n), app(app(cons(), m), x))) -> app#(if_min(), app(app(le(), n), m)))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(sort(), app(app(cons(), n), x)) -> app#(app(app(replace(), app(min(), app(app(cons(), n), x))), n), x))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(sort(), app(app(cons(), n), x)) -> app#(app(cons(), app(min(), app(app(cons(), n), x))), app(sort(), app(app(app(replace(), app(min(), app(app(cons(), n), x))), n), x))))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(sort(), app(app(cons(), n), x)) -> app#(app(replace(), app(min(), app(app(cons(), n), x))), n))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(sort(), app(app(cons(), n), x)) -> app#(min(), app(app(cons(), n), x)))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(sort(), app(app(cons(), n), x)) -> app#(cons(), app(min(), app(app(cons(), n), x))))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(sort(), app(app(cons(), n), x)) -> app#(replace(), app(min(), app(app(cons(), n), x))))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(sort(), app(app(cons(), n), x)) -> app#(sort(), app(app(app(replace(), app(min(), app(app(cons(), n), x))), n), x)))
     (app#(app(le(), app(s(), n)), app(s(), m)) -> app#(app(le(), n), m), app#(app(le(), app(s(), n)), app(s(), m)) -> app#(app(le(), n), m))
     (app#(app(le(), app(s(), n)), app(s(), m)) -> app#(app(le(), n), m), app#(app(le(), app(s(), n)), app(s(), m)) -> app#(le(), n))
     (app#(sort(), app(app(cons(), n), x)) -> app#(app(app(replace(), app(min(), app(app(cons(), n), x))), n), x), app#(app(app(replace(), n), m), app(app(cons(), k), x)) -> app#(app(app(app(if_replace(), app(app(eq(), n), k)), n), m), app(app(cons(), k), x)))
     (app#(sort(), app(app(cons(), n), x)) -> app#(app(app(replace(), app(min(), app(app(cons(), n), x))), n), x), app#(app(app(replace(), n), m), app(app(cons(), k), x)) -> app#(app(app(if_replace(), app(app(eq(), n), k)), n), m))
     (app#(sort(), app(app(cons(), n), x)) -> app#(app(app(replace(), app(min(), app(app(cons(), n), x))), n), x), app#(app(app(replace(), n), m), app(app(cons(), k), x)) -> app#(app(eq(), n), k))
     (app#(sort(), app(app(cons(), n), x)) -> app#(app(app(replace(), app(min(), app(app(cons(), n), x))), n), x), app#(app(app(replace(), n), m), app(app(cons(), k), x)) -> app#(app(if_replace(), app(app(eq(), n), k)), n))
     (app#(sort(), app(app(cons(), n), x)) -> app#(app(app(replace(), app(min(), app(app(cons(), n), x))), n), x), app#(app(app(replace(), n), m), app(app(cons(), k), x)) -> app#(eq(), n))
     (app#(sort(), app(app(cons(), n), x)) -> app#(app(app(replace(), app(min(), app(app(cons(), n), x))), n), x), app#(app(app(replace(), n), m), app(app(cons(), k), x)) -> app#(if_replace(), app(app(eq(), n), k)))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(cons(), app(f, x)), app(app(map(), f), xs)))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(cons(), app(f, x)))
     (app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(filter(), f), xs), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x))
     (app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(filter(), f), xs), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(app(filter2(), app(f, x)), f), x), xs))
     (app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(filter(), f), xs), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(filter2(), app(f, x)), f), x))
     (app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(filter(), f), xs), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(filter2(), app(f, x)), f))
     (app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(filter(), f), xs), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(filter2(), app(f, x)))
     (app#(sort(), app(app(cons(), n), x)) -> app#(sort(), app(app(app(replace(), app(min(), app(app(cons(), n), x))), n), x)), app#(sort(), app(app(cons(), n), x)) -> app#(app(app(replace(), app(min(), app(app(cons(), n), x))), n), x))
     (app#(sort(), app(app(cons(), n), x)) -> app#(sort(), app(app(app(replace(), app(min(), app(app(cons(), n), x))), n), x)), app#(sort(), app(app(cons(), n), x)) -> app#(app(cons(), app(min(), app(app(cons(), n), x))), app(sort(), app(app(app(replace(), app(min(), app(app(cons(), n), x))), n), x))))
     (app#(sort(), app(app(cons(), n), x)) -> app#(sort(), app(app(app(replace(), app(min(), app(app(cons(), n), x))), n), x)), app#(sort(), app(app(cons(), n), x)) -> app#(app(replace(), app(min(), app(app(cons(), n), x))), n))
     (app#(sort(), app(app(cons(), n), x)) -> app#(sort(), app(app(app(replace(), app(min(), app(app(cons(), n), x))), n), x)), app#(sort(), app(app(cons(), n), x)) -> app#(min(), app(app(cons(), n), x)))
     (app#(sort(), app(app(cons(), n), x)) -> app#(sort(), app(app(app(replace(), app(min(), app(app(cons(), n), x))), n), x)), app#(sort(), app(app(cons(), n), x)) -> app#(cons(), app(min(), app(app(cons(), n), x))))
     (app#(sort(), app(app(cons(), n), x)) -> app#(sort(), app(app(app(replace(), app(min(), app(app(cons(), n), x))), n), x)), app#(sort(), app(app(cons(), n), x)) -> app#(replace(), app(min(), app(app(cons(), n), x))))
     (app#(sort(), app(app(cons(), n), x)) -> app#(sort(), app(app(app(replace(), app(min(), app(app(cons(), n), x))), n), x)), app#(sort(), app(app(cons(), n), x)) -> app#(sort(), app(app(app(replace(), app(min(), app(app(cons(), n), x))), n), x)))
     (app#(app(if_min(), false()), app(app(cons(), n), app(app(cons(), m), x))) -> app#(min(), app(app(cons(), m), x)), app#(min(), app(app(cons(), n), app(app(cons(), m), x))) -> app#(app(le(), n), m))
     (app#(app(if_min(), false()), app(app(cons(), n), app(app(cons(), m), x))) -> app#(min(), app(app(cons(), m), x)), app#(min(), app(app(cons(), n), app(app(cons(), m), x))) -> app#(app(if_min(), app(app(le(), n), m)), app(app(cons(), n), app(app(cons(), m), x))))
     (app#(app(if_min(), false()), app(app(cons(), n), app(app(cons(), m), x))) -> app#(min(), app(app(cons(), m), x)), app#(min(), app(app(cons(), n), app(app(cons(), m), x))) -> app#(le(), n))
     (app#(app(if_min(), false()), app(app(cons(), n), app(app(cons(), m), x))) -> app#(min(), app(app(cons(), m), x)), app#(min(), app(app(cons(), n), app(app(cons(), m), x))) -> app#(if_min(), app(app(le(), n), m)))
     (app#(min(), app(app(cons(), n), app(app(cons(), m), x))) -> app#(app(if_min(), app(app(le(), n), m)), app(app(cons(), n), app(app(cons(), m), x))), app#(app(if_min(), true()), app(app(cons(), n), app(app(cons(), m), x))) -> app#(app(cons(), n), x))
     (app#(min(), app(app(cons(), n), app(app(cons(), m), x))) -> app#(app(if_min(), app(app(le(), n), m)), app(app(cons(), n), app(app(cons(), m), x))), app#(app(if_min(), true()), app(app(cons(), n), app(app(cons(), m), x))) -> app#(min(), app(app(cons(), n), x)))
     (app#(min(), app(app(cons(), n), app(app(cons(), m), x))) -> app#(app(if_min(), app(app(le(), n), m)), app(app(cons(), n), app(app(cons(), m), x))), app#(app(if_min(), false()), app(app(cons(), n), app(app(cons(), m), x))) -> app#(min(), app(app(cons(), m), x)))
    }
    STATUS:
     arrows: 0.921975
     SCCS (6):
      Scc:
       { app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(filter(), f), xs),
        app#(app(app(app(filter2(), false()), f), x), xs) -> app#(app(filter(), f), xs),
             app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x),
             app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs),
          app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x),
          app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(app(filter2(), app(f, x)), f), x), xs)}
      Scc:
       {app#(sort(), app(app(cons(), n), x)) -> app#(sort(), app(app(app(replace(), app(min(), app(app(cons(), n), x))), n), x))}
      Scc:
       {app#(app(app(app(if_replace(), false()), n), m), app(app(cons(), k), x)) -> app#(app(app(replace(), n), m), x),
                         app#(app(app(replace(), n), m), app(app(cons(), k), x)) -> app#(app(app(app(if_replace(), app(app(eq(), n), k)), n), m), app(app(cons(), k), x))}
      Scc:
       {app#(app(eq(), app(s(), n)), app(s(), m)) -> app#(app(eq(), n), m)}
      Scc:
       { app#(app(if_min(), true()), app(app(cons(), n), app(app(cons(), m), x))) -> app#(min(), app(app(cons(), n), x)),
        app#(app(if_min(), false()), app(app(cons(), n), app(app(cons(), m), x))) -> app#(min(), app(app(cons(), m), x)),
                         app#(min(), app(app(cons(), n), app(app(cons(), m), x))) -> app#(app(if_min(), app(app(le(), n), m)), app(app(cons(), n), app(app(cons(), m), x)))}
      Scc:
       {app#(app(le(), app(s(), n)), app(s(), m)) -> app#(app(le(), n), m)}
      
      SCC (6):
       Strict:
        { app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(filter(), f), xs),
         app#(app(app(app(filter2(), false()), f), x), xs) -> app#(app(filter(), f), xs),
              app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x),
              app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs),
           app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x),
           app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(app(filter2(), app(f, x)), f), x), xs)}
       Weak:
       {  app(app(app(app(if_replace(), true()), n), m), app(app(cons(), k), x)) -> app(app(cons(), m), x),
         app(app(app(app(if_replace(), false()), n), m), app(app(cons(), k), x)) -> app(app(cons(), k), app(app(app(replace(), n), m), x)),
                                 app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs)),
                                app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs),
                          app(app(app(replace(), n), m), app(app(cons(), k), x)) -> app(app(app(app(if_replace(), app(app(eq(), n), k)), n), m), app(app(cons(), k), x)),
                                           app(app(app(replace(), n), m), nil()) -> nil(),
                                        app(app(eq(), app(s(), n)), app(s(), m)) -> app(app(eq(), n), m),
                                                app(app(eq(), app(s(), n)), 0()) -> false(),
                                                app(app(eq(), 0()), app(s(), m)) -> false(),
                                                        app(app(eq(), 0()), 0()) -> true(),
                                        app(app(le(), app(s(), n)), app(s(), m)) -> app(app(le(), n), m),
                                                app(app(le(), app(s(), n)), 0()) -> false(),
                                                          app(app(le(), 0()), m) -> true(),
         app(app(if_min(), true()), app(app(cons(), n), app(app(cons(), m), x))) -> app(min(), app(app(cons(), n), x)),
        app(app(if_min(), false()), app(app(cons(), n), app(app(cons(), m), x))) -> app(min(), app(app(cons(), m), x)),
                                     app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)),
                                                       app(app(map(), f), nil()) -> nil(),
                                  app(app(filter(), f), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(f, x)), f), x), xs),
                                                    app(app(filter(), f), nil()) -> nil(),
                         app(min(), app(app(cons(), n), app(app(cons(), m), x))) -> app(app(if_min(), app(app(le(), n), m)), app(app(cons(), n), app(app(cons(), m), x))),
                                app(min(), app(app(cons(), app(s(), n)), nil())) -> app(s(), n),
                                        app(min(), app(app(cons(), 0()), nil())) -> 0(),
                                             app(sort(), app(app(cons(), n), x)) -> app(app(cons(), app(min(), app(app(cons(), n), x))), app(sort(), app(app(app(replace(), app(min(), app(app(cons(), n), x))), n), x))),
                                                              app(sort(), nil()) -> nil()}
       Open
      
      
      
      
      SCC (1):
       Strict:
        {app#(sort(), app(app(cons(), n), x)) -> app#(sort(), app(app(app(replace(), app(min(), app(app(cons(), n), x))), n), x))}
       Weak:
       {  app(app(app(app(if_replace(), true()), n), m), app(app(cons(), k), x)) -> app(app(cons(), m), x),
         app(app(app(app(if_replace(), false()), n), m), app(app(cons(), k), x)) -> app(app(cons(), k), app(app(app(replace(), n), m), x)),
                                 app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs)),
                                app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs),
                          app(app(app(replace(), n), m), app(app(cons(), k), x)) -> app(app(app(app(if_replace(), app(app(eq(), n), k)), n), m), app(app(cons(), k), x)),
                                           app(app(app(replace(), n), m), nil()) -> nil(),
                                        app(app(eq(), app(s(), n)), app(s(), m)) -> app(app(eq(), n), m),
                                                app(app(eq(), app(s(), n)), 0()) -> false(),
                                                app(app(eq(), 0()), app(s(), m)) -> false(),
                                                        app(app(eq(), 0()), 0()) -> true(),
                                        app(app(le(), app(s(), n)), app(s(), m)) -> app(app(le(), n), m),
                                                app(app(le(), app(s(), n)), 0()) -> false(),
                                                          app(app(le(), 0()), m) -> true(),
         app(app(if_min(), true()), app(app(cons(), n), app(app(cons(), m), x))) -> app(min(), app(app(cons(), n), x)),
        app(app(if_min(), false()), app(app(cons(), n), app(app(cons(), m), x))) -> app(min(), app(app(cons(), m), x)),
                                     app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)),
                                                       app(app(map(), f), nil()) -> nil(),
                                  app(app(filter(), f), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(f, x)), f), x), xs),
                                                    app(app(filter(), f), nil()) -> nil(),
                         app(min(), app(app(cons(), n), app(app(cons(), m), x))) -> app(app(if_min(), app(app(le(), n), m)), app(app(cons(), n), app(app(cons(), m), x))),
                                app(min(), app(app(cons(), app(s(), n)), nil())) -> app(s(), n),
                                        app(min(), app(app(cons(), 0()), nil())) -> 0(),
                                             app(sort(), app(app(cons(), n), x)) -> app(app(cons(), app(min(), app(app(cons(), n), x))), app(sort(), app(app(app(replace(), app(min(), app(app(cons(), n), x))), n), x))),
                                                              app(sort(), nil()) -> nil()}
       Open
      
      
      
      
      
      
      SCC (2):
       Strict:
        {app#(app(app(app(if_replace(), false()), n), m), app(app(cons(), k), x)) -> app#(app(app(replace(), n), m), x),
                          app#(app(app(replace(), n), m), app(app(cons(), k), x)) -> app#(app(app(app(if_replace(), app(app(eq(), n), k)), n), m), app(app(cons(), k), x))}
       Weak:
       {  app(app(app(app(if_replace(), true()), n), m), app(app(cons(), k), x)) -> app(app(cons(), m), x),
         app(app(app(app(if_replace(), false()), n), m), app(app(cons(), k), x)) -> app(app(cons(), k), app(app(app(replace(), n), m), x)),
                                 app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs)),
                                app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs),
                          app(app(app(replace(), n), m), app(app(cons(), k), x)) -> app(app(app(app(if_replace(), app(app(eq(), n), k)), n), m), app(app(cons(), k), x)),
                                           app(app(app(replace(), n), m), nil()) -> nil(),
                                        app(app(eq(), app(s(), n)), app(s(), m)) -> app(app(eq(), n), m),
                                                app(app(eq(), app(s(), n)), 0()) -> false(),
                                                app(app(eq(), 0()), app(s(), m)) -> false(),
                                                        app(app(eq(), 0()), 0()) -> true(),
                                        app(app(le(), app(s(), n)), app(s(), m)) -> app(app(le(), n), m),
                                                app(app(le(), app(s(), n)), 0()) -> false(),
                                                          app(app(le(), 0()), m) -> true(),
         app(app(if_min(), true()), app(app(cons(), n), app(app(cons(), m), x))) -> app(min(), app(app(cons(), n), x)),
        app(app(if_min(), false()), app(app(cons(), n), app(app(cons(), m), x))) -> app(min(), app(app(cons(), m), x)),
                                     app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)),
                                                       app(app(map(), f), nil()) -> nil(),
                                  app(app(filter(), f), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(f, x)), f), x), xs),
                                                    app(app(filter(), f), nil()) -> nil(),
                         app(min(), app(app(cons(), n), app(app(cons(), m), x))) -> app(app(if_min(), app(app(le(), n), m)), app(app(cons(), n), app(app(cons(), m), x))),
                                app(min(), app(app(cons(), app(s(), n)), nil())) -> app(s(), n),
                                        app(min(), app(app(cons(), 0()), nil())) -> 0(),
                                             app(sort(), app(app(cons(), n), x)) -> app(app(cons(), app(min(), app(app(cons(), n), x))), app(sort(), app(app(app(replace(), app(min(), app(app(cons(), n), x))), n), x))),
                                                              app(sort(), nil()) -> nil()}
       Open
      
      
      
      
      
      
      SCC (1):
       Strict:
        {app#(app(eq(), app(s(), n)), app(s(), m)) -> app#(app(eq(), n), m)}
       Weak:
       {  app(app(app(app(if_replace(), true()), n), m), app(app(cons(), k), x)) -> app(app(cons(), m), x),
         app(app(app(app(if_replace(), false()), n), m), app(app(cons(), k), x)) -> app(app(cons(), k), app(app(app(replace(), n), m), x)),
                                 app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs)),
                                app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs),
                          app(app(app(replace(), n), m), app(app(cons(), k), x)) -> app(app(app(app(if_replace(), app(app(eq(), n), k)), n), m), app(app(cons(), k), x)),
                                           app(app(app(replace(), n), m), nil()) -> nil(),
                                        app(app(eq(), app(s(), n)), app(s(), m)) -> app(app(eq(), n), m),
                                                app(app(eq(), app(s(), n)), 0()) -> false(),
                                                app(app(eq(), 0()), app(s(), m)) -> false(),
                                                        app(app(eq(), 0()), 0()) -> true(),
                                        app(app(le(), app(s(), n)), app(s(), m)) -> app(app(le(), n), m),
                                                app(app(le(), app(s(), n)), 0()) -> false(),
                                                          app(app(le(), 0()), m) -> true(),
         app(app(if_min(), true()), app(app(cons(), n), app(app(cons(), m), x))) -> app(min(), app(app(cons(), n), x)),
        app(app(if_min(), false()), app(app(cons(), n), app(app(cons(), m), x))) -> app(min(), app(app(cons(), m), x)),
                                     app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)),
                                                       app(app(map(), f), nil()) -> nil(),
                                  app(app(filter(), f), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(f, x)), f), x), xs),
                                                    app(app(filter(), f), nil()) -> nil(),
                         app(min(), app(app(cons(), n), app(app(cons(), m), x))) -> app(app(if_min(), app(app(le(), n), m)), app(app(cons(), n), app(app(cons(), m), x))),
                                app(min(), app(app(cons(), app(s(), n)), nil())) -> app(s(), n),
                                        app(min(), app(app(cons(), 0()), nil())) -> 0(),
                                             app(sort(), app(app(cons(), n), x)) -> app(app(cons(), app(min(), app(app(cons(), n), x))), app(sort(), app(app(app(replace(), app(min(), app(app(cons(), n), x))), n), x))),
                                                              app(sort(), nil()) -> nil()}
       Open
      
      
      
      
      
      
      
      
      
      
      SCC (3):
       Strict:
        { app#(app(if_min(), true()), app(app(cons(), n), app(app(cons(), m), x))) -> app#(min(), app(app(cons(), n), x)),
         app#(app(if_min(), false()), app(app(cons(), n), app(app(cons(), m), x))) -> app#(min(), app(app(cons(), m), x)),
                          app#(min(), app(app(cons(), n), app(app(cons(), m), x))) -> app#(app(if_min(), app(app(le(), n), m)), app(app(cons(), n), app(app(cons(), m), x)))}
       Weak:
       {  app(app(app(app(if_replace(), true()), n), m), app(app(cons(), k), x)) -> app(app(cons(), m), x),
         app(app(app(app(if_replace(), false()), n), m), app(app(cons(), k), x)) -> app(app(cons(), k), app(app(app(replace(), n), m), x)),
                                 app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs)),
                                app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs),
                          app(app(app(replace(), n), m), app(app(cons(), k), x)) -> app(app(app(app(if_replace(), app(app(eq(), n), k)), n), m), app(app(cons(), k), x)),
                                           app(app(app(replace(), n), m), nil()) -> nil(),
                                        app(app(eq(), app(s(), n)), app(s(), m)) -> app(app(eq(), n), m),
                                                app(app(eq(), app(s(), n)), 0()) -> false(),
                                                app(app(eq(), 0()), app(s(), m)) -> false(),
                                                        app(app(eq(), 0()), 0()) -> true(),
                                        app(app(le(), app(s(), n)), app(s(), m)) -> app(app(le(), n), m),
                                                app(app(le(), app(s(), n)), 0()) -> false(),
                                                          app(app(le(), 0()), m) -> true(),
         app(app(if_min(), true()), app(app(cons(), n), app(app(cons(), m), x))) -> app(min(), app(app(cons(), n), x)),
        app(app(if_min(), false()), app(app(cons(), n), app(app(cons(), m), x))) -> app(min(), app(app(cons(), m), x)),
                                     app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)),
                                                       app(app(map(), f), nil()) -> nil(),
                                  app(app(filter(), f), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(f, x)), f), x), xs),
                                                    app(app(filter(), f), nil()) -> nil(),
                         app(min(), app(app(cons(), n), app(app(cons(), m), x))) -> app(app(if_min(), app(app(le(), n), m)), app(app(cons(), n), app(app(cons(), m), x))),
                                app(min(), app(app(cons(), app(s(), n)), nil())) -> app(s(), n),
                                        app(min(), app(app(cons(), 0()), nil())) -> 0(),
                                             app(sort(), app(app(cons(), n), x)) -> app(app(cons(), app(min(), app(app(cons(), n), x))), app(sort(), app(app(app(replace(), app(min(), app(app(cons(), n), x))), n), x))),
                                                              app(sort(), nil()) -> nil()}
       Open
      
      
      
      SCC (1):
       Strict:
        {app#(app(le(), app(s(), n)), app(s(), m)) -> app#(app(le(), n), m)}
       Weak:
       {  app(app(app(app(if_replace(), true()), n), m), app(app(cons(), k), x)) -> app(app(cons(), m), x),
         app(app(app(app(if_replace(), false()), n), m), app(app(cons(), k), x)) -> app(app(cons(), k), app(app(app(replace(), n), m), x)),
                                 app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs)),
                                app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs),
                          app(app(app(replace(), n), m), app(app(cons(), k), x)) -> app(app(app(app(if_replace(), app(app(eq(), n), k)), n), m), app(app(cons(), k), x)),
                                           app(app(app(replace(), n), m), nil()) -> nil(),
                                        app(app(eq(), app(s(), n)), app(s(), m)) -> app(app(eq(), n), m),
                                                app(app(eq(), app(s(), n)), 0()) -> false(),
                                                app(app(eq(), 0()), app(s(), m)) -> false(),
                                                        app(app(eq(), 0()), 0()) -> true(),
                                        app(app(le(), app(s(), n)), app(s(), m)) -> app(app(le(), n), m),
                                                app(app(le(), app(s(), n)), 0()) -> false(),
                                                          app(app(le(), 0()), m) -> true(),
         app(app(if_min(), true()), app(app(cons(), n), app(app(cons(), m), x))) -> app(min(), app(app(cons(), n), x)),
        app(app(if_min(), false()), app(app(cons(), n), app(app(cons(), m), x))) -> app(min(), app(app(cons(), m), x)),
                                     app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)),
                                                       app(app(map(), f), nil()) -> nil(),
                                  app(app(filter(), f), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(f, x)), f), x), xs),
                                                    app(app(filter(), f), nil()) -> nil(),
                         app(min(), app(app(cons(), n), app(app(cons(), m), x))) -> app(app(if_min(), app(app(le(), n), m)), app(app(cons(), n), app(app(cons(), m), x))),
                                app(min(), app(app(cons(), app(s(), n)), nil())) -> app(s(), n),
                                        app(min(), app(app(cons(), 0()), nil())) -> 0(),
                                             app(sort(), app(app(cons(), n), x)) -> app(app(cons(), app(min(), app(app(cons(), n), x))), app(sort(), app(app(app(replace(), app(min(), app(app(cons(), n), x))), n), x))),
                                                              app(sort(), nil()) -> nil()}
       Open