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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. 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.
  4. 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

Namesubmitted/manquinho/routing/normalized-s4-4-3-5pb.opb
MD5SUM4ca29b1bc7e76812f7871e2b937d8a23
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 60
Optimality of the best value was proved YES
Number of terms in the objective function 720
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 720
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 720
Number of bits of the biggest sum of numbers10
Best result obtained on this benchmarkOPTIMUM FOUND
Best CPU time to get the best result obtained on this benchmark112.282
Number of variables720
Total number of constraints2168
Number of constraints which are clauses2144
Number of constraints which are cardinality constraints (but not clauses)24
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint2
Maximum length of a constraint30

Trace number 2164

Launcher Data

LAUNCH ON wulflinc13 THE 2005-09-18 18:08:32 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2584 boxname=wulflinc13 idbench=240 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4ca29b1bc7e76812f7871e2b937d8a23  /oldhome/oroussel/tmp/wulflinc13/normalized-s4-4-3-5pb.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc13/normalized-s4-4-3-5pb.opb
IDLAUNCH: 2584
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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:        882860 kB
Buffers:         34080 kB
Cached:          91488 kB
SwapCached:        708 kB
Active:          65296 kB
Inactive:        62876 kB
HighTotal:      131008 kB
HighFree:        66472 kB
LowTotal:       903652 kB
LowFree:        816388 kB
SwapTotal:     2097136 kB
SwapFree:      2095936 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5740 kB
Slab:            18012 kB
Committed_AS:    64148 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 18:10:52 (client local time) WITH STATUS 30 IN 139.629 SECONDS
stats: 2584 0 139.629 30

Solver Data

