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 15635

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc18 THE 2005-04-21 05:19:27 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17035 boxname=wulflinc18 idbench=1311 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  4f0cac14ed3568050c2c57bb69fdb664  /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-mod010.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-mod010.opb
IDLAUNCH: 17035
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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:        375976 kB
Buffers:         35004 kB
Cached:         592112 kB
SwapCached:        388 kB
Active:         322484 kB
Inactive:       307132 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        375724 kB
SwapTotal:     2097892 kB
SwapFree:      2096996 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6224 kB
Slab:            23280 kB
Committed_AS:    63768 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 05:39:29 (client local time) WITH STATUS 0 IN 1200.25 SECONDS
stats: 17035 7 1200.25 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 291 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 289]---> BDD-cost:   67
c ---[ 287]---> BDD-cost:  113
c ---[ 285]---> BDD-cost:  181
c ---[ 283]---> BDD-cost:  115
c ---[ 281]---> BDD-cost:   69
c ---[ 279]---> BDD-cost:  125
c ---[ 277]---> BDD-cost:  155
c ---[ 275]---> BDD-cost:   87
c ---[ 273]---> BDD-cost:   97
c ---[ 271]---> BDD-cost:   73
c ---[ 269]---> BDD-cost:  119
c ---[ 267]---> BDD-cost:   45
c ---[ 265]---> BDD-cost:  171
c ---[ 263]---> BDD-cost:  111
c ---[ 261]---> BDD-cost:  149
c ---[ 259]---> BDD-cost:  195
c ---[ 257]---> BDD-cost:  131
c ---[ 255]---> BDD-cost:  123
c ---[ 253]---> BDD-cost:  167
c ---[ 251]---> BDD-cost:  101
c ---[ 249]---> BDD-cost:   97
c ---[ 247]---> BDD-cost:   23
c ---[ 245]---> BDD-cost:  135
c ---[ 243]---> BDD-cost:   59
c ---[ 241]---> BDD-cost:   95
c ---[ 239]---> BDD-cost:   59
c ---[ 237]---> BDD-cost:  133
c ---[ 235]---> BDD-cost:   99
c ---[ 233]---> BDD-cost:  179
c ---[ 231]---> BDD-cost:  111
c ---[ 229]---> BDD-cost:   23
c ---[ 227]---> BDD-cost:   89
c ---[ 225]---> BDD-cost:   95
c ---[ 223]---> BDD-cost:  117
c ---[ 221]---> BDD-cost:   23
c ---[ 219]---> BDD-cost:   51
c ---[ 217]---> BDD-cost:  311
c ---[ 215]---> BDD-cost:  259
c ---[ 213]---> BDD-cost:  169
c ---[ 211]---> BDD-cost:  131
c ---[ 209]---> BDD-cost:  155
c ---[ 207]---> BDD-cost:   89
c ---[ 205]---> BDD-cost:   51
c ---[ 203]---> BDD-cost:  165
c ---[ 201]---> BDD-cost:   75
c ---[ 199]---> BDD-cost:  139
c ---[ 197]---> BDD-cost:   67
c ---[ 195]---> BDD-cost:  173
c ---[ 193]---> BDD-cost:  235
c ---[ 191]---> BDD-cost:  185
c ---[ 189]---> BDD-cost:  127
c ---[ 187]---> BDD-cost:   37
c ---[ 185]---> BDD-cost:   37
c ---[ 183]---> BDD-cost:   91
c ---[ 181]---> BDD-cost:   77
c ---[ 179]---> BDD-cost:   29
c ---[ 177]---> BDD-cost:   77
c ---[ 175]---> BDD-cost:   77
c ---[ 173]---> BDD-cost:  101
c ---[ 171]---> BDD-cost:  131
c ---[ 169]---> BDD-cost:  155
c ---[ 167]---> BDD-cost:  177
c ---[ 165]---> BDD-cost:  143
c ---[ 163]---> BDD-cost:   93
c ---[ 161]---> BDD-cost:   79
c ---[ 159]---> BDD-cost:   53
c ---[ 157]---> BDD-cost:   71
c ---[ 155]---> BDD-cost:  127
c ---[ 153]---> BDD-cost:  127
c ---[ 151]---> BDD-cost:   67
c ---[ 149]---> BDD-cost:   83
c ---[ 147]---> BDD-cost:   47
c ---[ 145]---> BDD-cost:   63
c ---[ 143]---> BDD-cost:  121
c ---[ 141]---> BDD-cost:  155
c ---[ 139]---> BDD-cost:   87
c ---[ 137]---> BDD-cost:   91
c ---[ 135]---> BDD-cost:   47
c ---[ 133]---> BDD-cost:   67
c ---[ 131]---> BDD-cost:   33
c ---[ 129]---> BDD-cost:   91
c ---[ 127]---> BDD-cost:   69
c ---[ 125]---> BDD-cost:    5
c ---[ 123]---> BDD-cost:   47
c ---[ 121]---> BDD-cost:   45
c ---[ 119]---> BDD-cost:   37
c ---[ 117]---> BDD-cost:  117
c ---[ 115]---> BDD-cost:   97
c ---[ 113]---> BDD-cost:   77
c ---[ 111]---> BDD-cost:   97
c ---[ 109]---> BDD-cost:  137
c ---[ 107]---> BDD-cost:  125
c ---[ 105]---> BDD-cost:   79
c ---[ 103]---> BDD-cost:  133
c ---[ 101]---> BDD-cost:  153
c ---[  99]---> BDD-cost:  139
c ---[  97]---> BDD-cost:  125
c ---[  95]---> BDD-cost:    5
c ---[  93]---> BDD-cost:   73
c ---[  91]---> BDD-cost:  157
c ---[  89]---> BDD-cost:  127
c ---[  87]---> BDD-cost:  199
c ---[  85]---> BDD-cost:  121
c ---[  83]---> BDD-cost:  107
c ---[  81]---> BDD-cost:  169
c ---[  79]---> BDD-cost:  113
c ---[  77]---> BDD-cost:  103
c ---[  75]---> BDD-cost:   75
c ---[  73]---> BDD-cost:   97
c ---[  71]---> BDD-cost:  151
c ---[  69]---> BDD-cost:  199
c ---[  67]---> BDD-cost:  109
c ---[  65]---> BDD-cost:  131
c ---[  63]---> BDD-cost:  113
c ---[  61]---> BDD-cost:  173
c ---[  59]---> BDD-cost:  119
c ---[  57]---> BDD-cost:  173
c ---[  55]---> BDD-cost:  119
c ---[  53]---> BDD-cost:   71
c ---[  51]---> BDD-cost:  179
c ---[  49]---> BDD-cost:  241
c ---[  47]---> BDD-cost:  201
c ---[  45]---> BDD-cost:  173
c ---[  43]---> BDD-cost:  147
c ---[  41]---> BDD-cost:  157
c ---[  39]---> BDD-cost:  201
c ---[  37]---> BDD-cost:  129
c ---[  35]---> BDD-cost:  117
c ---[  33]---> BDD-cost:  177
c ---[  31]---> BDD-cost:  123
c ---[  29]---> BDD-cost:  131
c ---[  27]---> BDD-cost:  115
c ---[  25]---> BDD-cost:   51
c ---[  23]---> BDD-cost:  123
c ---[  21]---> BDD-cost:   55
c ---[  19]---> BDD-cost:    5
c ---[  17]---> BDD-cost:   99
c ---[  15]---> BDD-cost:   85
c ---[  13]---> BDD-cost:  109
c ---[  11]---> BDD-cost:  153
c ---[   9]---> BDD-cost:  201
c ---[   7]---> BDD-cost:  133
c ---[   5]---> BDD-cost:  121
c ---[   3]---> BDD-cost:  171
c ---[   1]---> Adder-cost: 5294   maxlim: 2609   bits: 12/12
c ---[   0]---> BDD-cost:  751
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   79291   242194 |   26430       0        0     nan |  0.000 % |
c |       101 |   79216   241933 |   29073      93      735     7.9 |  0.735 % |
c |       253 |   79216   241933 |   31980     245     2664    10.9 |  0.735 % |
c |       478 |   79216   241933 |   35178     470    26790    57.0 |  0.735 % |
c |       816 |   79216   241933 |   38696     808    31842    39.4 |  0.735 % |
c |      1323 |   79216   241933 |   42565    1315    62134    47.3 |  0.735 % |
c |      2082 |   79216   241933 |   46822    2074   107560    51.9 |  0.735 % |
c |      3222 |   79188   241847 |   51504    3207   277140    86.4 |  0.751 % |
c |      4930 |   79188   241847 |   56655    4915   483903    98.5 |  0.751 % |
c |      7493 |   79188   241847 |   62320    7478   739580    98.9 |  0.751 % |
c |     11337 |   79188   241847 |   68552   11322  1362239   120.3 |  0.751 % |
c |     17103 |   79164   241769 |   75407   17085  2978250   174.3 |  0.767 % |
c |     25752 |   79164   241769 |   82948   25734  6444146   250.4 |  0.767 % |
c |     38727 |   79164   241769 |   91243   38709 10596182   273.7 |  0.767 % |
c |     58188 |   79145   241708 |  100367   58167 16215504   278.8 |  0.779 % |
c |     87383 |   79101   241554 |  110404   87356 23978747   274.5 |  0.807 % |
c |    131172 |   79079   241468 |  121445   35237  6368599   180.7 |  0.823 % |
c |    196857 |   78549   239688 |  133589  100806 30304920   300.6 |  1.134 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.68 0.88 0.89 2/55 20100
Raw data (stat): 20100 (runsolver) R 20099 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 542498084 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.73 0.89 0.89 2/55 20100
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 5374 0 0 0 985 13 0 0 25 0 1 0 542498084 22405120 4705 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5470 4705 603 41 0 5429 0
vsize: 21880
[startup+20.0013 s]
Raw data (loadavg): 0.77 0.89 0.89 2/55 20100
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 5910 0 0 0 1983 15 0 0 25 0 1 0 542498084 24596480 5241 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6005 5241 603 41 0 5964 0
vsize: 24020
[startup+30.0022 s]
Raw data (loadavg): 0.81 0.89 0.89 2/55 20100
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 6491 0 0 0 2982 17 0 0 25 0 1 0 542498084 26890240 5822 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6565 5822 603 41 0 6524 0
vsize: 26260
[startup+40.0025 s]
Raw data (loadavg): 0.83 0.89 0.89 2/55 20100
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 7304 0 0 0 3980 19 0 0 25 0 1 0 542498084 30257152 6635 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7387 6635 603 41 0 7346 0
vsize: 29548
[startup+50.003 s]
Raw data (loadavg): 0.86 0.90 0.89 2/55 20100
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 8021 0 0 0 4979 20 0 0 25 0 1 0 542498084 33226752 7352 4294967295 134512640 134672761 3221224624 3221223760 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8112 7352 603 41 0 8071 0
vsize: 32448
[startup+60.0029 s]
Raw data (loadavg): 0.88 0.90 0.89 2/55 20100
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 8666 0 0 0 5976 23 0 0 25 0 1 0 542498084 35872768 7997 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8758 7997 603 41 0 8717 0
vsize: 35032
[startup+70.0032 s]
Raw data (loadavg): 0.90 0.90 0.89 2/55 20100
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 9294 0 0 0 6974 25 0 0 25 0 1 0 542498084 38436864 8625 4294967295 134512640 134672761 3221224624 3221223728 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9384 8625 603 41 0 9343 0
vsize: 37536
[startup+80.0037 s]
Raw data (loadavg): 0.91 0.91 0.89 2/55 20102
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 9910 0 0 0 7972 27 0 0 25 0 1 0 542498084 40992768 9241 4294967295 134512640 134672761 3221224624 3221223728 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10008 9241 603 41 0 9967 0
vsize: 40032
[startup+90.0037 s]
Raw data (loadavg): 0.93 0.91 0.89 2/55 20102
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 10482 0 0 0 8971 29 0 0 25 0 1 0 542498084 43278336 9813 4294967295 134512640 134672761 3221224624 3221223728 134560034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10566 9813 603 41 0 10525 0
vsize: 42264
[startup+100.004 s]
Raw data (loadavg): 0.94 0.91 0.90 2/55 20102
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 11033 0 0 0 9969 30 0 0 25 0 1 0 542498084 45572096 10364 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11126 10364 603 41 0 11085 0
vsize: 44504
[startup+110.004 s]
Raw data (loadavg): 0.95 0.91 0.90 2/55 20102
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 11572 0 0 0 10967 33 0 0 25 0 1 0 542498084 47841280 10903 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11680 10903 603 41 0 11639 0
vsize: 46720
[startup+120.006 s]
Raw data (loadavg): 0.95 0.92 0.90 2/55 20102
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 12186 0 0 0 11965 34 0 0 25 0 1 0 542498084 50262016 11517 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12271 11517 603 41 0 12230 0
vsize: 49084
[startup+130.007 s]
Raw data (loadavg): 0.96 0.92 0.90 2/55 20102
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 12922 0 0 0 12963 37 0 0 25 0 1 0 542498084 53354496 12253 4294967295 134512640 134672761 3221224624 3221223728 134560036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13026 12253 603 41 0 12985 0
vsize: 52104
[startup+140.007 s]
Raw data (loadavg): 0.97 0.92 0.90 2/55 20102
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 13565 0 0 0 13961 38 0 0 25 0 1 0 542498084 55894016 12896 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13646 12896 603 41 0 13605 0
vsize: 54584
[startup+150.008 s]
Raw data (loadavg): 0.97 0.92 0.90 2/55 20102
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 14252 0 0 0 14959 41 0 0 25 0 1 0 542498084 58724352 13583 4294967295 134512640 134672761 3221224624 3221223728 134560005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14337 13583 603 41 0 14296 0
vsize: 57348
[startup+160.008 s]
Raw data (loadavg): 0.98 0.92 0.90 2/55 20102
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 14858 0 0 0 15957 43 0 0 25 0 1 0 542498084 61284352 14189 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14962 14189 603 41 0 14921 0
vsize: 59848
[startup+170.008 s]
Raw data (loadavg): 0.98 0.93 0.90 2/55 20102
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 15470 0 0 0 16955 45 0 0 25 0 1 0 542498084 63848448 14801 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15588 14801 603 41 0 15547 0
vsize: 62352
[startup+180.01 s]
Raw data (loadavg): 0.98 0.93 0.90 2/55 20102
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 16077 0 0 0 17953 48 0 0 25 0 1 0 542498084 66269184 15408 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16179 15408 603 41 0 16138 0
vsize: 64716
[startup+190.01 s]
Raw data (loadavg): 0.98 0.93 0.90 2/55 20102
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 16612 0 0 0 18951 49 0 0 25 0 1 0 542498084 68550656 15943 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16736 15943 603 41 0 16695 0
vsize: 66944
[startup+200.01 s]
Raw data (loadavg): 0.99 0.93 0.91 2/55 20102
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 17314 0 0 0 19950 51 0 0 25 0 1 0 542498084 71389184 16645 4294967295 134512640 134672761 3221224624 3221223792 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17429 16645 603 41 0 17388 0
vsize: 69716
[startup+210.01 s]
Raw data (loadavg): 0.99 0.93 0.91 2/55 20102
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 18092 0 0 0 20948 53 0 0 25 0 1 0 542498084 74493952 17423 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18187 17423 603 41 0 18146 0
vsize: 72748
[startup+220.011 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 20102
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 18794 0 0 0 21946 55 0 0 25 0 1 0 542498084 77467648 18125 4294967295 134512640 134672761 3221224624 3221223728 134560005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18913 18125 603 41 0 18872 0
vsize: 75652
[startup+230.011 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 20102
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 19424 0 0 0 22944 57 0 0 25 0 1 0 542498084 80015360 18755 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19535 18755 603 41 0 19494 0
vsize: 78140
[startup+240.012 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 20102
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 20056 0 0 0 23942 60 0 0 25 0 1 0 542498084 82579456 19387 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20161 19387 603 41 0 20120 0
vsize: 80644
[startup+250.013 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 20102
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 20653 0 0 0 24940 61 0 0 25 0 1 0 542498084 85012480 19984 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20755 19984 603 41 0 20714 0
vsize: 83020
[startup+260.013 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 20102
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 21267 0 0 0 25938 63 0 0 25 0 1 0 542498084 87580672 20598 4294967295 134512640 134672761 3221224624 3221223728 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21382 20598 603 41 0 21341 0
vsize: 85528
[startup+270.014 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 20102
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 21735 0 0 0 26936 65 0 0 25 0 1 0 542498084 89473024 21066 4294967295 134512640 134672761 3221224624 3221223728 134560022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21844 21066 603 41 0 21803 0
vsize: 87376
[startup+280.014 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 20102
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 22230 0 0 0 27935 66 0 0 25 0 1 0 542498084 91492352 21561 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22337 21561 603 41 0 22296 0
vsize: 89348
[startup+290.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 20102
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 22867 0 0 0 28933 69 0 0 25 0 1 0 542498084 94052352 22198 4294967295 134512640 134672761 3221224624 3221223792 134560825 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22962 22198 603 41 0 22921 0
vsize: 91848
[startup+300.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 20102
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 23487 0 0 0 29931 70 0 0 25 0 1 0 542498084 96595968 22818 4294967295 134512640 134672761 3221224624 3221223728 134559883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23583 22818 603 41 0 23542 0
vsize: 94332
[startup+310.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 20102
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 23957 0 0 0 30929 72 0 0 25 0 1 0 542498084 98492416 23288 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24046 23288 603 41 0 24005 0
vsize: 96184
[startup+320.017 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 20102
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 24444 0 0 0 31927 75 0 0 25 0 1 0 542498084 100765696 23775 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24601 23775 603 41 0 24560 0
vsize: 98404
[startup+330.018 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 20102
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 24996 0 0 0 32927 75 0 0 25 0 1 0 542498084 103063552 24327 4294967295 134512640 134672761 3221224624 3221223796 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25162 24327 603 41 0 25121 0
vsize: 100648
[startup+340.019 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 20102
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 25499 0 0 0 33926 76 0 0 25 0 1 0 542498084 105070592 24830 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25652 24830 603 41 0 25611 0
vsize: 102608
[startup+350.018 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 20102
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 26223 0 0 0 34924 79 0 0 25 0 1 0 542498084 108023808 25554 4294967295 134512640 134672761 3221224624 3221223728 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26373 25554 603 41 0 26332 0
vsize: 105492
[startup+360.02 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 20102
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 26992 0 0 0 35922 81 0 0 25 0 1 0 542498084 111267840 26323 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27165 26323 603 41 0 27124 0
vsize: 108660
[startup+370.019 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 20102
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 27572 0 0 0 36920 83 0 0 25 0 1 0 542498084 113565696 26903 4294967295 134512640 134672761 3221224624 3221223728 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27726 26903 603 41 0 27685 0
vsize: 110904
[startup+380.02 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 20104
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 28011 0 0 0 37919 84 0 0 25 0 1 0 542498084 115310592 27342 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28152 27342 603 41 0 28111 0
vsize: 112608
[startup+390.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 20104
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 28428 0 0 0 38918 85 0 0 25 0 1 0 542498084 117059584 27759 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28579 27759 603 41 0 28538 0
vsize: 114316
[startup+400.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 20104
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 28938 0 0 0 39917 87 0 0 25 0 1 0 542498084 119091200 28269 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29075 28269 603 41 0 29034 0
vsize: 116300
[startup+410.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 20104
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 29357 0 0 0 40916 88 0 0 25 0 1 0 542498084 120848384 28688 4294967295 134512640 134672761 3221224624 3221223728 134560250 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29504 28688 603 41 0 29463 0
vsize: 118016
[startup+420.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 20104
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 29924 0 0 0 41915 89 0 0 25 0 1 0 542498084 123146240 29255 4294967295 134512640 134672761 3221224624 3221223728 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30065 29255 603 41 0 30024 0
vsize: 120260
[startup+430.022 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 20104
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 30492 0 0 0 42914 90 0 0 25 0 1 0 542498084 125444096 29823 4294967295 134512640 134672761 3221224624 3221223808 134559572 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30626 29823 603 41 0 30585 0
vsize: 122504
[startup+440.022 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 20104
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 31198 0 0 0 43912 92 0 0 25 0 1 0 542498084 128380928 30529 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31343 30529 603 41 0 31302 0
vsize: 125372
[startup+450.022 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 20104
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 31907 0 0 0 44911 93 0 0 25 0 1 0 542498084 131211264 31238 4294967295 134512640 134672761 3221224624 3221223728 134559835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32034 31238 603 41 0 31993 0
vsize: 128136
[startup+460.023 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 20104
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 32572 0 0 0 45909 95 0 0 25 0 1 0 542498084 134017024 31903 4294967295 134512640 134672761 3221224624 3221223728 134560248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32719 31903 603 41 0 32678 0
vsize: 130876
[startup+470.022 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 20104
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 33155 0 0 0 46908 97 0 0 25 0 1 0 542498084 136310784 32486 4294967295 134512640 134672761 3221224624 3221223728 134560376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33279 32486 603 41 0 33238 0
vsize: 133116
[startup+480.023 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 20104
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 33766 0 0 0 47906 98 0 0 25 0 1 0 542498084 138883072 33097 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33907 33097 603 41 0 33866 0
vsize: 135628
[startup+490.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20104
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 34375 0 0 0 48905 100 0 0 25 0 1 0 542498084 141336576 33706 4294967295 134512640 134672761 3221224624 3221223792 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34506 33706 603 41 0 34465 0
vsize: 138024
[startup+500.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20104
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 34845 0 0 0 49904 101 0 0 25 0 1 0 542498084 143233024 34176 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34969 34176 603 41 0 34928 0
vsize: 139876
[startup+510.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20104
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 35422 0 0 0 50903 102 0 0 25 0 1 0 542498084 145653760 34753 4294967295 134512640 134672761 3221224624 3221223728 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35560 34753 603 41 0 35519 0
vsize: 142240
[startup+520.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20104
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 35777 0 0 0 51902 103 0 0 25 0 1 0 542498084 147132416 35108 4294967295 134512640 134672761 3221224624 3221223728 134560059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35921 35108 603 41 0 35880 0
vsize: 143684
[startup+530.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20104
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 36364 0 0 0 52901 104 0 0 25 0 1 0 542498084 149430272 35695 4294967295 134512640 134672761 3221224624 3221223680 134565098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36482 35695 603 41 0 36441 0
vsize: 145928
[startup+540.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20104
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 36879 0 0 0 53900 105 0 0 25 0 1 0 542498084 151588864 36210 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37009 36210 603 41 0 36968 0
vsize: 148036
[startup+550.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20104
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 37212 0 0 0 54899 106 0 0 25 0 1 0 542498084 152940544 36543 4294967295 134512640 134672761 3221224624 3221223624 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37339 36543 603 41 0 37298 0
vsize: 149356
[startup+560.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20104
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 37616 0 0 0 55899 107 0 0 25 0 1 0 542498084 154566656 36947 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37736 36947 603 41 0 37695 0
vsize: 150944
[startup+570.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20104
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 38085 0 0 0 56898 109 0 0 25 0 1 0 542498084 156463104 37416 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38199 37416 603 41 0 38158 0
vsize: 152796
[startup+580.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20104
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 38622 0 0 0 57896 110 0 0 25 0 1 0 542498084 158752768 37953 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38758 37953 603 41 0 38717 0
vsize: 155032
[startup+590.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20104
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39198 0 0 0 58894 112 0 0 25 0 1 0 542498084 161050624 38529 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39319 38529 603 41 0 39278 0
vsize: 157276
[startup+600.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20104
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 59894 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+610.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20104
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 60894 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+620.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20104
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 61894 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+630.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20104
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 62895 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134560393 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+640.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20104
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 63894 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+650.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20104
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 64895 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+660.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20104
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 65894 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+670.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20104
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 66894 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+680.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20106
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 67894 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+690.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20106
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 68895 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+700.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20106
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 69895 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+710.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20106
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 70895 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+720.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20106
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 71895 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+730.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20106
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 72895 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+740.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20106
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 73896 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+750.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20106
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 74896 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+760.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20106
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 75896 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223760 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+770.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20106
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 76896 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223808 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+780.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20106
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 77896 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+790.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20106
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 78896 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+800.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20106
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 79897 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134560039 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+810.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20106
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 80897 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+820.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20106
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 81897 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+830.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20106
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 82897 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+840.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20106
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 83897 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223824 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+850.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20106
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 84897 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+860.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20106
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 85898 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+870.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20106
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 86898 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+880.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20106
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 87898 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223748 134566047 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+890.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20106
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 88898 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134559933 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+900.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20106
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 89898 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134559902 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+910.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20106
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 90898 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+920.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20106
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 91899 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+930.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20106
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 92899 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223808 134559611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+940.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20106
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 93899 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+950.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20106
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 94899 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+960.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20106
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 95899 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223796 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+970.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20106
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 96899 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223784 134561029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+980.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20108
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 97900 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+990.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20108
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 98900 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223764 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20108
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 99900 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20108
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 100900 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20108
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 101900 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20108
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 102901 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20108
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 103901 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20108
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 104900 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20108
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 105900 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20108
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 106900 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134559908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20108
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 107900 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20108
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39541 0 0 0 108901 113 0 0 25 0 1 0 542498084 162398208 38872 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20108
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 39755 0 0 0 109900 114 0 0 25 0 1 0 542498084 163352576 39086 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39881 39087 603 41 0 39840 0
vsize: 159524
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20108
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 40207 0 0 0 110900 115 0 0 25 0 1 0 542498084 165240832 39538 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40342 39538 603 41 0 40301 0
vsize: 161368
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20108
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 40651 0 0 0 111898 116 0 0 25 0 1 0 542498084 166989824 39982 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40769 39982 603 41 0 40728 0
vsize: 163076
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20108
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 41375 0 0 0 112898 117 0 0 25 0 1 0 542498084 169934848 40706 4294967295 134512640 134672761 3221224624 3221223728 134559916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41488 40706 603 41 0 41447 0
vsize: 165952
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20108
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 41839 0 0 0 113897 118 0 0 25 0 1 0 542498084 171798528 41170 4294967295 134512640 134672761 3221224624 3221223728 134559991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41943 41170 603 41 0 41902 0
vsize: 167772
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20108
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 42356 0 0 0 114895 120 0 0 25 0 1 0 542498084 173977600 41687 4294967295 134512640 134672761 3221224624 3221223728 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42475 41687 603 41 0 42434 0
vsize: 169900
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20108
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 42855 0 0 0 115895 120 0 0 25 0 1 0 542498084 175976448 42186 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42963 42186 603 41 0 42922 0
vsize: 171852
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20108
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 43433 0 0 0 116894 122 0 0 25 0 1 0 542498084 178401280 42764 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43555 42764 603 41 0 43514 0
vsize: 174220
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20108
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 44171 0 0 0 117892 124 0 0 25 0 1 0 542498084 181391360 43502 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44285 43503 603 41 0 44244 0
vsize: 177140
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20108
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 44887 0 0 0 118891 124 0 0 25 0 1 0 542498084 184377344 44218 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45014 44218 603 41 0 44973 0
vsize: 180056
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 20108
Raw data (stat): 20100 (minisat+) R 20099 20024 20023 0 -1 0 45483 0 0 0 119891 125 0 0 25 0 1 0 542498084 186806272 44814 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45607 44814 603 41 0 45566 0
vsize: 182428
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.13 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 20108
Raw data (stat): 20100 (minisat+) Z 20099 20024 20023 0 -1 12 45485 0 0 0 119891 134 0 0 25 0 1 0 542498084 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.13
CPU time (s): 1200.25
CPU user time (s): 1198.91
CPU system time (s): 1.3408
CPU usage (%): 100.01
Max. virtual memory (Kb): 182428
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####