Problem Various 04 14

Tool CaT

Execution Time	Unknown
Answer	MAYBE
Input	Various 04 14

stdout:

MAYBE

Problem:
O(0()) -> 0()
+(0(),x) -> x
+(x,0()) -> x
+(O(x),O(y)) -> O(+(x,y))
+(O(x),I(y)) -> I(+(x,y))
+(I(x),O(y)) -> I(+(x,y))
+(I(x),I(y)) -> O(+(+(x,y),I(0())))
+(x,+(y,z)) -> +(+(x,y),z)
-(x,0()) -> x
-(0(),x) -> 0()
-(O(x),O(y)) -> O(-(x,y))
-(O(x),I(y)) -> I(-(-(x,y),I(1())))
-(I(x),O(y)) -> I(-(x,y))
-(I(x),I(y)) -> O(-(x,y))
not(true()) -> false()
not(false()) -> true()
and(x,true()) -> x
and(x,false()) -> false()
if(true(),x,y) -> x
if(false(),x,y) -> y
ge(O(x),O(y)) -> ge(x,y)
ge(O(x),I(y)) -> not(ge(y,x))
ge(I(x),O(y)) -> ge(x,y)
ge(I(x),I(y)) -> ge(x,y)
ge(x,0()) -> true()
ge(0(),O(x)) -> ge(0(),x)
ge(0(),I(x)) -> false()
Log'(0()) -> 0()
Log'(I(x)) -> +(Log'(x),I(0()))
Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),0())
Log(x) -> -(Log'(x),I(0()))
Val(L(x)) -> x
Val(N(x,l(),r())) -> x
Min(L(x)) -> x
Min(N(x,l(),r())) -> Min(l())
Max(L(x)) -> x
Max(N(x,l(),r())) -> Max(r())
BS(L(x)) -> true()
BS(N(x,l(),r())) -> and(and(ge(x,Max(l())),ge(Min(r()),x)),and(BS(l()),BS(r())))
Size(L(x)) -> I(0())
Size(N(x,l(),r())) -> +(+(Size(l()),Size(r())),I(1()))
WB(L(x)) -> true()
WB(N(x,l(),r())) ->
and(if(ge(Size(l()),Size(r())),ge(I(0()),-(Size(l()),Size(r()))),ge(I(0()),-(Size(r()),Size(l())))),
and(WB(l()),WB(r())))

Proof:
Open

Tool IRC1

Execution Time	Unknown
Answer	MAYBE
Input	Various 04 14

stdout:

MAYBE

Tool IRC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Various 04 14

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  O(0()) -> 0()
     , +(0(), x) -> x
     , +(x, 0()) -> x
     , +(O(x), O(y)) -> O(+(x, y))
     , +(O(x), I(y)) -> I(+(x, y))
     , +(I(x), O(y)) -> I(+(x, y))
     , +(I(x), I(y)) -> O(+(+(x, y), I(0())))
     , +(x, +(y, z)) -> +(+(x, y), z)
     , -(x, 0()) -> x
     , -(0(), x) -> 0()
     , -(O(x), O(y)) -> O(-(x, y))
     , -(O(x), I(y)) -> I(-(-(x, y), I(1())))
     , -(I(x), O(y)) -> I(-(x, y))
     , -(I(x), I(y)) -> O(-(x, y))
     , not(true()) -> false()
     , not(false()) -> true()
     , and(x, true()) -> x
     , and(x, false()) -> false()
     , if(true(), x, y) -> x
     , if(false(), x, y) -> y
     , ge(O(x), O(y)) -> ge(x, y)
     , ge(O(x), I(y)) -> not(ge(y, x))
     , ge(I(x), O(y)) -> ge(x, y)
     , ge(I(x), I(y)) -> ge(x, y)
     , ge(x, 0()) -> true()
     , ge(0(), O(x)) -> ge(0(), x)
     , ge(0(), I(x)) -> false()
     , Log'(0()) -> 0()
     , Log'(I(x)) -> +(Log'(x), I(0()))
     , Log'(O(x)) -> if(ge(x, I(0())), +(Log'(x), I(0())), 0())
     , Log(x) -> -(Log'(x), I(0()))
     , Val(L(x)) -> x
     , Val(N(x, l(), r())) -> x
     , Min(L(x)) -> x
     , Min(N(x, l(), r())) -> Min(l())
     , Max(L(x)) -> x
     , Max(N(x, l(), r())) -> Max(r())
     , BS(L(x)) -> true()
     , BS(N(x, l(), r())) ->
       and(and(ge(x, Max(l())), ge(Min(r()), x)), and(BS(l()), BS(r())))
     , Size(L(x)) -> I(0())
     , Size(N(x, l(), r())) -> +(+(Size(l()), Size(r())), I(1()))
     , WB(L(x)) -> true()
     , WB(N(x, l(), r())) ->
       and(if(ge(Size(l()), Size(r())),
              ge(I(0()), -(Size(l()), Size(r()))),
              ge(I(0()), -(Size(r()), Size(l())))),
           and(WB(l()), WB(r())))}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution Time	Unknown
