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-20-10/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-nug08.opb
MD5SUM	c527241c4d9537dec2ef265de58c54af
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	20160
Biggest coefficient in the objective function	20971520
Number of bits for the biggest coefficient in the objective function	25
Sum of the numbers in the objective function	9042910800
Number of bits of the sum of numbers in the objective function	34
Biggest number in a constraint	20971520
Number of bits of the biggest number in a constraint	25
Biggest sum of numbers in a constraint	9042910800
Number of bits of the biggest sum of numbers	34
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	922.173
Number of variables	32640
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	160
Maximum length of a constraint	160
Trace number 30924

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc8 THE 2005-05-25 20:52:04 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22321 boxname=wulflinc8 idbench=1137 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  c527241c4d9537dec2ef265de58c54af  /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-20-10-nug08.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-20-10-nug08.opb
IDLAUNCH: 22321
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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:        355044 kB
Buffers:         37540 kB
Cached:         615192 kB
SwapCached:          0 kB
Active:          27960 kB
Inactive:       631724 kB
HighTotal:      131008 kB
HighFree:        15176 kB
LowTotal:       903652 kB
LowFree:        339868 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7068 kB
Slab:            14260 kB
Committed_AS:    63732 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 21:12:35 (client local time) WITH STATUS 152 IN 1229.87 SECONDS
stats: 22321 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 | 71.737 % |
c ==============================================================================
c [1mFound solution: 143[0m
c ---[   0]---> Adder-cost: 3232   maxlim: 8481   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       114 |   51690   156972 |   17230     114     3037    26.6 | 71.737 % |
c ==============================================================================
c [1mFound solution: 125[0m
c ---[   0]---> Adder-cost: 0   maxlim: 8499   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       128 |   51696   157004 |   17232     128     6419    50.1 | 71.737 % |
c ==============================================================================
c [1mFound solution: 117[0m
c ---[   0]---> Adder-cost: 0   maxlim: 8507   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       131 |   51700   157027 |   17233     131     6791    51.8 | 71.737 % |
c |       233 |   51700   157027 |   18956     233    24566   105.4 | 66.906 % |
c |       383 |   51700   157027 |   20851     383    45857   119.7 | 66.906 % |
c |       609 |   51700   157027 |   22937     609    99114   162.7 | 66.906 % |
c |       946 |   51700   157027 |   25230     946   139261   147.2 | 66.906 % |
c |      1455 |   51700   157027 |   27753    1455   258743   177.8 | 66.906 % |
c |      2215 |   51700   157027 |   30529    2215   400099   180.6 | 66.906 % |
c |      3354 |   51700   157027 |   33582    3354   592644   176.7 | 66.906 % |
c |      5064 |   51700   157027 |   36940    5064   811748   160.3 | 66.906 % |
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 |      6126 |   51701   157032 |   17233    6126   989052   161.5 | 66.906 % |
c |      6226 |   51701   157032 |   18956    6226  1014757   163.0 | 66.907 % |
c |      6376 |   51701   157032 |   20851    6376  1044878   163.9 | 66.907 % |
c |      6602 |   51701   157032 |   22937    6602  1093623   165.7 | 66.907 % |
c |      6942 |   51701   157032 |   25230    6942  1135557   163.6 | 66.907 % |
c |      7449 |   51701   157032 |   27753    7449  1210967   162.6 | 66.907 % |
c |      8209 |   51701   157032 |   30529    8209  1287633   156.9 | 66.907 % |
c |      9348 |   51701   157032 |   33582    9348  1445463   154.6 | 66.907 % |
c |     11057 |   51701   157032 |   36940   11057  1625837   147.0 | 66.907 % |
c ==============================================================================
c [1mFound solution: 110[0m
c ---[   0]---> Adder-cost: 0   maxlim: 8514   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13491 |   51710   157073 |   17236   13491  1988804   147.4 | 66.907 % |
c |     13592 |   51710   157073 |   18959   13592  2008712   147.8 | 66.905 % |
c |     13742 |   51710   157073 |   20855   13742  2034564   148.1 | 66.905 % |
c |     13967 |   51710   157073 |   22941   13967  2079073   148.9 | 66.905 % |
c |     14305 |   51710   157073 |   25235   14305  2118928   148.1 | 66.905 % |
c |     14812 |   51710   157073 |   27758   14812  2185488   147.5 | 66.905 % |
c |     15571 |   51710   157073 |   30534   15571  2293448   147.3 | 66.905 % |
c |     16711 |   51710   157073 |   33588   16711  2436209   145.8 | 66.905 % |
c |     18421 |   51701   157042 |   36946   18418  2653018   144.0 | 66.908 % |
c |     20983 |   51692   157011 |   40641   20977  3143493   149.9 | 66.910 % |
c |     24829 |   51656   156887 |   44705   24804  3571326   144.0 | 66.918 % |
c |     30595 |   51602   156701 |   49176   30545  4333084   141.9 | 66.931 % |
c |     39244 |   51512   156391 |   54093   39158  5510331   140.7 | 66.952 % |
c |     52219 |   51449   156174 |   59503   52110  7094364   136.1 | 66.966 % |
c |     71681 |   51303   155662 |   65453   71527  9682874   135.4 | 67.008 % |
c |    100875 |   49658   150460 |   71999   84015 10562496   125.7 | 67.657 % |
c ==============================================================================
c [1mFound solution: 107[0m
c ---[   0]---> Adder-cost: 2430   maxlim: 8005   bits: 13/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    107799 |   66409   210137 |   22136   90928 11339164   124.7 | 67.657 % |
c |    107899 |   66409   210137 |   24349   27617  1662868    60.2 | 64.411 % |
c |    108049 |   66409   210137 |   26784   27767  1682484    60.6 | 64.411 % |
c |    108277 |   66409   210137 |   29463   27995  1712235    61.2 | 64.411 % |
c |    108615 |   66409   210137 |   32409   28333  1745804    61.6 | 64.411 % |
c |    109123 |   66400   210108 |   35650   28840  1810008    62.8 | 64.415 % |
c |    109882 |   66376   210024 |   39215   29596  1907557    64.5 | 64.419 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 22485 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.93 0.97 0.91 2/54 22481
Raw data (stat): 22481 (runsolver) R 22480 3132 3131 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 770115459 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.0138 s]
Raw data (loadavg): 0.94 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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.0349 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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.0349 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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.0363 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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.0367 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+60.0379 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+70.0387 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+80.039 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+90.0395 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+100.04 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+120.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+130.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+140.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+150.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+160.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+170.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+180.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+190.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+200.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+210.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+220.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+230.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+240.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+250.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+260.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+270.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+280.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+290.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+300.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+310.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+320.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+330.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+340.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+350.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+360.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+370.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+380.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+390.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+400.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+410.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+420.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+430.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+440.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+450.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+460.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+470.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 22485
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+480.052 s]
Raw data (loadavg): 1.07 0.99 0.92 2/58 22488
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+490.053 s]
Raw data (loadavg): 1.06 0.99 0.92 2/55 22538
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+500.053 s]
Raw data (loadavg): 1.05 0.99 0.92 2/55 22538
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+510.054 s]
Raw data (loadavg): 1.04 0.99 0.92 2/55 22538
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+520.054 s]
Raw data (loadavg): 1.04 0.99 0.92 2/55 22538
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+530.054 s]
Raw data (loadavg): 1.03 0.99 0.92 2/55 22538
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+540.055 s]
Raw data (loadavg): 1.03 0.99 0.92 2/55 22538
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+550.055 s]
Raw data (loadavg): 1.02 0.99 0.92 2/55 22538
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+560.055 s]
Raw data (loadavg): 1.02 0.99 0.92 2/55 22540
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+570.057 s]
Raw data (loadavg): 1.01 0.99 0.92 2/55 22540
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+580.056 s]
Raw data (loadavg): 1.01 0.99 0.92 2/55 22540
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+590.056 s]
Raw data (loadavg): 1.01 0.99 0.92 2/55 22540
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+600.057 s]
Raw data (loadavg): 1.01 0.99 0.92 2/55 22540
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+610.057 s]
Raw data (loadavg): 1.01 0.99 0.92 2/55 22540
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+620.058 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22540
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+630.058 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22540
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+640.059 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22540
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+650.058 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22540
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+660.058 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22540
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+670.063 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22540
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+680.063 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22540
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+690.064 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22540
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+700.064 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22540
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+710.065 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22540
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+720.065 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22540
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+730.065 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22540
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+740.065 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22540
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+750.066 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22540
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+760.066 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22540
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+770.066 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22540
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+780.067 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22540
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+790.067 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22540
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+800.067 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+810.068 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+820.069 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+830.068 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+840.068 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+850.069 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+860.069 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+870.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+880.069 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+890.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+900.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+910.071 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+920.071 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+930.071 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+940.072 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+950.071 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+960.072 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+970.072 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+980.072 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+990.073 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+1000.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+1050.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+1090.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+1100.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+1110.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+1120.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+1130.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+1140.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+1150.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+1160.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+1170.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+1180.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+1190.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+1200.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+1210.08 s]
Raw data (loadavg): 1.08 1.00 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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+1220.08 s]
Raw data (loadavg): 1.07 1.00 0.92 2/55 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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.85 s]
Raw data (loadavg): 1.06 1.00 0.92 1/53 22542
Raw data (stat): 22481 (minisat+_script) S 22480 3132 3131 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 770115459 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.85
CPU time (s): 1229.87
CPU user time (s): 1228.98
CPU system time (s): 0.882865
CPU usage (%): 100.001
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####