% This set of miscellaneous non-BA structures were % found in ad hoc ways. interpretation(2, [ function(or(_,_), [1,0, 0,0]), function(not(_), [0,0]) ]). interpretation(8, [ function(or(_,_), [0,1,7,4,6,2,5,3, 1,1,1,1,1,1,1,1, 7,1,7,1,1,2,1,7, 4,1,1,4,4,1,1,3, 6,1,1,4,6,1,6,1, 2,1,2,1,1,2,5,1, 5,1,1,1,6,5,5,1, 3,1,7,3,1,1,1,3]), function(not(_), [1,0,3,6,5,7,2,4]) ]). interpretation(4, [ function(or(_,_), [0,0,0,0, 1,1,1,1, 2,2,2,2, 3,3,3,3]), function(not(_), [0,1,2,3]) ]). interpretation(4, [ function(or(_,_), [0,0,0,0, 2,1,0,3, 2,2,2,2, 0,1,2,3]), function(not(_), [1,0,3,2]) ]). interpretation(4, [ function(or(_,_), [0,0,0,0, 2,1,0,3, 2,2,2,2, 0,1,2,3]), function(not(_), [1,2,3,0]) ]). interpretation(4, [ function(or(_,_), [0,0,0,0, 2,1,0,3, 2,2,2,2, 2,1,0,3]), function(not(_), [1,0,3,2]) ]). interpretation(4, [ function(or(_,_), [0,0,0,0, 2,1,0,3, 2,2,2,2, 2,1,0,3]), function(not(_), [1,2,3,0]) ]). interpretation(4, [ function(or(_,_), [0,0,1,1, 2,2,3,3, 0,0,1,1, 2,2,3,3]), function(not(_), [0,1,2,3]) ]). interpretation(4, [ function(or(_,_), [0,1,2,3, 0,1,2,3, 0,1,2,3, 0,1,2,3]), function(not(_), [0,1,2,3]) ]). interpretation(4, [ function(or(_,_), [0,2,0,2, 0,2,0,2, 1,3,1,3, 1,3,1,3]), function(not(_), [0,1,2,3]) ]). interpretation(4, [ function(or(_,_), [1,0,0,0, 0,1,2,3, 0,2,0,0, 0,3,0,0]), function(not(_), [1,1,0,0]) ]). interpretation(4, [ function(or(_,_), [1,0,0,0, 0,1,2,3, 0,2,0,0, 0,3,0,0]), function(not(_), [1,1,1,1]) ]). interpretation(4, [ function(or(_,_), [1,0,0,3, 0,1,1,3, 0,1,2,2, 3,3,2,3]), function(not(_), [1,1,3,2]) ]). interpretation(4, [ function(or(_,_), [1,0,0,3, 0,1,1,3, 0,1,2,3, 3,3,3,3]), function(not(_), [1,1,3,2]) ]). interpretation(4, [ function(or(_,_), [1,0,1,0, 0,0,1,1, 1,1,3,2, 0,1,2,3]), function(not(_), [0,2,2,2]) ]). interpretation(4, [ function(or(_,_), [1,0,1,0, 0,1,1,0, 1,1,2,3, 0,0,3,3]), function(not(_), [1,2,1,1]) ]). interpretation(4, [ function(or(_,_), [1,0,1,1, 0,2,3,1, 1,3,2,3, 1,1,3,3]), function(not(_), [1,2,2,2]) ]). interpretation(4, [ function(or(_,_), [1,0,2,0, 0,1,2,3, 2,2,2,2, 0,3,2,1]), function(not(_), [0,2,1,3]) ]). interpretation(4, [ function(or(_,_), [1,1,0,1, 1,1,1,1, 0,1,2,3, 1,1,3,1]), function(not(_), [0,2,1,3]) ]). interpretation(4, [ function(or(_,_), [1,1,3,0, 1,1,1,1, 3,1,2,3, 0,1,3,3]), function(not(_), [1,2,0,2]) ]). interpretation(4, [ function(or(_,_), [1,1,3,0, 1,1,1,1, 3,1,2,3, 0,1,3,3]), function(not(_), [1,2,1,1]) ]). interpretation(4, [ function(or(_,_), [1,1,3,0, 1,1,1,3, 3,1,2,1, 0,3,1,0]), function(not(_), [1,2,1,2]) ]). interpretation(4, [ function(or(_,_), [1,2,2,1, 2,0,2,0, 2,2,2,2, 1,0,2,3]), function(not(_), [0,1,3,2]) ]). interpretation(4, [ function(or(_,_), [1,2,2,1, 2,0,2,0, 2,2,2,2, 1,0,2,3]), function(not(_), [1,0,3,2]) ]). interpretation(4, [ function(or(_,_), [1,3,1,3, 1,3,1,3, 0,2,0,2, 0,2,0,2]), function(not(_), [1,0,3,2]) ]). % This set of noncommutative structures was obtained by going through % the xxxyzzz=z single axiom candidates with sem (2 seconds each). % See /home/mccune/exp/ornot/xxxyzzz/README. % Models from idx.01 (0 -> 0). % Models from idx.02 (192 -> 192). % Models from idx.03 (64 -> 64). interpretation(4, [ function(or(_,_), [ 0,0,1,1, 0,0,1,0, 2,2,3,3, 0,0,1,0 ]), function(not(_), [0,2,0,2]) ]). interpretation(4, [ function(or(_,_), [ 0,0,1,1, 0,0,1,1, 2,0,3,1, 0,0,3,1 ]), function(not(_), [0,2,0,2]) ]). interpretation(4, [ function(or(_,_), [ 0,0,1,1, 0,0,1,1, 2,2,3,3, 0,0,1,1 ]), function(not(_), [0,2,0,2]) ]). interpretation(4, [ function(or(_,_), [ 0,0,2,2, 1,1,3,3, 0,0,2,2, 1,1,3,3 ]), function(not(_), [0,2,1,3]) ]). % Models from idx.04 (64 -> 24). % Models from idx.05 (384 -> 252). interpretation(4, [ function(or(_,_), [ 0,0,1,1, 0,0,2,0, 3,3,2,2, 0,0,0,0 ]), function(not(_), [0,2,2,0]) ]). interpretation(4, [ function(or(_,_), [ 0,0,1,1, 0,0,2,1, 3,0,2,1, 0,0,2,1 ]), function(not(_), [0,2,2,0]) ]). interpretation(4, [ function(or(_,_), [ 0,0,1,1, 0,0,2,1, 3,3,2,2, 0,0,1,1 ]), function(not(_), [0,2,2,0]) ]). interpretation(4, [ function(or(_,_), [ 0,0,2,0, 0,1,2,3, 2,2,2,0, 0,3,2,0 ]), function(not(_), [0,2,1,2]) ]). interpretation(4, [ function(or(_,_), [ 0,0,2,0, 0,1,2,3, 2,2,2,2, 0,3,0,0 ]), function(not(_), [0,2,1,2]) ]). interpretation(4, [ function(or(_,_), [ 0,0,2,0, 0,1,2,3, 2,2,2,2, 0,3,3,2 ]), function(not(_), [0,2,1,2]) ]). interpretation(4, [ function(or(_,_), [ 0,0,2,2, 1,1,3,3, 2,2,0,0, 3,3,1,1 ]), function(not(_), [0,2,1,3]) ]). interpretation(4, [ function(or(_,_), [ 0,0,2,3, 0,1,2,3, 2,2,2,2, 3,3,3,0 ]), function(not(_), [0,2,1,1]) ]). interpretation(4, [ function(or(_,_), [ 0,0,2,3, 0,1,2,3, 2,2,2,2, 3,3,3,2 ]), function(not(_), [0,2,1,1]) ]). interpretation(4, [ function(or(_,_), [ 0,0,3,1, 0,0,1,0, 0,1,3,2, 2,0,1,0 ]), function(not(_), [0,2,2,0]) ]). interpretation(4, [ function(or(_,_), [ 0,0,3,1, 0,0,1,1, 0,1,3,2, 2,0,1,1 ]), function(not(_), [0,2,2,0]) ]). % Models from idx.06 (448 -> 268). interpretation(4, [ function(or(_,_), [ 0,0,3,1, 0,0,3,1, 1,0,2,0, 1,0,2,0 ]), function(not(_), [0,2,2,0]) ]). % Models from idx.07 (448 -> 220). % Models from idx.08 (512 -> 252). % Models from idx.09 (384 -> 384). % Models from idx.10 (288 -> 120). % Models from idx.11 (1184 -> 384). interpretation(4, [ function(or(_,_), [ 0,0,1,0, 0,0,2,0, 1,2,1,3, 3,0,0,0 ]), function(not(_), [0,2,2,2]) ]). interpretation(4, [ function(or(_,_), [ 0,0,1,0, 0,0,2,3, 1,2,1,3, 3,0,0,3 ]), function(not(_), [0,2,2,2]) ]). interpretation(4, [ function(or(_,_), [ 0,0,1,0, 1,0,0,0, 0,1,2,3, 3,0,0,0 ]), function(not(_), [0,2,2,2]) ]). interpretation(4, [ function(or(_,_), [ 0,0,1,0, 1,0,1,3, 0,1,2,3, 3,0,0,3 ]), function(not(_), [0,2,2,2]) ]). interpretation(4, [ function(or(_,_), [ 0,0,1,2, 1,0,1,1, 2,1,3,0, 2,0,2,1 ]), function(not(_), [0,2,0,2]) ]). interpretation(4, [ function(or(_,_), [ 0,0,1,3, 0,0,1,0, 1,0,3,2, 3,0,1,0 ]), function(not(_), [0,2,2,0]) ]). interpretation(4, [ function(or(_,_), [ 0,0,1,3, 0,0,1,0, 1,1,3,2, 3,0,1,0 ]), function(not(_), [0,2,2,0]) ]). interpretation(4, [ function(or(_,_), [ 0,0,1,3, 0,0,2,0, 1,2,1,0, 3,0,3,0 ]), function(not(_), [0,2,2,0]) ]). interpretation(4, [ function(or(_,_), [ 0,0,1,3, 0,0,2,0, 1,2,1,1, 2,0,3,2 ]), function(not(_), [0,2,2,0]) ]). interpretation(4, [ function(or(_,_), [ 0,0,1,3, 0,2,1,2, 1,2,3,2, 3,0,1,0 ]), function(not(_), [0,2,2,0]) ]). interpretation(4, [ function(or(_,_), [ 0,0,1,3, 1,0,0,0, 3,1,2,2, 3,0,0,0 ]), function(not(_), [0,2,2,0]) ]). interpretation(4, [ function(or(_,_), [ 0,0,1,3, 1,0,1,0, 3,1,2,2, 3,0,0,0 ]), function(not(_), [0,2,2,0]) ]). interpretation(4, [ function(or(_,_), [ 0,0,1,3, 1,0,1,0, 3,1,2,2, 3,0,3,0 ]), function(not(_), [0,2,2,0]) ]). interpretation(4, [ function(or(_,_), [ 0,0,2,0, 0,1,2,3, 2,2,2,3, 0,3,0,2 ]), function(not(_), [0,2,1,2]) ]). interpretation(4, [ function(or(_,_), [ 0,0,2,0, 0,1,2,3, 2,2,2,3, 0,3,2,2 ]), function(not(_), [0,2,1,2]) ]). interpretation(4, [ function(or(_,_), [ 0,0,2,3, 0,1,1,3, 2,1,2,1, 3,3,2,0 ]), function(not(_), [0,2,1,0]) ]). interpretation(4, [ function(or(_,_), [ 0,0,2,3, 0,1,1,3, 2,1,2,2, 3,3,1,0 ]), function(not(_), [0,2,1,0]) ]). interpretation(4, [ function(or(_,_), [ 0,0,2,3, 0,1,2,3, 2,2,2,3, 3,3,2,0 ]), function(not(_), [0,2,1,1]) ]). interpretation(4, [ function(or(_,_), [ 0,0,3,0, 1,1,3,1, 0,0,3,0, 2,1,3,2 ]), function(not(_), [0,2,2,3]) ]). interpretation(4, [ function(or(_,_), [ 0,0,3,0, 1,1,3,2, 0,3,3,0, 2,2,3,0 ]), function(not(_), [0,2,2,1]) ]). % Models from idx.12 (512 -> 86). % Models from idx.13 (224 -> 200). interpretation(4, [ function(or(_,_), [ 0,0,3,3, 2,2,1,1, 1,1,2,2, 3,3,0,0 ]), function(not(_), [0,3,2,1]) ]). % Models from idx.14 (672 -> 360). % Models from idx.15 (1152 -> 916). interpretation(4, [ function(or(_,_), [ 0,0,1,1, 0,0,2,0, 3,3,3,2, 2,3,3,2 ]), function(not(_), [0,2,2,0]) ]). interpretation(4, [ function(or(_,_), [ 0,0,1,2, 0,0,2,0, 3,3,3,2, 0,0,0,0 ]), function(not(_), [0,2,2,2]) ]). interpretation(4, [ function(or(_,_), [ 0,0,1,3, 0,2,1,3, 3,1,0,3, 3,3,0,3 ]), function(not(_), [0,3,3,1]) ]). interpretation(4, [ function(or(_,_), [ 0,0,3,1, 0,0,3,0, 1,0,2,0, 2,0,2,0 ]), function(not(_), [0,2,2,0]) ]). % Models from idx.16 (1664 -> 1316). interpretation(4, [ function(or(_,_), [ 0,0,2,0, 0,0,0,0, 1,1,3,1, 1,0,3,0 ]), function(not(_), [0,2,0,2]) ]). interpretation(4, [ function(or(_,_), [ 0,0,2,0, 0,0,0,0, 1,1,3,1, 1,1,3,1 ]), function(not(_), [0,2,0,2]) ]). interpretation(4, [ function(or(_,_), [ 0,0,2,0, 0,0,2,0, 1,1,3,0, 1,0,3,1 ]), function(not(_), [0,2,0,2]) ]). interpretation(4, [ function(or(_,_), [ 0,0,2,0, 0,0,2,0, 1,1,3,1, 1,0,3,1 ]), function(not(_), [0,2,0,2]) ]). interpretation(4, [ function(or(_,_), [ 0,0,2,0, 0,0,2,0, 1,1,3,1, 1,1,3,1 ]), function(not(_), [0,2,0,2]) ]). interpretation(4, [ function(or(_,_), [ 0,0,2,1, 2,0,1,2, 2,1,0,2, 3,2,1,3 ]), function(not(_), [0,3,0,3]) ]). % Models from idx.17 (1280 -> 913). % Models from idx.18 (1568 -> 1105). % Models from idx.19 (448 -> 200). % Models from idx.20 (960 -> 688). interpretation(4, [ function(or(_,_), [ 0,0,2,2, 0,0,0,0, 1,3,3,0, 1,1,1,1 ]), function(not(_), [0,2,0,2]) ]). interpretation(4, [ function(or(_,_), [ 0,0,2,2, 0,0,0,0, 1,3,3,3, 1,1,1,1 ]), function(not(_), [0,2,0,2]) ]). interpretation(4, [ function(or(_,_), [ 0,0,2,3, 0,1,2,3, 2,2,2,3, 3,3,2,2 ]), function(not(_), [0,2,1,1]) ]). interpretation(4, [ function(or(_,_), [ 0,0,3,0, 0,0,0,0, 1,2,2,0, 2,0,1,0 ]), function(not(_), [0,2,2,0]) ]). interpretation(4, [ function(or(_,_), [ 0,0,3,0, 0,0,0,0, 1,2,2,0, 2,0,2,0 ]), function(not(_), [0,2,2,0]) ]). interpretation(4, [ function(or(_,_), [ 0,0,3,0, 0,0,0,0, 1,2,2,1, 2,1,2,1 ]), function(not(_), [0,2,2,0]) ]). interpretation(4, [ function(or(_,_), [ 0,0,3,2, 0,0,3,2, 1,0,2,3, 1,0,2,2 ]), function(not(_), [0,2,2,0]) ]). interpretation(4, [ function(or(_,_), [ 0,0,3,3, 0,0,3,0, 1,1,2,3, 1,1,2,1 ]), function(not(_), [0,2,2,0]) ]). % Models from idx.21 (352 -> 251). interpretation(4, [ function(or(_,_), [ 0,0,3,0, 0,0,3,0, 1,1,2,1, 1,1,2,1 ]), function(not(_), [0,2,2,0]) ]). % Models from idx.22 (1376 -> 613). interpretation(4, [ function(or(_,_), [ 0,0,1,1, 0,0,3,0, 3,3,2,1, 1,0,0,0 ]), function(not(_), [0,2,2,0]) ]). interpretation(4, [ function(or(_,_), [ 0,0,1,1, 0,0,3,0, 3,3,2,2, 1,0,0,0 ]), function(not(_), [0,2,2,0]) ]). interpretation(4, [ function(or(_,_), [ 0,0,1,1, 2,0,3,3, 0,0,1,1, 2,2,3,3 ]), function(not(_), [0,1,2,3]) ]). interpretation(4, [ function(or(_,_), [ 0,0,1,1, 2,2,3,3, 0,0,1,1, 2,2,3,3 ]), function(not(_), [0,2,1,3]) ]). interpretation(4, [ function(or(_,_), [ 0,0,1,3, 0,2,1,3, 1,1,0,0, 3,3,1,3 ]), function(not(_), [0,3,0,1]) ]). interpretation(4, [ function(or(_,_), [ 0,0,1,3, 0,2,1,3, 1,1,1,3, 3,3,0,3 ]), function(not(_), [0,3,0,1]) ]). interpretation(4, [ function(or(_,_), [ 0,0,3,0, 0,0,1,0, 0,1,3,0, 2,2,2,2 ]), function(not(_), [0,2,2,2]) ]). interpretation(4, [ function(or(_,_), [ 0,0,3,0, 1,0,1,0, 2,1,2,0, 2,1,2,0 ]), function(not(_), [0,2,2,3]) ]). interpretation(4, [ function(or(_,_), [ 0,0,3,0, 1,1,1,0, 2,1,2,0, 2,1,2,0 ]), function(not(_), [0,2,2,3]) ]). interpretation(4, [ function(or(_,_), [ 0,0,3,3, 0,2,1,3, 1,1,0,0, 3,3,3,3 ]), function(not(_), [0,3,3,1]) ]). interpretation(4, [ function(or(_,_), [ 0,1,2,3, 1,0,0,0, 2,0,0,0, 3,0,1,0 ]), function(not(_), [0,0,0,0]) ]). % Models from idx.23 (3136 -> 1144). % Models from idx.24 (2336 -> 816). interpretation(4, [ function(or(_,_), [ 0,0,1,1, 2,2,3,3, 0,0,0,1, 2,2,3,3 ]), function(not(_), [0,1,2,3]) ]). interpretation(4, [ function(or(_,_), [ 0,0,3,3, 1,1,2,2, 0,0,3,3, 1,1,2,2 ]), function(not(_), [0,2,3,1]) ]). % Models from idx.25 (2944 -> 1000). % Models from idx.26 (2720 -> 1104). interpretation(4, [ function(or(_,_), [ 0,0,1,1, 2,2,3,3, 0,0,1,1, 2,2,3,3 ]), function(not(_), [0,1,2,3]) ]). % Models from idx.27 (1504 -> 352). % Models from idx.28 (1760 -> 96). % Models from idx.29 (3424 -> 172). % Models from idx.30 (2176 -> 204). % Models from idx.31 (192 -> 152). % Models from idx.32 (288 -> 120). % Models from idx.33 (1184 -> 176). % Models from idx.34 (512 -> 16). % Models from idx.35 (96 -> 72). % Models from idx.36 (704 -> 480). % Models from idx.37 (288 -> 200). % Models from idx.38 (1632 -> 616). % Models from idx.39 (1568 -> 356). interpretation(4, [ function(or(_,_), [ 0,0,2,1, 0,0,0,0, 2,0,1,3, 0,2,2,1 ]), function(not(_), [0,2,3,2]) ]). % Models from idx.40 (512 -> 144). % This set of noncommutative structures was obtained by going through % the xxxxyzz=z single axiom candidates (prefiltered with bool1 and % bool 2) with sem (2 seconds each). % See /home/mccune/exp/ornot/catchup/README. % Models from xaa (500 -> 500). interpretation(4, [ function(or(_,_), [ 0,0,1,1, 1,0,0,0, 2,0,3,1, 1,0,0,0 ]), function(not(_), [0,2,0,2]) ]). % Models from xab (500 -> 500). % Models from xac (500 -> 500). % Models from xad (500 -> 500). interpretation(4, [ function(or(_,_), [ 0,0,3,3, 1,1,2,2, 3,3,0,0, 2,2,1,1 ]), function(not(_), [0,2,3,1]) ]). % Models from xae (500 -> 495). % Models from xaf (500 -> 499). interpretation(4, [ function(or(_,_), [ 0,1,2,3, 0,1,2,3, 2,3,0,1, 2,3,0,1 ]), function(not(_), [0,2,1,3]) ]). % Models from xag (500 -> 488). % Models from xah (500 -> 500). % Models from xai (500 -> 500). % Models from xaj (500 -> 500). % Models from xak (500 -> 500). % Models from xal (500 -> 500). % Models from xam (500 -> 499). % Models from xan (500 -> 499). % Models from xao (500 -> 500). % Models from xap (500 -> 500). % Models from xaq (500 -> 500). % Models from xar (500 -> 500). % Models from xas (500 -> 500). interpretation(4, [ function(or(_,_), [ 0,0,1,2, 0,2,1,3, 2,0,3,3, 3,0,0,3 ]), function(not(_), [0,1,0,2]) ]). interpretation(4, [ function(or(_,_), [ 0,0,1,2, 0,2,3,0, 2,2,3,0, 3,3,1,2 ]), function(not(_), [0,1,0,2]) ]). interpretation(4, [ function(or(_,_), [ 0,0,1,3, 0,0,1,0, 1,0,3,2, 3,0,1,3 ]), function(not(_), [0,2,2,0]) ]). interpretation(4, [ function(or(_,_), [ 0,0,2,3, 0,2,0,1, 3,0,3,0, 2,0,2,2 ]), function(not(_), [0,2,1,1]) ]). % Models from xat (500 -> 497). % Models from xau (500 -> 495). % Models from xav (500 -> 500). % Models from xaw (500 -> 500). interpretation(4, [ function(or(_,_), [ 0,0,1,2, 0,2,0,0, 3,1,2,1, 0,2,0,0 ]), function(not(_), [0,0,2,2]) ]). % Models from xax (500 -> 497). % Models from xay (500 -> 498). % Models from xaz (500 -> 498). % Models from xba (500 -> 500). % Models from xbb (500 -> 500). interpretation(4, [ function(or(_,_), [ 0,0,2,0, 0,0,2,0, 1,2,3,0, 1,2,3,0 ]), function(not(_), [0,2,0,2]) ]). interpretation(4, [ function(or(_,_), [ 0,0,3,0, 0,0,0,0, 1,2,2,1, 2,0,2,3 ]), function(not(_), [0,2,2,0]) ]). interpretation(4, [ function(or(_,_), [ 0,0,3,0, 0,0,3,0, 1,2,2,1, 1,2,2,1 ]), function(not(_), [0,2,2,0]) ]). % Models from xbc (500 -> 497). % Models from xbd (500 -> 500). % Models from xbe (500 -> 500). % Models from xbf (500 -> 500). % Models from xbg (500 -> 500). % Models from xbh (500 -> 500). % Models from xbi (500 -> 500). interpretation(4, [ function(or(_,_), [ 0,0,3,1, 0,0,3,3, 2,2,1,1, 2,2,3,1 ]), function(not(_), [0,2,1,3]) ]). % Models from xbj (500 -> 496). % Models from xbk (500 -> 500). interpretation(4, [ function(or(_,_), [ 0,0,2,1, 0,2,2,3, 2,2,2,2, 3,0,1,3 ]), function(not(_), [0,3,1,3]) ]). interpretation(4, [ function(or(_,_), [ 0,0,3,2, 0,2,1,2, 2,2,3,0, 3,3,2,2 ]), function(not(_), [0,3,1,0]) ]). interpretation(4, [ function(or(_,_), [ 0,0,3,2, 0,2,1,2, 2,2,3,0, 3,3,3,2 ]), function(not(_), [0,3,1,0]) ]). % Models from xbl (500 -> 494). interpretation(4, [ function(or(_,_), [ 0,0,3,1, 0,2,0,0, 2,0,3,0, 3,0,1,2 ]), function(not(_), [0,3,3,0]) ]). % Models from xbm (500 -> 488). % Models from xbn (500 -> 484). interpretation(4, [ function(or(_,_), [ 0,0,2,1, 0,0,0,0, 3,1,2,1, 0,0,0,1 ]), function(not(_), [0,2,2,3]) ]). % Models from xbo (500 -> 481). interpretation(4, [ function(or(_,_), [ 0,0,1,1, 2,1,0,3, 0,0,0,1, 2,2,3,3 ]), function(not(_), [0,0,3,3]) ]). % Models from xbp (500 -> 480). % Models from xbq (500 -> 498). interpretation(4, [ function(or(_,_), [ 0,0,3,1, 1,0,3,1, 2,2,3,1, 3,0,0,3 ]), function(not(_), [0,2,0,1]) ]). interpretation(4, [ function(or(_,_), [ 0,0,3,1, 1,0,3,1, 2,2,3,1, 3,3,0,3 ]), function(not(_), [0,2,0,1]) ]). interpretation(4, [ function(or(_,_), [ 0,0,3,1, 1,1,3,0, 0,2,3,1, 2,2,0,3 ]), function(not(_), [0,2,1,1]) ]). interpretation(4, [ function(or(_,_), [ 0,0,3,1, 1,1,3,0, 0,2,3,1, 2,2,2,3 ]), function(not(_), [0,2,1,1]) ]). % Models from xbr (500 -> 492). interpretation(4, [ function(or(_,_), [ 0,0,3,1, 2,0,1,3, 0,0,3,1, 2,0,3,3 ]), function(not(_), [0,1,2,3]) ]). % Models from xbs (343 -> 331). interpretation(4, [ function(or(_,_), [ 0,0,1,2, 0,2,1,3, 2,2,3,3, 3,3,0,3 ]), function(not(_), [0,1,0,2]) ]). % All of these are from one MACE job with the following input % % list(usable). % o(x,y) = o(y,x). % % o(n(o(z,n(z))),n(o(n(x),n(o(x,y))))) = x. % o(0,n(o(n(x),n(o(x,y))))) = x. % o(x,n(x)) = 1. % o(n(x),x) = 1. % n(0) = 1. % n(1) = 0. % o(x,1) = 1. % o(1,x) = 1. % o(2,2) = 3. % % This was from the search for a simple 2-basis with commutativity. % The first model proved useful for the single axiom search, % and the whole set proved a bit more useful than just the first. interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 4, 5, 7, 2, 6, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 1, 1, 2, 1, 4, 1, 3, 4, 4, 1, 1, 1, 5, 1, 1, 4, 5, 5, 1, 1, 7, 1, 1, 1, 5, 7, 1, 7, 2, 1, 2, 1, 1, 1, 2, 6, 6, 1, 1, 1, 1, 7, 6, 6 ]), function(not(_), [1, 0, 4, 5, 7, 6, 3, 2])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 6, 5, 7, 2, 4, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 1, 1, 2, 1, 6, 1, 3, 6, 1, 1, 6, 1, 5, 1, 1, 1, 5, 5, 1, 4, 7, 1, 1, 1, 5, 7, 1, 7, 2, 1, 2, 6, 1, 1, 2, 1, 4, 1, 1, 1, 4, 7, 1, 4 ]), function(not(_), [1, 0, 4, 5, 3, 6, 7, 2])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 4, 5, 6, 7, 2, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 1, 1, 1, 2, 4, 1, 3, 4, 4, 1, 1, 1, 5, 1, 1, 4, 5, 5, 1, 1, 6, 1, 1, 1, 5, 6, 6, 1, 7, 1, 1, 1, 1, 6, 7, 7, 2, 1, 2, 1, 1, 1, 7, 2 ]), function(not(_), [1, 0, 4, 5, 6, 7, 2, 3])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 7, 5, 6, 4, 2, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 1, 1, 1, 2, 7, 1, 3, 7, 1, 1, 1, 7, 5, 1, 1, 1, 5, 5, 4, 1, 6, 1, 1, 1, 5, 6, 6, 1, 4, 1, 1, 1, 4, 6, 4, 1, 2, 1, 2, 7, 1, 1, 1, 2 ]), function(not(_), [1, 0, 4, 5, 3, 7, 2, 6])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 4, 6, 2, 7, 5, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 1, 2, 1, 1, 4, 1, 3, 4, 4, 1, 1, 1, 6, 1, 1, 4, 6, 1, 6, 1, 2, 1, 2, 1, 1, 2, 1, 5, 7, 1, 1, 1, 6, 1, 7, 7, 5, 1, 1, 1, 1, 5, 7, 5 ]), function(not(_), [1, 0, 4, 6, 7, 3, 5, 2])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 5, 6, 2, 7, 4, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 1, 2, 1, 1, 5, 1, 3, 5, 1, 5, 1, 1, 6, 1, 1, 1, 6, 1, 6, 4, 2, 1, 2, 5, 1, 2, 1, 1, 7, 1, 1, 1, 6, 1, 7, 7, 4, 1, 1, 1, 4, 1, 7, 4 ]), function(not(_), [1, 0, 4, 6, 3, 7, 5, 2])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 4, 6, 7, 5, 2, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 1, 1, 1, 2, 4, 1, 3, 4, 4, 1, 1, 1, 6, 1, 1, 4, 6, 1, 6, 1, 7, 1, 1, 1, 1, 7, 5, 7, 5, 1, 1, 1, 6, 5, 5, 1, 2, 1, 2, 1, 1, 7, 1, 2 ]), function(not(_), [1, 0, 4, 6, 5, 2, 7, 3])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 7, 6, 4, 5, 2, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 1, 1, 1, 2, 7, 1, 3, 7, 1, 1, 1, 7, 6, 1, 1, 1, 6, 4, 6, 1, 4, 1, 1, 1, 4, 4, 5, 1, 5, 1, 1, 1, 6, 5, 5, 1, 2, 1, 2, 7, 1, 1, 1, 2 ]), function(not(_), [1, 0, 4, 6, 3, 2, 7, 5])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 4, 7, 2, 5, 6, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 1, 2, 1, 1, 4, 1, 3, 4, 4, 1, 1, 1, 7, 1, 1, 4, 7, 1, 1, 7, 2, 1, 2, 1, 1, 2, 5, 1, 5, 1, 1, 1, 1, 5, 5, 6, 6, 1, 1, 1, 7, 1, 6, 6 ]), function(not(_), [1, 0, 4, 7, 6, 3, 2, 5])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 5, 7, 2, 4, 6, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 1, 2, 1, 1, 5, 1, 3, 5, 1, 5, 1, 1, 7, 1, 1, 1, 7, 1, 4, 7, 2, 1, 2, 5, 1, 2, 1, 1, 4, 1, 1, 1, 4, 1, 4, 6, 6, 1, 1, 1, 7, 1, 6, 6 ]), function(not(_), [1, 0, 4, 7, 3, 6, 2, 5])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 4, 7, 6, 2, 5, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 1, 1, 2, 1, 4, 1, 3, 4, 4, 1, 1, 1, 7, 1, 1, 4, 7, 1, 1, 7, 6, 1, 1, 1, 1, 6, 6, 5, 2, 1, 2, 1, 1, 6, 2, 1, 5, 1, 1, 1, 7, 5, 1, 5 ]), function(not(_), [1, 0, 4, 7, 5, 2, 3, 6])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 6, 7, 4, 2, 5, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 1, 1, 2, 1, 6, 1, 3, 6, 1, 1, 6, 1, 7, 1, 1, 1, 7, 4, 1, 7, 4, 1, 1, 1, 4, 4, 1, 5, 2, 1, 2, 6, 1, 1, 2, 1, 5, 1, 1, 1, 7, 5, 1, 5 ]), function(not(_), [1, 0, 4, 7, 3, 2, 5, 6])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 7, 6, 4, 5, 2, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 1, 1, 1, 2, 7, 1, 3, 7, 1, 1, 1, 7, 6, 1, 1, 1, 6, 4, 6, 1, 4, 1, 1, 1, 4, 4, 5, 1, 5, 1, 1, 1, 6, 5, 5, 1, 2, 1, 2, 7, 1, 1, 1, 2 ]), function(not(_), [1, 0, 5, 4, 7, 3, 2, 6])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 5, 6, 4, 7, 2, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 1, 1, 1, 2, 5, 1, 3, 5, 1, 5, 1, 1, 6, 1, 1, 1, 6, 4, 6, 1, 4, 1, 1, 5, 4, 4, 1, 1, 7, 1, 1, 1, 6, 1, 7, 7, 2, 1, 2, 1, 1, 1, 7, 2 ]), function(not(_), [1, 0, 5, 4, 7, 6, 2, 3])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 6, 7, 4, 2, 5, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 1, 1, 2, 1, 6, 1, 3, 6, 1, 1, 6, 1, 7, 1, 1, 1, 7, 4, 1, 7, 4, 1, 1, 1, 4, 4, 1, 5, 2, 1, 2, 6, 1, 1, 2, 1, 5, 1, 1, 1, 7, 5, 1, 5 ]), function(not(_), [1, 0, 5, 4, 6, 3, 7, 2])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 5, 7, 4, 2, 6, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 1, 1, 2, 1, 5, 1, 3, 5, 1, 5, 1, 1, 7, 1, 1, 1, 7, 4, 1, 7, 4, 1, 1, 5, 4, 4, 1, 1, 2, 1, 2, 1, 1, 1, 2, 6, 6, 1, 1, 1, 7, 1, 6, 6 ]), function(not(_), [1, 0, 5, 4, 6, 7, 3, 2])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 5, 2, 6, 7, 4, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 2, 1, 1, 1, 5, 1, 3, 5, 1, 5, 1, 1, 2, 1, 2, 1, 2, 1, 1, 4, 6, 1, 1, 5, 1, 6, 6, 1, 7, 1, 1, 1, 1, 6, 7, 7, 4, 1, 1, 1, 4, 1, 7, 4 ]), function(not(_), [1, 0, 5, 6, 3, 7, 4, 2])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 4, 2, 6, 7, 5, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 2, 1, 1, 1, 4, 1, 3, 4, 4, 1, 1, 1, 2, 1, 2, 4, 2, 1, 1, 1, 6, 1, 1, 1, 1, 6, 6, 5, 7, 1, 1, 1, 1, 6, 7, 7, 5, 1, 1, 1, 1, 5, 7, 5 ]), function(not(_), [1, 0, 5, 6, 7, 3, 4, 2])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 5, 7, 6, 4, 2, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 1, 1, 1, 2, 5, 1, 3, 5, 1, 5, 1, 1, 7, 1, 1, 1, 7, 1, 4, 7, 6, 1, 1, 5, 1, 6, 6, 1, 4, 1, 1, 1, 4, 6, 4, 1, 2, 1, 2, 1, 7, 1, 1, 2 ]), function(not(_), [1, 0, 5, 6, 2, 4, 7, 3])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 7, 5, 6, 4, 2, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 1, 1, 1, 2, 7, 1, 3, 7, 1, 1, 1, 7, 5, 1, 1, 1, 5, 5, 4, 1, 6, 1, 1, 1, 5, 6, 6, 1, 4, 1, 1, 1, 4, 6, 4, 1, 2, 1, 2, 7, 1, 1, 1, 2 ]), function(not(_), [1, 0, 5, 6, 2, 3, 7, 4])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 5, 2, 7, 4, 6, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 2, 1, 1, 1, 5, 1, 3, 5, 1, 5, 1, 1, 2, 1, 2, 1, 2, 1, 4, 1, 7, 1, 1, 5, 1, 7, 1, 7, 4, 1, 1, 1, 4, 1, 4, 6, 6, 1, 1, 1, 1, 7, 6, 6 ]), function(not(_), [1, 0, 5, 7, 3, 6, 2, 4])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 4, 2, 7, 5, 6, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 2, 1, 1, 1, 4, 1, 3, 4, 4, 1, 1, 1, 2, 1, 2, 4, 2, 1, 1, 1, 7, 1, 1, 1, 1, 7, 5, 7, 5, 1, 1, 1, 1, 5, 5, 6, 6, 1, 1, 1, 1, 7, 6, 6 ]), function(not(_), [1, 0, 5, 7, 6, 3, 2, 4])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 5, 6, 7, 2, 4, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 1, 1, 2, 1, 5, 1, 3, 5, 1, 5, 1, 1, 6, 1, 1, 1, 6, 1, 6, 4, 7, 1, 1, 5, 1, 7, 1, 7, 2, 1, 2, 1, 6, 1, 2, 1, 4, 1, 1, 1, 4, 7, 1, 4 ]), function(not(_), [1, 0, 5, 7, 2, 4, 3, 6])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 6, 5, 7, 2, 4, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 1, 1, 2, 1, 6, 1, 3, 6, 1, 1, 6, 1, 5, 1, 1, 1, 5, 5, 1, 4, 7, 1, 1, 1, 5, 7, 1, 7, 2, 1, 2, 6, 1, 1, 2, 1, 4, 1, 1, 1, 4, 7, 1, 4 ]), function(not(_), [1, 0, 5, 7, 2, 3, 4, 6])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 7, 5, 6, 4, 2, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 1, 1, 1, 2, 7, 1, 3, 7, 1, 1, 1, 7, 5, 1, 1, 1, 5, 5, 4, 1, 6, 1, 1, 1, 5, 6, 6, 1, 4, 1, 1, 1, 4, 6, 4, 1, 2, 1, 2, 7, 1, 1, 1, 2 ]), function(not(_), [1, 0, 6, 4, 7, 2, 3, 5])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 6, 5, 7, 4, 2, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 1, 1, 1, 2, 6, 1, 3, 6, 1, 1, 6, 1, 5, 1, 1, 1, 5, 5, 4, 1, 7, 1, 1, 1, 5, 7, 1, 7, 4, 1, 1, 6, 4, 1, 4, 1, 2, 1, 2, 1, 1, 7, 1, 2 ]), function(not(_), [1, 0, 6, 4, 7, 2, 5, 3])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 6, 7, 2, 4, 5, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 1, 2, 1, 1, 6, 1, 3, 6, 1, 1, 6, 1, 7, 1, 1, 1, 7, 1, 4, 7, 2, 1, 2, 1, 1, 2, 1, 5, 4, 1, 1, 6, 4, 1, 4, 1, 5, 1, 1, 1, 7, 5, 1, 5 ]), function(not(_), [1, 0, 6, 4, 5, 3, 7, 2])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 5, 7, 2, 4, 6, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 1, 2, 1, 1, 5, 1, 3, 5, 1, 5, 1, 1, 7, 1, 1, 1, 7, 1, 4, 7, 2, 1, 2, 5, 1, 2, 1, 1, 4, 1, 1, 1, 4, 1, 4, 6, 6, 1, 1, 1, 7, 1, 6, 6 ]), function(not(_), [1, 0, 6, 4, 5, 7, 3, 2])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 7, 6, 4, 5, 2, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 1, 1, 1, 2, 7, 1, 3, 7, 1, 1, 1, 7, 6, 1, 1, 1, 6, 4, 6, 1, 4, 1, 1, 1, 4, 4, 5, 1, 5, 1, 1, 1, 6, 5, 5, 1, 2, 1, 2, 7, 1, 1, 1, 2 ]), function(not(_), [1, 0, 6, 5, 2, 7, 3, 4])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 6, 7, 4, 5, 2, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 1, 1, 1, 2, 6, 1, 3, 6, 1, 1, 6, 1, 7, 1, 1, 1, 7, 4, 1, 7, 4, 1, 1, 1, 4, 4, 5, 1, 5, 1, 1, 6, 1, 5, 5, 1, 2, 1, 2, 1, 7, 1, 1, 2 ]), function(not(_), [1, 0, 6, 5, 2, 7, 4, 3])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 6, 2, 7, 5, 4, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 2, 1, 1, 1, 6, 1, 3, 6, 1, 1, 6, 1, 2, 1, 2, 1, 2, 1, 1, 4, 7, 1, 1, 1, 1, 7, 5, 7, 5, 1, 1, 6, 1, 5, 5, 1, 4, 1, 1, 1, 4, 7, 1, 4 ]), function(not(_), [1, 0, 6, 5, 3, 4, 7, 2])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 4, 2, 7, 5, 6, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 2, 1, 1, 1, 4, 1, 3, 4, 4, 1, 1, 1, 2, 1, 2, 4, 2, 1, 1, 1, 7, 1, 1, 1, 1, 7, 5, 7, 5, 1, 1, 1, 1, 5, 5, 6, 6, 1, 1, 1, 1, 7, 6, 6 ]), function(not(_), [1, 0, 6, 5, 7, 4, 3, 2])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 6, 2, 4, 7, 5, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 2, 1, 1, 1, 6, 1, 3, 6, 1, 1, 6, 1, 2, 1, 2, 1, 2, 4, 1, 1, 4, 1, 1, 1, 4, 4, 1, 5, 7, 1, 1, 6, 1, 1, 7, 7, 5, 1, 1, 1, 1, 5, 7, 5 ]), function(not(_), [1, 0, 6, 7, 3, 2, 5, 4])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 4, 2, 6, 7, 5, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 2, 1, 1, 1, 4, 1, 3, 4, 4, 1, 1, 1, 2, 1, 2, 4, 2, 1, 1, 1, 6, 1, 1, 1, 1, 6, 6, 5, 7, 1, 1, 1, 1, 6, 7, 7, 5, 1, 1, 1, 1, 5, 7, 5 ]), function(not(_), [1, 0, 6, 7, 5, 2, 3, 4])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 6, 5, 2, 7, 4, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 1, 2, 1, 1, 6, 1, 3, 6, 1, 1, 6, 1, 5, 1, 1, 1, 5, 5, 1, 4, 2, 1, 2, 1, 5, 2, 1, 1, 7, 1, 1, 6, 1, 1, 7, 7, 4, 1, 1, 1, 4, 1, 7, 4 ]), function(not(_), [1, 0, 6, 7, 2, 3, 4, 5])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 5, 6, 2, 7, 4, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 1, 2, 1, 1, 5, 1, 3, 5, 1, 5, 1, 1, 6, 1, 1, 1, 6, 1, 6, 4, 2, 1, 2, 5, 1, 2, 1, 1, 7, 1, 1, 1, 6, 1, 7, 7, 4, 1, 1, 1, 4, 1, 7, 4 ]), function(not(_), [1, 0, 6, 7, 2, 4, 3, 5])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 7, 5, 6, 2, 4, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 1, 1, 2, 1, 7, 1, 3, 7, 1, 1, 1, 7, 5, 1, 1, 1, 5, 5, 1, 4, 6, 1, 1, 1, 5, 6, 6, 1, 2, 1, 2, 1, 1, 6, 2, 1, 4, 1, 1, 7, 4, 1, 1, 4 ]), function(not(_), [1, 0, 7, 4, 6, 2, 3, 5])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 6, 5, 7, 2, 4, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 1, 1, 2, 1, 6, 1, 3, 6, 1, 1, 6, 1, 5, 1, 1, 1, 5, 5, 1, 4, 7, 1, 1, 1, 5, 7, 1, 7, 2, 1, 2, 6, 1, 1, 2, 1, 4, 1, 1, 1, 4, 7, 1, 4 ]), function(not(_), [1, 0, 7, 4, 6, 2, 5, 3])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 7, 6, 2, 5, 4, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 1, 2, 1, 1, 7, 1, 3, 7, 1, 1, 1, 7, 6, 1, 1, 1, 6, 1, 6, 4, 2, 1, 2, 1, 1, 2, 5, 1, 5, 1, 1, 1, 6, 5, 5, 1, 4, 1, 1, 7, 4, 1, 1, 4 ]), function(not(_), [1, 0, 7, 4, 5, 3, 2, 6])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 5, 6, 2, 7, 4, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 1, 2, 1, 1, 5, 1, 3, 5, 1, 5, 1, 1, 6, 1, 1, 1, 6, 1, 6, 4, 2, 1, 2, 5, 1, 2, 1, 1, 7, 1, 1, 1, 6, 1, 7, 7, 4, 1, 1, 1, 4, 1, 7, 4 ]), function(not(_), [1, 0, 7, 4, 5, 6, 2, 3])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 7, 6, 4, 2, 5, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 1, 1, 2, 1, 7, 1, 3, 7, 1, 1, 1, 7, 6, 1, 1, 1, 6, 4, 6, 1, 4, 1, 1, 1, 4, 4, 1, 5, 2, 1, 2, 1, 6, 1, 2, 1, 5, 1, 1, 7, 1, 5, 1, 5 ]), function(not(_), [1, 0, 7, 5, 2, 6, 3, 4])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 6, 7, 4, 2, 5, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 1, 1, 2, 1, 6, 1, 3, 6, 1, 1, 6, 1, 7, 1, 1, 1, 7, 4, 1, 7, 4, 1, 1, 1, 4, 4, 1, 5, 2, 1, 2, 6, 1, 1, 2, 1, 5, 1, 1, 1, 7, 5, 1, 5 ]), function(not(_), [1, 0, 7, 5, 2, 6, 4, 3])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 7, 2, 6, 4, 5, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 2, 1, 1, 1, 7, 1, 3, 7, 1, 1, 1, 7, 2, 1, 2, 1, 2, 1, 4, 1, 6, 1, 1, 1, 1, 6, 6, 5, 4, 1, 1, 1, 4, 6, 4, 1, 5, 1, 1, 7, 1, 5, 1, 5 ]), function(not(_), [1, 0, 7, 5, 3, 4, 2, 6])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 4, 2, 6, 7, 5, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 2, 1, 1, 1, 4, 1, 3, 4, 4, 1, 1, 1, 2, 1, 2, 4, 2, 1, 1, 1, 6, 1, 1, 1, 1, 6, 6, 5, 7, 1, 1, 1, 1, 6, 7, 7, 5, 1, 1, 1, 1, 5, 7, 5 ]), function(not(_), [1, 0, 7, 5, 6, 4, 2, 3])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 7, 5, 2, 4, 6, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 1, 2, 1, 1, 7, 1, 3, 7, 1, 1, 1, 7, 5, 1, 1, 1, 5, 5, 4, 1, 2, 1, 2, 1, 5, 2, 1, 1, 4, 1, 1, 1, 4, 1, 4, 6, 6, 1, 1, 7, 1, 1, 6, 6 ]), function(not(_), [1, 0, 7, 6, 2, 3, 5, 4])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 5, 7, 2, 4, 6, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 1, 2, 1, 1, 5, 1, 3, 5, 1, 5, 1, 1, 7, 1, 1, 1, 7, 1, 4, 7, 2, 1, 2, 5, 1, 2, 1, 1, 4, 1, 1, 1, 4, 1, 4, 6, 6, 1, 1, 1, 7, 1, 6, 6 ]), function(not(_), [1, 0, 7, 6, 2, 4, 5, 3])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 7, 2, 4, 5, 6, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 2, 1, 1, 1, 7, 1, 3, 7, 1, 1, 1, 7, 2, 1, 2, 1, 2, 4, 1, 1, 4, 1, 1, 1, 4, 4, 5, 1, 5, 1, 1, 1, 1, 5, 5, 6, 6, 1, 1, 7, 1, 1, 6, 6 ]), function(not(_), [1, 0, 7, 6, 3, 2, 4, 5])]). interpretation( 8, [ function(or(_,_), [ 0, 1, 3, 4, 2, 7, 5, 6, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 3, 3, 2, 1, 1, 1, 4, 1, 3, 4, 4, 1, 1, 1, 2, 1, 2, 4, 2, 1, 1, 1, 7, 1, 1, 1, 1, 7, 5, 7, 5, 1, 1, 1, 1, 5, 5, 6, 6, 1, 1, 1, 1, 7, 6, 6 ]), function(not(_), [1, 0, 7, 6, 5, 2, 4, 3])]).