============================================================================
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: reduction-finding-full-set-params-k1c3n4 (4608 formulas)

combined solved unsat:	927
combined solved sat:	963
combined solved all:	1890

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

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

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

statistics for bloqqer:
  solved unsat:	659
  solved sat:	837
  solved all:	1496

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

statistics for hiqqer3p:
  solved unsat:	726
  solved sat:	924
  solved all:	1650

statistics for squeeze:
  solved unsat:	348
  solved sat:	326
  solved all:	674

statistics for num-rounds-6-120sec-ABCD:
  solved unsat:	919
  solved sat:	936
  solved all:	1855

  solved in round 1: 1711
  solved in round 2: 121
  solved in round 3: 22
  solved in round 4: 0
  solved in round 5: 1
  solved in round 6: 0

  fixpoints after round 1: 0
  fixpoints after round 2: 903
  fixpoints after round 3: 1654
  fixpoints after round 4: 152
  fixpoints after round 5: 21
  fixpoints after round 6: 1
  total fixpoints: 2731


bloqqer vs. hiqqer3e (format "< | = | >"):
all solved:	1320 | 176 | 0
unsat solved:	483 | 176 | 0
sat solved:	837 | 0 | 0

bloqqer vs. hiqqer3p (format "< | = | >"):
all solved:	29 | 1467 | 183
unsat solved:	13 | 646 | 80
sat solved:	16 | 821 | 103

bloqqer vs. squeeze (format "< | = | >"):
all solved:	822 | 674 | 0
unsat solved:	311 | 348 | 0
sat solved:	511 | 326 | 0

bloqqer vs. num-rounds-6-120sec-ABCD (format "< | = | >"):
all solved:	2 | 1494 | 361
unsat solved:	1 | 658 | 261
sat solved:	1 | 836 | 100

hiqqer3e vs. hiqqer3p (format "< | = | >"):
all solved:	0 | 176 | 1474
unsat solved:	0 | 176 | 550
sat solved:	0 | 0 | 924

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

hiqqer3e vs. num-rounds-6-120sec-ABCD (format "< | = | >"):
all solved:	0 | 176 | 1679
unsat solved:	0 | 176 | 743
sat solved:	0 | 0 | 936

hiqqer3p vs. squeeze (format "< | = | >"):
all solved:	976 | 674 | 0
unsat solved:	378 | 348 | 0
sat solved:	598 | 326 | 0

hiqqer3p vs. num-rounds-6-120sec-ABCD (format "< | = | >"):
all solved:	35 | 1615 | 240
unsat solved:	8 | 718 | 201
sat solved:	27 | 897 | 39

squeeze vs. num-rounds-6-120sec-ABCD (format "< | = | >"):
all solved:	0 | 674 | 1181
unsat solved:	0 | 348 | 571
sat solved:	0 | 326 | 610