MAYBE
Time: 0.010701
TRS:
 { cond2(true(), x, y) -> cond3(gr(x, 0()), x, y),
  cond2(false(), x, y) -> cond4(gr(y, 0()), x, y),
            gr(0(), x) -> false(),
          gr(s x, 0()) -> true(),
          gr(s x, s y) -> gr(x, y),
   cond1(true(), x, y) -> cond2(gr(x, y), x, y),
   cond3(true(), x, y) -> cond3(gr(x, 0()), p x, y),
  cond3(false(), x, y) -> cond1(and(gr(x, 0()), gr(y, 0())), x, y),
   cond4(true(), x, y) -> cond4(gr(y, 0()), x, p y),
  cond4(false(), x, y) -> cond1(and(gr(x, 0()), gr(y, 0())), x, y),
                 p 0() -> 0(),
                 p s x -> x,
       and(x, false()) -> false(),
   and(true(), true()) -> true(),
       and(false(), x) -> false()}
 DP:
  DP:
   { cond2#(true(), x, y) -> gr#(x, 0()),
     cond2#(true(), x, y) -> cond3#(gr(x, 0()), x, y),
    cond2#(false(), x, y) -> gr#(y, 0()),
    cond2#(false(), x, y) -> cond4#(gr(y, 0()), x, y),
            gr#(s x, s y) -> gr#(x, y),
     cond1#(true(), x, y) -> cond2#(gr(x, y), x, y),
     cond1#(true(), x, y) -> gr#(x, y),
     cond3#(true(), x, y) -> gr#(x, 0()),
     cond3#(true(), x, y) -> cond3#(gr(x, 0()), p x, y),
     cond3#(true(), x, y) -> p# x,
    cond3#(false(), x, y) -> gr#(x, 0()),
    cond3#(false(), x, y) -> gr#(y, 0()),
    cond3#(false(), x, y) -> cond1#(and(gr(x, 0()), gr(y, 0())), x, y),
    cond3#(false(), x, y) -> and#(gr(x, 0()), gr(y, 0())),
     cond4#(true(), x, y) -> gr#(y, 0()),
     cond4#(true(), x, y) -> cond4#(gr(y, 0()), x, p y),
     cond4#(true(), x, y) -> p# y,
    cond4#(false(), x, y) -> gr#(x, 0()),
    cond4#(false(), x, y) -> gr#(y, 0()),
    cond4#(false(), x, y) -> cond1#(and(gr(x, 0()), gr(y, 0())), x, y),
    cond4#(false(), x, y) -> and#(gr(x, 0()), gr(y, 0()))}
  TRS:
  { cond2(true(), x, y) -> cond3(gr(x, 0()), x, y),
   cond2(false(), x, y) -> cond4(gr(y, 0()), x, y),
             gr(0(), x) -> false(),
           gr(s x, 0()) -> true(),
           gr(s x, s y) -> gr(x, y),
    cond1(true(), x, y) -> cond2(gr(x, y), x, y),
    cond3(true(), x, y) -> cond3(gr(x, 0()), p x, y),
   cond3(false(), x, y) -> cond1(and(gr(x, 0()), gr(y, 0())), x, y),
    cond4(true(), x, y) -> cond4(gr(y, 0()), x, p y),
   cond4(false(), x, y) -> cond1(and(gr(x, 0()), gr(y, 0())), x, y),
                  p 0() -> 0(),
                  p s x -> x,
        and(x, false()) -> false(),
    and(true(), true()) -> true(),
        and(false(), x) -> false()}
  UR:
   {         gr(0(), x) -> false(),
           gr(s x, 0()) -> true(),
           gr(s x, s y) -> gr(x, y),
                  p 0() -> 0(),
                  p s x -> x,
        and(x, false()) -> false(),
    and(true(), true()) -> true(),
        and(false(), x) -> false(),
                a(z, w) -> z,
                a(z, w) -> w}
   EDG:
    {(cond2#(false(), x, y) -> gr#(y, 0()), gr#(s x, s y) -> gr#(x, y))
     (cond3#(false(), x, y) -> gr#(x, 0()), gr#(s x, s y) -> gr#(x, y))
     (cond4#(true(), x, y) -> gr#(y, 0()), gr#(s x, s y) -> gr#(x, y))
     (cond4#(false(), x, y) -> gr#(y, 0()), gr#(s x, s y) -> gr#(x, y))
     (cond1#(true(), x, y) -> gr#(x, y), gr#(s x, s y) -> gr#(x, y))
     (cond3#(true(), x, y) -> cond3#(gr(x, 0()), p x, y), cond3#(false(), x, y) -> and#(gr(x, 0()), gr(y, 0())))
     (cond3#(true(), x, y) -> cond3#(gr(x, 0()), p x, y), cond3#(false(), x, y) -> cond1#(and(gr(x, 0()), gr(y, 0())), x, y))
     (cond3#(true(), x, y) -> cond3#(gr(x, 0()), p x, y), cond3#(false(), x, y) -> gr#(y, 0()))
     (cond3#(true(), x, y) -> cond3#(gr(x, 0()), p x, y), cond3#(false(), x, y) -> gr#(x, 0()))
     (cond3#(true(), x, y) -> cond3#(gr(x, 0()), p x, y), cond3#(true(), x, y) -> p# x)
     (cond3#(true(), x, y) -> cond3#(gr(x, 0()), p x, y), cond3#(true(), x, y) -> cond3#(gr(x, 0()), p x, y))
     (cond3#(true(), x, y) -> cond3#(gr(x, 0()), p x, y), cond3#(true(), x, y) -> gr#(x, 0()))
     (cond2#(false(), x, y) -> cond4#(gr(y, 0()), x, y), cond4#(false(), x, y) -> and#(gr(x, 0()), gr(y, 0())))
     (cond2#(false(), x, y) -> cond4#(gr(y, 0()), x, y), cond4#(false(), x, y) -> cond1#(and(gr(x, 0()), gr(y, 0())), x, y))
     (cond2#(false(), x, y) -> cond4#(gr(y, 0()), x, y), cond4#(false(), x, y) -> gr#(y, 0()))
     (cond2#(false(), x, y) -> cond4#(gr(y, 0()), x, y), cond4#(false(), x, y) -> gr#(x, 0()))
     (cond2#(false(), x, y) -> cond4#(gr(y, 0()), x, y), cond4#(true(), x, y) -> p# y)
     (cond2#(false(), x, y) -> cond4#(gr(y, 0()), x, y), cond4#(true(), x, y) -> cond4#(gr(y, 0()), x, p y))
     (cond2#(false(), x, y) -> cond4#(gr(y, 0()), x, y), cond4#(true(), x, y) -> gr#(y, 0()))
     (cond3#(false(), x, y) -> cond1#(and(gr(x, 0()), gr(y, 0())), x, y), cond1#(true(), x, y) -> gr#(x, y))
     (cond3#(false(), x, y) -> cond1#(and(gr(x, 0()), gr(y, 0())), x, y), cond1#(true(), x, y) -> cond2#(gr(x, y), x, y))
     (cond4#(false(), x, y) -> cond1#(and(gr(x, 0()), gr(y, 0())), x, y), cond1#(true(), x, y) -> cond2#(gr(x, y), x, y))
     (cond4#(false(), x, y) -> cond1#(and(gr(x, 0()), gr(y, 0())), x, y), cond1#(true(), x, y) -> gr#(x, y))
     (cond1#(true(), x, y) -> cond2#(gr(x, y), x, y), cond2#(true(), x, y) -> gr#(x, 0()))
     (cond1#(true(), x, y) -> cond2#(gr(x, y), x, y), cond2#(true(), x, y) -> cond3#(gr(x, 0()), x, y))
     (cond1#(true(), x, y) -> cond2#(gr(x, y), x, y), cond2#(false(), x, y) -> gr#(y, 0()))
     (cond1#(true(), x, y) -> cond2#(gr(x, y), x, y), cond2#(false(), x, y) -> cond4#(gr(y, 0()), x, y))
     (cond2#(true(), x, y) -> cond3#(gr(x, 0()), x, y), cond3#(true(), x, y) -> gr#(x, 0()))
     (cond2#(true(), x, y) -> cond3#(gr(x, 0()), x, y), cond3#(true(), x, y) -> cond3#(gr(x, 0()), p x, y))
     (cond2#(true(), x, y) -> cond3#(gr(x, 0()), x, y), cond3#(true(), x, y) -> p# x)
     (cond2#(true(), x, y) -> cond3#(gr(x, 0()), x, y), cond3#(false(), x, y) -> gr#(x, 0()))
     (cond2#(true(), x, y) -> cond3#(gr(x, 0()), x, y), cond3#(false(), x, y) -> gr#(y, 0()))
     (cond2#(true(), x, y) -> cond3#(gr(x, 0()), x, y), cond3#(false(), x, y) -> cond1#(and(gr(x, 0()), gr(y, 0())), x, y))
     (cond2#(true(), x, y) -> cond3#(gr(x, 0()), x, y), cond3#(false(), x, y) -> and#(gr(x, 0()), gr(y, 0())))
     (cond4#(true(), x, y) -> cond4#(gr(y, 0()), x, p y), cond4#(true(), x, y) -> gr#(y, 0()))
     (cond4#(true(), x, y) -> cond4#(gr(y, 0()), x, p y), cond4#(true(), x, y) -> cond4#(gr(y, 0()), x, p y))
     (cond4#(true(), x, y) -> cond4#(gr(y, 0()), x, p y), cond4#(true(), x, y) -> p# y)
     (cond4#(true(), x, y) -> cond4#(gr(y, 0()), x, p y), cond4#(false(), x, y) -> gr#(x, 0()))
     (cond4#(true(), x, y) -> cond4#(gr(y, 0()), x, p y), cond4#(false(), x, y) -> gr#(y, 0()))
     (cond4#(true(), x, y) -> cond4#(gr(y, 0()), x, p y), cond4#(false(), x, y) -> cond1#(and(gr(x, 0()), gr(y, 0())), x, y))
     (cond4#(true(), x, y) -> cond4#(gr(y, 0()), x, p y), cond4#(false(), x, y) -> and#(gr(x, 0()), gr(y, 0())))
     (gr#(s x, s y) -> gr#(x, y), gr#(s x, s y) -> gr#(x, y))
     (cond4#(false(), x, y) -> gr#(x, 0()), gr#(s x, s y) -> gr#(x, y))
     (cond3#(false(), x, y) -> gr#(y, 0()), gr#(s x, s y) -> gr#(x, y))
     (cond3#(true(), x, y) -> gr#(x, 0()), gr#(s x, s y) -> gr#(x, y))
     (cond2#(true(), x, y) -> gr#(x, 0()), gr#(s x, s y) -> gr#(x, y))}
    EDG:
     {(cond1#(true(), x, y) -> gr#(x, y), gr#(s x, s y) -> gr#(x, y))
      (cond3#(true(), x, y) -> cond3#(gr(x, 0()), p x, y), cond3#(false(), x, y) -> and#(gr(x, 0()), gr(y, 0())))
      (cond3#(true(), x, y) -> cond3#(gr(x, 0()), p x, y), cond3#(false(), x, y) -> cond1#(and(gr(x, 0()), gr(y, 0())), x, y))
      (cond3#(true(), x, y) -> cond3#(gr(x, 0()), p x, y), cond3#(false(), x, y) -> gr#(y, 0()))
      (cond3#(true(), x, y) -> cond3#(gr(x, 0()), p x, y), cond3#(false(), x, y) -> gr#(x, 0()))
      (cond3#(true(), x, y) -> cond3#(gr(x, 0()), p x, y), cond3#(true(), x, y) -> p# x)
      (cond3#(true(), x, y) -> cond3#(gr(x, 0()), p x, y), cond3#(true(), x, y) -> cond3#(gr(x, 0()), p x, y))
      (cond3#(true(), x, y) -> cond3#(gr(x, 0()), p x, y), cond3#(true(), x, y) -> gr#(x, 0()))
      (cond2#(false(), x, y) -> cond4#(gr(y, 0()), x, y), cond4#(false(), x, y) -> and#(gr(x, 0()), gr(y, 0())))
      (cond2#(false(), x, y) -> cond4#(gr(y, 0()), x, y), cond4#(false(), x, y) -> cond1#(and(gr(x, 0()), gr(y, 0())), x, y))
      (cond2#(false(), x, y) -> cond4#(gr(y, 0()), x, y), cond4#(false(), x, y) -> gr#(y, 0()))
      (cond2#(false(), x, y) -> cond4#(gr(y, 0()), x, y), cond4#(false(), x, y) -> gr#(x, 0()))
      (cond2#(false(), x, y) -> cond4#(gr(y, 0()), x, y), cond4#(true(), x, y) -> p# y)
      (cond2#(false(), x, y) -> cond4#(gr(y, 0()), x, y), cond4#(true(), x, y) -> cond4#(gr(y, 0()), x, p y))
      (cond2#(false(), x, y) -> cond4#(gr(y, 0()), x, y), cond4#(true(), x, y) -> gr#(y, 0()))
      (cond3#(false(), x, y) -> cond1#(and(gr(x, 0()), gr(y, 0())), x, y), cond1#(true(), x, y) -> gr#(x, y))
      (cond3#(false(), x, y) -> cond1#(and(gr(x, 0()), gr(y, 0())), x, y), cond1#(true(), x, y) -> cond2#(gr(x, y), x, y))
      (cond4#(false(), x, y) -> cond1#(and(gr(x, 0()), gr(y, 0())), x, y), cond1#(true(), x, y) -> cond2#(gr(x, y), x, y))
      (cond4#(false(), x, y) -> cond1#(and(gr(x, 0()), gr(y, 0())), x, y), cond1#(true(), x, y) -> gr#(x, y))
      (cond1#(true(), x, y) -> cond2#(gr(x, y), x, y), cond2#(true(), x, y) -> gr#(x, 0()))
      (cond1#(true(), x, y) -> cond2#(gr(x, y), x, y), cond2#(true(), x, y) -> cond3#(gr(x, 0()), x, y))
      (cond1#(true(), x, y) -> cond2#(gr(x, y), x, y), cond2#(false(), x, y) -> gr#(y, 0()))
      (cond1#(true(), x, y) -> cond2#(gr(x, y), x, y), cond2#(false(), x, y) -> cond4#(gr(y, 0()), x, y))
      (cond2#(true(), x, y) -> cond3#(gr(x, 0()), x, y), cond3#(true(), x, y) -> gr#(x, 0()))
      (cond2#(true(), x, y) -> cond3#(gr(x, 0()), x, y), cond3#(true(), x, y) -> cond3#(gr(x, 0()), p x, y))
      (cond2#(true(), x, y) -> cond3#(gr(x, 0()), x, y), cond3#(true(), x, y) -> p# x)
      (cond2#(true(), x, y) -> cond3#(gr(x, 0()), x, y), cond3#(false(), x, y) -> gr#(x, 0()))
      (cond2#(true(), x, y) -> cond3#(gr(x, 0()), x, y), cond3#(false(), x, y) -> gr#(y, 0()))
      (cond2#(true(), x, y) -> cond3#(gr(x, 0()), x, y), cond3#(false(), x, y) -> cond1#(and(gr(x, 0()), gr(y, 0())), x, y))
      (cond2#(true(), x, y) -> cond3#(gr(x, 0()), x, y), cond3#(false(), x, y) -> and#(gr(x, 0()), gr(y, 0())))
      (cond4#(true(), x, y) -> cond4#(gr(y, 0()), x, p y), cond4#(true(), x, y) -> gr#(y, 0()))
      (cond4#(true(), x, y) -> cond4#(gr(y, 0()), x, p y), cond4#(true(), x, y) -> cond4#(gr(y, 0()), x, p y))
      (cond4#(true(), x, y) -> cond4#(gr(y, 0()), x, p y), cond4#(true(), x, y) -> p# y)
      (cond4#(true(), x, y) -> cond4#(gr(y, 0()), x, p y), cond4#(false(), x, y) -> gr#(x, 0()))
      (cond4#(true(), x, y) -> cond4#(gr(y, 0()), x, p y), cond4#(false(), x, y) -> gr#(y, 0()))
      (cond4#(true(), x, y) -> cond4#(gr(y, 0()), x, p y), cond4#(false(), x, y) -> cond1#(and(gr(x, 0()), gr(y, 0())), x, y))
      (cond4#(true(), x, y) -> cond4#(gr(y, 0()), x, p y), cond4#(false(), x, y) -> and#(gr(x, 0()), gr(y, 0())))
      (gr#(s x, s y) -> gr#(x, y), gr#(s x, s y) -> gr#(x, y))}
     EDG:
      {(cond1#(true(), x, y) -> gr#(x, y), gr#(s x, s y) -> gr#(x, y))
       (cond3#(true(), x, y) -> cond3#(gr(x, 0()), p x, y), cond3#(false(), x, y) -> and#(gr(x, 0()), gr(y, 0())))
       (cond3#(true(), x, y) -> cond3#(gr(x, 0()), p x, y), cond3#(false(), x, y) -> cond1#(and(gr(x, 0()), gr(y, 0())), x, y))
       (cond3#(true(), x, y) -> cond3#(gr(x, 0()), p x, y), cond3#(false(), x, y) -> gr#(y, 0()))
       (cond3#(true(), x, y) -> cond3#(gr(x, 0()), p x, y), cond3#(false(), x, y) -> gr#(x, 0()))
       (cond3#(true(), x, y) -> cond3#(gr(x, 0()), p x, y), cond3#(true(), x, y) -> p# x)
       (cond3#(true(), x, y) -> cond3#(gr(x, 0()), p x, y), cond3#(true(), x, y) -> cond3#(gr(x, 0()), p x, y))
       (cond3#(true(), x, y) -> cond3#(gr(x, 0()), p x, y), cond3#(true(), x, y) -> gr#(x, 0()))
       (cond2#(false(), x, y) -> cond4#(gr(y, 0()), x, y), cond4#(false(), x, y) -> and#(gr(x, 0()), gr(y, 0())))
       (cond2#(false(), x, y) -> cond4#(gr(y, 0()), x, y), cond4#(false(), x, y) -> cond1#(and(gr(x, 0()), gr(y, 0())), x, y))
       (cond2#(false(), x, y) -> cond4#(gr(y, 0()), x, y), cond4#(false(), x, y) -> gr#(y, 0()))
       (cond2#(false(), x, y) -> cond4#(gr(y, 0()), x, y), cond4#(false(), x, y) -> gr#(x, 0()))
       (cond2#(false(), x, y) -> cond4#(gr(y, 0()), x, y), cond4#(true(), x, y) -> p# y)
       (cond2#(false(), x, y) -> cond4#(gr(y, 0()), x, y), cond4#(true(), x, y) -> cond4#(gr(y, 0()), x, p y))
       (cond2#(false(), x, y) -> cond4#(gr(y, 0()), x, y), cond4#(true(), x, y) -> gr#(y, 0()))
       (cond3#(false(), x, y) -> cond1#(and(gr(x, 0()), gr(y, 0())), x, y), cond1#(true(), x, y) -> gr#(x, y))
       (cond3#(false(), x, y) -> cond1#(and(gr(x, 0()), gr(y, 0())), x, y), cond1#(true(), x, y) -> cond2#(gr(x, y), x, y))
       (cond4#(false(), x, y) -> cond1#(and(gr(x, 0()), gr(y, 0())), x, y), cond1#(true(), x, y) -> cond2#(gr(x, y), x, y))
       (cond4#(false(), x, y) -> cond1#(and(gr(x, 0()), gr(y, 0())), x, y), cond1#(true(), x, y) -> gr#(x, y))
       (cond1#(true(), x, y) -> cond2#(gr(x, y), x, y), cond2#(true(), x, y) -> gr#(x, 0()))
       (cond1#(true(), x, y) -> cond2#(gr(x, y), x, y), cond2#(true(), x, y) -> cond3#(gr(x, 0()), x, y))
       (cond1#(true(), x, y) -> cond2#(gr(x, y), x, y), cond2#(false(), x, y) -> gr#(y, 0()))
       (cond1#(true(), x, y) -> cond2#(gr(x, y), x, y), cond2#(false(), x, y) -> cond4#(gr(y, 0()), x, y))
       (cond2#(true(), x, y) -> cond3#(gr(x, 0()), x, y), cond3#(true(), x, y) -> gr#(x, 0()))
       (cond2#(true(), x, y) -> cond3#(gr(x, 0()), x, y), cond3#(true(), x, y) -> cond3#(gr(x, 0()), p x, y))
       (cond2#(true(), x, y) -> cond3#(gr(x, 0()), x, y), cond3#(true(), x, y) -> p# x)
       (cond2#(true(), x, y) -> cond3#(gr(x, 0()), x, y), cond3#(false(), x, y) -> gr#(x, 0()))
       (cond2#(true(), x, y) -> cond3#(gr(x, 0()), x, y), cond3#(false(), x, y) -> gr#(y, 0()))
       (cond2#(true(), x, y) -> cond3#(gr(x, 0()), x, y), cond3#(false(), x, y) -> cond1#(and(gr(x, 0()), gr(y, 0())), x, y))
       (cond2#(true(), x, y) -> cond3#(gr(x, 0()), x, y), cond3#(false(), x, y) -> and#(gr(x, 0()), gr(y, 0())))
       (cond4#(true(), x, y) -> cond4#(gr(y, 0()), x, p y), cond4#(true(), x, y) -> gr#(y, 0()))
       (cond4#(true(), x, y) -> cond4#(gr(y, 0()), x, p y), cond4#(true(), x, y) -> cond4#(gr(y, 0()), x, p y))
       (cond4#(true(), x, y) -> cond4#(gr(y, 0()), x, p y), cond4#(true(), x, y) -> p# y)
       (cond4#(true(), x, y) -> cond4#(gr(y, 0()), x, p y), cond4#(false(), x, y) -> gr#(x, 0()))
       (cond4#(true(), x, y) -> cond4#(gr(y, 0()), x, p y), cond4#(false(), x, y) -> gr#(y, 0()))
       (cond4#(true(), x, y) -> cond4#(gr(y, 0()), x, p y), cond4#(false(), x, y) -> cond1#(and(gr(x, 0()), gr(y, 0())), x, y))
       (cond4#(true(), x, y) -> cond4#(gr(y, 0()), x, p y), cond4#(false(), x, y) -> and#(gr(x, 0()), gr(y, 0())))
       (gr#(s x, s y) -> gr#(x, y), gr#(s x, s y) -> gr#(x, y))}
      EDG:
       {(cond1#(true(), x, y) -> gr#(x, y), gr#(s x, s y) -> gr#(x, y))
        (cond3#(true(), x, y) -> cond3#(gr(x, 0()), p x, y), cond3#(false(), x, y) -> and#(gr(x, 0()), gr(y, 0())))
        (cond3#(true(), x, y) -> cond3#(gr(x, 0()), p x, y), cond3#(false(), x, y) -> cond1#(and(gr(x, 0()), gr(y, 0())), x, y))
        (cond3#(true(), x, y) -> cond3#(gr(x, 0()), p x, y), cond3#(false(), x, y) -> gr#(y, 0()))
        (cond3#(true(), x, y) -> cond3#(gr(x, 0()), p x, y), cond3#(false(), x, y) -> gr#(x, 0()))
        (cond3#(true(), x, y) -> cond3#(gr(x, 0()), p x, y), cond3#(true(), x, y) -> p# x)
        (cond3#(true(), x, y) -> cond3#(gr(x, 0()), p x, y), cond3#(true(), x, y) -> cond3#(gr(x, 0()), p x, y))
        (cond3#(true(), x, y) -> cond3#(gr(x, 0()), p x, y), cond3#(true(), x, y) -> gr#(x, 0()))
        (cond2#(false(), x, y) -> cond4#(gr(y, 0()), x, y), cond4#(false(), x, y) -> and#(gr(x, 0()), gr(y, 0())))
        (cond2#(false(), x, y) -> cond4#(gr(y, 0()), x, y), cond4#(false(), x, y) -> cond1#(and(gr(x, 0()), gr(y, 0())), x, y))
        (cond2#(false(), x, y) -> cond4#(gr(y, 0()), x, y), cond4#(false(), x, y) -> gr#(y, 0()))
        (cond2#(false(), x, y) -> cond4#(gr(y, 0()), x, y), cond4#(false(), x, y) -> gr#(x, 0()))
        (cond2#(false(), x, y) -> cond4#(gr(y, 0()), x, y), cond4#(true(), x, y) -> p# y)
        (cond2#(false(), x, y) -> cond4#(gr(y, 0()), x, y), cond4#(true(), x, y) -> cond4#(gr(y, 0()), x, p y))
        (cond2#(false(), x, y) -> cond4#(gr(y, 0()), x, y), cond4#(true(), x, y) -> gr#(y, 0()))
        (cond3#(false(), x, y) -> cond1#(and(gr(x, 0()), gr(y, 0())), x, y), cond1#(true(), x, y) -> gr#(x, y))
        (cond3#(false(), x, y) -> cond1#(and(gr(x, 0()), gr(y, 0())), x, y), cond1#(true(), x, y) -> cond2#(gr(x, y), x, y))
        (cond4#(false(), x, y) -> cond1#(and(gr(x, 0()), gr(y, 0())), x, y), cond1#(true(), x, y) -> cond2#(gr(x, y), x, y))
        (cond4#(false(), x, y) -> cond1#(and(gr(x, 0()), gr(y, 0())), x, y), cond1#(true(), x, y) -> gr#(x, y))
        (cond1#(true(), x, y) -> cond2#(gr(x, y), x, y), cond2#(true(), x, y) -> gr#(x, 0()))
        (cond1#(true(), x, y) -> cond2#(gr(x, y), x, y), cond2#(true(), x, y) -> cond3#(gr(x, 0()), x, y))
        (cond1#(true(), x, y) -> cond2#(gr(x, y), x, y), cond2#(false(), x, y) -> gr#(y, 0()))
        (cond1#(true(), x, y) -> cond2#(gr(x, y), x, y), cond2#(false(), x, y) -> cond4#(gr(y, 0()), x, y))
        (cond2#(true(), x, y) -> cond3#(gr(x, 0()), x, y), cond3#(true(), x, y) -> gr#(x, 0()))
        (cond2#(true(), x, y) -> cond3#(gr(x, 0()), x, y), cond3#(true(), x, y) -> cond3#(gr(x, 0()), p x, y))
        (cond2#(true(), x, y) -> cond3#(gr(x, 0()), x, y), cond3#(true(), x, y) -> p# x)
        (cond2#(true(), x, y) -> cond3#(gr(x, 0()), x, y), cond3#(false(), x, y) -> gr#(x, 0()))
        (cond2#(true(), x, y) -> cond3#(gr(x, 0()), x, y), cond3#(false(), x, y) -> gr#(y, 0()))
        (cond2#(true(), x, y) -> cond3#(gr(x, 0()), x, y), cond3#(false(), x, y) -> cond1#(and(gr(x, 0()), gr(y, 0())), x, y))
        (cond2#(true(), x, y) -> cond3#(gr(x, 0()), x, y), cond3#(false(), x, y) -> and#(gr(x, 0()), gr(y, 0())))
        (cond4#(true(), x, y) -> cond4#(gr(y, 0()), x, p y), cond4#(true(), x, y) -> gr#(y, 0()))
        (cond4#(true(), x, y) -> cond4#(gr(y, 0()), x, p y), cond4#(true(), x, y) -> cond4#(gr(y, 0()), x, p y))
        (cond4#(true(), x, y) -> cond4#(gr(y, 0()), x, p y), cond4#(true(), x, y) -> p# y)
        (cond4#(true(), x, y) -> cond4#(gr(y, 0()), x, p y), cond4#(false(), x, y) -> gr#(x, 0()))
        (cond4#(true(), x, y) -> cond4#(gr(y, 0()), x, p y), cond4#(false(), x, y) -> gr#(y, 0()))
        (cond4#(true(), x, y) -> cond4#(gr(y, 0()), x, p y), cond4#(false(), x, y) -> cond1#(and(gr(x, 0()), gr(y, 0())), x, y))
        (cond4#(true(), x, y) -> cond4#(gr(y, 0()), x, p y), cond4#(false(), x, y) -> and#(gr(x, 0()), gr(y, 0())))
        (gr#(s x, s y) -> gr#(x, y), gr#(s x, s y) -> gr#(x, y))}
       STATUS:
        arrows: 0.913832
        SCCS (2):
         Scc:
          { cond2#(true(), x, y) -> cond3#(gr(x, 0()), x, y),
           cond2#(false(), x, y) -> cond4#(gr(y, 0()), x, y),
            cond1#(true(), x, y) -> cond2#(gr(x, y), x, y),
            cond3#(true(), x, y) -> cond3#(gr(x, 0()), p x, y),
           cond3#(false(), x, y) -> cond1#(and(gr(x, 0()), gr(y, 0())), x, y),
            cond4#(true(), x, y) -> cond4#(gr(y, 0()), x, p y),
           cond4#(false(), x, y) -> cond1#(and(gr(x, 0()), gr(y, 0())), x, y)}
         Scc:
          {gr#(s x, s y) -> gr#(x, y)}
         
         SCC (7):
          Strict:
           { cond2#(true(), x, y) -> cond3#(gr(x, 0()), x, y),
            cond2#(false(), x, y) -> cond4#(gr(y, 0()), x, y),
             cond1#(true(), x, y) -> cond2#(gr(x, y), x, y),
             cond3#(true(), x, y) -> cond3#(gr(x, 0()), p x, y),
            cond3#(false(), x, y) -> cond1#(and(gr(x, 0()), gr(y, 0())), x, y),
             cond4#(true(), x, y) -> cond4#(gr(y, 0()), x, p y),
            cond4#(false(), x, y) -> cond1#(and(gr(x, 0()), gr(y, 0())), x, y)}
          Weak:
          { cond2(true(), x, y) -> cond3(gr(x, 0()), x, y),
           cond2(false(), x, y) -> cond4(gr(y, 0()), x, y),
                     gr(0(), x) -> false(),
                   gr(s x, 0()) -> true(),
                   gr(s x, s y) -> gr(x, y),
            cond1(true(), x, y) -> cond2(gr(x, y), x, y),
            cond3(true(), x, y) -> cond3(gr(x, 0()), p x, y),
           cond3(false(), x, y) -> cond1(and(gr(x, 0()), gr(y, 0())), x, y),
            cond4(true(), x, y) -> cond4(gr(y, 0()), x, p y),
           cond4(false(), x, y) -> cond1(and(gr(x, 0()), gr(y, 0())), x, y),
                          p 0() -> 0(),
                          p s x -> x,
                and(x, false()) -> false(),
            and(true(), true()) -> true(),
                and(false(), x) -> false()}
          Open
         
         
         
         SCC (1):
          Strict:
           {gr#(s x, s y) -> gr#(x, y)}
          Weak:
          { cond2(true(), x, y) -> cond3(gr(x, 0()), x, y),
           cond2(false(), x, y) -> cond4(gr(y, 0()), x, y),
                     gr(0(), x) -> false(),
                   gr(s x, 0()) -> true(),
                   gr(s x, s y) -> gr(x, y),
            cond1(true(), x, y) -> cond2(gr(x, y), x, y),
            cond3(true(), x, y) -> cond3(gr(x, 0()), p x, y),
           cond3(false(), x, y) -> cond1(and(gr(x, 0()), gr(y, 0())), x, y),
            cond4(true(), x, y) -> cond4(gr(y, 0()), x, p y),
           cond4(false(), x, y) -> cond1(and(gr(x, 0()), gr(y, 0())), x, y),
                          p 0() -> 0(),
                          p s x -> x,
                and(x, false()) -> false(),
            and(true(), true()) -> true(),
                and(false(), x) -> false()}
          Open