MAYBE
* Step 1: Failure MAYBE
  + Considered Problem:
      - Strict TRS:
          'abs('0()) -> '0()
          'abs('neg(x)) -> 'pos(x)
          'abs('pos(x)) -> 'pos(x)
          'abs('s(x)) -> 'pos('s(x))
          'add('0(),y) -> y
          'add('neg('s('0())),y) -> 'pred(y)
          'add('neg('s('s(x))),y) -> 'pred('add('pos('s(x)),y))
          'add('pos('s('0())),y) -> 'succ(y)
          'add('pos('s('s(x))),y) -> 'succ('add('pos('s(x)),y))
          'and('false(),'false()) -> 'false()
          'and('false(),'true()) -> 'false()
          'and('true(),'false()) -> 'false()
          'and('true(),'true()) -> 'true()
          'ckgt('EQ()) -> 'false()
          'ckgt('GT()) -> 'true()
          'ckgt('LT()) -> 'false()
          'cklt('EQ()) -> 'false()
          'cklt('GT()) -> 'false()
          'cklt('LT()) -> 'true()
          'compare('0(),'0()) -> 'EQ()
          'compare('0(),'neg(y)) -> 'GT()
          'compare('0(),'pos(y)) -> 'LT()
          'compare('0(),'s(y)) -> 'LT()
          'compare('neg(x),'0()) -> 'LT()
          'compare('neg(x),'neg(y)) -> 'compare(y,x)
          'compare('neg(x),'pos(y)) -> 'LT()
          'compare('pos(x),'0()) -> 'GT()
          'compare('pos(x),'neg(y)) -> 'GT()
          'compare('pos(x),'pos(y)) -> 'compare(x,y)
          'compare('s(x),'0()) -> 'GT()
          'compare('s(x),'s(y)) -> 'compare(x,y)
          'div('0(),'0()) -> 'divByZero()
          'div('0(),'neg(y)) -> '0()
          'div('0(),'pos(y)) -> '0()
          'div('neg(x),'0()) -> 'divByZero()
          'div('neg(x),'neg(y)) -> 'positive('natdiv(x,y))
          'div('neg(x),'pos(y)) -> 'negative('natdiv(x,y))
          'div('pos(x),'0()) -> 'divByZero()
          'div('pos(x),'neg(y)) -> 'negative('natdiv(x,y))
          'div('pos(x),'pos(y)) -> 'positive('natdiv(x,y))
          'divsub('0(),'0()) -> '0()
          'divsub('0(),'s(y)) -> 'underflow()
          'divsub('s(x),'0()) -> 's(x)
          'divsub('s(x),'s(y)) -> 'divsub(x,y)
          'eq('0(),'0()) -> 'true()
          'eq('0(),'neg(y)) -> 'false()
          'eq('0(),'pos(y)) -> 'false()
          'eq('0(),'s(y)) -> 'false()
          'eq('neg(x),'0()) -> 'false()
          'eq('neg(x),'neg(y)) -> 'eq(x,y)
          'eq('neg(x),'pos(y)) -> 'false()
          'eq('pos(x),'0()) -> 'false()
          'eq('pos(x),'neg(y)) -> 'false()
          'eq('pos(x),'pos(y)) -> 'eq(x,y)
          'eq('s(x),'0()) -> 'false()
          'eq('s(x),'s(y)) -> 'eq(x,y)
          'eq(dd(x'1,x'2),dd(y'1,y'2)) -> 'and('eq(x'1,y'1),'eq(x'2,y'2))
          'eq(dd(x'1,x'2),nil()) -> 'false()
          'eq(dd(x'1,x'2),tuple'2(y'1,y'2)) -> 'false()
          'eq(nil(),dd(y'1,y'2)) -> 'false()
          'eq(nil(),nil()) -> 'true()
          'eq(nil(),tuple'2(y'1,y'2)) -> 'false()
          'eq(tuple'2(x'1,x'2),dd(y'1,y'2)) -> 'false()
          'eq(tuple'2(x'1,x'2),nil()) -> 'false()
          'eq(tuple'2(x'1,x'2),tuple'2(y'1,y'2)) -> 'and('eq(x'1,y'1),'eq(x'2,y'2))
          'equal(x,y) -> 'eq(x,y)
          'greater(x,y) -> 'ckgt('compare(x,y))
          'less(x,y) -> 'cklt('compare(x,y))
          'mult('0(),'0()) -> '0()
          'mult('0(),'neg(y)) -> '0()
          'mult('0(),'pos(y)) -> '0()
          'mult('neg(x),'0()) -> '0()
          'mult('neg(x),'neg(y)) -> 'pos('natmult(x,y))
          'mult('neg(x),'pos(y)) -> 'neg('natmult(x,y))
          'mult('pos(x),'0()) -> '0()
          'mult('pos(x),'neg(y)) -> 'neg('natmult(x,y))
          'mult('pos(x),'pos(y)) -> 'pos('natmult(x,y))
          'natadd('0(),y) -> y
          'natadd('s(x),y) -> 's('natadd(x,y))
          'natdiv('0(),'0()) -> 'divByZero()
          'natdiv('0(),'s(y)) -> '0()
          'natdiv('s(x),'0()) -> 'divByZero()
          'natdiv('s(x),'s(y)) -> 'natdiv'('divsub(x,y),'s(y))
          'natdiv'('0(),y) -> 's('0())
          'natdiv'('s(x),y) -> 's('natdiv('s(x),y))
          'natdiv'('underflow(),y) -> '0()
          'natmult('0(),y) -> '0()
          'natmult('s(x),y) -> 'natadd(y,'natmult(x,y))
          'natsub(x,'0()) -> x
          'natsub('s(x),'s(y)) -> 'natsub(x,y)
          'negative('0()) -> '0()
          'negative('neg(x)) -> 'pos(x)
          'negative('pos(x)) -> 'neg(x)
          'negative('s(x)) -> 'neg('s(x))
          'positive('0()) -> '0()
          'positive('neg(x)) -> 'neg(x)
          'positive('pos(x)) -> 'pos(x)
          'positive('s(x)) -> 'pos('s(x))
          'pred('0()) -> 'neg('s('0()))
          'pred('neg('s(x))) -> 'neg('s('s(x)))
          'pred('pos('s('0()))) -> '0()
          'pred('pos('s('s(x)))) -> 'pos('s(x))
          'sub(x,'0()) -> x
          'sub(x,'neg(y)) -> 'add(x,'pos(y))
          'sub(x,'pos(y)) -> 'add(x,'neg(y))
          'succ('0()) -> 'pos('s('0()))
          'succ('neg('s('0()))) -> '0()
          'succ('neg('s('s(x)))) -> 'neg('s(x))
          'succ('pos('s(x))) -> 'pos('s('s(x)))
          add(b1,b2) -> add'(b1,b2,'abs('0()))
          add(x,y) -> 'add(x,y)
          add'(b1,b2,r) -> add''1(b1,b2,r)
          add''1(dd(x,xs),b2,r) -> add''2(b2,r,x,xs)
          add''1(nil(),b2,r) -> nil()
          add''2(dd(y,ys),r,x,xs) -> add''3(sum(x,y,r),xs,ys)
          add''2(nil(),r,x,xs) -> nil()
          add''3(tuple'2(z,r'),xs,ys) -> dd(z,add'(xs,ys,r'))
          bitToInt(b) -> bitToInt'(b,'abs('pos('s('0()))))
          bitToInt'(b,n) -> bitToInt''1(b,n)
          bitToInt''1(dd(x,xs),n) -> add(mult(x,n),bitToInt'(xs,mult(n,'pos('s('s('0()))))))
          bitToInt''1(nil(),n) -> 'abs('0())
          compare(b1,b2) -> compare'1(b1,b2)
          compare'1(dd(x,xs),b2) -> compare'2(b2,x,xs)
          compare'1(nil(),b2) -> 'abs('0())
          compare'2(dd(y,ys),x,xs) -> compare'3(compare(xs,ys),x,y)
          compare'2(nil(),x,xs) -> 'abs('0())
          compare'3(r,x,y) -> compare'4('equal(r,'0()),r,x,y)
          compare'4('false(),r,x,y) -> r
          compare'4('true(),r,x,y) -> compare'5('less(x,y),x,y)
          compare'5('false(),x,y) -> compare'6('greater(x,y))
          compare'5('true(),x,y) -> sub('0(),'pos('s('0())))
          compare'6('false()) -> 'abs('0())
          compare'6('true()) -> 'abs('pos('s('0())))
          diff(x,y,r) -> tuple'2(mod(add(add(x,y),r),'pos('s('s('0())))),diff'1('less(sub(sub(x,y),r),'0())))
          diff'1('false()) -> 'abs('0())
          diff'1('true()) -> 'abs('pos('s('0())))
          div(x,y) -> 'div(x,y)
          leq(b1,b2) -> 'less(compare(b1,b2),'pos('s('0())))
          mod(x,y) -> sub(x,mult(y,div(x,y)))
          mult(b1,b2) -> mult'1(b1,b2)
          mult(x,y) -> 'mult(x,y)
          mult'1(dd(x,xs),b2) -> mult'2(dd('abs('0()),mult(xs,b2)),b2,x)
          mult'1(nil(),b2) -> nil()
          mult'2(zs,b2,x) -> mult'3('equal(x,'pos('s('0()))),b2,zs)
          mult'3('false(),b2,zs) -> zs
          mult'3('true(),b2,zs) -> add(b2,zs)
          mult3(b1,b2,b3) -> mult(mult(b1,b2),b2)
          sub(b1,b2) -> sub'1(sub'(b1,b2,'abs('0())))
          sub(x,y) -> 'sub(x,y)
          sub'(b1,b2,r) -> sub''1(b1,b2,r)
          sub''1(dd(x,xs),b2,r) -> sub''2(b2,r,x,xs)
          sub''1(nil(),b2,r) -> tuple'2(nil(),r)
          sub''2(dd(y,ys),r,x,xs) -> sub''3(diff(x,y,r),xs,ys)
          sub''2(nil(),r,x,xs) -> tuple'2(nil(),r)
          sub''3(tuple'2(z,r'),xs,ys) -> sub''4(sub'(xs,ys,r'),z)
          sub''4(tuple'2(zs,s),z) -> tuple'2(sub''5('equal(s,'pos('s('0()))),z,zs),s)
          sub''5('false(),z,zs) -> dd(z,zs)
          sub''5('true(),z,zs) -> dd('abs('0()),zs)
          sub'1(tuple'2(b,'1)) -> b
          sum(x,y,r) -> sum'1(add(add(x,y),r))
          sum'1(s) -> sum'2('equal(s,'0()),s)
          sum'2('false(),s) -> sum'3('equal(s,'pos('s('0()))),s)
          sum'2('true(),s) -> tuple'2('abs('0()),'abs('0()))
          sum'3('false(),s) -> sum'4('equal(s,'pos('s('s('0())))))
          sum'3('true(),s) -> tuple'2('abs('pos('s('0()))),'abs('0()))
          sum'4('false()) -> tuple'2('abs('pos('s('0()))),'abs('pos('s('0()))))
          sum'4('true()) -> tuple'2('abs('0()),'abs('pos('s('0()))))
      - Signature:
          {'abs/1,'add/2,'and/2,'ckgt/1,'cklt/1,'compare/2,'div/2,'divsub/2,'eq/2,'equal/2,'greater/2,'less/2,'mult/2
          ,'natadd/2,'natdiv/2,'natdiv'/2,'natmult/2,'natsub/2,'negative/1,'positive/1,'pred/1,'sub/2,'succ/1,add/2
          ,add'/3,add''1/3,add''2/4,add''3/3,bitToInt/1,bitToInt'/2,bitToInt''1/2,compare/2,compare'1/2,compare'2/3
          ,compare'3/3,compare'4/4,compare'5/3,compare'6/1,diff/3,diff'1/1,div/2,leq/2,mod/2,mult/2,mult'1/2,mult'2/3
          ,mult'3/3,mult3/3,sub/2,sub'/3,sub''1/3,sub''2/4,sub''3/3,sub''4/2,sub''5/3,sub'1/1,sum/3,sum'1/1,sum'2/2
          ,sum'3/2,sum'4/1} / {'0/0,'EQ/0,'GT/0,'LT/0,'divByZero/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,'underflow/0
          ,dd/2,nil/0,tuple'2/2}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {'abs,'add,'and,'ckgt,'cklt,'compare,'div,'divsub,'eq
          ,'equal,'greater,'less,'mult,'natadd,'natdiv,'natdiv','natmult,'natsub,'negative,'positive,'pred,'sub,'succ
          ,add,add',add''1,add''2,add''3,bitToInt,bitToInt',bitToInt''1,compare,compare'1,compare'2,compare'3
          ,compare'4,compare'5,compare'6,diff,diff'1,div,leq,mod,mult,mult'1,mult'2,mult'3,mult3,sub,sub',sub''1
          ,sub''2,sub''3,sub''4,sub''5,sub'1,sum,sum'1,sum'2,sum'3,sum'4} and constructors {'0,'EQ,'GT,'LT,'divByZero
          ,'false,'neg,'pos,'s,'true,'underflow,dd,nil,tuple'2}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE