Satisfiability [emulating Turing machines]

Given variables [t, s], [t, x, a], [t, n] representing whether at step t a non-deterministic Turing machine is in state s, the tape square at position x has color a, and the head is at position n, the following CNF expression represents the assertion that a Turing machine with stot states and ktot possible colors follows the specified rules and halts after at most t steps:

NDTMToCNF[rules_, {s_, a_, n_}, t_] := {Table[Apply[Or, Table[[i, j], {j, stot}]], {i, t - 1}], Table[![i, j] || ![i, k], {i, 0, t - 1}, {j, stot}, {k, j + 1, stot}], Table[Apply[Or, Table[[i, j], {j, n + i, Max[0, n - i], -2}]], {i, 0, t}], Table[![i, j] || ![i, k], {i, 0, t}, {j, n + i, Max[0, n - i], -2}, {k, j + 2, n + i}], Table[Apply[Or, Table[[i, j, k], {k, 0, ktot - 1}]], {i, 0, t - 1}, {j, Max[1, n - i], n + i}], Table[![i, j, k] || ![i, j, m], {i, 0, t - 1}, {j, Max[1, n - i], n + i}, {k, 0, ktot - 1}, {m, k + 1, ktot - 1}], [0, s], Cases[MapIndexed[[Abs[n - First[#2]], First[#2], #1]&, a], [x_, _, _] /; x < t], Table[[Abs[n - i], i, 0], {i, Length[a] + 1, n + t - 1}], Table[![i, j, k] || If[EvenQ[n + i - j], [i, j], False] || [i + 1, j, k], {i, 0, t - 2}, {j, Max[1, n - i], n + i}, {k, 0, ktot - 1}], Table[Map[Function[z, Outer[![i, j] || ![i, z〚1, 1〛] || ![i, j, z〚1, 2〛] || ## &, Apply[Sequence, Map[If[i < t - 1, {[i + 1, #〚1〛],[i + 1, j - #〚3〛], [i + 1, j, #〚2〛]}, {[i + 1, j - #〚3〛]}]&, z〚2〛]]]], rules], {i, 0, t - 1}, {j, n + i, Max[1, n - i], -2}], Apply[Or, Table[[i, 0], {i, n, t, 2}]]} /. List  And