(* rulefit 1RB0LF_0RC0RB_1LC1LD_1RE0RD_---0RA_1LA0LF: no validated rules (qsim edge C:R: 4 fitted rule(s) failed validation; record R:B: 4 fitted rule(s) failed validation; record R:C: 4 fitted rule(s) failed validation; record L:F: 4 fitted rule(s) failed validation) *)

(* low-level rules: sligocki prover (block size 4, 2000 loops), normalised to plain tapes, re-verified by direct simulation: 2/2 OK
   [0] 0^inf 01^3 10^2 01^(2a+11) 10^3 <F 01^(2b+4) 010^2 1 10^2 1 110^2 1 0 1^3 10^2 1^6 0^inf  -->  0^inf 01^3 10^2 01^(2a+9) 10^3 <F 01^(2b+10) 010^2 1 10^2 1 110^2 1 0 1^3 10^2 1^6 0^inf   steps 40a+344   verified 10/10
   [1] 0^inf 01^3 10^2 0 10^2 0^2 1 01^(2a+4) 10^(2b+11) 1^2 01^(2c+5) 10^2 01^(2d+7) <A 10^2 01^(2e+4) 0 01^2 1^2 0^inf  -->  0^inf 01^3 10^2 0 10^2 0^2 1 01^(2a+8) 10^(2b+7) 1^2 01^(2c+9) 10^2 01^(2d+5) <A 10^2 01^(2e+10) 0 01^2 1^2 0^inf   steps 80a+80b+40c+40d+1360   verified 10/10  (decrement >= 2: needs a mod split)
*)