MAYBE

Problem:
 if(true(),x,y) -> x
 if(false(),x,y) -> y
 eq(0(),0()) -> true()
 eq(0(),s(x)) -> false()
 eq(s(x),0()) -> false()
 eq(s(x),s(y)) -> eq(x,y)
 app(nil(),l) -> l
 app(cons(x,l1),l2) -> cons(x,app(l1,l2))
 app(app(l1,l2),l3) -> app(l1,app(l2,l3))
 mem(x,nil()) -> false()
 mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
 ifmem(true(),x,l) -> true()
 ifmem(false(),x,l) -> mem(x,l)
 inter(x,nil()) -> nil()
 inter(nil(),x) -> nil()
 inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
 inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
 inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
 inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
 ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
 ifinter(false(),x,l1,l2) -> inter(l1,l2)

Proof:
 DP Processor:
  DPs:
   eq#(s(x),s(y)) -> eq#(x,y)
   app#(cons(x,l1),l2) -> app#(l1,l2)
   app#(app(l1,l2),l3) -> app#(l2,l3)
   app#(app(l1,l2),l3) -> app#(l1,app(l2,l3))
   mem#(x,cons(y,l)) -> eq#(x,y)
   mem#(x,cons(y,l)) -> ifmem#(eq(x,y),x,l)
   ifmem#(false(),x,l) -> mem#(x,l)
   inter#(app(l1,l2),l3) -> inter#(l2,l3)
   inter#(app(l1,l2),l3) -> inter#(l1,l3)
   inter#(app(l1,l2),l3) -> app#(inter(l1,l3),inter(l2,l3))
   inter#(l1,app(l2,l3)) -> inter#(l1,l3)
   inter#(l1,app(l2,l3)) -> inter#(l1,l2)
   inter#(l1,app(l2,l3)) -> app#(inter(l1,l2),inter(l1,l3))
   inter#(cons(x,l1),l2) -> mem#(x,l2)
   inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2)
   inter#(l1,cons(x,l2)) -> mem#(x,l1)
   inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1)
   ifinter#(true(),x,l1,l2) -> inter#(l1,l2)
   ifinter#(false(),x,l1,l2) -> inter#(l1,l2)
  TRS:
   if(true(),x,y) -> x
   if(false(),x,y) -> y
   eq(0(),0()) -> true()
   eq(0(),s(x)) -> false()
   eq(s(x),0()) -> false()
   eq(s(x),s(y)) -> eq(x,y)
   app(nil(),l) -> l
   app(cons(x,l1),l2) -> cons(x,app(l1,l2))
   app(app(l1,l2),l3) -> app(l1,app(l2,l3))
   mem(x,nil()) -> false()
   mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
   ifmem(true(),x,l) -> true()
   ifmem(false(),x,l) -> mem(x,l)
   inter(x,nil()) -> nil()
   inter(nil(),x) -> nil()
   inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
   inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
   inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
   inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
   ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
   ifinter(false(),x,l1,l2) -> inter(l1,l2)
  EDG Processor:
   DPs:
    eq#(s(x),s(y)) -> eq#(x,y)
    app#(cons(x,l1),l2) -> app#(l1,l2)
    app#(app(l1,l2),l3) -> app#(l2,l3)
    app#(app(l1,l2),l3) -> app#(l1,app(l2,l3))
    mem#(x,cons(y,l)) -> eq#(x,y)
    mem#(x,cons(y,l)) -> ifmem#(eq(x,y),x,l)
    ifmem#(false(),x,l) -> mem#(x,l)
    inter#(app(l1,l2),l3) -> inter#(l2,l3)
    inter#(app(l1,l2),l3) -> inter#(l1,l3)
    inter#(app(l1,l2),l3) -> app#(inter(l1,l3),inter(l2,l3))
    inter#(l1,app(l2,l3)) -> inter#(l1,l3)
    inter#(l1,app(l2,l3)) -> inter#(l1,l2)
    inter#(l1,app(l2,l3)) -> app#(inter(l1,l2),inter(l1,l3))
    inter#(cons(x,l1),l2) -> mem#(x,l2)
    inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2)
    inter#(l1,cons(x,l2)) -> mem#(x,l1)
    inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1)
    ifinter#(true(),x,l1,l2) -> inter#(l1,l2)
    ifinter#(false(),x,l1,l2) -> inter#(l1,l2)
   TRS:
    if(true(),x,y) -> x
    if(false(),x,y) -> y
    eq(0(),0()) -> true()
    eq(0(),s(x)) -> false()
    eq(s(x),0()) -> false()
    eq(s(x),s(y)) -> eq(x,y)
    app(nil(),l) -> l
    app(cons(x,l1),l2) -> cons(x,app(l1,l2))
    app(app(l1,l2),l3) -> app(l1,app(l2,l3))
    mem(x,nil()) -> false()
    mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
    ifmem(true(),x,l) -> true()
    ifmem(false(),x,l) -> mem(x,l)
    inter(x,nil()) -> nil()
    inter(nil(),x) -> nil()
    inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
    inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
    inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
    inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
    ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
    ifinter(false(),x,l1,l2) -> inter(l1,l2)
   graph:
    ifinter#(false(),x,l1,l2) -> inter#(l1,l2) ->
    inter#(app(l1,l2),l3) -> inter#(l2,l3)
    ifinter#(false(),x,l1,l2) -> inter#(l1,l2) ->
    inter#(app(l1,l2),l3) -> inter#(l1,l3)
    ifinter#(false(),x,l1,l2) -> inter#(l1,l2) ->
    inter#(app(l1,l2),l3) -> app#(inter(l1,l3),inter(l2,l3))
    ifinter#(false(),x,l1,l2) -> inter#(l1,l2) ->
    inter#(l1,app(l2,l3)) -> inter#(l1,l3)
    ifinter#(false(),x,l1,l2) -> inter#(l1,l2) ->
    inter#(l1,app(l2,l3)) -> inter#(l1,l2)
    ifinter#(false(),x,l1,l2) -> inter#(l1,l2) ->
    inter#(l1,app(l2,l3)) -> app#(inter(l1,l2),inter(l1,l3))
    ifinter#(false(),x,l1,l2) -> inter#(l1,l2) ->
    inter#(cons(x,l1),l2) -> mem#(x,l2)
    ifinter#(false(),x,l1,l2) -> inter#(l1,l2) ->
    inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2)
    ifinter#(false(),x,l1,l2) -> inter#(l1,l2) ->
    inter#(l1,cons(x,l2)) -> mem#(x,l1)
    ifinter#(false(),x,l1,l2) -> inter#(l1,l2) ->
    inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1)
    ifinter#(true(),x,l1,l2) -> inter#(l1,l2) ->
    inter#(app(l1,l2),l3) -> inter#(l2,l3)
    ifinter#(true(),x,l1,l2) -> inter#(l1,l2) ->
    inter#(app(l1,l2),l3) -> inter#(l1,l3)
    ifinter#(true(),x,l1,l2) -> inter#(l1,l2) ->
    inter#(app(l1,l2),l3) -> app#(inter(l1,l3),inter(l2,l3))
    ifinter#(true(),x,l1,l2) -> inter#(l1,l2) ->
    inter#(l1,app(l2,l3)) -> inter#(l1,l3)
    ifinter#(true(),x,l1,l2) -> inter#(l1,l2) ->
    inter#(l1,app(l2,l3)) -> inter#(l1,l2)
    ifinter#(true(),x,l1,l2) -> inter#(l1,l2) ->
    inter#(l1,app(l2,l3)) -> app#(inter(l1,l2),inter(l1,l3))
    ifinter#(true(),x,l1,l2) -> inter#(l1,l2) ->
    inter#(cons(x,l1),l2) -> mem#(x,l2)
    ifinter#(true(),x,l1,l2) -> inter#(l1,l2) ->
    inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2)
    ifinter#(true(),x,l1,l2) -> inter#(l1,l2) ->
    inter#(l1,cons(x,l2)) -> mem#(x,l1)
    ifinter#(true(),x,l1,l2) -> inter#(l1,l2) ->
    inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1)
    inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2) ->
    ifinter#(true(),x,l1,l2) -> inter#(l1,l2)
    inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2) ->
    ifinter#(false(),x,l1,l2) -> inter#(l1,l2)
    inter#(cons(x,l1),l2) -> mem#(x,l2) ->
    mem#(x,cons(y,l)) -> eq#(x,y)
    inter#(cons(x,l1),l2) -> mem#(x,l2) ->
    mem#(x,cons(y,l)) -> ifmem#(eq(x,y),x,l)
    inter#(app(l1,l2),l3) -> inter#(l2,l3) ->
    inter#(app(l1,l2),l3) -> inter#(l2,l3)
    inter#(app(l1,l2),l3) -> inter#(l2,l3) ->
    inter#(app(l1,l2),l3) -> inter#(l1,l3)
    inter#(app(l1,l2),l3) -> inter#(l2,l3) ->
    inter#(app(l1,l2),l3) -> app#(inter(l1,l3),inter(l2,l3))
    inter#(app(l1,l2),l3) -> inter#(l2,l3) ->
    inter#(l1,app(l2,l3)) -> inter#(l1,l3)
    inter#(app(l1,l2),l3) -> inter#(l2,l3) ->
    inter#(l1,app(l2,l3)) -> inter#(l1,l2)
    inter#(app(l1,l2),l3) -> inter#(l2,l3) ->
    inter#(l1,app(l2,l3)) -> app#(inter(l1,l2),inter(l1,l3))
    inter#(app(l1,l2),l3) -> inter#(l2,l3) ->
    inter#(cons(x,l1),l2) -> mem#(x,l2)
    inter#(app(l1,l2),l3) -> inter#(l2,l3) ->
    inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2)
    inter#(app(l1,l2),l3) -> inter#(l2,l3) ->
    inter#(l1,cons(x,l2)) -> mem#(x,l1)
    inter#(app(l1,l2),l3) -> inter#(l2,l3) ->
    inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1)
    inter#(app(l1,l2),l3) -> inter#(l1,l3) ->
    inter#(app(l1,l2),l3) -> inter#(l2,l3)
    inter#(app(l1,l2),l3) -> inter#(l1,l3) ->
    inter#(app(l1,l2),l3) -> inter#(l1,l3)
    inter#(app(l1,l2),l3) -> inter#(l1,l3) ->
    inter#(app(l1,l2),l3) -> app#(inter(l1,l3),inter(l2,l3))
    inter#(app(l1,l2),l3) -> inter#(l1,l3) ->
    inter#(l1,app(l2,l3)) -> inter#(l1,l3)
    inter#(app(l1,l2),l3) -> inter#(l1,l3) ->
    inter#(l1,app(l2,l3)) -> inter#(l1,l2)
    inter#(app(l1,l2),l3) -> inter#(l1,l3) ->
    inter#(l1,app(l2,l3)) -> app#(inter(l1,l2),inter(l1,l3))
    inter#(app(l1,l2),l3) -> inter#(l1,l3) ->
    inter#(cons(x,l1),l2) -> mem#(x,l2)
    inter#(app(l1,l2),l3) -> inter#(l1,l3) ->
    inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2)
    inter#(app(l1,l2),l3) -> inter#(l1,l3) ->
    inter#(l1,cons(x,l2)) -> mem#(x,l1)
    inter#(app(l1,l2),l3) -> inter#(l1,l3) ->
    inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1)
    inter#(app(l1,l2),l3) -> app#(inter(l1,l3),inter(l2,l3)) ->
    app#(cons(x,l1),l2) -> app#(l1,l2)
    inter#(app(l1,l2),l3) -> app#(inter(l1,l3),inter(l2,l3)) ->
    app#(app(l1,l2),l3) -> app#(l2,l3)
    inter#(app(l1,l2),l3) -> app#(inter(l1,l3),inter(l2,l3)) ->
    app#(app(l1,l2),l3) -> app#(l1,app(l2,l3))
    inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1) ->
    ifinter#(true(),x,l1,l2) -> inter#(l1,l2)
    inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1) ->
    ifinter#(false(),x,l1,l2) -> inter#(l1,l2)
    inter#(l1,cons(x,l2)) -> mem#(x,l1) ->
    mem#(x,cons(y,l)) -> eq#(x,y)
    inter#(l1,cons(x,l2)) -> mem#(x,l1) ->
    mem#(x,cons(y,l)) -> ifmem#(eq(x,y),x,l)
    inter#(l1,app(l2,l3)) -> inter#(l1,l3) ->
    inter#(app(l1,l2),l3) -> inter#(l2,l3)
    inter#(l1,app(l2,l3)) -> inter#(l1,l3) ->
    inter#(app(l1,l2),l3) -> inter#(l1,l3)
    inter#(l1,app(l2,l3)) -> inter#(l1,l3) ->
    inter#(app(l1,l2),l3) -> app#(inter(l1,l3),inter(l2,l3))
    inter#(l1,app(l2,l3)) -> inter#(l1,l3) ->
    inter#(l1,app(l2,l3)) -> inter#(l1,l3)
    inter#(l1,app(l2,l3)) -> inter#(l1,l3) ->
    inter#(l1,app(l2,l3)) -> inter#(l1,l2)
    inter#(l1,app(l2,l3)) -> inter#(l1,l3) ->
    inter#(l1,app(l2,l3)) -> app#(inter(l1,l2),inter(l1,l3))
    inter#(l1,app(l2,l3)) -> inter#(l1,l3) ->
    inter#(cons(x,l1),l2) -> mem#(x,l2)
    inter#(l1,app(l2,l3)) -> inter#(l1,l3) ->
    inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2)
    inter#(l1,app(l2,l3)) -> inter#(l1,l3) ->
    inter#(l1,cons(x,l2)) -> mem#(x,l1)
    inter#(l1,app(l2,l3)) -> inter#(l1,l3) ->
    inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1)
    inter#(l1,app(l2,l3)) -> inter#(l1,l2) ->
    inter#(app(l1,l2),l3) -> inter#(l2,l3)
    inter#(l1,app(l2,l3)) -> inter#(l1,l2) ->
    inter#(app(l1,l2),l3) -> inter#(l1,l3)
    inter#(l1,app(l2,l3)) -> inter#(l1,l2) ->
    inter#(app(l1,l2),l3) -> app#(inter(l1,l3),inter(l2,l3))
    inter#(l1,app(l2,l3)) -> inter#(l1,l2) ->
    inter#(l1,app(l2,l3)) -> inter#(l1,l3)
    inter#(l1,app(l2,l3)) -> inter#(l1,l2) ->
    inter#(l1,app(l2,l3)) -> inter#(l1,l2)
    inter#(l1,app(l2,l3)) -> inter#(l1,l2) ->
    inter#(l1,app(l2,l3)) -> app#(inter(l1,l2),inter(l1,l3))
    inter#(l1,app(l2,l3)) -> inter#(l1,l2) ->
    inter#(cons(x,l1),l2) -> mem#(x,l2)
    inter#(l1,app(l2,l3)) -> inter#(l1,l2) ->
    inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2)
    inter#(l1,app(l2,l3)) -> inter#(l1,l2) ->
    inter#(l1,cons(x,l2)) -> mem#(x,l1)
    inter#(l1,app(l2,l3)) -> inter#(l1,l2) ->
    inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1)
    inter#(l1,app(l2,l3)) -> app#(inter(l1,l2),inter(l1,l3)) ->
    app#(cons(x,l1),l2) -> app#(l1,l2)
    inter#(l1,app(l2,l3)) -> app#(inter(l1,l2),inter(l1,l3)) ->
    app#(app(l1,l2),l3) -> app#(l2,l3)
    inter#(l1,app(l2,l3)) -> app#(inter(l1,l2),inter(l1,l3)) ->
    app#(app(l1,l2),l3) -> app#(l1,app(l2,l3))
    ifmem#(false(),x,l) -> mem#(x,l) ->
    mem#(x,cons(y,l)) -> eq#(x,y)
    ifmem#(false(),x,l) -> mem#(x,l) ->
    mem#(x,cons(y,l)) -> ifmem#(eq(x,y),x,l)
    mem#(x,cons(y,l)) -> ifmem#(eq(x,y),x,l) ->
    ifmem#(false(),x,l) -> mem#(x,l)
    mem#(x,cons(y,l)) -> eq#(x,y) -> eq#(s(x),s(y)) -> eq#(x,y)
    app#(cons(x,l1),l2) -> app#(l1,l2) ->
    app#(cons(x,l1),l2) -> app#(l1,l2)
    app#(cons(x,l1),l2) -> app#(l1,l2) ->
    app#(app(l1,l2),l3) -> app#(l2,l3)
    app#(cons(x,l1),l2) -> app#(l1,l2) ->
    app#(app(l1,l2),l3) -> app#(l1,app(l2,l3))
    app#(app(l1,l2),l3) -> app#(l2,l3) ->
    app#(cons(x,l1),l2) -> app#(l1,l2)
    app#(app(l1,l2),l3) -> app#(l2,l3) ->
    app#(app(l1,l2),l3) -> app#(l2,l3)
    app#(app(l1,l2),l3) -> app#(l2,l3) ->
    app#(app(l1,l2),l3) -> app#(l1,app(l2,l3))
    app#(app(l1,l2),l3) -> app#(l1,app(l2,l3)) ->
    app#(cons(x,l1),l2) -> app#(l1,l2)
    app#(app(l1,l2),l3) -> app#(l1,app(l2,l3)) ->
    app#(app(l1,l2),l3) -> app#(l2,l3)
    app#(app(l1,l2),l3) -> app#(l1,app(l2,l3)) ->
    app#(app(l1,l2),l3) -> app#(l1,app(l2,l3))
    eq#(s(x),s(y)) -> eq#(x,y) -> eq#(s(x),s(y)) -> eq#(x,y)
   SCC Processor:
    #sccs: 4
    #rules: 14
    #arcs: 88/361
    DPs:
     ifinter#(false(),x,l1,l2) -> inter#(l1,l2)
     inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1)
     ifinter#(true(),x,l1,l2) -> inter#(l1,l2)
     inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2)
     inter#(l1,app(l2,l3)) -> inter#(l1,l2)
     inter#(l1,app(l2,l3)) -> inter#(l1,l3)
     inter#(app(l1,l2),l3) -> inter#(l1,l3)
     inter#(app(l1,l2),l3) -> inter#(l2,l3)
    TRS:
     if(true(),x,y) -> x
     if(false(),x,y) -> y
     eq(0(),0()) -> true()
     eq(0(),s(x)) -> false()
     eq(s(x),0()) -> false()
     eq(s(x),s(y)) -> eq(x,y)
     app(nil(),l) -> l
     app(cons(x,l1),l2) -> cons(x,app(l1,l2))
     app(app(l1,l2),l3) -> app(l1,app(l2,l3))
     mem(x,nil()) -> false()
     mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
     ifmem(true(),x,l) -> true()
     ifmem(false(),x,l) -> mem(x,l)
     inter(x,nil()) -> nil()
     inter(nil(),x) -> nil()
     inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
     inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
     inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
     inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
     ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
     ifinter(false(),x,l1,l2) -> inter(l1,l2)
    Open
    
    DPs:
     app#(app(l1,l2),l3) -> app#(l1,app(l2,l3))
     app#(app(l1,l2),l3) -> app#(l2,l3)
     app#(cons(x,l1),l2) -> app#(l1,l2)
    TRS:
     if(true(),x,y) -> x
     if(false(),x,y) -> y
     eq(0(),0()) -> true()
     eq(0(),s(x)) -> false()
     eq(s(x),0()) -> false()
     eq(s(x),s(y)) -> eq(x,y)
     app(nil(),l) -> l
     app(cons(x,l1),l2) -> cons(x,app(l1,l2))
     app(app(l1,l2),l3) -> app(l1,app(l2,l3))
     mem(x,nil()) -> false()
     mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
     ifmem(true(),x,l) -> true()
     ifmem(false(),x,l) -> mem(x,l)
     inter(x,nil()) -> nil()
     inter(nil(),x) -> nil()
     inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
     inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
     inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
     inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
     ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
     ifinter(false(),x,l1,l2) -> inter(l1,l2)
    Subterm Criterion Processor:
     simple projection:
      pi(app#) = 0
     problem:
      DPs:
       
      TRS:
       if(true(),x,y) -> x
       if(false(),x,y) -> y
       eq(0(),0()) -> true()
       eq(0(),s(x)) -> false()
       eq(s(x),0()) -> false()
       eq(s(x),s(y)) -> eq(x,y)
       app(nil(),l) -> l
       app(cons(x,l1),l2) -> cons(x,app(l1,l2))
       app(app(l1,l2),l3) -> app(l1,app(l2,l3))
       mem(x,nil()) -> false()
       mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
       ifmem(true(),x,l) -> true()
       ifmem(false(),x,l) -> mem(x,l)
       inter(x,nil()) -> nil()
       inter(nil(),x) -> nil()
       inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
       inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
       inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
       inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
       ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
       ifinter(false(),x,l1,l2) -> inter(l1,l2)
     Qed
    
    DPs:
     mem#(x,cons(y,l)) -> ifmem#(eq(x,y),x,l)
     ifmem#(false(),x,l) -> mem#(x,l)
    TRS:
     if(true(),x,y) -> x
     if(false(),x,y) -> y
     eq(0(),0()) -> true()
     eq(0(),s(x)) -> false()
     eq(s(x),0()) -> false()
     eq(s(x),s(y)) -> eq(x,y)
     app(nil(),l) -> l
     app(cons(x,l1),l2) -> cons(x,app(l1,l2))
     app(app(l1,l2),l3) -> app(l1,app(l2,l3))
     mem(x,nil()) -> false()
     mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
     ifmem(true(),x,l) -> true()
     ifmem(false(),x,l) -> mem(x,l)
     inter(x,nil()) -> nil()
     inter(nil(),x) -> nil()
     inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
     inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
     inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
     inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
     ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
     ifinter(false(),x,l1,l2) -> inter(l1,l2)
    Subterm Criterion Processor:
     simple projection:
      pi(mem#) = 1
      pi(ifmem#) = 2
     problem:
      DPs:
       ifmem#(false(),x,l) -> mem#(x,l)
      TRS:
       if(true(),x,y) -> x
       if(false(),x,y) -> y
       eq(0(),0()) -> true()
       eq(0(),s(x)) -> false()
       eq(s(x),0()) -> false()
       eq(s(x),s(y)) -> eq(x,y)
       app(nil(),l) -> l
       app(cons(x,l1),l2) -> cons(x,app(l1,l2))
       app(app(l1,l2),l3) -> app(l1,app(l2,l3))
       mem(x,nil()) -> false()
       mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
       ifmem(true(),x,l) -> true()
       ifmem(false(),x,l) -> mem(x,l)
       inter(x,nil()) -> nil()
       inter(nil(),x) -> nil()
       inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
       inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
       inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
       inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
       ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
       ifinter(false(),x,l1,l2) -> inter(l1,l2)
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [ifmem#](x0, x1, x2) = x0 + 1,
       
       [mem#](x0, x1) = 0,
       
       [ifinter](x0, x1, x2, x3) = 0,
       
       [inter](x0, x1) = 0,
       
       [ifmem](x0, x1, x2) = 1,
       
       [mem](x0, x1) = 1,
       
       [cons](x0, x1) = x1,
       
       [app](x0, x1) = x1,
       
       [nil] = 0,
       
       [s](x0) = 0,
       
       [eq](x0, x1) = 1,
       
       [0] = 0,
       
       [false] = 1,
       
       [if](x0, x1, x2) = x1 + x2,
       
       [true] = 1
      orientation:
       ifmem#(false(),x,l) = 2 >= 0 = mem#(x,l)
       
       if(true(),x,y) = x + y >= x = x
       
       if(false(),x,y) = x + y >= y = y
       
       eq(0(),0()) = 1 >= 1 = true()
       
       eq(0(),s(x)) = 1 >= 1 = false()
       
       eq(s(x),0()) = 1 >= 1 = false()
       
       eq(s(x),s(y)) = 1 >= 1 = eq(x,y)
       
       app(nil(),l) = l >= l = l
       
       app(cons(x,l1),l2) = l2 >= l2 = cons(x,app(l1,l2))
       
       app(app(l1,l2),l3) = l3 >= l3 = app(l1,app(l2,l3))
       
       mem(x,nil()) = 1 >= 1 = false()
       
       mem(x,cons(y,l)) = 1 >= 1 = ifmem(eq(x,y),x,l)
       
       ifmem(true(),x,l) = 1 >= 1 = true()
       
       ifmem(false(),x,l) = 1 >= 1 = mem(x,l)
       
       inter(x,nil()) = 0 >= 0 = nil()
       
       inter(nil(),x) = 0 >= 0 = nil()
       
       inter(app(l1,l2),l3) = 0 >= 0 = app(inter(l1,l3),inter(l2,l3))
       
       inter(l1,app(l2,l3)) = 0 >= 0 = app(inter(l1,l2),inter(l1,l3))
       
       inter(cons(x,l1),l2) = 0 >= 0 = ifinter(mem(x,l2),x,l1,l2)
       
       inter(l1,cons(x,l2)) = 0 >= 0 = ifinter(mem(x,l1),x,l2,l1)
       
       ifinter(true(),x,l1,l2) = 0 >= 0 = cons(x,inter(l1,l2))
       
       ifinter(false(),x,l1,l2) = 0 >= 0 = inter(l1,l2)
      problem:
       DPs:
        
       TRS:
        if(true(),x,y) -> x
        if(false(),x,y) -> y
        eq(0(),0()) -> true()
        eq(0(),s(x)) -> false()
        eq(s(x),0()) -> false()
        eq(s(x),s(y)) -> eq(x,y)
        app(nil(),l) -> l
        app(cons(x,l1),l2) -> cons(x,app(l1,l2))
        app(app(l1,l2),l3) -> app(l1,app(l2,l3))
        mem(x,nil()) -> false()
        mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
        ifmem(true(),x,l) -> true()
        ifmem(false(),x,l) -> mem(x,l)
        inter(x,nil()) -> nil()
        inter(nil(),x) -> nil()
        inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
        inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
        inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
        inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
        ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
        ifinter(false(),x,l1,l2) -> inter(l1,l2)
      Qed
    
    DPs:
     eq#(s(x),s(y)) -> eq#(x,y)
    TRS:
     if(true(),x,y) -> x
     if(false(),x,y) -> y
     eq(0(),0()) -> true()
     eq(0(),s(x)) -> false()
     eq(s(x),0()) -> false()
     eq(s(x),s(y)) -> eq(x,y)
     app(nil(),l) -> l
     app(cons(x,l1),l2) -> cons(x,app(l1,l2))
     app(app(l1,l2),l3) -> app(l1,app(l2,l3))
     mem(x,nil()) -> false()
     mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
     ifmem(true(),x,l) -> true()
     ifmem(false(),x,l) -> mem(x,l)
     inter(x,nil()) -> nil()
     inter(nil(),x) -> nil()
     inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
     inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
     inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
     inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
     ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
     ifinter(false(),x,l1,l2) -> inter(l1,l2)
    Subterm Criterion Processor:
     simple projection:
      pi(eq#) = 1
     problem:
      DPs:
       
      TRS:
       if(true(),x,y) -> x
       if(false(),x,y) -> y
       eq(0(),0()) -> true()
       eq(0(),s(x)) -> false()
       eq(s(x),0()) -> false()
       eq(s(x),s(y)) -> eq(x,y)
       app(nil(),l) -> l
       app(cons(x,l1),l2) -> cons(x,app(l1,l2))
       app(app(l1,l2),l3) -> app(l1,app(l2,l3))
       mem(x,nil()) -> false()
       mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
       ifmem(true(),x,l) -> true()
       ifmem(false(),x,l) -> mem(x,l)
       inter(x,nil()) -> nil()
       inter(nil(),x) -> nil()
       inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
       inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
       inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
       inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
       ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
       ifinter(false(),x,l1,l2) -> inter(l1,l2)
     Qed