MAYBE
Time: 0.030203
TRS:
 {       f mark x -> mark f x,
       f active x -> active f x,
           f no x -> no f x,
       active f x -> mark f f x,
       chk no f x -> f chk mat(f f f f f f f f f f X(), x),
       chk no c() -> active c(),
  mat(f x, f y()) -> f mat(x, y()),
    mat(f x, c()) -> no c(),
        tp mark x -> tp chk mat(f f f f f f f f f f X(), x)}
 DP:
  DP:
   {       f# mark x -> f# x,
         f# active x -> f# x,
         f# active x -> active# f x,
             f# no x -> f# x,
         active# f x -> f# f x,
         chk# no f x -> f# f f f f f f f f f X(),
         chk# no f x -> f# f f f f f f f f X(),
         chk# no f x -> f# f f f f f f f X(),
         chk# no f x -> f# f f f f f f X(),
         chk# no f x -> f# f f f f f X(),
         chk# no f x -> f# f f f f X(),
         chk# no f x -> f# f f f X(),
         chk# no f x -> f# f f X(),
         chk# no f x -> f# f X(),
         chk# no f x -> f# chk mat(f f f f f f f f f f X(), x),
         chk# no f x -> f# X(),
         chk# no f x -> chk# mat(f f f f f f f f f f X(), x),
         chk# no f x -> mat#(f f f f f f f f f f X(), x),
         chk# no c() -> active# c(),
    mat#(f x, f y()) -> f# mat(x, y()),
    mat#(f x, f y()) -> mat#(x, y()),
          tp# mark x -> f# f f f f f f f f f X(),
          tp# mark x -> f# f f f f f f f f X(),
          tp# mark x -> f# f f f f f f f X(),
          tp# mark x -> f# f f f f f f X(),
          tp# mark x -> f# f f f f f X(),
          tp# mark x -> f# f f f f X(),
          tp# mark x -> f# f f f X(),
          tp# mark x -> f# f f X(),
          tp# mark x -> f# f X(),
          tp# mark x -> f# X(),
          tp# mark x -> chk# mat(f f f f f f f f f f X(), x),
          tp# mark x -> mat#(f f f f f f f f f f X(), x),
          tp# mark x -> tp# chk mat(f f f f f f f f f f X(), x)}
  TRS:
  {       f mark x -> mark f x,
        f active x -> active f x,
            f no x -> no f x,
        active f x -> mark f f x,
        chk no f x -> f chk mat(f f f f f f f f f f X(), x),
        chk no c() -> active c(),
   mat(f x, f y()) -> f mat(x, y()),
     mat(f x, c()) -> no c(),
         tp mark x -> tp chk mat(f f f f f f f f f f X(), x)}
  EDG:
   {(tp# mark x -> mat#(f f f f f f f f f f X(), x), mat#(f x, f y()) -> mat#(x, y()))
    (tp# mark x -> mat#(f f f f f f f f f f X(), x), mat#(f x, f y()) -> f# mat(x, y()))
    (active# f x -> f# f x, f# no x -> f# x)
    (active# f x -> f# f x, f# active x -> active# f x)
    (active# f x -> f# f x, f# active x -> f# x)
    (active# f x -> f# f x, f# mark x -> f# x)
    (f# mark x -> f# x, f# no x -> f# x)
    (f# mark x -> f# x, f# active x -> active# f x)
    (f# mark x -> f# x, f# active x -> f# x)
    (f# mark x -> f# x, f# mark x -> f# x)
    (f# no x -> f# x, f# no x -> f# x)
    (f# no x -> f# x, f# active x -> active# f x)
    (f# no x -> f# x, f# active x -> f# x)
    (f# no x -> f# x, f# mark x -> f# x)
    (chk# no f x -> f# chk mat(f f f f f f f f f f X(), x), f# no x -> f# x)
    (chk# no f x -> f# chk mat(f f f f f f f f f f X(), x), f# active x -> active# f x)
    (chk# no f x -> f# chk mat(f f f f f f f f f f X(), x), f# active x -> f# x)
    (chk# no f x -> f# chk mat(f f f f f f f f f f X(), x), f# mark x -> f# x)
    (tp# mark x -> tp# chk mat(f f f f f f f f f f X(), x), tp# mark x -> tp# chk mat(f f f f f f f f f f X(), x))
    (tp# mark x -> tp# chk mat(f f f f f f f f f f X(), x), tp# mark x -> mat#(f f f f f f f f f f X(), x))
    (tp# mark x -> tp# chk mat(f f f f f f f f f f X(), x), tp# mark x -> chk# mat(f f f f f f f f f f X(), x))
    (tp# mark x -> tp# chk mat(f f f f f f f f f f X(), x), tp# mark x -> f# X())
    (tp# mark x -> tp# chk mat(f f f f f f f f f f X(), x), tp# mark x -> f# f X())
    (tp# mark x -> tp# chk mat(f f f f f f f f f f X(), x), tp# mark x -> f# f f X())
    (tp# mark x -> tp# chk mat(f f f f f f f f f f X(), x), tp# mark x -> f# f f f X())
    (tp# mark x -> tp# chk mat(f f f f f f f f f f X(), x), tp# mark x -> f# f f f f X())
    (tp# mark x -> tp# chk mat(f f f f f f f f f f X(), x), tp# mark x -> f# f f f f f X())
    (tp# mark x -> tp# chk mat(f f f f f f f f f f X(), x), tp# mark x -> f# f f f f f f X())
    (tp# mark x -> tp# chk mat(f f f f f f f f f f X(), x), tp# mark x -> f# f f f f f f f X())
    (tp# mark x -> tp# chk mat(f f f f f f f f f f X(), x), tp# mark x -> f# f f f f f f f f X())
    (tp# mark x -> tp# chk mat(f f f f f f f f f f X(), x), tp# mark x -> f# f f f f f f f f f X())
    (tp# mark x -> chk# mat(f f f f f f f f f f X(), x), chk# no c() -> active# c())
    (tp# mark x -> chk# mat(f f f f f f f f f f X(), x), chk# no f x -> mat#(f f f f f f f f f f X(), x))
    (tp# mark x -> chk# mat(f f f f f f f f f f X(), x), chk# no f x -> chk# mat(f f f f f f f f f f X(), x))
    (tp# mark x -> chk# mat(f f f f f f f f f f X(), x), chk# no f x -> f# X())
    (tp# mark x -> chk# mat(f f f f f f f f f f X(), x), chk# no f x -> f# chk mat(f f f f f f f f f f X(), x))
    (tp# mark x -> chk# mat(f f f f f f f f f f X(), x), chk# no f x -> f# f X())
    (tp# mark x -> chk# mat(f f f f f f f f f f X(), x), chk# no f x -> f# f f X())
    (tp# mark x -> chk# mat(f f f f f f f f f f X(), x), chk# no f x -> f# f f f X())
    (tp# mark x -> chk# mat(f f f f f f f f f f X(), x), chk# no f x -> f# f f f f X())
    (tp# mark x -> chk# mat(f f f f f f f f f f X(), x), chk# no f x -> f# f f f f f X())
    (tp# mark x -> chk# mat(f f f f f f f f f f X(), x), chk# no f x -> f# f f f f f f X())
    (tp# mark x -> chk# mat(f f f f f f f f f f X(), x), chk# no f x -> f# f f f f f f f X())
    (tp# mark x -> chk# mat(f f f f f f f f f f X(), x), chk# no f x -> f# f f f f f f f f X())
    (tp# mark x -> chk# mat(f f f f f f f f f f X(), x), chk# no f x -> f# f f f f f f f f f X())
    (chk# no f x -> chk# mat(f f f f f f f f f f X(), x), chk# no f x -> f# f f f f f f f f f X())
    (chk# no f x -> chk# mat(f f f f f f f f f f X(), x), chk# no f x -> f# f f f f f f f f X())
    (chk# no f x -> chk# mat(f f f f f f f f f f X(), x), chk# no f x -> f# f f f f f f f X())
    (chk# no f x -> chk# mat(f f f f f f f f f f X(), x), chk# no f x -> f# f f f f f f X())
    (chk# no f x -> chk# mat(f f f f f f f f f f X(), x), chk# no f x -> f# f f f f f X())
    (chk# no f x -> chk# mat(f f f f f f f f f f X(), x), chk# no f x -> f# f f f f X())
    (chk# no f x -> chk# mat(f f f f f f f f f f X(), x), chk# no f x -> f# f f f X())
    (chk# no f x -> chk# mat(f f f f f f f f f f X(), x), chk# no f x -> f# f f X())
    (chk# no f x -> chk# mat(f f f f f f f f f f X(), x), chk# no f x -> f# f X())
    (chk# no f x -> chk# mat(f f f f f f f f f f X(), x), chk# no f x -> f# chk mat(f f f f f f f f f f X(), x))
    (chk# no f x -> chk# mat(f f f f f f f f f f X(), x), chk# no f x -> f# X())
    (chk# no f x -> chk# mat(f f f f f f f f f f X(), x), chk# no f x -> chk# mat(f f f f f f f f f f X(), x))
    (chk# no f x -> chk# mat(f f f f f f f f f f X(), x), chk# no f x -> mat#(f f f f f f f f f f X(), x))
    (chk# no f x -> chk# mat(f f f f f f f f f f X(), x), chk# no c() -> active# c())
    (f# active x -> f# x, f# mark x -> f# x)
    (f# active x -> f# x, f# active x -> f# x)
    (f# active x -> f# x, f# active x -> active# f x)
    (f# active x -> f# x, f# no x -> f# x)
    (f# active x -> active# f x, active# f x -> f# f x)
    (chk# no f x -> mat#(f f f f f f f f f f X(), x), mat#(f x, f y()) -> f# mat(x, y()))
    (chk# no f x -> mat#(f f f f f f f f f f X(), x), mat#(f x, f y()) -> mat#(x, y()))}
   EDG:
    {(active# f x -> f# f x, f# no x -> f# x)
     (active# f x -> f# f x, f# active x -> active# f x)
     (active# f x -> f# f x, f# active x -> f# x)
     (active# f x -> f# f x, f# mark x -> f# x)
     (f# mark x -> f# x, f# no x -> f# x)
     (f# mark x -> f# x, f# active x -> active# f x)
     (f# mark x -> f# x, f# active x -> f# x)
     (f# mark x -> f# x, f# mark x -> f# x)
     (f# no x -> f# x, f# no x -> f# x)
     (f# no x -> f# x, f# active x -> active# f x)
     (f# no x -> f# x, f# active x -> f# x)
     (f# no x -> f# x, f# mark x -> f# x)
     (chk# no f x -> f# chk mat(f f f f f f f f f f X(), x), f# active x -> active# f x)
     (chk# no f x -> f# chk mat(f f f f f f f f f f X(), x), f# active x -> f# x)
     (tp# mark x -> chk# mat(f f f f f f f f f f X(), x), chk# no c() -> active# c())
     (chk# no f x -> chk# mat(f f f f f f f f f f X(), x), chk# no c() -> active# c())
     (f# active x -> f# x, f# mark x -> f# x)
     (f# active x -> f# x, f# active x -> f# x)
     (f# active x -> f# x, f# active x -> active# f x)
     (f# active x -> f# x, f# no x -> f# x)
     (f# active x -> active# f x, active# f x -> f# f x)}
    EDG:
     {(active# f x -> f# f x, f# no x -> f# x)
      (active# f x -> f# f x, f# active x -> active# f x)
      (active# f x -> f# f x, f# active x -> f# x)
      (active# f x -> f# f x, f# mark x -> f# x)
      (f# mark x -> f# x, f# no x -> f# x)
      (f# mark x -> f# x, f# active x -> active# f x)
      (f# mark x -> f# x, f# active x -> f# x)
      (f# mark x -> f# x, f# mark x -> f# x)
      (f# no x -> f# x, f# no x -> f# x)
      (f# no x -> f# x, f# active x -> active# f x)
      (f# no x -> f# x, f# active x -> f# x)
      (f# no x -> f# x, f# mark x -> f# x)
      (chk# no f x -> f# chk mat(f f f f f f f f f f X(), x), f# active x -> active# f x)
      (chk# no f x -> f# chk mat(f f f f f f f f f f X(), x), f# active x -> f# x)
      (tp# mark x -> chk# mat(f f f f f f f f f f X(), x), chk# no c() -> active# c())
      (chk# no f x -> chk# mat(f f f f f f f f f f X(), x), chk# no c() -> active# c())
      (f# active x -> f# x, f# mark x -> f# x)
      (f# active x -> f# x, f# active x -> f# x)
      (f# active x -> f# x, f# active x -> active# f x)
      (f# active x -> f# x, f# no x -> f# x)
      (f# active x -> active# f x, active# f x -> f# f x)}
     STATUS:
      arrows: 0.981834
      SCCS (1):
       Scc:
        {  f# mark x -> f# x,
         f# active x -> f# x,
         f# active x -> active# f x,
             f# no x -> f# x,
         active# f x -> f# f x}
       
       
       
       
       
       
       
       
       
       
       
       
       
       
       
       
       
       
       
       
       
       
       
       
       
       
       
       
       SCC (5):
        Strict:
         {  f# mark x -> f# x,
          f# active x -> f# x,
          f# active x -> active# f x,
              f# no x -> f# x,
          active# f x -> f# f x}
        Weak:
        {       f mark x -> mark f x,
              f active x -> active f x,
                  f no x -> no f x,
              active f x -> mark f f x,
              chk no f x -> f chk mat(f f f f f f f f f f X(), x),
              chk no c() -> active c(),
         mat(f x, f y()) -> f mat(x, y()),
           mat(f x, c()) -> no c(),
               tp mark x -> tp chk mat(f f f f f f f f f f X(), x)}
        Open