PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-mod010.opb
MD5SUM	ef7064a9be2b712276f7b600af28e2b0
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	6571
Optimality of the best value was proved	NO
Number of terms in the objective function	2655
Biggest coefficient in the objective function	266
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	489211
Number of bits of the sum of numbers in the objective function	19
Biggest number in a constraint	266
Number of bits of the biggest number in a constraint	9
Biggest sum of numbers in a constraint	489211
Number of bits of the biggest sum of numbers	19
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.18
Number of variables	2655
Total number of constraints	2801
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	2800
Number of constraints which are nor clauses,nor cardinality constraints	1
Minimum length of a constraint	1
Maximum length of a constraint	2655
Trace number 18066

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc10 THE 2005-04-21 13:18:54 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18642 boxname=wulflinc10 idbench=1434 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ef7064a9be2b712276f7b600af28e2b0  /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-mod010.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-mod010.opb /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-mod010.opb
IDLAUNCH: 18642
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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	: 2
cpu MHz		: 450.999
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:        743000 kB
Buffers:         27804 kB
Cached:         242020 kB
SwapCached:          0 kB
Active:          28176 kB
Inactive:       244188 kB
HighTotal:      131008 kB
HighFree:        82264 kB
LowTotal:       903652 kB
LowFree:        660736 kB
SwapTotal:     2097136 kB
SwapFree:      2096784 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6412 kB
Slab:            13888 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 13:38:57 (client local time) WITH STATUS 0 IN 1200.3 SECONDS
stats: 18642 7 1200.3 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 291 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 289]---> BDD-cost:   67
c ---[ 287]---> BDD-cost:  113
c ---[ 285]---> BDD-cost:  181
c ---[ 283]---> BDD-cost:  115
c ---[ 281]---> BDD-cost:   69
c ---[ 279]---> BDD-cost:  125
c ---[ 277]---> BDD-cost:  155
c ---[ 275]---> BDD-cost:   87
c ---[ 273]---> BDD-cost:   97
c ---[ 271]---> BDD-cost:   73
c ---[ 269]---> BDD-cost:  119
c ---[ 267]---> BDD-cost:   45
c ---[ 265]---> BDD-cost:  171
c ---[ 263]---> BDD-cost:  111
c ---[ 261]---> BDD-cost:  149
c ---[ 259]---> BDD-cost:  195
c ---[ 257]---> BDD-cost:  131
c ---[ 255]---> BDD-cost:  123
c ---[ 253]---> BDD-cost:  167
c ---[ 251]---> BDD-cost:  101
c ---[ 249]---> BDD-cost:   97
c ---[ 247]---> BDD-cost:   23
c ---[ 245]---> BDD-cost:  135
c ---[ 243]---> BDD-cost:   59
c ---[ 241]---> BDD-cost:   95
c ---[ 239]---> BDD-cost:   59
c ---[ 237]---> BDD-cost:  133
c ---[ 235]---> BDD-cost:   99
c ---[ 233]---> BDD-cost:  179
c ---[ 231]---> BDD-cost:  111
c ---[ 229]---> BDD-cost:   23
c ---[ 227]---> BDD-cost:   89
c ---[ 225]---> BDD-cost:   95
c ---[ 223]---> BDD-cost:  117
c ---[ 221]---> BDD-cost:   23
c ---[ 219]---> BDD-cost:   51
c ---[ 217]---> BDD-cost:  311
c ---[ 215]---> BDD-cost:  259
c ---[ 213]---> BDD-cost:  169
c ---[ 211]---> BDD-cost:  131
c ---[ 209]---> BDD-cost:  155
c ---[ 207]---> BDD-cost:   89
c ---[ 205]---> BDD-cost:   51
c ---[ 203]---> BDD-cost:  165
c ---[ 201]---> BDD-cost:   75
c ---[ 199]---> BDD-cost:  139
c ---[ 197]---> BDD-cost:   67
c ---[ 195]---> BDD-cost:  173
c ---[ 193]---> BDD-cost:  235
c ---[ 191]---> BDD-cost:  185
c ---[ 189]---> BDD-cost:  127
c ---[ 187]---> BDD-cost:   37
c ---[ 185]---> BDD-cost:   37
c ---[ 183]---> BDD-cost:   91
c ---[ 181]---> BDD-cost:   77
c ---[ 179]---> BDD-cost:   29
c ---[ 177]---> BDD-cost:   77
c ---[ 175]---> BDD-cost:   77
c ---[ 173]---> BDD-cost:  101
c ---[ 171]---> BDD-cost:  131
c ---[ 169]---> BDD-cost:  155
c ---[ 167]---> BDD-cost:  177
c ---[ 165]---> BDD-cost:  143
c ---[ 163]---> BDD-cost:   93
c ---[ 161]---> BDD-cost:   79
c ---[ 159]---> BDD-cost:   53
c ---[ 157]---> BDD-cost:   71
c ---[ 155]---> BDD-cost:  127
c ---[ 153]---> BDD-cost:  127
c ---[ 151]---> BDD-cost:   67
c ---[ 149]---> BDD-cost:   83
c ---[ 147]---> BDD-cost:   47
c ---[ 145]---> BDD-cost:   63
c ---[ 143]---> BDD-cost:  121
c ---[ 141]---> BDD-cost:  155
c ---[ 139]---> BDD-cost:   87
c ---[ 137]---> BDD-cost:   91
c ---[ 135]---> BDD-cost:   47
c ---[ 133]---> BDD-cost:   67
c ---[ 131]---> BDD-cost:   33
c ---[ 129]---> BDD-cost:   91
c ---[ 127]---> BDD-cost:   69
c ---[ 125]---> BDD-cost:    5
c ---[ 123]---> BDD-cost:   47
c ---[ 121]---> BDD-cost:   45
c ---[ 119]---> BDD-cost:   37
c ---[ 117]---> BDD-cost:  117
c ---[ 115]---> BDD-cost:   97
c ---[ 113]---> BDD-cost:   77
c ---[ 111]---> BDD-cost:   97
c ---[ 109]---> BDD-cost:  137
c ---[ 107]---> BDD-cost:  125
c ---[ 105]---> BDD-cost:   79
c ---[ 103]---> BDD-cost:  133
c ---[ 101]---> BDD-cost:  153
c ---[  99]---> BDD-cost:  139
c ---[  97]---> BDD-cost:  125
c ---[  95]---> BDD-cost:    5
c ---[  93]---> BDD-cost:   73
c ---[  91]---> BDD-cost:  157
c ---[  89]---> BDD-cost:  127
c ---[  87]---> BDD-cost:  199
c ---[  85]---> BDD-cost:  121
c ---[  83]---> BDD-cost:  107
c ---[  81]---> BDD-cost:  169
c ---[  79]---> BDD-cost:  113
c ---[  77]---> BDD-cost:  103
c ---[  75]---> BDD-cost:   75
c ---[  73]---> BDD-cost:   97
c ---[  71]---> BDD-cost:  151
c ---[  69]---> BDD-cost:  199
c ---[  67]---> BDD-cost:  109
c ---[  65]---> BDD-cost:  131
c ---[  63]---> BDD-cost:  113
c ---[  61]---> BDD-cost:  173
c ---[  59]---> BDD-cost:  119
c ---[  57]---> BDD-cost:  173
c ---[  55]---> BDD-cost:  119
c ---[  53]---> BDD-cost:   71
c ---[  51]---> BDD-cost:  179
c ---[  49]---> BDD-cost:  241
c ---[  47]---> BDD-cost:  201
c ---[  45]---> BDD-cost:  173
c ---[  43]---> BDD-cost:  147
c ---[  41]---> BDD-cost:  157
c ---[  39]---> BDD-cost:  201
c ---[  37]---> BDD-cost:  129
c ---[  35]---> BDD-cost:  117
c ---[  33]---> BDD-cost:  177
c ---[  31]---> BDD-cost:  123
c ---[  29]---> BDD-cost:  131
c ---[  27]---> BDD-cost:  115
c ---[  25]---> BDD-cost:   51
c ---[  23]---> BDD-cost:  123
c ---[  21]---> BDD-cost:   55
c ---[  19]---> BDD-cost:    5
c ---[  17]---> BDD-cost:   99
c ---[  15]---> BDD-cost:   85
c ---[  13]---> BDD-cost:  109
c ---[  11]---> BDD-cost:  153
c ---[   9]---> BDD-cost:  201
c ---[   7]---> BDD-cost:  133
c ---[   5]---> BDD-cost:  121
c ---[   3]---> BDD-cost:  171
c ---[   1]---> Adder-cost: 5294   maxlim: 2609   bits: 12/12
c ---[   0]---> BDD-cost:  751
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  112641   342501 |   37547       0        0     nan |  0.000 % |
c |       100 |  112566   342248 |   41301      93      747     8.0 |  0.739 % |
c |       251 |  112566   342248 |   45431     244     4453    18.2 |  0.739 % |
c |       477 |  112566   342248 |   49975     470    15059    32.0 |  0.739 % |
c |       819 |  112566   342248 |   54972     812    37441    46.1 |  0.739 % |
c |      1331 |  112566   342248 |   60469    1324    71852    54.3 |  0.739 % |
c |      2095 |  112566   342248 |   66516    2088   201139    96.3 |  0.739 % |
c |      3235 |  112566   342248 |   73168    3228   326074   101.0 |  0.739 % |
c |      4943 |  112537   342164 |   80485    4914   477218    97.1 |  0.751 % |
c |      7505 |  112537   342164 |   88533    7476  1210959   162.0 |  0.751 % |
c |     11350 |  112537   342164 |   97387   11321  1873735   165.5 |  0.751 % |
c |     17116 |  112537   342164 |  107125   17087  3521450   206.1 |  0.751 % |
c |     25767 |  112512   342081 |  117838   25734  4545362   176.6 |  0.767 % |
c |     38741 |  112460   341924 |  129622   38597  6644314   172.1 |  0.783 % |
c |     58202 |  112449   341881 |  142584   58057 12905884   222.3 |  0.791 % |
c |     87396 |  112356   341607 |  156843   87217 24567040   281.7 |  0.823 % |
c |    131185 |  112327   341502 |  172527  131001 48087197   367.1 |  0.840 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.93 0.98 0.93 2/54 32019
Raw data (stat): 32019 (runsolver) R 32018 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487170581 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.94 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 5603 0 0 0 984 14 0 0 25 0 1 0 487170581 22962176 4934 4294967295 134512640 134672761 3221224544 3221223728 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5606 4934 603 41 0 5565 0
vsize: 22424
[startup+20.0008 s]
Raw data (loadavg): 0.95 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 6117 0 0 0 1982 15 0 0 25 0 1 0 487170581 25116672 5448 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6132 5448 603 41 0 6091 0
vsize: 24528
[startup+30.0012 s]
Raw data (loadavg): 0.95 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 6674 0 0 0 2981 17 0 0 25 0 1 0 487170581 27410432 6005 4294967295 134512640 134672761 3221224544 3221223648 134560237 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6692 6005 603 41 0 6651 0
vsize: 26768
[startup+40.0012 s]
Raw data (loadavg): 0.96 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 7325 0 0 0 3979 18 0 0 25 0 1 0 487170581 30113792 6656 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7352 6656 603 41 0 7311 0
vsize: 29408
[startup+50.0018 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 8070 0 0 0 4977 20 0 0 25 0 1 0 487170581 33087488 7401 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8078 7401 603 41 0 8037 0
vsize: 32312
[startup+60.0018 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 8746 0 0 0 5974 22 0 0 25 0 1 0 487170581 35917824 8077 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8769 8077 603 41 0 8728 0
vsize: 35076
[startup+70.002 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 9387 0 0 0 6972 24 0 0 25 0 1 0 487170581 38502400 8718 4294967295 134512640 134672761 3221224544 3221223648 134560008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9400 8718 603 41 0 9359 0
vsize: 37600
[startup+80.0022 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 9867 0 0 0 7971 25 0 0 25 0 1 0 487170581 40521728 9198 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9893 9198 603 41 0 9852 0
vsize: 39572
[startup+90.0014 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 10255 0 0 0 8970 27 0 0 25 0 1 0 487170581 42131456 9586 4294967295 134512640 134672761 3221224544 3221223648 134560501 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10286 9586 603 41 0 10245 0
vsize: 41144
[startup+100.001 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 10734 0 0 0 9968 28 0 0 25 0 1 0 487170581 44019712 10065 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10747 10065 603 41 0 10706 0
vsize: 42988
[startup+110.002 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 11302 0 0 0 10967 30 0 0 25 0 1 0 487170581 46309376 10633 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11306 10633 603 41 0 11265 0
vsize: 45224
[startup+120.001 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 11737 0 0 0 11966 31 0 0 25 0 1 0 487170581 48189440 11068 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11765 11068 603 41 0 11724 0
vsize: 47060
[startup+130.001 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 12298 0 0 0 12965 32 0 0 25 0 1 0 487170581 50601984 11629 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12354 11629 603 41 0 12313 0
vsize: 49416
[startup+140.002 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 12777 0 0 0 13963 34 0 0 25 0 1 0 487170581 52486144 12108 4294967295 134512640 134672761 3221224544 3221223648 134560477 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12814 12108 603 41 0 12773 0
vsize: 51256
[startup+150.001 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 13466 0 0 0 14962 36 0 0 25 0 1 0 487170581 55345152 12797 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13512 12797 603 41 0 13471 0
vsize: 54048
[startup+160.001 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 14006 0 0 0 15960 38 0 0 25 0 1 0 487170581 57495552 13337 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14037 13337 603 41 0 13996 0
vsize: 56148
[startup+170.001 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 14607 0 0 0 16958 40 0 0 25 0 1 0 487170581 59899904 13938 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14624 13938 603 41 0 14583 0
vsize: 58496
[startup+180.002 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 15192 0 0 0 17957 41 0 0 25 0 1 0 487170581 62308352 14523 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15212 14523 603 41 0 15171 0
vsize: 60848
[startup+190.001 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 15829 0 0 0 18955 43 0 0 25 0 1 0 487170581 64991232 15160 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15867 15160 603 41 0 15826 0
vsize: 63468
[startup+200.001 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 16615 0 0 0 19953 46 0 0 25 0 1 0 487170581 68165632 15946 4294967295 134512640 134672761 3221224544 3221223648 134560010 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16642 15946 603 41 0 16601 0
vsize: 66568
[startup+210.002 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 17233 0 0 0 20951 48 0 0 25 0 1 0 487170581 70717440 16564 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17265 16564 603 41 0 17224 0
vsize: 69060
[startup+220.001 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 17858 0 0 0 21949 50 0 0 25 0 1 0 487170581 73273344 17189 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17889 17189 603 41 0 17848 0
vsize: 71556
[startup+230.002 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 18387 0 0 0 22948 51 0 0 25 0 1 0 487170581 75440128 17718 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18418 17718 603 41 0 18377 0
vsize: 73672
[startup+240.001 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 18873 0 0 0 23947 53 0 0 25 0 1 0 487170581 77332480 18204 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18880 18204 603 41 0 18839 0
vsize: 75520
[startup+250.001 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 19420 0 0 0 24945 54 0 0 25 0 1 0 487170581 79613952 18751 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19437 18751 603 41 0 19396 0
vsize: 77748
[startup+260.001 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 20136 0 0 0 25943 57 0 0 25 0 1 0 487170581 82587648 19467 4294967295 134512640 134672761 3221224544 3221223648 134559958 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20163 19467 603 41 0 20122 0
vsize: 80652
[startup+270.002 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 20912 0 0 0 26941 59 0 0 25 0 1 0 487170581 85688320 20243 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20920 20243 603 41 0 20879 0
vsize: 83680
[startup+280.002 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 21603 0 0 0 27939 61 0 0 25 0 1 0 487170581 88481792 20934 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21602 20934 603 41 0 21561 0
vsize: 86408
[startup+290.002 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 22417 0 0 0 28937 63 0 0 25 0 1 0 487170581 92119040 21748 4294967295 134512640 134672761 3221224544 3221223616 134553549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22490 21748 603 41 0 22449 0
vsize: 89960
[startup+300.002 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 23003 0 0 0 29935 65 0 0 25 0 1 0 487170581 94556160 22334 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23085 22334 603 41 0 23044 0
vsize: 92340
[startup+310.002 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 23688 0 0 0 30934 67 0 0 25 0 1 0 487170581 97370112 23019 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23772 23019 603 41 0 23731 0
vsize: 95088
[startup+320.002 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 24331 0 0 0 31932 68 0 0 25 0 1 0 487170581 99946496 23662 4294967295 134512640 134672761 3221224544 3221223648 134559841 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24401 23662 603 41 0 24360 0
vsize: 97604
[startup+330.002 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 25105 0 0 0 32931 70 0 0 25 0 1 0 487170581 103067648 24436 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25163 24436 603 41 0 25122 0
vsize: 100652
[startup+340.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 25669 0 0 0 33929 72 0 0 25 0 1 0 487170581 105361408 25000 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25723 25000 603 41 0 25682 0
vsize: 102892
[startup+350.002 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 26280 0 0 0 34928 74 0 0 25 0 1 0 487170581 107917312 25611 4294967295 134512640 134672761 3221224544 3221223648 134559835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26347 25611 603 41 0 26306 0
vsize: 105388
[startup+360.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 26790 0 0 0 35926 76 0 0 25 0 1 0 487170581 109940736 26121 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26841 26121 603 41 0 26800 0
vsize: 107364
[startup+370.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 27328 0 0 0 36925 77 0 0 25 0 1 0 487170581 112234496 26659 4294967295 134512640 134672761 3221224544 3221223648 134560350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27401 26659 603 41 0 27360 0
vsize: 109604
[startup+380.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 27761 0 0 0 37925 78 0 0 25 0 1 0 487170581 113991680 27092 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27830 27092 603 41 0 27789 0
vsize: 111320
[startup+390.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 28174 0 0 0 38924 79 0 0 25 0 1 0 487170581 115609600 27505 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28225 27505 603 41 0 28184 0
vsize: 112900
[startup+400.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 28862 0 0 0 39921 81 0 0 25 0 1 0 487170581 118444032 28193 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28917 28193 603 41 0 28876 0
vsize: 115668
[startup+410.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 29560 0 0 0 40920 83 0 0 25 0 1 0 487170581 121282560 28891 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29610 28891 603 41 0 29569 0
vsize: 118440
[startup+420.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 30245 0 0 0 41918 85 0 0 25 0 1 0 487170581 124108800 29576 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30300 29576 603 41 0 30259 0
vsize: 121200
[startup+430.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 30812 0 0 0 42916 87 0 0 25 0 1 0 487170581 126382080 30143 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30855 30143 603 41 0 30814 0
vsize: 123420
[startup+440.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 31335 0 0 0 43915 88 0 0 25 0 1 0 487170581 128540672 30666 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31382 30666 603 41 0 31341 0
vsize: 125528
[startup+450.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 32022 0 0 0 44913 89 0 0 25 0 1 0 487170581 131383296 31353 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32076 31353 603 41 0 32035 0
vsize: 128304
[startup+460.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 32246 0 0 0 45913 90 0 0 25 0 1 0 487170581 132329472 31577 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32307 31577 603 41 0 32266 0
vsize: 129228
[startup+470.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 32752 0 0 0 46912 90 0 0 25 0 1 0 487170581 134352896 32083 4294967295 134512640 134672761 3221224544 3221223648 134559835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32801 32083 603 41 0 32760 0
vsize: 131204
[startup+480.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 33341 0 0 0 47911 92 0 0 25 0 1 0 487170581 136773632 32672 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33392 32672 603 41 0 33351 0
vsize: 133568
[startup+490.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 33909 0 0 0 48910 93 0 0 25 0 1 0 487170581 139055104 33240 4294967295 134512640 134672761 3221224544 3221223648 134559969 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33949 33240 603 41 0 33908 0
vsize: 135796
[startup+500.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 34510 0 0 0 49908 95 0 0 25 0 1 0 487170581 141598720 33841 4294967295 134512640 134672761 3221224544 3221223648 134560154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34570 33841 603 41 0 34529 0
vsize: 138280
[startup+510.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 35091 0 0 0 50906 97 0 0 25 0 1 0 487170581 143892480 34422 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35130 34422 603 41 0 35089 0
vsize: 140520
[startup+520.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 35854 0 0 0 51905 98 0 0 25 0 1 0 487170581 146997248 35185 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35888 35185 603 41 0 35847 0
vsize: 143552
[startup+530.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 36515 0 0 0 52904 100 0 0 25 0 1 0 487170581 149696512 35846 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36547 35846 603 41 0 36506 0
vsize: 146188
[startup+540.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 37201 0 0 0 53902 102 0 0 25 0 1 0 487170581 152588288 36532 4294967295 134512640 134672761 3221224544 3221223648 134559976 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37253 36532 603 41 0 37212 0
vsize: 149012
[startup+550.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 37648 0 0 0 54901 103 0 0 25 0 1 0 487170581 154333184 36979 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37679 36979 603 41 0 37638 0
vsize: 150716
[startup+560.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 38107 0 0 0 55900 105 0 0 25 0 1 0 487170581 156217344 37438 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38139 37438 603 41 0 38098 0
vsize: 152556
[startup+570.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 38580 0 0 0 56899 106 0 0 25 0 1 0 487170581 158109696 37911 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38601 37911 603 41 0 38560 0
vsize: 154404
[startup+580.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 38956 0 0 0 57898 106 0 0 25 0 1 0 487170581 159735808 38287 4294967295 134512640 134672761 3221224544 3221223648 134560008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38998 38287 603 41 0 38957 0
vsize: 155992
[startup+590.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 39598 0 0 0 58897 108 0 0 25 0 1 0 487170581 162263040 38929 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39615 38929 603 41 0 39574 0
vsize: 158460
[startup+600.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 40215 0 0 0 59895 110 0 0 25 0 1 0 487170581 164810752 39546 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40237 39546 603 41 0 40196 0
vsize: 160948
[startup+610.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 40811 0 0 0 60894 111 0 0 25 0 1 0 487170581 167223296 40142 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40826 40142 603 41 0 40785 0
vsize: 163304
[startup+620.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 41453 0 0 0 61894 112 0 0 25 0 1 0 487170581 169885696 40784 4294967295 134512640 134672761 3221224544 3221223648 134559964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41476 40784 603 41 0 41435 0
vsize: 165904
[startup+630.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 42074 0 0 0 62892 114 0 0 25 0 1 0 487170581 172429312 41405 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42097 41405 603 41 0 42056 0
vsize: 168388
[startup+640.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 42572 0 0 0 63891 115 0 0 25 0 1 0 487170581 174432256 41903 4294967295 134512640 134672761 3221224544 3221223648 134560059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42586 41903 603 41 0 42545 0
vsize: 170344
[startup+650.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 43288 0 0 0 64889 117 0 0 25 0 1 0 487170581 177397760 42619 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43310 42619 603 41 0 43269 0
vsize: 173240
[startup+660.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 44009 0 0 0 65888 118 0 0 25 0 1 0 487170581 180363264 43340 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44034 43340 603 41 0 43993 0
vsize: 176136
[startup+670.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 44721 0 0 0 66886 121 0 0 25 0 1 0 487170581 183320576 44052 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44756 44052 603 41 0 44715 0
vsize: 179024
[startup+680.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 45392 0 0 0 67884 123 0 0 25 0 1 0 487170581 186036224 44723 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45419 44723 603 41 0 45378 0
vsize: 181676
[startup+690.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 46046 0 0 0 68882 124 0 0 25 0 1 0 487170581 188743680 45377 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46080 45377 603 41 0 46039 0
vsize: 184320
[startup+700.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 46685 0 0 0 69881 126 0 0 25 0 1 0 487170581 191291392 46016 4294967295 134512640 134672761 3221224544 3221223648 134560005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46702 46016 603 41 0 46661 0
vsize: 186808
[startup+710.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 47294 0 0 0 70881 126 0 0 25 0 1 0 487170581 193851392 46625 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47327 46625 603 41 0 47286 0
vsize: 189308
[startup+720.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 47895 0 0 0 71880 127 0 0 25 0 1 0 487170581 196284416 47226 4294967295 134512640 134672761 3221224544 3221223648 134560399 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47921 47226 603 41 0 47880 0
vsize: 191684
[startup+730.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 48537 0 0 0 72879 128 0 0 25 0 1 0 487170581 198844416 47868 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48546 47868 603 41 0 48505 0
vsize: 194184
[startup+740.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 49172 0 0 0 73877 131 0 0 25 0 1 0 487170581 201555968 48503 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49208 48503 603 41 0 49167 0
vsize: 196832
[startup+750.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 49789 0 0 0 74876 132 0 0 25 0 1 0 487170581 204005376 49120 4294967295 134512640 134672761 3221224544 3221223648 134559933 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49806 49120 603 41 0 49765 0
vsize: 199224
[startup+760.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 50410 0 0 0 75874 134 0 0 25 0 1 0 487170581 206565376 49741 4294967295 134512640 134672761 3221224544 3221223648 134559927 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50431 49741 603 41 0 50390 0
vsize: 201724
[startup+770.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 51006 0 0 0 76873 135 0 0 25 0 1 0 487170581 209002496 50337 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51026 50337 603 41 0 50985 0
vsize: 204104
[startup+780.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 51603 0 0 0 77872 137 0 0 25 0 1 0 487170581 211546112 50934 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51647 50934 603 41 0 51606 0
vsize: 206588
[startup+790.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 52219 0 0 0 78870 139 0 0 25 0 1 0 487170581 213975040 51550 4294967295 134512640 134672761 3221224544 3221223648 134559927 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52240 51550 603 41 0 52199 0
vsize: 208960
[startup+800.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 52797 0 0 0 79869 140 0 0 25 0 1 0 487170581 216416256 52128 4294967295 134512640 134672761 3221224544 3221223648 134560059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52836 52128 603 41 0 52795 0
vsize: 211344
[startup+810.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 53414 0 0 0 80868 141 0 0 25 0 1 0 487170581 218841088 52745 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53428 52745 603 41 0 53387 0
vsize: 213712
[startup+820.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 53998 0 0 0 81866 143 0 0 25 0 1 0 487170581 221265920 53329 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54020 53329 603 41 0 53979 0
vsize: 216080
[startup+830.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 54577 0 0 0 82864 145 0 0 25 0 1 0 487170581 224215040 53908 4294967295 134512640 134672761 3221224544 3221223648 134560059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54740 53908 603 41 0 54699 0
vsize: 218960
[startup+840.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 55280 0 0 0 83861 148 0 0 25 0 1 0 487170581 227008512 54611 4294967295 134512640 134672761 3221224544 3221223648 134559998 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55422 54611 603 41 0 55381 0
vsize: 221688
[startup+850.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 55722 0 0 0 84860 150 0 0 25 0 1 0 487170581 228880384 55053 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55879 55053 603 41 0 55838 0
vsize: 223516
[startup+860.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 56084 0 0 0 85859 150 0 0 25 0 1 0 487170581 230350848 55415 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56238 55415 603 41 0 56197 0
vsize: 224952
[startup+870.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 56326 0 0 0 86859 151 0 0 25 0 1 0 487170581 231280640 55657 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56465 55657 603 41 0 56424 0
vsize: 225860
[startup+880.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 56816 0 0 0 87858 152 0 0 25 0 1 0 487170581 233299968 56147 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56958 56147 603 41 0 56917 0
vsize: 227832
[startup+890.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 57470 0 0 0 88857 154 0 0 25 0 1 0 487170581 235986944 56801 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57614 56801 603 41 0 57573 0
vsize: 230456
[startup+900.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 58145 0 0 0 89855 155 0 0 25 0 1 0 487170581 238817280 57476 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58305 57476 603 41 0 58264 0
vsize: 233220
[startup+910.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 58632 0 0 0 90854 157 0 0 25 0 1 0 487170581 240717824 57963 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58769 57963 603 41 0 58728 0
vsize: 235076
[startup+920.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 58891 0 0 0 91854 157 0 0 25 0 1 0 487170581 241795072 58222 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59032 58222 603 41 0 58991 0
vsize: 236128
[startup+930.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 59350 0 0 0 92853 158 0 0 25 0 1 0 487170581 243679232 58681 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59492 58681 603 41 0 59451 0
vsize: 237968
[startup+940.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 59441 0 0 0 93853 158 0 0 25 0 1 0 487170581 244084736 58772 4294967295 134512640 134672761 3221224544 3221223648 134560379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59591 58772 603 41 0 59550 0
vsize: 238364
[startup+950.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 60002 0 0 0 94851 160 0 0 25 0 1 0 487170581 246407168 59333 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60158 59333 603 41 0 60117 0
vsize: 240632
[startup+960.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 60369 0 0 0 95851 161 0 0 25 0 1 0 487170581 247889920 59700 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60520 59700 603 41 0 60479 0
vsize: 242080
[startup+970.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 60802 0 0 0 96850 162 0 0 25 0 1 0 487170581 249638912 60133 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60947 60133 603 41 0 60906 0
vsize: 243788
[startup+980.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 61449 0 0 0 97848 164 0 0 25 0 1 0 487170581 252313600 60780 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61600 60780 603 41 0 61559 0
vsize: 246400
[startup+990.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 62047 0 0 0 98846 166 0 0 25 0 1 0 487170581 254746624 61378 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62194 61378 603 41 0 62153 0
vsize: 248776
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 62474 0 0 0 99845 167 0 0 25 0 1 0 487170581 256499712 61805 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62622 61805 603 41 0 62581 0
vsize: 250488
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 62865 0 0 0 100844 169 0 0 25 0 1 0 487170581 257982464 62196 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62984 62196 603 41 0 62943 0
vsize: 251936
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 63272 0 0 0 101844 169 0 0 25 0 1 0 487170581 259723264 62603 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63409 62603 603 41 0 63368 0
vsize: 253636
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 63761 0 0 0 102842 171 0 0 25 0 1 0 487170581 261718016 63092 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63896 63092 603 41 0 63855 0
vsize: 255584
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 64352 0 0 0 103841 172 0 0 25 0 1 0 487170581 264069120 63683 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64470 63683 603 41 0 64429 0
vsize: 257880
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 64928 0 0 0 104839 174 0 0 25 0 1 0 487170581 266452992 64259 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65052 64259 603 41 0 65011 0
vsize: 260208
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 65483 0 0 0 105838 175 0 0 25 0 1 0 487170581 268718080 64814 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65605 64814 603 41 0 65564 0
vsize: 262420
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 65796 0 0 0 106838 176 0 0 25 0 1 0 487170581 270036992 65127 4294967295 134512640 134672761 3221224544 3221223648 134559866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65927 65127 603 41 0 65886 0
vsize: 263708
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 65912 0 0 0 107837 177 0 0 25 0 1 0 487170581 270438400 65243 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66025 65243 603 41 0 65984 0
vsize: 264100
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 66435 0 0 0 108836 178 0 0 25 0 1 0 487170581 272592896 65766 4294967295 134512640 134672761 3221224544 3221223648 134560252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66551 65766 603 41 0 66510 0
vsize: 266204
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 66962 0 0 0 109835 179 0 0 25 0 1 0 487170581 274743296 66293 4294967295 134512640 134672761 3221224544 3221223648 134559958 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67076 66293 603 41 0 67035 0
vsize: 268304
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 67457 0 0 0 110833 181 0 0 25 0 1 0 487170581 276770816 66788 4294967295 134512640 134672761 3221224544 3221223728 134559332 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67571 66788 603 41 0 67530 0
vsize: 270284
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 67931 0 0 0 111832 183 0 0 25 0 1 0 487170581 278794240 67262 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68065 67262 603 41 0 68024 0
vsize: 272260
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 68244 0 0 0 112832 183 0 0 25 0 1 0 487170581 280014848 67575 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68363 67575 603 41 0 68322 0
vsize: 273452
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 68782 0 0 0 113830 185 0 0 25 0 1 0 487170581 282284032 68113 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68917 68113 603 41 0 68876 0
vsize: 275668
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 69265 0 0 0 114829 186 0 0 25 0 1 0 487170581 284147712 68596 4294967295 134512640 134672761 3221224544 3221223648 134560248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69372 68596 603 41 0 69331 0
vsize: 277488
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 69770 0 0 0 115828 188 0 0 25 0 1 0 487170581 286289920 69101 4294967295 134512640 134672761 3221224544 3221223648 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69895 69101 603 41 0 69854 0
vsize: 279580
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 70215 0 0 0 116826 190 0 0 25 0 1 0 487170581 288030720 69546 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70320 69546 603 41 0 70279 0
vsize: 281280
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 70602 0 0 0 117825 191 0 0 25 0 1 0 487170581 289648640 69933 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70715 69933 603 41 0 70674 0
vsize: 282860
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 70835 0 0 0 118825 192 0 0 25 0 1 0 487170581 290598912 70166 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70947 70166 603 41 0 70906 0
vsize: 283788
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 32019
Raw data (stat): 32019 (minisat+) R 32018 25347 25346 0 -1 0 71108 0 0 0 119824 192 0 0 25 0 1 0 487170581 291672064 70439 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71209 70439 603 41 0 71168 0
vsize: 284836
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.14 s]
Raw data (loadavg): 0.99 0.98 0.93 1/54 32019
Raw data (stat): 32019 (minisat+) Z 32018 25347 25346 0 -1 12 71110 0 0 0 119824 205 0 0 25 0 1 0 487170581 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.14
CPU time (s): 1200.3
CPU user time (s): 1198.25
CPU system time (s): 2.05569
CPU usage (%): 100.013
Max. virtual memory (Kb): 284836
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####