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/web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-10:10:4.5:0.95:98.opb
MD5SUM	ac510382bae6003fe0373ad32fd0064f
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	5
Optimality of the best value was proved	NO
Number of terms in the objective function	411
Biggest coefficient in the objective function	268
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	1129
Number of bits of the sum of numbers in the objective function	11
Biggest number in a constraint	268
Number of bits of the biggest number in a constraint	9
Biggest sum of numbers in a constraint	1129
Number of bits of the biggest sum of numbers	11
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03584
Number of variables	411
Total number of constraints	887
Number of constraints which are clauses	387
Number of constraints which are cardinality constraints (but not clauses)	500
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	16
Trace number 5688

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc21 THE 2005-04-14 01:23:53 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4128 boxname=wulflinc21 idbench=368 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ac510382bae6003fe0373ad32fd0064f  /oldhome/oroussel/tmp/wulflinc21/normalized-10:10:4.5:0.95:98.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc21/normalized-10:10:4.5:0.95:98.opb /oldhome/oroussel/tmp/wulflinc21/normalized-10:10:4.5:0.95:98.opb
IDLAUNCH: 4128
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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.161
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:        880340 kB
Buffers:         27764 kB
Cached:         106672 kB
SwapCached:          0 kB
Active:          34520 kB
Inactive:       102804 kB
HighTotal:      131008 kB
HighFree:        20720 kB
LowTotal:       903652 kB
LowFree:        859620 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11392 kB
Committed_AS:    63796 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 01:44:06 (client local time) WITH STATUS 10 IN 1209.76 SECONDS
stats: 4128 7 1209.76 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 476 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...................................................................................................................................................................................................................................................................................................................................................................................................
c ---[  95]---> BDD-cost:    8
c ---[  94]---> BDD-cost:    8
c ---[  93]---> BDD-cost:   14
c ---[  92]---> BDD-cost:    8
c ---[  91]---> BDD-cost:   11
c ---[  90]---> BDD-cost:   17
c ---[  89]---> BDD-cost:   14
c ---[  88]---> BDD-cost:   11
c ---[  87]---> BDD-cost:   11
c ---[  86]---> BDD-cost:    5
c ---[  85]---> BDD-cost:   11
c ---[  84]---> BDD-cost:   14
c ---[  83]---> BDD-cost:   17
c ---[  82]---> BDD-cost:   17
c ---[  81]---> BDD-cost:   21
c ---[  80]---> BDD-cost:   23
c ---[  79]---> BDD-cost:   17
c ---[  78]---> BDD-cost:   11
c ---[  77]---> BDD-cost:    8
c ---[  76]---> BDD-cost:   14
c ---[  75]---> BDD-cost:   17
c ---[  74]---> BDD-cost:   23
c ---[  73]---> BDD-cost:   26
c ---[  72]---> BDD-cost:   26
c ---[  71]---> BDD-cost:   32
c ---[  70]---> BDD-cost:   23
c ---[  69]---> BDD-cost:   14
c ---[  68]---> BDD-cost:   20
c ---[  67]---> BDD-cost:   11
c ---[  66]---> BDD-cost:   17
c ---[  65]---> BDD-cost:   23
c ---[  64]---> BDD-cost:   26
c ---[  63]---> BDD-cost:   29
c ---[  62]---> BDD-cost:   29
c ---[  61]---> BDD-cost:   32
c ---[  60]---> BDD-cost:   35
c ---[  59]---> BDD-cost:   23
c ---[  58]---> BDD-cost:   23
c ---[  57]---> BDD-cost:   17
c ---[  56]---> BDD-cost:   14
c ---[  55]---> BDD-cost:   26
c ---[  54]---> BDD-cost:   26
c ---[  53]---> BDD-cost:   29
c ---[  52]---> BDD-cost:   32
c ---[  51]---> BDD-cost:   41
c ---[  50]---> BDD-cost:   38
c ---[  49]---> BDD-cost:   26
c ---[  48]---> BDD-cost:   24
c ---[  47]---> BDD-cost:   20
c ---[  46]---> BDD-cost:   14
c ---[  45]---> BDD-cost:   23
c ---[  44]---> BDD-cost:   15
c ---[  43]---> BDD-cost:   29
c ---[  42]---> BDD-cost:   32
c ---[  41]---> BDD-cost:   38
c ---[  40]---> BDD-cost:   32
c ---[  39]---> BDD-cost:   29
c ---[  38]---> BDD-cost:   29
c ---[  37]---> BDD-cost:   23
c ---[  36]---> BDD-cost:    7
c ---[  35]---> BDD-cost:   20
c ---[  34]---> BDD-cost:   15
c ---[  33]---> BDD-cost:   23
c ---[  32]---> BDD-cost:   23
c ---[  31]---> BDD-cost:   32
c ---[  30]---> BDD-cost:   29
c ---[  29]---> BDD-cost:   23
c ---[  28]---> BDD-cost:   23
c ---[  24]---> BDD-cost:   13
c ---[  23]---> BDD-cost:   23
c ---[  22]---> BDD-cost:   29
c ---[  21]---> BDD-cost:   23
c ---[  20]---> BDD-cost:   23
c ---[  19]---> BDD-cost:   17
c ---[  18]---> BDD-cost:   17
c ---[  15]---> BDD-cost:   11
c ---[  14]---> BDD-cost:   20
c ---[  13]---> BDD-cost:   23
c ---[  12]---> BDD-cost:   20
c ---[  11]---> BDD-cost:   20
c ---[  10]---> BDD-cost:   11
c ---[   9]---> BDD-cost:   11
c ---[   6]---> BDD-cost:    7
c ---[   5]---> BDD-cost:   11
c ---[   4]---> BDD-cost:   17
c ---[   3]---> BDD-cost:   11
c ---[   2]---> BDD-cost:   14
c ---[   1]---> BDD-cost:    9
c ---[   0]---> BDD-cost:   11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    4472    12709 |    1341       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2100          
c   -- var.elim.:  2000/2100          
c   -- var.elim.:  2100/2100          
c   -- var.elim.:  1000/1059          
c   -- var.elim.:  1059/1059          
c   -- subsuming                       
c   -- var.elim.:  972/972          
c   -- var.elim.:  566/566          
c   -- subsuming                       
c   -- var.elim.:  4/4          
c   -- var.elim.:  4/4          
c |         0 |    3343    11656 |      --       0       --      -- |     --   | -1129/-786
c |         0 |    3343    11656 |    1337       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.219966 s)
c ==============================================================================
c [1mFound solution: 384[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:23127     Base: 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   31497    77730 |    9449       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/19109          
c   -- var.elim.:  2000/19109          
c   -- var.elim.:  3000/19109          
c   -- var.elim.:  4000/19109          
c   -- var.elim.:  5000/19109          
c   -- var.elim.:  6000/19109          
c   -- var.elim.:  7000/19109          
c   -- var.elim.:  8000/19109          
c   -- var.elim.:  9000/19109          
c   -- var.elim.:  10000/19109          
c   -- var.elim.:  11000/19109          
c   -- var.elim.:  12000/19109          
c   -- var.elim.:  13000/19109          
c   -- var.elim.:  14000/19109          
c   -- var.elim.:  15000/19109          
c   -- var.elim.:  16000/19109          
c   -- var.elim.:  17000/19109          
c   -- var.elim.:  18000/19109          
c   -- var.elim.:  19000/19109          
c   -- var.elim.:  19109/19109          
c   -- var.elim.:  1000/9631          
c   -- var.elim.:  2000/9631          
c   -- var.elim.:  3000/9631          
c   -- var.elim.:  4000/9631          
c   -- var.elim.:  5000/9631          
c   -- var.elim.:  6000/9631          
c   -- var.elim.:  7000/9631          
c   -- var.elim.:  8000/9631          
c   -- var.elim.:  9000/9631          
c   -- var.elim.:  9631/9631          
c   -- subsuming                       
c   -- var.elim.:  1000/9399          
c   -- var.elim.:  2000/9399          
c   -- var.elim.:  3000/9399          
c   -- var.elim.:  4000/9399          
c   -- var.elim.:  5000/9399          
c   -- var.elim.:  6000/9399          
c   -- var.elim.:  7000/9399          
c   -- var.elim.:  8000/9399          
c   -- var.elim.:  9000/9399          
c   -- var.elim.:  9399/9399          
c   -- var.elim.:  1000/3082          
c   -- var.elim.:  2000/3082          
c   -- var.elim.:  3000/3082          
c   -- var.elim.:  3082/3082          
c   -- subsuming                       
c   -- var.elim.:  1000/3026          
c   -- var.elim.:  2000/3026          
c   -- var.elim.:  3000/3026          
c   -- var.elim.:  3026/3026          
c   -- var.elim.:  773/773          
c |         0 |   22062   163809 |      --       0       --      -- |     --   | -9435/86080
c |         0 |   22062   163809 |    8824       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 109.625 s)
c ==============================================================================
c [1mFound solution: 54[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |        52 |   26764   176834 |    8029      51     1808    35.5 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/8904          
c   -- var.elim.:  2000/8904          
c   -- var.elim.:  3000/8904          
c   -- var.elim.:  4000/8904          
c   -- var.elim.:  5000/8904          
c   -- var.elim.:  6000/8904          
c   -- var.elim.:  7000/8904          
c   -- var.elim.:  8000/8904          
c   -- var.elim.:  8904/8904          
c   -- var.elim.:  1000/3813          
c   -- var.elim.:  2000/3813          
c   -- var.elim.:  3000/3813          
c   -- var.elim.:  3813/3813          
c   -- var.elim.:  20/20          
c   -- subsuming                       
c   -- var.elim.:  1000/2894          
c   -- var.elim.:  2000/2894          
c   -- var.elim.:  2894/2894          
c |        52 |   23019   174930 |      --      51       --      -- |     --   | -3745/-1903
c |        52 |   23019   174930 |    9207      51     1808    35.5 |  0.000 % |
c |       154 |   23019   174930 |   10128     153     7336    47.9 |  0.993 % |
c |       304 |   23019   174930 |   11141     303    21524    71.0 |  0.993 % |
c |       531 |   23019   174930 |   12255     530    48674    91.8 |  0.993 % |
c |       868 |   22922   174038 |   13424     864   106292   123.0 |  1.434 % |
c ==============================================================================
c (current CPU-time: 123.97 s)
c ==============================================================================
c [1mFound solution: 31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1009 |   37390   209377 |   11216    1003   126206   125.8 |  1.434 % |
c   -- subsuming                       
c   -- var.elim.:  1000/11255          
c   -- var.elim.:  2000/11255          
c   -- var.elim.:  3000/11255          
c   -- var.elim.:  4000/11255          
c   -- var.elim.:  5000/11255          
c   -- var.elim.:  6000/11255          
c   -- var.elim.:  7000/11255          
c   -- var.elim.:  8000/11255          
c   -- var.elim.:  9000/11255          
c   -- var.elim.:  10000/11255          
c   -- var.elim.:  11000/11255          
c   -- var.elim.:  11255/11255          
c   -- var.elim.:  1000/5227          
c   -- var.elim.:  2000/5227          
c   -- var.elim.:  3000/5227          
c   -- var.elim.:  4000/5227          
c   -- var.elim.:  5000/5227          
c   -- var.elim.:  5227/5227          
c   -- subsuming                       
c   -- var.elim.:  1000/2370          
c   -- var.elim.:  2000/2370          
c   -- var.elim.:  2370/2370          
c |      1009 |   35317   207790 |      --    1003       --      -- |     --   | -2065/-1570
c |      1009 |   35317   207790 |   14126     764    63323    82.9 |  1.434 % |
c |      1109 |   35317   207790 |   15539     864    67392    78.0 |  1.733 % |
c |      1259 |   35221   207200 |   17046    1010    71064    70.4 |  1.928 % |
c |      1485 |   35221   207200 |   18751    1236    88707    71.8 |  1.928 % |
c |      1823 |   35221   207200 |   20626    1574   103240    65.6 |  1.928 % |
c |      2329 |   34951   205582 |   22515    2075   126338    60.9 |  2.513 % |
c |      3088 |   34951   205582 |   24767    2834   199589    70.4 |  2.513 % |
c |      4228 |   34825   204776 |   27145    3963   286280    72.2 |  2.814 % |
c |      5936 |   34825   204776 |   29860    5671   488976    86.2 |  2.814 % |
c |      8500 |   34671   203554 |   32700    8229   830242   100.9 |  3.311 % |
c ==============================================================================
c (current CPU-time: 155.387 s)
c ==============================================================================
c [1mFound solution: 19[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     10607 |   34988   204248 |   10496   10335  1021300    98.8 |  3.311 % |
c   -- subsuming                       
c   -- var.elim.:  1000/7880          
c   -- var.elim.:  2000/7880          
c   -- var.elim.:  3000/7880          
c   -- var.elim.:  4000/7880          
c   -- var.elim.:  5000/7880          
c   -- var.elim.:  6000/7880          
c   -- var.elim.:  7000/7880          
c   -- var.elim.:  7880/7880          
c   -- var.elim.:  626/626          
c   -- subsuming                       
c |     10607 |   34644   204412 |      --   10335       --      -- |     --   | -344/165
c |     10607 |   34644   204412 |   13857   10223   987157    96.6 |  3.311 % |
c |     10707 |   34609   204113 |   15227   10321   993077    96.2 |  3.644 % |
c |     10859 |   34609   204113 |   16750   10473  1006984    96.2 |  3.644 % |
c |     11086 |   34609   204113 |   18425   10700  1028717    96.1 |  3.644 % |
c |     11423 |   34609   204113 |   20268   11037  1053205    95.4 |  3.644 % |
c |     11929 |   34609   204113 |   22295   11543  1085590    94.0 |  3.644 % |
c |     12688 |   34609   204113 |   24524   12302  1156331    94.0 |  3.644 % |
c |     13827 |   34609   204113 |   26977   13441  1243018    92.5 |  3.644 % |
c |     15536 |   34609   204113 |   29674   15150  1383896    91.3 |  3.644 % |
c |     18098 |   34476   203189 |   32517   17704  1764940    99.7 |  4.026 % |
c |     21942 |   34395   202778 |   35684   21542  2371118   110.1 |  4.165 % |
c |     27709 |   34395   202778 |   39253   27309  3381537   123.8 |  4.165 % |
c |     36358 |   34256   201876 |   43004   35952  4647796   129.3 |  4.474 % |
c |     49333 |   34256   201876 |   47304   48927  6807681   139.1 |  4.474 % |
c |     68798 |   34256   201876 |   52034   34733  5533504   159.3 |  4.474 % |
c |     97993 |   34256   201876 |   57238   24382  4089954   167.7 |  4.474 % |
c |    141782 |   34186   201414 |   62833   19173  5544241   289.2 |  4.685 % |
c |    207469 |   34158   201163 |   69060   31489  6472402   205.5 |  4.791 % |
c |    305997 |   34158   201163 |   75966   71351 25839743   362.1 |  4.791 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v v294 v230 -v205 v190 -v138 v293 -v210 v191 -v142 -v358 v301 -v278 v234 -v209 v195 v295 v232 v194 -v357 v296 v212 -v192 -v118 -v361 v297 v233 v213 -v193 -v179 -v82 -v237 -v216 v178 -v163 v117 v81 -v362 -v214 v121 v83 -v215 v180 -v162 v84 v183 -v167 v122 v85 v304 -v274 v229 v189 -v137 v305 -v204 v188 v141 -v384 -v300 -v277 v235 -v206 v199 v211 -v359 v312 -v298 -v238 v208 -v36 -v363 -v316 -v236 v217 -v174 v173 v119 v123 v365 v181 -v164 -v88 v366 v182 -v166 -v89 v380 v302 -v273 v227 -v202 -v139 -v353 v231 -v203 v143 -v383 -v352 -v279 v228 -v198 -v32 v239 -v207 -v113 -v360 v311 -v299 v225 -v196 -v145 -v112 v35 v364 -v315 v221 -v158 -v146 v368 -v282 -v220 -v157 v120 -v87 v367 v175 v124 -v86 -v341 v176 -v165 v125 -v70 v177 -v168 -v126 v74 v379 -v303 v275 -v200 -v140 v226 v144 v396 -v385 -v280 -v247 -v222 -v148 v31 -v400 -v354 v243 -v224 -v147 v355 v313 -v283 -v242 -v197 v37 -v7 v356 -v317 -v281 v114 -v11 -v388 -v372 -v337 -v218 v115 -v100 -v159 v116 v340 v319 -v219 -v186 -v160 v130 -v69 -v40 -v320 v187 -v161 v73 v381 -v271 -v244 -v201 v136 -v27 -v307 v276 -v246 -v223 v135 v395 -v386 -v306 v272 -v152 v33 v399 -v284 -v389 -v375 v314 -v240 -v96 v38 -v6 -v387 v376 -v318 -v10 -v371 -v336 v322 -v241 -v185 -v133 v99 v41 v321 -v184 v134 v39 -v369 v342 -v254 -v171 v129 -v71 -v258 -v172 v75 v378 -v264 -v245 v155 v382 -v270 v156 -v26 v397 -v374 v292 -v151 -v28 v401 -v390 -v373 -v308 v288 v34 -v332 -v309 v287 -v149 -v132 -v95 v30 -v8 v310 -v131 -v65 v42 -v12 v403 -v338 -v326 -v170 v101 -v64 v404 -v169 -v370 v343 -v253 -v127 -v72 -v60 -v#### 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.85 0.97 0.92 2/55 3214
Raw data (stat): 3214 (runsolver) R 3213 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 357868292 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.87 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 3294 0 0 0 896 51 0 0 25 0 1 0 357868292 15691776 3125 4294967295 134512640 134672761 3221224544 3221222992 134643548 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3831 3125 603 41 0 3790 0
vsize: 15324
[startup+20.0011 s]
Raw data (loadavg): 0.89 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 3295 0 0 0 1897 51 0 0 25 0 1 0 357868292 15691776 3126 4294967295 134512640 134672761 3221224544 3221222992 134643468 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3831 3126 603 41 0 3790 0
vsize: 15324
[startup+30.0015 s]
Raw data (loadavg): 0.91 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 3328 0 0 0 2894 54 0 0 25 0 1 0 357868292 15822848 3159 4294967295 134512640 134672761 3221224544 3221222992 134643532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3863 3159 603 41 0 3822 0
vsize: 15452
[startup+40.0013 s]
Raw data (loadavg): 0.92 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 3328 0 0 0 3894 54 0 0 25 0 1 0 357868292 15822848 3159 4294967295 134512640 134672761 3221224544 3221222992 134643516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3863 3159 603 41 0 3822 0
vsize: 15452
[startup+50.0021 s]
Raw data (loadavg): 0.93 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 3411 0 0 0 4894 55 0 0 25 0 1 0 357868292 16306176 3242 4294967295 134512640 134672761 3221224544 3221223036 134642759 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3981 3242 603 41 0 3940 0
vsize: 15924
[startup+60.0018 s]
Raw data (loadavg): 0.94 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 3411 0 0 0 5894 55 0 0 25 0 1 0 357868292 16306176 3242 4294967295 134512640 134672761 3221224544 3221222944 134604052 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3981 3242 603 41 0 3940 0
vsize: 15924
[startup+70.0024 s]
Raw data (loadavg): 0.95 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 3411 0 0 0 6893 55 0 0 25 0 1 0 357868292 16306176 3242 4294967295 134512640 134672761 3221224544 3221223088 134621071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3981 3242 603 41 0 3940 0
vsize: 15924
[startup+80.0025 s]
Raw data (loadavg): 0.96 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 3411 0 0 0 7893 55 0 0 25 0 1 0 357868292 15822848 3180 4294967295 134512640 134672761 3221224544 3221222992 134643987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3863 3180 603 41 0 3822 0
vsize: 15452
[startup+90.0028 s]
Raw data (loadavg): 0.96 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 3411 0 0 0 8893 56 0 0 25 0 1 0 357868292 15822848 3180 4294967295 134512640 134672761 3221224544 3221222992 134643580 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3863 3180 603 41 0 3822 0
vsize: 15452
[startup+100.003 s]
Raw data (loadavg): 0.97 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 3525 0 0 0 9892 56 0 0 25 0 1 0 357868292 16269312 3245 4294967295 134512640 134672761 3221224544 3221223104 134607998 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3972 3245 603 41 0 3931 0
vsize: 15888
[startup+110.002 s]
Raw data (loadavg): 0.97 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 3525 0 0 0 10892 57 0 0 25 0 1 0 357868292 15826944 3183 4294967295 134512640 134672761 3221224544 3221222992 134643548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3864 3183 603 41 0 3823 0
vsize: 15456
[startup+120.002 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 4299 0 0 0 11875 74 0 0 25 0 1 0 357868292 17326080 3608 4294967295 134512640 134672761 3221224544 3221222992 134643483 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4230 3608 603 41 0 4189 0
vsize: 16920
[startup+130.002 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 5300 0 0 0 12860 89 0 0 25 0 1 0 357868292 18956288 4028 4294967295 134512640 134672761 3221224544 3221223088 134621330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4628 4028 603 41 0 4587 0
vsize: 18512
[startup+140.003 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 5395 0 0 0 13859 90 0 0 25 0 1 0 357868292 18784256 4015 4294967295 134512640 134672761 3221224544 3221223088 134621211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4586 4015 603 41 0 4545 0
vsize: 18344
[startup+150.003 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 5718 0 0 0 14858 91 0 0 25 0 1 0 357868292 19664896 4264 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4801 4264 603 41 0 4760 0
vsize: 19204
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 7159 0 0 0 15843 106 0 0 25 0 1 0 357868292 23613440 5220 4294967295 134512640 134672761 3221224544 3221223036 134642890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5765 5220 603 41 0 5724 0
vsize: 23060
[startup+170.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 7161 0 0 0 16843 107 0 0 25 0 1 0 357868292 23613440 5222 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5765 5222 603 41 0 5724 0
vsize: 23060
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 7590 0 0 0 17842 107 0 0 25 0 1 0 357868292 25481216 5651 4294967295 134512640 134672761 3221224544 3221223392 134604146 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6221 5651 603 41 0 6180 0
vsize: 24884
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 8390 0 0 0 18841 109 0 0 25 0 1 0 357868292 28643328 6451 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6993 6451 603 41 0 6952 0
vsize: 27972
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 9300 0 0 0 19839 111 0 0 25 0 1 0 357868292 32456704 7361 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7924 7361 603 41 0 7883 0
vsize: 31696
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 9929 0 0 0 20838 112 0 0 25 0 1 0 357868292 34942976 7990 4294967295 134512640 134672761 3221224544 3221223584 134603506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8531 7990 603 41 0 8490 0
vsize: 34124
[startup+220.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 10670 0 0 0 21836 114 0 0 25 0 1 0 357868292 38092800 8731 4294967295 134512640 134672761 3221224544 3221223728 134615551 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9300 8731 603 41 0 9259 0
vsize: 37200
[startup+230.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 11397 0 0 0 22834 116 0 0 25 0 1 0 357868292 41095168 9458 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10033 9458 603 41 0 9992 0
vsize: 40132
[startup+240.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 12236 0 0 0 23832 119 0 0 25 0 1 0 357868292 44527616 10297 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10871 10297 603 41 0 10830 0
vsize: 43484
[startup+250.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 12892 0 0 0 24830 121 0 0 25 0 1 0 357868292 47022080 10905 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11480 10905 603 41 0 11439 0
vsize: 45920
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 12892 0 0 0 25830 121 0 0 25 0 1 0 357868292 47022080 10905 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11480 10905 603 41 0 11439 0
vsize: 45920
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 12892 0 0 0 26830 121 0 0 25 0 1 0 357868292 47022080 10905 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11480 10905 603 41 0 11439 0
vsize: 45920
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 12892 0 0 0 27830 121 0 0 25 0 1 0 357868292 47022080 10905 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11480 10905 603 41 0 11439 0
vsize: 45920
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 12892 0 0 0 28830 121 0 0 25 0 1 0 357868292 47022080 10905 4294967295 134512640 134672761 3221224544 3221223584 134613748 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11480 10905 603 41 0 11439 0
vsize: 45920
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 12892 0 0 0 29830 121 0 0 25 0 1 0 357868292 47022080 10905 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11480 10905 603 41 0 11439 0
vsize: 45920
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 13097 0 0 0 30829 122 0 0 25 0 1 0 357868292 47943680 11110 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11705 11110 603 41 0 11664 0
vsize: 46820
[startup+320.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 14128 0 0 0 31827 125 0 0 25 0 1 0 357868292 52142080 12141 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12730 12141 603 41 0 12689 0
vsize: 50920
[startup+330.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 15111 0 0 0 32824 128 0 0 25 0 1 0 357868292 56217600 13124 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13725 13124 603 41 0 13684 0
vsize: 54900
[startup+340.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 15876 0 0 0 33822 130 0 0 25 0 1 0 357868292 59232256 13889 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14461 13889 603 41 0 14420 0
vsize: 57844
[startup+350.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 16151 0 0 0 34821 131 0 0 25 0 1 0 357868292 60100608 14110 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14673 14110 603 41 0 14632 0
vsize: 58692
[startup+360.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 16151 0 0 0 35821 131 0 0 25 0 1 0 357868292 60100608 14110 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14673 14110 603 41 0 14632 0
vsize: 58692
[startup+370.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 16151 0 0 0 36822 131 0 0 25 0 1 0 357868292 60100608 14110 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14673 14110 603 41 0 14632 0
vsize: 58692
[startup+380.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 16151 0 0 0 37822 131 0 0 25 0 1 0 357868292 60100608 14110 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14673 14110 603 41 0 14632 0
vsize: 58692
[startup+390.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 16151 0 0 0 38822 131 0 0 25 0 1 0 357868292 60100608 14110 4294967295 134512640 134672761 3221224544 3221223728 134616017 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14673 14110 603 41 0 14632 0
vsize: 58692
[startup+400.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 16151 0 0 0 39822 131 0 0 25 0 1 0 357868292 60100608 14110 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14673 14110 603 41 0 14632 0
vsize: 58692
[startup+410.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 16151 0 0 0 40822 131 0 0 25 0 1 0 357868292 60100608 14110 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14673 14110 603 41 0 14632 0
vsize: 58692
[startup+420.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 16151 0 0 0 41822 131 0 0 25 0 1 0 357868292 60100608 14110 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14673 14110 603 41 0 14632 0
vsize: 58692
[startup+430.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 16151 0 0 0 42822 132 0 0 25 0 1 0 357868292 60100608 14110 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14673 14110 603 41 0 14632 0
vsize: 58692
[startup+440.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 17111 0 0 0 43819 134 0 0 25 0 1 0 357868292 64053248 15070 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15638 15070 603 41 0 15597 0
vsize: 62552
[startup+450.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 18062 0 0 0 44816 137 0 0 25 0 1 0 357868292 67969024 16021 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16594 16021 603 41 0 16553 0
vsize: 66376
[startup+460.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 18904 0 0 0 45814 140 0 0 25 0 1 0 357868292 71380992 16863 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17427 16863 603 41 0 17386 0
vsize: 69708
[startup+470.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 19618 0 0 0 46812 141 0 0 25 0 1 0 357868292 74407936 17577 4294967295 134512640 134672761 3221224544 3221223680 134614756 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18166 17577 603 41 0 18125 0
vsize: 72664
[startup+480.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 20274 0 0 0 47811 143 0 0 25 0 1 0 357868292 77045760 18233 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18810 18233 603 41 0 18769 0
vsize: 75240
[startup+490.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 21106 0 0 0 48809 144 0 0 25 0 1 0 357868292 80330752 19065 4294967295 134512640 134672761 3221224544 3221223640 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19612 19065 603 41 0 19571 0
vsize: 78448
[startup+500.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 21106 0 0 0 49809 144 0 0 25 0 1 0 357868292 80199680 19033 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19580 19033 603 41 0 19539 0
vsize: 78320
[startup+510.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 21106 0 0 0 50809 145 0 0 25 0 1 0 357868292 80199680 19033 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19580 19033 603 41 0 19539 0
vsize: 78320
[startup+520.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 21106 0 0 0 51809 145 0 0 25 0 1 0 357868292 80199680 19033 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19580 19033 603 41 0 19539 0
vsize: 78320
[startup+530.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 21106 0 0 0 52809 145 0 0 25 0 1 0 357868292 80199680 19033 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19580 19033 603 41 0 19539 0
vsize: 78320
[startup+540.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 21106 0 0 0 53810 145 0 0 25 0 1 0 357868292 80199680 19033 4294967295 134512640 134672761 3221224544 3221223680 134614727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19580 19033 603 41 0 19539 0
vsize: 78320
[startup+550.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 21106 0 0 0 54810 145 0 0 25 0 1 0 357868292 80199680 19033 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19580 19033 603 41 0 19539 0
vsize: 78320
[startup+560.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 21106 0 0 0 55810 145 0 0 25 0 1 0 357868292 80199680 19033 4294967295 134512640 134672761 3221224544 3221223800 134618007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19580 19033 603 41 0 19539 0
vsize: 78320
[startup+570.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 21106 0 0 0 56810 145 0 0 25 0 1 0 357868292 80199680 19033 4294967295 134512640 134672761 3221224544 3221223728 134615794 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19580 19033 603 41 0 19539 0
vsize: 78320
[startup+580.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 21106 0 0 0 57809 145 0 0 25 0 1 0 357868292 80199680 19033 4294967295 134512640 134672761 3221224544 3221223728 134615585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19580 19033 603 41 0 19539 0
vsize: 78320
[startup+590.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 21106 0 0 0 58810 145 0 0 25 0 1 0 357868292 80199680 19033 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19580 19033 603 41 0 19539 0
vsize: 78320
[startup+600.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 21106 0 0 0 59810 145 0 0 25 0 1 0 357868292 80199680 19033 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19580 19033 603 41 0 19539 0
vsize: 78320
[startup+610.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 21106 0 0 0 60810 145 0 0 25 0 1 0 357868292 80199680 19033 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19580 19033 603 41 0 19539 0
vsize: 78320
[startup+620.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 21384 0 0 0 61809 146 0 0 25 0 1 0 357868292 81387520 19311 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19870 19311 603 41 0 19829 0
vsize: 79480
[startup+630.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 21956 0 0 0 62808 148 0 0 25 0 1 0 357868292 84029440 19883 4294967295 134512640 134672761 3221224544 3221223584 134612694 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20515 19883 603 41 0 20474 0
vsize: 82060
[startup+640.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 22154 0 0 0 63807 149 0 0 25 0 1 0 357868292 84312064 19982 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20584 19982 603 41 0 20543 0
vsize: 82336
[startup+650.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 22154 0 0 0 64807 149 0 0 25 0 1 0 357868292 84312064 19982 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20584 19982 603 41 0 20543 0
vsize: 82336
[startup+660.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 22154 0 0 0 65808 149 0 0 25 0 1 0 357868292 84312064 19982 4294967295 134512640 134672761 3221224544 3221223536 134565127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20584 19982 603 41 0 20543 0
vsize: 82336
[startup+670.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 22154 0 0 0 66808 149 0 0 25 0 1 0 357868292 84312064 19982 4294967295 134512640 134672761 3221224544 3221223680 134614576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20584 19982 603 41 0 20543 0
vsize: 82336
[startup+680.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 22154 0 0 0 67808 149 0 0 25 0 1 0 357868292 84312064 19982 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20584 19982 603 41 0 20543 0
vsize: 82336
[startup+690.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 22154 0 0 0 68808 149 0 0 25 0 1 0 357868292 84312064 19982 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20584 19982 603 41 0 20543 0
vsize: 82336
[startup+700.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 22154 0 0 0 69808 149 0 0 25 0 1 0 357868292 84312064 19982 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20584 19982 603 41 0 20543 0
vsize: 82336
[startup+710.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 22154 0 0 0 70809 149 0 0 25 0 1 0 357868292 84312064 19982 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20584 19982 603 41 0 20543 0
vsize: 82336
[startup+720.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 22154 0 0 0 71809 149 0 0 25 0 1 0 357868292 84312064 19982 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20584 19982 603 41 0 20543 0
vsize: 82336
[startup+730.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 22154 0 0 0 72809 149 0 0 25 0 1 0 357868292 84312064 19982 4294967295 134512640 134672761 3221224544 3221223576 134603663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20584 19982 603 41 0 20543 0
vsize: 82336
[startup+740.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 22154 0 0 0 73809 149 0 0 25 0 1 0 357868292 84312064 19982 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20584 19982 603 41 0 20543 0
vsize: 82336
[startup+750.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 22154 0 0 0 74809 149 0 0 25 0 1 0 357868292 84312064 19982 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20584 19982 603 41 0 20543 0
vsize: 82336
[startup+760.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 22154 0 0 0 75809 149 0 0 25 0 1 0 357868292 84312064 19982 4294967295 134512640 134672761 3221224544 3221223744 134610528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20584 19982 603 41 0 20543 0
vsize: 82336
[startup+770.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 22154 0 0 0 76810 149 0 0 25 0 1 0 357868292 84312064 19982 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20584 19982 603 41 0 20543 0
vsize: 82336
[startup+780.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 22423 0 0 0 77809 149 0 0 25 0 1 0 357868292 85487616 20251 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20871 20251 603 41 0 20830 0
vsize: 83484
[startup+790.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 23285 0 0 0 78807 151 0 0 25 0 1 0 357868292 89038848 21113 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21738 21113 603 41 0 21697 0
vsize: 86952
[startup+800.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 24094 0 0 0 79806 153 0 0 25 0 1 0 357868292 92327936 21922 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22541 21922 603 41 0 22500 0
vsize: 90164
[startup+810.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 24997 0 0 0 80803 156 0 0 25 0 1 0 357868292 95989760 22825 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23435 22825 603 41 0 23394 0
vsize: 93740
[startup+820.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 25821 0 0 0 81801 158 0 0 25 0 1 0 357868292 99401728 23649 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24268 23649 603 41 0 24227 0
vsize: 97072
[startup+830.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 26518 0 0 0 82799 161 0 0 25 0 1 0 357868292 102289408 24346 4294967295 134512640 134672761 3221224544 3221223728 134615686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24973 24346 603 41 0 24932 0
vsize: 99892
[startup+840.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 27287 0 0 0 83797 162 0 0 25 0 1 0 357868292 105459712 25115 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25747 25115 603 41 0 25706 0
vsize: 102988
[startup+850.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 28024 0 0 0 84796 164 0 0 25 0 1 0 357868292 108462080 25852 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26480 25852 603 41 0 26439 0
vsize: 105920
[startup+860.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 28731 0 0 0 85794 166 0 0 25 0 1 0 357868292 111378432 26559 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27192 26559 603 41 0 27151 0
vsize: 108768
[startup+870.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 29446 0 0 0 86793 167 0 0 25 0 1 0 357868292 114323456 27274 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27911 27274 603 41 0 27870 0
vsize: 111644
[startup+880.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 30169 0 0 0 87791 169 0 0 25 0 1 0 357868292 117317632 27997 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28642 27997 603 41 0 28601 0
vsize: 114568
[startup+890.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 30927 0 0 0 88789 171 0 0 25 0 1 0 357868292 120344576 28755 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29381 28755 603 41 0 29340 0
vsize: 117524
[startup+900.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 31680 0 0 0 89787 173 0 0 25 0 1 0 357868292 123490304 29508 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30149 29508 603 41 0 30108 0
vsize: 120596
[startup+910.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 32455 0 0 0 90785 176 0 0 25 0 1 0 357868292 126660608 30283 4294967295 134512640 134672761 3221224544 3221223728 134615996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30923 30283 603 41 0 30882 0
vsize: 123692
[startup+920.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 33317 0 0 0 91783 178 0 0 25 0 1 0 357868292 130195456 31145 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31786 31145 603 41 0 31745 0
vsize: 127144
[startup+930.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 34022 0 0 0 92781 179 0 0 25 0 1 0 357868292 132526080 31745 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32355 31745 603 41 0 32314 0
vsize: 129420
[startup+940.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 34022 0 0 0 93781 180 0 0 25 0 1 0 357868292 132526080 31745 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32355 31745 603 41 0 32314 0
vsize: 129420
[startup+950.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 34022 0 0 0 94781 180 0 0 25 0 1 0 357868292 132526080 31745 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32355 31745 603 41 0 32314 0
vsize: 129420
[startup+960.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 34022 0 0 0 95781 180 0 0 25 0 1 0 357868292 132526080 31745 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32355 31745 603 41 0 32314 0
vsize: 129420
[startup+970.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 34022 0 0 0 96781 180 0 0 25 0 1 0 357868292 132526080 31745 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32355 31745 603 41 0 32314 0
vsize: 129420
[startup+980.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 34022 0 0 0 97781 180 0 0 25 0 1 0 357868292 132526080 31745 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32355 31745 603 41 0 32314 0
vsize: 129420
[startup+990.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 34022 0 0 0 98781 180 0 0 25 0 1 0 357868292 132526080 31745 4294967295 134512640 134672761 3221224544 3221223584 134614205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32355 31745 603 41 0 32314 0
vsize: 129420
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 34022 0 0 0 99781 180 0 0 25 0 1 0 357868292 132526080 31745 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32355 31745 603 41 0 32314 0
vsize: 129420
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 34022 0 0 0 100781 181 0 0 25 0 1 0 357868292 132526080 31745 4294967295 134512640 134672761 3221224544 3221223680 134614696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32355 31745 603 41 0 32314 0
vsize: 129420
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 34023 0 0 0 101781 181 0 0 25 0 1 0 357868292 132526080 31746 4294967295 134512640 134672761 3221224544 3221223708 134614558 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32355 31746 603 41 0 32314 0
vsize: 129420
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 34023 0 0 0 102781 181 0 0 25 0 1 0 357868292 132526080 31746 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32355 31746 603 41 0 32314 0
vsize: 129420
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 34023 0 0 0 103782 181 0 0 25 0 1 0 357868292 132526080 31746 4294967295 134512640 134672761 3221224544 3221223416 1075352992 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32355 31746 603 41 0 32314 0
vsize: 129420
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 34023 0 0 0 104781 181 0 0 25 0 1 0 357868292 132526080 31746 4294967295 134512640 134672761 3221224544 3221223712 134564689 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32355 31746 603 41 0 32314 0
vsize: 129420
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 34023 0 0 0 105781 181 0 0 25 0 1 0 357868292 132526080 31746 4294967295 134512640 134672761 3221224544 3221223584 134614205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32355 31746 603 41 0 32314 0
vsize: 129420
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 34023 0 0 0 106781 181 0 0 25 0 1 0 357868292 132526080 31746 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32355 31746 603 41 0 32314 0
vsize: 129420
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 34023 0 0 0 107782 181 0 0 25 0 1 0 357868292 132526080 31746 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32355 31746 603 41 0 32314 0
vsize: 129420
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 34023 0 0 0 108782 181 0 0 25 0 1 0 357868292 132526080 31746 4294967295 134512640 134672761 3221224544 3221223584 134612927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32355 31746 603 41 0 32314 0
vsize: 129420
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 34023 0 0 0 109782 181 0 0 25 0 1 0 357868292 132526080 31746 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32355 31746 603 41 0 32314 0
vsize: 129420
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 34023 0 0 0 110782 181 0 0 25 0 1 0 357868292 132526080 31746 4294967295 134512640 134672761 3221224544 3221223584 134613748 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32355 31746 603 41 0 32314 0
vsize: 129420
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 34023 0 0 0 111782 181 0 0 25 0 1 0 357868292 132526080 31746 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32355 31746 603 41 0 32314 0
vsize: 129420
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 34023 0 0 0 112782 181 0 0 25 0 1 0 357868292 132526080 31746 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32355 31746 603 41 0 32314 0
vsize: 129420
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 34023 0 0 0 113783 181 0 0 25 0 1 0 357868292 132526080 31746 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32355 31746 603 41 0 32314 0
vsize: 129420
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 34023 0 0 0 114783 181 0 0 25 0 1 0 357868292 132526080 31746 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32355 31746 603 41 0 32314 0
vsize: 129420
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 34023 0 0 0 115783 181 0 0 25 0 1 0 357868292 132526080 31746 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32355 31746 603 41 0 32314 0
vsize: 129420
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 34441 0 0 0 116782 182 0 0 25 0 1 0 357868292 134234112 32164 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32772 32164 603 41 0 32731 0
vsize: 131088
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 35146 0 0 0 117780 185 0 0 25 0 1 0 357868292 137134080 32869 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33480 32869 603 41 0 33439 0
vsize: 133920
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 35731 0 0 0 118778 187 0 0 25 0 1 0 357868292 139628544 33454 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34089 33454 603 41 0 34048 0
vsize: 136356
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 35952 0 0 0 119778 187 0 0 25 0 1 0 357868292 139956224 33564 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34169 33564 603 41 0 34128 0
vsize: 136676
[startup+1210.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3214
Raw data (stat): 3214 (minisat+) R 3213 30927 30926 0 -1 0 35952 0 0 0 120778 187 0 0 25 0 1 0 357868292 139956224 33564 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34169 33564 603 41 0 34128 0
vsize: 136676
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.92 1/55 3214
Raw data (stat): 3214 (minisat+) Z 3213 30927 30926 0 -1 12 35953 0 0 0 120778 196 0 0 25 0 1 0 357868292 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1210.1
CPU time (s): 1209.76
CPU user time (s): 1207.79
CPU system time (s): 1.9677
CPU usage (%): 99.9713
Max. virtual memory (Kb): 136676
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####