bbeaver(4,[t(a,0,1,r,b),t(a,1,1,l,b),t(b,0,1,l,a),t(b,1,0,l,c),t(c,0,1,r,h),t(c,1,1,l,d),t(d,0,1,r,d),t(d,1,0,r,a)],13,107).
bbeaver(3,[t(a,0,1,r,b),t(a,1,1,r,h),t(b,0,0,r,c),t(b,1,1,r,b),t(c,0,1,l,c),t(c,1,1,l,a)],6,14).
bbeaver(2,[t(a,0,1,r,b),t(a,1,1,l,b),t(b,0,1,l,a),t(b,1,1,r,h)], 4, 6).
bbeaver(1,[t(a,0,1,r,h),t(a,1,1,r,a)], 1, a). 

lbeaver(4,[t(a,0,1,r,b),t(a,1,0,r,c),t(b,0,1,l,a),t(b,1,1,r,a),t(c,0,1,r,h),t(c,1,1,r,d),t(d,0,1,l,d),t(d,1,0,l,b)],13,96).
lbeaver(2,[t(a,0,1,r,b),t(a,1,1,l,c),t(b,0,1,r,c),t(b,1,1,r,h),t(c,0,1,l,a),t(c,1,0,l,b)],6,11).

platypus(1, [t(a,0,1,r,h),t(a,1,1,r,a)], 1, 1). 
platypus(2, [t(a,0,1,r,b),t(a,1,1,r,a),t(b,0,1,r,h),t(b,1,1,r,b)], 2, 2).
platypus(3, [t(a,0,1,r,b),t(a,1,1,l,a),t(b,0,1,l,a),t(b,1,1,r,h)], 2, 5).
platypus(4, [t(a,0,1,r,b),t(a,1,1,l,b),t(b,0,1,l,a),t(b,1,1,r,h)], 2, 6).
platypus(5, [t(a,0,1,r,b),t(a,1,1,l,c),t(b,0,1,l,a),t(b,1,1,r,h),t(c,0,1,l,b)],3,7).
platypus(4, [t(a,0,1,r,b),t(b,0,1,l,c),t(b,1,1,r,h),t(c,0,1,l,a),t(c,1,1,l,b)],3,7).
platypus(6, [t(a,0,1,r,b),t(a,1,1,l,c),t(b,0,1,r,c),t(b,1,1,r,h),t(c,0,1,l,a),t(c,1,0,l,b)], 3, 11).
platypus(7, [t(a,0,1,r,b),t(a,1,0,r,b),t(b,0,1,l,c),t(b,1,1,r,h),t(c,0,1,l,d),t(c,1,1,r,a),t(d,0,1,l,a),t(d,1,1,l,b)], 4, 12).
platypus(7, [t(a,0,1,r,b),t(a,1,1,r,h),t(b,0,1,l,d),t(b,1,1,r,c),t(c,0,1,r,d),t(c,1,1,r,c),t(d,0,1,r,a),t(d,1,1,l,a)], 4, 12).
platypus(7, [t(a,0,1,r,b),t(a,1,1,r,h),t(b,0,1,l,d),t(b,1,1,r,c),t(c,0,1,r,a),t(c,1,1,r,d),t(d,0,1,r,c),t(d,1,1,l,a)], 4, 12).
platypus(7, [t(a,0,1,r,b),t(a,1,1,r,h),t(b,0,1,l,c),t(b,1,1,r,d),t(c,0,1,r,d),t(c,1,1,l,a),t(d,0,1,r,a),t(d,1,1,r,c)], 4, 12).
platypus(7, [t(a,0,1,r,b),t(a,1,1,r,h),t(b,0,1,l,c),t(b,1,1,r,d),t(c,0,1,r,a),t(c,1,1,l,a),t(d,0,1,r,c),t(d,1,1,r,d)], 4, 12).
platypus(7, [t(a,0,1,r,b),t(a,1,1,r,d),t(b,0,1,l,b),t(b,1,1,l,c),t(c,0,1,r,a),t(c,1,1,r,h),t(d,0,1,r,c),t(d,1,1,r,d)], 4, 12).
platypus(7, [t(a,0,1,r,b),t(a,1,1,r,c),t(b,0,1,l,b),t(b,1,1,l,c),t(c,0,1,r,d),t(c,1,1,r,h),t(d,0,1,r,a),t(d,1,1,r,a)], 4, 12).
platypus(7, [t(a,0,1,r,b),t(a,1,1,l,d),t(b,0,1,r,c),t(b,1,1,r,h),t(c,0,1,l,a),t(c,1,1,l,c),t(d,0,1,l,b),t(d,1,1,l,d)], 4, 12).
platypus(7, [t(a,0,1,r,b),t(a,1,1,l,d),t(b,0,1,r,c),t(b,1,1,r,h),t(c,0,1,l,a),t(c,1,1,l,a),t(d,0,1,l,c),t(d,1,1,l,b)], 4, 12).
platypus(7, [t(a,0,1,r,b),t(a,1,1,l,d),t(b,0,1,r,c),t(b,1,1,l,b),t(c,0,1,l,a),t(c,1,1,r,h),t(d,0,1,l,c),t(d,1,1,l,d)], 4, 12).
platypus(7, [t(a,0,1,r,b),t(a,1,1,l,d),t(b,0,1,r,c),t(b,1,1,l,a),t(c,0,1,l,a),t(c,1,1,r,h),t(d,0,1,l,b),t(d,1,1,l,c)], 4, 12).
platypus(7, [t(a,0,1,r,b),t(a,1,1,l,d),t(b,0,1,l,c),t(b,1,1,r,h),t(c,0,1,l,a),t(c,1,1,r,d),t(d,0,1,l,b),t(d,1,0,r,b)], 4, 12).
platypus(7, [t(a,0,1,r,b),t(a,1,1,l,d),t(b,0,1,l,c),t(b,1,1,r,h),t(c,0,1,l,a),t(c,1,1,r,c),t(d,0,1,l,b),t(d,1,1,l,d)], 4, 12).
platypus(7, [t(a,0,1,r,b),t(a,1,1,l,c),t(b,0,1,r,d),t(b,1,1,r,h),t(c,0,1,l,d),t(c,1,1,l,b),t(d,0,1,l,a),t(d,1,1,l,a)], 4, 12).
platypus(7, [t(a,0,1,r,b),t(a,1,1,l,c),t(b,0,1,r,d),t(b,1,1,r,h),t(c,0,1,l,b),t(c,1,1,l,c),t(d,0,1,l,a),t(d,1,1,l,d)], 4, 12).
platypus(7, [t(a,0,1,r,b),t(a,1,1,l,c),t(b,0,1,r,c),t(b,1,1,r,h),t(c,0,1,l,d),t(c,1,1,l,d),t(d,0,1,l,b),t(d,1,1,l,a)], 4, 12).
platypus(7, [t(a,0,1,r,b),t(a,1,1,l,c),t(b,0,1,r,c),t(b,1,1,r,h),t(c,0,1,l,a),t(c,1,1,l,d),t(d,0,1,l,b),t(d,1,1,l,c)], 4, 12).
platypus(7, [t(a,0,1,r,b),t(a,1,1,l,c),t(b,0,1,r,c),t(b,1,1,l,b),t(c,0,1,l,d),t(c,1,1,r,h),t(d,0,1,l,a),t(d,1,1,l,a)], 4, 12).
platypus(7, [t(a,0,1,r,b),t(a,1,1,l,c),t(b,0,1,r,c),t(b,1,1,l,a),t(c,0,1,l,d),t(c,1,1,r,h),t(d,0,1,l,b),t(d,1,1,l,b)], 4, 12).
platypus(7, [t(a,0,1,r,b),t(a,1,1,l,c),t(b,0,1,l,d),t(b,1,1,r,h),t(c,0,1,l,b),t(c,1,0,r,b),t(d,0,1,l,a),t(d,1,1,r,c)], 4, 12).
platypus(7, [t(a,0,1,r,b),t(a,1,1,l,c),t(b,0,1,l,d),t(b,1,1,r,h),t(c,0,1,l,b),t(c,1,1,l,c),t(d,0,1,l,a),t(d,1,1,r,d)], 4, 12).
platypus(7, [t(a,0,1,r,b),t(a,1,1,l,c),t(b,0,1,l,a),t(b,1,1,r,c),t(c,0,1,r,d),t(c,1,1,r,h),t(d,0,1,r,a),t(d,1,1,r,b)], 4, 12).
platypus(7, [t(a,0,1,r,b),t(a,1,1,l,b),t(b,0,1,r,c),t(b,1,1,r,h),t(c,0,1,l,d),t(c,1,1,l,c),t(d,0,1,l,a),t(d,1,1,l,a)], 4, 12).
platypus(7, [t(a,0,1,r,b),t(a,1,1,l,b),t(b,0,1,r,c),t(b,1,1,l,d),t(c,0,1,l,a),t(c,1,1,r,h),t(d,0,1,l,c),t(d,1,1,l,b)], 4, 12).
platypus(7, [t(a,0,1,r,b),t(a,1,1,l,b),t(b,0,1,l,c),t(b,1,1,r,h),t(c,0,1,l,d),t(c,1,1,r,d),t(d,0,1,l,a),t(d,1,0,r,c)], 4, 12).
platypus(7, [t(a,0,1,r,b),t(a,1,1,l,b),t(b,0,1,l,c),t(b,1,1,r,h),t(c,0,1,l,d),t(c,1,1,r,c),t(d,0,1,l,a),t(d,1,1,l,a)], 4, 12).
platypus(8, [t(a,0,1,r,b),t(a,1,1,r,d),t(b,0,1,l,c),t(b,1,1,r,h),t(c,0,1,r,a),t(c,1,1,l,b),t(d,0,1,r,c),t(d,1,1,r,d)], 4, 14).
platypus(8, [t(a,0,1,r,b),t(a,1,1,r,d),t(b,0,1,l,c),t(b,1,1,r,h),t(c,0,1,r,a),t(c,1,1,l,b),t(d,0,1,r,c),t(d,1,1,r,a)], 4, 14).
platypus(8, [t(a,0,1,r,b),t(a,1,1,r,c),t(b,0,1,l,d),t(b,1,1,r,h),t(c,0,1,r,d),t(c,1,1,r,c),t(d,0,1,r,a),t(d,1,1,l,b)], 4, 14).
platypus(8, [t(a,0,1,r,b),t(a,1,1,r,c),t(b,0,1,l,d),t(b,1,1,r,h),t(c,0,1,r,d),t(c,1,1,r,a),t(d,0,1,r,a),t(d,1,1,l,b)], 4, 14).
platypus(9, [t(a,0,1,r,b),t(a,1,1,r,c),t(b,0,1,l,d),t(b,1,0,l,b),t(c,0,1,r,d),t(c,1,1,r,h),t(d,0,1,r,a),t(d,1,1,l,a)], 4, 19).
platypus(10, [t(a,0,1,r,b),t(a,1,0,r,c),t(b,0,1,l,d),t(b,1,1,r,a),t(c,0,1,l,a),t(c,1,1,r,h),t(d,0,0,l,c),t(d,1,1,l,d)], 4, 30).
platypus(11, [t(a,0,1,r,b),t(a,1,0,l,d),t(b,0,1,l,a),t(b,1,1,r,c),t(c,0,1,r,a),t(c,1,1,r,h),t(d,0,0,l,b),t(d,1,1,r,b)], 4, 40).
platypus(12, [t(a,0,1,r,b),t(a,1,1,l,b),t(b,0,1,l,d),t(b,1,1,r,c),t(c,0,1,r,h),t(c,1,0,r,d),t(d,0,1,r,a),t(d,1,1,l,a)], 4, 53).
platypus(13, [t(a,0,1,r,b),t(a,1,0,r,c),t(b,0,1,l,a),t(b,1,1,r,a),t(c,0,1,r,h),t(c,1,1,r,d),t(d,0,1,l,d),t(d,1,0,l,b)], 4, 96).

