PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:

LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.

General information on the benchmark

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-bk4x3.opb
MD5SUM	c2339539ffa69702e62053614fe34ce1
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	44800
Optimality of the best value was proved	NO
Number of terms in the objective function	252
Biggest coefficient in the objective function	2621440
Number of bits for the biggest coefficient in the objective function	22
Sum of the numbers in the objective function	35682270
Number of bits of the sum of numbers in the objective function	26
Biggest number in a constraint	2621440
Number of bits of the biggest number in a constraint	22
Biggest sum of numbers in a constraint	35682270
Number of bits of the biggest sum of numbers	26
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	24.1133
Number of variables	252
Total number of constraints	19
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	19
Minimum length of a constraint	21
Maximum length of a constraint	80

Trace number 17788

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc8 THE 2005-04-21 12:24:01 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18980 boxname=wulflinc8 idbench=1460 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c2339539ffa69702e62053614fe34ce1  /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-bk4x3.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-bk4x3.opb /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-bk4x3.opb
IDLAUNCH: 18980
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        679112 kB
Buffers:         29536 kB
Cached:         303868 kB
SwapCached:          0 kB
Active:          75180 kB
Inactive:       261076 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        678860 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            13504 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 12:24:32 (client local time) WITH STATUS 30 IN 30.7393 SECONDS
stats: 18980 0 30.7393 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 26 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######
c   -- Clauses(.)/Splits(s): (none)
c ---[  24]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  22]---> Sorter-cost:  261     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  20]---> Sorter-cost:  275     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  18]---> Sorter-cost:  261     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  16]---> Sorter-cost:  455     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  14]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  12]---> Sorter-cost:  455     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  11]---> BDD-cost:   14
c ---[  10]---> BDD-cost:   14
c ---[   9]---> BDD-cost:   15
c ---[   8]---> BDD-cost:   15
c ---[   7]---> BDD-cost:   14
c ---[   6]---> BDD-cost:   15
c ---[   5]---> BDD-cost:   16
c ---[   4]---> BDD-cost:   16
c ---[   3]---> BDD-cost:   15
c ---[   2]---> BDD-cost:   16
c ---[   1]---> BDD-cost:   16
c ---[   0]---> BDD-cost:   15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    5825    13949 |    1941       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 65792[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 6116     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         4 |   22275    52576 |    7425       4       79    19.8 |  0.000 % |
c |       104 |   22275    52576 |    8167     104     1413    13.6 |  4.282 % |
c |       256 |   22204    52417 |    8984     249     3597    14.4 |  4.530 % |
c |       482 |   22204    52417 |    9882     475     9729    20.5 |  4.530 % |
c ==============================================================================
c [1mFound solution: 64770[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       518 |   22281    52622 |    7427     511    10640    20.8 |  4.530 % |
c |       619 |   22281    52622 |    8169     612    12071    19.7 |  4.535 % |
c ==============================================================================
c [1mFound solution: 64430[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       755 |   22300    52671 |    7433     748    15922    21.3 |  4.535 % |
c ==============================================================================
c [1mFound solution: 60844[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       777 |   22387    52884 |    7462     770    16097    20.9 |  4.535 % |
c |       878 |   22331    52759 |    8208     868    17315    19.9 |  4.738 % |
c |      1029 |   22234    52540 |    9029    1016    18827    18.5 |  5.062 % |
c |      1256 |   22234    52540 |    9931    1243    33207    26.7 |  5.062 % |
c ==============================================================================
c [1mFound solution: 59264[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1467 |   22070    52183 |    7356    1445    35416    24.5 |  5.062 % |
c |      1567 |   22070    52183 |    8091    1545    38231    24.7 |  5.779 % |
c ==============================================================================
c [1mFound solution: 59132[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1662 |   22069    52189 |    7356    1639    40588    24.8 |  5.779 % |
c |      1763 |   22069    52189 |    8091    1740    43647    25.1 |  5.878 % |
c ==============================================================================
c [1mFound solution: 54528[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1778 |   22132    52347 |    7377    1755    43800    25.0 |  5.878 % |
c |      1878 |   22128    52337 |    8114    1854    46254    24.9 |  5.889 % |
c ==============================================================================
c [1mFound solution: 54016[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1897 |   22148    52389 |    7382    1873    46501    24.8 |  5.889 % |
c |      1997 |   22144    52380 |    8120    1972    50391    25.6 |  5.911 % |
c |      2147 |   22119    52325 |    8932    2118    56697    26.8 |  6.001 % |
c ==============================================================================
c [1mFound solution: 51968[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2290 |   21942    51926 |    7314    2230    57387    25.7 |  6.001 % |
c |      2390 |   21942    51926 |    8045    2330    62839    27.0 |  6.732 % |
c |      2541 |   21942    51926 |    8849    2481    66992    27.0 |  6.732 % |
c ==============================================================================
c [1mFound solution: 49920[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2580 |   21974    52006 |    7324    2520    67806    26.9 |  6.732 % |
c |      2680 |   21921    51887 |    8056    2617    70855    27.1 |  6.928 % |
c |      2831 |   21921    51887 |    8862    2768    74266    26.8 |  6.928 % |
c |      3060 |   21910    51863 |    9748    2996    80014    26.7 |  6.966 % |
c |      3397 |   21910    51863 |   10723    3333    89368    26.8 |  6.966 % |
c |      3904 |   21910    51863 |   11795    3840   100023    26.0 |  6.966 % |
c |      4663 |   21873    51779 |   12974    4598   124013    27.0 |  7.095 % |
c |      5802 |   21873    51779 |   14272    5737   152063    26.5 |  7.095 % |
c |      7513 |   21873    51779 |   15699    7448   208330    28.0 |  7.095 % |
c |     10075 |   21873    51779 |   17269   10010   291552    29.1 |  7.095 % |
c |     13919 |   21873    51779 |   18996   13854   388315    28.0 |  7.095 % |
c ==============================================================================
c [1mFound solution: 49788[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14939 |   21897    51839 |    7299   14874   442859    29.8 |  7.095 % |
c |     15041 |   21897    51839 |    8028    7539   199867    26.5 |  7.102 % |
c |     15193 |   21897    51839 |    8831    7691   205789    26.8 |  7.102 % |
c ==============================================================================
c [1mFound solution: 48640[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15320 |   21916    51886 |    7305    7818   208861    26.7 |  7.102 % |
c |     15420 |   21916    51886 |    8035    7918   211404    26.7 |  7.109 % |
c |     15571 |   21916    51886 |    8839    8069   215707    26.7 |  7.109 % |
c |     15797 |   21916    51886 |    9722    8295   221766    26.7 |  7.109 % |
c |     16135 |   21916    51886 |   10695    8633   244121    28.3 |  7.109 % |
c |     16642 |   21916    51886 |   11764    9140   255079    27.9 |  7.109 % |
c ==============================================================================
c [1mFound solution: 48384[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17349 |   21920    51896 |    7306    9847   289653    29.4 |  7.109 % |
c |     17449 |   21916    51887 |    8036    5022   155735    31.0 |  7.133 % |
c |     17599 |   21916    51887 |    8840    5172   160564    31.0 |  7.133 % |
c |     17824 |   21916    51887 |    9724    5397   171739    31.8 |  7.133 % |
c ==============================================================================
c [1mFound solution: 48280[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17934 |   21941    51948 |    7313    5507   175558    31.9 |  7.133 % |
c |     18034 |   21941    51948 |    8044    5607   176712    31.5 |  7.138 % |
c |     18185 |   21941    51948 |    8848    5758   178732    31.0 |  7.138 % |
c |     18411 |   21941    51948 |    9733    5984   185431    31.0 |  7.138 % |
c |     18748 |   21941    51948 |   10706    6321   195258    30.9 |  7.138 % |
c |     19255 |   21938    51942 |   11777    6827   209198    30.6 |  7.151 % |
c ==============================================================================
c [1mFound solution: 44800[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19581 |   21969    52018 |    7323    7151   218349    30.5 |  7.151 % |
c |     19681 |   21969    52018 |    8055    7251   220564    30.4 |  7.250 % |
c |     19831 |   21969    52018 |    8860    7401   223248    30.2 |  7.250 % |
c |     20056 |   21969    52018 |    9746    7626   227635    29.8 |  7.250 % |
c |     20393 |   21969    52018 |   10721    7963   232942    29.3 |  7.250 % |
c |     20899 |   21956    51989 |   11793    8467   242195    28.6 |  7.301 % |
c |     21658 |   21273    50415 |   12973    4939   133172    27.0 |  9.735 % |
c ==============================================================================
c [1mOptimal solution: 44800[0m
s OPTIMUM FOUND
v -X0_bit_7 -X0_bit_6 -X0_bit_5 -X0_bit_4 -X0_bit_3 -X0_bit_2 -X0_bit_1 -X0_bit0 -X0_bit1 -X0_bit2 -X0_bit3 -X0_bit4 -X0_bit5 -X0_bit6 -X0_bit7 -X0_bit8 -X0_bit9 -X0_bit10 -X0_bit11 -X0_bit12 -X1_bit_7 -X1_bit_6 -X1_bit_5 -X1_bit_4 -X1_bit_3 -X1_bit_2 -X1_bit_1 -X1_bit0 -X1_bit1 -X1_bit2 -X1_bit3 -X1_bit4 -X1_bit5 -X1_bit6 -X1_bit7 -X1_bit8 -X1_bit9 -X1_bit10 -X1_bit11 -X1_bit12 -X2_bit_7 -X2_bit_6 -X2_bit_5 -X2_bit_4 -X2_bit_3 -X2_bit_2 -X2_bit_1 -X2_bit0 X2_bit1 -X2_bit2 X2_bit3 -X2_bit4 -X2_bit5 -X2_bit6 -X2_bit7 -X2_bit8 -X2_bit9 -X2_bit10 -X2_bit11 -X2_bit12 -X3_bit_7 -X3_bit_6 -X3_bit_5 -X3_bit_4 -X3_bit_3 -X3_bit_2 -X3_bit_1 -X3_bit0 -X3_bit1 -X3_bit2 -X3_bit3 -X3_bit4 -X3_bit5 -X3_bit6 -X3_bit7 -X3_bit8 -X3_bit9 -X3_bit10 -X3_bit11 -X3_bit12 -X4_bit_7 -X4_bit_6 -X4_bit_5 -X4_bit_4 -X4_bit_3 -X4_bit_2 -X4_bit_1 -X4_bit0 X4_bit1 X4_bit2 X4_bit3 X4_bit4 -X4_bit5 -X4_bit6 -X4_bit7 -X4_bit8 -X4_bit9 -X4_bit10 -X4_bit11 -X4_bit12 -X5_bit_7 -X5_bit_6 -X5_bit_5 -X5_bit_4 -X5_bit_3 -X5_bit_2 -X5_bit_1 -X5_bit0 -X5_bit1 -X5_bit2 -X5_bit3 -X5_bit4 -X5_bit5 -X5_bit6 -X5_bit7 -X5_bit8 -X5_bit9 -X5_bit10 -X5_bit11 -X5_bit12 -X6_bit_7 -X6_bit_6 -X6_bit_5 -X6_bit_4 -X6_bit_3 -X6_bit_2 -X6_bit_1 -X6_bit0 -X6_bit1 X6_bit2 -X6_bit3 X6_bit4 -X6_bit5 -X6_bit6 -X6_bit7 -X6_bit8 -X6_bit9 -X6_bit10 -X6_bit11 -X6_bit12 -X7_bit_7 -X7_bit_6 -X7_bit_5 -X7_bit_4 -X7_bit_3 -X7_bit_2 -X7_bit_1 -X7_bit0 -X7_bit1 X7_bit2 -X7_bit3 X7_bit4 -X7_bit5 -X7_bit6 -X7_bit7 -X7_bit8 -X7_bit9 -X7_bit10 -X7_bit11 -X7_bit12 -X8_bit_7 -X8_bit_6 -X8_bit_5 -X8_bit_4 -X8_bit_3 -X8_bit_2 -X8_bit_1 -X8_bit0 -X8_bit1 -X8_bit2 -X8_bit3 -X8_bit4 -X8_bit5 -X8_bit6 -X8_bit7 -X8_bit8 -X8_bit9 -X8_bit10 -X8_bit11 -X8_bit12 -X9_bit_7 -X9_bit_6 -X9_bit_5 -X9_bit_4 -X9_bit_3 -X9_bit_2 -X9_bit_1 -X9_bit0 -X9_bit1 -X9_bit2 -X9_bit3 -X9_bit4 -X9_bit5 -X9_bit6 -X9_bit7 -X9_bit8 -X9_bit9 -X9_bit10 -X9_bit11 -X9_bit12 -X10_bit_7 -X10_bit_6 -X10_bit_5 -X10_bit_4 -X10_bit_3 -X10_bit_2 -X10_bit_1 -X10_bit0 -X10_bit1 -X10_bit2 -X10_bit3 -X10_bit4 -X10_bit5 -X10_bit6 -X10_bit7 -X10_bit8 -X10_bit9 -X10_bit10 -X10_bit11 -X10_bit12 -X11_bit_7 -X11_bit_6 -X11_bit_5 -X11_bit_4 -X11_bit_3 -X11_bit_2 -X11_bit_1 -X11_bit0 -X11_bit1 X11_bit2 -X11_bit3 X11_bit4 -X11_bit5 -X11_bit6 -X11_bit7 -X11_bit8 -X11_bit9 -X11_bit10 -X11_bit11 -X11_bit12 -Y0_bit0 -Y1_bit0 Y2_bit0 -Y3_bit0 Y4_bit0 -Y5_bit0 Y6_bit0 Y7_bit0 -Y8_bit0 -Y9_bit0 -Y10_bit0 Y11_bit0
c _______________________________________________________________________________
c 
c restarts              : 61
c conflicts             : 21813          (711 /sec)
c decisions             : 35162          (1146 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 30.6793 s
c _______________________________________________________________________________
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.79 0.92 0.90 2/54 29906
Raw data (stat): 29906 (runsolver) R 29905 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 473268230 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.82 0.93 0.90 2/54 29906
Raw data (stat): 29906 (minisat+) R 29905 26667 26666 0 -1 0 1226 0 0 0 995 3 0 0 25 0 1 0 473268230 6627328 1204 4294967295 134512640 134672761 3221224544 3221223648 134559953 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1618 1204 603 41 0 1577 0
vsize: 6472
[startup+20.0022 s]
Raw data (loadavg): 0.85 0.93 0.90 2/54 29906
Raw data (stat): 29906 (minisat+) R 29905 26667 26666 0 -1 0 1513 0 0 0 1993 4 0 0 25 0 1 0 473268230 7823360 1491 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1910 1491 603 41 0 1869 0
vsize: 7640
[startup+30.0034 s]
Raw data (loadavg): 0.87 0.93 0.90 2/54 29906
Raw data (stat): 29906 (minisat+) R 29905 26667 26666 0 -1 0 1531 0 0 0 2993 5 0 0 25 0 1 0 473268230 7954432 1509 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1942 1509 603 41 0 1901 0
vsize: 7768
[startup+30.7642 s]
Raw data (loadavg): 0.87 0.93 0.90 1/53 29906
Raw data (stat): 29906 (minisat+) R 29905 26667 26666 0 -1 0 1531 0 0 0 2993 5 0 0 25 0 1 0 473268230 7954432 1509 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1942 1509 603 41 0 1901 0
vsize: 0

Child status: 30
Real time (s): 30.7639
CPU time (s): 30.7393
CPU user time (s): 30.6823
CPU system time (s): 0.056991
CPU usage (%): 99.92
Max. virtual memory (Kb): 7768
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	44800
#### END VERIFIER DATA ####