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/miplib3/normalized-mps-v2-13-7-noswot.opb
MD5SUM9b64c494b06e0d267a16a958bcbc40bb
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 113777046323200
Number of bits of the biggest number in a constraint 47
Biggest sum of numbers in a constraint 235765682083953
Number of bits of the biggest sum of numbers48
Best result obtained on this benchmarkOPTIMUM FOUND
Best CPU time to get the best result obtained on this benchmark206.622
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 6188

Launcher Data

LAUNCH ON wulflinc2 THE 2005-09-20 04:30:46 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3377 boxname=wulflinc2 idbench=1033 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  9b64c494b06e0d267a16a958bcbc40bb  /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-noswot.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-noswot.opb
IDLAUNCH: 3377
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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.191
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:        912608 kB
Buffers:         13468 kB
Cached:          83992 kB
SwapCached:       1004 kB
Active:          16676 kB
Inactive:        83424 kB
HighTotal:      131008 kB
HighFree:        45528 kB
LowTotal:       903652 kB
LowFree:        867080 kB
SwapTotal:     2097136 kB
SwapFree:      2095552 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5600 kB
Slab:            16408 kB
Committed_AS:    72456 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 04:34:13 (client local time) WITH STATUS 30 IN 206.622 SECONDS
stats: 3377 0 206.622 30

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 235] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
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 ---[ 182]---> BDD-cost:  230
c ---[ 181]---> BDD-cost:  519
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:    6
c ---[ 171]---> BDD-cost:   43
c ---[ 169]---> BDD-cost:    2
c ---[ 167]---> BDD-cost:    2
c ---[ 165]---> BDD-cost:    2
c ---[ 163]---> BDD-cost:    2
c ---[ 160]---> BDD-cost:    2
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:    6
c ---[ 149]---> 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 ---[ 138]---> BDD-cost:  241
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 ---[ 127]---> BDD-cost:    6
c ---[ 125]---> 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 ---[ 114]---> BDD-cost:  102
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:    3
c ---[ 103]---> BDD-cost:   42
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:  592
c ---[  92]---> BDD-cost:    2
c ---[  90]---> BDD-cost:    2
c ---[  89]---> BDD-cost:   19
c ---[  88]---> BDD-cost:  493
c ---[  87]---> Adder-cost: 112   maxlim: 93   bits: 8/7
c ---[  86]---> BDD-cost:  592
c ---[  85]---> BDD-cost:  493
c ---[  84]---> BDD-cost:  592
c ---[  83]---> BDD-cost:  493
c ---[  82]---> BDD-cost:  592
c ---[  81]---> BDD-cost:  493
c ---[  80]---> BDD-cost:  592
c ---[  79]---> BDD-cost:  308
c ---[  78]---> BDD-cost:  322
c ---[  77]---> BDD-cost:  521
c ---[  76]---> BDD-cost:   80
c ---[  75]---> BDD-cost:  322
c ---[  74]---> BDD-cost:  521
c ---[  73]---> BDD-cost:  322
c ---[  72]---> BDD-cost:  521
c ---[  71]---> BDD-cost:  322
c ---[  70]---> BDD-cost:  521
c ---[  69]---> BDD-cost:  322
c ---[  68]---> BDD-cost:  314
c ---[  67]---> BDD-cost:  123
c ---[  66]---> BDD-cost:  526
c ---[  65]---> BDD-cost:   80
c ---[  64]---> BDD-cost:  123
c ---[  63]---> BDD-cost:  526
c ---[  62]---> BDD-cost:  123
c ---[  61]---> BDD-cost:  526
c ---[  60]---> BDD-cost:  123
c ---[  59]---> BDD-cost:  526
c ---[  58]---> BDD-cost:  123
c ---[  57]---> BDD-cost:  352
c ---[  56]---> BDD-cost:  249
c ---[  55]---> BDD-cost:  487
c ---[  54]---> BDD-cost:   80
c ---[  53]---> BDD-cost:  249
c ---[  52]---> BDD-cost:  487
c ---[  51]---> BDD-cost:  249
c ---[  50]---> BDD-cost:  487
c ---[  49]---> BDD-cost:  249
c ---[  48]---> BDD-cost:  487
c ---[  47]---> BDD-cost:  249
c ---[  46]---> BDD-cost:  313
c ---[  45]---> Sorter-cost:  147     Base: 2 2 2
c ---[  44]---> BDD-cost:   75
c ---[  43]---> BDD-cost:   80
c ---[  42]---> BDD-cost:   75
c ---[  41]---> BDD-cost:   75
c ---[  40]---> BDD-cost:   75
c ---[  39]---> BDD-cost:   63
c ---[  37]---> BDD-cost:    5
c ---[  35]---> BDD-cost:    5
c ---[  33]---> BDD-cost:    5
c ---[  32]---> BDD-cost:   62
c ---[  30]---> BDD-cost:    5
c ---[  28]---> BDD-cost:    4
c ---[  27]---> BDD-cost:  272
c ---[  26]---> BDD-cost:  516
c ---[  25]---> BDD-cost:  272
c ---[  24]---> BDD-cost:  516
c ---[  23]---> BDD-cost:  272
c ---[  22]---> BDD-cost:  516
c ---[  20]---> BDD-cost:  272
c ---[  19]---> BDD-cost:  516
c ---[  18]---> BDD-cost:  272
c ---[  17]---> BDD-cost:  516
c ---[  16]---> BDD-cost:  131
c ---[  15]---> BDD-cost:  561
c ---[  14]---> BDD-cost:  131
c ---[  13]---> BDD-cost:  561
c ---[  12]---> BDD-cost:  131
c ---[  11]---> BDD-cost:  561
c ---[  10]---> BDD-cost:    6
c ---[   9]---> BDD-cost:  131
c ---[   8]---> BDD-cost:  561
c ---[   7]---> BDD-cost:  131
c ---[   6]---> BDD-cost:  561
c ---[   5]---> BDD-cost:  230
c ---[   4]---> BDD-cost:  519
c ---[   3]---> BDD-cost:  230
c ---[   2]---> BDD-cost:  519
c ---[   1]---> BDD-cost:  230
c ---[   0]---> BDD-cost:  519
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: -24
c ---[   0]---> Sorter-cost: 1129     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        25 |   75237   209454 |   25079      23      119     5.2 |  0.000 % |
c ==============================================================================
c Found solution: -33
c ---[   0]---> Sorter-cost:    2     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        62 |   75247   209511 |   25082      59      330     5.6 |  0.000 % |
c |       162 |   75247   209511 |   27590     159     2011    12.6 |  6.760 % |
c ==============================================================================
c Found solution: -36
c ---[   0]---> Sorter-cost:    2     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       220 |   75230   209483 |   25076     216     2407    11.1 |  6.760 % |
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 |       228 |   75234   209496 |   25078     224     2460    11.0 |  6.760 % |
c |       331 |   75234   209496 |   27585     327     5604    17.1 |  6.797 % |
c |       481 |   75205   209432 |   30344     476     7867    16.5 |  6.822 % |
c |       708 |   75205   209432 |   33378     703    10221    14.5 |  6.821 % |
c |      1046 |   74969   208902 |   36716    1031    14493    14.1 |  7.062 % |
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 |      1203 |   74974   208922 |   24991    1188    18484    15.6 |  7.062 % |
c |      1305 |   74862   208667 |   27490    1281    19942    15.6 |  7.185 % |
c |      1455 |   74862   208667 |   30239    1431    23275    16.3 |  7.185 % |
c |      1680 |   74862   208667 |   33263    1656    26676    16.1 |  7.185 % |
c |      2017 |   74862   208667 |   36589    1993    31973    16.0 |  7.185 % |
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 |      2308 |   74866   208679 |   24955    2284    41532    18.2 |  7.185 % |
c |      2409 |   74866   208679 |   27450    2385    42739    17.9 |  7.188 % |
c |      2560 |   74866   208679 |   30195    2536    45714    18.0 |  7.188 % |
c |      2786 |   74837   208614 |   33215    2759    51484    18.7 |  7.215 % |
c |      3123 |   74837   208614 |   36536    3096    58481    18.9 |  7.215 % |
c |      3632 |   74798   208528 |   40190    3600    65084    18.1 |  7.271 % |
c |      4392 |   74798   208528 |   44209    4360    81658    18.7 |  7.271 % |
c |      5534 |   74798   208528 |   48630    5502   103793    18.9 |  7.271 % |
c |      7244 |   74798   208528 |   53493    7212   135581    18.8 |  7.271 % |
c |      9808 |   74755   208429 |   58842    9771   178768    18.3 |  7.311 % |
c |     13653 |   74755   208429 |   64726   13616   276866    20.3 |  7.311 % |
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 |     13994 |   74758   208436 |   24919   13957   282781    20.3 |  7.311 % |
c |     14094 |   74758   208436 |   27410   14057   285208    20.3 |  7.314 % |
c |     14244 |   74758   208436 |   30151   14207   288086    20.3 |  7.314 % |
c |     14469 |   74758   208436 |   33167   14432   292689    20.3 |  7.314 % |
c |     14808 |   74758   208436 |   36483   14771   300172    20.3 |  7.314 % |
c |     15314 |   74758   208436 |   40132   15277   311034    20.4 |  7.314 % |
c |     16074 |   74758   208436 |   44145   16037   327414    20.4 |  7.314 % |
c |     17213 |   74758   208436 |   48560   17176   350631    20.4 |  7.314 % |
c |     18921 |   74758   208436 |   53416   18884   386547    20.5 |  7.314 % |
c |     21488 |   74758   208436 |   58757   21451   436479    20.3 |  7.314 % |
c |     25332 |   74758   208436 |   64633   25295   524602    20.7 |  7.314 % |
c |     31099 |   74758   208436 |   71096   31062   652469    21.0 |  7.314 % |
c |     39748 |   74718   208346 |   78206   39699   855543    21.6 |  7.357 % |
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 |     45406 |   74721   208353 |   24907   45357   989059    21.8 |  7.357 % |
c |     45506 |   74721   208353 |   27397   15173   320832    21.1 |  7.360 % |
c |     45657 |   74721   208353 |   30137   15324   323126    21.1 |  7.360 % |
c |     45882 |   74721   208353 |   33151   15549   327530    21.1 |  7.360 % |
c |     46219 |   74721   208353 |   36466   15886   334077    21.0 |  7.360 % |
c |     46725 |   74721   208353 |   40112   16392   342815    20.9 |  7.360 % |
c |     47484 |   74721   208353 |   44124   17151   357204    20.8 |  7.360 % |
c |     48623 |   74721   208353 |   48536   18290   384674    21.0 |  7.360 % |
c |     50331 |   74721   208353 |   53390   19998   414575    20.7 |  7.360 % |
c |     52894 |   74721   208353 |   58729   22561   462369    20.5 |  7.360 % |
c |     56738 |   74721   208353 |   64602   26405   535134    20.3 |  7.360 % |
c |     62504 |   74684   208249 |   71062    8011   142662    17.8 |  7.372 % |
c |     71155 |   74527   207847 |   78168   11113   215104    19.4 |  7.548 % |
c ==============================================================================
c Optimal solution: -41
s OPTIMUM FOUND
v 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 -X11_bit13 -X11_bit14 -X11_bit15 -X11_bit16 -X12_bit0 X12_bit1 -X12_bit2 -X12_bit3 -X12_bit4 -X12_bit5 -X12_bit6 -X12_bit7 -X12_bit8 -X12_bit9 -X12_bit10 -X12_bit11 -X12_bit12 -X12_bit13 -X12_bit14 -X12_bit15 -X12_bit16 X13_bit0 -X13_bit1 -X13_bit2 X13_bit3 -X13_bit4 -X13_bit5 -X13_bit6 -X13_bit7 -X13_bit8 -X13_bit9 -X13_bit10 -X13_bit11 -X13_bit12 -X13_bit13 -X13_bit14 -X13_bit15 -X13_bit16 X14_bit0 -X14_bit1 -X14_bit2 X14_bit3 -X14_bit4 -X14_bit5 -X14_bit6 -X14_bit7 -X14_bit8 -X14_bit9 -X14_bit10 -X14_bit11 -X14_bit12 -X14_bit13 -X14_bit14 -X14_bit15 -X14_bit16 X15_bit0 X15_bit1 X15_bit2 -X15_bit3 -X15_bit4 -X15_bit5 -X15_bit6 -X15_bit7 -X15_bit8 -X15_bit9 -X15_bit10 -X15_bit11 -X15_bit12 -X15_bit13 -X15_bit14 -X15_bit15 -X15_bit16 -X21_bit0 -X21_bit1 -X21_bit2 -X21_bit3 -X21_bit4 -X21_bit5 -X21_bit6 -X21_bit7 -X21_bit8 -X21_bit9 -X21_bit10 -X21_bit11 -X21_bit12 -X21_bit13 -X21_bit14 -X21_bit15 -X21_bit16 X22_bit0 -X22_bit1 X22_bit2 -X22_bit3 -X22_bit4 -X22_bit5 -X22_bit6 -X22_bit7 -X22_bit8 -X22_bit9 -X22_bit10 -X22_bit11 -X22_bit12 -X22_bit13 -X22_bit14 -X22_bit15 -X22_bit16 -X23_bit0 -X23_bit1 -X23_bit2 -X23_bit3 -X23_bit4 -X23_bit5 -X23_bit6 -X23_bit7 -X23_bit8 -X23_bit9 -X23_bit10 -X23_bit11 -X23_bit12 -X23_bit13 -X23_bit14 -X23_bit15 -X23_bit16 -X24_bit0 -X24_bit1 -X24_bit2 -X24_bit3 -X24_bit4 -X24_bit5 -X24_bit6 -X24_bit7 -X24_bit8 -X24_bit9 -X24_bit10 -X24_bit11 -X24_bit12 -X24_bit13 -X24_bit14 -X24_bit15 -X24_bit16 -X25_bit0 -X25_bit1 -X25_bit2 -X25_bit3 -X25_bit4 -X25_bit5 -X25_bit6 -X25_bit7 -X25_bit8 -X25_bit9 -X25_bit10 -X25_bit11 -X25_bit12 -X25_bit13 -X25_bit14 -X25_bit15 -X25_bit16 -X31_bit0 -X31_bit1 -X31_bit2 -X31_bit3 -X31_bit4 -X31_bit5 -X31_bit6 -X31_bit7 -X31_bit8 -X31_bit9 -X31_bit10 -X31_bit11 -X31_bit12 -X31_bit13 -X31_bit14 -X31_bit15 -X31_bit16 -X32_bit0 -X32_bit1 -X32_bit2 -X32_bit3 -X32_bit4 -X32_bit5 -X32_bit6 -X32_bit7 -X32_bit8 -X32_bit9 -X32_bit10 -X32_bit11 -X32_bit12 -X32_bit13 -X32_bit14 -X32_bit15 -X32_bit16 -X33_bit0 -X33_bit1 -X33_bit2 -X33_bit3 -X33_bit4 -X33_bit5 -X33_bit6 -X33_bit7 -X33_bit8 -X33_bit9 -X33_bit10 -X33_bit11 -X33_bit12 -X33_bit13 -X33_bit14 -X33_bit15 -X33_bit16 -X34_bit0 -X34_bit1 -X34_bit2 -X34_bit3 -X34_bit4 -X34_bit5 -X34_bit6 -X34_bit7 -X34_bit8 -X34_bit9 -X34_bit10 -X34_bit11 -X34_bit12 -X34_bit13 -X34_bit14 -X34_bit15 -X34_bit16 -X35_bit0 -X35_bit1 -X35_bit2 -X35_bit3 -X35_bit4 -X35_bit5 -X35_bit6 -X35_bit7 -X35_bit8 -X35_bit9 -X35_bit10 -X35_bit11 -X35_bit12 -X35_bit13 -X35_bit14 -X35_bit15 -X35_bit16 -X41_bit0 -X41_bit1 -X41_bit2 -X41_bit3 -X41_bit4 -X41_bit5 -X41_bit6 -X41_bit7 -X41_bit8 -X41_bit9 -X41_bit10 -X41_bit11 -X41_bit12 -X41_bit13 -X41_bit14 -X41_bit15 -X41_bit16 -X42_bit0 -X42_bit1 -X42_bit2 -X42_bit3 -X42_bit4 -X42_bit5 -X42_bit6 -X42_bit7 -X42_bit8 -X42_bit9 -X42_bit10 -X42_bit11 -X42_bit12 -X42_bit13 -X42_bit14 -X42_bit15 -X42_bit16 -X43_bit0 -X43_bit1 -X43_bit2 -X43_bit3 -X43_bit4 -X43_bit5 -X43_bit6 -X43_bit7 -X43_bit8 -X43_bit9 -X43_bit10 -X43_bit11 -X43_bit12 -X43_bit13 -X43_bit14 -X43_bit15 -X43_bit16 -X44_bit0 -X44_bit1 -X44_bit2 -X44_bit3 -X44_bit4 -X44_bit5 -X44_bit6 -X44_bit7 -X44_bit8 -X44_bit9 -X44_bit10 -X44_bit11 -X44_bit12 -X44_bit13 -X44_bit14 -X44_bit15 -X44_bit16 -X45_bit0 -X45_bit1 -X45_bit2 -X45_bit3 -X45_bit4 -X45_bit5 -X45_bit6 -X45_bit7 -X45_bit8 -X45_bit9 -X45_bit10 -X45_bit11 -X45_bit12 -X45_bit13 -X45_bit14 -X45_bit15 -X45_bit16 -X51_bit0 X51_bit1 -X51_bit2 -X51_bit3 -X51_bit4 -X51_bit5 -X51_bit6 -X51_bit7 -X51_bit8 -X51_bit9 -X51_bit10 -X51_bit11 -X51_bit12 -X51_bit13 -X51_bit14 -X51_bit15 -X51_bit16 -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 -X53_bit0 -X53_bit1 -X53_bit2 -X53_bit3 -X53_bit4 -X53_bit5 -X53_bit6 -X53_bit7 -X53_bit8 -X53_bit9 -X53_bit10 -X53_bit11 -X53_bit12 -X53_bit13 -X53_bit14 -X53_bit15 -X53_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 -X55_bit0 -X55_bit1 -X55_bit2 -X55_bit3 -X55_bit4 -X55_bit5 -X55_bit6 -X55_bit7 -X55_bit8 -X55_bit9 -X55_bit10 -X55_bit11 -X55_bit12 -X55_bit13 -X55_bit14 -X55_bit15 -X55_bit16 -T121_bit0 T122_bit0 -T123_bit0 -T124_bit0 -T125_bit0 -T131_bit0 -T132_bit0 -T133_bit0 -T134_bit0 -T135_bit0 -T141_bit0 -T142_bit0 -T143_bit0 -T144_bit0 -T145_bit0 T151_bit0 -T152_bit0 -T153_bit0 -T154_bit0 -T155_bit0 -T231_bit0 -T232_bit0 T233_bit0 T234_bit0 -T235_bit0 -T241_bit0 -T242_bit0 -T243_bit0 T244_bit0 T245_bit0 T251_bit0 -T252_bit0 -T253_bit0 -T254_bit0 T255_bit0 T341_bit0 T342_bit0 -T343_bit0 -T344_bit0 -T345_bit0 T351_bit0 -T352_bit0 -T353_bit0 T354_bit0 -T355_bit0 T451_bit0 T452_bit0 -T453_bit0 T454_bit0 T455_bit0 W11_bit0 W12_bit0 W13_bit0 W14_bit0 W15_bit0 -W21_bit0 W22_bit0 -W23_bit0 -W24_bit0 -W25_bit0 -W31_bit0 -W32_bit0 -W33_bit0 -W34_bit0 -W35_bit0 -W41_bit0 -W42_bit0 -W43_bit0 -W44_bit0 -W45_bit0 W51_bit0 -W52_bit0 -W53_bit0 -W54_bit0 -W55_bit0 -S24_bit_7 -S24_bit_6 -S24_bit_5 -S24_bit_4 -S24_bit_3 -S24_bit_2 -S24_bit_1 -S24_bit0 -S24_bit1 -S24_bit2 -S24_bit3 -S24_bit4 -S24_bit5 -S24_bit6 -S24_bit7 -S24_bit8 -S24_bit9 -S24_bit10 -S24_bit11 -S24_bit12 -S54_bit_7 -S54_bit_6 -S54_bit_5 -S54_bit_4 -S54_bit_3 -S54_bit_2 -S54_bit_1 -S54_bit0 -S54_bit1 -S54_bit2 -S54_bit3 -S54_bit4 -S54_bit5 -S54_bit6 -S54_bit7 -S54_bit8 -S54_bit9 -S54_bit10 -S54_bit11 -S54_bit12 -S25_bit_7 -S25_bit_6 -S25_bit_5 -S25_bit_4 -S25_bit_3 -S25_bit_2 -S25_bit_1 -S25_bit0 -S25_bit1 -S25_bit2 -S25_bit3 -S25_bit4 -S25_bit5 -S25_bit6 -S25_bit7 -S25_bit8 -S25_bit9 -S25_bit10 -S25_bit11 -S25_bit12 -S55_bit_7 -S55_bit_6 -S55_bit_5 -S55_bit_4 -S55_bit_3 -S55_bit_2 -S55_bit_1 -S55_bit0 -S55_bit1 -S55_bit2 -S55_bit3 -S55_bit4 -S55_bit5 -S55_bit6 -S55_bit7 -S55_bit8 -S55_bit9 -S55_bit10 -S55_bit11 -S55_bit12 -S31_bit_7 -S31_bit_6 -S31_bit_5 -S31_bit_4 -S31_bit_3 -S31_bit_2 -S31_bit_1 -S31_bit0 -S31_bit1 -S31_bit2 -S31_bit3 -S31_bit4 -S31_bit5 -S31_bit6 -S31_bit7 -S31_bit8 -S31_bit9 -S31_bit10 -S31_bit11 -S31_bit12 -S32_bit_7 -S32_bit_6 -S32_bit_5 -S32_bit_4 -S32_bit_3 -S32_bit_2 -S32_bit_1 -S32_bit0 -S32_bit1 -S32_bit2 -S32_bit3 -S32_bit4 -S32_bit5 -S32_bit6 -S32_bit7 -S32_bit8 -S32_bit9 -S32_bit10 -S32_bit11 -S32_bit12 -S33_bit_7 -S33_bit_6 -S33_bit_5 -S33_bit_4 -S33_bit_3 -S33_bit_2 -S33_bit_1 -S33_bit0 -S33_bit1 -S33_bit2 -S33_bit3 -S33_bit4 -S33_bit5 -S33_bit6 -S33_bit7 -S33_bit8 -S33_bit9 -S33_bit10 -S33_bit11 -S33_bit12 -S34_bit_7 -S34_bit_6 -S34_bit_5 -S34_bit_4 -S34_bit_3 -S34_bit_2 -S34_bit_1 -S34_bit0 -S34_bit1 -S34_bit2 -S34_bit3 -S34_bit4 -S34_bit5 -S34_bit6 -S34_bit7 -S34_bit8 -S34_bit9 -S34_bit10 -S34_bit11 -S34_bit12 -S35_bit_7 -S35_bit_6 -S35_bit_5 -S35_bit_4 -S35_bit_3 -S35_bit_2 -S35_bit_1 -S35_bit0 -S35_bit1 -S35_bit2 -S35_bit3 -S35_bit4 -S35_bit5 -S35_bit6 -S35_bit7 -S35_bit8 -S35_bit9 -S35_bit10 -S35_bit11 -S35_bit12 -S41_bit_7 -S41_bit_6 -S41_bit_5 -S41_bit_4 -S41_bit_3 -S41_bit_2 -S41_bit_1 -S41_bit0 -S41_bit1 -S41_bit2 -S41_bit3 -S41_bit4 -S41_bit5 -S41_bit6 -S41_bit7 -S41_bit8 -S41_bit9 -S41_bit10 -S41_bit11 -S41_bit12 -S42_bit_7 -S42_bit_6 -S42_bit_5 -S42_bit_4 -S42_bit_3 -S42_bit_2 -S42_bit_1 -S42_bit0 -S42_bit1 -S42_bit2 -S42_bit3 -S42_bit4 -S42_bit5 -S42_bit6 -S42_bit7 -S42_bit8 -S42_bit9 -S42_bit10 -S42_bit11 -S42_bit12 -S43_bit_7 -S43_bit_6 -S43_bit_5 -S43_bit_4 -S43_bit_3 -S43_bit_2 -S43_bit_1 -S43_bit0 -S43_bit1 -S43_bit2 -S43_bit3 -S43_bit4 -S43_bit5 -S43_bit6 -S43_bit7 -S43_bit8 -S43_bit9 -S43_bit10 -S43_bit11 -S43_bit12 -S44_bit_7 -S44_bit_6 -S44_bit_5 -S44_bit_4 -S44_bit_3 -S44_bit_2 -S44_bit_1 -S44_bit0 -S44_bit1 -S44_bit2 -S44_bit3 -S44_bit4 -S44_bit5 -S44_bit6 -S44_bit7 -S44_bit8 -S44_bit9 -S44_bit10 -S44_bit11 -S44_bit12 -S45_bit_7 -S45_bit_6 -S45_bit_5 -S45_bit_4 -S45_bit_3 -S45_bit_2 -S45_bit_1 -S45_bit0 -S45_bit1 -S45_bit2 -S45_bit3 -S45_bit4 -S45_bit5 -S45_bit6 -S45_bit7 -S45_bit8 -S45_bit9 -S45_bit10 -S45_bit11 -S45_bit12 -S51_bit_7 -S51_bit_6 S51_bit_5 -S51_bit_4 S51_bit_3 -S51_bit_2 -S51_bit_1 S51_bit0 S51_bit1 S51_bit2 S51_bit3 -S51_bit4 -S51_bit5 -S51_bit6 -S51_bit7 -S51_bit8 -S51_bit9 -S51_bit10 -S51_bit11 -S51_bit12 -S52_bit_7 -S52_bit_6 -S52_bit_5 -S52_bit_4 -S52_bit_3 -S52_bit_2 -S52_bit_1 -S52_bit0 -S52_bit1 -S52_bit2 -S52_bit3 -S52_bit4 -S52_bit5 -S52_bit6 -S52_bit7 -S52_bit8 -S52_bit9 -S52_bit10 -S52_bit11 -S52_bit12 -S53_bit_7 -S53_bit_6 -S53_bit_5 -S53_bit_4 -S53_bit_3 -S53_bit_2 -S53_bit_1 -S53_bit0 -S53_bit1 -S53_bit2 -S53_bit3 -S53_bit4 -S53_bit5 -S53_bit6 -S53_bit7 -S53_bit8 -S53_bit9 -S53_bit10 -S53_bit11 -S53_bit12 -V148_bit_7 -V148_bit_6 -V148_bit_5 -V148_bit_4 -V148_bit_3 -V148_bit_2 -V148_bit_1 -V148_bit0 -V148_bit1 -V148_bit2 -V148_bit3 -V148_bit4 -V148_bit5 -V148_bit6 -V148_bit7 -V148_bit8 -V148_bit9 -V148_bit10 -V148_bit11 -V148_bit12 -V150_bit_7 -V150_bit_6 -V150_bit_5 -V150_bit_4 -V150_bit_3 -V150_bit_2 -V150_bit_1 -V150_bit0 -V150_bit1 -V150_bit2 -V150_bit3 -V150_bit4 -V150_bit5 -V150_bit6 -V150_bit7 -V150_bit8 -V150_bit9 -V150_bit10 -V150_bit11 -V150_bit12 -Q246_bit_7 -Q246_bit_6 -Q246_bit_5 -Q246_bit_4 -Q246_bit_3 -Q246_bit_2 -Q246_bit_1 -Q246_bit0 -Q246_bit1 -Q246_bit2 -Q246_bit3 -Q246_bit4 -Q246_bit5 -Q246_bit6 -Q246_bit7 -Q246_bit8 -Q246_bit9 -Q246_bit10 -Q246_bit11 -Q246_bit12 -S11_bit_7 S11_bit_6 -S11_bit_5 S11_bit_4 S11_bit_3 -S11_bit_2 -S11_bit_1 -S11_bit0 -S11_bit1 -S11_bit2 -S11_bit3 -S11_bit4 -S11_bit5 -S11_bit6 -S11_bit7 -S11_bit8 -S11_bit9 -S11_bit10 -S11_bit11 -S11_bit12 -S21_bit_7 -S21_bit_6 -S21_bit_5 -S21_bit_4 -S21_bit_3 -S21_bit_2 -S21_bit_1 -S21_bit0 -S21_bit1 -S21_bit2 -S21_bit3 -S21_bit4 -S21_bit5 -S21_bit6 -S21_bit7 -S21_bit8 -S21_bit9 -S21_bit10 -S21_bit11 -S21_bit12 S12_bit_7 -S12_bit_6 -S12_bit_5 S12_bit_4 -S12_bit_3 -S12_bit_2 -S12_bit_1 -S12_bit0 -S12_bit1 -S12_bit2 -S12_bit3 -S12_bit4 -S12_bit5 -S12_bit6 -S12_bit7 -S12_bit8 -S12_bit9 -S12_bit10 -S12_bit11 -S12_bit12 S22_bit_7 S22_bit_6 -S22_bit_5 -S22_bit_4 -S22_bit_3 -S22_bit_2 -S22_bit_1 S22_bit0 -S22_bit1 S22_bit2 -S22_bit3 -S22_bit4 -S22_bit5 -S22_bit6 -S22_bit7 -S22_bit8 -S22_bit9 -S22_bit10 -S22_bit11 -S22_bit12 -S13_bit_7 -S13_bit_6 S13_bit_5 -S13_bit_4 -S13_bit_3 S13_bit_2 -S13_bit_1 -S13_bit0 -S13_bit1 -S13_bit2 -S13_bit3 -S13_bit4 -S13_bit5 -S13_bit6 -S13_bit7 -S13_bit8 -S13_bit9 -S13_bit10 -S13_bit11 -S13_bit12 -S23_bit_7 -S23_bit_6 -S23_bit_5 -S23_bit_4 -S23_bit_3 -S23_bit_2 -S23_bit_1 -S23_bit0 -S23_bit1 -S23_bit2 -S23_bit3 -S23_bit4 -S23_bit5 -S23_bit6 -S23_bit7 -S23_bit8 -S23_bit9 -S23_bit10 -S23_bit11 -S23_bit12 -S14_bit_7 -S14_bit_6 -S14_bit_5 -S14_bit_4 -S14_bit_3 -S14_bit_2 -S14_bit_1 S14_bit0 -S14_bit1 -S14_bit2 -S14_bit3 -S14_bit4 -S14_bit5 -S14_bit6 -S14_bit7 -S14_bit8 -S14_bit9 -S14_bit10 -S14_bit11 -S14_bit12 S15_bit_7 -S15_bit_6 S15_bit_5 -S15_bit_4 -S15_bit_3 S15_bit_2 S15_bit_1 -S15_bit0 -S15_bit1 -S15_bit2 -S15_bit3 -S15_bit4 -S15_bit5 -S15_bit6 -S15_bit7 -S15_bit8 -S15_bit9 -S15_bit10 -S15_bit11 -S15_bit12
c _______________________________________________________________________________
c 
c restarts              : 52
c conflicts             : 72614          (352 /sec)
c decisions             : 198116         (960 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 206.331 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/8400/stat): 8400 (minisat+_script) R 8399 8400 6872 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1797456774 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/8400/statm): 174 3 169 147 0 27 0
[pid=8400] 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=8401
New process pid=8402
New process pid=8403
execve syscall for /bin/sed executable
One traced child (pid=8402) exited with status: 0
open syscall for file /etc/ld.so.preload
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=8403) exited with status: 0
One traced child (pid=8401) exited with status: 0
New process pid=8404
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-noswot.opb
One traced child (pid=8404) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=8405
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-noswot.opb

