YES Rewrite Rules: [ F(D(?x),?y) -> F(D(?x),G(G(?y))), F(?x,E(?y)) -> F(G(?x),E(?y)), G(?x) -> ?x, H(I(?x)) -> K(J(?x)), J(?x) -> K(J(?x)), I(?x) -> I(J(?x)), J(?x) -> J(K(J(?x))), S(?x,T(?x)) -> T(?x) ] Apply Direct Methods... Inner CPs: [ H(I(J(?x_5))) = K(J(?x_5)) ] Outer CPs: [ F(D(?x),G(G(E(?y_1)))) = F(G(D(?x)),E(?y_1)), K(J(?x_4)) = J(K(J(?x_4))) ] unknown Terminating not Left-Linear, Right-Linear unknown Ohta&Oyamaguchi&Toyama unknown Gomi&Oyamaguchi&Ohta check Non-Confluence...Unknown Direct Methods: Can't judge Try Persistent Decomposition for... [ F(D(?x),?y) -> F(D(?x),G(G(?y))), F(?x,E(?y)) -> F(G(?x),E(?y)), G(?x) -> ?x, H(I(?x)) -> K(J(?x)), J(?x) -> K(J(?x)), I(?x) -> I(J(?x)), J(?x) -> J(K(J(?x))), S(?x,T(?x)) -> T(?x) ] Sort Assignment: D : 11=>38 E : 13=>38 F : 38*38=>39 G : 38=>38 H : 35=>34 I : 34=>35 J : 34=>34 K : 34=>34 S : 31*33=>33 T : 31=>33 maximal types: {31,33}{34,35}{11,13,38,39} {31,33} (ps)Rewrite Rules: [ S(?x,T(?x)) -> T(?x) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR: CR {34,35} (ps)Rewrite Rules: [ H(I(?x)) -> K(J(?x)), J(?x) -> K(J(?x)), I(?x) -> I(J(?x)), J(?x) -> J(K(J(?x))) ] Apply Direct Methods... Inner CPs: [ H(I(J(?x_2))) = K(J(?x_2)) ] Outer CPs: [ K(J(?x_1)) = J(K(J(?x_1))) ] unknown Terminating Linear unknown Development Closed unknown Strongly Closed unknown Oyamaguchi&Ohta (inner) Parallel CPs: (not computed) unknown Toyama (Parallel CPs) Simultaneous CPs: [ K(J(?x)) = J(K(J(?x))), K(J(?x)) = H(I(J(?x))), J(K(J(?x))) = K(J(?x)), H(I(J(?x))) = K(J(?x)) ] Okui (Simultaneous CPs) Direct Methods: CR {11,13,38,39} (ps)Rewrite Rules: [ F(D(?x),?y) -> F(D(?x),G(G(?y))), F(?x,E(?y)) -> F(G(?x),E(?y)), G(?x) -> ?x ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ F(D(?x),G(G(E(?y_1)))) = F(G(D(?x)),E(?y_1)) ] Overlay, check Innermost Termination... unknown Innermost Terminating Linear Development Closed Direct Methods: CR Result by Persistent Decomposition: CR Final result: CR 94.trs: YES (40 msec.)