YES

We show the termination of the TRS R:

  if(true(),t,e) -> t
  if(false(),t,e) -> e
  member(x,nil()) -> false()
  member(x,cons(y,ys)) -> if(eq(x,y),true(),member(x,ys))
  eq(nil(),nil()) -> true()
  eq(O(x),|0|(y)) -> eq(x,y)
  eq(|0|(x),|1|(y)) -> false()
  eq(|1|(x),|0|(y)) -> false()
  eq(|1|(x),|1|(y)) -> eq(x,y)
  negate(|0|(x)) -> |1|(x)
  negate(|1|(x)) -> |0|(x)
  choice(cons(x,xs)) -> x
  choice(cons(x,xs)) -> choice(xs)
  guess(nil()) -> nil()
  guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf))
  verify(nil()) -> true()
  verify(cons(l,ls)) -> if(member(negate(l),ls),false(),verify(ls))
  sat(cnf) -> satck(cnf,guess(cnf))
  satck(cnf,assign) -> if(verify(assign),assign,unsat())

-- SCC decomposition.

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

p1: member#(x,cons(y,ys)) -> if#(eq(x,y),true(),member(x,ys))
p2: member#(x,cons(y,ys)) -> eq#(x,y)
p3: member#(x,cons(y,ys)) -> member#(x,ys)
p4: eq#(O(x),|0|(y)) -> eq#(x,y)
p5: eq#(|1|(x),|1|(y)) -> eq#(x,y)
p6: choice#(cons(x,xs)) -> choice#(xs)
p7: guess#(cons(clause,cnf)) -> choice#(clause)
p8: guess#(cons(clause,cnf)) -> guess#(cnf)
p9: verify#(cons(l,ls)) -> if#(member(negate(l),ls),false(),verify(ls))
p10: verify#(cons(l,ls)) -> member#(negate(l),ls)
p11: verify#(cons(l,ls)) -> negate#(l)
p12: verify#(cons(l,ls)) -> verify#(ls)
p13: sat#(cnf) -> satck#(cnf,guess(cnf))
p14: sat#(cnf) -> guess#(cnf)
p15: satck#(cnf,assign) -> if#(verify(assign),assign,unsat())
p16: satck#(cnf,assign) -> verify#(assign)

and R consists of:

r1: if(true(),t,e) -> t
r2: if(false(),t,e) -> e
r3: member(x,nil()) -> false()
r4: member(x,cons(y,ys)) -> if(eq(x,y),true(),member(x,ys))
r5: eq(nil(),nil()) -> true()
r6: eq(O(x),|0|(y)) -> eq(x,y)
r7: eq(|0|(x),|1|(y)) -> false()
r8: eq(|1|(x),|0|(y)) -> false()
r9: eq(|1|(x),|1|(y)) -> eq(x,y)
r10: negate(|0|(x)) -> |1|(x)
r11: negate(|1|(x)) -> |0|(x)
r12: choice(cons(x,xs)) -> x
r13: choice(cons(x,xs)) -> choice(xs)
r14: guess(nil()) -> nil()
r15: guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf))
r16: verify(nil()) -> true()
r17: verify(cons(l,ls)) -> if(member(negate(l),ls),false(),verify(ls))
r18: sat(cnf) -> satck(cnf,guess(cnf))
r19: satck(cnf,assign) -> if(verify(assign),assign,unsat())

The estimated dependency graph contains the following SCCs:

  {p12}
  {p3}
  {p4, p5}
  {p8}
  {p6}


-- Reduction pair.

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

p1: verify#(cons(l,ls)) -> verify#(ls)

and R consists of:

r1: if(true(),t,e) -> t
r2: if(false(),t,e) -> e
r3: member(x,nil()) -> false()
r4: member(x,cons(y,ys)) -> if(eq(x,y),true(),member(x,ys))
r5: eq(nil(),nil()) -> true()
r6: eq(O(x),|0|(y)) -> eq(x,y)
r7: eq(|0|(x),|1|(y)) -> false()
r8: eq(|1|(x),|0|(y)) -> false()
r9: eq(|1|(x),|1|(y)) -> eq(x,y)
r10: negate(|0|(x)) -> |1|(x)
r11: negate(|1|(x)) -> |0|(x)
r12: choice(cons(x,xs)) -> x
r13: choice(cons(x,xs)) -> choice(xs)
r14: guess(nil()) -> nil()
r15: guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf))
r16: verify(nil()) -> true()
r17: verify(cons(l,ls)) -> if(member(negate(l),ls),false(),verify(ls))
r18: sat(cnf) -> satck(cnf,guess(cnf))
r19: satck(cnf,assign) -> if(verify(assign),assign,unsat())

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: standard order
    interpretations:
      verify#_A(x1) = ((1,1),(1,1)) x1
      cons_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,0)

The next rules are strictly ordered:

  p1
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19

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: member#(x,cons(y,ys)) -> member#(x,ys)

and R consists of:

