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
   [1>2, 2>3, 2>4, 5>6, 5>7, 5>8]
 sort attachment (strict)
   Ap : 5 x 5 -> 5
   S : 8
   K : 7
   I : 6
   B : 2 x 1 x 1 -> 1
   true : 4
   false : 3
 -----
 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:
      [false] = 0,
      
      [B](x0, x1, x2) = x0 + x1 + x2 + 3,
      
      [true] = 0
     orientation:
      B(true(),x,y) = x + y + 3 >= x = x
      
      B(false(),x,y) = x + y + 3 >= y = y
      
      B(z,x,x) = 2x + z + 3 >= 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:
    
    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