Problem:
 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

Proof:
 sorted: (order)
 0:Dh(z,z) -> z
 1:Ap(Ap(Ap(S(),x),y),z) -> Ap(Ap(x,z),Ap(y,z))
   Ap(Ap(K(),x),y) -> x
   Ap(I(),x) -> x
 -----
 sorts
   [2>3, 2>4, 2>5]
 sort attachment (strict)
   Ap : 2 x 2 -> 2
   S : 5
   K : 4
   I : 3
   Dh : 1 x 1 -> 1
 -----
 0:Dh(z,z) -> z
   Church Rosser Transformation Processor (kb):
    Dh(z,z) -> z
    critical peaks: joinable
    Matrix Interpretation Processor: dim=3
     
     interpretation:
                               [1]
      [Dh](x0, x1) = x0 + x1 + [0]
                               [0]
     orientation:
                [2 0 0]    [1]         
      Dh(z,z) = [0 2 0]z + [0] >= z = z
                [0 0 2]    [0]         
     problem:
      
     Qed
 
 
 1:Ap(Ap(Ap(S(),x),y),z) -> Ap(Ap(x,z),Ap(y,z))
   Ap(Ap(K(),x),y) -> x
   Ap(I(),x) -> x
   Church Rosser Transformation Processor:
    
    strict:
     Ap(Ap(Ap(S(),x),y),z) -> Ap(Ap(x,z),Ap(y,z))
     Ap(Ap(K(),x),y) -> x
     Ap(I(),x) -> x
    weak:
     
    critical peaks: 0
    Closedness Processor (*parallel*):
     
     strict:
      
     weak:
      
     Qed