LMPO

Execution Time (secs)	0.124
Answer	MAYBE
Input	AProVE 07 thiemann16

MAYBE

We consider the following Problem:

  Strict Trs:
    {  check(0()) -> zero()
     , check(s(0())) -> odd()
     , check(s(s(0()))) -> even()
     , check(s(s(s(x)))) -> check(s(x))
     , half(0()) -> 0()
     , half(s(0())) -> 0()
     , half(s(s(x))) -> s(half(x))
     , plus(0(), y) -> y
     , plus(s(x), y) -> s(plus(x, y))
     , times(x, y) -> timesIter(x, y, 0())
     , timesIter(x, y, z) -> if(check(x), x, y, z, plus(z, y))
     , p(s(x)) -> x
     , p(0()) -> 0()
     , if(zero(), x, y, z, u) -> z
     , if(odd(), x, y, z, u) -> timesIter(p(x), y, u)
     , if(even(), x, y, z, u) ->
       plus(timesIter(half(x), y, half(z)),
            timesIter(half(x), y, half(s(z))))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MPO

Execution Time (secs)	0.126
Answer	MAYBE
Input	AProVE 07 thiemann16

MAYBE

We consider the following Problem:

  Strict Trs:
    {  check(0()) -> zero()
     , check(s(0())) -> odd()
     , check(s(s(0()))) -> even()
     , check(s(s(s(x)))) -> check(s(x))
     , half(0()) -> 0()
     , half(s(0())) -> 0()
     , half(s(s(x))) -> s(half(x))
     , plus(0(), y) -> y
     , plus(s(x), y) -> s(plus(x, y))
     , times(x, y) -> timesIter(x, y, 0())
     , timesIter(x, y, z) -> if(check(x), x, y, z, plus(z, y))
     , p(s(x)) -> x
     , p(0()) -> 0()
     , if(zero(), x, y, z, u) -> z
     , if(odd(), x, y, z, u) -> timesIter(p(x), y, u)
     , if(even(), x, y, z, u) ->
       plus(timesIter(half(x), y, half(z)),
            timesIter(half(x), y, half(s(z))))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

POP*

Execution Time (secs)	0.157
Answer	MAYBE
Input	AProVE 07 thiemann16

MAYBE

We consider the following Problem:

  Strict Trs:
    {  check(0()) -> zero()
     , check(s(0())) -> odd()
     , check(s(s(0()))) -> even()
     , check(s(s(s(x)))) -> check(s(x))
     , half(0()) -> 0()
     , half(s(0())) -> 0()
     , half(s(s(x))) -> s(half(x))
     , plus(0(), y) -> y
     , plus(s(x), y) -> s(plus(x, y))
     , times(x, y) -> timesIter(x, y, 0())
     , timesIter(x, y, z) -> if(check(x), x, y, z, plus(z, y))
     , p(s(x)) -> x
     , p(0()) -> 0()
     , if(zero(), x, y, z, u) -> z
     , if(odd(), x, y, z, u) -> timesIter(p(x), y, u)
     , if(even(), x, y, z, u) ->
       plus(timesIter(half(x), y, half(z)),
            timesIter(half(x), y, half(s(z))))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

POP* (PS)

Execution Time (secs)	0.143
Answer	MAYBE
Input	AProVE 07 thiemann16

MAYBE

We consider the following Problem:

  Strict Trs:
    {  check(0()) -> zero()
     , check(s(0())) -> odd()
     , check(s(s(0()))) -> even()
     , check(s(s(s(x)))) -> check(s(x))
     , half(0()) -> 0()
     , half(s(0())) -> 0()
     , half(s(s(x))) -> s(half(x))
     , plus(0(), y) -> y
     , plus(s(x), y) -> s(plus(x, y))
     , times(x, y) -> timesIter(x, y, 0())
     , timesIter(x, y, z) -> if(check(x), x, y, z, plus(z, y))
     , p(s(x)) -> x
     , p(0()) -> 0()
     , if(zero(), x, y, z, u) -> z
     , if(odd(), x, y, z, u) -> timesIter(p(x), y, u)
     , if(even(), x, y, z, u) ->
       plus(timesIter(half(x), y, half(z)),
            timesIter(half(x), y, half(s(z))))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

Small POP*

Execution Time (secs)	0.171
Answer	MAYBE
Input	AProVE 07 thiemann16

MAYBE

We consider the following Problem:

  Strict Trs:
    {  check(0()) -> zero()
     , check(s(0())) -> odd()
     , check(s(s(0()))) -> even()
     , check(s(s(s(x)))) -> check(s(x))
     , half(0()) -> 0()
     , half(s(0())) -> 0()
     , half(s(s(x))) -> s(half(x))
     , plus(0(), y) -> y
     , plus(s(x), y) -> s(plus(x, y))
     , times(x, y) -> timesIter(x, y, 0())
     , timesIter(x, y, z) -> if(check(x), x, y, z, plus(z, y))
     , p(s(x)) -> x
     , p(0()) -> 0()
     , if(zero(), x, y, z, u) -> z
     , if(odd(), x, y, z, u) -> timesIter(p(x), y, u)
     , if(even(), x, y, z, u) ->
       plus(timesIter(half(x), y, half(z)),
            timesIter(half(x), y, half(s(z))))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

Small POP* (PS)

Execution Time (secs)	0.111
Answer	MAYBE
Input	AProVE 07 thiemann16

MAYBE

We consider the following Problem:

  Strict Trs:
    {  check(0()) -> zero()
     , check(s(0())) -> odd()
     , check(s(s(0()))) -> even()
     , check(s(s(s(x)))) -> check(s(x))
     , half(0()) -> 0()
     , half(s(0())) -> 0()
     , half(s(s(x))) -> s(half(x))
     , plus(0(), y) -> y
     , plus(s(x), y) -> s(plus(x, y))
     , times(x, y) -> timesIter(x, y, 0())
     , timesIter(x, y, z) -> if(check(x), x, y, z, plus(z, y))
     , p(s(x)) -> x
     , p(0()) -> 0()
     , if(zero(), x, y, z, u) -> z
     , if(odd(), x, y, z, u) -> timesIter(p(x), y, u)
     , if(even(), x, y, z, u) ->
       plus(timesIter(half(x), y, half(z)),
            timesIter(half(x), y, half(s(z))))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

Problem AProVE 07 thiemann16

LMPO

MPO

POP*

POP* (PS)

Small POP*

Small POP* (PS)