MAYBE
Time: 0.008888
TRS:
 {                        p s x -> x,
                          p 0() -> 0(),
                   le(s x, s y) -> le(x, y),
                   le(s x, 0()) -> false(),
                     le(0(), y) -> true(),
   if(true(), b1, b2, b3, x, y) -> if2(b1, b2, b3, x, y),
  if(false(), b1, b2, b3, x, y) -> average(p x, s y),
                  average(x, y) -> if(le(x, 0()), le(y, 0()), le(y, s 0()), le(y, s s 0()), x, y),
      if2(true(), b2, b3, x, y) -> 0(),
     if2(false(), b2, b3, x, y) -> if3(b2, b3, x, y),
          if3(true(), b3, x, y) -> 0(),
         if3(false(), b3, x, y) -> if4(b3, x, y),
              if4(true(), x, y) -> s 0(),
             if4(false(), x, y) -> average(s x, p p y)}
 DP:
  DP:
   {                 le#(s x, s y) -> le#(x, y),
     if#(true(), b1, b2, b3, x, y) -> if2#(b1, b2, b3, x, y),
    if#(false(), b1, b2, b3, x, y) -> p# x,
    if#(false(), b1, b2, b3, x, y) -> average#(p x, s y),
                    average#(x, y) -> le#(x, 0()),
                    average#(x, y) -> le#(y, s s 0()),
                    average#(x, y) -> le#(y, s 0()),
                    average#(x, y) -> le#(y, 0()),
                    average#(x, y) -> if#(le(x, 0()), le(y, 0()), le(y, s 0()), le(y, s s 0()), x, y),
       if2#(false(), b2, b3, x, y) -> if3#(b2, b3, x, y),
           if3#(false(), b3, x, y) -> if4#(b3, x, y),
               if4#(false(), x, y) -> p# y,
               if4#(false(), x, y) -> p# p y,
               if4#(false(), x, y) -> average#(s x, p p y)}
  TRS:
  {                        p s x -> x,
                           p 0() -> 0(),
                    le(s x, s y) -> le(x, y),
                    le(s x, 0()) -> false(),
                      le(0(), y) -> true(),
    if(true(), b1, b2, b3, x, y) -> if2(b1, b2, b3, x, y),
   if(false(), b1, b2, b3, x, y) -> average(p x, s y),
                   average(x, y) -> if(le(x, 0()), le(y, 0()), le(y, s 0()), le(y, s s 0()), x, y),
       if2(true(), b2, b3, x, y) -> 0(),
      if2(false(), b2, b3, x, y) -> if3(b2, b3, x, y),
           if3(true(), b3, x, y) -> 0(),
          if3(false(), b3, x, y) -> if4(b3, x, y),
               if4(true(), x, y) -> s 0(),
              if4(false(), x, y) -> average(s x, p p y)}
  EDG:
   {(average#(x, y) -> le#(y, s 0()), le#(s x, s y) -> le#(x, y))
    (if#(true(), b1, b2, b3, x, y) -> if2#(b1, b2, b3, x, y), if2#(false(), b2, b3, x, y) -> if3#(b2, b3, x, y))
    (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
    (if#(false(), b1, b2, b3, x, y) -> average#(p x, s y), average#(x, y) -> if#(le(x, 0()), le(y, 0()), le(y, s 0()), le(y, s s 0()), x, y))
    (if#(false(), b1, b2, b3, x, y) -> average#(p x, s y), average#(x, y) -> le#(y, 0()))
    (if#(false(), b1, b2, b3, x, y) -> average#(p x, s y), average#(x, y) -> le#(y, s 0()))
    (if#(false(), b1, b2, b3, x, y) -> average#(p x, s y), average#(x, y) -> le#(y, s s 0()))
    (if#(false(), b1, b2, b3, x, y) -> average#(p x, s y), average#(x, y) -> le#(x, 0()))
    (if2#(false(), b2, b3, x, y) -> if3#(b2, b3, x, y), if3#(false(), b3, x, y) -> if4#(b3, x, y))
    (average#(x, y) -> if#(le(x, 0()), le(y, 0()), le(y, s 0()), le(y, s s 0()), x, y), if#(true(), b1, b2, b3, x, y) -> if2#(b1, b2, b3, x, y))
    (average#(x, y) -> if#(le(x, 0()), le(y, 0()), le(y, s 0()), le(y, s s 0()), x, y), if#(false(), b1, b2, b3, x, y) -> p# x)
    (average#(x, y) -> if#(le(x, 0()), le(y, 0()), le(y, s 0()), le(y, s s 0()), x, y), if#(false(), b1, b2, b3, x, y) -> average#(p x, s y))
    (if3#(false(), b3, x, y) -> if4#(b3, x, y), if4#(false(), x, y) -> p# y)
    (if3#(false(), b3, x, y) -> if4#(b3, x, y), if4#(false(), x, y) -> p# p y)
    (if3#(false(), b3, x, y) -> if4#(b3, x, y), if4#(false(), x, y) -> average#(s x, p p y))
    (if4#(false(), x, y) -> average#(s x, p p y), average#(x, y) -> le#(x, 0()))
    (if4#(false(), x, y) -> average#(s x, p p y), average#(x, y) -> le#(y, s s 0()))
    (if4#(false(), x, y) -> average#(s x, p p y), average#(x, y) -> le#(y, s 0()))
    (if4#(false(), x, y) -> average#(s x, p p y), average#(x, y) -> le#(y, 0()))
    (if4#(false(), x, y) -> average#(s x, p p y), average#(x, y) -> if#(le(x, 0()), le(y, 0()), le(y, s 0()), le(y, s s 0()), x, y))
    (average#(x, y) -> le#(y, s s 0()), le#(s x, s y) -> le#(x, y))}
   EDG:
    {(average#(x, y) -> le#(y, s 0()), le#(s x, s y) -> le#(x, y))
     (if#(true(), b1, b2, b3, x, y) -> if2#(b1, b2, b3, x, y), if2#(false(), b2, b3, x, y) -> if3#(b2, b3, x, y))
     (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
     (if#(false(), b1, b2, b3, x, y) -> average#(p x, s y), average#(x, y) -> if#(le(x, 0()), le(y, 0()), le(y, s 0()), le(y, s s 0()), x, y))
     (if#(false(), b1, b2, b3, x, y) -> average#(p x, s y), average#(x, y) -> le#(y, 0()))
     (if#(false(), b1, b2, b3, x, y) -> average#(p x, s y), average#(x, y) -> le#(y, s 0()))
     (if#(false(), b1, b2, b3, x, y) -> average#(p x, s y), average#(x, y) -> le#(y, s s 0()))
     (if#(false(), b1, b2, b3, x, y) -> average#(p x, s y), average#(x, y) -> le#(x, 0()))
     (if2#(false(), b2, b3, x, y) -> if3#(b2, b3, x, y), if3#(false(), b3, x, y) -> if4#(b3, x, y))
     (average#(x, y) -> if#(le(x, 0()), le(y, 0()), le(y, s 0()), le(y, s s 0()), x, y), if#(true(), b1, b2, b3, x, y) -> if2#(b1, b2, b3, x, y))
     (average#(x, y) -> if#(le(x, 0()), le(y, 0()), le(y, s 0()), le(y, s s 0()), x, y), if#(false(), b1, b2, b3, x, y) -> p# x)
     (average#(x, y) -> if#(le(x, 0()), le(y, 0()), le(y, s 0()), le(y, s s 0()), x, y), if#(false(), b1, b2, b3, x, y) -> average#(p x, s y))
     (if3#(false(), b3, x, y) -> if4#(b3, x, y), if4#(false(), x, y) -> p# y)
     (if3#(false(), b3, x, y) -> if4#(b3, x, y), if4#(false(), x, y) -> p# p y)
     (if3#(false(), b3, x, y) -> if4#(b3, x, y), if4#(false(), x, y) -> average#(s x, p p y))
     (if4#(false(), x, y) -> average#(s x, p p y), average#(x, y) -> le#(x, 0()))
     (if4#(false(), x, y) -> average#(s x, p p y), average#(x, y) -> le#(y, s s 0()))
     (if4#(false(), x, y) -> average#(s x, p p y), average#(x, y) -> le#(y, s 0()))
     (if4#(false(), x, y) -> average#(s x, p p y), average#(x, y) -> le#(y, 0()))
     (if4#(false(), x, y) -> average#(s x, p p y), average#(x, y) -> if#(le(x, 0()), le(y, 0()), le(y, s 0()), le(y, s s 0()), x, y))
     (average#(x, y) -> le#(y, s s 0()), le#(s x, s y) -> le#(x, y))}
    EDG:
     {(average#(x, y) -> le#(y, s 0()), le#(s x, s y) -> le#(x, y))
      (if#(true(), b1, b2, b3, x, y) -> if2#(b1, b2, b3, x, y), if2#(false(), b2, b3, x, y) -> if3#(b2, b3, x, y))
      (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
      (if#(false(), b1, b2, b3, x, y) -> average#(p x, s y), average#(x, y) -> if#(le(x, 0()), le(y, 0()), le(y, s 0()), le(y, s s 0()), x, y))
      (if#(false(), b1, b2, b3, x, y) -> average#(p x, s y), average#(x, y) -> le#(y, 0()))
      (if#(false(), b1, b2, b3, x, y) -> average#(p x, s y), average#(x, y) -> le#(y, s 0()))
      (if#(false(), b1, b2, b3, x, y) -> average#(p x, s y), average#(x, y) -> le#(y, s s 0()))
      (if#(false(), b1, b2, b3, x, y) -> average#(p x, s y), average#(x, y) -> le#(x, 0()))
      (if2#(false(), b2, b3, x, y) -> if3#(b2, b3, x, y), if3#(false(), b3, x, y) -> if4#(b3, x, y))
      (average#(x, y) -> if#(le(x, 0()), le(y, 0()), le(y, s 0()), le(y, s s 0()), x, y), if#(true(), b1, b2, b3, x, y) -> if2#(b1, b2, b3, x, y))
      (average#(x, y) -> if#(le(x, 0()), le(y, 0()), le(y, s 0()), le(y, s s 0()), x, y), if#(false(), b1, b2, b3, x, y) -> p# x)
      (average#(x, y) -> if#(le(x, 0()), le(y, 0()), le(y, s 0()), le(y, s s 0()), x, y), if#(false(), b1, b2, b3, x, y) -> average#(p x, s y))
      (if3#(false(), b3, x, y) -> if4#(b3, x, y), if4#(false(), x, y) -> p# y)
      (if3#(false(), b3, x, y) -> if4#(b3, x, y), if4#(false(), x, y) -> p# p y)
      (if3#(false(), b3, x, y) -> if4#(b3, x, y), if4#(false(), x, y) -> average#(s x, p p y))
      (if4#(false(), x, y) -> average#(s x, p p y), average#(x, y) -> le#(x, 0()))
      (if4#(false(), x, y) -> average#(s x, p p y), average#(x, y) -> le#(y, s s 0()))
      (if4#(false(), x, y) -> average#(s x, p p y), average#(x, y) -> le#(y, s 0()))
      (if4#(false(), x, y) -> average#(s x, p p y), average#(x, y) -> le#(y, 0()))
      (if4#(false(), x, y) -> average#(s x, p p y), average#(x, y) -> if#(le(x, 0()), le(y, 0()), le(y, s 0()), le(y, s s 0()), x, y))
      (average#(x, y) -> le#(y, s s 0()), le#(s x, s y) -> le#(x, y))}
     STATUS:
      arrows: 0.892857
      SCCS (2):
       Scc:
        { if#(true(), b1, b2, b3, x, y) -> if2#(b1, b2, b3, x, y),
         if#(false(), b1, b2, b3, x, y) -> average#(p x, s y),
                         average#(x, y) -> if#(le(x, 0()), le(y, 0()), le(y, s 0()), le(y, s s 0()), x, y),
            if2#(false(), b2, b3, x, y) -> if3#(b2, b3, x, y),
                if3#(false(), b3, x, y) -> if4#(b3, x, y),
                    if4#(false(), x, y) -> average#(s x, p p y)}
       Scc:
        {le#(s x, s y) -> le#(x, y)}
       
       SCC (6):
        Strict:
         { if#(true(), b1, b2, b3, x, y) -> if2#(b1, b2, b3, x, y),
          if#(false(), b1, b2, b3, x, y) -> average#(p x, s y),
                          average#(x, y) -> if#(le(x, 0()), le(y, 0()), le(y, s 0()), le(y, s s 0()), x, y),
             if2#(false(), b2, b3, x, y) -> if3#(b2, b3, x, y),
                 if3#(false(), b3, x, y) -> if4#(b3, x, y),
                     if4#(false(), x, y) -> average#(s x, p p y)}
        Weak:
        {                        p s x -> x,
                                 p 0() -> 0(),
                          le(s x, s y) -> le(x, y),
                          le(s x, 0()) -> false(),
                            le(0(), y) -> true(),
          if(true(), b1, b2, b3, x, y) -> if2(b1, b2, b3, x, y),
         if(false(), b1, b2, b3, x, y) -> average(p x, s y),
                         average(x, y) -> if(le(x, 0()), le(y, 0()), le(y, s 0()), le(y, s s 0()), x, y),
             if2(true(), b2, b3, x, y) -> 0(),
            if2(false(), b2, b3, x, y) -> if3(b2, b3, x, y),
                 if3(true(), b3, x, y) -> 0(),
                if3(false(), b3, x, y) -> if4(b3, x, y),
                     if4(true(), x, y) -> s 0(),
                    if4(false(), x, y) -> average(s x, p p y)}
        Open
       
       
       
       
       
       
       
       SCC (1):
        Strict:
         {le#(s x, s y) -> le#(x, y)}
        Weak:
        {                        p s x -> x,
                                 p 0() -> 0(),
                          le(s x, s y) -> le(x, y),
                          le(s x, 0()) -> false(),
                            le(0(), y) -> true(),
          if(true(), b1, b2, b3, x, y) -> if2(b1, b2, b3, x, y),
         if(false(), b1, b2, b3, x, y) -> average(p x, s y),
                         average(x, y) -> if(le(x, 0()), le(y, 0()), le(y, s 0()), le(y, s s 0()), x, y),
             if2(true(), b2, b3, x, y) -> 0(),
            if2(false(), b2, b3, x, y) -> if3(b2, b3, x, y),
                 if3(true(), b3, x, y) -> 0(),
                if3(false(), b3, x, y) -> if4(b3, x, y),
                     if4(true(), x, y) -> s 0(),
                    if4(false(), x, y) -> average(s x, p p y)}
        Open