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 30449

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc6 THE 2005-05-25 16:51:17 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=21821 boxname=wulflinc6 idbench=239 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  c267b57d74142f6538ad16680277f9bf  /oldhome/oroussel/tmp/wulflinc6/normalized-s4-4-3-3pb.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc6/normalized-s4-4-3-3pb.opb
IDLAUNCH: 21821
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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:        688892 kB
Buffers:         34516 kB
Cached:         286508 kB
SwapCached:        412 kB
Active:          91208 kB
Inactive:       232188 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        688640 kB
SwapTotal:     2097136 kB
SwapFree:      2096036 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           5696 kB
Slab:            16692 kB
Committed_AS:    63724 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 17:02:18 (client local time) WITH STATUS 30 IN 661.56 SECONDS
stats: 21821 0 661.56 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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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         (856 /sec)
c decisions             : 846030         (1280 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 661.089 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.92 0.95 0.95 2/54 9499
Raw data (stat): 9499 (runsolver) R 9498 25568 25567 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 782235607 1052672 99 4294967295 134512640 135381576 3221224496 3221219704 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.93 0.96 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0011 s]
Raw data (loadavg): 0.94 0.96 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0017 s]
Raw data (loadavg): 0.95 0.96 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0019 s]
Raw data (loadavg): 0.96 0.96 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0024 s]
Raw data (loadavg): 0.96 0.96 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0022 s]
Raw data (loadavg): 0.97 0.96 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0023 s]
Raw data (loadavg): 0.97 0.96 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0029 s]
Raw data (loadavg): 0.98 0.96 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0026 s]
Raw data (loadavg): 0.98 0.96 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.003 s]
Raw data (loadavg): 0.98 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.016 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.016 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.016 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.016 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.016 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 9503
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.016 s]
Raw data (loadavg): 1.07 0.99 0.96 3/59 9550
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.018 s]
Raw data (loadavg): 1.06 0.99 0.96 2/55 9556
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.017 s]
Raw data (loadavg): 1.05 0.99 0.96 2/55 9556
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.018 s]
Raw data (loadavg): 1.04 0.99 0.96 2/55 9556
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.019 s]
Raw data (loadavg): 1.04 0.99 0.96 2/55 9556
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.019 s]
Raw data (loadavg): 1.03 0.99 0.96 2/55 9556
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.019 s]
Raw data (loadavg): 1.03 0.99 0.96 2/55 9556
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.019 s]
Raw data (loadavg): 1.02 0.99 0.96 2/55 9558
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.02 s]
Raw data (loadavg): 1.02 0.99 0.96 2/55 9558
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.021 s]
Raw data (loadavg): 1.01 0.99 0.96 2/55 9558
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.02 s]
Raw data (loadavg): 1.01 0.99 0.96 2/55 9558
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.02 s]
Raw data (loadavg): 1.01 0.99 0.96 2/55 9558
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.021 s]
Raw data (loadavg): 1.01 0.99 0.96 2/55 9558
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.021 s]
Raw data (loadavg): 1.01 0.99 0.96 2/55 9558
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+661.408 s]
Raw data (loadavg): 1.01 0.99 0.96 1/53 9558
Raw data (stat): 9499 (minisat+_script) S 9498 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782235607 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 30
Real time (s): 661.407
CPU time (s): 661.56
CPU user time (s): 661.117
CPU system time (s): 0.442932
CPU usage (%): 100.023
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	62
#### END VERIFIER DATA ####