c Parsing PB file...
c Converting 2168 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################################################################################################################
c   -- Clauses(.)/Splits(s): ................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[2119]---> BDD-cost:    1
c ---[2109]---> BDD-cost:    1
c ---[2099]---> BDD-cost:    1
c ---[2097]---> BDD-cost:    1
c ---[2083]---> BDD-cost:    1
c ---[2057]---> BDD-cost:    1
c ---[2035]---> BDD-cost:    1
c ---[2025]---> BDD-cost:    1
c ---[1976]---> BDD-cost:    1
c ---[1966]---> BDD-cost:    1
c ---[1956]---> BDD-cost:    1
c ---[1954]---> BDD-cost:    1
c ---[1940]---> BDD-cost:    1
c ---[1914]---> BDD-cost:    1
c ---[1892]---> BDD-cost:    1
c ---[1882]---> BDD-cost:    1
c ---[1864]---> BDD-cost:    1
c ---[1842]---> BDD-cost:    1
c ---[1816]---> BDD-cost:    1
c ---[1810]---> BDD-cost:    1
c ---[1808]---> BDD-cost:    1
c ---[1782]---> BDD-cost:    1
c ---[1765]---> BDD-cost:    1
c ---[1739]---> BDD-cost:    1
c ---[1733]---> BDD-cost:    1
c ---[1715]---> BDD-cost:    1
c ---[1677]---> BDD-cost:    1
c ---[1667]---> BDD-cost:    1
c ---[1630]---> BDD-cost:    1
c ---[1608]---> BDD-cost:    1
c ---[1602]---> BDD-cost:    1
c ---[1596]---> BDD-cost:    1
c ---[1563]---> BDD-cost:    1
c ---[1537]---> BDD-cost:    1
c ---[1535]---> BDD-cost:    1
c ---[1525]---> BDD-cost:    1
c ---[1488]---> BDD-cost:    1
c ---[1466]---> BDD-cost:    1
c ---[1460]---> BDD-cost:    1
c ---[1454]---> BDD-cost:    1
c ---[1452]---> BDD-cost:    1
c ---[1426]---> BDD-cost:    1
c ---[1409]---> BDD-cost:    1
c ---[1383]---> BDD-cost:    1
c ---[1377]---> BDD-cost:    1
c ---[1359]---> BDD-cost:    1
c ---[1322]---> BDD-cost:    1
c ---[1312]---> BDD-cost:    1
c ---[1298]---> BDD-cost:    1
c ---[1272]---> BDD-cost:    1
c ---[1250]---> BDD-cost:    1
c ---[1240]---> BDD-cost:    1
c ---[1222]---> BDD-cost:    1
c ---[1200]---> BDD-cost:    1
c ---[1174]---> BDD-cost:    1
c ---[1168]---> BDD-cost:    1
c ---[1158]---> BDD-cost:    1
c ---[1148]---> BDD-cost:    1
c ---[1098]---> BDD-cost:    1
c ---[1096]---> BDD-cost:    1
c ---[1047]---> BDD-cost:    1
c ---[1037]---> BDD-cost:    1
c ---[1027]---> BDD-cost:    1
c ---[1025]---> BDD-cost:    1
c ---[1023]---> BDD-cost:    1
c ---[ 997]---> BDD-cost:    1
c ---[ 979]---> BDD-cost:    1
c ---[ 953]---> BDD-cost:    1
c ---[ 935]---> BDD-cost:    1
c ---[ 914]---> BDD-cost:    1
c ---[ 888]---> BDD-cost:    1
c ---[ 882]---> BDD-cost:    1
c ---[ 864]---> BDD-cost:    1
c ---[ 842]---> BDD-cost:    1
c ---[ 816]---> BDD-cost:    1
c ---[ 810]---> BDD-cost:    1
c ---[ 804]---> BDD-cost:    1
c ---[ 786]---> BDD-cost:    1
c ---[ 749]---> BDD-cost:    1
c ---[ 739]---> BDD-cost:    1
c ---[ 721]---> BDD-cost:    1
c ---[ 700]---> BDD-cost:    1
c ---[ 674]---> BDD-cost:    1
c ---[ 668]---> BDD-cost:    1
c ---[ 654]---> BDD-cost:    1
c ---[ 629]---> BDD-cost:    1
c ---[ 607]---> BDD-cost:    1
c ---[ 597]---> BDD-cost:    1
c ---[ 564]---> BDD-cost:    1
c ---[ 538]---> BDD-cost:    1
c ---[ 536]---> BDD-cost:    1
c ---[ 526]---> BDD-cost:    1
c ---[ 477]---> BDD-cost:    1
c ---[ 467]---> BDD-cost:    1
c ---[ 457]---> BDD-cost:    1
c ---[ 455]---> BDD-cost:    1
c ---[ 437]---> BDD-cost:    1
c ---[ 415]---> BDD-cost:    1
c ---[ 389]---> BDD-cost:    1
c ---[ 383]---> BDD-cost:    1
c ---[ 381]---> BDD-cost:    1
c ---[ 355]---> BDD-cost:    1
c ---[ 337]---> BDD-cost:    1
c ---[ 311]---> BDD-cost:    1
c ---[ 305]---> BDD-cost:    1
c ---[ 287]---> BDD-cost:    1
c ---[ 249]---> BDD-cost:    1
c ---[ 239]---> BDD-cost:    1
c ---[ 186]---> BDD-cost:    1
c ---[ 176]---> BDD-cost:    1
c ---[ 170]---> BDD-cost:    1
c ---[ 168]---> BDD-cost:    1
c ---[ 154]---> BDD-cost:    1
c ---[ 128]---> BDD-cost:    1
c ---[ 106]---> BDD-cost:    1
c ---[  96]---> BDD-cost:    1
c ---[  78]---> BDD-cost:    1
c ---[  56]---> BDD-cost:    1
c ---[  30]---> BDD-cost:    1
c ---[  24]---> BDD-cost:    1
c ---[  23]---> BDD-cost:  107
c ---[  22]---> BDD-cost:  107
c ---[  21]---> BDD-cost:  107
c ---[  20]---> BDD-cost:  107
c ---[  19]---> BDD-cost:  107
c ---[  18]---> BDD-cost:  107
c ---[  17]---> BDD-cost:  107
c ---[  16]---> BDD-cost:  107
c ---[  15]---> BDD-cost:  107
c ---[  14]---> BDD-cost:  107
c ---[  13]---> BDD-cost:  107
c ---[  12]---> BDD-cost:  107
c ---[  11]---> BDD-cost:  107
c ---[  10]---> BDD-cost:  107
c ---[   9]---> BDD-cost:  107
c ---[   8]---> BDD-cost:  107
c ---[   7]---> BDD-cost:  107
c ---[   6]---> BDD-cost:  107
c ---[   5]---> BDD-cost:  107
c ---[   4]---> BDD-cost:  107
c ---[   3]---> BDD-cost:  107
c ---[   2]---> BDD-cost:  107
c ---[   1]---> BDD-cost:  107
c ---[   0]---> BDD-cost:  107
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    9080    26232 |    3026       0        0     nan |  0.000 % |
c |       101 |    9080    26232 |    3328     101     1819    18.0 |  4.225 % |
c |       251 |    9080    26232 |    3661     251     5151    20.5 |  4.225 % |
c |       476 |    9080    26232 |    4027     476     9792    20.6 |  4.225 % |
c |       814 |    9080    26232 |    4430     814    20689    25.4 |  4.225 % |
c |      1322 |    9080    26232 |    4873    1322    36064    27.3 |  4.225 % |
c |      2081 |    9080    26232 |    5360    2081    58572    28.1 |  4.225 % |
c |      3221 |    9080    26232 |    5896    3221    92118    28.6 |  4.225 % |
c |      4929 |    9080    26232 |    6486    4929   150690    30.6 |  4.225 % |
c |      7491 |    9080    26232 |    7135    4132   108513    26.3 |  4.225 % |
c |     11339 |    9080    26232 |    7848    7980   291311    36.5 |  4.225 % |
c |     17105 |    9080    26232 |    8633    5522   185461    33.6 |  4.225 % |
c ==============================================================================
c Found solution: 72
c ---[   0]---> Sorter-cost:33028     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25666 |   46925   114504 |   15641    5158   131922    25.6 |  4.225 % |
c |     25767 |   46925   114504 |   17205    5259   135005    25.7 |  1.158 % |
c |     25917 |   46925   114504 |   18925    5409   138704    25.6 |  1.158 % |
c |     26142 |   46925   114504 |   20818    5634   144561    25.7 |  1.158 % |
c |     26479 |   46925   114504 |   22899    5971   155030    26.0 |  1.158 % |
c |     26986 |   46925   114504 |   25189    6478   169326    26.1 |  1.158 % |
c |     27745 |   46925   114504 |   27708    7237   192918    26.7 |  1.158 % |
c |     28887 |   46925   114504 |   30479    8379   226919    27.1 |  1.158 % |
c |     30595 |   46925   114504 |   33527   10087   269917    26.8 |  1.158 % |
c |     33157 |   46925   114504 |   36880   12649   338749    26.8 |  1.158 % |
c |     37003 |   46875   114403 |   40568   16493   452030    27.4 |  1.243 % |
c |     42769 |   46875   114403 |   44625   22259   582687    26.2 |  1.243 % |
c |     51418 |   46862   114377 |   49088   30907   795116    25.7 |  1.260 % |
c |     64394 |   46792   114233 |   53996   43881  1147014    26.1 |  1.380 % |
c |     83855 |   46689   114022 |   59396   23513   481009    20.5 |  1.553 % |
c |    113047 |   46141   112856 |   65336   52687  1186597    22.5 |  2.556 % |
c ==============================================================================
c Found solution: 70
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    124253 |   45971   112500 |   15323   63888  1527900    23.9 |  2.556 % |
c |    124355 |   45946   112445 |   16855   14801   391968    26.5 |  2.995 % |
c |    124507 |   45946   112445 |   18540   14953   394834    26.4 |  2.995 % |
c |    124732 |   45946   112445 |   20394   15178   399350    26.3 |  2.995 % |
c |    125071 |   45946   112445 |   22434   15517   405436    26.1 |  2.995 % |
c |    125579 |   45946   112445 |   24677   16025   415506    25.9 |  2.995 % |
c |    126338 |   45946   112445 |   27145   16784   432450    25.8 |  2.995 % |
c |    127477 |   45946   112445 |   29860   17923   454720    25.4 |  2.995 % |
c |    129188 |   45946   112445 |   32846   19634   499324    25.4 |  2.995 % |
c |    131750 |   45946   112445 |   36130   22196   556949    25.1 |  2.995 % |
c ==============================================================================
c Found solution: 68
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    132441 |   45844   112207 |   15281   22887   573960    25.1 |  2.995 % |
c |    132541 |   45799   112110 |   16809   11540   242958    21.1 |  3.391 % |
c |    132691 |   45690   111877 |   18490   11686   246572    21.1 |  3.595 % |
c |    132916 |   45547   111566 |   20339   11906   251216    21.1 |  3.873 % |
c ==============================================================================
c Found solution: 66
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    132929 |   45547   111571 |   15182   11917   251221    21.1 |  3.873 % |
c |    133029 |   45416   111273 |   16700   12014   253603    21.1 |  4.222 % |
c |    133179 |   45416   111273 |   18370   12164   256949    21.1 |  4.222 % |
c |    133406 |   45416   111273 |   20207   12391   262096    21.2 |  4.222 % |
c |    133745 |   45416   111273 |   22227   12730   269253    21.2 |  4.222 % |
c |    134251 |   45416   111273 |   24450   13236   279749    21.1 |  4.222 % |
c |    135011 |   45358   111144 |   26895   13990   296217    21.2 |  4.349 % |
c |    136151 |   45358   111144 |   29585   15130   318904    21.1 |  4.349 % |
c |    137859 |   45358   111144 |   32543   16838   349859    20.8 |  4.349 % |
c ==============================================================================
c Found solution: 64
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    139956 |   44390   108887 |   14796   18919   390400    20.6 |  4.349 % |
c |    140057 |   44390   108887 |   16275    9561   176788    18.5 |  6.677 % |
c |    140209 |   44335   108768 |   17903    9703   180104    18.6 |  6.768 % |
c |    140434 |   44335   108768 |   19693    9928   184761    18.6 |  6.768 % |
c |    140772 |   44335   108768 |   21662   10266   191610    18.7 |  6.768 % |
c ==============================================================================
c Found solution: 62
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    140864 |   44219   108519 |   14739   10351   193325    18.7 |  6.768 % |
c |    140964 |   44204   108486 |   16212   10445   195212    18.7 |  7.067 % |
c |    141115 |   44204   108486 |   17834   10596   198146    18.7 |  7.067 % |
c |    141340 |   44204   108486 |   19617   10821   202151    18.7 |  7.067 % |
c |    141677 |   43973   107967 |   21579   11137   207718    18.7 |  7.495 % |
c |    142184 |   42664   104932 |   23737   11628   213972    18.4 | 10.463 % |
c ==============================================================================
c Found solution: 60
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    142785 |   41468   102142 |   13822   12155   220764    18.2 | 10.463 % |
c |    142885 |   41468   102142 |   15204   12255   222340    18.1 | 13.260 % |
c |    143035 |   41468   102142 |   16724   12405   224196    18.1 | 13.260 % |
c ==============================================================================
c Optimal solution: 60
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 -v673 -v674 v675 -v676 -v677 -v678 -v679 -v680 -v681 -v682 -v683 -v684 -v685 -v686 -v687 -v688 -v689 -v690 -v691 -v692 -v693 -v694 -v695 -v696 -v697 -v698 -v699 -v700 -v701 -v702 -v703 -v704 -v705 v706 -v707 -v708 -v709 -v710 -v711 -v712 -v713 -v714 -v715 -v716 -v717 -v718 -v719 -v720
c _______________________________________________________________________________
c 
c restarts              : 65
c conflicts             : 143260         (1029 /sec)
c decisions             : 224268         (1610 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 139.263 s
c _______________________________________________________________________________

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/5468/stat): 5468 (minisat+_script) R 5467 5468 1333 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1785088904 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/5468/statm): 174 3 169 147 0 27 0
[pid=5468] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libtermcap.so.2
open syscall for file tls/i686/libtermcap.so.2
open syscall for file tls/mmx/libtermcap.so.2
open syscall for file tls/libtermcap.so.2
open syscall for file i686/mmx/libtermcap.so.2
open syscall for file i686/libtermcap.so.2
open syscall for file mmx/libtermcap.so.2
open syscall for file libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/libtermcap.so.2
open syscall for file /etc/ld.so.cache
open syscall for file /lib/libtermcap.so.2
open syscall for file tls/i686/mmx/libdl.so.2
open syscall for file tls/i686/libdl.so.2
open syscall for file tls/mmx/libdl.so.2
open syscall for file tls/libdl.so.2
open syscall for file i686/mmx/libdl.so.2
open syscall for file i686/libdl.so.2
open syscall for file mmx/libdl.so.2
open syscall for file libdl.so.2
open syscall for file /oldhome/oroussel/lib/libdl.so.2
open syscall for file /lib/libdl.so.2
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /lib/tls/libc.so.6
open syscall for file /dev/tty
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
New process pid=5469
New process pid=5470
New process pid=5471
execve syscall for /bin/sed executable
One traced child (pid=5470) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=5471) exited with status: 0
One traced child (pid=5469) exited with status: 0
New process pid=5472
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc13/normalized-s4-4-3-5pb.opb

[startup+10.0036 s]
Raw data (loadavg): 0.93 0.97 0.99 2/57 5472
Raw data (/proc/5468/stat): 5468 (minisat+_script) S 5467 5468 1333 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1785088904 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5468/statm): 531 226 485 147 0 384 0
[pid=5468] vsize: 2124
Raw data (/proc/5472/stat): 5472 (minisat+_64-bit) R 5468 5468 1333 0 -1 0 2691 0 0 0 970 12 0 0 25 0 1 0 1785088909 11849728 2578 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5472/statm): 2893 2578 145 145 0 2748 0
[pid=5472] vsize: 11572
Current children cumulated CPU time (s) 9.83
Current children cumulated vsize (Kb) 13696

[startup+20.0052 s]
Raw data (loadavg): 0.94 0.97 0.99 2/57 5472
Raw data (/proc/5468/stat): 5468 (minisat+_script) S 5467 5468 1333 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1785088904 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5468/statm): 531 226 485 147 0 384 0
[pid=5468] vsize: 2124
Raw data (/proc/5472/stat): 5472 (minisat+_64-bit) R 5468 5468 1333 0 -1 0 3355 0 0 0 1959 18 0 0 25 0 1 0 1785088909 14585856 3242 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5472/statm): 3561 3242 145 145 0 3416 0
[pid=5472] vsize: 14244
Current children cumulated CPU time (s) 19.78
Current children cumulated vsize (Kb) 16368

[startup+30.0059 s]
Raw data (loadavg): 0.95 0.97 0.99 2/57 5472
Raw data (/proc/5468/stat): 5468 (minisat+_script) S 5467 5468 1333 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1785088904 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5468/statm): 531 226 485 147 0 384 0
[pid=5468] vsize: 2124
Raw data (/proc/5472/stat): 5472 (minisat+_64-bit) R 5468 5468 1333 0 -1 0 3800 0 0 0 2954 20 0 0 25 0 1 0 1785088909 16519168 3687 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5472/statm): 4033 3687 145 145 0 3888 0
[pid=5472] vsize: 16132
Current children cumulated CPU time (s) 29.75
Current children cumulated vsize (Kb) 18256

[startup+40.0065 s]
Raw data (loadavg): 0.95 0.97 0.99 2/57 5472
Raw data (/proc/5468/stat): 5468 (minisat+_script) S 5467 5468 1333 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1785088904 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5468/statm): 531 226 485 147 0 384 0
[pid=5468] vsize: 2124
Raw data (/proc/5472/stat): 5472 (minisat+_64-bit) R 5468 5468 1333 0 -1 0 4108 0 0 0 3948 23 0 0 25 0 1 0 1785088909 17797120 3995 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5472/statm): 4345 3995 145 145 0 4200 0
[pid=5472] vsize: 17380
Current children cumulated CPU time (s) 39.72
Current children cumulated vsize (Kb) 19504

