YES

We show the termination of the TRS R:

  minus(n__0(),Y) -> |0|()
  minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
  geq(X,n__0()) -> true()
  geq(n__0(),n__s(Y)) -> false()
  geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y))
  div(|0|(),n__s(Y)) -> |0|()
  div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0())
  if(true(),X,Y) -> activate(X)
  if(false(),X,Y) -> activate(Y)
  |0|() -> n__0()
  s(X) -> n__s(X)
  div(X1,X2) -> n__div(X1,X2)
  minus(X1,X2) -> n__minus(X1,X2)
  activate(n__0()) -> |0|()
  activate(n__s(X)) -> s(activate(X))
  activate(n__div(X1,X2)) -> div(activate(X1),X2)
  activate(n__minus(X1,X2)) -> minus(X1,X2)
  activate(X) -> X

-- SCC decomposition.

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

p1: minus#(n__0(),Y) -> |0|#()
p2: minus#(n__s(X),n__s(Y)) -> minus#(activate(X),activate(Y))
p3: minus#(n__s(X),n__s(Y)) -> activate#(X)
p4: minus#(n__s(X),n__s(Y)) -> activate#(Y)
p5: geq#(n__s(X),n__s(Y)) -> geq#(activate(X),activate(Y))
p6: geq#(n__s(X),n__s(Y)) -> activate#(X)
p7: geq#(n__s(X),n__s(Y)) -> activate#(Y)
p8: div#(s(X),n__s(Y)) -> if#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0())
p9: div#(s(X),n__s(Y)) -> geq#(X,activate(Y))
p10: div#(s(X),n__s(Y)) -> activate#(Y)
p11: if#(true(),X,Y) -> activate#(X)
p12: if#(false(),X,Y) -> activate#(Y)
p13: activate#(n__0()) -> |0|#()
p14: activate#(n__s(X)) -> s#(activate(X))
p15: activate#(n__s(X)) -> activate#(X)
p16: activate#(n__div(X1,X2)) -> div#(activate(X1),X2)
p17: activate#(n__div(X1,X2)) -> activate#(X1)
p18: activate#(n__minus(X1,X2)) -> minus#(X1,X2)

and R consists of:

r1: minus(n__0(),Y) -> |0|()
r2: minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
r3: geq(X,n__0()) -> true()
r4: geq(n__0(),n__s(Y)) -> false()
r5: geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y))
r6: div(|0|(),n__s(Y)) -> |0|()
r7: div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0())
r8: if(true(),X,Y) -> activate(X)
r9: if(false(),X,Y) -> activate(Y)
r10: |0|() -> n__0()
r11: s(X) -> n__s(X)
r12: div(X1,X2) -> n__div(X1,X2)
r13: minus(X1,X2) -> n__minus(X1,X2)
r14: activate(n__0()) -> |0|()
r15: activate(n__s(X)) -> s(activate(X))
r16: activate(n__div(X1,X2)) -> div(activate(X1),X2)
r17: activate(n__minus(X1,X2)) -> minus(X1,X2)
r18: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p15, p16, p17, p18}


-- Reduction pair.

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

p1: minus#(n__s(X),n__s(Y)) -> minus#(activate(X),activate(Y))
p2: minus#(n__s(X),n__s(Y)) -> activate#(Y)
p3: activate#(n__minus(X1,X2)) -> minus#(X1,X2)
p4: minus#(n__s(X),n__s(Y)) -> activate#(X)
p5: activate#(n__div(X1,X2)) -> activate#(X1)
p6: activate#(n__div(X1,X2)) -> div#(activate(X1),X2)
p7: div#(s(X),n__s(Y)) -> activate#(Y)
p8: activate#(n__s(X)) -> activate#(X)
p9: div#(s(X),n__s(Y)) -> geq#(X,activate(Y))
p10: geq#(n__s(X),n__s(Y)) -> activate#(Y)
p11: geq#(n__s(X),n__s(Y)) -> activate#(X)
p12: geq#(n__s(X),n__s(Y)) -> geq#(activate(X),activate(Y))
p13: div#(s(X),n__s(Y)) -> if#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0())
p14: if#(false(),X,Y) -> activate#(Y)
p15: if#(true(),X,Y) -> activate#(X)

and R consists of:

