Tool CaT
stdout:
MAYBE
Problem:
app(nil(),xs) -> nil()
app(cons(x,xs),ys) -> cons(x,app(xs,ys))
rev(nil()) -> nil()
rev(cons(x,xs)) -> append(xs,rev(cons(x,nil())))
shuffle(nil()) -> nil()
shuffle(cons(x,xs)) -> cons(x,shuffle(rev(xs)))
Proof:
Complexity Transformation Processor:
strict:
app(nil(),xs) -> nil()
app(cons(x,xs),ys) -> cons(x,app(xs,ys))
rev(nil()) -> nil()
rev(cons(x,xs)) -> append(xs,rev(cons(x,nil())))
shuffle(nil()) -> nil()
shuffle(cons(x,xs)) -> cons(x,shuffle(rev(xs)))
weak:
Matrix Interpretation Processor:
dimension: 3
max_matrix:
[1 1 1]
[0 0 1]
[0 0 0]
interpretation:
[1 0 0] [1]
[shuffle](x0) = [0 0 0]x0 + [1]
[0 0 0] [0],
[1 0 0] [1 0 0] [0]
[append](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [1]
[0 0 0] [0 0 0] [1],
[1 0 0] [0]
[rev](x0) = [0 0 0]x0 + [1]
[0 0 0] [1],
[1 1 1] [1 0 0]
[cons](x0, x1) = [0 0 0]x0 + [0 0 0]x1
[0 0 0] [0 0 0] ,
[1 0 0] [1 1 0] [0]
[app](x0, x1) = [0 0 0]x0 + [0 0 1]x1 + [0]
[0 0 0] [0 0 0] [1],
[0]
[nil] = [0]
[0]
orientation:
[1 1 0] [0] [0]
app(nil(),xs) = [0 0 1]xs + [0] >= [0] = nil()
[0 0 0] [1] [0]
[1 1 1] [1 0 0] [1 1 0] [0] [1 1 1] [1 0 0] [1 1 0]
app(cons(x,xs),ys) = [0 0 0]x + [0 0 0]xs + [0 0 1]ys + [0] >= [0 0 0]x + [0 0 0]xs + [0 0 0]ys = cons(x,app(xs,ys))
[0 0 0] [0 0 0] [0 0 0] [1] [0 0 0] [0 0 0] [0 0 0]
[0] [0]
rev(nil()) = [1] >= [0] = nil()
[1] [0]
[1 1 1] [1 0 0] [0] [1 1 1] [1 0 0] [0]
rev(cons(x,xs)) = [0 0 0]x + [0 0 0]xs + [1] >= [0 0 0]x + [0 0 0]xs + [1] = append(xs,rev(cons(x,nil())))
[0 0 0] [0 0 0] [1] [0 0 0] [0 0 0] [1]
[1] [0]
shuffle(nil()) = [1] >= [0] = nil()
[0] [0]
[1 1 1] [1 0 0] [1] [1 1 1] [1 0 0] [1]
shuffle(cons(x,xs)) = [0 0 0]x + [0 0 0]xs + [1] >= [0 0 0]x + [0 0 0]xs + [0] = cons(x,shuffle(rev(xs)))
[0 0 0] [0 0 0] [0] [0 0 0] [0 0 0] [0]
problem:
strict:
app(nil(),xs) -> nil()
app(cons(x,xs),ys) -> cons(x,app(xs,ys))
rev(nil()) -> nil()
rev(cons(x,xs)) -> append(xs,rev(cons(x,nil())))
shuffle(cons(x,xs)) -> cons(x,shuffle(rev(xs)))
weak:
shuffle(nil()) -> nil()
Bounds Processor:
bound: 1
enrichment: match
automaton:
final states: {6,5,4}
transitions:
nil1() -> 13,12
cons1(2,12) -> 41*
cons1(2,18) -> 6*
cons1(3,13) -> 6*
cons1(1,12) -> 48*
cons1(1,18) -> 6*
cons1(2,13) -> 6*
cons1(3,12) -> 41*
cons1(3,18) -> 6*
cons1(1,13) -> 6*
append1(1,49) -> 17,5
append1(12,42) -> 42*
append1(2,42) -> 17,5
append1(3,49) -> 17,5
append1(1,42) -> 17,5
append1(12,49) -> 49*
append1(2,49) -> 17,5
append1(3,42) -> 17,5
rev1(2) -> 17*
rev1(41) -> 42*
rev1(1) -> 12*
rev1(48) -> 49*
rev1(3) -> 12*
shuffle1(17) -> 18*
shuffle1(12) -> 13*
app0(3,1) -> 4*
app0(3,3) -> 4*
app0(1,2) -> 4*
app0(2,1) -> 4*
app0(2,3) -> 4*
app0(3,2) -> 4*
app0(1,1) -> 4*
app0(1,3) -> 4*
app0(2,2) -> 4*
nil0() -> 6,5,4,1
cons0(3,1) -> 2*
cons0(3,3) -> 2*
cons0(1,2) -> 2*
cons0(1,4) -> 4*
cons0(2,1) -> 2*
cons0(2,3) -> 2*
cons0(3,2) -> 2*
cons0(3,4) -> 4*
cons0(1,1) -> 2*
cons0(1,3) -> 2*
cons0(2,2) -> 2*
cons0(2,4) -> 4*
rev0(2) -> 5*
rev0(1) -> 5*
rev0(3) -> 5*
append0(3,1) -> 3*
append0(3,3) -> 3*
append0(1,2) -> 3*
append0(2,1) -> 3*
append0(2,3) -> 3*
append0(3,2) -> 3*
append0(1,1) -> 3*
append0(1,3) -> 3*
append0(2,2) -> 3*
shuffle0(2) -> 6*
shuffle0(1) -> 6*
shuffle0(3) -> 6*
problem:
strict:
app(nil(),xs) -> nil()
app(cons(x,xs),ys) -> cons(x,app(xs,ys))
rev(nil()) -> nil()
rev(cons(x,xs)) -> append(xs,rev(cons(x,nil())))
weak:
shuffle(cons(x,xs)) -> cons(x,shuffle(rev(xs)))
shuffle(nil()) -> nil()
Bounds Processor:
bound: 1
enrichment: match
automaton:
final states: {6,5,4}
transitions:
nil1() -> 34,8
cons1(1,45) -> 6*
cons1(2,34) -> 6*
cons1(3,45) -> 6*
cons1(1,8) -> 22*
cons1(1,34) -> 6*
cons1(3,8) -> 15*
cons1(2,45) -> 6*
cons1(3,34) -> 6*
cons1(2,8) -> 15*
append1(2,16) -> 44,5
append1(8,23) -> 23*
append1(3,23) -> 44,5
append1(1,16) -> 44,5
append1(2,23) -> 44,5
append1(8,16) -> 16*
append1(3,16) -> 44,5
append1(1,23) -> 44,5
rev1(15) -> 16*
rev1(22) -> 23*
rev1(2) -> 44*
rev1(1) -> 33*
rev1(3) -> 33*
shuffle1(44) -> 45*
shuffle1(33) -> 34*
app0(3,1) -> 4*
app0(3,3) -> 4*
app0(1,2) -> 4*
app0(2,1) -> 4*
app0(2,3) -> 4*
app0(3,2) -> 4*
app0(1,1) -> 4*
app0(1,3) -> 4*
app0(2,2) -> 4*
nil0() -> 6,4,1
cons0(3,1) -> 2*
cons0(3,3) -> 2*
cons0(1,2) -> 2*
cons0(1,4) -> 4*
cons0(2,1) -> 2*
cons0(2,3) -> 2*
cons0(3,2) -> 2*
cons0(3,4) -> 4*
cons0(1,1) -> 2*
cons0(1,3) -> 2*
cons0(2,2) -> 2*
cons0(2,4) -> 4*
rev0(2) -> 5*
rev0(1) -> 5*
rev0(3) -> 5*
append0(3,1) -> 3*
append0(3,3) -> 3*
append0(1,2) -> 3*
append0(2,1) -> 3*
append0(2,3) -> 3*
append0(3,2) -> 3*
append0(1,1) -> 3*
append0(1,3) -> 3*
append0(2,2) -> 3*
shuffle0(2) -> 6*
shuffle0(1) -> 6*
shuffle0(3) -> 6*
8 -> 33,5
problem:
strict:
app(nil(),xs) -> nil()
app(cons(x,xs),ys) -> cons(x,app(xs,ys))
rev(cons(x,xs)) -> append(xs,rev(cons(x,nil())))
weak:
rev(nil()) -> nil()
shuffle(cons(x,xs)) -> cons(x,shuffle(rev(xs)))
shuffle(nil()) -> nil()
Bounds Processor:
bound: 1
enrichment: match
automaton:
final states: {6,5,4}
transitions:
nil1() -> 29,28,4
cons1(2,34) -> 6*
cons1(3,29) -> 6*
cons1(1,4) -> 16*
cons1(1,34) -> 6*
cons1(3,4) -> 14*
cons1(2,29) -> 6*
cons1(3,34) -> 6*
cons1(2,4) -> 14*
cons1(1,29) -> 6*
append1(3,15) -> 33,5
append1(3,17) -> 33,5
append1(2,15) -> 33,5
append1(2,17) -> 33,5
append1(4,15) -> 15*
append1(4,17) -> 17*
append1(1,15) -> 33,5
append1(1,17) -> 33,5
rev1(2) -> 33*
rev1(14) -> 15*
rev1(16) -> 17*
rev1(1) -> 28*
rev1(3) -> 28*
shuffle1(33) -> 34*
shuffle1(28) -> 29*
app0(3,1) -> 4*
app0(3,3) -> 4*
app0(1,2) -> 4*
app0(2,1) -> 4*
app0(2,3) -> 4*
app0(3,2) -> 4*
app0(1,1) -> 4*
app0(1,3) -> 4*
app0(2,2) -> 4*
nil0() -> 6,5,1
cons0(3,1) -> 2*
cons0(3,3) -> 2*
cons0(1,2) -> 2*
cons0(1,4) -> 4*
cons0(2,1) -> 2*
cons0(2,3) -> 2*
cons0(3,2) -> 2*
cons0(3,4) -> 4*
cons0(1,1) -> 2*
cons0(1,3) -> 2*
cons0(2,2) -> 2*
cons0(2,4) -> 4*
rev0(2) -> 5*
rev0(1) -> 5*
rev0(3) -> 5*
append0(3,1) -> 3*
append0(3,3) -> 3*
append0(1,2) -> 3*
append0(2,1) -> 3*
append0(2,3) -> 3*
append0(3,2) -> 3*
append0(1,1) -> 3*
append0(1,3) -> 3*
append0(2,2) -> 3*
shuffle0(2) -> 6*
shuffle0(1) -> 6*
shuffle0(3) -> 6*
problem:
strict:
app(cons(x,xs),ys) -> cons(x,app(xs,ys))
rev(cons(x,xs)) -> append(xs,rev(cons(x,nil())))
weak:
app(nil(),xs) -> nil()
rev(nil()) -> nil()
shuffle(cons(x,xs)) -> cons(x,shuffle(rev(xs)))
shuffle(nil()) -> nil()
Bounds Processor:
bound: 1
enrichment: match
automaton:
final states: {6,5,4}
transitions:
nil1() -> 58,57,7,37
cons1(1,37) -> 42*
cons1(3,7) -> 7,4
cons1(3,11) -> 7,4
cons1(1,65) -> 6*
cons1(3,37) -> 38*
cons1(2,58) -> 6*
cons1(3,65) -> 6*
cons1(2,7) -> 7,4
cons1(2,11) -> 7,4
cons1(2,37) -> 38*
cons1(1,58) -> 6*
cons1(2,65) -> 6*
cons1(3,58) -> 6*
cons1(1,7) -> 7,4
cons1(1,11) -> 7,4
app1(3,1) -> 7*
app1(3,3) -> 7*
app1(1,2) -> 7*
app1(2,1) -> 7*
app1(2,3) -> 11*
app1(3,2) -> 7*
app1(1,1) -> 7*
app1(1,3) -> 7*
app1(2,2) -> 7*
append1(1,39) -> 57,5
append1(1,43) -> 57,5
append1(3,39) -> 57,5
append1(3,43) -> 57,5
append1(37,39) -> 39*
append1(37,43) -> 43*
append1(2,39) -> 57,5
append1(2,43) -> 57,5
rev1(42) -> 43*
rev1(2) -> 64*
rev1(1) -> 57*
rev1(38) -> 39*
rev1(3) -> 57*
shuffle1(57) -> 58*
shuffle1(64) -> 65*
app0(3,1) -> 4*
app0(3,3) -> 4*
app0(1,2) -> 4*
app0(2,1) -> 4*
app0(2,3) -> 4*
app0(3,2) -> 4*
app0(1,1) -> 4*
app0(1,3) -> 4*
app0(2,2) -> 4*
nil0() -> 6,5,4,3
cons0(3,1) -> 1*
cons0(3,3) -> 1*
cons0(1,2) -> 1*
cons0(2,1) -> 1*
cons0(2,3) -> 1*
cons0(3,2) -> 1*
cons0(1,1) -> 1*
cons0(1,3) -> 1*
cons0(2,2) -> 1*
rev0(2) -> 5*
rev0(1) -> 5*
rev0(3) -> 5*
append0(3,1) -> 2*
append0(3,3) -> 2*
append0(1,2) -> 2*
append0(2,1) -> 2*
append0(2,3) -> 2*
append0(3,2) -> 2*
append0(1,1) -> 2*
append0(1,3) -> 2*
append0(2,2) -> 2*
shuffle0(2) -> 6*
shuffle0(1) -> 6*
shuffle0(3) -> 6*
problem:
strict:
rev(cons(x,xs)) -> append(xs,rev(cons(x,nil())))
weak:
app(cons(x,xs),ys) -> cons(x,app(xs,ys))
app(nil(),xs) -> nil()
rev(nil()) -> nil()
shuffle(cons(x,xs)) -> cons(x,shuffle(rev(xs)))
shuffle(nil()) -> nil()
Open
Tool IRC1
stdout:
MAYBE
Tool IRC2
stdout:
TIMEOUT
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: TIMEOUT
Input Problem: innermost runtime-complexity with respect to
Rules:
{ app(nil(), xs) -> nil()
, app(cons(x, xs), ys) -> cons(x, app(xs, ys))
, rev(nil()) -> nil()
, rev(cons(x, xs)) -> append(xs, rev(cons(x, nil())))
, shuffle(nil()) -> nil()
, shuffle(cons(x, xs)) -> cons(x, shuffle(rev(xs)))}
Proof Output:
Computation stopped due to timeout after 60.0 secondsTool RC1
stdout:
MAYBE
Tool RC2
stdout:
TIMEOUT
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: TIMEOUT
Input Problem: runtime-complexity with respect to
Rules:
{ app(nil(), xs) -> nil()
, app(cons(x, xs), ys) -> cons(x, app(xs, ys))
, rev(nil()) -> nil()
, rev(cons(x, xs)) -> append(xs, rev(cons(x, nil())))
, shuffle(nil()) -> nil()
, shuffle(cons(x, xs)) -> cons(x, shuffle(rev(xs)))}
Proof Output:
Computation stopped due to timeout after 60.0 secondsTool pair1rc
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ app(nil(), xs) -> nil()
, app(cons(x, xs), ys) -> cons(x, app(xs, ys))
, rev(nil()) -> nil()
, rev(cons(x, xs)) -> append(xs, rev(cons(x, nil())))
, shuffle(nil()) -> nil()
, shuffle(cons(x, xs)) -> cons(x, shuffle(rev(xs)))}
StartTerms: basic terms
Strategy: none
Certificate: TIMEOUT
Application of 'pair1 (timeout of 60.0 seconds)':
-------------------------------------------------
Computation stopped due to timeout after 60.0 seconds
Arrrr..Tool pair2rc
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ app(nil(), xs) -> nil()
, app(cons(x, xs), ys) -> cons(x, app(xs, ys))
, rev(nil()) -> nil()
, rev(cons(x, xs)) -> append(xs, rev(cons(x, nil())))
, shuffle(nil()) -> nil()
, shuffle(cons(x, xs)) -> cons(x, shuffle(rev(xs)))}
StartTerms: basic terms
Strategy: none
Certificate: TIMEOUT
Application of 'pair2 (timeout of 60.0 seconds)':
-------------------------------------------------
Computation stopped due to timeout after 60.0 seconds
Arrrr..Tool pair3irc
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ app(nil(), xs) -> nil()
, app(cons(x, xs), ys) -> cons(x, app(xs, ys))
, rev(nil()) -> nil()
, rev(cons(x, xs)) -> append(xs, rev(cons(x, nil())))
, shuffle(nil()) -> nil()
, shuffle(cons(x, xs)) -> cons(x, shuffle(rev(xs)))}
StartTerms: basic terms
Strategy: innermost
Certificate: TIMEOUT
Application of 'pair3 (timeout of 60.0 seconds)':
-------------------------------------------------
Computation stopped due to timeout after 60.0 seconds
Arrrr..Tool pair3rc
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ app(nil(), xs) -> nil()
, app(cons(x, xs), ys) -> cons(x, app(xs, ys))
, rev(nil()) -> nil()
, rev(cons(x, xs)) -> append(xs, rev(cons(x, nil())))
, shuffle(nil()) -> nil()
, shuffle(cons(x, xs)) -> cons(x, shuffle(rev(xs)))}
StartTerms: basic terms
Strategy: none
Certificate: TIMEOUT
Application of 'pair3 (timeout of 60.0 seconds)':
-------------------------------------------------
Computation stopped due to timeout after 60.0 seconds
Arrrr..Tool rc
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ app(nil(), xs) -> nil()
, app(cons(x, xs), ys) -> cons(x, app(xs, ys))
, rev(nil()) -> nil()
, rev(cons(x, xs)) -> append(xs, rev(cons(x, nil())))
, shuffle(nil()) -> nil()
, shuffle(cons(x, xs)) -> cons(x, shuffle(rev(xs)))}
StartTerms: basic terms
Strategy: none
Certificate: TIMEOUT
Application of 'rc (timeout of 60.0 seconds)':
----------------------------------------------
Computation stopped due to timeout after 60.0 seconds
Arrrr..Tool tup3irc
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ app(nil(), xs) -> nil()
, app(cons(x, xs), ys) -> cons(x, app(xs, ys))
, rev(nil()) -> nil()
, rev(cons(x, xs)) -> append(xs, rev(cons(x, nil())))
, shuffle(nil()) -> nil()
, shuffle(cons(x, xs)) -> cons(x, shuffle(rev(xs)))}
StartTerms: basic terms
Strategy: innermost
Certificate: TIMEOUT
Application of 'tup3 (timeout of 60.0 seconds)':
------------------------------------------------
Computation stopped due to timeout after 60.0 seconds
Arrrr..