[startup+10.0033 s]
Raw data (loadavg): 0.93 0.97 0.92 2/57 8405
Raw data (/proc/8400/stat): 8400 (minisat+_script) S 8399 8400 6872 0 -1 0 314 367 0 0 0 0 1 1 21 0 1 0 1797456774 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8400/statm): 532 234 485 147 0 385 0
[pid=8400] vsize: 2128
Raw data (/proc/8405/stat): 8405 (minisat+_bignum) R 8400 8400 6872 0 -1 0 3048 0 0 0 969 11 0 0 25 0 1 0 1797456781 13303808 2913 4294967295 134512640 135167914 3221224448 3221223120 134562239 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8405/statm): 3248 2913 162 162 0 3086 0
[pid=8405] vsize: 12992
Current children cumulated CPU time (s) 9.82
Current children cumulated vsize (Kb) 15120

[startup+20.004 s]
Raw data (loadavg): 0.94 0.97 0.92 2/57 8405
Raw data (/proc/8400/stat): 8400 (minisat+_script) S 8399 8400 6872 0 -1 0 314 367 0 0 0 0 1 1 21 0 1 0 1797456774 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8400/statm): 532 234 485 147 0 385 0
[pid=8400] vsize: 2128
Raw data (/proc/8405/stat): 8405 (minisat+_bignum) R 8400 8400 6872 0 -1 0 3187 0 0 0 1965 13 0 0 25 0 1 0 1797456781 13897728 3052 4294967295 134512640 135167914 3221224448 3221223152 134562535 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8405/statm): 3393 3052 162 162 0 3231 0
[pid=8405] vsize: 13572
Current children cumulated CPU time (s) 19.8
Current children cumulated vsize (Kb) 15700

