Problem SK90 2.48

Tool CaT

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

stdout:

YES(?,O(n^1))

Problem:
 d(x) -> e(u(x))
 d(u(x)) -> c(x)
 c(u(x)) -> b(x)
 v(e(x)) -> x
 b(u(x)) -> a(e(x))

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {7,6,5,4}
   transitions:
    a1(47) -> 48*
    e1(54) -> 55*
    e1(9) -> 10*
    e1(56) -> 57*
    e1(46) -> 47*
    b1(40) -> 41*
    b1(42) -> 43*
    b1(34) -> 35*
    c1(32) -> 33*
    c1(24) -> 25*
    c1(26) -> 27*
    u1(16) -> 17*
    u1(18) -> 19*
    u1(8) -> 9*
    d0(2) -> 4*
    d0(1) -> 4*
    d0(3) -> 4*
    e0(2) -> 1*
    e0(1) -> 1*
    e0(3) -> 1*
    u0(2) -> 2*
    u0(1) -> 2*
    u0(3) -> 2*
    c0(2) -> 5*
    c0(1) -> 5*
    c0(3) -> 5*
    b0(2) -> 7*
    b0(1) -> 7*
    b0(3) -> 7*
    v0(2) -> 6*
    v0(1) -> 6*
    v0(3) -> 6*
    a0(2) -> 3*
    a0(1) -> 3*
    a0(3) -> 3*
    1 -> 54,6,40,26,16
    2 -> 46,6,34,24,18
    3 -> 56,6,42,32,8
    10 -> 4*
    17 -> 9*
    19 -> 9*
    25 -> 4*
    27 -> 4*
    33 -> 4*
    35 -> 25,4,5
    41 -> 25,4,5
    43 -> 25,4,5
    48 -> 35,5,7
    55 -> 47*
    57 -> 47*
  problem:
   
  Qed

Tool IRC1

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

stdout:

YES(?,O(n^1))

Tool IRC2

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

stdout:

YES(?,O(n^1))

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           YES(?,O(n^1))
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  d(x) -> e(u(x))
     , d(u(x)) -> c(x)
     , c(u(x)) -> b(x)
     , v(e(x)) -> x
     , b(u(x)) -> a(e(x))}

Proof Output:    
  'Bounds with perSymbol-enrichment and initial automaton 'match'' proved the best result:
  
  Details:
  --------
    'Bounds with perSymbol-enrichment and initial automaton 'match'' succeeded with the following output:
     'Bounds with perSymbol-enrichment and initial automaton 'match''
     ----------------------------------------------------------------
     Answer:           YES(?,O(n^1))
     Input Problem:    innermost runtime-complexity with respect to
       Rules:
         {  d(x) -> e(u(x))
          , d(u(x)) -> c(x)
          , c(u(x)) -> b(x)
          , v(e(x)) -> x
          , b(u(x)) -> a(e(x))}
     
     Proof Output:    
       The problem is match-bounded by 1.
       The enriched problem is compatible with the following automaton:
       {  d_0(2) -> 1
        , d_0(3) -> 1
        , d_0(7) -> 1
        , e_0(2) -> 2
        , e_0(2) -> 6
        , e_0(3) -> 2
        , e_0(3) -> 6
        , e_0(7) -> 2
        , e_0(7) -> 6
        , e_1(2) -> 9
        , e_1(3) -> 9
        , e_1(7) -> 9
        , e_1(8) -> 1
        , u_0(2) -> 3
        , u_0(2) -> 6
        , u_0(3) -> 3
        , u_0(3) -> 6
        , u_0(7) -> 3
        , u_0(7) -> 6
        , u_1(2) -> 8
        , u_1(3) -> 8
        , u_1(7) -> 8
        , c_0(2) -> 4
        , c_0(3) -> 4
        , c_0(7) -> 4
        , c_1(2) -> 1
        , c_1(3) -> 1
        , c_1(7) -> 1
        , b_0(2) -> 5
        , b_0(3) -> 5
        , b_0(7) -> 5
        , b_1(2) -> 1
        , b_1(2) -> 4
        , b_1(3) -> 1
        , b_1(3) -> 4
        , b_1(7) -> 1
        , b_1(7) -> 4
        , v_0(2) -> 6
        , v_0(3) -> 6
        , v_0(7) -> 6
        , a_0(2) -> 6
        , a_0(2) -> 7
        , a_0(3) -> 6
        , a_0(3) -> 7
        , a_0(7) -> 6
        , a_0(7) -> 7
        , a_1(9) -> 1
        , a_1(9) -> 4
        , a_1(9) -> 5}

