Input TRS:
    1: app(app(app(fold(),f),nil()),x) -> x
    2: app(app(app(fold(),f),app(app(cons(),h),t)),x) -> app(app(app(fold(),f),t),app(app(f,x),h))
    3: app(sum(),l) -> app(app(app(fold(),add()),l),0())
    4: app(app(app(fold(),mul()),l),1()) -> app(prod(),l)
Number of strict rules: 4
Direct Order(PosReal,>,Poly) ... failed.
Freezing app
1: app❆3_fold(f,nil(),x) -> x
2: app❆3_fold(f,app❆2_cons(h,t),x) -> app❆3_fold(f,t,app(app(f,x),h))
3: app❆1_sum(l) -> app❆3_fold(add(),l,0())
4: app❆3_fold(mul(),l,1()) -> app❆1_prod(l)
5: app(prod(),_1) ->= app❆1_prod(_1)
6: app(cons(),_1) ->= app❆1_cons(_1)
7: app(app❆1_cons(_1),_2) ->= app❆2_cons(_1,_2)
8: app(fold(),_1) ->= app❆1_fold(_1)
9: app(app❆1_fold(_1),_2) ->= app❆2_fold(_1,_2)
10: app(app❆2_fold(_1,_2),_3) ->= app❆3_fold(_1,_2,_3)
11: app(sum(),_1) ->= app❆1_sum(_1)
Number of strict rules: 4
Direct Order(PosReal,>,Poly) ... failed.
Dependency Pairs:
   #1: #app❆3_fold(f,app❆2_cons(h,t),x) -> #app❆3_fold(f,t,app(app(f,x),h))
   #2: #app❆3_fold(f,app❆2_cons(h,t),x) -> #app(app(f,x),h)
   #3: #app❆3_fold(f,app❆2_cons(h,t),x) -> #app(f,x)
   #4: #app(sum(),_1) ->? #app❆1_sum(_1)
   #5: #app(app❆2_fold(_1,_2),_3) ->? #app❆3_fold(_1,_2,_3)
   #6: #app❆1_sum(l) -> #app❆3_fold(add(),l,0())
Number of SCCs: 1, DPs: 6, edges: 14
	SCC { #1..6 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... Order(PosReal,>,Sum-Sum; PosReal,≥,Sum-Sum)... Order(PosReal,>,Sum-Sum; NegReal,≥,Sum)... Order(PosReal,>,MaxSum-Sum; NegReal,≥,Sum)... succeeded.
   mul()	weight: (/ 1 4); (- (/ 1 4))
     1()	weight: (/ 1 4); (- (/ 1 4))
  prod()	weight: (/ 1 4); (- (/ 1 2))
app❆1_sum(x1)	weight: max{0, x1_1}; 0
app❆3_fold(x1,x2,x3)	weight: max{0, (- (/ 105143 4)) + x1_2, x1_1, (- (/ 1 4)) + x2_2, x2_1, x3_1}; 0
#app❆3_fold(x1,x2,x3)	weight: max{0, (/ 1 2) + x1_2, (/ 1 4) + x3_2}; x1_2
#app❆1_sum(x1)	weight: max{0, (- (/ 1 2)) + x1_2}; (- (/ 3 4))
   sum()	weight: (/ 1 2); 0
app❆1_prod(x1)	weight: max{0, -26286 + x1_2}; (- (/ 1 2))
app❆2_fold(x1,x2)	weight: max{0, -26286 + x1_2, x1_1, -26286 + x2_2, x2_1}; 0
     0()	weight: 0; (- (/ 1 4))
   nil()	weight: 0; (- (/ 1 4))
 #app(x1,x2)	weight: max{0, (/ 1 2) + x1_2}; x1_2
  fold()	weight: (/ 1 4); 0
  cons()	weight: (/ 1 4); (- (/ 1 4))
app❆2_cons(x1,x2)	weight: max{0, -26286 + x1_2, x1_1, x2_1}; (- (/ 1 2))
   add()	weight: 0; (- (/ 3 4))
app❆1_cons(x1)	weight: max{0, x1_1}; (- (/ 1 2))
app❆1_fold(x1)	weight: max{0, x1_1}; 0
   app(x1,x2)	weight: max{0, (- (/ 105143 4)) + x1_2, x1_1, (- (/ 105145 4)) + x2_2, x2_1}; x1_2
    Usable rules: { 1..11 }
    Removed DPs: #4
Number of SCCs: 1, DPs: 4, edges: 8
	SCC { #1..3 #5 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... Order(PosReal,>,Sum-Sum; PosReal,≥,Sum-Sum)... Order(PosReal,>,Sum-Sum; NegReal,≥,Sum)... Order(PosReal,>,MaxSum-Sum; NegReal,≥,Sum)... failed.
Removing edges: failed.
Finding a loop...  failed.
MAYBE