Problem Mixed TRS jones2

YES(?,O(n^2))

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

Strict Trs:
  { f(empty(), l) -> l
  , f(cons(x, k), l) -> g(k, l, cons(x, k))
  , g(a, b, c) -> f(a, cons(b, c)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^2))

The following argument positions are usable:
  Uargs(f) = {}, Uargs(cons) = {}, Uargs(g) = {}
TcT has computed following constructor-restricted polynomial
interpretation.
    [f](x1, x2) = 1 + x1 + 3*x1^2 + x2  
                                        
      [empty]() = 0                     
                                        
 [cons](x1, x2) = 1 + x2                
                                        
[g](x1, x2, x3) = 3 + 2*x1 + 3*x1^2 + x3
                                        

This order satisfies following ordering constraints

     [f(empty(), l)] = 1 + l                
                     > l                    
                     = [l]                  
                                            
  [f(cons(x, k), l)] = 5 + 7*k + 3*k^2 + l  
                     > 4 + 3*k + 3*k^2      
                     = [g(k, l, cons(x, k))]
                                            
        [g(a, b, c)] = 3 + 2*a + 3*a^2 + c  
                     > 2 + a + 3*a^2 + c    
                     = [f(a, cons(b, c))]   
                                            

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

MAYBE

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

Strict Trs:
  { f(empty(), l) -> l
  , f(cons(x, k), l) -> g(k, l, cons(x, k))
  , g(a, b, c) -> f(a, cons(b, c)) }
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:
  { f(empty(), l) -> l
  , f(cons(x, k), l) -> g(k, l, cons(x, k))
  , g(a, b, c) -> f(a, cons(b, c)) }
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:
  { f(empty(), l) -> l
  , f(cons(x, k), l) -> g(k, l, cons(x, k))
  , g(a, b, c) -> f(a, cons(b, c)) }
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:
  { f(empty(), l) -> l
  , f(cons(x, k), l) -> g(k, l, cons(x, k))
  , g(a, b, c) -> f(a, cons(b, c)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..