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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. 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.
  4. 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

Namemps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-noswot.opb
MD5SUM64bde1e66dd22efb34c363a61fb9a0ef
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function -41
Optimality of the best value was proved YES
Number of terms in the objective function 425
Biggest coefficient in the objective function 65536
Number of bits for the biggest coefficient in the objective function 17
Sum of the numbers in the objective function 3276775
Number of bits of the sum of numbers in the objective function 22
Biggest number in a constraint 2275540926464
Number of bits of the biggest number in a constraint 42
Biggest sum of numbers in a constraint 4715313641679
Number of bits of the biggest sum of numbers43
Best result obtained on this benchmarkOPTIMUM FOUND
Best CPU time to get the best result obtained on this benchmark171.787
Number of variables1060
Total number of constraints282
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)75
Number of constraints which are nor clauses,nor cardinality constraints207
Minimum length of a constraint1
Maximum length of a constraint425

Trace number 6125

Launcher Data

LAUNCH ON wulflinc31 THE 2005-09-20 03:50:07 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3314 boxname=wulflinc31 idbench=970 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  64bde1e66dd22efb34c363a61fb9a0ef  /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-noswot.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-noswot.opb
IDLAUNCH: 3314
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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	: 3
cpu MHz		: 451.153
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        923700 kB
Buffers:          5248 kB
Cached:          77960 kB
SwapCached:       1180 kB
Active:          14012 kB
Inactive:        72000 kB
HighTotal:      131008 kB
HighFree:        50232 kB
LowTotal:       903652 kB
LowFree:        873468 kB
SwapTotal:     2097892 kB
SwapFree:      2096228 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5672 kB
Slab:            19376 kB
Committed_AS:    64376 kB
PageTables:        340 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 03:53:00 (client local time) WITH STATUS 30 IN 171.787 SECONDS
stats: 3314 0 171.787 30

Solver Data