[startup+30.0057 s]
Raw data (loadavg): 0.95 0.97 0.92 2/57 8405
Raw data (/proc/8400/stat): 8400 (minisat+_script) S 8399 8400 6872 0 -1 0 314 367 0 0 0 0 1 1 21 0 1 0 1797456774 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8400/statm): 532 234 485 147 0 385 0
[pid=8400] vsize: 2128
Raw data (/proc/8405/stat): 8405 (minisat+_bignum) R 8400 8400 6872 0 -1 0 3344 0 0 0 2960 14 0 0 25 0 1 0 1797456781 14520320 3209 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8405/statm): 3545 3209 162 162 0 3383 0
[pid=8405] vsize: 14180
Current children cumulated CPU time (s) 29.76
Current children cumulated vsize (Kb) 16308

[startup+40.0064 s]
Raw data (loadavg): 0.96 0.97 0.92 2/57 8405
Raw data (/proc/8400/stat): 8400 (minisat+_script) S 8399 8400 6872 0 -1 0 314 367 0 0 0 0 1 1 21 0 1 0 1797456774 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8400/statm): 532 234 485 147 0 385 0
[pid=8400] vsize: 2128
Raw data (/proc/8405/stat): 8405 (minisat+_bignum) R 8400 8400 6872 0 -1 0 3470 0 0 0 3959 14 0 0 25 0 1 0 1797456781 15101952 3335 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8405/statm): 3687 3335 162 162 0 3525 0
[pid=8405] vsize: 14748
Current children cumulated CPU time (s) 39.75
Current children cumulated vsize (Kb) 16876

[startup+50.0081 s]
Raw data (loadavg): 0.96 0.97 0.92 2/57 8405
Raw data (/proc/8400/stat): 8400 (minisat+_script) S 8399 8400 6872 0 -1 0 314 367 0 0 0 0 1 1 21 0 1 0 1797456774 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8400/statm): 532 234 485 147 0 385 0
[pid=8400] vsize: 2128
Raw data (/proc/8405/stat): 8405 (minisat+_bignum) R 8400 8400 6872 0 -1 0 3587 0 0 0 4957 15 0 0 25 0 1 0 1797456781 15581184 3452 4294967295 134512640 135167914 3221224448 3221223152 134562493 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8405/statm): 3804 3452 162 162 0 3642 0
[pid=8405] vsize: 15216
Current children cumulated CPU time (s) 49.74
Current children cumulated vsize (Kb) 17344

[startup+60.0088 s]
Raw data (loadavg): 0.97 0.97 0.92 2/57 8405
Raw data (/proc/8400/stat): 8400 (minisat+_script) S 8399 8400 6872 0 -1 0 314 367 0 0 0 0 1 1 21 0 1 0 1797456774 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8400/statm): 532 234 485 147 0 385 0
[pid=8400] vsize: 2128
Raw data (/proc/8405/stat): 8405 (minisat+_bignum) R 8400 8400 6872 0 -1 0 3707 0 0 0 5955 16 0 0 25 0 1 0 1797456781 16064512 3572 4294967295 134512640 135167914 3221224448 3221223120 134562221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8405/statm): 3922 3572 162 162 0 3760 0
[pid=8405] vsize: 15688
Current children cumulated CPU time (s) 59.73
Current children cumulated vsize (Kb) 17816

[startup+70.0095 s]
Raw data (loadavg): 0.97 0.97 0.92 2/57 8405
Raw data (/proc/8400/stat): 8400 (minisat+_script) S 8399 8400 6872 0 -1 0 314 367 0 0 0 0 1 1 21 0 1 0 1797456774 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8400/statm): 532 234 485 147 0 385 0
[pid=8400] vsize: 2128
Raw data (/proc/8405/stat): 8405 (minisat+_bignum) R 8400 8400 6872 0 -1 0 3824 0 0 0 6953 17 0 0 25 0 1 0 1797456781 16535552 3689 4294967295 134512640 135167914 3221224448 3221223152 134562493 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8405/statm): 4037 3689 162 162 0 3875 0
[pid=8405] vsize: 16148
Current children cumulated CPU time (s) 69.72
Current children cumulated vsize (Kb) 18276

[startup+80.0112 s]
Raw data (loadavg): 0.98 0.97 0.92 2/57 8405
Raw data (/proc/8400/stat): 8400 (minisat+_script) S 8399 8400 6872 0 -1 0 314 367 0 0 0 0 1 1 21 0 1 0 1797456774 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8400/statm): 532 234 485 147 0 385 0
[pid=8400] vsize: 2128
Raw data (/proc/8405/stat): 8405 (minisat+_bignum) R 8400 8400 6872 0 -1 0 3937 0 0 0 7953 18 0 0 25 0 1 0 1797456781 16990208 3802 4294967295 134512640 135167914 3221224448 3221223152 134562502 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8405/statm): 4148 3802 162 162 0 3986 0
[pid=8405] vsize: 16592
Current children cumulated CPU time (s) 79.73
Current children cumulated vsize (Kb) 18720

