The file contains the mapping from variables of the SAL model NFM2014_submission16.sal to universally quantified variables in the QBF formula NFM2014_submission16.qdimacs Note that the variables in the SAL module are of type {one, zero, nil, nil2} and hence two Boolean variable are necessary to encode their values. Such encoding is as follows: [0,0] ---> zero [0,1] ---> one [1,0] ---> nil [1,1] ---> nil2 Since nil2 and nil are actually synonims, when interpreting a synthetized strategy we can safely assume that: [0,0] ---> zero [0,1] ---> one [1,0] ---> nil [1,1] ---> nil cvUpdate_zero_zero_zero_zero_zero ---> [6199, 6202] cvUpdate_one_nil_one_one_nil ---> [6024, 6027] cvUpdate_nil_zero_nil_zero_nil ---> [5940, 5943] cvUpdate_zero_zero_nil_nil_nil ---> [6150, 6153] cvUpdate_nil_one_one_one_one ---> [5919, 5922] cvUpdate_nil_nil_nil_one_nil ---> [5786, 5789] cvUpdate_nil_zero_nil_nil_nil ---> [5926, 5929] cvUpdate_nil_nil_one_nil_one ---> [5821, 5824] cvUpdate_zero_nil_nil_zero_zero ---> [6115, 6118] cvUpdate_one_one_nil_one_nil ---> [6052, 6055] cvUpdate_nil_nil_one_one_one ---> [5835, 5838] cvUpdate_nil_zero_zero_nil_zero ---> [5961, 5964] cvUpdate_one_nil_one_nil_nil ---> [6010, 6013] cvUpdate_nil_nil_nil_nil_one ---> [5772, 5775] cvUpdate_zero_zero_nil_zero_nil ---> [6164, 6167] cvUpdate_zero_nil_nil_nil_nil ---> [6094, 6097] cvUpdate_nil_zero_nil_nil_zero ---> [5933, 5936] cvUpdate_one_one_one_one_one ---> [6087, 6090] cvUpdate_zero_nil_zero_zero_zero ---> [6143, 6146] cvUpdate_one_one_one_nil_nil ---> [6066, 6069] cvUpdate_nil_nil_nil_one_one ---> [5793, 5796] cvUpdate_zero_zero_nil_zero_zero ---> [6171, 6174] cvUpdate_nil_zero_zero_nil_nil ---> [5954, 5957] cvUpdate_zero_nil_zero_nil_nil ---> [6122, 6125] cvUpdate_nil_one_one_nil_one ---> [5905, 5908] cvUpdate_zero_zero_zero_nil_zero ---> [6185, 6188] cvUpdate_nil_nil_nil_nil_zero ---> [5779, 5782] cvUpdate_nil_one_nil_nil_nil ---> [5870, 5873] cvUpdate_nil_nil_zero_nil_nil ---> [5842, 5845] cvUpdate_nil_nil_zero_zero_zero ---> [5863, 5866] cvUpdate_nil_one_one_one_nil ---> [5912, 5915] cvUpdate_nil_nil_nil_zero_nil ---> [5800, 5803] cvUpdate_zero_nil_nil_nil_zero ---> [6101, 6104] cvUpdate_zero_zero_zero_nil_nil ---> [6178, 6181] cvUpdate_nil_one_nil_one_one ---> [5891, 5894] cvUpdate_one_nil_one_one_one ---> [6031, 6034] cvUpdate_nil_one_nil_one_nil ---> [5884, 5887] cvUpdate_nil_nil_nil_zero_zero ---> [5807, 5810] cvUpdate_one_nil_nil_nil_one ---> [5989, 5992] cvUpdate_nil_nil_one_nil_nil ---> [5814, 5817] cvUpdate_nil_nil_zero_nil_zero ---> [5849, 5852] cvUpdate_nil_nil_nil_nil_nil ---> [5765, 5768] cvUpdate_zero_zero_zero_zero_nil ---> [6192, 6195] cvUpdate_one_nil_one_nil_one ---> [6017, 6020] cvUpdate_one_nil_nil_one_nil ---> [5996, 5999] cvUpdate_one_nil_nil_one_one ---> [6003, 6006] cvUpdate_zero_nil_zero_zero_nil ---> [6136, 6139] cvUpdate_nil_zero_zero_zero_nil ---> [5968, 5971] cvUpdate_one_one_one_nil_one ---> [6073, 6076] cvUpdate_nil_nil_one_one_nil ---> [5828, 5831] cvUpdate_nil_one_one_nil_nil ---> [5898, 5901] cvUpdate_zero_zero_nil_nil_zero ---> [6157, 6160] cvUpdate_one_one_nil_nil_nil ---> [6038, 6041] cvUpdate_nil_nil_zero_zero_nil ---> [5856, 5859] cvUpdate_one_one_one_one_nil ---> [6080, 6083] cvUpdate_zero_nil_zero_nil_zero ---> [6129, 6132] cvUpdate_nil_zero_nil_zero_zero ---> [5947, 5950] cvUpdate_nil_zero_zero_zero_zero ---> [5975, 5978] cvUpdate_nil_one_nil_nil_one ---> [5877, 5880] cvUpdate_one_one_nil_nil_one ---> [6045, 6048] cvUpdate_one_one_nil_one_one ---> [6059, 6062] cvUpdate_zero_nil_nil_zero_nil ---> [6108, 6111] cvUpdate_one_nil_nil_nil_nil ---> [5982, 5985]