MAYBE
(ignored inputs)COMMENT [Kapur et al. IC 1999] p.30
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ f(?x,?x) -> ?x,
     f(?x,e) -> ?x,
     f(e,?x) -> ?x,
     f(?x,i(?x)) -> e,
     f(i(?x),?x) -> e ]
Constructors: {e,f,i}
Defined function symbols: {}
Constructor subsystem:
   [ f(?x,e) -> ?x,
     f(e,?x) -> ?x,
     f(?x,i(?x)) -> e,
     f(i(?x),?x) -> e ]
Rule part & Conj Part:
   [ f(?x,e) -> ?x,
     f(e,?x) -> ?x,
     f(?x,i(?x)) -> e,
     f(i(?x),?x) -> e ]
   [ f(?x,?x) -> ?x ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Elem}
Signature:
   [ f : Elem,Elem -> Elem,
     i : Elem -> Elem,
     e : Elem ]
Rule Part:
   [ f(?x,e) -> ?x,
     f(e,?x) -> ?x,
     f(?x,i(?x)) -> e,
     f(i(?x),?x) -> e ]
Conjecture Part:
   [ f(?x,?x) = ?x ]
Precedence (by weight): {(e,0),(f,3),(i,2)}
Rule part is not confluent.
Check ground confluence of Rule part (R0) by basic RI.
Rules:
   [ f(?x,e) -> ?x,
     f(e,?x) -> ?x,
     f(?x,i(?x)) -> e,
     f(i(?x),?x) -> e ]
Conjectures:
   [ e = i(e),
     e = i(e) ]
STEP 0
ES:
   [ e = i(e),
     e = i(e) ]
HS:
   [ ]
ES0:
   [ e = i(e),
     e = i(e) ]
HS0:
   [ ]
ES1:
   [ e = i(e),
     e = i(e) ]
HS1:
   [ ]
No equation to expand
Failed to prove ground confluece R0.
examples/additions/elem2.trs: Failure(unknown)
(8 msec.)