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 14855

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc22 THE 2005-04-21 02:08:29 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18979 boxname=wulflinc22 idbench=1460 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c2339539ffa69702e62053614fe34ce1  /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-bk4x3.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-bk4x3.opb /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-bk4x3.opb
IDLAUNCH: 18979
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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:        814976 kB
Buffers:         18824 kB
Cached:         170396 kB
SwapCached:         24 kB
Active:          23416 kB
Inactive:       168544 kB
HighTotal:      131008 kB
HighFree:        59724 kB
LowTotal:       903652 kB
LowFree:        755252 kB
SwapTotal:     2097892 kB
SwapFree:      2097660 kB
Dirty:              52 kB
Writeback:           0 kB
Mapped:           6640 kB
Slab:            22128 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 02:08:53 (client local time) WITH STATUS 30 IN 24.1133 SECONDS
stats: 18979 0 24.1133 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]---> BDD-cost:  112
c ---[  22]---> BDD-cost:  126
c ---[  20]---> BDD-cost:  132
c ---[  18]---> BDD-cost:  124
c ---[  16]---> BDD-cost:  219
c ---[  14]---> BDD-cost:  238
c ---[  12]---> BDD-cost:  224
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 |    3221     8700 |    1073       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 68594[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 6120     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 |         3 |   17475    41975 |    5825       3       13     4.3 |  0.000 % |
c |       104 |   17335    41664 |    6407     100      478     4.8 |  2.319 % |
c |       254 |   17335    41664 |    7048     250     1427     5.7 |  2.320 % |
c ==============================================================================
c [1mFound solution: 62176[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 |       349 |   17308    41661 |    5769     339     3318     9.8 |  2.320 % |
c |       450 |   17308    41661 |    6345     440     6294    14.3 |  2.661 % |
c |       603 |   17230    41491 |    6980     587     8067    13.7 |  3.043 % |
c |       828 |   17230    41491 |    7678     812    11037    13.6 |  3.043 % |
c ==============================================================================
c [1mFound solution: 61220[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 |      1138 |   17248    41540 |    5749    1122    21213    18.9 |  3.043 % |
c ==============================================================================
c [1mFound solution: 58112[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     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 |      1223 |   17277    41615 |    5759    1207    22714    18.8 |  3.043 % |
c |      1323 |   17277    41615 |    6334    1307    31410    24.0 |  3.061 % |
c |      1474 |   17264    41588 |    6968    1457    32931    22.6 |  3.163 % |
c |      1699 |   17258    41576 |    7665    1679    39469    23.5 |  3.207 % |
c ==============================================================================
c [1mFound solution: 56064[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 |      1990 |   17267    41600 |    5755    1970    45677    23.2 |  3.207 % |
c |      2090 |   17267    41600 |    6330    2070    49716    24.0 |  3.219 % |
c |      2241 |   17267    41600 |    6963    2221    54310    24.5 |  3.219 % |
c |      2467 |   17267    41600 |    7659    2447    62204    25.4 |  3.219 % |
c ==============================================================================
c [1mFound solution: 56056[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 |      2548 |   17279    41629 |    5759    2528    65686    26.0 |  3.219 % |
c |      2648 |   17279    41629 |    6334    2628    67542    25.7 |  3.231 % |
c |      2798 |   17279    41629 |    6968    2778    73242    26.4 |  3.231 % |
c |      3023 |   17279    41629 |    7665    3003    82569    27.5 |  3.231 % |
c |      3360 |   17279    41629 |    8431    3340    95432    28.6 |  3.231 % |
c |      3867 |   17279    41629 |    9274    3847   109637    28.5 |  3.231 % |
c ==============================================================================
c [1mFound solution: 50688[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 |      4601 |   17325    41747 |    5775    4581   124476    27.2 |  3.231 % |
c |      4702 |   17325    41747 |    6352    4682   127134    27.2 |  3.232 % |
c |      4853 |   17325    41747 |    6987    4833   131175    27.1 |  3.232 % |
c |      5078 |   17325    41747 |    7686    5058   136238    26.9 |  3.232 % |
c |      5415 |   17325    41747 |    8455    5395   143722    26.6 |  3.231 % |
c |      5921 |   17325    41747 |    9300    5901   157255    26.6 |  3.232 % |
c |      6680 |   17325    41747 |   10230    6660   176915    26.6 |  3.231 % |
c |      7819 |   17325    41747 |   11253    7799   237338    30.4 |  3.232 % |
c |      9527 |   17181    41422 |   12379    9471   317735    33.5 |  3.974 % |
c ==============================================================================
c [1mFound solution: 50664[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 |      9651 |   17196    41461 |    5732    9595   322524    33.6 |  3.974 % |
c |      9751 |   17196    41461 |    6305    4898   175704    35.9 |  3.984 % |
c |      9901 |   17196    41461 |    6935    5048   178070    35.3 |  3.984 % |
c |     10126 |   17196    41461 |    7629    5273   185889    35.3 |  3.984 % |
c |     10463 |   17196    41461 |    8392    5610   193961    34.6 |  3.984 % |
c |     10969 |   17196    41461 |    9231    6116   226677    37.1 |  3.984 % |
c |     11729 |   17196    41461 |   10154    6876   258490    37.6 |  3.984 % |
c ==============================================================================
c [1mFound solution: 50432[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 |     12169 |   17203    41478 |    5734    7316   272573    37.3 |  3.984 % |
c |     12269 |   17203    41478 |    6307    3758   115307    30.7 |  3.996 % |
c ==============================================================================
c [1mFound solution: 50128[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 |     12344 |   17210    41499 |    5736    3833   118245    30.8 |  3.996 % |
c |     12445 |   17210    41499 |    6309    3934   120046    30.5 |  4.008 % |
c |     12596 |   17210    41499 |    6940    4085   122853    30.1 |  4.008 % |
c |     12821 |   17210    41499 |    7634    4310   129023    29.9 |  4.008 % |
c |     13158 |   17210    41499 |    8398    4647   137045    29.5 |  4.008 % |
c |     13667 |   17210    41499 |    9237    5156   150815    29.3 |  4.008 % |
c ==============================================================================
c [1mFound solution: 50120[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     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 |     13701 |   17217    41519 |    5739    5190   151728    29.2 |  4.008 % |
c |     13804 |   17217    41519 |    6312    5293   154064    29.1 |  4.020 % |
c |     13955 |   17217    41519 |    6944    5444   158866    29.2 |  4.020 % |
c ==============================================================================
c [1mFound solution: 49892[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     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 |     14066 |   17225    41538 |    5741    5555   162103    29.2 |  4.020 % |
c |     14166 |   17225    41538 |    6315    5655   165996    29.4 |  4.033 % |
c |     14316 |   17225    41538 |    6946    5805   169676    29.2 |  4.032 % |
c ==============================================================================
c [1mFound solution: 49408[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 |     14539 |   17229    41547 |    5743    6028   176329    29.3 |  4.032 % |
c |     14640 |   17229    41547 |    6317    3115    60371    19.4 |  4.046 % |
c |     14791 |   17229    41547 |    6949    3266    62832    19.2 |  4.046 % |
c |     15016 |   17229    41547 |    7643    3491    68482    19.6 |  4.046 % |
c |     15353 |   17229    41547 |    8408    3828    80321    21.0 |  4.046 % |
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 |     15803 |   17235    41564 |    5745    4278    98978    23.1 |  4.046 % |
c |     15903 |   17235    41564 |    6319    4378   102000    23.3 |  4.058 % |
c |     16053 |   17235    41564 |    6951    4528   105745    23.4 |  4.058 % |
c |     16278 |   17235    41564 |    7646    4753   110822    23.3 |  4.058 % |
c |     16617 |   17231    41555 |    8411    5090   119913    23.6 |  4.072 % |
c ==============================================================================
c [1mFound solution: 48256[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 |     16992 |   17241    41578 |    5747    5465   133218    24.4 |  4.072 % |
c |     17094 |   17241    41578 |    6321    5567   137069    24.6 |  4.083 % |
c |     17244 |   17241    41578 |    6953    5717   142123    24.9 |  4.083 % |
c |     17469 |   17241    41578 |    7649    5942   147502    24.8 |  4.083 % |
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 |     17626 |   17264    41640 |    5754    6099   151280    24.8 |  4.083 % |
c |     17726 |   17264    41640 |    6329    3150    62168    19.7 |  4.116 % |
c |     17878 |   17264    41640 |    6962    3302    65114    19.7 |  4.116 % |
c |     18103 |   17264    41640 |    7658    3527    68462    19.4 |  4.116 % |
c |     18441 |   17264    41640 |    8424    3865    75094    19.4 |  4.116 % |
c |     18948 |   17264    41640 |    9266    4372    84431    19.3 |  4.116 % |
c |     19708 |   17264    41640 |   10193    5132    96871    18.9 |  4.116 % |
c |     20848 |   17264    41640 |   11212    6272   117459    18.7 |  4.116 % |
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              : 75
c conflicts             : 22223          (923 /sec)
c decisions             : 38634          (1605 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 24.0663 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.73 0.93 0.90 2/54 25353
Raw data (stat): 25353 (runsolver) R 25352 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 541359168 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.001 s]
Raw data (loadavg): 0.77 0.94 0.90 2/54 25353
Raw data (stat): 25353 (minisat+) R 25352 26298 26297 0 -1 0 1264 0 0 0 995 3 0 0 25 0 1 0 541359168 6881280 1240 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1680 1240 603 41 0 1639 0
vsize: 6720
[startup+20.0018 s]
Raw data (loadavg): 0.80 0.94 0.90 2/54 25353
Raw data (stat): 25353 (minisat+) R 25352 26298 26297 0 -1 0 1278 0 0 0 1995 3 0 0 25 0 1 0 541359168 6881280 1254 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1680 1254 603 41 0 1639 0
vsize: 6720
[startup+24.1283 s]
Raw data (loadavg): 0.82 0.94 0.90 1/53 25353
Raw data (stat): 25353 (minisat+) R 25352 26298 26297 0 -1 0 1278 0 0 0 1995 3 0 0 25 0 1 0 541359168 6881280 1254 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1680 1254 603 41 0 1639 0
vsize: 0

Child status: 30
Real time (s): 24.1278
CPU time (s): 24.1133
CPU user time (s): 24.0693
CPU system time (s): 0.043993
CPU usage (%): 99.9402
Max. virtual memory (Kb): 6720
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	44800
#### END VERIFIER DATA ####