Problem AProVE 04 JFP Ex31

Tool CaT

Execution TimeUnknown
Answer
MAYBE
InputAProVE 04 JFP Ex31

stdout:

MAYBE

Problem:
 active(f(b(),c(),x)) -> mark(f(x,x,x))
 active(f(x,y,z)) -> f(x,y,active(z))
 active(d()) -> m(b())
 f(x,y,mark(z)) -> mark(f(x,y,z))
 active(d()) -> mark(c())
 proper(b()) -> ok(b())
 proper(c()) -> ok(c())
 proper(d()) -> ok(d())
 proper(f(x,y,z)) -> f(proper(x),proper(y),proper(z))
 f(ok(x),ok(y),ok(z)) -> ok(f(x,y,z))
 top(mark(x)) -> top(proper(x))
 top(ok(x)) -> top(active(x))

Proof:
 Open

Tool IRC1

Execution TimeUnknown
Answer
MAYBE
InputAProVE 04 JFP Ex31

stdout:

MAYBE

Tool IRC2

Execution TimeUnknown
Answer
TIMEOUT
InputAProVE 04 JFP Ex31

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  active(f(b(), c(), x)) -> mark(f(x, x, x))
     , active(f(x, y, z)) -> f(x, y, active(z))
     , active(d()) -> m(b())
     , f(x, y, mark(z)) -> mark(f(x, y, z))
     , active(d()) -> mark(c())
     , proper(b()) -> ok(b())
     , proper(c()) -> ok(c())
     , proper(d()) -> ok(d())
     , proper(f(x, y, z)) -> f(proper(x), proper(y), proper(z))
     , f(ok(x), ok(y), ok(z)) -> ok(f(x, y, z))
     , top(mark(x)) -> top(proper(x))
     , top(ok(x)) -> top(active(x))}

Proof Output:    
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution TimeUnknown
Answer
MAYBE
InputAProVE 04 JFP Ex31

stdout:

MAYBE

Tool RC2

Execution TimeUnknown
Answer
TIMEOUT
InputAProVE 04 JFP Ex31

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  active(f(b(), c(), x)) -> mark(f(x, x, x))
     , active(f(x, y, z)) -> f(x, y, active(z))
     , active(d()) -> m(b())
     , f(x, y, mark(z)) -> mark(f(x, y, z))
     , active(d()) -> mark(c())
     , proper(b()) -> ok(b())
     , proper(c()) -> ok(c())
     , proper(d()) -> ok(d())
     , proper(f(x, y, z)) -> f(proper(x), proper(y), proper(z))
     , f(ok(x), ok(y), ok(z)) -> ok(f(x, y, z))
     , top(mark(x)) -> top(proper(x))
     , top(ok(x)) -> top(active(x))}

Proof Output:    
  Computation stopped due to timeout after 60.0 seconds