YES

We show the termination of the TRS R:

  a__f(X) -> a__if(mark(X),c(),f(true()))
  a__if(true(),X,Y) -> mark(X)
  a__if(false(),X,Y) -> mark(Y)
  mark(f(X)) -> a__f(mark(X))
  mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3)
  mark(c()) -> c()
  mark(true()) -> true()
  mark(false()) -> false()
  a__f(X) -> f(X)
  a__if(X1,X2,X3) -> if(X1,X2,X3)

-- SCC decomposition.

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

p1: a__f#(X) -> a__if#(mark(X),c(),f(true()))
p2: a__f#(X) -> mark#(X)
p3: a__if#(true(),X,Y) -> mark#(X)
p4: a__if#(false(),X,Y) -> mark#(Y)
p5: mark#(f(X)) -> a__f#(mark(X))
p6: mark#(f(X)) -> mark#(X)
p7: mark#(if(X1,X2,X3)) -> a__if#(mark(X1),mark(X2),X3)
p8: mark#(if(X1,X2,X3)) -> mark#(X1)
p9: mark#(if(X1,X2,X3)) -> mark#(X2)

and R consists of:

r1: a__f(X) -> a__if(mark(X),c(),f(true()))
r2: a__if(true(),X,Y) -> mark(X)
r3: a__if(false(),X,Y) -> mark(Y)
r4: mark(f(X)) -> a__f(mark(X))
r5: mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3)
r6: mark(c()) -> c()
r7: mark(true()) -> true()
r8: mark(false()) -> false()
r9: a__f(X) -> f(X)
r10: a__if(X1,X2,X3) -> if(X1,X2,X3)

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p5, p6, p7, p8, p9}


-- Reduction pair.

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

p1: a__f#(X) -> a__if#(mark(X),c(),f(true()))
p2: a__if#(false(),X,Y) -> mark#(Y)
p3: mark#(if(X1,X2,X3)) -> mark#(X2)
p4: mark#(if(X1,X2,X3)) -> mark#(X1)
p5: mark#(if(X1,X2,X3)) -> a__if#(mark(X1),mark(X2),X3)
p6: a__if#(true(),X,Y) -> mark#(X)
p7: mark#(f(X)) -> mark#(X)
p8: mark#(f(X)) -> a__f#(mark(X))
p9: a__f#(X) -> mark#(X)

and R consists of:

