MAYBE
Time: 0.018541
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))}
   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))}
    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))}
     STATUS:
      arrows: 0.756233
      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:
        {eq#(s x, s y) -> eq#(x, y)}
       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 (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)}
        Open
       
       
       
       
       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)}
        Open
       
       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)}
        Open
       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)}
        Open