MAYBE

Problem:
 active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X)))))
 active(add(0(),X)) -> mark(X)
 active(add(s(X),Y)) -> mark(s(add(X,Y)))
 active(prod(0(),X)) -> mark(0())
 active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y)))
 active(if(true(),X,Y)) -> mark(X)
 active(if(false(),X,Y)) -> mark(Y)
 active(zero(0())) -> mark(true())
 active(zero(s(X))) -> mark(false())
 active(p(s(X))) -> mark(X)
 mark(fact(X)) -> active(fact(mark(X)))
 mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
 mark(zero(X)) -> active(zero(mark(X)))
 mark(s(X)) -> active(s(mark(X)))
 mark(0()) -> active(0())
 mark(prod(X1,X2)) -> active(prod(mark(X1),mark(X2)))
 mark(p(X)) -> active(p(mark(X)))
 mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
 mark(true()) -> active(true())
 mark(false()) -> active(false())
 fact(mark(X)) -> fact(X)
 fact(active(X)) -> fact(X)
 if(mark(X1),X2,X3) -> if(X1,X2,X3)
 if(X1,mark(X2),X3) -> if(X1,X2,X3)
 if(X1,X2,mark(X3)) -> if(X1,X2,X3)
 if(active(X1),X2,X3) -> if(X1,X2,X3)
 if(X1,active(X2),X3) -> if(X1,X2,X3)
 if(X1,X2,active(X3)) -> if(X1,X2,X3)
 zero(mark(X)) -> zero(X)
 zero(active(X)) -> zero(X)
 s(mark(X)) -> s(X)
 s(active(X)) -> s(X)
 prod(mark(X1),X2) -> prod(X1,X2)
 prod(X1,mark(X2)) -> prod(X1,X2)
 prod(active(X1),X2) -> prod(X1,X2)
 prod(X1,active(X2)) -> prod(X1,X2)
 p(mark(X)) -> p(X)
 p(active(X)) -> p(X)
 add(mark(X1),X2) -> add(X1,X2)
 add(X1,mark(X2)) -> add(X1,X2)
 add(active(X1),X2) -> add(X1,X2)
 add(X1,active(X2)) -> add(X1,X2)

Proof:
 DP Processor:
  DPs:
   active#(fact(X)) -> p#(X)
   active#(fact(X)) -> fact#(p(X))
   active#(fact(X)) -> prod#(X,fact(p(X)))
   active#(fact(X)) -> s#(0())
   active#(fact(X)) -> zero#(X)
   active#(fact(X)) -> if#(zero(X),s(0()),prod(X,fact(p(X))))
   active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X)))))
   active#(add(0(),X)) -> mark#(X)
   active#(add(s(X),Y)) -> add#(X,Y)
   active#(add(s(X),Y)) -> s#(add(X,Y))
   active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
   active#(prod(0(),X)) -> mark#(0())
   active#(prod(s(X),Y)) -> prod#(X,Y)
   active#(prod(s(X),Y)) -> add#(Y,prod(X,Y))
   active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y)))
   active#(if(true(),X,Y)) -> mark#(X)
   active#(if(false(),X,Y)) -> mark#(Y)
   active#(zero(0())) -> mark#(true())
   active#(zero(s(X))) -> mark#(false())
   active#(p(s(X))) -> mark#(X)
   mark#(fact(X)) -> mark#(X)
   mark#(fact(X)) -> fact#(mark(X))
   mark#(fact(X)) -> active#(fact(mark(X)))
   mark#(if(X1,X2,X3)) -> mark#(X1)
   mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
   mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
   mark#(zero(X)) -> mark#(X)
   mark#(zero(X)) -> zero#(mark(X))
   mark#(zero(X)) -> active#(zero(mark(X)))
   mark#(s(X)) -> mark#(X)
   mark#(s(X)) -> s#(mark(X))
   mark#(s(X)) -> active#(s(mark(X)))
   mark#(0()) -> active#(0())
   mark#(prod(X1,X2)) -> mark#(X2)
   mark#(prod(X1,X2)) -> mark#(X1)
   mark#(prod(X1,X2)) -> prod#(mark(X1),mark(X2))
   mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
   mark#(p(X)) -> mark#(X)
   mark#(p(X)) -> p#(mark(X))
   mark#(p(X)) -> active#(p(mark(X)))
   mark#(add(X1,X2)) -> mark#(X2)
   mark#(add(X1,X2)) -> mark#(X1)
   mark#(add(X1,X2)) -> add#(mark(X1),mark(X2))
   mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
   mark#(true()) -> active#(true())
   mark#(false()) -> active#(false())
   fact#(mark(X)) -> fact#(X)
   fact#(active(X)) -> fact#(X)
   if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
   if#(X1,mark(X2),X3) -> if#(X1,X2,X3)
   if#(X1,X2,mark(X3)) -> if#(X1,X2,X3)
   if#(active(X1),X2,X3) -> if#(X1,X2,X3)
   if#(X1,active(X2),X3) -> if#(X1,X2,X3)
   if#(X1,X2,active(X3)) -> if#(X1,X2,X3)
   zero#(mark(X)) -> zero#(X)
   zero#(active(X)) -> zero#(X)
   s#(mark(X)) -> s#(X)
   s#(active(X)) -> s#(X)
   prod#(mark(X1),X2) -> prod#(X1,X2)
   prod#(X1,mark(X2)) -> prod#(X1,X2)
   prod#(active(X1),X2) -> prod#(X1,X2)
   prod#(X1,active(X2)) -> prod#(X1,X2)
   p#(mark(X)) -> p#(X)
   p#(active(X)) -> p#(X)
   add#(mark(X1),X2) -> add#(X1,X2)
   add#(X1,mark(X2)) -> add#(X1,X2)
   add#(active(X1),X2) -> add#(X1,X2)
   add#(X1,active(X2)) -> add#(X1,X2)
  TRS:
   active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X)))))
   active(add(0(),X)) -> mark(X)
   active(add(s(X),Y)) -> mark(s(add(X,Y)))
   active(prod(0(),X)) -> mark(0())
   active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y)))
   active(if(true(),X,Y)) -> mark(X)
   active(if(false(),X,Y)) -> mark(Y)
   active(zero(0())) -> mark(true())
   active(zero(s(X))) -> mark(false())
   active(p(s(X))) -> mark(X)
   mark(fact(X)) -> active(fact(mark(X)))
   mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
   mark(zero(X)) -> active(zero(mark(X)))
   mark(s(X)) -> active(s(mark(X)))
   mark(0()) -> active(0())
   mark(prod(X1,X2)) -> active(prod(mark(X1),mark(X2)))
   mark(p(X)) -> active(p(mark(X)))
   mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
   mark(true()) -> active(true())
   mark(false()) -> active(false())
   fact(mark(X)) -> fact(X)
   fact(active(X)) -> fact(X)
   if(mark(X1),X2,X3) -> if(X1,X2,X3)
   if(X1,mark(X2),X3) -> if(X1,X2,X3)
   if(X1,X2,mark(X3)) -> if(X1,X2,X3)
   if(active(X1),X2,X3) -> if(X1,X2,X3)
   if(X1,active(X2),X3) -> if(X1,X2,X3)
   if(X1,X2,active(X3)) -> if(X1,X2,X3)
   zero(mark(X)) -> zero(X)
   zero(active(X)) -> zero(X)
   s(mark(X)) -> s(X)
   s(active(X)) -> s(X)
   prod(mark(X1),X2) -> prod(X1,X2)
   prod(X1,mark(X2)) -> prod(X1,X2)
   prod(active(X1),X2) -> prod(X1,X2)
   prod(X1,active(X2)) -> prod(X1,X2)
   p(mark(X)) -> p(X)
   p(active(X)) -> p(X)
   add(mark(X1),X2) -> add(X1,X2)
   add(X1,mark(X2)) -> add(X1,X2)
   add(active(X1),X2) -> add(X1,X2)
   add(X1,active(X2)) -> add(X1,X2)
  TDG Processor:
   DPs:
    active#(fact(X)) -> p#(X)
    active#(fact(X)) -> fact#(p(X))
    active#(fact(X)) -> prod#(X,fact(p(X)))
    active#(fact(X)) -> s#(0())
    active#(fact(X)) -> zero#(X)
    active#(fact(X)) -> if#(zero(X),s(0()),prod(X,fact(p(X))))
    active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X)))))
    active#(add(0(),X)) -> mark#(X)
    active#(add(s(X),Y)) -> add#(X,Y)
    active#(add(s(X),Y)) -> s#(add(X,Y))
    active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
    active#(prod(0(),X)) -> mark#(0())
    active#(prod(s(X),Y)) -> prod#(X,Y)
    active#(prod(s(X),Y)) -> add#(Y,prod(X,Y))
    active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y)))
    active#(if(true(),X,Y)) -> mark#(X)
    active#(if(false(),X,Y)) -> mark#(Y)
    active#(zero(0())) -> mark#(true())
    active#(zero(s(X))) -> mark#(false())
    active#(p(s(X))) -> mark#(X)
    mark#(fact(X)) -> mark#(X)
    mark#(fact(X)) -> fact#(mark(X))
    mark#(fact(X)) -> active#(fact(mark(X)))
    mark#(if(X1,X2,X3)) -> mark#(X1)
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    mark#(zero(X)) -> mark#(X)
    mark#(zero(X)) -> zero#(mark(X))
    mark#(zero(X)) -> active#(zero(mark(X)))
    mark#(s(X)) -> mark#(X)
    mark#(s(X)) -> s#(mark(X))
    mark#(s(X)) -> active#(s(mark(X)))
    mark#(0()) -> active#(0())
    mark#(prod(X1,X2)) -> mark#(X2)
    mark#(prod(X1,X2)) -> mark#(X1)
    mark#(prod(X1,X2)) -> prod#(mark(X1),mark(X2))
    mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
    mark#(p(X)) -> mark#(X)
    mark#(p(X)) -> p#(mark(X))
    mark#(p(X)) -> active#(p(mark(X)))
    mark#(add(X1,X2)) -> mark#(X2)
    mark#(add(X1,X2)) -> mark#(X1)
    mark#(add(X1,X2)) -> add#(mark(X1),mark(X2))
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
    mark#(true()) -> active#(true())
    mark#(false()) -> active#(false())
    fact#(mark(X)) -> fact#(X)
    fact#(active(X)) -> fact#(X)
    if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
    if#(X1,mark(X2),X3) -> if#(X1,X2,X3)
    if#(X1,X2,mark(X3)) -> if#(X1,X2,X3)
    if#(active(X1),X2,X3) -> if#(X1,X2,X3)
    if#(X1,active(X2),X3) -> if#(X1,X2,X3)
    if#(X1,X2,active(X3)) -> if#(X1,X2,X3)
    zero#(mark(X)) -> zero#(X)
    zero#(active(X)) -> zero#(X)
    s#(mark(X)) -> s#(X)
    s#(active(X)) -> s#(X)
    prod#(mark(X1),X2) -> prod#(X1,X2)
    prod#(X1,mark(X2)) -> prod#(X1,X2)
    prod#(active(X1),X2) -> prod#(X1,X2)
    prod#(X1,active(X2)) -> prod#(X1,X2)
    p#(mark(X)) -> p#(X)
    p#(active(X)) -> p#(X)
    add#(mark(X1),X2) -> add#(X1,X2)
    add#(X1,mark(X2)) -> add#(X1,X2)
    add#(active(X1),X2) -> add#(X1,X2)
    add#(X1,active(X2)) -> add#(X1,X2)
   TRS:
    active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X)))))
    active(add(0(),X)) -> mark(X)
    active(add(s(X),Y)) -> mark(s(add(X,Y)))
    active(prod(0(),X)) -> mark(0())
    active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y)))
    active(if(true(),X,Y)) -> mark(X)
    active(if(false(),X,Y)) -> mark(Y)
    active(zero(0())) -> mark(true())
    active(zero(s(X))) -> mark(false())
    active(p(s(X))) -> mark(X)
    mark(fact(X)) -> active(fact(mark(X)))
    mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
    mark(zero(X)) -> active(zero(mark(X)))
    mark(s(X)) -> active(s(mark(X)))
    mark(0()) -> active(0())
    mark(prod(X1,X2)) -> active(prod(mark(X1),mark(X2)))
    mark(p(X)) -> active(p(mark(X)))
    mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
    mark(true()) -> active(true())
    mark(false()) -> active(false())
    fact(mark(X)) -> fact(X)
    fact(active(X)) -> fact(X)
    if(mark(X1),X2,X3) -> if(X1,X2,X3)
    if(X1,mark(X2),X3) -> if(X1,X2,X3)
    if(X1,X2,mark(X3)) -> if(X1,X2,X3)
    if(active(X1),X2,X3) -> if(X1,X2,X3)
    if(X1,active(X2),X3) -> if(X1,X2,X3)
    if(X1,X2,active(X3)) -> if(X1,X2,X3)
    zero(mark(X)) -> zero(X)
    zero(active(X)) -> zero(X)
    s(mark(X)) -> s(X)
    s(active(X)) -> s(X)
    prod(mark(X1),X2) -> prod(X1,X2)
    prod(X1,mark(X2)) -> prod(X1,X2)
    prod(active(X1),X2) -> prod(X1,X2)
    prod(X1,active(X2)) -> prod(X1,X2)
    p(mark(X)) -> p(X)
    p(active(X)) -> p(X)
    add(mark(X1),X2) -> add(X1,X2)
    add(X1,mark(X2)) -> add(X1,X2)
    add(active(X1),X2) -> add(X1,X2)
    add(X1,active(X2)) -> add(X1,X2)
   graph:
    add#(mark(X1),X2) -> add#(X1,X2) ->
    add#(X1,active(X2)) -> add#(X1,X2)
    add#(mark(X1),X2) -> add#(X1,X2) ->
    add#(active(X1),X2) -> add#(X1,X2)
    add#(mark(X1),X2) -> add#(X1,X2) ->
    add#(X1,mark(X2)) -> add#(X1,X2)
    add#(mark(X1),X2) -> add#(X1,X2) ->
    add#(mark(X1),X2) -> add#(X1,X2)
    add#(active(X1),X2) -> add#(X1,X2) ->
    add#(X1,active(X2)) -> add#(X1,X2)
    add#(active(X1),X2) -> add#(X1,X2) ->
    add#(active(X1),X2) -> add#(X1,X2)
    add#(active(X1),X2) -> add#(X1,X2) ->
    add#(X1,mark(X2)) -> add#(X1,X2)
    add#(active(X1),X2) -> add#(X1,X2) ->
    add#(mark(X1),X2) -> add#(X1,X2)
    add#(X1,mark(X2)) -> add#(X1,X2) ->
    add#(X1,active(X2)) -> add#(X1,X2)
    add#(X1,mark(X2)) -> add#(X1,X2) ->
    add#(active(X1),X2) -> add#(X1,X2)
    add#(X1,mark(X2)) -> add#(X1,X2) ->
    add#(X1,mark(X2)) -> add#(X1,X2)
    add#(X1,mark(X2)) -> add#(X1,X2) ->
    add#(mark(X1),X2) -> add#(X1,X2)
    add#(X1,active(X2)) -> add#(X1,X2) ->
    add#(X1,active(X2)) -> add#(X1,X2)
    add#(X1,active(X2)) -> add#(X1,X2) ->
    add#(active(X1),X2) -> add#(X1,X2)
    add#(X1,active(X2)) -> add#(X1,X2) ->
    add#(X1,mark(X2)) -> add#(X1,X2)
    add#(X1,active(X2)) -> add#(X1,X2) ->
    add#(mark(X1),X2) -> add#(X1,X2)
    mark#(false()) -> active#(false()) ->
    active#(p(s(X))) -> mark#(X)
    mark#(false()) -> active#(false()) ->
    active#(zero(s(X))) -> mark#(false())
    mark#(false()) -> active#(false()) ->
    active#(zero(0())) -> mark#(true())
    mark#(false()) -> active#(false()) ->
    active#(if(false(),X,Y)) -> mark#(Y)
    mark#(false()) -> active#(false()) ->
    active#(if(true(),X,Y)) -> mark#(X)
    mark#(false()) -> active#(false()) ->
    active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y)))
    mark#(false()) -> active#(false()) ->
    active#(prod(s(X),Y)) -> add#(Y,prod(X,Y))
    mark#(false()) -> active#(false()) ->
    active#(prod(s(X),Y)) -> prod#(X,Y)
    mark#(false()) -> active#(false()) ->
    active#(prod(0(),X)) -> mark#(0())
    mark#(false()) -> active#(false()) ->
    active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
    mark#(false()) -> active#(false()) ->
    active#(add(s(X),Y)) -> s#(add(X,Y))
    mark#(false()) -> active#(false()) ->
    active#(add(s(X),Y)) -> add#(X,Y)
    mark#(false()) -> active#(false()) ->
    active#(add(0(),X)) -> mark#(X)
    mark#(false()) -> active#(false()) ->
    active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X)))))
    mark#(false()) -> active#(false()) ->
    active#(fact(X)) -> if#(zero(X),s(0()),prod(X,fact(p(X))))
    mark#(false()) -> active#(false()) ->
    active#(fact(X)) -> zero#(X)
    mark#(false()) -> active#(false()) ->
    active#(fact(X)) -> s#(0())
    mark#(false()) -> active#(false()) ->
    active#(fact(X)) -> prod#(X,fact(p(X)))
    mark#(false()) -> active#(false()) ->
    active#(fact(X)) -> fact#(p(X))
    mark#(false()) -> active#(false()) -> active#(fact(X)) -> p#(X)
    mark#(true()) -> active#(true()) ->
    active#(p(s(X))) -> mark#(X)
    mark#(true()) -> active#(true()) ->
    active#(zero(s(X))) -> mark#(false())
    mark#(true()) -> active#(true()) ->
    active#(zero(0())) -> mark#(true())
    mark#(true()) -> active#(true()) ->
    active#(if(false(),X,Y)) -> mark#(Y)
    mark#(true()) -> active#(true()) ->
    active#(if(true(),X,Y)) -> mark#(X)
    mark#(true()) -> active#(true()) ->
    active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y)))
    mark#(true()) -> active#(true()) ->
    active#(prod(s(X),Y)) -> add#(Y,prod(X,Y))
    mark#(true()) -> active#(true()) ->
    active#(prod(s(X),Y)) -> prod#(X,Y)
    mark#(true()) -> active#(true()) ->
    active#(prod(0(),X)) -> mark#(0())
    mark#(true()) -> active#(true()) ->
    active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
    mark#(true()) -> active#(true()) ->
    active#(add(s(X),Y)) -> s#(add(X,Y))
    mark#(true()) -> active#(true()) ->
    active#(add(s(X),Y)) -> add#(X,Y)
    mark#(true()) -> active#(true()) ->
    active#(add(0(),X)) -> mark#(X)
    mark#(true()) -> active#(true()) ->
    active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X)))))
    mark#(true()) -> active#(true()) ->
    active#(fact(X)) -> if#(zero(X),s(0()),prod(X,fact(p(X))))
    mark#(true()) -> active#(true()) ->
    active#(fact(X)) -> zero#(X)
    mark#(true()) -> active#(true()) -> active#(fact(X)) -> s#(0())
    mark#(true()) -> active#(true()) ->
    active#(fact(X)) -> prod#(X,fact(p(X)))
    mark#(true()) -> active#(true()) ->
    active#(fact(X)) -> fact#(p(X))
    mark#(true()) -> active#(true()) ->
    active#(fact(X)) -> p#(X)
    mark#(add(X1,X2)) -> add#(mark(X1),mark(X2)) ->
    add#(X1,active(X2)) -> add#(X1,X2)
    mark#(add(X1,X2)) -> add#(mark(X1),mark(X2)) ->
    add#(active(X1),X2) -> add#(X1,X2)
    mark#(add(X1,X2)) -> add#(mark(X1),mark(X2)) ->
    add#(X1,mark(X2)) -> add#(X1,X2)
    mark#(add(X1,X2)) -> add#(mark(X1),mark(X2)) ->
    add#(mark(X1),X2) -> add#(X1,X2)
    mark#(add(X1,X2)) -> mark#(X2) ->
    mark#(false()) -> active#(false())
    mark#(add(X1,X2)) -> mark#(X2) ->
    mark#(true()) -> active#(true())
    mark#(add(X1,X2)) -> mark#(X2) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
    mark#(add(X1,X2)) -> mark#(X2) ->
    mark#(add(X1,X2)) -> add#(mark(X1),mark(X2))
    mark#(add(X1,X2)) -> mark#(X2) -> mark#(add(X1,X2)) -> mark#(X1)
    mark#(add(X1,X2)) -> mark#(X2) -> mark#(add(X1,X2)) -> mark#(X2)
    mark#(add(X1,X2)) -> mark#(X2) ->
    mark#(p(X)) -> active#(p(mark(X)))
    mark#(add(X1,X2)) -> mark#(X2) -> mark#(p(X)) -> p#(mark(X))
    mark#(add(X1,X2)) -> mark#(X2) -> mark#(p(X)) -> mark#(X)
    mark#(add(X1,X2)) -> mark#(X2) ->
    mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
    mark#(add(X1,X2)) -> mark#(X2) ->
    mark#(prod(X1,X2)) -> prod#(mark(X1),mark(X2))
    mark#(add(X1,X2)) -> mark#(X2) -> mark#(prod(X1,X2)) -> mark#(X1)
    mark#(add(X1,X2)) -> mark#(X2) -> mark#(prod(X1,X2)) -> mark#(X2)
    mark#(add(X1,X2)) -> mark#(X2) -> mark#(0()) -> active#(0())
    mark#(add(X1,X2)) -> mark#(X2) ->
    mark#(s(X)) -> active#(s(mark(X)))
    mark#(add(X1,X2)) -> mark#(X2) -> mark#(s(X)) -> s#(mark(X))
    mark#(add(X1,X2)) -> mark#(X2) -> mark#(s(X)) -> mark#(X)
    mark#(add(X1,X2)) -> mark#(X2) ->
    mark#(zero(X)) -> active#(zero(mark(X)))
    mark#(add(X1,X2)) -> mark#(X2) ->
    mark#(zero(X)) -> zero#(mark(X))
    mark#(add(X1,X2)) -> mark#(X2) -> mark#(zero(X)) -> mark#(X)
    mark#(add(X1,X2)) -> mark#(X2) ->
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    mark#(add(X1,X2)) -> mark#(X2) ->
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
    mark#(add(X1,X2)) -> mark#(X2) ->
    mark#(if(X1,X2,X3)) -> mark#(X1)
    mark#(add(X1,X2)) -> mark#(X2) ->
    mark#(fact(X)) -> active#(fact(mark(X)))
    mark#(add(X1,X2)) -> mark#(X2) ->
    mark#(fact(X)) -> fact#(mark(X))
    mark#(add(X1,X2)) -> mark#(X2) -> mark#(fact(X)) -> mark#(X)
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(false()) -> active#(false())
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(true()) -> active#(true())
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(add(X1,X2)) -> add#(mark(X1),mark(X2))
    mark#(add(X1,X2)) -> mark#(X1) -> mark#(add(X1,X2)) -> mark#(X1)
    mark#(add(X1,X2)) -> mark#(X1) -> mark#(add(X1,X2)) -> mark#(X2)
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(p(X)) -> active#(p(mark(X)))
    mark#(add(X1,X2)) -> mark#(X1) -> mark#(p(X)) -> p#(mark(X))
    mark#(add(X1,X2)) -> mark#(X1) -> mark#(p(X)) -> mark#(X)
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(prod(X1,X2)) -> prod#(mark(X1),mark(X2))
    mark#(add(X1,X2)) -> mark#(X1) -> mark#(prod(X1,X2)) -> mark#(X1)
    mark#(add(X1,X2)) -> mark#(X1) -> mark#(prod(X1,X2)) -> mark#(X2)
    mark#(add(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(s(X)) -> active#(s(mark(X)))
    mark#(add(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> s#(mark(X))
    mark#(add(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(zero(X)) -> active#(zero(mark(X)))
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(zero(X)) -> zero#(mark(X))
    mark#(add(X1,X2)) -> mark#(X1) -> mark#(zero(X)) -> mark#(X)
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(if(X1,X2,X3)) -> mark#(X1)
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(fact(X)) -> active#(fact(mark(X)))
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(fact(X)) -> fact#(mark(X))
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(fact(X)) -> mark#(X)
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
    active#(p(s(X))) -> mark#(X)
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
    active#(zero(s(X))) -> mark#(false())
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
    active#(zero(0())) -> mark#(true())
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
    active#(if(false(),X,Y)) -> mark#(Y)
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
    active#(if(true(),X,Y)) -> mark#(X)
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
    active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y)))
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
    active#(prod(s(X),Y)) -> add#(Y,prod(X,Y))
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
    active#(prod(s(X),Y)) -> prod#(X,Y)
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
    active#(prod(0(),X)) -> mark#(0())
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
    active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
    active#(add(s(X),Y)) -> s#(add(X,Y))
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
    active#(add(s(X),Y)) -> add#(X,Y)
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
    active#(add(0(),X)) -> mark#(X)
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
    active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X)))))
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
    active#(fact(X)) -> if#(zero(X),s(0()),prod(X,fact(p(X))))
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
    active#(fact(X)) -> zero#(X)
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
    active#(fact(X)) -> s#(0())
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
    active#(fact(X)) -> prod#(X,fact(p(X)))
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
    active#(fact(X)) -> fact#(p(X))
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
    active#(fact(X)) -> p#(X)
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(false()) -> active#(false())
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(true()) -> active#(true())
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(add(X1,X2)) -> add#(mark(X1),mark(X2))
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(add(X1,X2)) -> mark#(X1)
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(add(X1,X2)) -> mark#(X2)
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(p(X)) -> active#(p(mark(X)))
    mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(p(X)) -> p#(mark(X))
    mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(p(X)) -> mark#(X)
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(prod(X1,X2)) -> prod#(mark(X1),mark(X2))
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(prod(X1,X2)) -> mark#(X1)
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(prod(X1,X2)) -> mark#(X2)
    mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(0()) -> active#(0())
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(s(X)) -> active#(s(mark(X)))
    mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(s(X)) -> s#(mark(X))
    mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(zero(X)) -> active#(zero(mark(X)))
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(zero(X)) -> zero#(mark(X))
    mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(zero(X)) -> mark#(X)
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(if(X1,X2,X3)) -> mark#(X1)
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(fact(X)) -> active#(fact(mark(X)))
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(fact(X)) -> fact#(mark(X))
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(fact(X)) -> mark#(X)
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3) ->
    if#(X1,X2,active(X3)) -> if#(X1,X2,X3)
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3) ->
    if#(X1,active(X2),X3) -> if#(X1,X2,X3)
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3) ->
    if#(active(X1),X2,X3) -> if#(X1,X2,X3)
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3) ->
    if#(X1,X2,mark(X3)) -> if#(X1,X2,X3)
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3) ->
    if#(X1,mark(X2),X3) -> if#(X1,X2,X3)
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3) ->
    if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(p(s(X))) -> mark#(X)
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(zero(s(X))) -> mark#(false())
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(zero(0())) -> mark#(true())
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(if(false(),X,Y)) -> mark#(Y)
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(if(true(),X,Y)) -> mark#(X)
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y)))
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(prod(s(X),Y)) -> add#(Y,prod(X,Y))
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(prod(s(X),Y)) -> prod#(X,Y)
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(prod(0(),X)) -> mark#(0())
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(add(s(X),Y)) -> s#(add(X,Y))
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(add(s(X),Y)) -> add#(X,Y)
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(add(0(),X)) -> mark#(X)
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X)))))
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(fact(X)) -> if#(zero(X),s(0()),prod(X,fact(p(X))))
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(fact(X)) -> zero#(X)
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(fact(X)) -> s#(0())
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(fact(X)) -> prod#(X,fact(p(X)))
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(fact(X)) -> fact#(p(X))
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
    active#(fact(X)) -> p#(X)
    mark#(prod(X1,X2)) -> mark#(X2) ->
    mark#(false()) -> active#(false())
    mark#(prod(X1,X2)) -> mark#(X2) ->
    mark#(true()) -> active#(true())
    mark#(prod(X1,X2)) -> mark#(X2) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
    mark#(prod(X1,X2)) -> mark#(X2) ->
    mark#(add(X1,X2)) -> add#(mark(X1),mark(X2))
    mark#(prod(X1,X2)) -> mark#(X2) ->
    mark#(add(X1,X2)) -> mark#(X1)
    mark#(prod(X1,X2)) -> mark#(X2) ->
    mark#(add(X1,X2)) -> mark#(X2)
    mark#(prod(X1,X2)) -> mark#(X2) ->
    mark#(p(X)) -> active#(p(mark(X)))
    mark#(prod(X1,X2)) -> mark#(X2) -> mark#(p(X)) -> p#(mark(X))
    mark#(prod(X1,X2)) -> mark#(X2) -> mark#(p(X)) -> mark#(X)
    mark#(prod(X1,X2)) -> mark#(X2) ->
    mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
    mark#(prod(X1,X2)) -> mark#(X2) ->
    mark#(prod(X1,X2)) -> prod#(mark(X1),mark(X2))
    mark#(prod(X1,X2)) -> mark#(X2) ->
    mark#(prod(X1,X2)) -> mark#(X1)
    mark#(prod(X1,X2)) -> mark#(X2) ->
    mark#(prod(X1,X2)) -> mark#(X2)
    mark#(prod(X1,X2)) -> mark#(X2) -> mark#(0()) -> active#(0())
    mark#(prod(X1,X2)) -> mark#(X2) ->
    mark#(s(X)) -> active#(s(mark(X)))
    mark#(prod(X1,X2)) -> mark#(X2) -> mark#(s(X)) -> s#(mark(X))
    mark#(prod(X1,X2)) -> mark#(X2) -> mark#(s(X)) -> mark#(X)
    mark#(prod(X1,X2)) -> mark#(X2) ->
    mark#(zero(X)) -> active#(zero(mark(X)))
    mark#(prod(X1,X2)) -> mark#(X2) ->
    mark#(zero(X)) -> zero#(mark(X))
    mark#(prod(X1,X2)) -> mark#(X2) -> mark#(zero(X)) -> mark#(X)
    mark#(prod(X1,X2)) -> mark#(X2) ->
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    mark#(prod(X1,X2)) -> mark#(X2) ->
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
    mark#(prod(X1,X2)) -> mark#(X2) ->
    mark#(if(X1,X2,X3)) -> mark#(X1)
    mark#(prod(X1,X2)) -> mark#(X2) ->
    mark#(fact(X)) -> active#(fact(mark(X)))
    mark#(prod(X1,X2)) -> mark#(X2) ->
    mark#(fact(X)) -> fact#(mark(X))
    mark#(prod(X1,X2)) -> mark#(X2) -> mark#(fact(X)) -> mark#(X)
    mark#(prod(X1,X2)) -> mark#(X1) ->
    mark#(false()) -> active#(false())
    mark#(prod(X1,X2)) -> mark#(X1) ->
    mark#(true()) -> active#(true())
    mark#(prod(X1,X2)) -> mark#(X1) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
    mark#(prod(X1,X2)) -> mark#(X1) ->
    mark#(add(X1,X2)) -> add#(mark(X1),mark(X2))
    mark#(prod(X1,X2)) -> mark#(X1) ->
    mark#(add(X1,X2)) -> mark#(X1)
    mark#(prod(X1,X2)) -> mark#(X1) ->
    mark#(add(X1,X2)) -> mark#(X2)
    mark#(prod(X1,X2)) -> mark#(X1) ->
    mark#(p(X)) -> active#(p(mark(X)))
    mark#(prod(X1,X2)) -> mark#(X1) -> mark#(p(X)) -> p#(mark(X))
    mark#(prod(X1,X2)) -> mark#(X1) -> mark#(p(X)) -> mark#(X)
    mark#(prod(X1,X2)) -> mark#(X1) ->
    mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
    mark#(prod(X1,X2)) -> mark#(X1) ->
    mark#(prod(X1,X2)) -> prod#(mark(X1),mark(X2))
    mark#(prod(X1,X2)) -> mark#(X1) ->
    mark#(prod(X1,X2)) -> mark#(X1)
    mark#(prod(X1,X2)) -> mark#(X1) ->
    mark#(prod(X1,X2)) -> mark#(X2)
    mark#(prod(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
    mark#(prod(X1,X2)) -> mark#(X1) ->
    mark#(s(X)) -> active#(s(mark(X)))
    mark#(prod(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> s#(mark(X))
    mark#(prod(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
    mark#(prod(X1,X2)) -> mark#(X1) ->
    mark#(zero(X)) -> active#(zero(mark(X)))
    mark#(prod(X1,X2)) -> mark#(X1) ->
    mark#(zero(X)) -> zero#(mark(X))
    mark#(prod(X1,X2)) -> mark#(X1) -> mark#(zero(X)) -> mark#(X)
    mark#(prod(X1,X2)) -> mark#(X1) ->
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    mark#(prod(X1,X2)) -> mark#(X1) ->
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
    mark#(prod(X1,X2)) -> mark#(X1) ->
    mark#(if(X1,X2,X3)) -> mark#(X1)
    mark#(prod(X1,X2)) -> mark#(X1) ->
    mark#(fact(X)) -> active#(fact(mark(X)))
    mark#(prod(X1,X2)) -> mark#(X1) ->
    mark#(fact(X)) -> fact#(mark(X))
    mark#(prod(X1,X2)) -> mark#(X1) ->
    mark#(fact(X)) -> mark#(X)
    mark#(prod(X1,X2)) -> prod#(mark(X1),mark(X2)) ->
    prod#(X1,active(X2)) -> prod#(X1,X2)
    mark#(prod(X1,X2)) -> prod#(mark(X1),mark(X2)) ->
    prod#(active(X1),X2) -> prod#(X1,X2)
    mark#(prod(X1,X2)) -> prod#(mark(X1),mark(X2)) ->
    prod#(X1,mark(X2)) -> prod#(X1,X2)
    mark#(prod(X1,X2)) -> prod#(mark(X1),mark(X2)) ->
    prod#(mark(X1),X2) -> prod#(X1,X2)
    mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2))) ->
    active#(p(s(X))) -> mark#(X)
    mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2))) ->
    active#(zero(s(X))) -> mark#(false())
    mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2))) ->
    active#(zero(0())) -> mark#(true())
    mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2))) ->
    active#(if(false(),X,Y)) -> mark#(Y)
    mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2))) ->
    active#(if(true(),X,Y)) -> mark#(X)
    mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2))) ->
    active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y)))
    mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2))) ->
    active#(prod(s(X),Y)) -> add#(Y,prod(X,Y))
    mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2))) ->
    active#(prod(s(X),Y)) -> prod#(X,Y)
    mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2))) ->
    active#(prod(0(),X)) -> mark#(0())
    mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2))) ->
    active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
    mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2))) ->
    active#(add(s(X),Y)) -> s#(add(X,Y))
    mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2))) ->
    active#(add(s(X),Y)) -> add#(X,Y)
    mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2))) ->
    active#(add(0(),X)) -> mark#(X)
    mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2))) ->
    active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X)))))
    mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2))) ->
    active#(fact(X)) -> if#(zero(X),s(0()),prod(X,fact(p(X))))
    mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2))) ->
    active#(fact(X)) -> zero#(X)
    mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2))) ->
    active#(fact(X)) -> s#(0())
    mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2))) ->
    active#(fact(X)) -> prod#(X,fact(p(X)))
    mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2))) ->
    active#(fact(X)) -> fact#(p(X))
    mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2))) ->
    active#(fact(X)) -> p#(X)
    mark#(p(X)) -> mark#(X) -> mark#(false()) -> active#(false())
    mark#(p(X)) -> mark#(X) -> mark#(true()) -> active#(true())
    mark#(p(X)) -> mark#(X) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
    mark#(p(X)) -> mark#(X) -> mark#(add(X1,X2)) -> add#(mark(X1),mark(X2))
    mark#(p(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1)
    mark#(p(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2)
    mark#(p(X)) -> mark#(X) -> mark#(p(X)) -> active#(p(mark(X)))
    mark#(p(X)) -> mark#(X) -> mark#(p(X)) -> p#(mark(X))
    mark#(p(X)) -> mark#(X) -> mark#(p(X)) -> mark#(X)
    mark#(p(X)) -> mark#(X) ->
    mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
    mark#(p(X)) -> mark#(X) ->
    mark#(prod(X1,X2)) -> prod#(mark(X1),mark(X2))
    mark#(p(X)) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X1)
    mark#(p(X)) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X2)
    mark#(p(X)) -> mark#(X) -> mark#(0()) -> active#(0())
    mark#(p(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
    mark#(p(X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X))
    mark#(p(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    mark#(p(X)) -> mark#(X) -> mark#(zero(X)) -> active#(zero(mark(X)))
    mark#(p(X)) -> mark#(X) -> mark#(zero(X)) -> zero#(mark(X))
    mark#(p(X)) -> mark#(X) -> mark#(zero(X)) -> mark#(X)
    mark#(p(X)) -> mark#(X) ->
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    mark#(p(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
    mark#(p(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1)
    mark#(p(X)) -> mark#(X) -> mark#(fact(X)) -> active#(fact(mark(X)))
    mark#(p(X)) -> mark#(X) -> mark#(fact(X)) -> fact#(mark(X))
    mark#(p(X)) -> mark#(X) -> mark#(fact(X)) -> mark#(X)
    mark#(p(X)) -> p#(mark(X)) -> p#(active(X)) -> p#(X)
    mark#(p(X)) -> p#(mark(X)) -> p#(mark(X)) -> p#(X)
    mark#(p(X)) -> active#(p(mark(X))) ->
    active#(p(s(X))) -> mark#(X)
    mark#(p(X)) -> active#(p(mark(X))) ->
    active#(zero(s(X))) -> mark#(false())
    mark#(p(X)) -> active#(p(mark(X))) ->
    active#(zero(0())) -> mark#(true())
    mark#(p(X)) -> active#(p(mark(X))) ->
    active#(if(false(),X,Y)) -> mark#(Y)
    mark#(p(X)) -> active#(p(mark(X))) ->
    active#(if(true(),X,Y)) -> mark#(X)
    mark#(p(X)) -> active#(p(mark(X))) ->
    active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y)))
    mark#(p(X)) -> active#(p(mark(X))) ->
    active#(prod(s(X),Y)) -> add#(Y,prod(X,Y))
    mark#(p(X)) -> active#(p(mark(X))) ->
    active#(prod(s(X),Y)) -> prod#(X,Y)
    mark#(p(X)) -> active#(p(mark(X))) ->
    active#(prod(0(),X)) -> mark#(0())
    mark#(p(X)) -> active#(p(mark(X))) ->
    active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
    mark#(p(X)) -> active#(p(mark(X))) ->
    active#(add(s(X),Y)) -> s#(add(X,Y))
    mark#(p(X)) -> active#(p(mark(X))) ->
    active#(add(s(X),Y)) -> add#(X,Y)
    mark#(p(X)) -> active#(p(mark(X))) ->
    active#(add(0(),X)) -> mark#(X)
    mark#(p(X)) -> active#(p(mark(X))) ->
    active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X)))))
    mark#(p(X)) -> active#(p(mark(X))) ->
    active#(fact(X)) -> if#(zero(X),s(0()),prod(X,fact(p(X))))
    mark#(p(X)) -> active#(p(mark(X))) ->
    active#(fact(X)) -> zero#(X)
    mark#(p(X)) -> active#(p(mark(X))) ->
    active#(fact(X)) -> s#(0())
    mark#(p(X)) -> active#(p(mark(X))) ->
    active#(fact(X)) -> prod#(X,fact(p(X)))
    mark#(p(X)) -> active#(p(mark(X))) ->
    active#(fact(X)) -> fact#(p(X))
    mark#(p(X)) -> active#(p(mark(X))) -> active#(fact(X)) -> p#(X)
    mark#(s(X)) -> mark#(X) -> mark#(false()) -> active#(false())
    mark#(s(X)) -> mark#(X) -> mark#(true()) -> active#(true())
    mark#(s(X)) -> mark#(X) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
    mark#(s(X)) -> mark#(X) -> mark#(add(X1,X2)) -> add#(mark(X1),mark(X2))
    mark#(s(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1)
    mark#(s(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2)
    mark#(s(X)) -> mark#(X) -> mark#(p(X)) -> active#(p(mark(X)))
    mark#(s(X)) -> mark#(X) -> mark#(p(X)) -> p#(mark(X))
    mark#(s(X)) -> mark#(X) -> mark#(p(X)) -> mark#(X)
    mark#(s(X)) -> mark#(X) ->
    mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
    mark#(s(X)) -> mark#(X) ->
    mark#(prod(X1,X2)) -> prod#(mark(X1),mark(X2))
    mark#(s(X)) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X1)
    mark#(s(X)) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X2)
    mark#(s(X)) -> mark#(X) -> mark#(0()) -> active#(0())
    mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
    mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X))
    mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    mark#(s(X)) -> mark#(X) -> mark#(zero(X)) -> active#(zero(mark(X)))
    mark#(s(X)) -> mark#(X) -> mark#(zero(X)) -> zero#(mark(X))
    mark#(s(X)) -> mark#(X) -> mark#(zero(X)) -> mark#(X)
    mark#(s(X)) -> mark#(X) ->
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    mark#(s(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
    mark#(s(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1)
    mark#(s(X)) -> mark#(X) -> mark#(fact(X)) -> active#(fact(mark(X)))
    mark#(s(X)) -> mark#(X) -> mark#(fact(X)) -> fact#(mark(X))
    mark#(s(X)) -> mark#(X) -> mark#(fact(X)) -> mark#(X)
    mark#(s(X)) -> s#(mark(X)) -> s#(active(X)) -> s#(X)
    mark#(s(X)) -> s#(mark(X)) -> s#(mark(X)) -> s#(X)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(p(s(X))) -> mark#(X)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(zero(s(X))) -> mark#(false())
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(zero(0())) -> mark#(true())
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(if(false(),X,Y)) -> mark#(Y)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(if(true(),X,Y)) -> mark#(X)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y)))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(prod(s(X),Y)) -> add#(Y,prod(X,Y))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(prod(s(X),Y)) -> prod#(X,Y)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(prod(0(),X)) -> mark#(0())
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(add(s(X),Y)) -> s#(add(X,Y))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(add(s(X),Y)) -> add#(X,Y)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(add(0(),X)) -> mark#(X)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X)))))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(fact(X)) -> if#(zero(X),s(0()),prod(X,fact(p(X))))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(fact(X)) -> zero#(X)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(fact(X)) -> s#(0())
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(fact(X)) -> prod#(X,fact(p(X)))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(fact(X)) -> fact#(p(X))
    mark#(s(X)) -> active#(s(mark(X))) -> active#(fact(X)) -> p#(X)
    mark#(0()) -> active#(0()) -> active#(p(s(X))) -> mark#(X)
    mark#(0()) -> active#(0()) -> active#(zero(s(X))) -> mark#(false())
    mark#(0()) -> active#(0()) -> active#(zero(0())) -> mark#(true())
    mark#(0()) -> active#(0()) -> active#(if(false(),X,Y)) -> mark#(Y)
    mark#(0()) -> active#(0()) -> active#(if(true(),X,Y)) -> mark#(X)
    mark#(0()) -> active#(0()) ->
    active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y)))
    mark#(0()) -> active#(0()) ->
    active#(prod(s(X),Y)) -> add#(Y,prod(X,Y))
    mark#(0()) -> active#(0()) -> active#(prod(s(X),Y)) -> prod#(X,Y)
    mark#(0()) -> active#(0()) -> active#(prod(0(),X)) -> mark#(0())
    mark#(0()) -> active#(0()) ->
    active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
    mark#(0()) -> active#(0()) -> active#(add(s(X),Y)) -> s#(add(X,Y))
    mark#(0()) -> active#(0()) -> active#(add(s(X),Y)) -> add#(X,Y)
    mark#(0()) -> active#(0()) -> active#(add(0(),X)) -> mark#(X)
    mark#(0()) -> active#(0()) ->
    active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X)))))
    mark#(0()) -> active#(0()) ->
    active#(fact(X)) -> if#(zero(X),s(0()),prod(X,fact(p(X))))
    mark#(0()) -> active#(0()) -> active#(fact(X)) -> zero#(X)
    mark#(0()) -> active#(0()) -> active#(fact(X)) -> s#(0())
    mark#(0()) -> active#(0()) -> active#(fact(X)) -> prod#(X,fact(p(X)))
    mark#(0()) -> active#(0()) -> active#(fact(X)) -> fact#(p(X))
    mark#(0()) -> active#(0()) -> active#(fact(X)) -> p#(X)
    mark#(zero(X)) -> mark#(X) -> mark#(false()) -> active#(false())
    mark#(zero(X)) -> mark#(X) -> mark#(true()) -> active#(true())
    mark#(zero(X)) -> mark#(X) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
    mark#(zero(X)) -> mark#(X) ->
    mark#(add(X1,X2)) -> add#(mark(X1),mark(X2))
    mark#(zero(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1)
    mark#(zero(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2)
    mark#(zero(X)) -> mark#(X) -> mark#(p(X)) -> active#(p(mark(X)))
    mark#(zero(X)) -> mark#(X) -> mark#(p(X)) -> p#(mark(X))
    mark#(zero(X)) -> mark#(X) -> mark#(p(X)) -> mark#(X)
    mark#(zero(X)) -> mark#(X) ->
    mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
    mark#(zero(X)) -> mark#(X) ->
    mark#(prod(X1,X2)) -> prod#(mark(X1),mark(X2))
    mark#(zero(X)) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X1)
    mark#(zero(X)) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X2)
    mark#(zero(X)) -> mark#(X) -> mark#(0()) -> active#(0())
    mark#(zero(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
    mark#(zero(X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X))
    mark#(zero(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    mark#(zero(X)) -> mark#(X) ->
    mark#(zero(X)) -> active#(zero(mark(X)))
    mark#(zero(X)) -> mark#(X) -> mark#(zero(X)) -> zero#(mark(X))
    mark#(zero(X)) -> mark#(X) -> mark#(zero(X)) -> mark#(X)
    mark#(zero(X)) -> mark#(X) ->
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    mark#(zero(X)) -> mark#(X) ->
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
    mark#(zero(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1)
    mark#(zero(X)) -> mark#(X) ->
    mark#(fact(X)) -> active#(fact(mark(X)))
    mark#(zero(X)) -> mark#(X) -> mark#(fact(X)) -> fact#(mark(X))
    mark#(zero(X)) -> mark#(X) -> mark#(fact(X)) -> mark#(X)
    mark#(zero(X)) -> zero#(mark(X)) ->
    zero#(active(X)) -> zero#(X)
    mark#(zero(X)) -> zero#(mark(X)) ->
    zero#(mark(X)) -> zero#(X)
    mark#(zero(X)) -> active#(zero(mark(X))) ->
    active#(p(s(X))) -> mark#(X)
    mark#(zero(X)) -> active#(zero(mark(X))) ->
    active#(zero(s(X))) -> mark#(false())
    mark#(zero(X)) -> active#(zero(mark(X))) ->
    active#(zero(0())) -> mark#(true())
    mark#(zero(X)) -> active#(zero(mark(X))) ->
    active#(if(false(),X,Y)) -> mark#(Y)
    mark#(zero(X)) -> active#(zero(mark(X))) ->
    active#(if(true(),X,Y)) -> mark#(X)
    mark#(zero(X)) -> active#(zero(mark(X))) ->
    active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y)))
    mark#(zero(X)) -> active#(zero(mark(X))) ->
    active#(prod(s(X),Y)) -> add#(Y,prod(X,Y))
    mark#(zero(X)) -> active#(zero(mark(X))) ->
    active#(prod(s(X),Y)) -> prod#(X,Y)
    mark#(zero(X)) -> active#(zero(mark(X))) ->
    active#(prod(0(),X)) -> mark#(0())
    mark#(zero(X)) -> active#(zero(mark(X))) ->
    active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
    mark#(zero(X)) -> active#(zero(mark(X))) ->
    active#(add(s(X),Y)) -> s#(add(X,Y))
    mark#(zero(X)) -> active#(zero(mark(X))) ->
    active#(add(s(X),Y)) -> add#(X,Y)
    mark#(zero(X)) -> active#(zero(mark(X))) ->
    active#(add(0(),X)) -> mark#(X)
    mark#(zero(X)) -> active#(zero(mark(X))) ->
    active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X)))))
    mark#(zero(X)) -> active#(zero(mark(X))) ->
    active#(fact(X)) -> if#(zero(X),s(0()),prod(X,fact(p(X))))
    mark#(zero(X)) -> active#(zero(mark(X))) ->
    active#(fact(X)) -> zero#(X)
    mark#(zero(X)) -> active#(zero(mark(X))) ->
    active#(fact(X)) -> s#(0())
    mark#(zero(X)) -> active#(zero(mark(X))) ->
    active#(fact(X)) -> prod#(X,fact(p(X)))
    mark#(zero(X)) -> active#(zero(mark(X))) ->
    active#(fact(X)) -> fact#(p(X))
    mark#(zero(X)) -> active#(zero(mark(X))) -> active#(fact(X)) -> p#(X)
    mark#(fact(X)) -> mark#(X) -> mark#(false()) -> active#(false())
    mark#(fact(X)) -> mark#(X) -> mark#(true()) -> active#(true())
    mark#(fact(X)) -> mark#(X) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
    mark#(fact(X)) -> mark#(X) ->
    mark#(add(X1,X2)) -> add#(mark(X1),mark(X2))
    mark#(fact(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1)
    mark#(fact(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2)
    mark#(fact(X)) -> mark#(X) -> mark#(p(X)) -> active#(p(mark(X)))
    mark#(fact(X)) -> mark#(X) -> mark#(p(X)) -> p#(mark(X))
    mark#(fact(X)) -> mark#(X) -> mark#(p(X)) -> mark#(X)
    mark#(fact(X)) -> mark#(X) ->
    mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
    mark#(fact(X)) -> mark#(X) ->
    mark#(prod(X1,X2)) -> prod#(mark(X1),mark(X2))
    mark#(fact(X)) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X1)
    mark#(fact(X)) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X2)
    mark#(fact(X)) -> mark#(X) -> mark#(0()) -> active#(0())
    mark#(fact(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
    mark#(fact(X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X))
    mark#(fact(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    mark#(fact(X)) -> mark#(X) ->
    mark#(zero(X)) -> active#(zero(mark(X)))
    mark#(fact(X)) -> mark#(X) -> mark#(zero(X)) -> zero#(mark(X))
    mark#(fact(X)) -> mark#(X) -> mark#(zero(X)) -> mark#(X)
    mark#(fact(X)) -> mark#(X) ->
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    mark#(fact(X)) -> mark#(X) ->
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
    mark#(fact(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1)
    mark#(fact(X)) -> mark#(X) ->
    mark#(fact(X)) -> active#(fact(mark(X)))
    mark#(fact(X)) -> mark#(X) -> mark#(fact(X)) -> fact#(mark(X))
    mark#(fact(X)) -> mark#(X) -> mark#(fact(X)) -> mark#(X)
    mark#(fact(X)) -> fact#(mark(X)) ->
    fact#(active(X)) -> fact#(X)
    mark#(fact(X)) -> fact#(mark(X)) ->
    fact#(mark(X)) -> fact#(X)
    mark#(fact(X)) -> active#(fact(mark(X))) ->
    active#(p(s(X))) -> mark#(X)
    mark#(fact(X)) -> active#(fact(mark(X))) ->
    active#(zero(s(X))) -> mark#(false())
    mark#(fact(X)) -> active#(fact(mark(X))) ->
    active#(zero(0())) -> mark#(true())
    mark#(fact(X)) -> active#(fact(mark(X))) ->
    active#(if(false(),X,Y)) -> mark#(Y)
    mark#(fact(X)) -> active#(fact(mark(X))) ->
    active#(if(true(),X,Y)) -> mark#(X)
    mark#(fact(X)) -> active#(fact(mark(X))) ->
    active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y)))
    mark#(fact(X)) -> active#(fact(mark(X))) ->
    active#(prod(s(X),Y)) -> add#(Y,prod(X,Y))
    mark#(fact(X)) -> active#(fact(mark(X))) ->
    active#(prod(s(X),Y)) -> prod#(X,Y)
    mark#(fact(X)) -> active#(fact(mark(X))) ->
    active#(prod(0(),X)) -> mark#(0())
    mark#(fact(X)) -> active#(fact(mark(X))) ->
    active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
    mark#(fact(X)) -> active#(fact(mark(X))) ->
    active#(add(s(X),Y)) -> s#(add(X,Y))
    mark#(fact(X)) -> active#(fact(mark(X))) ->
    active#(add(s(X),Y)) -> add#(X,Y)
    mark#(fact(X)) -> active#(fact(mark(X))) ->
    active#(add(0(),X)) -> mark#(X)
    mark#(fact(X)) -> active#(fact(mark(X))) ->
    active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X)))))
    mark#(fact(X)) -> active#(fact(mark(X))) ->
    active#(fact(X)) -> if#(zero(X),s(0()),prod(X,fact(p(X))))
    mark#(fact(X)) -> active#(fact(mark(X))) ->
    active#(fact(X)) -> zero#(X)
    mark#(fact(X)) -> active#(fact(mark(X))) ->
    active#(fact(X)) -> s#(0())
    mark#(fact(X)) -> active#(fact(mark(X))) ->
    active#(fact(X)) -> prod#(X,fact(p(X)))
    mark#(fact(X)) -> active#(fact(mark(X))) ->
    active#(fact(X)) -> fact#(p(X))
    mark#(fact(X)) -> active#(fact(mark(X))) ->
    active#(fact(X)) -> p#(X)
    if#(mark(X1),X2,X3) -> if#(X1,X2,X3) ->
    if#(X1,X2,active(X3)) -> if#(X1,X2,X3)
    if#(mark(X1),X2,X3) -> if#(X1,X2,X3) ->
    if#(X1,active(X2),X3) -> if#(X1,X2,X3)
    if#(mark(X1),X2,X3) -> if#(X1,X2,X3) ->
    if#(active(X1),X2,X3) -> if#(X1,X2,X3)
    if#(mark(X1),X2,X3) -> if#(X1,X2,X3) ->
    if#(X1,X2,mark(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#(active(X1),X2,X3) -> if#(X1,X2,X3) ->
    if#(X1,X2,active(X3)) -> if#(X1,X2,X3)
    if#(active(X1),X2,X3) -> if#(X1,X2,X3) ->
    if#(X1,active(X2),X3) -> if#(X1,X2,X3)
    if#(active(X1),X2,X3) -> if#(X1,X2,X3) ->
    if#(active(X1),X2,X3) -> if#(X1,X2,X3)
    if#(active(X1),X2,X3) -> if#(X1,X2,X3) ->
    if#(X1,X2,mark(X3)) -> if#(X1,X2,X3)
    if#(active(X1),X2,X3) -> if#(X1,X2,X3) ->
    if#(X1,mark(X2),X3) -> if#(X1,X2,X3)
    if#(active(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#(X1,X2,active(X3)) -> if#(X1,X2,X3)
    if#(X1,mark(X2),X3) -> if#(X1,X2,X3) ->
    if#(X1,active(X2),X3) -> if#(X1,X2,X3)
    if#(X1,mark(X2),X3) -> if#(X1,X2,X3) ->
    if#(active(X1),X2,X3) -> if#(X1,X2,X3)
    if#(X1,mark(X2),X3) -> if#(X1,X2,X3) ->
    if#(X1,X2,mark(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)
    if#(X1,active(X2),X3) -> if#(X1,X2,X3) ->
    if#(X1,X2,active(X3)) -> if#(X1,X2,X3)
    if#(X1,active(X2),X3) -> if#(X1,X2,X3) ->
    if#(X1,active(X2),X3) -> if#(X1,X2,X3)
    if#(X1,active(X2),X3) -> if#(X1,X2,X3) ->
    if#(active(X1),X2,X3) -> if#(X1,X2,X3)
    if#(X1,active(X2),X3) -> if#(X1,X2,X3) ->
    if#(X1,X2,mark(X3)) -> if#(X1,X2,X3)
    if#(X1,active(X2),X3) -> if#(X1,X2,X3) ->
    if#(X1,mark(X2),X3) -> if#(X1,X2,X3)
    if#(X1,active(X2),X3) -> if#(X1,X2,X3) ->
    if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
    if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) ->
    if#(X1,X2,active(X3)) -> if#(X1,X2,X3)
    if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) ->
    if#(X1,active(X2),X3) -> if#(X1,X2,X3)
    if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) ->
    if#(active(X1),X2,X3) -> if#(X1,X2,X3)
    if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) ->
    if#(X1,X2,mark(X3)) -> if#(X1,X2,X3)
    if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) ->
    if#(X1,mark(X2),X3) -> if#(X1,X2,X3)
    if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) ->
    if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
    if#(X1,X2,active(X3)) -> if#(X1,X2,X3) ->
    if#(X1,X2,active(X3)) -> if#(X1,X2,X3)
    if#(X1,X2,active(X3)) -> if#(X1,X2,X3) ->
    if#(X1,active(X2),X3) -> if#(X1,X2,X3)
    if#(X1,X2,active(X3)) -> if#(X1,X2,X3) ->
    if#(active(X1),X2,X3) -> if#(X1,X2,X3)
    if#(X1,X2,active(X3)) -> if#(X1,X2,X3) ->
    if#(X1,X2,mark(X3)) -> if#(X1,X2,X3)
    if#(X1,X2,active(X3)) -> if#(X1,X2,X3) ->
    if#(X1,mark(X2),X3) -> if#(X1,X2,X3)
    if#(X1,X2,active(X3)) -> if#(X1,X2,X3) ->
    if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
    zero#(mark(X)) -> zero#(X) -> zero#(active(X)) -> zero#(X)
    zero#(mark(X)) -> zero#(X) -> zero#(mark(X)) -> zero#(X)
    zero#(active(X)) -> zero#(X) -> zero#(active(X)) -> zero#(X)
    zero#(active(X)) -> zero#(X) -> zero#(mark(X)) -> zero#(X)
    s#(mark(X)) -> s#(X) -> s#(active(X)) -> s#(X)
    s#(mark(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
    s#(active(X)) -> s#(X) -> s#(active(X)) -> s#(X)
    s#(active(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
    prod#(mark(X1),X2) -> prod#(X1,X2) ->
    prod#(X1,active(X2)) -> prod#(X1,X2)
    prod#(mark(X1),X2) -> prod#(X1,X2) ->
    prod#(active(X1),X2) -> prod#(X1,X2)
    prod#(mark(X1),X2) -> prod#(X1,X2) ->
    prod#(X1,mark(X2)) -> prod#(X1,X2)
    prod#(mark(X1),X2) -> prod#(X1,X2) ->
    prod#(mark(X1),X2) -> prod#(X1,X2)
    prod#(active(X1),X2) -> prod#(X1,X2) ->
    prod#(X1,active(X2)) -> prod#(X1,X2)
    prod#(active(X1),X2) -> prod#(X1,X2) ->
    prod#(active(X1),X2) -> prod#(X1,X2)
    prod#(active(X1),X2) -> prod#(X1,X2) ->
    prod#(X1,mark(X2)) -> prod#(X1,X2)
    prod#(active(X1),X2) -> prod#(X1,X2) ->
    prod#(mark(X1),X2) -> prod#(X1,X2)
    prod#(X1,mark(X2)) -> prod#(X1,X2) ->
    prod#(X1,active(X2)) -> prod#(X1,X2)
    prod#(X1,mark(X2)) -> prod#(X1,X2) ->
    prod#(active(X1),X2) -> prod#(X1,X2)
    prod#(X1,mark(X2)) -> prod#(X1,X2) ->
    prod#(X1,mark(X2)) -> prod#(X1,X2)
    prod#(X1,mark(X2)) -> prod#(X1,X2) ->
    prod#(mark(X1),X2) -> prod#(X1,X2)
    prod#(X1,active(X2)) -> prod#(X1,X2) ->
    prod#(X1,active(X2)) -> prod#(X1,X2)
    prod#(X1,active(X2)) -> prod#(X1,X2) ->
    prod#(active(X1),X2) -> prod#(X1,X2)
    prod#(X1,active(X2)) -> prod#(X1,X2) ->
    prod#(X1,mark(X2)) -> prod#(X1,X2)
    prod#(X1,active(X2)) -> prod#(X1,X2) ->
    prod#(mark(X1),X2) -> prod#(X1,X2)
    fact#(mark(X)) -> fact#(X) -> fact#(active(X)) -> fact#(X)
    fact#(mark(X)) -> fact#(X) -> fact#(mark(X)) -> fact#(X)
    fact#(active(X)) -> fact#(X) -> fact#(active(X)) -> fact#(X)
    fact#(active(X)) -> fact#(X) -> fact#(mark(X)) -> fact#(X)
    p#(mark(X)) -> p#(X) -> p#(active(X)) -> p#(X)
    p#(mark(X)) -> p#(X) -> p#(mark(X)) -> p#(X)
    p#(active(X)) -> p#(X) -> p#(active(X)) -> p#(X)
    p#(active(X)) -> p#(X) -> p#(mark(X)) -> p#(X)
    active#(add(s(X),Y)) -> add#(X,Y) ->
    add#(X1,active(X2)) -> add#(X1,X2)
    active#(add(s(X),Y)) -> add#(X,Y) ->
    add#(active(X1),X2) -> add#(X1,X2)
    active#(add(s(X),Y)) -> add#(X,Y) ->
    add#(X1,mark(X2)) -> add#(X1,X2)
    active#(add(s(X),Y)) -> add#(X,Y) ->
    add#(mark(X1),X2) -> add#(X1,X2)
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(false()) -> active#(false())
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(true()) -> active#(true())
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(add(X1,X2)) -> add#(mark(X1),mark(X2))
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(add(X1,X2)) -> mark#(X1)
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(add(X1,X2)) -> mark#(X2)
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(p(X)) -> active#(p(mark(X)))
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(p(X)) -> p#(mark(X))
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(p(X)) -> mark#(X)
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(prod(X1,X2)) -> prod#(mark(X1),mark(X2))
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(prod(X1,X2)) -> mark#(X1)
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(prod(X1,X2)) -> mark#(X2)
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(0()) -> active#(0())
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(s(X)) -> s#(mark(X))
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(s(X)) -> mark#(X)
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(zero(X)) -> active#(zero(mark(X)))
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(zero(X)) -> zero#(mark(X))
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(zero(X)) -> mark#(X)
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(if(X1,X2,X3)) -> mark#(X1)
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(fact(X)) -> active#(fact(mark(X)))
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(fact(X)) -> fact#(mark(X))
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(fact(X)) -> mark#(X)
    active#(add(s(X),Y)) -> s#(add(X,Y)) ->
    s#(active(X)) -> s#(X)
    active#(add(s(X),Y)) -> s#(add(X,Y)) -> s#(mark(X)) -> s#(X)
    active#(add(0(),X)) -> mark#(X) ->
    mark#(false()) -> active#(false())
    active#(add(0(),X)) -> mark#(X) ->
    mark#(true()) -> active#(true())
    active#(add(0(),X)) -> mark#(X) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
    active#(add(0(),X)) -> mark#(X) ->
    mark#(add(X1,X2)) -> add#(mark(X1),mark(X2))
    active#(add(0(),X)) -> mark#(X) ->
    mark#(add(X1,X2)) -> mark#(X1)
    active#(add(0(),X)) -> mark#(X) ->
    mark#(add(X1,X2)) -> mark#(X2)
    active#(add(0(),X)) -> mark#(X) ->
    mark#(p(X)) -> active#(p(mark(X)))
    active#(add(0(),X)) -> mark#(X) -> mark#(p(X)) -> p#(mark(X))
    active#(add(0(),X)) -> mark#(X) -> mark#(p(X)) -> mark#(X)
    active#(add(0(),X)) -> mark#(X) ->
    mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
    active#(add(0(),X)) -> mark#(X) ->
    mark#(prod(X1,X2)) -> prod#(mark(X1),mark(X2))
    active#(add(0(),X)) -> mark#(X) ->
    mark#(prod(X1,X2)) -> mark#(X1)
    active#(add(0(),X)) -> mark#(X) ->
    mark#(prod(X1,X2)) -> mark#(X2)
    active#(add(0(),X)) -> mark#(X) -> mark#(0()) -> active#(0())
    active#(add(0(),X)) -> mark#(X) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(add(0(),X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X))
    active#(add(0(),X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    active#(add(0(),X)) -> mark#(X) ->
    mark#(zero(X)) -> active#(zero(mark(X)))
    active#(add(0(),X)) -> mark#(X) ->
    mark#(zero(X)) -> zero#(mark(X))
    active#(add(0(),X)) -> mark#(X) -> mark#(zero(X)) -> mark#(X)
    active#(add(0(),X)) -> mark#(X) ->
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    active#(add(0(),X)) -> mark#(X) ->
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
    active#(add(0(),X)) -> mark#(X) ->
    mark#(if(X1,X2,X3)) -> mark#(X1)
    active#(add(0(),X)) -> mark#(X) ->
    mark#(fact(X)) -> active#(fact(mark(X)))
    active#(add(0(),X)) -> mark#(X) ->
    mark#(fact(X)) -> fact#(mark(X))
    active#(add(0(),X)) -> mark#(X) ->
    mark#(fact(X)) -> mark#(X)
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(false()) -> active#(false())
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(true()) -> active#(true())
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(add(X1,X2)) -> add#(mark(X1),mark(X2))
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(add(X1,X2)) -> mark#(X1)
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(add(X1,X2)) -> mark#(X2)
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(p(X)) -> active#(p(mark(X)))
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(p(X)) -> p#(mark(X))
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(p(X)) -> mark#(X)
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(prod(X1,X2)) -> prod#(mark(X1),mark(X2))
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(prod(X1,X2)) -> mark#(X1)
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(prod(X1,X2)) -> mark#(X2)
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(0()) -> active#(0())
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(s(X)) -> s#(mark(X))
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(s(X)) -> mark#(X)
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(zero(X)) -> active#(zero(mark(X)))
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(zero(X)) -> zero#(mark(X))
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(zero(X)) -> mark#(X)
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(if(X1,X2,X3)) -> mark#(X1)
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(fact(X)) -> active#(fact(mark(X)))
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(fact(X)) -> fact#(mark(X))
    active#(if(false(),X,Y)) -> mark#(Y) ->
    mark#(fact(X)) -> mark#(X)
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(false()) -> active#(false())
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(true()) -> active#(true())
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(add(X1,X2)) -> add#(mark(X1),mark(X2))
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(add(X1,X2)) -> mark#(X1)
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(add(X1,X2)) -> mark#(X2)
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(p(X)) -> active#(p(mark(X)))
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(p(X)) -> p#(mark(X))
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(p(X)) -> mark#(X)
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(prod(X1,X2)) -> prod#(mark(X1),mark(X2))
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(prod(X1,X2)) -> mark#(X1)
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(prod(X1,X2)) -> mark#(X2)
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(0()) -> active#(0())
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(s(X)) -> s#(mark(X))
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(s(X)) -> mark#(X)
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(zero(X)) -> active#(zero(mark(X)))
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(zero(X)) -> zero#(mark(X))
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(zero(X)) -> mark#(X)
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(if(X1,X2,X3)) -> mark#(X1)
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(fact(X)) -> active#(fact(mark(X)))
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(fact(X)) -> fact#(mark(X))
    active#(if(true(),X,Y)) -> mark#(X) ->
    mark#(fact(X)) -> mark#(X)
    active#(prod(s(X),Y)) -> add#(Y,prod(X,Y)) ->
    add#(X1,active(X2)) -> add#(X1,X2)
    active#(prod(s(X),Y)) -> add#(Y,prod(X,Y)) ->
    add#(active(X1),X2) -> add#(X1,X2)
    active#(prod(s(X),Y)) -> add#(Y,prod(X,Y)) ->
    add#(X1,mark(X2)) -> add#(X1,X2)
    active#(prod(s(X),Y)) -> add#(Y,prod(X,Y)) ->
    add#(mark(X1),X2) -> add#(X1,X2)
    active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
    mark#(false()) -> active#(false())
    active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
    mark#(true()) -> active#(true())
    active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
    active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
    mark#(add(X1,X2)) -> add#(mark(X1),mark(X2))
    active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
    mark#(add(X1,X2)) -> mark#(X1)
    active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
    mark#(add(X1,X2)) -> mark#(X2)
    active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
    mark#(p(X)) -> active#(p(mark(X)))
    active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
    mark#(p(X)) -> p#(mark(X))
    active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
    mark#(p(X)) -> mark#(X)
    active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
    mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
    active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
    mark#(prod(X1,X2)) -> prod#(mark(X1),mark(X2))
    active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
    mark#(prod(X1,X2)) -> mark#(X1)
    active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
    mark#(prod(X1,X2)) -> mark#(X2)
    active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
    mark#(0()) -> active#(0())
    active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
    mark#(s(X)) -> s#(mark(X))
    active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
    mark#(s(X)) -> mark#(X)
    active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
    mark#(zero(X)) -> active#(zero(mark(X)))
    active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
    mark#(zero(X)) -> zero#(mark(X))
    active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
    mark#(zero(X)) -> mark#(X)
    active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
    active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
    mark#(if(X1,X2,X3)) -> mark#(X1)
    active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
    mark#(fact(X)) -> active#(fact(mark(X)))
    active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
    mark#(fact(X)) -> fact#(mark(X))
    active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
    mark#(fact(X)) -> mark#(X)
    active#(prod(s(X),Y)) -> prod#(X,Y) ->
    prod#(X1,active(X2)) -> prod#(X1,X2)
    active#(prod(s(X),Y)) -> prod#(X,Y) ->
    prod#(active(X1),X2) -> prod#(X1,X2)
    active#(prod(s(X),Y)) -> prod#(X,Y) ->
    prod#(X1,mark(X2)) -> prod#(X1,X2)
    active#(prod(s(X),Y)) -> prod#(X,Y) ->
    prod#(mark(X1),X2) -> prod#(X1,X2)
    active#(prod(0(),X)) -> mark#(0()) ->
    mark#(false()) -> active#(false())
    active#(prod(0(),X)) -> mark#(0()) ->
    mark#(true()) -> active#(true())
    active#(prod(0(),X)) -> mark#(0()) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
    active#(prod(0(),X)) -> mark#(0()) ->
    mark#(add(X1,X2)) -> add#(mark(X1),mark(X2))
    active#(prod(0(),X)) -> mark#(0()) ->
    mark#(add(X1,X2)) -> mark#(X1)
    active#(prod(0(),X)) -> mark#(0()) ->
    mark#(add(X1,X2)) -> mark#(X2)
    active#(prod(0(),X)) -> mark#(0()) ->
    mark#(p(X)) -> active#(p(mark(X)))
    active#(prod(0(),X)) -> mark#(0()) ->
    mark#(p(X)) -> p#(mark(X))
    active#(prod(0(),X)) -> mark#(0()) -> mark#(p(X)) -> mark#(X)
    active#(prod(0(),X)) -> mark#(0()) ->
    mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
    active#(prod(0(),X)) -> mark#(0()) ->
    mark#(prod(X1,X2)) -> prod#(mark(X1),mark(X2))
    active#(prod(0(),X)) -> mark#(0()) ->
    mark#(prod(X1,X2)) -> mark#(X1)
    active#(prod(0(),X)) -> mark#(0()) ->
    mark#(prod(X1,X2)) -> mark#(X2)
    active#(prod(0(),X)) -> mark#(0()) ->
    mark#(0()) -> active#(0())
    active#(prod(0(),X)) -> mark#(0()) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(prod(0(),X)) -> mark#(0()) ->
    mark#(s(X)) -> s#(mark(X))
    active#(prod(0(),X)) -> mark#(0()) -> mark#(s(X)) -> mark#(X)
    active#(prod(0(),X)) -> mark#(0()) ->
    mark#(zero(X)) -> active#(zero(mark(X)))
    active#(prod(0(),X)) -> mark#(0()) ->
    mark#(zero(X)) -> zero#(mark(X))
    active#(prod(0(),X)) -> mark#(0()) ->
    mark#(zero(X)) -> mark#(X)
    active#(prod(0(),X)) -> mark#(0()) ->
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    active#(prod(0(),X)) -> mark#(0()) ->
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
    active#(prod(0(),X)) -> mark#(0()) ->
    mark#(if(X1,X2,X3)) -> mark#(X1)
    active#(prod(0(),X)) -> mark#(0()) ->
    mark#(fact(X)) -> active#(fact(mark(X)))
    active#(prod(0(),X)) -> mark#(0()) ->
    mark#(fact(X)) -> fact#(mark(X))
    active#(prod(0(),X)) -> mark#(0()) -> mark#(fact(X)) -> mark#(X)
    active#(p(s(X))) -> mark#(X) -> mark#(false()) -> active#(false())
    active#(p(s(X))) -> mark#(X) -> mark#(true()) -> active#(true())
    active#(p(s(X))) -> mark#(X) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
    active#(p(s(X))) -> mark#(X) ->
    mark#(add(X1,X2)) -> add#(mark(X1),mark(X2))
    active#(p(s(X))) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1)
    active#(p(s(X))) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2)
    active#(p(s(X))) -> mark#(X) -> mark#(p(X)) -> active#(p(mark(X)))
    active#(p(s(X))) -> mark#(X) -> mark#(p(X)) -> p#(mark(X))
    active#(p(s(X))) -> mark#(X) -> mark#(p(X)) -> mark#(X)
    active#(p(s(X))) -> mark#(X) ->
    mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
    active#(p(s(X))) -> mark#(X) ->
    mark#(prod(X1,X2)) -> prod#(mark(X1),mark(X2))
    active#(p(s(X))) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X1)
    active#(p(s(X))) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X2)
    active#(p(s(X))) -> mark#(X) -> mark#(0()) -> active#(0())
    active#(p(s(X))) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
    active#(p(s(X))) -> mark#(X) -> mark#(s(X)) -> s#(mark(X))
    active#(p(s(X))) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    active#(p(s(X))) -> mark#(X) ->
    mark#(zero(X)) -> active#(zero(mark(X)))
    active#(p(s(X))) -> mark#(X) -> mark#(zero(X)) -> zero#(mark(X))
    active#(p(s(X))) -> mark#(X) -> mark#(zero(X)) -> mark#(X)
    active#(p(s(X))) -> mark#(X) ->
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    active#(p(s(X))) -> mark#(X) ->
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
    active#(p(s(X))) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1)
    active#(p(s(X))) -> mark#(X) ->
    mark#(fact(X)) -> active#(fact(mark(X)))
    active#(p(s(X))) -> mark#(X) -> mark#(fact(X)) -> fact#(mark(X))
    active#(p(s(X))) -> mark#(X) -> mark#(fact(X)) -> mark#(X)
    active#(zero(s(X))) -> mark#(false()) ->
    mark#(false()) -> active#(false())
    active#(zero(s(X))) -> mark#(false()) ->
    mark#(true()) -> active#(true())
    active#(zero(s(X))) -> mark#(false()) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
    active#(zero(s(X))) -> mark#(false()) ->
    mark#(add(X1,X2)) -> add#(mark(X1),mark(X2))
    active#(zero(s(X))) -> mark#(false()) ->
    mark#(add(X1,X2)) -> mark#(X1)
    active#(zero(s(X))) -> mark#(false()) ->
    mark#(add(X1,X2)) -> mark#(X2)
    active#(zero(s(X))) -> mark#(false()) ->
    mark#(p(X)) -> active#(p(mark(X)))
    active#(zero(s(X))) -> mark#(false()) ->
    mark#(p(X)) -> p#(mark(X))
    active#(zero(s(X))) -> mark#(false()) ->
    mark#(p(X)) -> mark#(X)
    active#(zero(s(X))) -> mark#(false()) ->
    mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
    active#(zero(s(X))) -> mark#(false()) ->
    mark#(prod(X1,X2)) -> prod#(mark(X1),mark(X2))
    active#(zero(s(X))) -> mark#(false()) ->
    mark#(prod(X1,X2)) -> mark#(X1)
    active#(zero(s(X))) -> mark#(false()) ->
    mark#(prod(X1,X2)) -> mark#(X2)
    active#(zero(s(X))) -> mark#(false()) ->
    mark#(0()) -> active#(0())
    active#(zero(s(X))) -> mark#(false()) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(zero(s(X))) -> mark#(false()) ->
    mark#(s(X)) -> s#(mark(X))
    active#(zero(s(X))) -> mark#(false()) ->
    mark#(s(X)) -> mark#(X)
    active#(zero(s(X))) -> mark#(false()) ->
    mark#(zero(X)) -> active#(zero(mark(X)))
    active#(zero(s(X))) -> mark#(false()) ->
    mark#(zero(X)) -> zero#(mark(X))
    active#(zero(s(X))) -> mark#(false()) ->
    mark#(zero(X)) -> mark#(X)
    active#(zero(s(X))) -> mark#(false()) ->
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    active#(zero(s(X))) -> mark#(false()) ->
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
    active#(zero(s(X))) -> mark#(false()) ->
    mark#(if(X1,X2,X3)) -> mark#(X1)
    active#(zero(s(X))) -> mark#(false()) ->
    mark#(fact(X)) -> active#(fact(mark(X)))
    active#(zero(s(X))) -> mark#(false()) ->
    mark#(fact(X)) -> fact#(mark(X))
    active#(zero(s(X))) -> mark#(false()) ->
    mark#(fact(X)) -> mark#(X)
    active#(zero(0())) -> mark#(true()) ->
    mark#(false()) -> active#(false())
    active#(zero(0())) -> mark#(true()) ->
    mark#(true()) -> active#(true())
    active#(zero(0())) -> mark#(true()) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
    active#(zero(0())) -> mark#(true()) ->
    mark#(add(X1,X2)) -> add#(mark(X1),mark(X2))
    active#(zero(0())) -> mark#(true()) ->
    mark#(add(X1,X2)) -> mark#(X1)
    active#(zero(0())) -> mark#(true()) ->
    mark#(add(X1,X2)) -> mark#(X2)
    active#(zero(0())) -> mark#(true()) ->
    mark#(p(X)) -> active#(p(mark(X)))
    active#(zero(0())) -> mark#(true()) ->
    mark#(p(X)) -> p#(mark(X))
    active#(zero(0())) -> mark#(true()) ->
    mark#(p(X)) -> mark#(X)
    active#(zero(0())) -> mark#(true()) ->
    mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
    active#(zero(0())) -> mark#(true()) ->
    mark#(prod(X1,X2)) -> prod#(mark(X1),mark(X2))
    active#(zero(0())) -> mark#(true()) ->
    mark#(prod(X1,X2)) -> mark#(X1)
    active#(zero(0())) -> mark#(true()) ->
    mark#(prod(X1,X2)) -> mark#(X2)
    active#(zero(0())) -> mark#(true()) ->
    mark#(0()) -> active#(0())
    active#(zero(0())) -> mark#(true()) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(zero(0())) -> mark#(true()) ->
    mark#(s(X)) -> s#(mark(X))
    active#(zero(0())) -> mark#(true()) ->
    mark#(s(X)) -> mark#(X)
    active#(zero(0())) -> mark#(true()) ->
    mark#(zero(X)) -> active#(zero(mark(X)))
    active#(zero(0())) -> mark#(true()) ->
    mark#(zero(X)) -> zero#(mark(X))
    active#(zero(0())) -> mark#(true()) ->
    mark#(zero(X)) -> mark#(X)
    active#(zero(0())) -> mark#(true()) ->
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    active#(zero(0())) -> mark#(true()) ->
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
    active#(zero(0())) -> mark#(true()) ->
    mark#(if(X1,X2,X3)) -> mark#(X1)
    active#(zero(0())) -> mark#(true()) ->
    mark#(fact(X)) -> active#(fact(mark(X)))
    active#(zero(0())) -> mark#(true()) ->
    mark#(fact(X)) -> fact#(mark(X))
    active#(zero(0())) -> mark#(true()) ->
    mark#(fact(X)) -> mark#(X)
    active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
    mark#(false()) -> active#(false())
    active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
    mark#(true()) -> active#(true())
    active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
    active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
    mark#(add(X1,X2)) -> add#(mark(X1),mark(X2))
    active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
    mark#(add(X1,X2)) -> mark#(X1)
    active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
    mark#(add(X1,X2)) -> mark#(X2)
    active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
    mark#(p(X)) -> active#(p(mark(X)))
    active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
    mark#(p(X)) -> p#(mark(X))
    active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
    mark#(p(X)) -> mark#(X)
    active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
    mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
    active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
    mark#(prod(X1,X2)) -> prod#(mark(X1),mark(X2))
    active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
    mark#(prod(X1,X2)) -> mark#(X1)
    active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
    mark#(prod(X1,X2)) -> mark#(X2)
    active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
    mark#(0()) -> active#(0())
    active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
    mark#(s(X)) -> s#(mark(X))
    active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
    mark#(s(X)) -> mark#(X)
    active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
    mark#(zero(X)) -> active#(zero(mark(X)))
    active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
    mark#(zero(X)) -> zero#(mark(X))
    active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
    mark#(zero(X)) -> mark#(X)
    active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
    active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
    mark#(if(X1,X2,X3)) -> mark#(X1)
    active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
    mark#(fact(X)) -> active#(fact(mark(X)))
    active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
    mark#(fact(X)) -> fact#(mark(X))
    active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
    mark#(fact(X)) -> mark#(X)
    active#(fact(X)) -> if#(zero(X),s(0()),prod(X,fact(p(X)))) ->
    if#(X1,X2,active(X3)) -> if#(X1,X2,X3)
    active#(fact(X)) -> if#(zero(X),s(0()),prod(X,fact(p(X)))) ->
    if#(X1,active(X2),X3) -> if#(X1,X2,X3)
    active#(fact(X)) -> if#(zero(X),s(0()),prod(X,fact(p(X)))) ->
    if#(active(X1),X2,X3) -> if#(X1,X2,X3)
    active#(fact(X)) -> if#(zero(X),s(0()),prod(X,fact(p(X)))) ->
    if#(X1,X2,mark(X3)) -> if#(X1,X2,X3)
    active#(fact(X)) -> if#(zero(X),s(0()),prod(X,fact(p(X)))) ->
    if#(X1,mark(X2),X3) -> if#(X1,X2,X3)
    active#(fact(X)) -> if#(zero(X),s(0()),prod(X,fact(p(X)))) ->
    if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
    active#(fact(X)) -> zero#(X) -> zero#(active(X)) -> zero#(X)
    active#(fact(X)) -> zero#(X) -> zero#(mark(X)) -> zero#(X)
    active#(fact(X)) -> s#(0()) -> s#(active(X)) -> s#(X)
    active#(fact(X)) -> s#(0()) -> s#(mark(X)) -> s#(X)
    active#(fact(X)) -> prod#(X,fact(p(X))) ->
    prod#(X1,active(X2)) -> prod#(X1,X2)
    active#(fact(X)) -> prod#(X,fact(p(X))) ->
    prod#(active(X1),X2) -> prod#(X1,X2)
    active#(fact(X)) -> prod#(X,fact(p(X))) ->
    prod#(X1,mark(X2)) -> prod#(X1,X2)
    active#(fact(X)) -> prod#(X,fact(p(X))) ->
    prod#(mark(X1),X2) -> prod#(X1,X2)
    active#(fact(X)) -> fact#(p(X)) -> fact#(active(X)) -> fact#(X)
    active#(fact(X)) -> fact#(p(X)) -> fact#(mark(X)) -> fact#(X)
    active#(fact(X)) -> p#(X) -> p#(active(X)) -> p#(X)
    active#(fact(X)) -> p#(X) -> p#(mark(X)) -> p#(X)
   SCC Processor:
    #sccs: 8
    #rules: 51
    #arcs: 832/4624
    DPs:
     mark#(false()) -> active#(false())
     active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X)))))
     mark#(fact(X)) -> mark#(X)
     mark#(fact(X)) -> active#(fact(mark(X)))
     active#(add(0(),X)) -> mark#(X)
     mark#(if(X1,X2,X3)) -> mark#(X1)
     mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
     active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
     mark#(zero(X)) -> mark#(X)
     mark#(zero(X)) -> active#(zero(mark(X)))
     active#(prod(0(),X)) -> mark#(0())
     mark#(s(X)) -> mark#(X)
     mark#(s(X)) -> active#(s(mark(X)))
     active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y)))
     mark#(0()) -> active#(0())
     active#(if(true(),X,Y)) -> mark#(X)
     mark#(prod(X1,X2)) -> mark#(X2)
     mark#(prod(X1,X2)) -> mark#(X1)
     mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
     active#(if(false(),X,Y)) -> mark#(Y)
     mark#(p(X)) -> mark#(X)
     mark#(p(X)) -> active#(p(mark(X)))
     active#(zero(0())) -> mark#(true())
     mark#(add(X1,X2)) -> mark#(X2)
     mark#(add(X1,X2)) -> mark#(X1)
     mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
     active#(zero(s(X))) -> mark#(false())
     mark#(true()) -> active#(true())
     active#(p(s(X))) -> mark#(X)
    TRS:
     active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X)))))
     active(add(0(),X)) -> mark(X)
     active(add(s(X),Y)) -> mark(s(add(X,Y)))
     active(prod(0(),X)) -> mark(0())
     active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y)))
     active(if(true(),X,Y)) -> mark(X)
     active(if(false(),X,Y)) -> mark(Y)
     active(zero(0())) -> mark(true())
     active(zero(s(X))) -> mark(false())
     active(p(s(X))) -> mark(X)
     mark(fact(X)) -> active(fact(mark(X)))
     mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
     mark(zero(X)) -> active(zero(mark(X)))
     mark(s(X)) -> active(s(mark(X)))
     mark(0()) -> active(0())
     mark(prod(X1,X2)) -> active(prod(mark(X1),mark(X2)))
     mark(p(X)) -> active(p(mark(X)))
     mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
     mark(true()) -> active(true())
     mark(false()) -> active(false())
     fact(mark(X)) -> fact(X)
     fact(active(X)) -> fact(X)
     if(mark(X1),X2,X3) -> if(X1,X2,X3)
     if(X1,mark(X2),X3) -> if(X1,X2,X3)
     if(X1,X2,mark(X3)) -> if(X1,X2,X3)
     if(active(X1),X2,X3) -> if(X1,X2,X3)
     if(X1,active(X2),X3) -> if(X1,X2,X3)
     if(X1,X2,active(X3)) -> if(X1,X2,X3)
     zero(mark(X)) -> zero(X)
     zero(active(X)) -> zero(X)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     prod(mark(X1),X2) -> prod(X1,X2)
     prod(X1,mark(X2)) -> prod(X1,X2)
     prod(active(X1),X2) -> prod(X1,X2)
     prod(X1,active(X2)) -> prod(X1,X2)
     p(mark(X)) -> p(X)
     p(active(X)) -> p(X)
     add(mark(X1),X2) -> add(X1,X2)
     add(X1,mark(X2)) -> add(X1,X2)
     add(active(X1),X2) -> add(X1,X2)
     add(X1,active(X2)) -> add(X1,X2)
    EDG Processor:
     DPs:
      mark#(false()) -> active#(false())
      active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X)))))
      mark#(fact(X)) -> mark#(X)
      mark#(fact(X)) -> active#(fact(mark(X)))
      active#(add(0(),X)) -> mark#(X)
      mark#(if(X1,X2,X3)) -> mark#(X1)
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
      active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
      mark#(zero(X)) -> mark#(X)
      mark#(zero(X)) -> active#(zero(mark(X)))
      active#(prod(0(),X)) -> mark#(0())
      mark#(s(X)) -> mark#(X)
      mark#(s(X)) -> active#(s(mark(X)))
      active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y)))
      mark#(0()) -> active#(0())
      active#(if(true(),X,Y)) -> mark#(X)
      mark#(prod(X1,X2)) -> mark#(X2)
      mark#(prod(X1,X2)) -> mark#(X1)
      mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
      active#(if(false(),X,Y)) -> mark#(Y)
      mark#(p(X)) -> mark#(X)
      mark#(p(X)) -> active#(p(mark(X)))
      active#(zero(0())) -> mark#(true())
      mark#(add(X1,X2)) -> mark#(X2)
      mark#(add(X1,X2)) -> mark#(X1)
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
      active#(zero(s(X))) -> mark#(false())
      mark#(true()) -> active#(true())
      active#(p(s(X))) -> mark#(X)
     TRS:
      active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X)))))
      active(add(0(),X)) -> mark(X)
      active(add(s(X),Y)) -> mark(s(add(X,Y)))
      active(prod(0(),X)) -> mark(0())
      active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y)))
      active(if(true(),X,Y)) -> mark(X)
      active(if(false(),X,Y)) -> mark(Y)
      active(zero(0())) -> mark(true())
      active(zero(s(X))) -> mark(false())
      active(p(s(X))) -> mark(X)
      mark(fact(X)) -> active(fact(mark(X)))
      mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
      mark(zero(X)) -> active(zero(mark(X)))
      mark(s(X)) -> active(s(mark(X)))
      mark(0()) -> active(0())
      mark(prod(X1,X2)) -> active(prod(mark(X1),mark(X2)))
      mark(p(X)) -> active(p(mark(X)))
      mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
      mark(true()) -> active(true())
      mark(false()) -> active(false())
      fact(mark(X)) -> fact(X)
      fact(active(X)) -> fact(X)
      if(mark(X1),X2,X3) -> if(X1,X2,X3)
      if(X1,mark(X2),X3) -> if(X1,X2,X3)
      if(X1,X2,mark(X3)) -> if(X1,X2,X3)
      if(active(X1),X2,X3) -> if(X1,X2,X3)
      if(X1,active(X2),X3) -> if(X1,X2,X3)
      if(X1,X2,active(X3)) -> if(X1,X2,X3)
      zero(mark(X)) -> zero(X)
      zero(active(X)) -> zero(X)
      s(mark(X)) -> s(X)
      s(active(X)) -> s(X)
      prod(mark(X1),X2) -> prod(X1,X2)
      prod(X1,mark(X2)) -> prod(X1,X2)
      prod(active(X1),X2) -> prod(X1,X2)
      prod(X1,active(X2)) -> prod(X1,X2)
      p(mark(X)) -> p(X)
      p(active(X)) -> p(X)
      add(mark(X1),X2) -> add(X1,X2)
      add(X1,mark(X2)) -> add(X1,X2)
      add(active(X1),X2) -> add(X1,X2)
      add(X1,active(X2)) -> add(X1,X2)
     graph:
      mark#(add(X1,X2)) -> mark#(X2) -> mark#(fact(X)) -> mark#(X)
      mark#(add(X1,X2)) -> mark#(X2) ->
      mark#(fact(X)) -> active#(fact(mark(X)))
      mark#(add(X1,X2)) -> mark#(X2) ->
      mark#(if(X1,X2,X3)) -> mark#(X1)
      mark#(add(X1,X2)) -> mark#(X2) ->
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
      mark#(add(X1,X2)) -> mark#(X2) -> mark#(zero(X)) -> mark#(X)
      mark#(add(X1,X2)) -> mark#(X2) ->
      mark#(zero(X)) -> active#(zero(mark(X)))
      mark#(add(X1,X2)) -> mark#(X2) -> mark#(s(X)) -> mark#(X)
      mark#(add(X1,X2)) -> mark#(X2) ->
      mark#(s(X)) -> active#(s(mark(X)))
      mark#(add(X1,X2)) -> mark#(X2) -> mark#(0()) -> active#(0())
      mark#(add(X1,X2)) -> mark#(X2) ->
      mark#(prod(X1,X2)) -> mark#(X2)
      mark#(add(X1,X2)) -> mark#(X2) ->
      mark#(prod(X1,X2)) -> mark#(X1)
      mark#(add(X1,X2)) -> mark#(X2) ->
      mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
      mark#(add(X1,X2)) -> mark#(X2) -> mark#(p(X)) -> mark#(X)
      mark#(add(X1,X2)) -> mark#(X2) ->
      mark#(p(X)) -> active#(p(mark(X)))
      mark#(add(X1,X2)) -> mark#(X2) ->
      mark#(add(X1,X2)) -> mark#(X2)
      mark#(add(X1,X2)) -> mark#(X2) ->
      mark#(add(X1,X2)) -> mark#(X1)
      mark#(add(X1,X2)) -> mark#(X2) ->
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
      mark#(add(X1,X2)) -> mark#(X2) ->
      mark#(true()) -> active#(true())
      mark#(add(X1,X2)) -> mark#(X2) ->
      mark#(false()) -> active#(false())
      mark#(add(X1,X2)) -> mark#(X1) -> mark#(fact(X)) -> mark#(X)
      mark#(add(X1,X2)) -> mark#(X1) ->
      mark#(fact(X)) -> active#(fact(mark(X)))
      mark#(add(X1,X2)) -> mark#(X1) ->
      mark#(if(X1,X2,X3)) -> mark#(X1)
      mark#(add(X1,X2)) -> mark#(X1) ->
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
      mark#(add(X1,X2)) -> mark#(X1) -> mark#(zero(X)) -> mark#(X)
      mark#(add(X1,X2)) -> mark#(X1) ->
      mark#(zero(X)) -> active#(zero(mark(X)))
      mark#(add(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
      mark#(add(X1,X2)) -> mark#(X1) ->
      mark#(s(X)) -> active#(s(mark(X)))
      mark#(add(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
      mark#(add(X1,X2)) -> mark#(X1) ->
      mark#(prod(X1,X2)) -> mark#(X2)
      mark#(add(X1,X2)) -> mark#(X1) ->
      mark#(prod(X1,X2)) -> mark#(X1)
      mark#(add(X1,X2)) -> mark#(X1) ->
      mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
      mark#(add(X1,X2)) -> mark#(X1) -> mark#(p(X)) -> mark#(X)
      mark#(add(X1,X2)) -> mark#(X1) ->
      mark#(p(X)) -> active#(p(mark(X)))
      mark#(add(X1,X2)) -> mark#(X1) ->
      mark#(add(X1,X2)) -> mark#(X2)
      mark#(add(X1,X2)) -> mark#(X1) ->
      mark#(add(X1,X2)) -> mark#(X1)
      mark#(add(X1,X2)) -> mark#(X1) ->
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
      mark#(add(X1,X2)) -> mark#(X1) ->
      mark#(true()) -> active#(true())
      mark#(add(X1,X2)) -> mark#(X1) ->
      mark#(false()) -> active#(false())
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
      active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X)))))
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
      active#(add(0(),X)) -> mark#(X)
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
      active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
      active#(prod(0(),X)) -> mark#(0())
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
      active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y)))
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
      active#(if(true(),X,Y)) -> mark#(X)
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
      active#(if(false(),X,Y)) -> mark#(Y)
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
      active#(zero(0())) -> mark#(true())
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
      active#(zero(s(X))) -> mark#(false())
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
      active#(p(s(X))) -> mark#(X)
      mark#(if(X1,X2,X3)) -> mark#(X1) ->
      mark#(fact(X)) -> mark#(X)
      mark#(if(X1,X2,X3)) -> mark#(X1) ->
      mark#(fact(X)) -> active#(fact(mark(X)))
      mark#(if(X1,X2,X3)) -> mark#(X1) ->
      mark#(if(X1,X2,X3)) -> mark#(X1)
      mark#(if(X1,X2,X3)) -> mark#(X1) ->
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
      mark#(if(X1,X2,X3)) -> mark#(X1) ->
      mark#(zero(X)) -> mark#(X)
      mark#(if(X1,X2,X3)) -> mark#(X1) ->
      mark#(zero(X)) -> active#(zero(mark(X)))
      mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
      mark#(if(X1,X2,X3)) -> mark#(X1) ->
      mark#(s(X)) -> active#(s(mark(X)))
      mark#(if(X1,X2,X3)) -> mark#(X1) ->
      mark#(0()) -> active#(0())
      mark#(if(X1,X2,X3)) -> mark#(X1) ->
      mark#(prod(X1,X2)) -> mark#(X2)
      mark#(if(X1,X2,X3)) -> mark#(X1) ->
      mark#(prod(X1,X2)) -> mark#(X1)
      mark#(if(X1,X2,X3)) -> mark#(X1) ->
      mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
      mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(p(X)) -> mark#(X)
      mark#(if(X1,X2,X3)) -> mark#(X1) ->
      mark#(p(X)) -> active#(p(mark(X)))
      mark#(if(X1,X2,X3)) -> mark#(X1) ->
      mark#(add(X1,X2)) -> mark#(X2)
      mark#(if(X1,X2,X3)) -> mark#(X1) ->
      mark#(add(X1,X2)) -> mark#(X1)
      mark#(if(X1,X2,X3)) -> mark#(X1) ->
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
      mark#(if(X1,X2,X3)) -> mark#(X1) ->
      mark#(true()) -> active#(true())
      mark#(if(X1,X2,X3)) -> mark#(X1) ->
      mark#(false()) -> active#(false())
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
      active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X)))))
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
      active#(add(0(),X)) -> mark#(X)
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
      active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
      active#(prod(0(),X)) -> mark#(0())
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
      active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y)))
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
      active#(if(true(),X,Y)) -> mark#(X)
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
      active#(if(false(),X,Y)) -> mark#(Y)
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
      active#(zero(0())) -> mark#(true())
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
      active#(zero(s(X))) -> mark#(false())
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
      active#(p(s(X))) -> mark#(X)
      mark#(prod(X1,X2)) -> mark#(X2) -> mark#(fact(X)) -> mark#(X)
      mark#(prod(X1,X2)) -> mark#(X2) ->
      mark#(fact(X)) -> active#(fact(mark(X)))
      mark#(prod(X1,X2)) -> mark#(X2) ->
      mark#(if(X1,X2,X3)) -> mark#(X1)
      mark#(prod(X1,X2)) -> mark#(X2) ->
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
      mark#(prod(X1,X2)) -> mark#(X2) -> mark#(zero(X)) -> mark#(X)
      mark#(prod(X1,X2)) -> mark#(X2) ->
      mark#(zero(X)) -> active#(zero(mark(X)))
      mark#(prod(X1,X2)) -> mark#(X2) -> mark#(s(X)) -> mark#(X)
      mark#(prod(X1,X2)) -> mark#(X2) ->
      mark#(s(X)) -> active#(s(mark(X)))
      mark#(prod(X1,X2)) -> mark#(X2) -> mark#(0()) -> active#(0())
      mark#(prod(X1,X2)) -> mark#(X2) ->
      mark#(prod(X1,X2)) -> mark#(X2)
      mark#(prod(X1,X2)) -> mark#(X2) ->
      mark#(prod(X1,X2)) -> mark#(X1)
      mark#(prod(X1,X2)) -> mark#(X2) ->
      mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
      mark#(prod(X1,X2)) -> mark#(X2) -> mark#(p(X)) -> mark#(X)
      mark#(prod(X1,X2)) -> mark#(X2) ->
      mark#(p(X)) -> active#(p(mark(X)))
      mark#(prod(X1,X2)) -> mark#(X2) ->
      mark#(add(X1,X2)) -> mark#(X2)
      mark#(prod(X1,X2)) -> mark#(X2) ->
      mark#(add(X1,X2)) -> mark#(X1)
      mark#(prod(X1,X2)) -> mark#(X2) ->
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
      mark#(prod(X1,X2)) -> mark#(X2) ->
      mark#(true()) -> active#(true())
      mark#(prod(X1,X2)) -> mark#(X2) ->
      mark#(false()) -> active#(false())
      mark#(prod(X1,X2)) -> mark#(X1) -> mark#(fact(X)) -> mark#(X)
      mark#(prod(X1,X2)) -> mark#(X1) ->
      mark#(fact(X)) -> active#(fact(mark(X)))
      mark#(prod(X1,X2)) -> mark#(X1) ->
      mark#(if(X1,X2,X3)) -> mark#(X1)
      mark#(prod(X1,X2)) -> mark#(X1) ->
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
      mark#(prod(X1,X2)) -> mark#(X1) -> mark#(zero(X)) -> mark#(X)
      mark#(prod(X1,X2)) -> mark#(X1) ->
      mark#(zero(X)) -> active#(zero(mark(X)))
      mark#(prod(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
      mark#(prod(X1,X2)) -> mark#(X1) ->
      mark#(s(X)) -> active#(s(mark(X)))
      mark#(prod(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
      mark#(prod(X1,X2)) -> mark#(X1) ->
      mark#(prod(X1,X2)) -> mark#(X2)
      mark#(prod(X1,X2)) -> mark#(X1) ->
      mark#(prod(X1,X2)) -> mark#(X1)
      mark#(prod(X1,X2)) -> mark#(X1) ->
      mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
      mark#(prod(X1,X2)) -> mark#(X1) -> mark#(p(X)) -> mark#(X)
      mark#(prod(X1,X2)) -> mark#(X1) ->
      mark#(p(X)) -> active#(p(mark(X)))
      mark#(prod(X1,X2)) -> mark#(X1) ->
      mark#(add(X1,X2)) -> mark#(X2)
      mark#(prod(X1,X2)) -> mark#(X1) ->
      mark#(add(X1,X2)) -> mark#(X1)
      mark#(prod(X1,X2)) -> mark#(X1) ->
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
      mark#(prod(X1,X2)) -> mark#(X1) ->
      mark#(true()) -> active#(true())
      mark#(prod(X1,X2)) -> mark#(X1) ->
      mark#(false()) -> active#(false())
      mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2))) ->
      active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X)))))
      mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2))) ->
      active#(add(0(),X)) -> mark#(X)
      mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2))) ->
      active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
      mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2))) ->
      active#(prod(0(),X)) -> mark#(0())
      mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2))) ->
      active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y)))
      mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2))) ->
      active#(if(true(),X,Y)) -> mark#(X)
      mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2))) ->
      active#(if(false(),X,Y)) -> mark#(Y)
      mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2))) ->
      active#(zero(0())) -> mark#(true())
      mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2))) ->
      active#(zero(s(X))) -> mark#(false())
      mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2))) ->
      active#(p(s(X))) -> mark#(X)
      mark#(p(X)) -> mark#(X) -> mark#(fact(X)) -> mark#(X)
      mark#(p(X)) -> mark#(X) -> mark#(fact(X)) -> active#(fact(mark(X)))
      mark#(p(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1)
      mark#(p(X)) -> mark#(X) ->
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
      mark#(p(X)) -> mark#(X) -> mark#(zero(X)) -> mark#(X)
      mark#(p(X)) -> mark#(X) -> mark#(zero(X)) -> active#(zero(mark(X)))
      mark#(p(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
      mark#(p(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
      mark#(p(X)) -> mark#(X) -> mark#(0()) -> active#(0())
      mark#(p(X)) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X2)
      mark#(p(X)) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X1)
      mark#(p(X)) -> mark#(X) ->
      mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
      mark#(p(X)) -> mark#(X) -> mark#(p(X)) -> mark#(X)
      mark#(p(X)) -> mark#(X) -> mark#(p(X)) -> active#(p(mark(X)))
      mark#(p(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2)
      mark#(p(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1)
      mark#(p(X)) -> mark#(X) ->
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
      mark#(p(X)) -> mark#(X) -> mark#(true()) -> active#(true())
      mark#(p(X)) -> mark#(X) ->
      mark#(false()) -> active#(false())
      mark#(p(X)) -> active#(p(mark(X))) ->
      active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X)))))
      mark#(p(X)) -> active#(p(mark(X))) ->
      active#(add(0(),X)) -> mark#(X)
      mark#(p(X)) -> active#(p(mark(X))) ->
      active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
      mark#(p(X)) -> active#(p(mark(X))) ->
      active#(prod(0(),X)) -> mark#(0())
      mark#(p(X)) -> active#(p(mark(X))) ->
      active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y)))
      mark#(p(X)) -> active#(p(mark(X))) ->
      active#(if(true(),X,Y)) -> mark#(X)
      mark#(p(X)) -> active#(p(mark(X))) ->
      active#(if(false(),X,Y)) -> mark#(Y)
      mark#(p(X)) -> active#(p(mark(X))) ->
      active#(zero(0())) -> mark#(true())
      mark#(p(X)) -> active#(p(mark(X))) ->
      active#(zero(s(X))) -> mark#(false())
      mark#(p(X)) -> active#(p(mark(X))) -> active#(p(s(X))) -> mark#(X)
      mark#(s(X)) -> mark#(X) -> mark#(fact(X)) -> mark#(X)
      mark#(s(X)) -> mark#(X) -> mark#(fact(X)) -> active#(fact(mark(X)))
      mark#(s(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1)
      mark#(s(X)) -> mark#(X) ->
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
      mark#(s(X)) -> mark#(X) -> mark#(zero(X)) -> mark#(X)
      mark#(s(X)) -> mark#(X) -> mark#(zero(X)) -> active#(zero(mark(X)))
      mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
      mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
      mark#(s(X)) -> mark#(X) -> mark#(0()) -> active#(0())
      mark#(s(X)) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X2)
      mark#(s(X)) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X1)
      mark#(s(X)) -> mark#(X) ->
      mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
      mark#(s(X)) -> mark#(X) -> mark#(p(X)) -> mark#(X)
      mark#(s(X)) -> mark#(X) -> mark#(p(X)) -> active#(p(mark(X)))
      mark#(s(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2)
      mark#(s(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1)
      mark#(s(X)) -> mark#(X) ->
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
      mark#(s(X)) -> mark#(X) -> mark#(true()) -> active#(true())
      mark#(s(X)) -> mark#(X) ->
      mark#(false()) -> active#(false())
      mark#(s(X)) -> active#(s(mark(X))) ->
      active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X)))))
      mark#(s(X)) -> active#(s(mark(X))) ->
      active#(add(0(),X)) -> mark#(X)
      mark#(s(X)) -> active#(s(mark(X))) ->
      active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
      mark#(s(X)) -> active#(s(mark(X))) ->
      active#(prod(0(),X)) -> mark#(0())
      mark#(s(X)) -> active#(s(mark(X))) ->
      active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y)))
      mark#(s(X)) -> active#(s(mark(X))) ->
      active#(if(true(),X,Y)) -> mark#(X)
      mark#(s(X)) -> active#(s(mark(X))) ->
      active#(if(false(),X,Y)) -> mark#(Y)
      mark#(s(X)) -> active#(s(mark(X))) ->
      active#(zero(0())) -> mark#(true())
      mark#(s(X)) -> active#(s(mark(X))) ->
      active#(zero(s(X))) -> mark#(false())
      mark#(s(X)) -> active#(s(mark(X))) -> active#(p(s(X))) -> mark#(X)
      mark#(zero(X)) -> mark#(X) -> mark#(fact(X)) -> mark#(X)
      mark#(zero(X)) -> mark#(X) ->
      mark#(fact(X)) -> active#(fact(mark(X)))
      mark#(zero(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1)
      mark#(zero(X)) -> mark#(X) ->
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
      mark#(zero(X)) -> mark#(X) -> mark#(zero(X)) -> mark#(X)
      mark#(zero(X)) -> mark#(X) ->
      mark#(zero(X)) -> active#(zero(mark(X)))
      mark#(zero(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
      mark#(zero(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
      mark#(zero(X)) -> mark#(X) -> mark#(0()) -> active#(0())
      mark#(zero(X)) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X2)
      mark#(zero(X)) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X1)
      mark#(zero(X)) -> mark#(X) ->
      mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
      mark#(zero(X)) -> mark#(X) -> mark#(p(X)) -> mark#(X)
      mark#(zero(X)) -> mark#(X) -> mark#(p(X)) -> active#(p(mark(X)))
      mark#(zero(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2)
      mark#(zero(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1)
      mark#(zero(X)) -> mark#(X) ->
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
      mark#(zero(X)) -> mark#(X) -> mark#(true()) -> active#(true())
      mark#(zero(X)) -> mark#(X) ->
      mark#(false()) -> active#(false())
      mark#(zero(X)) -> active#(zero(mark(X))) ->
      active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X)))))
      mark#(zero(X)) -> active#(zero(mark(X))) ->
      active#(add(0(),X)) -> mark#(X)
      mark#(zero(X)) -> active#(zero(mark(X))) ->
      active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
      mark#(zero(X)) -> active#(zero(mark(X))) ->
      active#(prod(0(),X)) -> mark#(0())
      mark#(zero(X)) -> active#(zero(mark(X))) ->
      active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y)))
      mark#(zero(X)) -> active#(zero(mark(X))) ->
      active#(if(true(),X,Y)) -> mark#(X)
      mark#(zero(X)) -> active#(zero(mark(X))) ->
      active#(if(false(),X,Y)) -> mark#(Y)
      mark#(zero(X)) -> active#(zero(mark(X))) ->
      active#(zero(0())) -> mark#(true())
      mark#(zero(X)) -> active#(zero(mark(X))) ->
      active#(zero(s(X))) -> mark#(false())
      mark#(zero(X)) -> active#(zero(mark(X))) ->
      active#(p(s(X))) -> mark#(X)
      mark#(fact(X)) -> mark#(X) -> mark#(fact(X)) -> mark#(X)
      mark#(fact(X)) -> mark#(X) ->
      mark#(fact(X)) -> active#(fact(mark(X)))
      mark#(fact(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1)
      mark#(fact(X)) -> mark#(X) ->
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
      mark#(fact(X)) -> mark#(X) -> mark#(zero(X)) -> mark#(X)
      mark#(fact(X)) -> mark#(X) ->
      mark#(zero(X)) -> active#(zero(mark(X)))
      mark#(fact(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
      mark#(fact(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
      mark#(fact(X)) -> mark#(X) -> mark#(0()) -> active#(0())
      mark#(fact(X)) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X2)
      mark#(fact(X)) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X1)
      mark#(fact(X)) -> mark#(X) ->
      mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
      mark#(fact(X)) -> mark#(X) -> mark#(p(X)) -> mark#(X)
      mark#(fact(X)) -> mark#(X) -> mark#(p(X)) -> active#(p(mark(X)))
      mark#(fact(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2)
      mark#(fact(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1)
      mark#(fact(X)) -> mark#(X) ->
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
      mark#(fact(X)) -> mark#(X) -> mark#(true()) -> active#(true())
      mark#(fact(X)) -> mark#(X) ->
      mark#(false()) -> active#(false())
      mark#(fact(X)) -> active#(fact(mark(X))) ->
      active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X)))))
      mark#(fact(X)) -> active#(fact(mark(X))) ->
      active#(add(0(),X)) -> mark#(X)
      mark#(fact(X)) -> active#(fact(mark(X))) ->
      active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
      mark#(fact(X)) -> active#(fact(mark(X))) ->
      active#(prod(0(),X)) -> mark#(0())
      mark#(fact(X)) -> active#(fact(mark(X))) ->
      active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y)))
      mark#(fact(X)) -> active#(fact(mark(X))) ->
      active#(if(true(),X,Y)) -> mark#(X)
      mark#(fact(X)) -> active#(fact(mark(X))) ->
      active#(if(false(),X,Y)) -> mark#(Y)
      mark#(fact(X)) -> active#(fact(mark(X))) ->
      active#(zero(0())) -> mark#(true())
      mark#(fact(X)) -> active#(fact(mark(X))) ->
      active#(zero(s(X))) -> mark#(false())
      mark#(fact(X)) -> active#(fact(mark(X))) ->
      active#(p(s(X))) -> mark#(X)
      active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
      mark#(fact(X)) -> mark#(X)
      active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
      mark#(fact(X)) -> active#(fact(mark(X)))
      active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
      mark#(if(X1,X2,X3)) -> mark#(X1)
      active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
      active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
      mark#(zero(X)) -> mark#(X)
      active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
      mark#(zero(X)) -> active#(zero(mark(X)))
      active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
      mark#(s(X)) -> mark#(X)
      active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
      mark#(s(X)) -> active#(s(mark(X)))
      active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
      mark#(prod(X1,X2)) -> mark#(X2)
      active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
      mark#(prod(X1,X2)) -> mark#(X1)
      active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
      mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
      active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
      mark#(p(X)) -> mark#(X)
      active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
      mark#(p(X)) -> active#(p(mark(X)))
      active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
      mark#(add(X1,X2)) -> mark#(X2)
      active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
      mark#(add(X1,X2)) -> mark#(X1)
      active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
      active#(add(0(),X)) -> mark#(X) -> mark#(fact(X)) -> mark#(X)
      active#(add(0(),X)) -> mark#(X) ->
      mark#(fact(X)) -> active#(fact(mark(X)))
      active#(add(0(),X)) -> mark#(X) ->
      mark#(if(X1,X2,X3)) -> mark#(X1)
      active#(add(0(),X)) -> mark#(X) ->
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
      active#(add(0(),X)) -> mark#(X) -> mark#(zero(X)) -> mark#(X)
      active#(add(0(),X)) -> mark#(X) ->
      mark#(zero(X)) -> active#(zero(mark(X)))
      active#(add(0(),X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
      active#(add(0(),X)) -> mark#(X) ->
      mark#(s(X)) -> active#(s(mark(X)))
      active#(add(0(),X)) -> mark#(X) -> mark#(0()) -> active#(0())
      active#(add(0(),X)) -> mark#(X) ->
      mark#(prod(X1,X2)) -> mark#(X2)
      active#(add(0(),X)) -> mark#(X) ->
      mark#(prod(X1,X2)) -> mark#(X1)
      active#(add(0(),X)) -> mark#(X) ->
      mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
      active#(add(0(),X)) -> mark#(X) -> mark#(p(X)) -> mark#(X)
      active#(add(0(),X)) -> mark#(X) ->
      mark#(p(X)) -> active#(p(mark(X)))
      active#(add(0(),X)) -> mark#(X) ->
      mark#(add(X1,X2)) -> mark#(X2)
      active#(add(0(),X)) -> mark#(X) ->
      mark#(add(X1,X2)) -> mark#(X1)
      active#(add(0(),X)) -> mark#(X) ->
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
      active#(add(0(),X)) -> mark#(X) ->
      mark#(true()) -> active#(true())
      active#(add(0(),X)) -> mark#(X) ->
      mark#(false()) -> active#(false())
      active#(if(false(),X,Y)) -> mark#(Y) ->
      mark#(fact(X)) -> mark#(X)
      active#(if(false(),X,Y)) -> mark#(Y) ->
      mark#(fact(X)) -> active#(fact(mark(X)))
      active#(if(false(),X,Y)) -> mark#(Y) ->
      mark#(if(X1,X2,X3)) -> mark#(X1)
      active#(if(false(),X,Y)) -> mark#(Y) ->
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
      active#(if(false(),X,Y)) -> mark#(Y) ->
      mark#(zero(X)) -> mark#(X)
      active#(if(false(),X,Y)) -> mark#(Y) ->
      mark#(zero(X)) -> active#(zero(mark(X)))
      active#(if(false(),X,Y)) -> mark#(Y) ->
      mark#(s(X)) -> mark#(X)
      active#(if(false(),X,Y)) -> mark#(Y) ->
      mark#(s(X)) -> active#(s(mark(X)))
      active#(if(false(),X,Y)) -> mark#(Y) ->
      mark#(0()) -> active#(0())
      active#(if(false(),X,Y)) -> mark#(Y) ->
      mark#(prod(X1,X2)) -> mark#(X2)
      active#(if(false(),X,Y)) -> mark#(Y) ->
      mark#(prod(X1,X2)) -> mark#(X1)
      active#(if(false(),X,Y)) -> mark#(Y) ->
      mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
      active#(if(false(),X,Y)) -> mark#(Y) ->
      mark#(p(X)) -> mark#(X)
      active#(if(false(),X,Y)) -> mark#(Y) ->
      mark#(p(X)) -> active#(p(mark(X)))
      active#(if(false(),X,Y)) -> mark#(Y) ->
      mark#(add(X1,X2)) -> mark#(X2)
      active#(if(false(),X,Y)) -> mark#(Y) ->
      mark#(add(X1,X2)) -> mark#(X1)
      active#(if(false(),X,Y)) -> mark#(Y) ->
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
      active#(if(false(),X,Y)) -> mark#(Y) ->
      mark#(true()) -> active#(true())
      active#(if(false(),X,Y)) -> mark#(Y) ->
      mark#(false()) -> active#(false())
      active#(if(true(),X,Y)) -> mark#(X) ->
      mark#(fact(X)) -> mark#(X)
      active#(if(true(),X,Y)) -> mark#(X) ->
      mark#(fact(X)) -> active#(fact(mark(X)))
      active#(if(true(),X,Y)) -> mark#(X) ->
      mark#(if(X1,X2,X3)) -> mark#(X1)
      active#(if(true(),X,Y)) -> mark#(X) ->
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
      active#(if(true(),X,Y)) -> mark#(X) ->
      mark#(zero(X)) -> mark#(X)
      active#(if(true(),X,Y)) -> mark#(X) ->
      mark#(zero(X)) -> active#(zero(mark(X)))
      active#(if(true(),X,Y)) -> mark#(X) ->
      mark#(s(X)) -> mark#(X)
      active#(if(true(),X,Y)) -> mark#(X) ->
      mark#(s(X)) -> active#(s(mark(X)))
      active#(if(true(),X,Y)) -> mark#(X) ->
      mark#(0()) -> active#(0())
      active#(if(true(),X,Y)) -> mark#(X) ->
      mark#(prod(X1,X2)) -> mark#(X2)
      active#(if(true(),X,Y)) -> mark#(X) ->
      mark#(prod(X1,X2)) -> mark#(X1)
      active#(if(true(),X,Y)) -> mark#(X) ->
      mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
      active#(if(true(),X,Y)) -> mark#(X) ->
      mark#(p(X)) -> mark#(X)
      active#(if(true(),X,Y)) -> mark#(X) ->
      mark#(p(X)) -> active#(p(mark(X)))
      active#(if(true(),X,Y)) -> mark#(X) ->
      mark#(add(X1,X2)) -> mark#(X2)
      active#(if(true(),X,Y)) -> mark#(X) ->
      mark#(add(X1,X2)) -> mark#(X1)
      active#(if(true(),X,Y)) -> mark#(X) ->
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
      active#(if(true(),X,Y)) -> mark#(X) ->
      mark#(true()) -> active#(true())
      active#(if(true(),X,Y)) -> mark#(X) ->
      mark#(false()) -> active#(false())
      active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
      mark#(fact(X)) -> mark#(X)
      active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
      mark#(fact(X)) -> active#(fact(mark(X)))
      active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
      mark#(if(X1,X2,X3)) -> mark#(X1)
      active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
      active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
      mark#(zero(X)) -> mark#(X)
      active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
      mark#(zero(X)) -> active#(zero(mark(X)))
      active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
      mark#(s(X)) -> mark#(X)
      active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
      mark#(s(X)) -> active#(s(mark(X)))
      active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
      mark#(prod(X1,X2)) -> mark#(X2)
      active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
      mark#(prod(X1,X2)) -> mark#(X1)
      active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
      mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
      active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
      mark#(p(X)) -> mark#(X)
      active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
      mark#(p(X)) -> active#(p(mark(X)))
      active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
      mark#(add(X1,X2)) -> mark#(X2)
      active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
      mark#(add(X1,X2)) -> mark#(X1)
      active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
      active#(prod(0(),X)) -> mark#(0()) -> mark#(0()) -> active#(0())
      active#(p(s(X))) -> mark#(X) -> mark#(fact(X)) -> mark#(X)
      active#(p(s(X))) -> mark#(X) ->
      mark#(fact(X)) -> active#(fact(mark(X)))
      active#(p(s(X))) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1)
      active#(p(s(X))) -> mark#(X) ->
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
      active#(p(s(X))) -> mark#(X) -> mark#(zero(X)) -> mark#(X)
      active#(p(s(X))) -> mark#(X) ->
      mark#(zero(X)) -> active#(zero(mark(X)))
      active#(p(s(X))) -> mark#(X) -> mark#(s(X)) -> mark#(X)
      active#(p(s(X))) -> mark#(X) ->
      mark#(s(X)) -> active#(s(mark(X)))
      active#(p(s(X))) -> mark#(X) -> mark#(0()) -> active#(0())
      active#(p(s(X))) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X2)
      active#(p(s(X))) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X1)
      active#(p(s(X))) -> mark#(X) ->
      mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
      active#(p(s(X))) -> mark#(X) -> mark#(p(X)) -> mark#(X)
      active#(p(s(X))) -> mark#(X) ->
      mark#(p(X)) -> active#(p(mark(X)))
      active#(p(s(X))) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2)
      active#(p(s(X))) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1)
      active#(p(s(X))) -> mark#(X) ->
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
      active#(p(s(X))) -> mark#(X) -> mark#(true()) -> active#(true())
      active#(p(s(X))) -> mark#(X) ->
      mark#(false()) -> active#(false())
      active#(zero(s(X))) -> mark#(false()) ->
      mark#(false()) -> active#(false())
      active#(zero(0())) -> mark#(true()) ->
      mark#(true()) -> active#(true())
      active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
      mark#(fact(X)) -> mark#(X)
      active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
      mark#(fact(X)) -> active#(fact(mark(X)))
      active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
      mark#(if(X1,X2,X3)) -> mark#(X1)
      active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
      active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
      mark#(zero(X)) -> mark#(X)
      active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
      mark#(zero(X)) -> active#(zero(mark(X)))
      active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
      mark#(s(X)) -> mark#(X)
      active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
      mark#(s(X)) -> active#(s(mark(X)))
      active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
      mark#(prod(X1,X2)) -> mark#(X2)
      active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
      mark#(prod(X1,X2)) -> mark#(X1)
      active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
      mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
      active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
      mark#(p(X)) -> mark#(X)
      active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
      mark#(p(X)) -> active#(p(mark(X)))
      active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
      mark#(add(X1,X2)) -> mark#(X2)
      active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
      mark#(add(X1,X2)) -> mark#(X1)
      active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
     CDG Processor:
      DPs:
       mark#(false()) -> active#(false())
       active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X)))))
       mark#(fact(X)) -> mark#(X)
       mark#(fact(X)) -> active#(fact(mark(X)))
       active#(add(0(),X)) -> mark#(X)
       mark#(if(X1,X2,X3)) -> mark#(X1)
       mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
       active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
       mark#(zero(X)) -> mark#(X)
       mark#(zero(X)) -> active#(zero(mark(X)))
       active#(prod(0(),X)) -> mark#(0())
       mark#(s(X)) -> mark#(X)
       mark#(s(X)) -> active#(s(mark(X)))
       active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y)))
       mark#(0()) -> active#(0())
       active#(if(true(),X,Y)) -> mark#(X)
       mark#(prod(X1,X2)) -> mark#(X2)
       mark#(prod(X1,X2)) -> mark#(X1)
       mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
       active#(if(false(),X,Y)) -> mark#(Y)
       mark#(p(X)) -> mark#(X)
       mark#(p(X)) -> active#(p(mark(X)))
       active#(zero(0())) -> mark#(true())
       mark#(add(X1,X2)) -> mark#(X2)
       mark#(add(X1,X2)) -> mark#(X1)
       mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
       active#(zero(s(X))) -> mark#(false())
       mark#(true()) -> active#(true())
       active#(p(s(X))) -> mark#(X)
      TRS:
       active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X)))))
       active(add(0(),X)) -> mark(X)
       active(add(s(X),Y)) -> mark(s(add(X,Y)))
       active(prod(0(),X)) -> mark(0())
       active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y)))
       active(if(true(),X,Y)) -> mark(X)
       active(if(false(),X,Y)) -> mark(Y)
       active(zero(0())) -> mark(true())
       active(zero(s(X))) -> mark(false())
       active(p(s(X))) -> mark(X)
       mark(fact(X)) -> active(fact(mark(X)))
       mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
       mark(zero(X)) -> active(zero(mark(X)))
       mark(s(X)) -> active(s(mark(X)))
       mark(0()) -> active(0())
       mark(prod(X1,X2)) -> active(prod(mark(X1),mark(X2)))
       mark(p(X)) -> active(p(mark(X)))
       mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
       mark(true()) -> active(true())
       mark(false()) -> active(false())
       fact(mark(X)) -> fact(X)
       fact(active(X)) -> fact(X)
       if(mark(X1),X2,X3) -> if(X1,X2,X3)
       if(X1,mark(X2),X3) -> if(X1,X2,X3)
       if(X1,X2,mark(X3)) -> if(X1,X2,X3)
       if(active(X1),X2,X3) -> if(X1,X2,X3)
       if(X1,active(X2),X3) -> if(X1,X2,X3)
       if(X1,X2,active(X3)) -> if(X1,X2,X3)
       zero(mark(X)) -> zero(X)
       zero(active(X)) -> zero(X)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(X)
       prod(mark(X1),X2) -> prod(X1,X2)
       prod(X1,mark(X2)) -> prod(X1,X2)
       prod(active(X1),X2) -> prod(X1,X2)
       prod(X1,active(X2)) -> prod(X1,X2)
       p(mark(X)) -> p(X)
       p(active(X)) -> p(X)
       add(mark(X1),X2) -> add(X1,X2)
       add(X1,mark(X2)) -> add(X1,X2)
       add(active(X1),X2) -> add(X1,X2)
       add(X1,active(X2)) -> add(X1,X2)
      graph:
       mark#(add(X1,X2)) -> mark#(X2) ->
       mark#(false()) -> active#(false())
       mark#(add(X1,X2)) -> mark#(X2) ->
       mark#(true()) -> active#(true())
       mark#(add(X1,X2)) -> mark#(X2) ->
       mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
       mark#(add(X1,X2)) -> mark#(X2) ->
       mark#(add(X1,X2)) -> mark#(X1)
       mark#(add(X1,X2)) -> mark#(X2) ->
       mark#(add(X1,X2)) -> mark#(X2)
       mark#(add(X1,X2)) -> mark#(X2) ->
       mark#(p(X)) -> active#(p(mark(X)))
       mark#(add(X1,X2)) -> mark#(X2) -> mark#(p(X)) -> mark#(X)
       mark#(add(X1,X2)) -> mark#(X2) ->
       mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
       mark#(add(X1,X2)) -> mark#(X2) ->
       mark#(prod(X1,X2)) -> mark#(X1)
       mark#(add(X1,X2)) -> mark#(X2) ->
       mark#(prod(X1,X2)) -> mark#(X2)
       mark#(add(X1,X2)) -> mark#(X2) -> mark#(0()) -> active#(0())
       mark#(add(X1,X2)) -> mark#(X2) ->
       mark#(s(X)) -> active#(s(mark(X)))
       mark#(add(X1,X2)) -> mark#(X2) -> mark#(s(X)) -> mark#(X)
       mark#(add(X1,X2)) -> mark#(X2) ->
       mark#(zero(X)) -> active#(zero(mark(X)))
       mark#(add(X1,X2)) -> mark#(X2) -> mark#(zero(X)) -> mark#(X)
       mark#(add(X1,X2)) -> mark#(X2) ->
       mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
       mark#(add(X1,X2)) -> mark#(X2) ->
       mark#(if(X1,X2,X3)) -> mark#(X1)
       mark#(add(X1,X2)) -> mark#(X2) ->
       mark#(fact(X)) -> active#(fact(mark(X)))
       mark#(add(X1,X2)) -> mark#(X2) -> mark#(fact(X)) -> mark#(X)
       mark#(add(X1,X2)) -> mark#(X1) ->
       mark#(false()) -> active#(false())
       mark#(add(X1,X2)) -> mark#(X1) ->
       mark#(true()) -> active#(true())
       mark#(add(X1,X2)) -> mark#(X1) ->
       mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
       mark#(add(X1,X2)) -> mark#(X1) ->
       mark#(add(X1,X2)) -> mark#(X1)
       mark#(add(X1,X2)) -> mark#(X1) ->
       mark#(add(X1,X2)) -> mark#(X2)
       mark#(add(X1,X2)) -> mark#(X1) ->
       mark#(p(X)) -> active#(p(mark(X)))
       mark#(add(X1,X2)) -> mark#(X1) -> mark#(p(X)) -> mark#(X)
       mark#(add(X1,X2)) -> mark#(X1) ->
       mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
       mark#(add(X1,X2)) -> mark#(X1) ->
       mark#(prod(X1,X2)) -> mark#(X1)
       mark#(add(X1,X2)) -> mark#(X1) ->
       mark#(prod(X1,X2)) -> mark#(X2)
       mark#(add(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
       mark#(add(X1,X2)) -> mark#(X1) ->
       mark#(s(X)) -> active#(s(mark(X)))
       mark#(add(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
       mark#(add(X1,X2)) -> mark#(X1) ->
       mark#(zero(X)) -> active#(zero(mark(X)))
       mark#(add(X1,X2)) -> mark#(X1) -> mark#(zero(X)) -> mark#(X)
       mark#(add(X1,X2)) -> mark#(X1) ->
       mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
       mark#(add(X1,X2)) -> mark#(X1) ->
       mark#(if(X1,X2,X3)) -> mark#(X1)
       mark#(add(X1,X2)) -> mark#(X1) ->
       mark#(fact(X)) -> active#(fact(mark(X)))
       mark#(add(X1,X2)) -> mark#(X1) ->
       mark#(fact(X)) -> mark#(X)
       mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
       active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
       mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
       active#(add(0(),X)) -> mark#(X)
       mark#(if(X1,X2,X3)) -> mark#(X1) ->
       mark#(false()) -> active#(false())
       mark#(if(X1,X2,X3)) -> mark#(X1) ->
       mark#(true()) -> active#(true())
       mark#(if(X1,X2,X3)) -> mark#(X1) ->
       mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
       mark#(if(X1,X2,X3)) -> mark#(X1) ->
       mark#(add(X1,X2)) -> mark#(X1)
       mark#(if(X1,X2,X3)) -> mark#(X1) ->
       mark#(add(X1,X2)) -> mark#(X2)
       mark#(if(X1,X2,X3)) -> mark#(X1) ->
       mark#(p(X)) -> active#(p(mark(X)))
       mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(p(X)) -> mark#(X)
       mark#(if(X1,X2,X3)) -> mark#(X1) ->
       mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
       mark#(if(X1,X2,X3)) -> mark#(X1) ->
       mark#(prod(X1,X2)) -> mark#(X1)
       mark#(if(X1,X2,X3)) -> mark#(X1) ->
       mark#(prod(X1,X2)) -> mark#(X2)
       mark#(if(X1,X2,X3)) -> mark#(X1) ->
       mark#(0()) -> active#(0())
       mark#(if(X1,X2,X3)) -> mark#(X1) ->
       mark#(s(X)) -> active#(s(mark(X)))
       mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
       mark#(if(X1,X2,X3)) -> mark#(X1) ->
       mark#(zero(X)) -> active#(zero(mark(X)))
       mark#(if(X1,X2,X3)) -> mark#(X1) ->
       mark#(zero(X)) -> mark#(X)
       mark#(if(X1,X2,X3)) -> mark#(X1) ->
       mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
       mark#(if(X1,X2,X3)) -> mark#(X1) ->
       mark#(if(X1,X2,X3)) -> mark#(X1)
       mark#(if(X1,X2,X3)) -> mark#(X1) ->
       mark#(fact(X)) -> active#(fact(mark(X)))
       mark#(if(X1,X2,X3)) -> mark#(X1) ->
       mark#(fact(X)) -> mark#(X)
       mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
       active#(if(false(),X,Y)) -> mark#(Y)
       mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
       active#(if(true(),X,Y)) -> mark#(X)
       mark#(prod(X1,X2)) -> mark#(X2) ->
       mark#(false()) -> active#(false())
       mark#(prod(X1,X2)) -> mark#(X2) ->
       mark#(true()) -> active#(true())
       mark#(prod(X1,X2)) -> mark#(X2) ->
       mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
       mark#(prod(X1,X2)) -> mark#(X2) ->
       mark#(add(X1,X2)) -> mark#(X1)
       mark#(prod(X1,X2)) -> mark#(X2) ->
       mark#(add(X1,X2)) -> mark#(X2)
       mark#(prod(X1,X2)) -> mark#(X2) ->
       mark#(p(X)) -> active#(p(mark(X)))
       mark#(prod(X1,X2)) -> mark#(X2) -> mark#(p(X)) -> mark#(X)
       mark#(prod(X1,X2)) -> mark#(X2) ->
       mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
       mark#(prod(X1,X2)) -> mark#(X2) ->
       mark#(prod(X1,X2)) -> mark#(X1)
       mark#(prod(X1,X2)) -> mark#(X2) ->
       mark#(prod(X1,X2)) -> mark#(X2)
       mark#(prod(X1,X2)) -> mark#(X2) -> mark#(0()) -> active#(0())
       mark#(prod(X1,X2)) -> mark#(X2) ->
       mark#(s(X)) -> active#(s(mark(X)))
       mark#(prod(X1,X2)) -> mark#(X2) -> mark#(s(X)) -> mark#(X)
       mark#(prod(X1,X2)) -> mark#(X2) ->
       mark#(zero(X)) -> active#(zero(mark(X)))
       mark#(prod(X1,X2)) -> mark#(X2) -> mark#(zero(X)) -> mark#(X)
       mark#(prod(X1,X2)) -> mark#(X2) ->
       mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
       mark#(prod(X1,X2)) -> mark#(X2) ->
       mark#(if(X1,X2,X3)) -> mark#(X1)
       mark#(prod(X1,X2)) -> mark#(X2) ->
       mark#(fact(X)) -> active#(fact(mark(X)))
       mark#(prod(X1,X2)) -> mark#(X2) -> mark#(fact(X)) -> mark#(X)
       mark#(prod(X1,X2)) -> mark#(X1) ->
       mark#(false()) -> active#(false())
       mark#(prod(X1,X2)) -> mark#(X1) ->
       mark#(true()) -> active#(true())
       mark#(prod(X1,X2)) -> mark#(X1) ->
       mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
       mark#(prod(X1,X2)) -> mark#(X1) ->
       mark#(add(X1,X2)) -> mark#(X1)
       mark#(prod(X1,X2)) -> mark#(X1) ->
       mark#(add(X1,X2)) -> mark#(X2)
       mark#(prod(X1,X2)) -> mark#(X1) ->
       mark#(p(X)) -> active#(p(mark(X)))
       mark#(prod(X1,X2)) -> mark#(X1) -> mark#(p(X)) -> mark#(X)
       mark#(prod(X1,X2)) -> mark#(X1) ->
       mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
       mark#(prod(X1,X2)) -> mark#(X1) ->
       mark#(prod(X1,X2)) -> mark#(X1)
       mark#(prod(X1,X2)) -> mark#(X1) ->
       mark#(prod(X1,X2)) -> mark#(X2)
       mark#(prod(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
       mark#(prod(X1,X2)) -> mark#(X1) ->
       mark#(s(X)) -> active#(s(mark(X)))
       mark#(prod(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
       mark#(prod(X1,X2)) -> mark#(X1) ->
       mark#(zero(X)) -> active#(zero(mark(X)))
       mark#(prod(X1,X2)) -> mark#(X1) -> mark#(zero(X)) -> mark#(X)
       mark#(prod(X1,X2)) -> mark#(X1) ->
       mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
       mark#(prod(X1,X2)) -> mark#(X1) ->
       mark#(if(X1,X2,X3)) -> mark#(X1)
       mark#(prod(X1,X2)) -> mark#(X1) ->
       mark#(fact(X)) -> active#(fact(mark(X)))
       mark#(prod(X1,X2)) -> mark#(X1) ->
       mark#(fact(X)) -> mark#(X)
       mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2))) ->
       active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y)))
       mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2))) ->
       active#(prod(0(),X)) -> mark#(0())
       mark#(p(X)) -> mark#(X) -> mark#(false()) -> active#(false())
       mark#(p(X)) -> mark#(X) -> mark#(true()) -> active#(true())
       mark#(p(X)) -> mark#(X) ->
       mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
       mark#(p(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1)
       mark#(p(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2)
       mark#(p(X)) -> mark#(X) -> mark#(p(X)) -> active#(p(mark(X)))
       mark#(p(X)) -> mark#(X) -> mark#(p(X)) -> mark#(X)
       mark#(p(X)) -> mark#(X) ->
       mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
       mark#(p(X)) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X1)
       mark#(p(X)) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X2)
       mark#(p(X)) -> mark#(X) -> mark#(0()) -> active#(0())
       mark#(p(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
       mark#(p(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
       mark#(p(X)) -> mark#(X) -> mark#(zero(X)) -> active#(zero(mark(X)))
       mark#(p(X)) -> mark#(X) -> mark#(zero(X)) -> mark#(X)
       mark#(p(X)) -> mark#(X) ->
       mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
       mark#(p(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1)
       mark#(p(X)) -> mark#(X) -> mark#(fact(X)) -> active#(fact(mark(X)))
       mark#(p(X)) -> mark#(X) -> mark#(fact(X)) -> mark#(X)
       mark#(p(X)) -> active#(p(mark(X))) -> active#(p(s(X))) -> mark#(X)
       mark#(s(X)) -> mark#(X) -> mark#(false()) -> active#(false())
       mark#(s(X)) -> mark#(X) -> mark#(true()) -> active#(true())
       mark#(s(X)) -> mark#(X) ->
       mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
       mark#(s(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1)
       mark#(s(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2)
       mark#(s(X)) -> mark#(X) -> mark#(p(X)) -> active#(p(mark(X)))
       mark#(s(X)) -> mark#(X) -> mark#(p(X)) -> mark#(X)
       mark#(s(X)) -> mark#(X) ->
       mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
       mark#(s(X)) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X1)
       mark#(s(X)) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X2)
       mark#(s(X)) -> mark#(X) -> mark#(0()) -> active#(0())
       mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
       mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
       mark#(s(X)) -> mark#(X) -> mark#(zero(X)) -> active#(zero(mark(X)))
       mark#(s(X)) -> mark#(X) -> mark#(zero(X)) -> mark#(X)
       mark#(s(X)) -> mark#(X) ->
       mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
       mark#(s(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1)
       mark#(s(X)) -> mark#(X) -> mark#(fact(X)) -> active#(fact(mark(X)))
       mark#(s(X)) -> mark#(X) -> mark#(fact(X)) -> mark#(X)
       mark#(zero(X)) -> mark#(X) -> mark#(false()) -> active#(false())
       mark#(zero(X)) -> mark#(X) -> mark#(true()) -> active#(true())
       mark#(zero(X)) -> mark#(X) ->
       mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
       mark#(zero(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1)
       mark#(zero(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2)
       mark#(zero(X)) -> mark#(X) -> mark#(p(X)) -> active#(p(mark(X)))
       mark#(zero(X)) -> mark#(X) -> mark#(p(X)) -> mark#(X)
       mark#(zero(X)) -> mark#(X) ->
       mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
       mark#(zero(X)) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X1)
       mark#(zero(X)) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X2)
       mark#(zero(X)) -> mark#(X) -> mark#(0()) -> active#(0())
       mark#(zero(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
       mark#(zero(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
       mark#(zero(X)) -> mark#(X) ->
       mark#(zero(X)) -> active#(zero(mark(X)))
       mark#(zero(X)) -> mark#(X) -> mark#(zero(X)) -> mark#(X)
       mark#(zero(X)) -> mark#(X) ->
       mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
       mark#(zero(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1)
       mark#(zero(X)) -> mark#(X) ->
       mark#(fact(X)) -> active#(fact(mark(X)))
       mark#(zero(X)) -> mark#(X) ->
       mark#(fact(X)) -> mark#(X)
       mark#(zero(X)) -> active#(zero(mark(X))) ->
       active#(zero(s(X))) -> mark#(false())
       mark#(zero(X)) -> active#(zero(mark(X))) ->
       active#(zero(0())) -> mark#(true())
       mark#(fact(X)) -> mark#(X) -> mark#(false()) -> active#(false())
       mark#(fact(X)) -> mark#(X) -> mark#(true()) -> active#(true())
       mark#(fact(X)) -> mark#(X) ->
       mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
       mark#(fact(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1)
       mark#(fact(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2)
       mark#(fact(X)) -> mark#(X) -> mark#(p(X)) -> active#(p(mark(X)))
       mark#(fact(X)) -> mark#(X) -> mark#(p(X)) -> mark#(X)
       mark#(fact(X)) -> mark#(X) ->
       mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
       mark#(fact(X)) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X1)
       mark#(fact(X)) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X2)
       mark#(fact(X)) -> mark#(X) -> mark#(0()) -> active#(0())
       mark#(fact(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
       mark#(fact(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
       mark#(fact(X)) -> mark#(X) ->
       mark#(zero(X)) -> active#(zero(mark(X)))
       mark#(fact(X)) -> mark#(X) -> mark#(zero(X)) -> mark#(X)
       mark#(fact(X)) -> mark#(X) ->
       mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
       mark#(fact(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1)
       mark#(fact(X)) -> mark#(X) ->
       mark#(fact(X)) -> active#(fact(mark(X)))
       mark#(fact(X)) -> mark#(X) ->
       mark#(fact(X)) -> mark#(X)
       mark#(fact(X)) -> active#(fact(mark(X))) ->
       active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X)))))
       active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
       mark#(s(X)) -> active#(s(mark(X)))
       active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
       mark#(s(X)) -> mark#(X)
       active#(add(0(),X)) -> mark#(X) ->
       mark#(false()) -> active#(false())
       active#(add(0(),X)) -> mark#(X) ->
       mark#(true()) -> active#(true())
       active#(add(0(),X)) -> mark#(X) ->
       mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
       active#(add(0(),X)) -> mark#(X) ->
       mark#(add(X1,X2)) -> mark#(X1)
       active#(add(0(),X)) -> mark#(X) ->
       mark#(add(X1,X2)) -> mark#(X2)
       active#(add(0(),X)) -> mark#(X) ->
       mark#(p(X)) -> active#(p(mark(X)))
       active#(add(0(),X)) -> mark#(X) -> mark#(p(X)) -> mark#(X)
       active#(add(0(),X)) -> mark#(X) ->
       mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
       active#(add(0(),X)) -> mark#(X) ->
       mark#(prod(X1,X2)) -> mark#(X1)
       active#(add(0(),X)) -> mark#(X) ->
       mark#(prod(X1,X2)) -> mark#(X2)
       active#(add(0(),X)) -> mark#(X) -> mark#(0()) -> active#(0())
       active#(add(0(),X)) -> mark#(X) ->
       mark#(s(X)) -> active#(s(mark(X)))
       active#(add(0(),X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
       active#(add(0(),X)) -> mark#(X) ->
       mark#(zero(X)) -> active#(zero(mark(X)))
       active#(add(0(),X)) -> mark#(X) -> mark#(zero(X)) -> mark#(X)
       active#(add(0(),X)) -> mark#(X) ->
       mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
       active#(add(0(),X)) -> mark#(X) ->
       mark#(if(X1,X2,X3)) -> mark#(X1)
       active#(add(0(),X)) -> mark#(X) ->
       mark#(fact(X)) -> active#(fact(mark(X)))
       active#(add(0(),X)) -> mark#(X) ->
       mark#(fact(X)) -> mark#(X)
       active#(if(false(),X,Y)) -> mark#(Y) ->
       mark#(false()) -> active#(false())
       active#(if(false(),X,Y)) -> mark#(Y) ->
       mark#(true()) -> active#(true())
       active#(if(false(),X,Y)) -> mark#(Y) ->
       mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
       active#(if(false(),X,Y)) -> mark#(Y) ->
       mark#(add(X1,X2)) -> mark#(X1)
       active#(if(false(),X,Y)) -> mark#(Y) ->
       mark#(add(X1,X2)) -> mark#(X2)
       active#(if(false(),X,Y)) -> mark#(Y) ->
       mark#(p(X)) -> active#(p(mark(X)))
       active#(if(false(),X,Y)) -> mark#(Y) ->
       mark#(p(X)) -> mark#(X)
       active#(if(false(),X,Y)) -> mark#(Y) ->
       mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
       active#(if(false(),X,Y)) -> mark#(Y) ->
       mark#(prod(X1,X2)) -> mark#(X1)
       active#(if(false(),X,Y)) -> mark#(Y) ->
       mark#(prod(X1,X2)) -> mark#(X2)
       active#(if(false(),X,Y)) -> mark#(Y) ->
       mark#(0()) -> active#(0())
       active#(if(false(),X,Y)) -> mark#(Y) ->
       mark#(s(X)) -> active#(s(mark(X)))
       active#(if(false(),X,Y)) -> mark#(Y) ->
       mark#(s(X)) -> mark#(X)
       active#(if(false(),X,Y)) -> mark#(Y) ->
       mark#(zero(X)) -> active#(zero(mark(X)))
       active#(if(false(),X,Y)) -> mark#(Y) ->
       mark#(zero(X)) -> mark#(X)
       active#(if(false(),X,Y)) -> mark#(Y) ->
       mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
       active#(if(false(),X,Y)) -> mark#(Y) ->
       mark#(if(X1,X2,X3)) -> mark#(X1)
       active#(if(false(),X,Y)) -> mark#(Y) ->
       mark#(fact(X)) -> active#(fact(mark(X)))
       active#(if(false(),X,Y)) -> mark#(Y) ->
       mark#(fact(X)) -> mark#(X)
       active#(if(true(),X,Y)) -> mark#(X) ->
       mark#(false()) -> active#(false())
       active#(if(true(),X,Y)) -> mark#(X) ->
       mark#(true()) -> active#(true())
       active#(if(true(),X,Y)) -> mark#(X) ->
       mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
       active#(if(true(),X,Y)) -> mark#(X) ->
       mark#(add(X1,X2)) -> mark#(X1)
       active#(if(true(),X,Y)) -> mark#(X) ->
       mark#(add(X1,X2)) -> mark#(X2)
       active#(if(true(),X,Y)) -> mark#(X) ->
       mark#(p(X)) -> active#(p(mark(X)))
       active#(if(true(),X,Y)) -> mark#(X) ->
       mark#(p(X)) -> mark#(X)
       active#(if(true(),X,Y)) -> mark#(X) ->
       mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
       active#(if(true(),X,Y)) -> mark#(X) ->
       mark#(prod(X1,X2)) -> mark#(X1)
       active#(if(true(),X,Y)) -> mark#(X) ->
       mark#(prod(X1,X2)) -> mark#(X2)
       active#(if(true(),X,Y)) -> mark#(X) ->
       mark#(0()) -> active#(0())
       active#(if(true(),X,Y)) -> mark#(X) ->
       mark#(s(X)) -> active#(s(mark(X)))
       active#(if(true(),X,Y)) -> mark#(X) ->
       mark#(s(X)) -> mark#(X)
       active#(if(true(),X,Y)) -> mark#(X) ->
       mark#(zero(X)) -> active#(zero(mark(X)))
       active#(if(true(),X,Y)) -> mark#(X) ->
       mark#(zero(X)) -> mark#(X)
       active#(if(true(),X,Y)) -> mark#(X) ->
       mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
       active#(if(true(),X,Y)) -> mark#(X) ->
       mark#(if(X1,X2,X3)) -> mark#(X1)
       active#(if(true(),X,Y)) -> mark#(X) ->
       mark#(fact(X)) -> active#(fact(mark(X)))
       active#(if(true(),X,Y)) -> mark#(X) ->
       mark#(fact(X)) -> mark#(X)
       active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
       mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
       active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
       mark#(add(X1,X2)) -> mark#(X1)
       active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y))) ->
       mark#(add(X1,X2)) -> mark#(X2)
       active#(prod(0(),X)) -> mark#(0()) -> mark#(0()) -> active#(0())
       active#(p(s(X))) -> mark#(X) ->
       mark#(false()) -> active#(false())
       active#(p(s(X))) -> mark#(X) -> mark#(true()) -> active#(true())
       active#(p(s(X))) -> mark#(X) ->
       mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
       active#(p(s(X))) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1)
       active#(p(s(X))) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2)
       active#(p(s(X))) -> mark#(X) ->
       mark#(p(X)) -> active#(p(mark(X)))
       active#(p(s(X))) -> mark#(X) -> mark#(p(X)) -> mark#(X)
       active#(p(s(X))) -> mark#(X) ->
       mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
       active#(p(s(X))) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X1)
       active#(p(s(X))) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X2)
       active#(p(s(X))) -> mark#(X) -> mark#(0()) -> active#(0())
       active#(p(s(X))) -> mark#(X) ->
       mark#(s(X)) -> active#(s(mark(X)))
       active#(p(s(X))) -> mark#(X) -> mark#(s(X)) -> mark#(X)
       active#(p(s(X))) -> mark#(X) ->
       mark#(zero(X)) -> active#(zero(mark(X)))
       active#(p(s(X))) -> mark#(X) -> mark#(zero(X)) -> mark#(X)
       active#(p(s(X))) -> mark#(X) ->
       mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
       active#(p(s(X))) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1)
       active#(p(s(X))) -> mark#(X) ->
       mark#(fact(X)) -> active#(fact(mark(X)))
       active#(p(s(X))) -> mark#(X) ->
       mark#(fact(X)) -> mark#(X)
       active#(zero(s(X))) -> mark#(false()) ->
       mark#(false()) -> active#(false())
       active#(zero(0())) -> mark#(true()) ->
       mark#(true()) -> active#(true())
       active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
       mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
       active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X))))) ->
       mark#(if(X1,X2,X3)) -> mark#(X1)
      SCC Processor:
       #sccs: 1
       #rules: 21
       #arcs: 267/841
       DPs:
        mark#(add(X1,X2)) -> mark#(X2)
        mark#(fact(X)) -> mark#(X)
        mark#(fact(X)) -> active#(fact(mark(X)))
        active#(fact(X)) -> mark#(if(zero(X),s(0()),prod(X,fact(p(X)))))
        mark#(if(X1,X2,X3)) -> mark#(X1)
        mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
        active#(if(true(),X,Y)) -> mark#(X)
        mark#(zero(X)) -> mark#(X)
        mark#(s(X)) -> mark#(X)
        mark#(prod(X1,X2)) -> mark#(X2)
        mark#(prod(X1,X2)) -> mark#(X1)
        mark#(prod(X1,X2)) -> active#(prod(mark(X1),mark(X2)))
        active#(prod(s(X),Y)) -> mark#(add(Y,prod(X,Y)))
        mark#(add(X1,X2)) -> mark#(X1)
        mark#(p(X)) -> mark#(X)
        mark#(p(X)) -> active#(p(mark(X)))
        active#(p(s(X))) -> mark#(X)
        mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
        active#(add(0(),X)) -> mark#(X)
        active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
        active#(if(false(),X,Y)) -> mark#(Y)
       TRS:
        active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X)))))
        active(add(0(),X)) -> mark(X)
        active(add(s(X),Y)) -> mark(s(add(X,Y)))
        active(prod(0(),X)) -> mark(0())
        active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y)))
        active(if(true(),X,Y)) -> mark(X)
        active(if(false(),X,Y)) -> mark(Y)
        active(zero(0())) -> mark(true())
        active(zero(s(X))) -> mark(false())
        active(p(s(X))) -> mark(X)
        mark(fact(X)) -> active(fact(mark(X)))
        mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
        mark(zero(X)) -> active(zero(mark(X)))
        mark(s(X)) -> active(s(mark(X)))
        mark(0()) -> active(0())
        mark(prod(X1,X2)) -> active(prod(mark(X1),mark(X2)))
        mark(p(X)) -> active(p(mark(X)))
        mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
        mark(true()) -> active(true())
        mark(false()) -> active(false())
        fact(mark(X)) -> fact(X)
        fact(active(X)) -> fact(X)
        if(mark(X1),X2,X3) -> if(X1,X2,X3)
        if(X1,mark(X2),X3) -> if(X1,X2,X3)
        if(X1,X2,mark(X3)) -> if(X1,X2,X3)
        if(active(X1),X2,X3) -> if(X1,X2,X3)
        if(X1,active(X2),X3) -> if(X1,X2,X3)
        if(X1,X2,active(X3)) -> if(X1,X2,X3)
        zero(mark(X)) -> zero(X)
        zero(active(X)) -> zero(X)
        s(mark(X)) -> s(X)
        s(active(X)) -> s(X)
        prod(mark(X1),X2) -> prod(X1,X2)
        prod(X1,mark(X2)) -> prod(X1,X2)
        prod(active(X1),X2) -> prod(X1,X2)
        prod(X1,active(X2)) -> prod(X1,X2)
        p(mark(X)) -> p(X)
        p(active(X)) -> p(X)
        add(mark(X1),X2) -> add(X1,X2)
        add(X1,mark(X2)) -> add(X1,X2)
        add(active(X1),X2) -> add(X1,X2)
        add(X1,active(X2)) -> add(X1,X2)
       Open
    
    DPs:
     if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
     if#(X1,mark(X2),X3) -> if#(X1,X2,X3)
     if#(X1,X2,mark(X3)) -> if#(X1,X2,X3)
     if#(active(X1),X2,X3) -> if#(X1,X2,X3)
     if#(X1,active(X2),X3) -> if#(X1,X2,X3)
     if#(X1,X2,active(X3)) -> if#(X1,X2,X3)
    TRS:
     active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X)))))
     active(add(0(),X)) -> mark(X)
     active(add(s(X),Y)) -> mark(s(add(X,Y)))
     active(prod(0(),X)) -> mark(0())
     active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y)))
     active(if(true(),X,Y)) -> mark(X)
     active(if(false(),X,Y)) -> mark(Y)
     active(zero(0())) -> mark(true())
     active(zero(s(X))) -> mark(false())
     active(p(s(X))) -> mark(X)
     mark(fact(X)) -> active(fact(mark(X)))
     mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
     mark(zero(X)) -> active(zero(mark(X)))
     mark(s(X)) -> active(s(mark(X)))
     mark(0()) -> active(0())
     mark(prod(X1,X2)) -> active(prod(mark(X1),mark(X2)))
     mark(p(X)) -> active(p(mark(X)))
     mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
     mark(true()) -> active(true())
     mark(false()) -> active(false())
     fact(mark(X)) -> fact(X)
     fact(active(X)) -> fact(X)
     if(mark(X1),X2,X3) -> if(X1,X2,X3)
     if(X1,mark(X2),X3) -> if(X1,X2,X3)
     if(X1,X2,mark(X3)) -> if(X1,X2,X3)
     if(active(X1),X2,X3) -> if(X1,X2,X3)
     if(X1,active(X2),X3) -> if(X1,X2,X3)
     if(X1,X2,active(X3)) -> if(X1,X2,X3)
     zero(mark(X)) -> zero(X)
     zero(active(X)) -> zero(X)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     prod(mark(X1),X2) -> prod(X1,X2)
     prod(X1,mark(X2)) -> prod(X1,X2)
     prod(active(X1),X2) -> prod(X1,X2)
     prod(X1,active(X2)) -> prod(X1,X2)
     p(mark(X)) -> p(X)
     p(active(X)) -> p(X)
     add(mark(X1),X2) -> add(X1,X2)
     add(X1,mark(X2)) -> add(X1,X2)
     add(active(X1),X2) -> add(X1,X2)
     add(X1,active(X2)) -> add(X1,X2)
    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)
       if#(active(X1),X2,X3) -> if#(X1,X2,X3)
       if#(X1,active(X2),X3) -> if#(X1,X2,X3)
      TRS:
       active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X)))))
       active(add(0(),X)) -> mark(X)
       active(add(s(X),Y)) -> mark(s(add(X,Y)))
       active(prod(0(),X)) -> mark(0())
       active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y)))
       active(if(true(),X,Y)) -> mark(X)
       active(if(false(),X,Y)) -> mark(Y)
       active(zero(0())) -> mark(true())
       active(zero(s(X))) -> mark(false())
       active(p(s(X))) -> mark(X)
       mark(fact(X)) -> active(fact(mark(X)))
       mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
       mark(zero(X)) -> active(zero(mark(X)))
       mark(s(X)) -> active(s(mark(X)))
       mark(0()) -> active(0())
       mark(prod(X1,X2)) -> active(prod(mark(X1),mark(X2)))
       mark(p(X)) -> active(p(mark(X)))
       mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
       mark(true()) -> active(true())
       mark(false()) -> active(false())
       fact(mark(X)) -> fact(X)
       fact(active(X)) -> fact(X)
       if(mark(X1),X2,X3) -> if(X1,X2,X3)
       if(X1,mark(X2),X3) -> if(X1,X2,X3)
       if(X1,X2,mark(X3)) -> if(X1,X2,X3)
       if(active(X1),X2,X3) -> if(X1,X2,X3)
       if(X1,active(X2),X3) -> if(X1,X2,X3)
       if(X1,X2,active(X3)) -> if(X1,X2,X3)
       zero(mark(X)) -> zero(X)
       zero(active(X)) -> zero(X)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(X)
       prod(mark(X1),X2) -> prod(X1,X2)
       prod(X1,mark(X2)) -> prod(X1,X2)
       prod(active(X1),X2) -> prod(X1,X2)
       prod(X1,active(X2)) -> prod(X1,X2)
       p(mark(X)) -> p(X)
       p(active(X)) -> p(X)
       add(mark(X1),X2) -> add(X1,X2)
       add(X1,mark(X2)) -> add(X1,X2)
       add(active(X1),X2) -> add(X1,X2)
       add(X1,active(X2)) -> add(X1,X2)
     Subterm Criterion Processor:
      simple projection:
       pi(if#) = 1
      problem:
       DPs:
        if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
        if#(active(X1),X2,X3) -> if#(X1,X2,X3)
       TRS:
        active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X)))))
        active(add(0(),X)) -> mark(X)
        active(add(s(X),Y)) -> mark(s(add(X,Y)))
        active(prod(0(),X)) -> mark(0())
        active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y)))
        active(if(true(),X,Y)) -> mark(X)
        active(if(false(),X,Y)) -> mark(Y)
        active(zero(0())) -> mark(true())
        active(zero(s(X))) -> mark(false())
        active(p(s(X))) -> mark(X)
        mark(fact(X)) -> active(fact(mark(X)))
        mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
        mark(zero(X)) -> active(zero(mark(X)))
        mark(s(X)) -> active(s(mark(X)))
        mark(0()) -> active(0())
        mark(prod(X1,X2)) -> active(prod(mark(X1),mark(X2)))
        mark(p(X)) -> active(p(mark(X)))
        mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
        mark(true()) -> active(true())
        mark(false()) -> active(false())
        fact(mark(X)) -> fact(X)
        fact(active(X)) -> fact(X)
        if(mark(X1),X2,X3) -> if(X1,X2,X3)
        if(X1,mark(X2),X3) -> if(X1,X2,X3)
        if(X1,X2,mark(X3)) -> if(X1,X2,X3)
        if(active(X1),X2,X3) -> if(X1,X2,X3)
        if(X1,active(X2),X3) -> if(X1,X2,X3)
        if(X1,X2,active(X3)) -> if(X1,X2,X3)
        zero(mark(X)) -> zero(X)
        zero(active(X)) -> zero(X)
        s(mark(X)) -> s(X)
        s(active(X)) -> s(X)
        prod(mark(X1),X2) -> prod(X1,X2)
        prod(X1,mark(X2)) -> prod(X1,X2)
        prod(active(X1),X2) -> prod(X1,X2)
        prod(X1,active(X2)) -> prod(X1,X2)
        p(mark(X)) -> p(X)
        p(active(X)) -> p(X)
        add(mark(X1),X2) -> add(X1,X2)
        add(X1,mark(X2)) -> add(X1,X2)
        add(active(X1),X2) -> add(X1,X2)
        add(X1,active(X2)) -> add(X1,X2)
      Subterm Criterion Processor:
       simple projection:
        pi(if#) = 0
       problem:
        DPs:
         
        TRS:
         active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X)))))
         active(add(0(),X)) -> mark(X)
         active(add(s(X),Y)) -> mark(s(add(X,Y)))
         active(prod(0(),X)) -> mark(0())
         active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y)))
         active(if(true(),X,Y)) -> mark(X)
         active(if(false(),X,Y)) -> mark(Y)
         active(zero(0())) -> mark(true())
         active(zero(s(X))) -> mark(false())
         active(p(s(X))) -> mark(X)
         mark(fact(X)) -> active(fact(mark(X)))
         mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
         mark(zero(X)) -> active(zero(mark(X)))
         mark(s(X)) -> active(s(mark(X)))
         mark(0()) -> active(0())
         mark(prod(X1,X2)) -> active(prod(mark(X1),mark(X2)))
         mark(p(X)) -> active(p(mark(X)))
         mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
         mark(true()) -> active(true())
         mark(false()) -> active(false())
         fact(mark(X)) -> fact(X)
         fact(active(X)) -> fact(X)
         if(mark(X1),X2,X3) -> if(X1,X2,X3)
         if(X1,mark(X2),X3) -> if(X1,X2,X3)
         if(X1,X2,mark(X3)) -> if(X1,X2,X3)
         if(active(X1),X2,X3) -> if(X1,X2,X3)
         if(X1,active(X2),X3) -> if(X1,X2,X3)
         if(X1,X2,active(X3)) -> if(X1,X2,X3)
         zero(mark(X)) -> zero(X)
         zero(active(X)) -> zero(X)
         s(mark(X)) -> s(X)
         s(active(X)) -> s(X)
         prod(mark(X1),X2) -> prod(X1,X2)
         prod(X1,mark(X2)) -> prod(X1,X2)
         prod(active(X1),X2) -> prod(X1,X2)
         prod(X1,active(X2)) -> prod(X1,X2)
         p(mark(X)) -> p(X)
         p(active(X)) -> p(X)
         add(mark(X1),X2) -> add(X1,X2)
         add(X1,mark(X2)) -> add(X1,X2)
         add(active(X1),X2) -> add(X1,X2)
         add(X1,active(X2)) -> add(X1,X2)
       Qed
    
    DPs:
     zero#(mark(X)) -> zero#(X)
     zero#(active(X)) -> zero#(X)
    TRS:
     active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X)))))
     active(add(0(),X)) -> mark(X)
     active(add(s(X),Y)) -> mark(s(add(X,Y)))
     active(prod(0(),X)) -> mark(0())
     active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y)))
     active(if(true(),X,Y)) -> mark(X)
     active(if(false(),X,Y)) -> mark(Y)
     active(zero(0())) -> mark(true())
     active(zero(s(X))) -> mark(false())
     active(p(s(X))) -> mark(X)
     mark(fact(X)) -> active(fact(mark(X)))
     mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
     mark(zero(X)) -> active(zero(mark(X)))
     mark(s(X)) -> active(s(mark(X)))
     mark(0()) -> active(0())
     mark(prod(X1,X2)) -> active(prod(mark(X1),mark(X2)))
     mark(p(X)) -> active(p(mark(X)))
     mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
     mark(true()) -> active(true())
     mark(false()) -> active(false())
     fact(mark(X)) -> fact(X)
     fact(active(X)) -> fact(X)
     if(mark(X1),X2,X3) -> if(X1,X2,X3)
     if(X1,mark(X2),X3) -> if(X1,X2,X3)
     if(X1,X2,mark(X3)) -> if(X1,X2,X3)
     if(active(X1),X2,X3) -> if(X1,X2,X3)
     if(X1,active(X2),X3) -> if(X1,X2,X3)
     if(X1,X2,active(X3)) -> if(X1,X2,X3)
     zero(mark(X)) -> zero(X)
     zero(active(X)) -> zero(X)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     prod(mark(X1),X2) -> prod(X1,X2)
     prod(X1,mark(X2)) -> prod(X1,X2)
     prod(active(X1),X2) -> prod(X1,X2)
     prod(X1,active(X2)) -> prod(X1,X2)
     p(mark(X)) -> p(X)
     p(active(X)) -> p(X)
     add(mark(X1),X2) -> add(X1,X2)
     add(X1,mark(X2)) -> add(X1,X2)
     add(active(X1),X2) -> add(X1,X2)
     add(X1,active(X2)) -> add(X1,X2)
    Subterm Criterion Processor:
     simple projection:
      pi(zero#) = 0
     problem:
      DPs:
       
      TRS:
       active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X)))))
       active(add(0(),X)) -> mark(X)
       active(add(s(X),Y)) -> mark(s(add(X,Y)))
       active(prod(0(),X)) -> mark(0())
       active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y)))
       active(if(true(),X,Y)) -> mark(X)
       active(if(false(),X,Y)) -> mark(Y)
       active(zero(0())) -> mark(true())
       active(zero(s(X))) -> mark(false())
       active(p(s(X))) -> mark(X)
       mark(fact(X)) -> active(fact(mark(X)))
       mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
       mark(zero(X)) -> active(zero(mark(X)))
       mark(s(X)) -> active(s(mark(X)))
       mark(0()) -> active(0())
       mark(prod(X1,X2)) -> active(prod(mark(X1),mark(X2)))
       mark(p(X)) -> active(p(mark(X)))
       mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
       mark(true()) -> active(true())
       mark(false()) -> active(false())
       fact(mark(X)) -> fact(X)
       fact(active(X)) -> fact(X)
       if(mark(X1),X2,X3) -> if(X1,X2,X3)
       if(X1,mark(X2),X3) -> if(X1,X2,X3)
       if(X1,X2,mark(X3)) -> if(X1,X2,X3)
       if(active(X1),X2,X3) -> if(X1,X2,X3)
       if(X1,active(X2),X3) -> if(X1,X2,X3)
       if(X1,X2,active(X3)) -> if(X1,X2,X3)
       zero(mark(X)) -> zero(X)
       zero(active(X)) -> zero(X)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(X)
       prod(mark(X1),X2) -> prod(X1,X2)
       prod(X1,mark(X2)) -> prod(X1,X2)
       prod(active(X1),X2) -> prod(X1,X2)
       prod(X1,active(X2)) -> prod(X1,X2)
       p(mark(X)) -> p(X)
       p(active(X)) -> p(X)
       add(mark(X1),X2) -> add(X1,X2)
       add(X1,mark(X2)) -> add(X1,X2)
       add(active(X1),X2) -> add(X1,X2)
       add(X1,active(X2)) -> add(X1,X2)
     Qed
    
    DPs:
     s#(mark(X)) -> s#(X)
     s#(active(X)) -> s#(X)
    TRS:
     active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X)))))
     active(add(0(),X)) -> mark(X)
     active(add(s(X),Y)) -> mark(s(add(X,Y)))
     active(prod(0(),X)) -> mark(0())
     active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y)))
     active(if(true(),X,Y)) -> mark(X)
     active(if(false(),X,Y)) -> mark(Y)
     active(zero(0())) -> mark(true())
     active(zero(s(X))) -> mark(false())
     active(p(s(X))) -> mark(X)
     mark(fact(X)) -> active(fact(mark(X)))
     mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
     mark(zero(X)) -> active(zero(mark(X)))
     mark(s(X)) -> active(s(mark(X)))
     mark(0()) -> active(0())
     mark(prod(X1,X2)) -> active(prod(mark(X1),mark(X2)))
     mark(p(X)) -> active(p(mark(X)))
     mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
     mark(true()) -> active(true())
     mark(false()) -> active(false())
     fact(mark(X)) -> fact(X)
     fact(active(X)) -> fact(X)
     if(mark(X1),X2,X3) -> if(X1,X2,X3)
     if(X1,mark(X2),X3) -> if(X1,X2,X3)
     if(X1,X2,mark(X3)) -> if(X1,X2,X3)
     if(active(X1),X2,X3) -> if(X1,X2,X3)
     if(X1,active(X2),X3) -> if(X1,X2,X3)
     if(X1,X2,active(X3)) -> if(X1,X2,X3)
     zero(mark(X)) -> zero(X)
     zero(active(X)) -> zero(X)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     prod(mark(X1),X2) -> prod(X1,X2)
     prod(X1,mark(X2)) -> prod(X1,X2)
     prod(active(X1),X2) -> prod(X1,X2)
     prod(X1,active(X2)) -> prod(X1,X2)
     p(mark(X)) -> p(X)
     p(active(X)) -> p(X)
     add(mark(X1),X2) -> add(X1,X2)
     add(X1,mark(X2)) -> add(X1,X2)
     add(active(X1),X2) -> add(X1,X2)
     add(X1,active(X2)) -> add(X1,X2)
    Subterm Criterion Processor:
     simple projection:
      pi(s#) = 0
     problem:
      DPs:
       
      TRS:
       active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X)))))
       active(add(0(),X)) -> mark(X)
       active(add(s(X),Y)) -> mark(s(add(X,Y)))
       active(prod(0(),X)) -> mark(0())
       active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y)))
       active(if(true(),X,Y)) -> mark(X)
       active(if(false(),X,Y)) -> mark(Y)
       active(zero(0())) -> mark(true())
       active(zero(s(X))) -> mark(false())
       active(p(s(X))) -> mark(X)
       mark(fact(X)) -> active(fact(mark(X)))
       mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
       mark(zero(X)) -> active(zero(mark(X)))
       mark(s(X)) -> active(s(mark(X)))
       mark(0()) -> active(0())
       mark(prod(X1,X2)) -> active(prod(mark(X1),mark(X2)))
       mark(p(X)) -> active(p(mark(X)))
       mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
       mark(true()) -> active(true())
       mark(false()) -> active(false())
       fact(mark(X)) -> fact(X)
       fact(active(X)) -> fact(X)
       if(mark(X1),X2,X3) -> if(X1,X2,X3)
       if(X1,mark(X2),X3) -> if(X1,X2,X3)
       if(X1,X2,mark(X3)) -> if(X1,X2,X3)
       if(active(X1),X2,X3) -> if(X1,X2,X3)
       if(X1,active(X2),X3) -> if(X1,X2,X3)
       if(X1,X2,active(X3)) -> if(X1,X2,X3)
       zero(mark(X)) -> zero(X)
       zero(active(X)) -> zero(X)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(X)
       prod(mark(X1),X2) -> prod(X1,X2)
       prod(X1,mark(X2)) -> prod(X1,X2)
       prod(active(X1),X2) -> prod(X1,X2)
       prod(X1,active(X2)) -> prod(X1,X2)
       p(mark(X)) -> p(X)
       p(active(X)) -> p(X)
       add(mark(X1),X2) -> add(X1,X2)
       add(X1,mark(X2)) -> add(X1,X2)
       add(active(X1),X2) -> add(X1,X2)
       add(X1,active(X2)) -> add(X1,X2)
     Qed
    
    DPs:
     prod#(mark(X1),X2) -> prod#(X1,X2)
     prod#(X1,mark(X2)) -> prod#(X1,X2)
     prod#(active(X1),X2) -> prod#(X1,X2)
     prod#(X1,active(X2)) -> prod#(X1,X2)
    TRS:
     active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X)))))
     active(add(0(),X)) -> mark(X)
     active(add(s(X),Y)) -> mark(s(add(X,Y)))
     active(prod(0(),X)) -> mark(0())
     active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y)))
     active(if(true(),X,Y)) -> mark(X)
     active(if(false(),X,Y)) -> mark(Y)
     active(zero(0())) -> mark(true())
     active(zero(s(X))) -> mark(false())
     active(p(s(X))) -> mark(X)
     mark(fact(X)) -> active(fact(mark(X)))
     mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
     mark(zero(X)) -> active(zero(mark(X)))
     mark(s(X)) -> active(s(mark(X)))
     mark(0()) -> active(0())
     mark(prod(X1,X2)) -> active(prod(mark(X1),mark(X2)))
     mark(p(X)) -> active(p(mark(X)))
     mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
     mark(true()) -> active(true())
     mark(false()) -> active(false())
     fact(mark(X)) -> fact(X)
     fact(active(X)) -> fact(X)
     if(mark(X1),X2,X3) -> if(X1,X2,X3)
     if(X1,mark(X2),X3) -> if(X1,X2,X3)
     if(X1,X2,mark(X3)) -> if(X1,X2,X3)
     if(active(X1),X2,X3) -> if(X1,X2,X3)
     if(X1,active(X2),X3) -> if(X1,X2,X3)
     if(X1,X2,active(X3)) -> if(X1,X2,X3)
     zero(mark(X)) -> zero(X)
     zero(active(X)) -> zero(X)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     prod(mark(X1),X2) -> prod(X1,X2)
     prod(X1,mark(X2)) -> prod(X1,X2)
     prod(active(X1),X2) -> prod(X1,X2)
     prod(X1,active(X2)) -> prod(X1,X2)
     p(mark(X)) -> p(X)
     p(active(X)) -> p(X)
     add(mark(X1),X2) -> add(X1,X2)
     add(X1,mark(X2)) -> add(X1,X2)
     add(active(X1),X2) -> add(X1,X2)
     add(X1,active(X2)) -> add(X1,X2)
    Subterm Criterion Processor:
     simple projection:
      pi(prod#) = 1
     problem:
      DPs:
       prod#(mark(X1),X2) -> prod#(X1,X2)
       prod#(active(X1),X2) -> prod#(X1,X2)
      TRS:
       active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X)))))
       active(add(0(),X)) -> mark(X)
       active(add(s(X),Y)) -> mark(s(add(X,Y)))
       active(prod(0(),X)) -> mark(0())
       active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y)))
       active(if(true(),X,Y)) -> mark(X)
       active(if(false(),X,Y)) -> mark(Y)
       active(zero(0())) -> mark(true())
       active(zero(s(X))) -> mark(false())
       active(p(s(X))) -> mark(X)
       mark(fact(X)) -> active(fact(mark(X)))
       mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
       mark(zero(X)) -> active(zero(mark(X)))
       mark(s(X)) -> active(s(mark(X)))
       mark(0()) -> active(0())
       mark(prod(X1,X2)) -> active(prod(mark(X1),mark(X2)))
       mark(p(X)) -> active(p(mark(X)))
       mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
       mark(true()) -> active(true())
       mark(false()) -> active(false())
       fact(mark(X)) -> fact(X)
       fact(active(X)) -> fact(X)
       if(mark(X1),X2,X3) -> if(X1,X2,X3)
       if(X1,mark(X2),X3) -> if(X1,X2,X3)
       if(X1,X2,mark(X3)) -> if(X1,X2,X3)
       if(active(X1),X2,X3) -> if(X1,X2,X3)
       if(X1,active(X2),X3) -> if(X1,X2,X3)
       if(X1,X2,active(X3)) -> if(X1,X2,X3)
       zero(mark(X)) -> zero(X)
       zero(active(X)) -> zero(X)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(X)
       prod(mark(X1),X2) -> prod(X1,X2)
       prod(X1,mark(X2)) -> prod(X1,X2)
       prod(active(X1),X2) -> prod(X1,X2)
       prod(X1,active(X2)) -> prod(X1,X2)
       p(mark(X)) -> p(X)
       p(active(X)) -> p(X)
       add(mark(X1),X2) -> add(X1,X2)
       add(X1,mark(X2)) -> add(X1,X2)
       add(active(X1),X2) -> add(X1,X2)
       add(X1,active(X2)) -> add(X1,X2)
     Subterm Criterion Processor:
      simple projection:
       pi(prod#) = 0
      problem:
       DPs:
        
       TRS:
        active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X)))))
        active(add(0(),X)) -> mark(X)
        active(add(s(X),Y)) -> mark(s(add(X,Y)))
        active(prod(0(),X)) -> mark(0())
        active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y)))
        active(if(true(),X,Y)) -> mark(X)
        active(if(false(),X,Y)) -> mark(Y)
        active(zero(0())) -> mark(true())
        active(zero(s(X))) -> mark(false())
        active(p(s(X))) -> mark(X)
        mark(fact(X)) -> active(fact(mark(X)))
        mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
        mark(zero(X)) -> active(zero(mark(X)))
        mark(s(X)) -> active(s(mark(X)))
        mark(0()) -> active(0())
        mark(prod(X1,X2)) -> active(prod(mark(X1),mark(X2)))
        mark(p(X)) -> active(p(mark(X)))
        mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
        mark(true()) -> active(true())
        mark(false()) -> active(false())
        fact(mark(X)) -> fact(X)
        fact(active(X)) -> fact(X)
        if(mark(X1),X2,X3) -> if(X1,X2,X3)
        if(X1,mark(X2),X3) -> if(X1,X2,X3)
        if(X1,X2,mark(X3)) -> if(X1,X2,X3)
        if(active(X1),X2,X3) -> if(X1,X2,X3)
        if(X1,active(X2),X3) -> if(X1,X2,X3)
        if(X1,X2,active(X3)) -> if(X1,X2,X3)
        zero(mark(X)) -> zero(X)
        zero(active(X)) -> zero(X)
        s(mark(X)) -> s(X)
        s(active(X)) -> s(X)
        prod(mark(X1),X2) -> prod(X1,X2)
        prod(X1,mark(X2)) -> prod(X1,X2)
        prod(active(X1),X2) -> prod(X1,X2)
        prod(X1,active(X2)) -> prod(X1,X2)
        p(mark(X)) -> p(X)
        p(active(X)) -> p(X)
        add(mark(X1),X2) -> add(X1,X2)
        add(X1,mark(X2)) -> add(X1,X2)
        add(active(X1),X2) -> add(X1,X2)
        add(X1,active(X2)) -> add(X1,X2)
      Qed
    
    DPs:
     fact#(mark(X)) -> fact#(X)
     fact#(active(X)) -> fact#(X)
    TRS:
     active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X)))))
     active(add(0(),X)) -> mark(X)
     active(add(s(X),Y)) -> mark(s(add(X,Y)))
     active(prod(0(),X)) -> mark(0())
     active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y)))
     active(if(true(),X,Y)) -> mark(X)
     active(if(false(),X,Y)) -> mark(Y)
     active(zero(0())) -> mark(true())
     active(zero(s(X))) -> mark(false())
     active(p(s(X))) -> mark(X)
     mark(fact(X)) -> active(fact(mark(X)))
     mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
     mark(zero(X)) -> active(zero(mark(X)))
     mark(s(X)) -> active(s(mark(X)))
     mark(0()) -> active(0())
     mark(prod(X1,X2)) -> active(prod(mark(X1),mark(X2)))
     mark(p(X)) -> active(p(mark(X)))
     mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
     mark(true()) -> active(true())
     mark(false()) -> active(false())
     fact(mark(X)) -> fact(X)
     fact(active(X)) -> fact(X)
     if(mark(X1),X2,X3) -> if(X1,X2,X3)
     if(X1,mark(X2),X3) -> if(X1,X2,X3)
     if(X1,X2,mark(X3)) -> if(X1,X2,X3)
     if(active(X1),X2,X3) -> if(X1,X2,X3)
     if(X1,active(X2),X3) -> if(X1,X2,X3)
     if(X1,X2,active(X3)) -> if(X1,X2,X3)
     zero(mark(X)) -> zero(X)
     zero(active(X)) -> zero(X)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     prod(mark(X1),X2) -> prod(X1,X2)
     prod(X1,mark(X2)) -> prod(X1,X2)
     prod(active(X1),X2) -> prod(X1,X2)
     prod(X1,active(X2)) -> prod(X1,X2)
     p(mark(X)) -> p(X)
     p(active(X)) -> p(X)
     add(mark(X1),X2) -> add(X1,X2)
     add(X1,mark(X2)) -> add(X1,X2)
     add(active(X1),X2) -> add(X1,X2)
     add(X1,active(X2)) -> add(X1,X2)
    Subterm Criterion Processor:
     simple projection:
      pi(fact#) = 0
     problem:
      DPs:
       
      TRS:
       active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X)))))
       active(add(0(),X)) -> mark(X)
       active(add(s(X),Y)) -> mark(s(add(X,Y)))
       active(prod(0(),X)) -> mark(0())
       active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y)))
       active(if(true(),X,Y)) -> mark(X)
       active(if(false(),X,Y)) -> mark(Y)
       active(zero(0())) -> mark(true())
       active(zero(s(X))) -> mark(false())
       active(p(s(X))) -> mark(X)
       mark(fact(X)) -> active(fact(mark(X)))
       mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
       mark(zero(X)) -> active(zero(mark(X)))
       mark(s(X)) -> active(s(mark(X)))
       mark(0()) -> active(0())
       mark(prod(X1,X2)) -> active(prod(mark(X1),mark(X2)))
       mark(p(X)) -> active(p(mark(X)))
       mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
       mark(true()) -> active(true())
       mark(false()) -> active(false())
       fact(mark(X)) -> fact(X)
       fact(active(X)) -> fact(X)
       if(mark(X1),X2,X3) -> if(X1,X2,X3)
       if(X1,mark(X2),X3) -> if(X1,X2,X3)
       if(X1,X2,mark(X3)) -> if(X1,X2,X3)
       if(active(X1),X2,X3) -> if(X1,X2,X3)
       if(X1,active(X2),X3) -> if(X1,X2,X3)
       if(X1,X2,active(X3)) -> if(X1,X2,X3)
       zero(mark(X)) -> zero(X)
       zero(active(X)) -> zero(X)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(X)
       prod(mark(X1),X2) -> prod(X1,X2)
       prod(X1,mark(X2)) -> prod(X1,X2)
       prod(active(X1),X2) -> prod(X1,X2)
       prod(X1,active(X2)) -> prod(X1,X2)
       p(mark(X)) -> p(X)
       p(active(X)) -> p(X)
       add(mark(X1),X2) -> add(X1,X2)
       add(X1,mark(X2)) -> add(X1,X2)
       add(active(X1),X2) -> add(X1,X2)
       add(X1,active(X2)) -> add(X1,X2)
     Qed
    
    DPs:
     p#(mark(X)) -> p#(X)
     p#(active(X)) -> p#(X)
    TRS:
     active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X)))))
     active(add(0(),X)) -> mark(X)
     active(add(s(X),Y)) -> mark(s(add(X,Y)))
     active(prod(0(),X)) -> mark(0())
     active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y)))
     active(if(true(),X,Y)) -> mark(X)
     active(if(false(),X,Y)) -> mark(Y)
     active(zero(0())) -> mark(true())
     active(zero(s(X))) -> mark(false())
     active(p(s(X))) -> mark(X)
     mark(fact(X)) -> active(fact(mark(X)))
     mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
     mark(zero(X)) -> active(zero(mark(X)))
     mark(s(X)) -> active(s(mark(X)))
     mark(0()) -> active(0())
     mark(prod(X1,X2)) -> active(prod(mark(X1),mark(X2)))
     mark(p(X)) -> active(p(mark(X)))
     mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
     mark(true()) -> active(true())
     mark(false()) -> active(false())
     fact(mark(X)) -> fact(X)
     fact(active(X)) -> fact(X)
     if(mark(X1),X2,X3) -> if(X1,X2,X3)
     if(X1,mark(X2),X3) -> if(X1,X2,X3)
     if(X1,X2,mark(X3)) -> if(X1,X2,X3)
     if(active(X1),X2,X3) -> if(X1,X2,X3)
     if(X1,active(X2),X3) -> if(X1,X2,X3)
     if(X1,X2,active(X3)) -> if(X1,X2,X3)
     zero(mark(X)) -> zero(X)
     zero(active(X)) -> zero(X)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     prod(mark(X1),X2) -> prod(X1,X2)
     prod(X1,mark(X2)) -> prod(X1,X2)
     prod(active(X1),X2) -> prod(X1,X2)
     prod(X1,active(X2)) -> prod(X1,X2)
     p(mark(X)) -> p(X)
     p(active(X)) -> p(X)
     add(mark(X1),X2) -> add(X1,X2)
     add(X1,mark(X2)) -> add(X1,X2)
     add(active(X1),X2) -> add(X1,X2)
     add(X1,active(X2)) -> add(X1,X2)
    Subterm Criterion Processor:
     simple projection:
      pi(p#) = 0
     problem:
      DPs:
       
      TRS:
       active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X)))))
       active(add(0(),X)) -> mark(X)
       active(add(s(X),Y)) -> mark(s(add(X,Y)))
       active(prod(0(),X)) -> mark(0())
       active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y)))
       active(if(true(),X,Y)) -> mark(X)
       active(if(false(),X,Y)) -> mark(Y)
       active(zero(0())) -> mark(true())
       active(zero(s(X))) -> mark(false())
       active(p(s(X))) -> mark(X)
       mark(fact(X)) -> active(fact(mark(X)))
       mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
       mark(zero(X)) -> active(zero(mark(X)))
       mark(s(X)) -> active(s(mark(X)))
       mark(0()) -> active(0())
       mark(prod(X1,X2)) -> active(prod(mark(X1),mark(X2)))
       mark(p(X)) -> active(p(mark(X)))
       mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
       mark(true()) -> active(true())
       mark(false()) -> active(false())
       fact(mark(X)) -> fact(X)
       fact(active(X)) -> fact(X)
       if(mark(X1),X2,X3) -> if(X1,X2,X3)
       if(X1,mark(X2),X3) -> if(X1,X2,X3)
       if(X1,X2,mark(X3)) -> if(X1,X2,X3)
       if(active(X1),X2,X3) -> if(X1,X2,X3)
       if(X1,active(X2),X3) -> if(X1,X2,X3)
       if(X1,X2,active(X3)) -> if(X1,X2,X3)
       zero(mark(X)) -> zero(X)
       zero(active(X)) -> zero(X)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(X)
       prod(mark(X1),X2) -> prod(X1,X2)
       prod(X1,mark(X2)) -> prod(X1,X2)
       prod(active(X1),X2) -> prod(X1,X2)
       prod(X1,active(X2)) -> prod(X1,X2)
       p(mark(X)) -> p(X)
       p(active(X)) -> p(X)
       add(mark(X1),X2) -> add(X1,X2)
       add(X1,mark(X2)) -> add(X1,X2)
       add(active(X1),X2) -> add(X1,X2)
       add(X1,active(X2)) -> add(X1,X2)
     Qed
    
    DPs:
     add#(mark(X1),X2) -> add#(X1,X2)
     add#(X1,mark(X2)) -> add#(X1,X2)
     add#(active(X1),X2) -> add#(X1,X2)
     add#(X1,active(X2)) -> add#(X1,X2)
    TRS:
     active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X)))))
     active(add(0(),X)) -> mark(X)
     active(add(s(X),Y)) -> mark(s(add(X,Y)))
     active(prod(0(),X)) -> mark(0())
     active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y)))
     active(if(true(),X,Y)) -> mark(X)
     active(if(false(),X,Y)) -> mark(Y)
     active(zero(0())) -> mark(true())
     active(zero(s(X))) -> mark(false())
     active(p(s(X))) -> mark(X)
     mark(fact(X)) -> active(fact(mark(X)))
     mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
     mark(zero(X)) -> active(zero(mark(X)))
     mark(s(X)) -> active(s(mark(X)))
     mark(0()) -> active(0())
     mark(prod(X1,X2)) -> active(prod(mark(X1),mark(X2)))
     mark(p(X)) -> active(p(mark(X)))
     mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
     mark(true()) -> active(true())
     mark(false()) -> active(false())
     fact(mark(X)) -> fact(X)
     fact(active(X)) -> fact(X)
     if(mark(X1),X2,X3) -> if(X1,X2,X3)
     if(X1,mark(X2),X3) -> if(X1,X2,X3)
     if(X1,X2,mark(X3)) -> if(X1,X2,X3)
     if(active(X1),X2,X3) -> if(X1,X2,X3)
     if(X1,active(X2),X3) -> if(X1,X2,X3)
     if(X1,X2,active(X3)) -> if(X1,X2,X3)
     zero(mark(X)) -> zero(X)
     zero(active(X)) -> zero(X)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     prod(mark(X1),X2) -> prod(X1,X2)
     prod(X1,mark(X2)) -> prod(X1,X2)
     prod(active(X1),X2) -> prod(X1,X2)
     prod(X1,active(X2)) -> prod(X1,X2)
     p(mark(X)) -> p(X)
     p(active(X)) -> p(X)
     add(mark(X1),X2) -> add(X1,X2)
     add(X1,mark(X2)) -> add(X1,X2)
     add(active(X1),X2) -> add(X1,X2)
     add(X1,active(X2)) -> add(X1,X2)
    Subterm Criterion Processor:
     simple projection:
      pi(add#) = 1
     problem:
      DPs:
       add#(mark(X1),X2) -> add#(X1,X2)
       add#(active(X1),X2) -> add#(X1,X2)
      TRS:
       active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X)))))
       active(add(0(),X)) -> mark(X)
       active(add(s(X),Y)) -> mark(s(add(X,Y)))
       active(prod(0(),X)) -> mark(0())
       active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y)))
       active(if(true(),X,Y)) -> mark(X)
       active(if(false(),X,Y)) -> mark(Y)
       active(zero(0())) -> mark(true())
       active(zero(s(X))) -> mark(false())
       active(p(s(X))) -> mark(X)
       mark(fact(X)) -> active(fact(mark(X)))
       mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
       mark(zero(X)) -> active(zero(mark(X)))
       mark(s(X)) -> active(s(mark(X)))
       mark(0()) -> active(0())
       mark(prod(X1,X2)) -> active(prod(mark(X1),mark(X2)))
       mark(p(X)) -> active(p(mark(X)))
       mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
       mark(true()) -> active(true())
       mark(false()) -> active(false())
       fact(mark(X)) -> fact(X)
       fact(active(X)) -> fact(X)
       if(mark(X1),X2,X3) -> if(X1,X2,X3)
       if(X1,mark(X2),X3) -> if(X1,X2,X3)
       if(X1,X2,mark(X3)) -> if(X1,X2,X3)
       if(active(X1),X2,X3) -> if(X1,X2,X3)
       if(X1,active(X2),X3) -> if(X1,X2,X3)
       if(X1,X2,active(X3)) -> if(X1,X2,X3)
       zero(mark(X)) -> zero(X)
       zero(active(X)) -> zero(X)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(X)
       prod(mark(X1),X2) -> prod(X1,X2)
       prod(X1,mark(X2)) -> prod(X1,X2)
       prod(active(X1),X2) -> prod(X1,X2)
       prod(X1,active(X2)) -> prod(X1,X2)
       p(mark(X)) -> p(X)
       p(active(X)) -> p(X)
       add(mark(X1),X2) -> add(X1,X2)
       add(X1,mark(X2)) -> add(X1,X2)
       add(active(X1),X2) -> add(X1,X2)
       add(X1,active(X2)) -> add(X1,X2)
     Subterm Criterion Processor:
      simple projection:
       pi(add#) = 0
      problem:
       DPs:
        
       TRS:
        active(fact(X)) -> mark(if(zero(X),s(0()),prod(X,fact(p(X)))))
        active(add(0(),X)) -> mark(X)
        active(add(s(X),Y)) -> mark(s(add(X,Y)))
        active(prod(0(),X)) -> mark(0())
        active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y)))
        active(if(true(),X,Y)) -> mark(X)
        active(if(false(),X,Y)) -> mark(Y)
        active(zero(0())) -> mark(true())
        active(zero(s(X))) -> mark(false())
        active(p(s(X))) -> mark(X)
        mark(fact(X)) -> active(fact(mark(X)))
        mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
        mark(zero(X)) -> active(zero(mark(X)))
        mark(s(X)) -> active(s(mark(X)))
        mark(0()) -> active(0())
        mark(prod(X1,X2)) -> active(prod(mark(X1),mark(X2)))
        mark(p(X)) -> active(p(mark(X)))
        mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
        mark(true()) -> active(true())
        mark(false()) -> active(false())
        fact(mark(X)) -> fact(X)
        fact(active(X)) -> fact(X)
        if(mark(X1),X2,X3) -> if(X1,X2,X3)
        if(X1,mark(X2),X3) -> if(X1,X2,X3)
        if(X1,X2,mark(X3)) -> if(X1,X2,X3)
        if(active(X1),X2,X3) -> if(X1,X2,X3)
        if(X1,active(X2),X3) -> if(X1,X2,X3)
        if(X1,X2,active(X3)) -> if(X1,X2,X3)
        zero(mark(X)) -> zero(X)
        zero(active(X)) -> zero(X)
        s(mark(X)) -> s(X)
        s(active(X)) -> s(X)
        prod(mark(X1),X2) -> prod(X1,X2)
        prod(X1,mark(X2)) -> prod(X1,X2)
        prod(active(X1),X2) -> prod(X1,X2)
        prod(X1,active(X2)) -> prod(X1,X2)
        p(mark(X)) -> p(X)
        p(active(X)) -> p(X)
        add(mark(X1),X2) -> add(X1,X2)
        add(X1,mark(X2)) -> add(X1,X2)
        add(active(X1),X2) -> add(X1,X2)
        add(X1,active(X2)) -> add(X1,X2)
      Qed