Problem Zantema 04 z092

Tool Bounds

Execution Time60.05269ms
Answer
TIMEOUT
InputZantema 04 z092

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  q3(b(x1)) -> b(q4(x1))
     , q3(1'(x1)) -> 1'(q3(x1))
     , q0(1'(x1)) -> 1'(q3(x1))
     , q2(0'(x1)) -> 0'(q0(x1))
     , 1'(q2(1'(x1))) -> q2(1'(1'(x1)))
     , 0'(q2(1'(x1))) -> q2(0'(1'(x1)))
     , 0(q2(1'(x1))) -> q2(0(1'(x1)))
     , 1'(q2(0(x1))) -> q2(1'(0(x1)))
     , 0'(q2(0(x1))) -> q2(0'(0(x1)))
     , 0(q2(0(x1))) -> q2(0(0(x1)))
     , 1'(q1(1(x1))) -> q2(1'(1'(x1)))
     , 0'(q1(1(x1))) -> q2(0'(1'(x1)))
     , 0(q1(1(x1))) -> q2(0(1'(x1)))
     , q1(1'(x1)) -> 1'(q1(x1))
     , q1(0(x1)) -> 0(q1(x1))
     , q0(0(x1)) -> 0'(q1(x1))}
  StartTerms: all
  Strategy: none

Certificate: TIMEOUT

Proof:
  Computation stopped due to timeout after 60.0 seconds.

Arrrr..

Tool CDI

Execution Time41.9128ms
Answer
YES(?,O(n^2))
InputZantema 04 z092

stdout:

YES(?,O(n^2))
QUADRATIC upper bound on the derivational complexity

This TRS is terminating using the deltarestricted interpretation
q4(delta, X0) =  + 0*X0 + 0 + 1*X0*delta + 0*delta
b(delta, X0) =  + 0*X0 + 2 + 1*X0*delta + 0*delta
q3(delta, X0) =  + 1*X0 + 0 + 1*X0*delta + 0*delta
1(delta, X0) =  + 1*X0 + 3 + 1*X0*delta + 1*delta
q2(delta, X0) =  + 1*X0 + 2 + 1*X0*delta + 0*delta
1'(delta, X0) =  + 1*X0 + 1 + 2*X0*delta + 0*delta
0(delta, X0) =  + 1*X0 + 1 + 2*X0*delta + 3*delta
q0(delta, X0) =  + 1*X0 + 0 + 1*X0*delta + 0*delta
q1(delta, X0) =  + 1*X0 + 0 + 2*X0*delta + 0*delta
0'(delta, X0) =  + 1*X0 + 1 + 1*X0*delta + 1*delta
q4_tau_1(delta) = delta/(0 + 1 * delta)
b_tau_1(delta) = delta/(0 + 1 * delta)
q3_tau_1(delta) = delta/(1 + 1 * delta)
1_tau_1(delta) = delta/(1 + 1 * delta)
q2_tau_1(delta) = delta/(1 + 1 * delta)
1'_tau_1(delta) = delta/(1 + 2 * delta)
0_tau_1(delta) = delta/(1 + 2 * delta)
q0_tau_1(delta) = delta/(1 + 1 * delta)
q1_tau_1(delta) = delta/(1 + 2 * delta)
0'_tau_1(delta) = delta/(1 + 1 * delta)

Time: 41.871522 seconds
Statistics:
Number of monomials: 3221
Last formula building started for bound 3
Last SAT solving started for bound 3

Tool EDA

Execution Time1.914304ms
Answer
YES(?,O(n^2))
InputZantema 04 z092

stdout:

YES(?,O(n^2))

We consider the following Problem:

  Strict Trs:
    {  q3(b(x1)) -> b(q4(x1))
     , q3(1'(x1)) -> 1'(q3(x1))
     , q0(1'(x1)) -> 1'(q3(x1))
     , q2(0'(x1)) -> 0'(q0(x1))
     , 1'(q2(1'(x1))) -> q2(1'(1'(x1)))
     , 0'(q2(1'(x1))) -> q2(0'(1'(x1)))
     , 0(q2(1'(x1))) -> q2(0(1'(x1)))
     , 1'(q2(0(x1))) -> q2(1'(0(x1)))
     , 0'(q2(0(x1))) -> q2(0'(0(x1)))
     , 0(q2(0(x1))) -> q2(0(0(x1)))
     , 1'(q1(1(x1))) -> q2(1'(1'(x1)))
     , 0'(q1(1(x1))) -> q2(0'(1'(x1)))
     , 0(q1(1(x1))) -> q2(0(1'(x1)))
     , q1(1'(x1)) -> 1'(q1(x1))
     , q1(0(x1)) -> 0(q1(x1))
     , q0(0(x1)) -> 0'(q1(x1))}
  StartTerms: all
  Strategy: none

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

Proof:
  We have the following EDA-non-satisfying matrix interpretation:
  Interpretation Functions:
   0(x1) = [1 2] x1 + [0]
           [0 1]      [3]
   q0(x1) = [1 1] x1 + [0]
            [0 1]      [0]
   q1(x1) = [1 2] x1 + [0]
            [0 1]      [1]
   0'(x1) = [1 1] x1 + [0]
            [0 1]      [2]
   1'(x1) = [1 1] x1 + [0]
            [0 1]      [1]
   1(x1) = [1 2] x1 + [0]
           [0 1]      [3]
   q2(x1) = [1 1] x1 + [0]
            [0 1]      [3]
   q3(x1) = [1 1] x1 + [0]
            [0 1]      [0]
   b(x1) = [1 0] x1 + [0]
           [0 0]      [1]
   q4(x1) = [1 0] x1 + [0]
            [0 0]      [3]

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

Tool IDA

Execution Time2.789418ms
Answer
YES(?,O(n^2))
InputZantema 04 z092

stdout:

YES(?,O(n^2))

We consider the following Problem:

  Strict Trs:
    {  q3(b(x1)) -> b(q4(x1))
     , q3(1'(x1)) -> 1'(q3(x1))
     , q0(1'(x1)) -> 1'(q3(x1))
     , q2(0'(x1)) -> 0'(q0(x1))
     , 1'(q2(1'(x1))) -> q2(1'(1'(x1)))
     , 0'(q2(1'(x1))) -> q2(0'(1'(x1)))
     , 0(q2(1'(x1))) -> q2(0(1'(x1)))
     , 1'(q2(0(x1))) -> q2(1'(0(x1)))
     , 0'(q2(0(x1))) -> q2(0'(0(x1)))
     , 0(q2(0(x1))) -> q2(0(0(x1)))
     , 1'(q1(1(x1))) -> q2(1'(1'(x1)))
     , 0'(q1(1(x1))) -> q2(0'(1'(x1)))
     , 0(q1(1(x1))) -> q2(0(1'(x1)))
     , q1(1'(x1)) -> 1'(q1(x1))
     , q1(0(x1)) -> 0(q1(x1))
     , q0(0(x1)) -> 0'(q1(x1))}
  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:
   0(x1) = [1 2] x1 + [0]
           [0 1]      [2]
   q0(x1) = [1 2] x1 + [0]
            [0 1]      [0]
   q1(x1) = [1 2] x1 + [0]
            [0 1]      [1]
   0'(x1) = [1 1] x1 + [0]
            [0 1]      [1]
   1'(x1) = [1 1] x1 + [2]
            [0 1]      [1]
   1(x1) = [1 2] x1 + [0]
           [0 1]      [3]
   q2(x1) = [1 2] x1 + [0]
            [0 1]      [3]
   q3(x1) = [1 2] x1 + [0]
            [0 1]      [0]
   b(x1) = [1 0] x1 + [0]
           [0 0]      [2]
   q4(x1) = [1 0] x1 + [0]
            [0 0]      [3]

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

Tool TRI

Execution Time0.858201ms
Answer
YES(?,O(n^2))
InputZantema 04 z092

stdout:

YES(?,O(n^2))

We consider the following Problem:

  Strict Trs:
    {  q3(b(x1)) -> b(q4(x1))
     , q3(1'(x1)) -> 1'(q3(x1))
     , q0(1'(x1)) -> 1'(q3(x1))
     , q2(0'(x1)) -> 0'(q0(x1))
     , 1'(q2(1'(x1))) -> q2(1'(1'(x1)))
     , 0'(q2(1'(x1))) -> q2(0'(1'(x1)))
     , 0(q2(1'(x1))) -> q2(0(1'(x1)))
     , 1'(q2(0(x1))) -> q2(1'(0(x1)))
     , 0'(q2(0(x1))) -> q2(0'(0(x1)))
     , 0(q2(0(x1))) -> q2(0(0(x1)))
     , 1'(q1(1(x1))) -> q2(1'(1'(x1)))
     , 0'(q1(1(x1))) -> q2(0'(1'(x1)))
     , 0(q1(1(x1))) -> q2(0(1'(x1)))
     , q1(1'(x1)) -> 1'(q1(x1))
     , q1(0(x1)) -> 0(q1(x1))
     , q0(0(x1)) -> 0'(q1(x1))}
  StartTerms: all
  Strategy: none

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

Proof:
  We have the following triangular matrix interpretation:
  Interpretation Functions:
   0(x1) = [1 2] x1 + [1]
           [0 1]      [1]
   q0(x1) = [1 1] x1 + [0]
            [0 1]      [0]
   q1(x1) = [1 2] x1 + [0]
            [0 1]      [0]
   0'(x1) = [1 1] x1 + [1]
            [0 1]      [1]
   1'(x1) = [1 1] x1 + [0]
            [0 1]      [1]
   1(x1) = [1 2] x1 + [0]
           [0 1]      [3]
   q2(x1) = [1 1] x1 + [0]
            [0 1]      [2]
   q3(x1) = [1 1] x1 + [0]
            [0 1]      [0]
   b(x1) = [1 3] x1 + [0]
           [0 1]      [1]
   q4(x1) = [1 1] x1 + [0]
            [0 1]      [0]

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

Tool TRI2

Execution Time0.837198ms
Answer
YES(?,O(n^2))
InputZantema 04 z092

stdout:

YES(?,O(n^2))

We consider the following Problem:

  Strict Trs:
    {  q3(b(x1)) -> b(q4(x1))
     , q3(1'(x1)) -> 1'(q3(x1))
     , q0(1'(x1)) -> 1'(q3(x1))
     , q2(0'(x1)) -> 0'(q0(x1))
     , 1'(q2(1'(x1))) -> q2(1'(1'(x1)))
     , 0'(q2(1'(x1))) -> q2(0'(1'(x1)))
     , 0(q2(1'(x1))) -> q2(0(1'(x1)))
     , 1'(q2(0(x1))) -> q2(1'(0(x1)))
     , 0'(q2(0(x1))) -> q2(0'(0(x1)))
     , 0(q2(0(x1))) -> q2(0(0(x1)))
     , 1'(q1(1(x1))) -> q2(1'(1'(x1)))
     , 0'(q1(1(x1))) -> q2(0'(1'(x1)))
     , 0(q1(1(x1))) -> q2(0(1'(x1)))
     , q1(1'(x1)) -> 1'(q1(x1))
     , q1(0(x1)) -> 0(q1(x1))
     , q0(0(x1)) -> 0'(q1(x1))}
  StartTerms: all
  Strategy: none

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

Proof:
  We have the following triangular matrix interpretation:
  Interpretation Functions:
   0(x1) = [1 3] x1 + [0]
           [0 1]      [1]
   q0(x1) = [1 1] x1 + [0]
            [0 1]      [0]
   q1(x1) = [1 2] x1 + [0]
            [0 1]      [0]
   0'(x1) = [1 2] x1 + [0]
            [0 1]      [1]
   1'(x1) = [1 3] x1 + [0]
            [0 1]      [2]
   1(x1) = [1 2] x1 + [2]
           [0 1]      [3]
   q2(x1) = [1 1] x1 + [0]
            [0 1]      [1]
   q3(x1) = [1 1] x1 + [0]
            [0 1]      [0]
   b(x1) = [1 3] x1 + [0]
           [0 1]      [1]
   q4(x1) = [1 1] x1 + [0]
            [0 1]      [0]

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