MAYBE
Time: 0.005019
TRS:
 {               app(app(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y)),
                         app(app(plus(), 0()), y) -> y,
  app(app(sumwith(), f), app(app(cons(), x), xs)) -> app(app(plus(), app(f, x)), app(app(sumwith(), f), xs)),
                    app(app(sumwith(), f), nil()) -> nil()}
 DP:
  DP:
   {               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#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(f, x),
    app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(plus(), app(f, x)), app(app(sumwith(), f), xs)),
    app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(sumwith(), f), xs),
    app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(plus(), app(f, x))}
  TRS:
  {               app(app(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y)),
                          app(app(plus(), 0()), y) -> y,
   app(app(sumwith(), f), app(app(cons(), x), xs)) -> app(app(plus(), app(f, x)), app(app(sumwith(), f), xs)),
                     app(app(sumwith(), f), nil()) -> nil()}
  UR:
   {               app(app(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y)),
                           app(app(plus(), 0()), y) -> y,
    app(app(sumwith(), f), app(app(cons(), x), xs)) -> app(app(plus(), app(f, x)), app(app(sumwith(), f), xs)),
                      app(app(sumwith(), f), nil()) -> nil(),
                                            a(z, w) -> z,
                                            a(z, w) -> w}
   EDG:
    {(app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(plus(), app(f, x)), app(app(sumwith(), f), xs)), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(plus(), app(f, x)))
     (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(plus(), app(f, x)), app(app(sumwith(), f), xs)), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(sumwith(), f), xs))
     (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(plus(), app(f, x)), app(app(sumwith(), f), xs)), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(plus(), app(f, x)), app(app(sumwith(), f), xs)))
     (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(plus(), app(f, x)), app(app(sumwith(), f), xs)), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(f, x))
     (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(plus(), app(f, x)), app(app(sumwith(), f), xs)), app#(app(plus(), app(s(), x)), y) -> app#(s(), app(app(plus(), x), y)))
     (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(plus(), app(f, x)), app(app(sumwith(), f), xs)), app#(app(plus(), app(s(), x)), y) -> app#(plus(), x))
     (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(plus(), app(f, x)), app(app(sumwith(), f), xs)), app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y))
     (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(plus(), app(f, x)))
     (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(sumwith(), f), xs))
     (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(plus(), app(f, x)), app(app(sumwith(), f), xs)))
     (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(f, x))
     (app#(app(sumwith(), 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(sumwith(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(plus(), app(s(), x)), y) -> app#(plus(), x))
     (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y))
     (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(sumwith(), f), xs), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(plus(), app(f, x)))
     (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(sumwith(), f), xs), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(sumwith(), f), xs))
     (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(sumwith(), f), xs), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(plus(), app(f, x)), app(app(sumwith(), f), xs)))
     (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(sumwith(), f), xs), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(f, x))
     (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(sumwith(), f), xs), app#(app(plus(), app(s(), x)), y) -> app#(s(), app(app(plus(), x), y)))
     (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(sumwith(), f), xs), app#(app(plus(), app(s(), x)), y) -> app#(plus(), x))
     (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(sumwith(), f), xs), 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#(app(plus(), app(s(), x)), y) -> 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#(s(), app(app(plus(), x), y)))
     (app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(f, x))
     (app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(plus(), app(f, x)), app(app(sumwith(), f), xs)))
     (app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(sumwith(), f), xs))
     (app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(plus(), app(f, x)))
     (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#(plus(), x), app#(app(plus(), app(s(), x)), y) -> app#(plus(), x))
     (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#(app(plus(), app(s(), x)), y) -> app#(plus(), x), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(f, x))
     (app#(app(plus(), app(s(), x)), y) -> app#(plus(), x), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(plus(), app(f, x)), app(app(sumwith(), f), xs)))
     (app#(app(plus(), app(s(), x)), y) -> app#(plus(), x), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(sumwith(), f), xs))
     (app#(app(plus(), app(s(), x)), y) -> app#(plus(), x), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(plus(), app(f, x)))
     (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(plus(), app(f, x)), app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y))
     (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(plus(), app(f, x)), app#(app(plus(), app(s(), x)), y) -> app#(plus(), x))
     (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(plus(), app(f, x)), app#(app(plus(), app(s(), x)), y) -> app#(s(), app(app(plus(), x), y)))
     (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(plus(), app(f, x)), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(f, x))
     (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(plus(), app(f, x)), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(plus(), app(f, x)), app(app(sumwith(), f), xs)))
     (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(plus(), app(f, x)), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(sumwith(), f), xs))
     (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(plus(), app(f, x)), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(plus(), app(f, x)))
     (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#(s(), 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#(app(plus(), app(s(), x)), y) -> app#(s(), app(app(plus(), x), y)))
     (app#(app(plus(), app(s(), x)), y) -> app#(s(), app(app(plus(), x), y)), app#(app(sumwith(), 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(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(plus(), app(f, x)), app(app(sumwith(), f), xs)))
     (app#(app(plus(), app(s(), x)), y) -> app#(s(), app(app(plus(), x), y)), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(sumwith(), f), xs))
     (app#(app(plus(), app(s(), x)), y) -> app#(s(), app(app(plus(), x), y)), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(plus(), app(f, x)))}
    EDG:
     {(app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(plus(), app(f, x)), app(app(sumwith(), f), xs)), app#(app(plus(), app(s(), x)), y) -> app#(s(), app(app(plus(), x), y)))
      (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(plus(), app(f, x)), app(app(sumwith(), f), xs)), app#(app(plus(), app(s(), x)), y) -> app#(plus(), x))
      (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(plus(), app(f, x)), app(app(sumwith(), f), xs)), app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y))
      (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(plus(), app(f, x)))
      (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(sumwith(), f), xs))
      (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(plus(), app(f, x)), app(app(sumwith(), f), xs)))
      (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(f, x))
      (app#(app(sumwith(), 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(sumwith(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(plus(), app(s(), x)), y) -> app#(plus(), x))
      (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y))
      (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(sumwith(), f), xs), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(plus(), app(f, x)))
      (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(sumwith(), f), xs), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(sumwith(), f), xs))
      (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(sumwith(), f), xs), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(plus(), app(f, x)), app(app(sumwith(), f), xs)))
      (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(sumwith(), f), xs), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(f, 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#(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#(s(), app(app(plus(), x), y)))}
     EDG:
      {(app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(plus(), app(f, x)), app(app(sumwith(), f), xs)), app#(app(plus(), app(s(), x)), y) -> app#(s(), app(app(plus(), x), y)))
       (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(plus(), app(f, x)), app(app(sumwith(), f), xs)), app#(app(plus(), app(s(), x)), y) -> app#(plus(), x))
       (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(plus(), app(f, x)), app(app(sumwith(), f), xs)), app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y))
       (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(plus(), app(f, x)))
       (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(sumwith(), f), xs))
       (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(plus(), app(f, x)), app(app(sumwith(), f), xs)))
       (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(f, x))
       (app#(app(sumwith(), 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(sumwith(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(plus(), app(s(), x)), y) -> app#(plus(), x))
       (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y))
       (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(sumwith(), f), xs), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(plus(), app(f, x)))
       (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(sumwith(), f), xs), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(sumwith(), f), xs))
       (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(sumwith(), f), xs), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(plus(), app(f, x)), app(app(sumwith(), f), xs)))
       (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(sumwith(), f), xs), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(f, 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#(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#(s(), app(app(plus(), x), y)))}
      EDG:
       {(app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(plus(), app(f, x)), app(app(sumwith(), f), xs)), app#(app(plus(), app(s(), x)), y) -> app#(s(), app(app(plus(), x), y)))
        (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(plus(), app(f, x)), app(app(sumwith(), f), xs)), app#(app(plus(), app(s(), x)), y) -> app#(plus(), x))
        (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(plus(), app(f, x)), app(app(sumwith(), f), xs)), app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y))
        (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(plus(), app(f, x)))
        (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(sumwith(), f), xs))
        (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(plus(), app(f, x)), app(app(sumwith(), f), xs)))
        (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(f, x))
        (app#(app(sumwith(), 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(sumwith(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(plus(), app(s(), x)), y) -> app#(plus(), x))
        (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y))
        (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(sumwith(), f), xs), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(plus(), app(f, x)))
        (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(sumwith(), f), xs), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(sumwith(), f), xs))
        (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(sumwith(), f), xs), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(plus(), app(f, x)), app(app(sumwith(), f), xs)))
        (app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(sumwith(), f), xs), app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(f, 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#(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#(s(), app(app(plus(), x), y)))}
       STATUS:
        arrows: 0.653061
        SCCS (2):
         Scc:
          {app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(f, x),
           app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(sumwith(), f), xs)}
         Scc:
          {app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y)}
         
         SCC (2):
          Strict:
           {app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(f, x),
            app#(app(sumwith(), f), app(app(cons(), x), xs)) -> app#(app(sumwith(), f), xs)}
          Weak:
          {               app(app(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y)),
                                  app(app(plus(), 0()), y) -> y,
           app(app(sumwith(), f), app(app(cons(), x), xs)) -> app(app(plus(), app(f, x)), app(app(sumwith(), f), xs)),
                             app(app(sumwith(), f), nil()) -> nil()}
          Open
         
         
         SCC (1):
          Strict:
           {app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y)}
          Weak:
          {               app(app(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y)),
                                  app(app(plus(), 0()), y) -> y,
           app(app(sumwith(), f), app(app(cons(), x), xs)) -> app(app(plus(), app(f, x)), app(app(sumwith(), f), xs)),
                             app(app(sumwith(), f), nil()) -> nil()}
          Open