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/submitted/manquinho/routing/normalized-s4-4-3-3pb.opb
MD5SUM	c267b57d74142f6538ad16680277f9bf
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	62
Optimality of the best value was proved	NO
Number of terms in the objective function	648
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	648
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	3
Number of bits of the biggest number in a constraint	2
Biggest sum of numbers in a constraint	648
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02984
Number of variables	648
Total number of constraints	1954
Number of constraints which are clauses	1930
Number of constraints which are cardinality constraints (but not clauses)	24
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	27
Trace number 5915

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc7 THE 2005-04-14 02:27:15 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4375 boxname=wulflinc7 idbench=239 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c267b57d74142f6538ad16680277f9bf  /oldhome/oroussel/tmp/wulflinc7/normalized-s4-4-3-3pb.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc7/normalized-s4-4-3-3pb.opb /oldhome/oroussel/tmp/wulflinc7/normalized-s4-4-3-3pb.opb
IDLAUNCH: 4375
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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		: 451.050
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:        896928 kB
Buffers:         37948 kB
Cached:          80304 kB
SwapCached:          0 kB
Active:          72984 kB
Inactive:        48128 kB
HighTotal:      131008 kB
HighFree:        46900 kB
LowTotal:       903652 kB
LowFree:        850028 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            11028 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 02:38:25 (client local time) WITH STATUS 30 IN 669.265 SECONDS
stats: 4375 0 669.265 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1954 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ############################################################################################################
c   -- Clauses(.)/Splits(s): ..................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[1944]---> BDD-cost:    1
c ---[1934]---> BDD-cost:    1
c ---[1885]---> BDD-cost:    1
c ---[1883]---> BDD-cost:    1
c ---[1869]---> BDD-cost:    1
c ---[1843]---> BDD-cost:    1
c ---[1821]---> BDD-cost:    1
c ---[1811]---> BDD-cost:    1
c ---[1778]---> BDD-cost:    1
c ---[1752]---> BDD-cost:    1
c ---[1750]---> BDD-cost:    1
c ---[1740]---> BDD-cost:    1
c ---[1726]---> BDD-cost:    1
c ---[1700]---> BDD-cost:    1
c ---[1678]---> BDD-cost:    1
c ---[1668]---> BDD-cost:    1
c ---[1654]---> BDD-cost:    1
c ---[1628]---> BDD-cost:    1
c ---[1606]---> BDD-cost:    1
c ---[1596]---> BDD-cost:    1
c ---[1594]---> BDD-cost:    1
c ---[1568]---> BDD-cost:    1
c ---[1550]---> BDD-cost:    1
c ---[1525]---> BDD-cost:    1
c ---[1507]---> BDD-cost:    1
c ---[1485]---> BDD-cost:    1
c ---[1459]---> BDD-cost:    1
c ---[1453]---> BDD-cost:    1
c ---[1435]---> BDD-cost:    1
c ---[1413]---> BDD-cost:    1
c ---[1387]---> BDD-cost:    1
c ---[1381]---> BDD-cost:    1
c ---[1333]---> BDD-cost:    1
c ---[1323]---> BDD-cost:    1
c ---[1313]---> BDD-cost:    1
c ---[1311]---> BDD-cost:    1
c ---[1258]---> BDD-cost:    1
c ---[1248]---> BDD-cost:    1
c ---[1242]---> BDD-cost:    1
c ---[1240]---> BDD-cost:    1
c ---[1203]---> BDD-cost:    1
c ---[1181]---> BDD-cost:    1
c ---[1175]---> BDD-cost:    1
c ---[1169]---> BDD-cost:    1
c ---[1167]---> BDD-cost:    1
c ---[1141]---> BDD-cost:    1
c ---[1123]---> BDD-cost:    1
c ---[1097]---> BDD-cost:    1
c ---[1060]---> BDD-cost:    1
c ---[1038]---> BDD-cost:    1
c ---[1032]---> BDD-cost:    1
c ---[1026]---> BDD-cost:    1
c ---[1024]---> BDD-cost:    1
c ---[ 998]---> BDD-cost:    1
c ---[ 980]---> BDD-cost:    1
c ---[ 954]---> BDD-cost:    1
c ---[ 952]---> BDD-cost:    1
c ---[ 926]---> BDD-cost:    1
c ---[ 908]---> BDD-cost:    1
c ---[ 882]---> BDD-cost:    1
c ---[ 868]---> BDD-cost:    1
c ---[ 842]---> BDD-cost:    1
c ---[ 820]---> BDD-cost:    1
c ---[ 810]---> BDD-cost:    1
c ---[ 792]---> BDD-cost:    1
c ---[ 771]---> BDD-cost:    1
c ---[ 745]---> BDD-cost:    1
c ---[ 739]---> BDD-cost:    1
c ---[ 722]---> BDD-cost:    1
c ---[ 700]---> BDD-cost:    1
c ---[ 674]---> BDD-cost:    1
c ---[ 668]---> BDD-cost:    1
c ---[ 658]---> BDD-cost:    1
c ---[ 648]---> BDD-cost:    1
c ---[ 598]---> BDD-cost:    1
c ---[ 596]---> BDD-cost:    1
c ---[ 586]---> BDD-cost:    1
c ---[ 576]---> BDD-cost:    1
c ---[ 526]---> BDD-cost:    1
c ---[ 524]---> BDD-cost:    1
c ---[ 487]---> BDD-cost:    1
c ---[ 465]---> BDD-cost:    1
c ---[ 459]---> BDD-cost:    1
c ---[ 453]---> BDD-cost:    1
c ---[ 400]---> BDD-cost:    1
c ---[ 390]---> BDD-cost:    1
c ---[ 384]---> BDD-cost:    1
c ---[ 382]---> BDD-cost:    1
c ---[ 372]---> BDD-cost:    1
c ---[ 362]---> BDD-cost:    1
c ---[ 312]---> BDD-cost:    1
c ---[ 310]---> BDD-cost:    1
c ---[ 304]---> BDD-cost:    1
c ---[ 286]---> BDD-cost:    1
c ---[ 248]---> BDD-cost:    1
c ---[ 238]---> BDD-cost:    1
c ---[ 236]---> BDD-cost:    1
c ---[ 210]---> BDD-cost:    1
c ---[ 192]---> BDD-cost:    1
c ---[ 166]---> BDD-cost:    1
c ---[ 129]---> BDD-cost:    1
c ---[ 107]---> BDD-cost:    1
c ---[ 101]---> BDD-cost:    1
c ---[  95]---> BDD-cost:    1
c ---[  62]---> BDD-cost:    1
c ---[  36]---> BDD-cost:    1
c ---[  34]---> BDD-cost:    1
c ---[  24]---> BDD-cost:    1
c ---[  23]---> BDD-cost:   95
c ---[  22]---> BDD-cost:   95
c ---[  21]---> BDD-cost:   95
c ---[  20]---> BDD-cost:   95
c ---[  19]---> BDD-cost:   95
c ---[  18]---> BDD-cost:   95
c ---[  17]---> BDD-cost:   95
c ---[  16]---> BDD-cost:   95
c ---[  15]---> BDD-cost:   95
c ---[  14]---> BDD-cost:   95
c ---[  13]---> BDD-cost:   95
c ---[  12]---> BDD-cost:   95
c ---[  11]---> BDD-cost:   95
c ---[  10]---> BDD-cost:   95
c ---[   9]---> BDD-cost:   95
c ---[   8]---> BDD-cost:   95
c ---[   7]---> BDD-cost:   95
c ---[   6]---> BDD-cost:   95
c ---[   5]---> BDD-cost:   95
c ---[   4]---> BDD-cost:   95
c ---[   3]---> BDD-cost:   95
c ---[   2]---> BDD-cost:   95
c ---[   1]---> BDD-cost:   95
c ---[   0]---> BDD-cost:   95
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    8074    23340 |    2691       0        0     nan |  0.000 % |
c |       102 |    8074    23340 |    2960     102     1442    14.1 |  4.348 % |
c |       252 |    8074    23340 |    3256     252     3799    15.1 |  4.348 % |
c |       480 |    8074    23340 |    3581     480     7765    16.2 |  4.348 % |
c |       817 |    8074    23340 |    3939     817    16005    19.6 |  4.348 % |
c |      1329 |    8074    23340 |    4333    1329    40635    30.6 |  4.348 % |
c |      2090 |    8074    23340 |    4767    2090    66094    31.6 |  4.348 % |
c |      3230 |    8074    23340 |    5243    3230   138206    42.8 |  4.348 % |
c |      4938 |    8074    23340 |    5768    4938   177073    35.9 |  4.348 % |
c |      7502 |    8074    23340 |    6345    4091   151590    37.1 |  4.348 % |
c |     11347 |    8074    23340 |    6979    4497   120713    26.8 |  4.348 % |
c |     17113 |    8074    23340 |    7677    6583   255623    38.8 |  4.348 % |
c |     25763 |    8074    23340 |    8445    6746   282069    41.8 |  4.348 % |
c |     38738 |    8074    23340 |    9290    6392   297596    46.6 |  4.348 % |
c |     58199 |    8074    23340 |   10219    6507   176077    27.1 |  4.348 % |
c |     87395 |    8074    23340 |   11240    9317   321418    34.5 |  4.348 % |
c ==============================================================================
c [1mFound solution: 70[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:29320     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    113284 |   41944   102393 |   13981    6209   195155    31.4 |  4.348 % |
c |    113385 |   41944   102393 |   15379    6310   198132    31.4 |  0.570 % |
c |    113535 |   41944   102393 |   16917    6460   203849    31.6 |  0.570 % |
c |    113760 |   41944   102393 |   18608    6685   211502    31.6 |  0.570 % |
c |    114099 |   41944   102393 |   20469    7024   220570    31.4 |  0.570 % |
c |    114608 |   41944   102393 |   22516    7533   236489    31.4 |  0.570 % |
c |    115367 |   41932   102369 |   24768    8291   259897    31.3 |  0.593 % |
c |    116506 |   41932   102369 |   27245    9430   299512    31.8 |  0.593 % |
c |    118214 |   41932   102369 |   29969   11138   349483    31.4 |  0.593 % |
c |    120778 |   41907   102318 |   32966   13701   452146    33.0 |  0.645 % |
c |    124622 |   41882   102267 |   36263   17544   571773    32.6 |  0.696 % |
c |    130390 |   41882   102267 |   39889   23312   778542    33.4 |  0.696 % |
c ==============================================================================
c [1mFound solution: 68[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    138293 |   41801   102101 |   13933   31214  1065607    34.1 |  0.696 % |
c |    138394 |   41801   102101 |   15326   13484   424371    31.5 |  0.981 % |
c |    138544 |   41801   102101 |   16858   13634   429467    31.5 |  0.981 % |
c |    138769 |   41801   102101 |   18544   13859   433478    31.3 |  0.981 % |
c |    139111 |   41801   102101 |   20399   14201   441685    31.1 |  0.981 % |
c |    139620 |   41801   102101 |   22439   14710   462914    31.5 |  0.981 % |
c |    140381 |   41801   102101 |   24683   15471   490629    31.7 |  0.981 % |
c |    141522 |   41801   102101 |   27151   16612   519133    31.3 |  0.981 % |
c |    143233 |   41801   102101 |   29866   18323   574634    31.4 |  0.981 % |
c |    145801 |   41801   102101 |   32853   20891   660751    31.6 |  0.981 % |
c |    149646 |   41781   102061 |   36138   24735   760512    30.7 |  1.016 % |
c |    155412 |   41781   102061 |   39752   30501   878079    28.8 |  1.016 % |
c |    164061 |   41717   101929 |   43727   39147  1079879    27.6 |  1.143 % |
c |    177036 |   41617   101718 |   48100   22012   483097    21.9 |  1.360 % |
c |    196498 |   41587   101652 |   52910   41473   845150    20.4 |  1.431 % |
c |    225690 |   41542   101559 |   58201   31944   814601    25.5 |  1.518 % |
c |    269481 |   41542   101559 |   64021   32065  1137175    35.5 |  1.518 % |
c |    335165 |   41467   101400 |   70423   49247  1388238    28.2 |  1.684 % |
c |    433692 |   41083   100562 |   77466   38900   776606    20.0 |  2.574 % |
c ==============================================================================
c [1mFound solution: 66[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    525778 |   41062   100523 |   13687   68345  1212971    17.7 |  2.574 % |
c |    525880 |   41062   100523 |   15055    7974   140769    17.7 |  2.691 % |
c |    526032 |   41062   100523 |   16561    8126   143870    17.7 |  2.691 % |
c |    526259 |   41062   100523 |   18217    8353   147844    17.7 |  2.691 % |
c |    526597 |   41062   100523 |   20039    8691   153752    17.7 |  2.691 % |
c |    527103 |   41062   100523 |   22043    9197   162601    17.7 |  2.691 % |
c |    527864 |   41062   100523 |   24247    9958   173677    17.4 |  2.691 % |
c |    529003 |   41062   100523 |   26672   11097   189986    17.1 |  2.691 % |
c |    530712 |   41062   100523 |   29339   12806   217213    17.0 |  2.691 % |
c |    533275 |   41062   100523 |   32273   15369   256491    16.7 |  2.691 % |
c |    537120 |   41062   100523 |   35500   19214   336697    17.5 |  2.691 % |
c |    542888 |   41062   100523 |   39050   24982   429208    17.2 |  2.691 % |
c |    551539 |   41062   100523 |   42955   33633   567257    16.9 |  2.691 % |
c |    564513 |   40100    98410 |   47251   16373   365874    22.3 |  4.936 % |
c ==============================================================================
c [1mFound solution: 64[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    565714 |   37929    93431 |   12643   17486   386189    22.1 |  4.936 % |
c ==============================================================================
c [1mFound solution: 62[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    565806 |   37880    93314 |   12626    8831   186716    21.1 |  4.936 % |
c ==============================================================================
c [1mOptimal solution: 62[0m
s OPTIMUM FOUND
v -v1 -v2 -v3 -v4 -v5 -v6 -v7 -v8 v9 -v10 -v11 -v12 -v13 -v14 -v15 -v16 -v17 -v18 -v19 v20 -v21 -v22 -v23 -v24 -v25 -v26 -v27 -v28 -v29 -v30 -v31 -v32 -v33 v34 v35 -v36 -v37 -v38 v39 -v40 -v41 -v42 v43 -v44 -v45 -v46 v47 -v48 -v49 -v50 -v51 -v52 -v53 -v54 -v55 -v56 -v57 -v58 -v59 -v60 -v61 -v62 v63 -v64 -v65 -v66 v67 -v68 -v69 -v70 -v71 -v72 -v73 -v74 -v75 -v76 -v77 -v78 -v79 -v80 -v81 -v82 -v83 v84 -v85 -v86 -v87 -v88 -v89 -v90 -v91 v92 -v93 -v94 -v95 v96 -v97 -v98 -v99 -v100 v101 -v102 -v103 -v104 -v105 -v106 -v107 -v108 -v109 v110 -v111 -v112 -v113 -v114 v115 -v116 -v117 -v118 v119 -v120 v121 -v122 -v123 -v124 -v125 -v126 -v127 v128 -v129 -v130 -v131 -v132 -v133 v134 -v135 -v136 -v137 v138 -v139 -v140 -v141 -v142 -v143 -v144 -v145 -v146 -v147 -v148 -v149 -v150 -v151 -v152 -v153 v154 -v155 -v156 -v157 -v158 -v159 -v160 -v161 -v162 -v163 -v164 -v165 -v166 -v167 -v168 -v169 -v170 -v171 -v172 -v173 -v174 -v175 -v176 -v177 v178 -v179 -v180 -v181 -v182 -v183 -v184 v185 -v186 -v187 -v188 v189 -v190 -v191 -v192 -v193 -v194 -v195 -v196 v197 -v198 -v199 -v200 -v201 -v202 -v203 -v204 -v205 -v206 -v207 -v208 -v209 v210 -v211 -v212 -v213 -v214 -v215 -v216 -v217 -v218 -v219 -v220 -v221 -v222 -v223 -v224 -v225 -v226 -v227 -v228 -v229 -v230 -v231 -v232 -v233 v234 -v235 -v236 -v237 v238 -v239 -v240 -v241 -v242 -v243 -v244 -v245 -v246 v247 -v248 -v249 -v250 -v251 -v252 -v253 -v254 -v255 -v256 v257 -v258 -v259 -v260 -v261 -v262 -v263 -v264 -v265 -v266 -v267 -v268 -v269 -v270 -v271 -v272 -v273 -v274 -v275 -v276 -v277 -v278 -v279 -v280 -v281 -v282 -v283 -v284 v285 -v286 -v287 -v288 -v289 -v290 -v291 -v292 -v293 -v294 v295 -v296 -v297 -v298 -v299 -v300 -v301 -v302 -v303 -v304 -v305 -v306 -v307 -v308 -v309 -v310 -v311 -v312 -v313 -v314 -v315 -v316 -v317 -v318 -v319 -v320 -v321 -v322 -v323 -v324 -v325 -v326 -v327 v328 -v329 -v330 -v331 v332 -v333 -v334 -v335 v336 -v337 -v338 -v339 -v340 -v341 -v342 v343 v344 v345 -v346 -v347 -v348 v349 -v350 -v351 -v352 v353 -v354 -v355 -v356 -v357 -v358 -v359 v360 v361 v362 -v363 -v364 -v365 -v366 -v367 -v368 -v369 -v370 -v371 -v372 -v373 -v374 -v375 -v376 -v377 -v378 -v379 -v380 -v381 -v382 -v383 -v384 -v385 v386 -v387 -v388 -v389 -v390 -v391 -v392 -v393 -v394 -v395 -v396 -v397 -v398 v399 -v400 -v401 -v402 -v403 -v404 -v405 -v406 -v407 -v408 -v409 -v410 -v411 -v412 -v413 -v414 -v415 -v416 -v417 -v418 -v419 -v420 -v421 -v422 -v423 -v424 -v425 -v426 -v427 -v428 -v429 v430 -v431 -v432 -v433 -v434 -v435 v436 v437 v438 -v439 -v440 -v441 -v442 -v443 -v444 -v445 -v446 -v447 -v448 -v449 -v450 -v451 -v452 -v453 -v454 -v455 -v456 v457 v458 v459 -v460 -v461 -v462 -v463 -v464 -v465 -v466 -v467 -v468 -v469 -v470 -v471 v472 -v473 -v474 -v475 -v476 -v477 -v478 -v479 -v480 -v481 -v482 -v483 -v484 -v485 -v486 -v487 v488 -v489 -v490 -v491 -v492 -v493 -v494 -v495 -v496 -v497 -v498 -v499 -v500 -v501 -v502 v503 -v504 -v505 -v506 -v507 -v508 -v509 -v510 -v511 -v512 -v513 -v514 -v515 -v516 -v517 v518 -v519 -v520 -v521 -v522 -v523 -v524 -v525 -v526 -v527 -v528 -v529 -v530 v531 -v532 -v533 -v534 -v535 -v536 -v537 -v538 -v539 -v540 -v541 -v542 -v543 v544 -v545 -v546 -v547 -v548 -v549 -v550 -v551 -v552 -v553 -v554 -v555 -v556 -v557 -v558 -v559 -v560 -v561 -v562 -v563 -v564 -v565 -v566 -v567 -v568 -v569 -v570 -v571 -v572 v573 -v574 -v575 -v576 -v577 -v578 v579 -v580 -v581 -v582 -v583 -v584 -v585 -v586 -v587 -v588 -v589 -v590 -v591 -v592 -v593 -v594 -v595 -v596 -v597 -v598 -v599 -v600 -v601 -v602 -v603 -v604 -v605 -v606 -v607 -v608 -v609 -v610 -v611 -v612 -v613 -v614 -v615 -v616 -v617 -v618 -v619 -v620 -v621 v622 -v623 -v624 -v625 -v626 -v627 -v628 -v629 -v630 -v631 -v632 v633 -v634 -v635 -v636 -v637 -v638 -v639 -v640 -v641 -v642 -v643 -v644 -v645 -v646 -v647 -v648
c _______________________________________________________________________________
c 
c restarts              : 63
c conflicts             : 565816         (846 /sec)
c decisions             : 846030         (1265 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 669.033 s
c _______________________________________________________________________________
#### 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.81 0.91 0.89 2/54 27957
Raw data (stat): 27957 (runsolver) R 27956 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422768270 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+9.99933 s]
Raw data (loadavg): 0.84 0.92 0.89 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 1130 0 0 0 995 2 0 0 25 0 1 0 422768270 6164480 1108 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1505 1108 603 41 0 1464 0
vsize: 6020
[startup+20.0002 s]
Raw data (loadavg): 0.87 0.92 0.89 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 1278 0 0 0 1994 3 0 0 25 0 1 0 422768270 6856704 1256 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1674 1256 603 41 0 1633 0
vsize: 6696
[startup+30.0004 s]
Raw data (loadavg): 0.89 0.92 0.90 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 1297 0 0 0 2995 3 0 0 25 0 1 0 422768270 6856704 1275 4294967295 134512640 134672761 3221224560 3221223664 134554677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1674 1275 603 41 0 1633 0
vsize: 6696
[startup+40 s]
Raw data (loadavg): 0.90 0.92 0.90 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 1471 0 0 0 3994 4 0 0 25 0 1 0 422768270 7532544 1449 4294967295 134512640 134672761 3221224560 3221223744 134559663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1839 1449 603 41 0 1798 0
vsize: 7356
[startup+50.0003 s]
Raw data (loadavg): 0.92 0.92 0.90 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 2940 0 0 0 4990 8 0 0 25 0 1 0 422768270 13770752 2842 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3362 2842 603 41 0 3321 0
vsize: 13448
[startup+59.9993 s]
Raw data (loadavg): 0.93 0.93 0.90 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 3619 0 0 0 5986 10 0 0 25 0 1 0 422768270 16617472 3521 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4057 3521 603 41 0 4016 0
vsize: 16228
[startup+69.9999 s]
Raw data (loadavg): 0.94 0.93 0.90 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 3980 0 0 0 6985 12 0 0 25 0 1 0 422768270 18030592 3882 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4402 3882 603 41 0 4361 0
vsize: 17608
[startup+79.9999 s]
Raw data (loadavg): 0.95 0.93 0.90 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 4057 0 0 0 7985 12 0 0 25 0 1 0 422768270 18587648 3959 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4538 3959 603 41 0 4497 0
vsize: 18152
[startup+90.0002 s]
Raw data (loadavg): 0.96 0.93 0.90 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 4321 0 0 0 8984 13 0 0 25 0 1 0 422768270 19668992 4223 4294967295 134512640 134672761 3221224560 3221223664 134554677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4802 4223 603 41 0 4761 0
vsize: 19208
[startup+100 s]
Raw data (loadavg): 0.96 0.93 0.90 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 4354 0 0 0 9984 13 0 0 25 0 1 0 422768270 19804160 4256 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4835 4256 603 41 0 4794 0
vsize: 19340
[startup+110 s]
Raw data (loadavg): 0.97 0.94 0.90 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 4384 0 0 0 10984 13 0 0 25 0 1 0 422768270 19968000 4286 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4875 4286 603 41 0 4834 0
vsize: 19500
[startup+120 s]
Raw data (loadavg): 0.97 0.94 0.90 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 4427 0 0 0 11984 13 0 0 25 0 1 0 422768270 20164608 4329 4294967295 134512640 134672761 3221224560 3221223728 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4923 4329 603 41 0 4882 0
vsize: 19692
[startup+130 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 4480 0 0 0 12984 14 0 0 25 0 1 0 422768270 20361216 4382 4294967295 134512640 134672761 3221224560 3221223664 134554677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4971 4382 603 41 0 4930 0
vsize: 19884
[startup+140 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 4491 0 0 0 13984 14 0 0 25 0 1 0 422768270 20361216 4393 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4971 4393 603 41 0 4930 0
vsize: 19884
[startup+150 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 4491 0 0 0 14984 14 0 0 25 0 1 0 422768270 20361216 4393 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4971 4393 603 41 0 4930 0
vsize: 19884
[startup+160 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 4517 0 0 0 15984 14 0 0 25 0 1 0 422768270 20557824 4419 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5019 4419 603 41 0 4978 0
vsize: 20076
[startup+170 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 4836 0 0 0 16983 15 0 0 25 0 1 0 422768270 21913600 4738 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5350 4738 603 41 0 5309 0
vsize: 21400
[startup+179.999 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 5183 0 0 0 17982 16 0 0 25 0 1 0 422768270 23252992 5085 4294967295 134512640 134672761 3221224560 3221223664 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5677 5085 603 41 0 5636 0
vsize: 22708
[startup+190 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 5186 0 0 0 18983 16 0 0 25 0 1 0 422768270 23252992 5088 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5677 5088 603 41 0 5636 0
vsize: 22708
[startup+199.999 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 5207 0 0 0 19983 16 0 0 25 0 1 0 422768270 23400448 5109 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5713 5109 603 41 0 5672 0
vsize: 22852
[startup+209.999 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 5235 0 0 0 20983 16 0 0 25 0 1 0 422768270 23543808 5137 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5748 5137 603 41 0 5707 0
vsize: 22992
[startup+219.999 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 5268 0 0 0 21983 16 0 0 25 0 1 0 422768270 23740416 5170 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5796 5170 603 41 0 5755 0
vsize: 23184
[startup+229.999 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 5270 0 0 0 22983 16 0 0 25 0 1 0 422768270 23740416 5172 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5796 5172 603 41 0 5755 0
vsize: 23184
[startup+240 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 5431 0 0 0 23983 16 0 0 25 0 1 0 422768270 24453120 5333 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5970 5333 603 41 0 5929 0
vsize: 23880
[startup+249.999 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 5550 0 0 0 24983 17 0 0 25 0 1 0 422768270 24858624 5452 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6069 5452 603 41 0 6028 0
vsize: 24276
[startup+259.999 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 5669 0 0 0 25982 17 0 0 25 0 1 0 422768270 25305088 5571 4294967295 134512640 134672761 3221224560 3221223728 134560797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6178 5571 603 41 0 6137 0
vsize: 24712
[startup+269.999 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 5774 0 0 0 26982 17 0 0 25 0 1 0 422768270 25878528 5676 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6318 5676 603 41 0 6277 0
vsize: 25272
[startup+279.998 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 5774 0 0 0 27982 17 0 0 25 0 1 0 422768270 25878528 5676 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6318 5676 603 41 0 6277 0
vsize: 25272
[startup+289.999 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 5775 0 0 0 28983 17 0 0 25 0 1 0 422768270 25878528 5677 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6318 5677 603 41 0 6277 0
vsize: 25272
[startup+299.999 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 5775 0 0 0 29983 17 0 0 25 0 1 0 422768270 25878528 5677 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6318 5677 603 41 0 6277 0
vsize: 25272
[startup+309.998 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 5779 0 0 0 30982 18 0 0 25 0 1 0 422768270 25878528 5681 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6318 5681 603 41 0 6277 0
vsize: 25272
[startup+319.998 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 5793 0 0 0 31981 18 0 0 25 0 1 0 422768270 25878528 5695 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6318 5695 603 41 0 6277 0
vsize: 25272
[startup+329.998 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 5816 0 0 0 32981 18 0 0 25 0 1 0 422768270 26140672 5718 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6382 5718 603 41 0 6341 0
vsize: 25528
[startup+339.998 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 5905 0 0 0 33981 18 0 0 25 0 1 0 422768270 26578944 5807 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6489 5807 603 41 0 6448 0
vsize: 25956
[startup+349.998 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 5924 0 0 0 34981 19 0 0 25 0 1 0 422768270 26726400 5826 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6525 5826 603 41 0 6484 0
vsize: 26100
[startup+359.998 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 5935 0 0 0 35981 19 0 0 25 0 1 0 422768270 26726400 5837 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6525 5837 603 41 0 6484 0
vsize: 26100
[startup+369.998 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 5953 0 0 0 36981 19 0 0 25 0 1 0 422768270 26955776 5855 4294967295 134512640 134672761 3221224560 3221223744 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6581 5855 603 41 0 6540 0
vsize: 26324
[startup+379.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 5954 0 0 0 37981 19 0 0 25 0 1 0 422768270 26955776 5856 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6581 5856 603 41 0 6540 0
vsize: 26324
[startup+389.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 5958 0 0 0 38982 19 0 0 25 0 1 0 422768270 26955776 5860 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6581 5860 603 41 0 6540 0
vsize: 26324
[startup+400.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 5969 0 0 0 39982 19 0 0 25 0 1 0 422768270 26955776 5871 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6581 5871 603 41 0 6540 0
vsize: 26324
[startup+410 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 6031 0 0 0 40982 19 0 0 25 0 1 0 422768270 27348992 5933 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6677 5933 603 41 0 6636 0
vsize: 26708
[startup+420 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 6061 0 0 0 41982 19 0 0 25 0 1 0 422768270 27348992 5963 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6677 5963 603 41 0 6636 0
vsize: 26708
[startup+430.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 6061 0 0 0 42982 19 0 0 25 0 1 0 422768270 27348992 5963 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6677 5963 603 41 0 6636 0
vsize: 26708
[startup+440.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 6061 0 0 0 43982 19 0 0 25 0 1 0 422768270 27348992 5963 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6677 5963 603 41 0 6636 0
vsize: 26708
[startup+450.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 6063 0 0 0 44982 19 0 0 25 0 1 0 422768270 27348992 5965 4294967295 134512640 134672761 3221224560 3221223744 134559599 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6677 5965 603 41 0 6636 0
vsize: 26708
[startup+460.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 6090 0 0 0 45982 19 0 0 25 0 1 0 422768270 27545600 5992 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6725 5992 603 41 0 6684 0
vsize: 26900
[startup+470.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 6140 0 0 0 46982 19 0 0 25 0 1 0 422768270 27742208 6042 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6773 6042 603 41 0 6732 0
vsize: 27092
[startup+480.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 6164 0 0 0 47982 19 0 0 25 0 1 0 422768270 28004352 6066 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6837 6066 603 41 0 6796 0
vsize: 27348
[startup+490.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 6169 0 0 0 48982 19 0 0 25 0 1 0 422768270 28004352 6071 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6837 6071 603 41 0 6796 0
vsize: 27348
[startup+500.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 6172 0 0 0 49982 19 0 0 25 0 1 0 422768270 28004352 6074 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6837 6074 603 41 0 6796 0
vsize: 27348
[startup+510.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 6203 0 0 0 50982 19 0 0 25 0 1 0 422768270 28004352 6105 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6837 6105 603 41 0 6796 0
vsize: 27348
[startup+520.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 6211 0 0 0 51982 19 0 0 25 0 1 0 422768270 28004352 6113 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6837 6113 603 41 0 6796 0
vsize: 27348
[startup+530.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 6211 0 0 0 52983 19 0 0 25 0 1 0 422768270 28004352 6113 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6837 6113 603 41 0 6796 0
vsize: 27348
[startup+540.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 6212 0 0 0 53983 19 0 0 25 0 1 0 422768270 28004352 6114 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6837 6114 603 41 0 6796 0
vsize: 27348
[startup+550.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 6233 0 0 0 54983 19 0 0 25 0 1 0 422768270 28266496 6135 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6901 6135 603 41 0 6860 0
vsize: 27604
[startup+560.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 6255 0 0 0 55983 19 0 0 25 0 1 0 422768270 28266496 6157 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6901 6157 603 41 0 6860 0
vsize: 27604
[startup+570.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 6280 0 0 0 56983 19 0 0 25 0 1 0 422768270 28524544 6182 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6964 6182 603 41 0 6923 0
vsize: 27856
[startup+580.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 6282 0 0 0 57984 19 0 0 25 0 1 0 422768270 28524544 6184 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6964 6184 603 41 0 6923 0
vsize: 27856
[startup+590.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 6284 0 0 0 58984 19 0 0 25 0 1 0 422768270 28524544 6186 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6964 6186 603 41 0 6923 0
vsize: 27856
[startup+600.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 6333 0 0 0 59984 20 0 0 25 0 1 0 422768270 28786688 6235 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7028 6235 603 41 0 6987 0
vsize: 28112
[startup+610.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 6334 0 0 0 60984 20 0 0 25 0 1 0 422768270 28786688 6236 4294967295 134512640 134672761 3221224560 3221223664 134554671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7028 6236 603 41 0 6987 0
vsize: 28112
[startup+620.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 6334 0 0 0 61984 20 0 0 25 0 1 0 422768270 28786688 6236 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7028 6236 603 41 0 6987 0
vsize: 28112
[startup+630.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 6334 0 0 0 62984 20 0 0 25 0 1 0 422768270 28786688 6236 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7028 6236 603 41 0 6987 0
vsize: 28112
[startup+640.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 6334 0 0 0 63984 20 0 0 25 0 1 0 422768270 28786688 6236 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7028 6236 603 41 0 6987 0
vsize: 28112
[startup+650.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 6334 0 0 0 64985 20 0 0 25 0 1 0 422768270 28786688 6236 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7028 6236 603 41 0 6987 0
vsize: 28112
[startup+660.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 6334 0 0 0 65985 20 0 0 25 0 1 0 422768270 28786688 6236 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7028 6236 603 41 0 6987 0
vsize: 28112
[startup+669.215 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 27957
Raw data (stat): 27957 (minisat+) R 27956 22932 22931 0 -1 0 6334 0 0 0 65985 20 0 0 25 0 1 0 422768270 28786688 6236 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7028 6236 603 41 0 6987 0
vsize: 0

Child status: 30
Real time (s): 669.214
CPU time (s): 669.265
CPU user time (s): 669.048
CPU system time (s): 0.216967
CPU usage (%): 100.008
Max. virtual memory (Kb): 28112
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	62
#### END VERIFIER DATA ####