Tehát az lenne a jó, ha mondjuk egy program találná meg a megoldást, hogy pl.:

w(Auvu)(Auvv) = C(T(Auvu))(Auvv) w =
 = S(BC(BT(C(Au)u)))(W(Au)) vw =
 = S(BS(B(BC)(B(BT)(W(BCA)))))(BWA) uvw =
 = S(BS(B(BS)(B(B(BC))(B(B(BT))(BW(BC))))))(BW) Auvw

ekkor ugyanis az alábbi egy megoldása az egyenletnek:

A = θ(S(BS(B(BS)(B(B(BC))(B(B(BT))(BW(BC))))))(BW))

ui
A = S(BS(B(BS)(B(B(BC))(B(B(BT))(BW(BC))))))(BW)) A
Au = S(BS(B(BS)(B(B(BC))(B(B(BT))(BW(BC))))))(BW)) Au

Auv = S(BS(B(BS)(B(B(BC))(B(B(BT))(BW(BC))))))(BW)) Auv

Auvw = S(BS(B(BS)(B(B(BC))(B(B(BT))(BW(BC))))))(BW)) Auvw =
 = w(Auvu)(Auvv)

Egyelőre Python-ban tákoltam valamit: https://github.com/lzsiga/hello-world/blob/master/lc_formstd.py