YES

We show the termination of the TRS R:

  active(and(true(),X)) -> mark(X)
  active(and(false(),Y)) -> mark(false())
  active(if(true(),X,Y)) -> mark(X)
  active(if(false(),X,Y)) -> mark(Y)
  active(add(|0|(),X)) -> mark(X)
  active(add(s(X),Y)) -> mark(s(add(X,Y)))
  active(first(|0|(),X)) -> mark(nil())
  active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
  active(from(X)) -> mark(cons(X,from(s(X))))
  mark(and(X1,X2)) -> active(and(mark(X1),X2))
  mark(true()) -> active(true())
  mark(false()) -> active(false())
  mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
  mark(add(X1,X2)) -> active(add(mark(X1),X2))
  mark(|0|()) -> active(|0|())
  mark(s(X)) -> active(s(X))
  mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
  mark(nil()) -> active(nil())
  mark(cons(X1,X2)) -> active(cons(X1,X2))
  mark(from(X)) -> active(from(X))
  and(mark(X1),X2) -> and(X1,X2)
  and(X1,mark(X2)) -> and(X1,X2)
  and(active(X1),X2) -> and(X1,X2)
  and(X1,active(X2)) -> and(X1,X2)
  if(mark(X1),X2,X3) -> if(X1,X2,X3)
  if(X1,mark(X2),X3) -> if(X1,X2,X3)
  if(X1,X2,mark(X3)) -> if(X1,X2,X3)
  if(active(X1),X2,X3) -> if(X1,X2,X3)
  if(X1,active(X2),X3) -> if(X1,X2,X3)
  if(X1,X2,active(X3)) -> if(X1,X2,X3)
  add(mark(X1),X2) -> add(X1,X2)
  add(X1,mark(X2)) -> add(X1,X2)
  add(active(X1),X2) -> add(X1,X2)
  add(X1,active(X2)) -> add(X1,X2)
  s(mark(X)) -> s(X)
  s(active(X)) -> s(X)
  first(mark(X1),X2) -> first(X1,X2)
  first(X1,mark(X2)) -> first(X1,X2)
  first(active(X1),X2) -> first(X1,X2)
  first(X1,active(X2)) -> first(X1,X2)
  cons(mark(X1),X2) -> cons(X1,X2)
  cons(X1,mark(X2)) -> cons(X1,X2)
  cons(active(X1),X2) -> cons(X1,X2)
  cons(X1,active(X2)) -> cons(X1,X2)
  from(mark(X)) -> from(X)
  from(active(X)) -> from(X)

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: active#(and(true(),X)) -> mark#(X)
p2: active#(and(false(),Y)) -> mark#(false())
p3: active#(if(true(),X,Y)) -> mark#(X)
p4: active#(if(false(),X,Y)) -> mark#(Y)
p5: active#(add(|0|(),X)) -> mark#(X)
p6: active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
p7: active#(add(s(X),Y)) -> s#(add(X,Y))
p8: active#(add(s(X),Y)) -> add#(X,Y)
p9: active#(first(|0|(),X)) -> mark#(nil())
p10: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
p11: active#(first(s(X),cons(Y,Z))) -> cons#(Y,first(X,Z))
p12: active#(first(s(X),cons(Y,Z))) -> first#(X,Z)
p13: active#(from(X)) -> mark#(cons(X,from(s(X))))
p14: active#(from(X)) -> cons#(X,from(s(X)))
p15: active#(from(X)) -> from#(s(X))
p16: active#(from(X)) -> s#(X)
p17: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p18: mark#(and(X1,X2)) -> and#(mark(X1),X2)
p19: mark#(and(X1,X2)) -> mark#(X1)
p20: mark#(true()) -> active#(true())
p21: mark#(false()) -> active#(false())
p22: mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
p23: mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
p24: mark#(if(X1,X2,X3)) -> mark#(X1)
p25: mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
p26: mark#(add(X1,X2)) -> add#(mark(X1),X2)
p27: mark#(add(X1,X2)) -> mark#(X1)
p28: mark#(|0|()) -> active#(|0|())
p29: mark#(s(X)) -> active#(s(X))
p30: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
p31: mark#(first(X1,X2)) -> first#(mark(X1),mark(X2))
p32: mark#(first(X1,X2)) -> mark#(X1)
p33: mark#(first(X1,X2)) -> mark#(X2)
p34: mark#(nil()) -> active#(nil())
p35: mark#(cons(X1,X2)) -> active#(cons(X1,X2))
p36: mark#(from(X)) -> active#(from(X))
p37: and#(mark(X1),X2) -> and#(X1,X2)
p38: and#(X1,mark(X2)) -> and#(X1,X2)
p39: and#(active(X1),X2) -> and#(X1,X2)
p40: and#(X1,active(X2)) -> and#(X1,X2)
p41: if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
p42: if#(X1,mark(X2),X3) -> if#(X1,X2,X3)
p43: if#(X1,X2,mark(X3)) -> if#(X1,X2,X3)
p44: if#(active(X1),X2,X3) -> if#(X1,X2,X3)
p45: if#(X1,active(X2),X3) -> if#(X1,X2,X3)
p46: if#(X1,X2,active(X3)) -> if#(X1,X2,X3)
p47: add#(mark(X1),X2) -> add#(X1,X2)
p48: add#(X1,mark(X2)) -> add#(X1,X2)
p49: add#(active(X1),X2) -> add#(X1,X2)
p50: add#(X1,active(X2)) -> add#(X1,X2)
p51: s#(mark(X)) -> s#(X)
p52: s#(active(X)) -> s#(X)
p53: first#(mark(X1),X2) -> first#(X1,X2)
p54: first#(X1,mark(X2)) -> first#(X1,X2)
p55: first#(active(X1),X2) -> first#(X1,X2)
p56: first#(X1,active(X2)) -> first#(X1,X2)
p57: cons#(mark(X1),X2) -> cons#(X1,X2)
p58: cons#(X1,mark(X2)) -> cons#(X1,X2)
p59: cons#(active(X1),X2) -> cons#(X1,X2)
p60: cons#(X1,active(X2)) -> cons#(X1,X2)
p61: from#(mark(X)) -> from#(X)
p62: from#(active(X)) -> from#(X)

