Problem Zantema 05 z02

Tool Bounds

Execution Time	7.2429895e-2ms
Answer	YES(?,O(n^1))
Input	Zantema 05 z02

stdout:

YES(?,O(n^1))

We consider the following Problem:

  Strict Trs:
    {  a(x, g()) -> a(f(), a(g(), a(f(), x)))
     , a(f(), a(f(), x)) -> a(x, g())}
  StartTerms: all
  Strategy: none

Certificate: YES(?,O(n^1))

Proof:
  The problem is match-bounded by 4.
  The enriched problem is compatible with the following automaton:
  {  f_0() -> 1
   , f_1() -> 2
   , f_1() -> 6
   , f_2() -> 9
   , f_2() -> 12
   , f_3() -> 13
   , f_3() -> 17
   , f_4() -> 20
   , f_4() -> 24
   , a_0(1, 1) -> 1
   , a_1(1, 4) -> 1
   , a_1(1, 4) -> 5
   , a_1(1, 4) -> 11
   , a_1(2, 3) -> 1
   , a_1(3, 4) -> 1
   , a_1(4, 4) -> 1
   , a_1(4, 4) -> 5
   , a_1(4, 4) -> 11
   , a_1(4, 5) -> 3
   , a_1(4, 8) -> 1
   , a_1(4, 19) -> 18
   , a_1(6, 1) -> 5
   , a_1(6, 6) -> 8
   , a_1(6, 12) -> 19
   , a_1(6, 18) -> 11
   , a_1(10, 4) -> 1
   , a_2(3, 7) -> 5
   , a_2(3, 7) -> 11
   , a_2(7, 11) -> 10
   , a_2(9, 10) -> 1
   , a_2(10, 7) -> 5
   , a_2(12, 1) -> 11
   , a_2(12, 3) -> 11
   , a_2(12, 4) -> 11
   , a_2(12, 10) -> 5
   , a_2(12, 10) -> 11
   , a_2(12, 12) -> 11
   , a_3(10, 15) -> 11
   , a_3(13, 14) -> 5
   , a_3(15, 16) -> 14
   , a_3(17, 3) -> 16
   , a_3(17, 10) -> 16
   , a_3(17, 14) -> 11
   , a_4(20, 21) -> 11
   , a_4(22, 23) -> 21
   , a_4(24, 10) -> 23
   , g_0() -> 1
   , g_1() -> 4
   , g_2() -> 7
   , g_3() -> 15
   , g_4() -> 22}

Hurray, we answered YES(?,O(n^1))

Tool CDI

Execution Time	15.803678ms
Answer	MAYBE
Input	Zantema 05 z02

stdout:

MAYBE

Statistics:
Number of monomials: 774
Last formula building started for bound 3
Last SAT solving started for bound 3

Tool EDA

Execution Time	46.30514ms
Answer	MAYBE
Input	Zantema 05 z02

stdout:

Tool IDA

Execution Time	16.177359ms
Answer	MAYBE
Input	Zantema 05 z02

stdout:

MAYBE

We consider the following Problem:

  Strict Trs:
    {  a(x, g()) -> a(f(), a(g(), a(f(), x)))
     , a(f(), a(f(), x)) -> a(x, g())}
  StartTerms: all
  Strategy: none

Certificate: MAYBE

Proof:
  None of the processors succeeded.

  Details of failed attempt(s):
  -----------------------------
    1) 'matrix-interpretation of dimension 4' failed due to the following reason:
         The input cannot be shown compatible

    2) 'matrix-interpretation of dimension 4' failed due to the following reason:
         The input cannot be shown compatible

    3) 'matrix-interpretation of dimension 4' failed due to the following reason:
         The input cannot be shown compatible

    4) 'matrix-interpretation of dimension 4' failed due to the following reason:
         The input cannot be shown compatible

    5) 'matrix-interpretation of dimension 3' failed due to the following reason:
         The input cannot be shown compatible

    6) 'matrix-interpretation of dimension 3' failed due to the following reason:
         The input cannot be shown compatible

    7) 'matrix-interpretation of dimension 3' failed due to the following reason:
         The input cannot be shown compatible

    8) 'matrix-interpretation of dimension 2' failed due to the following reason:
         The input cannot be shown compatible

    9) 'matrix-interpretation of dimension 2' failed due to the following reason:
         The input cannot be shown compatible

    10) 'matrix-interpretation of dimension 1' failed due to the following reason:
          The input cannot be shown compatible


Arrrr..

Tool TRI

Execution Time	4.8580904ms
Answer	MAYBE
Input	Zantema 05 z02

stdout:

Tool TRI2

Execution Time	0.13107395ms
Answer	MAYBE
Input	Zantema 05 z02