clauses=6663
variables=270
bytes=92378
ccs=1
cls1=0
cls2=1362
cls3=5280
cls4=0
cls5=0
cls6=0
cls7=0
cls8=12
cls9=0
cls10p=9
horn=21
invhorn=6642
positive=21
negative=1890
hornvars_mean=0.752768
hornvars_variance=0.186109
hornvars_min=0
hornvars_max=1
hornvars_entropy=0.806862
invhornvars_mean=68.5018
invhornvars_variance=1543.64
invhornvars_min=0
invhornvars_max=107
invhornvars_entropy=0.792709
balancecls_mean=0.356596
balancecls_variance=0.0511373
balancecls_min=0
balancecls_max=0.5
balancecls_entropy=0.864562
balancevars_mean=0.0506337
balancevars_variance=0.00159035
balancevars_min=0.00934579
balancevars_max=0.111111
balancevars_entropy=0.056794
vcg_vdegree_mean=69.2546
vcg_vdegree_variance=1538.74
vcg_vdegree_min=0
vcg_vdegree_max=108
vcg_vdegree_entropy=0.792709
vcg_cdegree_mean=2.81675
vcg_cdegree_variance=0.325267
vcg_cdegree_min=2
vcg_cdegree_max=12
vcg_cdegree_entropy=0.381729
vg_degree_mean=203.07
vg_degree_variance=13155
vg_degree_min=0
vg_degree_max=314
vg_degree_entropy=0.792709
cg_degree_mean=257.657
cg_degree_variance=6770.82
cg_degree_min=38
cg_degree_max=1296
cg_degree_entropy=0.502856