and R consists of:

r1: active(and(true(),X)) -> mark(X)
r2: active(and(false(),Y)) -> mark(false())
r3: active(if(true(),X,Y)) -> mark(X)
r4: active(if(false(),X,Y)) -> mark(Y)
r5: active(add(|0|(),X)) -> mark(X)
r6: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r7: active(first(|0|(),X)) -> mark(nil())
r8: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r9: active(from(X)) -> mark(cons(X,from(s(X))))
r10: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r11: mark(true()) -> active(true())
r12: mark(false()) -> active(false())
r13: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r14: mark(add(X1,X2)) -> active(add(mark(X1),X2))
r15: mark(|0|()) -> active(|0|())
r16: mark(s(X)) -> active(s(X))
r17: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r18: mark(nil()) -> active(nil())
r19: mark(cons(X1,X2)) -> active(cons(X1,X2))
r20: mark(from(X)) -> active(from(X))
r21: and(mark(X1),X2) -> and(X1,X2)
r22: and(X1,mark(X2)) -> and(X1,X2)
r23: and(active(X1),X2) -> and(X1,X2)
r24: and(X1,active(X2)) -> and(X1,X2)
r25: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r26: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r27: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r28: if(active(X1),X2,X3) -> if(X1,X2,X3)
r29: if(X1,active(X2),X3) -> if(X1,X2,X3)
r30: if(X1,X2,active(X3)) -> if(X1,X2,X3)
r31: add(mark(X1),X2) -> add(X1,X2)
r32: add(X1,mark(X2)) -> add(X1,X2)
r33: add(active(X1),X2) -> add(X1,X2)
r34: add(X1,active(X2)) -> add(X1,X2)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: first(mark(X1),X2) -> first(X1,X2)
r38: first(X1,mark(X2)) -> first(X1,X2)
r39: first(active(X1),X2) -> first(X1,X2)
r40: first(X1,active(X2)) -> first(X1,X2)
r41: cons(mark(X1),X2) -> cons(X1,X2)
r42: cons(X1,mark(X2)) -> cons(X1,X2)
r43: cons(active(X1),X2) -> cons(X1,X2)
r44: cons(X1,active(X2)) -> cons(X1,X2)
r45: from(mark(X)) -> from(X)
r46: from(active(X)) -> from(X)

The estimated dependency graph contains the following SCCs:

  {p1, p3, p4, p5, p6, p10, p13, p17, p19, p22, p24, p25, p27, p29, p30, p32, p33, p35, p36}
  {p51, p52}
  {p47, p48, p49, p50}
  {p57, p58, p59, p60}
  {p53, p54, p55, p56}
  {p61, p62}
  {p37, p38, p39, p40}
  {p41, p42, p43, p44, p45, p46}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: active#(and(true(),X)) -> mark#(X)
