============================================================================
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: conformant-planning (1750 formulas)

combined solved unsat:	925
combined solved sat:	13
combined solved all:	938

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

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

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

statistics for bloqqer:
  solved unsat:	478
  solved sat:	11
  solved all:	489

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

statistics for hiqqer3p:
  solved unsat:	474
  solved sat:	12
  solved all:	486

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

statistics for num-rounds-6-120sec-ABCD:
  solved unsat:	925
  solved sat:	13
  solved all:	938

  solved in round 1: 793
  solved in round 2: 137
  solved in round 3: 5
  solved in round 4: 2
  solved in round 5: 0
  solved in round 6: 1

  fixpoints after round 1: 0
  fixpoints after round 2: 0
  fixpoints after round 3: 31
  fixpoints after round 4: 385
  fixpoints after round 5: 123
  fixpoints after round 6: 32
  total fixpoints: 571


bloqqer vs. hiqqer3e (format "< | = | >"):
all solved:	105 | 384 | 262
unsat solved:	94 | 384 | 262
sat solved:	11 | 0 | 0

bloqqer vs. hiqqer3p (format "< | = | >"):
all solved:	69 | 420 | 66
unsat solved:	69 | 409 | 65
sat solved:	0 | 11 | 1

bloqqer vs. squeeze (format "< | = | >"):
all solved:	441 | 48 | 0
unsat solved:	430 | 48 | 0
sat solved:	11 | 0 | 0

bloqqer vs. num-rounds-6-120sec-ABCD (format "< | = | >"):
all solved:	0 | 489 | 449
unsat solved:	0 | 478 | 447
sat solved:	0 | 11 | 2

hiqqer3e vs. hiqqer3p (format "< | = | >"):
all solved:	261 | 385 | 101
unsat solved:	261 | 385 | 89
sat solved:	0 | 0 | 12

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

hiqqer3e vs. num-rounds-6-120sec-ABCD (format "< | = | >"):
all solved:	0 | 646 | 292
unsat solved:	0 | 646 | 279
sat solved:	0 | 0 | 13

hiqqer3p vs. squeeze (format "< | = | >"):
all solved:	438 | 48 | 0
unsat solved:	426 | 48 | 0
sat solved:	12 | 0 | 0

hiqqer3p vs. num-rounds-6-120sec-ABCD (format "< | = | >"):
all solved:	0 | 486 | 452
unsat solved:	0 | 474 | 451
sat solved:	0 | 12 | 1

squeeze vs. num-rounds-6-120sec-ABCD (format "< | = | >"):
all solved:	0 | 48 | 890
unsat solved:	0 | 48 | 877
sat solved:	0 | 0 | 13