[startup+50.0082 s]
Raw data (loadavg): 0.96 0.97 0.99 2/57 5472
Raw data (/proc/5468/stat): 5468 (minisat+_script) S 5467 5468 1333 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1785088904 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5468/statm): 531 226 485 147 0 384 0
[pid=5468] vsize: 2124
Raw data (/proc/5472/stat): 5472 (minisat+_64-bit) R 5468 5468 1333 0 -1 0 4353 0 0 0 4945 24 0 0 25 0 1 0 1785088909 18882560 4240 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5472/statm): 4610 4240 145 145 0 4465 0
[pid=5472] vsize: 18440
Current children cumulated CPU time (s) 49.7
Current children cumulated vsize (Kb) 20564

[startup+60.0088 s]
Raw data (loadavg): 0.97 0.97 0.99 2/57 5472
Raw data (/proc/5468/stat): 5468 (minisat+_script) S 5467 5468 1333 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1785088904 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5468/statm): 531 226 485 147 0 384 0
[pid=5468] vsize: 2124
Raw data (/proc/5472/stat): 5472 (minisat+_64-bit) R 5468 5468 1333 0 -1 0 4434 0 0 0 5944 25 0 0 25 0 1 0 1785088909 19267584 4321 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5472/statm): 4704 4321 145 145 0 4559 0
[pid=5472] vsize: 18816
Current children cumulated CPU time (s) 59.7
Current children cumulated vsize (Kb) 20940