p2: mark#(from(X)) -> active#(from(X))
p3: active#(from(X)) -> mark#(cons(X,from(s(X))))
p4: mark#(cons(X1,X2)) -> active#(cons(X1,X2))
p5: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
p6: mark#(first(X1,X2)) -> mark#(X2)
p7: mark#(first(X1,X2)) -> mark#(X1)
p8: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
p9: active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
p10: mark#(s(X)) -> active#(s(X))
p11: active#(add(|0|(),X)) -> mark#(X)
p12: mark#(add(X1,X2)) -> mark#(X1)
p13: mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
p14: active#(if(false(),X,Y)) -> mark#(Y)
p15: mark#(if(X1,X2,X3)) -> mark#(X1)
p16: mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
p17: active#(if(true(),X,Y)) -> mark#(X)
p18: mark#(and(X1,X2)) -> mark#(X1)
p19: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))

and R consists of:

r1: active(and(true(),X)) -> mark(X)
r2: active(and(false(),Y)) -> mark(false())
r3: active(if(true(),X,Y)) -> mark(X)
r4: active(if(false(),X,Y)) -> mark(Y)
r5: active(add(|0|(),X)) -> mark(X)
r6: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r7: active(first(|0|(),X)) -> mark(nil())
r8: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r9: active(from(X)) -> mark(cons(X,from(s(X))))
r10: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r11: mark(true()) -> active(true())
r12: mark(false()) -> active(false())
r13: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r14: mark(add(X1,X2)) -> active(add(mark(X1),X2))
r15: mark(|0|()) -> active(|0|())
r16: mark(s(X)) -> active(s(X))
r17: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r18: mark(nil()) -> active(nil())
r19: mark(cons(X1,X2)) -> active(cons(X1,X2))
r20: mark(from(X)) -> active(from(X))
r21: and(mark(X1),X2) -> and(X1,X2)
r22: and(X1,mark(X2)) -> and(X1,X2)
r23: and(active(X1),X2) -> and(X1,X2)
r24: and(X1,active(X2)) -> and(X1,X2)
r25: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r26: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r27: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r28: if(active(X1),X2,X3) -> if(X1,X2,X3)
r29: if(X1,active(X2),X3) -> if(X1,X2,X3)
r30: if(X1,X2,active(X3)) -> if(X1,X2,X3)
r31: add(mark(X1),X2) -> add(X1,X2)
r32: add(X1,mark(X2)) -> add(X1,X2)
r33: add(active(X1),X2) -> add(X1,X2)
r34: add(X1,active(X2)) -> add(X1,X2)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: first(mark(X1),X2) -> first(X1,X2)
r38: first(X1,mark(X2)) -> first(X1,X2)
r39: first(active(X1),X2) -> first(X1,X2)
r40: first(X1,active(X2)) -> first(X1,X2)
r41: cons(mark(X1),X2) -> cons(X1,X2)
r42: cons(X1,mark(X2)) -> cons(X1,X2)
r43: cons(active(X1),X2) -> cons(X1,X2)
r44: cons(X1,active(X2)) -> cons(X1,X2)
r45: from(mark(X)) -> from(X)
r46: from(active(X)) -> from(X)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      active#_A(x1) = x1 + (0,0,4)
      and_A(x1,x2) = x1 + x2 + (0,1,1)
      true_A() = (2,1,1)
      mark#_A(x1) = ((1,0,0),(0,0,0),(1,0,0)) x1 + (1,0,0)
      from_A(x1) = ((1,0,0),(1,0,0),(0,0,0)) x1 + (3,1,1)
      cons_A(x1,x2) = x1 + (1,1,1)
      s_A(x1) = (5,1,1)
      first_A(x1,x2) = ((1,0,0),(0,0,0),(1,0,0)) x1 + ((1,0,0),(1,0,0),(1,0,0)) x2 + (1,1,1)
      mark_A(x1) = x1 + (0,1,1)
      add_A(x1,x2) = ((1,0,0),(1,0,0),(0,0,0)) x1 + x2 + (5,1,1)
      |0|_A() = (1,1,1)
      if_A(x1,x2,x3) = x1 + x2 + ((1,0,0),(1,0,0),(0,0,0)) x3 + (5,1,1)
      false_A() = (1,1,1)
      active_A(x1) = x1 + (0,1,1)
      nil_A() = (2,1,1)

The next rules are strictly ordered:

  p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p19

We remove them from the problem.

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: mark#(and(X1,X2)) -> mark#(X1)

and R consists of:

