MAYBE
Time: 0.102944
TRS:
 {                                         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'(minus(), x), 0()) -> x,
                                             app'(app'(minus(), app'(app'(minus(), x), y)), z) -> app'(app'(minus(), x), app'(app'(plus(), y), z)),
                                               app'(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'(app'(minus(), x), y),
                                                           app'(app'(plus(), app'(s(), x)), y) -> app'(s(), app'(app'(plus(), x), y)),
                                                                    app'(app'(plus(), 0()), y) -> y,
                                                app'(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'(s(), app'(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y))),
                                                         app'(app'(quot(), 0()), app'(s(), y)) -> 0(),
                                                                   app'(app'(app(), l), nil()) -> l,
                                                app'(app'(app(), app'(app'(cons(), x), l)), k) -> app'(app'(cons(), x), app'(app'(app(), l), k)),
                                                                   app'(app'(app(), nil()), k) -> k,
                                               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'(sum(), app'(app'(app(), l), app'(app'(cons(), x), app'(app'(cons(), y), k)))) -> app'(sum(), app'(app'(app(), l), app'(sum(), app'(app'(cons(), x), app'(app'(cons(), y), k))))),
                                  app'(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'(sum(), app'(app'(cons(), app'(app'(plus(), x), y)), l)),
                                                     app'(sum(), app'(app'(cons(), x), nil())) -> app'(app'(cons(), x), nil())}
 DP:
  DP:
   {                                           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'(minus(), app'(app'(minus(), x), y)), z) -> app'#(app'(minus(), x), app'(app'(plus(), y), z)),
                                                 app'#(app'(minus(), app'(app'(minus(), x), y)), z) -> app'#(app'(plus(), y), z),
                                                 app'#(app'(minus(), app'(app'(minus(), x), y)), z) -> app'#(plus(), y),
                                                   app'#(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'#(app'(minus(), x), y),
                                                   app'#(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'#(minus(), x),
                                                               app'#(app'(plus(), app'(s(), x)), y) -> app'#(app'(plus(), x), y),
                                                               app'#(app'(plus(), app'(s(), x)), y) -> app'#(s(), app'(app'(plus(), x), y)),
                                                               app'#(app'(plus(), app'(s(), x)), y) -> app'#(plus(), x),
                                                    app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(app'(minus(), x), y),
                                                    app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y)),
                                                    app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(minus(), x),
                                                    app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(s(), app'(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y))),
                                                    app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(quot(), app'(app'(minus(), x), y)),
                                                    app'#(app'(app(), app'(app'(cons(), x), l)), k) -> app'#(app'(app(), l), k),
                                                    app'#(app'(app(), app'(app'(cons(), x), l)), k) -> app'#(app'(cons(), x), app'(app'(app(), l), k)),
                                                    app'#(app'(app(), app'(app'(cons(), x), l)), k) -> app'#(app(), l),
                                                   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'#(sum(), app'(app'(app(), l), app'(app'(cons(), x), app'(app'(cons(), y), k)))) -> app'#(app'(app(), l), app'(sum(), app'(app'(cons(), x), app'(app'(cons(), y), k)))),
    app'#(sum(), app'(app'(app(), l), app'(app'(cons(), x), app'(app'(cons(), y), k)))) -> app'#(sum(), app'(app'(app(), l), app'(sum(), app'(app'(cons(), x), app'(app'(cons(), y), k))))),
    app'#(sum(), app'(app'(app(), l), app'(app'(cons(), x), app'(app'(cons(), y), k)))) -> app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), k))),
                                      app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'#(app'(plus(), x), y),
                                      app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'#(app'(cons(), app'(app'(plus(), x), y)), l),
                                      app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'#(plus(), x),
                                      app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'#(cons(), app'(app'(plus(), x), y)),
                                      app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'#(sum(), app'(app'(cons(), app'(app'(plus(), x), y)), l))}
  TRS:
  {                                         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'(minus(), x), 0()) -> x,
                                              app'(app'(minus(), app'(app'(minus(), x), y)), z) -> app'(app'(minus(), x), app'(app'(plus(), y), z)),
                                                app'(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'(app'(minus(), x), y),
                                                            app'(app'(plus(), app'(s(), x)), y) -> app'(s(), app'(app'(plus(), x), y)),
                                                                     app'(app'(plus(), 0()), y) -> y,
                                                 app'(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'(s(), app'(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y))),
                                                          app'(app'(quot(), 0()), app'(s(), y)) -> 0(),
                                                                    app'(app'(app(), l), nil()) -> l,
                                                 app'(app'(app(), app'(app'(cons(), x), l)), k) -> app'(app'(cons(), x), app'(app'(app(), l), k)),
                                                                    app'(app'(app(), nil()), k) -> k,
                                                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'(sum(), app'(app'(app(), l), app'(app'(cons(), x), app'(app'(cons(), y), k)))) -> app'(sum(), app'(app'(app(), l), app'(sum(), app'(app'(cons(), x), app'(app'(cons(), y), k))))),
                                   app'(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'(sum(), app'(app'(cons(), app'(app'(plus(), x), y)), l)),
                                                      app'(sum(), app'(app'(cons(), x), nil())) -> app'(app'(cons(), x), nil())}
  EDG:
   {
    (app'#(app'(plus(), app'(s(), x)), y) -> app'#(app'(plus(), x), y), app'#(app'(plus(), app'(s(), x)), y) -> app'#(plus(), x))
    (app'#(app'(plus(), app'(s(), x)), y) -> app'#(app'(plus(), x), y), app'#(app'(plus(), app'(s(), x)), y) -> app'#(s(), app'(app'(plus(), x), y)))
    (app'#(app'(plus(), app'(s(), x)), y) -> app'#(app'(plus(), x), y), app'#(app'(plus(), app'(s(), x)), y) -> app'#(app'(plus(), x), y))
    (app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'#(app'(plus(), x), y), app'#(app'(plus(), app'(s(), x)), y) -> app'#(plus(), x))
    (app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'#(app'(plus(), x), y), app'#(app'(plus(), app'(s(), x)), y) -> app'#(s(), app'(app'(plus(), x), y)))
    (app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'#(app'(plus(), x), y), app'#(app'(plus(), app'(s(), x)), y) -> app'#(app'(plus(), x), y))
    (app'#(sum(), app'(app'(app(), l), app'(app'(cons(), x), app'(app'(cons(), y), k)))) -> app'#(sum(), app'(app'(app(), l), app'(sum(), app'(app'(cons(), x), app'(app'(cons(), y), k))))), app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'#(sum(), app'(app'(cons(), app'(app'(plus(), x), y)), l)))
    (app'#(sum(), app'(app'(app(), l), app'(app'(cons(), x), app'(app'(cons(), y), k)))) -> app'#(sum(), app'(app'(app(), l), app'(sum(), app'(app'(cons(), x), app'(app'(cons(), y), k))))), app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'#(cons(), app'(app'(plus(), x), y)))
    (app'#(sum(), app'(app'(app(), l), app'(app'(cons(), x), app'(app'(cons(), y), k)))) -> app'#(sum(), app'(app'(app(), l), app'(sum(), app'(app'(cons(), x), app'(app'(cons(), y), k))))), app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'#(plus(), x))
    (app'#(sum(), app'(app'(app(), l), app'(app'(cons(), x), app'(app'(cons(), y), k)))) -> app'#(sum(), app'(app'(app(), l), app'(sum(), app'(app'(cons(), x), app'(app'(cons(), y), k))))), app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'#(app'(cons(), app'(app'(plus(), x), y)), l))
    (app'#(sum(), app'(app'(app(), l), app'(app'(cons(), x), app'(app'(cons(), y), k)))) -> app'#(sum(), app'(app'(app(), l), app'(sum(), app'(app'(cons(), x), app'(app'(cons(), y), k))))), app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'#(app'(plus(), x), y))
    (app'#(sum(), app'(app'(app(), l), app'(app'(cons(), x), app'(app'(cons(), y), k)))) -> app'#(sum(), app'(app'(app(), l), app'(sum(), app'(app'(cons(), x), app'(app'(cons(), y), k))))), app'#(sum(), app'(app'(app(), l), app'(app'(cons(), x), app'(app'(cons(), y), k)))) -> app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), k))))
    (app'#(sum(), app'(app'(app(), l), app'(app'(cons(), x), app'(app'(cons(), y), k)))) -> app'#(sum(), app'(app'(app(), l), app'(sum(), app'(app'(cons(), x), app'(app'(cons(), y), k))))), app'#(sum(), app'(app'(app(), l), app'(app'(cons(), x), app'(app'(cons(), y), k)))) -> app'#(sum(), app'(app'(app(), l), app'(sum(), app'(app'(cons(), x), app'(app'(cons(), y), k))))))
    (app'#(sum(), app'(app'(app(), l), app'(app'(cons(), x), app'(app'(cons(), y), k)))) -> app'#(sum(), app'(app'(app(), l), app'(sum(), app'(app'(cons(), x), app'(app'(cons(), y), k))))), app'#(sum(), app'(app'(app(), l), app'(app'(cons(), x), app'(app'(cons(), y), k)))) -> app'#(app'(app(), l), app'(sum(), app'(app'(cons(), x), app'(app'(cons(), y), k)))))
    (app'#(app'(minus(), app'(app'(minus(), x), y)), z) -> app'#(app'(plus(), y), z), app'#(app'(plus(), app'(s(), x)), y) -> app'#(plus(), x))
    (app'#(app'(minus(), app'(app'(minus(), x), y)), z) -> app'#(app'(plus(), y), z), app'#(app'(plus(), app'(s(), x)), y) -> app'#(s(), app'(app'(plus(), x), y)))
    (app'#(app'(minus(), app'(app'(minus(), x), y)), z) -> app'#(app'(plus(), y), z), app'#(app'(plus(), app'(s(), x)), y) -> app'#(app'(plus(), x), y))
    (app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y)), app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(quot(), app'(app'(minus(), x), y)))
    (app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y)), app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(s(), app'(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y))))
    (app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y)), app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(minus(), x))
    (app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y)), app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y)))
    (app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y)), app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(app'(minus(), x), y))
    (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'#(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'#(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'(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'#(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'#(cons(), 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'(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'(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'#(f, x))
    (app'#(app'(map(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'#(sum(), app'(app'(cons(), app'(app'(plus(), x), y)), l)))
    (app'#(app'(map(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'#(cons(), app'(app'(plus(), x), y)))
    (app'#(app'(map(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'#(plus(), x))
    (app'#(app'(map(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'#(app'(cons(), app'(app'(plus(), x), y)), l))
    (app'#(app'(map(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'#(app'(plus(), x), y))
    (app'#(app'(map(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(sum(), app'(app'(app(), l), app'(app'(cons(), x), app'(app'(cons(), y), k)))) -> app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), k))))
    (app'#(app'(map(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(sum(), app'(app'(app(), l), app'(app'(cons(), x), app'(app'(cons(), y), k)))) -> app'#(sum(), app'(app'(app(), l), app'(sum(), app'(app'(cons(), x), app'(app'(cons(), y), k))))))
    (app'#(app'(map(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(sum(), app'(app'(app(), l), app'(app'(cons(), x), app'(app'(cons(), y), k)))) -> app'#(app'(app(), l), app'(sum(), app'(app'(cons(), x), app'(app'(cons(), y), k)))))
    (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'#(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'#(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'(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'#(f, x))
    (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'(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'(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'#(f, x))
    (app'#(app'(map(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(app'(app(), app'(app'(cons(), x), l)), k) -> app'#(app(), l))
    (app'#(app'(map(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(app'(app(), app'(app'(cons(), x), l)), k) -> app'#(app'(cons(), x), app'(app'(app(), l), k)))
    (app'#(app'(map(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(app'(app(), app'(app'(cons(), x), l)), k) -> app'#(app'(app(), l), k))
    (app'#(app'(map(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(quot(), app'(app'(minus(), x), y)))
    (app'#(app'(map(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(s(), app'(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y))))
    (app'#(app'(map(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(minus(), x))
    (app'#(app'(map(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y)))
    (app'#(app'(map(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(app'(minus(), x), y))
    (app'#(app'(map(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(app'(plus(), app'(s(), x)), y) -> app'#(plus(), x))
    (app'#(app'(map(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(app'(plus(), app'(s(), x)), y) -> app'#(s(), app'(app'(plus(), x), y)))
    (app'#(app'(map(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(app'(plus(), app'(s(), x)), y) -> app'#(app'(plus(), x), y))
    (app'#(app'(map(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'#(minus(), x))
    (app'#(app'(map(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'#(app'(minus(), x), y))
    (app'#(app'(map(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(app'(minus(), app'(app'(minus(), x), y)), z) -> app'#(plus(), y))
    (app'#(app'(map(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(app'(minus(), app'(app'(minus(), x), y)), z) -> app'#(app'(plus(), y), z))
    (app'#(app'(map(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(app'(minus(), app'(app'(minus(), x), y)), z) -> app'#(app'(minus(), x), app'(app'(plus(), y), z)))
    (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'(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(), true()), f), x), xs) -> app'#(filter(), f))
    (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'#(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'(cons(), x), 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'(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'#(cons(), x))
    (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(), 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(), false()), f), x), xs) -> app'#(filter(), f))
    (app'#(app'(filter(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(app'(minus(), app'(app'(minus(), x), y)), z) -> app'#(app'(minus(), x), app'(app'(plus(), y), z)))
    (app'#(app'(filter(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(app'(minus(), app'(app'(minus(), x), y)), z) -> app'#(app'(plus(), y), z))
    (app'#(app'(filter(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(app'(minus(), app'(app'(minus(), x), y)), z) -> app'#(plus(), y))
    (app'#(app'(filter(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'#(app'(minus(), x), y))
    (app'#(app'(filter(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'#(minus(), x))
    (app'#(app'(filter(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(app'(plus(), app'(s(), x)), y) -> app'#(app'(plus(), x), y))
    (app'#(app'(filter(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(app'(plus(), app'(s(), x)), y) -> app'#(s(), app'(app'(plus(), x), y)))
    (app'#(app'(filter(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(app'(plus(), app'(s(), x)), y) -> app'#(plus(), x))
    (app'#(app'(filter(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(app'(minus(), x), y))
    (app'#(app'(filter(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y)))
    (app'#(app'(filter(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(minus(), x))
    (app'#(app'(filter(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(s(), app'(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y))))
    (app'#(app'(filter(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(quot(), app'(app'(minus(), x), y)))
    (app'#(app'(filter(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(app'(app(), app'(app'(cons(), x), l)), k) -> app'#(app'(app(), l), k))
    (app'#(app'(filter(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(app'(app(), app'(app'(cons(), x), l)), k) -> app'#(app'(cons(), x), app'(app'(app(), l), k)))
    (app'#(app'(filter(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(app'(app(), app'(app'(cons(), x), l)), k) -> app'#(app(), l))
    (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'(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'#(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'#(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'#(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'#(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'(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'#(filter2(), app'(f, x)))
    (app'#(app'(filter(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(sum(), app'(app'(app(), l), app'(app'(cons(), x), app'(app'(cons(), y), k)))) -> app'#(app'(app(), l), app'(sum(), app'(app'(cons(), x), app'(app'(cons(), y), k)))))
    (app'#(app'(filter(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(sum(), app'(app'(app(), l), app'(app'(cons(), x), app'(app'(cons(), y), k)))) -> app'#(sum(), app'(app'(app(), l), app'(sum(), app'(app'(cons(), x), app'(app'(cons(), y), k))))))
    (app'#(app'(filter(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(sum(), app'(app'(app(), l), app'(app'(cons(), x), app'(app'(cons(), y), k)))) -> app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), k))))
    (app'#(app'(filter(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'#(app'(plus(), x), y))
    (app'#(app'(filter(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'#(app'(cons(), app'(app'(plus(), x), y)), l))
    (app'#(app'(filter(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'#(plus(), x))
    (app'#(app'(filter(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'#(cons(), app'(app'(plus(), x), y)))
    (app'#(app'(filter(), f), app'(app'(cons(), x), xs)) -> app'#(f, x), app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'#(sum(), app'(app'(cons(), app'(app'(plus(), x), y)), l)))
    (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'(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'#(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'#(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(), false()), f), x), xs) -> app'#(filter(), 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'#(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'#(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'(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'#(filter2(), app'(f, x)))
    (app'#(app'(app(), app'(app'(cons(), x), l)), k) -> app'#(app'(app(), l), k), app'#(app'(app(), app'(app'(cons(), x), l)), k) -> app'#(app'(app(), l), k))
    (app'#(app'(app(), app'(app'(cons(), x), l)), k) -> app'#(app'(app(), l), k), app'#(app'(app(), app'(app'(cons(), x), l)), k) -> app'#(app'(cons(), x), app'(app'(app(), l), k)))
    (app'#(app'(app(), app'(app'(cons(), x), l)), k) -> app'#(app'(app(), l), k), app'#(app'(app(), app'(app'(cons(), x), l)), k) -> app'#(app(), l))
    (app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'#(sum(), app'(app'(cons(), app'(app'(plus(), x), y)), l)), app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'#(app'(plus(), x), y))
    (app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'#(sum(), app'(app'(cons(), app'(app'(plus(), x), y)), l)), app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'#(app'(cons(), app'(app'(plus(), x), y)), l))
    (app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'#(sum(), app'(app'(cons(), app'(app'(plus(), x), y)), l)), app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'#(plus(), x))
    (app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'#(sum(), app'(app'(cons(), app'(app'(plus(), x), y)), l)), app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'#(cons(), app'(app'(plus(), x), y)))
    (app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'#(sum(), app'(app'(cons(), app'(app'(plus(), x), y)), l)), app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'#(sum(), app'(app'(cons(), app'(app'(plus(), x), y)), l)))
    (app'#(app'(minus(), app'(app'(minus(), x), y)), z) -> app'#(app'(minus(), x), app'(app'(plus(), y), z)), app'#(app'(minus(), app'(app'(minus(), x), y)), z) -> app'#(app'(minus(), x), app'(app'(plus(), y), z)))
    (app'#(app'(minus(), app'(app'(minus(), x), y)), z) -> app'#(app'(minus(), x), app'(app'(plus(), y), z)), app'#(app'(minus(), app'(app'(minus(), x), y)), z) -> app'#(app'(plus(), y), z))
    (app'#(app'(minus(), app'(app'(minus(), x), y)), z) -> app'#(app'(minus(), x), app'(app'(plus(), y), z)), app'#(app'(minus(), app'(app'(minus(), x), y)), z) -> app'#(plus(), y))
    (app'#(app'(minus(), app'(app'(minus(), x), y)), z) -> app'#(app'(minus(), x), app'(app'(plus(), y), z)), app'#(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'#(app'(minus(), x), y))
    (app'#(app'(minus(), app'(app'(minus(), x), y)), z) -> app'#(app'(minus(), x), app'(app'(plus(), y), z)), app'#(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'#(minus(), x))
    (app'#(sum(), app'(app'(app(), l), app'(app'(cons(), x), app'(app'(cons(), y), k)))) -> app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), k))), app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'#(app'(plus(), x), y))
    (app'#(sum(), app'(app'(app(), l), app'(app'(cons(), x), app'(app'(cons(), y), k)))) -> app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), k))), app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'#(app'(cons(), app'(app'(plus(), x), y)), l))
    (app'#(sum(), app'(app'(app(), l), app'(app'(cons(), x), app'(app'(cons(), y), k)))) -> app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), k))), app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'#(plus(), x))
    (app'#(sum(), app'(app'(app(), l), app'(app'(cons(), x), app'(app'(cons(), y), k)))) -> app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), k))), app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'#(cons(), app'(app'(plus(), x), y)))
    (app'#(sum(), app'(app'(app(), l), app'(app'(cons(), x), app'(app'(cons(), y), k)))) -> app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), k))), app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'#(sum(), app'(app'(cons(), app'(app'(plus(), x), y)), l)))
    (app'#(sum(), app'(app'(app(), l), app'(app'(cons(), x), app'(app'(cons(), y), k)))) -> app'#(app'(app(), l), app'(sum(), app'(app'(cons(), x), app'(app'(cons(), y), k)))), app'#(app'(app(), app'(app'(cons(), x), l)), k) -> app'#(app'(app(), l), k))
    (app'#(sum(), app'(app'(app(), l), app'(app'(cons(), x), app'(app'(cons(), y), k)))) -> app'#(app'(app(), l), app'(sum(), app'(app'(cons(), x), app'(app'(cons(), y), k)))), app'#(app'(app(), app'(app'(cons(), x), l)), k) -> app'#(app'(cons(), x), app'(app'(app(), l), k)))
    (app'#(sum(), app'(app'(app(), l), app'(app'(cons(), x), app'(app'(cons(), y), k)))) -> app'#(app'(app(), l), app'(sum(), app'(app'(cons(), x), app'(app'(cons(), y), k)))), app'#(app'(app(), app'(app'(cons(), x), l)), k) -> app'#(app(), l))
    (app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(app'(minus(), x), y), app'#(app'(minus(), app'(app'(minus(), x), y)), z) -> app'#(app'(minus(), x), app'(app'(plus(), y), z)))
    (app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(app'(minus(), x), y), app'#(app'(minus(), app'(app'(minus(), x), y)), z) -> app'#(app'(plus(), y), z))
    (app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(app'(minus(), x), y), app'#(app'(minus(), app'(app'(minus(), x), y)), z) -> app'#(plus(), y))
    (app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(app'(minus(), x), y), app'#(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'#(app'(minus(), x), y))
    (app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(app'(minus(), x), y), app'#(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'#(minus(), x))
    (app'#(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'#(app'(minus(), x), y), app'#(app'(minus(), app'(app'(minus(), x), y)), z) -> app'#(app'(minus(), x), app'(app'(plus(), y), z)))
    (app'#(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'#(app'(minus(), x), y), app'#(app'(minus(), app'(app'(minus(), x), y)), z) -> app'#(app'(plus(), y), z))
    (app'#(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'#(app'(minus(), x), y), app'#(app'(minus(), app'(app'(minus(), x), y)), z) -> app'#(plus(), y))
    (app'#(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'#(app'(minus(), x), y), app'#(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'#(app'(minus(), x), y))
    (app'#(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'#(app'(minus(), x), y), app'#(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'#(minus(), x))
   }
   STATUS:
    arrows: 0.900723
    SCCS (7):
     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'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y))}
     Scc:
      {app'#(sum(), app'(app'(app(), l), app'(app'(cons(), x), app'(app'(cons(), y), k)))) -> app'#(sum(), app'(app'(app(), l), app'(sum(), app'(app'(cons(), x), app'(app'(cons(), y), k)))))}
     Scc:
      {app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'#(sum(), app'(app'(cons(), app'(app'(plus(), x), y)), l))}
     Scc:
      {app'#(app'(app(), app'(app'(cons(), x), l)), k) -> app'#(app'(app(), l), k)}
     Scc:
      {app'#(app'(minus(), app'(app'(minus(), x), y)), z) -> app'#(app'(minus(), x), app'(app'(plus(), y), z)),
         app'#(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'#(app'(minus(), x), y)}
     Scc:
      {app'#(app'(plus(), app'(s(), x)), y) -> app'#(app'(plus(), x), y)}
     
     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'(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'(minus(), x), 0()) -> x,
                                                  app'(app'(minus(), app'(app'(minus(), x), y)), z) -> app'(app'(minus(), x), app'(app'(plus(), y), z)),
                                                    app'(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'(app'(minus(), x), y),
                                                                app'(app'(plus(), app'(s(), x)), y) -> app'(s(), app'(app'(plus(), x), y)),
                                                                         app'(app'(plus(), 0()), y) -> y,
                                                     app'(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'(s(), app'(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y))),
                                                              app'(app'(quot(), 0()), app'(s(), y)) -> 0(),
                                                                        app'(app'(app(), l), nil()) -> l,
                                                     app'(app'(app(), app'(app'(cons(), x), l)), k) -> app'(app'(cons(), x), app'(app'(app(), l), k)),
                                                                        app'(app'(app(), nil()), k) -> k,
                                                    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'(sum(), app'(app'(app(), l), app'(app'(cons(), x), app'(app'(cons(), y), k)))) -> app'(sum(), app'(app'(app(), l), app'(sum(), app'(app'(cons(), x), app'(app'(cons(), y), k))))),
                                       app'(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'(sum(), app'(app'(cons(), app'(app'(plus(), x), y)), l)),
                                                          app'(sum(), app'(app'(cons(), x), nil())) -> app'(app'(cons(), x), nil())}
      Open
     
     
     
     
     
     
     
     SCC (1):
      Strict:
       {app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y))}
      Weak:
      {                                         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'(minus(), x), 0()) -> x,
                                                  app'(app'(minus(), app'(app'(minus(), x), y)), z) -> app'(app'(minus(), x), app'(app'(plus(), y), z)),
                                                    app'(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'(app'(minus(), x), y),
                                                                app'(app'(plus(), app'(s(), x)), y) -> app'(s(), app'(app'(plus(), x), y)),
                                                                         app'(app'(plus(), 0()), y) -> y,
                                                     app'(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'(s(), app'(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y))),
                                                              app'(app'(quot(), 0()), app'(s(), y)) -> 0(),
                                                                        app'(app'(app(), l), nil()) -> l,
                                                     app'(app'(app(), app'(app'(cons(), x), l)), k) -> app'(app'(cons(), x), app'(app'(app(), l), k)),
                                                                        app'(app'(app(), nil()), k) -> k,
                                                    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'(sum(), app'(app'(app(), l), app'(app'(cons(), x), app'(app'(cons(), y), k)))) -> app'(sum(), app'(app'(app(), l), app'(sum(), app'(app'(cons(), x), app'(app'(cons(), y), k))))),
                                       app'(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'(sum(), app'(app'(cons(), app'(app'(plus(), x), y)), l)),
                                                          app'(sum(), app'(app'(cons(), x), nil())) -> app'(app'(cons(), x), nil())}
      Open
     
     
     
     
     SCC (1):
      Strict:
       {app'#(sum(), app'(app'(app(), l), app'(app'(cons(), x), app'(app'(cons(), y), k)))) -> app'#(sum(), app'(app'(app(), l), app'(sum(), app'(app'(cons(), x), app'(app'(cons(), y), k)))))}
      Weak:
      {                                         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'(minus(), x), 0()) -> x,
                                                  app'(app'(minus(), app'(app'(minus(), x), y)), z) -> app'(app'(minus(), x), app'(app'(plus(), y), z)),
                                                    app'(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'(app'(minus(), x), y),
                                                                app'(app'(plus(), app'(s(), x)), y) -> app'(s(), app'(app'(plus(), x), y)),
                                                                         app'(app'(plus(), 0()), y) -> y,
                                                     app'(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'(s(), app'(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y))),
                                                              app'(app'(quot(), 0()), app'(s(), y)) -> 0(),
                                                                        app'(app'(app(), l), nil()) -> l,
                                                     app'(app'(app(), app'(app'(cons(), x), l)), k) -> app'(app'(cons(), x), app'(app'(app(), l), k)),
                                                                        app'(app'(app(), nil()), k) -> k,
                                                    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'(sum(), app'(app'(app(), l), app'(app'(cons(), x), app'(app'(cons(), y), k)))) -> app'(sum(), app'(app'(app(), l), app'(sum(), app'(app'(cons(), x), app'(app'(cons(), y), k))))),
                                       app'(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'(sum(), app'(app'(cons(), app'(app'(plus(), x), y)), l)),
                                                          app'(sum(), app'(app'(cons(), x), nil())) -> app'(app'(cons(), x), nil())}
      Open
     
     SCC (1):
      Strict:
       {app'#(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'#(sum(), app'(app'(cons(), app'(app'(plus(), x), y)), l))}
      Weak:
      {                                         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'(minus(), x), 0()) -> x,
                                                  app'(app'(minus(), app'(app'(minus(), x), y)), z) -> app'(app'(minus(), x), app'(app'(plus(), y), z)),
                                                    app'(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'(app'(minus(), x), y),
                                                                app'(app'(plus(), app'(s(), x)), y) -> app'(s(), app'(app'(plus(), x), y)),
                                                                         app'(app'(plus(), 0()), y) -> y,
                                                     app'(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'(s(), app'(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y))),
                                                              app'(app'(quot(), 0()), app'(s(), y)) -> 0(),
                                                                        app'(app'(app(), l), nil()) -> l,
                                                     app'(app'(app(), app'(app'(cons(), x), l)), k) -> app'(app'(cons(), x), app'(app'(app(), l), k)),
                                                                        app'(app'(app(), nil()), k) -> k,
                                                    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'(sum(), app'(app'(app(), l), app'(app'(cons(), x), app'(app'(cons(), y), k)))) -> app'(sum(), app'(app'(app(), l), app'(sum(), app'(app'(cons(), x), app'(app'(cons(), y), k))))),
                                       app'(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'(sum(), app'(app'(cons(), app'(app'(plus(), x), y)), l)),
                                                          app'(sum(), app'(app'(cons(), x), nil())) -> app'(app'(cons(), x), nil())}
      Open
     
     
     
     SCC (1):
      Strict:
       {app'#(app'(app(), app'(app'(cons(), x), l)), k) -> app'#(app'(app(), l), k)}
      Weak:
      {                                         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'(minus(), x), 0()) -> x,
                                                  app'(app'(minus(), app'(app'(minus(), x), y)), z) -> app'(app'(minus(), x), app'(app'(plus(), y), z)),
                                                    app'(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'(app'(minus(), x), y),
                                                                app'(app'(plus(), app'(s(), x)), y) -> app'(s(), app'(app'(plus(), x), y)),
                                                                         app'(app'(plus(), 0()), y) -> y,
                                                     app'(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'(s(), app'(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y))),
                                                              app'(app'(quot(), 0()), app'(s(), y)) -> 0(),
                                                                        app'(app'(app(), l), nil()) -> l,
                                                     app'(app'(app(), app'(app'(cons(), x), l)), k) -> app'(app'(cons(), x), app'(app'(app(), l), k)),
                                                                        app'(app'(app(), nil()), k) -> k,
                                                    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'(sum(), app'(app'(app(), l), app'(app'(cons(), x), app'(app'(cons(), y), k)))) -> app'(sum(), app'(app'(app(), l), app'(sum(), app'(app'(cons(), x), app'(app'(cons(), y), k))))),
                                       app'(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'(sum(), app'(app'(cons(), app'(app'(plus(), x), y)), l)),
                                                          app'(sum(), app'(app'(cons(), x), nil())) -> app'(app'(cons(), x), nil())}
      Open
     
     
     
     
     
     
     SCC (2):
      Strict:
       {app'#(app'(minus(), app'(app'(minus(), x), y)), z) -> app'#(app'(minus(), x), app'(app'(plus(), y), z)),
          app'#(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'#(app'(minus(), x), y)}
      Weak:
      {                                         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'(minus(), x), 0()) -> x,
                                                  app'(app'(minus(), app'(app'(minus(), x), y)), z) -> app'(app'(minus(), x), app'(app'(plus(), y), z)),
                                                    app'(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'(app'(minus(), x), y),
                                                                app'(app'(plus(), app'(s(), x)), y) -> app'(s(), app'(app'(plus(), x), y)),
                                                                         app'(app'(plus(), 0()), y) -> y,
                                                     app'(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'(s(), app'(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y))),
                                                              app'(app'(quot(), 0()), app'(s(), y)) -> 0(),
                                                                        app'(app'(app(), l), nil()) -> l,
                                                     app'(app'(app(), app'(app'(cons(), x), l)), k) -> app'(app'(cons(), x), app'(app'(app(), l), k)),
                                                                        app'(app'(app(), nil()), k) -> k,
                                                    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'(sum(), app'(app'(app(), l), app'(app'(cons(), x), app'(app'(cons(), y), k)))) -> app'(sum(), app'(app'(app(), l), app'(sum(), app'(app'(cons(), x), app'(app'(cons(), y), k))))),
                                       app'(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'(sum(), app'(app'(cons(), app'(app'(plus(), x), y)), l)),
                                                          app'(sum(), app'(app'(cons(), x), nil())) -> app'(app'(cons(), x), nil())}
      Open
     
     
     
     SCC (1):
      Strict:
       {app'#(app'(plus(), app'(s(), x)), y) -> app'#(app'(plus(), x), y)}
      Weak:
      {                                         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'(minus(), x), 0()) -> x,
                                                  app'(app'(minus(), app'(app'(minus(), x), y)), z) -> app'(app'(minus(), x), app'(app'(plus(), y), z)),
                                                    app'(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'(app'(minus(), x), y),
                                                                app'(app'(plus(), app'(s(), x)), y) -> app'(s(), app'(app'(plus(), x), y)),
                                                                         app'(app'(plus(), 0()), y) -> y,
                                                     app'(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'(s(), app'(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y))),
                                                              app'(app'(quot(), 0()), app'(s(), y)) -> 0(),
                                                                        app'(app'(app(), l), nil()) -> l,
                                                     app'(app'(app(), app'(app'(cons(), x), l)), k) -> app'(app'(cons(), x), app'(app'(app(), l), k)),
                                                                        app'(app'(app(), nil()), k) -> k,
                                                    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'(sum(), app'(app'(app(), l), app'(app'(cons(), x), app'(app'(cons(), y), k)))) -> app'(sum(), app'(app'(app(), l), app'(sum(), app'(app'(cons(), x), app'(app'(cons(), y), k))))),
                                       app'(sum(), app'(app'(cons(), x), app'(app'(cons(), y), l))) -> app'(sum(), app'(app'(cons(), app'(app'(plus(), x), y)), l)),
                                                          app'(sum(), app'(app'(cons(), x), nil())) -> app'(app'(cons(), x), nil())}
      Open