MAYBE
(ignored inputs)COMMENT doi:10.1016/0004-3702 ( 85 ) 90074-8 [114] p. 261/262 ( BR ) submitted by: Aart Middeldorp
input TRS:
   [ +(?x,0) -> ?x,
     *(?x,0) -> 0,
     *(?x,1) -> ?x,
     *(?x,?x) -> ?x,
     *(+(?x,?y),?z) -> +(*(?x,?z),*(?y,?z)),
     +(?x,?x) -> 0,
     -(?x) -> ?x,
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(?x,?y) -> +(?y,?x),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(?x,?y) -> *(?y,?x) ]
TRS:
   [ +(?x,0) -> ?x,
     *(?x,0) -> 0,
     *(?x,1) -> ?x,
     *(?x,?x) -> ?x,
     *(+(?x,?y),?z) -> +(*(?x,?z),*(?y,?z)),
     +(?x,?x) -> 0,
     -(?x) -> ?x,
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(?x,?y) -> +(?y,?x),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(?x,?y) -> *(?y,?x) ]
New rules by rule reversing:
   [ +(?x,0) -> ?x,
     *(?x,0) -> 0,
     *(?x,1) -> ?x,
     *(?x,?x) -> ?x,
     +(*(?x,?z),*(?y,?z)) -> *(+(?x,?y),?z),
     +(?x,?x) -> 0,
     -(?x) -> ?x,
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(?x,?y) -> +(?y,?x),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(?x,?y) -> *(?y,?x) ]
unknown UNC Completion (Development Closed)
problems/533.trs: Failure(unknown UNC)
(0 msec.)