MAYBE
Time: 0.010094
TRS:
 {     active f x -> mark x,
       active f x -> f active x,
         f mark x -> mark f x,
           f ok x -> ok f x,
        f found x -> found f x,
       top mark x -> top check x,
   top active c() -> top mark c(),
      top found x -> top active x,
          check x -> start match(f X(), x),
        check f x -> f check x,
       start ok x -> found x,
  match(f x, f y) -> f match(x, y),
    match(X(), x) -> proper x,
       proper f x -> f proper x,
       proper c() -> ok c()}
 DP:
  DP:
   {     active# f x -> active# x,
         active# f x -> f# active x,
           f# mark x -> f# x,
             f# ok x -> f# x,
          f# found x -> f# x,
         top# mark x -> top# check x,
         top# mark x -> check# x,
     top# active c() -> top# mark c(),
        top# found x -> active# x,
        top# found x -> top# active x,
            check# x -> f# X(),
            check# x -> start# match(f X(), x),
            check# x -> match#(f X(), x),
          check# f x -> f# check x,
          check# f x -> check# x,
    match#(f x, f y) -> f# match(x, y),
    match#(f x, f y) -> match#(x, y),
      match#(X(), x) -> proper# x,
         proper# f x -> f# proper x,
         proper# f x -> proper# x}
  TRS:
  {     active f x -> mark x,
        active f x -> f active x,
          f mark x -> mark f x,
            f ok x -> ok f x,
         f found x -> found f x,
        top mark x -> top check x,
    top active c() -> top mark c(),
       top found x -> top active x,
           check x -> start match(f X(), x),
         check f x -> f check x,
        start ok x -> found x,
   match(f x, f y) -> f match(x, y),
     match(X(), x) -> proper x,
        proper f x -> f proper x,
        proper c() -> ok c()}
  UR:
   {     active f x -> mark x,
         active f x -> f active x,
           f mark x -> mark f x,
             f ok x -> ok f x,
          f found x -> found f x,
            check x -> start match(f X(), x),
          check f x -> f check x,
         start ok x -> found x,
    match(f x, f y) -> f match(x, y),
      match(X(), x) -> proper x,
         proper f x -> f proper x,
         proper c() -> ok c()}
   EDG:
    {(top# mark x -> top# check x, top# found x -> top# active x)
     (top# mark x -> top# check x, top# found x -> active# x)
     (top# mark x -> top# check x, top# mark x -> check# x)
     (top# mark x -> top# check x, top# mark x -> top# check x)
     (check# f x -> f# check x, f# found x -> f# x)
     (check# f x -> f# check x, f# ok x -> f# x)
     (check# f x -> f# check x, f# mark x -> f# x)
     (check# x -> match#(f X(), x), match#(f x, f y) -> match#(x, y))
     (check# x -> match#(f X(), x), match#(f x, f y) -> f# match(x, y))
     (match#(f x, f y) -> f# match(x, y), f# found x -> f# x)
     (match#(f x, f y) -> f# match(x, y), f# ok x -> f# x)
     (match#(f x, f y) -> f# match(x, y), f# mark x -> f# x)
     (active# f x -> active# x, active# f x -> f# active x)
     (active# f x -> active# x, active# f x -> active# x)
     (f# ok x -> f# x, f# found x -> f# x)
     (f# ok x -> f# x, f# ok x -> f# x)
     (f# ok x -> f# x, f# mark x -> f# x)
     (top# mark x -> check# x, check# f x -> check# x)
     (top# mark x -> check# x, check# f x -> f# check x)
     (top# mark x -> check# x, check# x -> match#(f X(), x))
     (top# mark x -> check# x, check# x -> start# match(f X(), x))
     (top# mark x -> check# x, check# x -> f# X())
     (check# f x -> check# x, check# f x -> check# x)
     (check# f x -> check# x, check# f x -> f# check x)
     (check# f x -> check# x, check# x -> match#(f X(), x))
     (check# f x -> check# x, check# x -> start# match(f X(), x))
     (check# f x -> check# x, check# x -> f# X())
     (proper# f x -> proper# x, proper# f x -> proper# x)
     (proper# f x -> proper# x, proper# f x -> f# proper x)
     (match#(f x, f y) -> match#(x, y), match#(X(), x) -> proper# x)
     (match#(f x, f y) -> match#(x, y), match#(f x, f y) -> match#(x, y))
     (match#(f x, f y) -> match#(x, y), match#(f x, f y) -> f# match(x, y))
     (match#(X(), x) -> proper# x, proper# f x -> f# proper x)
     (match#(X(), x) -> proper# x, proper# f x -> proper# x)
     (top# found x -> active# x, active# f x -> active# x)
     (top# found x -> active# x, active# f x -> f# active x)
     (f# found x -> f# x, f# mark x -> f# x)
     (f# found x -> f# x, f# ok x -> f# x)
     (f# found x -> f# x, f# found x -> f# x)
     (f# mark x -> f# x, f# mark x -> f# x)
     (f# mark x -> f# x, f# ok x -> f# x)
     (f# mark x -> f# x, f# found x -> f# x)
     (top# active c() -> top# mark c(), top# mark x -> top# check x)
     (top# active c() -> top# mark c(), top# mark x -> check# x)
     (proper# f x -> f# proper x, f# mark x -> f# x)
     (proper# f x -> f# proper x, f# ok x -> f# x)
     (proper# f x -> f# proper x, f# found x -> f# x)
     (top# found x -> top# active x, top# mark x -> top# check x)
     (top# found x -> top# active x, top# mark x -> check# x)
     (top# found x -> top# active x, top# active c() -> top# mark c())
     (top# found x -> top# active x, top# found x -> active# x)
     (top# found x -> top# active x, top# found x -> top# active x)
     (active# f x -> f# active x, f# mark x -> f# x)
     (active# f x -> f# active x, f# ok x -> f# x)
     (active# f x -> f# active x, f# found x -> f# x)}
    STATUS:
     arrows: 0.862500
     SCCS (6):
      Scc:
       {    top# mark x -> top# check x,
        top# active c() -> top# mark c(),
           top# found x -> top# active x}
      Scc:
       {active# f x -> active# x}
      Scc:
       {check# f x -> check# x}
      Scc:
       {match#(f x, f y) -> match#(x, y)}
      Scc:
       {proper# f x -> proper# x}
      Scc:
       { f# mark x -> f# x,
           f# ok x -> f# x,
        f# found x -> f# x}
      
      SCC (3):
       Strict:
        {    top# mark x -> top# check x,
         top# active c() -> top# mark c(),
            top# found x -> top# active x}
       Weak:
       {     active f x -> mark x,
             active f x -> f active x,
               f mark x -> mark f x,
                 f ok x -> ok f x,
              f found x -> found f x,
             top mark x -> top check x,
         top active c() -> top mark c(),
            top found x -> top active x,
                check x -> start match(f X(), x),
              check f x -> f check x,
             start ok x -> found x,
        match(f x, f y) -> f match(x, y),
          match(X(), x) -> proper x,
             proper f x -> f proper x,
             proper c() -> ok c()}
       Open
      
      SCC (1):
       Strict:
        {active# f x -> active# x}
       Weak:
       {     active f x -> mark x,
             active f x -> f active x,
               f mark x -> mark f x,
                 f ok x -> ok f x,
              f found x -> found f x,
             top mark x -> top check x,
         top active c() -> top mark c(),
            top found x -> top active x,
                check x -> start match(f X(), x),
              check f x -> f check x,
             start ok x -> found x,
        match(f x, f y) -> f match(x, y),
          match(X(), x) -> proper x,
             proper f x -> f proper x,
             proper c() -> ok c()}
       Open
      
      SCC (1):
       Strict:
        {check# f x -> check# x}
       Weak:
       {     active f x -> mark x,
             active f x -> f active x,
               f mark x -> mark f x,
                 f ok x -> ok f x,
              f found x -> found f x,
             top mark x -> top check x,
         top active c() -> top mark c(),
            top found x -> top active x,
                check x -> start match(f X(), x),
              check f x -> f check x,
             start ok x -> found x,
        match(f x, f y) -> f match(x, y),
          match(X(), x) -> proper x,
             proper f x -> f proper x,
             proper c() -> ok c()}
       Open
      
      
      SCC (1):
       Strict:
        {match#(f x, f y) -> match#(x, y)}
       Weak:
       {     active f x -> mark x,
             active f x -> f active x,
               f mark x -> mark f x,
                 f ok x -> ok f x,
              f found x -> found f x,
             top mark x -> top check x,
         top active c() -> top mark c(),
            top found x -> top active x,
                check x -> start match(f X(), x),
              check f x -> f check x,
             start ok x -> found x,
        match(f x, f y) -> f match(x, y),
          match(X(), x) -> proper x,
             proper f x -> f proper x,
             proper c() -> ok c()}
       Open
      
      SCC (1):
       Strict:
        {proper# f x -> proper# x}
       Weak:
       {     active f x -> mark x,
             active f x -> f active x,
               f mark x -> mark f x,
                 f ok x -> ok f x,
              f found x -> found f x,
             top mark x -> top check x,
         top active c() -> top mark c(),
            top found x -> top active x,
                check x -> start match(f X(), x),
              check f x -> f check x,
             start ok x -> found x,
        match(f x, f y) -> f match(x, y),
          match(X(), x) -> proper x,
             proper f x -> f proper x,
             proper c() -> ok c()}
       Open
      
      
      
      
      
      SCC (3):
       Strict:
        { f# mark x -> f# x,
            f# ok x -> f# x,
         f# found x -> f# x}
       Weak:
       {     active f x -> mark x,
             active f x -> f active x,
               f mark x -> mark f x,
                 f ok x -> ok f x,
              f found x -> found f x,
             top mark x -> top check x,
         top active c() -> top mark c(),
            top found x -> top active x,
                check x -> start match(f X(), x),
              check f x -> f check x,
             start ok x -> found x,
        match(f x, f y) -> f match(x, y),
          match(X(), x) -> proper x,
             proper f x -> f proper x,
             proper c() -> ok c()}
       Open