0.07/0.07 YES 0.07/0.07 Conditional Rewrite Rules: 0.07/0.07 [ g(a) -> c(b), 0.07/0.07 b -> f(a), 0.07/0.07 f(?x) -> ?x | g(?x) == c(?y) ] 0.07/0.07 Check whether all rules are type 3 0.07/0.07 OK 0.07/0.07 Check whether the input is deterministic 0.07/0.07 OK 0.07/0.07 Result of unraveling: 0.07/0.07 [ g(a) -> c(b), 0.07/0.07 b -> f(a), 0.07/0.07 f(?x) -> U0(g(?x),?x), 0.07/0.07 U0(c(?y),?x) -> ?x ] 0.07/0.07 Check whether U(R) is terminating 0.07/0.07 failed to show termination 0.07/0.07 Check whether the input is weakly left-linear 0.07/0.07 OK 0.07/0.07 Conditional critical pairs (CCPs): 0.07/0.07 [ ] 0.07/0.07 Check whether the input is almost orthogonale 0.07/0.07 OK 0.07/0.07 Check whether the input is properly oriented 0.07/0.07 OK 0.07/0.07 Check whether the input is right-stable 0.07/0.07 OK 0.07/0.07 R is almost orthogonal, properly oriented, right stable