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 reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        verify# > cons
      
      argument filter:
    
        pi(verify#) = [1]
        pi(cons) = 2
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        cons > verify#
      
      argument filter:
    
        pi(verify#) = [1]
        pi(cons) = [2]
    
    3. lexicographic path order with precedence:
    
      precedence:
      
        cons > verify#
      
      argument filter:
    
        pi(verify#) = []
        pi(cons) = 2
    

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: 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:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        cons > member#
      
      argument filter:
    
        pi(member#) = [2]
        pi(cons) = [1, 2]
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        cons > member#
      
      argument filter:
    
        pi(member#) = [2]
        pi(cons) = [1, 2]
    
    3. lexicographic path order with precedence:
    
      precedence:
      
        cons > member#
      
      argument filter:
    
        pi(member#) = [2]
        pi(cons) = [1, 2]
    

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 reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        eq# > |1| > |0| > O
      
      argument filter:
    
        pi(eq#) = [1, 2]
        pi(O) = 1
        pi(|0|) = [1]
        pi(|1|) = 1
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        eq# > |1| > |0| > O
      
      argument filter:
    
        pi(eq#) = [1, 2]
        pi(O) = 1
        pi(|0|) = 1
        pi(|1|) = 1
    
    3. lexicographic path order with precedence:
    
      precedence:
      
        |1| > |0| > O > eq#
      
      argument filter:
    
        pi(eq#) = [1]
        pi(O) = [1]
        pi(|0|) = []
        pi(|1|) = [1]
    

The next rules are strictly ordered:

  p1, p2

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 reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        guess# > cons
      
      argument filter:
    
        pi(guess#) = [1]
        pi(cons) = 2
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        cons > guess#
      
      argument filter:
    
        pi(guess#) = [1]
        pi(cons) = [2]
    
    3. lexicographic path order with precedence:
    
      precedence:
      
        cons > guess#
      
      argument filter:
    
        pi(guess#) = []
        pi(cons) = 2
    

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: 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 reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        choice# > cons
      
      argument filter:
    
        pi(choice#) = [1]
        pi(cons) = 2
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        cons > choice#
      
      argument filter:
    
        pi(choice#) = [1]
        pi(cons) = [2]
    
    3. lexicographic path order with precedence:
    
      precedence:
      
        cons > choice#
      
      argument filter:
    
        pi(choice#) = []
        pi(cons) = 2
    

The next rules are strictly ordered:

  p1

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