Tool RC1

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

stdout:

YES(?,O(n^1))

Tool RC2

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

stdout:

YES(?,O(n^1))

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           YES(?,O(n^1))
Input Problem:    runtime-complexity with respect to
  Rules:
    {  d(x) -> e(u(x))
     , d(u(x)) -> c(x)
     , c(u(x)) -> b(x)
     , v(e(x)) -> x
     , b(u(x)) -> a(e(x))}

Proof Output:    
  'Bounds with minimal-enrichment and initial automaton 'match'' proved the best result:
  
  Details:
  --------
    'Bounds with minimal-enrichment and initial automaton 'match'' succeeded with the following output:
     'Bounds with minimal-enrichment and initial automaton 'match''
     --------------------------------------------------------------
     Answer:           YES(?,O(n^1))
     Input Problem:    runtime-complexity with respect to
       Rules:
         {  d(x) -> e(u(x))
          , d(u(x)) -> c(x)
          , c(u(x)) -> b(x)
          , v(e(x)) -> x
          , b(u(x)) -> a(e(x))}
     
     Proof Output:    
       The problem is match-bounded by 1.
       The enriched problem is compatible with the following automaton:
       {  d_0(2) -> 1
        , e_0(2) -> 1
        , e_0(2) -> 2
        , e_1(2) -> 4
        , e_1(3) -> 1
        , u_0(2) -> 1
        , u_0(2) -> 2
        , u_1(2) -> 3
        , c_0(2) -> 1
        , c_1(2) -> 1
        , b_0(2) -> 1
        , b_1(2) -> 1
        , v_0(2) -> 1
        , a_0(2) -> 1
        , a_0(2) -> 2
        , a_1(4) -> 1}

Tool pair1rc

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

stdout:

YES(?,O(n^1))

We consider the following Problem:

  Strict Trs:
    {  d(x) -> e(u(x))
     , d(u(x)) -> c(x)
     , c(u(x)) -> b(x)
     , v(e(x)) -> x
     , b(u(x)) -> a(e(x))}
  StartTerms: basic terms
  Strategy: none

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

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:
    {  d(x) -> e(u(x))
     , d(u(x)) -> c(x)
     , c(u(x)) -> b(x)
     , v(e(x)) -> x
     , b(u(x)) -> a(e(x))}
  StartTerms: basic terms
  Strategy: none
  
  1) 'Fastest' proved the goal fastest:
     
     'Fastest' proved the goal fastest:
     
     'Bounds with minimal-enrichment and initial automaton 'match'' proved the goal fastest:
     
     The problem is match-bounded by 1.
     The enriched problem is compatible with the following automaton:
     {  d_0(2) -> 1
      , e_0(2) -> 1
      , e_0(2) -> 2
      , e_1(2) -> 4
      , e_1(3) -> 1
      , u_0(2) -> 1
      , u_0(2) -> 2
      , u_1(2) -> 3
      , c_0(2) -> 1
      , c_1(2) -> 1
      , b_0(2) -> 1
      , b_1(2) -> 1
      , v_0(2) -> 1
      , a_0(2) -> 1
      , a_0(2) -> 2
      , a_1(4) -> 1}
  

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

Tool pair2rc

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

stdout:

YES(?,O(n^1))

We consider the following Problem:

  Strict Trs:
    {  d(x) -> e(u(x))
     , d(u(x)) -> c(x)
     , c(u(x)) -> b(x)
     , v(e(x)) -> x
     , b(u(x)) -> a(e(x))}
  StartTerms: basic terms
  Strategy: none

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

Application of 'pair2 (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:
    {  d(x) -> e(u(x))
     , d(u(x)) -> c(x)
     , c(u(x)) -> b(x)
     , v(e(x)) -> x
     , b(u(x)) -> a(e(x))}
  StartTerms: basic terms
  Strategy: none
  
  1) 'Fastest' proved the goal fastest:
     
     'Fastest' proved the goal fastest:
     
     'Bounds with minimal-enrichment and initial automaton 'match'' proved the goal fastest:
     
     The problem is match-bounded by 1.
     The enriched problem is compatible with the following automaton:
     {  d_0(2) -> 1
      , e_0(2) -> 1
      , e_0(2) -> 2
      , e_1(2) -> 4
      , e_1(3) -> 1
      , u_0(2) -> 1
      , u_0(2) -> 2
      , u_1(2) -> 3
      , c_0(2) -> 1
      , c_1(2) -> 1
      , b_0(2) -> 1
      , b_1(2) -> 1
      , v_0(2) -> 1
      , a_0(2) -> 1
      , a_0(2) -> 2
      , a_1(4) -> 1}
  

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

