d 1: A = I I -> I = I. d 2: A = K K -> K = K. d 3: A = S S -> S = S. d 4: A = Z Z -> Z = Z. d 5: A = E E -> E = E. d 6: A = e e -> e = e. d 7: A = X X -> X = X. d 8: A = ! ! -> ! = !. d 11: A = --S--S-KSK-KI I -> ((S ((S (K S)) K)) (K I)) = I. d 12: A = --S--S-KS--S-KK--S-KSK-KK -S-KK -> ((S ((S (K S)) ((S (K K)) ((S (K S)) K)))) (K K)) = (S (K K)). d 13: A = --S-KS-S-KK K -> ((S (K S)) (S (K K))) = K. d 14: A = --S-K-S-KS--S-KS-S-KS --S--S-KS--S-KK--S-KS-S-K-S-KSS -> ((S (K (S (K S)))) ((S (K S)) (S (K S)))) = ((S ((S (K S)) ((S (K K)) ((S (K S)) (S (K (S (K S)))))))) S). d 15: A = -S-KI I -> (S (K I)) = I. d 16: A = --S-K-S-KS--S-KS-S-KS --S--S-KS--S-KK--S-KS--S-K-S-KSS-KS -> ((S (K (S (K S)))) ((S (K S)) (S (K S)))) = ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) S))))) (K S)). d 21: A = --SEI -KI -> ((S E) I) = (K I). d 22: A = --S--S-KSeK --S--S-KSe-KI -> ((S ((S (K S)) e)) K) = ((S ((S (K S)) e)) (K I)). d 23: A = --S-K-S-KS--S-K-S-KKe --S--S-KS--S-K-S-KS--S-K-S-K-S-KS--S-K-S-K-S-KKe--S-K-S-KKe -> ((S (K (S (K S)))) ((S (K (S (K K)))) e)) = ((S ((S (K S)) ((S (K (S (K S)))) ((S (K (S (K (S (K S)))))) ((S (K (S (K (S (K K)))))) e))))) ((S (K (S (K K)))) e)). d 31: S 2 2 7 -> ---SKKX = --KX-KX ; (((S K) K) X) = ((K X) (K X)). d 32: a 2 7 -> -KX = -KX ; (K X) = (K X). d 33: K 7 32 -> --KX-KX = X ; ((K X) (K X)) = X. d 34: t 31 33 -> ---SKKX = X ; (((S K) K) X) = X. d 41: A = x x -> x = x. d 42: A = y y -> y = y. d 43: A = z z -> z = z. d 51: A = t t -> t = t. d 52: A = o o -> o = o. d 53: A = u u -> u = u. d 54: A = f f -> f = f. d 61: A = -to I -> (t o) = I. d 62: A = -tu I -> (t u) = I. d 63: A = --S--S-KS--S-KK--S--S-K!t-KI--S-K-S--S--S-K!t-KI--S-K-S-Ktf --S--S-KS--S-KK--S--S-K!t-KI-K--S--S--S-K!t-KI-KI -> ((S ((S (K S)) ((S (K K)) ((S ((S (K !)) t)) (K I))))) ((S (K (S ((S ((S (K !)) t)) (K I))))) ((S (K (S (K t)))) f))) = ((S ((S (K S)) ((S (K K)) ((S ((S (K !)) t)) (K I))))) (K ((S ((S ((S (K !)) t)) (K I))) (K I)))). d 71: A = --S!I -KI -> ((S !) I) = (K I). d 72: A = i i -> i = i. d 73: A = k k -> k = k. d 74: A = s s -> s = s. d 80: A = & & -> & = &. d 81: A = T T -> T = T. d 82: A = --S-KTi --SfI -> ((S (K T)) i) = ((S f) I). d 83: A = --S-K-S-KTk --S--S-KS--S-KKf--S-K-SfK -> ((S (K (S (K T)))) k) = ((S ((S (K S)) ((S (K K)) f))) ((S (K (S f))) K)). d 84: A = --S-K-S-K-S-KTs --S--S-KS--S-K-S-KS--S-K-S-K-S-Kf--S--S-KS--S-KK--S-KS--S-KKf-Kf--S--S-KS--S-K-S-KS--S-K-S-KK--S-K-S-Kff--S-KKf -> ((S (K (S (K (S (K T)))))) s) = ((S ((S (K S)) ((S (K (S (K S)))) ((S (K (S (K (S (K f)))))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) f))))) (K f)))))) ((S ((S (K S)) ((S (K (S (K S)))) ((S (K (S (K K)))) ((S (K (S (K f)))) f))))) ((S (K K)) f))). d 85: A = --S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--S-K-S-K-S-KK--S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT& --S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf-K--S-K!T -> ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) ((S (K (S (K (S (K K)))))) ((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &))))) = ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) (K ((S (K !)) T))). d 101: a 2 3 -> -KS = -KS ; (K S) = (K S). d 102: a 3 101 -> -S-KS = -S-KS ; (S (K S)) = (S (K S)). d 103: a 2 2 -> -KK = -KK ; (K K) = (K K). d 104: a 3 103 -> -S-KK = -S-KK ; (S (K K)) = (S (K K)). d 105: a 104 2 -> --S-KKK = --S-KKK ; ((S (K K)) K) = ((S (K K)) K). d 106: a 102 105 -> --S-KS--S-KKK = --S-KS--S-KKK ; ((S (K S)) ((S (K K)) K)) = ((S (K S)) ((S (K K)) K)). d 107: a 2 1 -> -KI = -KI ; (K I) = (K I). d 108: S 106 107 7 -> ---S--S-KS--S-KKK-KIX = ----S-KS--S-KKKX--KIX ; (((S ((S (K S)) ((S (K K)) K))) (K I)) X) = ((((S (K S)) ((S (K K)) K)) X) ((K I) X)). d 109: S 101 105 7 -> ---S-KS--S-KKKX = ---KSX---S-KKKX ; (((S (K S)) ((S (K K)) K)) X) = (((K S) X) (((S (K K)) K) X)). d 110: K 3 7 -> --KSX = S ; ((K S) X) = S. d 111: S 103 2 7 -> ---S-KKKX = ---KKX-KX ; (((S (K K)) K) X) = (((K K) X) (K X)). d 112: K 2 7 -> --KKX = K ; ((K K) X) = K. d 113: a 112 32 -> ---KKX-KX = -K-KX ; (((K K) X) (K X)) = (K (K X)). d 114: a 2 32 -> -K-KX = -K-KX ; (K (K X)) = (K (K X)). d 115: t 111 113 -> ---S-KKKX = -K-KX ; (((S (K K)) K) X) = (K (K X)). d 116: a 110 115 -> ---KSX---S-KKKX = -S-K-KX ; (((K S) X) (((S (K K)) K) X)) = (S (K (K X))). d 117: a 3 114 -> -S-K-KX = -S-K-KX ; (S (K (K X))) = (S (K (K X))). d 118: t 109 116 -> ---S-KS--S-KKKX = -S-K-KX ; (((S (K S)) ((S (K K)) K)) X) = (S (K (K X))). d 119: K 1 7 -> --KIX = I ; ((K I) X) = I. d 120: a 118 119 -> ----S-KS--S-KKKX--KIX = --S-K-KXI ; ((((S (K S)) ((S (K K)) K)) X) ((K I) X)) = ((S (K (K X))) I). d 121: a 117 1 -> --S-K-KXI = --S-K-KXI ; ((S (K (K X))) I) = ((S (K (K X))) I). d 122: t 108 120 -> ---S--S-KS--S-KKK-KIX = --S-K-KXI ; (((S ((S (K S)) ((S (K K)) K))) (K I)) X) = ((S (K (K X))) I). d 123: a 122 4 -> ----S--S-KS--S-KKK-KIXZ = ---S-K-KXIZ ; ((((S ((S (K S)) ((S (K K)) K))) (K I)) X) Z) = (((S (K (K X))) I) Z). d 124: S 114 1 4 -> ---S-K-KXIZ = ---K-KXZ-IZ ; (((S (K (K X))) I) Z) = (((K (K X)) Z) (I Z)). d 125: K 32 4 -> --K-KXZ = -KX ; ((K (K X)) Z) = (K X). d 126: I 4 -> -IZ = Z ; (I Z) = Z. d 127: a 125 126 -> ---K-KXZ-IZ = --KXZ ; (((K (K X)) Z) (I Z)) = ((K X) Z). d 128: K 7 4 -> --KXZ = X ; ((K X) Z) = X. d 129: t 127 128 -> ---K-KXZ-IZ = X ; (((K (K X)) Z) (I Z)) = X. d 130: t 124 129 -> ---S-K-KXIZ = X ; (((S (K (K X))) I) Z) = X. d 131: t 123 130 -> ----S--S-KS--S-KKK-KIXZ = X ; ((((S ((S (K S)) ((S (K K)) K))) (K I)) X) Z) = X. d 132: a 63 52 -> ---S--S-KS--S-KK--S--S-K!t-KI--S-K-S--S--S-K!t-KI--S-K-S-Ktfo = ---S--S-KS--S-KK--S--S-K!t-KI-K--S--S--S-K!t-KI-KIo ; (((S ((S (K S)) ((S (K K)) ((S ((S (K !)) t)) (K I))))) ((S (K (S ((S ((S (K !)) t)) (K I))))) ((S (K (S (K t)))) f))) o) = (((S ((S (K S)) ((S (K K)) ((S ((S (K !)) t)) (K I))))) (K ((S ((S ((S (K !)) t)) (K I))) (K I)))) o). d 133: a 132 52 -> ----S--S-KS--S-KK--S--S-K!t-KI--S-K-S--S--S-K!t-KI--S-K-S-Ktfoo = ----S--S-KS--S-KK--S--S-K!t-KI-K--S--S--S-K!t-KI-KIoo ; ((((S ((S (K S)) ((S (K K)) ((S ((S (K !)) t)) (K I))))) ((S (K (S ((S ((S (K !)) t)) (K I))))) ((S (K (S (K t)))) f))) o) o) = ((((S ((S (K S)) ((S (K K)) ((S ((S (K !)) t)) (K I))))) (K ((S ((S ((S (K !)) t)) (K I))) (K I)))) o) o). d 134: a 82 52 -> ---S-KTio = ---SfIo ; (((S (K T)) i) o) = (((S f) I) o). d 135: a 2 81 -> -KT = -KT ; (K T) = (K T). d 136: S 54 1 52 -> ---SfIo = --fo-Io ; (((S f) I) o) = ((f o) (I o)). d 137: a 54 52 -> -fo = -fo ; (f o) = (f o). d 138: I 52 -> -Io = o ; (I o) = o. d 139: a 137 138 -> --fo-Io = --foo ; ((f o) (I o)) = ((f o) o). d 140: a 137 52 -> --foo = --foo ; ((f o) o) = ((f o) o). d 141: t 136 139 -> ---SfIo = --foo ; (((S f) I) o) = ((f o) o). d 142: s -1 -> -KS = -KS ; (K S) = (K S). d 143: s 101 -> -KS = -KS ; (K S) = (K S). d 144: t 142 143 -> -KS = -KS ; (K S) = (K S). d 145: ? -> I = I ; I = I. d 146: S 54 1 52 -> ---SfIo = --fo-Io ; (((S f) I) o) = ((f o) (I o)). d 147: I 52 -> -Io = o ; (I o) = o. d 148: t 146 139 -> ---SfIo = --foo ; (((S f) I) o) = ((f o) o). d 149: t 145 1 -> I = I ; I = I. d 150: s 148 -> --foo = ---SfIo ; ((f o) o) = (((S f) I) o). d 151: ? -> I = I ; I = I. d 152: ? -> I = I ; I = I. d 153: S 135 72 52 -> ---S-KTio = ---KTo-io ; (((S (K T)) i) o) = (((K T) o) (i o)). d 154: K 81 52 -> --KTo = T ; ((K T) o) = T. d 155: a 72 52 -> -io = -io ; (i o) = (i o). d 156: a 154 155 -> ---KTo-io = -T-io ; (((K T) o) (i o)) = (T (i o)). d 157: a 81 155 -> -T-io = -T-io ; (T (i o)) = (T (i o)). d 158: t 153 156 -> ---S-KTio = -T-io ; (((S (K T)) i) o) = (T (i o)). d 159: S 54 1 52 -> ---SfIo = --fo-Io ; (((S f) I) o) = ((f o) (I o)). d 160: I 52 -> -Io = o ; (I o) = o. d 161: t 159 139 -> ---SfIo = --foo ; (((S f) I) o) = ((f o) o). d 162: s 158 -> -T-io = ---S-KTio ; (T (i o)) = (((S (K T)) i) o). d 163: t 162 134 -> -T-io = ---SfIo ; (T (i o)) = (((S f) I) o). d 164: t 163 161 -> -T-io = --foo ; (T (i o)) = ((f o) o). d 165: a 83 140 -> ---S-K-S-KTk--foo = ---S--S-KS--S-KKf--S-K-SfK--foo ; (((S (K (S (K T)))) k) ((f o) o)) = (((S ((S (K S)) ((S (K K)) f))) ((S (K (S f))) K)) ((f o) o)). d 166: a 165 52 -> ----S-K-S-KTk--fooo = ----S--S-KS--S-KKf--S-K-SfK--fooo ; ((((S (K (S (K T)))) k) ((f o) o)) o) = ((((S ((S (K S)) ((S (K K)) f))) ((S (K (S f))) K)) ((f o) o)) o). d 167: a 3 135 -> -S-KT = -S-KT ; (S (K T)) = (S (K T)). d 168: a 2 167 -> -K-S-KT = -K-S-KT ; (K (S (K T))) = (K (S (K T))). d 169: S 168 73 140 -> ---S-K-S-KTk--foo = ---K-S-KT--foo-k--foo ; (((S (K (S (K T)))) k) ((f o) o)) = (((K (S (K T))) ((f o) o)) (k ((f o) o))). d 170: K 167 140 -> --K-S-KT--foo = -S-KT ; ((K (S (K T))) ((f o) o)) = (S (K T)). d 171: a 73 140 -> -k--foo = -k--foo ; (k ((f o) o)) = (k ((f o) o)). d 172: a 170 171 -> ---K-S-KT--foo-k--foo = --S-KT-k--foo ; (((K (S (K T))) ((f o) o)) (k ((f o) o))) = ((S (K T)) (k ((f o) o))). d 173: a 167 171 -> --S-KT-k--foo = --S-KT-k--foo ; ((S (K T)) (k ((f o) o))) = ((S (K T)) (k ((f o) o))). d 174: t 169 172 -> ---S-K-S-KTk--foo = --S-KT-k--foo ; (((S (K (S (K T)))) k) ((f o) o)) = ((S (K T)) (k ((f o) o))). d 175: a 174 52 -> ----S-K-S-KTk--fooo = ---S-KT-k--fooo ; ((((S (K (S (K T)))) k) ((f o) o)) o) = (((S (K T)) (k ((f o) o))) o). d 176: S 135 171 52 -> ---S-KT-k--fooo = ---KTo--k--fooo ; (((S (K T)) (k ((f o) o))) o) = (((K T) o) ((k ((f o) o)) o)). d 177: K 81 52 -> --KTo = T ; ((K T) o) = T. d 178: a 171 52 -> --k--fooo = --k--fooo ; ((k ((f o) o)) o) = ((k ((f o) o)) o). d 179: a 177 178 -> ---KTo--k--fooo = -T--k--fooo ; (((K T) o) ((k ((f o) o)) o)) = (T ((k ((f o) o)) o)). d 180: a 81 178 -> -T--k--fooo = -T--k--fooo ; (T ((k ((f o) o)) o)) = (T ((k ((f o) o)) o)). d 181: t 176 179 -> ---S-KT-k--fooo = -T--k--fooo ; (((S (K T)) (k ((f o) o))) o) = (T ((k ((f o) o)) o)). d 182: t 175 181 -> ----S-K-S-KTk--fooo = -T--k--fooo ; ((((S (K (S (K T)))) k) ((f o) o)) o) = (T ((k ((f o) o)) o)). d 183: a 104 54 -> --S-KKf = --S-KKf ; ((S (K K)) f) = ((S (K K)) f). d 184: a 102 183 -> --S-KS--S-KKf = --S-KS--S-KKf ; ((S (K S)) ((S (K K)) f)) = ((S (K S)) ((S (K K)) f)). d 185: a 3 54 -> -Sf = -Sf ; (S f) = (S f). d 186: a 2 185 -> -K-Sf = -K-Sf ; (K (S f)) = (K (S f)). d 187: a 3 186 -> -S-K-Sf = -S-K-Sf ; (S (K (S f))) = (S (K (S f))). d 188: a 187 2 -> --S-K-SfK = --S-K-SfK ; ((S (K (S f))) K) = ((S (K (S f))) K). d 189: S 184 188 140 -> ---S--S-KS--S-KKf--S-K-SfK--foo = ----S-KS--S-KKf--foo---S-K-SfK--foo ; (((S ((S (K S)) ((S (K K)) f))) ((S (K (S f))) K)) ((f o) o)) = ((((S (K S)) ((S (K K)) f)) ((f o) o)) (((S (K (S f))) K) ((f o) o))). d 190: S 101 183 140 -> ---S-KS--S-KKf--foo = ---KS--foo---S-KKf--foo ; (((S (K S)) ((S (K K)) f)) ((f o) o)) = (((K S) ((f o) o)) (((S (K K)) f) ((f o) o))). d 191: K 3 140 -> --KS--foo = S ; ((K S) ((f o) o)) = S. d 192: S 103 54 140 -> ---S-KKf--foo = ---KK--foo-f--foo ; (((S (K K)) f) ((f o) o)) = (((K K) ((f o) o)) (f ((f o) o))). d 193: K 2 140 -> --KK--foo = K ; ((K K) ((f o) o)) = K. d 194: a 54 140 -> -f--foo = -f--foo ; (f ((f o) o)) = (f ((f o) o)). d 195: a 193 194 -> ---KK--foo-f--foo = -K-f--foo ; (((K K) ((f o) o)) (f ((f o) o))) = (K (f ((f o) o))). d 196: a 2 194 -> -K-f--foo = -K-f--foo ; (K (f ((f o) o))) = (K (f ((f o) o))). d 197: t 192 195 -> ---S-KKf--foo = -K-f--foo ; (((S (K K)) f) ((f o) o)) = (K (f ((f o) o))). d 198: a 191 197 -> ---KS--foo---S-KKf--foo = -S-K-f--foo ; (((K S) ((f o) o)) (((S (K K)) f) ((f o) o))) = (S (K (f ((f o) o)))). d 199: a 3 196 -> -S-K-f--foo = -S-K-f--foo ; (S (K (f ((f o) o)))) = (S (K (f ((f o) o)))). d 200: t 190 198 -> ---S-KS--S-KKf--foo = -S-K-f--foo ; (((S (K S)) ((S (K K)) f)) ((f o) o)) = (S (K (f ((f o) o)))). d 201: S 186 2 140 -> ---S-K-SfK--foo = ---K-Sf--foo-K--foo ; (((S (K (S f))) K) ((f o) o)) = (((K (S f)) ((f o) o)) (K ((f o) o))). d 202: K 185 140 -> --K-Sf--foo = -Sf ; ((K (S f)) ((f o) o)) = (S f). d 203: a 2 140 -> -K--foo = -K--foo ; (K ((f o) o)) = (K ((f o) o)). d 204: a 202 203 -> ---K-Sf--foo-K--foo = --Sf-K--foo ; (((K (S f)) ((f o) o)) (K ((f o) o))) = ((S f) (K ((f o) o))). d 205: a 185 203 -> --Sf-K--foo = --Sf-K--foo ; ((S f) (K ((f o) o))) = ((S f) (K ((f o) o))). d 206: t 201 204 -> ---S-K-SfK--foo = --Sf-K--foo ; (((S (K (S f))) K) ((f o) o)) = ((S f) (K ((f o) o))). d 207: a 200 206 -> ----S-KS--S-KKf--foo---S-K-SfK--foo = --S-K-f--foo--Sf-K--foo ; ((((S (K S)) ((S (K K)) f)) ((f o) o)) (((S (K (S f))) K) ((f o) o))) = ((S (K (f ((f o) o)))) ((S f) (K ((f o) o)))). d 208: a 199 205 -> --S-K-f--foo--Sf-K--foo = --S-K-f--foo--Sf-K--foo ; ((S (K (f ((f o) o)))) ((S f) (K ((f o) o)))) = ((S (K (f ((f o) o)))) ((S f) (K ((f o) o)))). d 209: t 189 207 -> ---S--S-KS--S-KKf--S-K-SfK--foo = --S-K-f--foo--Sf-K--foo ; (((S ((S (K S)) ((S (K K)) f))) ((S (K (S f))) K)) ((f o) o)) = ((S (K (f ((f o) o)))) ((S f) (K ((f o) o)))). d 210: a 209 52 -> ----S--S-KS--S-KKf--S-K-SfK--fooo = ---S-K-f--foo--Sf-K--fooo ; ((((S ((S (K S)) ((S (K K)) f))) ((S (K (S f))) K)) ((f o) o)) o) = (((S (K (f ((f o) o)))) ((S f) (K ((f o) o)))) o). d 211: S 196 205 52 -> ---S-K-f--foo--Sf-K--fooo = ---K-f--fooo---Sf-K--fooo ; (((S (K (f ((f o) o)))) ((S f) (K ((f o) o)))) o) = (((K (f ((f o) o))) o) (((S f) (K ((f o) o))) o)). d 212: K 194 52 -> --K-f--fooo = -f--foo ; ((K (f ((f o) o))) o) = (f ((f o) o)). d 213: S 54 203 52 -> ---Sf-K--fooo = --fo--K--fooo ; (((S f) (K ((f o) o))) o) = ((f o) ((K ((f o) o)) o)). d 214: K 140 52 -> --K--fooo = --foo ; ((K ((f o) o)) o) = ((f o) o). d 215: a 137 214 -> --fo--K--fooo = --fo--foo ; ((f o) ((K ((f o) o)) o)) = ((f o) ((f o) o)). d 216: a 137 140 -> --fo--foo = --fo--foo ; ((f o) ((f o) o)) = ((f o) ((f o) o)). d 217: t 213 215 -> ---Sf-K--fooo = --fo--foo ; (((S f) (K ((f o) o))) o) = ((f o) ((f o) o)). d 218: a 212 217 -> ---K-f--fooo---Sf-K--fooo = --f--foo--fo--foo ; (((K (f ((f o) o))) o) (((S f) (K ((f o) o))) o)) = ((f ((f o) o)) ((f o) ((f o) o))). d 219: a 194 216 -> --f--foo--fo--foo = --f--foo--fo--foo ; ((f ((f o) o)) ((f o) ((f o) o))) = ((f ((f o) o)) ((f o) ((f o) o))). d 220: t 211 218 -> ---S-K-f--foo--Sf-K--fooo = --f--foo--fo--foo ; (((S (K (f ((f o) o)))) ((S f) (K ((f o) o)))) o) = ((f ((f o) o)) ((f o) ((f o) o))). d 221: t 210 220 -> ----S--S-KS--S-KKf--S-K-SfK--fooo = --f--foo--fo--foo ; ((((S ((S (K S)) ((S (K K)) f))) ((S (K (S f))) K)) ((f o) o)) o) = ((f ((f o) o)) ((f o) ((f o) o))). d 222: s 182 -> -T--k--fooo = ----S-K-S-KTk--fooo ; (T ((k ((f o) o)) o)) = ((((S (K (S (K T)))) k) ((f o) o)) o). d 223: t 222 166 -> -T--k--fooo = ----S--S-KS--S-KKf--S-K-SfK--fooo ; (T ((k ((f o) o)) o)) = ((((S ((S (K S)) ((S (K K)) f))) ((S (K (S f))) K)) ((f o) o)) o). d 224: t 223 221 -> -T--k--fooo = --f--foo--fo--foo ; (T ((k ((f o) o)) o)) = ((f ((f o) o)) ((f o) ((f o) o))). d 225: a 73 52 -> -ko = -ko ; (k o) = (k o). d 226: a 225 52 -> --koo = --koo ; ((k o) o) = ((k o) o). d 227: a 52 52 -> -oo = -oo ; (o o) = (o o). d 228: a 85 226 -> ---S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--S-K-S-K-S-KK--S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--koo = ---S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf-K--S-K!T--koo ; (((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) ((S (K (S (K (S (K K)))))) ((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &))))) ((k o) o)) = (((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) (K ((S (K !)) T))) ((k o) o)). d 229: a 228 155 -> ----S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--S-K-S-K-S-KK--S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--koo-io = ----S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf-K--S-K!T--koo-io ; ((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) ((S (K (S (K (S (K K)))))) ((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &))))) ((k o) o)) (i o)) = ((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) (K ((S (K !)) T))) ((k o) o)) (i o)). d 230: a 229 227 -> -----S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--S-K-S-K-S-KK--S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--koo-io-oo = -----S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf-K--S-K!T--koo-io-oo ; (((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) ((S (K (S (K (S (K K)))))) ((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &))))) ((k o) o)) (i o)) (o o)) = (((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) (K ((S (K !)) T))) ((k o) o)) (i o)) (o o)). d 231: a 230 52 -> ------S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--S-K-S-K-S-KK--S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--koo-io-ooo = ------S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf-K--S-K!T--koo-io-ooo ; ((((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) ((S (K (S (K (S (K K)))))) ((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &))))) ((k o) o)) (i o)) (o o)) o) = ((((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) (K ((S (K !)) T))) ((k o) o)) (i o)) (o o)) o). d 232: a 2 102 -> -K-S-KS = -K-S-KS ; (K (S (K S))) = (K (S (K S))). d 233: a 3 232 -> -S-K-S-KS = -S-K-S-KS ; (S (K (S (K S)))) = (S (K (S (K S)))). d 234: a 2 8 -> -K! = -K! ; (K !) = (K !). d 235: a 3 234 -> -S-K! = -S-K! ; (S (K !)) = (S (K !)). d 236: a 235 81 -> --S-K!T = --S-K!T ; ((S (K !)) T) = ((S (K !)) T). d 237: a 104 236 -> --S-KK--S-K!T = --S-KK--S-K!T ; ((S (K K)) ((S (K !)) T)) = ((S (K K)) ((S (K !)) T)). d 238: a 102 237 -> --S-KS--S-KK--S-K!T = --S-KS--S-KK--S-K!T ; ((S (K S)) ((S (K K)) ((S (K !)) T))) = ((S (K S)) ((S (K K)) ((S (K !)) T))). d 239: a 104 238 -> --S-KK--S-KS--S-KK--S-K!T = --S-KK--S-KS--S-KK--S-K!T ; ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))) = ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))). d 240: a 102 239 -> --S-KS--S-KK--S-KS--S-KK--S-K!T = --S-KS--S-KK--S-KS--S-KK--S-K!T ; ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T))))) = ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T))))). d 241: a 3 240 -> -S--S-KS--S-KK--S-KS--S-KK--S-K!T = -S--S-KS--S-KK--S-KS--S-KK--S-K!T ; (S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) = (S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))). d 242: a 2 54 -> -Kf = -Kf ; (K f) = (K f). d 243: a 241 242 -> --S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf = --S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf ; ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)) = ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)). d 244: a 233 243 -> --S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf = --S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf ; ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))) = ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))). d 245: a 102 244 -> --S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf = --S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf ; ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)))) = ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)))). d 246: a 104 245 -> --S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf = --S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf ; ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))) = ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))). d 247: a 102 246 -> --S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf = --S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf ; ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)))))) = ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)))))). d 248: a 2 104 -> -K-S-KK = -K-S-KK ; (K (S (K K))) = (K (S (K K))). d 249: a 3 248 -> -S-K-S-KK = -S-K-S-KK ; (S (K (S (K K)))) = (S (K (S (K K)))). d 250: a 2 249 -> -K-S-K-S-KK = -K-S-K-S-KK ; (K (S (K (S (K K))))) = (K (S (K (S (K K))))). d 251: a 3 250 -> -S-K-S-K-S-KK = -S-K-S-K-S-KK ; (S (K (S (K (S (K K)))))) = (S (K (S (K (S (K K)))))). d 252: a 102 236 -> --S-KS--S-K!T = --S-KS--S-K!T ; ((S (K S)) ((S (K !)) T)) = ((S (K S)) ((S (K !)) T)). d 253: a 3 252 -> -S--S-KS--S-K!T = -S--S-KS--S-K!T ; (S ((S (K S)) ((S (K !)) T))) = (S ((S (K S)) ((S (K !)) T))). d 254: a 2 253 -> -K-S--S-KS--S-K!T = -K-S--S-KS--S-K!T ; (K (S ((S (K S)) ((S (K !)) T)))) = (K (S ((S (K S)) ((S (K !)) T)))). d 255: a 3 254 -> -S-K-S--S-KS--S-K!T = -S-K-S--S-KS--S-K!T ; (S (K (S ((S (K S)) ((S (K !)) T))))) = (S (K (S ((S (K S)) ((S (K !)) T))))). d 256: a 3 168 -> -S-K-S-KT = -S-K-S-KT ; (S (K (S (K T)))) = (S (K (S (K T)))). d 257: a 256 80 -> --S-K-S-KT& = --S-K-S-KT& ; ((S (K (S (K T)))) &) = ((S (K (S (K T)))) &). d 258: a 249 257 -> --S-K-S-KK--S-K-S-KT& = --S-K-S-KK--S-K-S-KT& ; ((S (K (S (K K)))) ((S (K (S (K T)))) &)) = ((S (K (S (K K)))) ((S (K (S (K T)))) &)). d 259: a 255 258 -> --S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT& = --S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT& ; ((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &))) = ((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &))). d 260: a 251 259 -> --S-K-S-K-S-KK--S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT& = --S-K-S-K-S-KK--S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT& ; ((S (K (S (K (S (K K)))))) ((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &)))) = ((S (K (S (K (S (K K)))))) ((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &)))). d 261: S 247 260 226 -> ---S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--S-K-S-K-S-KK--S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--koo = ----S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--koo---S-K-S-K-S-KK--S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--koo ; (((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) ((S (K (S (K (S (K K)))))) ((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &))))) ((k o) o)) = ((((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)))))) ((k o) o)) (((S (K (S (K (S (K K)))))) ((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &)))) ((k o) o))). d 262: S 101 246 226 -> ---S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--koo = ---KS--koo---S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--koo ; (((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)))))) ((k o) o)) = (((K S) ((k o) o)) (((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))) ((k o) o))). d 263: K 3 226 -> --KS--koo = S ; ((K S) ((k o) o)) = S. d 264: S 103 245 226 -> ---S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--koo = ---KK--koo---S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--koo ; (((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))) ((k o) o)) = (((K K) ((k o) o)) (((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)))) ((k o) o))). d 265: K 2 226 -> --KK--koo = K ; ((K K) ((k o) o)) = K. d 266: S 101 244 226 -> ---S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--koo = ---KS--koo---S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--koo ; (((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)))) ((k o) o)) = (((K S) ((k o) o)) (((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))) ((k o) o))). d 267: K 3 226 -> --KS--koo = S ; ((K S) ((k o) o)) = S. d 268: S 232 243 226 -> ---S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--koo = ---K-S-KS--koo---S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--koo ; (((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))) ((k o) o)) = (((K (S (K S))) ((k o) o)) (((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)) ((k o) o))). d 269: K 102 226 -> --K-S-KS--koo = -S-KS ; ((K (S (K S))) ((k o) o)) = (S (K S)). d 270: S 240 242 226 -> ---S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--koo = ----S-KS--S-KK--S-KS--S-KK--S-K!T--koo--Kf--koo ; (((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)) ((k o) o)) = ((((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T))))) ((k o) o)) ((K f) ((k o) o))). d 271: S 101 239 226 -> ---S-KS--S-KK--S-KS--S-KK--S-K!T--koo = ---KS--koo---S-KK--S-KS--S-KK--S-K!T--koo ; (((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T))))) ((k o) o)) = (((K S) ((k o) o)) (((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))) ((k o) o))). d 272: K 3 226 -> --KS--koo = S ; ((K S) ((k o) o)) = S. d 273: S 103 238 226 -> ---S-KK--S-KS--S-KK--S-K!T--koo = ---KK--koo---S-KS--S-KK--S-K!T--koo ; (((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))) ((k o) o)) = (((K K) ((k o) o)) (((S (K S)) ((S (K K)) ((S (K !)) T))) ((k o) o))). d 274: K 2 226 -> --KK--koo = K ; ((K K) ((k o) o)) = K. d 275: S 101 237 226 -> ---S-KS--S-KK--S-K!T--koo = ---KS--koo---S-KK--S-K!T--koo ; (((S (K S)) ((S (K K)) ((S (K !)) T))) ((k o) o)) = (((K S) ((k o) o)) (((S (K K)) ((S (K !)) T)) ((k o) o))). d 276: K 3 226 -> --KS--koo = S ; ((K S) ((k o) o)) = S. d 277: S 103 236 226 -> ---S-KK--S-K!T--koo = ---KK--koo---S-K!T--koo ; (((S (K K)) ((S (K !)) T)) ((k o) o)) = (((K K) ((k o) o)) (((S (K !)) T) ((k o) o))). d 278: K 2 226 -> --KK--koo = K ; ((K K) ((k o) o)) = K. d 279: S 234 81 226 -> ---S-K!T--koo = ---K!--koo-T--koo ; (((S (K !)) T) ((k o) o)) = (((K !) ((k o) o)) (T ((k o) o))). d 280: K 8 226 -> --K!--koo = ! ; ((K !) ((k o) o)) = !. d 281: a 81 226 -> -T--koo = -T--koo ; (T ((k o) o)) = (T ((k o) o)). d 282: a 280 281 -> ---K!--koo-T--koo = -!-T--koo ; (((K !) ((k o) o)) (T ((k o) o))) = (! (T ((k o) o))). d 283: a 8 281 -> -!-T--koo = -!-T--koo ; (! (T ((k o) o))) = (! (T ((k o) o))). d 284: t 279 282 -> ---S-K!T--koo = -!-T--koo ; (((S (K !)) T) ((k o) o)) = (! (T ((k o) o))). d 285: a 278 284 -> ---KK--koo---S-K!T--koo = -K-!-T--koo ; (((K K) ((k o) o)) (((S (K !)) T) ((k o) o))) = (K (! (T ((k o) o)))). d 286: a 2 283 -> -K-!-T--koo = -K-!-T--koo ; (K (! (T ((k o) o)))) = (K (! (T ((k o) o)))). d 287: t 277 285 -> ---S-KK--S-K!T--koo = -K-!-T--koo ; (((S (K K)) ((S (K !)) T)) ((k o) o)) = (K (! (T ((k o) o)))). d 288: a 276 287 -> ---KS--koo---S-KK--S-K!T--koo = -S-K-!-T--koo ; (((K S) ((k o) o)) (((S (K K)) ((S (K !)) T)) ((k o) o))) = (S (K (! (T ((k o) o))))). d 289: a 3 286 -> -S-K-!-T--koo = -S-K-!-T--koo ; (S (K (! (T ((k o) o))))) = (S (K (! (T ((k o) o))))). d 290: t 275 288 -> ---S-KS--S-KK--S-K!T--koo = -S-K-!-T--koo ; (((S (K S)) ((S (K K)) ((S (K !)) T))) ((k o) o)) = (S (K (! (T ((k o) o))))). d 291: a 274 290 -> ---KK--koo---S-KS--S-KK--S-K!T--koo = -K-S-K-!-T--koo ; (((K K) ((k o) o)) (((S (K S)) ((S (K K)) ((S (K !)) T))) ((k o) o))) = (K (S (K (! (T ((k o) o)))))). d 292: a 2 289 -> -K-S-K-!-T--koo = -K-S-K-!-T--koo ; (K (S (K (! (T ((k o) o)))))) = (K (S (K (! (T ((k o) o)))))). d 293: t 273 291 -> ---S-KK--S-KS--S-KK--S-K!T--koo = -K-S-K-!-T--koo ; (((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))) ((k o) o)) = (K (S (K (! (T ((k o) o)))))). d 294: a 272 293 -> ---KS--koo---S-KK--S-KS--S-KK--S-K!T--koo = -S-K-S-K-!-T--koo ; (((K S) ((k o) o)) (((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))) ((k o) o))) = (S (K (S (K (! (T ((k o) o))))))). d 295: a 3 292 -> -S-K-S-K-!-T--koo = -S-K-S-K-!-T--koo ; (S (K (S (K (! (T ((k o) o))))))) = (S (K (S (K (! (T ((k o) o))))))). d 296: t 271 294 -> ---S-KS--S-KK--S-KS--S-KK--S-K!T--koo = -S-K-S-K-!-T--koo ; (((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T))))) ((k o) o)) = (S (K (S (K (! (T ((k o) o))))))). d 297: K 54 226 -> --Kf--koo = f ; ((K f) ((k o) o)) = f. d 298: a 296 297 -> ----S-KS--S-KK--S-KS--S-KK--S-K!T--koo--Kf--koo = --S-K-S-K-!-T--koof ; ((((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T))))) ((k o) o)) ((K f) ((k o) o))) = ((S (K (S (K (! (T ((k o) o))))))) f). d 299: a 295 54 -> --S-K-S-K-!-T--koof = --S-K-S-K-!-T--koof ; ((S (K (S (K (! (T ((k o) o))))))) f) = ((S (K (S (K (! (T ((k o) o))))))) f). d 300: t 270 298 -> ---S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--koo = --S-K-S-K-!-T--koof ; (((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)) ((k o) o)) = ((S (K (S (K (! (T ((k o) o))))))) f). d 301: a 269 300 -> ---K-S-KS--koo---S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--koo = --S-KS--S-K-S-K-!-T--koof ; (((K (S (K S))) ((k o) o)) (((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)) ((k o) o))) = ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f)). d 302: a 102 299 -> --S-KS--S-K-S-K-!-T--koof = --S-KS--S-K-S-K-!-T--koof ; ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f)) = ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f)). d 303: t 268 301 -> ---S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--koo = --S-KS--S-K-S-K-!-T--koof ; (((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))) ((k o) o)) = ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f)). d 304: a 267 303 -> ---KS--koo---S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--koo = -S--S-KS--S-K-S-K-!-T--koof ; (((K S) ((k o) o)) (((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))) ((k o) o))) = (S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))). d 305: a 3 302 -> -S--S-KS--S-K-S-K-!-T--koof = -S--S-KS--S-K-S-K-!-T--koof ; (S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))) = (S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))). d 306: t 266 304 -> ---S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--koo = -S--S-KS--S-K-S-K-!-T--koof ; (((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)))) ((k o) o)) = (S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))). d 307: a 265 306 -> ---KK--koo---S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--koo = -K-S--S-KS--S-K-S-K-!-T--koof ; (((K K) ((k o) o)) (((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)))) ((k o) o))) = (K (S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f)))). d 308: a 2 305 -> -K-S--S-KS--S-K-S-K-!-T--koof = -K-S--S-KS--S-K-S-K-!-T--koof ; (K (S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f)))) = (K (S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f)))). d 309: t 264 307 -> ---S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--koo = -K-S--S-KS--S-K-S-K-!-T--koof ; (((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))) ((k o) o)) = (K (S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f)))). d 310: a 263 309 -> ---KS--koo---S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--koo = -S-K-S--S-KS--S-K-S-K-!-T--koof ; (((K S) ((k o) o)) (((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))) ((k o) o))) = (S (K (S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))))). d 311: a 3 308 -> -S-K-S--S-KS--S-K-S-K-!-T--koof = -S-K-S--S-KS--S-K-S-K-!-T--koof ; (S (K (S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))))) = (S (K (S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))))). d 312: t 262 310 -> ---S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--koo = -S-K-S--S-KS--S-K-S-K-!-T--koof ; (((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)))))) ((k o) o)) = (S (K (S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))))). d 313: S 250 259 226 -> ---S-K-S-K-S-KK--S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--koo = ---K-S-K-S-KK--koo---S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--koo ; (((S (K (S (K (S (K K)))))) ((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &)))) ((k o) o)) = (((K (S (K (S (K K))))) ((k o) o)) (((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &))) ((k o) o))). d 314: K 249 226 -> --K-S-K-S-KK--koo = -S-K-S-KK ; ((K (S (K (S (K K))))) ((k o) o)) = (S (K (S (K K)))). d 315: S 254 258 226 -> ---S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--koo = ---K-S--S-KS--S-K!T--koo---S-K-S-KK--S-K-S-KT&--koo ; (((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &))) ((k o) o)) = (((K (S ((S (K S)) ((S (K !)) T)))) ((k o) o)) (((S (K (S (K K)))) ((S (K (S (K T)))) &)) ((k o) o))). d 316: K 253 226 -> --K-S--S-KS--S-K!T--koo = -S--S-KS--S-K!T ; ((K (S ((S (K S)) ((S (K !)) T)))) ((k o) o)) = (S ((S (K S)) ((S (K !)) T))). d 317: S 248 257 226 -> ---S-K-S-KK--S-K-S-KT&--koo = ---K-S-KK--koo---S-K-S-KT&--koo ; (((S (K (S (K K)))) ((S (K (S (K T)))) &)) ((k o) o)) = (((K (S (K K))) ((k o) o)) (((S (K (S (K T)))) &) ((k o) o))). d 318: K 104 226 -> --K-S-KK--koo = -S-KK ; ((K (S (K K))) ((k o) o)) = (S (K K)). d 319: S 168 80 226 -> ---S-K-S-KT&--koo = ---K-S-KT--koo-&--koo ; (((S (K (S (K T)))) &) ((k o) o)) = (((K (S (K T))) ((k o) o)) (& ((k o) o))). d 320: K 167 226 -> --K-S-KT--koo = -S-KT ; ((K (S (K T))) ((k o) o)) = (S (K T)). d 321: a 80 226 -> -&--koo = -&--koo ; (& ((k o) o)) = (& ((k o) o)). d 322: a 320 321 -> ---K-S-KT--koo-&--koo = --S-KT-&--koo ; (((K (S (K T))) ((k o) o)) (& ((k o) o))) = ((S (K T)) (& ((k o) o))). d 323: a 167 321 -> --S-KT-&--koo = --S-KT-&--koo ; ((S (K T)) (& ((k o) o))) = ((S (K T)) (& ((k o) o))). d 324: t 319 322 -> ---S-K-S-KT&--koo = --S-KT-&--koo ; (((S (K (S (K T)))) &) ((k o) o)) = ((S (K T)) (& ((k o) o))). d 325: a 318 324 -> ---K-S-KK--koo---S-K-S-KT&--koo = --S-KK--S-KT-&--koo ; (((K (S (K K))) ((k o) o)) (((S (K (S (K T)))) &) ((k o) o))) = ((S (K K)) ((S (K T)) (& ((k o) o)))). d 326: a 104 323 -> --S-KK--S-KT-&--koo = --S-KK--S-KT-&--koo ; ((S (K K)) ((S (K T)) (& ((k o) o)))) = ((S (K K)) ((S (K T)) (& ((k o) o)))). d 327: t 317 325 -> ---S-K-S-KK--S-K-S-KT&--koo = --S-KK--S-KT-&--koo ; (((S (K (S (K K)))) ((S (K (S (K T)))) &)) ((k o) o)) = ((S (K K)) ((S (K T)) (& ((k o) o)))). d 328: a 316 327 -> ---K-S--S-KS--S-K!T--koo---S-K-S-KK--S-K-S-KT&--koo = --S--S-KS--S-K!T--S-KK--S-KT-&--koo ; (((K (S ((S (K S)) ((S (K !)) T)))) ((k o) o)) (((S (K (S (K K)))) ((S (K (S (K T)))) &)) ((k o) o))) = ((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k o) o))))). d 329: a 253 326 -> --S--S-KS--S-K!T--S-KK--S-KT-&--koo = --S--S-KS--S-K!T--S-KK--S-KT-&--koo ; ((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k o) o))))) = ((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k o) o))))). d 330: t 315 328 -> ---S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--koo = --S--S-KS--S-K!T--S-KK--S-KT-&--koo ; (((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &))) ((k o) o)) = ((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k o) o))))). d 331: a 314 330 -> ---K-S-K-S-KK--koo---S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--koo = --S-K-S-KK--S--S-KS--S-K!T--S-KK--S-KT-&--koo ; (((K (S (K (S (K K))))) ((k o) o)) (((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &))) ((k o) o))) = ((S (K (S (K K)))) ((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k o) o)))))). d 332: a 249 329 -> --S-K-S-KK--S--S-KS--S-K!T--S-KK--S-KT-&--koo = --S-K-S-KK--S--S-KS--S-K!T--S-KK--S-KT-&--koo ; ((S (K (S (K K)))) ((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k o) o)))))) = ((S (K (S (K K)))) ((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k o) o)))))). d 333: t 313 331 -> ---S-K-S-K-S-KK--S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--koo = --S-K-S-KK--S--S-KS--S-K!T--S-KK--S-KT-&--koo ; (((S (K (S (K (S (K K)))))) ((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &)))) ((k o) o)) = ((S (K (S (K K)))) ((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k o) o)))))). d 334: a 312 333 -> ----S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--koo---S-K-S-K-S-KK--S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--koo = --S-K-S--S-KS--S-K-S-K-!-T--koof--S-K-S-KK--S--S-KS--S-K!T--S-KK--S-KT-&--koo ; ((((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)))))) ((k o) o)) (((S (K (S (K (S (K K)))))) ((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &)))) ((k o) o))) = ((S (K (S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))))) ((S (K (S (K K)))) ((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k o) o))))))). d 335: a 311 332 -> --S-K-S--S-KS--S-K-S-K-!-T--koof--S-K-S-KK--S--S-KS--S-K!T--S-KK--S-KT-&--koo = --S-K-S--S-KS--S-K-S-K-!-T--koof--S-K-S-KK--S--S-KS--S-K!T--S-KK--S-KT-&--koo ; ((S (K (S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))))) ((S (K (S (K K)))) ((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k o) o))))))) = ((S (K (S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))))) ((S (K (S (K K)))) ((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k o) o))))))). d 336: t 261 334 -> ---S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--S-K-S-K-S-KK--S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--koo = --S-K-S--S-KS--S-K-S-K-!-T--koof--S-K-S-KK--S--S-KS--S-K!T--S-KK--S-KT-&--koo ; (((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) ((S (K (S (K (S (K K)))))) ((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &))))) ((k o) o)) = ((S (K (S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))))) ((S (K (S (K K)))) ((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k o) o))))))). d 337: a 336 155 -> ----S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--S-K-S-K-S-KK--S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--koo-io = ---S-K-S--S-KS--S-K-S-K-!-T--koof--S-K-S-KK--S--S-KS--S-K!T--S-KK--S-KT-&--koo-io ; ((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) ((S (K (S (K (S (K K)))))) ((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &))))) ((k o) o)) (i o)) = (((S (K (S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))))) ((S (K (S (K K)))) ((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k o) o))))))) (i o)). d 338: S 308 332 155 -> ---S-K-S--S-KS--S-K-S-K-!-T--koof--S-K-S-KK--S--S-KS--S-K!T--S-KK--S-KT-&--koo-io = ---K-S--S-KS--S-K-S-K-!-T--koof-io---S-K-S-KK--S--S-KS--S-K!T--S-KK--S-KT-&--koo-io ; (((S (K (S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))))) ((S (K (S (K K)))) ((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k o) o))))))) (i o)) = (((K (S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f)))) (i o)) (((S (K (S (K K)))) ((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k o) o)))))) (i o))). d 339: K 305 155 -> --K-S--S-KS--S-K-S-K-!-T--koof-io = -S--S-KS--S-K-S-K-!-T--koof ; ((K (S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f)))) (i o)) = (S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))). d 340: S 248 329 155 -> ---S-K-S-KK--S--S-KS--S-K!T--S-KK--S-KT-&--koo-io = ---K-S-KK-io---S--S-KS--S-K!T--S-KK--S-KT-&--koo-io ; (((S (K (S (K K)))) ((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k o) o)))))) (i o)) = (((K (S (K K))) (i o)) (((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k o) o))))) (i o))). d 341: K 104 155 -> --K-S-KK-io = -S-KK ; ((K (S (K K))) (i o)) = (S (K K)). d 342: S 252 326 155 -> ---S--S-KS--S-K!T--S-KK--S-KT-&--koo-io = ----S-KS--S-K!T-io---S-KK--S-KT-&--koo-io ; (((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k o) o))))) (i o)) = ((((S (K S)) ((S (K !)) T)) (i o)) (((S (K K)) ((S (K T)) (& ((k o) o)))) (i o))). d 343: S 101 236 155 -> ---S-KS--S-K!T-io = ---KS-io---S-K!T-io ; (((S (K S)) ((S (K !)) T)) (i o)) = (((K S) (i o)) (((S (K !)) T) (i o))). d 344: K 3 155 -> --KS-io = S ; ((K S) (i o)) = S. d 345: S 234 81 155 -> ---S-K!T-io = ---K!-io-T-io ; (((S (K !)) T) (i o)) = (((K !) (i o)) (T (i o))). d 346: K 8 155 -> --K!-io = ! ; ((K !) (i o)) = !. d 347: a 346 157 -> ---K!-io-T-io = -!-T-io ; (((K !) (i o)) (T (i o))) = (! (T (i o))). d 348: a 8 157 -> -!-T-io = -!-T-io ; (! (T (i o))) = (! (T (i o))). d 349: t 345 347 -> ---S-K!T-io = -!-T-io ; (((S (K !)) T) (i o)) = (! (T (i o))). d 350: a 344 349 -> ---KS-io---S-K!T-io = -S-!-T-io ; (((K S) (i o)) (((S (K !)) T) (i o))) = (S (! (T (i o)))). d 351: a 3 348 -> -S-!-T-io = -S-!-T-io ; (S (! (T (i o)))) = (S (! (T (i o)))). d 352: t 343 350 -> ---S-KS--S-K!T-io = -S-!-T-io ; (((S (K S)) ((S (K !)) T)) (i o)) = (S (! (T (i o)))). d 353: S 103 323 155 -> ---S-KK--S-KT-&--koo-io = ---KK-io---S-KT-&--koo-io ; (((S (K K)) ((S (K T)) (& ((k o) o)))) (i o)) = (((K K) (i o)) (((S (K T)) (& ((k o) o))) (i o))). d 354: K 2 155 -> --KK-io = K ; ((K K) (i o)) = K. d 355: S 135 321 155 -> ---S-KT-&--koo-io = ---KT-io--&--koo-io ; (((S (K T)) (& ((k o) o))) (i o)) = (((K T) (i o)) ((& ((k o) o)) (i o))). d 356: K 81 155 -> --KT-io = T ; ((K T) (i o)) = T. d 357: a 321 155 -> --&--koo-io = --&--koo-io ; ((& ((k o) o)) (i o)) = ((& ((k o) o)) (i o)). d 358: a 356 357 -> ---KT-io--&--koo-io = -T--&--koo-io ; (((K T) (i o)) ((& ((k o) o)) (i o))) = (T ((& ((k o) o)) (i o))). d 359: a 81 357 -> -T--&--koo-io = -T--&--koo-io ; (T ((& ((k o) o)) (i o))) = (T ((& ((k o) o)) (i o))). d 360: t 355 358 -> ---S-KT-&--koo-io = -T--&--koo-io ; (((S (K T)) (& ((k o) o))) (i o)) = (T ((& ((k o) o)) (i o))). d 361: a 354 360 -> ---KK-io---S-KT-&--koo-io = -K-T--&--koo-io ; (((K K) (i o)) (((S (K T)) (& ((k o) o))) (i o))) = (K (T ((& ((k o) o)) (i o)))). d 362: a 2 359 -> -K-T--&--koo-io = -K-T--&--koo-io ; (K (T ((& ((k o) o)) (i o)))) = (K (T ((& ((k o) o)) (i o)))). d 363: t 353 361 -> ---S-KK--S-KT-&--koo-io = -K-T--&--koo-io ; (((S (K K)) ((S (K T)) (& ((k o) o)))) (i o)) = (K (T ((& ((k o) o)) (i o)))). d 364: a 352 363 -> ----S-KS--S-K!T-io---S-KK--S-KT-&--koo-io = --S-!-T-io-K-T--&--koo-io ; ((((S (K S)) ((S (K !)) T)) (i o)) (((S (K K)) ((S (K T)) (& ((k o) o)))) (i o))) = ((S (! (T (i o)))) (K (T ((& ((k o) o)) (i o))))). d 365: a 351 362 -> --S-!-T-io-K-T--&--koo-io = --S-!-T-io-K-T--&--koo-io ; ((S (! (T (i o)))) (K (T ((& ((k o) o)) (i o))))) = ((S (! (T (i o)))) (K (T ((& ((k o) o)) (i o))))). d 366: t 342 364 -> ---S--S-KS--S-K!T--S-KK--S-KT-&--koo-io = --S-!-T-io-K-T--&--koo-io ; (((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k o) o))))) (i o)) = ((S (! (T (i o)))) (K (T ((& ((k o) o)) (i o))))). d 367: a 341 366 -> ---K-S-KK-io---S--S-KS--S-K!T--S-KK--S-KT-&--koo-io = --S-KK--S-!-T-io-K-T--&--koo-io ; (((K (S (K K))) (i o)) (((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k o) o))))) (i o))) = ((S (K K)) ((S (! (T (i o)))) (K (T ((& ((k o) o)) (i o)))))). d 368: a 104 365 -> --S-KK--S-!-T-io-K-T--&--koo-io = --S-KK--S-!-T-io-K-T--&--koo-io ; ((S (K K)) ((S (! (T (i o)))) (K (T ((& ((k o) o)) (i o)))))) = ((S (K K)) ((S (! (T (i o)))) (K (T ((& ((k o) o)) (i o)))))). d 369: t 340 367 -> ---S-K-S-KK--S--S-KS--S-K!T--S-KK--S-KT-&--koo-io = --S-KK--S-!-T-io-K-T--&--koo-io ; (((S (K (S (K K)))) ((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k o) o)))))) (i o)) = ((S (K K)) ((S (! (T (i o)))) (K (T ((& ((k o) o)) (i o)))))). d 370: a 339 369 -> ---K-S--S-KS--S-K-S-K-!-T--koof-io---S-K-S-KK--S--S-KS--S-K!T--S-KK--S-KT-&--koo-io = --S--S-KS--S-K-S-K-!-T--koof--S-KK--S-!-T-io-K-T--&--koo-io ; (((K (S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f)))) (i o)) (((S (K (S (K K)))) ((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k o) o)))))) (i o))) = ((S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))) ((S (K K)) ((S (! (T (i o)))) (K (T ((& ((k o) o)) (i o))))))). d 371: a 305 368 -> --S--S-KS--S-K-S-K-!-T--koof--S-KK--S-!-T-io-K-T--&--koo-io = --S--S-KS--S-K-S-K-!-T--koof--S-KK--S-!-T-io-K-T--&--koo-io ; ((S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))) ((S (K K)) ((S (! (T (i o)))) (K (T ((& ((k o) o)) (i o))))))) = ((S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))) ((S (K K)) ((S (! (T (i o)))) (K (T ((& ((k o) o)) (i o))))))). d 372: t 338 370 -> ---S-K-S--S-KS--S-K-S-K-!-T--koof--S-K-S-KK--S--S-KS--S-K!T--S-KK--S-KT-&--koo-io = --S--S-KS--S-K-S-K-!-T--koof--S-KK--S-!-T-io-K-T--&--koo-io ; (((S (K (S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))))) ((S (K (S (K K)))) ((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k o) o))))))) (i o)) = ((S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))) ((S (K K)) ((S (! (T (i o)))) (K (T ((& ((k o) o)) (i o))))))). d 373: t 337 372 -> ----S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--S-K-S-K-S-KK--S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--koo-io = --S--S-KS--S-K-S-K-!-T--koof--S-KK--S-!-T-io-K-T--&--koo-io ; ((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) ((S (K (S (K (S (K K)))))) ((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &))))) ((k o) o)) (i o)) = ((S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))) ((S (K K)) ((S (! (T (i o)))) (K (T ((& ((k o) o)) (i o))))))). d 374: a 373 227 -> -----S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--S-K-S-K-S-KK--S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--koo-io-oo = ---S--S-KS--S-K-S-K-!-T--koof--S-KK--S-!-T-io-K-T--&--koo-io-oo ; (((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) ((S (K (S (K (S (K K)))))) ((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &))))) ((k o) o)) (i o)) (o o)) = (((S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))) ((S (K K)) ((S (! (T (i o)))) (K (T ((& ((k o) o)) (i o))))))) (o o)). d 375: S 302 368 227 -> ---S--S-KS--S-K-S-K-!-T--koof--S-KK--S-!-T-io-K-T--&--koo-io-oo = ----S-KS--S-K-S-K-!-T--koof-oo---S-KK--S-!-T-io-K-T--&--koo-io-oo ; (((S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))) ((S (K K)) ((S (! (T (i o)))) (K (T ((& ((k o) o)) (i o))))))) (o o)) = ((((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f)) (o o)) (((S (K K)) ((S (! (T (i o)))) (K (T ((& ((k o) o)) (i o)))))) (o o))). d 376: S 101 299 227 -> ---S-KS--S-K-S-K-!-T--koof-oo = ---KS-oo---S-K-S-K-!-T--koof-oo ; (((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f)) (o o)) = (((K S) (o o)) (((S (K (S (K (! (T ((k o) o))))))) f) (o o))). d 377: K 3 227 -> --KS-oo = S ; ((K S) (o o)) = S. d 378: S 292 54 227 -> ---S-K-S-K-!-T--koof-oo = ---K-S-K-!-T--koo-oo-f-oo ; (((S (K (S (K (! (T ((k o) o))))))) f) (o o)) = (((K (S (K (! (T ((k o) o)))))) (o o)) (f (o o))). d 379: K 289 227 -> --K-S-K-!-T--koo-oo = -S-K-!-T--koo ; ((K (S (K (! (T ((k o) o)))))) (o o)) = (S (K (! (T ((k o) o))))). d 380: a 54 227 -> -f-oo = -f-oo ; (f (o o)) = (f (o o)). d 381: a 379 380 -> ---K-S-K-!-T--koo-oo-f-oo = --S-K-!-T--koo-f-oo ; (((K (S (K (! (T ((k o) o)))))) (o o)) (f (o o))) = ((S (K (! (T ((k o) o))))) (f (o o))). d 382: a 289 380 -> --S-K-!-T--koo-f-oo = --S-K-!-T--koo-f-oo ; ((S (K (! (T ((k o) o))))) (f (o o))) = ((S (K (! (T ((k o) o))))) (f (o o))). d 383: t 378 381 -> ---S-K-S-K-!-T--koof-oo = --S-K-!-T--koo-f-oo ; (((S (K (S (K (! (T ((k o) o))))))) f) (o o)) = ((S (K (! (T ((k o) o))))) (f (o o))). d 384: a 377 383 -> ---KS-oo---S-K-S-K-!-T--koof-oo = -S--S-K-!-T--koo-f-oo ; (((K S) (o o)) (((S (K (S (K (! (T ((k o) o))))))) f) (o o))) = (S ((S (K (! (T ((k o) o))))) (f (o o)))). d 385: a 3 382 -> -S--S-K-!-T--koo-f-oo = -S--S-K-!-T--koo-f-oo ; (S ((S (K (! (T ((k o) o))))) (f (o o)))) = (S ((S (K (! (T ((k o) o))))) (f (o o)))). d 386: t 376 384 -> ---S-KS--S-K-S-K-!-T--koof-oo = -S--S-K-!-T--koo-f-oo ; (((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f)) (o o)) = (S ((S (K (! (T ((k o) o))))) (f (o o)))). d 387: S 103 365 227 -> ---S-KK--S-!-T-io-K-T--&--koo-io-oo = ---KK-oo---S-!-T-io-K-T--&--koo-io-oo ; (((S (K K)) ((S (! (T (i o)))) (K (T ((& ((k o) o)) (i o)))))) (o o)) = (((K K) (o o)) (((S (! (T (i o)))) (K (T ((& ((k o) o)) (i o))))) (o o))). d 388: K 2 227 -> --KK-oo = K ; ((K K) (o o)) = K. d 389: S 348 362 227 -> ---S-!-T-io-K-T--&--koo-io-oo = ---!-T-io-oo--K-T--&--koo-io-oo ; (((S (! (T (i o)))) (K (T ((& ((k o) o)) (i o))))) (o o)) = (((! (T (i o))) (o o)) ((K (T ((& ((k o) o)) (i o)))) (o o))). d 390: a 348 227 -> --!-T-io-oo = --!-T-io-oo ; ((! (T (i o))) (o o)) = ((! (T (i o))) (o o)). d 391: K 359 227 -> --K-T--&--koo-io-oo = -T--&--koo-io ; ((K (T ((& ((k o) o)) (i o)))) (o o)) = (T ((& ((k o) o)) (i o))). d 392: a 390 391 -> ---!-T-io-oo--K-T--&--koo-io-oo = ---!-T-io-oo-T--&--koo-io ; (((! (T (i o))) (o o)) ((K (T ((& ((k o) o)) (i o)))) (o o))) = (((! (T (i o))) (o o)) (T ((& ((k o) o)) (i o)))). d 393: a 390 359 -> ---!-T-io-oo-T--&--koo-io = ---!-T-io-oo-T--&--koo-io ; (((! (T (i o))) (o o)) (T ((& ((k o) o)) (i o)))) = (((! (T (i o))) (o o)) (T ((& ((k o) o)) (i o)))). d 394: t 389 392 -> ---S-!-T-io-K-T--&--koo-io-oo = ---!-T-io-oo-T--&--koo-io ; (((S (! (T (i o)))) (K (T ((& ((k o) o)) (i o))))) (o o)) = (((! (T (i o))) (o o)) (T ((& ((k o) o)) (i o)))). d 395: a 388 394 -> ---KK-oo---S-!-T-io-K-T--&--koo-io-oo = -K---!-T-io-oo-T--&--koo-io ; (((K K) (o o)) (((S (! (T (i o)))) (K (T ((& ((k o) o)) (i o))))) (o o))) = (K (((! (T (i o))) (o o)) (T ((& ((k o) o)) (i o))))). d 396: a 2 393 -> -K---!-T-io-oo-T--&--koo-io = -K---!-T-io-oo-T--&--koo-io ; (K (((! (T (i o))) (o o)) (T ((& ((k o) o)) (i o))))) = (K (((! (T (i o))) (o o)) (T ((& ((k o) o)) (i o))))). d 397: t 387 395 -> ---S-KK--S-!-T-io-K-T--&--koo-io-oo = -K---!-T-io-oo-T--&--koo-io ; (((S (K K)) ((S (! (T (i o)))) (K (T ((& ((k o) o)) (i o)))))) (o o)) = (K (((! (T (i o))) (o o)) (T ((& ((k o) o)) (i o))))). d 398: a 386 397 -> ----S-KS--S-K-S-K-!-T--koof-oo---S-KK--S-!-T-io-K-T--&--koo-io-oo = --S--S-K-!-T--koo-f-oo-K---!-T-io-oo-T--&--koo-io ; ((((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f)) (o o)) (((S (K K)) ((S (! (T (i o)))) (K (T ((& ((k o) o)) (i o)))))) (o o))) = ((S ((S (K (! (T ((k o) o))))) (f (o o)))) (K (((! (T (i o))) (o o)) (T ((& ((k o) o)) (i o)))))). d 399: a 385 396 -> --S--S-K-!-T--koo-f-oo-K---!-T-io-oo-T--&--koo-io = --S--S-K-!-T--koo-f-oo-K---!-T-io-oo-T--&--koo-io ; ((S ((S (K (! (T ((k o) o))))) (f (o o)))) (K (((! (T (i o))) (o o)) (T ((& ((k o) o)) (i o)))))) = ((S ((S (K (! (T ((k o) o))))) (f (o o)))) (K (((! (T (i o))) (o o)) (T ((& ((k o) o)) (i o)))))). d 400: t 375 398 -> ---S--S-KS--S-K-S-K-!-T--koof--S-KK--S-!-T-io-K-T--&--koo-io-oo = --S--S-K-!-T--koo-f-oo-K---!-T-io-oo-T--&--koo-io ; (((S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))) ((S (K K)) ((S (! (T (i o)))) (K (T ((& ((k o) o)) (i o))))))) (o o)) = ((S ((S (K (! (T ((k o) o))))) (f (o o)))) (K (((! (T (i o))) (o o)) (T ((& ((k o) o)) (i o)))))). d 401: t 374 400 -> -----S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--S-K-S-K-S-KK--S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--koo-io-oo = --S--S-K-!-T--koo-f-oo-K---!-T-io-oo-T--&--koo-io ; (((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) ((S (K (S (K (S (K K)))))) ((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &))))) ((k o) o)) (i o)) (o o)) = ((S ((S (K (! (T ((k o) o))))) (f (o o)))) (K (((! (T (i o))) (o o)) (T ((& ((k o) o)) (i o)))))). d 402: a 401 52 -> ------S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--S-K-S-K-S-KK--S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--koo-io-ooo = ---S--S-K-!-T--koo-f-oo-K---!-T-io-oo-T--&--koo-ioo ; ((((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) ((S (K (S (K (S (K K)))))) ((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &))))) ((k o) o)) (i o)) (o o)) o) = (((S ((S (K (! (T ((k o) o))))) (f (o o)))) (K (((! (T (i o))) (o o)) (T ((& ((k o) o)) (i o)))))) o). d 403: S 382 396 52 -> ---S--S-K-!-T--koo-f-oo-K---!-T-io-oo-T--&--koo-ioo = ----S-K-!-T--koo-f-ooo--K---!-T-io-oo-T--&--koo-ioo ; (((S ((S (K (! (T ((k o) o))))) (f (o o)))) (K (((! (T (i o))) (o o)) (T ((& ((k o) o)) (i o)))))) o) = ((((S (K (! (T ((k o) o))))) (f (o o))) o) ((K (((! (T (i o))) (o o)) (T ((& ((k o) o)) (i o))))) o)). d 404: S 286 380 52 -> ---S-K-!-T--koo-f-ooo = ---K-!-T--kooo--f-ooo ; (((S (K (! (T ((k o) o))))) (f (o o))) o) = (((K (! (T ((k o) o)))) o) ((f (o o)) o)). d 405: K 283 52 -> --K-!-T--kooo = -!-T--koo ; ((K (! (T ((k o) o)))) o) = (! (T ((k o) o))). d 406: a 380 52 -> --f-ooo = --f-ooo ; ((f (o o)) o) = ((f (o o)) o). d 407: a 405 406 -> ---K-!-T--kooo--f-ooo = --!-T--koo--f-ooo ; (((K (! (T ((k o) o)))) o) ((f (o o)) o)) = ((! (T ((k o) o))) ((f (o o)) o)). d 408: a 283 406 -> --!-T--koo--f-ooo = --!-T--koo--f-ooo ; ((! (T ((k o) o))) ((f (o o)) o)) = ((! (T ((k o) o))) ((f (o o)) o)). d 409: t 404 407 -> ---S-K-!-T--koo-f-ooo = --!-T--koo--f-ooo ; (((S (K (! (T ((k o) o))))) (f (o o))) o) = ((! (T ((k o) o))) ((f (o o)) o)). d 410: K 393 52 -> --K---!-T-io-oo-T--&--koo-ioo = ---!-T-io-oo-T--&--koo-io ; ((K (((! (T (i o))) (o o)) (T ((& ((k o) o)) (i o))))) o) = (((! (T (i o))) (o o)) (T ((& ((k o) o)) (i o)))). d 411: a 409 410 -> ----S-K-!-T--koo-f-ooo--K---!-T-io-oo-T--&--koo-ioo = ---!-T--koo--f-ooo---!-T-io-oo-T--&--koo-io ; ((((S (K (! (T ((k o) o))))) (f (o o))) o) ((K (((! (T (i o))) (o o)) (T ((& ((k o) o)) (i o))))) o)) = (((! (T ((k o) o))) ((f (o o)) o)) (((! (T (i o))) (o o)) (T ((& ((k o) o)) (i o))))). d 412: a 408 393 -> ---!-T--koo--f-ooo---!-T-io-oo-T--&--koo-io = ---!-T--koo--f-ooo---!-T-io-oo-T--&--koo-io ; (((! (T ((k o) o))) ((f (o o)) o)) (((! (T (i o))) (o o)) (T ((& ((k o) o)) (i o))))) = (((! (T ((k o) o))) ((f (o o)) o)) (((! (T (i o))) (o o)) (T ((& ((k o) o)) (i o))))). d 413: t 403 411 -> ---S--S-K-!-T--koo-f-oo-K---!-T-io-oo-T--&--koo-ioo = ---!-T--koo--f-ooo---!-T-io-oo-T--&--koo-io ; (((S ((S (K (! (T ((k o) o))))) (f (o o)))) (K (((! (T (i o))) (o o)) (T ((& ((k o) o)) (i o)))))) o) = (((! (T ((k o) o))) ((f (o o)) o)) (((! (T (i o))) (o o)) (T ((& ((k o) o)) (i o))))). d 414: t 402 413 -> ------S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--S-K-S-K-S-KK--S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--koo-io-ooo = ---!-T--koo--f-ooo---!-T-io-oo-T--&--koo-io ; ((((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) ((S (K (S (K (S (K K)))))) ((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &))))) ((k o) o)) (i o)) (o o)) o) = (((! (T ((k o) o))) ((f (o o)) o)) (((! (T (i o))) (o o)) (T ((& ((k o) o)) (i o))))). d 415: a 2 236 -> -K--S-K!T = -K--S-K!T ; (K ((S (K !)) T)) = (K ((S (K !)) T)). d 416: S 247 415 226 -> ---S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf-K--S-K!T--koo = ----S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--koo--K--S-K!T--koo ; (((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) (K ((S (K !)) T))) ((k o) o)) = ((((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)))))) ((k o) o)) ((K ((S (K !)) T)) ((k o) o))). d 417: S 101 246 226 -> ---S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--koo = ---KS--koo---S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--koo ; (((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)))))) ((k o) o)) = (((K S) ((k o) o)) (((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))) ((k o) o))). d 418: K 3 226 -> --KS--koo = S ; ((K S) ((k o) o)) = S. d 419: S 103 245 226 -> ---S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--koo = ---KK--koo---S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--koo ; (((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))) ((k o) o)) = (((K K) ((k o) o)) (((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)))) ((k o) o))). d 420: K 2 226 -> --KK--koo = K ; ((K K) ((k o) o)) = K. d 421: S 101 244 226 -> ---S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--koo = ---KS--koo---S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--koo ; (((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)))) ((k o) o)) = (((K S) ((k o) o)) (((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))) ((k o) o))). d 422: K 3 226 -> --KS--koo = S ; ((K S) ((k o) o)) = S. d 423: S 232 243 226 -> ---S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--koo = ---K-S-KS--koo---S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--koo ; (((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))) ((k o) o)) = (((K (S (K S))) ((k o) o)) (((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)) ((k o) o))). d 424: K 102 226 -> --K-S-KS--koo = -S-KS ; ((K (S (K S))) ((k o) o)) = (S (K S)). d 425: S 240 242 226 -> ---S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--koo = ----S-KS--S-KK--S-KS--S-KK--S-K!T--koo--Kf--koo ; (((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)) ((k o) o)) = ((((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T))))) ((k o) o)) ((K f) ((k o) o))). d 426: S 101 239 226 -> ---S-KS--S-KK--S-KS--S-KK--S-K!T--koo = ---KS--koo---S-KK--S-KS--S-KK--S-K!T--koo ; (((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T))))) ((k o) o)) = (((K S) ((k o) o)) (((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))) ((k o) o))). d 427: K 3 226 -> --KS--koo = S ; ((K S) ((k o) o)) = S. d 428: S 103 238 226 -> ---S-KK--S-KS--S-KK--S-K!T--koo = ---KK--koo---S-KS--S-KK--S-K!T--koo ; (((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))) ((k o) o)) = (((K K) ((k o) o)) (((S (K S)) ((S (K K)) ((S (K !)) T))) ((k o) o))). d 429: K 2 226 -> --KK--koo = K ; ((K K) ((k o) o)) = K. d 430: S 101 237 226 -> ---S-KS--S-KK--S-K!T--koo = ---KS--koo---S-KK--S-K!T--koo ; (((S (K S)) ((S (K K)) ((S (K !)) T))) ((k o) o)) = (((K S) ((k o) o)) (((S (K K)) ((S (K !)) T)) ((k o) o))). d 431: K 3 226 -> --KS--koo = S ; ((K S) ((k o) o)) = S. d 432: S 103 236 226 -> ---S-KK--S-K!T--koo = ---KK--koo---S-K!T--koo ; (((S (K K)) ((S (K !)) T)) ((k o) o)) = (((K K) ((k o) o)) (((S (K !)) T) ((k o) o))). d 433: K 2 226 -> --KK--koo = K ; ((K K) ((k o) o)) = K. d 434: S 234 81 226 -> ---S-K!T--koo = ---K!--koo-T--koo ; (((S (K !)) T) ((k o) o)) = (((K !) ((k o) o)) (T ((k o) o))). d 435: K 8 226 -> --K!--koo = ! ; ((K !) ((k o) o)) = !. d 436: t 434 282 -> ---S-K!T--koo = -!-T--koo ; (((S (K !)) T) ((k o) o)) = (! (T ((k o) o))). d 437: t 432 285 -> ---S-KK--S-K!T--koo = -K-!-T--koo ; (((S (K K)) ((S (K !)) T)) ((k o) o)) = (K (! (T ((k o) o)))). d 438: t 430 288 -> ---S-KS--S-KK--S-K!T--koo = -S-K-!-T--koo ; (((S (K S)) ((S (K K)) ((S (K !)) T))) ((k o) o)) = (S (K (! (T ((k o) o))))). d 439: t 428 291 -> ---S-KK--S-KS--S-KK--S-K!T--koo = -K-S-K-!-T--koo ; (((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))) ((k o) o)) = (K (S (K (! (T ((k o) o)))))). d 440: t 426 294 -> ---S-KS--S-KK--S-KS--S-KK--S-K!T--koo = -S-K-S-K-!-T--koo ; (((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T))))) ((k o) o)) = (S (K (S (K (! (T ((k o) o))))))). d 441: K 54 226 -> --Kf--koo = f ; ((K f) ((k o) o)) = f. d 442: t 425 298 -> ---S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--koo = --S-K-S-K-!-T--koof ; (((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)) ((k o) o)) = ((S (K (S (K (! (T ((k o) o))))))) f). d 443: t 423 301 -> ---S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--koo = --S-KS--S-K-S-K-!-T--koof ; (((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))) ((k o) o)) = ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f)). d 444: t 421 304 -> ---S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--koo = -S--S-KS--S-K-S-K-!-T--koof ; (((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)))) ((k o) o)) = (S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))). d 445: t 419 307 -> ---S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--koo = -K-S--S-KS--S-K-S-K-!-T--koof ; (((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))) ((k o) o)) = (K (S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f)))). d 446: t 417 310 -> ---S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--koo = -S-K-S--S-KS--S-K-S-K-!-T--koof ; (((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)))))) ((k o) o)) = (S (K (S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))))). d 447: K 236 226 -> --K--S-K!T--koo = --S-K!T ; ((K ((S (K !)) T)) ((k o) o)) = ((S (K !)) T). d 448: a 446 447 -> ----S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--koo--K--S-K!T--koo = --S-K-S--S-KS--S-K-S-K-!-T--koof--S-K!T ; ((((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)))))) ((k o) o)) ((K ((S (K !)) T)) ((k o) o))) = ((S (K (S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))))) ((S (K !)) T)). d 449: a 311 236 -> --S-K-S--S-KS--S-K-S-K-!-T--koof--S-K!T = --S-K-S--S-KS--S-K-S-K-!-T--koof--S-K!T ; ((S (K (S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))))) ((S (K !)) T)) = ((S (K (S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))))) ((S (K !)) T)). d 450: t 416 448 -> ---S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf-K--S-K!T--koo = --S-K-S--S-KS--S-K-S-K-!-T--koof--S-K!T ; (((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) (K ((S (K !)) T))) ((k o) o)) = ((S (K (S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))))) ((S (K !)) T)). d 451: a 450 155 -> ----S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf-K--S-K!T--koo-io = ---S-K-S--S-KS--S-K-S-K-!-T--koof--S-K!T-io ; ((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) (K ((S (K !)) T))) ((k o) o)) (i o)) = (((S (K (S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))))) ((S (K !)) T)) (i o)). d 452: S 308 236 155 -> ---S-K-S--S-KS--S-K-S-K-!-T--koof--S-K!T-io = ---K-S--S-KS--S-K-S-K-!-T--koof-io---S-K!T-io ; (((S (K (S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))))) ((S (K !)) T)) (i o)) = (((K (S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f)))) (i o)) (((S (K !)) T) (i o))). d 453: K 305 155 -> --K-S--S-KS--S-K-S-K-!-T--koof-io = -S--S-KS--S-K-S-K-!-T--koof ; ((K (S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f)))) (i o)) = (S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))). d 454: S 234 81 155 -> ---S-K!T-io = ---K!-io-T-io ; (((S (K !)) T) (i o)) = (((K !) (i o)) (T (i o))). d 455: K 8 155 -> --K!-io = ! ; ((K !) (i o)) = !. d 456: t 454 347 -> ---S-K!T-io = -!-T-io ; (((S (K !)) T) (i o)) = (! (T (i o))). d 457: a 453 456 -> ---K-S--S-KS--S-K-S-K-!-T--koof-io---S-K!T-io = --S--S-KS--S-K-S-K-!-T--koof-!-T-io ; (((K (S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f)))) (i o)) (((S (K !)) T) (i o))) = ((S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))) (! (T (i o)))). d 458: a 305 348 -> --S--S-KS--S-K-S-K-!-T--koof-!-T-io = --S--S-KS--S-K-S-K-!-T--koof-!-T-io ; ((S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))) (! (T (i o)))) = ((S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))) (! (T (i o)))). d 459: t 452 457 -> ---S-K-S--S-KS--S-K-S-K-!-T--koof--S-K!T-io = --S--S-KS--S-K-S-K-!-T--koof-!-T-io ; (((S (K (S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))))) ((S (K !)) T)) (i o)) = ((S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))) (! (T (i o)))). d 460: t 451 459 -> ----S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf-K--S-K!T--koo-io = --S--S-KS--S-K-S-K-!-T--koof-!-T-io ; ((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) (K ((S (K !)) T))) ((k o) o)) (i o)) = ((S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))) (! (T (i o)))). d 461: a 460 227 -> -----S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf-K--S-K!T--koo-io-oo = ---S--S-KS--S-K-S-K-!-T--koof-!-T-io-oo ; (((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) (K ((S (K !)) T))) ((k o) o)) (i o)) (o o)) = (((S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))) (! (T (i o)))) (o o)). d 462: S 302 348 227 -> ---S--S-KS--S-K-S-K-!-T--koof-!-T-io-oo = ----S-KS--S-K-S-K-!-T--koof-oo--!-T-io-oo ; (((S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))) (! (T (i o)))) (o o)) = ((((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f)) (o o)) ((! (T (i o))) (o o))). d 463: S 101 299 227 -> ---S-KS--S-K-S-K-!-T--koof-oo = ---KS-oo---S-K-S-K-!-T--koof-oo ; (((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f)) (o o)) = (((K S) (o o)) (((S (K (S (K (! (T ((k o) o))))))) f) (o o))). d 464: K 3 227 -> --KS-oo = S ; ((K S) (o o)) = S. d 465: S 292 54 227 -> ---S-K-S-K-!-T--koof-oo = ---K-S-K-!-T--koo-oo-f-oo ; (((S (K (S (K (! (T ((k o) o))))))) f) (o o)) = (((K (S (K (! (T ((k o) o)))))) (o o)) (f (o o))). d 466: K 289 227 -> --K-S-K-!-T--koo-oo = -S-K-!-T--koo ; ((K (S (K (! (T ((k o) o)))))) (o o)) = (S (K (! (T ((k o) o))))). d 467: t 465 381 -> ---S-K-S-K-!-T--koof-oo = --S-K-!-T--koo-f-oo ; (((S (K (S (K (! (T ((k o) o))))))) f) (o o)) = ((S (K (! (T ((k o) o))))) (f (o o))). d 468: t 463 384 -> ---S-KS--S-K-S-K-!-T--koof-oo = -S--S-K-!-T--koo-f-oo ; (((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f)) (o o)) = (S ((S (K (! (T ((k o) o))))) (f (o o)))). d 469: a 468 390 -> ----S-KS--S-K-S-K-!-T--koof-oo--!-T-io-oo = --S--S-K-!-T--koo-f-oo--!-T-io-oo ; ((((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f)) (o o)) ((! (T (i o))) (o o))) = ((S ((S (K (! (T ((k o) o))))) (f (o o)))) ((! (T (i o))) (o o))). d 470: a 385 390 -> --S--S-K-!-T--koo-f-oo--!-T-io-oo = --S--S-K-!-T--koo-f-oo--!-T-io-oo ; ((S ((S (K (! (T ((k o) o))))) (f (o o)))) ((! (T (i o))) (o o))) = ((S ((S (K (! (T ((k o) o))))) (f (o o)))) ((! (T (i o))) (o o))). d 471: t 462 469 -> ---S--S-KS--S-K-S-K-!-T--koof-!-T-io-oo = --S--S-K-!-T--koo-f-oo--!-T-io-oo ; (((S ((S (K S)) ((S (K (S (K (! (T ((k o) o))))))) f))) (! (T (i o)))) (o o)) = ((S ((S (K (! (T ((k o) o))))) (f (o o)))) ((! (T (i o))) (o o))). d 472: t 461 471 -> -----S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf-K--S-K!T--koo-io-oo = --S--S-K-!-T--koo-f-oo--!-T-io-oo ; (((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) (K ((S (K !)) T))) ((k o) o)) (i o)) (o o)) = ((S ((S (K (! (T ((k o) o))))) (f (o o)))) ((! (T (i o))) (o o))). d 473: a 472 52 -> ------S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf-K--S-K!T--koo-io-ooo = ---S--S-K-!-T--koo-f-oo--!-T-io-ooo ; ((((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) (K ((S (K !)) T))) ((k o) o)) (i o)) (o o)) o) = (((S ((S (K (! (T ((k o) o))))) (f (o o)))) ((! (T (i o))) (o o))) o). d 474: S 382 390 52 -> ---S--S-K-!-T--koo-f-oo--!-T-io-ooo = ----S-K-!-T--koo-f-ooo---!-T-io-ooo ; (((S ((S (K (! (T ((k o) o))))) (f (o o)))) ((! (T (i o))) (o o))) o) = ((((S (K (! (T ((k o) o))))) (f (o o))) o) (((! (T (i o))) (o o)) o)). d 475: S 286 380 52 -> ---S-K-!-T--koo-f-ooo = ---K-!-T--kooo--f-ooo ; (((S (K (! (T ((k o) o))))) (f (o o))) o) = (((K (! (T ((k o) o)))) o) ((f (o o)) o)). d 476: K 283 52 -> --K-!-T--kooo = -!-T--koo ; ((K (! (T ((k o) o)))) o) = (! (T ((k o) o))). d 477: t 475 407 -> ---S-K-!-T--koo-f-ooo = --!-T--koo--f-ooo ; (((S (K (! (T ((k o) o))))) (f (o o))) o) = ((! (T ((k o) o))) ((f (o o)) o)). d 478: a 390 52 -> ---!-T-io-ooo = ---!-T-io-ooo ; (((! (T (i o))) (o o)) o) = (((! (T (i o))) (o o)) o). d 479: a 477 478 -> ----S-K-!-T--koo-f-ooo---!-T-io-ooo = ---!-T--koo--f-ooo---!-T-io-ooo ; ((((S (K (! (T ((k o) o))))) (f (o o))) o) (((! (T (i o))) (o o)) o)) = (((! (T ((k o) o))) ((f (o o)) o)) (((! (T (i o))) (o o)) o)). d 480: a 408 478 -> ---!-T--koo--f-ooo---!-T-io-ooo = ---!-T--koo--f-ooo---!-T-io-ooo ; (((! (T ((k o) o))) ((f (o o)) o)) (((! (T (i o))) (o o)) o)) = (((! (T ((k o) o))) ((f (o o)) o)) (((! (T (i o))) (o o)) o)). d 481: t 474 479 -> ---S--S-K-!-T--koo-f-oo--!-T-io-ooo = ---!-T--koo--f-ooo---!-T-io-ooo ; (((S ((S (K (! (T ((k o) o))))) (f (o o)))) ((! (T (i o))) (o o))) o) = (((! (T ((k o) o))) ((f (o o)) o)) (((! (T (i o))) (o o)) o)). d 482: t 473 481 -> ------S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf-K--S-K!T--koo-io-ooo = ---!-T--koo--f-ooo---!-T-io-ooo ; ((((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) (K ((S (K !)) T))) ((k o) o)) (i o)) (o o)) o) = (((! (T ((k o) o))) ((f (o o)) o)) (((! (T (i o))) (o o)) o)). d 483: s 414 -> ---!-T--koo--f-ooo---!-T-io-oo-T--&--koo-io = ------S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--S-K-S-K-S-KK--S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--koo-io-ooo ; (((! (T ((k o) o))) ((f (o o)) o)) (((! (T (i o))) (o o)) (T ((& ((k o) o)) (i o))))) = ((((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) ((S (K (S (K (S (K K)))))) ((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &))))) ((k o) o)) (i o)) (o o)) o). d 484: t 483 231 -> ---!-T--koo--f-ooo---!-T-io-oo-T--&--koo-io = ------S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf-K--S-K!T--koo-io-ooo ; (((! (T ((k o) o))) ((f (o o)) o)) (((! (T (i o))) (o o)) (T ((& ((k o) o)) (i o))))) = ((((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) (K ((S (K !)) T))) ((k o) o)) (i o)) (o o)) o). d 485: t 484 482 -> ---!-T--koo--f-ooo---!-T-io-oo-T--&--koo-io = ---!-T--koo--f-ooo---!-T-io-ooo ; (((! (T ((k o) o))) ((f (o o)) o)) (((! (T (i o))) (o o)) (T ((& ((k o) o)) (i o))))) = (((! (T ((k o) o))) ((f (o o)) o)) (((! (T (i o))) (o o)) o)). d 486: a 73 137 -> -k-fo = -k-fo ; (k (f o)) = (k (f o)). d 487: a 486 52 -> --k-foo = --k-foo ; ((k (f o)) o) = ((k (f o)) o). d 488: a 85 178 -> ---S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--S-K-S-K-S-KK--S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--k--fooo = ---S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf-K--S-K!T--k--fooo ; (((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) ((S (K (S (K (S (K K)))))) ((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &))))) ((k ((f o) o)) o)) = (((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) (K ((S (K !)) T))) ((k ((f o) o)) o)). d 489: a 488 155 -> ----S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--S-K-S-K-S-KK--S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--k--fooo-io = ----S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf-K--S-K!T--k--fooo-io ; ((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) ((S (K (S (K (S (K K)))))) ((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &))))) ((k ((f o) o)) o)) (i o)) = ((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) (K ((S (K !)) T))) ((k ((f o) o)) o)) (i o)). d 490: a 489 140 -> -----S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--S-K-S-K-S-KK--S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--k--fooo-io--foo = -----S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf-K--S-K!T--k--fooo-io--foo ; (((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) ((S (K (S (K (S (K K)))))) ((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &))))) ((k ((f o) o)) o)) (i o)) ((f o) o)) = (((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) (K ((S (K !)) T))) ((k ((f o) o)) o)) (i o)) ((f o) o)). d 491: a 490 52 -> ------S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--S-K-S-K-S-KK--S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--k--fooo-io--fooo = ------S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf-K--S-K!T--k--fooo-io--fooo ; ((((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) ((S (K (S (K (S (K K)))))) ((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &))))) ((k ((f o) o)) o)) (i o)) ((f o) o)) o) = ((((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) (K ((S (K !)) T))) ((k ((f o) o)) o)) (i o)) ((f o) o)) o). d 492: S 247 260 178 -> ---S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--S-K-S-K-S-KK--S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--k--fooo = ----S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--k--fooo---S-K-S-K-S-KK--S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--k--fooo ; (((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) ((S (K (S (K (S (K K)))))) ((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &))))) ((k ((f o) o)) o)) = ((((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)))))) ((k ((f o) o)) o)) (((S (K (S (K (S (K K)))))) ((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &)))) ((k ((f o) o)) o))). d 493: S 101 246 178 -> ---S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--k--fooo = ---KS--k--fooo---S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--k--fooo ; (((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)))))) ((k ((f o) o)) o)) = (((K S) ((k ((f o) o)) o)) (((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))) ((k ((f o) o)) o))). d 494: K 3 178 -> --KS--k--fooo = S ; ((K S) ((k ((f o) o)) o)) = S. d 495: S 103 245 178 -> ---S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--k--fooo = ---KK--k--fooo---S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--k--fooo ; (((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))) ((k ((f o) o)) o)) = (((K K) ((k ((f o) o)) o)) (((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)))) ((k ((f o) o)) o))). d 496: K 2 178 -> --KK--k--fooo = K ; ((K K) ((k ((f o) o)) o)) = K. d 497: S 101 244 178 -> ---S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--k--fooo = ---KS--k--fooo---S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--k--fooo ; (((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)))) ((k ((f o) o)) o)) = (((K S) ((k ((f o) o)) o)) (((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))) ((k ((f o) o)) o))). d 498: K 3 178 -> --KS--k--fooo = S ; ((K S) ((k ((f o) o)) o)) = S. d 499: a 488 155 -> ----S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--S-K-S-K-S-KK--S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--k--fooo-io = ----S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf-K--S-K!T--k--fooo-io ; ((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) ((S (K (S (K (S (K K)))))) ((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &))))) ((k ((f o) o)) o)) (i o)) = ((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) (K ((S (K !)) T))) ((k ((f o) o)) o)) (i o)). d 500: S 232 243 178 -> ---S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--k--fooo = ---K-S-KS--k--fooo---S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--k--fooo ; (((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))) ((k ((f o) o)) o)) = (((K (S (K S))) ((k ((f o) o)) o)) (((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)) ((k ((f o) o)) o))). d 501: K 102 178 -> --K-S-KS--k--fooo = -S-KS ; ((K (S (K S))) ((k ((f o) o)) o)) = (S (K S)). d 502: S 240 242 178 -> ---S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--k--fooo = ----S-KS--S-KK--S-KS--S-KK--S-K!T--k--fooo--Kf--k--fooo ; (((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)) ((k ((f o) o)) o)) = ((((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T))))) ((k ((f o) o)) o)) ((K f) ((k ((f o) o)) o))). d 503: S 101 239 178 -> ---S-KS--S-KK--S-KS--S-KK--S-K!T--k--fooo = ---KS--k--fooo---S-KK--S-KS--S-KK--S-K!T--k--fooo ; (((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T))))) ((k ((f o) o)) o)) = (((K S) ((k ((f o) o)) o)) (((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))) ((k ((f o) o)) o))). d 504: K 3 178 -> --KS--k--fooo = S ; ((K S) ((k ((f o) o)) o)) = S. d 505: S 103 238 178 -> ---S-KK--S-KS--S-KK--S-K!T--k--fooo = ---KK--k--fooo---S-KS--S-KK--S-K!T--k--fooo ; (((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))) ((k ((f o) o)) o)) = (((K K) ((k ((f o) o)) o)) (((S (K S)) ((S (K K)) ((S (K !)) T))) ((k ((f o) o)) o))). d 506: K 2 178 -> --KK--k--fooo = K ; ((K K) ((k ((f o) o)) o)) = K. d 507: S 101 237 178 -> ---S-KS--S-KK--S-K!T--k--fooo = ---KS--k--fooo---S-KK--S-K!T--k--fooo ; (((S (K S)) ((S (K K)) ((S (K !)) T))) ((k ((f o) o)) o)) = (((K S) ((k ((f o) o)) o)) (((S (K K)) ((S (K !)) T)) ((k ((f o) o)) o))). d 508: K 3 178 -> --KS--k--fooo = S ; ((K S) ((k ((f o) o)) o)) = S. d 509: S 103 236 178 -> ---S-KK--S-K!T--k--fooo = ---KK--k--fooo---S-K!T--k--fooo ; (((S (K K)) ((S (K !)) T)) ((k ((f o) o)) o)) = (((K K) ((k ((f o) o)) o)) (((S (K !)) T) ((k ((f o) o)) o))). d 510: K 2 178 -> --KK--k--fooo = K ; ((K K) ((k ((f o) o)) o)) = K. d 511: S 234 81 178 -> ---S-K!T--k--fooo = ---K!--k--fooo-T--k--fooo ; (((S (K !)) T) ((k ((f o) o)) o)) = (((K !) ((k ((f o) o)) o)) (T ((k ((f o) o)) o))). d 512: K 8 178 -> --K!--k--fooo = ! ; ((K !) ((k ((f o) o)) o)) = !. d 513: a 512 180 -> ---K!--k--fooo-T--k--fooo = -!-T--k--fooo ; (((K !) ((k ((f o) o)) o)) (T ((k ((f o) o)) o))) = (! (T ((k ((f o) o)) o))). d 514: a 8 180 -> -!-T--k--fooo = -!-T--k--fooo ; (! (T ((k ((f o) o)) o))) = (! (T ((k ((f o) o)) o))). d 515: t 511 513 -> ---S-K!T--k--fooo = -!-T--k--fooo ; (((S (K !)) T) ((k ((f o) o)) o)) = (! (T ((k ((f o) o)) o))). d 516: a 510 515 -> ---KK--k--fooo---S-K!T--k--fooo = -K-!-T--k--fooo ; (((K K) ((k ((f o) o)) o)) (((S (K !)) T) ((k ((f o) o)) o))) = (K (! (T ((k ((f o) o)) o)))). d 517: a 2 514 -> -K-!-T--k--fooo = -K-!-T--k--fooo ; (K (! (T ((k ((f o) o)) o)))) = (K (! (T ((k ((f o) o)) o)))). d 518: t 509 516 -> ---S-KK--S-K!T--k--fooo = -K-!-T--k--fooo ; (((S (K K)) ((S (K !)) T)) ((k ((f o) o)) o)) = (K (! (T ((k ((f o) o)) o)))). d 519: a 508 518 -> ---KS--k--fooo---S-KK--S-K!T--k--fooo = -S-K-!-T--k--fooo ; (((K S) ((k ((f o) o)) o)) (((S (K K)) ((S (K !)) T)) ((k ((f o) o)) o))) = (S (K (! (T ((k ((f o) o)) o))))). d 520: a 3 517 -> -S-K-!-T--k--fooo = -S-K-!-T--k--fooo ; (S (K (! (T ((k ((f o) o)) o))))) = (S (K (! (T ((k ((f o) o)) o))))). d 521: t 507 519 -> ---S-KS--S-KK--S-K!T--k--fooo = -S-K-!-T--k--fooo ; (((S (K S)) ((S (K K)) ((S (K !)) T))) ((k ((f o) o)) o)) = (S (K (! (T ((k ((f o) o)) o))))). d 522: a 506 521 -> ---KK--k--fooo---S-KS--S-KK--S-K!T--k--fooo = -K-S-K-!-T--k--fooo ; (((K K) ((k ((f o) o)) o)) (((S (K S)) ((S (K K)) ((S (K !)) T))) ((k ((f o) o)) o))) = (K (S (K (! (T ((k ((f o) o)) o)))))). d 523: a 2 520 -> -K-S-K-!-T--k--fooo = -K-S-K-!-T--k--fooo ; (K (S (K (! (T ((k ((f o) o)) o)))))) = (K (S (K (! (T ((k ((f o) o)) o)))))). d 524: t 505 522 -> ---S-KK--S-KS--S-KK--S-K!T--k--fooo = -K-S-K-!-T--k--fooo ; (((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))) ((k ((f o) o)) o)) = (K (S (K (! (T ((k ((f o) o)) o)))))). d 525: a 504 524 -> ---KS--k--fooo---S-KK--S-KS--S-KK--S-K!T--k--fooo = -S-K-S-K-!-T--k--fooo ; (((K S) ((k ((f o) o)) o)) (((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))) ((k ((f o) o)) o))) = (S (K (S (K (! (T ((k ((f o) o)) o))))))). d 526: a 3 523 -> -S-K-S-K-!-T--k--fooo = -S-K-S-K-!-T--k--fooo ; (S (K (S (K (! (T ((k ((f o) o)) o))))))) = (S (K (S (K (! (T ((k ((f o) o)) o))))))). d 527: t 503 525 -> ---S-KS--S-KK--S-KS--S-KK--S-K!T--k--fooo = -S-K-S-K-!-T--k--fooo ; (((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T))))) ((k ((f o) o)) o)) = (S (K (S (K (! (T ((k ((f o) o)) o))))))). d 528: K 54 178 -> --Kf--k--fooo = f ; ((K f) ((k ((f o) o)) o)) = f. d 529: a 527 528 -> ----S-KS--S-KK--S-KS--S-KK--S-K!T--k--fooo--Kf--k--fooo = --S-K-S-K-!-T--k--fooof ; ((((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T))))) ((k ((f o) o)) o)) ((K f) ((k ((f o) o)) o))) = ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f). d 530: a 526 54 -> --S-K-S-K-!-T--k--fooof = --S-K-S-K-!-T--k--fooof ; ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f) = ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f). d 531: t 502 529 -> ---S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--k--fooo = --S-K-S-K-!-T--k--fooof ; (((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)) ((k ((f o) o)) o)) = ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f). d 532: a 501 531 -> ---K-S-KS--k--fooo---S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--k--fooo = --S-KS--S-K-S-K-!-T--k--fooof ; (((K (S (K S))) ((k ((f o) o)) o)) (((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)) ((k ((f o) o)) o))) = ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f)). d 533: a 102 530 -> --S-KS--S-K-S-K-!-T--k--fooof = --S-KS--S-K-S-K-!-T--k--fooof ; ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f)) = ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f)). d 534: t 500 532 -> ---S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--k--fooo = --S-KS--S-K-S-K-!-T--k--fooof ; (((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))) ((k ((f o) o)) o)) = ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f)). d 535: a 498 534 -> ---KS--k--fooo---S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--k--fooo = -S--S-KS--S-K-S-K-!-T--k--fooof ; (((K S) ((k ((f o) o)) o)) (((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))) ((k ((f o) o)) o))) = (S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))). d 536: a 3 533 -> -S--S-KS--S-K-S-K-!-T--k--fooof = -S--S-KS--S-K-S-K-!-T--k--fooof ; (S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))) = (S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))). d 537: t 497 535 -> ---S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--k--fooo = -S--S-KS--S-K-S-K-!-T--k--fooof ; (((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)))) ((k ((f o) o)) o)) = (S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))). d 538: a 496 537 -> ---KK--k--fooo---S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--k--fooo = -K-S--S-KS--S-K-S-K-!-T--k--fooof ; (((K K) ((k ((f o) o)) o)) (((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)))) ((k ((f o) o)) o))) = (K (S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f)))). d 539: a 2 536 -> -K-S--S-KS--S-K-S-K-!-T--k--fooof = -K-S--S-KS--S-K-S-K-!-T--k--fooof ; (K (S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f)))) = (K (S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f)))). d 540: t 495 538 -> ---S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--k--fooo = -K-S--S-KS--S-K-S-K-!-T--k--fooof ; (((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))) ((k ((f o) o)) o)) = (K (S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f)))). d 541: a 494 540 -> ---KS--k--fooo---S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--k--fooo = -S-K-S--S-KS--S-K-S-K-!-T--k--fooof ; (((K S) ((k ((f o) o)) o)) (((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))) ((k ((f o) o)) o))) = (S (K (S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))))). d 542: a 3 539 -> -S-K-S--S-KS--S-K-S-K-!-T--k--fooof = -S-K-S--S-KS--S-K-S-K-!-T--k--fooof ; (S (K (S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))))) = (S (K (S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))))). d 543: t 493 541 -> ---S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--k--fooo = -S-K-S--S-KS--S-K-S-K-!-T--k--fooof ; (((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)))))) ((k ((f o) o)) o)) = (S (K (S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))))). d 544: S 250 259 178 -> ---S-K-S-K-S-KK--S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--k--fooo = ---K-S-K-S-KK--k--fooo---S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--k--fooo ; (((S (K (S (K (S (K K)))))) ((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &)))) ((k ((f o) o)) o)) = (((K (S (K (S (K K))))) ((k ((f o) o)) o)) (((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &))) ((k ((f o) o)) o))). d 545: K 249 178 -> --K-S-K-S-KK--k--fooo = -S-K-S-KK ; ((K (S (K (S (K K))))) ((k ((f o) o)) o)) = (S (K (S (K K)))). d 546: S 254 258 178 -> ---S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--k--fooo = ---K-S--S-KS--S-K!T--k--fooo---S-K-S-KK--S-K-S-KT&--k--fooo ; (((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &))) ((k ((f o) o)) o)) = (((K (S ((S (K S)) ((S (K !)) T)))) ((k ((f o) o)) o)) (((S (K (S (K K)))) ((S (K (S (K T)))) &)) ((k ((f o) o)) o))). d 547: K 253 178 -> --K-S--S-KS--S-K!T--k--fooo = -S--S-KS--S-K!T ; ((K (S ((S (K S)) ((S (K !)) T)))) ((k ((f o) o)) o)) = (S ((S (K S)) ((S (K !)) T))). d 548: S 248 257 178 -> ---S-K-S-KK--S-K-S-KT&--k--fooo = ---K-S-KK--k--fooo---S-K-S-KT&--k--fooo ; (((S (K (S (K K)))) ((S (K (S (K T)))) &)) ((k ((f o) o)) o)) = (((K (S (K K))) ((k ((f o) o)) o)) (((S (K (S (K T)))) &) ((k ((f o) o)) o))). d 549: K 104 178 -> --K-S-KK--k--fooo = -S-KK ; ((K (S (K K))) ((k ((f o) o)) o)) = (S (K K)). d 550: S 168 80 178 -> ---S-K-S-KT&--k--fooo = ---K-S-KT--k--fooo-&--k--fooo ; (((S (K (S (K T)))) &) ((k ((f o) o)) o)) = (((K (S (K T))) ((k ((f o) o)) o)) (& ((k ((f o) o)) o))). d 551: K 167 178 -> --K-S-KT--k--fooo = -S-KT ; ((K (S (K T))) ((k ((f o) o)) o)) = (S (K T)). d 552: a 80 178 -> -&--k--fooo = -&--k--fooo ; (& ((k ((f o) o)) o)) = (& ((k ((f o) o)) o)). d 553: a 551 552 -> ---K-S-KT--k--fooo-&--k--fooo = --S-KT-&--k--fooo ; (((K (S (K T))) ((k ((f o) o)) o)) (& ((k ((f o) o)) o))) = ((S (K T)) (& ((k ((f o) o)) o))). d 554: a 167 552 -> --S-KT-&--k--fooo = --S-KT-&--k--fooo ; ((S (K T)) (& ((k ((f o) o)) o))) = ((S (K T)) (& ((k ((f o) o)) o))). d 555: t 550 553 -> ---S-K-S-KT&--k--fooo = --S-KT-&--k--fooo ; (((S (K (S (K T)))) &) ((k ((f o) o)) o)) = ((S (K T)) (& ((k ((f o) o)) o))). d 556: a 549 555 -> ---K-S-KK--k--fooo---S-K-S-KT&--k--fooo = --S-KK--S-KT-&--k--fooo ; (((K (S (K K))) ((k ((f o) o)) o)) (((S (K (S (K T)))) &) ((k ((f o) o)) o))) = ((S (K K)) ((S (K T)) (& ((k ((f o) o)) o)))). d 557: a 104 554 -> --S-KK--S-KT-&--k--fooo = --S-KK--S-KT-&--k--fooo ; ((S (K K)) ((S (K T)) (& ((k ((f o) o)) o)))) = ((S (K K)) ((S (K T)) (& ((k ((f o) o)) o)))). d 558: t 548 556 -> ---S-K-S-KK--S-K-S-KT&--k--fooo = --S-KK--S-KT-&--k--fooo ; (((S (K (S (K K)))) ((S (K (S (K T)))) &)) ((k ((f o) o)) o)) = ((S (K K)) ((S (K T)) (& ((k ((f o) o)) o)))). d 559: a 547 558 -> ---K-S--S-KS--S-K!T--k--fooo---S-K-S-KK--S-K-S-KT&--k--fooo = --S--S-KS--S-K!T--S-KK--S-KT-&--k--fooo ; (((K (S ((S (K S)) ((S (K !)) T)))) ((k ((f o) o)) o)) (((S (K (S (K K)))) ((S (K (S (K T)))) &)) ((k ((f o) o)) o))) = ((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k ((f o) o)) o))))). d 560: a 253 557 -> --S--S-KS--S-K!T--S-KK--S-KT-&--k--fooo = --S--S-KS--S-K!T--S-KK--S-KT-&--k--fooo ; ((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k ((f o) o)) o))))) = ((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k ((f o) o)) o))))). d 561: t 546 559 -> ---S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--k--fooo = --S--S-KS--S-K!T--S-KK--S-KT-&--k--fooo ; (((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &))) ((k ((f o) o)) o)) = ((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k ((f o) o)) o))))). d 562: a 545 561 -> ---K-S-K-S-KK--k--fooo---S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--k--fooo = --S-K-S-KK--S--S-KS--S-K!T--S-KK--S-KT-&--k--fooo ; (((K (S (K (S (K K))))) ((k ((f o) o)) o)) (((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &))) ((k ((f o) o)) o))) = ((S (K (S (K K)))) ((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k ((f o) o)) o)))))). d 563: a 249 560 -> --S-K-S-KK--S--S-KS--S-K!T--S-KK--S-KT-&--k--fooo = --S-K-S-KK--S--S-KS--S-K!T--S-KK--S-KT-&--k--fooo ; ((S (K (S (K K)))) ((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k ((f o) o)) o)))))) = ((S (K (S (K K)))) ((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k ((f o) o)) o)))))). d 564: t 544 562 -> ---S-K-S-K-S-KK--S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--k--fooo = --S-K-S-KK--S--S-KS--S-K!T--S-KK--S-KT-&--k--fooo ; (((S (K (S (K (S (K K)))))) ((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &)))) ((k ((f o) o)) o)) = ((S (K (S (K K)))) ((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k ((f o) o)) o)))))). d 565: a 543 564 -> ----S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--k--fooo---S-K-S-K-S-KK--S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--k--fooo = --S-K-S--S-KS--S-K-S-K-!-T--k--fooof--S-K-S-KK--S--S-KS--S-K!T--S-KK--S-KT-&--k--fooo ; ((((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)))))) ((k ((f o) o)) o)) (((S (K (S (K (S (K K)))))) ((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &)))) ((k ((f o) o)) o))) = ((S (K (S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))))) ((S (K (S (K K)))) ((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k ((f o) o)) o))))))). d 566: a 542 563 -> --S-K-S--S-KS--S-K-S-K-!-T--k--fooof--S-K-S-KK--S--S-KS--S-K!T--S-KK--S-KT-&--k--fooo = --S-K-S--S-KS--S-K-S-K-!-T--k--fooof--S-K-S-KK--S--S-KS--S-K!T--S-KK--S-KT-&--k--fooo ; ((S (K (S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))))) ((S (K (S (K K)))) ((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k ((f o) o)) o))))))) = ((S (K (S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))))) ((S (K (S (K K)))) ((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k ((f o) o)) o))))))). d 567: t 492 565 -> ---S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--S-K-S-K-S-KK--S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--k--fooo = --S-K-S--S-KS--S-K-S-K-!-T--k--fooof--S-K-S-KK--S--S-KS--S-K!T--S-KK--S-KT-&--k--fooo ; (((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) ((S (K (S (K (S (K K)))))) ((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &))))) ((k ((f o) o)) o)) = ((S (K (S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))))) ((S (K (S (K K)))) ((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k ((f o) o)) o))))))). d 568: a 567 155 -> ----S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--S-K-S-K-S-KK--S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--k--fooo-io = ---S-K-S--S-KS--S-K-S-K-!-T--k--fooof--S-K-S-KK--S--S-KS--S-K!T--S-KK--S-KT-&--k--fooo-io ; ((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) ((S (K (S (K (S (K K)))))) ((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &))))) ((k ((f o) o)) o)) (i o)) = (((S (K (S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))))) ((S (K (S (K K)))) ((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k ((f o) o)) o))))))) (i o)). d 569: S 539 563 155 -> ---S-K-S--S-KS--S-K-S-K-!-T--k--fooof--S-K-S-KK--S--S-KS--S-K!T--S-KK--S-KT-&--k--fooo-io = ---K-S--S-KS--S-K-S-K-!-T--k--fooof-io---S-K-S-KK--S--S-KS--S-K!T--S-KK--S-KT-&--k--fooo-io ; (((S (K (S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))))) ((S (K (S (K K)))) ((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k ((f o) o)) o))))))) (i o)) = (((K (S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f)))) (i o)) (((S (K (S (K K)))) ((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k ((f o) o)) o)))))) (i o))). d 570: K 536 155 -> --K-S--S-KS--S-K-S-K-!-T--k--fooof-io = -S--S-KS--S-K-S-K-!-T--k--fooof ; ((K (S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f)))) (i o)) = (S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))). d 571: S 248 560 155 -> ---S-K-S-KK--S--S-KS--S-K!T--S-KK--S-KT-&--k--fooo-io = ---K-S-KK-io---S--S-KS--S-K!T--S-KK--S-KT-&--k--fooo-io ; (((S (K (S (K K)))) ((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k ((f o) o)) o)))))) (i o)) = (((K (S (K K))) (i o)) (((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k ((f o) o)) o))))) (i o))). d 572: K 104 155 -> --K-S-KK-io = -S-KK ; ((K (S (K K))) (i o)) = (S (K K)). d 573: S 252 557 155 -> ---S--S-KS--S-K!T--S-KK--S-KT-&--k--fooo-io = ----S-KS--S-K!T-io---S-KK--S-KT-&--k--fooo-io ; (((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k ((f o) o)) o))))) (i o)) = ((((S (K S)) ((S (K !)) T)) (i o)) (((S (K K)) ((S (K T)) (& ((k ((f o) o)) o)))) (i o))). d 574: S 101 236 155 -> ---S-KS--S-K!T-io = ---KS-io---S-K!T-io ; (((S (K S)) ((S (K !)) T)) (i o)) = (((K S) (i o)) (((S (K !)) T) (i o))). d 575: K 3 155 -> --KS-io = S ; ((K S) (i o)) = S. d 576: S 234 81 155 -> ---S-K!T-io = ---K!-io-T-io ; (((S (K !)) T) (i o)) = (((K !) (i o)) (T (i o))). d 577: K 8 155 -> --K!-io = ! ; ((K !) (i o)) = !. d 578: t 576 347 -> ---S-K!T-io = -!-T-io ; (((S (K !)) T) (i o)) = (! (T (i o))). d 579: t 574 350 -> ---S-KS--S-K!T-io = -S-!-T-io ; (((S (K S)) ((S (K !)) T)) (i o)) = (S (! (T (i o)))). d 580: S 103 554 155 -> ---S-KK--S-KT-&--k--fooo-io = ---KK-io---S-KT-&--k--fooo-io ; (((S (K K)) ((S (K T)) (& ((k ((f o) o)) o)))) (i o)) = (((K K) (i o)) (((S (K T)) (& ((k ((f o) o)) o))) (i o))). d 581: K 2 155 -> --KK-io = K ; ((K K) (i o)) = K. d 582: S 135 552 155 -> ---S-KT-&--k--fooo-io = ---KT-io--&--k--fooo-io ; (((S (K T)) (& ((k ((f o) o)) o))) (i o)) = (((K T) (i o)) ((& ((k ((f o) o)) o)) (i o))). d 583: K 81 155 -> --KT-io = T ; ((K T) (i o)) = T. d 584: a 552 155 -> --&--k--fooo-io = --&--k--fooo-io ; ((& ((k ((f o) o)) o)) (i o)) = ((& ((k ((f o) o)) o)) (i o)). d 585: a 583 584 -> ---KT-io--&--k--fooo-io = -T--&--k--fooo-io ; (((K T) (i o)) ((& ((k ((f o) o)) o)) (i o))) = (T ((& ((k ((f o) o)) o)) (i o))). d 586: a 81 584 -> -T--&--k--fooo-io = -T--&--k--fooo-io ; (T ((& ((k ((f o) o)) o)) (i o))) = (T ((& ((k ((f o) o)) o)) (i o))). d 587: t 582 585 -> ---S-KT-&--k--fooo-io = -T--&--k--fooo-io ; (((S (K T)) (& ((k ((f o) o)) o))) (i o)) = (T ((& ((k ((f o) o)) o)) (i o))). d 588: a 581 587 -> ---KK-io---S-KT-&--k--fooo-io = -K-T--&--k--fooo-io ; (((K K) (i o)) (((S (K T)) (& ((k ((f o) o)) o))) (i o))) = (K (T ((& ((k ((f o) o)) o)) (i o)))). d 589: a 2 586 -> -K-T--&--k--fooo-io = -K-T--&--k--fooo-io ; (K (T ((& ((k ((f o) o)) o)) (i o)))) = (K (T ((& ((k ((f o) o)) o)) (i o)))). d 590: t 580 588 -> ---S-KK--S-KT-&--k--fooo-io = -K-T--&--k--fooo-io ; (((S (K K)) ((S (K T)) (& ((k ((f o) o)) o)))) (i o)) = (K (T ((& ((k ((f o) o)) o)) (i o)))). d 591: a 579 590 -> ----S-KS--S-K!T-io---S-KK--S-KT-&--k--fooo-io = --S-!-T-io-K-T--&--k--fooo-io ; ((((S (K S)) ((S (K !)) T)) (i o)) (((S (K K)) ((S (K T)) (& ((k ((f o) o)) o)))) (i o))) = ((S (! (T (i o)))) (K (T ((& ((k ((f o) o)) o)) (i o))))). d 592: a 351 589 -> --S-!-T-io-K-T--&--k--fooo-io = --S-!-T-io-K-T--&--k--fooo-io ; ((S (! (T (i o)))) (K (T ((& ((k ((f o) o)) o)) (i o))))) = ((S (! (T (i o)))) (K (T ((& ((k ((f o) o)) o)) (i o))))). d 593: t 573 591 -> ---S--S-KS--S-K!T--S-KK--S-KT-&--k--fooo-io = --S-!-T-io-K-T--&--k--fooo-io ; (((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k ((f o) o)) o))))) (i o)) = ((S (! (T (i o)))) (K (T ((& ((k ((f o) o)) o)) (i o))))). d 594: a 572 593 -> ---K-S-KK-io---S--S-KS--S-K!T--S-KK--S-KT-&--k--fooo-io = --S-KK--S-!-T-io-K-T--&--k--fooo-io ; (((K (S (K K))) (i o)) (((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k ((f o) o)) o))))) (i o))) = ((S (K K)) ((S (! (T (i o)))) (K (T ((& ((k ((f o) o)) o)) (i o)))))). d 595: a 104 592 -> --S-KK--S-!-T-io-K-T--&--k--fooo-io = --S-KK--S-!-T-io-K-T--&--k--fooo-io ; ((S (K K)) ((S (! (T (i o)))) (K (T ((& ((k ((f o) o)) o)) (i o)))))) = ((S (K K)) ((S (! (T (i o)))) (K (T ((& ((k ((f o) o)) o)) (i o)))))). d 596: t 571 594 -> ---S-K-S-KK--S--S-KS--S-K!T--S-KK--S-KT-&--k--fooo-io = --S-KK--S-!-T-io-K-T--&--k--fooo-io ; (((S (K (S (K K)))) ((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k ((f o) o)) o)))))) (i o)) = ((S (K K)) ((S (! (T (i o)))) (K (T ((& ((k ((f o) o)) o)) (i o)))))). d 597: a 570 596 -> ---K-S--S-KS--S-K-S-K-!-T--k--fooof-io---S-K-S-KK--S--S-KS--S-K!T--S-KK--S-KT-&--k--fooo-io = --S--S-KS--S-K-S-K-!-T--k--fooof--S-KK--S-!-T-io-K-T--&--k--fooo-io ; (((K (S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f)))) (i o)) (((S (K (S (K K)))) ((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k ((f o) o)) o)))))) (i o))) = ((S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))) ((S (K K)) ((S (! (T (i o)))) (K (T ((& ((k ((f o) o)) o)) (i o))))))). d 598: a 536 595 -> --S--S-KS--S-K-S-K-!-T--k--fooof--S-KK--S-!-T-io-K-T--&--k--fooo-io = --S--S-KS--S-K-S-K-!-T--k--fooof--S-KK--S-!-T-io-K-T--&--k--fooo-io ; ((S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))) ((S (K K)) ((S (! (T (i o)))) (K (T ((& ((k ((f o) o)) o)) (i o))))))) = ((S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))) ((S (K K)) ((S (! (T (i o)))) (K (T ((& ((k ((f o) o)) o)) (i o))))))). d 599: t 569 597 -> ---S-K-S--S-KS--S-K-S-K-!-T--k--fooof--S-K-S-KK--S--S-KS--S-K!T--S-KK--S-KT-&--k--fooo-io = --S--S-KS--S-K-S-K-!-T--k--fooof--S-KK--S-!-T-io-K-T--&--k--fooo-io ; (((S (K (S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))))) ((S (K (S (K K)))) ((S ((S (K S)) ((S (K !)) T))) ((S (K K)) ((S (K T)) (& ((k ((f o) o)) o))))))) (i o)) = ((S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))) ((S (K K)) ((S (! (T (i o)))) (K (T ((& ((k ((f o) o)) o)) (i o))))))). d 600: t 568 599 -> ----S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--S-K-S-K-S-KK--S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--k--fooo-io = --S--S-KS--S-K-S-K-!-T--k--fooof--S-KK--S-!-T-io-K-T--&--k--fooo-io ; ((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) ((S (K (S (K (S (K K)))))) ((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &))))) ((k ((f o) o)) o)) (i o)) = ((S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))) ((S (K K)) ((S (! (T (i o)))) (K (T ((& ((k ((f o) o)) o)) (i o))))))). d 601: a 600 140 -> -----S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--S-K-S-K-S-KK--S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--k--fooo-io--foo = ---S--S-KS--S-K-S-K-!-T--k--fooof--S-KK--S-!-T-io-K-T--&--k--fooo-io--foo ; (((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) ((S (K (S (K (S (K K)))))) ((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &))))) ((k ((f o) o)) o)) (i o)) ((f o) o)) = (((S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))) ((S (K K)) ((S (! (T (i o)))) (K (T ((& ((k ((f o) o)) o)) (i o))))))) ((f o) o)). d 602: S 533 595 140 -> ---S--S-KS--S-K-S-K-!-T--k--fooof--S-KK--S-!-T-io-K-T--&--k--fooo-io--foo = ----S-KS--S-K-S-K-!-T--k--fooof--foo---S-KK--S-!-T-io-K-T--&--k--fooo-io--foo ; (((S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))) ((S (K K)) ((S (! (T (i o)))) (K (T ((& ((k ((f o) o)) o)) (i o))))))) ((f o) o)) = ((((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f)) ((f o) o)) (((S (K K)) ((S (! (T (i o)))) (K (T ((& ((k ((f o) o)) o)) (i o)))))) ((f o) o))). d 603: S 101 530 140 -> ---S-KS--S-K-S-K-!-T--k--fooof--foo = ---KS--foo---S-K-S-K-!-T--k--fooof--foo ; (((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f)) ((f o) o)) = (((K S) ((f o) o)) (((S (K (S (K (! (T ((k ((f o) o)) o))))))) f) ((f o) o))). d 604: K 3 140 -> --KS--foo = S ; ((K S) ((f o) o)) = S. d 605: S 523 54 140 -> ---S-K-S-K-!-T--k--fooof--foo = ---K-S-K-!-T--k--fooo--foo-f--foo ; (((S (K (S (K (! (T ((k ((f o) o)) o))))))) f) ((f o) o)) = (((K (S (K (! (T ((k ((f o) o)) o)))))) ((f o) o)) (f ((f o) o))). d 606: K 520 140 -> --K-S-K-!-T--k--fooo--foo = -S-K-!-T--k--fooo ; ((K (S (K (! (T ((k ((f o) o)) o)))))) ((f o) o)) = (S (K (! (T ((k ((f o) o)) o))))). d 607: a 606 194 -> ---K-S-K-!-T--k--fooo--foo-f--foo = --S-K-!-T--k--fooo-f--foo ; (((K (S (K (! (T ((k ((f o) o)) o)))))) ((f o) o)) (f ((f o) o))) = ((S (K (! (T ((k ((f o) o)) o))))) (f ((f o) o))). d 608: a 520 194 -> --S-K-!-T--k--fooo-f--foo = --S-K-!-T--k--fooo-f--foo ; ((S (K (! (T ((k ((f o) o)) o))))) (f ((f o) o))) = ((S (K (! (T ((k ((f o) o)) o))))) (f ((f o) o))). d 609: t 605 607 -> ---S-K-S-K-!-T--k--fooof--foo = --S-K-!-T--k--fooo-f--foo ; (((S (K (S (K (! (T ((k ((f o) o)) o))))))) f) ((f o) o)) = ((S (K (! (T ((k ((f o) o)) o))))) (f ((f o) o))). d 610: a 604 609 -> ---KS--foo---S-K-S-K-!-T--k--fooof--foo = -S--S-K-!-T--k--fooo-f--foo ; (((K S) ((f o) o)) (((S (K (S (K (! (T ((k ((f o) o)) o))))))) f) ((f o) o))) = (S ((S (K (! (T ((k ((f o) o)) o))))) (f ((f o) o)))). d 611: a 3 608 -> -S--S-K-!-T--k--fooo-f--foo = -S--S-K-!-T--k--fooo-f--foo ; (S ((S (K (! (T ((k ((f o) o)) o))))) (f ((f o) o)))) = (S ((S (K (! (T ((k ((f o) o)) o))))) (f ((f o) o)))). d 612: t 603 610 -> ---S-KS--S-K-S-K-!-T--k--fooof--foo = -S--S-K-!-T--k--fooo-f--foo ; (((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f)) ((f o) o)) = (S ((S (K (! (T ((k ((f o) o)) o))))) (f ((f o) o)))). d 613: S 103 592 140 -> ---S-KK--S-!-T-io-K-T--&--k--fooo-io--foo = ---KK--foo---S-!-T-io-K-T--&--k--fooo-io--foo ; (((S (K K)) ((S (! (T (i o)))) (K (T ((& ((k ((f o) o)) o)) (i o)))))) ((f o) o)) = (((K K) ((f o) o)) (((S (! (T (i o)))) (K (T ((& ((k ((f o) o)) o)) (i o))))) ((f o) o))). d 614: K 2 140 -> --KK--foo = K ; ((K K) ((f o) o)) = K. d 615: S 348 589 140 -> ---S-!-T-io-K-T--&--k--fooo-io--foo = ---!-T-io--foo--K-T--&--k--fooo-io--foo ; (((S (! (T (i o)))) (K (T ((& ((k ((f o) o)) o)) (i o))))) ((f o) o)) = (((! (T (i o))) ((f o) o)) ((K (T ((& ((k ((f o) o)) o)) (i o)))) ((f o) o))). d 616: a 348 140 -> --!-T-io--foo = --!-T-io--foo ; ((! (T (i o))) ((f o) o)) = ((! (T (i o))) ((f o) o)). d 617: K 586 140 -> --K-T--&--k--fooo-io--foo = -T--&--k--fooo-io ; ((K (T ((& ((k ((f o) o)) o)) (i o)))) ((f o) o)) = (T ((& ((k ((f o) o)) o)) (i o))). d 618: a 616 617 -> ---!-T-io--foo--K-T--&--k--fooo-io--foo = ---!-T-io--foo-T--&--k--fooo-io ; (((! (T (i o))) ((f o) o)) ((K (T ((& ((k ((f o) o)) o)) (i o)))) ((f o) o))) = (((! (T (i o))) ((f o) o)) (T ((& ((k ((f o) o)) o)) (i o)))). d 619: a 616 586 -> ---!-T-io--foo-T--&--k--fooo-io = ---!-T-io--foo-T--&--k--fooo-io ; (((! (T (i o))) ((f o) o)) (T ((& ((k ((f o) o)) o)) (i o)))) = (((! (T (i o))) ((f o) o)) (T ((& ((k ((f o) o)) o)) (i o)))). d 620: t 615 618 -> ---S-!-T-io-K-T--&--k--fooo-io--foo = ---!-T-io--foo-T--&--k--fooo-io ; (((S (! (T (i o)))) (K (T ((& ((k ((f o) o)) o)) (i o))))) ((f o) o)) = (((! (T (i o))) ((f o) o)) (T ((& ((k ((f o) o)) o)) (i o)))). d 621: a 614 620 -> ---KK--foo---S-!-T-io-K-T--&--k--fooo-io--foo = -K---!-T-io--foo-T--&--k--fooo-io ; (((K K) ((f o) o)) (((S (! (T (i o)))) (K (T ((& ((k ((f o) o)) o)) (i o))))) ((f o) o))) = (K (((! (T (i o))) ((f o) o)) (T ((& ((k ((f o) o)) o)) (i o))))). d 622: a 2 619 -> -K---!-T-io--foo-T--&--k--fooo-io = -K---!-T-io--foo-T--&--k--fooo-io ; (K (((! (T (i o))) ((f o) o)) (T ((& ((k ((f o) o)) o)) (i o))))) = (K (((! (T (i o))) ((f o) o)) (T ((& ((k ((f o) o)) o)) (i o))))). d 623: t 613 621 -> ---S-KK--S-!-T-io-K-T--&--k--fooo-io--foo = -K---!-T-io--foo-T--&--k--fooo-io ; (((S (K K)) ((S (! (T (i o)))) (K (T ((& ((k ((f o) o)) o)) (i o)))))) ((f o) o)) = (K (((! (T (i o))) ((f o) o)) (T ((& ((k ((f o) o)) o)) (i o))))). d 624: a 612 623 -> ----S-KS--S-K-S-K-!-T--k--fooof--foo---S-KK--S-!-T-io-K-T--&--k--fooo-io--foo = --S--S-K-!-T--k--fooo-f--foo-K---!-T-io--foo-T--&--k--fooo-io ; ((((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f)) ((f o) o)) (((S (K K)) ((S (! (T (i o)))) (K (T ((& ((k ((f o) o)) o)) (i o)))))) ((f o) o))) = ((S ((S (K (! (T ((k ((f o) o)) o))))) (f ((f o) o)))) (K (((! (T (i o))) ((f o) o)) (T ((& ((k ((f o) o)) o)) (i o)))))). d 625: a 611 622 -> --S--S-K-!-T--k--fooo-f--foo-K---!-T-io--foo-T--&--k--fooo-io = --S--S-K-!-T--k--fooo-f--foo-K---!-T-io--foo-T--&--k--fooo-io ; ((S ((S (K (! (T ((k ((f o) o)) o))))) (f ((f o) o)))) (K (((! (T (i o))) ((f o) o)) (T ((& ((k ((f o) o)) o)) (i o)))))) = ((S ((S (K (! (T ((k ((f o) o)) o))))) (f ((f o) o)))) (K (((! (T (i o))) ((f o) o)) (T ((& ((k ((f o) o)) o)) (i o)))))). d 626: t 602 624 -> ---S--S-KS--S-K-S-K-!-T--k--fooof--S-KK--S-!-T-io-K-T--&--k--fooo-io--foo = --S--S-K-!-T--k--fooo-f--foo-K---!-T-io--foo-T--&--k--fooo-io ; (((S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))) ((S (K K)) ((S (! (T (i o)))) (K (T ((& ((k ((f o) o)) o)) (i o))))))) ((f o) o)) = ((S ((S (K (! (T ((k ((f o) o)) o))))) (f ((f o) o)))) (K (((! (T (i o))) ((f o) o)) (T ((& ((k ((f o) o)) o)) (i o)))))). d 627: t 601 626 -> -----S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--S-K-S-K-S-KK--S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--k--fooo-io--foo = --S--S-K-!-T--k--fooo-f--foo-K---!-T-io--foo-T--&--k--fooo-io ; (((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) ((S (K (S (K (S (K K)))))) ((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &))))) ((k ((f o) o)) o)) (i o)) ((f o) o)) = ((S ((S (K (! (T ((k ((f o) o)) o))))) (f ((f o) o)))) (K (((! (T (i o))) ((f o) o)) (T ((& ((k ((f o) o)) o)) (i o)))))). d 628: a 627 52 -> ------S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--S-K-S-K-S-KK--S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--k--fooo-io--fooo = ---S--S-K-!-T--k--fooo-f--foo-K---!-T-io--foo-T--&--k--fooo-ioo ; ((((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) ((S (K (S (K (S (K K)))))) ((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &))))) ((k ((f o) o)) o)) (i o)) ((f o) o)) o) = (((S ((S (K (! (T ((k ((f o) o)) o))))) (f ((f o) o)))) (K (((! (T (i o))) ((f o) o)) (T ((& ((k ((f o) o)) o)) (i o)))))) o). d 629: S 608 622 52 -> ---S--S-K-!-T--k--fooo-f--foo-K---!-T-io--foo-T--&--k--fooo-ioo = ----S-K-!-T--k--fooo-f--fooo--K---!-T-io--foo-T--&--k--fooo-ioo ; (((S ((S (K (! (T ((k ((f o) o)) o))))) (f ((f o) o)))) (K (((! (T (i o))) ((f o) o)) (T ((& ((k ((f o) o)) o)) (i o)))))) o) = ((((S (K (! (T ((k ((f o) o)) o))))) (f ((f o) o))) o) ((K (((! (T (i o))) ((f o) o)) (T ((& ((k ((f o) o)) o)) (i o))))) o)). d 630: S 517 194 52 -> ---S-K-!-T--k--fooo-f--fooo = ---K-!-T--k--foooo--f--fooo ; (((S (K (! (T ((k ((f o) o)) o))))) (f ((f o) o))) o) = (((K (! (T ((k ((f o) o)) o)))) o) ((f ((f o) o)) o)). d 631: K 514 52 -> --K-!-T--k--foooo = -!-T--k--fooo ; ((K (! (T ((k ((f o) o)) o)))) o) = (! (T ((k ((f o) o)) o))). d 632: a 194 52 -> --f--fooo = --f--fooo ; ((f ((f o) o)) o) = ((f ((f o) o)) o). d 633: a 631 632 -> ---K-!-T--k--foooo--f--fooo = --!-T--k--fooo--f--fooo ; (((K (! (T ((k ((f o) o)) o)))) o) ((f ((f o) o)) o)) = ((! (T ((k ((f o) o)) o))) ((f ((f o) o)) o)). d 634: a 514 632 -> --!-T--k--fooo--f--fooo = --!-T--k--fooo--f--fooo ; ((! (T ((k ((f o) o)) o))) ((f ((f o) o)) o)) = ((! (T ((k ((f o) o)) o))) ((f ((f o) o)) o)). d 635: t 630 633 -> ---S-K-!-T--k--fooo-f--fooo = --!-T--k--fooo--f--fooo ; (((S (K (! (T ((k ((f o) o)) o))))) (f ((f o) o))) o) = ((! (T ((k ((f o) o)) o))) ((f ((f o) o)) o)). d 636: K 619 52 -> --K---!-T-io--foo-T--&--k--fooo-ioo = ---!-T-io--foo-T--&--k--fooo-io ; ((K (((! (T (i o))) ((f o) o)) (T ((& ((k ((f o) o)) o)) (i o))))) o) = (((! (T (i o))) ((f o) o)) (T ((& ((k ((f o) o)) o)) (i o)))). d 637: a 635 636 -> ----S-K-!-T--k--fooo-f--fooo--K---!-T-io--foo-T--&--k--fooo-ioo = ---!-T--k--fooo--f--fooo---!-T-io--foo-T--&--k--fooo-io ; ((((S (K (! (T ((k ((f o) o)) o))))) (f ((f o) o))) o) ((K (((! (T (i o))) ((f o) o)) (T ((& ((k ((f o) o)) o)) (i o))))) o)) = (((! (T ((k ((f o) o)) o))) ((f ((f o) o)) o)) (((! (T (i o))) ((f o) o)) (T ((& ((k ((f o) o)) o)) (i o))))). d 638: a 634 619 -> ---!-T--k--fooo--f--fooo---!-T-io--foo-T--&--k--fooo-io = ---!-T--k--fooo--f--fooo---!-T-io--foo-T--&--k--fooo-io ; (((! (T ((k ((f o) o)) o))) ((f ((f o) o)) o)) (((! (T (i o))) ((f o) o)) (T ((& ((k ((f o) o)) o)) (i o))))) = (((! (T ((k ((f o) o)) o))) ((f ((f o) o)) o)) (((! (T (i o))) ((f o) o)) (T ((& ((k ((f o) o)) o)) (i o))))). d 639: t 629 637 -> ---S--S-K-!-T--k--fooo-f--foo-K---!-T-io--foo-T--&--k--fooo-ioo = ---!-T--k--fooo--f--fooo---!-T-io--foo-T--&--k--fooo-io ; (((S ((S (K (! (T ((k ((f o) o)) o))))) (f ((f o) o)))) (K (((! (T (i o))) ((f o) o)) (T ((& ((k ((f o) o)) o)) (i o)))))) o) = (((! (T ((k ((f o) o)) o))) ((f ((f o) o)) o)) (((! (T (i o))) ((f o) o)) (T ((& ((k ((f o) o)) o)) (i o))))). d 640: t 628 639 -> ------S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--S-K-S-K-S-KK--S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--k--fooo-io--fooo = ---!-T--k--fooo--f--fooo---!-T-io--foo-T--&--k--fooo-io ; ((((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) ((S (K (S (K (S (K K)))))) ((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &))))) ((k ((f o) o)) o)) (i o)) ((f o) o)) o) = (((! (T ((k ((f o) o)) o))) ((f ((f o) o)) o)) (((! (T (i o))) ((f o) o)) (T ((& ((k ((f o) o)) o)) (i o))))). d 641: S 247 415 178 -> ---S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf-K--S-K!T--k--fooo = ----S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--k--fooo--K--S-K!T--k--fooo ; (((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) (K ((S (K !)) T))) ((k ((f o) o)) o)) = ((((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)))))) ((k ((f o) o)) o)) ((K ((S (K !)) T)) ((k ((f o) o)) o))). d 642: S 101 246 178 -> ---S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--k--fooo = ---KS--k--fooo---S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--k--fooo ; (((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)))))) ((k ((f o) o)) o)) = (((K S) ((k ((f o) o)) o)) (((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))) ((k ((f o) o)) o))). d 643: K 3 178 -> --KS--k--fooo = S ; ((K S) ((k ((f o) o)) o)) = S. d 644: S 103 245 178 -> ---S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--k--fooo = ---KK--k--fooo---S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--k--fooo ; (((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))) ((k ((f o) o)) o)) = (((K K) ((k ((f o) o)) o)) (((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)))) ((k ((f o) o)) o))). d 645: K 2 178 -> --KK--k--fooo = K ; ((K K) ((k ((f o) o)) o)) = K. d 646: S 101 244 178 -> ---S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--k--fooo = ---KS--k--fooo---S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--k--fooo ; (((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)))) ((k ((f o) o)) o)) = (((K S) ((k ((f o) o)) o)) (((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))) ((k ((f o) o)) o))). d 647: K 3 178 -> --KS--k--fooo = S ; ((K S) ((k ((f o) o)) o)) = S. d 648: S 232 243 178 -> ---S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--k--fooo = ---K-S-KS--k--fooo---S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--k--fooo ; (((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))) ((k ((f o) o)) o)) = (((K (S (K S))) ((k ((f o) o)) o)) (((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)) ((k ((f o) o)) o))). d 649: K 102 178 -> --K-S-KS--k--fooo = -S-KS ; ((K (S (K S))) ((k ((f o) o)) o)) = (S (K S)). d 650: S 240 242 178 -> ---S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--k--fooo = ----S-KS--S-KK--S-KS--S-KK--S-K!T--k--fooo--Kf--k--fooo ; (((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)) ((k ((f o) o)) o)) = ((((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T))))) ((k ((f o) o)) o)) ((K f) ((k ((f o) o)) o))). d 651: S 101 239 178 -> ---S-KS--S-KK--S-KS--S-KK--S-K!T--k--fooo = ---KS--k--fooo---S-KK--S-KS--S-KK--S-K!T--k--fooo ; (((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T))))) ((k ((f o) o)) o)) = (((K S) ((k ((f o) o)) o)) (((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))) ((k ((f o) o)) o))). d 652: K 3 178 -> --KS--k--fooo = S ; ((K S) ((k ((f o) o)) o)) = S. d 653: S 103 238 178 -> ---S-KK--S-KS--S-KK--S-K!T--k--fooo = ---KK--k--fooo---S-KS--S-KK--S-K!T--k--fooo ; (((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))) ((k ((f o) o)) o)) = (((K K) ((k ((f o) o)) o)) (((S (K S)) ((S (K K)) ((S (K !)) T))) ((k ((f o) o)) o))). d 654: K 2 178 -> --KK--k--fooo = K ; ((K K) ((k ((f o) o)) o)) = K. d 655: S 101 237 178 -> ---S-KS--S-KK--S-K!T--k--fooo = ---KS--k--fooo---S-KK--S-K!T--k--fooo ; (((S (K S)) ((S (K K)) ((S (K !)) T))) ((k ((f o) o)) o)) = (((K S) ((k ((f o) o)) o)) (((S (K K)) ((S (K !)) T)) ((k ((f o) o)) o))). d 656: K 3 178 -> --KS--k--fooo = S ; ((K S) ((k ((f o) o)) o)) = S. d 657: S 103 236 178 -> ---S-KK--S-K!T--k--fooo = ---KK--k--fooo---S-K!T--k--fooo ; (((S (K K)) ((S (K !)) T)) ((k ((f o) o)) o)) = (((K K) ((k ((f o) o)) o)) (((S (K !)) T) ((k ((f o) o)) o))). d 658: K 2 178 -> --KK--k--fooo = K ; ((K K) ((k ((f o) o)) o)) = K. d 659: S 234 81 178 -> ---S-K!T--k--fooo = ---K!--k--fooo-T--k--fooo ; (((S (K !)) T) ((k ((f o) o)) o)) = (((K !) ((k ((f o) o)) o)) (T ((k ((f o) o)) o))). d 660: K 8 178 -> --K!--k--fooo = ! ; ((K !) ((k ((f o) o)) o)) = !. d 661: t 659 513 -> ---S-K!T--k--fooo = -!-T--k--fooo ; (((S (K !)) T) ((k ((f o) o)) o)) = (! (T ((k ((f o) o)) o))). d 662: t 657 516 -> ---S-KK--S-K!T--k--fooo = -K-!-T--k--fooo ; (((S (K K)) ((S (K !)) T)) ((k ((f o) o)) o)) = (K (! (T ((k ((f o) o)) o)))). d 663: t 655 519 -> ---S-KS--S-KK--S-K!T--k--fooo = -S-K-!-T--k--fooo ; (((S (K S)) ((S (K K)) ((S (K !)) T))) ((k ((f o) o)) o)) = (S (K (! (T ((k ((f o) o)) o))))). d 664: t 653 522 -> ---S-KK--S-KS--S-KK--S-K!T--k--fooo = -K-S-K-!-T--k--fooo ; (((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))) ((k ((f o) o)) o)) = (K (S (K (! (T ((k ((f o) o)) o)))))). d 665: t 651 525 -> ---S-KS--S-KK--S-KS--S-KK--S-K!T--k--fooo = -S-K-S-K-!-T--k--fooo ; (((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T))))) ((k ((f o) o)) o)) = (S (K (S (K (! (T ((k ((f o) o)) o))))))). d 666: K 54 178 -> --Kf--k--fooo = f ; ((K f) ((k ((f o) o)) o)) = f. d 667: t 650 529 -> ---S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--k--fooo = --S-K-S-K-!-T--k--fooof ; (((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)) ((k ((f o) o)) o)) = ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f). d 668: t 648 532 -> ---S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--k--fooo = --S-KS--S-K-S-K-!-T--k--fooof ; (((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))) ((k ((f o) o)) o)) = ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f)). d 669: t 646 535 -> ---S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--k--fooo = -S--S-KS--S-K-S-K-!-T--k--fooof ; (((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)))) ((k ((f o) o)) o)) = (S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))). d 670: t 644 538 -> ---S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--k--fooo = -K-S--S-KS--S-K-S-K-!-T--k--fooof ; (((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))) ((k ((f o) o)) o)) = (K (S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f)))). d 671: t 642 541 -> ---S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--k--fooo = -S-K-S--S-KS--S-K-S-K-!-T--k--fooof ; (((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)))))) ((k ((f o) o)) o)) = (S (K (S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))))). d 672: K 236 178 -> --K--S-K!T--k--fooo = --S-K!T ; ((K ((S (K !)) T)) ((k ((f o) o)) o)) = ((S (K !)) T). d 673: a 671 672 -> ----S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--k--fooo--K--S-K!T--k--fooo = --S-K-S--S-KS--S-K-S-K-!-T--k--fooof--S-K!T ; ((((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f)))))) ((k ((f o) o)) o)) ((K ((S (K !)) T)) ((k ((f o) o)) o))) = ((S (K (S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))))) ((S (K !)) T)). d 674: a 542 236 -> --S-K-S--S-KS--S-K-S-K-!-T--k--fooof--S-K!T = --S-K-S--S-KS--S-K-S-K-!-T--k--fooof--S-K!T ; ((S (K (S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))))) ((S (K !)) T)) = ((S (K (S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))))) ((S (K !)) T)). d 675: t 641 673 -> ---S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf-K--S-K!T--k--fooo = --S-K-S--S-KS--S-K-S-K-!-T--k--fooof--S-K!T ; (((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) (K ((S (K !)) T))) ((k ((f o) o)) o)) = ((S (K (S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))))) ((S (K !)) T)). d 676: a 675 155 -> ----S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf-K--S-K!T--k--fooo-io = ---S-K-S--S-KS--S-K-S-K-!-T--k--fooof--S-K!T-io ; ((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) (K ((S (K !)) T))) ((k ((f o) o)) o)) (i o)) = (((S (K (S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))))) ((S (K !)) T)) (i o)). d 677: S 539 236 155 -> ---S-K-S--S-KS--S-K-S-K-!-T--k--fooof--S-K!T-io = ---K-S--S-KS--S-K-S-K-!-T--k--fooof-io---S-K!T-io ; (((S (K (S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))))) ((S (K !)) T)) (i o)) = (((K (S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f)))) (i o)) (((S (K !)) T) (i o))). d 678: K 536 155 -> --K-S--S-KS--S-K-S-K-!-T--k--fooof-io = -S--S-KS--S-K-S-K-!-T--k--fooof ; ((K (S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f)))) (i o)) = (S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))). d 679: S 234 81 155 -> ---S-K!T-io = ---K!-io-T-io ; (((S (K !)) T) (i o)) = (((K !) (i o)) (T (i o))). d 680: K 8 155 -> --K!-io = ! ; ((K !) (i o)) = !. d 681: t 679 347 -> ---S-K!T-io = -!-T-io ; (((S (K !)) T) (i o)) = (! (T (i o))). d 682: a 678 681 -> ---K-S--S-KS--S-K-S-K-!-T--k--fooof-io---S-K!T-io = --S--S-KS--S-K-S-K-!-T--k--fooof-!-T-io ; (((K (S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f)))) (i o)) (((S (K !)) T) (i o))) = ((S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))) (! (T (i o)))). d 683: a 536 348 -> --S--S-KS--S-K-S-K-!-T--k--fooof-!-T-io = --S--S-KS--S-K-S-K-!-T--k--fooof-!-T-io ; ((S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))) (! (T (i o)))) = ((S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))) (! (T (i o)))). d 684: t 677 682 -> ---S-K-S--S-KS--S-K-S-K-!-T--k--fooof--S-K!T-io = --S--S-KS--S-K-S-K-!-T--k--fooof-!-T-io ; (((S (K (S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))))) ((S (K !)) T)) (i o)) = ((S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))) (! (T (i o)))). d 685: t 676 684 -> ----S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf-K--S-K!T--k--fooo-io = --S--S-KS--S-K-S-K-!-T--k--fooof-!-T-io ; ((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) (K ((S (K !)) T))) ((k ((f o) o)) o)) (i o)) = ((S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))) (! (T (i o)))). d 686: a 685 140 -> -----S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf-K--S-K!T--k--fooo-io--foo = ---S--S-KS--S-K-S-K-!-T--k--fooof-!-T-io--foo ; (((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) (K ((S (K !)) T))) ((k ((f o) o)) o)) (i o)) ((f o) o)) = (((S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))) (! (T (i o)))) ((f o) o)). d 687: S 533 348 140 -> ---S--S-KS--S-K-S-K-!-T--k--fooof-!-T-io--foo = ----S-KS--S-K-S-K-!-T--k--fooof--foo--!-T-io--foo ; (((S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))) (! (T (i o)))) ((f o) o)) = ((((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f)) ((f o) o)) ((! (T (i o))) ((f o) o))). d 688: S 101 530 140 -> ---S-KS--S-K-S-K-!-T--k--fooof--foo = ---KS--foo---S-K-S-K-!-T--k--fooof--foo ; (((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f)) ((f o) o)) = (((K S) ((f o) o)) (((S (K (S (K (! (T ((k ((f o) o)) o))))))) f) ((f o) o))). d 689: K 3 140 -> --KS--foo = S ; ((K S) ((f o) o)) = S. d 690: S 523 54 140 -> ---S-K-S-K-!-T--k--fooof--foo = ---K-S-K-!-T--k--fooo--foo-f--foo ; (((S (K (S (K (! (T ((k ((f o) o)) o))))))) f) ((f o) o)) = (((K (S (K (! (T ((k ((f o) o)) o)))))) ((f o) o)) (f ((f o) o))). d 691: K 520 140 -> --K-S-K-!-T--k--fooo--foo = -S-K-!-T--k--fooo ; ((K (S (K (! (T ((k ((f o) o)) o)))))) ((f o) o)) = (S (K (! (T ((k ((f o) o)) o))))). d 692: t 690 607 -> ---S-K-S-K-!-T--k--fooof--foo = --S-K-!-T--k--fooo-f--foo ; (((S (K (S (K (! (T ((k ((f o) o)) o))))))) f) ((f o) o)) = ((S (K (! (T ((k ((f o) o)) o))))) (f ((f o) o))). d 693: t 688 610 -> ---S-KS--S-K-S-K-!-T--k--fooof--foo = -S--S-K-!-T--k--fooo-f--foo ; (((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f)) ((f o) o)) = (S ((S (K (! (T ((k ((f o) o)) o))))) (f ((f o) o)))). d 694: a 693 616 -> ----S-KS--S-K-S-K-!-T--k--fooof--foo--!-T-io--foo = --S--S-K-!-T--k--fooo-f--foo--!-T-io--foo ; ((((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f)) ((f o) o)) ((! (T (i o))) ((f o) o))) = ((S ((S (K (! (T ((k ((f o) o)) o))))) (f ((f o) o)))) ((! (T (i o))) ((f o) o))). d 695: a 611 616 -> --S--S-K-!-T--k--fooo-f--foo--!-T-io--foo = --S--S-K-!-T--k--fooo-f--foo--!-T-io--foo ; ((S ((S (K (! (T ((k ((f o) o)) o))))) (f ((f o) o)))) ((! (T (i o))) ((f o) o))) = ((S ((S (K (! (T ((k ((f o) o)) o))))) (f ((f o) o)))) ((! (T (i o))) ((f o) o))). d 696: t 687 694 -> ---S--S-KS--S-K-S-K-!-T--k--fooof-!-T-io--foo = --S--S-K-!-T--k--fooo-f--foo--!-T-io--foo ; (((S ((S (K S)) ((S (K (S (K (! (T ((k ((f o) o)) o))))))) f))) (! (T (i o)))) ((f o) o)) = ((S ((S (K (! (T ((k ((f o) o)) o))))) (f ((f o) o)))) ((! (T (i o))) ((f o) o))). d 697: t 686 696 -> -----S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf-K--S-K!T--k--fooo-io--foo = --S--S-K-!-T--k--fooo-f--foo--!-T-io--foo ; (((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) (K ((S (K !)) T))) ((k ((f o) o)) o)) (i o)) ((f o) o)) = ((S ((S (K (! (T ((k ((f o) o)) o))))) (f ((f o) o)))) ((! (T (i o))) ((f o) o))). d 698: a 697 52 -> ------S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf-K--S-K!T--k--fooo-io--fooo = ---S--S-K-!-T--k--fooo-f--foo--!-T-io--fooo ; ((((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) (K ((S (K !)) T))) ((k ((f o) o)) o)) (i o)) ((f o) o)) o) = (((S ((S (K (! (T ((k ((f o) o)) o))))) (f ((f o) o)))) ((! (T (i o))) ((f o) o))) o). d 699: S 608 616 52 -> ---S--S-K-!-T--k--fooo-f--foo--!-T-io--fooo = ----S-K-!-T--k--fooo-f--fooo---!-T-io--fooo ; (((S ((S (K (! (T ((k ((f o) o)) o))))) (f ((f o) o)))) ((! (T (i o))) ((f o) o))) o) = ((((S (K (! (T ((k ((f o) o)) o))))) (f ((f o) o))) o) (((! (T (i o))) ((f o) o)) o)). d 700: S 517 194 52 -> ---S-K-!-T--k--fooo-f--fooo = ---K-!-T--k--foooo--f--fooo ; (((S (K (! (T ((k ((f o) o)) o))))) (f ((f o) o))) o) = (((K (! (T ((k ((f o) o)) o)))) o) ((f ((f o) o)) o)). d 701: K 514 52 -> --K-!-T--k--foooo = -!-T--k--fooo ; ((K (! (T ((k ((f o) o)) o)))) o) = (! (T ((k ((f o) o)) o))). d 702: t 700 633 -> ---S-K-!-T--k--fooo-f--fooo = --!-T--k--fooo--f--fooo ; (((S (K (! (T ((k ((f o) o)) o))))) (f ((f o) o))) o) = ((! (T ((k ((f o) o)) o))) ((f ((f o) o)) o)). d 703: a 616 52 -> ---!-T-io--fooo = ---!-T-io--fooo ; (((! (T (i o))) ((f o) o)) o) = (((! (T (i o))) ((f o) o)) o). d 704: a 702 703 -> ----S-K-!-T--k--fooo-f--fooo---!-T-io--fooo = ---!-T--k--fooo--f--fooo---!-T-io--fooo ; ((((S (K (! (T ((k ((f o) o)) o))))) (f ((f o) o))) o) (((! (T (i o))) ((f o) o)) o)) = (((! (T ((k ((f o) o)) o))) ((f ((f o) o)) o)) (((! (T (i o))) ((f o) o)) o)). d 705: a 634 703 -> ---!-T--k--fooo--f--fooo---!-T-io--fooo = ---!-T--k--fooo--f--fooo---!-T-io--fooo ; (((! (T ((k ((f o) o)) o))) ((f ((f o) o)) o)) (((! (T (i o))) ((f o) o)) o)) = (((! (T ((k ((f o) o)) o))) ((f ((f o) o)) o)) (((! (T (i o))) ((f o) o)) o)). d 706: t 699 704 -> ---S--S-K-!-T--k--fooo-f--foo--!-T-io--fooo = ---!-T--k--fooo--f--fooo---!-T-io--fooo ; (((S ((S (K (! (T ((k ((f o) o)) o))))) (f ((f o) o)))) ((! (T (i o))) ((f o) o))) o) = (((! (T ((k ((f o) o)) o))) ((f ((f o) o)) o)) (((! (T (i o))) ((f o) o)) o)). d 707: t 698 706 -> ------S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf-K--S-K!T--k--fooo-io--fooo = ---!-T--k--fooo--f--fooo---!-T-io--fooo ; ((((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) (K ((S (K !)) T))) ((k ((f o) o)) o)) (i o)) ((f o) o)) o) = (((! (T ((k ((f o) o)) o))) ((f ((f o) o)) o)) (((! (T (i o))) ((f o) o)) o)). d 708: s 640 -> ---!-T--k--fooo--f--fooo---!-T-io--foo-T--&--k--fooo-io = ------S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf--S-K-S-K-S-KK--S-K-S--S-KS--S-K!T--S-K-S-KK--S-K-S-KT&--k--fooo-io--fooo ; (((! (T ((k ((f o) o)) o))) ((f ((f o) o)) o)) (((! (T (i o))) ((f o) o)) (T ((& ((k ((f o) o)) o)) (i o))))) = ((((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) ((S (K (S (K (S (K K)))))) ((S (K (S ((S (K S)) ((S (K !)) T))))) ((S (K (S (K K)))) ((S (K (S (K T)))) &))))) ((k ((f o) o)) o)) (i o)) ((f o) o)) o). d 709: t 708 491 -> ---!-T--k--fooo--f--fooo---!-T-io--foo-T--&--k--fooo-io = ------S--S-KS--S-KK--S-KS--S-K-S-KS--S--S-KS--S-KK--S-KS--S-KK--S-K!T-Kf-K--S-K!T--k--fooo-io--fooo ; (((! (T ((k ((f o) o)) o))) ((f ((f o) o)) o)) (((! (T (i o))) ((f o) o)) (T ((& ((k ((f o) o)) o)) (i o))))) = ((((((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K K)) ((S (K !)) T)))))) (K f))))))) (K ((S (K !)) T))) ((k ((f o) o)) o)) (i o)) ((f o) o)) o). d 710: t 709 707 -> ---!-T--k--fooo--f--fooo---!-T-io--foo-T--&--k--fooo-io = ---!-T--k--fooo--f--fooo---!-T-io--fooo ; (((! (T ((k ((f o) o)) o))) ((f ((f o) o)) o)) (((! (T (i o))) ((f o) o)) (T ((& ((k ((f o) o)) o)) (i o))))) = (((! (T ((k ((f o) o)) o))) ((f ((f o) o)) o)) (((! (T (i o))) ((f o) o)) o)).