eval qma_rec "?msd_4 An (QMA[4*n]=QMA[n] & QMA[4*n+1]!=QMA[n] & QMA[4*n+2]=QMA[2*n] & QMA[4*n+3]!=QMA[2*n])";
eval qma_balance "?msd_4 An ((QMA[2*n]=0 <=> QMA[2*n+1]=1) & (QMA[2*n]=1 <=> QMA[2*n+1]=0))";
eval m1a_rec01 "?msd_4 An (M1A[4*n]=M1A[n] & M1A[4*n+1]!=M1A[n])";
eval m1a_rec23 "?msd_4 An (((M1A[n]=0 => M1A[4*n+2]=M1A[2*n+1]) & (M1A[n]=1 => M1A[4*n+2]=M1A[2*n])) & M1A[4*n+3]!=M1A[4*n+2])";
eval m1a_balance "?msd_4 An ((M1A[2*n]=0 <=> M1A[2*n+1]=1) & (M1A[2*n]=1 <=> M1A[2*n+1]=0))";
eval m2a_rec01 "?msd_4 An (((M2A[n]=0 => M2A[4*n]=M2A[2*n]) & (M2A[n]=1 => M2A[4*n]=M2A[2*n+1])) & M2A[4*n+1]!=M2A[4*n])";
eval m2a_rec23 "?msd_4 An (((M2A[n]=0 => M2A[4*n+2]=M2A[2*n+1]) & (M2A[n]=1 => M2A[4*n+2]=M2A[2*n])) & M2A[4*n+3]!=M2A[4*n+2])";
eval m2a_balance "?msd_4 An ((M2A[2*n]=0 <=> M2A[2*n+1]=1) & (M2A[2*n]=1 <=> M2A[2*n+1]=0))";