r1: active(and(true(),X)) -> mark(X)
r2: active(and(false(),Y)) -> mark(false())
r3: active(if(true(),X,Y)) -> mark(X)
r4: active(if(false(),X,Y)) -> mark(Y)
r5: active(add(|0|(),X)) -> mark(X)
r6: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r7: active(first(|0|(),X)) -> mark(nil())
r8: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r9: active(from(X)) -> mark(cons(X,from(s(X))))
r10: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r11: mark(true()) -> active(true())
r12: mark(false()) -> active(false())
r13: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r14: mark(add(X1,X2)) -> active(add(mark(X1),X2))
r15: mark(|0|()) -> active(|0|())
r16: mark(s(X)) -> active(s(X))
r17: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r18: mark(nil()) -> active(nil())
r19: mark(cons(X1,X2)) -> active(cons(X1,X2))
r20: mark(from(X)) -> active(from(X))
r21: and(mark(X1),X2) -> and(X1,X2)
r22: and(X1,mark(X2)) -> and(X1,X2)
r23: and(active(X1),X2) -> and(X1,X2)
r24: and(X1,active(X2)) -> and(X1,X2)
r25: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r26: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r27: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r28: if(active(X1),X2,X3) -> if(X1,X2,X3)
r29: if(X1,active(X2),X3) -> if(X1,X2,X3)
r30: if(X1,X2,active(X3)) -> if(X1,X2,X3)
r31: add(mark(X1),X2) -> add(X1,X2)
r32: add(X1,mark(X2)) -> add(X1,X2)
r33: add(active(X1),X2) -> add(X1,X2)
r34: add(X1,active(X2)) -> add(X1,X2)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: first(mark(X1),X2) -> first(X1,X2)
r38: first(X1,mark(X2)) -> first(X1,X2)
r39: first(active(X1),X2) -> first(X1,X2)
r40: first(X1,active(X2)) -> first(X1,X2)
r41: cons(mark(X1),X2) -> cons(X1,X2)
r42: cons(X1,mark(X2)) -> cons(X1,X2)
r43: cons(active(X1),X2) -> cons(X1,X2)
r44: cons(X1,active(X2)) -> cons(X1,X2)
r45: from(mark(X)) -> from(X)
r46: from(active(X)) -> from(X)

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: mark#(and(X1,X2)) -> mark#(X1)

and R consists of:

