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/miplib3/normalized-mps-v2-13-7-mod010.opb
MD5SUM	ef7064a9be2b712276f7b600af28e2b0
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	6571
Optimality of the best value was proved	NO
Number of terms in the objective function	2655
Biggest coefficient in the objective function	266
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	489211
Number of bits of the sum of numbers in the objective function	19
Biggest number in a constraint	266
Number of bits of the biggest number in a constraint	9
Biggest sum of numbers in a constraint	489211
Number of bits of the biggest sum of numbers	19
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.18
Number of variables	2655
Total number of constraints	2801
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	2800
Number of constraints which are nor clauses,nor cardinality constraints	1
Minimum length of a constraint	1
Maximum length of a constraint	2655
Trace number 15046

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc13 THE 2005-04-21 02:40:43 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18634 boxname=wulflinc13 idbench=1434 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  ef7064a9be2b712276f7b600af28e2b0  /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-mod010.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-mod010.opb
IDLAUNCH: 18634
/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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        812440 kB
Buffers:         32900 kB
Cached:         167048 kB
SwapCached:        176 kB
Active:          36156 kB
Inactive:       166576 kB
HighTotal:      131008 kB
HighFree:        25060 kB
LowTotal:       903652 kB
LowFree:        787380 kB
SwapTotal:     2097136 kB
SwapFree:      2096860 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6808 kB
Slab:            13808 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 03:00:45 (client local time) WITH STATUS 0 IN 1200.25 SECONDS
stats: 18634 7 1200.25 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 291 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 289]---> BDD-cost:   67
c ---[ 287]---> BDD-cost:  113
c ---[ 285]---> BDD-cost:  181
c ---[ 283]---> BDD-cost:  115
c ---[ 281]---> BDD-cost:   69
c ---[ 279]---> BDD-cost:  125
c ---[ 277]---> BDD-cost:  155
c ---[ 275]---> BDD-cost:   87
c ---[ 273]---> BDD-cost:   97
c ---[ 271]---> BDD-cost:   73
c ---[ 269]---> BDD-cost:  119
c ---[ 267]---> BDD-cost:   45
c ---[ 265]---> BDD-cost:  171
c ---[ 263]---> BDD-cost:  111
c ---[ 261]---> BDD-cost:  149
c ---[ 259]---> BDD-cost:  195
c ---[ 257]---> BDD-cost:  131
c ---[ 255]---> BDD-cost:  123
c ---[ 253]---> BDD-cost:  167
c ---[ 251]---> BDD-cost:  101
c ---[ 249]---> BDD-cost:   97
c ---[ 247]---> BDD-cost:   23
c ---[ 245]---> BDD-cost:  135
c ---[ 243]---> BDD-cost:   59
c ---[ 241]---> BDD-cost:   95
c ---[ 239]---> BDD-cost:   59
c ---[ 237]---> BDD-cost:  133
c ---[ 235]---> BDD-cost:   99
c ---[ 233]---> BDD-cost:  179
c ---[ 231]---> BDD-cost:  111
c ---[ 229]---> BDD-cost:   23
c ---[ 227]---> BDD-cost:   89
c ---[ 225]---> BDD-cost:   95
c ---[ 223]---> BDD-cost:  117
c ---[ 221]---> BDD-cost:   23
c ---[ 219]---> BDD-cost:   51
c ---[ 217]---> BDD-cost:  311
c ---[ 215]---> BDD-cost:  259
c ---[ 213]---> BDD-cost:  169
c ---[ 211]---> BDD-cost:  131
c ---[ 209]---> BDD-cost:  155
c ---[ 207]---> BDD-cost:   89
c ---[ 205]---> BDD-cost:   51
c ---[ 203]---> BDD-cost:  165
c ---[ 201]---> BDD-cost:   75
c ---[ 199]---> BDD-cost:  139
c ---[ 197]---> BDD-cost:   67
c ---[ 195]---> BDD-cost:  173
c ---[ 193]---> BDD-cost:  235
c ---[ 191]---> BDD-cost:  185
c ---[ 189]---> BDD-cost:  127
c ---[ 187]---> BDD-cost:   37
c ---[ 185]---> BDD-cost:   37
c ---[ 183]---> BDD-cost:   91
c ---[ 181]---> BDD-cost:   77
c ---[ 179]---> BDD-cost:   29
c ---[ 177]---> BDD-cost:   77
c ---[ 175]---> BDD-cost:   77
c ---[ 173]---> BDD-cost:  101
c ---[ 171]---> BDD-cost:  131
c ---[ 169]---> BDD-cost:  155
c ---[ 167]---> BDD-cost:  177
c ---[ 165]---> BDD-cost:  143
c ---[ 163]---> BDD-cost:   93
c ---[ 161]---> BDD-cost:   79
c ---[ 159]---> BDD-cost:   53
c ---[ 157]---> BDD-cost:   71
c ---[ 155]---> BDD-cost:  127
c ---[ 153]---> BDD-cost:  127
c ---[ 151]---> BDD-cost:   67
c ---[ 149]---> BDD-cost:   83
c ---[ 147]---> BDD-cost:   47
c ---[ 145]---> BDD-cost:   63
c ---[ 143]---> BDD-cost:  121
c ---[ 141]---> BDD-cost:  155
c ---[ 139]---> BDD-cost:   87
c ---[ 137]---> BDD-cost:   91
c ---[ 135]---> BDD-cost:   47
c ---[ 133]---> BDD-cost:   67
c ---[ 131]---> BDD-cost:   33
c ---[ 129]---> BDD-cost:   91
c ---[ 127]---> BDD-cost:   69
c ---[ 125]---> BDD-cost:    5
c ---[ 123]---> BDD-cost:   47
c ---[ 121]---> BDD-cost:   45
c ---[ 119]---> BDD-cost:   37
c ---[ 117]---> BDD-cost:  117
c ---[ 115]---> BDD-cost:   97
c ---[ 113]---> BDD-cost:   77
c ---[ 111]---> BDD-cost:   97
c ---[ 109]---> BDD-cost:  137
c ---[ 107]---> BDD-cost:  125
c ---[ 105]---> BDD-cost:   79
c ---[ 103]---> BDD-cost:  133
c ---[ 101]---> BDD-cost:  153
c ---[  99]---> BDD-cost:  139
c ---[  97]---> BDD-cost:  125
c ---[  95]---> BDD-cost:    5
c ---[  93]---> BDD-cost:   73
c ---[  91]---> BDD-cost:  157
c ---[  89]---> BDD-cost:  127
c ---[  87]---> BDD-cost:  199
c ---[  85]---> BDD-cost:  121
c ---[  83]---> BDD-cost:  107
c ---[  81]---> BDD-cost:  169
c ---[  79]---> BDD-cost:  113
c ---[  77]---> BDD-cost:  103
c ---[  75]---> BDD-cost:   75
c ---[  73]---> BDD-cost:   97
c ---[  71]---> BDD-cost:  151
c ---[  69]---> BDD-cost:  199
c ---[  67]---> BDD-cost:  109
c ---[  65]---> BDD-cost:  131
c ---[  63]---> BDD-cost:  113
c ---[  61]---> BDD-cost:  173
c ---[  59]---> BDD-cost:  119
c ---[  57]---> BDD-cost:  173
c ---[  55]---> BDD-cost:  119
c ---[  53]---> BDD-cost:   71
c ---[  51]---> BDD-cost:  179
c ---[  49]---> BDD-cost:  241
c ---[  47]---> BDD-cost:  201
c ---[  45]---> BDD-cost:  173
c ---[  43]---> BDD-cost:  147
c ---[  41]---> BDD-cost:  157
c ---[  39]---> BDD-cost:  201
c ---[  37]---> BDD-cost:  129
c ---[  35]---> BDD-cost:  117
c ---[  33]---> BDD-cost:  177
c ---[  31]---> BDD-cost:  123
c ---[  29]---> BDD-cost:  131
c ---[  27]---> BDD-cost:  115
c ---[  25]---> BDD-cost:   51
c ---[  23]---> BDD-cost:  123
c ---[  21]---> BDD-cost:   55
c ---[  19]---> BDD-cost:    5
c ---[  17]---> BDD-cost:   99
c ---[  15]---> BDD-cost:   85
c ---[  13]---> BDD-cost:  109
c ---[  11]---> BDD-cost:  153
c ---[   9]---> BDD-cost:  201
c ---[   7]---> BDD-cost:  133
c ---[   5]---> BDD-cost:  121
c ---[   3]---> BDD-cost:  171
c ---[   1]---> Adder-cost: 5294   maxlim: 2609   bits: 12/12
c ---[   0]---> BDD-cost:  751
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   79291   242194 |   26430       0        0     nan |  0.000 % |
c |       101 |   79216   241933 |   29073      93      735     7.9 |  0.735 % |
c |       253 |   79216   241933 |   31980     245     2664    10.9 |  0.735 % |
c |       478 |   79216   241933 |   35178     470    26790    57.0 |  0.735 % |
c |       816 |   79216   241933 |   38696     808    31842    39.4 |  0.735 % |
c |      1323 |   79216   241933 |   42565    1315    62134    47.3 |  0.735 % |
c |      2082 |   79216   241933 |   46822    2074   107560    51.9 |  0.735 % |
c |      3222 |   79188   241847 |   51504    3207   277140    86.4 |  0.751 % |
c |      4930 |   79188   241847 |   56655    4915   483903    98.5 |  0.751 % |
c |      7493 |   79188   241847 |   62320    7478   739580    98.9 |  0.751 % |
c |     11337 |   79188   241847 |   68552   11322  1362239   120.3 |  0.751 % |
c |     17103 |   79164   241769 |   75407   17085  2978250   174.3 |  0.767 % |
c |     25752 |   79164   241769 |   82948   25734  6444146   250.4 |  0.767 % |
c |     38727 |   79164   241769 |   91243   38709 10596182   273.7 |  0.767 % |
c |     58188 |   79145   241708 |  100367   58167 16215504   278.8 |  0.779 % |
c |     87383 |   79101   241554 |  110404   87356 23978747   274.5 |  0.807 % |
c |    131172 |   79079   241468 |  121445   35237  6368599   180.7 |  0.823 % |
c |    196857 |   78549   239688 |  133589  100806 30304920   300.6 |  1.134 % |
#### 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.86 0.95 0.91 2/54 29073
Raw data (stat): 29073 (runsolver) R 29072 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 483337031 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.88 0.95 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 5374 0 0 0 984 14 0 0 25 0 1 0 483337031 22405120 4705 4294967295 134512640 134672761 3221224624 3221223728 134560396 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5470 4705 603 41 0 5429 0
vsize: 21880
[startup+20.0008 s]
Raw data (loadavg): 0.90 0.95 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 5912 0 0 0 1982 15 0 0 25 0 1 0 483337031 24596480 5243 4294967295 134512640 134672761 3221224624 3221223748 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6005 5243 603 41 0 5964 0
vsize: 24020
[startup+30.0008 s]
Raw data (loadavg): 0.92 0.95 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 6499 0 0 0 2981 16 0 0 25 0 1 0 483337031 27025408 5830 4294967295 134512640 134672761 3221224624 3221223808 134559324 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6598 5830 603 41 0 6557 0
vsize: 26392
[startup+40.0011 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 7316 0 0 0 3977 20 0 0 25 0 1 0 483337031 30257152 6647 4294967295 134512640 134672761 3221224624 3221223728 134559985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7387 6647 603 41 0 7346 0
vsize: 29548
[startup+50.0018 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 8051 0 0 0 4976 21 0 0 25 0 1 0 483337031 33443840 7382 4294967295 134512640 134672761 3221224624 3221223792 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8165 7382 603 41 0 8124 0
vsize: 32660
[startup+60.002 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 8689 0 0 0 5974 23 0 0 25 0 1 0 483337031 36007936 8020 4294967295 134512640 134672761 3221224624 3221223728 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8791 8020 603 41 0 8750 0
vsize: 35164
[startup+70.002 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 9326 0 0 0 6972 25 0 0 25 0 1 0 483337031 38572032 8657 4294967295 134512640 134672761 3221224624 3221223728 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9417 8657 603 41 0 9376 0
vsize: 37668
[startup+80.0018 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 9951 0 0 0 7971 27 0 0 25 0 1 0 483337031 41127936 9282 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10041 9282 603 41 0 10000 0
vsize: 40164
[startup+90.0027 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 10520 0 0 0 8970 28 0 0 25 0 1 0 483337031 43413504 9851 4294967295 134512640 134672761 3221224624 3221223728 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10599 9851 603 41 0 10558 0
vsize: 42396
[startup+100.002 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 11082 0 0 0 9969 29 0 0 25 0 1 0 483337031 45838336 10413 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11191 10413 603 41 0 11150 0
vsize: 44764
[startup+110.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 11625 0 0 0 10968 30 0 0 25 0 1 0 483337031 47976448 10956 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11713 10956 603 41 0 11672 0
vsize: 46852
[startup+120.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 12265 0 0 0 11966 32 0 0 25 0 1 0 483337031 50663424 11596 4294967295 134512640 134672761 3221224624 3221223728 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12369 11596 603 41 0 12328 0
vsize: 49476
[startup+130.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 13005 0 0 0 12964 35 0 0 25 0 1 0 483337031 53624832 12336 4294967295 134512640 134672761 3221224624 3221223728 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13092 12336 603 41 0 13051 0
vsize: 52368
[startup+140.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 13640 0 0 0 13963 37 0 0 25 0 1 0 483337031 56299520 12971 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13745 12971 603 41 0 13704 0
vsize: 54980
[startup+150.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 14330 0 0 0 14961 38 0 0 25 0 1 0 483337031 59125760 13661 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14435 13661 603 41 0 14394 0
vsize: 57740
[startup+160.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 14958 0 0 0 15960 40 0 0 25 0 1 0 483337031 61825024 14289 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14289 603 41 0 15053 0
vsize: 60376
[startup+170.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 15556 0 0 0 16959 41 0 0 25 0 1 0 483337031 64249856 14887 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15686 14887 603 41 0 15645 0
vsize: 62744
[startup+180.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 16173 0 0 0 17957 43 0 0 25 0 1 0 483337031 66670592 15504 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16277 15504 603 41 0 16236 0
vsize: 65108
[startup+190.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 16735 0 0 0 18956 44 0 0 25 0 1 0 483337031 68956160 16066 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16835 16066 603 41 0 16794 0
vsize: 67340
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 17464 0 0 0 19954 46 0 0 25 0 1 0 483337031 71929856 16795 4294967295 134512640 134672761 3221224624 3221223760 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17561 16795 603 41 0 17520 0
vsize: 70244
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 18229 0 0 0 20953 47 0 0 25 0 1 0 483337031 75169792 17560 4294967295 134512640 134672761 3221224624 3221223728 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18352 17560 603 41 0 18311 0
vsize: 73408
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 18930 0 0 0 21951 49 0 0 25 0 1 0 483337031 78008320 18261 4294967295 134512640 134672761 3221224624 3221223728 134559979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19045 18261 603 41 0 19004 0
vsize: 76180
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 19558 0 0 0 22949 51 0 0 25 0 1 0 483337031 80556032 18889 4294967295 134512640 134672761 3221224624 3221223728 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19667 18889 603 41 0 19626 0
vsize: 78668
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 20203 0 0 0 23948 52 0 0 25 0 1 0 483337031 83120128 19534 4294967295 134512640 134672761 3221224624 3221223728 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20293 19534 603 41 0 20252 0
vsize: 81172
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 20814 0 0 0 24947 54 0 0 25 0 1 0 483337031 85688320 20145 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20920 20145 603 41 0 20879 0
vsize: 83680
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 21410 0 0 0 25946 55 0 0 25 0 1 0 483337031 88125440 20741 4294967295 134512640 134672761 3221224624 3221223788 134559748 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21515 20741 603 41 0 21474 0
vsize: 86060
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 21861 0 0 0 26945 56 0 0 25 0 1 0 483337031 90005504 21192 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21974 21192 603 41 0 21933 0
vsize: 87896
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 22389 0 0 0 27944 57 0 0 25 0 1 0 483337031 92168192 21720 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22502 21720 603 41 0 22461 0
vsize: 90008
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 23005 0 0 0 28943 58 0 0 25 0 1 0 483337031 94588928 22336 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23093 22336 603 41 0 23052 0
vsize: 92372
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 23634 0 0 0 29941 60 0 0 25 0 1 0 483337031 97271808 22965 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23748 22965 603 41 0 23707 0
vsize: 94992
[startup+310.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 24089 0 0 0 30941 61 0 0 25 0 1 0 483337031 99291136 23420 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24241 23420 603 41 0 24200 0
vsize: 96964
[startup+320.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 24681 0 0 0 31939 62 0 0 25 0 1 0 483337031 101715968 24012 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24833 24012 603 41 0 24792 0
vsize: 99332
[startup+330.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 25122 0 0 0 32938 63 0 0 25 0 1 0 483337031 103600128 24453 4294967295 134512640 134672761 3221224624 3221223728 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25293 24454 603 41 0 25252 0
vsize: 101172
[startup+340.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 25715 0 0 0 33937 65 0 0 25 0 1 0 483337031 106016768 25046 4294967295 134512640 134672761 3221224624 3221223728 134560051 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25883 25046 603 41 0 25842 0
vsize: 103532
[startup+350.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 26471 0 0 0 34936 66 0 0 25 0 1 0 483337031 109096960 25802 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26635 25802 603 41 0 26594 0
vsize: 106540
[startup+360.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 27243 0 0 0 35935 68 0 0 25 0 1 0 483337031 112209920 26574 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27395 26574 603 41 0 27354 0
vsize: 109580
[startup+370.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 27777 0 0 0 36933 69 0 0 25 0 1 0 483337031 114368512 27108 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27922 27108 603 41 0 27881 0
vsize: 111688
[startup+380.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 28111 0 0 0 37933 70 0 0 25 0 1 0 483337031 115712000 27442 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28250 27442 603 41 0 28209 0
vsize: 113000
[startup+390.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 28631 0 0 0 38932 71 0 0 25 0 1 0 483337031 117870592 27962 4294967295 134512640 134672761 3221224624 3221223808 134559379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28777 27962 603 41 0 28736 0
vsize: 115108
[startup+400.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 29046 0 0 0 39931 72 0 0 25 0 1 0 483337031 119631872 28377 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29207 28377 603 41 0 29166 0
vsize: 116828
[startup+410.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 29566 0 0 0 40930 74 0 0 25 0 1 0 483337031 121663488 28897 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29703 28897 603 41 0 29662 0
vsize: 118812
[startup+420.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 30140 0 0 0 41928 75 0 0 25 0 1 0 483337031 124092416 29471 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30296 29471 603 41 0 30255 0
vsize: 121184
[startup+430.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 30714 0 0 0 42926 76 0 0 25 0 1 0 483337031 126390272 30045 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30857 30045 603 41 0 30816 0
vsize: 123428
[startup+440.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 31418 0 0 0 43924 78 0 0 25 0 1 0 483337031 129318912 30749 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31572 30749 603 41 0 31531 0
vsize: 126288
[startup+450.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 32126 0 0 0 44922 80 0 0 25 0 1 0 483337031 132145152 31457 4294967295 134512640 134672761 3221224624 3221223728 134559939 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32262 31457 603 41 0 32221 0
vsize: 129048
[startup+460.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 32768 0 0 0 45921 82 0 0 25 0 1 0 483337031 134828032 32099 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32917 32099 603 41 0 32876 0
vsize: 131668
[startup+470.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 33362 0 0 0 46920 84 0 0 25 0 1 0 483337031 137261056 32693 4294967295 134512640 134672761 3221224624 3221223728 134559941 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33511 32693 603 41 0 33470 0
vsize: 134044
[startup+480.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 33948 0 0 0 47918 85 0 0 25 0 1 0 483337031 139571200 33279 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34075 33279 603 41 0 34034 0
vsize: 136300
[startup+490.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 34503 0 0 0 48917 86 0 0 25 0 1 0 483337031 141889536 33834 4294967295 134512640 134672761 3221224624 3221223728 134560291 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34641 33834 603 41 0 34600 0
vsize: 138564
[startup+500.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 35023 0 0 0 49916 88 0 0 25 0 1 0 483337031 144031744 34354 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35164 34354 603 41 0 35123 0
vsize: 140656
[startup+510.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 35469 0 0 0 50915 89 0 0 25 0 1 0 483337031 145788928 34800 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35593 34800 603 41 0 35552 0
vsize: 142372
[startup+520.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 35988 0 0 0 51914 90 0 0 25 0 1 0 483337031 147947520 35319 4294967295 134512640 134672761 3221224624 3221223728 134560376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36120 35319 603 41 0 36079 0
vsize: 144480
[startup+530.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 36506 0 0 0 52913 92 0 0 25 0 1 0 483337031 150106112 35837 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36647 35837 603 41 0 36606 0
vsize: 146588
[startup+540.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 37011 0 0 0 53912 93 0 0 25 0 1 0 483337031 152129536 36342 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37141 36342 603 41 0 37100 0
vsize: 148564
[startup+550.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 37303 0 0 0 54911 94 0 0 25 0 1 0 483337031 153346048 36634 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37438 36634 603 41 0 37397 0
vsize: 149752
[startup+560.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 37731 0 0 0 55910 95 0 0 25 0 1 0 483337031 155111424 37062 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37869 37062 603 41 0 37828 0
vsize: 151476
[startup+570.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 38211 0 0 0 56909 96 0 0 25 0 1 0 483337031 157003776 37542 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38331 37542 603 41 0 38290 0
vsize: 153324
[startup+580.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 38798 0 0 0 57907 98 0 0 25 0 1 0 483337031 159432704 38129 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38924 38129 603 41 0 38883 0
vsize: 155696
[startup+590.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39390 0 0 0 58906 100 0 0 25 0 1 0 483337031 161857536 38721 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39516 38721 603 41 0 39475 0
vsize: 158064
[startup+600.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 59906 100 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223760 134565076 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+610.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 60906 100 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223824 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+620.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 61906 100 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+630.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 62906 100 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+640.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 63906 100 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134559908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+650.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 64907 100 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+660.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 65906 100 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+670.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 66905 101 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+680.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 67905 101 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+690.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 68905 101 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+700.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 69905 102 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134559964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+710.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 70905 102 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+720.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 71905 102 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+730.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 72905 103 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+740.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 73904 103 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+750.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 74905 103 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+760.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 75904 104 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+770.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 76904 104 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+780.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 77904 104 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134560034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+790.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 78904 105 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+800.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 79903 105 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134560367 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+810.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 80903 105 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134559953 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+820.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 81903 106 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+830.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 82903 106 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134559866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+840.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 83902 107 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134559866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+850.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 84902 107 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+860.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 85902 107 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+870.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 86902 108 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+880.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 87902 108 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+890.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 88901 109 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+900.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 89901 109 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+910.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 90901 109 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+920.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 91901 110 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+930.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 92901 110 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+940.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 93901 110 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+950.017 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 94901 110 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+960.017 s]
Raw data (loadavg): 1.14 1.00 0.92 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 95901 110 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+970.017 s]
Raw data (loadavg): 1.11 1.00 0.92 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 96901 110 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134560299 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+980.017 s]
Raw data (loadavg): 1.10 1.00 0.92 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 97902 110 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+990.025 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 98902 110 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+1000.03 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 99903 110 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134560148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+1010.02 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 100903 110 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+1020.03 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 101903 110 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134560150 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+1030.03 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 102903 110 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+1040.02 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 103903 110 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223768 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+1050.03 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 104903 110 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+1060.03 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 105903 110 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+1070.03 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 106904 110 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+1080.03 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 107904 110 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+1090.02 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39541 0 0 0 108904 110 0 0 25 0 1 0 483337031 162398208 38872 4294967295 134512640 134672761 3221224624 3221223796 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+1100.03 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 39740 0 0 0 109904 110 0 0 25 0 1 0 483337031 163213312 39071 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39847 39071 603 41 0 39806 0
vsize: 159388
[startup+1110.03 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 40195 0 0 0 110903 111 0 0 25 0 1 0 483337031 165105664 39526 4294967295 134512640 134672761 3221224624 3221223768 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40309 39526 603 41 0 40268 0
vsize: 161236
[startup+1120.03 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 40633 0 0 0 111902 112 0 0 25 0 1 0 483337031 166989824 39964 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40769 39964 603 41 0 40728 0
vsize: 163076
[startup+1130.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 41362 0 0 0 112901 113 0 0 25 0 1 0 483337031 169934848 40693 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41488 40693 603 41 0 41447 0
vsize: 165952
[startup+1140.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 41821 0 0 0 113900 114 0 0 25 0 1 0 483337031 171798528 41152 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41943 41152 603 41 0 41902 0
vsize: 167772
[startup+1150.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 42347 0 0 0 114900 115 0 0 25 0 1 0 483337031 173977600 41678 4294967295 134512640 134672761 3221224624 3221223808 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42475 41678 603 41 0 42434 0
vsize: 169900
[startup+1160.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29073
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 42854 0 0 0 115899 116 0 0 25 0 1 0 483337031 175976448 42185 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42963 42185 603 41 0 42922 0
vsize: 171852
[startup+1170.03 s]
Raw data (loadavg): 1.07 1.02 0.93 2/54 29126
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 43422 0 0 0 116898 117 0 0 25 0 1 0 483337031 178266112 42753 4294967295 134512640 134672761 3221224624 3221223728 134559933 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43522 42753 603 41 0 43481 0
vsize: 174088
[startup+1180.03 s]
Raw data (loadavg): 1.06 1.02 0.93 2/54 29126
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 44163 0 0 0 117897 118 0 0 25 0 1 0 483337031 181391360 43494 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44285 43494 603 41 0 44244 0
vsize: 177140
[startup+1190.03 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 29126
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 44880 0 0 0 118896 119 0 0 25 0 1 0 483337031 184242176 44211 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44981 44211 603 41 0 44940 0
vsize: 179924
[startup+1200.03 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 29126
Raw data (stat): 29073 (minisat+) R 29072 30701 30700 0 -1 0 45474 0 0 0 119895 121 0 0 25 0 1 0 483337031 186671104 44805 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45574 44805 603 41 0 45533 0
vsize: 182296
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 1.04 1.01 0.93 1/54 29126
Raw data (stat): 29073 (minisat+) Z 29072 30701 30700 0 -1 12 45476 0 0 0 119895 129 0 0 25 0 1 0 483337031 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.11
CPU time (s): 1200.25
CPU user time (s): 1198.95
CPU system time (s): 1.2928
CPU usage (%): 100.011
Max. virtual memory (Kb): 182296
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####