def tribsync0 "?msd_trib Ea Eb (s=a+b) & ((TRL[n]=@0)=>b=0) & ((TRL[n]=@1)=>b=1) & $rst(n,a)": def tribsync1 "?msd_trib Ea Eb Ec (s=b+c) & ((TRL[a]=@0)=>c=0) & ((TRL[a]=@1)=>c=1) & $rst(n,a) & $rst(a,b)": def tribsync2 "?msd_trib Ea Eb Ec Ed (s=c+d) & ((TRL[b]=@0)=>d=0) & ((TRL[b]=@1)=>d=1) & $rst(n,a) & $rst(a,b) & $rst(b,c)": def tribfac0 "?msd_trib Aq Ar ($tribsync0(i+n,q) & $tribsync0(i,r)) => (q=r+s)": def tribfac1 "?msd_trib Aq Ar ($tribsync1(i+n,q) & $tribsync1(i,r)) => (q=r+s)": def tribfac2 "?msd_trib Aq Ar ($tribsync2(i+n,q) & $tribsync2(i,r)) => (q=r+s)": def posrange0 "?msd_trib E i,n,s,t $tribfac0(i,n,s) & $tribfac0(0,n,t) & u+t=s": def negrange0 "?msd_trib E i,n,s,t $tribfac0(i,n,s) & $tribfac0(0,n,t) & u+s=t": def posrange1 "?msd_trib E i,n,s,t $tribfac1(i,n,s) & $tribfac1(0,n,t) & u+t=s": def negrange1 "?msd_trib E i,n,s,t $tribfac1(i,n,s) & $tribfac1(0,n,t) & u+s=t": def posrange2 "?msd_trib E i,n,s,t $tribfac2(i,n,s) & $tribfac2(0,n,t) & u+t=s": def negrange2 "?msd_trib E i,n,s,t $tribfac2(i,n,s) & $tribfac2(0,n,t) & u+s=t": def validtriples "?msd_trib Ei,n,a,b,c,d,e,f $tribfac0(i,n,a) & $tribfac0(0,n,b) & s+b=a+1 & $tribfac1(i,n,c) & $tribfac1(0,n,d) & t+d=c+1 & $tribfac2(i,n,e) & $tribfac2(0,n,f) & u+f=e+1": def t000 "?msd_trib Ea,b,c,d,e,f $tribfac0(i,n,a) & $tribfac0(0,n,b) & a=b & $tribfac1(i,n,c) & $tribfac1(0,n,d) & c=d & $tribfac2(i,n,e) & $tribfac2(0,n,f) & e=f": def t10m1 "?msd_trib Ea,b,c,d,e,f $tribfac0(i,n,a) & $tribfac0(0,n,b) & a=b+1 & $tribfac1(i,n,c) & $tribfac1(0,n,d) & c=d & $tribfac2(i,n,e) & $tribfac2(0,n,f) & e+1=f": def t1m10 "?msd_trib Ea,b,c,d,e,f $tribfac0(i,n,a) & $tribfac0(0,n,b) & a=b+1 & $tribfac1(i,n,c) & $tribfac1(0,n,d) & c+1=d & $tribfac2(i,n,e) & $tribfac2(0,n,f) & e=f": def t01m1 "?msd_trib Ea,b,c,d,e,f $tribfac0(i,n,a) & $tribfac0(0,n,b) & a=b & $tribfac1(i,n,c) & $tribfac1(0,n,d) & c=d+1 & $tribfac2(i,n,e) & $tribfac2(0,n,f) & e+1=f": def tm12m1 "?msd_trib Ea,b,c,d,e,f $tribfac0(i,n,a) & $tribfac0(0,n,b) & a+1=b & $tribfac1(i,n,c) & $tribfac1(0,n,d) & c=d+2 & $tribfac2(i,n,e) & $tribfac2(0,n,f) & e+1=f": def tm110 "?msd_trib Ea,b,c,d,e,f $tribfac0(i,n,a) & $tribfac0(0,n,b) & a+1=b & $tribfac1(i,n,c) & $tribfac1(0,n,d) & c=d+1 & $tribfac2(i,n,e) & $tribfac2(0,n,f) & e=f": def t0m11 "?msd_trib Ea,b,c,d,e,f $tribfac0(i,n,a) & $tribfac0(0,n,b) & a=b & $tribfac1(i,n,c) & $tribfac1(0,n,d) & c+1=d & $tribfac2(i,n,e) & $tribfac2(0,n,f) & e=f+1": def tm101 "?msd_trib Ea,b,c,d,e,f $tribfac0(i,n,a) & $tribfac0(0,n,b) & a+1=b & $tribfac1(i,n,c) & $tribfac1(0,n,d) & c=d & $tribfac2(i,n,e) & $tribfac2(0,n,f) & e=f+1": def tm1m12 "?msd_trib Ea,b,c,d,e,f $tribfac0(i,n,a) & $tribfac0(0,n,b) & a+1=b & $tribfac1(i,n,c) & $tribfac1(0,n,d) & c+1=d & $tribfac2(i,n,e) & $tribfac2(0,n,f) & e=f+2": def subset "?msd_trib ((Ei $t000(i,m)) <=> (Ej $t000(j,n))) & ((Ei $t10m1(i,m)) <=> (Ej $t10m1(j,n))) & ((Ei $t1m10(i,m)) <=> (Ej $t1m10(j,n))) & ((Ei $t01m1(i,m)) <=> (Ej $t01m1(j,n))) & ((Ei $tm12m1(i,m)) <=> (Ej $tm12m1(j,n))) & ((Ei $tm110(i,m)) <=> (Ej $tm110(j,n))) & ((Ei $t0m11(i,m)) <=> (Ej $t0m11(j,n))) & ((Ei $tm101(i,m)) <=> (Ej $tm101(j,n))) & ((Ei $tm1m12(i,m)) <=> (Ej $tm1m12(j,n)))": def last "?msd_trib ~($subset(n,0) | $subset(n,1) | $subset(n,2) | $subset(n,3) | $subset(n,4) | $subset(n,5) | $subset(n,6) | $subset(n,9) | $subset(n,11) | $subset(n,17) | $subset(n,30) | $subset(n,31) | $subset(n,55) | $subset(n,57) | $subset(n,101) | $subset(n,105) | $subset(n,185) | $subset(n,340) | $subset(n,341) | $subset(n,342) | $subset(n,355) | $subset(n,629) | $subset(n,653) | $subset(n,1157) | $subset(n,1201))": def missing "?msd_trib $last(n) & Am (m ~$last(m)": eval test4 "?msd_trib An Em (m>n) & TRAC[m]=@4": def a0 "?msd_trib $subset(m,0)": def a1 "?msd_trib $subset(m,1)": def a2 "?msd_trib $subset(m,2)": def a3 "?msd_trib $subset(m,3)": def a4 "?msd_trib $subset(m,4)": def a5 "?msd_trib $subset(m,5)": def a6 "?msd_trib $subset(m,6)": def a9 "?msd_trib $subset(m,9)": def a11 "?msd_trib $subset(m,11)": def a17 "?msd_trib $subset(m,17)": def a30 "?msd_trib $subset(m,30)": def a31 "?msd_trib $subset(m,31)": def a55 "?msd_trib $subset(m,55)": def a57 "?msd_trib $subset(m,57)": def a101 "?msd_trib $subset(m,101)": def a105 "?msd_trib $subset(m,105)": def a185 "?msd_trib $subset(m,185)": def a340 "?msd_trib $subset(m,340)": def a341 "?msd_trib $subset(m,341)": def a342 "?msd_trib $subset(m,342)": def a355 "?msd_trib $subset(m,355)": def a629 "?msd_trib $subset(m,629)": def a653 "?msd_trib $subset(m,653)": def a1157 "?msd_trib $subset(m,1157)": def a1201 "?msd_trib $subset(m,1201)": def a3914 "?msd_trib $subset(m,3914)": def b3 "?msd_trib $a1(n) | $a2(n) | $a4(n)": def b4 "?msd_trib $a3(n) | $a5(n) | $a6(n) | $a9(n) | $a11(n) | $a17(n)": def b5 "?msd_trib $a30(n) | $a31(n) | $a55(n) | $a57(n) | $a101(n) | $a105(n) | $a185(n) | $a340(n) | $a341(n)": def b6 "?msd_trib $a342(n) | $a355(n) | $a629(n) | $a653(n) | $a1157(n) | $a1201(n)": def b7 "?msd_trib $a3914(n)": def testa0 "?msd_trib An Em (m>n) & TRAS[m]=@0": def testa1 "?msd_trib An Em (m>n) & TRAS[m]=@1": def testa2 "?msd_trib An Em (m>n) & TRAS[m]=@2": def testa3 "?msd_trib An Em (m>n) & TRAS[m]=@3": def testa4 "?msd_trib An Em (m>n) & TRAS[m]=@4": def testa5 "?msd_trib An Em (m>n) & TRAS[m]=@5": def testa6 "?msd_trib An Em (m>n) & TRAS[m]=@6": def testa9 "?msd_trib An Em (m>n) & TRAS[m]=@9": def testa11 "?msd_trib An Em (m>n) & TRAS[m]=@11": def testa17 "?msd_trib An Em (m>n) & TRAS[m]=@17": def testa30 "?msd_trib An Em (m>n) & TRAS[m]=@30": def testa31 "?msd_trib An Em (m>n) & TRAS[m]=@31": def testa55 "?msd_trib An Em (m>n) & TRAS[m]=@55": def testa57 "?msd_trib An Em (m>n) & TRAS[m]=@57": def testa101 "?msd_trib An Em (m>n) & TRAS[m]=@101": def testa105 "?msd_trib An Em (m>n) & TRAS[m]=@105": def testa185 "?msd_trib An Em (m>n) & TRAS[m]=@185": def testa340 "?msd_trib An Em (m>n) & TRAS[m]=@340": def testa341 "?msd_trib An Em (m>n) & TRAS[m]=@341": def testa342 "?msd_trib An Em (m>n) & TRAS[m]=@342": def testa355 "?msd_trib An Em (m>n) & TRAS[m]=@355": def testa629 "?msd_trib An Em (m>n) & TRAS[m]=@629": def testa653 "?msd_trib An Em (m>n) & TRAS[m]=@653": def testa1157 "?msd_trib An Em (m>n) & TRAS[m]=@1157": def testa1201 "?msd_trib An Em (m>n) & TRAS[m]=@1201": def testa3914 "?msd_trib An Em (m>n) & TRAS[m]=@3914":