MAYBE
(ignored inputs)COMMENT doi:10.1016/0004-3702 ( 85 ) 90074-8 [114] p. 262 ( BA ) submitted by: Aart Middeldorp
input TRS:
   [ +(?x,0) -> ?x,
     +(?x,?x) -> 0,
     *(?x,1) -> ?x,
     *(?x,?x) -> ?x,
     *(?x,0) -> 0,
     *(?x,+(?y,?z)) -> +(*(?x,?y),*(?x,?z)),
     or(?x,?y) -> +(*(?x,?y),+(?x,?y)),
     implies(?x,?y) -> +(*(?x,?y),+(?x,1)),
     equivalent(?x,?y) -> +(+(?x,?y),1),
     not(?x) -> +(?x,1),
     +(+(?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,?x) -> 0,
     *(?x,1) -> ?x,
     *(?x,?x) -> ?x,
     *(?x,0) -> 0,
     *(?x,+(?y,?z)) -> +(*(?x,?y),*(?x,?z)),
     or(?x,?y) -> +(*(?x,?y),+(?x,?y)),
     implies(?x,?y) -> +(*(?x,?y),+(?x,1)),
     equivalent(?x,?y) -> +(+(?x,?y),1),
     not(?x) -> +(?x,1),
     +(+(?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,?x) -> 0,
     *(?x,1) -> ?x,
     *(?x,?x) -> ?x,
     *(?x,0) -> 0,
     +(*(?x,?y),*(?x,?z)) -> *(?x,+(?y,?z)),
     or(?x,?y) -> or(?x,?y),
     +(*(?x,?y),+(?x,?y)) -> or(?x,?y),
     implies(?x,?y) -> implies(?x,?y),
     +(*(?x,?y),+(?x,1)) -> implies(?x,?y),
     equivalent(?x,?y) -> equivalent(?x,?y),
     +(+(?x,?y),1) -> equivalent(?x,?y),
     not(?x) -> not(?x),
     +(?x,1) -> not(?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 Parallel Closed Conditional Linearization
unknown Strongly Closed Conditional Linearization
problems/534.trs: Failure(unknown UNC)
(72 msec.)