arr=Import["/home/dennis/P/Rubik/TT","Table"] {{0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1}, {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0}, {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0,0}, {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,1,1}, {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0,0,1}, {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0,1,0}, {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,1,0,0}, {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,1,1,1}, {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,1}, ...2097135... , {1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,0,0,0,0}, {1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,0,0,1,1}, {1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,0,1,0,0}, {1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,0,1,1,1}, {1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,0,0,0}, {1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,0,1,1}, {1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,0,0}, {1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1}} TT=(Most[#]->Last[#])&/@arr {{0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0}->1, {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1}->0, {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0}->0, {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,1}->1, {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0,0}->1, {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0,1}->0, {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,1,0}->0, {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,1,1}->1, {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0}->1, ...2097135... , {1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,0,0,0}->0, {1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,0,0,1}->1, {1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,0,1,0}->0, {1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,0,1,1}->1, {1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,0,0}->0, {1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,0,1}->1, {1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,0}->0, {1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1}->1} BooleanConvert[BooleanFunction[TT,{s3,s2,s1,s0, i15,i14,i13,i12,i11,i10,i9,i8,i7,i6,i5,i4,i3, i2, i1, i0,x}],"CNF"] (!i0||s0||s1||s2||s3||x)&&(i0||s0||s1||s2||s3||!x)&&(!i1||!s0||s1||s2||s3||x)&&(i1||!s0||s1||s2||s3||!x)&&(!i10||s0||!s1||s2||!s3||x)&& (i10||s0||!s1||s2||!s3||!x)&&(!i11||!s0||!s1||s2||!s3||x)&&(i11||!s0||!s1||s2||!s3||!x)&&(!i12||s0||s1||!s2||!s3||x)&&(i12||s0||s1||!s2||!s3||!x)&& (!i13||!s0||s1||!s2||!s3||x)&&(i13||!s0||s1||!s2||!s3||!x)&&(!i14||s0||!s1||!s2||!s3||x)&&(i14||s0||!s1||!s2||!s3||!x)&& (!i15||!s0||!s1||!s2||!s3||x)&&(i15||!s0||!s1||!s2||!s3||!x)&&(!i2||s0||!s1||s2||s3||x)&&(i2||s0||!s1||s2||s3||!x)&&(!i3||!s0||!s1||s2||s3||x)&& (i3||!s0||!s1||s2||s3||!x)&&(!i4||s0||s1||!s2||s3||x)&&(i4||s0||s1||!s2||s3||!x)&&(!i5||!s0||s1||!s2||s3||x)&&(i5||!s0||s1||!s2||s3||!x)&& (!i6||s0||!s1||!s2||s3||x)&&(i6||s0||!s1||!s2||s3||!x)&&(!i7||!s0||!s1||!s2||s3||x)&&(i7||!s0||!s1||!s2||s3||!x)&&(!i8||s0||s1||s2||!s3||x)&& (i8||s0||s1||s2||!s3||!x)&&(!i9||!s0||s1||s2||!s3||x)&&(i9||!s0||s1||s2||!s3||!x)