Problem SK90 4.05

Tool CaT

Execution TimeUnknown
Answer
MAYBE
InputSK90 4.05

stdout:

MAYBE

Problem:
 *(x,+(y,z)) -> +(*(x,y),*(x,z))
 *(+(x,y),z) -> +(*(x,z),*(y,z))
 *(x,1()) -> x
 *(1(),y) -> y

Proof:
 Open

Tool IRC1

Execution TimeUnknown
Answer
MAYBE
InputSK90 4.05

stdout:

MAYBE

Tool IRC2

Execution TimeUnknown
Answer
MAYBE
InputSK90 4.05

stdout:

MAYBE

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           MAYBE
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  *(x, +(y, z)) -> +(*(x, y), *(x, z))
     , *(+(x, y), z) -> +(*(x, z), *(y, z))
     , *(x, 1()) -> x
     , *(1(), y) -> y}

Proof Output:    
  None of the processors succeeded.
  
  Details of failed attempt(s):
  -----------------------------
    1) 'wdg' failed due to the following reason:
         Transformation Details:
         -----------------------
           We have computed the following set of weak (innermost) dependency pairs:
           
             {  1: *^#(x, +(y, z)) -> c_0(*^#(x, y), *^#(x, z))
              , 2: *^#(+(x, y), z) -> c_1(*^#(x, z), *^#(y, z))
              , 3: *^#(x, 1()) -> c_2()
              , 4: *^#(1(), y) -> c_3()}
           
           Following Dependency Graph (modulo SCCs) was computed. (Answers to
           subproofs are indicated to the right.)
           
             ->{1,2}                                                     [       MAYBE        ]
                |
                |->{3}                                                   [         NA         ]
                |
                `->{4}                                                   [         NA         ]
             
           
         
         Sub-problems:
         -------------
           * Path {1,2}: MAYBE
             -----------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(*) = {}, Uargs(+) = {}, Uargs(*^#) = {}, Uargs(c_0) = {1, 2},
                 Uargs(c_1) = {1, 2}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                *(x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0]
                            [0 0 0]      [0 0 0]      [0]
                            [0 0 0]      [0 0 0]      [0]
                +(x1, x2) = [1 3 3] x1 + [1 3 3] x2 + [0]
                            [0 1 3]      [0 1 3]      [0]
                            [0 0 1]      [0 0 1]      [0]
                1() = [0]
                      [0]
                      [0]
                *^#(x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0]
                              [3 3 3]      [3 3 3]      [0]
                              [3 3 3]      [3 3 3]      [0]
                c_0(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
                              [0 1 0]      [0 1 0]      [0]
                              [0 0 1]      [0 0 1]      [0]
                c_1(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
                              [0 1 0]      [0 1 0]      [0]
                              [0 0 1]      [0 0 1]      [0]
                c_2() = [0]
                        [0]
                        [0]
                c_3() = [0]
                        [0]
                        [0]
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 3'
             --------------------------------------
             Answer:           MAYBE
             Input Problem:    innermost DP runtime-complexity with respect to
               Strict Rules:
                 {  *^#(x, +(y, z)) -> c_0(*^#(x, y), *^#(x, z))
                  , *^#(+(x, y), z) -> c_1(*^#(x, z), *^#(y, z))}
               Weak Rules: {}
             
             Proof Output:    
               The input cannot be shown compatible
           
           * Path {1,2}->{3}: NA
             -------------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(*) = {}, Uargs(+) = {}, Uargs(*^#) = {}, Uargs(c_0) = {1, 2},
                 Uargs(c_1) = {1, 2}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                *(x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0]
                            [0 0 0]      [0 0 0]      [0]
                            [0 0 0]      [0 0 0]      [0]
                +(x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0]
                            [0 0 0]      [0 0 0]      [0]
                            [0 0 0]      [0 0 0]      [0]
                1() = [0]
                      [0]
                      [0]
                *^#(x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0]
                              [0 0 0]      [0 0 0]      [0]
                              [0 0 0]      [0 0 0]      [0]
                c_0(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
                              [0 1 0]      [0 1 0]      [0]
                              [0 0 1]      [0 0 1]      [0]
                c_1(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
                              [0 1 0]      [0 1 0]      [0]
                              [0 0 1]      [0 0 1]      [0]
                c_2() = [0]
                        [0]
                        [0]
                c_3() = [0]
                        [0]
                        [0]
             
             We have not generated a proof for the resulting sub-problem.
           
           * Path {1,2}->{4}: NA
             -------------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(*) = {}, Uargs(+) = {}, Uargs(*^#) = {}, Uargs(c_0) = {1, 2},
                 Uargs(c_1) = {1, 2}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                *(x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0]
                            [0 0 0]      [0 0 0]      [0]
                            [0 0 0]      [0 0 0]      [0]
                +(x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0]
                            [0 0 0]      [0 0 0]      [0]
                            [0 0 0]      [0 0 0]      [0]
                1() = [0]
                      [0]
                      [0]
                *^#(x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0]
                              [0 0 0]      [0 0 0]      [0]
                              [0 0 0]      [0 0 0]      [0]
                c_0(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
                              [0 1 0]      [0 1 0]      [0]
                              [0 0 1]      [0 0 1]      [0]
                c_1(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
                              [0 1 0]      [0 1 0]      [0]
                              [0 0 1]      [0 0 1]      [0]
                c_2() = [0]
                        [0]
                        [0]
                c_3() = [0]
                        [0]
                        [0]
             
             We have not generated a proof for the resulting sub-problem.
    
    2) 'wdg' failed due to the following reason:
         Transformation Details:
         -----------------------
           We have computed the following set of weak (innermost) dependency pairs:
           
             {  1: *^#(x, +(y, z)) -> c_0(*^#(x, y), *^#(x, z))
              , 2: *^#(+(x, y), z) -> c_1(*^#(x, z), *^#(y, z))
              , 3: *^#(x, 1()) -> c_2()
              , 4: *^#(1(), y) -> c_3()}
           
           Following Dependency Graph (modulo SCCs) was computed. (Answers to
           subproofs are indicated to the right.)
           
             ->{1,2}                                                     [       MAYBE        ]
                |
                |->{3}                                                   [         NA         ]
                |
                `->{4}                                                   [         NA         ]
             
           
         
         Sub-problems:
         -------------
           * Path {1,2}: MAYBE
             -----------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(*) = {}, Uargs(+) = {}, Uargs(*^#) = {}, Uargs(c_0) = {1, 2},
                 Uargs(c_1) = {1, 2}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                *(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                            [0 0]      [0 0]      [0]
                +(x1, x2) = [1 3] x1 + [1 3] x2 + [0]
                            [0 1]      [0 1]      [0]
                1() = [0]
                      [0]
                *^#(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                              [3 3]      [3 3]      [0]
                c_0(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                              [0 1]      [0 1]      [0]
                c_1(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                              [0 1]      [0 1]      [0]
                c_2() = [0]
                        [0]
                c_3() = [0]
                        [0]
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 2'
             --------------------------------------
             Answer:           MAYBE
             Input Problem:    innermost DP runtime-complexity with respect to
               Strict Rules:
                 {  *^#(x, +(y, z)) -> c_0(*^#(x, y), *^#(x, z))
                  , *^#(+(x, y), z) -> c_1(*^#(x, z), *^#(y, z))}
               Weak Rules: {}
             
             Proof Output:    
               The input cannot be shown compatible
           
           * Path {1,2}->{3}: NA
             -------------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(*) = {}, Uargs(+) = {}, Uargs(*^#) = {}, Uargs(c_0) = {1, 2},
                 Uargs(c_1) = {1, 2}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                *(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                            [0 0]      [0 0]      [0]
                +(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                            [0 0]      [0 0]      [0]
                1() = [0]
                      [0]
                *^#(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                              [0 0]      [0 0]      [0]
                c_0(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                              [0 1]      [0 1]      [0]
                c_1(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                              [0 1]      [0 1]      [0]
                c_2() = [0]
                        [0]
                c_3() = [0]
                        [0]
             
             We have not generated a proof for the resulting sub-problem.
           
           * Path {1,2}->{4}: NA
             -------------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(*) = {}, Uargs(+) = {}, Uargs(*^#) = {}, Uargs(c_0) = {1, 2},
                 Uargs(c_1) = {1, 2}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                *(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                            [0 0]      [0 0]      [0]
                +(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                            [0 0]      [0 0]      [0]
                1() = [0]
                      [0]
                *^#(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                              [0 0]      [0 0]      [0]
                c_0(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                              [0 1]      [0 1]      [0]
                c_1(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                              [0 1]      [0 1]      [0]
                c_2() = [0]
                        [0]
                c_3() = [0]
                        [0]
             
             We have not generated a proof for the resulting sub-problem.
    
    3) 'wdg' failed due to the following reason:
         Transformation Details:
         -----------------------
           We have computed the following set of weak (innermost) dependency pairs:
           
             {  1: *^#(x, +(y, z)) -> c_0(*^#(x, y), *^#(x, z))
              , 2: *^#(+(x, y), z) -> c_1(*^#(x, z), *^#(y, z))
              , 3: *^#(x, 1()) -> c_2()
              , 4: *^#(1(), y) -> c_3()}
           
           Following Dependency Graph (modulo SCCs) was computed. (Answers to
           subproofs are indicated to the right.)
           
             ->{1,2}                                                     [       MAYBE        ]
                |
                |->{3}                                                   [         NA         ]
                |
                `->{4}                                                   [         NA         ]
             
           
         
         Sub-problems:
         -------------
           * Path {1,2}: MAYBE
             -----------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(*) = {}, Uargs(+) = {}, Uargs(*^#) = {}, Uargs(c_0) = {1, 2},
                 Uargs(c_1) = {1, 2}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                *(x1, x2) = [0] x1 + [0] x2 + [0]
                +(x1, x2) = [1] x1 + [1] x2 + [0]
                1() = [0]
                *^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_0(x1, x2) = [1] x1 + [1] x2 + [0]
                c_1(x1, x2) = [1] x1 + [1] x2 + [0]
                c_2() = [0]
                c_3() = [0]
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 1'
             --------------------------------------
             Answer:           MAYBE
             Input Problem:    innermost DP runtime-complexity with respect to
               Strict Rules:
                 {  *^#(x, +(y, z)) -> c_0(*^#(x, y), *^#(x, z))
                  , *^#(+(x, y), z) -> c_1(*^#(x, z), *^#(y, z))}
               Weak Rules: {}
             
             Proof Output:    
               The input cannot be shown compatible
           
           * Path {1,2}->{3}: NA
             -------------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(*) = {}, Uargs(+) = {}, Uargs(*^#) = {}, Uargs(c_0) = {1, 2},
                 Uargs(c_1) = {1, 2}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                *(x1, x2) = [0] x1 + [0] x2 + [0]
                +(x1, x2) = [0] x1 + [0] x2 + [0]
                1() = [0]
                *^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_0(x1, x2) = [1] x1 + [1] x2 + [0]
                c_1(x1, x2) = [1] x1 + [1] x2 + [0]
                c_2() = [0]
                c_3() = [0]
             
             We have not generated a proof for the resulting sub-problem.
           
           * Path {1,2}->{4}: NA
             -------------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(*) = {}, Uargs(+) = {}, Uargs(*^#) = {}, Uargs(c_0) = {1, 2},
                 Uargs(c_1) = {1, 2}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                *(x1, x2) = [0] x1 + [0] x2 + [0]
                +(x1, x2) = [0] x1 + [0] x2 + [0]
                1() = [0]
                *^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_0(x1, x2) = [1] x1 + [1] x2 + [0]
                c_1(x1, x2) = [1] x1 + [1] x2 + [0]
                c_2() = [0]
                c_3() = [0]
             
             We have not generated a proof for the resulting sub-problem.
    
    4) 'matrix-interpretation of dimension 1' failed due to the following reason:
         The input cannot be shown compatible
    
    5) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason:
         match-boundness of the problem could not be verified.
    
    6) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason:
         match-boundness of the problem could not be verified.
    

Tool RC1

Execution TimeUnknown
Answer
MAYBE
InputSK90 4.05

stdout:

MAYBE

Tool RC2

Execution TimeUnknown
Answer
MAYBE
InputSK90 4.05

stdout:

MAYBE

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           MAYBE
Input Problem:    runtime-complexity with respect to
  Rules:
    {  *(x, +(y, z)) -> +(*(x, y), *(x, z))
     , *(+(x, y), z) -> +(*(x, z), *(y, z))
     , *(x, 1()) -> x
     , *(1(), y) -> y}

Proof Output:    
  None of the processors succeeded.
  
  Details of failed attempt(s):
  -----------------------------
    1) 'wdg' failed due to the following reason:
         Transformation Details:
         -----------------------
           We have computed the following set of weak (innermost) dependency pairs:
           
             {  1: *^#(x, +(y, z)) -> c_0(*^#(x, y), *^#(x, z))
              , 2: *^#(+(x, y), z) -> c_1(*^#(x, z), *^#(y, z))
              , 3: *^#(x, 1()) -> c_2(x)
              , 4: *^#(1(), y) -> c_3(y)}
           
           Following Dependency Graph (modulo SCCs) was computed. (Answers to
           subproofs are indicated to the right.)
           
             ->{1,2}                                                     [       MAYBE        ]
                |
                |->{3}                                                   [         NA         ]
                |
                `->{4}                                                   [         NA         ]
             
           
         
         Sub-problems:
         -------------
           * Path {1,2}: MAYBE
             -----------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(*) = {}, Uargs(+) = {}, Uargs(*^#) = {}, Uargs(c_0) = {1, 2},
                 Uargs(c_1) = {1, 2}, Uargs(c_2) = {}, Uargs(c_3) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                *(x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0]
                            [0 0 0]      [0 0 0]      [0]
                            [0 0 0]      [0 0 0]      [0]
                +(x1, x2) = [1 3 3] x1 + [1 3 3] x2 + [0]
                            [0 1 3]      [0 1 3]      [0]
                            [0 0 1]      [0 0 1]      [0]
                1() = [0]
                      [0]
                      [0]
                *^#(x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0]
                              [3 3 3]      [3 3 3]      [0]
                              [3 3 3]      [3 3 3]      [0]
                c_0(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
                              [0 1 0]      [0 1 0]      [0]
                              [0 0 1]      [0 0 1]      [0]
                c_1(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
                              [0 1 0]      [0 1 0]      [0]
                              [0 0 1]      [0 0 1]      [0]
                c_2(x1) = [0 0 0] x1 + [0]
                          [0 0 0]      [0]
                          [0 0 0]      [0]
                c_3(x1) = [0 0 0] x1 + [0]
                          [0 0 0]      [0]
                          [0 0 0]      [0]
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 3'
             --------------------------------------
             Answer:           MAYBE
             Input Problem:    DP runtime-complexity with respect to
               Strict Rules:
                 {  *^#(x, +(y, z)) -> c_0(*^#(x, y), *^#(x, z))
                  , *^#(+(x, y), z) -> c_1(*^#(x, z), *^#(y, z))}
               Weak Rules: {}
             
             Proof Output:    
               The input cannot be shown compatible
           
           * Path {1,2}->{3}: NA
             -------------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(*) = {}, Uargs(+) = {}, Uargs(*^#) = {}, Uargs(c_0) = {1, 2},
                 Uargs(c_1) = {1, 2}, Uargs(c_2) = {}, Uargs(c_3) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                *(x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0]
                            [0 0 0]      [0 0 0]      [0]
                            [0 0 0]      [0 0 0]      [0]
                +(x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0]
                            [0 0 0]      [0 0 0]      [0]
                            [0 0 0]      [0 0 0]      [0]
                1() = [0]
                      [0]
                      [0]
                *^#(x1, x2) = [3 3 3] x1 + [0 0 0] x2 + [0]
                              [0 0 0]      [0 0 0]      [0]
                              [0 0 0]      [0 0 0]      [0]
                c_0(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
                              [0 1 0]      [0 1 0]      [0]
                              [0 0 1]      [0 0 1]      [0]
                c_1(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
                              [0 1 0]      [0 1 0]      [0]
                              [0 0 1]      [0 0 1]      [0]
                c_2(x1) = [1 1 1] x1 + [0]
                          [0 0 0]      [0]
                          [0 0 0]      [0]
                c_3(x1) = [0 0 0] x1 + [0]
                          [0 0 0]      [0]
                          [0 0 0]      [0]
             
             We have not generated a proof for the resulting sub-problem.
           
           * Path {1,2}->{4}: NA
             -------------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(*) = {}, Uargs(+) = {}, Uargs(*^#) = {}, Uargs(c_0) = {1, 2},
                 Uargs(c_1) = {1, 2}, Uargs(c_2) = {}, Uargs(c_3) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                *(x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0]
                            [0 0 0]      [0 0 0]      [0]
                            [0 0 0]      [0 0 0]      [0]
                +(x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0]
                            [0 0 0]      [0 0 0]      [0]
                            [0 0 0]      [0 0 0]      [0]
                1() = [0]
                      [0]
                      [0]
                *^#(x1, x2) = [0 0 0] x1 + [3 3 3] x2 + [0]
                              [0 0 0]      [0 0 0]      [0]
                              [0 0 0]      [0 0 0]      [0]
                c_0(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
                              [0 1 0]      [0 1 0]      [0]
                              [0 0 1]      [0 0 1]      [0]
                c_1(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
                              [0 1 0]      [0 1 0]      [0]
                              [0 0 1]      [0 0 1]      [0]
                c_2(x1) = [0 0 0] x1 + [0]
                          [0 0 0]      [0]
                          [0 0 0]      [0]
                c_3(x1) = [1 1 1] x1 + [0]
                          [0 0 0]      [0]
                          [0 0 0]      [0]
             
             We have not generated a proof for the resulting sub-problem.
    
    2) 'wdg' failed due to the following reason:
         Transformation Details:
         -----------------------
           We have computed the following set of weak (innermost) dependency pairs:
           
             {  1: *^#(x, +(y, z)) -> c_0(*^#(x, y), *^#(x, z))
              , 2: *^#(+(x, y), z) -> c_1(*^#(x, z), *^#(y, z))
              , 3: *^#(x, 1()) -> c_2(x)
              , 4: *^#(1(), y) -> c_3(y)}
           
           Following Dependency Graph (modulo SCCs) was computed. (Answers to
           subproofs are indicated to the right.)
           
             ->{1,2}                                                     [       MAYBE        ]
                |
                |->{3}                                                   [         NA         ]
                |
                `->{4}                                                   [         NA         ]
             
           
         
         Sub-problems:
         -------------
           * Path {1,2}: MAYBE
             -----------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(*) = {}, Uargs(+) = {}, Uargs(*^#) = {}, Uargs(c_0) = {1, 2},
                 Uargs(c_1) = {1, 2}, Uargs(c_2) = {}, Uargs(c_3) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                *(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                            [0 0]      [0 0]      [0]
                +(x1, x2) = [1 3] x1 + [1 3] x2 + [0]
                            [0 1]      [0 1]      [0]
                1() = [0]
                      [0]
                *^#(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                              [3 3]      [3 3]      [0]
                c_0(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                              [0 1]      [0 1]      [0]
                c_1(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                              [0 1]      [0 1]      [0]
                c_2(x1) = [0 0] x1 + [0]
                          [0 0]      [0]
                c_3(x1) = [0 0] x1 + [0]
                          [0 0]      [0]
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 2'
             --------------------------------------
             Answer:           MAYBE
             Input Problem:    DP runtime-complexity with respect to
               Strict Rules:
                 {  *^#(x, +(y, z)) -> c_0(*^#(x, y), *^#(x, z))
                  , *^#(+(x, y), z) -> c_1(*^#(x, z), *^#(y, z))}
               Weak Rules: {}
             
             Proof Output:    
               The input cannot be shown compatible
           
           * Path {1,2}->{3}: NA
             -------------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(*) = {}, Uargs(+) = {}, Uargs(*^#) = {}, Uargs(c_0) = {1, 2},
                 Uargs(c_1) = {1, 2}, Uargs(c_2) = {}, Uargs(c_3) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                *(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                            [0 0]      [0 0]      [0]
                +(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                            [0 0]      [0 0]      [0]
                1() = [0]
                      [0]
                *^#(x1, x2) = [3 3] x1 + [0 0] x2 + [0]
                              [0 0]      [0 0]      [0]
                c_0(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                              [0 1]      [0 1]      [0]
                c_1(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                              [0 1]      [0 1]      [0]
                c_2(x1) = [1 1] x1 + [0]
                          [0 0]      [0]
                c_3(x1) = [0 0] x1 + [0]
                          [0 0]      [0]
             
             We have not generated a proof for the resulting sub-problem.
           
           * Path {1,2}->{4}: NA
             -------------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(*) = {}, Uargs(+) = {}, Uargs(*^#) = {}, Uargs(c_0) = {1, 2},
                 Uargs(c_1) = {1, 2}, Uargs(c_2) = {}, Uargs(c_3) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                *(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                            [0 0]      [0 0]      [0]
                +(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                            [0 0]      [0 0]      [0]
                1() = [0]
                      [0]
                *^#(x1, x2) = [0 0] x1 + [3 3] x2 + [0]
                              [0 0]      [0 0]      [0]
                c_0(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                              [0 1]      [0 1]      [0]
                c_1(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                              [0 1]      [0 1]      [0]
                c_2(x1) = [0 0] x1 + [0]
                          [0 0]      [0]
                c_3(x1) = [1 1] x1 + [0]
                          [0 0]      [0]
             
             We have not generated a proof for the resulting sub-problem.
    
    3) 'wdg' failed due to the following reason:
         Transformation Details:
         -----------------------
           We have computed the following set of weak (innermost) dependency pairs:
           
             {  1: *^#(x, +(y, z)) -> c_0(*^#(x, y), *^#(x, z))
              , 2: *^#(+(x, y), z) -> c_1(*^#(x, z), *^#(y, z))
              , 3: *^#(x, 1()) -> c_2(x)
              , 4: *^#(1(), y) -> c_3(y)}
           
           Following Dependency Graph (modulo SCCs) was computed. (Answers to
           subproofs are indicated to the right.)
           
             ->{1,2}                                                     [       MAYBE        ]
                |
                |->{3}                                                   [         NA         ]
                |
                `->{4}                                                   [         NA         ]
             
           
         
         Sub-problems:
         -------------
           * Path {1,2}: MAYBE
             -----------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(*) = {}, Uargs(+) = {}, Uargs(*^#) = {}, Uargs(c_0) = {1, 2},
                 Uargs(c_1) = {1, 2}, Uargs(c_2) = {}, Uargs(c_3) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                *(x1, x2) = [0] x1 + [0] x2 + [0]
                +(x1, x2) = [1] x1 + [1] x2 + [0]
                1() = [0]
                *^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_0(x1, x2) = [1] x1 + [1] x2 + [0]
                c_1(x1, x2) = [1] x1 + [1] x2 + [0]
                c_2(x1) = [0] x1 + [0]
                c_3(x1) = [0] x1 + [0]
             
             We apply the sub-processor on the resulting sub-problem:
             
             'matrix-interpretation of dimension 1'
             --------------------------------------
             Answer:           MAYBE
             Input Problem:    DP runtime-complexity with respect to
               Strict Rules:
                 {  *^#(x, +(y, z)) -> c_0(*^#(x, y), *^#(x, z))
                  , *^#(+(x, y), z) -> c_1(*^#(x, z), *^#(y, z))}
               Weak Rules: {}
             
             Proof Output:    
               The input cannot be shown compatible
           
           * Path {1,2}->{3}: NA
             -------------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(*) = {}, Uargs(+) = {}, Uargs(*^#) = {}, Uargs(c_0) = {1, 2},
                 Uargs(c_1) = {1, 2}, Uargs(c_2) = {}, Uargs(c_3) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                *(x1, x2) = [0] x1 + [0] x2 + [0]
                +(x1, x2) = [0] x1 + [0] x2 + [0]
                1() = [0]
                *^#(x1, x2) = [3] x1 + [0] x2 + [0]
                c_0(x1, x2) = [1] x1 + [1] x2 + [0]
                c_1(x1, x2) = [1] x1 + [1] x2 + [0]
                c_2(x1) = [1] x1 + [0]
                c_3(x1) = [0] x1 + [0]
             
             We have not generated a proof for the resulting sub-problem.
           
           * Path {1,2}->{4}: NA
             -------------------
             
             The usable rules of this path are empty.
             
             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(*) = {}, Uargs(+) = {}, Uargs(*^#) = {}, Uargs(c_0) = {1, 2},
                 Uargs(c_1) = {1, 2}, Uargs(c_2) = {}, Uargs(c_3) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                *(x1, x2) = [0] x1 + [0] x2 + [0]
                +(x1, x2) = [0] x1 + [0] x2 + [0]
                1() = [0]
                *^#(x1, x2) = [0] x1 + [3] x2 + [0]
                c_0(x1, x2) = [1] x1 + [1] x2 + [0]
                c_1(x1, x2) = [1] x1 + [1] x2 + [0]
                c_2(x1) = [0] x1 + [0]
                c_3(x1) = [1] x1 + [0]
             
             We have not generated a proof for the resulting sub-problem.
    
    4) 'matrix-interpretation of dimension 1' failed due to the following reason:
         The input cannot be shown compatible
    
    5) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason:
         match-boundness of the problem could not be verified.
    
    6) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason:
         match-boundness of the problem could not be verified.
    

Tool pair1rc

Execution TimeUnknown
Answer
MAYBE
InputSK90 4.05

stdout:

MAYBE

We consider the following Problem:

  Strict Trs:
    {  *(x, +(y, z)) -> +(*(x, y), *(x, z))
     , *(+(x, y), z) -> +(*(x, z), *(y, z))
     , *(x, 1()) -> x
     , *(1(), y) -> y}
  StartTerms: basic terms
  Strategy: none

Certificate: MAYBE

Application of 'pair1 (timeout of 60.0 seconds)':
-------------------------------------------------
  The processor is not applicable, reason is:
   Input problem is not restricted to innermost rewriting
  
  We abort the transformation and continue with the subprocessor on the problem
  
  Strict Trs:
    {  *(x, +(y, z)) -> +(*(x, y), *(x, z))
     , *(+(x, y), z) -> +(*(x, z), *(y, z))
     , *(x, 1()) -> x
     , *(1(), y) -> y}
  StartTerms: basic terms
  Strategy: none
  
  1) None of the processors succeeded.
     
     Details of failed attempt(s):
     -----------------------------
       1) 'dp' failed due to the following reason:
            We have computed the following dependency pairs
            
            Strict Dependency Pairs:
              {  *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
               , *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))
               , *^#(x, 1()) -> c_3(x)
               , *^#(1(), y) -> c_4(y)}
            
            We consider the following Problem:
            
              Strict DPs:
                {  *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
                 , *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))
                 , *^#(x, 1()) -> c_3(x)
                 , *^#(1(), y) -> c_4(y)}
              Strict Trs:
                {  *(x, +(y, z)) -> +(*(x, y), *(x, z))
                 , *(+(x, y), z) -> +(*(x, z), *(y, z))
                 , *(x, 1()) -> x
                 , *(1(), y) -> y}
              StartTerms: basic terms
              Strategy: none
            
            Certificate: MAYBE
            
            Application of 'Fastest':
            -------------------------
              None of the processors succeeded.
              
              Details of failed attempt(s):
              -----------------------------
                1) 'pathanalysis' failed due to the following reason:
                     We use following congruence DG for path analysis
                     
                     ->{1,2}                                                     [       MAYBE        ]
                        |
                        |->{3}                                                   [         ?          ]
                        |
                        `->{4}                                                   [         ?          ]
                     
                     
                     Here rules are as follows:
                     
                       {  1: *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
                        , 2: *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))
                        , 3: *^#(x, 1()) -> c_3(x)
                        , 4: *^#(1(), y) -> c_4(y)}
                     
                     * Path {1,2}: MAYBE
                       -----------------
                       
                       We consider the following Problem:
                       
                         Strict DPs:
                           {  *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
                            , *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))}
                         Strict Trs:
                           {  *(x, +(y, z)) -> +(*(x, y), *(x, z))
                            , *(+(x, y), z) -> +(*(x, z), *(y, z))
                            , *(x, 1()) -> x
                            , *(1(), y) -> y}
                         StartTerms: basic terms
                         Strategy: none
                       
                       Certificate: MAYBE
                       
                       Application of 'removetails >>> ... >>> ... >>> ...':
                       -----------------------------------------------------
                         The processor is inapplicable since the strict component of the
                         input problem is not empty
                         
                         We apply the transformation 'weightgap of dimension Nat 2, maximal degree 1, cbits 4 <> ...' on the resulting sub-problems:
                         Sub-problem 1:
                         --------------
                           We consider the problem
                           
                           Strict DPs:
                             {  *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
                              , *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))}
                           Strict Trs:
                             {  *(x, +(y, z)) -> +(*(x, y), *(x, z))
                              , *(+(x, y), z) -> +(*(x, z), *(y, z))
                              , *(x, 1()) -> x
                              , *(1(), y) -> y}
                           StartTerms: basic terms
                           Strategy: none
                           
                           We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
                           
                             The weightgap principle does not apply
                           
                           We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
                           
                           Strict DPs:
                             {  *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
                              , *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))}
                           Strict Trs:
                             {  *(x, +(y, z)) -> +(*(x, y), *(x, z))
                              , *(+(x, y), z) -> +(*(x, z), *(y, z))
                              , *(x, 1()) -> x
                              , *(1(), y) -> y}
                           StartTerms: basic terms
                           Strategy: none
                           
                             We fail transforming the problem using 'weightgap of dimension Nat 3, maximal degree 3, cbits 4'
                             
                               The weightgap principle does not apply
                             
                             We try instead 'weightgap of dimension Nat 4, maximal degree 3, cbits 4' on the problem
                             
                             Strict DPs:
                               {  *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
                                , *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))}
                             Strict Trs:
                               {  *(x, +(y, z)) -> +(*(x, y), *(x, z))
                                , *(+(x, y), z) -> +(*(x, z), *(y, z))
                                , *(x, 1()) -> x
                                , *(1(), y) -> y}
                             StartTerms: basic terms
                             Strategy: none
                             
                               The weightgap principle does not apply
                         
                         We abort the transformation and continue with the subprocessor on the problem
                         
                         Strict DPs:
                           {  *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
                            , *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))}
                         Strict Trs:
                           {  *(x, +(y, z)) -> +(*(x, y), *(x, z))
                            , *(+(x, y), z) -> +(*(x, z), *(y, z))
                            , *(x, 1()) -> x
                            , *(1(), y) -> y}
                         StartTerms: basic terms
                         Strategy: none
                         
                         1) None of the processors succeeded.
                            
                            Details of failed attempt(s):
                            -----------------------------
                              1) 'empty' failed due to the following reason:
                                   Empty strict component of the problem is NOT empty.
                              
                              2) 'Fastest' failed due to the following reason:
                                   None of the processors succeeded.
                                   
                                   Details of failed attempt(s):
                                   -----------------------------
                                     1) 'matrix-interpretation of dimension 4 (timeout of 100.0 seconds)' failed due to the following reason:
                                          The input cannot be shown compatible
                                     
                                     2) 'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' failed due to the following reason:
                                          The input cannot be shown compatible
                                     
                                     3) 'matrix-interpretation of dimension 2 (timeout of 100.0 seconds)' failed due to the following reason:
                                          The input cannot be shown compatible
                                     
                              
                         
                     
                     * Path {1,2}->{3}: ?
                       ------------------
                       
                       CANNOT find proof of path {1,2}->{3}. Propably computation has been aborted since some other path cannot be solved.
                     
                     * Path {1,2}->{4}: ?
                       ------------------
                       
                       CANNOT find proof of path {1,2}->{4}. Propably computation has been aborted since some other path cannot be solved.
                
                2) 'Sequentially' failed due to the following reason:
                     None of the processors succeeded.
                     
                     Details of failed attempt(s):
                     -----------------------------
                       1) 'empty' failed due to the following reason:
                            Empty strict component of the problem is NOT empty.
                       
                       2) 'Fastest' failed due to the following reason:
                            None of the processors succeeded.
                            
                            Details of failed attempt(s):
                            -----------------------------
                              1) 'matrix-interpretation of dimension 4 (timeout of 100.0 seconds)' failed due to the following reason:
                                   The input cannot be shown compatible
                              
                              2) 'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' failed due to the following reason:
                                   The input cannot be shown compatible
                              
                              3) 'matrix-interpretation of dimension 2 (timeout of 100.0 seconds)' failed due to the following reason:
                                   The input cannot be shown compatible
                              
                       
                
       
       2) 'Fastest' failed due to the following reason:
            None of the processors succeeded.
            
            Details of failed attempt(s):
            -----------------------------
              1) 'Sequentially' failed due to the following reason:
                   None of the processors succeeded.
                   
                   Details of failed attempt(s):
                   -----------------------------
                     1) 'empty' failed due to the following reason:
                          Empty strict component of the problem is NOT empty.
                     
                     2) 'Fastest' failed due to the following reason:
                          None of the processors succeeded.
                          
                          Details of failed attempt(s):
                          -----------------------------
                            1) 'matrix-interpretation of dimension 4 (timeout of 100.0 seconds)' failed due to the following reason:
                                 The input cannot be shown compatible
                            
                            2) 'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' failed due to the following reason:
                                 The input cannot be shown compatible
                            
                            3) 'matrix-interpretation of dimension 2 (timeout of 100.0 seconds)' failed due to the following reason:
                                 The input cannot be shown compatible
                            
                     
              
              2) 'Fastest' failed due to the following reason:
                   None of the processors succeeded.
                   
                   Details of failed attempt(s):
                   -----------------------------
                     1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason:
                          match-boundness of the problem could not be verified.
                     
                     2) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason:
                          match-boundness of the problem could not be verified.
                     
              
       
  

Arrrr..

Tool pair2rc

Execution TimeUnknown
Answer
TIMEOUT
InputSK90 4.05

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  *(x, +(y, z)) -> +(*(x, y), *(x, z))
     , *(+(x, y), z) -> +(*(x, z), *(y, z))
     , *(x, 1()) -> x
     , *(1(), y) -> y}
  StartTerms: basic terms
  Strategy: none

Certificate: TIMEOUT

Application of 'pair2 (timeout of 60.0 seconds)':
-------------------------------------------------
  Computation stopped due to timeout after 60.0 seconds

Arrrr..

Tool pair3irc

Execution TimeUnknown
Answer
TIMEOUT
InputSK90 4.05

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  *(x, +(y, z)) -> +(*(x, y), *(x, z))
     , *(+(x, y), z) -> +(*(x, z), *(y, z))
     , *(x, 1()) -> x
     , *(1(), y) -> y}
  StartTerms: basic terms
  Strategy: innermost

Certificate: TIMEOUT

Application of 'pair3 (timeout of 60.0 seconds)':
-------------------------------------------------
  Computation stopped due to timeout after 60.0 seconds

Arrrr..

Tool pair3rc

Execution TimeUnknown
Answer
TIMEOUT
InputSK90 4.05

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  *(x, +(y, z)) -> +(*(x, y), *(x, z))
     , *(+(x, y), z) -> +(*(x, z), *(y, z))
     , *(x, 1()) -> x
     , *(1(), y) -> y}
  StartTerms: basic terms
  Strategy: none

Certificate: TIMEOUT

Application of 'pair3 (timeout of 60.0 seconds)':
-------------------------------------------------
  Computation stopped due to timeout after 60.0 seconds

Arrrr..

Tool rc

Execution TimeUnknown
Answer
YES(?,O(n^1))
InputSK90 4.05

stdout:

YES(?,O(n^1))

We consider the following Problem:

  Strict Trs:
    {  *(x, +(y, z)) -> +(*(x, y), *(x, z))
     , *(+(x, y), z) -> +(*(x, z), *(y, z))
     , *(x, 1()) -> x
     , *(1(), y) -> y}
  StartTerms: basic terms
  Strategy: none

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

Application of 'rc (timeout of 60.0 seconds)':
----------------------------------------------
  'dp' proved the goal fastest:
  
  We have computed the following dependency pairs
  
  Strict Dependency Pairs:
    {  *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
     , *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))
     , *^#(x, 1()) -> c_3(x)
     , *^#(1(), y) -> c_4(y)}
  
  We consider the following Problem:
  
    Strict DPs:
      {  *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
       , *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))
       , *^#(x, 1()) -> c_3(x)
       , *^#(1(), y) -> c_4(y)}
    Strict Trs:
      {  *(x, +(y, z)) -> +(*(x, y), *(x, z))
       , *(+(x, y), z) -> +(*(x, z), *(y, z))
       , *(x, 1()) -> x
       , *(1(), y) -> y}
    StartTerms: basic terms
    Strategy: none
  
  Certificate: YES(?,O(n^1))
  
  Application of 'usablerules':
  -----------------------------
    No rule is usable.
    
    We consider the following Problem:
    
      Strict DPs:
        {  *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
         , *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))
         , *^#(x, 1()) -> c_3(x)
         , *^#(1(), y) -> c_4(y)}
      StartTerms: basic terms
      Strategy: none
    
    Certificate: YES(?,O(n^1))
    
    Application of 'Fastest':
    -------------------------
      'pathanalysis' proved the goal fastest:
      
      We use following congruence DG for path analysis
      
      ->{1,2}                                                     [   YES(?,O(n^1))    ]
         |
         |->{3}                                                   [   YES(O(1),O(1))   ]
         |
         `->{4}                                                   [   YES(O(1),O(1))   ]
      
      
      Here rules are as follows:
      
        {  1: *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
         , 2: *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))
         , 3: *^#(x, 1()) -> c_3(x)
         , 4: *^#(1(), y) -> c_4(y)}
      
      * Path {1,2}: YES(?,O(n^1))
        -------------------------
        
        We consider the following Problem:
        
          Strict DPs:
            {  *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
             , *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))}
          StartTerms: basic terms
          Strategy: none
        
        Certificate: YES(?,O(n^1))
        
        Application of 'removetails >>> ... >>> ... >>> ...':
        -----------------------------------------------------
          No dependency-pair could be removed
          
          We apply the transformation 'weightgap of dimension Nat 2, maximal degree 1, cbits 4 <> ...' on the resulting sub-problems:
          Sub-problem 1:
          --------------
            We consider the problem
            
            Strict DPs:
              {  *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
               , *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))}
            StartTerms: basic terms
            Strategy: none
            
            We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
            
              The weightgap principle does not apply
            
            We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
            
            Strict DPs:
              {  *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
               , *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))}
            StartTerms: basic terms
            Strategy: none
            
              We fail transforming the problem using 'weightgap of dimension Nat 3, maximal degree 3, cbits 4'
              
                The weightgap principle does not apply
              
              We try instead 'weightgap of dimension Nat 4, maximal degree 3, cbits 4' on the problem
              
              Strict DPs:
                {  *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
                 , *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))}
              StartTerms: basic terms
              Strategy: none
              
                The weightgap principle does not apply
          
          We abort the transformation and continue with the subprocessor on the problem
          
          Strict DPs:
            {  *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
             , *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))}
          StartTerms: basic terms
          Strategy: none
          
          1) 'Fastest' proved the goal fastest:
             
             'Bounds with perSymbol-enrichment and initial automaton 'match' (timeout of 5.0 seconds)' proved the goal fastest:
             
             The problem is match-bounded by 0.
             The enriched problem is compatible with the following automaton:
             {}
          
      
      * Path {1,2}->{3}: YES(O(1),O(1))
        -------------------------------
        
        We consider the following Problem:
        
          Strict DPs: {*^#(x, 1()) -> c_3(x)}
          Weak DPs:
            {  *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
             , *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))}
          StartTerms: basic terms
          Strategy: none
        
        Certificate: YES(O(1),O(1))
        
        Application of 'removetails >>> ... >>> ... >>> ...':
        -----------------------------------------------------
          We consider the the dependency-graph
          
            1: *^#(x, 1()) -> c_3(x)
            
            2: *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
                 --> *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z)): 3
                 --> *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z)): 2
                 --> *^#(x, 1()) -> c_3(x): 1
            
            3: *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))
                 --> *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z)): 3
                 --> *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z)): 2
                 --> *^#(x, 1()) -> c_3(x): 1
            
          
          together with the congruence-graph
          
            ->{2,3}                                                     Weak SCC
               |
               `->{1}                                                   Noncyclic, trivial, SCC
            
            
            Here rules are as follows:
            
              {  1: *^#(x, 1()) -> c_3(x)
               , 2: *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
               , 3: *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))}
          
          The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
          
            {  2: *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
             , 3: *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))
             , 1: *^#(x, 1()) -> c_3(x)}
          
          We consider the following Problem:
          
            StartTerms: basic terms
            Strategy: none
          
          Certificate: YES(O(1),O(1))
          
          Application of 'simpDPRHS >>> ...':
          -----------------------------------
            No rule was simplified
            
            We apply the transformation 'usablerules' on the resulting sub-problems:
            Sub-problem 1:
            --------------
              We consider the problem
              
              StartTerms: basic terms
              Strategy: none
              
              The input problem is not a DP-problem.
            
            We abort the transformation and continue with the subprocessor on the problem
            
            StartTerms: basic terms
            Strategy: none
            
            1) We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
               
                 All strict components are empty, nothing to further orient
               
               We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
               
               StartTerms: basic terms
               Strategy: none
               
                 We fail transforming the problem using 'weightgap of dimension Nat 3, maximal degree 3, cbits 4'
                 
                   All strict components are empty, nothing to further orient
                 
                 We try instead 'weightgap of dimension Nat 4, maximal degree 3, cbits 4' on the problem
                 
                 StartTerms: basic terms
                 Strategy: none
                 
                   All strict components are empty, nothing to further orient
               
               We abort the transformation and continue with the subprocessor on the problem
               
               StartTerms: basic terms
               Strategy: none
               
               1) No dependency-pair could be removed
                  
                  We apply the transformation 'weightgap of dimension Nat 2, maximal degree 1, cbits 4 <> ...' on the resulting sub-problems:
                  Sub-problem 1:
                  --------------
                    We consider the problem
                    
                    StartTerms: basic terms
                    Strategy: none
                    
                    We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
                    
                      All strict components are empty, nothing to further orient
                    
                    We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
                    
                    StartTerms: basic terms
                    Strategy: none
                    
                      We fail transforming the problem using 'weightgap of dimension Nat 3, maximal degree 3, cbits 4'
                      
                        All strict components are empty, nothing to further orient
                      
                      We try instead 'weightgap of dimension Nat 4, maximal degree 3, cbits 4' on the problem
                      
                      StartTerms: basic terms
                      Strategy: none
                      
                        All strict components are empty, nothing to further orient
                  
                  We abort the transformation and continue with the subprocessor on the problem
                  
                  StartTerms: basic terms
                  Strategy: none
                  
                  1) 'Sequentially' proved the goal fastest:
                     
                     'empty' succeeded:
                     
                     Empty rules are trivially bounded
                  
               
            
      
      * Path {1,2}->{4}: YES(O(1),O(1))
        -------------------------------
        
        We consider the following Problem:
        
          Strict DPs: {*^#(1(), y) -> c_4(y)}
          Weak DPs:
            {  *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
             , *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))}
          StartTerms: basic terms
          Strategy: none
        
        Certificate: YES(O(1),O(1))
        
        Application of 'removetails >>> ... >>> ... >>> ...':
        -----------------------------------------------------
          We consider the the dependency-graph
          
            1: *^#(1(), y) -> c_4(y)
            
            2: *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
                 --> *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z)): 3
                 --> *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z)): 2
                 --> *^#(1(), y) -> c_4(y): 1
            
            3: *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))
                 --> *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z)): 3
                 --> *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z)): 2
                 --> *^#(1(), y) -> c_4(y): 1
            
          
          together with the congruence-graph
          
            ->{2,3}                                                     Weak SCC
               |
               `->{1}                                                   Noncyclic, trivial, SCC
            
            
            Here rules are as follows:
            
              {  1: *^#(1(), y) -> c_4(y)
               , 2: *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
               , 3: *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))}
          
          The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
          
            {  2: *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
             , 3: *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))
             , 1: *^#(1(), y) -> c_4(y)}
          
          We consider the following Problem:
          
            StartTerms: basic terms
            Strategy: none
          
          Certificate: YES(O(1),O(1))
          
          Application of 'simpDPRHS >>> ...':
          -----------------------------------
            No rule was simplified
            
            We apply the transformation 'usablerules' on the resulting sub-problems:
            Sub-problem 1:
            --------------
              We consider the problem
              
              StartTerms: basic terms
              Strategy: none
              
              The input problem is not a DP-problem.
            
            We abort the transformation and continue with the subprocessor on the problem
            
            StartTerms: basic terms
            Strategy: none
            
            1) We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
               
                 All strict components are empty, nothing to further orient
               
               We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
               
               StartTerms: basic terms
               Strategy: none
               
                 We fail transforming the problem using 'weightgap of dimension Nat 3, maximal degree 3, cbits 4'
                 
                   All strict components are empty, nothing to further orient
                 
                 We try instead 'weightgap of dimension Nat 4, maximal degree 3, cbits 4' on the problem
                 
                 StartTerms: basic terms
                 Strategy: none
                 
                   All strict components are empty, nothing to further orient
               
               We abort the transformation and continue with the subprocessor on the problem
               
               StartTerms: basic terms
               Strategy: none
               
               1) No dependency-pair could be removed
                  
                  We apply the transformation 'weightgap of dimension Nat 2, maximal degree 1, cbits 4 <> ...' on the resulting sub-problems:
                  Sub-problem 1:
                  --------------
                    We consider the problem
                    
                    StartTerms: basic terms
                    Strategy: none
                    
                    We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
                    
                      All strict components are empty, nothing to further orient
                    
                    We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
                    
                    StartTerms: basic terms
                    Strategy: none
                    
                      We fail transforming the problem using 'weightgap of dimension Nat 3, maximal degree 3, cbits 4'
                      
                        All strict components are empty, nothing to further orient
                      
                      We try instead 'weightgap of dimension Nat 4, maximal degree 3, cbits 4' on the problem
                      
                      StartTerms: basic terms
                      Strategy: none
                      
                        All strict components are empty, nothing to further orient
                  
                  We abort the transformation and continue with the subprocessor on the problem
                  
                  StartTerms: basic terms
                  Strategy: none
                  
                  1) 'Sequentially' proved the goal fastest:
                     
                     'empty' succeeded:
                     
                     Empty rules are trivially bounded
                  
               
            

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

