MAYBE (ignored inputs)COMMENT addition + commutative law Rewrite Rules: [ +(?x,0) -> ?x, +(?x,s(?y)) -> s(+(?x,?y)), +(?x,?y) -> +(?y,?x) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ?x = +(0,?x), s(+(?x_1,?y_1)) = +(s(?y_1),?x_1) ] Linear (inner) Parallel CPs: (not computed) unknown Toyama (Parallel CPs) Direct Methods: Can't judge Combined result: Can't judge 106.trs: Failure(unknown CR) (0 msec.)