Answer	MAYBE
Input	Various 04 14

stdout:

MAYBE

Tool RC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Various 04 14

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  O(0()) -> 0()
     , +(0(), x) -> x
     , +(x, 0()) -> x
     , +(O(x), O(y)) -> O(+(x, y))
     , +(O(x), I(y)) -> I(+(x, y))
     , +(I(x), O(y)) -> I(+(x, y))
     , +(I(x), I(y)) -> O(+(+(x, y), I(0())))
     , +(x, +(y, z)) -> +(+(x, y), z)
     , -(x, 0()) -> x
     , -(0(), x) -> 0()
     , -(O(x), O(y)) -> O(-(x, y))
     , -(O(x), I(y)) -> I(-(-(x, y), I(1())))
     , -(I(x), O(y)) -> I(-(x, y))
     , -(I(x), I(y)) -> O(-(x, y))
     , not(true()) -> false()
     , not(false()) -> true()
     , and(x, true()) -> x
     , and(x, false()) -> false()
     , if(true(), x, y) -> x
     , if(false(), x, y) -> y
     , ge(O(x), O(y)) -> ge(x, y)
     , ge(O(x), I(y)) -> not(ge(y, x))
     , ge(I(x), O(y)) -> ge(x, y)
     , ge(I(x), I(y)) -> ge(x, y)
     , ge(x, 0()) -> true()
     , ge(0(), O(x)) -> ge(0(), x)
     , ge(0(), I(x)) -> false()
     , Log'(0()) -> 0()
     , Log'(I(x)) -> +(Log'(x), I(0()))
     , Log'(O(x)) -> if(ge(x, I(0())), +(Log'(x), I(0())), 0())
     , Log(x) -> -(Log'(x), I(0()))
     , Val(L(x)) -> x
     , Val(N(x, l(), r())) -> x
     , Min(L(x)) -> x
     , Min(N(x, l(), r())) -> Min(l())
     , Max(L(x)) -> x
     , Max(N(x, l(), r())) -> Max(r())
     , BS(L(x)) -> true()
     , BS(N(x, l(), r())) ->
       and(and(ge(x, Max(l())), ge(Min(r()), x)), and(BS(l()), BS(r())))
     , Size(L(x)) -> I(0())
     , Size(N(x, l(), r())) -> +(+(Size(l()), Size(r())), I(1()))
     , WB(L(x)) -> true()
     , WB(N(x, l(), r())) ->
       and(if(ge(Size(l()), Size(r())),
              ge(I(0()), -(Size(l()), Size(r()))),
              ge(I(0()), -(Size(r()), Size(l())))),
           and(WB(l()), WB(r())))}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds