============================================================================
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: qbf-hardness (198 formulas)

combined solved unsat:	39
combined solved sat:	12
combined solved all:	51

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: 0

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: 0

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: 0

statistics for bloqqer:
  solved unsat:	37
  solved sat:	12
  solved all:	49

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

statistics for hiqqer3p:
  solved unsat:	39
  solved sat:	12
  solved all:	51

statistics for squeeze:
  solved unsat:	12
  solved sat:	0
  solved all:	12

statistics for num-rounds-6-120sec-ABCD:
  solved unsat:	39
  solved sat:	12
  solved all:	51

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

  fixpoints after round 1: 0
  fixpoints after round 2: 24
  fixpoints after round 3: 110
  fixpoints after round 4: 11
  fixpoints after round 5: 2
  fixpoints after round 6: 0
  total fixpoints: 147


bloqqer vs. hiqqer3e (format "< | = | >"):
all solved:	49 | 0 | 0
unsat solved:	37 | 0 | 0
sat solved:	12 | 0 | 0

bloqqer vs. hiqqer3p (format "< | = | >"):
all solved:	0 | 49 | 2
unsat solved:	0 | 37 | 2
sat solved:	0 | 12 | 0

bloqqer vs. squeeze (format "< | = | >"):
all solved:	37 | 12 | 0
unsat solved:	25 | 12 | 0
sat solved:	12 | 0 | 0

bloqqer vs. num-rounds-6-120sec-ABCD (format "< | = | >"):
all solved:	0 | 49 | 2
unsat solved:	0 | 37 | 2
sat solved:	0 | 12 | 0

hiqqer3e vs. hiqqer3p (format "< | = | >"):
all solved:	0 | 0 | 51
unsat solved:	0 | 0 | 39
sat solved:	0 | 0 | 12

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

hiqqer3e vs. num-rounds-6-120sec-ABCD (format "< | = | >"):
all solved:	0 | 0 | 51
unsat solved:	0 | 0 | 39
sat solved:	0 | 0 | 12

hiqqer3p vs. squeeze (format "< | = | >"):
all solved:	39 | 12 | 0
unsat solved:	27 | 12 | 0
sat solved:	12 | 0 | 0

hiqqer3p vs. num-rounds-6-120sec-ABCD (format "< | = | >"):
all solved:	0 | 51 | 0
unsat solved:	0 | 39 | 0
sat solved:	0 | 12 | 0

squeeze vs. num-rounds-6-120sec-ABCD (format "< | = | >"):
all solved:	0 | 12 | 39
unsat solved:	0 | 12 | 27
sat solved:	0 | 0 | 12