MAYBE

Problem:
 app(app(app(compose(),f),g),x) -> app(g,app(f,x))
 app(reverse(),l) -> app(app(reverse2(),l),nil())
 app(app(reverse2(),nil()),l) -> l
 app(app(reverse2(),app(app(cons(),x),xs)),l) -> app(app(reverse2(),xs),app(app(cons(),x),l))
 app(hd(),app(app(cons(),x),xs)) -> x
 app(tl(),app(app(cons(),x),xs)) -> xs
 last() -> app(app(compose(),hd()),reverse())
 init() -> app(app(compose(),reverse()),app(app(compose(),tl()),reverse()))

Proof:
 RT Transformation Processor:
  strict:
   app(app(app(compose(),f),g),x) -> app(g,app(f,x))
   app(reverse(),l) -> app(app(reverse2(),l),nil())
   app(app(reverse2(),nil()),l) -> l
   app(app(reverse2(),app(app(cons(),x),xs)),l) -> app(app(reverse2(),xs),app(app(cons(),x),l))
   app(hd(),app(app(cons(),x),xs)) -> x
   app(tl(),app(app(cons(),x),xs)) -> xs
   last() -> app(app(compose(),hd()),reverse())
   init() -> app(app(compose(),reverse()),app(app(compose(),tl()),reverse()))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [init] = 0,
    
    [last] = 0,
    
    [tl] = 27,
    
    [hd] = 2,
    
    [cons] = 7,
    
    [nil] = 11,
    
    [reverse2] = 25,
    
    [reverse] = 16,
    
    [app](x0, x1) = x0 + x1,
    
    [compose] = 0
   orientation:
    app(app(app(compose(),f),g),x) = f + g + x >= f + g + x = app(g,app(f,x))
    
    app(reverse(),l) = l + 16 >= l + 36 = app(app(reverse2(),l),nil())
    
    app(app(reverse2(),nil()),l) = l + 36 >= l = l
    
    app(app(reverse2(),app(app(cons(),x),xs)),l) = l + x + xs + 32 >= l + x + xs + 32 = app(app(reverse2(),xs),app(app(cons(),x),l))
    
    app(hd(),app(app(cons(),x),xs)) = x + xs + 9 >= x = x
    
    app(tl(),app(app(cons(),x),xs)) = x + xs + 34 >= xs = xs
    
    last() = 0 >= 18 = app(app(compose(),hd()),reverse())
    
    init() = 0 >= 59 = app(app(compose(),reverse()),app(app(compose(),tl()),reverse()))
   problem:
    strict:
     app(app(app(compose(),f),g),x) -> app(g,app(f,x))
     app(reverse(),l) -> app(app(reverse2(),l),nil())
     app(app(reverse2(),app(app(cons(),x),xs)),l) -> app(app(reverse2(),xs),app(app(cons(),x),l))
     last() -> app(app(compose(),hd()),reverse())
     init() -> app(app(compose(),reverse()),app(app(compose(),tl()),reverse()))
    weak:
     app(app(reverse2(),nil()),l) -> l
     app(hd(),app(app(cons(),x),xs)) -> x
     app(tl(),app(app(cons(),x),xs)) -> xs
   Matrix Interpretation Processor:
    dimension: 1
    interpretation:
     [init] = 31,
     
     [last] = 0,
     
     [tl] = 14,
     
     [hd] = 4,
     
     [cons] = 26,
     
     [nil] = 0,
     
     [reverse2] = 0,
     
     [reverse] = 8,
     
     [app](x0, x1) = x0 + x1,
     
     [compose] = 0
    orientation:
     app(app(app(compose(),f),g),x) = f + g + x >= f + g + x = app(g,app(f,x))
     
     app(reverse(),l) = l + 8 >= l = app(app(reverse2(),l),nil())
     
     app(app(reverse2(),app(app(cons(),x),xs)),l) = l + x + xs + 26 >= l + x + xs + 26 = app(app(reverse2(),xs),app(app(cons(),x),l))
     
     last() = 0 >= 12 = app(app(compose(),hd()),reverse())
     
     init() = 31 >= 30 = app(app(compose(),reverse()),app(app(compose(),tl()),reverse()))
     
     app(app(reverse2(),nil()),l) = l >= l = l
     
     app(hd(),app(app(cons(),x),xs)) = x + xs + 30 >= x = x
     
     app(tl(),app(app(cons(),x),xs)) = x + xs + 40 >= xs = xs
    problem:
     strict:
      app(app(app(compose(),f),g),x) -> app(g,app(f,x))
      app(app(reverse2(),app(app(cons(),x),xs)),l) -> app(app(reverse2(),xs),app(app(cons(),x),l))
      last() -> app(app(compose(),hd()),reverse())
     weak:
      app(reverse(),l) -> app(app(reverse2(),l),nil())
      init() -> app(app(compose(),reverse()),app(app(compose(),tl()),reverse()))
      app(app(reverse2(),nil()),l) -> l
      app(hd(),app(app(cons(),x),xs)) -> x
      app(tl(),app(app(cons(),x),xs)) -> xs
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [init] = 19,
      
      [last] = 4,
      
      [tl] = 17,
      
      [hd] = 0,
      
      [cons] = 3,
      
      [nil] = 0,
      
      [reverse2] = 1,
      
      [reverse] = 1,
      
      [app](x0, x1) = x0 + x1,
      
      [compose] = 0
     orientation:
      app(app(app(compose(),f),g),x) = f + g + x >= f + g + x = app(g,app(f,x))
      
      app(app(reverse2(),app(app(cons(),x),xs)),l) = l + x + xs + 4 >= l + x + xs + 4 = app(app(reverse2(),xs),app(app(cons(),x),l))
      
      last() = 4 >= 1 = app(app(compose(),hd()),reverse())
      
      app(reverse(),l) = l + 1 >= l + 1 = app(app(reverse2(),l),nil())
      
      init() = 19 >= 19 = app(app(compose(),reverse()),app(app(compose(),tl()),reverse()))
      
      app(app(reverse2(),nil()),l) = l + 1 >= l = l
      
      app(hd(),app(app(cons(),x),xs)) = x + xs + 3 >= x = x
      
      app(tl(),app(app(cons(),x),xs)) = x + xs + 20 >= xs = xs
     problem:
      strict:
       app(app(app(compose(),f),g),x) -> app(g,app(f,x))
       app(app(reverse2(),app(app(cons(),x),xs)),l) -> app(app(reverse2(),xs),app(app(cons(),x),l))
      weak:
       last() -> app(app(compose(),hd()),reverse())
       app(reverse(),l) -> app(app(reverse2(),l),nil())
       init() -> app(app(compose(),reverse()),app(app(compose(),tl()),reverse()))
       app(app(reverse2(),nil()),l) -> l
       app(hd(),app(app(cons(),x),xs)) -> x
       app(tl(),app(app(cons(),x),xs)) -> xs
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [init] = 20,
       
       [last] = 16,
       
       [tl] = 0,
       
       [hd] = 1,
       
       [cons] = 9,
       
       [nil] = 0,
       
       [reverse2] = 2,
       
       [reverse] = 4,
       
       [app](x0, x1) = x0 + x1 + 1,
       
       [compose] = 4
      orientation:
       app(app(app(compose(),f),g),x) = f + g + x + 7 >= f + g + x + 2 = app(g,app(f,x))
       
       app(app(reverse2(),app(app(cons(),x),xs)),l) = l + x + xs + 15 >= l + x + xs + 15 = app(app(reverse2(),xs),app(app(cons(),x),l))
       
       last() = 16 >= 11 = app(app(compose(),hd()),reverse())
       
       app(reverse(),l) = l + 5 >= l + 4 = app(app(reverse2(),l),nil())
       
       init() = 20 >= 20 = app(app(compose(),reverse()),app(app(compose(),tl()),reverse()))
       
       app(app(reverse2(),nil()),l) = l + 4 >= l = l
       
       app(hd(),app(app(cons(),x),xs)) = x + xs + 13 >= x = x
       
       app(tl(),app(app(cons(),x),xs)) = x + xs + 12 >= xs = xs
      problem:
       strict:
        app(app(reverse2(),app(app(cons(),x),xs)),l) ->
        app(app(reverse2(),xs),app(app(cons(),x),l))
       weak:
        app(app(app(compose(),f),g),x) -> app(g,app(f,x))
        last() -> app(app(compose(),hd()),reverse())
        app(reverse(),l) -> app(app(reverse2(),l),nil())
        init() -> app(app(compose(),reverse()),app(app(compose(),tl()),reverse()))
        app(app(reverse2(),nil()),l) -> l
        app(hd(),app(app(cons(),x),xs)) -> x
        app(tl(),app(app(cons(),x),xs)) -> xs
      Open