r1: minus(n__0(),Y) -> |0|()
r2: minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
r3: geq(X,n__0()) -> true()
r4: geq(n__0(),n__s(Y)) -> false()
r5: geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y))
r6: div(|0|(),n__s(Y)) -> |0|()
r7: div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0())
r8: if(true(),X,Y) -> activate(X)
r9: if(false(),X,Y) -> activate(Y)
r10: |0|() -> n__0()
r11: s(X) -> n__s(X)
r12: div(X1,X2) -> n__div(X1,X2)
r13: minus(X1,X2) -> n__minus(X1,X2)
r14: activate(n__0()) -> |0|()
r15: activate(n__s(X)) -> s(activate(X))
r16: activate(n__div(X1,X2)) -> div(activate(X1),X2)
r17: activate(n__minus(X1,X2)) -> minus(X1,X2)
r18: activate(X) -> 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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          minus#_A(x1,x2) = max{x1 + 6, x2 + 9}
          n__s_A(x1) = max{2, x1}
          activate_A(x1) = x1
          activate#_A(x1) = max{7, x1 + 6}
          n__minus_A(x1,x2) = max{x1, x2 + 4}
          n__div_A(x1,x2) = max{25, x1 + 19, x2 + 24}
          div#_A(x1,x2) = max{x1 + 25, x2 + 30}
          s_A(x1) = max{2, x1}
          geq#_A(x1,x2) = max{x1 + 14, x2 + 17}
          if#_A(x1,x2,x3) = max{13, x1 + 10, x2 + 6, x3 + 8}
          geq_A(x1,x2) = max{x1 + 14, x2 + 13}
          n__0_A = 4
          false_A = 4
          true_A = 4
          if_A(x1,x2,x3) = max{x1 + 5, x2, x3}
          minus_A(x1,x2) = max{x1, x2 + 4}
          |0|_A = 4
          div_A(x1,x2) = max{25, x1 + 19, x2 + 24}
    
      precedence:
      
        n__minus = minus > n__div = div > if > activate = |0| > n__0 > geq > false > s = true > geq# > minus# = n__s = activate# = div# = if#
      
      partial status:
    
        pi(minus#) = []
        pi(n__s) = []
        pi(activate) = [1]
        pi(activate#) = []
        pi(n__minus) = []
        pi(n__div) = []
        pi(div#) = []
        pi(s) = []
        pi(geq#) = []
        pi(if#) = []
        pi(geq) = []
        pi(n__0) = []
        pi(false) = []
        pi(true) = []
        pi(if) = [2, 3]
        pi(minus) = []
        pi(|0|) = []
        pi(div) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          minus#_A(x1,x2) = 147
          n__s_A(x1) = 149
          activate_A(x1) = max{142, x1 + 28}
          activate#_A(x1) = 147
          n__minus_A(x1,x2) = 112
          n__div_A(x1,x2) = 115
          div#_A(x1,x2) = 147
          s_A(x1) = 142
          geq#_A(x1,x2) = 147
          if#_A(x1,x2,x3) = 147
          geq_A(x1,x2) = 7
          n__0_A = 146
          false_A = 6
          true_A = 1
          if_A(x1,x2,x3) = max{x2 + 143, x3 + 11}
          minus_A(x1,x2) = 141
          |0|_A = 147
          div_A(x1,x2) = 143
    
      precedence:
      
        n__s > n__minus > activate = if = div > n__div = s > minus# = activate# = div# = geq# = if# > |0| > geq = n__0 = minus > false = true
      
      partial status:
    
        pi(minus#) = []
        pi(n__s) = []
        pi(activate) = [1]
        pi(activate#) = []
        pi(n__minus) = []
        pi(n__div) = []
        pi(div#) = []
        pi(s) = []
        pi(geq#) = []
        pi(if#) = []
        pi(geq) = []
        pi(n__0) = []
        pi(false) = []
        pi(true) = []
        pi(if) = [2, 3]
        pi(minus) = []
        pi(|0|) = []
        pi(div) = []
    

The next rules are strictly ordered:

  p7, p14

We remove them from the problem.

-- SCC decomposition.

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

p1: minus#(n__s(X),n__s(Y)) -> minus#(activate(X),activate(Y))
p2: minus#(n__s(X),n__s(Y)) -> activate#(Y)
p3: activate#(n__minus(X1,X2)) -> minus#(X1,X2)
p4: minus#(n__s(X),n__s(Y)) -> activate#(X)
p5: activate#(n__div(X1,X2)) -> activate#(X1)
p6: activate#(n__div(X1,X2)) -> div#(activate(X1),X2)
p7: activate#(n__s(X)) -> activate#(X)
p8: div#(s(X),n__s(Y)) -> geq#(X,activate(Y))
p9: geq#(n__s(X),n__s(Y)) -> activate#(Y)
p10: geq#(n__s(X),n__s(Y)) -> activate#(X)
p11: geq#(n__s(X),n__s(Y)) -> geq#(activate(X),activate(Y))
p12: div#(s(X),n__s(Y)) -> if#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0())
p13: if#(true(),X,Y) -> activate#(X)

and R consists of:

r1: minus(n__0(),Y) -> |0|()
r2: minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
r3: geq(X,n__0()) -> true()
r4: geq(n__0(),n__s(Y)) -> false()
r5: geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y))
r6: div(|0|(),n__s(Y)) -> |0|()
r7: div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0())
r8: if(true(),X,Y) -> activate(X)
r9: if(false(),X,Y) -> activate(Y)
r10: |0|() -> n__0()
r11: s(X) -> n__s(X)
r12: div(X1,X2) -> n__div(X1,X2)
r13: minus(X1,X2) -> n__minus(X1,X2)
r14: activate(n__0()) -> |0|()
r15: activate(n__s(X)) -> s(activate(X))
r16: activate(n__div(X1,X2)) -> div(activate(X1),X2)
r17: activate(n__minus(X1,X2)) -> minus(X1,X2)
r18: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13}


-- Reduction pair.

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

p1: minus#(n__s(X),n__s(Y)) -> minus#(activate(X),activate(Y))
p2: minus#(n__s(X),n__s(Y)) -> activate#(X)
p3: activate#(n__s(X)) -> activate#(X)
p4: activate#(n__div(X1,X2)) -> div#(activate(X1),X2)
p5: div#(s(X),n__s(Y)) -> if#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0())
p6: if#(true(),X,Y) -> activate#(X)
p7: activate#(n__div(X1,X2)) -> activate#(X1)
p8: activate#(n__minus(X1,X2)) -> minus#(X1,X2)
p9: minus#(n__s(X),n__s(Y)) -> activate#(Y)
p10: div#(s(X),n__s(Y)) -> geq#(X,activate(Y))
p11: geq#(n__s(X),n__s(Y)) -> geq#(activate(X),activate(Y))
p12: geq#(n__s(X),n__s(Y)) -> activate#(X)
p13: geq#(n__s(X),n__s(Y)) -> activate#(Y)

and R consists of:

r1: minus(n__0(),Y) -> |0|()
r2: minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
r3: geq(X,n__0()) -> true()
r4: geq(n__0(),n__s(Y)) -> false()
r5: geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y))
r6: div(|0|(),n__s(Y)) -> |0|()
r7: div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0())
r8: if(true(),X,Y) -> activate(X)
r9: if(false(),X,Y) -> activate(Y)
r10: |0|() -> n__0()
r11: s(X) -> n__s(X)
r12: div(X1,X2) -> n__div(X1,X2)
r13: minus(X1,X2) -> n__minus(X1,X2)
r14: activate(n__0()) -> |0|()
r15: activate(n__s(X)) -> s(activate(X))
r16: activate(n__div(X1,X2)) -> div(activate(X1),X2)
r17: activate(n__minus(X1,X2)) -> minus(X1,X2)
r18: activate(X) -> 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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          minus#_A(x1,x2) = max{x1, x2 + 2}
          n__s_A(x1) = max{17, x1}
          activate_A(x1) = max{5, x1}
          activate#_A(x1) = x1
          n__div_A(x1,x2) = max{x1 + 27, x2 + 36}
          div#_A(x1,x2) = max{x1 + 27, x2 + 36}
          s_A(x1) = max{17, x1}
          if#_A(x1,x2,x3) = max{26, x1 - 19, x2, x3 + 17}
          geq_A(x1,x2) = 36
          n__minus_A(x1,x2) = max{26, x1, x2 + 3}
          n__0_A = 0
          true_A = 36
          geq#_A(x1,x2) = max{x1 + 5, x2 + 18}
          if_A(x1,x2,x3) = max{x2, x3 + 6}
          false_A = 0
          minus_A(x1,x2) = max{26, x1, x2 + 3}
          |0|_A = 4
          div_A(x1,x2) = max{x1 + 27, x2 + 36}
    
      precedence:
      
        |0| > n__div = geq = div > geq# = if > activate > n__0 > false > minus > n__minus > s > n__s > minus# = activate# = div# = if# = true
      
      partial status:
    
        pi(minus#) = []
        pi(n__s) = []
        pi(activate) = [1]
        pi(activate#) = []
        pi(n__div) = []
        pi(div#) = []
        pi(s) = []
        pi(if#) = []
        pi(geq) = []
        pi(n__minus) = []
        pi(n__0) = []
        pi(true) = []
        pi(geq#) = []
        pi(if) = [2, 3]
        pi(false) = []
        pi(minus) = []
        pi(|0|) = []
        pi(div) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          minus#_A(x1,x2) = 21
          n__s_A(x1) = 13
          activate_A(x1) = max{13, x1}
          activate#_A(x1) = 21
          n__div_A(x1,x2) = 13
          div#_A(x1,x2) = 21
          s_A(x1) = 13
          if#_A(x1,x2,x3) = 21
          geq_A(x1,x2) = 13
          n__minus_A(x1,x2) = 14
          n__0_A = 0
          true_A = 12
          geq#_A(x1,x2) = 0
          if_A(x1,x2,x3) = max{13, x2}
          false_A = 25
          minus_A(x1,x2) = 15
          |0|_A = 18
          div_A(x1,x2) = 13
    
      precedence:
      
        minus# = activate# = div# = if# > geq# > s > geq = false > true = minus > n__div = div > n__s > n__minus = n__0 > activate = if = |0|
      
      partial status:
    
        pi(minus#) = []
        pi(n__s) = []
        pi(activate) = [1]
        pi(activate#) = []
        pi(n__div) = []
        pi(div#) = []
        pi(s) = []
        pi(if#) = []
        pi(geq) = []
        pi(n__minus) = []
        pi(n__0) = []
        pi(true) = []
        pi(geq#) = []
        pi(if) = [2]
        pi(false) = []
        pi(minus) = []
        pi(|0|) = []
        pi(div) = []
    

The next rules are strictly ordered:

  p9, p10, p12, p13

We remove them from the problem.

-- SCC decomposition.

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

p1: minus#(n__s(X),n__s(Y)) -> minus#(activate(X),activate(Y))
p2: minus#(n__s(X),n__s(Y)) -> activate#(X)
p3: activate#(n__s(X)) -> activate#(X)
p4: activate#(n__div(X1,X2)) -> div#(activate(X1),X2)
p5: div#(s(X),n__s(Y)) -> if#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0())
p6: if#(true(),X,Y) -> activate#(X)
p7: activate#(n__div(X1,X2)) -> activate#(X1)
p8: activate#(n__minus(X1,X2)) -> minus#(X1,X2)
p9: geq#(n__s(X),n__s(Y)) -> geq#(activate(X),activate(Y))

and R consists of:

r1: minus(n__0(),Y) -> |0|()
r2: minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
r3: geq(X,n__0()) -> true()
r4: geq(n__0(),n__s(Y)) -> false()
r5: geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y))
r6: div(|0|(),n__s(Y)) -> |0|()
r7: div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0())
r8: if(true(),X,Y) -> activate(X)
r9: if(false(),X,Y) -> activate(Y)
r10: |0|() -> n__0()
r11: s(X) -> n__s(X)
r12: div(X1,X2) -> n__div(X1,X2)
r13: minus(X1,X2) -> n__minus(X1,X2)
r14: activate(n__0()) -> |0|()
r15: activate(n__s(X)) -> s(activate(X))
r16: activate(n__div(X1,X2)) -> div(activate(X1),X2)
r17: activate(n__minus(X1,X2)) -> minus(X1,X2)
r18: activate(X) -> X

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: minus#(n__s(X),n__s(Y)) -> minus#(activate(X),activate(Y))
p2: minus#(n__s(X),n__s(Y)) -> activate#(X)
p3: activate#(n__minus(X1,X2)) -> minus#(X1,X2)
p4: activate#(n__div(X1,X2)) -> activate#(X1)
p5: activate#(n__div(X1,X2)) -> div#(activate(X1),X2)
p6: div#(s(X),n__s(Y)) -> if#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0())
p7: if#(true(),X,Y) -> activate#(X)
p8: activate#(n__s(X)) -> activate#(X)

and R consists of:

r1: minus(n__0(),Y) -> |0|()
r2: minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
r3: geq(X,n__0()) -> true()
r4: geq(n__0(),n__s(Y)) -> false()
r5: geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y))
r6: div(|0|(),n__s(Y)) -> |0|()
r7: div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0())
r8: if(true(),X,Y) -> activate(X)
r9: if(false(),X,Y) -> activate(Y)
r10: |0|() -> n__0()
r11: s(X) -> n__s(X)
r12: div(X1,X2) -> n__div(X1,X2)
r13: minus(X1,X2) -> n__minus(X1,X2)
r14: activate(n__0()) -> |0|()
r15: activate(n__s(X)) -> s(activate(X))
r16: activate(n__div(X1,X2)) -> div(activate(X1),X2)
r17: activate(n__minus(X1,X2)) -> minus(X1,X2)
r18: activate(X) -> 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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          minus#_A(x1,x2) = max{x1 + 31, x2 + 33}
          n__s_A(x1) = max{19, x1}
          activate_A(x1) = max{7, x1}
          activate#_A(x1) = x1 + 31
          n__minus_A(x1,x2) = max{15, x1, x2 + 3}
          n__div_A(x1,x2) = max{x1 + 3, x2 + 14}
          div#_A(x1,x2) = max{x1 + 34, x2 + 45}
          s_A(x1) = max{19, x1}
          if#_A(x1,x2,x3) = max{x1 - 7, x2 + 31, x3 + 31}
          geq_A(x1,x2) = max{64, x1 + 34, x2 + 45}
          n__0_A = 2
          true_A = 38
          if_A(x1,x2,x3) = max{4, x1 - 31, x2, x3 + 1}
          false_A = 46
          minus_A(x1,x2) = max{15, x1, x2 + 3}
          |0|_A = 4
          div_A(x1,x2) = max{x1 + 3, x2 + 14}
    
      precedence:
      
        false > geq > n__div = div > if > |0| > activate > s > minus > n__minus = true > n__0 > minus# = n__s = activate# = div# = if#
      
      partial status:
    
        pi(minus#) = []
        pi(n__s) = []
        pi(activate) = [1]
        pi(activate#) = []
        pi(n__minus) = [2]
        pi(n__div) = [2]
        pi(div#) = []
        pi(s) = []
        pi(if#) = []
        pi(geq) = []
        pi(n__0) = []
        pi(true) = []
        pi(if) = [2, 3]
        pi(false) = []
        pi(minus) = []
        pi(|0|) = []
        pi(div) = [2]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          minus#_A(x1,x2) = 55
          n__s_A(x1) = 70
          activate_A(x1) = 80
          activate#_A(x1) = 55
          n__minus_A(x1,x2) = 207
          n__div_A(x1,x2) = x2 + 104
          div#_A(x1,x2) = 55
          s_A(x1) = 428
          if#_A(x1,x2,x3) = 55
          geq_A(x1,x2) = 197
          n__0_A = 68
          true_A = 197
          if_A(x1,x2,x3) = x2 + 81
          false_A = 69
          minus_A(x1,x2) = 79
          |0|_A = 78
          div_A(x1,x2) = x2 + 104
    
      precedence:
      
        n__s = s > minus# = activate# = n__minus = div# = if# > false > geq > div > n__0 = true = if > activate > n__div > minus > |0|
      
      partial status:
    
        pi(minus#) = []
        pi(n__s) = []
        pi(activate) = []
        pi(activate#) = []
        pi(n__minus) = []
        pi(n__div) = []
        pi(div#) = []
        pi(s) = []
        pi(if#) = []
        pi(geq) = []
        pi(n__0) = []
        pi(true) = []
        pi(if) = [2]
        pi(false) = []
        pi(minus) = []
        pi(|0|) = []
        pi(div) = [2]
    

The next rules are strictly ordered:

  p4

We remove them from the problem.

-- SCC decomposition.

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

p1: minus#(n__s(X),n__s(Y)) -> minus#(activate(X),activate(Y))
p2: minus#(n__s(X),n__s(Y)) -> activate#(X)
p3: activate#(n__minus(X1,X2)) -> minus#(X1,X2)
p4: activate#(n__div(X1,X2)) -> div#(activate(X1),X2)
p5: div#(s(X),n__s(Y)) -> if#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0())
p6: if#(true(),X,Y) -> activate#(X)
p7: activate#(n__s(X)) -> activate#(X)

and R consists of:

r1: minus(n__0(),Y) -> |0|()
r2: minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
r3: geq(X,n__0()) -> true()
r4: geq(n__0(),n__s(Y)) -> false()
r5: geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y))
r6: div(|0|(),n__s(Y)) -> |0|()
r7: div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0())
r8: if(true(),X,Y) -> activate(X)
r9: if(false(),X,Y) -> activate(Y)
r10: |0|() -> n__0()
r11: s(X) -> n__s(X)
r12: div(X1,X2) -> n__div(X1,X2)
r13: minus(X1,X2) -> n__minus(X1,X2)
r14: activate(n__0()) -> |0|()
r15: activate(n__s(X)) -> s(activate(X))
r16: activate(n__div(X1,X2)) -> div(activate(X1),X2)
r17: activate(n__minus(X1,X2)) -> minus(X1,X2)
r18: activate(X) -> X

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: minus#(n__s(X),n__s(Y)) -> minus#(activate(X),activate(Y))
p2: minus#(n__s(X),n__s(Y)) -> activate#(X)
p3: activate#(n__s(X)) -> activate#(X)
p4: activate#(n__div(X1,X2)) -> div#(activate(X1),X2)
p5: div#(s(X),n__s(Y)) -> if#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0())
p6: if#(true(),X,Y) -> activate#(X)
p7: activate#(n__minus(X1,X2)) -> minus#(X1,X2)

and R consists of:

r1: minus(n__0(),Y) -> |0|()
r2: minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
r3: geq(X,n__0()) -> true()
r4: geq(n__0(),n__s(Y)) -> false()
r5: geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y))
r6: div(|0|(),n__s(Y)) -> |0|()
r7: div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0())
r8: if(true(),X,Y) -> activate(X)
r9: if(false(),X,Y) -> activate(Y)
r10: |0|() -> n__0()
r11: s(X) -> n__s(X)
r12: div(X1,X2) -> n__div(X1,X2)
r13: minus(X1,X2) -> n__minus(X1,X2)
r14: activate(n__0()) -> |0|()
r15: activate(n__s(X)) -> s(activate(X))
r16: activate(n__div(X1,X2)) -> div(activate(X1),X2)
r17: activate(n__minus(X1,X2)) -> minus(X1,X2)
r18: activate(X) -> 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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          minus#_A(x1,x2) = x1 + 41
          n__s_A(x1) = max{68, x1 + 29}
          activate_A(x1) = max{8, x1}
          activate#_A(x1) = max{69, x1 + 68}
          n__div_A(x1,x2) = max{50, x1 + 42}
          div#_A(x1,x2) = x1 + 110
          s_A(x1) = max{68, x1 + 29}
          if#_A(x1,x2,x3) = max{x2 + 68, x3 + 178}
          geq_A(x1,x2) = max{97, x1 - 29, x2 - 9}
          n__minus_A(x1,x2) = max{0, x1 - 26}
          n__0_A = 0
          true_A = 1
          if_A(x1,x2,x3) = max{110, x2 + 26, x3 + 56}
          false_A = 0
          minus_A(x1,x2) = max{8, x1 - 26}
          |0|_A = 7
          div_A(x1,x2) = max{50, x1 + 42}
    
      precedence:
      
        minus# = activate = activate# = div# = s = if# = |0| > n__s = n__0 > div > if > minus > n__div = n__minus = false > geq = true
      
      partial status:
    
        pi(minus#) = []
        pi(n__s) = []
        pi(activate) = [1]
        pi(activate#) = []
        pi(n__div) = []
        pi(div#) = []
        pi(s) = []
        pi(if#) = []
        pi(geq) = []
        pi(n__minus) = []
        pi(n__0) = []
        pi(true) = []
        pi(if) = [3]
        pi(false) = []
        pi(minus) = []
        pi(|0|) = []
        pi(div) = [1]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          minus#_A(x1,x2) = 97
          n__s_A(x1) = 24
          activate_A(x1) = 37
          activate#_A(x1) = 97
          n__div_A(x1,x2) = 32
          div#_A(x1,x2) = 97
          s_A(x1) = 27
          if#_A(x1,x2,x3) = 97
          geq_A(x1,x2) = 36
          n__minus_A(x1,x2) = 30
          n__0_A = 61
          true_A = 62
          if_A(x1,x2,x3) = max{117, x3 + 56}
          false_A = 62
          minus_A(x1,x2) = 37
          |0|_A = 62
          div_A(x1,x2) = 37
    
      precedence:
      
        |0| > n__s = activate > minus = div > n__div = s > minus# = activate# = div# = if# > geq = n__minus = n__0 = true = if = false
      
      partial status:
    
        pi(minus#) = []
        pi(n__s) = []
        pi(activate) = []
        pi(activate#) = []
        pi(n__div) = []
        pi(div#) = []
        pi(s) = []
        pi(if#) = []
        pi(geq) = []
        pi(n__minus) = []
        pi(n__0) = []
        pi(true) = []
        pi(if) = []
        pi(false) = []
        pi(minus) = []
        pi(|0|) = []
        pi(div) = []
    

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: minus#(n__s(X),n__s(Y)) -> activate#(X)
p2: activate#(n__s(X)) -> activate#(X)
p3: activate#(n__div(X1,X2)) -> div#(activate(X1),X2)
p4: div#(s(X),n__s(Y)) -> if#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0())
p5: if#(true(),X,Y) -> activate#(X)
p6: activate#(n__minus(X1,X2)) -> minus#(X1,X2)

and R consists of:

r1: minus(n__0(),Y) -> |0|()
r2: minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
r3: geq(X,n__0()) -> true()
r4: geq(n__0(),n__s(Y)) -> false()
r5: geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y))
r6: div(|0|(),n__s(Y)) -> |0|()
r7: div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0())
r8: if(true(),X,Y) -> activate(X)
r9: if(false(),X,Y) -> activate(Y)
r10: |0|() -> n__0()
r11: s(X) -> n__s(X)
r12: div(X1,X2) -> n__div(X1,X2)
r13: minus(X1,X2) -> n__minus(X1,X2)
r14: activate(n__0()) -> |0|()
r15: activate(n__s(X)) -> s(activate(X))
r16: activate(n__div(X1,X2)) -> div(activate(X1),X2)
r17: activate(n__minus(X1,X2)) -> minus(X1,X2)
r18: activate(X) -> X

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: minus#(n__s(X),n__s(Y)) -> activate#(X)
p2: activate#(n__minus(X1,X2)) -> minus#(X1,X2)
p3: activate#(n__div(X1,X2)) -> div#(activate(X1),X2)
p4: div#(s(X),n__s(Y)) -> if#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0())
p5: if#(true(),X,Y) -> activate#(X)
p6: activate#(n__s(X)) -> activate#(X)

and R consists of:

r1: minus(n__0(),Y) -> |0|()
r2: minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
r3: geq(X,n__0()) -> true()
r4: geq(n__0(),n__s(Y)) -> false()
r5: geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y))
r6: div(|0|(),n__s(Y)) -> |0|()
r7: div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0())
r8: if(true(),X,Y) -> activate(X)
r9: if(false(),X,Y) -> activate(Y)
r10: |0|() -> n__0()
r11: s(X) -> n__s(X)
r12: div(X1,X2) -> n__div(X1,X2)
r13: minus(X1,X2) -> n__minus(X1,X2)
r14: activate(n__0()) -> |0|()
r15: activate(n__s(X)) -> s(activate(X))
r16: activate(n__div(X1,X2)) -> div(activate(X1),X2)
r17: activate(n__minus(X1,X2)) -> minus(X1,X2)
r18: activate(X) -> 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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          minus#_A(x1,x2) = max{4, x1 + 1}
          n__s_A(x1) = max{53, x1 + 27}
          activate#_A(x1) = max{27, x1 + 26}
          n__minus_A(x1,x2) = max{21, x1 - 16}
          n__div_A(x1,x2) = max{78, x1 + 57}
          div#_A(x1,x2) = max{82, x1 + 71}
          activate_A(x1) = x1 + 11
          s_A(x1) = max{63, x1 + 27}
          if#_A(x1,x2,x3) = max{83, x2 + 28, x3 + 70}
          geq_A(x1,x2) = max{120, x1 + 29, x2 + 67}
          n__0_A = 27
          true_A = 0
          if_A(x1,x2,x3) = max{120, x2 + 15, x3 + 50}
          false_A = 27
          minus_A(x1,x2) = max{31, x1 - 16}
          |0|_A = 28
          div_A(x1,x2) = max{78, x1 + 57}
    
      precedence:
      
        n__0 > false > activate = div > minus > geq > n__minus = s > n__s > if# = true > n__div > activate# > minus# > if > div# = |0|
      
      partial status:
    
        pi(minus#) = [1]
        pi(n__s) = [1]
        pi(activate#) = []
        pi(n__minus) = []
        pi(n__div) = []
        pi(div#) = []
        pi(activate) = [1]
        pi(s) = []
        pi(if#) = [3]
        pi(geq) = [1, 2]
        pi(n__0) = []
        pi(true) = []
        pi(if) = []
        pi(false) = []
        pi(minus) = []
        pi(|0|) = []
        pi(div) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          minus#_A(x1,x2) = x1 + 49
          n__s_A(x1) = x1 + 20
          activate#_A(x1) = 5
          n__minus_A(x1,x2) = 35
          n__div_A(x1,x2) = 2
          div#_A(x1,x2) = 5
          activate_A(x1) = 20
          s_A(x1) = 20
          if#_A(x1,x2,x3) = 5
          geq_A(x1,x2) = max{x1 + 35, x2 - 14}
          n__0_A = 47
          true_A = 34
          if_A(x1,x2,x3) = 20
          false_A = 9
          minus_A(x1,x2) = 55
          |0|_A = 56
          div_A(x1,x2) = 20
    
      precedence:
      
        n__0 > minus# = n__minus = n__div > n__s = activate# = div# = if# > geq > true > false = minus > activate = if = div > |0| > s
      
      partial status:
    
        pi(minus#) = [1]
        pi(n__s) = []
        pi(activate#) = []
        pi(n__minus) = []
        pi(n__div) = []
        pi(div#) = []
        pi(activate) = []
        pi(s) = []
        pi(if#) = []
        pi(geq) = [1]
        pi(n__0) = []
        pi(true) = []
        pi(if) = []
        pi(false) = []
        pi(minus) = []
        pi(|0|) = []
        pi(div) = []
    

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: activate#(n__div(X1,X2)) -> div#(activate(X1),X2)
p2: div#(s(X),n__s(Y)) -> if#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0())
p3: if#(true(),X,Y) -> activate#(X)
p4: activate#(n__s(X)) -> activate#(X)

and R consists of:

r1: minus(n__0(),Y) -> |0|()
r2: minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
r3: geq(X,n__0()) -> true()
r4: geq(n__0(),n__s(Y)) -> false()
r5: geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y))
r6: div(|0|(),n__s(Y)) -> |0|()
r7: div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0())
r8: if(true(),X,Y) -> activate(X)
r9: if(false(),X,Y) -> activate(Y)
r10: |0|() -> n__0()
r11: s(X) -> n__s(X)
r12: div(X1,X2) -> n__div(X1,X2)
r13: minus(X1,X2) -> n__minus(X1,X2)
r14: activate(n__0()) -> |0|()
r15: activate(n__s(X)) -> s(activate(X))
r16: activate(n__div(X1,X2)) -> div(activate(X1),X2)
r17: activate(n__minus(X1,X2)) -> minus(X1,X2)
r18: activate(X) -> X

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: activate#(n__div(X1,X2)) -> div#(activate(X1),X2)
p2: div#(s(X),n__s(Y)) -> if#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0())
p3: if#(true(),X,Y) -> activate#(X)
p4: activate#(n__s(X)) -> activate#(X)

and R consists of:

r1: minus(n__0(),Y) -> |0|()
r2: minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
r3: geq(X,n__0()) -> true()
r4: geq(n__0(),n__s(Y)) -> false()
r5: geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y))
r6: div(|0|(),n__s(Y)) -> |0|()
r7: div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0())
r8: if(true(),X,Y) -> activate(X)
r9: if(false(),X,Y) -> activate(Y)
r10: |0|() -> n__0()
r11: s(X) -> n__s(X)
r12: div(X1,X2) -> n__div(X1,X2)
r13: minus(X1,X2) -> n__minus(X1,X2)
r14: activate(n__0()) -> |0|()
r15: activate(n__s(X)) -> s(activate(X))
r16: activate(n__div(X1,X2)) -> div(activate(X1),X2)
r17: activate(n__minus(X1,X2)) -> minus(X1,X2)
r18: activate(X) -> 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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          activate#_A(x1) = x1
          n__div_A(x1,x2) = x1 + 150
          div#_A(x1,x2) = x1 + 76
          activate_A(x1) = x1 + 73
          s_A(x1) = max{130, x1 + 34}
          n__s_A(x1) = max{58, x1 + 34}
          if#_A(x1,x2,x3) = max{x1 - 30, x2 + 21, x3 + 109}
          geq_A(x1,x2) = 109
          n__minus_A(x1,x2) = 0
          n__0_A = 0
          true_A = 31
          if_A(x1,x2,x3) = max{x1 + 74, x2 + 81, x3 + 137}
          false_A = 33
          minus_A(x1,x2) = 65
          |0|_A = 33
          div_A(x1,x2) = x1 + 150
    
      precedence:
      
        activate# = n__div = div# = activate = s = n__s = if# = geq = n__minus = n__0 = true = if = false = minus = |0| = div
      
      partial status:
    
        pi(activate#) = []
        pi(n__div) = []
        pi(div#) = []
        pi(activate) = []
        pi(s) = []
        pi(n__s) = []
        pi(if#) = []
        pi(geq) = []
        pi(n__minus) = []
        pi(n__0) = []
        pi(true) = []
        pi(if) = []
        pi(false) = []
        pi(minus) = []
        pi(|0|) = []
        pi(div) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          activate#_A(x1) = max{350, x1 + 29}
          n__div_A(x1,x2) = 9
          div#_A(x1,x2) = 27
          activate_A(x1) = max{39, x1 + 35}
          s_A(x1) = 120
          n__s_A(x1) = 119
          if#_A(x1,x2,x3) = 187
          geq_A(x1,x2) = 28
          n__minus_A(x1,x2) = 43
          n__0_A = 118
          true_A = 119
          if_A(x1,x2,x3) = 38
          false_A = 29
          minus_A(x1,x2) = 78
          |0|_A = 38
          div_A(x1,x2) = 43
    
      precedence:
      
        activate# > div# > activate = s = if# = geq = n__0 = true = |0| > div > n__s = n__minus = if = false = minus > n__div
      
      partial status:
    
        pi(activate#) = [1]
        pi(n__div) = []
        pi(div#) = []
        pi(activate) = [1]
        pi(s) = []
        pi(n__s) = []
        pi(if#) = []
        pi(geq) = []
        pi(n__minus) = []
        pi(n__0) = []
        pi(true) = []
        pi(if) = []
        pi(false) = []
        pi(minus) = []
        pi(|0|) = []
        pi(div) = []
    

The next rules are strictly ordered:

  p1, p2, p3, p4

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: geq#(n__s(X),n__s(Y)) -> geq#(activate(X),activate(Y))

and R consists of:

r1: minus(n__0(),Y) -> |0|()
r2: minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
r3: geq(X,n__0()) -> true()
r4: geq(n__0(),n__s(Y)) -> false()
r5: geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y))
r6: div(|0|(),n__s(Y)) -> |0|()
r7: div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0())
r8: if(true(),X,Y) -> activate(X)
r9: if(false(),X,Y) -> activate(Y)
r10: |0|() -> n__0()
r11: s(X) -> n__s(X)
r12: div(X1,X2) -> n__div(X1,X2)
r13: minus(X1,X2) -> n__minus(X1,X2)
r14: activate(n__0()) -> |0|()
r15: activate(n__s(X)) -> s(activate(X))
r16: activate(n__div(X1,X2)) -> div(activate(X1),X2)
r17: activate(n__minus(X1,X2)) -> minus(X1,X2)
r18: activate(X) -> 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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          geq#_A(x1,x2) = max{28, x1 + 1, x2 + 12}
          n__s_A(x1) = max{27, x1 + 17}
          activate_A(x1) = x1 + 8
          geq_A(x1,x2) = max{x1 + 37, x2 + 50}
          n__0_A = 0
          true_A = 0
          false_A = 2
          if_A(x1,x2,x3) = max{53, x2 + 9, x3 + 29}
          minus_A(x1,x2) = max{5, x1 - 10}
          |0|_A = 4
          div_A(x1,x2) = max{28, x1 + 26}
          s_A(x1) = max{27, x1 + 17}
          n__div_A(x1,x2) = max{27, x1 + 26}
          n__minus_A(x1,x2) = max{1, x1 - 18}
    
      precedence:
      
        activate > |0| = s > geq# = geq = n__0 = false = minus = div = n__div = n__minus > true > if > n__s
      
      partial status:
    
        pi(geq#) = []
        pi(n__s) = []
        pi(activate) = []
        pi(geq) = [2]
        pi(n__0) = []
        pi(true) = []
        pi(false) = []
        pi(if) = [2, 3]
        pi(minus) = []
        pi(|0|) = []
        pi(div) = [1]
        pi(s) = []
        pi(n__div) = []
        pi(n__minus) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          geq#_A(x1,x2) = 51
          n__s_A(x1) = 63
          activate_A(x1) = 51
          geq_A(x1,x2) = x2 + 130
          n__0_A = 39
          true_A = 99
          false_A = 99
          if_A(x1,x2,x3) = max{94, x2 + 56, x3 + 55}
          minus_A(x1,x2) = 51
          |0|_A = 40
          div_A(x1,x2) = max{54, x1 + 3}
          s_A(x1) = 44
          n__div_A(x1,x2) = 51
          n__minus_A(x1,x2) = 48
    
      precedence:
      
        geq# = n__s = activate = geq = n__0 = true = false > if > minus = |0| = div = s = n__div = n__minus
      
      partial status:
    
        pi(geq#) = []
        pi(n__s) = []
        pi(activate) = []
        pi(geq) = [2]
        pi(n__0) = []
        pi(true) = []
        pi(false) = []
        pi(if) = [3]
        pi(minus) = []
        pi(|0|) = []
        pi(div) = [1]
        pi(s) = []
        pi(n__div) = []
        pi(n__minus) = []
    

The next rules are strictly ordered:

  p1

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