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/web/uclid_pb_benchmarks/normalized-blast-tlan2.ucl.opb
MD5SUM	7100a312d793a62875e04da08d79c5f4
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	0
Biggest coefficient in the objective function	0
Number of bits for the biggest coefficient in the objective function	0
Sum of the numbers in the objective function	0
Number of bits of the sum of numbers in the objective function	0
Biggest number in a constraint	641
Number of bits of the biggest number in a constraint	10
Biggest sum of numbers in a constraint	2174
Number of bits of the biggest sum of numbers	12
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.350946
Number of variables	2221
Total number of constraints	3050
Number of constraints which are clauses	2330
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	720
Minimum length of a constraint	1
Maximum length of a constraint	19

Trace number 4400

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-04-13 17:17:50 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2376 boxname=wulflinc20 idbench=264 idsolver=9 numberseed=0
MD5SUM SOLVER: daf345f6fbf228671abfac48013b9cac  /oldhome/oroussel/solvers/sat4jPseudo.jar
MD5SUM BENCH:  7100a312d793a62875e04da08d79c5f4  /oldhome/oroussel/tmp/wulflinc20/normalized-blast-tlan2.ucl.opb
REAL COMMAND:  java -server -Xms650M -Xmx650M -jar /oldhome/oroussel/solvers/sat4jPseudo.jar /oldhome/oroussel/tmp/wulflinc20/normalized-blast-tlan2.ucl.opb
IDLAUNCH: 2376
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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.215
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:        912084 kB
Buffers:         31352 kB
Cached:          55840 kB
SwapCached:       2636 kB
Active:          39096 kB
Inactive:        53512 kB
HighTotal:      131008 kB
HighFree:        71512 kB
LowTotal:       903652 kB
LowFree:        840572 kB
SwapTotal:     2097892 kB
SwapFree:      2095256 kB
Dirty:              64 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            24416 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 17:18:08 (client local time) WITH STATUS 30 IN  SECONDS
stats: 2376 6  30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c solving /oldhome/oroussel/tmp/wulflinc20/normalized-blast-tlan2.ucl.opb
c reading problem 
c [nbvar=2221]
c [nbconstr=3050]
c time 4.932
c #vars     2221
c #clauses  3050
c starts	: 0
c conflicts	: 0
c decisions	: 0
c propagations	: 0
c inspects	: 0
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 0
c SATISFIABLE
c OPTIMIZING...
c 
c CURRENT OPTIMUM=0
c Total CPU time (ms) : 17.114
c 
s OPTIMUM FOUND
v v1432 v1 v2 -v1433 -v21 v22 v1434 v1435 v23 v24 v1436 v43 v44 v1437 v63 v64 v1438 v83 v84 v1439 v94 v95 v1440 v114 v115 v1441 v125 v126 v1442 v145 v146 v1443 v156 v157 v1444 v167 v168 v1445 v178 v179 v1446 v189 v190 v1447 v200 v201 v1448 v211 v212 -v1449 -v222 v223 -v1450 -v233 v234 -v1451 -v1452 v253 -v254 -v1453 v1454 v1455 v264 v265 v1456 v1457 v1458 v275 v276 v1459 v286 v287 v1460 v297 v298 v1461 v308 v309 v1462 v319 v320 v1463 v330 v331 v1464 v341 v342 v1465 v352 v353 v1466 v363 v364 v1467 v374 v375 v1468 v385 v386 v1469 v396 v397 v1470 v407 v408 v1471 v418 v419 -v1472 -v429 v430 v1473 v431 v432 -v1474 -v1475 -v1476 -v451 v452 -v1477 -v1478 -v1479 -v1480 v462 -v463 -v1481 v1482 v1483 v473 v474 v1484 v475 v476 v1485 v1486 v1487 v1488 v477 v478 v1489 -v1490 -v1491 -v1492 -v479 v480 -v1493 v1494 v1495 v1496 v490 v491 v1497 v501 v502 v1498 v512 v513 -v1499 -v523 v524 -v1500 v525 -v526 -v1501 v1502 -v1503 v536 -v537 -v1504 -v1505 v1506 v1507 -v1508 -v538 v539 -v1509 -v1510 -v1511 -v1512 v1513 v549 v550 -v1514 v1515 v1516 v560 v561 -v1517 -v1518 v562 -v563 -v1519 -v1520 -v1521 -v1522 -v1523 -v1524 -v564 v565 -v1525 v1526 v1527 v566 v567 -v1528 -v1529 -v1530 -v1531 -v1532 -v1533 -v1534 -v1535 v1536 -v1537 -v1538 -v1539 v568 -v569 -v1540 -v1541 -v1542 -v1543 -v1544 -v1545 -v1546 -v1547 -v570 v571 -v1548 v1549 v1550 v1551 v1552 v572 v573 v1553 v1554 v1555 v1556 v1557 v583 v584 v1558 v594 v595 v1559 v605 v606 v1560 v616 v617 v1561 v627 v628 v1562 -v1563 v1564 v638 v639 -v1565 v1566 v1567 v649 v650 v1568 v660 v661 v1569 v671 v672 v1570 v691 v692 v1571 v711 v712 v1572 v722 v723 v1573 v733 v734 v1574 v744 v745 v1575 v746 v747 v1576 -v1577 v1578 v757 v758 -v1579 -v1580 v1581 v759 v760 -v1582 -v1583 -v1584 v1585 v761 v762 -v1586 -v1587 -v1588 -v1589 -v1590 -v1591 v1592 -v1593 -v763 v764 v1594 -v1595 -v1596 -v783 v784 -v1597 v1598 v794 v795 v1599 v1600 v1601 v796 v797 -v1602 -v798 v799 v1603 v818 v819 -v1604 v1605 v1606 v820 v821 v1607 v1608 v1609 v831 v832 v1610 v842 v843 v1611 -v1612 v1613 v853 v854 -v1614 v1615 v1616 v864 v865 v1617 v866 -v867 -v1618 -v877 -v878 -v1619 -v888 -v889 -v1620 -v908 -v909 -v1621 -v910 -v911 -v1622 -v921 -v922 -v1623 -v941 -v942 -v1624 -v943 -v944 -v1625 -v954 -v955 -v1626 -v965 -v966 -v1627 -v976 -v977 -v1628 -v978 -v979 -v1629 -v989 -v990 -v1630 -v1000 -v1001 -v1631 -v1002 -v1003 -v1632 -v1013 -v1014 -v1633 -v1024 -v1025 -v1634 -v1044 -v1045 -v1635 -v1046 -v1047 v1636 v1057 v1058 v1637 v1068 v1069 -v1638 -v1639 v1640 v1070 v1071 -v1641 -v1642 -v1643 -v1644 -v1072 v1073 -v1645 -v1646 -v1647 v1648 -v1649 -v1650 -v1651 -v1074 v1075 -v1652 -v1653 -v1654 -v1655 -v1656 v1657 v1085 v1086 -v1658 v1659 -v1660 v1096 -v1097 -v1661 -v1662 v1663 v1098 v1099 -v1664 -v1665 -v1666 v1667 -v1668 -v1669 -v1670 -v1100 v1101 -v1671 v1672 -v1673 v1102 -v1103 v1674 -v1675 -v1676 v1677 -v1678 -v1679 -v1680 -v1681 -v1682 -v1683 -v1684 -v1685 -v1686 -v1687 -v1688 -v1689 v1690 v1104 v1105 -v1691 -v1692 -v1693 -v1694 v1695 -v1696 -v1697 -v1698 -v1699 -v1106 v1107 -v1700 v1701 -v1702 v1108 -v1109 -v1703 -v1704 -v1705 v1706 -v1707 -v1708 -v1709 -v1710 -v1711 -v1712 -v1713 -v1714 -v1715 -v1716 -v1717 -v1718 -v1719 -v1720 -v1721 -v1722 -v1723 -v1724 -v1725 -v1726 -v1727 -v1728 -v1729 -v1110 v1111 -v1730 -v1731 -v1732 -v1733 -v1734 -v1735 -v1736 -v1737 -v1738 -v1739 v1740 v1112 v1113 -v1741 v1742 v1743 v1744 v1745 v1746 v1114 v1115 v1747 v1748 v1749 v1750 -v1751 -v1752 -v1125 -v1126 -v1753 -v1136 -v1137 -v1754 -v1138 -v1139 -v1755 -v1149 -v1150 -v1756 -v1160 -v1161 -v1757 -v1180 -v1181 -v1758 -v1182 -v1183 -v1759 v1193 -v1194 -v1760 -v1195 v1196 -v1761 v1206 -v1207 -v1762 -v1763 v1764 v1217 v1218 -v1765 v1766 -v1767 v1228 -v1229 -v1768 v1769 -v1770 v1230 -v1231 -v1771 -v1772 -v1773 -v1774 -v1775 -v1232 v1233 -v1776 v1777 -v1778 v1234 -v1235 -v1779 -v1780 -v1781 -v1782 -v1783 v1784 -v1785 -v1786 -v1787 v1236 -v1237 -v1788 -v1789 -v1790 -v1791 -v1792 -v1793 -v1794 -v1238 v1239 -v1795 v1796 -v1797 v1240 -v1241 -v1798 -v1799 -v1800 -v1801 -v1802 -v1803 -v1804 -v1805 -v1806 -v1807 -v1808 -v1809 v1810 -v1811 v1242 -v1243 -v1812 -v1813 -v1814 -v1815 -v1816 -v1817 -v1818 -v1819 v1820 v1244 v1245 -v1821 v1822 -v1823 v1246 -v1247 -v1824 -v1825 -v1826 -v1827 -v1828 -v1829 -v1830 -v1831 -v1832 -v1833 -v1834 v1835 -v1836 -v1837 -v1838 -v1839 -v1840 -v1841 -v1842 v1248 -v1249 -v1843 -v1844 -v1845 -v1846 -v1847 -v1848 -v1849 -v1850 -v1851 -v1852 v1853 v1250 v1251 -v1854 v1855 v1856 v1857 v1858 v1859 v1860 v1252 v1253 v1861 v1862 v1863 v1864 v1865 -v1866 -v1867 -v1263 -v1264 -v1868 -v1274 -v1275 -v1869 -v1276 -v1277 -v1870 -v1287 -v1288 -v1871 -v1298 -v1299 -v1872 -v1309 -v1310 -v1873 -v1311 -v1312 v1874 v1322 v1323 v1875 v1333 v1334 -v1876 -v1877 v1878 v1335 v1336 -v1879 -v1880 -v1881 -v1882 -v1337 v1338 -v1883 -v1884 -v1885 v1886 v1887 v1339 v1340 v1888 -v1889 -v1890 -v1891 -v1892 -v1893 -v1894 -v1895 -v1896 -v1341 v1342 -v1897 -v1898 -v1899 -v1900 -v1901 -v1902 -v1903 v1352 -v1353 -v1904 v1905 -v1906 v1354 -v1355 -v1907 -v1908 -v1909 -v1910 v1356 -v1357 -v1911 -v1912 -v1913 -v1914 v1915 -v1916 -v1917 -v1918 -v1358 v1359 -v1919 v1920 -v1921 v1360 -v1361 v1922 -v1923 -v1924 v1925 -v1926 -v1927 -v1928 -v1929 -v1930 -v1931 -v1932 -v1933 -v1934 -v1935 -v1936 -v1937 -v1938 -v1939 -v1940 -v1941 -v1942 -v1943 v1362 -v1363 -v1944 -v1945 -v1946 -v1947 -v1948 v1949 -v1950 -v1951 -v1952 -v1953 -v1364 v1365 -v1954 v1955 -v1956 v1366 -v1367 -v1957 -v1958 -v1959 v1960 -v1961 -v1962 -v1963 -v1964 -v1965 -v1966 -v1967 -v1968 -v1969 -v1970 -v1971 -v1972 -v1973 -v1974 -v1975 -v1976 -v1977 -v1978 -v1979 -v1980 -v1981 -v1982 -v1983 -v1984 -v1985 -v1986 -v1987 -v1988 -v1989 -v1990 v1991 v1368 v1369 -v1992 -v1993 -v1994 -v1995 -v1996 -v1997 -v1998 -v1999 -v2000 -v2001 -v2002 -v2003 v1370 -v1371 -v2004 v2005 v2006 v1372 v1373 v2007 -v2008 -v2009 -v2010 -v2011 -v2012 -v2013 -v2014 -v2015 v2016 -v2017 -v2018 -v2019 -v2020 -v2021 -v2022 -v2023 -v2024 -v2025 -v2026 -v2027 -v2028 -v2029 -v2030 -v2031 -v2032 -v2033 -v2034 -v2035 -v2036 -v2037 -v2038 -v2039 -v2040 -v2041 -v2042 -v2043 -v2044 -v2045 -v2046 -v2047 -v2048 -v2049 -v2050 -v2051 -v2052 -v2053 -v2054 v1374 -v1375 -v2055 -v2056 -v2057 -v2058 -v2059 -v2060 -v2061 v2062 v2063 v2064 v2065 v2066 v2067 -v2068 v1376 -v1377 -v2069 -v2070 -v2071 -v1378 v1379 -v2072 -v2073 v2074 -v2075 -v2076 -v2077 -v2078 -v2079 -v2080 -v2081 -v2082 -v2083 -v2084 -v2085 -v2086 -v2087 -v2088 -v2089 -v2090 -v2091 -v2092 -v2093 -v2094 -v2095 -v1380 v1381 -v2096 -v2097 -v2098 -v2099 -v2100 -v2101 -v2102 -v2103 -v2104 -v2105 -v2106 -v2107 -v2108 v1382 -v1383 -v2109 v2110 -v2111 -v2112 -v2113 -v2114 -v2115 -v2116 -v1384 v1385 -v2117 -v2118 -v2119 -v2120 -v2121 -v2122 -v2123 -v2124 -v1395 -v1396 -v2125 -v1406 -v1407 -v2126 -v1408 -v1409 -v2127 -v1419 -v1420 -v2128 -v1430 -v1431 -v2129 -v2130 -v2131 -v2132 -v2133 -v2134 -v2135 -v2136 -v2137 -v2138 -v2139 -v2140 -v2141 -v2142 -v2143 -v2144 -v2145 -v2146 -v2147 -v2148 -v2149 -v2150 -v2151 -v2152 -v2153 -v2154 -v2155 -v2156 -v2157 -v2158 -v2159 -v2160 -v2161 -v2162 -v2163 -v2164 -v2165 -v2166 v2167 v2168 v2169 v2170 v2171 v2172 v2173 v2174 v2175 v2176 v2177 v2178 v2179 v2180 v2181 v2182 v2183 v2184 v2185 v2186 v2187 v2188 v2189 v2190 v2191 v2192 v2193 v2194 v2195 v2196 v2197 v2198 v2199 v2200 v2201 v2202 v2203 v2204 v2205 v2206 v2207 v2208 v2209 v2210 v2211 v2212 v2213 v2214 v2215 v2216 v2217 v2218 v2219 v2220 v2221 -v3 -v4 -v5 -v6 -v7 -v8 -v9 -v10 v11 -v12 -v13 -v14 -v15 -v16 -v17 -v18 -v19 -v20 v25 v26 v27 v28 v29 v30 v31 v32 v33 v34 v35 v36 v37 v38 v39 v40 v41 v42 -v45 -v46 -v47 -v48 -v49 -v50 -v51 -v52 -v53 -v54 -v55 -v56 -v57 -v58 -v59 -v60 -v61 -v62 -v65 -v66 -v67 -v68 -v69 v70 -v71 -v72 -v73 -v74 -v75 -v76 -v77 -v78 -v79 -v80 -v81 -v82 -v85 -v86 -v87 -v88 -v89 v90 v91 -v92 v93 -v96 -v97 -v98 -v99 -v100 -v101 -v102 -v103 -v104 -v105 -v106 -v107 -v108 -v109 -v110 -v111 -v112 -v113 -v116 -v117 -v118 -v119 -v120 -v121 -v122 -v123 -v124 v127 v128 v129 v130 v131 v132 -v133 -v134 v135 v136 v137 v138 v139 v140 v141 -v142 -v143 v144 -v147 -v148 -v149 -v150 -v151 v152 v153 v154 v155 -v158 -v159 -v160 -v161 -v162 -v163 -v164 -v165 -v166 -v169 -v170 -v171 -v172 -v173 -v174 -v175 -v176 -v177 -v180 -v181 -v182 v183 v184 -v185 v186 -v187 -v188 -v191 -v192 -v193 -v194 -v195 v196 v197 -v198 -v199 -v202 -v203 -v204 -v205 -v206 -v207 -v208 -v209 -v210 -v213 -v214 -v215 -v216 -v217 -v218 -v219 -v220 -v221 v224 v225 v226 v227 v228 v229 v230 -v231 v232 v235 v236 v237 v238 v239 v240 v241 -v242 v243 v244 v245 v246 v247 v248 v249 v250 v251 v252 v255 v256 v257 v258 v259 v260 v261 v262 -v263 v266 v267 v268 v269 v270 v271 v272 v273 -v274 -v277 -v278 -v279 -v280 -v281 v282 v283 v284 -v285 -v288 -v289 -v290 -v291 -v292 -v293 -v294 -v295 -v296 -v299 -v300 -v301 -v302 -v303 -v304 -v305 -v306 -v307 -v310 -v311 -v312 -v313 -v314 v315 -v316 -v317 -v318 -v321 -v322 -v323 -v324 -v325 v326 v327 -v328 v329 -v332 -v333 -v334 -v335 -v336 -v337 -v338 -v339 -v340 -v343 -v344 -v345 -v346 -v347 -v348 -v349 -v350 -v351 -v354 -v355 -v356 -v357 -v358 v359 v360 v361 v362 -v365 -v366 -v367 -v368 -v369 -v370 -v371 -v372 -v373 -v376 -v377 -v378 -v379 -v380 -v381 -v382 -v383 -v384 -v387 -v388 -v389 v390 v391 v392 v393 -v394 -v395 -v398 -v399 -v400 -v401 -v402 v403 v404 -v405 -v406 -v409 -v410 -v411 -v412 -v413 -v414 -v415 -v416 -v417 -v420 -v421 -v422 -v423 -v424 -v425 -v426 -v427 -v428 -v433 -v434 -v435 -v436 -v437 -v438 -v439 -v440 -v441 -v442 -v443 -v444 -v445 -v446 -v447 -v448 -v449 -v450 v453 v454 v455 v456 v457 v458 v459 v460 v461 v464 v465 v466 v467 v468 v469 v470 v471 -v472 v481 v482 v483 v484 v485 v486 v487 v488 v489 -v492 -v493 -v494 -v495 -v496 v497 v498 v499 -v500 -v503 -v504 -v505 -v506 -v507 -v508 -v509 -v510 -v511 -v514 -v515 -v516 -v517 -v518 -v519 -v520 -v521 -v522 -v527 -v528 -v529 -v530 -v531 -v532 -v533 -v534 v535 v540 v541 v542 v543 v544 v545 v546 v547 -v548 v551 v552 v553 v554 v555 v556 -v557 -v558 v559 v574 v575 v576 v577 v578 v579 -v580 -v581 v582 -v585 -v586 -v587 -v588 -v589 v590 -v591 -v592 -v593 -v596 -v597 -v598 -v599 -v600 v601 v602 -v603 v604 -v607 -v608 -v609 -v610 -v611 -v612 -v613 -v614 -v615 -v618 -v619 -v620 -v621 -v622 -v623 -v624 -v625 -v626 -v629 -v630 -v631 -v632 -v633 -v634 -v635 -v636 -v637 -v640 -v641 -v642 -v643 -v644 -v645 -v646 -v647 -v648 -v651 -v652 -v653 -v654 -v655 -v656 -v657 -v658 -v659 -v662 -v663 -v664 -v665 -v666 -v667 -v668 -v669 -v670 -v673 -v674 -v675 -v676 -v677 -v678 -v679 -v680 -v681 -v682 -v683 -v684 -v685 -v686 -v687 -v688 -v689 -v690 v693 v694 v695 v696 v697 v698 v699 v700 v701 v702 v703 v704 v705 v706 v707 v708 v709 v710 -v713 -v714 -v715 -v716 -v717 -v718 -v719 -v720 -v721 -v724 -v725 -v726 -v727 -v728 -v729 -v730 -v731 -v732 -v735 -v736 -v737 -v738 -v739 -v740 -v741 -v742 -v743 v748 v749 v750 v751 v752 v753 v754 v755 v756 -v765 -v766 -v767 -v768 -v769 -v770 -v771 -v772 -v773 -v774 -v775 -v776 -v777 -v778 -v779 -v780 -v781 v782 -v785 -v786 -v787 -v788 -v789 -v790 -v791 -v792 v793 -v800 -v801 -v802 -v803 -v804 -v805 -v806 -v807 -v808 -v809 -v810 -v811 -v812 -v813 -v814 -v815 -v816 v817 v822 v823 v824 v825 v826 v827 v828 v829 v830 v833 v834 v835 v836 v837 v838 v839 v840 v841 -v844 -v845 -v846 -v847 -v848 -v849 -v850 -v851 -v852 -v855 -v856 -v857 -v858 -v859 -v860 -v861 -v862 -v863 -v868 v869 -v870 -v871 -v872 -v873 -v874 -v875 -v876 v879 v880 v881 v882 v883 v884 v885 v886 v887 -v890 -v891 -v892 -v893 -v894 -v895 -v896 -v897 -v898 -v899 -v900 -v901 -v902 -v903 -v904 -v905 -v906 -v907 -v912 -v913 -v914 -v915 -v916 -v917 -v918 -v919 -v920 -v923 -v924 -v925 -v926 -v927 -v928 -v929 -v930 -v931 -v932 -v933 -v934 -v935 -v936 -v937 -v938 -v939 -v940 -v945 -v946 -v947 -v948 -v949 -v950 -v951 -v952 -v953 -v956 -v957 -v958 -v959 -v960 -v961 -v962 -v963 -v964 -v967 -v968 -v969 -v970 -v971 -v972 -v973 -v974 -v975 -v980 -v981 -v982 -v983 -v984 -v985 -v986 -v987 -v988 -v991 -v992 -v993 -v994 -v995 -v996 -v997 -v998 -v999 -v1004 -v1005 -v1006 -v1007 -v1008 -v1009 -v1010 -v1011 -v1012 -v1015 -v1016 -v1017 -v1018 -v1019 -v1020 -v1021 -v1022 -v1023 -v1026 -v1027 -v1028 -v1029 -v1030 -v1031 -v1032 -v1033 -v1034 -v1035 -v1036 -v1037 -v1038 -v1039 -v1040 -v1041 -v1042 -v1043 -v1048 -v1049 -v1050 -v1051 -v1052 -v1053 -v1054 -v1055 -v1056 v1059 v1060 v1061 v1062 v1063 v1064 v1065 -v1066 v1067 v1076 v1077 v1078 v1079 v1080 v1081 v1082 v1083 v1084 v1087 v1088 v1089 v1090 v1091 v1092 -v1093 -v1094 v1095 v1116 v1117 v1118 v1119 v1120 v1121 -v1122 -v1123 v1124 -v1127 -v1128 -v1129 -v1130 -v1131 -v1132 -v1133 -v1134 -v1135 -v1140 -v1141 -v1142 -v1143 -v1144 -v1145 -v1146 -v1147 -v1148 -v1151 -v1152 -v1153 -v1154 -v1155 -v1156 -v1157 -v1158 -v1159 -v1162 -v1163 -v1164 -v1165 -v1166 -v1167 -v1168 -v1169 -v1170 -v1171 -v1172 -v1173 -v1174 -v1175 -v1176 -v1177 -v1178 -v1179 -v1184 -v1185 -v1186 -v1187 -v1188 -v1189 -v1190 -v1191 -v1192 -v1197 -v1198 -v1199 -v1200 -v1201 -v1202 -v1203 -v1204 v1205 -v1208 v1209 v1210 v1211 v1212 v1213 v1214 -v1215 -v1216 v1219 v1220 v1221 v1222 v1223 v1224 -v1225 -v1226 v1227 v1254 v1255 v1256 v1257 v1258 v1259 -v1260 -v1261 v1262 -v1265 -v1266 -v1267 -v1268 -v1269 -v1270 -v1271 -v1272 -v1273 -v1278 -v1279 -v1280 -v1281 -v1282 -v1283 -v1284 -v1285 -v1286 -v1289 -v1290 -v1291 -v1292 -v1293 -v1294 -v1295 -v1296 -v1297 -v1300 -v1301 -v1302 -v1303 -v1304 -v1305 -v1306 -v1307 -v1308 -v1313 -v1314 -v1315 -v1316 -v1317 -v1318 -v1319 -v1320 -v1321 v1324 v1325 v1326 v1327 v1328 v1329 v1330 -v1331 v1332 v1343 v1344 v1345 v1346 v1347 v1348 v1349 v1350 -v1351 v1386 v1387 v1388 v1389 v1390 v1391 v1392 v1393 -v1394 -v1397 -v1398 -v1399 -v1400 -v1401 -v1402 -v1403 -v1404 -v1405 -v1410 -v1411 -v1412 -v1413 -v1414 -v1415 -v1416 -v1417 -v1418 -v1421 -v1422 -v1423 -v1424 -v1425 -v1426 -v1427 -v1428 -v1429 
c objectif function=0
#### 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): 1.25 1.06 1.02 2/54 28652
Raw data (stat): 28652 (runsolver) R 28651 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 477687464 1052672 99 4294967295 134512640 135381576 3221224432 3221219680 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 1.52 1.12 1.04 4/64 28662
Raw data (stat): 28652 (java) R 28651 27565 27564 0 -1 0 18080 0 1 0 692 45 0 0 25 0 11 0 477687464 865824768 22217 4294967295 134512640 134569956 3221224400 3221214892 1130914819 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211383 22217 13073 16 0 211367 0
vsize: 845532
[startup+17.9841 s]
Raw data (loadavg): 1.56 1.14 1.04 1/53 28663
Raw data (stat): 28652 (java) R 28651 27565 27564 0 -1 0 18080 0 1 0 692 45 0 0 25 0 11 0 477687464 865824768 22217 4294967295 134512640 134569956 3221224400 3221214892 1130914819 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211383 22217 13073 16 0 211367 0
vsize: 0

Child status: 30
Real time (s): 17.9838
CPU time (s): 26.057
CPU user time (s): 25.3581
CPU system time (s): 0.698893
CPU usage (%): 144.892
Max. virtual memory (Kb): 845532
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	FAILED
ERROR: unsatisfied constraint on line 541
#### END VERIFIER DATA ####