c Parsing PB file...
c Converting 209 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###
c   -- Clauses(.)/Splits(s): .........................
c ---[ 183]---> Adder-cost: 112   maxlim: 93   bits: 8/7
c ---[ 182]---> BDD-cost:    6
c ---[ 181]---> BDD-cost:  592
c ---[ 180]---> BDD-cost:  230
c ---[ 179]---> BDD-cost:  519
c ---[ 177]---> BDD-cost:   49
c ---[ 176]---> BDD-cost:   43
c ---[ 175]---> BDD-cost:   43
c ---[ 174]---> BDD-cost:   43
c ---[ 173]---> BDD-cost:   43
c ---[ 172]---> BDD-cost:   43
c ---[ 169]---> BDD-cost:    2
c ---[ 167]---> BDD-cost:    2
c ---[ 165]---> BDD-cost:    2
c ---[ 163]---> BDD-cost:    2
c ---[ 161]---> BDD-cost:    2
c ---[ 160]---> BDD-cost:    6
c ---[ 159]---> BDD-cost:  169
c ---[ 158]---> BDD-cost:  272
c ---[ 157]---> BDD-cost:  169
c ---[ 156]---> BDD-cost:  272
c ---[ 155]---> BDD-cost:  169
c ---[ 154]---> BDD-cost:  272
c ---[ 153]---> BDD-cost:  169
c ---[ 152]---> BDD-cost:  272
c ---[ 151]---> BDD-cost:  169
c ---[ 150]---> BDD-cost:  272
c ---[ 148]---> BDD-cost:  249
c ---[ 147]---> BDD-cost:  241
c ---[ 146]---> BDD-cost:  249
c ---[ 145]---> BDD-cost:  241
c ---[ 144]---> BDD-cost:  249
c ---[ 143]---> BDD-cost:  241
c ---[ 142]---> BDD-cost:  249
c ---[ 141]---> BDD-cost:  241
c ---[ 140]---> BDD-cost:  249
c ---[ 139]---> BDD-cost:  241
c ---[ 138]---> BDD-cost:    6
c ---[ 137]---> BDD-cost:   19
c ---[ 136]---> BDD-cost:   24
c ---[ 135]---> BDD-cost:   24
c ---[ 134]---> BDD-cost:   24
c ---[ 133]---> BDD-cost:   24
c ---[ 132]---> BDD-cost:   24
c ---[ 129]---> BDD-cost:   12
c ---[ 126]---> BDD-cost:   12
c ---[ 123]---> BDD-cost:    9
c ---[ 121]---> BDD-cost:    4
c ---[ 119]---> BDD-cost:   13
c ---[ 118]---> BDD-cost:  249
c ---[ 117]---> BDD-cost:  102
c ---[ 116]---> BDD-cost:  249
c ---[ 115]---> BDD-cost:  102
c ---[ 114]---> BDD-cost:    3
c ---[ 113]---> BDD-cost:  249
c ---[ 112]---> BDD-cost:  102
c ---[ 111]---> BDD-cost:  249
c ---[ 110]---> BDD-cost:  102
c ---[ 109]---> BDD-cost:  249
c ---[ 108]---> BDD-cost:  102
c ---[ 107]---> BDD-cost:    7
c ---[ 106]---> BDD-cost:   42
c ---[ 105]---> BDD-cost:   42
c ---[ 104]---> BDD-cost:   42
c ---[ 103]---> BDD-cost:  592
c ---[ 102]---> BDD-cost:   42
c ---[ 101]---> BDD-cost:   40
c ---[  99]---> BDD-cost:    2
c ---[  97]---> BDD-cost:    2
c ---[  95]---> BDD-cost:    2
c ---[  93]---> BDD-cost:    2
c ---[  92]---> BDD-cost:  493
c ---[  90]---> BDD-cost:    2
c ---[  89]---> BDD-cost:   19
c ---[  88]---> BDD-cost:  592
c ---[  87]---> BDD-cost:   80
c ---[  86]---> BDD-cost:  493
c ---[  85]---> BDD-cost:  592
c ---[  84]---> BDD-cost:  493
c ---[  83]---> BDD-cost:  592
c ---[  82]---> BDD-cost:  493
c ---[  81]---> BDD-cost:  592
c ---[  80]---> BDD-cost:  308
c ---[  79]---> BDD-cost:  322
c ---[  78]---> BDD-cost:  521
c ---[  77]---> BDD-cost:  322
c ---[  76]---> BDD-cost:   80
c ---[  75]---> BDD-cost:  521
c ---[  74]---> BDD-cost:  322
c ---[  73]---> BDD-cost:  521
c ---[  72]---> BDD-cost:  322
c ---[  71]---> BDD-cost:  521
c ---[  70]---> BDD-cost:  322
c ---[  69]---> BDD-cost:  314
c ---[  68]---> BDD-cost:  123
c ---[  67]---> BDD-cost:  526
c ---[  66]---> BDD-cost:  123
c ---[  65]---> BDD-cost:   80
c ---[  64]---> BDD-cost:  526
c ---[  63]---> BDD-cost:  123
c ---[  62]---> BDD-cost:  526
c ---[  61]---> BDD-cost:  123
c ---[  60]---> BDD-cost:  526
c ---[  59]---> BDD-cost:  123
c ---[  58]---> BDD-cost:  352
c ---[  57]---> BDD-cost:  249
c ---[  56]---> BDD-cost:  487
c ---[  55]---> BDD-cost:  249
c ---[  54]---> BDD-cost:   80
c ---[  53]---> BDD-cost:  487
c ---[  52]---> BDD-cost:  249
c ---[  51]---> BDD-cost:  487
c ---[  50]---> BDD-cost:  249
c ---[  49]---> BDD-cost:  487
c ---[  48]---> BDD-cost:  249
c ---[  47]---> BDD-cost:  313
c ---[  46]---> Sorter-cost:  147     Base: 2 2 2
c ---[  45]---> BDD-cost:   75
c ---[  44]---> BDD-cost:   75
c ---[  43]---> BDD-cost:   62
c ---[  42]---> BDD-cost:   75
c ---[  41]---> BDD-cost:   75
c ---[  40]---> BDD-cost:   63
c ---[  38]---> BDD-cost:    5
c ---[  36]---> BDD-cost:    5
c ---[  34]---> BDD-cost:    5
c ---[  31]---> BDD-cost:    5
c ---[  29]---> BDD-cost:    4
c ---[  28]---> BDD-cost:  272
c ---[  27]---> BDD-cost:  516
c ---[  26]---> BDD-cost:  272
c ---[  25]---> BDD-cost:  516
c ---[  24]---> BDD-cost:  272
c ---[  23]---> BDD-cost:  516
c ---[  22]---> BDD-cost:  272
c ---[  21]---> BDD-cost:    6
c ---[  20]---> BDD-cost:  516
c ---[  19]---> BDD-cost:  272
c ---[  18]---> BDD-cost:  516
c ---[  17]---> BDD-cost:  131
c ---[  16]---> BDD-cost:  561
c ---[  15]---> BDD-cost:  131
c ---[  14]---> BDD-cost:  561
c ---[  13]---> BDD-cost:  131
c ---[  12]---> BDD-cost:  561
c ---[  11]---> BDD-cost:  131
c ---[   9]---> BDD-cost:  561
c ---[   8]---> BDD-cost:  131
c ---[   7]---> BDD-cost:  561
c ---[   6]---> BDD-cost:  230
c ---[   5]---> BDD-cost:  519
c ---[   4]---> BDD-cost:  230
c ---[   3]---> BDD-cost:  519
c ---[   2]---> BDD-cost:  230
c ---[   1]---> BDD-cost:  519
c ---[   0]---> BDD-cost:  157
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   73032   204316 |   24344       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: -27
c ---[   0]---> Sorter-cost: 1127     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        47 |   74304   207317 |   24768      46      375     8.2 |  0.000 % |
c |       147 |   74142   206970 |   27244     132     1006     7.6 |  7.015 % |
c ==============================================================================
c Found solution: -35
c ---[   0]---> Sorter-cost:    1     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       163 |   74161   207024 |   24720     148     1085     7.3 |  7.015 % |
c ==============================================================================
c Found solution: -36
c ---[   0]---> Sorter-cost:    3     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       202 |   74991   208948 |   24997     187     1530     8.2 |  7.015 % |
c |       303 |   74971   208902 |   27496     286     2408     8.4 |  7.058 % |
c |       453 |   74971   208902 |   30246     436     4455    10.2 |  7.058 % |
c |       679 |   74896   208732 |   33271     656    11058    16.9 |  7.148 % |
c ==============================================================================
c Found solution: -37
c ---[   0]---> Sorter-cost:    2     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       780 |   74900   208751 |   24966     757    11842    15.6 |  7.148 % |
c |       880 |   74900   208751 |   27462     857    13016    15.2 |  7.150 % |
c |      1032 |   74850   208639 |   30208    1005    14560    14.5 |  7.197 % |
c |      1257 |   74838   208613 |   33229    1227    18387    15.0 |  7.206 % |
c |      1595 |   74838   208613 |   36552    1565    22849    14.6 |  7.206 % |
c ==============================================================================
c Found solution: -38
c ---[   0]---> Sorter-cost:    3     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2005 |   74843   208632 |   24947    1975    29509    14.9 |  7.206 % |
c |      2106 |   74843   208632 |   27441    2076    31322    15.1 |  7.208 % |
c |      2256 |   74843   208632 |   30185    2226    34066    15.3 |  7.208 % |
c |      2484 |   74839   208623 |   33204    2451    37807    15.4 |  7.211 % |
c |      2821 |   74839   208623 |   36524    2788    43893    15.7 |  7.211 % |
c |      3328 |   74839   208623 |   40177    3295    54429    16.5 |  7.211 % |
c ==============================================================================
c Found solution: -39
c ---[   0]---> Sorter-cost:    1     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3363 |   74843   208635 |   24947    3330    55060    16.5 |  7.211 % |
c |      3463 |   74843   208635 |   27441    3430    57210    16.7 |  7.213 % |
c |      3615 |   74843   208635 |   30185    3582    59329    16.6 |  7.213 % |
c |      3841 |   74843   208635 |   33204    3808    63903    16.8 |  7.213 % |
c |      4181 |   74843   208635 |   36524    4148    71927    17.3 |  7.213 % |
c ==============================================================================
c Found solution: -40
c ---[   0]---> Sorter-cost:    2     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4304 |   74846   208642 |   24948    4271    73538    17.2 |  7.213 % |
c |      4404 |   74846   208642 |   27442    4371    76156    17.4 |  7.216 % |
c |      4554 |   74821   208583 |   30187    4461    77761    17.4 |  7.247 % |
c |      4780 |   74821   208583 |   33205    4687    81987    17.5 |  7.247 % |
c |      5117 |   74821   208583 |   36526    5024    88876    17.7 |  7.247 % |
c |      5623 |   74821   208583 |   40179    5530    97878    17.7 |  7.247 % |
c |      6384 |   74821   208583 |   44196    6291   115143    18.3 |  7.247 % |
c |      7524 |   74821   208583 |   48616    7431   149147    20.1 |  7.247 % |
c |      9232 |   74821   208583 |   53478    9139   200666    22.0 |  7.247 % |
c |     11795 |   74821   208583 |   58826   11702   275025    23.5 |  7.247 % |
c |     15639 |   74821   208583 |   64708   15546   378202    24.3 |  7.247 % |
c ==============================================================================
c Found solution: -41
c ---[   0]---> Sorter-cost:    2     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18762 |   74795   208525 |   24931   18658   451127    24.2 |  7.247 % |
c |     18862 |   74795   208525 |   27424   18758   453439    24.2 |  7.281 % |
c |     19012 |   74795   208525 |   30166   18908   456994    24.2 |  7.280 % |
c |     19237 |   74795   208525 |   33183   19133   461543    24.1 |  7.280 % |
c |     19574 |   74795   208525 |   36501   19470   469022    24.1 |  7.280 % |
c |     20081 |   74795   208525 |   40151   19977   480486    24.1 |  7.280 % |
c |     20841 |   74795   208525 |   44166   20737   497262    24.0 |  7.280 % |
c |     21980 |   74795   208525 |   48583   21876   518994    23.7 |  7.280 % |
c |     23688 |   74795   208525 |   53441   23584   555683    23.6 |  7.280 % |
c |     26250 |   74795   208525 |   58785   26146   604565    23.1 |  7.280 % |
c |     30095 |   74589   208050 |   64664   26199   608830    23.2 |  7.512 % |
c |     35861 |   74484   207769 |   71131   29706   680979    22.9 |  7.599 % |
c |     44510 |   74474   207746 |   78244   38279   854314    22.3 |  7.608 % |
c ==============================================================================
c Optimal solution: -41
s OPTIMUM FOUND
v x52_bit0 x52_bit1 x52_bit2 -x52_bit3 -x52_bit4 -x52_bit5 -x52_bit6 -x52_bit7 -x52_bit8 -x52_bit9 -x52_bit10 -x52_bit11 -x52_bit12 -x52_bit13 -x52_bit14 -x52_bit15 -x52_bit16 x54_bit0 -x54_bit1 -x54_bit2 x54_bit3 -x54_bit4 -x54_bit5 -x54_bit6 -x54_bit7 -x54_bit8 -x54_bit9 -x54_bit10 -x54_bit11 -x54_bit12 -x54_bit13 -x54_bit14 -x54_bit15 -x54_bit16 -x56_bit0 x56_bit1 x56_bit2 -x56_bit3 -x56_bit4 -x56_bit5 -x56_bit6 -x56_bit7 -x56_bit8 -x56_bit9 -x56_bit10 -x56_bit11 -x56_bit12 -x56_bit13 -x56_bit14 -x56_bit15 -x56_bit16 -x58_bit0 -x58_bit1 -x58_bit2 x58_bit3 -x58_bit4 -x58_bit5 -x58_bit6 -x58_bit7 -x58_bit8 -x58_bit9 -x58_bit10 -x58_bit11 -x58_bit12 -x58_bit13 -x58_bit14 -x58_bit15 -x58_bit16 x60_bit0 x60_bit1 -x60_bit2 -x60_bit3 -x60_bit4 -x60_bit5 -x60_bit6 -x60_bit7 -x60_bit8 -x60_bit9 -x60_bit10 -x60_bit11 -x60_bit12 -x60_bit13 -x60_bit14 -x60_bit15 -x60_bit16 -x62_bit0 -x62_bit1 -x62_bit2 -x62_bit3 -x62_bit4 -x62_bit5 -x62_bit6 -x62_bit7 -x62_bit8 -x62_bit9 -x62_bit10 -x62_bit11 -x62_bit12 -x62_bit13 -x62_bit14 -x62_bit15 -x62_bit16 -x64_bit0 -x64_bit1 -x64_bit2 -x64_bit3 -x64_bit4 -x64_bit5 -x64_bit6 -x64_bit7 -x64_bit8 -x64_bit9 -x64_bit10 -x64_bit11 -x64_bit12 -x64_bit13 -x64_bit14 -x64_bit15 -x64_bit16 -x66_bit0 x66_bit1 -x66_bit2 -x66_bit3 -x66_bit4 -x66_bit5 -x66_bit6 -x66_bit7 -x66_bit8 -x66_bit9 -x66_bit10 -x66_bit11 -x66_bit12 -x66_bit13 -x66_bit14 -x66_bit15 -x66_bit16 -x68_bit0 -x68_bit1 -x68_bit2 -x68_bit3 -x68_bit4 -x68_bit5 -x68_bit6 -x68_bit7 -x68_bit8 -x68_bit9 -x68_bit10 -x68_bit11 -x68_bit12 -x68_bit13 -x68_bit14 -x68_bit15 -x68_bit16 x70_bit0 x70_bit1 -x70_bit2 -x70_bit3 -x70_bit4 -x70_bit5 -x70_bit6 -x70_bit7 -x70_bit8 -x70_bit9 -x70_bit10 -x70_bit11 -x70_bit12 -x70_bit13 -x70_bit14 -x70_bit15 -x70_bit16 -x72_bit0 -x72_bit1 -x72_bit2 -x72_bit3 -x72_bit4 -x72_bit5 -x72_bit6 -x72_bit7 -x72_bit8 -x72_bit9 -x72_bit10 -x72_bit11 -x72_bit12 -x72_bit13 -x72_bit14 -x72_bit15 -x72_bit16 -x74_bit0 -x74_bit1 -x74_bit2 -x74_bit3 -x74_bit4 -x74_bit5 -x74_bit6 -x74_bit7 -x74_bit8 -x74_bit9 -x74_bit10 -x74_bit11 -x74_bit12 -x74_bit13 -x74_bit14 -x74_bit15 -x74_bit16 -x76_bit0 -x76_bit1 -x76_bit2 -x76_bit3 -x76_bit4 -x76_bit5 -x76_bit6 -x76_bit7 -x76_bit8 -x76_bit9 -x76_bit10 -x76_bit11 -x76_bit12 -x76_bit13 -x76_bit14 -x76_bit15 -x76_bit16 -x78_bit0 -x78_bit1 -x78_bit2 -x78_bit3 -x78_bit4 -x78_bit5 -x78_bit6 -x78_bit7 -x78_bit8 -x78_bit9 -x78_bit10 -x78_bit11 -x78_bit12 -x78_bit13 -x78_bit14 -x78_bit15 -x78_bit16 -x80_bit0 -x80_bit1 -x80_bit2 -x80_bit3 -x80_bit4 -x80_bit5 -x80_bit6 -x80_bit7 -x80_bit8 -x80_bit9 -x80_bit10 -x80_bit11 -x80_bit12 -x80_bit13 -x80_bit14 -x80_bit15 -x80_bit16 -x82_bit0 -x82_bit1 -x82_bit2 -x82_bit3 -x82_bit4 -x82_bit5 -x82_bit6 -x82_bit7 -x82_bit8 -x82_bit9 -x82_bit10 -x82_bit11 -x82_bit12 -x82_bit13 -x82_bit14 -x82_bit15 -x82_bit16 -x84_bit0 -x84_bit1 -x84_bit2 -x84_bit3 -x84_bit4 -x84_bit5 -x84_bit6 -x84_bit7 -x84_bit8 -x84_bit9 -x84_bit10 -x84_bit11 -x84_bit12 -x84_bit13 -x84_bit14 -x84_bit15 -x84_bit16 -x86_bit0 -x86_bit1 -x86_bit2 -x86_bit3 -x86_bit4 -x86_bit5 -x86_bit6 -x86_bit7 -x86_bit8 -x86_bit9 -x86_bit10 -x86_bit11 -x86_bit12 -x86_bit13 -x86_bit14 -x86_bit15 -x86_bit16 x88_bit0 -x88_bit1 -x88_bit2 -x88_bit3 -x88_bit4 -x88_bit5 -x88_bit6 -x88_bit7 -x88_bit8 -x88_bit9 -x88_bit10 -x88_bit11 -x88_bit12 -x88_bit13 -x88_bit14 -x88_bit15 -x88_bit16 -x90_bit0 -x90_bit1 -x90_bit2 -x90_bit3 -x90_bit4 -x90_bit5 -x90_bit6 -x90_bit7 -x90_bit8 -x90_bit9 -x90_bit10 -x90_bit11 -x90_bit12 -x90_bit13 -x90_bit14 -x90_bit15 -x90_bit16 -x92_bit0 x92_bit1 -x92_bit2 -x92_bit3 -x92_bit4 -x92_bit5 -x92_bit6 -x92_bit7 -x92_bit8 -x92_bit9 -x92_bit10 -x92_bit11 -x92_bit12 -x92_bit13 -x92_bit14 -x92_bit15 -x92_bit16 -x94_bit0 -x94_bit1 -x94_bit2 -x94_bit3 -x94_bit4 -x94_bit5 -x94_bit6 -x94_bit7 -x94_bit8 -x94_bit9 -x94_bit10 -x94_bit11 -x94_bit12 -x94_bit13 -x94_bit14 -x94_bit15 -x94_bit16 -x96_bit0 -x96_bit1 -x96_bit2 -x96_bit3 -x96_bit4 -x96_bit5 -x96_bit6 -x96_bit7 -x96_bit8 -x96_bit9 -x96_bit10 -x96_bit11 -x96_bit12 -x96_bit13 -x96_bit14 -x96_bit15 -x96_bit16 -x98_bit0 -x98_bit1 -x98_bit2 -x98_bit3 -x98_bit4 -x98_bit5 -x98_bit6 -x98_bit7 -x98_bit8 -x98_bit9 -x98_bit10 -x98_bit11 -x98_bit12 -x98_bit13 -x98_bit14 -x98_bit15 -x98_bit16 -x100_bit0 -x100_bit1 -x100_bit2 -x100_bit3 -x100_bit4 -x100_bit5 -x100_bit6 -x100_bit7 -x100_bit8 -x100_bit9 -x100_bit10 -x100_bit11 -x100_bit12 -x100_bit13 -x100_bit14 -x100_bit15 -x100_bit16 -x1_bit0 -x2_bit0 -x3_bit0 -x4_bit0 x5_bit0 -x6_bit0 -x7_bit0 -x8_bit0 -x9_bit0 -x10_bit0 -x11_bit0 -x12_bit0 -x13_bit0 x14_bit0 -x15_bit0 x16_bit0 -x17_bit0 -x18_bit0 -x19_bit0 -x20_bit0 -x21_bit0 x22_bit0 -x23_bit0 -x24_bit0 -x25_bit0 x26_bit0 -x27_bit0 -x28_bit0 x29_bit0 -x30_bit0 x31_bit0 -x32_bit0 -x33_bit0 -x34_bit0 -x35_bit0 -x36_bit0 x37_bit0 x38_bit0 x39_bit0 -x40_bit0 x41_bit0 -x42_bit0 x43_bit0 x44_bit0 x45_bit0 x46_bit0 x47_bit0 x48_bit0 -x49_bit0 x50_bit0 x51_bit0 x53_bit0 x55_bit0 x57_bit0 x59_bit0 -x61_bit0 -x63_bit0 x65_bit0 -x67_bit0 x69_bit0 -x71_bit0 -x73_bit0 -x75_bit0 -x77_bit0 -x79_bit0 -x81_bit0 -x83_bit0 -x85_bit0 x87_bit0 -x89_bit0 x91_bit0 -x93_bit0 -x95_bit0 -x97_bit0 -x99_bit0 -x109_bit_7 -x109_bit_6 -x109_bit_5 -x109_bit_4 -x109_bit_3 -x109_bit_2 -x109_bit_1 -x109_bit0 -x109_bit1 -x109_bit2 -x109_bit3 -x109_bit4 -x109_bit5 -x109_bit6 -x109_bit7 -x109_bit8 -x109_bit9 -x109_bit10 -x109_bit11 -x109_bit12 -x124_bit_7 -x124_bit_6 -x124_bit_5 -x124_bit_4 -x124_bit_3 -x124_bit_2 -x124_bit_1 -x124_bit0 -x124_bit1 -x124_bit2 -x124_bit3 -x124_bit4 -x124_bit5 -x124_bit6 -x124_bit7 -x124_bit8 -x124_bit9 -x124_bit10 -x124_bit11 -x124_bit12 -x110_bit_7 -x110_bit_6 -x110_bit_5 -x110_bit_4 -x110_bit_3 -x110_bit_2 -x110_bit_1 x110_bit0 x110_bit1 x110_bit2 -x110_bit3 -x110_bit4 -x110_bit5 -x110_bit6 -x110_bit7 -x110_bit8 -x110_bit9 -x110_bit10 -x110_bit11 -x110_bit12 -x125_bit_7 -x125_bit_6 -x125_bit_5 -x125_bit_4 -x125_bit_3 -x125_bit_2 -x125_bit_1 -x125_bit0 -x125_bit1 -x125_bit2 -x125_bit3 -x125_bit4 -x125_bit5 -x125_bit6 -x125_bit7 -x125_bit8 -x125_bit9 -x125_bit10 -x125_bit11 -x125_bit12 -x111_bit_7 -x111_bit_6 -x111_bit_5 -x111_bit_4 -x111_bit_3 -x111_bit_2 -x111_bit_1 -x111_bit0 -x111_bit1 -x111_bit2 -x111_bit3 -x111_bit4 -x111_bit5 -x111_bit6 -x111_bit7 -x111_bit8 -x111_bit9 -x111_bit10 -x111_bit11 -x111_bit12 -x112_bit_7 -x112_bit_6 -x112_bit_5 -x112_bit_4 -x112_bit_3 -x112_bit_2 -x112_bit_1 -x112_bit0 -x112_bit1 -x112_bit2 -x112_bit3 -x112_bit4 -x112_bit5 -x112_bit6 -x112_bit7 -x112_bit8 -x112_bit9 -x112_bit10 -x112_bit11 -x112_bit12 -x113_bit_7 -x113_bit_6 -x113_bit_5 -x113_bit_4 -x113_bit_3 -x113_bit_2 -x113_bit_1 -x113_bit0 -x113_bit1 -x113_bit2 -x113_bit3 -x113_bit4 -x113_bit5 -x113_bit6 -x113_bit7 -x113_bit8 -x113_bit9 -x113_bit10 -x113_bit11 -x113_bit12 -x114_bit_7 -x114_bit_6 -x114_bit_5 -x114_bit_4 -x114_bit_3 -x114_bit_2 -x114_bit_1 -x114_bit0 -x114_bit1 -x114_bit2 -x114_bit3 -x114_bit4 -x114_bit5 -x114_bit6 -x114_bit7 -x114_bit8 -x114_bit9 -x114_bit10 -x114_bit11 -x114_bit12 -x115_bit_7 -x115_bit_6 -x115_bit_5 -x115_bit_4 -x115_bit_3 -x115_bit_2 -x115_bit_1 -x115_bit0 -x115_bit1 -x115_bit2 -x115_bit3 -x115_bit4 -x115_bit5 -x115_bit6 -x115_bit7 -x115_bit8 -x115_bit9 -x115_bit10 -x115_bit11 -x115_bit12 -x116_bit_7 -x116_bit_6 -x116_bit_5 -x116_bit_4 -x116_bit_3 -x116_bit_2 -x116_bit_1 -x116_bit0 -x116_bit1 -x116_bit2 -x116_bit3 -x116_bit4 -x116_bit5 -x116_bit6 -x116_bit7 -x116_bit8 -x116_bit9 -x116_bit10 -x116_bit11 -x116_bit12 -x117_bit_7 -x117_bit_6 -x117_bit_5 -x117_bit_4 -x117_bit_3 -x117_bit_2 -x117_bit_1 -x117_bit0 -x117_bit1 -x117_bit2 -x117_bit3 -x117_bit4 -x117_bit5 -x117_bit6 -x117_bit7 -x117_bit8 -x117_bit9 -x117_bit10 -x117_bit11 -x117_bit12 -x118_bit_7 -x118_bit_6 -x118_bit_5 -x118_bit_4 -x118_bit_3 -x118_bit_2 -x118_bit_1 -x118_bit0 -x118_bit1 -x118_bit2 -x118_bit3 -x118_bit4 -x118_bit5 -x118_bit6 -x118_bit7 -x118_bit8 -x118_bit9 -x118_bit10 -x118_bit11 -x118_bit12 -x119_bit_7 -x119_bit_6 x119_bit_5 x119_bit_4 x119_bit_3 x119_bit_2 x119_bit_1 -x119_bit0 -x119_bit1 -x119_bit2 -x119_bit3 x119_bit4 -x119_bit5 -x119_bit6 -x119_bit7 -x119_bit8 -x119_bit9 -x119_bit10 -x119_bit11 -x119_bit12 -x120_bit_7 -x120_bit_6 -x120_bit_5 -x120_bit_4 -x120_bit_3 -x120_bit_2 -x120_bit_1 -x120_bit0 -x120_bit1 -x120_bit2 -x120_bit3 -x120_bit4 -x120_bit5 -x120_bit6 -x120_bit7 -x120_bit8 -x120_bit9 -x120_bit10 -x120_bit11 -x120_bit12 -x121_bit_7 -x121_bit_6 x121_bit_5 -x121_bit_4 -x121_bit_3 -x121_bit_2 -x121_bit_1 x121_bit0 x121_bit1 x121_bit2 x121_bit3 -x121_bit4 -x121_bit5 -x121_bit6 -x121_bit7 -x121_bit8 -x121_bit9 -x121_bit10 -x121_bit11 -x121_bit12 -x122_bit_7 -x122_bit_6 -x122_bit_5 -x122_bit_4 -x122_bit_3 -x122_bit_2 -x122_bit_1 -x122_bit0 -x122_bit1 -x122_bit2 -x122_bit3 -x122_bit4 -x122_bit5 -x122_bit6 -x122_bit7 -x122_bit8 -x122_bit9 -x122_bit10 -x122_bit11 -x122_bit12 -x123_bit_7 -x123_bit_6 -x123_bit_5 -x123_bit_4 -x123_bit_3 -x123_bit_2 -x123_bit_1 -x123_bit0 -x123_bit1 -x123_bit2 -x123_bit3 -x123_bit4 -x123_bit5 -x123_bit6 -x123_bit7 -x123_bit8 -x123_bit9 -x123_bit10 -x123_bit11 -x123_bit12 -x127_bit_7 -x127_bit_6 -x127_bit_5 -x127_bit_4 -x127_bit_3 -x127_bit_2 -x127_bit_1 -x127_bit0 -x127_bit1 -x127_bit2 -x127_bit3 -x127_bit4 -x127_bit5 -x127_bit6 -x127_bit7 -x127_bit8 -x127_bit9 -x127_bit10 -x127_bit11 -x127_bit12 -x126_bit_7 -x126_bit_6 -x126_bit_5 -x126_bit_4 -x126_bit_3 -x126_bit_2 -x126_bit_1 -x126_bit0 -x126_bit1 -x126_bit2 -x126_bit3 -x126_bit4 -x126_bit5 -x126_bit6 -x126_bit7 -x126_bit8 -x126_bit9 -x126_bit10 -x126_bit11 -x126_bit12 -x128_bit_7 -x128_bit_6 -x128_bit_5 -x128_bit_4 -x128_bit_3 -x128_bit_2 -x128_bit_1 -x128_bit0 -x128_bit1 -x128_bit2 -x128_bit3 -x128_bit4 -x128_bit5 -x128_bit6 -x128_bit7 -x128_bit8 -x128_bit9 -x128_bit10 -x128_bit11 -x128_bit12 -x101_bit_7 -x101_bit_6 -x101_bit_5 -x101_bit_4 -x101_bit_3 -x101_bit_2 -x101_bit_1 -x101_bit0 -x101_bit1 -x101_bit2 -x101_bit3 -x101_bit4 -x101_bit5 -x101_bit6 -x101_bit7 -x101_bit8 -x101_bit9 -x101_bit10 -x101_bit11 -x101_bit12 -x106_bit_7 -x106_bit_6 -x106_bit_5 -x106_bit_4 -x106_bit_3 -x106_bit_2 -x106_bit_1 -x106_bit0 -x106_bit1 -x106_bit2 -x106_bit3 -x106_bit4 -x106_bit5 -x106_bit6 -x106_bit7 -x106_bit8 -x106_bit9 -x106_bit10 -x106_bit11 -x106_bit12 -x102_bit_7 -x102_bit_6 -x102_bit_5 -x102_bit_4 -x102_bit_3 x102_bit_2 -x102_bit_1 -x102_bit0 -x102_bit1 -x102_bit2 -x102_bit3 -x102_bit4 -x102_bit5 -x102_bit6 -x102_bit7 -x102_bit8 -x102_bit9 -x102_bit10 -x102_bit11 -x102_bit12 -x107_bit_7 -x107_bit_6 -x107_bit_5 -x107_bit_4 -x107_bit_3 -x107_bit_2 -x107_bit_1 -x107_bit0 -x107_bit1 -x107_bit2 -x107_bit3 -x107_bit4 -x107_bit5 -x107_bit6 -x107_bit7 -x107_bit8 -x107_bit9 -x107_bit10 -x107_bit11 -x107_bit12 x103_bit_7 -x103_bit_6 -x103_bit_5 x103_bit_4 -x103_bit_3 x103_bit_2 x103_bit_1 -x103_bit0 x103_bit1 x103_bit2 -x103_bit3 -x103_bit4 -x103_bit5 -x103_bit6 -x103_bit7 -x103_bit8 -x103_bit9 -x103_bit10 -x103_bit11 -x103_bit12 -x108_bit_7 x108_bit_6 x108_bit_5 -x108_bit_4 x108_bit_3 -x108_bit_2 -x108_bit_1 -x108_bit0 -x108_bit1 -x108_bit2 -x108_bit3 -x108_bit4 -x108_bit5 -x108_bit6 -x108_bit7 -x108_bit8 -x108_bit9 -x108_bit10 -x108_bit11 -x108_bit12 -x104_bit_7 -x104_bit_6 x104_bit_5 -x104_bit_4 -x104_bit_3 -x104_bit_2 -x104_bit_1 -x104_bit0 -x104_bit1 -x104_bit2 -x104_bit3 -x104_bit4 -x104_bit5 -x104_bit6 -x104_bit7 -x104_bit8 -x104_bit9 -x104_bit10 -x104_bit11 -x104_bit12 -x105_bit_7 -x105_bit_6 -x105_bit_5 -x105_bit_4 -x105_bit_3 -x105_bit_2 -x105_bit_1 -x105_bit0 -x105_bit1 -x105_bit2 -x105_bit3 -x105_bit4 -x105_bit5 -x105_bit6 -x105_bit7 -x105_bit8 -x105_bit9 -x105_bit10 -x105_bit11 -x105_bit12
c _______________________________________________________________________________
c 
c restarts              : 48
c conflicts             : 53813          (314 /sec)
c decisions             : 176068         (1027 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 171.445 s
c _______________________________________________________________________________

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/818/stat): 818 (minisat+_script) R 817 818 9102 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855388009 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/818/statm): 174 3 169 147 0 27 0
[pid=818] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libtermcap.so.2
open syscall for file tls/i686/libtermcap.so.2
open syscall for file tls/mmx/libtermcap.so.2
open syscall for file tls/libtermcap.so.2
open syscall for file i686/mmx/libtermcap.so.2
open syscall for file i686/libtermcap.so.2
open syscall for file mmx/libtermcap.so.2
open syscall for file libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/libtermcap.so.2
open syscall for file /etc/ld.so.cache
open syscall for file /lib/libtermcap.so.2
open syscall for file tls/i686/mmx/libdl.so.2
open syscall for file tls/i686/libdl.so.2
open syscall for file tls/mmx/libdl.so.2
open syscall for file tls/libdl.so.2
open syscall for file i686/mmx/libdl.so.2
open syscall for file i686/libdl.so.2
open syscall for file mmx/libdl.so.2
open syscall for file libdl.so.2
open syscall for file /oldhome/oroussel/lib/libdl.so.2
open syscall for file /lib/libdl.so.2
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /lib/tls/libc.so.6
open syscall for file /dev/tty
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
New process pid=819
New process pid=820
New process pid=821
execve syscall for /bin/sed executable
open syscall for file /etc/ld.so.preload
One traced child (pid=820) exited with status: 0
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=821) exited with status: 0
One traced child (pid=819) exited with status: 0
New process pid=824
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-noswot.opb

