PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-noswot.opb
MD5SUM	7e99578ddcc33d345a5429ff14167339
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-41
Optimality of the best value was proved	NO
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 numbers	48
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	165.164
Number of variables	1060
Total number of constraints	282
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	75
Number of constraints which are nor clauses,nor cardinality constraints	207
Minimum length of a constraint	1
Maximum length of a constraint	425
Trace number 31072

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc19 THE 2005-05-25 22:03:11 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22498 boxname=wulflinc19 idbench=1314 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  7e99578ddcc33d345a5429ff14167339  /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-noswot.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-noswot.opb
IDLAUNCH: 22498
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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.037
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:        882668 kB
Buffers:         30344 kB
Cached:          95724 kB
SwapCached:        752 kB
Active:          20864 kB
Inactive:       107528 kB
HighTotal:      131008 kB
HighFree:        99624 kB
LowTotal:       903652 kB
LowFree:        783044 kB
SwapTotal:     2097892 kB
SwapFree:      2096424 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5404 kB
Slab:            17992 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 22:06:39 (client local time) WITH STATUS 30 IN 207.802 SECONDS
stats: 22498 0 207.802 30
#### END LAUNCHER DATA ####
#### BEGIN 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 [1mFound solution: -24[0m
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 [1mFound solution: -33[0m
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 [1mFound solution: -36[0m
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 [1mFound solution: -37[0m
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 [1mFound solution: -38[0m
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 [1mFound solution: -39[0m
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 [1mFound solution: -40[0m
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 [1mFound solution: -41[0m
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 [1mOptimal solution: -41[0m
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          (350 /sec)
c decisions             : 198116         (955 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 207.559 s
c _______________________________________________________________________________
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.95 0.96 2/54 27514
Raw data (stat): 27514 (runsolver) R 27513 10795 10794 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 842322064 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.87 0.95 0.96 2/55 27519
Raw data (stat): 27514 (minisat+_script) S 27513 10795 10794 0 -1 0 300 369 0 0 0 0 0 1 20 0 1 0 842322064 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+20.0012 s]
Raw data (loadavg): 0.89 0.96 0.96 2/55 27519
Raw data (stat): 27514 (minisat+_script) S 27513 10795 10794 0 -1 0 300 369 0 0 0 0 0 1 20 0 1 0 842322064 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+30.002 s]
Raw data (loadavg): 0.91 0.96 0.96 2/55 27519
Raw data (stat): 27514 (minisat+_script) S 27513 10795 10794 0 -1 0 300 369 0 0 0 0 0 1 20 0 1 0 842322064 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+40.0022 s]
Raw data (loadavg): 0.92 0.96 0.96 2/55 27519
Raw data (stat): 27514 (minisat+_script) S 27513 10795 10794 0 -1 0 300 369 0 0 0 0 0 1 20 0 1 0 842322064 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+50.0026 s]
Raw data (loadavg): 0.93 0.96 0.96 2/55 27519
Raw data (stat): 27514 (minisat+_script) S 27513 10795 10794 0 -1 0 300 369 0 0 0 0 0 1 20 0 1 0 842322064 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+60.0024 s]
Raw data (loadavg): 0.94 0.96 0.96 2/55 27519
Raw data (stat): 27514 (minisat+_script) S 27513 10795 10794 0 -1 0 300 369 0 0 0 0 0 1 20 0 1 0 842322064 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+70.0026 s]
Raw data (loadavg): 0.95 0.96 0.96 2/55 27519
Raw data (stat): 27514 (minisat+_script) S 27513 10795 10794 0 -1 0 300 369 0 0 0 0 0 1 20 0 1 0 842322064 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+80.003 s]
Raw data (loadavg): 0.96 0.96 0.96 2/55 27519
Raw data (stat): 27514 (minisat+_script) S 27513 10795 10794 0 -1 0 300 369 0 0 0 0 0 1 20 0 1 0 842322064 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+90.0028 s]
Raw data (loadavg): 0.96 0.96 0.96 2/55 27519
Raw data (stat): 27514 (minisat+_script) S 27513 10795 10794 0 -1 0 300 369 0 0 0 0 0 1 20 0 1 0 842322064 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+100.004 s]
Raw data (loadavg): 0.97 0.96 0.96 2/55 27519
Raw data (stat): 27514 (minisat+_script) S 27513 10795 10794 0 -1 0 300 369 0 0 0 0 0 1 20 0 1 0 842322064 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+110.004 s]
Raw data (loadavg): 0.97 0.96 0.96 2/55 27519
Raw data (stat): 27514 (minisat+_script) S 27513 10795 10794 0 -1 0 300 369 0 0 0 0 0 1 20 0 1 0 842322064 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+120.004 s]
Raw data (loadavg): 0.98 0.97 0.96 2/55 27519
Raw data (stat): 27514 (minisat+_script) S 27513 10795 10794 0 -1 0 300 369 0 0 0 0 0 1 20 0 1 0 842322064 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+130.004 s]
Raw data (loadavg): 0.98 0.97 0.96 2/55 27519
Raw data (stat): 27514 (minisat+_script) S 27513 10795 10794 0 -1 0 300 369 0 0 0 0 0 1 20 0 1 0 842322064 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+140.004 s]
Raw data (loadavg): 0.98 0.97 0.96 2/55 27521
Raw data (stat): 27514 (minisat+_script) S 27513 10795 10794 0 -1 0 300 369 0 0 0 0 0 1 20 0 1 0 842322064 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+150.005 s]
Raw data (loadavg): 0.98 0.97 0.96 2/55 27521
Raw data (stat): 27514 (minisat+_script) S 27513 10795 10794 0 -1 0 300 369 0 0 0 0 0 1 20 0 1 0 842322064 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 27521
Raw data (stat): 27514 (minisat+_script) S 27513 10795 10794 0 -1 0 300 369 0 0 0 0 0 1 20 0 1 0 842322064 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 27521
Raw data (stat): 27514 (minisat+_script) S 27513 10795 10794 0 -1 0 300 369 0 0 0 0 0 1 20 0 1 0 842322064 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 27521
Raw data (stat): 27514 (minisat+_script) S 27513 10795 10794 0 -1 0 300 369 0 0 0 0 0 1 20 0 1 0 842322064 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 27521
Raw data (stat): 27514 (minisat+_script) S 27513 10795 10794 0 -1 0 300 369 0 0 0 0 0 1 20 0 1 0 842322064 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 27521
Raw data (stat): 27514 (minisat+_script) S 27513 10795 10794 0 -1 0 300 369 0 0 0 0 0 1 20 0 1 0 842322064 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+207.799 s]
Raw data (loadavg): 0.99 0.97 0.96 1/53 27521
Raw data (stat): 27514 (minisat+_script) S 27513 10795 10794 0 -1 0 300 369 0 0 0 0 0 1 20 0 1 0 842322064 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 0

Child status: 30
Real time (s): 207.798
CPU time (s): 207.802
CPU user time (s): 207.584
CPU system time (s): 0.217966
CPU usage (%): 100.002
Max. virtual memory (Kb): 2128
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	-41
#### END VERIFIER DATA ####