Problem CiME 04 log2

Tool CaT

Execution TimeUnknown
Answer
MAYBE
InputCiME 04 log2

stdout:

MAYBE

Problem:
 0(#()) -> #()
 +(#(),x) -> x
 +(x,#()) -> x
 +(0(x),0(y)) -> 0(+(x,y))
 +(0(x),1(y)) -> 1(+(x,y))
 +(1(x),0(y)) -> 1(+(x,y))
 +(1(x),1(y)) -> 0(+(+(x,y),1(#())))
 +(+(x,y),z) -> +(x,+(y,z))
 -(#(),x) -> #()
 -(x,#()) -> x
 -(0(x),0(y)) -> 0(-(x,y))
 -(0(x),1(y)) -> 1(-(-(x,y),1(#())))
 -(1(x),0(y)) -> 1(-(x,y))
 -(1(x),1(y)) -> 0(-(x,y))
 not(true()) -> false()
 not(false()) -> true()
 if(true(),x,y) -> x
 if(false(),x,y) -> y
 ge(0(x),0(y)) -> ge(x,y)
 ge(0(x),1(y)) -> not(ge(y,x))
 ge(1(x),0(y)) -> ge(x,y)
 ge(1(x),1(y)) -> ge(x,y)
 ge(x,#()) -> true()
 ge(#(),0(x)) -> ge(#(),x)
 ge(#(),1(x)) -> false()
 log(x) -> -(log'(x),1(#()))
 log'(#()) -> #()
 log'(1(x)) -> +(log'(x),1(#()))
 log'(0(x)) -> if(ge(x,1(#())),+(log'(x),1(#())),#())

Proof:
 Open

Tool IRC1

Execution TimeUnknown
Answer
MAYBE
InputCiME 04 log2

stdout:

MAYBE

Tool IRC2

Execution TimeUnknown
Answer
TIMEOUT
InputCiME 04 log2

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  0(#()) -> #()
     , +(#(), x) -> x
     , +(x, #()) -> x
     , +(0(x), 0(y)) -> 0(+(x, y))
     , +(0(x), 1(y)) -> 1(+(x, y))
     , +(1(x), 0(y)) -> 1(+(x, y))
     , +(1(x), 1(y)) -> 0(+(+(x, y), 1(#())))
     , +(+(x, y), z) -> +(x, +(y, z))
     , -(#(), x) -> #()
     , -(x, #()) -> x
     , -(0(x), 0(y)) -> 0(-(x, y))
     , -(0(x), 1(y)) -> 1(-(-(x, y), 1(#())))
     , -(1(x), 0(y)) -> 1(-(x, y))
     , -(1(x), 1(y)) -> 0(-(x, y))
     , not(true()) -> false()
     , not(false()) -> true()
     , if(true(), x, y) -> x
     , if(false(), x, y) -> y
     , ge(0(x), 0(y)) -> ge(x, y)
     , ge(0(x), 1(y)) -> not(ge(y, x))
     , ge(1(x), 0(y)) -> ge(x, y)
     , ge(1(x), 1(y)) -> ge(x, y)
     , ge(x, #()) -> true()
     , ge(#(), 0(x)) -> ge(#(), x)
     , ge(#(), 1(x)) -> false()
     , log(x) -> -(log'(x), 1(#()))
     , log'(#()) -> #()
     , log'(1(x)) -> +(log'(x), 1(#()))
     , log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #())}

Proof Output:    
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution TimeUnknown
Answer
MAYBE
InputCiME 04 log2

stdout:

MAYBE

Tool RC2

Execution TimeUnknown
Answer
TIMEOUT
InputCiME 04 log2

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  0(#()) -> #()
     , +(#(), x) -> x
     , +(x, #()) -> x
     , +(0(x), 0(y)) -> 0(+(x, y))
     , +(0(x), 1(y)) -> 1(+(x, y))
     , +(1(x), 0(y)) -> 1(+(x, y))
     , +(1(x), 1(y)) -> 0(+(+(x, y), 1(#())))
     , +(+(x, y), z) -> +(x, +(y, z))
     , -(#(), x) -> #()
     , -(x, #()) -> x
     , -(0(x), 0(y)) -> 0(-(x, y))
     , -(0(x), 1(y)) -> 1(-(-(x, y), 1(#())))
     , -(1(x), 0(y)) -> 1(-(x, y))
     , -(1(x), 1(y)) -> 0(-(x, y))
     , not(true()) -> false()
     , not(false()) -> true()
     , if(true(), x, y) -> x
     , if(false(), x, y) -> y
     , ge(0(x), 0(y)) -> ge(x, y)
     , ge(0(x), 1(y)) -> not(ge(y, x))
     , ge(1(x), 0(y)) -> ge(x, y)
     , ge(1(x), 1(y)) -> ge(x, y)
     , ge(x, #()) -> true()
     , ge(#(), 0(x)) -> ge(#(), x)
     , ge(#(), 1(x)) -> false()
     , log(x) -> -(log'(x), 1(#()))
     , log'(#()) -> #()
     , log'(1(x)) -> +(log'(x), 1(#()))
     , log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #())}

Proof Output:    
  Computation stopped due to timeout after 60.0 seconds