[startup+70.0105 s]
Raw data (loadavg): 0.97 0.97 0.99 2/57 5472
Raw data (/proc/5468/stat): 5468 (minisat+_script) S 5467 5468 1333 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1785088904 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5468/statm): 531 226 485 147 0 384 0
[pid=5468] vsize: 2124
Raw data (/proc/5472/stat): 5472 (minisat+_64-bit) R 5468 5468 1333 0 -1 0 4465 0 0 0 6943 25 0 0 25 0 1 0 1785088909 19382272 4352 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5472/statm): 4732 4352 145 145 0 4587 0
[pid=5472] vsize: 18928
Current children cumulated CPU time (s) 69.69
Current children cumulated vsize (Kb) 21052

[startup+80.0121 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 5472
Raw data (/proc/5468/stat): 5468 (minisat+_script) S 5467 5468 1333 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1785088904 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5468/statm): 531 226 485 147 0 384 0
[pid=5468] vsize: 2124
Raw data (/proc/5472/stat): 5472 (minisat+_64-bit) R 5468 5468 1333 0 -1 0 4500 0 0 0 7943 26 0 0 25 0 1 0 1785088909 19562496 4387 4294967295 134512640 135094434 3221224448 3221223060 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5472/statm): 4776 4387 145 145 0 4631 0
[pid=5472] vsize: 19104
Current children cumulated CPU time (s) 79.7
Current children cumulated vsize (Kb) 21228

