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/miplib2003/normalized-mps-v2-13-7-noswot.opb
MD5SUM	64bde1e66dd22efb34c363a61fb9a0ef
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	2275540926464
Number of bits of the biggest number in a constraint	42
Biggest sum of numbers in a constraint	4715313641679
Number of bits of the biggest sum of numbers	43
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	139.56
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 31131

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

Child status: 30
Real time (s): 162.075
CPU time (s): 162.052
CPU user time (s): 161.836
CPU system time (s): 0.215967
CPU usage (%): 99.9861
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	-41
#### END VERIFIER DATA ####