(* rulefit 1RB1LE_0RC1RC_0RD0RB_1RE0RF_1LA0LE_---1RB: no validated rules (time cap during validation; time cap during validation; time cap during validation; record R:B: 4 fitted rule(s) failed validation) *)

(* low-level rules: sligocki prover (block size 2, 2000 loops), normalised to plain tapes, re-verified by direct simulation: 5/5 OK
   [0] 0^inf 1^(2a+2) 0^2 1 0 01^(b+1) 0^2 1 0 1^(2c+2) 0^2 1^2 0^(2d+2) 1^2 0 1 0^(2e+2) 1^2 01^(f+1) 1^(2g+2) 0^2 F> 1^(2h+7) 0 1^(2i+4) 0^inf  -->  0^inf 1^(2a+2) 0^2 1 0 01^(b+1) 0^2 1 0 1^(2c+2) 0^2 1^2 0^(2d+2) 1^2 0 1 0^(2e+2) 1^2 01^(f+1) 1^(2g+4) 0^2 F> 1^(2h+5) 0 1^(2i+10) 0^inf   steps 4h+8i+54   verified 10/10
   [1] 0^inf 1^2 0^2 1^2 0^(2a+2) 1 0 1 1001^3 0 01^(b+1) 0^2 1 0^3 1^2 01^(c+1) 1^2 0^2 1^2 01^(d+1) 0011^2 01^(e+1) 0^2 1^(2f+2) 0^2 F> 1^(2g+7) 0 1^(2h+4) 0^inf  -->  0^inf 1^2 0^2 1^2 0^(2a+2) 1 0 1 1001^3 0 01^(b+1) 0^2 1 0^3 1^2 01^(c+1) 1^2 0^2 1^2 01^(d+1) 0011^2 01^(e+1) 0^2 1^(2f+4) 0^2 F> 1^(2g+5) 0 1^(2h+10) 0^inf   steps 4g+8h+54   verified 10/10
   [2] 0^inf 1^2 0^2 1^2 0^(2a+2) 1 0 1 1001^3 0 01^(b+1) 0^2 1 0^3 1^2 01^(c+1) 1^2 0^2 1^2 01^(d+1) 0^2 1^(2e+2) 0^2 1 0^3 1^2 01^(f+1) 0011^2 01^(g+1) 0^2 1^(2h+2) 0^2 F> 1^(2i+7) 0 1^(2j+4) 0^2 1^(2k+4) 0^inf  -->  0^inf 1^2 0^2 1^2 0^(2a+2) 1 0 1 1001^3 0 01^(b+1) 0^2 1 0^3 1^2 01^(c+1) 1^2 0^2 1^2 01^(d+1) 0^2 1^(2e+2) 0^2 1 0^3 1^2 01^(f+1) 0011^2 01^(g+1) 0^2 1^(2h+4) 0^2 F> 1^(2i+5) 0 1^(2j+6) 0^2 1^(2k+2) 0^inf   steps 4i+8j+50   verified 10/10
   [3] 0^inf 1^2 0^2 1^2 0^(2a+2) 1 0 1 1001^3 0 01^(b+1) 0^2 1 0^3 1^2 01^(c+1) 1^2 0^2 1^2 01^(d+1) 0^2 1^(2e+2) 0^2 1 0 1^(2f+2) 0^2 1^2 0^(2g+2) 1^2 0 1 0011^2 01^(h+1) 0 0110^2 1 0011^2 01^(i+1) 0011^2 01^(j+1) 0^2 1^(2k+2) 0^2 F> 1^(2m+7) 0 1^(2n+4) 0^inf  -->  0^inf 1^2 0^2 1^2 0^(2a+2) 1 0 1 1001^3 0 01^(b+1) 0^2 1 0^3 1^2 01^(c+1) 1^2 0^2 1^2 01^(d+1) 0^2 1^(2e+2) 0^2 1 0 1^(2f+2) 0^2 1^2 0^(2g+2) 1^2 0 1 0011^2 01^(h+1) 0 0110^2 1 0011^2 01^(i+1) 0011^2 01^(j+1) 0^2 1^(2k+4) 0^2 F> 1^(2m+5) 0 1^(2n+10) 0^inf   steps 4m+8n+54   verified 10/10
   [4] 0^inf 1^2 0^2 1^2 0^(2a+2) 1 0 1 1001^3 0 01^(b+1) 0^2 1 0^3 1^2 01^(c+1) 1^2 0^2 1^2 01^(d+1) 0^2 1^(2e+2) 0^2 1 0 1^(2f+2) 0^2 1^2 0^(2g+2) 1^2 0 1 0011^2 01^(h+1) 0 0110^2 1 0011^2 01^(i+1) 0^2 1^(2j+2) 0^2 1^2 01^(k+1) 0^(2m+2) 1^2 01^(n+1) 0011^2 01^(p+1) 0^2 1^(2q+2) 0^2 F> 1^(2r+7) 0 1^(2s+4) 0^(2t+9) 1^2 0^2 1^(2u+3) 0^inf  -->  0^inf 1^2 0^2 1^2 0^(2a+2) 1 0 1 1001^3 0 01^(b+1) 0^2 1 0^3 1^2 01^(c+1) 1^2 0^2 1^2 01^(d+1) 0^2 1^(2e+2) 0^2 1 0 1^(2f+2) 0^2 1^2 0^(2g+2) 1^2 0 1 0011^2 01^(h+1) 0 0110^2 1 0011^2 01^(i+1) 0^2 1^(2j+2) 0^2 1^2 01^(k+1) 0^(2m+2) 1^2 01^(n+1) 0011^2 01^(p+1) 0^2 1^(2q+4) 0^2 F> 1^(2r+5) 0 1^(2s+10) 0^(2t+3) 1^2 0^2 1^(2u+3) 0^inf   steps 4r+8s+54   verified 10/10  (decrement >= 2: needs a mod split)
*)