YES

Problem:
 app(app(neq(),0()),0()) -> false()
 app(app(neq(),0()),app(s(),y)) -> true()
 app(app(neq(),app(s(),x)),0()) -> true()
 app(app(neq(),app(s(),x)),app(s(),y)) -> app(app(neq(),x),y)
 app(app(filter(),f),nil()) -> nil()
 app(app(filter(),f),app(app(cons(),y),ys)) ->
 app(app(app(filtersub(),app(f,y)),f),app(app(cons(),y),ys))
 app(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) ->
 app(app(cons(),y),app(app(filter(),f),ys))
 app(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app(app(filter(),f),ys)
 nonzero() -> app(filter(),app(neq(),0()))

Proof:
 DP Processor:
  DPs:
   app#(app(neq(),app(s(),x)),app(s(),y)) -> app#(neq(),x)
   app#(app(neq(),app(s(),x)),app(s(),y)) -> app#(app(neq(),x),y)
   app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(f,y)
   app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(filtersub(),app(f,y))
   app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(app(filtersub(),app(f,y)),f)
   app#(app(filter(),f),app(app(cons(),y),ys)) ->
   app#(app(app(filtersub(),app(f,y)),f),app(app(cons(),y),ys))
   app#(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) -> app#(filter(),f)
   app#(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) -> app#(app(filter(),f),ys)
   app#(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) ->
   app#(app(cons(),y),app(app(filter(),f),ys))
   app#(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app#(filter(),f)
   app#(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app#(app(filter(),f),ys)
   nonzero#() -> app#(neq(),0())
   nonzero#() -> app#(filter(),app(neq(),0()))
  TRS:
   app(app(neq(),0()),0()) -> false()
   app(app(neq(),0()),app(s(),y)) -> true()
   app(app(neq(),app(s(),x)),0()) -> true()
   app(app(neq(),app(s(),x)),app(s(),y)) -> app(app(neq(),x),y)
   app(app(filter(),f),nil()) -> nil()
   app(app(filter(),f),app(app(cons(),y),ys)) ->
   app(app(app(filtersub(),app(f,y)),f),app(app(cons(),y),ys))
   app(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) ->
   app(app(cons(),y),app(app(filter(),f),ys))
   app(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app(app(filter(),f),ys)
   nonzero() -> app(filter(),app(neq(),0()))
  EDG Processor:
   DPs:
    app#(app(neq(),app(s(),x)),app(s(),y)) -> app#(neq(),x)
    app#(app(neq(),app(s(),x)),app(s(),y)) -> app#(app(neq(),x),y)
    app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(f,y)
    app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(filtersub(),app(f,y))
    app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(app(filtersub(),app(f,y)),f)
    app#(app(filter(),f),app(app(cons(),y),ys)) ->
    app#(app(app(filtersub(),app(f,y)),f),app(app(cons(),y),ys))
    app#(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) -> app#(filter(),f)
    app#(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) -> app#(app(filter(),f),ys)
    app#(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) ->
    app#(app(cons(),y),app(app(filter(),f),ys))
    app#(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app#(filter(),f)
    app#(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app#(app(filter(),f),ys)
    nonzero#() -> app#(neq(),0())
    nonzero#() -> app#(filter(),app(neq(),0()))
   TRS:
    app(app(neq(),0()),0()) -> false()
    app(app(neq(),0()),app(s(),y)) -> true()
    app(app(neq(),app(s(),x)),0()) -> true()
    app(app(neq(),app(s(),x)),app(s(),y)) -> app(app(neq(),x),y)
    app(app(filter(),f),nil()) -> nil()
    app(app(filter(),f),app(app(cons(),y),ys)) ->
    app(app(app(filtersub(),app(f,y)),f),app(app(cons(),y),ys))
    app(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) ->
    app(app(cons(),y),app(app(filter(),f),ys))
    app(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app(app(filter(),f),ys)
    nonzero() -> app(filter(),app(neq(),0()))
   graph:
    app#(app(filter(),f),app(app(cons(),y),ys)) ->
    app#(app(app(filtersub(),app(f,y)),f),app(app(cons(),y),ys)) ->
    app#(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) -> app#(filter(),f)
    app#(app(filter(),f),app(app(cons(),y),ys)) ->
    app#(app(app(filtersub(),app(f,y)),f),app(app(cons(),y),ys)) ->
    app#(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) -> app#(app(filter(),f),ys)
    app#(app(filter(),f),app(app(cons(),y),ys)) ->
    app#(app(app(filtersub(),app(f,y)),f),app(app(cons(),y),ys)) ->
    app#(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) ->
    app#(app(cons(),y),app(app(filter(),f),ys))
    app#(app(filter(),f),app(app(cons(),y),ys)) ->
    app#(app(app(filtersub(),app(f,y)),f),app(app(cons(),y),ys)) ->
    app#(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app#(filter(),f)
    app#(app(filter(),f),app(app(cons(),y),ys)) ->
    app#(app(app(filtersub(),app(f,y)),f),app(app(cons(),y),ys)) ->
    app#(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app#(app(filter(),f),ys)
    app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(f,y) ->
    app#(app(neq(),app(s(),x)),app(s(),y)) -> app#(neq(),x)
    app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(f,y) ->
    app#(app(neq(),app(s(),x)),app(s(),y)) -> app#(app(neq(),x),y)
    app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(f,y) ->
    app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(f,y)
    app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(f,y) ->
    app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(filtersub(),app(f,y))
    app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(f,y) ->
    app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(app(filtersub(),app(f,y)),f)
    app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(f,y) ->
    app#(app(filter(),f),app(app(cons(),y),ys)) ->
    app#(app(app(filtersub(),app(f,y)),f),app(app(cons(),y),ys))
    app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(f,y) ->
    app#(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) -> app#(filter(),f)
    app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(f,y) ->
    app#(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) -> app#(app(filter(),f),ys)
    app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(f,y) ->
    app#(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) ->
    app#(app(cons(),y),app(app(filter(),f),ys))
    app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(f,y) ->
    app#(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app#(filter(),f)
    app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(f,y) ->
    app#(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app#(app(filter(),f),ys)
    app#(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) -> app#(app(filter(),f),ys) ->
    app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(f,y)
    app#(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) -> app#(app(filter(),f),ys) ->
    app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(filtersub(),app(f,y))
    app#(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) -> app#(app(filter(),f),ys) ->
    app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(app(filtersub(),app(f,y)),f)
    app#(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) -> app#(app(filter(),f),ys) ->
    app#(app(filter(),f),app(app(cons(),y),ys)) ->
    app#(app(app(filtersub(),app(f,y)),f),app(app(cons(),y),ys))
    app#(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app#(app(filter(),f),ys) ->
    app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(f,y)
    app#(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app#(app(filter(),f),ys) ->
    app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(filtersub(),app(f,y))
    app#(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app#(app(filter(),f),ys) ->
    app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(app(filtersub(),app(f,y)),f)
    app#(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app#(app(filter(),f),ys) ->
    app#(app(filter(),f),app(app(cons(),y),ys)) ->
    app#(app(app(filtersub(),app(f,y)),f),app(app(cons(),y),ys))
    app#(app(neq(),app(s(),x)),app(s(),y)) -> app#(app(neq(),x),y) ->
    app#(app(neq(),app(s(),x)),app(s(),y)) -> app#(neq(),x)
    app#(app(neq(),app(s(),x)),app(s(),y)) -> app#(app(neq(),x),y) ->
    app#(app(neq(),app(s(),x)),app(s(),y)) -> app#(app(neq(),x),y)
   SCC Processor:
    #sccs: 2
    #rules: 5
    #arcs: 26/169
    DPs:
     app#(app(filter(),f),app(app(cons(),y),ys)) ->
     app#(app(app(filtersub(),app(f,y)),f),app(app(cons(),y),ys))
     app#(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app#(app(filter(),f),ys)
     app#(app(filter(),f),app(app(cons(),y),ys)) -> app#(f,y)
     app#(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) -> app#(app(filter(),f),ys)
    TRS:
     app(app(neq(),0()),0()) -> false()
     app(app(neq(),0()),app(s(),y)) -> true()
     app(app(neq(),app(s(),x)),0()) -> true()
     app(app(neq(),app(s(),x)),app(s(),y)) -> app(app(neq(),x),y)
     app(app(filter(),f),nil()) -> nil()
     app(app(filter(),f),app(app(cons(),y),ys)) ->
     app(app(app(filtersub(),app(f,y)),f),app(app(cons(),y),ys))
     app(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) ->
     app(app(cons(),y),app(app(filter(),f),ys))
     app(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app(app(filter(),f),ys)
     nonzero() -> app(filter(),app(neq(),0()))
    Subterm Criterion Processor:
     simple projection:
      pi(app#) = 1
     problem:
      DPs:
       app#(app(filter(),f),app(app(cons(),y),ys)) ->
       app#(app(app(filtersub(),app(f,y)),f),app(app(cons(),y),ys))
      TRS:
       app(app(neq(),0()),0()) -> false()
       app(app(neq(),0()),app(s(),y)) -> true()
       app(app(neq(),app(s(),x)),0()) -> true()
       app(app(neq(),app(s(),x)),app(s(),y)) -> app(app(neq(),x),y)
       app(app(filter(),f),nil()) -> nil()
       app(app(filter(),f),app(app(cons(),y),ys)) ->
       app(app(app(filtersub(),app(f,y)),f),app(app(cons(),y),ys))
       app(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) ->
       app(app(cons(),y),app(app(filter(),f),ys))
       app(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app(app(filter(),f),ys)
       nonzero() -> app(filter(),app(neq(),0()))
     Bounds Processor:
      bound: 0
      enrichment: top-dp
      automaton:
       final states: {13}
       transitions:
        nonzero0() -> 29*
        app{#,0}(39,36) -> 13*
        app0(26,35) -> 30*
        app0(21,35) -> 33*
        app0(36,39) -> 30*
        app0(26,39) -> 30*
        app0(27,20) -> 30*
        app0(21,39) -> 33*
        app0(22,20) -> 30*
        app0(27,22) -> 30*
        app0(22,22) -> 30*
        app0(27,24) -> 30*
        app0(22,24) -> 30*
        app0(27,26) -> 30*
        app0(22,26) -> 30*
        app0(27,28) -> 30*
        app0(22,28) -> 30*
        app0(27,30) -> 30*
        app0(22,30) -> 35*
        app0(27,36) -> 30*
        app0(22,36) -> 35*
        app0(33,21) -> 36*
        app0(28,21) -> 30*
        app0(33,23) -> 36*
        app0(23,21) -> 30*
        app0(28,23) -> 30*
        app0(33,25) -> 36*
        app0(23,23) -> 30*
        app0(28,25) -> 30*
        app0(33,27) -> 36*
        app0(23,25) -> 30*
        app0(28,27) -> 30*
        app0(33,29) -> 36*
        app0(23,27) -> 30*
        app0(28,29) -> 30*
        app0(23,29) -> 30*
        app0(33,33) -> 36*
        app0(28,33) -> 30*
        app0(33,35) -> 36*
        app0(23,33) -> 30*
        app0(28,35) -> 30*
        app0(23,35) -> 30*
        app0(39,20) -> 30*
        app0(33,39) -> 36*
        app0(28,39) -> 30*
        app0(39,22) -> 30*
        app0(29,20) -> 30*
        app0(23,39) -> 30*
        app0(24,20) -> 30*
        app0(39,24) -> 30*
        app0(29,22) -> 30*
        app0(24,22) -> 30*
        app0(39,26) -> 30*
        app0(29,24) -> 30*
        app0(24,24) -> 30*
        app0(39,28) -> 30*
        app0(29,26) -> 30*
        app0(24,26) -> 30*
        app0(39,30) -> 30*
        app0(29,28) -> 30*
        app0(24,28) -> 30*
        app0(29,30) -> 30*
        app0(24,30) -> 30*
        app0(39,36) -> 30*
        app0(29,36) -> 30*
        app0(24,36) -> 30*
        app0(35,21) -> 39*
        app0(30,21) -> 30*
        app0(35,23) -> 39*
        app0(25,21) -> 30*
        app0(30,23) -> 30*
        app0(20,21) -> 30*
        app0(35,25) -> 39*
        app0(25,23) -> 30*
        app0(30,25) -> 30*
        app0(20,23) -> 30*
        app0(35,27) -> 39*
        app0(25,25) -> 30*
        app0(30,27) -> 30*
        app0(20,25) -> 30*
        app0(35,29) -> 39*
        app0(25,27) -> 30*
        app0(30,29) -> 30*
        app0(20,27) -> 30*
        app0(25,29) -> 30*
        app0(20,29) -> 30*
        app0(35,33) -> 39*
        app0(30,33) -> 30*
        app0(35,35) -> 39*
        app0(25,33) -> 30*
        app0(30,35) -> 30*
        app0(20,33) -> 30*
        app0(25,35) -> 30*
        app0(20,35) -> 30*
        app0(35,39) -> 39*
        app0(36,20) -> 30*
        app0(30,39) -> 30*
        app0(25,39) -> 30*
        app0(36,22) -> 30*
        app0(26,20) -> 30*
        app0(20,39) -> 30*
        app0(21,20) -> 33*
        app0(36,24) -> 30*
        app0(26,22) -> 30*
        app0(21,22) -> 33*
        app0(36,26) -> 30*
        app0(26,24) -> 30*
        app0(21,24) -> 33*
        app0(36,28) -> 30*
        app0(26,26) -> 30*
        app0(21,26) -> 33*
        app0(36,30) -> 30*
        app0(26,28) -> 30*
        app0(21,28) -> 33*
        app0(26,30) -> 30*
        app0(21,30) -> 33*
        app0(36,36) -> 30*
        app0(26,36) -> 30*
        app0(21,36) -> 33*
        app0(27,21) -> 30*
        app0(22,21) -> 30*
        app0(27,23) -> 30*
        app0(22,23) -> 30*
        app0(27,25) -> 30*
        app0(22,25) -> 30*
        app0(27,27) -> 30*
        app0(22,27) -> 30*
        app0(27,29) -> 30*
        app0(22,29) -> 30*
        app0(27,33) -> 30*
        app0(22,33) -> 35*
        app0(27,35) -> 30*
        app0(22,35) -> 35*
        app0(33,20) -> 36*
        app0(27,39) -> 30*
        app0(28,20) -> 30*
        app0(22,39) -> 35*
        app0(33,22) -> 36*
        app0(23,20) -> 30*
        app0(28,22) -> 30*
        app0(33,24) -> 36*
        app0(23,22) -> 30*
        app0(28,24) -> 30*
        app0(33,26) -> 36*
        app0(23,24) -> 30*
        app0(28,26) -> 30*
        app0(33,28) -> 36*
        app0(23,26) -> 30*
        app0(28,28) -> 30*
        app0(33,30) -> 30,36
        app0(23,28) -> 30*
        app0(28,30) -> 30*
        app0(23,30) -> 30*
        app0(33,36) -> 36*
        app0(28,36) -> 30*
        app0(23,36) -> 30*
        app0(39,21) -> 30*
        app0(39,23) -> 30*
        app0(29,21) -> 30*
        app0(24,21) -> 30*
        app0(39,25) -> 30*
        app0(29,23) -> 30*
        app0(24,23) -> 30*
        app0(39,27) -> 30*
        app0(29,25) -> 30*
        app0(24,25) -> 30*
        app0(39,29) -> 30*
        app0(29,27) -> 30*
        app0(24,27) -> 30*
        app0(29,29) -> 30*
        app0(24,29) -> 30*
        app0(39,33) -> 30*
        app0(39,35) -> 30*
        app0(29,33) -> 30*
        app0(24,33) -> 30*
        app0(29,35) -> 30*
        app0(24,35) -> 30*
        app0(39,39) -> 30*
        app0(35,20) -> 39*
        app0(29,39) -> 30*
        app0(30,20) -> 30*
        app0(24,39) -> 30*
        app0(35,22) -> 39*
        app0(25,20) -> 30*
        app0(30,22) -> 30*
        app0(20,20) -> 30*
        app0(35,24) -> 39*
        app0(25,22) -> 30*
        app0(30,24) -> 30*
        app0(20,22) -> 30*
        app0(35,26) -> 39*
        app0(25,24) -> 30*
        app0(30,26) -> 30*
        app0(20,24) -> 30*
        app0(35,28) -> 39*
        app0(25,26) -> 30*
        app0(30,28) -> 30*
        app0(20,26) -> 30*
        app0(35,30) -> 39*
        app0(25,28) -> 30*
        app0(30,30) -> 30*
        app0(20,28) -> 30*
        app0(25,30) -> 30*
        app0(20,30) -> 29,30
        app0(35,36) -> 39*
        app0(30,36) -> 30*
        app0(25,36) -> 30*
        app0(20,36) -> 30*
        app0(36,21) -> 30*
        app0(36,23) -> 30*
        app0(26,21) -> 30*
        app0(21,21) -> 33*
        app0(36,25) -> 30*
        app0(26,23) -> 30*
        app0(21,23) -> 33*
        app0(36,27) -> 30*
        app0(26,25) -> 30*
        app0(21,25) -> 33*
        app0(36,29) -> 30*
        app0(26,27) -> 30*
        app0(21,27) -> 33*
        app0(26,29) -> 30*
        app0(21,29) -> 33*
        app0(36,33) -> 30*
        app0(36,35) -> 30*
        app0(26,33) -> 30*
        app0(21,33) -> 33*
        filter0() -> 20*
        cons0() -> 21*
        filtersub0() -> 22*
        neq0() -> 23*
        00() -> 24*
        false0() -> 30,25
        s0() -> 26*
        true0() -> 30,27
        nil0() -> 30,28
      problem:
       DPs:
        
       TRS:
        app(app(neq(),0()),0()) -> false()
        app(app(neq(),0()),app(s(),y)) -> true()
        app(app(neq(),app(s(),x)),0()) -> true()
        app(app(neq(),app(s(),x)),app(s(),y)) -> app(app(neq(),x),y)
        app(app(filter(),f),nil()) -> nil()
        app(app(filter(),f),app(app(cons(),y),ys)) ->
        app(app(app(filtersub(),app(f,y)),f),app(app(cons(),y),ys))
        app(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) ->
        app(app(cons(),y),app(app(filter(),f),ys))
        app(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app(app(filter(),f),ys)
        nonzero() -> app(filter(),app(neq(),0()))
      Qed
    
    DPs:
     app#(app(neq(),app(s(),x)),app(s(),y)) -> app#(app(neq(),x),y)
    TRS:
     app(app(neq(),0()),0()) -> false()
     app(app(neq(),0()),app(s(),y)) -> true()
     app(app(neq(),app(s(),x)),0()) -> true()
     app(app(neq(),app(s(),x)),app(s(),y)) -> app(app(neq(),x),y)
     app(app(filter(),f),nil()) -> nil()
     app(app(filter(),f),app(app(cons(),y),ys)) ->
     app(app(app(filtersub(),app(f,y)),f),app(app(cons(),y),ys))
     app(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) ->
     app(app(cons(),y),app(app(filter(),f),ys))
     app(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app(app(filter(),f),ys)
     nonzero() -> app(filter(),app(neq(),0()))
    Subterm Criterion Processor:
     simple projection:
      pi(app#) = 1
     problem:
      DPs:
       
      TRS:
       app(app(neq(),0()),0()) -> false()
       app(app(neq(),0()),app(s(),y)) -> true()
       app(app(neq(),app(s(),x)),0()) -> true()
       app(app(neq(),app(s(),x)),app(s(),y)) -> app(app(neq(),x),y)
       app(app(filter(),f),nil()) -> nil()
       app(app(filter(),f),app(app(cons(),y),ys)) ->
       app(app(app(filtersub(),app(f,y)),f),app(app(cons(),y),ys))
       app(app(app(filtersub(),true()),f),app(app(cons(),y),ys)) ->
       app(app(cons(),y),app(app(filter(),f),ys))
       app(app(app(filtersub(),false()),f),app(app(cons(),y),ys)) -> app(app(filter(),f),ys)
       nonzero() -> app(filter(),app(neq(),0()))
     Qed