\\ U(B U(B K))(cons(U(B* U(B K)S)(cons(C' S(C'(B* |)&(=(2)))(=(3)))(cons(U(B* U(B K)(S(B*(B*(B(/ +)))S(S'(B* cons)' I))(S(B*(S' S)(B* cons)')(S'(S' S)(C'(B* cons)')(B*(S' S(S'(B* cons)' I))(S'(S' cons)')(C(S(B* B*(S' cons)')(S' cons))(C(C' cons)nil)))))))(cons(!(-1))(cons(!(1))nil)))nil)))(cons(cons(0 0 0 0 0 0)(cons(0 0 1 0 0 0)(cons(0 1 0 0 0 0)(cons(0 1 1 1 1 0)(cons(0 0 0 0 0 0)nil)))))nil))