Overall CNF Statistics
----------------------
Number of domains                     30
Number of abstract problems         4530
Number of generic problems            86
Number of problems                  5689       : 5644 NP (99%) +   45 Pr ( 0%)
Number of non-Horn problems         3354 (58%) : 3323 NP (58%) +   31 Pr ( 0%)
Number of range rest. problems       583 ( 10%) :  538 NP ( 9%) +   45 Pr ( 0%)
Number of problems with equality    3754 (65%)
Number of pure equality problems    1299 (22%)
Number of unit equality problems     860 (15%)
Number of satisfiable problems >=   815 ( 14%) :  807 NP (14%) +    8 Pr ( 0%)
Number of standard problems         3496 (61%) : 3494 NP (61%) +    2 Pr ( 0%)
 
 
Problem-by-problem              Non-propositional            Propositional
------------------           Min    Max    Av   Med     Min    Max    Av   Med
                             ----------------------     ----------------------
Number of clauses              1   3240    92    34       1    204    33    18
% of non-Horn clauses         0%    99%   13%    7%      0%    81%   24%   20%
  in non-Horn problems        1%    99%   22%   13%      4%    81%   34%   33%
% of unit clauses             0%   100%   45%   34%      0%   100%   22%    9%
% of range rest. clauses      0%   100%   67%   74%
Number of literals             1 127126   707    81       1    448    86    40
% of equality literals        0%   100%   32%   17%
  in equality problems        0%   100%   48%   22%
Maximal clause size            1     60     6     5       1     11     3     3
Average clause size            1     40     2     2       1      5     1     2
Number of predicate symbols    1   1817    21     4       1     63    16    11
% of propositions             0%    95%    2%    0%
Minimal predicate arity        0     54     1     1
Maximal predicate arity        1     56     3     2
Number of functors             0    244    21    10
% of constants                0%   100%   50%   50%
Minimal functor arity          0      2     0     0
Maximal functor arity          0      8     2     2
Number of variables            0 120428   603    62
% of singletons               0%   100%    9%    6%
Maximal term depth             1     85     4     4
Average term depth             1      8     1     2
