YES
Time: 0.026129
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:
  DP:
   {               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)}
  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)}
  EDG:
   {(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)))
    (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)))
    (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#(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))
    (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))
    (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))}
   SCCS (4):
    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 (8):
     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:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [ifinter](x0, x1, x2, x3) = x0,
       
       [if](x0, x1, x2) = x0 + 1,
       
       [ifmem](x0, x1, x2) = x0 + x1 + 1,
       
       [eq](x0, x1) = x0 + 1,
       
       [app](x0, x1) = x0 + x1,
       
       [cons](x0, x1) = x0 + 1,
       
       [mem](x0, x1) = 0,
       
       [inter](x0, x1) = 0,
       
       [s](x0) = 1,
       
       [true] = 1,
       
       [false] = 0,
       
       [0] = 1,
       
       [nil] = 0,
       
       [ifinter#](x0, x1, x2, x3) = x0 + x1 + 1,
       
       [inter#](x0, x1) = x0 + x1
      Strict:
       ifinter#(false(), x, l1, l2) -> inter#(l1, l2)
       1 + 0x + 1l1 + 1l2 >= 0 + 1l1 + 1l2
       ifinter#(true(), x, l1, l2) -> inter#(l1, l2)
       1 + 0x + 1l1 + 1l2 >= 0 + 1l1 + 1l2
       inter#(cons(x, l1), l2) -> ifinter#(mem(x, l2), x, l1, l2)
       1 + 0x + 1l1 + 1l2 >= 1 + 0x + 1l1 + 1l2
       inter#(app(l1, l2), l3) -> inter#(l2, l3)
       0 + 1l1 + 1l2 + 1l3 >= 0 + 1l2 + 1l3
       inter#(app(l1, l2), l3) -> inter#(l1, l3)
       0 + 1l1 + 1l2 + 1l3 >= 0 + 1l1 + 1l3
       inter#(l1, cons(x, l2)) -> ifinter#(mem(x, l1), x, l2, l1)
       1 + 0x + 1l1 + 1l2 >= 1 + 0x + 1l1 + 1l2
       inter#(l1, app(l2, l3)) -> inter#(l1, l3)
       0 + 1l1 + 1l2 + 1l3 >= 0 + 1l1 + 1l3
       inter#(l1, app(l2, l3)) -> inter#(l1, l2)
       0 + 1l1 + 1l2 + 1l3 >= 0 + 1l1 + 1l2
      Weak:
       
     EDG:
      {(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#(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, cons(x, l2)) -> ifinter#(mem(x, l1), x, l2, 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#(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#(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, cons(x, l2)) -> ifinter#(mem(x, l1), x, l2, l1))
       (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#(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#(l1, l3))
       (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#(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, 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#(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#(l1, l3))
       (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#(cons(x, l1), l2) -> ifinter#(mem(x, l2), x, l1, l2))}
      SCCS (1):
       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 (4):
        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#) = 1
         Strict:
          {inter#(l1, app(l2, l3)) -> inter#(l1, l3),
           inter#(app(l1, l2), l3) -> inter#(l1, l3),
           inter#(app(l1, l2), l3) -> inter#(l2, l3)}
         EDG:
          {(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#(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#(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#(l1, app(l2, l3)) -> inter#(l1, l3), inter#(l1, app(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, l3), inter#(app(l1, l2), l3) -> inter#(l2, l3))}
          SCCS (1):
           Scc:
            {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 (3):
            Strict:
             {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#) = 1
             Strict:
              {inter#(app(l1, l2), l3) -> inter#(l1, l3),
               inter#(app(l1, l2), l3) -> inter#(l2, l3)}
             EDG:
              {(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#(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))}
              SCCS (1):
               Scc:
                {inter#(app(l1, l2), l3) -> inter#(l1, l3),
                 inter#(app(l1, l2), l3) -> inter#(l2, l3)}
               SCC (2):
                Strict:
                 {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#(app(l1, l2), l3) -> inter#(l2, l3)}
                 EDG:
                  {(inter#(app(l1, l2), l3) -> inter#(l2, l3), inter#(app(l1, l2), l3) -> inter#(l2, l3))}
                  SCCS (1):
                   Scc:
                    {inter#(app(l1, l2), l3) -> inter#(l2, l3)}
                   SCC (1):
                    Strict:
                     {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:
                      {}
                     Qed
   SCC (2):
    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 (0):
       
       Qed
   SCC (3):
    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 (1):
       Scc:
        {app#(app(l1, l2), l3) -> app#(l1, app(l2, l3)),
         app#(cons(x, l1), l2) -> app#(l1, l2)}
       SCC (2):
        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 (1):
           Scc:
            {app#(cons(x, l1), l2) -> app#(l1, l2)}
           SCC (1):
            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 (1):
    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