Problem Secret 07 TRS aprove01

Tool CaT

Execution TimeUnknown
Answer
MAYBE
InputSecret 07 TRS aprove01

stdout:

MAYBE

Problem:
 times(x,y) -> sum(generate(x,y))
 generate(x,y) -> gen(x,y,0())
 gen(x,y,z) -> if(ge(z,x),x,y,z)
 if(true(),x,y,z) -> nil()
 if(false(),x,y,z) -> cons(y,gen(x,y,s(z)))
 sum(xs) -> sum2(xs,0())
 sum2(xs,y) -> ifsum(isNil(xs),isZero(head(xs)),xs,y)
 ifsum(true(),b,xs,y) -> y
 ifsum(false(),b,xs,y) -> ifsum2(b,xs,y)
 ifsum2(true(),xs,y) -> sum2(tail(xs),y)
 ifsum2(false(),xs,y) -> sum2(cons(p(head(xs)),tail(xs)),s(y))
 isNil(nil()) -> true()
 isNil(cons(x,xs)) -> false()
 tail(nil()) -> nil()
 tail(cons(x,xs)) -> xs
 head(cons(x,xs)) -> x
 head(nil()) -> error()
 isZero(0()) -> true()
 isZero(s(0())) -> false()
 isZero(s(s(x))) -> isZero(s(x))
 p(0()) -> s(s(0()))
 p(s(0())) -> 0()
 p(s(s(x))) -> s(p(s(x)))
 ge(x,0()) -> true()
 ge(0(),s(y)) -> false()
 ge(s(x),s(y)) -> ge(x,y)
 a() -> c()
 a() -> d()

Proof:
 Open

Tool IRC1

Execution TimeUnknown
Answer
MAYBE
InputSecret 07 TRS aprove01

stdout:

MAYBE

Tool IRC2

Execution TimeUnknown
Answer
TIMEOUT
InputSecret 07 TRS aprove01

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  times(x, y) -> sum(generate(x, y))
     , generate(x, y) -> gen(x, y, 0())
     , gen(x, y, z) -> if(ge(z, x), x, y, z)
     , if(true(), x, y, z) -> nil()
     , if(false(), x, y, z) -> cons(y, gen(x, y, s(z)))
     , sum(xs) -> sum2(xs, 0())
     , sum2(xs, y) -> ifsum(isNil(xs), isZero(head(xs)), xs, y)
     , ifsum(true(), b, xs, y) -> y
     , ifsum(false(), b, xs, y) -> ifsum2(b, xs, y)
     , ifsum2(true(), xs, y) -> sum2(tail(xs), y)
     , ifsum2(false(), xs, y) -> sum2(cons(p(head(xs)), tail(xs)), s(y))
     , isNil(nil()) -> true()
     , isNil(cons(x, xs)) -> false()
     , tail(nil()) -> nil()
     , tail(cons(x, xs)) -> xs
     , head(cons(x, xs)) -> x
     , head(nil()) -> error()
     , isZero(0()) -> true()
     , isZero(s(0())) -> false()
     , isZero(s(s(x))) -> isZero(s(x))
     , p(0()) -> s(s(0()))
     , p(s(0())) -> 0()
     , p(s(s(x))) -> s(p(s(x)))
     , ge(x, 0()) -> true()
     , ge(0(), s(y)) -> false()
     , ge(s(x), s(y)) -> ge(x, y)
     , a() -> c()
     , a() -> d()}

Proof Output:    
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution TimeUnknown
Answer
MAYBE
InputSecret 07 TRS aprove01

stdout:

MAYBE

Tool RC2

Execution TimeUnknown
Answer
TIMEOUT
InputSecret 07 TRS aprove01

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  times(x, y) -> sum(generate(x, y))
     , generate(x, y) -> gen(x, y, 0())
     , gen(x, y, z) -> if(ge(z, x), x, y, z)
     , if(true(), x, y, z) -> nil()
     , if(false(), x, y, z) -> cons(y, gen(x, y, s(z)))
     , sum(xs) -> sum2(xs, 0())
     , sum2(xs, y) -> ifsum(isNil(xs), isZero(head(xs)), xs, y)
     , ifsum(true(), b, xs, y) -> y
     , ifsum(false(), b, xs, y) -> ifsum2(b, xs, y)
     , ifsum2(true(), xs, y) -> sum2(tail(xs), y)
     , ifsum2(false(), xs, y) -> sum2(cons(p(head(xs)), tail(xs)), s(y))
     , isNil(nil()) -> true()
     , isNil(cons(x, xs)) -> false()
     , tail(nil()) -> nil()
     , tail(cons(x, xs)) -> xs
     , head(cons(x, xs)) -> x
     , head(nil()) -> error()
     , isZero(0()) -> true()
     , isZero(s(0())) -> false()
     , isZero(s(s(x))) -> isZero(s(x))
     , p(0()) -> s(s(0()))
     , p(s(0())) -> 0()
     , p(s(s(x))) -> s(p(s(x)))
     , ge(x, 0()) -> true()
     , ge(0(), s(y)) -> false()
     , ge(s(x), s(y)) -> ge(x, y)
     , a() -> c()
     , a() -> d()}

Proof Output:    
  Computation stopped due to timeout after 60.0 seconds