MAYBE
Time: 4.843782
TRS:
 {              a__p X -> p X,
              a__p 0() -> 0(),
              a__p s X -> mark X,
              mark 0() -> 0(),
              mark s X -> s mark X,
           mark true() -> true(),
          mark false() -> false(),
     mark diff(X1, X2) -> a__diff(mark X1, mark X2),
              mark p X -> a__p mark X,
      mark leq(X1, X2) -> a__leq(mark X1, mark X2),
   mark if(X1, X2, X3) -> a__if(mark X1, X2, X3),
        a__leq(X1, X2) -> leq(X1, X2),
        a__leq(0(), Y) -> true(),
      a__leq(s X, 0()) -> false(),
      a__leq(s X, s Y) -> a__leq(mark X, mark Y),
     a__if(X1, X2, X3) -> if(X1, X2, X3),
   a__if(true(), X, Y) -> mark X,
  a__if(false(), X, Y) -> mark Y,
         a__diff(X, Y) -> a__if(a__leq(mark X, mark Y), 0(), s diff(p X, Y)),
       a__diff(X1, X2) -> diff(X1, X2)}
 DP:
  DP:
   {            a__p# s X -> mark# X,
                mark# s X -> mark# X,
       mark# diff(X1, X2) -> mark# X1,
       mark# diff(X1, X2) -> mark# X2,
       mark# diff(X1, X2) -> a__diff#(mark X1, mark X2),
                mark# p X -> a__p# mark X,
                mark# p X -> mark# X,
        mark# leq(X1, X2) -> mark# X1,
        mark# leq(X1, X2) -> mark# X2,
        mark# leq(X1, X2) -> a__leq#(mark X1, mark X2),
     mark# if(X1, X2, X3) -> mark# X1,
     mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3),
        a__leq#(s X, s Y) -> mark# X,
        a__leq#(s X, s Y) -> mark# Y,
        a__leq#(s X, s Y) -> a__leq#(mark X, mark Y),
     a__if#(true(), X, Y) -> mark# X,
    a__if#(false(), X, Y) -> mark# Y,
           a__diff#(X, Y) -> mark# X,
           a__diff#(X, Y) -> mark# Y,
           a__diff#(X, Y) -> a__leq#(mark X, mark Y),
           a__diff#(X, Y) -> a__if#(a__leq(mark X, mark Y), 0(), s diff(p X, Y))}
  TRS:
  {              a__p X -> p X,
               a__p 0() -> 0(),
               a__p s X -> mark X,
               mark 0() -> 0(),
               mark s X -> s mark X,
            mark true() -> true(),
           mark false() -> false(),
      mark diff(X1, X2) -> a__diff(mark X1, mark X2),
               mark p X -> a__p mark X,
       mark leq(X1, X2) -> a__leq(mark X1, mark X2),
    mark if(X1, X2, X3) -> a__if(mark X1, X2, X3),
         a__leq(X1, X2) -> leq(X1, X2),
         a__leq(0(), Y) -> true(),
       a__leq(s X, 0()) -> false(),
       a__leq(s X, s Y) -> a__leq(mark X, mark Y),
      a__if(X1, X2, X3) -> if(X1, X2, X3),
    a__if(true(), X, Y) -> mark X,
   a__if(false(), X, Y) -> mark Y,
          a__diff(X, Y) -> a__if(a__leq(mark X, mark Y), 0(), s diff(p X, Y)),
        a__diff(X1, X2) -> diff(X1, X2)}
  EDG:
   {
    (mark# p X -> a__p# mark X, a__p# s X -> mark# X)
    (mark# leq(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
    (mark# leq(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> mark# X1)
    (mark# leq(X1, X2) -> mark# X2, mark# leq(X1, X2) -> a__leq#(mark X1, mark X2))
    (mark# leq(X1, X2) -> mark# X2, mark# leq(X1, X2) -> mark# X2)
    (mark# leq(X1, X2) -> mark# X2, mark# leq(X1, X2) -> mark# X1)
    (mark# leq(X1, X2) -> mark# X2, mark# p X -> mark# X)
    (mark# leq(X1, X2) -> mark# X2, mark# p X -> a__p# mark X)
    (mark# leq(X1, X2) -> mark# X2, mark# diff(X1, X2) -> a__diff#(mark X1, mark X2))
    (mark# leq(X1, X2) -> mark# X2, mark# diff(X1, X2) -> mark# X2)
    (mark# leq(X1, X2) -> mark# X2, mark# diff(X1, X2) -> mark# X1)
    (mark# leq(X1, X2) -> mark# X2, mark# s X -> mark# X)
    (mark# diff(X1, X2) -> a__diff#(mark X1, mark X2), a__diff#(X, Y) -> a__if#(a__leq(mark X, mark Y), 0(), s diff(p X, Y)))
    (mark# diff(X1, X2) -> a__diff#(mark X1, mark X2), a__diff#(X, Y) -> a__leq#(mark X, mark Y))
    (mark# diff(X1, X2) -> a__diff#(mark X1, mark X2), a__diff#(X, Y) -> mark# Y)
    (mark# diff(X1, X2) -> a__diff#(mark X1, mark X2), a__diff#(X, Y) -> mark# X)
    (mark# leq(X1, X2) -> a__leq#(mark X1, mark X2), a__leq#(s X, s Y) -> a__leq#(mark X, mark Y))
    (mark# leq(X1, X2) -> a__leq#(mark X1, mark X2), a__leq#(s X, s Y) -> mark# Y)
    (mark# leq(X1, X2) -> a__leq#(mark X1, mark X2), a__leq#(s X, s Y) -> mark# X)
    (mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3), a__if#(false(), X, Y) -> mark# Y)
    (mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3), a__if#(true(), X, Y) -> mark# X)
    (a__diff#(X, Y) -> a__leq#(mark X, mark Y), a__leq#(s X, s Y) -> a__leq#(mark X, mark Y))
    (a__diff#(X, Y) -> a__leq#(mark X, mark Y), a__leq#(s X, s Y) -> mark# Y)
    (a__diff#(X, Y) -> a__leq#(mark X, mark Y), a__leq#(s X, s Y) -> mark# X)
    (a__if#(false(), X, Y) -> mark# Y, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
    (a__if#(false(), X, Y) -> mark# Y, mark# if(X1, X2, X3) -> mark# X1)
    (a__if#(false(), X, Y) -> mark# Y, mark# leq(X1, X2) -> a__leq#(mark X1, mark X2))
    (a__if#(false(), X, Y) -> mark# Y, mark# leq(X1, X2) -> mark# X2)
    (a__if#(false(), X, Y) -> mark# Y, mark# leq(X1, X2) -> mark# X1)
    (a__if#(false(), X, Y) -> mark# Y, mark# p X -> mark# X)
    (a__if#(false(), X, Y) -> mark# Y, mark# p X -> a__p# mark X)
    (a__if#(false(), X, Y) -> mark# Y, mark# diff(X1, X2) -> a__diff#(mark X1, mark X2))
    (a__if#(false(), X, Y) -> mark# Y, mark# diff(X1, X2) -> mark# X2)
    (a__if#(false(), X, Y) -> mark# Y, mark# diff(X1, X2) -> mark# X1)
    (a__if#(false(), X, Y) -> mark# Y, mark# s X -> mark# X)
    (a__p# s X -> mark# X, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
    (a__p# s X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
    (a__p# s X -> mark# X, mark# leq(X1, X2) -> a__leq#(mark X1, mark X2))
    (a__p# s X -> mark# X, mark# leq(X1, X2) -> mark# X2)
    (a__p# s X -> mark# X, mark# leq(X1, X2) -> mark# X1)
    (a__p# s X -> mark# X, mark# p X -> mark# X)
    (a__p# s X -> mark# X, mark# p X -> a__p# mark X)
    (a__p# s X -> mark# X, mark# diff(X1, X2) -> a__diff#(mark X1, mark X2))
    (a__p# s X -> mark# X, mark# diff(X1, X2) -> mark# X2)
    (a__p# s X -> mark# X, mark# diff(X1, X2) -> mark# X1)
    (a__p# s X -> mark# X, mark# s X -> mark# X)
    (mark# p X -> mark# X, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
    (mark# p X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
    (mark# p X -> mark# X, mark# leq(X1, X2) -> a__leq#(mark X1, mark X2))
    (mark# p X -> mark# X, mark# leq(X1, X2) -> mark# X2)
    (mark# p X -> mark# X, mark# leq(X1, X2) -> mark# X1)
    (mark# p X -> mark# X, mark# p X -> mark# X)
    (mark# p X -> mark# X, mark# p X -> a__p# mark X)
    (mark# p X -> mark# X, mark# diff(X1, X2) -> a__diff#(mark X1, mark X2))
    (mark# p X -> mark# X, mark# diff(X1, X2) -> mark# X2)
    (mark# p X -> mark# X, mark# diff(X1, X2) -> mark# X1)
    (mark# p X -> mark# X, mark# s X -> mark# X)
    (a__if#(true(), X, Y) -> mark# X, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
    (a__if#(true(), X, Y) -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
    (a__if#(true(), X, Y) -> mark# X, mark# leq(X1, X2) -> a__leq#(mark X1, mark X2))
    (a__if#(true(), X, Y) -> mark# X, mark# leq(X1, X2) -> mark# X2)
    (a__if#(true(), X, Y) -> mark# X, mark# leq(X1, X2) -> mark# X1)
    (a__if#(true(), X, Y) -> mark# X, mark# p X -> mark# X)
    (a__if#(true(), X, Y) -> mark# X, mark# p X -> a__p# mark X)
    (a__if#(true(), X, Y) -> mark# X, mark# diff(X1, X2) -> a__diff#(mark X1, mark X2))
    (a__if#(true(), X, Y) -> mark# X, mark# diff(X1, X2) -> mark# X2)
    (a__if#(true(), X, Y) -> mark# X, mark# diff(X1, X2) -> mark# X1)
    (a__if#(true(), X, Y) -> mark# X, mark# s X -> mark# X)
    (a__diff#(X, Y) -> mark# X, mark# s X -> mark# X)
    (a__diff#(X, Y) -> mark# X, mark# diff(X1, X2) -> mark# X1)
    (a__diff#(X, Y) -> mark# X, mark# diff(X1, X2) -> mark# X2)
    (a__diff#(X, Y) -> mark# X, mark# diff(X1, X2) -> a__diff#(mark X1, mark X2))
    (a__diff#(X, Y) -> mark# X, mark# p X -> a__p# mark X)
    (a__diff#(X, Y) -> mark# X, mark# p X -> mark# X)
    (a__diff#(X, Y) -> mark# X, mark# leq(X1, X2) -> mark# X1)
    (a__diff#(X, Y) -> mark# X, mark# leq(X1, X2) -> mark# X2)
    (a__diff#(X, Y) -> mark# X, mark# leq(X1, X2) -> a__leq#(mark X1, mark X2))
    (a__diff#(X, Y) -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
    (a__diff#(X, Y) -> mark# X, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
    (a__leq#(s X, s Y) -> mark# X, mark# s X -> mark# X)
    (a__leq#(s X, s Y) -> mark# X, mark# diff(X1, X2) -> mark# X1)
    (a__leq#(s X, s Y) -> mark# X, mark# diff(X1, X2) -> mark# X2)
    (a__leq#(s X, s Y) -> mark# X, mark# diff(X1, X2) -> a__diff#(mark X1, mark X2))
    (a__leq#(s X, s Y) -> mark# X, mark# p X -> a__p# mark X)
    (a__leq#(s X, s Y) -> mark# X, mark# p X -> mark# X)
    (a__leq#(s X, s Y) -> mark# X, mark# leq(X1, X2) -> mark# X1)
    (a__leq#(s X, s Y) -> mark# X, mark# leq(X1, X2) -> mark# X2)
    (a__leq#(s X, s Y) -> mark# X, mark# leq(X1, X2) -> a__leq#(mark X1, mark X2))
    (a__leq#(s X, s Y) -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
    (a__leq#(s X, s Y) -> mark# X, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
    (mark# s X -> mark# X, mark# s X -> mark# X)
    (mark# s X -> mark# X, mark# diff(X1, X2) -> mark# X1)
    (mark# s X -> mark# X, mark# diff(X1, X2) -> mark# X2)
    (mark# s X -> mark# X, mark# diff(X1, X2) -> a__diff#(mark X1, mark X2))
    (mark# s X -> mark# X, mark# p X -> a__p# mark X)
    (mark# s X -> mark# X, mark# p X -> mark# X)
    (mark# s X -> mark# X, mark# leq(X1, X2) -> mark# X1)
    (mark# s X -> mark# X, mark# leq(X1, X2) -> mark# X2)
    (mark# s X -> mark# X, mark# leq(X1, X2) -> a__leq#(mark X1, mark X2))
    (mark# s X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
    (mark# s X -> mark# X, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
    (a__diff#(X, Y) -> mark# Y, mark# s X -> mark# X)
    (a__diff#(X, Y) -> mark# Y, mark# diff(X1, X2) -> mark# X1)
    (a__diff#(X, Y) -> mark# Y, mark# diff(X1, X2) -> mark# X2)
    (a__diff#(X, Y) -> mark# Y, mark# diff(X1, X2) -> a__diff#(mark X1, mark X2))
    (a__diff#(X, Y) -> mark# Y, mark# p X -> a__p# mark X)
    (a__diff#(X, Y) -> mark# Y, mark# p X -> mark# X)
    (a__diff#(X, Y) -> mark# Y, mark# leq(X1, X2) -> mark# X1)
    (a__diff#(X, Y) -> mark# Y, mark# leq(X1, X2) -> mark# X2)
    (a__diff#(X, Y) -> mark# Y, mark# leq(X1, X2) -> a__leq#(mark X1, mark X2))
    (a__diff#(X, Y) -> mark# Y, mark# if(X1, X2, X3) -> mark# X1)
    (a__diff#(X, Y) -> mark# Y, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
    (a__leq#(s X, s Y) -> mark# Y, mark# s X -> mark# X)
    (a__leq#(s X, s Y) -> mark# Y, mark# diff(X1, X2) -> mark# X1)
    (a__leq#(s X, s Y) -> mark# Y, mark# diff(X1, X2) -> mark# X2)
    (a__leq#(s X, s Y) -> mark# Y, mark# diff(X1, X2) -> a__diff#(mark X1, mark X2))
    (a__leq#(s X, s Y) -> mark# Y, mark# p X -> a__p# mark X)
    (a__leq#(s X, s Y) -> mark# Y, mark# p X -> mark# X)
    (a__leq#(s X, s Y) -> mark# Y, mark# leq(X1, X2) -> mark# X1)
    (a__leq#(s X, s Y) -> mark# Y, mark# leq(X1, X2) -> mark# X2)
    (a__leq#(s X, s Y) -> mark# Y, mark# leq(X1, X2) -> a__leq#(mark X1, mark X2))
    (a__leq#(s X, s Y) -> mark# Y, mark# if(X1, X2, X3) -> mark# X1)
    (a__leq#(s X, s Y) -> mark# Y, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
    (a__leq#(s X, s Y) -> a__leq#(mark X, mark Y), a__leq#(s X, s Y) -> mark# X)
    (a__leq#(s X, s Y) -> a__leq#(mark X, mark Y), a__leq#(s X, s Y) -> mark# Y)
    (a__leq#(s X, s Y) -> a__leq#(mark X, mark Y), a__leq#(s X, s Y) -> a__leq#(mark X, mark Y))
    (mark# if(X1, X2, X3) -> mark# X1, mark# s X -> mark# X)
    (mark# if(X1, X2, X3) -> mark# X1, mark# diff(X1, X2) -> mark# X1)
    (mark# if(X1, X2, X3) -> mark# X1, mark# diff(X1, X2) -> mark# X2)
    (mark# if(X1, X2, X3) -> mark# X1, mark# diff(X1, X2) -> a__diff#(mark X1, mark X2))
    (mark# if(X1, X2, X3) -> mark# X1, mark# p X -> a__p# mark X)
    (mark# if(X1, X2, X3) -> mark# X1, mark# p X -> mark# X)
    (mark# if(X1, X2, X3) -> mark# X1, mark# leq(X1, X2) -> mark# X1)
    (mark# if(X1, X2, X3) -> mark# X1, mark# leq(X1, X2) -> mark# X2)
    (mark# if(X1, X2, X3) -> mark# X1, mark# leq(X1, X2) -> a__leq#(mark X1, mark X2))
    (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) -> a__if#(mark X1, X2, X3))
    (mark# leq(X1, X2) -> mark# X1, mark# s X -> mark# X)
    (mark# leq(X1, X2) -> mark# X1, mark# diff(X1, X2) -> mark# X1)
    (mark# leq(X1, X2) -> mark# X1, mark# diff(X1, X2) -> mark# X2)
    (mark# leq(X1, X2) -> mark# X1, mark# diff(X1, X2) -> a__diff#(mark X1, mark X2))
    (mark# leq(X1, X2) -> mark# X1, mark# p X -> a__p# mark X)
    (mark# leq(X1, X2) -> mark# X1, mark# p X -> mark# X)
    (mark# leq(X1, X2) -> mark# X1, mark# leq(X1, X2) -> mark# X1)
    (mark# leq(X1, X2) -> mark# X1, mark# leq(X1, X2) -> mark# X2)
    (mark# leq(X1, X2) -> mark# X1, mark# leq(X1, X2) -> a__leq#(mark X1, mark X2))
    (mark# leq(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1)
    (mark# leq(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
    (mark# diff(X1, X2) -> mark# X1, mark# s X -> mark# X)
    (mark# diff(X1, X2) -> mark# X1, mark# diff(X1, X2) -> mark# X1)
    (mark# diff(X1, X2) -> mark# X1, mark# diff(X1, X2) -> mark# X2)
    (mark# diff(X1, X2) -> mark# X1, mark# diff(X1, X2) -> a__diff#(mark X1, mark X2))
    (mark# diff(X1, X2) -> mark# X1, mark# p X -> a__p# mark X)
    (mark# diff(X1, X2) -> mark# X1, mark# p X -> mark# X)
    (mark# diff(X1, X2) -> mark# X1, mark# leq(X1, X2) -> mark# X1)
    (mark# diff(X1, X2) -> mark# X1, mark# leq(X1, X2) -> mark# X2)
    (mark# diff(X1, X2) -> mark# X1, mark# leq(X1, X2) -> a__leq#(mark X1, mark X2))
    (mark# diff(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1)
    (mark# diff(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
    (mark# diff(X1, X2) -> mark# X2, mark# s X -> mark# X)
    (mark# diff(X1, X2) -> mark# X2, mark# diff(X1, X2) -> mark# X1)
    (mark# diff(X1, X2) -> mark# X2, mark# diff(X1, X2) -> mark# X2)
    (mark# diff(X1, X2) -> mark# X2, mark# diff(X1, X2) -> a__diff#(mark X1, mark X2))
    (mark# diff(X1, X2) -> mark# X2, mark# p X -> a__p# mark X)
    (mark# diff(X1, X2) -> mark# X2, mark# p X -> mark# X)
    (mark# diff(X1, X2) -> mark# X2, mark# leq(X1, X2) -> mark# X1)
    (mark# diff(X1, X2) -> mark# X2, mark# leq(X1, X2) -> mark# X2)
    (mark# diff(X1, X2) -> mark# X2, mark# leq(X1, X2) -> a__leq#(mark X1, mark X2))
    (mark# diff(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> mark# X1)
    (mark# diff(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
    (a__diff#(X, Y) -> a__if#(a__leq(mark X, mark Y), 0(), s diff(p X, Y)), a__if#(true(), X, Y) -> mark# X)
    (a__diff#(X, Y) -> a__if#(a__leq(mark X, mark Y), 0(), s diff(p X, Y)), a__if#(false(), X, Y) -> mark# Y)
   }
   STATUS:
    arrows: 0.609977
    SCCS (1):
     Scc:
      {            a__p# s X -> mark# X,
                   mark# s X -> mark# X,
          mark# diff(X1, X2) -> mark# X1,
          mark# diff(X1, X2) -> mark# X2,
          mark# diff(X1, X2) -> a__diff#(mark X1, mark X2),
                   mark# p X -> a__p# mark X,
                   mark# p X -> mark# X,
           mark# leq(X1, X2) -> mark# X1,
           mark# leq(X1, X2) -> mark# X2,
           mark# leq(X1, X2) -> a__leq#(mark X1, mark X2),
        mark# if(X1, X2, X3) -> mark# X1,
        mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3),
           a__leq#(s X, s Y) -> mark# X,
           a__leq#(s X, s Y) -> mark# Y,
           a__leq#(s X, s Y) -> a__leq#(mark X, mark Y),
        a__if#(true(), X, Y) -> mark# X,
       a__if#(false(), X, Y) -> mark# Y,
              a__diff#(X, Y) -> mark# X,
              a__diff#(X, Y) -> mark# Y,
              a__diff#(X, Y) -> a__leq#(mark X, mark Y),
              a__diff#(X, Y) -> a__if#(a__leq(mark X, mark Y), 0(), s diff(p X, Y))}
     
     SCC (21):
      Strict:
       {            a__p# s X -> mark# X,
                    mark# s X -> mark# X,
           mark# diff(X1, X2) -> mark# X1,
           mark# diff(X1, X2) -> mark# X2,
           mark# diff(X1, X2) -> a__diff#(mark X1, mark X2),
                    mark# p X -> a__p# mark X,
                    mark# p X -> mark# X,
            mark# leq(X1, X2) -> mark# X1,
            mark# leq(X1, X2) -> mark# X2,
            mark# leq(X1, X2) -> a__leq#(mark X1, mark X2),
         mark# if(X1, X2, X3) -> mark# X1,
         mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3),
            a__leq#(s X, s Y) -> mark# X,
            a__leq#(s X, s Y) -> mark# Y,
            a__leq#(s X, s Y) -> a__leq#(mark X, mark Y),
         a__if#(true(), X, Y) -> mark# X,
        a__if#(false(), X, Y) -> mark# Y,
               a__diff#(X, Y) -> mark# X,
               a__diff#(X, Y) -> mark# Y,
               a__diff#(X, Y) -> a__leq#(mark X, mark Y),
               a__diff#(X, Y) -> a__if#(a__leq(mark X, mark Y), 0(), s diff(p X, Y))}
      Weak:
      {              a__p X -> p X,
                   a__p 0() -> 0(),
                   a__p s X -> mark X,
                   mark 0() -> 0(),
                   mark s X -> s mark X,
                mark true() -> true(),
               mark false() -> false(),
          mark diff(X1, X2) -> a__diff(mark X1, mark X2),
                   mark p X -> a__p mark X,
           mark leq(X1, X2) -> a__leq(mark X1, mark X2),
        mark if(X1, X2, X3) -> a__if(mark X1, X2, X3),
             a__leq(X1, X2) -> leq(X1, X2),
             a__leq(0(), Y) -> true(),
           a__leq(s X, 0()) -> false(),
           a__leq(s X, s Y) -> a__leq(mark X, mark Y),
          a__if(X1, X2, X3) -> if(X1, X2, X3),
        a__if(true(), X, Y) -> mark X,
       a__if(false(), X, Y) -> mark Y,
              a__diff(X, Y) -> a__if(a__leq(mark X, mark Y), 0(), s diff(p X, Y)),
            a__diff(X1, X2) -> diff(X1, X2)}
      Fail