mslf_g	mslf_g_r	sat_g	sat_g_r	mslf_sat_g	mslf_sat_g_r
Avg. runtime compare	7.73461 sec (#2230)	7.80199 sec (#2230)	2.15843 sec (#2230)	2.023 sec (#2230)	2.21536 sec (#2230)	2.04052 sec (#2230)
Avg. Choice Points compare	6851.25 CP (#2230)	6897.5 CP (#2230)	1614.5 CP (#2230)	1447.98 CP (#2230)	1747.39 CP (#2230)	1576.47 CP (#2230)
Avg. Fails compare	6804.24 Fails (#2230)	6793.02 Fails (#2230)	1567.49 Fails (#2230)	1363.12 Fails (#2230)	1684.51 Fails (#2230)	1475.73 Fails (#2230)
Avg. Clauses Begin compare	7668.95 Cl (#2230)	7668.95 Cl (#2230)	7668.95 Cl (#2230)	7668.95 Cl (#2230)	7668.95 Cl (#2230)	7668.95 Cl (#2230)
Avg. Clauses End compare	22145.6 Cl (#2230)	22232.4 Cl (#2230)	15186.2 Cl (#2230)	15519.3 Cl (#2230)	16107.1 Cl (#2230)	16555.7 Cl (#2230)
Avg. Nogoods compare	4212.7 Ng (#2230)	4211.52 Ng (#2230)	711.604 Ng (#2230)	613.494 Ng (#2230)	742.449 Ng (#2230)	631.276 Ng (#2230)
Avg. Restarts compare	0 Rs (#2230)	1.52915 Rs (#2230)	0 Rs (#2230)	0.9 Rs (#2230)	0 Rs (#2230)	0.890135 Rs (#2230)
Avg. runtime solved	8.29086 sec (#2237)	8.37174 sec (#2237)	5.01373 sec (#2276)	4.47357 sec (#2276)	5.07609 sec (#2277)	4.97931 sec (#2278)
Avg. Choice Points solved	7332.86 CP (#2237)	7347.09 CP (#2237)	3796.24 CP (#2276)	3350.74 CP (#2276)	4013.34 CP (#2277)	3699.68 CP (#2278)
Avg. Fails solved	7285.82 Fails (#2237)	7241.85 Fails (#2237)	3748.39 Fails (#2276)	3258.9 Fails (#2276)	3948.89 Fails (#2277)	3590.57 Fails (#2278)
Avg. Clauses Begin solved	7706.04 Cl (#2237)	7705.76 Cl (#2237)	8077.6 Cl (#2276)	8069.37 Cl (#2276)	8086.6 Cl (#2277)	8097.04 Cl (#2278)
Avg. Clauses End solved	22840 Cl (#2237)	22961.4 Cl (#2237)	18739.3 Cl (#2276)	19046.7 Cl (#2276)	19760.6 Cl (#2277)	20488.8 Cl (#2278)
Avg. Nogoods solved	4576.94 Ng (#2237)	4543.02 Ng (#2237)	2140.83 Ng (#2276)	1856.63 Ng (#2276)	2230.31 Ng (#2277)	2021.32 Ng (#2278)
Avg. Restarts solved	0 Rs (#2237)	1.55431 Rs (#2237)	0 Rs (#2276)	1.06371 Rs (#2276)	0 Rs (#2277)	1.06541 Rs (#2278)
Avg. runtime all	35.9591 sec (#2340)	36.0402 sec (#2340)	22.9057 sec (#2340)	22.3777 sec (#2340)	22.7105 sec (#2340)	22.364 sec (#2340)
Avg. Choice Points all	7010.09 CP (#2340)	7023.69 CP (#2340)	3692.41 CP (#2340)	3259.09 CP (#2340)	3905.29 CP (#2340)	3601.66 CP (#2340)
Infeasibility	351/351/2340	351/351/2340	351/351/2340	351/351/2340	351/351/2340	351/351/2340
Feasibility	1989/1989/2340	1989/1989/2340	1989/1989/2340	1989/1989/2340	1989/1989/2340	1989/1989/2340
Avg. LB distance all	3.96785 (No UB: #0)	3.96352 (No UB: #0)	3.76928 (No UB: #0)	3.73334 (No UB: #0)	3.84003 (No UB: #0)	3.73049 (No UB: #0)
Avg. LB distance shown	3.96785 (No UB: #0)	3.96352 (No UB: #0)	3.76928 (No UB: #0)	3.73334 (No UB: #0)	3.84003 (No UB: #0)	3.73049 (No UB: #0)
Avg. UB distance all	-0.340013 (No UB: #0)	-0.343166 (No UB: #0)	-0.495157 (No UB: #0)	-0.52308 (No UB: #0)	-0.444492 (No UB: #0)	-0.525536 (No UB: #0)
Avg. UB distance shown	-0.340013 (No UB: #0)	-0.343166 (No UB: #0)	-0.495157 (No UB: #0)	-0.52308 (No UB: #0)	-0.444492 (No UB: #0)	-0.525536 (No UB: #0)
Avg. Fails all	23781.6 Fails (#2340)	23787.9 Fails (#2340)	13211.3 Fails (#2340)	12212.9 Fails (#2340)	12933.1 Fails (#2340)	12341.6 Fails (#2340)
Avg. Clauses Begin all	9227.13 Cl (#2340)	9227.13 Cl (#2340)	9227.13 Cl (#2340)	9227.13 Cl (#2340)	9227.13 Cl (#2340)	9227.13 Cl (#2340)
Avg. Clauses End all	33336.6 Cl (#2340)	33467.3 Cl (#2340)	25929.3 Cl (#2340)	31798.6 Cl (#2340)	27640.1 Cl (#2340)	33256.7 Cl (#2340)
Avg. Nogoods all	16195.4 Ng (#2340)	16206.3 Ng (#2340)	8105.3 Ng (#2340)	7476.75 Ng (#2340)	7899.57 Ng (#2340)	7509.38 Ng (#2340)
Avg. Restarts all	0 Rs (#2340)	1.95171 Rs (#2340)	0 Rs (#2340)	1.33547 Rs (#2340)	0 Rs (#2340)	1.32607 Rs (#2340)

Problem	Previously best		mslf\_g									mslf\_g\_r									sat\_g									sat\_g\_r									mslf\_sat\_g									mslf\_sat\_g\_r
	LB	UB	LB	UB	Run time	Choice Points	Fails	Cl Begin	Cl End	Nogoods	Restarts	LB	UB	Run time	Choice Points	Fails	Cl Begin	Cl End	Nogoods	Restarts	LB	UB	Run time	Choice Points	Fails	Cl Begin	Cl End	Nogoods	Restarts	LB	UB	Run time	Choice Points	Fails	Cl Begin	Cl End	Nogoods	Restarts	LB	UB	Run time	Choice Points	Fails	Cl Begin	Cl End	Nogoods	Restarts	LB	UB	Run time	Choice Points	Fails	Cl Begin	Cl End	Nogoods	Restarts
psp_c_1	335	336	336	336	0.62s	1633	1564	24801	37694	144	0	336	336	0.64s	1717	1532	24801	37898	142	3	336	336	0.67s	1810	1741	24801	37554	101	0	336	336	0.67s	1687	1280	24801	40627	158	4	336	336	0.61s	1683	1575	24801	37442	130	0	336	336	0.62s	1424	1093	24801	39865	202	3
psp_c_2	576	576	576	576	0.63s	1603	1510	27783	43742	152	0	576	576	0.66s	1662	1405	27783	43798	141	3	576	576	0.18s	160	67	27783	30568	7	0	576	576	0.18s	161	66	27783	30568	8	1	576	576	0.25s	454	281	27783	32333	9	0	576	576	0.25s	454	281	27783	32333	9	0
psp_c_3	372	379	379	379	0.99s	2366	2314	17504	35687	1047	0	379	379	1.06s	2558	2354	17504	36139	1060	4	379	379	0.38s	1267	1215	17504	22245	24	0	379	379	0.24s	452	327	17504	21600	24	2	379	379	0.45s	1109	1022	17504	28815	182	0	379	379	0.46s	1146	893	17504	29133	170	3
psp_c_4	244	258	258	258	2.10s	6710	6651	13592	30685	2799	0	258	258	2.14s	6847	6638	13592	30800	2808	5	258	258	0.70s	1650	1591	13592	25773	530	0	258	258	0.78s	1930	1668	13592	27326	496	4	258	258	0.83s	2325	2245	13592	27476	582	0	258	258	0.80s	2207	1870	13592	27490	454	4
psp_c_5	403	403	403	403	1.20s	3937	3847	26712	49707	206	0	403	403	1.21s	4128	3747	26712	50045	206	4	403	403	0.23s	160	70	26712	28941	17	0	403	403	0.22s	160	67	26712	28941	17	1	403	403	0.28s	457	301	26712	31188	16	0	403	403	0.27s	457	301	26712	31188	16	0
psp_c_6	316	336	327	327	5.62s	13647	13601	19766	51794	7051	0	327	327	5.79s	13741	13504	19766	52778	6959	6	327	327	0.53s	1047	1001	19766	30273	221	0	327	327	0.44s	714	502	19766	29529	135	3	327	327	0.71s	1557	1461	19766	37666	423	0	327	327	0.49s	1045	758	19766	31433	171	3
psp_c_7	426	426	426	426	1.21s	3392	3303	23642	47120	567	0	426	426	1.24s	3542	3185	23642	47585	561	4	426	426	0.68s	2599	2510	23642	31609	44	0	426	426	0.75s	2195	1519	23642	36829	175	4	426	426	1.22s	3720	3566	23642	46873	320	0	426	426	1.28s	3823	3368	23642	49098	252	5
psp_c_8	493	493	493	493	0.45s	1315	1241	20963	27637	91	0	493	493	0.47s	1368	1212	20963	27699	86	3	493	493	0.16s	141	67	20963	22529	2	0	493	493	0.16s	142	68	20963	22516	2	1	493	493	0.22s	471	354	20963	25264	29	0	493	493	0.23s	471	314	20963	25264	29	1
psp_c_9	253	253	253	253	2.80s	7293	7219	16369	35391	3324	0	253	253	2.83s	7394	7136	16369	35327	3261	5	253	253	0.92s	2224	2150	16369	29247	936	0	253	253	0.56s	1063	869	16369	28834	313	3	253	253	5.73s	11250	11116	16369	56007	7099	0	253	253	0.82s	1756	1447	16369	32218	587	4
psp_c_10	374	374	374	374	1.47s	4794	4702	28749	56528	193	0	374	374	1.48s	4999	4604	28749	57234	190	5	374	374	0.76s	1999	1907	28749	42112	164	0	374	374	0.82s	2070	1686	28749	42637	240	4	374	374	0.70s	1782	1603	28749	40355	190	0	374	374	0.59s	1416	1027	28749	40118	94	3
psp_c_11	272	272	272	272	0.17s	208	150	6823	7236	0	0	272	272	0.18s	208	123	6823	7236	0	1	272	272	0.15s	86	28	6823	7055	0	0	272	272	0.14s	86	28	6823	7055	0	0	272	272	0.17s	208	150	6823	7236	0	0	272	272	0.18s	208	150	6823	7236	0	0
psp_c_12	320	331	331	331	0.26s	688	602	5762	8822	160	0	331	331	0.26s	774	584	5762	8883	165	2	331	331	0.30s	650	564	5762	9543	211	0	331	331	0.26s	527	417	5762	9351	142	2	331	331	0.24s	562	421	5762	9274	114	0	331	331	0.26s	664	500	5762	9391	180	2
psp_c_13	389	389	389	389	0.13s	130	57	9574	9600	0	0	389	389	0.13s	130	57	9574	9600	0	0	389	389	0.12s	105	32	9574	9638	0	0	389	389	0.13s	105	32	9574	9638	0	0	389	389	0.13s	130	57	9574	9600	0	0	389	389	0.13s	130	57	9574	9600	0	0
psp_c_14	379	379	379	379	0.24s	589	520	16666	19645	49	0	379	379	0.26s	634	506	16666	19741	51	2	379	379	0.16s	98	29	16666	16963	0	0	379	379	0.14s	98	29	16666	16963	0	0	379	379	0.21s	398	312	16666	18991	27	0	379	379	0.22s	398	312	16666	18991	27	0
psp_c_15	510	510	510	510	0.15s	318	227	11185	11726	0	0	510	510	0.14s	325	162	11185	11740	0	1	510	510	0.11s	112	21	11185	11354	0	0	510	510	0.10s	112	21	11185	11354	0	0	510	510	0.14s	318	227	11185	11726	0	0	510	510	0.14s	318	227	11185	11726	0	0
psp_c_16	412	412	412	412	0.14s	206	130	10325	10673	0	0	412	412	0.13s	206	124	10325	10673	0	1	412	412	0.13s	108	32	10325	10530	0	0	412	412	0.13s	108	32	10325	10530	0	0	412	412	0.14s	206	130	10325	10673	0	0	412	412	0.13s	206	130	10325	10673	0	0
psp_c_17	320	320	320	320	0.19s	442	354	7530	8549	7	0	320	320	0.19s	448	350	7530	8556	7	1	320	320	0.13s	114	26	7530	7744	0	0	320	320	0.13s	114	26	7530	7744	0	0	320	320	0.19s	442	282	7530	8737	7	0	320	320	0.18s	442	282	7530	8737	7	0
psp_c_18	310	310	310	310	0.18s	334	252	8103	8779	0	0	310	310	0.18s	367	225	8103	8829	1	1	310	310	0.13s	121	39	8103	8426	1	0	310	310	0.14s	121	39	8103	8426	1	0	310	310	0.18s	334	245	8103	8779	0	0	310	310	0.18s	334	245	8103	8779	0	0
psp_c_19	440	440	440	440	0.14s	268	181	11656	11975	0	0	440	440	0.14s	268	123	11656	11975	0	1	440	440	0.11s	119	32	11656	11847	0	0	440	440	0.12s	119	32	11656	11847	0	0	440	440	0.14s	268	181	11656	11975	0	0	440	440	0.14s	268	181	11656	11975	0	0
psp_c_20	380	380	380	380	0.24s	597	506	14820	15857	0	0	380	380	0.26s	674	463	14820	15951	0	2	380	380	0.14s	128	37	14820	15040	0	0	380	380	0.16s	128	37	14820	15040	0	0	380	380	0.22s	461	282	14820	15888	0	0	380	380	0.21s	461	282	14820	15888	0	0
psp_c_21	393	393	393	393	0.14s	213	131	8596	9027	0	0	393	393	0.13s	213	122	8596	9027	0	1	393	393	0.13s	103	21	8596	8838	0	0	393	393	0.13s	103	21	8596	8838	0	0	393	393	0.14s	213	131	8596	9027	0	0	393	393	0.14s	213	131	8596	9027	0	0
psp_c_22	398	398	398	398	0.14s	205	115	6117	6261	0	0	398	398	0.13s	205	115	6117	6261	0	0	398	398	0.12s	111	21	6117	6297	0	0	398	398	0.13s	111	21	6117	6297	0	0	398	398	0.13s	205	115	6117	6261	0	0	398	398	0.14s	205	115	6117	6261	0	0
psp_c_23	239	239	239	239	0.13s	120	42	4188	4241	0	0	239	239	0.15s	120	42	4188	4241	0	0	239	239	0.12s	103	25	4188	4253	0	0	239	239	0.13s	103	25	4188	4253	0	0	239	239	0.13s	120	42	4188	4241	0	0	239	239	0.15s	120	42	4188	4241	0	0
psp_c_24	321	321	321	321	0.15s	141	55	7883	7924	0	0	321	321	0.14s	141	55	7883	7924	0	0	321	321	0.13s	107	21	7883	7953	0	0	321	321	0.15s	107	21	7883	7953	0	0	321	321	0.15s	141	55	7883	7924	0	0	321	321	0.13s	141	55	7883	7924	0	0
psp_c_25	225	225	225	225	0.13s	73	35	5637	5693	0	0	225	225	0.13s	73	35	5637	5693	0	0	225	225	0.13s	65	27	5637	5694	0	0	225	225	0.13s	65	27	5637	5694	0	0	225	225	0.13s	73	35	5637	5693	0	0	225	225	0.13s	73	35	5637	5693	0	0
psp_c_26	255	255	255	255	0.15s	118	50	4568	4609	0	0	255	255	0.14s	118	50	4568	4609	0	0	255	255	0.15s	91	23	4568	4678	0	0	255	255	0.14s	91	23	4568	4678	0	0	255	255	0.15s	118	50	4568	4609	0	0	255	255	0.15s	118	50	4568	4609	0	0
psp_c_27	231	231	231	231	0.18s	271	200	5062	5671	0	0	231	231	0.19s	273	175	5062	5704	0	1	231	231	0.15s	99	28	5062	5340	0	0	231	231	0.15s	99	28	5062	5340	0	0	231	231	0.19s	271	200	5062	5671	0	0	231	231	0.19s	271	200	5062	5671	0	0
psp_c_28	297	297	297	297	0.12s	84	35	6100	6100	0	0	297	297	0.11s	84	35	6100	6100	0	0	297	297	0.12s	72	23	6100	6112	0	0	297	297	0.12s	72	23	6100	6112	0	0	297	297	0.13s	84	35	6100	6100	0	0	297	297	0.12s	84	35	6100	6100	0	0
psp_c_29	373	373	373	373	0.14s	126	48	12147	12203	0	0	373	373	0.14s	126	48	12147	12203	0	0	373	373	0.13s	102	24	12147	12212	0	0	373	373	0.13s	102	24	12147	12212	0	0	373	373	0.14s	126	48	12147	12203	0	0	373	373	0.14s	126	48	12147	12203	0	0
psp_c_30	346	346	346	346	0.13s	137	55	8938	8959	0	0	346	346	0.14s	137	55	8938	8959	0	0	346	346	0.13s	109	27	8938	8994	0	0	346	346	0.14s	109	27	8938	8994	0	0	346	346	0.13s	137	55	8938	8959	0	0	346	346	0.13s	137	55	8938	8959	0	0
psp_c_31	413	413	413	413	1.99s	3609	3518	22353	45068	516	0	413	413	2.03s	3771	3444	22353	45769	522	4	413	413	0.26s	167	76	22353	25160	23	0	413	413	0.26s	167	68	22353	25171	21	1	413	413	0.36s	465	345	22353	27579	31	0	413	413	0.36s	465	314	22353	27579	30	1
psp_c_32	293	370	367	367	371.78s	365417	365358	27844	207637	260493	0	367	367	330.98s	334029	333618	27844	204697	236743	11	367	367	6.12s	8929	8870	27844	95332	5498	0	367	367	8.72s	11924	11596	27844	108590	7428	7	367	367	7.74s	11003	10903	27844	97753	6539	0	367	367	12.15s	16381	15931	27844	119013	10030	7
psp_c_33	345	383	383	383	149.23s	196878	196814	25277	137119	126097	0	383	383	141.89s	186272	185817	25277	137406	119411	10	383	383	2.43s	3335	3271	25277	74083	1827	0	383	383	4.10s	5486	5241	25277	81161	3255	6	383	383	2.59s	3561	3456	25277	74694	1651	0	383	383	3.58s	4933	4706	25277	82683	2733	6
psp_c_34	334	421	-	409	Time Out		474198	36238	329259	319641	0	-	407	Time Out		481874	36238	322048	324938	11	391	391	84.93s	82430	82339	36238	214319	51829	0	391	391	107.10s	84851	84434	36238	236362	52937	10	391	391	127.04s	101117	100956	36238	224882	62796	0	391	391	60.40s	57466	56896	36238	204101	35703	9
psp_c_35	204	259	-	260	Time Out		453314	22371	144595	297029	0	-	260	Time Out		446361	22371	143265	295344	11	254	254	221.81s	186110	186059	22371	237758	125977	0	-	254	Time Out		299860	22371	226867	198002	12	254	254	426.87s	257147	257047	22371	318339	173692	0	-	254	Time Out		329616	22371	272540	218717	12
psp_c_36	418	418	418	418	4.14s	6215	6127	26126	70101	2066	0	418	418	4.24s	6428	6113	26126	70624	2116	5	418	418	2.05s	3188	3100	26126	49897	187	0	418	418	2.02s	2919	2470	26126	54663	347	5	418	418	1.13s	1568	1423	26126	41082	121	0	418	418	0.93s	1274	887	26126	40764	175	3
psp_c_37	249	325	-	327	Time Out		410895	27060	252976	290696	0	-	327	Time Out		409423	27060	245110	290389	11	-	315	Time Out		325577	27060	362928	222636	0	312	312	240.29s	187544	187168	27060	314715	128788	11	312	312	129.92s	120093	119992	27060	269048	84367	0	312	312	145.40s	128385	128051	27060	288340	89157	10
psp_c_38	235	306	-	291	Time Out		516128	27776	236895	347120	0	-	291	Time Out		515749	27776	236813	347157	12	291	291	40.96s	54032	53967	27776	140614	34938	0	291	291	67.05s	84615	84162	27776	152085	55249	10	291	291	65.05s	89087	88958	27776	201935	57310	0	291	291	48.52s	64104	63593	27776	142306	41504	9
psp_c_39	398	428	421	421	6.25s	9462	9378	27812	86338	4197	0	421	421	6.41s	9870	9539	27812	86598	4269	6	421	421	11.90s	17818	17734	27812	95506	10194	0	421	421	5.10s	6961	6616	27812	101848	3702	6	421	421	12.38s	17958	17809	27812	92124	11066	0	421	421	7.21s	8945	8603	27812	92086	5020	6
psp_c_40	366	395	386	386	57.38s	129787	129703	21206	108674	84390	0	386	386	57.24s	127433	127048	21206	107799	82787	9	386	386	1.45s	2385	2301	21206	39733	767	0	386	386	1.57s	2542	2372	21206	41363	849	5	386	386	1.78s	3085	2931	21206	43395	963	0	386	386	2.29s	4569	4210	21206	46880	1624	5
psp_c_41	280	280	280	280	0.30s	545	467	7811	9482	0	0	280	280	0.31s	591	448	7811	9580	0	2	280	280	0.18s	124	46	7811	8166	1	0	280	280	0.17s	124	46	7811	8166	1	0	280	280	0.25s	371	287	7811	9049	1	0	280	280	0.25s	371	287	7811	9049	1	0
psp_c_42	325	325	325	325	0.24s	496	415	7228	8720	0	0	325	325	0.23s	501	371	7228	8706	0	2	325	325	0.14s	107	26	7228	7465	0	0	325	325	0.13s	107	26	7228	7465	0	0	325	325	0.19s	364	272	7228	8455	0	0	325	325	0.20s	364	272	7228	8455	0	0
psp_c_43	321	321	321	321	0.38s	618	539	11424	13426	0	0	321	321	0.39s	639	456	11424	13477	0	2	321	321	0.19s	137	58	11424	11770	2	0	321	321	0.18s	137	58	11424	11770	2	0	321	321	0.32s	454	302	11424	13098	2	0	321	321	0.33s	454	302	11424	13098	2	0
psp_c_44	322	322	322	322	0.28s	487	403	5729	6955	0	0	322	322	0.29s	519	370	5729	7021	0	2	322	322	0.16s	129	45	5729	6028	2	0	322	322	0.16s	129	45	5729	6028	2	0	322	322	0.26s	435	290	5729	7125	2	0	322	322	0.25s	435	290	5729	7125	2	0
psp_c_45	245	245	245	245	0.26s	357	297	8151	9678	10	0	245	245	0.27s	362	270	8151	9666	9	1	245	245	0.16s	89	29	8151	8351	0	0	245	245	0.18s	89	29	8151	8351	0	0	245	245	0.26s	357	244	8151	9678	10	0	245	245	0.27s	357	244	8151	9678	10	0
psp_c_46	377	377	377	377	0.21s	302	210	9403	9918	1	0	377	377	0.21s	302	121	9403	9918	1	1	377	377	0.15s	136	44	9403	9834	2	0	377	377	0.16s	136	44	9403	9834	2	0	377	377	0.22s	302	210	9403	9918	1	0	377	377	0.21s	302	210	9403	9918	1	0
psp_c_47	416	416	416	416	0.34s	722	635	12786	14913	4	0	416	416	0.35s	761	569	12786	14960	5	2	416	416	0.14s	131	44	12786	13048	1	0	416	416	0.15s	131	44	12786	13048	1	0	416	416	0.26s	450	291	12786	14057	1	0	416	416	0.26s	450	291	12786	14057	1	0
psp_c_48	318	318	318	318	0.20s	216	158	10123	10521	0	0	318	318	0.20s	216	123	10123	10521	0	1	318	318	0.17s	104	46	10123	10315	1	0	318	318	0.17s	104	46	10123	10315	1	0	318	318	0.20s	216	158	10123	10521	0	0	318	318	0.20s	216	158	10123	10521	0	0
psp_c_49	366	366	366	366	0.26s	465	386	12105	13345	0	0	366	366	0.26s	470	324	12105	13340	0	1	366	366	0.15s	103	24	12105	12296	0	0	366	366	0.14s	103	24	12105	12296	0	0	366	366	0.24s	400	271	12105	13327	0	0	366	366	0.25s	400	271	12105	13327	0	0
psp_c_50	360	360	360	360	0.14s	126	72	8995	9228	3	0	360	360	0.15s	126	72	8995	9228	3	0	360	360	0.14s	66	12	8995	9189	0	0	360	360	0.12s	66	12	8995	9189	0	0	360	360	0.14s	126	72	8995	9228	3	0	360	360	0.15s	126	72	8995	9228	3	0
psp_c_51	302	302	302	302	0.18s	177	111	5903	6146	0	0	302	302	0.18s	177	111	5903	6146	0	0	302	302	0.15s	85	19	5903	6073	0	0	302	302	0.15s	85	19	5903	6073	0	0	302	302	0.18s	177	111	5903	6146	0	0	302	302	0.17s	177	111	5903	6146	0	0
psp_c_52	381	381	381	381	0.17s	222	126	4726	4882	0	0	381	381	0.18s	222	124	4726	4882	0	1	381	381	0.14s	117	21	4726	4893	0	0	381	381	0.15s	117	21	4726	4893	0	0	381	381	0.17s	222	126	4726	4882	0	0	381	381	0.17s	222	126	4726	4882	0	0
psp_c_53	204	204	204	204	0.24s	310	251	4052	4790	4	0	204	204	0.26s	341	244	4052	4875	4	1	204	204	0.16s	86	27	4052	4303	0	0	204	204	0.16s	86	27	4052	4303	0	0	204	204	0.26s	310	243	4052	4790	4	0	204	204	0.25s	310	243	4052	4790	4	0
psp_c_54	361	361	361	361	0.21s	308	224	8911	9333	0	0	361	361	0.22s	326	208	8911	9352	0	1	361	361	0.15s	112	28	8911	9100	0	0	361	361	0.15s	112	28	8911	9100	0	0	361	361	0.21s	308	224	8911	9333	0	0	361	361	0.21s	308	224	8911	9333	0	0
psp_c_55	706	706	706	706	0.16s	212	122	14063	14453	0	0	706	706	0.16s	212	122	14063	14453	0	0	706	706	0.12s	106	16	14063	14193	0	0	706	706	0.12s	106	16	14063	14193	0	0	706	706	0.16s	212	122	14063	14453	0	0	706	706	0.16s	212	122	14063	14453	0	0
psp_c_56	510	510	510	510	0.13s	134	45	7426	7458	0	0	510	510	0.13s	134	45	7426	7458	0	0	510	510	0.13s	105	16	7426	7468	0	0	510	510	0.13s	105	16	7426	7468	0	0	510	510	0.13s	134	45	7426	7458	0	0	510	510	0.13s	134	45	7426	7458	0	0
psp_c_57	259	259	259	259	0.16s	107	48	8002	8095	0	0	259	259	0.17s	107	48	8002	8095	0	0	259	259	0.16s	84	25	8002	8099	0	0	259	259	0.16s	84	25	8002	8099	0	0	259	259	0.16s	107	48	8002	8095	0	0	259	259	0.16s	107	48	8002	8095	0	0
psp_c_58	469	469	469	469	0.14s	139	47	13121	13128	0	0	469	469	0.14s	139	47	13121	13128	0	0	469	469	0.15s	110	18	13121	13178	0	0	469	469	0.13s	110	18	13121	13178	0	0	469	469	0.16s	139	47	13121	13128	0	0	469	469	0.14s	139	47	13121	13128	0	0
psp_c_59	271	271	271	271	0.15s	130	59	5231	5252	0	0	271	271	0.15s	130	59	5231	5252	0	0	271	271	0.15s	102	31	5231	5285	0	0	271	271	0.15s	102	31	5231	5285	0	0	271	271	0.15s	130	59	5231	5252	0	0	271	271	0.15s	130	59	5231	5252	0	0
psp_c_60	432	432	432	432	0.16s	161	82	15538	15917	0	0	432	432	0.16s	161	82	15538	15917	0	0	432	432	0.14s	96	17	15538	15747	0	0	432	432	0.14s	96	17	15538	15747	0	0	432	432	0.18s	161	82	15538	15917	0	0	432	432	0.18s	161	82	15538	15917	0	0
psp_c_61	304	407	-	400	Time Out		503899	26780	177771	349787	0	-	400	Time Out		511944	26780	179366	355488	12	-	400	Time Out		409920	26780	248770	273919	0	-	405	Time Out		434022	26780	435269	287709	12	-	395	Time Out		391445	26780	237745	259410	0	-	393	Time Out		453139	26780	467248	297857	12
psp_c_62	519	621	602	602	63.16s	37371	37312	44175	328103	26734	0	602	602	62.01s	37923	37554	44175	327631	26872	8	602	602	10.72s	6735	6676	44175	197760	3936	0	602	602	20.18s	10076	9714	44175	235706	5987	7	602	602	13.69s	8876	8774	44175	223425	5120	0	602	602	21.18s	11021	10653	44175	250247	6455	7
psp_c_63	302	380	-	393	Time Out		482614	28674	191095	365818	0	-	393	Time Out		486163	28674	195222	366606	11	-	367	Time Out		383975	28674	374224	250759	0	-	372	Time Out		379905	28674	380963	250670	12	-	382	Time Out		374650	28674	377091	246177	0	-	366	Time Out		410157	28674	340427	270071	12
psp_c_64	669	688	688	688	1.64s	2305	2222	22534	33588	759	0	688	688	1.71s	2562	2233	22534	33680	786	4	688	688	0.39s	435	352	22534	28159	92	0	688	688	0.42s	467	255	22534	29594	110	2	688	688	0.61s	770	617	22534	30877	181	0	688	688	0.66s	802	575	22534	31474	182	2
psp_c_65	285	376	-	364	Time Out		508307	27306	200494	359892	0	-	364	Time Out		511222	27306	197179	363369	11	355	355	102.25s	88992	88924	27306	177314	57431	0	355	355	94.88s	86889	86408	27306	152855	56523	10	355	355	60.37s	58768	58666	27306	159099	37031	0	355	355	71.50s	66448	65953	27306	148916	42903	9
psp_c_66	315	385	-	382	Time Out		489969	21606	107200	352276	0	-	382	Time Out		498179	21606	107254	358766	11	-	368	Time Out		536930	21606	262428	351453	0	-	369	Time Out		512560	21606	262610	339135	12	-	372	Time Out		443275	21606	216207	293941	0	-	372	Time Out		525920	21606	273631	348120	12
psp_c_67	291	367	-	365	Time Out		459194	29863	182189	324806	0	-	365	Time Out		439174	29863	176207	310500	11	-	352	Time Out		388292	29863	308763	253995	0	-	356	Time Out		363742	29863	360524	237586	12	-	350	Time Out		368510	29863	347864	240587	0	-	353	Time Out		374563	29863	438932	245281	12
psp_c_68	unsat		unsat		0.89s	898	800	0	0	0	0	unsat		0.89s	898	800	0	0	0	0	unsat		0.89s	898	800	0	0	0	0	unsat		0.88s	898	800	0	0	0	0	unsat		0.91s	898	800	0	0	0	0	unsat		0.87s	898	800	0	0	0	0
psp_c_69	308	388	-	403	Time Out		471503	27600	170242	335823	0	-	403	Time Out		472464	27600	169103	337041	11	-	386	Time Out		384830	27600	226584	253942	0	-	382	Time Out		372957	27600	312159	248482	12	-	382	Time Out		366500	27600	218177	243960	0	-	380	Time Out		340343	27600	328579	223106	12
psp_c_70	353	391	-	383	Time Out		393766	25988	173450	288766	0	-	383	Time Out		389029	25988	173052	284912	11	-	389	Time Out		410544	25988	214491	271715	0	-	385	Time Out		329297	25988	253382	213605	12	-	379	Time Out		322305	25988	253827	207650	0	-	380	Time Out		329904	25988	280058	215754	12
psp_c_71	292	292	292	292	0.39s	440	373	3461	4851	2	0	292	292	0.40s	448	336	3461	4896	0	1	292	292	0.18s	92	25	3461	3857	1	0	292	292	0.17s	92	25	3461	3857	1	0	292	292	0.47s	525	452	3461	5322	22	0	292	292	0.44s	476	385	3461	5385	21	1
psp_c_72	195	195	195	195	0.70s	729	663	5846	8789	150	0	195	195	0.67s	757	644	5846	8866	143	2	195	195	0.28s	156	90	5846	6806	10	0	195	195	0.27s	156	85	5846	6806	10	1	195	195	0.78s	805	713	5846	9355	207	0	195	195	0.67s	741	550	5846	9108	135	2
psp_c_73	630	630	630	630	0.15s	114	27	13369	13388	0	0	630	630	0.14s	114	27	13369	13388	0	0	630	630	0.13s	101	14	13369	13387	0	0	630	630	0.15s	101	14	13369	13387	0	0	630	630	0.13s	114	27	13369	13388	0	0	630	630	0.15s	114	27	13369	13388	0	0
psp_c_74	365	365	365	365	1.40s	1923	1828	11464	21189	49	0	365	365	1.45s	2024	1750	11464	21365	49	3	365	365	0.19s	120	25	11464	12122	0	0	365	365	0.18s	120	25	11464	12122	0	0	365	365	1.12s	1455	1317	11464	18212	77	0	365	365	0.60s	734	449	11464	15772	36	2
psp_c_75	406	406	406	406	0.36s	457	371	9480	10812	0	0	406	406	0.37s	460	321	9480	10817	0	1	406	406	0.18s	125	39	9480	9760	2	0	406	406	0.17s	125	39	9480	9760	2	0	406	406	0.35s	436	283	9480	10918	2	0	406	406	0.36s	436	283	9480	10918	2	0
psp_c_76	409	409	409	409	0.84s	995	909	12405	17839	13	0	409	409	0.89s	1074	852	12405	17976	13	3	409	409	0.22s	143	57	12405	13445	6	0	409	409	0.22s	143	57	12405	13445	6	0	409	409	0.43s	452	299	12405	14994	6	0	409	409	0.44s	452	299	12405	14994	6	0
psp_c_77	365	365	365	365	0.58s	733	651	13097	15378	0	0	365	365	0.58s	766	571	13097	15427	0	2	365	365	0.20s	123	41	13097	13355	1	0	365	365	0.20s	123	41	13097	13355	1	0	365	365	0.40s	448	285	13097	14665	1	0	365	365	0.40s	448	285	13097	14665	1	0
psp_c_78	239	239	239	239	0.39s	437	379	8846	10743	17	0	239	239	0.40s	467	359	8846	10788	17	1	239	239	0.18s	82	24	8846	9169	0	0	239	239	0.18s	82	24	8846	9169	0	0	239	239	0.39s	424	332	8846	10752	17	0	239	239	0.39s	424	304	8846	10752	17	1
psp_c_79	310	310	310	310	0.76s	1023	951	13567	17184	1	0	310	310	0.80s	1081	937	13567	17319	1	3	310	310	0.19s	100	28	13567	13890	0	0	310	310	0.20s	100	28	13567	13890	0	0	310	310	0.36s	366	273	13567	15053	0	0	310	310	0.36s	366	273	13567	15053	0	0
psp_c_80	283	283	283	283	0.79s	1111	1025	5947	9298	4	0	283	283	0.82s	1168	949	5947	9392	4	3	283	283	0.18s	108	22	5947	6169	0	0	283	283	0.18s	108	22	5947	6169	0	0	283	283	0.65s	886	728	5947	8521	11	0	283	283	0.49s	647	387	5947	8133	8	1
psp_c_81	342	342	342	342	0.28s	375	290	7439	7980	0	0	342	342	0.28s	378	209	7439	7982	0	1	342	342	0.17s	107	22	7439	7645	0	0	342	342	0.18s	107	22	7439	7645	0	0	342	342	0.29s	375	247	7439	7980	0	0	342	342	0.28s	375	247	7439	7980	0	0
psp_c_82	394	394	394	394	0.24s	272	188	11682	12112	0	0	394	394	0.24s	272	125	11682	12112	0	1	394	394	0.18s	128	44	11682	11953	1	0	394	394	0.18s	128	44	11682	11953	1	0	394	394	0.24s	272	188	11682	12112	0	0	394	394	0.24s	272	188	11682	12112	0	0
psp_c_83	210	210	210	210	0.21s	152	104	4793	5117	4	0	210	210	0.22s	152	104	4793	5117	4	0	210	210	0.18s	92	44	4793	5043	2	0	210	210	0.18s	92	44	4793	5043	2	0	210	210	0.21s	152	104	4793	5117	4	0	210	210	0.22s	152	104	4793	5117	4	0
psp_c_84	584	584	584	584	0.12s	76	18	6913	6913	0	0	584	584	0.11s	76	18	6913	6913	0	0	584	584	0.11s	72	14	6913	6917	0	0	584	584	0.10s	72	14	6913	6917	0	0	584	584	0.11s	76	18	6913	6913	0	0	584	584	0.11s	76	18	6913	6913	0	0
psp_c_85	430	430	430	430	0.64s	926	837	12591	16301	5	0	430	430	0.61s	946	785	12591	16318	5	2	430	430	0.17s	114	25	12591	13021	1	0	430	430	0.15s	114	25	12591	13021	1	0	430	430	0.35s	420	270	12591	14347	1	0	430	430	0.34s	420	270	12591	14347	1	0
psp_c_86	296	296	296	296	0.30s	334	258	10454	11147	0	0	296	296	0.32s	374	254	10454	11197	0	1	296	296	0.18s	106	30	10454	10668	0	0	296	296	0.19s	106	30	10454	10668	0	0	296	296	0.31s	334	245	10454	11147	0	0	296	296	0.30s	334	245	10454	11147	0	0
psp_c_87	367	367	367	367	0.22s	191	118	6948	7252	0	0	367	367	0.21s	191	118	6948	7252	0	0	367	367	0.17s	96	23	6948	7096	0	0	367	367	0.17s	96	23	6948	7096	0	0	367	367	0.21s	191	118	6948	7252	0	0	367	367	0.21s	191	118	6948	7252	0	0
psp_c_88	258	258	258	258	0.38s	563	474	5535	6568	0	0	258	258	0.40s	592	369	5535	6610	0	2	258	258	0.19s	125	36	5535	5726	0	0	258	258	0.19s	125	36	5535	5726	0	0	258	258	0.31s	401	283	5535	6414	0	0	258	258	0.31s	401	283	5535	6414	0	0
psp_c_89	374	374	374	374	0.17s	95	37	7955	7999	0	0	374	374	0.17s	95	37	7955	7999	0	0	374	374	0.16s	84	26	7955	8009	0	0	374	374	0.17s	84	26	7955	8009	0	0	374	374	0.17s	95	37	7955	7999	0	0	374	374	0.17s	95	37	7955	7999	0	0
psp_c_90	289	293	293	293	0.48s	622	543	5558	7136	12	0	293	293	0.51s	698	475	5558	7232	13	2	293	293	0.19s	131	52	5558	6393	4	0	293	293	0.19s	131	52	5558	6393	4	0	293	293	0.52s	627	502	5558	8092	35	0	293	293	0.68s	841	681	5558	8583	49	2
psp_c_91	258	260	260	260	5.47s	13123	13076	14495	40201	7424	0	260	260	5.41s	13022	12819	14495	40257	7275	6	260	260	1.59s	3498	3451	14495	34103	1847	0	260	260	0.85s	1522	1404	14495	31546	771	4	260	260	2.64s	6069	5998	14495	44386	3342	0	260	260	0.74s	1288	1080	14495	33187	560	3
psp_c_92	342	360	360	360	0.31s	467	402	12294	17902	127	0	360	360	0.31s	471	383	12294	17920	128	1	360	360	0.24s	278	213	12294	16737	71	0	360	360	0.26s	294	188	12294	17450	89	1	360	360	0.30s	479	393	12294	18287	131	0	360	360	0.31s	482	369	12294	18387	132	1
psp_c_93	568	568	568	568	0.54s	1047	981	27443	46469	200	0	568	568	0.58s	1124	921	27443	46610	198	3	568	568	0.33s	695	629	27443	30413	2	0	568	568	0.35s	708	299	27443	31227	4	2	568	568	0.38s	586	493	27443	44218	177	0	568	568	0.39s	602	450	27443	44111	174	2
psp_c_94	425	428	428	428	0.39s	868	800	18185	26667	221	0	428	428	0.41s	962	812	18185	26834	227	2	428	428	0.22s	393	325	18185	22711	31	0	428	428	0.22s	345	201	18185	22578	29	2	428	428	0.36s	817	696	18185	27797	210	0	428	428	0.43s	1036	832	18185	29782	205	3
psp_c_95	383	399	399	399	2.97s	8119	8028	23261	57358	3306	0	399	399	3.23s	9267	8844	23261	59167	3737	6	399	399	0.60s	1477	1386	23261	37086	191	0	399	399	0.63s	1233	828	23261	43325	206	3	399	399	0.92s	2251	2090	23261	46834	325	0	399	399	0.58s	907	630	23261	47959	163	2
psp_c_96	481	501	501	501	1.31s	2030	1961	22890	60453	977	0	501	501	1.33s	2165	1951	22890	60739	979	3	501	501	0.83s	1578	1509	22890	47023	323	0	501	501	0.81s	1315	1074	22890	46255	266	4	501	501	1.22s	1959	1850	22890	67166	818	0	501	501	1.00s	1695	1478	22890	58547	433	4
psp_c_97	479	489	489	489	1.62s	5416	5325	28530	59020	1824	0	489	489	1.76s	5609	5225	28530	59499	1781	5	489	489	0.99s	2452	2361	28530	53488	502	0	489	489	0.79s	1745	1482	28530	50948	306	4	489	489	0.53s	1130	967	28530	43074	204	0	489	489	0.71s	1562	1249	28530	49499	267	4
psp_c_98	507	518	518	518	2.15s	5393	5308	23382	58664	1603	0	518	518	2.17s	5457	5102	23382	58730	1551	5	518	518	0.55s	1242	1157	23382	33522	82	0	518	518	0.59s	1267	853	23382	37447	102	3	518	518	0.68s	1403	1248	23382	38635	127	0	518	518	0.63s	1426	975	23382	39016	132	3
psp_c_99	299	299	299	299	0.72s	1987	1932	10924	19128	933	0	299	299	0.73s	2045	1869	10924	19168	946	4	299	299	0.19s	135	80	10924	12395	18	0	299	299	0.18s	135	71	10924	12395	18	1	299	299	0.39s	832	769	10924	17658	155	0	299	299	0.40s	921	696	10924	17756	145	3
psp_c_100	371	399	399	399	1.11s	2178	2117	19571	42965	876	0	399	399	1.12s	2249	2090	19571	43168	874	4	399	399	0.49s	1199	1138	19571	33300	163	0	399	399	0.42s	792	574	19571	32910	172	3	399	399	0.97s	2253	2150	19571	41195	672	0	399	399	0.56s	1323	1058	19571	34645	171	3
psp_c_101	380	380	380	380	0.17s	396	305	9055	9737	0	0	380	380	0.18s	412	282	9055	9755	0	1	380	380	0.13s	128	37	9055	9268	0	0	380	380	0.14s	128	37	9055	9268	0	0	380	380	0.17s	396	247	9055	9737	0	0	380	380	0.17s	396	247	9055	9737	0	0
psp_c_102	295	295	295	295	0.14s	92	37	5808	5874	0	0	295	295	0.15s	92	37	5808	5874	0	0	295	295	0.14s	80	25	5808	5884	0	0	295	295	0.14s	80	25	5808	5884	0	0	295	295	0.14s	92	37	5808	5874	0	0	295	295	0.14s	92	37	5808	5874	0	0
psp_c_103	332	332	332	332	0.19s	512	426	8186	9298	0	0	332	332	0.19s	525	370	8186	9316	0	2	332	332	0.12s	126	40	8186	8378	0	0	332	332	0.14s	126	40	8186	8378	0	0	332	332	0.16s	391	287	8186	9184	0	0	332	332	0.17s	391	287	8186	9184	0	0
psp_c_104	610	610	610	610	0.12s	121	38	14517	14518	0	0	610	610	0.11s	121	38	14517	14518	0	0	610	610	0.11s	95	12	14517	14547	0	0	610	610	0.11s	95	12	14517	14547	0	0	610	610	0.11s	121	38	14517	14518	0	0	610	610	0.11s	121	38	14517	14518	0	0
psp_c_105	568	568	568	568	0.13s	188	98	13341	13543	0	0	568	568	0.13s	188	98	13341	13543	0	0	568	568	0.12s	119	29	13341	13747	1	0	568	568	0.12s	119	29	13341	13747	1	0	568	568	0.13s	188	98	13341	13543	0	0	568	568	0.12s	188	98	13341	13543	0	0
psp_c_106	350	350	350	350	0.15s	167	100	13077	13303	0	0	350	350	0.15s	167	100	13077	13303	0	0	350	350	0.15s	106	39	13077	13267	1	0	350	350	0.16s	106	39	13077	13267	1	0	350	350	0.17s	167	100	13077	13303	0	0	350	350	0.16s	167	100	13077	13303	0	0
psp_c_107	424	424	424	424	0.13s	115	45	12310	12334	0	0	424	424	0.14s	115	45	12310	12334	0	0	424	424	0.13s	99	29	12310	12379	0	0	424	424	0.13s	99	29	12310	12379	0	0	424	424	0.13s	115	45	12310	12334	0	0	424	424	0.13s	115	45	12310	12334	0	0
psp_c_108	280	280	280	280	0.19s	371	279	5847	6831	2	0	280	280	0.19s	399	221	5847	6854	2	1	280	280	0.14s	122	30	5847	6127	0	0	280	280	0.14s	122	30	5847	6127	0	0	280	280	0.19s	371	248	5847	6831	2	0	280	280	0.19s	371	248	5847	6831	2	0
psp_c_109	368	368	368	368	0.18s	419	347	10001	10982	0	0	368	368	0.18s	431	322	10001	11009	0	1	368	368	0.13s	113	41	10001	10281	1	0	368	368	0.13s	113	41	10001	10281	1	0	368	368	0.18s	396	293	10001	11049	3	0	368	368	0.18s	396	293	10001	11049	3	0
psp_c_110	388	388	388	388	0.17s	419	333	5951	6987	6	0	388	388	0.17s	420	308	5951	6988	6	1	388	388	0.13s	130	44	5951	6207	1	0	388	388	0.13s	130	44	5951	6207	1	0	388	388	0.17s	418	300	5951	7330	7	0	388	388	0.17s	418	300	5951	7330	7	0
psp_c_111	380	380	380	380	0.12s	158	66	5118	5233	3	0	380	380	0.14s	158	66	5118	5233	3	0	380	380	0.12s	119	27	5118	5194	0	0	380	380	0.14s	119	27	5118	5194	0	0	380	380	0.12s	158	66	5118	5233	3	0	380	380	0.13s	158	66	5118	5233	3	0
psp_c_112	316	316	316	316	0.12s	96	37	5710	5729	0	0	316	316	0.12s	96	37	5710	5729	0	0	316	316	0.12s	79	20	5710	5752	0	0	316	316	0.13s	79	20	5710	5752	0	0	316	316	0.13s	96	37	5710	5729	0	0	316	316	0.13s	96	37	5710	5729	0	0
psp_c_113	393	393	393	393	0.13s	143	52	11436	11456	0	0	393	393	0.13s	143	52	11436	11456	0	0	393	393	0.13s	122	31	11436	11531	0	0	393	393	0.13s	122	31	11436	11531	0	0	393	393	0.13s	143	52	11436	11456	0	0	393	393	0.12s	143	52	11436	11456	0	0
psp_c_114	540	540	540	540	0.14s	219	135	14548	15073	2	0	540	540	0.14s	219	123	14548	15073	2	1	540	540	0.12s	119	35	14548	14781	1	0	540	540	0.12s	119	35	14548	14781	1	0	540	540	0.14s	219	135	14548	15073	2	0	540	540	0.14s	219	135	14548	15073	2	0
psp_c_115	467	467	467	467	0.12s	114	35	10661	10671	0	0	467	467	0.12s	114	35	10661	10671	0	0	467	467	0.11s	99	20	10661	10687	0	0	467	467	0.11s	99	20	10661	10687	0	0	467	467	0.12s	114	35	10661	10671	0	0	467	467	0.12s	114	35	10661	10671	0	0
psp_c_116	429	429	429	429	0.10s	118	43	7351	7356	0	0	429	429	0.11s	118	43	7351	7356	0	0	429	429	0.10s	102	27	7351	7386	0	0	429	429	0.10s	102	27	7351	7386	0	0	429	429	0.11s	118	43	7351	7356	0	0	429	429	0.11s	118	43	7351	7356	0	0
psp_c_117	388	388	388	388	0.14s	148	81	11141	11299	0	0	388	388	0.14s	148	81	11141	11299	0	0	388	388	0.13s	98	31	11141	11298	0	0	388	388	0.12s	98	31	11141	11298	0	0	388	388	0.14s	148	81	11141	11299	0	0	388	388	0.14s	148	81	11141	11299	0	0
psp_c_118	252	252	252	252	0.14s	88	37	5153	5235	0	0	252	252	0.13s	88	37	5153	5235	0	0	252	252	0.15s	77	26	5153	5221	0	0	252	252	0.15s	77	26	5153	5221	0	0	252	252	0.12s	88	37	5153	5235	0	0	252	252	0.14s	88	37	5153	5235	0	0
psp_c_119	247	247	247	247	0.14s	84	35	4691	4737	0	0	247	247	0.14s	84	35	4691	4737	0	0	247	247	0.14s	75	26	4691	4751	0	0	247	247	0.14s	75	26	4691	4751	0	0	247	247	0.13s	84	35	4691	4737	0	0	247	247	0.13s	84	35	4691	4737	0	0
psp_c_120	525	525	525	525	0.11s	98	35	11319	11339	0	0	525	525	0.10s	98	35	11319	11339	0	0	525	525	0.10s	88	25	11319	11361	0	0	525	525	0.11s	88	25	11319	11361	0	0	525	525	0.11s	98	35	11319	11339	0	0	525	525	0.11s	98	35	11319	11339	0	0
psp_c_121	350	410	399	399	55.90s	89675	89605	28175	94916	59878	0	399	399	59.13s	92403	91975	28175	95298	61118	9	399	399	28.60s	46730	46660	28175	103078	29225	0	399	399	8.99s	16302	15722	28175	77600	8923	7	399	399	6.40s	12749	12621	28175	72271	8063	0	399	399	6.19s	11164	10857	28175	69717	7054	7
psp_c_122	unsat		unsat		1.00s	1182	1004	0	0	0	0	unsat		0.99s	1182	1004	0	0	0	0	unsat		1.00s	1182	1004	0	0	0	0	unsat		0.99s	1182	1004	0	0	0	0	unsat		1.00s	1182	1004	0	0	0	0	unsat		1.00s	1182	1004	0	0	0	0
psp_c_123	unsat		unsat		0.74s	1080	990	0	0	0	0	unsat		0.73s	1080	990	0	0	0	0	unsat		0.75s	1080	990	0	0	0	0	unsat		0.73s	1080	990	0	0	0	0	unsat		0.73s	1080	990	0	0	0	0	unsat		0.73s	1080	990	0	0	0	0
psp_c_124	237	304	-	286	Time Out		615190	14987	92480	391760	0	-	286	Time Out		622935	14987	91216	396783	12	270	270	26.90s	43782	43719	14987	87220	29140	0	270	270	59.57s	78132	77791	14987	103088	51295	10	270	270	31.25s	47650	47549	14987	95793	31479	0	270	270	106.87s	121739	121269	14987	114883	80481	10
psp_c_125	282	351	-	371	Time Out		538258	31380	180234	381292	0	-	371	Time Out		543618	31380	183551	387282	12	-	336	Time Out		374662	31380	241974	251489	0	-	316	Time Out		353898	31380	473440	233737	12	-	328	Time Out		450714	31380	438141	289672	0	-	330	Time Out		339342	31380	439435	221181	12
psp_c_126	466	502	502	502	22.74s	28343	28263	28164	164533	14558	0	502	502	23.65s	29318	28855	28164	164787	14870	7	502	502	2.64s	3223	3143	28164	82697	1519	0	502	502	3.39s	4365	3970	28164	90234	1460	5	502	502	4.12s	5666	5524	28164	101623	2844	0	502	502	9.34s	10737	10367	28164	132786	5719	7
psp_c_127	401	404	401	401	5.64s	8846	8762	24738	54627	4757	0	401	401	5.91s	9259	8879	24738	54931	4837	6	401	401	0.24s	169	85	24738	27873	37	0	401	401	0.24s	169	71	24738	27873	37	1	401	401	2.08s	3753	3595	24738	43992	495	0	401	401	0.79s	1347	899	24738	34165	132	3
psp_c_128	499	505	505	505	7.91s	16472	16391	22818	52462	7218	0	505	505	7.87s	16506	16065	22818	53269	7075	7	505	505	0.53s	754	673	22818	28071	118	0	505	505	0.63s	907	578	22818	30704	168	3	505	505	0.97s	1560	1407	22818	35772	254	0	505	505	1.28s	2195	1789	22818	38335	295	4
psp_c_129	441	517	506	506	75.60s	80572	80483	28467	268225	50043	0	506	506	73.91s	81768	81176	28467	268041	50299	9	506	506	9.42s	11474	11385	28467	147766	5854	0	506	506	12.59s	15397	15105	28467	165772	8378	7	506	506	9.26s	11717	11542	28467	130008	6337	0	506	506	11.09s	11215	10873	28467	146056	6263	7
psp_c_130	359	434	-	417	Time Out		336361	30016	303643	233450	0	417	417	555.67s	323490	322996	30016	306655	223954	11	417	417	82.03s	65389	65307	30016	182710	42712	0	417	417	28.87s	29037	28543	30016	173521	17499	8	417	417	63.90s	57417	57262	30016	194101	36261	0	417	417	29.00s	28287	27773	30016	162918	17527	8
psp_c_131	561	561	561	561	0.31s	707	614	13548	15364	7	0	561	561	0.33s	822	567	13548	15504	8	2	561	561	0.14s	122	29	13548	13950	2	0	561	561	0.15s	122	29	13548	13950	2	0	561	561	0.39s	951	807	13548	16648	11	0	561	561	0.41s	857	638	13548	17149	15	2
psp_c_132	481	481	481	481	0.18s	151	100	15205	15906	3	0	481	481	0.18s	151	100	15205	15906	3	0	481	481	0.14s	75	24	15205	15420	0	0	481	481	0.14s	75	24	15205	15420	0	0	481	481	0.18s	151	100	15205	15906	3	0	481	481	0.18s	151	100	15205	15906	3	0
psp_c_133	474	474	474	474	0.14s	179	106	9765	10011	0	0	474	474	0.14s	179	106	9765	10011	0	0	474	474	0.13s	94	21	9765	9924	0	0	474	474	0.13s	94	21	9765	9924	0	0	474	474	0.14s	179	106	9765	10011	0	0	474	474	0.15s	179	106	9765	10011	0	0
psp_c_134	283	283	283	283	0.18s	123	72	4364	4642	0	0	283	283	0.17s	123	72	4364	4642	0	0	283	283	0.15s	64	13	4364	4515	0	0	283	283	0.15s	64	13	4364	4515	0	0	283	283	0.18s	123	72	4364	4642	0	0	283	283	0.17s	123	72	4364	4642	0	0
psp_c_135	443	443	443	443	0.28s	458	396	8872	10844	3	0	443	443	0.29s	462	370	8872	10848	3	2	443	443	0.14s	85	23	8872	9077	0	0	443	443	0.14s	85	23	8872	9077	0	0	443	443	0.24s	375	277	8872	10707	1	0	443	443	0.26s	375	277	8872	10707	1	0
psp_c_136	396	396	396	396	0.18s	201	118	2620	2865	0	0	396	396	0.16s	201	118	2620	2865	0	0	396	396	0.13s	108	25	2620	2926	0	0	396	396	0.12s	108	25	2620	2926	0	0	396	396	0.16s	201	118	2620	2865	0	0	396	396	0.17s	201	118	2620	2865	0	0
psp_c_137	281	281	281	281	0.21s	284	222	5546	6509	1	0	281	281	0.23s	313	221	5546	6551	1	1	281	281	0.17s	111	49	5546	5913	6	0	281	281	0.17s	111	49	5546	5913	6	0	281	281	0.22s	284	222	5546	6509	1	0	281	281	0.22s	284	222	5546	6509	1	0
psp_c_138	410	410	410	410	0.20s	247	167	9345	9713	0	0	410	410	0.21s	247	123	9345	9713	0	1	410	410	0.16s	107	27	9345	9599	0	0	410	410	0.15s	107	27	9345	9599	0	0	410	410	0.20s	247	167	9345	9713	0	0	410	410	0.22s	247	167	9345	9713	0	0
psp_c_139	306	306	306	306	0.15s	86	34	6254	6393	0	0	306	306	0.16s	86	34	6254	6393	0	0	306	306	0.16s	75	23	6254	6393	0	0	306	306	0.15s	75	23	6254	6393	0	0	306	306	0.16s	86	34	6254	6393	0	0	306	306	0.16s	86	34	6254	6393	0	0
psp_c_140	311	311	311	311	0.19s	228	158	5850	6423	6	0	311	311	0.20s	228	124	5850	6423	6	1	311	311	0.17s	114	44	5850	6384	3	0	311	311	0.16s	114	44	5850	6384	3	0	311	311	0.19s	228	158	5850	6423	6	0	311	311	0.20s	228	158	5850	6423	6	0
psp_c_141	290	290	290	290	0.19s	179	105	7199	7377	0	0	290	290	0.19s	179	105	7199	7377	0	0	290	290	0.16s	110	36	7199	7374	0	0	290	290	0.17s	110	36	7199	7374	0	0	290	290	0.19s	179	105	7199	7377	0	0	290	290	0.19s	179	105	7199	7377	0	0
psp_c_142	526	526	526	526	0.21s	344	256	12003	12577	0	0	526	526	0.22s	354	212	12003	12602	0	1	526	526	0.13s	114	26	12003	12182	0	0	526	526	0.13s	114	26	12003	12182	0	0	526	526	0.21s	344	248	12003	12577	0	0	526	526	0.21s	344	248	12003	12577	0	0
psp_c_143	373	373	373	373	0.13s	141	61	4690	4690	0	0	373	373	0.14s	141	61	4690	4690	0	0	373	373	0.12s	107	27	4690	4743	0	0	373	373	0.13s	107	27	4690	4743	0	0	373	373	0.13s	141	61	4690	4690	0	0	373	373	0.13s	141	61	4690	4690	0	0
psp_c_144	420	420	420	420	0.13s	148	75	9888	9946	0	0	420	420	0.14s	148	75	9888	9946	0	0	420	420	0.13s	102	29	9888	10043	0	0	420	420	0.13s	102	29	9888	10043	0	0	420	420	0.14s	148	75	9888	9946	0	0	420	420	0.13s	148	75	9888	9946	0	0
psp_c_145	668	668	668	668	0.12s	97	27	13211	13211	0	0	668	668	0.10s	97	27	13211	13211	0	0	668	668	0.10s	83	13	13211	13225	0	0	668	668	0.10s	83	13	13211	13225	0	0	668	668	0.11s	97	27	13211	13211	0	0	668	668	0.10s	97	27	13211	13211	0	0
psp_c_146	420	420	420	420	0.14s	93	31	8535	8556	0	0	420	420	0.14s	93	31	8535	8556	0	0	420	420	0.14s	80	18	8535	8592	0	0	420	420	0.14s	80	18	8535	8592	0	0	420	420	0.14s	93	31	8535	8556	0	0	420	420	0.15s	93	31	8535	8556	0	0
psp_c_147	241	241	241	241	0.14s	91	44	4575	4608	0	0	241	241	0.15s	91	44	4575	4608	0	0	241	241	0.13s	76	29	4575	4644	0	0	241	241	0.14s	76	29	4575	4644	0	0	241	241	0.14s	91	44	4575	4608	0	0	241	241	0.15s	91	44	4575	4608	0	0
psp_c_148	197	197	197	197	0.40s	572	528	5170	8063	150	0	197	197	0.41s	601	508	5170	8140	155	2	197	197	0.18s	104	60	5170	6188	14	0	197	197	0.18s	104	60	5170	6188	14	0	197	197	0.34s	456	392	5170	7709	49	0	197	197	0.42s	618	506	5170	8414	87	2
psp_c_149	345	345	345	345	0.18s	198	126	7398	7737	0	0	345	345	0.17s	198	123	7398	7737	0	1	345	345	0.14s	95	23	7398	7559	0	0	345	345	0.14s	95	23	7398	7559	0	0	345	345	0.18s	198	126	7398	7737	0	0	345	345	0.16s	198	126	7398	7737	0	0
psp_c_150	396	396	396	396	0.12s	92	32	6930	6957	0	0	396	396	0.12s	92	32	6930	6957	0	0	396	396	0.13s	80	20	6930	6985	0	0	396	396	0.12s	80	20	6930	6985	0	0	396	396	0.13s	92	32	6930	6957	0	0	396	396	0.12s	92	32	6930	6957	0	0
psp_c_151	unsat		unsat		0.89s	532	512	0	0	0	0	unsat		0.88s	532	512	0	0	0	0	unsat		0.91s	532	512	0	0	0	0	unsat		0.88s	532	512	0	0	0	0	unsat		0.91s	532	512	0	0	0	0	unsat		0.91s	532	512	0	0	0	0
psp_c_152	307	384	-	400	Time Out		415320	21540	118870	309611	0	-	400	Time Out		443921	21540	119235	330543	11	-	375	Time Out		438391	21540	306348	289303	0	-	369	Time Out		414918	21540	343532	275048	12	-	393	Time Out		393662	21540	181194	262900	0	-	371	Time Out		441747	21540	376197	290233	12
psp_c_153	533	554	553	553	51.71s	54855	54764	35613	178898	30255	0	553	553	57.88s	61434	60862	35613	182964	34603	8	553	553	3.80s	3417	3326	35613	65121	1290	0	553	553	4.57s	4085	3748	35613	74074	1681	5	553	553	4.37s	3837	3670	35613	73257	1622	0	553	553	3.76s	3133	2823	35613	74531	1280	5
psp_c_154	444	535	524	524	64.58s	47384	47318	37549	274672	31194	0	524	524	65.77s	48654	48293	37549	281251	31699	8	524	524	14.40s	12333	12267	37549	188446	7143	0	524	524	12.41s	10291	9923	37549	182882	6207	7	524	524	14.22s	11397	11291	37549	195900	7005	0	524	524	14.09s	10669	10283	37549	186770	6286	7
psp_c_155	320	375	-	382	Time Out		504841	18465	149035	363580	0	-	382	Time Out		496476	18465	150279	356403	11	361	361	331.46s	312587	312504	18465	146778	208216	0	361	361	296.13s	264693	264254	18465	143252	175199	11	361	361	201.56s	200333	200186	18465	111388	133330	0	361	361	402.81s	303644	303062	18465	142472	201706	12
psp_c_156	356	399	-	396	Time Out		412848	24059	227379	297100	0	-	396	Time Out		393164	24059	223232	282657	11	387	387	134.98s	125560	125480	24059	159182	81369	0	387	387	215.61s	190416	189926	24059	220919	122100	11	387	387	216.76s	184729	184590	24059	163886	119900	0	387	387	176.45s	159621	159124	24059	160950	104010	11
psp_c_157	410	475	453	453	93.10s	141641	141512	14870	66950	99763	0	453	453	102.36s	152269	151815	14870	68098	107643	10	453	453	2.08s	3103	2974	14870	30756	1129	0	453	453	1.89s	3399	3191	14870	28930	1299	5	453	453	8.73s	21082	20916	14870	51258	13754	0	453	453	2.28s	4044	3668	14870	32420	1793	5
psp_c_158	349	397	397	397	13.67s	17945	17910	29359	73929	12842	0	397	397	13.97s	18128	17932	29359	74154	12851	7	397	397	1.28s	1383	1348	29359	48234	424	0	397	397	1.34s	1652	1389	29359	50486	788	4	397	397	1.56s	1655	1596	29359	50570	934	0	397	397	1.39s	1675	1494	29359	51273	867	4
psp_c_159	447	488	488	488	4.81s	6706	6614	21739	63606	2271	0	488	488	5.15s	7338	6921	21739	64726	2422	5	488	488	2.93s	3298	3206	21739	51134	642	0	488	488	2.44s	2687	2264	21739	57321	781	5	488	488	2.72s	3093	2931	21739	50830	722	0	488	488	3.24s	3721	3269	21739	64622	1365	5
psp_c_160	323	394	-	396	Time Out		472890	26368	152351	326577	0	-	396	Time Out		473452	26368	152735	326730	11	-	375	Time Out		441175	26368	204762	286861	0	-	377	Time Out		493258	26368	226818	322799	12	-	380	Time Out		445913	26368	188822	288463	0	-	374	Time Out		491873	26368	211219	321664	12
psp_c_161	339	339	339	339	0.37s	448	362	8329	9447	0	0	339	339	0.39s	453	315	8329	9454	1	1	339	339	0.20s	128	42	8329	8725	1	0	339	339	0.20s	128	42	8329	8725	1	0	339	339	0.37s	439	289	8329	9600	1	0	339	339	0.38s	439	289	8329	9600	1	0
psp_c_162	458	458	458	458	0.24s	260	187	10097	10844	0	0	458	458	0.25s	260	122	10097	10844	0	1	458	458	0.17s	96	23	10097	10329	0	0	458	458	0.17s	96	23	10097	10329	0	0	458	458	0.25s	260	187	10097	10844	0	0	458	458	0.25s	260	187	10097	10844	0	0
psp_c_163	434	434	434	434	1.91s	2601	2514	16330	25841	606	0	434	434	1.96s	2768	2412	16330	26068	607	4	434	434	0.18s	122	35	16330	16811	2	0	434	434	0.19s	122	35	16330	16811	2	0	434	434	1.18s	1512	1361	16330	24521	183	0	434	434	0.86s	1095	876	16330	21935	38	3
psp_c_164	292	292	292	292	0.27s	203	161	7607	9127	5	0	292	292	0.27s	203	122	7607	9127	5	1	292	292	0.16s	64	22	7607	7929	0	0	292	292	0.17s	64	22	7607	7929	0	0	292	292	0.26s	203	161	7607	9127	5	0	292	292	0.26s	203	161	7607	9127	5	0
psp_c_165	361	371	371	371	40.50s	55154	55084	13855	58677	32328	0	371	371	42.39s	55088	54644	13855	58597	32241	8	371	371	7.95s	9454	9384	13855	52860	5201	0	371	371	3.17s	3708	3484	13855	34077	1403	5	371	371	8.52s	12325	12196	13855	40185	7224	0	371	371	4.31s	5351	5074	13855	36434	2109	6
psp_c_166	473	473	473	473	0.16s	128	44	9089	9092	0	0	473	473	0.16s	128	44	9089	9092	0	0	473	473	0.16s	102	18	9089	9128	0	0	473	473	0.16s	102	18	9089	9128	0	0	473	473	0.16s	128	44	9089	9092	0	0	473	473	0.17s	128	44	9089	9092	0	0
psp_c_167	373	373	373	373	0.27s	353	265	5435	5883	0	0	373	373	0.28s	382	213	5435	5929	0	1	373	373	0.17s	109	21	5435	5688	0	0	373	373	0.17s	109	21	5435	5688	0	0	373	373	0.28s	353	245	5435	5883	0	0	373	373	0.28s	353	245	5435	5883	0	0
psp_c_168	439	439	439	439	0.46s	567	494	9806	11741	3	0	439	439	0.48s	614	448	9806	11826	2	2	439	439	0.17s	104	31	9806	10044	2	0	439	439	0.18s	104	31	9806	10044	2	0	439	439	0.37s	405	282	9806	11459	6	0	439	439	0.36s	405	282	9806	11459	6	0
psp_c_169	328	328	328	328	0.25s	234	168	7602	8283	4	0	328	328	0.25s	234	121	7602	8283	4	1	328	328	0.18s	104	38	7602	7874	1	0	328	328	0.18s	104	38	7602	7874	1	0	328	328	0.25s	234	168	7602	8283	4	0	328	328	0.25s	234	168	7602	8283	4	0
psp_c_170	410	410	410	410	0.86s	1032	973	18063	23855	40	0	410	410	0.89s	1068	919	18063	24004	40	3	410	410	0.21s	89	30	18063	18498	0	0	410	410	0.21s	89	30	18063	18498	0	0	410	410	1.16s	1393	1293	18063	27780	150	0	410	410	1.03s	1249	1044	18063	27550	120	3
psp_c_171	321	321	321	321	0.17s	122	57	3470	3498	0	0	321	321	0.17s	122	57	3470	3498	0	0	321	321	0.16s	92	27	3470	3528	0	0	321	321	0.16s	92	27	3470	3528	0	0	321	321	0.17s	122	57	3470	3498	0	0	321	321	0.17s	122	57	3470	3498	0	0
psp_c_172	378	378	378	378	0.16s	115	46	8349	8374	0	0	378	378	0.16s	115	46	8349	8374	0	0	378	378	0.16s	97	28	8349	8406	0	0	378	378	0.16s	97	28	8349	8406	0	0	378	378	0.17s	115	46	8349	8374	0	0	378	378	0.18s	115	46	8349	8374	0	0
psp_c_173	397	397	397	397	0.26s	339	251	8188	8675	0	0	397	397	0.26s	342	246	8188	8677	0	1	397	397	0.16s	109	21	8188	8432	0	0	397	397	0.16s	109	21	8188	8432	0	0	397	397	0.26s	339	247	8188	8675	0	0	397	397	0.26s	339	247	8188	8675	0	0
psp_c_174	489	489	489	489	0.25s	232	156	14760	15118	0	0	489	489	0.25s	232	123	14760	15118	0	1	489	489	0.17s	99	23	14760	14923	1	0	489	489	0.17s	99	23	14760	14923	1	0	489	489	0.25s	232	156	14760	15118	0	0	489	489	0.25s	232	156	14760	15118	0	0
psp_c_175	288	288	288	288	0.20s	142	90	7082	7431	0	0	288	288	0.20s	142	90	7082	7431	0	0	288	288	0.17s	77	25	7082	7290	0	0	288	288	0.16s	77	25	7082	7290	0	0	288	288	0.21s	142	90	7082	7431	0	0	288	288	0.20s	142	90	7082	7431	0	0
psp_c_176	538	538	538	538	0.57s	805	724	16562	19140	0	0	538	538	0.60s	854	620	16562	19193	1	2	538	538	0.16s	101	20	16562	16892	0	0	538	538	0.16s	101	20	16562	16892	0	0	538	538	0.32s	400	264	16562	18069	0	0	538	538	0.33s	400	264	16562	18069	0	0
psp_c_177	261	261	261	261	0.20s	114	60	5980	6155	0	0	261	261	0.20s	114	60	5980	6155	0	0	261	261	0.20s	92	38	5980	6472	5	0	261	261	0.19s	92	38	5980	6472	5	0	261	261	0.20s	114	60	5980	6155	0	0	261	261	0.20s	114	60	5980	6155	0	0
psp_c_178	412	412	412	412	0.20s	178	121	9759	10352	1	0	412	412	0.19s	178	121	9759	10352	1	0	412	412	0.16s	84	27	9759	10024	0	0	412	412	0.15s	84	27	9759	10024	0	0	412	412	0.20s	178	121	9759	10352	1	0	412	412	0.20s	178	121	9759	10352	1	0
psp_c_179	362	362	362	362	0.24s	264	200	9481	10059	0	0	362	362	0.25s	270	187	9481	10078	0	1	362	362	0.17s	90	26	9481	9642	0	0	362	362	0.18s	90	26	9481	9642	0	0	362	362	0.24s	264	200	9481	10059	0	0	362	362	0.25s	264	200	9481	10059	0	0
psp_c_180	551	551	551	551	0.35s	401	315	14382	15166	0	0	551	551	0.37s	430	299	14382	15203	0	1	551	551	0.17s	121	35	14382	14570	1	0	551	551	0.18s	121	35	14382	14570	1	0	551	551	0.35s	401	245	14382	15166	0	0	551	551	0.36s	401	245	14382	15166	0	0
psp_c_181	454	456	456	456	0.75s	1562	1494	21725	46178	365	0	456	456	0.78s	1672	1501	21725	46653	361	3	456	456	0.66s	1769	1701	21725	39447	102	0	456	456	0.48s	1115	620	21725	34481	70	3	456	456	0.37s	539	418	21725	36574	86	0	456	456	0.36s	536	336	21725	36492	77	1
psp_c_182	360	376	376	376	1.21s	3971	3886	12297	28582	1623	0	376	376	1.25s	4278	3962	12297	28512	1708	5	376	376	0.37s	974	889	12297	19385	71	0	376	376	0.45s	1053	840	12297	21647	132	3	376	376	0.45s	1147	1012	12297	21927	147	0	376	376	0.54s	1407	1041	12297	23194	165	3
psp_c_183	447	461	461	461	2.99s	7988	7942	16286	39164	4295	0	461	461	2.65s	7034	6844	16286	36935	3572	5	461	461	0.64s	1367	1321	16286	32876	411	0	461	461	0.77s	1533	1304	16286	37160	558	4	461	461	0.45s	789	732	16286	30462	368	0	461	461	0.67s	1320	1208	16286	34646	509	3
psp_c_184	574	574	574	574	0.98s	1992	1920	19896	37571	888	0	574	574	1.09s	2445	2127	19896	38146	1014	4	574	574	0.42s	1288	1216	19896	29371	80	0	574	574	0.43s	1162	745	19896	29981	78	3	574	574	0.48s	1069	933	19896	36027	262	0	574	574	0.45s	708	526	19896	36516	272	1
psp_c_185	318	370	364	364	30.71s	61669	61602	18432	75880	36159	0	364	364	31.05s	62471	62227	18432	76441	36619	8	364	364	2.61s	5357	5290	18432	61323	2730	0	364	364	2.41s	4491	4341	18432	56690	2739	5	364	364	2.36s	4850	4741	18432	63532	2406	0	364	364	3.00s	5671	5377	18432	70391	3033	6
psp_c_186	408	410	410	410	1.06s	3021	2937	23596	44177	655	0	410	410	1.07s	3123	2850	23596	44102	640	4	410	410	0.60s	1977	1893	23596	30498	58	0	410	410	0.49s	1325	603	23596	30671	45	3	410	410	0.51s	1246	1106	23596	35666	158	0	410	410	0.40s	769	475	23596	34786	131	2
psp_c_187	585	585	585	585	0.46s	1526	1441	19318	28563	37	0	585	585	0.50s	1632	1370	19318	28875	38	3	585	585	0.18s	142	57	19318	21675	10	0	585	585	0.18s	142	57	19318	21675	10	0	585	585	0.23s	466	301	19318	23725	10	0	585	585	0.23s	466	301	19318	23725	10	0
psp_c_188	275	321	307	307	61.23s	115624	115563	19383	71444	65127	0	307	307	53.46s	104363	104039	19383	71121	58292	9	307	307	1.29s	2807	2746	19383	42935	1393	0	307	307	1.40s	2906	2622	19383	42535	1470	5	307	307	0.97s	1775	1682	19383	46130	874	0	307	307	1.74s	3496	3257	19383	57042	1777	5
psp_c_189	640	640	640	640	0.50s	1435	1361	16114	27375	40	0	640	640	0.51s	1548	1329	16114	27714	38	3	640	640	0.35s	1332	1258	16114	20266	8	0	640	640	0.39s	1321	443	16114	21650	9	3	640	640	0.45s	1680	1562	16114	24386	12	0	640	640	0.56s	1912	1282	16114	26314	29	4
psp_c_190	390	401	401	401	0.32s	777	712	9715	14256	167	0	401	401	0.34s	866	698	9715	14324	172	2	401	401	0.21s	394	329	9715	12799	40	0	401	401	0.19s	371	209	9715	12638	25	2	401	401	0.29s	753	657	9715	14136	96	0	401	401	0.28s	709	446	9715	14204	100	2
psp_c_191	492	493	493	493	0.13s	205	127	9016	9529	21	0	493	493	0.13s	205	121	9016	9529	21	1	493	493	0.15s	232	154	9016	10070	4	0	493	493	0.14s	234	66	9016	10092	5	1	493	493	0.13s	205	127	9016	9529	21	0	493	493	0.13s	205	127	9016	9529	21	0
psp_c_192	274	274	274	274	0.17s	323	252	4790	5532	10	0	274	274	0.18s	375	251	4790	5611	10	1	274	274	0.13s	115	44	4790	5258	2	0	274	274	0.13s	115	44	4790	5258	2	0	274	274	0.17s	323	238	4790	5532	10	0	274	274	0.17s	323	238	4790	5532	10	0
psp_c_193	623	623	623	623	0.07s	118	27	10124	10128	0	0	623	623	0.08s	118	27	10124	10128	0	0	623	623	0.08s	108	17	10124	10150	0	0	623	623	0.09s	108	17	10124	10150	0	0	623	623	0.07s	118	27	10124	10128	0	0	623	623	0.08s	118	27	10124	10128	0	0
psp_c_194	451	451	451	451	0.13s	231	174	8355	8898	7	0	451	451	0.12s	231	124	8355	8898	7	1	451	451	0.12s	86	29	8355	8609	1	0	451	451	0.13s	86	29	8355	8609	1	0	451	451	0.13s	231	174	8355	8898	7	0	451	451	0.13s	231	174	8355	8898	7	0
psp_c_195	475	475	475	475	0.21s	597	513	8852	10525	20	0	475	475	0.21s	642	433	8852	10579	21	2	475	475	0.13s	128	44	8852	9418	3	0	475	475	0.12s	128	44	8852	9418	3	0	475	475	0.17s	448	285	8852	10365	4	0	475	475	0.18s	448	285	8852	10365	4	0
psp_c_196	340	340	340	340	0.14s	196	142	6547	7201	0	0	340	340	0.14s	196	120	6547	7201	0	1	340	340	0.12s	83	29	6547	6827	0	0	340	340	0.12s	83	29	6547	6827	0	0	340	340	0.14s	196	142	6547	7201	0	0	340	340	0.14s	196	142	6547	7201	0	0
psp_c_197	564	564	564	564	0.16s	425	332	11036	11845	0	0	564	564	0.16s	440	305	11036	11860	0	1	564	564	0.11s	127	34	11036	11337	0	0	564	564	0.12s	127	34	11036	11337	0	0	564	564	0.16s	425	244	11036	11845	0	0	564	564	0.16s	425	244	11036	11845	0	0
psp_c_198	459	459	459	459	0.15s	294	240	5140	5941	0	0	459	459	0.16s	297	208	5140	5944	0	1	459	459	0.11s	92	38	5140	5311	1	0	459	459	0.11s	92	38	5140	5311	1	0	459	459	0.14s	294	240	5140	5941	0	0	459	459	0.15s	294	240	5140	5941	0	0
psp_c_199	417	417	417	417	0.12s	209	137	4690	5150	0	0	417	417	0.11s	209	123	4690	5150	0	1	417	417	0.10s	92	20	4690	4842	0	0	417	417	0.10s	92	20	4690	4842	0	0	417	417	0.12s	209	137	4690	5150	0	0	417	417	0.12s	209	137	4690	5150	0	0
psp_c_200	349	349	349	349	0.14s	223	160	7415	8130	5	0	349	349	0.14s	223	124	7415	8130	5	1	349	349	0.12s	89	26	7415	7617	0	0	349	349	0.12s	89	26	7415	7617	0	0	349	349	0.15s	223	160	7415	8130	5	0	349	349	0.14s	223	160	7415	8130	5	0
psp_c_201	461	461	461	461	0.12s	262	170	7697	7967	0	0	461	461	0.12s	262	123	7697	7967	0	1	461	461	0.11s	121	29	7697	7836	0	0	461	461	0.11s	121	29	7697	7836	0	0	461	461	0.12s	262	170	7697	7967	0	0	461	461	0.12s	262	170	7697	7967	0	0
psp_c_202	381	381	381	381	0.16s	323	244	8197	8896	6	0	381	381	0.16s	332	206	8197	8905	6	1	381	381	0.13s	123	44	8197	8440	2	0	381	381	0.13s	123	44	8197	8440	2	0	381	381	0.16s	323	244	8197	8896	6	0	381	381	0.15s	323	244	8197	8896	6	0
psp_c_203	392	392	392	392	0.14s	180	110	10422	10660	0	0	392	392	0.13s	180	110	10422	10660	0	0	392	392	0.12s	97	27	10422	10637	0	0	392	392	0.12s	97	27	10422	10637	0	0	392	392	0.13s	180	110	10422	10660	0	0	392	392	0.14s	180	110	10422	10660	0	0
psp_c_204	333	333	333	333	0.16s	332	268	5156	5854	2	0	333	333	0.17s	345	253	5156	5904	1	1	333	333	0.13s	94	30	5156	5337	0	0	333	333	0.12s	94	30	5156	5337	0	0	333	333	0.16s	332	247	5156	5854	2	0	333	333	0.16s	332	247	5156	5854	2	0
psp_c_205	560	560	560	560	0.12s	231	137	9290	9602	0	0	560	560	0.12s	231	123	9290	9602	0	1	560	560	0.10s	113	19	9290	9548	0	0	560	560	0.10s	113	19	9290	9548	0	0	560	560	0.12s	231	137	9290	9602	0	0	560	560	0.12s	231	137	9290	9602	0	0
psp_c_206	425	425	425	425	0.10s	140	53	6167	6181	0	0	425	425	0.10s	140	53	6167	6181	0	0	425	425	0.11s	124	37	6167	6213	0	0	425	425	0.12s	124	37	6167	6213	0	0	425	425	0.11s	140	53	6167	6181	0	0	425	425	0.11s	140	53	6167	6181	0	0
psp_c_207	481	481	481	481	0.12s	129	41	10370	10386	0	0	481	481	0.12s	129	41	10370	10386	0	0	481	481	0.12s	133	45	10370	10428	1	0	481	481	0.12s	133	45	10370	10428	1	0	481	481	0.12s	129	41	10370	10386	0	0	481	481	0.13s	129	41	10370	10386	0	0
psp_c_208	660	660	660	660	0.08s	118	28	10989	11023	0	0	660	660	0.08s	118	28	10989	11023	0	0	660	660	0.09s	106	16	10989	11085	0	0	660	660	0.08s	106	16	10989	11085	0	0	660	660	0.08s	118	28	10989	11023	0	0	660	660	0.08s	118	28	10989	11023	0	0
psp_c_209	619	619	619	619	0.09s	94	21	6787	6815	0	0	619	619	0.09s	94	21	6787	6815	0	0	619	619	0.08s	101	28	6787	6889	0	0	619	619	0.08s	101	28	6787	6889	0	0	619	619	0.08s	94	21	6787	6815	0	0	619	619	0.08s	94	21	6787	6815	0	0
psp_c_210	290	290	290	290	0.13s	175	115	6355	6697	0	0	290	290	0.14s	175	115	6355	6697	0	0	290	290	0.13s	102	42	6355	6671	1	0	290	290	0.13s	102	42	6355	6671	1	0	290	290	0.14s	175	115	6355	6697	0	0	290	290	0.13s	175	115	6355	6697	0	0
psp_c_211	434	445	445	445	4.71s	9817	9734	21620	61590	4809	0	445	445	5.33s	11085	10705	21620	63179	5582	6	445	445	0.93s	1436	1353	21620	36466	213	0	445	445	1.02s	1737	1325	21620	40156	286	4	445	445	0.93s	1537	1401	21620	40574	253	0	445	445	0.88s	1361	1036	21620	43493	249	3
psp_c_212	554	564	564	564	2.58s	3912	3830	20679	51931	2325	0	564	564	2.59s	4023	3727	20679	52252	2241	4	564	564	1.57s	2855	2773	20679	45032	623	0	564	564	0.89s	1448	1215	20679	39687	307	4	564	564	0.97s	1530	1397	20679	40011	383	0	564	564	1.05s	1722	1409	20679	41377	444	4
psp_c_213	709	710	710	710	3.42s	4740	4662	38809	99390	1394	0	710	710	3.41s	4769	4476	38809	101478	1347	5	710	710	1.46s	2062	1984	38809	62292	226	0	710	710	1.01s	1409	804	38809	57824	158	3	710	710	1.48s	1737	1615	38809	75337	248	0	710	710	2.02s	2762	2213	38809	87760	354	4
psp_c_214	618	624	624	624	19.11s	22946	22866	37308	181650	11969	0	624	624	18.50s	21588	21076	37308	177267	10865	7	624	624	3.31s	3433	3353	37308	94570	1264	0	624	624	1.84s	1924	1715	37308	72465	433	4	624	624	1.60s	2131	1988	37308	64500	440	0	624	624	1.56s	1752	1448	37308	68738	333	4
psp_c_215	573	573	573	573	0.52s	767	704	11281	17220	49	0	573	573	0.50s	794	657	11281	17486	47	2	573	573	0.23s	264	201	11281	13110	9	0	573	573	0.23s	268	80	11281	13288	10	1	573	573	0.32s	439	334	11281	16018	26	0	573	573	0.35s	439	319	11281	16040	23	1
psp_c_216	unsat		unsat		0.43s	464	464	0	0	0	0	unsat		0.43s	464	464	0	0	0	0	unsat		0.43s	464	464	0	0	0	0	unsat		0.43s	464	464	0	0	0	0	unsat		0.43s	464	464	0	0	0	0	unsat		0.43s	464	464	0	0	0	0
psp_c_217	275	365	362	362	95.13s	93168	93108	25194	147059	63154	0	362	362	92.99s	89825	89555	25194	147692	60358	9	362	362	2.64s	3513	3453	25194	79673	2088	0	362	362	2.99s	3750	3558	25194	93837	2319	5	362	362	3.45s	4655	4543	25194	86732	2861	0	362	362	3.24s	4160	3818	25194	88445	2379	5
psp_c_218	247	325	-	317	Time Out		539501	17133	107262	374296	0	-	317	Time Out		534416	17133	107160	371193	12	-	310	Time Out		445260	17133	178786	299346	0	-	314	Time Out		428974	17133	257603	284926	12	-	310	Time Out		399585	17133	162210	269921	0	-	309	Time Out		412967	17133	221219	275965	12
psp_c_219	761	761	761	761	1.60s	2594	2494	26665	47993	409	0	761	761	1.70s	2864	2573	26665	49089	447	4	761	761	0.65s	1061	961	26665	35203	54	0	761	761	0.59s	882	475	26665	34913	30	3	761	761	1.02s	1763	1605	26665	40807	102	0	761	761	0.78s	1230	811	26665	40781	88	3
psp_c_220	352	403	393	393	5.32s	8919	8841	21576	61519	3989	0	393	393	5.04s	8567	8209	21576	60109	3661	6	393	393	2.74s	4007	3929	21576	52578	2058	0	393	393	2.20s	3416	3140	21576	55676	1283	5	393	393	1.98s	3309	3173	21576	51504	1308	0	393	393	1.95s	3345	2846	21576	48649	1257	5
psp_c_221	559	559	559	559	0.16s	239	154	7799	8250	5	0	559	559	0.15s	239	124	7799	8250	5	1	559	559	0.12s	126	41	7799	8339	2	0	559	559	0.12s	126	41	7799	8339	2	0	559	559	0.16s	239	154	7799	8250	5	0	559	559	0.16s	239	154	7799	8250	5	0
psp_c_222	647	647	647	647	0.10s	133	33	7089	7115	0	0	647	647	0.11s	133	33	7089	7115	0	0	647	647	0.10s	113	13	7089	7167	0	0	647	647	0.10s	113	13	7089	7167	0	0	647	647	0.10s	133	33	7089	7115	0	0	647	647	0.11s	133	33	7089	7115	0	0
psp_c_223	573	573	573	573	0.14s	205	125	7684	8226	4	0	573	573	0.14s	205	124	7684	8226	4	1	573	573	0.11s	122	42	7684	8098	0	0	573	573	0.12s	122	42	7684	8098	0	0	573	573	0.14s	205	125	7684	8226	4	0	573	573	0.14s	205	125	7684	8226	4	0
psp_c_224	292	304	304	304	0.54s	1052	975	6058	9586	330	0	304	304	0.54s	1141	920	6058	9691	320	3	304	304	0.48s	830	753	6058	10882	130	0	304	304	0.56s	1007	749	6058	11453	191	3	304	304	0.45s	771	654	6058	10441	145	0	304	304	0.54s	944	755	6058	10737	205	3
psp_c_225	526	526	526	526	0.17s	325	234	7626	8364	0	0	526	526	0.17s	333	205	7626	8374	0	1	526	526	0.11s	120	29	7626	7766	0	0	526	526	0.12s	120	29	7626	7766	0	0	526	526	0.17s	325	234	7626	8364	0	0	526	526	0.17s	325	234	7626	8364	0	0
psp_c_226	357	357	357	357	0.18s	241	171	8315	8745	1	0	357	357	0.19s	247	164	8315	8764	1	1	357	357	0.16s	98	28	8315	8500	0	0	357	357	0.15s	98	28	8315	8500	0	0	357	357	0.19s	241	171	8315	8745	1	0	357	357	0.18s	241	171	8315	8745	1	0
psp_c_227	402	402	402	402	0.30s	552	470	8689	10109	17	0	402	402	0.31s	573	420	8689	10148	17	2	402	402	0.14s	131	49	8689	8907	2	0	402	402	0.14s	131	49	8689	8907	2	0	402	402	0.30s	560	419	8689	10458	12	0	402	402	0.31s	560	314	8689	10458	12	1
psp_c_228	515	515	515	515	0.30s	609	525	10345	12083	41	0	515	515	0.31s	662	496	10345	12144	40	2	515	515	0.14s	115	31	10345	10625	0	0	515	515	0.14s	115	31	10345	10625	0	0	515	515	0.35s	713	566	10345	12889	32	0	515	515	0.35s	707	437	10345	12917	29	2
psp_c_229	314	314	314	314	0.27s	541	470	5718	7200	1	0	314	314	0.29s	554	438	5718	7207	0	2	314	314	0.16s	109	38	5718	5991	0	0	314	314	0.16s	109	38	5718	5991	0	0	314	314	0.23s	376	285	5718	7007	0	0	314	314	0.24s	376	285	5718	7007	0	0
psp_c_230	321	321	321	321	0.24s	314	245	7317	8206	3	0	321	321	0.24s	351	226	7317	8315	1	1	321	321	0.19s	172	103	7317	8249	0	0	321	321	0.19s	172	64	7317	8249	0	1	321	321	0.24s	314	241	7317	8206	3	0	321	321	0.24s	314	241	7317	8206	3	0
psp_c_231	285	285	285	285	0.22s	330	251	7487	8125	0	0	285	285	0.23s	359	242	7487	8164	0	1	285	285	0.16s	130	51	7487	7815	2	0	285	285	0.15s	130	51	7487	7815	2	0	285	285	0.22s	330	246	7487	8125	0	0	285	285	0.23s	330	246	7487	8125	0	0
psp_c_232	494	494	494	494	0.14s	219	131	8425	8665	0	0	494	494	0.15s	219	124	8425	8665	0	1	494	494	0.12s	112	24	8425	8715	0	0	494	494	0.12s	112	24	8425	8715	0	0	494	494	0.15s	219	131	8425	8665	0	0	494	494	0.15s	219	131	8425	8665	0	0
psp_c_233	551	551	551	551	0.14s	163	90	7151	7289	0	0	551	551	0.14s	163	90	7151	7289	0	0	551	551	0.12s	91	18	7151	7281	0	0	551	551	0.12s	91	18	7151	7281	0	0	551	551	0.14s	163	90	7151	7289	0	0	551	551	0.13s	163	90	7151	7289	0	0
psp_c_234	279	279	279	279	0.13s	60	28	6312	6347	0	0	279	279	0.14s	60	28	6312	6347	0	0	279	279	0.13s	53	21	6312	6367	0	0	279	279	0.14s	53	21	6312	6367	0	0	279	279	0.14s	60	28	6312	6347	0	0	279	279	0.14s	60	28	6312	6347	0	0
psp_c_235	327	327	327	327	0.15s	93	34	5560	5595	0	0	327	327	0.14s	93	34	5560	5595	0	0	327	327	0.15s	85	26	5560	5631	0	0	327	327	0.15s	85	26	5560	5631	0	0	327	327	0.15s	93	34	5560	5595	0	0	327	327	0.15s	93	34	5560	5595	0	0
psp_c_236	348	348	348	348	0.21s	312	238	6690	7441	0	0	348	348	0.21s	339	221	6690	7483	0	1	348	348	0.13s	96	22	6690	6925	0	0	348	348	0.13s	96	22	6690	6925	0	0	348	348	0.21s	312	238	6690	7441	0	0	348	348	0.21s	312	238	6690	7441	0	0
psp_c_237	328	328	328	328	0.15s	81	40	5977	6065	0	0	328	328	0.14s	81	40	5977	6065	0	0	328	328	0.15s	63	22	5977	6113	0	0	328	328	0.15s	63	22	5977	6113	0	0	328	328	0.15s	81	40	5977	6065	0	0	328	328	0.14s	81	40	5977	6065	0	0
psp_c_238	422	422	422	422	0.13s	111	39	7340	7363	0	0	422	422	0.13s	111	39	7340	7363	0	0	422	422	0.12s	91	19	7340	7381	0	0	422	422	0.12s	91	19	7340	7381	0	0	422	422	0.12s	111	39	7340	7363	0	0	422	422	0.13s	111	39	7340	7363	0	0
psp_c_239	332	332	332	332	0.14s	147	99	5343	5898	2	0	332	332	0.15s	147	99	5343	5898	2	0	332	332	0.14s	65	17	5343	5485	0	0	332	332	0.13s	65	17	5343	5485	0	0	332	332	0.14s	147	99	5343	5898	2	0	332	332	0.15s	147	99	5343	5898	2	0
psp_c_240	434	434	434	434	0.25s	472	387	6208	7353	3	0	434	434	0.26s	489	371	6208	7368	2	2	434	434	0.14s	119	34	6208	6370	0	0	434	434	0.13s	119	34	6208	6370	0	0	434	434	0.29s	606	517	6208	7946	3	0	434	434	0.29s	615	434	6208	8001	3	2
psp_c_241	382	430	-	489	Time Out		416770	23712	71222	300003	0	-	489	Time Out		417749	23712	72066	300255	11	-	431	Time Out		480540	23712	92038	318349	0	-	416	Time Out		517651	23712	139754	344529	12	-	438	Time Out		414243	23712	94784	280813	0	-	418	Time Out		499695	23712	150610	332379	12
psp_c_242	355	431	-	449	Time Out		364106	31217	178134	255970	0	-	450	Time Out		367179	31217	179558	259289	11	425	425	76.30s	64902	64837	31217	215332	42929	0	425	425	105.25s	85428	85038	31217	242555	56743	10	425	425	110.57s	96030	95924	31217	234506	63179	0	425	425	98.92s	80165	79687	31217	240237	53411	10
psp_c_243	463	533	-	539	Time Out		410644	29888	239770	298857	0	-	539	Time Out		402115	29888	240546	292102	11	519	519	22.96s	27741	27670	29888	116992	17708	0	519	519	8.40s	10546	10191	29888	94225	6384	7	519	519	10.53s	13749	13610	29888	88869	8326	0	519	519	7.76s	9070	8637	29888	93627	4902	6
psp_c_244	472	514	508	508	161.72s	186790	186719	22371	135307	132353	0	508	508	157.56s	182968	182539	22371	135835	129629	10	508	508	6.54s	7866	7795	22371	67682	5155	0	508	508	5.50s	7042	6721	22371	65803	4195	6	508	508	5.68s	7458	7342	22371	66520	4611	0	508	508	4.74s	5929	5636	22371	67852	3249	6
psp_c_245	388	468	-	498	Time Out		335096	25881	87140	251351	0	-	498	Time Out		327366	25881	87870	245741	11	-	458	Time Out		393858	25881	164132	262950	0	-	455	Time Out		406756	25881	263327	272240	12	-	463	Time Out		426708	25881	147090	283262	0	-	453	Time Out		517912	25881	258815	344725	12
psp_c_246	543	574	574	574	6.96s	8226	8174	23013	85960	3882	0	574	574	7.76s	9239	9011	23013	86296	4193	6	574	574	1.70s	1794	1742	23013	59275	786	0	574	574	1.70s	1545	1387	23013	66281	785	4	574	574	1.54s	1528	1432	23013	63786	700	0	574	574	2.24s	2199	2042	23013	74913	981	4
psp_c_247	434	478	471	471	61.44s	83597	83513	17968	115559	54637	0	471	471	60.94s	83969	83370	17968	118013	54617	9	471	471	32.39s	42013	41929	17968	91542	25405	0	471	471	20.07s	31050	30641	17968	80717	18359	8	471	471	21.10s	33340	33181	17968	76722	20674	0	471	471	15.98s	22520	21956	17968	78721	13148	8
psp_c_248	372	443	-	431	Time Out		514165	25920	243003	363073	0	-	431	Time Out		512081	25920	241520	359956	12	430	430	80.85s	76849	76774	25920	152957	49050	0	430	430	33.57s	38162	37719	25920	120490	23442	9	430	430	44.42s	47846	47718	25920	106493	30079	0	430	430	31.29s	34388	33896	25920	118627	21136	8
psp_c_249	608	635	633	633	11.45s	12697	12614	29580	122336	7043	0	633	633	12.14s	13265	12859	29580	124648	7236	6	633	633	3.22s	3471	3388	29580	75468	1561	0	633	633	1.95s	1875	1562	29580	69884	598	4	633	633	2.77s	3155	3029	29580	71949	949	0	633	633	2.97s	3169	2859	29580	80932	1261	5
psp_c_250	unsat		unsat		0.45s	678	624	0	0	0	0	unsat		0.45s	678	624	0	0	0	0	unsat		0.45s	678	624	0	0	0	0	unsat		0.45s	678	624	0	0	0	0	unsat		0.46s	678	624	0	0	0	0	unsat		0.46s	678	624	0	0	0	0
psp_c_251	297	308	308	308	2.91s	4168	4087	8224	15152	2094	0	308	308	2.91s	4322	3958	8224	15339	2046	5	308	308	1.46s	1973	1892	8224	16906	598	0	308	308	1.61s	2253	1860	8224	18776	702	4	308	308	1.45s	2088	1956	8224	16940	1060	0	308	308	1.21s	1759	1568	8224	16923	829	4
psp_c_252	420	420	420	420	0.22s	265	192	7672	8237	0	0	420	420	0.21s	265	120	7672	8237	0	1	420	420	0.16s	123	50	7672	8090	5	0	420	420	0.16s	123	50	7672	8090	5	0	420	420	0.22s	265	192	7672	8237	0	0	420	420	0.22s	265	192	7672	8237	0	0
psp_c_253	509	509	509	509	0.43s	576	488	12760	14258	3	0	509	509	0.43s	594	370	12760	14290	3	2	509	509	0.17s	119	31	12760	13092	1	0	509	509	0.17s	119	31	12760	13092	1	0	509	509	0.32s	402	280	12760	14115	1	0	509	509	0.32s	402	280	12760	14115	1	0
psp_c_254	305	305	305	305	0.40s	495	408	3825	5043	0	0	305	305	0.38s	499	352	3825	5046	0	1	305	305	0.21s	153	66	3825	4158	4	0	305	305	0.21s	153	65	3825	4158	4	1	305	305	0.37s	452	312	3825	5167	4	0	305	305	0.37s	452	312	3825	5167	4	1
psp_c_255	599	599	599	599	0.32s	383	303	8063	9041	28	0	599	599	0.33s	417	259	8063	9144	28	1	599	599	0.12s	100	20	8063	8286	0	0	599	599	0.13s	100	20	8063	8286	0	0	599	599	0.31s	383	243	8063	9041	28	0	599	599	0.31s	383	243	8063	9041	28	0
psp_c_256	452	452	452	452	0.14s	102	58	6196	6404	0	0	452	452	0.14s	102	58	6196	6404	0	0	452	452	0.13s	75	31	6196	6342	0	0	452	452	0.12s	75	31	6196	6342	0	0	452	452	0.14s	102	58	6196	6404	0	0	452	452	0.14s	102	58	6196	6404	0	0
psp_c_257	319	319	319	319	0.42s	537	475	4906	6903	0	0	319	319	0.42s	552	442	4906	6931	0	2	319	319	0.17s	99	37	4906	5097	0	0	319	319	0.17s	99	37	4906	5097	0	0	319	319	0.32s	374	281	4906	6317	0	0	319	319	0.32s	374	281	4906	6317	0	0
psp_c_258	338	338	338	338	0.39s	459	389	6055	7841	1	0	338	338	0.41s	473	357	6055	7863	2	1	338	338	0.18s	115	45	6055	6298	1	0	338	338	0.18s	115	45	6055	6298	1	0	338	338	0.38s	418	337	6055	7618	1	0	338	338	0.39s	418	308	6055	7618	1	1
psp_c_259	396	396	396	396	0.20s	194	124	5061	5678	2	0	396	396	0.20s	194	124	5061	5678	2	0	396	396	0.16s	136	66	5061	5644	9	0	396	396	0.18s	136	66	5061	5644	9	1	396	396	0.20s	194	124	5061	5678	2	0	396	396	0.20s	194	124	5061	5678	2	0
psp_c_260	455	469	469	469	0.62s	858	782	13893	19929	110	0	469	469	0.63s	932	739	13893	19986	104	2	469	469	0.67s	889	813	13893	19918	52	0	469	469	0.54s	642	446	13893	20486	64	3	469	469	0.58s	715	584	13893	19834	59	0	469	469	0.58s	735	506	13893	19925	57	2
psp_c_261	306	306	306	306	0.16s	119	53	4037	4053	0	0	306	306	0.18s	119	53	4037	4053	0	0	306	306	0.16s	97	31	4037	4081	0	0	306	306	0.16s	97	31	4037	4081	0	0	306	306	0.16s	119	53	4037	4053	0	0	306	306	0.16s	119	53	4037	4053	0	0
psp_c_262	400	400	400	400	0.12s	105	35	4944	4958	0	0	400	400	0.13s	105	35	4944	4958	0	0	400	400	0.12s	86	16	4944	4978	0	0	400	400	0.13s	86	16	4944	4978	0	0	400	400	0.13s	105	35	4944	4958	0	0	400	400	0.13s	105	35	4944	4958	0	0
psp_c_263	377	377	377	377	0.22s	204	129	2912	3239	1	0	377	377	0.22s	204	121	2912	3239	1	1	377	377	0.18s	118	43	2912	3289	2	0	377	377	0.18s	118	43	2912	3289	2	0	377	377	0.23s	204	129	2912	3239	1	0	377	377	0.22s	204	129	2912	3239	1	0
psp_c_264	429	429	429	429	0.23s	244	166	6207	6802	6	0	429	429	0.21s	244	126	6207	6838	5	1	429	429	0.17s	125	47	6207	6930	2	0	429	429	0.16s	125	47	6207	6930	2	0	429	429	0.20s	244	166	6207	6802	6	0	429	429	0.21s	244	166	6207	6802	6	0
psp_c_265	263	263	263	263	0.29s	341	257	4128	5019	0	0	263	263	0.29s	344	229	4128	5015	0	1	263	263	0.20s	138	54	4128	4482	1	0	263	263	0.20s	138	54	4128	4482	1	0	263	263	0.29s	341	246	4128	5019	0	0	263	263	0.28s	341	246	4128	5019	0	0
psp_c_266	430	430	430	430	0.44s	620	536	11596	13061	0	0	430	430	0.45s	640	460	11596	13101	0	2	430	430	0.17s	114	30	11596	11791	0	0	430	430	0.18s	114	30	11596	11791	0	0	430	430	0.36s	449	276	11596	12924	0	0	430	430	0.35s	449	276	11596	12924	0	0
psp_c_267	563	563	563	563	0.22s	231	155	10909	11430	0	0	563	563	0.22s	231	123	10909	11430	0	1	563	563	0.14s	105	29	10909	11063	0	0	563	563	0.15s	105	29	10909	11063	0	0	563	563	0.22s	231	155	10909	11430	0	0	563	563	0.22s	231	155	10909	11430	0	0
psp_c_268	366	366	366	366	0.24s	242	171	6248	6789	0	0	366	366	0.23s	242	122	6248	6789	0	1	366	366	0.17s	105	34	6248	6466	0	0	366	366	0.17s	105	34	6248	6466	0	0	366	366	0.24s	242	171	6248	6789	0	0	366	366	0.24s	242	171	6248	6789	0	0
psp_c_269	247	247	247	247	0.23s	134	104	6096	7030	9	0	247	247	0.22s	134	104	6096	7030	9	0	247	247	0.18s	59	29	6096	6650	4	0	247	247	0.17s	59	29	6096	6650	4	0	247	247	0.22s	134	104	6096	7030	9	0	247	247	0.23s	134	104	6096	7030	9	0
psp_c_270	437	437	437	437	0.25s	279	208	8056	8629	1	0	437	437	0.27s	287	195	8056	8643	1	1	437	437	0.17s	101	30	8056	8258	1	0	437	437	0.17s	101	30	8056	8258	1	0	437	437	0.26s	279	208	8056	8629	1	0	437	437	0.26s	279	208	8056	8629	1	0
psp_c_271	445	498	497	497	12.09s	7563	7538	29159	207713	5904	0	497	497	12.53s	8168	8107	29159	206473	6405	6	497	497	2.94s	2418	2393	29159	110915	1654	0	497	497	6.94s	5531	5354	29159	157145	3616	6	497	497	2.84s	2665	2630	29159	111060	1845	0	497	497	3.25s	2949	2785	29159	122734	1917	5
psp_c_272	261	277	277	277	0.64s	1921	1856	11599	17901	661	0	277	277	0.70s	2201	1951	11599	18158	753	4	277	277	0.45s	1164	1099	11599	18359	119	0	277	277	0.43s	1094	738	11599	18360	74	3	277	277	0.43s	1079	964	11599	18314	194	0	277	277	0.39s	839	635	11599	18586	193	2
psp_c_273	575	598	579	579	25.05s	24685	24629	31626	189861	18406	0	579	579	29.82s	28648	28493	31626	194619	21722	7	579	579	1.05s	1551	1495	31626	74739	705	0	579	579	1.81s	2257	2143	31626	92355	1040	5	579	579	1.90s	2560	2487	31626	93560	1146	0	579	579	1.39s	1866	1663	31626	84675	753	4
psp_c_274	323	323	323	323	0.29s	782	703	11425	15159	24	0	323	323	0.29s	838	656	11425	15252	20	2	323	323	0.14s	133	54	11425	12003	1	0	323	323	0.14s	133	54	11425	12003	1	0	323	323	0.22s	469	336	11425	13905	21	0	323	323	0.22s	469	309	11425	13905	21	1
psp_c_275	486	486	486	486	0.84s	2797	2720	24496	40391	61	0	486	486	0.89s	2891	2589	24496	40872	70	4	486	486	0.32s	729	652	24496	28007	16	0	486	486	0.36s	697	550	24496	29453	31	3	486	486	0.37s	816	692	24496	30821	40	0	486	486	0.45s	1193	784	24496	31383	53	3
psp_c_276	unsat		unsat		0.57s	1042	1004	0	0	0	0	unsat		0.57s	1042	1004	0	0	0	0	unsat		0.56s	1042	1004	0	0	0	0	unsat		0.57s	1042	1004	0	0	0	0	unsat		0.58s	1042	1004	0	0	0	0	unsat		0.57s	1042	1004	0	0	0	0
psp_c_277	334	448	410	410	31.46s	41998	41930	26950	153198	26690	0	410	410	29.31s	40363	39987	26950	150121	25258	8	410	410	4.18s	4881	4813	26950	118375	2661	0	410	410	2.74s	3232	3032	26950	96178	1831	5	410	410	2.08s	2783	2666	26950	92342	1494	0	410	410	3.40s	4408	4091	26950	122420	2412	5
psp_c_278	578	587	587	587	0.51s	1206	1130	21528	32233	384	0	587	587	0.57s	1345	1097	21528	32446	376	3	587	587	0.27s	355	279	21528	28332	71	0	587	587	0.33s	621	499	21528	29933	107	3	587	587	0.34s	648	525	21528	29758	148	0	587	587	0.32s	616	470	21528	29837	141	1
psp_c_279	298	298	298	298	0.58s	1801	1749	16494	28862	92	0	298	298	0.59s	1855	1709	16494	29020	94	3	298	298	0.15s	102	50	16494	17441	4	0	298	298	0.14s	102	50	16494	17441	4	0	298	298	0.24s	453	356	16494	20701	34	0	298	298	0.25s	453	313	16494	20701	34	1
psp_c_280	436	451	451	451	1.98s	3561	3519	21621	48511	1745	0	451	451	1.85s	3353	3221	21621	48459	1569	4	451	451	0.32s	404	362	21621	30533	110	0	451	451	0.30s	383	265	21621	30523	92	2	451	451	0.53s	974	895	21621	38116	211	0	451	451	0.58s	1037	830	21621	38860	238	3
psp_c_281	207	207	207	207	0.13s	164	102	4466	4671	0	0	207	207	0.14s	164	102	4466	4671	0	0	207	207	0.13s	92	30	4466	4642	0	0	207	207	0.13s	92	30	4466	4642	0	0	207	207	0.16s	164	102	4466	4671	0	0	207	207	0.15s	164	102	4466	4671	0	0
psp_c_282	320	320	320	320	0.11s	106	44	3056	3076	0	0	320	320	0.11s	106	44	3056	3076	0	0	320	320	0.11s	76	14	3056	3176	0	0	320	320	0.11s	76	14	3056	3176	0	0	320	320	0.10s	106	44	3056	3076	0	0	320	320	0.10s	106	44	3056	3076	0	0
psp_c_283	302	302	302	302	0.16s	122	59	11033	11203	0	0	302	302	0.16s	122	59	11033	11203	0	0	302	302	0.16s	94	31	11033	11217	0	0	302	302	0.16s	94	31	11033	11217	0	0	302	302	0.15s	122	59	11033	11203	0	0	302	302	0.16s	122	59	11033	11203	0	0
psp_c_284	279	279	279	279	0.13s	95	41	4418	4473	0	0	279	279	0.13s	95	41	4418	4473	0	0	279	279	0.13s	79	25	4418	4513	0	0	279	279	0.13s	79	25	4418	4513	0	0	279	279	0.13s	95	41	4418	4473	0	0	279	279	0.13s	95	41	4418	4473	0	0
psp_c_285	454	454	454	454	0.14s	133	87	11624	12026	0	0	454	454	0.14s	133	87	11624	12026	0	0	454	454	0.12s	70	24	11624	11787	0	0	454	454	0.12s	70	24	11624	11787	0	0	454	454	0.14s	133	87	11624	12026	0	0	454	454	0.14s	133	87	11624	12026	0	0
psp_c_286	444	444	444	444	0.13s	191	111	12922	13148	0	0	444	444	0.13s	191	111	12922	13148	0	0	444	444	0.11s	92	12	12922	13078	0	0	444	444	0.12s	92	12	12922	13078	0	0	444	444	0.14s	191	111	12922	13148	0	0	444	444	0.12s	191	111	12922	13148	0	0
psp_c_287	416	416	416	416	0.18s	161	126	21796	23782	32	0	416	416	0.18s	161	123	21796	23782	32	1	416	416	0.15s	72	37	21796	22255	1	0	416	416	0.15s	72	37	21796	22255	1	0	416	416	0.19s	161	126	21796	23782	32	0	416	416	0.17s	161	126	21796	23782	32	0
psp_c_288	325	325	325	325	0.17s	247	181	10729	11357	16	0	325	325	0.18s	259	168	10729	11392	16	1	325	325	0.15s	102	36	10729	11066	1	0	325	325	0.15s	102	36	10729	11066	1	0	325	325	0.18s	247	181	10729	11357	16	0	325	325	0.18s	247	181	10729	11357	16	0
psp_c_289	336	336	336	336	0.25s	763	681	10793	13302	1	0	336	336	0.27s	810	637	10793	13365	1	2	336	336	0.13s	124	42	10793	11190	1	0	336	336	0.14s	124	42	10793	11190	1	0	336	336	0.20s	490	382	10793	12696	5	0	336	336	0.22s	490	308	10793	12696	5	1
psp_c_290	288	288	288	288	0.11s	122	52	2914	3033	0	0	288	288	0.13s	122	52	2914	3033	0	0	288	288	0.12s	101	31	2914	2994	0	0	288	288	0.13s	101	31	2914	2994	0	0	288	288	0.13s	122	52	2914	3033	0	0	288	288	0.14s	122	52	2914	3033	0	0
psp_c_291	346	346	346	346	0.13s	60	27	10795	10825	0	0	346	346	0.14s	60	27	10795	10825	0	0	346	346	0.13s	51	18	10795	10834	0	0	346	346	0.13s	51	18	10795	10834	0	0	346	346	0.13s	60	27	10795	10825	0	0	346	346	0.13s	60	27	10795	10825	0	0
psp_c_292	224	224	224	224	0.14s	229	162	5471	5844	0	0	224	224	0.14s	229	123	5471	5844	0	1	224	224	0.13s	96	29	5471	5630	0	0	224	224	0.12s	96	29	5471	5630	0	0	224	224	0.13s	229	162	5471	5844	0	0	224	224	0.15s	229	162	5471	5844	0	0
psp_c_293	275	275	275	275	0.14s	159	120	4780	5606	1	0	275	275	0.14s	159	120	4780	5606	1	0	275	275	0.12s	57	18	4780	5171	0	0	275	275	0.12s	57	18	4780	5171	0	0	275	275	0.14s	159	120	4780	5606	1	0	275	275	0.14s	159	120	4780	5606	1	0
psp_c_294	401	401	401	401	0.11s	42	20	6844	6892	0	0	401	401	0.12s	42	20	6844	6892	0	0	401	401	0.12s	37	15	6844	6915	0	0	401	401	0.12s	37	15	6844	6915	0	0	401	401	0.12s	42	20	6844	6892	0	0	401	401	0.12s	42	20	6844	6892	0	0
psp_c_295	326	326	326	326	0.15s	151	91	5313	5562	0	0	326	326	0.15s	151	91	5313	5562	0	0	326	326	0.14s	80	20	5313	5671	0	0	326	326	0.14s	80	20	5313	5671	0	0	326	326	0.14s	151	91	5313	5562	0	0	326	326	0.15s	151	91	5313	5562	0	0
psp_c_296	379	379	379	379	0.12s	66	23	9052	9101	0	0	379	379	0.12s	66	23	9052	9101	0	0	379	379	0.13s	55	12	9052	9126	0	0	379	379	0.13s	55	12	9052	9126	0	0	379	379	0.11s	66	23	9052	9101	0	0	379	379	0.12s	66	23	9052	9101	0	0
psp_c_297	357	357	357	357	0.14s	182	99	8456	8637	0	0	357	357	0.15s	182	99	8456	8637	0	0	357	357	0.14s	107	24	8456	8622	0	0	357	357	0.14s	107	24	8456	8622	0	0	357	357	0.16s	182	99	8456	8637	0	0	357	357	0.15s	182	99	8456	8637	0	0
psp_c_298	328	328	328	328	0.14s	106	64	10359	10682	0	0	328	328	0.16s	106	64	10359	10682	0	0	328	328	0.14s	68	26	10359	10645	0	0	328	328	0.13s	68	26	10359	10645	0	0	328	328	0.15s	106	64	10359	10682	0	0	328	328	0.15s	106	64	10359	10682	0	0
psp_c_299	352	352	352	352	0.13s	72	33	10618	10661	0	0	352	352	0.12s	72	33	10618	10661	0	0	352	352	0.13s	64	25	10618	10684	0	0	352	352	0.14s	64	25	10618	10684	0	0	352	352	0.13s	72	33	10618	10661	0	0	352	352	0.13s	72	33	10618	10661	0	0
psp_c_300	330	330	330	330	0.14s	119	46	8878	8943	0	0	330	330	0.13s	119	46	8878	8943	0	0	330	330	0.13s	101	28	8878	8944	0	0	330	330	0.13s	101	28	8878	8944	0	0	330	330	0.13s	119	46	8878	8943	0	0	330	330	0.11s	119	46	8878	8943	0	0
psp_c_301	407	412	412	412	2.85s	4689	4629	18679	44650	2328	0	412	412	2.89s	4795	4586	18679	44759	2326	5	412	412	1.70s	2373	2313	18679	34087	929	0	412	412	1.62s	2206	2026	18679	33723	932	4	412	412	1.92s	2844	2740	18679	42230	1083	0	412	412	1.33s	1865	1624	18679	36853	606	4
psp_c_302	unsat		unsat		0.68s	878	844	0	0	0	0	unsat		0.67s	878	844	0	0	0	0	unsat		0.68s	878	844	0	0	0	0	unsat		0.67s	878	844	0	0	0	0	unsat		0.66s	878	844	0	0	0	0	unsat		0.68s	878	844	0	0	0	0
psp_c_303	261	329	319	319	16.71s	29136	29082	23851	110131	19765	0	319	319	16.54s	28926	28672	23851	108804	19521	7	319	319	2.10s	4015	3961	23851	54042	2067	0	319	319	1.53s	2825	2657	23851	51840	1673	5	319	319	15.54s	27525	27444	23851	123834	17899	0	319	319	2.62s	4656	4284	23851	66980	2149	5
psp_c_304	268	346	-	344	Time Out		364856	23250	293439	285252	0	-	341	Time Out		364945	23250	315922	287523	11	333	333	146.73s	129604	129565	23250	350306	86486	0	333	333	132.18s	114107	113707	23250	319685	75503	10	333	333	233.42s	165081	165022	23250	338158	110234	0	333	333	168.35s	129757	129364	23250	319224	87056	10
psp_c_305	unsat		unsat		0.55s	790	708	0	0	0	0	unsat		0.54s	790	708	0	0	0	0	unsat		0.55s	790	708	0	0	0	0	unsat		0.54s	790	708	0	0	0	0	unsat		0.55s	790	708	0	0	0	0	unsat		0.54s	790	708	0	0	0	0
psp_c_306	286	296	288	288	6.98s	12752	12693	23284	60443	6617	0	288	288	7.09s	12904	12625	23284	60844	6607	6	288	288	1.78s	2929	2870	23284	39820	669	0	288	288	1.00s	1454	1270	23284	32670	514	4	288	288	2.40s	3963	3847	23284	48802	801	0	288	288	2.94s	5339	4995	23284	52957	1401	6
psp_c_307	261	342	-	311	Time Out		454716	18225	154742	291519	0	-	311	Time Out		465230	18225	155156	297769	11	309	309	112.57s	112727	112693	18225	135548	74905	0	309	309	110.16s	112108	111804	18225	146816	73351	10	309	309	209.50s	191506	191442	18225	146390	127844	0	309	309	121.65s	120530	120180	18225	171028	79307	10
psp_c_308	423	564	545	545	246.03s	85309	85284	40030	433121	63067	0	545	545	243.69s	83398	83247	40030	431921	61972	9	545	545	31.48s	20318	20293	40030	319314	14030	0	545	545	27.62s	17184	16970	40030	292422	11552	7	545	545	19.74s	12759	12721	40030	260439	8873	0	545	545	25.81s	13853	13650	40030	292407	9604	7
psp_c_309	458	503	503	503	10.75s	7901	7864	35934	159569	6315	0	503	503	11.03s	7906	7781	35934	160374	6289	5	503	503	2.87s	2806	2769	35934	104136	1635	0	503	503	4.44s	4263	4084	35934	137370	2468	5	503	503	3.18s	2876	2817	35934	105410	1538	0	503	503	3.62s	3302	3186	35934	128201	2140	5
psp_c_310	207	277	-	282	Time Out		663409	18684	93489	464834	0	-	282	Time Out		664305	18684	90638	463592	12	-	290	Time Out		377738	18684	315025	253218	0	-	267	Time Out		384546	18684	376307	253266	12	-	281	Time Out		402594	18684	284644	268003	0	-	267	Time Out		409108	18684	350775	273807	12
psp_c_311	220	220	220	220	0.15s	104	48	5734	5793	0	0	220	220	0.16s	104	48	5734	5793	0	0	220	220	0.15s	89	33	5734	5842	0	0	220	220	0.15s	89	33	5734	5842	0	0	220	220	0.15s	104	48	5734	5793	0	0	220	220	0.16s	104	48	5734	5793	0	0
psp_c_312	431	431	431	431	0.21s	352	272	11248	12234	12	0	431	431	0.22s	339	243	11248	12233	13	1	431	431	0.15s	129	49	11248	11969	1	0	431	431	0.15s	129	49	11248	11969	1	0	431	431	0.21s	352	250	11248	12234	11	0	431	431	0.22s	352	250	11248	12234	11	0
psp_c_313	328	328	328	328	0.22s	202	175	10144	11790	15	0	328	328	0.22s	203	169	10144	11786	13	1	328	328	0.15s	57	30	10144	10888	3	0	328	328	0.16s	57	30	10144	10888	3	0	328	328	0.22s	202	175	10144	11790	15	0	328	328	0.22s	202	175	10144	11790	15	0
psp_c_314	294	329	324	324	29.89s	50413	50401	7350	31560	33646	0	324	324	30.21s	50645	50540	7350	31438	33450	8	324	324	3.44s	5499	5487	7350	27855	3802	0	324	324	3.47s	5623	5562	7350	28630	4035	6	324	324	2.03s	3197	3181	7350	25039	2352	0	324	324	3.45s	5634	5585	7350	26529	4007	6
psp_c_315	274	294	294	294	8.93s	17093	17065	5913	12831	15108	0	294	294	8.93s	16739	16564	5913	12978	14640	7	294	294	0.49s	631	603	5913	12888	381	0	294	294	0.51s	673	612	5913	12974	402	3	294	294	0.63s	955	905	5913	12789	684	0	294	294	0.75s	1178	1112	5913	13320	864	3
psp_c_316	225	225	225	225	0.17s	82	32	5930	5985	0	0	225	225	0.17s	82	32	5930	5985	0	0	225	225	0.17s	74	24	5930	6010	0	0	225	225	0.17s	74	24	5930	6010	0	0	225	225	0.17s	82	32	5930	5985	0	0	225	225	0.17s	82	32	5930	5985	0	0
psp_c_317	465	465	465	465	0.16s	138	97	12282	13043	18	0	465	465	0.15s	138	97	12282	13043	18	0	465	465	0.13s	84	43	12282	12471	0	0	465	465	0.13s	84	43	12282	12471	0	0	465	465	0.16s	138	97	12282	13043	18	0	465	465	0.16s	138	97	12282	13043	18	0
psp_c_318	354	354	354	354	0.50s	642	602	13814	19499	170	0	354	354	0.48s	654	584	13814	19608	171	2	354	354	0.18s	81	41	13814	14437	4	0	354	354	0.18s	81	41	13814	14437	4	0	354	354	2.71s	3701	3640	13814	29969	2308	0	354	354	0.56s	650	570	13814	22311	206	2
psp_c_319	386	386	386	386	0.15s	104	32	12654	12694	0	0	386	386	0.16s	104	32	12654	12694	0	0	386	386	0.15s	93	21	12654	12701	0	0	386	386	0.15s	93	21	12654	12701	0	0	386	386	0.16s	104	32	12654	12694	0	0	386	386	0.16s	104	32	12654	12694	0	0
psp_c_320	274	274	274	274	3.58s	7839	7793	9110	19000	3979	0	274	274	3.88s	8424	8240	9110	19234	4288	6	274	274	0.21s	148	102	9110	11265	46	0	274	274	0.22s	148	72	9110	11265	46	1	274	274	0.58s	816	739	9110	15977	214	0	274	274	0.81s	1160	1012	9110	18457	315	3
psp_c_321	299	299	299	299	0.25s	246	207	4827	6452	75	0	299	299	0.26s	279	207	4827	6502	75	1	299	299	0.18s	76	37	4827	5885	17	0	299	299	0.17s	76	37	4827	5885	17	0	299	299	0.25s	246	207	4827	6452	75	0	299	299	0.25s	246	207	4827	6452	75	0
psp_c_322	276	276	276	276	0.19s	152	104	5266	5653	0	0	276	276	0.18s	152	104	5266	5653	0	0	276	276	0.16s	64	16	5266	5530	0	0	276	276	0.15s	64	16	5266	5530	0	0	276	276	0.18s	152	104	5266	5653	0	0	276	276	0.19s	152	104	5266	5653	0	0
psp_c_323	324	324	324	324	0.25s	190	181	10898	15308	99	0	324	324	0.25s	199	185	10898	15387	100	1	324	324	0.15s	40	31	10898	12606	17	0	324	324	0.15s	40	31	10898	12606	17	0	324	324	0.25s	190	181	10898	15308	99	0	324	324	0.25s	190	181	10898	15308	99	0
psp_c_324	371	371	371	371	0.17s	123	45	13708	13734	0	0	371	371	0.17s	123	45	13708	13734	0	0	371	371	0.16s	107	29	13708	13757	0	0	371	371	0.16s	107	29	13708	13757	0	0	371	371	0.16s	123	45	13708	13734	0	0	371	371	0.16s	123	45	13708	13734	0	0
psp_c_325	326	326	326	326	0.17s	215	130	2776	2926	0	0	326	326	0.17s	215	123	2776	2926	0	1	326	326	0.15s	104	19	2776	2979	2	0	326	326	0.14s	104	19	2776	2979	2	0	326	326	0.18s	215	130	2776	2926	0	0	326	326	0.17s	215	130	2776	2926	0	0
psp_c_326	304	304	304	304	0.13s	107	43	6301	6317	0	0	304	304	0.14s	107	43	6301	6317	0	0	304	304	0.14s	83	19	6301	6345	0	0	304	304	0.13s	83	19	6301	6345	0	0	304	304	0.13s	107	43	6301	6317	0	0	304	304	0.13s	107	43	6301	6317	0	0
psp_c_327	274	274	274	274	0.21s	175	132	7532	8419	11	0	274	274	0.21s	175	132	7532	8419	11	1	274	274	0.17s	82	39	7532	7793	0	0	274	274	0.17s	82	39	7532	7793	0	0	274	274	0.20s	175	132	7532	8419	11	0	274	274	0.21s	175	132	7532	8419	11	0
psp_c_328	248	255	255	255	0.62s	1253	1202	5383	11685	483	0	255	255	0.64s	1288	1207	5383	11642	491	3	255	255	0.34s	369	318	5383	9819	137	0	255	255	0.34s	379	291	5383	9880	135	2	255	255	0.55s	886	820	5383	11477	286	0	255	255	0.51s	758	673	5383	11094	206	2
psp_c_329	291	291	291	291	0.20s	216	138	2555	2806	1	0	291	291	0.18s	216	123	2555	2806	1	1	291	291	0.15s	112	34	2555	2754	1	0	291	291	0.14s	112	34	2555	2754	1	0	291	291	0.18s	216	138	2555	2806	1	0	291	291	0.19s	216	138	2555	2806	1	0
psp_c_330	238	238	238	238	0.17s	95	56	4820	5146	0	0	238	238	0.17s	95	56	4820	5146	0	0	238	238	0.17s	80	41	4820	5375	5	0	238	238	0.17s	80	41	4820	5375	5	0	238	238	0.17s	95	56	4820	5146	0	0	238	238	0.17s	95	56	4820	5146	0	0
psp_c_331	311	388	-	401	Time Out		429666	27389	160119	305968	0	-	400	Time Out		432878	27389	155675	308948	11	-	394	Time Out		497367	27389	164970	330416	0	-	381	Time Out		486271	27389	237978	323616	12	-	392	Time Out		557335	27389	154285	366422	0	-	381	Time Out		550114	27389	257097	366048	13
psp_c_332	317	336	326	326	118.22s	137879	137806	24694	137550	95146	0	326	326	119.96s	138475	138123	24694	138133	95522	10	326	326	25.56s	29922	29849	24694	102904	18979	0	326	326	15.10s	16814	16515	24694	76217	10090	7	-	369	Time Out		463198	24694	247866	312235	0	326	326	29.04s	29903	29458	24694	111566	18091	8
psp_c_333	332	410	404	404	410.78s	281452	281408	27937	190299	196355	0	404	404	387.47s	266971	266632	27937	188454	185445	11	404	404	9.26s	11474	11430	27937	125505	7534	0	404	404	9.45s	12045	11874	27937	119050	7766	7	404	404	3.71s	4891	4813	27937	92944	3139	0	404	404	5.91s	7567	7397	27937	103823	4893	6
psp_c_334	384	384	384	384	3.08s	3703	3622	23056	43209	1208	0	384	384	3.31s	3783	3546	23056	43373	1208	4	384	384	0.32s	232	151	23056	25781	45	0	384	384	0.58s	640	463	23056	29191	201	2	384	384	2.91s	3145	3022	23056	47601	719	0	384	384	2.32s	2815	2450	23056	46619	917	5
psp_c_335	362	426	413	413	46.77s	63112	63058	24651	110496	44439	0	413	413	44.67s	60675	60366	24651	110936	42398	8	413	413	3.67s	3608	3554	24651	59643	1814	0	413	413	5.37s	5636	5318	24651	69284	2899	6	413	413	3.03s	3615	3517	24651	59058	1852	0	413	413	5.31s	5525	5194	24651	69749	2965	6
psp_c_336	316	393	-	400	Time Out		453225	22956	135854	327863	0	-	400	Time Out		452061	22956	136258	326797	11	-	374	Time Out		396804	22956	174797	264129	0	-	375	Time Out		466250	22956	274212	310920	12	-	387	Time Out		429573	22956	174851	286561	0	-	371	Time Out		467619	22956	285582	308791	12
psp_c_337	242	296	-	299	Time Out		368985	17490	82217	260697	0	-	299	Time Out		376141	17490	83144	265676	11	-	287	Time Out		369883	17490	221637	248044	0	-	287	Time Out		391415	17490	317833	259625	12	-	335	Time Out		372057	17490	261355	250309	0	-	287	Time Out		388376	17490	335401	259649	12
psp_c_338	363	415	-	403	Time Out		389742	25454	218892	296293	0	-	403	Time Out		399496	25454	222484	302934	11	403	403	264.72s	188325	188263	25454	167146	124795	0	403	403	145.06s	133619	133282	25454	164646	86677	10	403	403	193.73s	161098	160989	25454	171910	104051	0	403	403	224.99s	187588	187208	25454	175610	123232	11
psp_c_339	362	429	-	443	Time Out		432062	29956	188044	309934	0	-	443	Time Out		430485	29956	188997	308120	11	-	415	Time Out		418439	29956	240572	271905	0	-	412	Time Out		384422	29956	291575	251728	12	-	417	Time Out		415902	29956	288917	272845	0	-	412	Time Out		392184	29956	280358	258688	12
psp_c_340	285	322	-	313	Time Out		504664	17129	175837	351546	0	-	313	Time Out		495759	17129	174253	343451	11	312	312	17.03s	16980	16921	17129	67583	10754	0	312	312	12.76s	13265	13054	17129	60810	8468	7	312	312	12.46s	13575	13484	17129	63172	8585	0	312	312	20.43s	21446	21076	17129	67559	13351	8
psp_c_341	405	405	405	405	0.54s	756	683	8903	12228	0	0	405	405	0.60s	786	622	8903	12266	0	2	405	405	0.17s	113	40	8903	9136	1	0	405	405	0.17s	113	40	8903	9136	1	0	405	405	0.34s	392	284	8903	10676	1	0	405	405	0.34s	392	284	8903	10676	1	0
psp_c_342	284	284	284	284	0.68s	640	604	13656	19213	33	0	284	284	0.70s	664	581	13656	19339	35	2	284	284	0.19s	72	36	13656	14142	1	0	284	284	0.21s	72	36	13656	14142	1	0	284	284	0.75s	774	716	13656	19226	40	0	284	284	0.80s	826	605	13656	19604	43	2
psp_c_343	263	263	263	263	0.31s	239	166	7254	8574	15	0	263	263	0.32s	239	132	7254	8574	15	1	263	263	0.24s	115	42	7254	7756	1	0	263	263	0.24s	115	42	7254	7756	1	0	263	263	0.32s	239	166	7254	8574	15	0	263	263	0.32s	239	166	7254	8574	15	0
psp_c_344	316	316	316	316	0.33s	453	367	8660	9991	2	0	316	316	0.36s	513	355	8660	10073	2	1	316	316	0.18s	126	40	8660	9250	3	0	316	316	0.18s	126	40	8660	9250	3	0	316	316	0.35s	463	294	8660	10678	10	0	316	316	0.35s	463	294	8660	10678	10	0
psp_c_345	282	282	282	282	1.66s	1816	1763	15974	26657	804	0	282	282	1.70s	1872	1706	15974	26775	810	3	282	282	0.20s	83	30	15974	16705	3	0	282	282	0.21s	83	30	15974	16705	3	0	282	282	0.43s	391	306	15974	19614	15	0	282	282	0.43s	391	305	15974	19614	15	1
psp_c_346	411	446	446	446	118.80s	91148	91130	20179	87449	71861	0	446	446	114.31s	88746	88623	20179	87183	70001	9	446	446	11.25s	11000	10982	20179	74882	7869	0	446	446	20.57s	21948	21835	20179	79590	15395	8	446	446	8.43s	8729	8700	20179	72055	6504	0	446	446	21.41s	22505	22334	20179	80142	15903	8
psp_c_347	280	280	280	280	0.43s	461	414	9271	12800	34	0	280	280	0.45s	484	377	9271	12831	34	2	280	280	0.19s	95	48	9271	10102	6	0	280	280	0.18s	95	48	9271	10102	6	0	280	280	0.45s	500	407	9271	12804	38	0	280	280	0.49s	549	392	9271	13086	41	1
psp_c_348	389	389	389	389	0.55s	786	713	15433	18458	1	0	389	389	0.56s	809	649	15433	18487	1	2	389	389	0.18s	104	31	15433	15665	0	0	389	389	0.19s	104	31	15433	15665	0	0	389	389	0.33s	375	275	15433	17065	0	0	389	389	0.32s	375	275	15433	17065	0	0
psp_c_349	401	451	444	444	340.68s	232693	232656	26487	140109	176441	0	444	444	317.65s	227934	227690	26487	140216	171401	10	444	444	37.51s	43045	43008	26487	116160	30431	0	444	444	45.35s	55038	54805	26487	126296	37699	9	444	444	17.53s	23698	23643	26487	105125	16710	0	444	444	52.08s	63046	62727	26487	121999	42664	9
psp_c_350	314	314	314	314	0.18s	151	93	9604	9870	1	0	314	314	0.19s	151	93	9604	9870	1	0	314	314	0.17s	88	30	9604	9767	0	0	314	314	0.17s	88	30	9604	9767	0	0	314	314	0.19s	151	93	9604	9870	1	0	314	314	0.20s	151	93	9604	9870	1	0
psp_c_351	379	379	379	379	0.17s	81	39	8618	8680	0	0	379	379	0.18s	81	39	8618	8680	0	0	379	379	0.18s	86	44	8618	8717	2	0	379	379	0.18s	86	44	8618	8717	2	0	379	379	0.17s	81	39	8618	8680	0	0	379	379	0.17s	81	39	8618	8680	0	0
psp_c_352	345	345	345	345	0.32s	377	299	9607	10454	2	0	345	345	0.34s	426	276	9607	10524	2	1	345	345	0.19s	123	45	9607	10019	3	0	345	345	0.19s	123	45	9607	10019	3	0	345	345	0.33s	377	246	9607	10454	2	0	345	345	0.32s	377	246	9607	10454	2	0
psp_c_353	215	215	215	215	0.21s	115	85	9512	10146	8	0	215	215	0.20s	115	85	9512	10146	8	0	215	215	0.18s	65	35	9512	9797	1	0	215	215	0.18s	65	35	9512	9797	1	0	215	215	0.21s	115	85	9512	10146	8	0	215	215	0.20s	115	85	9512	10146	8	0
psp_c_354	293	293	293	293	0.24s	265	174	3759	4021	0	0	293	293	0.24s	265	124	3759	4021	0	1	293	293	0.18s	113	22	3759	3939	0	0	293	293	0.17s	113	22	3759	3939	0	0	293	293	0.24s	265	174	3759	4021	0	0	293	293	0.25s	265	174	3759	4021	0	0
psp_c_355	322	322	322	322	0.17s	92	35	9540	9565	0	0	322	322	0.17s	92	35	9540	9565	0	0	322	322	0.16s	81	24	9540	9581	0	0	322	322	0.16s	81	24	9540	9581	0	0	322	322	0.18s	92	35	9540	9565	0	0	322	322	0.17s	92	35	9540	9565	0	0
psp_c_356	251	251	251	251	0.25s	200	166	7441	8262	2	0	251	251	0.26s	210	163	7441	8305	2	1	251	251	0.17s	68	34	7441	7697	3	0	251	251	0.18s	68	34	7441	7697	3	0	251	251	0.25s	200	166	7441	8262	2	0	251	251	0.25s	200	166	7441	8262	2	0
psp_c_357	267	267	267	267	0.21s	188	113	4985	5150	0	0	267	267	0.21s	188	113	4985	5150	0	0	267	267	0.18s	107	32	4985	5150	0	0	267	267	0.18s	107	32	4985	5150	0	0	267	267	0.22s	188	113	4985	5150	0	0	267	267	0.22s	188	113	4985	5150	0	0
psp_c_358	201	201	201	201	0.18s	90	41	3342	3385	0	0	201	201	0.19s	90	41	3342	3385	0	0	201	201	0.17s	78	29	3342	3407	0	0	201	201	0.18s	78	29	3342	3407	0	0	201	201	0.18s	90	41	3342	3385	0	0	201	201	0.19s	90	41	3342	3385	0	0
psp_c_359	386	386	386	386	0.32s	331	267	11512	12654	10	0	386	386	0.33s	355	259	11512	12696	10	1	386	386	0.18s	80	16	11512	11727	0	0	386	386	0.17s	80	16	11512	11727	0	0	386	386	0.32s	331	247	11512	12654	10	0	386	386	0.32s	331	247	11512	12654	10	0
psp_c_360	655	655	655	655	0.11s	94	18	8388	8388	0	0	655	655	0.11s	94	18	8388	8388	0	0	655	655	0.10s	89	13	8388	8393	0	0	655	655	0.11s	89	13	8388	8393	0	0	655	655	0.11s	94	18	8388	8388	0	0	655	655	0.12s	94	18	8388	8388	0	0
psp_c_361	441	523	513	513	26.16s	25778	25752	34019	178392	18656	0	513	513	29.24s	27976	27858	34019	179998	20277	7	513	513	5.18s	4878	4852	34019	129994	2994	0	513	513	7.12s	6151	6018	34019	147521	4038	6	513	513	6.58s	6079	6045	34019	148146	3925	0	513	513	7.53s	6285	6149	34019	151224	4122	6
psp_c_362	529	529	529	529	0.29s	949	870	11201	17061	28	0	529	529	0.30s	969	842	11201	17107	23	2	529	529	0.23s	603	524	11201	14677	15	0	529	529	0.20s	568	324	11201	14077	10	2	529	529	0.30s	1057	944	11201	15939	18	0	529	529	0.25s	712	434	11201	16143	13	2
psp_c_363	481	566	566	566	7.86s	5425	5394	30942	172076	4273	0	566	566	7.65s	5125	5023	30942	172512	4061	5	566	566	2.17s	1989	1958	30942	104035	1204	0	566	566	1.91s	1862	1752	30942	102221	1005	4	566	566	1.77s	1522	1469	30942	102651	1066	0	566	566	3.02s	2922	2781	30942	114575	1779	5
psp_c_364	341	372	360	360	2.29s	6512	6460	12293	27948	4049	0	360	360	2.33s	6516	6314	12293	28310	4009	5	360	360	0.42s	828	776	12293	21488	155	0	360	360	0.36s	649	522	12293	21189	165	3	360	360	0.39s	741	656	12293	20709	266	0	360	360	0.45s	848	680	12293	21950	348	2
psp_c_365	423	445	445	445	8.03s	13561	13499	23935	91457	6559	0	445	445	8.80s	14869	14563	23935	91607	7317	6	445	445	0.76s	1622	1560	23935	45272	296	0	445	445	0.83s	1628	1317	23935	49100	276	4	445	445	0.65s	933	837	23935	49355	341	0	445	445	0.88s	1814	1377	23935	55087	431	4
psp_c_366	411	419	419	419	0.33s	593	547	13127	19267	237	0	419	419	0.33s	627	528	13127	19310	228	2	419	419	0.29s	538	492	13127	19072	58	0	419	419	0.25s	396	210	13127	16968	22	2	419	419	0.28s	415	338	13127	19230	117	0	419	419	0.27s	415	329	13127	19204	113	1
psp_c_367	319	322	322	322	1.33s	3260	3205	17202	39850	1044	0	322	322	1.37s	3372	3181	17202	40366	1064	4	322	322	0.32s	682	627	17202	22240	74	0	322	322	0.41s	836	570	17202	27508	156	3	322	322	0.59s	1485	1400	17202	31094	189	0	322	322	0.65s	1698	1485	17202	32070	209	4
psp_c_368	346	346	346	346	0.24s	517	459	10605	12949	30	0	346	346	0.25s	574	448	10605	13145	30	2	346	346	0.16s	106	48	10605	11091	2	0	346	346	0.15s	106	48	10605	11091	2	0	346	346	0.33s	876	778	10605	14315	36	0	346	346	0.28s	621	445	10605	13585	31	2
psp_c_369	389	390	390	390	0.34s	991	909	14067	18954	210	0	390	390	0.37s	1110	871	14067	19005	204	3	390	390	0.21s	448	366	14067	17045	23	0	390	390	0.28s	782	334	14067	17938	39	2	390	390	0.31s	782	623	14067	19318	121	0	390	390	0.30s	774	543	14067	18808	100	2
psp_c_370	378	378	378	378	0.52s	1814	1732	14631	22266	51	0	378	378	0.55s	1913	1712	14631	22487	48	3	378	378	0.21s	496	414	14631	16729	2	0	378	378	0.23s	496	68	14631	16729	2	1	378	378	0.49s	1937	1776	14631	21046	18	0	378	378	0.60s	2310	1641	14631	21745	23	4
psp_c_371	213	213	213	213	0.13s	102	43	4400	4442	0	0	213	213	0.13s	102	43	4400	4442	0	0	213	213	0.14s	91	32	4400	4475	0	0	213	213	0.12s	91	32	4400	4475	0	0	213	213	0.13s	102	43	4400	4442	0	0	213	213	0.13s	102	43	4400	4442	0	0
psp_c_372	368	368	368	368	0.15s	105	71	11370	11889	9	0	368	368	0.17s	105	71	11370	11889	9	0	368	368	0.14s	62	28	11370	11760	0	0	368	368	0.15s	62	28	11370	11760	0	0	368	368	0.15s	105	71	11370	11889	9	0	368	368	0.16s	105	71	11370	11889	9	0
psp_c_373	553	553	553	553	0.11s	52	22	12321	12492	0	0	553	553	0.11s	52	22	12321	12492	0	0	553	553	0.12s	51	21	12321	12588	1	0	553	553	0.12s	51	21	12321	12588	1	0	553	553	0.11s	52	22	12321	12492	0	0	553	553	0.12s	52	22	12321	12492	0	0
psp_c_374	316	316	316	316	0.13s	93	38	8416	8459	0	0	316	316	0.14s	93	38	8416	8459	0	0	316	316	0.14s	95	40	8416	8487	1	0	316	316	0.13s	95	40	8416	8487	1	0	316	316	0.13s	93	38	8416	8459	0	0	316	316	0.13s	93	38	8416	8459	0	0
psp_c_375	327	327	327	327	0.26s	370	333	7936	10482	113	0	327	327	0.26s	385	339	7936	10541	118	1	327	327	0.15s	90	53	7936	8553	1	0	327	327	0.16s	90	53	7936	8553	1	0	327	327	0.28s	429	372	7936	11284	122	0	327	327	0.28s	429	353	7936	11284	122	1
psp_c_376	307	307	307	307	0.14s	127	57	5590	5629	0	0	307	307	0.15s	127	57	5590	5629	0	0	307	307	0.12s	110	40	5590	5692	0	0	307	307	0.14s	110	40	5590	5692	0	0	307	307	0.15s	127	57	5590	5629	0	0	307	307	0.15s	127	57	5590	5629	0	0
psp_c_377	365	365	365	365	0.14s	208	148	7669	8136	0	0	365	365	0.15s	208	124	7669	8136	0	1	365	365	0.11s	93	33	7669	7852	0	0	365	365	0.12s	93	33	7669	7852	0	0	365	365	0.14s	208	148	7669	8136	0	0	365	365	0.14s	208	148	7669	8136	0	0
psp_c_378	259	259	259	259	0.13s	100	48	5580	5738	1	0	259	259	0.16s	100	48	5580	5738	1	0	259	259	0.13s	94	42	5580	5760	2	0	259	259	0.13s	94	42	5580	5760	2	0	259	259	0.13s	100	48	5580	5738	1	0	259	259	0.14s	100	48	5580	5738	1	0
psp_c_379	371	371	371	371	0.12s	124	45	6142	6172	0	0	371	371	0.11s	124	45	6142	6172	0	0	371	371	0.12s	110	31	6142	6203	0	0	371	371	0.13s	110	31	6142	6203	0	0	371	371	0.11s	124	45	6142	6172	0	0	371	371	0.11s	124	45	6142	6172	0	0
psp_c_380	264	264	264	264	0.14s	160	113	6789	7246	0	0	264	264	0.14s	160	113	6789	7246	0	0	264	264	0.13s	74	27	6789	7016	0	0	264	264	0.12s	74	27	6789	7016	0	0	264	264	0.14s	160	113	6789	7246	0	0	264	264	0.14s	160	113	6789	7246	0	0
psp_c_381	254	254	254	254	0.12s	91	40	5378	5413	0	0	254	254	0.12s	91	40	5378	5413	0	0	254	254	0.12s	72	21	5378	5459	0	0	254	254	0.12s	72	21	5378	5459	0	0	254	254	0.13s	91	40	5378	5413	0	0	254	254	0.12s	91	40	5378	5413	0	0
psp_c_382	273	273	273	273	0.12s	28	12	2559	2659	0	0	273	273	0.13s	28	12	2559	2659	0	0	273	273	0.12s	28	12	2559	2664	0	0	273	273	0.12s	28	12	2559	2664	0	0	273	273	0.13s	28	12	2559	2659	0	0	273	273	0.12s	28	12	2559	2659	0	0
psp_c_383	288	288	288	288	0.12s	84	35	4529	4571	0	0	288	288	0.13s	84	35	4529	4571	0	0	288	288	0.12s	72	23	4529	4574	0	0	288	288	0.12s	72	23	4529	4574	0	0	288	288	0.12s	84	35	4529	4571	0	0	288	288	0.12s	84	35	4529	4571	0	0
psp_c_384	338	338	338	338	0.13s	101	37	8573	8604	0	0	338	338	0.13s	101	37	8573	8604	0	0	338	338	0.13s	91	27	8573	8634	0	0	338	338	0.12s	91	27	8573	8634	0	0	338	338	0.12s	101	37	8573	8604	0	0	338	338	0.11s	101	37	8573	8604	0	0
psp_c_385	317	317	317	317	0.12s	69	33	6516	6621	0	0	317	317	0.12s	69	33	6516	6621	0	0	317	317	0.12s	59	23	6516	6623	0	0	317	317	0.13s	59	23	6516	6623	0	0	317	317	0.13s	69	33	6516	6621	0	0	317	317	0.12s	69	33	6516	6621	0	0
psp_c_386	418	418	418	418	0.12s	99	32	6592	6610	0	0	418	418	0.12s	99	32	6592	6610	0	0	418	418	0.11s	79	12	6592	6639	0	0	418	418	0.12s	79	12	6592	6639	0	0	418	418	0.12s	99	32	6592	6610	0	0	418	418	0.13s	99	32	6592	6610	0	0
psp_c_387	376	376	376	376	0.11s	67	22	6184	6234	0	0	376	376	0.11s	67	22	6184	6234	0	0	376	376	0.11s	66	21	6184	6253	0	0	376	376	0.11s	66	21	6184	6253	0	0	376	376	0.11s	67	22	6184	6234	0	0	376	376	0.12s	67	22	6184	6234	0	0
psp_c_388	279	279	279	279	0.15s	129	57	10201	10271	0	0	279	279	0.16s	129	57	10201	10271	0	0	279	279	0.15s	102	30	10201	10287	0	0	279	279	0.15s	102	30	10201	10287	0	0	279	279	0.15s	129	57	10201	10271	0	0	279	279	0.15s	129	57	10201	10271	0	0
psp_c_389	426	426	426	426	0.16s	123	45	12953	13012	0	0	426	426	0.14s	123	45	12953	13012	0	0	426	426	0.15s	97	19	12953	13040	0	0	426	426	0.15s	97	19	12953	13040	0	0	426	426	0.15s	123	45	12953	13012	0	0	426	426	0.14s	123	45	12953	13012	0	0
psp_c_390	401	401	401	401	0.12s	85	33	4567	4592	0	0	401	401	0.11s	85	33	4567	4592	0	0	401	401	0.10s	79	27	4567	4633	0	0	401	401	0.11s	79	27	4567	4633	0	0	401	401	0.11s	85	33	4567	4592	0	0	401	401	0.12s	85	33	4567	4592	0	0
psp_c_391	250	323	314	314	34.61s	48508	48442	21275	92951	32623	0	314	314	34.33s	48497	48112	21275	93413	32313	8	314	314	12.64s	18521	18455	21275	111911	10416	0	314	314	6.78s	11452	11152	21275	84880	6555	7	314	314	7.52s	12750	12632	21275	80273	8138	0	314	314	7.96s	12238	12025	21275	82848	7375	7
psp_c_392	287	322	-	312	Time Out		571112	13060	124712	391436	0	-	312	Time Out		563838	13060	123692	385904	12	311	311	157.95s	197486	197409	13060	139113	128962	0	311	311	30.72s	47234	46847	13060	75532	29935	9	311	311	45.18s	79977	79852	13060	82951	51806	0	311	311	42.48s	66674	66152	13060	92814	42689	9
psp_c_393	331	337	331	331	4.95s	7864	7803	20035	52679	3615	0	331	331	5.09s	8120	7897	20035	53017	3674	6	331	331	0.37s	316	255	20035	24504	125	0	331	331	1.08s	1503	1276	20035	33161	377	4	331	331	1.25s	1806	1707	20035	31606	476	0	331	331	1.13s	1525	1327	20035	32585	440	4
psp_c_394	466	469	469	469	1.56s	3047	2963	22178	41117	1005	0	469	469	1.62s	3253	2944	22178	41522	985	4	469	469	1.03s	1748	1664	22178	33297	256	0	469	469	0.50s	893	463	22178	29733	57	3	469	469	0.86s	1480	1338	22178	33627	113	0	469	469	0.70s	1254	833	22178	32505	100	3
psp_c_395	393	393	393	393	1.71s	3245	3155	25055	44535	175	0	393	393	1.73s	3417	3065	25055	44876	174	4	393	393	0.48s	591	501	25055	30696	78	0	393	393	0.60s	826	589	25055	31431	96	3	393	393	1.56s	2451	2306	25055	41041	450	0	393	393	1.08s	1942	1403	25055	37984	283	4
psp_c_396	unsat		unsat		0.67s	606	568	0	0	0	0	unsat		0.68s	606	568	0	0	0	0	unsat		0.66s	606	568	0	0	0	0	unsat		0.67s	606	568	0	0	0	0	unsat		0.67s	606	568	0	0	0	0	unsat		0.67s	606	568	0	0	0	0
psp_c_397	402	588	524	524	101.08s	61370	61312	32630	226847	38454	0	524	524	93.65s	58688	58479	32630	227694	36127	8	524	524	20.24s	11640	11582	32630	241688	7993	0	524	524	22.58s	12349	12117	32630	276768	8428	7	524	524	15.42s	8991	8909	32630	213585	6319	0	524	524	8.76s	5772	5572	32630	170065	3925	6
psp_c_398	303	303	303	303	1.88s	3878	3826	17393	40249	1469	0	303	303	1.92s	3949	3797	17393	40230	1472	4	303	303	0.20s	108	56	17393	18235	2	0	303	303	0.20s	108	56	17393	18235	2	0	303	303	1.08s	2005	1928	17393	31401	322	0	303	303	0.94s	1705	1462	17393	31479	262	4
psp_c_399	224	315	-	306	Time Out		413619	18247	88886	295911	0	-	306	Time Out		406794	18247	89680	292261	11	290	290	143.70s	165853	165800	18247	193035	111042	0	290	290	72.91s	107260	106807	18247	158646	71102	10	290	290	97.69s	127111	127009	18247	162611	85272	0	290	290	132.16s	162557	162032	18247	181183	108310	11
psp_c_400	355	420	411	411	14.41s	20329	20269	22976	90978	11662	0	411	411	14.89s	20054	19820	22976	91520	11398	7	411	411	2.21s	3330	3270	22976	67592	1730	0	411	411	2.39s	3650	3333	22976	69350	1875	5	411	411	3.73s	5637	5534	22976	80091	3324	0	411	411	4.97s	7383	7119	22976	87343	4199	6
psp_c_401	327	327	327	327	0.15s	102	44	6922	6993	1	0	327	327	0.15s	102	44	6922	6993	1	0	327	327	0.14s	91	33	6922	7010	0	0	327	327	0.15s	91	33	6922	7010	0	0	327	327	0.16s	102	44	6922	6993	1	0	327	327	0.15s	102	44	6922	6993	1	0
psp_c_402	284	284	284	284	0.21s	262	216	6602	8014	1	0	284	284	0.22s	267	207	6602	8016	1	1	284	284	0.15s	86	40	6602	7081	2	0	284	284	0.15s	86	40	6602	7081	2	0	284	284	0.21s	262	216	6602	8014	1	0	284	284	0.22s	262	216	6602	8014	1	0
psp_c_403	491	491	491	491	0.12s	105	32	9028	9032	0	0	491	491	0.12s	105	32	9028	9032	0	0	491	491	0.12s	95	22	9028	9044	0	0	491	491	0.12s	95	22	9028	9044	0	0	491	491	0.12s	105	32	9028	9032	0	0	491	491	0.13s	105	32	9028	9032	0	0
psp_c_404	326	326	326	326	0.17s	168	98	6499	6705	0	0	326	326	0.17s	168	98	6499	6705	0	0	326	326	0.15s	99	29	6499	6658	0	0	326	326	0.14s	99	29	6499	6658	0	0	326	326	0.17s	168	98	6499	6705	0	0	326	326	0.16s	168	98	6499	6705	0	0
psp_c_405	304	304	304	304	0.16s	80	45	7143	7267	0	0	304	304	0.15s	80	45	7143	7267	0	0	304	304	0.13s	56	21	7143	7320	0	0	304	304	0.15s	56	21	7143	7320	0	0	304	304	0.14s	80	45	7143	7267	0	0	304	304	0.15s	80	45	7143	7267	0	0
psp_c_406	356	362	362	362	0.22s	329	253	5110	5791	25	0	362	362	0.24s	375	234	5110	5842	24	1	362	362	0.27s	389	313	5110	6864	16	0	362	362	0.27s	416	286	5110	6946	13	2	362	362	0.25s	329	242	5110	5791	25	0	362	362	0.23s	329	242	5110	5791	25	0
psp_c_407	324	324	324	324	1.17s	2282	2212	11079	16048	826	0	324	324	1.21s	2392	2200	11079	16205	830	4	324	324	0.19s	132	62	11079	11680	6	0	324	324	0.19s	132	62	11079	11680	6	0	324	324	0.59s	932	806	11079	16052	258	0	324	324	0.50s	856	619	11079	14941	72	2
psp_c_408	271	271	271	271	0.20s	168	118	6698	7061	0	0	271	271	0.19s	168	118	6698	7061	0	0	271	271	0.16s	82	32	6698	6918	0	0	271	271	0.16s	82	32	6698	6918	0	0	271	271	0.19s	168	118	6698	7061	0	0	271	271	0.18s	168	118	6698	7061	0	0
psp_c_409	393	393	393	393	0.17s	111	85	10642	11923	2	0	393	393	0.18s	111	85	10642	11923	2	0	393	393	0.16s	44	18	10642	11054	1	0	393	393	0.14s	44	18	10642	11054	1	0	393	393	0.19s	111	85	10642	11923	2	0	393	393	0.20s	111	85	10642	11923	2	0
psp_c_410	487	487	487	487	0.14s	62	42	13686	14338	0	0	487	487	0.15s	62	42	13686	14338	0	0	487	487	0.13s	33	13	13686	13882	0	0	487	487	0.13s	33	13	13686	13882	0	0	487	487	0.15s	62	42	13686	14338	0	0	487	487	0.14s	62	42	13686	14338	0	0
psp_c_411	325	325	325	325	0.14s	121	45	5209	5224	0	0	325	325	0.15s	121	45	5209	5224	0	0	325	325	0.14s	99	23	5209	5306	0	0	325	325	0.15s	99	23	5209	5306	0	0	325	325	0.15s	121	45	5209	5224	0	0	325	325	0.14s	121	45	5209	5224	0	0
psp_c_412	321	321	321	321	0.16s	134	50	7418	7433	0	0	321	321	0.16s	134	50	7418	7433	0	0	321	321	0.14s	116	32	7418	7480	0	0	321	321	0.15s	116	32	7418	7480	0	0	321	321	0.15s	134	50	7418	7433	0	0	321	321	0.16s	134	50	7418	7433	0	0
psp_c_413	333	344	344	344	0.39s	501	474	5741	10983	247	0	344	344	0.37s	476	428	5741	10902	217	2	344	344	0.36s	374	347	5741	10563	130	0	344	344	0.46s	606	547	5741	11511	261	3	344	344	0.43s	563	517	5741	11565	239	0	344	344	0.43s	541	468	5741	11407	224	2
psp_c_414	352	352	352	352	0.13s	83	28	7458	7493	0	0	352	352	0.14s	83	28	7458	7493	0	0	352	352	0.12s	69	14	7458	7522	0	0	352	352	0.14s	69	14	7458	7522	0	0	352	352	0.13s	83	28	7458	7493	0	0	352	352	0.14s	83	28	7458	7493	0	0
psp_c_415	185	185	185	185	0.16s	105	48	2327	2390	0	0	185	185	0.16s	105	48	2327	2390	0	0	185	185	0.16s	82	25	2327	2438	0	0	185	185	0.16s	82	25	2327	2438	0	0	185	185	0.16s	105	48	2327	2390	0	0	185	185	0.15s	105	48	2327	2390	0	0
psp_c_416	458	458	458	458	0.13s	132	42	8826	8847	0	0	458	458	0.13s	132	42	8826	8847	0	0	458	458	0.12s	106	16	8826	8867	0	0	458	458	0.13s	106	16	8826	8867	0	0	458	458	0.13s	132	42	8826	8847	0	0	458	458	0.13s	132	42	8826	8847	0	0
psp_c_417	307	307	307	307	0.14s	91	41	6041	6090	0	0	307	307	0.16s	91	41	6041	6090	0	0	307	307	0.14s	72	22	6041	6170	0	0	307	307	0.15s	72	22	6041	6170	0	0	307	307	0.15s	91	41	6041	6090	0	0	307	307	0.16s	91	41	6041	6090	0	0
psp_c_418	365	365	365	365	0.15s	101	72	8417	9187	6	0	365	365	0.15s	101	72	8417	9187	6	0	365	365	0.13s	58	29	8417	8875	4	0	365	365	0.13s	58	29	8417	8875	4	0	365	365	0.15s	101	72	8417	9187	6	0	365	365	0.15s	101	72	8417	9187	6	0
psp_c_419	298	298	298	298	0.15s	52	27	3714	3938	0	0	298	298	0.15s	52	27	3714	3938	0	0	298	298	0.15s	39	14	3714	4099	1	0	298	298	0.15s	39	14	3714	4099	1	0	298	298	0.14s	52	27	3714	3938	0	0	298	298	0.14s	52	27	3714	3938	0	0
psp_c_420	422	422	422	422	0.14s	34	21	20382	21586	0	0	422	422	0.14s	34	21	20382	21586	0	0	422	422	0.16s	24	11	20382	20802	0	0	422	422	0.15s	24	11	20382	20802	0	0	422	422	0.16s	34	21	20382	21586	0	0	422	422	0.16s	34	21	20382	21586	0	0
psp_c_421	396	469	458	458	29.10s	27423	27379	29083	136443	18949	0	458	458	29.57s	28735	28548	29083	136038	19598	7	458	458	8.64s	9122	9078	29083	104964	5024	0	458	458	10.04s	9843	9617	29083	112933	6065	7	458	458	7.04s	6951	6885	29083	101663	4392	0	458	458	8.47s	8368	8152	29083	111697	5046	6
psp_c_422	444	794	776	776	63.54s	14737	14705	60465	655190	10885	0	776	776	65.06s	14961	14830	60465	652995	10993	6	776	776	50.55s	16734	16702	60465	431131	11575	0	776	776	34.83s	11707	11432	60465	401335	8109	7	776	776	34.66s	12397	12335	60465	393382	8652	0	776	776	33.42s	12705	12443	60465	408906	8781	7
psp_c_423	359	401	401	401	11.28s	14155	14085	21852	55003	8230	0	401	401	11.69s	14549	14178	21852	55370	8186	6	401	401	1.11s	1282	1212	21852	32643	553	0	401	401	1.15s	1366	1150	21852	32802	519	4	401	401	1.19s	1487	1357	21852	34352	612	0	401	401	1.54s	1854	1554	21852	36777	624	4
psp_c_424	352	394	-	390	Time Out		436360	18228	120429	303035	0	-	390	Time Out		429832	18228	119696	298787	11	382	382	468.83s	377161	377097	18228	249802	251208	0	382	382	89.26s	85362	84978	18228	131363	56431	10	382	382	97.09s	97670	97565	18228	115384	64266	0	382	382	74.41s	81793	81212	18228	114322	53614	10
psp_c_425	unsat		unsat		0.83s	626	566	0	0	0	0	unsat		0.84s	626	566	0	0	0	0	unsat		0.83s	626	566	0	0	0	0	unsat		0.83s	626	566	0	0	0	0	unsat		0.83s	626	566	0	0	0	0	unsat		0.83s	626	566	0	0	0	0
psp_c_426	283	350	-	347	Time Out		456172	24920	165722	319576	0	-	347	Time Out		461721	24920	165437	322738	11	333	333	302.85s	302662	302605	24920	355604	202106	0	333	333	440.96s	339725	339153	24920	322065	223745	12	333	333	460.13s	380866	380761	24920	285140	255134	0	333	333	420.41s	326719	326198	24920	299041	216577	12
psp_c_427	305	314	308	308	21.33s	26414	26329	14587	47661	17747	0	308	308	21.76s	27232	26752	14587	48177	18072	7	308	308	4.55s	5175	5090	14587	33660	2876	0	308	308	2.07s	2479	2190	14587	28188	1115	5	308	308	4.60s	5740	5599	14587	39779	2582	0	308	308	2.71s	3853	3510	14587	32438	1473	5
psp_c_428	514	831	831	831	66.41s	7359	7341	58923	632602	6707	0	831	831	66.44s	7477	7433	58923	624906	6737	5	831	831	57.32s	18346	18328	58923	465007	12742	0	831	831	36.80s	12600	12339	58923	430509	8541	7	831	831	30.62s	10684	10656	58923	388725	7549	0	831	831	42.63s	13213	12984	58923	451403	9160	7
psp_c_429	529	529	529	529	0.89s	1005	948	20147	28075	57	0	529	529	0.91s	1033	862	20147	28158	59	3	529	529	0.16s	80	23	20147	20638	0	0	529	529	0.15s	80	23	20147	20638	0	0	529	529	0.70s	808	732	20147	26348	44	0	529	529	0.54s	632	439	20147	25165	30	2
psp_c_430	293	361	-	358	Time Out		426003	18970	132884	293797	0	-	358	Time Out		423343	18970	133644	292302	11	345	345	108.07s	162748	162674	18970	123548	106472	0	345	345	298.05s	320991	320588	18970	148221	211018	12	345	345	435.48s	406813	406680	18970	146310	267777	0	345	345	237.22s	264299	263751	18970	154743	172887	11
psp_c_431	416	416	416	416	0.30s	295	221	10396	11083	0	0	416	416	0.32s	345	204	10396	11144	0	1	416	416	0.18s	105	31	10396	10735	1	0	416	416	0.18s	105	31	10396	10735	1	0	416	416	0.30s	295	221	10396	11083	0	0	416	416	0.29s	295	221	10396	11083	0	0
psp_c_432	349	349	349	349	0.87s	1223	1152	14336	18306	15	0	349	349	0.90s	1294	1079	14336	18407	16	3	349	349	0.19s	104	33	14336	14668	0	0	349	349	0.19s	104	33	14336	14668	0	0	349	349	0.58s	748	618	14336	16436	2	0	349	349	0.58s	748	309	14336	16436	2	1
psp_c_433	293	372	369	369	351.58s	255515	255493	18011	115800	203134	0	369	369	350.51s	254667	254493	18011	115750	202907	10	369	369	17.18s	25904	25882	18011	85615	18967	0	369	369	17.66s	16992	16829	18011	94728	12681	7	369	369	9.68s	11962	11928	18011	73645	8788	0	369	369	22.35s	23463	23269	18011	86968	17106	8
psp_c_434	362	362	362	362	0.20s	182	112	6224	6464	0	0	362	362	0.19s	182	112	6224	6464	0	0	362	362	0.15s	92	22	6224	6391	0	0	362	362	0.16s	92	22	6224	6391	0	0	362	362	0.20s	182	112	6224	6464	0	0	362	362	0.21s	182	112	6224	6464	0	0
psp_c_435	353	361	359	359	15.20s	18404	18371	27053	59728	11668	0	359	359	15.03s	17894	17746	27053	59945	11407	7	359	359	4.49s	3956	3923	27053	60278	2876	0	359	359	6.27s	6050	5942	27053	58610	4280	6	359	359	10.16s	13397	13344	27053	73517	9488	0	359	359	3.53s	3277	3076	27053	56246	2046	5
psp_c_436	287	287	287	287	0.74s	829	769	11999	16453	57	0	287	287	0.75s	851	719	11999	16518	58	2	287	287	1.22s	1319	1259	11999	23086	903	0	287	287	4.20s	4205	4033	11999	32142	2329	5	287	287	4.24s	4238	4153	11999	29168	2593	0	287	287	2.88s	3006	2761	11999	27962	1534	5
psp_c_437	360	360	360	360	0.18s	91	39	10443	10468	0	0	360	360	0.17s	91	39	10443	10468	0	0	360	360	0.16s	75	23	10443	10521	0	0	360	360	0.17s	75	23	10443	10521	0	0	360	360	0.17s	91	39	10443	10468	0	0	360	360	0.17s	91	39	10443	10468	0	0
psp_c_438	267	267	267	267	0.29s	190	155	7374	9206	40	0	267	267	0.30s	207	154	7374	9283	42	1	267	267	0.20s	99	64	7374	8502	25	0	267	267	0.20s	99	64	7374	8502	25	0	267	267	0.29s	190	155	7374	9206	40	0	267	267	0.30s	190	155	7374	9206	40	0
psp_c_439	377	377	377	377	0.44s	439	380	11515	14293	4	0	377	377	0.44s	464	370	11515	14337	4	2	377	377	0.18s	91	32	11515	12090	3	0	377	377	0.19s	91	32	11515	12090	3	0	377	377	0.39s	374	293	11515	14272	9	0	377	377	0.39s	374	293	11515	14272	9	0
psp_c_440	257	260	258	258	102.63s	135497	135453	11094	57606	80569	0	258	258	88.81s	120909	120672	11094	56879	72229	9	258	258	5.82s	8475	8431	11094	33298	5290	0	258	258	5.52s	7061	6862	11094	36718	4359	6	258	258	8.15s	11060	10975	11094	44678	7195	0	258	258	6.00s	8293	8154	11094	38732	5437	6
psp_c_441	281	281	281	281	0.24s	195	159	8671	10022	3	0	281	281	0.24s	205	156	8671	10066	4	1	281	281	0.16s	62	26	8671	9079	2	0	281	281	0.17s	62	26	8671	9079	2	0	281	281	0.24s	195	159	8671	10022	3	0	281	281	0.23s	195	159	8671	10022	3	0
psp_c_442	325	325	325	325	1.08s	1258	1195	10647	13849	403	0	325	325	1.08s	1309	1178	10647	13975	399	3	325	325	0.35s	264	201	10647	11052	2	0	325	325	0.32s	264	201	10647	11052	2	0	325	325	0.90s	1077	978	10647	13632	159	0	325	325	0.88s	1106	856	10647	13787	166	3
psp_c_443	579	579	579	579	0.14s	96	29	14562	14599	0	0	579	579	0.14s	96	29	14562	14599	0	0	579	579	0.14s	86	19	14562	14611	0	0	579	579	0.15s	86	19	14562	14611	0	0	579	579	0.14s	96	29	14562	14599	0	0	579	579	0.13s	96	29	14562	14599	0	0
psp_c_444	243	243	243	243	0.19s	137	87	4309	4519	1	0	243	243	0.19s	137	87	4309	4519	1	0	243	243	0.17s	82	32	4309	4544	0	0	243	243	0.17s	82	32	4309	4544	0	0	243	243	0.19s	137	87	4309	4519	1	0	243	243	0.20s	137	87	4309	4519	1	0
psp_c_445	306	306	306	306	0.20s	149	97	2701	3098	1	0	306	306	0.20s	149	97	2701	3098	1	0	306	306	0.16s	78	26	2701	2920	0	0	306	306	0.16s	78	26	2701	2920	0	0	306	306	0.20s	149	97	2701	3098	1	0	306	306	0.21s	149	97	2701	3098	1	0
psp_c_446	354	354	354	354	0.19s	144	83	7757	8053	0	0	354	354	0.20s	144	83	7757	8053	0	0	354	354	0.16s	85	24	7757	8127	0	0	354	354	0.17s	85	24	7757	8127	0	0	354	354	0.18s	144	83	7757	8053	0	0	354	354	0.19s	144	83	7757	8053	0	0
psp_c_447	416	416	416	416	0.15s	116	40	5698	5715	0	0	416	416	0.15s	116	40	5698	5715	0	0	416	416	0.13s	97	21	5698	5724	0	0	416	416	0.13s	97	21	5698	5724	0	0	416	416	0.17s	116	40	5698	5715	0	0	416	416	0.14s	116	40	5698	5715	0	0
psp_c_448	416	416	416	416	0.17s	112	37	10366	10383	0	0	416	416	0.17s	112	37	10366	10383	0	0	416	416	0.16s	89	14	10366	10408	0	0	416	416	0.17s	89	14	10366	10408	0	0	416	416	0.17s	112	37	10366	10383	0	0	416	416	0.17s	112	37	10366	10383	0	0
psp_c_449	417	417	417	417	0.22s	293	205	8029	8467	0	0	417	417	0.24s	325	168	8029	8533	0	1	417	417	0.16s	119	31	8029	8255	0	0	417	417	0.14s	119	31	8029	8255	0	0	417	417	0.24s	293	205	8029	8467	0	0	417	417	0.23s	293	205	8029	8467	0	0
psp_c_450	362	362	362	362	0.40s	305	289	14525	20589	143	0	362	362	0.38s	308	289	14525	20617	143	1	362	362	0.19s	62	46	14525	15731	19	0	362	362	0.20s	62	46	14525	15731	19	0	362	362	0.88s	791	763	14525	24075	514	0	362	362	0.52s	454	405	14525	23287	226	1
psp_c_451	354	365	365	365	0.43s	774	709	14807	23452	241	0	365	365	0.43s	898	764	14807	23729	258	2	365	365	0.26s	275	210	14807	20496	65	0	365	365	0.25s	276	146	14807	20355	59	1	365	365	0.32s	542	440	14807	22979	142	0	365	365	0.33s	550	399	14807	23041	137	1
psp_c_452	395	420	419	419	1.67s	2706	2660	17401	47873	1836	0	419	419	1.63s	2764	2651	17401	48129	1784	4	419	419	0.62s	1054	1008	17401	38163	384	0	419	419	0.69s	1304	1133	17401	41347	414	4	419	419	0.65s	1113	1048	17401	41881	453	0	419	419	0.76s	1349	1160	17401	44679	521	3
psp_c_453	467	659	659	659	12.85s	2822	2811	40706	302122	2370	0	659	659	12.57s	2805	2776	40706	296732	2343	4	659	659	5.46s	3281	3270	40706	160097	2260	0	659	659	5.45s	3273	3145	40706	162950	2174	5	659	659	7.21s	4222	4199	40706	187632	2885	0	659	659	7.82s	4463	4339	40706	183826	3023	5
psp_c_454	469	498	493	493	1.73s	4095	4008	22933	55627	1827	0	493	493	1.84s	4511	4111	22933	56742	1898	5	493	493	1.00s	2474	2387	22933	46241	555	0	493	493	0.84s	1845	1325	22933	48880	389	4	493	493	0.78s	1527	1358	22933	44475	469	0	493	493	0.65s	1047	804	22933	43961	386	3
psp_c_455	300	304	304	304	0.59s	1194	1136	11188	20831	498	0	304	304	0.61s	1278	1170	11188	20882	527	3	304	304	0.29s	426	368	11188	15267	35	0	304	304	0.30s	477	282	11188	15410	41	2	304	304	0.39s	803	689	11188	17993	171	0	304	304	0.50s	1210	930	11188	20163	227	3
psp_c_456	598	609	609	609	0.26s	542	487	12539	18194	120	0	609	609	0.28s	615	472	12539	18421	119	2	609	609	0.26s	519	464	12539	18403	80	0	609	609	0.27s	606	358	12539	19099	88	2	609	609	0.28s	575	486	12539	18873	98	0	609	609	0.26s	530	440	12539	18959	101	1
psp_c_457	423	430	428	428	0.67s	1955	1886	15059	29597	499	0	428	428	0.77s	2348	2170	15059	30170	610	4	428	428	0.29s	413	344	15059	21010	60	0	428	428	0.31s	490	330	15059	21838	49	2	428	428	0.34s	686	568	15059	22674	71	0	428	428	0.36s	688	488	15059	23960	94	2
psp_c_458	401	402	402	402	0.58s	1676	1600	15820	27648	67	0	402	402	0.61s	1791	1563	15820	27925	68	3	402	402	0.24s	469	393	15820	18785	25	0	402	402	0.27s	521	309	15820	18737	17	2	402	402	0.42s	1259	1131	15820	21699	29	0	402	402	0.36s	878	555	15820	21640	25	2
psp_c_459	352	499	447	447	5.89s	6244	6227	22243	84950	5167	0	447	447	6.33s	6461	6390	22243	84069	5262	5	447	447	4.25s	3781	3764	22243	120517	2632	0	447	447	1.50s	1329	1264	22243	77200	891	4	447	447	1.26s	1360	1329	22243	67833	1032	0	447	447	2.08s	1995	1931	22243	86746	1432	4
psp_c_460	unsat		unsat		0.47s	1080	1002	0	0	0	0	unsat		0.48s	1080	1002	0	0	0	0	unsat		0.48s	1080	1002	0	0	0	0	unsat		0.48s	1080	1002	0	0	0	0	unsat		0.47s	1080	1002	0	0	0	0	unsat		0.48s	1080	1002	0	0	0	0
psp_c_461	418	418	418	418	0.18s	382	334	6187	7675	9	0	418	418	0.17s	390	311	6187	7692	8	1	418	418	0.12s	80	32	6187	6496	1	0	418	418	0.11s	80	32	6187	6496	1	0	418	418	0.18s	379	298	6187	7913	10	0	418	418	0.18s	379	298	6187	7913	10	0
psp_c_462	602	602	602	602	0.09s	102	25	11031	11040	0	0	602	602	0.10s	102	25	11031	11040	0	0	602	602	0.10s	91	14	11031	11058	0	0	602	602	0.09s	91	14	11031	11058	0	0	602	602	0.10s	102	25	11031	11040	0	0	602	602	0.10s	102	25	11031	11040	0	0
psp_c_463	457	457	457	457	0.12s	125	79	7563	7816	0	0	457	457	0.12s	125	79	7563	7816	0	0	457	457	0.12s	71	25	7563	7707	0	0	457	457	0.11s	71	25	7563	7707	0	0	457	457	0.12s	125	79	7563	7816	0	0	457	457	0.12s	125	79	7563	7816	0	0
psp_c_464	367	367	367	367	0.14s	90	70	7540	8247	0	0	367	367	0.13s	90	70	7540	8247	0	0	367	367	0.13s	47	27	7540	7992	2	0	367	367	0.12s	47	27	7540	7992	2	0	367	367	0.13s	90	70	7540	8247	0	0	367	367	0.14s	90	70	7540	8247	0	0
psp_c_465	316	316	316	316	0.15s	183	129	6813	7450	5	0	316	316	0.16s	183	124	6813	7450	5	1	316	316	0.16s	112	58	6813	7061	2	0	316	316	0.15s	112	58	6813	7061	2	0	316	316	0.15s	183	129	6813	7450	5	0	316	316	0.16s	183	129	6813	7450	5	0
psp_c_466	269	269	269	269	0.12s	66	26	5704	5741	0	0	269	269	0.12s	66	26	5704	5741	0	0	269	269	0.12s	60	20	5704	5749	0	0	269	269	0.13s	60	20	5704	5749	0	0	269	269	0.13s	66	26	5704	5741	0	0	269	269	0.12s	66	26	5704	5741	0	0
psp_c_467	423	423	423	423	0.15s	193	129	9166	9585	7	0	423	423	0.14s	193	129	9166	9585	7	0	423	423	0.13s	95	31	9166	9349	0	0	423	423	0.13s	95	31	9166	9349	0	0	423	423	0.14s	193	129	9166	9585	7	0	423	423	0.15s	193	129	9166	9585	7	0
psp_c_468	438	438	438	438	0.12s	129	47	6242	6274	0	0	438	438	0.13s	129	47	6242	6274	0	0	438	438	0.12s	112	30	6242	6308	0	0	438	438	0.12s	112	30	6242	6308	0	0	438	438	0.13s	129	47	6242	6274	0	0	438	438	0.12s	129	47	6242	6274	0	0
psp_c_469	365	365	365	365	0.15s	115	83	12601	14526	17	0	365	365	0.15s	115	83	12601	14526	17	0	365	365	0.14s	49	17	12601	12938	0	0	365	365	0.14s	49	17	12601	12938	0	0	365	365	0.15s	115	83	12601	14526	17	0	365	365	0.15s	115	83	12601	14526	17	0
psp_c_470	313	313	313	313	0.15s	100	49	5651	5817	5	0	313	313	0.14s	100	49	5651	5817	5	0	313	313	0.12s	83	32	5651	5772	0	0	313	313	0.14s	83	32	5651	5772	0	0	313	313	0.13s	100	49	5651	5817	5	0	313	313	0.14s	100	49	5651	5817	5	0
psp_c_471	275	275	275	275	0.13s	123	53	3803	3862	0	0	275	275	0.15s	123	53	3803	3862	0	0	275	275	0.13s	112	42	3803	3980	0	0	275	275	0.13s	112	42	3803	3980	0	0	275	275	0.13s	123	53	3803	3862	0	0	275	275	0.13s	123	53	3803	3862	0	0
psp_c_472	395	395	395	395	0.12s	113	62	4726	4821	0	0	395	395	0.12s	113	62	4726	4821	0	0	395	395	0.11s	75	24	4726	4864	0	0	395	395	0.11s	75	24	4726	4864	0	0	395	395	0.11s	113	62	4726	4821	0	0	395	395	0.13s	113	62	4726	4821	0	0
psp_c_473	346	346	346	346	0.14s	352	267	3930	4385	1	0	346	346	0.14s	394	233	3930	4457	0	1	346	346	0.11s	127	42	3930	4105	1	0	346	346	0.12s	127	42	3930	4105	1	0	346	346	0.15s	352	245	3930	4385	1	0	346	346	0.15s	352	245	3930	4385	1	0
psp_c_474	368	368	368	368	0.11s	55	25	2697	2762	0	0	368	368	0.12s	55	25	2697	2762	0	0	368	368	0.12s	62	32	2697	2864	0	0	368	368	0.12s	62	32	2697	2864	0	0	368	368	0.11s	55	25	2697	2762	0	0	368	368	0.11s	55	25	2697	2762	0	0
psp_c_475	252	252	252	252	0.15s	58	28	3321	3417	0	0	252	252	0.15s	58	28	3321	3417	0	0	252	252	0.15s	49	19	3321	3470	0	0	252	252	0.14s	49	19	3321	3470	0	0	252	252	0.15s	58	28	3321	3417	0	0	252	252	0.14s	58	28	3321	3417	0	0
psp_c_476	292	292	292	292	0.16s	172	103	3330	3558	0	0	292	292	0.16s	172	103	3330	3558	0	0	292	292	0.15s	92	23	3330	3620	1	0	292	292	0.15s	92	23	3330	3620	1	0	292	292	0.17s	172	103	3330	3558	0	0	292	292	0.17s	172	103	3330	3558	0	0
psp_c_477	296	296	296	296	0.13s	73	34	5222	5266	0	0	296	296	0.14s	73	34	5222	5266	0	0	296	296	0.13s	72	33	5222	5277	0	0	296	296	0.15s	72	33	5222	5277	0	0	296	296	0.14s	73	34	5222	5266	0	0	296	296	0.15s	73	34	5222	5266	0	0
psp_c_478	415	415	415	415	0.12s	117	49	7062	7073	0	0	415	415	0.12s	117	49	7062	7073	0	0	415	415	0.12s	104	36	7062	7105	0	0	415	415	0.12s	104	36	7062	7105	0	0	415	415	0.12s	117	49	7062	7073	0	0	415	415	0.12s	117	49	7062	7073	0	0
psp_c_479	303	303	303	303	0.14s	116	67	5625	5837	1	0	303	303	0.15s	116	67	5625	5837	1	0	303	303	0.16s	74	25	5625	5856	0	0	303	303	0.14s	74	25	5625	5856	0	0	303	303	0.13s	116	67	5625	5837	1	0	303	303	0.15s	116	67	5625	5837	1	0
psp_c_480	427	427	427	427	0.11s	118	40	6647	6666	0	0	427	427	0.12s	118	40	6647	6666	0	0	427	427	0.12s	103	25	6647	6687	0	0	427	427	0.11s	103	25	6647	6687	0	0	427	427	0.11s	118	40	6647	6666	0	0	427	427	0.12s	118	40	6647	6666	0	0
psp_c_481	361	433	420	420	8.95s	17123	17059	14956	39991	11631	0	420	420	9.11s	17574	17229	14956	40434	11714	7	420	420	2.06s	4910	4846	14956	36637	2954	0	420	420	1.55s	2886	2675	14956	35293	1652	5	420	420	1.77s	4074	3960	14956	36995	2557	0	420	420	1.22s	2644	2374	14956	35273	1596	4
psp_c_482	651	905	905	905	16.12s	3203	3182	53168	397946	2771	0	905	905	16.12s	3109	3029	53168	414271	2681	4	905	905	17.27s	6737	6716	53168	268394	4551	0	905	905	25.50s	8172	8007	53168	304907	5399	6	905	905	28.25s	8973	8937	53168	307747	6117	0	905	905	19.88s	7724	7451	53168	306357	5176	6
psp_c_483	363	426	402	402	59.00s	98663	98580	20635	144850	59536	0	402	402	63.89s	101773	101249	20635	149039	61113	9	402	402	6.25s	9928	9845	20635	80610	4408	0	402	402	5.14s	7988	7651	20635	80998	4251	6	402	402	4.73s	8142	8002	20635	68474	3594	0	402	402	7.32s	10824	10393	20635	97259	5010	7
psp_c_484	532	574	574	574	1.69s	3037	2983	24822	45252	1805	0	574	574	1.79s	3339	3160	24822	44801	1851	4	574	574	0.58s	684	630	24822	39170	255	0	574	574	0.61s	794	680	24822	39281	271	3	574	574	0.79s	1108	1021	24822	46150	493	0	574	574	0.82s	1096	924	24822	46580	494	3
psp_c_485	561	561	561	561	1.22s	2264	2186	18808	30306	256	0	561	561	1.27s	2323	2046	18808	30474	256	4	561	561	0.20s	135	57	18808	19461	6	0	561	561	0.18s	135	57	18808	19461	6	0	561	561	0.31s	447	332	18808	21774	37	0	561	561	0.30s	447	321	18808	21774	37	1
psp_c_486	390	586	568	568	154.26s	94491	94460	30986	268437	68584	0	568	568	180.92s	104074	103888	30986	268351	75525	9	568	568	20.12s	14043	14012	30986	235557	9569	0	568	568	21.76s	12903	12766	30986	242317	8896	7	568	568	15.16s	9976	9926	30986	203514	6932	0	568	568	18.69s	11640	11445	30986	234660	8077	7
psp_c_487	581	734	734	734	71.89s	17403	17367	43495	447082	15117	0	734	734	73.44s	17734	17614	43495	450144	15248	7	734	734	15.72s	9302	9266	43495	255297	6156	0	734	734	11.47s	7330	7149	43495	211829	4803	6	734	734	15.58s	8787	8731	43495	260181	5833	0	734	734	14.95s	8519	8215	43495	252908	5481	6
psp_c_488	462	485	483	483	2.71s	5719	5661	15773	25427	3440	0	483	483	2.75s	5801	5548	15773	25506	3332	5	483	483	0.46s	640	582	15773	27134	264	0	483	483	0.66s	1082	926	15773	30940	354	3	483	483	0.47s	717	613	15773	23352	194	0	483	483	0.60s	973	767	15773	24375	235	3
psp_c_489	351	397	382	382	249.25s	312415	312341	26324	180149	207369	0	382	382	275.76s	320184	319596	26324	183590	212447	11	382	382	9.88s	18438	18364	26324	79528	11306	0	382	382	6.55s	11373	11107	26324	80542	6570	7	382	382	45.32s	68599	68448	26324	124004	43604	0	382	382	7.82s	12652	12256	26324	89745	6390	7
psp_c_490	456	462	462	462	0.63s	1200	1133	13564	20854	119	0	462	462	0.64s	1246	1080	13564	20933	120	3	462	462	0.22s	269	202	13564	15404	17	0	462	462	0.22s	289	203	13564	15445	18	2	462	462	0.41s	683	597	13564	18782	58	0	462	462	0.44s	755	624	13564	19107	78	2
psp_c_491	563	563	563	563	0.14s	144	104	8407	8962	0	0	563	563	0.14s	144	104	8407	8962	0	0	563	563	0.11s	64	24	8407	8565	0	0	563	563	0.12s	64	24	8407	8565	0	0	563	563	0.14s	144	104	8407	8962	0	0	563	563	0.13s	144	104	8407	8962	0	0
psp_c_492	635	635	635	635	0.12s	171	93	9665	9810	0	0	635	635	0.12s	171	93	9665	9810	0	0	635	635	0.11s	100	22	9665	9814	0	0	635	635	0.11s	100	22	9665	9814	0	0	635	635	0.13s	171	93	9665	9810	0	0	635	635	0.13s	171	93	9665	9810	0	0
psp_c_493	485	503	503	503	0.72s	1039	1014	12409	18877	609	0	503	503	0.71s	1054	1009	12409	18985	608	3	503	503	0.21s	212	187	12409	16416	53	0	503	503	0.22s	214	124	12409	16369	54	1	503	503	0.40s	473	436	12409	17919	169	0	503	503	0.41s	502	456	12409	18110	179	1
psp_c_494	462	462	462	462	0.26s	588	501	9005	10707	28	0	462	462	0.28s	643	451	9005	10806	22	2	462	462	0.25s	555	468	9005	10673	12	0	462	462	0.25s	569	347	9005	10688	7	2	462	462	0.25s	529	377	9005	11118	23	0	462	462	0.25s	529	307	9005	11118	22	1
psp_c_495	350	353	353	353	0.20s	168	133	7823	10217	47	0	353	353	0.20s	168	127	7823	10217	47	1	353	353	0.16s	110	75	7823	9083	13	0	353	353	0.17s	114	73	7823	9089	9	1	353	353	0.20s	168	133	7823	10217	47	0	353	353	0.20s	168	133	7823	10217	47	0
psp_c_496	360	360	360	360	0.15s	79	29	6098	6140	0	0	360	360	0.14s	79	29	6098	6140	0	0	360	360	0.14s	69	19	6098	6151	0	0	360	360	0.14s	69	19	6098	6151	0	0	360	360	0.14s	79	29	6098	6140	0	0	360	360	0.15s	79	29	6098	6140	0	0
psp_c_497	275	333	323	323	9.52s	17273	17249	19170	59368	15262	0	323	323	10.22s	17957	17887	19170	59337	15841	7	323	323	3.77s	5097	5073	19170	58686	3817	0	323	323	2.58s	3596	3454	19170	53786	2546	5	323	323	8.73s	13616	13581	19170	68921	9862	0	323	323	4.88s	7083	6921	19170	62561	5183	6
psp_c_498	307	307	307	307	0.31s	497	423	6774	8417	8	0	307	307	0.32s	529	365	6774	8476	8	2	307	307	0.18s	126	52	6774	7116	2	0	307	307	0.18s	126	52	6774	7116	2	0	307	307	0.30s	451	314	6774	8676	6	0	307	307	0.30s	451	305	6774	8676	6	1
psp_c_499	364	364	364	364	0.18s	212	154	6442	6966	0	0	364	364	0.19s	212	123	6442	6966	0	1	364	364	0.15s	98	40	6442	6695	0	0	364	364	0.16s	98	40	6442	6695	0	0	364	364	0.19s	212	154	6442	6966	0	0	364	364	0.19s	212	154	6442	6966	0	0
psp_c_500	261	261	261	261	0.27s	413	355	7458	9455	8	0	261	261	0.29s	473	371	7458	9712	8	2	261	261	0.16s	82	24	7458	7737	0	0	261	261	0.16s	82	24	7458	7737	0	0	261	261	0.26s	391	280	7458	9381	3	0	261	261	0.26s	391	280	7458	9381	3	0
psp_c_501	276	276	276	276	0.20s	256	195	2942	3596	0	0	276	276	0.20s	261	189	2942	3607	0	1	276	276	0.15s	93	32	2942	3149	0	0	276	276	0.15s	93	32	2942	3149	0	0	276	276	0.21s	256	195	2942	3596	0	0	276	276	0.20s	256	195	2942	3596	0	0
psp_c_502	396	396	396	396	0.13s	78	47	5007	5185	1	0	396	396	0.13s	78	47	5007	5185	1	0	396	396	0.13s	60	29	5007	5208	1	0	396	396	0.13s	60	29	5007	5208	1	0	396	396	0.14s	78	47	5007	5185	1	0	396	396	0.13s	78	47	5007	5185	1	0
psp_c_503	286	286	286	286	4.61s	9855	9809	6828	14300	5305	0	286	286	4.57s	9799	9609	6828	14501	5318	6	286	286	0.19s	114	68	6828	7517	13	0	286	286	0.19s	114	68	6828	7517	13	0	286	286	0.51s	786	719	6828	10210	150	0	286	286	0.61s	995	811	6828	11452	247	3
psp_c_504	378	378	378	378	0.13s	68	31	3851	3904	0	0	378	378	0.13s	68	31	3851	3904	0	0	378	378	0.13s	59	22	3851	3969	0	0	378	378	0.12s	59	22	3851	3969	0	0	378	378	0.12s	68	31	3851	3904	0	0	378	378	0.13s	68	31	3851	3904	0	0
psp_c_505	417	417	417	417	0.17s	97	49	7006	7326	5	0	417	417	0.17s	97	49	7006	7326	5	0	417	417	0.16s	71	23	7006	7264	0	0	417	417	0.16s	71	23	7006	7264	0	0	417	417	0.16s	97	49	7006	7326	5	0	417	417	0.18s	97	49	7006	7326	5	0
psp_c_506	483	483	483	483	0.12s	124	37	7470	7475	0	0	483	483	0.12s	124	37	7470	7475	0	0	483	483	0.12s	113	26	7470	7495	0	0	483	483	0.12s	113	26	7470	7495	0	0	483	483	0.12s	124	37	7470	7475	0	0	483	483	0.11s	124	37	7470	7475	0	0
psp_c_507	505	505	505	505	0.12s	98	36	6278	6289	0	0	505	505	0.12s	98	36	6278	6289	0	0	505	505	0.12s	90	28	6278	6304	0	0	505	505	0.11s	90	28	6278	6304	0	0	505	505	0.11s	98	36	6278	6289	0	0	505	505	0.12s	98	36	6278	6289	0	0
psp_c_508	356	356	356	356	0.14s