============================================================================
2013-06-25 QBF Gallery 2013 preliminary results for showcase "Preprocessing"
============================================================================

Results for individual preprocessors. Each preprocessor is run individually
and no interaction with the other preprocessors can happen.

Wall clock time limit 300 sec., memory limit 7 GB

---------------------------------------------
eval2012r2 (345 formulas)

combined solved unsat:  51
combined solved sat:    36
combined solved all:    87

bloqqer unique solved unsat: 0
hiqqer3e unique solved unsat: 9
hiqqer3p unique solved unsat: 6
squeeze unique solved unsat: 0

bloqqer unique solved sat: 1
hiqqer3e unique solved sat: 0
hiqqer3p unique solved sat: 3
squeeze unique solved sat: 0

bloqqer unique solved all: 1
hiqqer3e unique solved all: 9
hiqqer3p unique solved all: 9
squeeze unique solved all: 0

statistics for bloqqer:
  solved unsat: 36
  solved sat:   33
  solved all:   69

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

statistics for hiqqer3p:
  solved unsat: 42
  solved sat:   35
  solved all:   77

statistics for squeeze:
  solved unsat: 8
  solved sat:   3
  solved all:   11

bloqqer vs. hiqqer3e (format "< | = | >"):
all solved:     59 | 10 | 9
unsat solved:   26 | 10 | 9
sat solved:     33 | 0 | 0

bloqqer vs. hiqqer3p (format "< | = | >"):
all solved:     1 | 68 | 9
unsat solved:   0 | 36 | 6
sat solved:     1 | 32 | 3

bloqqer vs. squeeze (format "< | = | >"):
all solved:     58 | 11 | 0
unsat solved:   28 | 8 | 0
sat solved:     30 | 3 | 0

hiqqer3e vs. hiqqer3p (format "< | = | >"):
all solved:     9 | 10 | 67
unsat solved:   9 | 10 | 32
sat solved:     0 | 0 | 35

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

hiqqer3p vs. squeeze (format "< | = | >"):
all solved:     66 | 11 | 0
unsat solved:   34 | 8 | 0
sat solved:     32 | 3 | 0

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

qbf-hardness (198 formulas)

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

bloqqer unique solved unsat: 0
hiqqer3e unique solved unsat: 0
hiqqer3p unique solved unsat: 2
squeeze unique solved unsat: 0

bloqqer unique solved sat: 0
hiqqer3e unique solved sat: 0
hiqqer3p unique solved sat: 0
squeeze unique solved sat: 0

bloqqer unique solved all: 0
hiqqer3e unique solved all: 0
hiqqer3p unique solved all: 2
squeeze 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

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

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

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

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

sauer-reimer (924 formulas)


combined solved unsat:  129
combined solved sat:    29
combined solved all:    158

bloqqer unique solved unsat: 0
hiqqer3e unique solved unsat: 5
hiqqer3p unique solved unsat: 10
squeeze unique solved unsat: 0

bloqqer unique solved sat: 0
hiqqer3e unique solved sat: 0
hiqqer3p unique solved sat: 5
squeeze unique solved sat: 0

bloqqer unique solved all: 0
hiqqer3e unique solved all: 5
hiqqer3p unique solved all: 15
squeeze unique solved all: 0

statistics for bloqqer:
  solved unsat: 113
  solved sat:   24
  solved all:   137

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

statistics for hiqqer3p:
  solved unsat: 124
  solved sat:   29
  solved all:   153

statistics for squeeze:
  solved unsat: 69
  solved sat:   9
  solved all:   78

bloqqer vs. hiqqer3e (format "< | = | >"):
all solved:     62 | 75 | 6
unsat solved:   38 | 75 | 6
sat solved:     24 | 0 | 0

bloqqer vs. hiqqer3p (format "< | = | >"):
all solved:     0 | 137 | 16
unsat solved:   0 | 113 | 11
sat solved:     0 | 24 | 5

bloqqer vs. squeeze (format "< | = | >"):
all solved:     59 | 78 | 0
unsat solved:   44 | 69 | 0
sat solved:     15 | 9 | 0

hiqqer3e vs. hiqqer3p (format "< | = | >"):
all solved:     5 | 76 | 77
unsat solved:   5 | 76 | 48
sat solved:     0 | 0 | 29

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

hiqqer3p vs. squeeze (format "< | = | >"):
all solved:     75 | 78 | 0
unsat solved:   55 | 69 | 0
sat solved:     20 | 9 | 0

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

planning-CTE (150 formulas)

combined solved unsat:  1
combined solved sat:    6
combined solved all:    7

bloqqer unique solved unsat: 0
hiqqer3e unique solved unsat: 0
hiqqer3p unique solved unsat: 0
squeeze unique solved unsat: 0

bloqqer unique solved sat: 0
hiqqer3e unique solved sat: 0
hiqqer3p unique solved sat: 4
squeeze unique solved sat: 0

bloqqer unique solved all: 0
hiqqer3e unique solved all: 0
hiqqer3p unique solved all: 4
squeeze unique solved all: 0

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

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

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

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

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

conformant-planning (1750 formulas)

combined solved unsat:  745
combined solved sat:    12
combined solved all:    757

bloqqer unique solved unsat: 10
hiqqer3e unique solved unsat: 202
hiqqer3p unique solved unsat: 5
squeeze unique solved unsat: 0

bloqqer unique solved sat: 0
hiqqer3e unique solved sat: 0
hiqqer3p unique solved sat: 1
squeeze unique solved sat: 0

bloqqer unique solved all: 10
hiqqer3e unique solved all: 202
hiqqer3p unique solved all: 6
squeeze unique solved all: 0

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

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

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

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

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

reduction-finding-full-set-params-k1c3n4 (4608 formulas)

combined solved unsat:  739
combined solved sat:    940
combined solved all:    1679

bloqqer unique solved unsat: 13
hiqqer3e unique solved unsat: 0
hiqqer3p unique solved unsat: 80
squeeze unique solved unsat: 0

bloqqer unique solved sat: 16
hiqqer3e unique solved sat: 0
hiqqer3p unique solved sat: 103
squeeze unique solved sat: 0

bloqqer unique solved all: 29
hiqqer3e unique solved all: 0
hiqqer3p unique solved all: 183
squeeze unique solved all: 0

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

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

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

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