MAYBE
Time: 0.114938
TRS:
 {     app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs)),
      app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs),
            app(app(app(quot(), x), 0()), app(s(), z)) -> app(s(), app(app(app(quot(), x), app(s(), z)), app(s(), z))),
  app(app(app(quot(), 0()), app(s(), y)), app(s(), z)) -> 0(),
    app(app(app(quot(), app(s(), x)), app(s(), y)), z) -> app(app(app(quot(), x), y), z),
           app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)),
                             app(app(map(), f), nil()) -> nil(),
        app(app(filter(), f), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(f, x)), f), x), xs),
                          app(app(filter(), f), nil()) -> nil()}
 DP:
  DP:
   {   app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(cons(), x), app(app(filter(), f), xs)),
       app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(filter(), f), xs),
       app#(app(app(app(filter2(), true()), f), x), xs) -> app#(cons(), x),
       app#(app(app(app(filter2(), true()), f), x), xs) -> app#(filter(), f),
      app#(app(app(app(filter2(), false()), f), x), xs) -> app#(app(filter(), f), xs),
      app#(app(app(app(filter2(), false()), f), x), xs) -> app#(filter(), f),
            app#(app(app(quot(), x), 0()), app(s(), z)) -> app#(app(app(quot(), x), app(s(), z)), app(s(), z)),
            app#(app(app(quot(), x), 0()), app(s(), z)) -> app#(app(quot(), x), app(s(), z)),
            app#(app(app(quot(), x), 0()), app(s(), z)) -> app#(s(), app(app(app(quot(), x), app(s(), z)), app(s(), z))),
    app#(app(app(quot(), app(s(), x)), app(s(), y)), z) -> app#(app(app(quot(), x), y), z),
    app#(app(app(quot(), app(s(), x)), app(s(), y)), z) -> app#(app(quot(), x), y),
    app#(app(app(quot(), app(s(), x)), app(s(), y)), z) -> app#(quot(), 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#(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(filter(), f), app(app(cons(), x), xs)) -> app#(f, x),
        app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(app(filter2(), app(f, x)), f), x), xs),
        app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(filter2(), app(f, x)), f), x),
        app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(filter2(), app(f, x)), f),
        app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(filter2(), app(f, x))}
  TRS:
  {     app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs)),
       app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs),
             app(app(app(quot(), x), 0()), app(s(), z)) -> app(s(), app(app(app(quot(), x), app(s(), z)), app(s(), z))),
   app(app(app(quot(), 0()), app(s(), y)), app(s(), z)) -> 0(),
     app(app(app(quot(), app(s(), x)), app(s(), y)), z) -> app(app(app(quot(), x), y), z),
            app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)),
                              app(app(map(), f), nil()) -> nil(),
         app(app(filter(), f), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(f, x)), f), x), xs),
                           app(app(filter(), f), nil()) -> nil()}
  EDG:
   {(app#(app(app(quot(), x), 0()), app(s(), z)) -> app#(app(app(quot(), x), app(s(), z)), app(s(), z)), app#(app(app(quot(), app(s(), x)), app(s(), y)), z) -> app#(quot(), x))
    (app#(app(app(quot(), x), 0()), app(s(), z)) -> app#(app(app(quot(), x), app(s(), z)), app(s(), z)), app#(app(app(quot(), app(s(), x)), app(s(), y)), z) -> app#(app(quot(), x), y))
    (app#(app(app(quot(), x), 0()), app(s(), z)) -> app#(app(app(quot(), x), app(s(), z)), app(s(), z)), app#(app(app(quot(), app(s(), x)), app(s(), y)), z) -> app#(app(app(quot(), x), y), z))
    (app#(app(app(quot(), app(s(), x)), app(s(), y)), z) -> app#(app(app(quot(), x), y), z), app#(app(app(quot(), app(s(), x)), app(s(), y)), z) -> app#(quot(), x))
    (app#(app(app(quot(), app(s(), x)), app(s(), y)), z) -> app#(app(app(quot(), x), y), z), app#(app(app(quot(), app(s(), x)), app(s(), y)), z) -> app#(app(quot(), x), y))
    (app#(app(app(quot(), app(s(), x)), app(s(), y)), z) -> app#(app(app(quot(), x), y), z), app#(app(app(quot(), app(s(), x)), app(s(), y)), z) -> app#(app(app(quot(), x), y), z))
    (app#(app(app(quot(), app(s(), x)), app(s(), y)), z) -> app#(app(app(quot(), x), y), z), app#(app(app(quot(), x), 0()), app(s(), z)) -> app#(s(), app(app(app(quot(), x), app(s(), z)), app(s(), z))))
    (app#(app(app(quot(), app(s(), x)), app(s(), y)), z) -> app#(app(app(quot(), x), y), z), app#(app(app(quot(), x), 0()), app(s(), z)) -> app#(app(quot(), x), app(s(), z)))
    (app#(app(app(quot(), app(s(), x)), app(s(), y)), z) -> app#(app(app(quot(), x), y), z), app#(app(app(quot(), x), 0()), app(s(), z)) -> app#(app(app(quot(), x), app(s(), z)), app(s(), z)))
    (app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(filter(), f), xs), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(filter2(), app(f, x)))
    (app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(filter(), f), xs), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(filter2(), app(f, x)), f))
    (app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(filter(), f), xs), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(filter2(), app(f, x)), f), x))
    (app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(filter(), f), xs), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(app(filter2(), app(f, x)), f), x), xs))
    (app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(filter(), f), xs), app#(app(filter(), 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#(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#(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#(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#(f, x))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(filter2(), app(f, x)))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(filter2(), app(f, x)), f))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(filter2(), app(f, x)), f), x))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(app(filter2(), app(f, x)), f), x), xs))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), 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#(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#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(quot(), app(s(), x)), app(s(), y)), z) -> app#(quot(), x))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(quot(), app(s(), x)), app(s(), y)), z) -> app#(app(quot(), x), y))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(quot(), app(s(), x)), app(s(), y)), z) -> app#(app(app(quot(), x), y), z))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(quot(), x), 0()), app(s(), z)) -> app#(s(), app(app(app(quot(), x), app(s(), z)), app(s(), z))))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(quot(), x), 0()), app(s(), z)) -> app#(app(quot(), x), app(s(), z)))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(quot(), x), 0()), app(s(), z)) -> app#(app(app(quot(), x), app(s(), z)), app(s(), z)))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), false()), f), x), xs) -> app#(filter(), f))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), false()), f), x), xs) -> app#(app(filter(), f), xs))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(filter(), f))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(cons(), x))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(filter(), f), xs))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(cons(), x), app(app(filter(), f), xs)))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(cons(), x), app(app(filter(), f), xs)))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(filter(), f), xs))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(cons(), x))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(filter(), f))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), false()), f), x), xs) -> app#(app(filter(), f), xs))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), false()), f), x), xs) -> app#(filter(), f))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(quot(), x), 0()), app(s(), z)) -> app#(app(app(quot(), x), app(s(), z)), app(s(), z)))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(quot(), x), 0()), app(s(), z)) -> app#(app(quot(), x), app(s(), z)))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(quot(), x), 0()), app(s(), z)) -> app#(s(), app(app(app(quot(), x), app(s(), z)), app(s(), z))))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(quot(), app(s(), x)), app(s(), y)), z) -> app#(app(app(quot(), x), y), z))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(quot(), app(s(), x)), app(s(), y)), z) -> app#(app(quot(), x), y))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(quot(), app(s(), x)), app(s(), y)), z) -> app#(quot(), x))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x))
    (app#(app(filter(), 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(filter(), 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(filter(), 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(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(app(filter2(), app(f, x)), f), x), xs))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(filter2(), app(f, x)), f), x))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(filter2(), app(f, x)), f))
    (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(filter2(), app(f, x)))
    (app#(app(app(app(filter2(), false()), f), x), xs) -> app#(app(filter(), f), xs), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x))
    (app#(app(app(app(filter2(), false()), f), x), xs) -> app#(app(filter(), f), xs), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(app(filter2(), app(f, x)), f), x), xs))
    (app#(app(app(app(filter2(), false()), f), x), xs) -> app#(app(filter(), f), xs), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(filter2(), app(f, x)), f), x))
    (app#(app(app(app(filter2(), false()), f), x), xs) -> app#(app(filter(), f), xs), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(filter2(), app(f, x)), f))
    (app#(app(app(app(filter2(), false()), f), x), xs) -> app#(app(filter(), f), xs), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(filter2(), app(f, x)))}
   STATUS:
    arrows: 0.852608
    SCCS (2):
     Scc:
      { app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(filter(), f), xs),
       app#(app(app(app(filter2(), false()), f), x), xs) -> app#(app(filter(), 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(filter(), f), app(app(cons(), x), xs)) -> app#(f, x)}
     Scc:
      {        app#(app(app(quot(), x), 0()), app(s(), z)) -> app#(app(app(quot(), x), app(s(), z)), app(s(), z)),
       app#(app(app(quot(), app(s(), x)), app(s(), y)), z) -> app#(app(app(quot(), x), y), z)}
     
     SCC (5):
      Strict:
       { app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(filter(), f), xs),
        app#(app(app(app(filter2(), false()), f), x), xs) -> app#(app(filter(), 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(filter(), f), app(app(cons(), x), xs)) -> app#(f, x)}
      Weak:
      {     app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs)),
           app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs),
                 app(app(app(quot(), x), 0()), app(s(), z)) -> app(s(), app(app(app(quot(), x), app(s(), z)), app(s(), z))),
       app(app(app(quot(), 0()), app(s(), y)), app(s(), z)) -> 0(),
         app(app(app(quot(), app(s(), x)), app(s(), y)), z) -> app(app(app(quot(), x), y), z),
                app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)),
                                  app(app(map(), f), nil()) -> nil(),
             app(app(filter(), f), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(f, x)), f), x), xs),
                               app(app(filter(), f), nil()) -> nil()}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [app](x0, x1) = x0 + x1,
        
        [0] = 0,
        
        [quot] = 1,
        
        [s] = 0,
        
        [nil] = 0,
        
        [map] = 0,
        
        [cons] = 1,
        
        [filter] = 0,
        
        [filter2] = 0,
        
        [true] = 0,
        
        [false] = 0,
        
        [app#](x0, x1) = x0
       Strict:
        app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x)
        1 + 1x + 0f + 1xs >= 0 + 1x + 0f
        app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs)
        1 + 1x + 0f + 1xs >= 0 + 0f + 1xs
        app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x)
        1 + 1x + 0f + 1xs >= 0 + 1x + 0f
        app#(app(app(app(filter2(), false()), f), x), xs) -> app#(app(filter(), f), xs)
        0 + 0x + 0f + 1xs >= 0 + 0f + 1xs
        app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(filter(), f), xs)
        0 + 0x + 0f + 1xs >= 0 + 0f + 1xs
       Weak:
        app(app(filter(), f), nil()) -> nil()
        0 + 1f >= 0
        app(app(filter(), f), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(f, x)), f), x), xs)
        1 + 1x + 1f + 1xs >= 0 + 2x + 2f + 1xs
        app(app(map(), f), nil()) -> nil()
        0 + 1f >= 0
        app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs))
        1 + 1x + 1f + 1xs >= 1 + 1x + 2f + 1xs
        app(app(app(quot(), app(s(), x)), app(s(), y)), z) -> app(app(app(quot(), x), y), z)
        1 + 1y + 1z + 1x >= 1 + 1y + 1z + 1x
        app(app(app(quot(), 0()), app(s(), y)), app(s(), z)) -> 0()
        1 + 1y + 1z >= 0
        app(app(app(quot(), x), 0()), app(s(), z)) -> app(s(), app(app(app(quot(), x), app(s(), z)), app(s(), z)))
        1 + 1z + 1x >= 1 + 2z + 1x
        app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs)
        0 + 1x + 1f + 1xs >= 0 + 1f + 1xs
        app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs))
        0 + 1x + 1f + 1xs >= 1 + 1x + 1f + 1xs
      SCCS (0):
       
       
       
    
    
    
    
    
    
    
    
    
    SCC (2):
     Strict:
      {        app#(app(app(quot(), x), 0()), app(s(), z)) -> app#(app(app(quot(), x), app(s(), z)), app(s(), z)),
       app#(app(app(quot(), app(s(), x)), app(s(), y)), z) -> app#(app(app(quot(), x), y), z)}
     Weak:
     {     app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs)),
          app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs),
                app(app(app(quot(), x), 0()), app(s(), z)) -> app(s(), app(app(app(quot(), x), app(s(), z)), app(s(), z))),
      app(app(app(quot(), 0()), app(s(), y)), app(s(), z)) -> 0(),
        app(app(app(quot(), app(s(), x)), app(s(), y)), z) -> app(app(app(quot(), x), y), z),
               app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)),
                                 app(app(map(), f), nil()) -> nil(),
            app(app(filter(), f), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(f, x)), f), x), xs),
                              app(app(filter(), f), nil()) -> nil()}
     Fail