[startup+10.0047 s]
Raw data (loadavg): 0.89 0.98 0.97 2/58 828
Raw data (/proc/818/stat): 818 (minisat+_script) S 817 818 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855388009 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/818/statm): 531 226 485 147 0 384 0
[pid=818] vsize: 2124
Raw data (/proc/824/stat): 824 (minisat+_64-bit) R 818 818 9102 0 -1 0 2975 0 0 0 968 13 0 0 25 0 1 0 1855388014 13160448 2877 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/824/statm): 3213 2877 145 145 0 3068 0
[pid=824] vsize: 12852
Current children cumulated CPU time (s) 9.81
Current children cumulated vsize (Kb) 14976

[startup+20.0066 s]
Raw data (loadavg): 0.91 0.98 0.97 2/58 830
Raw data (/proc/818/stat): 818 (minisat+_script) S 817 818 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855388009 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/818/statm): 531 226 485 147 0 384 0
[pid=818] vsize: 2124
Raw data (/proc/824/stat): 824 (minisat+_64-bit) R 818 818 9102 0 -1 0 3126 0 0 0 1963 15 0 0 25 0 1 0 1855388014 13795328 3028 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/824/statm): 3368 3028 145 145 0 3223 0
[pid=824] vsize: 13472
Current children cumulated CPU time (s) 19.78
Current children cumulated vsize (Kb) 15596

