[1] symbolic identity, difference = 0
[1] numeric identity and 'x-y<=2d, change>=0 => y>x' checked on 59280 cases
[1] moves (3k+1,3k+2): (d,J) -> (d+1,J+k), ring invariant 3(d-k): checked
[2] k=0 d=2 (4 shifts max): J=0:T J=1:T J=2:- J=3:- J=4:- J=5:- J=6:- J=7:-
[2] k=0 d=3 (4 shifts max): J=0:T J=1:T J=2:- J=3:- J=4:- J=5:- J=6:- J=7:-
[2] k=0 d=4 (4 shifts max): J=0:T J=1:T J=2:- J=3:- J=4:- J=5:- J=6:- J=7:-
[2] k=0 d=5 (4 shifts max): J=0:T J=1:T J=2:- J=3:- J=4:- J=5:- J=6:- J=7:-
[2] k=1 d=2 (25 shifts max): J=0:T J=1:T J=2:T J=3:- J=4:- J=5:- J=6:- J=7:-
[2] k=1 d=3 (25 shifts max): J=0:T J=1:T J=2:T J=3:- J=4:- J=5:- J=6:- J=7:-
[2] k=1 d=4 (25 shifts max): J=0:T J=1:T J=2:T J=3:- J=4:- J=5:- J=6:- J=7:-
[2] k=1 d=5 (25 shifts max): J=0:T J=1:T J=2:T J=3:- J=4:- J=5:- J=6:- J=7:-
[2] k=2 d=3 (64 shifts max): J=0:T J=1:T J=2:T J=3:T J=4:- J=5:- J=6:- J=7:-
[2] k=2 d=4 (64 shifts max): J=0:T J=1:T J=2:T J=3:T J=4:- J=5:- J=6:- J=7:-
[2] rings tileable for some translation iff J <= k+1: 80 of 80 cases agree
[3] bounds attained for all 780 pairs 2<=a<=b<=2a-2, a<=40; not attained for the 78 pairs with b in {2a-1,2a}
FAILURES: 0  (6.8s)