Tool pair3irc

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

stdout:

YES(?,O(n^1))

We consider the following Problem:

  Strict Trs:
    {  d(x) -> e(u(x))
     , d(u(x)) -> c(x)
     , c(u(x)) -> b(x)
     , v(e(x)) -> x
     , b(u(x)) -> a(e(x))}
  StartTerms: basic terms
  Strategy: innermost

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

Application of 'pair3 (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:
    {  d(x) -> e(u(x))
     , d(u(x)) -> c(x)
     , c(u(x)) -> b(x)
     , v(e(x)) -> x
     , b(u(x)) -> a(e(x))}
  StartTerms: basic terms
  Strategy: innermost
  
  1) 'Fastest' proved the goal fastest:
     
     'Fastest' proved the goal fastest:
     
     'Bounds with perSymbol-enrichment and initial automaton 'match'' proved the goal fastest:
     
     The problem is match-bounded by 1.
     The enriched problem is compatible with the following automaton:
     {  d_0(2) -> 1
      , d_0(3) -> 1
      , d_0(7) -> 1
      , e_0(2) -> 2
      , e_0(2) -> 6
      , e_0(3) -> 2
      , e_0(3) -> 6
      , e_0(7) -> 2
      , e_0(7) -> 6
      , e_1(2) -> 9
      , e_1(3) -> 9
      , e_1(7) -> 9
      , e_1(8) -> 1
      , u_0(2) -> 3
      , u_0(2) -> 6
      , u_0(3) -> 3
      , u_0(3) -> 6
      , u_0(7) -> 3
      , u_0(7) -> 6
      , u_1(2) -> 8
      , u_1(3) -> 8
      , u_1(7) -> 8
      , c_0(2) -> 4
      , c_0(3) -> 4
      , c_0(7) -> 4
      , c_1(2) -> 1
      , c_1(3) -> 1
      , c_1(7) -> 1
      , b_0(2) -> 5
      , b_0(3) -> 5
      , b_0(7) -> 5
      , b_1(2) -> 1
      , b_1(2) -> 4
      , b_1(3) -> 1
      , b_1(3) -> 4
      , b_1(7) -> 1
      , b_1(7) -> 4
      , v_0(2) -> 6
      , v_0(3) -> 6
      , v_0(7) -> 6
      , a_0(2) -> 6
      , a_0(2) -> 7
      , a_0(3) -> 6
      , a_0(3) -> 7
      , a_0(7) -> 6
      , a_0(7) -> 7
      , a_1(9) -> 1
      , a_1(9) -> 4
      , a_1(9) -> 5}
  

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

Tool pair3rc

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

stdout:

YES(?,O(n^1))

We consider the following Problem:

  Strict Trs:
    {  d(x) -> e(u(x))
     , d(u(x)) -> c(x)
     , c(u(x)) -> b(x)
     , v(e(x)) -> x
     , b(u(x)) -> a(e(x))}
  StartTerms: basic terms
  Strategy: none

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

Application of 'pair3 (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:
    {  d(x) -> e(u(x))
     , d(u(x)) -> c(x)
     , c(u(x)) -> b(x)
     , v(e(x)) -> x
     , b(u(x)) -> a(e(x))}
  StartTerms: basic terms
  Strategy: none
  
  1) 'Fastest' proved the goal fastest:
     
     'Fastest' proved the goal fastest:
     
     'Bounds with minimal-enrichment and initial automaton 'match'' proved the goal fastest:
     
     The problem is match-bounded by 1.
     The enriched problem is compatible with the following automaton:
     {  d_0(2) -> 1
      , e_0(2) -> 1
      , e_0(2) -> 2
      , e_1(2) -> 4
      , e_1(3) -> 1
      , u_0(2) -> 1
      , u_0(2) -> 2
      , u_1(2) -> 3
      , c_0(2) -> 1
      , c_1(2) -> 1
      , b_0(2) -> 1
      , b_1(2) -> 1
      , v_0(2) -> 1
      , a_0(2) -> 1
      , a_0(2) -> 2
      , a_1(4) -> 1}
  

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

Tool rc

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

