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-4pb.opb
MD5SUM	c1a86b94297136b91215b2ae8a8f5643
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	696
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	696
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	696
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.03784
Number of variables	696
Total number of constraints	2096
Number of constraints which are clauses	2072
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	29
Trace number 30408

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc4 THE 2005-05-25 16:51:46 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=21822 boxname=wulflinc4 idbench=240 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  c1a86b94297136b91215b2ae8a8f5643  /oldhome/oroussel/tmp/wulflinc4/normalized-s4-4-3-4pb.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc4/normalized-s4-4-3-4pb.opb
IDLAUNCH: 21822
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        613648 kB
Buffers:         34812 kB
Cached:         365992 kB
SwapCached:        600 kB
Active:          75868 kB
Inactive:       327448 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        613396 kB
SwapTotal:     2097136 kB
SwapFree:      2096004 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5784 kB
Slab:            12000 kB
Committed_AS:    71792 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 16:57:10 (client local time) WITH STATUS 30 IN 324.027 SECONDS
stats: 21822 0 324.027 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2096 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################################################################################################################
c   -- Clauses(.)/Splits(s): ................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[2082]---> BDD-cost:    1
c ---[2056]---> BDD-cost:    1
c ---[2034]---> BDD-cost:    1
c ---[2024]---> BDD-cost:    1
c ---[2022]---> BDD-cost:    1
c ---[1996]---> BDD-cost:    1
c ---[1978]---> BDD-cost:    1
c ---[1952]---> BDD-cost:    1
c ---[1950]---> BDD-cost:    1
c ---[1924]---> BDD-cost:    1
c ---[1906]---> BDD-cost:    1
c ---[1880]---> BDD-cost:    1
c ---[1866]---> BDD-cost:    1
c ---[1840]---> BDD-cost:    1
c ---[1818]---> BDD-cost:    1
c ---[1808]---> BDD-cost:    1
c ---[1794]---> BDD-cost:    1
c ---[1768]---> BDD-cost:    1
c ---[1746]---> BDD-cost:    1
c ---[1736]---> BDD-cost:    1
c ---[1699]---> BDD-cost:    1
c ---[1677]---> BDD-cost:    1
c ---[1671]---> BDD-cost:    1
c ---[1665]---> BDD-cost:    1
c ---[1663]---> BDD-cost:    1
c ---[1637]---> BDD-cost:    1
c ---[1619]---> BDD-cost:    1
c ---[1593]---> BDD-cost:    1
c ---[1557]---> BDD-cost:    1
c ---[1535]---> BDD-cost:    1
c ---[1529]---> BDD-cost:    1
c ---[1523]---> BDD-cost:    1
c ---[1474]---> BDD-cost:    1
c ---[1464]---> BDD-cost:    1
c ---[1454]---> BDD-cost:    1
c ---[1452]---> BDD-cost:    1
c ---[1446]---> BDD-cost:    1
c ---[1428]---> BDD-cost:    1
c ---[1390]---> BDD-cost:    1
c ---[1380]---> BDD-cost:    1
c ---[1378]---> BDD-cost:    1
c ---[1352]---> BDD-cost:    1
c ---[1334]---> BDD-cost:    1
c ---[1309]---> BDD-cost:    1
c ---[1291]---> BDD-cost:    1
c ---[1269]---> BDD-cost:    1
c ---[1243]---> BDD-cost:    1
c ---[1237]---> BDD-cost:    1
c ---[1235]---> BDD-cost:    1
c ---[1209]---> BDD-cost:    1
c ---[1191]---> BDD-cost:    1
c ---[1165]---> BDD-cost:    1
c ---[1112]---> BDD-cost:    1
c ---[1102]---> BDD-cost:    1
c ---[1096]---> BDD-cost:    1
c ---[1094]---> BDD-cost:    1
c ---[1057]---> BDD-cost:    1
c ---[1035]---> BDD-cost:    1
c ---[1029]---> BDD-cost:    1
c ---[1023]---> BDD-cost:    1
c ---[ 991]---> BDD-cost:    1
c ---[ 965]---> BDD-cost:    1
c ---[ 963]---> BDD-cost:    1
c ---[ 953]---> BDD-cost:    1
c ---[ 951]---> BDD-cost:    1
c ---[ 925]---> BDD-cost:    1
c ---[ 907]---> BDD-cost:    1
c ---[ 881]---> BDD-cost:    1
c ---[ 879]---> BDD-cost:    1
c ---[ 853]---> BDD-cost:    1
c ---[ 835]---> BDD-cost:    1
c ---[ 809]---> BDD-cost:    1
c ---[ 760]---> BDD-cost:    1
c ---[ 750]---> BDD-cost:    1
c ---[ 740]---> BDD-cost:    1
c ---[ 738]---> BDD-cost:    1
c ---[ 732]---> BDD-cost:    1
c ---[ 714]---> BDD-cost:    1
c ---[ 676]---> BDD-cost:    1
c ---[ 666]---> BDD-cost:    1
c ---[ 629]---> BDD-cost:    1
c ---[ 607]---> BDD-cost:    1
c ---[ 601]---> BDD-cost:    1
c ---[ 595]---> BDD-cost:    1
c ---[ 589]---> BDD-cost:    1
c ---[ 571]---> BDD-cost:    1
c ---[ 533]---> BDD-cost:    1
c ---[ 523]---> BDD-cost:    1
c ---[ 513]---> BDD-cost:    1
c ---[ 503]---> BDD-cost:    1
c ---[ 453]---> BDD-cost:    1
c ---[ 451]---> BDD-cost:    1
c ---[ 414]---> BDD-cost:    1
c ---[ 392]---> BDD-cost:    1
c ---[ 386]---> BDD-cost:    1
c ---[ 380]---> BDD-cost:    1
c ---[ 370]---> BDD-cost:    1
c ---[ 360]---> BDD-cost:    1
c ---[ 310]---> BDD-cost:    1
c ---[ 308]---> BDD-cost:    1
c ---[ 298]---> BDD-cost:    1
c ---[ 289]---> BDD-cost:    1
c ---[ 239]---> BDD-cost:    1
c ---[ 237]---> BDD-cost:    1
c ---[ 200]---> BDD-cost:    1
c ---[ 178]---> BDD-cost:    1
c ---[ 172]---> BDD-cost:    1
c ---[ 166]---> BDD-cost:    1
c ---[ 149]---> BDD-cost:    1
c ---[ 127]---> BDD-cost:    1
c ---[ 101]---> BDD-cost:    1
c ---[  95]---> 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:  103
c ---[  22]---> BDD-cost:  103
c ---[  21]---> BDD-cost:  103
c ---[  20]---> BDD-cost:  103
c ---[  19]---> BDD-cost:  103
c ---[  18]---> BDD-cost:  103
c ---[  17]---> BDD-cost:  103
c ---[  16]---> BDD-cost:  103
c ---[  15]---> BDD-cost:  103
c ---[  14]---> BDD-cost:  103
c ---[  13]---> BDD-cost:  103
c ---[  12]---> BDD-cost:  103
c ---[  11]---> BDD-cost:  103
c ---[  10]---> BDD-cost:  103
c ---[   9]---> BDD-cost:  103
c ---[   8]---> BDD-cost:  103
c ---[   7]---> BDD-cost:  103
c ---[   6]---> BDD-cost:  103
c ---[   5]---> BDD-cost:  103
c ---[   4]---> BDD-cost:  103
c ---[   3]---> BDD-cost:  103
c ---[   2]---> BDD-cost:  103
c ---[   1]---> BDD-cost:  103
c ---[   0]---> BDD-cost:  103
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    8744    25274 |    2914       0        0     nan |  0.000 % |
c |       102 |    8744    25274 |    3205     102     1854    18.2 |  4.263 % |
c |       252 |    8744    25274 |    3525     252     8914    35.4 |  4.263 % |
c |       480 |    8744    25274 |    3878     480    16252    33.9 |  4.263 % |
c |       818 |    8744    25274 |    4266     818    27632    33.8 |  4.263 % |
c |      1330 |    8744    25274 |    4693    1330    40079    30.1 |  4.263 % |
c |      2092 |    8744    25274 |    5162    2092    66220    31.7 |  4.263 % |
c |      3234 |    8744    25274 |    5678    3234   112659    34.8 |  4.263 % |
c |      4947 |    8744    25274 |    6246    4947   200492    40.5 |  4.263 % |
c |      7511 |    8744    25274 |    6871    4053   147677    36.4 |  4.263 % |
c |     11355 |    8744    25274 |    7558    4314   120608    28.0 |  4.263 % |
c ==============================================================================
c [1mFound solution: 70[0m
c ---[   0]---> Sorter-cost:31844     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16770 |   45551   111127 |   15183    5795   193248    33.3 |  4.263 % |
c |     16870 |   45551   111127 |   16701    5895   196033    33.3 |  0.554 % |
c |     17020 |   45551   111127 |   18371    6045   200593    33.2 |  0.554 % |
c |     17246 |   45551   111127 |   20208    6271   207325    33.1 |  0.554 % |
c |     17584 |   45551   111127 |   22229    6609   218144    33.0 |  0.554 % |
c |     18090 |   45551   111127 |   24452    7115   233458    32.8 |  0.554 % |
c |     18850 |   45551   111127 |   26897    7875   260928    33.1 |  0.554 % |
c |     19989 |   45551   111127 |   29587    9014   303975    33.7 |  0.554 % |
c |     21698 |   45551   111127 |   32546   10723   364355    34.0 |  0.554 % |
c |     24260 |   45539   111103 |   35800   13284   454653    34.2 |  0.576 % |
c |     28104 |   45539   111103 |   39380   17128   569292    33.2 |  0.576 % |
c |     33870 |   45519   111063 |   43318   22892   762166    33.3 |  0.609 % |
c |     42519 |   45519   111063 |   47650   31541  1014782    32.2 |  0.609 % |
c |     55493 |   45494   111012 |   52415   44514  1375081    30.9 |  0.656 % |
c |     74956 |   45494   111012 |   57657   25926   619156    23.9 |  0.656 % |
c |    104148 |   45469   110961 |   63423   55117  1371941    24.9 |  0.703 % |
c |    147937 |   45425   110871 |   69765   51217  1026070    20.0 |  0.787 % |
c ==============================================================================
c [1mFound solution: 68[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    162691 |   45251   110490 |   15083   65969  1325224    20.1 |  0.787 % |
c |    162794 |   45251   110490 |   16591    8596   150390    17.5 |  1.268 % |
c |    162945 |   45251   110490 |   18250    8747   153049    17.5 |  1.268 % |
c |    163171 |   45251   110490 |   20075    8973   158495    17.7 |  1.268 % |
c |    163509 |   45251   110490 |   22083    9311   165961    17.8 |  1.268 % |
c |    164018 |   45251   110490 |   24291    9820   177554    18.1 |  1.268 % |
c |    164777 |   45251   110490 |   26720   10579   194824    18.4 |  1.268 % |
c |    165917 |   45251   110490 |   29392   11719   225785    19.3 |  1.268 % |
c |    167625 |   45107   110183 |   32331   13424   256721    19.1 |  1.559 % |
c |    170187 |   45062   110088 |   35564   15985   311087    19.5 |  1.639 % |
c |    174032 |   45062   110088 |   39121   19830   393033    19.8 |  1.639 % |
c |    179798 |   45062   110088 |   43033   25596   497332    19.4 |  1.639 % |
c |    188447 |   45062   110088 |   47336   34245   694865    20.3 |  1.639 % |
c ==============================================================================
c [1mFound solution: 66[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    189825 |   45062   110090 |   15020   35623   718705    20.2 |  1.639 % |
c |    189925 |   44941   109835 |   16522   14357   276516    19.3 |  1.930 % |
c |    190080 |   44941   109835 |   18174   14512   279937    19.3 |  1.930 % |
c |    190305 |   44941   109835 |   19991   14737   284880    19.3 |  1.930 % |
c |    190642 |   44802   109541 |   21990   15070   291877    19.4 |  2.196 % |
c ==============================================================================
c [1mFound solution: 64[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    191120 |   44421   108654 |   14807   15548   314191    20.2 |  2.196 % |
c |    191220 |   44421   108654 |   16287   15648   318112    20.3 |  3.210 % |
c |    191371 |   44331   108462 |   17916   15792   323356    20.5 |  3.381 % |
c |    191598 |   44331   108462 |   19708   16019   327914    20.5 |  3.381 % |
c |    191935 |   44331   108462 |   21678   16356   334846    20.5 |  3.381 % |
c |    192443 |   44331   108462 |   23846   16864   347077    20.6 |  3.381 % |
c |    193204 |   44331   108462 |   26231   17625   362351    20.6 |  3.381 % |
c |    194343 |   44225   108234 |   28854   18759   388671    20.7 |  3.588 % |
c |    196052 |   44113   107994 |   31740   20456   426188    20.8 |  3.799 % |
c |    198614 |   43964   107671 |   34914   23013   484185    21.0 |  4.098 % |
c |    202459 |   43964   107671 |   38405   26858   551368    20.5 |  4.098 % |
c ==============================================================================
c [1mFound solution: 62[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    203064 |   43962   107664 |   14654   27463   562617    20.5 |  4.098 % |
c |    203165 |   43962   107664 |   16119   13833   248851    18.0 |  4.168 % |
c |    203315 |   43962   107664 |   17731   13983   252059    18.0 |  4.168 % |
c |    203540 |   43893   107521 |   19504   14205   258006    18.2 |  4.292 % |
c |    203877 |   43893   107521 |   21454   14542   265507    18.3 |  4.292 % |
c |    204383 |   43865   107460 |   23600   15047   275133    18.3 |  4.350 % |
c |    205142 |   43865   107460 |   25960   15806   288978    18.3 |  4.350 % |
c |    206281 |   43788   107291 |   28556   16939   312056    18.4 |  4.507 % |
c |    207989 |   43732   107173 |   31412   18644   347555    18.6 |  4.609 % |
c ==============================================================================
c [1mFound solution: 60[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    209269 |   43594   106848 |   14531   19906   372723    18.7 |  4.609 % |
c |    209369 |   43594   106848 |   15984   10053   172758    17.2 |  5.021 % |
c |    209522 |   43554   106760 |   17582   10204   174881    17.1 |  5.097 % |
c |    209749 |   43467   106570 |   19340   10422   178532    17.1 |  5.272 % |
c |    210086 |   43270   106132 |   21274   10744   182597    17.0 |  5.690 % |
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
c _______________________________________________________________________________
c 
c restarts              : 71
c conflicts             : 210539         (650 /sec)
c decisions             : 317098         (980 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 323.724 s
c _______________________________________________________________________________
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.95 0.98 2/54 3171
Raw data (stat): 3171 (runsolver) R 3170 21152 21151 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 782230969 1052672 99 4294967295 134512640 135381576 3221224496 3221219704 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0014 s]
Raw data (loadavg): 0.93 0.95 0.98 2/55 3175
Raw data (stat): 3171 (minisat+_script) S 3170 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782230969 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0023 s]
Raw data (loadavg): 0.94 0.96 0.98 2/55 3175
Raw data (stat): 3171 (minisat+_script) S 3170 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782230969 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0026 s]
Raw data (loadavg): 0.95 0.96 0.98 2/55 3175
Raw data (stat): 3171 (minisat+_script) S 3170 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782230969 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.003 s]
Raw data (loadavg): 0.95 0.96 0.98 2/55 3175
Raw data (stat): 3171 (minisat+_script) S 3170 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782230969 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0039 s]
Raw data (loadavg): 0.96 0.96 0.98 2/55 3175
Raw data (stat): 3171 (minisat+_script) S 3170 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782230969 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0042 s]
Raw data (loadavg): 0.97 0.96 0.98 2/55 3175
Raw data (stat): 3171 (minisat+_script) S 3170 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782230969 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0055 s]
Raw data (loadavg): 0.97 0.96 0.98 2/55 3175
Raw data (stat): 3171 (minisat+_script) S 3170 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782230969 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0064 s]
Raw data (loadavg): 0.98 0.96 0.98 2/55 3175
Raw data (stat): 3171 (minisat+_script) S 3170 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782230969 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0068 s]
Raw data (loadavg): 0.98 0.96 0.98 2/55 3175
Raw data (stat): 3171 (minisat+_script) S 3170 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782230969 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.007 s]
Raw data (loadavg): 0.98 0.96 0.98 2/55 3175
Raw data (stat): 3171 (minisat+_script) S 3170 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782230969 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.008 s]
Raw data (loadavg): 0.98 0.96 0.98 2/55 3175
Raw data (stat): 3171 (minisat+_script) S 3170 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782230969 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 3175
Raw data (stat): 3171 (minisat+_script) S 3170 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782230969 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.01 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 3175
Raw data (stat): 3171 (minisat+_script) S 3170 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782230969 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.011 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 3175
Raw data (stat): 3171 (minisat+_script) S 3170 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782230969 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.011 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 3175
Raw data (stat): 3171 (minisat+_script) S 3170 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782230969 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.011 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 3175
Raw data (stat): 3171 (minisat+_script) S 3170 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782230969 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.011 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 3175
Raw data (stat): 3171 (minisat+_script) S 3170 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782230969 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.012 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 3175
Raw data (stat): 3171 (minisat+_script) S 3170 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782230969 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.013 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 3175
Raw data (stat): 3171 (minisat+_script) S 3170 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782230969 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.013 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 3175
Raw data (stat): 3171 (minisat+_script) S 3170 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782230969 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 3175
Raw data (stat): 3171 (minisat+_script) S 3170 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782230969 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 3175
Raw data (stat): 3171 (minisat+_script) S 3170 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782230969 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 3175
Raw data (stat): 3171 (minisat+_script) S 3170 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782230969 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 3175
Raw data (stat): 3171 (minisat+_script) S 3170 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782230969 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 3175
Raw data (stat): 3171 (minisat+_script) S 3170 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782230969 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.017 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 3175
Raw data (stat): 3171 (minisat+_script) S 3170 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782230969 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.017 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 3175
Raw data (stat): 3171 (minisat+_script) S 3170 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782230969 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.018 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 3175
Raw data (stat): 3171 (minisat+_script) S 3170 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782230969 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.019 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 3175
Raw data (stat): 3171 (minisat+_script) S 3170 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782230969 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.018 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 3175
Raw data (stat): 3171 (minisat+_script) S 3170 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782230969 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.018 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 3175
Raw data (stat): 3171 (minisat+_script) S 3170 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782230969 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.018 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 3175
Raw data (stat): 3171 (minisat+_script) S 3170 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782230969 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+324.042 s]
Raw data (loadavg): 0.99 0.97 0.98 1/53 3175
Raw data (stat): 3171 (minisat+_script) S 3170 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782230969 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 30
Real time (s): 324.042
CPU time (s): 324.027
CPU user time (s): 323.741
CPU system time (s): 0.285956
CPU usage (%): 99.9954
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	60
#### END VERIFIER DATA ####