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-5pb.opb
MD5SUM	4ca29b1bc7e76812f7871e2b937d8a23
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	60
Optimality of the best value was proved	NO
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 numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.04084
Number of variables	720
Total number of constraints	2168
Number of constraints which are clauses	2144
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	30
Trace number 4930

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-04-13 21:10:23 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2165 boxname=wulflinc31 idbench=241 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  4ca29b1bc7e76812f7871e2b937d8a23  /oldhome/oroussel/tmp/wulflinc31/normalized-s4-4-3-5pb.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc31/normalized-s4-4-3-5pb.opb
IDLAUNCH: 2165
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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.153
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:        912224 kB
Buffers:         34572 kB
Cached:          49560 kB
SwapCached:        392 kB
Active:          45800 kB
Inactive:        41484 kB
HighTotal:      131008 kB
HighFree:        77756 kB
LowTotal:       903652 kB
LowFree:        834468 kB
SwapTotal:     2097892 kB
SwapFree:      2097452 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6832 kB
Slab:            29576 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 21:12:48 (client local time) WITH STATUS 30 IN 144.097 SECONDS
stats: 2165 0 144.097 30
#### END LAUNCHER DATA ####
#### BEGIN 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 [1mFound solution: 72[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 [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 |    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 [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 |    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 [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 |    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 [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 |    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 [1mFound solution: 62[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    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 [1mFound solution: 60[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 |    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 [1mOptimal solution: 60[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 -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         (995 /sec)
c decisions             : 224268         (1558 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 143.924 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.85 0.97 0.91 2/54 25759
Raw data (stat): 25759 (runsolver) R 25758 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479071001 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.0006 s]
Raw data (loadavg): 0.87 0.97 0.91 2/54 25759
Raw data (stat): 25759 (minisat+) R 25758 23176 23175 0 -1 0 2804 0 0 0 991 6 0 0 25 0 1 0 479071001 13799424 2712 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3369 2712 603 41 0 3328 0
vsize: 13476
[startup+20.0019 s]
Raw data (loadavg): 0.89 0.97 0.91 2/54 25759
Raw data (stat): 25759 (minisat+) R 25758 23176 23175 0 -1 0 3446 0 0 0 1989 8 0 0 25 0 1 0 479071001 16445440 3354 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4015 3354 603 41 0 3974 0
vsize: 16060
[startup+30.0029 s]
Raw data (loadavg): 0.91 0.97 0.91 2/54 25759
Raw data (stat): 25759 (minisat+) R 25758 23176 23175 0 -1 0 3896 0 0 0 2987 10 0 0 25 0 1 0 479071001 18395136 3804 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4491 3804 603 41 0 4450 0
vsize: 17964
[startup+40.0022 s]
Raw data (loadavg): 0.92 0.97 0.91 2/54 25759
Raw data (stat): 25759 (minisat+) R 25758 23176 23175 0 -1 0 4181 0 0 0 3984 11 0 0 25 0 1 0 479071001 19615744 4089 4294967295 134512640 134672761 3221224624 3221223824 134557876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4789 4089 603 41 0 4748 0
vsize: 19156
[startup+50.0034 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 25759
Raw data (stat): 25759 (minisat+) R 25758 23176 23175 0 -1 0 4440 0 0 0 4984 12 0 0 25 0 1 0 479071001 20697088 4348 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5053 4348 603 41 0 5012 0
vsize: 20212
[startup+60.0031 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 25759
Raw data (stat): 25759 (minisat+) R 25758 23176 23175 0 -1 0 4541 0 0 0 5984 12 0 0 25 0 1 0 479071001 21118976 4449 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5156 4449 603 41 0 5115 0
vsize: 20624
[startup+70.0042 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 25759
Raw data (stat): 25759 (minisat+) R 25758 23176 23175 0 -1 0 4574 0 0 0 6983 12 0 0 25 0 1 0 479071001 21262336 4482 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5191 4482 603 41 0 5150 0
vsize: 20764
[startup+80.0054 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 25759
Raw data (stat): 25759 (minisat+) R 25758 23176 23175 0 -1 0 4612 0 0 0 7983 12 0 0 25 0 1 0 479071001 21409792 4520 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5227 4520 603 41 0 5186 0
vsize: 20908
[startup+90.005 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 25759
Raw data (stat): 25759 (minisat+) R 25758 23176 23175 0 -1 0 4632 0 0 0 8983 12 0 0 25 0 1 0 479071001 21606400 4540 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5275 4540 603 41 0 5234 0
vsize: 21100
[startup+100.005 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 25759
Raw data (stat): 25759 (minisat+) R 25758 23176 23175 0 -1 0 4660 0 0 0 9983 13 0 0 25 0 1 0 479071001 21606400 4568 4294967295 134512640 134672761 3221224624 3221223792 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5275 4568 603 41 0 5234 0
vsize: 21100
[startup+110.005 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 25759
Raw data (stat): 25759 (minisat+) R 25758 23176 23175 0 -1 0 4993 0 0 0 10982 13 0 0 25 0 1 0 479071001 23040000 4901 4294967295 134512640 134672761 3221224624 3221223728 134554679 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5625 4901 603 41 0 5584 0
vsize: 22500
[startup+120.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 25759
Raw data (stat): 25759 (minisat+) R 25758 23176 23175 0 -1 0 4993 0 0 0 11982 14 0 0 25 0 1 0 479071001 23040000 4901 4294967295 134512640 134672761 3221224624 3221223760 134560640 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5625 4901 603 41 0 5584 0
vsize: 22500
[startup+130.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 25759
Raw data (stat): 25759 (minisat+) R 25758 23176 23175 0 -1 0 5001 0 0 0 12983 14 0 0 25 0 1 0 479071001 23040000 4909 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5625 4909 603 41 0 5584 0
vsize: 22500
[startup+140.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 25759
Raw data (stat): 25759 (minisat+) R 25758 23176 23175 0 -1 0 5009 0 0 0 13982 14 0 0 25 0 1 0 479071001 23134208 4917 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5648 4917 603 41 0 5607 0
vsize: 22592
[startup+144.132 s]
Raw data (loadavg): 0.98 0.97 0.91 1/53 25759
Raw data (stat): 25759 (minisat+) R 25758 23176 23175 0 -1 0 5009 0 0 0 13982 14 0 0 25 0 1 0 479071001 23134208 4917 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5648 4917 603 41 0 5607 0
vsize: 0

Child status: 30
Real time (s): 144.132
CPU time (s): 144.097
CPU user time (s): 143.943
CPU system time (s): 0.153976
CPU usage (%): 99.9761
Max. virtual memory (Kb): 22592
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	60
#### END VERIFIER DATA ####