r1: active(and(true(),X)) -> mark(X)
r2: active(and(false(),Y)) -> mark(false())
r3: active(if(true(),X,Y)) -> mark(X)
r4: active(if(false(),X,Y)) -> mark(Y)
r5: active(add(|0|(),X)) -> mark(X)
r6: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r7: active(first(|0|(),X)) -> mark(nil())
r8: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r9: active(from(X)) -> mark(cons(X,from(s(X))))
r10: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r11: mark(true()) -> active(true())
r12: mark(false()) -> active(false())
r13: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r14: mark(add(X1,X2)) -> active(add(mark(X1),X2))
r15: mark(|0|()) -> active(|0|())
r16: mark(s(X)) -> active(s(X))
r17: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r18: mark(nil()) -> active(nil())
r19: mark(cons(X1,X2)) -> active(cons(X1,X2))
r20: mark(from(X)) -> active(from(X))
r21: and(mark(X1),X2) -> and(X1,X2)
r22: and(X1,mark(X2)) -> and(X1,X2)
r23: and(active(X1),X2) -> and(X1,X2)
r24: and(X1,active(X2)) -> and(X1,X2)
r25: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r26: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r27: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r28: if(active(X1),X2,X3) -> if(X1,X2,X3)
r29: if(X1,active(X2),X3) -> if(X1,X2,X3)
r30: if(X1,X2,active(X3)) -> if(X1,X2,X3)
r31: add(mark(X1),X2) -> add(X1,X2)
r32: add(X1,mark(X2)) -> add(X1,X2)
r33: add(active(X1),X2) -> add(X1,X2)
r34: add(X1,active(X2)) -> add(X1,X2)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: first(mark(X1),X2) -> first(X1,X2)
r38: first(X1,mark(X2)) -> first(X1,X2)
r39: first(active(X1),X2) -> first(X1,X2)
r40: first(X1,active(X2)) -> first(X1,X2)
r41: cons(mark(X1),X2) -> cons(X1,X2)
r42: cons(X1,mark(X2)) -> cons(X1,X2)
r43: cons(active(X1),X2) -> cons(X1,X2)
r44: cons(X1,active(X2)) -> cons(X1,X2)
r45: from(mark(X)) -> from(X)
r46: from(active(X)) -> from(X)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      mark#_A(x1) = ((1,0,0),(0,0,0),(1,1,0)) x1
      and_A(x1,x2) = ((1,0,0),(1,1,0),(1,1,1)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2 + (1,1,1)

The next rules are strictly ordered:

  p1

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: s#(mark(X)) -> s#(X)
p2: s#(active(X)) -> s#(X)

and R consists of:

r1: active(and(true(),X)) -> mark(X)
r2: active(and(false(),Y)) -> mark(false())
r3: active(if(true(),X,Y)) -> mark(X)
r4: active(if(false(),X,Y)) -> mark(Y)
r5: active(add(|0|(),X)) -> mark(X)
r6: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r7: active(first(|0|(),X)) -> mark(nil())
r8: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r9: active(from(X)) -> mark(cons(X,from(s(X))))
r10: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r11: mark(true()) -> active(true())
r12: mark(false()) -> active(false())
r13: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r14: mark(add(X1,X2)) -> active(add(mark(X1),X2))
r15: mark(|0|()) -> active(|0|())
r16: mark(s(X)) -> active(s(X))
r17: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r18: mark(nil()) -> active(nil())
r19: mark(cons(X1,X2)) -> active(cons(X1,X2))
r20: mark(from(X)) -> active(from(X))
r21: and(mark(X1),X2) -> and(X1,X2)
r22: and(X1,mark(X2)) -> and(X1,X2)
r23: and(active(X1),X2) -> and(X1,X2)
r24: and(X1,active(X2)) -> and(X1,X2)
r25: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r26: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r27: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r28: if(active(X1),X2,X3) -> if(X1,X2,X3)
r29: if(X1,active(X2),X3) -> if(X1,X2,X3)
r30: if(X1,X2,active(X3)) -> if(X1,X2,X3)
r31: add(mark(X1),X2) -> add(X1,X2)
r32: add(X1,mark(X2)) -> add(X1,X2)
r33: add(active(X1),X2) -> add(X1,X2)
r34: add(X1,active(X2)) -> add(X1,X2)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: first(mark(X1),X2) -> first(X1,X2)
r38: first(X1,mark(X2)) -> first(X1,X2)
r39: first(active(X1),X2) -> first(X1,X2)
r40: first(X1,active(X2)) -> first(X1,X2)
r41: cons(mark(X1),X2) -> cons(X1,X2)
r42: cons(X1,mark(X2)) -> cons(X1,X2)
r43: cons(active(X1),X2) -> cons(X1,X2)
r44: cons(X1,active(X2)) -> cons(X1,X2)
r45: from(mark(X)) -> from(X)
r46: from(active(X)) -> from(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      s#_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1
      mark_A(x1) = ((1,0,0),(0,1,0),(1,1,1)) x1 + (1,1,1)
      active_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)

The next rules are strictly ordered:

  p1, p2
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: add#(mark(X1),X2) -> add#(X1,X2)
p2: add#(X1,active(X2)) -> add#(X1,X2)
p3: add#(active(X1),X2) -> add#(X1,X2)
p4: add#(X1,mark(X2)) -> add#(X1,X2)

and R consists of:

r1: active(and(true(),X)) -> mark(X)
r2: active(and(false(),Y)) -> mark(false())
r3: active(if(true(),X,Y)) -> mark(X)
r4: active(if(false(),X,Y)) -> mark(Y)
r5: active(add(|0|(),X)) -> mark(X)
r6: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r7: active(first(|0|(),X)) -> mark(nil())
r8: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r9: active(from(X)) -> mark(cons(X,from(s(X))))
r10: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r11: mark(true()) -> active(true())
r12: mark(false()) -> active(false())
r13: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r14: mark(add(X1,X2)) -> active(add(mark(X1),X2))
r15: mark(|0|()) -> active(|0|())
r16: mark(s(X)) -> active(s(X))
r17: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r18: mark(nil()) -> active(nil())
r19: mark(cons(X1,X2)) -> active(cons(X1,X2))
r20: mark(from(X)) -> active(from(X))
r21: and(mark(X1),X2) -> and(X1,X2)
r22: and(X1,mark(X2)) -> and(X1,X2)
r23: and(active(X1),X2) -> and(X1,X2)
r24: and(X1,active(X2)) -> and(X1,X2)
r25: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r26: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r27: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r28: if(active(X1),X2,X3) -> if(X1,X2,X3)
r29: if(X1,active(X2),X3) -> if(X1,X2,X3)
r30: if(X1,X2,active(X3)) -> if(X1,X2,X3)
r31: add(mark(X1),X2) -> add(X1,X2)
r32: add(X1,mark(X2)) -> add(X1,X2)
r33: add(active(X1),X2) -> add(X1,X2)
r34: add(X1,active(X2)) -> add(X1,X2)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: first(mark(X1),X2) -> first(X1,X2)
r38: first(X1,mark(X2)) -> first(X1,X2)
r39: first(active(X1),X2) -> first(X1,X2)
r40: first(X1,active(X2)) -> first(X1,X2)
r41: cons(mark(X1),X2) -> cons(X1,X2)
r42: cons(X1,mark(X2)) -> cons(X1,X2)
r43: cons(active(X1),X2) -> cons(X1,X2)
r44: cons(X1,active(X2)) -> cons(X1,X2)
r45: from(mark(X)) -> from(X)
r46: from(active(X)) -> from(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      add#_A(x1,x2) = ((1,0,0),(0,1,0),(1,1,1)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2
      mark_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)
      active_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)

