Problem Rubio 04 test4

Tool Bounds

Execution Time5.606389e-2ms
Answer
YES(?,O(n^1))
InputRubio 04 test4

stdout:

YES(?,O(n^1))

We consider the following Problem:

  Strict Trs:
    {  f(c(), c()) -> f(a(), a())
     , f(s(X), c()) -> f(X, c())
     , f(a(), b()) -> f(s(a()), c())
     , f(a(), a()) -> f(a(), b())}
  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:
  {  a_0() -> 1
   , a_1() -> 2
   , a_1() -> 3
   , a_2() -> 5
   , a_3() -> 10
   , f_0(1, 1) -> 1
   , f_1(1, 4) -> 1
   , f_1(2, 3) -> 1
   , f_1(3, 4) -> 1
   , f_2(3, 7) -> 1
   , f_2(5, 6) -> 1
   , f_2(5, 7) -> 1
   , f_3(5, 9) -> 1
   , f_3(8, 9) -> 1
   , f_4(10, 11) -> 1
   , b_0() -> 1
   , b_1() -> 3
   , b_2() -> 6
   , s_0(1) -> 1
   , s_1(3) -> 1
   , s_2(5) -> 3
   , s_3(10) -> 8
   , c_0() -> 1
   , c_1() -> 4
   , c_2() -> 7
   , c_3() -> 9
   , c_4() -> 11}

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

Tool CDI

Execution Time5.77376ms
Answer
MAYBE
InputRubio 04 test4

stdout:

MAYBE

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

Tool EDA

Execution Time0.398705ms
Answer
YES(?,O(n^2))
InputRubio 04 test4

stdout:

YES(?,O(n^2))

We consider the following Problem:

  Strict Trs:
    {  f(c(), c()) -> f(a(), a())
     , f(s(X), c()) -> f(X, c())
     , f(a(), b()) -> f(s(a()), c())
     , f(a(), a()) -> f(a(), b())}
  StartTerms: all
  Strategy: none

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

Proof:
  We have the following EDA-non-satisfying matrix interpretation:
  Interpretation Functions:
   a() = [3]
         [0]
   f(x1, x2) = [1 3] x1 + [1 0] x2 + [0]
               [0 0]      [0 0]      [0]
   b() = [2]
         [3]
   s(x1) = [1 3] x1 + [1]
           [0 0]      [0]
   c() = [0]
         [3]

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

Tool IDA

Execution Time0.6412101ms
Answer
YES(?,O(n^2))
InputRubio 04 test4

stdout:

YES(?,O(n^2))

We consider the following Problem:

  Strict Trs:
    {  f(c(), c()) -> f(a(), a())
     , f(s(X), c()) -> f(X, c())
     , f(a(), b()) -> f(s(a()), c())
     , f(a(), a()) -> f(a(), b())}
  StartTerms: all
  Strategy: none

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

Proof:
  We have the following EDA-non-satisfying and IDA(2)-non-satisfying matrix interpretation:
  Interpretation Functions:
   a() = [3]
         [0]
   f(x1, x2) = [1 3] x1 + [1 0] x2 + [0]
               [0 0]      [0 0]      [0]
   b() = [2]
         [3]
   s(x1) = [1 3] x1 + [1]
           [0 0]      [0]
   c() = [0]
         [3]

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

Tool TRI

Execution Time0.18579698ms
Answer
YES(?,O(n^1))
InputRubio 04 test4

stdout:

YES(?,O(n^1))

We consider the following Problem:

  Strict Trs:
    {  f(c(), c()) -> f(a(), a())
     , f(s(X), c()) -> f(X, c())
     , f(a(), b()) -> f(s(a()), c())
     , f(a(), a()) -> f(a(), b())}
  StartTerms: all
  Strategy: none

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

Proof:
  We have the following triangular matrix interpretation:
  Interpretation Functions:
   a() = [3]
         [0]
   f(x1, x2) = [1 3] x1 + [1 0] x2 + [0]
               [0 0]      [0 0]      [0]
   b() = [2]
         [3]
   s(x1) = [1 3] x1 + [1]
           [0 0]      [0]
   c() = [0]
         [3]

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

Tool TRI2

Execution Time0.19034505ms
Answer
YES(?,O(n^1))
InputRubio 04 test4

stdout:

YES(?,O(n^1))

We consider the following Problem:

  Strict Trs:
    {  f(c(), c()) -> f(a(), a())
     , f(s(X), c()) -> f(X, c())
     , f(a(), b()) -> f(s(a()), c())
     , f(a(), a()) -> f(a(), b())}
  StartTerms: all
  Strategy: none

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

Proof:
  We have the following triangular matrix interpretation:
  Interpretation Functions:
   a() = [3]
         [0]
   f(x1, x2) = [1 3] x1 + [1 0] x2 + [0]
               [0 0]      [0 0]      [0]
   b() = [2]
         [3]
   s(x1) = [1 3] x1 + [1]
           [0 0]      [0]
   c() = [0]
         [3]

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