{"text_format":"5","workbook":"xls","n_sheets":3,"sheets":["Sheet1","Sheet2","Sheet3"],"props":{"last_modified_by":"George Hagen"},"read":"whole","wrapped":"gz","date_system":"1900","formulas":"cached_only"}

{"sheet":"Sheet1","index":0,"n_rows":851,"n_cols":30,"rows_kept":851,"flags":["formulas_cached_only"]}
[{"$nulls":3},"kind bmc",null,null,"kind bmc w/abstraction",null,null,"sal bmc",null,null,"kind inductive + path compression",null,null,"kind inductive + path compression w/abstraction",null,null,"sal inductive +acyclic",null,null,"luke",null,null,"rantanplan",null,null,"lesar"]
["valid?","group","filename","result","steps","tottime","result","steps","tottime","result","steps","finaltime","result","steps","tottime","result","steps","tottime","result","steps","tottime","result","steps","tottime","result","steps","tottime","result","steps","tottime"]
["invalid","misc","_6counter","cex",7,0.03,"cex",7,0.04,"cex",6,0.34,"--","--","--","cex",7,0.15,"--","--","--","cex",7,0.03,"cex",7,0.3,"--","--","--"]
["invalid","misc","_6counter2","cex",6,0.01,"cex",6,0.03,"cex",5,0.29,"--","--","--","cex",6,0.09,"--","--","--","cex",6,0.29,"cex",6,0.01,"--","--","--"]
["invalid","misc","_6countern","cex",2,0.01,"cex",2,0.02,"cex",0,0.22,"--","--","--","cex",2,0.02,"--","--","--","cex",1,0.02,"cex",1,0.02,"--","--","--"]
["invalid","misc","_6counters","cex",11,0.03,"cex",11,0.07,"cex",10,0.44,"--","--","--","cex",11,0.34,"--","--","--","cex",11,0.15,"cex",6,0.06,"--","--","--"]
["invalid","misc","_6counters_e8_371_e7_304","cex",6,0.02,"cex",6,0.04,"cex",5,0.3,"--","--","--","cex",6,0.12,"--","--","--","cex",6,0.05,"cex",6,0.04,"--","--","--"]
["invalid","simulation","car_3_e1_586","cex",3,0.02,"cex",3,0.05,"cex",2,0.24,"--","--","--","cex",3,0.05,"--","--","--","cex",3,0.08,"cex",3,0.08,"--","--","--"]
["invalid","simulation","car_3_e1_924","cex",3,0.02,"cex",3,0.04,"cex",2,0.25,"--","--","--","cex",3,0.05,"--","--","--","cex",3,0.08,"cex",3,0.04,"--","--","--"]
["invalid","simulation","car_3_e7_626_e1_305","cex",3,0.02,"cex",3,0.05,"cex",2,0.25,"--","--","--","cex",3,0.05,"--","--","--","cex",3,0.08,"cex",3,0.03,"--","--","--"]
["invalid","simulation","car_3_e8_33_e1_856","cex",3,0.02,"cex",3,0.05,"cex",2,0.25,"--","--","--","cex",3,0.07,"--","--","--","cex",3,0.04,"cex",3,0.05,"--","--","--"]
["invalid","simulation","car_4_e3_556","cex",2,0.01,"cex",2,0.03,"cex",1,0.23,"--","--","--","cex",2,0.04,"--","--","--","cex",2,0.06,"cex",2,0.5,"--","--","--"]
["invalid","simulation","car_4_e3_57","cex",2,0.04,"cex",2,0.04,"cex",1,0.22,"--","--","--","cex",2,0.04,"--","--","--","cex",2,0.06,"cex",2,0.03,"--","--","--"]
["invalid","simulation","car_4_e3_57_e5_999","cex",2,0.01,"cex",2,0.03,"cex",1,0.23,"--","--","--","cex",2,0.05,"--","--","--","cex",2,0.03,"cex",2,0.04,"--","--","--"]
["invalid","simulation","car_4_e3_57_e7_350","cex",2,0.01,"cex",2,0.03,"cex",1,0.23,"--","--","--","cex",2,0.04,"--","--","--","cex",2,0.06,"cex",2,0.02,"--","--","--"]
["invalid","simulation","car_4_e7_592_e3_442","cex",2,0.01,"cex",2,0.03,"cex",1,0.22,"--","--","--","cex",2,0.04,"--","--","--","cex",2,0.06,"cex",2,0.03,"--","--","--"]
["invalid","simulation","car_4_e8_118_e3_514","cex",2,0.04,"cex",2,0.04,"cex",1,0.23,"--","--","--","cex",2,0.05,"--","--","--","cex",2,0.03,"cex",2,0.02,"--","--","--"]
["invalid","simulation","car_5_e2_405_e2_1083","cex",11,0.1,"cex",11,0.19,"cex",10,0.55,"--","--","--","cex",11,1.05,"--","--","--","cex",11,0.37,"cex",11,4.66,"--","--","--"]
["invalid","simulation","car_5_e2_405_e3_473","cex",11,0.09,"cex",11,0.19,"cex",10,0.54,"--","--","--","cex",11,0.95,"--","--","--","cex",11,0.29,"cex",11,3.89,"--","--","--"]
["invalid","simulation","car_5_e2_405_e7_1028","cex",11,0.09,"cex",11,0.19,"cex",10,0.5,"--","--","--","cex",11,0.94,"--","--","--","cex",11,0.32,"cex",11,5.51,"--","--","--"]
["invalid","simulation","car_5_e2_405_e8_1055","cex",11,0.09,"cex",11,0.18,"cex",10,0.55,"--","--","--","cex",11,0.94,"--","--","--","cex",11,0.32,"cex",11,9.69,"--","--","--"]
["invalid","simulation","car_5_e3_11","cex",11,0.1,"cex",11,0.19,"cex",10,0.55,"--","--","--","cex",11,0.97,"--","--","--","cex",11,0.29,"cex",11,8.41,"--","--","--"]
["invalid","simulation","car_5_e3_11_e1_429","cex",11,0.1,"cex",11,0.19,"cex",10,0.51,"--","--","--","cex",11,0.99,"--","--","--","cex",11,0.28,"cex",11,7.69,"--","--","--"]
["invalid","simulation","car_5_e3_11_e5_24","cex",11,0.11,"cex",11,0.19,"cex",10,0.56,"--","--","--","cex",11,1.02,"--","--","--","cex",11,0.28,"cex",11,7.97,"--","--","--"]
["invalid","simulation","car_5_e3_11_e7_693","cex",11,0.13,"cex",11,0.21,"cex",10,0.54,"--","--","--","cex",11,1.04,"--","--","--","cex",11,0.32,"cex",11,10.78,"--","--","--"]
["invalid","simulation","car_5_e3_661","cex",11,0.1,"cex",11,0.19,"cex",10,0.56,"--","--","--","cex",11,0.97,"--","--","--","cex",11,0.29,"cex",11,8.38,"--","--","--"]
["invalid","simulation","car_5_e7_244_e2_693","cex",11,0.09,"cex",11,0.19,"cex",10,0.5,"--","--","--","cex",11,0.94,"--","--","--","cex",11,0.28,"cex",11,5.58,"--","--","--"]
["invalid","simulation","car_5_e7_244_e3_1071","cex",11,0.13,"cex",11,0.19,"cex",10,0.54,"--","--","--","cex",11,0.97,"--","--","--","cex",11,0.32,"cex",11,10.69,"--","--","--"]
["invalid","simulation","car_6_e2_589_e2_506","cex",12,0.06,"cex",12,0.15,"cex",11,0.56,"--","--","--","cex",12,1,"--","--","--","cex",12,0.48,"cex",12,1.79,"--","--","--"]
["invalid","simulation","car_6_e2_589_e3_349","cex",12,0.07,"cex",12,0.14,"cex",11,0.51,"--","--","--","cex",12,0.91,"--","--","--","cex",12,0.3,"cex",12,4.86,"--","--","--"]
["invalid","simulation","car_6_e2_893","cex",12,0.07,"cex",12,0.14,"cex",11,0.56,"--","--","--","cex",12,0.92,"--","--","--","cex",12,0.25,"cex",12,6.39,"--","--","--"]
["invalid","simulation","car_6_e3_294_e1_956","cex",12,0.08,"cex",12,0.15,"cex",11,0.58,"--","--","--","cex",12,0.93,"--","--","--","cex",12,0.3,"cex",12,5.59,"--","--","--"]
["invalid","simulation","car_6_e3_294_e3_47","cex",12,0.07,"cex",12,0.14,"cex",11,0.55,"--","--","--","cex",12,1.05,"--","--","--","cex",12,0.29,"cex",12,10.45,"--","--","--"]
["invalid","simulation","car_6_e3_294_e5_979","cex",12,0.07,"cex",12,0.14,"cex",11,0.52,"--","--","--","cex",12,0.93,"--","--","--","cex",12,0.25,"cex",12,6.06,"--","--","--"]
["invalid","simulation","car_all_e1_388","cex",3,0.02,"cex",3,0.06,"cex",2,0.25,"--","--","--","cex",3,0.07,"--","--","--","cex",3,0.09,"cex",3,0.12,"--","--","--"]
["invalid","simulation","car_all_e1_618","cex",3,0.02,"cex",3,0.06,"cex",2,0.25,"--","--","--","cex",3,0.07,"--","--","--","cex",3,0.09,"cex",3,0.09,"--","--","--"]
["invalid","simulation","car_all_e1_618_e3_303","cex",3,0.02,"cex",3,0.06,"cex",2,0.25,"--","--","--","cex",3,0.07,"--","--","--","cex",3,0.08,"cex",3,0.06,"--","--","--"]
["invalid","simulation","car_all_e3_1068","cex",2,0.01,"cex",2,0.05,"cex",1,0.23,"--","--","--","cex",2,0.06,"--","--","--","cex",2,0.07,"cex",2,0.04,"--","--","--"]
["invalid","simulation","car_all_e3_1068_e1_178","cex",2,0.01,"cex",2,0.04,"cex",1,0.23,"--","--","--","cex",2,0.06,"--","--","--","cex",2,0.07,"cex",2,0.05,"--","--","--"]
["invalid","simulation","car_all_e3_1068_e2_13","cex",2,0.03,"cex",2,0.05,"cex",1,0.23,"--","--","--","cex",2,0.06,"--","--","--","cex",2,0.07,"cex",2,0.04,"--","--","--"]
["invalid","simulation","car_all_e3_1068_e3_163","cex",2,0.01,"cex",2,0.05,"cex",1,0.22,"--","--","--","cex",2,0.06,"--","--","--","cex",2,0.07,"cex",2,0.06,"--","--","--"]
["invalid","simulation","car_all_e3_1068_e5_882","cex",2,0.01,"cex",2,0.05,"cex",1,0.24,"--","--","--","cex",2,0.06,"--","--","--","cex",2,0.07,"cex",2,0.04,"--","--","--"]
["invalid","simulation","car_all_e8_856_e1_217","cex",3,0.02,"cex",3,0.07,"cex",2,0.26,"--","--","--","cex",3,0.08,"--","--","--","cex",3,0.08,"cex",3,0.09,"--","--","--"]
["invalid","simulation","car_all_e8_856_e3_180","cex",2,0.01,"cex",2,0.05,"cex",1,0.22,"--","--","--","cex",2,0.06,"--","--","--","cex",2,0.07,"cex",2,0.04,"--","--","--"]
["invalid","large","ccp10","cex",3,0.2,"cex",3,1.51,"cex",2,0.57,"--","--","--","cex",3,1.53,"--","--","--","err:error",0,900,"err:error",0,900,"--","--","--"]
["invalid","large","ccp11","cex",22,124.73,"cex",22,104.35,"cex",21,272,"--","--","--","timeout",9,900,"--","--","--","err:error",0,900,"err:error",0,900,"--","--","--"]
["invalid","large","ccp12","cex",4,0.33,"cex",4,1.45,"cex",3,0.76,"--","--","--","cex",4,3.6,"--","--","--","err:error",0,900,"err:error",0,900,"--","--","--"]
["invalid","large","ccp13","cex",22,61.56,"cex",22,57.81,"cex",21,77.04,"--","--","--","timeout",12,900,"--","--","--","err:error",0,900,"err:error",0,900,"--","--","--"]
["invalid","large","ccp14","cex",20,47.71,"cex",20,43.9,"cex",19,59.85,"--","--","--","timeout",12,900,"--","--","--","err:error",0,900,"err:error",0,900,"--","--","--"]
["invalid","large","ccp21","cex",4,0.28,"cex",4,1.15,"cex",3,0.73,"--","--","--","cex",4,3.32,"--","--","--","err:error",0,900,"err:error",0,900,"--","--","--"]
["invalid","large","ccp22","cex",23,80.21,"cex",23,79.09,"cex",22,86.42,"--","--","--","timeout",9,900,"--","--","--","err:error",0,900,"err:error",0,900,"--","--","--"]
["invalid","large","ccp23","cex",21,49.48,"cex",21,52.36,"cex",20,63.81,"--","--","--","timeout",12,900,"--","--","--","err:error",0,900,"err:error",0,900,"--","--","--"]
["invalid","large","ccp24","cex",22,190.97,"cex",22,178.38,"cex",21,305.41,"--","--","--","timeout",9,900,"--","--","--","err:error",0,900,"err:error",0,900,"--","--","--"]
["invalid","simulation","cd_e7_621","cex",10,0.04,"cex",10,0.13,"cex",9,0.43,"--","--","--","cex",10,0.82,"--","--","--","cex",10,0.23,"cex",10,3.05,"--","--","--"]
["invalid","simulation","cd_e7_621_e7_669","cex",10,0.04,"cex",10,0.13,"cex",9,0.43,"--","--","--","cex",10,0.93,"--","--","--","cex",10,0.21,"cex",10,4.23,"--","--","--"]
["invalid","simulation","cd_e7_8","cex",10,0.04,"cex",10,0.14,"cex",9,0.39,"--","--","--","cex",10,0.76,"--","--","--","cex",10,0.19,"cex",10,3.04,"--","--","--"]
["invalid","large","cruise_controller_08","cex",22,315.51,"cex",22,296.53,"cex",21,397.53,"--","--","--","timeout",18,900,"--","--","--","err:error",0,900,"err:error",0,900,"--","--","--"]
["invalid","large","cruise_controller_09","cex",3,0.16,"cex",3,0.54,"cex",2,0.59,"--","--","--","cex",3,0.59,"--","--","--","err:error",0,900,"err:error",0,900,"--","--","--"]
["invalid","large","cruise_controller_15","cex",4,0.23,"cex",4,0.62,"cex",3,0.76,"--","--","--","cex",4,1.8,"--","--","--","err:error",0,900,"err:error",0,900,"--","--","--"]
["invalid","large","cruise_controller_16","cex",22,111.46,"cex",22,150.74,"cex",21,386.32,"--","--","--","timeout",18,900,"--","--","--","err:error",0,900,"err:error",0,900,"--","--","--"]
["invalid","large","cruise_controller_17","cex",4,0.29,"cex",4,0.81,"cex",3,0.82,"--","--","--","cex",4,2.16,"--","--","--","err:error",0,900,"err:error",0,900,"--","--","--"]
["invalid","large","cruise_controller_20","cex",4,0.19,"cex",4,0.77,"cex",3,0.77,"--","--","--","cex",4,1.99,"--","--","--","err:error",0,900,"err:error",0,900,"--","--","--"]
["invalid","large","cruise_controller_21","cex",2,0.1,"cex",2,0.43,"cex",0,0.41,"--","--","--","cex",2,0.47,"--","--","--","err:error",0,900,"err:error",0,900,"--","--","--"]
["invalid","large","cruise_controller_22","cex",4,0.18,"cex",4,0.66,"cex",3,0.76,"--","--","--","cex",4,1.77,"--","--","--","err:error",0,900,"err:error",0,900,"--","--","--"]
["invalid","large","cruise_controller_23","cex",22,304.52,"cex",22,266.85,"cex",21,419.59,"--","--","--","timeout",18,900,"--","--","--","err:error",0,900,"err:error",0,900,"--","--","--"]
["invalid","memory1","DRAGON_10_e1_3587_e7_872","cex",2,0.03,"cex",2,0.08,"cex",1,0.34,"--","--","--","cex",2,0.11,"--","--","--","cex",2,0.25,"cex",2,1.06,"--","--","--"]
["invalid","memory1","DRAGON_10_e2_2785_e7_1466","cex",2,0.03,"cex",2,0.08,"cex",1,0.34,"--","--","--","cex",2,0.09,"--","--","--","cex",2,0.25,"cex",2,0.86,"--","--","--"]
["invalid","memory1","DRAGON_10_e3_144_e7_523","cex",2,0.04,"cex",2,0.08,"cex",1,0.33,"--","--","--","cex",2,0.09,"--","--","--","cex",2,0.25,"cex",2,1.29,"--","--","--"]
["invalid","memory1","DRAGON_10_e7_3861_e2_1020","cex",2,0.03,"cex",2,0.08,"cex",1,0.33,"--","--","--","cex",2,0.09,"--","--","--","cex",2,0.29,"cex",2,0.84,"--","--","--"]
["invalid","memory1","DRAGON_10_e7_3861_e7_2180","cex",2,0.05,"cex",2,0.1,"cex",1,0.33,"--","--","--","cex",2,0.11,"--","--","--","cex",2,0.33,"cex",2,0.31,"--","--","--"]
["invalid","memory1","DRAGON_11_e1_1117_e7_4950","cex",2,0.06,"cex",2,0.06,"cex",1,0.34,"--","--","--","cex",2,0.07,"--","--","--","cex",2,0.29,"cex",2,0.58,"--","--","--"]
["invalid","memory1","DRAGON_11_e1_2450_e7_5791","cex",2,0.04,"cex",2,0.06,"cex",1,0.32,"--","--","--","cex",2,0.07,"--","--","--","cex",2,0.27,"cex",2,0.56,"--","--","--"]
["invalid","memory1","DRAGON_12_e1_4640_e7_128","cex",2,0.04,"cex",2,0.06,"cex",1,0.34,"--","--","--","cex",2,0.07,"--","--","--","cex",2,0.29,"cex",2,0.81,"--","--","--"]
["invalid","memory1","DRAGON_12_e2_1618_e7_4732","cex",2,0.04,"cex",2,0.05,"cex",1,0.33,"--","--","--","cex",2,0.08,"--","--","--","cex",2,0.27,"cex",2,0.74,"--","--","--"]
["invalid","memory1","DRAGON_13_e7_2336","cex",2,0.05,"cex",2,0.06,"cex",1,0.33,"--","--","--","cex",2,0.07,"--","--","--","cex",2,0.3,"cex",2,1.83,"--","--","--"]
["invalid","memory1","DRAGON_13_e7_2336_e1_541","cex",2,0.04,"cex",2,0.06,"cex",1,0.35,"--","--","--","cex",2,0.07,"--","--","--","cex",2,0.29,"cex",2,0.97,"--","--","--"]
["invalid","memory1","DRAGON_13_e7_2336_e2_1255","cex",2,0.04,"cex",2,0.06,"cex",1,0.34,"--","--","--","cex",2,0.07,"--","--","--","cex",2,0.27,"cex",2,1.17,"--","--","--"]
["invalid","memory1","DRAGON_13_e7_2336_e3_3117","cex",2,0.04,"cex",2,0.06,"cex",1,0.33,"--","--","--","cex",2,0.07,"--","--","--","cex",2,0.31,"cex",2,1.35,"--","--","--"]
["invalid","memory1","DRAGON_13_e7_2336_e7_685","cex",2,0.05,"cex",2,0.06,"cex",1,0.34,"--","--","--","cex",2,0.07,"--","--","--","cex",2,0.3,"cex",2,0.35,"--","--","--"]
["invalid","memory1","DRAGON_14_e2_3606_e7_4891","cex",4,0.1,"cex",4,0.25,"cex",3,0.45,"--","--","--","cex",4,0.79,"--","--","--","cex",4,1.24,"cex",4,32.71,"--","--","--"]
["invalid","memory1","DRAGON_14_e7_3162","cex",4,0.1,"cex",4,0.18,"cex",3,0.46,"--","--","--","cex",4,0.71,"--","--","--","cex",4,0.78,"cex",4,29.95,"--","--","--"]
["invalid","memory1","DRAGON_14_e7_3162_e1_3998","cex",4,0.1,"cex",4,0.27,"cex",3,0.47,"--","--","--","cex",4,0.93,"--","--","--","cex",4,1.44,"cex",4,25.53,"--","--","--"]
["invalid","memory1","DRAGON_14_e7_3162_e2_753","cex",4,0.1,"cex",4,0.26,"cex",3,0.47,"--","--","--","cex",4,0.79,"--","--","--","cex",4,1.3,"cex",4,32.67,"--","--","--"]
["invalid","memory1","DRAGON_14_e7_3162_e3_4298","cex",4,0.1,"cex",4,0.26,"cex",3,0.45,"--","--","--","cex",4,0.92,"--","--","--","cex",4,1,"cex",4,29.69,"--","--","--"]
["invalid","memory1","DRAGON_14_e7_3162_e7_3528","cex",4,0.1,"cex",4,0.24,"cex",3,0.46,"--","--","--","cex",4,0.85,"--","--","--","cex",4,1.6,"cex",4,30.91,"--","--","--"]
["invalid","memory1","DRAGON_2_e7_25","cex",2,0.05,"cex",2,0.13,"cex",1,0.34,"--","--","--","cex",2,0.14,"--","--","--","cex",2,0.33,"cex",2,3.03,"--","--","--"]
["invalid","memory1","DRAGON_2_e7_25_e1_154","cex",2,0.04,"cex",2,0.12,"cex",1,0.34,"--","--","--","cex",2,0.14,"--","--","--","cex",2,0.29,"cex",2,3.22,"--","--","--"]
["invalid","memory1","DRAGON_2_e7_25_e2_5340","cex",2,0.04,"cex",2,0.12,"cex",1,0.34,"--","--","--","cex",2,0.13,"--","--","--","cex",2,0.37,"cex",2,3.6,"--","--","--"]
["invalid","memory1","DRAGON_2_e7_25_e3_829","cex",2,0.04,"cex",2,0.12,"cex",1,0.33,"--","--","--","cex",2,0.14,"--","--","--","cex",2,0.29,"cex",2,3.21,"--","--","--"]
["invalid","memory1","DRAGON_2_e7_25_e7_4469","cex",2,0.04,"cex",2,0.12,"cex",1,0.34,"--","--","--","cex",2,0.13,"--","--","--","cex",2,0.33,"cex",2,2.59,"--","--","--"]
["invalid","memory1","DRAGON_3_e1_4783_e7_4070","cex",2,0.04,"cex",2,0.12,"cex",1,0.34,"--","--","--","cex",2,0.14,"--","--","--","cex",2,0.28,"cex",2,3.79,"--","--","--"]
["invalid","memory1","DRAGON_3_e7_3211","cex",2,0.04,"cex",2,0.12,"cex",1,0.32,"--","--","--","cex",2,0.14,"--","--","--","cex",2,0.3,"cex",2,3.29,"--","--","--"]
["invalid","memory1","DRAGON_3_e7_4884","cex",2,0.06,"cex",2,0.12,"cex",1,0.34,"--","--","--","cex",2,0.15,"--","--","--","cex",2,0.34,"cex",2,3.26,"--","--","--"]
["invalid","memory1","DRAGON_4_e2_2799_e7_2499","cex",3,0.07,"cex",3,0.18,"cex",2,0.39,"--","--","--","cex",3,0.2,"--","--","--","cex",3,0.57,"cex",3,6.08,"--","--","--"]
["invalid","memory1","DRAGON_4_e7_2077","cex",3,0.05,"cex",3,0.16,"cex",2,0.38,"--","--","--","cex",3,0.19,"--","--","--","cex",3,0.36,"cex",3,4.67,"--","--","--"]
["invalid","memory1","DRAGON_4_e7_2329","cex",3,0.05,"cex",3,0.16,"cex",2,0.38,"--","--","--","cex",3,0.22,"--","--","--","cex",3,0.4,"cex",3,4.65,"--","--","--"]
["invalid","memory1","DRAGON_4_e7_2329_e3_4574","cex",3,0.07,"cex",3,0.17,"cex",2,0.38,"--","--","--","cex",3,0.2,"--","--","--","cex",3,0.4,"cex",3,6.81,"--","--","--"]
["invalid","memory1","DRAGON_4_e7_2329_e7_3856","cex",3,0.06,"cex",3,0.31,"cex",2,0.38,"--","--","--","cex",3,0.19,"--","--","--","cex",3,0.36,"cex",3,7.81,"--","--","--"]
["invalid","memory1","DRAGON_5_e2_3018_e7_2443","cex",3,0.06,"cex",3,0.16,"cex",2,0.38,"--","--","--","cex",3,0.17,"--","--","--","cex",3,0.52,"cex",3,10.93,"--","--","--"]
["invalid","memory1","DRAGON_5_e3_1503_e7_1879","cex",3,0.06,"cex",3,0.17,"cex",2,0.37,"--","--","--","cex",3,0.2,"--","--","--","cex",3,0.36,"cex",3,13.88,"--","--","--"]
["invalid","memory1","DRAGON_5_e7_2017","cex",3,0.05,"cex",3,0.17,"cex",2,0.38,"--","--","--","cex",3,0.21,"--","--","--","cex",3,0.39,"cex",3,9.92,"--","--","--"]
["invalid","memory1","DRAGON_5_e7_2017_e1_5832","cex",3,0.05,"cex",3,0.18,"cex",2,0.38,"--","--","--","cex",3,0.2,"--","--","--","cex",3,0.42,"cex",3,8.68,"--","--","--"]
["invalid","memory1","DRAGON_5_e7_2017_e2_664","cex",3,0.08,"cex",3,0.17,"cex",2,0.38,"--","--","--","cex",3,0.17,"--","--","--","cex",3,0.48,"cex",3,10.91,"--","--","--"]
["invalid","memory1","DRAGON_5_e7_2017_e3_1763","cex",3,0.06,"cex",3,0.17,"cex",2,0.37,"--","--","--","cex",3,0.2,"--","--","--","cex",3,0.4,"cex",3,15,"--","--","--"]
["invalid","memory1","DRAGON_5_e7_2017_e7_2326","cex",3,0.08,"cex",3,0.14,"cex",2,0.38,"--","--","--","cex",3,0.19,"--","--","--","cex",3,0.37,"cex",3,9.8,"--","--","--"]
["invalid","memory1","DRAGON_all_e1_4022_e7_2886","cex",2,0.04,"cex",2,0.16,"cex",1,0.34,"--","--","--","cex",2,0.17,"--","--","--","cex",2,0.35,"cex",2,4.56,"--","--","--"]
["invalid","memory1","DRAGON_all_e2_6104_e7_5856","cex",2,0.04,"cex",2,0.16,"cex",1,0.34,"--","--","--","cex",2,0.17,"--","--","--","cex",2,0.35,"cex",2,7.29,"--","--","--"]
["invalid","memory1","DRAGON_all_e7_1941_e2_6086","cex",2,0.07,"cex",2,0.17,"cex",1,0.35,"--","--","--","cex",2,0.17,"--","--","--","cex",2,0.35,"cex",2,7.25,"--","--","--"]
["invalid","memory1","DRAGON_all_e7_4065","cex",2,0.04,"cex",2,0.16,"cex",1,0.34,"--","--","--","cex",2,0.18,"--","--","--","cex",2,0.32,"cex",2,6.87,"--","--","--"]
["invalid","memory1","DRAGON_all2_e1_2636_e7_4699","cex",2,0.05,"cex",2,0.41,"cex",1,0.35,"--","--","--","cex",2,0.45,"--","--","--","cex",2,0.5,"cex",2,3.06,"--","--","--"]
["invalid","memory1","DRAGON_all2_e1_2636_e8_5957","cex",2,0.05,"cex",2,0.45,"cex",1,0.35,"--","--","--","cex",2,0.44,"--","--","--","cex",2,0.96,"cex",2,5.36,"--","--","--"]
["invalid","memory1","DRAGON_all2_e2_2073_e7_1864","cex",2,0.05,"cex",2,0.41,"cex",1,0.36,"--","--","--","cex",2,0.43,"--","--","--","cex",2,0.46,"cex",2,3.12,"--","--","--"]
["invalid","memory1","DRAGON_all2_e2_2073_e8_3691","cex",2,0.05,"cex",2,0.41,"cex",1,0.35,"--","--","--","cex",2,0.44,"--","--","--","cex",2,0.95,"cex",2,5.97,"--","--","--"]
["invalid","memory1","DRAGON_all2_e3_4612_e7_2291","cex",2,0.05,"cex",2,0.42,"cex",1,0.35,"--","--","--","cex",2,0.44,"--","--","--","cex",2,3.73,"cex",2,3.16,"--","--","--"]
["invalid","memory1","DRAGON_all2_e3_4612_e8_5861","cex",2,0.05,"cex",2,0.45,"cex",1,0.35,"--","--","--","cex",2,0.44,"--","--","--","cex",2,3.01,"cex",2,8.57,"--","--","--"]
["invalid","memory1","DRAGON_all2_e7_5322","cex",2,0.05,"cex",2,0.41,"cex",1,0.34,"--","--","--","cex",2,0.44,"--","--","--","cex",2,3.11,"cex",2,3.17,"--","--","--"]
["invalid","memory1","DRAGON_all2_e7_5406","cex",2,0.05,"cex",2,0.41,"cex",1,0.35,"--","--","--","cex",2,0.48,"--","--","--","cex",2,3.03,"cex",2,3.14,"--","--","--"]
["invalid","memory1","DRAGON_all2_e7_5406_e1_6690","cex",2,0.05,"cex",2,0.41,"cex",1,0.35,"--","--","--","cex",2,0.44,"--","--","--","cex",2,0.46,"cex",2,3.05,"--","--","--"]
["invalid","memory1","DRAGON_all2_e7_5406_e2_3084","cex",2,0.05,"cex",2,0.44,"cex",1,0.34,"--","--","--","cex",2,0.44,"--","--","--","cex",2,0.5,"cex",2,3.09,"--","--","--"]
["invalid","memory1","DRAGON_all2_e7_5406_e3_506","cex",2,0.05,"cex",2,0.42,"cex",1,0.35,"--","--","--","cex",2,0.44,"--","--","--","cex",2,3.74,"cex",2,3.08,"--","--","--"]
["invalid","memory1","DRAGON_all2_e7_5406_e7_6697","cex",2,0.06,"cex",2,0.36,"cex",1,0.35,"--","--","--","cex",2,0.55,"--","--","--","cex",2,3.11,"cex",2,5.83,"--","--","--"]
["invalid","memory1","DRAGON_all2_e8_4626","cex",2,0.05,"cex",2,0.41,"cex",1,0.35,"--","--","--","cex",2,0.46,"--","--","--","cex",2,3.73,"cex",2,8.6,"--","--","--"]
["invalid","memory1","DRAGON_all2_e8_5504","cex",2,0.05,"cex",2,0.42,"cex",1,0.35,"--","--","--","cex",2,0.45,"--","--","--","cex",2,3.82,"cex",2,8.59,"--","--","--"]
["invalid","memory1","DRAGON_all2_e8_5504_e1_4719","cex",2,0.05,"cex",2,0.45,"cex",1,0.36,"--","--","--","cex",2,0.44,"--","--","--","cex",2,0.96,"cex",2,5.28,"--","--","--"]
["invalid","memory1","DRAGON_all2_e8_5504_e2_1598","cex",2,0.05,"cex",2,0.41,"cex",1,0.35,"--","--","--","cex",2,0.44,"--","--","--","cex",2,0.91,"cex",2,5.91,"--","--","--"]
["invalid","memory1","DRAGON_all2_e8_5504_e7_579","cex",2,0.05,"cex",2,0.42,"cex",1,0.34,"--","--","--","cex",2,0.5,"--","--","--","cex",2,3.05,"cex",2,3.3,"--","--","--"]
["invalid","misc","durationThm_1_e1_197","cex",2,0.01,"cex",2,0.04,"cex",1,0.23,"--","--","--","cex",2,0.05,"--","--","--","cex",2,0.08,"cex",2,0.02,"--","--","--"]
["invalid","misc","durationThm_1_e1_197_e7_289","cex",2,0.01,"cex",2,0.06,"cex",1,0.23,"--","--","--","cex",2,0.07,"--","--","--","cex",2,0.08,"cex",2,0.06,"--","--","--"]
["invalid","misc","durationThm_1_e1_350","cex",2,0.01,"cex",2,0.04,"cex",1,0.23,"--","--","--","cex",2,0.05,"--","--","--","cex",2,0.07,"cex",2,0.03,"--","--","--"]
["invalid","misc","durationThm_1_e7_12","cex",3,0.02,"cex",3,0.07,"cex",2,0.25,"--","--","--","cex",3,0.12,"--","--","--","cex",2,0.07,"cex",3,0.1,"--","--","--"]
["invalid","misc","durationThm_1_e7_217","cex",3,0.01,"cex",3,0.08,"cex",2,0.25,"--","--","--","cex",3,0.1,"--","--","--","cex",2,0.07,"cex",3,0.06,"--","--","--"]
["invalid","misc","durationThm_1_e7_217_e1_89","cex",2,0.01,"cex",2,0.06,"cex",1,0.23,"--","--","--","cex",2,0.07,"--","--","--","cex",2,0.06,"cex",2,0.02,"--","--","--"]
["invalid","misc","durationThm_1_e7_217_e7_31","cex",2,0.01,"cex",2,0.06,"cex",1,0.23,"--","--","--","cex",2,0.07,"--","--","--","cex",2,0.04,"cex",2,0.03,"--","--","--"]
["invalid","misc","durationThm_2_e1_301_e7_64","cex",2,0.01,"cex",2,0.05,"cex",1,0.23,"--","--","--","cex",2,0.06,"--","--","--","cex",2,0.03,"cex",2,0.02,"--","--","--"]
["invalid","misc","durationThm_2_e7_145","cex",2,0.01,"cex",2,0.06,"cex",1,0.23,"--","--","--","cex",2,0.06,"--","--","--","cex",2,0.06,"cex",2,0.02,"--","--","--"]
["invalid","misc","durationThm_2_e7_145_e1_343","cex",2,0.01,"cex",2,0.05,"cex",1,0.23,"--","--","--","cex",2,0.06,"--","--","--","cex",2,0.07,"cex",2,0.04,"--","--","--"]
["invalid","misc","durationThm_2_e7_145_e7_154","cex",2,0.01,"cex",2,0.05,"cex",1,0.23,"--","--","--","cex",2,0.06,"--","--","--","cex",2,0.06,"cex",2,0.04,"--","--","--"]
["invalid","misc","durationThm_2_e7_149","cex",2,0.01,"cex",2,0.05,"cex",1,0.27,"--","--","--","cex",2,0.09,"--","--","--","cex",2,0.06,"cex",2,0.04,"--","--","--"]
["invalid","misc","durationThm_3_e1_36","cex",3,0.01,"cex",3,0.05,"cex",2,0.24,"--","--","--","cex",3,0.06,"--","--","--","cex",1,0.04,"cex",3,0.05,"--","--","--"]
["invalid","misc","durationThm_3_e1_36_e7_432","cex",3,0.02,"cex",3,0.05,"cex",2,0.25,"--","--","--","cex",3,0.06,"--","--","--","cex",1,0.06,"cex",3,0.09,"--","--","--"]
["invalid","misc","durationThm_3_e1_71","cex",3,0.01,"cex",3,0.04,"cex",2,0.25,"--","--","--","cex",3,0.05,"--","--","--","cex",1,0.06,"cex",3,0.06,"--","--","--"]
["invalid","misc","durationThm_3_e7_201","cex",4,0.02,"cex",4,0.06,"cex",3,0.27,"--","--","--","cex",4,0.16,"--","--","--","cex",1,0.05,"cex",4,0.11,"--","--","--"]
["invalid","misc","durationThm_3_e7_334","cex",4,0.02,"cex",4,0.07,"cex",3,0.25,"--","--","--","cex",4,0.15,"--","--","--","cex",1,0.05,"cex",4,0.11,"--","--","--"]
["invalid","misc","durationThm_3_e7_334_e1_431","cex",3,0.02,"cex",3,0.05,"cex",2,0.25,"--","--","--","cex",3,0.06,"--","--","--","cex",1,0.05,"cex",3,0.09,"--","--","--"]
["invalid","misc","durationThm_3_e7_334_e7_118","cex",2,0.01,"cex",2,0.04,"cex",0,0.22,"--","--","--","cex",2,0.05,"--","--","--","cex",1,0.05,"cex",1,0.05,"--","--","--"]
["invalid","misc","ex8","cex",2,0.01,"cex",2,0.02,"cex",1,0.22,"--","--","--","cex",2,0.03,"--","--","--","cex",2,0.05,"cex",2,0.05,"--","--","--"]
["invalid","misc","ex8_e7_55","cex",2,0.01,"cex",2,0.02,"cex",1,0.23,"--","--","--","cex",2,0.03,"--","--","--","cex",2,0.05,"cex",2,0.03,"--","--","--"]
["invalid","misc","ex8_e7_74","cex",2,0.04,"cex",2,0.02,"cex",1,0.23,"--","--","--","cex",2,0.03,"--","--","--","cex",2,0.05,"cex",2,0.03,"--","--","--"]
["invalid","misc","ex8_e7_74_e7_740","cex",2,0.01,"cex",2,0.02,"cex",1,0.23,"--","--","--","cex",2,0.03,"--","--","--","cex",2,0.05,"cex",2,0.02,"--","--","--"]
["invalid","misc","ex8_e7_74_e8_302","cex",2,0.01,"cex",2,0.02,"cex",1,0.22,"--","--","--","cex",2,0.03,"--","--","--","cex",2,0.02,"cex",2,0.05,"--","--","--"]
["invalid","misc","ex8_e8_220","cex",2,0.01,"cex",2,0.02,"cex",1,0.23,"--","--","--","cex",2,0.03,"--","--","--","cex",2,0.05,"cex",2,0.03,"--","--","--"]
["invalid","misc","ex8_e8_220_e7_249","cex",2,0.01,"cex",2,0.02,"cex",1,0.22,"--","--","--","cex",2,0.03,"--","--","--","cex",2,0.04,"cex",2,0.02,"--","--","--"]
["invalid","misc","ex8_e8_376","cex",2,0.01,"cex",2,0.02,"cex",1,0.23,"--","--","--","cex",2,0.03,"--","--","--","cex",2,0.02,"cex",2,0.01,"--","--","--"]
["invalid","simulation","fast_1_e7_1035","cex",3,0.02,"cex",3,0.1,"cex",1,0.24,"--","--","--","cex",3,0.12,"--","--","--","cex",2,0.06,"cex",2,0.06,"--","--","--"]
["invalid","simulation","fast_1_e7_2044","cex",3,0.02,"cex",3,0.1,"cex",1,0.24,"--","--","--","cex",3,0.11,"--","--","--","cex",2,0.04,"cex",2,0.02,"--","--","--"]
["invalid","simulation","fast_1_e7_2044_e7_1287","cex",3,0.03,"cex",3,0.1,"cex",1,0.23,"--","--","--","cex",3,0.12,"--","--","--","cex",2,0.06,"cex",2,0.06,"--","--","--"]
["invalid","simulation","fast_1_e8_747_e7_692","cex",3,0.02,"cex",3,0.1,"cex",1,0.24,"--","--","--","cex",3,0.11,"--","--","--","cex",2,0.06,"cex",2,0.03,"--","--","--"]
["invalid","simulation","fast_2_e7_1871","cex",3,0.03,"cex",3,0.46,"cex",1,0.24,"--","--","--","cex",3,0.47,"--","--","--","cex",2,0.07,"cex",2,0.05,"--","--","--"]
["invalid","simulation","fast_2_e7_2526","cex",3,0.03,"cex",3,0.45,"cex",1,0.24,"--","--","--","cex",3,0.51,"--","--","--","cex",2,0.07,"cex",2,0.04,"--","--","--"]
["invalid","simulation","fast_2_e7_2526_e7_2736","cex",3,0.03,"cex",3,0.5,"cex",1,0.25,"--","--","--","cex",3,0.48,"--","--","--","cex",2,0.07,"cex",2,0.06,"--","--","--"]
["invalid","simulation","fast_2_e8_460_e7_43","cex",3,0.03,"cex",3,0.42,"cex",1,0.24,"--","--","--","cex",3,0.44,"--","--","--","cex",2,0.07,"cex",2,0.03,"--","--","--"]
["invalid","memory1","FIREFLY_1_e1_1092","cex",3,0.03,"cex",3,0.11,"cex",2,0.33,"--","--","--","cex",3,0.13,"--","--","--","cex",3,12.28,"cex",3,3.54,"--","--","--"]
["invalid","memory1","FIREFLY_1_e1_1092_e1_1486","cex",3,0.03,"cex",3,0.11,"cex",2,0.32,"--","--","--","cex",3,0.15,"--","--","--","cex",3,0.53,"cex",3,3.44,"--","--","--"]
["invalid","memory1","FIREFLY_1_e1_1092_e3_389","cex",3,0.03,"cex",3,0.11,"cex",2,0.3,"--","--","--","cex",3,0.13,"--","--","--","cex",3,8.38,"cex",3,3.21,"--","--","--"]
["invalid","memory1","FIREFLY_1_e1_1092_e7_1119","cex",2,0.03,"cex",2,0.09,"cex",1,0.29,"--","--","--","cex",2,0.1,"--","--","--","cex",2,0.25,"cex",2,1.39,"--","--","--"]
["invalid","memory1","FIREFLY_2_e1_3099","cex",3,0.04,"cex",3,0.12,"cex",2,0.32,"--","--","--","cex",3,0.15,"--","--","--","cex",3,0.4,"cex",3,4.47,"--","--","--"]
["invalid","memory1","FIREFLY_2_e1_3099_e1_3277","cex",3,0.04,"cex",3,0.12,"cex",2,0.31,"--","--","--","cex",3,0.14,"--","--","--","cex",3,33.61,"cex",3,3.72,"--","--","--"]
["invalid","memory1","FIREFLY_2_e1_3099_e3_2660","cex",3,0.04,"cex",3,0.12,"cex",2,0.32,"--","--","--","cex",3,0.14,"--","--","--","cex",3,0.4,"cex",3,4.29,"--","--","--"]
["invalid","memory1","FIREFLY_2_e1_3099_e7_1817","cex",2,0.06,"cex",2,0.09,"cex",1,0.28,"--","--","--","cex",2,0.11,"--","--","--","cex",2,0.21,"cex",2,2.41,"--","--","--"]
["invalid","memory1","FIREFLY_2_e2_3244_e3_1305","cex",3,0.06,"cex",3,0.13,"cex",2,0.32,"--","--","--","cex",3,0.14,"--","--","--","cex",3,0.4,"cex",3,4,"--","--","--"]
["invalid","memory1","FIREFLY_2_e3_151_e3_1540","cex",3,0.04,"cex",3,0.12,"cex",2,0.3,"--","--","--","cex",3,0.15,"--","--","--","cex",3,25.64,"cex",3,3.37,"--","--","--"]
["invalid","memory1","FIREFLY_2_e7_1776_e2_3202","cex",2,0.03,"cex",2,0.09,"cex",1,0.28,"--","--","--","cex",2,0.1,"--","--","--","cex",2,0.22,"cex",2,2.45,"--","--","--"]
["invalid","memory1","FIREFLY_3_e2_2236_e3_2657","cex",3,0.04,"cex",3,0.12,"cex",2,0.31,"--","--","--","cex",3,0.14,"--","--","--","cex",3,0.27,"cex",3,0.96,"--","--","--"]
["invalid","memory1","FIREFLY_4_e3_3511_e1_2375","cex",4,0.05,"cex",4,0.14,"cex",3,0.38,"--","--","--","cex",4,0.37,"--","--","--","cex",4,17.81,"cex",4,6.16,"--","--","--"]
["invalid","memory1","FIREFLY_4_e3_3511_e4_1464","cex",4,0.05,"cex",4,0.15,"cex",3,0.4,"--","--","--","cex",4,0.38,"--","--","--","cex",4,67.46,"cex",4,6.15,"--","--","--"]
["invalid","memory1","FIREFLY_4_e3_3511_e7_3568","cex",2,0.03,"cex",2,0.09,"cex",1,0.28,"--","--","--","cex",2,0.11,"--","--","--","cex",2,0.22,"cex",2,1.53,"--","--","--"]
["invalid","memory1","FIREFLY_8_e2_1711_e7_1962","cex",2,0.03,"cex",2,0.04,"cex",1,0.28,"--","--","--","cex",2,0.05,"--","--","--","cex",2,0.2,"cex",2,0.1,"--","--","--"]
["invalid","memory1","FIREFLY_a3_e1_195","cex",3,0.04,"cex",3,0.16,"cex",2,0.32,"--","--","--","cex",3,0.19,"--","--","--","cex",3,0.38,"cex",3,2.43,"--","--","--"]
["invalid","memory1","FIREFLY_a3_e1_3233","cex",3,0.04,"cex",3,0.16,"cex",2,0.32,"--","--","--","cex",3,0.2,"--","--","--","cex",3,0.39,"cex",3,2.38,"--","--","--"]
["invalid","memory1","FIREFLY_a3_e1_3233_e1_3123","cex",3,0.04,"cex",3,0.15,"cex",2,0.33,"--","--","--","cex",3,0.19,"--","--","--","cex",3,0.61,"cex",3,1.81,"--","--","--"]
["invalid","memory1","FIREFLY_a3_e1_3233_e7_906","cex",2,0.03,"cex",2,0.12,"cex",1,0.3,"--","--","--","cex",2,0.14,"--","--","--","cex",2,0.22,"cex",2,0.75,"--","--","--"]
["invalid","memory1","FIREFLY_a3_e2_2086_e7_2614","cex",2,0.06,"cex",2,0.13,"cex",1,0.28,"--","--","--","cex",2,0.14,"--","--","--","cex",2,0.22,"cex",2,0.76,"--","--","--"]
["invalid","memory1","FIREFLY_a3_e3_314_e1_1979","cex",4,0.06,"cex",4,0.18,"cex",3,0.41,"--","--","--","cex",4,0.46,"--","--","--","cex",4,4.88,"cex",4,6.26,"--","--","--"]
["invalid","memory1","FIREFLY_a3_e3_314_e4_897","cex",4,0.06,"cex",4,0.18,"cex",3,0.39,"--","--","--","cex",4,0.49,"--","--","--","cex",4,9.62,"cex",4,6.31,"--","--","--"]
["invalid","memory1","FIREFLY_all_e1_1207","cex",3,0.04,"cex",3,0.14,"cex",2,0.35,"--","--","--","cex",3,0.17,"--","--","--","cex",3,3.52,"cex",3,10.05,"--","--","--"]
["invalid","memory1","FIREFLY_all_e1_1207_e1_1201","cex",3,0.04,"cex",3,0.15,"cex",2,0.34,"--","--","--","cex",3,0.17,"--","--","--","cex",3,0.72,"cex",3,8.49,"--","--","--"]
["invalid","memory1","FIREFLY_all_e1_1207_e3_1928","cex",3,0.04,"cex",3,0.14,"cex",2,0.35,"--","--","--","cex",3,0.17,"--","--","--","cex",3,22.32,"cex",3,9.54,"--","--","--"]
["invalid","memory1","FIREFLY_all_e1_1207_e7_156","cex",2,0.03,"cex",2,0.11,"cex",1,0.27,"--","--","--","cex",2,0.12,"--","--","--","cex",2,0.26,"cex",2,1.41,"--","--","--"]
["invalid","memory1","FIREFLY_all_e1_3406","cex",3,0.04,"cex",3,0.14,"cex",2,0.35,"--","--","--","cex",3,0.17,"--","--","--","cex",3,3.73,"cex",3,10.07,"--","--","--"]
["invalid","memory1","FIREFLY_all_e2_2924","cex",3,0.04,"cex",3,0.14,"cex",2,0.34,"--","--","--","cex",3,0.17,"--","--","--","cex",3,0.36,"cex",3,9.71,"--","--","--"]
["invalid","memory1","FIREFLY_all_e2_2924_e2_1767","cex",3,0.05,"cex",3,0.15,"cex",2,0.35,"--","--","--","cex",3,0.17,"--","--","--","cex",3,0.66,"cex",3,10.84,"--","--","--"]
["invalid","memory1","FIREFLY_all_e2_2924_e3_3946","cex",3,0.04,"cex",3,0.14,"cex",2,0.35,"--","--","--","cex",3,0.17,"--","--","--","timeout",0,900,"cex",3,10.78,"--","--","--"]
["invalid","memory1","FIREFLY_all_e2_2924_e7_3371","cex",2,0.03,"cex",2,0.11,"cex",1,0.29,"--","--","--","cex",2,0.12,"--","--","--","cex",2,0.22,"cex",2,2.62,"--","--","--"]
["invalid","memory1","FIREFLY_all_e2_3678","cex",3,0.04,"cex",3,0.14,"cex",2,0.34,"--","--","--","cex",3,0.17,"--","--","--","cex",3,0.32,"cex",3,9.79,"--","--","--"]
["invalid","memory1","FIREFLY_all_e3_1600","cex",3,0.04,"cex",3,0.15,"cex",2,0.32,"--","--","--","cex",3,0.17,"--","--","--","cex",3,98.53,"cex",3,8.41,"--","--","--"]
["invalid","memory1","FIREFLY_all_e3_1600_e1_667","cex",3,0.04,"cex",3,0.14,"cex",2,0.34,"--","--","--","cex",3,0.16,"--","--","--","cex",3,0.35,"cex",3,8.69,"--","--","--"]
["invalid","memory1","FIREFLY_all_e3_1600_e2_676","cex",3,0.04,"cex",3,0.14,"cex",2,0.34,"--","--","--","cex",3,0.18,"--","--","--","cex",3,51.61,"cex",3,10.46,"--","--","--"]
["invalid","memory1","FIREFLY_all_e3_1600_e3_2055","cex",3,0.04,"cex",3,0.14,"cex",2,0.33,"--","--","--","cex",3,0.17,"--","--","--","cex",3,0.33,"timeout",0,900,"--","--","--"]
["invalid","memory1","FIREFLY_all_e3_1600_e4_2415","cex",3,0.04,"cex",3,0.15,"cex",2,0.34,"--","--","--","cex",3,0.16,"--","--","--","cex",3,15.17,"cex",3,8.63,"--","--","--"]
["invalid","memory1","FIREFLY_all_e3_1600_e5_84","cex",3,0.04,"cex",3,0.14,"cex",2,0.34,"--","--","--","cex",3,0.17,"--","--","--","cex",3,97.73,"cex",3,10.56,"--","--","--"]
["invalid","memory1","FIREFLY_all_e3_1600_e7_1607","cex",2,0.03,"cex",2,0.1,"cex",1,0.29,"--","--","--","cex",2,0.51,"--","--","--","cex",2,0.26,"cex",2,2.49,"--","--","--"]
["invalid","memory1","FIREFLY_all_e3_3496","cex",3,0.04,"cex",3,0.14,"cex",2,0.32,"--","--","--","cex",3,0.16,"--","--","--","cex",3,99,"cex",3,8.35,"--","--","--"]
["invalid","memory1","FIREFLY_all_e7_1909","cex",2,0.03,"cex",2,0.11,"cex",1,0.3,"--","--","--","cex",2,0.12,"--","--","--","cex",2,0.26,"cex",2,2.53,"--","--","--"]
["invalid","memory1","FIREFLY_luke_1a_e2_284_e7_998","cex",4,0.06,"cex",4,0.16,"cex",3,0.36,"--","--","--","cex",4,0.48,"--","--","--","cex",4,0.38,"cex",4,4.94,"--","--","--"]
["invalid","memory1","FIREFLY_luke_1b_e1_1139","cex",3,0.06,"cex",3,0.11,"cex",2,0.32,"--","--","--","cex",3,0.13,"--","--","--","cex",3,3.02,"cex",3,3.54,"--","--","--"]
["invalid","memory1","FIREFLY_luke_1b_e1_1139_e1_1565","cex",3,0.04,"cex",3,0.11,"cex",2,0.31,"--","--","--","cex",3,0.18,"--","--","--","cex",3,3.91,"cex",3,3.33,"--","--","--"]
["invalid","memory1","FIREFLY_luke_1b_e1_1139_e3_1839","cex",3,0.04,"cex",3,0.3,"cex",2,0.31,"--","--","--","cex",3,0.21,"--","--","--","cex",3,15.1,"cex",3,3.86,"--","--","--"]
["invalid","memory1","FIREFLY_luke_1b_e1_1139_e7_616","cex",2,0.03,"cex",2,0.09,"cex",1,0.28,"--","--","--","cex",2,0.1,"--","--","--","cex",2,0.22,"cex",2,1.45,"--","--","--"]
["invalid","memory1","FIREFLY_luke_1b_e1_1691","cex",3,0.04,"cex",3,0.11,"cex",2,0.33,"--","--","--","cex",3,0.14,"--","--","--","cex",3,3.03,"cex",3,3.54,"--","--","--"]
["invalid","memory1","FIREFLY_luke_1b_e2_1192","cex",3,0.04,"cex",3,0.11,"cex",2,0.32,"--","--","--","cex",3,0.13,"--","--","--","cex",3,144.84,"cex",3,3.92,"--","--","--"]
["invalid","memory1","FIREFLY_luke_1b_e2_3049","cex",3,0.04,"cex",3,0.11,"cex",2,0.32,"--","--","--","cex",3,0.13,"--","--","--","cex",3,147.48,"cex",3,3.86,"--","--","--"]
["invalid","memory1","FIREFLY_luke_1b_e2_3049_e2_698","cex",3,0.06,"cex",3,0.12,"cex",2,0.32,"--","--","--","cex",3,0.14,"--","--","--","cex",3,5.46,"cex",3,2.62,"--","--","--"]
["invalid","memory1","FIREFLY_luke_1b_e2_3049_e3_2697","cex",3,0.04,"cex",3,0.11,"cex",2,0.32,"--","--","--","cex",3,0.14,"--","--","--","cex",3,5.44,"cex",3,3.19,"--","--","--"]
["invalid","memory1","FIREFLY_luke_1b_e2_3049_e7_1173","cex",2,0.03,"cex",2,0.09,"cex",1,0.27,"--","--","--","cex",2,0.1,"--","--","--","cex",2,0.23,"cex",2,1.44,"--","--","--"]
["invalid","memory1","FIREFLY_luke_1b_e3_144","cex",3,0.04,"cex",3,0.11,"cex",2,0.32,"--","--","--","cex",3,0.13,"--","--","--","cex",3,361.86,"cex",3,2.04,"--","--","--"]
["invalid","memory1","FIREFLY_luke_1b_e3_671","cex",3,0.04,"cex",3,0.12,"cex",2,0.33,"--","--","--","cex",3,0.13,"--","--","--","cex",3,355.42,"cex",3,2.03,"--","--","--"]
["invalid","memory1","FIREFLY_luke_1b_e3_671_e1_725","cex",3,0.04,"cex",3,0.11,"cex",2,0.3,"--","--","--","cex",3,0.14,"--","--","--","cex",3,7.06,"cex",3,3.18,"--","--","--"]
["invalid","memory1","FIREFLY_luke_1b_e3_671_e2_2131","cex",3,0.04,"cex",3,0.11,"cex",2,0.32,"--","--","--","cex",3,0.16,"--","--","--","cex",3,3.74,"cex",3,3.8,"--","--","--"]
["invalid","memory1","FIREFLY_luke_1b_e3_671_e3_941","cex",3,0.04,"cex",3,0.11,"cex",2,0.32,"--","--","--","cex",3,0.13,"--","--","--","cex",3,79.1,"cex",3,2.03,"--","--","--"]
["invalid","memory1","FIREFLY_luke_1b_e3_671_e4_147","cex",3,0.04,"cex",3,0.12,"cex",2,0.32,"--","--","--","cex",3,0.14,"--","--","--","cex",3,1.92,"cex",3,3.21,"--","--","--"]
["invalid","memory1","FIREFLY_luke_1b_e3_671_e5_1637","cex",3,0.04,"cex",3,0.11,"cex",2,0.3,"--","--","--","cex",3,0.14,"--","--","--","cex",3,14.21,"cex",3,3.77,"--","--","--"]
["invalid","memory1","FIREFLY_luke_1b_e3_671_e7_1882","cex",2,0.03,"cex",2,0.09,"cex",1,0.33,"--","--","--","cex",2,0.12,"--","--","--","cex",2,0.25,"cex",2,1.27,"--","--","--"]
["invalid","memory1","FIREFLY_luke_1b_e7_2574","cex",2,0.03,"cex",2,0.09,"cex",1,0.28,"--","--","--","cex",2,0.11,"--","--","--","cex",2,0.25,"cex",2,1.47,"--","--","--"]
["invalid","memory1","FIREFLY_luke_1b_e7_3191","cex",2,0.05,"cex",2,0.09,"cex",1,0.34,"--","--","--","cex",2,0.1,"--","--","--","cex",2,0.24,"cex",2,1.47,"--","--","--"]
["invalid","memory1","FIREFLY_luke_1b_e7_3191_e1_1303","cex",2,0.03,"cex",2,0.09,"cex",1,0.28,"--","--","--","cex",2,0.1,"--","--","--","cex",2,0.23,"cex",2,1.48,"--","--","--"]
["invalid","memory1","FIREFLY_luke_1b_e7_3191_e2_1864","cex",2,0.03,"cex",2,0.09,"cex",1,0.29,"--","--","--","cex",2,0.1,"--","--","--","cex",2,0.26,"cex",2,1.44,"--","--","--"]
["invalid","memory1","FIREFLY_luke_1b_e7_3191_e3_1250","cex",2,0.03,"cex",2,0.09,"cex",1,0.28,"--","--","--","cex",2,0.1,"--","--","--","cex",2,0.25,"cex",2,1.27,"--","--","--"]
["invalid","memory1","FIREFLY_luke_1b_e7_3191_e7_2146","cex",2,0.03,"cex",2,0.09,"cex",1,0.27,"--","--","--","cex",2,0.1,"--","--","--","cex",2,0.24,"cex",2,1.01,"--","--","--"]
["invalid","memory1","FIREFLY_luke_rt_e1_1269","cex",3,0.04,"cex",3,0.13,"cex",2,0.32,"--","--","--","cex",3,0.14,"--","--","--","cex",3,0.38,"cex",3,4.37,"--","--","--"]
["invalid","memory1","FIREFLY_luke_rt_e1_913","cex",3,0.04,"cex",3,0.12,"cex",2,0.32,"--","--","--","cex",3,0.16,"--","--","--","cex",3,0.4,"cex",3,4.42,"--","--","--"]
["invalid","memory1","FIREFLY_luke_rt_e1_913_e1_1993","cex",3,0.04,"cex",3,0.12,"cex",2,0.31,"--","--","--","cex",3,0.14,"--","--","--","cex",3,33.84,"cex",3,3.75,"--","--","--"]
["invalid","memory1","FIREFLY_luke_rt_e1_913_e3_2128","cex",3,0.04,"cex",3,0.12,"cex",2,0.32,"--","--","--","cex",3,0.14,"--","--","--","cex",3,0.4,"cex",3,4.26,"--","--","--"]
["invalid","memory1","FIREFLY_luke_rt_e1_913_e7_1403","cex",2,0.03,"cex",2,0.09,"cex",1,0.28,"--","--","--","cex",2,0.1,"--","--","--","cex",2,0.21,"cex",2,2.42,"--","--","--"]
["invalid","memory1","FIREFLY_luke_rt_e2_1315","cex",3,0.04,"cex",3,0.12,"cex",2,0.32,"--","--","--","cex",3,0.16,"--","--","--","cex",3,1.08,"cex",3,4.31,"--","--","--"]
["invalid","memory1","FIREFLY_luke_rt_e2_3460","cex",3,0.04,"cex",3,0.12,"cex",2,0.3,"--","--","--","cex",3,0.14,"--","--","--","cex",3,1.08,"cex",3,4.31,"--","--","--"]
["invalid","memory1","FIREFLY_luke_rt_e2_3460_e2_2670","cex",3,0.04,"cex",3,0.12,"cex",2,0.31,"--","--","--","cex",3,0.15,"--","--","--","cex",3,3.02,"cex",3,3.97,"--","--","--"]
["invalid","memory1","FIREFLY_luke_rt_e2_3460_e3_1333","cex",3,0.04,"cex",3,0.13,"cex",2,0.33,"--","--","--","cex",3,0.14,"--","--","--","cex",3,0.4,"cex",3,4,"--","--","--"]
["invalid","memory1","FIREFLY_luke_rt_e2_3460_e7_471","cex",2,0.03,"cex",2,0.09,"cex",1,0.28,"--","--","--","cex",2,0.1,"--","--","--","cex",2,0.18,"cex",2,2.45,"--","--","--"]
["invalid","memory1","FIREFLY_luke_rt_e3_1549","cex",3,0.04,"cex",3,0.12,"cex",2,0.31,"--","--","--","cex",3,0.14,"--","--","--","cex",3,0.98,"cex",3,4.08,"--","--","--"]
["invalid","memory1","FIREFLY_u1_e7_3318","cex",3,0.04,"cex",3,0.12,"cex",2,0.31,"--","--","--","cex",3,0.15,"--","--","--","cex",3,0.26,"cex",3,0.53,"--","--","--"]
["invalid","memory2","ILLINOIS_2_e1_3758","cex",2,0.03,"cex",2,0.07,"cex",1,0.28,"--","--","--","cex",2,0.08,"--","--","--","cex",2,0.28,"cex",2,0.15,"--","--","--"]
["invalid","memory2","ILLINOIS_2_e1_834","cex",2,0.03,"cex",2,0.07,"cex",1,0.28,"--","--","--","cex",2,0.08,"--","--","--","cex",2,0.28,"cex",2,0.13,"--","--","--"]
["invalid","memory2","ILLINOIS_2_e1_834_e1_1895","cex",2,0.02,"cex",2,0.07,"cex",1,0.27,"--","--","--","cex",2,0.08,"--","--","--","cex",2,0.24,"cex",2,0.15,"--","--","--"]
["invalid","memory2","ILLINOIS_2_e1_834_e3_2931","cex",2,0.03,"cex",2,0.07,"cex",1,0.28,"--","--","--","cex",2,0.08,"--","--","--","cex",2,0.3,"cex",2,0.14,"--","--","--"]
["invalid","memory2","ILLINOIS_2_e1_834_e7_3738","cex",2,0.06,"cex",2,0.06,"cex",1,0.3,"--","--","--","cex",2,0.09,"--","--","--","cex",2,0.26,"cex",2,0.13,"--","--","--"]
["invalid","memory2","ILLINOIS_2_e2_2367","cex",2,0.03,"cex",2,0.07,"cex",1,0.28,"--","--","--","cex",2,0.08,"--","--","--","cex",2,0.25,"cex",2,0.13,"--","--","--"]
["invalid","memory2","ILLINOIS_2_e2_2367_e2_1561","cex",2,0.03,"cex",2,0.07,"cex",1,0.27,"--","--","--","cex",2,0.08,"--","--","--","cex",2,0.24,"cex",2,0.15,"--","--","--"]
["invalid","memory2","ILLINOIS_2_e2_2367_e3_1601","cex",2,0.03,"cex",2,0.07,"cex",1,0.28,"--","--","--","cex",2,0.08,"--","--","--","cex",2,0.25,"cex",2,0.13,"--","--","--"]
["invalid","memory2","ILLINOIS_2_e2_2367_e7_2728","cex",2,0.03,"cex",2,0.08,"cex",1,0.29,"--","--","--","cex",2,0.09,"--","--","--","cex",2,0.26,"cex",2,0.09,"--","--","--"]
["invalid","memory2","ILLINOIS_2_e2_876","cex",2,0.03,"cex",2,0.07,"cex",1,0.28,"--","--","--","cex",2,0.08,"--","--","--","cex",2,0.22,"cex",2,0.14,"--","--","--"]
["invalid","memory2","ILLINOIS_3_e3_2581","cex",2,0.03,"cex",2,0.09,"cex",1,0.29,"--","--","--","cex",2,0.1,"--","--","--","cex",2,0.23,"cex",2,1.55,"--","--","--"]
["invalid","memory2","ILLINOIS_3_e3_2581_e1_1130","cex",2,0.03,"cex",2,0.09,"cex",0,0.26,"--","--","--","cex",2,0.1,"--","--","--","cex",1,0.15,"cex",1,0.07,"--","--","--"]
["invalid","memory2","ILLINOIS_3_e3_2581_e2_2545","cex",2,0.03,"cex",2,0.09,"cex",0,0.26,"--","--","--","cex",2,0.1,"--","--","--","cex",1,0.15,"cex",1,0.07,"--","--","--"]
["invalid","memory2","ILLINOIS_3_e3_2581_e3_979","cex",2,0.03,"cex",2,0.08,"cex",1,0.3,"--","--","--","cex",2,0.1,"--","--","--","cex",2,0.23,"cex",2,1.16,"--","--","--"]
["invalid","memory2","ILLINOIS_3_e3_2581_e4_958","cex",2,0.03,"cex",2,0.09,"cex",0,0.25,"--","--","--","cex",2,0.11,"--","--","--","cex",1,0.15,"cex",1,0.08,"--","--","--"]
["invalid","memory2","ILLINOIS_3_e3_2581_e5_4006","cex",2,0.03,"cex",2,0.09,"cex",0,0.26,"--","--","--","cex",2,0.1,"--","--","--","cex",1,0.15,"cex",1,0.05,"--","--","--"]
["invalid","memory2","ILLINOIS_3_e3_2581_e7_3447","cex",2,0.03,"cex",2,0.09,"cex",1,0.28,"--","--","--","cex",2,0.11,"--","--","--","cex",2,0.21,"cex",2,1.11,"--","--","--"]
["invalid","memory2","MESI_3_e2_1872","cex",2,0.04,"cex",2,0.09,"cex",1,0.24,"--","--","--","cex",2,0.1,"--","--","--","cex",2,0.23,"cex",2,0.51,"--","--","--"]
["invalid","memory2","MESI_3_e2_819","cex",2,0.02,"cex",2,0.09,"cex",1,0.25,"--","--","--","cex",2,0.11,"--","--","--","cex",2,0.24,"cex",2,0.54,"--","--","--"]
["invalid","memory2","MESI_3_e2_819_e2_562","cex",2,0.02,"cex",2,0.09,"cex",1,0.24,"--","--","--","cex",2,0.1,"--","--","--","cex",2,0.17,"cex",2,0.47,"--","--","--"]
["invalid","memory2","MESI_3_e2_819_e3_2698","cex",2,0.02,"cex",2,0.09,"cex",1,0.25,"--","--","--","cex",2,0.1,"--","--","--","cex",2,0.24,"cex",2,0.3,"--","--","--"]
["invalid","memory2","MESI_3_e2_819_e5_2554","cex",2,0.02,"cex",2,0.09,"cex",1,0.25,"--","--","--","cex",2,0.1,"--","--","--","cex",2,0.17,"cex",2,0.53,"--","--","--"]
["invalid","memory2","MESI_3_e2_819_e7_1665","cex",2,0.02,"cex",2,0.09,"cex",1,0.25,"--","--","--","cex",2,0.11,"--","--","--","cex",2,0.33,"cex",2,0.16,"--","--","--"]
["invalid","memory2","MESI_3_e2_819_e8_1896","cex",2,0.02,"cex",2,0.09,"cex",1,0.24,"--","--","--","cex",2,0.1,"--","--","--","cex",2,4.05,"cex",2,0.38,"--","--","--"]
["invalid","memory2","MESI_i1","cex",2,0.02,"cex",2,0.05,"cex",1,0.25,"--","--","--","cex",2,0.06,"--","--","--","cex",2,0.17,"cex",2,0.14,"--","--","--"]
["invalid","memory2","MESI_i1_e2_1758_e8_12","cex",2,0.04,"cex",2,0.05,"cex",1,0.24,"--","--","--","cex",2,0.06,"--","--","--","cex",2,0.17,"cex",2,0.13,"--","--","--"]
["invalid","memory2","MESI_i1_e2_2656","cex",2,0.02,"cex",2,0.05,"cex",1,0.24,"--","--","--","cex",2,0.06,"--","--","--","cex",2,0.74,"cex",2,0.15,"--","--","--"]
["invalid","memory2","MESI_i1_e3_188","cex",2,0.02,"cex",2,0.05,"cex",1,0.23,"--","--","--","cex",2,0.07,"--","--","--","cex",2,0.19,"cex",2,0.15,"--","--","--"]
["invalid","memory2","MESI_i1_e3_2145","cex",2,0.02,"cex",2,0.05,"cex",1,0.24,"--","--","--","cex",2,0.06,"--","--","--","cex",2,0.19,"cex",2,0.14,"--","--","--"]
["invalid","memory2","MESI_i1_e3_2145_e1_2667","cex",2,0.02,"cex",2,0.05,"cex",1,0.25,"--","--","--","cex",2,0.06,"--","--","--","cex",2,0.19,"cex",2,0.2,"--","--","--"]
["invalid","memory2","MESI_i1_e3_2145_e2_2228","cex",2,0.02,"cex",2,0.05,"cex",1,0.24,"--","--","--","cex",2,0.06,"--","--","--","cex",2,0.14,"cex",2,0.13,"--","--","--"]
["invalid","memory2","MESI_i1_e3_2145_e3_977","cex",2,0.02,"cex",2,0.05,"cex",1,0.23,"--","--","--","cex",2,0.06,"--","--","--","cex",2,0.17,"cex",2,0.15,"--","--","--"]
["invalid","memory2","MESI_i1_e3_2145_e4_1717","cex",2,0.02,"cex",2,0.05,"cex",1,0.24,"--","--","--","cex",2,0.06,"--","--","--","cex",2,0.2,"cex",2,0.17,"--","--","--"]
["invalid","memory2","MESI_i1_e3_2145_e5_2391","cex",2,0.02,"cex",2,0.05,"cex",1,0.24,"--","--","--","cex",2,0.06,"--","--","--","cex",2,0.17,"cex",2,0.14,"--","--","--"]
["invalid","memory2","MESI_i1_e3_2145_e6_500","cex",2,0.02,"cex",2,0.05,"cex",1,0.24,"--","--","--","cex",2,0.06,"--","--","--","cex",2,0.14,"cex",2,0.15,"--","--","--"]
["invalid","memory2","MESI_i1_e3_2145_e7_1847","cex",2,0.02,"cex",2,0.04,"cex",1,0.25,"--","--","--","cex",2,0.05,"--","--","--","cex",2,0.17,"cex",2,0.13,"--","--","--"]
["invalid","memory2","MESI_i1_e3_2145_e8_2325","cex",2,0.02,"cex",2,0.05,"cex",1,0.25,"--","--","--","cex",2,0.08,"--","--","--","cex",2,0.17,"cex",2,0.13,"--","--","--"]
["invalid","memory2","MESI_i1_e4_1986","cex",2,0.02,"cex",2,0.05,"cex",1,0.25,"--","--","--","cex",2,0.06,"--","--","--","cex",2,0.17,"cex",2,0.21,"--","--","--"]
["invalid","memory2","MESI_i1_e4_1986_e1_1519","cex",3,0.03,"cex",3,0.07,"cex",2,0.27,"--","--","--","cex",3,0.09,"--","--","--","cex",3,178.83,"cex",3,0.74,"--","--","--"]
["invalid","memory2","MESI_i2","cex",3,0.02,"cex",3,0.07,"cex",2,0.25,"--","--","--","cex",3,0.08,"--","--","--","cex",3,0.2,"cex",3,0.21,"--","--","--"]
["invalid","memory2","MESI_i3","cex",2,0.04,"cex",2,0.05,"cex",1,0.24,"--","--","--","cex",2,0.06,"--","--","--","cex",2,0.13,"cex",2,0.06,"--","--","--"]
["invalid","memory2","MESI_i3_e1_2143","cex",4,0.03,"cex",4,0.09,"cex",3,0.3,"--","--","--","cex",4,0.25,"--","--","--","cex",4,0.29,"cex",4,1.37,"--","--","--"]
["invalid","memory2","MESI_i3_e1_447","cex",4,0.03,"cex",4,0.09,"cex",3,0.28,"--","--","--","cex",4,0.24,"--","--","--","cex",4,0.29,"cex",4,1.33,"--","--","--"]
["invalid","memory2","MESI_i3_e1_447_e2_1098","cex",2,0.02,"cex",2,0.05,"cex",1,0.24,"--","--","--","cex",2,0.06,"--","--","--","cex",2,0.14,"cex",2,0.09,"--","--","--"]
["invalid","memory2","MESI_i3_e1_447_e5_2444","cex",2,0.02,"cex",2,0.05,"cex",1,0.24,"--","--","--","cex",2,0.06,"--","--","--","cex",2,0.14,"cex",2,0.04,"--","--","--"]
["invalid","memory2","MESI_i3_e1_447_e7_2194","cex",4,0.04,"cex",4,0.09,"cex",3,0.3,"--","--","--","cex",4,0.26,"--","--","--","cex",4,0.26,"cex",4,1.17,"--","--","--"]
["invalid","memory2","MESI_i4","cex",4,0.03,"cex",4,0.09,"cex",3,0.29,"--","--","--","cex",4,0.26,"--","--","--","cex",4,0.25,"cex",4,2.05,"--","--","--"]
["invalid","memory2","MESI_i4_e1_1023_e8_2498","cex",5,0.06,"cex",5,0.13,"cex",4,0.35,"--","--","--","cex",5,0.29,"--","--","--","cex",5,0.42,"cex",5,6.14,"--","--","--"]
["invalid","memory2","MESI_i4_e4_1689","cex",5,0.06,"cex",5,0.14,"cex",4,0.36,"--","--","--","cex",5,0.3,"--","--","--","cex",5,0.33,"cex",5,7.5,"--","--","--"]
["invalid","memory2","MESI_i4_e4_1689_e8_290","cex",5,0.06,"cex",5,0.13,"cex",4,0.33,"--","--","--","cex",5,0.31,"--","--","--","cex",5,0.34,"cex",5,6.22,"--","--","--"]
["invalid","memory2","MESI_i4_e8_1381_e1_1837","cex",5,0.07,"cex",5,0.13,"cex",4,0.36,"--","--","--","cex",5,0.29,"--","--","--","cex",5,0.43,"cex",5,6.14,"--","--","--"]
["invalid","memory2","MESI_i4_e8_1381_e4_313","cex",5,0.06,"cex",5,0.12,"cex",4,0.35,"--","--","--","cex",5,0.29,"--","--","--","cex",5,0.34,"cex",5,6.18,"--","--","--"]
["invalid","simulation","metros_2_e1_1116_e1_556","cex",13,0.73,"cex",13,1.02,"cex",12,1.57,"--","--","--","cex",13,5.15,"--","--","--","cex",13,1.3,"timeout",0,900,"--","--","--"]
["invalid","simulation","metros_2_e1_1116_e3_287","cex",8,0.09,"cex",8,0.27,"cex",7,0.51,"--","--","--","cex",8,0.9,"--","--","--","cex",8,0.35,"cex",8,13.08,"--","--","--"]
["invalid","simulation","metros_2_e1_1116_e7_1440","cex",13,0.98,"cex",13,1.03,"cex",12,1.66,"--","--","--","cex",13,4.17,"--","--","--","cex",13,0.97,"timeout",0,900,"--","--","--"]
["invalid","simulation","metros_2_e2_704","cex",23,6.19,"cex",23,6.39,"cex",22,7.64,"--","--","--","cex",23,31.91,"--","--","--","cex",23,7.67,"timeout",0,900,"--","--","--"]
["invalid","simulation","metros_2_e2_704_e1_389","cex",13,0.5,"cex",13,0.78,"cex",12,1.51,"--","--","--","cex",13,4.33,"--","--","--","cex",13,1.3,"timeout",0,900,"--","--","--"]
["invalid","simulation","metros_2_e2_704_e3_76","cex",8,0.11,"cex",8,0.28,"cex",7,0.48,"--","--","--","cex",8,0.95,"--","--","--","cex",8,0.39,"cex",8,27.58,"--","--","--"]
["invalid","simulation","metros_2_e2_704_e7_810","cex",13,0.87,"cex",13,1.06,"cex",12,1.5,"--","--","--","cex",13,4.22,"--","--","--","cex",13,0.81,"timeout",0,900,"--","--","--"]
["invalid","simulation","metros_2_e2_968","cex",23,6.19,"cex",23,6.68,"cex",22,7.66,"--","--","--","cex",23,31.91,"--","--","--","cex",23,7.51,"timeout",0,900,"--","--","--"]
["invalid","simulation","metros_2_e3_112","cex",23,4.49,"cex",23,6.29,"cex",22,8.19,"--","--","--","cex",23,28.55,"--","--","--","cex",23,6.93,"timeout",0,900,"--","--","--"]
["invalid","simulation","metros_3","cex",43,95.32,"cex",43,23.03,"cex",42,22.7,"--","--","--","cex",43,470.96,"--","--","--","cex",43,76.78,"timeout",0,900,"--","--","--"]
["invalid","simulation","metros_3_e3_1117","cex",43,91.19,"cex",43,23.13,"cex",42,23.14,"--","--","--","cex",43,483.03,"--","--","--","cex",43,79.92,"timeout",0,900,"--","--","--"]
["invalid","simulation","metros_3_e3_1275","cex",43,91.23,"cex",43,23.11,"cex",42,23,"--","--","--","cex",43,482.91,"--","--","--","cex",43,78.26,"timeout",0,900,"--","--","--"]
["invalid","simulation","metros_3_e3_1275_e1_1350","cex",23,5.8,"cex",23,2.76,"cex",22,5.29,"--","--","--","cex",23,26.37,"--","--","--","cex",23,7.54,"timeout",0,900,"--","--","--"]
["invalid","simulation","metros_3_e3_1275_e4_164","cex",43,129.49,"cex",43,23.06,"cex",42,25.4,"--","--","--","cex",43,514.03,"--","--","--","cex",43,59.9,"timeout",0,900,"--","--","--"]
["invalid","simulation","metros_3_e3_1275_e5_846","cex",43,96.74,"cex",43,23.29,"cex",42,22.59,"--","--","--","cex",43,520.57,"--","--","--","cex",43,78.38,"timeout",0,900,"--","--","--"]
["invalid","simulation","metros_3_e3_1275_e6_1315","cex",43,96.27,"cex",43,23.21,"cex",42,23.13,"--","--","--","cex",43,471.37,"--","--","--","cex",43,76.75,"timeout",0,900,"--","--","--"]
["invalid","simulation","metros_3_e3_1275_e7_529","cex",43,86.92,"cex",43,22.05,"cex",42,25.57,"--","--","--","cex",43,304.92,"--","--","--","cex",43,76.23,"timeout",0,900,"--","--","--"]
["invalid","simulation","metros_3_e4_1251","cex",42,83.74,"cex",42,21.69,"cex",41,23.53,"--","--","--","cex",42,269.32,"--","--","--","cex",42,111.89,"timeout",0,900,"--","--","--"]
["invalid","simulation","metros_3_e4_987","cex",42,82.69,"cex",42,21.53,"cex",41,23.34,"--","--","--","cex",42,269.82,"--","--","--","cex",42,109.86,"timeout",0,900,"--","--","--"]
["invalid","simulation","metros_3_e4_987_e1_1115","cex",42,98.47,"cex",42,22.5,"cex",41,24.11,"--","--","--","cex",42,313.42,"--","--","--","cex",42,96.21,"timeout",0,900,"--","--","--"]
["invalid","simulation","metros_3_e4_987_e2_80","cex",42,117.83,"cex",42,22.51,"cex",41,23.46,"--","--","--","cex",42,361.25,"--","--","--","cex",42,55.44,"timeout",0,900,"--","--","--"]
["invalid","simulation","metros_3_e4_987_e3_291","cex",42,89.74,"cex",42,21.88,"cex",41,23.32,"--","--","--","cex",42,303.94,"--","--","--","cex",42,133.88,"timeout",0,900,"--","--","--"]
["invalid","simulation","metros_4","cex",33,29.62,"cex",33,10.1,"cex",32,10.44,"--","--","--","cex",33,126.28,"--","--","--","cex",33,31.73,"timeout",0,900,"--","--","--"]
["invalid","simulation","metros_4_e1_821_e5_911","cex",34,33.61,"cex",34,11.21,"cex",33,11.38,"--","--","--","cex",34,163.41,"--","--","--","cex",34,35.64,"timeout",0,900,"--","--","--"]
["invalid","simulation","metros_4_e1_917","cex",33,29.97,"cex",33,10.4,"cex",32,9.89,"--","--","--","cex",33,116.06,"--","--","--","cex",33,18.07,"timeout",0,900,"--","--","--"]
["invalid","simulation","metros_4_e2_532","cex",33,43.07,"cex",33,10.32,"cex",32,11.26,"--","--","--","cex",33,161.83,"--","--","--","cex",33,36.46,"timeout",0,900,"--","--","--"]
["invalid","simulation","metros_4_e2_968","cex",33,42.3,"cex",33,10.3,"cex",32,11.35,"--","--","--","cex",33,162.05,"--","--","--","cex",33,36.42,"timeout",0,900,"--","--","--"]
["invalid","simulation","metros_4_e2_968_e1_956","cex",18,3.87,"cex",18,1.35,"cex",17,2.23,"--","--","--","cex",18,10.22,"--","--","--","cex",18,3.18,"timeout",0,900,"--","--","--"]
["invalid","simulation","metros_4_e2_968_e4_801","cex",32,32.47,"cex",32,9.5,"cex",31,10.15,"--","--","--","cex",32,125.06,"--","--","--","cex",32,36.78,"timeout",0,900,"--","--","--"]
["invalid","simulation","metros_4_e2_968_e5_991","cex",34,44.23,"cex",34,11.18,"cex",33,11.62,"--","--","--","cex",34,215.37,"--","--","--","cex",34,41.04,"timeout",0,900,"--","--","--"]
["invalid","simulation","metros_4_e2_968_e6_236","cex",18,2.88,"cex",18,1.68,"cex",17,1.58,"--","--","--","cex",18,9.19,"--","--","--","cex",18,6.9,"timeout",0,900,"--","--","--"]
["invalid","simulation","metros_4_e2_968_e7_860","cex",33,41.53,"cex",33,10.04,"cex",32,11.35,"--","--","--","cex",33,89.04,"--","--","--","cex",33,27.6,"timeout",0,900,"--","--","--"]
["invalid","simulation","metros_4_e3_1025","cex",33,30.7,"cex",33,10.02,"cex",32,10.23,"--","--","--","cex",33,117.48,"--","--","--","cex",33,27.85,"timeout",0,900,"--","--","--"]
["invalid","simulation","metros_4_e3_1091","cex",33,31.35,"cex",33,10,"cex",32,10.27,"--","--","--","cex",33,118.53,"--","--","--","cex",33,27.17,"timeout",0,900,"--","--","--"]
["invalid","simulation","metros_4_e3_1091_e1_1044","cex",18,2.28,"cex",18,1.3,"cex",17,2.23,"--","--","--","cex",18,8.89,"--","--","--","cex",18,3.85,"timeout",0,900,"--","--","--"]
["invalid","simulation","metros_4_e3_1091_e4_232","cex",33,42.87,"cex",33,10.34,"cex",32,11.07,"--","--","--","cex",33,162.38,"--","--","--","cex",33,33.47,"timeout",0,900,"--","--","--"]
["invalid","simulation","metros_4_e5_1150","cex",34,31.18,"cex",34,11.17,"cex",33,11.23,"--","--","--","cex",34,160.88,"--","--","--","cex",34,36.52,"timeout",0,900,"--","--","--"]
["invalid","simulation","metros_4_e6_239_e2_307","cex",18,2.88,"cex",18,1.69,"cex",17,1.6,"--","--","--","cex",18,9.49,"--","--","--","cex",18,6.89,"timeout",0,900,"--","--","--"]
["invalid","simulation","metros_5","cex",33,40.58,"cex",33,22.37,"cex",32,21.58,"--","--","--","cex",33,190.02,"--","--","--","cex",33,33.94,"timeout",0,900,"--","--","--"]
["invalid","simulation","metros_5_e4_1208_e1_337","cex",32,35.38,"cex",32,18.8,"cex",31,21.91,"--","--","--","cex",32,169.24,"--","--","--","cex",32,34.73,"timeout",0,900,"--","--","--"]
["invalid","large","microwave12","cex",3,0.14,"cex",3,0.34,"cex",2,0.5,"--","--","--","cex",3,0.52,"--","--","--","cex",3,9.12,"err:error",0,900,"--","--","--"]
["invalid","large","microwave14","cex",3,0.12,"cex",3,0.36,"cex",2,0.5,"--","--","--","cex",3,0.49,"--","--","--","cex",3,7.03,"err:error",0,900,"--","--","--"]
["invalid","large","microwave18","cex",3,0.14,"cex",3,0.46,"cex",2,0.54,"--","--","--","cex",3,0.47,"--","--","--","cex",3,8.85,"err:error",0,900,"--","--","--"]
["invalid","large","microwave20","cex",2,0.11,"cex",2,0.43,"cex",1,0.45,"--","--","--","cex",2,0.46,"--","--","--","cex",2,3.78,"err:error",0,900,"--","--","--"]
["invalid","large","microwave23","cex",3,0.22,"cex",3,0.55,"cex",2,0.56,"--","--","--","cex",3,0.53,"--","--","--","cex",3,5.76,"err:error",0,900,"--","--","--"]
["invalid","large","microwave25","cex",2,0.13,"cex",2,0.38,"cex",1,0.44,"--","--","--","cex",2,0.41,"--","--","--","cex",2,2.69,"err:error",0,900,"--","--","--"]
["invalid","large","microwave28","cex",3,0.27,"cex",3,0.53,"cex",2,0.57,"--","--","--","cex",3,0.55,"--","--","--","cex",3,4.83,"err:error",0,900,"--","--","--"]
["invalid","large","microwave31","cex",4,1.35,"cex",4,1.52,"cex",3,1.14,"--","--","--","cex",4,3.5,"--","--","--","cex",4,9.54,"err:error",0,900,"--","--","--"]
["invalid","large","microwave32","cex",4,0.92,"cex",4,1.13,"cex",3,1.21,"--","--","--","cex",4,2.77,"--","--","--","cex",4,7.46,"err:error",0,900,"--","--","--"]
["invalid","large","microwave33","cex",4,1.26,"cex",4,1.72,"cex",3,1.28,"--","--","--","cex",4,3.1,"--","--","--","cex",4,6.67,"err:error",0,900,"--","--","--"]
["invalid","large","microwave34","cex",4,1.06,"cex",4,1.31,"cex",3,1.34,"--","--","--","cex",4,2.93,"--","--","--","cex",4,8.91,"err:error",0,900,"--","--","--"]
["invalid","large","microwave35","cex",4,1.24,"cex",4,1.85,"cex",3,1.22,"--","--","--","cex",4,3.5,"--","--","--","cex",4,8.26,"err:error",0,900,"--","--","--"]
["invalid","large","microwave36","cex",4,1.91,"cex",4,1.52,"cex",3,1.25,"--","--","--","cex",4,3.16,"--","--","--","cex",4,9.44,"err:error",0,900,"--","--","--"]
["invalid","large","microwave37","cex",4,1.08,"cex",4,1.53,"cex",3,1.35,"--","--","--","cex",4,3.05,"--","--","--","cex",4,7.47,"err:error",0,900,"--","--","--"]
["invalid","large","microwave38","cex",4,1.49,"cex",4,1.09,"cex",3,1.24,"--","--","--","cex",4,2.76,"--","--","--","cex",4,7.2,"err:error",0,900,"--","--","--"]
["invalid","large","microwave39","cex",4,1.34,"cex",4,0.99,"cex",3,1.14,"--","--","--","cex",4,2.51,"--","--","--","cex",4,11.3,"err:error",0,900,"--","--","--"]
["invalid","large","microwave40","cex",2,0.09,"cex",2,0.34,"cex",1,0.45,"--","--","--","cex",2,0.37,"--","--","--","cex",2,2.77,"err:error",0,900,"--","--","--"]
["invalid","memory2","MOESI_2_e1_1753_e1_1510","cex",2,0.02,"cex",2,0.06,"cex",1,0.25,"--","--","--","cex",2,0.07,"--","--","--","cex",2,0.18,"cex",2,0.2,"--","--","--"]
["invalid","memory2","MOESI_2_e1_1753_e2_615","cex",2,0.02,"cex",2,0.06,"cex",1,0.24,"--","--","--","cex",2,0.07,"--","--","--","cex",2,0.22,"cex",2,0.17,"--","--","--"]
["invalid","memory2","MOESI_2_e1_1753_e3_2021","cex",3,0.03,"cex",3,0.08,"cex",2,0.28,"--","--","--","cex",3,0.1,"--","--","--","cex",3,3.04,"cex",3,1.38,"--","--","--"]
["invalid","memory2","MOESI_2_e1_1753_e7_1626","cex",2,0.02,"cex",2,0.05,"cex",1,0.25,"--","--","--","cex",2,0.06,"--","--","--","cex",2,0.19,"cex",2,0.29,"--","--","--"]
["invalid","memory2","MOESI_2_e2_1599_e1_2383","cex",2,0.02,"cex",2,0.05,"cex",1,0.24,"--","--","--","cex",2,0.07,"--","--","--","cex",2,0.19,"cex",2,0.18,"--","--","--"]
["invalid","memory2","MOESI_2_e2_1599_e2_1815","cex",2,0.02,"cex",2,0.06,"cex",1,0.25,"--","--","--","cex",2,0.07,"--","--","--","cex",2,0.2,"cex",2,0.16,"--","--","--"]
["invalid","memory2","MOESI_2_e2_1599_e3_1658","cex",3,0.03,"cex",3,0.08,"cex",2,0.28,"--","--","--","cex",3,0.1,"--","--","--","cex",3,2.45,"cex",3,1.6,"--","--","--"]
["invalid","memory2","MOESI_2_e2_1599_e7_1597","cex",2,0.02,"cex",2,0.06,"cex",1,0.25,"--","--","--","cex",2,0.07,"--","--","--","timeout",0,900,"cex",2,0.33,"--","--","--"]
["invalid","memory2","MOESI_2_e3_929_e1_2319","cex",2,0.02,"cex",2,0.06,"cex",1,0.24,"--","--","--","cex",2,0.07,"--","--","--","cex",2,0.17,"cex",2,0.19,"--","--","--"]
["invalid","memory2","MOESI_2_e3_929_e2_2421","cex",2,0.02,"cex",2,0.06,"cex",1,0.25,"--","--","--","cex",2,0.07,"--","--","--","cex",2,0.22,"cex",2,0.17,"--","--","--"]
["invalid","memory2","MOESI_2_e3_929_e3_2294","cex",3,0.03,"cex",3,0.08,"cex",2,0.26,"--","--","--","cex",3,0.1,"--","--","--","cex",3,4.5,"cex",3,1.57,"--","--","--"]
["invalid","memory2","MOESI_2_e3_929_e7_619","cex",2,0.02,"cex",2,0.06,"cex",1,0.25,"--","--","--","cex",2,0.07,"--","--","--","timeout",0,900,"cex",2,0.36,"--","--","--"]
["invalid","memory2","MOESI_2_e7_2607","cex",2,0.02,"cex",2,0.06,"cex",1,0.25,"--","--","--","cex",2,0.07,"--","--","--","timeout",0,900,"cex",2,0.36,"--","--","--"]
["invalid","memory2","MOESI_2_e7_2910","cex",2,0.02,"cex",2,0.06,"cex",1,0.25,"--","--","--","cex",2,0.07,"--","--","--","timeout",0,900,"cex",2,0.34,"--","--","--"]
["invalid","memory2","MOESI_2_e7_2910_e1_1021","cex",2,0.02,"cex",2,0.05,"cex",1,0.25,"--","--","--","cex",2,0.06,"--","--","--","cex",2,0.18,"cex",2,0.31,"--","--","--"]
["invalid","memory2","MOESI_2_e7_2910_e2_611","cex",2,0.02,"cex",2,0.06,"cex",1,0.24,"--","--","--","cex",2,0.07,"--","--","--","timeout",0,900,"cex",2,0.33,"--","--","--"]
["invalid","memory2","MOESI_2_e7_2910_e3_2002","cex",2,0.02,"cex",2,0.06,"cex",1,0.25,"--","--","--","cex",2,0.07,"--","--","--","timeout",0,900,"cex",2,0.34,"--","--","--"]
["invalid","memory2","MOESI_2_e7_2910_e7_1804","cex",2,0.02,"cex",2,0.05,"cex",1,0.25,"--","--","--","cex",2,0.06,"--","--","--","timeout",0,900,"cex",2,0.41,"--","--","--"]
["invalid","memory2","MOESI_2_e8_926_e7_961","cex",2,0.02,"cex",2,0.06,"cex",1,0.26,"--","--","--","cex",2,0.07,"--","--","--","timeout",0,900,"cex",2,0.34,"--","--","--"]
["invalid","memory2","MOESI_all_e3_2032_e3_2788","cex",3,0.03,"cex",3,0.09,"cex",2,0.28,"--","--","--","cex",3,0.11,"--","--","--","timeout",0,900,"cex",3,1.58,"--","--","--"]
["invalid","protocol","peterson_vt","cex",4,0.1,"cex",4,0.23,"cex",3,0.5,"--","--","--","cex",4,0.58,"--","--","--","cex",4,724.92,"cex",4,44.68,"--","--","--"]
["invalid","simulation","PRODUCER_CONSUMMER_luke_1","cex",2,0.01,"cex",2,0.04,"cex",1,0.24,"--","--","--","cex",2,0.07,"--","--","--","cex",2,0.08,"cex",2,0.07,"--","--","--"]
["invalid","simulation","production_cell_e7_207","cex",2,0.01,"cex",2,0.07,"cex",1,0.24,"--","--","--","cex",2,0.09,"--","--","--","cex",2,0.03,"cex",2,0.03,"--","--","--"]
["invalid","simulation","production_cell_e7_207_e7_41","cex",2,0.01,"cex",2,0.07,"cex",1,0.23,"--","--","--","cex",2,0.08,"--","--","--","cex",2,0.03,"cex",2,0.03,"--","--","--"]
["invalid","simulation","production_cell_e7_21","cex",2,0.01,"cex",2,0.07,"cex",1,0.24,"--","--","--","cex",2,0.08,"--","--","--","cex",2,0.02,"cex",2,0.01,"--","--","--"]
["invalid","simulation","production_cell_e8_6_e7_651","cex",2,0.01,"cex",2,0.08,"cex",1,0.24,"--","--","--","cex",2,0.1,"--","--","--","cex",2,0.03,"cex",2,0.02,"--","--","--"]
["invalid","simulation","production_cell_e8_6_e8_427","cex",3,0.02,"cex",3,0.09,"cex",2,0.24,"--","--","--","cex",3,0.1,"--","--","--","cex",3,0.02,"cex",3,0.03,"--","--","--"]
["invalid","misc","stalmark_e8_48","cex",2,0.01,"cex",2,0.02,"cex",1,0.23,"--","--","--","cex",2,0.04,"--","--","--","cex",2,0.03,"cex",2,0.02,"--","--","--"]
["invalid","misc","stalmark_e8_64","cex",2,0.01,"cex",2,0.02,"cex",1,0.23,"--","--","--","cex",2,0.03,"--","--","--","cex",2,0.02,"cex",2,0.02,"--","--","--"]
["invalid","misc","stalmark_e8_64_e7_80","cex",3,0.01,"cex",3,0.02,"cex",2,0.24,"--","--","--","cex",3,0.03,"--","--","--","cex",3,0.02,"cex",3,0.02,"--","--","--"]
["invalid","misc","stalmark_e8_64_e8_207","cex",2,0.01,"cex",2,0.07,"cex",0,0.21,"--","--","--","cex",2,0.03,"--","--","--","cex",1,0.02,"cex",1,0.03,"--","--","--"]
["invalid","protocol","swimmingpool_1","cex",6,0.13,"cex",6,0.27,"cex",5,0.55,"--","--","--","cex",6,0.59,"--","--","--","cex",6,120.1,"cex",6,30.95,"--","--","--"]
["invalid","protocol","swimmingpool_1_e7_1621","cex",4,0.07,"cex",4,0.16,"cex",3,0.36,"--","--","--","cex",4,0.44,"--","--","--","cex",4,2,"cex",4,31.24,"--","--","--"]
["invalid","protocol","swimmingpool_2","cex",2,0.03,"cex",2,0.08,"cex",1,0.26,"--","--","--","cex",2,0.09,"--","--","--","cex",2,0.13,"cex",2,0.4,"--","--","--"]
["invalid","protocol","swimmingpool_3","cex",3,0.03,"cex",3,0.11,"cex",2,0.31,"--","--","--","cex",3,0.13,"--","--","--","cex",3,0.2,"cex",3,1.35,"--","--","--"]
["invalid","protocol","swimmingpool_4","cex",4,0.05,"cex",4,0.14,"cex",3,0.33,"--","--","--","cex",4,0.38,"--","--","--","cex",4,0.28,"cex",4,3.31,"--","--","--"]
["invalid","protocol","swimmingpool_4_e7_2197","cex",4,0.05,"cex",4,0.14,"cex",3,0.35,"--","--","--","cex",4,0.41,"--","--","--","cex",4,0.29,"cex",4,7.44,"--","--","--"]
["invalid","protocol","swimmingpool_5","cex",5,0.06,"cex",5,0.18,"cex",4,0.4,"--","--","--","cex",5,0.43,"--","--","--","cex",5,0.39,"cex",5,7.53,"--","--","--"]
["invalid","protocol","swimmingpool_6","cex",6,0.07,"cex",6,0.2,"cex",5,0.44,"--","--","--","cex",6,0.48,"--","--","--","cex",6,0.47,"cex",6,19.42,"--","--","--"]
["invalid","protocol","swimmingpool_6_e7_10","cex",6,0.1,"cex",6,0.2,"cex",5,0.46,"--","--","--","cex",6,0.5,"--","--","--","cex",6,0.52,"cex",6,20.21,"--","--","--"]
["invalid","protocol","swimmingpool_6_e7_10_e7_341","cex",6,0.09,"cex",6,0.2,"cex",5,0.46,"--","--","--","cex",6,0.5,"--","--","--","cex",6,0.52,"cex",6,23.42,"--","--","--"]
["invalid","protocol","swimmingpool_6_e7_10_e8_1713","cex",6,0.07,"cex",6,0.2,"cex",5,0.46,"--","--","--","cex",6,0.49,"--","--","--","cex",6,0.48,"cex",6,18.83,"--","--","--"]
["invalid","protocol","swimmingpool_6_e7_399","cex",6,0.1,"cex",6,0.2,"cex",5,0.44,"--","--","--","cex",6,0.5,"--","--","--","cex",6,0.5,"cex",6,20.29,"--","--","--"]
["invalid","protocol","swimmingpool_7","cex",7,0.09,"cex",7,0.26,"cex",6,0.53,"--","--","--","cex",7,1.03,"--","--","--","cex",7,0.64,"cex",7,38.19,"--","--","--"]
["invalid","protocol","swimmingpool_8","cex",8,0.12,"cex",8,0.31,"cex",7,0.61,"--","--","--","cex",8,1.08,"--","--","--","cex",8,0.79,"cex",8,93.06,"--","--","--"]
["invalid","protocol","swimmingpool_9","cex",12,0.37,"cex",12,1.63,"cex",11,1.19,"--","--","--","cex",12,5.43,"--","--","--","cex",12,9.9,"cex",12,390.04,"--","--","--"]
["invalid","misc","switch","cex",3,0.01,"cex",3,0.02,"cex",2,0.23,"--","--","--","cex",3,0.03,"--","--","--","cex",3,0.01,"cex",3,0.05,"--","--","--"]
["invalid","misc","switch2","cex",3,0.01,"cex",3,0.02,"cex",2,0.23,"--","--","--","cex",3,0.03,"--","--","--","cex",3,0.01,"cex",3,0.03,"--","--","--"]
["invalid","memory2","SYNAPSE_123_e2_1350_e8_1354","cex",2,0.02,"cex",2,0.06,"cex",1,0.24,"--","--","--","cex",2,0.07,"--","--","--","cex",2,0.1,"cex",2,0.32,"--","--","--"]
["invalid","memory2","SYNAPSE_123_e2_1653","cex",2,0.02,"cex",2,0.07,"cex",1,0.26,"--","--","--","cex",2,0.08,"--","--","--","cex",2,0.1,"cex",2,0.31,"--","--","--"]
["invalid","memory2","SYNAPSE_123_e3_302","cex",3,0.02,"cex",3,0.09,"cex",2,0.25,"--","--","--","cex",3,0.1,"--","--","--","timeout",0,900,"timeout",0,900,"--","--","--"]
["invalid","memory2","SYNAPSE_123_e3_302_e1_1141","cex",3,0.02,"cex",3,0.26,"cex",2,0.27,"--","--","--","cex",3,0.1,"--","--","--","cex",3,30.64,"timeout",0,900,"--","--","--"]
["invalid","memory2","SYNAPSE_123_e7_837_e2_1394","cex",2,0.02,"cex",2,0.06,"cex",1,0.24,"--","--","--","cex",2,0.08,"--","--","--","cex",2,0.12,"cex",2,0.16,"--","--","--"]
["invalid","memory2","SYNAPSE_123_e7_837_e3_135","cex",3,0.03,"cex",3,0.08,"cex",2,0.26,"--","--","--","cex",3,0.11,"--","--","--","cex",3,22.95,"timeout",0,900,"--","--","--"]
["invalid","memory2","SYNAPSE_123_e8_953_e1_1128","cex",2,0.02,"cex",2,0.06,"cex",1,0.24,"--","--","--","cex",2,0.08,"--","--","--","cex",2,0.14,"cex",2,0.36,"--","--","--"]
["invalid","memory2","SYNAPSE_123_e8_953_e2_458","cex",2,0.02,"cex",2,0.06,"cex",1,0.24,"--","--","--","cex",2,0.08,"--","--","--","cex",2,0.11,"cex",2,0.3,"--","--","--"]
["invalid","memory2","SYNAPSE_123_e8_953_e3_271","cex",3,0.03,"cex",3,0.09,"cex",2,0.25,"--","--","--","cex",3,0.11,"--","--","--","timeout",0,900,"timeout",0,900,"--","--","--"]
["invalid","memory2","SYNAPSE_2_e1_1239","cex",2,0.02,"cex",2,0.07,"cex",1,0.24,"--","--","--","cex",2,0.06,"--","--","--","cex",2,0.13,"cex",2,0.11,"--","--","--"]
["invalid","memory2","SYNAPSE_2_e1_1239_e1_1331","cex",2,0.02,"cex",2,0.05,"cex",1,0.24,"--","--","--","cex",2,0.06,"--","--","--","cex",2,0.11,"cex",2,0.11,"--","--","--"]
["invalid","memory2","SYNAPSE_2_e1_1239_e2_74","cex",2,0.02,"cex",2,0.05,"cex",1,0.23,"--","--","--","cex",2,0.06,"--","--","--","cex",2,0.12,"cex",2,0.1,"--","--","--"]
["invalid","memory2","SYNAPSE_2_e3_216","cex",3,0.02,"cex",3,0.07,"cex",2,0.26,"--","--","--","cex",3,0.09,"--","--","--","cex",3,121.58,"timeout",0,900,"--","--","--"]
["invalid","memory2","SYNAPSE_2_e8_1118_e1_667","cex",2,0.02,"cex",2,0.05,"cex",1,0.24,"--","--","--","cex",2,0.06,"--","--","--","cex",2,0.19,"cex",2,0.12,"--","--","--"]
["invalid","memory2","SYNAPSE_2_e8_1118_e2_237","cex",2,0.02,"cex",2,0.05,"cex",1,0.23,"--","--","--","cex",2,0.06,"--","--","--","cex",2,0.24,"cex",2,0.08,"--","--","--"]
["invalid","memory2","SYNAPSE_2_e8_1118_e3_1216","cex",3,0.02,"cex",3,0.07,"cex",2,0.26,"--","--","--","cex",3,0.08,"--","--","--","cex",3,14.4,"timeout",0,900,"--","--","--"]
["invalid","memory2","SYNAPSE_3_e1_1303","cex",2,0.02,"cex",2,0.05,"cex",1,0.24,"--","--","--","cex",2,0.07,"--","--","--","cex",2,0.1,"cex",2,0.19,"--","--","--"]
["invalid","memory2","SYNAPSE_3_e1_1416","cex",2,0.02,"cex",2,0.05,"cex",1,0.23,"--","--","--","cex",2,0.07,"--","--","--","cex",2,0.1,"cex",2,0.18,"--","--","--"]
["invalid","memory2","SYNAPSE_3_e1_1416_e1_1675","cex",2,0.02,"cex",2,0.06,"cex",1,0.24,"--","--","--","cex",2,0.07,"--","--","--","cex",2,0.1,"cex",2,0.18,"--","--","--"]
["invalid","memory2","SYNAPSE_3_e1_1416_e2_753","cex",2,0.02,"cex",2,0.06,"cex",1,0.24,"--","--","--","cex",2,0.07,"--","--","--","cex",2,0.09,"cex",2,0.16,"--","--","--"]
["invalid","memory2","SYNAPSE_3_e1_1416_e3_1191","cex",2,0.02,"cex",2,0.06,"cex",1,0.23,"--","--","--","cex",2,0.07,"--","--","--","cex",2,0.1,"cex",2,0.18,"--","--","--"]
["invalid","memory2","SYNAPSE_3_e1_1416_e7_193","cex",2,0.02,"cex",2,0.06,"cex",1,0.24,"--","--","--","cex",2,0.07,"--","--","--","cex",2,0.1,"cex",2,0.18,"--","--","--"]
["invalid","memory2","SYNAPSE_3_e3_1041","cex",3,0.02,"cex",3,0.07,"cex",2,0.26,"--","--","--","cex",3,0.1,"--","--","--","cex",3,194.75,"timeout",0,900,"--","--","--"]
["invalid","memory2","SYNAPSE_3_e3_518_e8_922","cex",3,0.02,"cex",3,0.07,"cex",2,0.25,"--","--","--","cex",3,0.1,"--","--","--","cex",3,39.19,"timeout",0,900,"--","--","--"]
["invalid","memory2","SYNAPSE_3_e8_1329_e1_1270","cex",2,0.02,"cex",2,0.05,"cex",1,0.24,"--","--","--","cex",2,0.06,"--","--","--","cex",2,0.1,"cex",2,0.22,"--","--","--"]
["invalid","memory2","SYNAPSE_3_e8_1329_e2_236","cex",2,0.02,"cex",2,0.05,"cex",1,0.24,"--","--","--","cex",2,0.06,"--","--","--","cex",2,0.09,"cex",2,0.19,"--","--","--"]
["invalid","memory2","SYNAPSE_3_e8_1329_e3_421","cex",3,0.02,"cex",3,0.07,"cex",2,0.26,"--","--","--","cex",3,0.1,"--","--","--","cex",3,38.86,"timeout",0,900,"--","--","--"]
["invalid","memory2","SYNAPSE_5_e1_1375","cex",3,0.02,"cex",3,0.06,"cex",2,0.26,"--","--","--","cex",3,0.09,"--","--","--","cex",3,0.14,"cex",3,0.28,"--","--","--"]
["invalid","memory2","SYNAPSE_5_e1_811","cex",3,0.02,"cex",3,0.06,"cex",2,0.25,"--","--","--","cex",3,0.09,"--","--","--","cex",3,0.15,"cex",3,0.28,"--","--","--"]
["invalid","memory2","SYNAPSE_5_e1_811_e1_823","cex",3,0.02,"cex",3,0.06,"cex",2,0.26,"--","--","--","cex",3,0.09,"--","--","--","cex",3,0.17,"cex",3,0.27,"--","--","--"]
["invalid","memory2","SYNAPSE_5_e1_811_e2_1026","cex",3,0.02,"cex",3,0.06,"cex",2,0.26,"--","--","--","cex",3,0.09,"--","--","--","cex",3,0.33,"cex",3,0.27,"--","--","--"]
["invalid","memory2","SYNAPSE_all_e3_1750","cex",3,0.03,"cex",3,0.08,"cex",2,0.27,"--","--","--","cex",3,0.1,"--","--","--","cex",3,62.33,"timeout",0,900,"--","--","--"]
["invalid","memory2","SYNAPSE_all_e3_1864_e3_495","cex",3,0.02,"cex",3,0.08,"cex",2,0.26,"--","--","--","cex",3,0.1,"--","--","--","cex",3,15.04,"timeout",0,900,"--","--","--"]
["invalid","memory2","SYNAPSE_all_e3_1864_e4_34","cex",2,0.02,"cex",2,0.07,"cex",1,0.24,"--","--","--","cex",2,0.08,"--","--","--","cex",2,0.12,"cex",2,0.32,"--","--","--"]
["invalid","memory2","SYNAPSE_all_e3_1864_e5_1637","cex",2,0.02,"cex",2,0.07,"cex",1,0.24,"--","--","--","cex",2,0.08,"--","--","--","cex",2,0.1,"timeout",0,900,"--","--","--"]
["invalid","memory2","SYNAPSE_all_e3_1864_e7_251","cex",3,0.03,"cex",3,0.09,"cex",2,0.27,"--","--","--","cex",3,0.11,"--","--","--","cex",3,13.54,"timeout",0,900,"--","--","--"]
["invalid","memory2","SYNAPSE_all_e8_251_e1_1852","cex",2,0.02,"cex",2,0.06,"cex",1,0.24,"--","--","--","cex",2,0.08,"--","--","--","cex",2,0.1,"cex",2,0.3,"--","--","--"]
["invalid","memory2","SYNAPSE_all_e8_251_e2_1053","cex",2,0.02,"cex",2,0.06,"cex",1,0.24,"--","--","--","cex",2,0.08,"--","--","--","cex",2,0.1,"cex",2,0.27,"--","--","--"]
["invalid","memory2","SYNAPSE_all_e8_251_e3_1472","cex",3,0.02,"cex",3,0.08,"cex",2,0.27,"--","--","--","cex",3,0.1,"--","--","--","timeout",0,900,"timeout",0,900,"--","--","--"]
["invalid","memory2","SYNAPSE_i1","cex",2,0.02,"cex",2,0.05,"cex",1,0.23,"--","--","--","cex",2,0.06,"--","--","--","cex",2,0.1,"cex",2,0.06,"--","--","--"]
["invalid","misc","ticket3i_3_e7_1312","cex",2,0.03,"cex",2,0.04,"cex",1,0.28,"--","--","--","cex",2,0.06,"--","--","--","cex",2,0.15,"cex",2,0.28,"--","--","--"]
["invalid","misc","ticket3i_3_e7_1312_e7_1495","cex",2,0.03,"cex",2,0.05,"cex",1,0.3,"--","--","--","cex",2,0.07,"--","--","--","cex",2,0.14,"cex",2,0.57,"--","--","--"]
["invalid","misc","ticket3i_3_e7_99","cex",2,0.03,"cex",2,0.04,"cex",1,0.29,"--","--","--","cex",2,0.06,"--","--","--","cex",2,0.15,"cex",2,0.31,"--","--","--"]
["invalid","misc","ticket3i_3_e8_1703_e7_3491","cex",2,0.03,"cex",2,0.04,"cex",1,0.28,"--","--","--","cex",2,0.06,"--","--","--","cex",2,0.13,"cex",2,0.27,"--","--","--"]
["invalid","misc","traffic_e7_348","cex",2,0.01,"cex",2,0.02,"cex",0,0.22,"--","--","--","cex",2,0.02,"--","--","--","cex",1,0.03,"cex",1,0.02,"--","--","--"]
["invalid","misc","traffic_e7_46","cex",2,0.01,"cex",2,0.02,"cex",0,0.21,"--","--","--","cex",2,0.02,"--","--","--","cex",1,0.03,"cex",1,0.05,"--","--","--"]
["invalid","misc","traffic_e7_46_e7_171","cex",2,0.01,"cex",2,0.02,"cex",0,0.21,"--","--","--","cex",2,0.03,"--","--","--","cex",1,0.03,"cex",1,0.01,"--","--","--"]
["invalid","misc","two_counters_e1_268","cex",2,0.01,"cex",2,0.02,"cex",1,0.23,"--","--","--","cex",2,0.03,"--","--","--","cex",2,0.03,"cex",2,0.02,"--","--","--"]
["invalid","misc","two_counters_e2_3","cex",3,0.01,"cex",3,0.03,"cex",2,0.24,"--","--","--","cex",3,0.04,"--","--","--","cex",3,0.03,"cex",3,0.01,"--","--","--"]
["invalid","misc","two_counters_e3_325","cex",3,0.01,"cex",3,0.03,"cex",2,0.24,"--","--","--","cex",3,0.04,"--","--","--","cex",3,0.01,"cex",3,0.01,"--","--","--"]
["invalid","misc","two_counters_e7_222","cex",2,0.01,"cex",2,0.02,"cex",1,0.23,"--","--","--","cex",2,0.03,"--","--","--","cex",2,0.02,"cex",2,0.03,"--","--","--"]
["invalid","simulation","ums_e7_1700","cex",3,0.05,"cex",3,0.4,"cex",1,0.25,"--","--","--","cex",3,0.43,"--","--","--","cex",3,0.05,"err:stack",0,900,"--","--","--"]
["valid","misc","_6counters_e8_371_e2_80",{"$nulls":6},"--","--","--","holds",3,0.02,"holds",3,0.05,"holds",3,0.27,"holds",0,0.61,"holds",1,0.01,"holds",0,0.17]
["valid","simulation","car_1",{"$nulls":6},"--","--","--","holds",3,0.04,"holds",3,0.1,"holds",3,0.34,"holds",1,0.44,"holds",1,0.05,"cex",0,900]
["valid","simulation","car_2",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.11,"holds",3,0.32,"holds",1,0.47,"holds",1,0.05,"cex",0,900]
["valid","simulation","car_3",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.11,"holds",3,0.3,"holds",1,0.43,"holds",1,0.03,"cex",0,900]
["valid","simulation","car_3_e2_695",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.11,"holds",3,0.28,"holds",1,0.04,"holds",1,0.05,"cex",0,900]
["valid","simulation","car_3_e2_777",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.08,"holds",3,0.3,"holds",1,0.05,"holds",1,0.01,"cex",0,900]
["valid","simulation","car_3_e7_626",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.12,"holds",3,0.28,"holds",1,0.07,"holds",1,0.05,"cex",0,900]
["valid","simulation","car_3_e8_33",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.11,"holds",3,0.31,"holds",1,0.04,"holds",1,0.05,"cex",0,900]
["valid","simulation","car_3_e8_33_e2_1010",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.1,"holds",3,0.3,"holds",1,0.06,"holds",1,0.01,"cex",0,900]
["valid","simulation","car_3_e8_33_e7_220",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.14,"holds",3,0.3,"holds",2,0.05,"holds",2,0.05,"cex",0,900]
["valid","simulation","car_4",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.08,"holds",3,0.28,"holds",1,0.05,"holds",1,0.05,"cex",0,900]
["valid","simulation","car_4_e3_57_e4_1047",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.09,"holds",3,0.32,"holds",1,0.06,"holds",1,0.01,"cex",0,900]
["valid","simulation","car_4_e3_57_e6_784",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.09,"holds",3,0.3,"holds",1,0.05,"holds",1,0.05,"cex",0,900]
["valid","simulation","car_4_e7_592",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.11,"holds",3,0.28,"holds",1,0.08,"holds",1,0.05,"cex",0,900]
["valid","simulation","car_4_e8_118",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.09,"holds",3,0.3,"holds",1,0.05,"holds",1,0.01,"cex",0,900]
["valid","simulation","car_all",{"$nulls":6},"--","--","--","holds",3,0.04,"holds",3,0.1,"holds",3,0.32,"holds",1,0.05,"holds",1,0.06,"cex",0,900]
["valid","simulation","car_all_e2_108",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.09,"holds",3,0.31,"holds",1,0.06,"holds",1,0.05,"cex",0,900]
["valid","simulation","car_all_e2_142",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.11,"holds",3,0.28,"holds",1,0.05,"holds",1,0.02,"cex",0,900]
["valid","simulation","car_all_e2_142_e8_194",{"$nulls":6},"--","--","--","holds",3,0.04,"holds",3,0.1,"holds",3,0.33,"holds",1,0.05,"holds",1,0.05,"cex",0,900]
["valid","simulation","car_all_e3_1068_e4_275",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.1,"holds",3,0.3,"holds",1,0.05,"holds",1,0.05,"cex",0,900]
["valid","simulation","car_all_e3_1068_e6_790",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.1,"holds",3,0.33,"holds",1,0.04,"holds",1,0.06,"cex",0,900]
["valid","simulation","car_all_e8_856",{"$nulls":6},"--","--","--","holds",3,0.04,"holds",3,0.1,"holds",3,0.31,"holds",1,0.04,"holds",1,0.02,"cex",0,900]
["valid","simulation","car_all_e8_856_e2_585",{"$nulls":6},"--","--","--","holds",3,0.04,"holds",3,0.1,"holds",3,0.3,"holds",1,0.06,"holds",1,0.06,"cex",0,900]
["valid","large","ccp01",{"$nulls":6},"--","--","--","holds",3,0.25,"holds",3,0.83,"holds",3,1.03,"err:error",0,900,"err:error",0,900,"cex",0,900]
["valid","large","ccp02",{"$nulls":6},"--","--","--","holds",3,0.24,"holds",3,0.87,"holds",3,0.95,"err:error",0,900,"err:error",0,900,"cex",0,900]
["valid","large","ccp03",{"$nulls":6},"--","--","--","holds",3,0.23,"holds",3,0.84,"holds",3,0.89,"err:error",0,900,"err:error",0,900,"cex",0,900]
["valid","large","ccp04",{"$nulls":6},"--","--","--","holds",3,0.21,"holds",3,0.88,"holds",3,0.96,"err:error",0,900,"err:error",0,900,"cex",0,900]
["valid","large","ccp05",{"$nulls":6},"--","--","--","holds",3,0.22,"holds",3,0.44,"holds",3,0.83,"err:error",0,900,"err:error",0,900,"holds",0,6.32]
["valid","large","ccp06",{"$nulls":6},"--","--","--","holds",3,0.44,"holds",3,1.43,"holds",3,0.95,"err:error",0,900,"err:error",0,900,"timeout",0,900]
["valid","large","ccp07",{"$nulls":6},"--","--","--","holds",3,0.36,"holds",3,1.41,"holds",3,0.87,"err:error",0,900,"err:error",0,900,"cex",0,900]
["valid","large","ccp09",{"$nulls":6},"--","--","--","holds",3,0.31,"holds",3,0.68,"holds",3,0.85,"err:error",0,900,"err:error",0,900,"holds",0,167.88]
["valid","large","ccp15",{"$nulls":6},"--","--","--","holds",3,0.35,"holds",3,1.78,"holds",3,0.9,"err:error",0,900,"err:error",0,900,"holds",0,32.21]
["valid","large","ccp16",{"$nulls":6},"--","--","--","holds",3,0.02,"holds",3,0.04,"holds",3,0.82,"err:error",0,900,"err:error",0,900,"holds",0,0.04]
["valid","large","ccp19",{"$nulls":6},"--","--","--","holds",3,0.32,"holds",3,0.63,"holds",3,0.86,"err:error",0,900,"err:error",0,900,"timeout",0,900]
["valid","simulation","cd",{"$nulls":6},"--","--","--","holds",12,0.3,"holds",12,0.85,"holds",12,1.95,"holds",9,0.18,"holds",9,2.27,"cex",0,900]
["valid","simulation","cd_e7_621_e8_714",{"$nulls":6},"--","--","--","holds",12,0.3,"holds",12,0.83,"holds",12,1.97,"holds",9,0.19,"holds",9,2.23,"cex",0,900]
["valid","large","cruise_controller_01",{"$nulls":6},"--","--","--","holds",3,0.17,"holds",3,0.54,"holds",3,0.96,"err:error",0,900,"err:error",0,900,"???",0,900]
["valid","large","cruise_controller_02",{"$nulls":6},"--","--","--","holds",3,0.19,"holds",3,0.49,"holds",3,0.94,"err:error",0,900,"err:error",0,900,"???",0,900]
["valid","large","cruise_controller_03",{"$nulls":6},"--","--","--","holds",3,0.17,"holds",3,0.54,"holds",3,0.93,"err:error",0,900,"err:error",0,900,"???",0,900]
["valid","large","cruise_controller_04",{"$nulls":6},"--","--","--","holds",3,0.19,"holds",3,0.39,"holds",3,1,"err:error",0,900,"err:error",0,900,"???",0,900]
["valid","large","cruise_controller_05",{"$nulls":6},"--","--","--","holds",3,0.16,"holds",3,0.31,"holds",3,0.89,"err:error",0,900,"err:error",0,900,"???",0,900]
["valid","large","cruise_controller_06",{"$nulls":6},"--","--","--","holds",3,0.26,"holds",3,0.45,"holds",3,1.05,"err:error",0,900,"err:error",0,900,"???",0,900]
["valid","large","cruise_controller_07",{"$nulls":6},"--","--","--","holds",3,0.24,"holds",3,0.43,"holds",3,0.9,"err:error",0,900,"err:error",0,900,"???",0,900]
["valid","large","cruise_controller_11",{"$nulls":6},"--","--","--","holds",3,0.26,"holds",3,0.43,"holds",3,0.88,"err:error",0,900,"err:error",0,900,"???",0,900]
["valid","large","cruise_controller_13",{"$nulls":6},"--","--","--","holds",3,0.23,"holds",3,0.75,"holds",3,0.92,"err:error",0,900,"err:error",0,900,"???",0,900]
["valid","memory1","DRAGON_1",{"$nulls":6},"--","--","--","holds",3,0.1,"holds",3,0.39,"holds",3,0.51,"holds",1,0.27,"holds",1,0.17,"cex",0,900]
["valid","memory1","DRAGON_1_e1_3184",{"$nulls":6},"--","--","--","holds",3,0.1,"holds",3,0.34,"holds",3,0.56,"holds",1,0.31,"holds",1,0.15,"cex",0,900]
["valid","memory1","DRAGON_1_e1_5070",{"$nulls":6},"--","--","--","holds",3,0.1,"holds",3,0.35,"holds",3,0.52,"holds",1,0.3,"holds",1,0.17,"cex",0,900]
["valid","memory1","DRAGON_1_e2_1997",{"$nulls":6},"--","--","--","holds",3,0.1,"holds",3,0.32,"holds",3,0.59,"holds",1,0.28,"holds",1,0.17,"cex",0,900]
["valid","memory1","DRAGON_10",{"$nulls":6},"--","--","--","holds",3,0.1,"holds",3,0.21,"holds",3,0.5,"timeout",0,900,"holds",1,0.24,"cex",0,900]
["valid","memory1","DRAGON_10_e1_3587_e3_2749",{"$nulls":6},"--","--","--","holds",3,0.09,"holds",3,0.22,"holds",3,0.54,"timeout",0,900,"holds",1,0.24,"cex",0,900]
["valid","memory1","DRAGON_10_e1_998",{"$nulls":6},"--","--","--","holds",3,0.09,"holds",3,0.23,"holds",3,0.51,"timeout",0,900,"holds",1,0.24,"cex",0,900]
["valid","memory1","DRAGON_10_e2_2785_e3_1744",{"$nulls":6},"--","--","--","holds",3,0.11,"holds",3,0.22,"holds",3,0.55,"timeout",0,900,"holds",1,0.25,"cex",0,900]
["valid","memory1","DRAGON_10_e2_402",{"$nulls":6},"--","--","--","holds",3,0.1,"holds",3,0.23,"holds",3,0.54,"timeout",0,900,"holds",1,0.25,"cex",0,900]
["valid","memory1","DRAGON_10_e3_144_e5_2046",{"$nulls":6},"--","--","--","holds",3,0.1,"holds",3,0.21,"holds",3,0.56,"timeout",0,900,"holds",1,0.24,"cex",0,900]
["valid","memory1","DRAGON_10_e3_144_e6_4484",{"$nulls":6},"--","--","--","holds",3,0.09,"holds",3,0.21,"holds",3,0.5,"timeout",0,900,"holds",1,0.22,"cex",0,900]
["valid","memory1","DRAGON_10_e3_3429",{"$nulls":6},"--","--","--","holds",3,0.1,"holds",3,0.21,"holds",3,0.56,"timeout",0,900,"holds",1,0.25,"cex",0,900]
["valid","memory1","DRAGON_10_e7_3861_e8_3524",{"$nulls":6},"--","--","--","holds",3,0.1,"holds",3,0.23,"holds",3,0.53,"timeout",0,900,"holds",1,0.23,"cex",0,900]
["valid","memory1","DRAGON_2",{"$nulls":6},"--","--","--","holds",3,0.12,"holds",3,0.24,"holds",3,0.6,"timeout",0,900,"holds",1,3.23,"cex",0,900]
["valid","memory1","DRAGON_2_e1_2316",{"$nulls":6},"--","--","--","holds",3,0.11,"holds",3,0.23,"holds",3,0.54,"timeout",0,900,"holds",1,3.3,"cex",0,900]
["valid","memory1","DRAGON_2_e2_3183",{"$nulls":6},"--","--","--","holds",3,0.12,"holds",3,0.22,"holds",3,0.62,"timeout",0,900,"holds",1,3.31,"cex",0,900]
["valid","memory1","DRAGON_2_e2_3183_e1_2644",{"$nulls":6},"--","--","--","holds",3,0.12,"holds",3,0.22,"holds",3,0.57,"timeout",0,900,"holds",1,3.16,"cex",0,900]
["valid","memory1","DRAGON_2_e2_3183_e2_3580",{"$nulls":6},"--","--","--","holds",3,0.12,"holds",3,0.23,"holds",3,0.6,"timeout",0,900,"holds",1,3.11,"cex",0,900]
["valid","memory1","DRAGON_2_e2_3183_e3_5972",{"$nulls":6},"--","--","--","holds",3,0.11,"holds",3,0.22,"holds",3,0.56,"timeout",0,900,"holds",1,3.12,"cex",0,900]
["valid","memory1","DRAGON_2_e2_4481",{"$nulls":6},"--","--","--","holds",3,0.12,"holds",3,0.22,"holds",3,0.61,"timeout",0,900,"holds",1,3.34,"cex",0,900]
["valid","memory1","DRAGON_2_e7_25_e8_3171",{"$nulls":6},"--","--","--","holds",3,0.12,"holds",3,0.22,"holds",3,0.62,"timeout",0,900,"holds",1,3.16,"cex",0,900]
["valid","memory1","DRAGON_3",{"$nulls":6},"--","--","--","holds",3,0.12,"holds",3,0.26,"holds",3,0.61,"timeout",0,900,"holds",1,4.7,"cex",0,900]
["valid","memory1","DRAGON_3_e1_4783",{"$nulls":6},"--","--","--","holds",3,0.12,"holds",3,0.23,"holds",3,0.62,"timeout",0,900,"holds",1,4.39,"cex",0,900]
["valid","memory1","DRAGON_3_e1_4783_e1_3755",{"$nulls":6},"--","--","--","holds",3,0.12,"holds",3,0.22,"holds",3,0.6,"timeout",0,900,"holds",1,4.34,"cex",0,900]
["valid","memory1","DRAGON_3_e1_4783_e2_158",{"$nulls":6},"--","--","--","holds",3,0.12,"holds",3,0.24,"holds",3,0.62,"timeout",0,900,"holds",1,4.68,"cex",0,900]
["valid","memory1","DRAGON_3_e1_4783_e3_511",{"$nulls":6},"--","--","--","holds",3,0.14,"holds",3,0.24,"holds",3,0.63,"timeout",0,900,"holds",1,4.71,"cex",0,900]
["valid","memory1","DRAGON_3_e2_5343_e1_988",{"$nulls":6},"--","--","--","holds",3,0.12,"holds",3,0.24,"holds",3,0.56,"timeout",0,900,"holds",1,4.64,"cex",0,900]
["valid","memory1","DRAGON_3_e3_3846",{"$nulls":6},"--","--","--","holds",3,0.14,"holds",3,0.25,"holds",3,0.61,"timeout",0,900,"holds",1,5.04,"cex",0,900]
["valid","memory1","DRAGON_3_e3_5422_e1_2288",{"$nulls":6},"--","--","--","holds",3,0.13,"holds",3,0.24,"holds",3,0.61,"timeout",0,900,"holds",1,4.54,"cex",0,900]
["valid","memory1","DRAGON_3_e3_5422_e2_3135",{"$nulls":6},"--","--","--","holds",3,0.12,"holds",3,0.26,"holds",3,0.6,"timeout",0,900,"holds",1,4.34,"cex",0,900]
["valid","memory1","DRAGON_6",{"$nulls":6},"--","--","--","holds",3,0.09,"holds",3,0.36,"holds",3,0.52,"holds",1,0.28,"holds",1,0.16,"cex",0,900]
["valid","memory1","DRAGON_7",{"$nulls":6},"--","--","--","holds",3,0.1,"holds",3,0.37,"holds",3,0.54,"timeout",0,900,"holds",1,0.63,"cex",0,900]
["valid","memory1","DRAGON_7_e2_2872_e2_5844",{"$nulls":6},"--","--","--","holds",3,0.1,"holds",3,0.41,"holds",3,0.55,"timeout",0,900,"holds",1,0.54,"cex",0,900]
["valid","memory1","DRAGON_7_e2_2872_e3_2640",{"$nulls":6},"--","--","--","holds",3,0.1,"holds",3,0.41,"holds",3,0.57,"timeout",0,900,"holds",1,0.51,"cex",0,900]
["valid","memory1","DRAGON_9",{"$nulls":6},"--","--","--","holds",3,0.09,"holds",3,0.33,"holds",3,0.5,"timeout",0,900,"holds",1,0.24,"cex",0,900]
["valid","memory1","DRAGON_9_e7_1843_e8_3031",{"$nulls":6},"--","--","--","holds",3,0.09,"holds",3,0.33,"holds",3,0.53,"timeout",0,900,"holds",1,0.2,"cex",0,900]
["valid","memory1","DRAGON_all",{"$nulls":6},"--","--","--","holds",3,0.13,"holds",3,0.28,"holds",3,0.62,"timeout",0,900,"holds",1,10.26,"cex",0,900]
["valid","memory1","DRAGON_all_e1_4022",{"$nulls":6},"--","--","--","holds",3,0.14,"holds",3,0.3,"holds",3,0.66,"timeout",0,900,"holds",1,9.63,"cex",0,900]
["valid","memory1","DRAGON_all_e1_4022_e1_1759",{"$nulls":6},"--","--","--","holds",3,0.14,"holds",3,0.27,"holds",3,0.65,"timeout",0,900,"holds",1,10.2,"cex",0,900]
["valid","memory1","DRAGON_all_e1_4022_e2_267",{"$nulls":6},"--","--","--","holds",3,0.13,"holds",3,0.28,"holds",3,0.65,"timeout",0,900,"holds",1,9.97,"cex",0,900]
["valid","memory1","DRAGON_all_e1_4022_e3_3628",{"$nulls":6},"--","--","--","holds",3,0.13,"holds",3,0.29,"holds",3,0.67,"timeout",0,900,"holds",1,10.06,"cex",0,900]
["valid","memory1","DRAGON_all_e1_4037",{"$nulls":6},"--","--","--","holds",3,0.14,"holds",3,0.54,"holds",3,0.69,"timeout",0,900,"holds",1,9.66,"cex",0,900]
["valid","memory1","DRAGON_all_e2_1514",{"$nulls":6},"--","--","--","holds",3,0.12,"holds",3,0.28,"holds",3,0.59,"timeout",0,900,"holds",1,10.19,"cex",0,900]
["valid","memory1","DRAGON_all_e2_6104",{"$nulls":6},"--","--","--","holds",3,0.12,"holds",3,0.27,"holds",3,0.64,"timeout",0,900,"holds",1,10.16,"cex",0,900]
["valid","memory1","DRAGON_all_e2_6104_e1_6205",{"$nulls":6},"--","--","--","holds",3,0.13,"holds",3,0.54,"holds",3,0.63,"timeout",0,900,"holds",1,10.07,"cex",0,900]
["valid","memory1","DRAGON_all_e2_6104_e2_3308",{"$nulls":6},"--","--","--","holds",3,0.12,"holds",3,0.38,"holds",3,0.64,"timeout",0,900,"holds",1,9.67,"cex",0,900]
["valid","memory1","DRAGON_all_e2_6104_e3_2607",{"$nulls":6},"--","--","--","holds",3,0.14,"holds",3,0.29,"holds",3,0.58,"timeout",0,900,"holds",1,10.18,"cex",0,900]
["valid","memory1","DRAGON_all_e3_4821",{"$nulls":6},"--","--","--","holds",3,0.14,"holds",3,0.3,"holds",3,0.61,"timeout",0,900,"holds",1,9.85,"cex",0,900]
["valid","memory1","DRAGON_all_e3_4821_e1_1318",{"$nulls":6},"--","--","--","holds",3,0.14,"holds",3,0.29,"holds",3,0.67,"timeout",0,900,"holds",1,9.86,"cex",0,900]
["valid","memory1","DRAGON_all_e3_4821_e2_1089",{"$nulls":6},"--","--","--","holds",3,0.14,"holds",3,0.31,"holds",3,0.65,"timeout",0,900,"holds",1,10.13,"cex",0,900]
["valid","memory1","DRAGON_all_e3_4821_e4_1791",{"$nulls":6},"--","--","--","holds",3,0.14,"holds",3,0.29,"holds",3,0.61,"timeout",0,900,"holds",1,9.84,"cex",0,900]
["valid","memory1","DRAGON_all_e3_4821_e5_1536",{"$nulls":6},"--","--","--","holds",3,0.13,"holds",3,0.31,"holds",3,0.62,"timeout",0,900,"holds",1,10.03,"cex",0,900]
["valid","memory1","DRAGON_all_e3_4821_e6_2061",{"$nulls":6},"--","--","--","holds",3,0.13,"holds",3,0.28,"holds",3,0.64,"timeout",0,900,"holds",1,10.1,"cex",0,900]
["valid","memory1","DRAGON_all_e3_5957",{"$nulls":6},"--","--","--","holds",3,0.14,"holds",3,0.28,"holds",3,0.61,"timeout",0,900,"holds",1,9.94,"cex",0,900]
["valid","memory1","DRAGON_all_e7_1941_e8_2826",{"$nulls":6},"--","--","--","holds",3,0.13,"holds",3,0.28,"holds",3,0.62,"timeout",0,900,"holds",1,10.11,"cex",0,900]
["valid","misc","durationThm_1_e2_3",{"$nulls":6},"--","--","--","holds*",8,0.14,"holds*",9,0.41,"holds",3,0.33,"cex",2,900,"holds",4,0.19,"cex",0,900]
["valid","misc","durationThm_1_e2_3_e7_336",{"$nulls":6},"--","--","--","holds*",8,0.15,"holds*",14,1.01,"holds",6,0.77,"cex",2,900,"holds",9,5.27,"cex",0,900]
["valid","misc","durationThm_1_e2_305",{"$nulls":6},"--","--","--","holds*",8,0.14,"holds*",9,0.36,"holds",3,0.35,"cex",2,900,"holds",4,0.19,"cex",0,900]
["valid","misc","durationThm_1_e3_389_e4_294",{"$nulls":6},"--","--","--","holds*",8,0.15,"holds*",9,0.36,"holds",3,0.3,"cex",2,900,"holds",4,0.19,"cex",0,900]
["valid","misc","durationThm_1_e7_217_e2_352",{"$nulls":6},"--","--","--","holds*",8,0.15,"holds*",14,1.06,"holds",6,0.75,"cex",2,900,"holds",9,5.21,"cex",0,900]
["valid","misc","durationThm_2_e2_206",{"$nulls":6},"--","--","--","holds",6,0.08,"holds*",6,0.21,"holds",3,0.29,"holds",2,5.87,"holds",2,0.04,"cex",0,900]
["valid","misc","durationThm_2_e2_206_e7_33",{"$nulls":6},"--","--","--","holds*",8,0.14,"holds*",14,0.95,"holds",6,0.75,"holds",10,16.27,"holds",10,4.34,"cex",0,900]
["valid","misc","durationThm_2_e2_63",{"$nulls":6},"--","--","--","holds",6,0.09,"holds*",6,0.21,"holds",3,0.3,"holds",2,5.81,"holds",2,0.06,"cex",0,900]
["valid","misc","durationThm_2_e3_329_e4_1",{"$nulls":6},"--","--","--","holds",6,0.09,"holds*",6,0.21,"holds",3,0.28,"holds",2,0.11,"holds",2,0.06,"cex",0,900]
["valid","misc","durationThm_2_e7_145_e2_169",{"$nulls":6},"--","--","--","holds*",8,0.14,"holds*",14,0.96,"holds",6,0.72,"holds",10,16.39,"holds",10,4.33,"cex",0,900]
["valid","misc","durationThm_3_e2_148",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.06,"holds",3,0.32,"cex",1,900,"holds",1,0.01,"cex",0,900]
["valid","misc","durationThm_3_e2_63",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.06,"holds",3,0.28,"cex",1,900,"holds",1,0.01,"cex",0,900]
["valid","misc","durationThm_3_e2_63_e7_21",{"$nulls":6},"--","--","--","holds*",8,0.16,"holds*",8,0.28,"holds",6,0.74,"cex",1,900,"holds",5,0.5,"cex",0,900]
["valid","misc","durationThm_3_e3_207",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.06,"holds",3,0.31,"cex",1,900,"holds",1,0.05,"cex",0,900]
["valid","misc","durationThm_3_e3_442",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.06,"holds",3,0.28,"cex",1,900,"holds",1,0.05,"cex",0,900]
["valid","misc","durationThm_3_e3_442_e4_165",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.05,"holds",3,0.28,"cex",1,900,"holds",1,0.05,"cex",0,900]
["valid","misc","durationThm_3_e3_442_e5_260",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.06,"holds",3,0.33,"cex",1,900,"holds",1,0.05,"cex",0,900]
["valid","misc","durationThm_3_e7_334_e2_62",{"$nulls":6},"--","--","--","holds*",8,0.15,"holds*",8,0.28,"holds",6,0.74,"cex",1,900,"holds",5,0.5,"cex",0,900]
["valid","misc","ex3",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.13,"holds",3,0.27,"timeout",0,900,"holds",1,0.02,"cex",0,900]
["valid","misc","ex3_e7_590",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.12,"holds",3,0.31,"timeout",0,900,"holds",1,0.04,"cex",0,900]
["valid","misc","ex3_e7_590_e7_590",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.12,"holds",3,0.27,"timeout",0,900,"holds",1,0.05,"cex",0,900]
["valid","misc","ex3_e7_590_e8_550",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.13,"holds",3,0.3,"timeout",0,900,"holds",1,0.01,"cex",0,900]
["valid","misc","ex3_e7_655",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.12,"holds",3,0.27,"timeout",0,900,"holds",1,0.02,"cex",0,900]
["valid","misc","ex3_e8_120",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.12,"holds",3,0.29,"holds",1,0.04,"holds",1,0.03,"cex",0,900]
["valid","misc","ex3_e8_381",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.13,"holds",3,0.3,"holds",1,0.04,"holds",1,0.04,"cex",0,900]
["valid","misc","ex3_e8_381_e7_224",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.12,"holds",3,0.27,"timeout",0,900,"holds",1,0.04,"cex",0,900]
["valid","misc","ex3_e8_381_e8_477",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.07,"holds",3,0.32,"holds",2,0.05,"holds",2,0.05,"cex",0,900]
["valid","simulation","fast_1",{"$nulls":6},"--","--","--","holds",3,0.04,"holds",3,0.32,"holds",3,0.33,"holds",1,0.03,"holds",1,0.06,"holds",0,1.41]
["valid","simulation","fast_1_e7_2044_e8_1396",{"$nulls":6},"--","--","--","holds",3,0.04,"holds",3,0.35,"holds",3,0.34,"holds",1,0.02,"holds",1,0.06,"holds",0,1.41]
["valid","simulation","fast_1_e8_747",{"$nulls":6},"--","--","--","holds",3,0.04,"holds",3,0.34,"holds",3,0.32,"holds",1,0.04,"holds",1,0.02,"holds",0,0.33]
["valid","simulation","fast_1_e8_747_e8_1041",{"$nulls":6},"--","--","--","holds",3,0.04,"holds",3,0.24,"holds",3,0.35,"holds",1,0.02,"holds",1,0.06,"holds",0,0.12]
["valid","simulation","fast_1_e8_751",{"$nulls":6},"--","--","--","holds",3,0.04,"holds",3,0.32,"holds",3,0.31,"holds",1,0.02,"holds",1,0.04,"holds",0,0.33]
["valid","simulation","fast_2",{"$nulls":6},"--","--","--","holds",3,0.06,"holds",3,0.49,"holds",3,0.33,"holds",1,0.04,"holds",1,0.03,"holds",0,1.12]
["valid","simulation","fast_2_e7_2526_e8_1145",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.54,"holds",3,0.36,"holds",1,0.03,"holds",1,0.03,"holds",0,1.13]
["valid","simulation","fast_2_e8_460",{"$nulls":6},"--","--","--","holds",3,0.06,"holds",3,0.49,"holds",3,0.34,"holds",1,0.03,"holds",1,0.06,"holds",0,0.33]
["valid","simulation","fast_2_e8_460_e8_1920",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.49,"holds",3,0.37,"holds",1,0.03,"holds",1,0.03,"holds",0,0.13]
["valid","simulation","fast_2_e8_976",{"$nulls":6},"--","--","--","holds",3,0.06,"holds",3,0.49,"holds",3,0.34,"holds",1,0.04,"holds",1,0.06,"holds",0,0.33]
["valid","memory1","FIREFLY_1",{"$nulls":6},"--","--","--","holds",3,0.08,"holds",3,0.15,"holds",3,0.45,"timeout",0,900,"holds",1,1.13,"cex",0,900]
["valid","memory1","FIREFLY_1_e1_1092_e2_1853",{"$nulls":6},"--","--","--","holds",3,0.08,"holds",3,0.15,"holds",3,0.47,"timeout",0,900,"holds",1,1.12,"cex",0,900]
["valid","memory1","FIREFLY_10",{"$nulls":6},"--","--","--","holds",3,0.07,"holds",3,0.24,"holds",3,0.43,"timeout",0,900,"holds",1,0.08,"cex",0,900]
["valid","memory1","FIREFLY_2",{"$nulls":6},"--","--","--","holds",3,0.07,"holds",3,0.16,"holds",3,0.46,"timeout",0,900,"holds",1,1.74,"cex",0,900]
["valid","memory1","FIREFLY_2_e1_3099_e2_846",{"$nulls":6},"--","--","--","holds",3,0.08,"holds",3,0.18,"holds",3,0.47,"timeout",0,900,"holds",1,1.75,"cex",0,900]
["valid","memory1","FIREFLY_3",{"$nulls":6},"--","--","--","holds",3,0.06,"holds",3,0.26,"holds",3,0.41,"timeout",0,900,"holds",1,0.22,"cex",0,900]
["valid","memory1","FIREFLY_3_e2_2236",{"$nulls":6},"--","--","--","holds",3,0.06,"holds",3,0.23,"holds",3,0.42,"timeout",0,900,"holds",1,0.22,"cex",0,900]
["valid","memory1","FIREFLY_3_e2_2236_e1_2305",{"$nulls":6},"--","--","--","holds",3,0.06,"holds",3,0.25,"holds",3,0.49,"timeout",0,900,"holds",1,0.25,"cex",0,900]
["valid","memory1","FIREFLY_3_e2_2236_e2_1058",{"$nulls":6},"--","--","--","holds",3,0.06,"holds",3,0.25,"holds",3,0.47,"timeout",0,900,"holds",1,0.25,"cex",0,900]
["valid","memory1","FIREFLY_4",{"$nulls":6},"--","--","--","holds",3,0.07,"holds",3,0.16,"holds",3,0.41,"timeout",0,900,"holds",1,0.93,"cex",0,900]
["valid","memory1","FIREFLY_4_e3_3511_e6_1826",{"$nulls":6},"--","--","--","holds",3,0.07,"holds",3,0.4,"holds",3,0.46,"timeout",0,900,"holds",1,0.92,"cex",0,900]
["valid","memory1","FIREFLY_5",{"$nulls":6},"--","--","--","holds",3,0.06,"holds",3,0.24,"holds",3,0.45,"timeout",0,900,"holds",1,0.12,"cex",0,900]
["valid","memory1","FIREFLY_5_e2_2229",{"$nulls":6},"--","--","--","holds",3,0.06,"holds",3,0.24,"holds",3,0.46,"timeout",0,900,"holds",1,0.15,"cex",0,900]
["valid","memory1","FIREFLY_5_e2_2884",{"$nulls":6},"--","--","--","holds",3,0.07,"holds",3,0.22,"holds",3,0.38,"timeout",0,900,"holds",1,0.11,"cex",0,900]
["valid","memory1","FIREFLY_5_e2_2884_e1_2678",{"$nulls":6},"--","--","--","holds",3,0.06,"holds",3,0.24,"holds",3,0.42,"timeout",0,900,"holds",1,0.15,"cex",0,900]
["valid","memory1","FIREFLY_5_e2_2884_e2_1492",{"$nulls":6},"--","--","--","holds",3,0.06,"holds",3,0.27,"holds",3,0.42,"timeout",0,900,"holds",1,0.12,"cex",0,900]
["valid","memory1","FIREFLY_5_e2_2884_e3_1882",{"$nulls":6},"--","--","--","holds",3,0.06,"holds",3,0.22,"holds",3,0.45,"timeout",0,900,"holds",1,0.15,"cex",0,900]
["valid","memory1","FIREFLY_8",{"$nulls":6},"--","--","--","holds",3,0.06,"holds",3,0.15,"holds",3,0.41,"holds",1,0.18,"holds",1,0.09,"cex",0,900]
["valid","memory1","FIREFLY_8_e2_1692",{"$nulls":6},"--","--","--","holds",3,0.06,"holds",3,0.16,"holds",3,0.45,"holds",1,0.19,"holds",1,0.12,"cex",0,900]
["valid","memory1","FIREFLY_8_e2_1711",{"$nulls":6},"--","--","--","holds",3,0.06,"holds",3,0.15,"holds",3,0.4,"holds",1,0.17,"holds",1,0.1,"cex",0,900]
["valid","memory1","FIREFLY_8_e2_1711_e1_1489",{"$nulls":6},"--","--","--","holds",3,0.06,"holds",3,0.16,"holds",3,0.44,"holds",1,0.19,"holds",1,0.09,"cex",0,900]
["valid","memory1","FIREFLY_8_e2_1711_e2_2673",{"$nulls":6},"--","--","--","holds",3,0.06,"holds",3,0.19,"holds",3,0.43,"holds",1,0.19,"holds",1,0.12,"cex",0,900]
["valid","memory1","FIREFLY_8_e2_1711_e3_1753",{"$nulls":6},"--","--","--","holds",3,0.07,"holds",3,0.15,"holds",3,0.46,"holds",1,0.18,"holds",1,0.11,"cex",0,900]
["valid","memory1","FIREFLY_9",{"$nulls":6},"--","--","--","holds",3,0.07,"holds",3,0.24,"holds",3,0.4,"holds",1,0.56,"holds",1,0.56,"cex",0,900]
["valid","memory1","FIREFLY_a3",{"$nulls":6},"--","--","--","holds",3,0.09,"holds",3,0.23,"holds",3,0.48,"timeout",0,900,"holds",1,1.41,"cex",0,900]
["valid","memory1","FIREFLY_a3_e1_3233_e2_2392",{"$nulls":6},"--","--","--","holds",3,0.09,"holds",3,0.21,"holds",3,0.46,"timeout",0,900,"holds",1,1.44,"cex",0,900]
["valid","memory1","FIREFLY_a3_e1_3233_e3_2970",{"$nulls":6},"--","--","--","holds",3,0.09,"holds",3,0.21,"holds",3,0.49,"timeout",0,900,"holds",1,1.43,"cex",0,900]
["valid","memory1","FIREFLY_a3_e2_2086",{"$nulls":6},"--","--","--","holds",3,0.08,"holds",3,0.21,"holds",3,0.43,"timeout",0,900,"holds",1,1.46,"cex",0,900]
["valid","memory1","FIREFLY_a3_e2_2086_e1_3235",{"$nulls":6},"--","--","--","holds",3,0.09,"holds",3,0.23,"holds",3,0.5,"timeout",0,900,"holds",1,1.4,"cex",0,900]
["valid","memory1","FIREFLY_a3_e2_2086_e2_2689",{"$nulls":6},"--","--","--","holds",3,0.08,"holds",3,0.21,"holds",3,0.45,"timeout",0,900,"holds",1,1.44,"cex",0,900]
["valid","memory1","FIREFLY_a3_e2_2086_e3_2542",{"$nulls":6},"--","--","--","holds",3,0.08,"holds",3,0.21,"holds",3,0.44,"timeout",0,900,"holds",1,1.44,"cex",0,900]
["valid","memory1","FIREFLY_a3_e2_2952",{"$nulls":6},"--","--","--","holds",3,0.08,"holds",3,0.21,"holds",3,0.43,"timeout",0,900,"holds",1,1.43,"cex",0,900]
["valid","memory1","FIREFLY_a3_e3_314_e2_2812",{"$nulls":6},"--","--","--","holds",3,0.08,"holds",3,0.23,"holds",3,0.48,"timeout",0,900,"holds",1,1.45,"cex",0,900]
["valid","memory1","FIREFLY_all",{"$nulls":6},"--","--","--","holds",3,0.08,"holds",3,0.21,"holds",3,0.51,"timeout",0,900,"holds",1,5.38,"cex",0,900]
["valid","memory1","FIREFLY_all_e1_1207_e2_3220",{"$nulls":6},"--","--","--","holds",3,0.08,"holds",3,0.2,"holds",3,0.52,"timeout",0,900,"holds",1,5.33,"cex",0,900]
["valid","memory1","FIREFLY_all_e2_2924_e1_768",{"$nulls":6},"--","--","--","holds",3,0.08,"holds",3,0.2,"holds",3,0.48,"timeout",0,900,"holds",1,5.31,"cex",0,900]
["valid","memory1","FIREFLY_all_e3_1600_e6_1569",{"$nulls":6},"--","--","--","holds",3,0.08,"holds",3,0.2,"holds",3,0.5,"timeout",0,900,"holds",1,5.25,"cex",0,900]
["valid","memory1","FIREFLY_all_e7_2052_e8_631",{"$nulls":6},"--","--","--","holds",3,0.08,"holds",3,0.21,"holds",3,0.5,"timeout",0,900,"holds",1,5.33,"cex",0,900]
["valid","memory1","FIREFLY_luke_1b",{"$nulls":6},"--","--","--","holds",3,0.07,"holds",3,0.15,"holds",3,0.49,"timeout",0,900,"holds",1,1.08,"cex",0,900]
["valid","memory1","FIREFLY_luke_1b_e1_1139_e2_2893",{"$nulls":6},"--","--","--","holds",3,0.07,"holds",3,0.15,"holds",3,0.42,"timeout",0,900,"holds",1,1.06,"cex",0,900]
["valid","memory1","FIREFLY_luke_1b_e2_3049_e1_946",{"$nulls":6},"--","--","--","holds",3,0.07,"holds",3,0.15,"holds",3,0.44,"timeout",0,900,"holds",1,1.05,"cex",0,900]
["valid","memory1","FIREFLY_luke_1b_e3_671_e6_1974",{"$nulls":6},"--","--","--","holds",3,0.07,"holds",3,0.17,"holds",3,0.47,"timeout",0,900,"holds",1,1.05,"cex",0,900]
["valid","memory1","FIREFLY_luke_1b_e7_3191_e8_2830",{"$nulls":6},"--","--","--","holds",3,0.08,"holds",3,0.15,"holds",3,0.49,"timeout",0,900,"holds",1,1.09,"cex",0,900]
["valid","memory1","FIREFLY_luke_rt",{"$nulls":6},"--","--","--","holds",3,0.08,"holds",3,0.17,"holds",3,0.42,"timeout",0,900,"holds",1,1.78,"cex",0,900]
["valid","memory1","FIREFLY_luke_rt_e1_913_e2_3353",{"$nulls":6},"--","--","--","holds",3,0.08,"holds",3,0.17,"holds",3,0.45,"timeout",0,900,"holds",1,1.71,"cex",0,900]
["valid","memory1","FIREFLY_luke_rt_e2_3460_e1_1455",{"$nulls":6},"--","--","--","holds",3,0.07,"holds",3,0.18,"holds",3,0.49,"timeout",0,900,"holds",1,1.76,"cex",0,900]
["valid","simulation","hysteresis_1",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.13,"holds",3,0.31,"holds",0,0.04,"holds",0,0.04,"holds",0,0.04]
["valid","simulation","hysteresis_2",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.12,"holds",3,0.3,"holds",1,0.03,"holds",1,0.01,"cex",0,900]
["valid","simulation","hysteresis_3",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.12,"holds",3,0.32,"holds",1,0.03,"holds",1,0.01,"cex",0,900]
["valid","simulation","hysteresis_all",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.13,"holds",3,0.31,"holds",1,0.04,"holds",1,0.05,"cex",0,900]
["valid","memory2","ILLINOIS_1",{"$nulls":6},"--","--","--","holds",3,0.07,"holds",3,0.23,"holds",3,0.43,"holds",1,0.2,"holds",1,0.09,"cex",0,900]
["valid","memory2","ILLINOIS_2",{"$nulls":6},"--","--","--","holds",3,0.09,"holds",3,0.15,"holds",3,0.46,"timeout",0,900,"holds",1,2.41,"cex",0,900]
["valid","memory2","ILLINOIS_2_e1_834_e2_3395",{"$nulls":6},"--","--","--","holds",3,0.09,"holds",3,0.16,"holds",3,0.45,"timeout",0,900,"holds",1,2.4,"cex",0,900]
["valid","memory2","ILLINOIS_2_e2_2367_e1_3182",{"$nulls":6},"--","--","--","holds",3,0.09,"holds",3,0.15,"holds",3,0.45,"timeout",0,900,"holds",1,2.35,"cex",0,900]
["valid","memory2","ILLINOIS_2_e3_1554_e6_2223",{"$nulls":6},"--","--","--","holds",3,0.09,"holds",3,0.16,"holds",3,0.42,"timeout",0,900,"holds",1,2.39,"cex",0,900]
["valid","memory2","ILLINOIS_3",{"$nulls":6},"--","--","--","holds",3,0.09,"holds",3,0.16,"holds",3,0.49,"timeout",0,900,"holds",1,2.36,"cex",0,900]
["valid","memory2","ILLINOIS_3_e3_2581_e6_2476",{"$nulls":6},"--","--","--","holds",3,0.09,"holds",3,0.16,"holds",3,0.46,"timeout",0,900,"holds",1,2.29,"cex",0,900]
["valid","memory2","ILLINOIS_4",{"$nulls":6},"--","--","--","holds",3,0.07,"holds",3,0.25,"holds",3,0.46,"timeout",0,900,"holds",1,0.1,"cex",0,900]
["valid","memory2","ILLINOIS_5",{"$nulls":6},"--","--","--","holds",3,0.07,"holds",3,0.26,"holds",3,0.43,"holds",1,0.23,"holds",1,0.12,"cex",0,900]
["valid","memory2","ILLINOIS_all",{"$nulls":6},"--","--","--","holds",3,0.09,"holds",3,0.2,"holds",3,0.49,"timeout",0,900,"holds",1,4.41,"cex",0,900]
["valid","memory2","ILLINOIS_all_e3_2354_e6_993",{"$nulls":6},"--","--","--","holds",3,0.09,"holds",3,0.2,"holds",3,0.52,"timeout",0,900,"holds",1,4.27,"cex",0,900]
["valid","memory2","MESI_1",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.12,"holds",3,0.36,"holds",1,0.14,"holds",1,0.08,"cex",0,900]
["valid","memory2","MESI_1_e2_162_e7_1545",{"$nulls":6},"--","--","--","holds*",11,2.07,"holds*",11,3.84,"timeout",69,900,"timeout",0,900,"timeout",0,900,"cex",0,900]
["valid","memory2","MESI_2",{"$nulls":6},"--","--","--","holds",3,0.04,"holds",3,0.14,"holds",3,0.37,"holds",1,0.13,"holds",1,0.05,"cex",0,900]
["valid","memory2","MESI_3",{"$nulls":6},"--","--","--","holds",3,0.09,"holds",3,0.19,"holds",3,0.47,"timeout",0,900,"timeout",0,900,"cex",0,900]
["valid","memory2","MESI_3_e1_2517_e8_2163",{"$nulls":6},"--","--","--","holds",3,0.11,"holds",3,0.2,"holds",3,0.47,"timeout",0,900,"timeout",0,900,"cex",0,900]
["valid","memory2","MESI_3_e2_819_e1_1145",{"$nulls":6},"--","--","--","holds",3,0.09,"holds",3,0.21,"holds",3,0.48,"timeout",0,900,"timeout",0,900,"cex",0,900]
["valid","memory2","MESI_3_e2_819_e4_1595",{"$nulls":6},"--","--","--","holds",3,0.09,"holds",3,0.19,"holds",3,0.52,"timeout",0,900,"timeout",0,900,"cex",0,900]
["valid","memory2","MESI_3_e2_819_e6_1459",{"$nulls":6},"--","--","--","holds",3,0.09,"holds",3,0.2,"holds",3,0.45,"timeout",0,900,"timeout",0,900,"cex",0,900]
["valid","memory2","MESI_3_e3_2584",{"$nulls":6},"--","--","--","holds",3,0.12,"holds",3,0.27,"holds",3,0.49,"timeout",0,900,"timeout",0,900,"cex",0,900]
["valid","memory2","MESI_3_e3_2669",{"$nulls":6},"--","--","--","holds",3,0.12,"holds",3,0.25,"holds",3,0.49,"timeout",0,900,"timeout",0,900,"cex",0,900]
["valid","memory2","MESI_4",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.13,"holds",3,0.35,"holds",1,0.13,"holds",1,0.09,"cex",0,900]
["valid","memory2","MESI_4_e7_1140_e7_433",{"$nulls":6},"--","--","--","holds*",11,1.73,"holds*",11,3.05,"timeout",75,900,"timeout",0,900,"timeout",0,900,"cex",0,900]
["valid","memory2","MESI_all",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.14,"holds",3,0.36,"holds",1,0.15,"holds",1,0.07,"cex",0,900]
["valid","memory2","MESI_all_e4_1147_e7_497",{"$nulls":6},"--","--","--","holds*",11,2.3,"holds*",11,5.35,"timeout",69,900,"timeout",0,900,"timeout",0,900,"cex",0,900]
["valid","memory2","MESI_i3_e1_447_e1_1292",{"$nulls":6},"--","--","--","holds*",17,17.05,"holds*",17,41.25,"timeout",72,900,"timeout",0,900,"timeout",0,900,"cex",0,900]
["valid","memory2","MESI_i3_e1_447_e3_1180",{"$nulls":6},"--","--","--","holds*",14,5.65,"holds*",14,14.12,"timeout",81,900,"timeout",0,900,"timeout",0,900,"cex",0,900]
["valid","memory2","MESI_i4_e6_2175",{"$nulls":6},"--","--","--","holds*",17,88.84,"holds*",17,136.88,"timeout",57,900,"timeout",0,900,"timeout",0,900,"cex",0,900]
["valid","memory2","MESI_i4_e7_1017_e6_1132",{"$nulls":6},"--","--","--","holds*",17,101.21,"holds*",17,138.38,"timeout",57,900,"timeout",0,900,"timeout",0,900,"cex",0,900]
["valid","simulation","metros_1",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.09,"holds",3,0.37,"holds",2,1.33,"holds",2,0.37,"cex",0,900]
["valid","simulation","metros_1_e1_846_e1_1317",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.09,"holds",3,0.35,"timeout",0,900,"holds",2,0.37,"cex",0,900]
["valid","simulation","metros_1_e1_846_e2_1394",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.09,"holds",3,0.35,"holds",2,0.22,"holds",2,0.26,"cex",0,900]
["valid","simulation","metros_1_e1_846_e3_1060",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.09,"holds",3,0.35,"holds",2,2.27,"holds",2,0.37,"cex",0,900]
["valid","simulation","metros_1_e1_846_e7_397",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.09,"holds",3,0.38,"timeout",0,900,"holds",2,1.25,"cex",0,900]
["valid","simulation","metros_1_e1_846_e8_1253",{"$nulls":6},"--","--","--","holds",3,0.04,"holds",3,0.09,"holds",3,0.38,"holds",1,0.07,"holds",1,0.06,"holds",0,0.11]
["valid","simulation","metros_1_e2_1102",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.09,"holds",3,0.35,"holds",2,0.17,"holds",2,0.29,"cex",0,900]
["valid","simulation","metros_1_e2_1102_e1_317",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.09,"holds",3,0.35,"timeout",0,900,"holds",2,0.28,"cex",0,900]
["valid","simulation","metros_1_e2_1102_e2_943",{"$nulls":6},"--","--","--","holds",3,0.04,"holds",3,0.09,"holds",3,0.35,"holds",2,0.34,"holds",2,0.12,"cex",0,900]
["valid","simulation","metros_1_e2_1102_e3_961",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.09,"holds",3,0.37,"holds",2,0.39,"holds",2,0.31,"cex",0,900]
["valid","simulation","metros_1_e2_1102_e7_1163",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.09,"holds",3,0.37,"timeout",0,900,"holds",2,0.96,"cex",0,900]
["valid","simulation","metros_1_e2_1102_e8_311",{"$nulls":6},"--","--","--","holds",3,0.04,"holds",3,0.09,"holds",3,0.36,"holds",1,0.08,"holds",1,0.06,"holds",0,0.11]
["valid","simulation","metros_1_e2_627",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.09,"holds",3,0.38,"holds",2,0.16,"holds",2,0.29,"cex",0,900]
["valid","simulation","metros_1_e7_1255_e7_12",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.09,"holds",3,0.35,"timeout",0,900,"holds",2,1.36,"cex",0,900]
["valid","simulation","metros_1_e7_1255_e8_598",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.09,"holds",3,0.39,"holds",2,1.36,"holds",2,0.37,"cex",0,900]
["valid","simulation","metros_1_e7_606",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.09,"holds",3,0.38,"timeout",0,900,"holds",2,1.25,"cex",0,900]
["valid","simulation","metros_1_e8_1567",{"$nulls":6},"--","--","--","holds",3,0.04,"holds",3,0.09,"holds",3,0.38,"holds",1,0.09,"holds",1,0.04,"holds",0,0.1]
["valid","simulation","metros_1_e8_725",{"$nulls":6},"--","--","--","holds",3,0.04,"holds",3,0.09,"holds",3,0.35,"holds",1,0.07,"holds",1,0.06,"holds",0,0.1]
["valid","simulation","metros_1_e8_725_e1_919",{"$nulls":6},"--","--","--","holds",3,0.04,"holds",3,0.09,"holds",3,0.35,"holds",1,0.08,"holds",1,0.06,"holds",0,0.12]
["valid","simulation","metros_1_e8_725_e2_1144",{"$nulls":6},"--","--","--","holds",3,0.04,"holds",3,0.09,"holds",3,0.38,"holds",1,0.07,"holds",1,0.06,"holds",0,0.11]
["valid","simulation","metros_1_e8_725_e3_556",{"$nulls":6},"--","--","--","holds",3,0.04,"holds",3,0.09,"holds",3,0.35,"holds",1,0.07,"holds",1,0.06,"holds",0,0.11]
["valid","simulation","metros_2_e1_1116_e2_617",{"$nulls":6},"--","--","--","holds",3,0.04,"holds",3,0.16,"holds",3,0.34,"holds",2,0.24,"holds",2,0.22,"cex",0,900]
["valid","simulation","metros_2_e2_704_e2_13",{"$nulls":6},"--","--","--","holds",3,0.04,"holds",3,0.16,"holds",3,0.38,"holds",2,0.34,"holds",2,0.27,"cex",0,900]
["valid","simulation","metros_3_e3_1275_e2_454",{"$nulls":6},"--","--","--","holds",3,0.04,"holds",3,0.08,"holds",3,0.36,"timeout",0,900,"holds",2,0.23,"cex",0,900]
["valid","simulation","metros_3_e3_1275_e3_640",{"$nulls":6},"--","--","--","holds",3,0.04,"holds",3,0.08,"holds",3,0.37,"timeout",0,900,"holds",2,0.36,"cex",0,900]
["valid","simulation","metros_4_e2_968_e2_1166",{"$nulls":6},"--","--","--","holds",3,0.04,"holds",3,0.08,"holds",3,0.38,"timeout",0,900,"holds",2,0.24,"cex",0,900]
["valid","simulation","metros_4_e2_968_e3_931",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.08,"holds",3,0.34,"timeout",0,900,"holds",2,0.29,"cex",0,900]
["valid","simulation","metros_4_e3_1091_e2_1317",{"$nulls":6},"--","--","--","holds",3,0.04,"holds",3,0.08,"holds",3,0.34,"timeout",0,900,"holds",2,0.23,"cex",0,900]
["valid","simulation","metros_4_e3_1091_e3_522",{"$nulls":6},"--","--","--","holds",3,0.04,"holds",3,0.08,"holds",3,0.34,"timeout",0,900,"holds",2,0.36,"cex",0,900]
["valid","large","microwave01",{"$nulls":6},"--","--","--","holds",3,0.25,"holds",3,1.17,"holds",3,0.8,"holds",1,6.76,"err:error",0,900,"???",0,900]
["valid","large","microwave02",{"$nulls":6},"--","--","--","holds",3,0.22,"holds",3,0.41,"holds",3,0.68,"holds",0,0.92,"err:error",0,900,"???",0,900]
["valid","large","microwave03",{"$nulls":6},"--","--","--","holds",3,0.3,"holds",3,0.58,"timeout",3,900,"timeout",0,900,"err:error",0,900,"timeout",0,900]
["valid","large","microwave04",{"$nulls":6},"--","--","--","holds",3,0.36,"holds",3,0.52,"timeout",3,900,"timeout",0,900,"err:error",0,900,"timeout",0,900]
["valid","large","microwave15",{"$nulls":6},"--","--","--","holds",3,0.18,"holds",3,0.43,"holds",3,0.67,"holds",0,0.88,"err:error",0,900,"???",0,900]
["valid","large","microwave16",{"$nulls":6},"--","--","--","holds",3,0.23,"holds",3,0.42,"holds",3,0.73,"holds",0,0.86,"err:error",0,900,"???",0,900]
["valid","memory2","MOESI_1",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.16,"holds",3,0.39,"holds",1,0.17,"holds",1,0.08,"cex",0,900]
["valid","memory2","MOESI_2",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.11,"holds",3,0.38,"timeout",0,900,"holds",1,0.32,"cex",0,900]
["valid","memory2","MOESI_2_e1_1121",{"$nulls":6},"--","--","--","holds",3,0.06,"holds",3,0.11,"holds",3,0.4,"timeout",0,900,"holds",1,0.3,"cex",0,900]
["valid","memory2","MOESI_2_e1_1753",{"$nulls":6},"--","--","--","holds",3,0.06,"holds",3,0.11,"holds",3,0.39,"timeout",0,900,"holds",1,0.32,"cex",0,900]
["valid","memory2","MOESI_2_e1_1753_e8_1769",{"$nulls":6},"--","--","--","holds",3,0.06,"holds",3,0.11,"holds",3,0.38,"timeout",0,900,"holds",1,0.3,"cex",0,900]
["valid","memory2","MOESI_2_e2_155",{"$nulls":6},"--","--","--","holds",3,0.06,"holds",3,0.1,"holds",3,0.39,"timeout",0,900,"holds",1,0.28,"cex",0,900]
["valid","memory2","MOESI_2_e2_1599",{"$nulls":6},"--","--","--","holds",3,0.06,"holds",3,0.1,"holds",3,0.38,"timeout",0,900,"holds",1,0.32,"cex",0,900]
["valid","memory2","MOESI_2_e2_1599_e8_1334",{"$nulls":6},"--","--","--","holds",3,0.06,"holds",3,0.11,"holds",3,0.41,"timeout",0,900,"holds",1,0.32,"cex",0,900]
["valid","memory2","MOESI_2_e3_1523",{"$nulls":6},"--","--","--","holds",3,0.06,"holds",3,0.21,"holds",3,0.41,"timeout",0,900,"holds",1,0.3,"cex",0,900]
["valid","memory2","MOESI_2_e3_929",{"$nulls":6},"--","--","--","holds",3,0.06,"holds",3,0.11,"holds",3,0.4,"timeout",0,900,"holds",1,0.33,"cex",0,900]
["valid","memory2","MOESI_2_e3_929_e4_578",{"$nulls":6},"--","--","--","holds",3,0.06,"holds",3,0.12,"holds",3,0.41,"timeout",0,900,"holds",1,0.46,"cex",0,900]
["valid","memory2","MOESI_2_e3_929_e5_1826",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.11,"holds",3,0.4,"timeout",0,900,"holds",1,0.32,"cex",0,900]
["valid","memory2","MOESI_2_e3_929_e6_2707",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.11,"holds",3,0.4,"timeout",0,900,"holds",1,0.28,"cex",0,900]
["valid","memory2","MOESI_2_e3_929_e8_1167",{"$nulls":6},"--","--","--","holds",3,0.06,"holds",3,0.11,"holds",3,0.4,"timeout",0,900,"holds",1,0.33,"cex",0,900]
["valid","memory2","MOESI_2_e7_2910_e8_2590",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.11,"holds",3,0.4,"timeout",0,900,"holds",1,0.32,"cex",0,900]
["valid","memory2","MOESI_2_e8_101",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.11,"holds",3,0.39,"timeout",0,900,"holds",1,0.28,"cex",0,900]
["valid","memory2","MOESI_2_e8_926",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.11,"holds",3,0.39,"timeout",0,900,"holds",1,0.31,"cex",0,900]
["valid","memory2","MOESI_2_e8_926_e1_1065",{"$nulls":6},"--","--","--","holds",3,0.06,"holds",3,0.11,"holds",3,0.39,"timeout",0,900,"holds",1,0.29,"cex",0,900]
["valid","memory2","MOESI_2_e8_926_e2_349",{"$nulls":6},"--","--","--","holds",3,0.06,"holds",3,0.11,"holds",3,0.4,"timeout",0,900,"holds",1,0.32,"cex",0,900]
["valid","memory2","MOESI_2_e8_926_e3_1758",{"$nulls":6},"--","--","--","holds",3,0.06,"holds",3,0.11,"holds",3,0.38,"timeout",0,900,"holds",1,0.29,"cex",0,900]
["valid","memory2","MOESI_2_e8_926_e8_2138",{"$nulls":6},"--","--","--","holds",3,0.08,"holds",3,0.11,"holds",3,0.39,"timeout",0,900,"holds",1,0.32,"cex",0,900]
["valid","memory2","MOESI_all",{"$nulls":6},"--","--","--","holds",3,0.06,"holds",3,0.11,"holds",3,0.39,"timeout",0,900,"holds",1,0.37,"cex",0,900]
["valid","protocol","peterson_1",{"$nulls":6},"--","--","--","holds",3,0.1,"holds",3,0.39,"holds",3,0.61,"holds",1,0.28,"holds",1,0.13,"cex",0,900]
["valid","protocol","peterson_2",{"$nulls":6},"--","--","--","holds",3,0.09,"holds",3,0.36,"holds",3,0.57,"holds",1,0.26,"holds",1,0.12,"cex",0,900]
["valid","protocol","peterson_3",{"$nulls":6},"--","--","--","holds",3,0.11,"holds",3,0.52,"holds",3,0.56,"holds",1,0.26,"holds",1,0.15,"cex",0,900]
["valid","protocol","peterson_4",{"$nulls":6},"--","--","--","holds",3,0.09,"holds",3,0.55,"holds",3,0.57,"holds",1,0.26,"holds",1,0.16,"cex",0,900]
["valid","protocol","peterson_all",{"$nulls":6},"--","--","--","holds",3,0.11,"holds",3,0.43,"holds",3,0.64,"holds",1,0.29,"holds",1,0.39,"cex",0,900]
["valid","simulation","PRODUCER_CONSUMER_1",{"$nulls":6},"--","--","--","holds",3,0.04,"holds",3,0.11,"holds",3,0.33,"timeout",0,900,"holds",1,0.02,"cex",0,900]
["valid","simulation","PRODUCER_CONSUMER_2",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.05,"holds",3,0.31,"holds",1,0.07,"holds",1,0.05,"cex",0,900]
["valid","simulation","PRODUCER_CONSUMER_3",{"$nulls":6},"--","--","--","holds",3,0.04,"holds",3,0.1,"holds",3,0.32,"holds",1,0.08,"holds",1,0.04,"holds",0,0.03]
["valid","simulation","PRODUCER_CONSUMER_all",{"$nulls":6},"--","--","--","holds",3,0.04,"holds",3,0.14,"holds",3,0.32,"holds",1,0.15,"holds",1,0.08,"cex",0,900]
["valid","simulation","production_cell",{"$nulls":6},"--","--","--","holds",6,0.1,"holds",6,0.27,"holds",3,0.33,"holds",3,0.03,"holds",3,0.01,"holds",0,0.01]
["valid","simulation","production_cell_e7_207_e8_241",{"$nulls":6},"--","--","--","holds",6,0.1,"holds",6,0.27,"holds",3,0.32,"holds",3,0.02,"holds",3,0.05,"holds",0,0.02]
["valid","simulation","production_cell_e8_6",{"$nulls":6},"--","--","--","holds",6,0.1,"holds",6,0.29,"holds",3,0.33,"holds",3,0.06,"holds",3,0.03,"holds",0,0.04]
["valid","simulation","production_cell_e8_792",{"$nulls":6},"--","--","--","holds",6,0.1,"holds",6,0.29,"holds",3,0.34,"holds",3,0.02,"holds",3,0.01,"holds",0,0.01]
["valid","protocol","readwrit",{"$nulls":6},"--","--","--","holds",3,0.07,"holds",3,0.14,"holds",3,0.56,"timeout",0,900,"holds",1,0.13,"cex",0,900]
["valid","protocol","rtp_1",{"$nulls":6},"--","--","--","holds",3,0.04,"holds",3,0.08,"holds",3,0.47,"holds",1,0.69,"holds",1,0.11,"cex",0,900]
["valid","protocol","rtp_10",{"$nulls":6},"--","--","--","holds",3,0.08,"holds",3,0.3,"holds",3,0.49,"holds",1,0.7,"holds",1,0.09,"cex",0,900]
["valid","protocol","rtp_2",{"$nulls":6},"--","--","--","holds",3,0.04,"holds",3,0.08,"holds",3,0.47,"holds",1,0.35,"holds",1,0.08,"cex",0,900]
["valid","protocol","rtp_3",{"$nulls":6},"--","--","--","holds",3,0.08,"holds",3,0.27,"holds",3,0.48,"holds",1,0.62,"holds",1,0.16,"cex",0,900]
["valid","protocol","rtp_4",{"$nulls":6},"--","--","--","holds",3,0.08,"holds",3,0.33,"holds",3,0.48,"holds",1,0.62,"holds",1,0.13,"cex",0,900]
["valid","protocol","rtp_5",{"$nulls":6},"--","--","--","holds",3,0.07,"holds",3,0.28,"holds",3,0.79,"holds",1,0.62,"holds",1,0.09,"cex",0,900]
["valid","protocol","rtp_6",{"$nulls":6},"--","--","--","holds",3,0.07,"holds",3,0.28,"holds",3,0.5,"holds",1,0.63,"holds",1,0.13,"cex",0,900]
["valid","protocol","rtp_7",{"$nulls":6},"--","--","--","holds",3,0.08,"holds",3,0.28,"holds",3,0.47,"holds",1,0.59,"holds",1,0.09,"cex",0,900]
["valid","protocol","rtp_8",{"$nulls":6},"--","--","--","holds",3,0.08,"holds",3,0.29,"holds",3,0.48,"holds",1,0.54,"holds",1,0.1,"cex",0,900]
["valid","protocol","rtp_9",{"$nulls":6},"--","--","--","holds",3,0.08,"holds",3,0.28,"holds",3,0.5,"holds",1,0.51,"holds",1,0.12,"cex",0,900]
["valid","protocol","rtp_all",{"$nulls":6},"--","--","--","holds",3,0.1,"holds",3,0.21,"holds",3,0.54,"holds",1,0.52,"holds",1,0.84,"???",0,900]
["valid","simulation","speed_e7_207",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.12,"holds",3,0.29,"holds",0,0.03,"holds",0,0.04,"holds",0,0.01]
["valid","simulation","speed_e7_207_e7_538",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.12,"holds",3,0.29,"holds",0,0.04,"holds",0,0.01,"holds",0,0.02]
["valid","simulation","speed_e7_207_e8_507",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.12,"holds",3,0.29,"holds",0,0.02,"holds",0,0.02,"holds",0,0.02]
["valid","simulation","speed_e7_492",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.12,"holds",3,0.33,"holds",0,0.04,"holds",0,0.01,"holds",0,0.02]
["valid","simulation","speed_e8_136",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.12,"holds",3,0.29,"holds",0,0.02,"holds",0,0.04,"holds",0,0.01]
["valid","simulation","speed_e8_649",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.12,"holds",3,0.3,"holds",0,0.02,"holds",0,0.04,"holds",0,0.03]
["valid","simulation","speed_e8_649_e7_709",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.12,"holds",3,0.3,"holds",0,0.02,"holds",0,0.01,"holds",0,0.03]
["valid","simulation","speed2",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.12,"holds",3,0.31,"timeout",0,900,"holds",1,0.05,"cex",0,900]
["valid","simulation","speed2_e7_223",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.12,"holds",3,0.31,"timeout",0,900,"holds",1,0.04,"cex",0,900]
["valid","simulation","speed2_e7_223_e7_213",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.12,"holds",3,0.29,"timeout",0,900,"holds",1,0.01,"cex",0,900]
["valid","simulation","speed2_e7_223_e8_329",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.12,"holds",3,0.31,"timeout",0,900,"holds",1,0.05,"cex",0,900]
["valid","simulation","speed2_e7_496",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.12,"holds",3,0.29,"timeout",0,900,"holds",1,0.01,"cex",0,900]
["valid","simulation","speed2_e8_449",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.12,"holds",3,0.31,"holds",1,0.02,"holds",1,0.04,"cex",0,900]
["valid","simulation","speed2_e8_449_e7_353",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.12,"holds",3,0.32,"timeout",0,900,"holds",1,0.04,"cex",0,900]
["valid","simulation","speed2_e8_449_e8_517",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.07,"holds",3,0.32,"holds",2,0.05,"holds",2,0.02,"cex",0,900]
["valid","simulation","speed2_e8_750",{"$nulls":6},"--","--","--","holds",3,0.03,"holds",3,0.12,"holds",3,0.3,"holds",1,0.03,"holds",1,0.03,"cex",0,900]
["valid","misc","stalmark",{"$nulls":6},"--","--","--","holds",3,0.02,"holds",3,0.03,"holds",3,0.31,"holds",1,0.01,"holds",1,0.04,"holds",0,0.03]
["valid","misc","stalmark_e7_27",{"$nulls":6},"--","--","--","holds*",5,0.04,"holds*",5,0.07,"holds",3,0.31,"holds",3,0.02,"holds",3,0.01,"holds",0,0.02]
["valid","misc","stalmark_e7_27_e7_31",{"$nulls":6},"--","--","--","holds*",5,0.04,"holds*",5,0.07,"holds",3,0.31,"holds",3,0.02,"holds",3,0.04,"holds",0,0.01]
["valid","misc","stalmark_e7_27_e8_261",{"$nulls":6},"--","--","--","holds",3,0.02,"holds",3,0.03,"holds",3,0.31,"holds",1,0.02,"holds",1,0.01,"holds",0,0.02]
["valid","misc","stalmark_e7_76",{"$nulls":6},"--","--","--","holds*",5,0.04,"holds*",5,0.07,"holds",3,0.32,"holds",3,0.02,"holds",3,0.04,"holds",0,0.01]
["valid","large","steam_boiler_no_arr1",{"$nulls":6},"--","--","--","holds",3,0.77,"holds",3,2.69,"holds",3,0.72,"holds",0,0.4,"holds",0,0.22,"timeout",0,900]
["valid","large","steam_boiler_no_arr1_e4_23904_e4_2384",{"$nulls":6},"--","--","--","holds",3,0.62,"holds",3,3.75,"holds",3,0.75,"holds",0,0.39,"holds",0,0.24,"timeout",0,900]
["valid","large","steam_boiler_no_arr2",{"$nulls":6},"--","--","--","holds",3,0.07,"holds",3,1.56,"holds",3,0.38,"holds",1,0.16,"holds",1,0.15,"holds",0,0.47]
["valid","large","steam_boiler_no_arr2_e1_17214_e5_18600",{"$nulls":6},"--","--","--","holds",3,0.07,"holds",3,1.51,"holds",3,0.38,"holds",1,0.15,"holds",1,0.15,"holds",0,0.36]
["valid","large","steam_boiler_no_arr2_e3_514_e4_11150",{"$nulls":6},"--","--","--","holds",3,0.07,"holds",3,1.57,"holds",3,0.38,"holds",1,0.17,"holds",1,0.15,"holds",0,0.49]
["valid","large","steam_boiler_no_arr2_e6_3003_e4_15091",{"$nulls":6},"--","--","--","holds",3,0.07,"holds",3,1.5,"holds",3,0.35,"holds",1,0.17,"holds",1,0.15,"holds",0,0.66]
["valid","large","steam_boiler_no_arr2_e7_12307",{"$nulls":6},"--","--","--","holds",3,0.07,"holds",3,1.71,"holds",3,0.35,"holds",1,0.17,"holds",1,0.15,"holds",0,0.52]
["valid","large","steam_boiler_no_arr2_e8_21449_e5_18210",{"$nulls":6},"--","--","--","holds",3,0.07,"holds",3,1.51,"holds",3,0.35,"holds",1,0.16,"holds",1,0.14,"holds",0,0.51]
["valid","memory2","SYNAPSE_1",{"$nulls":6},"--","--","--","holds",3,0.04,"holds",3,0.4,"holds",3,0.34,"holds",1,0.1,"holds",1,0.03,"cex",0,900]
["valid","memory2","SYNAPSE_123",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.13,"holds",3,0.38,"timeout",0,900,"holds",1,0.47,"cex",0,900]
["valid","memory2","SYNAPSE_123_e7_837_e8_12",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.17,"holds",3,0.37,"timeout",0,900,"holds",1,0.43,"cex",0,900]
["valid","memory2","SYNAPSE_123_e8_748",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.13,"holds",3,0.35,"timeout",0,900,"holds",1,0.52,"cex",0,900]
["valid","memory2","SYNAPSE_123_e8_953",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.12,"holds",3,0.37,"timeout",0,900,"holds",1,0.52,"cex",0,900]
["valid","memory2","SYNAPSE_123_e8_953_e8_941",{"$nulls":6},"--","--","--","holds",3,0.06,"holds",3,0.12,"holds",3,0.38,"timeout",0,900,"holds",1,0.44,"cex",0,900]
["valid","memory2","SYNAPSE_2",{"$nulls":6},"--","--","--","holds",3,0.04,"holds",3,0.1,"holds",3,0.46,"holds",1,39.34,"holds",1,0.15,"cex",0,900]
["valid","memory2","SYNAPSE_2_e7_790_e8_1344",{"$nulls":6},"--","--","--","holds",3,0.04,"holds",3,0.11,"holds",3,0.35,"holds",1,39.28,"holds",1,0.14,"cex",0,900]
["valid","memory2","SYNAPSE_2_e8_1118",{"$nulls":6},"--","--","--","holds",3,0.04,"holds",3,0.1,"holds",3,0.34,"holds",1,15.56,"holds",1,0.14,"cex",0,900]
["valid","memory2","SYNAPSE_2_e8_1118_e7_1043",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.11,"holds",3,0.33,"holds",1,15.67,"holds",1,0.11,"cex",0,900]
["valid","memory2","SYNAPSE_2_e8_1118_e8_1177",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.1,"holds",3,0.35,"holds",1,12.9,"holds",1,0.14,"cex",0,900]
["valid","memory2","SYNAPSE_2_e8_656",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.11,"holds",3,0.35,"holds",1,15.59,"holds",1,0.11,"cex",0,900]
["valid","memory2","SYNAPSE_3",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.15,"holds",3,0.35,"holds",1,10.56,"holds",1,0.25,"cex",0,900]
["valid","memory2","SYNAPSE_3_e7_1444_e8_1581",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.16,"holds",3,0.36,"holds",1,10.6,"holds",1,0.25,"cex",0,900]
["valid","memory2","SYNAPSE_3_e8_1329",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.15,"holds",3,0.33,"holds",1,26.86,"holds",1,0.21,"cex",0,900]
["valid","memory2","SYNAPSE_3_e8_1329_e8_320",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.16,"holds",3,0.33,"holds",1,10.46,"holds",1,0.24,"cex",0,900]
["valid","memory2","SYNAPSE_3_e8_1708",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.15,"holds",3,0.37,"holds",1,26.82,"holds",1,0.25,"cex",0,900]
["valid","memory2","SYNAPSE_4",{"$nulls":6},"--","--","--","holds",3,0.04,"holds",3,0.13,"holds",3,0.32,"timeout",0,900,"holds",1,0.03,"cex",0,900]
["valid","memory2","SYNAPSE_4_e8_420_e7_572",{"$nulls":6},"--","--","--","holds",6,0.17,"holds",6,0.36,"holds",3,0.32,"holds",1,0.13,"holds",1,0.12,"cex",0,900]
["valid","memory2","SYNAPSE_4_e8_420_e8_1525",{"$nulls":6},"--","--","--","holds",3,0.04,"holds",3,0.13,"holds",3,0.35,"holds",1,0.1,"holds",1,0.06,"cex",0,900]
["valid","memory2","SYNAPSE_4_e8_974",{"$nulls":6},"--","--","--","holds",3,0.04,"holds",3,0.13,"holds",3,0.35,"holds",1,0.1,"holds",1,0.04,"cex",0,900]
["valid","memory2","SYNAPSE_all",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.14,"holds",3,0.37,"timeout",0,900,"holds",1,0.54,"cex",0,900]
["valid","memory2","SYNAPSE_all_e3_1864_e6_1336",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.16,"holds",3,0.35,"timeout",0,900,"holds",1,0.55,"cex",0,900]
["valid","memory2","SYNAPSE_all_e7_907_e8_915",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.14,"holds",3,0.38,"timeout",0,900,"holds",1,0.58,"cex",0,900]
["valid","memory2","SYNAPSE_all_e8_251",{"$nulls":6},"--","--","--","holds",3,0.05,"holds",3,0.17,"holds",3,0.35,"timeout",0,900,"holds",1,0.54,"cex",0,900]
["valid","misc","ticket3i_1",{"$nulls":6},"--","--","--","holds",3,0.08,"holds",3,0.24,"holds",3,0.48,"holds",1,0.13,"holds",1,0.21,"cex",0,900]
["valid","misc","ticket3i_2",{"$nulls":6},"--","--","--","holds",3,0.07,"holds",3,0.18,"holds",3,0.41,"cex",4,900,"holds",1,0.12,"cex",0,900]
["valid","misc","ticket3i_3",{"$nulls":6},"--","--","--","holds",3,0.07,"holds",3,0.16,"holds",3,0.46,"cex",2,900,"holds",1,0.11,"cex",0,900]
["valid","misc","ticket3i_3_e7_1312_e8_1916",{"$nulls":6},"--","--","--","holds",3,0.06,"holds",3,0.18,"holds",3,0.47,"cex",2,900,"holds",1,0.11,"cex",0,900]
["valid","misc","ticket3i_3_e8_1703",{"$nulls":6},"--","--","--","holds",3,0.07,"holds",3,0.16,"holds",3,0.46,"cex",2,900,"holds",1,0.11,"cex",0,900]
["valid","misc","ticket3i_3_e8_1703_e8_2560",{"$nulls":6},"--","--","--","holds",3,0.06,"holds",3,0.18,"holds",3,0.46,"cex",2,900,"holds",1,0.07,"cex",0,900]
["valid","misc","ticket3i_3_e8_1788",{"$nulls":6},"--","--","--","holds",3,0.06,"holds",3,0.16,"holds",3,0.43,"cex",2,900,"holds",1,0.11,"cex",0,900]
["valid","misc","ticket3i_4",{"$nulls":6},"--","--","--","holds",3,0.07,"holds",3,0.25,"holds",3,0.43,"holds",1,0.13,"holds",1,0.09,"cex",0,900]
["valid","misc","ticket3i_5",{"$nulls":6},"--","--","--","holds",3,0.07,"holds",3,0.23,"holds",3,0.46,"holds",1,0.13,"holds",1,0.13,"cex",0,900]
["valid","misc","ticket3i_6",{"$nulls":6},"--","--","--","holds",3,0.07,"holds",3,0.25,"holds",3,0.44,"holds",1,0.13,"holds",1,0.13,"cex",0,900]
["valid","misc","ticket3i_7",{"$nulls":6},"--","--","--","holds",3,0.08,"holds",3,0.26,"holds",3,0.48,"holds",1,0.13,"holds",1,0.3,"cex",0,900]
["valid","misc","ticket3i_7_e1_2192_e1_1852",{"$nulls":6},"--","--","--","holds",6,0.35,"holds",6,1.3,"holds",6,1.46,"holds",3,1.1,"holds",3,17.73,"cex",0,900]
["valid","misc","ticket3i_all",{"$nulls":6},"--","--","--","holds",3,0.08,"holds",3,0.19,"holds",3,0.48,"holds",1,0.14,"holds",1,0.38,"cex",0,900]
["valid","misc","traffic",{"$nulls":6},"--","--","--","holds",3,0.02,"holds",3,0.04,"holds",3,0.29,"holds",1,0.04,"holds",1,0.02,"cex",0,900]
["valid","misc","traffic_e7_46_e8_16",{"$nulls":6},"--","--","--","holds",3,0.02,"holds",3,0.04,"holds",3,0.3,"holds",1,0.02,"holds",1,0.02,"cex",0,900]
["valid","simulation","tramway",{"$nulls":6},"--","--","--","holds",9,0.35,"holds",9,2.7,"holds",3,0.3,"holds",4,0.03,"holds",4,0.03,"holds",0,0.03]
["valid","simulation","tramway_e7_1834",{"$nulls":6},"--","--","--","holds",3,0.07,"holds",3,0.65,"holds",3,0.32,"holds",1,0.03,"holds",1,0.02,"holds",0,0.04]
["valid","simulation","tramway_e7_1834_e7_2363",{"$nulls":6},"--","--","--","holds",3,0.07,"holds",3,0.27,"holds",3,0.33,"holds",1,0.03,"holds",1,0.05,"holds",0,0.02]
["valid","simulation","tramway_e7_1834_e8_3192",{"$nulls":6},"--","--","--","holds",9,0.37,"holds",9,2.96,"holds",3,0.33,"holds",4,0.04,"holds",4,0.03,"holds",0,0.03]
["valid","simulation","tramway_e7_3304",{"$nulls":6},"--","--","--","holds",3,0.06,"holds",3,0.61,"holds",3,0.31,"holds",1,0.03,"holds",1,0.05,"holds",0,0.02]
["valid","misc","twisted_counters",{"$nulls":6},"--","--","--","holds*",11,0.17,"holds*",11,0.35,"timeout",126,900,"timeout",0,900,"cex",2,900,"cex",0,900]
["valid","misc","two_counters",{"$nulls":6},"--","--","--","holds",6,0.05,"holds*",5,0.09,"holds",6,0.65,"holds",4,0.03,"cex",3,900,"cex",0,900]
["valid","simulation","ums",{"$nulls":6},"--","--","--","holds",3,0.09,"holds",3,0.72,"holds",3,0.39,"holds",1,0.03,"err:stack",0,900,"holds",0,0.1]
["valid","simulation","ums_e8_1032",{"$nulls":6},"--","--","--","holds",6,0.27,"holds",6,3.22,"holds",6,0.99,"holds",3,0.03,"err:stack",0,900,"holds",0,0.02]
[]
["INVALID TOTAL",{"$nulls":4},3021.2199999999975,null,null,1767.9399999999898,null,null,2704.5000000000045,null,null,0,null,null,15248.97000000001,null,null,0,null,null,33036.03999999994,null,null,81851.89000000003,null,null,0]
["VALID TOTAL",{"$nulls":4},0,null,null,0,null,null,0,null,null,251.75000000000028,null,null,454.8699999999998,null,null,9171.65999999998,null,null,190205.94999999998,null,null,40022.79000000004,null,null,290917.67]
[]
[]
[]
[null,null,"KEY:"]
[null,null,"kind bmc","Kind in BMC mode, no abstraction, no path compression"]
[null,null,"kind bmc w/abstraction","Kind in BMC mode, with \"path\" abstraction, no path compression"]
[null,null,"sal bmc","SAL in BMC mode, no path compression"]
[null,null,"kind inductive + path compression","Kind in (incremental) induction mode, with path compression, no abstraction; each iteration has a depth 3 greater than the former"]
[null,null,"kind inductive + path compression w/abstraction","Kind in (incremental) induction mode, with path compression, with \"path\" abstraction; each iteration has a depth 3 greater than the former"]
[null,null,"sal inductive +acyclic","SAL in (incremental) induction mode, with --acyclic option"]
[null,null,"luke","luke (default options)"]
[null,null,"rantanplan","Rantanplan --offline glpk --online pooh"]
[null,null,"lesar","lesar (with -poly library)"]
[]
[null,null,"result:","the result of the test:"]
[{"$nulls":3},"holds: valid"]
[{"$nulls":3},"holds*: found valid with termination check"]
[{"$nulls":3},"cex: counterexample found or \"invalid\" reported"]
[{"$nulls":3},"err, timeout: error or timeout"]
[]
[null,null,"step:","The reported depth of halting (note that SAL appears to usually count depths as 1 less than Kind)"]
[]
[null,null,"tottime:","The total time spent on the run, in seconds (max 900)"]

{"sheet":"Sheet2","index":1,"n_rows":0,"n_cols":0,"rows_kept":0,"flags":["formulas_cached_only"]}

{"sheet":"Sheet3","index":2,"n_rows":0,"n_cols":0,"rows_kept":0,"flags":["formulas_cached_only"]}