The next rules are strictly ordered:

  p1, p2, p3, p4
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: cons#(mark(X1),X2) -> cons#(X1,X2)
p2: cons#(X1,active(X2)) -> cons#(X1,X2)
p3: cons#(active(X1),X2) -> cons#(X1,X2)
p4: cons#(X1,mark(X2)) -> cons#(X1,X2)

and R consists of:

r1: active(and(true(),X)) -> mark(X)
r2: active(and(false(),Y)) -> mark(false())
r3: active(if(true(),X,Y)) -> mark(X)
r4: active(if(false(),X,Y)) -> mark(Y)
r5: active(add(|0|(),X)) -> mark(X)
r6: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r7: active(first(|0|(),X)) -> mark(nil())
r8: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r9: active(from(X)) -> mark(cons(X,from(s(X))))
r10: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r11: mark(true()) -> active(true())
r12: mark(false()) -> active(false())
r13: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r14: mark(add(X1,X2)) -> active(add(mark(X1),X2))
r15: mark(|0|()) -> active(|0|())
r16: mark(s(X)) -> active(s(X))
r17: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r18: mark(nil()) -> active(nil())
r19: mark(cons(X1,X2)) -> active(cons(X1,X2))
r20: mark(from(X)) -> active(from(X))
r21: and(mark(X1),X2) -> and(X1,X2)
r22: and(X1,mark(X2)) -> and(X1,X2)
r23: and(active(X1),X2) -> and(X1,X2)
r24: and(X1,active(X2)) -> and(X1,X2)
r25: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r26: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r27: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r28: if(active(X1),X2,X3) -> if(X1,X2,X3)
r29: if(X1,active(X2),X3) -> if(X1,X2,X3)
r30: if(X1,X2,active(X3)) -> if(X1,X2,X3)
r31: add(mark(X1),X2) -> add(X1,X2)
r32: add(X1,mark(X2)) -> add(X1,X2)
r33: add(active(X1),X2) -> add(X1,X2)
r34: add(X1,active(X2)) -> add(X1,X2)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: first(mark(X1),X2) -> first(X1,X2)
r38: first(X1,mark(X2)) -> first(X1,X2)
r39: first(active(X1),X2) -> first(X1,X2)
r40: first(X1,active(X2)) -> first(X1,X2)
r41: cons(mark(X1),X2) -> cons(X1,X2)
r42: cons(X1,mark(X2)) -> cons(X1,X2)
r43: cons(active(X1),X2) -> cons(X1,X2)
r44: cons(X1,active(X2)) -> cons(X1,X2)
r45: from(mark(X)) -> from(X)
r46: from(active(X)) -> from(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      cons#_A(x1,x2) = ((1,0,0),(1,1,0),(1,1,1)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2
      mark_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)
      active_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)

The next rules are strictly ordered:

  p1, p2, p3, p4
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: first#(mark(X1),X2) -> first#(X1,X2)
p2: first#(X1,active(X2)) -> first#(X1,X2)
p3: first#(active(X1),X2) -> first#(X1,X2)
p4: first#(X1,mark(X2)) -> first#(X1,X2)

and R consists of:

r1: active(and(true(),X)) -> mark(X)
r2: active(and(false(),Y)) -> mark(false())
r3: active(if(true(),X,Y)) -> mark(X)
r4: active(if(false(),X,Y)) -> mark(Y)
r5: active(add(|0|(),X)) -> mark(X)
r6: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r7: active(first(|0|(),X)) -> mark(nil())
r8: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r9: active(from(X)) -> mark(cons(X,from(s(X))))
r10: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r11: mark(true()) -> active(true())
r12: mark(false()) -> active(false())
r13: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r14: mark(add(X1,X2)) -> active(add(mark(X1),X2))
r15: mark(|0|()) -> active(|0|())
r16: mark(s(X)) -> active(s(X))
r17: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r18: mark(nil()) -> active(nil())
r19: mark(cons(X1,X2)) -> active(cons(X1,X2))
r20: mark(from(X)) -> active(from(X))
r21: and(mark(X1),X2) -> and(X1,X2)
r22: and(X1,mark(X2)) -> and(X1,X2)
r23: and(active(X1),X2) -> and(X1,X2)
r24: and(X1,active(X2)) -> and(X1,X2)
r25: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r26: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r27: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r28: if(active(X1),X2,X3) -> if(X1,X2,X3)
r29: if(X1,active(X2),X3) -> if(X1,X2,X3)
r30: if(X1,X2,active(X3)) -> if(X1,X2,X3)
r31: add(mark(X1),X2) -> add(X1,X2)
r32: add(X1,mark(X2)) -> add(X1,X2)
r33: add(active(X1),X2) -> add(X1,X2)
r34: add(X1,active(X2)) -> add(X1,X2)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: first(mark(X1),X2) -> first(X1,X2)
r38: first(X1,mark(X2)) -> first(X1,X2)
r39: first(active(X1),X2) -> first(X1,X2)
r40: first(X1,active(X2)) -> first(X1,X2)
r41: cons(mark(X1),X2) -> cons(X1,X2)
r42: cons(X1,mark(X2)) -> cons(X1,X2)
r43: cons(active(X1),X2) -> cons(X1,X2)
r44: cons(X1,active(X2)) -> cons(X1,X2)
r45: from(mark(X)) -> from(X)
r46: from(active(X)) -> from(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      first#_A(x1,x2) = ((1,0,0),(1,1,0),(1,1,1)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2
      mark_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)
      active_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)

