MAYBE
Time: 0.019570
TRS:
 {app(app(append(), app(app(append(), l1), l2)), l3) -> app(app(append(), l1), app(app(append(), l2), l3)),
       app(app(append(), app(app(cons(), h), t)), l) -> app(app(cons(), h), app(app(append(), t), l)),
                        app(app(append(), nil()), l) -> l,
      app(app(map(), f), app(app(append(), l1), l2)) -> app(app(append(), app(app(map(), f), l1)), app(app(map(), f), l2)),
          app(app(map(), f), app(app(cons(), h), t)) -> app(app(cons(), app(f, h)), app(app(map(), f), t)),
                           app(app(map(), f), nil()) -> nil()}
 DP:
  DP:
   {app#(app(append(), app(app(append(), l1), l2)), l3) -> app#(app(append(), l1), app(app(append(), l2), l3)),
    app#(app(append(), app(app(append(), l1), l2)), l3) -> app#(app(append(), l2), l3),
    app#(app(append(), app(app(append(), l1), l2)), l3) -> app#(append(), l2),
         app#(app(append(), app(app(cons(), h), t)), l) -> app#(app(append(), t), l),
         app#(app(append(), app(app(cons(), h), t)), l) -> app#(app(cons(), h), app(app(append(), t), l)),
         app#(app(append(), app(app(cons(), h), t)), l) -> app#(append(), t),
        app#(app(map(), f), app(app(append(), l1), l2)) -> app#(app(append(), app(app(map(), f), l1)), app(app(map(), f), l2)),
        app#(app(map(), f), app(app(append(), l1), l2)) -> app#(app(map(), f), l1),
        app#(app(map(), f), app(app(append(), l1), l2)) -> app#(app(map(), f), l2),
        app#(app(map(), f), app(app(append(), l1), l2)) -> app#(append(), app(app(map(), f), l1)),
            app#(app(map(), f), app(app(cons(), h), t)) -> app#(f, h),
            app#(app(map(), f), app(app(cons(), h), t)) -> app#(app(cons(), app(f, h)), app(app(map(), f), t)),
            app#(app(map(), f), app(app(cons(), h), t)) -> app#(app(map(), f), t),
            app#(app(map(), f), app(app(cons(), h), t)) -> app#(cons(), app(f, h))}
  TRS:
  {app(app(append(), app(app(append(), l1), l2)), l3) -> app(app(append(), l1), app(app(append(), l2), l3)),
        app(app(append(), app(app(cons(), h), t)), l) -> app(app(cons(), h), app(app(append(), t), l)),
                         app(app(append(), nil()), l) -> l,
       app(app(map(), f), app(app(append(), l1), l2)) -> app(app(append(), app(app(map(), f), l1)), app(app(map(), f), l2)),
           app(app(map(), f), app(app(cons(), h), t)) -> app(app(cons(), app(f, h)), app(app(map(), f), t)),
                            app(app(map(), f), nil()) -> nil()}
  EDG:
   {
    (app#(app(map(), f), app(app(cons(), h), t)) -> app#(f, h), app#(app(map(), f), app(app(cons(), h), t)) -> app#(cons(), app(f, h)))
    (app#(app(map(), f), app(app(cons(), h), t)) -> app#(f, h), app#(app(map(), f), app(app(cons(), h), t)) -> app#(app(map(), f), t))
    (app#(app(map(), f), app(app(cons(), h), t)) -> app#(f, h), app#(app(map(), f), app(app(cons(), h), t)) -> app#(app(cons(), app(f, h)), app(app(map(), f), t)))
    (app#(app(map(), f), app(app(cons(), h), t)) -> app#(f, h), app#(app(map(), f), app(app(cons(), h), t)) -> app#(f, h))
    (app#(app(map(), f), app(app(cons(), h), t)) -> app#(f, h), app#(app(map(), f), app(app(append(), l1), l2)) -> app#(append(), app(app(map(), f), l1)))
    (app#(app(map(), f), app(app(cons(), h), t)) -> app#(f, h), app#(app(map(), f), app(app(append(), l1), l2)) -> app#(app(map(), f), l2))
    (app#(app(map(), f), app(app(cons(), h), t)) -> app#(f, h), app#(app(map(), f), app(app(append(), l1), l2)) -> app#(app(map(), f), l1))
    (app#(app(map(), f), app(app(cons(), h), t)) -> app#(f, h), app#(app(map(), f), app(app(append(), l1), l2)) -> app#(app(append(), app(app(map(), f), l1)), app(app(map(), f), l2)))
    (app#(app(map(), f), app(app(cons(), h), t)) -> app#(f, h), app#(app(append(), app(app(cons(), h), t)), l) -> app#(append(), t))
    (app#(app(map(), f), app(app(cons(), h), t)) -> app#(f, h), app#(app(append(), app(app(cons(), h), t)), l) -> app#(app(cons(), h), app(app(append(), t), l)))
    (app#(app(map(), f), app(app(cons(), h), t)) -> app#(f, h), app#(app(append(), app(app(cons(), h), t)), l) -> app#(app(append(), t), l))
    (app#(app(map(), f), app(app(cons(), h), t)) -> app#(f, h), app#(app(append(), app(app(append(), l1), l2)), l3) -> app#(append(), l2))
    (app#(app(map(), f), app(app(cons(), h), t)) -> app#(f, h), app#(app(append(), app(app(append(), l1), l2)), l3) -> app#(app(append(), l2), l3))
    (app#(app(map(), f), app(app(cons(), h), t)) -> app#(f, h), app#(app(append(), app(app(append(), l1), l2)), l3) -> app#(app(append(), l1), app(app(append(), l2), l3)))
    (app#(app(map(), f), app(app(append(), l1), l2)) -> app#(app(map(), f), l2), app#(app(map(), f), app(app(cons(), h), t)) -> app#(cons(), app(f, h)))
    (app#(app(map(), f), app(app(append(), l1), l2)) -> app#(app(map(), f), l2), app#(app(map(), f), app(app(cons(), h), t)) -> app#(app(map(), f), t))
    (app#(app(map(), f), app(app(append(), l1), l2)) -> app#(app(map(), f), l2), app#(app(map(), f), app(app(cons(), h), t)) -> app#(app(cons(), app(f, h)), app(app(map(), f), t)))
    (app#(app(map(), f), app(app(append(), l1), l2)) -> app#(app(map(), f), l2), app#(app(map(), f), app(app(cons(), h), t)) -> app#(f, h))
    (app#(app(map(), f), app(app(append(), l1), l2)) -> app#(app(map(), f), l2), app#(app(map(), f), app(app(append(), l1), l2)) -> app#(append(), app(app(map(), f), l1)))
    (app#(app(map(), f), app(app(append(), l1), l2)) -> app#(app(map(), f), l2), app#(app(map(), f), app(app(append(), l1), l2)) -> app#(app(map(), f), l2))
    (app#(app(map(), f), app(app(append(), l1), l2)) -> app#(app(map(), f), l2), app#(app(map(), f), app(app(append(), l1), l2)) -> app#(app(map(), f), l1))
    (app#(app(map(), f), app(app(append(), l1), l2)) -> app#(app(map(), f), l2), app#(app(map(), f), app(app(append(), l1), l2)) -> app#(app(append(), app(app(map(), f), l1)), app(app(map(), f), l2)))
    (app#(app(map(), f), app(app(append(), l1), l2)) -> app#(app(map(), f), l1), app#(app(map(), f), app(app(append(), l1), l2)) -> app#(app(append(), app(app(map(), f), l1)), app(app(map(), f), l2)))
    (app#(app(map(), f), app(app(append(), l1), l2)) -> app#(app(map(), f), l1), app#(app(map(), f), app(app(append(), l1), l2)) -> app#(app(map(), f), l1))
    (app#(app(map(), f), app(app(append(), l1), l2)) -> app#(app(map(), f), l1), app#(app(map(), f), app(app(append(), l1), l2)) -> app#(app(map(), f), l2))
    (app#(app(map(), f), app(app(append(), l1), l2)) -> app#(app(map(), f), l1), app#(app(map(), f), app(app(append(), l1), l2)) -> app#(append(), app(app(map(), f), l1)))
    (app#(app(map(), f), app(app(append(), l1), l2)) -> app#(app(map(), f), l1), app#(app(map(), f), app(app(cons(), h), t)) -> app#(f, h))
    (app#(app(map(), f), app(app(append(), l1), l2)) -> app#(app(map(), f), l1), app#(app(map(), f), app(app(cons(), h), t)) -> app#(app(cons(), app(f, h)), app(app(map(), f), t)))
    (app#(app(map(), f), app(app(append(), l1), l2)) -> app#(app(map(), f), l1), app#(app(map(), f), app(app(cons(), h), t)) -> app#(app(map(), f), t))
    (app#(app(map(), f), app(app(append(), l1), l2)) -> app#(app(map(), f), l1), app#(app(map(), f), app(app(cons(), h), t)) -> app#(cons(), app(f, h)))
    (app#(app(map(), f), app(app(cons(), h), t)) -> app#(app(map(), f), t), app#(app(map(), f), app(app(append(), l1), l2)) -> app#(app(append(), app(app(map(), f), l1)), app(app(map(), f), l2)))
    (app#(app(map(), f), app(app(cons(), h), t)) -> app#(app(map(), f), t), app#(app(map(), f), app(app(append(), l1), l2)) -> app#(app(map(), f), l1))
    (app#(app(map(), f), app(app(cons(), h), t)) -> app#(app(map(), f), t), app#(app(map(), f), app(app(append(), l1), l2)) -> app#(app(map(), f), l2))
    (app#(app(map(), f), app(app(cons(), h), t)) -> app#(app(map(), f), t), app#(app(map(), f), app(app(append(), l1), l2)) -> app#(append(), app(app(map(), f), l1)))
    (app#(app(map(), f), app(app(cons(), h), t)) -> app#(app(map(), f), t), app#(app(map(), f), app(app(cons(), h), t)) -> app#(f, h))
    (app#(app(map(), f), app(app(cons(), h), t)) -> app#(app(map(), f), t), app#(app(map(), f), app(app(cons(), h), t)) -> app#(app(cons(), app(f, h)), app(app(map(), f), t)))
    (app#(app(map(), f), app(app(cons(), h), t)) -> app#(app(map(), f), t), app#(app(map(), f), app(app(cons(), h), t)) -> app#(app(map(), f), t))
    (app#(app(map(), f), app(app(cons(), h), t)) -> app#(app(map(), f), t), app#(app(map(), f), app(app(cons(), h), t)) -> app#(cons(), app(f, h)))
    (app#(app(append(), app(app(cons(), h), t)), l) -> app#(app(append(), t), l), app#(app(append(), app(app(append(), l1), l2)), l3) -> app#(app(append(), l1), app(app(append(), l2), l3)))
    (app#(app(append(), app(app(cons(), h), t)), l) -> app#(app(append(), t), l), app#(app(append(), app(app(append(), l1), l2)), l3) -> app#(app(append(), l2), l3))
    (app#(app(append(), app(app(cons(), h), t)), l) -> app#(app(append(), t), l), app#(app(append(), app(app(append(), l1), l2)), l3) -> app#(append(), l2))
    (app#(app(append(), app(app(cons(), h), t)), l) -> app#(app(append(), t), l), app#(app(append(), app(app(cons(), h), t)), l) -> app#(app(append(), t), l))
    (app#(app(append(), app(app(cons(), h), t)), l) -> app#(app(append(), t), l), app#(app(append(), app(app(cons(), h), t)), l) -> app#(app(cons(), h), app(app(append(), t), l)))
    (app#(app(append(), app(app(cons(), h), t)), l) -> app#(app(append(), t), l), app#(app(append(), app(app(cons(), h), t)), l) -> app#(append(), t))
    (app#(app(append(), app(app(append(), l1), l2)), l3) -> app#(app(append(), l2), l3), app#(app(append(), app(app(append(), l1), l2)), l3) -> app#(app(append(), l1), app(app(append(), l2), l3)))
    (app#(app(append(), app(app(append(), l1), l2)), l3) -> app#(app(append(), l2), l3), app#(app(append(), app(app(append(), l1), l2)), l3) -> app#(app(append(), l2), l3))
    (app#(app(append(), app(app(append(), l1), l2)), l3) -> app#(app(append(), l2), l3), app#(app(append(), app(app(append(), l1), l2)), l3) -> app#(append(), l2))
    (app#(app(append(), app(app(append(), l1), l2)), l3) -> app#(app(append(), l2), l3), app#(app(append(), app(app(cons(), h), t)), l) -> app#(app(append(), t), l))
    (app#(app(append(), app(app(append(), l1), l2)), l3) -> app#(app(append(), l2), l3), app#(app(append(), app(app(cons(), h), t)), l) -> app#(app(cons(), h), app(app(append(), t), l)))
    (app#(app(append(), app(app(append(), l1), l2)), l3) -> app#(app(append(), l2), l3), app#(app(append(), app(app(cons(), h), t)), l) -> app#(append(), t))
    (app#(app(map(), f), app(app(append(), l1), l2)) -> app#(app(append(), app(app(map(), f), l1)), app(app(map(), f), l2)), app#(app(append(), app(app(append(), l1), l2)), l3) -> app#(app(append(), l1), app(app(append(), l2), l3)))
    (app#(app(map(), f), app(app(append(), l1), l2)) -> app#(app(append(), app(app(map(), f), l1)), app(app(map(), f), l2)), app#(app(append(), app(app(append(), l1), l2)), l3) -> app#(app(append(), l2), l3))
    (app#(app(map(), f), app(app(append(), l1), l2)) -> app#(app(append(), app(app(map(), f), l1)), app(app(map(), f), l2)), app#(app(append(), app(app(append(), l1), l2)), l3) -> app#(append(), l2))
    (app#(app(map(), f), app(app(append(), l1), l2)) -> app#(app(append(), app(app(map(), f), l1)), app(app(map(), f), l2)), app#(app(append(), app(app(cons(), h), t)), l) -> app#(app(append(), t), l))
    (app#(app(map(), f), app(app(append(), l1), l2)) -> app#(app(append(), app(app(map(), f), l1)), app(app(map(), f), l2)), app#(app(append(), app(app(cons(), h), t)), l) -> app#(app(cons(), h), app(app(append(), t), l)))
    (app#(app(map(), f), app(app(append(), l1), l2)) -> app#(app(append(), app(app(map(), f), l1)), app(app(map(), f), l2)), app#(app(append(), app(app(cons(), h), t)), l) -> app#(append(), t))
    (app#(app(append(), app(app(append(), l1), l2)), l3) -> app#(app(append(), l1), app(app(append(), l2), l3)), app#(app(append(), app(app(append(), l1), l2)), l3) -> app#(app(append(), l1), app(app(append(), l2), l3)))
    (app#(app(append(), app(app(append(), l1), l2)), l3) -> app#(app(append(), l1), app(app(append(), l2), l3)), app#(app(append(), app(app(append(), l1), l2)), l3) -> app#(app(append(), l2), l3))
    (app#(app(append(), app(app(append(), l1), l2)), l3) -> app#(app(append(), l1), app(app(append(), l2), l3)), app#(app(append(), app(app(append(), l1), l2)), l3) -> app#(append(), l2))
    (app#(app(append(), app(app(append(), l1), l2)), l3) -> app#(app(append(), l1), app(app(append(), l2), l3)), app#(app(append(), app(app(cons(), h), t)), l) -> app#(app(append(), t), l))
    (app#(app(append(), app(app(append(), l1), l2)), l3) -> app#(app(append(), l1), app(app(append(), l2), l3)), app#(app(append(), app(app(cons(), h), t)), l) -> app#(app(cons(), h), app(app(append(), t), l)))
    (app#(app(append(), app(app(append(), l1), l2)), l3) -> app#(app(append(), l1), app(app(append(), l2), l3)), app#(app(append(), app(app(cons(), h), t)), l) -> app#(append(), t))
   }
   STATUS:
    arrows: 0.683673
    SCCS (2):
     Scc:
      {app#(app(map(), f), app(app(append(), l1), l2)) -> app#(app(map(), f), l1),
       app#(app(map(), f), app(app(append(), l1), l2)) -> app#(app(map(), f), l2),
           app#(app(map(), f), app(app(cons(), h), t)) -> app#(f, h),
           app#(app(map(), f), app(app(cons(), h), t)) -> app#(app(map(), f), t)}
     Scc:
      {app#(app(append(), app(app(append(), l1), l2)), l3) -> app#(app(append(), l1), app(app(append(), l2), l3)),
       app#(app(append(), app(app(append(), l1), l2)), l3) -> app#(app(append(), l2), l3),
            app#(app(append(), app(app(cons(), h), t)), l) -> app#(app(append(), t), l)}
     
     SCC (4):
      Strict:
       {app#(app(map(), f), app(app(append(), l1), l2)) -> app#(app(map(), f), l1),
        app#(app(map(), f), app(app(append(), l1), l2)) -> app#(app(map(), f), l2),
            app#(app(map(), f), app(app(cons(), h), t)) -> app#(f, h),
            app#(app(map(), f), app(app(cons(), h), t)) -> app#(app(map(), f), t)}
      Weak:
      {app(app(append(), app(app(append(), l1), l2)), l3) -> app(app(append(), l1), app(app(append(), l2), l3)),
            app(app(append(), app(app(cons(), h), t)), l) -> app(app(cons(), h), app(app(append(), t), l)),
                             app(app(append(), nil()), l) -> l,
           app(app(map(), f), app(app(append(), l1), l2)) -> app(app(append(), app(app(map(), f), l1)), app(app(map(), f), l2)),
               app(app(map(), f), app(app(cons(), h), t)) -> app(app(cons(), app(f, h)), app(app(map(), f), t)),
                                app(app(map(), f), nil()) -> nil()}
      Open
     
     
     
     
     SCC (3):
      Strict:
       {app#(app(append(), app(app(append(), l1), l2)), l3) -> app#(app(append(), l1), app(app(append(), l2), l3)),
        app#(app(append(), app(app(append(), l1), l2)), l3) -> app#(app(append(), l2), l3),
             app#(app(append(), app(app(cons(), h), t)), l) -> app#(app(append(), t), l)}
      Weak:
      {app(app(append(), app(app(append(), l1), l2)), l3) -> app(app(append(), l1), app(app(append(), l2), l3)),
            app(app(append(), app(app(cons(), h), t)), l) -> app(app(cons(), h), app(app(append(), t), l)),
                             app(app(append(), nil()), l) -> l,
           app(app(map(), f), app(app(append(), l1), l2)) -> app(app(append(), app(app(map(), f), l1)), app(app(map(), f), l2)),
               app(app(map(), f), app(app(cons(), h), t)) -> app(app(cons(), app(f, h)), app(app(map(), f), t)),
                                app(app(map(), f), nil()) -> nil()}
      Open