Tool tup3irc

Execution Time51.090866ms
Answer
MAYBE
InputSK90 4.05

stdout:

MAYBE

We consider the following Problem:

  Strict Trs:
    {  *(x, +(y, z)) -> +(*(x, y), *(x, z))
     , *(+(x, y), z) -> +(*(x, z), *(y, z))
     , *(x, 1()) -> x
     , *(1(), y) -> y}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Application of 'tup3 (timeout of 60.0 seconds)':
------------------------------------------------
  The input problem contains no overlaps that give rise to inapplicable rules.
  
  We abort the transformation and continue with the subprocessor on the problem
  
  Strict Trs:
    {  *(x, +(y, z)) -> +(*(x, y), *(x, z))
     , *(+(x, y), z) -> +(*(x, z), *(y, z))
     , *(x, 1()) -> x
     , *(1(), y) -> y}
  StartTerms: basic terms
  Strategy: innermost
  
  1) None of the processors succeeded.
     
     Details of failed attempt(s):
     -----------------------------
       1) 'dp' failed due to the following reason:
            We have computed the following dependency pairs
            
            Strict Dependency Pairs:
              {  *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
               , *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))
               , *^#(x, 1()) -> c_3()
               , *^#(1(), y) -> c_4()}
            
            We consider the following Problem:
            
              Strict DPs:
                {  *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
                 , *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))
                 , *^#(x, 1()) -> c_3()
                 , *^#(1(), y) -> c_4()}
              Weak Trs:
                {  *(x, +(y, z)) -> +(*(x, y), *(x, z))
                 , *(+(x, y), z) -> +(*(x, z), *(y, z))
                 , *(x, 1()) -> x
                 , *(1(), y) -> y}
              StartTerms: basic terms
              Strategy: innermost
            
            Certificate: MAYBE
            
            Application of 'Fastest':
            -------------------------
              None of the processors succeeded.
              
              Details of failed attempt(s):
              -----------------------------
                1) 'compose (statically using 'split all congruence from CWD except leafs', multiplication)' failed due to the following reason:
                     Compose is inapplicable since some weak rule is size increasing
                     
                     We abort the transformation and continue with the subprocessor on the problem
                     
                     Strict DPs:
                       {  *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
                        , *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))
                        , *^#(x, 1()) -> c_3()
                        , *^#(1(), y) -> c_4()}
                     Weak Trs:
                       {  *(x, +(y, z)) -> +(*(x, y), *(x, z))
                        , *(+(x, y), z) -> +(*(x, z), *(y, z))
                        , *(x, 1()) -> x
                        , *(1(), y) -> y}
                     StartTerms: basic terms
                     Strategy: innermost
                     
                     1) We consider the the dependency-graph
                        
                          1: *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
                               --> *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z)): 2
                               --> *^#(1(), y) -> c_4(): 4
                               --> *^#(x, 1()) -> c_3(): 3
                               --> *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z)): 1
                          
                          2: *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))
                               --> *^#(1(), y) -> c_4(): 4
                               --> *^#(x, 1()) -> c_3(): 3
                               --> *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z)): 2
                               --> *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z)): 1
                          
                          3: *^#(x, 1()) -> c_3()
                          
                          4: *^#(1(), y) -> c_4()
                          
                        
                        together with the congruence-graph
                        
                          ->{1,2}
                             |
                             |->{3}                                                   Noncyclic, trivial, SCC
                             |
                             `->{4}                                                   Noncyclic, trivial, SCC
                          
                          
                          Here rules are as follows:
                          
                            {  1: *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
                             , 2: *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))
                             , 3: *^#(x, 1()) -> c_3()
                             , 4: *^#(1(), y) -> c_4()}
                        
                        The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
                        
                          {  3: *^#(x, 1()) -> c_3()
                           , 4: *^#(1(), y) -> c_4()}
                        
                        We consider the following Problem:
                        
                          Strict DPs:
                            {  *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
                             , *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))}
                          Weak Trs:
                            {  *(x, +(y, z)) -> +(*(x, y), *(x, z))
                             , *(+(x, y), z) -> +(*(x, z), *(y, z))
                             , *(x, 1()) -> x
                             , *(1(), y) -> y}
                          StartTerms: basic terms
                          Strategy: innermost
                        
                        Certificate: MAYBE
                        
                        Application of 'simpDPRHS >>> ...':
                        -----------------------------------
                          No rule was simplified
                          
                          We abort the transformation and continue with the subprocessor on the problem
                          
                          Strict DPs:
                            {  *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
                             , *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))}
                          Weak Trs:
                            {  *(x, +(y, z)) -> +(*(x, y), *(x, z))
                             , *(+(x, y), z) -> +(*(x, z), *(y, z))
                             , *(x, 1()) -> x
                             , *(1(), y) -> y}
                          StartTerms: basic terms
                          Strategy: innermost
                          
                          1) No rule is usable.
                             
                             We consider the following Problem:
                             
                               Strict DPs:
                                 {  *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
                                  , *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))}
                               StartTerms: basic terms
                               Strategy: innermost
                             
                             Certificate: MAYBE
                             
                             Application of 'weightgap of dimension Nat 2, maximal degree 1, cbits 4 <> ...':
                             --------------------------------------------------------------------------------
                               We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
                               
                                 The weightgap principle does not apply
                               
                               We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
                               
                               Strict DPs:
                                 {  *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
                                  , *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))}
                               StartTerms: basic terms
                               Strategy: innermost
                               
                                 We fail transforming the problem using 'weightgap of dimension Nat 3, maximal degree 3, cbits 4'
                                 
                                   The weightgap principle does not apply
                                 
                                 We try instead 'weightgap of dimension Nat 4, maximal degree 3, cbits 4' on the problem
                                 
                                 Strict DPs:
                                   {  *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
                                    , *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))}
                                 StartTerms: basic terms
                                 Strategy: innermost
                                 
                                   The weightgap principle does not apply
                               
                               We abort the transformation and continue with the subprocessor on the problem
                               
                               Strict DPs:
                                 {  *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
                                  , *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))}
                               StartTerms: basic terms
                               Strategy: innermost
                               
                               1) No dependency-pair could be removed
                                  
                                  We apply the transformation 'weightgap of dimension Nat 2, maximal degree 1, cbits 4 <> ...' on the resulting sub-problems:
                                  Sub-problem 1:
                                  --------------
                                    We consider the problem
                                    
                                    Strict DPs:
                                      {  *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
                                       , *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))}
                                    StartTerms: basic terms
                                    Strategy: innermost
                                    
                                    We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
                                    
                                      The weightgap principle does not apply
                                    
                                    We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
                                    
                                    Strict DPs:
                                      {  *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
                                       , *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))}
                                    StartTerms: basic terms
                                    Strategy: innermost
                                    
                                      We fail transforming the problem using 'weightgap of dimension Nat 3, maximal degree 3, cbits 4'
                                      
                                        The weightgap principle does not apply
                                      
                                      We try instead 'weightgap of dimension Nat 4, maximal degree 3, cbits 4' on the problem
                                      
                                      Strict DPs:
                                        {  *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
                                         , *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))}
                                      StartTerms: basic terms
                                      Strategy: innermost
                                      
                                        The weightgap principle does not apply
                                  
                                  We abort the transformation and continue with the subprocessor on the problem
                                  
                                  Strict DPs:
                                    {  *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
                                     , *^#(+(x, y), z) -> c_2(*^#(x, z), *^#(y, z))}
                                  StartTerms: basic terms
                                  Strategy: innermost
                                  
                                  1) None of the processors succeeded.
                                     
                                     Details of failed attempt(s):
                                     -----------------------------
                                       1) 'empty' failed due to the following reason:
                                            Empty strict component of the problem is NOT empty.
                                       
                                       2) 'Fastest' failed due to the following reason:
                                            None of the processors succeeded.
                                            
                                            Details of failed attempt(s):
                                            -----------------------------
                                              1) 'matrix-interpretation of dimension 4 (timeout of 100.0 seconds)' failed due to the following reason:
                                                   The input cannot be shown compatible
                                              
                                              2) 'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' failed due to the following reason:
                                                   The input cannot be shown compatible
                                              
                                              3) 'matrix-interpretation of dimension 2 (timeout of 100.0 seconds)' failed due to the following reason:
                                                   The input cannot be shown compatible
                                              
                                       
                                  
                               
                          
                     
                
                2) 'Sequentially' failed due to the following reason:
                     None of the processors succeeded.
                     
                     Details of failed attempt(s):
                     -----------------------------
                       1) 'empty' failed due to the following reason:
                            Empty strict component of the problem is NOT empty.
                       
                       2) 'Fastest' failed due to the following reason:
                            None of the processors succeeded.
                            
                            Details of failed attempt(s):
                            -----------------------------
                              1) 'matrix-interpretation of dimension 4 (timeout of 100.0 seconds)' failed due to the following reason:
                                   The input cannot be shown compatible
                              
                              2) 'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' failed due to the following reason:
                                   The input cannot be shown compatible
                              
                              3) 'matrix-interpretation of dimension 2 (timeout of 100.0 seconds)' failed due to the following reason:
                                   The input cannot be shown compatible
                              
                       
                
       
       2) 'Fastest' failed due to the following reason:
            None of the processors succeeded.
            
            Details of failed attempt(s):
            -----------------------------
              1) 'Sequentially' failed due to the following reason:
                   None of the processors succeeded.
                   
                   Details of failed attempt(s):
                   -----------------------------
                     1) 'empty' failed due to the following reason:
                          Empty strict component of the problem is NOT empty.
                     
                     2) 'Fastest' failed due to the following reason:
                          None of the processors succeeded.
                          
                          Details of failed attempt(s):
                          -----------------------------
                            1) 'matrix-interpretation of dimension 4 (timeout of 100.0 seconds)' failed due to the following reason:
                                 The input cannot be shown compatible
                            
                            2) 'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' failed due to the following reason:
                                 The input cannot be shown compatible
                            
                            3) 'matrix-interpretation of dimension 2 (timeout of 100.0 seconds)' failed due to the following reason:
                                 The input cannot be shown compatible
                            
                     
              
              2) 'Fastest' failed due to the following reason:
                   None of the processors succeeded.
                   
                   Details of failed attempt(s):
                   -----------------------------
                     1) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason:
                          match-boundness of the problem could not be verified.
                     
                     2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason:
                          match-boundness of the problem could not be verified.
                     
              
       
  

Arrrr..