PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-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	1185.16
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 21854

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        377096 kB
Buffers:         24900 kB
Cached:         608312 kB
SwapCached:        548 kB
Active:          93336 kB
Inactive:       541928 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        376844 kB
SwapTotal:     2097136 kB
SwapFree:      2095732 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5104 kB
Slab:            16652 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 01:38:47 (client local time) WITH STATUS 0 IN 1200.2 SECONDS
stats: 12438 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.68 0.92 0.90 2/54 19474
Raw data (stat): 19474 (runsolver) R 19473 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 549703100 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.0007 s]
Raw data (loadavg): 0.72 0.92 0.90 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 14588 0 0 0 962 37 0 0 25 0 1 0 549703100 71503872 14219 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17457 14219 603 41 0 17416 0
vsize: 69828
[startup+20.0004 s]
Raw data (loadavg): 0.77 0.92 0.90 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 14597 0 0 0 1962 37 0 0 25 0 1 0 549703100 71503872 14228 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17457 14228 603 41 0 17416 0
vsize: 69828
[startup+30.001 s]
Raw data (loadavg): 0.80 0.93 0.90 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 14598 0 0 0 2961 37 0 0 25 0 1 0 549703100 71503872 14229 4294967295 134512640 134672761 3221224544 3221223716 134556688 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.0006 s]
Raw data (loadavg): 0.83 0.93 0.90 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 14599 0 0 0 3961 37 0 0 25 0 1 0 549703100 71503872 14230 4294967295 134512640 134672761 3221224544 3221223716 134556649 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.0003 s]
Raw data (loadavg): 0.86 0.93 0.90 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 14599 0 0 0 4962 37 0 0 25 0 1 0 549703100 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 s]
Raw data (loadavg): 0.88 0.93 0.90 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 14611 0 0 0 5962 37 0 0 25 0 1 0 549703100 71667712 14242 4294967295 134512640 134672761 3221224544 3221223748 134561964 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.0006 s]
Raw data (loadavg): 0.90 0.93 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 14632 0 0 0 6960 37 0 0 25 0 1 0 549703100 71667712 14263 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17497 14263 603 41 0 17456 0
vsize: 69988
[startup+80.0002 s]
Raw data (loadavg): 0.91 0.93 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 14657 0 0 0 7960 38 0 0 25 0 1 0 549703100 71802880 14288 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17530 14288 603 41 0 17489 0
vsize: 70120
[startup+89.9998 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 14681 0 0 0 8959 38 0 0 25 0 1 0 549703100 71938048 14312 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17563 14312 603 41 0 17522 0
vsize: 70252
[startup+99.9994 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 14697 0 0 0 9960 38 0 0 25 0 1 0 549703100 71938048 14328 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17563 14328 603 41 0 17522 0
vsize: 70252
[startup+110 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 14717 0 0 0 10959 38 0 0 25 0 1 0 549703100 72073216 14348 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 14348 603 41 0 17555 0
vsize: 70384
[startup+120.001 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 14744 0 0 0 11959 38 0 0 25 0 1 0 549703100 72073216 14375 4294967295 134512640 134672761 3221224544 3221223716 134556634 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 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 14761 0 0 0 12959 38 0 0 25 0 1 0 549703100 72208384 14392 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17629 14392 603 41 0 17588 0
vsize: 70516
[startup+140 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 14777 0 0 0 13960 38 0 0 25 0 1 0 549703100 72208384 14408 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17629 14408 603 41 0 17588 0
vsize: 70516
[startup+150 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 14797 0 0 0 14960 38 0 0 25 0 1 0 549703100 72343552 14428 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17662 14428 603 41 0 17621 0
vsize: 70648
[startup+160 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 14816 0 0 0 15960 39 0 0 25 0 1 0 549703100 72478720 14447 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17695 14447 603 41 0 17654 0
vsize: 70780
[startup+170 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 14840 0 0 0 16960 39 0 0 25 0 1 0 549703100 72626176 14471 4294967295 134512640 134672761 3221224544 3221223712 134560869 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 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 14850 0 0 0 17960 39 0 0 25 0 1 0 549703100 72626176 14481 4294967295 134512640 134672761 3221224544 3221223740 134556678 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17731 14481 603 41 0 17690 0
vsize: 70924
[startup+190.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 14866 0 0 0 18960 39 0 0 25 0 1 0 549703100 72626176 14497 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17731 14497 603 41 0 17690 0
vsize: 70924
[startup+200 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 14876 0 0 0 19960 39 0 0 25 0 1 0 549703100 72761344 14507 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17764 14507 603 41 0 17723 0
vsize: 71056
[startup+210 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 14888 0 0 0 20960 39 0 0 25 0 1 0 549703100 72761344 14519 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17764 14519 603 41 0 17723 0
vsize: 71056
[startup+220 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 14909 0 0 0 21960 39 0 0 25 0 1 0 549703100 72761344 14540 4294967295 134512640 134672761 3221224544 3221223716 134556634 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 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 14918 0 0 0 22960 39 0 0 25 0 1 0 549703100 72896512 14549 4294967295 134512640 134672761 3221224544 3221223696 134565101 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17797 14549 603 41 0 17756 0
vsize: 71188
[startup+240 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 14939 0 0 0 23960 40 0 0 25 0 1 0 549703100 72896512 14570 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17797 14570 603 41 0 17756 0
vsize: 71188
[startup+250 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 14949 0 0 0 24960 40 0 0 25 0 1 0 549703100 73031680 14580 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17830 14580 603 41 0 17789 0
vsize: 71320
[startup+260 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 14964 0 0 0 25961 40 0 0 25 0 1 0 549703100 73031680 14595 4294967295 134512640 134672761 3221224544 3221223716 134556606 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17830 14595 603 41 0 17789 0
vsize: 71320
[startup+270 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 14980 0 0 0 26961 40 0 0 25 0 1 0 549703100 73166848 14611 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17863 14611 603 41 0 17822 0
vsize: 71452
[startup+279.999 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 14989 0 0 0 27961 40 0 0 25 0 1 0 549703100 73166848 14620 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17863 14620 603 41 0 17822 0
vsize: 71452
[startup+290 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15002 0 0 0 28961 40 0 0 25 0 1 0 549703100 73166848 14633 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17863 14633 603 41 0 17822 0
vsize: 71452
[startup+300 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15014 0 0 0 29961 40 0 0 25 0 1 0 549703100 73166848 14645 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17863 14645 603 41 0 17822 0
vsize: 71452
[startup+310 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15019 0 0 0 30961 40 0 0 25 0 1 0 549703100 73302016 14650 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17896 14650 603 41 0 17855 0
vsize: 71584
[startup+320.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15028 0 0 0 31962 40 0 0 25 0 1 0 549703100 73302016 14659 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17896 14659 603 41 0 17855 0
vsize: 71584
[startup+330 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15038 0 0 0 32962 40 0 0 25 0 1 0 549703100 73302016 14669 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17896 14669 603 41 0 17855 0
vsize: 71584
[startup+340.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15045 0 0 0 33962 40 0 0 25 0 1 0 549703100 73302016 14676 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17896 14676 603 41 0 17855 0
vsize: 71584
[startup+350 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15050 0 0 0 34962 40 0 0 25 0 1 0 549703100 73437184 14681 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17929 14681 603 41 0 17888 0
vsize: 71716
[startup+360.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15055 0 0 0 35963 40 0 0 25 0 1 0 549703100 73437184 14686 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17929 14686 603 41 0 17888 0
vsize: 71716
[startup+370.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15064 0 0 0 36963 40 0 0 25 0 1 0 549703100 73437184 14695 4294967295 134512640 134672761 3221224544 3221223760 134557677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17929 14695 603 41 0 17888 0
vsize: 71716
[startup+380.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15079 0 0 0 37963 40 0 0 25 0 1 0 549703100 73437184 14710 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17929 14710 603 41 0 17888 0
vsize: 71716
[startup+390.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15087 0 0 0 38963 40 0 0 25 0 1 0 549703100 73437184 14718 4294967295 134512640 134672761 3221224544 3221223716 134556680 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15088 0 0 0 39963 40 0 0 25 0 1 0 549703100 73572352 14719 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15092 0 0 0 40963 40 0 0 25 0 1 0 549703100 73572352 14723 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17962 14723 603 41 0 17921 0
vsize: 71848
[startup+420.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15097 0 0 0 41963 40 0 0 25 0 1 0 549703100 73572352 14728 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17962 14728 603 41 0 17921 0
vsize: 71848
[startup+430.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15105 0 0 0 42963 40 0 0 25 0 1 0 549703100 73572352 14736 4294967295 134512640 134672761 3221224544 3221223760 134561987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17962 14736 603 41 0 17921 0
vsize: 71848
[startup+440.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15109 0 0 0 43964 40 0 0 25 0 1 0 549703100 73572352 14740 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17962 14740 603 41 0 17921 0
vsize: 71848
[startup+450.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15115 0 0 0 44964 40 0 0 25 0 1 0 549703100 73572352 14746 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17962 14746 603 41 0 17921 0
vsize: 71848
[startup+460.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15118 0 0 0 45964 40 0 0 25 0 1 0 549703100 73572352 14749 4294967295 134512640 134672761 3221224544 3221223696 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17962 14749 603 41 0 17921 0
vsize: 71848
[startup+470.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15123 0 0 0 46964 40 0 0 25 0 1 0 549703100 73572352 14754 4294967295 134512640 134672761 3221224544 3221223808 134562262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17962 14754 603 41 0 17921 0
vsize: 71848
[startup+480.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15127 0 0 0 47964 40 0 0 25 0 1 0 549703100 73707520 14758 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17995 14758 603 41 0 17954 0
vsize: 71980
[startup+490.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15130 0 0 0 48964 40 0 0 25 0 1 0 549703100 73707520 14761 4294967295 134512640 134672761 3221224544 3221223668 134566049 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15130 0 0 0 49965 40 0 0 25 0 1 0 549703100 73707520 14761 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17995 14761 603 41 0 17954 0
vsize: 71980
[startup+510.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15132 0 0 0 50965 40 0 0 25 0 1 0 549703100 73707520 14763 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15134 0 0 0 51965 40 0 0 25 0 1 0 549703100 73707520 14765 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17995 14765 603 41 0 17954 0
vsize: 71980
[startup+530.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15135 0 0 0 52965 40 0 0 25 0 1 0 549703100 73707520 14766 4294967295 134512640 134672761 3221224544 3221223760 134561999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17995 14766 603 41 0 17954 0
vsize: 71980
[startup+540.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15138 0 0 0 53965 40 0 0 25 0 1 0 549703100 73707520 14769 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17995 14769 603 41 0 17954 0
vsize: 71980
[startup+550.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15142 0 0 0 54965 40 0 0 25 0 1 0 549703100 73707520 14773 4294967295 134512640 134672761 3221224544 3221223728 134556675 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15142 0 0 0 55965 40 0 0 25 0 1 0 549703100 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+570.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15142 0 0 0 56965 40 0 0 25 0 1 0 549703100 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.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15143 0 0 0 57966 40 0 0 25 0 1 0 549703100 73707520 14774 4294967295 134512640 134672761 3221224544 3221223748 134561964 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15145 0 0 0 58966 40 0 0 25 0 1 0 549703100 73707520 14776 4294967295 134512640 134672761 3221224544 3221223716 134556653 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15146 0 0 0 59966 40 0 0 25 0 1 0 549703100 73707520 14777 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15146 0 0 0 60966 40 0 0 25 0 1 0 549703100 73707520 14777 4294967295 134512640 134672761 3221224544 3221223716 134556649 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15147 0 0 0 61966 40 0 0 25 0 1 0 549703100 73707520 14778 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15148 0 0 0 62967 40 0 0 25 0 1 0 549703100 73707520 14779 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17995 14779 603 41 0 17954 0
vsize: 71980
[startup+640.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15150 0 0 0 63967 40 0 0 25 0 1 0 549703100 73707520 14781 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17995 14781 603 41 0 17954 0
vsize: 71980
[startup+650.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15151 0 0 0 64967 40 0 0 25 0 1 0 549703100 73707520 14782 4294967295 134512640 134672761 3221224544 3221223760 134557662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17995 14782 603 41 0 17954 0
vsize: 71980
[startup+660.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15153 0 0 0 65967 40 0 0 25 0 1 0 549703100 73707520 14784 4294967295 134512640 134672761 3221224544 3221223716 134556667 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15154 0 0 0 66967 40 0 0 25 0 1 0 549703100 73707520 14785 4294967295 134512640 134672761 3221224544 3221223716 134556643 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15155 0 0 0 67967 40 0 0 25 0 1 0 549703100 73707520 14786 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17995 14786 603 41 0 17954 0
vsize: 71980
[startup+690.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15156 0 0 0 68968 40 0 0 25 0 1 0 549703100 73707520 14787 4294967295 134512640 134672761 3221224544 3221223716 134556596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17995 14787 603 41 0 17954 0
vsize: 71980
[startup+700.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15159 0 0 0 69968 40 0 0 25 0 1 0 549703100 73707520 14790 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17995 14790 603 41 0 17954 0
vsize: 71980
[startup+710.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15161 0 0 0 70968 40 0 0 25 0 1 0 549703100 73707520 14792 4294967295 134512640 134672761 3221224544 3221223716 134556653 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.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15161 0 0 0 71968 40 0 0 25 0 1 0 549703100 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+730 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15162 0 0 0 72968 40 0 0 25 0 1 0 549703100 73707520 14793 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17995 14793 603 41 0 17954 0
vsize: 71980
[startup+740.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15168 0 0 0 73968 41 0 0 25 0 1 0 549703100 73842688 14799 4294967295 134512640 134672761 3221224544 3221223716 134556598 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 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15168 0 0 0 74968 41 0 0 25 0 1 0 549703100 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+760 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15168 0 0 0 75968 41 0 0 25 0 1 0 549703100 73842688 14799 4294967295 134512640 134672761 3221224544 3221223712 134564459 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14799 603 41 0 17987 0
vsize: 72112
[startup+769.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15168 0 0 0 76968 41 0 0 25 0 1 0 549703100 73842688 14799 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14799 603 41 0 17987 0
vsize: 72112
[startup+779.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15169 0 0 0 77969 41 0 0 25 0 1 0 549703100 73842688 14800 4294967295 134512640 134672761 3221224544 3221223716 134556632 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 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15169 0 0 0 78969 41 0 0 25 0 1 0 549703100 73842688 14800 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14800 603 41 0 17987 0
vsize: 72112
[startup+799.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15170 0 0 0 79969 41 0 0 25 0 1 0 549703100 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+809.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15171 0 0 0 80969 41 0 0 25 0 1 0 549703100 73842688 14802 4294967295 134512640 134672761 3221224544 3221223752 134561960 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14802 603 41 0 17987 0
vsize: 72112
[startup+819.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15171 0 0 0 81969 41 0 0 25 0 1 0 549703100 73842688 14802 4294967295 134512640 134672761 3221224544 3221223716 134556596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14802 603 41 0 17987 0
vsize: 72112
[startup+829.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15171 0 0 0 82969 41 0 0 25 0 1 0 549703100 73842688 14802 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14802 603 41 0 17987 0
vsize: 72112
[startup+839.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15171 0 0 0 83969 41 0 0 25 0 1 0 549703100 73842688 14802 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14802 603 41 0 17987 0
vsize: 72112
[startup+849.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15174 0 0 0 84969 41 0 0 25 0 1 0 549703100 73842688 14805 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14805 603 41 0 17987 0
vsize: 72112
[startup+859.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15174 0 0 0 85970 41 0 0 25 0 1 0 549703100 73842688 14805 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14805 603 41 0 17987 0
vsize: 72112
[startup+869.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15175 0 0 0 86970 41 0 0 25 0 1 0 549703100 73842688 14806 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14806 603 41 0 17987 0
vsize: 72112
[startup+879.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15179 0 0 0 87970 41 0 0 25 0 1 0 549703100 73842688 14810 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18028 14810 603 41 0 17987 0
vsize: 72112
[startup+889.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15179 0 0 0 88970 41 0 0 25 0 1 0 549703100 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+899.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15179 0 0 0 89970 41 0 0 25 0 1 0 549703100 73842688 14810 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14810 603 41 0 17987 0
vsize: 72112
[startup+909.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15179 0 0 0 90970 41 0 0 25 0 1 0 549703100 73842688 14810 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14810 603 41 0 17987 0
vsize: 72112
[startup+919.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15180 0 0 0 91970 41 0 0 25 0 1 0 549703100 73842688 14811 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14811 603 41 0 17987 0
vsize: 72112
[startup+929.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15182 0 0 0 92970 41 0 0 25 0 1 0 549703100 73842688 14813 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14813 603 41 0 17987 0
vsize: 72112
[startup+939.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15183 0 0 0 93971 41 0 0 25 0 1 0 549703100 73842688 14814 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14814 603 41 0 17987 0
vsize: 72112
[startup+949.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15183 0 0 0 94971 41 0 0 25 0 1 0 549703100 73842688 14814 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14814 603 41 0 17987 0
vsize: 72112
[startup+959.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15184 0 0 0 95971 41 0 0 25 0 1 0 549703100 73842688 14815 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14815 603 41 0 17987 0
vsize: 72112
[startup+969.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15185 0 0 0 96971 41 0 0 25 0 1 0 549703100 73842688 14816 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14816 603 41 0 17987 0
vsize: 72112
[startup+979.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15185 0 0 0 97971 41 0 0 25 0 1 0 549703100 73842688 14816 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14816 603 41 0 17987 0
vsize: 72112
[startup+989.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15185 0 0 0 98971 41 0 0 25 0 1 0 549703100 73842688 14816 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14816 603 41 0 17987 0
vsize: 72112
[startup+999.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15185 0 0 0 99972 41 0 0 25 0 1 0 549703100 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+1010 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15185 0 0 0 100972 41 0 0 25 0 1 0 549703100 73842688 14816 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14816 603 41 0 17987 0
vsize: 72112
[startup+1020 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15195 0 0 0 101972 41 0 0 25 0 1 0 549703100 73842688 14826 4294967295 134512640 134672761 3221224544 3221223716 134556634 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 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15195 0 0 0 102972 41 0 0 25 0 1 0 549703100 73842688 14826 4294967295 134512640 134672761 3221224544 3221223724 134556590 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 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15195 0 0 0 103972 41 0 0 25 0 1 0 549703100 73842688 14826 4294967295 134512640 134672761 3221224544 3221223716 134556618 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 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15195 0 0 0 104973 41 0 0 25 0 1 0 549703100 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+1060 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15195 0 0 0 105973 41 0 0 25 0 1 0 549703100 73842688 14826 4294967295 134512640 134672761 3221224544 3221223668 134566012 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 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15195 0 0 0 106973 41 0 0 25 0 1 0 549703100 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+1080 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15195 0 0 0 107973 41 0 0 25 0 1 0 549703100 73842688 14826 4294967295 134512640 134672761 3221224544 3221223716 134556634 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 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15195 0 0 0 108973 41 0 0 25 0 1 0 549703100 73842688 14826 4294967295 134512640 134672761 3221224544 3221223716 134556627 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 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15195 0 0 0 109973 41 0 0 25 0 1 0 549703100 73842688 14826 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14826 603 41 0 17987 0
vsize: 72112
[startup+1110 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15196 0 0 0 110974 41 0 0 25 0 1 0 549703100 73842688 14827 4294967295 134512640 134672761 3221224544 3221223716 134556598 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 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15196 0 0 0 111974 41 0 0 25 0 1 0 549703100 73842688 14827 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14827 603 41 0 17987 0
vsize: 72112
[startup+1130 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15197 0 0 0 112974 41 0 0 25 0 1 0 549703100 73842688 14828 4294967295 134512640 134672761 3221224544 3221223716 134556602 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 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15197 0 0 0 113974 41 0 0 25 0 1 0 549703100 73842688 14828 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14828 603 41 0 17987 0
vsize: 72112
[startup+1150 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15198 0 0 0 114974 41 0 0 25 0 1 0 549703100 73842688 14829 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14829 603 41 0 17987 0
vsize: 72112
[startup+1160 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15199 0 0 0 115974 41 0 0 25 0 1 0 549703100 73842688 14830 4294967295 134512640 134672761 3221224544 3221223716 134556606 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18028 14830 603 41 0 17987 0
vsize: 72112
[startup+1170 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15202 0 0 0 116974 41 0 0 25 0 1 0 549703100 73842688 14833 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14833 603 41 0 17987 0
vsize: 72112
[startup+1180 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15204 0 0 0 117974 41 0 0 25 0 1 0 549703100 73842688 14835 4294967295 134512640 134672761 3221224544 3221223736 134556585 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 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15204 0 0 0 118974 41 0 0 25 0 1 0 549703100 73842688 14835 4294967295 134512640 134672761 3221224544 3221223728 134556675 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 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19474
Raw data (stat): 19474 (minisat+) R 19473 3260 3259 0 -1 0 15204 0 0 0 119974 41 0 0 25 0 1 0 549703100 73842688 14835 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18028 14835 603 41 0 17987 0
vsize: 72112
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 19474
Raw data (stat): 19474 (minisat+) Z 19473 3260 3259 0 -1 12 15206 0 0 0 119974 44 0 0 25 0 1 0 549703100 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.03
CPU time (s): 1200.2
CPU user time (s): 1199.75
CPU system time (s): 0.448931
CPU usage (%): 100.014
Max. virtual memory (Kb): 72112
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####