MAYBE
Time: 0.113683
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(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y)),
                     app(app(plus(), 0()), x) -> 0(),
          app(sum(), app(app(cons(), x), xs)) -> app(app(plus(), x), app(sum(), xs)),
         app(size(), app(app(node(), x), xs)) -> app(s(), app(sum(), app(app(map(), size()), 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(plus(), app(s(), x)), y) -> app#(app(plus(), x), y),
               app#(app(plus(), app(s(), x)), y) -> app#(plus(), x),
               app#(app(plus(), app(s(), x)), y) -> app#(s(), app(app(plus(), x), y)),
            app#(sum(), app(app(cons(), x), xs)) -> app#(app(plus(), x), app(sum(), xs)),
            app#(sum(), app(app(cons(), x), xs)) -> app#(plus(), x),
            app#(sum(), app(app(cons(), x), xs)) -> app#(sum(), xs),
           app#(size(), app(app(node(), x), xs)) -> app#(app(map(), size()), xs),
           app#(size(), app(app(node(), x), xs)) -> app#(map(), size()),
           app#(size(), app(app(node(), x), xs)) -> app#(sum(), app(app(map(), size()), xs)),
           app#(size(), app(app(node(), x), xs)) -> app#(s(), app(sum(), app(app(map(), size()), xs)))}
  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(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y)),
                      app(app(plus(), 0()), x) -> 0(),
           app(sum(), app(app(cons(), x), xs)) -> app(app(plus(), x), app(sum(), xs)),
          app(size(), app(app(node(), x), xs)) -> app(s(), app(sum(), app(app(map(), size()), xs)))}
  EDG:
   {(app#(sum(), app(app(cons(), x), xs)) -> app#(app(plus(), x), app(sum(), xs)), app#(app(plus(), app(s(), x)), y) -> app#(s(), app(app(plus(), x), y)))
    (app#(sum(), app(app(cons(), x), xs)) -> app#(app(plus(), x), app(sum(), xs)), app#(app(plus(), app(s(), x)), y) -> app#(plus(), x))
    (app#(sum(), app(app(cons(), x), xs)) -> app#(app(plus(), x), app(sum(), xs)), app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(size(), app(app(node(), x), xs)) -> app#(s(), app(sum(), app(app(map(), size()), xs))))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(size(), app(app(node(), x), xs)) -> app#(sum(), app(app(map(), size()), xs)))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(size(), app(app(node(), x), xs)) -> app#(map(), size()))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(size(), app(app(node(), x), xs)) -> app#(app(map(), size()), xs))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(sum(), app(app(cons(), x), xs)) -> app#(sum(), xs))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(sum(), app(app(cons(), x), xs)) -> app#(plus(), x))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(sum(), app(app(cons(), x), xs)) -> app#(app(plus(), x), app(sum(), xs)))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(plus(), app(s(), x)), y) -> app#(s(), app(app(plus(), x), y)))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(plus(), app(s(), x)), y) -> app#(plus(), x))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(cons(), app(f, x)))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(cons(), app(f, x)), app(app(map(), f), xs)))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x))
    (app#(sum(), app(app(cons(), x), xs)) -> app#(sum(), xs), app#(sum(), app(app(cons(), x), xs)) -> app#(sum(), xs))
    (app#(sum(), app(app(cons(), x), xs)) -> app#(sum(), xs), app#(sum(), app(app(cons(), x), xs)) -> app#(plus(), x))
    (app#(sum(), app(app(cons(), x), xs)) -> app#(sum(), xs), app#(sum(), app(app(cons(), x), xs)) -> app#(app(plus(), x), app(sum(), xs)))
    (app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y), app#(app(plus(), app(s(), x)), y) -> app#(s(), app(app(plus(), x), y)))
    (app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y), app#(app(plus(), app(s(), x)), y) -> app#(plus(), x))
    (app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y), app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y))
    (app#(size(), app(app(node(), x), xs)) -> app#(app(map(), size()), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x))
    (app#(size(), app(app(node(), x), xs)) -> app#(app(map(), size()), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs))
    (app#(size(), app(app(node(), x), xs)) -> app#(app(map(), size()), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(cons(), app(f, x)), app(app(map(), f), xs)))
    (app#(size(), app(app(node(), x), xs)) -> app#(app(map(), size()), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(cons(), app(f, x)))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(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#(size(), app(app(node(), x), xs)) -> app#(sum(), app(app(map(), size()), xs)), app#(sum(), app(app(cons(), x), xs)) -> app#(app(plus(), x), app(sum(), xs)))
    (app#(size(), app(app(node(), x), xs)) -> app#(sum(), app(app(map(), size()), xs)), app#(sum(), app(app(cons(), x), xs)) -> app#(plus(), x))
    (app#(size(), app(app(node(), x), xs)) -> app#(sum(), app(app(map(), size()), xs)), app#(sum(), app(app(cons(), x), xs)) -> app#(sum(), xs))}
   STATUS:
    arrows: 0.826531
    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#(size(), app(app(node(), x), xs)) -> app#(app(map(), size()), xs)}
     Scc:
      {app#(sum(), app(app(cons(), x), xs)) -> app#(sum(), xs)}
     Scc:
      {app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), 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#(size(), app(app(node(), x), xs)) -> app#(app(map(), size()), 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(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y)),
                          app(app(plus(), 0()), x) -> 0(),
               app(sum(), app(app(cons(), x), xs)) -> app(app(plus(), x), app(sum(), xs)),
              app(size(), app(app(node(), x), xs)) -> app(s(), app(sum(), app(app(map(), size()), xs)))}
      Open
     
     
     
     SCC (1):
      Strict:
       {app#(sum(), app(app(cons(), x), xs)) -> app#(sum(), 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(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y)),
                          app(app(plus(), 0()), x) -> 0(),
               app(sum(), app(app(cons(), x), xs)) -> app(app(plus(), x), app(sum(), xs)),
              app(size(), app(app(node(), x), xs)) -> app(s(), app(sum(), app(app(map(), size()), xs)))}
      Open
     
     
     SCC (1):
      Strict:
       {app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), 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(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y)),
                          app(app(plus(), 0()), x) -> 0(),
               app(sum(), app(app(cons(), x), xs)) -> app(app(plus(), x), app(sum(), xs)),
              app(size(), app(app(node(), x), xs)) -> app(s(), app(sum(), app(app(map(), size()), xs)))}
      Open