NKS code

CCheckAxiom[ax_,k_,maxret_:40,max_:-1]:=If[ax==={aaa},CCheckAxiomSpecial[k,maxret,max],Block[{axx,f,vars,loops},axx=CForm[(Apply[Or,ax]/.EqualUnequal)];vars=Union[Level[ax,{-1}]];loops=SequenceForm@@(StringForm["for (`1`=0; `1`<k; `1`++) ",#]&/@vars);Splice["axiomchecker.mc","axiomchecker.c",FormatTypeTextForm];Run["cc -o axiomchecker -O axiomchecker.c"];{Reverse/@Drop[#,-1],Last[#]}&[ReadList["!axiomchecker "<>ToString[k]<>" "<>ToString[maxret]<>" "<>ToString[max],Expression]]]]
TAx[axioms_,k_]:=Module[{c,v},c=Apply[Function,{v=Union[Level[axioms,{-1}]],Apply[And,axioms]}];Select[Range[0,k^(k^2)-1],With[{u=IntegerDigits[#,k,k^2]},Block[{f},f[x_,y_]:=u[[-1-kx-y]];Array[c,Table[k,{Length[v]}],0,And]]]&]]