MAYBE
Time: 0.087435
TRS:
 {f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3),
     active f(X, g X, Y) -> mark f(Y, Y, Y),
              active g X -> g active X,
            active g b() -> mark c(),
              active b() -> mark c(),
                g mark X -> mark g X,
                  g ok X -> ok g X,
    proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3),
              proper g X -> g proper X,
              proper c() -> ok c(),
              proper b() -> ok b(),
              top mark X -> top proper X,
                top ok X -> top active X}
 DP:
  DP:
   {f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3),
       active# f(X, g X, Y) -> f#(Y, Y, Y),
                active# g X -> active# X,
                active# g X -> g# active X,
                  g# mark X -> g# X,
                    g# ok X -> g# X,
      proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper X3),
      proper# f(X1, X2, X3) -> proper# X1,
      proper# f(X1, X2, X3) -> proper# X2,
      proper# f(X1, X2, X3) -> proper# X3,
                proper# g X -> g# proper X,
                proper# g X -> proper# X,
                top# mark X -> proper# X,
                top# mark X -> top# proper X,
                  top# ok X -> active# X,
                  top# ok X -> top# active X}
  TRS:
  {f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3),
      active f(X, g X, Y) -> mark f(Y, Y, Y),
               active g X -> g active X,
             active g b() -> mark c(),
               active b() -> mark c(),
                 g mark X -> mark g X,
                   g ok X -> ok g X,
     proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3),
               proper g X -> g proper X,
               proper c() -> ok c(),
               proper b() -> ok b(),
               top mark X -> top proper X,
                 top ok X -> top active X}
  EDG:
   {(active# g X -> g# active X, g# ok X -> g# X)
    (active# g X -> g# active X, g# mark X -> g# X)
    (top# mark X -> top# proper X, top# ok X -> top# active X)
    (top# mark X -> top# proper X, top# ok X -> active# X)
    (top# mark X -> top# proper X, top# mark X -> top# proper X)
    (top# mark X -> top# proper X, top# mark X -> proper# X)
    (proper# f(X1, X2, X3) -> proper# X3, proper# g X -> proper# X)
    (proper# f(X1, X2, X3) -> proper# X3, proper# g X -> g# proper X)
    (proper# f(X1, X2, X3) -> proper# X3, proper# f(X1, X2, X3) -> proper# X3)
    (proper# f(X1, X2, X3) -> proper# X3, proper# f(X1, X2, X3) -> proper# X2)
    (proper# f(X1, X2, X3) -> proper# X3, proper# f(X1, X2, X3) -> proper# X1)
    (proper# f(X1, X2, X3) -> proper# X3, proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper X3))
    (g# mark X -> g# X, g# ok X -> g# X)
    (g# mark X -> g# X, g# mark X -> g# X)
    (proper# g X -> proper# X, proper# g X -> proper# X)
    (proper# g X -> proper# X, proper# g X -> g# proper X)
    (proper# g X -> proper# X, proper# f(X1, X2, X3) -> proper# X3)
    (proper# g X -> proper# X, proper# f(X1, X2, X3) -> proper# X2)
    (proper# g X -> proper# X, proper# f(X1, X2, X3) -> proper# X1)
    (proper# g X -> proper# X, proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper X3))
    (top# ok X -> active# X, active# g X -> g# active X)
    (top# ok X -> active# X, active# g X -> active# X)
    (top# ok X -> active# X, active# f(X, g X, Y) -> f#(Y, Y, Y))
    (proper# f(X1, X2, X3) -> proper# X1, proper# g X -> proper# X)
    (proper# f(X1, X2, X3) -> proper# X1, proper# g X -> g# proper X)
    (proper# f(X1, X2, X3) -> proper# X1, proper# f(X1, X2, X3) -> proper# X3)
    (proper# f(X1, X2, X3) -> proper# X1, proper# f(X1, X2, X3) -> proper# X2)
    (proper# f(X1, X2, X3) -> proper# X1, proper# f(X1, X2, X3) -> proper# X1)
    (proper# f(X1, X2, X3) -> proper# X1, proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper X3))
    (proper# f(X1, X2, X3) -> proper# X2, proper# g X -> proper# X)
    (proper# f(X1, X2, X3) -> proper# X2, proper# g X -> g# proper X)
    (proper# f(X1, X2, X3) -> proper# X2, proper# f(X1, X2, X3) -> proper# X3)
    (proper# f(X1, X2, X3) -> proper# X2, proper# f(X1, X2, X3) -> proper# X2)
    (proper# f(X1, X2, X3) -> proper# X2, proper# f(X1, X2, X3) -> proper# X1)
    (proper# f(X1, X2, X3) -> proper# X2, proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper X3))
    (f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3), f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3))
    (proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper X3), f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3))
    (top# mark X -> proper# X, proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper X3))
    (top# mark X -> proper# X, proper# f(X1, X2, X3) -> proper# X1)
    (top# mark X -> proper# X, proper# f(X1, X2, X3) -> proper# X2)
    (top# mark X -> proper# X, proper# f(X1, X2, X3) -> proper# X3)
    (top# mark X -> proper# X, proper# g X -> g# proper X)
    (top# mark X -> proper# X, proper# g X -> proper# X)
    (g# ok X -> g# X, g# mark X -> g# X)
    (g# ok X -> g# X, g# ok X -> g# X)
    (active# g X -> active# X, active# f(X, g X, Y) -> f#(Y, Y, Y))
    (active# g X -> active# X, active# g X -> active# X)
    (active# g X -> active# X, active# g X -> g# active X)
    (top# ok X -> top# active X, top# mark X -> proper# X)
    (top# ok X -> top# active X, top# mark X -> top# proper X)
    (top# ok X -> top# active X, top# ok X -> active# X)
    (top# ok X -> top# active X, top# ok X -> top# active X)
    (proper# g X -> g# proper X, g# mark X -> g# X)
    (proper# g X -> g# proper X, g# ok X -> g# X)
    (active# f(X, g X, Y) -> f#(Y, Y, Y), f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3))}
   STATUS:
    arrows: 0.785156
    SCCS (5):
     Scc:
      {top# mark X -> top# proper X,
         top# ok X -> top# active X}
     Scc:
      {active# g X -> active# X}
     Scc:
      {proper# f(X1, X2, X3) -> proper# X1,
       proper# f(X1, X2, X3) -> proper# X2,
       proper# f(X1, X2, X3) -> proper# X3,
                 proper# g X -> proper# X}
     Scc:
      {g# mark X -> g# X,
         g# ok X -> g# X}
     Scc:
      {f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3)}
     
     SCC (2):
      Strict:
       {top# mark X -> top# proper X,
          top# ok X -> top# active X}
      Weak:
      {f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3),
          active f(X, g X, Y) -> mark f(Y, Y, Y),
                   active g X -> g active X,
                 active g b() -> mark c(),
                   active b() -> mark c(),
                     g mark X -> mark g X,
                       g ok X -> ok g X,
         proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3),
                   proper g X -> g proper X,
                   proper c() -> ok c(),
                   proper b() -> ok b(),
                   top mark X -> top proper X,
                     top ok X -> top active X}
      Fail
     
     SCC (1):
      Strict:
       {active# g X -> active# X}
      Weak:
      {f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3),
          active f(X, g X, Y) -> mark f(Y, Y, Y),
                   active g X -> g active X,
                 active g b() -> mark c(),
                   active b() -> mark c(),
                     g mark X -> mark g X,
                       g ok X -> ok g X,
         proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3),
                   proper g X -> g proper X,
                   proper c() -> ok c(),
                   proper b() -> ok b(),
                   top mark X -> top proper X,
                     top ok X -> top active X}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [f](x0, x1, x2) = x0 + 1,
        
        [mark](x0) = x0 + 1,
        
        [active](x0) = x0 + 1,
        
        [g](x0) = x0 + 1,
        
        [proper](x0) = 0,
        
        [ok](x0) = x0 + 1,
        
        [top](x0) = x0 + 1,
        
        [c] = 1,
        
        [b] = 0,
        
        [active#](x0) = x0
       Strict:
        active# g X -> active# X
        1 + 1X >= 0 + 1X
       Weak:
        top ok X -> top active X
        2 + 1X >= 2 + 1X
        top mark X -> top proper X
        2 + 1X >= 1 + 0X
        proper b() -> ok b()
        0 >= 1
        proper c() -> ok c()
        0 >= 2
        proper g X -> g proper X
        0 + 0X >= 1 + 0X
        proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3)
        0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3
        g ok X -> ok g X
        2 + 1X >= 2 + 1X
        g mark X -> mark g X
        2 + 1X >= 2 + 1X
        active b() -> mark c()
        1 >= 2
        active g b() -> mark c()
        2 >= 2
        active g X -> g active X
        2 + 1X >= 2 + 1X
        active f(X, g X, Y) -> mark f(Y, Y, Y)
        2 + 1Y + 0X >= 2 + 1Y
        f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3)
        2 + 0X1 + 0X2 + 1X3 >= 2 + 0X1 + 0X2 + 1X3
      Qed
    
    SCC (4):
     Strict:
      {proper# f(X1, X2, X3) -> proper# X1,
       proper# f(X1, X2, X3) -> proper# X2,
       proper# f(X1, X2, X3) -> proper# X3,
                 proper# g X -> proper# X}
     Weak:
     {f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3),
         active f(X, g X, Y) -> mark f(Y, Y, Y),
                  active g X -> g active X,
                active g b() -> mark c(),
                  active b() -> mark c(),
                    g mark X -> mark g X,
                      g ok X -> ok g X,
        proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3),
                  proper g X -> g proper X,
                  proper c() -> ok c(),
                  proper b() -> ok b(),
                  top mark X -> top proper X,
                    top ok X -> top active X}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [f](x0, x1, x2) = x0 + x1 + x2,
       
       [mark](x0) = 0,
       
       [active](x0) = x0 + 1,
       
       [g](x0) = x0 + 1,
       
       [proper](x0) = x0 + 1,
       
       [ok](x0) = 0,
       
       [top](x0) = 0,
       
       [c] = 1,
       
       [b] = 0,
       
       [proper#](x0) = x0
      Strict:
       proper# g X -> proper# X
       1 + 1X >= 0 + 1X
       proper# f(X1, X2, X3) -> proper# X3
       0 + 1X1 + 1X2 + 1X3 >= 0 + 1X3
       proper# f(X1, X2, X3) -> proper# X2
       0 + 1X1 + 1X2 + 1X3 >= 0 + 1X2
       proper# f(X1, X2, X3) -> proper# X1
       0 + 1X1 + 1X2 + 1X3 >= 0 + 1X1
      Weak:
       top ok X -> top active X
       0 + 0X >= 0 + 0X
       top mark X -> top proper X
       0 + 0X >= 0 + 0X
       proper b() -> ok b()
       1 >= 0
       proper c() -> ok c()
       2 >= 0
       proper g X -> g proper X
       2 + 1X >= 2 + 1X
       proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3)
       1 + 1X1 + 1X2 + 1X3 >= 3 + 1X1 + 1X2 + 1X3
       g ok X -> ok g X
       1 + 0X >= 0 + 0X
       g mark X -> mark g X
       1 + 0X >= 0 + 0X
       active b() -> mark c()
       1 >= 0
       active g b() -> mark c()
       2 >= 0
       active g X -> g active X
       2 + 1X >= 2 + 1X
       active f(X, g X, Y) -> mark f(Y, Y, Y)
       2 + 1Y + 2X >= 0 + 0Y
       f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3)
       0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3
     SCCS (1):
      Scc:
       {proper# f(X1, X2, X3) -> proper# X1,
        proper# f(X1, X2, X3) -> proper# X2,
        proper# f(X1, X2, X3) -> proper# X3}
      
      SCC (3):
       Strict:
        {proper# f(X1, X2, X3) -> proper# X1,
         proper# f(X1, X2, X3) -> proper# X2,
         proper# f(X1, X2, X3) -> proper# X3}
       Weak:
       {f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3),
           active f(X, g X, Y) -> mark f(Y, Y, Y),
                    active g X -> g active X,
                  active g b() -> mark c(),
                    active b() -> mark c(),
                      g mark X -> mark g X,
                        g ok X -> ok g X,
          proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3),
                    proper g X -> g proper X,
                    proper c() -> ok c(),
                    proper b() -> ok b(),
                    top mark X -> top proper X,
                      top ok X -> top active X}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [f](x0, x1, x2) = x0 + x1 + x2 + 1,
         
         [mark](x0) = x0 + 1,
         
         [active](x0) = 0,
         
         [g](x0) = x0 + 1,
         
         [proper](x0) = 0,
         
         [ok](x0) = x0 + 1,
         
         [top](x0) = 0,
         
         [c] = 1,
         
         [b] = 1,
         
         [proper#](x0) = x0 + 1
        Strict:
         proper# f(X1, X2, X3) -> proper# X3
         2 + 1X1 + 1X2 + 1X3 >= 1 + 1X3
         proper# f(X1, X2, X3) -> proper# X2
         2 + 1X1 + 1X2 + 1X3 >= 1 + 1X2
         proper# f(X1, X2, X3) -> proper# X1
         2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1
        Weak:
         top ok X -> top active X
         0 + 0X >= 0 + 0X
         top mark X -> top proper X
         0 + 0X >= 0 + 0X
         proper b() -> ok b()
         0 >= 2
         proper c() -> ok c()
         0 >= 2
         proper g X -> g proper X
         0 + 0X >= 1 + 0X
         proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3)
         0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3
         g ok X -> ok g X
         2 + 1X >= 2 + 1X
         g mark X -> mark g X
         2 + 1X >= 2 + 1X
         active b() -> mark c()
         0 >= 2
         active g b() -> mark c()
         0 >= 2
         active g X -> g active X
         0 + 0X >= 1 + 0X
         active f(X, g X, Y) -> mark f(Y, Y, Y)
         0 + 0Y + 0X >= 2 + 3Y
         f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3)
         4 + 1X1 + 1X2 + 1X3 >= 2 + 1X1 + 1X2 + 1X3
       Qed
   
   
   
   SCC (2):
    Strict:
     {g# mark X -> g# X,
        g# ok X -> g# X}
    Weak:
    {f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3),
        active f(X, g X, Y) -> mark f(Y, Y, Y),
                 active g X -> g active X,
               active g b() -> mark c(),
                 active b() -> mark c(),
                   g mark X -> mark g X,
                     g ok X -> ok g X,
       proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3),
                 proper g X -> g proper X,
                 proper c() -> ok c(),
                 proper b() -> ok b(),
                 top mark X -> top proper X,
                   top ok X -> top active X}
    POLY:
     Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
     Interpretation:
      [f](x0, x1, x2) = x0 + 1,
      
      [mark](x0) = x0,
      
      [active](x0) = x0 + 1,
      
      [g](x0) = x0 + 1,
      
      [proper](x0) = 0,
      
      [ok](x0) = x0 + 1,
      
      [top](x0) = 0,
      
      [c] = 0,
      
      [b] = 0,
      
      [g#](x0) = x0
     Strict:
      g# ok X -> g# X
      1 + 1X >= 0 + 1X
      g# mark X -> g# X
      0 + 1X >= 0 + 1X
     Weak:
      top ok X -> top active X
      0 + 0X >= 0 + 0X
      top mark X -> top proper X
      0 + 0X >= 0 + 0X
      proper b() -> ok b()
      0 >= 1
      proper c() -> ok c()
      0 >= 1
      proper g X -> g proper X
      0 + 0X >= 1 + 0X
      proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3)
      0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3
      g ok X -> ok g X
      2 + 1X >= 2 + 1X
      g mark X -> mark g X
      1 + 1X >= 1 + 1X
      active b() -> mark c()
      1 >= 0
      active g b() -> mark c()
      2 >= 0
      active g X -> g active X
      2 + 1X >= 2 + 1X
      active f(X, g X, Y) -> mark f(Y, Y, Y)
      2 + 1Y + 0X >= 1 + 1Y
      f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3)
      2 + 0X1 + 0X2 + 1X3 >= 2 + 0X1 + 0X2 + 1X3
    SCCS (1):
     Scc:
      {g# mark X -> g# X}
     
     SCC (1):
      Strict:
       {g# mark X -> g# X}
      Weak:
      {f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3),
          active f(X, g X, Y) -> mark f(Y, Y, Y),
                   active g X -> g active X,
                 active g b() -> mark c(),
                   active b() -> mark c(),
                     g mark X -> mark g X,
                       g ok X -> ok g X,
         proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3),
                   proper g X -> g proper X,
                   proper c() -> ok c(),
                   proper b() -> ok b(),
                   top mark X -> top proper X,
                     top ok X -> top active X}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [f](x0, x1, x2) = x0 + 1,
        
        [mark](x0) = x0 + 1,
        
        [active](x0) = x0 + 1,
        
        [g](x0) = x0 + 1,
        
        [proper](x0) = 0,
        
        [ok](x0) = x0 + 1,
        
        [top](x0) = x0 + 1,
        
        [c] = 1,
        
        [b] = 0,
        
        [g#](x0) = x0
       Strict:
        g# mark X -> g# X
        1 + 1X >= 0 + 1X
       Weak:
        top ok X -> top active X
        2 + 1X >= 2 + 1X
        top mark X -> top proper X
        2 + 1X >= 1 + 0X
        proper b() -> ok b()
        0 >= 1
        proper c() -> ok c()
        0 >= 2
        proper g X -> g proper X
        0 + 0X >= 1 + 0X
        proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3)
        0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3
        g ok X -> ok g X
        2 + 1X >= 2 + 1X
        g mark X -> mark g X
        2 + 1X >= 2 + 1X
        active b() -> mark c()
        1 >= 2
        active g b() -> mark c()
        2 >= 2
        active g X -> g active X
        2 + 1X >= 2 + 1X
        active f(X, g X, Y) -> mark f(Y, Y, Y)
        2 + 1Y + 0X >= 2 + 1Y
        f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3)
        2 + 0X1 + 0X2 + 1X3 >= 2 + 0X1 + 0X2 + 1X3
      Qed
  
  SCC (1):
   Strict:
    {f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3)}
   Weak:
   {f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3),
       active f(X, g X, Y) -> mark f(Y, Y, Y),
                active g X -> g active X,
              active g b() -> mark c(),
                active b() -> mark c(),
                  g mark X -> mark g X,
                    g ok X -> ok g X,
      proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3),
                proper g X -> g proper X,
                proper c() -> ok c(),
                proper b() -> ok b(),
                top mark X -> top proper X,
                  top ok X -> top active X}
   POLY:
    Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
    Interpretation:
     [f](x0, x1, x2) = x0 + x1 + x2 + 1,
     
     [mark](x0) = x0 + 1,
     
     [active](x0) = 0,
     
     [g](x0) = x0 + 1,
     
     [proper](x0) = x0 + 1,
     
     [ok](x0) = x0 + 1,
     
     [top](x0) = 0,
     
     [c] = 1,
     
     [b] = 1,
     
     [f#](x0, x1, x2) = x0
    Strict:
     f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3)
     1 + 0X1 + 0X2 + 1X3 >= 0 + 0X1 + 0X2 + 1X3
    Weak:
     top ok X -> top active X
     0 + 0X >= 0 + 0X
     top mark X -> top proper X
     0 + 0X >= 0 + 0X
     proper b() -> ok b()
     2 >= 2
     proper c() -> ok c()
     2 >= 2
     proper g X -> g proper X
     2 + 1X >= 2 + 1X
     proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3)
     2 + 1X1 + 1X2 + 1X3 >= 4 + 1X1 + 1X2 + 1X3
     g ok X -> ok g X
     2 + 1X >= 2 + 1X
     g mark X -> mark g X
     2 + 1X >= 2 + 1X
     active b() -> mark c()
     0 >= 2
     active g b() -> mark c()
     0 >= 2
     active g X -> g active X
     0 + 0X >= 1 + 0X
     active f(X, g X, Y) -> mark f(Y, Y, Y)
     0 + 0Y + 0X >= 2 + 3Y
     f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3)
     4 + 1X1 + 1X2 + 1X3 >= 2 + 1X1 + 1X2 + 1X3
   Qed