[startup+30.0086 s]
Raw data (loadavg): 0.92 0.98 0.97 2/58 830
Raw data (/proc/818/stat): 818 (minisat+_script) S 817 818 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855388009 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/818/statm): 531 226 485 147 0 384 0
[pid=818] vsize: 2124
Raw data (/proc/824/stat): 824 (minisat+_64-bit) R 818 818 9102 0 -1 0 3273 0 0 0 2959 18 0 0 25 0 1 0 1855388014 14389248 3175 4294967295 134512640 135094434 3221224432 3221223120 134554793 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/824/statm): 3513 3175 145 145 0 3368 0
[pid=824] vsize: 14052
Current children cumulated CPU time (s) 29.77
Current children cumulated vsize (Kb) 16176

[startup+40.0095 s]
Raw data (loadavg): 0.93 0.98 0.97 2/58 830
Raw data (/proc/818/stat): 818 (minisat+_script) S 817 818 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855388009 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/818/statm): 531 226 485 147 0 384 0
[pid=818] vsize: 2124
Raw data (/proc/824/stat): 824 (minisat+_64-bit) R 818 818 9102 0 -1 0 3402 0 0 0 3955 20 0 0 25 0 1 0 1855388014 14901248 3304 4294967295 134512640 135094434 3221224432 3221223120 134554733 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/824/statm): 3638 3304 145 145 0 3493 0
[pid=824] vsize: 14552
Current children cumulated CPU time (s) 39.75
Current children cumulated vsize (Kb) 16676

