MAYBE
(ignored inputs)COMMENT doi:10.4230/LIPIcs.RTA.2015.257 [81] Example 13
Rewrite Rules:
   [ f(f(f(f(?x)))) -> f(f(f(g(?x,f(?x))))),
     f(?x) -> g(?x,f(?x)) ]
Apply Direct Methods...
Inner CPs:
   [ f(g(f(f(?x)),f(f(f(?x))))) = f(f(f(g(?x,f(?x))))),
     f(f(g(f(?x),f(f(?x))))) = f(f(f(g(?x,f(?x))))),
     f(f(f(g(?x_1,f(?x_1))))) = f(f(f(g(?x_1,f(?x_1))))),
     f(f(f(f(g(?x,f(?x)))))) = f(f(f(g(f(?x),f(f(?x)))))),
     f(f(f(f(f(g(?x,f(?x))))))) = f(f(f(g(f(f(?x)),f(f(f(?x))))))),
     f(f(f(f(f(f(g(?x,f(?x)))))))) = f(f(f(g(f(f(f(?x))),f(f(f(f(?x)))))))) ]
Outer CPs:
   [ f(f(f(g(?x,f(?x))))) = g(f(f(f(?x))),f(f(f(f(?x))))) ]
Left-Linear, not Right-Linear
(inner) Parallel CPs:
   [ f(f(f(g(?x_12,f(?x_12))))) = f(f(f(g(?x_12,f(?x_12))))) {?x_12},
     f(f(f(f(f(f(g(?x_9,f(?x_9)))))))) = f(f(f(g(f(f(f(?x_9))),f(f(f(f(?x_9)))))))) {?x_9},
     f(f(g(?x_7,f(?x_7)))) = f(f(f(g(?x,f(?x))))) {?x},
     f(f(f(f(f(g(?x_4,f(?x_4))))))) = f(f(f(g(f(f(?x_4)),f(f(f(?x_4))))))) {?x_4},
     f(g(f(f(?x)),f(f(f(?x))))) = f(f(f(g(?x,f(?x))))) {?x},
     f(f(f(f(g(?x_1,f(?x_1)))))) = f(f(f(g(f(?x_1),f(f(?x_1)))))) {?x_1} ]
unknown Toyama (Parallel CPs)
Direct Methods: Can't judge

Combined result: Can't judge
424.trs: Failure(unknown CR)
(4 msec.)