YES
Time: 0.963520
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(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(D(), app(app(+(), x), y)) -> app(app(+(), app(D(), x)), app(D(), y)),
                     app(D(), app(app(*(), x), y)) -> app(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y))),
                     app(D(), app(app(-(), x), y)) -> app(app(-(), app(D(), x)), app(D(), y)),
                   app(D(), app(app(div(), x), y)) -> app(app(-(), app(app(div(), app(D(), x)), y)), app(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2()))),
                   app(D(), app(app(pow(), x), y)) -> app(app(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))), app(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y))),
                         app(D(), app(minus(), x)) -> app(minus(), app(D(), x)),
                            app(D(), app(ln(), x)) -> app(app(div(), app(D(), x)), x),
                                     app(D(), t()) -> 1(),
                              app(D(), constant()) -> 0()}
 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(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#(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#(D(), app(app(+(), x), y)) -> app#(app(+(), app(D(), x)), app(D(), y)),
                       app#(D(), app(app(+(), x), y)) -> app#(D(), x),
                       app#(D(), app(app(+(), x), y)) -> app#(D(), y),
                       app#(D(), app(app(+(), x), y)) -> app#(+(), app(D(), x)),
                       app#(D(), app(app(*(), x), y)) -> app#(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y))),
                       app#(D(), app(app(*(), x), y)) -> app#(app(*(), x), app(D(), y)),
                       app#(D(), app(app(*(), x), y)) -> app#(app(*(), y), app(D(), x)),
                       app#(D(), app(app(*(), x), y)) -> app#(D(), x),
                       app#(D(), app(app(*(), x), y)) -> app#(D(), y),
                       app#(D(), app(app(*(), x), y)) -> app#(+(), app(app(*(), y), app(D(), x))),
                       app#(D(), app(app(*(), x), y)) -> app#(*(), y),
                       app#(D(), app(app(-(), x), y)) -> app#(app(-(), app(D(), x)), app(D(), y)),
                       app#(D(), app(app(-(), x), y)) -> app#(D(), x),
                       app#(D(), app(app(-(), x), y)) -> app#(D(), y),
                       app#(D(), app(app(-(), x), y)) -> app#(-(), app(D(), x)),
                     app#(D(), app(app(div(), x), y)) -> app#(app(*(), x), app(D(), y)),
                     app#(D(), app(app(div(), x), y)) -> app#(app(-(), app(app(div(), app(D(), x)), y)), app(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2()))),
                     app#(D(), app(app(div(), x), y)) -> app#(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2())),
                     app#(D(), app(app(div(), x), y)) -> app#(app(div(), app(D(), x)), y),
                     app#(D(), app(app(div(), x), y)) -> app#(app(pow(), y), 2()),
                     app#(D(), app(app(div(), x), y)) -> app#(D(), x),
                     app#(D(), app(app(div(), x), y)) -> app#(D(), y),
                     app#(D(), app(app(div(), x), y)) -> app#(*(), x),
                     app#(D(), app(app(div(), x), y)) -> app#(-(), app(app(div(), app(D(), x)), y)),
                     app#(D(), app(app(div(), x), y)) -> app#(div(), app(app(*(), x), app(D(), y))),
                     app#(D(), app(app(div(), x), y)) -> app#(div(), app(D(), x)),
                     app#(D(), app(app(div(), x), y)) -> app#(pow(), y),
                     app#(D(), app(app(pow(), x), y)) -> app#(app(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))), app(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y))),
                     app#(D(), app(app(pow(), x), y)) -> app#(app(*(), y), app(app(pow(), x), app(app(-(), y), 1()))),
                     app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x)),
                     app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y)),
                     app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(pow(), x), y)), app(ln(), x)),
                     app#(D(), app(app(pow(), x), y)) -> app#(app(-(), y), 1()),
                     app#(D(), app(app(pow(), x), y)) -> app#(app(pow(), x), app(app(-(), y), 1())),
                     app#(D(), app(app(pow(), x), y)) -> app#(D(), x),
                     app#(D(), app(app(pow(), x), y)) -> app#(D(), y),
                     app#(D(), app(app(pow(), x), y)) -> app#(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))),
                     app#(D(), app(app(pow(), x), y)) -> app#(*(), y),
                     app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))),
                     app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))),
                     app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(pow(), x), y)),
                     app#(D(), app(app(pow(), x), y)) -> app#(-(), y),
                     app#(D(), app(app(pow(), x), y)) -> app#(ln(), x),
                           app#(D(), app(minus(), x)) -> app#(D(), x),
                           app#(D(), app(minus(), x)) -> app#(minus(), app(D(), x)),
                              app#(D(), app(ln(), x)) -> app#(app(div(), app(D(), x)), x),
                              app#(D(), app(ln(), x)) -> app#(D(), x),
                              app#(D(), app(ln(), x)) -> app#(div(), app(D(), x))}
  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(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(D(), app(app(+(), x), y)) -> app(app(+(), app(D(), x)), app(D(), y)),
                      app(D(), app(app(*(), x), y)) -> app(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y))),
                      app(D(), app(app(-(), x), y)) -> app(app(-(), app(D(), x)), app(D(), y)),
                    app(D(), app(app(div(), x), y)) -> app(app(-(), app(app(div(), app(D(), x)), y)), app(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2()))),
                    app(D(), app(app(pow(), x), y)) -> app(app(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))), app(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y))),
                          app(D(), app(minus(), x)) -> app(minus(), app(D(), x)),
                             app(D(), app(ln(), x)) -> app(app(div(), app(D(), x)), x),
                                      app(D(), t()) -> 1(),
                               app(D(), constant()) -> 0()}
  EDG:
   {
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(ln(), x)) -> app#(div(), app(D(), x)))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(ln(), x)) -> app#(D(), x))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(ln(), x)) -> app#(app(div(), app(D(), x)), x))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(minus(), x)) -> app#(minus(), app(D(), x)))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(minus(), x)) -> app#(D(), x))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(ln(), x))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(-(), y))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(pow(), x), y)))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(*(), y))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(app(pow(), x), app(app(-(), y), 1())))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(app(-(), y), 1()))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(pow(), x), y)), app(ln(), x)))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y)))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x)))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), y), app(app(pow(), x), app(app(-(), y), 1()))))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(app(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))), app(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y))))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(pow(), y))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(div(), app(D(), x)))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(div(), app(app(*(), x), app(D(), y))))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(-(), app(app(div(), app(D(), x)), y)))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(*(), x))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(app(pow(), y), 2()))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(app(div(), app(D(), x)), y))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2())))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(app(-(), app(app(div(), app(D(), x)), y)), app(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2()))))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(app(*(), x), app(D(), y)))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(-(), x), y)) -> app#(-(), app(D(), x)))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(-(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(-(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(-(), x), y)) -> app#(app(-(), app(D(), x)), app(D(), y)))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(*(), y))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(+(), app(app(*(), y), app(D(), x))))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(app(*(), y), app(D(), x)))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(app(*(), x), app(D(), y)))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y))))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(+(), x), y)) -> app#(+(), app(D(), x)))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(+(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(+(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(+(), x), y)) -> app#(app(+(), app(D(), x)), app(D(), y)))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(ln(), x)) -> app#(div(), app(D(), x)))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(ln(), x)) -> app#(D(), x))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(ln(), x)) -> app#(app(div(), app(D(), x)), x))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(minus(), x)) -> app#(minus(), app(D(), x)))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(minus(), x)) -> app#(D(), x))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(ln(), x))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(-(), y))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(pow(), x), y)))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(*(), y))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(app(pow(), x), app(app(-(), y), 1())))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(app(-(), y), 1()))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(pow(), x), y)), app(ln(), x)))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y)))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x)))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), y), app(app(pow(), x), app(app(-(), y), 1()))))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(app(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))), app(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y))))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(pow(), y))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(div(), app(D(), x)))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(div(), app(app(*(), x), app(D(), y))))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(-(), app(app(div(), app(D(), x)), y)))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(*(), x))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(app(pow(), y), 2()))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(app(div(), app(D(), x)), y))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2())))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(app(-(), app(app(div(), app(D(), x)), y)), app(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2()))))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(app(*(), x), app(D(), y)))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(-(), x), y)) -> app#(-(), app(D(), x)))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(-(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(-(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(-(), x), y)) -> app#(app(-(), app(D(), x)), app(D(), y)))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(*(), y))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(+(), app(app(*(), y), app(D(), x))))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(app(*(), y), app(D(), x)))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(app(*(), x), app(D(), y)))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y))))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(+(), x), y)) -> app#(+(), app(D(), x)))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(+(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(+(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(+(), x), y)) -> app#(app(+(), app(D(), x)), app(D(), y)))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(ln(), x)) -> app#(div(), app(D(), x)))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(ln(), x)) -> app#(D(), x))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(ln(), x)) -> app#(app(div(), app(D(), x)), x))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(minus(), x)) -> app#(minus(), app(D(), x)))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(minus(), x)) -> app#(D(), x))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(pow(), x), y)) -> app#(ln(), x))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(pow(), x), y)) -> app#(-(), y))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(pow(), x), y)))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(pow(), x), y)) -> app#(*(), y))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(pow(), x), y)) -> app#(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(pow(), x), y)) -> app#(D(), y))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(pow(), x), y)) -> app#(D(), x))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(pow(), x), y)) -> app#(app(pow(), x), app(app(-(), y), 1())))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(pow(), x), y)) -> app#(app(-(), y), 1()))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(pow(), x), y)), app(ln(), x)))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y)))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x)))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), y), app(app(pow(), x), app(app(-(), y), 1()))))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(pow(), x), y)) -> app#(app(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))), app(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y))))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(div(), x), y)) -> app#(pow(), y))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(div(), x), y)) -> app#(div(), app(D(), x)))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(div(), x), y)) -> app#(div(), app(app(*(), x), app(D(), y))))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(div(), x), y)) -> app#(-(), app(app(div(), app(D(), x)), y)))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(div(), x), y)) -> app#(*(), x))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(div(), x), y)) -> app#(D(), y))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(div(), x), y)) -> app#(D(), x))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(div(), x), y)) -> app#(app(pow(), y), 2()))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(div(), x), y)) -> app#(app(div(), app(D(), x)), y))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(div(), x), y)) -> app#(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2())))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(div(), x), y)) -> app#(app(-(), app(app(div(), app(D(), x)), y)), app(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2()))))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(div(), x), y)) -> app#(app(*(), x), app(D(), y)))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(-(), x), y)) -> app#(-(), app(D(), x)))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(-(), x), y)) -> app#(D(), y))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(-(), x), y)) -> app#(D(), x))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(-(), x), y)) -> app#(app(-(), app(D(), x)), app(D(), y)))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(*(), x), y)) -> app#(*(), y))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(*(), x), y)) -> app#(+(), app(app(*(), y), app(D(), x))))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(*(), x), y)) -> app#(D(), y))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(*(), x), y)) -> app#(D(), x))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(*(), x), y)) -> app#(app(*(), y), app(D(), x)))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(*(), x), y)) -> app#(app(*(), x), app(D(), y)))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(*(), x), y)) -> app#(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y))))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(+(), x), y)) -> app#(+(), app(D(), x)))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(+(), x), y)) -> app#(D(), y))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(+(), x), y)) -> app#(D(), x))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(+(), x), y)) -> app#(app(+(), app(D(), x)), app(D(), y)))
    (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(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#(f, 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(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#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(ln(), x)) -> app#(div(), app(D(), x)))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(ln(), x)) -> app#(D(), x))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(ln(), x)) -> app#(app(div(), app(D(), x)), x))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(minus(), x)) -> app#(minus(), app(D(), x)))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(minus(), x)) -> app#(D(), x))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(ln(), x))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(-(), y))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(pow(), x), y)))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(*(), y))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(pow(), x), app(app(-(), y), 1())))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(-(), y), 1()))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(pow(), x), y)), app(ln(), x)))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y)))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x)))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), y), app(app(pow(), x), app(app(-(), y), 1()))))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))), app(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y))))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(pow(), y))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(div(), app(D(), x)))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(div(), app(app(*(), x), app(D(), y))))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(-(), app(app(div(), app(D(), x)), y)))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(*(), x))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(app(pow(), y), 2()))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(app(div(), app(D(), x)), y))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2())))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(app(-(), app(app(div(), app(D(), x)), y)), app(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2()))))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(app(*(), x), app(D(), y)))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(-(), app(D(), x)))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(app(-(), app(D(), x)), app(D(), y)))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(*(), y))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(+(), app(app(*(), y), app(D(), x))))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(app(*(), y), app(D(), x)))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(app(*(), x), app(D(), y)))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y))))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(+(), app(D(), x)))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(app(+(), app(D(), x)), app(D(), y)))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(ln(), x)) -> app#(div(), app(D(), x)))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(ln(), x)) -> app#(D(), x))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(ln(), x)) -> app#(app(div(), app(D(), x)), x))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(minus(), x)) -> app#(minus(), app(D(), x)))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(minus(), x)) -> app#(D(), x))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(ln(), x))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(-(), y))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(pow(), x), y)))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(*(), y))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(pow(), x), app(app(-(), y), 1())))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(-(), y), 1()))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(pow(), x), y)), app(ln(), x)))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y)))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x)))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), y), app(app(pow(), x), app(app(-(), y), 1()))))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))), app(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y))))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(pow(), y))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(div(), app(D(), x)))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(div(), app(app(*(), x), app(D(), y))))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(-(), app(app(div(), app(D(), x)), y)))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(*(), x))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(app(pow(), y), 2()))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(app(div(), app(D(), x)), y))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2())))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(app(-(), app(app(div(), app(D(), x)), y)), app(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2()))))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(app(*(), x), app(D(), y)))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(-(), app(D(), x)))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(app(-(), app(D(), x)), app(D(), y)))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(*(), y))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(+(), app(app(*(), y), app(D(), x))))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(app(*(), y), app(D(), x)))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(app(*(), x), app(D(), y)))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y))))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(+(), app(D(), x)))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(app(+(), app(D(), x)), app(D(), y)))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(ln(), x)) -> app#(div(), app(D(), x)))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(ln(), x)) -> app#(D(), x))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(ln(), x)) -> app#(app(div(), app(D(), x)), x))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(minus(), x)) -> app#(minus(), app(D(), x)))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(minus(), x)) -> app#(D(), x))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(ln(), x))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(-(), y))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(pow(), x), y)))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(*(), y))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(pow(), x), app(app(-(), y), 1())))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(-(), y), 1()))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(pow(), x), y)), app(ln(), x)))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y)))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x)))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), y), app(app(pow(), x), app(app(-(), y), 1()))))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))), app(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y))))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(pow(), y))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(div(), app(D(), x)))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(div(), app(app(*(), x), app(D(), y))))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(-(), app(app(div(), app(D(), x)), y)))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(*(), x))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(app(pow(), y), 2()))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(app(div(), app(D(), x)), y))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2())))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(app(-(), app(app(div(), app(D(), x)), y)), app(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2()))))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(app(*(), x), app(D(), y)))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(-(), app(D(), x)))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(app(-(), app(D(), x)), app(D(), y)))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(*(), y))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(+(), app(app(*(), y), app(D(), x))))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(app(*(), y), app(D(), x)))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(app(*(), x), app(D(), y)))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y))))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(+(), app(D(), x)))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(app(+(), app(D(), x)), app(D(), y)))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(ln(), x)) -> app#(div(), app(D(), x)))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(ln(), x)) -> app#(D(), x))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(ln(), x)) -> app#(app(div(), app(D(), x)), x))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(minus(), x)) -> app#(minus(), app(D(), x)))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(minus(), x)) -> app#(D(), x))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(ln(), x))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(-(), y))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(pow(), x), y)))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(*(), y))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(D(), y))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(D(), x))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(pow(), x), app(app(-(), y), 1())))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(-(), y), 1()))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(pow(), x), y)), app(ln(), x)))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y)))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x)))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), y), app(app(pow(), x), app(app(-(), y), 1()))))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))), app(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y))))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(pow(), y))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(div(), app(D(), x)))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(div(), app(app(*(), x), app(D(), y))))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(-(), app(app(div(), app(D(), x)), y)))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(*(), x))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(D(), y))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(D(), x))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(app(pow(), y), 2()))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(app(div(), app(D(), x)), y))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2())))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(app(-(), app(app(div(), app(D(), x)), y)), app(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2()))))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(app(*(), x), app(D(), y)))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(-(), app(D(), x)))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(D(), y))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(D(), x))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(app(-(), app(D(), x)), app(D(), y)))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(*(), y))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(+(), app(app(*(), y), app(D(), x))))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(D(), y))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(D(), x))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(app(*(), y), app(D(), x)))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(app(*(), x), app(D(), y)))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y))))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(+(), app(D(), x)))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(D(), y))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(D(), x))
    (app#(D(), app(minus(), x)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(app(+(), app(D(), x)), app(D(), y)))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(app(+(), app(D(), x)), app(D(), y)))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(D(), x))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(D(), y))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(+(), app(D(), x)))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y))))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(app(*(), x), app(D(), y)))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(app(*(), y), app(D(), x)))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(D(), x))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(D(), y))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(+(), app(app(*(), y), app(D(), x))))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(*(), y))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(app(-(), app(D(), x)), app(D(), y)))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(D(), x))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(D(), y))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(-(), app(D(), x)))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(app(*(), x), app(D(), y)))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(app(-(), app(app(div(), app(D(), x)), y)), app(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2()))))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2())))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(app(div(), app(D(), x)), y))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(app(pow(), y), 2()))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(D(), x))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(D(), y))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(*(), x))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(-(), app(app(div(), app(D(), x)), y)))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(div(), app(app(*(), x), app(D(), y))))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(div(), app(D(), x)))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(pow(), y))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))), app(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y))))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), y), app(app(pow(), x), app(app(-(), y), 1()))))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x)))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y)))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(pow(), x), y)), app(ln(), x)))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(-(), y), 1()))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(pow(), x), app(app(-(), y), 1())))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(D(), x))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(D(), y))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(*(), y))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(pow(), x), y)))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(-(), y))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(ln(), x))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(minus(), x)) -> app#(D(), x))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(minus(), x)) -> app#(minus(), app(D(), x)))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(ln(), x)) -> app#(app(div(), app(D(), x)), x))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(ln(), x)) -> app#(D(), x))
    (app#(D(), app(ln(), x)) -> app#(D(), x), app#(D(), app(ln(), x)) -> app#(div(), app(D(), x)))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(app(+(), app(D(), x)), app(D(), y)))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(+(), app(D(), x)))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y))))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(app(*(), x), app(D(), y)))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(app(*(), y), app(D(), x)))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(+(), app(app(*(), y), app(D(), x))))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(*(), y))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(app(-(), app(D(), x)), app(D(), y)))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(-(), app(D(), x)))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(app(*(), x), app(D(), y)))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(app(-(), app(app(div(), app(D(), x)), y)), app(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2()))))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2())))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(app(div(), app(D(), x)), y))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(app(pow(), y), 2()))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(*(), x))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(-(), app(app(div(), app(D(), x)), y)))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(div(), app(app(*(), x), app(D(), y))))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(div(), app(D(), x)))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(pow(), y))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))), app(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y))))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), y), app(app(pow(), x), app(app(-(), y), 1()))))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x)))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y)))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(pow(), x), y)), app(ln(), x)))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(-(), y), 1()))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(pow(), x), app(app(-(), y), 1())))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(*(), y))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(pow(), x), y)))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(-(), y))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(ln(), x))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(minus(), x)) -> app#(D(), x))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(minus(), x)) -> app#(minus(), app(D(), x)))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(ln(), x)) -> app#(app(div(), app(D(), x)), x))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(ln(), x)) -> app#(D(), x))
    (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(ln(), x)) -> app#(div(), app(D(), x)))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(app(+(), app(D(), x)), app(D(), y)))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(+(), app(D(), x)))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y))))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(app(*(), x), app(D(), y)))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(app(*(), y), app(D(), x)))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(+(), app(app(*(), y), app(D(), x))))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(*(), y))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(app(-(), app(D(), x)), app(D(), y)))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(-(), app(D(), x)))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(app(*(), x), app(D(), y)))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(app(-(), app(app(div(), app(D(), x)), y)), app(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2()))))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2())))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(app(div(), app(D(), x)), y))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(app(pow(), y), 2()))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(*(), x))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(-(), app(app(div(), app(D(), x)), y)))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(div(), app(app(*(), x), app(D(), y))))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(div(), app(D(), x)))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(div(), x), y)) -> app#(pow(), y))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))), app(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y))))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), y), app(app(pow(), x), app(app(-(), y), 1()))))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x)))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y)))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(pow(), x), y)), app(ln(), x)))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(-(), y), 1()))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(app(pow(), x), app(app(-(), y), 1())))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(*(), y))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(pow(), x), y)))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(-(), y))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(pow(), x), y)) -> app#(ln(), x))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(minus(), x)) -> app#(D(), x))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(minus(), x)) -> app#(minus(), app(D(), x)))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(ln(), x)) -> app#(app(div(), app(D(), x)), x))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(ln(), x)) -> app#(D(), x))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(ln(), x)) -> app#(div(), app(D(), 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(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#(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#(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(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(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#(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#(D(), app(app(+(), x), y)) -> app#(app(+(), app(D(), x)), app(D(), y)))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(+(), x), y)) -> app#(D(), x))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(+(), x), y)) -> app#(D(), y))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(+(), x), y)) -> app#(+(), app(D(), x)))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(*(), x), y)) -> app#(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y))))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(*(), x), y)) -> app#(app(*(), x), app(D(), y)))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(*(), x), y)) -> app#(app(*(), y), app(D(), x)))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(*(), x), y)) -> app#(D(), x))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(*(), x), y)) -> app#(D(), y))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(*(), x), y)) -> app#(+(), app(app(*(), y), app(D(), x))))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(*(), x), y)) -> app#(*(), y))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(-(), x), y)) -> app#(app(-(), app(D(), x)), app(D(), y)))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(-(), x), y)) -> app#(D(), x))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(-(), x), y)) -> app#(D(), y))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(-(), x), y)) -> app#(-(), app(D(), x)))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(div(), x), y)) -> app#(app(*(), x), app(D(), y)))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(div(), x), y)) -> app#(app(-(), app(app(div(), app(D(), x)), y)), app(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2()))))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(div(), x), y)) -> app#(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2())))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(div(), x), y)) -> app#(app(div(), app(D(), x)), y))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(div(), x), y)) -> app#(app(pow(), y), 2()))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(div(), x), y)) -> app#(D(), x))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(div(), x), y)) -> app#(D(), y))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(div(), x), y)) -> app#(*(), x))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(div(), x), y)) -> app#(-(), app(app(div(), app(D(), x)), y)))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(div(), x), y)) -> app#(div(), app(app(*(), x), app(D(), y))))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(div(), x), y)) -> app#(div(), app(D(), x)))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(div(), x), y)) -> app#(pow(), y))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(pow(), x), y)) -> app#(app(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))), app(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y))))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), y), app(app(pow(), x), app(app(-(), y), 1()))))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x)))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y)))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(pow(), x), y)), app(ln(), x)))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(pow(), x), y)) -> app#(app(-(), y), 1()))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(pow(), x), y)) -> app#(app(pow(), x), app(app(-(), y), 1())))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(pow(), x), y)) -> app#(D(), x))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(pow(), x), y)) -> app#(D(), y))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(pow(), x), y)) -> app#(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(pow(), x), y)) -> app#(*(), y))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(pow(), x), y)))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(pow(), x), y)) -> app#(-(), y))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(pow(), x), y)) -> app#(ln(), x))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(minus(), x)) -> app#(D(), x))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(minus(), x)) -> app#(minus(), app(D(), x)))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(ln(), x)) -> app#(app(div(), app(D(), x)), x))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(ln(), x)) -> app#(D(), x))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(ln(), x)) -> app#(div(), app(D(), x)))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(+(), x), y)) -> app#(app(+(), app(D(), x)), app(D(), y)))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(+(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(+(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(+(), x), y)) -> app#(+(), app(D(), x)))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y))))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(app(*(), x), app(D(), y)))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(app(*(), y), app(D(), x)))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(+(), app(app(*(), y), app(D(), x))))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(*(), y))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(-(), x), y)) -> app#(app(-(), app(D(), x)), app(D(), y)))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(-(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(-(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(-(), x), y)) -> app#(-(), app(D(), x)))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(app(*(), x), app(D(), y)))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(app(-(), app(app(div(), app(D(), x)), y)), app(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2()))))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2())))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(app(div(), app(D(), x)), y))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(app(pow(), y), 2()))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(*(), x))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(-(), app(app(div(), app(D(), x)), y)))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(div(), app(app(*(), x), app(D(), y))))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(div(), app(D(), x)))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(pow(), y))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(app(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))), app(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y))))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), y), app(app(pow(), x), app(app(-(), y), 1()))))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x)))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y)))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(pow(), x), y)), app(ln(), x)))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(app(-(), y), 1()))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(app(pow(), x), app(app(-(), y), 1())))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(*(), y))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(pow(), x), y)))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(-(), y))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(ln(), x))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(minus(), x)) -> app#(D(), x))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(minus(), x)) -> app#(minus(), app(D(), x)))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(ln(), x)) -> app#(app(div(), app(D(), x)), x))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(ln(), x)) -> app#(D(), x))
    (app#(D(), app(app(pow(), x), y)) -> app#(D(), y), app#(D(), app(ln(), x)) -> app#(div(), app(D(), x)))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(+(), x), y)) -> app#(app(+(), app(D(), x)), app(D(), y)))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(+(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(+(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(+(), x), y)) -> app#(+(), app(D(), x)))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y))))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(app(*(), x), app(D(), y)))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(app(*(), y), app(D(), x)))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(+(), app(app(*(), y), app(D(), x))))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(*(), y))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(-(), x), y)) -> app#(app(-(), app(D(), x)), app(D(), y)))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(-(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(-(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(-(), x), y)) -> app#(-(), app(D(), x)))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(app(*(), x), app(D(), y)))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(app(-(), app(app(div(), app(D(), x)), y)), app(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2()))))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2())))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(app(div(), app(D(), x)), y))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(app(pow(), y), 2()))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(*(), x))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(-(), app(app(div(), app(D(), x)), y)))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(div(), app(app(*(), x), app(D(), y))))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(div(), app(D(), x)))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(pow(), y))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(app(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))), app(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y))))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), y), app(app(pow(), x), app(app(-(), y), 1()))))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x)))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y)))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(pow(), x), y)), app(ln(), x)))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(app(-(), y), 1()))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(app(pow(), x), app(app(-(), y), 1())))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(*(), y))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(pow(), x), y)))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(-(), y))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(ln(), x))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(minus(), x)) -> app#(D(), x))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(minus(), x)) -> app#(minus(), app(D(), x)))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(ln(), x)) -> app#(app(div(), app(D(), x)), x))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(ln(), x)) -> app#(D(), x))
    (app#(D(), app(app(div(), x), y)) -> app#(D(), y), app#(D(), app(ln(), x)) -> app#(div(), app(D(), x)))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(+(), x), y)) -> app#(app(+(), app(D(), x)), app(D(), y)))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(+(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(+(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(+(), x), y)) -> app#(+(), app(D(), x)))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y))))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(app(*(), x), app(D(), y)))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(app(*(), y), app(D(), x)))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(+(), app(app(*(), y), app(D(), x))))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(*(), y))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(-(), x), y)) -> app#(app(-(), app(D(), x)), app(D(), y)))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(-(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(-(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(-(), x), y)) -> app#(-(), app(D(), x)))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(app(*(), x), app(D(), y)))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(app(-(), app(app(div(), app(D(), x)), y)), app(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2()))))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2())))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(app(div(), app(D(), x)), y))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(app(pow(), y), 2()))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(*(), x))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(-(), app(app(div(), app(D(), x)), y)))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(div(), app(app(*(), x), app(D(), y))))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(div(), app(D(), x)))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(div(), x), y)) -> app#(pow(), y))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(app(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))), app(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y))))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), y), app(app(pow(), x), app(app(-(), y), 1()))))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x)))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y)))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(app(*(), app(app(pow(), x), y)), app(ln(), x)))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(app(-(), y), 1()))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(app(pow(), x), app(app(-(), y), 1())))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(D(), x))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(D(), y))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(*(), y))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(*(), app(app(pow(), x), y)))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(-(), y))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(pow(), x), y)) -> app#(ln(), x))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(minus(), x)) -> app#(D(), x))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(minus(), x)) -> app#(minus(), app(D(), x)))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(ln(), x)) -> app#(app(div(), app(D(), x)), x))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(ln(), x)) -> app#(D(), x))
    (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(ln(), x)) -> app#(div(), app(D(), x)))
   }
   STATUS:
    arrows: 0.819602
    SCCS (2):
     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)}
     Scc:
      {  app#(D(), app(app(+(), x), y)) -> app#(D(), x),
         app#(D(), app(app(+(), x), y)) -> app#(D(), y),
         app#(D(), app(app(*(), x), y)) -> app#(D(), x),
         app#(D(), app(app(*(), x), y)) -> app#(D(), y),
         app#(D(), app(app(-(), x), y)) -> app#(D(), x),
         app#(D(), app(app(-(), x), y)) -> app#(D(), y),
       app#(D(), app(app(div(), x), y)) -> app#(D(), x),
       app#(D(), app(app(div(), x), y)) -> app#(D(), y),
       app#(D(), app(app(pow(), x), y)) -> app#(D(), x),
       app#(D(), app(app(pow(), x), y)) -> app#(D(), y),
             app#(D(), app(minus(), x)) -> app#(D(), x),
                app#(D(), app(ln(), x)) -> app#(D(), x)}
     
     SCC (5):
      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)}
      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(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(D(), app(app(+(), x), y)) -> app(app(+(), app(D(), x)), app(D(), y)),
                          app(D(), app(app(*(), x), y)) -> app(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y))),
                          app(D(), app(app(-(), x), y)) -> app(app(-(), app(D(), x)), app(D(), y)),
                        app(D(), app(app(div(), x), y)) -> app(app(-(), app(app(div(), app(D(), x)), y)), app(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2()))),
                        app(D(), app(app(pow(), x), y)) -> app(app(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))), app(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y))),
                              app(D(), app(minus(), x)) -> app(minus(), app(D(), x)),
                                 app(D(), app(ln(), x)) -> app(app(div(), app(D(), x)), x),
                                          app(D(), t()) -> 1(),
                                   app(D(), constant()) -> 0()}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [app](x0, x1) = x0 + x1,
        
        [1] = 0,
        
        [D] = 0,
        
        [t] = 0,
        
        [0] = 0,
        
        [constant] = 0,
        
        [+] = 0,
        
        [*] = 0,
        
        [-] = 0,
        
        [minus] = 0,
        
        [div] = 0,
        
        [pow] = 0,
        
        [2] = 0,
        
        [ln] = 0,
        
        [nil] = 0,
        
        [map] = 0,
        
        [cons] = 1,
        
        [filter] = 0,
        
        [filter2] = 0,
        
        [true] = 0,
        
        [false] = 0,
        
        [app#](x0, x1) = x0
       Strict:
        app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x)
        1 + 1x + 0f + 1xs >= 0 + 1x + 0f
        app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs)
        1 + 1x + 0f + 1xs >= 0 + 0f + 1xs
        app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x)
        1 + 1x + 0f + 1xs >= 0 + 1x + 0f
        app#(app(app(app(filter2(), false()), f), x), xs) -> app#(app(filter(), f), xs)
        0 + 0x + 0f + 1xs >= 0 + 0f + 1xs
        app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(filter(), f), xs)
        0 + 0x + 0f + 1xs >= 0 + 0f + 1xs
       Weak:
        app(D(), constant()) -> 0()
        0 >= 0
        app(D(), t()) -> 1()
        0 >= 0
        app(D(), app(ln(), x)) -> app(app(div(), app(D(), x)), x)
        0 + 1x >= 0 + 2x
        app(D(), app(minus(), x)) -> app(minus(), app(D(), x))
        0 + 1x >= 0 + 1x
        app(D(), app(app(pow(), x), y)) -> app(app(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))), app(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y)))
        0 + 1x + 1y >= 0 + 4x + 4y
        app(D(), app(app(div(), x), y)) -> app(app(-(), app(app(div(), app(D(), x)), y)), app(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2())))
        0 + 1x + 1y >= 0 + 2x + 3y
        app(D(), app(app(-(), x), y)) -> app(app(-(), app(D(), x)), app(D(), y))
        0 + 1x + 1y >= 0 + 1x + 1y
        app(D(), app(app(*(), x), y)) -> app(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y)))
        0 + 1x + 1y >= 0 + 2x + 2y
        app(D(), app(app(+(), x), y)) -> app(app(+(), app(D(), x)), app(D(), y))
        0 + 1x + 1y >= 0 + 1x + 1y
        app(app(filter(), f), nil()) -> nil()
        0 + 1f >= 0
        app(app(filter(), f), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(f, x)), f), x), xs)
        1 + 1x + 1f + 1xs >= 0 + 2x + 2f + 1xs
        app(app(map(), f), nil()) -> nil()
        0 + 1f >= 0
        app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs))
        1 + 1x + 1f + 1xs >= 1 + 1x + 2f + 1xs
        app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs)
        0 + 1x + 1f + 1xs >= 0 + 1f + 1xs
        app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs))
        0 + 1x + 1f + 1xs >= 1 + 1x + 1f + 1xs
      SCCS (0):
       
       
       
    
    
    
    
    
    
    
    
    
    
    SCC (12):
     Strict:
      {  app#(D(), app(app(+(), x), y)) -> app#(D(), x),
         app#(D(), app(app(+(), x), y)) -> app#(D(), y),
         app#(D(), app(app(*(), x), y)) -> app#(D(), x),
         app#(D(), app(app(*(), x), y)) -> app#(D(), y),
         app#(D(), app(app(-(), x), y)) -> app#(D(), x),
         app#(D(), app(app(-(), x), y)) -> app#(D(), y),
       app#(D(), app(app(div(), x), y)) -> app#(D(), x),
       app#(D(), app(app(div(), x), y)) -> app#(D(), y),
       app#(D(), app(app(pow(), x), y)) -> app#(D(), x),
       app#(D(), app(app(pow(), x), y)) -> app#(D(), y),
             app#(D(), app(minus(), x)) -> app#(D(), x),
                app#(D(), app(ln(), x)) -> app#(D(), x)}
     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(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(D(), app(app(+(), x), y)) -> app(app(+(), app(D(), x)), app(D(), y)),
                         app(D(), app(app(*(), x), y)) -> app(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y))),
                         app(D(), app(app(-(), x), y)) -> app(app(-(), app(D(), x)), app(D(), y)),
                       app(D(), app(app(div(), x), y)) -> app(app(-(), app(app(div(), app(D(), x)), y)), app(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2()))),
                       app(D(), app(app(pow(), x), y)) -> app(app(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))), app(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y))),
                             app(D(), app(minus(), x)) -> app(minus(), app(D(), x)),
                                app(D(), app(ln(), x)) -> app(app(div(), app(D(), x)), x),
                                         app(D(), t()) -> 1(),
                                  app(D(), constant()) -> 0()}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [app](x0, x1) = x0 + x1,
       
       [1] = 0,
       
       [D] = 1,
       
       [t] = 1,
       
       [0] = 0,
       
       [constant] = 1,
       
       [+] = 0,
       
       [*] = 0,
       
       [-] = 0,
       
       [minus] = 0,
       
       [div] = 0,
       
       [pow] = 0,
       
       [2] = 1,
       
       [ln] = 1,
       
       [nil] = 0,
       
       [map] = 0,
       
       [cons] = 0,
       
       [filter] = 0,
       
       [filter2] = 0,
       
       [true] = 0,
       
       [false] = 0,
       
       [app#](x0, x1) = x0 + x1
      Strict:
       app#(D(), app(ln(), x)) -> app#(D(), x)
       2 + 1x >= 1 + 1x
       app#(D(), app(minus(), x)) -> app#(D(), x)
       1 + 1x >= 1 + 1x
       app#(D(), app(app(pow(), x), y)) -> app#(D(), y)
       1 + 1x + 1y >= 1 + 1y
       app#(D(), app(app(pow(), x), y)) -> app#(D(), x)
       1 + 1x + 1y >= 1 + 1x
       app#(D(), app(app(div(), x), y)) -> app#(D(), y)
       1 + 1x + 1y >= 1 + 1y
       app#(D(), app(app(div(), x), y)) -> app#(D(), x)
       1 + 1x + 1y >= 1 + 1x
       app#(D(), app(app(-(), x), y)) -> app#(D(), y)
       1 + 1x + 1y >= 1 + 1y
       app#(D(), app(app(-(), x), y)) -> app#(D(), x)
       1 + 1x + 1y >= 1 + 1x
       app#(D(), app(app(*(), x), y)) -> app#(D(), y)
       1 + 1x + 1y >= 1 + 1y
       app#(D(), app(app(*(), x), y)) -> app#(D(), x)
       1 + 1x + 1y >= 1 + 1x
       app#(D(), app(app(+(), x), y)) -> app#(D(), y)
       1 + 1x + 1y >= 1 + 1y
       app#(D(), app(app(+(), x), y)) -> app#(D(), x)
       1 + 1x + 1y >= 1 + 1x
      Weak:
       app(D(), constant()) -> 0()
       2 >= 0
       app(D(), t()) -> 1()
       2 >= 0
       app(D(), app(ln(), x)) -> app(app(div(), app(D(), x)), x)
       2 + 1x >= 1 + 2x
       app(D(), app(minus(), x)) -> app(minus(), app(D(), x))
       1 + 1x >= 1 + 1x
       app(D(), app(app(pow(), x), y)) -> app(app(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))), app(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y)))
       1 + 1x + 1y >= 3 + 4x + 4y
       app(D(), app(app(div(), x), y)) -> app(app(-(), app(app(div(), app(D(), x)), y)), app(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2())))
       1 + 1x + 1y >= 3 + 2x + 3y
       app(D(), app(app(-(), x), y)) -> app(app(-(), app(D(), x)), app(D(), y))
       1 + 1x + 1y >= 2 + 1x + 1y
       app(D(), app(app(*(), x), y)) -> app(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y)))
       1 + 1x + 1y >= 2 + 2x + 2y
       app(D(), app(app(+(), x), y)) -> app(app(+(), app(D(), x)), app(D(), y))
       1 + 1x + 1y >= 2 + 1x + 1y
       app(app(filter(), f), nil()) -> nil()
       0 + 1f >= 0
       app(app(filter(), f), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(f, x)), f), x), xs)
       0 + 1x + 1f + 1xs >= 0 + 2x + 2f + 1xs
       app(app(map(), f), nil()) -> nil()
       0 + 1f >= 0
       app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs))
       0 + 1x + 1f + 1xs >= 0 + 1x + 2f + 1xs
       app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs)
       0 + 1x + 1f + 1xs >= 0 + 1f + 1xs
       app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs))
       0 + 1x + 1f + 1xs >= 0 + 1x + 1f + 1xs
     SCCS (1):
      Scc:
       {  app#(D(), app(app(+(), x), y)) -> app#(D(), x),
          app#(D(), app(app(+(), x), y)) -> app#(D(), y),
          app#(D(), app(app(*(), x), y)) -> app#(D(), x),
          app#(D(), app(app(*(), x), y)) -> app#(D(), y),
          app#(D(), app(app(-(), x), y)) -> app#(D(), x),
          app#(D(), app(app(-(), x), y)) -> app#(D(), y),
        app#(D(), app(app(div(), x), y)) -> app#(D(), x),
        app#(D(), app(app(div(), x), y)) -> app#(D(), y),
        app#(D(), app(app(pow(), x), y)) -> app#(D(), x),
        app#(D(), app(app(pow(), x), y)) -> app#(D(), y),
              app#(D(), app(minus(), x)) -> app#(D(), x)}
      
      SCC (11):
       Strict:
        {  app#(D(), app(app(+(), x), y)) -> app#(D(), x),
           app#(D(), app(app(+(), x), y)) -> app#(D(), y),
           app#(D(), app(app(*(), x), y)) -> app#(D(), x),
           app#(D(), app(app(*(), x), y)) -> app#(D(), y),
           app#(D(), app(app(-(), x), y)) -> app#(D(), x),
           app#(D(), app(app(-(), x), y)) -> app#(D(), y),
         app#(D(), app(app(div(), x), y)) -> app#(D(), x),
         app#(D(), app(app(div(), x), y)) -> app#(D(), y),
         app#(D(), app(app(pow(), x), y)) -> app#(D(), x),
         app#(D(), app(app(pow(), x), y)) -> app#(D(), y),
               app#(D(), app(minus(), x)) -> app#(D(), x)}
       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(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(D(), app(app(+(), x), y)) -> app(app(+(), app(D(), x)), app(D(), y)),
                           app(D(), app(app(*(), x), y)) -> app(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y))),
                           app(D(), app(app(-(), x), y)) -> app(app(-(), app(D(), x)), app(D(), y)),
                         app(D(), app(app(div(), x), y)) -> app(app(-(), app(app(div(), app(D(), x)), y)), app(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2()))),
                         app(D(), app(app(pow(), x), y)) -> app(app(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))), app(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y))),
                               app(D(), app(minus(), x)) -> app(minus(), app(D(), x)),
                                  app(D(), app(ln(), x)) -> app(app(div(), app(D(), x)), x),
                                           app(D(), t()) -> 1(),
                                    app(D(), constant()) -> 0()}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [app](x0, x1) = x0 + x1,
         
         [1] = 0,
         
         [D] = 1,
         
         [t] = 1,
         
         [0] = 0,
         
         [constant] = 1,
         
         [+] = 0,
         
         [*] = 0,
         
         [-] = 0,
         
         [minus] = 1,
         
         [div] = 0,
         
         [pow] = 0,
         
         [2] = 1,
         
         [ln] = 1,
         
         [nil] = 0,
         
         [map] = 0,
         
         [cons] = 0,
         
         [filter] = 0,
         
         [filter2] = 0,
         
         [true] = 0,
         
         [false] = 0,
         
         [app#](x0, x1) = x0 + x1
        Strict:
         app#(D(), app(minus(), x)) -> app#(D(), x)
         2 + 1x >= 1 + 1x
         app#(D(), app(app(pow(), x), y)) -> app#(D(), y)
         1 + 1x + 1y >= 1 + 1y
         app#(D(), app(app(pow(), x), y)) -> app#(D(), x)
         1 + 1x + 1y >= 1 + 1x
         app#(D(), app(app(div(), x), y)) -> app#(D(), y)
         1 + 1x + 1y >= 1 + 1y
         app#(D(), app(app(div(), x), y)) -> app#(D(), x)
         1 + 1x + 1y >= 1 + 1x
         app#(D(), app(app(-(), x), y)) -> app#(D(), y)
         1 + 1x + 1y >= 1 + 1y
         app#(D(), app(app(-(), x), y)) -> app#(D(), x)
         1 + 1x + 1y >= 1 + 1x
         app#(D(), app(app(*(), x), y)) -> app#(D(), y)
         1 + 1x + 1y >= 1 + 1y
         app#(D(), app(app(*(), x), y)) -> app#(D(), x)
         1 + 1x + 1y >= 1 + 1x
         app#(D(), app(app(+(), x), y)) -> app#(D(), y)
         1 + 1x + 1y >= 1 + 1y
         app#(D(), app(app(+(), x), y)) -> app#(D(), x)
         1 + 1x + 1y >= 1 + 1x
        Weak:
         app(D(), constant()) -> 0()
         2 >= 0
         app(D(), t()) -> 1()
         2 >= 0
         app(D(), app(ln(), x)) -> app(app(div(), app(D(), x)), x)
         2 + 1x >= 1 + 2x
         app(D(), app(minus(), x)) -> app(minus(), app(D(), x))
         2 + 1x >= 2 + 1x
         app(D(), app(app(pow(), x), y)) -> app(app(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))), app(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y)))
         1 + 1x + 1y >= 3 + 4x + 4y
         app(D(), app(app(div(), x), y)) -> app(app(-(), app(app(div(), app(D(), x)), y)), app(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2())))
         1 + 1x + 1y >= 3 + 2x + 3y
         app(D(), app(app(-(), x), y)) -> app(app(-(), app(D(), x)), app(D(), y))
         1 + 1x + 1y >= 2 + 1x + 1y
         app(D(), app(app(*(), x), y)) -> app(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y)))
         1 + 1x + 1y >= 2 + 2x + 2y
         app(D(), app(app(+(), x), y)) -> app(app(+(), app(D(), x)), app(D(), y))
         1 + 1x + 1y >= 2 + 1x + 1y
         app(app(filter(), f), nil()) -> nil()
         0 + 1f >= 0
         app(app(filter(), f), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(f, x)), f), x), xs)
         0 + 1x + 1f + 1xs >= 0 + 2x + 2f + 1xs
         app(app(map(), f), nil()) -> nil()
         0 + 1f >= 0
         app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs))
         0 + 1x + 1f + 1xs >= 0 + 1x + 2f + 1xs
         app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs)
         0 + 1x + 1f + 1xs >= 0 + 1f + 1xs
         app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs))
         0 + 1x + 1f + 1xs >= 0 + 1x + 1f + 1xs
       SCCS (1):
        Scc:
         {  app#(D(), app(app(+(), x), y)) -> app#(D(), x),
            app#(D(), app(app(+(), x), y)) -> app#(D(), y),
            app#(D(), app(app(*(), x), y)) -> app#(D(), x),
            app#(D(), app(app(*(), x), y)) -> app#(D(), y),
            app#(D(), app(app(-(), x), y)) -> app#(D(), x),
            app#(D(), app(app(-(), x), y)) -> app#(D(), y),
          app#(D(), app(app(div(), x), y)) -> app#(D(), x),
          app#(D(), app(app(div(), x), y)) -> app#(D(), y),
          app#(D(), app(app(pow(), x), y)) -> app#(D(), x),
          app#(D(), app(app(pow(), x), y)) -> app#(D(), y)}
        
        SCC (10):
         Strict:
          {  app#(D(), app(app(+(), x), y)) -> app#(D(), x),
             app#(D(), app(app(+(), x), y)) -> app#(D(), y),
             app#(D(), app(app(*(), x), y)) -> app#(D(), x),
             app#(D(), app(app(*(), x), y)) -> app#(D(), y),
             app#(D(), app(app(-(), x), y)) -> app#(D(), x),
             app#(D(), app(app(-(), x), y)) -> app#(D(), y),
           app#(D(), app(app(div(), x), y)) -> app#(D(), x),
           app#(D(), app(app(div(), x), y)) -> app#(D(), y),
           app#(D(), app(app(pow(), x), y)) -> app#(D(), x),
           app#(D(), app(app(pow(), x), y)) -> app#(D(), 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(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(D(), app(app(+(), x), y)) -> app(app(+(), app(D(), x)), app(D(), y)),
                             app(D(), app(app(*(), x), y)) -> app(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y))),
                             app(D(), app(app(-(), x), y)) -> app(app(-(), app(D(), x)), app(D(), y)),
                           app(D(), app(app(div(), x), y)) -> app(app(-(), app(app(div(), app(D(), x)), y)), app(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2()))),
                           app(D(), app(app(pow(), x), y)) -> app(app(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))), app(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y))),
                                 app(D(), app(minus(), x)) -> app(minus(), app(D(), x)),
                                    app(D(), app(ln(), x)) -> app(app(div(), app(D(), x)), x),
                                             app(D(), t()) -> 1(),
                                      app(D(), constant()) -> 0()}
         POLY:
          Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
          Interpretation:
           [app](x0, x1) = x0 + x1,
           
           [1] = 0,
           
           [D] = 1,
           
           [t] = 1,
           
           [0] = 0,
           
           [constant] = 1,
           
           [+] = 0,
           
           [*] = 0,
           
           [-] = 0,
           
           [minus] = 0,
           
           [div] = 0,
           
           [pow] = 1,
           
           [2] = 0,
           
           [ln] = 0,
           
           [nil] = 0,
           
           [map] = 0,
           
           [cons] = 0,
           
           [filter] = 0,
           
           [filter2] = 0,
           
           [true] = 0,
           
           [false] = 0,
           
           [app#](x0, x1) = x0 + x1
          Strict:
           app#(D(), app(app(pow(), x), y)) -> app#(D(), y)
           2 + 1x + 1y >= 1 + 1y
           app#(D(), app(app(pow(), x), y)) -> app#(D(), x)
           2 + 1x + 1y >= 1 + 1x
           app#(D(), app(app(div(), x), y)) -> app#(D(), y)
           1 + 1x + 1y >= 1 + 1y
           app#(D(), app(app(div(), x), y)) -> app#(D(), x)
           1 + 1x + 1y >= 1 + 1x
           app#(D(), app(app(-(), x), y)) -> app#(D(), y)
           1 + 1x + 1y >= 1 + 1y
           app#(D(), app(app(-(), x), y)) -> app#(D(), x)
           1 + 1x + 1y >= 1 + 1x
           app#(D(), app(app(*(), x), y)) -> app#(D(), y)
           1 + 1x + 1y >= 1 + 1y
           app#(D(), app(app(*(), x), y)) -> app#(D(), x)
           1 + 1x + 1y >= 1 + 1x
           app#(D(), app(app(+(), x), y)) -> app#(D(), y)
           1 + 1x + 1y >= 1 + 1y
           app#(D(), app(app(+(), x), y)) -> app#(D(), x)
           1 + 1x + 1y >= 1 + 1x
          Weak:
           app(D(), constant()) -> 0()
           2 >= 0
           app(D(), t()) -> 1()
           2 >= 0
           app(D(), app(ln(), x)) -> app(app(div(), app(D(), x)), x)
           1 + 1x >= 1 + 2x
           app(D(), app(minus(), x)) -> app(minus(), app(D(), x))
           1 + 1x >= 1 + 1x
           app(D(), app(app(pow(), x), y)) -> app(app(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))), app(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y)))
           2 + 1x + 1y >= 4 + 4x + 4y
           app(D(), app(app(div(), x), y)) -> app(app(-(), app(app(div(), app(D(), x)), y)), app(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2())))
           1 + 1x + 1y >= 3 + 2x + 3y
           app(D(), app(app(-(), x), y)) -> app(app(-(), app(D(), x)), app(D(), y))
           1 + 1x + 1y >= 2 + 1x + 1y
           app(D(), app(app(*(), x), y)) -> app(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y)))
           1 + 1x + 1y >= 2 + 2x + 2y
           app(D(), app(app(+(), x), y)) -> app(app(+(), app(D(), x)), app(D(), y))
           1 + 1x + 1y >= 2 + 1x + 1y
           app(app(filter(), f), nil()) -> nil()
           0 + 1f >= 0
           app(app(filter(), f), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(f, x)), f), x), xs)
           0 + 1x + 1f + 1xs >= 0 + 2x + 2f + 1xs
           app(app(map(), f), nil()) -> nil()
           0 + 1f >= 0
           app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs))
           0 + 1x + 1f + 1xs >= 0 + 1x + 2f + 1xs
           app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs)
           0 + 1x + 1f + 1xs >= 0 + 1f + 1xs
           app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs))
           0 + 1x + 1f + 1xs >= 0 + 1x + 1f + 1xs
         SCCS (1):
          Scc:
           {  app#(D(), app(app(+(), x), y)) -> app#(D(), x),
              app#(D(), app(app(+(), x), y)) -> app#(D(), y),
              app#(D(), app(app(*(), x), y)) -> app#(D(), x),
              app#(D(), app(app(*(), x), y)) -> app#(D(), y),
              app#(D(), app(app(-(), x), y)) -> app#(D(), x),
              app#(D(), app(app(-(), x), y)) -> app#(D(), y),
            app#(D(), app(app(div(), x), y)) -> app#(D(), x),
            app#(D(), app(app(div(), x), y)) -> app#(D(), y)}
          
          SCC (8):
           Strict:
            {  app#(D(), app(app(+(), x), y)) -> app#(D(), x),
               app#(D(), app(app(+(), x), y)) -> app#(D(), y),
               app#(D(), app(app(*(), x), y)) -> app#(D(), x),
               app#(D(), app(app(*(), x), y)) -> app#(D(), y),
               app#(D(), app(app(-(), x), y)) -> app#(D(), x),
               app#(D(), app(app(-(), x), y)) -> app#(D(), y),
             app#(D(), app(app(div(), x), y)) -> app#(D(), x),
             app#(D(), app(app(div(), x), y)) -> app#(D(), 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(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(D(), app(app(+(), x), y)) -> app(app(+(), app(D(), x)), app(D(), y)),
                               app(D(), app(app(*(), x), y)) -> app(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y))),
                               app(D(), app(app(-(), x), y)) -> app(app(-(), app(D(), x)), app(D(), y)),
                             app(D(), app(app(div(), x), y)) -> app(app(-(), app(app(div(), app(D(), x)), y)), app(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2()))),
                             app(D(), app(app(pow(), x), y)) -> app(app(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))), app(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y))),
                                   app(D(), app(minus(), x)) -> app(minus(), app(D(), x)),
                                      app(D(), app(ln(), x)) -> app(app(div(), app(D(), x)), x),
                                               app(D(), t()) -> 1(),
                                        app(D(), constant()) -> 0()}
           POLY:
            Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
            Interpretation:
             [app](x0, x1) = x0 + x1,
             
             [1] = 1,
             
             [D] = 1,
             
             [t] = 1,
             
             [0] = 0,
             
             [constant] = 1,
             
             [+] = 0,
             
             [*] = 0,
             
             [-] = 0,
             
             [minus] = 0,
             
             [div] = 1,
             
             [pow] = 0,
             
             [2] = 0,
             
             [ln] = 0,
             
             [nil] = 0,
             
             [map] = 0,
             
             [cons] = 0,
             
             [filter] = 0,
             
             [filter2] = 0,
             
             [true] = 0,
             
             [false] = 0,
             
             [app#](x0, x1) = x0 + x1
            Strict:
             app#(D(), app(app(div(), x), y)) -> app#(D(), y)
             2 + 1x + 1y >= 1 + 1y
             app#(D(), app(app(div(), x), y)) -> app#(D(), x)
             2 + 1x + 1y >= 1 + 1x
             app#(D(), app(app(-(), x), y)) -> app#(D(), y)
             1 + 1x + 1y >= 1 + 1y
             app#(D(), app(app(-(), x), y)) -> app#(D(), x)
             1 + 1x + 1y >= 1 + 1x
             app#(D(), app(app(*(), x), y)) -> app#(D(), y)
             1 + 1x + 1y >= 1 + 1y
             app#(D(), app(app(*(), x), y)) -> app#(D(), x)
             1 + 1x + 1y >= 1 + 1x
             app#(D(), app(app(+(), x), y)) -> app#(D(), y)
             1 + 1x + 1y >= 1 + 1y
             app#(D(), app(app(+(), x), y)) -> app#(D(), x)
             1 + 1x + 1y >= 1 + 1x
            Weak:
             app(D(), constant()) -> 0()
             2 >= 0
             app(D(), t()) -> 1()
             2 >= 1
             app(D(), app(ln(), x)) -> app(app(div(), app(D(), x)), x)
             1 + 1x >= 2 + 2x
             app(D(), app(minus(), x)) -> app(minus(), app(D(), x))
             1 + 1x >= 1 + 1x
             app(D(), app(app(pow(), x), y)) -> app(app(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))), app(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y)))
             1 + 1x + 1y >= 3 + 4x + 4y
             app(D(), app(app(div(), x), y)) -> app(app(-(), app(app(div(), app(D(), x)), y)), app(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2())))
             2 + 1x + 1y >= 4 + 2x + 3y
             app(D(), app(app(-(), x), y)) -> app(app(-(), app(D(), x)), app(D(), y))
             1 + 1x + 1y >= 2 + 1x + 1y
             app(D(), app(app(*(), x), y)) -> app(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y)))
             1 + 1x + 1y >= 2 + 2x + 2y
             app(D(), app(app(+(), x), y)) -> app(app(+(), app(D(), x)), app(D(), y))
             1 + 1x + 1y >= 2 + 1x + 1y
             app(app(filter(), f), nil()) -> nil()
             0 + 1f >= 0
             app(app(filter(), f), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(f, x)), f), x), xs)
             0 + 1x + 1f + 1xs >= 0 + 2x + 2f + 1xs
             app(app(map(), f), nil()) -> nil()
             0 + 1f >= 0
             app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs))
             0 + 1x + 1f + 1xs >= 0 + 1x + 2f + 1xs
             app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs)
             0 + 1x + 1f + 1xs >= 0 + 1f + 1xs
             app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs))
             0 + 1x + 1f + 1xs >= 0 + 1x + 1f + 1xs
           SCCS (1):
            Scc:
             {app#(D(), app(app(+(), x), y)) -> app#(D(), x),
              app#(D(), app(app(+(), x), y)) -> app#(D(), y),
              app#(D(), app(app(*(), x), y)) -> app#(D(), x),
              app#(D(), app(app(*(), x), y)) -> app#(D(), y),
              app#(D(), app(app(-(), x), y)) -> app#(D(), x),
              app#(D(), app(app(-(), x), y)) -> app#(D(), y)}
            
            SCC (6):
             Strict:
              {app#(D(), app(app(+(), x), y)) -> app#(D(), x),
               app#(D(), app(app(+(), x), y)) -> app#(D(), y),
               app#(D(), app(app(*(), x), y)) -> app#(D(), x),
               app#(D(), app(app(*(), x), y)) -> app#(D(), y),
               app#(D(), app(app(-(), x), y)) -> app#(D(), x),
               app#(D(), app(app(-(), x), y)) -> app#(D(), 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(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(D(), app(app(+(), x), y)) -> app(app(+(), app(D(), x)), app(D(), y)),
                                 app(D(), app(app(*(), x), y)) -> app(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y))),
                                 app(D(), app(app(-(), x), y)) -> app(app(-(), app(D(), x)), app(D(), y)),
                               app(D(), app(app(div(), x), y)) -> app(app(-(), app(app(div(), app(D(), x)), y)), app(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2()))),
                               app(D(), app(app(pow(), x), y)) -> app(app(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))), app(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y))),
                                     app(D(), app(minus(), x)) -> app(minus(), app(D(), x)),
                                        app(D(), app(ln(), x)) -> app(app(div(), app(D(), x)), x),
                                                 app(D(), t()) -> 1(),
                                          app(D(), constant()) -> 0()}
             POLY:
              Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
              Interpretation:
               [app](x0, x1) = x0 + x1,
               
               [1] = 1,
               
               [D] = 1,
               
               [t] = 1,
               
               [0] = 0,
               
               [constant] = 1,
               
               [+] = 0,
               
               [*] = 1,
               
               [-] = 1,
               
               [minus] = 0,
               
               [div] = 0,
               
               [pow] = 0,
               
               [2] = 0,
               
               [ln] = 0,
               
               [nil] = 0,
               
               [map] = 0,
               
               [cons] = 0,
               
               [filter] = 0,
               
               [filter2] = 0,
               
               [true] = 0,
               
               [false] = 0,
               
               [app#](x0, x1) = x0 + x1
              Strict:
               app#(D(), app(app(-(), x), y)) -> app#(D(), y)
               2 + 1x + 1y >= 1 + 1y
               app#(D(), app(app(-(), x), y)) -> app#(D(), x)
               2 + 1x + 1y >= 1 + 1x
               app#(D(), app(app(*(), x), y)) -> app#(D(), y)
               2 + 1x + 1y >= 1 + 1y
               app#(D(), app(app(*(), x), y)) -> app#(D(), x)
               2 + 1x + 1y >= 1 + 1x
               app#(D(), app(app(+(), x), y)) -> app#(D(), y)
               1 + 1x + 1y >= 1 + 1y
               app#(D(), app(app(+(), x), y)) -> app#(D(), x)
               1 + 1x + 1y >= 1 + 1x
              Weak:
               app(D(), constant()) -> 0()
               2 >= 0
               app(D(), t()) -> 1()
               2 >= 1
               app(D(), app(ln(), x)) -> app(app(div(), app(D(), x)), x)
               1 + 1x >= 1 + 2x
               app(D(), app(minus(), x)) -> app(minus(), app(D(), x))
               1 + 1x >= 1 + 1x
               app(D(), app(app(pow(), x), y)) -> app(app(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))), app(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y)))
               1 + 1x + 1y >= 8 + 4x + 4y
               app(D(), app(app(div(), x), y)) -> app(app(-(), app(app(div(), app(D(), x)), y)), app(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2())))
               1 + 1x + 1y >= 4 + 2x + 3y
               app(D(), app(app(-(), x), y)) -> app(app(-(), app(D(), x)), app(D(), y))
               2 + 1x + 1y >= 3 + 1x + 1y
               app(D(), app(app(*(), x), y)) -> app(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y)))
               2 + 1x + 1y >= 4 + 2x + 2y
               app(D(), app(app(+(), x), y)) -> app(app(+(), app(D(), x)), app(D(), y))
               1 + 1x + 1y >= 2 + 1x + 1y
               app(app(filter(), f), nil()) -> nil()
               0 + 1f >= 0
               app(app(filter(), f), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(f, x)), f), x), xs)
               0 + 1x + 1f + 1xs >= 0 + 2x + 2f + 1xs
               app(app(map(), f), nil()) -> nil()
               0 + 1f >= 0
               app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs))
               0 + 1x + 1f + 1xs >= 0 + 1x + 2f + 1xs
               app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs)
               0 + 1x + 1f + 1xs >= 0 + 1f + 1xs
               app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs))
               0 + 1x + 1f + 1xs >= 0 + 1x + 1f + 1xs
             SCCS (1):
              Scc:
               {app#(D(), app(app(+(), x), y)) -> app#(D(), x),
                app#(D(), app(app(+(), x), y)) -> app#(D(), y)}
              
              SCC (2):
               Strict:
                {app#(D(), app(app(+(), x), y)) -> app#(D(), x),
                 app#(D(), app(app(+(), x), y)) -> app#(D(), 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(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(D(), app(app(+(), x), y)) -> app(app(+(), app(D(), x)), app(D(), y)),
                                   app(D(), app(app(*(), x), y)) -> app(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y))),
                                   app(D(), app(app(-(), x), y)) -> app(app(-(), app(D(), x)), app(D(), y)),
                                 app(D(), app(app(div(), x), y)) -> app(app(-(), app(app(div(), app(D(), x)), y)), app(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2()))),
                                 app(D(), app(app(pow(), x), y)) -> app(app(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))), app(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y))),
                                       app(D(), app(minus(), x)) -> app(minus(), app(D(), x)),
                                          app(D(), app(ln(), x)) -> app(app(div(), app(D(), x)), x),
                                                   app(D(), t()) -> 1(),
                                            app(D(), constant()) -> 0()}
               POLY:
                Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
                Interpretation:
                 [app](x0, x1) = x0 + x1,
                 
                 [1] = 1,
                 
                 [D] = 1,
                 
                 [t] = 1,
                 
                 [0] = 0,
                 
                 [constant] = 1,
                 
                 [+] = 1,
                 
                 [*] = 0,
                 
                 [-] = 0,
                 
                 [minus] = 0,
                 
                 [div] = 1,
                 
                 [pow] = 1,
                 
                 [2] = 1,
                 
                 [ln] = 0,
                 
                 [nil] = 1,
                 
                 [map] = 0,
                 
                 [cons] = 0,
                 
                 [filter] = 1,
                 
                 [filter2] = 0,
                 
                 [true] = 0,
                 
                 [false] = 0,
                 
                 [app#](x0, x1) = x0 + x1
                Strict:
                 app#(D(), app(app(+(), x), y)) -> app#(D(), y)
                 2 + 1x + 1y >= 1 + 1y
                 app#(D(), app(app(+(), x), y)) -> app#(D(), x)
                 2 + 1x + 1y >= 1 + 1x
                Weak:
                 app(D(), constant()) -> 0()
                 2 >= 0
                 app(D(), t()) -> 1()
                 2 >= 1
                 app(D(), app(ln(), x)) -> app(app(div(), app(D(), x)), x)
                 1 + 1x >= 2 + 2x
                 app(D(), app(minus(), x)) -> app(minus(), app(D(), x))
                 1 + 1x >= 1 + 1x
                 app(D(), app(app(pow(), x), y)) -> app(app(+(), app(app(*(), app(app(*(), y), app(app(pow(), x), app(app(-(), y), 1())))), app(D(), x))), app(app(*(), app(app(*(), app(app(pow(), x), y)), app(ln(), x))), app(D(), y)))
                 2 + 1x + 1y >= 6 + 4x + 4y
                 app(D(), app(app(div(), x), y)) -> app(app(-(), app(app(div(), app(D(), x)), y)), app(app(div(), app(app(*(), x), app(D(), y))), app(app(pow(), y), 2())))
                 2 + 1x + 1y >= 6 + 2x + 3y
                 app(D(), app(app(-(), x), y)) -> app(app(-(), app(D(), x)), app(D(), y))
                 1 + 1x + 1y >= 2 + 1x + 1y
                 app(D(), app(app(*(), x), y)) -> app(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y)))
                 1 + 1x + 1y >= 3 + 2x + 2y
                 app(D(), app(app(+(), x), y)) -> app(app(+(), app(D(), x)), app(D(), y))
                 2 + 1x + 1y >= 3 + 1x + 1y
                 app(app(filter(), f), nil()) -> nil()
                 2 + 1f >= 1
                 app(app(filter(), f), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(f, x)), f), x), xs)
                 1 + 1x + 1f + 1xs >= 0 + 2x + 2f + 1xs
                 app(app(map(), f), nil()) -> nil()
                 1 + 1f >= 1
                 app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs))
                 0 + 1x + 1f + 1xs >= 0 + 1x + 2f + 1xs
                 app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs)
                 0 + 1x + 1f + 1xs >= 1 + 1f + 1xs
                 app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs))
                 0 + 1x + 1f + 1xs >= 1 + 1x + 1f + 1xs
               Qed