Tool CaT
stdout:
YES(?,O(n^1))
Problem:
rec(rec(x)) -> sent(rec(x))
rec(sent(x)) -> sent(rec(x))
rec(no(x)) -> sent(rec(x))
rec(bot()) -> up(sent(bot()))
rec(up(x)) -> up(rec(x))
sent(up(x)) -> up(sent(x))
no(up(x)) -> up(no(x))
top(rec(up(x))) -> top(check(rec(x)))
top(sent(up(x))) -> top(check(rec(x)))
top(no(up(x))) -> top(check(rec(x)))
check(up(x)) -> up(check(x))
check(sent(x)) -> sent(check(x))
check(rec(x)) -> rec(check(x))
check(no(x)) -> no(check(x))
check(no(x)) -> no(x)
Proof:
Bounds Processor:
bound: 1
enrichment: match
automaton:
final states: {7,6,5,4,3}
transitions:
up1(9) -> 10*
up1(46) -> 47*
up1(36) -> 37*
up1(26) -> 27*
check1(45) -> 46*
check1(48) -> 49*
no1(35) -> 36*
no1(38) -> 39*
sent1(25) -> 26*
sent1(28) -> 29*
sent1(8) -> 9*
rec1(16) -> 17*
rec1(18) -> 19*
bot1() -> 8*
rec0(2) -> 3*
rec0(1) -> 3*
sent0(2) -> 4*
sent0(1) -> 4*
no0(2) -> 5*
no0(1) -> 5*
bot0() -> 1*
up0(2) -> 2*
up0(1) -> 2*
top0(2) -> 6*
top0(1) -> 6*
check0(2) -> 7*
check0(1) -> 7*
1 -> 48,38,28,18
2 -> 45,35,25,16
10 -> 17,19,9,3
17 -> 9*
19 -> 9*
27 -> 26,4
29 -> 26*
37 -> 36,5
39 -> 36*
47 -> 46,7
49 -> 46*
problem:
QedTool IRC1
stdout:
YES(?,O(n^1))
Tool IRC2
stdout:
YES(?,O(n^1))
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ rec(rec(x)) -> sent(rec(x))
, rec(sent(x)) -> sent(rec(x))
, rec(no(x)) -> sent(rec(x))
, rec(bot()) -> up(sent(bot()))
, rec(up(x)) -> up(rec(x))
, sent(up(x)) -> up(sent(x))
, no(up(x)) -> up(no(x))
, top(rec(up(x))) -> top(check(rec(x)))
, top(sent(up(x))) -> top(check(rec(x)))
, top(no(up(x))) -> top(check(rec(x)))
, check(up(x)) -> up(check(x))
, check(sent(x)) -> sent(check(x))
, check(rec(x)) -> rec(check(x))
, check(no(x)) -> no(check(x))
, check(no(x)) -> no(x)}
Proof Output:
'Bounds with minimal-enrichment and initial automaton 'match'' proved the best result:
Details:
--------
'Bounds with minimal-enrichment and initial automaton 'match'' succeeded with the following output:
'Bounds with minimal-enrichment and initial automaton 'match''
--------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ rec(rec(x)) -> sent(rec(x))
, rec(sent(x)) -> sent(rec(x))
, rec(no(x)) -> sent(rec(x))
, rec(bot()) -> up(sent(bot()))
, rec(up(x)) -> up(rec(x))
, sent(up(x)) -> up(sent(x))
, no(up(x)) -> up(no(x))
, top(rec(up(x))) -> top(check(rec(x)))
, top(sent(up(x))) -> top(check(rec(x)))
, top(no(up(x))) -> top(check(rec(x)))
, check(up(x)) -> up(check(x))
, check(sent(x)) -> sent(check(x))
, check(rec(x)) -> rec(check(x))
, check(no(x)) -> no(check(x))
, check(no(x)) -> no(x)}
Proof Output:
The problem is match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ rec_0(2) -> 1
, rec_1(2) -> 3
, sent_0(2) -> 1
, sent_1(2) -> 3
, sent_1(4) -> 3
, no_0(2) -> 1
, no_1(2) -> 3
, bot_0() -> 2
, bot_1() -> 4
, up_0(2) -> 2
, up_1(3) -> 1
, up_1(3) -> 3
, top_0(2) -> 1
, check_0(2) -> 1
, check_1(2) -> 3}Tool RC1
stdout:
YES(?,O(n^1))
Tool RC2
stdout:
YES(?,O(n^1))
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: YES(?,O(n^1))
Input Problem: runtime-complexity with respect to
Rules:
{ rec(rec(x)) -> sent(rec(x))
, rec(sent(x)) -> sent(rec(x))
, rec(no(x)) -> sent(rec(x))
, rec(bot()) -> up(sent(bot()))
, rec(up(x)) -> up(rec(x))
, sent(up(x)) -> up(sent(x))
, no(up(x)) -> up(no(x))
, top(rec(up(x))) -> top(check(rec(x)))
, top(sent(up(x))) -> top(check(rec(x)))
, top(no(up(x))) -> top(check(rec(x)))
, check(up(x)) -> up(check(x))
, check(sent(x)) -> sent(check(x))
, check(rec(x)) -> rec(check(x))
, check(no(x)) -> no(check(x))
, check(no(x)) -> no(x)}
Proof Output:
'Bounds with minimal-enrichment and initial automaton 'match'' proved the best result:
Details:
--------
'Bounds with minimal-enrichment and initial automaton 'match'' succeeded with the following output:
'Bounds with minimal-enrichment and initial automaton 'match''
--------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: runtime-complexity with respect to
Rules:
{ rec(rec(x)) -> sent(rec(x))
, rec(sent(x)) -> sent(rec(x))
, rec(no(x)) -> sent(rec(x))
, rec(bot()) -> up(sent(bot()))
, rec(up(x)) -> up(rec(x))
, sent(up(x)) -> up(sent(x))
, no(up(x)) -> up(no(x))
, top(rec(up(x))) -> top(check(rec(x)))
, top(sent(up(x))) -> top(check(rec(x)))
, top(no(up(x))) -> top(check(rec(x)))
, check(up(x)) -> up(check(x))
, check(sent(x)) -> sent(check(x))
, check(rec(x)) -> rec(check(x))
, check(no(x)) -> no(check(x))
, check(no(x)) -> no(x)}
Proof Output:
The problem is match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ rec_0(2) -> 1
, rec_1(2) -> 3
, sent_0(2) -> 1
, sent_1(2) -> 3
, sent_1(4) -> 3
, no_0(2) -> 1
, no_1(2) -> 3
, bot_0() -> 2
, bot_1() -> 4
, up_0(2) -> 2
, up_1(3) -> 1
, up_1(3) -> 3
, top_0(2) -> 1
, check_0(2) -> 1
, check_1(2) -> 3}