[startup+50.0104 s]
Raw data (loadavg): 0.94 0.98 0.97 2/58 830
Raw data (/proc/818/stat): 818 (minisat+_script) S 817 818 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855388009 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/818/statm): 531 226 485 147 0 384 0
[pid=818] vsize: 2124
Raw data (/proc/824/stat): 824 (minisat+_64-bit) R 818 818 9102 0 -1 0 3526 0 0 0 4953 21 0 0 25 0 1 0 1855388014 15478784 3428 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/824/statm): 3779 3428 145 145 0 3634 0
[pid=824] vsize: 15116
Current children cumulated CPU time (s) 49.74
Current children cumulated vsize (Kb) 17240

[startup+60.0113 s]
Raw data (loadavg): 0.95 0.98 0.97 2/58 830
Raw data (/proc/818/stat): 818 (minisat+_script) S 817 818 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855388009 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/818/statm): 531 226 485 147 0 384 0
[pid=818] vsize: 2124
Raw data (/proc/824/stat): 824 (minisat+_64-bit) R 818 818 9102 0 -1 0 3627 0 0 0 5950 22 0 0 25 0 1 0 1855388014 15892480 3529 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/824/statm): 3880 3529 145 145 0 3735 0
[pid=824] vsize: 15520
Current children cumulated CPU time (s) 59.72
Current children cumulated vsize (Kb) 17644

