MAYBE
Time: 0.013794
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(minus(), x), 0()) -> x,
  app(app(minus(), app(s(), x)), app(s(), y)) -> app(app(minus(), app(p(), app(s(), x))), app(p(), app(s(), y))),
    app(app(div(), app(s(), x)), app(s(), y)) -> app(s(), app(app(div(), app(app(minus(), x), y)), app(s(), y))),
            app(app(div(), 0()), app(s(), y)) -> 0(),
                        app(p(), app(s(), x)) -> x}
 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(minus(), app(s(), x)), app(s(), y)) -> app#(app(minus(), app(p(), app(s(), x))), app(p(), app(s(), y))),
    app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(minus(), app(p(), app(s(), x))),
    app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(p(), app(s(), x)),
    app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(p(), app(s(), y)),
      app#(app(div(), app(s(), x)), app(s(), y)) -> app#(app(minus(), x), y),
      app#(app(div(), app(s(), x)), app(s(), y)) -> app#(app(div(), app(app(minus(), x), y)), app(s(), y)),
      app#(app(div(), app(s(), x)), app(s(), y)) -> app#(minus(), x),
      app#(app(div(), app(s(), x)), app(s(), y)) -> app#(s(), app(app(div(), app(app(minus(), x), y)), app(s(), y))),
      app#(app(div(), app(s(), x)), app(s(), y)) -> app#(div(), app(app(minus(), x), y))}
  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(minus(), x), 0()) -> x,
   app(app(minus(), app(s(), x)), app(s(), y)) -> app(app(minus(), app(p(), app(s(), x))), app(p(), app(s(), y))),
     app(app(div(), app(s(), x)), app(s(), y)) -> app(s(), app(app(div(), app(app(minus(), x), y)), app(s(), y))),
             app(app(div(), 0()), app(s(), y)) -> 0(),
                         app(p(), app(s(), x)) -> x}
  EDG:
   {(app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(app(minus(), app(p(), app(s(), x))), app(p(), app(s(), y))), app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(p(), app(s(), y)))
    (app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(app(minus(), app(p(), app(s(), x))), app(p(), app(s(), y))), app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(p(), app(s(), x)))
    (app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(app(minus(), app(p(), app(s(), x))), app(p(), app(s(), y))), app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(minus(), app(p(), app(s(), x))))
    (app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(app(minus(), app(p(), app(s(), x))), app(p(), app(s(), y))), app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(app(minus(), app(p(), app(s(), x))), app(p(), app(s(), y))))
    (app#(app(div(), app(s(), x)), app(s(), y)) -> app#(app(minus(), x), y), app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(p(), app(s(), y)))
    (app#(app(div(), app(s(), x)), app(s(), y)) -> app#(app(minus(), x), y), app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(p(), app(s(), x)))
    (app#(app(div(), app(s(), x)), app(s(), y)) -> app#(app(minus(), x), y), app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(minus(), app(p(), app(s(), x))))
    (app#(app(div(), app(s(), x)), app(s(), y)) -> app#(app(minus(), x), y), app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(app(minus(), app(p(), app(s(), x))), app(p(), app(s(), y))))
    (app#(app(div(), app(s(), x)), app(s(), y)) -> app#(app(div(), app(app(minus(), x), y)), app(s(), y)), app#(app(div(), app(s(), x)), app(s(), y)) -> app#(app(minus(), x), y))
    (app#(app(div(), app(s(), x)), app(s(), y)) -> app#(app(div(), app(app(minus(), x), y)), app(s(), y)), app#(app(div(), app(s(), x)), app(s(), y)) -> app#(app(div(), app(app(minus(), x), y)), app(s(), y)))
    (app#(app(div(), app(s(), x)), app(s(), y)) -> app#(app(div(), app(app(minus(), x), y)), app(s(), y)), app#(app(div(), app(s(), x)), app(s(), y)) -> app#(minus(), x))
    (app#(app(div(), app(s(), x)), app(s(), y)) -> app#(app(div(), app(app(minus(), x), y)), app(s(), y)), app#(app(div(), app(s(), x)), app(s(), y)) -> app#(s(), app(app(div(), app(app(minus(), x), y)), app(s(), y))))
    (app#(app(div(), app(s(), x)), app(s(), y)) -> app#(app(div(), app(app(minus(), x), y)), app(s(), y)), app#(app(div(), app(s(), x)), app(s(), y)) -> app#(div(), app(app(minus(), x), y)))
    (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(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(minus(), app(s(), x)), app(s(), y)) -> app#(app(minus(), app(p(), app(s(), x))), app(p(), app(s(), y))))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(minus(), app(p(), app(s(), x))))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(p(), app(s(), x)))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(p(), app(s(), y)))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(div(), app(s(), x)), app(s(), y)) -> app#(app(minus(), x), y))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(div(), app(s(), x)), app(s(), y)) -> app#(app(div(), app(app(minus(), x), y)), app(s(), y)))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(div(), app(s(), x)), app(s(), y)) -> app#(minus(), x))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(div(), app(s(), x)), app(s(), y)) -> app#(s(), app(app(div(), app(app(minus(), x), y)), app(s(), y))))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(div(), app(s(), x)), app(s(), y)) -> app#(div(), app(app(minus(), x), y)))}
   STATUS:
    arrows: 0.822485
    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)}
     Scc:
      {app#(app(div(), app(s(), x)), app(s(), y)) -> app#(app(div(), app(app(minus(), x), y)), app(s(), y))}
     Scc:
      {app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(app(minus(), app(p(), app(s(), x))), app(p(), app(s(), y)))}
     
     SCC (2):
      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)}
      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(minus(), x), 0()) -> x,
       app(app(minus(), app(s(), x)), app(s(), y)) -> app(app(minus(), app(p(), app(s(), x))), app(p(), app(s(), y))),
         app(app(div(), app(s(), x)), app(s(), y)) -> app(s(), app(app(div(), app(app(minus(), x), y)), app(s(), y))),
                 app(app(div(), 0()), app(s(), y)) -> 0(),
                             app(p(), app(s(), x)) -> x}
      Open
     SCC (1):
      Strict:
       {app#(app(div(), app(s(), x)), app(s(), y)) -> app#(app(div(), app(app(minus(), x), y)), app(s(), 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(minus(), x), 0()) -> x,
       app(app(minus(), app(s(), x)), app(s(), y)) -> app(app(minus(), app(p(), app(s(), x))), app(p(), app(s(), y))),
         app(app(div(), app(s(), x)), app(s(), y)) -> app(s(), app(app(div(), app(app(minus(), x), y)), app(s(), y))),
                 app(app(div(), 0()), app(s(), y)) -> 0(),
                             app(p(), app(s(), x)) -> x}
      Open
     
     
     
     
     SCC (1):
      Strict:
       {app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(app(minus(), app(p(), app(s(), x))), app(p(), app(s(), 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(minus(), x), 0()) -> x,
       app(app(minus(), app(s(), x)), app(s(), y)) -> app(app(minus(), app(p(), app(s(), x))), app(p(), app(s(), y))),
         app(app(div(), app(s(), x)), app(s(), y)) -> app(s(), app(app(div(), app(app(minus(), x), y)), app(s(), y))),
                 app(app(div(), 0()), app(s(), y)) -> 0(),
                             app(p(), app(s(), x)) -> x}
      Open