PART 1: principal reloids on [n]:  S(S(F)) == S(F) and S(F)oS(F) == S(F)
  n=0: relations=     1, violations=0
  n=1: relations=     2, violations=0
  n=2: relations=    16, violations=0
  n=3: relations=   512, violations=0
  n=4: relations= 65536, violations=0
PART 2: window check of the counterexample, N=40
  (a) closed form of (F_m)^m on the window: OK for m=1..43
  (b) (0,c_n) not in K for n=1..40: OK
  (c) (0,c_n) in F_j o P^n for all 1<=j<=n<=40: OK (820 pairs (j,n))
  (d) K_tau o K_tau not<= K for all maps tau:{1..M}->{1..M}, M=1..6: OK (50069 maps)
  (e) S(F_j) <= (id u F_j) o (id u U_n P^n) on the window for j=1..40: OK
ALL CHECKS PASSED in 12.8s
