Problem SK90 4.47

LMPO

Execution Time (secs)
0.103
Answer
MAYBE
InputSK90 4.47
MAYBE

We consider the following Problem:

  Strict Trs:
    {  f(g(i(a(), b(), b'()), c()), d()) ->
       if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))
     , f(g(h(a(), b()), c()), d()) ->
       if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MPO

Execution Time (secs)
0.166
Answer
MAYBE
InputSK90 4.47
MAYBE

We consider the following Problem:

  Strict Trs:
    {  f(g(i(a(), b(), b'()), c()), d()) ->
       if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))
     , f(g(h(a(), b()), c()), d()) ->
       if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

POP*

Execution Time (secs)
0.098
Answer
MAYBE
InputSK90 4.47
MAYBE

We consider the following Problem:

  Strict Trs:
    {  f(g(i(a(), b(), b'()), c()), d()) ->
       if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))
     , f(g(h(a(), b()), c()), d()) ->
       if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

POP* (PS)

Execution Time (secs)
0.098
Answer
MAYBE
InputSK90 4.47
MAYBE

We consider the following Problem:

  Strict Trs:
    {  f(g(i(a(), b(), b'()), c()), d()) ->
       if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))
     , f(g(h(a(), b()), c()), d()) ->
       if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

Small POP*

Execution Time (secs)
0.113
Answer
MAYBE
InputSK90 4.47
MAYBE

We consider the following Problem:

  Strict Trs:
    {  f(g(i(a(), b(), b'()), c()), d()) ->
       if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))
     , f(g(h(a(), b()), c()), d()) ->
       if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

Small POP* (PS)

Execution Time (secs)
0.140
Answer
MAYBE
InputSK90 4.47
MAYBE

We consider the following Problem:

  Strict Trs:
    {  f(g(i(a(), b(), b'()), c()), d()) ->
       if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))
     , f(g(h(a(), b()), c()), d()) ->
       if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..