stdout:

YES(?,O(n^1))

We consider the following Problem:

  Strict Trs:
    {  d(x) -> e(u(x))
     , d(u(x)) -> c(x)
     , c(u(x)) -> b(x)
     , v(e(x)) -> x
     , b(u(x)) -> a(e(x))}
  StartTerms: basic terms
  Strategy: none

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

Application of 'rc (timeout of 60.0 seconds)':
----------------------------------------------
  'Fastest' proved the goal fastest:
  
  'Fastest' proved the goal fastest:
  
  'Bounds with minimal-enrichment and initial automaton 'match' (timeout of 100.0 seconds)' proved the goal fastest:
  
  The problem is match-bounded by 1.
  The enriched problem is compatible with the following automaton:
  {  d_0(2) -> 1
   , e_0(2) -> 1
   , e_0(2) -> 2
   , e_1(2) -> 4
   , e_1(3) -> 1
   , u_0(2) -> 1
   , u_0(2) -> 2
   , u_1(2) -> 3
   , c_0(2) -> 1
   , c_1(2) -> 1
   , b_0(2) -> 1
   , b_1(2) -> 1
   , v_0(2) -> 1
   , a_0(2) -> 1
   , a_0(2) -> 2
   , a_1(4) -> 1}

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

Tool tup3irc

Execution Time6.266999e-2ms
Answer
YES(O(1),O(1))
InputSK90 2.48

stdout:

YES(O(1),O(1))