[startup+90.0118 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 5472
Raw data (/proc/5468/stat): 5468 (minisat+_script) S 5467 5468 1333 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1785088904 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5468/statm): 531 226 485 147 0 384 0
[pid=5468] vsize: 2124
Raw data (/proc/5472/stat): 5472 (minisat+_64-bit) R 5468 5468 1333 0 -1 0 4521 0 0 0 8942 26 0 0 25 0 1 0 1785088909 19677184 4408 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5472/statm): 4804 4408 145 145 0 4659 0
[pid=5472] vsize: 19216
Current children cumulated CPU time (s) 89.69
Current children cumulated vsize (Kb) 21340

[startup+100.012 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 5472
Raw data (/proc/5468/stat): 5468 (minisat+_script) S 5467 5468 1333 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1785088904 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5468/statm): 531 226 485 147 0 384 0
[pid=5468] vsize: 2124
Raw data (/proc/5472/stat): 5472 (minisat+_64-bit) R 5468 5468 1333 0 -1 0 4590 0 0 0 9941 27 0 0 25 0 1 0 1785088909 19951616 4477 4294967295 134512640 135094434 3221224448 3221223104 134557976 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5472/statm): 4871 4477 145 145 0 4726 0
[pid=5472] vsize: 19484
Current children cumulated CPU time (s) 99.69
Current children cumulated vsize (Kb) 21608

[startup+110.013 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 5472
Raw data (/proc/5468/stat): 5468 (minisat+_script) S 5467 5468 1333 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1785088904 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5468/statm): 531 226 485 147 0 384 0
[pid=5468] vsize: 2124
Raw data (/proc/5472/stat): 5472 (minisat+_64-bit) R 5468 5468 1333 0 -1 0 4873 0 0 0 10937 29 0 0 25 0 1 0 1785088909 21164032 4760 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5472/statm): 5167 4760 145 145 0 5022 0
[pid=5472] vsize: 20668
Current children cumulated CPU time (s) 109.67
Current children cumulated vsize (Kb) 22792

[startup+120.014 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 5472
Raw data (/proc/5468/stat): 5468 (minisat+_script) S 5467 5468 1333 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1785088904 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5468/statm): 531 226 485 147 0 384 0
[pid=5468] vsize: 2124
Raw data (/proc/5472/stat): 5472 (minisat+_64-bit) R 5468 5468 1333 0 -1 0 4882 0 0 0 11936 30 0 0 25 0 1 0 1785088909 21196800 4769 4294967295 134512640 135094434 3221224448 3221223120 134555599 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5472/statm): 5175 4769 145 145 0 5030 0
[pid=5472] vsize: 20700
Current children cumulated CPU time (s) 119.67
Current children cumulated vsize (Kb) 22824

[startup+130.014 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 5472
Raw data (/proc/5468/stat): 5468 (minisat+_script) S 5467 5468 1333 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1785088904 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5468/statm): 531 226 485 147 0 384 0
[pid=5468] vsize: 2124
Raw data (/proc/5472/stat): 5472 (minisat+_64-bit) R 5468 5468 1333 0 -1 0 4890 0 0 0 12936 30 0 0 25 0 1 0 1785088909 21229568 4777 4294967295 134512640 135094434 3221224448 3221223104 134558411 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5472/statm): 5183 4777 145 145 0 5038 0
[pid=5472] vsize: 20732
Current children cumulated CPU time (s) 129.67
Current children cumulated vsize (Kb) 22856
One traced child (pid=5472) exited with status: 30
One traced child (pid=5468) exited with status: 30
All traced children have exited ! Game is over.

Child status: 30
Real time (s): 139.954
CPU time (s): 139.629
CPU user time (s): 139.29
CPU system time (s): 0.338948
CPU usage (%): 99.7673
Max. virtual memory (cumulated for all children) (Kb): 22856

Verifier Data

Verifier:	OK	60