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/miplib/normalized-mps-v2-13-7-noswot.opb
MD5SUM7e99578ddcc33d345a5429ff14167339
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.701
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 6066

Launcher Data

LAUNCH ON wulflinc22 THE 2005-09-20 03:16:31 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3255 boxname=wulflinc22 idbench=911 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  7e99578ddcc33d345a5429ff14167339  /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-noswot.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-noswot.opb
IDLAUNCH: 3255
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        899948 kB
Buffers:          5152 kB
Cached:         102960 kB
SwapCached:        484 kB
Active:          14904 kB
Inactive:        95680 kB
HighTotal:      131008 kB
HighFree:        24500 kB
LowTotal:       903652 kB
LowFree:        875448 kB
SwapTotal:     2097892 kB
SwapFree:      2096748 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5676 kB
Slab:            18420 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 03:19:58 (client local time) WITH STATUS 30 IN 206.701 SECONDS
stats: 3255 0 206.701 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.316 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/15814/stat): 15814 (minisat+_script) R 15813 15814 21452 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1855227053 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/15814/statm): 174 3 169 147 0 27 0
[pid=15814] 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=15815
New process pid=15816
New process pid=15817
execve syscall for /bin/sed executable
One traced child (pid=15816) 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=15817) exited with status: 0
One traced child (pid=15815) exited with status: 0
New process pid=15818
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-noswot.opb
One traced child (pid=15818) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=15819
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-noswot.opb

[startup+10.0046 s]
Raw data (loadavg): 0.94 0.97 0.91 2/57 15819
Raw data (/proc/15814/stat): 15814 (minisat+_script) S 15813 15814 21452 0 -1 0 314 367 0 0 0 0 0 1 22 0 1 0 1855227053 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15814/statm): 532 234 485 147 0 385 0
[pid=15814] vsize: 2128
Raw data (/proc/15819/stat): 15819 (minisat+_bignum) R 15814 15814 21452 0 -1 0 3048 0 2 0 965 15 0 0 25 0 1 0 1855227060 13312000 2915 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15819/statm): 3250 2915 162 162 0 3088 0
[pid=15819] vsize: 13000
Current children cumulated CPU time (s) 9.81
Current children cumulated vsize (Kb) 15128

[startup+20.0053 s]
Raw data (loadavg): 0.95 0.97 0.91 2/57 15819
Raw data (/proc/15814/stat): 15814 (minisat+_script) S 15813 15814 21452 0 -1 0 314 367 0 0 0 0 0 1 22 0 1 0 1855227053 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15814/statm): 532 234 485 147 0 385 0
[pid=15814] vsize: 2128
Raw data (/proc/15819/stat): 15819 (minisat+_bignum) R 15814 15814 21452 0 -1 0 3188 0 2 0 1962 16 0 0 25 0 1 0 1855227060 13910016 3055 4294967295 134512640 135167914 3221224448 3221223152 134562628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15819/statm): 3396 3055 162 162 0 3234 0
[pid=15819] vsize: 13584
Current children cumulated CPU time (s) 19.79
Current children cumulated vsize (Kb) 15712

[startup+30.006 s]
Raw data (loadavg): 0.95 0.97 0.91 2/57 15819
Raw data (/proc/15814/stat): 15814 (minisat+_script) S 15813 15814 21452 0 -1 0 314 367 0 0 0 0 0 1 22 0 1 0 1855227053 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15814/statm): 532 234 485 147 0 385 0
[pid=15814] vsize: 2128
Raw data (/proc/15819/stat): 15819 (minisat+_bignum) R 15814 15814 21452 0 -1 0 3343 0 2 0 2958 18 0 0 25 0 1 0 1855227060 14528512 3210 4294967295 134512640 135167914 3221224448 3221223152 134562843 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15819/statm): 3547 3210 162 162 0 3385 0
[pid=15819] vsize: 14188
Current children cumulated CPU time (s) 29.77
Current children cumulated vsize (Kb) 16316

[startup+40.0067 s]
Raw data (loadavg): 0.96 0.97 0.91 2/57 15819
Raw data (/proc/15814/stat): 15814 (minisat+_script) S 15813 15814 21452 0 -1 0 314 367 0 0 0 0 0 1 22 0 1 0 1855227053 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15814/statm): 532 234 485 147 0 385 0
[pid=15814] vsize: 2128
Raw data (/proc/15819/stat): 15819 (minisat+_bignum) R 15814 15814 21452 0 -1 0 3468 0 2 0 3956 19 0 0 25 0 1 0 1855227060 15101952 3335 4294967295 134512640 135167914 3221224448 3221223152 134562647 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15819/statm): 3687 3335 162 162 0 3525 0
[pid=15819] vsize: 14748
Current children cumulated CPU time (s) 39.76
Current children cumulated vsize (Kb) 16876

[startup+50.0074 s]
Raw data (loadavg): 0.97 0.97 0.91 2/57 15819
Raw data (/proc/15814/stat): 15814 (minisat+_script) S 15813 15814 21452 0 -1 0 314 367 0 0 0 0 0 1 22 0 1 0 1855227053 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15814/statm): 532 234 485 147 0 385 0
[pid=15814] vsize: 2128
Raw data (/proc/15819/stat): 15819 (minisat+_bignum) R 15814 15814 21452 0 -1 0 3585 0 2 0 4954 20 0 0 25 0 1 0 1855227060 15581184 3452 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15819/statm): 3804 3452 162 162 0 3642 0
[pid=15819] vsize: 15216
Current children cumulated CPU time (s) 49.75
Current children cumulated vsize (Kb) 17344

[startup+60.0091 s]
Raw data (loadavg): 0.97 0.97 0.91 2/57 15819
Raw data (/proc/15814/stat): 15814 (minisat+_script) S 15813 15814 21452 0 -1 0 314 367 0 0 0 0 0 1 22 0 1 0 1855227053 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15814/statm): 532 234 485 147 0 385 0
[pid=15814] vsize: 2128
Raw data (/proc/15819/stat): 15819 (minisat+_bignum) R 15814 15814 21452 0 -1 0 3705 0 2 0 5952 21 0 0 25 0 1 0 1855227060 16064512 3572 4294967295 134512640 135167914 3221224448 3221223120 134562252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15819/statm): 3922 3572 162 162 0 3760 0
[pid=15819] vsize: 15688
Current children cumulated CPU time (s) 59.74
Current children cumulated vsize (Kb) 17816

[startup+70.0099 s]
Raw data (loadavg): 0.97 0.97 0.91 2/57 15819
Raw data (/proc/15814/stat): 15814 (minisat+_script) S 15813 15814 21452 0 -1 0 314 367 0 0 0 0 0 1 22 0 1 0 1855227053 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15814/statm): 532 234 485 147 0 385 0
[pid=15814] vsize: 2128
Raw data (/proc/15819/stat): 15819 (minisat+_bignum) R 15814 15814 21452 0 -1 0 3823 0 2 0 6950 22 0 0 25 0 1 0 1855227060 16539648 3690 4294967295 134512640 135167914 3221224448 3221223120 134562230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15819/statm): 4038 3690 162 162 0 3876 0
[pid=15819] vsize: 16152
Current children cumulated CPU time (s) 69.73
Current children cumulated vsize (Kb) 18280

[startup+80.0106 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 15819
Raw data (/proc/15814/stat): 15814 (minisat+_script) S 15813 15814 21452 0 -1 0 314 367 0 0 0 0 0 1 22 0 1 0 1855227053 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15814/statm): 532 234 485 147 0 385 0
[pid=15814] vsize: 2128
Raw data (/proc/15819/stat): 15819 (minisat+_bignum) R 15814 15814 21452 0 -1 0 3936 0 2 0 7947 23 0 0 25 0 1 0 1855227060 16990208 3803 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15819/statm): 4148 3803 162 162 0 3986 0
[pid=15819] vsize: 16592
Current children cumulated CPU time (s) 79.71
Current children cumulated vsize (Kb) 18720

[startup+90.0123 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 15819
Raw data (/proc/15814/stat): 15814 (minisat+_script) S 15813 15814 21452 0 -1 0 314 367 0 0 0 0 0 1 22 0 1 0 1855227053 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15814/statm): 532 234 485 147 0 385 0
[pid=15814] vsize: 2128
Raw data (/proc/15819/stat): 15819 (minisat+_bignum) R 15814 15814 21452 0 -1 0 4034 0 2 0 8945 24 0 0 25 0 1 0 1855227060 17518592 3901 4294967295 134512640 135167914 3221224448 3221223152 134562815 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15819/statm): 4277 3901 162 162 0 4115 0
[pid=15819] vsize: 17108
Current children cumulated CPU time (s) 89.7
Current children cumulated vsize (Kb) 19236

[startup+100.013 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 15819
Raw data (/proc/15814/stat): 15814 (minisat+_script) S 15813 15814 21452 0 -1 0 314 367 0 0 0 0 0 1 22 0 1 0 1855227053 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15814/statm): 532 234 485 147 0 385 0
[pid=15814] vsize: 2128
Raw data (/proc/15819/stat): 15819 (minisat+_bignum) R 15814 15814 21452 0 -1 0 4123 0 2 0 9944 25 0 0 25 0 1 0 1855227060 17899520 3990 4294967295 134512640 135167914 3221224448 3221223184 134559402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15819/statm): 4370 3990 162 162 0 4208 0
[pid=15819] vsize: 17480
Current children cumulated CPU time (s) 99.7
Current children cumulated vsize (Kb) 19608

[startup+110.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15819
Raw data (/proc/15814/stat): 15814 (minisat+_script) S 15813 15814 21452 0 -1 0 314 367 0 0 0 0 0 1 22 0 1 0 1855227053 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15814/statm): 532 234 485 147 0 385 0
[pid=15814] vsize: 2128
Raw data (/proc/15819/stat): 15819 (minisat+_bignum) R 15814 15814 21452 0 -1 0 4225 0 2 0 10942 26 0 0 25 0 1 0 1855227060 18333696 4092 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15819/statm): 4476 4092 162 162 0 4314 0
[pid=15819] vsize: 17904
Current children cumulated CPU time (s) 109.69
Current children cumulated vsize (Kb) 20032

[startup+120.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15819
Raw data (/proc/15814/stat): 15814 (minisat+_script) S 15813 15814 21452 0 -1 0 314 367 0 0 0 0 0 1 22 0 1 0 1855227053 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15814/statm): 532 234 485 147 0 385 0
[pid=15814] vsize: 2128
Raw data (/proc/15819/stat): 15819 (minisat+_bignum) R 15814 15814 21452 0 -1 0 4309 0 2 0 11940 27 0 0 25 0 1 0 1855227060 18661376 4176 4294967295 134512640 135167914 3221224448 3221223184 134559395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15819/statm): 4556 4176 162 162 0 4394 0
[pid=15819] vsize: 18224
Current children cumulated CPU time (s) 119.68
Current children cumulated vsize (Kb) 20352

[startup+130.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15819
Raw data (/proc/15814/stat): 15814 (minisat+_script) S 15813 15814 21452 0 -1 0 314 367 0 0 0 0 0 1 22 0 1 0 1855227053 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15814/statm): 532 234 485 147 0 385 0
[pid=15814] vsize: 2128
Raw data (/proc/15819/stat): 15819 (minisat+_bignum) R 15814 15814 21452 0 -1 0 4380 0 2 0 12939 28 0 0 25 0 1 0 1855227060 18960384 4247 4294967295 134512640 135167914 3221224448 3221223184 134559387 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15819/statm): 4629 4247 162 162 0 4467 0
[pid=15819] vsize: 18516
Current children cumulated CPU time (s) 129.68
Current children cumulated vsize (Kb) 20644

[startup+140.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15819
Raw data (/proc/15814/stat): 15814 (minisat+_script) S 15813 15814 21452 0 -1 0 314 367 0 0 0 0 0 1 22 0 1 0 1855227053 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15814/statm): 532 234 485 147 0 385 0
[pid=15814] vsize: 2128
Raw data (/proc/15819/stat): 15819 (minisat+_bignum) R 15814 15814 21452 0 -1 0 4381 0 2 0 13938 29 0 0 25 0 1 0 1855227060 18960384 4248 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15819/statm): 4629 4248 162 162 0 4467 0
[pid=15819] vsize: 18516
Current children cumulated CPU time (s) 139.68
Current children cumulated vsize (Kb) 20644

[startup+150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15819
Raw data (/proc/15814/stat): 15814 (minisat+_script) S 15813 15814 21452 0 -1 0 314 367 0 0 0 0 0 1 22 0 1 0 1855227053 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15814/statm): 532 234 485 147 0 385 0
[pid=15814] vsize: 2128
Raw data (/proc/15819/stat): 15819 (minisat+_bignum) R 15814 15814 21452 0 -1 0 4382 0 2 0 14938 29 0 0 25 0 1 0 1855227060 18960384 4249 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15819/statm): 4629 4249 162 162 0 4467 0
[pid=15819] vsize: 18516
Current children cumulated CPU time (s) 149.68
Current children cumulated vsize (Kb) 20644

[startup+160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15819
Raw data (/proc/15814/stat): 15814 (minisat+_script) S 15813 15814 21452 0 -1 0 314 367 0 0 0 0 0 1 22 0 1 0 1855227053 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15814/statm): 532 234 485 147 0 385 0
[pid=15814] vsize: 2128
Raw data (/proc/15819/stat): 15819 (minisat+_bignum) R 15814 15814 21452 0 -1 0 4382 0 2 0 15938 30 0 0 25 0 1 0 1855227060 18960384 4249 4294967295 134512640 135167914 3221224448 3221223152 134562647 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15819/statm): 4629 4249 162 162 0 4467 0
[pid=15819] vsize: 18516
Current children cumulated CPU time (s) 159.69
Current children cumulated vsize (Kb) 20644

[startup+170.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15819
Raw data (/proc/15814/stat): 15814 (minisat+_script) S 15813 15814 21452 0 -1 0 314 367 0 0 0 0 0 1 22 0 1 0 1855227053 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15814/statm): 532 234 485 147 0 385 0
[pid=15814] vsize: 2128
Raw data (/proc/15819/stat): 15819 (minisat+_bignum) R 15814 15814 21452 0 -1 0 4382 0 2 0 16937 30 0 0 25 0 1 0 1855227060 18960384 4249 4294967295 134512640 135167914 3221224448 3221223088 134561560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15819/statm): 4629 4249 162 162 0 4467 0
[pid=15819] vsize: 18516
Current children cumulated CPU time (s) 169.68
Current children cumulated vsize (Kb) 20644

[startup+180.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15819
Raw data (/proc/15814/stat): 15814 (minisat+_script) S 15813 15814 21452 0 -1 0 314 367 0 0 0 0 0 1 22 0 1 0 1855227053 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15814/statm): 532 234 485 147 0 385 0
[pid=15814] vsize: 2128
Raw data (/proc/15819/stat): 15819 (minisat+_bignum) R 15814 15814 21452 0 -1 0 4382 0 2 0 17937 31 0 0 25 0 1 0 1855227060 18960384 4249 4294967295 134512640 135167914 3221224448 3221223136 134556090 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15819/statm): 4629 4249 162 162 0 4467 0
[pid=15819] vsize: 18516
Current children cumulated CPU time (s) 179.69
Current children cumulated vsize (Kb) 20644

[startup+190.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15819
Raw data (/proc/15814/stat): 15814 (minisat+_script) S 15813 15814 21452 0 -1 0 314 367 0 0 0 0 0 1 22 0 1 0 1855227053 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15814/statm): 532 234 485 147 0 385 0
[pid=15814] vsize: 2128
Raw data (/proc/15819/stat): 15819 (minisat+_bignum) R 15814 15814 21452 0 -1 0 4382 0 2 0 18936 31 0 0 25 0 1 0 1855227060 18960384 4249 4294967295 134512640 135167914 3221224448 3221223152 134562593 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15819/statm): 4629 4249 162 162 0 4467 0
[pid=15819] vsize: 18516
Current children cumulated CPU time (s) 189.68
Current children cumulated vsize (Kb) 20644

[startup+200.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 15819
Raw data (/proc/15814/stat): 15814 (minisat+_script) S 15813 15814 21452 0 -1 0 314 367 0 0 0 0 0 1 22 0 1 0 1855227053 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15814/statm): 532 234 485 147 0 385 0
[pid=15814] vsize: 2128
Raw data (/proc/15819/stat): 15819 (minisat+_bignum) R 15814 15814 21452 0 -1 0 4382 0 2 0 19936 32 0 0 25 0 1 0 1855227060 18960384 4249 4294967295 134512640 135167914 3221224448 3221223184 134559395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15819/statm): 4629 4249 162 162 0 4467 0
[pid=15819] vsize: 18516
Current children cumulated CPU time (s) 199.69
Current children cumulated vsize (Kb) 20644
One traced child (pid=15819) exited with status: 30
One traced child (pid=15814) exited with status: 30
All traced children have exited ! Game is over.

Child status: 30
Real time (s): 207.01
CPU time (s): 206.701
CPU user time (s): 206.342
CPU system time (s): 0.358945
CPU usage (%): 99.8506
Max. virtual memory (cumulated for all children) (Kb): 20644

Verifier Data

Verifier:	OK	-41