platypus(20,[t(a,0,1,r,b),t(b,0,0,l,a),t(a,1,1,r,c),t(c,0,1,r,d),t(d,0,1,l,a),t(c,1,1,l,e),t(e,1,1,l,d),t(d,1,0,l,d),t(b,1,0,r,c),t(e,0,1,r,h)],5,84).
platypus(29,[t(a,0,1,r,b),t(b,0,0,l,a),t(a,1,1,r,c),t(c,0,1,r,d),t(d,0,1,l,e),t(e,1,1,l,d),t(d,1,0,l,d),t(e,0,1,r,b),t(b,1,0,r,c),t(c,1,1,r,h)],5,69).
platypus(18,[t(a,0,1,r,b),t(b,0,0,l,a),t(a,1,1,l,c),t(c,0,1,l,d),t(d,0,1,l,e),t(e,0,1,l,a),t(b,1,1,r,e),t(e,1,0,r,e),t(c,1,0,l,b),t(d,1,1,r,h)],5,63).
platypus(17,[t(a,0,1,r,b),t(b,0,0,l,a),t(a,1,1,l,c),t(c,0,1,l,d),t(d,0,1,l,a),t(b,1,1,r,e),t(e,1,0,r,e),t(e,0,1,l,d),t(c,1,0,l,a),t(d,1,1,r,h)],5,57).
platypus(16,[t(a,0,1,r,b),t(b,0,0,l,a),t(a,1,1,r,c),t(c,0,1,l,b),t(b,1,1,l,d),t(d,0,1,l,e),t(e,0,1,r,a),t(c,1,0,r,c),t(d,1,0,l,c),t(e,1,1,r,h)],5,57).
platypus(15,[t(a,0,1,r,b),t(b,0,0,l,a),t(a,1,1,l,c),t(c,0,1,r,a),t(c,1,1,r,d),t(d,1,1,l,e),t(e,1,0,l,e),t(e,0,1,l,d),t(d,0,1,r,c),t(b,1,1,r,h)],5,45).
platypus(14,[t(a,0,1,r,b),t(b,0,0,l,a),t(a,1,1,l,c),t(c,0,1,l,d),t(d,0,1,r,e),t(e,1,1,r,d),t(d,1,0,l,d),t(e,0,1,r,b),t(c,1,0,l,c),t(b,1,1,r,h)],5,41).
platypus(13,[t(a,0,1,r,b),t(b,0,0,l,a),t(a,1,1,r,c),t(c,0,0,r,d),t(d,0,1,l,e),t(e,0,1,l,d),t(d,1,1,l,a),t(b,1,1,r,c),t(c,1,0,r,c),t(e,1,1,r,h)],5,32).
platypus(12,[t(a,0,1,r,b),t(b,0,0,l,a),t(a,1,1,l,c),t(c,0,1,l,d),t(d,0,1,r,e),t(e,1,1,r,d),t(d,1,1,r,c),t(c,1,0,l,c),t(e,0,1,r,a),t(b,1,1,r,h)],5,30).
platypus(11,[t(a,0,1,r,b),t(b,0,0,l,a),t(a,1,1,r,c),t(c,0,1,l,d),t(d,1,1,l,e),t(e,0,1,l,c),t(d,0,1,l,a),t(b,1,1,r,e),t(e,1,0,r,e),t(c,1,1,r,h)],5,26).
platypus(10,[t(a,0,1,r,b),t(b,0,0,l,a),t(a,1,1,r,c),t(c,0,1,r,d),t(d,0,1,l,b),t(b,1,1,l,e),t(e,1,1,r,c),t(c,1,0,r,c),t(e,0,1,l,d),t(d,1,1,r,h)],5,23). 
platypus( 9,[t(a,0,1,r,b),t(b,0,0,l,a),t(a,1,1,l,c),t(c,0,1,r,a),t(c,1,1,l,d),t(d,0,1,l,a),t(b,1,1,r,e),t(e,1,0,l,e),t(e,0,1,r,c),t(d,1,1,r,h)],5,22).
platypus( 8,[t(a,0,1,r,b),t(b,0,0,l,a),t(a,1,1,r,c),t(c,0,1,l,d),t(d,1,1,l,e),t(e,0,0,l,d),t(d,0,1,l,a),t(b,1,1,r,c),t(e,1,1,l,c),t(c,1,1,r,h)],5,17).

