Input TRS:
    1: f(g(f(x))) -> f(g(g(g(f(x)))))
    2: g(x) ->= g(g(x))
    3: g(x) ->= g(g(f(g(g(x)))))
    4: f(x) ->= g(g(f(g(g(x)))))
Number of strict rules: 1
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #g(x) ->? #g(g(x))
   #2: #g(x) ->? #g(x)
   #3: #g(x) ->? #g(g(f(g(g(x)))))
   #4: #g(x) ->? #g(f(g(g(x))))
   #5: #g(x) ->? #f(g(g(x)))
   #6: #g(x) ->? #g(g(x))
   #7: #g(x) ->? #g(x)
   #8: #f(g(f(x))) -> #f(g(g(g(f(x)))))
   #9: #f(g(f(x))) -> #g(g(g(f(x))))
   #10: #f(g(f(x))) -> #g(g(f(x)))
   #11: #f(x) ->? #g(g(f(g(g(x)))))
   #12: #f(x) ->? #g(f(g(g(x))))
   #13: #f(x) ->? #f(g(g(x)))
   #14: #f(x) ->? #g(g(x))
   #15: #f(x) ->? #g(x)
Number of SCCs: 1, DPs: 15, edges: 108
	SCC { #1..15 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... succeeded.
     f(x1)	weight: (max (/ 3 2) 0)
   #f(x1)	weight: max{0, x1}
   #g(x1)	weight: max{0, -2 + x1}
     g(x1)	weight: max{0, -1 + x1}
    Usable rules: { 1..4 }
    Removed DPs: #8..10
Number of SCCs: 1, DPs: 12, edges: 80
	SCC { #1..7 #11..15 }
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