Problem AProVE 07 thiemann05

Tool CaT

Execution TimeUnknown
Answer
MAYBE
InputAProVE 07 thiemann05

stdout:

MAYBE

Problem:
 isLeaf(leaf()) -> true()
 isLeaf(cons(u,v)) -> false()
 left(cons(u,v)) -> u
 right(cons(u,v)) -> v
 concat(leaf(),y) -> y
 concat(cons(u,v),y) -> cons(u,concat(v,y))
 less_leaves(u,v) -> if1(isLeaf(u),isLeaf(v),u,v)
 if1(b,true(),u,v) -> false()
 if1(b,false(),u,v) -> if2(b,u,v)
 if2(true(),u,v) -> true()
 if2(false(),u,v) -> less_leaves(concat(left(u),right(u)),concat(left(v),right(v)))

Proof:
 Open

Tool IRC1

Execution TimeUnknown
Answer
MAYBE
InputAProVE 07 thiemann05

stdout:

MAYBE

Tool IRC2

Execution TimeUnknown
Answer
TIMEOUT
InputAProVE 07 thiemann05

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  isLeaf(leaf()) -> true()
     , isLeaf(cons(u, v)) -> false()
     , left(cons(u, v)) -> u
     , right(cons(u, v)) -> v
     , concat(leaf(), y) -> y
     , concat(cons(u, v), y) -> cons(u, concat(v, y))
     , less_leaves(u, v) -> if1(isLeaf(u), isLeaf(v), u, v)
     , if1(b, true(), u, v) -> false()
     , if1(b, false(), u, v) -> if2(b, u, v)
     , if2(true(), u, v) -> true()
     , if2(false(), u, v) ->
       less_leaves(concat(left(u), right(u)), concat(left(v), right(v)))}

Proof Output:    
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution TimeUnknown
Answer
MAYBE
InputAProVE 07 thiemann05

stdout:

MAYBE

Tool RC2

Execution TimeUnknown
Answer
TIMEOUT
InputAProVE 07 thiemann05

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  isLeaf(leaf()) -> true()
     , isLeaf(cons(u, v)) -> false()
     , left(cons(u, v)) -> u
     , right(cons(u, v)) -> v
     , concat(leaf(), y) -> y
     , concat(cons(u, v), y) -> cons(u, concat(v, y))
     , less_leaves(u, v) -> if1(isLeaf(u), isLeaf(v), u, v)
     , if1(b, true(), u, v) -> false()
     , if1(b, false(), u, v) -> if2(b, u, v)
     , if2(true(), u, v) -> true()
     , if2(false(), u, v) ->
       less_leaves(concat(left(u), right(u)), concat(left(v), right(v)))}

Proof Output:    
  Computation stopped due to timeout after 60.0 seconds