We consider the following Problem:

  Strict Trs:
    {  d(x) -> e(u(x))
     , d(u(x)) -> c(x)
     , c(u(x)) -> b(x)
     , v(e(x)) -> x
     , b(u(x)) -> a(e(x))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: YES(O(1),O(1))

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:
    {  d(x) -> e(u(x))
     , d(u(x)) -> c(x)
     , c(u(x)) -> b(x)
     , v(e(x)) -> x
     , b(u(x)) -> a(e(x))}
  StartTerms: basic terms
  Strategy: innermost
  
  1) 'dp' proved the goal fastest:
     
     We have computed the following dependency pairs
     
     Strict Dependency Pairs:
       {  d^#(x) -> c_1()
        , d^#(u(x)) -> c_2(c^#(x))
        , c^#(u(x)) -> c_3(b^#(x))
        , v^#(e(x)) -> c_4()
        , b^#(u(x)) -> c_5()}
     
     We consider the following Problem:
     
       Strict DPs:
         {  d^#(x) -> c_1()
          , d^#(u(x)) -> c_2(c^#(x))
          , c^#(u(x)) -> c_3(b^#(x))
          , v^#(e(x)) -> c_4()
          , b^#(u(x)) -> c_5()}
       Weak Trs:
         {  d(x) -> e(u(x))
          , d(u(x)) -> c(x)
          , c(u(x)) -> b(x)
          , v(e(x)) -> x
          , b(u(x)) -> a(e(x))}
       StartTerms: basic terms
       Strategy: innermost
     
     Certificate: YES(O(1),O(1))
     
     Application of 'Fastest':
     -------------------------
       'compose (statically using 'split all congruence from CWD except leafs', multiplication)' proved the goal fastest:
       
       Compose is inapplicable since some weak rule is size increasing
       
       We abort the transformation and continue with the subprocessor on the problem
       
       Strict DPs:
         {  d^#(x) -> c_1()
          , d^#(u(x)) -> c_2(c^#(x))
          , c^#(u(x)) -> c_3(b^#(x))
          , v^#(e(x)) -> c_4()
          , b^#(u(x)) -> c_5()}
       Weak Trs:
         {  d(x) -> e(u(x))
          , d(u(x)) -> c(x)
          , c(u(x)) -> b(x)
          , v(e(x)) -> x
          , b(u(x)) -> a(e(x))}
       StartTerms: basic terms
       Strategy: innermost
       
       1) We consider the the dependency-graph
          
            1: d^#(x) -> c_1()
            
            2: d^#(u(x)) -> c_2(c^#(x))   --> c^#(u(x)) -> c_3(b^#(x)): 3
            
            3: c^#(u(x)) -> c_3(b^#(x))   --> b^#(u(x)) -> c_5(): 5
            
            4: v^#(e(x)) -> c_4()
            
            5: b^#(u(x)) -> c_5()
            
          
          together with the congruence-graph
          
            ->{1}                                                       Noncyclic, trivial, SCC
            
            ->{2}                                                       Noncyclic, trivial, SCC
               |
               `->{3}                                                   Noncyclic, trivial, SCC
                   |
                   `->{5}                                               Noncyclic, trivial, SCC
            
            ->{4}                                                       Noncyclic, trivial, SCC
            
            
            Here rules are as follows:
            
              {  1: d^#(x) -> c_1()
               , 2: d^#(u(x)) -> c_2(c^#(x))
               , 3: c^#(u(x)) -> c_3(b^#(x))
               , 4: v^#(e(x)) -> c_4()
               , 5: b^#(u(x)) -> c_5()}
          
          The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
          
            {  4: v^#(e(x)) -> c_4()
             , 2: d^#(u(x)) -> c_2(c^#(x))
             , 3: c^#(u(x)) -> c_3(b^#(x))
             , 5: b^#(u(x)) -> c_5()
             , 1: d^#(x) -> c_1()}
          
          We consider the following Problem:
          
            Weak Trs:
              {  d(x) -> e(u(x))
               , d(u(x)) -> c(x)
               , c(u(x)) -> b(x)
               , v(e(x)) -> x
               , b(u(x)) -> a(e(x))}
            StartTerms: basic terms
            Strategy: innermost
          
          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
              
              Weak Trs:
                {  d(x) -> e(u(x))
                 , d(u(x)) -> c(x)
                 , c(u(x)) -> b(x)
                 , v(e(x)) -> x
                 , b(u(x)) -> a(e(x))}
              StartTerms: basic terms
              Strategy: innermost
              
              The input problem is not a DP-problem.
            
            We abort the transformation and continue with the subprocessor on the problem
            
            Weak Trs:
              {  d(x) -> e(u(x))
               , d(u(x)) -> c(x)
               , c(u(x)) -> b(x)
               , v(e(x)) -> x
               , b(u(x)) -> a(e(x))}
            StartTerms: basic terms
            Strategy: innermost
            
            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
               
               Weak Trs:
                 {  d(x) -> e(u(x))
                  , d(u(x)) -> c(x)
                  , c(u(x)) -> b(x)
                  , v(e(x)) -> x
                  , b(u(x)) -> a(e(x))}
               StartTerms: basic terms
               Strategy: innermost
               
                 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
                 
                 Weak Trs:
                   {  d(x) -> e(u(x))
                    , d(u(x)) -> c(x)
                    , c(u(x)) -> b(x)
                    , v(e(x)) -> x
                    , b(u(x)) -> a(e(x))}
                 StartTerms: basic terms
                 Strategy: innermost
                 
                   All strict components are empty, nothing to further orient
               
               We abort the transformation and continue with the subprocessor on the problem
               
               Weak Trs:
                 {  d(x) -> e(u(x))
                  , d(u(x)) -> c(x)
                  , c(u(x)) -> b(x)
                  , v(e(x)) -> x
                  , b(u(x)) -> a(e(x))}
               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
                    
                    Weak Trs:
                      {  d(x) -> e(u(x))
                       , d(u(x)) -> c(x)
                       , c(u(x)) -> b(x)
                       , v(e(x)) -> x
                       , b(u(x)) -> a(e(x))}
                    StartTerms: basic terms
                    Strategy: innermost
                    
                    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
                    
                    Weak Trs:
                      {  d(x) -> e(u(x))
                       , d(u(x)) -> c(x)
                       , c(u(x)) -> b(x)
                       , v(e(x)) -> x
                       , b(u(x)) -> a(e(x))}
                    StartTerms: basic terms
                    Strategy: innermost
                    
                      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
                      
                      Weak Trs:
                        {  d(x) -> e(u(x))
                         , d(u(x)) -> c(x)
                         , c(u(x)) -> b(x)
                         , v(e(x)) -> x
                         , b(u(x)) -> a(e(x))}
                      StartTerms: basic terms
                      Strategy: innermost
                      
                        All strict components are empty, nothing to further orient
                  
                  We abort the transformation and continue with the subprocessor on the problem
                  
                  Weak Trs:
                    {  d(x) -> e(u(x))
                     , d(u(x)) -> c(x)
                     , c(u(x)) -> b(x)
                     , v(e(x)) -> x
                     , b(u(x)) -> a(e(x))}
                  StartTerms: basic terms
                  Strategy: innermost
                  
                  1) 'empty' succeeded:
                     
                     Empty rules are trivially bounded
                  
               
            
       
  

Hurray, we answered YES(O(1),O(1))