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/mps-v2-13-7/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-nug08.opb
MD5SUM	d34a8d0bd0d9ecfef5752930c6cb50a0
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	107
Optimality of the best value was proved	NO
Number of terms in the objective function	13104
Biggest coefficient in the objective function	163840
Number of bits for the biggest coefficient in the objective function	18
Sum of the numbers in the objective function	70639184
Number of bits of the sum of numbers in the objective function	27
Biggest number in a constraint	163840
Number of bits of the biggest number in a constraint	18
Biggest sum of numbers in a constraint	70639184
Number of bits of the biggest sum of numbers	27
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	683.845
Number of variables	21216
Total number of constraints	912
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	912
Minimum length of a constraint	104
Maximum length of a constraint	104
Trace number 31310

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc21 THE 2005-05-26 00:01:21 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22706 boxname=wulflinc21 idbench=1522 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  d34a8d0bd0d9ecfef5752930c6cb50a0  /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-nug08.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-nug08.opb
IDLAUNCH: 22706
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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	: 3
cpu MHz		: 451.161
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:        870856 kB
Buffers:         22608 kB
Cached:         120176 kB
SwapCached:        968 kB
Active:          20300 kB
Inactive:       124636 kB
HighTotal:      131008 kB
HighFree:        36372 kB
LowTotal:       903652 kB
LowFree:        834484 kB
SwapTotal:     2097892 kB
SwapFree:      2096008 kB
Dirty:              48 kB
Writeback:           0 kB
Mapped:           5112 kB
Slab:            13256 kB
Committed_AS:    63900 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-26 00:21:51 (client local time) WITH STATUS 152 IN 1229.87 SECONDS
stats: 22706 7 1229.87 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1824 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[1822]---> BDD-cost:   13
c ---[1820]---> BDD-cost:   13
c ---[1818]---> BDD-cost:   13
c ---[1816]---> BDD-cost:   13
c ---[1814]---> BDD-cost:   13
c ---[1812]---> BDD-cost:   13
c ---[1810]---> BDD-cost:   13
c ---[1808]---> BDD-cost:   13
c ---[1806]---> BDD-cost:   13
c ---[1804]---> BDD-cost:   13
c ---[1802]---> BDD-cost:   13
c ---[1800]---> BDD-cost:   13
c ---[1798]---> BDD-cost:   13
c ---[1796]---> BDD-cost:   13
c ---[1794]---> BDD-cost:   13
c ---[1792]---> BDD-cost:   13
c ---[1790]---> BDD-cost:   13
c ---[1788]---> BDD-cost:   13
c ---[1786]---> BDD-cost:   13
c ---[1784]---> BDD-cost:   13
c ---[1782]---> BDD-cost:   13
c ---[1780]---> BDD-cost:   13
c ---[1778]---> BDD-cost:   13
c ---[1776]---> BDD-cost:   13
c ---[1774]---> BDD-cost:   13
c ---[1772]---> BDD-cost:   13
c ---[1770]---> BDD-cost:   13
c ---[1768]---> BDD-cost:   13
c ---[1766]---> BDD-cost:   13
c ---[1764]---> BDD-cost:   13
c ---[1762]---> BDD-cost:   13
c ---[1760]---> BDD-cost:   13
c ---[1758]---> BDD-cost:   13
c ---[1756]---> BDD-cost:   13
c ---[1754]---> BDD-cost:   13
c ---[1752]---> BDD-cost:   13
c ---[1750]---> BDD-cost:   13
c ---[1748]---> BDD-cost:   13
c ---[1746]---> BDD-cost:   13
c ---[1744]---> BDD-cost:   13
c ---[1742]---> BDD-cost:   13
c ---[1740]---> BDD-cost:   13
c ---[1738]---> BDD-cost:   13
c ---[1736]---> BDD-cost:   13
c ---[1734]---> BDD-cost:   13
c ---[1732]---> BDD-cost:   13
c ---[1730]---> BDD-cost:   13
c ---[1728]---> BDD-cost:   13
c ---[1726]---> BDD-cost:   13
c ---[1724]---> BDD-cost:   13
c ---[1722]---> BDD-cost:   13
c ---[1720]---> BDD-cost:   13
c ---[1718]---> BDD-cost:   13
c ---[1716]---> BDD-cost:   13
c ---[1714]---> BDD-cost:   13
c ---[1712]---> BDD-cost:   13
c ---[1710]---> BDD-cost:   13
c ---[1708]---> BDD-cost:   13
c ---[1706]---> BDD-cost:   13
c ---[1704]---> BDD-cost:   13
c ---[1702]---> BDD-cost:   13
c ---[1700]---> BDD-cost:   13
c ---[1698]---> BDD-cost:   13
c ---[1696]---> BDD-cost:   13
c ---[1694]---> BDD-cost:   13
c ---[1692]---> BDD-cost:   13
c ---[1690]---> BDD-cost:   13
c ---[1688]---> BDD-cost:   13
c ---[1686]---> BDD-cost:   13
c ---[1684]---> BDD-cost:   13
c ---[1682]---> BDD-cost:   13
c ---[1680]---> BDD-cost:   13
c ---[1678]---> BDD-cost:   13
c ---[1676]---> BDD-cost:   13
c ---[1674]---> BDD-cost:   13
c ---[1672]---> BDD-cost:   13
c ---[1670]---> BDD-cost:   13
c ---[1668]---> BDD-cost:   13
c ---[1666]---> BDD-cost:   13
c ---[1664]---> BDD-cost:   13
c ---[1662]---> BDD-cost:   13
c ---[1660]---> BDD-cost:   13
c ---[1658]---> BDD-cost:   13
c ---[1656]---> BDD-cost:   13
c ---[1654]---> BDD-cost:   13
c ---[1652]---> BDD-cost:   13
c ---[1650]---> BDD-cost:   13
c ---[1648]---> BDD-cost:   13
c ---[1646]---> BDD-cost:   13
c ---[1644]---> BDD-cost:   13
c ---[1642]---> BDD-cost:   13
c ---[1640]---> BDD-cost:   13
c ---[1638]---> BDD-cost:   13
c ---[1636]---> BDD-cost:   13
c ---[1634]---> BDD-cost:   13
c ---[1632]---> BDD-cost:   13
c ---[1630]---> BDD-cost:   13
c ---[1628]---> BDD-cost:   13
c ---[1626]---> BDD-cost:   13
c ---[1624]---> BDD-cost:   13
c ---[1622]---> BDD-cost:   13
c ---[1620]---> BDD-cost:   13
c ---[1618]---> BDD-cost:   13
c ---[1616]---> BDD-cost:   13
c ---[1614]---> BDD-cost:   13
c ---[1612]---> BDD-cost:   13
c ---[1610]---> BDD-cost:   13
c ---[1608]---> BDD-cost:   13
c ---[1606]---> BDD-cost:   13
c ---[1604]---> BDD-cost:   13
c ---[1602]---> BDD-cost:   13
c ---[1600]---> BDD-cost:   13
c ---[1598]---> BDD-cost:   13
c ---[1596]---> BDD-cost:   13
c ---[1594]---> BDD-cost:   13
c ---[1592]---> BDD-cost:   13
c ---[1590]---> BDD-cost:   13
c ---[1588]---> BDD-cost:   13
c ---[1586]---> BDD-cost:   13
c ---[1584]---> BDD-cost:   13
c ---[1582]---> BDD-cost:   13
c ---[1580]---> BDD-cost:   13
c ---[1578]---> BDD-cost:   13
c ---[1576]---> BDD-cost:   13
c ---[1574]---> BDD-cost:   13
c ---[1572]---> BDD-cost:   13
c ---[1570]---> BDD-cost:   13
c ---[1568]---> BDD-cost:   13
c ---[1566]---> BDD-cost:   13
c ---[1564]---> BDD-cost:   13
c ---[1562]---> BDD-cost:   13
c ---[1560]---> BDD-cost:   13
c ---[1558]---> BDD-cost:   13
c ---[1556]---> BDD-cost:   13
c ---[1554]---> BDD-cost:   13
c ---[1552]---> BDD-cost:   13
c ---[1550]---> BDD-cost:   13
c ---[1548]---> BDD-cost:   13
c ---[1546]---> BDD-cost:   13
c ---[1544]---> BDD-cost:   13
c ---[1542]---> BDD-cost:   13
c ---[1540]---> BDD-cost:   13
c ---[1538]---> BDD-cost:   13
c ---[1536]---> BDD-cost:   13
c ---[1534]---> BDD-cost:   13
c ---[1532]---> BDD-cost:   13
c ---[1530]---> BDD-cost:   13
c ---[1528]---> BDD-cost:   13
c ---[1526]---> BDD-cost:   13
c ---[1524]---> BDD-cost:   13
c ---[1522]---> BDD-cost:   13
c ---[1520]---> BDD-cost:   13
c ---[1518]---> BDD-cost:   13
c ---[1516]---> BDD-cost:   13
c ---[1514]---> BDD-cost:   13
c ---[1512]---> BDD-cost:   13
c ---[1510]---> BDD-cost:   13
c ---[1508]---> BDD-cost:   13
c ---[1506]---> BDD-cost:   13
c ---[1504]---> BDD-cost:   13
c ---[1502]---> BDD-cost:   13
c ---[1500]---> BDD-cost:   13
c ---[1498]---> BDD-cost:   13
c ---[1496]---> BDD-cost:   13
c ---[1494]---> BDD-cost:   13
c ---[1492]---> BDD-cost:   13
c ---[1490]---> BDD-cost:   13
c ---[1488]---> BDD-cost:   13
c ---[1486]---> BDD-cost:   13
c ---[1484]---> BDD-cost:   13
c ---[1482]---> BDD-cost:   13
c ---[1480]---> BDD-cost:   13
c ---[1478]---> BDD-cost:   13
c ---[1476]---> BDD-cost:   13
c ---[1474]---> BDD-cost:   13
c ---[1472]---> BDD-cost:   13
c ---[1470]---> BDD-cost:   13
c ---[1468]---> BDD-cost:   13
c ---[1466]---> BDD-cost:   13
c ---[1464]---> BDD-cost:   13
c ---[1462]---> BDD-cost:   13
c ---[1460]---> BDD-cost:   13
c ---[1458]---> BDD-cost:   13
c ---[1456]---> BDD-cost:   13
c ---[1454]---> BDD-cost:   13
c ---[1452]---> BDD-cost:   13
c ---[1450]---> BDD-cost:   13
c ---[1448]---> BDD-cost:   13
c ---[1446]---> BDD-cost:   13
c ---[1444]---> BDD-cost:   13
c ---[1442]---> BDD-cost:   13
c ---[1440]---> BDD-cost:   13
c ---[1438]---> BDD-cost:   13
c ---[1436]---> BDD-cost:   13
c ---[1434]---> BDD-cost:   13
c ---[1432]---> BDD-cost:   13
c ---[1430]---> BDD-cost:   13
c ---[1428]---> BDD-cost:   13
c ---[1426]---> BDD-cost:   13
c ---[1424]---> BDD-cost:   13
c ---[1422]---> BDD-cost:   13
c ---[1420]---> BDD-cost:   13
c ---[1418]---> BDD-cost:   13
c ---[1416]---> BDD-cost:   13
c ---[1414]---> BDD-cost:   13
c ---[1412]---> BDD-cost:   13
c ---[1410]---> BDD-cost:   13
c ---[1408]---> BDD-cost:   13
c ---[1406]---> BDD-cost:   13
c ---[1404]---> BDD-cost:   13
c ---[1402]---> BDD-cost:   13
c ---[1400]---> BDD-cost:   13
c ---[1398]---> BDD-cost:   13
c ---[1396]---> BDD-cost:   13
c ---[1394]---> BDD-cost:   13
c ---[1392]---> BDD-cost:   13
c ---[1390]---> BDD-cost:   13
c ---[1388]---> BDD-cost:   13
c ---[1386]---> BDD-cost:   13
c ---[1384]---> BDD-cost:   13
c ---[1382]---> BDD-cost:   13
c ---[1380]---> BDD-cost:   13
c ---[1378]---> BDD-cost:   13
c ---[1376]---> BDD-cost:   13
c ---[1374]---> BDD-cost:   13
c ---[1372]---> BDD-cost:   13
c ---[1370]---> BDD-cost:   13
c ---[1368]---> BDD-cost:   13
c ---[1366]---> BDD-cost:   13
c ---[1364]---> BDD-cost:   13
c ---[1362]---> BDD-cost:   13
c ---[1360]---> BDD-cost:   13
c ---[1358]---> BDD-cost:   13
c ---[1356]---> BDD-cost:   13
c ---[1354]---> BDD-cost:   13
c ---[1352]---> BDD-cost:   13
c ---[1350]---> BDD-cost:   13
c ---[1348]---> BDD-cost:   13
c ---[1346]---> BDD-cost:   13
c ---[1344]---> BDD-cost:   13
c ---[1342]---> BDD-cost:   13
c ---[1340]---> BDD-cost:   13
c ---[1338]---> BDD-cost:   13
c ---[1336]---> BDD-cost:   13
c ---[1334]---> BDD-cost:   13
c ---[1332]---> BDD-cost:   13
c ---[1330]---> BDD-cost:   13
c ---[1328]---> BDD-cost:   13
c ---[1326]---> BDD-cost:   13
c ---[1324]---> BDD-cost:   13
c ---[1322]---> BDD-cost:   13
c ---[1320]---> BDD-cost:   13
c ---[1318]---> BDD-cost:   13
c ---[1316]---> BDD-cost:   13
c ---[1314]---> BDD-cost:   13
c ---[1312]---> BDD-cost:   13
c ---[1310]---> BDD-cost:   13
c ---[1308]---> BDD-cost:   13
c ---[1306]---> BDD-cost:   13
c ---[1304]---> BDD-cost:   13
c ---[1302]---> BDD-cost:   13
c ---[1300]---> BDD-cost:   13
c ---[1298]---> BDD-cost:   13
c ---[1296]---> BDD-cost:   13
c ---[1294]---> BDD-cost:   13
c ---[1292]---> BDD-cost:   13
c ---[1290]---> BDD-cost:   13
c ---[1288]---> BDD-cost:   13
c ---[1286]---> BDD-cost:   13
c ---[1284]---> BDD-cost:   13
c ---[1282]---> BDD-cost:   13
c ---[1280]---> BDD-cost:   13
c ---[1278]---> BDD-cost:   13
c ---[1276]---> BDD-cost:   13
c ---[1274]---> BDD-cost:   13
c ---[1272]---> BDD-cost:   13
c ---[1270]---> BDD-cost:   13
c ---[1268]---> BDD-cost:   13
c ---[1266]---> BDD-cost:   13
c ---[1264]---> BDD-cost:   13
c ---[1262]---> BDD-cost:   13
c ---[1260]---> BDD-cost:   13
c ---[1258]---> BDD-cost:   13
c ---[1256]---> BDD-cost:   13
c ---[1254]---> BDD-cost:   13
c ---[1252]---> BDD-cost:   13
c ---[1250]---> BDD-cost:   13
c ---[1248]---> BDD-cost:   13
c ---[1246]---> BDD-cost:   13
c ---[1244]---> BDD-cost:   13
c ---[1242]---> BDD-cost:   13
c ---[1240]---> BDD-cost:   13
c ---[1238]---> BDD-cost:   13
c ---[1236]---> BDD-cost:   13
c ---[1234]---> BDD-cost:   13
c ---[1232]---> BDD-cost:   13
c ---[1230]---> BDD-cost:   13
c ---[1228]---> BDD-cost:   13
c ---[1226]---> BDD-cost:   13
c ---[1224]---> BDD-cost:   13
c ---[1222]---> BDD-cost:   13
c ---[1220]---> BDD-cost:   13
c ---[1218]---> BDD-cost:   13
c ---[1216]---> BDD-cost:   13
c ---[1214]---> BDD-cost:   13
c ---[1212]---> BDD-cost:   13
c ---[1210]---> BDD-cost:   13
c ---[1208]---> BDD-cost:   13
c ---[1206]---> BDD-cost:   13
c ---[1204]---> BDD-cost:   13
c ---[1202]---> BDD-cost:   13
c ---[1200]---> BDD-cost:   13
c ---[1198]---> BDD-cost:   13
c ---[1196]---> BDD-cost:   13
c ---[1194]---> BDD-cost:   13
c ---[1192]---> BDD-cost:   13
c ---[1190]---> BDD-cost:   13
c ---[1188]---> BDD-cost:   13
c ---[1186]---> BDD-cost:   13
c ---[1184]---> BDD-cost:   13
c ---[1182]---> BDD-cost:   13
c ---[1180]---> BDD-cost:   13
c ---[1178]---> BDD-cost:   13
c ---[1176]---> BDD-cost:   13
c ---[1174]---> BDD-cost:   13
c ---[1172]---> BDD-cost:   13
c ---[1170]---> BDD-cost:   13
c ---[1168]---> BDD-cost:   13
c ---[1166]---> BDD-cost:   13
c ---[1164]---> BDD-cost:   13
c ---[1162]---> BDD-cost:   13
c ---[1160]---> BDD-cost:   13
c ---[1158]---> BDD-cost:   13
c ---[1156]---> BDD-cost:   13
c ---[1154]---> BDD-cost:   13
c ---[1152]---> BDD-cost:   13
c ---[1150]---> BDD-cost:   13
c ---[1148]---> BDD-cost:   13
c ---[1146]---> BDD-cost:   13
c ---[1144]---> BDD-cost:   13
c ---[1142]---> BDD-cost:   13
c ---[1140]---> BDD-cost:   13
c ---[1138]---> BDD-cost:   13
c ---[1136]---> BDD-cost:   13
c ---[1134]---> BDD-cost:   13
c ---[1132]---> BDD-cost:   13
c ---[1130]---> BDD-cost:   13
c ---[1128]---> BDD-cost:   13
c ---[1126]---> BDD-cost:   13
c ---[1124]---> BDD-cost:   13
c ---[1122]---> BDD-cost:   13
c ---[1120]---> BDD-cost:   13
c ---[1118]---> BDD-cost:   13
c ---[1116]---> BDD-cost:   13
c ---[1114]---> BDD-cost:   13
c ---[1112]---> BDD-cost:   13
c ---[1110]---> BDD-cost:   13
c ---[1108]---> BDD-cost:   13
c ---[1106]---> BDD-cost:   13
c ---[1104]---> BDD-cost:   13
c ---[1102]---> BDD-cost:   13
c ---[1100]---> BDD-cost:   13
c ---[1098]---> BDD-cost:   13
c ---[1096]---> BDD-cost:   13
c ---[1094]---> BDD-cost:   13
c ---[1092]---> BDD-cost:   13
c ---[1090]---> BDD-cost:   13
c ---[1088]---> BDD-cost:   13
c ---[1086]---> BDD-cost:   13
c ---[1084]---> BDD-cost:   13
c ---[1082]---> BDD-cost:   13
c ---[1080]---> BDD-cost:   13
c ---[1078]---> BDD-cost:   13
c ---[1076]---> BDD-cost:   13
c ---[1074]---> BDD-cost:   13
c ---[1072]---> BDD-cost:   13
c ---[1070]---> BDD-cost:   13
c ---[1068]---> BDD-cost:   13
c ---[1066]---> BDD-cost:   13
c ---[1064]---> BDD-cost:   13
c ---[1062]---> BDD-cost:   13
c ---[1060]---> BDD-cost:   13
c ---[1058]---> BDD-cost:   13
c ---[1056]---> BDD-cost:   13
c ---[1054]---> BDD-cost:   13
c ---[1052]---> BDD-cost:   13
c ---[1050]---> BDD-cost:   13
c ---[1048]---> BDD-cost:   13
c ---[1046]---> BDD-cost:   13
c ---[1044]---> BDD-cost:   13
c ---[1042]---> BDD-cost:   13
c ---[1040]---> BDD-cost:   13
c ---[1038]---> BDD-cost:   13
c ---[1036]---> BDD-cost:   13
c ---[1034]---> BDD-cost:   13
c ---[1032]---> BDD-cost:   13
c ---[1030]---> BDD-cost:   13
c ---[1028]---> BDD-cost:   13
c ---[1026]---> BDD-cost:   13
c ---[1024]---> BDD-cost:   13
c ---[1022]---> BDD-cost:   13
c ---[1020]---> BDD-cost:   13
c ---[1018]---> BDD-cost:   13
c ---[1016]---> BDD-cost:   13
c ---[1014]---> BDD-cost:   13
c ---[1012]---> BDD-cost:   13
c ---[1010]---> BDD-cost:   13
c ---[1008]---> BDD-cost:   13
c ---[1006]---> BDD-cost:   13
c ---[1004]---> BDD-cost:   13
c ---[1002]---> BDD-cost:   13
c ---[1000]---> BDD-cost:   13
c ---[ 998]---> BDD-cost:   13
c ---[ 996]---> BDD-cost:   13
c ---[ 994]---> BDD-cost:   13
c ---[ 992]---> BDD-cost:   13
c ---[ 990]---> BDD-cost:   13
c ---[ 988]---> BDD-cost:   13
c ---[ 986]---> BDD-cost:   13
c ---[ 984]---> BDD-cost:   13
c ---[ 982]---> BDD-cost:   13
c ---[ 980]---> BDD-cost:   13
c ---[ 978]---> BDD-cost:   13
c ---[ 976]---> BDD-cost:   13
c ---[ 974]---> BDD-cost:   13
c ---[ 972]---> BDD-cost:   13
c ---[ 970]---> BDD-cost:   13
c ---[ 968]---> BDD-cost:   13
c ---[ 966]---> BDD-cost:   13
c ---[ 964]---> BDD-cost:   13
c ---[ 962]---> BDD-cost:   13
c ---[ 960]---> BDD-cost:   13
c ---[ 958]---> BDD-cost:   13
c ---[ 956]---> BDD-cost:   13
c ---[ 954]---> BDD-cost:   13
c ---[ 952]---> BDD-cost:   13
c ---[ 950]---> BDD-cost:   13
c ---[ 948]---> BDD-cost:   13
c ---[ 946]---> BDD-cost:   13
c ---[ 944]---> BDD-cost:   13
c ---[ 942]---> BDD-cost:   13
c ---[ 940]---> BDD-cost:   13
c ---[ 938]---> BDD-cost:   13
c ---[ 936]---> BDD-cost:   13
c ---[ 934]---> BDD-cost:   13
c ---[ 932]---> BDD-cost:   13
c ---[ 930]---> BDD-cost:   13
c ---[ 928]---> BDD-cost:   13
c ---[ 926]---> BDD-cost:   13
c ---[ 924]---> BDD-cost:   13
c ---[ 922]---> BDD-cost:   13
c ---[ 920]---> BDD-cost:   13
c ---[ 918]---> BDD-cost:   13
c ---[ 916]---> BDD-cost:   13
c ---[ 914]---> BDD-cost:   13
c ---[ 912]---> BDD-cost:   13
c ---[ 910]---> BDD-cost:   13
c ---[ 908]---> BDD-cost:   13
c ---[ 906]---> BDD-cost:   13
c ---[ 904]---> BDD-cost:   13
c ---[ 902]---> BDD-cost:   13
c ---[ 900]---> BDD-cost:   13
c ---[ 898]---> BDD-cost:   13
c ---[ 896]---> BDD-cost:   13
c ---[ 894]---> BDD-cost:   13
c ---[ 892]---> BDD-cost:   13
c ---[ 890]---> BDD-cost:   13
c ---[ 888]---> BDD-cost:   13
c ---[ 886]---> BDD-cost:   13
c ---[ 884]---> BDD-cost:   13
c ---[ 882]---> BDD-cost:   13
c ---[ 880]---> BDD-cost:   13
c ---[ 878]---> BDD-cost:   13
c ---[ 876]---> BDD-cost:   13
c ---[ 874]---> BDD-cost:   13
c ---[ 872]---> BDD-cost:   13
c ---[ 870]---> BDD-cost:   13
c ---[ 868]---> BDD-cost:   13
c ---[ 866]---> BDD-cost:   13
c ---[ 864]---> BDD-cost:   13
c ---[ 862]---> BDD-cost:   13
c ---[ 860]---> BDD-cost:   13
c ---[ 858]---> BDD-cost:   13
c ---[ 856]---> BDD-cost:   13
c ---[ 854]---> BDD-cost:   13
c ---[ 852]---> BDD-cost:   13
c ---[ 850]---> BDD-cost:   13
c ---[ 848]---> BDD-cost:   13
c ---[ 846]---> BDD-cost:   13
c ---[ 844]---> BDD-cost:   13
c ---[ 842]---> BDD-cost:   13
c ---[ 840]---> BDD-cost:   13
c ---[ 838]---> BDD-cost:   13
c ---[ 836]---> BDD-cost:   13
c ---[ 834]---> BDD-cost:   13
c ---[ 832]---> BDD-cost:   13
c ---[ 830]---> BDD-cost:   13
c ---[ 828]---> BDD-cost:   13
c ---[ 826]---> BDD-cost:   13
c ---[ 824]---> BDD-cost:   13
c ---[ 822]---> BDD-cost:   13
c ---[ 820]---> BDD-cost:   13
c ---[ 818]---> BDD-cost:   13
c ---[ 816]---> BDD-cost:   13
c ---[ 814]---> BDD-cost:   13
c ---[ 812]---> BDD-cost:   13
c ---[ 810]---> BDD-cost:   13
c ---[ 808]---> BDD-cost:   13
c ---[ 806]---> BDD-cost:   13
c ---[ 804]---> BDD-cost:   13
c ---[ 802]---> BDD-cost:   13
c ---[ 800]---> BDD-cost:   13
c ---[ 798]---> BDD-cost:   13
c ---[ 796]---> BDD-cost:   13
c ---[ 794]---> BDD-cost:   13
c ---[ 792]---> BDD-cost:   13
c ---[ 790]---> BDD-cost:   13
c ---[ 788]---> BDD-cost:   13
c ---[ 786]---> BDD-cost:   13
c ---[ 784]---> BDD-cost:   13
c ---[ 782]---> BDD-cost:   13
c ---[ 780]---> BDD-cost:   13
c ---[ 778]---> BDD-cost:   13
c ---[ 776]---> BDD-cost:   13
c ---[ 774]---> BDD-cost:   13
c ---[ 772]---> BDD-cost:   13
c ---[ 770]---> BDD-cost:   13
c ---[ 768]---> BDD-cost:   13
c ---[ 766]---> BDD-cost:   13
c ---[ 764]---> BDD-cost:   13
c ---[ 762]---> BDD-cost:   13
c ---[ 760]---> BDD-cost:   13
c ---[ 758]---> BDD-cost:   13
c ---[ 756]---> BDD-cost:   13
c ---[ 754]---> BDD-cost:   13
c ---[ 752]---> BDD-cost:   13
c ---[ 750]---> BDD-cost:   13
c ---[ 748]---> BDD-cost:   13
c ---[ 746]---> BDD-cost:   13
c ---[ 744]---> BDD-cost:   13
c ---[ 742]---> BDD-cost:   13
c ---[ 740]---> BDD-cost:   13
c ---[ 738]---> BDD-cost:   13
c ---[ 736]---> BDD-cost:   13
c ---[ 734]---> BDD-cost:   13
c ---[ 732]---> BDD-cost:   13
c ---[ 730]---> BDD-cost:   13
c ---[ 728]---> BDD-cost:   13
c ---[ 726]---> BDD-cost:   13
c ---[ 724]---> BDD-cost:   13
c ---[ 722]---> BDD-cost:   13
c ---[ 720]---> BDD-cost:   13
c ---[ 718]---> BDD-cost:   13
c ---[ 716]---> BDD-cost:   13
c ---[ 714]---> BDD-cost:   13
c ---[ 712]---> BDD-cost:   13
c ---[ 710]---> BDD-cost:   13
c ---[ 708]---> BDD-cost:   13
c ---[ 706]---> BDD-cost:   13
c ---[ 704]---> BDD-cost:   13
c ---[ 702]---> BDD-cost:   13
c ---[ 700]---> BDD-cost:   13
c ---[ 698]---> BDD-cost:   13
c ---[ 696]---> BDD-cost:   13
c ---[ 694]---> BDD-cost:   13
c ---[ 692]---> BDD-cost:   13
c ---[ 690]---> BDD-cost:   13
c ---[ 688]---> BDD-cost:   13
c ---[ 686]---> BDD-cost:   13
c ---[ 684]---> BDD-cost:   13
c ---[ 682]---> BDD-cost:   13
c ---[ 680]---> BDD-cost:   13
c ---[ 678]---> BDD-cost:   13
c ---[ 676]---> BDD-cost:   13
c ---[ 674]---> BDD-cost:   13
c ---[ 672]---> BDD-cost:   13
c ---[ 670]---> BDD-cost:   13
c ---[ 668]---> BDD-cost:   13
c ---[ 666]---> BDD-cost:   13
c ---[ 664]---> BDD-cost:   13
c ---[ 662]---> BDD-cost:   13
c ---[ 660]---> BDD-cost:   13
c ---[ 658]---> BDD-cost:   13
c ---[ 656]---> BDD-cost:   13
c ---[ 654]---> BDD-cost:   13
c ---[ 652]---> BDD-cost:   13
c ---[ 650]---> BDD-cost:   13
c ---[ 648]---> BDD-cost:   13
c ---[ 646]---> BDD-cost:   13
c ---[ 644]---> BDD-cost:   13
c ---[ 642]---> BDD-cost:   13
c ---[ 640]---> BDD-cost:   13
c ---[ 638]---> BDD-cost:   13
c ---[ 636]---> BDD-cost:   13
c ---[ 634]---> BDD-cost:   13
c ---[ 632]---> BDD-cost:   13
c ---[ 630]---> BDD-cost:   13
c ---[ 628]---> BDD-cost:   13
c ---[ 626]---> BDD-cost:   13
c ---[ 624]---> BDD-cost:   13
c ---[ 622]---> BDD-cost:   13
c ---[ 620]---> BDD-cost:   13
c ---[ 618]---> BDD-cost:   13
c ---[ 616]---> BDD-cost:   13
c ---[ 614]---> BDD-cost:   13
c ---[ 612]---> BDD-cost:   13
c ---[ 610]---> BDD-cost:   13
c ---[ 608]---> BDD-cost:   13
c ---[ 606]---> BDD-cost:   13
c ---[ 604]---> BDD-cost:   13
c ---[ 602]---> BDD-cost:   13
c ---[ 600]---> BDD-cost:   13
c ---[ 598]---> BDD-cost:   13
c ---[ 596]---> BDD-cost:   13
c ---[ 594]---> BDD-cost:   13
c ---[ 592]---> BDD-cost:   13
c ---[ 590]---> BDD-cost:   13
c ---[ 588]---> BDD-cost:   13
c ---[ 586]---> BDD-cost:   13
c ---[ 584]---> BDD-cost:   13
c ---[ 582]---> BDD-cost:   13
c ---[ 580]---> BDD-cost:   13
c ---[ 578]---> BDD-cost:   13
c ---[ 576]---> BDD-cost:   13
c ---[ 574]---> BDD-cost:   13
c ---[ 572]---> BDD-cost:   13
c ---[ 570]---> BDD-cost:   13
c ---[ 568]---> BDD-cost:   13
c ---[ 566]---> BDD-cost:   13
c ---[ 564]---> BDD-cost:   13
c ---[ 562]---> BDD-cost:   13
c ---[ 560]---> BDD-cost:   13
c ---[ 558]---> BDD-cost:   13
c ---[ 556]---> BDD-cost:   13
c ---[ 554]---> BDD-cost:   13
c ---[ 552]---> BDD-cost:   13
c ---[ 550]---> BDD-cost:   13
c ---[ 548]---> BDD-cost:   13
c ---[ 546]---> BDD-cost:   13
c ---[ 544]---> BDD-cost:   13
c ---[ 542]---> BDD-cost:   13
c ---[ 540]---> BDD-cost:   13
c ---[ 538]---> BDD-cost:   13
c ---[ 536]---> BDD-cost:   13
c ---[ 534]---> BDD-cost:   13
c ---[ 532]---> BDD-cost:   13
c ---[ 530]---> BDD-cost:   13
c ---[ 528]---> BDD-cost:   13
c ---[ 526]---> BDD-cost:   13
c ---[ 524]---> BDD-cost:   13
c ---[ 522]---> BDD-cost:   13
c ---[ 520]---> BDD-cost:   13
c ---[ 518]---> BDD-cost:   13
c ---[ 516]---> BDD-cost:   13
c ---[ 514]---> BDD-cost:   13
c ---[ 512]---> BDD-cost:   13
c ---[ 510]---> BDD-cost:   13
c ---[ 508]---> BDD-cost:   13
c ---[ 506]---> BDD-cost:   13
c ---[ 504]---> BDD-cost:   13
c ---[ 502]---> BDD-cost:   13
c ---[ 500]---> BDD-cost:   13
c ---[ 498]---> BDD-cost:   13
c ---[ 496]---> BDD-cost:   13
c ---[ 494]---> BDD-cost:   13
c ---[ 492]---> BDD-cost:   13
c ---[ 490]---> BDD-cost:   13
c ---[ 488]---> BDD-cost:   13
c ---[ 486]---> BDD-cost:   13
c ---[ 484]---> BDD-cost:   13
c ---[ 482]---> BDD-cost:   13
c ---[ 480]---> BDD-cost:   13
c ---[ 478]---> BDD-cost:   13
c ---[ 476]---> BDD-cost:   13
c ---[ 474]---> BDD-cost:   13
c ---[ 472]---> BDD-cost:   13
c ---[ 470]---> BDD-cost:   13
c ---[ 468]---> BDD-cost:   13
c ---[ 466]---> BDD-cost:   13
c ---[ 464]---> BDD-cost:   13
c ---[ 462]---> BDD-cost:   13
c ---[ 460]---> BDD-cost:   13
c ---[ 458]---> BDD-cost:   13
c ---[ 456]---> BDD-cost:   13
c ---[ 454]---> BDD-cost:   13
c ---[ 452]---> BDD-cost:   13
c ---[ 450]---> BDD-cost:   13
c ---[ 448]---> BDD-cost:   13
c ---[ 446]---> BDD-cost:   13
c ---[ 444]---> BDD-cost:   13
c ---[ 442]---> BDD-cost:   13
c ---[ 440]---> BDD-cost:   13
c ---[ 438]---> BDD-cost:   13
c ---[ 436]---> BDD-cost:   13
c ---[ 434]---> BDD-cost:   13
c ---[ 432]---> BDD-cost:   13
c ---[ 430]---> BDD-cost:   13
c ---[ 428]---> BDD-cost:   13
c ---[ 426]---> BDD-cost:   13
c ---[ 424]---> BDD-cost:   13
c ---[ 422]---> BDD-cost:   13
c ---[ 420]---> BDD-cost:   13
c ---[ 418]---> BDD-cost:   13
c ---[ 416]---> BDD-cost:   13
c ---[ 414]---> BDD-cost:   13
c ---[ 412]---> BDD-cost:   13
c ---[ 410]---> BDD-cost:   13
c ---[ 408]---> BDD-cost:   13
c ---[ 406]---> BDD-cost:   13
c ---[ 404]---> BDD-cost:   13
c ---[ 402]---> BDD-cost:   13
c ---[ 400]---> BDD-cost:   13
c ---[ 398]---> BDD-cost:   13
c ---[ 396]---> BDD-cost:   13
c ---[ 394]---> BDD-cost:   13
c ---[ 392]---> BDD-cost:   13
c ---[ 390]---> BDD-cost:   13
c ---[ 388]---> BDD-cost:   13
c ---[ 386]---> BDD-cost:   13
c ---[ 384]---> BDD-cost:   13
c ---[ 382]---> BDD-cost:   13
c ---[ 380]---> BDD-cost:   13
c ---[ 378]---> BDD-cost:   13
c ---[ 376]---> BDD-cost:   13
c ---[ 374]---> BDD-cost:   13
c ---[ 372]---> BDD-cost:   13
c ---[ 370]---> BDD-cost:   13
c ---[ 368]---> BDD-cost:   13
c ---[ 366]---> BDD-cost:   13
c ---[ 364]---> BDD-cost:   13
c ---[ 362]---> BDD-cost:   13
c ---[ 360]---> BDD-cost:   13
c ---[ 358]---> BDD-cost:   13
c ---[ 356]---> BDD-cost:   13
c ---[ 354]---> BDD-cost:   13
c ---[ 352]---> BDD-cost:   13
c ---[ 350]---> BDD-cost:   13
c ---[ 348]---> BDD-cost:   13
c ---[ 346]---> BDD-cost:   13
c ---[ 344]---> BDD-cost:   13
c ---[ 342]---> BDD-cost:   13
c ---[ 340]---> BDD-cost:   13
c ---[ 338]---> BDD-cost:   13
c ---[ 336]---> BDD-cost:   13
c ---[ 334]---> BDD-cost:   13
c ---[ 332]---> BDD-cost:   13
c ---[ 330]---> BDD-cost:   13
c ---[ 328]---> BDD-cost:   13
c ---[ 326]---> BDD-cost:   13
c ---[ 324]---> BDD-cost:   13
c ---[ 322]---> BDD-cost:   13
c ---[ 320]---> BDD-cost:   13
c ---[ 318]---> BDD-cost:   13
c ---[ 316]---> BDD-cost:   13
c ---[ 314]---> BDD-cost:   13
c ---[ 312]---> BDD-cost:   13
c ---[ 310]---> BDD-cost:   13
c ---[ 308]---> BDD-cost:   13
c ---[ 306]---> BDD-cost:   13
c ---[ 304]---> BDD-cost:   13
c ---[ 302]---> BDD-cost:   13
c ---[ 300]---> BDD-cost:   13
c ---[ 298]---> BDD-cost:   13
c ---[ 296]---> BDD-cost:   13
c ---[ 294]---> BDD-cost:   13
c ---[ 292]---> BDD-cost:   13
c ---[ 290]---> BDD-cost:   13
c ---[ 288]---> BDD-cost:   13
c ---[ 286]---> BDD-cost:   13
c ---[ 284]---> BDD-cost:   13
c ---[ 282]---> BDD-cost:   13
c ---[ 280]---> BDD-cost:   13
c ---[ 278]---> BDD-cost:   13
c ---[ 276]---> BDD-cost:   13
c ---[ 274]---> BDD-cost:   13
c ---[ 272]---> BDD-cost:   13
c ---[ 270]---> BDD-cost:   13
c ---[ 268]---> BDD-cost:   13
c ---[ 266]---> BDD-cost:   13
c ---[ 264]---> BDD-cost:   13
c ---[ 262]---> BDD-cost:   13
c ---[ 260]---> BDD-cost:   13
c ---[ 258]---> BDD-cost:   13
c ---[ 256]---> BDD-cost:   13
c ---[ 254]---> BDD-cost:   13
c ---[ 252]---> BDD-cost:   13
c ---[ 250]---> BDD-cost:   13
c ---[ 248]---> BDD-cost:   13
c ---[ 246]---> BDD-cost:   13
c ---[ 244]---> BDD-cost:   13
c ---[ 242]---> BDD-cost:   13
c ---[ 240]---> BDD-cost:   13
c ---[ 238]---> BDD-cost:   13
c ---[ 236]---> BDD-cost:   13
c ---[ 234]---> BDD-cost:   13
c ---[ 232]---> BDD-cost:   13
c ---[ 230]---> BDD-cost:   13
c ---[ 228]---> BDD-cost:   13
c ---[ 226]---> BDD-cost:   13
c ---[ 224]---> BDD-cost:   13
c ---[ 222]---> BDD-cost:   13
c ---[ 220]---> BDD-cost:   13
c ---[ 218]---> BDD-cost:   13
c ---[ 216]---> BDD-cost:   13
c ---[ 214]---> BDD-cost:   13
c ---[ 212]---> BDD-cost:   13
c ---[ 210]---> BDD-cost:   13
c ---[ 208]---> BDD-cost:   13
c ---[ 206]---> BDD-cost:   13
c ---[ 204]---> BDD-cost:   13
c ---[ 202]---> BDD-cost:   13
c ---[ 200]---> BDD-cost:   13
c ---[ 198]---> BDD-cost:   13
c ---[ 196]---> BDD-cost:   13
c ---[ 194]---> BDD-cost:   13
c ---[ 192]---> BDD-cost:   13
c ---[ 190]---> BDD-cost:   13
c ---[ 188]---> BDD-cost:   13
c ---[ 186]---> BDD-cost:   13
c ---[ 184]---> BDD-cost:   13
c ---[ 182]---> BDD-cost:   13
c ---[ 180]---> BDD-cost:   13
c ---[ 178]---> BDD-cost:   13
c ---[ 176]---> BDD-cost:   13
c ---[ 174]---> BDD-cost:   13
c ---[ 172]---> BDD-cost:   13
c ---[ 170]---> BDD-cost:   13
c ---[ 168]---> BDD-cost:   13
c ---[ 166]---> BDD-cost:   13
c ---[ 164]---> BDD-cost:   13
c ---[ 162]---> BDD-cost:   13
c ---[ 160]---> BDD-cost:   13
c ---[ 158]---> BDD-cost:   13
c ---[ 156]---> BDD-cost:   13
c ---[ 154]---> BDD-cost:   13
c ---[ 152]---> BDD-cost:   13
c ---[ 150]---> BDD-cost:   13
c ---[ 148]---> BDD-cost:   13
c ---[ 146]---> BDD-cost:   13
c ---[ 144]---> BDD-cost:   13
c ---[ 142]---> BDD-cost:   13
c ---[ 140]---> BDD-cost:   13
c ---[ 138]---> BDD-cost:   13
c ---[ 136]---> BDD-cost:   13
c ---[ 134]---> BDD-cost:   13
c ---[ 132]---> BDD-cost:   13
c ---[ 130]---> BDD-cost:   13
c ---[ 128]---> BDD-cost:   13
c ---[ 126]---> BDD-cost:   13
c ---[ 124]---> BDD-cost:   13
c ---[ 122]---> BDD-cost:   13
c ---[ 120]---> BDD-cost:   13
c ---[ 118]---> BDD-cost:   13
c ---[ 116]---> BDD-cost:   13
c ---[ 114]---> BDD-cost:   13
c ---[ 112]---> BDD-cost:   13
c ---[ 110]---> BDD-cost:   13
c ---[ 108]---> BDD-cost:   13
c ---[ 106]---> BDD-cost:   13
c ---[ 104]---> BDD-cost:   13
c ---[ 102]---> BDD-cost:   13
c ---[ 100]---> BDD-cost:   13
c ---[  98]---> BDD-cost:   13
c ---[  96]---> BDD-cost:   13
c ---[  94]---> BDD-cost:   13
c ---[  92]---> BDD-cost:   13
c ---[  90]---> BDD-cost:   13
c ---[  88]---> BDD-cost:   13
c ---[  86]---> BDD-cost:   13
c ---[  84]---> BDD-cost:   13
c ---[  82]---> BDD-cost:   13
c ---[  80]---> BDD-cost:   13
c ---[  78]---> BDD-cost:   13
c ---[  76]---> BDD-cost:   13
c ---[  74]---> BDD-cost:   13
c ---[  72]---> BDD-cost:   13
c ---[  70]---> BDD-cost:   13
c ---[  68]---> BDD-cost:   13
c ---[  66]---> BDD-cost:   13
c ---[  64]---> BDD-cost:   13
c ---[  62]---> BDD-cost:   13
c ---[  60]---> BDD-cost:   13
c ---[  58]---> BDD-cost:   13
c ---[  56]---> BDD-cost:   13
c ---[  54]---> BDD-cost:   13
c ---[  52]---> BDD-cost:   13
c ---[  50]---> BDD-cost:   13
c ---[  48]---> BDD-cost:   13
c ---[  46]---> BDD-cost:   13
c ---[  44]---> BDD-cost:   13
c ---[  42]---> BDD-cost:   13
c ---[  40]---> BDD-cost:   13
c ---[  38]---> BDD-cost:   13
c ---[  36]---> BDD-cost:   13
c ---[  34]---> BDD-cost:   13
c ---[  32]---> BDD-cost:   13
c ---[  30]---> BDD-cost:   13
c ---[  28]---> BDD-cost:   13
c ---[  26]---> BDD-cost:   13
c ---[  24]---> BDD-cost:   13
c ---[  22]---> BDD-cost:   13
c ---[  20]---> BDD-cost:   13
c ---[  18]---> BDD-cost:   13
c ---[  16]---> BDD-cost:   13
c ---[  14]---> BDD-cost:   13
c ---[  12]---> BDD-cost:   13
c ---[  10]---> BDD-cost:   13
c ---[   8]---> BDD-cost:   13
c ---[   6]---> BDD-cost:   13
c ---[   4]---> BDD-cost:   13
c ---[   2]---> BDD-cost:   13
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   29184    76608 |    9728       0        0     nan |  0.000 % |
c |       101 |   29184    76608 |   10700     101     2942    29.1 | 61.974 % |
c ==============================================================================
c [1mFound solution: 152[0m
c ---[   0]---> Adder-cost: 3232   maxlim: 8472   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       118 |   51695   156998 |   17231     118     3093    26.2 | 61.974 % |
c ==============================================================================
c [1mFound solution: 150[0m
c ---[   0]---> Adder-cost: 0   maxlim: 8474   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       148 |   51699   157025 |   17233     148    11195    75.6 | 61.974 % |
c ==============================================================================
c [1mFound solution: 144[0m
c ---[   0]---> Adder-cost: 0   maxlim: 8480   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       171 |   51706   157060 |   17235     171    12446    72.8 | 61.974 % |
c |       271 |   51706   157060 |   18958     271    17440    64.4 | 56.492 % |
c ==============================================================================
c [1mFound solution: 140[0m
c ---[   0]---> Adder-cost: 0   maxlim: 8484   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       286 |   51710   157086 |   17236     286    25717    89.9 | 56.492 % |
c ==============================================================================
c [1mFound solution: 129[0m
c ---[   0]---> Adder-cost: 0   maxlim: 8495   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       290 |   51711   157093 |   17237     290    25756    88.8 | 56.492 % |
c |       390 |   51711   157093 |   18960     390    40395   103.6 | 56.496 % |
c |       540 |   51711   157093 |   20856     540    71176   131.8 | 56.496 % |
c ==============================================================================
c [1mFound solution: 128[0m
c ---[   0]---> Adder-cost: 0   maxlim: 8496   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       611 |   51713   157105 |   17237     611    82006   134.2 | 56.496 % |
c |       712 |   51713   157105 |   18960     712    90246   126.8 | 56.495 % |
c |       867 |   51713   157105 |   20856     867   102007   117.7 | 56.495 % |
c ==============================================================================
c [1mFound solution: 124[0m
c ---[   0]---> Adder-cost: 0   maxlim: 8500   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1014 |   51716   157127 |   17238    1014   124489   122.8 | 56.495 % |
c ==============================================================================
c [1mFound solution: 115[0m
c ---[   0]---> Adder-cost: 0   maxlim: 8509   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1055 |   51719   157154 |   17239    1055   132485   125.6 | 56.495 % |
c |      1158 |   51719   157154 |   18962    1158   148750   128.5 | 56.500 % |
c |      1309 |   51719   157154 |   20859    1309   183561   140.2 | 56.500 % |
c |      1534 |   51719   157154 |   22945    1534   222519   145.1 | 56.500 % |
c |      1871 |   51719   157154 |   25239    1871   272603   145.7 | 56.500 % |
c |      2377 |   51719   157154 |   27763    2377   376372   158.3 | 56.500 % |
c |      3136 |   51719   157154 |   30539    3136   476325   151.9 | 56.500 % |
c |      4276 |   51719   157154 |   33593    4276   644814   150.8 | 56.500 % |
c ==============================================================================
c [1mFound solution: 113[0m
c ---[   0]---> Adder-cost: 0   maxlim: 8511   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5208 |   51711   157128 |   17237    5206   795773   152.9 | 56.500 % |
c |      5312 |   51711   157128 |   18960    5310   801595   151.0 | 56.504 % |
c |      5465 |   51711   157128 |   20856    5463   837278   153.3 | 56.504 % |
c |      5692 |   51711   157128 |   22942    5690   864242   151.9 | 56.504 % |
c |      6031 |   51711   157128 |   25236    6029   924267   153.3 | 56.504 % |
c |      6537 |   51702   157097 |   27760    6532   985003   150.8 | 56.507 % |
c |      7297 |   51702   157097 |   30536    7292  1147805   157.4 | 56.507 % |
c |      8436 |   51702   157097 |   33590    8431  1375362   163.1 | 56.507 % |
c |     10148 |   51702   157097 |   36949   10143  1640311   161.7 | 56.507 % |
c |     12712 |   51702   157097 |   40643   12707  2240837   176.3 | 56.507 % |
c |     16559 |   51693   157066 |   44708   16549  2855833   172.6 | 56.510 % |
c ==============================================================================
c [1mFound solution: 111[0m
c ---[   0]---> Adder-cost: 0   maxlim: 8513   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20124 |   51687   157051 |   17229   20109  3270800   162.7 | 56.510 % |
c |     20226 |   51687   157051 |   18951   20211  3288496   162.7 | 56.513 % |
c |     20377 |   51687   157051 |   20847   20362  3295854   161.9 | 56.513 % |
c |     20603 |   51687   157051 |   22931   20588  3335955   162.0 | 56.513 % |
c |     20940 |   51687   157051 |   25224   20925  3381230   161.6 | 56.513 % |
c |     21446 |   51687   157051 |   27747   21431  3462806   161.6 | 56.513 % |
c ==============================================================================
c [1mFound solution: 107[0m
c ---[   0]---> Adder-cost: 0   maxlim: 8517   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21966 |   51690   157072 |   17230   21951  3546704   161.6 | 56.513 % |
c |     22068 |   51690   157072 |   18953   22053  3555588   161.2 | 56.514 % |
c |     22219 |   51690   157072 |   20848   22204  3572112   160.9 | 56.514 % |
c |     22446 |   51690   157072 |   22933   22431  3604999   160.7 | 56.514 % |
c |     22783 |   51690   157072 |   25226   22768  3637289   159.8 | 56.514 % |
c |     23292 |   51690   157072 |   27749   23277  3674357   157.9 | 56.514 % |
c |     24052 |   51690   157072 |   30523   24037  3785341   157.5 | 56.514 % |
c |     25191 |   51690   157072 |   33576   25176  3934804   156.3 | 56.514 % |
c |     26899 |   51681   157041 |   36934   26881  4160951   154.8 | 56.517 % |
c |     29461 |   51681   157041 |   40627   29443  4573450   155.3 | 56.517 % |
c |     33306 |   51657   156959 |   44690   33278  5226446   157.1 | 56.525 % |
c |     39074 |   51615   156815 |   49159   39017  6119729   156.8 | 56.539 % |
c |     47724 |   51574   156670 |   54075   47649  7390049   155.1 | 56.550 % |
c |     60698 |   51529   156515 |   59482   60586  9080672   149.9 | 56.564 % |
c |     80163 |   51142   155162 |   65430   79819 12046611   150.9 | 56.729 % |
c |    109358 |   51046   154830 |   71973   42981  4213360    98.0 | 56.765 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 19357 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### 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.92 0.97 0.95 2/55 19353
Raw data (stat): 19353 (runsolver) R 19352 32363 32362 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 720303799 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 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.0003 s]
Raw data (loadavg): 0.93 0.97 0.95 2/56 19357
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0009 s]
Raw data (loadavg): 0.94 0.97 0.95 2/56 19357
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0006 s]
Raw data (loadavg): 0.95 0.97 0.95 2/56 19357
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0002 s]
Raw data (loadavg): 0.96 0.97 0.95 2/56 19357
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50 s]
Raw data (loadavg): 0.96 0.97 0.95 2/56 19357
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+59.9997 s]
Raw data (loadavg): 0.97 0.97 0.95 2/56 19357
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+69.9994 s]
Raw data (loadavg): 0.97 0.97 0.95 2/56 19357
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+79.9991 s]
Raw data (loadavg): 0.98 0.97 0.95 2/56 19357
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+89.9987 s]
Raw data (loadavg): 0.98 0.97 0.95 2/56 19357
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+99.9985 s]
Raw data (loadavg): 0.98 0.97 0.95 2/56 19357
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+109.999 s]
Raw data (loadavg): 0.98 0.97 0.95 2/56 19357
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+119.999 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19357
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+129.999 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19357
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+139.998 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19357
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+149.998 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19357
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+159.998 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19357
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+169.997 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19357
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+179.997 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19357
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+189.998 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19357
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+199.998 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19357
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+209.998 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19357
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+219.998 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19357
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+229.998 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19357
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+239.997 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19357
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+249.997 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19357
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+259.998 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+269.997 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+279.998 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+289.998 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+299.998 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+309.997 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+319.997 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+329.997 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+339.997 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+349.996 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+359.997 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+369.997 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+379.996 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+389.997 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+399.997 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+409.997 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+419.997 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+429.997 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+439.996 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+449.996 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+459.997 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+469.997 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+479.996 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+489.996 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+499.996 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+509.995 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+519.995 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+529.995 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+539.995 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+549.994 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+559.994 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+569.995 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+579.995 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+589.995 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+599.996 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+609.996 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+619.996 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+629.996 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+639.997 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+649.996 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+659.996 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+669.996 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+679.995 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+689.995 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+699.995 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+709.996 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+719.995 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+729.995 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+739.996 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+749.995 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+759.996 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+769.996 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+779.996 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+789.995 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+799.995 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+809.996 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+819.996 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+829.995 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+839.995 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+849.995 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+859.994 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+869.994 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+879.994 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+889.994 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+899.994 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+909.995 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+919.995 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+929.994 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+939.995 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+949.995 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+959.995 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+969.996 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+979.996 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+989.996 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+999.996 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1049.99 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1089.99 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1099.99 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1109.99 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1119.99 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1129.99 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1139.99 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1149.99 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1159.99 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1169.99 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1179.99 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1189.99 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1199.99 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1209.99 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1219.99 s]
Raw data (loadavg): 0.99 0.97 0.95 2/56 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.72 s]
Raw data (loadavg): 0.99 0.97 0.95 1/54 19359
Raw data (stat): 19353 (minisat+_script) S 19352 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 720303799 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.72
CPU time (s): 1229.87
CPU user time (s): 1229.28
CPU system time (s): 0.58791
CPU usage (%): 100.012
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####