The next rules are strictly ordered:

  p1, p2, p3, p4
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: from#(mark(X)) -> from#(X)
p2: from#(active(X)) -> from#(X)

and R consists of:

r1: active(and(true(),X)) -> mark(X)
r2: active(and(false(),Y)) -> mark(false())
r3: active(if(true(),X,Y)) -> mark(X)
r4: active(if(false(),X,Y)) -> mark(Y)
r5: active(add(|0|(),X)) -> mark(X)
r6: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r7: active(first(|0|(),X)) -> mark(nil())
r8: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r9: active(from(X)) -> mark(cons(X,from(s(X))))
r10: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r11: mark(true()) -> active(true())
r12: mark(false()) -> active(false())
r13: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r14: mark(add(X1,X2)) -> active(add(mark(X1),X2))
r15: mark(|0|()) -> active(|0|())
r16: mark(s(X)) -> active(s(X))
r17: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r18: mark(nil()) -> active(nil())
r19: mark(cons(X1,X2)) -> active(cons(X1,X2))
r20: mark(from(X)) -> active(from(X))
r21: and(mark(X1),X2) -> and(X1,X2)
r22: and(X1,mark(X2)) -> and(X1,X2)
r23: and(active(X1),X2) -> and(X1,X2)
r24: and(X1,active(X2)) -> and(X1,X2)
r25: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r26: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r27: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r28: if(active(X1),X2,X3) -> if(X1,X2,X3)
r29: if(X1,active(X2),X3) -> if(X1,X2,X3)
r30: if(X1,X2,active(X3)) -> if(X1,X2,X3)
r31: add(mark(X1),X2) -> add(X1,X2)
r32: add(X1,mark(X2)) -> add(X1,X2)
r33: add(active(X1),X2) -> add(X1,X2)
r34: add(X1,active(X2)) -> add(X1,X2)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: first(mark(X1),X2) -> first(X1,X2)
r38: first(X1,mark(X2)) -> first(X1,X2)
r39: first(active(X1),X2) -> first(X1,X2)
r40: first(X1,active(X2)) -> first(X1,X2)
r41: cons(mark(X1),X2) -> cons(X1,X2)
r42: cons(X1,mark(X2)) -> cons(X1,X2)
r43: cons(active(X1),X2) -> cons(X1,X2)
r44: cons(X1,active(X2)) -> cons(X1,X2)
r45: from(mark(X)) -> from(X)
r46: from(active(X)) -> from(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      from#_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1
      mark_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)
      active_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)

The next rules are strictly ordered:

  p1, p2
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: and#(mark(X1),X2) -> and#(X1,X2)
p2: and#(X1,active(X2)) -> and#(X1,X2)
p3: and#(active(X1),X2) -> and#(X1,X2)
p4: and#(X1,mark(X2)) -> and#(X1,X2)

and R consists of:

r1: active(and(true(),X)) -> mark(X)
r2: active(and(false(),Y)) -> mark(false())
r3: active(if(true(),X,Y)) -> mark(X)
r4: active(if(false(),X,Y)) -> mark(Y)
r5: active(add(|0|(),X)) -> mark(X)
r6: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r7: active(first(|0|(),X)) -> mark(nil())
r8: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r9: active(from(X)) -> mark(cons(X,from(s(X))))
r10: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r11: mark(true()) -> active(true())
r12: mark(false()) -> active(false())
r13: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r14: mark(add(X1,X2)) -> active(add(mark(X1),X2))
r15: mark(|0|()) -> active(|0|())
r16: mark(s(X)) -> active(s(X))
r17: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r18: mark(nil()) -> active(nil())
r19: mark(cons(X1,X2)) -> active(cons(X1,X2))
r20: mark(from(X)) -> active(from(X))
r21: and(mark(X1),X2) -> and(X1,X2)
r22: and(X1,mark(X2)) -> and(X1,X2)
r23: and(active(X1),X2) -> and(X1,X2)
r24: and(X1,active(X2)) -> and(X1,X2)
r25: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r26: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r27: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r28: if(active(X1),X2,X3) -> if(X1,X2,X3)
r29: if(X1,active(X2),X3) -> if(X1,X2,X3)
r30: if(X1,X2,active(X3)) -> if(X1,X2,X3)
r31: add(mark(X1),X2) -> add(X1,X2)
r32: add(X1,mark(X2)) -> add(X1,X2)
r33: add(active(X1),X2) -> add(X1,X2)
r34: add(X1,active(X2)) -> add(X1,X2)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: first(mark(X1),X2) -> first(X1,X2)
r38: first(X1,mark(X2)) -> first(X1,X2)
r39: first(active(X1),X2) -> first(X1,X2)
r40: first(X1,active(X2)) -> first(X1,X2)
r41: cons(mark(X1),X2) -> cons(X1,X2)
r42: cons(X1,mark(X2)) -> cons(X1,X2)
r43: cons(active(X1),X2) -> cons(X1,X2)
r44: cons(X1,active(X2)) -> cons(X1,X2)
r45: from(mark(X)) -> from(X)
r46: from(active(X)) -> from(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      and#_A(x1,x2) = ((1,0,0),(0,1,0),(1,1,1)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2
      mark_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)
      active_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)

The next rules are strictly ordered:

  p1, p2, p3, p4
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
p2: if#(X1,X2,active(X3)) -> if#(X1,X2,X3)
p3: if#(X1,active(X2),X3) -> if#(X1,X2,X3)
p4: if#(active(X1),X2,X3) -> if#(X1,X2,X3)
p5: if#(X1,X2,mark(X3)) -> if#(X1,X2,X3)
p6: if#(X1,mark(X2),X3) -> if#(X1,X2,X3)

and R consists of:

r1: active(and(true(),X)) -> mark(X)
r2: active(and(false(),Y)) -> mark(false())
r3: active(if(true(),X,Y)) -> mark(X)
r4: active(if(false(),X,Y)) -> mark(Y)
r5: active(add(|0|(),X)) -> mark(X)
r6: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r7: active(first(|0|(),X)) -> mark(nil())
r8: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r9: active(from(X)) -> mark(cons(X,from(s(X))))
r10: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r11: mark(true()) -> active(true())
r12: mark(false()) -> active(false())
r13: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r14: mark(add(X1,X2)) -> active(add(mark(X1),X2))
r15: mark(|0|()) -> active(|0|())
r16: mark(s(X)) -> active(s(X))
r17: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r18: mark(nil()) -> active(nil())
r19: mark(cons(X1,X2)) -> active(cons(X1,X2))
r20: mark(from(X)) -> active(from(X))
r21: and(mark(X1),X2) -> and(X1,X2)
r22: and(X1,mark(X2)) -> and(X1,X2)
r23: and(active(X1),X2) -> and(X1,X2)
r24: and(X1,active(X2)) -> and(X1,X2)
r25: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r26: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r27: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r28: if(active(X1),X2,X3) -> if(X1,X2,X3)
r29: if(X1,active(X2),X3) -> if(X1,X2,X3)
r30: if(X1,X2,active(X3)) -> if(X1,X2,X3)
r31: add(mark(X1),X2) -> add(X1,X2)
r32: add(X1,mark(X2)) -> add(X1,X2)
r33: add(active(X1),X2) -> add(X1,X2)
r34: add(X1,active(X2)) -> add(X1,X2)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: first(mark(X1),X2) -> first(X1,X2)
r38: first(X1,mark(X2)) -> first(X1,X2)
r39: first(active(X1),X2) -> first(X1,X2)
r40: first(X1,active(X2)) -> first(X1,X2)
r41: cons(mark(X1),X2) -> cons(X1,X2)
r42: cons(X1,mark(X2)) -> cons(X1,X2)
r43: cons(active(X1),X2) -> cons(X1,X2)
r44: cons(X1,active(X2)) -> cons(X1,X2)
r45: from(mark(X)) -> from(X)
r46: from(active(X)) -> from(X)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      if#_A(x1,x2,x3) = ((1,0,0),(1,1,0),(1,1,1)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2 + ((1,0,0),(1,1,0),(1,1,0)) x3
      mark_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)
      active_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)

The next rules are strictly ordered:

  p1, p2, p3, p4, p5, p6

We remove them from the problem.  Then no dependency pair remains.