[startup+70.0123 s]
Raw data (loadavg): 0.96 0.98 0.97 2/58 830
Raw data (/proc/818/stat): 818 (minisat+_script) S 817 818 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855388009 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/818/statm): 531 226 485 147 0 384 0
[pid=818] vsize: 2124
Raw data (/proc/824/stat): 824 (minisat+_64-bit) R 818 818 9102 0 -1 0 3711 0 0 0 6949 22 0 0 25 0 1 0 1855388014 16224256 3613 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/824/statm): 3961 3613 145 145 0 3816 0
[pid=824] vsize: 15844
Current children cumulated CPU time (s) 69.71
Current children cumulated vsize (Kb) 17968

[startup+80.0143 s]
Raw data (loadavg): 0.96 0.98 0.97 2/58 832
Raw data (/proc/818/stat): 818 (minisat+_script) S 817 818 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855388009 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/818/statm): 531 226 485 147 0 384 0
[pid=818] vsize: 2124
Raw data (/proc/824/stat): 824 (minisat+_64-bit) R 818 818 9102 0 -1 0 3802 0 0 0 7947 24 0 0 25 0 1 0 1855388014 16592896 3704 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/824/statm): 4051 3704 145 145 0 3906 0
[pid=824] vsize: 16204
Current children cumulated CPU time (s) 79.71
Current children cumulated vsize (Kb) 18328

