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-7pb.opb
MD5SUM	24909033929a72aa74b2fd8b12f27bce
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	64
Optimality of the best value was proved	NO
Number of terms in the objective function	672
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	672
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	672
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.02884
Number of variables	672
Total number of constraints	2030
Number of constraints which are clauses	2006
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	28
Trace number 4931

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc21 THE 2005-04-13 21:10:35 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2183 boxname=wulflinc21 idbench=243 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  24909033929a72aa74b2fd8b12f27bce  /oldhome/oroussel/tmp/wulflinc21/normalized-s4-4-3-7pb.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc21/normalized-s4-4-3-7pb.opb
IDLAUNCH: 2183
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        910728 kB
Buffers:         26228 kB
Cached:          78016 kB
SwapCached:          0 kB
Active:          33776 kB
Inactive:        73284 kB
HighTotal:      131008 kB
HighFree:        49364 kB
LowTotal:       903652 kB
LowFree:        861364 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11188 kB
Committed_AS:    63792 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 21:13:21 (client local time) WITH STATUS 30 IN 166.061 SECONDS
stats: 2183 0 166.061 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2030 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################################################################################################
c   -- Clauses(.)/Splits(s): ......................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[2016]---> BDD-cost:    1
c ---[1991]---> BDD-cost:    1
c ---[1969]---> BDD-cost:    1
c ---[1959]---> BDD-cost:    1
c ---[1941]---> BDD-cost:    1
c ---[1919]---> BDD-cost:    1
c ---[1893]---> BDD-cost:    1
c ---[1887]---> BDD-cost:    1
c ---[1877]---> BDD-cost:    1
c ---[1867]---> BDD-cost:    1
c ---[1817]---> BDD-cost:    1
c ---[1815]---> BDD-cost:    1
c ---[1813]---> BDD-cost:    1
c ---[1787]---> BDD-cost:    1
c ---[1769]---> BDD-cost:    1
c ---[1743]---> BDD-cost:    1
c ---[1729]---> BDD-cost:    1
c ---[1703]---> BDD-cost:    1
c ---[1681]---> BDD-cost:    1
c ---[1671]---> BDD-cost:    1
c ---[1665]---> BDD-cost:    1
c ---[1647]---> BDD-cost:    1
c ---[1609]---> BDD-cost:    1
c ---[1599]---> BDD-cost:    1
c ---[1582]---> BDD-cost:    1
c ---[1560]---> BDD-cost:    1
c ---[1534]---> BDD-cost:    1
c ---[1528]---> BDD-cost:    1
c ---[1526]---> BDD-cost:    1
c ---[1500]---> BDD-cost:    1
c ---[1482]---> BDD-cost:    1
c ---[1456]---> BDD-cost:    1
c ---[1446]---> BDD-cost:    1
c ---[1436]---> BDD-cost:    1
c ---[1386]---> BDD-cost:    1
c ---[1384]---> BDD-cost:    1
c ---[1366]---> BDD-cost:    1
c ---[1344]---> BDD-cost:    1
c ---[1318]---> BDD-cost:    1
c ---[1312]---> BDD-cost:    1
c ---[1310]---> BDD-cost:    1
c ---[1284]---> BDD-cost:    1
c ---[1266]---> BDD-cost:    1
c ---[1240]---> BDD-cost:    1
c ---[1234]---> BDD-cost:    1
c ---[1216]---> BDD-cost:    1
c ---[1178]---> BDD-cost:    1
c ---[1168]---> BDD-cost:    1
c ---[1166]---> BDD-cost:    1
c ---[1140]---> BDD-cost:    1
c ---[1122]---> BDD-cost:    1
c ---[1096]---> BDD-cost:    1
c ---[1094]---> BDD-cost:    1
c ---[1068]---> BDD-cost:    1
c ---[1050]---> BDD-cost:    1
c ---[1024]---> BDD-cost:    1
c ---[1014]---> BDD-cost:    1
c ---[1004]---> BDD-cost:    1
c ---[ 954]---> BDD-cost:    1
c ---[ 952]---> BDD-cost:    1
c ---[ 934]---> BDD-cost:    1
c ---[ 912]---> BDD-cost:    1
c ---[ 886]---> BDD-cost:    1
c ---[ 880]---> BDD-cost:    1
c ---[ 870]---> BDD-cost:    1
c ---[ 860]---> BDD-cost:    1
c ---[ 811]---> BDD-cost:    1
c ---[ 809]---> BDD-cost:    1
c ---[ 799]---> BDD-cost:    1
c ---[ 789]---> BDD-cost:    1
c ---[ 739]---> BDD-cost:    1
c ---[ 737]---> BDD-cost:    1
c ---[ 684]---> BDD-cost:    1
c ---[ 674]---> BDD-cost:    1
c ---[ 668]---> BDD-cost:    1
c ---[ 666]---> BDD-cost:    1
c ---[ 617]---> BDD-cost:    1
c ---[ 607]---> BDD-cost:    1
c ---[ 597]---> BDD-cost:    1
c ---[ 595]---> BDD-cost:    1
c ---[ 542]---> BDD-cost:    1
c ---[ 532]---> 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 ---[ 435]---> BDD-cost:    1
c ---[ 413]---> BDD-cost:    1
c ---[ 387]---> BDD-cost:    1
c ---[ 381]---> BDD-cost:    1
c ---[ 332]---> BDD-cost:    1
c ---[ 322]---> 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 ---[ 224]---> BDD-cost:    1
c ---[ 198]---> BDD-cost:    1
c ---[ 176]---> BDD-cost:    1
c ---[ 166]---> BDD-cost:    1
c ---[ 114]---> BDD-cost:    1
c ---[ 104]---> BDD-cost:    1
c ---[  98]---> BDD-cost:    1
c ---[  96]---> BDD-cost:    1
c ---[  94]---> BDD-cost:    1
c ---[  68]---> BDD-cost:    1
c ---[  50]---> BDD-cost:    1
c ---[  24]---> BDD-cost:    1
c ---[  23]---> BDD-cost:   99
c ---[  22]---> BDD-cost:   99
c ---[  21]---> BDD-cost:   99
c ---[  20]---> BDD-cost:   99
c ---[  19]---> BDD-cost:   99
c ---[  18]---> BDD-cost:   99
c ---[  17]---> BDD-cost:   99
c ---[  16]---> BDD-cost:   99
c ---[  15]---> BDD-cost:   99
c ---[  14]---> BDD-cost:   99
c ---[  13]---> BDD-cost:   99
c ---[  12]---> BDD-cost:   99
c ---[  11]---> BDD-cost:   99
c ---[  10]---> BDD-cost:   99
c ---[   9]---> BDD-cost:   99
c ---[   8]---> BDD-cost:   99
c ---[   7]---> BDD-cost:   99
c ---[   6]---> BDD-cost:   99
c ---[   5]---> BDD-cost:   99
c ---[   4]---> BDD-cost:   99
c ---[   3]---> BDD-cost:   99
c ---[   2]---> BDD-cost:   99
c ---[   1]---> BDD-cost:   99
c ---[   0]---> BDD-cost:   99
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    8414    24352 |    2804       0        0     nan |  0.000 % |
c |       102 |    8414    24352 |    3084     102     1435    14.1 |  4.304 % |
c |       253 |    8414    24352 |    3392     253     4525    17.9 |  4.304 % |
c |       479 |    8414    24352 |    3732     479    13584    28.4 |  4.304 % |
c |       818 |    8414    24352 |    4105     818    22084    27.0 |  4.304 % |
c |      1324 |    8414    24352 |    4515    1324    35488    26.8 |  4.304 % |
c |      2083 |    8414    24352 |    4967    2083    58571    28.1 |  4.304 % |
c |      3223 |    8414    24352 |    5464    3223    79607    24.7 |  4.304 % |
c |      4931 |    8414    24352 |    6010    4931   111128    22.5 |  4.304 % |
c |      7494 |    8414    24352 |    6611    4402    80202    18.2 |  4.304 % |
c |     11338 |    8414    24352 |    7272    4833    90241    18.7 |  4.304 % |
c |     17104 |    8414    24352 |    8000    6862   116041    16.9 |  4.304 % |
c |     25753 |    8414    24352 |    8800    7295   151785    20.8 |  4.304 % |
c |     38731 |    8414    24352 |    9680    6400   170131    26.6 |  4.304 % |
c |     58195 |    8414    24352 |   10648    5233   120703    23.1 |  4.304 % |
c |     87387 |    8414    24352 |   11713    7222   191228    26.5 |  4.304 % |
c |    131176 |    8414    24352 |   12884    9156   224748    24.5 |  4.304 % |
c ==============================================================================
c [1mFound solution: 72[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:30564     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    157119 |   43669   106611 |   14556    8772   190320    21.7 |  4.304 % |
c |    157219 |   43669   106611 |   16011    8872   192047    21.6 |  0.984 % |
c |    157370 |   43669   106611 |   17612    9023   195263    21.6 |  0.984 % |
c |    157595 |   43669   106611 |   19374    9248   199823    21.6 |  0.984 % |
c |    157932 |   43669   106611 |   21311    9585   206998    21.6 |  0.984 % |
c |    158439 |   43669   106611 |   23442   10092   216440    21.4 |  0.984 % |
c |    159198 |   43669   106611 |   25786   10851   229396    21.1 |  0.984 % |
c |    160338 |   43669   106611 |   28365   11991   247231    20.6 |  0.984 % |
c |    162046 |   43659   106591 |   31202   13698   277550    20.3 |  1.003 % |
c |    164608 |   43659   106591 |   34322   16260   345997    21.3 |  1.003 % |
c |    168452 |   43659   106591 |   37754   20104   425132    21.1 |  1.003 % |
c |    174220 |   43659   106591 |   41529   25872   531470    20.5 |  1.003 % |
c |    182869 |   43659   106591 |   45682   34521   676501    19.6 |  1.003 % |
c |    195844 |   43659   106591 |   50251   15667   266499    17.0 |  1.003 % |
c ==============================================================================
c [1mFound solution: 70[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 |    212129 |   43628   106539 |   14542   31950   561723    17.6 |  1.003 % |
c |    212229 |   43541   106358 |   15996   14112   233643    16.6 |  1.302 % |
c |    212381 |   43541   106358 |   17595   14264   236765    16.6 |  1.302 % |
c |    212607 |   43541   106358 |   19355   14490   240094    16.6 |  1.302 % |
c |    212944 |   43541   106358 |   21290   14827   248435    16.8 |  1.302 % |
c |    213451 |   43541   106358 |   23420   15334   258286    16.8 |  1.302 % |
c |    214211 |   43541   106358 |   25762   16094   270666    16.8 |  1.302 % |
c |    215351 |   43541   106358 |   28338   17234   287319    16.7 |  1.302 % |
c |    217059 |   43512   106299 |   31172   18941   335982    17.7 |  1.351 % |
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 |    217755 |   43431   106122 |   14477   19636   349703    17.8 |  1.351 % |
c |    217856 |   43004   105199 |   15924    9884   186986    18.9 |  2.564 % |
c |    218011 |   43004   105199 |   17517   10039   190518    19.0 |  2.564 % |
c |    218236 |   43004   105199 |   19268   10264   194433    18.9 |  2.564 % |
c |    218574 |   43004   105199 |   21195   10602   201176    19.0 |  2.564 % |
c |    219080 |   42867   104893 |   23315   11106   215752    19.4 |  2.878 % |
c |    219839 |   42867   104893 |   25646   11865   230177    19.4 |  2.878 % |
c |    220982 |   42832   104820 |   28211   13007   257700    19.8 |  2.943 % |
c |    222691 |   42832   104820 |   31032   14716   294522    20.0 |  2.943 % |
c |    225253 |   42775   104697 |   34136   17277   338898    19.6 |  3.071 % |
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 |    225908 |   42616   104333 |   14205   17930   351633    19.6 |  3.071 % |
c |    226009 |   42574   104244 |   15625    9064   162768    18.0 |  3.614 % |
c |    226161 |   42574   104244 |   17188    9216   167726    18.2 |  3.614 % |
c |    226388 |   42574   104244 |   18906    9443   174020    18.4 |  3.614 % |
c |    226725 |   42574   104244 |   20797    9780   183720    18.8 |  3.614 % |
c |    227233 |   42516   104120 |   22877   10282   198976    19.4 |  3.735 % |
c |    227992 |   42516   104120 |   25165   11041   220335    20.0 |  3.735 % |
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 |    228164 |   42190   103359 |   14063   11212   225803    20.1 |  3.735 % |
c |    228264 |   42190   103359 |   15469   11312   228312    20.2 |  4.636 % |
c |    228414 |   42134   103241 |   17016   11460   230725    20.1 |  4.742 % |
c |    228639 |   42134   103241 |   18717   11685   233381    20.0 |  4.742 % |
c |    228978 |   41897   102702 |   20589   12021   242649    20.2 |  5.305 % |
c |    229484 |   41897   102702 |   22648   12527   250195    20.0 |  5.305 % |
c |    230243 |   41897   102702 |   24913   13286   259796    19.6 |  5.305 % |
c ==============================================================================
c [1mOptimal solution: 64[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 -v649 -v650 -v651 -v652 -v653 -v654 -v655 -v656 -v657 -v658 -v659 v660 -v661 -v662 -v663 -v664 -v665 -v666 -v667 -v668 -v669 -v670 -v671 -v672
c _______________________________________________________________________________
c 
c restarts              : 64
c conflicts             : 231342         (1394 /sec)
c decisions             : 334898         (2019 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 165.902 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.91 0.95 0.90 2/55 1615
Raw data (stat): 1615 (runsolver) R 1614 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 356348271 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.93 0.95 0.90 2/55 1615
Raw data (stat): 1615 (minisat+) R 1614 30927 30926 0 -1 0 1013 0 0 0 997 2 0 0 25 0 1 0 356348271 5730304 991 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1399 991 603 41 0 1358 0
vsize: 5596
[startup+20.0015 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 1615
Raw data (stat): 1615 (minisat+) R 1614 30927 30926 0 -1 0 1113 0 0 0 1996 3 0 0 25 0 1 0 356348271 6279168 1091 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1533 1091 603 41 0 1492 0
vsize: 6132
[startup+30.0015 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 1615
Raw data (stat): 1615 (minisat+) R 1614 30927 30926 0 -1 0 1306 0 0 0 2995 3 0 0 25 0 1 0 356348271 7086080 1284 4294967295 134512640 134672761 3221224624 3221223728 134554671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1730 1284 603 41 0 1689 0
vsize: 6920
[startup+40.0018 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 1615
Raw data (stat): 1615 (minisat+) R 1614 30927 30926 0 -1 0 1356 0 0 0 3995 4 0 0 25 0 1 0 356348271 7221248 1334 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1763 1334 603 41 0 1722 0
vsize: 7052
[startup+50.0029 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 1615
Raw data (stat): 1615 (minisat+) R 1614 30927 30926 0 -1 0 1391 0 0 0 4995 4 0 0 25 0 1 0 356348271 7360512 1369 4294967295 134512640 134672761 3221224624 3221223728 134554677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1797 1369 603 41 0 1756 0
vsize: 7188
[startup+60.0032 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 1615
Raw data (stat): 1615 (minisat+) R 1614 30927 30926 0 -1 0 1409 0 0 0 5995 4 0 0 25 0 1 0 356348271 7524352 1387 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1837 1387 603 41 0 1796 0
vsize: 7348
[startup+70.0039 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 1615
Raw data (stat): 1615 (minisat+) R 1614 30927 30926 0 -1 0 3109 0 0 0 6991 8 0 0 25 0 1 0 356348271 15298560 3016 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3735 3016 603 41 0 3694 0
vsize: 14940
[startup+80.0035 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 1615
Raw data (stat): 1615 (minisat+) R 1614 30927 30926 0 -1 0 3439 0 0 0 7990 10 0 0 25 0 1 0 356348271 16793600 3346 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4100 3346 603 41 0 4059 0
vsize: 16400
[startup+90.0046 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 1615
Raw data (stat): 1615 (minisat+) R 1614 30927 30926 0 -1 0 3630 0 0 0 8989 10 0 0 25 0 1 0 356348271 17637376 3537 4294967295 134512640 134672761 3221224624 3221223792 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4306 3537 603 41 0 4265 0
vsize: 17224
[startup+100.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 1615
Raw data (stat): 1615 (minisat+) R 1614 30927 30926 0 -1 0 3755 0 0 0 9989 11 0 0 25 0 1 0 356348271 18202624 3662 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4444 3662 603 41 0 4403 0
vsize: 17776
[startup+110.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 1615
Raw data (stat): 1615 (minisat+) R 1614 30927 30926 0 -1 0 3936 0 0 0 10988 11 0 0 25 0 1 0 356348271 18890752 3843 4294967295 134512640 134672761 3221224624 3221222976 134565852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4612 3843 603 41 0 4571 0
vsize: 18448
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1615
Raw data (stat): 1615 (minisat+) R 1614 30927 30926 0 -1 0 3944 0 0 0 11988 12 0 0 25 0 1 0 356348271 18890752 3851 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4612 3851 603 41 0 4571 0
vsize: 18448
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1615
Raw data (stat): 1615 (minisat+) R 1614 30927 30926 0 -1 0 3959 0 0 0 12988 12 0 0 25 0 1 0 356348271 19038208 3866 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4648 3866 603 41 0 4607 0
vsize: 18592
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1615
Raw data (stat): 1615 (minisat+) R 1614 30927 30926 0 -1 0 3988 0 0 0 13988 12 0 0 25 0 1 0 356348271 19185664 3895 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4684 3895 603 41 0 4643 0
vsize: 18736
[startup+150.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1615
Raw data (stat): 1615 (minisat+) R 1614 30927 30926 0 -1 0 4030 0 0 0 14988 13 0 0 25 0 1 0 356348271 19390464 3937 4294967295 134512640 134672761 3221224624 3221223792 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4734 3937 603 41 0 4693 0
vsize: 18936
[startup+160.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1615
Raw data (stat): 1615 (minisat+) R 1614 30927 30926 0 -1 0 4032 0 0 0 15988 13 0 0 25 0 1 0 356348271 19390464 3939 4294967295 134512640 134672761 3221224624 3221223728 134554665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4734 3939 603 41 0 4693 0
vsize: 18936
[startup+166.055 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 1615
Raw data (stat): 1615 (minisat+) R 1614 30927 30926 0 -1 0 4032 0 0 0 15988 13 0 0 25 0 1 0 356348271 19390464 3939 4294967295 134512640 134672761 3221224624 3221223728 134554665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4734 3939 603 41 0 4693 0
vsize: 0

Child status: 30
Real time (s): 166.054
CPU time (s): 166.061
CPU user time (s): 165.918
CPU system time (s): 0.142978
CPU usage (%): 100.004
Max. virtual memory (Kb): 18936
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	64
#### END VERIFIER DATA ####