YES
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(app(l1, l2), l3) -> app(l1, app(l2, l3)),
                app(nil(), l) -> l,
         app(cons(x, l1), l2) -> cons(x, app(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),
              inter(x, nil()) -> nil(),
       inter(l1, app(l2, l3)) -> app(inter(l1, l2), 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)),
              inter(nil(), x) -> nil(),
       inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2),
   ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2)),
  ifinter(false(), x, l1, l2) -> inter(l1, l2)}
 DP:
  Strict:
   {             eq#(s(x), s(y)) -> eq#(x, y),
           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),
             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#(l1, app(l2, l3)) -> app#(inter(l1, l2), inter(l1, l3)),
         inter#(l1, app(l2, l3)) -> inter#(l1, l2),
         inter#(l1, app(l2, l3)) -> inter#(l1, l3),
         inter#(l1, cons(x, l2)) -> mem#(x, l1),
         inter#(l1, cons(x, l2)) -> ifinter#(mem(x, l1), x, l2, l1),
         inter#(app(l1, l2), l3) -> app#(inter(l1, l3), inter(l2, l3)),
         inter#(app(l1, l2), l3) -> inter#(l1, l3),
         inter#(app(l1, l2), l3) -> inter#(l2, l3),
         inter#(cons(x, l1), l2) -> mem#(x, l2),
         inter#(cons(x, l1), l2) -> ifinter#(mem(x, l2), x, l1, l2),
     ifinter#(true(), x, l1, l2) -> inter#(l1, l2),
    ifinter#(false(), x, l1, l2) -> inter#(l1, l2)}
  Weak:
  {           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(app(l1, l2), l3) -> app(l1, app(l2, l3)),
                 app(nil(), l) -> l,
          app(cons(x, l1), l2) -> cons(x, app(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),
               inter(x, nil()) -> nil(),
        inter(l1, app(l2, l3)) -> app(inter(l1, l2), 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)),
               inter(nil(), x) -> nil(),
        inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2),
    ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2)),
   ifinter(false(), x, l1, l2) -> inter(l1, l2)}
  EDG:
   {(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)))
    (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#(cons(x, l1), l2) -> mem#(x, l2))
    (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, cons(x, l2)) -> ifinter#(mem(x, l1), x, l2, l1))
    (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, 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#(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#(cons(x, l1), l2) -> mem#(x, l2))
    (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, cons(x, l2)) -> ifinter#(mem(x, l1), x, l2, l1))
    (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, 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#(cons(x, l1), l2) -> ifinter#(mem(x, l2), x, l1, l2), ifinter#(false(), 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))
    (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)))
    (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)))
    (mem#(x, cons(y, l)) -> ifmem#(eq(x, y), x, l), ifmem#(false(), x, l) -> mem#(x, l))
    (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#(cons(x, l1), l2) -> mem#(x, l2))
    (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, cons(x, l2)) -> ifinter#(mem(x, l1), x, l2, l1))
    (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, 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)))
    (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#(cons(x, l1), l2) -> mem#(x, l2))
    (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, cons(x, l2)) -> ifinter#(mem(x, l1), x, l2, l1))
    (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, 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#(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#(l1, app(l2, l3)) -> inter#(l1, l2))
    (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, 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#(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#(app(l1, l2), l3) -> inter#(l1, l3))
    (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#(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))
    (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))
    (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))
    (app#(cons(x, l1), l2) -> app#(l1, l2), app#(app(l1, l2), l3) -> app#(l1, app(l2, l3)))
    (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#(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#(l1, app(l2, l3)))
    (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#(cons(x, l1), l2) -> app#(l1, l2))
    (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#(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#(l1, app(l2, l3)) -> inter#(l1, l2))
    (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, 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#(l2, l3), inter#(app(l1, l2), l3) -> app#(inter(l1, 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) -> inter#(l2, 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#(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))
    (mem#(x, cons(y, l)) -> eq#(x, y), eq#(s(x), s(y)) -> eq#(x, y))
    (eq#(s(x), s(y)) -> eq#(x, y), eq#(s(x), s(y)) -> eq#(x, y))}
   SCCS:
    Scc:
     {     inter#(l1, app(l2, l3)) -> inter#(l1, l2),
           inter#(l1, app(l2, l3)) -> inter#(l1, 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#(cons(x, l1), l2) -> ifinter#(mem(x, l2), x, l1, l2),
       ifinter#(true(), x, l1, l2) -> inter#(l1, l2),
      ifinter#(false(), x, l1, l2) -> inter#(l1, l2)}
    Scc:
     {  mem#(x, cons(y, l)) -> ifmem#(eq(x, y), x, l),
      ifmem#(false(), x, l) -> mem#(x, l)}
    Scc:
     {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)}
    Scc:
     {eq#(s(x), s(y)) -> eq#(x, y)}
    SCC:
     Strict:
      {     inter#(l1, app(l2, l3)) -> inter#(l1, l2),
            inter#(l1, app(l2, l3)) -> inter#(l1, 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#(cons(x, l1), l2) -> ifinter#(mem(x, l2), x, l1, l2),
        ifinter#(true(), x, l1, l2) -> inter#(l1, l2),
       ifinter#(false(), x, l1, l2) -> inter#(l1, l2)}
     Weak:
     {           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(app(l1, l2), l3) -> app(l1, app(l2, l3)),
                    app(nil(), l) -> l,
             app(cons(x, l1), l2) -> cons(x, app(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),
                  inter(x, nil()) -> nil(),
           inter(l1, app(l2, l3)) -> app(inter(l1, l2), 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)),
                  inter(nil(), x) -> nil(),
           inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2),
       ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2)),
      ifinter(false(), x, l1, l2) -> inter(l1, l2)}
     POLY:
      Argument Filtering:
       pi(ifinter#) = [2,3], pi(ifinter) = [], pi(inter#) = [0,1], pi(inter) = [], pi(ifmem) = [], pi(mem) = [], pi(cons) = [1], pi(nil) = [], pi(app) = [0,1], pi(s) = [], pi(0) = [], pi(eq) = [], pi(false) = [], pi(true) = [], pi(if) = []
      Usable Rules:
       {}
      Interpretation:
       [ifinter#](x0, x1) = x0 + x1,
       [inter#](x0, x1) = x0 + x1,
       [cons](x0) = x0 + 1,
       [app](x0, x1) = x0 + x1
      Strict:
       {     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),
         ifinter#(true(), x, l1, l2) -> inter#(l1, l2),
        ifinter#(false(), x, l1, l2) -> inter#(l1, l2)}
      Weak:
       {           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(app(l1, l2), l3) -> app(l1, app(l2, l3)),
                      app(nil(), l) -> l,
               app(cons(x, l1), l2) -> cons(x, app(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),
                    inter(x, nil()) -> nil(),
             inter(l1, app(l2, l3)) -> app(inter(l1, l2), 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)),
                    inter(nil(), x) -> nil(),
             inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2),
         ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2)),
        ifinter(false(), x, l1, l2) -> inter(l1, l2)}
      EDG:
       {(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#(l1, app(l2, l3)) -> inter#(l1, l3))
        (ifinter#(true(), x, l1, l2) -> inter#(l1, l2), inter#(l1, app(l2, l3)) -> inter#(l1, l2))
        (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#(l1, app(l2, l3)) -> inter#(l1, l3))
        (inter#(l1, app(l2, l3)) -> inter#(l1, l3), inter#(l1, app(l2, l3)) -> inter#(l1, l2))
        (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#(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#(l1, l3), inter#(l1, app(l2, l3)) -> inter#(l1, l2))
        (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#(app(l1, l2), l3) -> inter#(l1, l3))
        (inter#(app(l1, l2), l3) -> inter#(l1, l3), inter#(app(l1, l2), l3) -> inter#(l2, 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)) -> inter#(l1, 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) -> inter#(l2, 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)) -> inter#(l1, 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) -> inter#(l2, l3))}
       SCCS:
        Scc:
         {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)}
        SCC:
         Strict:
          {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)}
         Weak:
         {           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(app(l1, l2), l3) -> app(l1, app(l2, l3)),
                        app(nil(), l) -> l,
                 app(cons(x, l1), l2) -> cons(x, app(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),
                      inter(x, nil()) -> nil(),
               inter(l1, app(l2, l3)) -> app(inter(l1, l2), 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)),
                      inter(nil(), x) -> nil(),
               inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2),
           ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2)),
          ifinter(false(), x, l1, l2) -> inter(l1, l2)}
         SPSC:
          Simple Projection:
           pi(inter#) = 0
          Strict:
           {inter#(l1, app(l2, l3)) -> inter#(l1, l2),
            inter#(l1, app(l2, l3)) -> inter#(l1, l3),
            inter#(app(l1, l2), l3) -> inter#(l1, l3)}
          EDG:
           {(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#(l1, app(l2, l3)) -> inter#(l1, l3))
            (inter#(l1, app(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)) -> inter#(l1, l2))
            (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#(app(l1, 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)) -> inter#(l1, l3))
            (inter#(l1, app(l2, l3)) -> inter#(l1, l2), inter#(app(l1, l2), l3) -> inter#(l1, l3))}
           SCCS:
            Scc:
             {inter#(l1, app(l2, l3)) -> inter#(l1, l2),
              inter#(l1, app(l2, l3)) -> inter#(l1, l3),
              inter#(app(l1, l2), l3) -> inter#(l1, l3)}
            SCC:
             Strict:
              {inter#(l1, app(l2, l3)) -> inter#(l1, l2),
               inter#(l1, app(l2, l3)) -> inter#(l1, l3),
               inter#(app(l1, l2), l3) -> inter#(l1, l3)}
             Weak:
             {           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(app(l1, l2), l3) -> app(l1, app(l2, l3)),
                            app(nil(), l) -> l,
                     app(cons(x, l1), l2) -> cons(x, app(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),
                          inter(x, nil()) -> nil(),
                   inter(l1, app(l2, l3)) -> app(inter(l1, l2), 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)),
                          inter(nil(), x) -> nil(),
                   inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2),
               ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2)),
              ifinter(false(), x, l1, l2) -> inter(l1, l2)}
             SPSC:
              Simple Projection:
               pi(inter#) = 0
              Strict:
               {inter#(l1, app(l2, l3)) -> inter#(l1, l2),
                inter#(l1, app(l2, l3)) -> inter#(l1, l3)}
              EDG:
               {(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, l2), inter#(l1, app(l2, l3)) -> inter#(l1, l2))
                (inter#(l1, app(l2, l3)) -> inter#(l1, l2), inter#(l1, app(l2, l3)) -> inter#(l1, l3))}
               SCCS:
                Scc:
                 {inter#(l1, app(l2, l3)) -> inter#(l1, l2),
                  inter#(l1, app(l2, l3)) -> inter#(l1, l3)}
                SCC:
                 Strict:
                  {inter#(l1, app(l2, l3)) -> inter#(l1, l2),
                   inter#(l1, app(l2, l3)) -> inter#(l1, l3)}
                 Weak:
                 {           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(app(l1, l2), l3) -> app(l1, app(l2, l3)),
                                app(nil(), l) -> l,
                         app(cons(x, l1), l2) -> cons(x, app(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),
                              inter(x, nil()) -> nil(),
                       inter(l1, app(l2, l3)) -> app(inter(l1, l2), 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)),
                              inter(nil(), x) -> nil(),
                       inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2),
                   ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2)),
                  ifinter(false(), x, l1, l2) -> inter(l1, l2)}
                 SPSC:
                  Simple Projection:
                   pi(inter#) = 1
                  Strict:
                   {inter#(l1, app(l2, l3)) -> inter#(l1, l3)}
                  EDG:
                   {(inter#(l1, app(l2, l3)) -> inter#(l1, l3), inter#(l1, app(l2, l3)) -> inter#(l1, l3))}
                   SCCS:
                    Scc:
                     {inter#(l1, app(l2, l3)) -> inter#(l1, l3)}
                    SCC:
                     Strict:
                      {inter#(l1, app(l2, l3)) -> inter#(l1, l3)}
                     Weak:
                     {           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(app(l1, l2), l3) -> app(l1, app(l2, l3)),
                                    app(nil(), l) -> l,
                             app(cons(x, l1), l2) -> cons(x, app(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),
                                  inter(x, nil()) -> nil(),
                           inter(l1, app(l2, l3)) -> app(inter(l1, l2), 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)),
                                  inter(nil(), x) -> nil(),
                           inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2),
                       ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2)),
                      ifinter(false(), x, l1, l2) -> inter(l1, l2)}
                     SPSC:
                      Simple Projection:
                       pi(inter#) = 1
                      Strict:
                       {}
                      Qed
    SCC:
     Strict:
      {  mem#(x, cons(y, l)) -> ifmem#(eq(x, y), x, l),
       ifmem#(false(), x, l) -> mem#(x, l)}
     Weak:
     {           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(app(l1, l2), l3) -> app(l1, app(l2, l3)),
                    app(nil(), l) -> l,
             app(cons(x, l1), l2) -> cons(x, app(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),
                  inter(x, nil()) -> nil(),
           inter(l1, app(l2, l3)) -> app(inter(l1, l2), 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)),
                  inter(nil(), x) -> nil(),
           inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2),
       ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2)),
      ifinter(false(), x, l1, l2) -> inter(l1, l2)}
     SPSC:
      Simple Projection:
       pi(ifmem#) = 2, pi(mem#) = 1
      Strict:
       {ifmem#(false(), x, l) -> mem#(x, l)}
      EDG:
       {}
       SCCS:
        
        Qed
    SCC:
     Strict:
      {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)}
     Weak:
     {           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(app(l1, l2), l3) -> app(l1, app(l2, l3)),
                    app(nil(), l) -> l,
             app(cons(x, l1), l2) -> cons(x, app(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),
                  inter(x, nil()) -> nil(),
           inter(l1, app(l2, l3)) -> app(inter(l1, l2), 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)),
                  inter(nil(), x) -> nil(),
           inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2),
       ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2)),
      ifinter(false(), x, l1, l2) -> inter(l1, l2)}
     SPSC:
      Simple Projection:
       pi(app#) = 0
      Strict:
       {app#(app(l1, l2), l3) -> app#(l1, app(l2, l3)),
        app#(cons(x, l1), l2) -> app#(l1, l2)}
      EDG:
       {(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#(l1, app(l2, l3)))
        (app#(cons(x, l1), l2) -> app#(l1, l2), app#(app(l1, l2), l3) -> app#(l1, app(l2, l3)))
        (app#(cons(x, l1), l2) -> app#(l1, l2), app#(cons(x, l1), l2) -> app#(l1, l2))}
       SCCS:
        Scc:
         {app#(app(l1, l2), l3) -> app#(l1, app(l2, l3)),
          app#(cons(x, l1), l2) -> app#(l1, l2)}
        SCC:
         Strict:
          {app#(app(l1, l2), l3) -> app#(l1, app(l2, l3)),
           app#(cons(x, l1), l2) -> app#(l1, l2)}
         Weak:
         {           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(app(l1, l2), l3) -> app(l1, app(l2, l3)),
                        app(nil(), l) -> l,
                 app(cons(x, l1), l2) -> cons(x, app(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),
                      inter(x, nil()) -> nil(),
               inter(l1, app(l2, l3)) -> app(inter(l1, l2), 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)),
                      inter(nil(), x) -> nil(),
               inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2),
           ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2)),
          ifinter(false(), x, l1, l2) -> inter(l1, l2)}
         SPSC:
          Simple Projection:
           pi(app#) = 0
          Strict:
           {app#(cons(x, l1), l2) -> app#(l1, l2)}
          EDG:
           {(app#(cons(x, l1), l2) -> app#(l1, l2), app#(cons(x, l1), l2) -> app#(l1, l2))}
           SCCS:
            Scc:
             {app#(cons(x, l1), l2) -> app#(l1, l2)}
            SCC:
             Strict:
              {app#(cons(x, l1), l2) -> app#(l1, l2)}
             Weak:
             {           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(app(l1, l2), l3) -> app(l1, app(l2, l3)),
                            app(nil(), l) -> l,
                     app(cons(x, l1), l2) -> cons(x, app(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),
                          inter(x, nil()) -> nil(),
                   inter(l1, app(l2, l3)) -> app(inter(l1, l2), 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)),
                          inter(nil(), x) -> nil(),
                   inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2),
               ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2)),
              ifinter(false(), x, l1, l2) -> inter(l1, l2)}
             SPSC:
              Simple Projection:
               pi(app#) = 0
              Strict:
               {}
              Qed
    SCC:
     Strict:
      {eq#(s(x), s(y)) -> eq#(x, y)}
     Weak:
     {           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(app(l1, l2), l3) -> app(l1, app(l2, l3)),
                    app(nil(), l) -> l,
             app(cons(x, l1), l2) -> cons(x, app(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),
                  inter(x, nil()) -> nil(),
           inter(l1, app(l2, l3)) -> app(inter(l1, l2), 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)),
                  inter(nil(), x) -> nil(),
           inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2),
       ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2)),
      ifinter(false(), x, l1, l2) -> inter(l1, l2)}
     SPSC:
      Simple Projection:
       pi(eq#) = 1
      Strict:
       {}
      Qed