Examples from CHC competition 2023

benchmark name	result LoAT ABMC_b	time LoAT ABMC_b	result LoAT ABMC	time LoAT ABMC	result LoAT BMC	time LoAT BMC	result LoAT ADCL	time LoAT ADCL	result Z3 BMC	time Z3 BMC	result Spacer	time Spacer	result Golem Split TPA	time Golem Split TPA	result Golem BMC	time Golem BMC	result Eldarica CEGAR	time Eldarica CEGAR	result Eldarica SYM	time Eldarica SYM
chc lia lin 23/chc-LIA-Lin_000.smt2	unknown	300.014	unknown	300.014	unknown	300.014	unknown	300.023	unknown	300.027	unknown	300.015	unknown	300.105	unknown	300.106	unknown	300.021	unknown	300.054
chc lia lin 23/chc-LIA-Lin_001.smt2	unknown	300.014	unknown	300.101	unknown	300.112	unknown	11.2318	unknown	300.102	unknown	300.095	unknown	300.105	unknown	300.118	sat	3.33384	unknown	300.11
chc lia lin 23/chc-LIA-Lin_002.smt2	sat	0.0630329	unknown	300.087	unknown	300.033	unknown	0.061905	unknown	300.015	unknown	300.017	unknown	300.015	unknown	300.104	sat	2.95663	unknown	300.042
chc lia lin 23/chc-LIA-Lin_003.smt2	sat	0.055381	unknown	300.014	sat	0.0831579	unknown	0.0649309	unknown	300.106	sat	9.74248	sat	0.334509	unknown	300.027	sat	2.83672	sat	2.40458
chc lia lin 23/chc-LIA-Lin_004.smt2	unknown	300.06	unknown	300.047	unknown	300.031	unknown	0.331048	unknown	300.023	unknown	300.115	unknown	300.015	unknown	300.026	unknown	300.071	unknown	300.022
chc lia lin 23/chc-LIA-Lin_005.smt2	sat	275.25	unknown	300.023	unknown	300.015	unknown	0.0614059	unknown	300.015	unknown	300.016	unknown	300.029	unknown	300.017	sat	2.9352	unknown	300.039
chc lia lin 23/chc-LIA-Lin_006.smt2	sat	0.12824	unknown	300.012	unknown	300.095	unknown	0.0860849	unknown	300.1	sat	0.317352	unknown	300.036	unknown	300.104	unknown	300.021	unknown	300.084
chc lia lin 23/chc-LIA-Lin_007.smt2	sat	0.0423371	unknown	300.022	unknown	300.098	unknown	0.0533071	unknown	300.019	sat	0.0392101	unknown	300.06	unknown	300.017	sat	2.63477	unknown	300.105
chc lia lin 23/chc-LIA-Lin_008.smt2	sat	0.06074	unknown	300.031	sat	0.294678	unknown	0.063145	unknown	300.016	sat	52.7585	sat	0.761477	unknown	300.018	sat	3.14898	sat	3.08006
chc lia lin 23/chc-LIA-Lin_009.smt2	unknown	300.056	unknown	300.039	unknown	300.08	unknown	0.208389	unknown	300.014	sat	3.06299	unknown	300.015	unknown	300.014	sat	6.6519	unknown	300.091
chc lia lin 23/chc-LIA-Lin_010.smt2	sat	0.113078	unknown	300.013	unknown	300.096	unknown	0.0802009	unknown	300.024	unknown	300.016	sat	0.020261	unknown	300.057	sat	2.21959	unknown	300.042
chc lia lin 23/chc-LIA-Lin_011.smt2	sat	0.053841	unknown	300.031	unknown	300.063	unknown	0.068383	unknown	300.015	sat	0.0636511	unknown	300.025	unknown	300.043	unknown	300.049	unknown	300.119
chc lia lin 23/chc-LIA-Lin_012.smt2	sat	0.0899439	unknown	300.016	sat	21.848	unknown	0.122076	unknown	300.016	unknown	300.015	sat	2.6986	unknown	300.028	sat	88.7133	sat	4.25265
chc lia lin 23/chc-LIA-Lin_013.smt2	unknown	300.098	unknown	300.031	unknown	300.017	unknown	0.107356	unknown	300.032	unknown	300.063	unknown	300.108	unknown	300.028	unknown	300.03	unknown	300.118
chc lia lin 23/chc-LIA-Lin_014.smt2	unknown	300.114	unknown	300.023	unknown	300.013	unknown	0.321595	unknown	300.07	unknown	300.069	unknown	300.022	unknown	300.017	sat	2.79655	unknown	300.069
chc lia lin 23/chc-LIA-Lin_015.smt2	sat	1.20914	unknown	300.024	sat	0.115914	unknown	0.0954269	unknown	300.024	unknown	300.015	sat	7.68007	unknown	300.088	unknown	300.127	sat	2.43489
chc lia lin 23/chc-LIA-Lin_016.smt2	unknown	300.105	unknown	300.102	unknown	300.055	unknown	0.11737	unknown	300.075	unknown	300.105	unknown	300.015	unknown	300.02	unknown	300.031	unknown	300.031
chc lia lin 23/chc-LIA-Lin_017.smt2	sat	0.169591	unknown	300.068	unknown	300.029	unknown	0.0975169	unknown	300.101	sat	49.9906	unknown	300.015	unknown	300.018	sat	31.3794	unknown	300.029
chc lia lin 23/chc-LIA-Lin_018.smt2	sat	0.0572349	unknown	300.022	sat	0.101984	unknown	0.0598879	unknown	300.019	sat	73.7524	sat	0.758442	unknown	300.027	sat	3.13435	sat	2.35636
chc lia lin 23/chc-LIA-Lin_019.smt2	unknown	300.109	unknown	300.031	unknown	300.101	unknown	300.087	unknown	300.021	unknown	300.026	unknown	300.069	unknown	300.104	sat	2.53251	unknown	300.117
chc lia lin 23/chc-LIA-Lin_020.smt2	sat	0.0809021	unknown	300.015	unknown	300.029	unknown	0.071743	unknown	300.104	unknown	300.021	unknown	300.025	unknown	300.114	sat	4.79067	unknown	300.106
chc lia lin 23/chc-LIA-Lin_021.smt2	unknown	300.013	unknown	300.014	unknown	300.013	unknown	0.0769359	unknown	300.101	unknown	300.016	unknown	300.026	unknown	300.119	unknown	300.026	unknown	300.075
chc lia lin 23/chc-LIA-Lin_022.smt2	unsat	0.0696791	unsat	0.0706261	unsat	0.048822	unsat	5.67657	unsat	0.050109	unsat	0.199479	unsat	0.0532031	unsat	0.019134	unsat	3.69071	unsat	2.18783
chc lia lin 23/chc-LIA-Lin_023.smt2	unsat	0.074805	unsat	0.0431109	unsat	0.0557709	unsat	0.058544	unsat	0.0293059	unsat	0.0438069	unsat	0.0157741	unsat	0.011455	unsat	2.72648	unsat	1.90027
chc lia lin 23/chc-LIA-Lin_024.smt2	unsat	0.0962139	unsat	0.0962829	unsat	0.0460701	unknown	0.121267	unsat	0.071317	unsat	0.0889199	unsat	0.0522461	unsat	0.021656	unsat	7.72942	unsat	2.05664
chc lia lin 23/chc-LIA-Lin_025.smt2	unsat	0.040774	unsat	0.039278	unsat	0.041354	unsat	0.0945239	unsat	0.027655	unsat	0.0322809	unsat	0.0120169	unsat	0.0139709	unsat	2.61778	unsat	1.95929
chc lia lin 23/chc-LIA-Lin_026.smt2	unsat	6.9593	unsat	6.95562	unsat	0.123126	unknown	2.72843	unsat	6.03769	unsat	3.90333	unsat	0.133305	unsat	0.618889	unsat	19.4879	unsat	3.58689
chc lia lin 23/chc-LIA-Lin_027.smt2	unsat	0.0406081	unsat	0.0404181	unsat	0.040611	unsat	0.0529699	unsat	0.027361	unsat	0.0322411	unsat	0.010538	unsat	0.0162199	unsat	2.42326	unsat	1.80643
chc lia lin 23/chc-LIA-Lin_028.smt2	unsat	0.054306	unsat	0.054474	unknown	300.104	unsat	0.0683461	unknown	300.025	unknown	300.014	unsat	1.07071	unknown	300.061	unknown	300.022	unsat	11.9698
chc lia lin 23/chc-LIA-Lin_029.smt2	unsat	0.0472251	unsat	0.045609	unsat	109.433	unsat	0.054545	unknown	300.021	unknown	300.025	unsat	12.3368	unknown	300.02	unsat	3.01513	unsat	145.277
chc lia lin 23/chc-LIA-Lin_030.smt2	unsat	83.844	unsat	82.3526	unsat	42.6656	unknown	0.294229	unsat	161.046	unsat	5.41088	unsat	0.34703	unknown	300.02	unknown	300.044	unsat	5.938
chc lia lin 23/chc-LIA-Lin_031.smt2	unknown	300.105	unknown	300.096	unknown	300.018	unknown	0.60295	unknown	300.026	unknown	300.049	unsat	11.8138	unknown	300.028	unsat	3.5697	unsat	10.5458
chc lia lin 23/chc-LIA-Lin_032.smt2	unknown	300.023	unknown	300.023	unknown	300.014	unknown	67.2296	unknown	300.03	unknown	300.094	unsat	87.4168	unknown	300.021	unknown	300.112	unsat	24.2437
chc lia lin 23/chc-LIA-Lin_033.smt2	unsat	0.0538021	unsat	0.0618731	unsat	38.5275	unsat	0.0580741	unknown	300.068	unknown	300.016	unsat	19.3824	unknown	300.035	unsat	2.80627	unsat	144.137
chc lia lin 23/chc-LIA-Lin_034.smt2	unknown	300.085	unknown	300.072	unknown	300.044	unknown	0.0749581	unknown	300.015	unknown	300.066	unknown	300.095	unknown	300.022	unknown	300.063	unknown	300.021
chc lia lin 23/chc-LIA-Lin_035.smt2	unsat	0.044928	unsat	0.0799841	unsat	7.55751	unsat	0.057673	unknown	300.059	unknown	300.021	unsat	3.6149	unknown	300.014	unknown	300.02	unsat	43.2876
chc lia lin 23/chc-LIA-Lin_036.smt2	unsat	0.103194	unsat	0.16961	unknown	300.017	unsat	0.082574	unknown	300.023	unknown	300.079	unsat	22.4064	unknown	300.107	unknown	300.028	unsat	149.13
chc lia lin 23/chc-LIA-Lin_037.smt2	unknown	300.113	unknown	300.014	unknown	300.109	unknown	14.5687	unknown	300.033	unknown	300.034	unknown	300.106	unknown	300.023	unknown	300.034	unknown	300.043
chc lia lin 23/chc-LIA-Lin_038.smt2	unsat	0.0593701	unsat	0.26668	unsat	201.639	unsat	0.0609979	unknown	300.021	unknown	300.061	unsat	51.0737	unknown	300.018	unsat	3.02635	unknown	300.039
chc lia lin 23/chc-LIA-Lin_039.smt2	unsat	0.0778441	unsat	0.249172	unknown	300.094	unsat	0.068669	unknown	300.081	unknown	300.061	unsat	24.418	unknown	300.105	unknown	300.061	unknown	300.057
chc lia lin 23/chc-LIA-Lin_040.smt2	unknown	300.027	unknown	300.014	unknown	300.024	unsat	37.234	unknown	300.038	unknown	300.023	unsat	8.63954	unknown	300.02	unknown	300.035	unsat	15.0487
chc lia lin 23/chc-LIA-Lin_041.smt2	unsat	0.0581521	unsat	0.0906639	unsat	50.1067	unsat	0.0612551	unknown	300.015	unknown	300.085	unsat	84.0822	unknown	300.024	unsat	2.83989	unsat	149.483
chc lia lin 23/chc-LIA-Lin_042.smt2	unknown	300.011	unknown	300.028	unsat	16.1982	unknown	0.061239	unknown	300.113	unknown	300.017	unsat	120.345	unknown	300.027	unknown	300.038	unsat	49.5879
chc lia lin 23/chc-LIA-Lin_043.smt2	unsat	0.0555919	unsat	0.0522119	unknown	300.015	unsat	0.064125	unknown	300.024	unknown	300.085	unknown	300.036	unknown	300.018	unknown	300.022	unknown	300.07
chc lia lin 23/chc-LIA-Lin_044.smt2	unsat	0.069241	unsat	0.314535	unsat	188.376	unsat	0.067896	unknown	300.105	unknown	300.045	unsat	40.4985	unknown	300.113	unsat	3.20156	unknown	300.058
chc lia lin 23/chc-LIA-Lin_045.smt2	unknown	300.086	unknown	300.027	unsat	1.06757	unknown	0.317878	unknown	300.107	unknown	300.015	unsat	8.95947	unknown	300.026	unsat	2.80025	unsat	9.96956
chc lia lin 23/chc-LIA-Lin_046.smt2	unsat	0.121382	unsat	0.127742	unknown	300.015	unsat	0.111556	unknown	300.038	unknown	300.017	unknown	300.037	unknown	300.035	unknown	300.12	unknown	300.087
chc lia lin 23/chc-LIA-Lin_047.smt2	unsat	0.163902	unsat	1.17897	unknown	300.025	unsat	0.143985	unknown	300.017	unknown	300.114	unknown	300.016	unknown	300.012	unknown	300.11	unknown	300.031
chc lia lin 23/chc-LIA-Lin_048.smt2	unknown	300.012	unknown	300.021	unknown	300.041	unknown	0.0862719	unknown	300.016	unknown	300.042	unknown	300.026	unknown	300.014	unknown	300.11	unknown	300.027
chc lia lin 23/chc-LIA-Lin_049.smt2	unsat	0.058987	unsat	0.0636429	unknown	300.015	unsat	0.0623569	unknown	300.03	unknown	300.078	unknown	300.087	unknown	300.022	unsat	2.9441	unknown	300.077
chc lia lin 23/chc-LIA-Lin_050.smt2	unknown	300.012	unknown	300.018	unknown	300.015	unknown	300.03	unknown	300.078	unknown	300.016	unknown	300.039	unknown	300.104	unknown	300.029	unknown	300.116
chc lia lin 23/chc-LIA-Lin_051.smt2	unknown	300.018	unknown	300.06	unknown	300.023	unknown	0.081845	unknown	300.024	unknown	300.017	unknown	300.036	unknown	300.028	unsat	2.86432	unknown	300.044
chc lia lin 23/chc-LIA-Lin_052.smt2	unsat	0.0600761	unsat	0.059304	unsat	0.173417	unsat	0.075585	unsat	0.614459	unsat	87.231	unsat	0.214787	unsat	1.14577	unsat	13.7927	unsat	3.95605
chc lia lin 23/chc-LIA-Lin_053.smt2	sat	0.086276	unknown	300.03	unknown	300.02	unknown	0.090107	unknown	300.084	unknown	300.016	sat	0.022164	unknown	300.015	sat	2.40201	unknown	300.033
chc lia lin 23/chc-LIA-Lin_054.smt2	unknown	300.012	unknown	300.047	unknown	300.024	unknown	300.02	unknown	300.066	unknown	300.026	sat	0.0252851	unknown	300.022	sat	2.97844	unknown	300.084
chc lia lin 23/chc-LIA-Lin_055.smt2	unsat	0.090286	unsat	0.0888089	unsat	0.0882791	unsat	0.101632	unsat	0.032872	unsat	0.038722	unsat	0.0130339	unsat	0.02063	unsat	2.84632	unsat	2.17616
chc lia lin 23/chc-LIA-Lin_056.smt2	sat	0.074514	unknown	300.021	unknown	300.015	unknown	0.080217	unknown	300.015	unknown	300.099	sat	0.0150611	unknown	300.083	sat	2.64763	unknown	300.113
chc lia lin 23/chc-LIA-Lin_057.smt2	unsat	0.056906	unsat	0.0581279	unsat	0.052031	unsat	0.0759939	unsat	0.029436	unsat	0.043395	unsat	0.010657	unsat	0.0160501	unsat	2.58743	unsat	1.91894
chc lia lin 23/chc-LIA-Lin_058.smt2	unsat	0.066084	unsat	0.0696991	unsat	0.0617991	unsat	0.074373	unsat	0.071506	unsat	0.154494	unsat	0.196644	unsat	0.020547	unsat	3.13883	unsat	2.27077
chc lia lin 23/chc-LIA-Lin_059.smt2	unsat	0.053537	unsat	0.054011	unsat	0.0534291	unsat	0.0654581	unsat	0.030155	unsat	0.0399609	unsat	0.0137809	unsat	0.015637	unsat	2.72393	unsat	1.97308
chc lia lin 23/chc-LIA-Lin_060.smt2	unknown	300.019	unknown	300.038	unknown	300.022	unknown	0.122493	unknown	300.041	sat	0.0376101	sat	0.020313	unknown	300.017	sat	2.59424	unknown	300.038
chc lia lin 23/chc-LIA-Lin_061.smt2	unknown	300.024	unknown	300.014	unknown	300.022	unknown	300.019	unknown	300.016	sat	0.164145	unknown	300.049	unknown	300.02	unknown	300.031	unknown	300.08
chc lia lin 23/chc-LIA-Lin_062.smt2	unknown	300.012	unknown	300.089	unknown	300.065	unknown	300.103	unknown	300.02	unknown	300.025	unknown	300.015	unknown	300.094	unknown	300.121	unknown	300.083
chc lia lin 23/chc-LIA-Lin_063.smt2	unknown	300.067	unknown	300.074	unknown	300.014	unknown	0.176761	unknown	300.038	unknown	300.024	unknown	300.089	unknown	300.014	unknown	300.094	unknown	300.021
chc lia lin 23/chc-LIA-Lin_064.smt2	unsat	0.0596681	unsat	0.0611299	unsat	37.2735	unsat	0.073118	unknown	300.015	unknown	300.025	unsat	1.51082	unknown	300.016	unknown	300.065	unsat	28.1578
chc lia lin 23/chc-LIA-Lin_065.smt2	sat	0.086659	unknown	300.022	unknown	300.015	unknown	0.0943161	unknown	300.013	unknown	0.0740311	unknown	300.022	unknown	300.109	sat	3.09257	unknown	300.07
chc lia lin 23/chc-LIA-Lin_066.smt2	sat	12.1047	unknown	300.023	unknown	300.016	unknown	3.25025	unknown	300.106	sat	0.178877	sat	0.192256	unknown	300.113	sat	5.22931	unknown	300.072
chc lia lin 23/chc-LIA-Lin_067.smt2	unknown	300.022	unknown	300.114	unknown	300.024	unknown	1.88878	unknown	300.025	sat	0.838966	unknown	300.095	unknown	300.016	sat	4.82676	unknown	300.034
chc lia lin 23/chc-LIA-Lin_068.smt2	sat	0.0901731	unknown	300.105	unknown	300.03	unknown	0.0933581	unknown	300.105	unknown	300.024	sat	0.0210779	unknown	300.016	sat	2.34221	unknown	300.121
chc lia lin 23/chc-LIA-Lin_069.smt2	unsat	0.05815	unsat	0.05972	unsat	0.054511	unsat	0.0897949	unsat	0.03511	unsat	0.080501	unsat	0.015605	unsat	0.019114	unsat	2.77765	unsat	2.10003
chc lia lin 23/chc-LIA-Lin_070.smt2	unknown	300.08	unknown	300.021	unknown	300.015	unknown	0.0879919	unknown	300.035	unknown	300.072	unknown	300.06	unknown	300.104	sat	3.79528	unknown	300.082
chc lia lin 23/chc-LIA-Lin_071.smt2	unsat	0.094172	unsat	0.0546421	unsat	0.051331	unsat	0.073825	unsat	0.0313109	unsat	0.0588981	unsat	0.018257	unsat	0.015854	unsat	2.70196	unsat	2.06896
chc lia lin 23/chc-LIA-Lin_072.smt2	unsat	0.057233	unsat	0.0569181	unsat	0.053798	unsat	0.094973	unsat	0.0331301	unsat	0.0548751	unsat	0.0231011	unsat	0.016463	unsat	2.69837	unsat	2.1023
chc lia lin 23/chc-LIA-Lin_073.smt2	sat	0.323775	unknown	300.025	unknown	300.114	unknown	0.157687	unknown	300.085	sat	0.0822889	sat	0.0272109	unknown	300.063	sat	4.63129	unknown	300.025
chc lia lin 23/chc-LIA-Lin_074.smt2	sat	0.096633	unknown	300.112	unknown	300.015	unknown	0.0797541	unknown	300.024	sat	0.202014	unknown	300.015	unknown	300.017	sat	3.49651	unknown	300.058
chc lia lin 23/chc-LIA-Lin_075.smt2	sat	0.0823119	unknown	300.043	unknown	300.025	unknown	0.078971	unknown	300.021	unknown	300.016	unknown	300.026	unknown	300.103	unknown	300.108	unknown	300.032
chc lia lin 23/chc-LIA-Lin_076.smt2	sat	0.112943	unknown	300.071	unknown	300.073	unknown	0.0744	unknown	300.02	unknown	300.096	unknown	300.02	unknown	300.026	unknown	300.127	unknown	300.111
chc lia lin 23/chc-LIA-Lin_077.smt2	sat	0.125536	unknown	300.026	unknown	300.015	unknown	0.079346	unknown	300.014	unknown	300.016	unknown	300.106	unknown	300.019	unknown	300.022	unknown	300.052
chc lia lin 23/chc-LIA-Lin_078.smt2	unknown	300.016	unknown	300.015	unknown	300.015	unknown	5.21206	unknown	300.036	sat	0.0921401	unknown	300.035	unknown	300.015	unknown	300.075	unknown	300.085
chc lia lin 23/chc-LIA-Lin_079.smt2	sat	0.078757	unknown	300.089	unknown	300.025	unknown	0.074348	unknown	300.019	unknown	300.022	unknown	300.101	unknown	300.106	unknown	300.114	unknown	300.03
chc lia lin 23/chc-LIA-Lin_080.smt2	unknown	300.02	unknown	300.115	unknown	300.115	unknown	300.037	unknown	300.115	unknown	300.024	unknown	300.062	unknown	300.093	unknown	300.021	unknown	300.025
chc lia lin 23/chc-LIA-Lin_081.smt2	unknown	300.015	unknown	300.095	unknown	300.013	unknown	2.00677	unknown	300.025	unknown	300.105	unknown	300.026	unknown	300.014	unknown	300.108	unknown	300.049
chc lia lin 23/chc-LIA-Lin_082.smt2	unknown	300.032	unknown	300.09	unknown	300.025	unknown	0.69103	unknown	300.025	unknown	300.116	unknown	300.064	unknown	300.104	unknown	300.021	unknown	300.089
chc lia lin 23/chc-LIA-Lin_083.smt2	unknown	300.106	unknown	300.109	unknown	300.015	unknown	0.17416	unknown	300.11	unknown	300.116	sat	0.0689641	unknown	300.109	unknown	300.118	unknown	300.066
chc lia lin 23/chc-LIA-Lin_084.smt2	unknown	300.014	unknown	300.099	unknown	300.023	unknown	0.182287	unknown	300.024	unknown	300.015	unknown	300.026	unknown	300.118	sat	5.85672	unknown	300.113
chc lia lin 23/chc-LIA-Lin_085.smt2	unknown	300.104	unknown	300.098	unknown	300.015	unknown	1.09652	unknown	300.026	unknown	300.045	unknown	300.034	unknown	300.075	unknown	300.045	unknown	300.032
chc lia lin 23/chc-LIA-Lin_086.smt2	sat	0.826994	unknown	300.022	unknown	300.116	unknown	0.739412	unknown	300.025	unknown	300.026	unknown	300.022	unknown	300.126	unknown	300.022	sat	5.3814
chc lia lin 23/chc-LIA-Lin_087.smt2	unknown	300.114	unknown	300.018	unknown	300.111	unknown	1.11425	unknown	300.028	sat	11.6312	unknown	300.025	unknown	300.018	sat	4.48433	unknown	300.042
chc lia lin 23/chc-LIA-Lin_088.smt2	unknown	300.014	unknown	300.113	unknown	300.022	unknown	300.03	unknown	300.02	unknown	300.026	unknown	300.016	unsat	4.94012	unknown	300.033	unknown	300.051
chc lia lin 23/chc-LIA-Lin_089.smt2	unknown	300.015	unknown	300.013	unknown	300.021	unknown	0.130885	unknown	300.015	unknown	300.026	unknown	300.106	unknown	300.02	unknown	283.182	unknown	300.116
chc lia lin 23/chc-LIA-Lin_090.smt2	unknown	300.103	unknown	300.016	unknown	300.102	unknown	0.139004	unknown	300.015	unknown	300.059	unknown	300.064	unknown	300.027	unknown	300.033	unknown	300.022
chc lia lin 23/chc-LIA-Lin_091.smt2	unknown	300.089	unknown	300.081	unknown	300.024	unknown	300.063	unknown	300.025	sat	93.2127	sat	10.7016	unknown	300.029	sat	157.155	unknown	300.034
chc lia lin 23/chc-LIA-Lin_092.smt2	unknown	300.067	unknown	300.026	unknown	300.021	unknown	0.130125	unknown	300.02	sat	0.0467051	sat	0.01815	unknown	300.016	sat	2.90157	unknown	300.062
chc lia lin 23/chc-LIA-Lin_093.smt2	unsat	0.0713979	unsat	0.0723081	unsat	0.0395779	unsat	0.130405	unsat	0.0334029	unsat	0.0777229	unsat	0.0201491	unsat	0.013864	unsat	2.56292	unsat	1.89846
chc lia lin 23/chc-LIA-Lin_094.smt2	unknown	300.024	unknown	300.025	unknown	300.016	unknown	300.019	unknown	300.105	sat	0.190405	sat	0.112009	unknown	300.114	sat	4.73266	unknown	300.025
chc lia lin 23/chc-LIA-Lin_095.smt2	unsat	0.50545	unsat	0.503995	unsat	0.503916	unsat	1.08074	unsat	0.126405	unsat	0.17573	unsat	0.152983	unsat	0.179855	unsat	12.8771	unsat	4.54255
chc lia lin 23/chc-LIA-Lin_096.smt2	unknown	300.107	unknown	300.024	unknown	300.064	unknown	300.015	unknown	300.027	sat	1.57576	unknown	300.037	unknown	300.04	unknown	300.033	sat	17.7829
chc lia lin 23/chc-LIA-Lin_097.smt2	unsat	7.58913	unsat	7.5729	unsat	7.1329	unsat	5.61794	unsat	1.89559	unsat	3.25987	unsat	4.40279	unsat	11.2194	unsat	9.84486	unsat	7.09191
chc lia lin 23/chc-LIA-Lin_098.smt2	unsat	8.23707	unsat	8.21542	unsat	7.92798	unsat	1.43499	unsat	1.82405	unsat	3.8676	unsat	2.97612	unsat	11.8595	unsat	10.6049	unsat	7.06973
chc lia lin 23/chc-LIA-Lin_099.smt2	unsat	16.6495	unsat	16.6459	unsat	14.6455	unsat	8.14357	unsat	8.14682	unsat	29.2169	unsat	9.73683	unsat	22.2936	unsat	15.0781	unsat	12.544
chc lia lin 23/chc-LIA-Lin_100.smt2	unsat	5.98695	unsat	6.0082	unsat	6.29099	unsat	5.87539	unsat	1.12294	unsat	1.34069	unsat	1.22368	unsat	11.4026	unsat	23.0751	unsat	6.86536
chc lia lin 23/chc-LIA-Lin_101.smt2	unsat	1.5424	unsat	1.54647	unsat	0.823257	unsat	0.065556	unsat	0.806935	unsat	0.786187	unknown	300.016	unsat	0.838883	unsat	21.1606	unsat	3.47119
chc lia lin 23/chc-LIA-Lin_102.smt2	unsat	2.40217	unsat	2.405	unsat	2.44292	unsat	42.0461	unsat	0.325124	unsat	0.316129	unsat	0.664454	unsat	2.1329	unsat	14.581	unsat	4.78704
chc lia lin 23/chc-LIA-Lin_103.smt2	unknown	300.033	unknown	300.037	unknown	300.016	unknown	300.024	unknown	300.105	sat	10.6262	unknown	300.113	unknown	300.07	unknown	159.076	unknown	300.027
chc lia lin 23/chc-LIA-Lin_104.smt2	unknown	300.028	unknown	300.015	unknown	300.016	unknown	300.015	unknown	300.025	sat	7.99791	unknown	300.014	unknown	300.025	unknown	166.304	unknown	300.026
chc lia lin 23/chc-LIA-Lin_105.smt2	sat	1.14771	sat	1.14488	sat	0.593558	unknown	0.237084	unknown	300.019	sat	5.30451	unknown	300.026	unknown	300.066	sat	8.31002	sat	3.2649
chc lia lin 23/chc-LIA-Lin_106.smt2	sat	0.0459371	unknown	300.015	unknown	300.099	unknown	0.05532	unknown	300.026	unknown	300.061	unknown	300.09	unknown	300.024	unknown	300.039	unknown	300.059
chc lia lin 23/chc-LIA-Lin_107.smt2	sat	6.46546	sat	6.45477	sat	1.82374	unknown	0.074755	unknown	300.015	sat	5.64139	unknown	300.036	unknown	300.076	sat	42.0268	sat	3.53527
chc lia lin 23/chc-LIA-Lin_108.smt2	sat	0.0446951	unknown	300.014	unknown	300.086	unknown	0.0559069	unknown	300.035	unknown	300.072	unknown	300.026	unknown	300.031	unknown	300.05	unknown	300.05
chc lia lin 23/chc-LIA-Lin_109.smt2	sat	0.049258	unknown	300.118	unknown	300.105	unknown	0.0586061	unknown	300.024	sat	0.0463529	unknown	300.014	unknown	300.022	sat	2.6741	unknown	300.022
chc lia lin 23/chc-LIA-Lin_110.smt2	unknown	300.109	unknown	300.02	unknown	300.033	unknown	300.11	unknown	300.064	unknown	300.052	sat	49.0196	unknown	300.027	unknown	300.044	unknown	300.038
chc lia lin 23/chc-LIA-Lin_111.smt2	unsat	0.04453	unsat	0.043028	unsat	0.587726	unsat	0.053163	unknown	300.114	unsat	102.862	unsat	0.665063	unsat	76.3249	unsat	2.71258	unsat	8.69811
chc lia lin 23/chc-LIA-Lin_112.smt2	unknown	300.058	unknown	300.109	unknown	300.04	unknown	0.0739059	unknown	300.029	unknown	300.106	sat	0.013672	unknown	300.108	unknown	300.101	unknown	300.069
chc lia lin 23/chc-LIA-Lin_113.smt2	unknown	300.106	unknown	300.023	unknown	300.025	unknown	300.038	unknown	300.026	unknown	300.105	unknown	300.082	unknown	300.015	unknown	300.101	unknown	300.032
chc lia lin 23/chc-LIA-Lin_114.smt2	unknown	300.015	unknown	300.029	unknown	300.115	unknown	300.023	unknown	300.105	unknown	300.025	unknown	300.018	unknown	300.105	unknown	300.043	sat	61.9855
chc lia lin 23/chc-LIA-Lin_115.smt2	unknown	300.025	unknown	300.023	unknown	300.054	unknown	300.025	unknown	300.016	unknown	300.015	unknown	300.019	unknown	300.018	unknown	300.026	sat	35.8633
chc lia lin 23/chc-LIA-Lin_116.smt2	unknown	300.105	unknown	300.069	unknown	300.015	unknown	300.02	unknown	300.019	unknown	300.105	unknown	300.025	unknown	300.094	unknown	300.039	unknown	300.054
chc lia lin 23/chc-LIA-Lin_117.smt2	unknown	300.024	unknown	300.105	unknown	300.034	unknown	300.111	unknown	300.015	unknown	300.016	unknown	300.03	unknown	300.017	unknown	300.043	unknown	300.032
chc lia lin 23/chc-LIA-Lin_118.smt2	unknown	300.015	unknown	300.105	unknown	300.105	unknown	300.031	unknown	300.015	unknown	300.026	unknown	300.083	unknown	300.022	unknown	300.065	unknown	300.044
chc lia lin 23/chc-LIA-Lin_119.smt2	unknown	300.025	unknown	300.028	unknown	300.024	unknown	300.024	unknown	300.096	unknown	300.015	unknown	300.035	unknown	300.112	unknown	300.069	unknown	300.022
chc lia lin 23/chc-LIA-Lin_120.smt2	unknown	300.033	unknown	300.095	unknown	300.014	unknown	300.041	unknown	300.115	unknown	300.016	unknown	300.096	unknown	300.032	unknown	300.029	unknown	300.072
chc lia lin 23/chc-LIA-Lin_121.smt2	unknown	300.024	unknown	300.016	unknown	300.105	unknown	300.024	unknown	300.082	unknown	300.114	unknown	300.021	unknown	300.017	unknown	300.047	unsat	63.3439
chc lia lin 23/chc-LIA-Lin_122.smt2	unknown	300.024	unknown	300.047	unknown	300.015	unknown	300.022	unknown	300.1	unknown	300.02	unknown	300.018	unknown	300.018	unknown	300.03	unknown	300.095
chc lia lin 23/chc-LIA-Lin_123.smt2	unknown	300.112	unknown	300.017	unknown	300.071	unknown	300.015	unknown	300.025	unknown	300.114	unknown	300.104	unknown	300.016	unknown	300.03	unknown	300.033
chc lia lin 23/chc-LIA-Lin_124.smt2	unknown	300.113	unknown	300.025	unknown	300.107	unknown	300.073	unknown	300.026	unknown	300.026	unknown	300.014	unknown	300.026	unknown	300.028	unknown	300.081
chc lia lin 23/chc-LIA-Lin_125.smt2	unknown	300.115	unknown	300.055	unknown	300.026	unknown	300.019	unknown	300.015	unknown	300.029	unknown	300.077	unknown	300.087	unknown	300.024	sat	34.1569
chc lia lin 23/chc-LIA-Lin_126.smt2	unknown	300.114	unknown	300.014	unknown	300.04	unknown	300.022	unknown	300.015	unknown	300.075	unknown	300.031	unknown	300.016	unknown	300.109	unknown	300.102
chc lia lin 23/chc-LIA-Lin_127.smt2	unknown	300.027	unknown	300.041	unknown	300.024	unknown	300.026	unknown	300.08	unknown	300.015	unknown	300.038	unknown	300.103	unknown	300.103	unknown	300.043
chc lia lin 23/chc-LIA-Lin_128.smt2	unknown	300.015	unknown	300.038	unknown	300.025	unknown	300.024	unknown	300.026	unknown	300.015	unknown	300.019	unknown	300.024	unknown	300.036	sat	62.2627
chc lia lin 23/chc-LIA-Lin_129.smt2	unknown	300.015	unknown	300.018	unknown	300.117	unknown	300.073	unknown	300.021	unknown	300.015	unknown	300.024	unknown	300.026	unknown	300.022	unknown	300.061
chc lia lin 23/chc-LIA-Lin_130.smt2	unknown	300.019	unknown	300.073	unknown	300.015	unknown	300.02	unknown	300.025	unknown	300.035	unknown	300.064	unknown	300.032	unknown	300.031	unknown	300.02
chc lia lin 23/chc-LIA-Lin_131.smt2	unknown	300.014	unknown	300.019	unknown	300.026	unknown	300.097	unknown	300.09	unknown	300.104	unknown	300.028	unknown	300.016	unknown	300.063	sat	35.4177
chc lia lin 23/chc-LIA-Lin_132.smt2	unknown	300.026	unknown	300.014	unknown	300.094	unknown	300.015	unknown	300.016	unknown	300.026	unknown	300.106	unknown	300.015	unknown	300.031	unknown	300.03
chc lia lin 23/chc-LIA-Lin_133.smt2	unknown	300.024	unknown	300.015	unknown	300.106	unknown	300.113	unknown	300.064	unknown	300.12	unknown	300.02	unknown	300.026	unknown	300.093	sat	62.637
chc lia lin 23/chc-LIA-Lin_134.smt2	unknown	300.015	unknown	300.054	unknown	300.024	unknown	300.056	unknown	300.036	unknown	300.035	unknown	300.026	unknown	300.033	unknown	300.107	unknown	300.023
chc lia lin 23/chc-LIA-Lin_135.smt2	unknown	300.118	unknown	300.015	unknown	300.109	unknown	300.015	unknown	300.026	unknown	300.016	unknown	300.081	unknown	300.025	unknown	300.026	sat	63.1554
chc lia lin 23/chc-LIA-Lin_136.smt2	unknown	300.115	unknown	300.114	unknown	300.015	unknown	300.017	unknown	300.015	unknown	300.015	unknown	300.021	unknown	300.016	unknown	300.022	sat	62.4133
chc lia lin 23/chc-LIA-Lin_137.smt2	unknown	300.021	unknown	300.022	unknown	300.023	unknown	300.035	unknown	300.029	unknown	300.105	unknown	300.038	unknown	300.115	unknown	300.068	unknown	300.034
chc lia lin 23/chc-LIA-Lin_138.smt2	unknown	300.015	unknown	300.054	unknown	300.022	unknown	300.026	unknown	300.115	unknown	300.026	unknown	300.065	unknown	300.016	unknown	300.042	unknown	300.08
chc lia lin 23/chc-LIA-Lin_139.smt2	unknown	300.042	unknown	300.027	unknown	300.022	unknown	300.024	unknown	300.115	unknown	300.117	unknown	300.035	unknown	300.105	unknown	300.039	unknown	300.032
chc lia lin 23/chc-LIA-Lin_140.smt2	unknown	300.024	unknown	300.056	unknown	300.065	unknown	300.097	unknown	300.016	unknown	300.027	unknown	300.025	unknown	300.017	unknown	300.024	unknown	300.062
chc lia lin 23/chc-LIA-Lin_141.smt2	unknown	300.015	unknown	300.015	unknown	300.105	unknown	300.026	unknown	300.111	unknown	300.015	unknown	300.03	unknown	300.027	unknown	300.075	unknown	300.022
chc lia lin 23/chc-LIA-Lin_142.smt2	unknown	300.015	unknown	300.015	unknown	300.025	unknown	300.026	unknown	300.087	unknown	300.026	unknown	300.036	unknown	300.117	sat	34.0764	sat	52.7298
chc lia lin 23/chc-LIA-Lin_143.smt2	unknown	300.074	unknown	300.024	unknown	300.096	unknown	300.03	unknown	300.105	unknown	300.055	unknown	300.065	unknown	300.025	unknown	300.071	unknown	300.031
chc lia lin 23/chc-LIA-Lin_144.smt2	sat	179.664	sat	181.015	sat	188.248	unknown	300.017	unknown	300.015	sat	54.9289	unknown	300.017	unknown	300.028	sat	20.4564	sat	40.4518
chc lia lin 23/chc-LIA-Lin_145.smt2	unknown	300.026	unknown	300.015	unknown	300.016	unknown	300.022	unknown	300.016	unknown	300.024	unknown	300.05	unknown	300.018	unknown	300.105	unknown	300.025
chc lia lin 23/chc-LIA-Lin_146.smt2	unknown	300.026	unknown	300.015	unknown	300.083	unknown	300.106	unknown	300.105	unknown	300.026	unknown	300.055	unknown	300.017	unknown	300.029	sat	62.0009
chc lia lin 23/chc-LIA-Lin_147.smt2	unknown	300.024	unknown	300.105	unknown	300.035	unknown	300.114	unknown	300.016	unknown	300.025	unknown	300.091	unknown	300.016	unknown	300.045	sat	59.2086
chc lia lin 23/chc-LIA-Lin_148.smt2	unknown	300.066	unknown	300.105	unknown	300.016	unknown	300.114	unknown	300.015	unknown	300.016	unknown	300.077	unknown	300.027	unknown	300.038	sat	63.8482
chc lia lin 23/chc-LIA-Lin_149.smt2	unsat	0.046187	unsat	0.045333	unknown	300.106	unsat	0.055479	unknown	300.016	unknown	300.015	unknown	300.036	unknown	300.019	unknown	300.102	unknown	300.044
chc lia lin 23/chc-LIA-Lin_150.smt2	unknown	300.032	unknown	300.024	unknown	300.02	unknown	300.025	unknown	300.024	unknown	300.115	unknown	300.027	unknown	300.023	unknown	300.023	unknown	300.062
chc lia lin 23/chc-LIA-Lin_151.smt2	unknown	300.015	unknown	300.059	unknown	300.023	unknown	300.089	unknown	300.026	sat	0.163493	sat	172.879	unknown	300.016	unknown	300.022	unknown	300.024
chc lia lin 23/chc-LIA-Lin_152.smt2	unsat	0.237805	unsat	0.238059	unsat	0.218667	unknown	300.015	unsat	0.102759	unsat	0.075913	unsat	0.0538769	unsat	0.034945	unsat	232.625	unknown	300.123
chc lia lin 23/chc-LIA-Lin_153.smt2	unknown	300.027	unknown	300.065	unknown	300.016	unknown	300.022	unknown	300.072	sat	0.0574879	sat	0.0426109	unknown	300.015	unknown	300.07	unknown	300.03
chc lia lin 23/chc-LIA-Lin_154.smt2	unknown	300.026	unknown	300.027	unknown	300.084	unknown	300.015	unknown	300.023	sat	4.70422	sat	2.85709	unknown	300.026	unknown	300.031	unknown	300.024
chc lia lin 23/chc-LIA-Lin_155.smt2	unsat	156.305	unsat	176.548	unsat	10.1939	unknown	300.101	unsat	0.765598	unsat	23.3733	unsat	0.436693	unsat	1.6269	unknown	300.117	unknown	300.02
chc lia lin 23/chc-LIA-Lin_156.smt2	unknown	300.014	unknown	300.024	unknown	300.058	unknown	300.015	unknown	300.015	sat	0.347938	sat	1.13981	unknown	300.048	sat	4.8504	sat	3.86952
chc lia lin 23/chc-LIA-Lin_157.smt2	unknown	300.097	unknown	300.025	unknown	300.014	unknown	300.103	unknown	300.035	sat	0.040884	sat	0.0179581	unknown	300.027	sat	9.05152	unknown	300.024
chc lia lin 23/chc-LIA-Lin_158.smt2	unknown	300.047	unknown	300.015	unknown	300.015	unknown	300.025	unknown	300.101	sat	2.38982	unknown	300.116	unknown	300.098	unknown	300.026	unknown	300.021
chc lia lin 23/chc-LIA-Lin_159.smt2	unknown	300.025	unsat	96.6485	unsat	19.4997	unknown	300.039	unsat	1.28736	unsat	3.61493	unsat	0.479886	unsat	2.77527	unknown	300.027	unknown	300.028
chc lia lin 23/chc-LIA-Lin_160.smt2	unsat	0.164218	unsat	0.164748	unsat	0.153112	unknown	300.014	unsat	0.050545	unsat	0.063814	unsat	0.041529	unsat	0.028048	unsat	34.8845	unsat	60.8341
chc lia lin 23/chc-LIA-Lin_161.smt2	unsat	0.154313	unsat	0.15391	unsat	0.13866	unknown	300.032	unsat	0.0559051	unsat	0.158184	unsat	0.103809	unsat	0.03955	unsat	29.9994	unsat	14.0307
chc lia lin 23/chc-LIA-Lin_162.smt2	unsat	0.27074	unsat	0.271046	unsat	0.234845	unknown	300.023	unsat	0.116531	unsat	0.204223	unsat	0.103	unsat	0.053388	unknown	300.023	unsat	62.5253
chc lia lin 23/chc-LIA-Lin_163.smt2	unsat	0.065329	unsat	0.065322	unsat	0.062776	unsat	0.0949299	unsat	0.033664	unsat	0.0426981	unsat	0.0137711	unsat	0.012268	unsat	5.36374	unsat	5.5393
chc lia lin 23/chc-LIA-Lin_164.smt2	unknown	300.114	unknown	300.051	unknown	300.015	unknown	300.109	unknown	300.094	sat	0.076759	sat	32.0414	unknown	300.12	unknown	300.124	unknown	300.057
chc lia lin 23/chc-LIA-Lin_165.smt2	unknown	300.014	unknown	300.017	unknown	300.031	unknown	300.104	unknown	300.023	sat	0.0454001	sat	0.02146	unknown	300.018	sat	156.295	unknown	300.097
chc lia lin 23/chc-LIA-Lin_166.smt2	unknown	300.015	unknown	300.021	unknown	300.015	unknown	300.014	unknown	300.015	sat	0.0435199	sat	0.019993	unknown	300.083	unknown	300.04	unknown	300.03
chc lia lin 23/chc-LIA-Lin_167.smt2	unknown	300.071	unknown	300.024	unknown	300.016	unknown	300.015	unknown	300.064	sat	0.0852481	sat	0.162437	unknown	300.024	unknown	300.13	unknown	300.033
chc lia lin 23/chc-LIA-Lin_168.smt2	unknown	300.022	unknown	300.022	unknown	300.022	unknown	300.015	unknown	300.115	sat	0.116727	sat	0.142395	unknown	300.025	unknown	300.036	unknown	300.105
chc lia lin 23/chc-LIA-Lin_169.smt2	unknown	300.015	unknown	300.014	unknown	300.113	unknown	300.02	unknown	300.016	sat	6.75937	unknown	300.025	unknown	300.017	sat	40.0178	unknown	300.022
chc lia lin 23/chc-LIA-Lin_170.smt2	unknown	300.02	unknown	300.025	unknown	300.078	unknown	300.022	unknown	300.059	unknown	300.016	unknown	300.061	unknown	300.025	unknown	300.033	sat	23.8824
chc lia lin 23/chc-LIA-Lin_171.smt2	unknown	300.024	unknown	300.105	unknown	300.015	unknown	300.114	unknown	300.015	sat	3.98242	unknown	300.105	unknown	300.028	unknown	300.035	unknown	300.031
chc lia lin 23/chc-LIA-Lin_172.smt2	unknown	300.077	unknown	300.024	unknown	300.015	unknown	300.105	unknown	300.116	unknown	300.035	unknown	300.015	unknown	300.066	unknown	300.04	unknown	300.031
chc lia lin 23/chc-LIA-Lin_173.smt2	unknown	300.021	unknown	300.109	unknown	300.113	unknown	300.091	unknown	300.115	unknown	300.025	unknown	300.016	unknown	300.024	unknown	300.089	unknown	300.041
chc lia lin 23/chc-LIA-Lin_174.smt2	unknown	300.031	unknown	300.034	unknown	300.016	unknown	300.023	unknown	300.022	unknown	300.036	unknown	300.016	unknown	300.018	unknown	300.025	unknown	300.04
chc lia lin 23/chc-LIA-Lin_175.smt2	unknown	300.022	unknown	300.102	unknown	300.022	unknown	300.024	unknown	300.113	sat	1.27984	unknown	300.043	unknown	300.027	unknown	300.041	sat	299.018
chc lia lin 23/chc-LIA-Lin_176.smt2	unknown	300.105	unknown	300.013	unknown	300.113	unknown	300.04	unknown	300.114	unknown	300.024	unknown	300.024	unknown	300.105	unknown	300.03	unknown	300.024
chc lia lin 23/chc-LIA-Lin_177.smt2	unknown	300.019	unknown	300.015	unknown	300.024	unknown	300.014	unknown	300.021	sat	3.0946	unknown	300.021	unknown	300.025	unknown	300.118	unknown	300.043
chc lia lin 23/chc-LIA-Lin_178.smt2	unknown	300.023	unknown	300.014	unknown	300.101	unknown	300.103	unknown	300.081	unknown	300.015	unknown	300.015	unknown	300.016	unknown	300.029	unknown	300.04
chc lia lin 23/chc-LIA-Lin_179.smt2	unknown	300.013	unknown	300.014	unknown	300.013	unknown	300.024	unknown	300.024	unknown	300.106	unknown	300.025	unknown	300.015	unknown	300.031	unknown	300.043
chc lia lin 23/chc-LIA-Lin_180.smt2	unknown	300.014	unknown	300.023	unknown	300.047	unknown	300.112	unknown	300.024	unknown	300.015	unknown	300.116	unknown	300.027	unknown	300.041	unknown	300.022
chc lia lin 23/chc-LIA-Lin_181.smt2	unknown	300.014	unknown	300.104	unknown	300.013	unknown	300.114	unknown	300.109	sat	58.193	unknown	300.094	unknown	300.113	unknown	300.028	unknown	300.115
chc lia lin 23/chc-LIA-Lin_182.smt2	unknown	300.103	unknown	300.015	unknown	300.016	unknown	300.015	unknown	300.029	unknown	300.025	unknown	300.025	unknown	300.012	unknown	300.03	unknown	300.027
chc lia lin 23/chc-LIA-Lin_183.smt2	unknown	300.114	unknown	300.033	unknown	300.015	unknown	300.013	unknown	300.024	unknown	300.024	unknown	300.015	unknown	300.115	unknown	300.1	unknown	300.021
chc lia lin 23/chc-LIA-Lin_184.smt2	unknown	300.024	unknown	300.025	unknown	300.027	unknown	300.015	unknown	300.024	sat	2.79566	unknown	300.073	unknown	300.048	unknown	300.032	unknown	300.036
chc lia lin 23/chc-LIA-Lin_185.smt2	unknown	300.015	unknown	300.114	unknown	300.024	unknown	300.013	unknown	300.089	unknown	300.016	unknown	300.016	unknown	300.017	unknown	300.041	unknown	300.021
chc lia lin 23/chc-LIA-Lin_186.smt2	unknown	300.015	unknown	300.094	unknown	300.105	unknown	300.103	unknown	300.016	sat	5.3497	unknown	300.025	unknown	300.103	unknown	300.033	unknown	300.028
chc lia lin 23/chc-LIA-Lin_187.smt2	unknown	300.083	unknown	300.022	unknown	300.018	unknown	300.025	unknown	300.015	unsat	193.483	unsat	20.0597	unknown	300.017	unknown	300.021	unknown	300.021
chc lia lin 23/chc-LIA-Lin_188.smt2	unknown	300.045	unknown	300.014	unknown	300.018	unknown	300.101	unknown	300.023	unknown	300.025	unknown	300.027	unknown	300.025	unknown	300.034	unknown	300.021
chc lia lin 23/chc-LIA-Lin_189.smt2	unknown	300.106	unknown	300.026	unknown	300.091	unknown	300.018	unknown	300.024	sat	269.342	unknown	300.025	unknown	300.114	sat	10.0996	unknown	300.126
chc lia lin 23/chc-LIA-Lin_190.smt2	unknown	300.014	unknown	300.024	unknown	300.062	unknown	300.113	unknown	300.014	unknown	300.108	unknown	300.025	unknown	300.016	sat	5.43095	unknown	300.027
chc lia lin 23/chc-LIA-Lin_191.smt2	unknown	300.022	unknown	300.022	unknown	300.012	unknown	300.019	unknown	300.111	unknown	300.026	unknown	300.015	unknown	300.016	sat	7.73401	unknown	300.058
chc lia lin 23/chc-LIA-Lin_192.smt2	unknown	300.015	unknown	300.052	unknown	300.016	unknown	300.022	unknown	300.025	unknown	300.015	unknown	300.112	unknown	300.035	sat	13.5081	unknown	300.126
chc lia lin 23/chc-LIA-Lin_193.smt2	unknown	300.021	unknown	300.111	unknown	300.111	unknown	300.013	unknown	300.015	unknown	300.057	unknown	300.069	unknown	300.012	unknown	300.026	unknown	300.022
chc lia lin 23/chc-LIA-Lin_194.smt2	unknown	300.037	unknown	300.014	unknown	300.024	unknown	300.113	unknown	300.116	unknown	300.105	unknown	300.026	unknown	300.026	sat	13.699	unknown	300.038
chc lia lin 23/chc-LIA-Lin_195.smt2	unknown	300.047	unknown	300.03	unknown	300.012	unknown	300.116	unknown	300.025	unknown	300.024	unknown	300.018	unknown	300.107	unknown	300.03	sat	6.49402
chc lia lin 23/chc-LIA-Lin_196.smt2	unknown	300.033	unknown	300.096	unknown	300.057	unknown	300.013	unknown	300.106	unknown	300.069	unknown	300.104	unknown	300.017	unknown	300.102	unknown	300.056
chc lia lin 23/chc-LIA-Lin_197.smt2	unknown	300.015	unknown	300.031	unknown	300.028	unknown	300.017	unknown	300.096	unknown	300.025	unknown	300.068	unknown	300.022	unknown	300.038	unknown	300.089
chc lia lin 23/chc-LIA-Lin_198.smt2	unknown	300.071	unknown	300.017	unknown	300.062	unknown	300.013	unknown	300.112	unknown	300.08	unknown	300.105	unknown	300.022	unknown	300.113	unknown	300.115
chc lia lin 23/chc-LIA-Lin_199.smt2	unknown	300.013	unknown	300.014	unknown	300.016	unknown	300.023	unknown	300.018	sat	144.742	unknown	300.107	unknown	300.119	unknown	300.031	unknown	300.035
chc lia lin 23/chc-LIA-Lin_200.smt2	unknown	300.017	unknown	300.116	unknown	300.015	unknown	300.065	unknown	300.025	sat	221.61	unknown	300.116	unknown	300.031	sat	179.927	unknown	300.021
chc lia lin 23/chc-LIA-Lin_201.smt2	unknown	300.039	unknown	300.018	unknown	300.104	unknown	300.023	unknown	300.016	unknown	300.016	unknown	300.114	unknown	300.013	unknown	300.025	unknown	300.03
chc lia lin 23/chc-LIA-Lin_202.smt2	unknown	300.065	unknown	300.024	unknown	300.016	unknown	300.016	unknown	300.083	unknown	300.015	unknown	300.114	unknown	300.115	unknown	300.027	unknown	300.083
chc lia lin 23/chc-LIA-Lin_203.smt2	unknown	300.042	unknown	300.024	unknown	300.014	unknown	300.012	unknown	300.021	unknown	300.015	unknown	300.019	unknown	300.067	unknown	300.03	unknown	300.038
chc lia lin 23/chc-LIA-Lin_204.smt2	unknown	300.019	unknown	300.022	unknown	300.015	unknown	300.019	unknown	300.12	sat	26.5122	unknown	300.015	unknown	300.016	sat	16.9502	unknown	300.036
chc lia lin 23/chc-LIA-Lin_205.smt2	unknown	300.026	unknown	300.053	unknown	300.034	unknown	300.078	unknown	300.015	unknown	300.034	unknown	300.022	unknown	300.02	sat	163.166	sat	24.1973
chc lia lin 23/chc-LIA-Lin_206.smt2	unknown	300.012	unknown	300.018	unknown	300.044	unknown	300.024	unknown	300.114	unknown	300.057	unknown	300.024	unknown	300.024	unknown	300.026	unknown	300.02
chc lia lin 23/chc-LIA-Lin_207.smt2	unknown	300.071	unknown	300.113	unknown	300.013	unknown	300.014	unknown	300.017	sat	75.8652	unknown	300.115	unknown	300.108	unknown	300.024	sat	209.418
chc lia lin 23/chc-LIA-Lin_208.smt2	unknown	300.026	unknown	300.028	unknown	300.012	unknown	300.024	unknown	300.02	unknown	300.017	unknown	300.105	unknown	300.074	unknown	300.101	unknown	300.04
chc lia lin 23/chc-LIA-Lin_209.smt2	unknown	300.014	unknown	300.014	unknown	300.034	unknown	300.013	unknown	300.068	sat	164.413	unknown	300.028	unknown	300.03	sat	234.645	sat	52.2019
chc lia lin 23/chc-LIA-Lin_210.smt2	unknown	300.024	unknown	300.018	unknown	300.034	unknown	300.025	unknown	300.119	unknown	300.015	unknown	300.017	unknown	300.029	unknown	300.037	unknown	300.025
chc lia lin 23/chc-LIA-Lin_211.smt2	unknown	300.013	unknown	300.062	unknown	300.016	unknown	300.013	unknown	300.019	unknown	300.115	unknown	300.015	unknown	300.038	unknown	300.022	sat	143.585
chc lia lin 23/chc-LIA-Lin_212.smt2	unknown	300.024	unknown	300.02	unknown	300.106	unknown	300.016	unknown	300.115	sat	21.4872	unknown	300.115	unknown	300.103	unknown	300.065	unknown	300.041
chc lia lin 23/chc-LIA-Lin_213.smt2	unknown	300.104	unknown	300.105	unknown	300.113	unknown	300.029	unknown	300.017	sat	116.015	unknown	300.015	unknown	300.103	unknown	300.054	unknown	300.025
chc lia lin 23/chc-LIA-Lin_214.smt2	unknown	300.024	unknown	300.094	unknown	300.093	unknown	300.051	unknown	300.014	unknown	300.081	unknown	300.016	unknown	300.094	unknown	300.126	unknown	300.034
chc lia lin 23/chc-LIA-Lin_215.smt2	unknown	300.104	unknown	300.027	unknown	300.013	unknown	300.012	unknown	300.018	unknown	300.015	unknown	300.107	unknown	300.019	unknown	300.029	unknown	300.046
chc lia lin 23/chc-LIA-Lin_216.smt2	unknown	300.105	unknown	300.073	unknown	300.096	unknown	300.017	unknown	300.023	unknown	300.025	unknown	300.016	unknown	300.117	unknown	300.081	unknown	300.12
chc lia lin 23/chc-LIA-Lin_217.smt2	unknown	300.062	unknown	300.114	unknown	300.04	unknown	300.013	unknown	300.115	unknown	300.015	unknown	300.016	unknown	300.115	unknown	300.108	unknown	300.039
chc lia lin 23/chc-LIA-Lin_218.smt2	unknown	300.022	unknown	300.014	unknown	300.018	unknown	300.022	unknown	300.018	unknown	300.015	unknown	300.018	unknown	300.061	unknown	300.112	unknown	300.028
chc lia lin 23/chc-LIA-Lin_219.smt2	unknown	300.02	unknown	300.024	unknown	300.022	unknown	300.017	unknown	300.031	sat	16.5382	unknown	300.023	unknown	300.016	sat	22.0382	unknown	300.04
chc lia lin 23/chc-LIA-Lin_220.smt2	unknown	300.013	unknown	300.025	unknown	300.114	unknown	300.02	unknown	300.014	unknown	300.025	unknown	300.019	unknown	300.026	unknown	300.026	unknown	300.035
chc lia lin 23/chc-LIA-Lin_221.smt2	unknown	300.104	unknown	300.013	unknown	300.012	unknown	300.014	unknown	300.017	unknown	300.057	unknown	300.025	unknown	300.113	unknown	300.036	unknown	300.115
chc lia lin 23/chc-LIA-Lin_222.smt2	unknown	300.114	unknown	300.016	unknown	300.114	unknown	300.023	unknown	300.097	sat	80.2282	unknown	300.025	unknown	300.026	sat	44.0103	unknown	300.031
chc lia lin 23/chc-LIA-Lin_223.smt2	unknown	300.014	unknown	300.013	unknown	300.104	unknown	300.014	unknown	300.115	unknown	300.017	unknown	300.115	unknown	300.013	unknown	300.023	unknown	300.116
chc lia lin 23/chc-LIA-Lin_224.smt2	unknown	300.034	unknown	300.015	unknown	300.08	unknown	300.015	unknown	300.017	sat	288.677	unknown	300.022	unknown	300.116	unknown	300.112	unknown	300.023
chc lia lin 23/chc-LIA-Lin_225.smt2	unknown	300.093	unknown	300.116	unknown	300.074	unknown	300.022	unknown	300.022	unknown	300.015	unknown	300.026	unknown	300.024	unknown	300.1	unknown	300.033
chc lia lin 23/chc-LIA-Lin_226.smt2	unknown	300.113	unknown	300.027	unknown	300.014	unknown	300.021	unknown	300.102	sat	17.555	unknown	300.025	unknown	300.069	sat	9.39713	unknown	300.041
chc lia lin 23/chc-LIA-Lin_227.smt2	unknown	300.103	unknown	300.015	unknown	300.074	unknown	300.014	unknown	300.015	unknown	300.025	unknown	300.017	unknown	300.026	unknown	300.041	unknown	300.033
chc lia lin 23/chc-LIA-Lin_228.smt2	unknown	300.069	unknown	300.012	unknown	300.012	unknown	183.575	unknown	300.068	unknown	300.108	unknown	300.114	unknown	300.054	unknown	300.031	unknown	300.08
chc lia lin 23/chc-LIA-Lin_229.smt2	unknown	300.077	unknown	300.035	unknown	300.07	unknown	300.022	unknown	300.036	unknown	300.106	unknown	300.068	unknown	300.095	unknown	300.021	unknown	300.044
chc lia lin 23/chc-LIA-Lin_230.smt2	unknown	300.084	unknown	300.021	unknown	300.022	unknown	300.015	unknown	300.105	unknown	300.035	unknown	300.026	unknown	300.113	unknown	300.029	unknown	300.022
chc lia lin 23/chc-LIA-Lin_231.smt2	unknown	300.013	unknown	300.114	unknown	300.076	unknown	300.1	unknown	300.105	unknown	300.033	unknown	300.018	unknown	300.036	unknown	300.115	unknown	300.063
chc lia lin 23/chc-LIA-Lin_232.smt2	unknown	300.015	unknown	300.013	unknown	300.016	unknown	300.077	unknown	300.025	sat	15.1671	unknown	300.016	unknown	300.06	sat	9.04266	unknown	300.121
chc lia lin 23/chc-LIA-Lin_233.smt2	unknown	300.024	unknown	300.023	unknown	300.014	unknown	300.013	unknown	300.023	unknown	300.016	unknown	300.105	unknown	300.117	unknown	300.116	unknown	300.034
chc lia lin 23/chc-LIA-Lin_234.smt2	unknown	300.024	unknown	300.025	unknown	300.013	unknown	300.037	unknown	300.015	unknown	300.035	unknown	300.064	unknown	300.016	unknown	300.042	sat	76.5919
chc lia lin 23/chc-LIA-Lin_235.smt2	unknown	300.068	unknown	300.014	unknown	300.015	unknown	300.019	unknown	300.113	sat	116.266	unknown	300.016	unknown	300.027	unknown	300.062	unknown	300.022
chc lia lin 23/chc-LIA-Lin_236.smt2	unknown	300.084	unknown	300.096	unknown	300.025	unknown	300.019	unknown	300.032	unknown	300.105	unknown	300.016	unknown	300.103	unknown	300.11	unknown	300.022
chc lia lin 23/chc-LIA-Lin_237.smt2	unknown	300.024	unknown	300.025	unknown	300.105	unknown	300.043	unknown	300.015	unknown	300.021	unknown	300.115	unknown	300.043	unknown	300.112	unknown	300.022
chc lia lin 23/chc-LIA-Lin_238.smt2	unknown	300.077	unknown	300.015	unknown	300.077	unknown	300.025	unknown	300.095	sat	39.3216	unknown	300.018	unknown	300.017	sat	16.7829	unknown	300.091
chc lia lin 23/chc-LIA-Lin_239.smt2	unknown	300.04	unknown	300.023	unknown	300.013	unknown	300.013	unknown	300.103	unknown	300.106	unknown	300.016	unknown	300.016	unknown	300.029	unknown	300.118
chc lia lin 23/chc-LIA-Lin_240.smt2	unknown	300.015	unknown	300.09	unknown	300.024	unknown	300.014	unknown	300.03	sat	15.7864	unknown	300.016	unknown	300.016	unknown	300.117	unknown	300.104
chc lia lin 23/chc-LIA-Lin_241.smt2	unknown	300.013	unknown	300.022	unknown	300.034	unknown	0.0806201	unknown	300.098	unknown	129.904	sat	0.0587389	unknown	300.026	unknown	300.029	sat	1.89678
chc lia lin 23/chc-LIA-Lin_242.smt2	unknown	300.051	unknown	300.092	unknown	300.109	unknown	0.0776791	unknown	300.024	unknown	300.014	sat	255.275	unknown	300.054	sat	26.6645	unknown	300.032
chc lia lin 23/chc-LIA-Lin_243.smt2	unknown	300.016	unknown	300.04	unknown	300.027	unknown	300.025	unknown	300.013	unknown	300.016	unknown	300.016	unknown	300.07	sat	4.04067	unknown	300.089
chc lia lin 23/chc-LIA-Lin_244.smt2	unknown	300.014	unknown	300.019	unknown	300.023	unknown	0.215363	unknown	300.016	sat	0.0566009	sat	0.0472599	unknown	300.023	sat	2.78143	unknown	300.036
chc lia lin 23/chc-LIA-Lin_245.smt2	unknown	300.047	unknown	300.026	unknown	300.023	unknown	300.024	unknown	300.114	sat	5.36539	sat	0.228375	unknown	300.026	unknown	300.123	unknown	300.022
chc lia lin 23/chc-LIA-Lin_246.smt2	unknown	300.016	unknown	300.113	unknown	300.015	unknown	0.0691931	unknown	300.026	unknown	300.081	unknown	300.06	unknown	300.026	sat	3.35092	unknown	300.049
chc lia lin 23/chc-LIA-Lin_247.smt2	sat	0.0724049	unknown	300.021	unknown	300.015	unknown	0.069811	unknown	300.025	unknown	300.048	unknown	300.041	unknown	300.017	sat	3.11506	unknown	300.036
chc lia lin 23/chc-LIA-Lin_248.smt2	sat	0.113289	unknown	300.039	unknown	300.015	unknown	0.278724	unknown	300.081	unknown	300.072	unknown	300.021	unknown	300.09	unknown	300.029	unknown	300.061
chc lia lin 23/chc-LIA-Lin_249.smt2	unknown	300.022	unknown	300.026	unknown	300.026	unknown	0.089054	unknown	300.027	sat	13.6126	unknown	300.015	unknown	300.025	unknown	300.02	sat	4.32557
chc lia lin 23/chc-LIA-Lin_250.smt2	unknown	300.018	unknown	300.103	unknown	300.042	unknown	0.114079	unknown	300.017	unknown	300.015	unknown	300.092	unknown	300.023	sat	2.81272	unknown	300.096
chc lia lin 23/chc-LIA-Lin_251.smt2	sat	0.060551	unknown	300.018	unknown	300.085	unknown	0.0697719	unknown	300.063	sat	280.122	unknown	300.024	unknown	300.053	sat	3.11197	unknown	300.022
chc lia lin 23/chc-LIA-Lin_252.smt2	unknown	300.05	unknown	300.095	unknown	300.105	unknown	0.129917	unknown	300.025	unknown	300.015	unknown	300.031	unknown	300.097	sat	3.18965	unknown	300.04
chc lia lin 23/chc-LIA-Lin_253.smt2	unknown	300.035	unknown	300.017	unknown	300.015	unknown	300.024	unknown	300.018	unknown	300.024	unknown	300.016	unknown	300.104	sat	108.952	sat	6.13019
chc lia lin 23/chc-LIA-Lin_254.smt2	unknown	300.027	unknown	300.094	unknown	300.02	unknown	0.122542	unknown	300.028	unknown	300.114	unknown	300.015	unknown	300.015	unknown	300.03	unknown	300.032
chc lia lin 23/chc-LIA-Lin_255.smt2	unknown	300.017	unknown	300.021	unknown	300.018	unknown	300.037	unknown	300.036	unknown	300.105	sat	0.455836	unknown	300.029	unknown	300.024	unknown	300.032
chc lia lin 23/chc-LIA-Lin_256.smt2	unknown	300.022	unknown	300.033	unknown	300.047	unknown	2.70692	unknown	300.024	unknown	300.024	sat	37.3343	unknown	300.029	sat	21.7968	unknown	300.032
chc lia lin 23/chc-LIA-Lin_257.smt2	sat	0.162685	unknown	300.107	unknown	300.025	unknown	0.204801	unknown	300.037	unknown	300.094	unknown	300.021	unknown	300.123	unknown	300.029	unknown	300.078
chc lia lin 23/chc-LIA-Lin_258.smt2	unknown	300.013	unknown	300.023	unknown	300.023	unknown	0.104546	unknown	300.017	unknown	300.06	unknown	300.066	unknown	300.028	unknown	300.122	unknown	300.053
chc lia lin 23/chc-LIA-Lin_259.smt2	unknown	300.056	unknown	300.103	unknown	300.024	unknown	300.019	unknown	300.015	unknown	300.038	unknown	300.035	unknown	300.015	unknown	300.033	unknown	300.041
chc lia lin 23/chc-LIA-Lin_260.smt2	unknown	300.1	unknown	300.026	unknown	300.024	unknown	51.3621	unknown	300.019	unknown	300.098	sat	140.575	unknown	300.024	unknown	300.043	unknown	300.034
chc lia lin 23/chc-LIA-Lin_261.smt2	sat	0.0581261	unknown	300.066	unknown	300.021	unknown	0.0669489	unknown	300.043	unknown	300.025	unknown	300.116	unknown	300.073	sat	2.86098	unknown	300.052
chc lia lin 23/chc-LIA-Lin_262.smt2	unknown	300.113	unknown	300.113	unknown	300.014	unknown	0.326738	unknown	300.026	unknown	21.7082	unknown	300.05	unknown	300.018	unknown	300.021	unknown	300.031
chc lia lin 23/chc-LIA-Lin_263.smt2	sat	0.066658	unknown	300.014	unknown	300.066	unknown	0.083419	unknown	300.115	unknown	300.016	unknown	300.048	unknown	300.021	unknown	300.027	unknown	300.025
chc lia lin 23/chc-LIA-Lin_264.smt2	unknown	300.017	unknown	300.027	unknown	300.015	unknown	0.0631671	unknown	300.02	unknown	300.019	unknown	300.105	unknown	300.035	unknown	300.099	unknown	300.022
chc lia lin 23/chc-LIA-Lin_265.smt2	sat	0.0543399	unknown	300.012	unknown	300.106	unknown	0.0652589	unknown	300.023	unknown	300.024	sat	24.1228	unknown	300.032	sat	2.76402	unknown	300.034
chc lia lin 23/chc-LIA-Lin_266.smt2	sat	0.07325	unknown	300.083	unknown	300.02	unknown	0.0817751	unknown	300.024	unknown	300.094	unknown	300.111	unknown	300.095	unknown	300.115	unknown	300.05
chc lia lin 23/chc-LIA-Lin_267.smt2	unknown	300.048	unknown	300.024	unknown	300.018	unknown	300.019	unknown	300.025	unknown	300.015	unknown	300.027	unknown	300.074	unknown	300.032	unknown	300.112
chc lia lin 23/chc-LIA-Lin_268.smt2	unknown	300.095	unknown	300.013	unknown	300.026	unknown	0.105148	unknown	300.015	unknown	300.016	unknown	300.026	unknown	300.072	unknown	300.037	unknown	300.033
chc lia lin 23/chc-LIA-Lin_269.smt2	sat	0.062065	unknown	300.071	unknown	300.048	unknown	300.113	unknown	300.017	unknown	300.057	unknown	300.071	unknown	300.021	unknown	300.093	unknown	300.059
chc lia lin 23/chc-LIA-Lin_270.smt2	unknown	300.014	unknown	300.018	unknown	300.026	unknown	44.9378	unknown	300.097	unknown	300.015	unknown	300.024	unknown	300.107	unknown	300.035	unknown	300.033
chc lia lin 23/chc-LIA-Lin_271.smt2	sat	0.057806	unknown	300.014	unknown	300.115	unknown	0.0699671	unknown	300.101	sat	0.09412	sat	0.645378	unknown	300.104	sat	3.2065	unknown	300.022
chc lia lin 23/chc-LIA-Lin_272.smt2	unknown	300.024	unknown	300.023	unknown	300.012	unknown	0.207007	unknown	300.016	sat	7.68547	unknown	300.105	unknown	300.115	unknown	300.111	unknown	300.038
chc lia lin 23/chc-LIA-Lin_273.smt2	sat	0.0418189	sat	0.042152	sat	0.0414621	unknown	0.085043	unknown	300.026	sat	0.0569	sat	0.0216729	unknown	300.117	sat	2.525	sat	1.74261
chc lia lin 23/chc-LIA-Lin_274.smt2	sat	0.102665	unknown	300.065	unknown	300.015	unknown	0.0886939	unknown	300.026	sat	0.0785311	sat	0.0344081	unknown	300.013	sat	3.87067	unknown	300.035
chc lia lin 23/chc-LIA-Lin_275.smt2	sat	0.0540831	unknown	300.074	unknown	300.015	unknown	0.0607029	unknown	300.035	sat	0.0537621	sat	0.0178111	unknown	300.043	sat	3.21889	unknown	300.081
chc lia lin 23/chc-LIA-Lin_276.smt2	sat	0.0813389	unknown	300.016	unknown	300.024	unknown	0.0841841	unknown	300.062	sat	0.135036	sat	3.726	unknown	300.115	sat	3.73251	unknown	300.021
chc lia lin 23/chc-LIA-Lin_277.smt2	unknown	300.015	unknown	300.091	unknown	300.022	unknown	0.173014	unknown	300.029	sat	2.35272	unknown	300.024	unknown	300.035	unknown	300.023	unknown	300.095
chc lia lin 23/chc-LIA-Lin_278.smt2	unknown	300.015	unknown	300.024	unknown	300.104	unknown	0.314168	unknown	300.025	unknown	300.017	unknown	300.021	unknown	300.015	unknown	300.025	unknown	300.032
chc lia lin 23/chc-LIA-Lin_279.smt2	unknown	300.014	unknown	300.034	unknown	300.021	unknown	0.349352	unknown	300.024	unknown	300.106	unknown	300.03	unknown	300.104	unknown	300.035	unknown	300.08
chc lia lin 23/chc-LIA-Lin_280.smt2	unknown	300.028	unknown	300.105	unknown	300.014	unknown	0.328138	unknown	300.105	unknown	300.09	unknown	300.016	unknown	300.014	unknown	300.032	unknown	300.035
chc lia lin 23/chc-LIA-Lin_281.smt2	unknown	300.015	unknown	300.074	unknown	300.014	unknown	0.174779	unknown	300.035	sat	0.86997	unknown	300.099	unknown	300.016	unknown	300.029	unknown	300.031
chc lia lin 23/chc-LIA-Lin_282.smt2	sat	0.0361919	sat	0.0349611	sat	0.0353139	unknown	0.035645	sat	0.0250581	sat	0.038369	sat	0.012529	sat	0.0122051	sat	1.48971	sat	1.43092
chc lia lin 23/chc-LIA-Lin_283.smt2	sat	0.035703	sat	0.0356239	sat	0.0352779	unknown	0.036004	sat	0.0237739	sat	0.025071	sat	0.010188	sat	0.0130501	sat	1.48191	sat	1.4618
chc lia lin 23/chc-LIA-Lin_284.smt2	sat	0.0426389	sat	0.043133	sat	0.043237	unknown	0.0439281	sat	0.0241601	sat	0.0270029	sat	0.0143221	sat	0.0113191	sat	1.53339	sat	1.44751
chc lia lin 23/chc-LIA-Lin_285.smt2	sat	0.0509169	sat	0.0713199	sat	0.050585	unknown	0.067179	unknown	300.116	sat	0.038806	sat	0.011757	unknown	300.02	sat	2.50493	sat	1.82255
chc lia lin 23/chc-LIA-Lin_286.smt2	unknown	300.015	unknown	300.113	unknown	300.018	unknown	0.537995	unknown	300.114	sat	0.160072	sat	0.0769279	unknown	300.013	unknown	300.029	unknown	300.031
chc lia lin 23/chc-LIA-Lin_287.smt2	sat	0.0495091	unknown	300.075	unknown	300.042	unknown	0.0641631	unknown	300.025	sat	0.037629	sat	0.021163	unknown	300.025	sat	2.28398	unknown	300.034
chc lia lin 23/chc-LIA-Lin_288.smt2	sat	0.076273	sat	0.076215	sat	0.075737	unknown	0.076359	sat	0.0269691	sat	0.0299799	sat	0.0135251	sat	0.0135821	sat	1.68535	sat	1.6349
chc lia lin 23/chc-LIA-Lin_289.smt2	unsat	0.0696111	unsat	0.0706811	unsat	0.070717	unsat	0.0860489	unsat	0.02844	unsat	0.03268	unsat	0.0127019	unsat	0.017369	unsat	1.90891	unsat	1.79176
chc lia lin 23/chc-LIA-Lin_290.smt2	sat	0.0781291	sat	0.0798071	sat	0.078926	unknown	0.088702	unknown	300.047	sat	0.0365601	sat	0.0165349	sat	0.0163421	sat	1.79371	sat	1.8112
chc lia lin 23/chc-LIA-Lin_291.smt2	sat	0.188562	sat	0.188603	sat	0.193019	unknown	0.187535	sat	0.0289641	sat	0.034571	sat	0.0351411	sat	0.0421381	sat	2.14837	sat	1.86399
chc lia lin 23/chc-LIA-Lin_292.smt2	unsat	0.107504	unsat	0.108302	unsat	0.10839	unsat	0.12261	unsat	0.0310651	unsat	0.0348461	unsat	0.033942	unsat	0.0343629	unsat	2.08073	unsat	2.01349
chc lia lin 23/chc-LIA-Lin_293.smt2	sat	0.0791041	sat	0.0796179	sat	0.125349	unknown	0.088571	unknown	300.108	sat	0.0355959	sat	0.0250799	sat	0.0129651	sat	1.80204	sat	1.77021
chc lia lin 23/chc-LIA-Lin_294.smt2	unsat	2.4051	unsat	2.43329	unsat	1.72137	unknown	300.015	unsat	0.583869	unsat	0.496787	unsat	1.41195	unsat	1.18801	unknown	300.03	unknown	300.042
chc lia lin 23/chc-LIA-Lin_295.smt2	unsat	5.07929	unsat	5.09138	unsat	2.06223	unknown	300.015	unsat	1.65893	unsat	1.47361	unsat	6.83677	unsat	1.54511	unknown	300.03	unknown	300.103
chc lia lin 23/chc-LIA-Lin_296.smt2	unknown	300.015	unknown	300.024	unknown	300.025	unknown	300.026	unknown	300.041	sat	0.400586	sat	0.443002	unknown	300.118	unknown	300.112	unknown	300.031
chc lia lin 23/chc-LIA-Lin_297.smt2	unknown	300.014	unknown	300.021	unknown	300.016	unknown	300.024	sat	0.515244	sat	0.544804	sat	28.7426	unknown	300.019	sat	118.452	sat	116.947
chc lia lin 23/chc-LIA-Lin_298.smt2	unsat	5.31086	unsat	5.31714	unsat	4.85944	unsat	2.15513	unsat	0.284105	unsat	0.269675	unsat	2.79993	unsat	0.821032	unknown	300.068	unknown	300.109
chc lia lin 23/chc-LIA-Lin_299.smt2	unknown	300.024	unknown	300.024	unknown	300.02	unknown	300.024	sat	0.0523971	sat	0.055586	sat	0.06602	unknown	300.017	sat	10.214	sat	9.66237
chc lia lin 23/chc-LIA-Lin_300.smt2	unsat	0.244126	unsat	0.239648	unsat	0.215107	unsat	0.278788	unsat	0.0611421	unsat	0.0906011	unsat	0.104454	unsat	0.0395751	unsat	7.31476	unsat	6.86293
chc lia lin 23/chc-LIA-Lin_301.smt2	unknown	300.015	unknown	300.015	unknown	300.105	unknown	300.104	sat	0.0440599	sat	0.049714	sat	0.0438999	unknown	300.015	sat	8.3145	sat	8.23327
chc lia lin 23/chc-LIA-Lin_302.smt2	unknown	300.024	unknown	300.068	unknown	300.024	unknown	300.018	unknown	300.077	sat	3.28469	unknown	300.102	unknown	300.082	unknown	300.038	unknown	300.033
chc lia lin 23/chc-LIA-Lin_303.smt2	unknown	300.024	unknown	300.024	unknown	300.016	unknown	300.024	sat	0.0380719	sat	0.0394569	sat	0.0318961	unknown	300.022	sat	4.20676	sat	4.75046
chc lia lin 23/chc-LIA-Lin_304.smt2	unknown	300.014	unknown	300.105	unknown	300.025	unknown	300.022	unknown	300.023	sat	0.223049	sat	0.199719	unknown	300.016	unknown	300.029	unknown	300.06
chc lia lin 23/chc-LIA-Lin_305.smt2	unsat	1.94616	unsat	1.95443	unsat	1.97942	unsat	1.26305	unsat	0.128376	unsat	0.130896	unsat	1.25567	unsat	0.293652	unknown	300.086	unknown	300.021
chc lia lin 23/chc-LIA-Lin_306.smt2	unknown	300.103	unknown	300.089	unknown	300.015	unknown	300.022	unknown	300.027	sat	159.197	unknown	300.125	unknown	300.025	sat	3.17961	unknown	300.085
chc lia lin 23/chc-LIA-Lin_307.smt2	unknown	300.025	unknown	300.105	unknown	300.121	unknown	300.064	unknown	300.074	sat	0.647256	sat	214.078	unknown	300.02	unknown	300.122	unknown	300.037
chc lia lin 23/chc-LIA-Lin_308.smt2	unsat	1.0994	unsat	1.10224	unsat	0.854256	unsat	0.608109	unsat	0.0872059	unsat	0.0931821	unsat	0.493532	unsat	0.155998	unknown	300.036	unknown	300.122
chc lia lin 23/chc-LIA-Lin_309.smt2	unknown	300.017	unknown	300.015	unknown	300.068	unknown	300.027	unknown	300.029	sat	1.09531	sat	0.898649	unknown	300.108	unknown	300.036	unknown	300.108
chc lia lin 23/chc-LIA-Lin_310.smt2	unknown	300.081	unknown	300.023	unknown	300.017	unknown	300.03	sat	0.170914	sat	0.174933	sat	0.221128	unknown	300.107	sat	30.068	sat	31.5091
chc lia lin 23/chc-LIA-Lin_311.smt2	unknown	300.108	unknown	300.024	unknown	300.093	unknown	300.015	sat	0.0528189	sat	0.055919	sat	0.049896	unknown	300.03	sat	8.04347	sat	7.24962
chc lia lin 23/chc-LIA-Lin_312.smt2	unsat	21.6052	unsat	21.7741	unsat	17.6533	unknown	300.024	unsat	7.00437	unknown	300.016	unknown	300.058	unsat	19.1762	unknown	300.12	unknown	300.095
chc lia lin 23/chc-LIA-Lin_313.smt2	sat	0.164748	unknown	300.033	unknown	300.105	unknown	0.104658	unknown	300.023	sat	0.106735	unknown	300.032	unknown	300.035	sat	3.54409	unknown	300.023
chc lia lin 23/chc-LIA-Lin_314.smt2	sat	0.170532	unknown	300.101	unknown	300.025	unknown	0.141241	unknown	300.105	unknown	300.025	unknown	300.015	unknown	300.103	sat	3.89703	unknown	300.05
chc lia lin 23/chc-LIA-Lin_315.smt2	unsat	118.762	unsat	119.116	unsat	82.7441	unknown	300.096	unsat	12.0795	unknown	294.877	unknown	300.098	unsat	30.3963	unknown	300.038	unknown	300.078
chc lia lin 23/chc-LIA-Lin_316.smt2	unknown	300.015	unknown	300.098	unknown	300.105	unknown	300.015	unknown	300.016	sat	4.3161	unknown	300.015	unknown	300.015	unknown	300.045	unknown	300.025
chc lia lin 23/chc-LIA-Lin_317.smt2	unsat	41.11	unsat	40.7482	unsat	31.5394	unknown	300.025	unsat	6.53134	unsat	100.326	unknown	300.06	unsat	22.1674	unknown	300.032	unknown	300.023
chc lia lin 23/chc-LIA-Lin_318.smt2	unsat	208.456	unsat	208.202	unsat	234.312	unknown	300.035	unsat	9.11947	unsat	65.9016	unsat	234.355	unsat	52.8005	unknown	300.031	unknown	300.058
chc lia lin 23/chc-LIA-Lin_319.smt2	unsat	292.554	unsat	292.592	unknown	300.029	unsat	35.1091	unsat	10.2858	unsat	6.02293	unsat	96.278	unsat	4.66573	unknown	300.047	unknown	300.045
chc lia lin 23/chc-LIA-Lin_320.smt2	unknown	300.024	unknown	300.025	unknown	300.016	unknown	300.036	unknown	300.076	sat	3.35551	unknown	300.016	unknown	300.032	unknown	300.031	unknown	300.054
chc lia lin 23/chc-LIA-Lin_321.smt2	unknown	300.038	unknown	300.074	unknown	300.018	unknown	300.11	unknown	300.016	sat	19.2218	unknown	300.106	unknown	300.027	unknown	300.032	unknown	300.029
chc lia lin 23/chc-LIA-Lin_322.smt2	unsat	10.6762	unsat	10.7235	unsat	8.26567	unsat	12.5945	unsat	2.07216	unsat	10.2077	unsat	47.2092	unsat	5.37539	unknown	300.105	unknown	300.133
chc lia lin 23/chc-LIA-Lin_323.smt2	unknown	300.048	unknown	300.024	unknown	300.111	unknown	300.027	unknown	300.015	sat	13.4792	unknown	300.068	unknown	300.116	unknown	300.025	unknown	300.113
chc lia lin 23/chc-LIA-Lin_324.smt2	unsat	86.0603	unsat	86.0135	unsat	59.6641	unknown	300.024	unsat	7.47017	unsat	5.0818	unsat	100.696	unsat	31.2603	unknown	300.074	unknown	300.044
chc lia lin 23/chc-LIA-Lin_325.smt2	unknown	300.015	unknown	300.024	unknown	300.023	unknown	300.029	unknown	300.065	sat	3.76683	unknown	300.106	unknown	300.117	unknown	300.021	unknown	300.022
chc lia lin 23/chc-LIA-Lin_326.smt2	unknown	300.014	unknown	300.02	unknown	300.023	unknown	10.6331	unknown	300.017	sat	0.0427769	unknown	300.101	unknown	300.114	sat	2.55528	unknown	300.033
chc lia lin 23/chc-LIA-Lin_327.smt2	unknown	300.024	unknown	300.032	unknown	300.016	unknown	300.019	unknown	300.016	sat	4.68375	unknown	300.016	unknown	300.029	unknown	300.072	unknown	300.031
chc lia lin 23/chc-LIA-Lin_328.smt2	unsat	6.47261	unsat	6.41954	unsat	3.93346	unknown	300.115	unsat	2.40466	unsat	1.73221	unsat	2.81668	unsat	2.16965	unknown	300.021	unknown	300.037
chc lia lin 23/chc-LIA-Lin_329.smt2	unsat	17.3469	unsat	17.4122	unsat	14.9475	unknown	300.019	unsat	7.40895	unknown	300.06	unknown	300.025	unsat	15.4196	unknown	300.024	unknown	300.04
chc lia lin 23/chc-LIA-Lin_330.smt2	unknown	300.034	unknown	300.039	unknown	300.116	unknown	300.019	unknown	300.115	sat	16.003	unknown	300.026	unknown	300.088	unknown	300.105	unknown	300.112
chc lia lin 23/chc-LIA-Lin_331.smt2	unknown	300.025	unknown	300.024	unknown	300.015	unknown	300.023	unknown	300.036	sat	28.4175	unknown	300.068	unknown	300.021	unknown	300.091	unknown	300.031
chc lia lin 23/chc-LIA-Lin_332.smt2	unsat	74.1061	unsat	73.3798	unsat	59.7889	unsat	101.452	unsat	27.5344	unknown	300.094	unsat	48.8224	unsat	52.8288	unknown	300.035	unknown	300.06
chc lia lin 23/chc-LIA-Lin_333.smt2	unknown	300.025	unknown	300.024	unknown	300.016	unknown	300.019	unknown	300.032	sat	30.1467	unknown	300.102	unknown	300.03	unknown	300.032	unknown	300.122
chc lia lin 23/chc-LIA-Lin_334.smt2	unknown	300.062	unknown	300.018	unknown	300.024	unknown	300.065	unknown	300.03	sat	15.0051	unknown	300.032	unknown	300.107	unknown	300.022	unknown	300.043
chc lia lin 23/chc-LIA-Lin_335.smt2	unknown	300.03	unknown	300.099	unknown	300.024	unknown	300.11	unknown	300.027	sat	13.5815	unknown	300.025	unknown	300.105	unknown	300.022	unknown	300.025
chc lia lin 23/chc-LIA-Lin_336.smt2	unknown	300.025	unknown	300.015	unknown	300.015	unknown	300.019	unknown	300.015	sat	13.6954	unknown	300.025	unknown	300.087	unknown	300.122	unknown	300.062
chc lia lin 23/chc-LIA-Lin_337.smt2	unsat	71.5721	unsat	71.6721	unsat	44.114	unsat	133.478	unsat	29.3672	unknown	300.05	unsat	46.3284	unsat	53.2397	unknown	300.038	unknown	300.057
chc lia lin 23/chc-LIA-Lin_338.smt2	unknown	300.024	unknown	300.016	unknown	300.12	unknown	300.028	unknown	300.026	sat	47.373	unknown	300.099	unknown	300.028	unknown	300.106	unknown	300.031
chc lia lin 23/chc-LIA-Lin_339.smt2	unknown	300.014	unknown	300.121	unknown	300.025	unknown	300.105	unknown	300.025	sat	15.2447	unknown	300.034	unknown	300.029	unknown	300.054	unknown	300.028
chc lia lin 23/chc-LIA-Lin_340.smt2	unsat	0.092613	unsat	0.0954349	unknown	300.093	unsat	0.095369	unknown	300.05	unknown	300.044	unsat	2.71095	unknown	300.115	unsat	3.13078	unsat	12.7744
chc lia lin 23/chc-LIA-Lin_341.smt2	unknown	300.028	unknown	300.022	unknown	300.024	unknown	300.035	unknown	300.024	sat	23.4389	sat	7.49694	unknown	300.017	unknown	300.036	unknown	300.106
chc lia lin 23/chc-LIA-Lin_342.smt2	unknown	300.033	unknown	300.115	unknown	300.046	unknown	300.12	unknown	300.015	sat	14.5765	unknown	300.027	unknown	300.028	unknown	300.072	unknown	300.125
chc lia lin 23/chc-LIA-Lin_343.smt2	unknown	300.017	unknown	300.022	unknown	300.031	unknown	300.06	unknown	300.041	sat	24.8824	sat	7.29025	unknown	300.116	unknown	300.034	unknown	300.029
chc lia lin 23/chc-LIA-Lin_344.smt2	unknown	300.044	unknown	300.059	unknown	300.025	unknown	300.112	unknown	300.048	sat	119.719	unknown	300.102	unknown	300.018	unknown	300.025	unknown	300.048
chc lia lin 23/chc-LIA-Lin_345.smt2	unknown	300.019	unknown	300.085	unknown	300.098	unknown	300.11	unknown	300.02	sat	41.6403	unknown	300.099	unknown	300.108	unknown	300.03	unknown	300.021
chc lia lin 23/chc-LIA-Lin_346.smt2	unsat	145.518	unsat	147.831	unsat	106.307	unknown	300.021	unsat	34.425	unknown	300.021	unknown	300.116	unsat	88.3961	unknown	300.055	unknown	300.067
chc lia lin 23/chc-LIA-Lin_347.smt2	unknown	300.048	unknown	300.034	unknown	300.029	unknown	300.024	unknown	300.015	sat	23.2137	sat	7.37052	unknown	300.033	unknown	300.034	unknown	300.114
chc lia lin 23/chc-LIA-Lin_348.smt2	unsat	0.143945	unsat	0.160912	unknown	300.032	unsat	0.0895789	unknown	300.083	unknown	300.113	unknown	300.082	unknown	300.016	unsat	3.43307	unknown	300.121
chc lia lin 23/chc-LIA-Lin_349.smt2	unknown	300.014	unknown	300.015	unknown	300.015	unknown	300.019	unknown	300.019	unknown	300.074	unknown	300.026	unknown	300.015	unknown	300.025	unknown	300.07
chc lia lin 23/chc-LIA-Lin_350.smt2	unknown	300.075	unknown	300.015	unknown	300.025	unknown	300.014	unknown	300.053	sat	6.308	unknown	300.025	unknown	300.076	unknown	300.028	unknown	300.073
chc lia lin 23/chc-LIA-Lin_351.smt2	unknown	300.115	unknown	300.032	unknown	300.105	unknown	300.021	unknown	300.087	unknown	300.096	unknown	300.106	unknown	300.016	unknown	300.097	unknown	300.022
chc lia lin 23/chc-LIA-Lin_352.smt2	unsat	0.078625	unsat	0.0800051	unknown	300.015	unsat	0.0777371	unknown	300.021	unknown	300.077	unsat	253.828	unknown	300.109	unsat	2.89384	unknown	300.021
chc lia lin 23/chc-LIA-Lin_353.smt2	unknown	300.025	unknown	300.015	unknown	300.025	unknown	300.02	unknown	300.076	unknown	300.018	unknown	300.035	unknown	300.031	unknown	300.032	unknown	300.093
chc lia lin 23/chc-LIA-Lin_354.smt2	unknown	300.015	unknown	300.067	unknown	300.015	unknown	300.022	unknown	300.015	unknown	300.034	unknown	300.025	unknown	300.048	unknown	300.101	unknown	300.039
chc lia lin 23/chc-LIA-Lin_355.smt2	unknown	300.024	unknown	300.115	unknown	300.025	unknown	300.023	unknown	300.026	unknown	300.015	unknown	300.024	unknown	300.095	unknown	300.023	unknown	300.025
chc lia lin 23/chc-LIA-Lin_356.smt2	unknown	300.026	unknown	300.077	unknown	300.1	unknown	300.031	unknown	300.073	unknown	300.084	unknown	300.018	unknown	300.061	unknown	300.037	unknown	300.023
chc lia lin 23/chc-LIA-Lin_357.smt2	unknown	300.034	unknown	300.106	unknown	300.024	unknown	300.062	unknown	300.035	sat	63.6783	unknown	300.016	unknown	300.105	unknown	300.025	unknown	300.118
chc lia lin 23/chc-LIA-Lin_358.smt2	unknown	300.014	unknown	300.02	unknown	300.015	unknown	300.023	unknown	300.018	unknown	300.026	unknown	300.056	unknown	300.018	unknown	300.024	unknown	300.021
chc lia lin 23/chc-LIA-Lin_359.smt2	unknown	300.017	unknown	300.074	unknown	300.015	unknown	300.02	unknown	300.018	unknown	300.016	unknown	300.024	unknown	300.029	unknown	300.03	unknown	300.035
chc lia lin 23/chc-LIA-Lin_360.smt2	unsat	0.181549	unsat	0.684393	unknown	300.014	unsat	0.109422	unknown	300.114	unknown	300.036	unknown	300.031	unknown	300.106	unsat	3.32886	unknown	300.1
chc lia lin 23/chc-LIA-Lin_361.smt2	unknown	300.021	unknown	300.025	unknown	300.024	unknown	300.108	unknown	300.081	unknown	300.032	unknown	300.014	unknown	300.014	unknown	300.058	unknown	300.074
chc lia lin 23/chc-LIA-Lin_362.smt2	unknown	300.065	unknown	300.018	unknown	300.017	unknown	300.106	unknown	300.025	sat	31.7986	unknown	300.022	unknown	300.019	unknown	300.111	unknown	300.099
chc lia lin 23/chc-LIA-Lin_363.smt2	unknown	300.014	unknown	300.074	unknown	300.023	unknown	300.029	unknown	300.026	sat	20.5424	unknown	300.024	unknown	300.016	unknown	300.033	unknown	300.046
chc lia lin 23/chc-LIA-Lin_364.smt2	unknown	300.043	unknown	300.08	unknown	300.016	unknown	300.024	unknown	300.038	unknown	300.025	unknown	300.095	unknown	300.106	unknown	300.119	unknown	300.02
chc lia lin 23/chc-LIA-Lin_365.smt2	unknown	300.015	unknown	300.049	unknown	300.025	unknown	300.087	unknown	300.023	unknown	300.015	unknown	300.015	unsat	206.951	unknown	300.045	unknown	300.111
chc lia lin 23/chc-LIA-Lin_366.smt2	unknown	300.014	unknown	300.022	unknown	300.025	unknown	300.125	unsat	26.8154	unsat	19.7613	unknown	300.017	unsat	124.284	unknown	300.041	unknown	300.033
chc lia lin 23/chc-LIA-Lin_367.smt2	unknown	300.022	unknown	300.025	unknown	300.053	unknown	300.014	unknown	300.077	unknown	300.023	unknown	300.103	unknown	300.068	unknown	300.034	unknown	300.05
chc lia lin 23/chc-LIA-Lin_368.smt2	unknown	300.03	unknown	300.028	unknown	300.043	unknown	300.023	unknown	300.042	unknown	300.016	unknown	300.021	unknown	300.035	unknown	300.033	unknown	300.11
chc lia lin 23/chc-LIA-Lin_369.smt2	unknown	300.015	unknown	300.115	unknown	300.015	unknown	300.014	unknown	300.106	unknown	300.016	unknown	300.073	unknown	300.067	unknown	300.022	unknown	300.113
chc lia lin 23/chc-LIA-Lin_370.smt2	unsat	0.092511	unsat	0.090004	unknown	300.022	unsat	0.127583	unknown	300.015	unknown	300.016	unknown	300.016	unknown	300.015	unsat	3.08202	unknown	300.041
chc lia lin 23/chc-LIA-Lin_371.smt2	unknown	300.108	unknown	300.024	unknown	300.027	unknown	300.019	unknown	300.016	unsat	100.38	unknown	300.033	unknown	300.032	unknown	300.028	unknown	300.033
chc lia lin 23/chc-LIA-Lin_372.smt2	unknown	300.05	unknown	300.032	unknown	300.018	unknown	300.024	unknown	300.106	sat	100.609	unknown	300.016	unknown	300.016	unknown	300.037	unknown	300.119
chc lia lin 23/chc-LIA-Lin_373.smt2	unknown	300.015	unknown	300.034	unknown	300.108	unknown	300.015	unknown	300.058	unknown	300.126	unknown	300.021	unknown	300.104	unknown	300.114	unknown	300.053
chc lia lin 23/chc-LIA-Lin_374.smt2	unknown	300.097	unknown	300.037	unknown	300.082	unknown	300.027	unknown	300.016	sat	133.085	unknown	300.113	unknown	300.08	unknown	300.031	unknown	300.12
chc lia lin 23/chc-LIA-Lin_375.smt2	unsat	0.349553	unsat	0.681077	unknown	300.029	unsat	0.191066	unknown	300.026	unknown	300.027	unknown	300.031	unknown	300.097	unsat	4.20912	unknown	300.041
chc lia lin 23/chc-LIA-Lin_376.smt2	unknown	300.017	unknown	300.02	unknown	300.041	unknown	300.021	unknown	300.029	unknown	300.094	unknown	300.02	unknown	300.027	unknown	300.103	unknown	300.099
chc lia lin 23/chc-LIA-Lin_377.smt2	sat	126.974	sat	126.588	sat	104.56	unknown	300.015	unknown	300.015	unknown	300.116	unknown	300.024	unknown	300.041	unknown	300.027	unknown	300.022
chc lia lin 23/chc-LIA-Lin_378.smt2	unknown	300.015	unknown	300.014	unknown	300.024	unsat	167.648	unsat	183.66	unknown	300.031	unknown	300.072	unknown	300.096	unknown	300.102	unknown	300.103
chc lia lin 23/chc-LIA-Lin_379.smt2	unknown	300.014	unknown	300.039	unknown	300.086	unknown	300.028	unsat	87.6181	unknown	300.038	unknown	300.053	unsat	24.4528	unknown	300.128	unknown	300.022
chc lia lin 23/chc-LIA-Lin_380.smt2	unknown	300.083	unknown	300.015	unknown	300.024	unknown	300.021	unsat	51.3085	unknown	300.016	unknown	300.026	unknown	300.073	unknown	300.025	unknown	300.078
chc lia lin 23/chc-LIA-Lin_381.smt2	unknown	300.014	unknown	300.055	unknown	300.015	unknown	300.026	unknown	300.016	unknown	300.022	unknown	300.063	unknown	300.09	unknown	300.12	unknown	300.022
chc lia lin 23/chc-LIA-Lin_382.smt2	unknown	300.113	unknown	300.023	unknown	300.016	unknown	300.025	unknown	300.059	unknown	300.026	unknown	300.013	unknown	300.025	unknown	300.039	unknown	300.037
chc lia lin 23/chc-LIA-Lin_383.smt2	unknown	300.035	unknown	300.024	unknown	300.06	unknown	300.051	unsat	128.206	unsat	256.143	unknown	300.026	unknown	300.058	unknown	300.034	unknown	300.029
chc lia lin 23/chc-LIA-Lin_384.smt2	sat	0.130689	sat	0.130588	sat	0.130876	unknown	0.126353	sat	0.0292741	sat	0.0417409	sat	0.028888	sat	0.0286111	sat	1.95914	sat	1.83965
chc lia lin 23/chc-LIA-Lin_385.smt2	sat	2.88318	sat	2.88493	sat	2.87038	unknown	2.86618	sat	0.082009	sat	0.167309	sat	1.25481	sat	1.27017	sat	7.54084	sat	6.09595
chc lia lin 23/chc-LIA-Lin_386.smt2	sat	0.0476629	sat	0.048388	sat	0.0489979	unknown	0.050075	sat	0.025282	sat	0.0294529	sat	0.0131659	sat	0.020178	sat	1.5765	sat	1.54295
chc lia lin 23/chc-LIA-Lin_387.smt2	sat	1.56569	sat	1.57244	sat	1.48167	unknown	2.41752	unknown	300.026	sat	0.180729	sat	0.235715	unknown	300.023	sat	3.69394	sat	3.99955
chc lia lin 23/chc-LIA-Lin_388.smt2	sat	0.609113	sat	0.602609	sat	0.594823	unknown	0.370994	unknown	300.105	sat	0.109734	sat	0.143714	unknown	300.067	sat	2.76851	sat	2.86494
chc lia lin 23/chc-LIA-Lin_389.smt2	sat	0.221578	sat	0.220719	sat	0.222569	unknown	0.210981	unknown	300.025	sat	0.0537909	sat	0.130833	sat	0.0789051	sat	2.59883	sat	2.55902
chc lia lin 23/chc-LIA-Lin_390.smt2	sat	0.229585	sat	0.228803	sat	0.230366	unknown	0.219845	sat	0.034309	sat	0.083705	sat	0.043678	sat	0.043736	sat	2.12082	sat	2.04384
chc lia lin 23/chc-LIA-Lin_391.smt2	sat	0.045513	sat	0.045707	sat	0.04477	unknown	0.0462799	sat	0.0247831	sat	0.027495	sat	0.0108009	sat	0.011587	sat	1.58959	sat	1.51923
chc lia lin 23/chc-LIA-Lin_392.smt2	sat	0.404809	sat	0.408614	sat	0.403534	unknown	0.348726	unknown	300.017	sat	0.101439	sat	0.131767	unknown	300.029	sat	3.34313	sat	3.16908
chc lia lin 23/chc-LIA-Lin_393.smt2	sat	0.0462061	sat	0.047166	sat	0.0469629	unknown	0.062573	sat	0.025293	sat	0.027724	sat	0.015766	sat	0.0150889	sat	1.56965	sat	1.52473
chc lia lin 23/chc-LIA-Lin_394.smt2	sat	0.084306	sat	0.136298	sat	0.085081	unknown	0.0823131	unknown	300.025	sat	0.0404751	sat	0.0271969	sat	0.027134	sat	2.04862	sat	2.0142
chc lia lin 23/chc-LIA-Lin_395.smt2	sat	0.423951	sat	0.364979	sat	0.361926	unknown	0.307713	unknown	300.115	sat	0.085493	sat	0.116689	unknown	300.042	sat	3.0917	sat	3.11107
chc lia lin 23/chc-LIA-Lin_396.smt2	sat	0.167075	sat	0.167807	sat	0.169014	unknown	0.16491	sat	0.033579	sat	0.04355	sat	0.110886	sat	0.0680091	sat	2.30859	sat	2.27089
chc lia lin 23/chc-LIA-Lin_397.smt2	sat	0.0668411	sat	0.066787	sat	0.0682879	unknown	0.0788139	sat	0.0436779	sat	0.032423	sat	0.0175009	sat	0.017072	sat	1.73824	sat	1.69896
chc lia lin 23/chc-LIA-Lin_398.smt2	sat	0.0381379	sat	0.0375219	sat	0.0381391	unknown	0.0384591	sat	0.0242361	sat	0.0267161	sat	0.012382	sat	0.028014	sat	1.50696	sat	1.47832
chc lia lin 23/chc-LIA-Lin_399.smt2	sat	0.0495939	sat	0.049348	sat	0.049291	unknown	0.051698	unknown	300.015	sat	0.0330761	sat	0.0206219	sat	0.015686	sat	1.68008	sat	1.68326
chc lia lin 23/chc-LIA-Lin_400.smt2	sat	0.948931	sat	0.964099	sat	0.95347	unknown	0.923558	sat	0.0515999	sat	0.132553	sat	0.394004	sat	0.334295	sat	3.34227	sat	3.49757
chc lia lin 23/chc-LIA-Lin_401.smt2	unsat	0.0248221	unsat	0.024036	unsat	0.0246279	unsat	0.0425109	unsat	0.036137	unsat	0.0304751	unsat	0.023006	unsat	0.011067	unsat	1.72631	unsat	1.63235
chc lia lin 23/chc-LIA-Lin_402.smt2	unknown	300.018	unknown	300.019	unknown	300.054	unknown	21.8812	unknown	300.03	sat	0.156218	unknown	300.085	unknown	300.023	unknown	300.024	sat	10.3912
chc lia lin 23/chc-LIA-Lin_403.smt2	unknown	300.059	unknown	300.073	unknown	300.014	unknown	300.015	unknown	300.044	sat	14.7143	unknown	300.021	unknown	300.026	unknown	300.036	unknown	300.099
chc lia lin 23/chc-LIA-Lin_404.smt2	unknown	300.073	unknown	300.013	unknown	300.025	unknown	300.015	unsat	133.338	unsat	11.6092	unknown	300.026	unknown	300.025	unknown	300.11	unknown	300.046
chc lia lin 23/chc-LIA-Lin_405.smt2	unknown	300.015	unknown	300.022	unknown	300.024	unknown	300.023	unknown	300.055	unknown	300.02	unknown	300.024	unknown	300.018	unknown	300.053	unknown	300.032
chc lia lin 23/chc-LIA-Lin_406.smt2	unknown	300.04	unknown	300.076	unknown	300.025	unknown	300.115	unknown	300.102	sat	6.1247	unknown	300.115	unknown	300.03	unknown	300.112	unknown	300.039
chc lia lin 23/chc-LIA-Lin_407.smt2	unknown	300.024	unknown	300.018	unknown	300.114	unknown	300.114	unknown	300.026	sat	12.1233	unknown	300.015	unknown	300.039	unknown	300.038	unknown	300.021
chc lia lin 23/chc-LIA-Lin_408.smt2	unknown	300.105	unknown	300.05	unknown	300.015	unknown	300.105	unknown	300.045	sat	38.253	unknown	300.032	unknown	300.033	unknown	300.03	unknown	300.077
chc lia lin 23/chc-LIA-Lin_409.smt2	unknown	300.014	unknown	300.019	unknown	300.029	unknown	300.109	unknown	300.027	unknown	300.095	unknown	300.105	unknown	300.024	unknown	300.033	unknown	300.124
chc lia lin 23/chc-LIA-Lin_410.smt2	unknown	300.014	unknown	300.055	unknown	300.075	unknown	300.103	unknown	300.03	unknown	300.015	unknown	300.015	unknown	300.027	unknown	300.025	unknown	300.028
chc lia lin 23/chc-LIA-Lin_411.smt2	sat	0.256398	sat	0.259069	sat	0.255685	unknown	0.232016	unknown	0.0775559	sat	0.100787	sat	0.120511	unknown	300.026	sat	2.5451	sat	2.58066
chc lia lin 23/chc-LIA-Lin_412.smt2	unknown	300.081	unknown	300.017	unknown	300.019	unknown	300.018	unknown	300.061	sat	4.89079	unknown	300.015	unknown	300.024	unknown	300.083	unknown	300.026
chc lia lin 23/chc-LIA-Lin_413.smt2	unknown	300.105	unknown	300.015	unknown	300.015	unknown	300.014	unknown	300.035	unknown	300.056	unknown	300.024	unknown	300.116	unknown	300.124	unknown	300.107
chc lia lin 23/chc-LIA-Lin_414.smt2	unknown	300.071	unknown	300.096	unknown	300.093	unknown	300.105	unknown	300.015	unknown	300.116	unknown	300.026	unknown	300.017	unknown	300.119	unknown	300.049
chc lia lin 23/chc-LIA-Lin_415.smt2	unknown	300.047	unknown	300.06	unknown	300.042	unknown	300.105	unknown	300.028	sat	80.9289	unknown	300.105	unknown	300.116	unknown	300.034	unknown	300.034
chc lia lin 23/chc-LIA-Lin_416.smt2	unknown	300.023	unknown	300.042	unknown	300.025	unknown	300.105	unknown	300.025	sat	2.8116	unknown	300.033	unknown	300.032	unknown	300.032	unknown	300.091
chc lia lin 23/chc-LIA-Lin_417.smt2	unknown	300.115	unknown	300.02	unknown	300.025	unknown	300.024	unknown	300.113	unknown	300.024	unknown	300.026	unknown	300.11	unknown	300.023	unknown	300.035
chc lia lin 23/chc-LIA-Lin_418.smt2	unknown	300.014	unknown	300.025	unknown	300.017	unknown	300.015	unknown	300.024	sat	5.09071	unknown	300.015	unknown	300.015	unknown	300.108	unknown	300.022
chc lia lin 23/chc-LIA-Lin_419.smt2	unknown	300.077	unknown	300.022	unknown	300.023	unknown	300.028	unknown	300.062	sat	6.98434	unknown	300.015	unknown	300.031	unknown	300.025	unknown	300.036
chc lia lin 23/chc-LIA-Lin_420.smt2	unknown	300.014	unknown	300.033	unknown	300.014	unknown	300.098	unknown	300.015	sat	20.8573	unknown	300.019	unknown	300.017	unknown	300.021	unknown	300.113
chc lia lin 23/chc-LIA-Lin_421.smt2	unknown	300.024	unknown	300.024	unknown	300.015	unknown	300.052	unknown	300.105	unknown	300.038	unknown	300.024	unknown	300.026	unknown	300.056	unknown	300.034