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/miplib/normalized-mps-v2-13-7-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.78
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 19075

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc6 THE 2005-04-21 17:46:56 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17042 boxname=wulflinc6 idbench=1311 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4f0cac14ed3568050c2c57bb69fdb664  /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-13-7-mod010.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-13-7-mod010.opb /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-13-7-mod010.opb
IDLAUNCH: 17042
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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.042
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:        546748 kB
Buffers:         24360 kB
Cached:         442868 kB
SwapCached:        544 kB
Active:          48092 kB
Inactive:       421200 kB
HighTotal:      131008 kB
HighFree:          616 kB
LowTotal:       903652 kB
LowFree:        546132 kB
SwapTotal:     2097136 kB
SwapFree:      2095720 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5112 kB
Slab:            13092 kB
Committed_AS:    63560 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 18:06:58 (client local time) WITH STATUS 0 IN 1200.4 SECONDS
stats: 17042 7 1200.4 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.84 0.94 0.90 2/54 20741
Raw data (stat): 20741 (runsolver) R 20740 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 488770312 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+10.0002 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 13521 0 0 0 965 33 0 0 25 0 1 0 488770312 62861312 12547 4294967295 134512640 134672761 3221224544 3221223864 134556677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15347 12547 603 41 0 15306 0
vsize: 61388
[startup+20 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 13747 0 0 0 1963 34 0 0 25 0 1 0 488770312 63410176 12773 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15481 12773 603 41 0 15440 0
vsize: 61924
[startup+30.0008 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 13828 0 0 0 2963 35 0 0 25 0 1 0 488770312 63688704 12854 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15549 12854 603 41 0 15508 0
vsize: 62196
[startup+40.0006 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 13959 0 0 0 3962 35 0 0 25 0 1 0 488770312 64270336 12985 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15691 12985 603 41 0 15650 0
vsize: 62764
[startup+50.0009 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 14019 0 0 0 4962 35 0 0 25 0 1 0 488770312 64409600 13045 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15725 13045 603 41 0 15684 0
vsize: 62900
[startup+60.001 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 14050 0 0 0 5963 35 0 0 25 0 1 0 488770312 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.0011 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 14181 0 0 0 6962 36 0 0 25 0 1 0 488770312 65069056 13207 4294967295 134512640 134672761 3221224544 3221223648 134560408 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15886 13207 603 41 0 15845 0
vsize: 63544
[startup+80.0009 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 14249 0 0 0 7962 36 0 0 25 0 1 0 488770312 65343488 13275 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15953 13275 603 41 0 15912 0
vsize: 63812
[startup+90.0004 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 14349 0 0 0 8963 36 0 0 25 0 1 0 488770312 65880064 13375 4294967295 134512640 134672761 3221224544 3221223680 134565089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16084 13375 603 41 0 16043 0
vsize: 64336
[startup+100.001 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 14507 0 0 0 9963 36 0 0 25 0 1 0 488770312 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.001 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 14539 0 0 0 10963 36 0 0 25 0 1 0 488770312 66650112 13565 4294967295 134512640 134672761 3221224544 3221223648 134560196 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.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 14648 0 0 0 11963 36 0 0 25 0 1 0 488770312 67158016 13674 4294967295 134512640 134672761 3221224544 3221223728 134559045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16396 13674 603 41 0 16355 0
vsize: 65584
[startup+130.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 14772 0 0 0 12963 36 0 0 25 0 1 0 488770312 67690496 13798 4294967295 134512640 134672761 3221224544 3221223648 134560504 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.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 14814 0 0 0 13963 37 0 0 25 0 1 0 488770312 67829760 13840 4294967295 134512640 134672761 3221224544 3221223648 134559869 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.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 14884 0 0 0 14963 37 0 0 25 0 1 0 488770312 68104192 13910 4294967295 134512640 134672761 3221224544 3221223648 134560196 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.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 14978 0 0 0 15964 37 0 0 25 0 1 0 488770312 68509696 14004 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16726 14004 603 41 0 16685 0
vsize: 66904
[startup+170.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 15039 0 0 0 16964 37 0 0 25 0 1 0 488770312 68775936 14065 4294967295 134512640 134672761 3221224544 3221223648 134559890 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.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 15060 0 0 0 17964 37 0 0 25 0 1 0 488770312 68775936 14086 4294967295 134512640 134672761 3221224544 3221223648 134560402 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.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 15080 0 0 0 18964 38 0 0 25 0 1 0 488770312 68911104 14106 4294967295 134512640 134672761 3221224544 3221223648 134560396 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.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 15099 0 0 0 19964 38 0 0 25 0 1 0 488770312 69050368 14125 4294967295 134512640 134672761 3221224544 3221223648 134560504 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.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 15169 0 0 0 20965 38 0 0 25 0 1 0 488770312 69320704 14195 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16924 14195 603 41 0 16883 0
vsize: 67696
[startup+220.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 15239 0 0 0 21965 38 0 0 25 0 1 0 488770312 69595136 14265 4294967295 134512640 134672761 3221224544 3221223648 134559916 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.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 15256 0 0 0 22965 38 0 0 25 0 1 0 488770312 69595136 14282 4294967295 134512640 134672761 3221224544 3221223648 134559872 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.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 15273 0 0 0 23965 38 0 0 25 0 1 0 488770312 69730304 14299 4294967295 134512640 134672761 3221224544 3221223648 134560218 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.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 15283 0 0 0 24966 38 0 0 25 0 1 0 488770312 69730304 14309 4294967295 134512640 134672761 3221224544 3221223648 134560196 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 15316 0 0 0 25966 38 0 0 25 0 1 0 488770312 69865472 14342 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17057 14342 603 41 0 17016 0
vsize: 68228
[startup+270.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 15361 0 0 0 26966 38 0 0 25 0 1 0 488770312 70000640 14387 4294967295 134512640 134672761 3221224544 3221223648 134560529 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 15372 0 0 0 27967 38 0 0 25 0 1 0 488770312 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 15384 0 0 0 28967 38 0 0 25 0 1 0 488770312 70135808 14410 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17123 14410 603 41 0 17082 0
vsize: 68492
[startup+300.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 15399 0 0 0 29967 38 0 0 25 0 1 0 488770312 70279168 14425 4294967295 134512640 134672761 3221224544 3221223648 134560514 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 15410 0 0 0 30968 38 0 0 25 0 1 0 488770312 70279168 14436 4294967295 134512640 134672761 3221224544 3221223648 134560235 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 15422 0 0 0 31968 38 0 0 25 0 1 0 488770312 70279168 14448 4294967295 134512640 134672761 3221224544 3221223648 134560287 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17158 14448 603 41 0 17117 0
vsize: 68632
[startup+330.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 15440 0 0 0 32968 38 0 0 25 0 1 0 488770312 70422528 14466 4294967295 134512640 134672761 3221224544 3221223648 134560235 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 15452 0 0 0 33969 38 0 0 25 0 1 0 488770312 70422528 14478 4294967295 134512640 134672761 3221224544 3221223616 134553549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17193 14479 603 41 0 17152 0
vsize: 68772
[startup+350.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 15468 0 0 0 34969 38 0 0 25 0 1 0 488770312 70529024 14494 4294967295 134512640 134672761 3221224544 3221223648 134560276 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 15728 0 0 0 35969 38 0 0 25 0 1 0 488770312 71598080 14754 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17480 14754 603 41 0 17439 0
vsize: 69920
[startup+370.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 15886 0 0 0 36968 39 0 0 25 0 1 0 488770312 72245248 14912 4294967295 134512640 134672761 3221224544 3221223648 134560355 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 16111 0 0 0 37969 39 0 0 25 0 1 0 488770312 73179136 15137 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17866 15137 603 41 0 17825 0
vsize: 71464
[startup+390.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 16238 0 0 0 38968 40 0 0 25 0 1 0 488770312 73707520 15264 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17995 15264 603 41 0 17954 0
vsize: 71980
[startup+400.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 16309 0 0 0 39969 40 0 0 25 0 1 0 488770312 73961472 15335 4294967295 134512640 134672761 3221224544 3221223648 134560218 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 16520 0 0 0 40969 40 0 0 25 0 1 0 488770312 74760192 15546 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18252 15546 603 41 0 18211 0
vsize: 73008
[startup+420.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 16560 0 0 0 41969 40 0 0 25 0 1 0 488770312 75034624 15586 4294967295 134512640 134672761 3221224544 3221223648 134560289 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 16593 0 0 0 42969 40 0 0 25 0 1 0 488770312 75034624 15619 4294967295 134512640 134672761 3221224544 3221223648 134560399 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 16628 0 0 0 43970 40 0 0 25 0 1 0 488770312 75304960 15654 4294967295 134512640 134672761 3221224544 3221223648 134560235 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 16660 0 0 0 44970 40 0 0 25 0 1 0 488770312 75304960 15686 4294967295 134512640 134672761 3221224544 3221223648 134560196 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 16724 0 0 0 45970 41 0 0 25 0 1 0 488770312 75583488 15750 4294967295 134512640 134672761 3221224544 3221223648 134560529 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 16750 0 0 0 46970 41 0 0 25 0 1 0 488770312 75722752 15776 4294967295 134512640 134672761 3221224544 3221223648 134560196 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 16787 0 0 0 47971 41 0 0 25 0 1 0 488770312 75849728 15813 4294967295 134512640 134672761 3221224544 3221223648 134560196 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 16808 0 0 0 48971 41 0 0 25 0 1 0 488770312 75988992 15834 4294967295 134512640 134672761 3221224544 3221223648 134560402 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 16834 0 0 0 49971 41 0 0 25 0 1 0 488770312 76128256 15860 4294967295 134512640 134672761 3221224544 3221223648 134560215 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 16881 0 0 0 50971 41 0 0 25 0 1 0 488770312 76267520 15907 4294967295 134512640 134672761 3221224544 3221223648 134560370 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 16956 0 0 0 51971 41 0 0 25 0 1 0 488770312 76517376 15982 4294967295 134512640 134672761 3221224544 3221223648 134560514 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 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 17076 0 0 0 52971 42 0 0 25 0 1 0 488770312 77070336 16102 4294967295 134512640 134672761 3221224544 3221223648 134560237 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 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 17266 0 0 0 53971 42 0 0 25 0 1 0 488770312 77864960 16292 4294967295 134512640 134672761 3221224544 3221223648 134560196 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 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 17403 0 0 0 54971 43 0 0 25 0 1 0 488770312 78364672 16429 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19132 16429 603 41 0 19091 0
vsize: 76528
[startup+560.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 17528 0 0 0 55971 43 0 0 25 0 1 0 488770312 78897152 16554 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19262 16554 603 41 0 19221 0
vsize: 77048
[startup+570.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 17704 0 0 0 56971 43 0 0 25 0 1 0 488770312 79577088 16730 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19428 16730 603 41 0 19387 0
vsize: 77712
[startup+580.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 17729 0 0 0 57971 44 0 0 25 0 1 0 488770312 79708160 16755 4294967295 134512640 134672761 3221224544 3221223648 134560529 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 17845 0 0 0 58971 44 0 0 25 0 1 0 488770312 80232448 16871 4294967295 134512640 134672761 3221224544 3221223680 134560566 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 18000 0 0 0 59971 45 0 0 25 0 1 0 488770312 80785408 17026 4294967295 134512640 134672761 3221224544 3221223648 134560529 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 18124 0 0 0 60971 45 0 0 25 0 1 0 488770312 81326080 17150 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19855 17150 603 41 0 19814 0
vsize: 79420
[startup+620.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 18210 0 0 0 61971 45 0 0 25 0 1 0 488770312 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 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 18234 0 0 0 62971 45 0 0 25 0 1 0 488770312 81731584 17260 4294967295 134512640 134672761 3221224544 3221223648 134560504 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 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 18250 0 0 0 63971 45 0 0 25 0 1 0 488770312 81866752 17276 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19987 17276 603 41 0 19946 0
vsize: 79948
[startup+650.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 18463 0 0 0 64971 46 0 0 25 0 1 0 488770312 82681856 17489 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20186 17489 603 41 0 20145 0
vsize: 80744
[startup+660.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 18663 0 0 0 65971 46 0 0 25 0 1 0 488770312 83488768 17689 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20383 17689 603 41 0 20342 0
vsize: 81532
[startup+670.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 18801 0 0 0 66972 46 0 0 25 0 1 0 488770312 84152320 17827 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20545 17827 603 41 0 20504 0
vsize: 82180
[startup+680.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 19021 0 0 0 67971 47 0 0 25 0 1 0 488770312 84955136 18047 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20741 18047 603 41 0 20700 0
vsize: 82964
[startup+690.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 19148 0 0 0 68972 47 0 0 25 0 1 0 488770312 85499904 18174 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20874 18174 603 41 0 20833 0
vsize: 83496
[startup+700.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 19265 0 0 0 69972 47 0 0 25 0 1 0 488770312 86048768 18291 4294967295 134512640 134672761 3221224544 3221223648 134560402 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.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 19315 0 0 0 70972 47 0 0 25 0 1 0 488770312 86183936 18341 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21041 18341 603 41 0 21000 0
vsize: 84164
[startup+720.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 19448 0 0 0 71972 48 0 0 25 0 1 0 488770312 86716416 18474 4294967295 134512640 134672761 3221224544 3221223712 134559063 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21171 18474 603 41 0 21130 0
vsize: 84684
[startup+730.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 19513 0 0 0 72972 48 0 0 25 0 1 0 488770312 86974464 18539 4294967295 134512640 134672761 3221224544 3221223648 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21234 18539 603 41 0 21193 0
vsize: 84936
[startup+740.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 19688 0 0 0 73972 48 0 0 25 0 1 0 488770312 87760896 18714 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21426 18714 603 41 0 21385 0
vsize: 85704
[startup+750.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 19841 0 0 0 74972 48 0 0 25 0 1 0 488770312 88424448 18867 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21588 18867 603 41 0 21547 0
vsize: 86352
[startup+760.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 19957 0 0 0 75972 48 0 0 25 0 1 0 488770312 88829952 18983 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21687 18983 603 41 0 21646 0
vsize: 86748
[startup+770.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 20013 0 0 0 76973 49 0 0 25 0 1 0 488770312 88969216 19039 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21721 19039 603 41 0 21680 0
vsize: 86884
[startup+780.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20741
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 20151 0 0 0 77973 49 0 0 25 0 1 0 488770312 89612288 19177 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21878 19177 603 41 0 21837 0
vsize: 87512
[startup+790.012 s]
Raw data (loadavg): 1.07 0.99 0.91 3/58 20791
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 20240 0 0 0 78965 57 0 0 25 0 1 0 488770312 90021888 19266 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21978 19266 603 41 0 21937 0
vsize: 87912
[startup+800.013 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 20794
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 20285 0 0 0 79964 57 0 0 25 0 1 0 488770312 90157056 19311 4294967295 134512640 134672761 3221224544 3221223648 134560196 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.013 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 20794
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 20306 0 0 0 80964 57 0 0 25 0 1 0 488770312 90292224 19332 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22044 19332 603 41 0 22003 0
vsize: 88176
[startup+820.013 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 20794
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 20337 0 0 0 81965 57 0 0 25 0 1 0 488770312 90411008 19363 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22073 19363 603 41 0 22032 0
vsize: 88292
[startup+830.013 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 20794
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 20370 0 0 0 82965 57 0 0 25 0 1 0 488770312 90550272 19396 4294967295 134512640 134672761 3221224544 3221223648 134559851 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.014 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 20794
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 20418 0 0 0 83965 57 0 0 25 0 1 0 488770312 90689536 19444 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22141 19444 603 41 0 22100 0
vsize: 88564
[startup+850.014 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 20794
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 20459 0 0 0 84965 58 0 0 25 0 1 0 488770312 90824704 19485 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22174 19485 603 41 0 22133 0
vsize: 88696
[startup+860.014 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 20794
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 20503 0 0 0 85966 58 0 0 25 0 1 0 488770312 90963968 19529 4294967295 134512640 134672761 3221224544 3221223648 134560196 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.015 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 20796
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 20623 0 0 0 86965 58 0 0 25 0 1 0 488770312 91496448 19649 4294967295 134512640 134672761 3221224544 3221223648 134560198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22338 19649 603 41 0 22297 0
vsize: 89352
[startup+880.015 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 20796
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 20739 0 0 0 87965 58 0 0 25 0 1 0 488770312 92045312 19765 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22472 19765 603 41 0 22431 0
vsize: 89888
[startup+890.015 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 20796
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 20840 0 0 0 88965 58 0 0 25 0 1 0 488770312 92422144 19866 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22564 19866 603 41 0 22523 0
vsize: 90256
[startup+900.015 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 20796
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 20905 0 0 0 89966 58 0 0 25 0 1 0 488770312 92696576 19931 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22631 19931 603 41 0 22590 0
vsize: 90524
[startup+910.015 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 20796
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 21004 0 0 0 90966 59 0 0 25 0 1 0 488770312 93106176 20030 4294967295 134512640 134672761 3221224544 3221223648 134559908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22731 20030 603 41 0 22690 0
vsize: 90924
[startup+920.015 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 20796
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 21199 0 0 0 91966 59 0 0 25 0 1 0 488770312 93929472 20225 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22932 20225 603 41 0 22891 0
vsize: 91728
[startup+930.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 20796
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 21414 0 0 0 92966 59 0 0 25 0 1 0 488770312 94810112 20440 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23147 20440 603 41 0 23106 0
vsize: 92588
[startup+940.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 20796
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 21557 0 0 0 93966 60 0 0 25 0 1 0 488770312 95346688 20583 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23278 20583 603 41 0 23237 0
vsize: 93112
[startup+950.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 20796
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 21610 0 0 0 94966 60 0 0 25 0 1 0 488770312 95604736 20636 4294967295 134512640 134672761 3221224544 3221223744 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23341 20636 603 41 0 23300 0
vsize: 93364
[startup+960.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 20796
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 21776 0 0 0 95966 60 0 0 25 0 1 0 488770312 96288768 20802 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23508 20802 603 41 0 23467 0
vsize: 94032
[startup+970.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 20796
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 22017 0 0 0 96966 61 0 0 25 0 1 0 488770312 97222656 21043 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23736 21043 603 41 0 23695 0
vsize: 94944
[startup+980.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 20796
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 22163 0 0 0 97966 61 0 0 25 0 1 0 488770312 97906688 21189 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23903 21189 603 41 0 23862 0
vsize: 95612
[startup+990.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 20796
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 22369 0 0 0 98965 62 0 0 25 0 1 0 488770312 98684928 21395 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24093 21395 603 41 0 24052 0
vsize: 96372
[startup+1000.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 20796
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 22537 0 0 0 99965 62 0 0 25 0 1 0 488770312 99336192 21563 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24252 21563 603 41 0 24211 0
vsize: 97008
[startup+1010.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 20796
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 22654 0 0 0 100966 62 0 0 25 0 1 0 488770312 99856384 21680 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24379 21680 603 41 0 24338 0
vsize: 97516
[startup+1020.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 20796
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 22734 0 0 0 101966 63 0 0 25 0 1 0 488770312 100257792 21760 4294967295 134512640 134672761 3221224544 3221223728 134558654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24477 21760 603 41 0 24436 0
vsize: 97908
[startup+1030.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 20796
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 22809 0 0 0 102966 63 0 0 25 0 1 0 488770312 100524032 21835 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24542 21835 603 41 0 24501 0
vsize: 98168
[startup+1040.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 20796
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 22855 0 0 0 103966 63 0 0 25 0 1 0 488770312 100663296 21881 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24576 21881 603 41 0 24535 0
vsize: 98304
[startup+1050.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 20796
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 22922 0 0 0 104966 63 0 0 25 0 1 0 488770312 100937728 21948 4294967295 134512640 134672761 3221224544 3221223648 134560201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24643 21948 603 41 0 24602 0
vsize: 98572
[startup+1060.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 20796
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 22956 0 0 0 105967 63 0 0 25 0 1 0 488770312 101072896 21982 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24676 21982 603 41 0 24635 0
vsize: 98704
[startup+1070.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 20796
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 23180 0 0 0 106966 64 0 0 25 0 1 0 488770312 102010880 22206 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24905 22206 603 41 0 24864 0
vsize: 99620
[startup+1080.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 20796
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 23280 0 0 0 107967 64 0 0 25 0 1 0 488770312 102420480 22306 4294967295 134512640 134672761 3221224544 3221223648 134559981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25005 22306 603 41 0 24964 0
vsize: 100020
[startup+1090.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 20796
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 23416 0 0 0 108967 64 0 0 25 0 1 0 488770312 102940672 22442 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25132 22442 603 41 0 25091 0
vsize: 100528
[startup+1100.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 20798
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 23441 0 0 0 109967 64 0 0 25 0 1 0 488770312 103075840 22467 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25165 22467 603 41 0 25124 0
vsize: 100660
[startup+1110.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 20798
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 23544 0 0 0 110967 65 0 0 25 0 1 0 488770312 103489536 22570 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25266 22570 603 41 0 25225 0
vsize: 101064
[startup+1120.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 20798
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 23608 0 0 0 111967 65 0 0 25 0 1 0 488770312 103759872 22634 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25332 22634 603 41 0 25291 0
vsize: 101328
[startup+1130.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 20798
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 23672 0 0 0 112967 65 0 0 25 0 1 0 488770312 104005632 22698 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25392 22698 603 41 0 25351 0
vsize: 101568
[startup+1140.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 20798
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 23694 0 0 0 113968 65 0 0 25 0 1 0 488770312 104148992 22720 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25427 22720 603 41 0 25386 0
vsize: 101708
[startup+1150.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 20798
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 23719 0 0 0 114968 65 0 0 25 0 1 0 488770312 104292352 22745 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25462 22745 603 41 0 25421 0
vsize: 101848
[startup+1160.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 20798
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 23752 0 0 0 115968 65 0 0 25 0 1 0 488770312 104292352 22778 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25462 22778 603 41 0 25421 0
vsize: 101848
[startup+1170.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 20798
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 23815 0 0 0 116968 65 0 0 25 0 1 0 488770312 104570880 22841 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25530 22841 603 41 0 25489 0
vsize: 102120
[startup+1180.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 20798
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 23877 0 0 0 117969 65 0 0 25 0 1 0 488770312 104828928 22903 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25593 22903 603 41 0 25552 0
vsize: 102372
[startup+1190.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 20798
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 23905 0 0 0 118969 65 0 0 25 0 1 0 488770312 104964096 22931 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25626 22931 603 41 0 25585 0
vsize: 102504
[startup+1200.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 20798
Raw data (stat): 20741 (minisat+) R 20740 29653 29652 0 -1 0 23934 0 0 0 119969 65 0 0 25 0 1 0 488770312 105103360 22960 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25660 22960 603 41 0 25619 0
vsize: 102640
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 20798
Raw data (stat): 20741 (minisat+) Z 20740 29653 29652 0 -1 12 23936 0 0 0 119969 70 0 0 25 0 1 0 488770312 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.07
CPU time (s): 1200.4
CPU user time (s): 1199.7
CPU system time (s): 0.702893
CPU usage (%): 100.028
Max. virtual memory (Kb): 102640
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####