[startup+90.0152 s]
Raw data (loadavg): 0.97 0.98 0.97 2/58 832
Raw data (/proc/818/stat): 818 (minisat+_script) S 817 818 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855388009 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/818/statm): 531 226 485 147 0 384 0
[pid=818] vsize: 2124
Raw data (/proc/824/stat): 824 (minisat+_64-bit) R 818 818 9102 0 -1 0 3854 0 0 0 8946 25 0 0 25 0 1 0 1855388014 16830464 3756 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/824/statm): 4109 3756 145 145 0 3964 0
[pid=824] vsize: 16436
Current children cumulated CPU time (s) 89.71
Current children cumulated vsize (Kb) 18560

[startup+100.016 s]
Raw data (loadavg): 0.97 0.98 0.97 2/58 832
Raw data (/proc/818/stat): 818 (minisat+_script) S 817 818 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855388009 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/818/statm): 531 226 485 147 0 384 0
[pid=818] vsize: 2124
Raw data (/proc/824/stat): 824 (minisat+_64-bit) R 818 818 9102 0 -1 0 3860 0 0 0 9945 25 0 0 25 0 1 0 1855388014 16855040 3762 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/824/statm): 4115 3762 145 145 0 3970 0
[pid=824] vsize: 16460
Current children cumulated CPU time (s) 99.7
Current children cumulated vsize (Kb) 18584

