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/MIPLIB/miplib/normalized-mps-v2-13-7-air06.opb
MD5SUM	f85d0079133f298b06c25764b03ff228
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	50233
Optimality of the best value was proved	NO
Number of terms in the objective function	8627
Biggest coefficient in the objective function	1859
Number of bits for the biggest coefficient in the objective function	11
Sum of the numbers in the objective function	4587852
Number of bits of the sum of numbers in the objective function	23
Biggest number in a constraint	1859
Number of bits of the biggest number in a constraint	11
Biggest sum of numbers in a constraint	4587852
Number of bits of the biggest sum of numbers	23
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.81
Number of variables	8627
Total number of constraints	9452
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	9452
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	461
Trace number 15787

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc30 THE 2005-04-21 05:47:30 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16676 boxname=wulflinc30 idbench=1283 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f85d0079133f298b06c25764b03ff228  /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-air06.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-air06.opb /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-air06.opb
IDLAUNCH: 16676
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        666280 kB
Buffers:         23216 kB
Cached:         312976 kB
SwapCached:          0 kB
Active:         148164 kB
Inactive:       190872 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        666028 kB
SwapTotal:     2097892 kB
SwapFree:      2097824 kB
Dirty:               0 kB
Writeback:           0 kB
Mapped:           6800 kB
Slab:            23720 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 06:07:32 (client local time) WITH STATUS 0 IN 1200.36 SECONDS
stats: 16676 7 1200.36 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1628 PB-constraints to clauses...
c   -- Unit propagations: ppp
c   -- Detecting intervals from adjacent constraints: #####################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[1626]---> Adder-cost: 98   maxlim: 52   bits: 6/6
c ---[1622]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[1618]---> Adder-cost: 52   maxlim: 30   bits: 5/5
c ---[1616]---> Adder-cost: 46   maxlim: 34   bits: 6/6
c ---[1614]---> Adder-cost: 86   maxlim: 55   bits: 6/6
c ---[1612]---> Adder-cost: 108   maxlim: 57   bits: 6/6
c ---[1610]---> Adder-cost: 76   maxlim: 40   bits: 6/6
c ---[1608]---> Adder-cost: 26   maxlim: 29   bits: 5/5
c ---[1604]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[1602]---> Adder-cost: 76   maxlim: 55   bits: 6/6
c ---[1600]---> Adder-cost: 142   maxlim: 74   bits: 7/7
c ---[1598]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1596]---> Adder-cost: 34   maxlim: 30   bits: 5/5
c ---[1594]---> Adder-cost: 136   maxlim: 75   bits: 7/7
c ---[1592]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[1590]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[1588]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1586]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1584]---> Adder-cost: 22   maxlim: 17   bits: 5/5
c ---[1582]---> Adder-cost: 70   maxlim: 42   bits: 6/6
c ---[1580]---> Adder-cost: 134   maxlim: 69   bits: 7/7
c ---[1578]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1576]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1574]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1572]---> Adder-cost: 20   maxlim: 16   bits: 5/5
c ---[1570]---> Adder-cost: 124   maxlim: 66   bits: 7/7
c ---[1566]---> Adder-cost: 44   maxlim: 24   bits: 5/5
c ---[1564]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[1562]---> Adder-cost: 30   maxlim: 18   bits: 5/5
c ---[1560]---> Adder-cost: 38   maxlim: 24   bits: 5/5
c ---[1558]---> Adder-cost: 132   maxlim: 67   bits: 7/7
c ---[1556]---> Adder-cost: 294   maxlim: 154   bits: 8/8
c ---[1554]---> Adder-cost: 230   maxlim: 150   bits: 8/8
c ---[1552]---> Adder-cost: 152   maxlim: 90   bits: 7/7
c ---[1550]---> Adder-cost: 110   maxlim: 66   bits: 7/7
c ---[1548]---> Adder-cost: 76   maxlim: 45   bits: 6/6
c ---[1546]---> Adder-cost: 60   maxlim: 48   bits: 6/6
c ---[1544]---> Adder-cost: 54   maxlim: 33   bits: 6/6
c ---[1542]---> Adder-cost: 148   maxlim: 80   bits: 7/7
c ---[1540]---> Adder-cost: 128   maxlim: 65   bits: 7/7
c ---[1538]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[1536]---> Adder-cost: 16   maxlim: 12   bits: 4/4
c ---[1534]---> Adder-cost: 78   maxlim: 43   bits: 6/6
c ---[1532]---> Adder-cost: 62   maxlim: 32   bits: 6/6
c ---[1530]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[1528]---> Adder-cost: 8   maxlim: 6   bits: 3/3
c ---[1526]---> Adder-cost: 12   maxlim: 7   bits: 4/3
c ---[1524]---> Adder-cost: 42   maxlim: 24   bits: 5/5
c ---[1522]---> Adder-cost: 90   maxlim: 47   bits: 6/6
c ---[1520]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1518]---> Adder-cost: 36   maxlim: 24   bits: 5/5
c ---[1516]---> Adder-cost: 254   maxlim: 127   bits: 8/7
c ---[1514]---> Adder-cost: 182   maxlim: 98   bits: 7/7
c ---[1512]---> Adder-cost: 140   maxlim: 106   bits: 7/7
c ---[1510]---> Adder-cost: 172   maxlim: 128   bits: 8/8
c ---[1508]---> Adder-cost: 58   maxlim: 37   bits: 6/6
c ---[1506]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[1504]---> Adder-cost: 348   maxlim: 179   bits: 8/8
c ---[1502]---> Adder-cost: 332   maxlim: 197   bits: 8/8
c ---[1500]---> Adder-cost: 348   maxlim: 181   bits: 8/8
c ---[1498]---> Adder-cost: 192   maxlim: 130   bits: 8/8
c ---[1496]---> Adder-cost: 260   maxlim: 132   bits: 8/8
c ---[1494]---> Adder-cost: 262   maxlim: 149   bits: 8/8
c ---[1492]---> Adder-cost: 66   maxlim: 46   bits: 6/6
c ---[1488]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1486]---> Adder-cost: 16   maxlim: 11   bits: 4/4
c ---[1484]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1478]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1476]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1474]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[1472]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1470]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1468]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1466]---> Adder-cost: 96   maxlim: 52   bits: 6/6
c ---[1464]---> Adder-cost: 196   maxlim: 102   bits: 7/7
c ---[1462]---> Adder-cost: 92   maxlim: 47   bits: 6/6
c ---[1460]---> Adder-cost: 46   maxlim: 26   bits: 5/5
c ---[1458]---> Adder-cost: 20   maxlim: 26   bits: 5/5
c ---[1456]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[1452]---> Adder-cost: 46   maxlim: 28   bits: 5/5
c ---[1450]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[1448]---> Adder-cost: 88   maxlim: 51   bits: 6/6
c ---[1446]---> Adder-cost: 98   maxlim: 53   bits: 6/6
c ---[1444]---> Adder-cost: 98   maxlim: 62   bits: 6/6
c ---[1442]---> Adder-cost: 64   maxlim: 40   bits: 6/6
c ---[1440]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[1438]---> Adder-cost: 30   maxlim: 17   bits: 5/5
c ---[1436]---> Adder-cost: 92   maxlim: 47   bits: 6/6
c ---[1434]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1428]---> Adder-cost: 8   maxlim: 6   bits: 3/3
c ---[1426]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[1424]---> Adder-cost: 28   maxlim: 17   bits: 5/5
c ---[1422]---> Adder-cost: 126   maxlim: 64   bits: 7/7
c ---[1420]---> Adder-cost: 188   maxlim: 98   bits: 7/7
c ---[1418]---> Adder-cost: 168   maxlim: 99   bits: 7/7
c ---[1416]---> Adder-cost: 106   maxlim: 56   bits: 6/6
c ---[1414]---> Adder-cost: 162   maxlim: 88   bits: 7/7
c ---[1412]---> Adder-cost: 170   maxlim: 89   bits: 7/7
c ---[1410]---> Adder-cost: 156   maxlim: 100   bits: 7/7
c ---[1408]---> Adder-cost: 112   maxlim: 80   bits: 7/7
c ---[1406]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[1404]---> Adder-cost: 256   maxlim: 129   bits: 8/8
c ---[1402]---> Adder-cost: 244   maxlim: 147   bits: 8/8
c ---[1400]---> Adder-cost: 164   maxlim: 88   bits: 7/7
c ---[1398]---> Adder-cost: 106   maxlim: 65   bits: 7/7
c ---[1396]---> Adder-cost: 126   maxlim: 64   bits: 7/7
c ---[1394]---> Adder-cost: 36   maxlim: 22   bits: 5/5
c ---[1392]---> Adder-cost: 34   maxlim: 20   bits: 5/5
c ---[1390]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[1386]---> Adder-cost: 32   maxlim: 28   bits: 5/5
c ---[1384]---> Adder-cost: 26   maxlim: 22   bits: 5/5
c ---[1382]---> Adder-cost: 100   maxlim: 54   bits: 6/6
c ---[1380]---> Adder-cost: 46   maxlim: 29   bits: 5/5
c ---[1378]---> Adder-cost: 164   maxlim: 85   bits: 7/7
c ---[1376]---> Adder-cost: 76   maxlim: 42   bits: 6/6
c ---[1374]---> Adder-cost: 84   maxlim: 48   bits: 6/6
c ---[1372]---> Adder-cost: 214   maxlim: 112   bits: 7/7
c ---[1370]---> Adder-cost: 246   maxlim: 138   bits: 8/8
c ---[1368]---> Adder-cost: 106   maxlim: 57   bits: 6/6
c ---[1366]---> Adder-cost: 54   maxlim: 56   bits: 6/6
c ---[1364]---> Adder-cost: 92   maxlim: 56   bits: 6/6
c ---[1362]---> Adder-cost: 380   maxlim: 195   bits: 8/8
c ---[1360]---> Adder-cost: 300   maxlim: 196   bits: 8/8
c ---[1358]---> Adder-cost: 172   maxlim: 96   bits: 7/7
c ---[1356]---> Adder-cost: 114   maxlim: 61   bits: 6/6
c ---[1354]---> Adder-cost: 134   maxlim: 69   bits: 7/7
c ---[1352]---> Adder-cost: 78   maxlim: 50   bits: 6/6
c ---[1350]---> Adder-cost: 192   maxlim: 101   bits: 7/7
c ---[1348]---> Adder-cost: 88   maxlim: 104   bits: 7/7
c ---[1346]---> Adder-cost: 94   maxlim: 58   bits: 6/6
c ---[1344]---> Adder-cost: 50   maxlim: 28   bits: 5/5
c ---[1342]---> Adder-cost: 172   maxlim: 92   bits: 7/7
c ---[1340]---> Adder-cost: 126   maxlim: 68   bits: 7/7
c ---[1338]---> Adder-cost: 66   maxlim: 44   bits: 6/6
c ---[1336]---> Adder-cost: 54   maxlim: 47   bits: 6/6
c ---[1334]---> Adder-cost: 122   maxlim: 71   bits: 7/7
c ---[1332]---> Adder-cost: 70   maxlim: 38   bits: 6/6
c ---[1330]---> Adder-cost: 56   maxlim: 31   bits: 6/5
c ---[1328]---> Adder-cost: 26   maxlim: 22   bits: 5/5
c ---[1326]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[1324]---> Adder-cost: 122   maxlim: 65   bits: 7/7
c ---[1322]---> Adder-cost: 68   maxlim: 36   bits: 6/6
c ---[1320]---> Adder-cost: 270   maxlim: 137   bits: 8/8
c ---[1318]---> Adder-cost: 256   maxlim: 139   bits: 8/8
c ---[1316]---> Adder-cost: 82   maxlim: 52   bits: 6/6
c ---[1314]---> Adder-cost: 112   maxlim: 60   bits: 6/6
c ---[1312]---> Adder-cost: 50   maxlim: 29   bits: 5/5
c ---[1310]---> Adder-cost: 42   maxlim: 25   bits: 5/5
c ---[1308]---> Adder-cost: 60   maxlim: 34   bits: 6/6
c ---[1306]---> Adder-cost: 88   maxlim: 50   bits: 6/6
c ---[1304]---> Adder-cost: 72   maxlim: 48   bits: 6/6
c ---[1302]---> Adder-cost: 160   maxlim: 83   bits: 7/7
c ---[1300]---> Adder-cost: 228   maxlim: 119   bits: 7/7
c ---[1298]---> Adder-cost: 96   maxlim: 62   bits: 6/6
c ---[1296]---> Adder-cost: 110   maxlim: 69   bits: 7/7
c ---[1294]---> Adder-cost: 218   maxlim: 116   bits: 7/7
c ---[1292]---> Adder-cost: 34   maxlim: 20   bits: 5/5
c ---[1290]---> Adder-cost: 58   maxlim: 31   bits: 6/5
c ---[1288]---> Adder-cost: 134   maxlim: 90   bits: 7/7
c ---[1286]---> Adder-cost: 128   maxlim: 68   bits: 7/7
c ---[1284]---> Adder-cost: 108   maxlim: 57   bits: 6/6
c ---[1282]---> Adder-cost: 166   maxlim: 89   bits: 7/7
c ---[1280]---> Adder-cost: 142   maxlim: 78   bits: 7/7
c ---[1278]---> Adder-cost: 100   maxlim: 54   bits: 6/6
c ---[1276]---> Adder-cost: 174   maxlim: 91   bits: 7/7
c ---[1274]---> Adder-cost: 62   maxlim: 36   bits: 6/6
c ---[1272]---> Adder-cost: 162   maxlim: 84   bits: 7/7
c ---[1270]---> Adder-cost: 132   maxlim: 74   bits: 7/7
c ---[1268]---> Adder-cost: 166   maxlim: 108   bits: 7/7
c ---[1266]---> Adder-cost: 230   maxlim: 122   bits: 7/7
c ---[1264]---> Adder-cost: 122   maxlim: 120   bits: 7/7
c ---[1262]---> Adder-cost: 142   maxlim: 82   bits: 7/7
c ---[1260]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[1258]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1254]---> Adder-cost: 42   maxlim: 26   bits: 5/5
c ---[1252]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[1250]---> Adder-cost: 18   maxlim: 12   bits: 4/4
c ---[1248]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[1246]---> Adder-cost: 80   maxlim: 46   bits: 6/6
c ---[1244]---> Adder-cost: 78   maxlim: 49   bits: 6/6
c ---[1242]---> Adder-cost: 62   maxlim: 35   bits: 6/6
c ---[1240]---> Adder-cost: 76   maxlim: 40   bits: 6/6
c ---[1238]---> Adder-cost: 70   maxlim: 46   bits: 6/6
c ---[1236]---> Adder-cost: 94   maxlim: 53   bits: 6/6
c ---[1234]---> Adder-cost: 92   maxlim: 49   bits: 6/6
c ---[1232]---> Adder-cost: 92   maxlim: 53   bits: 6/6
c ---[1230]---> Adder-cost: 72   maxlim: 42   bits: 6/6
c ---[1228]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[1226]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1224]---> Adder-cost: 10   maxlim: 7   bits: 4/3
c ---[1222]---> Adder-cost: 28   maxlim: 17   bits: 5/5
c ---[1220]---> Adder-cost: 62   maxlim: 33   bits: 6/6
c ---[1218]---> Adder-cost: 36   maxlim: 23   bits: 5/5
c ---[1216]---> Adder-cost: 66   maxlim: 35   bits: 6/6
c ---[1214]---> Adder-cost: 38   maxlim: 26   bits: 5/5
c ---[1212]---> Adder-cost: 54   maxlim: 34   bits: 6/6
c ---[1210]---> Adder-cost: 84   maxlim: 47   bits: 6/6
c ---[1208]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[1206]---> Adder-cost: 94   maxlim: 51   bits: 6/6
c ---[1204]---> Adder-cost: 74   maxlim: 47   bits: 6/6
c ---[1202]---> Adder-cost: 92   maxlim: 54   bits: 6/6
c ---[1200]---> Adder-cost: 66   maxlim: 35   bits: 6/6
c ---[1198]---> Adder-cost: 106   maxlim: 60   bits: 6/6
c ---[1196]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1194]---> Adder-cost: 34   maxlim: 29   bits: 5/5
c ---[1192]---> Adder-cost: 46   maxlim: 31   bits: 6/5
c ---[1190]---> Adder-cost: 268   maxlim: 137   bits: 8/8
c ---[1188]---> Adder-cost: 232   maxlim: 131   bits: 8/8
c ---[1186]---> Adder-cost: 232   maxlim: 122   bits: 7/7
c ---[1184]---> Adder-cost: 150   maxlim: 100   bits: 7/7
c ---[1182]---> Adder-cost: 274   maxlim: 148   bits: 8/8
c ---[1180]---> Adder-cost: 158   maxlim: 90   bits: 7/7
c ---[1178]---> Adder-cost: 102   maxlim: 59   bits: 6/6
c ---[1176]---> Adder-cost: 162   maxlim: 88   bits: 7/7
c ---[1174]---> Adder-cost: 248   maxlim: 128   bits: 8/8
c ---[1172]---> Adder-cost: 242   maxlim: 129   bits: 8/8
c ---[1170]---> Adder-cost: 114   maxlim: 64   bits: 7/7
c ---[1168]---> Adder-cost: 76   maxlim: 42   bits: 6/6
c ---[1166]---> Adder-cost: 46   maxlim: 43   bits: 6/6
c ---[1164]---> Adder-cost: 66   maxlim: 41   bits: 6/6
c ---[1162]---> Adder-cost: 68   maxlim: 40   bits: 6/6
c ---[1160]---> Adder-cost: 46   maxlim: 27   bits: 5/5
c ---[1156]---> Adder-cost: 58   maxlim: 37   bits: 6/6
c ---[1154]---> Adder-cost: 50   maxlim: 33   bits: 6/6
c ---[1152]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[1150]---> Adder-cost: 18   maxlim: 13   bits: 4/4
c ---[1148]---> Adder-cost: 10   maxlim: 13   bits: 4/4
c ---[1146]---> Adder-cost: 18   maxlim: 11   bits: 4/4
c ---[1144]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[1142]---> Adder-cost: 32   maxlim: 19   bits: 5/5
c ---[1140]---> Adder-cost: 22   maxlim: 16   bits: 5/5
c ---[1138]---> Adder-cost: 24   maxlim: 16   bits: 5/5
c ---[1136]---> Adder-cost: 86   maxlim: 48   bits: 6/6
c ---[1134]---> Adder-cost: 72   maxlim: 40   bits: 6/6
c ---[1132]---> Adder-cost: 38   maxlim: 23   bits: 5/5
c ---[1130]---> Adder-cost: 266   maxlim: 137   bits: 8/8
c ---[1128]---> Adder-cost: 218   maxlim: 111   bits: 7/7
c ---[1126]---> Adder-cost: 182   maxlim: 101   bits: 7/7
c ---[1124]---> Adder-cost: 76   maxlim: 41   bits: 6/6
c ---[1122]---> Adder-cost: 34   maxlim: 20   bits: 5/5
c ---[1120]---> Adder-cost: 164   maxlim: 94   bits: 7/7
c ---[1118]---> Adder-cost: 92   maxlim: 47   bits: 6/6
c ---[1116]---> Adder-cost: 60   maxlim: 31   bits: 6/5
c ---[1114]---> Adder-cost: 44   maxlim: 34   bits: 6/6
c ---[1112]---> Adder-cost: 110   maxlim: 65   bits: 7/7
c ---[1110]---> Adder-cost: 124   maxlim: 68   bits: 7/7
c ---[1108]---> Adder-cost: 92   maxlim: 62   bits: 6/6
c ---[1096]---> Adder-cost: 68   maxlim: 37   bits: 6/6
c ---[1094]---> Adder-cost: 86   maxlim: 48   bits: 6/6
c ---[1092]---> Adder-cost: 70   maxlim: 47   bits: 6/6
c ---[1090]---> Adder-cost: 110   maxlim: 66   bits: 7/7
c ---[1088]---> Adder-cost: 94   maxlim: 59   bits: 6/6
c ---[1086]---> Adder-cost: 190   maxlim: 101   bits: 7/7
c ---[1084]---> Adder-cost: 186   maxlim: 95   bits: 7/7
c ---[1082]---> Adder-cost: 84   maxlim: 101   bits: 7/7
c ---[1080]---> Adder-cost: 170   maxlim: 88   bits: 7/7
c ---[1078]---> Adder-cost: 42   maxlim: 23   bits: 5/5
c ---[1074]---> Adder-cost: 18   maxlim: 11   bits: 4/4
c ---[1072]---> Adder-cost: 210   maxlim: 110   bits: 7/7
c ---[1070]---> Adder-cost: 162   maxlim: 84   bits: 7/7
c ---[1068]---> Adder-cost: 122   maxlim: 77   bits: 7/7
c ---[1066]---> Adder-cost: 204   maxlim: 112   bits: 7/7
c ---[1064]---> Adder-cost: 18   maxlim: 14   bits: 4/4
c ---[1062]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1060]---> Adder-cost: 82   maxlim: 44   bits: 6/6
c ---[1058]---> Adder-cost: 116   maxlim: 65   bits: 7/7
c ---[1056]---> Adder-cost: 160   maxlim: 85   bits: 7/7
c ---[1054]---> Adder-cost: 230   maxlim: 126   bits: 7/7
c ---[1052]---> Adder-cost: 148   maxlim: 89   bits: 7/7
c ---[1048]---> Adder-cost: 84   maxlim: 49   bits: 6/6
c ---[1044]---> Adder-cost: 138   maxlim: 71   bits: 7/7
c ---[1042]---> Adder-cost: 92   maxlim: 57   bits: 6/6
c ---[1040]---> Adder-cost: 170   maxlim: 87   bits: 7/7
c ---[1038]---> Adder-cost: 202   maxlim: 111   bits: 7/7
c ---[1036]---> Adder-cost: 184   maxlim: 100   bits: 7/7
c ---[1034]---> Adder-cost: 146   maxlim: 97   bits: 7/7
c ---[1032]---> Adder-cost: 254   maxlim: 130   bits: 8/8
c ---[1030]---> Adder-cost: 198   maxlim: 135   bits: 8/8
c ---[1028]---> Adder-cost: 270   maxlim: 143   bits: 8/8
c ---[1026]---> Adder-cost: 188   maxlim: 103   bits: 7/7
c ---[1024]---> Adder-cost: 176   maxlim: 102   bits: 7/7
c ---[1022]---> Adder-cost: 192   maxlim: 112   bits: 7/7
c ---[1018]---> Adder-cost: 48   maxlim: 28   bits: 5/5
c ---[1014]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1012]---> Adder-cost: 52   maxlim: 30   bits: 5/5
c ---[1010]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1008]---> Adder-cost: 46   maxlim: 25   bits: 5/5
c ---[1004]---> Adder-cost: 16   maxlim: 22   bits: 5/5
c ---[1002]---> Adder-cost: 64   maxlim: 36   bits: 6/6
c ---[1000]---> Adder-cost: 92   maxlim: 49   bits: 6/6
c ---[ 998]---> Adder-cost: 130   maxlim: 69   bits: 7/7
c ---[ 996]---> Adder-cost: 116   maxlim: 79   bits: 7/7
c ---[ 994]---> Adder-cost: 122   maxlim: 63   bits: 7/6
c ---[ 992]---> Adder-cost: 80   maxlim: 62   bits: 6/6
c ---[ 990]---> Adder-cost: 98   maxlim: 52   bits: 6/6
c ---[ 988]---> Adder-cost: 102   maxlim: 63   bits: 7/6
c ---[ 986]---> Adder-cost: 108   maxlim: 65   bits: 7/7
c ---[ 984]---> Adder-cost: 106   maxlim: 63   bits: 7/6
c ---[ 982]---> Adder-cost: 122   maxlim: 64   bits: 7/7
c ---[ 980]---> Adder-cost: 76   maxlim: 66   bits: 7/7
c ---[ 978]---> Adder-cost: 124   maxlim: 70   bits: 7/7
c ---[ 976]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[ 974]---> Adder-cost: 98   maxlim: 57   bits: 6/6
c ---[ 972]---> Adder-cost: 74   maxlim: 39   bits: 6/6
c ---[ 970]---> Adder-cost: 68   maxlim: 37   bits: 6/6
c ---[ 968]---> Adder-cost: 52   maxlim: 32   bits: 6/6
c ---[ 966]---> Adder-cost: 48   maxlim: 32   bits: 6/6
c ---[ 962]---> Adder-cost: 60   maxlim: 35   bits: 6/6
c ---[ 960]---> Adder-cost: 60   maxlim: 38   bits: 6/6
c ---[ 958]---> Adder-cost: 202   maxlim: 107   bits: 7/7
c ---[ 956]---> Adder-cost: 230   maxlim: 124   bits: 7/7
c ---[ 954]---> Adder-cost: 230   maxlim: 137   bits: 8/8
c ---[ 952]---> Adder-cost: 144   maxlim: 81   bits: 7/7
c ---[ 950]---> Adder-cost: 516   maxlim: 268   bits: 9/9
c ---[ 948]---> Adder-cost: 618   maxlim: 330   bits: 9/9
c ---[ 946]---> Adder-cost: 248   maxlim: 130   bits: 8/8
c ---[ 944]---> Adder-cost: 182   maxlim: 107   bits: 7/7
c ---[ 942]---> Adder-cost: 142   maxlim: 86   bits: 7/7
c ---[ 940]---> Adder-cost: 104   maxlim: 76   bits: 7/7
c ---[ 938]---> Adder-cost: 512   maxlim: 282   bits: 9/9
c ---[ 936]---> Adder-cost: 112   maxlim: 59   bits: 6/6
c ---[ 932]---> Adder-cost: 142   maxlim: 78   bits: 7/7
c ---[ 930]---> Adder-cost: 110   maxlim: 64   bits: 7/7
c ---[ 928]---> Adder-cost: 98   maxlim: 60   bits: 6/6
c ---[ 926]---> Adder-cost: 94   maxlim: 62   bits: 6/6
c ---[ 922]---> Adder-cost: 52   maxlim: 65   bits: 7/7
c ---[ 920]---> Adder-cost: 116   maxlim: 72   bits: 7/7
c ---[ 918]---> Adder-cost: 66   maxlim: 38   bits: 6/6
c ---[ 914]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 912]---> Adder-cost: 144   maxlim: 75   bits: 7/7
c ---[ 910]---> Adder-cost: 60   maxlim: 38   bits: 6/6
c ---[ 908]---> Adder-cost: 54   maxlim: 31   bits: 6/5
c ---[ 906]---> Adder-cost: 130   maxlim: 75   bits: 7/7
c ---[ 904]---> Adder-cost: 94   maxlim: 52   bits: 6/6
c ---[ 902]---> Adder-cost: 84   maxlim: 51   bits: 6/6
c ---[ 900]---> Adder-cost: 70   maxlim: 40   bits: 6/6
c ---[ 898]---> Adder-cost: 322   maxlim: 167   bits: 8/8
c ---[ 896]---> Adder-cost: 134   maxlim: 167   bits: 8/8
c ---[ 894]---> Adder-cost: 378   maxlim: 204   bits: 8/8
c ---[ 892]---> Adder-cost: 372   maxlim: 201   bits: 8/8
c ---[ 890]---> Adder-cost: 328   maxlim: 176   bits: 8/8
c ---[ 888]---> Adder-cost: 198   maxlim: 161   bits: 8/8
c ---[ 886]---> Adder-cost: 212   maxlim: 114   bits: 7/7
c ---[ 884]---> Adder-cost: 102   maxlim: 58   bits: 6/6
c ---[ 882]---> Adder-cost: 102   maxlim: 65   bits: 7/7
c ---[ 880]---> Adder-cost: 80   maxlim: 61   bits: 6/6
c ---[ 878]---> Adder-cost: 116   maxlim: 67   bits: 7/7
c ---[ 876]---> Adder-cost: 212   maxlim: 122   bits: 7/7
c ---[ 874]---> Adder-cost: 132   maxlim: 70   bits: 7/7
c ---[ 872]---> Adder-cost: 216   maxlim: 120   bits: 7/7
c ---[ 870]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[ 868]---> Adder-cost: 34   maxlim: 22   bits: 5/5
c ---[ 866]---> Adder-cost: 60   maxlim: 31   bits: 6/5
c ---[ 862]---> Adder-cost: 36   maxlim: 32   bits: 6/6
c ---[ 860]---> Adder-cost: 228   maxlim: 120   bits: 7/7
c ---[ 858]---> Adder-cost: 198   maxlim: 122   bits: 7/7
c ---[ 856]---> Adder-cost: 194   maxlim: 104   bits: 7/7
c ---[ 854]---> Adder-cost: 150   maxlim: 111   bits: 7/7
c ---[ 852]---> Adder-cost: 372   maxlim: 196   bits: 8/8
c ---[ 850]---> Adder-cost: 328   maxlim: 200   bits: 8/8
c ---[ 848]---> Adder-cost: 144   maxlim: 75   bits: 7/7
c ---[ 846]---> Adder-cost: 68   maxlim: 70   bits: 7/7
c ---[ 844]---> Adder-cost: 172   maxlim: 94   bits: 7/7
c ---[ 842]---> Adder-cost: 282   maxlim: 156   bits: 8/8
c ---[ 840]---> Adder-cost: 176   maxlim: 94   bits: 7/7
c ---[ 838]---> Adder-cost: 180   maxlim: 104   bits: 7/7
c ---[ 836]---> Adder-cost: 108   maxlim: 59   bits: 6/6
c ---[ 834]---> Adder-cost: 92   maxlim: 56   bits: 6/6
c ---[ 830]---> Adder-cost: 84   maxlim: 46   bits: 6/6
c ---[ 828]---> Adder-cost: 310   maxlim: 168   bits: 8/8
c ---[ 826]---> Adder-cost: 254   maxlim: 161   bits: 8/8
c ---[ 822]---> Adder-cost: 252   maxlim: 127   bits: 8/7
c ---[ 820]---> Adder-cost: 74   maxlim: 39   bits: 6/6
c ---[ 818]---> Adder-cost: 70   maxlim: 41   bits: 6/6
c ---[ 816]---> Adder-cost: 186   maxlim: 96   bits: 7/7
c ---[ 814]---> Adder-cost: 136   maxlim: 77   bits: 7/7
c ---[ 812]---> Adder-cost: 248   maxlim: 128   bits: 8/8
c ---[ 810]---> Adder-cost: 198   maxlim: 134   bits: 8/8
c ---[ 808]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 806]---> Adder-cost: 34   maxlim: 20   bits: 5/5
c ---[ 802]---> Adder-cost: 176   maxlim: 94   bits: 7/7
c ---[ 800]---> Adder-cost: 106   maxlim: 59   bits: 6/6
c ---[ 798]---> Adder-cost: 58   maxlim: 38   bits: 6/6
c ---[ 796]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 794]---> Adder-cost: 62   maxlim: 31   bits: 6/5
c ---[ 792]---> Adder-cost: 32   maxlim: 20   bits: 5/5
c ---[ 790]---> Adder-cost: 20   maxlim: 19   bits: 5/5
c ---[ 788]---> Adder-cost: 78   maxlim: 42   bits: 6/6
c ---[ 786]---> Adder-cost: 60   maxlim: 37   bits: 6/6
c ---[ 784]---> Adder-cost: 80   maxlim: 46   bits: 6/6
c ---[ 782]---> Adder-cost: 72   maxlim: 48   bits: 6/6
c ---[ 780]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[ 778]---> Adder-cost: 80   maxlim: 55   bits: 6/6
c ---[ 776]---> Adder-cost: 328   maxlim: 173   bits: 8/8
c ---[ 774]---> Adder-cost: 256   maxlim: 151   bits: 8/8
c ---[ 772]---> Adder-cost: 98   maxlim: 51   bits: 6/6
c ---[ 770]---> Adder-cost: 58   maxlim: 49   bits: 6/6
c ---[ 768]---> Adder-cost: 64   maxlim: 36   bits: 6/6
c ---[ 766]---> Adder-cost: 74   maxlim: 40   bits: 6/6
c ---[ 764]---> Adder-cost: 58   maxlim: 32   bits: 6/6
c ---[ 762]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 760]---> Adder-cost: 194   maxlim: 100   bits: 7/7
c ---[ 758]---> Adder-cost: 180   maxlim: 98   bits: 7/7
c ---[ 756]---> Adder-cost: 142   maxlim: 85   bits: 7/7
c ---[ 754]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[ 752]---> Adder-cost: 26   maxlim: 20   bits: 5/5
c ---[ 750]---> Adder-cost: 120   maxlim: 67   bits: 7/7
c ---[ 748]---> Adder-cost: 62   maxlim: 33   bits: 6/6
c ---[ 746]---> Adder-cost: 58   maxlim: 32   bits: 6/6
c ---[ 744]---> Adder-cost: 138   maxlim: 81   bits: 7/7
c ---[ 742]---> Adder-cost: 328   maxlim: 173   bits: 8/8
c ---[ 740]---> Adder-cost: 240   maxlim: 156   bits: 8/8
c ---[ 738]---> Adder-cost: 190   maxlim: 103   bits: 7/7
c ---[ 736]---> Adder-cost: 142   maxlim: 80   bits: 7/7
c ---[ 734]---> Adder-cost: 138   maxlim: 81   bits: 7/7
c ---[ 732]---> Adder-cost: 94   maxlim: 93   bits: 7/7
c ---[ 730]---> Adder-cost: 112   maxlim: 92   bits: 7/7
c ---[ 728]---> Adder-cost: 164   maxlim: 91   bits: 7/7
c ---[ 726]---> Adder-cost: 152   maxlim: 89   bits: 7/7
c ---[ 724]---> Adder-cost: 286   maxlim: 147   bits: 8/8
c ---[ 722]---> Adder-cost: 244   maxlim: 141   bits: 8/8
c ---[ 720]---> Adder-cost: 194   maxlim: 103   bits: 7/7
c ---[ 718]---> Adder-cost: 162   maxlim: 102   bits: 7/7
c ---[ 716]---> Adder-cost: 276   maxlim: 145   bits: 8/8
c ---[ 714]---> Adder-cost: 152   maxlim: 82   bits: 7/7
c ---[ 712]---> Adder-cost: 172   maxlim: 91   bits: 7/7
c ---[ 710]---> Adder-cost: 124   maxlim: 72   bits: 7/7
c ---[ 708]---> Adder-cost: 112   maxlim: 59   bits: 6/6
c ---[ 706]---> Adder-cost: 88   maxlim: 62   bits: 6/6
c ---[ 704]---> Adder-cost: 174   maxlim: 97   bits: 7/7
c ---[ 702]---> Adder-cost: 130   maxlim: 70   bits: 7/7
c ---[ 700]---> Adder-cost: 98   maxlim: 69   bits: 7/7
c ---[ 698]---> Adder-cost: 452   maxlim: 240   bits: 8/8
c ---[ 696]---> Adder-cost: 376   maxlim: 231   bits: 8/8
c ---[ 694]---> Adder-cost: 262   maxlim: 146   bits: 8/8
c ---[ 692]---> Adder-cost: 84   maxlim: 146   bits: 8/8
c ---[ 690]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 688]---> Adder-cost: 0   maxlim: 2   bits: 2/2
c ---[ 686]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 684]---> Adder-cost: 4   maxlim: 4   bits: 3/3
c ---[ 680]---> Adder-cost: 146   maxlim: 78   bits: 7/7
c ---[ 678]---> Adder-cost: 122   maxlim: 64   bits: 7/7
c ---[ 676]---> Adder-cost: 112   maxlim: 64   bits: 7/7
c ---[ 674]---> Adder-cost: 264   maxlim: 139   bits: 8/8
c ---[ 672]---> Adder-cost: 60   maxlim: 32   bits: 6/6
c ---[ 670]---> Adder-cost: 42   maxlim: 31   bits: 6/5
c ---[ 668]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 666]---> Adder-cost: 28   maxlim: 15   bits: 5/4
c ---[ 664]---> Adder-cost: 232   maxlim: 123   bits: 7/7
c ---[ 662]---> Adder-cost: 210   maxlim: 115   bits: 7/7
c ---[ 660]---> Adder-cost: 46   maxlim: 25   bits: 5/5
c ---[ 658]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[ 656]---> Adder-cost: 20   maxlim: 21   bits: 5/5
c ---[ 654]---> Adder-cost: 144   maxlim: 75   bits: 7/7
c ---[ 652]---> Adder-cost: 170   maxlim: 101   bits: 7/7
c ---[ 650]---> Adder-cost: 112   maxlim: 60   bits: 6/6
c ---[ 648]---> Adder-cost: 88   maxlim: 54   bits: 6/6
c ---[ 646]---> Adder-cost: 224   maxlim: 118   bits: 7/7
c ---[ 644]---> Adder-cost: 224   maxlim: 125   bits: 7/7
c ---[ 642]---> Adder-cost: 224   maxlim: 120   bits: 7/7
c ---[ 640]---> Adder-cost: 244   maxlim: 136   bits: 8/8
c ---[ 638]---> Adder-cost: 588   maxlim: 308   bits: 9/9
c ---[ 636]---> Adder-cost: 480   maxlim: 298   bits: 9/9
c ---[ 634]---> Adder-cost: 224   maxlim: 116   bits: 7/7
c ---[ 632]---> Adder-cost: 170   maxlim: 115   bits: 7/7
c ---[ 630]---> Adder-cost: 524   maxlim: 276   bits: 9/9
c ---[ 628]---> Adder-cost: 428   maxlim: 279   bits: 9/9
c ---[ 626]---> Adder-cost: 332   maxlim: 179   bits: 8/8
c ---[ 624]---> Adder-cost: 246   maxlim: 145   bits: 8/8
c ---[ 620]---> Adder-cost: 306   maxlim: 165   bits: 8/8
c ---[ 618]---> Adder-cost: 248   maxlim: 170   bits: 8/8
c ---[ 616]---> Adder-cost: 236   maxlim: 152   bits: 8/8
c ---[ 614]---> Adder-cost: 194   maxlim: 116   bits: 7/7
c ---[ 612]---> Adder-cost: 164   maxlim: 109   bits: 7/7
c ---[ 610]---> Adder-cost: 260   maxlim: 162   bits: 8/8
c ---[ 608]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[ 606]---> Adder-cost: 54   maxlim: 31   bits: 6/5
c ---[ 604]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 602]---> Adder-cost: 36   maxlim: 28   bits: 5/5
c ---[ 600]---> Adder-cost: 130   maxlim: 67   bits: 7/7
c ---[ 598]---> Adder-cost: 114   maxlim: 68   bits: 7/7
c ---[ 596]---> Adder-cost: 84   maxlim: 46   bits: 6/6
c ---[ 594]---> Adder-cost: 86   maxlim: 55   bits: 6/6
c ---[ 592]---> Adder-cost: 42   maxlim: 27   bits: 5/5
c ---[ 590]---> Adder-cost: 184   maxlim: 97   bits: 7/7
c ---[ 588]---> Adder-cost: 558   maxlim: 287   bits: 9/9
c ---[ 586]---> Adder-cost: 408   maxlim: 288   bits: 9/9
c ---[ 584]---> Adder-cost: 594   maxlim: 305   bits: 9/9
c ---[ 582]---> Adder-cost: 460   maxlim: 293   bits: 9/9
c ---[ 580]---> Adder-cost: 204   maxlim: 107   bits: 7/7
c ---[ 578]---> Adder-cost: 190   maxlim: 110   bits: 7/7
c ---[ 576]---> Adder-cost: 162   maxlim: 87   bits: 7/7
c ---[ 574]---> Adder-cost: 88   maxlim: 89   bits: 7/7
c ---[ 572]---> Adder-cost: 274   maxlim: 144   bits: 8/8
c ---[ 570]---> Adder-cost: 262   maxlim: 140   bits: 8/8
c ---[ 568]---> Adder-cost: 126   maxlim: 63   bits: 7/6
c ---[ 566]---> Adder-cost: 72   maxlim: 46   bits: 6/6
c ---[ 564]---> Adder-cost: 76   maxlim: 42   bits: 6/6
c ---[ 562]---> Adder-cost: 376   maxlim: 203   bits: 8/8
c ---[ 560]---> Adder-cost: 360   maxlim: 215   bits: 8/8
c ---[ 558]---> Adder-cost: 166   maxlim: 88   bits: 7/7
c ---[ 556]---> Adder-cost: 140   maxlim: 88   bits: 7/7
c ---[ 554]---> Adder-cost: 134   maxlim: 81   bits: 7/7
c ---[ 552]---> Adder-cost: 118   maxlim: 76   bits: 7/7
c ---[ 550]---> Adder-cost: 130   maxlim: 81   bits: 7/7
c ---[ 548]---> Adder-cost: 134   maxlim: 83   bits: 7/7
c ---[ 546]---> Adder-cost: 134   maxlim: 81   bits: 7/7
c ---[ 544]---> Adder-cost: 118   maxlim: 69   bits: 7/7
c ---[ 542]---> Adder-cost: 102   maxlim: 70   bits: 7/7
c ---[ 540]---> Adder-cost: 148   maxlim: 88   bits: 7/7
c ---[ 538]---> Adder-cost: 100   maxlim: 89   bits: 7/7
c ---[ 536]---> Adder-cost: 138   maxlim: 75   bits: 7/7
c ---[ 534]---> Adder-cost: 144   maxlim: 78   bits: 7/7
c ---[ 532]---> Adder-cost: 146   maxlim: 87   bits: 7/7
c ---[ 530]---> Adder-cost: 260   maxlim: 134   bits: 8/8
c ---[ 528]---> Adder-cost: 154   maxlim: 84   bits: 7/7
c ---[ 526]---> Adder-cost: 110   maxlim: 77   bits: 7/7
c ---[ 524]---> Adder-cost: 242   maxlim: 130   bits: 8/8
c ---[ 522]---> Adder-cost: 112   maxlim: 59   bits: 6/6
c ---[ 520]---> Adder-cost: 106   maxlim: 61   bits: 6/6
c ---[ 518]---> Adder-cost: 306   maxlim: 162   bits: 8/8
c ---[ 516]---> Adder-cost: 310   maxlim: 163   bits: 8/8
c ---[ 514]---> Adder-cost: 292   maxlim: 156   bits: 8/8
c ---[ 512]---> Adder-cost: 288   maxlim: 157   bits: 8/8
c ---[ 510]---> Adder-cost: 236   maxlim: 167   bits: 8/8
c ---[ 508]---> Adder-cost: 262   maxlim: 149   bits: 8/8
c ---[ 506]---> Adder-cost: 220   maxlim: 158   bits: 8/8
c ---[ 504]---> Adder-cost: 354   maxlim: 185   bits: 8/8
c ---[ 500]---> Adder-cost: 260   maxlim: 158   bits: 8/8
c ---[ 498]---> Adder-cost: 262   maxlim: 179   bits: 8/8
c ---[ 496]---> Adder-cost: 264   maxlim: 143   bits: 8/8
c ---[ 494]---> Adder-cost: 124   maxlim: 116   bits: 7/7
c ---[ 492]---> Adder-cost: 302   maxlim: 159   bits: 8/8
c ---[ 490]---> Adder-cost: 258   maxlim: 152   bits: 8/8
c ---[ 488]---> Adder-cost: 412   maxlim: 213   bits: 8/8
c ---[ 486]---> Adder-cost: 320   maxlim: 204   bits: 8/8
c ---[ 484]---> Adder-cost: 288   maxlim: 155   bits: 8/8
c ---[ 482]---> Adder-cost: 294   maxlim: 165   bits: 8/8
c ---[ 480]---> Adder-cost: 262   maxlim: 154   bits: 8/8
c ---[ 478]---> Adder-cost: 278   maxlim: 158   bits: 8/8
c ---[ 476]---> Adder-cost: 280   maxlim: 149   bits: 8/8
c ---[ 474]---> Adder-cost: 276   maxlim: 154   bits: 8/8
c ---[ 472]---> Adder-cost: 672   maxlim: 364   bits: 9/9
c ---[ 470]---> Adder-cost: 266   maxlim: 145   bits: 8/8
c ---[ 468]---> Adder-cost: 226   maxlim: 138   bits: 8/8
c ---[ 466]---> Adder-cost: 376   maxlim: 193   bits: 8/8
c ---[ 464]---> Adder-cost: 348   maxlim: 188   bits: 8/8
c ---[ 462]---> Adder-cost: 186   maxlim: 190   bits: 8/8
c ---[ 458]---> Adder-cost: 138   maxlim: 73   bits: 7/7
c ---[ 456]---> Adder-cost: 118   maxlim: 74   bits: 7/7
c ---[ 454]---> Adder-cost: 140   maxlim: 75   bits: 7/7
c ---[ 452]---> Adder-cost: 116   maxlim: 72   bits: 7/7
c ---[ 450]---> Adder-cost: 138   maxlim: 74   bits: 7/7
c ---[ 448]---> Adder-cost: 110   maxlim: 72   bits: 7/7
c ---[ 446]---> Adder-cost: 300   maxlim: 162   bits: 8/8
c ---[ 444]---> Adder-cost: 300   maxlim: 170   bits: 8/8
c ---[ 438]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[ 436]---> Adder-cost: 12   maxlim: 12   bits: 4/4
c ---[ 434]---> Adder-cost: 372   maxlim: 200   bits: 8/8
c ---[ 432]---> Adder-cost: 378   maxlim: 201   bits: 8/8
c ---[ 430]---> Adder-cost: 310   maxlim: 202   bits: 8/8
c ---[ 426]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[ 422]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[ 418]---> Adder-cost: 24   maxlim: 17   bits: 5/5
c ---[ 416]---> Adder-cost: 444   maxlim: 227   bits: 8/8
c ---[ 414]---> Adder-cost: 442   maxlim: 233   bits: 8/8
c ---[ 412]---> Adder-cost: 184   maxlim: 99   bits: 7/7
c ---[ 410]---> Adder-cost: 142   maxlim: 89   bits: 7/7
c ---[ 408]---> Adder-cost: 170   maxlim: 107   bits: 7/7
c ---[ 404]---> Adder-cost: 318   maxlim: 174   bits: 8/8
c ---[ 402]---> Adder-cost: 178   maxlim: 109   bits: 7/7
c ---[ 400]---> Adder-cost: 190   maxlim: 111   bits: 7/7
c ---[ 398]---> Adder-cost: 62   maxlim: 31   bits: 6/5
c ---[ 396]---> Adder-cost: 14   maxlim: 10   bits: 4/4
c ---[ 394]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 392]---> Adder-cost: 12   maxlim: 8   bits: 4/4
c ---[ 390]---> Adder-cost: 36   maxlim: 22   bits: 5/5
c ---[ 388]---> Adder-cost: 208   maxlim: 115   bits: 7/7
c ---[ 386]---> Adder-cost: 200   maxlim: 126   bits: 7/7
c ---[ 384]---> Adder-cost: 216   maxlim: 127   bits: 8/7
c ---[ 378]---> Adder-cost: 310   maxlim: 160   bits: 8/8
c ---[ 376]---> Adder-cost: 210   maxlim: 112   bits: 7/7
c ---[ 374]---> Adder-cost: 212   maxlim: 121   bits: 7/7
c ---[ 372]---> Adder-cost: 232   maxlim: 123   bits: 7/7
c ---[ 370]---> Adder-cost: 198   maxlim: 129   bits: 8/8
c ---[ 368]---> Adder-cost: 106   maxlim: 55   bits: 6/6
c ---[ 366]---> Adder-cost: 82   maxlim: 54   bits: 6/6
c ---[ 364]---> Adder-cost: 80   maxlim: 43   bits: 6/6
c ---[ 362]---> Adder-cost: 88   maxlim: 55   bits: 6/6
c ---[ 360]---> Adder-cost: 96   maxlim: 52   bits: 6/6
c ---[ 358]---> Adder-cost: 54   maxlim: 53   bits: 6/6
c ---[ 356]---> Adder-cost: 186   maxlim: 102   bits: 7/7
c ---[ 354]---> Adder-cost: 186   maxlim: 109   bits: 7/7
c ---[ 352]---> Adder-cost: 168   maxlim: 100   bits: 7/7
c ---[ 348]---> Adder-cost: 134   maxlim: 70   bits: 7/7
c ---[ 344]---> Adder-cost: 78   maxlim: 42   bits: 6/6
c ---[ 340]---> Adder-cost: 124   maxlim: 63   bits: 7/6
c ---[ 338]---> Adder-cost: 214   maxlim: 113   bits: 7/7
c ---[ 336]---> Adder-cost: 198   maxlim: 111   bits: 7/7
c ---[ 334]---> Adder-cost: 122   maxlim: 94   bits: 7/7
c ---[ 332]---> Adder-cost: 230   maxlim: 122   bits: 7/7
c ---[ 330]---> Adder-cost: 206   maxlim: 121   bits: 7/7
c ---[ 328]---> Adder-cost: 194   maxlim: 104   bits: 7/7
c ---[ 326]---> Adder-cost: 136   maxlim: 73   bits: 7/7
c ---[ 324]---> Adder-cost: 82   maxlim: 72   bits: 7/7
c ---[ 322]---> Adder-cost: 218   maxlim: 119   bits: 7/7
c ---[ 320]---> Adder-cost: 192   maxlim: 105   bits: 7/7
c ---[ 318]---> Adder-cost: 92   maxlim: 68   bits: 7/7
c ---[ 316]---> Adder-cost: 210   maxlim: 112   bits: 7/7
c ---[ 314]---> Adder-cost: 200   maxlim: 113   bits: 7/7
c ---[ 312]---> Adder-cost: 166   maxlim: 87   bits: 7/7
c ---[ 310]---> Adder-cost: 96   maxlim: 76   bits: 7/7
c ---[ 308]---> Adder-cost: 110   maxlim: 77   bits: 7/7
c ---[ 306]---> Adder-cost: 76   maxlim: 44   bits: 6/6
c ---[ 304]---> Adder-cost: 52   maxlim: 37   bits: 6/6
c ---[ 302]---> Adder-cost: 132   maxlim: 68   bits: 7/7
c ---[ 300]---> Adder-cost: 64   maxlim: 50   bits: 6/6
c ---[ 298]---> Adder-cost: 230   maxlim: 121   bits: 7/7
c ---[ 296]---> Adder-cost: 158   maxlim: 121   bits: 7/7
c ---[ 294]---> Adder-cost: 200   maxlim: 106   bits: 7/7
c ---[ 292]---> Adder-cost: 130   maxlim: 106   bits: 7/7
c ---[ 290]---> Adder-cost: 258   maxlim: 135   bits: 8/8
c ---[ 288]---> Adder-cost: 104   maxlim: 108   bits: 7/7
c ---[ 286]---> Adder-cost: 194   maxlim: 103   bits: 7/7
c ---[ 284]---> Adder-cost: 156   maxlim: 117   bits: 7/7
c ---[ 282]---> Adder-cost: 188   maxlim: 105   bits: 7/7
c ---[ 280]---> Adder-cost: 176   maxlim: 125   bits: 7/7
c ---[ 278]---> Adder-cost: 442   maxlim: 227   bits: 8/8
c ---[ 276]---> Adder-cost: 316   maxlim: 233   bits: 8/8
c ---[ 274]---> Adder-cost: 250   maxlim: 130   bits: 8/8
c ---[ 272]---> Adder-cost: 208   maxlim: 144   bits: 8/8
c ---[ 270]---> Adder-cost: 334   maxlim: 180   bits: 8/8
c ---[ 268]---> Adder-cost: 250   maxlim: 187   bits: 8/8
c ---[ 266]---> Adder-cost: 308   maxlim: 160   bits: 8/8
c ---[ 264]---> Adder-cost: 282   maxlim: 159   bits: 8/8
c ---[ 262]---> Adder-cost: 206   maxlim: 113   bits: 7/7
c ---[ 260]---> Adder-cost: 218   maxlim: 114   bits: 7/7
c ---[ 258]---> Adder-cost: 416   maxlim: 223   bits: 8/8
c ---[ 256]---> Adder-cost: 364   maxlim: 222   bits: 8/8
c ---[ 254]---> Adder-cost: 282   maxlim: 176   bits: 8/8
c ---[ 252]---> Adder-cost: 98   maxlim: 55   bits: 6/6
c ---[ 250]---> Adder-cost: 112   maxlim: 80   bits: 7/7
c ---[ 248]---> Adder-cost: 82   maxlim: 45   bits: 6/6
c ---[ 246]---> Adder-cost: 94   maxlim: 60   bits: 6/6
c ---[ 242]---> Adder-cost: 560   maxlim: 299   bits: 9/9
c ---[ 240]---> Adder-cost: 286   maxlim: 152   bits: 8/8
c ---[ 238]---> Adder-cost: 244   maxlim: 149   bits: 8/8
c ---[ 236]---> Adder-cost: 122   maxlim: 67   bits: 7/7
c ---[ 234]---> Adder-cost: 120   maxlim: 68   bits: 7/7
c ---[ 232]---> Adder-cost: 120   maxlim: 75   bits: 7/7
c ---[ 230]---> Adder-cost: 110   maxlim: 60   bits: 6/6
c ---[ 228]---> Adder-cost: 64   maxlim: 51   bits: 6/6
c ---[ 226]---> Adder-cost: 132   maxlim: 73   bits: 7/7
c ---[ 224]---> Adder-cost: 122   maxlim: 80   bits: 7/7
c ---[ 222]---> Adder-cost: 208   maxlim: 109   bits: 7/7
c ---[ 220]---> Adder-cost: 186   maxlim: 106   bits: 7/7
c ---[ 218]---> Adder-cost: 122   maxlim: 103   bits: 7/7
c ---[ 214]---> Adder-cost: 152   maxlim: 84   bits: 7/7
c ---[ 212]---> Adder-cost: 180   maxlim: 96   bits: 7/7
c ---[ 210]---> Adder-cost: 148   maxlim: 94   bits: 7/7
c ---[ 208]---> Adder-cost: 144   maxlim: 97   bits: 7/7
c ---[ 206]---> Adder-cost: 138   maxlim: 74   bits: 7/7
c ---[ 204]---> Adder-cost: 94   maxlim: 73   bits: 7/7
c ---[ 202]---> Adder-cost: 382   maxlim: 195   bits: 8/8
c ---[ 200]---> Adder-cost: 366   maxlim: 196   bits: 8/8
c ---[ 198]---> Adder-cost: 142   maxlim: 76   bits: 7/7
c ---[ 196]---> Adder-cost: 134   maxlim: 76   bits: 7/7
c ---[ 194]---> Adder-cost: 280   maxlim: 154   bits: 8/8
c ---[ 192]---> Adder-cost: 314   maxlim: 196   bits: 8/8
c ---[ 190]---> Adder-cost: 250   maxlim: 153   bits: 8/8
c ---[ 188]---> Adder-cost: 220   maxlim: 142   bits: 8/8
c ---[ 186]---> Adder-cost: 258   maxlim: 164   bits: 8/8
c ---[ 184]---> Adder-cost: 302   maxlim: 191   bits: 8/8
c ---[ 182]---> Adder-cost: 168   maxlim: 94   bits: 7/7
c ---[ 180]---> Adder-cost: 144   maxlim: 93   bits: 7/7
c ---[ 178]---> Adder-cost: 34   maxlim: 19   bits: 5/5
c ---[ 176]---> Adder-cost: 24   maxlim: 18   bits: 5/5
c ---[ 174]---> Adder-cost: 160   maxlim: 87   bits: 7/7
c ---[ 170]---> Adder-cost: 324   maxlim: 170   bits: 8/8
c ---[ 168]---> Adder-cost: 396   maxlim: 216   bits: 8/8
c ---[ 166]---> Adder-cost: 406   maxlim: 222   bits: 8/8
c ---[ 164]---> Adder-cost: 366   maxlim: 234   bits: 8/8
c ---[ 162]---> Adder-cost: 398   maxlim: 257   bits: 9/9
c ---[ 160]---> Adder-cost: 348   maxlim: 193   bits: 8/8
c ---[ 158]---> Adder-cost: 294   maxlim: 197   bits: 8/8
c ---[ 156]---> Adder-cost: 808   maxlim: 456   bits: 9/9
c ---[ 154]---> Adder-cost: 414   maxlim: 220   bits: 8/8
c ---[ 152]---> Adder-cost: 312   maxlim: 189   bits: 8/8
c ---[ 150]---> Adder-cost: 220   maxlim: 120   bits: 7/7
c ---[ 148]---> Adder-cost: 194   maxlim: 125   bits: 7/7
c ---[ 146]---> Adder-cost: 244   maxlim: 131   bits: 8/8
c ---[ 144]---> Adder-cost: 210   maxlim: 130   bits: 8/8
c ---[ 142]---> Adder-cost: 210   maxlim: 133   bits: 8/8
c ---[ 140]---> Adder-cost: 226   maxlim: 142   bits: 8/8
c ---[ 138]---> Adder-cost: 634   maxlim: 337   bits: 9/9
c ---[ 136]---> Adder-cost: 500   maxlim: 348   bits: 9/9
c ---[ 134]---> Adder-cost: 304   maxlim: 159   bits: 8/8
c ---[ 132]---> Adder-cost: 154   maxlim: 141   bits: 8/8
c ---[ 130]---> Adder-cost: 182   maxlim: 100   bits: 7/7
c ---[ 128]---> Adder-cost: 138   maxlim: 84   bits: 7/7
c ---[ 126]---> Adder-cost: 96   maxlim: 53   bits: 6/6
c ---[ 124]---> Adder-cost: 72   maxlim: 61   bits: 6/6
c ---[ 122]---> Adder-cost: 106   maxlim: 60   bits: 6/6
c ---[ 120]---> Adder-cost: 102   maxlim: 56   bits: 6/6
c ---[ 118]---> Adder-cost: 140   maxlim: 81   bits: 7/7
c ---[ 116]---> Adder-cost: 146   maxlim: 94   bits: 7/7
c ---[ 114]---> Adder-cost: 206   maxlim: 111   bits: 7/7
c ---[ 110]---> Adder-cost: 136   maxlim: 82   bits: 7/7
c ---[ 108]---> Adder-cost: 178   maxlim: 97   bits: 7/7
c ---[ 106]---> Adder-cost: 130   maxlim: 70   bits: 7/7
c ---[ 104]---> Adder-cost: 104   maxlim: 69   bits: 7/7
c ---[ 102]---> Adder-cost: 64   maxlim: 34   bits: 6/6
c ---[ 100]---> Adder-cost: 86   maxlim: 47   bits: 6/6
c ---[  98]---> Adder-cost: 36   maxlim: 26   bits: 5/5
c ---[  96]---> Adder-cost: 34   maxlim: 27   bits: 5/5
c ---[  94]---> Adder-cost: 50   maxlim: 31   bits: 6/5
c ---[  92]---> Adder-cost: 86   maxlim: 49   bits: 6/6
c ---[  90]---> Adder-cost: 408   maxlim: 216   bits: 8/8
c ---[  88]---> Adder-cost: 228   maxlim: 218   bits: 8/8
c ---[  86]---> Adder-cost: 498   maxlim: 285   bits: 9/9
c ---[  84]---> Adder-cost: 534   maxlim: 308   bits: 9/9
c ---[  82]---> Adder-cost: 328   maxlim: 174   bits: 8/8
c ---[  80]---> Adder-cost: 216   maxlim: 168   bits: 8/8
c ---[  78]---> Adder-cost: 512   maxlim: 263   bits: 9/9
c ---[  76]---> Adder-cost: 512   maxlim: 268   bits: 9/9
c ---[  74]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  72]---> Adder-cost: 44   maxlim: 27   bits: 5/5
c ---[  70]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  68]---> Adder-cost: 42   maxlim: 31   bits: 6/5
c ---[  66]---> Adder-cost: 46   maxlim: 28   bits: 5/5
c ---[  64]---> Adder-cost: 62   maxlim: 40   bits: 6/6
c ---[  62]---> Adder-cost: 66   maxlim: 42   bits: 6/6
c ---[  60]---> Adder-cost: 150   maxlim: 80   bits: 7/7
c ---[  58]---> Adder-cost: 80   maxlim: 77   bits: 7/7
c ---[  56]---> Adder-cost: 188   maxlim: 100   bits: 7/7
c ---[  54]---> Adder-cost: 184   maxlim: 99   bits: 7/7
c ---[  52]---> Adder-cost: 208   maxlim: 113   bits: 7/7
c ---[  50]---> Adder-cost: 174   maxlim: 117   bits: 7/7
c ---[  48]---> Adder-cost: 456   maxlim: 255   bits: 9/8
c ---[  46]---> Adder-cost: 296   maxlim: 161   bits: 8/8
c ---[  44]---> Adder-cost: 300   maxlim: 189   bits: 8/8
c ---[  42]---> Adder-cost: 338   maxlim: 219   bits: 8/8
c ---[  40]---> Adder-cost: 184   maxlim: 99   bits: 7/7
c ---[  38]---> Adder-cost: 142   maxlim: 94   bits: 7/7
c ---[  36]---> Adder-cost: 358   maxlim: 190   bits: 8/8
c ---[  34]---> Adder-cost: 280   maxlim: 208   bits: 8/8
c ---[  32]---> Adder-cost: 60   maxlim: 32   bits: 6/6
c ---[  30]---> Adder-cost: 34   maxlim: 21   bits: 5/5
c ---[  28]---> Adder-cost: 36   maxlim: 30   bits: 5/5
c ---[  26]---> Adder-cost: 30   maxlim: 20   bits: 5/5
c ---[  24]---> Adder-cost: 14   maxlim: 9   bits: 4/4
c ---[  22]---> Adder-cost: 18   maxlim: 11   bits: 4/4
c ---[  20]---> Adder-cost: 34   maxlim: 19   bits: 5/5
c ---[  18]---> Adder-cost: 52   maxlim: 37   bits: 6/6
c ---[  16]---> Adder-cost: 134   maxlim: 73   bits: 7/7
c ---[  14]---> Adder-cost: 78   maxlim: 72   bits: 7/7
c ---[  12]---> Adder-cost: 128   maxlim: 68   bits: 7/7
c ---[  10]---> Adder-cost: 82   maxlim: 50   bits: 6/6
c ---[   8]---> Adder-cost: 72   maxlim: 56   bits: 6/6
c ---[   6]---> Adder-cost: 122   maxlim: 65   bits: 7/7
c ---[   4]---> Adder-cost: 56   maxlim: 58   bits: 6/6
c ---[   2]---> Adder-cost: 104   maxlim: 61   bits: 6/6
c ---[   0]---> Adder-cost: 70   maxlim: 43   bits: 6/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  765675  2724851 |  255225       0        0     nan |  0.000 % |
c |       100 |  765144  2723024 |  280747      42      162     3.9 |  8.564 % |
c |       250 |  764258  2719958 |  308822      85      321     3.8 |  8.686 % |
c |       476 |  762617  2714259 |  339704     128      496     3.9 |  8.909 % |
c |       813 |  760724  2707724 |  373674     267     1038     3.9 |  9.172 % |
c |      1319 |  757964  2698124 |  411042     479     1880     3.9 |  9.548 % |
c |      2078 |  753130  2681308 |  452146     723     2911     4.0 | 10.198 % |
c |      3217 |  747418  2661386 |  497361    1231     5275     4.3 | 10.966 % |
c |      4927 |  739659  2634389 |  547097    2054     9470     4.6 | 11.988 % |
c |      7489 |  731497  2606017 |  601807    3650    18443     5.1 | 13.075 % |
c |     11333 |  722132  2573000 |  661987    6393    34761     5.4 | 14.305 % |
c |     17099 |  707025  2519737 |  728186   10243    59810     5.8 | 16.262 % |
#### 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.70 0.90 0.89 2/54 12911
Raw data (stat): 12911 (runsolver) R 12910 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 542672168 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.74 0.90 0.89 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14095 0 0 0 959 38 0 0 25 0 1 0 542672168 59625472 13740 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14557 13740 603 41 0 14516 0
vsize: 58228
[startup+20.0016 s]
Raw data (loadavg): 0.78 0.90 0.89 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14104 0 0 0 1960 38 0 0 25 0 1 0 542672168 59625472 13749 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14557 13749 603 41 0 14516 0
vsize: 58228
[startup+30.002 s]
Raw data (loadavg): 0.81 0.90 0.89 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14105 0 0 0 2959 39 0 0 25 0 1 0 542672168 59625472 13750 4294967295 134512640 134672761 3221224544 3221223716 134556641 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14557 13750 603 41 0 14516 0
vsize: 58228
[startup+40.0027 s]
Raw data (loadavg): 0.84 0.91 0.89 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14106 0 0 0 3959 39 0 0 25 0 1 0 542672168 59625472 13751 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14557 13751 603 41 0 14516 0
vsize: 58228
[startup+50.004 s]
Raw data (loadavg): 0.87 0.91 0.89 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14106 0 0 0 4959 39 0 0 25 0 1 0 542672168 59625472 13751 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14557 13751 603 41 0 14516 0
vsize: 58228
[startup+60.0033 s]
Raw data (loadavg): 0.89 0.91 0.89 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14123 0 0 0 5959 39 0 0 25 0 1 0 542672168 59760640 13768 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14590 13768 603 41 0 14549 0
vsize: 58360
[startup+70.0041 s]
Raw data (loadavg): 0.90 0.91 0.89 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14150 0 0 0 6959 39 0 0 25 0 1 0 542672168 59895808 13795 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14623 13795 603 41 0 14582 0
vsize: 58492
[startup+80.0042 s]
Raw data (loadavg): 0.92 0.92 0.89 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14182 0 0 0 7959 39 0 0 25 0 1 0 542672168 60030976 13827 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14656 13827 603 41 0 14615 0
vsize: 58624
[startup+90.0047 s]
Raw data (loadavg): 0.93 0.92 0.89 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14202 0 0 0 8960 39 0 0 25 0 1 0 542672168 60030976 13847 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14656 13847 603 41 0 14615 0
vsize: 58624
[startup+100.004 s]
Raw data (loadavg): 0.94 0.92 0.90 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14219 0 0 0 9960 39 0 0 25 0 1 0 542672168 60166144 13864 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14689 13864 603 41 0 14648 0
vsize: 58756
[startup+110.005 s]
Raw data (loadavg): 0.95 0.92 0.90 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14254 0 0 0 10960 39 0 0 25 0 1 0 542672168 60301312 13899 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14722 13899 603 41 0 14681 0
vsize: 58888
[startup+120.005 s]
Raw data (loadavg): 0.96 0.92 0.90 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14275 0 0 0 11960 39 0 0 25 0 1 0 542672168 60301312 13920 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14722 13920 603 41 0 14681 0
vsize: 58888
[startup+130.005 s]
Raw data (loadavg): 0.96 0.93 0.90 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14284 0 0 0 12960 39 0 0 25 0 1 0 542672168 60436480 13929 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14755 13929 603 41 0 14714 0
vsize: 59020
[startup+140.006 s]
Raw data (loadavg): 0.97 0.93 0.90 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14309 0 0 0 13960 39 0 0 25 0 1 0 542672168 60579840 13954 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14790 13954 603 41 0 14749 0
vsize: 59160
[startup+150.006 s]
Raw data (loadavg): 0.97 0.93 0.90 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14321 0 0 0 14960 39 0 0 25 0 1 0 542672168 60579840 13966 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14790 13966 603 41 0 14749 0
vsize: 59160
[startup+160.006 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14342 0 0 0 15960 39 0 0 25 0 1 0 542672168 60715008 13987 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14823 13987 603 41 0 14782 0
vsize: 59292
[startup+170.007 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14354 0 0 0 16961 39 0 0 25 0 1 0 542672168 60715008 13999 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14823 13999 603 41 0 14782 0
vsize: 59292
[startup+180.007 s]
Raw data (loadavg): 0.98 0.94 0.90 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14372 0 0 0 17961 39 0 0 25 0 1 0 542672168 60715008 14017 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14823 14017 603 41 0 14782 0
vsize: 59292
[startup+190.008 s]
Raw data (loadavg): 0.98 0.94 0.90 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14383 0 0 0 18961 39 0 0 25 0 1 0 542672168 60850176 14028 4294967295 134512640 134672761 3221224544 3221223716 134556664 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14856 14028 603 41 0 14815 0
vsize: 59424
[startup+200.008 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14393 0 0 0 19961 39 0 0 25 0 1 0 542672168 60850176 14038 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14856 14038 603 41 0 14815 0
vsize: 59424
[startup+210.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14409 0 0 0 20961 40 0 0 25 0 1 0 542672168 60850176 14054 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14856 14054 603 41 0 14815 0
vsize: 59424
[startup+220.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14427 0 0 0 21961 40 0 0 25 0 1 0 542672168 60985344 14072 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14889 14072 603 41 0 14848 0
vsize: 59556
[startup+230.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14445 0 0 0 22961 40 0 0 25 0 1 0 542672168 60985344 14090 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14889 14090 603 41 0 14848 0
vsize: 59556
[startup+240.008 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14457 0 0 0 23962 40 0 0 25 0 1 0 542672168 61120512 14102 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14922 14102 603 41 0 14881 0
vsize: 59688
[startup+250.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14472 0 0 0 24961 40 0 0 25 0 1 0 542672168 61120512 14117 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14922 14117 603 41 0 14881 0
vsize: 59688
[startup+260.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14478 0 0 0 25961 40 0 0 25 0 1 0 542672168 61120512 14123 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14922 14123 603 41 0 14881 0
vsize: 59688
[startup+270.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14485 0 0 0 26962 40 0 0 25 0 1 0 542672168 61255680 14130 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14955 14130 603 41 0 14914 0
vsize: 59820
[startup+280.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14497 0 0 0 27962 40 0 0 25 0 1 0 542672168 61255680 14142 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14955 14142 603 41 0 14914 0
vsize: 59820
[startup+290.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14508 0 0 0 28962 40 0 0 25 0 1 0 542672168 61255680 14153 4294967295 134512640 134672761 3221224544 3221223760 134561993 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14955 14153 603 41 0 14914 0
vsize: 59820
[startup+300.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14515 0 0 0 29962 40 0 0 25 0 1 0 542672168 61255680 14160 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14955 14160 603 41 0 14914 0
vsize: 59820
[startup+310.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14522 0 0 0 30962 40 0 0 25 0 1 0 542672168 61390848 14167 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14988 14167 603 41 0 14947 0
vsize: 59952
[startup+320.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14531 0 0 0 31962 40 0 0 25 0 1 0 542672168 61390848 14176 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14988 14176 603 41 0 14947 0
vsize: 59952
[startup+330.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14538 0 0 0 32962 40 0 0 25 0 1 0 542672168 61390848 14183 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14988 14183 603 41 0 14947 0
vsize: 59952
[startup+340.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14545 0 0 0 33962 41 0 0 25 0 1 0 542672168 61390848 14190 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14988 14190 603 41 0 14947 0
vsize: 59952
[startup+350.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14552 0 0 0 34962 41 0 0 25 0 1 0 542672168 61390848 14197 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14988 14197 603 41 0 14947 0
vsize: 59952
[startup+360.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14556 0 0 0 35962 41 0 0 25 0 1 0 542672168 61526016 14201 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15021 14201 603 41 0 14980 0
vsize: 60084
[startup+370.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14564 0 0 0 36963 41 0 0 25 0 1 0 542672168 61526016 14209 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15021 14209 603 41 0 14980 0
vsize: 60084
[startup+380.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14570 0 0 0 37963 41 0 0 25 0 1 0 542672168 61526016 14215 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15021 14215 603 41 0 14980 0
vsize: 60084
[startup+390.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14577 0 0 0 38963 41 0 0 25 0 1 0 542672168 61526016 14222 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15021 14222 603 41 0 14980 0
vsize: 60084
[startup+400.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14582 0 0 0 39963 41 0 0 25 0 1 0 542672168 61526016 14227 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15021 14227 603 41 0 14980 0
vsize: 60084
[startup+410.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14589 0 0 0 40963 41 0 0 25 0 1 0 542672168 61526016 14234 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15021 14234 603 41 0 14980 0
vsize: 60084
[startup+420.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14595 0 0 0 41964 41 0 0 25 0 1 0 542672168 61661184 14240 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15054 14240 603 41 0 15013 0
vsize: 60216
[startup+430.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14596 0 0 0 42964 42 0 0 25 0 1 0 542672168 61661184 14241 4294967295 134512640 134672761 3221224544 3221223732 134556676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15054 14241 603 41 0 15013 0
vsize: 60216
[startup+440.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14597 0 0 0 43964 42 0 0 25 0 1 0 542672168 61661184 14242 4294967295 134512640 134672761 3221224544 3221223760 134561993 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15054 14242 603 41 0 15013 0
vsize: 60216
[startup+450.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14600 0 0 0 44964 42 0 0 25 0 1 0 542672168 61661184 14245 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15054 14245 603 41 0 15013 0
vsize: 60216
[startup+460.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14601 0 0 0 45964 42 0 0 25 0 1 0 542672168 61661184 14246 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15054 14246 603 41 0 15013 0
vsize: 60216
[startup+470.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14603 0 0 0 46964 42 0 0 25 0 1 0 542672168 61661184 14248 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15054 14248 603 41 0 15013 0
vsize: 60216
[startup+480.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14605 0 0 0 47965 42 0 0 25 0 1 0 542672168 61661184 14250 4294967295 134512640 134672761 3221224544 3221223760 134561979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15054 14250 603 41 0 15013 0
vsize: 60216
[startup+490.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14608 0 0 0 48965 42 0 0 25 0 1 0 542672168 61661184 14253 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15054 14253 603 41 0 15013 0
vsize: 60216
[startup+500.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14608 0 0 0 49965 42 0 0 25 0 1 0 542672168 61661184 14253 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15054 14253 603 41 0 15013 0
vsize: 60216
[startup+510.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14615 0 0 0 50965 42 0 0 25 0 1 0 542672168 61661184 14260 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15054 14260 603 41 0 15013 0
vsize: 60216
[startup+520.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14615 0 0 0 51964 42 0 0 25 0 1 0 542672168 61661184 14260 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15054 14260 603 41 0 15013 0
vsize: 60216
[startup+530.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14617 0 0 0 52964 42 0 0 25 0 1 0 542672168 61661184 14262 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15054 14262 603 41 0 15013 0
vsize: 60216
[startup+540.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14618 0 0 0 53965 42 0 0 25 0 1 0 542672168 61661184 14263 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15054 14263 603 41 0 15013 0
vsize: 60216
[startup+550.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14620 0 0 0 54965 42 0 0 25 0 1 0 542672168 61661184 14265 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15054 14265 603 41 0 15013 0
vsize: 60216
[startup+560.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14623 0 0 0 55965 42 0 0 25 0 1 0 542672168 61661184 14268 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15054 14268 603 41 0 15013 0
vsize: 60216
[startup+570.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14626 0 0 0 56965 42 0 0 25 0 1 0 542672168 61661184 14271 4294967295 134512640 134672761 3221224544 3221223760 134561985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15054 14271 603 41 0 15013 0
vsize: 60216
[startup+580.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14628 0 0 0 57965 42 0 0 25 0 1 0 542672168 61661184 14273 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15054 14273 603 41 0 15013 0
vsize: 60216
[startup+590.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14628 0 0 0 58966 42 0 0 25 0 1 0 542672168 61661184 14273 4294967295 134512640 134672761 3221224544 3221223728 134556589 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15054 14273 603 41 0 15013 0
vsize: 60216
[startup+600.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14631 0 0 0 59966 42 0 0 25 0 1 0 542672168 61661184 14276 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15054 14276 603 41 0 15013 0
vsize: 60216
[startup+610.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14633 0 0 0 60966 42 0 0 25 0 1 0 542672168 61661184 14278 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15054 14278 603 41 0 15013 0
vsize: 60216
[startup+620.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14634 0 0 0 61966 42 0 0 25 0 1 0 542672168 61661184 14279 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15054 14279 603 41 0 15013 0
vsize: 60216
[startup+630.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14635 0 0 0 62966 42 0 0 25 0 1 0 542672168 61661184 14280 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15054 14280 603 41 0 15013 0
vsize: 60216
[startup+640.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14636 0 0 0 63967 42 0 0 25 0 1 0 542672168 61661184 14281 4294967295 134512640 134672761 3221224544 3221223668 134566075 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15054 14281 603 41 0 15013 0
vsize: 60216
[startup+650.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14637 0 0 0 64967 42 0 0 25 0 1 0 542672168 61661184 14282 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15054 14282 603 41 0 15013 0
vsize: 60216
[startup+660.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14638 0 0 0 65967 42 0 0 25 0 1 0 542672168 61661184 14283 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15054 14283 603 41 0 15013 0
vsize: 60216
[startup+670.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14639 0 0 0 66967 42 0 0 25 0 1 0 542672168 61661184 14284 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15054 14284 603 41 0 15013 0
vsize: 60216
[startup+680.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14640 0 0 0 67967 42 0 0 25 0 1 0 542672168 61661184 14285 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15054 14285 603 41 0 15013 0
vsize: 60216
[startup+690.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14642 0 0 0 68967 42 0 0 25 0 1 0 542672168 61661184 14287 4294967295 134512640 134672761 3221224544 3221223728 134556589 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15054 14287 603 41 0 15013 0
vsize: 60216
[startup+700.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14642 0 0 0 69967 42 0 0 25 0 1 0 542672168 61661184 14287 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15054 14287 603 41 0 15013 0
vsize: 60216
[startup+710.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14649 0 0 0 70967 42 0 0 25 0 1 0 542672168 61825024 14294 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14294 603 41 0 15053 0
vsize: 60376
[startup+720.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14650 0 0 0 71967 42 0 0 25 0 1 0 542672168 61825024 14295 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14295 603 41 0 15053 0
vsize: 60376
[startup+730.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14651 0 0 0 72968 42 0 0 25 0 1 0 542672168 61825024 14296 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14296 603 41 0 15053 0
vsize: 60376
[startup+740.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14651 0 0 0 73968 42 0 0 25 0 1 0 542672168 61825024 14296 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14296 603 41 0 15053 0
vsize: 60376
[startup+750.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14651 0 0 0 74968 42 0 0 25 0 1 0 542672168 61825024 14296 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14296 603 41 0 15053 0
vsize: 60376
[startup+760.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 12954
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14651 0 0 0 75968 42 0 0 25 0 1 0 542672168 61825024 14296 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14296 603 41 0 15053 0
vsize: 60376
[startup+770.155 s]
Raw data (loadavg): 1.14 1.00 0.92 2/54 12964
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14651 0 0 0 76981 42 0 0 25 0 1 0 542672168 61825024 14296 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14296 603 41 0 15053 0
vsize: 60376
[startup+780.16 s]
Raw data (loadavg): 1.12 1.00 0.92 2/54 12964
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14652 0 0 0 77982 42 0 0 25 0 1 0 542672168 61825024 14297 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14297 603 41 0 15053 0
vsize: 60376
[startup+790.161 s]
Raw data (loadavg): 1.10 1.00 0.92 2/54 12964
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14652 0 0 0 78982 42 0 0 25 0 1 0 542672168 61825024 14297 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14297 603 41 0 15053 0
vsize: 60376
[startup+800.166 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 12964
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14653 0 0 0 79982 42 0 0 25 0 1 0 542672168 61825024 14298 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14298 603 41 0 15053 0
vsize: 60376
[startup+810.173 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 12964
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14653 0 0 0 80983 42 0 0 25 0 1 0 542672168 61825024 14298 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14298 603 41 0 15053 0
vsize: 60376
[startup+820.173 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 12964
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14653 0 0 0 81984 42 0 0 25 0 1 0 542672168 61825024 14298 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14298 603 41 0 15053 0
vsize: 60376
[startup+830.173 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14653 0 0 0 82984 42 0 0 25 0 1 0 542672168 61825024 14298 4294967295 134512640 134672761 3221224544 3221223716 134556618 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14298 603 41 0 15053 0
vsize: 60376
[startup+840.174 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14653 0 0 0 83984 42 0 0 25 0 1 0 542672168 61825024 14298 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14298 603 41 0 15053 0
vsize: 60376
[startup+850.174 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14654 0 0 0 84984 42 0 0 25 0 1 0 542672168 61825024 14299 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14299 603 41 0 15053 0
vsize: 60376
[startup+860.174 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14654 0 0 0 85984 42 0 0 25 0 1 0 542672168 61825024 14299 4294967295 134512640 134672761 3221224544 3221223712 134560845 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14299 603 41 0 15053 0
vsize: 60376
[startup+870.175 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14654 0 0 0 86983 43 0 0 25 0 1 0 542672168 61825024 14299 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14299 603 41 0 15053 0
vsize: 60376
[startup+880.176 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14655 0 0 0 87982 43 0 0 25 0 1 0 542672168 61825024 14300 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15094 14300 603 41 0 15053 0
vsize: 60376
[startup+890.177 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14655 0 0 0 88982 43 0 0 25 0 1 0 542672168 61825024 14300 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14300 603 41 0 15053 0
vsize: 60376
[startup+900.177 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14655 0 0 0 89983 43 0 0 25 0 1 0 542672168 61825024 14300 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14300 603 41 0 15053 0
vsize: 60376
[startup+910.177 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14655 0 0 0 90983 43 0 0 25 0 1 0 542672168 61825024 14300 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14300 603 41 0 15053 0
vsize: 60376
[startup+920.178 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14655 0 0 0 91983 43 0 0 25 0 1 0 542672168 61825024 14300 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14300 603 41 0 15053 0
vsize: 60376
[startup+930.178 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14656 0 0 0 92983 43 0 0 25 0 1 0 542672168 61825024 14301 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14301 603 41 0 15053 0
vsize: 60376
[startup+940.178 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14656 0 0 0 93983 43 0 0 25 0 1 0 542672168 61825024 14301 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14301 603 41 0 15053 0
vsize: 60376
[startup+950.187 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14656 0 0 0 94984 44 0 0 25 0 1 0 542672168 61825024 14301 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14301 603 41 0 15053 0
vsize: 60376
[startup+960.186 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14658 0 0 0 95984 44 0 0 25 0 1 0 542672168 61825024 14303 4294967295 134512640 134672761 3221224544 3221223696 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14303 603 41 0 15053 0
vsize: 60376
[startup+970.186 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14659 0 0 0 96984 44 0 0 25 0 1 0 542672168 61825024 14304 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14304 603 41 0 15053 0
vsize: 60376
[startup+980.186 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14659 0 0 0 97984 44 0 0 25 0 1 0 542672168 61825024 14304 4294967295 134512640 134672761 3221224544 3221223668 134566092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14304 603 41 0 15053 0
vsize: 60376
[startup+990.187 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14659 0 0 0 98984 44 0 0 25 0 1 0 542672168 61825024 14304 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14304 603 41 0 15053 0
vsize: 60376
[startup+1000.19 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14668 0 0 0 99984 44 0 0 25 0 1 0 542672168 61825024 14313 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14313 603 41 0 15053 0
vsize: 60376
[startup+1010.19 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14668 0 0 0 100985 44 0 0 25 0 1 0 542672168 61825024 14313 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14313 603 41 0 15053 0
vsize: 60376
[startup+1020.19 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14671 0 0 0 101985 44 0 0 25 0 1 0 542672168 61825024 14316 4294967295 134512640 134672761 3221224544 3221223728 134556589 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14316 603 41 0 15053 0
vsize: 60376
[startup+1030.19 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14671 0 0 0 102985 44 0 0 25 0 1 0 542672168 61825024 14316 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14316 603 41 0 15053 0
vsize: 60376
[startup+1040.19 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14671 0 0 0 103985 44 0 0 25 0 1 0 542672168 61825024 14316 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14316 603 41 0 15053 0
vsize: 60376
[startup+1050.19 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14671 0 0 0 104985 44 0 0 25 0 1 0 542672168 61825024 14316 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14316 603 41 0 15053 0
vsize: 60376
[startup+1060.19 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14671 0 0 0 105985 44 0 0 25 0 1 0 542672168 61825024 14316 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14316 603 41 0 15053 0
vsize: 60376
[startup+1070.19 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14672 0 0 0 106985 44 0 0 25 0 1 0 542672168 61825024 14317 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14317 603 41 0 15053 0
vsize: 60376
[startup+1080.19 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14672 0 0 0 107986 44 0 0 25 0 1 0 542672168 61825024 14317 4294967295 134512640 134672761 3221224544 3221223740 134556678 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14317 603 41 0 15053 0
vsize: 60376
[startup+1090.19 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14673 0 0 0 108986 44 0 0 25 0 1 0 542672168 61825024 14318 4294967295 134512640 134672761 3221224544 3221223712 134564729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14318 603 41 0 15053 0
vsize: 60376
[startup+1100.19 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14673 0 0 0 109986 44 0 0 25 0 1 0 542672168 61825024 14318 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14318 603 41 0 15053 0
vsize: 60376
[startup+1110.19 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12968
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14673 0 0 0 110986 44 0 0 25 0 1 0 542672168 61825024 14318 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14318 603 41 0 15053 0
vsize: 60376
[startup+1120.19 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12968
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14674 0 0 0 111986 44 0 0 25 0 1 0 542672168 61825024 14319 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14319 603 41 0 15053 0
vsize: 60376
[startup+1130.19 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12968
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14674 0 0 0 112986 44 0 0 25 0 1 0 542672168 61825024 14319 4294967295 134512640 134672761 3221224544 3221223760 134557662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14319 603 41 0 15053 0
vsize: 60376
[startup+1140.19 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12968
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14674 0 0 0 113986 44 0 0 25 0 1 0 542672168 61825024 14319 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14319 603 41 0 15053 0
vsize: 60376
[startup+1150.19 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12968
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14675 0 0 0 114986 44 0 0 25 0 1 0 542672168 61825024 14320 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14320 603 41 0 15053 0
vsize: 60376
[startup+1160.19 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12968
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14675 0 0 0 115987 44 0 0 25 0 1 0 542672168 61825024 14320 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14320 603 41 0 15053 0
vsize: 60376
[startup+1170.19 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12968
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14678 0 0 0 116987 44 0 0 25 0 1 0 542672168 61825024 14323 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14323 603 41 0 15053 0
vsize: 60376
[startup+1180.19 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12968
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14680 0 0 0 117987 44 0 0 25 0 1 0 542672168 61825024 14325 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14325 603 41 0 15053 0
vsize: 60376
[startup+1190.19 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12968
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14682 0 0 0 118987 44 0 0 25 0 1 0 542672168 61825024 14327 4294967295 134512640 134672761 3221224544 3221223696 134565101 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14327 603 41 0 15053 0
vsize: 60376
[startup+1200.19 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12968
Raw data (stat): 12911 (minisat+) R 12910 11931 11930 0 -1 0 14682 0 0 0 119987 44 0 0 25 0 1 0 542672168 61825024 14327 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15094 14327 603 41 0 15053 0
vsize: 60376
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.22 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 12968
Raw data (stat): 12911 (minisat+) Z 12910 11931 11930 0 -1 12 14684 0 0 0 119987 47 0 0 25 0 1 0 542672168 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.22
CPU time (s): 1200.36
CPU user time (s): 1199.88
CPU system time (s): 0.477927
CPU usage (%): 100.011
Max. virtual memory (Kb): 60376
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####