PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-mod010.opb
MD5SUM	ef7064a9be2b712276f7b600af28e2b0
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	6571
Optimality of the best value was proved	NO
Number of terms in the objective function	2655
Biggest coefficient in the objective function	266
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	489211
Number of bits of the sum of numbers in the objective function	19
Biggest number in a constraint	266
Number of bits of the biggest number in a constraint	9
Biggest sum of numbers in a constraint	489211
Number of bits of the biggest sum of numbers	19
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1176.54
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 21198

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc23 THE 2005-04-21 23:03:57 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13642 boxname=wulflinc23 idbench=1050 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  ef7064a9be2b712276f7b600af28e2b0  /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-mod010.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-mod010.opb
IDLAUNCH: 13642
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        689112 kB
Buffers:         19048 kB
Cached:         302724 kB
SwapCached:        548 kB
Active:          59016 kB
Inactive:       264752 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        688860 kB
SwapTotal:     2097136 kB
SwapFree:      2095732 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5104 kB
Slab:            16008 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 23:24:00 (client local time) WITH STATUS 0 IN 1200.26 SECONDS
stats: 13642 7 1200.26 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.89 0.98 0.92 2/54 15590
Raw data (stat): 15590 (runsolver) R 15589 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 548894234 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 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.0007 s]
Raw data (loadavg): 0.90 0.98 0.92 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 5371 0 0 0 986 12 0 0 25 0 1 0 548894234 22274048 4702 4294967295 134512640 134672761 3221224624 3221223792 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5438 4702 603 41 0 5397 0
vsize: 21752
[startup+20.0015 s]
Raw data (loadavg): 0.92 0.98 0.92 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 5904 0 0 0 1985 14 0 0 25 0 1 0 548894234 24461312 5235 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5972 5235 603 41 0 5931 0
vsize: 23888
[startup+30.0016 s]
Raw data (loadavg): 0.93 0.98 0.92 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 6477 0 0 0 2982 16 0 0 25 0 1 0 548894234 26890240 5808 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6565 5808 603 41 0 6524 0
vsize: 26260
[startup+40.0017 s]
Raw data (loadavg): 0.94 0.98 0.92 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 7279 0 0 0 3979 18 0 0 25 0 1 0 548894234 30121984 6610 4294967295 134512640 134672761 3221224624 3221223728 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7354 6610 603 41 0 7313 0
vsize: 29416
[startup+50.0022 s]
Raw data (loadavg): 0.95 0.98 0.92 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 8000 0 0 0 4978 19 0 0 25 0 1 0 548894234 33095680 7331 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8080 7331 603 41 0 8039 0
vsize: 32320
[startup+60.0025 s]
Raw data (loadavg): 0.96 0.98 0.92 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 8647 0 0 0 5976 21 0 0 25 0 1 0 548894234 35872768 7978 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8758 7978 603 41 0 8717 0
vsize: 35032
[startup+70.0024 s]
Raw data (loadavg): 0.96 0.98 0.92 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 9275 0 0 0 6975 23 0 0 25 0 1 0 548894234 38436864 8606 4294967295 134512640 134672761 3221224624 3221223728 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9384 8606 603 41 0 9343 0
vsize: 37536
[startup+80.003 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 9895 0 0 0 7973 25 0 0 25 0 1 0 548894234 40857600 9226 4294967295 134512640 134672761 3221224624 3221223728 134560010 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9975 9226 603 41 0 9934 0
vsize: 39900
[startup+90.0024 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 10470 0 0 0 8972 27 0 0 25 0 1 0 548894234 43278336 9801 4294967295 134512640 134672761 3221224624 3221223776 134541817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10566 9801 603 41 0 10525 0
vsize: 42264
[startup+100.002 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 11023 0 0 0 9970 28 0 0 25 0 1 0 548894234 45572096 10354 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11126 10354 603 41 0 11085 0
vsize: 44504
[startup+110.003 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 11563 0 0 0 10969 30 0 0 25 0 1 0 548894234 47706112 10894 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11647 10894 603 41 0 11606 0
vsize: 46588
[startup+120.003 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 12177 0 0 0 11968 31 0 0 25 0 1 0 548894234 50262016 11508 4294967295 134512640 134672761 3221224624 3221223728 134560520 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12271 11508 603 41 0 12230 0
vsize: 49084
[startup+130.004 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 12911 0 0 0 12966 33 0 0 25 0 1 0 548894234 53219328 12242 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12993 12242 603 41 0 12952 0
vsize: 51972
[startup+140.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 13553 0 0 0 13965 35 0 0 25 0 1 0 548894234 55894016 12884 4294967295 134512640 134672761 3221224624 3221223808 134559503 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13646 12884 603 41 0 13605 0
vsize: 54584
[startup+150.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 14236 0 0 0 14963 36 0 0 25 0 1 0 548894234 58724352 13567 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14337 13567 603 41 0 14296 0
vsize: 57348
[startup+160.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 14843 0 0 0 15962 37 0 0 25 0 1 0 548894234 61284352 14174 4294967295 134512640 134672761 3221224624 3221223728 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14962 14174 603 41 0 14921 0
vsize: 59848
[startup+170.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 15453 0 0 0 16961 39 0 0 25 0 1 0 548894234 63713280 14784 4294967295 134512640 134672761 3221224624 3221223728 134554910 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15555 14784 603 41 0 15514 0
vsize: 62220
[startup+180.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 16060 0 0 0 17959 41 0 0 25 0 1 0 548894234 66269184 15391 4294967295 134512640 134672761 3221224624 3221223792 134561115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16179 15391 603 41 0 16138 0
vsize: 64716
[startup+190.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 16591 0 0 0 18957 43 0 0 25 0 1 0 548894234 68415488 15922 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16703 15922 603 41 0 16662 0
vsize: 66812
[startup+200.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 17287 0 0 0 19954 46 0 0 25 0 1 0 548894234 71249920 16618 4294967295 134512640 134672761 3221224624 3221223728 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17395 16618 603 41 0 17354 0
vsize: 69580
[startup+210.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 18063 0 0 0 20952 48 0 0 25 0 1 0 548894234 74493952 17394 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18187 17394 603 41 0 18146 0
vsize: 72748
[startup+220.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 18770 0 0 0 21951 50 0 0 25 0 1 0 548894234 77332480 18101 4294967295 134512640 134672761 3221224624 3221223728 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18880 18101 603 41 0 18839 0
vsize: 75520
[startup+230.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 19403 0 0 0 22949 53 0 0 25 0 1 0 548894234 79880192 18734 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19502 18734 603 41 0 19461 0
vsize: 78008
[startup+240.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 20033 0 0 0 23947 54 0 0 25 0 1 0 548894234 82444288 19364 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20128 19364 603 41 0 20087 0
vsize: 80512
[startup+250.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 20634 0 0 0 24945 56 0 0 25 0 1 0 548894234 84877312 19965 4294967295 134512640 134672761 3221224624 3221223728 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20722 19965 603 41 0 20681 0
vsize: 82888
[startup+260.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 21247 0 0 0 25944 58 0 0 25 0 1 0 548894234 87445504 20578 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21349 20578 603 41 0 21308 0
vsize: 85396
[startup+270.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 21718 0 0 0 26943 59 0 0 25 0 1 0 548894234 89337856 21049 4294967295 134512640 134672761 3221224624 3221223624 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21811 21049 603 41 0 21770 0
vsize: 87244
[startup+280.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 22222 0 0 0 27941 61 0 0 25 0 1 0 548894234 91492352 21553 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22337 21553 603 41 0 22296 0
vsize: 89348
[startup+290.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 22834 0 0 0 28940 62 0 0 25 0 1 0 548894234 93917184 22165 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22929 22165 603 41 0 22888 0
vsize: 91716
[startup+300.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 23447 0 0 0 29938 64 0 0 25 0 1 0 548894234 96460800 22778 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23550 22778 603 41 0 23509 0
vsize: 94200
[startup+310.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 23934 0 0 0 30937 65 0 0 25 0 1 0 548894234 98492416 23265 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24046 23265 603 41 0 24005 0
vsize: 96184
[startup+320.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 24407 0 0 0 31936 66 0 0 25 0 1 0 548894234 100630528 23738 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24568 23738 603 41 0 24527 0
vsize: 98272
[startup+330.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 24994 0 0 0 32935 68 0 0 25 0 1 0 548894234 103063552 24325 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25162 24325 603 41 0 25121 0
vsize: 100648
[startup+340.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 25436 0 0 0 33934 69 0 0 25 0 1 0 548894234 104800256 24767 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25586 24767 603 41 0 25545 0
vsize: 102344
[startup+350.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 26149 0 0 0 34932 70 0 0 25 0 1 0 548894234 107753472 25480 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26307 25480 603 41 0 26266 0
vsize: 105228
[startup+360.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 26898 0 0 0 35931 72 0 0 25 0 1 0 548894234 110866432 26229 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27067 26229 603 41 0 27026 0
vsize: 108268
[startup+370.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 27505 0 0 0 36929 74 0 0 25 0 1 0 548894234 113295360 26836 4294967295 134512640 134672761 3221224624 3221223792 134560797 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27660 26836 603 41 0 27619 0
vsize: 110640
[startup+380.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 27951 0 0 0 37929 74 0 0 25 0 1 0 548894234 115175424 27282 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28119 27282 603 41 0 28078 0
vsize: 112476
[startup+390.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 28319 0 0 0 38928 75 0 0 25 0 1 0 548894234 116654080 27650 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28480 27650 603 41 0 28439 0
vsize: 113920
[startup+400.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 28876 0 0 0 39927 77 0 0 25 0 1 0 548894234 118820864 28207 4294967295 134512640 134672761 3221224624 3221223808 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29009 28207 603 41 0 28968 0
vsize: 116036
[startup+410.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 29252 0 0 0 40926 78 0 0 25 0 1 0 548894234 120446976 28583 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29406 28583 603 41 0 29365 0
vsize: 117624
[startup+420.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 29768 0 0 0 41925 80 0 0 25 0 1 0 548894234 122470400 29099 4294967295 134512640 134672761 3221224624 3221223728 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29900 29099 603 41 0 29859 0
vsize: 119600
[startup+430.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 30335 0 0 0 42924 80 0 0 25 0 1 0 548894234 124772352 29666 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30462 29666 603 41 0 30421 0
vsize: 121848
[startup+440.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 30981 0 0 0 43921 82 0 0 25 0 1 0 548894234 127459328 30312 4294967295 134512640 134672761 3221224624 3221223728 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31118 30312 603 41 0 31077 0
vsize: 124472
[startup+450.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 31686 0 0 0 44919 85 0 0 25 0 1 0 548894234 130400256 31017 4294967295 134512640 134672761 3221224624 3221223728 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31836 31017 603 41 0 31795 0
vsize: 127344
[startup+460.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 32366 0 0 0 45917 87 0 0 25 0 1 0 548894234 133087232 31697 4294967295 134512640 134672761 3221224624 3221223760 134560604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32492 31697 603 41 0 32451 0
vsize: 129968
[startup+470.008 s]
Raw data (loadavg): 1.07 0.99 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 32956 0 0 0 46916 89 0 0 25 0 1 0 548894234 135503872 32287 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33082 32287 603 41 0 33041 0
vsize: 132328
[startup+480.009 s]
Raw data (loadavg): 1.14 1.01 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 33548 0 0 0 47915 90 0 0 25 0 1 0 548894234 137936896 32879 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33676 32879 603 41 0 33635 0
vsize: 134704
[startup+490.008 s]
Raw data (loadavg): 1.11 1.01 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 34140 0 0 0 48913 91 0 0 25 0 1 0 548894234 140386304 33471 4294967295 134512640 134672761 3221224624 3221223728 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34274 33471 603 41 0 34233 0
vsize: 137096
[startup+500.008 s]
Raw data (loadavg): 1.10 1.01 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 34629 0 0 0 49911 94 0 0 25 0 1 0 548894234 142430208 33960 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34773 33960 603 41 0 34732 0
vsize: 139092
[startup+510.008 s]
Raw data (loadavg): 1.08 1.01 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 35194 0 0 0 50910 95 0 0 25 0 1 0 548894234 144707584 34525 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35329 34525 603 41 0 35288 0
vsize: 141316
[startup+520.008 s]
Raw data (loadavg): 1.07 1.01 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 35560 0 0 0 51909 96 0 0 25 0 1 0 548894234 146186240 34891 4294967295 134512640 134672761 3221224624 3221223728 134560260 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35690 34891 603 41 0 35649 0
vsize: 142760
[startup+530.009 s]
Raw data (loadavg): 1.06 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 36121 0 0 0 52907 98 0 0 25 0 1 0 548894234 148488192 35452 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36252 35452 603 41 0 36211 0
vsize: 145008
[startup+540.009 s]
Raw data (loadavg): 1.05 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 36620 0 0 0 53907 99 0 0 25 0 1 0 548894234 150507520 35951 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36745 35951 603 41 0 36704 0
vsize: 146980
[startup+550.008 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 37088 0 0 0 54906 100 0 0 25 0 1 0 548894234 152399872 36419 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37207 36419 603 41 0 37166 0
vsize: 148828
[startup+560.009 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 37385 0 0 0 55906 101 0 0 25 0 1 0 548894234 153616384 36716 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37504 36716 603 41 0 37463 0
vsize: 150016
[startup+570.009 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 37773 0 0 0 56904 102 0 0 25 0 1 0 548894234 155246592 37104 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37902 37104 603 41 0 37861 0
vsize: 151608
[startup+580.009 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 38277 0 0 0 57903 103 0 0 25 0 1 0 548894234 157265920 37608 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38395 37608 603 41 0 38354 0
vsize: 153580
[startup+590.009 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 38828 0 0 0 58902 104 0 0 25 0 1 0 548894234 159567872 38159 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38957 38159 603 41 0 38916 0
vsize: 155828
[startup+600.009 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39419 0 0 0 59901 105 0 0 25 0 1 0 548894234 161992704 38750 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39549 38750 603 41 0 39508 0
vsize: 158196
[startup+610.009 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 60901 106 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+620.008 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 61902 106 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+630.01 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 62902 106 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+640.01 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 63902 106 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+650.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 64902 106 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223824 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+660.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 65902 106 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+670.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 66902 106 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134559883 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.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 67901 106 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+690.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 68901 106 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+700.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 69901 106 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+710.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 70901 106 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+720.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 71902 106 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+730.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 72902 106 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+740.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 73902 106 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134560158 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+750.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 74902 106 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+760.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 75902 106 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+770.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 76902 106 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+780.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 77903 106 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+790.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 78903 106 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+800.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 79903 106 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+810.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 80903 106 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+820.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 81903 106 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+830.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 82904 106 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+840.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 83904 106 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223808 134558352 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+850.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 84904 106 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+860.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 85904 106 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+870.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 86904 106 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134559896 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+880.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 87905 106 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+890.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 88905 106 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+900.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 89905 106 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+910.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 90905 106 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223808 134559564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+920.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 91905 106 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223760 134565039 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+930.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 92906 106 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134560160 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+940.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 93906 107 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+950.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 94906 107 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+960.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 95906 107 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+970.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 96906 107 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+980.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 97906 107 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+990.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 98906 107 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+1000.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 99906 107 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+1010.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 100907 107 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+1020.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 101907 107 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+1030.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 102907 107 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+1040.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 103907 107 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+1050.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 104907 107 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223728 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 105907 107 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134561167 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.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 106906 108 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+1080.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 107906 108 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 108907 108 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134560825 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+1100.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39541 0 0 0 109907 108 0 0 25 0 1 0 548894234 162398208 38872 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39648 38872 603 41 0 39607 0
vsize: 158592
[startup+1110.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39566 0 0 0 110907 108 0 0 25 0 1 0 548894234 162537472 38897 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39682 38897 603 41 0 39641 0
vsize: 158728
[startup+1120.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 39846 0 0 0 111906 109 0 0 25 0 1 0 548894234 163753984 39177 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39979 39177 603 41 0 39938 0
vsize: 159916
[startup+1130.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 40293 0 0 0 112905 110 0 0 25 0 1 0 548894234 165507072 39624 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40407 39624 603 41 0 40366 0
vsize: 161628
[startup+1140.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 40852 0 0 0 113904 112 0 0 25 0 1 0 548894234 167796736 40183 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40966 40183 603 41 0 40925 0
vsize: 163864
[startup+1150.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 41494 0 0 0 114902 113 0 0 25 0 1 0 548894234 170475520 40825 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41620 40825 603 41 0 41579 0
vsize: 166480
[startup+1160.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 41966 0 0 0 115902 114 0 0 25 0 1 0 548894234 172343296 41297 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42076 41297 603 41 0 42035 0
vsize: 168304
[startup+1170.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 42460 0 0 0 116901 115 0 0 25 0 1 0 548894234 174366720 41791 4294967295 134512640 134672761 3221224624 3221223808 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42570 41791 603 41 0 42529 0
vsize: 170280
[startup+1180.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 42922 0 0 0 117900 116 0 0 25 0 1 0 548894234 176242688 42253 4294967295 134512640 134672761 3221224624 3221223556 1074972064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43028 42253 603 41 0 42987 0
vsize: 172112
[startup+1190.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 43563 0 0 0 118899 118 0 0 25 0 1 0 548894234 178946048 42894 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43688 42894 603 41 0 43647 0
vsize: 174752
[startup+1200.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15592
Raw data (stat): 15590 (minisat+) R 15589 3260 3259 0 -1 0 44295 0 0 0 119898 119 0 0 25 0 1 0 548894234 181919744 43626 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44414 43626 603 41 0 44373 0
vsize: 177656
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 15592
Raw data (stat): 15590 (minisat+) Z 15589 3260 3259 0 -1 12 44297 0 0 0 119898 127 0 0 25 0 1 0 548894234 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.1
CPU time (s): 1200.26
CPU user time (s): 1198.98
CPU system time (s): 1.27581
CPU usage (%): 100.013
Max. virtual memory (Kb): 177656
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####