(ignored inputs)COMMENT from p.208 of \cite{Klop80}
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,
     Ap(D0,Ap(Ap(D,?z0),?z1)) -> ?z0,
     Ap(D1,Ap(Ap(D,?z0),?z1)) -> ?z1,
     Ap(Ap(D,Ap(D0,?z)),Ap(D1,?z)) -> ?z ]
Apply Direct Methods...
Inner CPs:
   [ Ap(D0,?z_5) = Ap(D0,?z_5),
     Ap(D1,?z_5) = Ap(D1,?z_5),
     Ap(Ap(D,?z0_3),Ap(D1,Ap(Ap(D,?z0_3),?z1_3))) = Ap(Ap(D,?z0_3),?z1_3),
     Ap(Ap(D,Ap(D0,Ap(Ap(D,?z0_4),?z1_4))),?z1_4) = Ap(Ap(D,?z0_4),?z1_4) ]
Outer CPs:
   [  ]
not Overlay, check Termination...
unknown/not Terminating
unknown Knuth&Bendix
not Left-Linear, not Right-Linear
unknown Strongly Depth-Preserving & Non-E-Overlapping
check by Reduction-Preserving Completion...
failure(empty P)
unknown Reduction-Preserving Completion
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,
     Ap(D0,Ap(Ap(D,?z0),?z1)) -> ?z0,
     Ap(D1,Ap(Ap(D,?z0),?z1)) -> ?z1,
     Ap(Ap(D,Ap(D0,?z)),Ap(D1,?z)) -> ?z ]
Sort Assignment:
 D : =>21
 I : =>21
 K : =>21
 S : =>21
 Ap : 21*21=>21
 D0 : =>21
 D1 : =>21
maximal types: {21}
Persistent Decomposition failed: Can't judge

Try Layer Preserving 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,
     Ap(D0,Ap(Ap(D,?z0),?z1)) -> ?z0,
     Ap(D1,Ap(Ap(D,?z0),?z1)) -> ?z1,
     Ap(Ap(D,Ap(D0,?z)),Ap(D1,?z)) -> ?z ]
Layer Preserving Decomposition failed: Can't judge

Try Commutative 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,
     Ap(D0,Ap(Ap(D,?z0),?z1)) -> ?z0,
     Ap(D1,Ap(Ap(D,?z0),?z1)) -> ?z1,
     Ap(Ap(D,Ap(D0,?z)),Ap(D1,?z)) -> ?z ]
Commutative Decomposition failed (not left-linear): Can't judge
No further decomposition possible


Final result: Can't judge
/local-scratch/hzankl/2012/cops2012/58.trs: Failure(unknown)
(65 msec.)