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()))
     Usable Rule Processor:
      DPs:
       app#(app(filter(),f),app(app(cons(),y),ys)) ->
       app#(app(app(filtersub(),app(f,y)),f),app(app(cons(),y),ys))
      TRS:
       f13(x,y) -> x
       f13(x,y) -> y
       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)
      Bounds Processor:
       bound: 0
       enrichment: top-dp
       automaton:
        final states: {13}
        transitions:
         true0() -> 30,28
         nil0() -> 30,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) -> 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) -> 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*
         f130(21,33) -> 23*
         f130(26,35) -> 23*
         f130(21,35) -> 23*
         f130(36,39) -> 23*
         f130(26,39) -> 23*
         f130(27,20) -> 23*
         f130(21,39) -> 23*
         f130(22,20) -> 23*
         f130(27,22) -> 23*
         f130(22,22) -> 23*
         f130(27,24) -> 23*
         f130(22,24) -> 23*
         f130(27,26) -> 23*
         f130(22,26) -> 23*
         f130(27,28) -> 23*
         f130(22,28) -> 23*
         f130(27,30) -> 23*
         f130(22,30) -> 23*
         f130(27,36) -> 23*
         f130(22,36) -> 23*
         f130(33,21) -> 23*
         f130(28,21) -> 23*
         f130(33,23) -> 23*
         f130(23,21) -> 23*
         f130(28,23) -> 23*
         f130(33,25) -> 23*
         f130(23,23) -> 23*
         f130(28,25) -> 23*
         f130(33,27) -> 23*
         f130(23,25) -> 23*
         f130(28,27) -> 23*
         f130(33,29) -> 23*
         f130(23,27) -> 23*
         f130(28,29) -> 23*
         f130(23,29) -> 23*
         f130(33,33) -> 23*
         f130(28,33) -> 23*
         f130(33,35) -> 23*
         f130(23,33) -> 23*
         f130(28,35) -> 23*
         f130(23,35) -> 23*
         f130(39,20) -> 23*
         f130(33,39) -> 23*
         f130(28,39) -> 23*
         f130(39,22) -> 23*
         f130(29,20) -> 23*
         f130(23,39) -> 23*
         f130(24,20) -> 23*
         f130(39,24) -> 23*
         f130(29,22) -> 23*
         f130(24,22) -> 23*
         f130(39,26) -> 23*
         f130(29,24) -> 23*
         f130(24,24) -> 23*
         f130(39,28) -> 23*
         f130(29,26) -> 23*
         f130(24,26) -> 23*
         f130(39,30) -> 23*
         f130(29,28) -> 23*
         f130(24,28) -> 23*
         f130(29,30) -> 23*
         f130(24,30) -> 23*
         f130(39,36) -> 23*
         f130(29,36) -> 23*
         f130(24,36) -> 23*
         f130(35,21) -> 23*
         f130(30,21) -> 23*
         f130(35,23) -> 23*
         f130(25,21) -> 23*
         f130(30,23) -> 23*
         f130(20,21) -> 23*
         f130(35,25) -> 23*
         f130(25,23) -> 23*
         f130(30,25) -> 23*
         f130(20,23) -> 23*
         f130(35,27) -> 23*
         f130(25,25) -> 23*
         f130(30,27) -> 23*
         f130(20,25) -> 23*
         f130(35,29) -> 23*
         f130(25,27) -> 23*
         f130(30,29) -> 23*
         f130(20,27) -> 23*
         f130(25,29) -> 23*
         f130(20,29) -> 23*
         f130(35,33) -> 23*
         f130(30,33) -> 23*
         f130(35,35) -> 23*
         f130(25,33) -> 23*
         f130(30,35) -> 23*
         f130(20,33) -> 23*
         f130(25,35) -> 23*
         f130(20,35) -> 23*
         f130(35,39) -> 23*
         f130(36,20) -> 23*
         f130(30,39) -> 23*
         f130(25,39) -> 23*
         f130(36,22) -> 23*
         f130(26,20) -> 23*
         f130(20,39) -> 23*
         f130(21,20) -> 23*
         f130(36,24) -> 23*
         f130(26,22) -> 23*
         f130(21,22) -> 23*
         f130(36,26) -> 23*
         f130(26,24) -> 23*
         f130(21,24) -> 23*
         f130(36,28) -> 23*
         f130(26,26) -> 23*
         f130(21,26) -> 23*
         f130(36,30) -> 23*
         f130(26,28) -> 23*
         f130(21,28) -> 23*
         f130(26,30) -> 23*
         f130(21,30) -> 23*
         f130(36,36) -> 23*
         f130(26,36) -> 23*
         f130(21,36) -> 23*
         f130(27,21) -> 23*
         f130(22,21) -> 23*
         f130(27,23) -> 23*
         f130(22,23) -> 23*
         f130(27,25) -> 23*
         f130(22,25) -> 23*
         f130(27,27) -> 23*
         f130(22,27) -> 23*
         f130(27,29) -> 23*
         f130(22,29) -> 23*
         f130(27,33) -> 23*
         f130(22,33) -> 23*
         f130(27,35) -> 23*
         f130(22,35) -> 23*
         f130(33,20) -> 23*
         f130(27,39) -> 23*
         f130(28,20) -> 23*
         f130(22,39) -> 23*
         f130(33,22) -> 23*
         f130(23,20) -> 23*
         f130(28,22) -> 23*
         f130(33,24) -> 23*
         f130(23,22) -> 23*
         f130(28,24) -> 23*
         f130(33,26) -> 23*
         f130(23,24) -> 23*
         f130(28,26) -> 23*
         f130(33,28) -> 23*
         f130(23,26) -> 23*
         f130(28,28) -> 23*
         f130(33,30) -> 23*
         f130(23,28) -> 23*
         f130(28,30) -> 23*
         f130(23,30) -> 23*
         f130(33,36) -> 23*
         f130(28,36) -> 23*
         f130(23,36) -> 23*
         f130(39,21) -> 23*
         f130(39,23) -> 23*
         f130(29,21) -> 23*
         f130(24,21) -> 23*
         f130(39,25) -> 23*
         f130(29,23) -> 23*
         f130(24,23) -> 23*
         f130(39,27) -> 23*
         f130(29,25) -> 23*
         f130(24,25) -> 23*
         f130(39,29) -> 23*
         f130(29,27) -> 23*
         f130(24,27) -> 23*
         f130(29,29) -> 23*
         f130(24,29) -> 23*
         f130(39,33) -> 23*
         f130(39,35) -> 23*
         f130(29,33) -> 23*
         f130(24,33) -> 23*
         f130(29,35) -> 23*
         f130(24,35) -> 23*
         f130(39,39) -> 23*
         f130(35,20) -> 23*
         f130(29,39) -> 23*
         f130(30,20) -> 23*
         f130(24,39) -> 23*
         f130(35,22) -> 23*
         f130(25,20) -> 23*
         f130(30,22) -> 23*
         f130(20,20) -> 23*
         f130(35,24) -> 23*
         f130(25,22) -> 23*
         f130(30,24) -> 23*
         f130(20,22) -> 23*
         f130(35,26) -> 23*
         f130(25,24) -> 23*
         f130(30,26) -> 23*
         f130(20,24) -> 23*
         f130(35,28) -> 23*
         f130(25,26) -> 23*
         f130(30,28) -> 23*
         f130(20,26) -> 23*
         f130(35,30) -> 23*
         f130(25,28) -> 23*
         f130(30,30) -> 23*
         f130(20,28) -> 23*
         f130(25,30) -> 23*
         f130(20,30) -> 23*
         f130(35,36) -> 23*
         f130(30,36) -> 23*
         f130(25,36) -> 23*
         f130(20,36) -> 23*
         f130(36,21) -> 23*
         f130(36,23) -> 23*
         f130(26,21) -> 23*
         f130(21,21) -> 23*
         f130(36,25) -> 23*
         f130(26,23) -> 23*
         f130(21,23) -> 23*
         f130(36,27) -> 23*
         f130(26,25) -> 23*
         f130(21,25) -> 23*
         f130(36,29) -> 23*
         f130(26,27) -> 23*
         f130(21,27) -> 23*
         f130(26,29) -> 23*
         f130(21,29) -> 23*
         f130(36,33) -> 23*
         f130(36,35) -> 23*
         f130(26,33) -> 23*
         neq0() -> 24*
         00() -> 25*
         false0() -> 30,26
         s0() -> 27*
         20 -> 23*
         21 -> 23*
         22 -> 23*
         24 -> 23*
         25 -> 23*
         26 -> 23*
         27 -> 23*
         28 -> 23*
         29 -> 23*
         30 -> 23*
         33 -> 23*
         35 -> 23*
         36 -> 23*
         39 -> 23*
       problem:
        DPs:
         
        TRS:
         f13(x,y) -> x
         f13(x,y) -> y
         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)
       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