[startup+110.018 s]
Raw data (loadavg): 0.98 0.98 0.97 2/58 832
Raw data (/proc/818/stat): 818 (minisat+_script) S 817 818 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855388009 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/818/statm): 531 226 485 147 0 384 0
[pid=818] vsize: 2124
Raw data (/proc/824/stat): 824 (minisat+_64-bit) R 818 818 9102 0 -1 0 3908 0 0 0 10944 26 0 0 25 0 1 0 1855388014 17047552 3810 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/824/statm): 4162 3810 145 145 0 4017 0
[pid=824] vsize: 16648
Current children cumulated CPU time (s) 109.7
Current children cumulated vsize (Kb) 18772

[startup+120.019 s]
Raw data (loadavg): 0.98 0.98 0.97 2/58 832
Raw data (/proc/818/stat): 818 (minisat+_script) S 817 818 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855388009 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/818/statm): 531 226 485 147 0 384 0
[pid=818] vsize: 2124
Raw data (/proc/824/stat): 824 (minisat+_64-bit) R 818 818 9102 0 -1 0 3991 0 0 0 11943 26 0 0 25 0 1 0 1855388014 17526784 3893 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/824/statm): 4279 3893 145 145 0 4134 0
[pid=824] vsize: 17116
Current children cumulated CPU time (s) 119.69
Current children cumulated vsize (Kb) 19240

[startup+130.021 s]
Raw data (loadavg): 0.98 0.98 0.97 2/58 832
Raw data (/proc/818/stat): 818 (minisat+_script) S 817 818 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855388009 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/818/statm): 531 226 485 147 0 384 0
[pid=818] vsize: 2124
Raw data (/proc/824/stat): 824 (minisat+_64-bit) R 818 818 9102 0 -1 0 4066 0 0 0 12942 27 0 0 25 0 1 0 1855388014 17833984 3968 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/824/statm): 4354 3968 145 145 0 4209 0
[pid=824] vsize: 17416
Current children cumulated CPU time (s) 129.69
Current children cumulated vsize (Kb) 19540

[startup+140.022 s]
Raw data (loadavg): 0.98 0.98 0.97 3/58 834
Raw data (/proc/818/stat): 818 (minisat+_script) S 817 818 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855388009 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/818/statm): 531 226 485 147 0 384 0
[pid=818] vsize: 2124
Raw data (/proc/824/stat): 824 (minisat+_64-bit) R 818 818 9102 0 -1 0 4139 0 0 0 13940 27 0 0 25 0 1 0 1855388014 18116608 4041 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/824/statm): 4423 4041 145 145 0 4278 0
[pid=824] vsize: 17692
Current children cumulated CPU time (s) 139.67
Current children cumulated vsize (Kb) 19816

[startup+150.023 s]
Raw data (loadavg): 0.99 0.98 0.97 2/58 834
Raw data (/proc/818/stat): 818 (minisat+_script) S 817 818 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855388009 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/818/statm): 531 226 485 147 0 384 0
[pid=818] vsize: 2124
Raw data (/proc/824/stat): 824 (minisat+_64-bit) R 818 818 9102 0 -1 0 4207 0 0 0 14939 28 0 0 25 0 1 0 1855388014 18374656 4109 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/824/statm): 4486 4109 145 145 0 4341 0
[pid=824] vsize: 17944
Current children cumulated CPU time (s) 149.67
Current children cumulated vsize (Kb) 20068

[startup+160.024 s]
Raw data (loadavg): 0.99 0.98 0.97 2/58 834
Raw data (/proc/818/stat): 818 (minisat+_script) S 817 818 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855388009 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/818/statm): 531 226 485 147 0 384 0
[pid=818] vsize: 2124
Raw data (/proc/824/stat): 824 (minisat+_64-bit) R 818 818 9102 0 -1 0 4283 0 0 0 15938 29 0 0 25 0 1 0 1855388014 18669568 4185 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/824/statm): 4558 4185 145 145 0 4413 0
[pid=824] vsize: 18232
Current children cumulated CPU time (s) 159.67
Current children cumulated vsize (Kb) 20356

[startup+170.025 s]
Raw data (loadavg): 0.99 0.98 0.97 2/58 834
Raw data (/proc/818/stat): 818 (minisat+_script) S 817 818 9102 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855388009 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/818/statm): 531 226 485 147 0 384 0
[pid=818] vsize: 2124
Raw data (/proc/824/stat): 824 (minisat+_64-bit) R 818 818 9102 0 -1 0 4350 0 0 0 16937 29 0 0 25 0 1 0 1855388014 18948096 4252 4294967295 134512640 135094434 3221224432 3221223072 134551454 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/824/statm): 4626 4252 145 145 0 4481 0
[pid=824] vsize: 18504
Current children cumulated CPU time (s) 169.66
Current children cumulated vsize (Kb) 20628
One traced child (pid=824) exited with status: 30
One traced child (pid=818) exited with status: 30
All traced children have exited ! Game is over.

Child status: 30
Real time (s): 172.122
CPU time (s): 171.787
CPU user time (s): 171.463
CPU system time (s): 0.32395
CPU usage (%): 99.8054
Max. virtual memory (cumulated for all children) (Kb): 20628

Verifier Data

Verifier:	OK	-41