eval tribup "?msd_trib (p>=1) & En Ai (i >= n) => TR[i]=TR[i+p]":

eval trib4 "?msd_trib (n > 0) & Ei At (t<3*n) => TR[i+t] = TR[i+n+t]":
# doesn't work, runs out of space

eval trib4a "?msd_trib (n>0) & Ei Aj ((j >= i)&(j<i+3*n)) => TR[j] = TR[j+n]":
# an alternative that works

eval tribsq "?msd_trib (n>0) & Ei Aj ((i<=j)&(j<i+n)) => TR[j] = TR[j+n]":

eval tribsqp "?msd_trib (n>0) & Aj ((i<=j)&(j<i+n)) => TR[j] = TR[j+n]":

eval tribcube "?msd_trib (n>0) & Ei Aj ((i<=j)&(j<i+2*n)) => TR[j] = TR[j+n]":

eval tribfact "?msd_trib Ak (((k>0)&(k<=i)) => (Eu ((u>=j)&(u<n+j)&(TR[u]!=TR[u+k]))))":

eval tribsquare "?msd_trib (j>=1) & (i+2*j <= n) & Au ((u>=i)&(u<i+j)) => TR[u] = TR[u+j]":

eval tribcubepos "?msd_trib (n>0) & Aj ((i<=j)&(j<i+2*n)) => TR[j] = TR[j+n]":

eval tribevenpal "?msd_trib Ei ((i>=n) & Aj (j<n) => TR[i+j] = TR[i-j-1])":

eval triboddpal "?msd_trib Ei ((i>=n) & Aj ((1<=j)&(j<=n)) => TR[i+j] = TR[i-j])":
# dies on memory error

eval tribprefpal "?msd_trib Ai (i<n) => TR[i] = TR[n-1-i]":

eval tribquasi "?msd_trib Ai (Ej (i<n+j)&(j<=i)& (At (t<n) => TR[t]=TR[j+t]))":

eval tribborder "?msd_trib Ei Atp ((n<=2*tp)&(tp<n)) => (Eu 
	(i<=u)&(u+tp<i+n)&(TR[u]!=TR[u+tp]))":

eval triblyndon "?msd_trib Ei (Aj ((j>=1)&(j<n)) => Et (t+j<n)& (Aup 
	((i<=up)&(up<i+t)) => TR[up]=TR[up+j]) & (TR[i+t] < TR[i+j+t]))":

eval tribmaxper "?msd_trib (n>p)&(p>=1)&(Ei Aj ((j>=i)&(j+p<i+n)) => (TR[j]=TR[j+p])) & (Aip (Ejp (jp>=ip)&(jp+p<=ip+n)&(TR[jp]!=TR[jp+p])))":

eval tribprefpower "?msd_trib Ed (0<d)&(d<n)&(Aj (j+d<n) => (TR[j]=TR[j+d]))&(Ak (k<d) => (TR[n-d+k]=TR[k]))":

eval tribmirror "?msd_trib Ai Ej (j>=n) & (At ((t < n) => (TR[i + t] = TR[j-t])))":
# dies on memory error like before