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/miplib2003/normalized-mps-v2-20-10-noswot.opb
MD5SUM	ce1061a060a0716eafe03a61d610732a
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	41943040000000
Number of bits of the biggest number in a constraint	46
Biggest sum of numbers in a constraint	204183950227182
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	145.757
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 30747

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-05-25 19:23:15 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22172 boxname=wulflinc20 idbench=988 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  ce1061a060a0716eafe03a61d610732a  /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-noswot.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-noswot.opb
IDLAUNCH: 22172
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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	: 3
cpu MHz		: 451.215
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        173848 kB
Buffers:         37764 kB
Cached:         793160 kB
SwapCached:        716 kB
Active:          72176 kB
Inactive:       765544 kB
HighTotal:      131008 kB
HighFree:         2716 kB
LowTotal:       903652 kB
LowFree:        171132 kB
SwapTotal:     2097892 kB
SwapFree:      2096336 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5072 kB
Slab:            17448 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 19:25:41 (client local time) WITH STATUS 30 IN 145.757 SECONDS
stats: 22172 0 145.757 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:  820
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:   56
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:  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:  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 ---[ 139]---> BDD-cost:  301
c ---[ 138]---> BDD-cost:    6
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 ---[ 126]---> 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 ---[ 115]---> BDD-cost:  102
c ---[ 114]---> BDD-cost:    3
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:   51
c ---[ 103]---> BDD-cost:  820
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:    2
c ---[  92]---> BDD-cost:  561
c ---[  90]---> BDD-cost:    2
c ---[  89]---> BDD-cost:   19
c ---[  88]---> BDD-cost:  820
c ---[  87]---> BDD-cost:   89
c ---[  86]---> BDD-cost:  561
c ---[  85]---> BDD-cost:  820
c ---[  84]---> BDD-cost:  561
c ---[  83]---> BDD-cost:  820
c ---[  82]---> BDD-cost:  561
c ---[  81]---> BDD-cost:  820
c ---[  80]---> BDD-cost:  308
c ---[  79]---> BDD-cost:  415
c ---[  78]---> BDD-cost:  598
c ---[  77]---> BDD-cost:  415
c ---[  76]---> BDD-cost:   89
c ---[  75]---> BDD-cost:  598
c ---[  74]---> BDD-cost:  415
c ---[  73]---> BDD-cost:  598
c ---[  72]---> BDD-cost:  415
c ---[  71]---> BDD-cost:  598
c ---[  70]---> BDD-cost:  415
c ---[  69]---> BDD-cost:  329
c ---[  68]---> BDD-cost:  144
c ---[  67]---> BDD-cost:  621
c ---[  66]---> BDD-cost:  144
c ---[  65]---> BDD-cost:   89
c ---[  64]---> BDD-cost:  621
c ---[  63]---> BDD-cost:  144
c ---[  62]---> BDD-cost:  621
c ---[  61]---> BDD-cost:  144
c ---[  60]---> BDD-cost:  621
c ---[  59]---> BDD-cost:  144
c ---[  58]---> BDD-cost:  379
c ---[  57]---> BDD-cost:  297
c ---[  56]---> BDD-cost:  555
c ---[  55]---> BDD-cost:  297
c ---[  54]---> BDD-cost:   89
c ---[  53]---> BDD-cost:  555
c ---[  52]---> BDD-cost:  297
c ---[  51]---> BDD-cost:  555
c ---[  50]---> BDD-cost:  297
c ---[  49]---> BDD-cost:  555
c ---[  48]---> BDD-cost:  297
c ---[  47]---> BDD-cost:  313
c ---[  46]---> Sorter-cost:  147     Base: 2 2 2
c ---[  45]---> BDD-cost:   94
c ---[  44]---> BDD-cost:   94
c ---[  43]---> BDD-cost:   71
c ---[  42]---> BDD-cost:   94
c ---[  41]---> BDD-cost:   94
c ---[  40]---> BDD-cost:   78
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:  320
c ---[  27]---> BDD-cost:  738
c ---[  26]---> BDD-cost:  320
c ---[  25]---> BDD-cost:  738
c ---[  24]---> BDD-cost:  320
c ---[  23]---> BDD-cost:  738
c ---[  22]---> BDD-cost:  320
c ---[  21]---> BDD-cost:    6
c ---[  20]---> BDD-cost:  738
c ---[  19]---> BDD-cost:  320
c ---[  18]---> BDD-cost:  738
c ---[  17]---> BDD-cost:  152
c ---[  16]---> BDD-cost:  773
c ---[  15]---> BDD-cost:  152
c ---[  14]---> BDD-cost:  773
c ---[  13]---> BDD-cost:  152
c ---[  12]---> BDD-cost:  773
c ---[  11]---> BDD-cost:  152
c ---[   9]---> BDD-cost:  773
c ---[   8]---> BDD-cost:  152
c ---[   7]---> BDD-cost:  773
c ---[   6]---> BDD-cost:  269
c ---[   5]---> BDD-cost:  708
c ---[   4]---> BDD-cost:  269
c ---[   3]---> BDD-cost:  708
c ---[   2]---> BDD-cost:  269
c ---[   1]---> BDD-cost:  708
c ---[   0]---> BDD-cost:  157
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   90344   252471 |   30114       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -31[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 |        43 |   91603   255441 |   30534      42      256     6.1 |  0.000 % |
c |       143 |   91469   255159 |   33587     133      877     6.6 |  7.325 % |
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 |       173 |   92322   257131 |   30774     163     1083     6.6 |  7.325 % |
c |       273 |   92322   257131 |   33851     263     2956    11.2 |  7.336 % |
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 |       409 |   92194   256850 |   30731     396     4382    11.1 |  7.336 % |
c |       510 |   92194   256850 |   33804     497     5486    11.0 |  7.472 % |
c |       660 |   92194   256850 |   37184     647     7891    12.2 |  7.472 % |
c |       886 |   92169   256796 |   40902     869    10323    11.9 |  7.493 % |
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 |       939 |   92173   256809 |   30724     922    10670    11.6 |  7.493 % |
c |      1039 |   92173   256809 |   33796    1022    12154    11.9 |  7.495 % |
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 |      1171 |   92110   256662 |   30703    1146    14368    12.5 |  7.495 % |
c |      1271 |   92110   256662 |   33773    1246    16246    13.0 |  7.555 % |
c |      1422 |   92088   256612 |   37150    1337    17847    13.3 |  7.585 % |
c |      1647 |   92088   256612 |   40865    1562    22000    14.1 |  7.585 % |
c |      1985 |   92088   256612 |   44952    1900    26986    14.2 |  7.585 % |
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 |      2224 |   92088   256614 |   30696    2131    29132    13.7 |  7.585 % |
c |      2324 |   92088   256614 |   33765    2231    31881    14.3 |  7.597 % |
c |      2474 |   92088   256614 |   37142    2381    35912    15.1 |  7.597 % |
c |      2699 |   92088   256614 |   40856    2606    40514    15.5 |  7.597 % |
c |      3038 |   92088   256614 |   44942    2945    48868    16.6 |  7.597 % |
c |      3545 |   92059   256549 |   49436    3442    59252    17.2 |  7.622 % |
c |      4306 |   92059   256549 |   54379    4203    75585    18.0 |  7.622 % |
c |      5445 |   92059   256549 |   59817    5342    97997    18.3 |  7.622 % |
c |      7155 |   92059   256549 |   65799    7052   138180    19.6 |  7.622 % |
c |      9721 |   92037   256499 |   72379    9615   186814    19.4 |  7.637 % |
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 |     10614 |   92040   256506 |   30680   10508   205251    19.5 |  7.637 % |
c |     10715 |   92040   256506 |   33748   10609   206710    19.5 |  7.640 % |
c |     10866 |   92040   256506 |   37122   10760   209045    19.4 |  7.639 % |
c |     11091 |   92040   256506 |   40835   10985   214376    19.5 |  7.639 % |
c |     11428 |   92040   256506 |   44918   11322   221302    19.5 |  7.640 % |
c |     11935 |   92040   256506 |   49410   11829   231814    19.6 |  7.639 % |
c |     12694 |   92040   256506 |   54351   12588   244329    19.4 |  7.639 % |
c |     13834 |   92040   256506 |   59786   13728   264379    19.3 |  7.639 % |
c |     15544 |   92040   256506 |   65765   15438   298402    19.3 |  7.639 % |
c |     18108 |   92040   256506 |   72341   18002   349937    19.4 |  7.639 % |
c |     21954 |   92025   256473 |   79576   21834   409442    18.8 |  7.652 % |
c |     27720 |   91859   256088 |   87533   23963   460743    19.2 |  7.801 % |
c |     36369 |   91800   255923 |   96286   23369   440632    18.9 |  7.829 % |
c |     49343 |   91536   255217 |  105915   21394   398691    18.6 |  8.005 % |
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_10 -x109_bit_9 -x109_bit_8 -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 -x109_bit13 -x109_bit14 -x109_bit15 -x109_bit16 -x109_bit17 -x109_bit18 -x109_bit19 -x124_bit_10 -x124_bit_9 -x124_bit_8 -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 -x124_bit13 -x124_bit14 -x124_bit15 -x124_bit16 -x124_bit17 -x124_bit18 -x124_bit19 -x110_bit_10 -x110_bit_9 -x110_bit_8 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 -x110_bit13 -x110_bit14 -x110_bit15 -x110_bit16 -x110_bit17 -x110_bit18 -x110_bit19 -x125_bit_10 -x125_bit_9 -x125_bit_8 -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 -x125_bit13 -x125_bit14 -x125_bit15 -x125_bit16 -x125_bit17 -x125_bit18 -x125_bit19 -x111_bit_10 -x111_bit_9 -x111_bit_8 -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 -x111_bit13 -x111_bit14 -x111_bit15 -x111_bit16 -x111_bit17 -x111_bit18 -x111_bit19 -x112_bit_10 -x112_bit_9 -x112_bit_8 -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 -x112_bit13 -x112_bit14 -x112_bit15 -x112_bit16 -x112_bit17 -x112_bit18 -x112_bit19 -x113_bit_10 -x113_bit_9 -x113_bit_8 -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 -x113_bit13 -x113_bit14 -x113_bit15 -x113_bit16 -x113_bit17 -x113_bit18 -x113_bit19 -x114_bit_10 -x114_bit_9 -x114_bit_8 -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 -x114_bit13 -x114_bit14 -x114_bit15 -x114_bit16 -x114_bit17 -x114_bit18 -x114_bit19 -x115_bit_10 -x115_bit_9 -x115_bit_8 -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 -x115_bit13 -x115_bit14 -x115_bit15 -x115_bit16 -x115_bit17 -x115_bit18 -x115_bit19 -x116_bit_10 -x116_bit_9 -x116_bit_8 -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 -x116_bit13 -x116_bit14 -x116_bit15 -x116_bit16 -x116_bit17 -x116_bit18 -x116_bit19 -x117_bit_10 -x117_bit_9 -x117_bit_8 -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 -x117_bit13 -x117_bit14 -x117_bit15 -x117_bit16 -x117_bit17 -x117_bit18 -x117_bit19 x118_bit_10 x118_bit_9 x118_bit_8 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 -x118_bit13 -x118_bit14 -x118_bit15 -x118_bit16 -x118_bit17 -x118_bit18 -x118_bit19 -x119_bit_10 -x119_bit_9 -x119_bit_8 -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 -x119_bit13 -x119_bit14 -x119_bit15 -x119_bit16 -x119_bit17 -x119_bit18 -x119_bit19 -x120_bit_10 -x120_bit_9 -x120_bit_8 -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 -x120_bit13 -x120_bit14 -x120_bit15 -x120_bit16 -x120_bit17 -x120_bit18 -x120_bit19 x121_bit_10 -x121_bit_9 -x121_bit_8 -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 -x121_bit13 -x121_bit14 -x121_bit15 -x121_bit16 -x121_bit17 -x121_bit18 -x121_bit19 -x122_bit_10 -x122_bit_9 -x122_bit_8 -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 -x122_bit13 -x122_bit14 -x122_bit15 -x122_bit16 -x122_bit17 -x122_bit18 -x122_bit19 -x123_bit_10 -x123_bit_9 -x123_bit_8 -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 -x123_bit13 -x123_bit14 -x123_bit15 -x123_bit16 -x123_bit17 -x123_bit18 -x123_bit19 -x127_bit_10 -x127_bit_9 -x127_bit_8 -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 -x127_bit13 -x127_bit14 -x127_bit15 -x127_bit16 -x127_bit17 -x127_bit18 -x127_bit19 -x126_bit_10 -x126_bit_9 -x126_bit_8 -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 -x126_bit13 -x126_bit14 -x126_bit15 -x126_bit16 -x126_bit17 -x126_bit18 -x126_bit19 -x128_bit_10 -x128_bit_9 -x128_bit_8 -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 -x128_bit13 -x128_bit14 -x128_bit15 -x128_bit16 -x128_bit17 -x128_bit18 -x128_bit19 -x101_bit_10 x101_bit_9 -x101_bit_8 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 -x101_bit13 -x101_bit14 -x101_bit15 -x101_bit16 -x101_bit17 -x101_bit18 -x101_bit19 -x106_bit_10 -x106_bit_9 -x106_bit_8 -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 -x106_bit13 -x106_bit14 -x106_bit15 -x106_bit16 -x106_bit17 -x106_bit18 -x106_bit19 -x102_bit_10 -x102_bit_9 -x102_bit_8 -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 -x102_bit13 -x102_bit14 -x102_bit15 -x102_bit16 -x102_bit17 -x102_bit18 -x102_bit19 -x107_bit_10 -x107_bit_9 -x107_bit_8 -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 -x107_bit13 -x107_bit14 -x107_bit15 -x107_bit16 -x107_bit17 -x107_bit18 -x107_bit19 -x103_bit_10 -x103_bit_9 x103_bit_8 -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 -x103_bit13 -x103_bit14 -x103_bit15 -x103_bit16 -x103_bit17 -x103_bit18 -x103_bit19 -x108_bit_10 -x108_bit_9 -x108_bit_8 -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 -x108_bit13 -x108_bit14 -x108_bit15 -x108_bit16 -x108_bit17 -x108_bit18 -x108_bit19 -x104_bit_10 -x104_bit_9 -x104_bit_8 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 -x104_bit13 -x104_bit14 -x104_bit15 -x104_bit16 -x104_bit17 -x104_bit18 -x104_bit19 -x105_bit_10 x105_bit_9 x105_bit_8 -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 -x105_bit13 -x105_bit14 -x105_bit15 -x105_bit16 -x105_bit17 -x105_bit18 -x105_bit19
c _______________________________________________________________________________
c 
c restarts              : 40
c conflicts             : 49863          (343 /sec)
c decisions             : 176974         (1216 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 145.577 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.91 0.95 0.91 1/54 8181
Raw data (stat): 8181 (runsolver) D 8180 25399 25398 0 -1 64 4 0 0 0 0 0 0 0 18 0 1 0 841369379 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 3225161850 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.93 0.95 0.91 2/55 8185
Raw data (stat): 8181 (minisat+_script) S 8180 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841369379 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.001 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 8185
Raw data (stat): 8181 (minisat+_script) S 8180 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841369379 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0021 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 8185
Raw data (stat): 8181 (minisat+_script) S 8180 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841369379 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0018 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 8185
Raw data (stat): 8181 (minisat+_script) S 8180 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841369379 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0015 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 8185
Raw data (stat): 8181 (minisat+_script) S 8180 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841369379 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0012 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 8185
Raw data (stat): 8181 (minisat+_script) S 8180 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841369379 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.001 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 8185
Raw data (stat): 8181 (minisat+_script) S 8180 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841369379 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0017 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 8185
Raw data (stat): 8181 (minisat+_script) S 8180 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841369379 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0013 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 8185
Raw data (stat): 8181 (minisat+_script) S 8180 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841369379 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.001 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 8185
Raw data (stat): 8181 (minisat+_script) S 8180 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841369379 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 8185
Raw data (stat): 8181 (minisat+_script) S 8180 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841369379 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 8185
Raw data (stat): 8181 (minisat+_script) S 8180 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841369379 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 8185
Raw data (stat): 8181 (minisat+_script) S 8180 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841369379 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 8185
Raw data (stat): 8181 (minisat+_script) S 8180 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841369379 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+145.801 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 8185
Raw data (stat): 8181 (minisat+_script) S 8180 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 841369379 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 30
Real time (s): 145.801
CPU time (s): 145.757
CPU user time (s): 145.598
CPU system time (s): 0.158975
CPU usage (%): 99.97
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	-41
#### END VERIFIER DATA ####