MAYBE
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:
  Strict:
   {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))}
  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))}
  EDG:
   {(active#(g(X)) -> active#(X), active#(g(X)) -> g#(active(X)))
    (active#(g(X)) -> active#(X), active#(g(X)) -> active#(X))
    (active#(g(X)) -> active#(X), active#(f(X, g(X), Y)) -> f#(Y, Y, Y))
    (g#(ok(X)) -> g#(X), g#(ok(X)) -> g#(X))
    (g#(ok(X)) -> g#(X), g#(mark(X)) -> g#(X))
    (top#(mark(X)) -> proper#(X), proper#(g(X)) -> proper#(X))
    (top#(mark(X)) -> proper#(X), proper#(g(X)) -> g#(proper(X)))
    (top#(mark(X)) -> proper#(X), proper#(f(X1, X2, X3)) -> proper#(X3))
    (top#(mark(X)) -> proper#(X), proper#(f(X1, X2, X3)) -> proper#(X2))
    (top#(mark(X)) -> proper#(X), proper#(f(X1, X2, X3)) -> proper#(X1))
    (top#(mark(X)) -> proper#(X), proper#(f(X1, X2, X3)) -> f#(proper(X1), proper(X2), proper(X3)))
    (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))
    (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))
    (active#(f(X, g(X), Y)) -> f#(Y, Y, Y), f#(ok(X1), ok(X2), ok(X3)) -> f#(X1, X2, X3))
    (proper#(f(X1, X2, X3)) -> proper#(X2), proper#(f(X1, X2, X3)) -> f#(proper(X1), proper(X2), proper(X3)))
    (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)) -> proper#(X2))
    (proper#(f(X1, X2, X3)) -> proper#(X2), proper#(f(X1, X2, X3)) -> proper#(X3))
    (proper#(f(X1, X2, X3)) -> proper#(X2), proper#(g(X)) -> g#(proper(X)))
    (proper#(f(X1, X2, X3)) -> proper#(X2), proper#(g(X)) -> proper#(X))
    (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#(X1), proper#(f(X1, X2, X3)) -> proper#(X1))
    (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#(X3))
    (proper#(f(X1, X2, X3)) -> proper#(X1), proper#(g(X)) -> g#(proper(X)))
    (proper#(f(X1, X2, X3)) -> proper#(X1), proper#(g(X)) -> proper#(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))
    (top#(ok(X)) -> active#(X), active#(f(X, g(X), Y)) -> f#(Y, Y, Y))
    (top#(ok(X)) -> active#(X), active#(g(X)) -> active#(X))
    (top#(ok(X)) -> active#(X), active#(g(X)) -> g#(active(X)))
    (proper#(g(X)) -> proper#(X), proper#(f(X1, X2, X3)) -> f#(proper(X1), proper(X2), proper(X3)))
    (proper#(g(X)) -> proper#(X), proper#(f(X1, X2, X3)) -> proper#(X1))
    (proper#(g(X)) -> proper#(X), proper#(f(X1, X2, X3)) -> proper#(X2))
    (proper#(g(X)) -> proper#(X), proper#(f(X1, X2, X3)) -> proper#(X3))
    (proper#(g(X)) -> proper#(X), proper#(g(X)) -> g#(proper(X)))
    (proper#(g(X)) -> proper#(X), proper#(g(X)) -> proper#(X))
    (g#(mark(X)) -> g#(X), g#(mark(X)) -> g#(X))
    (g#(mark(X)) -> g#(X), g#(ok(X)) -> g#(X))
    (proper#(f(X1, X2, X3)) -> proper#(X3), proper#(f(X1, X2, X3)) -> f#(proper(X1), proper(X2), proper(X3)))
    (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)) -> proper#(X2))
    (proper#(f(X1, X2, X3)) -> proper#(X3), proper#(f(X1, X2, X3)) -> proper#(X3))
    (proper#(f(X1, X2, X3)) -> proper#(X3), proper#(g(X)) -> g#(proper(X)))
    (proper#(f(X1, X2, X3)) -> proper#(X3), proper#(g(X)) -> proper#(X))}
   SCCS:
    Scc:
     {top#(mark(X)) -> top#(proper(X)),
        top#(ok(X)) -> top#(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:
     {active#(g(X)) -> active#(X)}
    Scc:
     {f#(ok(X1), ok(X2), ok(X3)) -> f#(X1, X2, X3)}
    SCC:
     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:
     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))}
     SPSC:
      Simple Projection:
       pi(proper#) = 0
      Strict:
       {proper#(f(X1, X2, X3)) -> proper#(X1),
        proper#(f(X1, X2, X3)) -> proper#(X2),
                 proper#(g(X)) -> proper#(X)}
      EDG:
       {(proper#(f(X1, X2, X3)) -> proper#(X1), proper#(g(X)) -> proper#(X))
        (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#(g(X)) -> proper#(X), proper#(f(X1, X2, X3)) -> proper#(X1))
        (proper#(g(X)) -> proper#(X), proper#(f(X1, X2, X3)) -> proper#(X2))
        (proper#(g(X)) -> proper#(X), proper#(g(X)) -> proper#(X))
        (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)) -> proper#(X2))
        (proper#(f(X1, X2, X3)) -> proper#(X2), proper#(g(X)) -> proper#(X))}
       SCCS:
        Scc:
         {proper#(f(X1, X2, X3)) -> proper#(X1),
          proper#(f(X1, X2, X3)) -> proper#(X2),
                   proper#(g(X)) -> proper#(X)}
        SCC:
         Strict:
          {proper#(f(X1, X2, X3)) -> proper#(X1),
           proper#(f(X1, X2, X3)) -> proper#(X2),
                    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))}
         SPSC:
          Simple Projection:
           pi(proper#) = 0
          Strict:
           {proper#(f(X1, X2, X3)) -> proper#(X1),
                     proper#(g(X)) -> proper#(X)}
          EDG:
           {(proper#(f(X1, X2, X3)) -> proper#(X1), proper#(g(X)) -> proper#(X))
            (proper#(f(X1, X2, X3)) -> proper#(X1), proper#(f(X1, X2, X3)) -> proper#(X1))
            (proper#(g(X)) -> proper#(X), proper#(f(X1, X2, X3)) -> proper#(X1))
            (proper#(g(X)) -> proper#(X), proper#(g(X)) -> proper#(X))}
           SCCS:
            Scc:
             {proper#(f(X1, X2, X3)) -> proper#(X1),
                       proper#(g(X)) -> proper#(X)}
            SCC:
             Strict:
              {proper#(f(X1, X2, X3)) -> proper#(X1),
                        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))}
             SPSC:
              Simple Projection:
               pi(proper#) = 0
              Strict:
               {proper#(g(X)) -> proper#(X)}
              EDG:
               {(proper#(g(X)) -> proper#(X), proper#(g(X)) -> proper#(X))}
               SCCS:
                Scc:
                 {proper#(g(X)) -> proper#(X)}
                SCC:
                 Strict:
                  {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))}
                 SPSC:
                  Simple Projection:
                   pi(proper#) = 0
                  Strict:
                   {}
                  Qed
    SCC:
     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))}
     SPSC:
      Simple Projection:
       pi(g#) = 0
      Strict:
       {g#(ok(X)) -> g#(X)}
      EDG:
       {(g#(ok(X)) -> g#(X), g#(ok(X)) -> g#(X))}
       SCCS:
        Scc:
         {g#(ok(X)) -> g#(X)}
        SCC:
         Strict:
          {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))}
         SPSC:
          Simple Projection:
           pi(g#) = 0
          Strict:
           {}
          Qed
    SCC:
     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))}
     SPSC:
      Simple Projection:
       pi(active#) = 0
      Strict:
       {}
      Qed
    SCC:
     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))}
     SPSC:
      Simple Projection:
       pi(f#) = 2
      Strict:
       {}
      Qed