============================================================================
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: planning-CTE (150 formulas)

combined solved unsat:	3
combined solved sat:	8
combined solved all:	11

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

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

statistics for bloqqer:
  solved unsat:	1
  solved sat:	2
  solved all:	3

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

statistics for hiqqer3p:
  solved unsat:	1
  solved sat:	6
  solved all:	7

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

statistics for num-rounds-6-120sec-ABCD:
  solved unsat:	3
  solved sat:	8
  solved all:	11

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

  fixpoints after round 1: 16
  fixpoints after round 2: 42
  fixpoints after round 3: 55
  fixpoints after round 4: 15
  fixpoints after round 5: 7
  fixpoints after round 6: 1
  total fixpoints: 136


bloqqer vs. hiqqer3e (format "< | = | >"):
all solved:	3 | 0 | 0
unsat solved:	1 | 0 | 0
sat solved:	2 | 0 | 0

bloqqer vs. hiqqer3p (format "< | = | >"):
all solved:	0 | 3 | 4
unsat solved:	0 | 1 | 0
sat solved:	0 | 2 | 4

bloqqer vs. squeeze (format "< | = | >"):
all solved:	3 | 0 | 0
unsat solved:	1 | 0 | 0
sat solved:	2 | 0 | 0

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

hiqqer3e vs. hiqqer3p (format "< | = | >"):
all solved:	0 | 0 | 7
unsat solved:	0 | 0 | 1
sat solved:	0 | 0 | 6

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

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

hiqqer3p vs. squeeze (format "< | = | >"):
all solved:	7 | 0 | 0
unsat solved:	1 | 0 | 0
sat solved:	6 | 0 | 0

hiqqer3p vs. num-rounds-6-120sec-ABCD (format "< | = | >"):
all solved:	0 | 7 | 4
unsat solved:	0 | 1 | 2
sat solved:	0 | 6 | 2

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