monster(4,[t(a,0,1,r,b),t(a,1,1,l,b),t(b,0,1,l,a),t(b,1,0,l,c),t(c,0,1,r,h),t(c,1,1,l,d),t(d,0,1,r,d),t(d,1,0,r,a)],13,107).
monster(4,[t(a,0,1,r,b),t(a,1,0,r,c),t(b,0,1,l,a),t(b,1,1,r,a),t(c,0,1,r,h),t(c,1,1,r,d),t(d,0,1,l,d),t(d,1,0,l,b)],13,96).
monster(4,[t(a,0,1,r,b),t(a,1,0,r,c),t(b,0,1,l,d),t(b,1,0,l,a),t(c,0,1,r,h),t(c,1,0,r,d),t(d,0,1,r,a),t(d,1,1,l,b)],12,78).
monster(4,[t(a,0,1,r,b),t(a,1,0,r,d),t(b,0,1,l,c),t(b,1,0,l,a),t(c,0,1,r,a),t(c,1,1,l,b),t(d,0,1,r,h),t(d,1,0,r,c)],12,78).
monster(4,[t(a,0,1,r,b),t(a,1,0,l,a),t(b,0,1,r,c),t(b,1,1,l,b),t(c,0,1,l,b),t(c,1,1,r,d),t(d,0,1,r,h),t(d,1,0,r,a)],12,63).
monster(4,[t(a,0,1,r,b),t(a,1,1,l,b),t(b,0,1,l,d),t(b,1,1,r,c),t(c,0,1,r,h),t(c,1,0,r,d),t(d,0,1,r,a),t(d,1,1,l,a)],12,53).
monster(4,[t(a,0,1,r,b),t(a,1,1,l,b),t(b,0,1,l,c),t(b,1,1,r,d),t(c,0,1,r,a),t(c,1,1,l,a),t(d,0,1,r,h),t(d,1,0,r,c)],12,53).
monster(4,[t(a,0,1,r,b),t(a,1,1,l,c),t(b,0,0,l,d),t(b,1,0,r,d),t(c,0,1,r,h),t(c,1,0,l,a),t(d,0,1,l,d),t(d,1,1,l,a)],11,84).
monster(4,[t(a,0,1,r,b),t(a,1,1,l,d),t(b,0,0,l,c),t(b,1,0,r,c),t(c,0,1,l,c),t(c,1,1,l,a),t(d,0,1,r,h),t(d,1,0,l,a)],11,84).
monster(4,[t(a,0,1,r,b),t(a,1,1,l,c),t(b,0,1,r,d),t(b,1,1,r,h),t(c,0,1,r,d),t(c,1,0,l,c),t(d,0,1,l,a),t(d,1,0,r,a)],11,59).
monster(4,[t(a,0,1,r,b),t(a,1,0,r,c),t(b,0,1,l,c),t(b,1,1,r,h),t(c,0,1,r,a),t(c,1,1,l,d),t(d,0,1,r,a),t(d,1,1,l,b)],11,46).
monster(4,[t(a,0,1,r,b),t(a,1,0,l,d),t(b,0,1,l,a),t(b,1,1,r,c),t(c,0,1,r,a),t(c,1,1,r,h),t(d,0,0,l,b),t(d,1,1,r,b)],11,40).
monster(4,[t(a,0,1,r,b),t(a,1,0,l,c),t(b,0,1,l,a),t(b,1,1,r,d),t(c,0,0,l,b),t(c,1,1,r,b),t(d,0,1,r,a),t(d,1,1,r,h)],11,40).
monster(4,[t(a,0,1,r,b),t(a,1,1,r,d),t(b,0,1,l,d),t(b,1,0,l,c),t(c,0,1,r,d),t(c,1,1,r,h),t(d,0,0,r,a),t(d,1,1,l,b)],10,63).
monster(4,[t(a,0,1,r,b),t(a,1,1,r,c),t(b,0,1,l,c),t(b,1,0,l,d),t(c,0,0,r,a),t(c,1,1,l,b),t(d,0,1,r,c),t(d,1,1,r,h)],10,63).
monster(4,[t(a,0,1,r,b),t(a,1,1,l,d),t(b,0,1,l,c),t(b,1,0,r,c),t(c,0,1,r,h),t(c,1,1,r,a),t(d,0,1,l,c),t(d,1,1,l,a)],10,51).
monster(4,[t(a,0,1,r,b),t(a,1,1,l,c),t(b,0,1,l,d),t(b,1,0,r,d),t(c,0,1,l,d),t(c,1,1,l,a),t(d,0,1,r,h),t(d,1,1,r,a)],10,51).
monster(4,[t(a,0,1,r,b),t(a,1,1,r,h),t(b,0,0,r,d),t(b,1,0,r,c),t(c,0,0,r,b),t(c,1,1,l,a),t(d,0,1,l,d),t(d,1,1,l,c)],10,47).
monster(4,[t(a,0,1,r,b),t(a,1,1,l,c),t(b,0,1,l,c),t(b,1,0,r,d),t(c,0,1,l,d),t(c,1,1,l,a),t(d,0,1,r,h),t(d,1,1,r,a)],10,45).
monster(4,[t(a,0,1,r,b),t(a,1,0,l,d),t(b,0,1,l,a),t(b,1,1,r,c),t(c,0,1,r,h),t(c,1,1,r,d),t(d,0,1,l,b),t(d,1,1,r,b)],10,40).
monster(4,[t(a,0,1,r,b),t(a,1,1,l,d),t(b,0,0,r,c),t(b,1,1,r,b),t(c,0,1,r,d),t(c,1,1,r,h),t(d,0,1,l,a),t(d,1,0,l,d)],10,40).
monster(4,[t(a,0,1,r,b),t(a,1,0,l,c),t(b,0,1,l,a),t(b,1,1,r,d),t(c,0,1,l,b),t(c,1,1,r,b),t(d,0,1,r,h),t(d,1,1,r,c)],10,40).
monster(4,[t(a,0,1,r,b),t(a,1,1,l,c),t(b,0,0,r,d),t(b,1,1,r,b),t(c,0,1,l,a),t(c,1,0,l,c),t(d,0,1,r,c),t(d,1,1,r,h)],10,40).
monster(4,[t(a,0,1,r,b),t(a,1,0,r,c),t(b,0,1,l,d),t(b,1,1,r,a),t(c,0,1,l,a),t(c,1,1,r,h),t(d,0,0,l,c),t(d,1,1,l,d)],10,30).
monster(4,[t(a,0,1,r,b),t(a,1,0,l,b),t(b,0,1,l,c),t(b,1,1,l,a),t(c,0,1,r,d),t(c,1,1,l,a),t(d,0,1,r,h),t(d,1,1,r,c)],10,30).
monster(4,[t(a,0,1,r,b),t(a,1,0,r,d),t(b,0,1,l,c),t(b,1,1,r,a),t(c,0,0,l,d),t(c,1,1,l,c),t(d,0,1,l,a),t(d,1,1,r,h)],10,30).

monster(5,[t(a,0,1,r,b),t(a,1,1,l,c),t(b,0,1,r,c),t(b,1,1,r,b),t(c,0,1,r,d),t(c,1,0,l,e),t(d,0,1,l,a),t(d,1,1,l,d),t(e,0,1,r,h),t(e,1,0,l,a)],4098,47176870).
monster(5,[t(a,0,1,r,b),t(a,1,1,r,a),t(b,0,1,l,c),t(b,1,1,l,b),t(c,0,1,r,a),t(c,1,1,l,d),t(d,0,1,r,a),t(d,1,1,l,e),t(e,0,1,r,h),t(e,1,0,l,c)],4098,11798826).
monster(5,[t(a,0,1,r,b),t(a,1,0,l,d),t(b,0,1,l,c),t(b,1,1,r,d),t(c,0,1,l,a),t(c,1,1,l,c),t(d,0,1,r,h),t(d,1,1,r,e),t(e,0,1,r,a),t(e,1,0,r,b)],4097,23554764).
monster(5,[t(a,0,1,r,b),t(a,1,1,r,a),t(b,0,1,l,c),t(b,1,1,r,d),t(c,0,1,l,a),t(c,1,1,l,c),t(d,0,1,r,h),t(d,1,0,r,e),t(e,0,1,l,c),t(e,1,1,r,b)],4097,11797896).
monster(5,[t(a,0,1,r,b),t(a,1,1,r,a),t(b,0,1,l,c),t(b,1,0,r,d),t(c,0,1,l,a),t(c,1,1,l,c),t(d,0,1,r,h),t(d,1,1,r,e),t(e,0,0,l,e),t(e,1,1,r,b)],4096,11804910).
monster(5,[t(a,0,1,r,b),t(a,1,1,r,a),t(b,0,1,l,c),t(b,1,0,r,d),t(c,0,1,l,a),t(c,1,1,l,c),t(d,0,1,r,h),t(d,1,1,r,e),t(e,0,1,l,c),t(e,1,1,r,b)],4096,11804896).
monster(5,[t(a,0,1,r,b),t(a,1,1,l,c),t(b,0,0,l,a),t(b,1,0,l,d),t(c,0,1,l,a),t(c,1,1,r,h),t(d,0,1,l,b),t(d,1,1,r,e),t(e,0,0,r,d),t(e,1,0,r,b)],1915,2133492).
monster(5,[t(a,0,1,r,b),t(a,1,1,r,d),t(b,0,1,l,c),t(b,1,0,l,e),t(c,0,0,r,a),t(c,1,0,l,b),t(d,0,1,r,e),t(d,1,1,r,h),t(e,0,1,l,c),t(e,1,1,r,c)],1471,2358064).
monster(5,[t(a,0,1,r,b),t(a,1,0,l,c),t(b,0,1,r,c),t(b,1,1,r,d),t(c,0,1,l,a),t(c,1,0,r,b),t(d,0,0,r,e),t(d,1,1,r,h),t(e,0,1,l,c),t(e,1,1,r,a)], 501, 134467).

monster(6,[t(a,0,1,r,b),t(a,1,1,r,a),t(b,0,1,l,c),t(b,1,1,l,b),t(c,0,0,l,f),t(c,1,1,l,d),t(d,0,1,r,a),t(d,1,0,l,e),t(e,0,0,r,a),t(e,1,1,l,c),t(f,0,1,r,e),t(f,1,1,r,h)],136612,13122572797). 
monster(6,[t(a,0,1,r,b),t(a,1,1,r,a),t(b,0,1,l,c),t(b,1,1,l,b),t(c,0,0,r,f),t(c,1,1,l,d),t(d,0,1,r,a),t(d,1,0,l,e),t(e,0,1,r,h),t(e,1,1,l,f),t(f,0,1,l,a),t(f,1,1,l,c)],95524079,8690333381690951). 
monster(6,[t(a,0,1,r,b),t(a,1,0,l,c),t(b,0,1,l,a),t(b,1,0,r,a),t(c,0,0,l,d),t(c,1,1,r,h),t(d,0,1,r,e),t(d,1,1,l,d),t(e,0,0,l,f),t(e,1,0,l,e),t(f,0,1,r,f),t(f,1,0,l,b)], 17485734, 95547257425490).

