Input TRS:
    1: app(app(app(comp(),f),g),x) -> app(f,app(g,x))
    2: app(twice(),f) -> app(app(comp(),f),f)
Number of strict rules: 2
Direct Order(PosReal,>,Poly) ... failed.
Freezing app
1: app❆3_comp(f,g,x) -> app(f,app(g,x))
2: app❆1_twice(f) -> app❆2_comp(f,f)
3: app(twice(),_1) ->= app❆1_twice(_1)
4: app(comp(),_1) ->= app❆1_comp(_1)
5: app(app❆1_comp(_1),_2) ->= app❆2_comp(_1,_2)
6: app(app❆2_comp(_1,_2),_3) ->= app❆3_comp(_1,_2,_3)
Number of strict rules: 2
Direct Order(PosReal,>,Poly) ... failed.
Dependency Pairs:
   #1: #app(app❆2_comp(_1,_2),_3) ->? #app❆3_comp(_1,_2,_3)
   #2: #app(twice(),_1) ->? #app❆1_twice(_1)
   #3: #app❆3_comp(f,g,x) -> #app(f,app(g,x))
   #4: #app❆3_comp(f,g,x) -> #app(g,x)
Number of SCCs: 1, DPs: 3, edges: 4
	SCC { #1 #3 #4 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 twice()	weight: 0
app❆2_comp(x1,x2)	weight: (/ 1 2) + x1 + x2
app❆1_comp(x1)	weight: (/ 1 4) + x1
 #app(x1,x2)	weight: x1
#app❆3_comp(x1,x2,x3)	weight: (/ 1 8) + x1 + x2
#app❆1_twice(x1)	weight: 0
app❆3_comp(x1,x2,x3)	weight: x3
app❆1_twice(x1)	weight: (/ 1 4)
  comp()	weight: 0
   app(x1,x2)	weight: (/ 1 8) + x1
    Usable rules: { }
    Removed DPs: #1 #3 #4
Number of SCCs: 0, DPs: 0, edges: 0
YES