Problem Mixed CTRS quick

Tool CaT

Execution TimeUnknown
Answer
MAYBE
InputMixed CTRS quick

stdout:

MAYBE

Problem:
 test(x_0,y) -> True()
 test(x_0,y) -> False()
 append(l1_2,l2_1) -> match_0(l1_2,l2_1,l1_2)
 match_0(l1_2,l2_1,Nil()) -> l2_1
 match_0(l1_2,l2_1,Cons(x,l)) -> Cons(x,append(l,l2_1))
 part(a_4,l_3) -> match_1(a_4,l_3,l_3)
 match_1(a_4,l_3,Nil()) -> Pair(Nil(),Nil())
 match_1(a_4,l_3,Cons(x,l')) -> match_2(x,l',a_4,l_3,part(a_4,l'))
 match_2(x,l',a_4,l_3,Pair(l1,l2)) -> match_3(l1,l2,x,l',a_4,l_3,test(a_4,x))
 match_3(l1,l2,x,l',a_4,l_3,False()) -> Pair(Cons(x,l1),l2)
 match_3(l1,l2,x,l',a_4,l_3,True()) -> Pair(l1,Cons(x,l2))
 quick(l_5) -> match_4(l_5,l_5)
 match_4(l_5,Nil()) -> Nil()
 match_4(l_5,Cons(a,l')) -> match_5(a,l',l_5,part(a,l'))
 match_5(a,l',l_5,Pair(l1,l2)) -> append(quick(l1),Cons(a,quick(l2)))

Proof:
 Open

Tool IRC1

Execution TimeUnknown
Answer
MAYBE
InputMixed CTRS quick

stdout:

MAYBE

Tool IRC2

Execution TimeUnknown
Answer
TIMEOUT
InputMixed CTRS quick

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  test(x_0, y) -> True()
     , test(x_0, y) -> False()
     , append(l1_2, l2_1) -> match_0(l1_2, l2_1, l1_2)
     , match_0(l1_2, l2_1, Nil()) -> l2_1
     , match_0(l1_2, l2_1, Cons(x, l)) -> Cons(x, append(l, l2_1))
     , part(a_4, l_3) -> match_1(a_4, l_3, l_3)
     , match_1(a_4, l_3, Nil()) -> Pair(Nil(), Nil())
     , match_1(a_4, l_3, Cons(x, l')) ->
       match_2(x, l', a_4, l_3, part(a_4, l'))
     , match_2(x, l', a_4, l_3, Pair(l1, l2)) ->
       match_3(l1, l2, x, l', a_4, l_3, test(a_4, x))
     , match_3(l1, l2, x, l', a_4, l_3, False()) ->
       Pair(Cons(x, l1), l2)
     , match_3(l1, l2, x, l', a_4, l_3, True()) -> Pair(l1, Cons(x, l2))
     , quick(l_5) -> match_4(l_5, l_5)
     , match_4(l_5, Nil()) -> Nil()
     , match_4(l_5, Cons(a, l')) -> match_5(a, l', l_5, part(a, l'))
     , match_5(a, l', l_5, Pair(l1, l2)) ->
       append(quick(l1), Cons(a, quick(l2)))}

Proof Output:    
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution TimeUnknown
Answer
MAYBE
InputMixed CTRS quick

stdout:

MAYBE

Tool RC2

Execution TimeUnknown
Answer
TIMEOUT
InputMixed CTRS quick

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  test(x_0, y) -> True()
     , test(x_0, y) -> False()
     , append(l1_2, l2_1) -> match_0(l1_2, l2_1, l1_2)
     , match_0(l1_2, l2_1, Nil()) -> l2_1
     , match_0(l1_2, l2_1, Cons(x, l)) -> Cons(x, append(l, l2_1))
     , part(a_4, l_3) -> match_1(a_4, l_3, l_3)
     , match_1(a_4, l_3, Nil()) -> Pair(Nil(), Nil())
     , match_1(a_4, l_3, Cons(x, l')) ->
       match_2(x, l', a_4, l_3, part(a_4, l'))
     , match_2(x, l', a_4, l_3, Pair(l1, l2)) ->
       match_3(l1, l2, x, l', a_4, l_3, test(a_4, x))
     , match_3(l1, l2, x, l', a_4, l_3, False()) ->
       Pair(Cons(x, l1), l2)
     , match_3(l1, l2, x, l', a_4, l_3, True()) -> Pair(l1, Cons(x, l2))
     , quick(l_5) -> match_4(l_5, l_5)
     , match_4(l_5, Nil()) -> Nil()
     , match_4(l_5, Cons(a, l')) -> match_5(a, l', l_5, part(a, l'))
     , match_5(a, l', l_5, Pair(l1, l2)) ->
       append(quick(l1), Cons(a, quick(l2)))}

Proof Output:    
  Computation stopped due to timeout after 60.0 seconds