m1(5,[t(a,0,1,r,b),t(a,1,1,r,a),t(b,0,1,l,c),t(b,1,1,l,b),t(c,0,1,r,a),t(c,1,1,l,d),t(d,0,1,r,a),t(d,1,1,l,e),t(e,0,1,r,h),t(e,1,0,l,c)],4098,11798826). % best with comp(3)
m2(5,[t(a,0,1,r,b),t(a,1,1,l,c),t(b,0,1,r,c),t(b,1,1,r,b),t(c,0,1,r,d),t(c,1,0,l,e),t(d,0,1,l,a),t(d,1,1,l,d),t(e,0,1,r,h),t(e,1,0,l,a)],4098,47176870). % best with comp(3)
m3(5,[t(a,0,1,r,b),t(a,1,0,l,d),t(b,0,1,l,c),t(b,1,1,r,d),t(c,0,1,l,a),t(c,1,1,l,c),t(d,0,1,r,h),t(d,1,1,r,e),t(e,0,1,r,a),t(e,1,0,r,b)],4097,23554764). % best with comp(3)
m4(5,[t(a,0,1,r,b),t(a,1,1,r,a),t(b,0,1,l,c),t(b,1,1,r,d),t(c,0,1,l,a),t(c,1,1,l,c),t(d,0,1,r,h),t(d,1,0,r,e),t(e,0,1,l,c),t(e,1,1,r,b)],4097,11797896). % best with comp(3)
m5(5,[t(a,0,1,r,b),t(a,1,1,r,a),t(b,0,1,l,c),t(b,1,0,r,d),t(c,0,1,l,a),t(c,1,1,l,c),t(d,0,1,r,h),t(d,1,1,r,e),t(e,0,0,l,e),t(e,1,1,r,b)],4096,11804910).% best with comp(3)
m6(5,[t(a,0,1,r,b),t(a,1,1,r,a),t(b,0,1,l,c),t(b,1,0,r,d),t(c,0,1,l,a),t(c,1,1,l,c),t(d,0,1,r,h),t(d,1,1,r,e),t(e,0,1,l,c),t(e,1,1,r,b)],4096,11804896). % best with comp(3)
m7(5,[t(a,0,1,r,b),t(a,1,1,r,d),t(b,0,1,l,c),t(b,1,0,l,e),t(c,0,0,r,a),t(c,1,0,l,b),t(d,0,1,r,e),t(d,1,1,r,h),t(e,0,1,l,c),t(e,1,1,r,c)],1471,2358064). % best with comp(4)
m8(5,[t(a,0,1,r,b),t(a,1,1,l,c),t(b,0,0,l,a),t(b,1,0,l,d),t(c,0,1,l,a),t(c,1,1,r,h),t(d,0,1,l,b),t(d,1,1,r,e),t(e,0,0,r,d),t(e,1,0,r,b)],1915,2133492). % best with comp(4)
m9(5,[t(a,0,1,r,b),t(a,1,0,l,c),t(b,0,1,r,c),t(b,1,1,r,d),t(c,0,1,l,a),t(c,1,0,r,b),t(d,0,0,r,e),t(d,1,1,r,h),t(e,0,1,l,c),t(e,1,1,r,a)],501, 134467).  % best with comp(4)

interest(3,[t(a,0,1,r,b),t(a,1,1,l,c),t(b,0,1,r,c),t(b,1,1,r,h),t(c,0,1,l,a),t(c,1,0,l,b)],6, 11).
interest(4,[t(a,0,1,r,b),t(b,0,1,r,c),t(b,1,1,r,h),t(c,0,1,l,d),t(c,1,1,l,c),t(d,0,1,l,a),t(d,1,1,l,c)],6, 9).
interest(5,[t(a,0,1,r,b),t(b,0,1,l,c),t(b,1,1,r,h),t(c,0,1,l,d),t(c,1,1,l,c),t(d,0,1,l,e),t(e,0,1,l,a)],6, 8).
interest(6,[t(a,0,1,r,b),t(b,0,1,r,c),t(c,0,1,r,d),t(d,0,1,r,e),t(e,0,1,r,6),t(6,0,1,r,h)],6, 6).

interest(5,[t(a,0,1,r,b),t(b,0,1,l,b),t(b,1,1,l,a),t(a,1,0,l,c),t(c,0,1,l,d),t(d,0,1,r,e),t(e,1,1,r,d),t(d,1,0,r,b),t(c,1,1,l,a),t(e,0,1,r,h)], 12, 49).
interest(5,[t(a,0,1,r,b),t(b,0,1,l,b),t(b,1,1,l,a),t(a,1,1,l,c),t(c,0,1,l,d),t(d,0,1,r,a),t(c,1,1,r,e),t(e,1,1,r,c),t(e,0,1,r,d),t(d,1,1,r,h)], 10, 26).
interest(5,[t(a,0,1,r,b),t(b,0,1,r,c),t(c,0,1,r,d),t(d,0,1,l,e),t(e,1,0,l,e),t(e,0,1,r,a),t(d,1,1,l,c),t(c,1,0,r,a),t(a,1,1,r,a),t(b,1,1,r,h)],31,512).

