Input TRS:
    1: h(g(x,y),z) -> h(d(g(x,y),z),g(z,0()))
    2: d(0(),z) -> 0()
    3: d(g(x,0()),z) -> x
    4: d(g(x,g(y,0())),0()) -> x
    5: d(g(x,g(y,0())),g(z,v)) -> g(d(g(x,g(y,0())),z),y)
    6: d(g(x,g(y,g(u,v))),z) -> g(x,d(g(y,g(u,v)),z))
Number of strict rules: 6
Direct Order(PosReal,>,Poly) ... failed.
Freezing d
1: h(g(x,y),z) -> h(d❆1_g(x,y,z),g(z,0()))
2: d❆1_0(z) -> 0()
3: d❆1_g(x,0(),z) -> x
4: d❆1_g(x,g(y,0()),0()) -> x
5: d❆1_g(x,g(y,0()),g(z,v)) -> g(d❆1_g(x,g(y,0()),z),y)
6: d❆1_g(x,g(y,g(u,v)),z) -> g(x,d❆1_g(y,g(u,v),z))
7: d(0(),_1) ->= d❆1_0(_1)
8: d(g(_1,_2),_3) ->= d❆1_g(_1,_2,_3)
Number of strict rules: 6
Direct Order(PosReal,>,Poly) ... failed.
Dependency Pairs:
   #1: #d❆1_g(x,g(y,g(u,v)),z) -> #d❆1_g(y,g(u,v),z)
   #2: #d(0(),_1) ->? #d❆1_0(_1)
   #3: #d❆1_g(x,g(y,0()),g(z,v)) -> #d❆1_g(x,g(y,0()),z)
   #4: #h(g(x,y),z) -> #h(d❆1_g(x,y,z),g(z,0()))
   #5: #h(g(x,y),z) -> #d❆1_g(x,y,z)
   #6: #d(g(_1,_2),_3) ->? #d❆1_g(_1,_2,_3)
Number of SCCs: 3, DPs: 3, edges: 3
	SCC { #4 }
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