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 15045

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-04-21 02:40:30 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18641 boxname=wulflinc5 idbench=1434 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ef7064a9be2b712276f7b600af28e2b0  /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-mod010.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-mod010.opb /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-mod010.opb
IDLAUNCH: 18641
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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.007
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        368176 kB
Buffers:         39516 kB
Cached:         601356 kB
SwapCached:       2272 kB
Active:         236156 kB
Inactive:       409864 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        367924 kB
SwapTotal:     2097136 kB
SwapFree:      2094864 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6940 kB
Slab:            14736 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:32 (client local time) WITH STATUS 0 IN 1200.21 SECONDS
stats: 18641 7 1200.21 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]---> BDD-cost:122663
c ---[   0]---> BDD-cost:  751
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  407646  1200847 |  135882       0        0     nan |  0.000 % |
c |       102 |  407646  1200847 |  149470     102     8289    81.3 |  0.103 % |
c |       255 |  407646  1200847 |  164417     255    14708    57.7 |  0.103 % |
c |       481 |  407646  1200847 |  180858     481   132399   275.3 |  0.103 % |
c |       820 |  407646  1200847 |  198944     820   355047   433.0 |  0.103 % |
c |      1327 |  407646  1200847 |  218839    1327   541014   407.7 |  0.103 % |
c |      2087 |  407646  1200847 |  240723    2087   956748   458.4 |  0.103 % |
c |      3228 |  407646  1200847 |  264795    3228  1798377   557.1 |  0.103 % |
c |      4939 |  407646  1200847 |  291275    4939  3812069   771.8 |  0.103 % |
c |      7501 |  407646  1200847 |  320402    7501  6883879   917.7 |  0.103 % |
#### 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.72 0.91 0.89 2/54 14802
Raw data (stat): 14802 (runsolver) R 14801 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 483331904 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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+9.99993 s]
Raw data (loadavg): 0.76 0.91 0.89 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 13521 0 0 0 969 30 0 0 25 0 1 0 483331904 62861312 12547 4294967295 134512640 134672761 3221224544 3221223844 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15347 12547 603 41 0 15306 0
vsize: 61388
[startup+20.0003 s]
Raw data (loadavg): 0.80 0.91 0.89 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 13748 0 0 0 1968 30 0 0 25 0 1 0 483331904 63410176 12774 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15481 12774 603 41 0 15440 0
vsize: 61924
[startup+30.001 s]
Raw data (loadavg): 0.83 0.91 0.89 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 13832 0 0 0 2968 31 0 0 25 0 1 0 483331904 63688704 12858 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15549 12858 603 41 0 15508 0
vsize: 62196
[startup+40.0018 s]
Raw data (loadavg): 0.86 0.92 0.89 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 13961 0 0 0 3967 31 0 0 25 0 1 0 483331904 64270336 12987 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15691 12987 603 41 0 15650 0
vsize: 62764
[startup+50.003 s]
Raw data (loadavg): 0.88 0.92 0.89 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 14022 0 0 0 4967 32 0 0 25 0 1 0 483331904 64548864 13048 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15759 13048 603 41 0 15718 0
vsize: 63036
[startup+60.0022 s]
Raw data (loadavg): 0.90 0.92 0.90 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 14050 0 0 0 5967 32 0 0 25 0 1 0 483331904 64532480 13076 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15755 13076 603 41 0 15714 0
vsize: 63020
[startup+70.003 s]
Raw data (loadavg): 0.91 0.92 0.90 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 14184 0 0 0 6966 32 0 0 25 0 1 0 483331904 65069056 13210 4294967295 134512640 134672761 3221224544 3221223648 134560148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15886 13210 603 41 0 15845 0
vsize: 63544
[startup+80.0031 s]
Raw data (loadavg): 0.92 0.92 0.90 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 14256 0 0 0 7966 33 0 0 25 0 1 0 483331904 65482752 13282 4294967295 134512640 134672761 3221224544 3221223648 134559995 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15987 13282 603 41 0 15946 0
vsize: 63948
[startup+90.0035 s]
Raw data (loadavg): 0.94 0.93 0.90 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 14351 0 0 0 8966 33 0 0 25 0 1 0 483331904 65880064 13377 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16084 13377 603 41 0 16043 0
vsize: 64336
[startup+100.003 s]
Raw data (loadavg): 0.94 0.93 0.90 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 14507 0 0 0 9966 33 0 0 25 0 1 0 483331904 66519040 13533 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16240 13533 603 41 0 16199 0
vsize: 64960
[startup+110.003 s]
Raw data (loadavg): 0.95 0.93 0.90 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 14539 0 0 0 10966 33 0 0 25 0 1 0 483331904 66650112 13565 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16272 13565 603 41 0 16231 0
vsize: 65088
[startup+120.004 s]
Raw data (loadavg): 0.96 0.93 0.90 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 14649 0 0 0 11966 34 0 0 25 0 1 0 483331904 67158016 13675 4294967295 134512640 134672761 3221224544 3221223648 134559866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16396 13675 603 41 0 16355 0
vsize: 65584
[startup+130.004 s]
Raw data (loadavg): 0.97 0.93 0.90 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 14772 0 0 0 12966 34 0 0 25 0 1 0 483331904 67690496 13798 4294967295 134512640 134672761 3221224544 3221223648 134560313 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16526 13798 603 41 0 16485 0
vsize: 66104
[startup+140.005 s]
Raw data (loadavg): 0.97 0.94 0.90 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 14814 0 0 0 13966 34 0 0 25 0 1 0 483331904 67829760 13840 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16560 13840 603 41 0 16519 0
vsize: 66240
[startup+150.005 s]
Raw data (loadavg): 0.97 0.94 0.90 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 14884 0 0 0 14966 34 0 0 25 0 1 0 483331904 68104192 13910 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16627 13910 603 41 0 16586 0
vsize: 66508
[startup+160.005 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 14983 0 0 0 15966 34 0 0 25 0 1 0 483331904 68509696 14009 4294967295 134512640 134672761 3221224544 3221223712 134560968 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16726 14009 603 41 0 16685 0
vsize: 66904
[startup+170.006 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 15039 0 0 0 16966 34 0 0 25 0 1 0 483331904 68775936 14065 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16791 14065 603 41 0 16750 0
vsize: 67164
[startup+180.005 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 15060 0 0 0 17966 34 0 0 25 0 1 0 483331904 68775936 14086 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16791 14086 603 41 0 16750 0
vsize: 67164
[startup+190.005 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 15080 0 0 0 18967 34 0 0 25 0 1 0 483331904 68911104 14106 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16824 14106 603 41 0 16783 0
vsize: 67296
[startup+200.005 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 15099 0 0 0 19967 34 0 0 25 0 1 0 483331904 69050368 14125 4294967295 134512640 134672761 3221224544 3221223648 134560194 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16858 14125 603 41 0 16817 0
vsize: 67432
[startup+210.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 15175 0 0 0 20967 34 0 0 25 0 1 0 483331904 69320704 14201 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16924 14201 603 41 0 16883 0
vsize: 67696
[startup+220.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 15239 0 0 0 21967 35 0 0 25 0 1 0 483331904 69595136 14265 4294967295 134512640 134672761 3221224544 3221223648 134560039 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16991 14265 603 41 0 16950 0
vsize: 67964
[startup+230.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 15256 0 0 0 22967 35 0 0 25 0 1 0 483331904 69595136 14282 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16991 14282 603 41 0 16950 0
vsize: 67964
[startup+240.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 15273 0 0 0 23967 35 0 0 25 0 1 0 483331904 69730304 14299 4294967295 134512640 134672761 3221224544 3221223648 134560008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17024 14299 603 41 0 16983 0
vsize: 68096
[startup+250.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 15283 0 0 0 24967 35 0 0 25 0 1 0 483331904 69730304 14309 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17024 14309 603 41 0 16983 0
vsize: 68096
[startup+260.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 15319 0 0 0 25967 35 0 0 25 0 1 0 483331904 69865472 14345 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17057 14345 603 41 0 17016 0
vsize: 68228
[startup+270.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 15361 0 0 0 26967 35 0 0 25 0 1 0 483331904 70000640 14387 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17090 14387 603 41 0 17049 0
vsize: 68360
[startup+280.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 15372 0 0 0 27967 35 0 0 25 0 1 0 483331904 70135808 14398 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17123 14398 603 41 0 17082 0
vsize: 68492
[startup+290.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 15387 0 0 0 28967 35 0 0 25 0 1 0 483331904 70135808 14413 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17123 14413 603 41 0 17082 0
vsize: 68492
[startup+300.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 15399 0 0 0 29968 35 0 0 25 0 1 0 483331904 70279168 14425 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17158 14425 603 41 0 17117 0
vsize: 68632
[startup+310.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 15410 0 0 0 30968 35 0 0 25 0 1 0 483331904 70279168 14436 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17158 14436 603 41 0 17117 0
vsize: 68632
[startup+320.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 15425 0 0 0 31968 35 0 0 25 0 1 0 483331904 70279168 14451 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17158 14451 603 41 0 17117 0
vsize: 68632
[startup+330.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 15440 0 0 0 32968 35 0 0 25 0 1 0 483331904 70422528 14466 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17193 14466 603 41 0 17152 0
vsize: 68772
[startup+340.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 15458 0 0 0 33968 35 0 0 25 0 1 0 483331904 70422528 14484 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17193 14484 603 41 0 17152 0
vsize: 68772
[startup+350.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 15468 0 0 0 34968 35 0 0 25 0 1 0 483331904 70529024 14494 4294967295 134512640 134672761 3221224544 3221223648 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17219 14494 603 41 0 17178 0
vsize: 68876
[startup+360.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 15740 0 0 0 35967 36 0 0 25 0 1 0 483331904 71598080 14766 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17480 14766 603 41 0 17439 0
vsize: 69920
[startup+370.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 15886 0 0 0 36967 36 0 0 25 0 1 0 483331904 72245248 14912 4294967295 134512640 134672761 3221224544 3221223648 134560506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17638 14912 603 41 0 17597 0
vsize: 70552
[startup+380.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 16120 0 0 0 37967 37 0 0 25 0 1 0 483331904 73179136 15146 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17866 15146 603 41 0 17825 0
vsize: 71464
[startup+390.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 16240 0 0 0 38967 37 0 0 25 0 1 0 483331904 73707520 15266 4294967295 134512640 134672761 3221224544 3221223648 134560252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17995 15266 603 41 0 17954 0
vsize: 71980
[startup+400.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 16309 0 0 0 39967 37 0 0 25 0 1 0 483331904 73961472 15335 4294967295 134512640 134672761 3221224544 3221223648 134560201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18057 15335 603 41 0 18016 0
vsize: 72228
[startup+410.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 16522 0 0 0 40966 38 0 0 25 0 1 0 483331904 74760192 15548 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18252 15548 603 41 0 18211 0
vsize: 73008
[startup+420.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 16560 0 0 0 41966 38 0 0 25 0 1 0 483331904 75034624 15586 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18319 15586 603 41 0 18278 0
vsize: 73276
[startup+430.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 16593 0 0 0 42966 38 0 0 25 0 1 0 483331904 75034624 15619 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18319 15619 603 41 0 18278 0
vsize: 73276
[startup+440.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 16628 0 0 0 43967 38 0 0 25 0 1 0 483331904 75304960 15654 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18385 15654 603 41 0 18344 0
vsize: 73540
[startup+450.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 16660 0 0 0 44967 38 0 0 25 0 1 0 483331904 75304960 15686 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18385 15686 603 41 0 18344 0
vsize: 73540
[startup+460.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 16724 0 0 0 45967 38 0 0 25 0 1 0 483331904 75583488 15750 4294967295 134512640 134672761 3221224544 3221223648 134560198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18453 15750 603 41 0 18412 0
vsize: 73812
[startup+470.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 16750 0 0 0 46967 38 0 0 25 0 1 0 483331904 75722752 15776 4294967295 134512640 134672761 3221224544 3221223648 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18487 15776 603 41 0 18446 0
vsize: 73948
[startup+480.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 16787 0 0 0 47967 38 0 0 25 0 1 0 483331904 75849728 15813 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18518 15813 603 41 0 18477 0
vsize: 74072
[startup+490.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 16808 0 0 0 48967 39 0 0 25 0 1 0 483331904 75988992 15834 4294967295 134512640 134672761 3221224544 3221223648 134560184 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18552 15834 603 41 0 18511 0
vsize: 74208
[startup+500.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 16834 0 0 0 49967 39 0 0 25 0 1 0 483331904 76128256 15860 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18586 15860 603 41 0 18545 0
vsize: 74344
[startup+510.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 16881 0 0 0 50967 39 0 0 25 0 1 0 483331904 76267520 15907 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18620 15907 603 41 0 18579 0
vsize: 74480
[startup+520.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 16956 0 0 0 51967 39 0 0 25 0 1 0 483331904 76517376 15982 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18681 15982 603 41 0 18640 0
vsize: 74724
[startup+530.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 17076 0 0 0 52967 39 0 0 25 0 1 0 483331904 77070336 16102 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18816 16102 603 41 0 18775 0
vsize: 75264
[startup+540.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 17266 0 0 0 53967 40 0 0 25 0 1 0 483331904 77864960 16292 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19010 16292 603 41 0 18969 0
vsize: 76040
[startup+550.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 17394 0 0 0 54966 40 0 0 25 0 1 0 483331904 78364672 16420 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19132 16420 603 41 0 19091 0
vsize: 76528
[startup+560.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 17525 0 0 0 55966 41 0 0 25 0 1 0 483331904 78897152 16551 4294967295 134512640 134672761 3221224544 3221223648 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19262 16551 603 41 0 19221 0
vsize: 77048
[startup+570.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 17702 0 0 0 56964 42 0 0 25 0 1 0 483331904 79577088 16728 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19428 16728 603 41 0 19387 0
vsize: 77712
[startup+580.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 17729 0 0 0 57964 42 0 0 25 0 1 0 483331904 79708160 16755 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19460 16755 603 41 0 19419 0
vsize: 77840
[startup+590.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 17845 0 0 0 58964 42 0 0 25 0 1 0 483331904 80232448 16871 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19588 16871 603 41 0 19547 0
vsize: 78352
[startup+600.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 18000 0 0 0 59964 42 0 0 25 0 1 0 483331904 80785408 17026 4294967295 134512640 134672761 3221224544 3221223648 134559953 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19723 17026 603 41 0 19682 0
vsize: 78892
[startup+610.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 18121 0 0 0 60964 43 0 0 25 0 1 0 483331904 81326080 17147 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19855 17147 603 41 0 19814 0
vsize: 79420
[startup+620.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 18210 0 0 0 61964 43 0 0 25 0 1 0 483331904 81731584 17236 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19954 17236 603 41 0 19913 0
vsize: 79816
[startup+630.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 18234 0 0 0 62964 43 0 0 25 0 1 0 483331904 81731584 17260 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19954 17260 603 41 0 19913 0
vsize: 79816
[startup+640.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 18242 0 0 0 63964 43 0 0 25 0 1 0 483331904 81866752 17268 4294967295 134512640 134672761 3221224544 3221223648 134560318 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19987 17268 603 41 0 19946 0
vsize: 79948
[startup+650.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 18457 0 0 0 64963 44 0 0 25 0 1 0 483331904 82681856 17483 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20186 17483 603 41 0 20145 0
vsize: 80744
[startup+660.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 18640 0 0 0 65963 44 0 0 25 0 1 0 483331904 83488768 17666 4294967295 134512640 134672761 3221224544 3221223708 134561028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20383 17666 603 41 0 20342 0
vsize: 81532
[startup+670.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 18780 0 0 0 66963 45 0 0 25 0 1 0 483331904 84017152 17806 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20512 17806 603 41 0 20471 0
vsize: 82048
[startup+680.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 19006 0 0 0 67962 46 0 0 25 0 1 0 483331904 84955136 18032 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20741 18032 603 41 0 20700 0
vsize: 82964
[startup+690.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 19131 0 0 0 68962 46 0 0 25 0 1 0 483331904 85499904 18157 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20874 18157 603 41 0 20833 0
vsize: 83496
[startup+700.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 19265 0 0 0 69962 46 0 0 25 0 1 0 483331904 86048768 18291 4294967295 134512640 134672761 3221224544 3221223648 134559866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21008 18291 603 41 0 20967 0
vsize: 84032
[startup+710.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 19311 0 0 0 70962 46 0 0 25 0 1 0 483331904 86183936 18337 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21041 18337 603 41 0 21000 0
vsize: 84164
[startup+720.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 19437 0 0 0 71962 47 0 0 25 0 1 0 483331904 86716416 18463 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21171 18463 603 41 0 21130 0
vsize: 84684
[startup+730.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 19511 0 0 0 72962 47 0 0 25 0 1 0 483331904 86974464 18537 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21234 18537 603 41 0 21193 0
vsize: 84936
[startup+740.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 19673 0 0 0 73962 47 0 0 25 0 1 0 483331904 87642112 18699 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21397 18699 603 41 0 21356 0
vsize: 85588
[startup+750.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 19834 0 0 0 74962 47 0 0 25 0 1 0 483331904 88285184 18860 4294967295 134512640 134672761 3221224544 3221223648 134560276 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21554 18860 603 41 0 21513 0
vsize: 86216
[startup+760.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 19935 0 0 0 75962 47 0 0 25 0 1 0 483331904 88694784 18961 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21654 18961 603 41 0 21613 0
vsize: 86616
[startup+770.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 20006 0 0 0 76962 48 0 0 25 0 1 0 483331904 88969216 19032 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21721 19032 603 41 0 21680 0
vsize: 86884
[startup+780.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 20134 0 0 0 77962 48 0 0 25 0 1 0 483331904 89481216 19160 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21846 19160 603 41 0 21805 0
vsize: 87384
[startup+790.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 20238 0 0 0 78962 48 0 0 25 0 1 0 483331904 90021888 19264 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21978 19264 603 41 0 21937 0
vsize: 87912
[startup+800.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 20285 0 0 0 79962 48 0 0 25 0 1 0 483331904 90157056 19311 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22011 19311 603 41 0 21970 0
vsize: 88044
[startup+810.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 20293 0 0 0 80962 48 0 0 25 0 1 0 483331904 90157056 19319 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22011 19319 603 41 0 21970 0
vsize: 88044
[startup+820.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 20333 0 0 0 81962 48 0 0 25 0 1 0 483331904 90292224 19359 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22044 19359 603 41 0 22003 0
vsize: 88176
[startup+830.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 20370 0 0 0 82962 48 0 0 25 0 1 0 483331904 90550272 19396 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22107 19396 603 41 0 22066 0
vsize: 88428
[startup+840.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 20409 0 0 0 83962 48 0 0 25 0 1 0 483331904 90689536 19435 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22141 19435 603 41 0 22100 0
vsize: 88564
[startup+850.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 20454 0 0 0 84962 48 0 0 25 0 1 0 483331904 90824704 19480 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22174 19480 603 41 0 22133 0
vsize: 88696
[startup+860.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 20503 0 0 0 85962 49 0 0 25 0 1 0 483331904 90963968 19529 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22208 19529 603 41 0 22167 0
vsize: 88832
[startup+870.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 20619 0 0 0 86962 49 0 0 25 0 1 0 483331904 91496448 19645 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22338 19645 603 41 0 22297 0
vsize: 89352
[startup+880.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 20729 0 0 0 87961 49 0 0 25 0 1 0 483331904 91906048 19755 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22438 19755 603 41 0 22397 0
vsize: 89752
[startup+890.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 20820 0 0 0 88961 50 0 0 25 0 1 0 483331904 92303360 19846 4294967295 134512640 134672761 3221224544 3221223648 134559835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22535 19846 603 41 0 22494 0
vsize: 90140
[startup+900.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 20886 0 0 0 89961 50 0 0 25 0 1 0 483331904 92561408 19912 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22598 19912 603 41 0 22557 0
vsize: 90392
[startup+910.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 20999 0 0 0 90961 50 0 0 25 0 1 0 483331904 93106176 20025 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22731 20025 603 41 0 22690 0
vsize: 90924
[startup+920.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 21166 0 0 0 91960 51 0 0 25 0 1 0 483331904 93794304 20192 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22899 20192 603 41 0 22858 0
vsize: 91596
[startup+930.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 21392 0 0 0 92960 51 0 0 25 0 1 0 483331904 94674944 20418 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23114 20418 603 41 0 23073 0
vsize: 92456
[startup+940.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 21550 0 0 0 93960 51 0 0 25 0 1 0 483331904 95346688 20576 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23278 20576 603 41 0 23237 0
vsize: 93112
[startup+950.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 21603 0 0 0 94960 51 0 0 25 0 1 0 483331904 95604736 20629 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23341 20629 603 41 0 23300 0
vsize: 93364
[startup+960.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 21758 0 0 0 95960 52 0 0 25 0 1 0 483331904 96149504 20784 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23474 20784 603 41 0 23433 0
vsize: 93896
[startup+970.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 21969 0 0 0 96960 52 0 0 25 0 1 0 483331904 97087488 20995 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23703 20995 603 41 0 23662 0
vsize: 94812
[startup+980.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 22139 0 0 0 97960 52 0 0 25 0 1 0 483331904 97771520 21165 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23870 21165 603 41 0 23829 0
vsize: 95480
[startup+990.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 22331 0 0 0 98960 53 0 0 25 0 1 0 483331904 98549760 21357 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24060 21357 603 41 0 24019 0
vsize: 96240
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 22520 0 0 0 99959 53 0 0 25 0 1 0 483331904 99336192 21546 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24252 21546 603 41 0 24211 0
vsize: 97008
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 22634 0 0 0 100959 53 0 0 25 0 1 0 483331904 99856384 21660 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24379 21660 603 41 0 24338 0
vsize: 97516
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 22723 0 0 0 101959 54 0 0 25 0 1 0 483331904 100118528 21749 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24443 21749 603 41 0 24402 0
vsize: 97772
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 22805 0 0 0 102959 54 0 0 25 0 1 0 483331904 100524032 21831 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24542 21831 603 41 0 24501 0
vsize: 98168
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 22844 0 0 0 103959 54 0 0 25 0 1 0 483331904 100663296 21870 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24576 21870 603 41 0 24535 0
vsize: 98304
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 22910 0 0 0 104959 54 0 0 25 0 1 0 483331904 100937728 21936 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24643 21936 603 41 0 24602 0
vsize: 98572
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 22949 0 0 0 105959 54 0 0 25 0 1 0 483331904 101072896 21975 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24676 21975 603 41 0 24635 0
vsize: 98704
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 23100 0 0 0 106959 55 0 0 25 0 1 0 483331904 101748736 22126 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24841 22126 603 41 0 24800 0
vsize: 99364
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 23271 0 0 0 107959 55 0 0 25 0 1 0 483331904 102420480 22297 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25005 22297 603 41 0 24964 0
vsize: 100020
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 23384 0 0 0 108958 56 0 0 25 0 1 0 483331904 102801408 22410 4294967295 134512640 134672761 3221224544 3221223648 134560226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25098 22410 603 41 0 25057 0
vsize: 100392
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 23430 0 0 0 109958 56 0 0 25 0 1 0 483331904 103075840 22456 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25165 22456 603 41 0 25124 0
vsize: 100660
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 23486 0 0 0 110959 56 0 0 25 0 1 0 483331904 103215104 22512 4294967295 134512640 134672761 3221224544 3221223648 134559883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25199 22512 603 41 0 25158 0
vsize: 100796
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 23597 0 0 0 111959 56 0 0 25 0 1 0 483331904 103759872 22623 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25332 22623 603 41 0 25291 0
vsize: 101328
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 23670 0 0 0 112959 56 0 0 25 0 1 0 483331904 104005632 22696 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25392 22696 603 41 0 25351 0
vsize: 101568
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 23681 0 0 0 113959 56 0 0 25 0 1 0 483331904 104005632 22707 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25392 22707 603 41 0 25351 0
vsize: 101568
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 23707 0 0 0 114959 56 0 0 25 0 1 0 483331904 104148992 22733 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25427 22733 603 41 0 25386 0
vsize: 101708
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 23743 0 0 0 115959 56 0 0 25 0 1 0 483331904 104292352 22769 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25462 22769 603 41 0 25421 0
vsize: 101848
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14802
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 23803 0 0 0 116959 56 0 0 25 0 1 0 483331904 104570880 22829 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25530 22829 603 41 0 25489 0
vsize: 102120
[startup+1180.01 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 14855
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 23868 0 0 0 117959 56 0 0 25 0 1 0 483331904 104828928 22894 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25593 22894 603 41 0 25552 0
vsize: 102372
[startup+1190.01 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 14855
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 23894 0 0 0 118959 57 0 0 25 0 1 0 483331904 104964096 22920 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25626 22920 603 41 0 25585 0
vsize: 102504
[startup+1200.01 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 14855
Raw data (stat): 14802 (minisat+) R 14801 24215 24214 0 -1 0 23925 0 0 0 119959 57 0 0 25 0 1 0 483331904 105103360 22951 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25660 22951 603 41 0 25619 0
vsize: 102640
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.05 0.99 0.91 1/54 14855
Raw data (stat): 14802 (minisat+) Z 14801 24215 24214 0 -1 12 23927 0 0 0 119959 61 0 0 25 0 1 0 483331904 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.06
CPU time (s): 1200.21
CPU user time (s): 1199.6
CPU system time (s): 0.618905
CPU usage (%): 100.013
Max. virtual memory (Kb): 102640
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####