SUCCESS 173.03 (total time) COMPLETED TRS g(refl) -> refl f(refl) -> refl symm(g(x)) -> g(symm(x)) symm(f(x)) -> f(symm(x)) symm(symm(x)) -> x symm(refl) -> refl symm(trans(x, y)) -> trans(symm(y), symm(x)) trans(g(x), g(y)) -> g(trans(x, y)) trans(g(x), f(y)) -> trans(f(y), g(x)) trans(g(x), trans(g(y), z)) -> trans(g(trans(x, y)), z) trans(g(x), trans(f(y), z)) -> trans(f(y), trans(g(x), z)) trans(f(x), f(y)) -> f(trans(x, y)) trans(f(x), trans(f(y), z)) -> trans(f(trans(x, y)), z) trans(symm(x), trans(x, y)) -> y trans(symm(x), x) -> refl trans(refl, x) -> x trans(trans(x, y), z) -> trans(x, trans(y, z)) trans(x, symm(x)) -> refl trans(x, refl) -> x trans(x, trans(symm(x), y)) -> y