Input TRS:
    1: h(|1|()) -> h(|0|())
    2: h(|2|()) -> h(|1|())
    3: f(|0|(),X) -> f(g(X,h(|2|()),X),g(X,h(|1|()),X))
    4: f(g(Y,h(|0|()),Y),X) -> f(Y,X)
Number of strict rules: 4
Direct Order(PosReal,>,Poly) ... failed.
Freezing f h
1: h❆1_|1|() -> h❆1_|0|()
2: h❆1_|2|() -> h❆1_|1|()
3: f❆1_|0|(X) -> f❆1_g(X,h❆1_|2|(),X,g(X,h❆1_|1|(),X))
4: f❆1_g(Y,h❆1_|0|(),Y,X) -> f(Y,X)
5: h(|0|()) ->= h❆1_|0|()
6: h(|2|()) ->= h❆1_|2|()
7: h(|1|()) ->= h❆1_|1|()
8: f(|0|(),_1) ->= f❆1_|0|(_1)
9: f(g(_1,_2,_3),_4) ->= f❆1_g(_1,_2,_3,_4)
Number of strict rules: 4
Direct Order(PosReal,>,Poly) ... failed.
Dependency Pairs:
   #1: #h❆1_|2|() -> #h❆1_|1|()
   #2: #h(|2|()) ->? #h❆1_|2|()
   #3: #f(g(_1,_2,_3),_4) ->? #f❆1_g(_1,_2,_3,_4)
   #4: #h(|1|()) ->? #h❆1_|1|()
   #5: #f❆1_|0|(X) -> #f❆1_g(X,h❆1_|2|(),X,g(X,h❆1_|1|(),X))
   #6: #f❆1_|0|(X) -> #h❆1_|2|()
   #7: #f❆1_|0|(X) -> #h❆1_|1|()
   #8: #f(|0|(),_1) ->? #f❆1_|0|(_1)
   #9: #f❆1_g(Y,h❆1_|0|(),Y,X) -> #f(Y,X)
Number of SCCs: 1, DPs: 4, edges: 5
	SCC { #3 #5 #8 #9 }
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