r1: if(true(),t,e) -> t
r2: if(false(),t,e) -> e
r3: member(x,nil()) -> false()
r4: member(x,cons(y,ys)) -> if(eq(x,y),true(),member(x,ys))
r5: eq(nil(),nil()) -> true()
r6: eq(O(x),|0|(y)) -> eq(x,y)
r7: eq(|0|(x),|1|(y)) -> false()
r8: eq(|1|(x),|0|(y)) -> false()
r9: eq(|1|(x),|1|(y)) -> eq(x,y)
r10: negate(|0|(x)) -> |1|(x)
r11: negate(|1|(x)) -> |0|(x)
r12: choice(cons(x,xs)) -> x
r13: choice(cons(x,xs)) -> choice(xs)
r14: guess(nil()) -> nil()
r15: guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf))
r16: verify(nil()) -> true()
r17: verify(cons(l,ls)) -> if(member(negate(l),ls),false(),verify(ls))
r18: sat(cnf) -> satck(cnf,guess(cnf))
r19: satck(cnf,assign) -> if(verify(assign),assign,unsat())

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: standard order
    interpretations:
      member#_A(x1,x2) = ((1,1),(1,1)) x2
      cons_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,0)

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: eq#(O(x),|0|(y)) -> eq#(x,y)
p2: eq#(|1|(x),|1|(y)) -> eq#(x,y)

and R consists of:

r1: if(true(),t,e) -> t
r2: if(false(),t,e) -> e
r3: member(x,nil()) -> false()
r4: member(x,cons(y,ys)) -> if(eq(x,y),true(),member(x,ys))
r5: eq(nil(),nil()) -> true()
r6: eq(O(x),|0|(y)) -> eq(x,y)
r7: eq(|0|(x),|1|(y)) -> false()
r8: eq(|1|(x),|0|(y)) -> false()
r9: eq(|1|(x),|1|(y)) -> eq(x,y)
r10: negate(|0|(x)) -> |1|(x)
r11: negate(|1|(x)) -> |0|(x)
r12: choice(cons(x,xs)) -> x
r13: choice(cons(x,xs)) -> choice(xs)
r14: guess(nil()) -> nil()
r15: guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf))
r16: verify(nil()) -> true()
r17: verify(cons(l,ls)) -> if(member(negate(l),ls),false(),verify(ls))
r18: sat(cnf) -> satck(cnf,guess(cnf))
r19: satck(cnf,assign) -> if(verify(assign),assign,unsat())

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: standard order
    interpretations:
      eq#_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2
      O_A(x1) = ((1,1),(1,1)) x1 + (1,1)
      |0|_A(x1) = ((1,1),(1,1)) x1 + (1,1)
      |1|_A(x1) = ((1,1),(1,1)) x1 + (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

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: guess#(cons(clause,cnf)) -> guess#(cnf)

and R consists of:

r1: if(true(),t,e) -> t
r2: if(false(),t,e) -> e
r3: member(x,nil()) -> false()
r4: member(x,cons(y,ys)) -> if(eq(x,y),true(),member(x,ys))
r5: eq(nil(),nil()) -> true()
r6: eq(O(x),|0|(y)) -> eq(x,y)
r7: eq(|0|(x),|1|(y)) -> false()
r8: eq(|1|(x),|0|(y)) -> false()
r9: eq(|1|(x),|1|(y)) -> eq(x,y)
r10: negate(|0|(x)) -> |1|(x)
r11: negate(|1|(x)) -> |0|(x)
r12: choice(cons(x,xs)) -> x
r13: choice(cons(x,xs)) -> choice(xs)
r14: guess(nil()) -> nil()
r15: guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf))
r16: verify(nil()) -> true()
r17: verify(cons(l,ls)) -> if(member(negate(l),ls),false(),verify(ls))
r18: sat(cnf) -> satck(cnf,guess(cnf))
r19: satck(cnf,assign) -> if(verify(assign),assign,unsat())

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: standard order
    interpretations:
      guess#_A(x1) = ((1,1),(1,1)) x1
      cons_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,0)

The next rules are strictly ordered:

  p1
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19

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: choice#(cons(x,xs)) -> choice#(xs)

and R consists of:

r1: if(true(),t,e) -> t
r2: if(false(),t,e) -> e
r3: member(x,nil()) -> false()
r4: member(x,cons(y,ys)) -> if(eq(x,y),true(),member(x,ys))
r5: eq(nil(),nil()) -> true()
r6: eq(O(x),|0|(y)) -> eq(x,y)
r7: eq(|0|(x),|1|(y)) -> false()
r8: eq(|1|(x),|0|(y)) -> false()
r9: eq(|1|(x),|1|(y)) -> eq(x,y)
r10: negate(|0|(x)) -> |1|(x)
r11: negate(|1|(x)) -> |0|(x)
r12: choice(cons(x,xs)) -> x
r13: choice(cons(x,xs)) -> choice(xs)
r14: guess(nil()) -> nil()
r15: guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf))
r16: verify(nil()) -> true()
r17: verify(cons(l,ls)) -> if(member(negate(l),ls),false(),verify(ls))
r18: sat(cnf) -> satck(cnf,guess(cnf))
r19: satck(cnf,assign) -> if(verify(assign),assign,unsat())

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: standard order
    interpretations:
      choice#_A(x1) = ((1,1),(1,1)) x1
      cons_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,0)

The next rules are strictly ordered:

  p1
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19

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