[startup+90.0119 s]
Raw data (loadavg): 0.98 0.97 0.92 2/57 8405
Raw data (/proc/8400/stat): 8400 (minisat+_script) S 8399 8400 6872 0 -1 0 314 367 0 0 0 0 1 1 21 0 1 0 1797456774 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8400/statm): 532 234 485 147 0 385 0
[pid=8400] vsize: 2128
Raw data (/proc/8405/stat): 8405 (minisat+_bignum) R 8400 8400 6872 0 -1 0 4036 0 0 0 8952 18 0 0 25 0 1 0 1797456781 17518592 3901 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8405/statm): 4277 3901 162 162 0 4115 0
[pid=8405] vsize: 17108
Current children cumulated CPU time (s) 89.72
Current children cumulated vsize (Kb) 19236

[startup+100.013 s]
Raw data (loadavg): 0.98 0.97 0.92 2/57 8405
Raw data (/proc/8400/stat): 8400 (minisat+_script) S 8399 8400 6872 0 -1 0 314 367 0 0 0 0 1 1 21 0 1 0 1797456774 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8400/statm): 532 234 485 147 0 385 0
[pid=8400] vsize: 2128
Raw data (/proc/8405/stat): 8405 (minisat+_bignum) R 8400 8400 6872 0 -1 0 4125 0 0 0 9951 19 0 0 25 0 1 0 1797456781 17899520 3990 4294967295 134512640 135167914 3221224448 3221223152 134562869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8405/statm): 4370 3990 162 162 0 4208 0
[pid=8405] vsize: 17480
Current children cumulated CPU time (s) 99.72
Current children cumulated vsize (Kb) 19608

