eval thm1test "(~Ei, n (n>=3) & At (t<n) => T1[i+t]=T1[i+n+t]) & (~Ej T1[j]=@1 & T1[j+1]=@1 & T1[j+2]=@1 & T1[j+3]=@1)":

# no squares of order >= 3, and only squares of smaller order
# are allowed to be 00, 11, 0000, 0101, 1010, but not 1111.

def ochem "Ei Ej (n=50*i+j) & (j < 50) &  
((VTM[i]=@0 & (j=3|j=4|j=7|j=9|j=10|j=14|j=15|j=16|j=19|j=21|j=22|j=25|j=26|j=27|j=31|j=33|j=34|j=35|j=38|j=40|j=41|j=45|j=47|j=48|j=49)) |
(VTM[i]=@1 & (j=3|j=4|j=7|j=9|j=10|j=14|j=16|j=17|j=18|j=21|j=23|j=24|j=27|j=28|j=29|j=33|j=35|j=36|j=40|j=41|j=42|j=45|j=47|j=48|j=49)) |
(VTM[i]=@2 & (j=3|j=4|j=7|j=9|j=10|j=14|j=16|j=17|j=18|j=21|j=23|j=24|j=28|j=29|j=30|j=33|j=35|j=36|j=37|j=41|j=43|j=44|j=47|j=48|j=49)))":

def thm2test "(~Ei, n (n>=3) & At (t<n) => ($ochem(i+t) <=> $ochem(i+n+t))) & 
(~Ej ($ochem(j) <=> $ochem(j+1)) & ($ochem(j) <=> $ochem(j+2)) & ($ochem(j) <=> $ochem(j+3)))
& (~Ej ($ochem(j) & (~$ochem(j+1)) & $ochem(j+2) & (~$ochem(j+3))))":
# 95 gigs of main memory needed!

def thm4test "(~Ei, n (n>=3) & At (t<n) => HN[i+t]=HN[i+t+n]) & 
(~Ej HN[j]=HN[j+1] & HN[j]=HN[j+2] & HN[j]=HN[j+3]) &
(~Ej HN[j]=@1 & HN[j+1]=@0 & HN[j+2]=@1 & HN[j+3]=@0)":
# 24 gigs of main memory needed!

def thm5test "(~Ei, n (n>=3) & At (t<n) => GAB[i+t]=GAB[i+t+n]) &
(~Ej GAB[j]=GAB[j+1] & GAB[j]=GAB[j+2] & GAB[j]=GAB[j+3]) &
(~Ej GAB[j]=@0 & GAB[j+1]=@1 & GAB[j+2]=@0 & GAB[j+3]=@1)":

eval thm6test "(~Ei En (n>=3) & At (t<n) => Q[i+t] = Q[i+t+n]) & 
(~Ei (Q[i]=Q[i+1])&(Q[i]=Q[i+2])&(Q[i]=Q[i+3])) &
(~Ei (Q[i]=@0)&(Q[i+1]=@1)&(Q[i+2]=@0)&(Q[i+3]=@1))":