Time: 5.254940
TRS:
 {                   eval(x, y) -> Cond_eval(and(and(greater_int(x, pos 0()), not equal_int(x, pos 0())), lesseq_int(x, y)), x, y),
                     eval(x, y) -> Cond_eval1(and(and(greater_int(x, pos 0()), not equal_int(x, pos 0())), greater_int(x, y)), x, y),
        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),
        Cond_eval(true(), x, y) -> eval(minus_int(x, pos s 0()), y),
            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(),
                     not true() -> false(),
                    not false() -> true(),
    equal_int(pos s x, pos s y) -> equal_int(pos x, pos y),
    equal_int(pos s x, pos 0()) -> false(),
    equal_int(pos s x, neg s y) -> false(),
    equal_int(pos s x, neg 0()) -> false(),
    equal_int(pos 0(), pos s y) -> false(),
    equal_int(pos 0(), pos 0()) -> true(),
    equal_int(pos 0(), neg s y) -> false(),
    equal_int(pos 0(), neg 0()) -> true(),
    equal_int(neg s x, pos s y) -> false(),
    equal_int(neg s x, pos 0()) -> false(),
    equal_int(neg s x, neg s y) -> equal_int(neg x, neg y),
    equal_int(neg s x, neg 0()) -> false(),
    equal_int(neg 0(), pos s y) -> false(),
    equal_int(neg 0(), pos 0()) -> true(),
    equal_int(neg 0(), neg s y) -> false(),
    equal_int(neg 0(), neg 0()) -> true(),
     lesseq_int(pos x, neg s y) -> false(),
   lesseq_int(pos s x, pos s y) -> lesseq_int(pos x, pos y),
   lesseq_int(pos s x, pos 0()) -> false(),
     lesseq_int(pos s x, neg y) -> false(),
     lesseq_int(pos 0(), pos y) -> true(),
   lesseq_int(pos 0(), neg 0()) -> true(),
       lesseq_int(neg x, pos y) -> true(),
     lesseq_int(neg x, neg 0()) -> true(),
   lesseq_int(neg s x, neg s y) -> lesseq_int(neg x, neg y),
   lesseq_int(neg 0(), neg s y) -> false(),
       Cond_eval1(true(), x, y) -> eval(y, y),
            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:
   {                   eval(x, y) -> Cond_eval(and(and(greater_int(x, pos 0()), not equal_int(x, pos 0())), lesseq_int(x, y)), x, y),
                       eval(x, y) -> Cond_eval1(and(and(greater_int(x, pos 0()), not equal_int(x, pos 0())), greater_int(x, y)), x, y),
          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),
          Cond_eval(true(), x, y) -> eval(minus_int(x, pos s 0()), y),
              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(),
                       not true() -> false(),
                      not false() -> true(),
      equal_int(pos s x, pos s y) -> equal_int(pos x, pos y),
      equal_int(pos s x, pos 0()) -> false(),
      equal_int(pos s x, neg s y) -> false(),
      equal_int(pos s x, neg 0()) -> false(),
      equal_int(pos 0(), pos s y) -> false(),
      equal_int(pos 0(), pos 0()) -> true(),
      equal_int(pos 0(), neg s y) -> false(),
      equal_int(pos 0(), neg 0()) -> true(),
      equal_int(neg s x, pos s y) -> false(),
      equal_int(neg s x, pos 0()) -> false(),
      equal_int(neg s x, neg s y) -> equal_int(neg x, neg y),
      equal_int(neg s x, neg 0()) -> false(),
      equal_int(neg 0(), pos s y) -> false(),
      equal_int(neg 0(), pos 0()) -> true(),
      equal_int(neg 0(), neg s y) -> false(),
      equal_int(neg 0(), neg 0()) -> true(),
       lesseq_int(pos x, neg s y) -> false(),
     lesseq_int(pos s x, pos s y) -> lesseq_int(pos x, pos y),
     lesseq_int(pos s x, pos 0()) -> false(),
       lesseq_int(pos s x, neg y) -> false(),
       lesseq_int(pos 0(), pos y) -> true(),
     lesseq_int(pos 0(), neg 0()) -> true(),
         lesseq_int(neg x, pos y) -> true(),
       lesseq_int(neg x, neg 0()) -> true(),
     lesseq_int(neg s x, neg s y) -> lesseq_int(neg x, neg y),
     lesseq_int(neg 0(), neg s y) -> false(),
         Cond_eval1(true(), x, y) -> eval(y, y),
              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}
  Fail