Problem SK90 2.37

YES(?,O(n^1))

We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).

Strict Trs:
  { and(not(not(x)), y, not(z)) -> and(y, band(x, z), x) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

The following argument positions are usable:
  Uargs(and) = {}, Uargs(not) = {}, Uargs(band) = {}

TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).

  [and](x1, x2, x3) = [1] x1 + [1] x2 + [0]
                                           
          [not](x1) = [1] x1 + [2]
                                  
     [band](x1, x2) = [3]

This order satisfies following ordering constraints

  [and(not(not(x)), y, not(z))] = [1] x + [1] y + [4]    
                                > [1] y + [3]            
                                = [and(y, band(x, z), x)]
                                                         

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

MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict Trs:
  { and(not(not(x)), y, not(z)) -> and(y, band(x, z), x) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..

MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict Trs:
  { and(not(not(x)), y, not(z)) -> and(y, band(x, z), x) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..

MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict Trs:
  { and(not(not(x)), y, not(z)) -> and(y, band(x, z), x) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..

MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict Trs:
  { and(not(not(x)), y, not(z)) -> and(y, band(x, z), x) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..