interest(5,[t(a,0,1,r,b),t(b,0,1,l,a),t(a,1,0,l,c),t(c,0,0,l,b),t(b,1,1,r,d),t(d,0,1,r,a),t(c,1,1,l,e),t(e,1,1,l,c),t(e,0,0,l,a),t(d,1,1,r,h)],14,41).
interest(5,[t(a,0,1,r,b),t(b,0,1,l,a),t(a,1,1,l,c),t(c,0,0,l,b),t(b,1,1,r,b),t(c,1,1,l,d),t(d,0,1,l,a),t(d,1,1,l,e),t(e,1,0,l,c),t(e,0,1,r,h)],15,54).
interest(5,[t(a,0,1,r,b),t(b,0,1,l,a),t(a,1,1,l,c),t(c,0,0,l,b),t(b,1,1,r,d),t(d,0,1,r,b),t(d,1,0,r,b),t(c,1,1,l,e),t(e,1,0,l,a),t(e,0,1,r,h)],16,59).
interest(5,[t(a,0,1,r,b),t(b,0,1,l,a),t(a,1,1,l,c),t(c,0,0,l,b),t(b,1,1,r,b),t(c,1,1,l,d),t(d,0,1,l,b),t(d,1,1,l,e),t(e,1,0,l,c),t(e,0,1,r,h)],17,63).
interest(5,[t(a,0,1,r,b),t(b,0,1,l,a),t(a,1,1,l,b),t(b,1,1,l,c),t(c,1,0,l,c),t(c,0,1,l,d),t(d,0,1,r,e),t(e,1,1,r,e),t(e,0,0,r,a),t(d,1,1,r,h)],18,91).
interest(5,[t(a,0,1,r,b),t(b,0,1,l,a),t(a,1,0,l,c),t(c,0,1,l,a),t(b,1,1,r,d),t(d,0,1,r,b),t(c,1,1,r,b),t(d,1,1,r,e),t(e,1,0,r,c),t(e,0,1,r,h)],19,189).
interest(5,[t(a,0,1,r,b),t(b,0,1,l,a),t(a,1,1,l,c),t(c,0,1,l,d),t(d,0,1,l,a),t(b,1,0,r,e),t(e,1,1,r,b),t(d,1,0,l,a),t(c,1,0,l,c),t(e,0,1,r,h)],20,118).
interest(5,[t(a,0,1,r,b),t(b,0,1,l,a),t(a,1,1,l,c),t(c,0,1,l,a),t(b,1,1,r,b),t(c,1,1,l,d),t(d,1,1,l,e),t(e,1,0,l,c),t(d,0,1,l,b),t(e,0,1,r,h)],21,112).
interest(5,[t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,1,l,a),t(b,1,1,l,b),t(c,0,1,l,d),t(d,0,1,r,e),t(e,1,1,r,d),t(d,1,0,r,e),t(e,0,0,r,a),t(a,1,1,r,h)],22,127).
interest(5,[t(a,0,1,r,b),t(b,0,1,r,c),t(c,0,1,r,d),t(d,0,0,l,e),t(e,1,1,l,a),t(a,1,1,l,e),t(b,1,1,l,c),t(c,1,0,l,b),t(d,1,1,r,c),t(e,0,1,r,h)],23,282). 
interest(5,[t(a,0,1,r,b),t(b,0,1,l,a),t(a,1,1,l,a),t(b,1,0,r,c),t(c,1,0,r,b),t(c,0,1,l,d),t(d,0,1,l,d),t(d,1,1,l,e),t(e,0,0,l,a),t(e,1,1,r,h)],24,280).
interest(5,[t(a,0,1,r,b),t(b,0,0,l,c),t(c,1,1,l,c),t(c,0,0,l,d),t(d,0,1,r,d),t(d,1,1,r,a),t(a,1,1,r,e),t(e,1,0,l,e),t(e,0,0,l,b),t(b,1,1,r,h)],25,155).
interest(5,[t(a,0,1,r,b),t(b,0,1,r,c),t(c,0,1,r,d),t(d,0,1,l,e),t(e,1,1,l,e),t(e,0,1,l,c),t(d,1,0,r,a),t(a,1,0,r,e),t(c,1,0,l,e),t(b,1,1,r,h)],26,336).
interest(5,[t(a,0,1,r,b),t(b,0,1,r,c),t(c,0,1,r,d),t(d,0,1,r,e),t(e,0,1,l,b),t(b,1,0,l,a),t(a,1,0,l,b),t(e,1,0,r,c),t(d,1,1,r,b),t(c,1,1,r,h)],27,441).
interest(5,[t(a,0,1,r,b),t(b,0,0,l,a),t(a,1,1,l,a),t(b,1,1,r,c),t(c,0,1,l,a),t(c,1,0,r,d),t(d,1,1,l,b),t(d,0,0,r,e),t(e,1,1,r,b),t(e,0,1,r,h)],29,1597). 
interest(5,[t(a,0,1,r,b),t(b,0,1,r,c),t(c,0,1,r,d),t(d,0,1,l,b),t(b,1,1,l,b),t(c,1,1,r,e),t(e,1,1,r,a),t(a,1,0,r,d),t(d,1,1,r,d),t(e,0,1,r,h)],30,299). 
interest(5,[t(a,0,1,r,b),t(b,0,1,l,a),t(a,1,1,l,c),t(c,0,1,l,b),t(b,1,1,r,b),t(c,1,1,l,d),t(d,1,0,l,e),t(e,1,1,l,e),t(e,0,1,r,b),t(d,0,1,r,h)],31,339).
interest(5,[t(a,0,1,r,b),t(b,0,1,r,c),t(c,0,1,r,d),t(d,0,0,r,e),t(e,0,1,l,e),t(e,1,0,l,b),t(b,1,0,l,b),t(d,1,0,r,a),t(a,1,1,l,c),t(c,1,1,r,h)],32,632).
interest(5,[t(a,0,1,r,b),t(b,0,1,l,a),t(a,1,1,l,a),t(b,1,1,r,c),t(c,1,1,r,d),t(d,0,1,r,a),t(d,1,0,r,e),t(e,1,1,r,e),t(e,0,1,l,a),t(c,0,1,r,h)],33,383).
interest(5,[t(a,0,1,r,b),t(b,0,1,l,a),t(a,1,0,l,c),t(c,0,0,l,d),t(d,0,1,l,e),t(e,0,1,r,e),t(e,1,0,r,b),t(b,1,1,r,b),t(c,1,0,l,e),t(d,1,1,r,h)],34,1600).
interest(5,[t(a,0,1,r,b),t(b,0,1,r,c),t(c,0,1,l,d),t(d,1,1,l,d),t(d,0,0,l,e),t(e,0,1,l,a),t(b,1,0,r,a),t(a,1,0,l,e),t(e,1,1,l,c),t(c,1,1,r,h)],35,496).
interest(5,[t(a,0,1,r,b),t(b,0,1,l,a),t(a,1,0,l,c),t(c,0,1,l,d),t(d,0,1,r,a),t(c,1,1,l,a),t(b,1,1,r,e),t(e,0,0,r,d),t(d,1,1,r,d),t(e,1,1,r,h)],36,494).
interest(5,[t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,1,l,d),t(d,0,0,l,c),t(c,0,1,r,a),t(b,1,1,r,e),t(e,1,1,r,c),t(d,1,0,l,a),t(a,1,0,r,c),t(e,0,1,r,h)],37,468). 
interest(5,[t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,1,r,c),t(c,0,0,r,d),t(d,0,1,l,a),t(b,1,1,l,b),t(d,1,1,r,e),t(e,1,0,r,a),t(a,1,1,r,d),t(e,0,1,r,h)],38,1038).
interest(5,[t(a,0,1,r,b),t(b,0,1,l,a),t(a,1,0,r,c),t(c,1,1,r,c),t(c,0,1,l,d),t(d,1,0,l,e),t(e,0,1,l,a),t(b,1,1,r,a),t(e,1,0,l,b),t(d,0,1,r,h)],39,856).
interest(5,[t(a,0,1,r,b),t(b,0,0,r,c),t(c,0,0,r,d),t(d,0,1,l,d),t(d,1,1,l,b),t(c,1,1,r,e),t(e,1,1,r,a),t(a,1,1,r,e),t(b,1,0,r,b),t(e,0,1,r,h)],40,446).
interest(5,[t(a,0,1,r,b),t(b,0,0,l,c),t(c,1,1,l,c),t(c,0,1,l,d),t(d,0,1,l,e),t(e,0,1,r,a),t(a,1,0,r,e),t(e,1,1,r,e),t(d,1,0,l,d),t(b,1,1,r,h)],41,573).
interest(5,[t(a,0,1,r,b),t(b,0,1,r,c),t(c,0,0,l,d),t(d,1,1,l,d),t(d,0,1,l,e),t(e,0,1,l,a),t(b,1,0,r,a),t(a,1,1,r,a),t(e,1,0,l,e),t(c,1,1,r,h)],42,589). 
interest(5,[t(a,0,1,r,b),t(b,0,0,l,c),t(c,1,1,l,c),t(c,0,0,l,d),t(d,0,1,l,a),t(b,1,1,r,a),t(a,1,1,r,e),t(e,1,0,r,e),t(e,0,0,l,a),t(d,1,1,r,h)],43,1422).
interest(5,[t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,1,l,a),t(b,1,0,r,b),t(c,0,1,r,a),t(a,1,1,l,d),t(d,1,0,l,c),t(d,0,1,l,e),t(e,0,0,l,a),t(e,1,1,r,h)],44,2166).
interest(5,[t(a,0,1,r,b),t(b,0,1,r,c),t(c,0,1,l,a),t(a,1,0,l,d),t(d,1,0,r,d),t(d,0,1,l,c),t(b,1,1,r,b),t(c,1,0,r,e),t(e,1,0,r,a),t(e,0,1,r,h)],45,1358).
interest(5,[t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,1,l,d),t(d,0,1,l,e),t(e,0,1,l,a),t(b,1,0,r,a),t(a,1,0,l,e),t(e,1,0,l,a),t(d,1,0,l,b),t(c,0,1,r,h)],47,653). 
interest(5,[t(a,0,1,r,b),t(b,0,1,r,c),t(c,0,0,r,d),t(d,0,1,l,d),t(d,1,0,l,a),t(a,1,0,l,a),t(c,1,0,r,e),t(e,0,0,r,c),t(e,1,1,r,a),t(b,1,1,r,h)],49,1968). 
interest(5,[t(a,0,1,r,b),t(b,0,0,r,c),t(c,0,0,r,d),t(d,0,1,l,d),t(d,1,1,l,e),t(e,0,1,r,c),t(c,1,0,r,a),t(a,1,0,l,e),t(e,1,0,l,a),t(b,1,1,r,h)],51,1988). 
interest(5,[t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,1,l,d),t(d,0,1,r,e),t(e,1,0,r,e),t(e,0,1,r,a),t(d,1,0,l,b),t(c,0,0,l,a),t(a,1,1,l,c),t(b,1,1,r,h)],52,1986). 
interest(5,[t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,0,l,c),t(c,0,1,l,a),t(b,1,1,r,d),t(d,0,0,r,e),t(e,1,0,r,e),t(e,0,1,r,c),t(a,1,1,r,a),t(d,1,1,r,h)],53,2767).
interest(5,[t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,1,l,b),t(c,0,1,l,a),t(b,1,0,l,d),t(d,1,1,l,d),t(d,0,1,r,e),t(e,1,0,r,a),t(a,1,1,r,b),t(e,0,1,r,h)],54,2861).
interest(5,[t(a,0,1,r,b),t(b,0,1,r,c),t(c,0,1,l,d),t(d,1,1,l,e),t(e,1,0,l,c),t(d,0,0,l,b),t(e,0,1,r,a),t(a,1,0,r,a),t(b,1,1,l,d),t(c,1,1,r,h)],55,2217). 
interest(5,[t(a,0,1,r,b),t(b,0,0,r,c),t(c,0,0,r,d),t(d,0,1,l,d),t(d,1,1,l,a),t(b,1,1,r,b),t(a,1,0,l,a),t(c,1,1,r,e),t(e,1,1,r,c),t(e,0,1,r,h)],56,2136).
interest(5,[t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,1,l,b),t(c,0,0,r,a),t(a,1,1,r,d),t(d,1,1,r,d),t(d,0,1,r,e),t(e,0,1,r,c),t(b,1,0,l,b),t(e,1,1,r,h)],57,1887).
interest(5,[t(a,0,1,r,b),t(b,0,0,r,c),t(c,0,1,l,a),t(b,1,1,r,d),t(d,0,1,l,e),t(e,1,0,l,e),t(e,0,1,l,c),t(d,1,0,r,a),t(c,1,1,r,b),t(a,1,1,r,h)],58,2456).
interest(5,[t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,1,l,d),t(d,0,1,r,c),t(d,1,1,l,a),t(b,1,0,r,d),t(c,0,1,r,e),t(e,0,0,r,a),t(a,1,0,l,a),t(e,1,1,r,h)],59,1326). 
interest(5,[t(a,0,1,r,b),t(b,0,1,r,c),t(c,0,1,l,a),t(a,1,0,l,d),t(d,1,1,l,e),t(e,0,0,l,c),t(b,1,1,r,b),t(c,1,1,l,c),t(e,1,1,l,a),t(d,0,1,r,h)],60,2566).
interest(5,[t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,1,l,c),t(c,0,0,l,d),t(d,0,1,r,e),t(e,0,0,r,b),t(b,1,1,r,e),t(e,1,0,r,e),t(d,1,0,l,a),t(a,1,1,r,h)],61,3720). 
interest(5,[t(a,0,1,r,b),t(b,0,1,r,c),t(c,0,1,l,d),t(d,1,1,l,d),t(d,0,1,l,a),t(b,1,0,r,e),t(e,1,0,r,c),t(c,1,0,l,a),t(a,1,1,r,a),t(e,0,1,r,h)],62,1797). 
interest(5,[t(a,0,1,r,b),t(b,0,0,r,c),t(c,0,1,l,d),t(d,0,1,l,e),t(e,1,1,l,e),t(e,0,0,l,a),t(c,1,1,r,b),t(b,1,0,r,b),t(a,1,1,l,d),t(d,1,1,r,h)],63,2938).
interest(5,[t(a,0,1,r,b),t(b,0,0,r,c),t(c,0,1,l,d),t(d,0,0,l,a),t(a,1,1,l,d),t(c,1,1,r,e),t(e,0,1,r,b),t(b,1,1,r,b),t(d,1,0,l,d),t(e,1,1,r,h)],64,3104). 
interest(5,[t(a,0,1,r,b),t(b,0,1,r,c),t(c,0,0,r,d),t(d,0,1,l,e),t(e,0,0,l,a),t(a,1,1,l,e),t(e,1,0,l,e),t(d,1,1,r,b),t(c,1,1,r,c),t(b,1,1,r,h)],65,3187).
interest(5,[t(a,0,1,r,b),t(b,0,0,r,c),t(c,0,1,l,d),t(d,0,0,l,a),t(a,1,1,l,e),t(e,0,1,l,d),t(c,1,1,r,b),t(b,1,0,r,b),t(d,1,1,l,d),t(e,1,1,r,h)],66,3355). 
interest(5,[t(a,0,1,r,b),t(b,0,0,r,c),t(c,0,0,l,d),t(d,0,1,l,e),t(e,1,1,l,e),t(e,0,0,l,a),t(c,1,1,r,b),t(b,1,0,r,b),t(a,1,1,l,d),t(d,1,1,r,h)],67,3858).
interest(5,[t(a,0,1,r,b),t(b,0,0,r,c),t(c,0,1,r,d),t(d,0,1,l,a),t(a,1,0,l,e),t(e,0,1,l,c),t(c,1,0,l,a),t(d,1,1,r,b),t(e,1,0,l,e),t(b,1,1,r,h)],68,3630).
interest(5,[t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,0,l,c),t(c,0,1,l,a),t(b,1,0,r,a),t(a,1,1,r,d),t(d,1,0,r,e),t(e,0,1,l,b),t(e,1,0,r,c),t(d,0,1,r,h)],69,6956).
interest(5,[t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,1,l,d),t(d,0,0,r,e),t(e,1,0,l,b),t(c,0,1,r,a),t(a,1,1,r,c),t(d,1,0,l,b),t(b,1,1,r,d),t(e,0,1,r,h)],70,2821). 
interest(5,[t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,0,l,d),t(d,0,1,l,a),t(b,1,1,l,b),t(c,0,1,r,a),t(a,1,1,r,a),t(d,1,1,l,e),t(e,1,1,l,c),t(e,0,1,r,h)],71,3545).
interest(5,[t(a,0,1,r,b),t(b,0,0,r,c),t(c,0,1,l,d),t(d,0,0,l,a),t(a,1,0,l,e),t(e,0,1,l,d),t(c,1,0,r,e),t(e,1,0,r,d),t(d,1,0,r,a),t(b,1,1,r,h)],72,7383).
interest(5,[t(a,0,1,r,b),t(b,0,0,r,c),t(c,0,1,r,d),t(d,0,1,l,a),t(a,1,1,l,e),t(e,0,1,r,a),t(e,1,1,l,c),t(c,1,0,l,c),t(d,1,0,r,e),t(b,1,1,r,h)],73,2052). 
interest(5,[t(a,0,1,r,b),t(b,0,1,r,c),t(c,0,1,l,d),t(d,1,1,l,b),t(b,1,0,l,b),t(c,1,1,r,e),t(e,1,0,r,d),t(d,0,1,r,a),t(a,1,0,r,a),t(e,0,1,r,h)],76,4172). 
interest(5,[t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,0,l,d),t(d,0,1,r,e),t(e,0,1,r,e),t(e,1,1,r,a),t(d,1,0,l,e),t(a,1,0,r,b),t(b,1,1,r,b),t(c,0,1,r,h)],78,6671). 
interest(5,[t(a,0,1,r,b),t(b,0,1,r,c),t(c,0,1,l,c),t(c,1,0,l,d),t(d,1,1,l,d),t(d,0,1,r,e),t(e,1,1,r,a),t(b,1,1,r,b),t(a,1,0,r,b),t(e,0,1,r,h)],79,4948).
interest(5,[t(a,0,1,r,b),t(b,0,1,r,c),t(c,0,0,r,d),t(d,0,1,r,e),t(e,0,1,l,b),t(b,1,1,l,a),t(a,1,1,l,d),t(d,1,0,l,d),t(e,1,0,r,a),t(c,1,1,r,h)],81,2636). 
interest(5,[t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,0,l,c),t(c,0,1,l,a),t(b,1,1,r,d),t(d,0,1,r,e),t(e,1,1,r,a),t(e,0,0,r,b),t(a,1,0,r,a),t(d,1,1,r,h)],83,5067). 
interest(5,[t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,0,l,b),t(c,0,1,r,d),t(d,1,1,r,e),t(e,0,0,r,a),t(a,1,0,r,b),t(b,1,0,r,a),t(e,1,1,r,c),t(d,0,1,r,h)],87,3189). 
interest(5,[t(a,0,1,r,b),t(b,0,1,r,c),t(c,0,1,l,a),t(a,1,0,l,c),t(c,1,0,l,c),t(b,1,0,r,d),t(d,0,1,r,d),t(d,1,1,r,e),t(e,0,0,r,a),t(e,1,1,r,h)],88,7706).
interest(5,[t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,1,l,d),t(d,0,1,l,e),t(e,0,0,l,c),t(c,0,1,r,a),t(b,1,0,l,b),t(a,1,0,r,a),t(e,1,1,l,b),t(d,1,1,r,h)],89,5685). 
interest(5,[t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,0,l,b),t(c,0,1,r,a),t(a,1,0,r,d),t(d,0,1,r,d),t(d,1,1,r,e),t(e,0,0,r,c),t(b,1,0,l,b),t(e,1,1,r,h)],91,8245). 
interest(5,[t(a,0,1,r,b),t(b,0,0,r,c),t(c,0,0,r,d),t(d,0,1,l,d),t(d,1,1,l,e),t(e,0,0,l,a),t(c,1,1,r,c),t(e,1,0,r,b),t(b,1,0,r,b),t(a,1,1,r,h)],99,2411). 
interest(5,[t(a,0,1,r,b),t(b,0,1,r,c),t(c,0,1,l,d),t(d,1,1,l,d),t(d,0,1,l,e),t(e,0,1,l,a),t(b,1,0,r,a),t(a,1,0,l,e),t(e,1,0,l,c),t(c,1,1,r,h)],112,6147).

