Problem Transformed CSR 04 Ex16 Luc06 C

Tool CaT

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

stdout:

YES(?,O(n^1))

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

Proof:
Complexity Transformation Processor:
  strict:
   active(f(X,X)) -> mark(f(a(),b()))
   active(b()) -> mark(a())
   active(f(X1,X2)) -> f(active(X1),X2)
   f(mark(X1),X2) -> mark(f(X1,X2))
   proper(f(X1,X2)) -> f(proper(X1),proper(X2))
   proper(a()) -> ok(a())
   proper(b()) -> ok(b())
   f(ok(X1),ok(X2)) -> ok(f(X1,X2))
   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 1 0]
     [top](x0) = [0 0 0]x0
                 [0 0 0]  ,

                [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 1 0]
     [mark](x0) = [0 0 1]x0
                  [0 0 0]  ,

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

           [0]
     [a] = [0]
           [0],

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

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

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

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

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

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

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

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

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

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

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

       [ok](x0) = x0 + 9,

       [proper](x0) = x0 + 26,

       [mark](x0) = x0 + 8,

       [b] = 8,

       [a] = 0,

       [active](x0) = x0,

       [f](x0, x1) = x0 + x1 + 20
      orientation:
       active(f(X,X)) = 2X + 20 >= 36 = mark(f(a(),b()))

       active(f(X1,X2)) = X1 + X2 + 20 >= X1 + X2 + 20 = f(active(X1),X2)

       f(mark(X1),X2) = X1 + X2 + 28 >= X1 + X2 + 28 = mark(f(X1,X2))

       proper(f(X1,X2)) = X1 + X2 + 46 >= X1 + X2 + 72 = f(proper(X1),proper(X2))

       proper(a()) = 26 >= 9 = ok(a())

       proper(b()) = 34 >= 17 = ok(b())

       f(ok(X1),ok(X2)) = X1 + X2 + 38 >= X1 + X2 + 29 = ok(f(X1,X2))

       top(mark(X)) = X + 14 >= X + 32 = top(proper(X))

       top(ok(X)) = X + 15 >= X + 6 = top(active(X))

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

         [ok](x0) = x0,

         [proper](x0) = x0,

         [mark](x0) = x0 + 1,

         [b] = 3,

         [a] = 2,

         [active](x0) = x0,

         [f](x0, x1) = x0 + x1
        orientation:
         active(f(X,X)) = 2X >= 6 = mark(f(a(),b()))

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

         f(mark(X1),X2) = X1 + X2 + 1 >= X1 + X2 + 1 = mark(f(X1,X2))

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

         top(mark(X)) = X + 1 >= X = top(proper(X))

         proper(a()) = 2 >= 2 = ok(a())

         proper(b()) = 3 >= 3 = ok(b())

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

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

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

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

Tool IRC1

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

stdout:

MAYBE

Tool IRC2

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

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  active(f(X, X)) -> mark(f(a(), b()))
     , active(b()) -> mark(a())
     , active(f(X1, X2)) -> f(active(X1), X2)
     , f(mark(X1), X2) -> mark(f(X1, X2))
     , proper(f(X1, X2)) -> f(proper(X1), proper(X2))
     , proper(a()) -> ok(a())
     , proper(b()) -> ok(b())
     , f(ok(X1), ok(X2)) -> ok(f(X1, X2))
     , 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 Ex16 Luc06 C

stdout:

MAYBE

Tool RC2

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

stdout:

TIMEOUT

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

Proof Output:
  Computation stopped due to timeout after 60.0 seconds