MAYBE

Problem:
 app(app(app(if(),true()),x),y) -> x
 app(app(app(if(),false()),x),y) -> y
 app(app(app(until(),p),f),x) -> app(app(app(if(),app(p,x)),x),app(app(app(until(),p),f),app(f,x)))

Proof:
 Uncurry Processor:
  if3(true(),x,y) -> x
  if3(false(),x,y) -> y
  until3(p,f,x) -> if3(app(p,x),x,until3(p,f,app(f,x)))
  app(if2(x5,x4),x6) -> if3(x5,x4,x6)
  app(if1(x5),x6) -> if2(x5,x6)
  app(if(),x6) -> if1(x6)
  app(until2(x5,x4),x6) -> until3(x5,x4,x6)
  app(until1(x5),x6) -> until2(x5,x6)
  app(until(),x6) -> until1(x6)
  DP Processor:
   DPs:
    until{3,#}(p,f,x) -> app#(f,x)
    until{3,#}(p,f,x) -> until{3,#}(p,f,app(f,x))
    until{3,#}(p,f,x) -> app#(p,x)
    until{3,#}(p,f,x) -> if{3,#}(app(p,x),x,until3(p,f,app(f,x)))
    app#(if2(x5,x4),x6) -> if{3,#}(x5,x4,x6)
    app#(until2(x5,x4),x6) -> until{3,#}(x5,x4,x6)
   TRS:
    if3(true(),x,y) -> x
    if3(false(),x,y) -> y
    until3(p,f,x) -> if3(app(p,x),x,until3(p,f,app(f,x)))
    app(if2(x5,x4),x6) -> if3(x5,x4,x6)
    app(if1(x5),x6) -> if2(x5,x6)
    app(if(),x6) -> if1(x6)
    app(until2(x5,x4),x6) -> until3(x5,x4,x6)
    app(until1(x5),x6) -> until2(x5,x6)
    app(until(),x6) -> until1(x6)
   TDG Processor:
    DPs:
     until{3,#}(p,f,x) -> app#(f,x)
     until{3,#}(p,f,x) -> until{3,#}(p,f,app(f,x))
     until{3,#}(p,f,x) -> app#(p,x)
     until{3,#}(p,f,x) -> if{3,#}(app(p,x),x,until3(p,f,app(f,x)))
     app#(if2(x5,x4),x6) -> if{3,#}(x5,x4,x6)
     app#(until2(x5,x4),x6) -> until{3,#}(x5,x4,x6)
    TRS:
     if3(true(),x,y) -> x
     if3(false(),x,y) -> y
     until3(p,f,x) -> if3(app(p,x),x,until3(p,f,app(f,x)))
     app(if2(x5,x4),x6) -> if3(x5,x4,x6)
     app(if1(x5),x6) -> if2(x5,x6)
     app(if(),x6) -> if1(x6)
     app(until2(x5,x4),x6) -> until3(x5,x4,x6)
     app(until1(x5),x6) -> until2(x5,x6)
     app(until(),x6) -> until1(x6)
    graph:
     app#(until2(x5,x4),x6) -> until{3,#}(x5,x4,x6) ->
     until{3,#}(p,f,x) -> if{3,#}(app(p,x),x,until3(p,f,app(f,x)))
     app#(until2(x5,x4),x6) -> until{3,#}(x5,x4,x6) ->
     until{3,#}(p,f,x) -> app#(p,x)
     app#(until2(x5,x4),x6) -> until{3,#}(x5,x4,x6) ->
     until{3,#}(p,f,x) -> until{3,#}(p,f,app(f,x))
     app#(until2(x5,x4),x6) -> until{3,#}(x5,x4,x6) ->
     until{3,#}(p,f,x) -> app#(f,x)
     until{3,#}(p,f,x) -> app#(p,x) ->
     app#(until2(x5,x4),x6) -> until{3,#}(x5,x4,x6)
     until{3,#}(p,f,x) -> app#(p,x) ->
     app#(if2(x5,x4),x6) -> if{3,#}(x5,x4,x6)
     until{3,#}(p,f,x) -> app#(f,x) ->
     app#(until2(x5,x4),x6) -> until{3,#}(x5,x4,x6)
     until{3,#}(p,f,x) -> app#(f,x) ->
     app#(if2(x5,x4),x6) -> if{3,#}(x5,x4,x6)
     until{3,#}(p,f,x) -> until{3,#}(p,f,app(f,x)) ->
     until{3,#}(p,f,x) -> if{3,#}(app(p,x),x,until3(p,f,app(f,x)))
     until{3,#}(p,f,x) -> until{3,#}(p,f,app(f,x)) ->
     until{3,#}(p,f,x) -> app#(p,x)
     until{3,#}(p,f,x) -> until{3,#}(p,f,app(f,x)) ->
     until{3,#}(p,f,x) -> until{3,#}(p,f,app(f,x))
     until{3,#}(p,f,x) -> until{3,#}(p,f,app(f,x)) -> until{3,#}(p,f,x) -> app#(f,x)
    SCC Processor:
     #sccs: 1
     #rules: 4
     #arcs: 12/36
     DPs:
      app#(until2(x5,x4),x6) -> until{3,#}(x5,x4,x6)
      until{3,#}(p,f,x) -> app#(f,x)
      until{3,#}(p,f,x) -> until{3,#}(p,f,app(f,x))
      until{3,#}(p,f,x) -> app#(p,x)
     TRS:
      if3(true(),x,y) -> x
      if3(false(),x,y) -> y
      until3(p,f,x) -> if3(app(p,x),x,until3(p,f,app(f,x)))
      app(if2(x5,x4),x6) -> if3(x5,x4,x6)
      app(if1(x5),x6) -> if2(x5,x6)
      app(if(),x6) -> if1(x6)
      app(until2(x5,x4),x6) -> until3(x5,x4,x6)
      app(until1(x5),x6) -> until2(x5,x6)
      app(until(),x6) -> until1(x6)
     Arctic Interpretation Processor:
      dimension: 1
      interpretation:
       [app#](x0, x1) = 4x0,
       
       [until{3,#}](x0, x1, x2) = 5x0 + 4x1,
       
       [until1](x0) = x0 + 5,
       
       [until3](x0, x1, x2) = x0 + 1x1 + x2 + 0,
       
       [until2](x0, x1) = 1x0 + x1 + 0,
       
       [if1](x0) = x0 + 3,
       
       [if3](x0, x1, x2) = x1 + x2,
       
       [if2](x0, x1) = x1 + 4,
       
       [until] = 4,
       
       [false] = 6,
       
       [app](x0, x1) = 1x0 + x1 + 0,
       
       [true] = 5,
       
       [if] = 2
      orientation:
       app#(until2(x5,x4),x6) = 4x4 + 5x5 + 4 >= 4x4 + 5x5 = until{3,#}(x5,x4,x6)
       
       until{3,#}(p,f,x) = 4f + 5p >= 4f = app#(f,x)
       
       until{3,#}(p,f,x) = 4f + 5p >= 4f + 5p = until{3,#}(p,f,app(f,x))
       
       until{3,#}(p,f,x) = 4f + 5p >= 4p = app#(p,x)
       
       if3(true(),x,y) = x + y >= x = x
       
       if3(false(),x,y) = x + y >= y = y
       
       until3(p,f,x) = 1f + p + x + 0 >= 1f + p + x + 0 = if3(app(p,x),x,until3(p,f,app(f,x)))
       
       app(if2(x5,x4),x6) = 1x4 + x6 + 5 >= x4 + x6 = if3(x5,x4,x6)
       
       app(if1(x5),x6) = 1x5 + x6 + 4 >= x6 + 4 = if2(x5,x6)
       
       app(if(),x6) = x6 + 3 >= x6 + 3 = if1(x6)
       
       app(until2(x5,x4),x6) = 1x4 + 2x5 + x6 + 1 >= 1x4 + x5 + x6 + 0 = until3(x5,x4,x6)
       
       app(until1(x5),x6) = 1x5 + x6 + 6 >= 1x5 + x6 + 0 = until2(x5,x6)
       
       app(until(),x6) = x6 + 5 >= x6 + 5 = until1(x6)
      problem:
       DPs:
        app#(until2(x5,x4),x6) -> until{3,#}(x5,x4,x6)
        until{3,#}(p,f,x) -> app#(f,x)
        until{3,#}(p,f,x) -> until{3,#}(p,f,app(f,x))
       TRS:
        if3(true(),x,y) -> x
        if3(false(),x,y) -> y
        until3(p,f,x) -> if3(app(p,x),x,until3(p,f,app(f,x)))
        app(if2(x5,x4),x6) -> if3(x5,x4,x6)
        app(if1(x5),x6) -> if2(x5,x6)
        app(if(),x6) -> if1(x6)
        app(until2(x5,x4),x6) -> until3(x5,x4,x6)
        app(until1(x5),x6) -> until2(x5,x6)
        app(until(),x6) -> until1(x6)
      Subterm Criterion Processor:
       simple projection:
        pi(until{3,#}) = 1
        pi(app#) = 0
       problem:
        DPs:
         until{3,#}(p,f,x) -> app#(f,x)
         until{3,#}(p,f,x) -> until{3,#}(p,f,app(f,x))
        TRS:
         if3(true(),x,y) -> x
         if3(false(),x,y) -> y
         until3(p,f,x) -> if3(app(p,x),x,until3(p,f,app(f,x)))
         app(if2(x5,x4),x6) -> if3(x5,x4,x6)
         app(if1(x5),x6) -> if2(x5,x6)
         app(if(),x6) -> if1(x6)
         app(until2(x5,x4),x6) -> until3(x5,x4,x6)
         app(until1(x5),x6) -> until2(x5,x6)
         app(until(),x6) -> until1(x6)
       SCC Processor:
        #sccs: 1
        #rules: 1
        #arcs: 8/4
        DPs:
         until{3,#}(p,f,x) -> until{3,#}(p,f,app(f,x))
        TRS:
         if3(true(),x,y) -> x
         if3(false(),x,y) -> y
         until3(p,f,x) -> if3(app(p,x),x,until3(p,f,app(f,x)))
         app(if2(x5,x4),x6) -> if3(x5,x4,x6)
         app(if1(x5),x6) -> if2(x5,x6)
         app(if(),x6) -> if1(x6)
         app(until2(x5,x4),x6) -> until3(x5,x4,x6)
         app(until1(x5),x6) -> until2(x5,x6)
         app(until(),x6) -> until1(x6)
        Open