magic(4, [t(a,0,1,r,b),t(b,0,1,r,c),t(c,0,1,l,d),t(d,1,0,l,c),t(c,1,0,r,b),t(d,0,1,r,b),t(b,1,1,r,a),t(a,1,1,r,h)]).
magic(4, [t(a,0,1,r,b),t(b,0,1,r,c),t(c,0,1,l,a),t(a,1,0,l,c),t(c,1,0,r,b),t(b,1,1,r,d),t(d,0,1,r,b),t(d,1,1,r,h)]). 
magic(4, [t(a,0,1,r,b),t(b,0,0,r,c),t(c,0,1,r,d),t(d,0,0,l,b),t(b,1,1,l,d),t(d,1,1,r,c),t(c,1,0,r,a),t(a,1,1,r,h)]).

brady(4, [t(a,0,1,r,b),t(a,1,0,l,c),t(b,0,1,l,a),t(b,1,1,r,a),t(c,0,0,r,a),t(c,1,0,l,d),t(d,0,1,r,h),t(d,1,1,l,c)], "ternary counter"). % loops(induction)
brady(4, [t(a,0,1,r,b),t(a,1,0,r,d),t(b,0,1,r,c),t(b,1,1,r,h),t(c,0,0,l,a),t(c,1,1,r,a),t(d,0,1,l,c),t(d,1,1,r,d)], "tail-eating dragon (fast)"). % hyp. multiplicative, 1{2}b1^n -> 1{2}b1^{3n-2}, commencing at n = 2
brady(4, [t(a,0,1,r,b),t(a,1,1,l,a),t(b,0,1,r,c),t(b,1,0,r,d),t(c,0,1,l,a),t(c,1,1,r,h),t(d,0,0,l,a),t(d,1,1,r,d)], "tail-eating dragon (slow)"). % loops(induction)
brady(4, [t(a,0,1,r,b),t(a,1,0,l,c),t(b,0,1,l,a),t(b,1,0,r,d),t(c,0,0,l,b),t(c,1,0,l,b),t(d,0,1,r,a),t(d,1,1,r,h)], "Christmas tree"). % loops(induction)
brady(4, [t(a,0,1,r,b),t(a,1,0,l,c),t(b,0,0,l,a),t(b,1,1,r,d),t(c,0,1,l,a),t(c,1,1,l,b),t(d,0,0,r,a),t(d,1,1,r,h)], "leaning tree"). % blanks!!! 
brady(4, [t(a,0,1,r,b),t(a,1,1,l,a),t(b,0,0,l,a),t(b,1,0,r,c),t(c,0,1,r,d),t(c,1,1,r,c),t(d,0,1,l,a),t(d,1,1,r,h)], "shadow tree"). % loops(induction)
brady(4, [t(a,0,1,r,b),t(a,1,0,l,c),t(b,0,1,l,a),t(b,1,0,r,c),t(c,0,1,l,d),t(c,1,0,r,a),t(d,0,1,l,a),t(d,1,1,r,h)], "alternating tree"). % loops(induction)
brady(4, [t(a,0,1,r,b),t(a,1,1,l,c),t(b,0,0,l,a),t(b,1,0,r,b),t(c,0,1,r,a),t(c,1,1,l,d),t(d,0,1,l,a),t(d,1,1,r,h)], "counter (c-square cell)"). % loops(induction) % 15 unclassififed additive, 41 killer kangaroos
brady(4, [t(a,0,1,r,b),t(a,1,1,l,c),t(b,0,0,l,a),t(b,1,1,r,d),t(c,0,1,r,a),t(c,1,1,l,a),t(d,0,1,r,h),t(d,1,0,r,b)], "counter (nonblank zero)"). % loops(induction)

