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 6275

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc30 THE 2005-04-14 04:21:37 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4755 boxname=wulflinc30 idbench=243 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  24909033929a72aa74b2fd8b12f27bce  /oldhome/oroussel/tmp/wulflinc30/normalized-s4-4-3-7pb.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc30/normalized-s4-4-3-7pb.opb /oldhome/oroussel/tmp/wulflinc30/normalized-s4-4-3-7pb.opb
IDLAUNCH: 4755
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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.072
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        720176 kB
Buffers:         38292 kB
Cached:         235544 kB
SwapCached:          0 kB
Active:          83420 kB
Inactive:       193316 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        719924 kB
SwapTotal:     2097892 kB
SwapFree:      2097892 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            32060 kB
Committed_AS:    63492 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 04:27:12 (client local time) WITH STATUS 30 IN 334.688 SECONDS
stats: 4755 0 334.688 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 |   14246    41704 |    4748       0        0     nan |  0.000 % |
c |       105 |   14246    41704 |    5222     105     1542    14.7 |  4.304 % |
c |       255 |   14246    41704 |    5745     255     5802    22.8 |  4.304 % |
c |       482 |   14246    41704 |    6319     482    12530    26.0 |  4.304 % |
c |       819 |   14246    41704 |    6951     819    19918    24.3 |  4.304 % |
c |      1325 |   14246    41704 |    7646    1325    30440    23.0 |  4.304 % |
c |      2086 |   14246    41704 |    8411    2086    58599    28.1 |  4.304 % |
c |      3229 |   14246    41704 |    9252    3229   113622    35.2 |  4.304 % |
c |      4937 |   14246    41704 |   10177    4937   168927    34.2 |  4.304 % |
c |      7499 |   14246    41704 |   11195    7499   212380    28.3 |  4.304 % |
c |     11343 |   14246    41704 |   12315   11343   350319    30.9 |  4.304 % |
c |     17110 |   14246    41704 |   13546   10836   319366    29.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 |     24560 |   83377   203568 |   27792   11418   365002    32.0 |  4.304 % |
c |     24660 |   83377   203568 |   30571   11518   367565    31.9 |  1.973 % |
c |     24818 |   83377   203568 |   33628   11676   369297    31.6 |  1.973 % |
c |     25043 |   83358   203526 |   36991   11900   377877    31.8 |  1.992 % |
c |     25382 |   83358   203526 |   40690   12239   389057    31.8 |  1.992 % |
c |     25889 |   83358   203526 |   44759   12746   402876    31.6 |  1.992 % |
c |     26649 |   83358   203526 |   49235   13506   421530    31.2 |  1.992 % |
c |     27790 |   83358   203526 |   54158   14647   446826    30.5 |  1.992 % |
c |     29499 |   83358   203526 |   59574   16356   488619    29.9 |  1.992 % |
c |     32061 |   83358   203526 |   65532   18918   595270    31.5 |  1.992 % |
c |     35908 |   83353   203511 |   72085   22737   800359    35.2 |  1.995 % |
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 |     38514 |   83360   203534 |   27786   25343   921763    36.4 |  1.995 % |
c |     38615 |   83360   203534 |   30564   25444   923468    36.3 |  2.036 % |
c |     38765 |   83360   203534 |   33621   25594   926713    36.2 |  2.036 % |
c |     38990 |   83360   203534 |   36983   25819   931249    36.1 |  2.036 % |
c |     39328 |   83360   203534 |   40681   26157   942973    36.1 |  2.036 % |
c |     39834 |   83360   203534 |   44749   26663   960420    36.0 |  2.036 % |
c |     40598 |   83360   203534 |   49224   27427   977026    35.6 |  2.036 % |
c |     41739 |   83331   203469 |   54147   28567  1003295    35.1 |  2.066 % |
c |     43447 |   83331   203469 |   59561   30275  1047206    34.6 |  2.066 % |
c |     46010 |   83282   203359 |   65517   32837  1112051    33.9 |  2.116 % |
c |     49855 |   83191   203153 |   72069   36680  1212935    33.1 |  2.206 % |
c |     55621 |   83176   203120 |   79276   42445  1349925    31.8 |  2.221 % |
c |     64270 |   82440   201451 |   87204   51074  1545426    30.3 |  2.997 % |
c |     77246 |   80987   198137 |   95924   63972  1836750    28.7 |  4.564 % |
c |     96707 |   80723   197536 |  105517   83427  2231182    26.7 |  4.848 % |
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 |    122894 |   73388   180698 |   24462  109324  2832745    25.9 |  4.848 % |
c |    122995 |   73388   180698 |   26908   18669   363984    19.5 | 13.140 % |
c |    123145 |   73191   180239 |   29599   18814   365529    19.4 | 13.382 % |
c |    123372 |   72931   179628 |   32558   18880   366636    19.4 | 13.666 % |
c |    123709 |   72931   179628 |   35814   19217   379591    19.8 | 13.666 % |
c |    124215 |   72931   179628 |   39396   19723   397067    20.1 | 13.666 % |
c |    124974 |   72931   179628 |   43335   20482   413325    20.2 | 13.666 % |
c |    126113 |   72892   179537 |   47669   21620   435174    20.1 | 13.719 % |
c |    127821 |   72892   179537 |   52436   23328   463282    19.9 | 13.719 % |
c ==============================================================================
c [1mFound solution: 66[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:18226     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    128577 |  101943   247380 |   33981   24082   487360    20.2 | 13.719 % |
c |    128677 |   97439   236999 |   37379   24028   486397    20.2 | 16.580 % |
c |    128827 |   97330   236740 |   41117   24173   489409    20.2 | 16.660 % |
c |    129052 |   96729   235354 |   45228   24328   490617    20.2 | 17.159 % |
c |    129389 |   96518   234865 |   49751   24455   499170    20.4 | 17.320 % |
c |    129897 |   96518   234865 |   54726   24963   516654    20.7 | 17.320 % |
c |    130656 |   96467   234745 |   60199   25721   539578    21.0 | 17.357 % |
c |    131795 |   96467   234745 |   66219   26860   575394    21.4 | 17.357 % |
c |    133503 |   96403   234592 |   72841   28567   630299    22.1 | 17.400 % |
c ==============================================================================
c [1mFound solution: 64[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:18778     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    133632 |  126048   303758 |   42016   28695   633889    22.1 | 17.400 % |
c |    133732 |  126048   303758 |   46217   28795   637026    22.1 | 16.318 % |
c |    133883 |  125977   303599 |   50839   28942   640727    22.1 | 16.359 % |
c |    134109 |  125977   303599 |   55923   29168   649450    22.3 | 16.359 % |
c |    134446 |  125638   302824 |   61515   29501   659925    22.4 | 16.563 % |
c |    134952 |  125638   302824 |   67667   30007   673672    22.5 | 16.563 % |
c |    135715 |  125638   302824 |   74433   30770   698392    22.7 | 16.563 % |
c |    136855 |  125638   302824 |   81877   31910   726607    22.8 | 16.563 % |
c |    138563 |  125331   302114 |   90065   33598   776836    23.1 | 16.747 % |
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              : 65
c conflicts             : 139079         (416 /sec)
c decisions             : 204650         (612 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 334.421 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.95 0.99 0.92 2/54 19085
Raw data (stat): 19085 (runsolver) D 19084 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481668941 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 3225161850 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.95 0.99 0.92 2/54 19085
Raw data (stat): 19085 (minisat+) R 19084 11931 11930 0 -1 0 1223 0 0 0 995 3 0 0 25 0 1 0 481668941 6594560 1201 4294967295 134512640 134672761 3221224560 3221223664 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1610 1201 603 41 0 1569 0
vsize: 6440
[startup+20.0003 s]
Raw data (loadavg): 0.96 0.99 0.92 2/54 19085
Raw data (stat): 19085 (minisat+) R 19084 11931 11930 0 -1 0 3410 0 0 0 1988 9 0 0 25 0 1 0 481668941 16453632 3321 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4017 3321 603 41 0 3976 0
vsize: 16068
[startup+30.0013 s]
Raw data (loadavg): 0.97 0.99 0.92 2/54 19085
Raw data (stat): 19085 (minisat+) R 19084 11931 11930 0 -1 0 3795 0 0 0 2987 10 0 0 25 0 1 0 481668941 17915904 3706 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4374 3706 603 41 0 4333 0
vsize: 17496
[startup+40.0006 s]
Raw data (loadavg): 0.97 0.99 0.92 2/54 19085
Raw data (stat): 19085 (minisat+) R 19084 11931 11930 0 -1 0 4076 0 0 0 3986 11 0 0 25 0 1 0 481668941 19197952 3987 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4687 3987 603 41 0 4646 0
vsize: 18748
[startup+50.0016 s]
Raw data (loadavg): 0.97 0.99 0.92 2/54 19085
Raw data (stat): 19085 (minisat+) R 19084 11931 11930 0 -1 0 4293 0 0 0 4986 12 0 0 25 0 1 0 481668941 20127744 4204 4294967295 134512640 134672761 3221224560 3221223696 134560683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4914 4204 603 41 0 4873 0
vsize: 19656
[startup+60.0018 s]
Raw data (loadavg): 0.98 0.99 0.92 2/54 19085
Raw data (stat): 19085 (minisat+) R 19084 11931 11930 0 -1 0 4504 0 0 0 5985 12 0 0 25 0 1 0 481668941 20951040 4415 4294967295 134512640 134672761 3221224560 3221223744 134559512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5115 4415 603 41 0 5074 0
vsize: 20460
[startup+70.002 s]
Raw data (loadavg): 0.98 0.99 0.92 2/54 19085
Raw data (stat): 19085 (minisat+) R 19084 11931 11930 0 -1 0 4695 0 0 0 6984 13 0 0 25 0 1 0 481668941 21778432 4606 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5317 4606 603 41 0 5276 0
vsize: 21268
[startup+80.0031 s]
Raw data (loadavg): 0.98 0.99 0.92 2/54 19085
Raw data (stat): 19085 (minisat+) R 19084 11931 11930 0 -1 0 4807 0 0 0 7984 13 0 0 25 0 1 0 481668941 22192128 4718 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5418 4718 603 41 0 5377 0
vsize: 21672
[startup+90.0029 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19085
Raw data (stat): 19085 (minisat+) R 19084 11931 11930 0 -1 0 4974 0 0 0 8984 14 0 0 25 0 1 0 481668941 22900736 4885 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5591 4885 603 41 0 5550 0
vsize: 22364
[startup+100.003 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19085
Raw data (stat): 19085 (minisat+) R 19084 11931 11930 0 -1 0 5103 0 0 0 9983 15 0 0 25 0 1 0 481668941 23441408 5014 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5723 5014 603 41 0 5682 0
vsize: 22892
[startup+110.004 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19085
Raw data (stat): 19085 (minisat+) R 19084 11931 11930 0 -1 0 5288 0 0 0 10983 16 0 0 25 0 1 0 481668941 24526848 5199 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5988 5199 603 41 0 5947 0
vsize: 23952
[startup+120.004 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19085
Raw data (stat): 19085 (minisat+) R 19084 11931 11930 0 -1 0 5405 0 0 0 11983 16 0 0 25 0 1 0 481668941 24993792 5316 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6102 5316 603 41 0 6061 0
vsize: 24408
[startup+130.005 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19085
Raw data (stat): 19085 (minisat+) R 19084 11931 11930 0 -1 0 5504 0 0 0 12983 16 0 0 25 0 1 0 481668941 25403392 5415 4294967295 134512640 134672761 3221224560 3221223560 1075350219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6202 5415 603 41 0 6161 0
vsize: 24808
[startup+140.005 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19085
Raw data (stat): 19085 (minisat+) R 19084 11931 11930 0 -1 0 5629 0 0 0 13982 16 0 0 25 0 1 0 481668941 25989120 5540 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6345 5540 603 41 0 6304 0
vsize: 25380
[startup+150.006 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19085
Raw data (stat): 19085 (minisat+) R 19084 11931 11930 0 -1 0 5711 0 0 0 14982 17 0 0 25 0 1 0 481668941 26292224 5622 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6419 5622 603 41 0 6378 0
vsize: 25676
[startup+160.005 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19085
Raw data (stat): 19085 (minisat+) R 19084 11931 11930 0 -1 0 5813 0 0 0 15982 17 0 0 25 0 1 0 481668941 26877952 5724 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6562 5724 603 41 0 6521 0
vsize: 26248
[startup+170.005 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19085
Raw data (stat): 19085 (minisat+) R 19084 11931 11930 0 -1 0 5883 0 0 0 16982 17 0 0 25 0 1 0 481668941 27156480 5794 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6630 5794 603 41 0 6589 0
vsize: 26520
[startup+180.006 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19085
Raw data (stat): 19085 (minisat+) R 19084 11931 11930 0 -1 0 5951 0 0 0 17982 17 0 0 25 0 1 0 481668941 27459584 5862 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6704 5862 603 41 0 6663 0
vsize: 26816
[startup+190.006 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19085
Raw data (stat): 19085 (minisat+) R 19084 11931 11930 0 -1 0 6054 0 0 0 18982 18 0 0 25 0 1 0 481668941 28020736 5965 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6841 5965 603 41 0 6800 0
vsize: 27364
[startup+200.006 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19085
Raw data (stat): 19085 (minisat+) R 19084 11931 11930 0 -1 0 6115 0 0 0 19982 18 0 0 25 0 1 0 481668941 28225536 6026 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6891 6026 603 41 0 6850 0
vsize: 27564
[startup+210.006 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19085
Raw data (stat): 19085 (minisat+) R 19084 11931 11930 0 -1 0 6181 0 0 0 20982 18 0 0 25 0 1 0 481668941 28438528 6092 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6943 6092 603 41 0 6902 0
vsize: 27772
[startup+220.006 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19085
Raw data (stat): 19085 (minisat+) R 19084 11931 11930 0 -1 0 6273 0 0 0 21982 18 0 0 25 0 1 0 481668941 28921856 6184 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7061 6184 603 41 0 7020 0
vsize: 28244
[startup+230.006 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19085
Raw data (stat): 19085 (minisat+) R 19084 11931 11930 0 -1 0 6353 0 0 0 22982 19 0 0 25 0 1 0 481668941 29192192 6264 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7127 6264 603 41 0 7086 0
vsize: 28508
[startup+240.007 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19085
Raw data (stat): 19085 (minisat+) R 19084 11931 11930 0 -1 0 6443 0 0 0 23982 19 0 0 25 0 1 0 481668941 29593600 6354 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7225 6354 603 41 0 7184 0
vsize: 28900
[startup+250.007 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19085
Raw data (stat): 19085 (minisat+) R 19084 11931 11930 0 -1 0 6545 0 0 0 24982 19 0 0 25 0 1 0 481668941 30060544 6456 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7339 6456 603 41 0 7298 0
vsize: 29356
[startup+260.007 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19085
Raw data (stat): 19085 (minisat+) R 19084 11931 11930 0 -1 0 6613 0 0 0 25982 19 0 0 25 0 1 0 481668941 30195712 6524 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7372 6524 603 41 0 7331 0
vsize: 29488
[startup+270.007 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19085
Raw data (stat): 19085 (minisat+) R 19084 11931 11930 0 -1 0 6670 0 0 0 26981 20 0 0 25 0 1 0 481668941 30466048 6581 4294967295 134512640 134672761 3221224560 3221223728 134561018 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7438 6581 603 41 0 7397 0
vsize: 29752
[startup+280.008 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19085
Raw data (stat): 19085 (minisat+) R 19084 11931 11930 0 -1 0 6785 0 0 0 27981 20 0 0 25 0 1 0 481668941 30937088 6696 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7553 6696 603 41 0 7512 0
vsize: 30212
[startup+290.008 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19085
Raw data (stat): 19085 (minisat+) R 19084 11931 11930 0 -1 0 6825 0 0 0 28981 20 0 0 25 0 1 0 481668941 31145984 6736 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7604 6736 603 41 0 7563 0
vsize: 30416
[startup+300.009 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19085
Raw data (stat): 19085 (minisat+) R 19084 11931 11930 0 -1 0 7376 0 0 0 29979 22 0 0 25 0 1 0 481668941 33841152 7199 4294967295 134512640 134672761 3221224560 3221223732 134556664 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8262 7199 603 41 0 8221 0
vsize: 33048
[startup+310.009 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19085
Raw data (stat): 19085 (minisat+) R 19084 11931 11930 0 -1 0 7380 0 0 0 30980 22 0 0 25 0 1 0 481668941 33841152 7203 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8262 7203 603 41 0 8221 0
vsize: 33048
[startup+320.009 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19085
Raw data (stat): 19085 (minisat+) R 19084 11931 11930 0 -1 0 7652 0 0 0 31980 22 0 0 25 0 1 0 481668941 35151872 7475 4294967295 134512640 134672761 3221224560 3221223696 134560606 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8582 7475 603 41 0 8541 0
vsize: 34328
[startup+330.01 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19085
Raw data (stat): 19085 (minisat+) R 19084 11931 11930 0 -1 0 7655 0 0 0 32980 22 0 0 25 0 1 0 481668941 35151872 7478 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8582 7478 603 41 0 8541 0
vsize: 34328
[startup+334.671 s]
Raw data (loadavg): 0.99 0.99 0.92 1/53 19085
Raw data (stat): 19085 (minisat+) R 19084 11931 11930 0 -1 0 7655 0 0 0 32980 22 0 0 25 0 1 0 481668941 35151872 7478 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8582 7478 603 41 0 8541 0
vsize: 0

Child status: 30
Real time (s): 334.671
CPU time (s): 334.688
CPU user time (s): 334.448
CPU system time (s): 0.239963
CPU usage (%): 100.005
Max. virtual memory (Kb): 34328
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	64
#### END VERIFIER DATA ####