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
 B(true(),x,y) -> x
 B(false(),x,y) -> y
 B(z,x,x) -> x

Proof:
 sorted: (order)
 0:B(true(),x,y) -> x
   B(false(),x,y) -> y
   B(z,x,x) -> x
 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
   [0>1, 1>2, 1>3, 4>5, 4>6, 4>7]
 sort attachment (strict)
   Ap : 4 x 4 -> 4
   S : 7
   K : 6
   I : 5
   B : 1 x 0 x 0 -> 0
   true : 3
   false : 2
 -----
 0:B(true(),x,y) -> x
   B(false(),x,y) -> y
   B(z,x,x) -> x
   Church Rosser Transformation Processor (kb):
    B(true(),x,y) -> x
    B(false(),x,y) -> y
    B(z,x,x) -> x
    critical peaks: joinable
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [true] = 5,
      
      [B](x0, x1, x2) = 2x0 + 4x1 + 4x2 + 5,
      
      [false] = 0
     orientation:
      B(true(),x,y) = 4x + 4y + 15 >= x = x
      
      B(false(),x,y) = 4x + 4y + 5 >= y = y
      
      B(z,x,x) = 8x + 2z + 5 >= x = x
     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 (critical pair closing system, Thm 2.11):
    
    critical peaks: joinable
    Qed