== Part 1: Lemma 3.1 (ping-pong in SL_2(F[x]))
  Lemma 3.1 over F_2   reduced words of length 1..24: 48 words; degree-invariant failures 0; words with an L-letter lying in U12: 0; words with a U-letter lying in U21: 0  (0.0s)
  Lemma 3.1 over F_3   reduced words of length 1..16: 262140 words; degree-invariant failures 0; words with an L-letter lying in U12: 0; words with a U-letter lying in U21: 0  (0.9s)
  Lemma 3.1 over F_4   reduced words of length 1..9: 59046 words; degree-invariant failures 0; words with an L-letter lying in U12: 0; words with a U-letter lying in U21: 0  (0.1s)
  Lemma 3.1 over F_5   reduced words of length 1..9: 699048 words; degree-invariant failures 0; words with an L-letter lying in U12: 0; words with a U-letter lying in U21: 0  (1.7s)
== Part 2: Proposition 5.1 (no closedness assumed)
  Prop 5.1: F=F_4  n=3: normalised irreducible elementary nets = 2; not completable = 0  (0.0s)
  Prop 5.1: F=F_8  n=3: normalised irreducible elementary nets = 2; not completable = 0  (0.0s)
  Prop 5.1: F=F_9  n=3: normalised irreducible elementary nets = 2; not completable = 0  (0.0s)
  Prop 5.1: F=F_25 n=3: normalised irreducible elementary nets = 2; not completable = 0  (0.0s)
  Prop 5.1: F=F_27 n=3: normalised irreducible elementary nets = 2; not completable = 0  (0.0s)
  Prop 5.1: F=F_49 n=3: normalised irreducible elementary nets = 2; not completable = 0  (0.0s)
  Prop 5.1: F=F_4  n=4: normalised irreducible elementary nets = 2; not completable = 0  (0.0s)
  Prop 5.1: F=F_8  n=4: normalised irreducible elementary nets = 2; not completable = 0  (0.0s)
  Prop 5.1: F=F_9  n=4: normalised irreducible elementary nets = 2; not completable = 0  (0.0s)
