MAYBE
454.72/185.64	MAYBE
454.72/185.64	
454.72/185.64	We are left with following problem, upon which TcT provides the
454.72/185.64	certificate MAYBE.
454.72/185.64	
454.72/185.64	Strict Trs:
454.72/185.64	  { g(Cons(x, xs), y) -> Cons(x, xs)
454.72/185.64	  , g(Nil(), y) -> h(Nil(), y)
454.72/185.64	  , h(Cons(x, xs), y) -> f(Cons(x, xs), y)
454.72/185.64	  , h(Nil(), y) -> h(Nil(), y)
454.72/185.64	  , f(Cons(x, xs), y) -> h(Cons(x, xs), y)
454.72/185.64	  , f(Nil(), y) -> g(Nil(), y)
454.72/185.64	  , sp1(x, y) -> f(x, y)
454.72/185.64	  , r(x, y) -> x }
454.72/185.64	Obligation:
454.72/185.64	  innermost runtime complexity
454.72/185.64	Answer:
454.72/185.64	  MAYBE
454.72/185.64	
454.72/185.64	None of the processors succeeded.
454.72/185.64	
454.72/185.64	Details of failed attempt(s):
454.72/185.64	-----------------------------
454.72/185.64	1) 'empty' failed due to the following reason:
454.72/185.64	   
454.72/185.64	   Empty strict component of the problem is NOT empty.
454.72/185.64	
454.72/185.64	2) 'Best' failed due to the following reason:
454.72/185.64	   
454.72/185.64	   None of the processors succeeded.
454.72/185.64	   
454.72/185.64	   Details of failed attempt(s):
454.72/185.64	   -----------------------------
454.72/185.64	   1) 'With Problem ... (timeout of 297 seconds)' failed due to the
454.72/185.64	      following reason:
454.72/185.64	      
454.72/185.64	      We add the following weak dependency pairs:
454.72/185.64	      
454.72/185.64	      Strict DPs:
454.72/185.64	        { g^#(Cons(x, xs), y) -> c_1()
454.72/185.64	        , g^#(Nil(), y) -> c_2(h^#(Nil(), y))
454.72/185.64	        , h^#(Cons(x, xs), y) -> c_3(f^#(Cons(x, xs), y))
454.72/185.64	        , h^#(Nil(), y) -> c_4(h^#(Nil(), y))
454.72/185.64	        , f^#(Cons(x, xs), y) -> c_5(h^#(Cons(x, xs), y))
454.72/185.64	        , f^#(Nil(), y) -> c_6(g^#(Nil(), y))
454.72/185.64	        , sp1^#(x, y) -> c_7(f^#(x, y))
454.72/185.64	        , r^#(x, y) -> c_8() }
454.72/185.64	      
454.72/185.64	      and mark the set of starting terms.
454.72/185.64	      
454.72/185.64	      We are left with following problem, upon which TcT provides the
454.72/185.64	      certificate MAYBE.
454.72/185.64	      
454.72/185.64	      Strict DPs:
454.72/185.64	        { g^#(Cons(x, xs), y) -> c_1()
454.72/185.64	        , g^#(Nil(), y) -> c_2(h^#(Nil(), y))
454.72/185.64	        , h^#(Cons(x, xs), y) -> c_3(f^#(Cons(x, xs), y))
454.72/185.64	        , h^#(Nil(), y) -> c_4(h^#(Nil(), y))
454.72/185.64	        , f^#(Cons(x, xs), y) -> c_5(h^#(Cons(x, xs), y))
454.72/185.64	        , f^#(Nil(), y) -> c_6(g^#(Nil(), y))
454.72/185.64	        , sp1^#(x, y) -> c_7(f^#(x, y))
454.72/185.64	        , r^#(x, y) -> c_8() }
454.72/185.64	      Strict Trs:
454.72/185.64	        { g(Cons(x, xs), y) -> Cons(x, xs)
454.72/185.64	        , g(Nil(), y) -> h(Nil(), y)
454.72/185.64	        , h(Cons(x, xs), y) -> f(Cons(x, xs), y)
454.72/185.64	        , h(Nil(), y) -> h(Nil(), y)
454.72/185.64	        , f(Cons(x, xs), y) -> h(Cons(x, xs), y)
454.72/185.64	        , f(Nil(), y) -> g(Nil(), y)
454.72/185.64	        , sp1(x, y) -> f(x, y)
454.72/185.64	        , r(x, y) -> x }
454.72/185.64	      Obligation:
454.72/185.64	        innermost runtime complexity
454.72/185.64	      Answer:
454.72/185.64	        MAYBE
454.72/185.64	      
454.72/185.64	      No rule is usable, rules are removed from the input problem.
454.72/185.64	      
454.72/185.64	      We are left with following problem, upon which TcT provides the
454.72/185.64	      certificate MAYBE.
454.72/185.64	      
454.72/185.64	      Strict DPs:
454.72/185.64	        { g^#(Cons(x, xs), y) -> c_1()
454.72/185.64	        , g^#(Nil(), y) -> c_2(h^#(Nil(), y))
454.72/185.64	        , h^#(Cons(x, xs), y) -> c_3(f^#(Cons(x, xs), y))
454.72/185.64	        , h^#(Nil(), y) -> c_4(h^#(Nil(), y))
454.72/185.64	        , f^#(Cons(x, xs), y) -> c_5(h^#(Cons(x, xs), y))
454.72/185.64	        , f^#(Nil(), y) -> c_6(g^#(Nil(), y))
454.72/185.64	        , sp1^#(x, y) -> c_7(f^#(x, y))
454.72/185.64	        , r^#(x, y) -> c_8() }
454.72/185.64	      Obligation:
454.72/185.64	        innermost runtime complexity
454.72/185.64	      Answer:
454.72/185.64	        MAYBE
454.72/185.64	      
454.72/185.64	      The weightgap principle applies (using the following constant
454.72/185.64	      growth matrix-interpretation)
454.72/185.64	      
454.72/185.64	      The following argument positions are usable:
454.72/185.64	        Uargs(c_2) = {1}, Uargs(c_3) = {1}, Uargs(c_4) = {1},
454.72/185.64	        Uargs(c_5) = {1}, Uargs(c_6) = {1}, Uargs(c_7) = {1}
454.72/185.64	      
454.72/185.64	      TcT has computed the following constructor-restricted matrix
454.72/185.64	      interpretation.
454.72/185.64	      
454.72/185.64	         [Cons](x1, x2) = [1 0] x1 + [1 0] x2 + [0]
454.72/185.64	                          [0 0]      [0 0]      [0]
454.72/185.64	                                                   
454.72/185.64	                  [Nil] = [0]                      
454.72/185.64	                          [0]                      
454.72/185.64	                                                   
454.72/185.64	          [g^#](x1, x2) = [2 2] x2 + [0]           
454.72/185.64	                          [2 2]      [0]           
454.72/185.64	                                                   
454.72/185.64	                  [c_1] = [2]                      
454.72/185.64	                          [0]                      
454.72/185.64	                                                   
454.72/185.64	              [c_2](x1) = [1 0] x1 + [2]           
454.72/185.64	                          [0 1]      [2]           
454.72/185.64	                                                   
454.72/185.64	          [h^#](x1, x2) = [2 2] x2 + [0]           
454.72/185.64	                          [1 1]      [0]           
454.72/185.64	                                                   
454.72/185.64	              [c_3](x1) = [1 0] x1 + [2]           
454.72/185.64	                          [0 1]      [2]           
454.72/185.64	                                                   
454.72/185.64	          [f^#](x1, x2) = [2 2] x2 + [0]           
454.72/185.64	                          [2 2]      [0]           
454.72/185.64	                                                   
454.72/185.64	              [c_4](x1) = [1 0] x1 + [2]           
454.72/185.64	                          [0 1]      [2]           
454.72/185.64	                                                   
454.72/185.64	              [c_5](x1) = [1 0] x1 + [2]           
454.72/185.64	                          [0 1]      [2]           
454.72/185.64	                                                   
454.72/185.64	              [c_6](x1) = [1 0] x1 + [2]           
454.72/185.64	                          [0 1]      [2]           
454.72/185.64	                                                   
454.72/185.64	        [sp1^#](x1, x2) = [1 1] x1 + [2 2] x2 + [1]
454.72/185.64	                          [2 1]      [1 2]      [1]
454.72/185.64	                                                   
454.72/185.64	              [c_7](x1) = [1 0] x1 + [2]           
454.72/185.64	                          [0 1]      [2]           
454.72/185.64	                                                   
454.72/185.64	          [r^#](x1, x2) = [2]                      
454.72/185.64	                          [1]                      
454.72/185.64	                                                   
454.72/185.64	                  [c_8] = [1]                      
454.72/185.64	                          [1]                      
454.72/185.64	      
454.72/185.64	      The order satisfies the following ordering constraints:
454.72/185.64	      
454.72/185.64	        [g^#(Cons(x, xs), y)] = [2 2] y + [0]             
454.72/185.64	                                [2 2]     [0]             
454.72/185.64	                              ? [2]                       
454.72/185.64	                                [0]                       
454.72/185.64	                              = [c_1()]                   
454.72/185.64	                                                          
454.72/185.64	              [g^#(Nil(), y)] = [2 2] y + [0]             
454.72/185.64	                                [2 2]     [0]             
454.72/185.64	                              ? [2 2] y + [2]             
454.72/185.64	                                [1 1]     [2]             
454.72/185.64	                              = [c_2(h^#(Nil(), y))]      
454.72/185.64	                                                          
454.72/185.64	        [h^#(Cons(x, xs), y)] = [2 2] y + [0]             
454.72/185.64	                                [1 1]     [0]             
454.72/185.64	                              ? [2 2] y + [2]             
454.72/185.64	                                [2 2]     [2]             
454.72/185.64	                              = [c_3(f^#(Cons(x, xs), y))]
454.72/185.64	                                                          
454.72/185.64	              [h^#(Nil(), y)] = [2 2] y + [0]             
454.72/185.64	                                [1 1]     [0]             
454.72/185.64	                              ? [2 2] y + [2]             
454.72/185.64	                                [1 1]     [2]             
454.72/185.64	                              = [c_4(h^#(Nil(), y))]      
454.72/185.64	                                                          
454.72/185.64	        [f^#(Cons(x, xs), y)] = [2 2] y + [0]             
454.72/185.64	                                [2 2]     [0]             
454.72/185.64	                              ? [2 2] y + [2]             
454.72/185.64	                                [1 1]     [2]             
454.72/185.64	                              = [c_5(h^#(Cons(x, xs), y))]
454.72/185.64	                                                          
454.72/185.64	              [f^#(Nil(), y)] = [2 2] y + [0]             
454.72/185.64	                                [2 2]     [0]             
454.72/185.64	                              ? [2 2] y + [2]             
454.72/185.64	                                [2 2]     [2]             
454.72/185.64	                              = [c_6(g^#(Nil(), y))]      
454.72/185.64	                                                          
454.72/185.64	                [sp1^#(x, y)] = [1 1] x + [2 2] y + [1]   
454.72/185.64	                                [2 1]     [1 2]     [1]   
454.72/185.64	                              ? [2 2] y + [2]             
454.72/185.64	                                [2 2]     [2]             
454.72/185.64	                              = [c_7(f^#(x, y))]          
454.72/185.64	                                                          
454.72/185.65	                  [r^#(x, y)] = [2]                       
454.72/185.65	                                [1]                       
454.72/185.65	                              > [1]                       
454.72/185.65	                                [1]                       
454.72/185.65	                              = [c_8()]                   
454.72/185.65	                                                          
454.72/185.65	      
454.72/185.65	      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
454.72/185.65	      
454.72/185.65	      We are left with following problem, upon which TcT provides the
454.72/185.65	      certificate MAYBE.
454.72/185.65	      
454.72/185.65	      Strict DPs:
454.72/185.65	        { g^#(Cons(x, xs), y) -> c_1()
454.72/185.65	        , g^#(Nil(), y) -> c_2(h^#(Nil(), y))
454.72/185.65	        , h^#(Cons(x, xs), y) -> c_3(f^#(Cons(x, xs), y))
454.72/185.65	        , h^#(Nil(), y) -> c_4(h^#(Nil(), y))
454.72/185.65	        , f^#(Cons(x, xs), y) -> c_5(h^#(Cons(x, xs), y))
454.72/185.65	        , f^#(Nil(), y) -> c_6(g^#(Nil(), y))
454.72/185.65	        , sp1^#(x, y) -> c_7(f^#(x, y)) }
454.72/185.65	      Weak DPs: { r^#(x, y) -> c_8() }
454.72/185.65	      Obligation:
454.72/185.65	        innermost runtime complexity
454.72/185.65	      Answer:
454.72/185.65	        MAYBE
454.72/185.65	      
454.72/185.65	      We estimate the number of application of {1} by applications of
454.72/185.65	      Pre({1}) = {}. Here rules are labeled as follows:
454.72/185.65	      
454.72/185.65	        DPs:
454.72/185.65	          { 1: g^#(Cons(x, xs), y) -> c_1()
454.72/185.65	          , 2: g^#(Nil(), y) -> c_2(h^#(Nil(), y))
454.72/185.65	          , 3: h^#(Cons(x, xs), y) -> c_3(f^#(Cons(x, xs), y))
454.72/185.65	          , 4: h^#(Nil(), y) -> c_4(h^#(Nil(), y))
454.72/185.65	          , 5: f^#(Cons(x, xs), y) -> c_5(h^#(Cons(x, xs), y))
454.72/185.65	          , 6: f^#(Nil(), y) -> c_6(g^#(Nil(), y))
454.72/185.65	          , 7: sp1^#(x, y) -> c_7(f^#(x, y))
454.72/185.65	          , 8: r^#(x, y) -> c_8() }
454.72/185.65	      
454.72/185.65	      We are left with following problem, upon which TcT provides the
454.72/185.65	      certificate MAYBE.
454.72/185.65	      
454.72/185.65	      Strict DPs:
454.72/185.65	        { g^#(Nil(), y) -> c_2(h^#(Nil(), y))
454.72/185.65	        , h^#(Cons(x, xs), y) -> c_3(f^#(Cons(x, xs), y))
454.72/185.65	        , h^#(Nil(), y) -> c_4(h^#(Nil(), y))
454.72/185.65	        , f^#(Cons(x, xs), y) -> c_5(h^#(Cons(x, xs), y))
454.72/185.65	        , f^#(Nil(), y) -> c_6(g^#(Nil(), y))
454.72/185.65	        , sp1^#(x, y) -> c_7(f^#(x, y)) }
454.72/185.65	      Weak DPs:
454.72/185.65	        { g^#(Cons(x, xs), y) -> c_1()
454.72/185.65	        , r^#(x, y) -> c_8() }
454.72/185.65	      Obligation:
454.72/185.65	        innermost runtime complexity
454.72/185.65	      Answer:
454.72/185.65	        MAYBE
454.72/185.65	      
454.72/185.65	      The following weak DPs constitute a sub-graph of the DG that is
454.72/185.65	      closed under successors. The DPs are removed.
454.72/185.65	      
454.72/185.65	      { g^#(Cons(x, xs), y) -> c_1()
454.72/185.65	      , r^#(x, y) -> c_8() }
454.72/185.65	      
454.72/185.65	      We are left with following problem, upon which TcT provides the
454.72/185.65	      certificate MAYBE.
454.72/185.65	      
454.72/185.65	      Strict DPs:
454.72/185.65	        { g^#(Nil(), y) -> c_2(h^#(Nil(), y))
454.72/185.65	        , h^#(Cons(x, xs), y) -> c_3(f^#(Cons(x, xs), y))
454.72/185.65	        , h^#(Nil(), y) -> c_4(h^#(Nil(), y))
454.72/185.65	        , f^#(Cons(x, xs), y) -> c_5(h^#(Cons(x, xs), y))
454.72/185.65	        , f^#(Nil(), y) -> c_6(g^#(Nil(), y))
454.72/185.65	        , sp1^#(x, y) -> c_7(f^#(x, y)) }
454.72/185.65	      Obligation:
454.72/185.65	        innermost runtime complexity
454.72/185.65	      Answer:
454.72/185.65	        MAYBE
454.72/185.65	      
454.72/185.65	      Consider the dependency graph
454.72/185.65	      
454.72/185.65	        1: g^#(Nil(), y) -> c_2(h^#(Nil(), y))
454.72/185.65	           -->_1 h^#(Nil(), y) -> c_4(h^#(Nil(), y)) :3
454.72/185.65	        
454.72/185.65	        2: h^#(Cons(x, xs), y) -> c_3(f^#(Cons(x, xs), y))
454.72/185.65	           -->_1 f^#(Cons(x, xs), y) -> c_5(h^#(Cons(x, xs), y)) :4
454.72/185.65	        
454.72/185.65	        3: h^#(Nil(), y) -> c_4(h^#(Nil(), y))
454.72/185.65	           -->_1 h^#(Nil(), y) -> c_4(h^#(Nil(), y)) :3
454.72/185.65	        
454.72/185.65	        4: f^#(Cons(x, xs), y) -> c_5(h^#(Cons(x, xs), y))
454.72/185.65	           -->_1 h^#(Cons(x, xs), y) -> c_3(f^#(Cons(x, xs), y)) :2
454.72/185.65	        
454.72/185.65	        5: f^#(Nil(), y) -> c_6(g^#(Nil(), y))
454.72/185.65	           -->_1 g^#(Nil(), y) -> c_2(h^#(Nil(), y)) :1
454.72/185.65	        
454.72/185.65	        6: sp1^#(x, y) -> c_7(f^#(x, y))
454.72/185.65	           -->_1 f^#(Nil(), y) -> c_6(g^#(Nil(), y)) :5
454.72/185.65	           -->_1 f^#(Cons(x, xs), y) -> c_5(h^#(Cons(x, xs), y)) :4
454.72/185.65	        
454.72/185.65	      
454.72/185.65	      Following roots of the dependency graph are removed, as the
454.72/185.65	      considered set of starting terms is closed under reduction with
454.72/185.65	      respect to these rules (modulo compound contexts).
454.72/185.65	      
454.72/185.65	        { sp1^#(x, y) -> c_7(f^#(x, y)) }
454.72/185.65	      
454.72/185.65	      
454.72/185.65	      We are left with following problem, upon which TcT provides the
454.72/185.65	      certificate MAYBE.
454.72/185.65	      
454.72/185.65	      Strict DPs:
454.72/185.65	        { g^#(Nil(), y) -> c_2(h^#(Nil(), y))
454.72/185.65	        , h^#(Cons(x, xs), y) -> c_3(f^#(Cons(x, xs), y))
454.72/185.65	        , h^#(Nil(), y) -> c_4(h^#(Nil(), y))
454.72/185.65	        , f^#(Cons(x, xs), y) -> c_5(h^#(Cons(x, xs), y))
454.72/185.65	        , f^#(Nil(), y) -> c_6(g^#(Nil(), y)) }
454.72/185.65	      Obligation:
454.72/185.65	        innermost runtime complexity
454.72/185.65	      Answer:
454.72/185.65	        MAYBE
454.72/185.65	      
454.72/185.65	      Consider the dependency graph
454.72/185.65	      
454.72/185.65	        1: g^#(Nil(), y) -> c_2(h^#(Nil(), y))
454.72/185.65	           -->_1 h^#(Nil(), y) -> c_4(h^#(Nil(), y)) :3
454.72/185.65	        
454.72/185.65	        2: h^#(Cons(x, xs), y) -> c_3(f^#(Cons(x, xs), y))
454.72/185.65	           -->_1 f^#(Cons(x, xs), y) -> c_5(h^#(Cons(x, xs), y)) :4
454.72/185.65	        
454.72/185.65	        3: h^#(Nil(), y) -> c_4(h^#(Nil(), y))
454.72/185.65	           -->_1 h^#(Nil(), y) -> c_4(h^#(Nil(), y)) :3
454.72/185.65	        
454.72/185.65	        4: f^#(Cons(x, xs), y) -> c_5(h^#(Cons(x, xs), y))
454.72/185.65	           -->_1 h^#(Cons(x, xs), y) -> c_3(f^#(Cons(x, xs), y)) :2
454.72/185.65	        
454.72/185.65	        5: f^#(Nil(), y) -> c_6(g^#(Nil(), y))
454.72/185.65	           -->_1 g^#(Nil(), y) -> c_2(h^#(Nil(), y)) :1
454.72/185.65	        
454.72/185.65	      
454.72/185.65	      Following roots of the dependency graph are removed, as the
454.72/185.65	      considered set of starting terms is closed under reduction with
454.72/185.65	      respect to these rules (modulo compound contexts).
454.72/185.65	      
454.72/185.65	        { f^#(Nil(), y) -> c_6(g^#(Nil(), y)) }
454.72/185.65	      
454.72/185.65	      
454.72/185.65	      We are left with following problem, upon which TcT provides the
454.72/185.65	      certificate MAYBE.
454.72/185.65	      
454.72/185.65	      Strict DPs:
454.72/185.65	        { g^#(Nil(), y) -> c_2(h^#(Nil(), y))
454.72/185.65	        , h^#(Cons(x, xs), y) -> c_3(f^#(Cons(x, xs), y))
454.72/185.65	        , h^#(Nil(), y) -> c_4(h^#(Nil(), y))
454.72/185.65	        , f^#(Cons(x, xs), y) -> c_5(h^#(Cons(x, xs), y)) }
454.72/185.65	      Obligation:
454.72/185.65	        innermost runtime complexity
454.72/185.65	      Answer:
454.72/185.65	        MAYBE
454.72/185.65	      
454.72/185.65	      Consider the dependency graph
454.72/185.65	      
454.72/185.65	        1: g^#(Nil(), y) -> c_2(h^#(Nil(), y))
454.72/185.65	           -->_1 h^#(Nil(), y) -> c_4(h^#(Nil(), y)) :3
454.72/185.65	        
454.72/185.65	        2: h^#(Cons(x, xs), y) -> c_3(f^#(Cons(x, xs), y))
454.72/185.65	           -->_1 f^#(Cons(x, xs), y) -> c_5(h^#(Cons(x, xs), y)) :4
454.72/185.65	        
454.72/185.65	        3: h^#(Nil(), y) -> c_4(h^#(Nil(), y))
454.72/185.65	           -->_1 h^#(Nil(), y) -> c_4(h^#(Nil(), y)) :3
454.72/185.65	        
454.72/185.65	        4: f^#(Cons(x, xs), y) -> c_5(h^#(Cons(x, xs), y))
454.72/185.65	           -->_1 h^#(Cons(x, xs), y) -> c_3(f^#(Cons(x, xs), y)) :2
454.72/185.65	        
454.72/185.65	      
454.72/185.65	      Following roots of the dependency graph are removed, as the
454.72/185.65	      considered set of starting terms is closed under reduction with
454.72/185.65	      respect to these rules (modulo compound contexts).
454.72/185.65	      
454.72/185.65	        { g^#(Nil(), y) -> c_2(h^#(Nil(), y)) }
454.72/185.65	      
454.72/185.65	      
454.72/185.65	      We are left with following problem, upon which TcT provides the
454.72/185.65	      certificate MAYBE.
454.72/185.65	      
454.72/185.65	      Strict DPs:
454.72/185.65	        { h^#(Cons(x, xs), y) -> c_3(f^#(Cons(x, xs), y))
454.72/185.65	        , h^#(Nil(), y) -> c_4(h^#(Nil(), y))
454.72/185.65	        , f^#(Cons(x, xs), y) -> c_5(h^#(Cons(x, xs), y)) }
454.72/185.65	      Obligation:
454.72/185.65	        innermost runtime complexity
454.72/185.65	      Answer:
454.72/185.65	        MAYBE
454.72/185.65	      
454.72/185.65	      None of the processors succeeded.
454.72/185.65	      
454.72/185.65	      Details of failed attempt(s):
454.72/185.65	      -----------------------------
454.72/185.65	      1) 'empty' failed due to the following reason:
454.72/185.65	         
454.72/185.65	         Empty strict component of the problem is NOT empty.
454.72/185.65	      
454.72/185.65	      2) 'With Problem ...' failed due to the following reason:
454.72/185.65	         
454.72/185.65	         None of the processors succeeded.
454.72/185.65	         
454.72/185.65	         Details of failed attempt(s):
454.72/185.65	         -----------------------------
454.72/185.65	         1) 'empty' failed due to the following reason:
454.72/185.65	            
454.72/185.65	            Empty strict component of the problem is NOT empty.
454.72/185.65	         
454.72/185.65	         2) 'Fastest' failed due to the following reason:
454.72/185.65	            
454.72/185.65	            None of the processors succeeded.
454.72/185.65	            
454.72/185.65	            Details of failed attempt(s):
454.72/185.65	            -----------------------------
454.72/185.65	            1) 'With Problem ...' failed due to the following reason:
454.72/185.65	               
454.72/185.65	               None of the processors succeeded.
454.72/185.65	               
454.72/185.65	               Details of failed attempt(s):
454.72/185.65	               -----------------------------
454.72/185.65	               1) 'empty' failed due to the following reason:
454.72/185.65	                  
454.72/185.65	                  Empty strict component of the problem is NOT empty.
454.72/185.65	               
454.72/185.65	               2) 'Polynomial Path Order (PS)' failed due to the following reason:
454.72/185.65	                  
454.72/185.65	                  The input cannot be shown compatible
454.72/185.65	               
454.72/185.65	            
454.72/185.65	            2) 'Fastest (timeout of 24 seconds)' failed due to the following
454.72/185.65	               reason:
454.72/185.65	               
454.72/185.65	               Computation stopped due to timeout after 24.0 seconds.
454.72/185.65	            
454.72/185.65	            3) 'Polynomial Path Order (PS)' failed due to the following reason:
454.72/185.65	               
454.72/185.65	               The input cannot be shown compatible
454.72/185.65	            
454.72/185.65	         
454.72/185.65	      
454.72/185.65	   
454.72/185.65	   2) 'Best' failed due to the following reason:
454.72/185.65	      
454.72/185.65	      None of the processors succeeded.
454.72/185.65	      
454.72/185.65	      Details of failed attempt(s):
454.72/185.65	      -----------------------------
454.72/185.65	      1) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)'
454.72/185.65	         failed due to the following reason:
454.72/185.65	         
454.72/185.65	         Computation stopped due to timeout after 24.0 seconds.
454.72/185.65	      
454.72/185.65	      2) 'With Problem ... (timeout of 148 seconds) (timeout of 297
454.72/185.65	         seconds)' failed due to the following reason:
454.72/185.65	         
454.72/185.65	         We use the processor 'matrix interpretation of dimension 1' to
454.72/185.65	         orient following rules strictly.
454.72/185.65	         
454.72/185.65	         Trs:
454.72/185.65	           { sp1(x, y) -> f(x, y)
454.72/185.65	           , r(x, y) -> x }
454.72/185.65	         
454.72/185.65	         The induced complexity on above rules (modulo remaining rules) is
454.72/185.65	         YES(?,O(n^1)) . These rules are moved into the corresponding weak
454.72/185.65	         component(s).
454.72/185.65	         
454.72/185.65	         Sub-proof:
454.72/185.65	         ----------
454.72/185.65	           The following argument positions are usable:
454.72/185.65	             none
454.72/185.65	           
454.72/185.65	           TcT has computed the following constructor-based matrix
454.72/185.65	           interpretation satisfying not(EDA).
454.72/185.65	           
454.72/185.65	                [g](x1, x2) = [7] x2 + [0]         
454.72/185.65	                                                   
454.72/185.65	             [Cons](x1, x2) = [0]                  
454.72/185.65	                                                   
454.72/185.65	                [h](x1, x2) = [7] x2 + [0]         
454.72/185.65	                                                   
454.72/185.65	                      [Nil] = [0]                  
454.72/185.65	                                                   
454.72/185.65	                [f](x1, x2) = [7] x2 + [0]         
454.72/185.65	                                                   
454.72/185.65	              [sp1](x1, x2) = [7] x1 + [7] x2 + [7]
454.72/185.65	                                                   
454.72/185.65	                [r](x1, x2) = [7] x1 + [7] x2 + [7]
454.72/185.65	           
454.72/185.65	           The order satisfies the following ordering constraints:
454.72/185.65	           
454.72/185.65	             [g(Cons(x, xs), y)] =  [7] y + [0]        
454.72/185.65	                                 >= [0]                
454.72/185.65	                                 =  [Cons(x, xs)]      
454.72/185.65	                                                       
454.72/185.65	                   [g(Nil(), y)] =  [7] y + [0]        
454.72/185.65	                                 >= [7] y + [0]        
454.72/185.65	                                 =  [h(Nil(), y)]      
454.72/185.65	                                                       
454.72/185.65	             [h(Cons(x, xs), y)] =  [7] y + [0]        
454.72/185.65	                                 >= [7] y + [0]        
454.72/185.65	                                 =  [f(Cons(x, xs), y)]
454.72/185.65	                                                       
454.72/185.65	                   [h(Nil(), y)] =  [7] y + [0]        
454.72/185.65	                                 >= [7] y + [0]        
454.72/185.65	                                 =  [h(Nil(), y)]      
454.72/185.65	                                                       
454.72/185.65	             [f(Cons(x, xs), y)] =  [7] y + [0]        
454.72/185.65	                                 >= [7] y + [0]        
454.72/185.65	                                 =  [h(Cons(x, xs), y)]
454.72/185.65	                                                       
454.72/185.65	                   [f(Nil(), y)] =  [7] y + [0]        
454.72/185.65	                                 >= [7] y + [0]        
454.72/185.65	                                 =  [g(Nil(), y)]      
454.72/185.65	                                                       
454.72/185.65	                     [sp1(x, y)] =  [7] x + [7] y + [7]
454.72/185.65	                                 >  [7] y + [0]        
454.72/185.65	                                 =  [f(x, y)]          
454.72/185.65	                                                       
454.72/185.65	                       [r(x, y)] =  [7] x + [7] y + [7]
454.72/185.65	                                 >  [1] x + [0]        
454.72/185.65	                                 =  [x]                
454.72/185.65	                                                       
454.72/185.65	         
454.72/185.65	         We return to the main proof.
454.72/185.65	         
454.72/185.65	         We are left with following problem, upon which TcT provides the
454.72/185.65	         certificate MAYBE.
454.72/185.65	         
454.72/185.65	         Strict Trs:
454.72/185.65	           { g(Cons(x, xs), y) -> Cons(x, xs)
454.72/185.65	           , g(Nil(), y) -> h(Nil(), y)
454.72/185.65	           , h(Cons(x, xs), y) -> f(Cons(x, xs), y)
454.72/185.65	           , h(Nil(), y) -> h(Nil(), y)
454.72/185.65	           , f(Cons(x, xs), y) -> h(Cons(x, xs), y)
454.72/185.65	           , f(Nil(), y) -> g(Nil(), y) }
454.72/185.65	         Weak Trs:
454.72/185.65	           { sp1(x, y) -> f(x, y)
454.72/185.65	           , r(x, y) -> x }
454.72/185.65	         Obligation:
454.72/185.65	           innermost runtime complexity
454.72/185.65	         Answer:
454.72/185.65	           MAYBE
454.72/185.65	         
454.72/185.65	         The weightgap principle applies (using the following nonconstant
454.72/185.65	         growth matrix-interpretation)
454.72/185.65	         
454.72/185.65	         The following argument positions are usable:
454.72/185.65	           none
454.72/185.65	         
454.72/185.65	         TcT has computed the following matrix interpretation satisfying
454.72/185.65	         not(EDA) and not(IDA(1)).
454.72/185.65	         
454.72/185.65	              [g](x1, x2) = [1] x1 + [1] x2 + [0]
454.72/185.65	                                                 
454.72/185.65	           [Cons](x1, x2) = [1] x1 + [1] x2 + [0]
454.72/185.65	                                                 
454.72/185.65	              [h](x1, x2) = [1] x2 + [0]         
454.72/185.65	                                                 
454.72/185.65	                    [Nil] = [4]                  
454.72/185.65	                                                 
454.72/185.65	              [f](x1, x2) = [1] x2 + [0]         
454.72/185.65	                                                 
454.72/185.65	            [sp1](x1, x2) = [1] x1 + [1] x2 + [7]
454.72/185.65	                                                 
454.72/185.65	              [r](x1, x2) = [1] x1 + [1] x2 + [0]
454.72/185.65	         
454.72/185.65	         The order satisfies the following ordering constraints:
454.72/185.65	         
454.72/185.65	           [g(Cons(x, xs), y)] =  [1] x + [1] xs + [1] y + [0]
454.72/185.65	                               >= [1] x + [1] xs + [0]        
454.72/185.65	                               =  [Cons(x, xs)]               
454.72/185.65	                                                              
454.72/185.65	                 [g(Nil(), y)] =  [1] y + [4]                 
454.72/185.65	                               >  [1] y + [0]                 
454.72/185.65	                               =  [h(Nil(), y)]               
454.72/185.65	                                                              
454.72/185.65	           [h(Cons(x, xs), y)] =  [1] y + [0]                 
454.72/185.65	                               >= [1] y + [0]                 
454.72/185.65	                               =  [f(Cons(x, xs), y)]         
454.72/185.65	                                                              
454.72/185.65	                 [h(Nil(), y)] =  [1] y + [0]                 
454.72/185.65	                               >= [1] y + [0]                 
454.72/185.65	                               =  [h(Nil(), y)]               
454.72/185.65	                                                              
454.72/185.65	           [f(Cons(x, xs), y)] =  [1] y + [0]                 
454.72/185.65	                               >= [1] y + [0]                 
454.72/185.65	                               =  [h(Cons(x, xs), y)]         
454.72/185.65	                                                              
454.72/185.65	                 [f(Nil(), y)] =  [1] y + [0]                 
454.72/185.65	                               ?  [1] y + [4]                 
454.72/185.65	                               =  [g(Nil(), y)]               
454.72/185.65	                                                              
454.72/185.65	                   [sp1(x, y)] =  [1] x + [1] y + [7]         
454.72/185.65	                               >  [1] y + [0]                 
454.72/185.65	                               =  [f(x, y)]                   
454.72/185.65	                                                              
454.72/185.65	                     [r(x, y)] =  [1] x + [1] y + [0]         
454.72/185.65	                               >= [1] x + [0]                 
454.72/185.65	                               =  [x]                         
454.72/185.66	                                                              
454.72/185.66	         
454.72/185.66	         Further, it can be verified that all rules not oriented are covered by the weightgap condition.
454.72/185.66	         
454.72/185.66	         We are left with following problem, upon which TcT provides the
454.72/185.66	         certificate MAYBE.
454.72/185.66	         
454.72/185.66	         Strict Trs:
454.72/185.66	           { g(Cons(x, xs), y) -> Cons(x, xs)
454.72/185.66	           , h(Cons(x, xs), y) -> f(Cons(x, xs), y)
454.72/185.66	           , h(Nil(), y) -> h(Nil(), y)
454.72/185.66	           , f(Cons(x, xs), y) -> h(Cons(x, xs), y)
454.72/185.66	           , f(Nil(), y) -> g(Nil(), y) }
454.72/185.66	         Weak Trs:
454.72/185.66	           { g(Nil(), y) -> h(Nil(), y)
454.72/185.66	           , sp1(x, y) -> f(x, y)
454.72/185.66	           , r(x, y) -> x }
454.72/185.66	         Obligation:
454.72/185.66	           innermost runtime complexity
454.72/185.66	         Answer:
454.72/185.66	           MAYBE
454.72/185.66	         
454.72/185.66	         The weightgap principle applies (using the following nonconstant
454.72/185.66	         growth matrix-interpretation)
454.72/185.66	         
454.72/185.66	         The following argument positions are usable:
454.72/185.66	           none
454.72/185.66	         
454.72/185.66	         TcT has computed the following matrix interpretation satisfying
454.72/185.66	         not(EDA) and not(IDA(1)).
454.72/185.66	         
454.72/185.66	              [g](x1, x2) = [1] x1 + [1] x2 + [0]
454.72/185.66	                                                 
454.72/185.66	           [Cons](x1, x2) = [4]                  
454.72/185.66	                                                 
454.72/185.66	              [h](x1, x2) = [1] x2 + [0]         
454.72/185.66	                                                 
454.72/185.66	                    [Nil] = [4]                  
454.72/185.66	                                                 
454.72/185.66	              [f](x1, x2) = [1] x1 + [1] x2 + [0]
454.72/185.66	                                                 
454.72/185.66	            [sp1](x1, x2) = [1] x1 + [1] x2 + [7]
454.72/185.66	                                                 
454.72/185.66	              [r](x1, x2) = [1] x1 + [1] x2 + [0]
454.72/185.66	         
454.72/185.66	         The order satisfies the following ordering constraints:
454.72/185.66	         
454.72/185.66	           [g(Cons(x, xs), y)] =  [1] y + [4]        
454.72/185.66	                               >= [4]                
454.72/185.66	                               =  [Cons(x, xs)]      
454.72/185.66	                                                     
454.72/185.66	                 [g(Nil(), y)] =  [1] y + [4]        
454.72/185.66	                               >  [1] y + [0]        
454.72/185.66	                               =  [h(Nil(), y)]      
454.72/185.66	                                                     
454.72/185.66	           [h(Cons(x, xs), y)] =  [1] y + [0]        
454.72/185.66	                               ?  [1] y + [4]        
454.72/185.66	                               =  [f(Cons(x, xs), y)]
454.72/185.66	                                                     
454.72/185.66	                 [h(Nil(), y)] =  [1] y + [0]        
454.72/185.66	                               >= [1] y + [0]        
454.72/185.66	                               =  [h(Nil(), y)]      
454.72/185.66	                                                     
454.72/185.66	           [f(Cons(x, xs), y)] =  [1] y + [4]        
454.72/185.66	                               >  [1] y + [0]        
454.72/185.66	                               =  [h(Cons(x, xs), y)]
454.72/185.66	                                                     
454.72/185.66	                 [f(Nil(), y)] =  [1] y + [4]        
454.72/185.66	                               >= [1] y + [4]        
454.72/185.66	                               =  [g(Nil(), y)]      
454.72/185.66	                                                     
454.72/185.66	                   [sp1(x, y)] =  [1] x + [1] y + [7]
454.72/185.66	                               >  [1] x + [1] y + [0]
454.72/185.66	                               =  [f(x, y)]          
454.72/185.66	                                                     
454.72/185.66	                     [r(x, y)] =  [1] x + [1] y + [0]
454.72/185.66	                               >= [1] x + [0]        
454.72/185.66	                               =  [x]                
454.72/185.66	                                                     
454.72/185.66	         
454.72/185.66	         Further, it can be verified that all rules not oriented are covered by the weightgap condition.
454.72/185.66	         
454.72/185.66	         We are left with following problem, upon which TcT provides the
454.72/185.66	         certificate MAYBE.
454.72/185.66	         
454.72/185.66	         Strict Trs:
454.72/185.66	           { g(Cons(x, xs), y) -> Cons(x, xs)
454.72/185.66	           , h(Cons(x, xs), y) -> f(Cons(x, xs), y)
454.72/185.66	           , h(Nil(), y) -> h(Nil(), y)
454.72/185.66	           , f(Nil(), y) -> g(Nil(), y) }
454.72/185.66	         Weak Trs:
454.72/185.66	           { g(Nil(), y) -> h(Nil(), y)
454.72/185.66	           , f(Cons(x, xs), y) -> h(Cons(x, xs), y)
454.72/185.66	           , sp1(x, y) -> f(x, y)
454.72/185.66	           , r(x, y) -> x }
454.72/185.66	         Obligation:
454.72/185.66	           innermost runtime complexity
454.72/185.66	         Answer:
454.72/185.66	           MAYBE
454.72/185.66	         
454.72/185.66	         The weightgap principle applies (using the following nonconstant
454.72/185.66	         growth matrix-interpretation)
454.72/185.66	         
454.72/185.66	         The following argument positions are usable:
454.72/185.66	           none
454.72/185.66	         
454.72/185.66	         TcT has computed the following matrix interpretation satisfying
454.72/185.66	         not(EDA) and not(IDA(1)).
454.72/185.66	         
454.72/185.66	              [g](x1, x2) = [1] x2 + [0]         
454.72/185.66	                                                 
454.72/185.66	           [Cons](x1, x2) = [4]                  
454.72/185.66	                                                 
454.72/185.66	              [h](x1, x2) = [1] x2 + [0]         
454.72/185.66	                                                 
454.72/185.66	                    [Nil] = [4]                  
454.72/185.66	                                                 
454.72/185.66	              [f](x1, x2) = [1] x1 + [1] x2 + [0]
454.72/185.66	                                                 
454.72/185.66	            [sp1](x1, x2) = [1] x1 + [1] x2 + [7]
454.72/185.66	                                                 
454.72/185.66	              [r](x1, x2) = [1] x1 + [1] x2 + [0]
454.72/185.66	         
454.72/185.66	         The order satisfies the following ordering constraints:
454.72/185.66	         
454.72/185.66	           [g(Cons(x, xs), y)] =  [1] y + [0]        
454.72/185.66	                               ?  [4]                
454.72/185.66	                               =  [Cons(x, xs)]      
454.72/185.66	                                                     
454.72/185.66	                 [g(Nil(), y)] =  [1] y + [0]        
454.72/185.66	                               >= [1] y + [0]        
454.72/185.66	                               =  [h(Nil(), y)]      
454.72/185.66	                                                     
454.72/185.66	           [h(Cons(x, xs), y)] =  [1] y + [0]        
454.72/185.66	                               ?  [1] y + [4]        
454.72/185.66	                               =  [f(Cons(x, xs), y)]
454.72/185.66	                                                     
454.72/185.66	                 [h(Nil(), y)] =  [1] y + [0]        
454.72/185.66	                               >= [1] y + [0]        
454.72/185.66	                               =  [h(Nil(), y)]      
454.72/185.66	                                                     
454.72/185.66	           [f(Cons(x, xs), y)] =  [1] y + [4]        
454.72/185.66	                               >  [1] y + [0]        
454.72/185.66	                               =  [h(Cons(x, xs), y)]
454.72/185.66	                                                     
454.72/185.66	                 [f(Nil(), y)] =  [1] y + [4]        
454.72/185.66	                               >  [1] y + [0]        
454.72/185.66	                               =  [g(Nil(), y)]      
454.72/185.66	                                                     
454.72/185.66	                   [sp1(x, y)] =  [1] x + [1] y + [7]
454.72/185.66	                               >  [1] x + [1] y + [0]
454.72/185.66	                               =  [f(x, y)]          
454.72/185.66	                                                     
454.72/185.66	                     [r(x, y)] =  [1] x + [1] y + [0]
454.72/185.66	                               >= [1] x + [0]        
454.72/185.66	                               =  [x]                
454.72/185.66	                                                     
454.72/185.66	         
454.72/185.66	         Further, it can be verified that all rules not oriented are covered by the weightgap condition.
454.72/185.66	         
454.72/185.66	         We are left with following problem, upon which TcT provides the
454.72/185.66	         certificate MAYBE.
454.72/185.66	         
454.72/185.66	         Strict Trs:
454.72/185.66	           { g(Cons(x, xs), y) -> Cons(x, xs)
454.72/185.66	           , h(Cons(x, xs), y) -> f(Cons(x, xs), y)
454.72/185.66	           , h(Nil(), y) -> h(Nil(), y) }
454.72/185.66	         Weak Trs:
454.72/185.66	           { g(Nil(), y) -> h(Nil(), y)
454.72/185.66	           , f(Cons(x, xs), y) -> h(Cons(x, xs), y)
454.72/185.66	           , f(Nil(), y) -> g(Nil(), y)
454.72/185.66	           , sp1(x, y) -> f(x, y)
454.72/185.66	           , r(x, y) -> x }
454.72/185.66	         Obligation:
454.72/185.66	           innermost runtime complexity
454.72/185.66	         Answer:
454.72/185.66	           MAYBE
454.72/185.66	         
454.72/185.66	         The weightgap principle applies (using the following nonconstant
454.72/185.66	         growth matrix-interpretation)
454.72/185.66	         
454.72/185.66	         The following argument positions are usable:
454.72/185.66	           none
454.72/185.66	         
454.72/185.66	         TcT has computed the following matrix interpretation satisfying
454.72/185.66	         not(EDA) and not(IDA(1)).
454.72/185.66	         
454.72/185.66	              [g](x1, x2) = [1] x1 + [1] x2 + [4]
454.72/185.66	                                                 
454.72/185.66	           [Cons](x1, x2) = [4]                  
454.72/185.66	                                                 
454.72/185.66	              [h](x1, x2) = [1] x2 + [0]         
454.72/185.66	                                                 
454.72/185.66	                    [Nil] = [4]                  
454.72/185.66	                                                 
454.72/185.66	              [f](x1, x2) = [1] x1 + [1] x2 + [4]
454.72/185.66	                                                 
454.72/185.66	            [sp1](x1, x2) = [1] x1 + [1] x2 + [7]
454.72/185.66	                                                 
454.72/185.66	              [r](x1, x2) = [1] x1 + [1] x2 + [0]
454.72/185.66	         
454.72/185.66	         The order satisfies the following ordering constraints:
454.72/185.66	         
454.72/185.66	           [g(Cons(x, xs), y)] =  [1] y + [8]        
454.72/185.66	                               >  [4]                
454.72/185.66	                               =  [Cons(x, xs)]      
454.72/185.66	                                                     
454.72/185.66	                 [g(Nil(), y)] =  [1] y + [8]        
454.72/185.66	                               >  [1] y + [0]        
454.72/185.66	                               =  [h(Nil(), y)]      
454.72/185.66	                                                     
454.72/185.66	           [h(Cons(x, xs), y)] =  [1] y + [0]        
454.72/185.66	                               ?  [1] y + [8]        
454.72/185.66	                               =  [f(Cons(x, xs), y)]
454.72/185.66	                                                     
454.72/185.66	                 [h(Nil(), y)] =  [1] y + [0]        
454.72/185.66	                               >= [1] y + [0]        
454.72/185.66	                               =  [h(Nil(), y)]      
454.72/185.66	                                                     
454.72/185.66	           [f(Cons(x, xs), y)] =  [1] y + [8]        
454.72/185.66	                               >  [1] y + [0]        
454.72/185.66	                               =  [h(Cons(x, xs), y)]
454.72/185.66	                                                     
454.72/185.66	                 [f(Nil(), y)] =  [1] y + [8]        
454.72/185.66	                               >= [1] y + [8]        
454.72/185.66	                               =  [g(Nil(), y)]      
454.72/185.66	                                                     
454.72/185.66	                   [sp1(x, y)] =  [1] x + [1] y + [7]
454.72/185.66	                               >  [1] x + [1] y + [4]
454.72/185.66	                               =  [f(x, y)]          
454.72/185.66	                                                     
454.72/185.66	                     [r(x, y)] =  [1] x + [1] y + [0]
454.72/185.66	                               >= [1] x + [0]        
454.72/185.66	                               =  [x]                
454.72/185.66	                                                     
454.72/185.66	         
454.72/185.66	         Further, it can be verified that all rules not oriented are covered by the weightgap condition.
454.72/185.66	         
454.72/185.66	         We are left with following problem, upon which TcT provides the
454.72/185.66	         certificate MAYBE.
454.72/185.66	         
454.72/185.66	         Strict Trs:
454.72/185.66	           { h(Cons(x, xs), y) -> f(Cons(x, xs), y)
454.72/185.66	           , h(Nil(), y) -> h(Nil(), y) }
454.72/185.66	         Weak Trs:
454.72/185.66	           { g(Cons(x, xs), y) -> Cons(x, xs)
454.72/185.66	           , g(Nil(), y) -> h(Nil(), y)
454.72/185.66	           , f(Cons(x, xs), y) -> h(Cons(x, xs), y)
454.72/185.66	           , f(Nil(), y) -> g(Nil(), y)
454.72/185.66	           , sp1(x, y) -> f(x, y)
454.72/185.66	           , r(x, y) -> x }
454.72/185.66	         Obligation:
454.72/185.66	           innermost runtime complexity
454.72/185.66	         Answer:
454.72/185.66	           MAYBE
454.72/185.66	         
454.72/185.66	         None of the processors succeeded.
454.72/185.66	         
454.72/185.66	         Details of failed attempt(s):
454.72/185.66	         -----------------------------
454.72/185.66	         1) 'empty' failed due to the following reason:
454.72/185.66	            
454.72/185.66	            Empty strict component of the problem is NOT empty.
454.72/185.66	         
454.72/185.66	         2) 'With Problem ...' failed due to the following reason:
454.72/185.66	            
454.72/185.66	            None of the processors succeeded.
454.72/185.66	            
454.72/185.66	            Details of failed attempt(s):
454.72/185.66	            -----------------------------
454.72/185.66	            1) 'empty' failed due to the following reason:
454.72/185.66	               
454.72/185.66	               Empty strict component of the problem is NOT empty.
454.72/185.66	            
454.72/185.66	            2) 'Fastest' failed due to the following reason:
454.72/185.66	               
454.72/185.66	               None of the processors succeeded.
454.72/185.66	               
454.72/185.66	               Details of failed attempt(s):
454.72/185.66	               -----------------------------
454.72/185.66	               1) 'With Problem ...' failed due to the following reason:
454.72/185.66	                  
454.72/185.66	                  None of the processors succeeded.
454.72/185.66	                  
454.72/185.66	                  Details of failed attempt(s):
454.72/185.66	                  -----------------------------
454.72/185.66	                  1) 'empty' failed due to the following reason:
454.72/185.66	                     
454.72/185.66	                     Empty strict component of the problem is NOT empty.
454.72/185.66	                  
454.72/185.66	                  2) 'With Problem ...' failed due to the following reason:
454.72/185.66	                     
454.72/185.66	                     None of the processors succeeded.
454.72/185.66	                     
454.72/185.66	                     Details of failed attempt(s):
454.72/185.66	                     -----------------------------
454.72/185.66	                     1) 'empty' failed due to the following reason:
454.72/185.66	                        
454.72/185.66	                        Empty strict component of the problem is NOT empty.
454.72/185.66	                     
454.72/185.66	                     2) 'With Problem ...' failed due to the following reason:
454.72/185.66	                        
454.72/185.66	                        None of the processors succeeded.
454.72/185.66	                        
454.72/185.66	                        Details of failed attempt(s):
454.72/185.66	                        -----------------------------
454.72/185.66	                        1) 'empty' failed due to the following reason:
454.72/185.66	                           
454.72/185.66	                           Empty strict component of the problem is NOT empty.
454.72/185.66	                        
454.72/185.66	                        2) 'With Problem ...' failed due to the following reason:
454.72/185.66	                           
454.72/185.66	                           Empty strict component of the problem is NOT empty.
454.72/185.66	                        
454.72/185.66	                     
454.72/185.66	                  
454.72/185.66	               
454.72/185.66	               2) 'With Problem ...' failed due to the following reason:
454.72/185.66	                  
454.72/185.66	                  None of the processors succeeded.
454.72/185.66	                  
454.72/185.66	                  Details of failed attempt(s):
454.72/185.66	                  -----------------------------
454.72/185.66	                  1) 'empty' failed due to the following reason:
454.72/185.66	                     
454.72/185.66	                     Empty strict component of the problem is NOT empty.
454.72/185.66	                  
454.72/185.66	                  2) 'With Problem ...' failed due to the following reason:
454.72/185.66	                     
454.72/185.66	                     Empty strict component of the problem is NOT empty.
454.72/185.66	                  
454.72/185.66	               
454.72/185.66	            
454.72/185.66	         
454.72/185.66	      
454.72/185.66	      3) 'Best' failed due to the following reason:
454.72/185.66	         
454.72/185.66	         None of the processors succeeded.
454.72/185.66	         
454.72/185.66	         Details of failed attempt(s):
454.72/185.66	         -----------------------------
454.72/185.66	         1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the
454.72/185.66	            following reason:
454.72/185.66	            
454.72/185.66	            The input cannot be shown compatible
454.72/185.66	         
454.72/185.66	         2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due
454.72/185.66	            to the following reason:
454.72/185.66	            
454.72/185.66	            The input cannot be shown compatible
454.72/185.66	         
454.72/185.66	      
454.72/185.66	   
454.72/185.66	
454.72/185.66	
454.72/185.66	Arrrr..
454.98/185.89	EOF