MAYBE
Time: 0.016388
TRS:
 {                      app(app(map(), f), nil()) -> nil(),
      app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)),
         app(app(le(), app(s(), x)), app(s(), y)) -> app(app(le(), x), y),
                 app(app(le(), app(s(), x)), 0()) -> false(),
                           app(app(le(), 0()), y) -> true(),
                    app(app(maxlist(), x), nil()) -> x,
  app(app(maxlist(), x), app(app(cons(), y), ys)) -> app(app(if(), app(app(le(), x), y)), app(app(maxlist(), y), ys)),
           app(height(), app(app(node(), x), xs)) -> app(s(), app(app(maxlist(), 0()), app(app(map(), height()), xs)))}
 DP:
  DP:
   {    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(le(), app(s(), x)), app(s(), y)) -> app#(app(le(), x), y),
           app#(app(le(), app(s(), x)), app(s(), y)) -> app#(le(), x),
    app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(le(), x), y),
    app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(if(), app(app(le(), x), y)), app(app(maxlist(), y), ys)),
    app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(maxlist(), y), ys),
    app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(le(), x),
    app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(if(), app(app(le(), x), y)),
    app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(maxlist(), y),
             app#(height(), app(app(node(), x), xs)) -> app#(app(map(), height()), xs),
             app#(height(), app(app(node(), x), xs)) -> app#(app(maxlist(), 0()), app(app(map(), height()), xs)),
             app#(height(), app(app(node(), x), xs)) -> app#(map(), height()),
             app#(height(), app(app(node(), x), xs)) -> app#(s(), app(app(maxlist(), 0()), app(app(map(), height()), xs))),
             app#(height(), app(app(node(), x), xs)) -> app#(maxlist(), 0())}
  TRS:
  {                      app(app(map(), f), nil()) -> nil(),
       app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)),
          app(app(le(), app(s(), x)), app(s(), y)) -> app(app(le(), x), y),
                  app(app(le(), app(s(), x)), 0()) -> false(),
                            app(app(le(), 0()), y) -> true(),
                     app(app(maxlist(), x), nil()) -> x,
   app(app(maxlist(), x), app(app(cons(), y), ys)) -> app(app(if(), app(app(le(), x), y)), app(app(maxlist(), y), ys)),
            app(height(), app(app(node(), x), xs)) -> app(s(), app(app(maxlist(), 0()), app(app(map(), height()), xs)))}
  EDG:
   {(app#(app(le(), app(s(), x)), app(s(), y)) -> app#(app(le(), x), y), app#(app(le(), app(s(), x)), app(s(), y)) -> app#(le(), x))
    (app#(app(le(), app(s(), x)), app(s(), y)) -> app#(app(le(), x), y), app#(app(le(), app(s(), x)), app(s(), y)) -> app#(app(le(), x), y))
    (app#(height(), app(app(node(), x), xs)) -> app#(app(maxlist(), 0()), app(app(map(), height()), xs)), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(maxlist(), y))
    (app#(height(), app(app(node(), x), xs)) -> app#(app(maxlist(), 0()), app(app(map(), height()), xs)), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(if(), app(app(le(), x), y)))
    (app#(height(), app(app(node(), x), xs)) -> app#(app(maxlist(), 0()), app(app(map(), height()), xs)), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(le(), x))
    (app#(height(), app(app(node(), x), xs)) -> app#(app(maxlist(), 0()), app(app(map(), height()), xs)), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(maxlist(), y), ys))
    (app#(height(), app(app(node(), x), xs)) -> app#(app(maxlist(), 0()), app(app(map(), height()), xs)), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(if(), app(app(le(), x), y)), app(app(maxlist(), y), ys)))
    (app#(height(), app(app(node(), x), xs)) -> app#(app(maxlist(), 0()), app(app(map(), height()), xs)), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(le(), x), y))
    (app#(height(), app(app(node(), x), xs)) -> app#(app(map(), height()), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(cons(), app(f, x)))
    (app#(height(), app(app(node(), x), xs)) -> app#(app(map(), height()), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(cons(), app(f, x)), app(app(map(), f), xs)))
    (app#(height(), app(app(node(), x), xs)) -> app#(app(map(), height()), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs))
    (app#(height(), app(app(node(), x), xs)) -> app#(app(map(), height()), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x))
    (app#(app(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(le(), app(s(), x)), app(s(), y)) -> app#(app(le(), x), y))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(le(), app(s(), x)), app(s(), y)) -> app#(le(), x))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(le(), x), y))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(if(), app(app(le(), x), y)), app(app(maxlist(), y), ys)))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(maxlist(), y), ys))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(le(), x))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(if(), app(app(le(), x), y)))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(maxlist(), y))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(height(), app(app(node(), x), xs)) -> app#(app(map(), height()), xs))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(height(), app(app(node(), x), xs)) -> app#(app(maxlist(), 0()), app(app(map(), height()), xs)))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(height(), app(app(node(), x), xs)) -> app#(map(), height()))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(height(), app(app(node(), x), xs)) -> app#(s(), app(app(maxlist(), 0()), app(app(map(), height()), xs))))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(height(), app(app(node(), x), xs)) -> app#(maxlist(), 0()))
    (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(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(maxlist(), y), ys), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(le(), x), y))
    (app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(maxlist(), y), ys), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(if(), app(app(le(), x), y)), app(app(maxlist(), y), ys)))
    (app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(maxlist(), y), ys), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(maxlist(), y), ys))
    (app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(maxlist(), y), ys), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(le(), x))
    (app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(maxlist(), y), ys), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(if(), app(app(le(), x), y)))
    (app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(maxlist(), y), ys), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(maxlist(), y))
    (app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(le(), x), y), app#(app(le(), app(s(), x)), app(s(), y)) -> app#(app(le(), x), y))
    (app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(le(), x), y), app#(app(le(), app(s(), x)), app(s(), y)) -> app#(le(), x))}
   EDG:
    {(app#(app(le(), app(s(), x)), app(s(), y)) -> app#(app(le(), x), y), app#(app(le(), app(s(), x)), app(s(), y)) -> app#(le(), x))
     (app#(app(le(), app(s(), x)), app(s(), y)) -> app#(app(le(), x), y), app#(app(le(), app(s(), x)), app(s(), y)) -> app#(app(le(), x), y))
     (app#(height(), app(app(node(), x), xs)) -> app#(app(maxlist(), 0()), app(app(map(), height()), xs)), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(maxlist(), y))
     (app#(height(), app(app(node(), x), xs)) -> app#(app(maxlist(), 0()), app(app(map(), height()), xs)), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(if(), app(app(le(), x), y)))
     (app#(height(), app(app(node(), x), xs)) -> app#(app(maxlist(), 0()), app(app(map(), height()), xs)), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(le(), x))
     (app#(height(), app(app(node(), x), xs)) -> app#(app(maxlist(), 0()), app(app(map(), height()), xs)), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(maxlist(), y), ys))
     (app#(height(), app(app(node(), x), xs)) -> app#(app(maxlist(), 0()), app(app(map(), height()), xs)), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(if(), app(app(le(), x), y)), app(app(maxlist(), y), ys)))
     (app#(height(), app(app(node(), x), xs)) -> app#(app(maxlist(), 0()), app(app(map(), height()), xs)), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(le(), x), y))
     (app#(height(), app(app(node(), x), xs)) -> app#(app(map(), height()), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(cons(), app(f, x)))
     (app#(height(), app(app(node(), x), xs)) -> app#(app(map(), height()), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(cons(), app(f, x)), app(app(map(), f), xs)))
     (app#(height(), app(app(node(), x), xs)) -> app#(app(map(), height()), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs))
     (app#(height(), app(app(node(), x), xs)) -> app#(app(map(), height()), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x))
     (app#(app(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(le(), app(s(), x)), app(s(), y)) -> app#(app(le(), x), y))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(le(), app(s(), x)), app(s(), y)) -> app#(le(), x))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(le(), x), y))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(if(), app(app(le(), x), y)), app(app(maxlist(), y), ys)))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(maxlist(), y), ys))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(le(), x))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(if(), app(app(le(), x), y)))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(maxlist(), y))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(height(), app(app(node(), x), xs)) -> app#(app(map(), height()), xs))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(height(), app(app(node(), x), xs)) -> app#(app(maxlist(), 0()), app(app(map(), height()), xs)))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(height(), app(app(node(), x), xs)) -> app#(map(), height()))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(height(), app(app(node(), x), xs)) -> app#(s(), app(app(maxlist(), 0()), app(app(map(), height()), xs))))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(height(), app(app(node(), x), xs)) -> app#(maxlist(), 0()))
     (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(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(maxlist(), y), ys), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(le(), x), y))
     (app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(maxlist(), y), ys), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(if(), app(app(le(), x), y)), app(app(maxlist(), y), ys)))
     (app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(maxlist(), y), ys), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(maxlist(), y), ys))
     (app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(maxlist(), y), ys), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(le(), x))
     (app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(maxlist(), y), ys), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(if(), app(app(le(), x), y)))
     (app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(maxlist(), y), ys), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(maxlist(), y))
     (app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(le(), x), y), app#(app(le(), app(s(), x)), app(s(), y)) -> app#(app(le(), x), y))
     (app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(le(), x), y), app#(app(le(), app(s(), x)), app(s(), y)) -> app#(le(), x))}
    EDG:
     {(app#(app(le(), app(s(), x)), app(s(), y)) -> app#(app(le(), x), y), app#(app(le(), app(s(), x)), app(s(), y)) -> app#(le(), x))
      (app#(app(le(), app(s(), x)), app(s(), y)) -> app#(app(le(), x), y), app#(app(le(), app(s(), x)), app(s(), y)) -> app#(app(le(), x), y))
      (app#(height(), app(app(node(), x), xs)) -> app#(app(maxlist(), 0()), app(app(map(), height()), xs)), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(maxlist(), y))
      (app#(height(), app(app(node(), x), xs)) -> app#(app(maxlist(), 0()), app(app(map(), height()), xs)), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(if(), app(app(le(), x), y)))
      (app#(height(), app(app(node(), x), xs)) -> app#(app(maxlist(), 0()), app(app(map(), height()), xs)), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(le(), x))
      (app#(height(), app(app(node(), x), xs)) -> app#(app(maxlist(), 0()), app(app(map(), height()), xs)), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(maxlist(), y), ys))
      (app#(height(), app(app(node(), x), xs)) -> app#(app(maxlist(), 0()), app(app(map(), height()), xs)), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(if(), app(app(le(), x), y)), app(app(maxlist(), y), ys)))
      (app#(height(), app(app(node(), x), xs)) -> app#(app(maxlist(), 0()), app(app(map(), height()), xs)), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(le(), x), y))
      (app#(height(), app(app(node(), x), xs)) -> app#(app(map(), height()), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(cons(), app(f, x)))
      (app#(height(), app(app(node(), x), xs)) -> app#(app(map(), height()), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(cons(), app(f, x)), app(app(map(), f), xs)))
      (app#(height(), app(app(node(), x), xs)) -> app#(app(map(), height()), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs))
      (app#(height(), app(app(node(), x), xs)) -> app#(app(map(), height()), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x))
      (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x))
      (app#(app(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(le(), app(s(), x)), app(s(), y)) -> app#(app(le(), x), y))
      (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(le(), app(s(), x)), app(s(), y)) -> app#(le(), x))
      (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(le(), x), y))
      (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(if(), app(app(le(), x), y)), app(app(maxlist(), y), ys)))
      (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(maxlist(), y), ys))
      (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(le(), x))
      (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(if(), app(app(le(), x), y)))
      (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(maxlist(), y))
      (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(height(), app(app(node(), x), xs)) -> app#(app(map(), height()), xs))
      (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(height(), app(app(node(), x), xs)) -> app#(app(maxlist(), 0()), app(app(map(), height()), xs)))
      (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(height(), app(app(node(), x), xs)) -> app#(map(), height()))
      (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(height(), app(app(node(), x), xs)) -> app#(s(), app(app(maxlist(), 0()), app(app(map(), height()), xs))))
      (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(height(), app(app(node(), x), xs)) -> app#(maxlist(), 0()))
      (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(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(maxlist(), y), ys), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(le(), x), y))
      (app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(maxlist(), y), ys), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(if(), app(app(le(), x), y)), app(app(maxlist(), y), ys)))
      (app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(maxlist(), y), ys), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(maxlist(), y), ys))
      (app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(maxlist(), y), ys), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(le(), x))
      (app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(maxlist(), y), ys), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(if(), app(app(le(), x), y)))
      (app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(maxlist(), y), ys), app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(maxlist(), y))
      (app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(le(), x), y), app#(app(le(), app(s(), x)), app(s(), y)) -> app#(app(le(), x), y))
      (app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(le(), x), y), app#(app(le(), app(s(), x)), app(s(), y)) -> app#(le(), x))}
     STATUS:
      arrows: 0.858131
      SCCS (3):
       Scc:
        {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#(height(), app(app(node(), x), xs)) -> app#(app(map(), height()), xs)}
       Scc:
        {app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(maxlist(), y), ys)}
       Scc:
        {app#(app(le(), app(s(), x)), app(s(), y)) -> app#(app(le(), x), y)}
       
       SCC (3):
        Strict:
         {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#(height(), app(app(node(), x), xs)) -> app#(app(map(), height()), xs)}
        Weak:
        {                      app(app(map(), f), nil()) -> nil(),
             app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)),
                app(app(le(), app(s(), x)), app(s(), y)) -> app(app(le(), x), y),
                        app(app(le(), app(s(), x)), 0()) -> false(),
                                  app(app(le(), 0()), y) -> true(),
                           app(app(maxlist(), x), nil()) -> x,
         app(app(maxlist(), x), app(app(cons(), y), ys)) -> app(app(if(), app(app(le(), x), y)), app(app(maxlist(), y), ys)),
                  app(height(), app(app(node(), x), xs)) -> app(s(), app(app(maxlist(), 0()), app(app(map(), height()), xs)))}
        Open
       
       
       
       SCC (1):
        Strict:
         {app#(app(maxlist(), x), app(app(cons(), y), ys)) -> app#(app(maxlist(), y), ys)}
        Weak:
        {                      app(app(map(), f), nil()) -> nil(),
             app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)),
                app(app(le(), app(s(), x)), app(s(), y)) -> app(app(le(), x), y),
                        app(app(le(), app(s(), x)), 0()) -> false(),
                                  app(app(le(), 0()), y) -> true(),
                           app(app(maxlist(), x), nil()) -> x,
         app(app(maxlist(), x), app(app(cons(), y), ys)) -> app(app(if(), app(app(le(), x), y)), app(app(maxlist(), y), ys)),
                  app(height(), app(app(node(), x), xs)) -> app(s(), app(app(maxlist(), 0()), app(app(map(), height()), xs)))}
        Open
       
       
       
       
       
       
       
       SCC (1):
        Strict:
         {app#(app(le(), app(s(), x)), app(s(), y)) -> app#(app(le(), x), y)}
        Weak:
        {                      app(app(map(), f), nil()) -> nil(),
             app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)),
                app(app(le(), app(s(), x)), app(s(), y)) -> app(app(le(), x), y),
                        app(app(le(), app(s(), x)), 0()) -> false(),
                                  app(app(le(), 0()), y) -> true(),
                           app(app(maxlist(), x), nil()) -> x,
         app(app(maxlist(), x), app(app(cons(), y), ys)) -> app(app(if(), app(app(le(), x), y)), app(app(maxlist(), y), ys)),
                  app(height(), app(app(node(), x), xs)) -> app(s(), app(app(maxlist(), 0()), app(app(map(), height()), xs)))}
        Open