[startup+110.013 s]
Raw data (loadavg): 0.98 0.97 0.92 2/57 8405
Raw data (/proc/8400/stat): 8400 (minisat+_script) S 8399 8400 6872 0 -1 0 314 367 0 0 0 0 1 1 21 0 1 0 1797456774 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8400/statm): 532 234 485 147 0 385 0
[pid=8400] vsize: 2128
Raw data (/proc/8405/stat): 8405 (minisat+_bignum) R 8400 8400 6872 0 -1 0 4227 0 0 0 10949 20 0 0 25 0 1 0 1797456781 18333696 4092 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8405/statm): 4476 4092 162 162 0 4314 0
[pid=8405] vsize: 17904
Current children cumulated CPU time (s) 109.71
Current children cumulated vsize (Kb) 20032

[startup+120.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 8405
Raw data (/proc/8400/stat): 8400 (minisat+_script) S 8399 8400 6872 0 -1 0 314 367 0 0 0 0 1 1 21 0 1 0 1797456774 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8400/statm): 532 234 485 147 0 385 0
[pid=8400] vsize: 2128
Raw data (/proc/8405/stat): 8405 (minisat+_bignum) R 8400 8400 6872 0 -1 0 4312 0 0 0 11947 21 0 0 25 0 1 0 1797456781 18665472 4177 4294967295 134512640 135167914 3221224448 3221223088 134562079 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8405/statm): 4557 4177 162 162 0 4395 0
[pid=8405] vsize: 18228
Current children cumulated CPU time (s) 119.7
Current children cumulated vsize (Kb) 20356

