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,
     Dh(?z,?z) -> ?z ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [  ]
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,
     Dh(?z,?z) -> ?z ]
Sort Assignment:
 I : =>18
 K : =>18
 S : =>18
 Ap : 18*18=>18
 Dh : 17*17=>17
maximal types: {17}{18}
{17}
(ps)Rewrite Rules:
   [ Dh(?z,?z) -> ?z ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [  ]
Overlay, check Innermost Termination...
Innermost Terminating (hence Terminating), WCR: CR
{18}
(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
55.trs: YES (120 msec.)