MAYBE
Time: 0.005705
TRS:
 {app(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app(app(app(branch(), app(f, x)), app(app(mapbt(), f), l)), app(app(mapbt(), f), r)),
                    app(app(mapbt(), f), app(leaf(), x)) -> app(leaf(), app(f, x))}
 DP:
  DP:
   {app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(f, x),
    app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(app(branch(), app(f, x)), app(app(mapbt(), f), l)), app(app(mapbt(), f), r)),
    app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), l),
    app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), r),
    app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(branch(), app(f, x)), app(app(mapbt(), f), l)),
    app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(branch(), app(f, x)),
                      app#(app(mapbt(), f), app(leaf(), x)) -> app#(f, x),
                      app#(app(mapbt(), f), app(leaf(), x)) -> app#(leaf(), app(f, x))}
  TRS:
  {app(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app(app(app(branch(), app(f, x)), app(app(mapbt(), f), l)), app(app(mapbt(), f), r)),
                     app(app(mapbt(), f), app(leaf(), x)) -> app(leaf(), app(f, x))}
  EDG:
   {(app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(f, x), app#(app(mapbt(), f), app(leaf(), x)) -> app#(leaf(), app(f, x)))
    (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(f, x), app#(app(mapbt(), f), app(leaf(), x)) -> app#(f, x))
    (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(f, x), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(branch(), app(f, x)))
    (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(f, x), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(branch(), app(f, x)), app(app(mapbt(), f), l)))
    (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(f, x), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), r))
    (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(f, x), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), l))
    (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(f, x), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(app(branch(), app(f, x)), app(app(mapbt(), f), l)), app(app(mapbt(), f), r)))
    (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(f, x), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(f, x))
    (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), l), app#(app(mapbt(), f), app(leaf(), x)) -> app#(leaf(), app(f, x)))
    (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), l), app#(app(mapbt(), f), app(leaf(), x)) -> app#(f, x))
    (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), l), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(branch(), app(f, x)))
    (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), l), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(branch(), app(f, x)), app(app(mapbt(), f), l)))
    (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), l), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), r))
    (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), l), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), l))
    (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), l), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(app(branch(), app(f, x)), app(app(mapbt(), f), l)), app(app(mapbt(), f), r)))
    (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), l), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(f, x))
    (app#(app(mapbt(), f), app(leaf(), x)) -> app#(f, x), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(f, x))
    (app#(app(mapbt(), f), app(leaf(), x)) -> app#(f, x), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(app(branch(), app(f, x)), app(app(mapbt(), f), l)), app(app(mapbt(), f), r)))
    (app#(app(mapbt(), f), app(leaf(), x)) -> app#(f, x), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), l))
    (app#(app(mapbt(), f), app(leaf(), x)) -> app#(f, x), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), r))
    (app#(app(mapbt(), f), app(leaf(), x)) -> app#(f, x), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(branch(), app(f, x)), app(app(mapbt(), f), l)))
    (app#(app(mapbt(), f), app(leaf(), x)) -> app#(f, x), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(branch(), app(f, x)))
    (app#(app(mapbt(), f), app(leaf(), x)) -> app#(f, x), app#(app(mapbt(), f), app(leaf(), x)) -> app#(f, x))
    (app#(app(mapbt(), f), app(leaf(), x)) -> app#(f, x), app#(app(mapbt(), f), app(leaf(), x)) -> app#(leaf(), app(f, x)))
    (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), r), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(f, x))
    (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), r), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(app(branch(), app(f, x)), app(app(mapbt(), f), l)), app(app(mapbt(), f), r)))
    (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), r), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), l))
    (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), r), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), r))
    (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), r), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(branch(), app(f, x)), app(app(mapbt(), f), l)))
    (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), r), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(branch(), app(f, x)))
    (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), r), app#(app(mapbt(), f), app(leaf(), x)) -> app#(f, x))
    (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), r), app#(app(mapbt(), f), app(leaf(), x)) -> app#(leaf(), app(f, x)))}
   EDG:
    {(app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(f, x), app#(app(mapbt(), f), app(leaf(), x)) -> app#(leaf(), app(f, x)))
     (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(f, x), app#(app(mapbt(), f), app(leaf(), x)) -> app#(f, x))
     (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(f, x), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(branch(), app(f, x)))
     (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(f, x), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(branch(), app(f, x)), app(app(mapbt(), f), l)))
     (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(f, x), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), r))
     (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(f, x), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), l))
     (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(f, x), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(app(branch(), app(f, x)), app(app(mapbt(), f), l)), app(app(mapbt(), f), r)))
     (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(f, x), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(f, x))
     (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), l), app#(app(mapbt(), f), app(leaf(), x)) -> app#(leaf(), app(f, x)))
     (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), l), app#(app(mapbt(), f), app(leaf(), x)) -> app#(f, x))
     (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), l), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(branch(), app(f, x)))
     (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), l), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(branch(), app(f, x)), app(app(mapbt(), f), l)))
     (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), l), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), r))
     (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), l), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), l))
     (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), l), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(app(branch(), app(f, x)), app(app(mapbt(), f), l)), app(app(mapbt(), f), r)))
     (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), l), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(f, x))
     (app#(app(mapbt(), f), app(leaf(), x)) -> app#(f, x), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(f, x))
     (app#(app(mapbt(), f), app(leaf(), x)) -> app#(f, x), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(app(branch(), app(f, x)), app(app(mapbt(), f), l)), app(app(mapbt(), f), r)))
     (app#(app(mapbt(), f), app(leaf(), x)) -> app#(f, x), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), l))
     (app#(app(mapbt(), f), app(leaf(), x)) -> app#(f, x), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), r))
     (app#(app(mapbt(), f), app(leaf(), x)) -> app#(f, x), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(branch(), app(f, x)), app(app(mapbt(), f), l)))
     (app#(app(mapbt(), f), app(leaf(), x)) -> app#(f, x), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(branch(), app(f, x)))
     (app#(app(mapbt(), f), app(leaf(), x)) -> app#(f, x), app#(app(mapbt(), f), app(leaf(), x)) -> app#(f, x))
     (app#(app(mapbt(), f), app(leaf(), x)) -> app#(f, x), app#(app(mapbt(), f), app(leaf(), x)) -> app#(leaf(), app(f, x)))
     (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), r), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(f, x))
     (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), r), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(app(branch(), app(f, x)), app(app(mapbt(), f), l)), app(app(mapbt(), f), r)))
     (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), r), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), l))
     (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), r), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), r))
     (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), r), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(branch(), app(f, x)), app(app(mapbt(), f), l)))
     (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), r), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(branch(), app(f, x)))
     (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), r), app#(app(mapbt(), f), app(leaf(), x)) -> app#(f, x))
     (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), r), app#(app(mapbt(), f), app(leaf(), x)) -> app#(leaf(), app(f, x)))}
    EDG:
     {(app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(f, x), app#(app(mapbt(), f), app(leaf(), x)) -> app#(leaf(), app(f, x)))
      (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(f, x), app#(app(mapbt(), f), app(leaf(), x)) -> app#(f, x))
      (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(f, x), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(branch(), app(f, x)))
      (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(f, x), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(branch(), app(f, x)), app(app(mapbt(), f), l)))
      (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(f, x), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), r))
      (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(f, x), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), l))
      (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(f, x), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(app(branch(), app(f, x)), app(app(mapbt(), f), l)), app(app(mapbt(), f), r)))
      (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(f, x), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(f, x))
      (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), l), app#(app(mapbt(), f), app(leaf(), x)) -> app#(leaf(), app(f, x)))
      (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), l), app#(app(mapbt(), f), app(leaf(), x)) -> app#(f, x))
      (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), l), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(branch(), app(f, x)))
      (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), l), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(branch(), app(f, x)), app(app(mapbt(), f), l)))
      (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), l), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), r))
      (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), l), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), l))
      (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), l), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(app(branch(), app(f, x)), app(app(mapbt(), f), l)), app(app(mapbt(), f), r)))
      (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), l), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(f, x))
      (app#(app(mapbt(), f), app(leaf(), x)) -> app#(f, x), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(f, x))
      (app#(app(mapbt(), f), app(leaf(), x)) -> app#(f, x), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(app(branch(), app(f, x)), app(app(mapbt(), f), l)), app(app(mapbt(), f), r)))
      (app#(app(mapbt(), f), app(leaf(), x)) -> app#(f, x), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), l))
      (app#(app(mapbt(), f), app(leaf(), x)) -> app#(f, x), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), r))
      (app#(app(mapbt(), f), app(leaf(), x)) -> app#(f, x), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(branch(), app(f, x)), app(app(mapbt(), f), l)))
      (app#(app(mapbt(), f), app(leaf(), x)) -> app#(f, x), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(branch(), app(f, x)))
      (app#(app(mapbt(), f), app(leaf(), x)) -> app#(f, x), app#(app(mapbt(), f), app(leaf(), x)) -> app#(f, x))
      (app#(app(mapbt(), f), app(leaf(), x)) -> app#(f, x), app#(app(mapbt(), f), app(leaf(), x)) -> app#(leaf(), app(f, x)))
      (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), r), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(f, x))
      (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), r), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(app(branch(), app(f, x)), app(app(mapbt(), f), l)), app(app(mapbt(), f), r)))
      (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), r), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), l))
      (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), r), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), r))
      (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), r), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(branch(), app(f, x)), app(app(mapbt(), f), l)))
      (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), r), app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(branch(), app(f, x)))
      (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), r), app#(app(mapbt(), f), app(leaf(), x)) -> app#(f, x))
      (app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), r), app#(app(mapbt(), f), app(leaf(), x)) -> app#(leaf(), app(f, x)))}
     STATUS:
      arrows: 0.500000
      SCCS (1):
       Scc:
        {app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(f, x),
         app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), l),
         app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), r),
                           app#(app(mapbt(), f), app(leaf(), x)) -> app#(f, x)}
       
       SCC (4):
        Strict:
         {app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(f, x),
          app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), l),
          app#(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app#(app(mapbt(), f), r),
                            app#(app(mapbt(), f), app(leaf(), x)) -> app#(f, x)}
        Weak:
        {app(app(mapbt(), f), app(app(app(branch(), x), l), r)) -> app(app(app(branch(), app(f, x)), app(app(mapbt(), f), l)), app(app(mapbt(), f), r)),
                           app(app(mapbt(), f), app(leaf(), x)) -> app(leaf(), app(f, x))}
        Open