YES

Problem:
 active(f(X)) -> mark(if(X,c(),f(true())))
 active(if(true(),X,Y)) -> mark(X)
 active(if(false(),X,Y)) -> mark(Y)
 active(f(X)) -> f(active(X))
 active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
 active(if(X1,X2,X3)) -> if(X1,active(X2),X3)
 f(mark(X)) -> mark(f(X))
 if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
 if(X1,mark(X2),X3) -> mark(if(X1,X2,X3))
 proper(f(X)) -> f(proper(X))
 proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
 proper(c()) -> ok(c())
 proper(true()) -> ok(true())
 proper(false()) -> ok(false())
 f(ok(X)) -> ok(f(X))
 if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
 top(mark(X)) -> top(proper(X))
 top(ok(X)) -> top(active(X))

Proof:
 Matrix Interpretation Processor: dim=3
  
  interpretation:
               [1 0 0]  
   [top](x0) = [0 0 0]x0
               [0 0 0]  ,
   
              [1 0 0]  
   [ok](x0) = [0 1 0]x0
              [0 0 0]  ,
   
                    
   [proper](x0) = x0
                    ,
   
             [1]
   [false] = [0]
             [1],
   
                [1 0 0]  
   [mark](x0) = [0 0 0]x0
                [0 0 0]  ,
   
                      [1 0 0]     [1 0 0]     [1 0 0]     [0]
   [if](x0, x1, x2) = [0 0 0]x0 + [0 0 0]x1 + [0 0 0]x2 + [1]
                      [0 0 0]     [1 0 1]     [0 0 0]     [0],
   
            [0]
   [true] = [0]
            [0],
   
         [0]
   [c] = [1]
         [1],
   
                  [1 0 0]     [0]
   [active](x0) = [0 0 0]x0 + [1]
                  [0 0 1]     [0],
   
             [1 0 0]  
   [f](x0) = [0 0 0]x0
             [0 0 1]  
  orientation:
                  [1 0 0]    [0]    [1 0 0]                             
   active(f(X)) = [0 0 0]X + [1] >= [0 0 0]X = mark(if(X,c(),f(true())))
                  [0 0 1]    [0]    [0 0 0]                             
   
                            [1 0 0]    [1 0 0]    [0]    [1 0 0]           
   active(if(true(),X,Y)) = [0 0 0]X + [0 0 0]Y + [1] >= [0 0 0]X = mark(X)
                            [1 0 1]    [0 0 0]    [0]    [0 0 0]           
   
                             [1 0 0]    [1 0 0]    [1]    [1 0 0]           
   active(if(false(),X,Y)) = [0 0 0]X + [0 0 0]Y + [1] >= [0 0 0]Y = mark(Y)
                             [1 0 1]    [0 0 0]    [0]    [0 0 0]           
   
                  [1 0 0]    [0]    [1 0 0]                
   active(f(X)) = [0 0 0]X + [1] >= [0 0 0]X = f(active(X))
                  [0 0 1]    [0]    [0 0 1]                
   
                          [1 0 0]     [1 0 0]     [1 0 0]     [0]    [1 0 0]     [1 0 0]     [1 0 0]     [0]                       
   active(if(X1,X2,X3)) = [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 + [1] >= [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 + [1] = if(active(X1),X2,X3)
                          [0 0 0]     [1 0 1]     [0 0 0]     [0]    [0 0 0]     [1 0 1]     [0 0 0]     [0]                       
   
                          [1 0 0]     [1 0 0]     [1 0 0]     [0]    [1 0 0]     [1 0 0]     [1 0 0]     [0]                       
   active(if(X1,X2,X3)) = [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 + [1] >= [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 + [1] = if(X1,active(X2),X3)
                          [0 0 0]     [1 0 1]     [0 0 0]     [0]    [0 0 0]     [1 0 1]     [0 0 0]     [0]                       
   
                [1 0 0]     [1 0 0]              
   f(mark(X)) = [0 0 0]X >= [0 0 0]X = mark(f(X))
                [0 0 0]     [0 0 0]              
   
                        [1 0 0]     [1 0 0]     [1 0 0]     [0]    [1 0 0]     [1 0 0]     [1 0 0]                       
   if(mark(X1),X2,X3) = [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 + [1] >= [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 = mark(if(X1,X2,X3))
                        [0 0 0]     [1 0 1]     [0 0 0]     [0]    [0 0 0]     [0 0 0]     [0 0 0]                       
   
                        [1 0 0]     [1 0 0]     [1 0 0]     [0]    [1 0 0]     [1 0 0]     [1 0 0]                       
   if(X1,mark(X2),X3) = [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 + [1] >= [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 = mark(if(X1,X2,X3))
                        [0 0 0]     [1 0 0]     [0 0 0]     [0]    [0 0 0]     [0 0 0]     [0 0 0]                       
   
                  [1 0 0]     [1 0 0]                
   proper(f(X)) = [0 0 0]X >= [0 0 0]X = f(proper(X))
                  [0 0 1]     [0 0 1]                
   
                          [1 0 0]     [1 0 0]     [1 0 0]     [0]    [1 0 0]     [1 0 0]     [1 0 0]     [0]                                       
   proper(if(X1,X2,X3)) = [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 + [1] >= [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 + [1] = if(proper(X1),proper(X2),proper(X3))
                          [0 0 0]     [1 0 1]     [0 0 0]     [0]    [0 0 0]     [1 0 1]     [0 0 0]     [0]                                       
   
                 [0]    [0]          
   proper(c()) = [1] >= [1] = ok(c())
                 [1]    [0]          
   
                    [0]    [0]             
   proper(true()) = [0] >= [0] = ok(true())
                    [0]    [0]             
   
                     [1]    [1]              
   proper(false()) = [0] >= [0] = ok(false())
                     [1]    [0]              
   
              [1 0 0]     [1 0 0]            
   f(ok(X)) = [0 0 0]X >= [0 0 0]X = ok(f(X))
              [0 0 0]     [0 0 0]            
   
                              [1 0 0]     [1 0 0]     [1 0 0]     [0]    [1 0 0]     [1 0 0]     [1 0 0]     [0]                   
   if(ok(X1),ok(X2),ok(X3)) = [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 + [1] >= [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 + [1] = ok(if(X1,X2,X3))
                              [0 0 0]     [1 0 0]     [0 0 0]     [0]    [0 0 0]     [0 0 0]     [0 0 0]     [0]                   
   
                  [1 0 0]     [1 0 0]                  
   top(mark(X)) = [0 0 0]X >= [0 0 0]X = top(proper(X))
                  [0 0 0]     [0 0 0]                  
   
                [1 0 0]     [1 0 0]                  
   top(ok(X)) = [0 0 0]X >= [0 0 0]X = top(active(X))
                [0 0 0]     [0 0 0]                  
  problem:
   active(f(X)) -> mark(if(X,c(),f(true())))
   active(if(true(),X,Y)) -> mark(X)
   active(f(X)) -> f(active(X))
   active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
   active(if(X1,X2,X3)) -> if(X1,active(X2),X3)
   f(mark(X)) -> mark(f(X))
   if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
   if(X1,mark(X2),X3) -> mark(if(X1,X2,X3))
   proper(f(X)) -> f(proper(X))
   proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
   proper(c()) -> ok(c())
   proper(true()) -> ok(true())
   proper(false()) -> ok(false())
   f(ok(X)) -> ok(f(X))
   if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
   top(mark(X)) -> top(proper(X))
   top(ok(X)) -> top(active(X))
  DP Processor:
   DPs:
    active#(f(X)) -> f#(true())
    active#(f(X)) -> if#(X,c(),f(true()))
    active#(f(X)) -> active#(X)
    active#(f(X)) -> f#(active(X))
    active#(if(X1,X2,X3)) -> active#(X1)
    active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3)
    active#(if(X1,X2,X3)) -> active#(X2)
    active#(if(X1,X2,X3)) -> if#(X1,active(X2),X3)
    f#(mark(X)) -> f#(X)
    if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
    if#(X1,mark(X2),X3) -> if#(X1,X2,X3)
    proper#(f(X)) -> proper#(X)
    proper#(f(X)) -> f#(proper(X))
    proper#(if(X1,X2,X3)) -> proper#(X3)
    proper#(if(X1,X2,X3)) -> proper#(X2)
    proper#(if(X1,X2,X3)) -> proper#(X1)
    proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
    f#(ok(X)) -> f#(X)
    if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3)
    top#(mark(X)) -> proper#(X)
    top#(mark(X)) -> top#(proper(X))
    top#(ok(X)) -> active#(X)
    top#(ok(X)) -> top#(active(X))
   TRS:
    active(f(X)) -> mark(if(X,c(),f(true())))
    active(if(true(),X,Y)) -> mark(X)
    active(f(X)) -> f(active(X))
    active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
    active(if(X1,X2,X3)) -> if(X1,active(X2),X3)
    f(mark(X)) -> mark(f(X))
    if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
    if(X1,mark(X2),X3) -> mark(if(X1,X2,X3))
    proper(f(X)) -> f(proper(X))
    proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
    proper(c()) -> ok(c())
    proper(true()) -> ok(true())
    proper(false()) -> ok(false())
    f(ok(X)) -> ok(f(X))
    if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
    top(mark(X)) -> top(proper(X))
    top(ok(X)) -> top(active(X))
   TDG Processor:
    DPs:
     active#(f(X)) -> f#(true())
     active#(f(X)) -> if#(X,c(),f(true()))
     active#(f(X)) -> active#(X)
     active#(f(X)) -> f#(active(X))
     active#(if(X1,X2,X3)) -> active#(X1)
     active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3)
     active#(if(X1,X2,X3)) -> active#(X2)
     active#(if(X1,X2,X3)) -> if#(X1,active(X2),X3)
     f#(mark(X)) -> f#(X)
     if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
     if#(X1,mark(X2),X3) -> if#(X1,X2,X3)
     proper#(f(X)) -> proper#(X)
     proper#(f(X)) -> f#(proper(X))
     proper#(if(X1,X2,X3)) -> proper#(X3)
     proper#(if(X1,X2,X3)) -> proper#(X2)
     proper#(if(X1,X2,X3)) -> proper#(X1)
     proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
     f#(ok(X)) -> f#(X)
     if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3)
     top#(mark(X)) -> proper#(X)
     top#(mark(X)) -> top#(proper(X))
     top#(ok(X)) -> active#(X)
     top#(ok(X)) -> top#(active(X))
    TRS:
     active(f(X)) -> mark(if(X,c(),f(true())))
     active(if(true(),X,Y)) -> mark(X)
     active(f(X)) -> f(active(X))
     active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
     active(if(X1,X2,X3)) -> if(X1,active(X2),X3)
     f(mark(X)) -> mark(f(X))
     if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
     if(X1,mark(X2),X3) -> mark(if(X1,X2,X3))
     proper(f(X)) -> f(proper(X))
     proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
     proper(c()) -> ok(c())
     proper(true()) -> ok(true())
     proper(false()) -> ok(false())
     f(ok(X)) -> ok(f(X))
     if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
    graph:
     top#(ok(X)) -> top#(active(X)) -> top#(ok(X)) -> top#(active(X))
     top#(ok(X)) -> top#(active(X)) -> top#(ok(X)) -> active#(X)
     top#(ok(X)) -> top#(active(X)) ->
     top#(mark(X)) -> top#(proper(X))
     top#(ok(X)) -> top#(active(X)) -> top#(mark(X)) -> proper#(X)
     top#(ok(X)) -> active#(X) ->
     active#(if(X1,X2,X3)) -> if#(X1,active(X2),X3)
     top#(ok(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> active#(X2)
     top#(ok(X)) -> active#(X) ->
     active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3)
     top#(ok(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> active#(X1)
     top#(ok(X)) -> active#(X) -> active#(f(X)) -> f#(active(X))
     top#(ok(X)) -> active#(X) -> active#(f(X)) -> active#(X)
     top#(ok(X)) -> active#(X) -> active#(f(X)) -> if#(X,c(),f(true()))
     top#(ok(X)) -> active#(X) -> active#(f(X)) -> f#(true())
     top#(mark(X)) -> top#(proper(X)) ->
     top#(ok(X)) -> top#(active(X))
     top#(mark(X)) -> top#(proper(X)) -> top#(ok(X)) -> active#(X)
     top#(mark(X)) -> top#(proper(X)) ->
     top#(mark(X)) -> top#(proper(X))
     top#(mark(X)) -> top#(proper(X)) -> top#(mark(X)) -> proper#(X)
     top#(mark(X)) -> proper#(X) ->
     proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
     top#(mark(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X1)
     top#(mark(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X2)
     top#(mark(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X3)
     top#(mark(X)) -> proper#(X) -> proper#(f(X)) -> f#(proper(X))
     top#(mark(X)) -> proper#(X) -> proper#(f(X)) -> proper#(X)
     proper#(if(X1,X2,X3)) -> proper#(X3) ->
     proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
     proper#(if(X1,X2,X3)) -> proper#(X3) ->
     proper#(if(X1,X2,X3)) -> proper#(X1)
     proper#(if(X1,X2,X3)) -> proper#(X3) ->
     proper#(if(X1,X2,X3)) -> proper#(X2)
     proper#(if(X1,X2,X3)) -> proper#(X3) ->
     proper#(if(X1,X2,X3)) -> proper#(X3)
     proper#(if(X1,X2,X3)) -> proper#(X3) ->
     proper#(f(X)) -> f#(proper(X))
     proper#(if(X1,X2,X3)) -> proper#(X3) ->
     proper#(f(X)) -> proper#(X)
     proper#(if(X1,X2,X3)) -> proper#(X2) ->
     proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
     proper#(if(X1,X2,X3)) -> proper#(X2) ->
     proper#(if(X1,X2,X3)) -> proper#(X1)
     proper#(if(X1,X2,X3)) -> proper#(X2) ->
     proper#(if(X1,X2,X3)) -> proper#(X2)
     proper#(if(X1,X2,X3)) -> proper#(X2) ->
     proper#(if(X1,X2,X3)) -> proper#(X3)
     proper#(if(X1,X2,X3)) -> proper#(X2) ->
     proper#(f(X)) -> f#(proper(X))
     proper#(if(X1,X2,X3)) -> proper#(X2) ->
     proper#(f(X)) -> proper#(X)
     proper#(if(X1,X2,X3)) -> proper#(X1) ->
     proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
     proper#(if(X1,X2,X3)) -> proper#(X1) ->
     proper#(if(X1,X2,X3)) -> proper#(X1)
     proper#(if(X1,X2,X3)) -> proper#(X1) ->
     proper#(if(X1,X2,X3)) -> proper#(X2)
     proper#(if(X1,X2,X3)) -> proper#(X1) ->
     proper#(if(X1,X2,X3)) -> proper#(X3)
     proper#(if(X1,X2,X3)) -> proper#(X1) ->
     proper#(f(X)) -> f#(proper(X))
     proper#(if(X1,X2,X3)) -> proper#(X1) ->
     proper#(f(X)) -> proper#(X)
     proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) ->
     if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3)
     proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) ->
     if#(X1,mark(X2),X3) -> if#(X1,X2,X3)
     proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) ->
     if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
     proper#(f(X)) -> proper#(X) ->
     proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
     proper#(f(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X1)
     proper#(f(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X2)
     proper#(f(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X3)
     proper#(f(X)) -> proper#(X) -> proper#(f(X)) -> f#(proper(X))
     proper#(f(X)) -> proper#(X) -> proper#(f(X)) -> proper#(X)
     proper#(f(X)) -> f#(proper(X)) -> f#(ok(X)) -> f#(X)
     proper#(f(X)) -> f#(proper(X)) ->
     f#(mark(X)) -> f#(X)
     if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) ->
     if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3)
     if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) ->
     if#(X1,mark(X2),X3) -> if#(X1,X2,X3)
     if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) ->
     if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
     if#(mark(X1),X2,X3) -> if#(X1,X2,X3) ->
     if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3)
     if#(mark(X1),X2,X3) -> if#(X1,X2,X3) ->
     if#(X1,mark(X2),X3) -> if#(X1,X2,X3)
     if#(mark(X1),X2,X3) -> if#(X1,X2,X3) ->
     if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
     if#(X1,mark(X2),X3) -> if#(X1,X2,X3) ->
     if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3)
     if#(X1,mark(X2),X3) -> if#(X1,X2,X3) ->
     if#(X1,mark(X2),X3) -> if#(X1,X2,X3)
     if#(X1,mark(X2),X3) -> if#(X1,X2,X3) -> if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
     f#(ok(X)) -> f#(X) -> f#(ok(X)) -> f#(X)
     f#(ok(X)) -> f#(X) -> f#(mark(X)) -> f#(X)
     f#(mark(X)) -> f#(X) -> f#(ok(X)) -> f#(X)
     f#(mark(X)) -> f#(X) -> f#(mark(X)) -> f#(X)
     active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) ->
     if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3)
     active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) ->
     if#(X1,mark(X2),X3) -> if#(X1,X2,X3)
     active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) ->
     if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
     active#(if(X1,X2,X3)) -> if#(X1,active(X2),X3) ->
     if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3)
     active#(if(X1,X2,X3)) -> if#(X1,active(X2),X3) ->
     if#(X1,mark(X2),X3) -> if#(X1,X2,X3)
     active#(if(X1,X2,X3)) -> if#(X1,active(X2),X3) ->
     if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
     active#(if(X1,X2,X3)) -> active#(X2) ->
     active#(if(X1,X2,X3)) -> if#(X1,active(X2),X3)
     active#(if(X1,X2,X3)) -> active#(X2) ->
     active#(if(X1,X2,X3)) -> active#(X2)
     active#(if(X1,X2,X3)) -> active#(X2) ->
     active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3)
     active#(if(X1,X2,X3)) -> active#(X2) ->
     active#(if(X1,X2,X3)) -> active#(X1)
     active#(if(X1,X2,X3)) -> active#(X2) ->
     active#(f(X)) -> f#(active(X))
     active#(if(X1,X2,X3)) -> active#(X2) ->
     active#(f(X)) -> active#(X)
     active#(if(X1,X2,X3)) -> active#(X2) ->
     active#(f(X)) -> if#(X,c(),f(true()))
     active#(if(X1,X2,X3)) -> active#(X2) ->
     active#(f(X)) -> f#(true())
     active#(if(X1,X2,X3)) -> active#(X1) ->
     active#(if(X1,X2,X3)) -> if#(X1,active(X2),X3)
     active#(if(X1,X2,X3)) -> active#(X1) ->
     active#(if(X1,X2,X3)) -> active#(X2)
     active#(if(X1,X2,X3)) -> active#(X1) ->
     active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3)
     active#(if(X1,X2,X3)) -> active#(X1) ->
     active#(if(X1,X2,X3)) -> active#(X1)
     active#(if(X1,X2,X3)) -> active#(X1) ->
     active#(f(X)) -> f#(active(X))
     active#(if(X1,X2,X3)) -> active#(X1) ->
     active#(f(X)) -> active#(X)
     active#(if(X1,X2,X3)) -> active#(X1) ->
     active#(f(X)) -> if#(X,c(),f(true()))
     active#(if(X1,X2,X3)) -> active#(X1) ->
     active#(f(X)) -> f#(true())
     active#(f(X)) -> if#(X,c(),f(true())) ->
     if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3)
     active#(f(X)) -> if#(X,c(),f(true())) ->
     if#(X1,mark(X2),X3) -> if#(X1,X2,X3)
     active#(f(X)) -> if#(X,c(),f(true())) ->
     if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
     active#(f(X)) -> f#(true()) -> f#(ok(X)) -> f#(X)
     active#(f(X)) -> f#(true()) -> f#(mark(X)) -> f#(X)
     active#(f(X)) -> f#(active(X)) -> f#(ok(X)) -> f#(X)
     active#(f(X)) -> f#(active(X)) -> f#(mark(X)) -> f#(X)
     active#(f(X)) -> active#(X) ->
     active#(if(X1,X2,X3)) -> if#(X1,active(X2),X3)
     active#(f(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> active#(X2)
     active#(f(X)) -> active#(X) ->
     active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3)
     active#(f(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> active#(X1)
     active#(f(X)) -> active#(X) -> active#(f(X)) -> f#(active(X))
     active#(f(X)) -> active#(X) -> active#(f(X)) -> active#(X)
     active#(f(X)) -> active#(X) ->
     active#(f(X)) -> if#(X,c(),f(true()))
     active#(f(X)) -> active#(X) -> active#(f(X)) -> f#(true())
    SCC Processor:
     #sccs: 5
     #rules: 14
     #arcs: 101/529
     DPs:
      top#(ok(X)) -> top#(active(X))
      top#(mark(X)) -> top#(proper(X))
     TRS:
      active(f(X)) -> mark(if(X,c(),f(true())))
      active(if(true(),X,Y)) -> mark(X)
      active(f(X)) -> f(active(X))
      active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
      active(if(X1,X2,X3)) -> if(X1,active(X2),X3)
      f(mark(X)) -> mark(f(X))
      if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
      if(X1,mark(X2),X3) -> mark(if(X1,X2,X3))
      proper(f(X)) -> f(proper(X))
      proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
      proper(c()) -> ok(c())
      proper(true()) -> ok(true())
      proper(false()) -> ok(false())
      f(ok(X)) -> ok(f(X))
      if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
      top(mark(X)) -> top(proper(X))
      top(ok(X)) -> top(active(X))
     LPO Processor:
      argument filtering:
       pi(f) = [0]
       pi(active) = 0
       pi(c) = []
       pi(true) = []
       pi(if) = [0,1]
       pi(mark) = [0]
       pi(false) = []
       pi(proper) = 0
       pi(ok) = 0
       pi(top) = 0
       pi(top#) = 0
      precedence:
       f > if > top# ~ top ~ ok ~ proper ~ false ~ mark ~ true ~ c ~ active
      problem:
       DPs:
        top#(ok(X)) -> top#(active(X))
       TRS:
        active(f(X)) -> mark(if(X,c(),f(true())))
        active(if(true(),X,Y)) -> mark(X)
        active(f(X)) -> f(active(X))
        active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
        active(if(X1,X2,X3)) -> if(X1,active(X2),X3)
        f(mark(X)) -> mark(f(X))
        if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
        if(X1,mark(X2),X3) -> mark(if(X1,X2,X3))
        proper(f(X)) -> f(proper(X))
        proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
        proper(c()) -> ok(c())
        proper(true()) -> ok(true())
        proper(false()) -> ok(false())
        f(ok(X)) -> ok(f(X))
        if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
        top(mark(X)) -> top(proper(X))
        top(ok(X)) -> top(active(X))
      Arctic Interpretation Processor:
       dimension: 1
       interpretation:
        [top#](x0) = x0 + 1,
        
        [top](x0) = 8,
        
        [ok](x0) = 3x0 + 2,
        
        [proper](x0) = 3x0,
        
        [false] = 3,
        
        [mark](x0) = x0 + 0,
        
        [if](x0, x1, x2) = 1x0 + x1 + 0,
        
        [true] = 1,
        
        [c] = 0,
        
        [active](x0) = 2x0 + 0,
        
        [f](x0) = x0
       orientation:
        top#(ok(X)) = 3X + 2 >= 2X + 1 = top#(active(X))
        
        active(f(X)) = 2X + 0 >= 1X + 0 = mark(if(X,c(),f(true())))
        
        active(if(true(),X,Y)) = 2X + 4 >= X + 0 = mark(X)
        
        active(f(X)) = 2X + 0 >= 2X + 0 = f(active(X))
        
        active(if(X1,X2,X3)) = 3X1 + 2X2 + 2 >= 3X1 + X2 + 1 = if(active(X1),X2,X3)
        
        active(if(X1,X2,X3)) = 3X1 + 2X2 + 2 >= 1X1 + 2X2 + 0 = if(X1,active(X2),X3)
        
        f(mark(X)) = X + 0 >= X + 0 = mark(f(X))
        
        if(mark(X1),X2,X3) = 1X1 + X2 + 1 >= 1X1 + X2 + 0 = mark(if(X1,X2,X3))
        
        if(X1,mark(X2),X3) = 1X1 + X2 + 0 >= 1X1 + X2 + 0 = mark(if(X1,X2,X3))
        
        proper(f(X)) = 3X >= 3X = f(proper(X))
        
        proper(if(X1,X2,X3)) = 4X1 + 3X2 + 3 >= 4X1 + 3X2 + 0 = if(proper(X1),proper(X2),proper(X3))
        
        proper(c()) = 3 >= 3 = ok(c())
        
        proper(true()) = 4 >= 4 = ok(true())
        
        proper(false()) = 6 >= 6 = ok(false())
        
        f(ok(X)) = 3X + 2 >= 3X + 2 = ok(f(X))
        
        if(ok(X1),ok(X2),ok(X3)) = 4X1 + 3X2 + 3 >= 4X1 + 3X2 + 3 = ok(if(X1,X2,X3))
        
        top(mark(X)) = 8 >= 8 = top(proper(X))
        
        top(ok(X)) = 8 >= 8 = top(active(X))
       problem:
        DPs:
         
        TRS:
         active(f(X)) -> mark(if(X,c(),f(true())))
         active(if(true(),X,Y)) -> mark(X)
         active(f(X)) -> f(active(X))
         active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
         active(if(X1,X2,X3)) -> if(X1,active(X2),X3)
         f(mark(X)) -> mark(f(X))
         if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
         if(X1,mark(X2),X3) -> mark(if(X1,X2,X3))
         proper(f(X)) -> f(proper(X))
         proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
         proper(c()) -> ok(c())
         proper(true()) -> ok(true())
         proper(false()) -> ok(false())
         f(ok(X)) -> ok(f(X))
         if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
         top(mark(X)) -> top(proper(X))
         top(ok(X)) -> top(active(X))
       Qed
     
     DPs:
      active#(f(X)) -> active#(X)
      active#(if(X1,X2,X3)) -> active#(X1)
      active#(if(X1,X2,X3)) -> active#(X2)
     TRS:
      active(f(X)) -> mark(if(X,c(),f(true())))
      active(if(true(),X,Y)) -> mark(X)
      active(f(X)) -> f(active(X))
      active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
      active(if(X1,X2,X3)) -> if(X1,active(X2),X3)
      f(mark(X)) -> mark(f(X))
      if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
      if(X1,mark(X2),X3) -> mark(if(X1,X2,X3))
      proper(f(X)) -> f(proper(X))
      proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
      proper(c()) -> ok(c())
      proper(true()) -> ok(true())
      proper(false()) -> ok(false())
      f(ok(X)) -> ok(f(X))
      if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
      top(mark(X)) -> top(proper(X))
      top(ok(X)) -> top(active(X))
     Subterm Criterion Processor:
      simple projection:
       pi(active#) = 0
      problem:
       DPs:
        
       TRS:
        active(f(X)) -> mark(if(X,c(),f(true())))
        active(if(true(),X,Y)) -> mark(X)
        active(f(X)) -> f(active(X))
        active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
        active(if(X1,X2,X3)) -> if(X1,active(X2),X3)
        f(mark(X)) -> mark(f(X))
        if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
        if(X1,mark(X2),X3) -> mark(if(X1,X2,X3))
        proper(f(X)) -> f(proper(X))
        proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
        proper(c()) -> ok(c())
        proper(true()) -> ok(true())
        proper(false()) -> ok(false())
        f(ok(X)) -> ok(f(X))
        if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
        top(mark(X)) -> top(proper(X))
        top(ok(X)) -> top(active(X))
      Qed
     
     DPs:
      proper#(f(X)) -> proper#(X)
      proper#(if(X1,X2,X3)) -> proper#(X3)
      proper#(if(X1,X2,X3)) -> proper#(X2)
      proper#(if(X1,X2,X3)) -> proper#(X1)
     TRS:
      active(f(X)) -> mark(if(X,c(),f(true())))
      active(if(true(),X,Y)) -> mark(X)
      active(f(X)) -> f(active(X))
      active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
      active(if(X1,X2,X3)) -> if(X1,active(X2),X3)
      f(mark(X)) -> mark(f(X))
      if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
      if(X1,mark(X2),X3) -> mark(if(X1,X2,X3))
      proper(f(X)) -> f(proper(X))
      proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
      proper(c()) -> ok(c())
      proper(true()) -> ok(true())
      proper(false()) -> ok(false())
      f(ok(X)) -> ok(f(X))
      if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
      top(mark(X)) -> top(proper(X))
      top(ok(X)) -> top(active(X))
     Subterm Criterion Processor:
      simple projection:
       pi(proper#) = 0
      problem:
       DPs:
        
       TRS:
        active(f(X)) -> mark(if(X,c(),f(true())))
        active(if(true(),X,Y)) -> mark(X)
        active(f(X)) -> f(active(X))
        active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
        active(if(X1,X2,X3)) -> if(X1,active(X2),X3)
        f(mark(X)) -> mark(f(X))
        if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
        if(X1,mark(X2),X3) -> mark(if(X1,X2,X3))
        proper(f(X)) -> f(proper(X))
        proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
        proper(c()) -> ok(c())
        proper(true()) -> ok(true())
        proper(false()) -> ok(false())
        f(ok(X)) -> ok(f(X))
        if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
        top(mark(X)) -> top(proper(X))
        top(ok(X)) -> top(active(X))
      Qed
     
     DPs:
      if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
      if#(X1,mark(X2),X3) -> if#(X1,X2,X3)
      if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3)
     TRS:
      active(f(X)) -> mark(if(X,c(),f(true())))
      active(if(true(),X,Y)) -> mark(X)
      active(f(X)) -> f(active(X))
      active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
      active(if(X1,X2,X3)) -> if(X1,active(X2),X3)
      f(mark(X)) -> mark(f(X))
      if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
      if(X1,mark(X2),X3) -> mark(if(X1,X2,X3))
      proper(f(X)) -> f(proper(X))
      proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
      proper(c()) -> ok(c())
      proper(true()) -> ok(true())
      proper(false()) -> ok(false())
      f(ok(X)) -> ok(f(X))
      if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
      top(mark(X)) -> top(proper(X))
      top(ok(X)) -> top(active(X))
     Subterm Criterion Processor:
      simple projection:
       pi(if#) = 2
      problem:
       DPs:
        if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
        if#(X1,mark(X2),X3) -> if#(X1,X2,X3)
       TRS:
        active(f(X)) -> mark(if(X,c(),f(true())))
        active(if(true(),X,Y)) -> mark(X)
        active(f(X)) -> f(active(X))
        active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
        active(if(X1,X2,X3)) -> if(X1,active(X2),X3)
        f(mark(X)) -> mark(f(X))
        if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
        if(X1,mark(X2),X3) -> mark(if(X1,X2,X3))
        proper(f(X)) -> f(proper(X))
        proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
        proper(c()) -> ok(c())
        proper(true()) -> ok(true())
        proper(false()) -> ok(false())
        f(ok(X)) -> ok(f(X))
        if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
        top(mark(X)) -> top(proper(X))
        top(ok(X)) -> top(active(X))
      Subterm Criterion Processor:
       simple projection:
        pi(if#) = 1
       problem:
        DPs:
         if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
        TRS:
         active(f(X)) -> mark(if(X,c(),f(true())))
         active(if(true(),X,Y)) -> mark(X)
         active(f(X)) -> f(active(X))
         active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
         active(if(X1,X2,X3)) -> if(X1,active(X2),X3)
         f(mark(X)) -> mark(f(X))
         if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
         if(X1,mark(X2),X3) -> mark(if(X1,X2,X3))
         proper(f(X)) -> f(proper(X))
         proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
         proper(c()) -> ok(c())
         proper(true()) -> ok(true())
         proper(false()) -> ok(false())
         f(ok(X)) -> ok(f(X))
         if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
         top(mark(X)) -> top(proper(X))
         top(ok(X)) -> top(active(X))
       Subterm Criterion Processor:
        simple projection:
         pi(if#) = 0
        problem:
         DPs:
          
         TRS:
          active(f(X)) -> mark(if(X,c(),f(true())))
          active(if(true(),X,Y)) -> mark(X)
          active(f(X)) -> f(active(X))
          active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
          active(if(X1,X2,X3)) -> if(X1,active(X2),X3)
          f(mark(X)) -> mark(f(X))
          if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
          if(X1,mark(X2),X3) -> mark(if(X1,X2,X3))
          proper(f(X)) -> f(proper(X))
          proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
          proper(c()) -> ok(c())
          proper(true()) -> ok(true())
          proper(false()) -> ok(false())
          f(ok(X)) -> ok(f(X))
          if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
          top(mark(X)) -> top(proper(X))
          top(ok(X)) -> top(active(X))
        Qed
     
     DPs:
      f#(mark(X)) -> f#(X)
      f#(ok(X)) -> f#(X)
     TRS:
      active(f(X)) -> mark(if(X,c(),f(true())))
      active(if(true(),X,Y)) -> mark(X)
      active(f(X)) -> f(active(X))
      active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
      active(if(X1,X2,X3)) -> if(X1,active(X2),X3)
      f(mark(X)) -> mark(f(X))
      if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
      if(X1,mark(X2),X3) -> mark(if(X1,X2,X3))
      proper(f(X)) -> f(proper(X))
      proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
      proper(c()) -> ok(c())
      proper(true()) -> ok(true())
      proper(false()) -> ok(false())
      f(ok(X)) -> ok(f(X))
      if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
      top(mark(X)) -> top(proper(X))
      top(ok(X)) -> top(active(X))
     Subterm Criterion Processor:
      simple projection:
       pi(f#) = 0
      problem:
       DPs:
        
       TRS:
        active(f(X)) -> mark(if(X,c(),f(true())))
        active(if(true(),X,Y)) -> mark(X)
        active(f(X)) -> f(active(X))
        active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
        active(if(X1,X2,X3)) -> if(X1,active(X2),X3)
        f(mark(X)) -> mark(f(X))
        if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
        if(X1,mark(X2),X3) -> mark(if(X1,X2,X3))
        proper(f(X)) -> f(proper(X))
        proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
        proper(c()) -> ok(c())
        proper(true()) -> ok(true())
        proper(false()) -> ok(false())
        f(ok(X)) -> ok(f(X))
        if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
        top(mark(X)) -> top(proper(X))
        top(ok(X)) -> top(active(X))
      Qed