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/miplib2003/normalized-mps-v2-13-7-air04.opb
MD5SUM	ee388359e66788d310d5d5b34d6465c1
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	63236
Optimality of the best value was proved	NO
Number of terms in the objective function	8904
Biggest coefficient in the objective function	2258
Number of bits for the biggest coefficient in the objective function	12
Sum of the numbers in the objective function	5135151
Number of bits of the sum of numbers in the objective function	23
Biggest number in a constraint	2258
Number of bits of the biggest number in a constraint	12
Biggest sum of numbers in a constraint	5135151
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	1176.04
Number of variables	8904
Total number of constraints	9727
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	9727
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	368
Trace number 18825

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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:        374224 kB
Buffers:         35636 kB
Cached:         601892 kB
SwapCached:        176 kB
Active:         274524 kB
Inactive:       365792 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        373972 kB
SwapTotal:     2097136 kB
SwapFree:      2096860 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6812 kB
Slab:            14252 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 17:02:23 (client local time) WITH STATUS 0 IN 1200.2 SECONDS
stats: 17430 7 1200.2 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1646 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[1644]---> Adder-cost: 46   maxlim: 25   bits: 5/5
c ---[1642]---> Adder-cost: 64   maxlim: 34   bits: 6/6
c ---[1640]---> Adder-cost: 298   maxlim: 152   bits: 8/8
c ---[1638]---> Adder-cost: 112   maxlim: 60   bits: 6/6
c ---[1636]---> Adder-cost: 142   maxlim: 73   bits: 7/7
c ---[1634]---> Adder-cost: 166   maxlim: 91   bits: 7/7
c ---[1632]---> Adder-cost: 232   maxlim: 120   bits: 7/7
c ---[1630]---> Adder-cost: 170   maxlim: 113   bits: 7/7
c ---[1628]---> Adder-cost: 48   maxlim: 30   bits: 5/5
c ---[1626]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1624]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[1622]---> Adder-cost: 62   maxlim: 41   bits: 6/6
c ---[1620]---> Adder-cost: 208   maxlim: 107   bits: 7/7
c ---[1618]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[1616]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[1614]---> Adder-cost: 62   maxlim: 33   bits: 6/6
c ---[1612]---> Adder-cost: 98   maxlim: 51   bits: 6/6
c ---[1608]---> Adder-cost: 178   maxlim: 94   bits: 7/7
c ---[1606]---> Adder-cost: 40   maxlim: 28   bits: 5/5
c ---[1604]---> Adder-cost: 100   maxlim: 54   bits: 6/6
c ---[1602]---> Adder-cost: 62   maxlim: 36   bits: 6/6
c ---[1600]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1598]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[1596]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1594]---> Adder-cost: 146   maxlim: 75   bits: 7/7
c ---[1592]---> Adder-cost: 98   maxlim: 69   bits: 7/7
c ---[1590]---> Adder-cost: 190   maxlim: 98   bits: 7/7
c ---[1588]---> Adder-cost: 108   maxlim: 83   bits: 7/7
c ---[1586]---> Adder-cost: 152   maxlim: 79   bits: 7/7
c ---[1584]---> Adder-cost: 226   maxlim: 117   bits: 7/7
c ---[1582]---> Adder-cost: 200   maxlim: 120   bits: 7/7
c ---[1580]---> Adder-cost: 208   maxlim: 113   bits: 7/7
c ---[1578]---> Adder-cost: 232   maxlim: 124   bits: 7/7
c ---[1576]---> Adder-cost: 76   maxlim: 41   bits: 6/6
c ---[1574]---> Adder-cost: 158   maxlim: 93   bits: 7/7
c ---[1572]---> Adder-cost: 220   maxlim: 113   bits: 7/7
c ---[1570]---> Adder-cost: 228   maxlim: 123   bits: 7/7
c ---[1568]---> Adder-cost: 162   maxlim: 114   bits: 7/7
c ---[1566]---> Adder-cost: 48   maxlim: 28   bits: 5/5
c ---[1564]---> Adder-cost: 50   maxlim: 34   bits: 6/6
c ---[1562]---> Adder-cost: 84   maxlim: 50   bits: 6/6
c ---[1560]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1558]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1556]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[1554]---> Adder-cost: 50   maxlim: 28   bits: 5/5
c ---[1552]---> Adder-cost: 44   maxlim: 26   bits: 5/5
c ---[1550]---> Adder-cost: 24   maxlim: 16   bits: 5/5
c ---[1548]---> Adder-cost: 32   maxlim: 23   bits: 5/5
c ---[1546]---> Adder-cost: 22   maxlim: 14   bits: 4/4
c ---[1544]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1542]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1540]---> Adder-cost: 62   maxlim: 34   bits: 6/6
c ---[1538]---> Adder-cost: 74   maxlim: 47   bits: 6/6
c ---[1536]---> Adder-cost: 108   maxlim: 63   bits: 7/6
c ---[1534]---> Adder-cost: 202   maxlim: 106   bits: 7/7
c ---[1532]---> Adder-cost: 42   maxlim: 32   bits: 6/6
c ---[1530]---> Adder-cost: 0   maxlim: 106   bits: 7/7
c ---[1526]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[1524]---> Adder-cost: 108   maxlim: 59   bits: 6/6
c ---[1522]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[1520]---> Adder-cost: 62   maxlim: 35   bits: 6/6
c ---[1518]---> Adder-cost: 50   maxlim: 38   bits: 6/6
c ---[1516]---> Adder-cost: 430   maxlim: 220   bits: 8/8
c ---[1514]---> Adder-cost: 422   maxlim: 215   bits: 8/8
c ---[1512]---> Adder-cost: 284   maxlim: 145   bits: 8/8
c ---[1510]---> Adder-cost: 144   maxlim: 120   bits: 7/7
c ---[1508]---> Adder-cost: 218   maxlim: 129   bits: 8/8
c ---[1506]---> Adder-cost: 188   maxlim: 98   bits: 7/7
c ---[1504]---> Adder-cost: 66   maxlim: 36   bits: 6/6
c ---[1502]---> Adder-cost: 56   maxlim: 35   bits: 6/6
c ---[1500]---> Adder-cost: 350   maxlim: 180   bits: 8/8
c ---[1498]---> Adder-cost: 322   maxlim: 195   bits: 8/8
c ---[1494]---> Adder-cost: 152   maxlim: 85   bits: 7/7
c ---[1492]---> Adder-cost: 146   maxlim: 86   bits: 7/7
c ---[1490]---> Adder-cost: 154   maxlim: 84   bits: 7/7
c ---[1488]---> Adder-cost: 46   maxlim: 26   bits: 5/5
c ---[1486]---> Adder-cost: 218   maxlim: 113   bits: 7/7
c ---[1484]---> Adder-cost: 158   maxlim: 114   bits: 7/7
c ---[1482]---> Adder-cost: 70   maxlim: 38   bits: 6/6
c ---[1480]---> Adder-cost: 102   maxlim: 55   bits: 6/6
c ---[1478]---> Adder-cost: 114   maxlim: 68   bits: 7/7
c ---[1476]---> Adder-cost: 82   maxlim: 46   bits: 6/6
c ---[1474]---> Adder-cost: 58   maxlim: 46   bits: 6/6
c ---[1472]---> Adder-cost: 54   maxlim: 47   bits: 6/6
c ---[1468]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[1466]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1464]---> Adder-cost: 70   maxlim: 44   bits: 6/6
c ---[1462]---> Adder-cost: 100   maxlim: 54   bits: 6/6
c ---[1460]---> Adder-cost: 76   maxlim: 40   bits: 6/6
c ---[1458]---> Adder-cost: 38   maxlim: 35   bits: 6/6
c ---[1456]---> Adder-cost: 106   maxlim: 55   bits: 6/6
c ---[1454]---> Adder-cost: 120   maxlim: 68   bits: 7/7
c ---[1452]---> Adder-cost: 134   maxlim: 69   bits: 7/7
c ---[1450]---> Adder-cost: 104   maxlim: 71   bits: 7/7
c ---[1448]---> Adder-cost: 146   maxlim: 84   bits: 7/7
c ---[1446]---> Adder-cost: 110   maxlim: 62   bits: 6/6
c ---[1444]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1442]---> Adder-cost: 56   maxlim: 61   bits: 6/6
c ---[1440]---> Adder-cost: 78   maxlim: 44   bits: 6/6
c ---[1438]---> Adder-cost: 144   maxlim: 78   bits: 7/7
c ---[1436]---> Adder-cost: 158   maxlim: 86   bits: 7/7
c ---[1434]---> Adder-cost: 194   maxlim: 106   bits: 7/7
c ---[1432]---> Adder-cost: 222   maxlim: 117   bits: 7/7
c ---[1430]---> Adder-cost: 140   maxlim: 74   bits: 7/7
c ---[1428]---> Adder-cost: 128   maxlim: 70   bits: 7/7
c ---[1426]---> Adder-cost: 58   maxlim: 32   bits: 6/6
c ---[1424]---> Adder-cost: 50   maxlim: 31   bits: 6/5
c ---[1422]---> Adder-cost: 62   maxlim: 32   bits: 6/6
c ---[1420]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[1418]---> Adder-cost: 88   maxlim: 50   bits: 6/6
c ---[1416]---> Adder-cost: 316   maxlim: 163   bits: 8/8
c ---[1414]---> Adder-cost: 326   maxlim: 168   bits: 8/8
c ---[1412]---> Adder-cost: 204   maxlim: 156   bits: 8/8
c ---[1410]---> Adder-cost: 262   maxlim: 136   bits: 8/8
c ---[1408]---> Adder-cost: 142   maxlim: 135   bits: 8/8
c ---[1406]---> Adder-cost: 404   maxlim: 207   bits: 8/8
c ---[1404]---> Adder-cost: 342   maxlim: 202   bits: 8/8
c ---[1402]---> Adder-cost: 120   maxlim: 65   bits: 7/7
c ---[1400]---> Adder-cost: 98   maxlim: 61   bits: 6/6
c ---[1398]---> Adder-cost: 8   maxlim: 6   bits: 3/3
c ---[1396]---> Adder-cost: 220   maxlim: 127   bits: 8/7
c ---[1394]---> Adder-cost: 48   maxlim: 29   bits: 5/5
c ---[1392]---> Adder-cost: 212   maxlim: 119   bits: 7/7
c ---[1390]---> Adder-cost: 158   maxlim: 98   bits: 7/7
c ---[1388]---> Adder-cost: 104   maxlim: 61   bits: 6/6
c ---[1386]---> Adder-cost: 76   maxlim: 73   bits: 7/7
c ---[1384]---> Adder-cost: 136   maxlim: 72   bits: 7/7
c ---[1382]---> Adder-cost: 98   maxlim: 68   bits: 7/7
c ---[1380]---> Adder-cost: 108   maxlim: 62   bits: 6/6
c ---[1378]---> Adder-cost: 82   maxlim: 57   bits: 6/6
c ---[1376]---> Adder-cost: 36   maxlim: 20   bits: 5/5
c ---[1374]---> Adder-cost: 96   maxlim: 53   bits: 6/6
c ---[1372]---> Adder-cost: 76   maxlim: 53   bits: 6/6
c ---[1370]---> Adder-cost: 62   maxlim: 41   bits: 6/6
c ---[1368]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1366]---> Adder-cost: 130   maxlim: 69   bits: 7/7
c ---[1364]---> Adder-cost: 168   maxlim: 106   bits: 7/7
c ---[1362]---> Adder-cost: 258   maxlim: 134   bits: 8/8
c ---[1360]---> Adder-cost: 210   maxlim: 115   bits: 7/7
c ---[1358]---> Adder-cost: 216   maxlim: 116   bits: 7/7
c ---[1356]---> Adder-cost: 216   maxlim: 129   bits: 8/8
c ---[1354]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1352]---> Adder-cost: 226   maxlim: 121   bits: 7/7
c ---[1350]---> Adder-cost: 202   maxlim: 115   bits: 7/7
c ---[1348]---> Adder-cost: 46   maxlim: 35   bits: 6/6
c ---[1346]---> Adder-cost: 112   maxlim: 59   bits: 6/6
c ---[1344]---> Adder-cost: 186   maxlim: 99   bits: 7/7
c ---[1342]---> Adder-cost: 180   maxlim: 120   bits: 7/7
c ---[1340]---> Adder-cost: 260   maxlim: 144   bits: 8/8
c ---[1338]---> Adder-cost: 134   maxlim: 97   bits: 7/7
c ---[1336]---> Adder-cost: 204   maxlim: 108   bits: 7/7
c ---[1334]---> Adder-cost: 142   maxlim: 104   bits: 7/7
c ---[1332]---> Adder-cost: 50   maxlim: 29   bits: 5/5
c ---[1330]---> Adder-cost: 234   maxlim: 123   bits: 7/7
c ---[1328]---> Adder-cost: 192   maxlim: 130   bits: 8/8
c ---[1326]---> Adder-cost: 258   maxlim: 145   bits: 8/8
c ---[1324]---> Adder-cost: 212   maxlim: 120   bits: 7/7
c ---[1322]---> Adder-cost: 186   maxlim: 102   bits: 7/7
c ---[1320]---> Adder-cost: 140   maxlim: 72   bits: 7/7
c ---[1318]---> Adder-cost: 202   maxlim: 110   bits: 7/7
c ---[1316]---> Adder-cost: 126   maxlim: 66   bits: 7/7
c ---[1314]---> Adder-cost: 232   maxlim: 124   bits: 7/7
c ---[1312]---> Adder-cost: 106   maxlim: 58   bits: 6/6
c ---[1310]---> Adder-cost: 254   maxlim: 130   bits: 8/8
c ---[1308]---> Adder-cost: 80   maxlim: 46   bits: 6/6
c ---[1306]---> Adder-cost: 44   maxlim: 29   bits: 5/5
c ---[1304]---> Adder-cost: 36   maxlim: 20   bits: 5/5
c ---[1302]---> Adder-cost: 90   maxlim: 47   bits: 6/6
c ---[1300]---> Adder-cost: 176   maxlim: 91   bits: 7/7
c ---[1298]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[1296]---> Adder-cost: 40   maxlim: 29   bits: 5/5
c ---[1294]---> Adder-cost: 174   maxlim: 95   bits: 7/7
c ---[1292]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[1290]---> Adder-cost: 72   maxlim: 39   bits: 6/6
c ---[1288]---> Adder-cost: 188   maxlim: 97   bits: 7/7
c ---[1286]---> Adder-cost: 98   maxlim: 52   bits: 6/6
c ---[1284]---> Adder-cost: 104   maxlim: 57   bits: 6/6
c ---[1282]---> Adder-cost: 98   maxlim: 58   bits: 6/6
c ---[1280]---> Adder-cost: 48   maxlim: 42   bits: 6/6
c ---[1278]---> Adder-cost: 90   maxlim: 47   bits: 6/6
c ---[1276]---> Adder-cost: 90   maxlim: 53   bits: 6/6
c ---[1274]---> Adder-cost: 96   maxlim: 51   bits: 6/6
c ---[1272]---> Adder-cost: 90   maxlim: 52   bits: 6/6
c ---[1270]---> Adder-cost: 64   maxlim: 34   bits: 6/6
c ---[1268]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[1266]---> Adder-cost: 98   maxlim: 51   bits: 6/6
c ---[1264]---> Adder-cost: 88   maxlim: 47   bits: 6/6
c ---[1262]---> Adder-cost: 76   maxlim: 46   bits: 6/6
c ---[1260]---> Adder-cost: 42   maxlim: 45   bits: 6/6
c ---[1258]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[1256]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[1254]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[1252]---> Adder-cost: 58   maxlim: 32   bits: 6/6
c ---[1250]---> Adder-cost: 178   maxlim: 93   bits: 7/7
c ---[1248]---> Adder-cost: 234   maxlim: 127   bits: 8/7
c ---[1246]---> Adder-cost: 300   maxlim: 158   bits: 8/8
c ---[1244]---> Adder-cost: 132   maxlim: 69   bits: 7/7
c ---[1242]---> Adder-cost: 236   maxlim: 130   bits: 8/8
c ---[1240]---> Adder-cost: 140   maxlim: 89   bits: 7/7
c ---[1238]---> Adder-cost: 258   maxlim: 132   bits: 8/8
c ---[1236]---> Adder-cost: 162   maxlim: 84   bits: 7/7
c ---[1234]---> Adder-cost: 148   maxlim: 84   bits: 7/7
c ---[1232]---> Adder-cost: 142   maxlim: 77   bits: 7/7
c ---[1230]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[1228]---> Adder-cost: 22   maxlim: 17   bits: 5/5
c ---[1226]---> Adder-cost: 92   maxlim: 49   bits: 6/6
c ---[1224]---> Adder-cost: 140   maxlim: 71   bits: 7/7
c ---[1222]---> Adder-cost: 0   maxlim: 69   bits: 7/7
c ---[1220]---> Adder-cost: 112   maxlim: 62   bits: 6/6
c ---[1218]---> Adder-cost: 118   maxlim: 84   bits: 7/7
c ---[1216]---> Adder-cost: 108   maxlim: 92   bits: 7/7
c ---[1214]---> Adder-cost: 166   maxlim: 93   bits: 7/7
c ---[1212]---> Adder-cost: 246   maxlim: 137   bits: 8/8
c ---[1210]---> Adder-cost: 60   maxlim: 33   bits: 6/6
c ---[1208]---> Adder-cost: 42   maxlim: 25   bits: 5/5
c ---[1206]---> Adder-cost: 30   maxlim: 24   bits: 5/5
c ---[1204]---> Adder-cost: 94   maxlim: 51   bits: 6/6
c ---[1202]---> Adder-cost: 46   maxlim: 26   bits: 5/5
c ---[1200]---> Adder-cost: 18   maxlim: 13   bits: 4/4
c ---[1198]---> Adder-cost: 98   maxlim: 51   bits: 6/6
c ---[1196]---> Adder-cost: 44   maxlim: 24   bits: 5/5
c ---[1194]---> Adder-cost: 28   maxlim: 24   bits: 5/5
c ---[1192]---> Adder-cost: 82   maxlim: 44   bits: 6/6
c ---[1190]---> Adder-cost: 46   maxlim: 38   bits: 6/6
c ---[1188]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1186]---> Adder-cost: 34   maxlim: 28   bits: 5/5
c ---[1184]---> Adder-cost: 106   maxlim: 58   bits: 6/6
c ---[1182]---> Adder-cost: 92   maxlim: 50   bits: 6/6
c ---[1180]---> Adder-cost: 66   maxlim: 36   bits: 6/6
c ---[1178]---> Adder-cost: 76   maxlim: 55   bits: 6/6
c ---[1176]---> Adder-cost: 42   maxlim: 26   bits: 5/5
c ---[1174]---> Adder-cost: 132   maxlim: 70   bits: 7/7
c ---[1172]---> Adder-cost: 138   maxlim: 87   bits: 7/7
c ---[1170]---> Adder-cost: 368   maxlim: 206   bits: 8/8
c ---[1168]---> Adder-cost: 292   maxlim: 186   bits: 8/8
c ---[1166]---> Adder-cost: 102   maxlim: 55   bits: 6/6
c ---[1164]---> Adder-cost: 92   maxlim: 47   bits: 6/6
c ---[1162]---> Adder-cost: 68   maxlim: 45   bits: 6/6
c ---[1160]---> Adder-cost: 68   maxlim: 40   bits: 6/6
c ---[1158]---> Adder-cost: 74   maxlim: 42   bits: 6/6
c ---[1156]---> Adder-cost: 138   maxlim: 74   bits: 7/7
c ---[1154]---> Adder-cost: 0   maxlim: 26   bits: 5/5
c ---[1152]---> Adder-cost: 118   maxlim: 85   bits: 7/7
c ---[1150]---> Adder-cost: 196   maxlim: 105   bits: 7/7
c ---[1148]---> Adder-cost: 66   maxlim: 36   bits: 6/6
c ---[1146]---> Adder-cost: 56   maxlim: 40   bits: 6/6
c ---[1144]---> Adder-cost: 80   maxlim: 43   bits: 6/6
c ---[1140]---> Adder-cost: 98   maxlim: 52   bits: 6/6
c ---[1138]---> Adder-cost: 126   maxlim: 64   bits: 7/7
c ---[1136]---> Adder-cost: 68   maxlim: 49   bits: 6/6
c ---[1134]---> Adder-cost: 84   maxlim: 50   bits: 6/6
c ---[1132]---> Adder-cost: 138   maxlim: 118   bits: 7/7
c ---[1130]---> Adder-cost: 140   maxlim: 73   bits: 7/7
c ---[1128]---> Adder-cost: 112   maxlim: 69   bits: 7/7
c ---[1126]---> Adder-cost: 78   maxlim: 43   bits: 6/6
c ---[1124]---> Adder-cost: 106   maxlim: 60   bits: 6/6
c ---[1122]---> Adder-cost: 68   maxlim: 36   bits: 6/6
c ---[1120]---> Adder-cost: 76   maxlim: 47   bits: 6/6
c ---[1118]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[1116]---> Adder-cost: 44   maxlim: 24   bits: 5/5
c ---[1114]---> Adder-cost: 62   maxlim: 33   bits: 6/6
c ---[1112]---> Adder-cost: 50   maxlim: 38   bits: 6/6
c ---[1110]---> Adder-cost: 276   maxlim: 142   bits: 8/8
c ---[1106]---> Adder-cost: 174   maxlim: 92   bits: 7/7
c ---[1104]---> Adder-cost: 114   maxlim: 61   bits: 6/6
c ---[1102]---> Adder-cost: 90   maxlim: 49   bits: 6/6
c ---[1100]---> Adder-cost: 214   maxlim: 113   bits: 7/7
c ---[1098]---> Adder-cost: 254   maxlim: 141   bits: 8/8
c ---[1094]---> Adder-cost: 154   maxlim: 80   bits: 7/7
c ---[1092]---> Adder-cost: 202   maxlim: 105   bits: 7/7
c ---[1090]---> Adder-cost: 142   maxlim: 109   bits: 7/7
c ---[1088]---> Adder-cost: 92   maxlim: 50   bits: 6/6
c ---[1086]---> Adder-cost: 222   maxlim: 119   bits: 7/7
c ---[1084]---> Adder-cost: 114   maxlim: 96   bits: 7/7
c ---[1082]---> Adder-cost: 358   maxlim: 185   bits: 8/8
c ---[1080]---> Adder-cost: 322   maxlim: 185   bits: 8/8
c ---[1078]---> Adder-cost: 128   maxlim: 65   bits: 7/7
c ---[1076]---> Adder-cost: 112   maxlim: 70   bits: 7/7
c ---[1074]---> Adder-cost: 276   maxlim: 145   bits: 8/8
c ---[1072]---> Adder-cost: 244   maxlim: 140   bits: 8/8
c ---[1070]---> Adder-cost: 328   maxlim: 174   bits: 8/8
c ---[1068]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[1066]---> Adder-cost: 48   maxlim: 48   bits: 6/6
c ---[1064]---> Adder-cost: 78   maxlim: 49   bits: 6/6
c ---[1062]---> Adder-cost: 78   maxlim: 42   bits: 6/6
c ---[1060]---> Adder-cost: 50   maxlim: 30   bits: 5/5
c ---[1058]---> Adder-cost: 66   maxlim: 36   bits: 6/6
c ---[1056]---> Adder-cost: 66   maxlim: 40   bits: 6/6
c ---[1054]---> Adder-cost: 140   maxlim: 74   bits: 7/7
c ---[1052]---> Adder-cost: 142   maxlim: 75   bits: 7/7
c ---[1050]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[1048]---> Adder-cost: 56   maxlim: 54   bits: 6/6
c ---[1046]---> Adder-cost: 94   maxlim: 53   bits: 6/6
c ---[1044]---> Adder-cost: 106   maxlim: 55   bits: 6/6
c ---[1042]---> Adder-cost: 98   maxlim: 57   bits: 6/6
c ---[1040]---> Adder-cost: 144   maxlim: 75   bits: 7/7
c ---[1038]---> Adder-cost: 224   maxlim: 117   bits: 7/7
c ---[1036]---> Adder-cost: 184   maxlim: 98   bits: 7/7
c ---[1034]---> Adder-cost: 150   maxlim: 88   bits: 7/7
c ---[1032]---> Adder-cost: 214   maxlim: 125   bits: 7/7
c ---[1030]---> Adder-cost: 380   maxlim: 194   bits: 8/8
c ---[1028]---> Adder-cost: 64   maxlim: 34   bits: 6/6
c ---[1026]---> Adder-cost: 68   maxlim: 36   bits: 6/6
c ---[1024]---> Adder-cost: 46   maxlim: 25   bits: 5/5
c ---[1022]---> Adder-cost: 70   maxlim: 41   bits: 6/6
c ---[1020]---> Adder-cost: 132   maxlim: 74   bits: 7/7
c ---[1018]---> Adder-cost: 132   maxlim: 75   bits: 7/7
c ---[1016]---> Adder-cost: 258   maxlim: 138   bits: 8/8
c ---[1014]---> Adder-cost: 198   maxlim: 109   bits: 7/7
c ---[1012]---> Adder-cost: 156   maxlim: 90   bits: 7/7
c ---[1010]---> Adder-cost: 214   maxlim: 120   bits: 7/7
c ---[1008]---> Adder-cost: 282   maxlim: 154   bits: 8/8
c ---[1006]---> Adder-cost: 106   maxlim: 55   bits: 6/6
c ---[1004]---> Adder-cost: 104   maxlim: 57   bits: 6/6
c ---[1002]---> Adder-cost: 136   maxlim: 74   bits: 7/7
c ---[1000]---> Adder-cost: 226   maxlim: 119   bits: 7/7
c ---[ 998]---> Adder-cost: 100   maxlim: 58   bits: 6/6
c ---[ 996]---> Adder-cost: 92   maxlim: 58   bits: 6/6
c ---[ 994]---> Adder-cost: 72   maxlim: 40   bits: 6/6
c ---[ 992]---> Adder-cost: 322   maxlim: 165   bits: 8/8
c ---[ 990]---> Adder-cost: 282   maxlim: 155   bits: 8/8
c ---[ 988]---> Adder-cost: 46   maxlim: 26   bits: 5/5
c ---[ 986]---> Adder-cost: 76   maxlim: 47   bits: 6/6
c ---[ 984]---> Adder-cost: 272   maxlim: 159   bits: 8/8
c ---[ 982]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[ 980]---> Adder-cost: 68   maxlim: 41   bits: 6/6
c ---[ 978]---> Adder-cost: 30   maxlim: 16   bits: 5/5
c ---[ 976]---> Adder-cost: 112   maxlim: 60   bits: 6/6
c ---[ 974]---> Adder-cost: 64   maxlim: 43   bits: 6/6
c ---[ 972]---> Adder-cost: 80   maxlim: 44   bits: 6/6
c ---[ 970]---> Adder-cost: 58   maxlim: 45   bits: 6/6
c ---[ 968]---> Adder-cost: 68   maxlim: 35   bits: 6/6
c ---[ 964]---> Adder-cost: 40   maxlim: 25   bits: 5/5
c ---[ 962]---> Adder-cost: 72   maxlim: 40   bits: 6/6
c ---[ 960]---> Adder-cost: 48   maxlim: 28   bits: 5/5
c ---[ 956]---> Adder-cost: 32   maxlim: 20   bits: 5/5
c ---[ 954]---> Adder-cost: 104   maxlim: 55   bits: 6/6
c ---[ 952]---> Adder-cost: 34   maxlim: 28   bits: 5/5
c ---[ 950]---> Adder-cost: 238   maxlim: 123   bits: 7/7
c ---[ 948]---> Adder-cost: 198   maxlim: 113   bits: 7/7
c ---[ 946]---> Adder-cost: 104   maxlim: 56   bits: 6/6
c ---[ 944]---> Adder-cost: 108   maxlim: 64   bits: 7/7
c ---[ 942]---> Adder-cost: 124   maxlim: 69   bits: 7/7
c ---[ 940]---> Adder-cost: 124   maxlim: 70   bits: 7/7
c ---[ 938]---> Adder-cost: 240   maxlim: 130   bits: 8/8
c ---[ 936]---> Adder-cost: 238   maxlim: 131   bits: 8/8
c ---[ 934]---> Adder-cost: 254   maxlim: 138   bits: 8/8
c ---[ 932]---> Adder-cost: 114   maxlim: 77   bits: 7/7
c ---[ 930]---> Adder-cost: 170   maxlim: 141   bits: 8/8
c ---[ 928]---> Adder-cost: 256   maxlim: 134   bits: 8/8
c ---[ 926]---> Adder-cost: 160   maxlim: 86   bits: 7/7
c ---[ 924]---> Adder-cost: 80   maxlim: 55   bits: 6/6
c ---[ 920]---> Adder-cost: 130   maxlim: 67   bits: 7/7
c ---[ 918]---> Adder-cost: 160   maxlim: 93   bits: 7/7
c ---[ 916]---> Adder-cost: 104   maxlim: 93   bits: 7/7
c ---[ 914]---> Adder-cost: 272   maxlim: 146   bits: 8/8
c ---[ 912]---> Adder-cost: 182   maxlim: 151   bits: 8/8
c ---[ 910]---> Adder-cost: 50   maxlim: 77   bits: 7/7
c ---[ 908]---> Adder-cost: 316   maxlim: 168   bits: 8/8
c ---[ 906]---> Adder-cost: 350   maxlim: 197   bits: 8/8
c ---[ 904]---> Adder-cost: 232   maxlim: 128   bits: 8/8
c ---[ 902]---> Adder-cost: 92   maxlim: 56   bits: 6/6
c ---[ 900]---> Adder-cost: 64   maxlim: 45   bits: 6/6
c ---[ 898]---> Adder-cost: 94   maxlim: 52   bits: 6/6
c ---[ 896]---> Adder-cost: 182   maxlim: 101   bits: 7/7
c ---[ 894]---> Adder-cost: 354   maxlim: 194   bits: 8/8
c ---[ 892]---> Adder-cost: 316   maxlim: 165   bits: 8/8
c ---[ 890]---> Adder-cost: 224   maxlim: 161   bits: 8/8
c ---[ 888]---> Adder-cost: 154   maxlim: 79   bits: 7/7
c ---[ 886]---> Adder-cost: 126   maxlim: 65   bits: 7/7
c ---[ 884]---> Adder-cost: 86   maxlim: 50   bits: 6/6
c ---[ 882]---> Adder-cost: 66   maxlim: 36   bits: 6/6
c ---[ 880]---> Adder-cost: 56   maxlim: 35   bits: 6/6
c ---[ 878]---> Adder-cost: 70   maxlim: 41   bits: 6/6
c ---[ 876]---> Adder-cost: 44   maxlim: 26   bits: 5/5
c ---[ 874]---> Adder-cost: 128   maxlim: 67   bits: 7/7
c ---[ 872]---> Adder-cost: 126   maxlim: 72   bits: 7/7
c ---[ 870]---> Adder-cost: 356   maxlim: 189   bits: 8/8
c ---[ 868]---> Adder-cost: 168   maxlim: 177   bits: 8/8
c ---[ 866]---> Adder-cost: 110   maxlim: 89   bits: 7/7
c ---[ 862]---> Adder-cost: 116   maxlim: 64   bits: 7/7
c ---[ 860]---> Adder-cost: 98   maxlim: 61   bits: 6/6
c ---[ 858]---> Adder-cost: 132   maxlim: 76   bits: 7/7
c ---[ 856]---> Adder-cost: 208   maxlim: 111   bits: 7/7
c ---[ 854]---> Adder-cost: 156   maxlim: 91   bits: 7/7
c ---[ 850]---> Adder-cost: 86   maxlim: 54   bits: 6/6
c ---[ 848]---> Adder-cost: 128   maxlim: 74   bits: 7/7
c ---[ 846]---> Adder-cost: 272   maxlim: 150   bits: 8/8
c ---[ 844]---> Adder-cost: 100   maxlim: 72   bits: 7/7
c ---[ 842]---> Adder-cost: 304   maxlim: 166   bits: 8/8
c ---[ 838]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 836]---> Adder-cost: 200   maxlim: 103   bits: 7/7
c ---[ 834]---> Adder-cost: 236   maxlim: 131   bits: 8/8
c ---[ 832]---> Adder-cost: 340   maxlim: 175   bits: 8/8
c ---[ 830]---> Adder-cost: 272   maxlim: 177   bits: 8/8
c ---[ 828]---> Adder-cost: 156   maxlim: 83   bits: 7/7
c ---[ 826]---> Adder-cost: 138   maxlim: 86   bits: 7/7
c ---[ 824]---> Adder-cost: 62   maxlim: 31   bits: 6/5
c ---[ 822]---> Adder-cost: 72   maxlim: 39   bits: 6/6
c ---[ 820]---> Adder-cost: 56   maxlim: 31   bits: 6/5
c ---[ 818]---> Adder-cost: 106   maxlim: 58   bits: 6/6
c ---[ 816]---> Adder-cost: 58   maxlim: 54   bits: 6/6
c ---[ 814]---> Adder-cost: 186   maxlim: 95   bits: 7/7
c ---[ 812]---> Adder-cost: 150   maxlim: 80   bits: 7/7
c ---[ 810]---> Adder-cost: 136   maxlim: 75   bits: 7/7
c ---[ 808]---> Adder-cost: 136   maxlim: 76   bits: 7/7
c ---[ 806]---> Adder-cost: 152   maxlim: 83   bits: 7/7
c ---[ 804]---> Adder-cost: 164   maxlim: 91   bits: 7/7
c ---[ 802]---> Adder-cost: 242   maxlim: 127   bits: 8/7
c ---[ 800]---> Adder-cost: 0   maxlim: 39   bits: 6/6
c ---[ 798]---> Adder-cost: 142   maxlim: 129   bits: 8/8
c ---[ 796]---> Adder-cost: 140   maxlim: 73   bits: 7/7
c ---[ 794]---> Adder-cost: 138   maxlim: 71   bits: 7/7
c ---[ 792]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[ 790]---> Adder-cost: 80   maxlim: 52   bits: 6/6
c ---[ 788]---> Adder-cost: 68   maxlim: 38   bits: 6/6
c ---[ 786]---> Adder-cost: 90   maxlim: 56   bits: 6/6
c ---[ 784]---> Adder-cost: 144   maxlim: 76   bits: 7/7
c ---[ 782]---> Adder-cost: 128   maxlim: 69   bits: 7/7
c ---[ 780]---> Adder-cost: 52   maxlim: 30   bits: 5/5
c ---[ 778]---> Adder-cost: 130   maxlim: 67   bits: 7/7
c ---[ 776]---> Adder-cost: 26   maxlim: 23   bits: 5/5
c ---[ 774]---> Adder-cost: 32   maxlim: 18   bits: 5/5
c ---[ 772]---> Adder-cost: 18   maxlim: 18   bits: 5/5
c ---[ 770]---> Adder-cost: 32   maxlim: 18   bits: 5/5
c ---[ 768]---> Adder-cost: 42   maxlim: 26   bits: 5/5
c ---[ 764]---> Adder-cost: 50   maxlim: 30   bits: 5/5
c ---[ 762]---> Adder-cost: 186   maxlim: 99   bits: 7/7
c ---[ 760]---> Adder-cost: 78   maxlim: 99   bits: 7/7
c ---[ 758]---> Adder-cost: 120   maxlim: 63   bits: 7/6
c ---[ 756]---> Adder-cost: 10   maxlim: 11   bits: 4/4
c ---[ 754]---> Adder-cost: 90   maxlim: 52   bits: 6/6
c ---[ 752]---> Adder-cost: 156   maxlim: 89   bits: 7/7
c ---[ 748]---> Adder-cost: 90   maxlim: 48   bits: 6/6
c ---[ 746]---> Adder-cost: 60   maxlim: 47   bits: 6/6
c ---[ 744]---> Adder-cost: 292   maxlim: 161   bits: 8/8
c ---[ 742]---> Adder-cost: 196   maxlim: 158   bits: 8/8
c ---[ 740]---> Adder-cost: 144   maxlim: 84   bits: 7/7
c ---[ 734]---> Adder-cost: 116   maxlim: 78   bits: 7/7
c ---[ 732]---> Adder-cost: 106   maxlim: 59   bits: 6/6
c ---[ 730]---> Adder-cost: 234   maxlim: 127   bits: 8/7
c ---[ 728]---> Adder-cost: 332   maxlim: 196   bits: 8/8
c ---[ 726]---> Adder-cost: 324   maxlim: 174   bits: 8/8
c ---[ 724]---> Adder-cost: 172   maxlim: 94   bits: 7/7
c ---[ 720]---> Adder-cost: 78   maxlim: 42   bits: 6/6
c ---[ 718]---> Adder-cost: 66   maxlim: 35   bits: 6/6
c ---[ 716]---> Adder-cost: 54   maxlim: 31   bits: 6/5
c ---[ 714]---> Adder-cost: 44   maxlim: 26   bits: 5/5
c ---[ 712]---> Adder-cost: 60   maxlim: 31   bits: 6/5
c ---[ 710]---> Adder-cost: 178   maxlim: 94   bits: 7/7
c ---[ 708]---> Adder-cost: 76   maxlim: 43   bits: 6/6
c ---[ 706]---> Adder-cost: 88   maxlim: 54   bits: 6/6
c ---[ 704]---> Adder-cost: 318   maxlim: 182   bits: 8/8
c ---[ 702]---> Adder-cost: 216   maxlim: 187   bits: 8/8
c ---[ 700]---> Adder-cost: 280   maxlim: 177   bits: 8/8
c ---[ 698]---> Adder-cost: 338   maxlim: 175   bits: 8/8
c ---[ 696]---> Adder-cost: 232   maxlim: 160   bits: 8/8
c ---[ 694]---> Adder-cost: 282   maxlim: 160   bits: 8/8
c ---[ 692]---> Adder-cost: 230   maxlim: 175   bits: 8/8
c ---[ 690]---> Adder-cost: 134   maxlim: 77   bits: 7/7
c ---[ 688]---> Adder-cost: 172   maxlim: 104   bits: 7/7
c ---[ 686]---> Adder-cost: 94   maxlim: 57   bits: 6/6
c ---[ 684]---> Adder-cost: 88   maxlim: 56   bits: 6/6
c ---[ 682]---> Adder-cost: 66   maxlim: 38   bits: 6/6
c ---[ 680]---> Adder-cost: 36   maxlim: 25   bits: 5/5
c ---[ 678]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 676]---> Adder-cost: 12   maxlim: 14   bits: 4/4
c ---[ 674]---> Adder-cost: 30   maxlim: 16   bits: 5/5
c ---[ 670]---> Adder-cost: 28   maxlim: 17   bits: 5/5
c ---[ 668]---> Adder-cost: 146   maxlim: 75   bits: 7/7
c ---[ 666]---> Adder-cost: 164   maxlim: 87   bits: 7/7
c ---[ 664]---> Adder-cost: 0   maxlim: 75   bits: 7/7
c ---[ 662]---> Adder-cost: 122   maxlim: 74   bits: 7/7
c ---[ 660]---> Adder-cost: 144   maxlim: 81   bits: 7/7
c ---[ 658]---> Adder-cost: 374   maxlim: 198   bits: 8/8
c ---[ 656]---> Adder-cost: 214   maxlim: 199   bits: 8/8
c ---[ 654]---> Adder-cost: 378   maxlim: 197   bits: 8/8
c ---[ 652]---> Adder-cost: 290   maxlim: 177   bits: 8/8
c ---[ 650]---> Adder-cost: 348   maxlim: 188   bits: 8/8
c ---[ 648]---> Adder-cost: 322   maxlim: 197   bits: 8/8
c ---[ 646]---> Adder-cost: 256   maxlim: 134   bits: 8/8
c ---[ 644]---> Adder-cost: 124   maxlim: 68   bits: 7/7
c ---[ 642]---> Adder-cost: 190   maxlim: 130   bits: 8/8
c ---[ 640]---> Adder-cost: 226   maxlim: 133   bits: 8/8
c ---[ 638]---> Adder-cost: 252   maxlim: 132   bits: 8/8
c ---[ 636]---> Adder-cost: 210   maxlim: 136   bits: 8/8
c ---[ 634]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 632]---> Adder-cost: 42   maxlim: 28   bits: 5/5
c ---[ 630]---> Adder-cost: 126   maxlim: 64   bits: 7/7
c ---[ 628]---> Adder-cost: 104   maxlim: 59   bits: 6/6
c ---[ 626]---> Adder-cost: 56   maxlim: 36   bits: 6/6
c ---[ 624]---> Adder-cost: 142   maxlim: 76   bits: 7/7
c ---[ 622]---> Adder-cost: 72   maxlim: 63   bits: 7/6
c ---[ 620]---> Adder-cost: 106   maxlim: 91   bits: 7/7
c ---[ 618]---> Adder-cost: 196   maxlim: 108   bits: 7/7
c ---[ 616]---> Adder-cost: 138   maxlim: 110   bits: 7/7
c ---[ 614]---> Adder-cost: 178   maxlim: 103   bits: 7/7
c ---[ 612]---> Adder-cost: 316   maxlim: 173   bits: 8/8
c ---[ 610]---> Adder-cost: 242   maxlim: 138   bits: 8/8
c ---[ 608]---> Adder-cost: 164   maxlim: 89   bits: 7/7
c ---[ 606]---> Adder-cost: 116   maxlim: 76   bits: 7/7
c ---[ 604]---> Adder-cost: 248   maxlim: 134   bits: 8/8
c ---[ 602]---> Adder-cost: 224   maxlim: 144   bits: 8/8
c ---[ 600]---> Adder-cost: 80   maxlim: 43   bits: 6/6
c ---[ 598]---> Adder-cost: 104   maxlim: 55   bits: 6/6
c ---[ 596]---> Adder-cost: 112   maxlim: 64   bits: 7/7
c ---[ 594]---> Adder-cost: 104   maxlim: 57   bits: 6/6
c ---[ 592]---> Adder-cost: 44   maxlim: 29   bits: 5/5
c ---[ 590]---> Adder-cost: 112   maxlim: 59   bits: 6/6
c ---[ 588]---> Adder-cost: 94   maxlim: 60   bits: 6/6
c ---[ 586]---> Adder-cost: 64   maxlim: 50   bits: 6/6
c ---[ 584]---> Adder-cost: 74   maxlim: 54   bits: 6/6
c ---[ 582]---> Adder-cost: 250   maxlim: 132   bits: 8/8
c ---[ 580]---> Adder-cost: 148   maxlim: 126   bits: 7/7
c ---[ 578]---> Adder-cost: 136   maxlim: 72   bits: 7/7
c ---[ 576]---> Adder-cost: 252   maxlim: 143   bits: 8/8
c ---[ 574]---> Adder-cost: 352   maxlim: 195   bits: 8/8
c ---[ 572]---> Adder-cost: 274   maxlim: 170   bits: 8/8
c ---[ 570]---> Adder-cost: 296   maxlim: 179   bits: 8/8
c ---[ 568]---> Adder-cost: 290   maxlim: 178   bits: 8/8
c ---[ 566]---> Adder-cost: 238   maxlim: 133   bits: 8/8
c ---[ 564]---> Adder-cost: 166   maxlim: 128   bits: 8/8
c ---[ 562]---> Adder-cost: 264   maxlim: 148   bits: 8/8
c ---[ 558]---> Adder-cost: 398   maxlim: 210   bits: 8/8
c ---[ 556]---> Adder-cost: 110   maxlim: 68   bits: 7/7
c ---[ 554]---> Adder-cost: 368   maxlim: 221   bits: 8/8
c ---[ 552]---> Adder-cost: 404   maxlim: 237   bits: 8/8
c ---[ 550]---> Adder-cost: 418   maxlim: 239   bits: 8/8
c ---[ 548]---> Adder-cost: 342   maxlim: 204   bits: 8/8
c ---[ 546]---> Adder-cost: 216   maxlim: 121   bits: 7/7
c ---[ 544]---> Adder-cost: 190   maxlim: 108   bits: 7/7
c ---[ 542]---> Adder-cost: 276   maxlim: 157   bits: 8/8
c ---[ 540]---> Adder-cost: 330   maxlim: 187   bits: 8/8
c ---[ 538]---> Adder-cost: 364   maxlim: 196   bits: 8/8
c ---[ 536]---> Adder-cost: 216   maxlim: 112   bits: 7/7
c ---[ 534]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[ 532]---> Adder-cost: 60   maxlim: 32   bits: 6/6
c ---[ 530]---> Adder-cost: 184   maxlim: 121   bits: 7/7
c ---[ 528]---> Adder-cost: 140   maxlim: 74   bits: 7/7
c ---[ 526]---> Adder-cost: 128   maxlim: 67   bits: 7/7
c ---[ 524]---> Adder-cost: 172   maxlim: 94   bits: 7/7
c ---[ 522]---> Adder-cost: 112   maxlim: 76   bits: 7/7
c ---[ 520]---> Adder-cost: 250   maxlim: 130   bits: 8/8
c ---[ 518]---> Adder-cost: 262   maxlim: 137   bits: 8/8
c ---[ 516]---> Adder-cost: 304   maxlim: 156   bits: 8/8
c ---[ 514]---> Adder-cost: 284   maxlim: 173   bits: 8/8
c ---[ 512]---> Adder-cost: 368   maxlim: 194   bits: 8/8
c ---[ 510]---> Adder-cost: 54   maxlim: 31   bits: 6/5
c ---[ 508]---> Adder-cost: 284   maxlim: 194   bits: 8/8
c ---[ 506]---> Adder-cost: 278   maxlim: 148   bits: 8/8
c ---[ 504]---> Adder-cost: 116   maxlim: 139   bits: 8/8
c ---[ 502]---> Adder-cost: 342   maxlim: 178   bits: 8/8
c ---[ 500]---> Adder-cost: 208   maxlim: 184   bits: 8/8
c ---[ 498]---> Adder-cost: 420   maxlim: 222   bits: 8/8
c ---[ 496]---> Adder-cost: 586   maxlim: 327   bits: 9/9
c ---[ 494]---> Adder-cost: 658   maxlim: 353   bits: 9/9
c ---[ 492]---> Adder-cost: 462   maxlim: 346   bits: 9/9
c ---[ 490]---> Adder-cost: 394   maxlim: 221   bits: 8/8
c ---[ 488]---> Adder-cost: 128   maxlim: 80   bits: 7/7
c ---[ 486]---> Adder-cost: 364   maxlim: 224   bits: 8/8
c ---[ 484]---> Adder-cost: 260   maxlim: 145   bits: 8/8
c ---[ 482]---> Adder-cost: 256   maxlim: 140   bits: 8/8
c ---[ 480]---> Adder-cost: 222   maxlim: 121   bits: 7/7
c ---[ 478]---> Adder-cost: 118   maxlim: 130   bits: 8/8
c ---[ 476]---> Adder-cost: 296   maxlim: 155   bits: 8/8
c ---[ 474]---> Adder-cost: 280   maxlim: 144   bits: 8/8
c ---[ 472]---> Adder-cost: 156   maxlim: 89   bits: 7/7
c ---[ 470]---> Adder-cost: 138   maxlim: 78   bits: 7/7
c ---[ 468]---> Adder-cost: 128   maxlim: 66   bits: 7/7
c ---[ 466]---> Adder-cost: 138   maxlim: 78   bits: 7/7
c ---[ 464]---> Adder-cost: 70   maxlim: 62   bits: 6/6
c ---[ 462]---> Adder-cost: 180   maxlim: 95   bits: 7/7
c ---[ 460]---> Adder-cost: 204   maxlim: 112   bits: 7/7
c ---[ 456]---> Adder-cost: 254   maxlim: 134   bits: 8/8
c ---[ 454]---> Adder-cost: 124   maxlim: 68   bits: 7/7
c ---[ 452]---> Adder-cost: 80   maxlim: 54   bits: 6/6
c ---[ 450]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 448]---> Adder-cost: 52   maxlim: 38   bits: 6/6
c ---[ 446]---> Adder-cost: 112   maxlim: 61   bits: 6/6
c ---[ 444]---> Adder-cost: 172   maxlim: 108   bits: 7/7
c ---[ 442]---> Adder-cost: 80   maxlim: 61   bits: 6/6
c ---[ 436]---> Adder-cost: 184   maxlim: 95   bits: 7/7
c ---[ 434]---> Adder-cost: 68   maxlim: 37   bits: 6/6
c ---[ 432]---> Adder-cost: 64   maxlim: 41   bits: 6/6
c ---[ 430]---> Adder-cost: 50   maxlim: 29   bits: 5/5
c ---[ 428]---> Adder-cost: 86   maxlim: 50   bits: 6/6
c ---[ 426]---> Adder-cost: 306   maxlim: 164   bits: 8/8
c ---[ 424]---> Adder-cost: 210   maxlim: 147   bits: 8/8
c ---[ 422]---> Adder-cost: 72   maxlim: 40   bits: 6/6
c ---[ 420]---> Adder-cost: 50   maxlim: 29   bits: 5/5
c ---[ 418]---> Adder-cost: 38   maxlim: 23   bits: 5/5
c ---[ 416]---> Adder-cost: 252   maxlim: 128   bits: 8/8
c ---[ 414]---> Adder-cost: 260   maxlim: 143   bits: 8/8
c ---[ 412]---> Adder-cost: 176   maxlim: 96   bits: 7/7
c ---[ 410]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 408]---> Adder-cost: 76   maxlim: 46   bits: 6/6
c ---[ 406]---> Adder-cost: 186   maxlim: 106   bits: 7/7
c ---[ 404]---> Adder-cost: 140   maxlim: 80   bits: 7/7
c ---[ 402]---> Adder-cost: 102   maxlim: 69   bits: 7/7
c ---[ 400]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 398]---> Adder-cost: 50   maxlim: 45   bits: 6/6
c ---[ 396]---> Adder-cost: 100   maxlim: 58   bits: 6/6
c ---[ 394]---> Adder-cost: 128   maxlim: 74   bits: 7/7
c ---[ 390]---> Adder-cost: 106   maxlim: 55   bits: 6/6
c ---[ 388]---> Adder-cost: 312   maxlim: 161   bits: 8/8
c ---[ 386]---> Adder-cost: 228   maxlim: 172   bits: 8/8
c ---[ 384]---> Adder-cost: 584   maxlim: 302   bits: 9/9
c ---[ 382]---> Adder-cost: 434   maxlim: 302   bits: 9/9
c ---[ 380]---> Adder-cost: 348   maxlim: 196   bits: 8/8
c ---[ 378]---> Adder-cost: 74   maxlim: 44   bits: 6/6
c ---[ 376]---> Adder-cost: 312   maxlim: 200   bits: 8/8
c ---[ 374]---> Adder-cost: 278   maxlim: 145   bits: 8/8
c ---[ 372]---> Adder-cost: 230   maxlim: 139   bits: 8/8
c ---[ 370]---> Adder-cost: 284   maxlim: 155   bits: 8/8
c ---[ 368]---> Adder-cost: 208   maxlim: 122   bits: 7/7
c ---[ 366]---> Adder-cost: 198   maxlim: 124   bits: 7/7
c ---[ 364]---> Adder-cost: 234   maxlim: 143   bits: 8/8
c ---[ 362]---> Adder-cost: 148   maxlim: 84   bits: 7/7
c ---[ 360]---> Adder-cost: 120   maxlim: 96   bits: 7/7
c ---[ 358]---> Adder-cost: 40   maxlim: 25   bits: 5/5
c ---[ 356]---> Adder-cost: 70   maxlim: 42   bits: 6/6
c ---[ 354]---> Adder-cost: 40   maxlim: 23   bits: 5/5
c ---[ 352]---> Adder-cost: 86   maxlim: 54   bits: 6/6
c ---[ 350]---> Adder-cost: 48   maxlim: 28   bits: 5/5
c ---[ 346]---> Adder-cost: 170   maxlim: 89   bits: 7/7
c ---[ 344]---> Adder-cost: 216   maxlim: 112   bits: 7/7
c ---[ 342]---> Adder-cost: 146   maxlim: 109   bits: 7/7
c ---[ 340]---> Adder-cost: 118   maxlim: 69   bits: 7/7
c ---[ 338]---> Adder-cost: 88   maxlim: 56   bits: 6/6
c ---[ 336]---> Adder-cost: 172   maxlim: 92   bits: 7/7
c ---[ 334]---> Adder-cost: 104   maxlim: 57   bits: 6/6
c ---[ 332]---> Adder-cost: 188   maxlim: 103   bits: 7/7
c ---[ 330]---> Adder-cost: 260   maxlim: 143   bits: 8/8
c ---[ 328]---> Adder-cost: 190   maxlim: 131   bits: 8/8
c ---[ 326]---> Adder-cost: 162   maxlim: 89   bits: 7/7
c ---[ 324]---> Adder-cost: 168   maxlim: 106   bits: 7/7
c ---[ 320]---> Adder-cost: 144   maxlim: 79   bits: 7/7
c ---[ 318]---> Adder-cost: 114   maxlim: 61   bits: 6/6
c ---[ 316]---> Adder-cost: 90   maxlim: 54   bits: 6/6
c ---[ 314]---> Adder-cost: 106   maxlim: 56   bits: 6/6
c ---[ 312]---> Adder-cost: 42   maxlim: 28   bits: 5/5
c ---[ 310]---> Adder-cost: 116   maxlim: 64   bits: 7/7
c ---[ 308]---> Adder-cost: 0   maxlim: 56   bits: 6/6
c ---[ 306]---> Adder-cost: 266   maxlim: 141   bits: 8/8
c ---[ 304]---> Adder-cost: 246   maxlim: 134   bits: 8/8
c ---[ 302]---> Adder-cost: 152   maxlim: 86   bits: 7/7
c ---[ 300]---> Adder-cost: 154   maxlim: 88   bits: 7/7
c ---[ 298]---> Adder-cost: 160   maxlim: 85   bits: 7/7
c ---[ 296]---> Adder-cost: 146   maxlim: 84   bits: 7/7
c ---[ 292]---> Adder-cost: 348   maxlim: 188   bits: 8/8
c ---[ 290]---> Adder-cost: 262   maxlim: 144   bits: 8/8
c ---[ 288]---> Adder-cost: 238   maxlim: 125   bits: 7/7
c ---[ 286]---> Adder-cost: 238   maxlim: 139   bits: 8/8
c ---[ 284]---> Adder-cost: 124   maxlim: 66   bits: 7/7
c ---[ 282]---> Adder-cost: 180   maxlim: 98   bits: 7/7
c ---[ 280]---> Adder-cost: 120   maxlim: 68   bits: 7/7
c ---[ 278]---> Adder-cost: 114   maxlim: 65   bits: 7/7
c ---[ 276]---> Adder-cost: 310   maxlim: 159   bits: 8/8
c ---[ 274]---> Adder-cost: 342   maxlim: 207   bits: 8/8
c ---[ 272]---> Adder-cost: 222   maxlim: 118   bits: 7/7
c ---[ 270]---> Adder-cost: 220   maxlim: 136   bits: 8/8
c ---[ 268]---> Adder-cost: 256   maxlim: 142   bits: 8/8
c ---[ 266]---> Adder-cost: 186   maxlim: 129   bits: 8/8
c ---[ 264]---> Adder-cost: 236   maxlim: 137   bits: 8/8
c ---[ 262]---> Adder-cost: 260   maxlim: 150   bits: 8/8
c ---[ 260]---> Adder-cost: 268   maxlim: 144   bits: 8/8
c ---[ 258]---> Adder-cost: 178   maxlim: 101   bits: 7/7
c ---[ 256]---> Adder-cost: 218   maxlim: 117   bits: 7/7
c ---[ 254]---> Adder-cost: 152   maxlim: 84   bits: 7/7
c ---[ 252]---> Adder-cost: 140   maxlim: 81   bits: 7/7
c ---[ 250]---> Adder-cost: 92   maxlim: 74   bits: 7/7
c ---[ 246]---> Adder-cost: 132   maxlim: 68   bits: 7/7
c ---[ 244]---> Adder-cost: 48   maxlim: 30   bits: 5/5
c ---[ 242]---> Adder-cost: 136   maxlim: 74   bits: 7/7
c ---[ 240]---> Adder-cost: 164   maxlim: 91   bits: 7/7
c ---[ 238]---> Adder-cost: 170   maxlim: 109   bits: 7/7
c ---[ 236]---> Adder-cost: 266   maxlim: 138   bits: 8/8
c ---[ 234]---> Adder-cost: 214   maxlim: 134   bits: 8/8
c ---[ 232]---> Adder-cost: 28   maxlim: 16   bits: 5/5
c ---[ 230]---> Adder-cost: 14   maxlim: 14   bits: 4/4
c ---[ 228]---> Adder-cost: 30   maxlim: 17   bits: 5/5
c ---[ 226]---> Adder-cost: 26   maxlim: 20   bits: 5/5
c ---[ 224]---> Adder-cost: 212   maxlim: 114   bits: 7/7
c ---[ 222]---> Adder-cost: 66   maxlim: 36   bits: 6/6
c ---[ 220]---> Adder-cost: 142   maxlim: 122   bits: 7/7
c ---[ 218]---> Adder-cost: 352   maxlim: 193   bits: 8/8
c ---[ 216]---> Adder-cost: 276   maxlim: 193   bits: 8/8
c ---[ 214]---> Adder-cost: 66   maxlim: 37   bits: 6/6
c ---[ 212]---> Adder-cost: 78   maxlim: 46   bits: 6/6
c ---[ 208]---> Adder-cost: 124   maxlim: 66   bits: 7/7
c ---[ 206]---> Adder-cost: 140   maxlim: 73   bits: 7/7
c ---[ 204]---> Adder-cost: 116   maxlim: 64   bits: 7/7
c ---[ 202]---> Adder-cost: 104   maxlim: 59   bits: 6/6
c ---[ 200]---> Adder-cost: 68   maxlim: 41   bits: 6/6
c ---[ 198]---> Adder-cost: 94   maxlim: 56   bits: 6/6
c ---[ 196]---> Adder-cost: 110   maxlim: 62   bits: 6/6
c ---[ 194]---> Adder-cost: 112   maxlim: 68   bits: 7/7
c ---[ 192]---> Adder-cost: 224   maxlim: 122   bits: 7/7
c ---[ 190]---> Adder-cost: 182   maxlim: 121   bits: 7/7
c ---[ 188]---> Adder-cost: 138   maxlim: 75   bits: 7/7
c ---[ 186]---> Adder-cost: 100   maxlim: 58   bits: 6/6
c ---[ 184]---> Adder-cost: 132   maxlim: 87   bits: 7/7
c ---[ 182]---> Adder-cost: 224   maxlim: 126   bits: 7/7
c ---[ 180]---> Adder-cost: 120   maxlim: 105   bits: 7/7
c ---[ 178]---> Adder-cost: 82   maxlim: 46   bits: 6/6
c ---[ 176]---> Adder-cost: 80   maxlim: 46   bits: 6/6
c ---[ 174]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[ 172]---> Adder-cost: 72   maxlim: 50   bits: 6/6
c ---[ 170]---> Adder-cost: 112   maxlim: 63   bits: 7/6
c ---[ 168]---> Adder-cost: 82   maxlim: 45   bits: 6/6
c ---[ 166]---> Adder-cost: 62   maxlim: 36   bits: 6/6
c ---[ 164]---> Adder-cost: 124   maxlim: 64   bits: 7/7
c ---[ 162]---> Adder-cost: 104   maxlim: 68   bits: 7/7
c ---[ 160]---> Adder-cost: 146   maxlim: 81   bits: 7/7
c ---[ 158]---> Adder-cost: 138   maxlim: 82   bits: 7/7
c ---[ 156]---> Adder-cost: 84   maxlim: 49   bits: 6/6
c ---[ 154]---> Adder-cost: 386   maxlim: 219   bits: 8/8
c ---[ 152]---> Adder-cost: 302   maxlim: 171   bits: 8/8
c ---[ 150]---> Adder-cost: 212   maxlim: 172   bits: 8/8
c ---[ 148]---> Adder-cost: 378   maxlim: 247   bits: 8/8
c ---[ 146]---> Adder-cost: 456   maxlim: 245   bits: 8/8
c ---[ 144]---> Adder-cost: 376   maxlim: 247   bits: 8/8
c ---[ 142]---> Adder-cost: 412   maxlim: 229   bits: 8/8
c ---[ 140]---> Adder-cost: 366   maxlim: 234   bits: 8/8
c ---[ 138]---> Adder-cost: 400   maxlim: 211   bits: 8/8
c ---[ 136]---> Adder-cost: 324   maxlim: 210   bits: 8/8
c ---[ 134]---> Adder-cost: 132   maxlim: 73   bits: 7/7
c ---[ 132]---> Adder-cost: 400   maxlim: 217   bits: 8/8
c ---[ 130]---> Adder-cost: 338   maxlim: 204   bits: 8/8
c ---[ 128]---> Adder-cost: 316   maxlim: 207   bits: 8/8
c ---[ 126]---> Adder-cost: 632   maxlim: 337   bits: 9/9
c ---[ 124]---> Adder-cost: 612   maxlim: 367   bits: 9/9
c ---[ 122]---> Adder-cost: 364   maxlim: 194   bits: 8/8
c ---[ 120]---> Adder-cost: 258   maxlim: 152   bits: 8/8
c ---[ 118]---> Adder-cost: 308   maxlim: 174   bits: 8/8
c ---[ 116]---> Adder-cost: 334   maxlim: 185   bits: 8/8
c ---[ 114]---> Adder-cost: 290   maxlim: 203   bits: 8/8
c ---[ 112]---> Adder-cost: 94   maxlim: 67   bits: 7/7
c ---[ 110]---> Adder-cost: 280   maxlim: 157   bits: 8/8
c ---[ 108]---> Adder-cost: 242   maxlim: 151   bits: 8/8
c ---[ 106]---> Adder-cost: 234   maxlim: 129   bits: 8/8
c ---[ 104]---> Adder-cost: 222   maxlim: 127   bits: 8/7
c ---[ 102]---> Adder-cost: 290   maxlim: 160   bits: 8/8
c ---[ 100]---> Adder-cost: 192   maxlim: 169   bits: 8/8
c ---[  98]---> Adder-cost: 252   maxlim: 174   bits: 8/8
c ---[  96]---> Adder-cost: 216   maxlim: 122   bits: 7/7
c ---[  94]---> Adder-cost: 204   maxlim: 124   bits: 7/7
c ---[  92]---> Adder-cost: 228   maxlim: 120   bits: 7/7
c ---[  90]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[  88]---> Adder-cost: 88   maxlim: 48   bits: 6/6
c ---[  86]---> Adder-cost: 0   maxlim: 120   bits: 7/7
c ---[  84]---> Adder-cost: 140   maxlim: 75   bits: 7/7
c ---[  80]---> Adder-cost: 84   maxlim: 58   bits: 6/6
c ---[  78]---> Adder-cost: 110   maxlim: 74   bits: 7/7
c ---[  76]---> Adder-cost: 94   maxlim: 55   bits: 6/6
c ---[  74]---> Adder-cost: 68   maxlim: 50   bits: 6/6
c ---[  72]---> Adder-cost: 82   maxlim: 58   bits: 6/6
c ---[  70]---> Adder-cost: 74   maxlim: 40   bits: 6/6
c ---[  68]---> Adder-cost: 68   maxlim: 43   bits: 6/6
c ---[  66]---> Adder-cost: 156   maxlim: 85   bits: 7/7
c ---[  64]---> Adder-cost: 142   maxlim: 76   bits: 7/7
c ---[  62]---> Adder-cost: 134   maxlim: 76   bits: 7/7
c ---[  60]---> Adder-cost: 160   maxlim: 89   bits: 7/7
c ---[  58]---> Adder-cost: 140   maxlim: 88   bits: 7/7
c ---[  56]---> Adder-cost: 120   maxlim: 75   bits: 7/7
c ---[  54]---> Adder-cost: 140   maxlim: 79   bits: 7/7
c ---[  52]---> Adder-cost: 196   maxlim: 108   bits: 7/7
c ---[  50]---> Adder-cost: 162   maxlim: 108   bits: 7/7
c ---[  48]---> Adder-cost: 208   maxlim: 118   bits: 7/7
c ---[  46]---> Adder-cost: 146   maxlim: 83   bits: 7/7
c ---[  44]---> Adder-cost: 138   maxlim: 96   bits: 7/7
c ---[  42]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[  40]---> Adder-cost: 54   maxlim: 36   bits: 6/6
c ---[  38]---> Adder-cost: 134   maxlim: 71   bits: 7/7
c ---[  36]---> Adder-cost: 86   maxlim: 70   bits: 7/7
c ---[  34]---> Adder-cost: 136   maxlim: 77   bits: 7/7
c ---[  32]---> Adder-cost: 86   maxlim: 67   bits: 7/7
c ---[  30]---> Adder-cost: 44   maxlim: 24   bits: 5/5
c ---[  28]---> Adder-cost: 36   maxlim: 24   bits: 5/5
c ---[  26]---> Adder-cost: 44   maxlim: 25   bits: 5/5
c ---[  24]---> Adder-cost: 60   maxlim: 33   bits: 6/6
c ---[  22]---> Adder-cost: 96   maxlim: 55   bits: 6/6
c ---[  20]---> Adder-cost: 0   maxlim: 13   bits: 4/4
c ---[  16]---> Adder-cost: 48   maxlim: 30   bits: 5/5
c ---[  12]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  10]---> Adder-cost: 22   maxlim: 14   bits: 4/4
c ---[   8]---> Adder-cost: 16   maxlim: 12   bits: 4/4
c ---[   4]---> Adder-cost: 70   maxlim: 41   bits: 6/6
c ---[   2]---> Adder-cost: 204   maxlim: 117   bits: 7/7
c ---[   0]---> Adder-cost: 222   maxlim: 143   bits: 8/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  794675  2828045 |  264891       0        0     nan |  0.000 % |
c |       100 |  793759  2824871 |  291380       9       31     3.4 |  8.620 % |
c |       250 |  793026  2822328 |  320518      81      261     3.2 |  8.715 % |
c |       476 |  791571  2817281 |  352569     152      514     3.4 |  8.905 % |
c |       813 |  789321  2809431 |  387826     247      857     3.5 |  9.198 % |
c |      1319 |  786402  2799332 |  426609     458     1693     3.7 |  9.583 % |
c |      2078 |  781592  2782646 |  469270     695     3032     4.4 | 10.206 % |
c |      3219 |  775699  2762157 |  516197    1212     5629     4.6 | 10.971 % |
c |      4928 |  768025  2735479 |  567817    2021     9667     4.8 | 11.946 % |
c |      7490 |  760382  2708766 |  624599    3701    18343     5.0 | 12.919 % |
c |     11334 |  751404  2676984 |  687059    6433    36707     5.7 | 14.045 % |
c |     17100 |  735816  2622006 |  755764   10224    60155     5.9 | 15.999 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.95 0.94 2/54 21397
Raw data (stat): 21397 (runsolver) R 21396 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 488387512 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.93 0.95 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 14588 0 0 0 959 38 0 0 25 0 1 0 488387512 71503872 14219 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17457 14219 603 41 0 17416 0
vsize: 69828
[startup+20.001 s]
Raw data (loadavg): 0.94 0.96 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 14597 0 0 0 1959 38 0 0 25 0 1 0 488387512 71503872 14228 4294967295 134512640 134672761 3221224544 3221223752 134561962 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17457 14228 603 41 0 17416 0
vsize: 69828
[startup+30.0013 s]
Raw data (loadavg): 0.95 0.96 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 14598 0 0 0 2959 38 0 0 25 0 1 0 488387512 71503872 14229 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17457 14229 603 41 0 17416 0
vsize: 69828
[startup+40.0014 s]
Raw data (loadavg): 0.95 0.96 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 14599 0 0 0 3959 38 0 0 25 0 1 0 488387512 71503872 14230 4294967295 134512640 134672761 3221224544 3221223712 134561415 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17457 14230 603 41 0 17416 0
vsize: 69828
[startup+50.001 s]
Raw data (loadavg): 0.96 0.96 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 14599 0 0 0 4959 38 0 0 25 0 1 0 488387512 71503872 14230 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17457 14230 603 41 0 17416 0
vsize: 69828
[startup+60.0012 s]
Raw data (loadavg): 0.97 0.96 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 14611 0 0 0 5959 39 0 0 25 0 1 0 488387512 71667712 14242 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17497 14242 603 41 0 17456 0
vsize: 69988
[startup+70.0013 s]
Raw data (loadavg): 0.97 0.96 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 14632 0 0 0 6959 39 0 0 25 0 1 0 488387512 71667712 14263 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17497 14263 603 41 0 17456 0
vsize: 69988
[startup+80.001 s]
Raw data (loadavg): 0.98 0.96 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 14661 0 0 0 7959 39 0 0 25 0 1 0 488387512 71802880 14292 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17530 14292 603 41 0 17489 0
vsize: 70120
[startup+90.0012 s]
Raw data (loadavg): 0.98 0.96 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 14684 0 0 0 8959 39 0 0 25 0 1 0 488387512 71938048 14315 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17563 14315 603 41 0 17522 0
vsize: 70252
[startup+100 s]
Raw data (loadavg): 0.98 0.96 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 14701 0 0 0 9959 39 0 0 25 0 1 0 488387512 71938048 14332 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17563 14332 603 41 0 17522 0
vsize: 70252
[startup+110.001 s]
Raw data (loadavg): 0.98 0.96 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 14721 0 0 0 10959 39 0 0 25 0 1 0 488387512 72073216 14352 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 14352 603 41 0 17555 0
vsize: 70384
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 14744 0 0 0 11960 39 0 0 25 0 1 0 488387512 72073216 14375 4294967295 134512640 134672761 3221224544 3221223716 134556685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 14375 603 41 0 17555 0
vsize: 70384
[startup+130.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 14763 0 0 0 12959 39 0 0 25 0 1 0 488387512 72208384 14394 4294967295 134512640 134672761 3221224544 3221223716 134556664 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17629 14394 603 41 0 17588 0
vsize: 70516
[startup+140.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 14778 0 0 0 13959 40 0 0 25 0 1 0 488387512 72343552 14409 4294967295 134512640 134672761 3221224544 3221223724 134556674 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17662 14409 603 41 0 17621 0
vsize: 70648
[startup+150.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 14801 0 0 0 14959 40 0 0 25 0 1 0 488387512 72343552 14432 4294967295 134512640 134672761 3221224544 3221223536 1075350401 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17662 14432 603 41 0 17621 0
vsize: 70648
[startup+160.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 14820 0 0 0 15959 40 0 0 25 0 1 0 488387512 72478720 14451 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17695 14451 603 41 0 17654 0
vsize: 70780
[startup+170.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 14840 0 0 0 16960 40 0 0 25 0 1 0 488387512 72626176 14471 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17731 14471 603 41 0 17690 0
vsize: 70924
[startup+180.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 14851 0 0 0 17960 40 0 0 25 0 1 0 488387512 72626176 14482 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17731 14482 603 41 0 17690 0
vsize: 70924
[startup+190.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 14867 0 0 0 18960 40 0 0 25 0 1 0 488387512 72626176 14498 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17731 14498 603 41 0 17690 0
vsize: 70924
[startup+200.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 14880 0 0 0 19960 40 0 0 25 0 1 0 488387512 72761344 14511 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17764 14511 603 41 0 17723 0
vsize: 71056
[startup+210.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 14890 0 0 0 20961 40 0 0 25 0 1 0 488387512 72761344 14521 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17764 14521 603 41 0 17723 0
vsize: 71056
[startup+220.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 14909 0 0 0 21962 40 0 0 25 0 1 0 488387512 72761344 14540 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17764 14540 603 41 0 17723 0
vsize: 71056
[startup+230.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 14922 0 0 0 22962 40 0 0 25 0 1 0 488387512 72896512 14553 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17797 14553 603 41 0 17756 0
vsize: 71188
[startup+240.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 14943 0 0 0 23962 40 0 0 25 0 1 0 488387512 72896512 14574 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17797 14574 603 41 0 17756 0
vsize: 71188
[startup+250.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 14952 0 0 0 24962 40 0 0 25 0 1 0 488387512 73031680 14583 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17830 14583 603 41 0 17789 0
vsize: 71320
[startup+260.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 14969 0 0 0 25962 40 0 0 25 0 1 0 488387512 73031680 14600 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17830 14600 603 41 0 17789 0
vsize: 71320
[startup+270.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 14982 0 0 0 26962 41 0 0 25 0 1 0 488387512 73166848 14613 4294967295 134512640 134672761 3221224544 3221223760 134557501 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17863 14613 603 41 0 17822 0
vsize: 71452
[startup+280.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 14992 0 0 0 27962 41 0 0 25 0 1 0 488387512 73166848 14623 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17863 14623 603 41 0 17822 0
vsize: 71452
[startup+290.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15007 0 0 0 28962 41 0 0 25 0 1 0 488387512 73166848 14638 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17863 14638 603 41 0 17822 0
vsize: 71452
[startup+300.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15015 0 0 0 29963 41 0 0 25 0 1 0 488387512 73302016 14646 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17896 14646 603 41 0 17855 0
vsize: 71584
[startup+310.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15021 0 0 0 30963 41 0 0 25 0 1 0 488387512 73302016 14652 4294967295 134512640 134672761 3221224544 3221223784 134561421 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17896 14652 603 41 0 17855 0
vsize: 71584
[startup+320.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15033 0 0 0 31963 41 0 0 25 0 1 0 488387512 73302016 14664 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17896 14664 603 41 0 17855 0
vsize: 71584
[startup+330.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15039 0 0 0 32963 41 0 0 25 0 1 0 488387512 73302016 14670 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17896 14670 603 41 0 17855 0
vsize: 71584
[startup+340.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15048 0 0 0 33963 41 0 0 25 0 1 0 488387512 73302016 14679 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17896 14679 603 41 0 17855 0
vsize: 71584
[startup+350.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15052 0 0 0 34963 41 0 0 25 0 1 0 488387512 73437184 14683 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17929 14683 603 41 0 17888 0
vsize: 71716
[startup+360.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15056 0 0 0 35964 41 0 0 25 0 1 0 488387512 73437184 14687 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17929 14687 603 41 0 17888 0
vsize: 71716
[startup+370.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15072 0 0 0 36964 41 0 0 25 0 1 0 488387512 73437184 14703 4294967295 134512640 134672761 3221224544 3221223732 134556676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17929 14703 603 41 0 17888 0
vsize: 71716
[startup+380.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15080 0 0 0 37964 41 0 0 25 0 1 0 488387512 73437184 14711 4294967295 134512640 134672761 3221224544 3221223668 134566031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17929 14711 603 41 0 17888 0
vsize: 71716
[startup+390.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15087 0 0 0 38964 41 0 0 25 0 1 0 488387512 73437184 14718 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17929 14718 603 41 0 17888 0
vsize: 71716
[startup+400.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15088 0 0 0 39964 41 0 0 25 0 1 0 488387512 73572352 14719 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17962 14719 603 41 0 17921 0
vsize: 71848
[startup+410.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15094 0 0 0 40964 41 0 0 25 0 1 0 488387512 73572352 14725 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17962 14725 603 41 0 17921 0
vsize: 71848
[startup+420.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15101 0 0 0 41965 41 0 0 25 0 1 0 488387512 73572352 14732 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17962 14732 603 41 0 17921 0
vsize: 71848
[startup+430.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15107 0 0 0 42965 41 0 0 25 0 1 0 488387512 73572352 14738 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17962 14738 603 41 0 17921 0
vsize: 71848
[startup+440.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15112 0 0 0 43965 41 0 0 25 0 1 0 488387512 73572352 14743 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17962 14743 603 41 0 17921 0
vsize: 71848
[startup+450.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15117 0 0 0 44965 41 0 0 25 0 1 0 488387512 73572352 14748 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17962 14748 603 41 0 17921 0
vsize: 71848
[startup+460.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15121 0 0 0 45965 41 0 0 25 0 1 0 488387512 73572352 14752 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17962 14752 603 41 0 17921 0
vsize: 71848
[startup+470.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15124 0 0 0 46965 41 0 0 25 0 1 0 488387512 73572352 14755 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17962 14755 603 41 0 17921 0
vsize: 71848
[startup+480.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15128 0 0 0 47966 41 0 0 25 0 1 0 488387512 73707520 14759 4294967295 134512640 134672761 3221224544 3221223736 134556585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17995 14759 603 41 0 17954 0
vsize: 71980
[startup+490.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15130 0 0 0 48966 41 0 0 25 0 1 0 488387512 73707520 14761 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17995 14761 603 41 0 17954 0
vsize: 71980
[startup+500.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15132 0 0 0 49966 41 0 0 25 0 1 0 488387512 73707520 14763 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17995 14763 603 41 0 17954 0
vsize: 71980
[startup+510.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15132 0 0 0 50966 41 0 0 25 0 1 0 488387512 73707520 14763 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17995 14763 603 41 0 17954 0
vsize: 71980
[startup+520.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15135 0 0 0 51966 41 0 0 25 0 1 0 488387512 73707520 14766 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17995 14766 603 41 0 17954 0
vsize: 71980
[startup+530.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15136 0 0 0 52966 41 0 0 25 0 1 0 488387512 73707520 14767 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17995 14767 603 41 0 17954 0
vsize: 71980
[startup+540.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15142 0 0 0 53966 41 0 0 25 0 1 0 488387512 73707520 14773 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17995 14773 603 41 0 17954 0
vsize: 71980
[startup+550.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15142 0 0 0 54966 41 0 0 25 0 1 0 488387512 73707520 14773 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17995 14773 603 41 0 17954 0
vsize: 71980
[startup+560.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15142 0 0 0 55966 41 0 0 25 0 1 0 488387512 73707520 14773 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17995 14773 603 41 0 17954 0
vsize: 71980
[startup+570.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15142 0 0 0 56966 41 0 0 25 0 1 0 488387512 73707520 14773 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17995 14773 603 41 0 17954 0
vsize: 71980
[startup+580.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15143 0 0 0 57966 41 0 0 25 0 1 0 488387512 73707520 14774 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17995 14774 603 41 0 17954 0
vsize: 71980
[startup+590.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15145 0 0 0 58967 41 0 0 25 0 1 0 488387512 73707520 14776 4294967295 134512640 134672761 3221224544 3221223668 134566068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17995 14776 603 41 0 17954 0
vsize: 71980
[startup+600.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15146 0 0 0 59967 41 0 0 25 0 1 0 488387512 73707520 14777 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17995 14777 603 41 0 17954 0
vsize: 71980
[startup+610.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15146 0 0 0 60967 41 0 0 25 0 1 0 488387512 73707520 14777 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17995 14777 603 41 0 17954 0
vsize: 71980
[startup+620.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15147 0 0 0 61967 41 0 0 25 0 1 0 488387512 73707520 14778 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17995 14778 603 41 0 17954 0
vsize: 71980
[startup+630.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15149 0 0 0 62967 42 0 0 25 0 1 0 488387512 73707520 14780 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17995 14780 603 41 0 17954 0
vsize: 71980
[startup+640.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15151 0 0 0 63968 42 0 0 25 0 1 0 488387512 73707520 14782 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17995 14782 603 41 0 17954 0
vsize: 71980
[startup+650.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15153 0 0 0 64968 42 0 0 25 0 1 0 488387512 73707520 14784 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17995 14784 603 41 0 17954 0
vsize: 71980
[startup+660.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15153 0 0 0 65968 42 0 0 25 0 1 0 488387512 73707520 14784 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17995 14784 603 41 0 17954 0
vsize: 71980
[startup+670.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15154 0 0 0 66968 42 0 0 25 0 1 0 488387512 73707520 14785 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17995 14785 603 41 0 17954 0
vsize: 71980
[startup+680.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15156 0 0 0 67968 42 0 0 25 0 1 0 488387512 73707520 14787 4294967295 134512640 134672761 3221224544 3221223728 134556589 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17995 14787 603 41 0 17954 0
vsize: 71980
[startup+690.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15159 0 0 0 68968 42 0 0 25 0 1 0 488387512 73707520 14790 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17995 14790 603 41 0 17954 0
vsize: 71980
[startup+700.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15160 0 0 0 69968 42 0 0 25 0 1 0 488387512 73707520 14791 4294967295 134512640 134672761 3221224544 3221223728 134556589 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17995 14791 603 41 0 17954 0
vsize: 71980
[startup+710.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15161 0 0 0 70968 42 0 0 25 0 1 0 488387512 73707520 14792 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17995 14792 603 41 0 17954 0
vsize: 71980
[startup+720.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15162 0 0 0 71968 42 0 0 25 0 1 0 488387512 73707520 14793 4294967295 134512640 134672761 3221224544 3221223668 134566031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17995 14793 603 41 0 17954 0
vsize: 71980
[startup+730.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15167 0 0 0 72968 42 0 0 25 0 1 0 488387512 73842688 14798 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18028 14798 603 41 0 17987 0
vsize: 72112
[startup+740.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15168 0 0 0 73967 42 0 0 25 0 1 0 488387512 73842688 14799 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14799 603 41 0 17987 0
vsize: 72112
[startup+750.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15168 0 0 0 74967 42 0 0 25 0 1 0 488387512 73842688 14799 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14799 603 41 0 17987 0
vsize: 72112
[startup+760.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15168 0 0 0 75967 42 0 0 25 0 1 0 488387512 73842688 14799 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14799 603 41 0 17987 0
vsize: 72112
[startup+770.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15169 0 0 0 76967 42 0 0 25 0 1 0 488387512 73842688 14800 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14800 603 41 0 17987 0
vsize: 72112
[startup+780.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15169 0 0 0 77968 42 0 0 25 0 1 0 488387512 73842688 14800 4294967295 134512640 134672761 3221224544 3221223728 134556675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14800 603 41 0 17987 0
vsize: 72112
[startup+790.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15170 0 0 0 78968 42 0 0 25 0 1 0 488387512 73842688 14801 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14801 603 41 0 17987 0
vsize: 72112
[startup+800.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15171 0 0 0 79968 42 0 0 25 0 1 0 488387512 73842688 14802 4294967295 134512640 134672761 3221224544 3221223716 134556685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14802 603 41 0 17987 0
vsize: 72112
[startup+810.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15171 0 0 0 80968 42 0 0 25 0 1 0 488387512 73842688 14802 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14802 603 41 0 17987 0
vsize: 72112
[startup+820.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15171 0 0 0 81968 42 0 0 25 0 1 0 488387512 73842688 14802 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14802 603 41 0 17987 0
vsize: 72112
[startup+830.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15171 0 0 0 82968 42 0 0 25 0 1 0 488387512 73842688 14802 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14802 603 41 0 17987 0
vsize: 72112
[startup+840.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15173 0 0 0 83969 42 0 0 25 0 1 0 488387512 73842688 14804 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14804 603 41 0 17987 0
vsize: 72112
[startup+850.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15174 0 0 0 84969 42 0 0 25 0 1 0 488387512 73842688 14805 4294967295 134512640 134672761 3221224544 3221223696 134565101 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14805 603 41 0 17987 0
vsize: 72112
[startup+860.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15174 0 0 0 85969 42 0 0 25 0 1 0 488387512 73842688 14805 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14805 603 41 0 17987 0
vsize: 72112
[startup+870.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15179 0 0 0 86969 42 0 0 25 0 1 0 488387512 73842688 14810 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18028 14810 603 41 0 17987 0
vsize: 72112
[startup+880.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15179 0 0 0 87969 42 0 0 25 0 1 0 488387512 73842688 14810 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14810 603 41 0 17987 0
vsize: 72112
[startup+890.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15179 0 0 0 88969 42 0 0 25 0 1 0 488387512 73842688 14810 4294967295 134512640 134672761 3221224544 3221223696 134564780 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14810 603 41 0 17987 0
vsize: 72112
[startup+900.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15179 0 0 0 89969 42 0 0 25 0 1 0 488387512 73842688 14810 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14810 603 41 0 17987 0
vsize: 72112
[startup+910.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15180 0 0 0 90969 42 0 0 25 0 1 0 488387512 73842688 14811 4294967295 134512640 134672761 3221224544 3221223728 134556589 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14811 603 41 0 17987 0
vsize: 72112
[startup+920.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15182 0 0 0 91969 42 0 0 25 0 1 0 488387512 73842688 14813 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14813 603 41 0 17987 0
vsize: 72112
[startup+930.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15183 0 0 0 92969 42 0 0 25 0 1 0 488387512 73842688 14814 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14814 603 41 0 17987 0
vsize: 72112
[startup+940.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15183 0 0 0 93970 42 0 0 25 0 1 0 488387512 73842688 14814 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14814 603 41 0 17987 0
vsize: 72112
[startup+950.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15184 0 0 0 94970 42 0 0 25 0 1 0 488387512 73842688 14815 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14815 603 41 0 17987 0
vsize: 72112
[startup+960.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15185 0 0 0 95970 42 0 0 25 0 1 0 488387512 73842688 14816 4294967295 134512640 134672761 3221224544 3221223712 134564457 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14816 603 41 0 17987 0
vsize: 72112
[startup+970.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15185 0 0 0 96970 42 0 0 25 0 1 0 488387512 73842688 14816 4294967295 134512640 134672761 3221224544 3221223760 134561990 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14816 603 41 0 17987 0
vsize: 72112
[startup+980.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15185 0 0 0 97970 42 0 0 25 0 1 0 488387512 73842688 14816 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14816 603 41 0 17987 0
vsize: 72112
[startup+990.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15185 0 0 0 98971 42 0 0 25 0 1 0 488387512 73842688 14816 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14816 603 41 0 17987 0
vsize: 72112
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15185 0 0 0 99971 42 0 0 25 0 1 0 488387512 73842688 14816 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14816 603 41 0 17987 0
vsize: 72112
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15195 0 0 0 100971 42 0 0 25 0 1 0 488387512 73842688 14826 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14826 603 41 0 17987 0
vsize: 72112
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15195 0 0 0 101971 42 0 0 25 0 1 0 488387512 73842688 14826 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14826 603 41 0 17987 0
vsize: 72112
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15195 0 0 0 102971 42 0 0 25 0 1 0 488387512 73842688 14826 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14826 603 41 0 17987 0
vsize: 72112
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15195 0 0 0 103971 42 0 0 25 0 1 0 488387512 73842688 14826 4294967295 134512640 134672761 3221224544 3221223740 134556678 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14826 603 41 0 17987 0
vsize: 72112
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15195 0 0 0 104972 42 0 0 25 0 1 0 488387512 73842688 14826 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14826 603 41 0 17987 0
vsize: 72112
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21397
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15195 0 0 0 105972 42 0 0 25 0 1 0 488387512 73842688 14826 4294967295 134512640 134672761 3221224544 3221223728 134556589 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14826 603 41 0 17987 0
vsize: 72112
[startup+1070.02 s]
Raw data (loadavg): 1.07 0.99 0.94 2/54 21450
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15195 0 0 0 106972 42 0 0 25 0 1 0 488387512 73842688 14826 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14826 603 41 0 17987 0
vsize: 72112
[startup+1080.02 s]
Raw data (loadavg): 1.06 0.99 0.94 2/54 21450
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15195 0 0 0 107971 43 0 0 25 0 1 0 488387512 73842688 14826 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14826 603 41 0 17987 0
vsize: 72112
[startup+1090.02 s]
Raw data (loadavg): 1.05 0.99 0.94 2/54 21450
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15195 0 0 0 108971 43 0 0 25 0 1 0 488387512 73842688 14826 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14826 603 41 0 17987 0
vsize: 72112
[startup+1100.02 s]
Raw data (loadavg): 1.04 0.99 0.94 2/54 21450
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15196 0 0 0 109971 43 0 0 25 0 1 0 488387512 73842688 14827 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14827 603 41 0 17987 0
vsize: 72112
[startup+1110.02 s]
Raw data (loadavg): 1.04 0.99 0.94 2/54 21450
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15196 0 0 0 110971 44 0 0 25 0 1 0 488387512 73842688 14827 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14827 603 41 0 17987 0
vsize: 72112
[startup+1120.02 s]
Raw data (loadavg): 1.03 0.99 0.94 2/54 21450
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15197 0 0 0 111971 44 0 0 25 0 1 0 488387512 73842688 14828 4294967295 134512640 134672761 3221224544 3221223728 134556589 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14828 603 41 0 17987 0
vsize: 72112
[startup+1130.02 s]
Raw data (loadavg): 1.03 0.99 0.94 2/54 21450
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15197 0 0 0 112971 44 0 0 25 0 1 0 488387512 73842688 14828 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14828 603 41 0 17987 0
vsize: 72112
[startup+1140.02 s]
Raw data (loadavg): 1.02 0.99 0.94 2/54 21452
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15198 0 0 0 113971 44 0 0 25 0 1 0 488387512 73842688 14829 4294967295 134512640 134672761 3221224544 3221223696 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14829 603 41 0 17987 0
vsize: 72112
[startup+1150.02 s]
Raw data (loadavg): 1.02 0.99 0.94 2/54 21452
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15199 0 0 0 114971 44 0 0 25 0 1 0 488387512 73842688 14830 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14830 603 41 0 17987 0
vsize: 72112
[startup+1160.02 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 21452
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15202 0 0 0 115970 45 0 0 25 0 1 0 488387512 73842688 14833 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14833 603 41 0 17987 0
vsize: 72112
[startup+1170.02 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 21452
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15204 0 0 0 116971 45 0 0 25 0 1 0 488387512 73842688 14835 4294967295 134512640 134672761 3221224544 3221223712 134564436 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14835 603 41 0 17987 0
vsize: 72112
[startup+1180.02 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 21452
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15204 0 0 0 117970 45 0 0 25 0 1 0 488387512 73842688 14835 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14835 603 41 0 17987 0
vsize: 72112
[startup+1190.02 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 21452
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15204 0 0 0 118970 46 0 0 25 0 1 0 488387512 73842688 14835 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14835 603 41 0 17987 0
vsize: 72112
[startup+1200.02 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 21452
Raw data (stat): 21397 (minisat+) R 21396 30701 30700 0 -1 0 15205 0 0 0 119970 46 0 0 25 0 1 0 488387512 73842688 14836 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14836 603 41 0 17987 0
vsize: 72112
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.01 0.99 0.94 1/54 21452
Raw data (stat): 21397 (minisat+) Z 21396 30701 30700 0 -1 12 15207 0 0 0 119970 49 0 0 25 0 1 0 488387512 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.05
CPU time (s): 1200.2
CPU user time (s): 1199.71
CPU system time (s): 0.491925
CPU usage (%): 100.012
Max. virtual memory (Kb): 72112
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####