In order to generate the 6-element non-distributive BCK+ matrices reported in the paper, all one needs to do is run MaGIC on the ->, &, v, t, T, F fragment of its built-in system LCK, using the formula (p & (q v r)) -> ((p & q) v (p & r)) as the `badguy'. NOTE: MaGIC only outputs the implication matrix. To generate the matrices for the other connectives, we used MACE (see MACE_BCK.in). Here is the output from just such a MaGIC run: Logic: LCK Fragment: ->, &, v, t, T, F Fail: (p & (q v r)) -> ((p & q) v (p & r)) TTY output: pretty File output: none Search concludes when 1 matrix found or when size 8 finished. A)xiom B)adguy C)onnective D)elete E)xit F)ragment G)enerate H)elp I)O J)ump K)ill L)ogic M)aGIC N)o. Procs O)rder P)rint Opts Q)uit R)ead S)tore g Searching..... Size: 6 Order 6.1 < | 0 1 2 3 4 5 --+------------ 0 | + + + + + + 1 | - + - + + + 2 | - - + - + + 3 | - - - + + + 4 | - - - - + + 5 | - - - - - + Choice 6.1.1 of t: 5 Implication matrix 6.1.1.1 -> | 0 1 2 3 4 5 ---+------------ 0 | 5 5 5 5 5 5 1 | 2 5 2 5 5 5 2 | 3 3 5 3 5 5 3 | 2 4 2 5 5 5 4 | 0 3 2 3 5 5 5 | 0 1 2 3 4 5 Failure: (3 & (2 v 1)) -> ((3 & 2) v (3 & 1))