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-mod010.opb
MD5SUM	4f0cac14ed3568050c2c57bb69fdb664
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.14
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 17016

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc13 THE 2005-04-21 09:22:32 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12051 boxname=wulflinc13 idbench=927 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4f0cac14ed3568050c2c57bb69fdb664  /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-20-10-mod010.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-20-10-mod010.opb /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-20-10-mod010.opb
IDLAUNCH: 12051
/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:        596416 kB
Buffers:         34444 kB
Cached:         381268 kB
SwapCached:        176 kB
Active:         185696 kB
Inactive:       232788 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        596164 kB
SwapTotal:     2097136 kB
SwapFree:      2096860 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6812 kB
Slab:            14088 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 09:42:34 (client local time) WITH STATUS 0 IN 1200.33 SECONDS
stats: 12051 7 1200.33 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 |  112641   342501 |   37547       0        0     nan |  0.000 % |
c |       100 |  112566   342248 |   41301      93      747     8.0 |  0.739 % |
c |       251 |  112566   342248 |   45431     244     4453    18.2 |  0.739 % |
c |       477 |  112566   342248 |   49975     470    15059    32.0 |  0.739 % |
c |       819 |  112566   342248 |   54972     812    37441    46.1 |  0.739 % |
c |      1331 |  112566   342248 |   60469    1324    71852    54.3 |  0.739 % |
c |      2095 |  112566   342248 |   66516    2088   201139    96.3 |  0.739 % |
c |      3235 |  112566   342248 |   73168    3228   326074   101.0 |  0.739 % |
c |      4943 |  112537   342164 |   80485    4914   477218    97.1 |  0.751 % |
c |      7505 |  112537   342164 |   88533    7476  1210959   162.0 |  0.751 % |
c |     11350 |  112537   342164 |   97387   11321  1873735   165.5 |  0.751 % |
c |     17116 |  112537   342164 |  107125   17087  3521450   206.1 |  0.751 % |
c |     25767 |  112512   342081 |  117838   25734  4545362   176.6 |  0.767 % |
c |     38741 |  112460   341924 |  129622   38597  6644314   172.1 |  0.783 % |
c |     58202 |  112449   341881 |  142584   58057 12905884   222.3 |  0.791 % |
c |     87396 |  112356   341607 |  156843   87217 24567040   281.7 |  0.823 % |
c |    131185 |  112327   341502 |  172527  131001 48087197   367.1 |  0.840 % |
#### 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.44 0.76 0.84 2/54 4091
Raw data (stat): 4091 (runsolver) R 4090 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 485748265 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.52 0.77 0.84 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 5613 0 0 0 984 14 0 0 25 0 1 0 485748265 23097344 4944 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5639 4944 603 41 0 5598 0
vsize: 22556
[startup+20.0012 s]
Raw data (loadavg): 0.60 0.78 0.85 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 6136 0 0 0 1983 15 0 0 25 0 1 0 485748265 25251840 5467 4294967295 134512640 134672761 3221224544 3221223728 134559116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6165 5467 603 41 0 6124 0
vsize: 24660
[startup+30.0023 s]
Raw data (loadavg): 0.66 0.79 0.85 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 6703 0 0 0 2981 17 0 0 25 0 1 0 485748265 27545600 6034 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6725 6034 603 41 0 6684 0
vsize: 26900
[startup+40.0029 s]
Raw data (loadavg): 0.71 0.79 0.85 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 7357 0 0 0 3980 18 0 0 25 0 1 0 485748265 30248960 6688 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7385 6688 603 41 0 7344 0
vsize: 29540
[startup+50.0041 s]
Raw data (loadavg): 0.75 0.80 0.85 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 8136 0 0 0 4977 22 0 0 25 0 1 0 485748265 33349632 7467 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8142 7467 603 41 0 8101 0
vsize: 32568
[startup+60.0043 s]
Raw data (loadavg): 0.79 0.80 0.85 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 8816 0 0 0 5975 23 0 0 25 0 1 0 485748265 36188160 8147 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8835 8147 603 41 0 8794 0
vsize: 35340
[startup+70.0049 s]
Raw data (loadavg): 0.82 0.81 0.85 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 9451 0 0 0 6973 26 0 0 25 0 1 0 485748265 38772736 8782 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9466 8782 603 41 0 9425 0
vsize: 37864
[startup+80.0051 s]
Raw data (loadavg): 0.85 0.82 0.85 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 9914 0 0 0 7972 27 0 0 25 0 1 0 485748265 40652800 9245 4294967295 134512640 134672761 3221224544 3221223744 134557922 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9925 9245 603 41 0 9884 0
vsize: 39700
[startup+90.0052 s]
Raw data (loadavg): 0.87 0.82 0.85 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 10332 0 0 0 8971 28 0 0 25 0 1 0 485748265 42401792 9663 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10352 9663 603 41 0 10311 0
vsize: 41408
[startup+100.006 s]
Raw data (loadavg): 0.89 0.83 0.85 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 10890 0 0 0 9970 29 0 0 25 0 1 0 485748265 44695552 10221 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10912 10221 603 41 0 10871 0
vsize: 43648
[startup+110.006 s]
Raw data (loadavg): 0.91 0.83 0.85 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 11387 0 0 0 10969 31 0 0 25 0 1 0 485748265 46714880 10718 4294967295 134512640 134672761 3221224544 3221223648 134560008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11405 10718 603 41 0 11364 0
vsize: 45620
[startup+120.006 s]
Raw data (loadavg): 0.92 0.84 0.85 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 11877 0 0 0 11967 32 0 0 25 0 1 0 485748265 48857088 11208 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11928 11208 603 41 0 11887 0
vsize: 47712
[startup+130.007 s]
Raw data (loadavg): 0.93 0.84 0.86 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 12430 0 0 0 12966 34 0 0 25 0 1 0 485748265 51138560 11761 4294967295 134512640 134672761 3221224544 3221223648 134560279 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12485 11761 603 41 0 12444 0
vsize: 49940
[startup+140.007 s]
Raw data (loadavg): 0.94 0.85 0.86 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 12992 0 0 0 13964 36 0 0 25 0 1 0 485748265 53305344 12323 4294967295 134512640 134672761 3221224544 3221223712 134560785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13014 12323 603 41 0 12973 0
vsize: 52056
[startup+150.008 s]
Raw data (loadavg): 0.95 0.85 0.86 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 13678 0 0 0 14962 38 0 0 25 0 1 0 485748265 56152064 13009 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13709 13009 603 41 0 13668 0
vsize: 54836
[startup+160.008 s]
Raw data (loadavg): 0.96 0.86 0.86 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 14249 0 0 0 15960 40 0 0 25 0 1 0 485748265 58445824 13580 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14269 13580 603 41 0 14228 0
vsize: 57076
[startup+170.008 s]
Raw data (loadavg): 0.96 0.86 0.86 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 14827 0 0 0 16958 42 0 0 25 0 1 0 485748265 60829696 14158 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14851 14158 603 41 0 14810 0
vsize: 59404
[startup+180.008 s]
Raw data (loadavg): 0.97 0.86 0.86 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 15385 0 0 0 17956 44 0 0 25 0 1 0 485748265 63111168 14716 4294967295 134512640 134672761 3221224544 3221223648 134560393 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15408 14716 603 41 0 15367 0
vsize: 61632
[startup+190.009 s]
Raw data (loadavg): 0.97 0.87 0.86 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 16148 0 0 0 18954 46 0 0 25 0 1 0 485748265 66318336 15479 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16191 15479 603 41 0 16150 0
vsize: 64764
[startup+200.01 s]
Raw data (loadavg): 0.98 0.87 0.86 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 16922 0 0 0 19952 49 0 0 25 0 1 0 485748265 69369856 16253 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16936 16253 603 41 0 16895 0
vsize: 67744
[startup+210.01 s]
Raw data (loadavg): 0.98 0.88 0.86 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 17549 0 0 0 20950 50 0 0 25 0 1 0 485748265 71929856 16880 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17561 16880 603 41 0 17520 0
vsize: 70244
[startup+220.01 s]
Raw data (loadavg): 0.98 0.88 0.86 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 18113 0 0 0 21949 52 0 0 25 0 1 0 485748265 74346496 17444 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18151 17444 603 41 0 18110 0
vsize: 72604
[startup+230.011 s]
Raw data (loadavg): 0.98 0.88 0.87 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 18689 0 0 0 22947 54 0 0 25 0 1 0 485748265 76652544 18020 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18714 18020 603 41 0 18673 0
vsize: 74856
[startup+240.01 s]
Raw data (loadavg): 0.99 0.89 0.87 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 19121 0 0 0 23945 55 0 0 25 0 1 0 485748265 78405632 18452 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19142 18452 603 41 0 19101 0
vsize: 76568
[startup+250.011 s]
Raw data (loadavg): 0.99 0.89 0.87 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 19794 0 0 0 24944 57 0 0 25 0 1 0 485748265 81096704 19125 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19799 19125 603 41 0 19758 0
vsize: 79196
[startup+260.012 s]
Raw data (loadavg): 0.99 0.89 0.87 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 20584 0 0 0 25942 59 0 0 25 0 1 0 485748265 84357120 19915 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20595 19915 603 41 0 20554 0
vsize: 82380
[startup+270.011 s]
Raw data (loadavg): 0.99 0.90 0.87 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 21378 0 0 0 26941 61 0 0 25 0 1 0 485748265 87678976 20709 4294967295 134512640 134672761 3221224544 3221223648 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21406 20709 603 41 0 21365 0
vsize: 85624
[startup+280.011 s]
Raw data (loadavg): 0.99 0.90 0.87 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 22057 0 0 0 27939 62 0 0 25 0 1 0 485748265 90382336 21388 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22066 21388 603 41 0 22025 0
vsize: 88264
[startup+290.011 s]
Raw data (loadavg): 0.99 0.90 0.87 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 22802 0 0 0 28938 64 0 0 25 0 1 0 485748265 93745152 22133 4294967295 134512640 134672761 3221224544 3221223680 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22887 22133 603 41 0 22846 0
vsize: 91548
[startup+300.012 s]
Raw data (loadavg): 0.99 0.90 0.87 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 23496 0 0 0 29936 66 0 0 25 0 1 0 485748265 96583680 22827 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23580 22827 603 41 0 23539 0
vsize: 94320
[startup+310.012 s]
Raw data (loadavg): 0.99 0.91 0.87 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 24040 0 0 0 30934 67 0 0 25 0 1 0 485748265 98725888 23371 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24103 23371 603 41 0 24062 0
vsize: 96412
[startup+320.011 s]
Raw data (loadavg): 0.99 0.91 0.87 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 24811 0 0 0 31933 69 0 0 25 0 1 0 485748265 101982208 24142 4294967295 134512640 134672761 3221224544 3221223416 1075755419 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24898 24143 603 41 0 24857 0
vsize: 99592
[startup+330.012 s]
Raw data (loadavg): 0.99 0.91 0.88 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 25439 0 0 0 32932 70 0 0 25 0 1 0 485748265 104419328 24770 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25493 24770 603 41 0 25452 0
vsize: 101972
[startup+340.012 s]
Raw data (loadavg): 0.99 0.91 0.88 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 26047 0 0 0 33929 73 0 0 25 0 1 0 485748265 106971136 25378 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26116 25378 603 41 0 26075 0
vsize: 104464
[startup+350.012 s]
Raw data (loadavg): 0.99 0.92 0.88 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 26599 0 0 0 34928 74 0 0 25 0 1 0 485748265 109264896 25930 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26676 25930 603 41 0 26635 0
vsize: 106704
[startup+360.012 s]
Raw data (loadavg): 0.99 0.92 0.88 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 27115 0 0 0 35927 75 0 0 25 0 1 0 485748265 111296512 26446 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27172 26446 603 41 0 27131 0
vsize: 108688
[startup+370.012 s]
Raw data (loadavg): 0.99 0.92 0.88 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 27638 0 0 0 36926 77 0 0 25 0 1 0 485748265 113451008 26969 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27698 26969 603 41 0 27657 0
vsize: 110792
[startup+380.013 s]
Raw data (loadavg): 0.99 0.92 0.88 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 28050 0 0 0 37925 78 0 0 25 0 1 0 485748265 115204096 27381 4294967295 134512640 134672761 3221224544 3221223680 134560619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28126 27381 603 41 0 28085 0
vsize: 112504
[startup+390.012 s]
Raw data (loadavg): 0.99 0.92 0.88 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 28654 0 0 0 38923 80 0 0 25 0 1 0 485748265 117641216 27985 4294967295 134512640 134672761 3221224544 3221223648 134560005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28721 27985 603 41 0 28680 0
vsize: 114884
[startup+400.014 s]
Raw data (loadavg): 0.99 0.93 0.88 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 29361 0 0 0 39921 82 0 0 25 0 1 0 485748265 120467456 28692 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29411 28692 603 41 0 29370 0
vsize: 117644
[startup+410.013 s]
Raw data (loadavg): 0.99 0.93 0.88 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 30002 0 0 0 40919 85 0 0 25 0 1 0 485748265 123158528 29333 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30068 29333 603 41 0 30027 0
vsize: 120272
[startup+420.012 s]
Raw data (loadavg): 0.99 0.93 0.88 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 30703 0 0 0 41918 86 0 0 25 0 1 0 485748265 125988864 30034 4294967295 134512640 134672761 3221224544 3221223648 134560399 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30759 30034 603 41 0 30718 0
vsize: 123036
[startup+430.014 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 31192 0 0 0 42916 88 0 0 25 0 1 0 485748265 128000000 30523 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31250 30523 603 41 0 31209 0
vsize: 125000
[startup+440.013 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 31825 0 0 0 43915 89 0 0 25 0 1 0 485748265 130572288 31156 4294967295 134512640 134672761 3221224544 3221223728 134558423 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31878 31156 603 41 0 31837 0
vsize: 127512
[startup+450.014 s]
Raw data (loadavg): 0.99 0.94 0.89 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 32176 0 0 0 44913 91 0 0 25 0 1 0 485748265 132059136 31507 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32241 31507 603 41 0 32200 0
vsize: 128964
[startup+460.013 s]
Raw data (loadavg): 0.99 0.94 0.89 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 32546 0 0 0 45912 92 0 0 25 0 1 0 485748265 133541888 31877 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32603 31877 603 41 0 32562 0
vsize: 130412
[startup+470.013 s]
Raw data (loadavg): 0.99 0.94 0.89 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 33173 0 0 0 46911 94 0 0 25 0 1 0 485748265 136097792 32504 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33227 32504 603 41 0 33186 0
vsize: 132908
[startup+480.013 s]
Raw data (loadavg): 1.07 0.96 0.90 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 33763 0 0 0 47910 95 0 0 25 0 1 0 485748265 138514432 33094 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33817 33094 603 41 0 33776 0
vsize: 135268
[startup+490.013 s]
Raw data (loadavg): 1.06 0.96 0.90 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 34349 0 0 0 48909 96 0 0 25 0 1 0 485748265 140922880 33680 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34405 33680 603 41 0 34364 0
vsize: 137620
[startup+500.014 s]
Raw data (loadavg): 1.05 0.96 0.90 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 34943 0 0 0 49908 97 0 0 25 0 1 0 485748265 143347712 34274 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34997 34274 603 41 0 34956 0
vsize: 139988
[startup+510.014 s]
Raw data (loadavg): 1.04 0.96 0.90 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 35679 0 0 0 50907 99 0 0 25 0 1 0 485748265 146321408 35010 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35723 35010 603 41 0 35682 0
vsize: 142892
[startup+520.013 s]
Raw data (loadavg): 1.03 0.96 0.90 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 36325 0 0 0 51905 100 0 0 25 0 1 0 485748265 148889600 35656 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36350 35656 603 41 0 36309 0
vsize: 145400
[startup+530.014 s]
Raw data (loadavg): 1.03 0.96 0.90 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 37028 0 0 0 52904 101 0 0 25 0 1 0 485748265 151789568 36359 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37058 36359 603 41 0 37017 0
vsize: 148232
[startup+540.014 s]
Raw data (loadavg): 1.02 0.96 0.90 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 37555 0 0 0 53903 103 0 0 25 0 1 0 485748265 153927680 36886 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37580 36886 603 41 0 37539 0
vsize: 150320
[startup+550.014 s]
Raw data (loadavg): 1.02 0.97 0.90 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 37997 0 0 0 54901 105 0 0 25 0 1 0 485748265 155824128 37328 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38043 37328 603 41 0 38002 0
vsize: 152172
[startup+560.014 s]
Raw data (loadavg): 1.02 0.97 0.90 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 38477 0 0 0 55900 106 0 0 25 0 1 0 485748265 157704192 37808 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38502 37808 603 41 0 38461 0
vsize: 154008
[startup+570.014 s]
Raw data (loadavg): 1.01 0.97 0.90 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 38815 0 0 0 56899 107 0 0 25 0 1 0 485748265 159059968 38146 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38833 38146 603 41 0 38792 0
vsize: 155332
[startup+580.014 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 39463 0 0 0 57898 109 0 0 25 0 1 0 485748265 161738752 38794 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39487 38794 603 41 0 39446 0
vsize: 157948
[startup+590.014 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 40079 0 0 0 58896 110 0 0 25 0 1 0 485748265 164265984 39410 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40104 39410 603 41 0 40063 0
vsize: 160416
[startup+600.015 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 40705 0 0 0 59896 111 0 0 25 0 1 0 485748265 166817792 40036 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40727 40036 603 41 0 40686 0
vsize: 162908
[startup+610.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 41321 0 0 0 60894 113 0 0 25 0 1 0 485748265 169353216 40652 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41346 40652 603 41 0 41305 0
vsize: 165384
[startup+620.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 41955 0 0 0 61893 114 0 0 25 0 1 0 485748265 172027904 41286 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41999 41287 603 41 0 41958 0
vsize: 167996
[startup+630.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 42467 0 0 0 62892 116 0 0 25 0 1 0 485748265 174039040 41798 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42490 41798 603 41 0 42449 0
vsize: 169960
[startup+640.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 43157 0 0 0 63890 117 0 0 25 0 1 0 485748265 176861184 42488 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43179 42488 603 41 0 43138 0
vsize: 172716
[startup+650.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 43869 0 0 0 64889 119 0 0 25 0 1 0 485748265 179822592 43200 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43902 43200 603 41 0 43861 0
vsize: 175608
[startup+660.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 44600 0 0 0 65888 121 0 0 25 0 1 0 485748265 182784000 43931 4294967295 134512640 134672761 3221224544 3221223728 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44625 43932 603 41 0 44584 0
vsize: 178500
[startup+670.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 45274 0 0 0 66886 122 0 0 25 0 1 0 485748265 185483264 44605 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45284 44605 603 41 0 45243 0
vsize: 181136
[startup+680.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 45929 0 0 0 67885 124 0 0 25 0 1 0 485748265 188198912 45260 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45947 45260 603 41 0 45906 0
vsize: 183788
[startup+690.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 46577 0 0 0 68883 126 0 0 25 0 1 0 485748265 190885888 45908 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46603 45908 603 41 0 46562 0
vsize: 186412
[startup+700.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 47187 0 0 0 69882 127 0 0 25 0 1 0 485748265 193306624 46518 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47194 46518 603 41 0 47153 0
vsize: 188776
[startup+710.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 47791 0 0 0 70880 130 0 0 25 0 1 0 485748265 195878912 47122 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47822 47122 603 41 0 47781 0
vsize: 191288
[startup+720.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 48423 0 0 0 71878 131 0 0 25 0 1 0 485748265 198438912 47754 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48447 47754 603 41 0 48406 0
vsize: 193788
[startup+730.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 49073 0 0 0 72877 133 0 0 25 0 1 0 485748265 201150464 48404 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49109 48404 603 41 0 49068 0
vsize: 196436
[startup+740.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 49689 0 0 0 73875 135 0 0 25 0 1 0 485748265 203595776 49020 4294967295 134512640 134672761 3221224544 3221223648 134560381 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49706 49020 603 41 0 49665 0
vsize: 198824
[startup+750.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 50311 0 0 0 74874 136 0 0 25 0 1 0 485748265 206131200 49642 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50325 49642 603 41 0 50284 0
vsize: 201300
[startup+760.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 50912 0 0 0 75872 138 0 0 25 0 1 0 485748265 208588800 50243 4294967295 134512640 134672761 3221224544 3221223648 134560134 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50925 50243 603 41 0 50884 0
vsize: 203700
[startup+770.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 51502 0 0 0 76871 139 0 0 25 0 1 0 485748265 211001344 50833 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51514 50833 603 41 0 51473 0
vsize: 206056
[startup+780.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 52135 0 0 0 77871 140 0 0 25 0 1 0 485748265 213708800 51466 4294967295 134512640 134672761 3221224544 3221223648 134559943 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52175 51466 603 41 0 52134 0
vsize: 208700
[startup+790.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 52698 0 0 0 78870 141 0 0 25 0 1 0 485748265 216010752 52029 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52737 52029 603 41 0 52696 0
vsize: 210948
[startup+800.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 53318 0 0 0 79868 143 0 0 25 0 1 0 485748265 218439680 52649 4294967295 134512640 134672761 3221224544 3221223648 134559933 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53330 52649 603 41 0 53289 0
vsize: 213320
[startup+810.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 53899 0 0 0 80867 144 0 0 25 0 1 0 485748265 220864512 53230 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53922 53230 603 41 0 53881 0
vsize: 215688
[startup+820.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 54500 0 0 0 81866 146 0 0 25 0 1 0 485748265 223817728 53831 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54643 53831 603 41 0 54602 0
vsize: 218572
[startup+830.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 55180 0 0 0 82863 149 0 0 25 0 1 0 485748265 226594816 54511 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55321 54511 603 41 0 55280 0
vsize: 221284
[startup+840.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 55666 0 0 0 83861 150 0 0 25 0 1 0 485748265 228610048 54997 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55813 54997 603 41 0 55772 0
vsize: 223252
[startup+850.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 56053 0 0 0 84860 152 0 0 25 0 1 0 485748265 230215680 55384 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56205 55384 603 41 0 56164 0
vsize: 224820
[startup+860.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 56326 0 0 0 85859 152 0 0 25 0 1 0 485748265 231280640 55657 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56465 55657 603 41 0 56424 0
vsize: 225860
[startup+870.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 56770 0 0 0 86858 153 0 0 25 0 1 0 485748265 233164800 56101 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56925 56101 603 41 0 56884 0
vsize: 227700
[startup+880.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 57392 0 0 0 87857 155 0 0 25 0 1 0 485748265 235732992 56723 4294967295 134512640 134672761 3221224544 3221223648 134559853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57552 56723 603 41 0 57511 0
vsize: 230208
[startup+890.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 58076 0 0 0 88856 157 0 0 25 0 1 0 485748265 238411776 57407 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58206 57407 603 41 0 58165 0
vsize: 232824
[startup+900.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 58596 0 0 0 89855 158 0 0 25 0 1 0 485748265 240582656 57927 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58736 57927 603 41 0 58695 0
vsize: 234944
[startup+910.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 58845 0 0 0 90855 158 0 0 25 0 1 0 485748265 241659904 58176 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58999 58176 603 41 0 58958 0
vsize: 235996
[startup+920.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 59334 0 0 0 91854 159 0 0 25 0 1 0 485748265 243679232 58665 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59492 58665 603 41 0 59451 0
vsize: 237968
[startup+930.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 59417 0 0 0 92854 159 0 0 25 0 1 0 485748265 243949568 58748 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59558 58748 603 41 0 59517 0
vsize: 238232
[startup+940.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 59944 0 0 0 93853 160 0 0 25 0 1 0 485748265 246132736 59275 4294967295 134512640 134672761 3221224544 3221223648 134560506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60091 59275 603 41 0 60050 0
vsize: 240364
[startup+950.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 60325 0 0 0 94853 160 0 0 25 0 1 0 485748265 247615488 59656 4294967295 134512640 134672761 3221224544 3221223648 134560034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60453 59656 603 41 0 60412 0
vsize: 241812
[startup+960.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 60792 0 0 0 95852 162 0 0 25 0 1 0 485748265 249503744 60123 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60914 60123 603 41 0 60873 0
vsize: 243656
[startup+970.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 61417 0 0 0 96851 163 0 0 25 0 1 0 485748265 252182528 60748 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61568 60748 603 41 0 61527 0
vsize: 246272
[startup+980.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 61997 0 0 0 97850 165 0 0 25 0 1 0 485748265 254476288 61328 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62128 61328 603 41 0 62087 0
vsize: 248512
[startup+990.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 62457 0 0 0 98848 166 0 0 25 0 1 0 485748265 256364544 61788 4294967295 134512640 134672761 3221224544 3221223648 134560036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62589 61788 603 41 0 62548 0
vsize: 250356
[startup+1000.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 62836 0 0 0 99847 168 0 0 25 0 1 0 485748265 257982464 62167 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62984 62167 603 41 0 62943 0
vsize: 251936
[startup+1010.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 63228 0 0 0 100846 169 0 0 25 0 1 0 485748265 259448832 62559 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63342 62559 603 41 0 63301 0
vsize: 253368
[startup+1020.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 63733 0 0 0 101845 170 0 0 25 0 1 0 485748265 261582848 63064 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63863 63064 603 41 0 63822 0
vsize: 255452
[startup+1030.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 64319 0 0 0 102843 172 0 0 25 0 1 0 485748265 263938048 63650 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64438 63650 603 41 0 64397 0
vsize: 257752
[startup+1040.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 64908 0 0 0 103842 174 0 0 25 0 1 0 485748265 266452992 64239 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65052 64239 603 41 0 65011 0
vsize: 260208
[startup+1050.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 65450 0 0 0 104841 174 0 0 25 0 1 0 485748265 268582912 64781 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65572 64781 603 41 0 65531 0
vsize: 262288
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 65778 0 0 0 105841 175 0 0 25 0 1 0 485748265 269901824 65109 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65894 65109 603 41 0 65853 0
vsize: 263576
[startup+1070.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 65904 0 0 0 106841 175 0 0 25 0 1 0 485748265 270438400 65235 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66025 65235 603 41 0 65984 0
vsize: 264100
[startup+1080.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 66414 0 0 0 107840 176 0 0 25 0 1 0 485748265 272592896 65745 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66551 65745 603 41 0 66510 0
vsize: 266204
[startup+1090.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 66942 0 0 0 108839 177 0 0 25 0 1 0 485748265 274743296 66273 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67076 66273 603 41 0 67035 0
vsize: 268304
[startup+1100.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 67445 0 0 0 109838 179 0 0 25 0 1 0 485748265 276770816 66776 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67571 66776 603 41 0 67530 0
vsize: 270284
[startup+1110.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 67916 0 0 0 110837 180 0 0 25 0 1 0 485748265 278659072 67247 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68032 67247 603 41 0 67991 0
vsize: 272128
[startup+1120.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 68232 0 0 0 111836 180 0 0 25 0 1 0 485748265 280014848 67563 4294967295 134512640 134672761 3221224544 3221223648 134560051 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68363 67563 603 41 0 68322 0
vsize: 273452
[startup+1130.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 68775 0 0 0 112835 182 0 0 25 0 1 0 485748265 282148864 68106 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68884 68106 603 41 0 68843 0
vsize: 275536
[startup+1140.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 69254 0 0 0 113834 183 0 0 25 0 1 0 485748265 284147712 68585 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69372 68585 603 41 0 69331 0
vsize: 277488
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 69763 0 0 0 114832 185 0 0 25 0 1 0 485748265 286289920 69094 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69895 69094 603 41 0 69854 0
vsize: 279580
[startup+1160.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 70209 0 0 0 115832 186 0 0 25 0 1 0 485748265 288030720 69540 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70320 69540 603 41 0 70279 0
vsize: 281280
[startup+1170.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 70602 0 0 0 116831 187 0 0 25 0 1 0 485748265 289648640 69933 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70715 69933 603 41 0 70674 0
vsize: 282860
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 70835 0 0 0 117831 187 0 0 25 0 1 0 485748265 290598912 70166 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70947 70166 603 41 0 70906 0
vsize: 283788
[startup+1190.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 71108 0 0 0 118830 188 0 0 25 0 1 0 485748265 291672064 70439 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71209 70439 603 41 0 71168 0
vsize: 284836
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4091
Raw data (stat): 4091 (minisat+) R 4090 30701 30700 0 -1 0 71239 0 0 0 119830 189 0 0 25 0 1 0 485748265 292212736 70570 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71341 70570 603 41 0 71300 0
vsize: 285364
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.16 s]
Raw data (loadavg): 1.00 0.97 0.91 1/54 4091
Raw data (stat): 4091 (minisat+) Z 4090 30701 30700 0 -1 12 71241 0 0 0 119830 202 0 0 25 0 1 0 485748265 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.16
CPU time (s): 1200.33
CPU user time (s): 1198.3
CPU system time (s): 2.02269
CPU usage (%): 100.014
Max. virtual memory (Kb): 285364
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####