ligocki(3,3,[t(a,0,1,r,b),t(a,1,2,r,c),t(a,2,1,l,a),t(b,0,2,l,a),t(b,1,1,r,b),t(b,2,1,r,h),t(c,0,2,r,b),t(c,1,2,r,a),t(c,2,1,l,c)], "3x3 champ"). 

addictive([t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,0,l,d),t(d,0,1,r,a),t(b,1,1,r,b),t(d,1,1,l,d),t(a,1,0,r,b),t(c,0,1,r,h)],0,0,hyp(induction(state([tape([1],_23147)],1,l,[b,tape([1],_23159)]),state([1,tape([1],_23147)],1,_23143,[b,1,tape([1],_23159)])))). % additive
addictive([t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,0,l,d),t(d,0,1,r,a),t(b,1,0,r,c),t(c,0,1,r,d),t(d,1,0,l,c),t(a,1,1,r,h)],0,0,hyp(induction(state([tape([1],_2600d)],1,l,[b,tape([1],_26016)]),state([1,tape([1],_2600d)],1,_26000,[b,1,tape([1],_26016)])))). % addtive
addictive([t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,0,l,d),t(d,0,1,l,b),t(c,0,1,r,a),t(a,1,0,r,b),t(b,1,0,r,a),t(d,1,1,r,h)],0,0,hyp(induction(state([tape([b,0,1],_2665c)],1,l,[b,tape([1],_26669)]),state([b,0,1,tape([b,0,1],_2665c)],1,_26649,[b,1,tape([1],_26669)])))). % additive
addictive([t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,0,l,d),t(d,0,0,l,c),t(c,0,1,r,c),t(d,1,1,r,a),t(b,1,0,r,a),t(a,1,1,r,h)],0,0,hyp(induction(state([tape([1,1,1],_2432a)],1,l,[b]),state([1,1,1,tape([1,1,1],_2432a)],1,_24317,[b])))). % additive
addictive([t(a,0,1,r,b),t(b,0,1,l,a),t(a,1,1,l,a),t(b,1,0,r,c),t(c,1,1,r,c),t(c,0,1,l,d),t(d,1,0,l,a),t(d,0,1,r,h)],0,0,hyp(induction(state([],1,l,[b,tape([1,1],_2304d)]),state([],1,_23040,[b,1,1,tape([1,1],_2304d)])))). % additive
addictive([t(a,0,1,r,b),t(b,0,1,l,b),t(b,1,1,r,c),t(c,1,0,r,c),t(c,0,1,l,d),t(d,0,0,l,b),t(d,1,0,l,a),t(a,1,1,r,h)],0,0,hyp(induction(state([],1,l,[b,tape([b,1,1],_2166a)]),state([],1,_21657,[b,0,1,1,tape([b,1,1],_2166a)])))). % additive
addictive([t(a,0,1,r,b),t(b,0,1,r,c),t(c,0,0,l,a),t(a,1,0,r,d),t(d,0,1,l,d),t(d,1,0,l,a),t(c,1,1,r,a),t(b,1,1,r,h)],0,0,hyp(induction(state([],1,l,[b,tape([b,1,1],_2494a)]),state([],1,_24937,[b,0,1,1,tape([b,1,1],_2494a)])))). % additive
addictive([t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,1,l,a),t(b,1,0,r,b),t(c,0,0,l,d),t(d,0,1,l,d),t(d,1,1,r,b),t(a,1,1,r,h)],0,0,hyp(induction(state([],1,l,[b,tape([1,1],_21807)]),state([],1,_21803,[b,1,1,tape([1,1],_21807)])))). % additive
addictive([t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,1,l,a),t(b,1,1,r,b),t(a,1,0,l,d),t(d,1,1,l,d),t(d,0,0,r,b),t(c,0,1,r,h)],0,0,hyp(induction(state([],1,l,[b,tape([1,1],_23065)]),state([],1,_23061,[b,1,1,tape([1,1],_23065)])))). % additive
addictive([t(a,0,1,r,b),t(b,0,0,r,c),t(c,0,1,r,d),t(d,0,1,l,a),t(a,1,0,l,c),t(c,1,1,r,b),t(b,1,0,r,b),t(d,1,1,r,h)],0,0,going). % additive, no hyps found
addictive([t(a,0,1,r,b),t(b,0,1,r,c),t(c,0,1,l,a),t(a,1,0,l,b),t(b,1,1,r,d),t(d,0,0,r,b),t(d,1,0,r,d),t(c,1,1,r,h)],0,0,going). % additive, no hyps found
addictive([t(a,0,1,r,b),t(b,0,1,l,a),t(a,1,1,l,a),t(b,1,0,r,c),t(c,1,0,r,d),t(d,0,1,r,a),t(d,1,1,r,d),t(c,0,1,r,h)],0,0,going). % additive, no hyps found
addictive([t(a,0,1,r,b),t(b,0,1,l,a),t(a,1,1,l,b),t(b,1,0,r,c),t(c,1,0,l,d),t(d,0,1,l,c),t(c,0,1,r,b),t(d,1,1,r,h)],0,0,going). % additive, no hyps found
addictive([t(a,0,1,r,b),t(b,0,0,r,c),t(c,0,1,l,a),t(b,1,1,l,b),t(c,1,1,r,d),t(d,1,0,r,a),t(a,1,1,r,a),t(d,0,1,r,h)],0,0,going). % additive, no hyps found
addictive([t(a,0,1,r,b),t(b,0,1,r,c),t(c,0,1,l,b),t(b,1,1,l,b),t(c,1,0,r,d),t(d,1,0,r,a),t(a,1,1,r,a),t(d,0,1,r,h)],0,0,going). % additive, no hyps found
kangaroo([t(a,0,1,r,b),t(b,0,1,l,a),t(a,1,0,l,c),t(c,0,1,l,a),t(b,1,1,r,a),t(c,1,0,r,d),t(d,0,1,r,c),t(d,1,1,r,h)],0,0,going). % killer kangaroo
kangaroo([t(a,0,1,r,b),t(b,0,0,r,c),t(c,0,1,l,c),t(c,1,0,l,d),t(d,0,1,l,a),t(b,1,0,r,b),t(d,1,0,r,d),t(a,1,1,r,h)],0,0,going). % killer kangaroo
kangaroo([t(a,0,1,r,b),t(b,0,0,r,c),t(c,0,1,l,d),t(d,0,1,l,b),t(b,1,1,l,c),t(c,1,0,l,a),t(a,1,1,l,a),t(d,1,1,r,h)],0,0,going). % killer kangaroo
kangaroo([t(a,0,1,r,b),t(b,0,0,r,c),t(c,0,1,l,d),t(d,0,1,l,c),t(c,1,0,l,a),t(a,1,1,l,a),t(b,1,0,r,c),t(d,1,1,r,h)],0,0,going). % killer kangaroo
kangaroo([t(a,0,1,r,b),t(b,0,0,r,c),t(c,0,1,l,d),t(d,0,1,l,c),t(c,1,0,l,a),t(a,1,1,l,b),t(b,1,1,l,b),t(d,1,1,r,h)],0,0,going). % killer kangaroo
kangaroo([t(a,0,1,r,b),t(b,0,0,r,c),t(c,0,1,r,d),t(d,0,1,l,a),t(a,1,0,l,d),t(b,1,1,r,a),t(d,1,0,r,c),t(c,1,1,r,h)],0,0,going). % killer kangaroo
kangaroo([t(a,0,1,r,b),t(b,0,0,r,c),t(c,0,1,r,d),t(d,0,0,l,b),t(b,1,1,l,d),t(d,1,1,r,c),t(c,1,0,r,a),t(a,1,1,r,h)],0,0,going). % killer kangaroo (!!)
kangaroo([t(a,0,1,r,b),t(b,0,1,r,c),t(c,0,0,l,a),t(a,1,1,l,c),t(c,1,0,l,b),t(b,1,0,r,d),t(d,0,0,r,a),t(d,1,1,r,h)],0,0,going). % killer kangaroo
kangaroo([t(a,0,1,r,b),t(b,0,1,r,c),t(c,0,1,l,a),t(a,1,0,l,c),t(c,1,0,r,b),t(b,1,1,r,d),t(d,0,1,r,b),t(d,1,1,r,h)],0,0,going). % killer kangaroo
kangaroo([t(a,0,1,r,b),t(b,0,1,r,c),t(c,0,1,l,a),t(a,1,0,l,c),t(c,1,1,l,d),t(d,0,1,l,c),t(b,1,0,r,a),t(d,1,1,r,h)],0,0,going). % killer kangaroo
kangaroo([t(a,0,1,r,b),t(b,0,1,r,c),t(c,0,1,l,a),t(a,1,0,l,c),t(c,1,0,r,d),t(d,0,1,r,c),t(b,1,1,r,a),t(d,1,1,r,h)],0,0,going). % killer kangaroo
kangaroo([t(a,0,1,r,b),t(b,0,1,r,c),t(c,0,1,l,d),t(d,1,0,l,c),t(c,1,0,r,b),t(d,0,1,r,a),t(a,1,1,r,d),t(b,1,1,r,h)],0,0,going). % killer kangaroo
kangaroo([t(a,0,1,r,b),t(b,0,1,r,c),t(c,0,1,l,d),t(d,1,0,l,c),t(c,1,0,r,b),t(d,0,1,l,b),t(b,1,1,r,a),t(a,1,1,r,h)],0,0,going). % killer kangaroo
kangaroo([t(a,0,1,r,b),t(b,0,1,r,c),t(c,0,1,l,d),t(d,1,0,l,c),t(c,1,0,r,b),t(d,0,0,r,b),t(b,1,1,r,a),t(a,1,1,r,h)],0,0,going). % killer kangaroo
kangaroo([t(a,0,1,r,b),t(b,0,1,r,c),t(c,0,1,l,d),t(d,1,0,l,c),t(c,1,0,r,b),t(d,0,1,r,b),t(b,1,1,r,a),t(a,1,1,r,h)],0,0,going). % killer kangaroo
kangaroo([t(a,0,1,r,b),t(b,0,1,r,c),t(c,0,1,r,d),t(d,0,1,l,a),t(a,1,0,l,d),t(d,1,0,r,c),t(b,1,1,r,a),t(c,1,1,r,h)],0,0,going). % killer kangaroo
kangaroo([t(a,0,1,r,b),t(b,0,0,l,c),t(c,1,1,l,b),t(c,0,0,r,a),t(b,1,1,r,a),t(a,1,0,r,d),t(d,0,1,r,c),t(d,1,1,r,h)],0,0,going). % killer kangaroo (!!)
kangaroo([t(a,0,1,r,b),t(b,0,0,l,c),t(c,1,1,l,c),t(c,0,0,r,b),t(b,1,1,r,a),t(a,1,1,l,d),t(d,1,0,l,a),t(d,0,1,r,h)],0,0,going). % killer kangaroo 
kangaroo([t(a,0,1,r,b),t(b,0,0,l,c),t(c,1,1,l,d),t(d,0,1,l,c),t(c,0,1,l,a),t(b,1,0,r,a),t(a,1,0,l,c),t(d,1,1,r,h)],0,0,going). % killer kangaroo 
kangaroo([t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,0,l,b),t(c,0,1,l,a),t(b,1,0,r,a),t(a,1,1,r,d),t(d,0,1,r,a),t(d,1,1,r,h)],0,0,going). % killer kangaroo 
kangaroo([t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,0,l,b),t(c,0,0,r,a),t(a,1,1,r,d),t(d,0,1,r,a),t(b,1,0,r,a),t(d,1,1,r,h)],0,0,going). % killer kangaroo 
kangaroo([t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,0,l,b),t(c,0,1,r,a),t(a,1,0,r,c),t(b,1,1,l,d),t(d,0,1,l,b),t(d,1,1,r,h)],0,0,going). % killer kangaroo 
kangaroo([t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,0,l,b),t(c,0,1,r,a),t(a,1,1,r,c),t(b,1,0,r,d),t(d,0,1,r,b),t(d,1,1,r,h)],0,0,going). % killer kangaroo 
kangaroo([t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,0,l,b),t(c,0,1,r,a),t(a,1,1,r,d),t(d,0,1,r,a),t(b,1,0,r,a),t(d,1,1,r,h)],0,0,going). % killer kangaroo 
kangaroo([t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,0,l,b),t(c,0,1,r,d),t(d,1,1,r,c),t(d,0,0,r,a),t(b,1,0,r,a),t(a,1,1,r,h)],0,0,going). % killer kangaroo 
kangaroo([t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,0,l,b),t(c,0,1,r,d),t(d,1,1,r,c),t(d,0,1,r,a),t(b,1,0,r,a),t(a,1,1,r,h)],0,0,going). % killer kangaroo 
kangaroo([t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,0,l,b),t(c,0,1,r,d),t(d,1,1,r,c),t(d,0,0,l,b),t(b,1,0,r,a),t(a,1,1,r,h)],0,0,going). % killer kangaroo 
kangaroo([t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,0,l,b),t(c,0,1,r,d),t(d,1,1,r,c),t(d,0,1,r,b),t(b,1,0,r,a),t(a,1,1,r,h)],0,0,going). % killer kangaroo 
kangaroo([t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,0,l,b),t(c,0,1,r,d),t(d,1,1,r,c),t(d,0,0,l,c),t(b,1,0,r,a),t(a,1,1,r,h)],0,0,going). % killer kangaroo 
kangaroo([t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,0,l,b),t(c,0,1,r,d),t(d,1,1,r,c),t(d,0,1,l,c),t(b,1,0,r,a),t(a,1,1,r,h)],0,0,going). % killer kangaroo 
kangaroo([t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,0,l,b),t(c,0,1,r,d),t(d,1,1,r,c),t(d,0,1,l,d),t(b,1,0,r,a),t(a,1,1,r,h)],0,0,going). % killer kangaroo 
kangaroo([t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,1,l,b),t(c,0,1,l,a),t(b,1,0,r,a),t(a,1,0,l,d),t(d,0,1,l,a),t(d,1,1,r,h)],0,0,going). % killer kangaroo 
kangaroo([t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,1,l,b),t(c,0,0,r,a),t(a,1,0,l,d),t(d,0,1,l,a),t(b,1,0,r,a),t(d,1,1,r,h)],0,0,going). % killer kangaroo 
kangaroo([t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,1,l,b),t(c,0,0,r,b),t(b,1,0,r,a),t(a,1,0,l,d),t(d,0,1,l,a),t(d,1,1,r,h)],0,0,going). % killer kangaroo 
kangaroo([t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,1,l,b),t(c,0,1,r,b),t(b,1,0,r,a),t(a,1,0,l,d),t(d,0,1,l,a),t(d,1,1,r,h)],0,0,going). % killer kangaroo 
kangaroo([t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,1,l,b),t(c,0,1,r,c),t(b,1,0,r,a),t(a,1,0,l,d),t(d,0,1,l,a),t(d,1,1,r,h)],0,0,going). % killer kangaroo 
kangaroo([t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,1,l,b),t(c,0,0,l,d),t(d,0,1,l,a),t(b,1,0,r,a),t(a,1,0,l,d),t(d,1,1,r,h)],0,0,going). % killer kangaroo 
kangaroo([t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,1,l,b),t(c,0,1,l,d),t(d,0,1,l,a),t(b,1,0,r,a),t(a,1,0,l,d),t(d,1,1,r,h)],0,0,going). % killer kangaroo 
kangaroo([t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,0,l,c),t(c,0,0,l,d),t(d,0,1,r,d),t(d,1,0,r,a),t(a,1,0,l,a),t(b,1,1,r,h)],0,0,going). % killer kangaroo 
kangaroo([t(a,0,1,r,b),t(b,0,1,l,c),t(c,1,1,l,d),t(d,0,1,l,c),t(c,0,1,l,a),t(b,1,0,r,a),t(a,1,0,l,c),t(d,1,1,r,h)],0,0,going). % killer kangaroo 
kangaroo([t(a,0,1,r,b),t(b,0,1,r,c),t(c,0,0,l,a),t(a,1,0,r,d),t(d,0,1,l,c),t(c,1,1,r,a),t(d,1,1,r,d),t(b,1,1,r,h)],0,0,hyp(induction(state([],1,l,[b,tape([b,1,1],_24245)]),state([],1,_24241,[b,0,1,1,tape([b,1,1],_24245)])))). % killer kangaroo

roo(1, [t(a,0,1,r,b),t(b,0,0,l,a),t(a,1,2,l,a),t(b,2,2,r,b),t(a,2,1,r,a),t(b,1,1,r,h)]). 
roo(2, [t(a,0,1,r,b),t(b,0,2,l,a),t(a,1,1,l,a),t(b,1,2,l,b),t(b,2,1,r,b),t(a,2,1,r,h)]). 
roo(3, [t(a,0,1,r,b),t(b,0,2,l,a),t(a,1,2,l,a),t(b,2,2,r,b),t(a,2,1,r,a),t(b,1,1,r,h)]). 
roo(4, [t(a,0,1,r,b),t(b,0,2,l,a),t(a,1,2,r,a),t(a,2,1,l,a),t(b,1,1,r,b),t(b,2,1,r,h)]).