MAYBE
Time: 0.106259
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(append(), nil()), xs) -> xs,
  app(app(append(), app(app(cons(), x), xs)), ys) -> app(app(cons(), x), app(app(append(), xs), ys)),
                             app(concat(), nil()) -> nil(),
           app(concat(), app(app(cons(), x), xs)) -> app(app(append(), x), app(concat(), xs)),
          app(flatten(), app(app(node(), x), xs)) -> app(app(cons(), x), app(concat(), app(app(map(), flatten()), 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(append(), app(app(cons(), x), xs)), ys) -> app#(app(cons(), x), app(app(append(), xs), ys)),
    app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(app(append(), xs), ys),
    app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(append(), xs),
             app#(concat(), app(app(cons(), x), xs)) -> app#(app(append(), x), app(concat(), xs)),
             app#(concat(), app(app(cons(), x), xs)) -> app#(concat(), xs),
             app#(concat(), app(app(cons(), x), xs)) -> app#(append(), x),
            app#(flatten(), app(app(node(), x), xs)) -> app#(app(map(), flatten()), xs),
            app#(flatten(), app(app(node(), x), xs)) -> app#(app(cons(), x), app(concat(), app(app(map(), flatten()), xs))),
            app#(flatten(), app(app(node(), x), xs)) -> app#(map(), flatten()),
            app#(flatten(), app(app(node(), x), xs)) -> app#(cons(), x),
            app#(flatten(), app(app(node(), x), xs)) -> app#(concat(), app(app(map(), flatten()), 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(append(), nil()), xs) -> xs,
   app(app(append(), app(app(cons(), x), xs)), ys) -> app(app(cons(), x), app(app(append(), xs), ys)),
                              app(concat(), nil()) -> nil(),
            app(concat(), app(app(cons(), x), xs)) -> app(app(append(), x), app(concat(), xs)),
           app(flatten(), app(app(node(), x), xs)) -> app(app(cons(), x), app(concat(), app(app(map(), flatten()), xs)))}
  UR:
   {                      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(append(), nil()), xs) -> xs,
    app(app(append(), app(app(cons(), x), xs)), ys) -> app(app(cons(), x), app(app(append(), xs), ys)),
                               app(concat(), nil()) -> nil(),
             app(concat(), app(app(cons(), x), xs)) -> app(app(append(), x), app(concat(), xs)),
            app(flatten(), app(app(node(), x), xs)) -> app(app(cons(), x), app(concat(), app(app(map(), flatten()), xs))),
                                            a(y, z) -> y,
                                            a(y, z) -> z}
   EDG:
    {(app#(flatten(), app(app(node(), x), xs)) -> app#(app(map(), flatten()), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(cons(), app(f, x)))
     (app#(flatten(), app(app(node(), x), xs)) -> app#(app(map(), flatten()), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(cons(), app(f, x)), app(app(map(), f), xs)))
     (app#(flatten(), app(app(node(), x), xs)) -> app#(app(map(), flatten()), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs))
     (app#(flatten(), app(app(node(), x), xs)) -> app#(app(map(), flatten()), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x))
     (app#(concat(), app(app(cons(), x), xs)) -> app#(app(append(), x), app(concat(), xs)), app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(append(), xs))
     (app#(concat(), app(app(cons(), x), xs)) -> app#(app(append(), x), app(concat(), xs)), app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(app(append(), xs), ys))
     (app#(concat(), app(app(cons(), x), xs)) -> app#(app(append(), x), app(concat(), xs)), app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(app(cons(), x), app(app(append(), xs), ys)))
     (app#(concat(), app(app(cons(), x), xs)) -> app#(concat(), xs), app#(concat(), app(app(cons(), x), xs)) -> app#(append(), x))
     (app#(concat(), app(app(cons(), x), xs)) -> app#(concat(), xs), app#(concat(), app(app(cons(), x), xs)) -> app#(concat(), xs))
     (app#(concat(), app(app(cons(), x), xs)) -> app#(concat(), xs), app#(concat(), app(app(cons(), x), xs)) -> app#(app(append(), x), app(concat(), xs)))
     (app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(app(append(), xs), ys), app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(app(cons(), x), app(app(append(), xs), ys)))
     (app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(app(append(), xs), ys), app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(app(append(), xs), ys))
     (app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(app(append(), xs), ys), app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(append(), 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#(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(append(), app(app(cons(), x), xs)), ys) -> app#(app(cons(), x), app(app(append(), xs), ys)))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(app(append(), xs), ys))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(append(), xs))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(concat(), app(app(cons(), x), xs)) -> app#(app(append(), x), app(concat(), xs)))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(concat(), app(app(cons(), x), xs)) -> app#(concat(), xs))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(concat(), app(app(cons(), x), xs)) -> app#(append(), x))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(flatten(), app(app(node(), x), xs)) -> app#(app(map(), flatten()), xs))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(flatten(), app(app(node(), x), xs)) -> app#(app(cons(), x), app(concat(), app(app(map(), flatten()), xs))))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(flatten(), app(app(node(), x), xs)) -> app#(map(), flatten()))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(flatten(), app(app(node(), x), xs)) -> app#(cons(), x))
     (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(flatten(), app(app(node(), x), xs)) -> app#(concat(), app(app(map(), flatten()), xs)))
     (app#(flatten(), app(app(node(), x), xs)) -> app#(concat(), app(app(map(), flatten()), xs)), app#(concat(), app(app(cons(), x), xs)) -> app#(app(append(), x), app(concat(), xs)))
     (app#(flatten(), app(app(node(), x), xs)) -> app#(concat(), app(app(map(), flatten()), xs)), app#(concat(), app(app(cons(), x), xs)) -> app#(concat(), xs))
     (app#(flatten(), app(app(node(), x), xs)) -> app#(concat(), app(app(map(), flatten()), xs)), app#(concat(), app(app(cons(), x), xs)) -> app#(append(), 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)))}
    STATUS:
     arrows: 0.844444
     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#(flatten(), app(app(node(), x), xs)) -> app#(app(map(), flatten()), xs)}
      Scc:
       {app#(concat(), app(app(cons(), x), xs)) -> app#(concat(), xs)}
      Scc:
       {app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(app(append(), xs), ys)}
      
      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#(flatten(), app(app(node(), x), xs)) -> app#(app(map(), flatten()), 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(append(), nil()), xs) -> xs,
        app(app(append(), app(app(cons(), x), xs)), ys) -> app(app(cons(), x), app(app(append(), xs), ys)),
                                   app(concat(), nil()) -> nil(),
                 app(concat(), app(app(cons(), x), xs)) -> app(app(append(), x), app(concat(), xs)),
                app(flatten(), app(app(node(), x), xs)) -> app(app(cons(), x), app(concat(), app(app(map(), flatten()), xs)))}
       Open
      
      
      
      
      SCC (1):
       Strict:
        {app#(concat(), app(app(cons(), x), xs)) -> app#(concat(), 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(append(), nil()), xs) -> xs,
        app(app(append(), app(app(cons(), x), xs)), ys) -> app(app(cons(), x), app(app(append(), xs), ys)),
                                   app(concat(), nil()) -> nil(),
                 app(concat(), app(app(cons(), x), xs)) -> app(app(append(), x), app(concat(), xs)),
                app(flatten(), app(app(node(), x), xs)) -> app(app(cons(), x), app(concat(), app(app(map(), flatten()), xs)))}
       Open
      
      
      SCC (1):
       Strict:
        {app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(app(append(), xs), 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(append(), nil()), xs) -> xs,
        app(app(append(), app(app(cons(), x), xs)), ys) -> app(app(cons(), x), app(app(append(), xs), ys)),
                                   app(concat(), nil()) -> nil(),
                 app(concat(), app(app(cons(), x), xs)) -> app(app(append(), x), app(concat(), xs)),
                app(flatten(), app(app(node(), x), xs)) -> app(app(cons(), x), app(concat(), app(app(map(), flatten()), xs)))}
       Open