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-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-noswot.opb
MD5SUM	b239ca7d2095d517ad5daa2331de8426
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	1048576000000000
Number of bits of the biggest number in a constraint	50
Biggest sum of numbers in a constraint	5104598755679562
Number of bits of the biggest sum of numbers	53
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	143.293
Number of variables	1340
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 31857

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc4 THE 2005-05-27 06:44:16 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=23286 boxname=wulflinc4 idbench=930 idsolver=16 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b239ca7d2095d517ad5daa2331de8426  /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-noswot.opb
REAL COMMAND:  minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-noswot.opb
IDLAUNCH: 23286
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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	: 2
cpu MHz		: 451.169
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:        816132 kB
Buffers:         33588 kB
Cached:         164200 kB
SwapCached:        500 kB
Active:          52700 kB
Inactive:       147460 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        815880 kB
SwapTotal:     2097136 kB
SwapFree:      2096004 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5788 kB
Slab:            12516 kB
Committed_AS:    71796 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-27 06:47:15 (client local time) WITH STATUS 30 IN 179.166 SECONDS
stats: 23286 0 179.166 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:  269
c ---[ 181]---> BDD-cost:  708
c ---[ 180]---> BDD-cost:  269
c ---[ 179]---> BDD-cost:  708
c ---[ 177]---> BDD-cost:   49
c ---[ 176]---> BDD-cost:   56
c ---[ 175]---> BDD-cost:   56
c ---[ 174]---> BDD-cost:   56
c ---[ 173]---> BDD-cost:   56
c ---[ 172]---> BDD-cost:    6
c ---[ 171]---> BDD-cost:   56
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:  217
c ---[ 158]---> BDD-cost:  342
c ---[ 157]---> BDD-cost:  217
c ---[ 156]---> BDD-cost:  342
c ---[ 155]---> BDD-cost:  217
c ---[ 154]---> BDD-cost:  342
c ---[ 153]---> BDD-cost:  217
c ---[ 152]---> BDD-cost:  342
c ---[ 151]---> BDD-cost:  217
c ---[ 150]---> BDD-cost:    6
c ---[ 149]---> BDD-cost:  342
c ---[ 148]---> BDD-cost:  297
c ---[ 147]---> BDD-cost:  301
c ---[ 146]---> BDD-cost:  297
c ---[ 145]---> BDD-cost:  301
c ---[ 144]---> BDD-cost:  297
c ---[ 143]---> BDD-cost:  301
c ---[ 142]---> BDD-cost:  297
c ---[ 141]---> BDD-cost:  301
c ---[ 140]---> BDD-cost:  297
c ---[ 138]---> BDD-cost:  301
c ---[ 137]---> BDD-cost:   19
c ---[ 136]---> BDD-cost:   31
c ---[ 135]---> BDD-cost:   31
c ---[ 134]---> BDD-cost:   31
c ---[ 133]---> BDD-cost:   31
c ---[ 132]---> BDD-cost:   31
c ---[ 129]---> BDD-cost:   15
c ---[ 127]---> BDD-cost:    6
c ---[ 125]---> BDD-cost:   15
c ---[ 123]---> BDD-cost:   12
c ---[ 121]---> BDD-cost:    4
c ---[ 119]---> BDD-cost:   16
c ---[ 118]---> BDD-cost:  297
c ---[ 117]---> BDD-cost:  102
c ---[ 116]---> BDD-cost:  297
c ---[ 114]---> BDD-cost:  102
c ---[ 113]---> BDD-cost:  297
c ---[ 112]---> BDD-cost:  102
c ---[ 111]---> BDD-cost:  297
c ---[ 110]---> BDD-cost:  102
c ---[ 109]---> BDD-cost:  297
c ---[ 108]---> BDD-cost:  102
c ---[ 107]---> BDD-cost:    7
c ---[ 106]---> BDD-cost:   51
c ---[ 105]---> BDD-cost:   51
c ---[ 104]---> BDD-cost:    3
c ---[ 103]---> BDD-cost:   51
c ---[ 102]---> BDD-cost:   51
c ---[ 101]---> BDD-cost:   49
c ---[  99]---> BDD-cost:    2
c ---[  97]---> BDD-cost:    2
c ---[  95]---> BDD-cost:    2
c ---[  93]---> BDD-cost:  820
c ---[  92]---> BDD-cost:    2
c ---[  90]---> BDD-cost:    2
c ---[  89]---> BDD-cost:   19
c ---[  88]---> BDD-cost:  561
c ---[  87]---> BDD-cost:  808
c ---[  86]---> BDD-cost:  820
c ---[  85]---> BDD-cost:  561
c ---[  84]---> BDD-cost:  820
c ---[  83]---> BDD-cost:  561
c ---[  82]---> BDD-cost:  820
c ---[  81]---> BDD-cost:  561
c ---[  80]---> BDD-cost:  820
c ---[  79]---> BDD-cost:  308
c ---[  78]---> BDD-cost:  415
c ---[  77]---> BDD-cost:  598
c ---[  76]---> BDD-cost:   89
c ---[  75]---> BDD-cost:  415
c ---[  74]---> BDD-cost:  598
c ---[  73]---> BDD-cost:  415
c ---[  72]---> BDD-cost:  598
c ---[  71]---> BDD-cost:  415
c ---[  70]---> BDD-cost:  598
c ---[  69]---> BDD-cost:  415
c ---[  68]---> BDD-cost:  329
c ---[  67]---> BDD-cost:  144
c ---[  66]---> BDD-cost:  621
c ---[  65]---> BDD-cost:   89
c ---[  64]---> BDD-cost:  144
c ---[  63]---> BDD-cost:  621
c ---[  62]---> BDD-cost:  144
c ---[  61]---> BDD-cost:  621
c ---[  60]---> BDD-cost:  144
c ---[  59]---> BDD-cost:  621
c ---[  58]---> BDD-cost:  144
c ---[  57]---> BDD-cost:  379
c ---[  56]---> BDD-cost:  297
c ---[  55]---> BDD-cost:  555
c ---[  54]---> BDD-cost:   89
c ---[  53]---> BDD-cost:  297
c ---[  52]---> BDD-cost:  555
c ---[  51]---> BDD-cost:  297
c ---[  50]---> BDD-cost:  555
c ---[  49]---> BDD-cost:  297
c ---[  48]---> BDD-cost:  555
c ---[  47]---> BDD-cost:  297
c ---[  46]---> BDD-cost:  313
c ---[  45]---> BDD-cost:   66
c ---[  44]---> BDD-cost:   94
c ---[  43]---> BDD-cost:   89
c ---[  42]---> BDD-cost:   94
c ---[  41]---> BDD-cost:   94
c ---[  40]---> BDD-cost:   94
c ---[  39]---> BDD-cost:   78
c ---[  37]---> BDD-cost:    5
c ---[  35]---> BDD-cost:    5
c ---[  33]---> BDD-cost:    5
c ---[  32]---> BDD-cost:   71
c ---[  30]---> BDD-cost:    5
c ---[  28]---> BDD-cost:    4
c ---[  27]---> BDD-cost:  320
c ---[  26]---> BDD-cost:  738
c ---[  25]---> BDD-cost:  320
c ---[  24]---> BDD-cost:  738
c ---[  23]---> BDD-cost:  320
c ---[  22]---> BDD-cost:  738
c ---[  20]---> BDD-cost:  320
c ---[  19]---> BDD-cost:  738
c ---[  18]---> BDD-cost:  320
c ---[  17]---> BDD-cost:  738
c ---[  16]---> BDD-cost:  152
c ---[  15]---> BDD-cost:  773
c ---[  14]---> BDD-cost:  152
c ---[  13]---> BDD-cost:  773
c ---[  12]---> BDD-cost:  152
c ---[  11]---> BDD-cost:  773
c ---[  10]---> BDD-cost:    6
c ---[   9]---> BDD-cost:  152
c ---[   8]---> BDD-cost:  773
c ---[   7]---> BDD-cost:  152
c ---[   6]---> BDD-cost:  773
c ---[   5]---> BDD-cost:  269
c ---[   4]---> BDD-cost:  708
c ---[   3]---> BDD-cost:  269
c ---[   2]---> BDD-cost:  708
c ---[   1]---> BDD-cost:  269
c ---[   0]---> BDD-cost:  708
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   91757   256405 |   30585       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -19[0m
c ---[   0]---> Sorter-cost: 1155     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        32 |   93024   259385 |   31008      30      162     5.4 |  0.000 % |
c ==============================================================================
c [1mFound solution: -32[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 |        46 |   94071   261847 |   31357      44      246     5.6 |  0.000 % |
c ==============================================================================
c [1mFound solution: -34[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 |        63 |   94077   261886 |   31359      61      355     5.8 |  0.000 % |
c |       163 |   94048   261822 |   34494     160     1328     8.3 |  7.029 % |
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 |       205 |   93913   261526 |   31304     194     1598     8.2 |  7.029 % |
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 |       247 |   93917   261539 |   31305     236     2086     8.8 |  7.029 % |
c |       348 |   93710   261073 |   34435     307     2493     8.1 |  7.322 % |
c |       498 |   93710   261073 |   37879     457     4560    10.0 |  7.322 % |
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 |       722 |   93713   261080 |   31237     681     7395    10.9 |  7.322 % |
c |       824 |   93713   261080 |   34360     783     8829    11.3 |  7.324 % |
c |       975 |   93713   261080 |   37796     934    10328    11.1 |  7.324 % |
c ==============================================================================
c [1mFound solution: -38[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 |      1043 |   93718   261091 |   31239    1002    11546    11.5 |  7.324 % |
c |      1143 |   93706   261067 |   34362    1096    12317    11.2 |  7.341 % |
c |      1293 |   93706   261067 |   37799    1246    14983    12.0 |  7.341 % |
c |      1518 |   93706   261067 |   41579    1471    19922    13.5 |  7.341 % |
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 |      1612 |   93710   261079 |   31236    1565    22040    14.1 |  7.341 % |
c |      1712 |   93710   261079 |   34359    1665    23109    13.9 |  7.343 % |
c |      1862 |   93710   261079 |   37795    1815    25516    14.1 |  7.343 % |
c |      2087 |   93710   261079 |   41575    2040    30354    14.9 |  7.343 % |
c |      2424 |   93710   261079 |   45732    2377    35349    14.9 |  7.343 % |
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 |      2782 |   93713   261086 |   31237    2735    43724    16.0 |  7.343 % |
c |      2882 |   93713   261086 |   34360    2835    45338    16.0 |  7.345 % |
c |      3034 |   93713   261086 |   37796    2987    50357    16.9 |  7.345 % |
c |      3259 |   93671   260989 |   41576    3210    55125    17.2 |  7.389 % |
c |      3597 |   93671   260989 |   45734    3548    63031    17.8 |  7.389 % |
c |      4105 |   93671   260989 |   50307    4056    77555    19.1 |  7.389 % |
c |      4864 |   93671   260989 |   55338    4815    94105    19.5 |  7.389 % |
c |      6005 |   93671   260989 |   60872    5956   124682    20.9 |  7.389 % |
c |      7713 |   93671   260989 |   66959    7664   174125    22.7 |  7.389 % |
c |     10275 |   93671   260989 |   73655   10226   234843    23.0 |  7.389 % |
c |     14119 |   93671   260989 |   81020   14070   315259    22.4 |  7.389 % |
c |     19885 |   93528   260663 |   89122   19792   443514    22.4 |  7.513 % |
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 |     22241 |   93531   260670 |   31177   22148   492015    22.2 |  7.513 % |
c |     22341 |   93531   260670 |   34294   22248   493566    22.2 |  7.516 % |
c |     22493 |   93531   260670 |   37724   22400   496918    22.2 |  7.516 % |
c |     22719 |   93531   260670 |   41496   22626   501251    22.2 |  7.516 % |
c |     23056 |   93531   260670 |   45646   22963   508412    22.1 |  7.516 % |
c |     23562 |   93518   260641 |   50210   23467   518317    22.1 |  7.528 % |
c |     24321 |   93518   260641 |   55231   24226   532215    22.0 |  7.528 % |
c |     25460 |   93518   260641 |   60755   25365   552021    21.8 |  7.528 % |
c |     27168 |   93518   260641 |   66830   27073   587607    21.7 |  7.528 % |
c |     29731 |   93518   260641 |   73513   29636   638150    21.5 |  7.528 % |
c |     33575 |   93496   260594 |   80865   33479   718669    21.5 |  7.558 % |
c |     39341 |   93398   260330 |   88951   29184   639779    21.9 |  7.602 % |
c |     47991 |   93091   259561 |   97846   22177   451467    20.4 |  7.858 % |
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_10 -S24_bit_9 -S24_bit_8 -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 -S24_bit13 -S24_bit14 -S24_bit15 -S24_bit16 -S24_bit17 -S24_bit18 -S24_bit19 -S54_bit_10 -S54_bit_9 -S54_bit_8 -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 -S54_bit13 -S54_bit14 -S54_bit15 -S54_bit16 -S54_bit17 -S54_bit18 -S54_bit19 -S25_bit_10 -S25_bit_9 -S25_bit_8 -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 -S25_bit13 -S25_bit14 -S25_bit15 -S25_bit16 -S25_bit17 -S25_bit18 -S25_bit19 -S55_bit_10 -S55_bit_9 -S55_bit_8 -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 -S55_bit13 -S55_bit14 -S55_bit15 -S55_bit16 -S55_bit17 -S55_bit18 -S55_bit19 -S31_bit_10 -S31_bit_9 -S31_bit_8 -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 -S31_bit13 -S31_bit14 -S31_bit15 -S31_bit16 -S31_bit17 -S31_bit18 -S31_bit19 -S32_bit_10 -S32_bit_9 -S32_bit_8 -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 -S32_bit13 -S32_bit14 -S32_bit15 -S32_bit16 -S32_bit17 -S32_bit18 -S32_bit19 -S33_bit_10 -S33_bit_9 -S33_bit_8 -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 -S33_bit13 -S33_bit14 -S33_bit15 -S33_bit16 -S33_bit17 -S33_bit18 -S33_bit19 -S34_bit_10 -S34_bit_9 -S34_bit_8 -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 -S34_bit13 -S34_bit14 -S34_bit15 -S34_bit16 -S34_bit17 -S34_bit18 -S34_bit19 -S35_bit_10 -S35_bit_9 -S35_bit_8 -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 -S35_bit13 -S35_bit14 -S35_bit15 -S35_bit16 -S35_bit17 -S35_bit18 -S35_bit19 -S41_bit_10 -S41_bit_9 -S41_bit_8 -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 -S41_bit13 -S41_bit14 -S41_bit15 -S41_bit16 -S41_bit17 -S41_bit18 -S41_bit19 -S42_bit_10 -S42_bit_9 -S42_bit_8 -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 -S42_bit13 -S42_bit14 -S42_bit15 -S42_bit16 -S42_bit17 -S42_bit18 -S42_bit19 -S43_bit_10 -S43_bit_9 -S43_bit_8 -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 -S43_bit13 -S43_bit14 -S43_bit15 -S43_bit16 -S43_bit17 -S43_bit18 -S43_bit19 -S44_bit_10 S44_bit_9 -S44_bit_8 -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 -S44_bit13 -S44_bit14 -S44_bit15 -S44_bit16 -S44_bit17 -S44_bit18 -S44_bit19 -S45_bit_10 -S45_bit_9 -S45_bit_8 -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 -S45_bit13 -S45_bit14 -S45_bit15 -S45_bit16 -S45_bit17 -S45_bit18 -S45_bit19 -S51_bit_10 -S51_bit_9 -S51_bit_8 -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 -S51_bit13 -S51_bit14 -S51_bit15 -S51_bit16 -S51_bit17 -S51_bit18 -S51_bit19 -S52_bit_10 -S52_bit_9 -S52_bit_8 -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 -S52_bit13 -S52_bit14 -S52_bit15 -S52_bit16 -S52_bit17 -S52_bit18 -S52_bit19 -S53_bit_10 -S53_bit_9 -S53_bit_8 -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 -S53_bit13 -S53_bit14 -S53_bit15 -S53_bit16 -S53_bit17 -S53_bit18 -S53_bit19 -V148_bit_10 -V148_bit_9 -V148_bit_8 -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 -V148_bit13 -V148_bit14 -V148_bit15 -V148_bit16 -V148_bit17 -V148_bit18 -V148_bit19 -V150_bit_10 -V150_bit_9 -V150_bit_8 -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 -V150_bit13 -V150_bit14 -V150_bit15 -V150_bit16 -V150_bit17 -V150_bit18 -V150_bit19 -Q246_bit_10 -Q246_bit_9 -Q246_bit_8 -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 -Q246_bit13 -Q246_bit14 -Q246_bit15 -Q246_bit16 -Q246_bit17 -Q246_bit18 -Q246_bit19 -S11_bit_10 -S11_bit_9 -S11_bit_8 -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 -S11_bit13 -S11_bit14 -S11_bit15 -S11_bit16 -S11_bit17 -S11_bit18 -S11_bit19 -S21_bit_10 -S21_bit_9 -S21_bit_8 -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 -S21_bit13 -S21_bit14 -S21_bit15 -S21_bit16 -S21_bit17 -S21_bit18 -S21_bit19 -S12_bit_10 -S12_bit_9 S12_bit_8 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 -S12_bit13 -S12_bit14 -S12_bit15 -S12_bit16 -S12_bit17 -S12_bit18 -S12_bit19 -S22_bit_10 -S22_bit_9 -S22_bit_8 -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 -S22_bit13 -S22_bit14 -S22_bit15 -S22_bit16 -S22_bit17 -S22_bit18 -S22_bit19 -S13_bit_10 -S13_bit_9 S13_bit_8 -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 -S13_bit13 -S13_bit14 -S13_bit15 -S13_bit16 -S13_bit17 -S13_bit18 -S13_bit19 -S23_bit_10 -S23_bit_9 -S23_bit_8 -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 -S23_bit13 -S23_bit14 -S23_bit15 -S23_bit16 -S23_bit17 -S23_bit18 -S23_bit19 -S14_bit_10 S14_bit_9 -S14_bit_8 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 -S14_bit13 -S14_bit14 -S14_bit15 -S14_bit16 -S14_bit17 -S14_bit18 -S14_bit19 -S15_bit_10 S15_bit_9 -S15_bit_8 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 -S15_bit13 -S15_bit14 -S15_bit15 -S15_bit16 -S15_bit17 -S15_bit18 -S15_bit19
c _______________________________________________________________________________
c 
c restarts              : 46
c conflicts             : 54369          (304 /sec)
c decisions             : 212504         (1188 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 178.909 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.99 0.99 0.91 2/54 14189
Raw data (stat): 14189 (runsolver) R 14188 21152 21151 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 795867689 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 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.0011 s]
Raw data (loadavg): 0.99 0.99 0.91 2/55 14194
Raw data (stat): 14189 (minisat+_script) S 14188 21152 21151 0 -1 0 300 368 0 0 0 0 1 0 20 0 1 0 795867689 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 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.0019 s]
Raw data (loadavg): 0.99 0.99 0.91 2/55 14194
Raw data (stat): 14189 (minisat+_script) S 14188 21152 21151 0 -1 0 300 368 0 0 0 0 1 0 20 0 1 0 795867689 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 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.0023 s]
Raw data (loadavg): 0.99 0.99 0.91 2/55 14194
Raw data (stat): 14189 (minisat+_script) S 14188 21152 21151 0 -1 0 300 368 0 0 0 0 1 0 20 0 1 0 795867689 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 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.0026 s]
Raw data (loadavg): 0.99 0.99 0.91 2/55 14194
Raw data (stat): 14189 (minisat+_script) S 14188 21152 21151 0 -1 0 300 368 0 0 0 0 1 0 20 0 1 0 795867689 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 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.0035 s]
Raw data (loadavg): 0.99 0.99 0.91 2/55 14194
Raw data (stat): 14189 (minisat+_script) S 14188 21152 21151 0 -1 0 300 368 0 0 0 0 1 0 20 0 1 0 795867689 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 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.0039 s]
Raw data (loadavg): 0.99 0.99 0.91 2/55 14194
Raw data (stat): 14189 (minisat+_script) S 14188 21152 21151 0 -1 0 300 368 0 0 0 0 1 0 20 0 1 0 795867689 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 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.0045 s]
Raw data (loadavg): 0.99 0.99 0.91 2/55 14194
Raw data (stat): 14189 (minisat+_script) S 14188 21152 21151 0 -1 0 300 368 0 0 0 0 1 0 20 0 1 0 795867689 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 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.006 s]
Raw data (loadavg): 0.99 0.99 0.91 2/55 14194
Raw data (stat): 14189 (minisat+_script) S 14188 21152 21151 0 -1 0 300 368 0 0 0 0 1 0 20 0 1 0 795867689 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 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.0055 s]
Raw data (loadavg): 0.99 0.99 0.91 2/55 14194
Raw data (stat): 14189 (minisat+_script) S 14188 21152 21151 0 -1 0 300 368 0 0 0 0 1 0 20 0 1 0 795867689 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 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.007 s]
Raw data (loadavg): 0.99 0.99 0.91 2/55 14194
Raw data (stat): 14189 (minisat+_script) S 14188 21152 21151 0 -1 0 300 368 0 0 0 0 1 0 20 0 1 0 795867689 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 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.008 s]
Raw data (loadavg): 0.99 0.99 0.91 2/55 14194
Raw data (stat): 14189 (minisat+_script) S 14188 21152 21151 0 -1 0 300 368 0 0 0 0 1 0 20 0 1 0 795867689 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 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.008 s]
Raw data (loadavg): 0.99 0.99 0.91 2/55 14194
Raw data (stat): 14189 (minisat+_script) S 14188 21152 21151 0 -1 0 300 368 0 0 0 0 1 0 20 0 1 0 795867689 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 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.009 s]
Raw data (loadavg): 0.99 0.99 0.91 2/55 14194
Raw data (stat): 14189 (minisat+_script) S 14188 21152 21151 0 -1 0 300 368 0 0 0 0 1 0 20 0 1 0 795867689 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 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.009 s]
Raw data (loadavg): 0.99 0.99 0.91 2/55 14194
Raw data (stat): 14189 (minisat+_script) S 14188 21152 21151 0 -1 0 300 368 0 0 0 0 1 0 20 0 1 0 795867689 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 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.01 s]
Raw data (loadavg): 0.99 0.99 0.91 2/55 14194
Raw data (stat): 14189 (minisat+_script) S 14188 21152 21151 0 -1 0 300 368 0 0 0 0 1 0 20 0 1 0 795867689 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 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.01 s]
Raw data (loadavg): 0.99 0.99 0.91 2/55 14194
Raw data (stat): 14189 (minisat+_script) S 14188 21152 21151 0 -1 0 300 368 0 0 0 0 1 0 20 0 1 0 795867689 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 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.01 s]
Raw data (loadavg): 0.99 0.99 0.91 2/55 14194
Raw data (stat): 14189 (minisat+_script) S 14188 21152 21151 0 -1 0 300 368 0 0 0 0 1 0 20 0 1 0 795867689 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 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+179.176 s]
Raw data (loadavg): 0.99 0.99 0.91 1/53 14194
Raw data (stat): 14189 (minisat+_script) S 14188 21152 21151 0 -1 0 300 368 0 0 0 0 1 0 20 0 1 0 795867689 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 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): 179.175
CPU time (s): 179.166
CPU user time (s): 178.94
CPU system time (s): 0.225965
CPU usage (%): 99.9947
Max. virtual memory (Kb): 2128
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	-41
#### END VERIFIER DATA ####