============================================================================
2013-06-03 QBF Gallery 2013 preliminary results for showcase "Preprocessing"
============================================================================

Notation:

"A" is hiqqer3e
"B" is bloqqer
"C" is hiqqer3p
"D" is squeeze

Experiment: 6 rounds of incremental preprocessing with detection of fixpoints,
120 seconds time limit for each call of a preprocessor.

The execution sequence "ABCD" was considered.

----------------------------------------------------------------

benchmark set: sauer-reimer (924 formulas)

combined solved unsat:	149
combined solved sat:	31
combined solved all:	180

count unique solved for unsat:
bloqqer unique solved unsat: 0
hiqqer3e unique solved unsat: 0
hiqqer3p unique solved unsat: 0
squeeze unique solved unsat: 0
num-rounds-6-120sec-ABCD unique solved unsat: 20

count unique solved for sat:
bloqqer unique solved sat: 0
hiqqer3e unique solved sat: 0
hiqqer3p unique solved sat: 0
squeeze unique solved sat: 0
num-rounds-6-120sec-ABCD unique solved sat: 2

count unique solved for all:
bloqqer unique solved all: 0
hiqqer3e unique solved all: 0
hiqqer3p unique solved all: 0
squeeze unique solved all: 0
num-rounds-6-120sec-ABCD unique solved all: 22

statistics for bloqqer:
  solved unsat:	113
  solved sat:	24
  solved all:	137

statistics for hiqqer3e:
  solved unsat:	81
  solved sat:	0
  solved all:	81

statistics for hiqqer3p:
  solved unsat:	124
  solved sat:	29
  solved all:	153

statistics for squeeze:
  solved unsat:	69
  solved sat:	9
  solved all:	78

statistics for num-rounds-6-120sec-ABCD:
  solved unsat:	149
  solved sat:	31
  solved all:	180

  solved in round 1: 169
  solved in round 2: 6
  solved in round 3: 3
  solved in round 4: 2
  solved in round 5: 0
  solved in round 6: 0

  fixpoints after round 1: 0
  fixpoints after round 2: 0
  fixpoints after round 3: 2
  fixpoints after round 4: 223
  fixpoints after round 5: 246
  fixpoints after round 6: 118
  total fixpoints: 589


bloqqer vs. hiqqer3e (format "< | = | >"):
all solved:	62 | 75 | 6
unsat solved:	38 | 75 | 6
sat solved:	24 | 0 | 0

bloqqer vs. hiqqer3p (format "< | = | >"):
all solved:	0 | 137 | 16
unsat solved:	0 | 113 | 11
sat solved:	0 | 24 | 5

bloqqer vs. squeeze (format "< | = | >"):
all solved:	59 | 78 | 0
unsat solved:	44 | 69 | 0
sat solved:	15 | 9 | 0

bloqqer vs. num-rounds-6-120sec-ABCD (format "< | = | >"):
all solved:	0 | 137 | 43
unsat solved:	0 | 113 | 36
sat solved:	0 | 24 | 7

hiqqer3e vs. hiqqer3p (format "< | = | >"):
all solved:	5 | 76 | 77
unsat solved:	5 | 76 | 48
sat solved:	0 | 0 | 29

hiqqer3e vs. squeeze (format "< | = | >"):
all solved:	15 | 66 | 12
unsat solved:	15 | 66 | 3
sat solved:	0 | 0 | 9

hiqqer3e vs. num-rounds-6-120sec-ABCD (format "< | = | >"):
all solved:	0 | 81 | 99
unsat solved:	0 | 81 | 68
sat solved:	0 | 0 | 31

hiqqer3p vs. squeeze (format "< | = | >"):
all solved:	75 | 78 | 0
unsat solved:	55 | 69 | 0
sat solved:	20 | 9 | 0

hiqqer3p vs. num-rounds-6-120sec-ABCD (format "< | = | >"):
all solved:	0 | 153 | 27
unsat solved:	0 | 124 | 25
sat solved:	0 | 29 | 2

squeeze vs. num-rounds-6-120sec-ABCD (format "< | = | >"):
all solved:	0 | 78 | 102
unsat solved:	0 | 69 | 80
sat solved:	0 | 9 | 22