YES Rewrite Rules: [ Ap(Ap(Ap(S,?x),?y),?z) -> Ap(Ap(?x,?z),Ap(?y,?z)), Ap(Ap(K,?x),?y) -> ?x, Ap(I,?x) -> ?x, B(true,?x,?y) -> ?x, B(false,?x,?y) -> ?y, B(?z,?x,?x) -> ?x ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ?y_3 = ?y_3, ?y_4 = ?y_4 ] Overlay, check Innermost Termination... unknown Innermost Terminating not Left-Linear, not Right-Linear unknown Gomi&Oyamaguchi&Ohta check Non-Confluence...Unknown Direct Methods: Can't judge Try Persistent Decomposition for... [ Ap(Ap(Ap(S,?x),?y),?z) -> Ap(Ap(?x,?z),Ap(?y,?z)), Ap(Ap(K,?x),?y) -> ?x, Ap(I,?x) -> ?x, B(true,?x,?y) -> ?x, B(false,?x,?y) -> ?y, B(?z,?x,?x) -> ?x ] Sort Assignment: B : 13*25*25=>25 I : =>28 K : =>28 S : =>28 Ap : 28*28=>28 true : =>13 false : =>13 maximal types: {13,25}{28} {13,25} (ps)Rewrite Rules: [ B(true,?x,?y) -> ?x, B(false,?x,?y) -> ?y, B(?z,?x,?x) -> ?x ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ?y = ?y, ?y_1 = ?y_1 ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR: CR {28} (ps)Rewrite Rules: [ Ap(Ap(Ap(S,?x),?y),?z) -> Ap(Ap(?x,?z),Ap(?y,?z)), Ap(Ap(K,?x),?y) -> ?x, Ap(I,?x) -> ?x ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... unknown Innermost Terminating Left-Linear, not Right-Linear Development Closed Direct Methods: CR Result by Persistent Decomposition: CR Final result: CR 53.trs: YES (88 msec.)