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 4969

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc18 THE 2005-04-13 21:09:04 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2147 boxname=wulflinc18 idbench=239 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  c267b57d74142f6538ad16680277f9bf  /oldhome/oroussel/tmp/wulflinc18/normalized-s4-4-3-3pb.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc18/normalized-s4-4-3-3pb.opb
IDLAUNCH: 2147
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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	: 3
cpu MHz		: 451.177
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:        907248 kB
Buffers:         34080 kB
Cached:          57400 kB
SwapCached:        320 kB
Active:          49756 kB
Inactive:        44932 kB
HighTotal:      131008 kB
HighFree:        69552 kB
LowTotal:       903652 kB
LowFree:        837696 kB
SwapTotal:     2097892 kB
SwapFree:      2097572 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6936 kB
Slab:            27052 kB
Committed_AS:    63700 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 21:20:24 (client local time) WITH STATUS 30 IN 679.55 SECONDS
stats: 2147 0 679.55 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         (833 /sec)
c decisions             : 846030         (1246 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 679.263 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): 1.00 0.99 0.91 2/55 23344
Raw data (stat): 23344 (runsolver) R 23343 20024 20023 0 -1 64 0 0 0 0 0 0 0 0 19 0 1 0 479068324 1052672 97 4294967295 134512640 135381576 3221224528 3221219968 134514522 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 97 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 1.07 1.00 0.92 2/55 23344
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 1129 0 0 0 995 3 0 0 25 0 1 0 479068324 6152192 1107 4294967295 134512640 134672761 3221224624 3221223728 134559805 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1502 1107 603 41 0 1461 0
vsize: 6008
[startup+20.0019 s]
Raw data (loadavg): 1.06 1.00 0.92 2/55 23344
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 1276 0 0 0 1995 3 0 0 25 0 1 0 479068324 6832128 1254 4294967295 134512640 134672761 3221224624 3221223792 134564451 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1668 1254 603 41 0 1627 0
vsize: 6672
[startup+30.0025 s]
Raw data (loadavg): 1.05 1.00 0.92 2/55 23344
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 1294 0 0 0 2995 4 0 0 25 0 1 0 479068324 6832128 1272 4294967295 134512640 134672761 3221224624 3221223792 134560845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1668 1272 603 41 0 1627 0
vsize: 6672
[startup+40.0027 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 23344
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 1449 0 0 0 3994 4 0 0 25 0 1 0 479068324 7507968 1427 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1833 1427 603 41 0 1792 0
vsize: 7332
[startup+50.0029 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 23344
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 2924 0 0 0 4991 8 0 0 25 0 1 0 479068324 13688832 2826 4294967295 134512640 134672761 3221224624 3221223792 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3342 2826 603 41 0 3301 0
vsize: 13368
[startup+60.0033 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 23344
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 3613 0 0 0 5988 11 0 0 25 0 1 0 479068324 16531456 3515 4294967295 134512640 134672761 3221224624 3221223580 1075349908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4036 3515 603 41 0 3995 0
vsize: 16144
[startup+70.0034 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 23344
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 4015 0 0 0 6987 12 0 0 25 0 1 0 479068324 18550784 3917 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4529 3917 603 41 0 4488 0
vsize: 18116
[startup+80.0043 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 23344
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 4097 0 0 0 7987 12 0 0 25 0 1 0 479068324 19107840 3999 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4665 3999 603 41 0 4624 0
vsize: 18660
[startup+90.004 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 23344
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 4339 0 0 0 8986 13 0 0 25 0 1 0 479068324 20058112 4241 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4897 4241 603 41 0 4856 0
vsize: 19588
[startup+100.004 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 23344
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 4387 0 0 0 9986 13 0 0 25 0 1 0 479068324 20205568 4289 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4933 4289 603 41 0 4892 0
vsize: 19732
[startup+110.005 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 23344
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 4417 0 0 0 10985 14 0 0 25 0 1 0 479068324 20353024 4319 4294967295 134512640 134672761 3221224624 3221223792 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4969 4319 603 41 0 4928 0
vsize: 19876
[startup+120.006 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 23344
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 4460 0 0 0 11983 14 0 0 25 0 1 0 479068324 20516864 4362 4294967295 134512640 134672761 3221224624 3221223792 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5009 4362 603 41 0 4968 0
vsize: 20036
[startup+130.007 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 23344
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 4515 0 0 0 12983 15 0 0 25 0 1 0 479068324 20844544 4417 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5089 4417 603 41 0 5048 0
vsize: 20356
[startup+140.008 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 23344
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 4515 0 0 0 13982 15 0 0 25 0 1 0 479068324 20844544 4417 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5089 4417 603 41 0 5048 0
vsize: 20356
[startup+150.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23344
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 4528 0 0 0 14982 16 0 0 25 0 1 0 479068324 20844544 4430 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5089 4430 603 41 0 5048 0
vsize: 20356
[startup+160.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23344
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 4549 0 0 0 15982 16 0 0 25 0 1 0 479068324 21041152 4451 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5137 4451 603 41 0 5096 0
vsize: 20548
[startup+170.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23346
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 4789 0 0 0 16982 16 0 0 25 0 1 0 479068324 21999616 4691 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5371 4691 603 41 0 5330 0
vsize: 21484
[startup+180.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23346
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 5189 0 0 0 17980 19 0 0 25 0 1 0 479068324 23609344 5091 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5764 5091 603 41 0 5723 0
vsize: 23056
[startup+190.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23346
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 5225 0 0 0 18980 19 0 0 25 0 1 0 479068324 23740416 5127 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5796 5127 603 41 0 5755 0
vsize: 23184
[startup+200.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23346
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 5243 0 0 0 19980 19 0 0 25 0 1 0 479068324 23883776 5145 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5831 5145 603 41 0 5790 0
vsize: 23324
[startup+210.011 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23346
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 5267 0 0 0 20980 19 0 0 25 0 1 0 479068324 24031232 5169 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5867 5169 603 41 0 5826 0
vsize: 23468
[startup+220.011 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23346
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 5300 0 0 0 21980 19 0 0 25 0 1 0 479068324 24211456 5202 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5911 5202 603 41 0 5870 0
vsize: 23644
[startup+230.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23346
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 5303 0 0 0 22980 19 0 0 25 0 1 0 479068324 24211456 5205 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5911 5205 603 41 0 5870 0
vsize: 23644
[startup+240.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23346
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 5406 0 0 0 23980 20 0 0 25 0 1 0 479068324 24481792 5308 4294967295 134512640 134672761 3221224624 3221223792 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5977 5308 603 41 0 5936 0
vsize: 23908
[startup+250.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23346
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 5549 0 0 0 24979 21 0 0 25 0 1 0 479068324 25206784 5451 4294967295 134512640 134672761 3221224624 3221223760 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6154 5451 603 41 0 6113 0
vsize: 24616
[startup+260.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23346
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 5671 0 0 0 25979 21 0 0 25 0 1 0 479068324 25788416 5573 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6296 5573 603 41 0 6255 0
vsize: 25184
[startup+270.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23346
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 5784 0 0 0 26979 21 0 0 25 0 1 0 479068324 26218496 5686 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6401 5686 603 41 0 6360 0
vsize: 25604
[startup+280.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23346
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 5809 0 0 0 27979 21 0 0 25 0 1 0 479068324 26361856 5711 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6436 5711 603 41 0 6395 0
vsize: 25744
[startup+290.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23346
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 5815 0 0 0 28979 21 0 0 25 0 1 0 479068324 26361856 5717 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6436 5717 603 41 0 6395 0
vsize: 25744
[startup+300.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23346
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 5815 0 0 0 29979 21 0 0 25 0 1 0 479068324 26361856 5717 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6436 5717 603 41 0 6395 0
vsize: 25744
[startup+310.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23346
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 5816 0 0 0 30979 21 0 0 25 0 1 0 479068324 26361856 5718 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6436 5718 603 41 0 6395 0
vsize: 25744
[startup+320.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23346
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 5830 0 0 0 31979 22 0 0 25 0 1 0 479068324 26361856 5732 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6436 5732 603 41 0 6395 0
vsize: 25744
[startup+330.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23346
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 5853 0 0 0 32979 22 0 0 25 0 1 0 479068324 26558464 5755 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6484 5755 603 41 0 6443 0
vsize: 25936
[startup+340.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23346
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 5899 0 0 0 33979 22 0 0 25 0 1 0 479068324 26968064 5801 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6584 5801 603 41 0 6543 0
vsize: 26336
[startup+350.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23346
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 5943 0 0 0 34979 22 0 0 25 0 1 0 479068324 27144192 5845 4294967295 134512640 134672761 3221224624 3221223824 134557919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6627 5845 603 41 0 6586 0
vsize: 26508
[startup+360.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23346
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 5967 0 0 0 35979 22 0 0 25 0 1 0 479068324 27308032 5869 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6667 5869 603 41 0 6626 0
vsize: 26668
[startup+370.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23346
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 5967 0 0 0 36979 22 0 0 25 0 1 0 479068324 27308032 5869 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6667 5869 603 41 0 6626 0
vsize: 26668
[startup+380.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23346
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 5986 0 0 0 37979 22 0 0 25 0 1 0 479068324 27308032 5888 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6667 5888 603 41 0 6626 0
vsize: 26668
[startup+390.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23346
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 5988 0 0 0 38979 22 0 0 25 0 1 0 479068324 27308032 5890 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6667 5890 603 41 0 6626 0
vsize: 26668
[startup+400.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23346
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 5994 0 0 0 39979 22 0 0 25 0 1 0 479068324 27308032 5896 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6667 5896 603 41 0 6626 0
vsize: 26668
[startup+410.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23346
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 6016 0 0 0 40980 23 0 0 25 0 1 0 479068324 27504640 5918 4294967295 134512640 134672761 3221224624 3221223792 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6715 5918 603 41 0 6674 0
vsize: 26860
[startup+420.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23346
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 6071 0 0 0 41979 23 0 0 25 0 1 0 479068324 27701248 5973 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6763 5973 603 41 0 6722 0
vsize: 27052
[startup+430.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23346
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 6098 0 0 0 42980 23 0 0 25 0 1 0 479068324 27963392 6000 4294967295 134512640 134672761 3221224624 3221223728 134554677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6827 6000 603 41 0 6786 0
vsize: 27308
[startup+440.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23346
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 6098 0 0 0 43980 23 0 0 25 0 1 0 479068324 27963392 6000 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6827 6000 603 41 0 6786 0
vsize: 27308
[startup+450.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23346
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 6098 0 0 0 44980 23 0 0 25 0 1 0 479068324 27963392 6000 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6827 6000 603 41 0 6786 0
vsize: 27308
[startup+460.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23346
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 6113 0 0 0 45979 23 0 0 25 0 1 0 479068324 27963392 6015 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6827 6015 603 41 0 6786 0
vsize: 27308
[startup+470.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23348
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 6133 0 0 0 46979 23 0 0 25 0 1 0 479068324 27963392 6035 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6827 6035 603 41 0 6786 0
vsize: 27308
[startup+480.023 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23348
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 6178 0 0 0 47979 24 0 0 25 0 1 0 479068324 28225536 6080 4294967295 134512640 134672761 3221224624 3221223792 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6891 6080 603 41 0 6850 0
vsize: 27564
[startup+490.024 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23348
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 6205 0 0 0 48979 24 0 0 25 0 1 0 479068324 28487680 6107 4294967295 134512640 134672761 3221224624 3221223792 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6955 6107 603 41 0 6914 0
vsize: 27820
[startup+500.024 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23348
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 6208 0 0 0 49980 24 0 0 25 0 1 0 479068324 28487680 6110 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6955 6110 603 41 0 6914 0
vsize: 27820
[startup+510.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23348
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 6213 0 0 0 50980 24 0 0 25 0 1 0 479068324 28487680 6115 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6955 6115 603 41 0 6914 0
vsize: 27820
[startup+520.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23348
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 6249 0 0 0 51980 24 0 0 25 0 1 0 479068324 28487680 6151 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6955 6151 603 41 0 6914 0
vsize: 27820
[startup+530.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23348
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 6249 0 0 0 52980 24 0 0 25 0 1 0 479068324 28487680 6151 4294967295 134512640 134672761 3221224624 3221223748 134566115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6955 6151 603 41 0 6914 0
vsize: 27820
[startup+540.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23348
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 6249 0 0 0 53980 24 0 0 25 0 1 0 479068324 28487680 6151 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6955 6151 603 41 0 6914 0
vsize: 27820
[startup+550.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23348
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 6269 0 0 0 54980 24 0 0 25 0 1 0 479068324 28749824 6171 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7019 6171 603 41 0 6978 0
vsize: 28076
[startup+560.032 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23348
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 6271 0 0 0 55981 24 0 0 25 0 1 0 479068324 28749824 6173 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7019 6173 603 41 0 6978 0
vsize: 28076
[startup+570.032 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23348
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 6296 0 0 0 56981 25 0 0 25 0 1 0 479068324 28749824 6198 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7019 6198 603 41 0 6978 0
vsize: 28076
[startup+580.033 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23348
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 6321 0 0 0 57981 25 0 0 25 0 1 0 479068324 29011968 6223 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7083 6223 603 41 0 7042 0
vsize: 28332
[startup+590.035 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23348
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 6323 0 0 0 58981 25 0 0 25 0 1 0 479068324 29011968 6225 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7083 6225 603 41 0 7042 0
vsize: 28332
[startup+600.035 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23348
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 6325 0 0 0 59981 25 0 0 25 0 1 0 479068324 29011968 6227 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7083 6227 603 41 0 7042 0
vsize: 28332
[startup+610.035 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23348
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 6374 0 0 0 60981 25 0 0 25 0 1 0 479068324 29274112 6276 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7147 6276 603 41 0 7106 0
vsize: 28588
[startup+620.035 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23348
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 6375 0 0 0 61980 25 0 0 25 0 1 0 479068324 29274112 6277 4294967295 134512640 134672761 3221224624 3221223728 134554665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7147 6277 603 41 0 7106 0
vsize: 28588
[startup+630.036 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23348
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 6375 0 0 0 62980 26 0 0 25 0 1 0 479068324 29274112 6277 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7147 6277 603 41 0 7106 0
vsize: 28588
[startup+640.036 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23348
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 6375 0 0 0 63980 26 0 0 25 0 1 0 479068324 29274112 6277 4294967295 134512640 134672761 3221224624 3221223792 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7147 6277 603 41 0 7106 0
vsize: 28588
[startup+650.036 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23348
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 6375 0 0 0 64980 26 0 0 25 0 1 0 479068324 29274112 6277 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7147 6277 603 41 0 7106 0
vsize: 28588
[startup+660.036 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23348
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 6376 0 0 0 65980 26 0 0 25 0 1 0 479068324 29274112 6278 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7147 6278 603 41 0 7106 0
vsize: 28588
[startup+670.036 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 23348
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 6376 0 0 0 66980 26 0 0 25 0 1 0 479068324 29274112 6278 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7147 6278 603 41 0 7106 0
vsize: 28588
[startup+679.519 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 23348
Raw data (stat): 23344 (minisat+) R 23343 20024 20023 0 -1 0 6376 0 0 0 66980 26 0 0 25 0 1 0 479068324 29274112 6278 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7147 6278 603 41 0 7106 0
vsize: 0

Child status: 30
Real time (s): 679.519
CPU time (s): 679.55
CPU user time (s): 679.274
CPU system time (s): 0.275958
CPU usage (%): 100.005
Max. virtual memory (Kb): 28588
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	62
#### END VERIFIER DATA ####