[startup+130.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 8405
Raw data (/proc/8400/stat): 8400 (minisat+_script) S 8399 8400 6872 0 -1 0 314 367 0 0 0 0 1 1 21 0 1 0 1797456774 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8400/statm): 532 234 485 147 0 385 0
[pid=8400] vsize: 2128
Raw data (/proc/8405/stat): 8405 (minisat+_bignum) R 8400 8400 6872 0 -1 0 4382 0 0 0 12947 21 0 0 25 0 1 0 1797456781 18960384 4247 4294967295 134512640 135167914 3221224448 3221223152 134562874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8405/statm): 4629 4247 162 162 0 4467 0
[pid=8405] vsize: 18516
Current children cumulated CPU time (s) 129.7
Current children cumulated vsize (Kb) 20644

[startup+140.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 8405
Raw data (/proc/8400/stat): 8400 (minisat+_script) S 8399 8400 6872 0 -1 0 314 367 0 0 0 0 1 1 21 0 1 0 1797456774 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8400/statm): 532 234 485 147 0 385 0
[pid=8400] vsize: 2128
Raw data (/proc/8405/stat): 8405 (minisat+_bignum) R 8400 8400 6872 0 -1 0 4383 0 0 0 13947 21 0 0 25 0 1 0 1797456781 18960384 4248 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8405/statm): 4629 4248 162 162 0 4467 0
[pid=8405] vsize: 18516
Current children cumulated CPU time (s) 139.7
Current children cumulated vsize (Kb) 20644

[startup+150.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 8405
Raw data (/proc/8400/stat): 8400 (minisat+_script) S 8399 8400 6872 0 -1 0 314 367 0 0 0 0 1 1 21 0 1 0 1797456774 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8400/statm): 532 234 485 147 0 385 0
[pid=8400] vsize: 2128
Raw data (/proc/8405/stat): 8405 (minisat+_bignum) R 8400 8400 6872 0 -1 0 4384 0 0 0 14947 21 0 0 25 0 1 0 1797456781 18960384 4249 4294967295 134512640 135167914 3221224448 3221223152 134562837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8405/statm): 4629 4249 162 162 0 4467 0
[pid=8405] vsize: 18516
Current children cumulated CPU time (s) 149.7
Current children cumulated vsize (Kb) 20644

[startup+160.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 8405
Raw data (/proc/8400/stat): 8400 (minisat+_script) S 8399 8400 6872 0 -1 0 314 367 0 0 0 0 1 1 21 0 1 0 1797456774 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8400/statm): 532 234 485 147 0 385 0
[pid=8400] vsize: 2128
Raw data (/proc/8405/stat): 8405 (minisat+_bignum) R 8400 8400 6872 0 -1 0 4384 0 0 0 15948 21 0 0 25 0 1 0 1797456781 18960384 4249 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8405/statm): 4629 4249 162 162 0 4467 0
[pid=8405] vsize: 18516
Current children cumulated CPU time (s) 159.71
Current children cumulated vsize (Kb) 20644

[startup+170.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 8405
Raw data (/proc/8400/stat): 8400 (minisat+_script) S 8399 8400 6872 0 -1 0 314 367 0 0 0 0 1 1 21 0 1 0 1797456774 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8400/statm): 532 234 485 147 0 385 0
[pid=8400] vsize: 2128
Raw data (/proc/8405/stat): 8405 (minisat+_bignum) R 8400 8400 6872 0 -1 0 4384 0 0 0 16948 21 0 0 25 0 1 0 1797456781 18960384 4249 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8405/statm): 4629 4249 162 162 0 4467 0
[pid=8405] vsize: 18516
Current children cumulated CPU time (s) 169.71
Current children cumulated vsize (Kb) 20644

[startup+180.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 8405
Raw data (/proc/8400/stat): 8400 (minisat+_script) S 8399 8400 6872 0 -1 0 314 367 0 0 0 0 1 1 21 0 1 0 1797456774 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8400/statm): 532 234 485 147 0 385 0
[pid=8400] vsize: 2128
Raw data (/proc/8405/stat): 8405 (minisat+_bignum) R 8400 8400 6872 0 -1 0 4384 0 0 0 17948 22 0 0 25 0 1 0 1797456781 18960384 4249 4294967295 134512640 135167914 3221224448 3221223136 134556119 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8405/statm): 4629 4249 162 162 0 4467 0
[pid=8405] vsize: 18516
Current children cumulated CPU time (s) 179.72
Current children cumulated vsize (Kb) 20644

[startup+190.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 8405
Raw data (/proc/8400/stat): 8400 (minisat+_script) S 8399 8400 6872 0 -1 0 314 367 0 0 0 0 1 1 21 0 1 0 1797456774 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8400/statm): 532 234 485 147 0 385 0
[pid=8400] vsize: 2128
Raw data (/proc/8405/stat): 8405 (minisat+_bignum) R 8400 8400 6872 0 -1 0 4384 0 0 0 18948 22 0 0 25 0 1 0 1797456781 18960384 4249 4294967295 134512640 135167914 3221224448 3221223152 134562869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8405/statm): 4629 4249 162 162 0 4467 0
[pid=8405] vsize: 18516
Current children cumulated CPU time (s) 189.72
Current children cumulated vsize (Kb) 20644

[startup+200.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 8405
Raw data (/proc/8400/stat): 8400 (minisat+_script) S 8399 8400 6872 0 -1 0 314 367 0 0 0 0 1 1 21 0 1 0 1797456774 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8400/statm): 532 234 485 147 0 385 0
[pid=8400] vsize: 2128
Raw data (/proc/8405/stat): 8405 (minisat+_bignum) R 8400 8400 6872 0 -1 0 4384 0 0 0 19949 22 0 0 25 0 1 0 1797456781 18960384 4249 4294967295 134512640 135167914 3221224448 3221223152 134562535 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8405/statm): 4629 4249 162 162 0 4467 0
[pid=8405] vsize: 18516
Current children cumulated CPU time (s) 199.73
Current children cumulated vsize (Kb) 20644
One traced child (pid=8405) exited with status: 30
One traced child (pid=8400) exited with status: 30
All traced children have exited ! Game is over.

Child status: 30
Real time (s): 206.891
CPU time (s): 206.622
CPU user time (s): 206.36
CPU system time (s): 0.26196
CPU usage (%): 99.8699
Max. virtual memory (cumulated for all children) (Kb): 20644

Verifier Data

Verifier:	OK	-41