Problem Transformed CSR 04 Ex9 Luc06 C

Tool CaT

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	Transformed CSR 04 Ex9 Luc06 C

stdout:

YES(?,O(n^1))

Problem:
active(f(a(),X,X)) -> mark(f(X,b(),b()))
active(b()) -> mark(a())
active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
proper(a()) -> ok(a())
proper(b()) -> ok(b())
f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))

Proof:
Complexity Transformation Processor:
  strict:
   active(f(a(),X,X)) -> mark(f(X,b(),b()))
   active(b()) -> mark(a())
   active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
   f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
   proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
   proper(a()) -> ok(a())
   proper(b()) -> ok(b())
   f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
   top(mark(X)) -> top(proper(X))
   top(ok(X)) -> top(active(X))
  weak:

  Matrix Interpretation Processor:
   dimension: 3
   max_matrix:
    [1 1 1]
    [0 0 1]
    [0 0 0]
    interpretation:
                 [1 0 0]     [0]
     [top](x0) = [0 0 0]x0 + [0]
                 [0 0 0]     [1],

                [1 1 0]
     [ok](x0) = [0 0 1]x0
                [0 0 0]  ,

                    [1 0 0]
     [proper](x0) = [0 0 1]x0
                    [0 0 0]  ,

                  [1 0 0]
     [mark](x0) = [0 0 0]x0
                  [0 0 0]  ,

           [0]
     [b] = [0]
           [0],

                    [1 0 0]
     [active](x0) = [0 0 0]x0
                    [0 0 0]  ,

                       [1 1 1]     [1 0 0]     [1 1 1]
     [f](x0, x1, x2) = [0 0 0]x0 + [0 0 0]x1 + [0 0 0]x2
                       [0 0 0]     [0 0 0]     [0 0 0]  ,

           [0]
     [a] = [0]
           [1]
    orientation:
                          [2 1 1]    [1]    [1 1 1]
     active(f(a(),X,X)) = [0 0 0]X + [0] >= [0 0 0]X = mark(f(X,b(),b()))
                          [0 0 0]    [0]    [0 0 0]

                   [0]    [0]
     active(b()) = [0] >= [0] = mark(a())
                   [0]    [0]

                           [1 1 1]     [1 0 0]     [1 1 1]      [1 1 1]     [1 0 0]     [1 1 1]
     active(f(X1,X2,X3)) = [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 >= [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 = f(X1,active(X2),X3)
                           [0 0 0]     [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]     [0 0 0]

                         [1 1 1]     [1 0 0]     [1 1 1]      [1 1 1]     [1 0 0]     [1 1 1]
     f(X1,mark(X2),X3) = [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 >= [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 = mark(f(X1,X2,X3))
                         [0 0 0]     [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]     [0 0 0]

                           [1 1 1]     [1 0 0]     [1 1 1]      [1 0 1]     [1 0 0]     [1 0 1]
     proper(f(X1,X2,X3)) = [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 >= [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 = f(proper(X1),proper(X2),proper(X3))
                           [0 0 0]     [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]     [0 0 0]

                   [0]    [0]
     proper(a()) = [1] >= [1] = ok(a())
                   [0]    [0]

                   [0]    [0]
     proper(b()) = [0] >= [0] = ok(b())
                   [0]    [0]

                               [1 1 1]     [1 1 0]     [1 1 1]      [1 1 1]     [1 0 0]     [1 1 1]
     f(ok(X1),ok(X2),ok(X3)) = [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 >= [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 = ok(f(X1,X2,X3))
                               [0 0 0]     [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]     [0 0 0]

                    [1 0 0]    [0]    [1 0 0]    [0]
     top(mark(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = top(proper(X))
                    [0 0 0]    [1]    [0 0 0]    [1]

                  [1 1 0]    [0]    [1 0 0]    [0]
     top(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = top(active(X))
                  [0 0 0]    [1]    [0 0 0]    [1]
    problem:
     strict:
      active(b()) -> mark(a())
      active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
      f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
      proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
      proper(a()) -> ok(a())
      proper(b()) -> ok(b())
      f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
      top(mark(X)) -> top(proper(X))
      top(ok(X)) -> top(active(X))
     weak:
      active(f(a(),X,X)) -> mark(f(X,b(),b()))
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [top](x0) = x0 + 39,

       [ok](x0) = x0 + 16,

       [proper](x0) = x0 + 26,

       [mark](x0) = x0 + 1,

       [b] = 34,

       [active](x0) = x0 + 11,

       [f](x0, x1, x2) = x0 + x1 + x2 + 40,

       [a] = 58
      orientation:
       active(b()) = 45 >= 59 = mark(a())

       active(f(X1,X2,X3)) = X1 + X2 + X3 + 51 >= X1 + X2 + X3 + 51 = f(X1,active(X2),X3)

       f(X1,mark(X2),X3) = X1 + X2 + X3 + 41 >= X1 + X2 + X3 + 41 = mark(f(X1,X2,X3))

       proper(f(X1,X2,X3)) = X1 + X2 + X3 + 66 >= X1 + X2 + X3 + 118 = f(proper(X1),proper(X2),proper(X3))

       proper(a()) = 84 >= 74 = ok(a())

       proper(b()) = 60 >= 50 = ok(b())

       f(ok(X1),ok(X2),ok(X3)) = X1 + X2 + X3 + 88 >= X1 + X2 + X3 + 56 = ok(f(X1,X2,X3))

       top(mark(X)) = X + 40 >= X + 65 = top(proper(X))

       top(ok(X)) = X + 55 >= X + 50 = top(active(X))

       active(f(a(),X,X)) = 2X + 109 >= X + 109 = mark(f(X,b(),b()))
      problem:
       strict:
        active(b()) -> mark(a())
        active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
        f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
        proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
        top(mark(X)) -> top(proper(X))
       weak:
        proper(a()) -> ok(a())
        proper(b()) -> ok(b())
        f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
        top(ok(X)) -> top(active(X))
        active(f(a(),X,X)) -> mark(f(X,b(),b()))
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [top](x0) = x0 + 209,

         [ok](x0) = x0,

         [proper](x0) = x0,

         [mark](x0) = x0 + 5,

         [b] = 62,

         [active](x0) = x0,

         [f](x0, x1, x2) = x0 + x1 + x2 + 181,

         [a] = 129
        orientation:
         active(b()) = 62 >= 134 = mark(a())

         active(f(X1,X2,X3)) = X1 + X2 + X3 + 181 >= X1 + X2 + X3 + 181 = f(X1,active(X2),X3)

         f(X1,mark(X2),X3) = X1 + X2 + X3 + 186 >= X1 + X2 + X3 + 186 = mark(f(X1,X2,X3))

         proper(f(X1,X2,X3)) = X1 + X2 + X3 + 181 >= X1 + X2 + X3 + 181 = f(proper(X1),proper(X2),proper(X3))

         top(mark(X)) = X + 214 >= X + 209 = top(proper(X))

         proper(a()) = 129 >= 129 = ok(a())

         proper(b()) = 62 >= 62 = ok(b())

         f(ok(X1),ok(X2),ok(X3)) = X1 + X2 + X3 + 181 >= X1 + X2 + X3 + 181 = ok(f(X1,X2,X3))

         top(ok(X)) = X + 209 >= X + 209 = top(active(X))

         active(f(a(),X,X)) = 2X + 310 >= X + 310 = mark(f(X,b(),b()))
        problem:
         strict:
          active(b()) -> mark(a())
          active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
          f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
          proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
         weak:
          top(mark(X)) -> top(proper(X))
          proper(a()) -> ok(a())
          proper(b()) -> ok(b())
          f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
          top(ok(X)) -> top(active(X))
          active(f(a(),X,X)) -> mark(f(X,b(),b()))
        Matrix Interpretation Processor:
         dimension: 3
         max_matrix:
          [1 1 2]
          [0 0 2]
          [0 0 0]
          interpretation:
                       [1 0 0]     [2]
           [top](x0) = [0 0 0]x0 + [3]
                       [0 0 0]     [1],

                      [1 1 0]
           [ok](x0) = [0 0 2]x0
                      [0 0 0]  ,

                          [1 0 0]
           [proper](x0) = [0 0 2]x0
                          [0 0 0]  ,

                        [1 0 0]
           [mark](x0) = [0 0 0]x0
                        [0 0 0]  ,

                 [1]
           [b] = [0]
                 [0],

                          [1 0 0]     [0]
           [active](x0) = [0 0 0]x0 + [0]
                          [0 0 0]     [3],

                             [1 1 2]     [1 0 0]     [1 1 2]
           [f](x0, x1, x2) = [0 0 0]x0 + [0 0 0]x1 + [0 0 0]x2
                             [0 0 0]     [0 0 0]     [0 0 0]  ,

                 [0]
           [a] = [0]
                 [1]
          orientation:
                         [1]    [0]
           active(b()) = [0] >= [0] = mark(a())
                         [3]    [0]

                                 [1 1 2]     [1 0 0]     [1 1 2]     [0]    [1 1 2]     [1 0 0]     [1 1 2]
           active(f(X1,X2,X3)) = [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 + [0] >= [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 = f(X1,active(X2),X3)
                                 [0 0 0]     [0 0 0]     [0 0 0]     [3]    [0 0 0]     [0 0 0]     [0 0 0]

                               [1 1 2]     [1 0 0]     [1 1 2]      [1 1 2]     [1 0 0]     [1 1 2]
           f(X1,mark(X2),X3) = [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 >= [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 = mark(f(X1,X2,X3))
                               [0 0 0]     [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]     [0 0 0]

                                 [1 1 2]     [1 0 0]     [1 1 2]      [1 0 2]     [1 0 0]     [1 0 2]
           proper(f(X1,X2,X3)) = [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 >= [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 = f(proper(X1),proper(X2),proper(X3))
                                 [0 0 0]     [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]     [0 0 0]

                          [1 0 0]    [2]    [1 0 0]    [2]
           top(mark(X)) = [0 0 0]X + [3] >= [0 0 0]X + [3] = top(proper(X))
                          [0 0 0]    [1]    [0 0 0]    [1]

                         [0]    [0]
           proper(a()) = [2] >= [2] = ok(a())
                         [0]    [0]

                         [1]    [1]
           proper(b()) = [0] >= [0] = ok(b())
                         [0]    [0]

                                     [1 1 2]     [1 1 0]     [1 1 2]      [1 1 2]     [1 0 0]     [1 1 2]
           f(ok(X1),ok(X2),ok(X3)) = [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 >= [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 = ok(f(X1,X2,X3))
                                     [0 0 0]     [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]     [0 0 0]

                        [1 1 0]    [2]    [1 0 0]    [2]
           top(ok(X)) = [0 0 0]X + [3] >= [0 0 0]X + [3] = top(active(X))
                        [0 0 0]    [1]    [0 0 0]    [1]

                                [2 1 2]    [2]    [1 1 2]    [2]
           active(f(a(),X,X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = mark(f(X,b(),b()))
                                [0 0 0]    [3]    [0 0 0]    [0]
          problem:
           strict:
            active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
            f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
            proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
           weak:
            active(b()) -> mark(a())
            top(mark(X)) -> top(proper(X))
            proper(a()) -> ok(a())
            proper(b()) -> ok(b())
            f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
            top(ok(X)) -> top(active(X))
            active(f(a(),X,X)) -> mark(f(X,b(),b()))
          Bounds Processor:
           bound: 0
           enrichment: match
           automaton:
            final states: {12,10,8,7,6,5}
            transitions:
             active0(10) -> 5*
             active0(12) -> 5*
             active0(2) -> 5*
             active0(4) -> 5*
             active0(1) -> 5*
             active0(3) -> 5*
             f0(4,4,12) -> 6*
             f0(3,4,2) -> 6*
             f0(4,10,3) -> 6*
             f0(4,12,3) -> 6*
             f0(10,10,1) -> 6*
             f0(4,10,12) -> 6*
             f0(12,2,10) -> 6*
             f0(3,10,2) -> 6*
             f0(10,12,1) -> 6*
             f0(1,1,4) -> 6*
             f0(4,12,12) -> 6*
             f0(2,2,10) -> 6*
             f0(12,4,10) -> 6*
             f0(3,12,2) -> 6*
             f0(1,3,4) -> 6*
             f0(2,4,10) -> 6*
             f0(10,1,3) -> 6*
             f0(10,3,3) -> 6*
             f0(12,10,10) -> 6*
             f0(10,1,12) -> 6*
             f0(2,10,10) -> 6*
             f0(12,12,10) -> 6*
             f0(4,1,2) -> 6*
             f0(10,3,12) -> 6*
             f0(1,1,1) -> 6*
             f0(2,12,10) -> 6*
             f0(4,3,2) -> 6*
             f0(1,3,1) -> 6*
             f0(12,2,4) -> 6*
             f0(3,1,10) -> 6*
             f0(2,2,4) -> 6*
             f0(12,4,4) -> 6*
             f0(3,3,10) -> 6*
             f0(2,4,4) -> 6*
             f0(1,2,3) -> 6*
             f0(12,10,4) -> 6*
             f0(1,4,3) -> 6*
             f0(2,10,4) -> 6*
             f0(12,12,4) -> 6*
             f0(12,2,1) -> 6*
             f0(10,2,2) -> 6*
             f0(1,2,12) -> 6*
             f0(2,12,4) -> 6*
             f0(2,2,1) -> 6*
             f0(12,4,1) -> 6*
             f0(10,4,2) -> 6*
             f0(1,4,12) -> 6*
             f0(2,4,1) -> 6*
             f0(1,10,3) -> 6*
             f0(1,12,3) -> 6*
             f0(12,10,1) -> 6*
             f0(10,10,2) -> 6*
             f0(1,10,12) -> 6*
             f0(2,10,1) -> 6*
             f0(12,12,1) -> 6*
             f0(10,12,2) -> 6*
             f0(3,1,4) -> 6*
             f0(4,2,10) -> 6*
             f0(1,12,12) -> 6*
             f0(2,12,1) -> 6*
             f0(3,3,4) -> 6*
             f0(4,4,10) -> 6*
             f0(12,1,3) -> 6*
             f0(2,1,3) -> 6*
             f0(12,3,3) -> 6*
             f0(2,3,3) -> 6*
             f0(12,1,12) -> 6*
             f0(4,10,10) -> 6*
             f0(12,3,12) -> 6*
             f0(2,1,12) -> 6*
             f0(3,1,1) -> 6*
             f0(1,1,2) -> 6*
             f0(4,12,10) -> 6*
             f0(2,3,12) -> 6*
             f0(3,3,1) -> 6*
             f0(1,3,2) -> 6*
             f0(10,1,10) -> 6*
             f0(10,3,10) -> 6*
             f0(4,2,4) -> 6*
             f0(4,4,4) -> 6*
             f0(3,2,3) -> 6*
             f0(3,4,3) -> 6*
             f0(4,10,4) -> 6*
             f0(12,2,2) -> 6*
             f0(3,2,12) -> 6*
             f0(4,12,4) -> 6*
             f0(4,2,1) -> 6*
             f0(2,2,2) -> 6*
             f0(12,4,2) -> 6*
             f0(3,4,12) -> 6*
             f0(4,4,1) -> 6*
             f0(2,4,2) -> 6*
             f0(3,10,3) -> 6*
             f0(3,12,3) -> 6*
             f0(12,10,2) -> 6*
             f0(10,1,4) -> 6*
             f0(3,10,12) -> 6*
             f0(4,10,1) -> 6*
             f0(2,10,2) -> 6*
             f0(12,12,2) -> 6*
             f0(10,3,4) -> 6*
             f0(3,12,12) -> 6*
             f0(1,2,10) -> 6*
             f0(4,12,1) -> 6*
             f0(2,12,2) -> 6*
             f0(1,4,10) -> 6*
             f0(4,1,3) -> 6*
             f0(4,3,3) -> 6*
             f0(10,1,1) -> 6*
             f0(1,10,10) -> 6*
             f0(4,1,12) -> 6*
             f0(3,1,2) -> 6*
             f0(10,3,1) -> 6*
             f0(1,12,10) -> 6*
             f0(4,3,12) -> 6*
             f0(3,3,2) -> 6*
             f0(12,1,10) -> 6*
             f0(2,1,10) -> 6*
             f0(12,3,10) -> 6*
             f0(1,2,4) -> 6*
             f0(2,3,10) -> 6*
             f0(1,4,4) -> 6*
             f0(10,2,3) -> 6*
             f0(10,4,3) -> 6*
             f0(10,2,12) -> 6*
             f0(1,10,4) -> 6*
             f0(4,2,2) -> 6*
             f0(10,4,12) -> 6*
             f0(1,12,4) -> 6*
             f0(1,2,1) -> 6*
             f0(10,10,3) -> 6*
             f0(4,4,2) -> 6*
             f0(1,4,1) -> 6*
             f0(10,12,3) -> 6*
             f0(10,10,12) -> 6*
             f0(12,1,4) -> 6*
             f0(4,10,2) -> 6*
             f0(10,12,12) -> 6*
             f0(1,10,1) -> 6*
             f0(2,1,4) -> 6*
             f0(12,3,4) -> 6*
             f0(3,2,10) -> 6*
             f0(4,12,2) -> 6*
             f0(1,12,1) -> 6*
             f0(2,3,4) -> 6*
             f0(3,4,10) -> 6*
             f0(1,1,3) -> 6*
             f0(1,3,3) -> 6*
             f0(12,1,1) -> 6*
             f0(3,10,10) -> 6*
             f0(10,1,2) -> 6*
             f0(1,1,12) -> 6*
             f0(2,1,1) -> 6*
             f0(12,3,1) -> 6*
             f0(10,3,2) -> 6*
             f0(3,12,10) -> 6*
             f0(1,3,12) -> 6*
             f0(2,3,1) -> 6*
             f0(4,1,10) -> 6*
             f0(3,2,4) -> 6*
             f0(4,3,10) -> 6*
             f0(3,4,4) -> 6*
             f0(12,2,3) -> 6*
             f0(2,2,3) -> 6*
             f0(12,4,3) -> 6*
             f0(2,4,3) -> 6*
             f0(12,2,12) -> 6*
             f0(3,10,4) -> 6*
             f0(12,4,12) -> 6*
             f0(2,2,12) -> 6*
             f0(3,12,4) -> 6*
             f0(3,2,1) -> 6*
             f0(1,2,2) -> 6*
             f0(12,10,3) -> 6*
             f0(2,4,12) -> 6*
             f0(3,4,1) -> 6*
             f0(1,4,2) -> 6*
             f0(2,10,3) -> 6*
             f0(12,12,3) -> 6*
             f0(2,12,3) -> 6*
             f0(12,10,12) -> 6*
             f0(2,10,12) -> 6*
             f0(12,12,12) -> 6*
             f0(3,10,1) -> 6*
             f0(10,2,10) -> 6*
             f0(1,10,2) -> 6*
             f0(4,1,4) -> 6*
             f0(2,12,12) -> 6*
             f0(10,4,10) -> 6*
             f0(3,12,1) -> 6*
             f0(1,12,2) -> 6*
             f0(4,3,4) -> 6*
             f0(3,1,3) -> 6*
             f0(3,3,3) -> 6*
             f0(10,10,10) -> 6*
             f0(12,1,2) -> 6*
             f0(10,12,10) -> 6*
             f0(3,1,12) -> 6*
             f0(4,1,1) -> 6*
             f0(2,1,2) -> 6*
             f0(12,3,2) -> 6*
             f0(3,3,12) -> 6*
             f0(4,3,1) -> 6*
             f0(2,3,2) -> 6*
             f0(10,2,4) -> 6*
             f0(1,1,10) -> 6*
             f0(10,4,4) -> 6*
             f0(1,3,10) -> 6*
             f0(4,2,3) -> 6*
             f0(10,10,4) -> 6*
             f0(4,4,3) -> 6*
             f0(10,12,4) -> 6*
             f0(10,2,1) -> 6*
             f0(4,2,12) -> 6*
             f0(3,2,2) -> 6*
             f0(10,4,1) -> 6*
             mark0(10) -> 1*
             mark0(12) -> 1*
             mark0(2) -> 1*
             mark0(4) -> 1*
             mark0(6) -> 6*
             mark0(1) -> 1*
             mark0(3) -> 10*,5,1
             proper0(10) -> 7*
             proper0(12) -> 7*
             proper0(2) -> 7*
             proper0(4) -> 7*
             proper0(1) -> 7*
             proper0(3) -> 7*
             b0() -> 2*
             a0() -> 3*
             top0(10) -> 8*
             top0(5) -> 8*
             top0(12) -> 8*
             top0(7) -> 8*
             top0(2) -> 8*
             top0(4) -> 8*
             top0(1) -> 8*
             top0(3) -> 8*
             ok0(10) -> 4*
             ok0(12) -> 4*
             ok0(2) -> 12*,7,4
             ok0(4) -> 4*
             ok0(6) -> 6*
             ok0(1) -> 4*
             ok0(3) -> 12*,7,4
           problem:
            strict:
             f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
             proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
            weak:
             active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
             active(b()) -> mark(a())
             top(mark(X)) -> top(proper(X))
             proper(a()) -> ok(a())
             proper(b()) -> ok(b())
             f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
             top(ok(X)) -> top(active(X))
             active(f(a(),X,X)) -> mark(f(X,b(),b()))
           Bounds Processor:
            bound: 0
            enrichment: match
            automaton:
             final states: {11,10,8,7,6,5}
             transitions:
              active0(10) -> 7*
              active0(2) -> 7*
              active0(4) -> 7*
              active0(11) -> 7*
              active0(1) -> 7*
              active0(3) -> 7*
              f0(3,4,2) -> 5*
              f0(4,10,3) -> 5*
              f0(3,2,11) -> 5*
              f0(3,4,11) -> 5*
              f0(10,10,1) -> 5*
              f0(11,1,4) -> 5*
              f0(3,10,2) -> 5*
              f0(1,1,4) -> 5*
              f0(11,3,4) -> 5*
              f0(2,2,10) -> 5*
              f0(1,3,4) -> 5*
              f0(2,4,10) -> 5*
              f0(10,1,3) -> 5*
              f0(3,10,11) -> 5*
              f0(10,3,3) -> 5*
              f0(11,11,4) -> 5*
              f0(11,1,1) -> 5*
              f0(2,10,10) -> 5*
              f0(4,1,2) -> 5*
              f0(1,11,4) -> 5*
              f0(1,1,1) -> 5*
              f0(11,3,1) -> 5*
              f0(4,3,2) -> 5*
              f0(1,3,1) -> 5*
              f0(10,11,3) -> 5*
              f0(4,1,11) -> 5*
              f0(4,3,11) -> 5*
              f0(11,11,1) -> 5*
              f0(3,1,10) -> 5*
              f0(4,11,2) -> 5*
              f0(1,11,1) -> 5*
              f0(2,2,4) -> 5*
              f0(3,3,10) -> 5*
              f0(2,4,4) -> 5*
              f0(11,2,3) -> 5*
              f0(4,11,11) -> 5*
              f0(1,2,3) -> 5*
              f0(11,4,3) -> 5*
              f0(1,4,3) -> 5*
              f0(2,10,4) -> 5*
              f0(10,2,2) -> 5*
              f0(3,11,10) -> 5*
              f0(2,2,1) -> 5*
              f0(10,4,2) -> 5*
              f0(11,10,3) -> 5*
              f0(2,4,1) -> 5*
              f0(10,2,11) -> 5*
              f0(1,10,3) -> 5*
              f0(10,4,11) -> 5*
              f0(10,10,2) -> 5*
              f0(2,10,1) -> 5*
              f0(3,1,4) -> 5*
              f0(4,2,10) -> 5*
              f0(3,3,4) -> 5*
              f0(10,10,11) -> 5*
              f0(4,4,10) -> 5*
              f0(2,1,3) -> 5*
              f0(2,3,3) -> 5*
              f0(4,10,10) -> 5*
              f0(11,1,2) -> 5*
              f0(3,11,4) -> 5*
              f0(3,1,1) -> 5*
              f0(1,1,2) -> 5*
              f0(11,3,2) -> 5*
              f0(3,3,1) -> 5*
              f0(1,3,2) -> 5*
              f0(11,1,11) -> 5*
              f0(11,3,11) -> 5*
              f0(1,1,11) -> 5*
              f0(2,11,3) -> 5*
              f0(1,3,11) -> 5*
              f0(10,1,10) -> 5*
              f0(11,11,2) -> 5*
              f0(10,3,10) -> 5*
              f0(3,11,1) -> 5*
              f0(1,11,2) -> 5*
              f0(4,2,4) -> 5*
              f0(4,4,4) -> 5*
              f0(11,11,11) -> 5*
              f0(1,11,11) -> 5*
              f0(3,2,3) -> 5*
              f0(3,4,3) -> 5*
              f0(10,11,10) -> 5*
              f0(4,10,4) -> 5*
              f0(4,2,1) -> 5*
              f0(2,2,2) -> 5*
              f0(4,4,1) -> 5*
              f0(2,4,2) -> 5*
              f0(3,10,3) -> 5*
              f0(2,2,11) -> 5*
              f0(2,4,11) -> 5*
              f0(10,1,4) -> 5*
              f0(4,10,1) -> 5*
              f0(11,2,10) -> 5*
              f0(2,10,2) -> 5*
              f0(10,3,4) -> 5*
              f0(1,2,10) -> 5*
              f0(11,4,10) -> 5*
              f0(1,4,10) -> 5*
              f0(2,10,11) -> 5*
              f0(4,1,3) -> 5*
              f0(4,3,3) -> 5*
              f0(11,10,10) -> 5*
              f0(10,11,4) -> 5*
              f0(10,1,1) -> 5*
              f0(1,10,10) -> 5*
              f0(3,1,2) -> 5*
              f0(10,3,1) -> 5*
              f0(3,3,2) -> 5*
              f0(3,1,11) -> 5*
              f0(4,11,3) -> 5*
              f0(3,3,11) -> 5*
              f0(10,11,1) -> 5*
              f0(11,2,4) -> 5*
              f0(2,1,10) -> 5*
              f0(3,11,2) -> 5*
              f0(1,2,4) -> 5*
              f0(11,4,4) -> 5*
              f0(2,3,10) -> 5*
              f0(1,4,4) -> 5*
              f0(10,2,3) -> 5*
              f0(3,11,11) -> 5*
              f0(10,4,3) -> 5*
              f0(11,10,4) -> 5*
              f0(1,10,4) -> 5*
              f0(11,2,1) -> 5*
              f0(2,11,10) -> 5*
              f0(4,2,2) -> 5*
              f0(1,2,1) -> 5*
              f0(11,4,1) -> 5*
              f0(10,10,3) -> 5*
              f0(4,4,2) -> 5*
              f0(1,4,1) -> 5*
              f0(4,2,11) -> 5*
              f0(4,4,11) -> 5*
              f0(11,10,1) -> 5*
              f0(4,10,2) -> 5*
              f0(1,10,1) -> 5*
              f0(2,1,4) -> 5*
              f0(3,2,10) -> 5*
              f0(2,3,4) -> 5*
              f0(3,4,10) -> 5*
              f0(4,10,11) -> 5*
              f0(11,1,3) -> 5*
              f0(1,1,3) -> 5*
              f0(11,3,3) -> 5*
              f0(1,3,3) -> 5*
              f0(3,10,10) -> 5*
              f0(10,1,2) -> 5*
              f0(2,11,4) -> 5*
              f0(2,1,1) -> 5*
              f0(10,3,2) -> 5*
              f0(2,3,1) -> 5*
              f0(10,1,11) -> 5*
              f0(11,11,3) -> 5*
              f0(10,3,11) -> 5*
              f0(1,11,3) -> 5*
              f0(10,11,2) -> 5*
              f0(4,1,10) -> 5*
              f0(2,11,1) -> 5*
              f0(3,2,4) -> 5*
              f0(4,3,10) -> 5*
              f0(3,4,4) -> 5*
              f0(10,11,11) -> 5*
              f0(2,2,3) -> 5*
              f0(2,4,3) -> 5*
              f0(3,10,4) -> 5*
              f0(11,2,2) -> 5*
              f0(4,11,10) -> 5*
              f0(3,2,1) -> 5*
              f0(1,2,2) -> 5*
              f0(11,4,2) -> 5*
              f0(3,4,1) -> 5*
              f0(1,4,2) -> 5*
              f0(11,2,11) -> 5*
              f0(2,10,3) -> 5*
              f0(1,2,11) -> 5*
              f0(11,4,11) -> 5*
              f0(11,10,2) -> 5*
              f0(1,4,11) -> 5*
              f0(3,10,1) -> 5*
              f0(10,2,10) -> 5*
              f0(1,10,2) -> 5*
              f0(4,1,4) -> 5*
              f0(10,4,10) -> 5*
              f0(4,3,4) -> 5*
              f0(11,10,11) -> 5*
              f0(1,10,11) -> 5*
              f0(3,1,3) -> 5*
              f0(3,3,3) -> 5*
              f0(10,10,10) -> 5*
              f0(4,11,4) -> 5*
              f0(4,1,1) -> 5*
              f0(2,1,2) -> 5*
              f0(4,3,1) -> 5*
              f0(2,3,2) -> 5*
              f0(2,1,11) -> 5*
              f0(3,11,3) -> 5*
              f0(2,3,11) -> 5*
              f0(11,1,10) -> 5*
              f0(10,2,4) -> 5*
              f0(1,1,10) -> 5*
              f0(11,3,10) -> 5*
              f0(4,11,1) -> 5*
              f0(2,11,2) -> 5*
              f0(10,4,4) -> 5*
              f0(1,3,10) -> 5*
              f0(2,11,11) -> 5*
              f0(4,2,3) -> 5*
              f0(10,10,4) -> 5*
              f0(4,4,3) -> 5*
              f0(11,11,10) -> 5*
              f0(10,2,1) -> 5*
              f0(1,11,10) -> 5*
              f0(3,2,2) -> 5*
              f0(10,4,1) -> 5*
              mark0(10) -> 1*
              mark0(5) -> 5*
              mark0(2) -> 1*
              mark0(4) -> 1*
              mark0(11) -> 1*
              mark0(1) -> 1*
              mark0(3) -> 10*,7,1
              proper0(10) -> 6*
              proper0(2) -> 6*
              proper0(4) -> 6*
              proper0(11) -> 6*
              proper0(1) -> 6*
              proper0(3) -> 6*
              b0() -> 2*
              a0() -> 3*
              top0(10) -> 8*
              top0(7) -> 8*
              top0(2) -> 8*
              top0(4) -> 8*
              top0(11) -> 8*
              top0(6) -> 8*
              top0(1) -> 8*
              top0(3) -> 8*
              ok0(10) -> 4*
              ok0(5) -> 5*
              ok0(2) -> 11*,6,4
              ok0(4) -> 4*
              ok0(11) -> 4*
              ok0(1) -> 4*
              ok0(3) -> 11*,6,4
            problem:
             strict:
              f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
             weak:
              proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
              active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
              active(b()) -> mark(a())
              top(mark(X)) -> top(proper(X))
              proper(a()) -> ok(a())
              proper(b()) -> ok(b())
              f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
              top(ok(X)) -> top(active(X))
              active(f(a(),X,X)) -> mark(f(X,b(),b()))
            Bounds Processor:
             bound: 1
             enrichment: match
             automaton:
              final states: {16,14,12,8,7,6,5}
              transitions:
               active0(2) -> 7*
               active0(14) -> 7*
               active0(4) -> 7*
               active0(16) -> 7*
               active0(1) -> 7*
               active0(3) -> 7*
               f0(3,4,2) -> 5*
               f0(16,3,16) -> 5*
               f0(14,14,3) -> 5*
               f0(1,3,16) -> 5*
               f0(16,1,4) -> 5*
               f0(3,14,14) -> 5*
               f0(14,16,3) -> 5*
               f0(4,14,3) -> 5*
               f0(3,1,16) -> 5*
               f0(16,3,4) -> 5*
               f0(3,16,14) -> 5*
               f0(4,16,3) -> 5*
               f0(1,1,4) -> 5*
               f0(14,1,14) -> 5*
               f0(1,3,4) -> 5*
               f0(3,14,2) -> 5*
               f0(14,3,14) -> 5*
               f0(4,1,14) -> 5*
               f0(3,16,2) -> 5*
               f0(4,3,14) -> 5*
               f0(16,1,1) -> 5*
               f0(14,1,2) -> 5*
               f0(16,3,1) -> 5*
               f0(14,3,2) -> 5*
               f0(4,1,2) -> 5*
               f0(1,1,1) -> 5*
               f0(4,3,2) -> 5*
               f0(1,3,1) -> 5*
               f0(2,2,16) -> 5*
               f0(2,4,16) -> 5*
               f0(2,2,4) -> 5*
               f0(2,4,4) -> 5*
               f0(16,2,3) -> 5*
               f0(16,4,3) -> 5*
               f0(1,2,3) -> 5*
               f0(2,14,16) -> 5*
               f0(1,4,3) -> 5*
               f0(2,16,16) -> 5*
               f0(2,2,1) -> 5*
               f0(2,14,4) -> 5*
               f0(2,4,1) -> 5*
               f0(2,16,4) -> 5*
               f0(16,14,3) -> 5*
               f0(3,3,16) -> 5*
               f0(16,16,3) -> 5*
               f0(1,14,3) -> 5*
               f0(3,1,4) -> 5*
               f0(1,16,3) -> 5*
               f0(16,1,14) -> 5*
               f0(3,3,4) -> 5*
               f0(2,14,1) -> 5*
               f0(16,3,14) -> 5*
               f0(1,1,14) -> 5*
               f0(2,1,3) -> 5*
               f0(2,16,1) -> 5*
               f0(1,3,14) -> 5*
               f0(2,3,3) -> 5*
               f0(16,1,2) -> 5*
               f0(16,3,2) -> 5*
               f0(3,1,1) -> 5*
               f0(1,1,2) -> 5*
               f0(3,3,1) -> 5*
               f0(1,3,2) -> 5*
               f0(14,2,16) -> 5*
               f0(4,2,16) -> 5*
               f0(14,4,16) -> 5*
               f0(4,4,16) -> 5*
               f0(14,2,4) -> 5*
               f0(14,4,4) -> 5*
               f0(4,2,4) -> 5*
               f0(4,4,4) -> 5*
               f0(14,14,16) -> 5*
               f0(2,2,14) -> 5*
               f0(3,2,3) -> 5*
               f0(14,16,16) -> 5*
               f0(4,14,16) -> 5*
               f0(2,4,14) -> 5*
               f0(3,4,3) -> 5*
               f0(14,2,1) -> 5*
               f0(4,16,16) -> 5*
               f0(14,14,4) -> 5*
               f0(14,4,1) -> 5*
               f0(4,2,1) -> 5*
               f0(2,2,2) -> 5*
               f0(14,16,4) -> 5*
               f0(4,14,4) -> 5*
               f0(4,4,1) -> 5*
               f0(2,4,2) -> 5*
               f0(4,16,4) -> 5*
               f0(2,14,14) -> 5*
               f0(3,14,3) -> 5*
               f0(2,1,16) -> 5*
               f0(2,16,14) -> 5*
               f0(3,16,3) -> 5*
               f0(14,14,1) -> 5*
               f0(14,1,3) -> 5*
               f0(14,16,1) -> 5*
               f0(4,14,1) -> 5*
               f0(2,14,2) -> 5*
               f0(3,1,14) -> 5*
               f0(14,3,3) -> 5*
               f0(4,1,3) -> 5*
               f0(4,16,1) -> 5*
               f0(2,16,2) -> 5*
               f0(3,3,14) -> 5*
               f0(4,3,3) -> 5*
               f0(3,1,2) -> 5*
               f0(3,3,2) -> 5*
               f0(16,2,16) -> 5*
               f0(16,4,16) -> 5*
               f0(1,2,16) -> 5*
               f0(1,4,16) -> 5*
               f0(16,2,4) -> 5*
               f0(16,4,4) -> 5*
               f0(1,2,4) -> 5*
               f0(14,2,14) -> 5*
               f0(1,4,4) -> 5*
               f0(16,14,16) -> 5*
               f0(4,2,14) -> 5*
               f0(14,4,14) -> 5*
               f0(16,16,16) -> 5*
               f0(4,4,14) -> 5*
               f0(1,14,16) -> 5*
               f0(16,2,1) -> 5*
               f0(14,2,2) -> 5*
               f0(1,16,16) -> 5*
               f0(16,14,4) -> 5*
               f0(16,4,1) -> 5*
               f0(14,4,2) -> 5*
               f0(4,2,2) -> 5*
               f0(1,2,1) -> 5*
               f0(16,16,4) -> 5*
               f0(4,4,2) -> 5*
               f0(1,14,4) -> 5*
               f0(1,4,1) -> 5*
               f0(14,14,14) -> 5*
               f0(1,16,4) -> 5*
               f0(2,3,16) -> 5*
               f0(14,16,14) -> 5*
               f0(4,14,14) -> 5*
               f0(4,16,14) -> 5*
               f0(2,1,4) -> 5*
               f0(16,14,1) -> 5*
               f0(14,14,2) -> 5*
               f0(2,3,4) -> 5*
               f0(16,1,3) -> 5*
               f0(16,16,1) -> 5*
               f0(14,16,2) -> 5*
               f0(4,14,2) -> 5*
               f0(1,14,1) -> 5*
               f0(16,3,3) -> 5*
               f0(4,16,2) -> 5*
               f0(1,1,3) -> 5*
               f0(1,16,1) -> 5*
               f0(1,3,3) -> 5*
               f0(2,1,1) -> 5*
               f0(2,3,1) -> 5*
               f0(3,2,16) -> 5*
               f0(3,4,16) -> 5*
               f0(3,2,4) -> 5*
               f0(16,2,14) -> 5*
               f0(3,4,4) -> 5*
               f0(16,4,14) -> 5*
               f0(1,2,14) -> 5*
               f0(2,2,3) -> 5*
               f0(3,14,16) -> 5*
               f0(1,4,14) -> 5*
               f0(2,4,3) -> 5*
               f0(16,2,2) -> 5*
               f0(3,16,16) -> 5*
               f0(16,4,2) -> 5*
               f0(3,2,1) -> 5*
               f0(1,2,2) -> 5*
               f0(14,1,16) -> 5*
               f0(3,14,4) -> 5*
               f0(3,4,1) -> 5*
               f0(1,4,2) -> 5*
               f0(14,3,16) -> 5*
               f0(4,1,16) -> 5*
               f0(16,14,14) -> 5*
               f0(3,16,4) -> 5*
               f0(4,3,16) -> 5*
               f0(16,16,14) -> 5*
               f0(14,1,4) -> 5*
               f0(1,14,14) -> 5*
               f0(2,14,3) -> 5*
               f0(1,1,16) -> 5*
               f0(1,16,14) -> 5*
               f0(14,3,4) -> 5*
               f0(4,1,4) -> 5*
               f0(2,16,3) -> 5*
               f0(16,14,2) -> 5*
               f0(4,3,4) -> 5*
               f0(16,16,2) -> 5*
               f0(3,14,1) -> 5*
               f0(1,14,2) -> 5*
               f0(2,1,14) -> 5*
               f0(3,1,3) -> 5*
               f0(3,16,1) -> 5*
               f0(1,16,2) -> 5*
               f0(2,3,14) -> 5*
               f0(3,3,3) -> 5*
               f0(14,1,1) -> 5*
               f0(14,3,1) -> 5*
               f0(4,1,1) -> 5*
               f0(2,1,2) -> 5*
               f0(4,3,1) -> 5*
               f0(2,3,2) -> 5*
               f0(14,2,3) -> 5*
               f0(3,2,14) -> 5*
               f0(14,4,3) -> 5*
               f0(4,2,3) -> 5*
               f0(3,4,14) -> 5*
               f0(4,4,3) -> 5*
               f0(3,2,2) -> 5*
               f0(16,1,16) -> 5*
               mark0(2) -> 1*
               mark0(14) -> 1*
               mark0(4) -> 1*
               mark0(16) -> 1*
               mark0(1) -> 1*
               mark0(3) -> 14*,7,1
               proper0(2) -> 6*
               proper0(14) -> 6*
               proper0(4) -> 6*
               proper0(16) -> 6*
               proper0(1) -> 6*
               proper0(3) -> 6*
               b0() -> 2*
               a0() -> 3*
               top0(7) -> 8*
               top0(2) -> 8*
               top0(14) -> 8*
               top0(4) -> 8*
               top0(16) -> 8*
               top0(6) -> 8*
               top0(1) -> 8*
               top0(3) -> 8*
               ok0(5) -> 5*
               ok0(12) -> 5*
               ok0(2) -> 16*,6,4
               ok0(14) -> 4*
               ok0(4) -> 4*
               ok0(16) -> 4*
               ok0(1) -> 4*
               ok0(3) -> 16*,6,4
               mark1(10) -> 5*
               mark1(5) -> 12*
               mark1(12) -> 12*,5
               f1(3,2,2) -> 12*,5,10
               f1(16,1,16) -> 5,12*
               f1(3,4,2) -> 12*,5,10
               f1(16,3,16) -> 5,12*
               f1(14,14,3) -> 5,12*
               f1(1,3,16) -> 5,12*
               f1(16,1,4) -> 5,12*
               f1(3,14,14) -> 5,12*
               f1(14,16,3) -> 5,12*
               f1(4,14,3) -> 5,12*
               f1(3,1,16) -> 5,12*
               f1(16,3,4) -> 5,12*
               f1(3,16,14) -> 5,12*
               f1(4,16,3) -> 5,12*
               f1(1,1,4) -> 12*,5,10
               f1(14,1,14) -> 5,12*
               f1(1,3,4) -> 12*,5,10
               f1(3,14,2) -> 5,12*
               f1(14,3,14) -> 5,12*
               f1(4,1,14) -> 5,12*
               f1(3,16,2) -> 5,12*
               f1(4,3,14) -> 5,12*
               f1(16,1,1) -> 5,12*
               f1(14,1,2) -> 5,12*
               f1(16,3,1) -> 5,12*
               f1(14,3,2) -> 5,12*
               f1(4,1,2) -> 12*,5,10
               f1(1,1,1) -> 12*,5,10
               f1(4,3,2) -> 12*,5,10
               f1(1,3,1) -> 12*,5,10
               f1(2,2,16) -> 5,12*
               f1(2,4,16) -> 5,12*
               f1(2,2,4) -> 12*,5,10
               f1(2,4,4) -> 12*,5,10
               f1(16,2,3) -> 5,12*
               f1(16,4,3) -> 5,12*
               f1(1,2,3) -> 12*,5,10
               f1(2,14,16) -> 5,12*
               f1(1,4,3) -> 12*,5,10
               f1(2,16,16) -> 5,12*
               f1(2,2,1) -> 12*,5,10
               f1(2,14,4) -> 5,12*
               f1(2,4,1) -> 12*,5,10
               f1(2,16,4) -> 5,12*
               f1(16,14,3) -> 5,12*
               f1(3,3,16) -> 5,12*
               f1(16,16,3) -> 5,12*
               f1(1,14,3) -> 5,12*
               f1(3,1,4) -> 12*,5,10
               f1(1,16,3) -> 5,12*
               f1(16,1,14) -> 5,12*
               f1(3,3,4) -> 12*,5,10
               f1(2,14,1) -> 5,12*
               f1(16,3,14) -> 5,12*
               f1(1,1,14) -> 5,12*
               f1(2,1,3) -> 12*,5,10
               f1(2,16,1) -> 5,12*
               f1(1,3,14) -> 5,12*
               f1(2,3,3) -> 12*,5,10
               f1(16,1,2) -> 5,12*
               f1(16,3,2) -> 5,12*
               f1(3,1,1) -> 12*,5,10
               f1(1,1,2) -> 12*,5,10
               f1(3,3,1) -> 12*,5,10
               f1(1,3,2) -> 12*,5,10
               f1(14,2,16) -> 5,12*
               f1(4,2,16) -> 5,12*
               f1(14,4,16) -> 5,12*
               f1(4,4,16) -> 5,12*
               f1(14,2,4) -> 5,12*
               f1(14,4,4) -> 5,12*
               f1(4,2,4) -> 12*,5,10
               f1(4,4,4) -> 12*,5,10
               f1(14,14,16) -> 5,12*
               f1(2,2,14) -> 5,12*
               f1(3,2,3) -> 12*,5,10
               f1(14,16,16) -> 5,12*
               f1(4,14,16) -> 5,12*
               f1(2,4,14) -> 5,12*
               f1(3,4,3) -> 12*,5,10
               f1(14,2,1) -> 5,12*
               f1(4,16,16) -> 5,12*
               f1(14,14,4) -> 5,12*
               f1(14,4,1) -> 5,12*
               f1(4,2,1) -> 12*,5,10
               f1(2,2,2) -> 12*,5,10
               f1(14,16,4) -> 5,12*
               f1(4,14,4) -> 5,12*
               f1(4,4,1) -> 12*,5,10
               f1(2,4,2) -> 12*,5,10
               f1(4,16,4) -> 5,12*
               f1(2,14,14) -> 5,12*
               f1(3,14,3) -> 5,12*
               f1(2,1,16) -> 5,12*
               f1(2,16,14) -> 5,12*
               f1(3,16,3) -> 5,12*
               f1(14,14,1) -> 5,12*
               f1(14,1,3) -> 5,12*
               f1(14,16,1) -> 5,12*
               f1(4,14,1) -> 5,12*
               f1(2,14,2) -> 5,12*
               f1(3,1,14) -> 5,12*
               f1(14,3,3) -> 5,12*
               f1(4,1,3) -> 12*,5,10
               f1(4,16,1) -> 5,12*
               f1(2,16,2) -> 5,12*
               f1(3,3,14) -> 5,12*
               f1(4,3,3) -> 12*,5,10
               f1(3,1,2) -> 12*,5,10
               f1(3,3,2) -> 12*,5,10
               f1(16,2,16) -> 5,12*
               f1(16,4,16) -> 5,12*
               f1(1,2,16) -> 5,12*
               f1(1,4,16) -> 5,12*
               f1(16,2,4) -> 5,12*
               f1(16,4,4) -> 5,12*
               f1(1,2,4) -> 12*,5,10
               f1(14,2,14) -> 5,12*
               f1(1,4,4) -> 12*,5,10
               f1(16,14,16) -> 5,12*
               f1(4,2,14) -> 5,12*
               f1(14,4,14) -> 5,12*
               f1(16,16,16) -> 5,12*
               f1(4,4,14) -> 5,12*
               f1(1,14,16) -> 5,12*
               f1(16,2,1) -> 5,12*
               f1(14,2,2) -> 5,12*
               f1(1,16,16) -> 5,12*
               f1(16,14,4) -> 5,12*
               f1(16,4,1) -> 5,12*
               f1(14,4,2) -> 5,12*
               f1(4,2,2) -> 12*,5,10
               f1(1,2,1) -> 12*,5,10
               f1(16,16,4) -> 5,12*
               f1(4,4,2) -> 12*,5,10
               f1(1,14,4) -> 5,12*
               f1(1,4,1) -> 12*,5,10
               f1(14,14,14) -> 5,12*
               f1(1,16,4) -> 5,12*
               f1(2,3,16) -> 5,12*
               f1(14,16,14) -> 5,12*
               f1(4,14,14) -> 5,12*
               f1(4,16,14) -> 5,12*
               f1(2,1,4) -> 12*,5,10
               f1(16,14,1) -> 5,12*
               f1(14,14,2) -> 5,12*
               f1(2,3,4) -> 12*,5,10
               f1(16,1,3) -> 5,12*
               f1(16,16,1) -> 5,12*
               f1(14,16,2) -> 5,12*
               f1(4,14,2) -> 5,12*
               f1(1,14,1) -> 5,12*
               f1(16,3,3) -> 5,12*
               f1(4,16,2) -> 5,12*
               f1(1,1,3) -> 12*,5,10
               f1(1,16,1) -> 5,12*
               f1(1,3,3) -> 12*,5,10
               f1(2,1,1) -> 12*,5,10
               f1(2,3,1) -> 12*,5,10
               f1(3,2,16) -> 5,12*
               f1(3,4,16) -> 5,12*
               f1(3,2,4) -> 12*,5,10
               f1(16,2,14) -> 5,12*
               f1(3,4,4) -> 12*,5,10
               f1(16,4,14) -> 5,12*
               f1(1,2,14) -> 5,12*
               f1(2,2,3) -> 12*,5,10
               f1(3,14,16) -> 5,12*
               f1(1,4,14) -> 5,12*
               f1(2,4,3) -> 12*,5,10
               f1(16,2,2) -> 5,12*
               f1(3,16,16) -> 5,12*
               f1(16,4,2) -> 5,12*
               f1(3,2,1) -> 12*,5,10
               f1(1,2,2) -> 12*,5,10
               f1(14,1,16) -> 5,12*
               f1(3,14,4) -> 5,12*
               f1(3,4,1) -> 12*,5,10
               f1(1,4,2) -> 12*,5,10
               f1(14,3,16) -> 5,12*
               f1(4,1,16) -> 5,12*
               f1(16,14,14) -> 5,12*
               f1(3,16,4) -> 5,12*
               f1(4,3,16) -> 5,12*
               f1(16,16,14) -> 5,12*
               f1(14,1,4) -> 5,12*
               f1(1,14,14) -> 5,12*
               f1(2,14,3) -> 5,12*
               f1(1,1,16) -> 5,12*
               f1(1,16,14) -> 5,12*
               f1(14,3,4) -> 5,12*
               f1(4,1,4) -> 12*,5,10
               f1(2,16,3) -> 5,12*
               f1(16,14,2) -> 5,12*
               f1(4,3,4) -> 12*,5,10
               f1(16,16,2) -> 5,12*
               f1(3,14,1) -> 5,12*
               f1(1,14,2) -> 5,12*
               f1(2,1,14) -> 5,12*
               f1(3,1,3) -> 12*,5,10
               f1(3,16,1) -> 5,12*
               f1(1,16,2) -> 5,12*
               f1(2,3,14) -> 5,12*
               f1(3,3,3) -> 12*,5,10
               f1(14,1,1) -> 5,12*
               f1(14,3,1) -> 5,12*
               f1(4,1,1) -> 12*,5,10
               f1(2,1,2) -> 12*,5,10
               f1(4,3,1) -> 12*,5,10
               f1(2,3,2) -> 12*,5,10
               f1(14,2,3) -> 5,12*
               f1(3,2,14) -> 5,12*
               f1(14,4,3) -> 5,12*
               f1(4,2,3) -> 12*,5,10
               f1(3,4,14) -> 5,12*
               f1(4,4,3) -> 12*,5,10
               ok1(5) -> 5,12*
               ok1(12) -> 5,12*
             problem:
              strict:

              weak:
               f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
               proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
               active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
               active(b()) -> mark(a())
               top(mark(X)) -> top(proper(X))
               proper(a()) -> ok(a())
               proper(b()) -> ok(b())
               f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
               top(ok(X)) -> top(active(X))
               active(f(a(),X,X)) -> mark(f(X,b(),b()))
             Qed

Tool IRC1

Execution Time	Unknown
Answer	MAYBE
Input	Transformed CSR 04 Ex9 Luc06 C

stdout:

MAYBE

Tool IRC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Transformed CSR 04 Ex9 Luc06 C

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  active(f(a(), X, X)) -> mark(f(X, b(), b()))
     , active(b()) -> mark(a())
     , active(f(X1, X2, X3)) -> f(X1, active(X2), X3)
     , f(X1, mark(X2), X3) -> mark(f(X1, X2, X3))
     , proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3))
     , proper(a()) -> ok(a())
     , proper(b()) -> ok(b())
     , f(ok(X1), ok(X2), ok(X3)) -> ok(f(X1, X2, X3))
     , top(mark(X)) -> top(proper(X))
     , top(ok(X)) -> top(active(X))}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution Time	Unknown
Answer	MAYBE
Input	Transformed CSR 04 Ex9 Luc06 C

stdout:

MAYBE

Tool RC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Transformed CSR 04 Ex9 Luc06 C

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  active(f(a(), X, X)) -> mark(f(X, b(), b()))
     , active(b()) -> mark(a())
     , active(f(X1, X2, X3)) -> f(X1, active(X2), X3)
     , f(X1, mark(X2), X3) -> mark(f(X1, X2, X3))
     , proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3))
     , proper(a()) -> ok(a())
     , proper(b()) -> ok(b())
     , f(ok(X1), ok(X2), ok(X3)) -> ok(f(X1, X2, X3))
     , top(mark(X)) -> top(proper(X))
     , top(ok(X)) -> top(active(X))}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds