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)
  Usable Rule 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:
    f20(x,y) -> x
    f20(x,y) -> 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))
    eq(0(),0()) -> true()
    eq(0(),s(x)) -> false()
    eq(s(x),0()) -> false()
    eq(s(x),s(y)) -> eq(x,y)
    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)
    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)
   ADG 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:
     f20(x,y) -> x
     f20(x,y) -> 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))
     eq(0(),0()) -> true()
     eq(0(),s(x)) -> false()
     eq(s(x),0()) -> false()
     eq(s(x),s(y)) -> eq(x,y)
     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)
     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)
    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)
    Restore Modifier:
     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)
     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)
      Open
      
      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)
      Open
      
      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)
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [eq#](x0, x1) = x1 + 1,
        
        [ifinter](x0, x1, x2, x3) = 0,
        
        [inter](x0, x1) = 0,
        
        [ifmem](x0, x1, x2) = 0,
        
        [mem](x0, x1) = 0,
        
        [cons](x0, x1) = x1,
        
        [app](x0, x1) = x1,
        
        [nil] = 0,
        
        [s](x0) = x0 + 1,
        
        [eq](x0, x1) = 0,
        
        [0] = 0,
        
        [false] = 0,
        
        [if](x0, x1, x2) = x1 + x2,
        
        [true] = 0
       orientation:
        eq#(s(x),s(y)) = y + 2 >= y + 1 = eq#(x,y)
        
        if(true(),x,y) = x + y >= x = x
        
        if(false(),x,y) = x + y >= y = y
        
        eq(0(),0()) = 0 >= 0 = true()
        
        eq(0(),s(x)) = 0 >= 0 = false()
        
        eq(s(x),0()) = 0 >= 0 = false()
        
        eq(s(x),s(y)) = 0 >= 0 = 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()) = 0 >= 0 = false()
        
        mem(x,cons(y,l)) = 0 >= 0 = ifmem(eq(x,y),x,l)
        
        ifmem(true(),x,l) = 0 >= 0 = true()
        
        ifmem(false(),x,l) = 0 >= 0 = 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