r1: a__f(X) -> a__if(mark(X),c(),f(true()))
r2: a__if(true(),X,Y) -> mark(X)
r3: a__if(false(),X,Y) -> mark(Y)
r4: mark(f(X)) -> a__f(mark(X))
r5: mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3)
r6: mark(c()) -> c()
r7: mark(true()) -> true()
r8: mark(false()) -> false()
r9: a__f(X) -> f(X)
r10: a__if(X1,X2,X3) -> if(X1,X2,X3)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__f#_A(x1) = x1 + 7
          a__if#_A(x1,x2,x3) = max{x1 + 6, x2 + 2, x3 + 1}
          mark_A(x1) = x1
          c_A = 0
          f_A(x1) = x1 + 6
          true_A = 0
          false_A = 1
          mark#_A(x1) = max{4, x1 + 1}
          if_A(x1,x2,x3) = max{x1 + 5, x2 + 5, x3}
          a__f_A(x1) = x1 + 6
          a__if_A(x1,x2,x3) = max{x1 + 5, x2 + 5, x3}
    
      precedence:
      
        a__f# = a__if# = mark = c = f = true = false = mark# = if = a__f = a__if
      
      partial status:
    
        pi(a__f#) = []
        pi(a__if#) = []
        pi(mark) = []
        pi(c) = []
        pi(f) = []
        pi(true) = []
        pi(false) = []
        pi(mark#) = []
        pi(if) = []
        pi(a__f) = []
        pi(a__if) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__f#_A(x1) = x1
          a__if#_A(x1,x2,x3) = 0
          mark_A(x1) = 0
          c_A = 0
          f_A(x1) = 0
          true_A = 0
          false_A = 0
          mark#_A(x1) = 0
          if_A(x1,x2,x3) = 0
          a__f_A(x1) = 0
          a__if_A(x1,x2,x3) = 0
    
      precedence:
      
        mark = c = f = a__f = a__if > a__f# = a__if# = true = false = mark# = if
      
      partial status:
    
        pi(a__f#) = []
        pi(a__if#) = []
        pi(mark) = []
        pi(c) = []
        pi(f) = []
        pi(true) = []
        pi(false) = []
        pi(mark#) = []
        pi(if) = []
        pi(a__f) = []
        pi(a__if) = []
    

The next rules are strictly ordered:

  p6

We remove them from the problem.

-- SCC decomposition.

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

p1: a__f#(X) -> a__if#(mark(X),c(),f(true()))
p2: a__if#(false(),X,Y) -> mark#(Y)
p3: mark#(if(X1,X2,X3)) -> mark#(X2)
p4: mark#(if(X1,X2,X3)) -> mark#(X1)
p5: mark#(if(X1,X2,X3)) -> a__if#(mark(X1),mark(X2),X3)
p6: mark#(f(X)) -> mark#(X)
p7: mark#(f(X)) -> a__f#(mark(X))
p8: a__f#(X) -> mark#(X)

and R consists of:

r1: a__f(X) -> a__if(mark(X),c(),f(true()))
r2: a__if(true(),X,Y) -> mark(X)
r3: a__if(false(),X,Y) -> mark(Y)
r4: mark(f(X)) -> a__f(mark(X))
r5: mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3)
r6: mark(c()) -> c()
r7: mark(true()) -> true()
r8: mark(false()) -> false()
r9: a__f(X) -> f(X)
r10: a__if(X1,X2,X3) -> if(X1,X2,X3)

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p5, p6, p7, p8}


-- Reduction pair.

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

p1: a__f#(X) -> a__if#(mark(X),c(),f(true()))
p2: a__if#(false(),X,Y) -> mark#(Y)
p3: mark#(f(X)) -> a__f#(mark(X))
p4: a__f#(X) -> mark#(X)
p5: mark#(f(X)) -> mark#(X)
p6: mark#(if(X1,X2,X3)) -> a__if#(mark(X1),mark(X2),X3)
p7: mark#(if(X1,X2,X3)) -> mark#(X1)
p8: mark#(if(X1,X2,X3)) -> mark#(X2)

and R consists of:

r1: a__f(X) -> a__if(mark(X),c(),f(true()))
r2: a__if(true(),X,Y) -> mark(X)
r3: a__if(false(),X,Y) -> mark(Y)
r4: mark(f(X)) -> a__f(mark(X))
r5: mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3)
r6: mark(c()) -> c()
r7: mark(true()) -> true()
r8: mark(false()) -> false()
r9: a__f(X) -> f(X)
r10: a__if(X1,X2,X3) -> if(X1,X2,X3)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__f#_A(x1) = max{13, x1 + 3}
          a__if#_A(x1,x2,x3) = max{10, x3 - 5}
          mark_A(x1) = max{2, x1}
          c_A = 0
          f_A(x1) = max{18, x1 + 16}
          true_A = 1
          false_A = 3
          mark#_A(x1) = max{6, x1 - 5}
          if_A(x1,x2,x3) = max{15, x1 + 12, x2, x3}
          a__f_A(x1) = max{18, x1 + 16}
          a__if_A(x1,x2,x3) = max{15, x1 + 12, x2, x3}
    
      precedence:
      
        mark = a__f = a__if > c > f > a__f# = a__if# = true = false = mark# = if
      
      partial status:
    
        pi(a__f#) = []
        pi(a__if#) = []
        pi(mark) = []
        pi(c) = []
        pi(f) = [1]
        pi(true) = []
        pi(false) = []
        pi(mark#) = []
        pi(if) = []
        pi(a__f) = []
        pi(a__if) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__f#_A(x1) = 0
          a__if#_A(x1,x2,x3) = 0
          mark_A(x1) = 8
          c_A = 7
          f_A(x1) = x1 + 22
          true_A = 9
          false_A = 3
          mark#_A(x1) = 0
          if_A(x1,x2,x3) = 8
          a__f_A(x1) = 8
          a__if_A(x1,x2,x3) = 8
    
      precedence:
      
        mark = f = true = a__f = a__if > c = if > a__f# = a__if# = false = mark#
      
      partial status:
    
        pi(a__f#) = []
        pi(a__if#) = []
        pi(mark) = []
        pi(c) = []
        pi(f) = [1]
        pi(true) = []
        pi(false) = []
        pi(mark#) = []
        pi(if) = []
        pi(a__f) = []
        pi(a__if) = []
    

The next rules are strictly ordered:

  p5

We remove them from the problem.

-- SCC decomposition.

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

p1: a__f#(X) -> a__if#(mark(X),c(),f(true()))
p2: a__if#(false(),X,Y) -> mark#(Y)
p3: mark#(f(X)) -> a__f#(mark(X))
p4: a__f#(X) -> mark#(X)
p5: mark#(if(X1,X2,X3)) -> a__if#(mark(X1),mark(X2),X3)
p6: mark#(if(X1,X2,X3)) -> mark#(X1)
p7: mark#(if(X1,X2,X3)) -> mark#(X2)

and R consists of:

r1: a__f(X) -> a__if(mark(X),c(),f(true()))
r2: a__if(true(),X,Y) -> mark(X)
r3: a__if(false(),X,Y) -> mark(Y)
r4: mark(f(X)) -> a__f(mark(X))
r5: mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3)
r6: mark(c()) -> c()
r7: mark(true()) -> true()
r8: mark(false()) -> false()
r9: a__f(X) -> f(X)
r10: a__if(X1,X2,X3) -> if(X1,X2,X3)

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p5, p6, p7}


-- Reduction pair.

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

p1: a__f#(X) -> a__if#(mark(X),c(),f(true()))
p2: a__if#(false(),X,Y) -> mark#(Y)
p3: mark#(if(X1,X2,X3)) -> mark#(X2)
p4: mark#(if(X1,X2,X3)) -> mark#(X1)
p5: mark#(if(X1,X2,X3)) -> a__if#(mark(X1),mark(X2),X3)
p6: mark#(f(X)) -> a__f#(mark(X))
p7: a__f#(X) -> mark#(X)

and R consists of:

r1: a__f(X) -> a__if(mark(X),c(),f(true()))
r2: a__if(true(),X,Y) -> mark(X)
r3: a__if(false(),X,Y) -> mark(Y)
r4: mark(f(X)) -> a__f(mark(X))
r5: mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3)
r6: mark(c()) -> c()
r7: mark(true()) -> true()
r8: mark(false()) -> false()
r9: a__f(X) -> f(X)
r10: a__if(X1,X2,X3) -> if(X1,X2,X3)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__f#_A(x1) = max{14, x1 - 23}
          a__if#_A(x1,x2,x3) = max{2, x1 - 40, x2 - 24, x3 - 22}
          mark_A(x1) = x1 + 16
          c_A = 0
          f_A(x1) = max{35, x1 + 34}
          true_A = 0
          false_A = 55
          mark#_A(x1) = max{14, x1 - 23}
          if_A(x1,x2,x3) = max{x1 + 17, x2 + 26, x3 + 15}
          a__f_A(x1) = max{51, x1 + 34}
          a__if_A(x1,x2,x3) = max{x1 + 17, x2 + 26, x3 + 16}
    
      precedence:
      
        a__if# = false > mark = a__f = a__if > f = true > if > a__f# = c = mark#
      
      partial status:
    
        pi(a__f#) = []
        pi(a__if#) = []
        pi(mark) = []
        pi(c) = []
        pi(f) = []
        pi(true) = []
        pi(false) = []
        pi(mark#) = []
        pi(if) = []
        pi(a__f) = []
        pi(a__if) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__f#_A(x1) = 12
          a__if#_A(x1,x2,x3) = 8
          mark_A(x1) = 5
          c_A = 21
          f_A(x1) = 4
          true_A = 8
          false_A = 22
          mark#_A(x1) = 12
          if_A(x1,x2,x3) = 2
          a__f_A(x1) = 5
          a__if_A(x1,x2,x3) = 5
    
      precedence:
      
        a__if# > true > false > a__f# = mark = c = mark# = if = a__f = a__if > f
      
      partial status:
    
        pi(a__f#) = []
        pi(a__if#) = []
        pi(mark) = []
        pi(c) = []
        pi(f) = []
        pi(true) = []
        pi(false) = []
        pi(mark#) = []
        pi(if) = []
        pi(a__f) = []
        pi(a__if) = []
    

The next rules are strictly ordered:

  p1, p2, p5

We remove them from the problem.

-- SCC decomposition.

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

p1: mark#(if(X1,X2,X3)) -> mark#(X2)
p2: mark#(if(X1,X2,X3)) -> mark#(X1)
p3: mark#(f(X)) -> a__f#(mark(X))
p4: a__f#(X) -> mark#(X)

and R consists of:

r1: a__f(X) -> a__if(mark(X),c(),f(true()))
r2: a__if(true(),X,Y) -> mark(X)
r3: a__if(false(),X,Y) -> mark(Y)
r4: mark(f(X)) -> a__f(mark(X))
r5: mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3)
r6: mark(c()) -> c()
r7: mark(true()) -> true()
r8: mark(false()) -> false()
r9: a__f(X) -> f(X)
r10: a__if(X1,X2,X3) -> if(X1,X2,X3)

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4}


-- Reduction pair.

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

p1: mark#(if(X1,X2,X3)) -> mark#(X2)
p2: mark#(f(X)) -> a__f#(mark(X))
p3: a__f#(X) -> mark#(X)
p4: mark#(if(X1,X2,X3)) -> mark#(X1)

and R consists of:

r1: a__f(X) -> a__if(mark(X),c(),f(true()))
r2: a__if(true(),X,Y) -> mark(X)
r3: a__if(false(),X,Y) -> mark(Y)
r4: mark(f(X)) -> a__f(mark(X))
r5: mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3)
r6: mark(c()) -> c()
r7: mark(true()) -> true()
r8: mark(false()) -> false()
r9: a__f(X) -> f(X)
r10: a__if(X1,X2,X3) -> if(X1,X2,X3)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = max{0, x1 - 1}
          if_A(x1,x2,x3) = max{6, x1 + 2, x2 + 2, x3}
          f_A(x1) = x1 + 6
          a__f#_A(x1) = x1 + 4
          mark_A(x1) = x1
          a__f_A(x1) = x1 + 6
          a__if_A(x1,x2,x3) = max{6, x1 + 2, x2 + 2, x3}
          c_A = 4
          true_A = 0
          false_A = 1
    
      precedence:
      
        mark = a__f = a__if > c = true > if > mark# = f = a__f# = false
      
      partial status:
    
        pi(mark#) = []
        pi(if) = []
        pi(f) = []
        pi(a__f#) = [1]
        pi(mark) = []
        pi(a__f) = []
        pi(a__if) = []
        pi(c) = []
        pi(true) = []
        pi(false) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = 23
          if_A(x1,x2,x3) = 10
          f_A(x1) = 8
          a__f#_A(x1) = 23
          mark_A(x1) = 12
          a__f_A(x1) = 12
          a__if_A(x1,x2,x3) = 12
          c_A = 0
          true_A = 4
          false_A = 11
    
      precedence:
      
        c > mark# = if = f = a__f# = mark = a__f = a__if = true = false
      
      partial status:
    
        pi(mark#) = []
        pi(if) = []
        pi(f) = []
        pi(a__f#) = []
        pi(mark) = []
        pi(a__f) = []
        pi(a__if) = []
        pi(c) = []
        pi(true) = []
        pi(false) = []
    

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

p1: mark#(f(X)) -> a__f#(mark(X))
p2: a__f#(X) -> mark#(X)
p3: mark#(if(X1,X2,X3)) -> mark#(X1)

and R consists of:

r1: a__f(X) -> a__if(mark(X),c(),f(true()))
r2: a__if(true(),X,Y) -> mark(X)
r3: a__if(false(),X,Y) -> mark(Y)
r4: mark(f(X)) -> a__f(mark(X))
r5: mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3)
r6: mark(c()) -> c()
r7: mark(true()) -> true()
r8: mark(false()) -> false()
r9: a__f(X) -> f(X)
r10: a__if(X1,X2,X3) -> if(X1,X2,X3)

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3}


-- Reduction pair.

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

p1: mark#(f(X)) -> a__f#(mark(X))
p2: a__f#(X) -> mark#(X)
p3: mark#(if(X1,X2,X3)) -> mark#(X1)

and R consists of:

r1: a__f(X) -> a__if(mark(X),c(),f(true()))
r2: a__if(true(),X,Y) -> mark(X)
r3: a__if(false(),X,Y) -> mark(Y)
r4: mark(f(X)) -> a__f(mark(X))
r5: mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3)
r6: mark(c()) -> c()
r7: mark(true()) -> true()
r8: mark(false()) -> false()
r9: a__f(X) -> f(X)
r10: a__if(X1,X2,X3) -> if(X1,X2,X3)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = x1 + 3
          f_A(x1) = x1 + 4
          a__f#_A(x1) = x1 + 4
          mark_A(x1) = x1
          if_A(x1,x2,x3) = max{4, x1, x2 + 3, x3}
          a__f_A(x1) = x1 + 4
          a__if_A(x1,x2,x3) = max{4, x1, x2 + 3, x3}
          c_A = 0
          true_A = 0
          false_A = 1
    
      precedence:
      
        mark = if = a__f = a__if > false > f > mark# = a__f# > true > c
      
      partial status:
    
        pi(mark#) = [1]
        pi(f) = []
        pi(a__f#) = [1]
        pi(mark) = []
        pi(if) = []
        pi(a__f) = []
        pi(a__if) = []
        pi(c) = []
        pi(true) = []
        pi(false) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = 0
          f_A(x1) = 0
          a__f#_A(x1) = 0
          mark_A(x1) = 0
          if_A(x1,x2,x3) = 0
          a__f_A(x1) = 0
          a__if_A(x1,x2,x3) = 0
          c_A = 1
          true_A = 4
          false_A = 1
    
      precedence:
      
        mark# > a__f# = mark = a__f = a__if = c = true = false > if > f
      
      partial status:
    
        pi(mark#) = []
        pi(f) = []
        pi(a__f#) = []
        pi(mark) = []
        pi(if) = []
        pi(a__f) = []
        pi(a__if) = []
        pi(c) = []
        pi(true) = []
        pi(false) = []
    

The next rules are strictly ordered:

  p1, p2

We remove them from the problem.

-- SCC decomposition.

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

p1: mark#(if(X1,X2,X3)) -> mark#(X1)

and R consists of:

r1: a__f(X) -> a__if(mark(X),c(),f(true()))
r2: a__if(true(),X,Y) -> mark(X)
r3: a__if(false(),X,Y) -> mark(Y)
r4: mark(f(X)) -> a__f(mark(X))
r5: mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3)
r6: mark(c()) -> c()
r7: mark(true()) -> true()
r8: mark(false()) -> false()
r9: a__f(X) -> f(X)
r10: a__if(X1,X2,X3) -> if(X1,X2,X3)

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: mark#(if(X1,X2,X3)) -> mark#(X1)

and R consists of:

r1: a__f(X) -> a__if(mark(X),c(),f(true()))
r2: a__if(true(),X,Y) -> mark(X)
r3: a__if(false(),X,Y) -> mark(Y)
r4: mark(f(X)) -> a__f(mark(X))
r5: mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3)
r6: mark(c()) -> c()
r7: mark(true()) -> true()
r8: mark(false()) -> false()
r9: a__f(X) -> f(X)
r10: a__if(X1,X2,X3) -> if(X1,X2,X3)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = x1 + 3
          if_A(x1,x2,x3) = max{x1 + 2, x2 + 2, x3 + 2}
    
      precedence:
      
        mark# = if
      
      partial status:
    
        pi(mark#) = []
        pi(if) = [2, 3]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = 1
          if_A(x1,x2,x3) = max{x2 + 1, x3 + 1}
    
      precedence:
      
        mark# = if
      
      partial status:
    
        pi(mark#) = []
        pi(if) = [3]
    

The next rules are strictly ordered:

  p1

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