Problem ICFP 2010 264405

LMPO

Execution Time (secs)
0.083
Answer
MAYBE
InputICFP 2010 264405
MAYBE

We consider the following Problem:

  Strict Trs:
    {  0(1(2(3(4(x1))))) -> 0(2(3(1(4(x1)))))
     , 0(5(1(2(3(4(x1)))))) -> 0(1(2(5(3(4(x1))))))
     , 0(5(1(2(3(4(x1)))))) -> 0(5(2(1(3(4(x1))))))
     , 0(5(1(2(3(4(x1)))))) -> 5(0(2(3(1(4(x1))))))
     , 0(5(2(3(1(4(x1)))))) -> 0(1(5(2(3(4(x1))))))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MPO

Execution Time (secs)
0.175
Answer
YES(?,PRIMREC)
InputICFP 2010 264405
YES(?,PRIMREC)

We consider the following Problem:

  Strict Trs:
    {  0(1(2(3(4(x1))))) -> 0(2(3(1(4(x1)))))
     , 0(5(1(2(3(4(x1)))))) -> 0(1(2(5(3(4(x1))))))
     , 0(5(1(2(3(4(x1)))))) -> 0(5(2(1(3(4(x1))))))
     , 0(5(1(2(3(4(x1)))))) -> 5(0(2(3(1(4(x1))))))
     , 0(5(2(3(1(4(x1)))))) -> 0(1(5(2(3(4(x1))))))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: YES(?,PRIMREC)

Proof:
  The input was oriented with the instance of
  'multiset path orders' as induced by the precedence
  
   1 > 2, 1 > 3, 5 > 1, 5 > 2, 0 ~ 5 .

Hurray, we answered YES(?,PRIMREC)

POP*

Execution Time (secs)
0.114
Answer
MAYBE
InputICFP 2010 264405
MAYBE

We consider the following Problem:

  Strict Trs:
    {  0(1(2(3(4(x1))))) -> 0(2(3(1(4(x1)))))
     , 0(5(1(2(3(4(x1)))))) -> 0(1(2(5(3(4(x1))))))
     , 0(5(1(2(3(4(x1)))))) -> 0(5(2(1(3(4(x1))))))
     , 0(5(1(2(3(4(x1)))))) -> 5(0(2(3(1(4(x1))))))
     , 0(5(2(3(1(4(x1)))))) -> 0(1(5(2(3(4(x1))))))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

POP* (PS)

Execution Time (secs)
0.079
Answer
MAYBE
InputICFP 2010 264405
MAYBE

We consider the following Problem:

  Strict Trs:
    {  0(1(2(3(4(x1))))) -> 0(2(3(1(4(x1)))))
     , 0(5(1(2(3(4(x1)))))) -> 0(1(2(5(3(4(x1))))))
     , 0(5(1(2(3(4(x1)))))) -> 0(5(2(1(3(4(x1))))))
     , 0(5(1(2(3(4(x1)))))) -> 5(0(2(3(1(4(x1))))))
     , 0(5(2(3(1(4(x1)))))) -> 0(1(5(2(3(4(x1))))))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

Small POP*

Execution Time (secs)
0.086
Answer
MAYBE
InputICFP 2010 264405
MAYBE

We consider the following Problem:

  Strict Trs:
    {  0(1(2(3(4(x1))))) -> 0(2(3(1(4(x1)))))
     , 0(5(1(2(3(4(x1)))))) -> 0(1(2(5(3(4(x1))))))
     , 0(5(1(2(3(4(x1)))))) -> 0(5(2(1(3(4(x1))))))
     , 0(5(1(2(3(4(x1)))))) -> 5(0(2(3(1(4(x1))))))
     , 0(5(2(3(1(4(x1)))))) -> 0(1(5(2(3(4(x1))))))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

Small POP* (PS)

Execution Time (secs)
0.079
Answer
MAYBE
InputICFP 2010 264405
MAYBE

We consider the following Problem:

  Strict Trs:
    {  0(1(2(3(4(x1))))) -> 0(2(3(1(4(x1)))))
     , 0(5(1(2(3(4(x1)))))) -> 0(1(2(5(3(4(x1))))))
     , 0(5(1(2(3(4(x1)))))) -> 0(5(2(1(3(4(x1))))))
     , 0(5(1(2(3(4(x1)))))) -> 5(0(2(3(1(4(x1))))))
     , 0(5(2(3(1(4(x1)))))) -> 0(1(5(2(3(4(x1))))))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..