Time: 3.582210
TRS:
 {         Cond_eval(true(), x) -> eval minus_int(x, pos s 0()),
            and(true(), true()) -> true(),
           and(true(), false()) -> false(),
           and(false(), true()) -> false(),
          and(false(), false()) -> false(),
  greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
  greater_int(pos s x, pos 0()) -> true(),
  greater_int(pos s x, neg s y) -> true(),
  greater_int(pos s x, neg 0()) -> true(),
  greater_int(pos 0(), pos s y) -> false(),
  greater_int(pos 0(), pos 0()) -> false(),
  greater_int(pos 0(), neg s y) -> true(),
  greater_int(pos 0(), neg 0()) -> false(),
  greater_int(neg s x, pos s y) -> false(),
  greater_int(neg s x, pos 0()) -> false(),
  greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
  greater_int(neg s x, neg 0()) -> false(),
  greater_int(neg 0(), pos s y) -> false(),
  greater_int(neg 0(), pos 0()) -> false(),
  greater_int(neg 0(), neg s y) -> true(),
  greater_int(neg 0(), neg 0()) -> false(),
          mod_int(pos x, pos y) -> pos mod_nat(x, y),
          mod_int(pos x, neg y) -> pos mod_nat(x, y),
          mod_int(neg x, pos y) -> neg mod_nat(x, y),
          mod_int(neg x, neg y) -> neg mod_nat(x, y),
                         eval x -> Cond_eval(and(greater_int(mod_int(x, pos s s 0()), pos 0()), greater_int(x, pos 0())), x),
        minus_int(pos x, pos y) -> minus_nat(x, y),
        minus_int(pos x, neg y) -> pos plus_nat(x, y),
        minus_int(neg x, pos y) -> neg plus_nat(x, y),
        minus_int(neg x, neg y) -> minus_nat(y, x),
              mod_nat(s x, s y) -> if(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x),
              mod_nat(0(), s x) -> 0(),
               if(true(), x, y) -> x,
              if(false(), x, y) -> y,
            minus_nat_s(x, 0()) -> x,
          minus_nat_s(s x, s y) -> minus_nat_s(x, y),
          minus_nat_s(0(), s y) -> 0(),
            minus_nat(s x, s y) -> minus_nat(x, y),
            minus_nat(s x, 0()) -> pos s x,
            minus_nat(0(), s y) -> neg s y,
            minus_nat(0(), 0()) -> pos 0(),
               plus_nat(s x, y) -> s plus_nat(x, y),
               plus_nat(0(), x) -> x}
 SRS: We consider a TRS.
  Trs:
   {         Cond_eval(true(), x) -> eval minus_int(x, pos s 0()),
              and(true(), true()) -> true(),
             and(true(), false()) -> false(),
             and(false(), true()) -> false(),
            and(false(), false()) -> false(),
    greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
    greater_int(pos s x, pos 0()) -> true(),
    greater_int(pos s x, neg s y) -> true(),
    greater_int(pos s x, neg 0()) -> true(),
    greater_int(pos 0(), pos s y) -> false(),
    greater_int(pos 0(), pos 0()) -> false(),
    greater_int(pos 0(), neg s y) -> true(),
    greater_int(pos 0(), neg 0()) -> false(),
    greater_int(neg s x, pos s y) -> false(),
    greater_int(neg s x, pos 0()) -> false(),
    greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
    greater_int(neg s x, neg 0()) -> false(),
    greater_int(neg 0(), pos s y) -> false(),
    greater_int(neg 0(), pos 0()) -> false(),
    greater_int(neg 0(), neg s y) -> true(),
    greater_int(neg 0(), neg 0()) -> false(),
            mod_int(pos x, pos y) -> pos mod_nat(x, y),
            mod_int(pos x, neg y) -> pos mod_nat(x, y),
            mod_int(neg x, pos y) -> neg mod_nat(x, y),
            mod_int(neg x, neg y) -> neg mod_nat(x, y),
                           eval x -> Cond_eval(and(greater_int(mod_int(x, pos s s 0()), pos 0()), greater_int(x, pos 0())), x),
          minus_int(pos x, pos y) -> minus_nat(x, y),
          minus_int(pos x, neg y) -> pos plus_nat(x, y),
          minus_int(neg x, pos y) -> neg plus_nat(x, y),
          minus_int(neg x, neg y) -> minus_nat(y, x),
                mod_nat(s x, s y) -> if(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x),
                mod_nat(0(), s x) -> 0(),
                 if(true(), x, y) -> x,
                if(false(), x, y) -> y,
              minus_nat_s(x, 0()) -> x,
            minus_nat_s(s x, s y) -> minus_nat_s(x, y),
            minus_nat_s(0(), s y) -> 0(),
              minus_nat(s x, s y) -> minus_nat(x, y),
              minus_nat(s x, 0()) -> pos s x,
              minus_nat(0(), s y) -> neg s y,
              minus_nat(0(), 0()) -> pos 0(),
                 plus_nat(s x, y) -> s plus_nat(x, y),
                 plus_nat(0(), x) -> x}
  APP: We consider a non-applicative system.
   Trs:
    {         Cond_eval(true(), x) -> eval minus_int(x, pos s 0()),
               and(true(), true()) -> true(),
              and(true(), false()) -> false(),
              and(false(), true()) -> false(),
             and(false(), false()) -> false(),
     greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
     greater_int(pos s x, pos 0()) -> true(),
     greater_int(pos s x, neg s y) -> true(),
     greater_int(pos s x, neg 0()) -> true(),
     greater_int(pos 0(), pos s y) -> false(),
     greater_int(pos 0(), pos 0()) -> false(),
     greater_int(pos 0(), neg s y) -> true(),
     greater_int(pos 0(), neg 0()) -> false(),
     greater_int(neg s x, pos s y) -> false(),
     greater_int(neg s x, pos 0()) -> false(),
     greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
     greater_int(neg s x, neg 0()) -> false(),
     greater_int(neg 0(), pos s y) -> false(),
     greater_int(neg 0(), pos 0()) -> false(),
     greater_int(neg 0(), neg s y) -> true(),
     greater_int(neg 0(), neg 0()) -> false(),
             mod_int(pos x, pos y) -> pos mod_nat(x, y),
             mod_int(pos x, neg y) -> pos mod_nat(x, y),
             mod_int(neg x, pos y) -> neg mod_nat(x, y),
             mod_int(neg x, neg y) -> neg mod_nat(x, y),
                            eval x -> Cond_eval(and(greater_int(mod_int(x, pos s s 0()), pos 0()), greater_int(x, pos 0())), x),
           minus_int(pos x, pos y) -> minus_nat(x, y),
           minus_int(pos x, neg y) -> pos plus_nat(x, y),
           minus_int(neg x, pos y) -> neg plus_nat(x, y),
           minus_int(neg x, neg y) -> minus_nat(y, x),
                 mod_nat(s x, s y) -> if(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x),
                 mod_nat(0(), s x) -> 0(),
                  if(true(), x, y) -> x,
                 if(false(), x, y) -> y,
               minus_nat_s(x, 0()) -> x,
             minus_nat_s(s x, s y) -> minus_nat_s(x, y),
             minus_nat_s(0(), s y) -> 0(),
               minus_nat(s x, s y) -> minus_nat(x, y),
               minus_nat(s x, 0()) -> pos s x,
               minus_nat(0(), s y) -> neg s y,
               minus_nat(0(), 0()) -> pos 0(),
                  plus_nat(s x, y) -> s plus_nat(x, y),
                  plus_nat(0(), x) -> x}
   REWRITE:
    Strict:
     {         Cond_eval(true(), x) -> Cond_eval(and(greater_int(mod_int(minus_int(x, pos s 0()), pos s s 0()), pos 0()), greater_int(minus_int(x, pos s 0()), pos 0())), minus_int(x, pos s 0())),
                and(true(), true()) -> true(),
               and(true(), false()) -> false(),
               and(false(), true()) -> false(),
              and(false(), false()) -> false(),
      greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
      greater_int(pos s x, pos 0()) -> true(),
      greater_int(pos s x, neg s y) -> true(),
      greater_int(pos s x, neg 0()) -> true(),
      greater_int(pos 0(), pos s y) -> false(),
      greater_int(pos 0(), pos 0()) -> false(),
      greater_int(pos 0(), neg s y) -> true(),
      greater_int(pos 0(), neg 0()) -> false(),
      greater_int(neg s x, pos s y) -> false(),
      greater_int(neg s x, pos 0()) -> false(),
      greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
      greater_int(neg s x, neg 0()) -> false(),
      greater_int(neg 0(), pos s y) -> false(),
      greater_int(neg 0(), pos 0()) -> false(),
      greater_int(neg 0(), neg s y) -> true(),
      greater_int(neg 0(), neg 0()) -> false(),
              mod_int(pos x, pos y) -> pos mod_nat(x, y),
              mod_int(pos x, neg y) -> pos mod_nat(x, y),
              mod_int(neg x, pos y) -> neg mod_nat(x, y),
              mod_int(neg x, neg y) -> neg mod_nat(x, y),
                             eval x -> Cond_eval(and(greater_int(mod_int(x, pos s s 0()), pos 0()), greater_int(x, pos 0())), x),
            minus_int(pos x, pos y) -> minus_nat(x, y),
            minus_int(pos x, neg y) -> pos plus_nat(x, y),
            minus_int(neg x, pos y) -> neg plus_nat(x, y),
            minus_int(neg x, neg y) -> minus_nat(y, x),
                  mod_nat(s x, s y) -> if(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x),
                  mod_nat(0(), s x) -> 0(),
                   if(true(), x, y) -> x,
                  if(false(), x, y) -> y,
                minus_nat_s(x, 0()) -> x,
              minus_nat_s(s x, s y) -> minus_nat_s(x, y),
              minus_nat_s(0(), s y) -> 0(),
                minus_nat(s x, s y) -> minus_nat(x, y),
                minus_nat(s x, 0()) -> pos s x,
                minus_nat(0(), s y) -> neg s y,
                minus_nat(0(), 0()) -> pos 0(),
                   plus_nat(s x, y) -> s plus_nat(x, y),
                   plus_nat(0(), x) -> x}
    Weak:
    {}
    DP:
     DP:
      {       Cond_eval#(true(), x) -> Cond_eval#(and(greater_int(mod_int(minus_int(x, pos s 0()), pos s s 0()), pos 0()), greater_int(minus_int(x, pos s 0()), pos 0())), minus_int(x, pos s 0())),
              Cond_eval#(true(), x) -> and#(greater_int(mod_int(minus_int(x, pos s 0()), pos s s 0()), pos 0()), greater_int(minus_int(x, pos s 0()), pos 0())),
              Cond_eval#(true(), x) -> greater_int#(mod_int(minus_int(x, pos s 0()), pos s s 0()), pos 0()),
              Cond_eval#(true(), x) -> greater_int#(minus_int(x, pos s 0()), pos 0()),
              Cond_eval#(true(), x) -> mod_int#(minus_int(x, pos s 0()), pos s s 0()),
              Cond_eval#(true(), x) -> minus_int#(x, pos s 0()),
       greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y),
       greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y),
           mod_int#(pos x, pos y) -> mod_nat#(x, y),
           mod_int#(pos x, neg y) -> mod_nat#(x, y),
           mod_int#(neg x, pos y) -> mod_nat#(x, y),
           mod_int#(neg x, neg y) -> mod_nat#(x, y),
                        eval# x -> Cond_eval#(and(greater_int(mod_int(x, pos s s 0()), pos 0()), greater_int(x, pos 0())), x),
                        eval# x -> and#(greater_int(mod_int(x, pos s s 0()), pos 0()), greater_int(x, pos 0())),
                        eval# x -> greater_int#(x, pos 0()),
                        eval# x -> greater_int#(mod_int(x, pos s s 0()), pos 0()),
                        eval# x -> mod_int#(x, pos s s 0()),
           minus_int#(pos x, pos y) -> minus_nat#(x, y),
           minus_int#(pos x, neg y) -> plus_nat#(x, y),
           minus_int#(neg x, pos y) -> plus_nat#(x, y),
           minus_int#(neg x, neg y) -> minus_nat#(y, x),
               mod_nat#(s x, s y) -> mod_nat#(minus_nat_s(x, y), s y),
               mod_nat#(s x, s y) -> if#(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x),
               mod_nat#(s x, s y) -> minus_nat_s#(x, y),
               minus_nat_s#(s x, s y) -> minus_nat_s#(x, y),
               minus_nat#(s x, s y) -> minus_nat#(x, y),
                 plus_nat#(s x, y) -> plus_nat#(x, y)}
     TRS:
     {         Cond_eval(true(), x) -> Cond_eval(and(greater_int(mod_int(minus_int(x, pos s 0()), pos s s 0()), pos 0()), greater_int(minus_int(x, pos s 0()), pos 0())), minus_int(x, pos s 0())),
                and(true(), true()) -> true(),
               and(true(), false()) -> false(),
               and(false(), true()) -> false(),
              and(false(), false()) -> false(),
      greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
      greater_int(pos s x, pos 0()) -> true(),
      greater_int(pos s x, neg s y) -> true(),
      greater_int(pos s x, neg 0()) -> true(),
      greater_int(pos 0(), pos s y) -> false(),
      greater_int(pos 0(), pos 0()) -> false(),
      greater_int(pos 0(), neg s y) -> true(),
      greater_int(pos 0(), neg 0()) -> false(),
      greater_int(neg s x, pos s y) -> false(),
      greater_int(neg s x, pos 0()) -> false(),
      greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
      greater_int(neg s x, neg 0()) -> false(),
      greater_int(neg 0(), pos s y) -> false(),
      greater_int(neg 0(), pos 0()) -> false(),
      greater_int(neg 0(), neg s y) -> true(),
      greater_int(neg 0(), neg 0()) -> false(),
              mod_int(pos x, pos y) -> pos mod_nat(x, y),
              mod_int(pos x, neg y) -> pos mod_nat(x, y),
              mod_int(neg x, pos y) -> neg mod_nat(x, y),
              mod_int(neg x, neg y) -> neg mod_nat(x, y),
                             eval x -> Cond_eval(and(greater_int(mod_int(x, pos s s 0()), pos 0()), greater_int(x, pos 0())), x),
            minus_int(pos x, pos y) -> minus_nat(x, y),
            minus_int(pos x, neg y) -> pos plus_nat(x, y),
            minus_int(neg x, pos y) -> neg plus_nat(x, y),
            minus_int(neg x, neg y) -> minus_nat(y, x),
                  mod_nat(s x, s y) -> if(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x),
                  mod_nat(0(), s x) -> 0(),
                   if(true(), x, y) -> x,
                  if(false(), x, y) -> y,
                minus_nat_s(x, 0()) -> x,
              minus_nat_s(s x, s y) -> minus_nat_s(x, y),
              minus_nat_s(0(), s y) -> 0(),
                minus_nat(s x, s y) -> minus_nat(x, y),
                minus_nat(s x, 0()) -> pos s x,
                minus_nat(0(), s y) -> neg s y,
                minus_nat(0(), 0()) -> pos 0(),
                   plus_nat(s x, y) -> s plus_nat(x, y),
                   plus_nat(0(), x) -> x}
     EDG:
      {(mod_int#(pos x, neg y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> minus_nat_s#(x, y))
       (mod_int#(pos x, neg y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> if#(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x))
       (mod_int#(pos x, neg y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> mod_nat#(minus_nat_s(x, y), s y))
       (mod_int#(neg x, neg y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> minus_nat_s#(x, y))
       (mod_int#(neg x, neg y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> if#(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x))
       (mod_int#(neg x, neg y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> mod_nat#(minus_nat_s(x, y), s y))
       (minus_int#(pos x, neg y) -> plus_nat#(x, y), plus_nat#(s x, y) -> plus_nat#(x, y))
       (mod_nat#(s x, s y) -> minus_nat_s#(x, y), minus_nat_s#(s x, s y) -> minus_nat_s#(x, y))
       (minus_nat#(s x, s y) -> minus_nat#(x, y), minus_nat#(s x, s y) -> minus_nat#(x, y))
       (Cond_eval#(true(), x) -> greater_int#(mod_int(minus_int(x, pos s 0()), pos s s 0()), pos 0()), greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y))
       (Cond_eval#(true(), x) -> greater_int#(mod_int(minus_int(x, pos s 0()), pos s s 0()), pos 0()), greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y))
       (Cond_eval#(true(), x) -> mod_int#(minus_int(x, pos s 0()), pos s s 0()), mod_int#(neg x, neg y) -> mod_nat#(x, y))
       (Cond_eval#(true(), x) -> mod_int#(minus_int(x, pos s 0()), pos s s 0()), mod_int#(neg x, pos y) -> mod_nat#(x, y))
       (Cond_eval#(true(), x) -> mod_int#(minus_int(x, pos s 0()), pos s s 0()), mod_int#(pos x, neg y) -> mod_nat#(x, y))
       (Cond_eval#(true(), x) -> mod_int#(minus_int(x, pos s 0()), pos s s 0()), mod_int#(pos x, pos y) -> mod_nat#(x, y))
       (eval# x -> greater_int#(x, pos 0()), greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y))
       (eval# x -> greater_int#(x, pos 0()), greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y))
       (eval# x -> mod_int#(x, pos s s 0()), mod_int#(neg x, neg y) -> mod_nat#(x, y))
       (eval# x -> mod_int#(x, pos s s 0()), mod_int#(neg x, pos y) -> mod_nat#(x, y))
       (eval# x -> mod_int#(x, pos s s 0()), mod_int#(pos x, neg y) -> mod_nat#(x, y))
       (eval# x -> mod_int#(x, pos s s 0()), mod_int#(pos x, pos y) -> mod_nat#(x, y))
       (greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y), greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y))
       (greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y), greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y))
       (mod_nat#(s x, s y) -> mod_nat#(minus_nat_s(x, y), s y), mod_nat#(s x, s y) -> minus_nat_s#(x, y))
       (mod_nat#(s x, s y) -> mod_nat#(minus_nat_s(x, y), s y), mod_nat#(s x, s y) -> if#(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x))
       (mod_nat#(s x, s y) -> mod_nat#(minus_nat_s(x, y), s y), mod_nat#(s x, s y) -> mod_nat#(minus_nat_s(x, y), s y))
       (Cond_eval#(true(), x) -> Cond_eval#(and(greater_int(mod_int(minus_int(x, pos s 0()), pos s s 0()), pos 0()), greater_int(minus_int(x, pos s 0()), pos 0())), minus_int(x, pos s 0())), Cond_eval#(true(), x) -> minus_int#(x, pos s 0()))
       (Cond_eval#(true(), x) -> Cond_eval#(and(greater_int(mod_int(minus_int(x, pos s 0()), pos s s 0()), pos 0()), greater_int(minus_int(x, pos s 0()), pos 0())), minus_int(x, pos s 0())), Cond_eval#(true(), x) -> mod_int#(minus_int(x, pos s 0()), pos s s 0()))
       (Cond_eval#(true(), x) -> Cond_eval#(and(greater_int(mod_int(minus_int(x, pos s 0()), pos s s 0()), pos 0()), greater_int(minus_int(x, pos s 0()), pos 0())), minus_int(x, pos s 0())), Cond_eval#(true(), x) -> greater_int#(minus_int(x, pos s 0()), pos 0()))
       (Cond_eval#(true(), x) -> Cond_eval#(and(greater_int(mod_int(minus_int(x, pos s 0()), pos s s 0()), pos 0()), greater_int(minus_int(x, pos s 0()), pos 0())), minus_int(x, pos s 0())), Cond_eval#(true(), x) -> greater_int#(mod_int(minus_int(x, pos s 0()), pos s s 0()), pos 0()))
       (Cond_eval#(true(), x) -> Cond_eval#(and(greater_int(mod_int(minus_int(x, pos s 0()), pos s s 0()), pos 0()), greater_int(minus_int(x, pos s 0()), pos 0())), minus_int(x, pos s 0())), Cond_eval#(true(), x) -> and#(greater_int(mod_int(minus_int(x, pos s 0()), pos s s 0()), pos 0()), greater_int(minus_int(x, pos s 0()), pos 0())))
       (Cond_eval#(true(), x) -> Cond_eval#(and(greater_int(mod_int(minus_int(x, pos s 0()), pos s s 0()), pos 0()), greater_int(minus_int(x, pos s 0()), pos 0())), minus_int(x, pos s 0())), Cond_eval#(true(), x) -> Cond_eval#(and(greater_int(mod_int(minus_int(x, pos s 0()), pos s s 0()), pos 0()), greater_int(minus_int(x, pos s 0()), pos 0())), minus_int(x, pos s 0())))
       (minus_int#(neg x, neg y) -> minus_nat#(y, x), minus_nat#(s x, s y) -> minus_nat#(x, y))
       (eval# x -> Cond_eval#(and(greater_int(mod_int(x, pos s s 0()), pos 0()), greater_int(x, pos 0())), x), Cond_eval#(true(), x) -> Cond_eval#(and(greater_int(mod_int(minus_int(x, pos s 0()), pos s s 0()), pos 0()), greater_int(minus_int(x, pos s 0()), pos 0())), minus_int(x, pos s 0())))
       (eval# x -> Cond_eval#(and(greater_int(mod_int(x, pos s s 0()), pos 0()), greater_int(x, pos 0())), x), Cond_eval#(true(), x) -> and#(greater_int(mod_int(minus_int(x, pos s 0()), pos s s 0()), pos 0()), greater_int(minus_int(x, pos s 0()), pos 0())))
       (eval# x -> Cond_eval#(and(greater_int(mod_int(x, pos s s 0()), pos 0()), greater_int(x, pos 0())), x), Cond_eval#(true(), x) -> greater_int#(mod_int(minus_int(x, pos s 0()), pos s s 0()), pos 0()))
       (eval# x -> Cond_eval#(and(greater_int(mod_int(x, pos s s 0()), pos 0()), greater_int(x, pos 0())), x), Cond_eval#(true(), x) -> greater_int#(minus_int(x, pos s 0()), pos 0()))
       (eval# x -> Cond_eval#(and(greater_int(mod_int(x, pos s s 0()), pos 0()), greater_int(x, pos 0())), x), Cond_eval#(true(), x) -> mod_int#(minus_int(x, pos s 0()), pos s s 0()))
       (eval# x -> Cond_eval#(and(greater_int(mod_int(x, pos s s 0()), pos 0()), greater_int(x, pos 0())), x), Cond_eval#(true(), x) -> minus_int#(x, pos s 0()))
       (greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y), greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y))
       (greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y), greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y))
       (eval# x -> greater_int#(mod_int(x, pos s s 0()), pos 0()), greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y))
       (eval# x -> greater_int#(mod_int(x, pos s s 0()), pos 0()), greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y))
       (Cond_eval#(true(), x) -> minus_int#(x, pos s 0()), minus_int#(pos x, pos y) -> minus_nat#(x, y))
       (Cond_eval#(true(), x) -> minus_int#(x, pos s 0()), minus_int#(pos x, neg y) -> plus_nat#(x, y))
       (Cond_eval#(true(), x) -> minus_int#(x, pos s 0()), minus_int#(neg x, pos y) -> plus_nat#(x, y))
       (Cond_eval#(true(), x) -> minus_int#(x, pos s 0()), minus_int#(neg x, neg y) -> minus_nat#(y, x))
       (Cond_eval#(true(), x) -> greater_int#(minus_int(x, pos s 0()), pos 0()), greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y))
       (Cond_eval#(true(), x) -> greater_int#(minus_int(x, pos s 0()), pos 0()), greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y))
       (plus_nat#(s x, y) -> plus_nat#(x, y), plus_nat#(s x, y) -> plus_nat#(x, y))
       (minus_nat_s#(s x, s y) -> minus_nat_s#(x, y), minus_nat_s#(s x, s y) -> minus_nat_s#(x, y))
       (minus_int#(neg x, pos y) -> plus_nat#(x, y), plus_nat#(s x, y) -> plus_nat#(x, y))
       (minus_int#(pos x, pos y) -> minus_nat#(x, y), minus_nat#(s x, s y) -> minus_nat#(x, y))
       (mod_int#(neg x, pos y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> mod_nat#(minus_nat_s(x, y), s y))
       (mod_int#(neg x, pos y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> if#(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x))
       (mod_int#(neg x, pos y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> minus_nat_s#(x, y))
       (mod_int#(pos x, pos y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> mod_nat#(minus_nat_s(x, y), s y))
       (mod_int#(pos x, pos y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> if#(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x))
       (mod_int#(pos x, pos y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> minus_nat_s#(x, y))}
      EDG:
       {(mod_int#(pos x, neg y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> minus_nat_s#(x, y))
        (mod_int#(pos x, neg y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> if#(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x))
        (mod_int#(pos x, neg y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> mod_nat#(minus_nat_s(x, y), s y))
        (mod_int#(neg x, neg y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> minus_nat_s#(x, y))
        (mod_int#(neg x, neg y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> if#(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x))
        (mod_int#(neg x, neg y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> mod_nat#(minus_nat_s(x, y), s y))
        (minus_int#(pos x, neg y) -> plus_nat#(x, y), plus_nat#(s x, y) -> plus_nat#(x, y))
        (mod_nat#(s x, s y) -> minus_nat_s#(x, y), minus_nat_s#(s x, s y) -> minus_nat_s#(x, y))
        (minus_nat#(s x, s y) -> minus_nat#(x, y), minus_nat#(s x, s y) -> minus_nat#(x, y))
        (Cond_eval#(true(), x) -> mod_int#(minus_int(x, pos s 0()), pos s s 0()), mod_int#(neg x, pos y) -> mod_nat#(x, y))
        (Cond_eval#(true(), x) -> mod_int#(minus_int(x, pos s 0()), pos s s 0()), mod_int#(pos x, pos y) -> mod_nat#(x, y))
        (eval# x -> mod_int#(x, pos s s 0()), mod_int#(neg x, pos y) -> mod_nat#(x, y))
        (eval# x -> mod_int#(x, pos s s 0()), mod_int#(pos x, pos y) -> mod_nat#(x, y))
        (greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y), greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y))
        (mod_nat#(s x, s y) -> mod_nat#(minus_nat_s(x, y), s y), mod_nat#(s x, s y) -> minus_nat_s#(x, y))
        (mod_nat#(s x, s y) -> mod_nat#(minus_nat_s(x, y), s y), mod_nat#(s x, s y) -> if#(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x))
        (mod_nat#(s x, s y) -> mod_nat#(minus_nat_s(x, y), s y), mod_nat#(s x, s y) -> mod_nat#(minus_nat_s(x, y), s y))
        (Cond_eval#(true(), x) -> Cond_eval#(and(greater_int(mod_int(minus_int(x, pos s 0()), pos s s 0()), pos 0()), greater_int(minus_int(x, pos s 0()), pos 0())), minus_int(x, pos s 0())), Cond_eval#(true(), x) -> minus_int#(x, pos s 0()))
        (Cond_eval#(true(), x) -> Cond_eval#(and(greater_int(mod_int(minus_int(x, pos s 0()), pos s s 0()), pos 0()), greater_int(minus_int(x, pos s 0()), pos 0())), minus_int(x, pos s 0())), Cond_eval#(true(), x) -> mod_int#(minus_int(x, pos s 0()), pos s s 0()))
        (Cond_eval#(true(), x) -> Cond_eval#(and(greater_int(mod_int(minus_int(x, pos s 0()), pos s s 0()), pos 0()), greater_int(minus_int(x, pos s 0()), pos 0())), minus_int(x, pos s 0())), Cond_eval#(true(), x) -> greater_int#(minus_int(x, pos s 0()), pos 0()))
        (Cond_eval#(true(), x) -> Cond_eval#(and(greater_int(mod_int(minus_int(x, pos s 0()), pos s s 0()), pos 0()), greater_int(minus_int(x, pos s 0()), pos 0())), minus_int(x, pos s 0())), Cond_eval#(true(), x) -> greater_int#(mod_int(minus_int(x, pos s 0()), pos s s 0()), pos 0()))
        (Cond_eval#(true(), x) -> Cond_eval#(and(greater_int(mod_int(minus_int(x, pos s 0()), pos s s 0()), pos 0()), greater_int(minus_int(x, pos s 0()), pos 0())), minus_int(x, pos s 0())), Cond_eval#(true(), x) -> and#(greater_int(mod_int(minus_int(x, pos s 0()), pos s s 0()), pos 0()), greater_int(minus_int(x, pos s 0()), pos 0())))
        (Cond_eval#(true(), x) -> Cond_eval#(and(greater_int(mod_int(minus_int(x, pos s 0()), pos s s 0()), pos 0()), greater_int(minus_int(x, pos s 0()), pos 0())), minus_int(x, pos s 0())), Cond_eval#(true(), x) -> Cond_eval#(and(greater_int(mod_int(minus_int(x, pos s 0()), pos s s 0()), pos 0()), greater_int(minus_int(x, pos s 0()), pos 0())), minus_int(x, pos s 0())))
        (minus_int#(neg x, neg y) -> minus_nat#(y, x), minus_nat#(s x, s y) -> minus_nat#(x, y))
        (eval# x -> Cond_eval#(and(greater_int(mod_int(x, pos s s 0()), pos 0()), greater_int(x, pos 0())), x), Cond_eval#(true(), x) -> Cond_eval#(and(greater_int(mod_int(minus_int(x, pos s 0()), pos s s 0()), pos 0()), greater_int(minus_int(x, pos s 0()), pos 0())), minus_int(x, pos s 0())))
        (eval# x -> Cond_eval#(and(greater_int(mod_int(x, pos s s 0()), pos 0()), greater_int(x, pos 0())), x), Cond_eval#(true(), x) -> and#(greater_int(mod_int(minus_int(x, pos s 0()), pos s s 0()), pos 0()), greater_int(minus_int(x, pos s 0()), pos 0())))
        (eval# x -> Cond_eval#(and(greater_int(mod_int(x, pos s s 0()), pos 0()), greater_int(x, pos 0())), x), Cond_eval#(true(), x) -> greater_int#(mod_int(minus_int(x, pos s 0()), pos s s 0()), pos 0()))
        (eval# x -> Cond_eval#(and(greater_int(mod_int(x, pos s s 0()), pos 0()), greater_int(x, pos 0())), x), Cond_eval#(true(), x) -> greater_int#(minus_int(x, pos s 0()), pos 0()))
        (eval# x -> Cond_eval#(and(greater_int(mod_int(x, pos s s 0()), pos 0()), greater_int(x, pos 0())), x), Cond_eval#(true(), x) -> mod_int#(minus_int(x, pos s 0()), pos s s 0()))
        (eval# x -> Cond_eval#(and(greater_int(mod_int(x, pos s s 0()), pos 0()), greater_int(x, pos 0())), x), Cond_eval#(true(), x) -> minus_int#(x, pos s 0()))
        (greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y), greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y))
        (Cond_eval#(true(), x) -> minus_int#(x, pos s 0()), minus_int#(pos x, pos y) -> minus_nat#(x, y))
        (Cond_eval#(true(), x) -> minus_int#(x, pos s 0()), minus_int#(neg x, pos y) -> plus_nat#(x, y))
        (plus_nat#(s x, y) -> plus_nat#(x, y), plus_nat#(s x, y) -> plus_nat#(x, y))
        (minus_nat_s#(s x, s y) -> minus_nat_s#(x, y), minus_nat_s#(s x, s y) -> minus_nat_s#(x, y))
        (minus_int#(neg x, pos y) -> plus_nat#(x, y), plus_nat#(s x, y) -> plus_nat#(x, y))
        (minus_int#(pos x, pos y) -> minus_nat#(x, y), minus_nat#(s x, s y) -> minus_nat#(x, y))
        (mod_int#(neg x, pos y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> mod_nat#(minus_nat_s(x, y), s y))
        (mod_int#(neg x, pos y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> if#(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x))
        (mod_int#(neg x, pos y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> minus_nat_s#(x, y))
        (mod_int#(pos x, pos y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> mod_nat#(minus_nat_s(x, y), s y))
        (mod_int#(pos x, pos y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> if#(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x))
        (mod_int#(pos x, pos y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> minus_nat_s#(x, y))}
       SCCS (7):
        Scc:
         {plus_nat#(s x, y) -> plus_nat#(x, y)}
        Scc:
         {minus_nat#(s x, s y) -> minus_nat#(x, y)}
        Scc:
         {minus_nat_s#(s x, s y) -> minus_nat_s#(x, y)}
        Scc:
         {mod_nat#(s x, s y) -> mod_nat#(minus_nat_s(x, y), s y)}
        Scc:
         {greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y)}
        Scc:
         {greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y)}
        Scc:
         {Cond_eval#(true(), x) -> Cond_eval#(and(greater_int(mod_int(minus_int(x, pos s 0()), pos s s 0()), pos 0()), greater_int(minus_int(x, pos s 0()), pos 0())), minus_int(x, pos s 0()))}
        SCC:
         Strict:
          {plus_nat#(s x, y) -> plus_nat#(x, y)}
         Weak:
         {         Cond_eval(true(), x) -> Cond_eval(and(greater_int(mod_int(minus_int(x, pos s 0()), pos s s 0()), pos 0()), greater_int(minus_int(x, pos s 0()), pos 0())), minus_int(x, pos s 0())),
                    and(true(), true()) -> true(),
                   and(true(), false()) -> false(),
                   and(false(), true()) -> false(),
                  and(false(), false()) -> false(),
          greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
          greater_int(pos s x, pos 0()) -> true(),
          greater_int(pos s x, neg s y) -> true(),
          greater_int(pos s x, neg 0()) -> true(),
          greater_int(pos 0(), pos s y) -> false(),
          greater_int(pos 0(), pos 0()) -> false(),
          greater_int(pos 0(), neg s y) -> true(),
          greater_int(pos 0(), neg 0()) -> false(),
          greater_int(neg s x, pos s y) -> false(),
          greater_int(neg s x, pos 0()) -> false(),
          greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
          greater_int(neg s x, neg 0()) -> false(),
          greater_int(neg 0(), pos s y) -> false(),
          greater_int(neg 0(), pos 0()) -> false(),
          greater_int(neg 0(), neg s y) -> true(),
          greater_int(neg 0(), neg 0()) -> false(),
                  mod_int(pos x, pos y) -> pos mod_nat(x, y),
                  mod_int(pos x, neg y) -> pos mod_nat(x, y),
                  mod_int(neg x, pos y) -> neg mod_nat(x, y),
                  mod_int(neg x, neg y) -> neg mod_nat(x, y),
                                 eval x -> Cond_eval(and(greater_int(mod_int(x, pos s s 0()), pos 0()), greater_int(x, pos 0())), x),
                minus_int(pos x, pos y) -> minus_nat(x, y),
                minus_int(pos x, neg y) -> pos plus_nat(x, y),
                minus_int(neg x, pos y) -> neg plus_nat(x, y),
                minus_int(neg x, neg y) -> minus_nat(y, x),
                      mod_nat(s x, s y) -> if(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x),
                      mod_nat(0(), s x) -> 0(),
                       if(true(), x, y) -> x,
                      if(false(), x, y) -> y,
                    minus_nat_s(x, 0()) -> x,
                  minus_nat_s(s x, s y) -> minus_nat_s(x, y),
                  minus_nat_s(0(), s y) -> 0(),
                    minus_nat(s x, s y) -> minus_nat(x, y),
                    minus_nat(s x, 0()) -> pos s x,
                    minus_nat(0(), s y) -> neg s y,
                    minus_nat(0(), 0()) -> pos 0(),
                       plus_nat(s x, y) -> s plus_nat(x, y),
                       plus_nat(0(), x) -> x}
         SPSC:
          Simple Projection:
           pi(plus_nat#) = 0
          Strict:
           {}
          Qed
        SCC:
         Strict:
          {minus_nat#(s x, s y) -> minus_nat#(x, y)}
         Weak:
         {         Cond_eval(true(), x) -> Cond_eval(and(greater_int(mod_int(minus_int(x, pos s 0()), pos s s 0()), pos 0()), greater_int(minus_int(x, pos s 0()), pos 0())), minus_int(x, pos s 0())),
                    and(true(), true()) -> true(),
                   and(true(), false()) -> false(),
                   and(false(), true()) -> false(),
                  and(false(), false()) -> false(),
          greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
          greater_int(pos s x, pos 0()) -> true(),
          greater_int(pos s x, neg s y) -> true(),
          greater_int(pos s x, neg 0()) -> true(),
          greater_int(pos 0(), pos s y) -> false(),
          greater_int(pos 0(), pos 0()) -> false(),
          greater_int(pos 0(), neg s y) -> true(),
          greater_int(pos 0(), neg 0()) -> false(),
          greater_int(neg s x, pos s y) -> false(),
          greater_int(neg s x, pos 0()) -> false(),
          greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
          greater_int(neg s x, neg 0()) -> false(),
          greater_int(neg 0(), pos s y) -> false(),
          greater_int(neg 0(), pos 0()) -> false(),
          greater_int(neg 0(), neg s y) -> true(),
          greater_int(neg 0(), neg 0()) -> false(),
                  mod_int(pos x, pos y) -> pos mod_nat(x, y),
                  mod_int(pos x, neg y) -> pos mod_nat(x, y),
                  mod_int(neg x, pos y) -> neg mod_nat(x, y),
                  mod_int(neg x, neg y) -> neg mod_nat(x, y),
                                 eval x -> Cond_eval(and(greater_int(mod_int(x, pos s s 0()), pos 0()), greater_int(x, pos 0())), x),
                minus_int(pos x, pos y) -> minus_nat(x, y),
                minus_int(pos x, neg y) -> pos plus_nat(x, y),
                minus_int(neg x, pos y) -> neg plus_nat(x, y),
                minus_int(neg x, neg y) -> minus_nat(y, x),
                      mod_nat(s x, s y) -> if(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x),
                      mod_nat(0(), s x) -> 0(),
                       if(true(), x, y) -> x,
                      if(false(), x, y) -> y,
                    minus_nat_s(x, 0()) -> x,
                  minus_nat_s(s x, s y) -> minus_nat_s(x, y),
                  minus_nat_s(0(), s y) -> 0(),
                    minus_nat(s x, s y) -> minus_nat(x, y),
                    minus_nat(s x, 0()) -> pos s x,
                    minus_nat(0(), s y) -> neg s y,
                    minus_nat(0(), 0()) -> pos 0(),
                       plus_nat(s x, y) -> s plus_nat(x, y),
                       plus_nat(0(), x) -> x}
         SPSC:
          Simple Projection:
           pi(minus_nat#) = 1
          Strict:
           {}
          Qed
        SCC:
         Strict:
          {minus_nat_s#(s x, s y) -> minus_nat_s#(x, y)}
         Weak:
         {         Cond_eval(true(), x) -> Cond_eval(and(greater_int(mod_int(minus_int(x, pos s 0()), pos s s 0()), pos 0()), greater_int(minus_int(x, pos s 0()), pos 0())), minus_int(x, pos s 0())),
                    and(true(), true()) -> true(),
                   and(true(), false()) -> false(),
                   and(false(), true()) -> false(),
                  and(false(), false()) -> false(),
          greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
          greater_int(pos s x, pos 0()) -> true(),
          greater_int(pos s x, neg s y) -> true(),
          greater_int(pos s x, neg 0()) -> true(),
          greater_int(pos 0(), pos s y) -> false(),
          greater_int(pos 0(), pos 0()) -> false(),
          greater_int(pos 0(), neg s y) -> true(),
          greater_int(pos 0(), neg 0()) -> false(),
          greater_int(neg s x, pos s y) -> false(),
          greater_int(neg s x, pos 0()) -> false(),
          greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
          greater_int(neg s x, neg 0()) -> false(),
          greater_int(neg 0(), pos s y) -> false(),
          greater_int(neg 0(), pos 0()) -> false(),
          greater_int(neg 0(), neg s y) -> true(),
          greater_int(neg 0(), neg 0()) -> false(),
                  mod_int(pos x, pos y) -> pos mod_nat(x, y),
                  mod_int(pos x, neg y) -> pos mod_nat(x, y),
                  mod_int(neg x, pos y) -> neg mod_nat(x, y),
                  mod_int(neg x, neg y) -> neg mod_nat(x, y),
                                 eval x -> Cond_eval(and(greater_int(mod_int(x, pos s s 0()), pos 0()), greater_int(x, pos 0())), x),
                minus_int(pos x, pos y) -> minus_nat(x, y),
                minus_int(pos x, neg y) -> pos plus_nat(x, y),
                minus_int(neg x, pos y) -> neg plus_nat(x, y),
                minus_int(neg x, neg y) -> minus_nat(y, x),
                      mod_nat(s x, s y) -> if(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x),
                      mod_nat(0(), s x) -> 0(),
                       if(true(), x, y) -> x,
                      if(false(), x, y) -> y,
                    minus_nat_s(x, 0()) -> x,
                  minus_nat_s(s x, s y) -> minus_nat_s(x, y),
                  minus_nat_s(0(), s y) -> 0(),
                    minus_nat(s x, s y) -> minus_nat(x, y),
                    minus_nat(s x, 0()) -> pos s x,
                    minus_nat(0(), s y) -> neg s y,
                    minus_nat(0(), 0()) -> pos 0(),
                       plus_nat(s x, y) -> s plus_nat(x, y),
                       plus_nat(0(), x) -> x}
         SPSC:
          Simple Projection:
           pi(minus_nat_s#) = 1
          Strict:
           {}
          Qed
        SCC:
         Strict:
          {mod_nat#(s x, s y) -> mod_nat#(minus_nat_s(x, y), s y)}
         Weak:
         {         Cond_eval(true(), x) -> Cond_eval(and(greater_int(mod_int(minus_int(x, pos s 0()), pos s s 0()), pos 0()), greater_int(minus_int(x, pos s 0()), pos 0())), minus_int(x, pos s 0())),
                    and(true(), true()) -> true(),
                   and(true(), false()) -> false(),
                   and(false(), true()) -> false(),
                  and(false(), false()) -> false(),
          greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
          greater_int(pos s x, pos 0()) -> true(),
          greater_int(pos s x, neg s y) -> true(),
          greater_int(pos s x, neg 0()) -> true(),
          greater_int(pos 0(), pos s y) -> false(),
          greater_int(pos 0(), pos 0()) -> false(),
          greater_int(pos 0(), neg s y) -> true(),
          greater_int(pos 0(), neg 0()) -> false(),
          greater_int(neg s x, pos s y) -> false(),
          greater_int(neg s x, pos 0()) -> false(),
          greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
          greater_int(neg s x, neg 0()) -> false(),
          greater_int(neg 0(), pos s y) -> false(),
          greater_int(neg 0(), pos 0()) -> false(),
          greater_int(neg 0(), neg s y) -> true(),
          greater_int(neg 0(), neg 0()) -> false(),
                  mod_int(pos x, pos y) -> pos mod_nat(x, y),
                  mod_int(pos x, neg y) -> pos mod_nat(x, y),
                  mod_int(neg x, pos y) -> neg mod_nat(x, y),
                  mod_int(neg x, neg y) -> neg mod_nat(x, y),
                                 eval x -> Cond_eval(and(greater_int(mod_int(x, pos s s 0()), pos 0()), greater_int(x, pos 0())), x),
                minus_int(pos x, pos y) -> minus_nat(x, y),
                minus_int(pos x, neg y) -> pos plus_nat(x, y),
                minus_int(neg x, pos y) -> neg plus_nat(x, y),
                minus_int(neg x, neg y) -> minus_nat(y, x),
                      mod_nat(s x, s y) -> if(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x),
                      mod_nat(0(), s x) -> 0(),
                       if(true(), x, y) -> x,
                      if(false(), x, y) -> y,
                    minus_nat_s(x, 0()) -> x,
                  minus_nat_s(s x, s y) -> minus_nat_s(x, y),
                  minus_nat_s(0(), s y) -> 0(),
                    minus_nat(s x, s y) -> minus_nat(x, y),
                    minus_nat(s x, 0()) -> pos s x,
                    minus_nat(0(), s y) -> neg s y,
                    minus_nat(0(), 0()) -> pos 0(),
                       plus_nat(s x, y) -> s plus_nat(x, y),
                       plus_nat(0(), x) -> x}
         UR:
          {  minus_nat_s(x, 0()) -> x,
           minus_nat_s(s x, s y) -> minus_nat_s(x, y),
           minus_nat_s(0(), s y) -> 0(),
                         a(z, w) -> z,
                         a(z, w) -> w}
          ARCTIC:
           Argument Filtering:
            pi(a) = [0,1], pi(minus_nat_s) = [0], pi(mod_nat#) = [0], pi(0) = [], pi(s) = [0]
           Usable Rules:
            {  minus_nat_s(x, 0()) -> x,
             minus_nat_s(s x, s y) -> minus_nat_s(x, y),
             minus_nat_s(0(), s y) -> 0()}
           Interpretation:
            [minus_nat_s](x0) = 1x0 + 2,
            
            [s](x0) = 2x0 + 3,
            
            [0] = 0,
            
            [mod_nat#](x0) = 4x0 + 0
           Strict:
            {}
           Weak:
            {  minus_nat_s(x, 0()) -> x,
             minus_nat_s(s x, s y) -> minus_nat_s(x, y),
             minus_nat_s(0(), s y) -> 0(),
                           a(z, w) -> z,
                           a(z, w) -> w}
           Qed
        SCC:
         Strict:
          {greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y)}
         Weak:
         {         Cond_eval(true(), x) -> Cond_eval(and(greater_int(mod_int(minus_int(x, pos s 0()), pos s s 0()), pos 0()), greater_int(minus_int(x, pos s 0()), pos 0())), minus_int(x, pos s 0())),
                    and(true(), true()) -> true(),
                   and(true(), false()) -> false(),
                   and(false(), true()) -> false(),
                  and(false(), false()) -> false(),
          greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
          greater_int(pos s x, pos 0()) -> true(),
          greater_int(pos s x, neg s y) -> true(),
          greater_int(pos s x, neg 0()) -> true(),
          greater_int(pos 0(), pos s y) -> false(),
          greater_int(pos 0(), pos 0()) -> false(),
          greater_int(pos 0(), neg s y) -> true(),
          greater_int(pos 0(), neg 0()) -> false(),
          greater_int(neg s x, pos s y) -> false(),
          greater_int(neg s x, pos 0()) -> false(),
          greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
          greater_int(neg s x, neg 0()) -> false(),
          greater_int(neg 0(), pos s y) -> false(),
          greater_int(neg 0(), pos 0()) -> false(),
          greater_int(neg 0(), neg s y) -> true(),
          greater_int(neg 0(), neg 0()) -> false(),
                  mod_int(pos x, pos y) -> pos mod_nat(x, y),
                  mod_int(pos x, neg y) -> pos mod_nat(x, y),
                  mod_int(neg x, pos y) -> neg mod_nat(x, y),
                  mod_int(neg x, neg y) -> neg mod_nat(x, y),
                                 eval x -> Cond_eval(and(greater_int(mod_int(x, pos s s 0()), pos 0()), greater_int(x, pos 0())), x),
                minus_int(pos x, pos y) -> minus_nat(x, y),
                minus_int(pos x, neg y) -> pos plus_nat(x, y),
                minus_int(neg x, pos y) -> neg plus_nat(x, y),
                minus_int(neg x, neg y) -> minus_nat(y, x),
                      mod_nat(s x, s y) -> if(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x),
                      mod_nat(0(), s x) -> 0(),
                       if(true(), x, y) -> x,
                      if(false(), x, y) -> y,
                    minus_nat_s(x, 0()) -> x,
                  minus_nat_s(s x, s y) -> minus_nat_s(x, y),
                  minus_nat_s(0(), s y) -> 0(),
                    minus_nat(s x, s y) -> minus_nat(x, y),
                    minus_nat(s x, 0()) -> pos s x,
                    minus_nat(0(), s y) -> neg s y,
                    minus_nat(0(), 0()) -> pos 0(),
                       plus_nat(s x, y) -> s plus_nat(x, y),
                       plus_nat(0(), x) -> x}
         UR:
          {}
          ARCTIC:
           Argument Filtering:
            pi(neg) = 0, pi(s) = [0], pi(greater_int#) = 1
           Usable Rules:
            {}
           Interpretation:
            [s](x0) = 1x0
           Strict:
            {}
           Weak:
            {}
           Qed
        SCC:
         Strict:
          {greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y)}
         Weak:
         {         Cond_eval(true(), x) -> Cond_eval(and(greater_int(mod_int(minus_int(x, pos s 0()), pos s s 0()), pos 0()), greater_int(minus_int(x, pos s 0()), pos 0())), minus_int(x, pos s 0())),
                    and(true(), true()) -> true(),
                   and(true(), false()) -> false(),
                   and(false(), true()) -> false(),
                  and(false(), false()) -> false(),
          greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
          greater_int(pos s x, pos 0()) -> true(),
          greater_int(pos s x, neg s y) -> true(),
          greater_int(pos s x, neg 0()) -> true(),
          greater_int(pos 0(), pos s y) -> false(),
          greater_int(pos 0(), pos 0()) -> false(),
          greater_int(pos 0(), neg s y) -> true(),
          greater_int(pos 0(), neg 0()) -> false(),
          greater_int(neg s x, pos s y) -> false(),
          greater_int(neg s x, pos 0()) -> false(),
          greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
          greater_int(neg s x, neg 0()) -> false(),
          greater_int(neg 0(), pos s y) -> false(),
          greater_int(neg 0(), pos 0()) -> false(),
          greater_int(neg 0(), neg s y) -> true(),
          greater_int(neg 0(), neg 0()) -> false(),
                  mod_int(pos x, pos y) -> pos mod_nat(x, y),
                  mod_int(pos x, neg y) -> pos mod_nat(x, y),
                  mod_int(neg x, pos y) -> neg mod_nat(x, y),
                  mod_int(neg x, neg y) -> neg mod_nat(x, y),
                                 eval x -> Cond_eval(and(greater_int(mod_int(x, pos s s 0()), pos 0()), greater_int(x, pos 0())), x),
                minus_int(pos x, pos y) -> minus_nat(x, y),
                minus_int(pos x, neg y) -> pos plus_nat(x, y),
                minus_int(neg x, pos y) -> neg plus_nat(x, y),
                minus_int(neg x, neg y) -> minus_nat(y, x),
                      mod_nat(s x, s y) -> if(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x),
                      mod_nat(0(), s x) -> 0(),
                       if(true(), x, y) -> x,
                      if(false(), x, y) -> y,
                    minus_nat_s(x, 0()) -> x,
                  minus_nat_s(s x, s y) -> minus_nat_s(x, y),
                  minus_nat_s(0(), s y) -> 0(),
                    minus_nat(s x, s y) -> minus_nat(x, y),
                    minus_nat(s x, 0()) -> pos s x,
                    minus_nat(0(), s y) -> neg s y,
                    minus_nat(0(), 0()) -> pos 0(),
                       plus_nat(s x, y) -> s plus_nat(x, y),
                       plus_nat(0(), x) -> x}
         UR:
          {}
          ARCTIC:
           Argument Filtering:
            pi(s) = [0], pi(pos) = [0], pi(greater_int#) = [1]
           Usable Rules:
            {}
           Interpretation:
            [s](x0) = 5x0 + 9,
            
            [pos](x0) = -4x0 + 0,
            
            [greater_int#](x0) = -4x0 + 0
           Strict:
            {}
           Weak:
            {}
           Qed
        SCC:
         Strict:
          {Cond_eval#(true(), x) -> Cond_eval#(and(greater_int(mod_int(minus_int(x, pos s 0()), pos s s 0()), pos 0()), greater_int(minus_int(x, pos s 0()), pos 0())), minus_int(x, pos s 0()))}
         Weak:
         {         Cond_eval(true(), x) -> Cond_eval(and(greater_int(mod_int(minus_int(x, pos s 0()), pos s s 0()), pos 0()), greater_int(minus_int(x, pos s 0()), pos 0())), minus_int(x, pos s 0())),
                    and(true(), true()) -> true(),
                   and(true(), false()) -> false(),
                   and(false(), true()) -> false(),
                  and(false(), false()) -> false(),
          greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
          greater_int(pos s x, pos 0()) -> true(),
          greater_int(pos s x, neg s y) -> true(),
          greater_int(pos s x, neg 0()) -> true(),
          greater_int(pos 0(), pos s y) -> false(),
          greater_int(pos 0(), pos 0()) -> false(),
          greater_int(pos 0(), neg s y) -> true(),
          greater_int(pos 0(), neg 0()) -> false(),
          greater_int(neg s x, pos s y) -> false(),
          greater_int(neg s x, pos 0()) -> false(),
          greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
          greater_int(neg s x, neg 0()) -> false(),
          greater_int(neg 0(), pos s y) -> false(),
          greater_int(neg 0(), pos 0()) -> false(),
          greater_int(neg 0(), neg s y) -> true(),
          greater_int(neg 0(), neg 0()) -> false(),
                  mod_int(pos x, pos y) -> pos mod_nat(x, y),
                  mod_int(pos x, neg y) -> pos mod_nat(x, y),
                  mod_int(neg x, pos y) -> neg mod_nat(x, y),
                  mod_int(neg x, neg y) -> neg mod_nat(x, y),
                                 eval x -> Cond_eval(and(greater_int(mod_int(x, pos s s 0()), pos 0()), greater_int(x, pos 0())), x),
                minus_int(pos x, pos y) -> minus_nat(x, y),
                minus_int(pos x, neg y) -> pos plus_nat(x, y),
                minus_int(neg x, pos y) -> neg plus_nat(x, y),
                minus_int(neg x, neg y) -> minus_nat(y, x),
                      mod_nat(s x, s y) -> if(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x),
                      mod_nat(0(), s x) -> 0(),
                       if(true(), x, y) -> x,
                      if(false(), x, y) -> y,
                    minus_nat_s(x, 0()) -> x,
                  minus_nat_s(s x, s y) -> minus_nat_s(x, y),
                  minus_nat_s(0(), s y) -> 0(),
                    minus_nat(s x, s y) -> minus_nat(x, y),
                    minus_nat(s x, 0()) -> pos s x,
                    minus_nat(0(), s y) -> neg s y,
                    minus_nat(0(), 0()) -> pos 0(),
                       plus_nat(s x, y) -> s plus_nat(x, y),
                       plus_nat(0(), x) -> x}
         UR:
          {          and(true(), true()) -> true(),
                    and(true(), false()) -> false(),
                    and(false(), true()) -> false(),
                   and(false(), false()) -> false(),
           greater_int(pos s x, pos 0()) -> true(),
           greater_int(pos 0(), pos 0()) -> false(),
           greater_int(neg s x, pos 0()) -> false(),
           greater_int(neg 0(), pos 0()) -> false(),
                   mod_int(pos x, pos y) -> pos mod_nat(x, y),
                   mod_int(neg x, pos y) -> neg mod_nat(x, y),
                 minus_int(pos x, pos y) -> minus_nat(x, y),
                 minus_int(neg x, pos y) -> neg plus_nat(x, y),
                       mod_nat(s x, s y) -> if(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x),
                       mod_nat(0(), s x) -> 0(),
                     minus_nat_s(x, 0()) -> x,
                   minus_nat_s(s x, s y) -> minus_nat_s(x, y),
                   minus_nat_s(0(), s y) -> 0(),
                     minus_nat(s x, s y) -> minus_nat(x, y),
                     minus_nat(s x, 0()) -> pos s x,
                     minus_nat(0(), s y) -> neg s y,
                     minus_nat(0(), 0()) -> pos 0(),
                        plus_nat(s x, y) -> s plus_nat(x, y),
                        plus_nat(0(), x) -> x,
                                 a(v, u) -> v,
                                 a(v, u) -> u}
          POLY:
           Mode: weak, max_in=7, output_bits=8, dnum=2, ur=true
           Interpretation:
            [if](x0, x1, x2) = 0,
            
            [and](x0, x1) = 1 / 2x0 + 1 / 2,
            
            [greater_int](x0, x1) = 1 / 2x0,
            
            [mod_int](x0, x1) = 1,
            
            [minus_int](x0, x1) = 1,
            
            [mod_nat](x0, x1) = 0,
            
            [greatereq_int](x0, x1) = x0 + 1 / 2x1 + 1 / 2,
            
            [minus_nat_s](x0, x1) = 2x0,
            
            [minus_nat](x0, x1) = 0,
            
            [plus_nat](x0, x1) = x0,
            
            [a](x0, x1) = 0,
            
            [pos](x0) = 2x0 + 1,
            
            [s](x0) = 7 / 2,
            
            [neg](x0) = 0,
            
            [0] = 0,
            
            [true] = 1,
            
            [false] = 0,
            
            [Cond_eval#](x0, x1) = 1 / 2x0
           Strict:
            Cond_eval#(true(), x) -> Cond_eval#(and(greater_int(mod_int(minus_int(x, pos s 0()), pos s s 0()), pos 0()), greater_int(minus_int(x, pos s 0()), pos 0())), minus_int(x, pos s 0()))
            1/2 + 0x >= 3/8 + 0x
           Weak:
            
          Qed