Time: 5.127839
TRS:
 {             cond(true(), x, y) -> pos s 0(),
              cond(false(), x, y) -> mult_int(pos s s 0(), log(x, mult_int(y, y))),
           mult_int(pos x, pos y) -> pos mult_nat(x, y),
           mult_int(pos x, neg y) -> neg mult_nat(x, y),
           mult_int(neg x, pos y) -> neg mult_nat(x, y),
           mult_int(neg x, neg y) -> pos mult_nat(x, y),
                        log(x, y) -> logNat(and(greatereq_int(x, pos 0()), greatereq_int(y, pos s s 0())), x, y),
       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(),
             logNat(true(), x, y) -> cond(lesseq_int(x, y), x, y),
              and(true(), true()) -> true(),
             and(true(), false()) -> false(),
             and(false(), true()) -> false(),
            and(false(), false()) -> false(),
    greatereq_int(pos x, pos 0()) -> true(),
      greatereq_int(pos x, neg y) -> true(),
  greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
  greatereq_int(pos 0(), pos s y) -> false(),
    greatereq_int(neg x, pos s y) -> false(),
  greatereq_int(neg s x, pos 0()) -> false(),
  greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y),
  greatereq_int(neg s x, neg 0()) -> false(),
  greatereq_int(neg 0(), pos 0()) -> true(),
    greatereq_int(neg 0(), neg y) -> true(),
               mult_nat(s x, s y) -> plus_nat(mult_nat(x, s y), s y),
               mult_nat(s x, 0()) -> 0(),
                 mult_nat(0(), y) -> 0(),
                 plus_nat(s x, y) -> s plus_nat(x, y),
                 plus_nat(0(), x) -> x}
 SRS: We consider a TRS.
  Trs:
   {             cond(true(), x, y) -> pos s 0(),
                cond(false(), x, y) -> mult_int(pos s s 0(), log(x, mult_int(y, y))),
             mult_int(pos x, pos y) -> pos mult_nat(x, y),
             mult_int(pos x, neg y) -> neg mult_nat(x, y),
             mult_int(neg x, pos y) -> neg mult_nat(x, y),
             mult_int(neg x, neg y) -> pos mult_nat(x, y),
                          log(x, y) -> logNat(and(greatereq_int(x, pos 0()), greatereq_int(y, pos s s 0())), x, y),
         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(),
               logNat(true(), x, y) -> cond(lesseq_int(x, y), x, y),
                and(true(), true()) -> true(),
               and(true(), false()) -> false(),
               and(false(), true()) -> false(),
              and(false(), false()) -> false(),
      greatereq_int(pos x, pos 0()) -> true(),
        greatereq_int(pos x, neg y) -> true(),
    greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
    greatereq_int(pos 0(), pos s y) -> false(),
      greatereq_int(neg x, pos s y) -> false(),
    greatereq_int(neg s x, pos 0()) -> false(),
    greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y),
    greatereq_int(neg s x, neg 0()) -> false(),
    greatereq_int(neg 0(), pos 0()) -> true(),
      greatereq_int(neg 0(), neg y) -> true(),
                 mult_nat(s x, s y) -> plus_nat(mult_nat(x, s y), s y),
                 mult_nat(s x, 0()) -> 0(),
                   mult_nat(0(), y) -> 0(),
                   plus_nat(s x, y) -> s plus_nat(x, y),
                   plus_nat(0(), x) -> x}
  Fail