============================================================================
2013-05-24 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 following execution sequences were considered:

AABBCCDD
AABBDDCC
AADDBBCC
BBCCDDAA
DDAABBCC

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

eval2012r2 (345 formulas)


combined solved unsat:	67
combined solved sat:	48
combined solved all:	115

count unique solved for unsat:
num-rounds-6-120sec-AABBCCDD-completion unique solved unsat: 0
num-rounds-6-120sec-AABBDDCC-completion unique solved unsat: 0
num-rounds-6-120sec-AADDBBCC-completion unique solved unsat: 0
num-rounds-6-120sec-BBCCDDAA-completion unique solved unsat: 0
num-rounds-6-120sec-DDAABBCC-completion unique solved unsat: 1

count unique solved for sat:
num-rounds-6-120sec-AABBCCDD-completion unique solved sat: 0
num-rounds-6-120sec-AABBDDCC-completion unique solved sat: 0
num-rounds-6-120sec-AADDBBCC-completion unique solved sat: 1
num-rounds-6-120sec-BBCCDDAA-completion unique solved sat: 1
num-rounds-6-120sec-DDAABBCC-completion unique solved sat: 0

count unique solved for all:
num-rounds-6-120sec-AABBCCDD-completion unique solved all: 0
num-rounds-6-120sec-AABBDDCC-completion unique solved all: 0
num-rounds-6-120sec-AADDBBCC-completion unique solved all: 1
num-rounds-6-120sec-BBCCDDAA-completion unique solved all: 1
num-rounds-6-120sec-DDAABBCC-completion unique solved all: 1

statistics for num-rounds-6-120sec-AABBCCDD-completion:
  solved unsat:	65
  solved sat:	46
  solved all:	111

  solved in round 1: 100
  solved in round 2: 8
  solved in round 3: 2
  solved in round 4: 1
  solved in round 5: 0
  solved in round 6: 0

  fixpoints after round 1: 2
  fixpoints after round 2: 52
  fixpoints after round 3: 76
  fixpoints after round 4: 60
  fixpoints after round 5: 14
  fixpoints after round 6: 2
  total fixpoints: 206

statistics for num-rounds-6-120sec-AABBDDCC-completion:
  solved unsat:	66
  solved sat:	45
  solved all:	111

  solved in round 1: 101
  solved in round 2: 7
  solved in round 3: 2
  solved in round 4: 1
  solved in round 5: 0
  solved in round 6: 0

  fixpoints after round 1: 1
  fixpoints after round 2: 16
  fixpoints after round 3: 113
  fixpoints after round 4: 58
  fixpoints after round 5: 16
  fixpoints after round 6: 3
  total fixpoints: 207

statistics for num-rounds-6-120sec-AADDBBCC-completion:
  solved unsat:	62
  solved sat:	42
  solved all:	104

  solved in round 1: 96
  solved in round 2: 8
  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: 16
  fixpoints after round 3: 137
  fixpoints after round 4: 53
  fixpoints after round 5: 12
  fixpoints after round 6: 0
  total fixpoints: 218

statistics for num-rounds-6-120sec-BBCCDDAA-completion:
  solved unsat:	61
  solved sat:	42
  solved all:	103

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

  fixpoints after round 1: 2
  fixpoints after round 2: 46
  fixpoints after round 3: 81
  fixpoints after round 4: 66
  fixpoints after round 5: 14
  fixpoints after round 6: 2
  total fixpoints: 211

statistics for num-rounds-6-120sec-DDAABBCC-completion:
  solved unsat:	64
  solved sat:	38
  solved all:	102

  solved in round 1: 93
  solved in round 2: 8
  solved in round 3: 1
  solved in round 4: 0
  solved in round 5: 0
  solved in round 6: 0

  fixpoints after round 1: 2
  fixpoints after round 2: 12
  fixpoints after round 3: 141
  fixpoints after round 4: 49
  fixpoints after round 5: 10
  fixpoints after round 6: 4
  total fixpoints: 218

num-rounds-6-120sec-AABBCCDD-completion vs. num-rounds-6-120sec-AABBDDCC-completion (format "< | = | >"):
all solved:	1 | 110 | 1
unsat solved:	0 | 65 | 1
sat solved:	1 | 45 | 0

num-rounds-6-120sec-AABBCCDD-completion vs. num-rounds-6-120sec-AADDBBCC-completion (format "< | = | >"):
all solved:	9 | 102 | 2
unsat solved:	4 | 61 | 1
sat solved:	5 | 41 | 1

num-rounds-6-120sec-AABBCCDD-completion vs. num-rounds-6-120sec-BBCCDDAA-completion (format "< | = | >"):
all solved:	9 | 102 | 1
unsat solved:	4 | 61 | 0
sat solved:	5 | 41 | 1

num-rounds-6-120sec-AABBCCDD-completion vs. num-rounds-6-120sec-DDAABBCC-completion (format "< | = | >"):
all solved:	10 | 101 | 1
unsat solved:	2 | 63 | 1
sat solved:	8 | 38 | 0

num-rounds-6-120sec-AABBDDCC-completion vs. num-rounds-6-120sec-AADDBBCC-completion (format "< | = | >"):
all solved:	8 | 103 | 1
unsat solved:	4 | 62 | 0
sat solved:	4 | 41 | 1

num-rounds-6-120sec-AABBDDCC-completion vs. num-rounds-6-120sec-BBCCDDAA-completion (format "< | = | >"):
all solved:	10 | 101 | 2
unsat solved:	5 | 61 | 0
sat solved:	5 | 40 | 2

num-rounds-6-120sec-AABBDDCC-completion vs. num-rounds-6-120sec-DDAABBCC-completion (format "< | = | >"):
all solved:	10 | 101 | 1
unsat solved:	3 | 63 | 1
sat solved:	7 | 38 | 0

num-rounds-6-120sec-AADDBBCC-completion vs. num-rounds-6-120sec-BBCCDDAA-completion (format "< | = | >"):
all solved:	5 | 99 | 4
unsat solved:	3 | 59 | 2
sat solved:	2 | 40 | 2

num-rounds-6-120sec-AADDBBCC-completion vs. num-rounds-6-120sec-DDAABBCC-completion (format "< | = | >"):
all solved:	6 | 98 | 4
unsat solved:	2 | 60 | 4
sat solved:	4 | 38 | 0

num-rounds-6-120sec-BBCCDDAA-completion vs. num-rounds-6-120sec-DDAABBCC-completion (format "< | = | >"):
all solved:	6 | 97 | 5
unsat solved:	1 | 60 | 4
sat solved:	5 | 37 | 1